diff --git a/lib/cbmc b/lib/cbmc index 18fef2504..db087cb17 160000 --- a/lib/cbmc +++ b/lib/cbmc @@ -1 +1 @@ -Subproject commit 18fef25049bc2ddbc426000e892f974eab14934e +Subproject commit db087cb17c962234cf36e25e2b6844e8c22d36c3 diff --git a/regression/memsafety/built_from_end_false/test.desc b/regression/memsafety/built_from_end_false/test.desc index db3c4b8ba..9fa1c84a2 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.17\] dereference failure: deallocated dynamic object in \*\(\(List\)\(char \*\)\(\(char \*\)p \+ \(signed long int\)8ul\)\): FAILURE +\[main.pointer_dereference.17\] dereference failure: deallocated dynamic object in p->n: FAILURE diff --git a/regression/memsafety/simple_false/test.desc b/regression/memsafety/simple_false/test.desc index ca06506c2..32937af8d 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.38\] dereference failure: deallocated dynamic object in \*\(\(List\)\(char \*\)\(\(char \*\)p \+ \(signed long int\)8ul\)\): FAILURE +\[main.pointer_dereference.38\] dereference failure: deallocated dynamic object in p->n: FAILURE diff --git a/regression/termination/precond_term1/test.desc b/regression/termination/precond_term1/test.desc index d04e470d6..0b4252a1b 100644 --- a/regression/termination/precond_term1/test.desc +++ b/regression/termination/precond_term1/test.desc @@ -1,6 +1,17 @@ -CORE +KNOWNBUG main.c --preconditions ^EXIT=5$ ^SIGNAL=0$ \[__CPROVER__start\]: !\(argc' <= 1 && -\(\(signed __CPROVER_bitvector\[33\]\)argc'\) <= -1\) +-- +-- +CBMC 5.12 introduced significant changes to solvers and this test failure +seems to be one of its consequences. The formulae pushed into the solver +seem to be identical to the previous 2LS version, however the solver in +SSA analyzer then throws UNSAT on the first iteration when doing +backward analysis (the invariants up until that point are correct) +resulting in no improvements done to the template. + +This problem will require further investigation once the CBMC rebase +is complete diff --git a/src/2ls/2ls_parse_options.cpp b/src/2ls/2ls_parse_options.cpp index 09ffda976..007bf951b 100644 --- a/src/2ls/2ls_parse_options.cpp +++ b/src/2ls/2ls_parse_options.cpp @@ -69,7 +69,7 @@ Author: Daniel Kroening, Peter Schrammel #define FILTER_ASSERTIONS 1 twols_parse_optionst::twols_parse_optionst(int argc, const char **argv): - parse_options_baset(TWOLS_OPTIONS, argc, argv), + parse_options_baset(TWOLS_OPTIONS, argc, argv, "2LS " TWOLS_VERSION), messaget(ui_message_handler), ui_message_handler(cmdline, "2LS " TWOLS_VERSION), recursion_detected(false), @@ -630,34 +630,43 @@ int twols_parse_optionst::doit() // do actual analysis switch((*checker)(goto_model)) { - case property_checkert::resultt::PASS: + case resultt::PASS: if(report_assertions) - report_properties(options, goto_model, checker->property_map); + report_properties( + options, + goto_model, + checker->property_map, + checker->traces); report_success(); if(cmdline.isset("graphml-witness")) output_graphml_proof(options, goto_model, *checker); retval=0; break; - case property_checkert::resultt::FAIL: + case resultt::FAIL: { if(report_assertions) - report_properties(options, goto_model, checker->property_map); + report_properties( + options, + goto_model, + checker->property_map, + checker->traces); // validate trace bool trace_valid=false; for(const auto &p : checker->property_map) { - if(p.second.result!=property_checkert::resultt::FAIL) + if(p.second.status!=property_statust::FAIL) continue; + goto_tracet trace=checker->traces[p.first]; if(options.get_bool_option("trace")) - show_counterexample(goto_model, p.second.error_trace); + show_counterexample(goto_model, trace); trace_valid= - !p.second.error_trace.steps.empty() && + !trace.steps.empty() && (options.get_bool_option("nontermination") || - p.second.error_trace.steps.back().is_assert()); + trace.steps.back().is_assert()); break; } @@ -678,9 +687,13 @@ int twols_parse_optionst::doit() retval=10; break; } - case property_checkert::resultt::UNKNOWN: + case resultt::UNKNOWN: if(report_assertions) - report_properties(options, goto_model, checker->property_map); + report_properties( + options, + goto_model, + checker->property_map, + checker->traces); retval=5; report_unknown(); break; @@ -693,6 +706,7 @@ int twols_parse_optionst::doit() { checker->instrument_and_output( goto_model, + ui_message_handler, ui_message_handler.get_verbosity()); } @@ -1128,10 +1142,7 @@ bool twols_parse_optionst::process_goto_program( if(cmdline.isset("show-properties")) { - show_properties( - goto_model, - get_message_handler(), - ui_message_handler.get_ui()); + show_properties(goto_model, ui_message_handler); return true; } @@ -1143,8 +1154,7 @@ bool twols_parse_optionst::process_goto_program( { show_goto_functions( goto_model, - get_message_handler(), - ui_message_handler.get_ui(), + ui_message_handler, false); return true; } @@ -1179,9 +1189,10 @@ bool twols_parse_optionst::process_goto_program( void twols_parse_optionst::report_properties( const optionst &options, const goto_modelt &goto_model, - const property_checkert::property_mapt &property_map) + const propertiest &property_map, + const tracest &traces) { - for(property_checkert::property_mapt::const_iterator + for(propertiest::const_iterator it=property_map.begin(); it!=property_map.end(); it++) @@ -1193,7 +1204,7 @@ void twols_parse_optionst::report_properties( #endif if(!options.get_bool_option("all-properties") && - it->second.result!=property_checkert::resultt::FAIL) + it->second.status!=property_statust::FAIL) continue; if(ui_message_handler.get_ui()==ui_message_handlert::uit::XML_UI) @@ -1202,27 +1213,27 @@ void twols_parse_optionst::report_properties( xml_result.set_attribute("property", id2string(it->first)); xml_result.set_attribute( "status", - property_checkert::as_string(it->second.result)); + as_string(it->second.status)); std::cout << xml_result << "\n"; } else { status() << "[" << it->first << "] " - << it->second.location->source_location.get_comment() + << it->second.pc->source_location.get_comment() << ": " - << property_checkert::as_string(it->second.result) + << as_string(it->second.status) << eom; } if(options.get_bool_option("trace") && - it->second.result==property_checkert::resultt::FAIL) - show_counterexample(goto_model, it->second.error_trace); + it->second.status==property_statust::FAIL) + show_counterexample(goto_model, traces.at(it->first)); if(cmdline.isset("json-cex") && - it->second.result==property_checkert::resultt::FAIL) + it->second.status==property_statust::FAIL) output_json_cex( options, goto_model, - it->second.error_trace, + traces.at(it->first), id2string(it->first)); } @@ -1233,14 +1244,15 @@ void twols_parse_optionst::report_properties( unsigned failed=0; unsigned unknown=0; - for(property_checkert::property_mapt::const_iterator + for(propertiest::const_iterator it=property_map.begin(); it!=property_map.end(); it++) { - if(it->second.result==property_checkert::resultt::UNKNOWN) + if(it->second.status==property_statust::UNKNOWN || + it->second.status==property_statust::NOT_CHECKED) unknown++; - if(it->second.result==property_checkert::resultt::FAIL) + if(it->second.status==property_statust::FAIL) failed++; } @@ -1309,7 +1321,7 @@ void twols_parse_optionst::output_graphml_cex( { for(const auto &p : summary_checker.property_map) { - if(p.second.result!=property_checkert::resultt::FAIL) + if(p.second.status!=property_statust::FAIL) continue; const namespacet ns(goto_model.symbol_table); @@ -1317,7 +1329,7 @@ void twols_parse_optionst::output_graphml_cex( if(!graphml.empty()) { graphml_witnesst graphml_witness(ns); - graphml_witness(p.second.error_trace); + graphml_witness(summary_checker.traces.at(p.first)); if(graphml=="-") write_graphml(graphml_witness.graph(), std::cout); diff --git a/src/2ls/2ls_parse_options.h b/src/2ls/2ls_parse_options.h index 3d0b04962..c1d60ec26 100644 --- a/src/2ls/2ls_parse_options.h +++ b/src/2ls/2ls_parse_options.h @@ -16,8 +16,6 @@ Author: Daniel Kroening, Peter Schrammel #include #include -#include - #include #include @@ -104,7 +102,8 @@ class twols_parse_optionst: void report_properties( const optionst &options, const goto_modelt &, - const summary_checker_baset::property_mapt &); + const propertiest &, + const tracest &traces); void show_counterexample( const goto_modelt &, diff --git a/src/2ls/Makefile b/src/2ls/Makefile index 6a0686276..b096803bf 100644 --- a/src/2ls/Makefile +++ b/src/2ls/Makefile @@ -27,6 +27,7 @@ OBJ+= $(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ $(CPROVER_DIR)/src/util/util$(LIBEXT) \ $(CPROVER_DIR)/src/goto-instrument/unwind$(OBJEXT) \ $(CPROVER_DIR)/src/goto-instrument/unwindset$(OBJEXT) \ + $(CPROVER_DIR)/src/goto-checker/goto-checker$(LIBEXT) \ ../domains/domains$(LIBEXT) \ ../ssa/ssa$(LIBEXT) \ ../solver/solver$(LIBEXT) \ diff --git a/src/2ls/cover_goals_ext.cpp b/src/2ls/cover_goals_ext.cpp index 17c3d1a45..d34cbee68 100644 --- a/src/2ls/cover_goals_ext.cpp +++ b/src/2ls/cover_goals_ext.cpp @@ -130,14 +130,15 @@ void cover_goals_extt::assignment() for(goal_mapt::const_iterator it=goal_map.begin(); it!=goal_map.end(); it++, g_it++) { - if(property_map[it->first].result==property_checkert::resultt::UNKNOWN && + if((property_map.at(it->first).status==property_statust::UNKNOWN || + property_map.at(it->first).status==property_statust::NOT_CHECKED) && solver.l_get(g_it->condition).is_true()) { - property_map[it->first].result=property_checkert::resultt::FAIL; + property_map.at(it->first).status=property_statust::FAIL; if(build_error_trace) { ssa_build_goto_tracet build_goto_trace(SSA, solver.get_solver()); - build_goto_trace(property_map[it->first].error_trace); + build_goto_trace(traces[it->first]); if(!all_properties) break; } @@ -159,14 +160,15 @@ void cover_goals_extt::assignment() for(goal_mapt::const_iterator it=goal_map.begin(); it!=goal_map.end(); it++, g_it++) { - if(property_map[it->first].result==property_checkert::resultt::UNKNOWN && + if((property_map.at(it->first).status==property_statust::UNKNOWN || + property_map.at(it->first).status==property_statust::NOT_CHECKED) && solver.l_get(g_it->condition).is_true()) { - property_map[it->first].result=property_checkert::resultt::FAIL; + property_map.at(it->first).status=property_statust::FAIL; if(build_error_trace) { ssa_build_goto_tracet build_goto_trace(SSA, solver.get_solver()); - build_goto_trace(property_map[it->first].error_trace); + build_goto_trace(traces[it->first]); #if 0 show_raw_countermodel( diff --git a/src/2ls/cover_goals_ext.h b/src/2ls/cover_goals_ext.h index 2e748a672..1a9e56788 100644 --- a/src/2ls/cover_goals_ext.h +++ b/src/2ls/cover_goals_ext.h @@ -13,11 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_2LS_2LS_COVER_GOALS_EXT_H #include -#include +#include #include "../ssa/local_ssa.h" #include "../ssa/unwindable_local_ssa.h" #include "../domains/incremental_solver.h" +#include "traces.h" /// Try to cover some given set of goals incrementally. This can be seen as a /// heuristic variant of SAT-based set-cover. No minimality guarantee. @@ -46,13 +47,15 @@ class cover_goals_extt:public messaget unwindable_local_SSAt &_SSA, incremental_solvert &_solver, const exprt::operandst& _loophead_selects, - property_checkert::property_mapt &_property_map, + propertiest &_property_map, + tracest &_traces, bool _spurious_check, bool _all_properties, bool _build_error_trace): SSA(_SSA), solver(_solver), property_map(_property_map), + traces(_traces), spurious_check(_spurious_check), all_properties(_all_properties), build_error_trace(_build_error_trace), @@ -111,7 +114,8 @@ class cover_goals_extt:public messaget unwindable_local_SSAt &SSA; unsigned _number_covered, _iterations; incremental_solvert &solver; - property_checkert::property_mapt &property_map; + propertiest &property_map; + tracest &traces; bool spurious_check, all_properties, build_error_trace; exprt::operandst loophead_selects; diff --git a/src/2ls/graphml_witness_ext.cpp b/src/2ls/graphml_witness_ext.cpp index 479f3f328..4feba2088 100644 --- a/src/2ls/graphml_witness_ext.cpp +++ b/src/2ls/graphml_witness_ext.cpp @@ -57,7 +57,7 @@ void graphml_witness_extt::operator()( continue; } - const graphmlt::node_indext node=add_node(cfg[i]); + const graphmlt::node_indext node=add_node(cfg[i], function_name); index_map[i]=node; } for(std::size_t i=0; ifunction); + graphml[node].invariant_scope=id2string(function_identifier); } return node; } diff --git a/src/2ls/graphml_witness_ext.h b/src/2ls/graphml_witness_ext.h index 57f30e939..6aae44908 100644 --- a/src/2ls/graphml_witness_ext.h +++ b/src/2ls/graphml_witness_ext.h @@ -30,11 +30,6 @@ class graphml_witness_extt:public graphml_witnesst void operator()(const summary_checker_baset &summary_checker); protected: - graphmlt::node_indext add_node( - std::map &loc_to_node, - goto_programt::const_targett it); - void add_edge( const graphmlt::node_indext &from, const dynamic_cfg_nodet &from_cfg_node, @@ -42,7 +37,8 @@ class graphml_witness_extt:public graphml_witnesst const dynamic_cfg_nodet &to_cfg_node); graphmlt::node_indext add_node( - const dynamic_cfg_nodet &cfg_node); + const dynamic_cfg_nodet &cfg_node, + const irep_idt &function_identifier); }; #endif // CPROVER_2LS_SUMMARIZER_GRAPHML_WITNESS_EXT_H diff --git a/src/2ls/preprocessing_util.cpp b/src/2ls/preprocessing_util.cpp index a4c53df75..a39081ab6 100644 --- a/src/2ls/preprocessing_util.cpp +++ b/src/2ls/preprocessing_util.cpp @@ -59,7 +59,8 @@ void twols_parse_optionst::propagate_constants(goto_modelt &goto_model) namespacet ns(goto_model.symbol_table); Forall_goto_functions(f_it, goto_model.goto_functions) { - constant_propagator_ait(f_it->first, f_it->second, ns); + constant_propagator_ait const_propagator(f_it->second); + const_propagator(f_it->first, f_it->second, ns); } } @@ -84,7 +85,9 @@ void twols_parse_optionst::nondet_locals(goto_modelt &goto_model) to_symbol_expr(to_code_assign(next->code).lhs())==decl.symbol()) continue; - side_effect_expr_nondett nondet(decl.symbol().type()); + side_effect_expr_nondett nondet( + decl.symbol().type(), + i_it->source_location); goto_programt::targett t=f_it->second.body.insert_after(i_it); t->make_assignment(); code_assignt c(decl.symbol(), nondet); @@ -112,13 +115,22 @@ bool twols_parse_optionst::unwind_goto_into_loop( loopst loops; Forall_goto_program_instructions(i_it, body) { - if(i_it->is_backwards_goto()) + bool is_loop_head=false; + goto_programt::targett loop_exit; + for(auto edge : i_it->incoming_edges) + { + if(edge->location_number>i_it->location_number) + { + is_loop_head=true; + loop_exit=edge; + } + } + + if(is_loop_head) { - goto_programt::targett loop_head=i_it->get_target(); - goto_programt::targett loop_exit=i_it; bool has_goto_into_loop=false; - goto_programt::targett it=loop_head; + goto_programt::targett it=i_it; if(it!=loop_exit) it++; for(; it!=loop_exit; it++) @@ -128,7 +140,7 @@ bool twols_parse_optionst::unwind_goto_into_loop( s_it!=it->incoming_edges.end(); ++s_it) { if((*s_it)->is_goto() && - (*s_it)->location_numberlocation_number) + (*s_it)->location_numberlocation_number) { has_goto_into_loop=true; result=true; @@ -141,7 +153,7 @@ bool twols_parse_optionst::unwind_goto_into_loop( if(has_goto_into_loop) { status() << "Unwinding jump into loop" << eom; - loops.push_back(loopst::value_type(++loop_exit, loop_head)); + loops.push_back(loopst::value_type(++loop_exit, i_it)); } } } @@ -152,6 +164,7 @@ bool twols_parse_optionst::unwind_goto_into_loop( goto_unwindt goto_unwind; goto_unwind.unwind( + f_it->first, body, l_it->second, l_it->first, @@ -343,10 +356,9 @@ void twols_parse_optionst::split_loopheads(goto_modelt &goto_model) // inserts the skip goto_programt::targett new_loophead= - f_it->second.body.insert_before(loophead); - new_loophead->make_skip(); - new_loophead->source_location=loophead->source_location; - new_loophead->function=i_it->function; + f_it->second.body.insert_before( + loophead, + goto_programt::make_skip(loophead->source_location)); // update jumps to loophead for(std::set::iterator j_it= @@ -372,10 +384,11 @@ void twols_parse_optionst::remove_loops_in_entry(goto_modelt &goto_model) if(f_it->second.body_available() && f_it->second.body.instructions.begin()->is_target()) { + auto insert_before=f_it->second.body.instructions.begin(); auto new_entry= - f_it->second.body.insert_before(f_it->second.body.instructions.begin()); - new_entry->function=f_it->first; - new_entry->make_skip(); + f_it->second.body.insert_before( + insert_before, + goto_programt::make_skip(insert_before->source_location)); } } } @@ -418,7 +431,7 @@ void twols_parse_optionst::add_dynamic_object_rec( if(pointed_type.id()==ID_symbol) { const symbolt type_symbol=symbol_table.lookup_ref( - to_symbol_type(pointed_type).get_identifier()); + to_struct_tag_type(pointed_type).get_identifier()); object_symbol.type=type_symbol.type; } else @@ -747,10 +760,10 @@ void make_freed_ptr_comparison_nondet( and_exprt( or_exprt( lhs_not_freed_cond, - side_effect_expr_nondett(bool_typet())), + side_effect_expr_nondett(bool_typet(), loc->source_location)), or_exprt( rhs_not_freed_cond, - side_effect_expr_nondett(bool_typet())))); + side_effect_expr_nondett(bool_typet(), loc->source_location)))); } } else if(cond.id()==ID_not) diff --git a/src/2ls/show.cpp b/src/2ls/show.cpp index 959e62e0d..cd34cde6a 100644 --- a/src/2ls/show.cpp +++ b/src/2ls/show.cpp @@ -94,7 +94,7 @@ void show_defs( ssa_value_ai); ssa_ait ssa_analysis(assignments); ssa_analysis(function_identifier, goto_function, ns); - ssa_analysis.output(ns, goto_function.body, out); + ssa_analysis.output(ns, goto_function, out); } void show_defs( diff --git a/src/2ls/summary_checker_ai.cpp b/src/2ls/summary_checker_ai.cpp index 91ea84bee..64063ec4c 100644 --- a/src/2ls/summary_checker_ai.cpp +++ b/src/2ls/summary_checker_ai.cpp @@ -12,7 +12,7 @@ Author: Peter Schrammel #include "summary_checker_ai.h" #include -property_checkert::resultt summary_checker_ait::operator()( +resultt summary_checker_ait::operator()( const goto_modelt &goto_model) { SSA_functions(goto_model, goto_model.symbol_table); @@ -30,9 +30,10 @@ property_checkert::resultt summary_checker_ait::operator()( } // properties - initialize_property_map(goto_model.goto_functions); + property_map=initialize_properties(goto_model); + set_properties_unknown(); - property_checkert::resultt result=property_checkert::resultt::UNKNOWN; + resultt result=resultt::UNKNOWN; bool finished=false; while(!finished) { @@ -54,7 +55,7 @@ property_checkert::resultt summary_checker_ait::operator()( { report_statistics(); report_preconditions(); - return property_checkert::resultt::UNKNOWN; + return resultt::UNKNOWN; } if(termination) @@ -65,13 +66,13 @@ property_checkert::resultt summary_checker_ait::operator()( #ifdef SHOW_CALLINGCONTEXTS if(options.get_bool_option("show-calling-contexts")) - return property_checkert::resultt::UNKNOWN; + return resultt::UNKNOWN; #endif result=check_properties(); report_statistics(); - if(result==property_checkert::resultt::UNKNOWN && + if(result==resultt::UNKNOWN && options.get_bool_option("values-refine") && options.get_bool_option("intervals")) { @@ -110,7 +111,7 @@ void summary_checker_ait::report_preconditions() } } -property_checkert::resultt summary_checker_ait::report_termination() +resultt summary_checker_ait::report_termination() { result() << eom; result() << "** Termination: " << eom; @@ -134,17 +135,17 @@ property_checkert::resultt summary_checker_ait::report_termination() << (!computed ? "not computed" : threeval2string(terminates)) << eom; } if(not_computed) - return property_checkert::resultt::UNKNOWN; + return resultt::UNKNOWN; if(all_terminate) - return property_checkert::resultt::PASS; + return resultt::PASS; if(one_nonterminate) { #if 0 - return property_checkert::resultt::FAIL; + return resultt::FAIL; #else // rely on nontermination checker to find counterexample - return property_checkert::resultt::UNKNOWN; + return resultt::UNKNOWN; #endif } - return property_checkert::resultt::UNKNOWN; + return resultt::UNKNOWN; } diff --git a/src/2ls/summary_checker_ai.h b/src/2ls/summary_checker_ai.h index a9e30767b..4d10e2687 100644 --- a/src/2ls/summary_checker_ai.h +++ b/src/2ls/summary_checker_ai.h @@ -24,7 +24,7 @@ class summary_checker_ait:public summary_checker_baset protected: void report_preconditions(); - property_checkert::resultt report_termination(); + resultt report_termination(); }; #endif diff --git a/src/2ls/summary_checker_base.cpp b/src/2ls/summary_checker_base.cpp index 42ae807e5..3ebc44c53 100644 --- a/src/2ls/summary_checker_base.cpp +++ b/src/2ls/summary_checker_base.cpp @@ -69,7 +69,8 @@ void summary_checker_baset::SSA_functions( } // properties - initialize_property_map(goto_model.goto_functions); + property_map=initialize_properties(goto_model); + set_properties_unknown(); } void summary_checker_baset::summarize( @@ -117,7 +118,8 @@ void summary_checker_baset::summarize( delete summarizer; } -summary_checker_baset::resultt summary_checker_baset::check_properties() + +resultt summary_checker_baset::check_properties() { // analyze all the functions for(ssa_dbt::functionst::const_iterator f_it=ssa_db.functions().begin(); @@ -141,14 +143,15 @@ summary_checker_baset::resultt summary_checker_baset::check_properties() } } - summary_checker_baset::resultt result=property_checkert::resultt::PASS; - for(property_mapt::const_iterator + resultt result=resultt::PASS; + for(propertiest::const_iterator p_it=property_map.begin(); p_it!=property_map.end(); p_it++) { - if(p_it->second.result==property_checkert::resultt::FAIL) - return property_checkert::resultt::FAIL; - if(p_it->second.result==property_checkert::resultt::UNKNOWN) - result=property_checkert::resultt::UNKNOWN; + if(p_it->second.status==property_statust::FAIL) + return resultt::FAIL; + if(p_it->second.status==property_statust::UNKNOWN || + p_it->second.status==property_statust::NOT_CHECKED) + result=resultt::UNKNOWN; } return result; @@ -206,7 +209,7 @@ void summary_checker_baset::check_properties( << "fully unwound" << eom; cover_goals_extt cover_goals( - SSA, solver, loophead_selects, property_map, + SSA, solver, loophead_selects, property_map, traces, !fully_unwound && options.get_bool_option("spurious-check"), all_properties, options.get_bool_option("trace") || @@ -232,12 +235,12 @@ void summary_checker_baset::check_properties( if(i_it->guard.is_true()) { - property_map[property_id].result=property_checkert::resultt::PASS; + property_map.at(property_id).status=property_statust::PASS; continue; } // do not recheck properties that have already been decided - if(property_map[property_id].result!=property_checkert::resultt::UNKNOWN) + if(property_map.at(property_id).status!=property_statust::UNKNOWN) continue; // TODO: some properties do not show up in initialize_property_map @@ -268,7 +271,7 @@ void summary_checker_baset::check_properties( << std::endl; #endif - property_map[property_id].location=i_it; + property_map.at(property_id).pc=i_it; cover_goals.goal_map[property_id].conjuncts.push_back(property); } } @@ -301,7 +304,7 @@ void summary_checker_baset::check_properties( it++, g_it++) { if(!g_it->covered) - property_map[it->first].result=property_checkert::resultt::PASS; + property_map.at(it->first).status=property_statust::PASS; } } @@ -361,7 +364,7 @@ void summary_checker_baset::do_show_vcc( /// countermodel is spurious exprt::operandst summary_checker_baset::get_loophead_selects( const irep_idt &function_name, - const local_SSAt &SSA, prop_convt &solver) + const local_SSAt &SSA, prop_conv_solvert &solver) { // TODO: this should be provided by unwindable_local_SSA exprt::operandst loophead_selects; @@ -497,6 +500,7 @@ bool summary_checker_baset::is_spurious( /// binary void summary_checker_baset::instrument_and_output( goto_modelt &goto_model, + ui_message_handlert &ui_message_handler, unsigned verbosity) { instrument_gotot instrument_goto(options, ssa_db, summary_db); @@ -504,8 +508,7 @@ void summary_checker_baset::instrument_and_output( if(verbosity==10) show_goto_functions( goto_model, - get_message_handler(), - ui_message_handlert::uit::PLAIN, + ui_message_handler, false); std::string filename=options.get_option("instrument-output"); status() << "Writing instrumented goto-binary " << filename << eom; diff --git a/src/2ls/summary_checker_base.h b/src/2ls/summary_checker_base.h index e4b7f3b33..20a4ccccc 100644 --- a/src/2ls/summary_checker_base.h +++ b/src/2ls/summary_checker_base.h @@ -12,8 +12,10 @@ Author: Peter Schrammel #ifndef CPROVER_2LS_2LS_SUMMARY_CHECKER_BASE_H #define CPROVER_2LS_2LS_SUMMARY_CHECKER_BASE_H -#include #include +#include +#include +#include #include #include @@ -23,10 +25,12 @@ Author: Peter Schrammel #include #include "cover_goals_ext.h" +#include "traces.h" class graphml_witness_extt; -class summary_checker_baset:public property_checkert + +class summary_checker_baset:public messaget { public: summary_checker_baset( @@ -48,14 +52,22 @@ class summary_checker_baset:public property_checkert virtual resultt operator()(const goto_modelt &) { assert(false); } - void instrument_and_output(goto_modelt &goto_model, unsigned verbosity); + void instrument_and_output( + goto_modelt &goto_model, + ui_message_handlert &ui_message_handler, + unsigned verbosity); void set_message_handler(message_handlert &_message_handler) override { messaget::set_message_handler(_message_handler); ssa_inliner.set_message_handler(_message_handler); + ssa_db.set_message_handler(_message_handler); } + propertiest property_map; + + tracest traces; + protected: optionst &options; @@ -84,14 +96,14 @@ class summary_checker_baset:public property_checkert bool forward=true, bool termination=false); - property_checkert::resultt check_properties(); + resultt check_properties(); virtual void check_properties( const ssa_dbt::functionst::const_iterator f_it); exprt::operandst get_loophead_selects( const irep_idt &function_name, const local_SSAt &, - prop_convt &); + prop_conv_solvert &); bool is_spurious( const exprt::operandst& loophead_selects, incremental_solvert&); @@ -104,6 +116,17 @@ class summary_checker_baset:public property_checkert const exprt::operandst& loophead_selects, incremental_solvert&); + // FIXME: This is a backwards-compatible hack. CPROVER introduced property + // status NOT_CHECKED (previously there was only UNKNOWN). Adjust + // 2LS to also differentiate between unknown properties and properties + // that were not checked at all. + inline void set_properties_unknown() + { + for(auto &property : property_map) + if(property.second.status==property_statust::NOT_CHECKED) + property.second.status=property_statust::UNKNOWN; + } + friend graphml_witness_extt; }; diff --git a/src/2ls/summary_checker_bmc.cpp b/src/2ls/summary_checker_bmc.cpp index f26e4cb54..d398af9d8 100644 --- a/src/2ls/summary_checker_bmc.cpp +++ b/src/2ls/summary_checker_bmc.cpp @@ -12,14 +12,14 @@ Author: Peter Schrammel #include "summary_checker_bmc.h" -property_checkert::resultt summary_checker_bmct::operator()( +resultt summary_checker_bmct::operator()( const goto_modelt &goto_model) { SSA_functions(goto_model, goto_model.symbol_table); ssa_unwinder.init(false, true); - property_checkert::resultt result=property_checkert::resultt::UNKNOWN; + resultt result=resultt::UNKNOWN; unsigned max_unwind=options.get_unsigned_int_option("unwind"); status() << "Max-unwind is " << max_unwind << eom; ssa_unwinder.init_localunwinders(); @@ -30,13 +30,13 @@ property_checkert::resultt summary_checker_bmct::operator()( summary_db.mark_recompute_all(); ssa_unwinder.unwind_all(unwind); result=check_properties(); - if(result==property_checkert::resultt::PASS) + if(result==resultt::PASS) { status() << "incremental BMC proof found after " << unwind << " unwinding(s)" << messaget::eom; break; } - else if(result==property_checkert::resultt::FAIL) + else if(result==resultt::FAIL) { status() << "incremental BMC counterexample found after " << unwind << " unwinding(s)" << messaget::eom; diff --git a/src/2ls/summary_checker_kind.cpp b/src/2ls/summary_checker_kind.cpp index aee19e83d..07a168446 100644 --- a/src/2ls/summary_checker_kind.cpp +++ b/src/2ls/summary_checker_kind.cpp @@ -11,14 +11,14 @@ Author: Peter Schrammel #include "summary_checker_kind.h" -property_checkert::resultt summary_checker_kindt::operator()( +resultt summary_checker_kindt::operator()( const goto_modelt &goto_model) { SSA_functions(goto_model, goto_model.symbol_table); ssa_unwinder.init(true, false); - property_checkert::resultt result=property_checkert::resultt::UNKNOWN; + resultt result=resultt::UNKNOWN; unsigned max_unwind=options.get_unsigned_int_option("unwind"); unsigned give_up_invariants= options.get_unsigned_int_option("give-up-invariants"); @@ -38,21 +38,20 @@ property_checkert::resultt summary_checker_kindt::operator()( bool magic_limit_not_reached= unwind -property_checkert::resultt summary_checker_nontermt::operator()( +resultt summary_checker_nontermt::operator()( const goto_modelt &goto_model) { SSA_functions(goto_model, goto_model.symbol_table); ssa_unwinder.init(false, true); - property_checkert::resultt result=property_checkert::resultt::UNKNOWN; + resultt result=resultt::UNKNOWN; unsigned max_unwind=options.get_unsigned_int_option("unwind"); status() << "Max-unwind is " << max_unwind << eom; ssa_unwinder.init_localunwinders(); @@ -38,14 +38,14 @@ property_checkert::resultt summary_checker_nontermt::operator()( if(unwind==51) // use a different nontermination technique { result=check_nonterm_linear(); - if(result==property_checkert::resultt::PASS) + if(result==resultt::PASS) { status() << "Termination proved after " << unwind << " unwinding(s)" << messaget::eom; report_statistics(); return result; } - else if(result==property_checkert::resultt::FAIL) + else if(result==resultt::FAIL) { status() << "Nonterminating program execution proved after " << unwind << " unwinding(s)" << messaget::eom; @@ -54,13 +54,13 @@ property_checkert::resultt summary_checker_nontermt::operator()( } } result=summary_checker_baset::check_properties(); - if(result==property_checkert::resultt::PASS) + if(result==resultt::PASS) { status() << "Termination proved after " << unwind << " unwinding(s)" << messaget::eom; break; } - else if(result==property_checkert::resultt::FAIL) + else if(result==resultt::FAIL) { status() << "Nonterminating program execution proved after " << unwind << " unwinding(s)" << messaget::eom; @@ -106,6 +106,7 @@ void summary_checker_nontermt::check_properties( solver, loophead_selects, property_map, + traces, false, false, options.get_bool_option("trace") || @@ -122,7 +123,7 @@ void summary_checker_nontermt::check_properties( if(n_it->loophead!=SSA.nodes.end()) // we've found a loop { irep_idt property_id( - id2string(n_it->location->function)+"."+ + id2string(SSA.function_identifier)+"."+ std::to_string(n_it->location->loop_number)+".term"); exprt lsguard= @@ -159,8 +160,10 @@ void summary_checker_nontermt::check_properties( SSA.name(*o_it, local_SSAt::PHI, n_it->loophead->location); ssa_local_unwinder.unwinder_rename(post_var, *n_it->loophead, false); - symbol_exprt phi_var; - phi_var=SSA.name(*o_it, local_SSAt::PHI, n_it->loophead->location); + symbol_exprt phi_var=SSA.name( + *o_it, + local_SSAt::PHI, + n_it->loophead->location); ssa_local_unwinder.unwinder_rename(phi_var, *n_it->loophead, true); loop_vars.push_back(equal_exprt(post_var, phi_var)); } @@ -169,8 +172,12 @@ void summary_checker_nontermt::check_properties( } SSA.current_unwinding=store_unwinding; - property_map[property_id].location=n_it->loophead->location; - property_map[property_id].result=property_checkert::resultt::UNKNOWN; + property_map.insert({ + property_id, + property_infot( + n_it->loophead->location, + "assertion", + property_statust::UNKNOWN)}); cover_goals.goal_map[property_id].conjuncts.push_back( disjunction(loop_check_operands)); ls_guards.push_back(not_exprt(lsguard)); @@ -251,7 +258,7 @@ void summary_checker_nontermt::check_properties_linear( loop_counter++; irep_idt property_id( - id2string(n_it->location->function)+"."+ + id2string(SSA.function_identifier)+"."+ std::to_string(n_it->location->loop_number)+".term"); const ssa_domaint::phi_nodest &phi_nodes= @@ -273,8 +280,12 @@ void summary_checker_nontermt::check_properties_linear( exprt::operandst loop_exit_cond; exprt::operandst neg_loop_exit_cond; - property_map[property_id].location=n_it->loophead->location; - property_map[property_id].result=property_checkert::resultt::UNKNOWN; + property_map.insert({ + property_id, + property_infot( + n_it->loophead->location, + "assertion", + property_statust::UNKNOWN)}); unsigned const_number=0; for(local_SSAt::objectst::const_iterator @@ -290,12 +301,16 @@ void summary_checker_nontermt::check_properties_linear( // first linearity check data preparation SSA.current_unwinding-=1; - symbol_exprt phi_var1; - phi_var1=SSA.name(*o_it, local_SSAt::PHI, n_it->loophead->location); + symbol_exprt phi_var1=SSA.name( + *o_it, + local_SSAt::PHI, + n_it->loophead->location); ssa_local_unwinder.unwinder_rename(phi_var1, *n_it->loophead, true); SSA.current_unwinding+=1; - symbol_exprt phi_var2; - phi_var2=SSA.name(*o_it, local_SSAt::PHI, n_it->loophead->location); + symbol_exprt phi_var2=SSA.name( + *o_it, + local_SSAt::PHI, + n_it->loophead->location); ssa_local_unwinder.unwinder_rename(phi_var2, *n_it->loophead, true); // works only for bitvectors @@ -545,7 +560,7 @@ void summary_checker_nontermt::check_properties_linear( case decision_proceduret::resultt::D_SATISFIABLE: // found nontermination - property_map[property_id].result=property_checkert::resultt::FAIL; + property_map.at(property_id).status=property_statust::FAIL; solver.pop_context(); solver.pop_context(); return; @@ -561,7 +576,7 @@ void summary_checker_nontermt::check_properties_linear( solver.pop_context(); } -summary_checker_baset::resultt summary_checker_nontermt::check_nonterm_linear() +resultt summary_checker_nontermt::check_nonterm_linear() { // analyze all the functions for(ssa_dbt::functionst::const_iterator f_it=ssa_db.functions().begin(); @@ -572,14 +587,15 @@ summary_checker_baset::resultt summary_checker_nontermt::check_nonterm_linear() check_properties_linear(f_it); } - summary_checker_baset::resultt result=property_checkert::resultt::PASS; - for(property_mapt::const_iterator + resultt result=resultt::PASS; + for(propertiest::const_iterator p_it=property_map.begin(); p_it!=property_map.end(); p_it++) { - if(p_it->second.result==property_checkert::resultt::FAIL) - return property_checkert::resultt::FAIL; - if(p_it->second.result==property_checkert::resultt::UNKNOWN) - result=property_checkert::resultt::UNKNOWN; + if(p_it->second.status==property_statust::FAIL) + return resultt::FAIL; + if(p_it->second.status==property_statust::UNKNOWN || + p_it->second.status==property_statust::NOT_CHECKED) + result=resultt::UNKNOWN; } return result; diff --git a/src/2ls/summary_checker_nonterm.h b/src/2ls/summary_checker_nonterm.h index 21695dc32..4122d74cd 100644 --- a/src/2ls/summary_checker_nonterm.h +++ b/src/2ls/summary_checker_nonterm.h @@ -31,7 +31,7 @@ class summary_checker_nontermt:public summary_checker_baset const ssa_dbt::functionst::const_iterator f_it); protected: - summary_checker_baset::resultt check_nonterm_linear(); + resultt check_nonterm_linear(); }; #endif // CPROVER_2LS_2LS_SUMMARY_CHECKER_NONTERM_H diff --git a/src/2ls/traces.h b/src/2ls/traces.h new file mode 100644 index 000000000..a3a45e664 --- /dev/null +++ b/src/2ls/traces.h @@ -0,0 +1,17 @@ +/*******************************************************************\ + +Module: GOTO traces + +Author: František Nečas + +\*******************************************************************/ + +/// \file +/// GOTO traces + +#ifndef CPROVER_2LS_2LS_TYPES_H +#define CPROVER_2LS_2LS_TYPES_H + +typedef std::unordered_map tracest; + +#endif diff --git a/src/2ls/version.h b/src/2ls/version.h index 987421874..6cd470f30 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.5" +#define TWOLS_VERSION "0.9.6" #endif diff --git a/src/domains/heap_domain.cpp b/src/domains/heap_domain.cpp index 05327ed6f..07089ea41 100644 --- a/src/domains/heap_domain.cpp +++ b/src/domains/heap_domain.cpp @@ -13,6 +13,7 @@ Author: Viktor Malik #include #include #include +#include /// Initialize abstract value. Clears value with empty value rows corresponding /// to template. diff --git a/src/domains/incremental_solver.cpp b/src/domains/incremental_solver.cpp index 09ba49a73..5c8fbcb8d 100644 --- a/src/domains/incremental_solver.cpp +++ b/src/domains/incremental_solver.cpp @@ -29,22 +29,9 @@ void incremental_solvert::new_context() #endif #else - - literalt activation_literal= - solver->convert( - symbol_exprt( - "goto_symex::\\act$"+ - std::to_string(activation_literal_counter++), bool_typet())); - + solver->push(); #ifdef DEBUG_OUTPUT - debug() << "new context: " << activation_literal<< eom; -#endif - - activation_literals.push_back(activation_literal); - solver->set_assumptions(activation_literals); - -#if 0 - return !activation_literals.back(); // not to be used anymore + debug() << "new context" << eom; #endif #endif } @@ -62,45 +49,10 @@ void incremental_solvert::pop_context() #else - assert(!activation_literals.empty()); - literalt activation_literal=activation_literals.back(); - activation_literals.pop_back(); -#ifndef DEBUG_FORMULA - solver->set_to_false(literal_exprt(activation_literal)); -#else - formula.push_back(!activation_literal); -#endif - + solver->pop(); #ifdef DEBUG_OUTPUT - debug() << "pop context: " << activation_literal << eom; + debug() << "pop context" << eom; #endif - - solver->set_assumptions(activation_literals); -#endif -} - -void incremental_solvert::make_context_permanent() -{ -#ifdef NON_INCREMENTAL - assert(contexts.size()>=2); - contextst::iterator c_it=contexts.end(); c_it--; c_it--; - c_it->insert(c_it->end(), contexts.back().begin(), contexts.back().end()); - contexts.pop_back(); -#else - assert(!activation_literals.empty()); - literalt activation_literal=activation_literals.back(); - activation_literals.pop_back(); -#ifndef DEBUG_FORMULA - solver->set_to_true(literal_exprt(activation_literal)); -#else - formula.push_back(activation_literal); -#endif - -#ifdef DEBUG_OUTPUT - debug() << "make context permanent: " << activation_literal<< eom; -#endif - - solver->set_assumptions(activation_literals); #endif } diff --git a/src/domains/incremental_solver.h b/src/domains/incremental_solver.h index 3f1704448..8ea0f452c 100644 --- a/src/domains/incremental_solver.h +++ b/src/domains/incremental_solver.h @@ -37,7 +37,9 @@ class incremental_solvert:public messaget explicit incremental_solvert( const namespacet &_ns, + message_handlert &_message_handler, bool _arith_refinement=false): + messaget(_message_handler), sat_check(NULL), solver(NULL), ns(_ns), @@ -110,32 +112,32 @@ class incremental_solvert:public messaget static incremental_solvert *allocate( const namespacet &_ns, + message_handlert &_message_handler, bool arith_refinement=false) { - return new incremental_solvert(_ns, arith_refinement); + return new incremental_solvert(_ns, _message_handler, arith_refinement); } inline prop_convt & get_solver() { return *solver; } propt *sat_check; - prop_convt *solver; + prop_conv_solvert *solver; const namespacet &ns; void new_context(); void pop_context(); - void make_context_permanent(); // for debugging bvt formula; void debug_add_to_formula(const exprt &expr); - // context assumption literals - bvt activation_literals; - // non-incremental solving contextst contexts; protected: +#ifndef DEBUG + null_message_handlert null_message_handler; +#endif unsigned activation_literal_counter; unsigned domain_number; // ids for each domain instance to make symbols unique bool arith_refinement; @@ -145,7 +147,11 @@ class incremental_solvert:public messaget void allocate_solvers(bool arith_refinement) { - sat_check=new satcheckt(); +#ifdef DEBUG + sat_check=new satcheckt(get_message_handler()); +#else + sat_check=new satcheckt(null_message_handler); +#endif #if 0 sat_check=new satcheck_minisat_no_simplifiert(); #endif @@ -189,11 +195,7 @@ static inline incremental_solvert &operator<<( dest.contexts.back().push_back(src); #else #ifndef DEBUG_FORMULA - if(!dest.activation_literals.empty()) - *dest.solver << - or_exprt(src, literal_exprt(!dest.activation_literals.back())); - else - *dest.solver << src; + *dest.solver << src; #else if(!dest.activation_literals.empty()) { diff --git a/src/domains/lexlinrank_domain.cpp b/src/domains/lexlinrank_domain.cpp index 1d23cdfa6..f5a86c05a 100644 --- a/src/domains/lexlinrank_domain.cpp +++ b/src/domains/lexlinrank_domain.cpp @@ -43,7 +43,7 @@ void lexlinrank_domaint::initialize_value(domaint::valuet &value) void lexlinrank_domaint::initialize() { delete inner_solver; - inner_solver=incremental_solvert::allocate(ns); + inner_solver=incremental_solvert::allocate(ns, message_handler); } bool lexlinrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved) @@ -133,7 +133,7 @@ bool lexlinrank_domaint::edit_row(const rowt &row, valuet &inv, bool improved) { number_elements_per_row[row]++; delete inner_solver; - inner_solver=incremental_solvert::allocate(ns); + inner_solver=incremental_solvert::allocate(ns, message_handler); reset_refinements(); rank[row].add_element(); diff --git a/src/domains/lexlinrank_domain.h b/src/domains/lexlinrank_domain.h index f22a925ae..3c113f0bf 100644 --- a/src/domains/lexlinrank_domain.h +++ b/src/domains/lexlinrank_domain.h @@ -102,14 +102,16 @@ class lexlinrank_domaint:public simple_domaint replace_mapt &_renaming_map, unsigned _max_elements, // lexicographic components unsigned _max_inner_iterations, - const namespacet &_ns): + const namespacet &_ns, + message_handlert &_message_handler): simple_domaint(_domain_number, _renaming_map, _ns), refinement_level(0), max_elements(_max_elements), max_inner_iterations(_max_inner_iterations), - number_inner_iterations(0) + number_inner_iterations(0), + message_handler(_message_handler) { - inner_solver=incremental_solvert::allocate(_ns); + inner_solver=incremental_solvert::allocate(_ns, _message_handler); } @@ -162,6 +164,7 @@ class lexlinrank_domaint:public simple_domaint const unsigned max_inner_iterations; incremental_solvert *inner_solver; unsigned number_inner_iterations; + message_handlert &message_handler; std::vector number_elements_per_row; }; diff --git a/src/domains/linrank_domain.h b/src/domains/linrank_domain.h index 2a3aaeb61..9bdd39293 100644 --- a/src/domains/linrank_domain.h +++ b/src/domains/linrank_domain.h @@ -79,14 +79,16 @@ class linrank_domaint:public simple_domaint replace_mapt &_renaming_map, unsigned _max_elements, // lexicographic components unsigned _max_inner_iterations, - const namespacet &_ns): + const namespacet &_ns, + message_handlert &_message_handler): simple_domaint(_domain_number, _renaming_map, _ns), refinement_level(0), max_elements(_max_elements), max_inner_iterations(_max_inner_iterations), - number_inner_iterations(0) + number_inner_iterations(0), + message_handler(_message_handler) { - inner_solver=incremental_solvert::allocate(_ns); + inner_solver=incremental_solvert::allocate(_ns, _message_handler); } // initialize value @@ -132,6 +134,7 @@ class linrank_domaint:public simple_domaint const unsigned max_inner_iterations; incremental_solvert *inner_solver; unsigned number_inner_iterations; + message_handlert &message_handler; }; #endif // CPROVER_2LS_DOMAINS_LINRANK_DOMAIN_H diff --git a/src/domains/predabs_domain.cpp b/src/domains/predabs_domain.cpp index 77e695037..2f804b08e 100644 --- a/src/domains/predabs_domain.cpp +++ b/src/domains/predabs_domain.cpp @@ -30,7 +30,7 @@ void predabs_domaint::initialize_value(domaint::valuet &value) for(std::size_t row=0; row { void set_row_value(rowt row, const constant_exprt &value) { - (*this)[row]=value; + (*this)[row]=row_valuet(value); } exprt get_row_expr(rowt row, const template_rowt &templ_row) const override diff --git a/src/domains/strategy_solver_binsearch2.cpp b/src/domains/strategy_solver_binsearch2.cpp index 04492db6a..6f15e7817 100644 --- a/src/domains/strategy_solver_binsearch2.cpp +++ b/src/domains/strategy_solver_binsearch2.cpp @@ -91,10 +91,12 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv) debug() << "improve row " << row << eom; #endif improve_rows.insert(row); - symb_values[row]=tpolyhedra_domain.get_row_symb_value(row); - lower_values[row]= + symb_values.insert({row, tpolyhedra_domain.get_row_symb_value(row)}); + lower_values.insert({ + row, simplify_const( - solver.get(tpolyhedra_domain.strategy_value_exprs[row][0])); + solver.get( + tpolyhedra_domain.strategy_value_exprs[row][0]))}); blocking_constraint.push_back( literal_exprt(!tpolyhedra_domain.strategy_cond_literals[row])); if(inv[row].is_neg_inf()) @@ -122,12 +124,12 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv) assert(lower_values.size()>=1); std::map::iterator it=symb_values.begin(); - exprt _lower=lower_values[it->first]; + exprt _lower=lower_values.at(it->first); #if 1 debug() << "update row " << it->first << ": " - << from_expr(SSA.ns, "", lower_values[it->first]) << eom; + << from_expr(SSA.ns, "", lower_values.at(it->first)) << eom; #endif - inv[it->first]=lower_values[it->first]; + inv[it->first]=lower_values.at(it->first); exprt _upper= tpolyhedra_domain.get_max_row_value(it->first); exprt sum=it->second; @@ -135,13 +137,13 @@ bool strategy_solver_binsearch2t::iterate(invariantt &_inv) { sum=plus_exprt(sum, it->second); _upper=plus_exprt(_upper, tpolyhedra_domain.get_max_row_value(it->first)); - _lower=plus_exprt(_lower, lower_values[it->first]); + _lower=plus_exprt(_lower, lower_values.at(it->first)); #if 1 debug() << "update row " << it->first << ": " - << from_expr(SSA.ns, "", lower_values[it->first]) << eom; + << from_expr(SSA.ns, "", lower_values.at(it->first)) << eom; #endif - inv[it->first]=lower_values[it->first]; + inv[it->first]=lower_values.at(it->first); } // do not solve system if we have just reached a new loop diff --git a/src/domains/strategy_solver_binsearch3.cpp b/src/domains/strategy_solver_binsearch3.cpp index 2eeed8bbe..8e6a2fa27 100644 --- a/src/domains/strategy_solver_binsearch3.cpp +++ b/src/domains/strategy_solver_binsearch3.cpp @@ -86,10 +86,12 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv) debug() << "improve row " << row << eom; #endif improve_rows.insert(row); - symb_values[row]=tpolyhedra_domain.get_row_symb_value(row); - lower_values[row]= + symb_values.insert({row, tpolyhedra_domain.get_row_symb_value(row)}); + lower_values.insert({ + row, simplify_const( - solver.get(tpolyhedra_domain.strategy_value_exprs[row][0])); + solver.get( + tpolyhedra_domain.strategy_value_exprs[row][0]))}); blocking_constraint.push_back( literal_exprt(!tpolyhedra_domain.strategy_cond_literals[row])); if(inv[row].is_neg_inf()) @@ -117,12 +119,12 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv) assert(lower_values.size()>=1); std::map::iterator it=symb_values.begin(); - exprt _lower=lower_values[it->first]; + exprt _lower=lower_values.at(it->first); #if 1 debug() << "update row " << it->first << ": " - << from_expr(SSA.ns, "", lower_values[it->first]) << eom; + << from_expr(SSA.ns, "", lower_values.at(it->first)) << eom; #endif - inv[it->first]=lower_values[it->first]; + inv[it->first]=lower_values.at(it->first); exprt _upper= tpolyhedra_domain.get_max_row_value(it->first); exprt sum=it->second; @@ -130,13 +132,13 @@ bool strategy_solver_binsearch3t::iterate(invariantt &_inv) { sum=plus_exprt(sum, it->second); _upper=plus_exprt(_upper, tpolyhedra_domain.get_max_row_value(it->first)); - _lower=plus_exprt(_lower, lower_values[it->first]); + _lower=plus_exprt(_lower, lower_values.at(it->first)); #if 1 debug() << "update row " << it->first << ": " - << from_expr(SSA.ns, "", lower_values[it->first]) << eom; + << from_expr(SSA.ns, "", lower_values.at(it->first)) << eom; #endif - inv[it->first]=lower_values[it->first]; + inv[it->first]=lower_values.at(it->first); } // do not solve system if we have just reached a new loop diff --git a/src/domains/template_generator_base.cpp b/src/domains/template_generator_base.cpp index bde9917f6..446636134 100644 --- a/src/domains/template_generator_base.cpp +++ b/src/domains/template_generator_base.cpp @@ -58,13 +58,12 @@ void template_generator_baset::get_pre_post_guards( post_guard=and_exprt(pguard, pcond); } -void template_generator_baset::get_pre_var( +symbol_exprt template_generator_baset::get_pre_var( const local_SSAt &SSA, local_SSAt::objectst::const_iterator o_it, - local_SSAt::nodest::const_iterator n_it, - symbol_exprt &pre_var) + local_SSAt::nodest::const_iterator n_it) { - pre_var=SSA.name(*o_it, local_SSAt::LOOP_BACK, n_it->location); + symbol_exprt pre_var=SSA.name(*o_it, local_SSAt::LOOP_BACK, n_it->location); ssa_local_unwinder.unwinder_rename(pre_var, *n_it, true); symbol_exprt post_var=SSA.read_rhs(*o_it, n_it->location); @@ -73,6 +72,7 @@ void template_generator_baset::get_pre_var( rename_aux_post(post_var); aux_renaming_map[pre_var]=post_var; + return pre_var; } /// supposes that loop head PHIs are of the form xphi=gls?xlb:x0 @@ -149,8 +149,7 @@ void template_generator_baset::collect_variables_loop( } } - symbol_exprt pre_var; - get_pre_var(SSA, o_it, n_it, pre_var); + symbol_exprt pre_var=get_pre_var(SSA, o_it, n_it); // For fields of dynamic objects, we add a guard that their value is not // equal to the corresponding input SSA variable that represents a state @@ -282,8 +281,10 @@ void template_generator_baset::add_var( if(var.type().id()==ID_array && options.get_bool_option("arrays")) { const array_typet &array_type=to_array_type(var.type()); + if(!array_type.size().is_constant()) + return; mp_integer size; - to_integer(array_type.size(), size); + to_integer(to_constant_expr(array_type.size()), size); for(mp_integer i=0; iget_identifier()).find("dynamic_object$")!= std::string::npos) { diff --git a/src/domains/template_generator_ranking.cpp b/src/domains/template_generator_ranking.cpp index 33e53bbcb..ca490bb09 100644 --- a/src/domains/template_generator_ranking.cpp +++ b/src/domains/template_generator_ranking.cpp @@ -38,7 +38,8 @@ void template_generator_rankingt::operator()( post_renaming_map, options.get_unsigned_int_option("lexicographic-ranking-function"), options.get_unsigned_int_option("max-inner-ranking-iterations"), - SSA.ns)); + SSA.ns, + get_message_handler())); } else { @@ -48,7 +49,8 @@ void template_generator_rankingt::operator()( post_renaming_map, options.get_unsigned_int_option("lexicographic-ranking-function"), options.get_unsigned_int_option("max-inner-ranking-iterations"), - SSA.ns)); + SSA.ns, + get_message_handler())); } collect_variables_ranking(SSA, forward); diff --git a/src/domains/template_generator_summary.cpp b/src/domains/template_generator_summary.cpp index fba9f9f91..0f83345a7 100644 --- a/src/domains/template_generator_summary.cpp +++ b/src/domains/template_generator_summary.cpp @@ -36,8 +36,7 @@ void template_generator_summaryt::operator()( collect_variables_loop(SSA, forward); // do not compute summary for entry-point - if(SSA.goto_function.body.instructions.front().function!= - goto_functionst::entry_point() || + if(SSA.function_identifier!=goto_functionst::entry_point() || options.get_bool_option("preconditions")) collect_variables_inout(SSA, forward); diff --git a/src/domains/tpolyhedra_domain.h b/src/domains/tpolyhedra_domain.h index 2cf90f1c0..f09bb9642 100644 --- a/src/domains/tpolyhedra_domain.h +++ b/src/domains/tpolyhedra_domain.h @@ -37,7 +37,7 @@ class tpolyhedra_domaint:public simple_domaint /// Row value (parameter) is a constant struct row_valuet:constant_exprt { - row_valuet()=default; + row_valuet(): constant_exprt(false_exprt()) {} explicit row_valuet(const constant_exprt &value) : constant_exprt(value) {} using constant_exprt::operator=; diff --git a/src/domains/util.cpp b/src/domains/util.cpp index 9cd8e53c0..9604ee330 100644 --- a/src/domains/util.cpp +++ b/src/domains/util.cpp @@ -190,7 +190,7 @@ mp_integer simplify_const_int(const exprt &expr) if(expr.id()==ID_constant) { mp_integer v; - to_integer(expr, v); + to_integer(to_constant_expr(expr), v); return v; } if(expr.id()==ID_typecast) @@ -227,7 +227,7 @@ mp_integer simplify_const_int(const exprt &expr) if(array_type.id()==ID_signedbv || array_type.id()==ID_unsignedbv) { mp_integer mp_index=simplify_const_int(index_expr.index()); - unsigned index=integer2unsigned(mp_index); // TODO: might overflow + auto index=numeric_cast_v(mp_index); // TODO: might overflow assert(index<(index_expr.array().operands().size())); return simplify_const_int(index_expr.array().operands()[index]); } @@ -308,7 +308,7 @@ ieee_floatt simplify_const_float(const exprt &expr) if(array_type.id()==ID_float) { mp_integer mp_index=simplify_const_int(index_expr.index()); - unsigned index=integer2unsigned(mp_index); // TODO: might overflow + auto index=numeric_cast_v(mp_index); // TODO: might overflow assert(index<(index_expr.array().operands().size())); return simplify_const_float(index_expr.array().operands()[index]); } diff --git a/src/solver/summarizer_fw_contexts.cpp b/src/solver/summarizer_fw_contexts.cpp index 38b458f5c..207db791f 100644 --- a/src/solver/summarizer_fw_contexts.cpp +++ b/src/solver/summarizer_fw_contexts.cpp @@ -18,7 +18,8 @@ Author: Peter Schrammel #include #include -#include +#include +#include #include "summarizer_fw_contexts.h" #include "summary_db.h" diff --git a/src/solver/summarizer_fw_contexts.h b/src/solver/summarizer_fw_contexts.h index 6651d186d..06aa042eb 100644 --- a/src/solver/summarizer_fw_contexts.h +++ b/src/solver/summarizer_fw_contexts.h @@ -14,7 +14,7 @@ Author: Peter Schrammel #include #include -#include +#include #include #include @@ -48,7 +48,7 @@ class summarizer_fw_contextst:public summarizer_fwt virtual void summarize(); protected: - language_uit::uit ui; // use gui format + ui_message_handlert::uit ui; // use gui format std::set excluded_functions; virtual void inline_summaries( diff --git a/src/ssa/address_canonizer.cpp b/src/ssa/address_canonizer.cpp index 413b6bf64..b391c5b91 100644 --- a/src/ssa/address_canonizer.cpp +++ b/src/ssa/address_canonizer.cpp @@ -40,22 +40,23 @@ exprt address_canonizer( else if(object.id()==ID_member) { // get offset - exprt offset=member_offset_expr(to_member_expr(object), ns); - - // &x.m ---> (&x)+offset - - address_of_exprt address_of_expr(to_member_expr(object).struct_op()); - exprt rec_result=address_canonizer(address_of_expr, ns); // rec. call - - pointer_typet byte_pointer( - unsigned_char_type(), - config.ansi_c.pointer_width); - typecast_exprt typecast_expr(rec_result, byte_pointer); - plus_exprt sum(typecast_expr, offset); - if(sum.type()!=address.type()) - sum.make_typecast(address.type()); - - return sum; + if(auto maybe_offset=member_offset_expr(to_member_expr(object), ns)) + { + // &x.m ---> (&x)+offset + + address_of_exprt address_of_expr(to_member_expr(object).struct_op()); + exprt rec_result=address_canonizer(address_of_expr, ns); // rec. call + + pointer_typet byte_pointer( + unsigned_char_type(), + config.ansi_c.pointer_width); + typecast_exprt typecast_expr(rec_result, byte_pointer); + exprt result=plus_exprt(typecast_expr, *maybe_offset); + if(result.type()!=address.type()) + result=typecast_exprt(result, address.type()); + + return result; + } } else if(object.id()==ID_index) { @@ -65,11 +66,11 @@ exprt address_canonizer( pointer_typet pointer_type(object.type(), config.ansi_c.pointer_width); typecast_exprt typecast_expr(rec_result, pointer_type); - plus_exprt sum(typecast_expr, to_index_expr(object).index()); - if(sum.type()!=address.type()) - sum.make_typecast(address.type()); + exprt result=plus_exprt(typecast_expr, to_index_expr(object).index()); + if(result.type()!=address.type()) + result=typecast_exprt(result, address.type()); - return sum; + return result; } else return address; diff --git a/src/ssa/dynobj_instance_analysis.cpp b/src/ssa/dynobj_instance_analysis.cpp index c1bf1976a..fe88f9e2e 100644 --- a/src/ssa/dynobj_instance_analysis.cpp +++ b/src/ssa/dynobj_instance_analysis.cpp @@ -262,3 +262,11 @@ void dynobj_instance_domaint::output( out << "\n"; } } + +void dynobj_instance_analysist::initialize( + const irep_idt &function_id, + const goto_programt &goto_program) +{ + forall_goto_program_instructions(i_it, goto_program) + get_state(i_it).make_bottom(); +} diff --git a/src/ssa/dynobj_instance_analysis.h b/src/ssa/dynobj_instance_analysis.h index c47017228..0521bb0c1 100644 --- a/src/ssa/dynobj_instance_analysis.h +++ b/src/ssa/dynobj_instance_analysis.h @@ -144,6 +144,8 @@ class must_alias_setst class dynobj_instance_domaint:public ai_domain_baset { public: + dynobj_instance_domaint(): has_values(false) {} + // Must-alias relation for each dynamic object (corresponding to allocation // site). std::map must_alias_relations; @@ -224,6 +226,9 @@ class dynobj_instance_analysist:public ait protected: const optionst &options; ssa_value_ait &value_analysis; + void initialize( + const irep_idt &function_id, + const goto_programt &goto_program) override; friend class dynobj_instance_domaint; }; diff --git a/src/ssa/local_ssa.cpp b/src/ssa/local_ssa.cpp index 4ee061c81..eb5d333a1 100644 --- a/src/ssa/local_ssa.cpp +++ b/src/ssa/local_ssa.cpp @@ -18,8 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include +#include #include @@ -83,7 +83,7 @@ void local_SSAt::get_entry_exit_vars() // get globals out (includes return value) goto_programt::const_targett last=goto_function.body.instructions.end(); last--; - get_globals(last, globals_out, true, true, last->function); + get_globals(last, globals_out, true, true, function_identifier); } void local_SSAt::get_globals( diff --git a/src/ssa/malloc_ssa.cpp b/src/ssa/malloc_ssa.cpp index 37ba76584..72757e32a 100644 --- a/src/ssa/malloc_ssa.cpp +++ b/src/ssa/malloc_ssa.cpp @@ -23,7 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "malloc_ssa.h" -inline static typet c_sizeof_type_rec(const exprt &expr) +inline static optionalt c_sizeof_type_rec(const exprt &expr) { const irept &sizeof_type=expr.find(ID_C_c_sizeof_type); @@ -35,13 +35,11 @@ inline static typet c_sizeof_type_rec(const exprt &expr) { forall_operands(it, expr) { - typet t=c_sizeof_type_rec(*it); - if(t.is_not_nil()) - return t; + if(auto maybe_t=c_sizeof_type_rec(*it)) + return maybe_t; } } - - return nil_typet(); + return {}; } /// Create new dynamic object, insert it into the symbol table and return its @@ -68,9 +66,10 @@ exprt create_dynamic_object( if(type.id()==ID_array) { object_type=value_symbol.type.subtype(); - index_exprt index_expr(value_symbol.type.subtype()); - index_expr.array()=value_symbol.symbol_expr(); - index_expr.index()=from_integer(0, index_type()); + index_exprt index_expr( + value_symbol.symbol_expr(), + from_integer(0, index_type()), + value_symbol.type.subtype()); object=index_expr; } else @@ -136,7 +135,7 @@ exprt malloc_ssa( namespacet ns(symbol_table); exprt size=code.op0(); - typet object_type=nil_typet(); + optionalt object_type; { // special treatment for sizeof(T)*x @@ -144,43 +143,46 @@ exprt malloc_ssa( size.operands().size()==2 && size.op0().find(ID_C_c_sizeof_type).is_not_nil()) { - object_type=array_typet( - c_sizeof_type_rec(size.op0()), - size.op1()); + if(auto maybe_type=c_sizeof_type_rec(size.op0())) + object_type=array_typet( + *maybe_type, + size.op1()); } else if(size.id()==ID_mult && size.operands().size()==2 && size.op1().find(ID_C_c_sizeof_type).is_not_nil()) { - object_type=array_typet( - c_sizeof_type_rec(size.op1()), - size.op0()); + if(auto maybe_type=c_sizeof_type_rec(size.op1())) + object_type=array_typet( + *maybe_type, + size.op0()); } else { - typet tmp_type=c_sizeof_type_rec(size); + auto maybe_type=c_sizeof_type_rec(size); - if(tmp_type.is_not_nil()) + if(maybe_type) { // Did the size get multiplied? - if(auto maybe_elem_size=pointer_offset_size(tmp_type, ns)) + if(auto maybe_elem_size=pointer_offset_size(*maybe_type, ns)) { mp_integer alloc_size; mp_integer elem_size=*maybe_elem_size; - if(elem_size<0 || to_integer(size, alloc_size)) + if(elem_size<0 || (size.is_constant() && + to_integer(to_constant_expr(size), alloc_size))) { } else { if(alloc_size==elem_size) - object_type=tmp_type; + object_type=*maybe_type; else { mp_integer elements=alloc_size/elem_size; if(elements*elem_size==alloc_size) object_type=array_typet( - tmp_type, + *maybe_type, from_integer(elements, size.type())); } } @@ -189,7 +191,7 @@ exprt malloc_ssa( } // the fall-back is to produce a byte-array - if(object_type.is_nil()) + if(!object_type) object_type=array_typet(unsigned_char_type(), size); } @@ -197,17 +199,17 @@ exprt malloc_ssa( std::cout << "OBJECT_TYPE: " << from_type(ns, "", object_type) << std::endl; #endif - auto pointers=collect_pointer_vars(symbol_table, object_type); + auto pointers=collect_pointer_vars(symbol_table, *object_type); exprt object=create_dynamic_object( - suffix, object_type, symbol_table, is_concrete); + suffix, *object_type, symbol_table, is_concrete); if(object.type()!=code.type()) object=typecast_exprt(object, code.type()); exprt result; if(!is_concrete && alloc_concrete) { exprt concrete_object=create_dynamic_object( - suffix+"$co", object_type, symbol_table, true); + suffix+"$co", *object_type, symbol_table, true); // Create nondet symbol symbolt nondet_symbol; @@ -329,10 +331,8 @@ bool replace_malloc( namespacet ns(goto_model.symbol_table); goto_functionst::goto_functiont function_copy; function_copy.copy_from(f_it->second); - constant_propagator_ait const_propagator( - f_it->first, - function_copy, - ns); + constant_propagator_ait const_propagator(function_copy); + const_propagator(f_it->first, function_copy, ns); forall_goto_program_instructions(copy_i_it, function_copy.body) { if(copy_i_it->location_number==i_it->location_number) diff --git a/src/ssa/may_alias_analysis.cpp b/src/ssa/may_alias_analysis.cpp index ab9d43cec..a7e4d827e 100644 --- a/src/ssa/may_alias_analysis.cpp +++ b/src/ssa/may_alias_analysis.cpp @@ -119,3 +119,12 @@ void may_alias_domaint::members_to_symbols(exprt &expr, const namespacet &ns) expr=object.symbol_expr(); Forall_operands(it, expr)members_to_symbols(*it, ns); } + +void may_alias_analysist::initialize( + const irep_idt &function_id, + const goto_functionst::goto_functiont &goto_function) +{ + ait::initialize(function_id, goto_function); + forall_goto_program_instructions(i_it, goto_function.body) + get_state(i_it).make_bottom(); +} diff --git a/src/ssa/may_alias_analysis.h b/src/ssa/may_alias_analysis.h index 4d14f13e9..a7814b190 100644 --- a/src/ssa/may_alias_analysis.h +++ b/src/ssa/may_alias_analysis.h @@ -20,6 +20,8 @@ Author: Viktor Malik, imalik@fit.vutbr.cz class may_alias_domaint:public ai_domain_baset { public: + may_alias_domaint(): has_values(false) {} + void transform( const irep_idt &, locationt from, @@ -81,6 +83,10 @@ class may_alias_analysist:public ait { operator()(function_identifier, goto_function, ns); } +protected: + void initialize( + const irep_idt &function_id, + const goto_functionst::goto_functiont &goto_function) override; }; diff --git a/src/ssa/ssa_build_goto_trace.cpp b/src/ssa/ssa_build_goto_trace.cpp index c8500e624..6c7fb74c6 100644 --- a/src/ssa/ssa_build_goto_trace.cpp +++ b/src/ssa/ssa_build_goto_trace.cpp @@ -64,6 +64,8 @@ bool ssa_build_goto_tracet::can_convert_ssa_expr(const exprt &expr) can_convert_ssa_expr(index.array()); mp_integer idx; + if(!index.index().is_constant()) + return false; if(to_integer(to_constant_expr(index.index()), idx)) return false; return true; @@ -166,9 +168,6 @@ bool ssa_build_goto_tracet::record_step( case ASSIGN: { - if(has_prefix(id2string(current_pc->function), CPROVER_PREFIX)) - break; - const code_assignt &code_assign= to_code_assign(current_pc->code); @@ -178,6 +177,8 @@ bool ssa_build_goto_tracet::record_step( exprt rhs_simplified=simplify_expr(rhs_value, unwindable_local_SSA.ns); exprt lhs_ssa=finalize_lhs(code_assign.lhs()); exprt lhs_simplified=simplify_expr(lhs_ssa, unwindable_local_SSA.ns); + if(from_expr(lhs_simplified).find(CPROVER_PREFIX)!=std::string::npos) + break; #if 0 std::cout << "ASSIGN " @@ -221,7 +222,7 @@ bool ssa_build_goto_tracet::record_step( break; // skip undetermined rhs - find_symbols_sett rhs_symbols; + std::set rhs_symbols; find_symbols(rhs_simplified, rhs_symbols); if(!rhs_symbols.empty() || rhs_simplified.id()==ID_nondet_symbol) break; diff --git a/src/ssa/ssa_db.h b/src/ssa/ssa_db.h index 603e70fc8..d0d6ba8da 100644 --- a/src/ssa/ssa_db.h +++ b/src/ssa/ssa_db.h @@ -18,7 +18,7 @@ Author: Peter Schrammel #include #include -class ssa_dbt +class ssa_dbt:public messaget { public: typedef irep_idt function_namet; @@ -52,6 +52,7 @@ class ssa_dbt the_solvers[function_name]= incremental_solvert::allocate( store.at(function_name)->ns, + get_message_handler(), options.get_bool_option("refine")); return *the_solvers.at(function_name); } diff --git a/src/ssa/ssa_dereference.cpp b/src/ssa/ssa_dereference.cpp index c63a4b06b..33e71bda6 100644 --- a/src/ssa/ssa_dereference.cpp +++ b/src/ssa/ssa_dereference.cpp @@ -254,11 +254,9 @@ exprt ssa_alias_value( } } - byte_extract_exprt byte_extract(byte_extract_id(), e1.type()); if(competition_mode) assert(!e2_type.get_bool("#dynamic")); - byte_extract.op()=e2; - byte_extract.offset()=offset1; + byte_extract_exprt byte_extract(byte_extract_id(), e2, offset1, e1.type()); return byte_extract; } diff --git a/src/ssa/ssa_domain.cpp b/src/ssa/ssa_domain.cpp index 0130a6280..9a6f66b54 100644 --- a/src/ssa/ssa_domain.cpp +++ b/src/ssa/ssa_domain.cpp @@ -229,16 +229,21 @@ ssa_domaint::def_mapt::const_iterator ssa_domaint::get_object_allocation_def( return def_map.end(); } -void ssa_ait::initialize(const goto_functionst::goto_functiont &goto_function) +void ssa_ait::initialize( + const irep_idt &function_id, + const goto_functionst::goto_functiont &goto_function) { - ait::initialize(goto_function); + ait::initialize(function_id, goto_function); + forall_goto_program_instructions(i_it, goto_function.body) + get_state(i_it).make_bottom(); // Make entry instruction have a source for the all objects. if(!goto_function.body.instructions.empty()) { locationt e=goto_function.body.instructions.begin(); - ssa_domaint &entry=operator[](e); + auto entry_s=entry_state(goto_function.body); + ssa_domaint &entry=dynamic_cast(get_state(entry_s)); #if 0 // parameters diff --git a/src/ssa/ssa_domain.h b/src/ssa/ssa_domain.h index 9950c7668..c22f233f0 100644 --- a/src/ssa/ssa_domain.h +++ b/src/ssa/ssa_domain.h @@ -20,6 +20,8 @@ Author: Daniel Kroening, kroening@kroening.com class ssa_domaint:public ai_domain_baset { public: + ssa_domaint(): has_values(false) {} + // sources for identifiers struct deft { @@ -145,7 +147,9 @@ class ssa_ait:public ait // The overload below is needed to make the entry point get a source // for all objects. - virtual void initialize(const goto_functionst::goto_functiont &goto_function); + void initialize( + const irep_idt &function_id, + const goto_functionst::goto_functiont &goto_function) override; }; #endif diff --git a/src/ssa/ssa_inliner.cpp b/src/ssa/ssa_inliner.cpp index 375530e81..fb8eef95e 100644 --- a/src/ssa/ssa_inliner.cpp +++ b/src/ssa/ssa_inliner.cpp @@ -204,64 +204,6 @@ void ssa_inlinert::replace( } } -/// replaces inlines functions if SSA is available in functions and does nothing -/// otherwise -void ssa_inlinert::replace( - local_SSAt &SSA, - const ssa_dbt &ssa_db, - bool recursive, bool rename) -{ - for(local_SSAt::nodest::iterator n_it=SSA.nodes.begin(); - n_it!=SSA.nodes.end(); n_it++) - { - for(local_SSAt::nodet::function_callst::iterator - f_it=n_it->function_calls.begin(); - f_it!=n_it->function_calls.end(); f_it++) - { - assert(f_it->function().id()==ID_symbol); // no function pointers - irep_idt fname=to_symbol_expr(f_it->function()).get_identifier(); - - if(ssa_db.exists(fname)) - { - status() << "Inlining function " << fname << eom; - local_SSAt fSSA=ssa_db.get(fname); // copy - - if(rename) - { - // getting globals at call site - local_SSAt::var_sett cs_globals_in, cs_globals_out; - goto_programt::const_targett loc=n_it->location; - SSA.get_globals(loc, cs_globals_in); - SSA.get_globals(loc, cs_globals_out, false); - - if(recursive) - { - replace(fSSA, ssa_db, true); - } - - // replace - replace(SSA.nodes, n_it, f_it, cs_globals_in, cs_globals_out, fSSA); - } - else // just add to nodes - { - for(local_SSAt::nodest::const_iterator fn_it=fSSA.nodes.begin(); - fn_it!=fSSA.nodes.end(); fn_it++) - { - debug() << "new node: "; fn_it->output(debug(), fSSA.ns); - debug() << eom; - - new_nodes.push_back(*fn_it); - } - } - } - else - debug() << "No body available for function " << fname << eom; - commit_node(n_it); - } - commit_nodes(SSA.nodes, n_it); - } -} - /// inline summary void ssa_inlinert::replace( local_SSAt &SSA, @@ -370,9 +312,9 @@ exprt ssa_inlinert::get_replace_globals_in( { symbol_exprt lhs=*it; // copy rename(lhs); - symbol_exprt rhs; - if(find_corresponding_symbol(*it, globals, rhs)) + if(auto maybe_rhs=find_corresponding_symbol(*it, globals)) { + symbol_exprt rhs=*maybe_rhs; debug() << "binding: " << lhs.get_identifier() << " == " << rhs.get_identifier() << eom; c.push_back(equal_exprt(lhs, rhs)); @@ -397,9 +339,9 @@ void ssa_inlinert::replace_globals_in( { symbol_exprt lhs=*it; // copy rename(lhs); - symbol_exprt rhs; - if(find_corresponding_symbol(*it, globals, rhs)) + if(auto maybe_rhs=find_corresponding_symbol(*it, globals)) { + symbol_exprt rhs=*maybe_rhs; debug() << "binding: " << lhs.get_identifier() << "==" << rhs.get_identifier() << eom; new_equs.push_back(equal_exprt(lhs, rhs)); @@ -590,25 +532,25 @@ exprt ssa_inlinert::get_replace_globals_out( for(summaryt::var_sett::const_iterator it=cs_globals_out.begin(); it!=cs_globals_out.end(); it++) { - symbol_exprt lhs; const exprt rhs=*it; - if(is_pointed(*it) || id2string(it->get_identifier()).find("dynamic_object$")!= std::string::npos) { - if(!cs_heap_covered(*it) && - !find_corresponding_symbol(*it, summary.globals_out, lhs)) + auto maybe_lhs=find_corresponding_symbol(*it, summary.globals_out); + if(!cs_heap_covered(*it) && !maybe_lhs) { - assert(find_corresponding_symbol(*it, cs_globals_in, lhs)); - c.push_back(equal_exprt(lhs, rhs)); + auto new_lhs=find_corresponding_symbol(*it, cs_globals_in); + assert(new_lhs); + c.push_back(equal_exprt(*new_lhs, rhs)); } } else { - if(find_corresponding_symbol(*it, summary.globals_out, lhs)) + if(auto maybe_lhs=find_corresponding_symbol(*it, summary.globals_out)) { + symbol_exprt lhs=*maybe_lhs; // Bind function return value rename(lhs); c.push_back(equal_exprt(lhs, rhs)); @@ -691,11 +633,13 @@ exprt ssa_inlinert::get_replace_globals_out( } else { - if(find_corresponding_symbol(*it, summary.globals_out, lhs)) - rename(lhs); + auto lhs=find_corresponding_symbol(*it, summary.globals_out); + if(lhs) + rename(*lhs); else - assert(find_corresponding_symbol(*it, cs_globals_in, lhs)); - c.push_back(equal_exprt(lhs, rhs)); + lhs=find_corresponding_symbol(*it, cs_globals_in); + assert(lhs); + c.push_back(equal_exprt(*lhs, rhs)); } } } @@ -713,12 +657,13 @@ void ssa_inlinert::replace_globals_out( it!=cs_globals_out.end(); it++) { symbol_exprt rhs=*it; // copy - symbol_exprt lhs; - if(find_corresponding_symbol(*it, globals_out, lhs)) - rename(lhs); + auto maybe_lhs=find_corresponding_symbol(*it, globals_out); + if(maybe_lhs) + rename(*maybe_lhs); else - assert(find_corresponding_symbol(*it, cs_globals_in, lhs)); - new_equs.push_back(equal_exprt(lhs, rhs)); + maybe_lhs=find_corresponding_symbol(*it, cs_globals_in); + assert(maybe_lhs); + new_equs.push_back(equal_exprt(*maybe_lhs, rhs)); } } @@ -799,9 +744,8 @@ void ssa_inlinert::rename_to_caller( for(summaryt::var_sett::const_iterator it=globals_in.begin(); it!=globals_in.end(); it++) { - symbol_exprt cg; - if(find_corresponding_symbol(*it, cs_globals_in, cg)) - replace_map[*it]=cg; + if(auto maybe_cg=find_corresponding_symbol(*it, cs_globals_in)) + replace_map[*it]=*maybe_cg; else { #if 0 @@ -850,9 +794,8 @@ void ssa_inlinert::rename_to_callee( for(summaryt::var_sett::const_iterator it=cs_globals_in.begin(); it!=cs_globals_in.end(); it++) { - symbol_exprt cg; - if(find_corresponding_symbol(*it, globals_in, cg)) - replace_map[*it]=cg; + if(auto maybe_cg=find_corresponding_symbol(*it, globals_in)) + replace_map[*it]=*maybe_cg; else { #if 0 @@ -901,11 +844,9 @@ bool ssa_inlinert::commit_nodes( return false; } -/// \return returns false if the symbol is not found -bool ssa_inlinert::find_corresponding_symbol( +optionalt ssa_inlinert::find_corresponding_symbol( const symbol_exprt &s, - const local_SSAt::var_sett &globals, - symbol_exprt &s_found) + const local_SSAt::var_sett &globals) { const irep_idt &s_orig_id=get_original_identifier(s); for(local_SSAt::var_sett::const_iterator it=globals.begin(); @@ -917,11 +858,10 @@ bool ssa_inlinert::find_corresponding_symbol( #endif if(s_orig_id==get_original_identifier(*it)) { - s_found=*it; - return true; + return *it; } } - return false; + return {}; } /// TODO: this is a potential source of bugs. Better way to do that? @@ -1047,8 +987,14 @@ exprt ssa_inlinert::param_out_transformer( else { symbol_exprt param_out=to_symbol_expr(param); - if(find_corresponding_symbol(to_symbol_expr(param), globals_out, param_out)) + auto maybe_new=find_corresponding_symbol( + to_symbol_expr(param), + globals_out); + if(maybe_new) + { + param_out=*maybe_new; rename(param_out); + } return param_out; } } @@ -1095,10 +1041,10 @@ exprt ssa_inlinert::param_out_member_transformer( symbol_exprt param_member( id2string(to_symbol_expr(param).get_identifier())+"."+ id2string(component.get_name()), component.type()); - symbol_exprt param_out; - assert(find_corresponding_symbol(param_member, globals_out, param_out)); - rename(param_out); - return param_out; + auto param_out=find_corresponding_symbol(param_member, globals_out); + assert(param_out); + rename(*param_out); + return *param_out; } exprt ssa_inlinert::arg_out_member_transformer( diff --git a/src/ssa/ssa_inliner.h b/src/ssa/ssa_inliner.h index ffe0214c7..455533a47 100644 --- a/src/ssa/ssa_inliner.h +++ b/src/ssa/ssa_inliner.h @@ -69,12 +69,6 @@ class ssa_inlinert:public messaget const local_SSAt::var_sett &cs_globals_out, // outgoing globals at call site const local_SSAt &function); - void replace( - local_SSAt &SSA, - const ssa_dbt &ssa_db, - bool recursive=false, - bool rename=true); - void havoc( local_SSAt::nodet &node, local_SSAt::nodet::function_callst::iterator f_it); @@ -99,10 +93,9 @@ class ssa_inlinert:public messaget const local_SSAt::var_sett &globals_in, exprt &expr); - static bool find_corresponding_symbol( + static optionalt find_corresponding_symbol( const symbol_exprt &s, - const local_SSAt::var_sett &globals, - symbol_exprt &s_found); + const local_SSAt::var_sett &globals); static irep_idt get_original_identifier(const symbol_exprt &s); diff --git a/src/ssa/ssa_object.cpp b/src/ssa/ssa_object.cpp index 69de5f58d..7bf4fd90f 100644 --- a/src/ssa/ssa_object.cpp +++ b/src/ssa/ssa_object.cpp @@ -52,7 +52,7 @@ void collect_ptr_objects( const symbolt *symbol; if(dynamic || (!ns.lookup(src.get_identifier(), symbol) && - !symbol->is_procedure_local())) + symbol->is_static_lifetime)) ptr_object.type().set("#dynamic", true); if(is_ptr_object(src)) @@ -240,7 +240,7 @@ void ssa_objectst::categorize_objects( else { const symbolt &symbol=ns.lookup(to_symbol_expr(root_object)); - if(symbol.is_procedure_local()) + if(!symbol.is_static_lifetime) { if(dirty(symbol.name)) dirty_locals.insert(*o_it); diff --git a/src/ssa/ssa_pointed_objects.cpp b/src/ssa/ssa_pointed_objects.cpp index 7247511e6..32aa1f409 100644 --- a/src/ssa/ssa_pointed_objects.cpp +++ b/src/ssa/ssa_pointed_objects.cpp @@ -96,7 +96,7 @@ symbol_exprt pointed_object(const exprt &expr, const namespacet &ns) { pointed.set( level_str(level, ID_pointer_subtype), - to_symbol_type(pointed_type).get_identifier()); + to_struct_tag_type(pointed_type).get_identifier()); } return pointed; @@ -108,7 +108,7 @@ symbol_exprt pointed_object(const exprt &expr, const namespacet &ns) const irep_idt pointer_root_id(const exprt &expr) { assert(expr.get_bool(ID_pointed)); - unsigned max_level_index=expr.get_unsigned_int(ID_pointed_level)-1; + unsigned max_level_index=expr.get_size_t(ID_pointed_level)-1; if(expr.get(level_str(max_level_index, ID_pointer_id))==ID_symbol) return expr.get(level_str(max_level_index, ID_pointer_sym)); else @@ -118,7 +118,7 @@ const irep_idt pointer_root_id(const exprt &expr) unsigned pointed_level(const exprt &expr) { if(is_pointed(expr)) - return expr.get_unsigned_int(ID_pointed_level); + return expr.get_size_t(ID_pointed_level); else return 0; } @@ -134,7 +134,7 @@ const exprt get_pointer(const exprt &expr, unsigned level) exprt pointer; const typet &pointed_type= - symbol_typet(expr.get(level_str(level, ID_pointer_subtype))); + struct_tag_typet(expr.get(level_str(level, ID_pointer_subtype))); if(expr.get(level_str(level, ID_pointer_id))==ID_symbol) { diff --git a/src/ssa/ssa_unwinder.cpp b/src/ssa/ssa_unwinder.cpp index bc20805ff..e7e93957d 100644 --- a/src/ssa/ssa_unwinder.cpp +++ b/src/ssa/ssa_unwinder.cpp @@ -118,7 +118,7 @@ void ssa_local_unwindert::build_pre_post_map() it->second.modified_vars.push_back(o_it->get_expr()); symbol_exprt pre=SSA.name(*o_it, local_SSAt::PHI, pre_loc); - it->second.pre_post_map[pre]=SSA.read_rhs(*o_it, post_loc); + it->second.pre_post_map.insert({pre, SSA.read_rhs(*o_it, post_loc)}); } } } @@ -447,7 +447,7 @@ void ssa_local_unwindert::add_loop_connector(loopt &loop) { node.equalities.push_back(*e_it); node.equalities.back().rhs()= - loop.pre_post_map[to_symbol_expr(e_it->lhs())]; + loop.pre_post_map.at(to_symbol_expr(e_it->lhs())); SSA.rename(node.equalities.back().rhs(), node.location); SSA.decrement_unwindings(0); SSA.rename(node.equalities.back().lhs(), node.location); diff --git a/src/ssa/ssa_unwinder.h b/src/ssa/ssa_unwinder.h index 5f106e9ff..9428f7683 100644 --- a/src/ssa/ssa_unwinder.h +++ b/src/ssa/ssa_unwinder.h @@ -29,7 +29,8 @@ class ssa_local_unwindert fname(_fname), SSA(_SSA), is_kinduction(_is_kinduction), - is_bmc(_is_bmc) + is_bmc(_is_bmc), + current_enabling_expr(bool_typet()) { } diff --git a/src/ssa/ssa_value_set.cpp b/src/ssa/ssa_value_set.cpp index 9f078a9bb..71b3b0f79 100644 --- a/src/ssa/ssa_value_set.cpp +++ b/src/ssa/ssa_value_set.cpp @@ -18,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "ssa_value_set.h" #include "ssa_dereference.h" @@ -310,7 +311,9 @@ void ssa_value_domaint::assign_rhs_rec( mp_integer pointer_offset=*maybe_pointer_offset; if(pointer_offset<1) pointer_offset=1; - unsigned a=merge_alignment(integer2ulong(pointer_offset), alignment); + unsigned a=merge_alignment( + numeric_cast_v(pointer_offset), + alignment); assign_rhs_rec(dest, *it, ns, true, a); pointer=true; @@ -336,7 +339,9 @@ void ssa_value_domaint::assign_rhs_rec( mp_integer pointer_offset=*maybe_pointer_offset; if(pointer_offset<1) pointer_offset=1; - unsigned a=merge_alignment(integer2ulong(pointer_offset), alignment); + unsigned a=merge_alignment( + numeric_cast_v(pointer_offset), + alignment); assign_rhs_rec(dest, rhs.op0(), ns, true, a); if(competition_mode) @@ -413,7 +418,9 @@ void ssa_value_domaint::assign_rhs_rec_address_of( mp_integer pointer_offset=*maybe_pointer_offset; if(pointer_offset<1) pointer_offset=1; - a=merge_alignment(a, integer2ulong(pointer_offset)); + a=merge_alignment( + a, + numeric_cast_v(pointer_offset)); } } @@ -611,16 +618,20 @@ void ssa_value_domaint::assign_pointed_rhs_rec( /// objects pointed by parameters. /// \par parameters: GOTO function void ssa_value_ait::initialize( + const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function) { - ait::initialize(goto_function); + ait::initialize(function_id, goto_function); + forall_goto_program_instructions(i_it, goto_function.body) + get_state(i_it).make_bottom(); // Initialize value sets for pointer parameters if(!goto_function.type.parameters().empty()) { - locationt e=goto_function.body.instructions.begin(); - ssa_value_domaint &entry=operator[](e); + auto entry_s=entry_state(goto_function.body); + ssa_value_domaint &entry=dynamic_cast( + get_state(entry_s)); for(auto ¶m : goto_function.type.parameters()) { diff --git a/src/ssa/ssa_value_set.h b/src/ssa/ssa_value_set.h index 5ed06e4a5..d1eae7394 100644 --- a/src/ssa/ssa_value_set.h +++ b/src/ssa/ssa_value_set.h @@ -21,6 +21,8 @@ Author: Daniel Kroening, kroening@kroening.com class ssa_value_domaint:public ai_domain_baset { public: + ssa_value_domaint(): has_values(false) {} + void transform( const irep_idt &, locationt, @@ -100,7 +102,7 @@ class ssa_value_domaint:public ai_domain_baset typedef std::map value_mapt; value_mapt value_map; - bool competition_mode; + bool competition_mode=false; const valuest operator()( const exprt &src, @@ -164,7 +166,8 @@ class ssa_value_ait:public ait } protected: - virtual void initialize( + void initialize( + const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function) override; void assign_ptr_param(const exprt &expr, ssa_value_domaint &entry); diff --git a/src/ssa/ssa_var_collector.cpp b/src/ssa/ssa_var_collector.cpp index 18b9bb43f..325bf0b85 100644 --- a/src/ssa/ssa_var_collector.cpp +++ b/src/ssa/ssa_var_collector.cpp @@ -52,7 +52,8 @@ void ssa_var_collectort::add_var( { const array_typet &array_type=to_array_type(var.type()); mp_integer size; - to_integer(array_type.size(), size); + if(array_type.size().is_constant()) + to_integer(to_constant_expr(array_type.size()), size); for(mp_integer i=0; ilocation); + symbol_exprt pre_var=SSA.name(*o_it, local_SSAt::LOOP_BACK, n_it->location); ssa_local_unwinder.unwinder_rename(pre_var, *n_it, true); symbol_exprt post_var=SSA.read_rhs(*o_it, n_it->location); @@ -109,6 +109,7 @@ void ssa_var_collectort::get_pre_var( rename_aux_post(post_var); aux_renaming_map[pre_var]=post_var; + return pre_var; } /// supposes that loop head PHIs are of the form xphi=gls?xlb:x0 @@ -172,8 +173,7 @@ void ssa_var_collectort::collect_variables_loop( if(p_it==phi_nodes.end()) continue; // object not modified in this loop - symbol_exprt pre_var; - get_pre_var(SSA, o_it, n_it, pre_var); + symbol_exprt pre_var=get_pre_var(SSA, o_it, n_it); exprt init_expr; get_init_expr(SSA, o_it, n_it, init_expr); add_var(pre_var, pre_guard, post_guard, guardst::LOOP, var_specs); diff --git a/src/ssa/ssa_var_collector.h b/src/ssa/ssa_var_collector.h index 665cb86ae..8288b9adb 100644 --- a/src/ssa/ssa_var_collector.h +++ b/src/ssa/ssa_var_collector.h @@ -53,11 +53,10 @@ class ssa_var_collectort exprt &pre_guard, exprt &post_guard); - void get_pre_var( + symbol_exprt get_pre_var( const local_SSAt &SSA, local_SSAt::objectst::const_iterator o_it, - local_SSAt::nodest::const_iterator n_it, - symbol_exprt &pre_var); + local_SSAt::nodest::const_iterator n_it); void get_init_expr( const local_SSAt &SSA,