Document the sharing map, and move sharing map unit tests to catch #1899

danpoe · 2018-03-01T17:24:15Z

No description provided.

tautschnig · 2018-03-02T08:42:34Z

Build failures are genuine:

../src/util/sharing_map.h:486:15: error: unused variable 'c' [-Werror,-Wunused-variable]

It seems that necessitates some changes to sharing_mapt. While at that: would it be possible to please add some documentation that in particular covers 1) complexity of operations and 2) reference counting/garbage collection semantics?

danpoe · 2018-03-02T10:29:50Z

@tautschnig Ok, I'll add some documentation.

hannes-steffenhagen-diffblue · 2018-03-06T14:56:04Z

unit/sharing_map.cpp is currently excluded from the cmake build (unit/CMakeLists.txt, line 11).

Also, the test for sharing_map and sharing_node should probably be under the unit/util directory.

tautschnig · 2018-03-25T19:11:32Z

unit/Makefile

@@ -28,6 +28,7 @@ SRC += unit_tests.cpp \
       java_bytecode/inherited_static_fields/inherited_static_fields.cpp \
       pointer-analysis/custom_value_set_analysis.cpp \
       sharing_node.cpp \
+       sharing_map.cpp \


As @hannes-steffenhagen-diffblue said: these should likely go in the util folder.

tautschnig · 2018-03-25T19:16:11Z

src/util/sharing_map.h

@@ -450,7 +450,7 @@ SHARING_MAPT2(, size_type)::erase(
    return 0;

  node_type *del=nullptr;
-  unsigned del_bit;
+  unsigned del_bit=0;


I'm pretty sure unsigned should not be used here at all and any such use should be a std::size_t instead.

tautschnig · 2018-03-25T19:18:57Z

src/util/sharing_map.h

+///
+/// When inserting a key-value pair into the map, first the hash of its key is
+/// computed. The `bits` number of lower order bits of the hash are deemed
+/// significant, and are grouped into `bits` / `chunk` chunks). The hash is then


The ) does not have a matching opening parenthesis.

tautschnig · 2018-03-25T19:19:49Z

src/util/sharing_map.h

+/// purposes of determining the position of the key-value pair in the trie. The
+/// actual key-value pairs are stored in the leaf nodes. Collisions (i.e., two
+/// different keys yield the same "string"), are handled by chaining the
+/// corresponding key-value pairs in a `std::list`.


Would a std::forward_list be sufficient?

Yes, this is fixed in an upcoming PR.

tautschnig · 2018-03-25T19:32:17Z

src/util/sharing_map.h

@@ -39,6 +39,66 @@ Author: Daniel Poetzl
  CV typename sharing_mapt<keyT, valueT, hashT, predT>::ST \
  sharing_mapt<keyT, valueT, hashT, predT>

+/// A map implemented as a tree where subtrees can be shared between different
+/// maps.


Can you somewhere explain how to generate sharing (likely via copy and/or assignment operations)?

Yes, I'll add an explanation for that.

tautschnig · 2018-03-25T19:41:58Z

Is is possible to add iterator and const_iterator members, or actually provide the same interface that a std::map provides?

danpoe · 2018-04-23T15:47:41Z

A few differences between the interfaces of sharing_mapt and std::map are necessary I think. I'd like to avoid having methods return/take iterators for the reasons below.

std::map is implemented as an RB tree, consisting of nodes that also have pointers to their parents. An iterator thus just needs to keep a pointer to a node. In our tree the nodes do not have parent pointers. An iterator would thus need to keep a stack of parent pointers. Moreover, dereferencing a std::map iterator yields a std::pair, which matches the implementation of std::map which stores key-value pairs as std::pair's internally, whereas sharing_mapt does not store them as std::pair's.

Since an iterator would need to contain a stack, it would cause unnecessary overhead to return an iterator on e.g. a call to find(). The iterator would also be less useful than a std::map iterator:

The elements are not stored in any particular order in sharing_mapt, thus idioms like first retrieving an iterator with find() and then starting to iterate from that position are not meaningful.
Passing an iterator to e.g. insert() in addition to a key as a hint would not be more efficient than just using the key, as when the map is modified all nodes on the path from the root of the tree to the newly inserted element need to be copied if they have use_count > 1 (thus a traversal from the root to the insert position needs to be done in any case).
Using an iterator (i.e. not a const_iterator) to iterate over sharing_mapt would break all the sharing as it would copy all the shared nodes on the assumption that they may be modified which is likely undesirable.

hannes-steffenhagen-diffblue

Looks good to me.

danpoe · 2018-05-17T15:15:33Z

