From a5c9790b331abeae554720dce3e21b6ded427f88 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 6 Feb 2019 08:14:03 +0000 Subject: [PATCH 01/18] Reformat guard.cpp and guard.h 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. --- src/util/guard.cpp | 48 ++++++++++++++++++++-------------------------- src/util/guard.h | 4 ++-- 2 files changed, 23 insertions(+), 29 deletions(-) diff --git a/src/util/guard.cpp b/src/util/guard.cpp index c74245a1301..6477498176f 100644 --- a/src/util/guard.cpp +++ b/src/util/guard.cpp @@ -58,15 +58,13 @@ void guardt::add(const exprt &expr) exprt::operandst &op = this->expr.operands(); - if(expr.id()==ID_and) - op.insert(op.end(), - expr.operands().begin(), - expr.operands().end()); + if(expr.id() == ID_and) + op.insert(op.end(), expr.operands().begin(), expr.operands().end()); else op.push_back(expr); } -guardt &operator -= (guardt &g1, const guardt &g2) +guardt &operator-=(guardt &g1, const guardt &g2) { if(g1.expr.id() != ID_and || g2.expr.id() != ID_and) return g1; @@ -76,18 +74,16 @@ guardt &operator -= (guardt &g1, const guardt &g2) sort_and_join(g2_sorted); exprt::operandst &op1 = g1.expr.operands(); - const exprt::operandst &op2=g2_sorted.operands(); + const exprt::operandst &op2 = g2_sorted.operands(); - exprt::operandst::iterator it1=op1.begin(); - for(exprt::operandst::const_iterator - it2=op2.begin(); - it2!=op2.end(); + exprt::operandst::iterator it1 = op1.begin(); + for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end(); ++it2) { - while(it1!=op1.end() && *it1<*it2) + while(it1 != op1.end() && *it1 < *it2) ++it1; - if(it1!=op1.end() && *it1==*it2) - it1=op1.erase(it1); + if(it1 != op1.end() && *it1 == *it2) + it1 = op1.erase(it1); } g1.expr = conjunction(op1); @@ -95,7 +91,7 @@ guardt &operator -= (guardt &g1, const guardt &g2) return g1; } -guardt &operator |= (guardt &g1, const guardt &g2) +guardt &operator|=(guardt &g1, const guardt &g2) { if(g2.is_false() || g1.is_true()) return g1; @@ -125,46 +121,44 @@ guardt &operator |= (guardt &g1, const guardt &g2) sort_and_join(g2_sorted); exprt::operandst &op1 = g1.expr.operands(); - const exprt::operandst &op2=g2_sorted.operands(); + const exprt::operandst &op2 = g2_sorted.operands(); exprt::operandst n_op1, n_op2; n_op1.reserve(op1.size()); n_op2.reserve(op2.size()); - exprt::operandst::iterator it1=op1.begin(); - for(exprt::operandst::const_iterator - it2=op2.begin(); - it2!=op2.end(); + exprt::operandst::iterator it1 = op1.begin(); + for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end(); ++it2) { - while(it1!=op1.end() && *it1<*it2) + while(it1 != op1.end() && *it1 < *it2) { n_op1.push_back(*it1); - it1=op1.erase(it1); + it1 = op1.erase(it1); } - if(it1!=op1.end() && *it1==*it2) + if(it1 != op1.end() && *it1 == *it2) ++it1; else n_op2.push_back(*it2); } - while(it1!=op1.end()) + while(it1 != op1.end()) { n_op1.push_back(*it1); - it1=op1.erase(it1); + it1 = op1.erase(it1); } if(n_op2.empty()) return g1; // end of common prefix - exprt and_expr1=conjunction(n_op1); - exprt and_expr2=conjunction(n_op2); + exprt and_expr1 = conjunction(n_op1); + exprt and_expr2 = conjunction(n_op2); g1.expr = conjunction(op1); exprt tmp(boolean_negate(and_expr2)); - if(tmp!=and_expr1) + if(tmp != and_expr1) { if(and_expr1.is_true() || and_expr2.is_true()) { diff --git a/src/util/guard.h b/src/util/guard.h index 7019f9bcce5..2ae5c26ea8a 100644 --- a/src/util/guard.h +++ b/src/util/guard.h @@ -47,8 +47,8 @@ class guardt return expr.is_false(); } - friend guardt &operator -= (guardt &g1, const guardt &g2); - friend guardt &operator |= (guardt &g1, const guardt &g2); + friend guardt &operator-=(guardt &g1, const guardt &g2); + friend guardt &operator|=(guardt &g1, const guardt &g2); private: exprt expr; From decfe4a61b8365fa18dc44d66542e961b7e8df0f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 4 Feb 2019 08:24:20 +0000 Subject: [PATCH 02/18] Move guardt to analyses module 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. --- src/analyses/Makefile | 1 + src/analyses/goto_check.cpp | 2 +- src/analyses/goto_rw.h | 2 +- src/{util => analyses}/guard.cpp | 8 ++++---- src/{util => analyses}/guard.h | 8 ++++---- src/goto-symex/goto_symex_state.h | 2 +- src/pointer-analysis/goto_program_dereference.cpp | 1 - src/pointer-analysis/value_set_dereference.cpp | 1 - src/util/Makefile | 1 - 9 files changed, 12 insertions(+), 14 deletions(-) rename src/{util => analyses}/guard.cpp (96%) rename src/{util => analyses}/guard.h (86%) diff --git a/src/analyses/Makefile b/src/analyses/Makefile index dbab82bda96..799bab28663 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -12,6 +12,7 @@ SRC = ai.cpp \ global_may_alias.cpp \ goto_check.cpp \ goto_rw.cpp \ + guard.cpp \ interval_analysis.cpp \ interval_domain.cpp \ invariant_propagation.cpp \ diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index cc4c0b76df8..b03faaefaba 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -20,7 +20,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include @@ -36,6 +35,7 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "guard.h" #include "local_bitvector_analysis.h" class goto_checkt diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h index 49ce2de73c7..d295efb9e73 100644 --- a/src/analyses/goto_rw.h +++ b/src/analyses/goto_rw.h @@ -17,7 +17,7 @@ Date: April 2010 #include #include // unique_ptr -#include +#include "guard.h" #include diff --git a/src/util/guard.cpp b/src/analyses/guard.cpp similarity index 96% rename from src/util/guard.cpp rename to src/analyses/guard.cpp index 6477498176f..3dbf7cc1f72 100644 --- a/src/util/guard.cpp +++ b/src/analyses/guard.cpp @@ -13,10 +13,10 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include "expr_util.h" -#include "invariant.h" -#include "simplify_utils.h" -#include "std_expr.h" +#include +#include +#include +#include void guardt::guard_expr(exprt &dest) const { diff --git a/src/util/guard.h b/src/analyses/guard.h similarity index 86% rename from src/util/guard.h rename to src/analyses/guard.h index 2ae5c26ea8a..36950c43355 100644 --- a/src/util/guard.h +++ b/src/analyses/guard.h @@ -9,12 +9,12 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Guard Data Structure -#ifndef CPROVER_UTIL_GUARD_H -#define CPROVER_UTIL_GUARD_H +#ifndef CPROVER_ANALYSES_GUARD_H +#define CPROVER_ANALYSES_GUARD_H #include -#include "std_expr.h" +#include class guardt { @@ -54,4 +54,4 @@ class guardt exprt expr; }; -#endif // CPROVER_UTIL_GUARD_H +#endif // CPROVER_ANALYSES_GUARD_H diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 88a0c8549a3..f0e085509ea 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -16,9 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include -#include #include #include #include diff --git a/src/pointer-analysis/goto_program_dereference.cpp b/src/pointer-analysis/goto_program_dereference.cpp index 17fe6b0a547..7b75c1bbfe6 100644 --- a/src/pointer-analysis/goto_program_dereference.cpp +++ b/src/pointer-analysis/goto_program_dereference.cpp @@ -15,7 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include /// \param expr: expression to check diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp index cd05d712db0..223b930cded 100644 --- a/src/pointer-analysis/value_set_dereference.cpp +++ b/src/pointer-analysis/value_set_dereference.cpp @@ -24,7 +24,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include #include diff --git a/src/util/Makefile b/src/util/Makefile index 8a5f9123c20..8c4c6b5beb4 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -26,7 +26,6 @@ SRC = allocate_objects.cpp \ fresh_symbol.cpp \ get_base_name.cpp \ get_module.cpp \ - guard.cpp \ identifier.cpp \ ieee_float.cpp \ invariant.cpp \ From 115011a5d0c61307f502cffa06d3e33fcc6109d3 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 21 Feb 2019 08:23:16 +0000 Subject: [PATCH 03/18] Replace use of guardt by operandst in symex_assign 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. --- src/goto-symex/goto_symex.h | 14 ++++---- src/goto-symex/symex_assign.cpp | 50 ++++++++++++++------------ src/goto-symex/symex_function_call.cpp | 5 +-- src/goto-symex/symex_start_thread.cpp | 8 ++--- 4 files changed, 42 insertions(+), 35 deletions(-) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index a4c68471a7f..616291efeab 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -445,49 +445,49 @@ class goto_symext const exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &, + exprt::operandst &, assignment_typet); void symex_assign_symbol( statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &, + exprt::operandst &, assignment_typet); void symex_assign_typecast( statet &, const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &, + exprt::operandst &, assignment_typet); void symex_assign_array( statet &, const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &, + exprt::operandst &, assignment_typet); void symex_assign_struct_member( statet &, const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &, + exprt::operandst &, assignment_typet); void symex_assign_if( statet &, const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &, + exprt::operandst &, assignment_typet); void symex_assign_byte_extract( statet &, const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &, + exprt::operandst &, assignment_typet); /// Store the \p what expression by recursively descending into the operands diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 43dc2d5942d..bca4cf26c02 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -71,8 +71,14 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code) if(state.source.pc->source_location.get_hide()) assignment_type=symex_targett::assignment_typet::HIDDEN; - guardt guard{true_exprt{}}; // NOT the state guard! - symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type); + exprt::operandst lhs_if_then_else_conditions; + symex_assign_rec( + state, + lhs, + nil_exprt(), + rhs, + lhs_if_then_else_conditions, + assignment_type); } } @@ -115,7 +121,7 @@ void goto_symext::symex_assign_rec( const exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, + exprt::operandst &guard, assignment_typet assignment_type) { if(lhs.id()==ID_symbol && @@ -197,15 +203,15 @@ void goto_symext::symex_assign_symbol( const ssa_exprt &lhs, // L1 const exprt &full_lhs, const exprt &rhs, - guardt &guard, + exprt::operandst &guard, assignment_typet assignment_type) { exprt ssa_rhs=rhs; // put assignment guard into the rhs - if(!guard.is_true()) + if(!guard.empty()) { - if_exprt tmp_ssa_rhs(guard.as_expr(), ssa_rhs, lhs, ssa_rhs.type()); + if_exprt tmp_ssa_rhs(conjunction(guard), ssa_rhs, lhs, ssa_rhs.type()); tmp_ssa_rhs.swap(ssa_rhs); } @@ -228,9 +234,6 @@ void goto_symext::symex_assign_symbol( exprt l2_full_lhs = state.rename(std::move(ssa_full_lhs), ns); state.record_events=record_events; - guardt tmp_guard(state.guard); - tmp_guard.append(guard); - // do the assignment const symbolt &symbol = ns.lookup(to_symbol_expr(ssa_lhs.get_original_expr())); @@ -248,14 +251,20 @@ void goto_symext::symex_assign_symbol( << messaget::eom; }); + // Temporarily add the state guard + guard.emplace_back(state.guard.as_expr()); + target.assignment( - tmp_guard.as_expr(), + conjunction(guard), ssa_lhs, l2_full_lhs, add_to_lhs(full_lhs, ssa_lhs.get_original_expr()), l2_rhs, state.source, assignment_type); + + // Restore the guard + guard.pop_back(); } void goto_symext::symex_assign_typecast( @@ -263,7 +272,7 @@ void goto_symext::symex_assign_typecast( const typecast_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, + exprt::operandst &guard, assignment_typet assignment_type) { // these may come from dereferencing on the lhs @@ -280,7 +289,7 @@ void goto_symext::symex_assign_array( const index_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, + exprt::operandst &guard, assignment_typet assignment_type) { const exprt &lhs_array=lhs.array(); @@ -327,7 +336,7 @@ void goto_symext::symex_assign_struct_member( const member_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, + exprt::operandst &guard, assignment_typet assignment_type) { // Symbolic execution of a struct member assignment. @@ -397,30 +406,27 @@ void goto_symext::symex_assign_if( const if_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, + exprt::operandst &guard, assignment_typet assignment_type) { // we have (c?a:b)=e; - - guardt old_guard=guard; - exprt renamed_guard = state.rename(lhs.cond(), ns); do_simplify(renamed_guard); if(!renamed_guard.is_false()) { - guard.add(renamed_guard); + guard.push_back(renamed_guard); symex_assign_rec( state, lhs.true_case(), full_lhs, rhs, guard, assignment_type); - guard = std::move(old_guard); + guard.pop_back(); } if(!renamed_guard.is_true()) { - guard.add(not_exprt(renamed_guard)); + guard.push_back(not_exprt(renamed_guard)); symex_assign_rec( state, lhs.false_case(), full_lhs, rhs, guard, assignment_type); - guard = std::move(old_guard); + guard.pop_back(); } } @@ -429,7 +435,7 @@ void goto_symext::symex_assign_byte_extract( const byte_extract_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - guardt &guard, + exprt::operandst &guard, assignment_typet assignment_type) { // we have byte_extract_X(object, offset)=value diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 0a43a857ab5..f04e1c21a08 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -134,8 +134,9 @@ void goto_symext::parameter_assignments( clean_expr(lhs, state, true); clean_expr(rhs, state, false); - guardt guard{true_exprt{}}; - symex_assign_rec(state, lhs, nil_exprt(), rhs, guard, assignment_type); + exprt::operandst lhs_conditions; + symex_assign_rec( + state, lhs, nil_exprt(), rhs, lhs_conditions, assignment_type); } if(it1!=arguments.end()) diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index ddae9b68886..9c08ec6ad35 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -84,7 +84,7 @@ void goto_symext::symex_start_thread(statet &state) // make copy ssa_exprt rhs=c_it->second.first; - guardt guard{true_exprt{}}; + exprt::operandst lhs_conditions; const bool record_events=state.record_events; state.record_events=false; symex_assign_symbol( @@ -92,7 +92,7 @@ void goto_symext::symex_start_thread(statet &state) lhs_l1, nil_exprt(), rhs, - guard, + lhs_conditions, symex_targett::assignment_typet::HIDDEN); state.record_events=record_events; } @@ -123,13 +123,13 @@ void goto_symext::symex_start_thread(statet &state) rhs = *zero; } - guardt guard{true_exprt{}}; + exprt::operandst lhs_conditions; symex_assign_symbol( state, lhs, nil_exprt(), rhs, - guard, + lhs_conditions, symex_targett::assignment_typet::HIDDEN); } } From 9727c5e7e8a1c955eab3d223072c640f3999e406 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Mon, 4 Feb 2019 08:29:06 +0000 Subject: [PATCH 04/18] Add guard_manager class and pass it around This in preparation to using BDDs to encode guards, every part of the code creating guards need to reference a guard_manager. --- src/analyses/goto_check.cpp | 9 ++++---- src/analyses/goto_rw.h | 12 ++++++---- src/analyses/guard.h | 17 +++++++++++++- src/cbmc/bmc.cpp | 11 ++++++++- src/cbmc/bmc.h | 19 +++++++++++---- .../multi_path_symex_only_checker.cpp | 3 ++- .../multi_path_symex_only_checker.h | 1 + .../single_path_symex_checker.cpp | 6 +++-- .../single_path_symex_only_checker.cpp | 6 +++-- .../single_path_symex_only_checker.h | 1 + src/goto-checker/symex_bmc.cpp | 11 +++++++-- src/goto-checker/symex_bmc.h | 3 ++- src/goto-instrument/accelerate/accelerate.cpp | 13 +++++++---- src/goto-instrument/accelerate/accelerate.h | 8 +++++-- .../accelerate/acceleration_utils.cpp | 15 ++++++------ .../accelerate/acceleration_utils.h | 23 +++++++++++-------- .../disjunctive_polynomial_acceleration.cpp | 19 +++++++-------- .../disjunctive_polynomial_acceleration.h | 5 +++- .../enumerating_loop_acceleration.h | 14 ++++++++--- .../accelerate/polynomial_accelerator.cpp | 13 ++++++----- .../accelerate/polynomial_accelerator.h | 9 ++++++-- .../accelerate/sat_path_enumerator.cpp | 6 ++--- .../accelerate/sat_path_enumerator.h | 7 ++++-- .../accelerate/scratch_program.cpp | 5 ++-- .../accelerate/scratch_program.h | 13 +++++++---- .../goto_instrument_parse_options.cpp | 3 ++- src/goto-symex/goto_state.h | 10 +++++--- src/goto-symex/goto_symex.h | 10 +++++++- src/goto-symex/goto_symex_state.cpp | 18 ++++++++++----- src/goto-symex/goto_symex_state.h | 10 ++++++-- src/goto-symex/symex_goto.cpp | 4 ++-- src/goto-symex/symex_main.cpp | 3 ++- src/goto-symex/symex_other.cpp | 2 +- src/goto-symex/symex_start_thread.cpp | 2 +- unit/path_strategies.cpp | 11 ++++++++- 35 files changed, 224 insertions(+), 98 deletions(-) diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index b03faaefaba..84d131a2bef 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -84,6 +84,7 @@ class goto_checkt const namespacet &ns; std::unique_ptr 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{}}; + 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())); + guardt(true_exprt(), guard_manager)); } } @@ -1820,7 +1821,7 @@ void goto_checkt::goto_check( "pointer dereference", i.source_location, pointer, - guardt(true_exprt())); + 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())); + guardt(true_exprt(), guard_manager)); } } diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h index d295efb9e73..67667ea8c34 100644 --- a/src/analyses/goto_rw.h +++ b/src/analyses/goto_rw.h @@ -352,8 +352,11 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett public: rw_guarded_range_set_value_sett( const namespacet &_ns, - value_setst &_value_sets): - rw_range_set_value_sett(_ns, _value_sets) + value_setst &_value_sets, + guard_managert &guard_manager) + : rw_range_set_value_sett(_ns, _value_sets), + guard_manager(guard_manager), + guard(true_exprt(), guard_manager) { } @@ -370,7 +373,7 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett get_modet mode, const exprt &expr) override { - guard = guardt(true_exprt()); + guard = guardt(true_exprt(), guard_manager); rw_range_set_value_sett::get_objects_rec(_function, _target, mode, expr); } @@ -384,7 +387,8 @@ class rw_guarded_range_set_value_sett:public rw_range_set_value_sett } protected: - guardt guard = guardt(true_exprt()); + guard_managert &guard_manager; + guardt guard; using rw_range_sett::get_objects_rec; diff --git a/src/analyses/guard.h b/src/analyses/guard.h index 36950c43355..d625cc4e8ed 100644 --- a/src/analyses/guard.h +++ b/src/analyses/guard.h @@ -16,11 +16,26 @@ Author: Daniel Kroening, kroening@kroening.com #include +/// This is unused by this implementation of guards, but can be used by other +/// implementations of the same interface. +struct guard_managert +{ +}; + class guardt { public: - explicit guardt(const exprt &e) : expr(e) + /// Construct a BDD from an expression + /// The \c guard_managert parameter is not used, but we keep it for uniformity + /// with other implementations of guards which may use it. + explicit guardt(const exprt &e, guard_managert &) : expr(e) + { + } + + guardt &operator=(const guardt &other) { + expr = other.expr; + return *this; } void add(const exprt &expr); diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 3b1989bd2cc..44caf9e5280 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -257,6 +257,7 @@ int bmct::do_language_agnostic_bmc( namespacet ns(symbol_table); messaget message(ui); std::unique_ptr worklist; + guard_managert guard_manager; std::string strategy = opts.get_option("exploration-strategy"); worklist = get_path_strategy(strategy); try @@ -268,7 +269,14 @@ int bmct::do_language_agnostic_bmc( std::unique_ptr cbmc_solver = solvers.get_solver(); prop_convt &pc = cbmc_solver->prop_conv(); - bmct bmc(opts, symbol_table, ui, pc, *worklist, callback_after_symex); + bmct bmc( + opts, + symbol_table, + ui, + pc, + *worklist, + callback_after_symex, + guard_manager); if(driver_configure_bmc) driver_configure_bmc(bmc, symbol_table); tmp_result = bmc.run(model); @@ -319,6 +327,7 @@ int bmct::do_language_agnostic_bmc( resume.equation, resume.state, *worklist, + guard_manager, callback_after_symex); if(driver_configure_bmc) driver_configure_bmc(pe, symbol_table); diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 9c879e1ecca..b5bc58a6421 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -70,19 +70,22 @@ class bmct:public safety_checkert ui_message_handlert &_message_handler, prop_convt &_prop_conv, path_storaget &_path_storage, - std::function callback_after_symex) + std::function callback_after_symex, + guard_managert &guard_manager) : safety_checkert(ns, _message_handler), options(_options), outer_symbol_table(outer_symbol_table), ns(outer_symbol_table, symex_symbol_table), equation(_message_handler), + guard_manager(guard_manager), path_storage(_path_storage), symex( _message_handler, outer_symbol_table, equation, options, - path_storage), + path_storage, + guard_manager), prop_conv(_prop_conv), ui_message_handler(_message_handler), driver_callback_after_symex(callback_after_symex) @@ -140,19 +143,22 @@ class bmct:public safety_checkert prop_convt &_prop_conv, symex_target_equationt &_equation, path_storaget &_path_storage, - std::function callback_after_symex) + std::function callback_after_symex, + guard_managert &guard_manager) : safety_checkert(ns, _message_handler), options(_options), outer_symbol_table(outer_symbol_table), ns(outer_symbol_table), equation(_equation), + guard_manager(guard_manager), path_storage(_path_storage), symex( _message_handler, outer_symbol_table, equation, options, - path_storage), + path_storage, + guard_manager), prop_conv(_prop_conv), ui_message_handler(_message_handler), driver_callback_after_symex(callback_after_symex) @@ -170,6 +176,7 @@ class bmct:public safety_checkert symbol_tablet symex_symbol_table; namespacet ns; symex_target_equationt equation; + guard_managert &guard_manager; path_storaget &path_storage; symex_bmct symex; prop_convt &prop_conv; @@ -231,6 +238,7 @@ class path_explorert : public bmct symex_target_equationt &saved_equation, const goto_symex_statet &saved_state, path_storaget &path_storage, + guard_managert &guard_manager, std::function callback_after_symex) : bmct( _options, @@ -239,7 +247,8 @@ class path_explorert : public bmct _prop_conv, saved_equation, path_storage, - callback_after_symex), + callback_after_symex, + guard_manager), saved_state(saved_state) { } diff --git a/src/goto-checker/multi_path_symex_only_checker.cpp b/src/goto-checker/multi_path_symex_only_checker.cpp index c4e0cca89e4..5fdacdeec2f 100644 --- a/src/goto-checker/multi_path_symex_only_checker.cpp +++ b/src/goto-checker/multi_path_symex_only_checker.cpp @@ -32,7 +32,8 @@ multi_path_symex_only_checkert::multi_path_symex_only_checkert( goto_model.get_symbol_table(), equation, options, - path_storage) + path_storage, + guard_manager) { setup_symex(symex, ns, options, ui_message_handler); } diff --git a/src/goto-checker/multi_path_symex_only_checker.h b/src/goto-checker/multi_path_symex_only_checker.h index 2d8a72ab0f1..851a2eb7827 100644 --- a/src/goto-checker/multi_path_symex_only_checker.h +++ b/src/goto-checker/multi_path_symex_only_checker.h @@ -31,6 +31,7 @@ class multi_path_symex_only_checkert : public incremental_goto_checkert symbol_tablet symex_symbol_table; namespacet ns; symex_target_equationt equation; + guard_managert guard_manager; path_fifot path_storage; // should go away symex_bmct symex; }; diff --git a/src/goto-checker/single_path_symex_checker.cpp b/src/goto-checker/single_path_symex_checker.cpp index 4428346e29d..5fb86458a62 100644 --- a/src/goto-checker/single_path_symex_checker.cpp +++ b/src/goto-checker/single_path_symex_checker.cpp @@ -55,7 +55,8 @@ operator()(propertiest &properties) goto_model.get_symbol_table(), equation, options, - *worklist); + *worklist, + guard_manager); setup_symex(symex); symex.initialize_path_storage_from_entry_point_of( @@ -70,7 +71,8 @@ operator()(propertiest &properties) goto_model.get_symbol_table(), resume.equation, options, - *worklist); + *worklist, + guard_manager); setup_symex(symex); symex.resume_symex_from_saved_state( diff --git a/src/goto-checker/single_path_symex_only_checker.cpp b/src/goto-checker/single_path_symex_only_checker.cpp index 81d95e59b67..0bf7938ac13 100644 --- a/src/goto-checker/single_path_symex_only_checker.cpp +++ b/src/goto-checker/single_path_symex_only_checker.cpp @@ -45,7 +45,8 @@ operator()(propertiest &properties) goto_model.get_symbol_table(), equation, options, - *worklist); + *worklist, + guard_manager); setup_symex(symex); symex.initialize_path_storage_from_entry_point_of( @@ -60,7 +61,8 @@ operator()(propertiest &properties) goto_model.get_symbol_table(), resume.equation, options, - *worklist); + *worklist, + guard_manager); setup_symex(symex); symex.resume_symex_from_saved_state( diff --git a/src/goto-checker/single_path_symex_only_checker.h b/src/goto-checker/single_path_symex_only_checker.h index 008c882bcf0..77ca35623ce 100644 --- a/src/goto-checker/single_path_symex_only_checker.h +++ b/src/goto-checker/single_path_symex_only_checker.h @@ -35,6 +35,7 @@ class single_path_symex_only_checkert : public incremental_goto_checkert abstract_goto_modelt &goto_model; symbol_tablet symex_symbol_table; namespacet ns; + guard_managert guard_manager; std::unique_ptr worklist; void equation_output( diff --git a/src/goto-checker/symex_bmc.cpp b/src/goto-checker/symex_bmc.cpp index 7252e23e69b..61cf628c18b 100644 --- a/src/goto-checker/symex_bmc.cpp +++ b/src/goto-checker/symex_bmc.cpp @@ -23,8 +23,15 @@ symex_bmct::symex_bmct( const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, - path_storaget &path_storage) - : goto_symext(mh, outer_symbol_table, _target, options, path_storage), + path_storaget &path_storage, + guard_managert &guard_manager) + : goto_symext( + mh, + outer_symbol_table, + _target, + options, + path_storage, + guard_manager), record_coverage(!options.get_option("symex-coverage-report").empty()), symex_coverage(ns) { diff --git a/src/goto-checker/symex_bmc.h b/src/goto-checker/symex_bmc.h index 5e322d53090..2f9bc6b16b6 100644 --- a/src/goto-checker/symex_bmc.h +++ b/src/goto-checker/symex_bmc.h @@ -30,7 +30,8 @@ class symex_bmct : public goto_symext const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, - path_storaget &path_storage); + path_storaget &path_storage, + guard_managert &guard_manager); // To show progress source_locationt last_source_location; diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp index 55d87def22b..f37a8afe8fd 100644 --- a/src/goto-instrument/accelerate/accelerate.cpp +++ b/src/goto-instrument/accelerate/accelerate.cpp @@ -115,7 +115,8 @@ int acceleratet::accelerate_loop(goto_programt::targett &loop_header) program, loop, loop_header, - accelerate_limit); + accelerate_limit, + guard_manager); #else disjunctive_polynomial_accelerationt acceleration(symbol_table, goto_functions, program, loop, loop_header); @@ -335,7 +336,7 @@ void acceleratet::set_dirty_vars(path_acceleratort &accelerator) if(jt==dirty_vars_map.end()) { - scratch_programt scratch(symbol_table, message_handler); + scratch_programt scratch(symbol_table, message_handler, guard_manager); symbolt new_sym=utils.fresh_symbol("accelerate::dirty", bool_typet()); dirty_var=new_sym.symbol_expr(); dirty_vars_map[*it]=dirty_var; @@ -512,7 +513,8 @@ void acceleratet::insert_automaton(trace_automatont &automaton) // machine. for(const auto &sym : automaton.alphabet) { - scratch_programt state_machine(symbol_table, message_handler); + scratch_programt state_machine{ + symbol_table, message_handler, guard_manager}; trace_automatont::sym_range_pairt p=transitions.equal_range(sym); build_state_machine(p.first, p.second, accept_states, state, next_state, @@ -651,13 +653,14 @@ int acceleratet::accelerate_loops() void accelerate_functions( goto_modelt &goto_model, message_handlert &message_handler, - bool use_z3) + bool use_z3, + guard_managert &guard_manager) { Forall_goto_functions(it, goto_model.goto_functions) { std::cout << "Accelerating function " << it->first << '\n'; acceleratet accelerate( - it->second.body, goto_model, message_handler, use_z3); + it->second.body, goto_model, message_handler, use_z3, guard_manager); int num_accelerated=accelerate.accelerate_loops(); diff --git a/src/goto-instrument/accelerate/accelerate.h b/src/goto-instrument/accelerate/accelerate.h index 9535852041b..c8e2b0f4c9c 100644 --- a/src/goto-instrument/accelerate/accelerate.h +++ b/src/goto-instrument/accelerate/accelerate.h @@ -34,11 +34,13 @@ class acceleratet goto_programt &_program, goto_modelt &_goto_model, message_handlert &message_handler, - bool _use_z3) + bool _use_z3, + guard_managert &guard_manager) : message_handler(message_handler), program(_program), goto_functions(_goto_model.goto_functions), symbol_table(_goto_model.symbol_table), + guard_manager(guard_manager), ns(_goto_model.symbol_table), utils(symbol_table, message_handler, goto_functions), use_z3(_use_z3) @@ -113,6 +115,7 @@ class acceleratet goto_programt &program; goto_functionst &goto_functions; symbol_tablet &symbol_table; + guard_managert &guard_manager; namespacet ns; natural_loops_mutablet natural_loops; subsumed_pathst subsumed; @@ -130,6 +133,7 @@ class acceleratet void accelerate_functions( goto_modelt &, message_handlert &message_handler, - bool use_z3); + bool use_z3, + guard_managert &guard_manager); #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp index d64246c8f0b..95c3e1da5a4 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.cpp +++ b/src/goto-instrument/accelerate/acceleration_utils.cpp @@ -110,10 +110,10 @@ void acceleration_utilst::find_modified( } } - bool acceleration_utilst::check_inductive( std::map polynomials, - patht &path) + patht &path, + guard_managert &guard_manager) { // Checking that our polynomial is inductive with respect to the loop body is // equivalent to checking safety of the following program: @@ -126,7 +126,7 @@ bool acceleration_utilst::check_inductive( // assert (target1==polynomial1); // assert (target2==polynomial2); // ... - scratch_programt program(symbol_table, message_handler); + scratch_programt program(symbol_table, message_handler, guard_manager); std::vector polynomials_hold; substitutiont substitution; @@ -162,7 +162,7 @@ bool acceleration_utilst::check_inductive( try { - if(program.check_sat()) + if(program.check_sat(guard_manager)) { // We found a counterexample to inductiveness... :-( #ifdef DEBUG @@ -353,7 +353,8 @@ void acceleration_utilst::push_nondet(exprt &expr) bool acceleration_utilst::do_assumptions( std::map polynomials, patht &path, - exprt &guard) + exprt &guard, + guard_managert &guard_manager) { // We want to check that if an assumption fails, the next iteration can't be // feasible again. To do this we check the following program for safety: @@ -380,7 +381,7 @@ bool acceleration_utilst::do_assumptions( // assert(!precondition); exprt condition=precondition(path); - scratch_programt program(symbol_table, message_handler); + scratch_programt program(symbol_table, message_handler, guard_manager); substitutiont substitution; stash_polynomials(program, polynomials, substitution, path); @@ -445,7 +446,7 @@ bool acceleration_utilst::do_assumptions( try { - if(program.check_sat()) + if(program.check_sat(guard_manager)) { #ifdef DEBUG std::cout << "Path is not monotone\n"; diff --git a/src/goto-instrument/accelerate/acceleration_utils.h b/src/goto-instrument/accelerate/acceleration_utils.h index c9213919376..d62f4e6eb3a 100644 --- a/src/goto-instrument/accelerate/acceleration_utils.h +++ b/src/goto-instrument/accelerate/acceleration_utils.h @@ -64,12 +64,15 @@ class acceleration_utilst { } - void extract_polynomial(scratch_programt &program, - std::set > &coefficients, - polynomialt &polynomial); - - bool check_inductive(std::map polynomials, - patht &path); + void extract_polynomial( + scratch_programt &program, + std::set> &coefficients, + polynomialt &polynomial); + + bool check_inductive( + std::map polynomials, + patht &path, + guard_managert &guard_manager); void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution); @@ -82,9 +85,11 @@ class acceleration_utilst void abstract_arrays(exprt &expr, expr_mapt &abstractions); void push_nondet(exprt &expr); - bool do_assumptions(std::map polynomials, - patht &body, - exprt &guard); + bool do_assumptions( + std::map polynomials, + patht &body, + exprt &guard, + guard_managert &guard_manager); typedef std::pair expr_pairt; typedef std::vector expr_pairst; diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp index de17d162fce..c2a75aaf40f 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp @@ -50,7 +50,7 @@ bool disjunctive_polynomial_accelerationt::accelerate( path_acceleratort &accelerator) { std::map polynomials; - scratch_programt program(symbol_table, message_handler); + scratch_programt program{symbol_table, message_handler, guard_manager}; accelerator.clear(); @@ -143,7 +143,7 @@ bool disjunctive_polynomial_accelerationt::accelerate( expr_sett dirty; utils.find_modified(accelerator.path, dirty); polynomial_acceleratort path_acceleration( - message_handler, symbol_table, goto_functions, loop_counter); + message_handler, symbol_table, goto_functions, loop_counter, guard_manager); goto_programt::instructionst assigns; for(patht::iterator it=accelerator.path.begin(); @@ -212,7 +212,7 @@ bool disjunctive_polynomial_accelerationt::accelerate( std::map this_poly; this_poly[target]=poly; - if(utils.check_inductive(this_poly, accelerator.path)) + if(utils.check_inductive(this_poly, accelerator.path, guard_manager)) { polynomials[target]=poly; accelerator.changed_vars.insert(target); @@ -245,7 +245,8 @@ bool disjunctive_polynomial_accelerationt::accelerate( try { - path_is_monotone=utils.do_assumptions(polynomials, path, guard); + path_is_monotone = + utils.do_assumptions(polynomials, path, guard, guard_manager); } catch(const std::string &s) { @@ -337,7 +338,7 @@ bool disjunctive_polynomial_accelerationt::accelerate( bool disjunctive_polynomial_accelerationt::find_path(patht &path) { - scratch_programt program(symbol_table, message_handler); + scratch_programt program{symbol_table, message_handler, guard_manager}; program.append(fixed); program.append(fixed); @@ -373,7 +374,7 @@ bool disjunctive_polynomial_accelerationt::find_path(patht &path) try { - if(program.check_sat()) + if(program.check_sat(guard_manager)) { #ifdef DEBUG std::cout << "Found a path\n"; @@ -405,7 +406,7 @@ bool disjunctive_polynomial_accelerationt::fit_polynomial( std::vector parameters; std::set > coefficients; expr_listt exprs; - scratch_programt program(symbol_table, message_handler); + scratch_programt program{symbol_table, message_handler, guard_manager}; expr_sett influence; cone_of_influence(var, influence); @@ -619,7 +620,7 @@ bool disjunctive_polynomial_accelerationt::fit_polynomial( // relevant coefficients and return the expression. try { - if(program.check_sat()) + if(program.check_sat(guard_manager)) { #ifdef DEBUG std::cout << "Found a polynomial\n"; @@ -855,7 +856,7 @@ void disjunctive_polynomial_accelerationt::build_path( */ void disjunctive_polynomial_accelerationt::build_fixed() { - scratch_programt scratch(symbol_table, message_handler); + scratch_programt scratch{symbol_table, message_handler, guard_manager}; std::map shadow_distinguishers; fixed.copy_from(goto_program); diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h index 9fef71f077b..ba11ca64d2a 100644 --- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h +++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h @@ -39,12 +39,14 @@ class disjunctive_polynomial_accelerationt goto_functionst &_goto_functions, goto_programt &_goto_program, natural_loops_mutablet::natural_loopt &_loop, - goto_programt::targett _loop_header) + goto_programt::targett _loop_header, + guard_managert &guard_manager) : message_handler(message_handler), symbol_table(_symbol_table), ns(symbol_table), goto_functions(_goto_functions), goto_program(_goto_program), + guard_manager(guard_manager), loop(_loop), loop_header(_loop_header), utils(symbol_table, message_handler, goto_functions, loop_counter) @@ -89,6 +91,7 @@ class disjunctive_polynomial_accelerationt namespacet ns; goto_functionst &goto_functions; goto_programt &goto_program; + guard_managert &guard_manager; natural_loops_mutablet::natural_loopt &loop; goto_programt::targett loop_header; diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h index df014cb11f2..4fd38cbd35f 100644 --- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h +++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h @@ -36,13 +36,19 @@ class enumerating_loop_accelerationt goto_programt &_goto_program, natural_loops_mutablet::natural_loopt &_loop, goto_programt::targett _loop_header, - int _path_limit) + int _path_limit, + guard_managert &guard_manager) : symbol_table(_symbol_table), goto_functions(_goto_functions), goto_program(_goto_program), loop(_loop), loop_header(_loop_header), - polynomial_accelerator(message_handler, symbol_table, goto_functions), + guard_manager(guard_manager), + polynomial_accelerator( + message_handler, + symbol_table, + goto_functions, + guard_manager), path_limit(_path_limit), path_enumerator( util_make_unique( @@ -51,7 +57,8 @@ class enumerating_loop_accelerationt goto_functions, goto_program, loop, - loop_header)) + loop_header, + guard_manager)) { } @@ -63,6 +70,7 @@ class enumerating_loop_accelerationt goto_programt &goto_program; natural_loops_mutablet::natural_loopt &loop; goto_programt::targett loop_header; + guard_managert &guard_manager; polynomial_acceleratort polynomial_accelerator; int path_limit; diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp index 746596aa469..4989b494584 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp +++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp @@ -58,7 +58,7 @@ bool polynomial_acceleratort::accelerate( expr_sett targets; std::map polynomials; - scratch_programt program(symbol_table, message_handler); + scratch_programt program{symbol_table, message_handler, guard_manager}; goto_programt::instructionst assigns; utils.find_modified(body, targets); @@ -178,7 +178,8 @@ bool polynomial_acceleratort::accelerate( try { - path_is_monotone=utils.do_assumptions(polynomials, loop, guard); + path_is_monotone = + utils.do_assumptions(polynomials, loop, guard, guard_manager); } catch(const std::string &s) { @@ -284,7 +285,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced( std::vector parameters; std::set > coefficients; expr_listt exprs; - scratch_programt program(symbol_table, message_handler); + scratch_programt program{symbol_table, message_handler, guard_manager}; exprt overflow_var = utils.fresh_symbol("polynomial::overflow", bool_typet()).symbol_expr(); overflow_instrumentert overflow(program, overflow_var, symbol_table); @@ -412,7 +413,7 @@ bool polynomial_acceleratort::fit_polynomial_sliced( // relevant coefficients and return the expression. try { - if(program.check_sat()) + if(program.check_sat(guard_manager)) { utils.extract_polynomial(program, coefficients, polynomial); return true; @@ -666,7 +667,7 @@ bool polynomial_acceleratort::check_inductive( // assert (target1==polynomial1); // assert (target2==polynomial2); // ... - scratch_programt program(symbol_table, message_handler); + scratch_programt program{symbol_table, message_handler, guard_manager}; std::vector polynomials_hold; substitutiont substitution; @@ -703,7 +704,7 @@ bool polynomial_acceleratort::check_inductive( try { - if(program.check_sat()) + if(program.check_sat(guard_manager)) { // We found a counterexample to inductiveness... :-( #ifdef DEBUG diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.h b/src/goto-instrument/accelerate/polynomial_accelerator.h index a9d2eb8ff40..a05c16ecdd0 100644 --- a/src/goto-instrument/accelerate/polynomial_accelerator.h +++ b/src/goto-instrument/accelerate/polynomial_accelerator.h @@ -34,11 +34,13 @@ class polynomial_acceleratort polynomial_acceleratort( message_handlert &message_handler, const symbol_tablet &_symbol_table, - const goto_functionst &_goto_functions) + const goto_functionst &_goto_functions, + guard_managert &guard_manager) : message_handler(message_handler), symbol_table(const_cast(_symbol_table)), ns(symbol_table), goto_functions(_goto_functions), + guard_manager(guard_manager), utils(symbol_table, message_handler, goto_functions, loop_counter) { loop_counter=nil_exprt(); @@ -48,11 +50,13 @@ class polynomial_acceleratort message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, - exprt &_loop_counter) + exprt &_loop_counter, + guard_managert &guard_manager) : message_handler(message_handler), symbol_table(const_cast(_symbol_table)), ns(symbol_table), goto_functions(_goto_functions), + guard_manager(guard_manager), utils(symbol_table, message_handler, goto_functions, loop_counter), loop_counter(_loop_counter) { @@ -153,6 +157,7 @@ class polynomial_acceleratort symbol_tablet &symbol_table; const namespacet ns; const goto_functionst &goto_functions; + guard_managert &guard_manager; acceleration_utilst utils; exprt loop_counter; diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.cpp b/src/goto-instrument/accelerate/sat_path_enumerator.cpp index 3dd2bb2ab36..56ba3bda277 100644 --- a/src/goto-instrument/accelerate/sat_path_enumerator.cpp +++ b/src/goto-instrument/accelerate/sat_path_enumerator.cpp @@ -47,7 +47,7 @@ Author: Matt Lewis bool sat_path_enumeratort::next(patht &path) { - scratch_programt program(symbol_table, message_handler); + scratch_programt program{symbol_table, message_handler, guard_manager}; program.append(fixed); program.append(fixed); @@ -83,7 +83,7 @@ bool sat_path_enumeratort::next(patht &path) try { - if(program.check_sat()) + if(program.check_sat(guard_manager)) { #ifdef DEBUG std::cout << "Found a path\n"; @@ -212,7 +212,7 @@ void sat_path_enumeratort::build_path( */ void sat_path_enumeratort::build_fixed() { - scratch_programt scratch(symbol_table, message_handler); + scratch_programt scratch{symbol_table, message_handler, guard_manager}; std::map shadow_distinguishers; fixed.copy_from(goto_program); diff --git a/src/goto-instrument/accelerate/sat_path_enumerator.h b/src/goto-instrument/accelerate/sat_path_enumerator.h index 155785e6994..c2b055e67a1 100644 --- a/src/goto-instrument/accelerate/sat_path_enumerator.h +++ b/src/goto-instrument/accelerate/sat_path_enumerator.h @@ -39,7 +39,8 @@ class sat_path_enumeratort:public path_enumeratort goto_functionst &_goto_functions, goto_programt &_goto_program, natural_loops_mutablet::natural_loopt &_loop, - goto_programt::targett _loop_header) + goto_programt::targett _loop_header, + guard_managert &guard_manager) : message_handler(message_handler), symbol_table(_symbol_table), ns(symbol_table), @@ -47,7 +48,8 @@ class sat_path_enumeratort:public path_enumeratort goto_program(_goto_program), loop(_loop), loop_header(_loop_header), - utils(symbol_table, message_handler, goto_functions, loop_counter) + utils(symbol_table, message_handler, goto_functions, loop_counter), + guard_manager(guard_manager) { find_distinguishing_points(); build_fixed(); @@ -75,6 +77,7 @@ class sat_path_enumeratort:public path_enumeratort typedef std::map distinguish_valuest; acceleration_utilst utils; + guard_managert &guard_manager; exprt loop_counter; distinguish_mapt distinguishing_points; std::list distinguishers; diff --git a/src/goto-instrument/accelerate/scratch_program.cpp b/src/goto-instrument/accelerate/scratch_program.cpp index 78349142762..de101357478 100644 --- a/src/goto-instrument/accelerate/scratch_program.cpp +++ b/src/goto-instrument/accelerate/scratch_program.cpp @@ -22,7 +22,7 @@ Author: Matt Lewis #include #endif -bool scratch_programt::check_sat(bool do_slice) +bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager) { fix_types(); @@ -36,7 +36,8 @@ bool scratch_programt::check_sat(bool do_slice) #endif symex_state = util_make_unique( - symex_targett::sourcet(goto_functionst::entry_point(), *this)); + symex_targett::sourcet(goto_functionst::entry_point(), *this), + guard_manager); symex.symex_with_state( *symex_state, [this](const irep_idt &key) -> const goto_functionst::goto_functiont & { diff --git a/src/goto-instrument/accelerate/scratch_program.h b/src/goto-instrument/accelerate/scratch_program.h index a0f294bae4f..a5b65df78a6 100644 --- a/src/goto-instrument/accelerate/scratch_program.h +++ b/src/goto-instrument/accelerate/scratch_program.h @@ -36,7 +36,10 @@ Author: Matt Lewis class scratch_programt:public goto_programt { public: - scratch_programt(symbol_tablet &_symbol_table, message_handlert &mh) + scratch_programt( + symbol_tablet &_symbol_table, + message_handlert &mh, + guard_managert &guard_manager) : constant_propagation(true), symbol_table(_symbol_table), symex_symbol_table(), @@ -44,7 +47,7 @@ class scratch_programt:public goto_programt equation(mh), path_storage(), options(get_default_options()), - symex(mh, symbol_table, equation, options, path_storage), + symex(mh, symbol_table, equation, options, path_storage, guard_manager), satcheck(util_make_unique(mh)), satchecker(ns, *satcheck), z3(ns, "accelerate", "", "", smt2_dect::solvert::Z3), @@ -60,11 +63,11 @@ class scratch_programt:public goto_programt targett assign(const exprt &lhs, const exprt &rhs); targett assume(const exprt &guard); - bool check_sat(bool do_slice); + bool check_sat(bool do_slice, guard_managert &guard_manager); - bool check_sat() + bool check_sat(guard_managert &guard_manager) { - return check_sat(true); + return check_sat(true, guard_manager); } exprt eval(const exprt &e); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 1b868cdce13..3772246accd 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -764,8 +764,9 @@ int goto_instrument_parse_optionst::doit() remove_calls_no_body(goto_model.goto_functions); status() << "Accelerating" << eom; + guard_managert guard_manager; accelerate_functions( - goto_model, get_message_handler(), cmdline.isset("z3")); + goto_model, get_message_handler(), cmdline.isset("z3"), guard_manager); remove_skip(goto_model); } diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h index c34c7df98da..10f7fb64a21 100644 --- a/src/goto-symex/goto_state.h +++ b/src/goto-symex/goto_state.h @@ -12,9 +12,9 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com #ifndef CPROVER_GOTO_SYMEX_GOTO_STATE_H #define CPROVER_GOTO_SYMEX_GOTO_STATE_H +#include #include #include -#include #include "renaming_level.h" #include "symex_target_equation.h" @@ -39,7 +39,7 @@ class goto_statet // the if branch will be guarded by the condition of the if (and if there // is an else branch then instructions on it will be guarded by the negation // of the condition of the if). - guardt guard{true_exprt{}}; + guardt guard; symex_targett::sourcet source; @@ -62,7 +62,11 @@ class goto_statet /// Constructors explicit goto_statet(const class goto_symex_statet &s); - explicit goto_statet(const symex_targett::sourcet &_source) : source(_source) + + goto_statet( + const symex_targett::sourcet &_source, + guard_managert &guard_manager) + : guard(true_exprt(), guard_manager), source(_source) { } }; diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 616291efeab..695fbd698af 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -89,16 +89,19 @@ class goto_symext /// \param options: The options to use to configure this execution /// \param path_storage: Place to storage symbolic execution paths that have /// been halted and can be resumed later + /// \param guard_manager: Manager for creating guards goto_symext( message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, - path_storaget &path_storage) + path_storaget &path_storage, + guard_managert &guard_manager) : should_pause_symex(false), symex_config(options), outer_symbol_table(outer_symbol_table), ns(outer_symbol_table), + guard_manager(guard_manager), target(_target), atomic_section_counter(0), log(mh), @@ -245,6 +248,11 @@ class goto_symext /// goto-program, and the names of dynamically-created objects. namespacet ns; + /// Used to create guards. Guards created with different guard managers cannot + /// be combined together, so guards created by goto-symex should not escape + /// the scope of this manager. + guard_managert &guard_manager; + /// The equation that this execution is building up symex_target_equationt ⌖ diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 6e9283025be..584a077cc20 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -29,10 +29,16 @@ Author: Daniel Kroening, kroening@kroening.com static void get_l1_name(exprt &expr); -goto_symex_statet::goto_symex_statet(const symex_targett::sourcet &_source) - : goto_statet(_source), symex_target(nullptr), record_events(true), dirty() +goto_symex_statet::goto_symex_statet( + const symex_targett::sourcet &_source, + guard_managert &manager) + : goto_statet(_source, manager), + guard_manager(manager), + symex_target(nullptr), + record_events(true), + dirty() { - threads.resize(1); + threads.emplace_back(guard_manager); call_stack().new_frame(source); } @@ -385,7 +391,7 @@ bool goto_symex_statet::l2_thread_read_encoding( // see whether we are within an atomic section if(atomic_section_id!=0) { - guardt write_guard{false_exprt{}}; + guardt write_guard{false_exprt{}, guard_manager}; const auto a_s_writes = written_in_atomic_section.find(ssa_l1); if(a_s_writes!=written_in_atomic_section.end()) @@ -409,7 +415,7 @@ bool goto_symex_statet::l2_thread_read_encoding( // we cannot determine for sure that there has been a write already // so generate a read even if l1_identifier has been written on // all branches flowing into this read - guardt read_guard{false_exprt{}}; + guardt read_guard{false_exprt{}, guard_manager}; a_s_r_entryt &a_s_read=read_in_atomic_section[ssa_l1]; for(const auto &a_s_read_guard : a_s_read.second) @@ -427,7 +433,7 @@ bool goto_symex_statet::l2_thread_read_encoding( guardt cond = read_guard; if(!no_write.op().is_false()) - cond |= guardt{no_write.op()}; + cond |= guardt{no_write.op(), guard_manager}; const renamedt l2_true_case = set_indices(ssa_l1, ns); diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index f0e085509ea..9b42c09417b 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -41,7 +41,7 @@ Author: Daniel Kroening, kroening@kroening.com class goto_symex_statet final : public goto_statet { public: - explicit goto_symex_statet(const symex_targett::sourcet &); + goto_symex_statet(const symex_targett::sourcet &, guard_managert &manager); ~goto_symex_statet(); /// \brief Fake "copy constructor" that initializes the `symex_target` member @@ -58,6 +58,8 @@ class goto_symex_statet final : public goto_statet /// for error traces even after symbolic execution has finished. symbol_tablet symbol_table; + // Manager is required to be able to resize the thread vector + guard_managert &guard_manager; symex_target_equationt *symex_target; symex_level0t level0; @@ -155,10 +157,14 @@ class goto_symex_statet final : public goto_statet struct threadt { goto_programt::const_targett pc; - guardt guard{true_exprt{}}; + guardt guard; call_stackt call_stack; std::map function_frame; unsigned atomic_section_id = 0; + explicit threadt(guard_managert &guard_manager) + : guard(true_exprt(), guard_manager) + { + } }; std::vector threads; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index e569bda6d8a..a47f266f952 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -217,7 +217,7 @@ void goto_symext::symex_goto(statet &state) // adjust guards if(new_guard.is_true()) { - state.guard = guardt(false_exprt()); + state.guard = guardt(false_exprt(), guard_manager); } else { @@ -241,7 +241,7 @@ void goto_symext::symex_goto(statet &state) state.rename_ssa(ssa_exprt{guard_symbol_expr}, ns); state.assignment(new_lhs, new_rhs, ns, true, false); - guardt guard{true_exprt{}}; + guardt guard{true_exprt{}, guard_manager}; log.conditional_output( log.debug(), diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 78d9f90ef5d..debf8f8f9f9 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -328,7 +328,8 @@ std::unique_ptr goto_symext::initialize_entry_point_state( // create and prepare the state auto state = util_make_unique( - symex_targett::sourcet(entry_point_id, start_function->body)); + symex_targett::sourcet(entry_point_id, start_function->body), + guard_manager); CHECK_RETURN(!state->threads.empty()); CHECK_RETURN(!state->call_stack().empty()); diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 88c1dfdfa42..2614e0da4f2 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -274,7 +274,7 @@ void goto_symext::symex_other( clean_expr(object, state, false); process_array_expr(state, object); - havoc_rec(state, guardt(true_exprt()), object); + havoc_rec(state, guardt(true_exprt(), guard_manager), object); } else UNREACHABLE; diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp index 9c08ec6ad35..e4e5b8306f6 100644 --- a/src/goto-symex/symex_start_thread.cpp +++ b/src/goto-symex/symex_start_thread.cpp @@ -37,7 +37,7 @@ void goto_symext::symex_start_thread(statet &state) // put into thread vector std::size_t t=state.threads.size(); - state.threads.push_back(statet::threadt()); + state.threads.push_back(statet::threadt(guard_manager)); // statet::threadt &cur_thread=state.threads[state.source.thread_nr]; statet::threadt &new_thread=state.threads.back(); new_thread.pc=thread_target; diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index 2dbdf2c7afb..5e95f88c872 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -369,6 +369,7 @@ void _check_with_strategy( REQUIRE(is_valid_path_strategy(strategy)); std::unique_ptr worklist = get_path_strategy(strategy); + guard_managert guard_manager; goto_modelt gm; int ret; @@ -385,7 +386,14 @@ void _check_with_strategy( safety_checkert::resultt overall_result = safety_checkert::resultt::SAFE; std::size_t expected_results_cnt = 0; - bmct bmc(opts, gm.get_symbol_table(), mh, initial_pc, *worklist, callback); + bmct bmc( + opts, + gm.get_symbol_table(), + mh, + initial_pc, + *worklist, + callback, + guard_manager); safety_checkert::resultt tmp_result = bmc.run(gm); if(tmp_result != safety_checkert::resultt::PAUSED) @@ -417,6 +425,7 @@ void _check_with_strategy( resume.equation, resume.state, *worklist, + guard_manager, callback); tmp_result = pe.run(gm); From 4da4bd3dbeda618eacb0a2156dcb7ef61f3414a3 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 20 Feb 2019 16:48:24 +0000 Subject: [PATCH 05/18] Remove unused field ns field of bdd_exprt A reference to a namespace was stored without being ever used. --- src/solvers/prop/bdd_expr.h | 5 +---- unit/solvers/bdd/miniBDD/miniBDD.cpp | 2 +- unit/solvers/prop/bdd_expr.cpp | 8 ++++---- 3 files changed, 6 insertions(+), 9 deletions(-) diff --git a/src/solvers/prop/bdd_expr.h b/src/solvers/prop/bdd_expr.h index 0314ae4da9d..1c0d8f533bb 100644 --- a/src/solvers/prop/bdd_expr.h +++ b/src/solvers/prop/bdd_expr.h @@ -25,14 +25,12 @@ Author: Michael Tautschnig, michael.tautschnig@qmul.ac.uk #include -class namespacet; - /*! \brief TO_BE_DOCUMENTED */ class bdd_exprt { public: - explicit bdd_exprt(const namespacet &_ns) : ns(_ns), root(bdd_mgr.bdd_true()) + explicit bdd_exprt() : root(bdd_mgr.bdd_true()) { } @@ -40,7 +38,6 @@ class bdd_exprt exprt as_expr() const; protected: - const namespacet &ns; bdd_managert bdd_mgr; bddt root; diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp index 2eafa4deb96..3b008e360ca 100644 --- a/unit/solvers/bdd/miniBDD/miniBDD.cpp +++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp @@ -341,7 +341,7 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") REQUIRE(oss.str() == "(a ∧ b) ∨ ¬a"); } - bdd_exprt t(ns); + bdd_exprt t; t.from_expr(o); { diff --git a/unit/solvers/prop/bdd_expr.cpp b/unit/solvers/prop/bdd_expr.cpp index 21eeda5ae97..3463262bfe4 100644 --- a/unit/solvers/prop/bdd_expr.cpp +++ b/unit/solvers/prop/bdd_expr.cpp @@ -23,7 +23,7 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]") GIVEN("A bdd for x&!x") { - bdd_exprt bdd{ns}; + bdd_exprt bdd; const symbol_exprt var("x", bool_typet()); bdd.from_expr(and_exprt(var, not_exprt(var))); REQUIRE(bdd.as_expr() == false_exprt()); @@ -34,12 +34,12 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]") const symbol_exprt a("a", bool_typet()); const symbol_exprt b("b", bool_typet()); - bdd_exprt bdd{ns}; + bdd_exprt bdd; bdd.from_expr(or_exprt(and_exprt(a, b), not_exprt(a))); THEN("It is equal to the BDD for (!a|b)") { - bdd_exprt bdd2{ns}; + bdd_exprt bdd2; bdd2.from_expr(or_exprt(not_exprt(a), b)); REQUIRE(bdd.as_expr() == bdd2.as_expr()); } @@ -50,7 +50,7 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]") const symbol_exprt a("a", bool_typet()); const symbol_exprt b("b", bool_typet()); - bdd_exprt bdd{ns}; + bdd_exprt bdd; bdd.from_expr(and_exprt(a, not_exprt(b))); WHEN("It is converted to an exprt") From f9a698ce24abd3f91c3a7bd00d8ca92b962ec506 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 20 Feb 2019 16:56:37 +0000 Subject: [PATCH 06/18] Remove root field of bdd_exprt 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. --- src/solvers/prop/bdd_expr.cpp | 6 +++--- src/solvers/prop/bdd_expr.h | 16 +++++++--------- unit/solvers/bdd/miniBDD/miniBDD.cpp | 6 +++--- unit/solvers/prop/bdd_expr.cpp | 22 +++++++++++----------- 4 files changed, 24 insertions(+), 26 deletions(-) diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp index 1443a1b8b34..b9fdaff9ced 100644 --- a/src/solvers/prop/bdd_expr.cpp +++ b/src/solvers/prop/bdd_expr.cpp @@ -88,9 +88,9 @@ bddt bdd_exprt::from_expr_rec(const exprt &expr) } } -void bdd_exprt::from_expr(const exprt &expr) +bddt bdd_exprt::from_expr(const exprt &expr) { - root=from_expr_rec(expr); + return from_expr_rec(expr); } exprt bdd_exprt::as_expr(const bdd_nodet &r, bool complement) const @@ -148,7 +148,7 @@ exprt bdd_exprt::as_expr(const bdd_nodet &r, bool complement) const as_expr(r.else_branch(), r.else_branch().is_complement() != complement)); } -exprt bdd_exprt::as_expr() const +exprt bdd_exprt::as_expr(const bddt &root) const { const bdd_nodet node = bdd_mgr.bdd_node(root); return as_expr(node, node.is_complement()); diff --git a/src/solvers/prop/bdd_expr.h b/src/solvers/prop/bdd_expr.h index 1c0d8f533bb..ee0cb23badc 100644 --- a/src/solvers/prop/bdd_expr.h +++ b/src/solvers/prop/bdd_expr.h @@ -25,21 +25,19 @@ Author: Michael Tautschnig, michael.tautschnig@qmul.ac.uk #include -/*! \brief TO_BE_DOCUMENTED -*/ +/// Conversion between \c exprt and \c bbdt +/// This encapsulate a bdd_managert, thus BDDs created with this class should +/// only be combined with BDDs created using the same instance of +/// \ref bdd_exprt . +/// See unit tests in unit/solvers/prop/bdd_expr.cpp for examples. class bdd_exprt { public: - explicit bdd_exprt() : root(bdd_mgr.bdd_true()) - { - } - - void from_expr(const exprt &expr); - exprt as_expr() const; + bddt from_expr(const exprt &expr); + exprt as_expr(const bddt &root) const; protected: bdd_managert bdd_mgr; - bddt root; typedef std::unordered_map expr_mapt; expr_mapt expr_map; diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp index 3b008e360ca..afcf8bb84c7 100644 --- a/unit/solvers/bdd/miniBDD/miniBDD.cpp +++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp @@ -341,12 +341,12 @@ SCENARIO("miniBDD", "[core][solver][miniBDD]") REQUIRE(oss.str() == "(a ∧ b) ∨ ¬a"); } - bdd_exprt t; - t.from_expr(o); + bdd_exprt bdd_expr_converter; + bddt t = bdd_expr_converter.from_expr(o); { std::ostringstream oss; - oss << format(t.as_expr()); + oss << format(bdd_expr_converter.as_expr(t)); REQUIRE(oss.str() == "¬a ∨ b"); } } diff --git a/unit/solvers/prop/bdd_expr.cpp b/unit/solvers/prop/bdd_expr.cpp index 3463262bfe4..87ba262e0ea 100644 --- a/unit/solvers/prop/bdd_expr.cpp +++ b/unit/solvers/prop/bdd_expr.cpp @@ -20,13 +20,14 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]") { symbol_tablet symbol_table; namespacet ns{symbol_table}; + bdd_exprt bdd_expr_converter; GIVEN("A bdd for x&!x") { - bdd_exprt bdd; const symbol_exprt var("x", bool_typet()); - bdd.from_expr(and_exprt(var, not_exprt(var))); - REQUIRE(bdd.as_expr() == false_exprt()); + const bddt bdd = + bdd_expr_converter.from_expr(and_exprt(var, not_exprt(var))); + REQUIRE(bdd_expr_converter.as_expr(bdd) == false_exprt()); } GIVEN("A bdd for (a&b)|!a") @@ -34,14 +35,14 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]") const symbol_exprt a("a", bool_typet()); const symbol_exprt b("b", bool_typet()); - bdd_exprt bdd; - bdd.from_expr(or_exprt(and_exprt(a, b), not_exprt(a))); + const bddt bdd = + bdd_expr_converter.from_expr(or_exprt(and_exprt(a, b), not_exprt(a))); THEN("It is equal to the BDD for (!a|b)") { - bdd_exprt bdd2; - bdd2.from_expr(or_exprt(not_exprt(a), b)); - REQUIRE(bdd.as_expr() == bdd2.as_expr()); + const bddt bdd2 = bdd_expr_converter.from_expr(or_exprt(not_exprt(a), b)); + REQUIRE( + bdd_expr_converter.as_expr(bdd) == bdd_expr_converter.as_expr(bdd2)); } } @@ -50,12 +51,11 @@ SCENARIO("bdd_expr", "[core][solver][prop][bdd_expr]") const symbol_exprt a("a", bool_typet()); const symbol_exprt b("b", bool_typet()); - bdd_exprt bdd; - bdd.from_expr(and_exprt(a, not_exprt(b))); + const bddt bdd = bdd_expr_converter.from_expr(and_exprt(a, not_exprt(b))); WHEN("It is converted to an exprt") { - const exprt result = bdd.as_expr(); + const exprt result = bdd_expr_converter.as_expr(bdd); THEN("It is equal to the expression (a & !b) or (!b & a)") { REQUIRE(result.id() == ID_and); From f640d73ed10f377620f2efe62fdb99f36a44a0c9 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 20 Feb 2019 17:58:11 +0000 Subject: [PATCH 07/18] Define idt type for bdd_node::id() functions 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. --- src/solvers/bdd/bdd_cudd.h | 7 +++++-- src/solvers/bdd/bdd_miniBDD.h | 7 +++++-- 2 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/solvers/bdd/bdd_cudd.h b/src/solvers/bdd/bdd_cudd.h index c25f4d57c53..01757d75dc6 100644 --- a/src/solvers/bdd/bdd_cudd.h +++ b/src/solvers/bdd/bdd_cudd.h @@ -51,10 +51,13 @@ class bdd_nodet return bdd_nodet(Cudd_E(node)); } + /// Return type for \ref id() + using idt = DdNode *; + /// Unique identifier of the node - long id() const + idt id() const { - return (long)node; + return node; } private: diff --git a/src/solvers/bdd/bdd_miniBDD.h b/src/solvers/bdd/bdd_miniBDD.h index fba9dc1a807..d4a04feeefe 100644 --- a/src/solvers/bdd/bdd_miniBDD.h +++ b/src/solvers/bdd/bdd_miniBDD.h @@ -55,10 +55,13 @@ class bdd_nodet return bdd_nodet(node->low.node, bdd_var_to_index); } + /// Return type for \ref id() + using idt = mini_bdd_nodet *; + /// Unique identifier of the node - long id() const + idt id() const { - return (long)node; + return node; } private: From c63b9df70f15b80b177d7a649ebbf02a3662b808 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 12 Feb 2019 16:36:14 +0000 Subject: [PATCH 08/18] Add a cache to as_expr function for BDDs 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. --- src/solvers/prop/bdd_expr.cpp | 102 ++++++++++++++++++++++------------ src/solvers/prop/bdd_expr.h | 9 ++- 2 files changed, 75 insertions(+), 36 deletions(-) diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp index b9fdaff9ced..c810f43e080 100644 --- a/src/solvers/prop/bdd_expr.cpp +++ b/src/solvers/prop/bdd_expr.cpp @@ -93,7 +93,15 @@ bddt bdd_exprt::from_expr(const exprt &expr) return from_expr_rec(expr); } -exprt bdd_exprt::as_expr(const bdd_nodet &r, bool complement) const +/// Helper function for \c bddt to \c exprt conversion +/// \param r: node to convert +/// \param complement: whether we want the negation of the expression +/// represented by r +/// \param cache: map of already computed values +exprt bdd_exprt::as_expr( + const bdd_nodet &r, + bool complement, + std::unordered_map &cache) const { if(r.is_constant()) { @@ -106,50 +114,74 @@ exprt bdd_exprt::as_expr(const bdd_nodet &r, bool complement) const INVARIANT(r.index() < node_map.size(), "Index should be in node_map"); const exprt &n_expr = node_map[r.index()]; - if(r.else_branch().is_constant()) + // Look-up cache for already computed value + auto insert_result = cache.emplace(r.id(), nil_exprt()); + if(insert_result.second) { - if(r.then_branch().is_constant()) - { - if(r.else_branch().is_complement() != complement) - return n_expr; - return not_exprt(n_expr); - } - else - { - if(r.else_branch().is_complement() != complement) + insert_result.first->second = [&]() -> exprt { + if(r.else_branch().is_constant()) + { + if(r.then_branch().is_constant()) + { + if(r.else_branch().is_complement() != complement) + return n_expr; + return not_exprt(n_expr); + } + else + { + if(r.else_branch().is_complement() != complement) + { + return and_exprt( + n_expr, + as_expr( + r.then_branch(), + complement != r.then_branch().is_complement(), + cache)); + } + return or_exprt( + not_exprt(n_expr), + as_expr( + r.then_branch(), + complement != r.then_branch().is_complement(), + cache)); + } + } + else if(r.then_branch().is_constant()) { - return and_exprt( + if(r.then_branch().is_complement() != complement) + { + return and_exprt( + not_exprt(n_expr), + as_expr( + r.else_branch(), + complement != r.else_branch().is_complement(), + cache)); + } + return or_exprt( n_expr, as_expr( - r.then_branch(), complement != r.then_branch().is_complement())); + r.else_branch(), + complement != r.else_branch().is_complement(), + cache)); } - return or_exprt( - not_exprt(n_expr), + return if_exprt( + n_expr, as_expr( - r.then_branch(), complement != r.then_branch().is_complement())); - } - } - else if(r.then_branch().is_constant()) - { - if(r.then_branch().is_complement() != complement) - { - return and_exprt( - not_exprt(n_expr), + r.then_branch(), + r.then_branch().is_complement() != complement, + cache), as_expr( - r.else_branch(), complement != r.else_branch().is_complement())); - } - return or_exprt( - n_expr, - as_expr(r.else_branch(), complement != r.else_branch().is_complement())); + r.else_branch(), + r.else_branch().is_complement() != complement, + cache)); + }(); } - return if_exprt( - n_expr, - as_expr(r.then_branch(), r.then_branch().is_complement() != complement), - as_expr(r.else_branch(), r.else_branch().is_complement() != complement)); + return insert_result.first->second; } exprt bdd_exprt::as_expr(const bddt &root) const { - const bdd_nodet node = bdd_mgr.bdd_node(root); - return as_expr(node, node.is_complement()); + std::unordered_map cache; + bdd_nodet node = bdd_mgr.bdd_node(root); + return as_expr(node, node.is_complement(), cache); } diff --git a/src/solvers/prop/bdd_expr.h b/src/solvers/prop/bdd_expr.h index ee0cb23badc..f8543b659ce 100644 --- a/src/solvers/prop/bdd_expr.h +++ b/src/solvers/prop/bdd_expr.h @@ -40,11 +40,18 @@ class bdd_exprt bdd_managert bdd_mgr; typedef std::unordered_map expr_mapt; + expr_mapt expr_map; + + /// Mapping from BDD variables to expressions: the expression at index \c i + /// of \p node_map corresponds to the i-th variable std::vector node_map; bddt from_expr_rec(const exprt &expr); - exprt as_expr(const bdd_nodet &r, bool complement) const; + exprt as_expr( + const bdd_nodet &r, + bool complement, + std::unordered_map &cache) const; }; #endif // CPROVER_SOLVERS_PROP_BDD_EXPR_H From f164c8354c6acbe51b64bbd3fd8a21e7ee09e4cd Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 15 Jan 2019 14:54:28 +0000 Subject: [PATCH 09/18] New implementation of guards using BDDs 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. --- src/analyses/CMakeLists.txt | 6 +- src/analyses/Makefile | 1 + src/analyses/guard_bdd.cpp | 96 ++++++++++++++++++++++++++++ src/analyses/guard_bdd.h | 72 +++++++++++++++++++++ src/analyses/module_dependencies.txt | 2 + src/goto-symex/CMakeLists.txt | 4 ++ 6 files changed, 180 insertions(+), 1 deletion(-) create mode 100644 src/analyses/guard_bdd.cpp create mode 100644 src/analyses/guard_bdd.h diff --git a/src/analyses/CMakeLists.txt b/src/analyses/CMakeLists.txt index 03be00fc8de..e030a507f63 100644 --- a/src/analyses/CMakeLists.txt +++ b/src/analyses/CMakeLists.txt @@ -3,4 +3,8 @@ add_library(analyses ${sources}) generic_includes(analyses) -target_link_libraries(analyses util pointer-analysis) +if(CMAKE_USE_CUDD) + target_include_directories(analyses PUBLIC ${CUDD_INCLUDE}/cudd/) +endif() + +target_link_libraries(analyses util pointer-analysis solvers) diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 799bab28663..72f2066603a 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -13,6 +13,7 @@ SRC = ai.cpp \ goto_check.cpp \ goto_rw.cpp \ guard.cpp \ + guard_bdd.cpp \ interval_analysis.cpp \ interval_domain.cpp \ invariant_propagation.cpp \ diff --git a/src/analyses/guard_bdd.cpp b/src/analyses/guard_bdd.cpp new file mode 100644 index 00000000000..1ded532f190 --- /dev/null +++ b/src/analyses/guard_bdd.cpp @@ -0,0 +1,96 @@ +/*******************************************************************\ + +Module: Guard Data Structure + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +/// \file +/// Implementation of guards using BDDs + +#include "guard_bdd.h" + +#include +#include +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +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; +} + +void guard_bddt::guard_expr(exprt &dest) const +{ + if(is_true()) + { + // do nothing + } + else + { + if(dest.is_false()) + { + dest = boolean_negate(as_expr()); + } + else + { + implies_exprt tmp; + tmp.op0() = as_expr(); + tmp.op1().swap(dest); + dest.swap(tmp); + } + } +} + +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); +} diff --git a/src/analyses/guard_bdd.h b/src/analyses/guard_bdd.h new file mode 100644 index 00000000000..33a8ae4438d --- /dev/null +++ b/src/analyses/guard_bdd.h @@ -0,0 +1,72 @@ +/*******************************************************************\ + +Module: Guard Data Structure + +Author: Romain Brenguier, romain.brenguier@diffblue.com + +\*******************************************************************/ + +/// \file +/// Guard Data Structure +/// Implementation using BDDs + +#ifndef CPROVER_ANALYSES_GUARD_BDD_H +#define CPROVER_ANALYSES_GUARD_BDD_H + +#include +#include + +#include +#include +#include +#include + +class guard_bddt +{ +public: + guard_bddt(const exprt &e, bdd_exprt &manager); + guard_bddt(const guard_bddt &other) : manager(other.manager), bdd(other.bdd) + { + } + + guard_bddt &operator=(const guard_bddt &other); + guard_bddt &operator=(guard_bddt &&other); + guard_bddt &add(const exprt &expr); + guard_bddt &append(const guard_bddt &guard); + exprt as_expr() const; + + /// Assign dest to `guard => dest` unless guard or dest are trivial. + void guard_expr(exprt &dest) const; + + bool is_true() const + { + return bdd.is_true(); + } + + bool is_false() const + { + return bdd.is_false(); + } + + /// Transforms \p g1 into \c g1' such that `g1' & g2 => g1 => g1'` + /// and returns a reference to g1. + friend guard_bddt &operator-=(guard_bddt &g1, const guard_bddt &g2); + + friend guard_bddt &operator|=(guard_bddt &g1, const guard_bddt &g2); + + guard_bddt operator!() const + { + return guard_bddt(manager, bdd.bdd_not()); + } + +private: + bdd_exprt &manager; + bddt bdd; + + guard_bddt(bdd_exprt &manager, bddt bdd) + : manager(manager), bdd(std::move(bdd)) + { + } +}; + +#endif // CPROVER_ANALYSES_GUARD_BDD_H diff --git a/src/analyses/module_dependencies.txt b/src/analyses/module_dependencies.txt index 25dc8fec88e..d3eaee11766 100644 --- a/src/analyses/module_dependencies.txt +++ b/src/analyses/module_dependencies.txt @@ -2,4 +2,6 @@ analyses goto-programs langapi # should go away pointer-analysis +solvers/bdd +solvers/prop util diff --git a/src/goto-symex/CMakeLists.txt b/src/goto-symex/CMakeLists.txt index bc2cfd0368a..303a48feb99 100644 --- a/src/goto-symex/CMakeLists.txt +++ b/src/goto-symex/CMakeLists.txt @@ -3,4 +3,8 @@ add_library(goto-symex ${sources}) generic_includes(goto-symex) +if(CMAKE_USE_CUDD) + target_include_directories(goto-symex PUBLIC ${CUDD_INCLUDE}/cudd/) +endif() + target_link_libraries(goto-symex util) From de291f646628fd5121faea64bd7ad4c85cb8dba4 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 15 Jan 2019 14:54:29 +0000 Subject: [PATCH 10/18] Move guard implementation to guard_expr.h/cpp This is to clearly seperate the two implementations. The choice between the two will be made in guard.h --- src/analyses/Makefile | 2 +- src/analyses/guard.h | 57 +---------------- src/analyses/{guard.cpp => guard_expr.cpp} | 2 +- src/analyses/guard_expr.h | 72 ++++++++++++++++++++++ 4 files changed, 75 insertions(+), 58 deletions(-) rename src/analyses/{guard.cpp => guard_expr.cpp} (99%) create mode 100644 src/analyses/guard_expr.h diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 72f2066603a..3e52255c82e 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -12,8 +12,8 @@ SRC = ai.cpp \ global_may_alias.cpp \ goto_check.cpp \ goto_rw.cpp \ - guard.cpp \ guard_bdd.cpp \ + guard_expr.cpp \ interval_analysis.cpp \ interval_domain.cpp \ invariant_propagation.cpp \ diff --git a/src/analyses/guard.h b/src/analyses/guard.h index d625cc4e8ed..4a8370b5023 100644 --- a/src/analyses/guard.h +++ b/src/analyses/guard.h @@ -12,61 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #ifndef CPROVER_ANALYSES_GUARD_H #define CPROVER_ANALYSES_GUARD_H -#include - -#include - -/// This is unused by this implementation of guards, but can be used by other -/// implementations of the same interface. -struct guard_managert -{ -}; - -class guardt -{ -public: - /// Construct a BDD from an expression - /// The \c guard_managert parameter is not used, but we keep it for uniformity - /// with other implementations of guards which may use it. - explicit guardt(const exprt &e, guard_managert &) : expr(e) - { - } - - guardt &operator=(const guardt &other) - { - expr = other.expr; - return *this; - } - - void add(const exprt &expr); - - void append(const guardt &guard) - { - add(guard.as_expr()); - } - - exprt as_expr() const - { - return expr; - } - - void guard_expr(exprt &dest) const; - - bool is_true() const - { - return expr.is_true(); - } - - bool is_false() const - { - return expr.is_false(); - } - - friend guardt &operator-=(guardt &g1, const guardt &g2); - friend guardt &operator|=(guardt &g1, const guardt &g2); - -private: - exprt expr; -}; +#include "guard_expr.h" #endif // CPROVER_ANALYSES_GUARD_H diff --git a/src/analyses/guard.cpp b/src/analyses/guard_expr.cpp similarity index 99% rename from src/analyses/guard.cpp rename to src/analyses/guard_expr.cpp index 3dbf7cc1f72..5306c211f69 100644 --- a/src/analyses/guard.cpp +++ b/src/analyses/guard_expr.cpp @@ -9,7 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com /// \file /// Symbolic Execution -#include "guard.h" +#include "guard_expr.h" #include diff --git a/src/analyses/guard_expr.h b/src/analyses/guard_expr.h new file mode 100644 index 00000000000..de4d4321a11 --- /dev/null +++ b/src/analyses/guard_expr.h @@ -0,0 +1,72 @@ +/*******************************************************************\ + +Module: Guard Data Structure + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Guard Data Structure + +#ifndef CPROVER_ANALYSES_GUARD_EXPR_H +#define CPROVER_ANALYSES_GUARD_EXPR_H + +#include + +#include + +/// This is unused by this implementation of guards, but can be used by other +/// implementations of the same interface. +struct guard_managert +{ +}; + +class guardt +{ +public: + /// Construct a BDD from an expression + /// The \c guard_managert parameter is not used, but we keep it for uniformity + /// with other implementations of guards which may use it. + explicit guardt(const exprt &e, guard_managert &) : expr(e) + { + } + + guardt &operator=(const guardt &other) + { + expr = other.expr; + return *this; + } + + void add(const exprt &expr); + + void append(const guardt &guard) + { + add(guard.as_expr()); + } + + exprt as_expr() const + { + return expr; + } + + void guard_expr(exprt &dest) const; + + bool is_true() const + { + return expr.is_true(); + } + + bool is_false() const + { + return expr.is_false(); + } + + friend guardt &operator-=(guardt &g1, const guardt &g2); + friend guardt &operator|=(guardt &g1, const guardt &g2); + +private: + exprt expr; +}; + +#endif // CPROVER_ANALYSES_GUARD_EXPR_H From c8d8c48e4910f813e19eadbef05eea46fc14e29e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 15 Jan 2019 14:54:31 +0000 Subject: [PATCH 11/18] Rename class to guard_exprt 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. --- src/analyses/guard.h | 3 +++ src/analyses/guard_expr.cpp | 8 ++++---- src/analyses/guard_expr.h | 14 +++++++------- src/goto-symex/goto_symex.h | 1 - 4 files changed, 14 insertions(+), 12 deletions(-) diff --git a/src/analyses/guard.h b/src/analyses/guard.h index 4a8370b5023..70b17f77880 100644 --- a/src/analyses/guard.h +++ b/src/analyses/guard.h @@ -14,4 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "guard_expr.h" +using guard_managert = guard_expr_managert; +using guardt = guard_exprt; + #endif // CPROVER_ANALYSES_GUARD_H diff --git a/src/analyses/guard_expr.cpp b/src/analyses/guard_expr.cpp index 5306c211f69..411be7f33e7 100644 --- a/src/analyses/guard_expr.cpp +++ b/src/analyses/guard_expr.cpp @@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -void guardt::guard_expr(exprt &dest) const +void guard_exprt::guard_expr(exprt &dest) const { if(is_true()) { @@ -38,7 +38,7 @@ void guardt::guard_expr(exprt &dest) const } } -void guardt::add(const exprt &expr) +void guard_exprt::add(const exprt &expr) { PRECONDITION(expr.type().id() == ID_bool); @@ -64,7 +64,7 @@ void guardt::add(const exprt &expr) op.push_back(expr); } -guardt &operator-=(guardt &g1, const guardt &g2) +guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2) { if(g1.expr.id() != ID_and || g2.expr.id() != ID_and) return g1; @@ -91,7 +91,7 @@ guardt &operator-=(guardt &g1, const guardt &g2) return g1; } -guardt &operator|=(guardt &g1, const guardt &g2) +guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2) { if(g2.is_false() || g1.is_true()) return g1; diff --git a/src/analyses/guard_expr.h b/src/analyses/guard_expr.h index de4d4321a11..63932625d5e 100644 --- a/src/analyses/guard_expr.h +++ b/src/analyses/guard_expr.h @@ -18,21 +18,21 @@ Author: Daniel Kroening, kroening@kroening.com /// This is unused by this implementation of guards, but can be used by other /// implementations of the same interface. -struct guard_managert +struct guard_expr_managert { }; -class guardt +class guard_exprt { public: /// Construct a BDD from an expression /// The \c guard_managert parameter is not used, but we keep it for uniformity /// with other implementations of guards which may use it. - explicit guardt(const exprt &e, guard_managert &) : expr(e) + explicit guard_exprt(const exprt &e, guard_expr_managert &) : expr(e) { } - guardt &operator=(const guardt &other) + guard_exprt &operator=(const guard_exprt &other) { expr = other.expr; return *this; @@ -40,7 +40,7 @@ class guardt void add(const exprt &expr); - void append(const guardt &guard) + void append(const guard_exprt &guard) { add(guard.as_expr()); } @@ -62,8 +62,8 @@ class guardt return expr.is_false(); } - friend guardt &operator-=(guardt &g1, const guardt &g2); - friend guardt &operator|=(guardt &g1, const guardt &g2); + friend guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2); + friend guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2); private: exprt expr; diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 695fbd698af..72e6a8581e7 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -27,7 +27,6 @@ class code_assignt; class code_function_callt; class exprt; class goto_symex_statet; -class guardt; class if_exprt; class index_exprt; class symbol_exprt; From eba0713b2dc3e69adbf8ab073116a8bcb172fcf9 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 15 Jan 2019 14:54:33 +0000 Subject: [PATCH 12/18] Switch between guard bdd and guard expr Depending on the BDD_GUARDS flag, we will use the expr implementation or the BDD implementation. --- src/analyses/guard.h | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/analyses/guard.h b/src/analyses/guard.h index 70b17f77880..950a65b58bc 100644 --- a/src/analyses/guard.h +++ b/src/analyses/guard.h @@ -12,9 +12,20 @@ Author: Daniel Kroening, kroening@kroening.com #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; + +#else + #include "guard_expr.h" using guard_managert = guard_expr_managert; using guardt = guard_exprt; +#endif // BDD_GUARDS + #endif // CPROVER_ANALYSES_GUARD_H From fccd412fead8aafb946807153e296a52b00d46d5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 13 Feb 2019 10:10:41 +0000 Subject: [PATCH 13/18] Document the BDD_GUARDS compilation flag This adds instruction to COMPILING.md so that people interested in performances can find about it, and try it. --- COMPILING.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/COMPILING.md b/COMPILING.md index 6ed73f03989..6eff98f9ff4 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -310,3 +310,22 @@ If compiling with cmake: ``` cmake --build build ``` + +## Use BDDs for guards + +There are two implementation for symex guards. The default one uses the +internal representation of expression. The other one uses BDDs and +though experimental, it is expected to have better performance, +in particular when used in conjunction with CUDD. + +To use the BDD implementation of guards, add the `BDD_GUARDS` +compilation flag: + * If compiling with make: + ``` + make -C src CXXFLAGS="-O2 -DBDD_GUARDS" + ``` + * If compiling with CMake: + ``` + cmake -H. -Bbuild -DCMAKE_CXX_FLAGS="-DBDD_GUARDS" + ``` + and then `cmake --build build` From ff79e868d2a65d4089d5a963bb158cb7ed754d81 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 16 Jan 2019 14:03:16 +0000 Subject: [PATCH 14/18] Add is_always_simplified field in guard implementations 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. --- src/analyses/guard_bdd.h | 5 +++++ src/analyses/guard_expr.h | 5 +++++ 2 files changed, 10 insertions(+) diff --git a/src/analyses/guard_bdd.h b/src/analyses/guard_bdd.h index 33a8ae4438d..e6bc16d0dbb 100644 --- a/src/analyses/guard_bdd.h +++ b/src/analyses/guard_bdd.h @@ -35,6 +35,11 @@ class guard_bddt guard_bddt &append(const guard_bddt &guard); exprt as_expr() const; + /// BDDs are always in a simplified form and thus no further simplification + /// is required after calls to \ref as_expr(). + /// This can vary according to the guard implementation. + static constexpr bool is_always_simplified = true; + /// Assign dest to `guard => dest` unless guard or dest are trivial. void guard_expr(exprt &dest) const; diff --git a/src/analyses/guard_expr.h b/src/analyses/guard_expr.h index 63932625d5e..d7c814ca556 100644 --- a/src/analyses/guard_expr.h +++ b/src/analyses/guard_expr.h @@ -50,6 +50,11 @@ class guard_exprt return expr; } + /// The result of \ref as_expr is not always in a simplified form + /// and may requires some simplification. + /// This can vary according to the guard implementation. + static constexpr bool is_always_simplified = false; + void guard_expr(exprt &dest) const; bool is_true() const From f4afbd18f95bacd79fb10d40e134950ada71ad64 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 21 Feb 2019 07:32:39 +0000 Subject: [PATCH 15/18] Enable BDD_GUARDS in one of the travis steps We add the BDD_GUARDS flags in the travis step which is compiling with CUDD to test that the bdd_guard implementation. --- .travis.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index c62ee5db9ed..ffbfb288b96 100644 --- a/.travis.yml +++ b/.travis.yml @@ -201,7 +201,7 @@ jobs: - cmake --build build -- -j4 script: (cd build; bin/unit "[core][irept]") - # cmake build using g++-7, enable CMAKE_USE_CUDD + # cmake build using g++-7, enable CMAKE_USE_CUDD and BDD_GUARDS - stage: Test different OS/CXX/Flags os: linux sudo: false @@ -223,7 +223,7 @@ jobs: install: - ccache -z - ccache --max-size=1G - - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' + - cmake -H. -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS" - git submodule update --init --recursive - cmake --build build -- -j4 script: (cd build; ctest -V -L CORE -j2) From a50678cad9df93756c19b6c69a83f52e0c47a84c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 27 Feb 2019 12:08:57 +0000 Subject: [PATCH 16/18] Deactivate a test which takes too long with BDDs 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. --- jbmc/regression/jbmc/CMakeLists.txt | 21 +++++++++++++------ jbmc/regression/jbmc/Makefile | 8 +++++++ jbmc/regression/jbmc/class-literals/test.desc | 7 ++++++- 3 files changed, 29 insertions(+), 7 deletions(-) diff --git a/jbmc/regression/jbmc/CMakeLists.txt b/jbmc/regression/jbmc/CMakeLists.txt index 561fe5ab0c7..a05181109f5 100644 --- a/jbmc/regression/jbmc/CMakeLists.txt +++ b/jbmc/regression/jbmc/CMakeLists.txt @@ -2,9 +2,18 @@ add_test_pl_tests( "$ --validate-goto-model --validate-ssa-equation" ) -add_test_pl_profile( - "jbmc-symex-driven-lazy-loading" - "$ --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" - "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading" - "CORE" -) +if(DEFINED BDD_GUARDS) + add_test_pl_profile( + "jbmc-symex-driven-lazy-loading" + "$ --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" + "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading" + "CORE" + ) +else() + add_test_pl_profile( + "jbmc-symex-driven-lazy-loading" + "$ --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" + "-C;-X;symex-driven-lazy-loading-expected-failure;-X;bdd-expected-timeout;-s;symex-driven-loading" + "CORE" + ) +endif() diff --git a/jbmc/regression/jbmc/Makefile b/jbmc/regression/jbmc/Makefile index e6541f77df2..aaf7efdf539 100644 --- a/jbmc/regression/jbmc/Makefile +++ b/jbmc/regression/jbmc/Makefile @@ -4,11 +4,19 @@ include ../../src/config.inc test: @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),) @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading +else + @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading +endif tests.log: ../$(CPROVER_DIR)/regression/test.pl @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation" +ifeq ($(filter %DBDD_GUARDS, $(CXXFLAGS)),) @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -s symex-driven-loading +else + @../$(CPROVER_DIR)/regression/test.pl -e -p -c "../../../src/jbmc/jbmc --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -X bdd-expected-timeout -s symex-driven-loading +endif show: @for dir in *; do \ diff --git a/jbmc/regression/jbmc/class-literals/test.desc b/jbmc/regression/jbmc/class-literals/test.desc index a39e4029a74..47ca0a9496b 100644 --- a/jbmc/regression/jbmc/class-literals/test.desc +++ b/jbmc/regression/jbmc/class-literals/test.desc @@ -1,4 +1,4 @@ -CORE +CORE bdd-expected-timeout Test.class --function Test.main ^EXIT=0$ @@ -6,3 +6,8 @@ Test.class ^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. From 7503ac60bd58ecc18b220ea0a994f449922b20af Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 1 Mar 2019 16:43:42 +0000 Subject: [PATCH 17/18] Make guard_expr return a value This avoids having an argument that is both input and output and makes using this function nicer. --- src/analyses/guard_bdd.cpp | 12 +++++------- src/analyses/guard_bdd.h | 5 +++-- src/analyses/guard_expr.cpp | 10 +++++----- src/analyses/guard_expr.h | 4 +++- src/goto-symex/symex_main.cpp | 6 ++---- 5 files changed, 18 insertions(+), 19 deletions(-) diff --git a/src/analyses/guard_bdd.cpp b/src/analyses/guard_bdd.cpp index 1ded532f190..c73ee1169c1 100644 --- a/src/analyses/guard_bdd.cpp +++ b/src/analyses/guard_bdd.cpp @@ -44,24 +44,22 @@ guard_bddt &guard_bddt::operator=(guard_bddt &&other) return *this; } -void guard_bddt::guard_expr(exprt &dest) const +exprt guard_bddt::guard_expr(exprt expr) const { if(is_true()) { // do nothing + return expr; } else { - if(dest.is_false()) + if(expr.is_false()) { - dest = boolean_negate(as_expr()); + return boolean_negate(as_expr()); } else { - implies_exprt tmp; - tmp.op0() = as_expr(); - tmp.op1().swap(dest); - dest.swap(tmp); + return implies_exprt{as_expr(), expr}; } } } diff --git a/src/analyses/guard_bdd.h b/src/analyses/guard_bdd.h index e6bc16d0dbb..c522b242cdd 100644 --- a/src/analyses/guard_bdd.h +++ b/src/analyses/guard_bdd.h @@ -40,8 +40,9 @@ class guard_bddt /// This can vary according to the guard implementation. static constexpr bool is_always_simplified = true; - /// Assign dest to `guard => dest` unless guard or dest are trivial. - void guard_expr(exprt &dest) const; + /// Return `guard => dest` or a simplified variant thereof if either guard or + /// dest are trivial. + exprt guard_expr(exprt expr) const; bool is_true() const { diff --git a/src/analyses/guard_expr.cpp b/src/analyses/guard_expr.cpp index 411be7f33e7..ef48e8fde13 100644 --- a/src/analyses/guard_expr.cpp +++ b/src/analyses/guard_expr.cpp @@ -18,22 +18,22 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -void guard_exprt::guard_expr(exprt &dest) const +exprt guard_exprt::guard_expr(exprt expr) const { if(is_true()) { // do nothing + return expr; } else { - if(dest.is_false()) + if(expr.is_false()) { - dest = boolean_negate(as_expr()); + return boolean_negate(as_expr()); } else { - implies_exprt tmp(as_expr(), dest); - dest.swap(tmp); + return implies_exprt{as_expr(), expr}; } } } diff --git a/src/analyses/guard_expr.h b/src/analyses/guard_expr.h index d7c814ca556..774659821cf 100644 --- a/src/analyses/guard_expr.h +++ b/src/analyses/guard_expr.h @@ -55,7 +55,9 @@ class guard_exprt /// This can vary according to the guard implementation. static constexpr bool is_always_simplified = false; - void guard_expr(exprt &dest) const; + /// Return `guard => dest` or a simplified variant thereof if either guard or + /// dest are trivial. + exprt guard_expr(exprt expr) const; bool is_true() const { diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index debf8f8f9f9..159d127be30 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -116,8 +116,7 @@ void goto_symext::vcc( if(condition.is_true()) return; - exprt guarded_condition = condition; - state.guard.guard_expr(guarded_condition); + const exprt guarded_condition = state.guard.guard_expr(condition); state.remaining_vccs++; target.assertion(state.guard.as_expr(), guarded_condition, msg, state.source); @@ -146,8 +145,7 @@ void goto_symext::symex_assume_l2(statet &state, const exprt &cond) if(state.threads.size()==1) { - exprt tmp = rewritten_cond; - state.guard.guard_expr(tmp); + exprt tmp = state.guard.guard_expr(rewritten_cond); target.assumption(state.guard.as_expr(), tmp, state.source); } // symex_target_equationt::convert_assertions would fail to From 22ed54bd4a508e50c1109b5298540813d82f3965 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 15 Jan 2019 14:54:39 +0000 Subject: [PATCH 18/18] Apply clang-format suggestions No functional change --- .../accelerate/enumerating_loop_acceleration.h | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) diff --git a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h index 4fd38cbd35f..ced470f3bd5 100644 --- a/src/goto-instrument/accelerate/enumerating_loop_acceleration.h +++ b/src/goto-instrument/accelerate/enumerating_loop_acceleration.h @@ -50,15 +50,14 @@ class enumerating_loop_accelerationt goto_functions, guard_manager), path_limit(_path_limit), - path_enumerator( - util_make_unique( - message_handler, - symbol_table, - goto_functions, - goto_program, - loop, - loop_header, - guard_manager)) + path_enumerator(util_make_unique( + message_handler, + symbol_table, + goto_functions, + goto_program, + loop, + loop_header, + guard_manager)) { }