Use BDDs for encoding symex guards #3730

romainbrenguier · 2019-01-09T10:19:29Z

The main commit is "Use BDDs for encoding guards in symex". Commits that are before are in preparation for this one (in particular getting rid of usage of functions the new version will not implement). Commits that follow are clean-up in the code that use the guard (in particular getting rid of simplifications that are now unnecessary).

I still wan't to run this on more benchmarks before it is merged. For what I've seen so far, this is about 10% faster than the current symex, but this is not uniform across benchmarks (it doesn't help for "simple" instances, i.e. which take less than 2s).

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
[na] The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
[na] White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig · 2019-01-09T10:29:14Z

Before reviewing this in any way: I believe I had mentioned #310. Does this PR relate to it in any way?

romainbrenguier · 2019-01-09T10:39:35Z

@tautschnig

Before reviewing this in any way: I believe I had mentioned #310. Does this PR relate to it in any way?

Yes, the idea is similar, but this is taking it one step further: instead of keeping guards as exprt and using BDDs to simplify them at some points in the code, we always keep the guards as BDDs and only convert to exprt when as_expr is called.

tautschnig

Given this is marked "In progress" I'm sure this is the plan, but just to be explicit: please turn this into a series of PRs, there are a lot of seemingly unrelated changes.

tautschnig · 2019-01-09T10:43:06Z

src/analyses/goto_check.cpp

@@ -1342,8 +1342,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
        guard.add(op);
    }

-    guard.swap(old_guard);
-
+    guard = std::move(old_guard);


Almost randomly poking at commits: what's the improvement here? (I actually have a yet-to-be-PR'ed commit lying around making the opposite change, i.e., replacing uses of std::move by swap.)

The new implementation of guardt doesn't have a swap (though exprt has). And since old_guard is not used afterward, I don't see a reason for using swap?

For irept-based implementations = std::move(...) is at best as efficient as swap, and possibly less efficient if USE_MOVE is not enabled. (But I do concede that we should just get rid of USE_MOVE as an optional feature as we require C++11 anyway.) So in that setting the change doesn't seem to provide any added value.

With the new implementation of guardt not being an irept, the situation of course is different. But that needs to be spelled out in the commit message...

tautschnig · 2019-01-09T10:47:45Z

Yes, the idea is similar, but this is taking it one step further: instead of keeping guards as exprt and using BDDs to simplify them at some points in the code, we always keep the guards as BDDs and only convert to exprt when as_expr is called.

Ok, but do note that in terms of history this is a step backwards: guardt used to be unrelated to exprt, and making it an exprt enabled access to more sharing when previously we had a lot of redundant copies.

tautschnig · 2019-01-09T10:52:48Z

src/analyses/goto_rw.cpp


-    guard.add(not_exprt(if_expr.cond()));
+    copy.add(not_exprt(if_expr.cond()));


This should be guard.add

tautschnig · 2019-01-09T10:54:28Z

There is a lot of great cleanup in this PR that should be merged as soon as possible, but via individual PRs (really one per commit). Then this PR can be reduced to the necessary minimum and also the effect of BDDs (and not that of the cleanup) can be measured.

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 468c01d).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103158445
Status will be re-evaluated on next push.
Common spurious failures:

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).
the compatibility was already broken by an earlier merge.

tautschnig · 2019-03-05T08:47:53Z

jbmc/regression/jbmc/class-literals/test.desc

+This test is deactivated for the build with BDDs because it takes more
+than 10 minutes for the test to complete.
+This is due to the size of the BDD representing the guards growing more than
+they do when reprented as exprt.


Nit pick: s/reprented/represented/

tautschnig · 2019-03-05T08:48:10Z

jbmc/regression/jbmc/class-literals/test.desc

+than 10 minutes for the test to complete.
+This is due to the size of the BDD representing the guards growing more than
+they do when reprented as exprt.
+


Nit pick 2: No need for blank line

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: ddf0491).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103176652
Status will be re-evaluated on next push.
Common spurious failures:

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).
the compatibility was already broken by an earlier merge.

No functional changes. This was done automatically using clang-format. This is in preparation to moving this two files, so that clang-format doesn't reformat the file at the same time they are moved, and so that the move commit is clean.

