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 
26 
28 
30 {
31  // gather all functions reachable from the entry point
32  const irep_idt entry_point=goto_functionst::entry_point();
34 
35  if(!goto_functions.function_map.count(entry_point))
36  throw "entry point not found";
37 
38  // Get the call graph restricted to functions reachable from
39  // the entry point:
40  call_grapht call_graph =
41  call_grapht::create_from_root_function(goto_model, entry_point, false);
42  const auto directed_graph = call_graph.get_directed_graph();
43  INVARIANT(
44  !directed_graph.empty(), "At least __CPROVER_start should be reachable");
45 
46  // gather all symbols used by reachable functions
47 
48  find_symbols_sett symbols;
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  const goto_programt &goto_program = it->second.body;
62 
64  {
65  const codet &code = i_it->code;
66  find_symbols(code, symbols, true, false);
67  const exprt &expr = i_it->guard;
68  find_symbols(expr, symbols, true, false);
69  }
70  }
71 
72  // now remove unnecessary initializations
73 
74  goto_functionst::function_mapt::iterator f_it;
76  assert(f_it!=goto_functions.function_map.end());
77 
78  goto_programt &goto_program=f_it->second.body;
79 
81  {
82  if(i_it->is_assign())
83  {
84  const code_assignt &code_assign=to_code_assign(i_it->code);
85  const symbol_exprt &symbol_expr=to_symbol_expr(code_assign.lhs());
86  const irep_idt id=symbol_expr.get_identifier();
87 
89  symbols.find(id)==symbols.end())
90  i_it->make_skip();
91  }
92  }
93 
95 }
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:128
Goto Programs with Functions.
Function Call Graphs.
function_mapt function_map
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
exprt & lhs()
Definition: std_code.h:209
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
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
static call_grapht create_from_root_function(const goto_modelt &model, const irep_idt &root, bool collect_callsites)
Definition: call_graph.h:31
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
static irep_idt entry_point()
Base class for all expressions.
Definition: expr.h:42
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
A statement in a programming language.
Definition: std_code.h:21
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:735
void find_symbols(const exprt &src, find_symbols_sett &dest)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Assignment.
Definition: std_code.h:196