From 79cb900649f3caf2dadbb569f0747d11ed32873a Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:11:34 +0000 Subject: [PATCH 01/10] Make literal return an optional This is clearer than a boolean signaling an error --- src/solvers/flattening/boolbv.cpp | 19 ++++++++----------- src/solvers/flattening/boolbv.h | 5 +---- src/solvers/prop/prop_conv.cpp | 25 ++++++++----------------- src/solvers/prop/prop_conv.h | 2 +- 4 files changed, 18 insertions(+), 33 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 219e372afcf..f5adfb21da6 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -29,15 +29,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -bool boolbvt::literal( - const exprt &expr, - const std::size_t bit, - literalt &dest) const +optionalt +boolbvt::literal(const exprt &expr, const std::size_t bit) const { if(expr.type().id()==ID_bool) { assert(bit==0); - return prop_conv_solvert::literal(expr, dest); + return prop_conv_solvert::literal(expr); } else { @@ -50,16 +48,15 @@ bool boolbvt::literal( map.mapping.find(identifier); if(it_m==map.mapping.end()) - return true; + return {}; const boolbv_mapt::map_entryt &map_entry=it_m->second; assert(bittype(); if(it->get_name()==component_name) - return literal(expr.op0(), bit+offset, dest); + return literal(expr.op0(), bit + offset); std::size_t element_width=boolbv_width(subtype); diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 429a5aa4b37..0e77b6d7cc5 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -65,10 +65,7 @@ class boolbvt:public arrayst } // get literals for variables/expressions, if available - virtual bool literal( - const exprt &expr, - std::size_t bit, - literalt &literal) const; + virtual optionalt literal(const exprt &expr, std::size_t bit) const; using arrayst::literal; diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 0e929871f53..a1db2a02631 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -33,24 +33,15 @@ void prop_convt::set_frozen(const bvt &bv) set_frozen(bit); } -bool prop_conv_solvert::literal(const exprt &expr, literalt &dest) const +optionalt prop_conv_solvert::literal(const exprt &expr) const { - assert(expr.type().id()==ID_bool); - - if(expr.id()==ID_symbol) - { - const irep_idt &identifier= - to_symbol_expr(expr).get_identifier(); - - symbolst::const_iterator result=symbols.find(identifier); - - if(result==symbols.end()) - return true; - dest=result->second; - return false; - } - - throw "found no literal for expression"; + PRECONDITION(expr.type().id() == ID_bool); + PRECONDITION(expr.id() == ID_symbol); + const irep_idt &identifier = to_symbol_expr(expr).get_identifier(); + auto result = symbols.find(identifier); + if(result == symbols.end()) + return {}; + return result->second; } literalt prop_conv_solvert::get_literal(const irep_idt &identifier) diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h index 261771040a6..d850df3bea5 100644 --- a/src/solvers/prop/prop_conv.h +++ b/src/solvers/prop/prop_conv.h @@ -106,7 +106,7 @@ class prop_conv_solvert:public prop_convt { return prop.has_is_in_conflict(); } // get literal for expression, if available - virtual bool literal(const exprt &expr, literalt &literal) const; + virtual optionalt literal(const exprt &expr) const; bool use_cache = true; bool equality_propagation = true; From fd7af7204e7edd1e4c5cc9662d9d494fe30e403d Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:21:13 +0000 Subject: [PATCH 02/10] Make get_bool return a optional --- src/solvers/prop/prop_conv.cpp | 98 +++++++++++++--------------------- src/solvers/prop/prop_conv.h | 2 +- 2 files changed, 37 insertions(+), 63 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index a1db2a02631..f5a81edfbef 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -62,43 +62,27 @@ literalt prop_conv_solvert::get_literal(const irep_idt &identifier) } /// get a boolean value from counter example if not valid -bool prop_conv_solvert::get_bool(const exprt &expr, tvt &value) const +optionalt prop_conv_solvert::get_bool(const exprt &expr) const { - // trivial cases - if(expr.is_true()) + return tvt(true); + if(expr.is_false()) + return tvt(false); + if(expr.id() == ID_symbol) { - value=tvt(true); - return false; - } - else if(expr.is_false()) - { - value=tvt(false); - return false; - } - else if(expr.id()==ID_symbol) - { - symbolst::const_iterator result= - symbols.find(to_symbol_expr(expr).get_identifier()); - + const auto result = symbols.find(to_symbol_expr(expr).get_identifier()); if(result==symbols.end()) - return true; - - value=prop.l_get(result->second); - return false; + return {}; + return prop.l_get(result->second); } - - // sub-expressions - if(expr.id()==ID_not) { if(expr.type().id()==ID_bool && expr.operands().size()==1) { - if(get_bool(expr.op0(), value)) - return true; - value=!value; - return false; + if(auto result = get_bool(expr.op0())) + return !*result; + return {}; } } else if(expr.id()==ID_and || expr.id()==ID_or) @@ -106,48 +90,35 @@ bool prop_conv_solvert::get_bool(const exprt &expr, tvt &value) const if(expr.type().id()==ID_bool && expr.operands().size()>=1) { - value=tvt(expr.id()==ID_and); + auto value = tvt(expr.id() == ID_and); forall_operands(it, expr) { - tvt tmp; - if(get_bool(*it, tmp)) - return true; - + auto tmp = get_bool(*it); + if(!tmp) + return {}; if(expr.id()==ID_and) { - if(tmp.is_false()) - { - value=tvt(false); - return false; - } - - value=value && tmp; + if(tmp->is_false()) + return tvt(false); + value = value && *tmp; } else // or { - if(tmp.is_true()) - { - value=tvt(true); - return false; - } - - value=value || tmp; + if(tmp->is_true()) + return tvt(true); + value = value || *tmp; } } - - return false; + return value; } } // check cache - - cachet::const_iterator cache_result=cache.find(expr); + const auto cache_result = cache.find(expr); if(cache_result==cache.end()) - return true; - - value=prop.l_get(cache_result->second); - return false; + return {}; + return prop.l_get(cache_result->second); } literalt prop_conv_solvert::convert(const exprt &expr) @@ -475,16 +446,19 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve() exprt prop_conv_solvert::get(const exprt &expr) const { - tvt value; - - if(expr.type().id()==ID_bool && - !get_bool(expr, value)) + if(expr.type().id() == ID_bool) { - switch(value.get_value()) + if(const auto value = get_bool(expr)) { - case tvt::tv_enumt::TV_TRUE: return true_exprt(); - case tvt::tv_enumt::TV_FALSE: return false_exprt(); - case tvt::tv_enumt::TV_UNKNOWN: return false_exprt(); // default + switch(value->get_value()) + { + case tvt::tv_enumt::TV_TRUE: + return true_exprt(); + case tvt::tv_enumt::TV_FALSE: + return false_exprt(); + case tvt::tv_enumt::TV_UNKNOWN: + return false_exprt(); // default + } } } diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h index d850df3bea5..224d845dac0 100644 --- a/src/solvers/prop/prop_conv.h +++ b/src/solvers/prop/prop_conv.h @@ -131,7 +131,7 @@ class prop_conv_solvert:public prop_convt bool post_processing_done = false; // get a _boolean_ value from counterexample if not valid - virtual bool get_bool(const exprt &expr, tvt &value) const; + virtual optionalt get_bool(const exprt &expr) const; virtual literalt convert_rest(const exprt &expr); virtual literalt convert_bool(const exprt &expr); From 16ae7dd181e7915470c77233ea300ac16518c97c Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 14:42:02 +0000 Subject: [PATCH 03/10] Refactoring set_equality_to_true --- src/solvers/prop/prop_conv.cpp | 26 +++++--------------------- 1 file changed, 5 insertions(+), 21 deletions(-) diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index f5a81edfbef..93cb937ce2b 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -299,29 +299,13 @@ literalt prop_conv_solvert::convert_rest(const exprt &expr) bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr) { - if(!equality_propagation) + if(!equality_propagation || expr.lhs().id() != ID_symbol) return true; - // optimization for constraint of the form - // new_variable = value - - if(expr.lhs().id()==ID_symbol) - { - const irep_idt &identifier= - to_symbol_expr(expr.lhs()).get_identifier(); - - literalt tmp=convert(expr.rhs()); - - std::pair result= - symbols.insert(std::pair(identifier, tmp)); - - if(result.second) - return false; // ok, inserted! - - // nah, already there - } - - return true; + const irep_idt &identifier = to_symbol_expr(expr.lhs()).get_identifier(); + const literalt tmp = convert(expr.rhs()); + const bool inserted = symbols.emplace(identifier, tmp).second; + return !inserted; } void prop_conv_solvert::set_to(const exprt &expr, bool value) From eedf20eb30546406700a09286f7887e24a7a489b Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 15:02:17 +0000 Subject: [PATCH 04/10] Rename SUB in baset The class actualy designated by this is a base class and not a subclass, so baset is clearer. --- src/solvers/flattening/arrays.cpp | 2 +- src/solvers/flattening/arrays.h | 7 ++++--- src/solvers/flattening/boolbv.cpp | 4 ++-- src/solvers/flattening/boolbv.h | 6 +++--- src/solvers/flattening/boolbv_bv_rel.cpp | 4 ++-- src/solvers/flattening/boolbv_extractbit.cpp | 4 ++-- src/solvers/flattening/boolbv_get.cpp | 2 +- .../flattening/boolbv_ieee_float_rel.cpp | 4 ++-- src/solvers/flattening/boolbv_overflow.cpp | 6 +++--- src/solvers/flattening/boolbv_quantifier.cpp | 2 +- src/solvers/flattening/boolbv_typecast.cpp | 2 +- src/solvers/flattening/bv_pointers.cpp | 20 +++++++++---------- src/solvers/flattening/bv_pointers.h | 6 +++--- src/solvers/refinement/bv_refinement.h | 1 + src/solvers/refinement/refine_arithmetic.cpp | 16 +++++++-------- 15 files changed, 44 insertions(+), 42 deletions(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index b48f4c65647..801f89b5cd0 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -62,7 +62,7 @@ literalt arrayst::record_array_equality( array_equalities.back().f1=op0; array_equalities.back().f2=op1; - array_equalities.back().l=SUB::equality(op0, op1); + array_equalities.back().l = baset::equality(op0, op1); arrays.make_union(op0, op1); collect_arrays(op0); diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h index a5434c3e48f..760bc86e549 100644 --- a/src/solvers/flattening/arrays.h +++ b/src/solvers/flattening/arrays.h @@ -27,17 +27,18 @@ class update_exprt; class arrayst:public equalityt { +private: + typedef equalityt baset; + public: arrayst(const namespacet &_ns, propt &_prop); void post_process() override { post_process_arrays(); - SUB::post_process(); + baset::post_process(); } - // NOLINTNEXTLINE(readability/identifiers) - typedef equalityt SUB; literalt record_array_equality(const equal_exprt &expr); void record_array_index(const index_exprt &expr); diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index f5adfb21da6..ce2f964d7f8 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -561,7 +561,7 @@ literalt boolbvt::convert_rest(const exprt &expr) return const_literal(true); } - return SUB::convert_rest(expr); + return baset::convert_rest(expr); } bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr) @@ -602,7 +602,7 @@ void boolbvt::set_to(const exprt &expr, bool 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); + baset::set_to(expr, value); } exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv) diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 0e77b6d7cc5..193ba9ebf0e 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -53,7 +53,7 @@ class boolbvt:public arrayst void clear_cache() override { - SUB::clear_cache(); + baset::clear_cache(); bv_cache.clear(); } @@ -61,7 +61,7 @@ class boolbvt:public arrayst { post_process_quantifiers(); functions.post_process(); - SUB::post_process(); + baset::post_process(); } // get literals for variables/expressions, if available @@ -100,7 +100,7 @@ class boolbvt:public arrayst virtual bool boolbv_set_equality_to_true(const equal_exprt &expr); // NOLINTNEXTLINE(readability/identifiers) - typedef arrayst SUB; + typedef arrayst baset; void conversion_failed(const exprt &expr, bvt &bv) { diff --git a/src/solvers/flattening/boolbv_bv_rel.cpp b/src/solvers/flattening/boolbv_bv_rel.cpp index 86140972cd2..31cd26de75d 100644 --- a/src/solvers/flattening/boolbv_bv_rel.cpp +++ b/src/solvers/flattening/boolbv_bv_rel.cpp @@ -46,7 +46,7 @@ literalt boolbvt::convert_bv_rel(const exprt &expr) else if(rel==ID_gt) return float_utils.relation(bv0, float_utilst::relt::GT, bv1); else - return SUB::convert_rest(expr); + return baset::convert_rest(expr); } else if((op0.type().id()==ID_range && op1.type()==op0.type()) || @@ -109,5 +109,5 @@ literalt boolbvt::convert_bv_rel(const exprt &expr) } } - return SUB::convert_rest(expr); + return baset::convert_rest(expr); } diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp index a2da9cc3352..ec6e3084ffc 100644 --- a/src/solvers/flattening/boolbv_extractbit.cpp +++ b/src/solvers/flattening/boolbv_extractbit.cpp @@ -50,7 +50,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr) std::size_t width_op1=boolbv_width(operands[1].type()); if(width_op0==0 || width_op1==0) - return SUB::convert_rest(expr); + return baset::convert_rest(expr); std::size_t index_width = std::max(address_bits(width_op0), width_op1); unsignedbv_typet index_type(index_width); @@ -90,5 +90,5 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr) } } - return SUB::convert_rest(expr); + return baset::convert_rest(expr); } diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp index 71d94d02f8a..62be8cf1942 100644 --- a/src/solvers/flattening/boolbv_get.cpp +++ b/src/solvers/flattening/boolbv_get.cpp @@ -62,7 +62,7 @@ exprt boolbvt::get(const exprt &expr) const } } - return SUB::get(expr); + return baset::get(expr); } exprt boolbvt::bv_get_rec( diff --git a/src/solvers/flattening/boolbv_ieee_float_rel.cpp b/src/solvers/flattening/boolbv_ieee_float_rel.cpp index 87c86572e0d..60518d21a54 100644 --- a/src/solvers/flattening/boolbv_ieee_float_rel.cpp +++ b/src/solvers/flattening/boolbv_ieee_float_rel.cpp @@ -40,9 +40,9 @@ literalt boolbvt::convert_ieee_float_rel(const exprt &expr) else if(rel==ID_ieee_float_notequal) return !float_utils.relation(bv0, float_utilst::relt::EQ, bv1); else - return SUB::convert_rest(expr); + return baset::convert_rest(expr); } } - return SUB::convert_rest(expr); + return baset::convert_rest(expr); } diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp index f7e4798f780..664adc400d7 100644 --- a/src/solvers/flattening/boolbv_overflow.cpp +++ b/src/solvers/flattening/boolbv_overflow.cpp @@ -26,7 +26,7 @@ literalt boolbvt::convert_overflow(const exprt &expr) const bvt &bv1=convert_bv(operands[1]); if(bv0.size()!=bv1.size()) - return SUB::convert_rest(expr); + return baset::convert_rest(expr); bv_utilst::representationt rep= expr.op0().type().id()==ID_signedbv?bv_utilst::representationt::SIGNED: @@ -43,7 +43,7 @@ literalt boolbvt::convert_overflow(const exprt &expr) if(operands[0].type().id()!=ID_unsignedbv && operands[0].type().id()!=ID_signedbv) - return SUB::convert_rest(expr); + return baset::convert_rest(expr); bvt bv0=convert_bv(operands[0]); bvt bv1=convert_bv(operands[1]); @@ -205,5 +205,5 @@ literalt boolbvt::convert_overflow(const exprt &expr) } } - return SUB::convert_rest(expr); + return baset::convert_rest(expr); } diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp index 23f8857f80d..0f85390abc3 100644 --- a/src/solvers/flattening/boolbv_quantifier.cpp +++ b/src/solvers/flattening/boolbv_quantifier.cpp @@ -205,7 +205,7 @@ literalt boolbvt::convert_quantifier(const exprt &src) { exprt expr(src); if(!instantiate_quantifier(expr, ns)) - return SUB::convert_rest(src); + return baset::convert_rest(src); quantifiert quantifier; quantifier.expr=expr; diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp index 724b59b6a78..45202b01a47 100644 --- a/src/solvers/flattening/boolbv_typecast.cpp +++ b/src/solvers/flattening/boolbv_typecast.cpp @@ -608,5 +608,5 @@ literalt boolbvt::convert_typecast(const typecast_exprt &expr) if(!bv.empty()) return prop.lor(bv); - return SUB::convert_rest(expr); + return baset::convert_rest(expr); } diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp index e899f386767..26cf6aadf56 100644 --- a/src/solvers/flattening/bv_pointers.cpp +++ b/src/solvers/flattening/bv_pointers.cpp @@ -83,7 +83,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr) } } - return SUB::convert_rest(expr); + return baset::convert_rest(expr); } bv_pointerst::bv_pointerst( @@ -283,15 +283,15 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) } else if(expr.id()==ID_if) { - return SUB::convert_if(to_if_expr(expr)); + return baset::convert_if(to_if_expr(expr)); } else if(expr.id()==ID_index) { - return SUB::convert_index(to_index_expr(expr)); + return baset::convert_index(to_index_expr(expr)); } else if(expr.id()==ID_member) { - return SUB::convert_member(to_member_expr(expr)); + return baset::convert_member(to_member_expr(expr)); } else if(expr.id()==ID_address_of) { @@ -452,7 +452,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) else if(expr.id()==ID_lshr || expr.id()==ID_shl) { - return SUB::convert_shift(to_shift_expr(expr)); + return baset::convert_shift(to_shift_expr(expr)); } else if(expr.id()==ID_bitand || expr.id()==ID_bitor || @@ -462,12 +462,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr) } else if(expr.id()==ID_concatenation) { - return SUB::convert_concatenation(expr); + return baset::convert_concatenation(expr); } else if(expr.id()==ID_byte_extract_little_endian || expr.id()==ID_byte_extract_big_endian) { - return SUB::convert_byte_extract(to_byte_extract_expr(expr)); + return baset::convert_byte_extract(to_byte_extract_expr(expr)); } else if( expr.id() == ID_byte_update_little_endian || @@ -601,7 +601,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr) return bv_utils.zero_extension(op0, width); } - return SUB::convert_bitvector(expr); + return baset::convert_bitvector(expr); } exprt bv_pointerst::bv_get_rec( @@ -611,7 +611,7 @@ exprt bv_pointerst::bv_get_rec( const typet &type) const { if(type.id()!=ID_pointer) - return SUB::bv_get_rec(bv, unknown, offset, type); + return baset::bv_get_rec(bv, unknown, offset, type); std::string value_addr, value_offset, value; @@ -838,7 +838,7 @@ void bv_pointerst::do_postponed( void bv_pointerst::post_process() { // post-processing arrays may yield further objects, do this first - SUB::post_process(); + baset::post_process(); for(postponed_listt::const_iterator it=postponed_list.begin(); diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h index cd0cc8166ef..e903f9d82fa 100644 --- a/src/solvers/flattening/bv_pointers.h +++ b/src/solvers/flattening/bv_pointers.h @@ -16,6 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com class bv_pointerst:public boolbvt { +private: + typedef boolbvt baset; + public: bv_pointerst(const namespacet &_ns, propt &_prop); @@ -24,9 +27,6 @@ class bv_pointerst:public boolbvt protected: pointer_logict pointer_logic; - // NOLINTNEXTLINE(readability/identifiers) - typedef boolbvt SUB; - unsigned object_bits, offset_bits, bits; void encode(std::size_t object, bvt &bv); diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h index 05b4c056d9b..6f16a5322f7 100644 --- a/src/solvers/refinement/bv_refinement.h +++ b/src/solvers/refinement/bv_refinement.h @@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com class bv_refinementt:public bv_pointerst { private: + typedef bv_pointerst baset; struct configt { ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN; diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp index 86641b8ffa4..e5106f0f021 100644 --- a/src/solvers/refinement/refine_arithmetic.cpp +++ b/src/solvers/refinement/refine_arithmetic.cpp @@ -39,11 +39,11 @@ void bv_refinementt::approximationt::add_under_assumption(literalt l) bvt bv_refinementt::convert_floatbv_op(const exprt &expr) { if(!config_.refine_arithmetic) - return SUB::convert_floatbv_op(expr); + return baset::convert_floatbv_op(expr); if(ns.follow(expr.type()).id()!=ID_floatbv || expr.operands().size()!=3) - return SUB::convert_floatbv_op(expr); + return baset::convert_floatbv_op(expr); bvt bv; add_approximation(expr, bv); @@ -53,7 +53,7 @@ bvt bv_refinementt::convert_floatbv_op(const exprt &expr) bvt bv_refinementt::convert_mult(const exprt &expr) { if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv) - return SUB::convert_mult(expr); + return baset::convert_mult(expr); // we catch any multiplication // unless it involves a constant @@ -70,7 +70,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr) // we keep multiplication by a constant for integers if(type.id()!=ID_floatbv) if(operands[0].is_constant() || operands[1].is_constant()) - return SUB::convert_mult(expr); + return baset::convert_mult(expr); bvt bv; approximationt &a=add_approximation(expr, bv); @@ -101,7 +101,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr) bvt bv_refinementt::convert_div(const div_exprt &expr) { if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv) - return SUB::convert_div(expr); + return baset::convert_div(expr); // we catch any division // unless it's integer division by a constant @@ -109,7 +109,7 @@ bvt bv_refinementt::convert_div(const div_exprt &expr) PRECONDITION(expr.operands().size()==2); if(expr.op1().is_constant()) - return SUB::convert_div(expr); + return baset::convert_div(expr); bvt bv; add_approximation(expr, bv); @@ -119,7 +119,7 @@ bvt bv_refinementt::convert_div(const div_exprt &expr) bvt bv_refinementt::convert_mod(const mod_exprt &expr) { if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv) - return SUB::convert_mod(expr); + return baset::convert_mod(expr); // we catch any mod // unless it's integer + constant @@ -127,7 +127,7 @@ bvt bv_refinementt::convert_mod(const mod_exprt &expr) PRECONDITION(expr.operands().size()==2); if(expr.op1().is_constant()) - return SUB::convert_mod(expr); + return baset::convert_mod(expr); bvt bv; add_approximation(expr, bv); From 444bf1426576a556c1251a502b90d506b4e0f023 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 7 Feb 2018 15:18:39 +0000 Subject: [PATCH 05/10] Simplify is_unbounded_array --- src/solvers/flattening/boolbv.cpp | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index ce2f964d7f8..6a628259c25 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -637,17 +637,9 @@ bool boolbvt::is_unbounded_array(const typet &type) const if(unbounded_array==unbounded_arrayt::U_ALL) return true; - const exprt &size=to_array_type(type).size(); - - mp_integer s; - if(to_integer(size, s)) - return true; - - if(unbounded_array==unbounded_arrayt::U_AUTO) - if(s>MAX_FLATTENED_ARRAY_SIZE) - return true; - - return false; + const auto s = numeric_cast(to_array_type(type).size()); + return !s.has_value() || (unbounded_array == unbounded_arrayt::U_AUTO && + *s > MAX_FLATTENED_ARRAY_SIZE); } void boolbvt::print_assignment(std::ostream &out) const From 4c9364ba95ebf5ecdddad3fe4cb03b1bd3518595 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 8 Feb 2018 06:38:14 +0000 Subject: [PATCH 06/10] Refactoring in boolbvt::convert_add_sub --- src/solvers/flattening/boolbv_add_sub.cpp | 44 +++++++++-------------- 1 file changed, 17 insertions(+), 27 deletions(-) diff --git a/src/solvers/flattening/boolbv_add_sub.cpp b/src/solvers/flattening/boolbv_add_sub.cpp index 3656b33384a..484c927260b 100644 --- a/src/solvers/flattening/boolbv_add_sub.cpp +++ b/src/solvers/flattening/boolbv_add_sub.cpp @@ -26,39 +26,30 @@ bvt boolbvt::convert_add_sub(const exprt &expr) type.id()!=ID_vector) return conversion_failed(expr); - std::size_t width=boolbv_width(type); - + const std::size_t width = boolbv_width(type); if(width==0) return conversion_failed(expr); const exprt::operandst &operands=expr.operands(); - if(operands.empty()) - throw "operator "+expr.id_string()+" takes at least one operand"; - + INVARIANT( + !operands.empty(), + "operator " + expr.id_string() + " takes at least one operand"); const exprt &op0=expr.op0(); DATA_INVARIANT( op0.type() == type, "add/sub with mixed types:\n" + expr.pretty()); bvt bv=convert_bv(op0); - if(bv.size()!=width) - throw "convert_add_sub: unexpected operand 0 width"; - - bool subtract=(expr.id()==ID_minus || - expr.id()=="no-overflow-minus"); - - bool no_overflow=(expr.id()=="no-overflow-plus" || - expr.id()=="no-overflow-minus"); + const typet arithmetic_type = + (type.id() == ID_vector || type.id() == ID_complex) + ? ns.follow(type.subtype()) + : type; - typet arithmetic_type= - (type.id()==ID_vector || type.id()==ID_complex)? - ns.follow(type.subtype()):type; - - bv_utilst::representationt rep= - (arithmetic_type.id()==ID_signedbv || - arithmetic_type.id()==ID_fixedbv)?bv_utilst::representationt::SIGNED: - bv_utilst::representationt::UNSIGNED; + const bv_utilst::representationt rep = + (arithmetic_type.id() == ID_signedbv || arithmetic_type.id() == ID_fixedbv) + ? bv_utilst::representationt::SIGNED + : bv_utilst::representationt::UNSIGNED; for(exprt::operandst::const_iterator it=operands.begin()+1; @@ -75,13 +66,12 @@ bvt boolbvt::convert_add_sub(const exprt &expr) if(type.id()==ID_vector || type.id()==ID_complex) { const typet &subtype=ns.follow(type.subtype()); + const std::size_t sub_width = boolbv_width(subtype); + INVARIANT( + sub_width != 0 && width % sub_width == 0, + "convert_add_sub: unexpected vector operand width"); - std::size_t sub_width=boolbv_width(subtype); - - if(sub_width==0 || width%sub_width!=0) - throw "convert_add_sub: unexpected vector operand width"; - - std::size_t size=width/sub_width; + const std::size_t size = width / sub_width; bv.resize(width); for(std::size_t i=0; i Date: Thu, 8 Feb 2018 06:38:36 +0000 Subject: [PATCH 07/10] Refactoring in boolbvt::convert_array --- src/solvers/flattening/arrays.cpp | 13 ++++--------- src/solvers/flattening/boolbv_array.cpp | 23 +++++++---------------- 2 files changed, 11 insertions(+), 25 deletions(-) diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp index 801f89b5cd0..f3cd3805432 100644 --- a/src/solvers/flattening/arrays.cpp +++ b/src/solvers/flattening/arrays.cpp @@ -34,7 +34,7 @@ void arrayst::record_array_index(const index_exprt &index) // we are not allowed to put the index directly in the // entry for the root of the equivalence class // because this map is accessed during building the error trace - std::size_t number=arrays.number(index.array()); + const std::size_t number = arrays.number(index.array()); index_map[number].insert(index.index()); update_indices.insert(number); } @@ -45,14 +45,9 @@ literalt arrayst::record_array_equality( const exprt &op0=equality.op0(); const exprt &op1=equality.op1(); - // check types - if(!base_type_eq(op0.type(), op1.type(), ns)) - { - prop.error() << equality.pretty() << messaget::eom; - DATA_INVARIANT( - false, - "record_array_equality got equality without matching types"); - } + DATA_INVARIANT( + base_type_eq(op0.type(), op1.type(), ns), + "record_array_equality should get matching types"); DATA_INVARIANT( ns.follow(op0.type()).id()==ID_array, diff --git a/src/solvers/flattening/boolbv_array.cpp b/src/solvers/flattening/boolbv_array.cpp index b96639a6d40..25083271da2 100644 --- a/src/solvers/flattening/boolbv_array.cpp +++ b/src/solvers/flattening/boolbv_array.cpp @@ -6,39 +6,30 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #include "boolbv.h" bvt boolbvt::convert_array(const exprt &expr) { - std::size_t width=boolbv_width(expr.type()); - + const std::size_t width = boolbv_width(expr.type()); if(width==0) return conversion_failed(expr); if(expr.type().id()==ID_array) { - assert(expr.has_operands()); + INVARIANT(expr.has_operands(), "array should have operands"); const exprt::operandst &operands=expr.operands(); - assert(!operands.empty()); - std::size_t op_width=width/operands.size(); - + const std::size_t op_width = width / operands.size(); bvt bv; bv.reserve(width); - forall_expr(it, operands) + for(const exprt &op : operands) { - const bvt &tmp=convert_bv(*it); - - if(tmp.size()!=op_width) - throw "convert_array: unexpected operand width"; - - forall_literals(it2, tmp) - bv.push_back(*it2); + const bvt &tmp = convert_bv(op); + CHECK_RETURN(tmp.size() == op_width); + bv.insert(bv.end(), tmp.begin(), tmp.end()); } return bv; } - return conversion_failed(expr); } From c41e26df8864f03e52b78a787c2c131775a93023 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Thu, 8 Feb 2018 06:38:53 +0000 Subject: [PATCH 08/10] Refactoring in boolbvt::convert_array_of --- src/solvers/flattening/boolbv_array_of.cpp | 19 +++++-------------- 1 file changed, 5 insertions(+), 14 deletions(-) diff --git a/src/solvers/flattening/boolbv_array_of.cpp b/src/solvers/flattening/boolbv_array_of.cpp index 2c01f095638..ea9455c3b99 100644 --- a/src/solvers/flattening/boolbv_array_of.cpp +++ b/src/solvers/flattening/boolbv_array_of.cpp @@ -13,16 +13,11 @@ Author: Daniel Kroening, kroening@kroening.com bvt boolbvt::convert_array_of(const array_of_exprt &expr) { - if(expr.type().id()!=ID_array) - throw "array_of must be array-typed"; - const array_typet &array_type=to_array_type(expr.type()); - if(is_unbounded_array(array_type)) return conversion_failed(expr); - std::size_t width=boolbv_width(array_type); - + const std::size_t width = boolbv_width(array_type); if(width==0) { // A zero-length array is acceptable; @@ -34,29 +29,25 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr) } const exprt &array_size=array_type.size(); + const auto size = numeric_cast(array_size); - mp_integer size; - - if(to_integer(array_size, size)) + if(!size) return conversion_failed(expr); const bvt &tmp=convert_bv(expr.op0()); bvt bv; bv.resize(width); - - if(size*tmp.size()!=width) - throw "convert_array_of: unexpected operand width"; + CHECK_RETURN(*size * tmp.size() == width); std::size_t offset=0; - for(mp_integer i=0; i Date: Thu, 8 Feb 2018 06:41:08 +0000 Subject: [PATCH 09/10] Refactoring in boolbvt::convert_index Factor out is_uniform function to reduce size of big function and make it clearer. Add const keyword where possible. Change assertions in INVARIANTS. Remove blank lines that are not helping clarity (for example between comments and instructions to which they apply). Use numeric_cast instead of to_integer. --- src/solvers/flattening/boolbv_index.cpp | 200 ++++++++---------------- 1 file changed, 66 insertions(+), 134 deletions(-) diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp index ca66fb2c697..0263837f464 100644 --- a/src/solvers/flattening/boolbv_index.cpp +++ b/src/solvers/flattening/boolbv_index.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" +#include #include #include @@ -15,33 +16,45 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +/// \param array: an array expression +/// \return true if all elements are equal +static bool is_uniform(const exprt &array) +{ + if(array.id() == ID_array_of) + return true; + if(array.id() == ID_constant || array.id() == ID_array) + { + return std::all_of( + array.operands().begin(), + array.operands().end(), + [&](const exprt &expr) { // NOLINT + return expr == array.op0(); + }); + } + return false; +} + bvt boolbvt::convert_index(const index_exprt &expr) { const exprt &array=expr.array(); const exprt &index=expr.index(); - const typet &array_op_type=ns.follow(array.type()); - bvt bv; if(array_op_type.id()==ID_array) { - const array_typet &array_type= - to_array_type(array_op_type); - - std::size_t width=boolbv_width(expr.type()); + const array_typet &array_type = to_array_type(array_op_type); + const std::size_t width = boolbv_width(expr.type()); if(width==0) return conversion_failed(expr); // see if the array size is constant - if(is_unbounded_array(array_type)) { // use array decision procedure // free variables - bv.resize(width); for(std::size_t i=0; i(array_type.size()); // see if the index address is constant // many of these are compacted by simplify_expr // but variable location writes will block this - mp_integer index_value; - if(!to_integer(index, index_value)) - return convert_index(array, index_value); + if(const auto index_value = numeric_cast(index)) + return convert_index(array, *index_value); // Special case : arrays of one thing (useful for constants) // TODO : merge with ACTUAL_ARRAY_HACK so that ranges of the same @@ -78,52 +86,25 @@ bvt boolbvt::convert_index(const index_exprt &expr) // this rather than as a series of individual options. #define UNIFORM_ARRAY_HACK #ifdef UNIFORM_ARRAY_HACK - bool is_uniform = false; - - if(array.id()==ID_array_of) - { - is_uniform = true; - } - else if(array.id()==ID_constant || array.id()==ID_array) - { - bool found_exception = false; - forall_expr(it, array.operands()) - { - if(*it != array.op0()) - { - found_exception = true; - break; - } - } - - if(!found_exception) - is_uniform = true; - } - - if(is_uniform && prop.has_set_to()) + if(is_uniform(array) && prop.has_set_to()) { static int uniform_array_counter; // Temporary hack - std::string identifier= - "__CPROVER_internal_uniform_array_"+ - std::to_string(uniform_array_counter++); + const std::string identifier = "__CPROVER_internal_uniform_array_" + + std::to_string(uniform_array_counter++); - symbol_exprt result(identifier, expr.type()); + const symbol_exprt result(identifier, expr.type()); bv = convert_bv(result); - equal_exprt value_equality(result, array.op0()); + const equal_exprt value_equality(result, array.op0()); - binary_relation_exprt lower_bound( + const binary_relation_exprt lower_bound( from_integer(0, index.type()), ID_le, index); - binary_relation_exprt upper_bound( + const binary_relation_exprt upper_bound( index, ID_lt, from_integer(array_size, index.type())); - if(lower_bound.lhs().is_nil() || - upper_bound.rhs().is_nil()) - throw "number conversion failed (2)"; - - and_exprt range_condition(lower_bound, upper_bound); - implies_exprt implication(range_condition, value_equality); + const and_exprt range_condition(lower_bound, upper_bound); + const implies_exprt implication(range_condition, value_equality); // Simplify may remove the lower bound if the type // is correct. @@ -147,42 +128,27 @@ bvt boolbvt::convert_index(const index_exprt &expr) // Symbol for output static int actual_array_counter; // Temporary hack - std::string identifier= - "__CPROVER_internal_actual_array_"+ - std::to_string(actual_array_counter++); + const std::string identifier = "__CPROVER_internal_actual_array_" + + std::to_string(actual_array_counter++); - symbol_exprt result(identifier, expr.type()); + const symbol_exprt result(identifier, expr.type()); bv = convert_bv(result); - // add implications - - equal_exprt index_equality; - index_equality.lhs()=index; // index operand - - equal_exprt value_equality; - value_equality.lhs()=result; + INVARIANT( + array_size <= array.operands().size(), + "size should not exceed number of operands"); #ifdef COMPACT_EQUAL_CONST bv_utils.equal_const_register(convert_bv(index)); // Definitely bv_utils.equal_const_register(convert_bv(result)); // Maybe #endif - exprt::operandst::const_iterator it = array.operands().begin(); - - for(mp_integer i=0; i 0, "array size should be positive"); #ifdef COMPACT_EQUAL_CONST bv_utils.equal_const_register(convert_bv(index)); // Definitely #endif - typet constant_type=index.type(); // type of index operand - - assert(array_size>0); - - for(mp_integer i=0; i=0 && - offset+width<=mp_integer(tmp.size())) + const bvt &tmp = convert_bv(array); + const mp_integer offset = index * width; + const bool in_bounds = + offset >= 0 && offset + width <= mp_integer(tmp.size()); + if(in_bounds) { - // in bounds - // The assertion below is disabled as we want to be able // to run CBMC without simplifier. // Expression simplification should remove these cases - // assert(array.id()!=ID_array_of && - // array.id()!=ID_array); // If not there are large improvements possible as above for(std::size_t i=0; i Date: Thu, 8 Feb 2018 06:41:30 +0000 Subject: [PATCH 10/10] Refactoring in boolbvt::convert_mult --- src/solvers/flattening/boolbv_mult.cpp | 59 ++++++++------------------ 1 file changed, 17 insertions(+), 42 deletions(-) diff --git a/src/solvers/flattening/boolbv_mult.cpp b/src/solvers/flattening/boolbv_mult.cpp index 15803b7ead5..b4711ce7f0d 100644 --- a/src/solvers/flattening/boolbv_mult.cpp +++ b/src/solvers/flattening/boolbv_mult.cpp @@ -12,53 +12,40 @@ Author: Daniel Kroening, kroening@kroening.com bvt boolbvt::convert_mult(const exprt &expr) { - std::size_t width=boolbv_width(expr.type()); - + const std::size_t width = boolbv_width(expr.type()); if(width==0) return conversion_failed(expr); - bvt bv; bv.resize(width); const exprt::operandst &operands=expr.operands(); - if(operands.empty()) - throw "mult without operands"; - + DATA_INVARIANT(!operands.empty(), "mult must have operands"); const exprt &op0=expr.op0(); - - bool no_overflow=expr.id()=="no-overflow-mult"; + const bool no_overflow = expr.id() == "no-overflow-mult"; if(expr.type().id()==ID_fixedbv) { - if(op0.type()!=expr.type()) - throw "multiplication with mixed types"; - + DATA_INVARIANT(op0.type() == expr.type(), "multiplication with mixed types"); bv=convert_bv(op0); - if(bv.size()!=width) - throw "convert_mult: unexpected operand width"; - - std::size_t fraction_bits= + DATA_INVARIANT(bv.size() == width, "convert_mult: unexpected operand width"); + const std::size_t fraction_bits = to_fixedbv_type(expr.type()).get_fraction_bits(); for(exprt::operandst::const_iterator it=operands.begin()+1; it!=operands.end(); it++) { - if(it->type()!=expr.type()) - throw "multiplication with mixed types"; + DATA_INVARIANT( + it->type() == expr.type(), + "multiplication should have uniform operand types"); // do a sign extension by fraction_bits bits bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits); - bvt op=convert_bv(*it); - if(op.size()!=width) - throw "convert_mult: unexpected operand width"; - + INVARIANT(op.size() == width, "convert_mult: unexpected operand width"); op=bv_utils.sign_extension(op, bv.size()); - bv=bv_utils.signed_multiplier(bv, op); - // cut it down again bv.erase(bv.begin(), bv.begin()+fraction_bits); } @@ -68,37 +55,25 @@ bvt boolbvt::convert_mult(const exprt &expr) else if(expr.type().id()==ID_unsignedbv || expr.type().id()==ID_signedbv) { - if(op0.type()!=expr.type()) - throw "multiplication with mixed types"; - + DATA_INVARIANT( + op0.type() == expr.type(), "multiplication with mixed types"); bv_utilst::representationt rep= expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED: bv_utilst::representationt::UNSIGNED; bv=convert_bv(op0); - - if(bv.size()!=width) - throw "convert_mult: unexpected operand width"; - + INVARIANT(bv.size() == width, "convert_mult: unexpected operand width"); for(exprt::operandst::const_iterator it=operands.begin()+1; it!=operands.end(); it++) { - if(it->type()!=expr.type()) - throw "multiplication with mixed types"; - + INVARIANT(it->type() == expr.type(), "multiplication with mixed types"); const bvt &op=convert_bv(*it); + CHECK_RETURN(op.size() == width); - if(op.size()!=width) - throw "convert_mult: unexpected operand width"; - - if(no_overflow) - bv=bv_utils.multiplier_no_overflow(bv, op, rep); - else - bv=bv_utils.multiplier(bv, op, rep); + bv = no_overflow ? bv_utils.multiplier_no_overflow(bv, op, rep) + : bv_utils.multiplier(bv, op, rep); } - return bv; } - return conversion_failed(expr); }