Dominator analysis: analyse on basic block granularity #5042

smowton · 2019-08-20T17:15:46Z

Our dominator analysis could produce very large data structures because it computed dominator sets on an instruction granularity. In typical programs the basic-block graph is of course considerably smaller, which combined with the worst-case n-squared space complexity of dominator sets can save a great deal of memory.

Of course there are knock-on consequences for users: most are simple, natural_loopst needs a little restructuring, and accelerate et al need some awkward functions to accommodate their desire to edit the program while keeping the analysis up to date (if this is too awful we could insist that it fully recomputes the analysis after each change).

Accelerate has no tests, so it's hard to know if it's still working, but the Java front-end uses dominator analysis for local variable analysis, so the JBMC testsuite provides good testing of cfg_dominatorst (but not natural_loopst)

hannes-steffenhagen-diffblue

Looks fine to me, mostly nitpicks (and because the second commit has a bunch of changes all at once it's a bit hard to review but since a lot of these need to be dragged through pretty winded code paths I'm not sure if this even can be sensibly broken up further)

hannes-steffenhagen-diffblue · 2019-08-21T10:03:59Z

src/goto-programs/goto_program.h

-  Target target) const
+std::list<Target> get_successors(
+  Target target,
+  std::function<bool(const Target &)> is_instruction_out_of_range)


