Symex: propagate assumptions and conditions #4386

smowton · 2019-03-14T15:13:46Z

This propagates simple tests and assumptions (e.g. ASSUME(x == 5), or IF y == null GOTO 1) similar to how assignments are already propagated.

My particular use case is to note that non-exceptional return from a Java function (dominated by IF @inflight_exception != NULL) and a catch block (terminated by @inflight_exception = NULL;) mean that we can be certain that there is no exception still in flight when executing normal code. However as the C tests accompanying this PR indicate, the concept is more general and is likely to have other benefits by eliminating e.g. redundant return-value or error checks.

~~This depends on #4199 (for easier L2 generation number management) and #4379 (to fix byte-update / SMT2 handling exposed by this PR), so please review only the last 5 commits.~~

tautschnig · 2019-03-14T15:22:58Z

src/goto-symex/goto_state.cpp

+      if(
+        previous_state.threads.size() > 1 &&
+        previous_state.write_is_shared(ssa_lhs, ns) ==
+        goto_symex_statet::write_is_shared_resultt::SHARED)


Not a proper review just yet, only poking at what I guessed would be key bits:

Why can't the goal of this PR be addressed completely by putting the RHS value in the propagation map? (And really just this, nothing else.)

I would have assumed the one case where we cannot do this is when we're dealing with shared variables. But now the above condition suggests that it's exactly that case that we do put in the propagation map?

According to our current merge logic, equal L2 generation numbers --> merge is a no-op. We must either introduce the possibility that despite equal L2 generation numbers the constant prop might disagree (moderately costly), or allocate an "administrative" L2 generation, as we do for constant assignment.

I accidentally flipped the condition while refactoring, fixed now.

But doesn't this then introduce spurious merge assignments? And is it actually a problem if constant propagation disagrees?

(the value-set assignment... just seems like we might as well; this way @owen-jones-diffblue's value-set-filtering will have less work to do as we have established a straightforward constant.

Extra merge assignments: yes, harmless but some noise, indeed. We must do something about the constant propagator, or else the knowledge will outlive the code dominated by the branch or test.

Basically would you rather handle this through the L2 mechanism, or pay cost prop. to the size of the propagator map at each branch to merge them?

Maybe it's worth adding an extra set of irep_idt that lists the constants inferred that way, and is then consulted at join points?

Happy to do that -- will appeal to @kroening for an opinion before doing it though

smowton · 2019-03-14T16:01:05Z

The win32 CI failure is inherited from #4199

allredj

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

owen-mc-diffblue · 2019-03-15T06:52:34Z

src/goto-symex/goto_state.h

@@ -82,6 +82,11 @@ class goto_statet
    value_set = std::move(other_state.value_set);
  }

