From a1ee4159fbdbe48a6ed52b0927f9c116954bcdc5 Mon Sep 17 00:00:00 2001 From: Martin Brain Date: Sat, 9 Sep 2023 19:16:00 +0100 Subject: [PATCH] Remove the static_analysist framework. This has been deprecated for many many years and only had one user which was a more obscure feature of goto-instrument. ait is better in almost every direction. --- src/analyses/Makefile | 1 - src/analyses/README.md | 13 +- src/analyses/static_analysis.cpp | 530 ------------------------------- src/analyses/static_analysis.h | 411 ------------------------ 4 files changed, 2 insertions(+), 953 deletions(-) delete mode 100644 src/analyses/static_analysis.cpp delete mode 100644 src/analyses/static_analysis.h diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 798ee0c6704e..5afb3574c92b 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -29,7 +29,6 @@ SRC = ai.cpp \ locals.cpp \ reaching_definitions.cpp \ sese_regions.cpp \ - static_analysis.cpp \ uncaught_exceptions_analysis.cpp \ uninitialized_domain.cpp \ variable-sensitivity/abstract_environment.cpp \ diff --git a/src/analyses/README.md b/src/analyses/README.md index 13b036b15804..3f813c21c050 100644 --- a/src/analyses/README.md +++ b/src/analyses/README.md @@ -8,9 +8,8 @@ static analyses that instantiate them. \section analyses-frameworks Frameworks: -There are currently three abstract interpretation frameworks provided in this -directory. \ref analyses-ait, \ref analyses-flow-insensitive-analysis, and the -deprecated and obsolete \ref analyses-static-analysist. +There are currently two abstract interpretation frameworks provided in this +directory. \ref analyses-ait and \ref analyses-flow-insensitive-analysis. \subsection analyses-ait Abstract interpreter framework (ait) @@ -22,14 +21,6 @@ is provided by \ref ait. This analysis framework is currently location sensitive run after the function pointer removal and return removal passes. There is ongoing work to make this framework also support context sensitivity. -\subsection analyses-static-analysist Old Abstract interpreter framework (static_analysist) - -The obsolete static analysis framework \ref static_analysist is only used by -\ref value_set_analysist. This abstract interpretation framework is deprecated in -favour of \ref analyses-ait, and should not be used as the basis for new code. -This framework is location sensitive (one domain per code location), but is able -to be run before function pointer removal and return removal phases. - \subsection analyses-flow-insensitive-analysis Flow-insensitive analysis (flow_insensitive_analysist) Framework for flow-insensitive analyses. Maintains a single global abstract diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp deleted file mode 100644 index 566f2816782a..000000000000 --- a/src/analyses/static_analysis.cpp +++ /dev/null @@ -1,530 +0,0 @@ -/*******************************************************************\ - -Module: Value Set Propagation - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Value Set Propagation - -#define USE_DEPRECATED_STATIC_ANALYSIS_H -#include "static_analysis.h" - -#include - -#include -#include - -#include "is_threaded.h" - -exprt static_analysis_baset::get_guard( - locationt from, - locationt to) -{ - if(!from->is_goto()) - return true_exprt(); - else if(std::next(from) == to) - return boolean_negate(from->condition()); - else - return from->condition(); -} - -exprt static_analysis_baset::get_return_lhs(locationt to) -{ - // get predecessor of "to" - - to--; - - if(to->is_end_function()) - return static_cast(get_nil_irep()); - - DATA_INVARIANT(to->is_function_call(), "must be the function call"); - - return to->call_lhs(); -} - -void static_analysis_baset::operator()( - const goto_functionst &goto_functions) -{ - initialize(goto_functions); - fixedpoint(goto_functions); -} - -void static_analysis_baset::operator()( - const irep_idt &function_identifier, - const goto_programt &goto_program) -{ - initialize(goto_program); - goto_functionst goto_functions; - fixedpoint(function_identifier, goto_program, goto_functions); -} - -void static_analysis_baset::output( - const goto_functionst &goto_functions, - std::ostream &out) const -{ - for(const auto &gf_entry : goto_functions.function_map) - { - if(gf_entry.second.body_available()) - { - out << "////\n"; - out << "//// Function: " << gf_entry.first << "\n"; - out << "////\n"; - out << "\n"; - - output(gf_entry.second.body, gf_entry.first, out); - } - } -} - -void static_analysis_baset::output( - const goto_programt &goto_program, - const irep_idt &, - std::ostream &out) const -{ - forall_goto_program_instructions(i_it, goto_program) - { - out << "**** " << i_it->location_number << " " << i_it->source_location() - << "\n"; - - get_state(i_it).output(ns, out); - out << "\n"; - #if 0 - i_it->output(out); - out << "\n"; - #endif - } -} - -void static_analysis_baset::generate_states( - const goto_functionst &goto_functions) -{ - for(const auto &gf_entry : goto_functions.function_map) - generate_states(gf_entry.second.body); -} - -void static_analysis_baset::generate_states( - const goto_programt &goto_program) -{ - forall_goto_program_instructions(i_it, goto_program) - generate_state(i_it); -} - -void static_analysis_baset::update( - const goto_functionst &goto_functions) -{ - for(const auto &gf_entry : goto_functions.function_map) - update(gf_entry.second.body); -} - -void static_analysis_baset::update( - const goto_programt &goto_program) -{ - locationt previous; - bool first=true; - - forall_goto_program_instructions(i_it, goto_program) - { - // do we have it already? - if(!has_location(i_it)) - { - generate_state(i_it); - - if(!first) - merge(get_state(i_it), get_state(previous), i_it); - } - - first=false; - previous=i_it; - } -} - -static_analysis_baset::locationt static_analysis_baset::get_next( - working_sett &working_set) -{ - PRECONDITION(!working_set.empty()); - - working_sett::iterator i=working_set.begin(); - locationt l=i->second; - working_set.erase(i); - - return l; -} - -bool static_analysis_baset::fixedpoint( - const irep_idt &function_identifier, - const goto_programt &goto_program, - const goto_functionst &goto_functions) -{ - if(goto_program.instructions.empty()) - return false; - - working_sett working_set; - - put_in_working_set( - working_set, - goto_program.instructions.begin()); - - bool new_data=false; - - while(!working_set.empty()) - { - locationt l=get_next(working_set); - - if(visit(function_identifier, l, working_set, goto_program, goto_functions)) - new_data=true; - } - - return new_data; -} - -bool static_analysis_baset::visit( - const irep_idt &function_identifier, - locationt l, - working_sett &working_set, - const goto_programt &goto_program, - const goto_functionst &goto_functions) -{ - bool new_data=false; - - statet ¤t=get_state(l); - - current.seen=true; - - for(const auto &to_l : goto_program.get_successors(l)) - { - if(to_l==goto_program.instructions.end()) - continue; - - std::unique_ptr tmp_state( - make_temporary_state(current)); - - statet &new_values=*tmp_state; - - if(l->is_function_call()) - { - // this is a big special case - do_function_call_rec( - function_identifier, - l, - to_l, - l->call_function(), - l->call_arguments(), - new_values, - goto_functions); - } - else - new_values.transform( - ns, function_identifier, l, function_identifier, to_l); - - statet &other=get_state(to_l); - - bool have_new_values= - merge(other, new_values, to_l); - - if(have_new_values) - new_data=true; - - if(have_new_values || !other.seen) - put_in_working_set(working_set, to_l); - } - - return new_data; -} - -void static_analysis_baset::do_function_call( - const irep_idt &calling_function, - locationt l_call, - locationt l_return, - const goto_functionst &goto_functions, - const goto_functionst::function_mapt::const_iterator f_it, - const exprt::operandst &, - statet &new_state) -{ - const goto_functionst::goto_functiont &goto_function=f_it->second; - - if(!goto_function.body_available()) - return; // do nothing - - CHECK_RETURN(!goto_function.body.instructions.empty()); - - { - // get the state at the beginning of the function - locationt l_begin=goto_function.body.instructions.begin(); - - // do the edge from the call site to the beginning of the function - std::unique_ptr tmp_state(make_temporary_state(new_state)); - tmp_state->transform(ns, calling_function, l_call, f_it->first, l_begin); - - statet &begin_state=get_state(l_begin); - - bool new_data=false; - - // merge the new stuff - if(merge(begin_state, *tmp_state, l_begin)) - new_data=true; - - // do each function at least once - if(functions_done.find(f_it->first)== - functions_done.end()) - { - new_data=true; - functions_done.insert(f_it->first); - } - - // do we need to do the fixedpoint of the body? - if(new_data) - { - // recursive call - fixedpoint(f_it->first, goto_function.body, goto_functions); - } - } - - { - // get location at end of procedure - locationt l_end=--goto_function.body.instructions.end(); - - DATA_INVARIANT(l_end->is_end_function(), "must be end of function"); - - statet &end_of_function=get_state(l_end); - - // do edge from end of function to instruction after call - std::unique_ptr tmp_state( - make_temporary_state(end_of_function)); - tmp_state->transform(ns, f_it->first, l_end, calling_function, l_return); - - // propagate those -- not exceedingly precise, this is, - // as still it contains all the state from the - // call site - merge(new_state, *tmp_state, l_return); - } - - { - // effect on current procedure (if any) - new_state.transform( - ns, calling_function, l_call, calling_function, l_return); - } -} - -void static_analysis_baset::do_function_call_rec( - const irep_idt &calling_function, - locationt l_call, - locationt l_return, - const exprt &function, - const exprt::operandst &arguments, - statet &new_state, - const goto_functionst &goto_functions) -{ - // see if we have the functions at all - if(goto_functions.function_map.empty()) - return; - - if(function.id()==ID_symbol) - { - const irep_idt &identifier = to_symbol_expr(function).get_identifier(); - - if(recursion_set.find(identifier)!=recursion_set.end()) - { - // recursion detected! - return; - } - else - recursion_set.insert(identifier); - - goto_functionst::function_mapt::const_iterator it= - goto_functions.function_map.find(identifier); - - if(it==goto_functions.function_map.end()) - throw "failed to find function "+id2string(identifier); - - do_function_call( - calling_function, - l_call, - l_return, - goto_functions, - it, - arguments, - new_state); - - recursion_set.erase(identifier); - } - else if(function.id()==ID_if) - { - if(function.operands().size()!=3) - throw "if takes three arguments"; - - std::unique_ptr n2(make_temporary_state(new_state)); - - do_function_call_rec( - calling_function, - l_call, - l_return, - to_if_expr(function).true_case(), - arguments, - new_state, - goto_functions); - - do_function_call_rec( - calling_function, - l_call, - l_return, - to_if_expr(function).false_case(), - arguments, - *n2, - goto_functions); - - merge(new_state, *n2, l_return); - } - else if(function.id()==ID_dereference) - { - // get value set - std::list values; - get_reference_set(l_call, function, values); - - std::unique_ptr state_from(make_temporary_state(new_state)); - - // now call all of these - for(const auto &value : values) - { - if(value.id()==ID_object_descriptor) - { - const object_descriptor_exprt &o=to_object_descriptor_expr(value); - std::unique_ptr n2(make_temporary_state(new_state)); - do_function_call_rec( - calling_function, - l_call, - l_return, - o.object(), - arguments, - *n2, - goto_functions); - merge(new_state, *n2, l_return); - } - } - } - else if(function.id() == ID_null_object || - function.id() == ID_integer_address) - { - // ignore, can't be a function - } - else if(function.id()==ID_member || function.id()==ID_index) - { - // ignore, can't be a function - } - else if(function.id()=="builtin-function") - { - // ignore, someone else needs to worry about this - } - else - { - throw "unexpected function_call argument: "+ - function.id_string(); - } -} - -void static_analysis_baset::sequential_fixedpoint( - const goto_functionst &goto_functions) -{ - // do each function at least once - - for(const auto &gf_entry : goto_functions.function_map) - { - if(functions_done.insert(gf_entry.first).second) - fixedpoint(gf_entry.first, gf_entry.second.body, goto_functions); - } -} - -void static_analysis_baset::concurrent_fixedpoint( - const goto_functionst &goto_functions) -{ - sequential_fixedpoint(goto_functions); - - is_threadedt is_threaded(goto_functions); - - // construct an initial shared state collecting the results of all - // functions - goto_programt tmp; - tmp.add_instruction(); - goto_programt::const_targett sh_target=tmp.instructions.begin(); - generate_state(sh_target); - statet &shared_state=get_state(sh_target); - - struct wl_entryt - { - wl_entryt( - const irep_idt &_function_identifier, - const goto_programt &_goto_program, - locationt _location) - : function_identifier(_function_identifier), - goto_program(&_goto_program), - location(_location) - { - } - - irep_idt function_identifier; - const goto_programt *goto_program; - locationt location; - }; - - typedef std::list thread_wlt; - thread_wlt thread_wl; - - for(const auto &gf_entry : goto_functions.function_map) - { - forall_goto_program_instructions(t_it, gf_entry.second.body) - { - if(is_threaded(t_it)) - { - thread_wl.push_back( - wl_entryt(gf_entry.first, gf_entry.second.body, t_it)); - - goto_programt::const_targett l_end = - gf_entry.second.body.instructions.end(); - --l_end; - - const statet &end_state=get_state(l_end); - merge_shared(shared_state, end_state, sh_target); - } - } - } - - // new feed in the shared state into all concurrently executing - // functions, and iterate until the shared state stabilizes - bool new_shared=true; - while(new_shared) - { - new_shared=false; - - for(const auto &thread : thread_wl) - { - working_sett working_set; - put_in_working_set(working_set, thread.location); - - statet &begin_state = get_state(thread.location); - merge(begin_state, shared_state, thread.location); - - while(!working_set.empty()) - { - goto_programt::const_targett l=get_next(working_set); - - visit( - thread.function_identifier, - l, - working_set, - *thread.goto_program, - goto_functions); - - // the underlying domain must make sure that the final state - // carries all possible values; otherwise we would need to - // merge over each and every state - if(l->is_end_function()) - { - statet &end_state=get_state(l); - new_shared|=merge_shared(shared_state, end_state, sh_target); - } - } - } - } -} diff --git a/src/analyses/static_analysis.h b/src/analyses/static_analysis.h deleted file mode 100644 index 75b5ed816d17..000000000000 --- a/src/analyses/static_analysis.h +++ /dev/null @@ -1,411 +0,0 @@ -/*******************************************************************\ - -Module: Static Analysis - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Static Analysis - -#ifndef CPROVER_ANALYSES_STATIC_ANALYSIS_H -#define CPROVER_ANALYSES_STATIC_ANALYSIS_H - -#ifndef USE_DEPRECATED_STATIC_ANALYSIS_H -#error Deprecated, use ai.h instead -#endif - -#include -#include -#include -#include - -#include - -#include - -// don't use me -- I am just a base class -// please derive from me -class domain_baset -{ -public: - domain_baset():seen(false) - { - } - - virtual ~domain_baset() - { - } - - typedef goto_programt::const_targett locationt; - - // will go away, - // to be replaced by a factory class option to static_analysist - virtual void initialize( - const namespacet &, - locationt) - { - } - - // how function calls are treated: - // a) there is an edge from each call site to the function head - // b) there is an edge from each return to the last instruction (END_FUNCTION) - // of each function - // c) there is an edge from the last instruction of the function - // to the instruction following the call site - // (for setting the LHS) - - virtual void transform( - const namespacet &ns, - const irep_idt &function_from, - locationt from, - const irep_idt &function_to, - locationt to) = 0; - - virtual void output( - const namespacet &, - std::ostream &) const - { - } - - typedef std::unordered_set expr_sett; - - // will go away - virtual void get_reference_set( - const namespacet &, - const exprt &, - std::list &dest) - { - // dummy, overload me! - dest.clear(); - } - - // also add - // - // bool merge(const T &b, locationt to); - // - // this computes the join between "this" and "b" - // return true if "this" has changed - -protected: - bool seen; - - friend class static_analysis_baset; -}; - -// don't use me -- I am just a base class -// use static_analysist instead -class static_analysis_baset -{ -public: - typedef domain_baset statet; - typedef goto_programt::const_targett locationt; - - explicit static_analysis_baset(const namespacet &_ns): - ns(_ns), - initialized(false) - { - } - - virtual void initialize( - const goto_programt &goto_program) - { - if(!initialized) - { - initialized=true; - generate_states(goto_program); - } - } - - virtual void initialize( - const goto_functionst &goto_functions) - { - if(!initialized) - { - initialized=true; - generate_states(goto_functions); - } - } - - virtual void update(const goto_programt &goto_program); - virtual void update(const goto_functionst &goto_functions); - - virtual void operator()( - const irep_idt &function_identifier, - const goto_programt &goto_program); - - virtual void operator()( - const goto_functionst &goto_functions); - - virtual ~static_analysis_baset() - { - } - - virtual void clear() - { - initialized=false; - } - - virtual void output( - const goto_functionst &goto_functions, - std::ostream &out) const; - - void output( - const goto_programt &goto_program, - std::ostream &out) const - { - output(goto_program, irep_idt(), out); - } - - virtual bool has_location(locationt l) const=0; - - void insert(locationt l) - { - generate_state(l); - } - - // utilities - - // get guard of a conditional edge - static exprt get_guard(locationt from, locationt to); - - // get lhs that return value is assigned to - // for an edge that returns from a function - static exprt get_return_lhs(locationt to); - -protected: - const namespacet &ns; - - virtual void output( - const goto_programt &goto_program, - const irep_idt &identifier, - std::ostream &out) const; - - typedef std::map working_sett; - - locationt get_next(working_sett &working_set); - - void put_in_working_set( - working_sett &working_set, - locationt l) - { - working_set.insert( - std::pair(l->location_number, l)); - } - - // true = found something new - bool fixedpoint( - const irep_idt &function_identifier, - const goto_programt &goto_program, - const goto_functionst &goto_functions); - - virtual void fixedpoint( - const goto_functionst &goto_functions)=0; - - void sequential_fixedpoint( - const goto_functionst &goto_functions); - void concurrent_fixedpoint( - const goto_functionst &goto_functions); - - // true = found something new - bool visit( - const irep_idt &function_identifier, - locationt l, - working_sett &working_set, - const goto_programt &goto_program, - const goto_functionst &goto_functions); - - static locationt successor(locationt l) - { - l++; - return l; - } - - virtual bool merge(statet &a, const statet &b, locationt to)=0; - // for concurrent fixedpoint - virtual bool merge_shared(statet &a, const statet &b, locationt to)=0; - - typedef std::set functions_donet; - functions_donet functions_done; - - typedef std::set recursion_sett; - recursion_sett recursion_set; - - void generate_states( - const goto_functionst &goto_functions); - - void generate_states( - const goto_programt &goto_program); - - bool initialized; - - // function calls - void do_function_call_rec( - const irep_idt &calling_function, - locationt l_call, - locationt l_return, - const exprt &function, - const exprt::operandst &arguments, - statet &new_state, - const goto_functionst &goto_functions); - - void do_function_call( - const irep_idt &calling_function, - locationt l_call, - locationt l_return, - const goto_functionst &goto_functions, - const goto_functionst::function_mapt::const_iterator f_it, - const exprt::operandst &arguments, - statet &new_state); - - // abstract methods - - virtual void generate_state(locationt l)=0; - virtual statet &get_state(locationt l)=0; - virtual const statet &get_state(locationt l) const=0; - virtual std::unique_ptr make_temporary_state(statet &s)=0; - - typedef domain_baset::expr_sett expr_sett; - - virtual void get_reference_set( - locationt l, - const exprt &expr, - std::list &dest)=0; -}; - -// T is expected to be derived from domain_baset -template -class static_analysist:public static_analysis_baset -{ -public: - // constructor - explicit static_analysist(const namespacet &_ns): - static_analysis_baset(_ns) - { - } - - typedef goto_programt::const_targett locationt; - - T &operator[](locationt l) - { - typename state_mapt::iterator it=state_map.find(l); - if(it==state_map.end()) - throw std::out_of_range("failed to find state"); - - return it->second; - } - - const T &operator[](locationt l) const - { - typename state_mapt::const_iterator it=state_map.find(l); - if(it==state_map.end()) - throw std::out_of_range("failed to find state"); - - return it->second; - } - - virtual void clear() - { - state_map.clear(); - static_analysis_baset::clear(); - } - - virtual bool has_location(locationt l) const - { - return state_map.count(l)!=0; - } - -protected: - typedef std::map state_mapt; - state_mapt state_map; - - virtual statet &get_state(locationt l) - { - typename state_mapt::iterator it=state_map.find(l); - if(it==state_map.end()) - throw std::out_of_range("failed to find state"); - - return it->second; - } - - virtual const statet &get_state(locationt l) const - { - typename state_mapt::const_iterator it=state_map.find(l); - if(it==state_map.end()) - throw std::out_of_range("failed to find state"); - - return it->second; - } - - virtual bool merge(statet &a, const statet &b, locationt to) - { - return static_cast(a).merge(static_cast(b), to); - } - - virtual std::unique_ptr make_temporary_state(statet &s) - { - return util_make_unique(static_cast(s)); - } - - virtual void generate_state(locationt l) - { - state_map[l].initialize(ns, l); - } - - virtual void get_reference_set( - locationt l, - const exprt &expr, - std::list &dest) - { - state_map[l].get_reference_set(ns, expr, dest); - } - - virtual void fixedpoint(const goto_functionst &goto_functions) - { - sequential_fixedpoint(goto_functions); - } - -private: - // to enforce that T is derived from domain_baset - void dummy(const T &s) { const statet &x=dummy1(s); (void)x; } - - // not implemented in sequential analyses - virtual bool merge_shared( - statet &, - const statet &, - goto_programt::const_targett) - { - throw "not implemented"; - } -}; - -template -class concurrency_aware_static_analysist:public static_analysist -{ -public: - // constructor - explicit concurrency_aware_static_analysist(const namespacet &_ns): - static_analysist(_ns) - { - } - - virtual bool merge_shared( - static_analysis_baset::statet &a, - const static_analysis_baset::statet &b, - goto_programt::const_targett to) - { - return static_cast(a).merge_shared( - this->ns, - static_cast(b), - to); - } - -protected: - virtual void fixedpoint(const goto_functionst &goto_functions) - { - this->concurrent_fixedpoint(goto_functions); - } -}; - -#endif // CPROVER_ANALYSES_STATIC_ANALYSIS_H