From 552b10080b63e7c77407da7ecb9238c8e23bb84d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 14 Feb 2018 11:47:51 +0000 Subject: [PATCH 1/2] Set function member of each goto instruction in goto program passes --- src/goto-programs/goto_convert_functions.cpp | 5 ++--- src/goto-programs/goto_functions_template.h | 19 +++++++++++++++++++ src/goto-programs/goto_model.h | 7 +++++++ src/goto-programs/goto_program_template.h | 16 ++++++++++++++++ src/jbmc/jbmc_parse_options.cpp | 3 +++ 5 files changed, 47 insertions(+), 3 deletions(-) diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index 88563287512..1f9f49867f1 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -213,9 +213,8 @@ void goto_convert_functionst::convert_function( // add "end of function" f.body.destructive_append(tmp_end_function); - // do function tags - Forall_goto_program_instructions(i_it, f.body) - i_it->function=identifier; + // do function tags (they are empty at this point) + f.update_instructions_function(identifier); f.body.update(); diff --git a/src/goto-programs/goto_functions_template.h b/src/goto-programs/goto_functions_template.h index 382b0ec023a..08dc0494252 100644 --- a/src/goto-programs/goto_functions_template.h +++ b/src/goto-programs/goto_functions_template.h @@ -62,6 +62,14 @@ class goto_function_templatet parameter_identifiers.clear(); } + /// update the function member in each instruction + /// \param function_id: the `function_id` used for assigning empty function + /// members + void update_instructions_function(const irep_idt &function_id) + { + body.update_instructions_function(function_id); + } + void swap(goto_function_templatet &other) { body.swap(other.body); @@ -149,12 +157,23 @@ class goto_functions_templatet void compute_target_numbers(); void compute_incoming_edges(); + /// update the function member in each instruction by setting it to + /// the goto function's identifier + void update_instructions_function() + { + for(auto &func : function_map) + { + func.second.update_instructions_function(func.first); + } + } + void update() { compute_incoming_edges(); compute_target_numbers(); compute_location_numbers(); compute_loop_numbers(); + update_instructions_function(); } static inline irep_idt entry_point() diff --git a/src/goto-programs/goto_model.h b/src/goto-programs/goto_model.h index 04236c201c9..c4ce8124978 100644 --- a/src/goto-programs/goto_model.h +++ b/src/goto-programs/goto_model.h @@ -103,6 +103,13 @@ class goto_model_functiont goto_functions.compute_location_numbers(goto_function.body); } + /// Updates the empty function member of each instruction by setting them + /// to `function_id` + void update_instructions_function() + { + goto_function.update_instructions_function(function_id); + } + /// Get symbol table /// \return journalling symbol table that (a) wraps the global symbol table, /// and (b) has recorded all symbol mutations (insertions, updates and diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index a7110c0cba3..50c489236d0 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -521,6 +521,22 @@ class goto_program_templatet } } + /// Sets the `function` member of each instruction if not yet set + /// Note that a goto program need not be a goto function and therefore, + /// we cannot do this in update(), but only at the level of + /// of goto_functionst where goto programs are guaranteed to be + /// named functions. + void update_instructions_function(const irep_idt &function_id) + { + for(auto &instruction : instructions) + { + if(instruction.function.empty()) + { + instruction.function = function_id; + } + } + } + /// Compute location numbers void compute_location_numbers() { diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 29eeb903919..31b0f7ef968 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -708,6 +708,9 @@ void jbmc_parse_optionst::process_goto_function( symbol_table.lookup_ref(new_symbol_name), symbol_table); } + + // update the function member in each instruction + function.update_instructions_function(); } catch(const char *e) From 5df3fca9cfe7b9732f0d87d1a0eaf740194bab87 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Wed, 14 Feb 2018 11:50:37 +0000 Subject: [PATCH 2/2] Clean up get_function_id hacks --- src/analyses/dependence_graph.cpp | 2 +- src/goto-instrument/full_slicer.cpp | 4 ++-- src/goto-programs/goto_program_template.h | 13 ++----------- src/goto-programs/remove_returns.cpp | 3 +-- 4 files changed, 6 insertions(+), 16 deletions(-) diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 6d691528ca8..1a4954fccc6 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -76,7 +76,7 @@ void dep_graph_domaint::control_dependencies( from->is_assume()) control_deps.insert(from); - const irep_idt id=goto_programt::get_function_id(from); + const irep_idt id=from->function; const cfg_post_dominatorst &pd=dep_graph.cfg_post_dominators().at(id); // check all candidates for M diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index f77bcec3298..43e60c030e3 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -150,7 +150,7 @@ void full_slicert::add_jumps( continue; } - const irep_idt id=goto_programt::get_function_id(j.PC); + const irep_idt id=j.PC->function; const cfg_post_dominatorst &pd=post_dominators.at(id); cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e= @@ -184,7 +184,7 @@ void full_slicert::add_jumps( if(cfg[entry->second].node_required) { - const irep_idt id2=goto_programt::get_function_id(*d_it); + const irep_idt id2=(*d_it)->function; INVARIANT(id==id2, "goto/jump expected to be within a single function"); diff --git a/src/goto-programs/goto_program_template.h b/src/goto-programs/goto_program_template.h index 50c489236d0..2727e628054 100644 --- a/src/goto-programs/goto_program_template.h +++ b/src/goto-programs/goto_program_template.h @@ -386,21 +386,12 @@ class goto_program_templatet return t; } - static const irep_idt get_function_id( - const_targett l) - { - while(!l->is_end_function()) - ++l; - - return l->function; - } - static const irep_idt get_function_id( const goto_program_templatet &p) { - assert(!p.empty()); + PRECONDITION(!p.empty()); - return get_function_id(--p.instructions.end()); + return p.instructions.back().function; } template diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 3894dae6ba3..4c275ff9bbb 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -244,8 +244,7 @@ void remove_returnst::operator()( if(goto_function.body.empty()) return; - replace_returns( - goto_programt::get_function_id(goto_function.body), goto_function); + replace_returns(model_function.get_function_id(), goto_function); do_function_calls(function_is_stub, goto_function.body); }