From ac5af68d8d41e402dd1a53f316899e0d45d4e16d Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 17 Jan 2018 11:17:17 +0000 Subject: [PATCH 1/3] Address-taken locals analysis: support incremental analysis This adds a constructor and incremental build function so that the set of address-taken locals can be populated one function at a time. This will be useful when goto-symex begins to use incremental loading, meaning it cannot populate the analysis in one operation. --- src/analyses/dirty.cpp | 11 +++++++++++ src/analyses/dirty.h | 32 ++++++++++++++++++++++++++++++++ 2 files changed, 43 insertions(+) diff --git a/src/analyses/dirty.cpp b/src/analyses/dirty.cpp index 0231b50c77c..b40e057a975 100644 --- a/src/analyses/dirty.cpp +++ b/src/analyses/dirty.cpp @@ -72,3 +72,14 @@ void dirtyt::output(std::ostream &out) const for(const auto &d : dirty) out << d << '\n'; } + +/// Analyse the given function with dirtyt if it hasn't been seen before +/// \param id: function id to analyse +/// \param function: function to analyse +void incremental_dirtyt::populate_dirty_for_function( + const irep_idt &id, const goto_functionst::goto_functiont &function) +{ + auto insert_result = dirty_processed_functions.insert(id); + if(insert_result.second) + dirty.add_function(function); +} diff --git a/src/analyses/dirty.h b/src/analyses/dirty.h index 52801d05281..880d01cb3ee 100644 --- a/src/analyses/dirty.h +++ b/src/analyses/dirty.h @@ -25,6 +25,10 @@ class dirtyt typedef std::unordered_set id_sett; typedef goto_functionst::goto_functiont goto_functiont; + dirtyt() + { + } + explicit dirtyt(const goto_functiont &goto_function) { build(goto_function); @@ -53,6 +57,11 @@ class dirtyt return dirty; } + void add_function(const goto_functiont &goto_function) + { + build(goto_function); + } + protected: void build(const goto_functiont &goto_function); @@ -71,4 +80,27 @@ inline std::ostream &operator<<( return out; } +/// Wrapper for dirtyt that permits incremental population, ensuring each +/// function is analysed exactly once. +class incremental_dirtyt +{ +public: + void populate_dirty_for_function( + const irep_idt &id, const goto_functionst::goto_functiont &function); + + bool operator()(const irep_idt &id) const + { + return dirty(id); + } + + bool operator()(const symbol_exprt &expr) const + { + return dirty(expr); + } + +private: + dirtyt dirty; + std::unordered_set dirty_processed_functions; +}; + #endif // CPROVER_ANALYSES_DIRTY_H From 9e31303f27ddbcb7fc48157b04cf712a4038196a Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 17 Jan 2018 11:19:02 +0000 Subject: [PATCH 2/3] Symex: switch to incrementally populating address-taken locals This populates address-taken locals as each function is first encountered, rather than analysing every function up front. This lays the groundwork for moving to incremental function loading. --- src/goto-symex/goto_symex_state.h | 7 +++++-- src/goto-symex/symex_function_call.cpp | 3 +++ src/goto-symex/symex_main.cpp | 13 +++++++++++-- 3 files changed, 19 insertions(+), 4 deletions(-) diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index 37d7d94d334..bbbc9b64d92 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -26,7 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "symex_target.h" -class dirtyt; +class incremental_dirtyt; // central data structure: state class goto_symex_statet final @@ -340,9 +340,12 @@ class goto_symex_statet final bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns); bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns); + void populate_dirty_for_function( + const irep_idt &id, const goto_functionst::goto_functiont &); + void switch_to_thread(unsigned t); bool record_events; - std::unique_ptr dirty; + std::unique_ptr dirty; }; #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index cfd98415367..55c8a66a1d7 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -235,6 +235,9 @@ void goto_symext::symex_function_call_code( const goto_functionst::goto_functiont &goto_function=it->second; + if(state.dirty) + state.dirty->populate_dirty_for_function(identifier, goto_function); + const bool stop_recursing=get_unwind_recursion( identifier, state.source.thread_nr, diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 3273041479d..191d4ec4e74 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -136,8 +136,17 @@ void goto_symext::initialize_entry_point( state.top().end_of_function=limit; state.top().calling_location.pc=state.top().end_of_function; state.symex_target=⌖ - state.dirty=util_make_unique(goto_functions); - + state.dirty=util_make_unique(); + if(!pc->function.empty()) + { + state.dirty->populate_dirty_for_function( + pc->function, goto_functions.function_map.at(pc->function)); + } + else + { + log.warning() << "Unable to analyse address-taken locals, as start " + "instruction does not state its function" << messaget::eom; + } symex_transition(state, state.source.pc); } From e918a91e185b453126946e767e19267313188bd5 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 17 Jan 2018 15:50:36 +0000 Subject: [PATCH 3/3] Goto-symex: add support for general function accessor Previously goto-symex presumed access to goto_functionst; now it only requires a function that somehow yields a goto_functiont. This will facilitate integration with lazy_goto_modelt, and in future any other kind of on-demand goto_functiont production. --- src/cbmc/symex_bmc.cpp | 6 +- src/cbmc/symex_bmc.h | 2 +- src/goto-symex/goto_symex.h | 57 ++++++++++++++--- src/goto-symex/symex_function_call.cpp | 21 ++---- src/goto-symex/symex_main.cpp | 88 ++++++++++++++++++-------- src/goto-symex/symex_other.cpp | 1 - 6 files changed, 119 insertions(+), 56 deletions(-) diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp index 31bc6acbb19..45615063cc9 100644 --- a/src/cbmc/symex_bmc.cpp +++ b/src/cbmc/symex_bmc.cpp @@ -31,7 +31,7 @@ symex_bmct::symex_bmct( /// show progress void symex_bmct::symex_step( - const goto_functionst &goto_functions, + const get_goto_functiont &get_goto_function, statet &state) { const source_locationt &source_location=state.source.pc->source_location; @@ -63,12 +63,12 @@ void symex_bmct::symex_step( log.statistics() << log.eom; } - goto_symext::symex_step(goto_functions, state); + goto_symext::symex_step(get_goto_function, state); if(record_coverage && // avoid an invalid iterator in state.source.pc (!cur_pc->is_end_function() || - cur_pc->function!=goto_functions.entry_point())) + cur_pc->function!=goto_functionst::entry_point())) { // forward goto will effectively be covered via phi function, // which does not invoke symex_step; as symex_step is called diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h index fb43bca88ee..02f9ba6a561 100644 --- a/src/cbmc/symex_bmc.h +++ b/src/cbmc/symex_bmc.h @@ -128,7 +128,7 @@ class symex_bmct: public goto_symext // overloaded from goto_symext // virtual void symex_step( - const goto_functionst &goto_functions, + const get_goto_functiont &get_goto_function, statet &state); virtual void merge_goto( diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 773aa721d70..385c10905cf 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -67,6 +67,10 @@ class goto_symext typedef goto_symex_statet statet; + typedef + std::function + get_goto_functiont; + /// \brief symex entire program starting from entry point /// /// The state that goto_symext maintains has a large memory footprint. @@ -76,6 +80,15 @@ class goto_symext virtual void symex_from_entry_point_of( const goto_functionst &goto_functions); + /// \brief symex entire program starting from entry point + /// + /// The state that goto_symext maintains has a large memory footprint. + /// This method deallocates the state as soon as symbolic execution + /// has completed, so use it if you don't care about having the state + /// around afterwards. + virtual void symex_from_entry_point_of( + const get_goto_functiont &get_goto_function); + //// \brief symex entire program starting from entry point /// /// This method uses the `state` argument as the symbolic execution @@ -88,6 +101,18 @@ class goto_symext const goto_functionst &, const goto_programt &); + //// \brief symex entire program starting from entry point + /// + /// This method uses the `state` argument as the symbolic execution + /// state, which is useful for examining the state after this method + /// returns. The state that goto_symext maintains has a large memory + /// footprint, so if keeping the state around is not necessary, + /// clients should instead call goto_symext::symex_from_entry_point_of(). + virtual void symex_with_state( + statet &, + const get_goto_functiont &, + const goto_programt &); + /// Symexes from the first instruction and the given state, terminating as /// soon as the last instruction is reached. This is useful to explicitly /// symex certain ranges of a program, e.g. in an incremental decision @@ -102,6 +127,20 @@ class goto_symext goto_programt::const_targett first, goto_programt::const_targett limit); + /// Symexes from the first instruction and the given state, terminating as + /// soon as the last instruction is reached. This is useful to explicitly + /// symex certain ranges of a program, e.g. in an incremental decision + /// procedure. + /// \param state Symex state to start with. + /// \param get_goto_function retrieves a function body + /// \param first Entry point in form of a first instruction. + /// \param limit Final instruction, which itself will not be symexed. + virtual void symex_instruction_range( + statet &state, + const get_goto_functiont &get_goto_function, + goto_programt::const_targett first, + goto_programt::const_targett limit); + protected: /// Initialise the symbolic execution and the given state with pc /// as entry point. @@ -111,21 +150,21 @@ class goto_symext /// \param limit final instruction, which itself will not /// be symexed. void initialize_entry_point( - statet &, - const goto_functionst &, + statet &state, + const get_goto_functiont &get_goto_function, goto_programt::const_targett pc, goto_programt::const_targett limit); /// Invokes symex_step and verifies whether additional threads can be /// executed. /// \param state Current GOTO symex step. - /// \param goto_functions GOTO model to symex. + /// \param get_goto_function function that retrieves function bodies void symex_threaded_step( - statet &, const goto_functionst &); + statet &, const get_goto_functiont &); /** execute just one step */ virtual void symex_step( - const goto_functionst &, + const get_goto_functiont &, statet &); public: @@ -213,7 +252,7 @@ class goto_symext virtual void symex_decl(statet &); virtual void symex_decl(statet &, const symbol_exprt &expr); virtual void symex_dead(statet &); - virtual void symex_other(const goto_functionst &, statet &); + virtual void symex_other(statet &); virtual void vcc( const exprt &, @@ -255,19 +294,19 @@ class goto_symext } virtual void symex_function_call( - const goto_functionst &, + const get_goto_functiont &, statet &, const code_function_callt &); virtual void symex_end_of_function(statet &); virtual void symex_function_call_symbol( - const goto_functionst &, + const get_goto_functiont &, statet &, const code_function_callt &); virtual void symex_function_call_code( - const goto_functionst &, + const get_goto_functiont &, statet &, const code_function_callt &); diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 55c8a66a1d7..15daefbee4a 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -172,14 +172,14 @@ void goto_symext::parameter_assignments( } void goto_symext::symex_function_call( - const goto_functionst &goto_functions, + const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &code) { const exprt &function=code.function(); if(function.id()==ID_symbol) - symex_function_call_symbol(goto_functions, state, code); + symex_function_call_symbol(get_goto_function, state, code); else if(function.id()==ID_if) throw "symex_function_call can't do if"; else if(function.id()==ID_dereference) @@ -189,7 +189,7 @@ void goto_symext::symex_function_call( } void goto_symext::symex_function_call_symbol( - const goto_functionst &goto_functions, + const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &code) { @@ -213,27 +213,20 @@ void goto_symext::symex_function_call_symbol( symex_macro(state, code); } else - symex_function_call_code(goto_functions, state, code); + symex_function_call_code(get_goto_function, state, code); } /// do function call by inlining void goto_symext::symex_function_call_code( - const goto_functionst &goto_functions, + const get_goto_functiont &get_goto_function, statet &state, const code_function_callt &call) { const irep_idt &identifier= to_symbol_expr(call.function()).get_identifier(); - // find code in function map - - goto_functionst::function_mapt::const_iterator it= - goto_functions.function_map.find(identifier); - - if(it==goto_functions.function_map.end()) - throw "failed to find `"+id2string(identifier)+"' in function_map"; - - const goto_functionst::goto_functiont &goto_function=it->second; + const goto_functionst::goto_functiont &goto_function = + get_goto_function(identifier); if(state.dirty) state.dirty->populate_dirty_for_function(identifier, goto_function); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 191d4ec4e74..1f0baf6dbe2 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -126,7 +126,7 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state) void goto_symext::initialize_entry_point( statet &state, - const goto_functionst &goto_functions, + const get_goto_functiont &get_goto_function, const goto_programt::const_targett pc, const goto_programt::const_targett limit) { @@ -137,23 +137,19 @@ void goto_symext::initialize_entry_point( state.top().calling_location.pc=state.top().end_of_function; state.symex_target=⌖ state.dirty=util_make_unique(); - if(!pc->function.empty()) - { - state.dirty->populate_dirty_for_function( - pc->function, goto_functions.function_map.at(pc->function)); - } - else - { - log.warning() << "Unable to analyse address-taken locals, as start " - "instruction does not state its function" << messaget::eom; - } + + INVARIANT( + !pc->function.empty(), "all symexed instructions should have a function"); + state.dirty->populate_dirty_for_function( + pc->function, get_goto_function(pc->function)); + symex_transition(state, state.source.pc); } void goto_symext::symex_threaded_step( - statet &state, const goto_functionst &goto_functions) + statet &state, const get_goto_functiont &get_goto_function) { - symex_step(goto_functions, state); + symex_step(get_goto_function, state); // is there another thread to execute? if(state.call_stack().empty() && @@ -168,21 +164,39 @@ void goto_symext::symex_threaded_step( } } +static goto_symext::get_goto_functiont get_function_from_goto_functions( + const goto_functionst &goto_functions) +{ + return [&goto_functions](const irep_idt &key) -> + const goto_functionst::goto_functiont & { // NOLINT(*) + return goto_functions.function_map.at(key); + }; +} + void goto_symext::symex_with_state( statet &state, const goto_functionst &goto_functions, const goto_programt &goto_program) +{ + symex_with_state( + state, get_function_from_goto_functions(goto_functions), goto_program); +} + +void goto_symext::symex_with_state( + statet &state, + const get_goto_functiont &get_goto_function, + const goto_programt &goto_program) { PRECONDITION(!goto_program.instructions.empty()); initialize_entry_point( state, - goto_functions, + get_goto_function, goto_program.instructions.begin(), prev(goto_program.instructions.end())); PRECONDITION(state.top().end_of_function->is_end_function()); while(!state.call_stack().empty()) - symex_threaded_step(state, goto_functions); + symex_threaded_step(state, get_goto_function); state.dirty=nullptr; } @@ -193,30 +207,48 @@ void goto_symext::symex_instruction_range( const goto_programt::const_targett first, const goto_programt::const_targett limit) { - initialize_entry_point(state, goto_functions, first, limit); + symex_instruction_range( + state, get_function_from_goto_functions(goto_functions), first, limit); +} + +void goto_symext::symex_instruction_range( + statet &state, + const get_goto_functiont &get_goto_function, + const goto_programt::const_targett first, + const goto_programt::const_targett limit) +{ + initialize_entry_point(state, get_goto_function, first, limit); while(state.source.pc->function!=limit->function || state.source.pc!=limit) - symex_threaded_step(state, goto_functions); + symex_threaded_step(state, get_goto_function); } -/// symex from entry point void goto_symext::symex_from_entry_point_of( - const goto_functionst &goto_functions) + const goto_functionst &goto_functions) { - goto_functionst::function_mapt::const_iterator it= - goto_functions.function_map.find(goto_functionst::entry_point()); + symex_from_entry_point_of(get_function_from_goto_functions(goto_functions)); +} - if(it==goto_functions.function_map.end()) +/// symex from entry point +void goto_symext::symex_from_entry_point_of( + const get_goto_functiont &get_goto_function) +{ + const goto_functionst::goto_functiont *start_function; + try + { + start_function = &get_goto_function(goto_functionst::entry_point()); + } + catch(const std::out_of_range &error) + { throw "the program has no entry point"; - - const goto_programt &body=it->second.body; + } statet state; - symex_with_state(state, goto_functions, body); + symex_with_state(state, get_goto_function, start_function->body); } /// do just one step void goto_symext::symex_step( - const goto_functionst &goto_functions, + const get_goto_functiont &get_goto_function, statet &state) { #if 0 @@ -321,7 +353,7 @@ void goto_symext::symex_step( Forall_expr(it, deref_code.arguments()) clean_expr(*it, state, false); - symex_function_call(goto_functions, state, deref_code); + symex_function_call(get_goto_function, state, deref_code); } else symex_transition(state); @@ -329,7 +361,7 @@ void goto_symext::symex_step( case OTHER: if(!state.guard.is_false()) - symex_other(goto_functions, state); + symex_other(state); symex_transition(state); break; diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp index 00e3cac907d..03b0ab5f211 100644 --- a/src/goto-symex/symex_other.cpp +++ b/src/goto-symex/symex_other.cpp @@ -79,7 +79,6 @@ void goto_symext::havoc_rec( } void goto_symext::symex_other( - const goto_functionst &goto_functions, statet &state) { const goto_programt::instructiont &instruction=*state.source.pc;