diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index a03ba3270c8..6e52de794e5 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -411,7 +411,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, @@ -422,11 +422,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, @@ -537,6 +537,27 @@ 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) { diff --git a/src/analyses/ai.h b/src/analyses/ai.h index cec1e110cca..934e9ec6297 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -469,7 +469,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; @@ -505,6 +505,40 @@ 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 + // by 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 @@ -525,7 +559,8 @@ class ai_recursive_interproceduralt : public ai_baset 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,