From d939de960662c2c8547dbba51970910aacbcb866 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Jan 2019 18:41:14 +0000 Subject: [PATCH] rw_set: store function identifier alongside instruction reference We are working towards removing the "function" field from goto_programt::instructionst::instructiont, and thus need to pass the identifier of the function whenever it actually is required. rw_set does not yet make use of this, but will need to once dereferencing is updated to require a function name. --- src/goto-instrument/interrupt.cpp | 31 +++++++----- src/goto-instrument/mmio.cpp | 17 +++++-- src/goto-instrument/race_check.cpp | 29 ++++++----- src/goto-instrument/race_check.h | 4 +- src/goto-instrument/rw_set.cpp | 15 ++++-- src/goto-instrument/rw_set.h | 47 ++++++++++-------- src/goto-instrument/wmm/goto2graph.cpp | 56 +++++++++++++++------- src/goto-instrument/wmm/goto2graph.h | 13 +++-- src/goto-instrument/wmm/shared_buffers.cpp | 20 ++++++-- src/goto-instrument/wmm/weak_memory.cpp | 15 ++++-- 10 files changed, 163 insertions(+), 84 deletions(-) diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp index f9882332fd5..a6b0bc48f5f 100644 --- a/src/goto-instrument/interrupt.cpp +++ b/src/goto-instrument/interrupt.cpp @@ -19,7 +19,7 @@ Date: September 2011 #include #endif -bool potential_race_on_read( +static bool potential_race_on_read( const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set) { @@ -33,7 +33,7 @@ bool potential_race_on_read( return false; } -bool potential_race_on_write( +static bool potential_race_on_write( const rw_set_baset &code_rw_set, const rw_set_baset &isr_rw_set) { @@ -50,9 +50,10 @@ bool potential_race_on_write( return false; } -void interrupt( +static void interrupt( value_setst &value_sets, const symbol_tablet &symbol_table, + const irep_idt &function_id, #ifdef LOCAL_MAY const goto_functionst::goto_functiont &goto_function, #endif @@ -69,11 +70,16 @@ void interrupt( #ifdef LOCAL_MAY local_may_aliast local_may(goto_function); #endif - rw_set_loct rw_set(ns, value_sets, i_it + rw_set_loct rw_set( + ns, + value_sets, + function_id, + i_it #ifdef LOCAL_MAY - , local_may + , + local_may #endif - ); // NOLINT(whitespace/parens) + ); // NOLINT(whitespace/parens) // potential race? bool race_on_read=potential_race_on_read(rw_set, isr_rw_set); @@ -143,9 +149,8 @@ void interrupt( } } -symbol_exprt get_isr( - const symbol_tablet &symbol_table, - const irep_idt &interrupt_handler) +static symbol_exprt +get_isr(const symbol_tablet &symbol_table, const irep_idt &interrupt_handler) { std::list matches; @@ -197,11 +202,15 @@ void interrupt( f_it->first!=goto_functionst::entry_point() && f_it->first!=isr.get_identifier()) interrupt( - value_sets, goto_model.symbol_table, + value_sets, + goto_model.symbol_table, + f_it->first, #ifdef LOCAL_MAY f_it->second, #endif - f_it->second.body, isr, isr_rw_set); + f_it->second.body, + isr, + isr_rw_set); goto_model.goto_functions.update(); } diff --git a/src/goto-instrument/mmio.cpp b/src/goto-instrument/mmio.cpp index 0e0a2a03693..a7d06fb86a1 100644 --- a/src/goto-instrument/mmio.cpp +++ b/src/goto-instrument/mmio.cpp @@ -21,9 +21,10 @@ Date: September 2011 #include #endif -void mmio( +static void mmio( value_setst &value_sets, const symbol_tablet &symbol_table, + const irep_idt &function_id, #ifdef LOCAL_MAY const goto_functionst::goto_functiont &goto_function, #endif @@ -41,9 +42,14 @@ void mmio( if(instruction.is_assign()) { - rw_set_loct rw_set(ns, value_sets, i_it + rw_set_loct rw_set( + ns, + value_sets, + function_id, + i_it #ifdef LOCAL_MAY - , local_may + , + local_may #endif ); // NOLINT(whitespace/parens) @@ -159,7 +165,10 @@ void mmio( Forall_goto_functions(f_it, goto_model.goto_functions) if(f_it->first != INITIALIZE_FUNCTION && f_it->first!=goto_functionst::entry_point()) - mmio(value_sets, goto_model.symbol_table, + mmio( + value_sets, + goto_model.symbol_table, + f_it->first, #ifdef LOCAL_MAY f_it->second, #endif diff --git a/src/goto-instrument/race_check.cpp b/src/goto-instrument/race_check.cpp index 0289148f1ec..26bf6763be1 100644 --- a/src/goto-instrument/race_check.cpp +++ b/src/goto-instrument/race_check.cpp @@ -104,7 +104,7 @@ void w_guardst::add_initialization(goto_programt &goto_program) const } } -std::string comment(const rw_set_baset::entryt &entry, bool write) +static std::string comment(const rw_set_baset::entryt &entry, bool write) { std::string result; if(write) @@ -117,9 +117,7 @@ std::string comment(const rw_set_baset::entryt &entry, bool write) return result; } -bool is_shared( - const namespacet &ns, - const symbol_exprt &symbol_expr) +static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr) { const irep_idt &identifier=symbol_expr.get_identifier(); @@ -137,9 +135,7 @@ bool is_shared( return symbol.is_shared(); } -bool has_shared_entries( - const namespacet &ns, - const rw_set_baset &rw_set) +static bool has_shared_entries(const namespacet &ns, const rw_set_baset &rw_set) { for(rw_set_baset::entriest::const_iterator it=rw_set.r_entries.begin(); @@ -158,12 +154,17 @@ bool has_shared_entries( return false; } -void race_check( +// clang-format off +// clang-format is confused by the L_M_ARG macro and wants to indent the line +// after +static void race_check( value_setst &value_sets, symbol_tablet &symbol_table, + const irep_idt &function_id, L_M_ARG(const goto_functionst::goto_functiont &goto_function) goto_programt &goto_program, w_guardst &w_guards) +// clang-format on { namespacet ns(symbol_table); @@ -177,7 +178,8 @@ void race_check( if(instruction.is_assign()) { - rw_set_loct rw_set(ns, value_sets, i_it L_M_LAST_ARG(local_may)); + rw_set_loct rw_set( + ns, value_sets, function_id, i_it L_M_LAST_ARG(local_may)); if(!has_shared_entries(ns, rw_set)) continue; @@ -266,6 +268,7 @@ void race_check( void race_check( value_setst &value_sets, symbol_tablet &symbol_table, + const irep_idt &function_id, #ifdef LOCAL_MAY const goto_functionst::goto_functiont &goto_function, #endif @@ -276,8 +279,8 @@ void race_check( race_check( value_sets, symbol_table, - L_M_ARG(goto_function) - goto_program, + function_id, + L_M_ARG(goto_function) goto_program, w_guards); w_guards.add_initialization(goto_program); @@ -296,8 +299,8 @@ void race_check( race_check( value_sets, goto_model.symbol_table, - L_M_ARG(f_it->second) - f_it->second.body, + f_it->first, + L_M_ARG(f_it->second) f_it->second.body, w_guards); // get "main" diff --git a/src/goto-instrument/race_check.h b/src/goto-instrument/race_check.h index 829ca529ea6..e328b0522d9 100644 --- a/src/goto-instrument/race_check.h +++ b/src/goto-instrument/race_check.h @@ -20,11 +20,11 @@ Date: February 2006 void race_check( value_setst &, class symbol_tablet &, + const irep_idt &function_id, #ifdef LOCAL_MAY const goto_functionst::goto_functiont &goto_function, #endif - goto_programt &goto_program -); + goto_programt &goto_program); void race_check(value_setst &, goto_modelt &); diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp index d1f535efc4a..7f29f3030f1 100644 --- a/src/goto-instrument/rw_set.cpp +++ b/src/goto-instrument/rw_set.cpp @@ -199,10 +199,10 @@ void rw_set_functiont::compute_rec(const exprt &function) { if(function.id()==ID_symbol) { - const irep_idt &id=to_symbol_expr(function).get_identifier(); + const irep_idt &function_id = to_symbol_expr(function).get_identifier(); - goto_functionst::function_mapt::const_iterator f_it= - goto_functions.function_map.find(id); + goto_functionst::function_mapt::const_iterator f_it = + goto_functions.function_map.find(function_id); if(f_it!=goto_functions.function_map.end()) { @@ -220,9 +220,14 @@ void rw_set_functiont::compute_rec(const exprt &function) forall_goto_program_instructions(i_it, body) { - *this+=rw_set_loct(ns, value_sets, i_it + *this += rw_set_loct( + ns, + value_sets, + function_id, + i_it #ifdef LOCAL_MAY - , local_may + , + local_may #endif ); // NOLINT(whitespace/parens) } diff --git a/src/goto-instrument/rw_set.h b/src/goto-instrument/rw_set.h index b59e71232a4..2e050f8c5b6 100644 --- a/src/goto-instrument/rw_set.h +++ b/src/goto-instrument/rw_set.h @@ -121,26 +121,31 @@ class _rw_set_loct:public rw_set_baset _rw_set_loct( const namespacet &_ns, value_setst &_value_sets, + const irep_idt &_function_id, goto_programt::const_targett _target, - local_may_aliast &may): - rw_set_baset(_ns), - value_sets(_value_sets), - target(_target), - local_may(may) + local_may_aliast &may) + : rw_set_baset(_ns), + value_sets(_value_sets), + function_id(_function_id), + target(_target), + local_may(may) #else _rw_set_loct( const namespacet &_ns, value_setst &_value_sets, - goto_programt::const_targett _target): - rw_set_baset(_ns), - value_sets(_value_sets), - target(_target) + const irep_idt &_function_id, + goto_programt::const_targett _target) + : rw_set_baset(_ns), + value_sets(_value_sets), + function_id(_function_id), + target(_target) #endif { } protected: value_setst &value_sets; + const irep_idt function_id; const goto_programt::const_targett target; #ifdef LOCAL_MAY @@ -180,15 +185,17 @@ class rw_set_loct:public _rw_set_loct rw_set_loct( const namespacet &_ns, value_setst &_value_sets, + const irep_idt &_function_id, goto_programt::const_targett _target, - local_may_aliast &may): - _rw_set_loct(_ns, _value_sets, _target, may) + local_may_aliast &may) + : _rw_set_loct(_ns, _value_sets, _function_id, _target, may) #else rw_set_loct( const namespacet &_ns, value_setst &_value_sets, - goto_programt::const_targett _target): - _rw_set_loct(_ns, _value_sets, _target) + const irep_idt &_function_id, + goto_programt::const_targett _target) + : _rw_set_loct(_ns, _value_sets, _function_id, _target) #endif { compute(); @@ -239,17 +246,19 @@ class rw_set_with_trackt:public _rw_set_loct rw_set_with_trackt( const namespacet &_ns, value_setst &_value_sets, + const irep_idt &_function_id, goto_programt::const_targett _target, - local_may_aliast &may): - _rw_set_loct(_ns, _value_sets, _target, may), - dereferencing(false) + local_may_aliast &may) + : _rw_set_loct(_ns, _value_sets, _function_id, _target, may), + dereferencing(false) #else rw_set_with_trackt( const namespacet &_ns, value_setst &_value_sets, - goto_programt::const_targett _target): - _rw_set_loct(_ns, _value_sets, _target), - dereferencing(false) + const irep_idt &_function_id, + goto_programt::const_targett _target) + : _rw_set_loct(_ns, _value_sets, _function_id, _target), + dereferencing(false) #endif { compute(); diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 05cc7eac7f5..a4d64441bef 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -210,6 +210,7 @@ void instrumentert::cfg_visitort::visit_cfg_function( { visit_cfg_assign( value_sets, + function_id, i_it, no_dependencies #ifdef LOCAL_MAY @@ -245,6 +246,7 @@ void instrumentert::cfg_visitort::visit_cfg_function( else if(instruction.is_goto()) { visit_cfg_goto( + function_id, goto_program, i_it, replicate_body, @@ -403,13 +405,15 @@ event_idt alt_copy_segment(wmm_grapht &alt_egraph, } bool instrumentert::cfg_visitort::contains_shared_array( + const irep_idt &function_id, goto_programt::const_targett targ, goto_programt::const_targett i_it, value_setst &value_sets - #ifdef LOCAL_MAY - , local_may_aliast local_may - #endif -) const +#ifdef LOCAL_MAY + , + local_may_aliast local_may +#endif + ) const // NOLINT(whitespace/parens) { instrumenter.message.debug() << "contains_shared_array called for " << targ->source_location.get_line() << " and " @@ -418,10 +422,15 @@ bool instrumentert::cfg_visitort::contains_shared_array( { instrumenter.message.debug() << "Do we have an array at line " <source_location.get_line()<<"?" << messaget::eom; - rw_set_loct rw_set(ns, value_sets, cur - #ifdef LOCAL_MAY - , local_may - #endif + rw_set_loct rw_set( + ns, + value_sets, + function_id, + cur +#ifdef LOCAL_MAY + , + local_may +#endif ); // NOLINT(whitespace/parens) instrumenter.message.debug() << "Writes: "<second.body) { - rw_set_loct rw_set(ns, value_sets, i_it + rw_set_loct rw_set( + ns, + value_sets, + f_it->first, + i_it #ifdef LOCAL_MAY - , local_may + , + local_may #endif - ); // NOLINT(whitespace/parens) + ); // NOLINT(whitespace/parens) forall_rw_set_w_entries(w_it, rw_set) forall_rw_set_r_entries(r_it, rw_set) { @@ -1093,9 +1098,14 @@ void shared_bufferst::cfg_visitort::weak_memory( { try { - rw_set_loct rw_set(ns, value_sets, i_it + rw_set_loct rw_set( + ns, + value_sets, + function_id, + i_it #ifdef LOCAL_MAY - , local_may + , + local_may #endif ); // NOLINT(whitespace/parens) diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp index d9014c54d3d..243119cc916 100644 --- a/src/goto-instrument/wmm/weak_memory.cpp +++ b/src/goto-instrument/wmm/weak_memory.cpp @@ -36,7 +36,7 @@ Date: September 2011 void introduce_temporaries( value_setst &value_sets, symbol_tablet &symbol_table, - const irep_idt &function, + const irep_idt &function_id, goto_programt &goto_program, #ifdef LOCAL_MAY const goto_functionst::goto_functiont &goto_function, @@ -60,9 +60,14 @@ void introduce_temporaries( instruction.is_assert() || instruction.is_assume()) { - rw_set_loct rw_set(ns, value_sets, i_it + rw_set_loct rw_set( + ns, + value_sets, + function_id, + i_it #ifdef LOCAL_MAY - , local_may + , + local_may #endif ); // NOLINT(whitespace/parens) if(rw_set.empty()) @@ -70,8 +75,8 @@ void introduce_temporaries( symbolt new_symbol; new_symbol.base_name="$tmp_guard"; - new_symbol.name= - id2string(function)+"$tmp_guard"+std::to_string(tmp_counter++); + new_symbol.name = + id2string(function_id) + "$tmp_guard" + std::to_string(tmp_counter++); new_symbol.type=bool_typet(); new_symbol.is_static_lifetime=true; new_symbol.is_thread_local=true;