Control dependency computation fix #1858

danpoe · 2018-02-16T16:47:19Z

Fixes a bug in the control dependency computation of the dependency graph (see regression test goto-instrument/dependence-graph4)

hannes-steffenhagen-diffblue · 2018-02-16T16:56:16Z

Can you explain in more detail what you are doing here? What bug are you fixing here? Also, this seems to be a fairly significant change in the code - is this also a significant change in behavior, or did you combine your bug fix with a refactoring?

danpoe · 2018-02-19T15:49:33Z

The PR does three things:

(1)

It fixes a bug in the control dependency computation. Previously in transform() only the control dependencies in the set control_deps (plus gotos and assumes at the from location) were considered candidates for the control dependencies at the to location. With this scheme however one misses control dependencies when there are nested if statements.

We use the following definition of control dependencies: A node N is control dependent on a node M iff N postdominates one but not all of M's CFG successors.

Consider the following example:

 1 void main(void)
 2 {
 3   if (a)
 4   {
 5     if (b)
 6       c=0; // no cd on if(a)
 7     else
 8       c=1; // no cd on if(a)
 9
10     d = 1; // cd on if(a)
11   }
12 }

Lines 6 and 8 do not have a control dependency on line 3, line 10 does have a control dependency on line 3. However, the previous implementation missed the latter dependency. The reason is that when computing the control dependencies at a node (e.g., line 10), only the control dependencies at the CFG predecessors (in this case lines 6 and 8) were considered candidates for the control dependencies.

This PR introduces a new set control_dep_candidates in addition to control_deps, which contains all control statements encountered so far.

(2)

It fixes an issue where merge() did not return true in a case where it should. The dependency graph has special handling for function entry edges (in transform()) where it merges the current state into the state of the return location before entering the function. This may change the abstract state at the return location. When later the function exit edge is handled, the merge() into the return location may not change the state, thus merge() may not return true, and thus the return location may not be inserted into the worklist of the fixpoint computation when it should.

This PR introduces a flag has_changed that records whether the abstract state has changed on the handling of the function entry edge. On the function return edge later, merge() checks the flag to know whether it needs to return true.

(3)

It simplifies the merging of the abstract states.

thk123 · 2018-02-20T16:57:35Z

It would be helpful to have these as separate commits (or even PRs) to make it easier to review.

For 3), does this PR help to address that/make it worse: #1843 In any case, could you have use goto_programt::get_function_id

thk123

I don't fully understand the definition of the control dependency so going to pause reviewing. How come in your example line 6 doesn't have control dependency on line 3? My reading of your definition led me to,

3 -> 5 -> 6 -> 10 (postdominates one)
3 -> 5 -> 7 -> 8 -> 10 (doesn't postdominate them all)

thk123 · 2018-02-20T16:58:26Z

regression/goto-analyzer/dependence-graph4/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--show --dependence-graph --text -


What's with the dash at the end?

--text takes an argument which is the file to print to, - means print to stdout.

thk123 · 2018-02-20T16:59:36Z

regression/goto-analyzer/dependence-graph4/test.desc

+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+Control dependencies: .\n\s*\n.*\n\s*g_out = 1;


I've not looked a the output of --dependence-graph, but what does the presence of this line signify? Should you be checking t=1 is not present?

Consider converting this to a unit test so you can be more precise.

It checks that there is a control dependency (the previous version wrongly reported no control dependency). It does however not check that the control dependency is to the correct instruction. This seems not to be possible easily in regression tests as control dependencies are reported as location numbers which are not stable across different systems.

I'll add a unit test for this.

thk123 · 2018-02-20T17:00:46Z

src/analyses/dependence_graph.cpp


-  depst::iterator it=control_deps.begin();
-  for(const auto &c_dep : src.control_deps)
+  if((has_values.is_false() || has_changed) &&


has_changed already includes the case that has_values.is_false()? I this is just has_changed && data_deps.empty()

thk123 · 2018-02-20T17:02:32Z

src/analyses/dependence_graph.cpp

  }
 }

