cfgt: index entry-map by instruction location number, not the instruction itself by smowton · Pull Request #5049 · diffblue/cbmc

smowton · 2019-08-22T15:32:04Z

Since function location numbers are almost always very dense, we can use a vector rather than a map to get from an instruction to its corresponding cfgt node. The introduced dense_integer_mapt for now has just enough functionality to do this, but could be extended in future to a general-purpose flat-map class a la boost::flat_map.

smowton · 2019-08-22T15:41:21Z

On thinking again, I'll make a "give cfgt a public interface" PR and then base this one on that

smowton · 2019-08-22T16:52:54Z

This is now rebased on #5051 which does all the cleanup work that doesn't depend on the underlying data structure; the final commit that does the real work is now much briefer

peterschrammel · 2019-08-23T16:03:43Z

src/util/dense_integer_map.h

+  {
+  }
+
+  template <typename Iter>


Some documentation for this function would be appreciated

peterschrammel · 2019-08-23T16:04:40Z

src/goto-programs/cfg.h

+/// Functor to convert cfg nodes into dense integers, used by \ref cfg_baset.
+/// Default implementation: the identity function.
+template <class T>
+class cfg_instruction_to_dense_integert


This could do with some unit tests.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: af101ef).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/124782661
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

martin-cs

Only a very small part touches my area of responsibility and that seems fine.

martin-cs · 2019-08-28T10:18:31Z

src/goto-instrument/dump_c.cpp


+  // goto_program2codet requires valid location numbers:
+  tmp.update();
+


This seems like it might fix an obscure bug or two...

This is required because otherwise a cfgt<..., goto_programt::targett> wouldn't be able to accept const_targett as an argument to get_node_index(...) etc, which is undesirable. In particular its own entry_mapt::keys() would not be usable. In general this ought to be some constified version of 'I', but since base `cfgt` is currently restricted to either targett or const_targett then statically specifying const_targett suffices.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: d56ce9e).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/129480980
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

chrisr-diffblue

Looks good, though I agree with @peterschrammel that some unit tests would be good to have.

smowton · 2019-09-30T10:05:32Z

@chrisr-diffblue added, had forgotten to git add...

danpoe

LGTM

danpoe · 2019-09-30T10:31:48Z

src/goto-programs/cfg.h

  /// node indices saves a map lookup, so it can be worthwhile when you expect
  /// to repeatedly look up the same program point.
-  entryt get_node_index(const I &program_point) const
+  entryt get_node_index(const goto_programt::const_targett &program_point) const


Could use pass-by-value 🍐

danpoe · 2019-09-30T10:31:56Z

src/goto-programs/cfg.h


  /// Get the CFG graph node relating to \p program_point.
-  nodet &get_node(const I &program_point)
+  nodet &get_node(const goto_programt::const_targett &program_point)


danpoe · 2019-09-30T10:32:09Z

src/goto-programs/cfg.h


  /// Get the CFG graph node relating to \p program_point.
-  const nodet &get_node(const I &program_point) const
+  const nodet &get_node(const goto_programt::const_targett &program_point) const


danpoe · 2019-09-30T10:33:24Z

src/util/dense_integer_map.h

+  // Main store: contains <key, value> pairs, where entries at positions with
+  // no corresponding key are default-initialised and entries with a
+  // corresponding key but no value set yet have the correct key but a default-
+  // initialized key. Both of these are skipped by this type's iterators.


initialized key -> initialized value

This gives a map-like interface but vector-like lookup cost, ideal for mapping keys that have a bijection with densely packed integers, such as the location numbers of a well-formed goto_modelt or goto_programt.

This saves a lot of allocations, memory, and time when the cfg is frequently queried.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 41585c5).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/129671093
Status will be re-evaluated on next push.
Common spurious failures include: the cbmc commit has disappeared in the mean time (e.g. in a force-push); the author is not in the list of contributors (e.g. first-time contributors); compatibility was already broken by an earlier merge.

codecov-io · 2019-09-30T11:19:22Z

Codecov Report

Merging #5049 into develop will increase coverage by 0.04%.
The diff coverage is 100%.

@@            Coverage Diff             @@
##           develop   #5049      +/-   ##
==========================================
+ Coverage    66.95%     67%   +0.04%     
==========================================
  Files         1146    1147       +1     
  Lines        93823   93842      +19     
==========================================
+ Hits         62823   62881      +58     
+ Misses       31000   30961      -39

Flag	Coverage Δ
#cproversmt2	`42.72% <98.43%> (+0.1%)`	⬆️
#regression	`63.5% <100%> (+0.04%)`	⬆️
#unit	`31.96% <92.3%> (+0.09%)`	⬆️

