From 9e8d0be070dbc978eab6016d8849889046229657 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 13 Jul 2016 14:52:53 -0400 Subject: [PATCH 1/2] abstract interpretation merge implementations may require a namespace --- src/analyses/ai.cpp | 10 +++++----- src/analyses/ai.h | 14 +++++++++++--- src/analyses/constant_propagator.cpp | 3 ++- src/analyses/constant_propagator.h | 5 +++-- src/analyses/custom_bitvector_analysis.cpp | 3 ++- src/analyses/custom_bitvector_analysis.h | 3 ++- src/analyses/dependence_graph.cpp | 3 ++- src/analyses/dependence_graph.h | 3 ++- src/analyses/escape_analysis.cpp | 3 ++- src/analyses/escape_analysis.h | 3 ++- src/analyses/global_may_alias.cpp | 3 ++- src/analyses/global_may_alias.h | 3 ++- src/analyses/interval_domain.h | 3 ++- src/analyses/invariant_set_domain.h | 3 ++- src/analyses/is_threaded.cpp | 3 ++- src/analyses/reaching_definitions.cpp | 3 ++- src/analyses/reaching_definitions.h | 3 ++- src/analyses/uninitialized_domain.cpp | 3 ++- src/analyses/uninitialized_domain.h | 3 ++- src/java_bytecode/java_local_variable_table.cpp | 10 ++++++++-- 20 files changed, 59 insertions(+), 28 deletions(-) diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index dedb2da9a3c..f43ad9f025c 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -367,7 +367,7 @@ bool ai_baset::visit( new_values.transform(l, to_l, *this, ns); - if(merge(new_values, l, to_l)) + if(merge(new_values, l, to_l, ns)) have_new_values=true; } @@ -400,7 +400,7 @@ bool ai_baset::do_function_call( std::unique_ptr tmp_state(make_temporary_state(get_state(l_call))); tmp_state->transform(l_call, l_return, *this, ns); - return merge(*tmp_state, l_call, l_return); + return merge(*tmp_state, l_call, l_return, ns); } assert(!goto_function.body.instructions.empty()); @@ -420,7 +420,7 @@ bool ai_baset::do_function_call( bool new_data=false; // merge the new stuff - if(merge(*tmp_state, l_call, l_begin)) + if(merge(*tmp_state, l_call, l_begin, ns)) new_data=true; // do we need to do/re-do the fixedpoint of the body? @@ -445,7 +445,7 @@ bool ai_baset::do_function_call( tmp_state->transform(l_end, l_return, *this, ns); // Propagate those - return merge(*tmp_state, l_end, l_return); + return merge(*tmp_state, l_end, l_return, ns); } } @@ -581,7 +581,7 @@ void ai_baset::concurrent_fixedpoint( put_in_working_set(working_set, wl_pair.second); statet &begin_state=get_state(wl_pair.second); - merge(begin_state, sh_target, wl_pair.second); + merge(begin_state, sh_target, wl_pair.second, ns); while(!working_set.empty()) { diff --git a/src/analyses/ai.h b/src/analyses/ai.h index dfe5e183a3d..245fa48eef6 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -360,7 +360,11 @@ class ai_baset // abstract methods - virtual bool merge(const statet &src, locationt from, locationt to)=0; + virtual bool merge( + const statet &src, + locationt from, + locationt to, + const namespacet &ns)=0; // for concurrent fixedpoint virtual bool merge_shared( const statet &src, @@ -436,11 +440,15 @@ class ait:public ai_baset return it->second; } - bool merge(const statet &src, locationt from, locationt to) override + virtual bool merge( + const statet &src, + locationt from, + locationt to, + const namespacet &ns) override { statet &dest=get_state(to); return static_cast(dest).merge( - static_cast(src), from, to); + static_cast(src), from, to, ns); } std::unique_ptr make_temporary_state(const statet &s) override diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 8a18888fbcf..03474b66d73 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -498,7 +498,8 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src) bool constant_propagator_domaint::merge( const constant_propagator_domaint &other, locationt from, - locationt to) + locationt to, + const namespacet &ns) { return values.merge(other.values); } diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 0fc4796e8b7..6c33ae620cd 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -25,7 +25,7 @@ class constant_propagator_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai_base, - const namespacet &ns) final override; + const namespacet &ns) override; virtual void output( std::ostream &out, @@ -35,7 +35,8 @@ class constant_propagator_domaint:public ai_domain_baset bool merge( const constant_propagator_domaint &other, locationt from, - locationt to); + locationt to, + const namespacet &); virtual bool ai_simplify( exprt &condition, diff --git a/src/analyses/custom_bitvector_analysis.cpp b/src/analyses/custom_bitvector_analysis.cpp index be96ce1e2c2..0e82247a57f 100644 --- a/src/analyses/custom_bitvector_analysis.cpp +++ b/src/analyses/custom_bitvector_analysis.cpp @@ -590,7 +590,8 @@ void custom_bitvector_domaint::output( bool custom_bitvector_domaint::merge( const custom_bitvector_domaint &b, locationt from, - locationt to) + locationt to, + const namespacet &ns) { bool changed=has_values.is_false(); has_values=tvt::unknown(); diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index 4142d6930c1..0914708758c 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -70,7 +70,8 @@ class custom_bitvector_domaint:public ai_domain_baset bool merge( const custom_bitvector_domaint &b, locationt from, - locationt to); + locationt to, + const namespacet &ns); typedef unsigned long long bit_vectort; diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index dd9a770d837..dfe5c6ec181 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -24,7 +24,8 @@ Date: August 2013 bool dep_graph_domaint::merge( const dep_graph_domaint &src, goto_programt::const_targett from, - goto_programt::const_targett to) + goto_programt::const_targett to, + const namespacet &ns) { bool changed=has_values.is_false(); has_values=tvt::unknown(); diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 30b97108776..41a3598aa0d 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -77,7 +77,8 @@ class dep_graph_domaint:public ai_domain_baset bool merge( const dep_graph_domaint &src, goto_programt::const_targett from, - goto_programt::const_targett to); + goto_programt::const_targett to, + const namespacet &ns); void transform( goto_programt::const_targett from, diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp index 1598b9ededa..36a154a5e90 100644 --- a/src/analyses/escape_analysis.cpp +++ b/src/analyses/escape_analysis.cpp @@ -302,7 +302,8 @@ void escape_domaint::output( bool escape_domaint::merge( const escape_domaint &b, locationt from, - locationt to) + locationt to, + const namespacet &ns) { bool changed=has_values.is_false(); has_values=tvt::unknown(); diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h index bbf05973b13..3ba22d5ce15 100644 --- a/src/analyses/escape_analysis.h +++ b/src/analyses/escape_analysis.h @@ -40,7 +40,8 @@ class escape_domaint:public ai_domain_baset bool merge( const escape_domaint &b, locationt from, - locationt to); + locationt to, + const namespacet &ns); void make_bottom() final override { diff --git a/src/analyses/global_may_alias.cpp b/src/analyses/global_may_alias.cpp index 82c1f5a72dc..8c94f841b02 100644 --- a/src/analyses/global_may_alias.cpp +++ b/src/analyses/global_may_alias.cpp @@ -159,7 +159,8 @@ void global_may_alias_domaint::output( bool global_may_alias_domaint::merge( const global_may_alias_domaint &b, locationt from, - locationt to) + locationt to, + const namespacet &ns) { bool changed=has_values.is_false(); has_values=tvt::unknown(); diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h index b8f3480bb1c..b797aa76cec 100644 --- a/src/analyses/global_may_alias.h +++ b/src/analyses/global_may_alias.h @@ -40,7 +40,8 @@ class global_may_alias_domaint:public ai_domain_baset bool merge( const global_may_alias_domaint &b, locationt from, - locationt to); + locationt to, + const namespacet &ns); void make_bottom() final override { diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index f94236861e6..36c8da324cf 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -48,7 +48,8 @@ class interval_domaint:public ai_domain_baset bool merge( const interval_domaint &b, locationt from, - locationt to) + locationt to, + const namespacet &ns) { return join(b); } diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h index 367e987c709..a065391b5be 100644 --- a/src/analyses/invariant_set_domain.h +++ b/src/analyses/invariant_set_domain.h @@ -32,7 +32,8 @@ class invariant_set_domaint:public ai_domain_baset bool merge( const invariant_set_domaint &other, locationt from, - locationt to) + locationt to, + const namespacet &ns) { bool changed=invariant_set.make_union(other.invariant_set) || has_values.is_false(); diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index ca1ddff4718..e375a9328d2 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -31,7 +31,8 @@ class is_threaded_domaint:public ai_domain_baset bool merge( const is_threaded_domaint &src, locationt from, - locationt to) + locationt to, + const namespacet &ns) { INVARIANT(src.reachable, "Abstract states are only merged at reachable locations"); diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 7788835f0db..6f00601dd5d 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -629,7 +629,8 @@ bool rd_range_domaint::merge_inner( bool rd_range_domaint::merge( const rd_range_domaint &other, locationt from, - locationt to) + locationt to, + const namespacet &ns) { bool changed=has_values.is_false(); has_values=tvt::unknown(); diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index 046dae22863..0e714554211 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -164,7 +164,8 @@ class rd_range_domaint:public ai_domain_baset bool merge( const rd_range_domaint &other, locationt from, - locationt to); + locationt to, + const namespacet &ns); bool merge_shared( const rd_range_domaint &other, diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp index 5cff1d3f0b9..09c807ebea1 100644 --- a/src/analyses/uninitialized_domain.cpp +++ b/src/analyses/uninitialized_domain.cpp @@ -83,7 +83,8 @@ void uninitialized_domaint::output( bool uninitialized_domaint::merge( const uninitialized_domaint &other, locationt from, - locationt to) + locationt to, + const namespacet &ns) { auto old_uninitialized=uninitialized.size(); diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h index 2d957d0bbb5..d5d0eade19a 100644 --- a/src/analyses/uninitialized_domain.h +++ b/src/analyses/uninitialized_domain.h @@ -73,7 +73,8 @@ class uninitialized_domaint:public ai_domain_baset bool merge( const uninitialized_domaint &other, locationt from, - locationt to); + locationt to, + const namespacet &ns); private: tvt has_values; diff --git a/src/java_bytecode/java_local_variable_table.cpp b/src/java_bytecode/java_local_variable_table.cpp index dc519b3fa09..f372bd509d3 100644 --- a/src/java_bytecode/java_local_variable_table.cpp +++ b/src/java_bytecode/java_local_variable_table.cpp @@ -35,7 +35,9 @@ struct procedure_local_cfg_baset< typedef std::map entry_mapt; entry_mapt entry_map; - procedure_local_cfg_baset() {} + explicit procedure_local_cfg_baset(const namespacet &_ns):ns(_ns) + { + } void operator()(const method_with_amapt &args) { @@ -96,6 +98,9 @@ struct procedure_local_cfg_baset< { return args.second.empty(); } + +protected: + const namespacet &ns; }; // Grab some class typedefs for brevity: @@ -708,7 +713,8 @@ void java_bytecode_convert_methodt::setup_local_variables( const address_mapt &amap) { // Compute CFG dominator tree - java_cfg_dominatorst dominator_analysis; + const namespacet ns(symbol_table); + java_cfg_dominatorst dominator_analysis(ns); method_with_amapt dominator_args(m, amap); dominator_analysis(dominator_args); From 336cf6cf650d7f41a08f14fc073aa60fc58bc93a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 11 Jul 2016 14:52:11 +0100 Subject: [PATCH 2/2] assume, assert do not have CFG successors if their guard evaluates to false Apply the simplifier as, e.g., the C front end may generate expressions such as 0!=0 for typing purposes. --- src/analyses/cfg_dominators.h | 36 +++-- src/analyses/dependence_graph.h | 3 +- src/analyses/natural_loops.cpp | 4 +- src/analyses/natural_loops.h | 40 ++++-- .../unreachable_instructions.cpp | 7 +- src/goto-instrument/accelerate/accelerate.h | 1 + src/goto-instrument/code_contracts.cpp | 2 +- src/goto-instrument/count_eloc.cpp | 3 +- src/goto-instrument/full_slicer.cpp | 19 ++- src/goto-instrument/full_slicer_class.h | 5 + .../goto_instrument_parse_options.cpp | 2 +- src/goto-instrument/goto_program2code.cpp | 36 ++--- src/goto-instrument/goto_program2code.h | 20 ++- src/goto-instrument/havoc_loops.cpp | 8 +- src/goto-instrument/k_induction.cpp | 7 +- src/goto-instrument/points_to.h | 2 +- src/goto-instrument/reachability_slicer.cpp | 6 +- .../reachability_slicer_class.h | 4 + src/goto-programs/cfg.h | 130 ++++++++++++------ 19 files changed, 223 insertions(+), 112 deletions(-) diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h index fa7d23ccf0a..fcf461a7a5c 100644 --- a/src/analyses/cfg_dominators.h +++ b/src/analyses/cfg_dominators.h @@ -22,10 +22,14 @@ Author: Georg Weissenbacher, georg@weissenbacher.name #include #include -template +template class cfg_dominators_templatet { public: + explicit cfg_dominators_templatet(const namespacet &ns):cfg(ns) + { + } + typedef std::set target_sett; struct nodet @@ -33,7 +37,7 @@ class cfg_dominators_templatet target_sett dominators; }; - typedef procedure_local_cfg_baset cfgt; + typedef procedure_local_cfg_baset cfgt; cfgt cfg; void operator()(P &program); @@ -48,33 +52,36 @@ class cfg_dominators_templatet }; /// Print the result of the dominator computation -template +template std::ostream &operator << ( std::ostream &out, - const cfg_dominators_templatet &cfg_dominators) + const cfg_dominators_templatet &cfg_dominators) { cfg_dominators.output(out); return out; } /// Compute dominators -template -void cfg_dominators_templatet::operator()(P &program) +template +void cfg_dominators_templatet::operator()( + P &program) { initialise(program); fixedpoint(program); } /// Initialises the elements of the fixed point analysis -template -void cfg_dominators_templatet::initialise(P &program) +template +void cfg_dominators_templatet::initialise( + P &program) { cfg(program); } /// Computes the MOP for the dominator analysis -template -void cfg_dominators_templatet::fixedpoint(P &program) +template +void cfg_dominators_templatet::fixedpoint( + P &program) { std::list worklist; @@ -181,8 +188,9 @@ inline void dominators_pretty_print_node( } /// Print the result of the dominator computation -template -void cfg_dominators_templatet::output(std::ostream &out) const +template +void cfg_dominators_templatet::output( + std::ostream &out) const { for(const auto &node : cfg.entry_map) { @@ -206,11 +214,11 @@ void cfg_dominators_templatet::output(std::ostream &out) const } typedef cfg_dominators_templatet< - const goto_programt, goto_programt::const_targett, false> + const goto_programt, goto_programt::const_targett, false, false> cfg_dominatorst; typedef cfg_dominators_templatet< - const goto_programt, goto_programt::const_targett, true> + const goto_programt, goto_programt::const_targett, true, false> cfg_post_dominatorst; template<> diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 41a3598aa0d..8dea14ed908 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -211,7 +211,8 @@ class dependence_grapht: if(!goto_program.empty()) { const irep_idt id=goto_programt::get_function_id(goto_program); - cfg_post_dominatorst &pd=post_dominators[id]; + cfg_post_dominatorst &pd= + post_dominators.insert({id, cfg_post_dominatorst(ns)}).first->second; pd(goto_program); } } diff --git a/src/analyses/natural_loops.cpp b/src/analyses/natural_loops.cpp index 2ac9bbc8ed7..733d169a1bd 100644 --- a/src/analyses/natural_loops.cpp +++ b/src/analyses/natural_loops.cpp @@ -15,11 +15,13 @@ void show_natural_loops( const goto_modelt &goto_model, std::ostream &out) { + namespacet ns(goto_model.symbol_table); + forall_goto_functions(it, goto_model.goto_functions) { out << "*** " << it->first << '\n'; - natural_loopst natural_loops; + natural_loopst natural_loops(ns); natural_loops(it->second.body); natural_loops.output(out); diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h index 710fd9d2c56..dee70edc7a9 100644 --- a/src/analyses/natural_loops.h +++ b/src/analyses/natural_loops.h @@ -20,7 +20,7 @@ Author: Georg Weissenbacher, georg@weissenbacher.name #include "cfg_dominators.h" -template +template class natural_loops_templatet { public: @@ -38,23 +38,27 @@ class natural_loops_templatet void output(std::ostream &) const; - const cfg_dominators_templatet &get_dominator_info() const + const cfg_dominators_templatet& + get_dominator_info() const { return cfg_dominators; } - natural_loops_templatet() + explicit natural_loops_templatet(const namespacet &ns): + cfg_dominators(ns) { } - explicit natural_loops_templatet(P &program) + natural_loops_templatet(P &program, const namespacet &ns): + cfg_dominators(ns) { compute(program); } protected: - cfg_dominators_templatet cfg_dominators; - typedef typename cfg_dominators_templatet::cfgt::nodet nodet; + cfg_dominators_templatet cfg_dominators; + typedef typename cfg_dominators_templatet:: + cfgt::nodet nodet; void compute(P &program); void compute_natural_loop(T, T); @@ -62,11 +66,19 @@ class natural_loops_templatet class natural_loopst: public natural_loops_templatet + goto_programt::const_targett, + false> { +public: + explicit natural_loopst(const namespacet &ns): + natural_loops_templatet(ns) + { + } }; -typedef natural_loops_templatet +typedef natural_loops_templatet natural_loops_mutablet; void show_natural_loops( @@ -78,8 +90,8 @@ void show_natural_loops( #include #endif -template -void natural_loops_templatet::compute(P &program) +template +void natural_loops_templatet::compute(P &program) { cfg_dominators(program); @@ -115,8 +127,8 @@ void natural_loops_templatet::compute(P &program) } /// Computes the natural loop for a given back-edge (see Muchnick section 7.4) -template -void natural_loops_templatet::compute_natural_loop(T m, T n) +template +void natural_loops_templatet::compute_natural_loop(T m, T n) { assert(n->location_number<=m->location_number); @@ -150,8 +162,8 @@ void natural_loops_templatet::compute_natural_loop(T m, T n) } /// Print all natural loops that were found -template -void natural_loops_templatet::output(std::ostream &out) const +template +void natural_loops_templatet::output(std::ostream &out) const { for(const auto &loop : loop_map) { diff --git a/src/goto-analyzer/unreachable_instructions.cpp b/src/goto-analyzer/unreachable_instructions.cpp index 0e783baaba5..37b637cfbe9 100644 --- a/src/goto-analyzer/unreachable_instructions.cpp +++ b/src/goto-analyzer/unreachable_instructions.cpp @@ -29,9 +29,10 @@ typedef std::map dead_mapt; static void unreachable_instructions( const goto_programt &goto_program, - dead_mapt &dest) + dead_mapt &dest, + const namespacet &ns) { - cfg_dominatorst dominators; + cfg_dominatorst dominators(ns); dominators(goto_program); for(cfg_dominatorst::cfgt::entry_mapt::const_iterator @@ -188,7 +189,7 @@ void unreachable_instructions( // base_name instead; do not list inlined functions if(called.find(decl.base_name)!=called.end() || f_it->second.is_inlined()) - unreachable_instructions(goto_program, dead_map); + unreachable_instructions(goto_program, dead_map, ns); else all_unreachable(goto_program, dead_map); diff --git a/src/goto-instrument/accelerate/accelerate.h b/src/goto-instrument/accelerate/accelerate.h index 05dec188f28..cc7134080c8 100644 --- a/src/goto-instrument/accelerate/accelerate.h +++ b/src/goto-instrument/accelerate/accelerate.h @@ -40,6 +40,7 @@ class acceleratet goto_functions(_goto_model.goto_functions), symbol_table(_goto_model.symbol_table), ns(_goto_model.symbol_table), + natural_loops(ns), utils(symbol_table, message_handler, goto_functions), use_z3(_use_z3) { diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index a33b0934349..198b93bcbc9 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -225,7 +225,7 @@ void code_contractst::code_contracts( goto_functionst::goto_functiont &goto_function) { local_may_aliast local_may_alias(goto_function); - natural_loops_mutablet natural_loops(goto_function.body); + natural_loops_mutablet natural_loops(goto_function.body, ns); // iterate over the (natural) loops in the function for(natural_loops_mutablet::loop_mapt::const_iterator diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp index ecd9c15ffbb..d085f73490a 100644 --- a/src/goto-instrument/count_eloc.cpp +++ b/src/goto-instrument/count_eloc.cpp @@ -97,7 +97,8 @@ void print_path_lengths(const goto_modelt &goto_model) }; typedef cfg_baset cfgt; - cfgt cfg; + namespacet ns(goto_model.symbol_table); + cfgt cfg(ns); cfg(goto_model.goto_functions); const goto_programt &start_program=start->second.body; diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 43e60c030e3..2e8e1031493 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -307,7 +307,13 @@ void full_slicert::operator()( add_to_queue(queue, e_it->second, e_it->first); else if(implicit(e_it->first)) add_to_queue(queue, e_it->second, e_it->first); - else if((e_it->first->is_goto() && e_it->first->guard.is_true()) || + // any jump (control transfer to an instruction other than the next one) + // that will always be taken, i.e., also include conditional jumps the + // condition of which always evaluates to true + else if((e_it->first->is_goto() && + cfg[e_it->second].out.size()==1 && + cfg[cfg[e_it->second].out.begin()->first].PC!= + std::next(e_it->first)) || e_it->first->is_throw()) jumps.push_back(e_it->second); else if(e_it->first->is_decl()) @@ -372,7 +378,8 @@ void full_slicer( const namespacet &ns, slicing_criteriont &criterion) { - full_slicert()(goto_functions, ns, criterion); + full_slicert s(ns); + s(goto_functions, ns, criterion); } void full_slicer( @@ -380,14 +387,15 @@ void full_slicer( const namespacet &ns) { assert_criteriont a; - full_slicert()(goto_functions, ns, a); + full_slicert s(ns); + s(goto_functions, ns, a); } void full_slicer(goto_modelt &goto_model) { assert_criteriont a; const namespacet ns(goto_model.symbol_table); - full_slicert()(goto_model.goto_functions, ns, a); + full_slicer(goto_model.goto_functions, ns); } void property_slicer( @@ -396,7 +404,8 @@ void property_slicer( const std::list &properties) { properties_criteriont p(properties); - full_slicert()(goto_functions, ns, p); + full_slicert s(ns); + s(goto_functions, ns, p); } void property_slicer( diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h index de1c50b54f4..2bdf209c302 100644 --- a/src/goto-instrument/full_slicer_class.h +++ b/src/goto-instrument/full_slicer_class.h @@ -38,6 +38,11 @@ echo 'digraph g {' > c.dot ; cat c.goto | \ class full_slicert { public: + explicit full_slicert(const namespacet &ns): + cfg(ns) + { + } + void operator()( goto_functionst &goto_functions, const namespacet &ns, diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index d5224337440..0f3483baa35 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -395,7 +395,7 @@ int goto_instrument_parse_optionst::doit() namespacet ns(goto_model.symbol_table); status() << "Pointer Analysis" << eom; - points_tot points_to; + points_tot points_to(ns); points_to(goto_model); points_to.output(std::cout); return CPROVER_EXIT_SUCCESS; diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp index d0339ec3ae8..0a8e78cc6fb 100644 --- a/src/goto-instrument/goto_program2code.cpp +++ b/src/goto-instrument/goto_program2code.cpp @@ -770,7 +770,7 @@ goto_programt::const_targett goto_program2codet::get_cases( bool goto_program2codet::set_block_end_points( goto_programt::const_targett upper_bound, - const cfg_dominatorst &dominators, + const syntactic_dominatorst &dominators, cases_listt &cases, std::set &processed_locations) { @@ -792,10 +792,10 @@ bool goto_program2codet::set_block_end_points( case_end!=upper_bound; ++case_end) { - cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry= + syntactic_dominatorst::cfgt::entry_mapt::const_iterator i_entry= dominators.cfg.entry_map.find(case_end); assert(i_entry!=dominators.cfg.entry_map.end()); - const cfg_dominatorst::cfgt::nodet &n= + const syntactic_dominatorst::cfgt::nodet &n= dominators.cfg[i_entry->second]; // ignore dead instructions for the following checks @@ -826,7 +826,7 @@ bool goto_program2codet::set_block_end_points( } bool goto_program2codet::remove_default( - const cfg_dominatorst &dominators, + const syntactic_dominatorst &dominators, const cases_listt &cases, goto_programt::const_targett default_target) { @@ -849,10 +849,10 @@ bool goto_program2codet::remove_default( next_case!=goto_program.instructions.end(); ++next_case) { - cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry= + syntactic_dominatorst::cfgt::entry_mapt::const_iterator i_entry= dominators.cfg.entry_map.find(next_case); assert(i_entry!=dominators.cfg.entry_map.end()); - const cfg_dominatorst::cfgt::nodet &n= + const syntactic_dominatorst::cfgt::nodet &n= dominators.cfg[i_entry->second]; if(!n.dominators.empty()) @@ -902,11 +902,11 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch( !skip_typecast(to_equal_expr(eq_cand).rhs()).is_constant()) return convert_goto_if(target, upper_bound, dest); - const cfg_dominatorst &dominators=loops.get_dominator_info(); + const syntactic_dominatorst &dominators=loops.get_dominator_info(); // always use convert_goto_if for dead code as the construction below relies // on effective dominator information - cfg_dominatorst::cfgt::entry_mapt::const_iterator t_entry= + syntactic_dominatorst::cfgt::entry_mapt::const_iterator t_entry= dominators.cfg.entry_map.find(target); assert(t_entry!=dominators.cfg.entry_map.end()); if(dominators.cfg[t_entry->second].dominators.empty()) @@ -1049,10 +1049,10 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch( if(processed_locations.find(it->location_number)== processed_locations.end()) { - cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry= + syntactic_dominatorst::cfgt::entry_mapt::const_iterator it_entry= dominators.cfg.entry_map.find(it); assert(it_entry!=dominators.cfg.entry_map.end()); - const cfg_dominatorst::cfgt::nodet &n= + const syntactic_dominatorst::cfgt::nodet &n= dominators.cfg[it_entry->second]; if(!n.dominators.empty()) @@ -1148,7 +1148,7 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue( codet &dest) { assert(!loop_last_stack.empty()); - const cfg_dominatorst &dominators=loops.get_dominator_info(); + const syntactic_dominatorst &dominators=loops.get_dominator_info(); // goto 1 // 1: ... @@ -1157,10 +1157,10 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue( next!=upper_bound && next!=goto_program.instructions.end(); ++next) { - cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry= + syntactic_dominatorst::cfgt::entry_mapt::const_iterator i_entry= dominators.cfg.entry_map.find(next); assert(i_entry!=dominators.cfg.entry_map.end()); - const cfg_dominatorst::cfgt::nodet &n= + const syntactic_dominatorst::cfgt::nodet &n= dominators.cfg[i_entry->second]; if(!n.dominators.empty()) @@ -1201,10 +1201,10 @@ goto_programt::const_targett goto_program2codet::convert_goto_break_continue( after_loop!=goto_program.instructions.end(); ++after_loop) { - cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry= + syntactic_dominatorst::cfgt::entry_mapt::const_iterator i_entry= dominators.cfg.entry_map.find(after_loop); assert(i_entry!=dominators.cfg.entry_map.end()); - const cfg_dominatorst::cfgt::nodet &n= + const syntactic_dominatorst::cfgt::nodet &n= dominators.cfg[i_entry->second]; if(!n.dominators.empty()) @@ -1241,11 +1241,11 @@ goto_programt::const_targett goto_program2codet::convert_goto_goto( if(target->get_target()==next) return target; - const cfg_dominatorst &dominators=loops.get_dominator_info(); - cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry= + const syntactic_dominatorst &dominators=loops.get_dominator_info(); + syntactic_dominatorst::cfgt::entry_mapt::const_iterator it_entry= dominators.cfg.entry_map.find(target); assert(it_entry!=dominators.cfg.entry_map.end()); - const cfg_dominatorst::cfgt::nodet &n= + const syntactic_dominatorst::cfgt::nodet &n= dominators.cfg[it_entry->second]; // skip dead goto L as the label might be skipped if it is dead diff --git a/src/goto-instrument/goto_program2code.h b/src/goto-instrument/goto_program2code.h index 2093774b709..a22b633363e 100644 --- a/src/goto-instrument/goto_program2code.h +++ b/src/goto-instrument/goto_program2code.h @@ -63,7 +63,8 @@ class goto_program2codet local_static(_local_static), type_names(_type_names), typedef_names(_typedef_names), - system_headers(_system_headers) + system_headers(_system_headers), + loops(ns) { assert(local_static.empty()); @@ -88,7 +89,18 @@ class goto_program2codet std::set &system_headers; std::unordered_set va_list_expr; - natural_loopst loops; + typedef natural_loops_templatet< + const goto_programt, + goto_programt::const_targett, + true> + natural_loops_no_simpt; + typedef cfg_dominators_templatet< + const goto_programt, + goto_programt::const_targett, + false, + true> + syntactic_dominatorst; + natural_loops_no_simpt loops; loopt loop_map; id_sett labels_in_use; dead_mapt dead_map; @@ -184,12 +196,12 @@ class goto_program2codet bool set_block_end_points( goto_programt::const_targett upper_bound, - const cfg_dominatorst &dominators, + const syntactic_dominatorst &dominators, cases_listt &cases, std::set &processed_locations); bool remove_default( - const cfg_dominatorst &dominators, + const syntactic_dominatorst &dominators, const cases_listt &cases, goto_programt::const_targett default_target); diff --git a/src/goto-instrument/havoc_loops.cpp b/src/goto-instrument/havoc_loops.cpp index 01bc2701dd8..1f9c9e00300 100644 --- a/src/goto-instrument/havoc_loops.cpp +++ b/src/goto-instrument/havoc_loops.cpp @@ -27,11 +27,12 @@ class havoc_loopst havoc_loopst( function_modifiest &_function_modifies, - goto_functiont &_goto_function): + goto_functiont &_goto_function, + const namespacet &ns): goto_function(_goto_function), local_may_alias(_goto_function), function_modifies(_function_modifies), - natural_loops(_goto_function.body) + natural_loops(_goto_function.body, ns) { havoc_loops(); } @@ -187,7 +188,8 @@ void havoc_loopst::havoc_loops() void havoc_loops(goto_modelt &goto_model) { function_modifiest function_modifies(goto_model.goto_functions); + namespacet ns(goto_model.symbol_table); Forall_goto_functions(it, goto_model.goto_functions) - havoc_loopst(function_modifies, it->second); + havoc_loopst(function_modifies, it->second, ns); } diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp index 900057f9f8b..c6b36893f08 100644 --- a/src/goto-instrument/k_induction.cpp +++ b/src/goto-instrument/k_induction.cpp @@ -28,11 +28,12 @@ class k_inductiont k_inductiont( goto_functiont &_goto_function, + const namespacet &ns, bool _base_case, bool _step_case, unsigned _k): goto_function(_goto_function), local_may_alias(_goto_function), - natural_loops(_goto_function.body), + natural_loops(_goto_function.body, ns), base_case(_base_case), step_case(_step_case), k(_k) { k_induction(); @@ -154,6 +155,8 @@ void k_induction( bool base_case, bool step_case, unsigned k) { + namespacet ns(goto_model.symbol_table); + Forall_goto_functions(it, goto_model.goto_functions) - k_inductiont(it->second, base_case, step_case, k); + k_inductiont(it->second, ns, base_case, step_case, k); } diff --git a/src/goto-instrument/points_to.h b/src/goto-instrument/points_to.h index 76775a6f636..6e8dd728f48 100644 --- a/src/goto-instrument/points_to.h +++ b/src/goto-instrument/points_to.h @@ -22,7 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com class points_tot { public: - points_tot() + explicit points_tot(const namespacet &ns):cfg(ns) { } diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index 9658c218a83..fca69018681 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -116,7 +116,8 @@ void reachability_slicer( goto_modelt &goto_model, const bool include_forward_reachability) { - reachability_slicert s; + namespacet ns(goto_model.symbol_table); + reachability_slicert s(ns); assert_criteriont a; s(goto_model.goto_functions, a, include_forward_reachability); } @@ -133,7 +134,8 @@ void reachability_slicer( const std::list &properties, const bool include_forward_reachability) { - reachability_slicert s; + namespacet ns(goto_model.symbol_table); + reachability_slicert s(ns); properties_criteriont p(properties); s(goto_model.goto_functions, p, include_forward_reachability); } diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h index 5f52a6d1795..2155fa7e7eb 100644 --- a/src/goto-instrument/reachability_slicer_class.h +++ b/src/goto-instrument/reachability_slicer_class.h @@ -22,6 +22,10 @@ class slicing_criteriont; class reachability_slicert { public: + explicit reachability_slicert(const namespacet &ns):cfg(ns) + { + } + void operator()( goto_functionst &goto_functions, slicing_criteriont &criterion, diff --git a/src/goto-programs/cfg.h b/src/goto-programs/cfg.h index da7bec886b9..8884791659f 100644 --- a/src/goto-programs/cfg.h +++ b/src/goto-programs/cfg.h @@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "goto_functions.h" @@ -58,8 +59,9 @@ struct cfg_base_nodet:public graph_nodet, public T /// specific edges constructed by operator() can be different in those. template -class cfg_baset:public grapht< cfg_base_nodet > + typename I=goto_programt::const_targett, + bool simp=true> +class cfg_baset:public grapht< cfg_base_nodet > { public: typedef std::size_t entryt; @@ -70,8 +72,6 @@ class cfg_baset:public grapht< cfg_base_nodet > data_typet data; public: - grapht< cfg_base_nodet > &container; - // NOLINTNEXTLINE(readability/identifiers) typedef data_typet::iterator iterator; // NOLINTNEXTLINE(readability/identifiers) @@ -102,10 +102,25 @@ class cfg_baset:public grapht< cfg_base_nodet > return e.first->second; } + + private: + friend cfg_baset; + + grapht< cfg_base_nodet > &container; + + entry_mapt( + const entry_mapt &other, + grapht< cfg_base_nodet > &_container): + data(other.data), + container(_container) + { + } }; entry_mapt entry_map; protected: + const namespacet &ns; + virtual void compute_edges_goto( const goto_programt &goto_program, const goto_programt::instructiont &instruction, @@ -150,7 +165,7 @@ class cfg_baset:public grapht< cfg_base_nodet > const goto_functionst &goto_functions); public: - cfg_baset():entry_map(*this) + explicit cfg_baset(const namespacet &_ns):entry_map(*this), ns(_ns) { } @@ -158,6 +173,11 @@ class cfg_baset:public grapht< cfg_base_nodet > { } + cfg_baset(const cfg_baset &other): + entry_map(other.entry_map, *this), ns(other.ns) + { + } + void operator()( const goto_functionst &goto_functions) { @@ -177,56 +197,82 @@ class cfg_baset:public grapht< cfg_base_nodet > template -class concurrent_cfg_baset:public virtual cfg_baset + typename I=goto_programt::const_targett, + bool simp=true> +class concurrent_cfg_baset:public virtual cfg_baset { +public: + explicit concurrent_cfg_baset(const namespacet &ns): + cfg_baset(ns) + { + } + protected: virtual void compute_edges_start_thread( const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, - typename cfg_baset::entryt &entry); + typename cfg_baset::entryt &entry); }; template -class procedure_local_cfg_baset:public virtual cfg_baset + typename I=goto_programt::const_targett, + bool simp=true> +class procedure_local_cfg_baset:public virtual cfg_baset { +public: + explicit procedure_local_cfg_baset(const namespacet &ns): + cfg_baset(ns) + { + } + protected: virtual void compute_edges_function_call( const goto_functionst &goto_functions, const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, - typename cfg_baset::entryt &entry); + typename cfg_baset::entryt &entry); }; template + typename I=goto_programt::const_targett, + bool simp=true> class procedure_local_concurrent_cfg_baset: - public concurrent_cfg_baset, - public procedure_local_cfg_baset + public concurrent_cfg_baset, + public procedure_local_cfg_baset { +public: + explicit procedure_local_concurrent_cfg_baset(const namespacet &ns): + concurrent_cfg_baset(ns), + procedure_local_cfg_baset(ns) + { + } }; -template -void cfg_baset::compute_edges_goto( +template +void cfg_baset::compute_edges_goto( const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, entryt &entry) { if(next_PC!=goto_program.instructions.end() && - !instruction.guard.is_true()) + !instruction.guard.is_true() && + (!S || !simplify_expr(instruction.guard, ns).is_true())) this->add_edge(entry, entry_map[next_PC]); - this->add_edge(entry, entry_map[instruction.get_target()]); + if(!instruction.guard.is_false() && + (!S || !simplify_expr(instruction.guard, ns).is_false())) + for(const auto &t : instruction.targets) + if(t!=goto_program.instructions.end()) + this->add_edge(entry, entry_map[t]); } -template -void cfg_baset::compute_edges_catch( +template +void cfg_baset::compute_edges_catch( const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, @@ -243,8 +289,8 @@ void cfg_baset::compute_edges_catch( this->add_edge(entry, entry_map[t]); } -template -void cfg_baset::compute_edges_throw( +template +void cfg_baset::compute_edges_throw( const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, @@ -253,8 +299,8 @@ void cfg_baset::compute_edges_throw( // no (trivial) successors } -template -void cfg_baset::compute_edges_start_thread( +template +void cfg_baset::compute_edges_start_thread( const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, @@ -264,14 +310,14 @@ void cfg_baset::compute_edges_start_thread( this->add_edge(entry, entry_map[next_PC]); } -template -void concurrent_cfg_baset::compute_edges_start_thread( +template +void concurrent_cfg_baset::compute_edges_start_thread( const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, - typename cfg_baset::entryt &entry) + typename cfg_baset::entryt &entry) { - cfg_baset::compute_edges_start_thread( + cfg_baset::compute_edges_start_thread( goto_program, instruction, next_PC, @@ -280,8 +326,8 @@ void concurrent_cfg_baset::compute_edges_start_thread( this->add_edge(entry, this->entry_map[instruction.get_target()]); } -template -void cfg_baset::compute_edges_function_call( +template +void cfg_baset::compute_edges_function_call( const goto_functionst &goto_functions, const goto_programt &goto_program, const goto_programt::instructiont &instruction, @@ -331,13 +377,13 @@ void cfg_baset::compute_edges_function_call( this->add_edge(entry, entry_map[next_PC]); } -template -void procedure_local_cfg_baset::compute_edges_function_call( +template +void procedure_local_cfg_baset::compute_edges_function_call( const goto_functionst &goto_functions, const goto_programt &goto_program, const goto_programt::instructiont &instruction, goto_programt::const_targett next_PC, - typename cfg_baset::entryt &entry) + typename cfg_baset::entryt &entry) { const exprt &function= to_code_function_call(instruction.code).function(); @@ -349,14 +395,15 @@ void procedure_local_cfg_baset::compute_edges_function_call( this->add_edge(entry, this->entry_map[next_PC]); } -template -void cfg_baset::compute_edges( +template +void cfg_baset::compute_edges( const goto_functionst &goto_functions, const goto_programt &goto_program, I PC) { const goto_programt::instructiont &instruction=*PC; entryt entry=entry_map[PC]; + assert(this->size()>entry); (*this)[entry].PC=PC; goto_programt::const_targett next_PC(PC); next_PC++; @@ -399,12 +446,13 @@ void cfg_baset::compute_edges( break; case ASSUME: + case ASSERT: // false guard -> no successor - if(instruction.guard.is_false()) + if(instruction.guard.is_false() || + (S && simplify_expr(instruction.guard, ns).is_false())) break; case ASSIGN: - case ASSERT: case OTHER: case RETURN: case SKIP: @@ -423,8 +471,8 @@ void cfg_baset::compute_edges( } } -template -void cfg_baset::compute_edges( +template +void cfg_baset::compute_edges( const goto_functionst &goto_functions, P &goto_program) { @@ -434,8 +482,8 @@ void cfg_baset::compute_edges( compute_edges(goto_functions, goto_program, it); } -template -void cfg_baset::compute_edges( +template +void cfg_baset::compute_edges( const goto_functionst &goto_functions) { forall_goto_functions(it, goto_functions)