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_to_keep;
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  for(const auto &i : it->second.body.instructions)
65  {
66  i.apply([&symbols_to_keep](const exprt &expr) {
67  find_symbols(expr, symbols_to_keep, true, false);
68  });
69  }
70  }
71 
72  goto_functionst::function_mapt::iterator f_it;
74 
75  if(f_it == goto_functions.function_map.end())
76  throw incorrect_goto_program_exceptiont("initialize function not found");
77 
78  goto_programt &goto_program=f_it->second.body;
79 
80  // add all symbols from right-hand sides of required symbols
81  bool fixed_point_reached = false;
82  // markers for each instruction to avoid repeatedly searching the same
83  // instruction for new symbols; initialized to false, and set to true whenever
84  // an instruction is determined to be irrelevant (not an assignment) or
85  // symbols have been collected from it
86  std::vector<bool> seen(goto_program.instructions.size(), false);
87  while(!fixed_point_reached)
88  {
89  fixed_point_reached = true;
90 
91  std::vector<bool>::iterator seen_it = seen.begin();
92  forall_goto_program_instructions(i_it, goto_program)
93  {
94  if(!*seen_it && i_it->is_assign())
95  {
96  const code_assignt &code_assign = i_it->get_assign();
97  const irep_idt id = to_symbol_expr(code_assign.lhs()).get_identifier();
98 
99  // if we are to keep the left-hand side, then we also need to keep all
100  // symbols occurring in the right-hand side
101  if(
103  symbols_to_keep.find(id) != symbols_to_keep.end())
104  {
105  fixed_point_reached = false;
106  find_symbols(code_assign.rhs(), symbols_to_keep, true, false);
107  *seen_it = true;
108  }
109  }
110  else if(!*seen_it)
111  *seen_it = true;
112 
113  ++seen_it;
114  }
115  }
116 
117  // now remove unnecessary initializations
118  Forall_goto_program_instructions(i_it, goto_program)
119  {
120  if(i_it->is_assign())
121  {
122  const code_assignt &code_assign = i_it->get_assign();
123  const symbol_exprt &symbol_expr=to_symbol_expr(code_assign.lhs());
124  const irep_idt id=symbol_expr.get_identifier();
125 
126  if(
128  symbols_to_keep.find(id) == symbols_to_keep.end())
129  {
130  i_it->turn_into_skip();
131  }
132  }
133  }
134 
136 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
prefix.h
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
call_graph.h
Function Call Graphs.
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespace.h
call_grapht::create_from_root_function
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:48
incorrect_goto_program_exceptiont
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Definition: exception_utils.h:90
find_symbols.h
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:23
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
slice_global_inits
void slice_global_inits(goto_modelt &goto_model)
Definition: slice_global_inits.cpp:31
call_grapht::get_directed_graph
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
find_symbols
void find_symbols(const exprt &src, find_symbols_sett &dest, bool current, bool next)
Add to the set dest the sub-expressions of src with id ID_symbol if current is true,...
Definition: find_symbols.cpp:23
cprover_prefix.h
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
call_grapht
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Definition: call_graph.h:39
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:22
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functions.h
Goto Programs with Functions.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
slice_global_inits.h
Remove initializations of unused global variables.
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:90
static_lifetime_init.h
user_input_error_exceptiont
Definition: slice_global_inits.h:22
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
std_expr.h
API to expression classes.
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
validation_modet::INVARIANT
@ INVARIANT