+bool dep_graph_domaint::merge_control_dependencies(
+  const depst &other_control_deps,


To reduce the cognitive load, it would be great if all deps could be renamed to dependencies

thk123 · 2018-02-20T17:06:21Z

src/analyses/dependence_graph.cpp

+
+  // Merge control dependencies
+
+  size_t n=control_deps.size();


Perhaps n could be original_control_deps_size

thk123 · 2018-02-20T17:06:39Z

src/analyses/dependence_graph.cpp

+
+  // Merge control dependency candidates
+
+  n=control_dep_candidates.size();


And this n could be original_control_dep_candidate_size

thk123 · 2018-02-20T17:08:41Z

src/analyses/dependence_graph.cpp

@@ -189,37 +214,42 @@ void dep_graph_domaint::transform(
  ai_baset &ai,
  const namespacet &ns)
 {
+  INVARIANT(!has_values.is_false(),


PRECONDITION probably makes more sense here

thk123 · 2018-02-20T17:09:14Z

src/analyses/dependence_graph.cpp


  // propagate control dependencies across function calls
  if(from->is_function_call())
  {
-    if(from->function == to->function)
+    goto_programt::const_targett next=from;


const goto_programt::const_targett next=std::next(from);

thk123 · 2018-02-20T17:10:03Z

src/analyses/dependence_graph.cpp

      dep_graph_domaint *s=
        dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));
-      assert(s!=nullptr);


Why is this assert no longer required?

martin-cs · 2018-02-20T20:03:52Z

src/analyses/dependence_graph.cpp

-      pd.cfg.entry_map.find(*it);
-
-    assert(e!=pd.cfg.entry_map.end());
+      pd.cfg.entry_map.find(cd);


Is this assertion no longer true?

martin-cs · 2018-02-20T20:05:43Z

src/goto-programs/goto_program_template.h

+
+    return l->function;
+  }
+


Didn't we just remove this method?

Indeed 5df3fca removes this method. It seems that since by f443b18 cbmc does not do partial inlining anymore, the function field of an instruction is now guaranteed to contain the id of the function it is in. I'll remove the method again.

(In goto-instrument there are still a few cases where the function field is not adjusted when the inliner is called explicitely, but we can fix this in the future.)

martin-cs · 2018-02-20T20:07:43Z

I'm tempted to be lazy and say +1 "what @thk123" said. Separate commits would be great. The brilliant explanations here : #1858 (comment) as commit messages would be even better.

danpoe · 2018-02-22T17:20:34Z

@thk123 Line 6 does not have a control dependency on line 3 as it does not postdominate a CFG successor of line 3 (i.e., postdominates_one is false). The two CFG successors of line 3 are line 5 and line 11. Starting from line 5, line 6 does not occur on all paths to the exit point. Similarly, starting from line 11, line 6 also does not occur on all paths to the exit point. Thus, line 6 does not postdominate a CFG successor of line 3.

danpoe · 2018-02-22T17:42:56Z

I'll split the PR up into several commits.

smowton

Main problem here: this absolutely cries out for a reasonably-thorough batch of test cases, since this is the 3rd slicer correctness fix to be PR'd in the last 6 months.

smowton · 2018-02-26T09:08:45Z

src/analyses/dependence_graph.cpp

-    }
-    else if(it!=data_deps.end())
-      ++it;
+    data_deps = src.data_deps;


Explain why when our own data deps are non-empty, we don't use src's data deps at all?

We wouldn't actually need a fixpoint computation for the data dependency analysis as it merely uses the result of the prior reaching definitions analysis to compute the data dependencies at each location. For this we need to inspect each location only once. Thus if the set data_deps is non-empty it means we have handled that location already.

That's one reason why it may be good to split up the data dependency and control dependency analysis (see issue #1859), and then implement the data dependency analysis without ait by simply iterating over all instructions.

smowton · 2018-02-26T09:12:04Z

src/analyses/dependence_graph.cpp

+  // The "successor" above refers to an immediate successor of M.
+
+  // Candidates for M for "to" are "from" and all existing control
+  // dependencies on nodes. "from" is added if it is a goto or assume


"all existing control dependencies on nodes" is less clear than the original phrasing I think. How about "all nodes X such that N is control-dependent on X"

I just realized that this comment is not accurate anymore in the fixed version. Now we consider all control statements in the current function from which there is a path to the current statement (i.e., to) as potential sources of control dependency edges. I'll add a comment to explain this.

smowton · 2018-02-26T09:15:46Z

src/analyses/dependence_graph.cpp


