cprover
slice_global_inits.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove initializations of unused global variables
4 
5 Author: Daniel Poetzl
6 
7 Date: December 2016
8 
9 \*******************************************************************/
10 
13 
14 #include "slice_global_inits.h"
15 
16 #include <analyses/call_graph.h>
17 
18 #include <util/find_symbols.h>
19 #include <util/namespace.h>
20 #include <util/std_expr.h>
21 #include <util/cprover_prefix.h>
22 #include <util/prefix.h>
23 
24 #include <util/invariant.h>
25 
28 
30 
32 {
33  // gather all functions reachable from the entry point
34  const irep_idt entry_point=goto_functionst::entry_point();
36 
37  if(goto_functions.function_map.count(entry_point) == 0)
38  throw user_input_error_exceptiont("entry point not found");
39 
40  // Get the call graph restricted to functions reachable from
41  // the entry point:
42  call_grapht call_graph =
43  call_grapht::create_from_root_function(goto_model, entry_point, false);
44  const auto directed_graph = call_graph.get_directed_graph();
45  INVARIANT(
46  !directed_graph.empty(),
47  "at least " + id2string(entry_point) + " should be reachable");
48 
49  // gather all symbols used by reachable functions
50 
51  find_symbols_sett symbols;
52 
53  for(std::size_t node_idx = 0; node_idx < directed_graph.size(); ++node_idx)
54  {
55  const irep_idt &id = directed_graph[node_idx].function;
56  if(id == INITIALIZE_FUNCTION)
57  continue;
58 
59  // assume function has no body if it is not in the function map
60  const auto &it = goto_functions.function_map.find(id);
61  if(it == goto_functions.function_map.end())
62  continue;
63 
64  const goto_programt &goto_program = it->second.body;
65 
66  forall_goto_program_instructions(i_it, goto_program)
67  {
68  const codet &code = i_it->code;
69  find_symbols(code, symbols, true, false);
70  const exprt &expr = i_it->guard;
71  find_symbols(expr, symbols, true, false);
72  }
73  }
74 
75  // now remove unnecessary initializations
76 
77  goto_functionst::function_mapt::iterator f_it;
79  if(f_it == goto_functions.function_map.end())
80  throw incorrect_goto_program_exceptiont("initialize function not found");
81 
82  goto_programt &goto_program=f_it->second.body;
83 
84  Forall_goto_program_instructions(i_it, goto_program)
85  {
86  if(i_it->is_assign())
87  {
88  const code_assignt &code_assign=to_code_assign(i_it->code);
89  const symbol_exprt &symbol_expr=to_symbol_expr(code_assign.lhs());
90  const irep_idt id=symbol_expr.get_identifier();
91 
93  symbols.find(id)==symbols.end())
94  i_it->make_skip();
95  }
96  }
97 
99 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
Remove initializations of unused global variables.
#define CPROVER_PREFIX
const irep_idt & get_identifier() const
Definition: std_expr.h:176
Goto Programs with Functions.
Function Call Graphs.
function_mapt function_map
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
exprt & lhs()
Definition: std_code.h:269
directed_grapht get_directed_graph() const
Returns a grapht representation of this call graph, suitable for use with generic grapht algorithms.
Definition: call_graph.cpp:208
#define INITIALIZE_FUNCTION
API to expression classes.
void slice_global_inits(goto_modelt &goto_model)
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:48
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Definition: call_graph.h:38
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Base class for all expressions.
Definition: expr.h:54
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Expression to hold a symbol (variable)
Definition: std_expr.h:143
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
Program Transformation.
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
void find_symbols(const exprt &src, find_symbols_sett &dest)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
A codet representing an assignment in the program.
Definition: std_code.h:256