Sharing map sharing statistics #2509

danpoe · 2018-07-02T18:23:16Z

This adds functionality to compute how many nodes are shared between a set of sharing maps.

tautschnig

That's probably very good work, but greater clarity would be appreciated. See details, below.

tautschnig · 2018-07-02T18:24:46Z

unit/util/sharing_map.cpp


 #include <climits>
 #include <random>
+#include <set>


This seems unrelated to the topic of the PR?

The newly introduced functions count_unmarked_nodes() and get_sharing_stats() use std::set which was not used before in the sharing map.

Ah, the comment might refer to the two changed defines. Yes, that's a fix that activates the internal assertions in the unit tests and is technically unrelated to the topic of this PR. Should I make a separate PR for this?

tautschnig · 2018-07-02T18:25:35Z

src/util/sharing_node.h

@@ -151,8 +153,6 @@ SN_TYPE_PAR_DEF class sharing_node_innert : public sharing_node_baset

  d_it &write_internal()
  {
-    SN_ASSERT(data.use_count() > 0);
-


Is there any test that shows that this is wrong (and is now correct)?

This code was already exercised by several tests, but I used the wrong macro names to activate the sharing map/node internal assertions in the unit tests. Thus, none of the internal assertions were enabled and we didn't see the assertion failures. This is corrected by the first commit in this PR.

tautschnig · 2018-07-02T18:26:21Z

src/util/sharing_node.h

-    SN_ASSERT(as_const(this)->find_leaf(k) == nullptr);
+    // we need to check empty() first as the const version of find_leaf() must
+    // not be called on an empty node
+    SN_ASSERT(empty() || as_const(this)->find_leaf(k) == nullptr);


Again, is there a test?

(see comment above)

tautschnig · 2018-07-02T18:31:13Z

src/util/sharing_map.h

@@ -128,6 +134,7 @@ class sharing_mapt
  friend void sharing_map_copy_test();
  friend void sharing_map_collision_test();
  friend void sharing_map_view_test();
+  friend void sharing_map_sharing_stats_test();


At the risk of getting side-tracked: couldn't those tests be implemented by deriving a new child that provides more access? Those far-away friends are a bit of a pain point...

Do you mean deriving a new class from sharing_mapt in the unit tests which has public methods that wrap the protected members that we want to test? Alternatively, we could also derive a new class from sharing_mapt in the unit tests which then includes those friend declarations above.

What is the issue with the current approach though? Since the friends declared above are only from the unit tests it seems relatively safe.

Far-away friends are easy to lose touch with. In code terms, I effectively need to git grep to figure out who you are trying to be friends with. Maybe the solution is just adding a comment :-) In practice, adding a new test currently requires touching this code, which really shouldn't be necessary. Hence my preference for deriving a new class from sharing_mapt in the unit tests, which would restrict any changes in unit tests to the unit test code.

Ah, I see. Yeah, I'll derive from sharing_mapt in the unit tests.

tautschnig · 2018-07-02T18:31:52Z

src/util/sharing_map.h

@@ -317,6 +354,11 @@ class sharing_mapt
  void gather_all(const baset &n, const unsigned depth, delta_viewt &delta_view)
    const;

