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 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:86
prefix.h
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:24
invariant.h
call_graph.h
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:143
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:89
find_symbols
void find_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:16
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:176
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
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:251
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
cprover_prefix.h
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
call_grapht
A call graph (https://en.wikipedia.org/wiki/Call_graph) for a GOTO model or GOTO functions collection...
Definition: call_graph.h:38
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
goto_functions.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
has_prefix
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
slice_global_inits.h
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:101
static_lifetime_init.h
user_input_error_exceptiont
Definition: slice_global_inits.h:21
remove_skip.h
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
std_expr.h
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
validation_modet::INVARIANT
@ INVARIANT
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34