From 703a04c49e5d0928788e0fdc08121c89b4e7736d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Wed, 3 Mar 2021 10:31:52 +0100 Subject: [PATCH 1/2] Update CBMC to 5.7 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Replace i2string with std::to_string. Adjust abstract domains: - In CBMC 5.7, abstract domains work slightly differently than they used to. Methods for creating top, bottom and entry must be implemented. Moreover, the first merge could have no effect resulting in the function not being entered due to changes in abstract interpretation implementation in CBMC. Replace dstring with dstringt. Replace deprecated gen_zero. Fix GOTO check options. Change graph to grapht. Add missing argument to goto_inlinet constructor call. Recompute locations after inlining. Adjust memsafety tests to new checks. Signed-off-by: František Nečas --- lib/cbmc | 2 +- .../memsafety/built_from_end_false/test.desc | 2 +- regression/memsafety/simple_false/test.desc | 2 +- src/2ls/2ls_parse_options.cpp | 10 +++++--- src/2ls/2ls_parse_options.h | 2 +- src/2ls/dynamic_cfg.h | 7 +++--- src/2ls/preprocessing_util.cpp | 4 ++-- src/2ls/show.cpp | 1 - src/2ls/summary_checker_base.cpp | 1 - src/2ls/summary_checker_nonterm.cpp | 1 - src/domains/domain.h | 1 - src/domains/incremental_solver.cpp | 3 +-- src/domains/lexlinrank_domain.cpp | 5 ++-- src/domains/linrank_domain.cpp | 6 ++--- src/domains/predabs_domain.cpp | 1 - src/domains/strategy_solver_binsearch2.cpp | 4 +--- src/domains/strategy_solver_binsearch3.cpp | 4 +--- src/domains/tpolyhedra_domain.cpp | 5 ++-- src/solver/summarizer_fw_contexts.cpp | 3 +-- src/ssa/dynobj_instance_analysis.cpp | 2 +- src/ssa/dynobj_instance_analysis.h | 23 +++++++++++++++++++ src/ssa/local_ssa.cpp | 20 ++++++++-------- src/ssa/malloc_ssa.cpp | 5 ++-- src/ssa/may_alias_analysis.cpp | 2 +- src/ssa/may_alias_analysis.h | 21 ++++++++++++++++- src/ssa/ssa_dereference.cpp | 4 ++-- src/ssa/ssa_domain.cpp | 2 +- src/ssa/ssa_domain.h | 23 ++++++++++++++++++- src/ssa/ssa_inliner.cpp | 9 ++++---- src/ssa/ssa_unwinder.cpp | 7 +++--- src/ssa/ssa_value_set.cpp | 5 +++- src/ssa/ssa_value_set.h | 20 ++++++++++++++++ src/ssa/unwindable_local_ssa.cpp | 5 ++-- 33 files changed, 143 insertions(+), 69 deletions(-) diff --git a/lib/cbmc b/lib/cbmc index 7ac49c6c1..6275632e7 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit 7ac49c6c1d53c7689d586b54945949fd3b8ad51e +Subproject commit 6275632e75a46a4ee8b87009ce8e7693878f1db9 diff --git a/regression/memsafety/built_from_end_false/test.desc b/regression/memsafety/built_from_end_false/test.desc index a91a719ec..e100b955f 100644 --- a/regression/memsafety/built_from_end_false/test.desc +++ b/regression/memsafety/built_from_end_false/test.desc @@ -4,4 +4,4 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -\[main.pointer_dereference.11\] dereference failure: deallocated dynamic object in \*p: FAILURE +\[main.pointer_dereference.15\] dereference failure: deallocated dynamic object in \*p: FAILURE diff --git a/regression/memsafety/simple_false/test.desc b/regression/memsafety/simple_false/test.desc index 8efda9ea8..f091cf7f8 100644 --- a/regression/memsafety/simple_false/test.desc +++ b/regression/memsafety/simple_false/test.desc @@ -4,4 +4,4 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -\[main.pointer_dereference.23\] dereference failure: deallocated dynamic object in \*p: FAILURE +\[main.pointer_dereference.33\] dereference failure: deallocated dynamic object in \*p: FAILURE diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index 933847401..80a748b7e 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -125,7 +125,7 @@ void twols_parse_optionst::get_command_line_options(optionst &options) options.set_option("slice", false); // all checks supported by goto_check - GOTO_CHECK_PARSE_OPTIONS(cmdline, options); + PARSE_OPTIONS_GOTO_CHECK(cmdline, options); // check assertions if(cmdline.isset("no-assertions")) @@ -1087,10 +1087,14 @@ bool twols_parse_optionst::process_goto_program( goto_inlinet goto_inline( goto_model.goto_functions, ns, - ui_message_handler); + ui_message_handler, + false); goto_inline(); #if IGNORE_RECURSION recursion_detected=goto_inline.recursion_detected(); + // since CBMC 5.7, inlining doesn't update location and loop numbers + goto_model.goto_functions.update(); + goto_model.goto_functions.compute_loop_numbers(); #endif } @@ -1559,7 +1563,7 @@ void twols_parse_optionst::help() " --round-to-zero IEEE floating point rounding mode\n" "\n" "Program instrumentation options:\n" - GOTO_CHECK_HELP + HELP_GOTO_CHECK " --error-label label check that label is unreachable\n" " --show-properties show the properties\n" " --no-assertions ignore user assertions\n" diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h index 272399fb7..99a53af82 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -31,7 +31,7 @@ class optionst; "(function):" \ "D:I:" \ "(depth):(context-bound):(unwind):" \ - GOTO_CHECK_OPTIONS \ + OPT_GOTO_CHECK \ "(non-incremental)" \ "(no-assertions)(no-assumptions)" \ "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ diff --git a/src/2ls/dynamic_cfg.h b/src/2ls/dynamic_cfg.h index 3d8a9537c..928e4dbbf 100644 --- a/src/2ls/dynamic_cfg.h +++ b/src/2ls/dynamic_cfg.h @@ -14,7 +14,6 @@ Author: Peter Schrammel #include #include -#include #include #include @@ -35,9 +34,9 @@ struct dynamic_cfg_idt std::string to_string() const { std::ostringstream sid; - sid << i2string(pc->location_number); + sid << std::to_string(pc->location_number); for(const auto &i : iteration_stack) - sid << "." < exprt assumption; }; -class dynamic_cfgt:public graph +class dynamic_cfgt:public grapht { public: inline dynamic_cfg_nodet& operator[](const dynamic_cfg_idt &id) diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp index 59f1e29a1..a4cd73134 100644 --- a/src/2ls/preprocessing_util.cpp +++ b/src/2ls/preprocessing_util.cpp @@ -190,7 +190,7 @@ void twols_parse_optionst::remove_multiple_dereferences( { symbolt new_symbol; new_symbol.type=member_expr.type(); - new_symbol.name="$deref"+i2string(var_counter++); + new_symbol.name="$deref"+std::to_string(var_counter++); new_symbol.base_name=new_symbol.name; new_symbol.pretty_name=new_symbol.name; goto_model.symbol_table.add(new_symbol); @@ -465,7 +465,7 @@ void twols_parse_optionst::split_same_symbolic_object_assignments( { symbolt tmp_symbol; tmp_symbol.type=assign.lhs().type(); - tmp_symbol.name="$symderef_tmp"+i2string(counter++); + tmp_symbol.name="$symderef_tmp"+std::to_string(counter++); tmp_symbol.base_name=tmp_symbol.name; tmp_symbol.pretty_name=tmp_symbol.name; diff --git a/src/2ls/show.cpp b/src/2ls/show.cpp index fe40e9b0e..ea90a8805 100644 --- a/src/2ls/show.cpp +++ b/src/2ls/show.cpp @@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include diff --git a/src/2ls/summary_checker_base.cpp b/src/2ls/summary_checker_base.cpp index 6e7cff796..06d200440 100644 --- a/src/2ls/summary_checker_base.cpp +++ b/src/2ls/summary_checker_base.cpp @@ -12,7 +12,6 @@ Author: Peter Schrammel #include #include -#include #include #include #include diff --git a/src/2ls/summary_checker_nonterm.cpp b/src/2ls/summary_checker_nonterm.cpp index e7e404d03..e6564719e 100644 --- a/src/2ls/summary_checker_nonterm.cpp +++ b/src/2ls/summary_checker_nonterm.cpp @@ -11,7 +11,6 @@ Author: Stefan Marticek #include "summary_checker_nonterm.h" -#include #include #include diff --git a/src/domains/domain.h b/src/domains/domain.h index 1b6fd060f..f90bac393 100644 --- a/src/domains/domain.h +++ b/src/domains/domain.h @@ -16,7 +16,6 @@ Author: Peter Schrammel #include #include -#include #include #include #include diff --git a/src/domains/incremental_solver.cpp b/src/domains/incremental_solver.cpp index 063ca9983..09ba49a73 100644 --- a/src/domains/incremental_solver.cpp +++ b/src/domains/incremental_solver.cpp @@ -16,7 +16,6 @@ Author: Peter Schrammel #include #include -#include #include "incremental_solver.h" @@ -35,7 +34,7 @@ void incremental_solvert::new_context() solver->convert( symbol_exprt( "goto_symex::\\act$"+ - i2string(activation_literal_counter++), bool_typet())); + std::to_string(activation_literal_counter++), bool_typet())); #ifdef DEBUG_OUTPUT debug() << "new context: " << activation_literal<< eom; diff --git a/src/domains/lexlinrank_domain.cpp b/src/domains/lexlinrank_domain.cpp index 36cc53d9a..257012efc 100644 --- a/src/domains/lexlinrank_domain.cpp +++ b/src/domains/lexlinrank_domain.cpp @@ -14,7 +14,6 @@ Author: Peter Schrammel #endif #include -#include #include #include #include @@ -372,7 +371,7 @@ exprt lexlinrank_domaint::get_row_symb_constraint( symb_values[elm].c[0]=symbol_exprt( SYMB_COEFF_VAR+std::string("c!")+ - i2string(row)+"$"+i2string(elm)+"$0", + std::to_string(row)+"$"+std::to_string(elm)+"$0", signedbv_typet(COEFF_C_SIZE)); // coefficients are signed integers #ifdef DIFFERENCE_ENCODING @@ -388,7 +387,7 @@ exprt lexlinrank_domaint::get_row_symb_constraint( { symb_values[elm].c[i]=symbol_exprt( SYMB_COEFF_VAR+std::string("c!")+ - i2string(row)+"$"+i2string(elm)+"$"+i2string(i), + std::to_string(row)+"$"+std::to_string(elm)+"$"+std::to_string(i), signedbv_typet(COEFF_C_SIZE)); #ifdef DIFFERENCE_ENCODING sum=plus_exprt( diff --git a/src/domains/linrank_domain.cpp b/src/domains/linrank_domain.cpp index 4441421ce..e072c6d98 100644 --- a/src/domains/linrank_domain.cpp +++ b/src/domains/linrank_domain.cpp @@ -14,7 +14,6 @@ Author: Peter Schrammel #endif #include -#include #include #include #include @@ -231,7 +230,7 @@ exprt linrank_domaint::get_row_symb_constraint( symb_values.c.resize(smt_model_values.size()/2); assert(!symb_values.c.empty()); symb_values.c[0]=symbol_exprt( - SYMB_COEFF_VAR+std::string("c!")+i2string(row)+"$0", + SYMB_COEFF_VAR+std::string("c!")+std::to_string(row)+"$0", signedbv_typet(COEFF_C_SIZE)); // coefficients are signed integers #ifdef DIFFERENCE_ENCODING @@ -245,7 +244,8 @@ exprt linrank_domaint::get_row_symb_constraint( for(unsigned i=1, vals_i=2; i #include -#include #include #include diff --git a/src/domains/strategy_solver_binsearch2.cpp b/src/domains/strategy_solver_binsearch2.cpp index 4c6fa4ee9..71038dd53 100644 --- a/src/domains/strategy_solver_binsearch2.cpp +++ b/src/domains/strategy_solver_binsearch2.cpp @@ -17,8 +17,6 @@ Author: Peter Schrammel #include -#include - #include "strategy_solver_binsearch2.h" #include "ssa/local_ssa.h" #include "util.h" @@ -163,7 +161,7 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv) assert(sum.type()==lower.type()); symbol_exprt sum_bound( - SUM_BOUND_VAR+i2string(sum_bound_counter++), + SUM_BOUND_VAR+std::to_string(sum_bound_counter++), sum.type()); solver << equal_exprt(sum_bound, sum); diff --git a/src/domains/strategy_solver_binsearch3.cpp b/src/domains/strategy_solver_binsearch3.cpp index 24d1716ea..c909d0433 100644 --- a/src/domains/strategy_solver_binsearch3.cpp +++ b/src/domains/strategy_solver_binsearch3.cpp @@ -15,8 +15,6 @@ Author: Peter Schrammel #include -#include - #include "strategy_solver_binsearch3.h" #include "util.h" @@ -164,7 +162,7 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv) assert(sum.type()==lower.type()); symbol_exprt sum_bound( - SUM_BOUND_VAR+i2string(sum_bound_counter++), + SUM_BOUND_VAR+std::to_string(sum_bound_counter++), sum.type()); solver << equal_exprt(sum_bound, sum); diff --git a/src/domains/tpolyhedra_domain.cpp b/src/domains/tpolyhedra_domain.cpp index aa3f8b43e..c5fb71271 100644 --- a/src/domains/tpolyhedra_domain.cpp +++ b/src/domains/tpolyhedra_domain.cpp @@ -15,7 +15,6 @@ Author: Peter Schrammel #endif #include -#include #include #include "tpolyhedra_domain.h" @@ -186,7 +185,7 @@ symbol_exprt tpolyhedra_domaint::get_row_symb_value(const rowt &row) assert(row(*templ[row].expr); return symbol_exprt( - SYMB_BOUND_VAR+i2string(domain_number)+"$"+i2string(row), + SYMB_BOUND_VAR+std::to_string(domain_number)+"$"+std::to_string(row), row_expr.type()); } @@ -358,7 +357,7 @@ void tpolyhedra_domaint::rename_for_row(exprt &expr, const rowt &row) const std::string &old_id=expr.get_string(ID_identifier); if(old_id.find(SYMB_BOUND_VAR)==std::string::npos) { - irep_idt id=old_id+"_"+i2string(row); + irep_idt id=old_id+"_"+std::to_string(row); expr.set(ID_identifier, id); } } diff --git a/src/solver/summarizer_fw_contexts.cpp b/src/solver/summarizer_fw_contexts.cpp index 74f225a9d..2b2c4d1cf 100644 --- a/src/solver/summarizer_fw_contexts.cpp +++ b/src/solver/summarizer_fw_contexts.cpp @@ -19,7 +19,6 @@ Author: Peter Schrammel #include #include -#include #include "summarizer_fw_contexts.h" #include "summary_db.h" @@ -86,7 +85,7 @@ void summarizer_fw_contextst::inline_summaries( xmlt xml_cc("calling-context"); xml_cc.set_attribute("function", id2string(fname)); xml_cc.set_attribute( - "goto_location", i2string(n_it->location->location_number)); + "goto_location", std::to_string(n_it->location->location_number)); // location const source_locationt &source_location= diff --git a/src/ssa/dynobj_instance_analysis.cpp b/src/ssa/dynobj_instance_analysis.cpp index 73efcb772..b240dc1d3 100644 --- a/src/ssa/dynobj_instance_analysis.cpp +++ b/src/ssa/dynobj_instance_analysis.cpp @@ -206,7 +206,7 @@ bool dynobj_instance_domaint::merge( ai_domain_baset::locationt from, ai_domain_baset::locationt to) { - bool result=false; + bool result=has_values.is_false() && !other.has_values.is_false(); for(auto &obj : other.must_alias_relations) { if(must_alias_relations.find(obj.first)==must_alias_relations.end()) diff --git a/src/ssa/dynobj_instance_analysis.h b/src/ssa/dynobj_instance_analysis.h index b381b0652..ff20ab620 100644 --- a/src/ssa/dynobj_instance_analysis.h +++ b/src/ssa/dynobj_instance_analysis.h @@ -25,6 +25,7 @@ Description: In some cases, multiple instances must be used so that the #include #include #include +#include #include "ssa_object.h" #include "ssa_value_set.h" @@ -159,6 +160,28 @@ class dynobj_instance_domaint:public ai_domain_baset locationt from, locationt to); + void make_bottom() override + { + must_alias_relations.clear(); + live_pointers.clear(); + has_values=tvt(false); + } + + void make_top() override + { + must_alias_relations.clear(); + live_pointers.clear(); + has_values=tvt(true); + } + + void make_entry() override + { + make_top(); + } + +protected: + tvt has_values; + private: void rhs_concretisation( const exprt &guard, diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp index ad6299fb6..3a75f746f 100644 --- a/src/ssa/local_ssa.cpp +++ b/src/ssa/local_ssa.cpp @@ -16,7 +16,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #endif -#include #include #include #include @@ -308,7 +307,7 @@ void local_SSAt::build_phi_nodes(locationt loc) exprt local_SSAt::dereference(const exprt &src, locationt loc) const { const ssa_value_domaint &ssa_value_domain=ssa_value_ai[loc]; - const std::string nondet_prefix="deref#"+i2string(loc->location_number); + const std::string nondet_prefix="deref#"+std::to_string(loc->location_number); return ::dereference( src, ssa_value_domain, nondet_prefix, ns, options.get_bool_option("competition-mode")); @@ -384,7 +383,8 @@ void local_SSAt::build_function_call(locationt loc) exprt deref_lhs=dereference(lhs, loc); // generate a symbol for rhs - irep_idt identifier="ssa::return_value"+i2string(loc->location_number); + irep_idt identifier="ssa::return_value"+ + std::to_string(loc->location_number); symbol_exprt rhs(identifier, code_function_call.lhs().type()); assign_rec(deref_lhs, rhs, true_exprt(), loc); @@ -441,8 +441,8 @@ void local_SSAt::build_function_call(locationt loc) for(exprt &a : f.arguments()) { const std::string arg_name= - id2string(fname)+"#arg"+i2string(i)+"#"+ - i2string(loc->location_number); + id2string(fname)+"#arg"+std::to_string(i)+"#"+ + std::to_string(loc->location_number); symbol_exprt arg(arg_name, a.type()); n_it->equalities.push_back(equal_exprt(a, arg)); a=arg; @@ -902,8 +902,8 @@ void local_SSAt::replace_side_effects_rec( assert(false); /* counter++; std::string tmp_suffix= - i2string(loc->location_number)+ - "."+i2string(counter)+suffix; + std::to_string(loc->location_number)+ + "."+std::to_string(counter)+suffix; expr=malloc_ssa(side_effect_expr, tmp_suffix, ns);*/ } else @@ -928,7 +928,7 @@ symbol_exprt local_SSAt::name( kind==LOOP_BACK?"lb": kind==LOOP_SELECT?"ls": kind==OBJECT_SELECT?"os":"")+ - i2string(cnt)+ + std::to_string(cnt)+ (kind==LOOP_SELECT?std::string(""):suffix); #ifdef DEBUG @@ -981,8 +981,8 @@ exprt local_SSAt::nondet_symbol( exprt s(ID_nondet_symbol, type); const irep_idt identifier= prefix+ - i2string(loc->location_number)+ - "."+i2string(counter)+suffix; + std::to_string(loc->location_number)+ + "."+std::to_string(counter)+suffix; s.set(ID_identifier, identifier); return s; } diff --git a/src/ssa/malloc_ssa.cpp b/src/ssa/malloc_ssa.cpp index de353dea2..12f590c52 100644 --- a/src/ssa/malloc_ssa.cpp +++ b/src/ssa/malloc_ssa.cpp @@ -14,7 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include -#include #include #include @@ -70,7 +69,7 @@ exprt create_dynamic_object( address_of_object.type()=pointer_typet(value_symbol.type.subtype()); index_exprt index_expr(value_symbol.type.subtype()); index_expr.array()=value_symbol.symbol_expr(); - index_expr.index()=gen_zero(index_type()); + index_expr.index()=from_integer(0, index_type()); address_of_object.op0()=index_expr; } else @@ -252,7 +251,7 @@ static bool replace_malloc_rec( expr=malloc_ssa( to_side_effect_expr(expr), - "$"+i2string(loc_number)+suffix, + "$"+std::to_string(loc_number)+suffix, symbol_table, is_concrete, alloc_concrete); diff --git a/src/ssa/may_alias_analysis.cpp b/src/ssa/may_alias_analysis.cpp index c7f182a8a..6d8f87082 100644 --- a/src/ssa/may_alias_analysis.cpp +++ b/src/ssa/may_alias_analysis.cpp @@ -35,7 +35,7 @@ bool may_alias_domaint::merge( ai_domain_baset::locationt from, ai_domain_baset::locationt to) { - bool changed=false; + bool changed=has_values.is_false() && !other.has_values.is_false(); // do union for(aliasest::const_iterator it=other.aliases.begin(); diff --git a/src/ssa/may_alias_analysis.h b/src/ssa/may_alias_analysis.h index c1e4adf90..dc2efb3ce 100644 --- a/src/ssa/may_alias_analysis.h +++ b/src/ssa/may_alias_analysis.h @@ -14,6 +14,7 @@ Author: Viktor Malik, imalik@fit.vutbr.cz #include #include +#include #include "ssa_value_set.h" class may_alias_domaint:public ai_domain_baset @@ -24,13 +25,31 @@ class may_alias_domaint:public ai_domain_baset locationt to, ai_baset &ai, const namespacet &ns) override; - bool merge(const may_alias_domaint &other, locationt from, locationt to); + void make_bottom() override + { + aliases.clear(); + has_values=tvt(false); + } + + void make_top() override + { + aliases.clear(); + has_values=tvt(true); + } + + void make_entry() override + { + make_top(); + } + typedef union_find aliasest; aliasest aliases; protected: + tvt has_values; + void assign_lhs_aliases( const exprt &lhs, const std::set &rhs_alias_set); diff --git a/src/ssa/ssa_dereference.cpp b/src/ssa/ssa_dereference.cpp index 9bb80bbd4..86a0f7e2b 100644 --- a/src/ssa/ssa_dereference.cpp +++ b/src/ssa/ssa_dereference.cpp @@ -134,12 +134,12 @@ bool ssa_may_alias( // If one is an array and the other not, consider the elements if(t1.id()==ID_array && t2.id()!=ID_array) if(ssa_may_alias( - index_exprt(e1, gen_zero(index_type()), t1.subtype()), e2, ns)) + index_exprt(e1, from_integer(0, index_type()), t1.subtype()), e2, ns)) return true; if(t2.id()==ID_array && t2.id()!=ID_array) if(ssa_may_alias( - e1, index_exprt(e2, gen_zero(index_type()), t2.subtype()), ns)) + e1, index_exprt(e2, from_integer(0, index_type()), t2.subtype()), ns)) return true; // Pointers only alias with other pointers, diff --git a/src/ssa/ssa_domain.cpp b/src/ssa/ssa_domain.cpp index 42de2f01b..5162cc3a5 100644 --- a/src/ssa/ssa_domain.cpp +++ b/src/ssa/ssa_domain.cpp @@ -126,7 +126,7 @@ bool ssa_domaint::merge( locationt from, locationt to) { - bool result=false; + bool result=has_values.is_false() && !b.has_values.is_false(); // should traverse both maps simultaneously for(def_mapt::const_iterator diff --git a/src/ssa/ssa_domain.h b/src/ssa/ssa_domain.h index b3a4d8d4f..aa1f74ef1 100644 --- a/src/ssa/ssa_domain.h +++ b/src/ssa/ssa_domain.h @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_2LS_SSA_SSA_DOMAIN_H #include +#include #include "assignments.h" @@ -90,8 +91,28 @@ class ssa_domaint:public ai_domain_baset locationt from, locationt to); + void make_bottom() override + { + phi_nodes.clear(); + def_map.clear(); + has_values=tvt(false); + } + void make_top() override + { + phi_nodes.clear(); + def_map.clear(); + has_values=tvt(true); + } + void make_entry() override + { + has_values=tvt(true); + } + +protected: + tvt has_values; + private: - static std::map::const_iterator + static std::map::const_iterator get_object_allocation_def( const irep_idt &id, const def_mapt &def_map); diff --git a/src/ssa/ssa_inliner.cpp b/src/ssa/ssa_inliner.cpp index 3ca76aab3..375530e81 100644 --- a/src/ssa/ssa_inliner.cpp +++ b/src/ssa/ssa_inliner.cpp @@ -11,7 +11,6 @@ Author: Peter Schrammel #include -#include #include #include "ssa_inliner.h" @@ -736,7 +735,7 @@ void ssa_inlinert::rename(exprt &expr) if(expr.id()==ID_symbol) { symbol_exprt &sexpr=to_symbol_expr(expr); - irep_idt id=id2string(sexpr.get_identifier())+"@"+i2string(counter); + irep_idt id=id2string(sexpr.get_identifier())+"@"+std::to_string(counter); sexpr.set_identifier(id); } else if(expr.id()==ID_address_of) @@ -751,7 +750,7 @@ void ssa_inlinert::rename(exprt &expr) else id=id2string(obj_id)+"'addr"; - id=id2string(id)+"@"+i2string(counter); + id=id2string(id)+"@"+std::to_string(counter); } symbol_exprt addr_symbol(id, expr.type()); expr=addr_symbol; @@ -811,7 +810,9 @@ void ssa_inlinert::rename_to_caller( #endif replace_map[*it]= symbol_exprt( - id2string(it->get_identifier())+"@"+i2string(++counter), it->type()); + id2string( + it->get_identifier())+"@"+std::to_string(++counter), + it->type()); } } diff --git a/src/ssa/ssa_unwinder.cpp b/src/ssa/ssa_unwinder.cpp index 8fa42c69b..bc20805ff 100644 --- a/src/ssa/ssa_unwinder.cpp +++ b/src/ssa/ssa_unwinder.cpp @@ -13,7 +13,6 @@ Author: Peter Schrammel, Saurabh Joshi #define COMPETITION #include -#include #include "ssa_unwinder.h" @@ -229,7 +228,7 @@ void ssa_local_unwindert::unwind(unsigned k) current_enabling_expr= symbol_exprt( - "unwind::"+id2string(fname)+"::enable"+i2string(k), + "unwind::"+id2string(fname)+"::enable"+std::to_string(k), bool_typet()); SSA.enabling_exprs.push_back(current_enabling_expr); @@ -620,12 +619,12 @@ void ssa_local_unwindert::unwinder_rename( unsigned unwinding=pre ? SSA.current_unwinding : 0; if(pos==pos1) { - suffix="%"+i2string(unwinding); + suffix="%"+std::to_string(unwinding); } else { suffix=id.substr(pos, pos1-pos); - suffix+="%"+i2string(unwinding); + suffix+="%"+std::to_string(unwinding); } var.set_identifier(id2string(var.get_identifier())+suffix); diff --git a/src/ssa/ssa_value_set.cpp b/src/ssa/ssa_value_set.cpp index 2a3d59096..6dd4a73fe 100644 --- a/src/ssa/ssa_value_set.cpp +++ b/src/ssa/ssa_value_set.cpp @@ -29,6 +29,8 @@ void ssa_value_domaint::transform( ai_baset &ai, const namespacet &ns) { + if(has_values.is_false()) + return; competition_mode=static_cast(ai).options .get_bool_option("competition-mode"); if(from->is_assign()) @@ -527,7 +529,8 @@ bool ssa_value_domaint::merge( { value_mapt::iterator v_it=value_map.begin(); const value_mapt &new_value_map=other.value_map; - bool result=false; + bool result=has_values.is_false() && !other.has_values.is_false(); + has_values=tvt::unknown(); for(value_mapt::const_iterator it=new_value_map.begin(); diff --git a/src/ssa/ssa_value_set.h b/src/ssa/ssa_value_set.h index 7b4a13908..eb3cf26fb 100644 --- a/src/ssa/ssa_value_set.h +++ b/src/ssa/ssa_value_set.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "ssa_object.h" @@ -27,6 +28,23 @@ class ssa_value_domaint:public ai_domain_baset const namespacet &) const; bool merge(const ssa_value_domaint &, locationt, locationt); + void make_bottom() override + { + value_map.clear(); + has_values=tvt(false); + } + + void make_top() override + { + value_map.clear(); + has_values=tvt(true); + } + + void make_entry() override + { + make_top(); + } + struct valuest { public: @@ -78,6 +96,8 @@ class ssa_value_domaint:public ai_domain_baset } protected: + tvt has_values; + void assign_lhs_rec( const exprt &lhs, const exprt &rhs, diff --git a/src/ssa/unwindable_local_ssa.cpp b/src/ssa/unwindable_local_ssa.cpp index 78b1ef588..44762c0e9 100644 --- a/src/ssa/unwindable_local_ssa.cpp +++ b/src/ssa/unwindable_local_ssa.cpp @@ -13,7 +13,6 @@ Author: Peter Schrammel, Saurabh Joshi #include -#include #include #include #include @@ -185,8 +184,8 @@ exprt unwindable_local_SSAt::nondet_symbol( exprt s(ID_nondet_symbol, type); const irep_idt identifier= prefix+ - i2string(loc->location_number)+ - "."+i2string(counter)+unwind_suffix+suffix; + std::to_string(loc->location_number)+ + "."+std::to_string(counter)+unwind_suffix+suffix; s.set(ID_identifier, identifier); #if 0 From fbbd67636068f7a4242eca5f7b529186c95a1a89 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franti=C5=A1ek=20Ne=C4=8Das?= Date: Wed, 3 Mar 2021 11:33:52 +0100 Subject: [PATCH 2/2] Version 0.9.2 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Signed-off-by: František Nečas --- src/2ls/version.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/2ls/version.h b/src/2ls/version.h index 467e36dc8..e1bf8e3c4 100644 --- a/src/2ls/version.h +++ b/src/2ls/version.h @@ -12,6 +12,6 @@ Author: Peter Schrammel #ifndef CPROVER_2LS_2LS_VERSION_H #define CPROVER_2LS_2LS_VERSION_H -#define TWOLS_VERSION "0.9.1" +#define TWOLS_VERSION "0.9.2" #endif