@tautschnig Would you mind if we merge this PR? (it's documentation, plus unit test refactoring, and some smaller fixes). We can move potential further discussions to #2126 or another upcoming PR.

tautschnig · 2018-05-17T15:18:07Z

Looking.

31ef182 Merge pull request diffblue#2208 from diffblue/cleanout-goto-programs 0e84d3e Merge pull request diffblue#2195 from smowton/smowton/feature/smarter-reachability-slicer c801126 Merge pull request diffblue#2209 from diffblue/travis-no-osx-g++ 3487bf7 Reachability slicer: mark reachable code more precisely 85e8451 Merge pull request diffblue#2066 from tautschnig/bv-endianness 5e5eafb Merge pull request diffblue#2191 from smowton/smowton/feature/java-fatal-assertions 8a68ab8 remove g++ build on OS X; this is identical to the clang++ build 48e5b25 Amend faulty long-string test 3f718ba Java: make null-pointer and similar checks fatal 821eb1d remove basic_blocks and goto_program_irep d87c2db Merge pull request diffblue#2203 from diffblue/typed-lookup d77dea3 strongly type the lookup() methods in namespacet 2382f27 Merge pull request diffblue#2193 from martin-cs/feature/correct-instruction-documentation c314272 Merge pull request diffblue#2181 from diffblue/format-expr-constants 514a0a5 Merge pull request diffblue#2167 from diffblue/parse_unwindset_options 0102452 move escape(s) to string_utils f1b6174 use unwindsett in goto-instrument dcc907a introduce unwindsett for unwinding limits 10aeae8 format_expr now does index, c_bool constants, string constants 92b92d6 Correct the documentation of ASSERT : it does not alter control flow. a11add8 Expand the documentation of the goto-program instructions. a06503b Merge pull request diffblue#2197 from tautschnig/fix-help 05e4bc3 Remove stray whitespace previously demanded by clang-format 3261f4d Fix help output of --generate-function-body-options 7c67b23 Merge pull request diffblue#2110 from tautschnig/type-mismatch-exception 18fb262 Merge pull request diffblue#2025 from tautschnig/stack-depth-fix 9191b6a Merge pull request diffblue#2199 from tautschnig/simplifier-typing f99e631 Merge pull request diffblue#2198 from tautschnig/fix-test-desc 1a79a11 stack depth instrumentation: __CPROVER_initialize may be empty a7690ba Merge pull request diffblue#2185 from smowton/smowton/fix/tolerate-ts18661-types fc02e8f Restore returns before writing the simplified binary 49333eb Make restore_returns handle simplified programs 46f7987 Fix perl regular expressioons in regression test descriptions 9fe432b Merge pull request diffblue#1899 from danpoe/sharing-map-catch-unit-tests 9cc6aae Merge pull request diffblue#2081 from hannes-steffenhagen-diffblue/floating_point_simplificiation da19abe Tolerate TS 18661 (_Float32 et al) types a055454 Try all rounding modes when domain is unknown 5f7bc15 Add float support to constant propagator domain 3dc2244 Move adjust_float_expressions to goto-programs 06d8bea Merge pull request diffblue#2187 from diffblue/move-convert-nondet 6d8c3fa Merge pull request diffblue#2189 from thk123/bugfix/json-parser-restart 2ad157f Merge pull request diffblue#2186 from smowton/smowton/fix/call-graph-uninit-field cd54ad7 Corrected state persistence in the json parser 4447be0 Fix uninitialised collect_callsites field in call_grapht ead0aa3 Merge pull request diffblue#2188 from smowton/smowton/fix/init-string-types-without-refine-strings 57988fc Fix String type initialisation when --refine-strings is not active 6a76aff Move convert_nondet to java_bytecode ac6eb21 Merge pull request diffblue#1858 from danpoe/dependence-graph-fix 10b8b09 Merge pull request diffblue#2011 from thomasspriggs/final_classes a154593 Merge pull request diffblue#2087 from danpoe/feature/small-map 7002909 More dependence graph tests 66263ea Make dependence graph merge() return true when abstract state changes 3aa6dca Control dependency computation fix a408423 Simplified state merging in the dependence graph 0315816 Merge pull request diffblue#2180 from thomasspriggs/json_id2string 8941567 Merge pull request diffblue#2124 from smowton/smowton/feature/fallback-function-provider cd04e70 JBMC: use simple method stubbing pass a6b2cda Add Java simple method stubbing pass ec1127c Lazy goto model: hook for driver program to replace or stub functions b6a4382 Remove `id2string` from inside calls to the `json_stringt` constructor. b673ebb Add storage of final modifier status of java classes in `java_class_typet`. a2ad909 Small map 808dade Provide suitable diagnostics for equality-without-matching-types 89cf6fe Throw appropriate exceptions when converting constraints 2ae66c2 Produce a proper error message when catching a std::runtime_error at top level e7b3ade Workaround for Visual Studio loss of CV qualifier bug 1f661f5 Move sharing map and sharing node unit tests to util 47463a3 Use std::size_t instead of unsigned in the sharing map 3e22217 Sharing map documentation e54f740 Fix sharing map compiler warnings bcc489c Move sharing map unit tests to catch 34114b8 Use a specialised endianness map for flattening git-subtree-dir: cbmc git-subtree-split: 31ef182

danpoe requested a review from smowton March 1, 2018 17:24

danpoe force-pushed the sharing-map-catch-unit-tests branch from 9547dde to ed0918d Compare March 1, 2018 18:07

danpoe force-pushed the sharing-map-catch-unit-tests branch from ed0918d to f721a5f Compare March 2, 2018 10:53

danpoe requested review from kroening, peterschrammel and tautschnig as code owners March 2, 2018 10:53

danpoe force-pushed the sharing-map-catch-unit-tests branch from f721a5f to 88ac580 Compare March 5, 2018 16:30

danpoe changed the title ~~Move sharing map unit tests to catch~~ Document the sharing map, and move sharing map unit tests to catch Mar 5, 2018

danpoe force-pushed the sharing-map-catch-unit-tests branch from 88ac580 to f2afe15 Compare March 5, 2018 18:25

tautschnig reviewed Mar 25, 2018

View reviewed changes

tautschnig assigned danpoe Apr 5, 2018

danpoe force-pushed the sharing-map-catch-unit-tests branch 2 times, most recently from 5f35d26 to ca9906e Compare April 23, 2018 17:03

danpoe added 6 commits April 25, 2018 11:21

Move sharing map unit tests to catch

bcc489c

Fix sharing map compiler warnings

e54f740

Sharing map documentation

3e22217

Use std::size_t instead of unsigned in the sharing map

47463a3

Move sharing map and sharing node unit tests to util

1f661f5

Workaround for Visual Studio loss of CV qualifier bug

e7b3ade

danpoe force-pushed the sharing-map-catch-unit-tests branch from 7728f95 to e7b3ade Compare April 25, 2018 11:21

danpoe mentioned this pull request Apr 26, 2018

Sharing map refactoring to reduce memory consumption #2126

Merged

hannes-steffenhagen-diffblue approved these changes May 17, 2018

View reviewed changes

tautschnig approved these changes May 17, 2018

View reviewed changes

tautschnig merged commit 9fe432b into diffblue:develop May 17, 2018

martin-cs mentioned this pull request May 17, 2018

Cleanup 'undefined-function' options to use 'generate-function-body' #2070

Open

danpoe deleted the sharing-map-catch-unit-tests branch June 2, 2020 17:20

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Document the sharing map, and move sharing map unit tests to catch #1899

Document the sharing map, and move sharing map unit tests to catch #1899

danpoe commented Mar 1, 2018

tautschnig commented Mar 2, 2018

danpoe commented Mar 2, 2018

hannes-steffenhagen-diffblue commented Mar 6, 2018

tautschnig Mar 25, 2018

tautschnig Mar 25, 2018

tautschnig Mar 25, 2018

tautschnig Mar 25, 2018

danpoe Apr 23, 2018

tautschnig Mar 25, 2018

danpoe Apr 23, 2018

tautschnig commented Mar 25, 2018

danpoe commented Apr 23, 2018

hannes-steffenhagen-diffblue left a comment

danpoe commented May 17, 2018

tautschnig commented May 17, 2018

Document the sharing map, and move sharing map unit tests to catch #1899

Document the sharing map, and move sharing map unit tests to catch #1899

Conversation

danpoe commented Mar 1, 2018

tautschnig commented Mar 2, 2018

danpoe commented Mar 2, 2018

hannes-steffenhagen-diffblue commented Mar 6, 2018

tautschnig Mar 25, 2018

Choose a reason for hiding this comment

tautschnig Mar 25, 2018

Choose a reason for hiding this comment

tautschnig Mar 25, 2018

Choose a reason for hiding this comment

tautschnig Mar 25, 2018

Choose a reason for hiding this comment

danpoe Apr 23, 2018

Choose a reason for hiding this comment

tautschnig Mar 25, 2018

Choose a reason for hiding this comment

danpoe Apr 23, 2018

Choose a reason for hiding this comment

tautschnig commented Mar 25, 2018

danpoe commented Apr 23, 2018

hannes-steffenhagen-diffblue left a comment

Choose a reason for hiding this comment

danpoe commented May 17, 2018

tautschnig commented May 17, 2018