We want to add an implementation of guard that uses BDDs, which are part of the solvers module. We cannot add a dependency of the util module on solvers.

The guard used there was actually only used as a conjunction, so it can be replaced by a list of expressions, of which we take the conjunction when needed.

This in preparation to using BDDs to encode guards, every part of the code creating guards need to reference a guard_manager.

A reference to a namespace was stored without being ever used.

Instead the result of from_exprt and the input of as_expr should be BDDs. This makes it possible to reuse the same manager for several exprt conversion and to combine the results obtain from the from_expr conversion with BDD operations.

The type of identifier can vary depending on the BDD implementation used. Using long there was kind of a hack and not correct on architecture where pointers wouldn't fit in a long.

Caching the intermediary results can lead to big performance improvements since the number of calls without cache could be potentially exponential in the size of the BDD.

This is not used yet in CBMC. The aim is to specify at compile time whether we want to use this new implementation or the old one. Using BDDs ensures the guards are always in some "simple" form.

This is to clearly seperate the two implementations. The choice between the two will be made in guard.h

To avoid confusion with the other guard implementation. This forces us to use includes instead of forward declaration for guardt because forward declaration doesn't work well with typedef.

Depending on the BDD_GUARDS flag, we will use the expr implementation or the BDD implementation.

This adds instruction to COMPILING.md so that people interested in performances can find about it, and try it.

Expressions obtained from BDDs are already simple. Trying to simplify them is redundant and can slow down the execution. We add this field so that symex code can take the decision to simplify or not an expression based on this information.

We add the BDD_GUARDS flags in the travis step which is compiling with CUDD to test that the bdd_guard implementation.

One of the JBMC tests will take a long time when BDD are used. We deactivate it for now in the case BDD_GUARDS is defined. This is acceptable since using BDDs for guards is still experimental. Ideally we should find what takes too long in the execution and optimize it, but it may be that we hit a particular class of guards for which the BDDs have to be big.

This avoids having an argument that is both input and output and makes using this function nicer.

No functional change

allredj

⚠️
This PR failed Diffblue compatibility checks (cbmc commit: 22ed54b).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/103523152
Status will be re-evaluated on next push.
Common spurious failures:

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).
the compatibility was already broken by an earlier merge.

romainbrenguier added do not merge In progress labels Jan 9, 2019

romainbrenguier requested review from cesaro, chrisr-diffblue, cristina-david, kroening, martin-cs, peterschrammel, pkesseli, smowton, tautschnig and thk123 as code owners January 9, 2019 10:19

tautschnig requested changes Jan 9, 2019

View reviewed changes

tautschnig reviewed Jan 9, 2019

View reviewed changes

romainbrenguier force-pushed the experiment/bdd-guards4 branch 3 times, most recently from 0b6eca3 to a8ba19d Compare January 10, 2019 10:55

romainbrenguier requested a review from forejtv as a code owner January 10, 2019 10:55

romainbrenguier force-pushed the experiment/bdd-guards4 branch 8 times, most recently from 9ca95cd to 88ff3a4 Compare January 11, 2019 14:04

romainbrenguier force-pushed the experiment/bdd-guards4 branch 3 times, most recently from 398bd01 to 468c01d Compare March 5, 2019 06:34

allredj reviewed Mar 5, 2019

View reviewed changes

tautschnig reviewed Mar 5, 2019

View reviewed changes

romainbrenguier force-pushed the experiment/bdd-guards4 branch from 468c01d to ddf0491 Compare March 5, 2019 09:28

allredj reviewed Mar 5, 2019

View reviewed changes

romainbrenguier added 18 commits March 7, 2019 11:02

Reformat guard.cpp and guard.h

a5c9790

No functional changes. This was done automatically using clang-format. This is in preparation to moving this two files, so that clang-format doesn't reformat the file at the same time they are moved, and so that the move commit is clean.

Move guardt to analyses module

decfe4a

We want to add an implementation of guard that uses BDDs, which are part of the solvers module. We cannot add a dependency of the util module on solvers.

Replace use of guardt by operandst in symex_assign

115011a

The guard used there was actually only used as a conjunction, so it can be replaced by a list of expressions, of which we take the conjunction when needed.