-    // check all CFG successors
+  for(const auto &cd : control_dep_candidates)


I think this bit is just cleanup for clarity and not a substantial change? If so, if not already, move it into a different commit than the substantial change.

The set control_dep_candidates was introduced in the fix so this is new code.

smowton · 2018-02-26T09:21:39Z

src/analyses/dependence_graph.cpp

+
+  size_t n = control_deps.size();
+
+  control_deps.insert(other_control_deps.begin(), other_control_deps.end());


It seems a shame to degrade the previous more-efficient algorithm that makes a single walk over the target set into this one that makes |other_control_deps| searches from the root. If it bothers you that the old algorithm is less clear, how about factoring it into a util called union_ordered_range or something?

Indeed. I assumed that it would implement the same algorithm if both ranges are sorted but it's not the case. I'll add a union_ordered_range utility function.

danpoe · 2018-02-26T12:25:39Z

@smowton I'll add some more dependence graph tests.

danpoe · 2018-04-26T11:02:59Z

@smowton, @thk123, @martin-cs: CI is passing and I've addressed all the comments. I think this is now ready to be merged.

thk123

Changes and commits look good.
Some requests for docs
I am not familiar enough with this to work out if the tests are correct - though it would be easier to check them if there was a comment at the bottom of the desc decoding the regex to see what is expected

thk123 · 2018-05-01T12:37:22Z

src/util/container_utils.h

+#define CPROVER_UTIL_CONTAINER_UTILS_H
+
+template <class C>
+bool union_ordered_range(C &target, const C &source)


Document please

In particular any requirements on what C can be (e.g. iterable, ordered?)

thk123 · 2018-05-01T12:41:29Z

src/analyses/dependence_graph.h

@@ -162,7 +162,9 @@ class dep_graph_domaint:public ai_domain_baset
  node_indext node_id;

  typedef std::set<goto_programt::const_targett> depst;
-  depst control_deps, data_deps;
+  depst control_deps;
+  depst control_dep_candidates;


It would be good to document here what the difference between a control dependency and a control dependency candidate is

thk123 · 2018-05-01T12:42:45Z

src/analyses/dependence_graph.cpp


-    // check all CFG successors
+  for(const auto &cd : control_dep_candidates)


