diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 3fd897c0d14..350feea578b 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -410,7 +410,7 @@ bool ai_baset::visit_edge( return return_value; } -bool ai_baset::visit_edge_function_call( +bool ai_localt::visit_edge_function_call( const irep_idt &calling_function_id, trace_ptrt p_call, locationt l_return, @@ -421,11 +421,11 @@ bool ai_baset::visit_edge_function_call( const namespacet &ns) { messaget log(message_handler); - log.progress() << "ai_baset::visit_edge_function_call from " + log.progress() << "ai_localt::visit_edge_function_call from " << p_call->current_location()->location_number << " to " << l_return->location_number << messaget::eom; - // The default implementation is not interprocedural + // This implementation is not interprocedural // so the effects of the call are approximated but nothing else return visit_edge( calling_function_id, @@ -536,6 +536,47 @@ bool ai_baset::visit_end_function( return false; } +void ai_localt::operator()( + const goto_functionst &goto_functions, + const namespacet &ns) +{ + initialize(goto_functions); + for(const auto &gf_entry : goto_functions.function_map) + { + if(gf_entry.second.body_available()) + { + trace_ptrt p = entry_state(gf_entry.second.body); + fixedpoint(p, gf_entry.first, gf_entry.second.body, goto_functions, ns); + } + } + finalize(); +} + +void ai_localt::operator()(const abstract_goto_modelt &goto_model) +{ + const namespacet ns(goto_model.get_symbol_table()); + operator()(goto_model.get_goto_functions(), ns); +} + +void ai_recursive_interproceduralt:: +operator()(const goto_functionst &goto_functions, const namespacet &ns) +{ + initialize(goto_functions); + trace_ptrt p = entry_state(goto_functions); + fixedpoint(p, goto_functions, ns); + finalize(); +} + +void ai_recursive_interproceduralt::operator()( + const abstract_goto_modelt &goto_model) +{ + const namespacet ns(goto_model.get_symbol_table()); + initialize(goto_model.get_goto_functions()); + trace_ptrt p = entry_state(goto_model.get_goto_functions()); + fixedpoint(p, goto_model.get_goto_functions(), ns); + finalize(); +} + bool ai_recursive_interproceduralt::visit_edge_function_call( const irep_idt &calling_function_id, trace_ptrt p_call, diff --git a/src/analyses/ai.h b/src/analyses/ai.h index a4f0bc34e69..e904cadc8c3 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -153,28 +153,12 @@ class ai_baset } /// Run abstract interpretation on a whole program - void operator()( - const goto_functionst &goto_functions, - const namespacet &ns) - { - initialize(goto_functions); - trace_ptrt p = entry_state(goto_functions); - fixedpoint(p, goto_functions, ns); - finalize(); - } - - /// Run abstract interpretation on a whole program - void operator()(const abstract_goto_modelt &goto_model) - { - const namespacet ns(goto_model.get_symbol_table()); - initialize(goto_model.get_goto_functions()); - trace_ptrt p = entry_state(goto_model.get_goto_functions()); - fixedpoint(p, goto_model.get_goto_functions(), ns); - finalize(); - } + virtual void + operator()(const goto_functionst &goto_functions, const namespacet &ns) = 0; + virtual void operator()(const abstract_goto_modelt &goto_model) = 0; /// Run abstract interpretation on a single function - void operator()( + virtual void operator()( const irep_idt &function_id, const goto_functionst::goto_functiont &goto_function, const namespacet &ns) @@ -308,9 +292,7 @@ class ai_baset std::ostream &out) const; /// Output the abstract states for a whole program - void output( - const goto_modelt &goto_model, - std::ostream &out) const + virtual void output(const goto_modelt &goto_model, std::ostream &out) const { const namespacet ns(goto_model.symbol_table); output(ns, goto_model.goto_functions, out); @@ -485,7 +467,7 @@ class ai_baset working_sett &working_set, const goto_programt &callee, const goto_functionst &goto_functions, - const namespacet &ns); + const namespacet &ns) = 0; /// For creating history objects std::unique_ptr history_factory; @@ -521,6 +503,41 @@ class ai_baset message_handlert &message_handler; }; +// Perform function local analysis on all functions in a program. +// No interprocedural analysis other than what a domain does when +// visit()'ing an edge that skips a function call. +class ai_localt : public ai_baset +{ +public: + ai_localt( + std::unique_ptr &&hf, + std::unique_ptr &&df, + std::unique_ptr &&st, + message_handlert &mh) + : ai_baset(std::move(hf), std::move(df), std::move(st), mh) + { + } + + // Handle every function independently + void operator()(const goto_functionst &goto_functions, const namespacet &ns) + override; + void operator()(const abstract_goto_modelt &goto_model) override; + +protected: + // Implement the function that handles a single function call edge + // using a single edge that gets the domain to approximate the whole + // function call + bool visit_edge_function_call( + const irep_idt &calling_function_id, + trace_ptrt p_call, + locationt l_return, + const irep_idt &callee_function_id, + working_sett &working_set, + const goto_programt &callee, + const goto_functionst &goto_functions, + const namespacet &ns) override; +}; + // Perform interprocedural analysis by simply recursing in the interpreter // This can lead to a call stack overflow if the domain has a large height class ai_recursive_interproceduralt : public ai_baset @@ -535,8 +552,14 @@ class ai_recursive_interproceduralt : public ai_baset { } + // Whole program analysis by starting at the entry function and recursing + void operator()(const goto_functionst &goto_functions, const namespacet &ns) + override; + void operator()(const abstract_goto_modelt &goto_model) override; + protected: - // Override the function that handles a single function call edge + // Implement the function that handles a single function call edge + // by a recursive call to fixpoint bool visit_edge_function_call( const irep_idt &calling_function_id, trace_ptrt p_call, diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index fd249904404..6167b95afad 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -207,7 +207,7 @@ class constant_propagator_ait:public ait should_track_valuet should_track_value = track_all_values) : dirty(goto_function), should_track_value(should_track_value) { - operator()(function_identifier, goto_function, ns); + ai_baset::operator()(function_identifier, goto_function, ns); replace(goto_function, ns); } diff --git a/src/goto-analyzer/build_analyzer.cpp b/src/goto-analyzer/build_analyzer.cpp index ac8dd224462..0cd7baeb5fd 100644 --- a/src/goto-analyzer/build_analyzer.cpp +++ b/src/goto-analyzer/build_analyzer.cpp @@ -39,7 +39,8 @@ std::unique_ptr build_analyzer( // These support all of the option categories if( options.get_bool_option("recursive-interprocedural") || - options.get_bool_option("three-way-merge")) + options.get_bool_option("three-way-merge") || + options.get_bool_option("local") ||) { // Build the history factory std::unique_ptr hf = nullptr; @@ -111,6 +112,11 @@ std::unique_ptr build_analyzer( std::move(hf), std::move(df), std::move(st), mh); } } + else if(options.get_bool_option("local")) + { + return util_make_unique( + std::move(hf), std::move(df), std::move(st), mh); + } } } else if(options.get_bool_option("legacy-ait")) diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index f6463eca656..436f4a6ce1d 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -225,6 +225,8 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) options.set_option("recursive-interprocedural", true); else if(cmdline.isset("three-way-merge")) options.set_option("three-way-merge", true); + else if(cmdline.isset("local")) + options.set_option("local", true); else if(cmdline.isset("legacy-ait") || cmdline.isset("location-sensitive")) { options.set_option("legacy-ait", true); @@ -758,6 +760,7 @@ void goto_analyzer_parse_optionst::help() " reasoning\n" " {y--three-way-merge} \t use VSD's three-way merge on return from function" " call\n" + " {y--local} \t perform function-local analysis for every function\n" " {y--legacy-concurrent} \t legacy-ait with an extended fixed-point for" " concurrency\n" " {y--location-sensitive} \t use location-sensitive abstract interpreter\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index a78643b12d7..8c29f6add02 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -117,7 +117,8 @@ class optionst; "(recursive-interprocedural)" \ "(three-way-merge)" \ "(legacy-ait)" \ - "(legacy-concurrent)" + "(legacy-concurrent)" \ + "(local)" #define GOTO_ANALYSER_OPTIONS_HISTORY \ "(ahistorical)" \