If this is already a template and you're not storing the function anywhere there's no real reason to use std::function here, you could just add the function type as another template parameter (I'm not sure if it's going to matter in this particular instance but since this avoids type erasure it can under some circumstance dramatically affect optimisation, for example in this case the difference is in one case generating a straight loop with virtual function calls and another that's partially unrolled/vectorised).

hannes-steffenhagen-diffblue · 2019-08-21T10:58:56Z

jbmc/src/java_bytecode/java_local_variable_table.cpp

+      const auto &this_var_dom_block =
+        dominator_analysis.cfg[this_var_dom_block_index].block;
+      // Only consider placing variable declarations at the head of
+      // a basic block (which conveniently is always a safe choice, even


I don't know what this means (i.e. why is it a safe choice and why would it not be a safe choice?)

hannes-steffenhagen-diffblue · 2019-08-21T10:59:27Z

src/analyses/cfg_dominators.h

@@ -26,20 +26,44 @@ template <class P, class T, bool post_dom>
 class cfg_dominators_templatet
 {
 public:
-  typedef std::set<T> target_sett;
+  typedef std::set<std::size_t> target_sett;


I'm guessing this is referring to the node indices? In that case, shouldn't this use node_indext?

⛏️ (As a side note, for cases like this I'd also prefer a "strong typedef" i.e. wrapping it in a struct just to avoid accidentally doing things with them they were not meant to do - like comparing them to unrelated indices or adding them together, things like that).

hannes-steffenhagen-diffblue · 2019-08-21T11:01:42Z

src/analyses/cfg_dominators.h

+  /// Returns true if basic block \p lhs [post]dominates \p rhs
+  bool basic_block_dominates(std::size_t lhs, std::size_t rhs) const
+  {
+    return cfg[rhs].dominators.count(lhs);


⛏️ > 0 for additional verbosity? Never a big fan of implicit to-bool conversion myself

hannes-steffenhagen-diffblue · 2019-08-21T11:03:01Z

src/analyses/cfg_dominators.h

+
+  bool basic_block_reachable(std::size_t block) const
+  {
+    return !cfg[block].dominators.empty();


Wouldn't this be false for the first block?

All blocks dominate themselves by definition

(except ones not reachable from the entry point, which are never visited by cfg_dominatorst)

hannes-steffenhagen-diffblue · 2019-08-21T11:13:12Z

src/analyses/cfg_dominators.h

+      return post_dom;
+  }
+
+  UNREACHABLE; // Entry map is inconsistent with block members?


⛏️ I think in this case it might be better to just use a regular invariant and put the comment on that instead

hannes-steffenhagen-diffblue · 2019-08-21T11:14:09Z

src/analyses/cfg_dominators.h

+  if(lhs == rhs)
+    return true;
+
+  const auto lhs_block = cfg.entry_map.at(lhs);


⛏️ Maybe call these block_id or something of the sort

smowton · 2019-08-21T16:36:02Z

@hannes-steffenhagen-diffblue take another look, I had to make the get-basic-block-from-instruction operation cheaper to get acceptable performance, for which I introduced dense_integer_mapt.

Preliminary performance figures, using the same benchmarking example as you did in #1787 (comment)

Examples:

straightline is like v1 in the linked comment: a long straight-line function.
small, medium and largeish are 100, 1000 and 3000 repeats of example v2 in the linked comment (a function with lots of small basic blocks)
blocks is a version of medium with basic blocks of size 3

As with the linked comment, I used dependency-graph to benchmark as a pass that both computes postdoms and then hammers it with queries (58% of runtime is spent in control_dependencies of which almost all of that is postdom queries).

Results:

Straightline: 4.5s -> 0.5s (down 89%)
Blocks: 7.5s -> 6.0s (down 20%)
Small: 0.05s -> 0.04s (unmeasurable)
Medium: 4.6s -> 3.3s (down 28%)
Largeish: 107s -> 61s (down 43%)

So up front this looks to me like we should get a huge win for mostly-straight-line code (as you'd expect from using basic-block form), and moderate wins (20-30%) from code consisting of 2-3 line basic blocks. Unlike #1787 we continue to use Cooper's dominator algorithm, but we shrink the sizes of the sets it tracks using basic-block form, which particularly shows its worth when we deal with large GOTO programs.

smowton · 2019-08-21T16:40:19Z

re: breaking up the PR, a lot of this now introduces and uses a sensible API for dominators, cf. the original code which merrily rummaged in both cfg_dominatorst and cfgt's fields. If this is looking like it might go in then I'll submit those first as cleanups.

smowton · 2019-08-21T16:53:04Z

Best case against the Java testsuite: regression/jbmc/coreModels, down from 3.2s to 1.7s. Total jbmc-CORE test suite time down from 67 to 59 seconds.

smowton · 2019-08-22T17:10:04Z

Have so far split out #5045 #5051 #5055, which should be pretty uncontroversial, and #5049, which floats the dense_integer_mapt concept for cfgt by itself, without the basic-blocks innovation introduced here. I will make one more PR in the morning, to factor out this PR's cleanup changes to natural_loopst, then this one will sit on top of the whole stack.

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.

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.

In order to accept both lvalue and rvalue arguments, their argument must be deduced, not a class template argument (and therefore concretely specified).

Previously this used instruction granularity, which especially combined with a naive dominator set (not a dominator tree) can waste a great deal of time and memory computing and storing the dominator sets. Now that cfg_dominatorst works on a basic-block granularity, natural_loopst does as well.

martin-cs · 2019-08-28T10:24:44Z

@smowton I am listed as a reviewer for this and am happy to do so but I think it might be best to wait until things have been rebased / merged. Correct me if I am wrong.

smowton · 2019-08-28T10:25:20Z

Agreed.

smowton requested review from cesaro, chrisr-diffblue, cristina-david, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, NathanJPhillips, owen-mc-diffblue, peterschrammel, pkesseli, tautschnig and thk123 as code owners August 20, 2019 17:15

hannes-steffenhagen-diffblue approved these changes Aug 21, 2019

View reviewed changes

smowton force-pushed the smowton/feature/dominator-analysis-use-basic-blocks branch from 1a28c15 to c1cac71 Compare August 21, 2019 16:24

smowton force-pushed the smowton/feature/dominator-analysis-use-basic-blocks branch from c1cac71 to a8cbb76 Compare August 27, 2019 15:48

smowton added 4 commits August 27, 2019 17:02

Add dense_integer_mapt type

ebc6099

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

af101ef

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

Add stateless variant of goto_programt::get_successors

08df8dc

smowton force-pushed the smowton/feature/dominator-analysis-use-basic-blocks branch from a8cbb76 to 1f25b16 Compare August 27, 2019 16:06

smowton added 2 commits August 27, 2019 17:31

Fix identity functors

5e5c46c

In order to accept both lvalue and rvalue arguments, their argument must be deduced, not a class template argument (and therefore concretely specified).

smowton force-pushed the smowton/feature/dominator-analysis-use-basic-blocks branch from 1f25b16 to 370fc30 Compare August 27, 2019 16:32

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Dominator analysis: analyse on basic block granularity #5042

Dominator analysis: analyse on basic block granularity #5042

smowton commented Aug 20, 2019

hannes-steffenhagen-diffblue left a comment

hannes-steffenhagen-diffblue Aug 21, 2019

hannes-steffenhagen-diffblue Aug 21, 2019

hannes-steffenhagen-diffblue Aug 21, 2019

hannes-steffenhagen-diffblue Aug 21, 2019

hannes-steffenhagen-diffblue Aug 21, 2019

smowton Aug 21, 2019

smowton Aug 21, 2019

hannes-steffenhagen-diffblue Aug 21, 2019

hannes-steffenhagen-diffblue Aug 21, 2019

smowton commented Aug 21, 2019

smowton commented Aug 21, 2019

smowton commented Aug 21, 2019

smowton commented Aug 22, 2019

martin-cs commented Aug 28, 2019

smowton commented Aug 28, 2019

Dominator analysis: analyse on basic block granularity #5042

Are you sure you want to change the base?

Dominator analysis: analyse on basic block granularity #5042

Conversation

smowton commented Aug 20, 2019

hannes-steffenhagen-diffblue left a 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

Choose a reason for hiding this comment

smowton commented Aug 21, 2019

smowton commented Aug 21, 2019

smowton commented Aug 21, 2019

smowton commented Aug 22, 2019

martin-cs commented Aug 28, 2019

smowton commented Aug 28, 2019