CBMC
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 <util/cprover_prefix.h>
17 #include <util/find_symbols.h>
18 #include <util/std_expr.h>
19 
20 #include <analyses/call_graph.h>
22 
23 #include "goto_functions.h"
24 #include "goto_model.h"
25 
27  goto_modelt &goto_model,
28  message_handlert &message_handler)
29 {
30  // gather all functions reachable from the entry point
31  const irep_idt entry_point=goto_functionst::entry_point();
32  goto_functionst &goto_functions=goto_model.goto_functions;
33 
34  if(goto_functions.function_map.count(entry_point) == 0)
35  throw user_input_error_exceptiont("entry point not found");
36 
37  // Get the call graph restricted to functions reachable from
38  // the entry point:
39  call_grapht call_graph =
40  call_grapht::create_from_root_function(goto_model, entry_point, false);
41  const auto directed_graph = call_graph.get_directed_graph();
42  INVARIANT(
43  !directed_graph.empty(),
44  "at least " + id2string(entry_point) + " should be reachable");
45 
46  // gather all symbols used by reachable functions
47 
48  find_symbols_sett symbols_to_keep;
49 
50  for(std::size_t node_idx = 0; node_idx < directed_graph.size(); ++node_idx)
51  {
52  const irep_idt &id = directed_graph[node_idx].function;
53  if(id == INITIALIZE_FUNCTION)
54  continue;
55 
56  // assume function has no body if it is not in the function map
57  const auto &it = goto_functions.function_map.find(id);
58  if(it == goto_functions.function_map.end())
59  continue;
60 
61  for(const auto &i : it->second.body.instructions)
62  {
63  i.apply([&symbols_to_keep](const exprt &expr) {
64  find_symbols(expr, symbols_to_keep);
65  });
66  }
67  }
68 
69  goto_functionst::function_mapt::iterator f_it;
70  f_it=goto_functions.function_map.find(INITIALIZE_FUNCTION);
71 
72  if(f_it == goto_functions.function_map.end())
73  throw incorrect_goto_program_exceptiont("initialize function not found");
74 
75  goto_programt &goto_program=f_it->second.body;
76 
77  // add all symbols from right-hand sides of required symbols
78  bool fixed_point_reached = false;
79  // markers for each instruction to avoid repeatedly searching the same
80  // instruction for new symbols; initialized to false, and set to true whenever
81  // an instruction is determined to be irrelevant (not an assignment) or
82  // symbols have been collected from it
83  std::vector<bool> seen(goto_program.instructions.size(), false);
84  while(!fixed_point_reached)
85  {
86  fixed_point_reached = true;
87 
88  std::vector<bool>::iterator seen_it = seen.begin();
89  for(const auto &instruction : goto_program.instructions)
90  {
91  if(!*seen_it && instruction.is_assign())
92  {
93  const irep_idt id =
94  to_symbol_expr(instruction.assign_lhs()).get_identifier();
95 
96  // if we are to keep the left-hand side, then we also need to keep all
97  // symbols occurring in the right-hand side
98  if(
99  id.starts_with(CPROVER_PREFIX) ||
100  symbols_to_keep.find(id) != symbols_to_keep.end())
101  {
102  fixed_point_reached = false;
103  find_symbols(instruction.assign_rhs(), symbols_to_keep);
104  *seen_it = true;
105  }
106  }
107  else if(!*seen_it)
108  *seen_it = true;
109 
110  ++seen_it;
111  }
112  }
113 
114  // now remove unnecessary initializations
115  bool changed = false;
116  for(auto it = goto_model.symbol_table.begin();
117  it != goto_model.symbol_table.end();
118  ++it)
119  {
120  if(
121  it->second.is_static_lifetime && !it->second.is_type &&
122  !it->second.is_macro && it->second.type.id() != ID_code &&
123  !it->first.starts_with(CPROVER_PREFIX) &&
124  symbols_to_keep.find(it->first) == symbols_to_keep.end())
125  {
126  symbolt &symbol = it.get_writeable_symbol();
127  symbol.is_extern = true;
128  symbol.value.make_nil();
129  symbol.value.set(ID_C_no_nondet_initialization, 1);
130  changed = true;
131  }
132  }
133 
134  if(changed && goto_model.can_produce_function(INITIALIZE_FUNCTION))
135  recreate_initialize_function(goto_model, message_handler);
136 }
Function Call Graphs.
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Definition: call_graph.h:44
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:209
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:53
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
A collection of goto functions.
function_mapt function_map
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool can_produce_function(const irep_idt &id) const override
Determines if this model can produce a body for the given function.
Definition: goto_model.h:95
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:408
void make_nil()
Definition: irep.h:442
const irep_idt & get_identifier() const
Definition: std_expr.h:160
virtual iteratort begin() override
Definition: symbol_table.h:108
virtual iteratort end() override
Definition: symbol_table.h:112
Symbol table entry.
Definition: symbol.h:28
bool is_extern
Definition: symbol.h:74
exprt value
Initial value of symbol.
Definition: symbol.h:34
#define CPROVER_PREFIX
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings)
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
Goto Programs with Functions.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
void slice_global_inits(goto_modelt &goto_model, message_handlert &message_handler)
Remove initialization of global variables that are not used in any function reachable from the entry ...
Remove initializations of unused global variables.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
void recreate_initialize_function(goto_modelt &goto_model, message_handlert &message_handler)
Regenerates the CPROVER_INITIALIZE function, which initializes all non-function symbols of the goto m...
#define INITIALIZE_FUNCTION
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272