Impacted Files	Coverage Δ
src/util/dense_integer_map.h	`100% <100%> (ø)`
.../goto-instrument/goto_instrument_parse_options.cpp	`58.05% <100%> (+0.31%)`	⬆️
src/goto-instrument/dump_c.cpp	`74.58% <100%> (-0.14%)`	⬇️
src/goto-programs/cfg.h	`80.21% <100%> (+4.54%)`	⬆️
src/goto-symex/goto_symex.cpp	`99.5% <0%> (-0.14%)`	⬇️
...c/java_bytecode/java_string_library_preprocess.cpp	`96.82% <0%> (-0.02%)`	⬇️
src/goto-symex/goto_symex.h	`92.3% <0%> (ø)`	⬆️
src/goto-instrument/points_to.h	`0% <0%> (ø)`	⬆️
src/analyses/cfg_dominators.h	`100% <0%> (ø)`	⬆️
... and 6 more

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update d8ed6fe...33ceb0a. Read the comment docs.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: 33ceb0a).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/129674156

kroening · 2019-09-30T14:17:44Z

src/goto-programs/cfg.h

+    const auto &instructions = goto_program.instructions;
+    possible_keys.reserve(
+      std::distance(instructions.begin(), instructions.end()));
+    for(auto it = instructions.begin(); it != instructions.end(); ++it)


why std::distance? On a list that's linear.
.size() is constant since C++11.

smowton requested review from chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, owen-mc-diffblue, peterschrammel, pkesseli, tautschnig and thk123 as code owners August 22, 2019 15:32

smowton force-pushed the smowton/feature/dominators-avoid-std-map branch from 6e06a40 to 17e9761 Compare August 22, 2019 16:45

smowton requested review from NathanJPhillips, cesaro and cristina-david as code owners August 22, 2019 16:45

smowton force-pushed the smowton/feature/dominators-avoid-std-map branch from 17e9761 to f55f0cf Compare August 22, 2019 16:52

smowton mentioned this pull request Aug 22, 2019

Dominator analysis: analyse on basic block granularity #5042

Open

smowton force-pushed the smowton/feature/dominators-avoid-std-map branch from f55f0cf to 8f6c82b Compare August 23, 2019 15:46

peterschrammel changed the title ~~cfgt: index entry-map by instruction location number, not the instruction itself~~ cfgt: index entry-map by instruction location number, not the instruction itself [depends: 5051] Aug 23, 2019

peterschrammel added the dependent - do not merge label Aug 23, 2019

peterschrammel reviewed Aug 23, 2019

View reviewed changes

smowton force-pushed the smowton/feature/dominators-avoid-std-map branch from 8f6c82b to be7b9da Compare August 27, 2019 08:01

smowton removed the dependent - do not merge label Aug 27, 2019

smowton changed the title ~~cfgt: index entry-map by instruction location number, not the instruction itself [depends: 5051]~~ cfgt: index entry-map by instruction location number, not the instruction itself Aug 27, 2019

smowton force-pushed the smowton/feature/dominators-avoid-std-map branch 2 times, most recently from 6d96310 to af101ef Compare August 27, 2019 16:03

allredj reviewed Aug 27, 2019

View reviewed changes

martin-cs approved these changes Aug 28, 2019

View reviewed changes

smowton force-pushed the smowton/feature/dominators-avoid-std-map branch 2 times, most recently from d56ce9e to b8a4382 Compare September 27, 2019 16:03

allredj reviewed Sep 27, 2019

View reviewed changes

smowton force-pushed the smowton/feature/dominators-avoid-std-map branch from b8a4382 to 1b5b0ae Compare September 30, 2019 09:26

chrisr-diffblue approved these changes Sep 30, 2019

View reviewed changes

smowton force-pushed the smowton/feature/dominators-avoid-std-map branch from 5cfd752 to 41585c5 Compare September 30, 2019 10:09

danpoe approved these changes Sep 30, 2019

View reviewed changes

smowton added 3 commits September 30, 2019 11:39

Add dense_integer_mapt type

313416a

This gives a map-like interface but vector-like lookup cost, ideal for mapping keys that have a bijection with densely packed integers, such as the location numbers of a well-formed goto_modelt or goto_programt.

cfgt: use dense_integer_mapt to provide instruction -> cfg node mapping

79be445

This saves a lot of allocations, memory, and time when the cfg is frequently queried.

Add unit tests for dense_integer_mapt

33ceb0a

smowton force-pushed the smowton/feature/dominators-avoid-std-map branch from 41585c5 to 33ceb0a Compare September 30, 2019 10:39

allredj reviewed Sep 30, 2019

View reviewed changes

kroening reviewed Sep 30, 2019

View reviewed changes

kroening approved these changes Sep 30, 2019

View reviewed changes

smowton merged commit cd54630 into diffblue:develop Sep 30, 2019


		// goto_program2codet requires valid location numbers:
		tmp.update();

Conversation

smowton commented Aug 22, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smowton commented Aug 22, 2019

Uh oh!

smowton commented Aug 22, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

martin-cs left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

chrisr-diffblue left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Sep 30, 2019

Uh oh!

danpoe left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

codecov-io commented Sep 30, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

smowton commented Aug 22, 2019 •

edited

Loading

codecov-io commented Sep 30, 2019 •

edited

Loading