Use BDDs for encoding symex guards #3730
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,8 +1,13 @@ | ||
| CORE bdd-expected-timeout | ||
|
There was a problem hiding this comment. Could you please include a comment at the bottom of this file what the behaviour with BDDs is? Is it taking minutes, hours, days? And maybe also an idea why that's happening on this particular test? |
||
| Test.class | ||
| --function Test.main | ||
| ^EXIT=0$ | ||
| ^SIGNAL=0$ | ||
| ^VERIFICATION SUCCESSFUL$ | ||
| -- | ||
| ^warning: ignoring | ||
| -- | ||
| 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 represented as exprt. | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -20,7 +20,6 @@ Author: Daniel Kroening, [email protected] | |
| #include <util/cprover_prefix.h> | ||
| #include <util/expr_util.h> | ||
| #include <util/find_symbols.h> | ||
| #include <util/ieee_float.h> | ||
| #include <util/invariant.h> | ||
| #include <util/make_unique.h> | ||
|
|
@@ -36,6 +35,7 @@ Author: Daniel Kroening, [email protected] | |
|
|
||
| #include <goto-programs/remove_skip.h> | ||
|
|
||
| #include "guard.h" | ||
| #include "local_bitvector_analysis.h" | ||
|
|
||
| class goto_checkt | ||
|
|
@@ -84,6 +84,7 @@ class goto_checkt | |
| const namespacet &ns; | ||
| std::unique_ptr<local_bitvector_analysist> local_bitvector_analysis; | ||
| goto_programt::const_targett current_target; | ||
| guard_managert guard_manager; | ||
|
|
||
| void check_rec( | ||
| const exprt &expr, | ||
|
|
@@ -1650,7 +1651,7 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address) | |
|
|
||
| void goto_checkt::check(const exprt &expr) | ||
| { | ||
| guardt guard{true_exprt{}, guard_manager}; | ||
| check_rec(expr, guard, false); | ||
| } | ||
|
|
||
|
|
@@ -1782,7 +1783,7 @@ void goto_checkt::goto_check( | |
| "pointer dereference", | ||
| i.source_location, | ||
| pointer, | ||
| guardt(true_exprt(), guard_manager)); | ||
| } | ||
| } | ||
|
|
||
|
|
@@ -1820,7 +1821,7 @@ void goto_checkt::goto_check( | |
| "pointer dereference", | ||
| i.source_location, | ||
| pointer, | ||
| guardt(true_exprt(), guard_manager)); | ||
| } | ||
|
|
||
| // this has no successor | ||
|
|
@@ -1897,7 +1898,7 @@ void goto_checkt::goto_check( | |
| "memory-leak", | ||
| source_location, | ||
| eq, | ||
| guardt(true_exprt(), guard_manager)); | ||
| } | ||
| } | ||
|
|
||
|
|
||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,31 @@ | ||
| /*******************************************************************\ | ||
|
|
||
| Module: Guard Data Structure | ||
|
|
||
| Author: Daniel Kroening, [email protected] | ||
|
|
||
| \*******************************************************************/ | ||
|
|
||
| /// \file | ||
| /// Guard Data Structure | ||
|
|
||
| #ifndef CPROVER_ANALYSES_GUARD_H | ||
| #define CPROVER_ANALYSES_GUARD_H | ||
|
|
||
| #ifdef BDD_GUARDS | ||
|
|
||
| #include "guard_bdd.h" | ||
|
|
||
| using guard_managert = bdd_exprt; | ||
| using guardt = guard_bddt; | ||
|
There was a problem hiding this comment. Would it be possible for them to please have a shared interface? Otherwise inconsistencies will creep in that can only be detected by compiling both with and without There was a problem hiding this comment. I'm reluctant to use virtual functions since they are not really needed here. I could try doing that using CRTP if you think that's a good idea ( There was a problem hiding this comment. I suppose we had the same discussion on the CUDD/miniBDD BDD PR :-) It's not the most important of all issues and can be left to a future PR - but I will remind you about it whenever there is a change to these interfaces and someone forgets to update both of them :-P There was a problem hiding this comment. fair enough |
||
|
|
||
| #else | ||
|
|
||
| #include "guard_expr.h" | ||
|
|
||
| using guard_managert = guard_expr_managert; | ||
| using guardt = guard_exprt; | ||
|
|
||
| #endif // BDD_GUARDS | ||
|
|
||
| #endif // CPROVER_ANALYSES_GUARD_H | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,94 @@ | ||
| /*******************************************************************\ | ||
|
|
||
| Module: Guard Data Structure | ||
|
|
||
| Author: Romain Brenguier, [email protected] | ||
|
|
||
| \*******************************************************************/ | ||
|
|
||
| /// \file | ||
| /// Implementation of guards using BDDs | ||
|
|
||
| #include "guard_bdd.h" | ||
|
|
||
| #include <algorithm> | ||
| #include <ostream> | ||
| #include <set> | ||
|
|
||
| #include <solvers/bdd/bdd.h> | ||
| #include <solvers/prop/bdd_expr.h> | ||
| #include <util/expr_util.h> | ||
| #include <util/invariant.h> | ||
| #include <util/make_unique.h> | ||
| #include <util/namespace.h> | ||
| #include <util/simplify_utils.h> | ||
| #include <util/std_expr.h> | ||
| #include <util/symbol_table.h> | ||
|
|
||
| guard_bddt::guard_bddt(const exprt &e, bdd_exprt &manager) | ||
| : manager(manager), bdd(manager.from_expr(e)) | ||
| { | ||
| } | ||
|
|
||
| guard_bddt &guard_bddt::operator=(const guard_bddt &other) | ||
| { | ||
| PRECONDITION(&manager == &other.manager); | ||
| bdd = other.bdd; | ||
| return *this; | ||
| } | ||
|
|
||
| guard_bddt &guard_bddt::operator=(guard_bddt &&other) | ||
| { | ||
| PRECONDITION(&manager == &other.manager); | ||
| std::swap(bdd, other.bdd); | ||
| return *this; | ||
| } | ||
|
|
||
| exprt guard_bddt::guard_expr(exprt expr) const | ||
| { | ||
| if(is_true()) | ||
| { | ||
| // do nothing | ||
| return expr; | ||
| } | ||
| else | ||
| { | ||
| if(expr.is_false()) | ||
| { | ||
| return boolean_negate(as_expr()); | ||
| } | ||
| else | ||
| { | ||
| return implies_exprt{as_expr(), expr}; | ||
|
There was a problem hiding this comment.
And I would get rid of a lot of braces now that the branches are one-liners. |
||
| } | ||
| } | ||
| } | ||
|
|
||
| guard_bddt &guard_bddt::append(const guard_bddt &guard) | ||
| { | ||
| bdd = bdd.bdd_and(guard.bdd); | ||
| return *this; | ||
| } | ||
|
|
||
| guard_bddt &guard_bddt::add(const exprt &expr) | ||
| { | ||
| bdd = bdd.bdd_and(manager.from_expr(expr)); | ||
| return *this; | ||
| } | ||
|
|
||
| guard_bddt &operator-=(guard_bddt &g1, const guard_bddt &g2) | ||
| { | ||
| g1.bdd = g1.bdd.constrain(g2.bdd.bdd_or(g1.bdd)); | ||
| return g1; | ||
| } | ||
|
|
||
| guard_bddt &operator|=(guard_bddt &g1, const guard_bddt &g2) | ||
| { | ||
| g1.bdd = g1.bdd.bdd_or(g2.bdd); | ||
| return g1; | ||
| } | ||
|
|
||
| exprt guard_bddt::as_expr() const | ||
| { | ||
| return manager.as_expr(bdd); | ||
| } | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We will need some equivalent thereof in the Makefile. Something like
ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),)