+  void apply_condition(


Please briefly document this function

Documented at definition site

owen-mc-diffblue · 2019-03-15T06:53:06Z

src/goto-symex/symex_goto.cpp

@@ -22,6 +22,28 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/dirty.h>
 #include <util/simplify_expr.h>

+static void apply_goto_condition(


Please briefly document this function

owen-mc-diffblue · 2019-03-15T06:56:11Z

src/goto-symex/symex_goto.cpp

+    if(!symex_config.doing_path_exploration)
+    {
+      // In --paths mode we would require the GOTO condition as a constraint
+      // as well, effectively treating the branch like an assumption.


I don't understand this comment. Possibly the condition is inverted by mistake.

smowton · 2019-03-15T10:39:38Z

@owen-jones-diffblue all comments applied

owen-mc-diffblue · 2019-03-15T13:05:39Z

src/goto-symex/goto_state.cpp

+/// assumption or a GOTO condition that we just passed through, we can propagate
+/// the constant '5' for future 'x' references. If the condition is (y == &o1)
+/// then we can use that to populate the value set.
+/// \param condition: condition that must hold on this path


Should you mention that this should be L2? There's a short end-of-line comment to that effect in the declaration.

No behavioural change.

This enables us to more conveniently allocate a new generation on a non-current state, such as a state copy that will be used on a pending branch. No behavioural change.

l2_thread_write_encoding both makes a quite complicated test regarding whether a write is to be considered shared state, and also enacts some side-effects for both shared and non-shared state. This splits part of its testing into write_is_shared. No behavioural change.

smowton · 2019-03-15T16:59:37Z

This is now rebased and ready to go.

peterschrammel

LGTM

allredj

Change looks sensible, but if the purpose is performance, it would be nice to post some performance results to at least check that there is no slowdown.

allredj · 2019-03-18T12:18:26Z

jbmc/regression/jbmc/exception-cleanup/Test.java

+    }
+
+    // Try it once more, to check we also know after an unreachable catch that
+    // there is still no inflight exception


💡 A test with nested try-catch would be useful to prove that point.

Such a case actually does not work yet, because symex can't tell that all exceptions were caught (i.e. the catch dispatch table is exhaustive). The reason is it isn't yet smart enough to notice that upon entering the catch block the incoming pointer cannot be null, and therefore e instanceof Exception certainly succeeds (null instanceof A returns false for any A).

Fixing that is my next task!

You could add a KNOWNBUG test for it now and turn it on as part of your next task.

allredj · 2019-03-18T12:20:17Z

jbmc/regression/jbmc/exception-cleanup/test.desc

+The unreachable function should be successfully marked unreachable by symex,
+but the final uncaught exception is not yet, as it requires symex to note that
+within a catch block @inflight_exception is definitely *not* null, which it
+can't just yet.


Not sure I understand what that comment is here for. The test is already marked as CORE, so what difference should we see when the stated limitation is resolved?

Then we'll resolve all conditions in symex. I'll amend to make that clearer.

owen-mc-diffblue

The commit message for "Symex: propagate constants implied by assumptions and conditions" says the constant propagator might be populated with new information. Is it also possible that the value-set gets updated? If so, please correct the commit message.

owen-mc-diffblue · 2019-03-18T14:53:08Z

jbmc/regression/jbmc/exception-cleanup/test.desc

+^warning: ignoring
+--
+The unreachable function should be successfully marked unreachable by symex,
+but the final uncaught exception is not yet, as it requires symex to note that


I don't understand what "the final uncaught exception" means. All the exceptions appear to be caught to me.

It refers to the "did any exception escape at top level?" test that's always generated in __CPROVER_start, and yes they are all caught, but symex isn't quite smart enough to determine that yet. This PR enables it to determine there's no exception in flight when we return to normal code (preventing exploration of catch blocks after future no-throw function calls), but doesn't yet enable it to determine catch block does not rethrow.

(I'll improve the wording here)

When passing `assume(symbol == constant)` or `if symbol == constant then GOTO`, we can populate the constant propagator and value-set accordingly and use that information until the next merge point without that constraint. We implement this by allocating and defining a fresh L2 generation on this path, which will be merged as "real", assignment-derived generations are. Symbols are subject to propagation under the same conditions as they are on assignment (e.g. requiring that they are not subject to concurrent modification by other threads).

smowton · 2019-03-18T17:22:16Z

@allredj I ran this on some Tika functions and observed that a small batch of 6 functions that took a total of 248s (symex-only) took 231s with this patch. Of course that's a small test, but it gives me some confidence this will be overall beneficial. I'll run a longer benchmark tomorrow to be sure and then merge if the results are also positive.

allredj

Great!

smowton · 2019-03-19T14:55:22Z

Extended benchmark results show a slight improvement, so merging this as-is and we can implement @tautschnig's suggestion re: using different data structures to record a path-local constant if and when we want to.

smowton requested review from allredj, chrisr-diffblue, danpoe, hannes-steffenhagen-diffblue, kroening, martin-cs, owen-mc-diffblue, peterschrammel, romainbrenguier and tautschnig as code owners March 14, 2019 15:13

tautschnig reviewed Mar 14, 2019

View reviewed changes

smowton force-pushed the smowton/feature/symex-condition-driving branch from 864a3e0 to 2fca1b8 Compare March 14, 2019 15:34

smowton mentioned this pull request Mar 14, 2019

Fix symex of functions that may throw #4343

Merged

allredj reviewed Mar 14, 2019

View reviewed changes

tautschnig changed the title ~~Symex: propagate assumptions and conditions~~ Symex: propagate assumptions and conditions [depends-on: #4199, #4379] Mar 14, 2019

tautschnig added the dependent - do not merge label Mar 14, 2019

owen-mc-diffblue reviewed Mar 15, 2019

View reviewed changes

smowton force-pushed the smowton/feature/symex-condition-driving branch from 2fca1b8 to 31451a4 Compare March 15, 2019 10:39

owen-mc-diffblue reviewed Mar 15, 2019

View reviewed changes

smowton changed the title ~~Symex: propagate assumptions and conditions [depends-on: #4199, #4379]~~ Symex: propagate assumptions and conditions [depends-on: #4199] Mar 15, 2019

smowton added 3 commits March 15, 2019 16:44

Move goto_symex_is_constantt into its own file

929c21d

No behavioural change.

Move increase_generation onto goto_statet

6441467

This enables us to more conveniently allocate a new generation on a non-current state, such as a state copy that will be used on a pending branch. No behavioural change.

smowton force-pushed the smowton/feature/symex-condition-driving branch 2 times, most recently from 241bae7 to 83ddfc2 Compare March 15, 2019 16:58

smowton removed the dependent - do not merge label Mar 15, 2019

smowton assigned tautschnig Mar 15, 2019

smowton assigned kroening and peterschrammel Mar 15, 2019

smowton changed the title ~~Symex: propagate assumptions and conditions [depends-on: #4199]~~ Symex: propagate assumptions and conditions Mar 15, 2019

peterschrammel approved these changes Mar 15, 2019

View reviewed changes

peterschrammel removed their assignment Mar 15, 2019

allredj reviewed Mar 18, 2019

View reviewed changes

owen-mc-diffblue approved these changes Mar 18, 2019

View reviewed changes

smowton added 2 commits March 18, 2019 16:15

Add tests for symex condition propagation

e0d4d78

smowton force-pushed the smowton/feature/symex-condition-driving branch from 83ddfc2 to e0d4d78 Compare March 18, 2019 16:16

allredj approved these changes Mar 18, 2019

View reviewed changes

peterschrammel assigned smowton and unassigned tautschnig and kroening Mar 18, 2019

smowton merged commit 17fa596 into diffblue:develop Mar 19, 2019

owen-mc-diffblue mentioned this pull request Mar 21, 2019

Filter value sets in symex #4288

Merged

7 tasks

Symex: propagate assumptions and conditions #4386

Symex: propagate assumptions and conditions #4386

Uh oh!

Conversation

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

Uh oh!

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!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Mar 14, 2019

Uh oh!

allredj 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!

smowton commented Mar 15, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smowton commented Mar 15, 2019

Uh oh!

peterschrammel left a comment

Choose a reason for hiding this comment

Uh oh!

allredj 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!

Choose a reason for hiding this comment

Uh oh!

owen-mc-diffblue 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!

smowton commented Mar 18, 2019

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

smowton commented Mar 19, 2019

Uh oh!

Uh oh!

smowton commented Mar 14, 2019 •

edited

Loading

smowton Mar 14, 2019 •

edited

Loading