+  unsigned count_unmarked_nodes(


This should almost certainly be std::size_t

tautschnig · 2018-07-02T18:32:56Z

src/util/sharing_map.h

@@ -317,6 +354,11 @@ class sharing_mapt
  void gather_all(const baset &n, const unsigned depth, delta_viewt &delta_view)
    const;

+  unsigned count_unmarked_nodes(
+    bool leafs_only,
+    std::set<void *> &marked,


Phew, what is this meant to be? What can be done using a set of void pointers?

The set marked contains pointers to the nodes with use_count >= 2 that have been visited already during the traversal. It's used to avoid exploring shared subtrees more than once.

The sharing map has two different types of nodes that don't have a common base class, so I used void pointers here to avoid having to keep two separate sets marked for both node types.

allredj

Passed Diffblue compatibility checks (cbmc commit: 7577e52).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/77894414

allredj

Passed Diffblue compatibility checks (cbmc commit: ab4f984).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/79729117

tautschnig · 2018-07-30T18:55:38Z

src/util/sharing_map.h

+  /// only leafs are counted.
+  class sharing_map_statst
+  {
+  public:


I'd just use a struct here as all members are public.

allredj

Passed Diffblue compatibility checks (cbmc commit: 4ae8eb6).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/80509299

6a10f1a Merge pull request diffblue#2462 from tautschnig/vs-goto-inline 96fc7b1 Merge pull request diffblue#2654 from peterschrammel/update-jml8 1847066 Update jbmc/lib/java-models-library to java-models-library#8 (remove sun.* imports) c157ba7 Revert "CMake version.cpp: switch back to add_custom_target" 7a009d6 Merge pull request diffblue#2650 from diffblue/aws-codebuild-clcache 63652fc add clcache to Windows build 6f72b3b Merge pull request diffblue#2657 from smowton/smowton/fix/cmake-version-cpp 35d09d5 CMake version.cpp: switch back to add_custom_target 80331d8 Merge pull request diffblue#2638 from diffblue/CBMC_VERSION_string 7c066f9 Merge pull request diffblue#2618 from owen-jones-diffblue/doc/move-irep-docs-from-util-to-irep ad5c375 use a string instead of macro for version number b6258db Merge pull request diffblue#2509 from danpoe/feature/sharing-map-stats eb71a01 Merge pull request diffblue#2639 from thk123/array-element-type c5519ec Merge pull request diffblue#2640 from allredj/support-for-load-containing-class-only 0855872 Address review comments diffblue#2 eaa7664 Wrap lines properly e682eb9 Add \ref in lots of places 3023cca Address review comments 758f069 Move dstringt documentation to above dstringt a54c82d Move documentation of irept to be above irept b827ea4 Use type equality check in unit tests 77185fd Merge pull request diffblue#2607 from jeannielynnmoulton/jeannie/ParseThrownExceptions2 1f4ef40 Add class loader debug output 4ae8eb6 Move sharing map friends declarations to unit tests 186897c Sharing stats for the sharing map 4438b43 Fix sharing map internal assertion 332febe Remove wrong sharing map internal assertions be7e140 Activate internal checks for the sharing map unit tests 713d3fe Merge pull request diffblue#2636 from polgreen/fix_function_map 87f90ee Add replace_all string utility ea2d393 Make test work on windows 4fa9943 Make array element type be not a comment 655248a Add unit test for when there are no exceptions. a6e7c4b Refactors interface for exceptions to not use irepts. 1134bba Creates java_method_typet which extends code_typet aa83622 Unit tests method get_super_class 565c999 Unit tests throws exceptions parsing. eb88509 Use parsed information for thrown exceptions. 5c7dcac Parses the exception attribute 7fcc42d Adds const to get/set_outer_class 5994dd8 Add method to get super class from java class type. fbad2d9 Rename variable extends to super_class 6d0776f if function is not in the function map, treat as if it has no body da86bdb Merge pull request diffblue#2602 from diffblue/__CPROVER_r/w_ok 0202f34 refactor pointer_validity_check using address_check 4a24ad4 use __CPROVER_r/w_ok in string.c library 732ce2a expand __CPROVER_r/w_ok in goto_check acfea65 __CPROVER_r_ok and __CPROVER_w_ok added to ANSI-C front-end 0618f7d Merge pull request diffblue#2628 from diffblue/clang-extensions 5e43131 Merge pull request diffblue#2608 from diffblue/ms_cl_int64 7c56091 Merge pull request diffblue#2634 from qaphla/local_bitvector_analysis_regression 44ef8d5 Merge pull request diffblue#2630 from diffblue/invalid-pointer-flattening f74c161 test for __float80 and __float128 8288a72 __float80 is a typedef, not a keyword 5495625 FreeBSD: default flavor is now CLANG e63402e added _Null_unspecified clang extension 16a49a7 bugfix: __float128 3849bb0 rename APPLE flavor to CLANG 060b59c separate pointer check for integer addresses 9b5847e fix flattening of ID_invalid_pointer 432dcf1 Added a regression test checking that --pointer-check does not generate excess checks if local_bitvector_analysis can gather information on the pointer being checked. cbfcc5c added support for _int64 keyword 0148347 Avoid signed/unsigned casts and conversion in goto_inline git-subtree-dir: cbmc git-subtree-split: 6a10f1a

danpoe requested review from kroening, peterschrammel, smowton and tautschnig as code owners July 2, 2018 18:23

tautschnig reviewed Jul 2, 2018

View reviewed changes

allredj reviewed Jul 2, 2018

View reviewed changes

danpoe force-pushed the feature/sharing-map-stats branch from 7577e52 to ab4f984 Compare July 23, 2018 12:56

allredj reviewed Jul 23, 2018

View reviewed changes

tautschnig approved these changes Jul 30, 2018

View reviewed changes

danpoe added 5 commits July 31, 2018 14:26

Activate internal checks for the sharing map unit tests

be7e140

Remove wrong sharing map internal assertions

332febe

Fix sharing map internal assertion

4438b43

Sharing stats for the sharing map

186897c

Move sharing map friends declarations to unit tests

4ae8eb6

danpoe force-pushed the feature/sharing-map-stats branch from ab4f984 to 4ae8eb6 Compare July 31, 2018 13:59

danpoe requested a review from pkesseli as a code owner July 31, 2018 13:59

allredj reviewed Jul 31, 2018

View reviewed changes

danpoe merged commit b6258db into diffblue:develop Jul 31, 2018

danpoe deleted the feature/sharing-map-stats branch June 2, 2020 17:18

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Sharing map sharing statistics #2509

Sharing map sharing statistics #2509

danpoe commented Jul 2, 2018

tautschnig left a comment

tautschnig Jul 2, 2018

danpoe Jul 23, 2018 •

edited

Loading

tautschnig Jul 2, 2018

danpoe Jul 23, 2018 •

edited

Loading

tautschnig Jul 2, 2018

danpoe Jul 23, 2018

tautschnig Jul 2, 2018

danpoe Jul 23, 2018

tautschnig Jul 30, 2018

danpoe Jul 31, 2018

tautschnig Jul 2, 2018

tautschnig Jul 2, 2018

danpoe Jul 23, 2018

allredj left a comment

allredj left a comment

tautschnig Jul 30, 2018

allredj left a comment

Sharing map sharing statistics #2509

Sharing map sharing statistics #2509

Conversation

danpoe commented Jul 2, 2018

tautschnig left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danpoe Jul 23, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danpoe Jul 23, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

danpoe Jul 23, 2018 •

edited

Loading

danpoe Jul 23, 2018 •

edited

Loading