Add guard_manager class and pass it around

9727c5e

This in preparation to using BDDs to encode guards, every part of the code creating guards need to reference a guard_manager.

Remove unused field ns field of bdd_exprt

4da4bd3

A reference to a namespace was stored without being ever used.

Remove root field of bdd_exprt

f9a698c

Instead the result of from_exprt and the input of as_expr should be BDDs. This makes it possible to reuse the same manager for several exprt conversion and to combine the results obtain from the from_expr conversion with BDD operations.

Define idt type for bdd_node::id() functions

f640d73

The type of identifier can vary depending on the BDD implementation used. Using long there was kind of a hack and not correct on architecture where pointers wouldn't fit in a long.

Add a cache to as_expr function for BDDs

c63b9df

Caching the intermediary results can lead to big performance improvements since the number of calls without cache could be potentially exponential in the size of the BDD.

New implementation of guards using BDDs

f164c83

This is not used yet in CBMC. The aim is to specify at compile time whether we want to use this new implementation or the old one. Using BDDs ensures the guards are always in some "simple" form.

Move guard implementation to guard_expr.h/cpp

de291f6

This is to clearly seperate the two implementations. The choice between the two will be made in guard.h

Rename class to guard_exprt

c8d8c48

To avoid confusion with the other guard implementation. This forces us to use includes instead of forward declaration for guardt because forward declaration doesn't work well with typedef.

Switch between guard bdd and guard expr

eba0713

Depending on the BDD_GUARDS flag, we will use the expr implementation or the BDD implementation.

Document the BDD_GUARDS compilation flag

fccd412

This adds instruction to COMPILING.md so that people interested in performances can find about it, and try it.

Enable BDD_GUARDS in one of the travis steps

f4afbd1

We add the BDD_GUARDS flags in the travis step which is compiling with CUDD to test that the bdd_guard implementation.

Make guard_expr return a value

7503ac6

This avoids having an argument that is both input and output and makes using this function nicer.

Apply clang-format suggestions

22ed54b

No functional change

romainbrenguier force-pushed the experiment/bdd-guards4 branch from ddf0491 to 22ed54b Compare March 7, 2019 11:03

allredj reviewed Mar 7, 2019

View reviewed changes

romainbrenguier merged commit 0b58dc5 into diffblue:develop Mar 7, 2019

romainbrenguier deleted the experiment/bdd-guards4 branch March 7, 2019 13:02

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Use BDDs for encoding symex guards #3730

Use BDDs for encoding symex guards #3730

romainbrenguier commented Jan 9, 2019 •

edited

Loading

tautschnig commented Jan 9, 2019

romainbrenguier commented Jan 9, 2019

tautschnig left a comment

tautschnig Jan 9, 2019

romainbrenguier Jan 9, 2019

tautschnig Jan 9, 2019

tautschnig commented Jan 9, 2019

tautschnig Jan 9, 2019

tautschnig commented Jan 9, 2019

allredj left a comment

tautschnig Mar 5, 2019

tautschnig Mar 5, 2019

allredj left a comment

allredj left a comment


		guard.add(not_exprt(if_expr.cond()));
		copy.add(not_exprt(if_expr.cond()));

Use BDDs for encoding symex guards #3730

Use BDDs for encoding symex guards #3730

Conversation

romainbrenguier commented Jan 9, 2019 • edited Loading

tautschnig commented Jan 9, 2019

romainbrenguier commented Jan 9, 2019

tautschnig left a comment

Choose a reason for hiding this comment

tautschnig Jan 9, 2019

Choose a reason for hiding this comment

romainbrenguier Jan 9, 2019

Choose a reason for hiding this comment

tautschnig Jan 9, 2019

Choose a reason for hiding this comment

tautschnig commented Jan 9, 2019

tautschnig Jan 9, 2019

Choose a reason for hiding this comment

tautschnig commented Jan 9, 2019

allredj left a comment

Choose a reason for hiding this comment

tautschnig Mar 5, 2019

Choose a reason for hiding this comment

tautschnig Mar 5, 2019

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

allredj left a comment

Choose a reason for hiding this comment

romainbrenguier commented Jan 9, 2019 •

edited

Loading