From dc799e00ae07cf55ebc679b2365b45d2d67006a1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:10:16 +0000 Subject: [PATCH 01/16] Assert replaced by unreachable --- src/solvers/prop/prop_conv.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 1469b25e040..9bbd52fc0ca 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -22,18 +22,18 @@ Author: Daniel Kroening, kroening@kroening.com /// determine whether a variable is in the final conflict bool prop_convt::is_in_conflict(literalt l) const { - assert(false); + UNREACHABLE; return false; } void prop_convt::set_assumptions(const bvt &) { - assert(false); + UNREACHABLE; } void prop_convt::set_frozen(const literalt) { - assert(false); + UNREACHABLE; } void prop_convt::set_frozen(const bvt &bv) From 8eb20f6cf933ab522b34c96caca04ee4e5fa8292 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:10:45 +0000 Subject: [PATCH 02/16] Use ranged for --- src/solvers/prop/prop_conv.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 9bbd52fc0ca..80097131f10 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -38,9 +38,9 @@ void prop_convt::set_frozen(const literalt) void prop_convt::set_frozen(const bvt &bv) { - for(unsigned i=0; i Date: Wed, 7 Feb 2018 14:42:33 +0000 Subject: [PATCH 03/16] Renaming `it` to symbol it is not an iterator in that case --- src/solvers/prop/prop_conv.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 80097131f10..408890abee2 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -547,6 +547,6 @@ exprt prop_conv_solvert::get(const exprt &expr) const void prop_conv_solvert::print_assignment(std::ostream &out) const { - for(const auto &it : symbols) - out << it.first << " = " << prop.l_get(it.second) << "\n"; + for(const auto &symbol : symbols) + out << symbol.first << " = " << prop.l_get(symbol.second) << '\n'; } From 990f33eaca5a0595b7fbb3a5fd44fabc4fdfeef0 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:43:27 +0000 Subject: [PATCH 04/16] Initialize at declaration instead of construction Should another constructor be added in the future (copy, move, default, overload of existing constructor), one set of default arguments will already be present. --- src/solvers/prop/prop_conv.h | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h index 816b7481a0e..bec28655cba 100644 --- a/src/solvers/prop/prop_conv.h +++ b/src/solvers/prop/prop_conv.h @@ -72,10 +72,6 @@ class prop_conv_solvert:public prop_convt public: prop_conv_solvert(const namespacet &_ns, propt &_prop): prop_convt(_ns), - use_cache(true), - equality_propagation(true), - freeze_all(false), - post_processing_done(false), prop(_prop) { } virtual ~prop_conv_solvert() { } @@ -106,9 +102,9 @@ class prop_conv_solvert:public prop_convt // get literal for expression, if available virtual bool literal(const exprt &expr, literalt &literal) const; - bool use_cache; - bool equality_propagation; - bool freeze_all; // freezing variables (for incremental solving) + bool use_cache = true; + bool equality_propagation = true; + bool freeze_all = false; // freezing variables (for incremental solving) virtual void clear_cache() { cache.clear();} @@ -126,7 +122,7 @@ class prop_conv_solvert:public prop_convt protected: virtual void post_process(); - bool post_processing_done; + bool post_processing_done = false; // get a _boolean_ value from counterexample if not valid virtual bool get_bool(const exprt &expr, tvt &value) const; From 7db44fcf717283ed6626fa89f417ec634dafe964 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:44:50 +0000 Subject: [PATCH 05/16] Remove virtual keyword where not needed No need to declare method virtual when it is already marked override. --- src/solvers/flattening/boolbv.h | 2 +- src/solvers/prop/prop_conv.h | 32 +++++++++++++++++++------------- 2 files changed, 20 insertions(+), 14 deletions(-) diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 08a39d05c80..906fd0666d8 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -99,7 +99,7 @@ class boolbvt:public arrayst boolbv_mapt map; // overloading - virtual literalt convert_rest(const exprt &expr) override; + literalt convert_rest(const exprt &expr) override; virtual bool boolbv_set_equality_to_true(const equal_exprt &expr); // NOLINTNEXTLINE(readability/identifiers) diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h index bec28655cba..261771040a6 100644 --- a/src/solvers/prop/prop_conv.h +++ b/src/solvers/prop/prop_conv.h @@ -74,29 +74,35 @@ class prop_conv_solvert:public prop_convt prop_convt(_ns), prop(_prop) { } - virtual ~prop_conv_solvert() { } + virtual ~prop_conv_solvert() = default; // overloading from decision_proceduret - virtual void set_to(const exprt &expr, bool value) override; - virtual decision_proceduret::resultt dec_solve() override; - virtual void print_assignment(std::ostream &out) const override; - virtual std::string decision_procedure_text() const override + void set_to(const exprt &expr, bool value) override; + decision_proceduret::resultt dec_solve() override; + void print_assignment(std::ostream &out) const override; + std::string decision_procedure_text() const override { return "propositional reduction"; } - virtual exprt get(const exprt &expr) const override; + exprt get(const exprt &expr) const override; // overloading from prop_convt using prop_convt::set_frozen; virtual tvt l_get(literalt a) const override { return prop.l_get(a); } - virtual void set_frozen(literalt a) override { prop.set_frozen(a); } - virtual void set_assumptions(const bvt &_assumptions) override + void set_frozen(literalt a) override + { + prop.set_frozen(a); + } + void set_assumptions(const bvt &_assumptions) override { prop.set_assumptions(_assumptions); } - virtual bool has_set_assumptions() const override + bool has_set_assumptions() const override { return prop.has_set_assumptions(); } - virtual void set_all_frozen() override { freeze_all = true; } - virtual literalt convert(const exprt &expr) override; - virtual bool is_in_conflict(literalt l) const override + void set_all_frozen() override + { + freeze_all = true; + } + literalt convert(const exprt &expr) override; + bool is_in_conflict(literalt l) const override { return prop.is_in_conflict(l); } - virtual bool has_is_in_conflict() const override + bool has_is_in_conflict() const override { return prop.has_is_in_conflict(); } // get literal for expression, if available From a905a07cafe3b2002fdba378d2670a4bde62842c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:46:08 +0000 Subject: [PATCH 06/16] Replace throws by invariant or preconditions --- src/solvers/prop/prop_conv.cpp | 29 +++++++---------------------- 1 file changed, 7 insertions(+), 22 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 408890abee2..f2ffd4596b7 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -208,13 +208,7 @@ literalt prop_conv_solvert::convert(const exprt &expr) literalt prop_conv_solvert::convert_bool(const exprt &expr) { - if(expr.type().id()!=ID_bool) - { - std::string msg="prop_convt::convert_bool got " - "non-boolean expression: "; - msg+=expr.pretty(); - throw msg; - } + PRECONDITION(expr.type().id() == ID_bool); const exprt::operandst &op=expr.operands(); @@ -280,8 +274,9 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr) else if(expr.id()==ID_or || expr.id()==ID_and || expr.id()==ID_xor || expr.id()==ID_nor || expr.id()==ID_nand) { - if(op.empty()) - throw "operator `"+expr.id_string()+"' takes at least one operand"; + INVARIANT( + !op.empty(), + "operator `" + expr.id_string() + "' takes at least one operand"); bvt bv; @@ -304,16 +299,12 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr) } else if(expr.id()==ID_not) { - if(op.size()!=1) - throw "not takes one operand"; - + INVARIANT(op.size() == 1, "not takes one operand"); return !convert(op.front()); } else if(expr.id()==ID_equal || expr.id()==ID_notequal) { - if(op.size()!=2) - throw "equality takes two operands"; - + INVARIANT(op.size() == 2, "equality takes two operands"); bool equal=(expr.id()==ID_equal); if(op[0].type().id()==ID_bool && @@ -387,13 +378,7 @@ bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr) void prop_conv_solvert::set_to(const exprt &expr, bool value) { - if(expr.type().id()!=ID_bool) - { - std::string msg="prop_convt::set_to got " - "non-boolean expression: "; - msg+=expr.pretty(); - throw msg; - } + PRECONDITION(expr.type().id() == ID_bool); bool boolean=true; From 9179571839f37caa739191376b08cfd75ff71ece Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:47:24 +0000 Subject: [PATCH 07/16] Remove useless includes --- src/solvers/prop/prop_conv.cpp | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index f2ffd4596b7..02b806efd1d 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -8,17 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "prop_conv.h" -#include -#include -#include - -#include -#include -#include - -#include "prop.h" -#include "literal_expr.h" - /// determine whether a variable is in the final conflict bool prop_convt::is_in_conflict(literalt l) const { From ba13c94a4544d0249ccac2c4739a04da15f8b491 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:54:55 +0000 Subject: [PATCH 08/16] Use auto for iterator types --- src/solvers/prop/prop_conv.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 02b806efd1d..1550e1d57b9 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -54,7 +54,7 @@ bool prop_conv_solvert::literal(const exprt &expr, literalt &dest) const literalt prop_conv_solvert::get_literal(const irep_idt &identifier) { - std::pair result= + auto result = symbols.insert(std::pair(identifier, literalt())); if(!result.second) @@ -172,10 +172,9 @@ literalt prop_conv_solvert::convert(const exprt &expr) prop.set_frozen(literal); return literal; } - // check cache first - std::pair result= - cache.insert(std::pair(expr, literalt())); + // check cache first + auto result = cache.insert({expr, literalt()}); if(!result.second) return result.first->second; From a0500f6d6303b2e297c27f618d18bcdcaf2b039e Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:56:11 +0000 Subject: [PATCH 09/16] Use standard algorithm for finding an element --- src/solvers/prop/prop_conv.cpp | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 1550e1d57b9..4447ca58152 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -7,6 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ #include "prop_conv.h" +#include /// determine whether a variable is in the final conflict bool prop_convt::is_in_conflict(literalt l) const @@ -368,16 +369,12 @@ void prop_conv_solvert::set_to(const exprt &expr, bool value) { PRECONDITION(expr.type().id() == ID_bool); - bool boolean=true; + const bool has_only_boolean_operands = std::all_of( + expr.operands().begin(), + expr.operands().end(), + [](const exprt &expr) { return expr.type().id() == ID_bool; }); - forall_operands(it, expr) - if(it->type().id()!=ID_bool) - { - boolean=false; - break; - } - - if(boolean) + if(has_only_boolean_operands) { if(expr.id()==ID_not) { From 13e87a9a4caf7c9202fda8a3ceb28f704fc1477f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:56:54 +0000 Subject: [PATCH 10/16] Simplify dec_solve Result is not modified, and the last return is never reached. --- src/solvers/prop/prop_conv.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 4447ca58152..80d107cc51f 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -477,16 +477,12 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve() statistics() << "Solving with " << prop.solver_text() << eom; - propt::resultt result=prop.prop_solve(); - - switch(result) + switch(prop.prop_solve()) { case propt::resultt::P_SATISFIABLE: return resultt::D_SATISFIABLE; case propt::resultt::P_UNSATISFIABLE: return resultt::D_UNSATISFIABLE; default: return resultt::D_ERROR; } - - return resultt::D_ERROR; } exprt prop_conv_solvert::get(const exprt &expr) const From 4987f3ab559159198b17a9a216cecb67ce76694b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:57:33 +0000 Subject: [PATCH 11/16] Remove useless comments The name of the functions already explain what we are doing. --- src/solvers/prop/prop_conv.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 80d107cc51f..4c87e18dc06 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -61,10 +61,7 @@ literalt prop_conv_solvert::get_literal(const irep_idt &identifier) if(!result.second) return result.first->second; - // produce new variable literalt literal=prop.new_variable(); - - // set the name of the new variable prop.set_variable_name(literal, id2string(identifier)); // insert From 5724a3514bce28baaa48ac5d391796a3d9d6f43c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:58:08 +0000 Subject: [PATCH 12/16] Simplify loop in prop_conv::get The iterator is not used as such and does not need to be exposed. --- src/solvers/prop/prop_conv.cpp | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 4c87e18dc06..578483f562a 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -497,14 +497,12 @@ exprt prop_conv_solvert::get(const exprt &expr) const } } - exprt tmp=expr; - - Forall_operands(it, tmp) + exprt tmp = expr; + for(auto &op : tmp.operands()) { - exprt tmp_op=get(*it); - it->swap(tmp_op); + exprt tmp_op = get(op); + op.swap(tmp_op); } - return tmp; } From b18109f4068c36c8659fa74df330360ff0a73982 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 15:19:23 +0000 Subject: [PATCH 13/16] Make make_(free_)bv_expr return exprt --- src/cbmc/bv_cbmc.cpp | 17 +++-------------- src/solvers/flattening/boolbv.cpp | 30 ++++++++++-------------------- src/solvers/flattening/boolbv.h | 4 ++-- 3 files changed, 15 insertions(+), 36 deletions(-) diff --git a/src/cbmc/bv_cbmc.cpp b/src/cbmc/bv_cbmc.cpp index 06a32d52686..019982f6fd7 100644 --- a/src/cbmc/bv_cbmc.cpp +++ b/src/cbmc/bv_cbmc.cpp @@ -20,13 +20,11 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr) throw 0; } - exprt new_cycle; const exprt &old_cycle=expr.op0(); const exprt &cycle_var=expr.op1(); const exprt &bound=expr.op2(); const exprt &predicate=expr.op3(); - - make_free_bv_expr(expr.type(), new_cycle); + const exprt new_cycle = make_free_bv_expr(expr.type()); mp_integer bound_value; if(to_integer(bound, bound_value)) @@ -98,18 +96,9 @@ bvt bv_cbmct::convert_waitfor(const exprt &expr) bvt bv_cbmct::convert_waitfor_symbol(const exprt &expr) { - if(expr.operands().size()!=1) - { - error().source_location=expr.find_source_location(); - error() << "waitfor_symbol expected to have one operand" << eom; - throw 0; - } - - exprt result; + PRECONDITION(expr.operands().size() == 1); const exprt &bound=expr.op0(); - - make_free_bv_expr(expr.type(), result); - + const exprt result = make_free_bv_expr(expr.type()); // constraint: result<=bound set_to_true(binary_relation_exprt(result, ID_le, bound)); diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 12571a7c01d..75894369ce8 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -650,35 +650,25 @@ void boolbvt::set_to(const exprt &expr, bool value) return SUB::set_to(expr, value); } -void boolbvt::make_bv_expr(const typet &type, const bvt &bv, exprt &dest) +exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv) { - dest=exprt(ID_bv_literals, type); + exprt dest(ID_bv_literals, type); irept::subt &bv_sub=dest.add(ID_bv).get_sub(); - bv_sub.resize(bv.size()); for(std::size_t i=0; i Date: Wed, 7 Feb 2018 15:38:06 +0000 Subject: [PATCH 14/16] Simplify boolbvt::set_to --- src/solvers/flattening/boolbv.cpp | 21 +++++---------------- 1 file changed, 5 insertions(+), 16 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 75894369ce8..8d6f98339e7 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -631,23 +631,12 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr) void boolbvt::set_to(const exprt &expr, bool value) { - if(expr.type().id()!=ID_bool) - { - error() << "boolbvt::set_to got non-boolean operand: " - << expr.pretty() << eom; - throw 0; - } - - if(value) - { - if(expr.id()==ID_equal) - { - if(!boolbv_set_equality_to_true(to_equal_expr(expr))) - return; - } - } + PRECONDITION(expr.type().id() == ID_bool); - return SUB::set_to(expr, value); + const auto equal_expr = expr_try_dynamic_cast(expr); + if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr)) + return; + SUB::set_to(expr, value); } exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv) From 2d8be0669a622ea2a6cbded02274357f8d5ded0a Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 15:39:37 +0000 Subject: [PATCH 15/16] Rename `it` to pair in boolbvt::print_assignment The variable represents a pair and not an iterator --- src/solvers/flattening/boolbv.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 8d6f98339e7..a61e50a0f33 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -687,12 +687,8 @@ bool boolbvt::is_unbounded_array(const typet &type) const void boolbvt::print_assignment(std::ostream &out) const { arrayst::print_assignment(out); - - for(const auto &it : map.mapping) - { - out << it.first << "=" - << it.second.get_value(prop) << '\n'; - } + for(const auto &pair : map.mapping) + out << pair.first << "=" << pair.second.get_value(prop) << '\n'; } void boolbvt::build_offset_map(const struct_typet &src, offset_mapt &dest) From 4147243eac1d5c680aa12d2208a380f5ae040a31 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 6 Apr 2018 14:44:44 +0100 Subject: [PATCH 16/16] Change set_variable_name API to consume irep_idt --- src/solvers/prop/prop.h | 2 +- src/solvers/prop/prop_conv.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h index 7ac5d88848e..cef918c0459 100644 --- a/src/solvers/prop/prop.h +++ b/src/solvers/prop/prop.h @@ -87,7 +87,7 @@ class propt:public messaget, public prop_assignmentt // variables virtual literalt new_variable()=0; - virtual void set_variable_name(literalt a, const std::string &name) { } + virtual void set_variable_name(literalt a, const irep_idt &name) { } virtual size_t no_variables() const=0; bvt new_variables(std::size_t width); diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 578483f562a..0e929871f53 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -62,7 +62,7 @@ literalt prop_conv_solvert::get_literal(const irep_idt &identifier) return result.first->second; literalt literal=prop.new_variable(); - prop.set_variable_name(literal, id2string(identifier)); + prop.set_variable_name(literal, identifier); // insert result.first->second=literal;