Expand cd (and possibly call it control_dep_candidate since it is a candidate not a control dependency(?? - I don't really know the difference)

thk123 · 2018-05-01T12:43:27Z

src/analyses/dependence_graph.cpp


-    assert(e!=pd.cfg.entry_map.end());
+    INVARIANT(
+      e != pd.cfg.entry_map.end(), "cfg has an entry for every location");


The wording for this invariant is a little confusing - do you mean cfg should have an entry for every location?

thk123 · 2018-05-01T12:46:19Z

src/analyses/dependence_graph.cpp

@@ -27,19 +27,20 @@ bool dep_graph_domaint::merge(
  goto_programt::const_targett from,


Nit: this commit message (Fix issue where merge() did not return true in the dependence graph w) isn't rendering correctly so I suggest the title is too long. Suggest making the short text:

Make dependency graph merge() return true when abstract state changes

I think that is short enough

thk123 · 2018-05-01T12:51:39Z

src/analyses/dependence_graph.cpp

  {
-    has_values = tvt::unknown();
    data_deps = src.data_deps;


Suggest something like the above comment goes into the code as this is entirely non-obvious!

It also might be clear to do:

if(changed) { // ... // comment explaining why not if data_deps in non-empty if(!data_deps.empty()) { data_deps = src.data_deps; } }

danpoe · 2018-05-01T19:25:30Z

@thk123 By adding a comment to the desc file which decodes the regex, do you mean adding an example (possibly with some placeholders for e.g. location numbers) for the portion of the output that the regex is designed to match?

thk123 · 2018-05-02T09:58:52Z

Comments can be added after two sets of -- (sorry if you already knew that). Then my suggested comment would be:

CORE
main.c
--dependence-graph --show
activate-multi-line-match
EXIT=0
SIGNAL=0
// First assignment has a control dependency on the if
\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1
// Second assignment has a control dependency on the if
\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2
--
^warning: ignoring
--
Matches:
// IF i < 10 THEN
// Control dependencies: 1
// a = 1
and
// IF i < 10 THEN 
// Control dependencies: 1
// a = 2

Assuming of course I've decoded your regex to approx right thing

thk123

Someone with a good understanding of control dependencies should check the tests!

thk123 · 2018-05-04T09:32:30Z

src/analyses/dependence_graph.cpp


-    assert(e!=pd.cfg.entry_map.end());
+    INVARIANT(
+      e != pd.cfg.entry_map.end(), "cfg has an entry for every location");


The wording here looks the same, I suggest "cfg must have an entry for every location"

Ah yes. I thought I'd change it once #2142 is resolved, but I'll rephrase it now with must.

thk123 · 2018-05-04T09:36:28Z

regression/goto-analyzer/dependence-graph10/test.desc

+// First assignment has a control dependency on the if
+\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 1
+// Second assignment has a control dependency on the if
+\/\/ ([0-9]+).*\n.*IF.*i < 10.*THEN(.*\n)*Control dependencies: \1\n(.*\n){2,3}.*a = 2


There's only one IF i < 10 how come it appears here twice with both dependencies?

That's because a = 1 and a = 2 appear in the then and else branches of this if. So the statements in both branches have a control dependency on the goto that decides which branch to take.

thk123 · 2018-05-04T09:37:40Z

regression/goto-analyzer/dependence-graph10/test.desc

+--
+^warning: ignoring
+--
+The two regexes above match output portions like shown below (with <N> being a


This explanation is great, though I was hoping to have both lines laid about explicitly

thk123 · 2018-05-04T09:40:17Z

regression/goto-analyzer/dependence-graph12/test.desc

+EXIT=0
+SIGNAL=0
+// Assignment has a control dependency on the if
+\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: .*\1.*\n(.*\n){2,3}.*a = 2


Why don't we care what has a dependency on a < 7?

danpoe · 2018-05-04T11:49:42Z

Ok, I've had a chat with @marek-trtik who worked on the slicer recently. He's up for double checking the control dependency regression tests.

marek-trtik

Half done, finish on Tuesday ...

marek-trtik · 2018-05-04T17:15:42Z

regression/goto-analyzer/dependence-graph12/test.desc

+\/\/ ([0-9]+).*\n.*IF.*a < 7.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2
+// Assignment has a control dependency on the second if
+\/\/ ([0-9]+).*\n.*IF.*a < 10.*THEN(.*\n)*Control dependencies: (([0-9]+,\1)|(\1,[0-9]+))\n(.*\n){2,3}.*a = 2
+--


why checking only for a=2 and not also for a=1?

Yes, I can add a check for a = 1 too.

marek-trtik · 2018-05-04T17:15:49Z

regression/goto-analyzer/dependence-graph11/test.desc

+location number). The intention is to check whether the assignment has a control
+dependency on the goto statement.
+
+        // <N> file main.c line 7 function main


The test regexes above actually ignore the line numbers and the comments currently just give examples of the kind of output that they would match. But I can change the line numbers in the output examples to match the tests.

marek-trtik · 2018-05-04T17:15:51Z

regression/goto-analyzer/dependence-graph11/test.desc

+**** 3 file main.c line 9 function main
+Control dependencies: <N>
+
+        // 3 file main.c line 9 function main


marek-trtik · 2018-05-04T17:17:16Z

regression/goto-analyzer/dependence-graph4/test.desc

+**** 3 file main.c line 9 function main
+Control dependencies: <N>
+
+        // 3 file main.c line 9 function main


marek-trtik · 2018-05-04T17:18:58Z

regression/goto-analyzer/dependence-graph4/test.desc

+EXIT=0
+SIGNAL=0
+\/\/ ([0-9]+) file.*\n.*IF.*g_in1.*THEN GOTO(.*\n)*Control dependencies: \1\n\n.*\n.*g_out = 1
+--


Would it be possible to check that neither 10 nor 12 have CD on 7?

Yes, I'll add a check for that too.

marek-trtik · 2018-05-04T17:20:07Z

regression/goto-analyzer/dependence-graph4/main.c

@@ -0,0 +1,16 @@
+int g_in1, g_in2;
+int g_out;


Why global vars and not automatic?

There is no reason for this. The variables do not matter for control dependencies.

marek-trtik

The regression tests look good to me.

marek-trtik · 2018-05-08T11:10:09Z

regression/goto-analyzer/dependence-graph7/test.desc

+**** 4 file main.c line 6 function main
+Control dependencies: <N>
+
+        // 4 file main.c line 6 function main


Should not be here rather line 8 or 9?

It seems that the source location assigned to the back edge of a loop is the source location of the loop head.

marek-trtik · 2018-05-08T11:13:41Z

regression/goto-analyzer/dependence-graph8/test.desc

+location number). The intention is to check whether the assignment has a control
+dependency on the if.
+
+        // <N> file main.c line 6 function main


marek-trtik · 2018-05-08T11:14:01Z

regression/goto-analyzer/dependence-graph8/test.desc

+**** 3 file main.c line 8 function main
+Control dependencies: <N>
+
+        // 3 file main.c line 8 function main


marek-trtik · 2018-05-08T11:21:40Z

regression/goto-analyzer/dependence-graph7/test.desc

+dependency on itself.
+
+Control dependencies: <N>
+Data dependencies: 1


We focus only on CD. So, this info seams to be redundant/misleading? Remove? What do you think?

The dependency graph outputs both the control dependencies and the data dependencies. The regex above ignores the data dependencies actually. But the example here shows the typical output that the dependency graph produces and which would be matched by the above regex.

smowton

One nitpick, otherwise lgtm.

smowton · 2018-05-15T12:37:08Z

src/util/container_utils.h

+/// \param source second input set
+/// \return true iff `target` was changed
+template <class T, class Compare, class Alloc>
+bool util_set_union(


Suggest _union_inplace, since set_union would usually be a binary op that returns a new set.

I'd suggest inplace_set_union as that would be in keeping with the STL's inplace_merge.

Any ideas of how much faster this implementation is over:

std::size_t before = target.size(); decltype(target) tmp; tmp.swap(target); std::set_union(tmp.begin(), tmp.end(), source.begin(), source.end(), target.end()); return target.size() != before;

? Just curious.

I just tried this, with std::set<std::size_t>'s, both sets being of equal size, and the sets containing random values. The runtimes (in microseconds) for the unions are as follows (union1 is the version in the PR). The leftmost column gives the sizes of the two sets being merged.

union1 union2 100 39 75 1K 368 698 10K 3,358 6,704 100K 54,455 104,597 1M 592,993 1,208,903

Thank you!! I suppose that memory allocation is the dominating factor, which of course has to be done from scratch when using std::set_union. So I'd still suggest to rename the function to some variation involving "inplace", and then this PR should just be merged?!

tautschnig

I am confused by the comment "With this scheme however one misses control dependencies when there are nested if statements." -- are you now computing the transitive closure?

tautschnig · 2018-05-15T13:56:51Z

src/util/container_utils.h

+/// \param source second input set
+/// \return true iff `target` was changed
+template <class T, class Compare, class Alloc>
+bool util_set_union(


I'd suggest inplace_set_union as that would be in keeping with the STL's inplace_merge.

Any ideas of how much faster this implementation is over:

std::size_t before = target.size(); decltype(target) tmp; tmp.swap(target); std::set_union(tmp.begin(), tmp.end(), source.begin(), source.end(), target.end()); return target.size() != before;

? Just curious.

danpoe · 2018-05-15T14:19:47Z

We're not computing transitive dependencies. It's just that the bug that this PR fixes appeared when there was an if statement (with both an if and an else branch) within another if statement. Then for the code that follows the inner if statement (and is contained within the outer if statement), we would not report a control dependency on the outer if condition (as shown in the example above).

tautschnig · 2018-05-15T15:15:55Z

[...] we would not report a control dependency on the outer if condition [...]

It's not clear to me whether that should be reported? The control dependency on the outer if is a transitive one, and would be found by looking at the control dependency of the inner if. But maybe I'm misunderstanding.

danpoe · 2018-05-15T15:31:56Z

In the example above, for line 10 currently no control dependency is reported (neither on line 3 nor on line 5). It's correct that it does not have a control dependency on line 5, but we need to report a control dependency on line 3. As no control dependency is currently reported for line 10, there's no dependency chain that we could follow to know that it depends on line 3.

tautschnig · 2018-05-15T15:34:00Z

Thanks a lot for the clarification!

Previously in transform() only the control dependencies in the set control_deps (plus gotos and assumes at the from location) were considered candidates for the control dependencies at the to location. With this scheme however one misses control dependencies when there are nested if statements. We introduce a new set control_dep_candidates in addition to control_deps, which contains all control statements encountered so far.

The dependency graph has special handling for function entry edges (in transform()) where it merges the current state into the state of the return location before entering the function. This may change the abstract state at the return location. When later the function exit edge is handled, the merge() into the return location may not change the state, thus merge() may not return true, and thus the return location may not be inserted into the worklist of the fixpoint computation when it should. We introduce a flag has_changed that records whether the abstract state has changed on the handling of the function entry edge. On the function return edge later, merge() checks the flag to know whether it needs to return true.

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 review from chrisr-diffblue, kroening, martin-cs, peterschrammel, smowton, tautschnig and thk123 as code owners February 16, 2018 16:47

thk123 reviewed Feb 20, 2018

View reviewed changes

martin-cs reviewed Feb 20, 2018

View reviewed changes

tautschnig assigned danpoe Feb 21, 2018

danpoe force-pushed the dependence-graph-fix branch 2 times, most recently from df7fccb to 4ea0d7a Compare February 23, 2018 12:56

smowton reviewed Feb 26, 2018

View reviewed changes

danpoe force-pushed the dependence-graph-fix branch 8 times, most recently from 34df547 to ceb9cdb Compare March 1, 2018 18:06

danpoe force-pushed the dependence-graph-fix branch from ceb9cdb to e243267 Compare April 25, 2018 14:40

danpoe force-pushed the dependence-graph-fix branch from e243267 to 7e0dbf1 Compare April 26, 2018 10:26

thk123 reviewed May 1, 2018

View reviewed changes

danpoe force-pushed the dependence-graph-fix branch from 7e0dbf1 to ad36d5a Compare May 3, 2018 13:49

thk123 approved these changes May 4, 2018

View reviewed changes

danpoe force-pushed the dependence-graph-fix branch from ad36d5a to 79e6377 Compare May 4, 2018 11:42

danpoe requested a review from marek-trtik May 4, 2018 11:50

marek-trtik reviewed May 4, 2018

View reviewed changes

marek-trtik approved these changes May 8, 2018

View reviewed changes

danpoe force-pushed the dependence-graph-fix branch 2 times, most recently from 1f80dfc to a811cb3 Compare May 12, 2018 19:52

smowton approved these changes May 15, 2018

View reviewed changes

tautschnig reviewed May 15, 2018

View reviewed changes

danpoe added 4 commits May 15, 2018 16:58

Simplified state merging in the dependence graph

a408423

More dependence graph tests

7002909

danpoe force-pushed the dependence-graph-fix branch from a811cb3 to 7002909 Compare May 15, 2018 16:04

danpoe merged commit ac6eb21 into diffblue:develop May 15, 2018

danpoe deleted the dependence-graph-fix branch June 2, 2020 17:19


		// Merge control dependency candidates

		n=control_dep_candidates.size();


		// check all CFG successors
		for(const auto &cd : control_dep_candidates)


		size_t n = control_deps.size();

		control_deps.insert(other_control_deps.begin(), other_control_deps.end());

		@@ -27,19 +27,20 @@ bool dep_graph_domaint::merge(
		goto_programt::const_targett from,

Control dependency computation fix #1858

Control dependency computation fix #1858

Conversation

danpoe commented Feb 16, 2018

hannes-steffenhagen-diffblue commented Feb 16, 2018

danpoe commented Feb 19, 2018 • edited Loading

thk123 commented Feb 20, 2018

thk123 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

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

martin-cs commented Feb 20, 2018

danpoe commented Feb 22, 2018

danpoe commented Feb 22, 2018

smowton left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

danpoe Feb 26, 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

danpoe commented Feb 26, 2018

danpoe commented Apr 26, 2018

thk123 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

danpoe commented May 1, 2018

thk123 commented May 2, 2018

thk123 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

danpoe commented May 4, 2018

marek-trtik 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

Choose a reason for hiding this comment

marek-trtik 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

smowton left a comment

danpoe commented Feb 19, 2018 •

edited

Loading

danpoe Feb 26, 2018 •

edited

Loading

danpoe commented May 15, 2018 •

edited

Loading