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 <unordered_set>
17 
18 #include <analyses/call_graph.h>
19 
20 #include <util/namespace.h>
21 #include <util/std_expr.h>
22 #include <util/cprover_prefix.h>
23 #include <util/prefix.h>
24 
27 
29  const namespacet &ns,
31 {
32  // gather all functions reachable from the entry point
33 
34  call_grapht call_graph(goto_functions);
35  const call_grapht::grapht &graph=call_graph.graph;
36 
37  std::list<irep_idt> worklist;
38  std::unordered_set<irep_idt, irep_id_hash> functions_reached;
39 
40  const irep_idt entry_point=goto_functionst::entry_point();
41 
42  goto_functionst::function_mapt::const_iterator e_it;
43  e_it=goto_functions.function_map.find(entry_point);
44 
45  if(e_it==goto_functions.function_map.end())
46  throw "entry point not found";
47 
48  worklist.push_back(entry_point);
49 
50  do
51  {
52  const irep_idt id=worklist.front();
53  worklist.pop_front();
54 
55  functions_reached.insert(id);
56 
57  const auto &p=graph.equal_range(id);
58 
59  for(auto it=p.first; it!=p.second; it++)
60  {
61  const irep_idt callee=it->second;
62 
63  if(functions_reached.find(callee)==functions_reached.end())
64  worklist.push_back(callee);
65  }
66  }
67  while(!worklist.empty());
68 
69  const irep_idt initialize=CPROVER_PREFIX "initialize";
70  functions_reached.erase(initialize);
71 
72  // gather all symbols used by reachable functions
73 
74  class symbol_collectort:public const_expr_visitort
75  {
76  public:
77  virtual void operator()(const exprt &expr)
78  {
79  if(expr.id()==ID_symbol)
80  {
81  const symbol_exprt &symbol_expr=to_symbol_expr(expr);
82  const irep_idt id=symbol_expr.get_identifier();
83  symbols.insert(id);
84  }
85  }
86 
87  std::unordered_set<irep_idt, irep_id_hash> symbols;
88  };
89 
90  symbol_collectort visitor;
91 
92  assert(!functions_reached.empty());
93 
94  for(const irep_idt &id : functions_reached)
95  {
96  const goto_functionst::goto_functiont &goto_function
97  =goto_functions.function_map.at(id);
98  const goto_programt &goto_program=goto_function.body;
99 
100  forall_goto_program_instructions(i_it, goto_program)
101  {
102  const codet &code=i_it->code;
103  code.visit(visitor);
104  }
105  }
106 
107  const std::unordered_set<irep_idt, irep_id_hash> &symbols=visitor.symbols;
108 
109  // now remove unnecessary initializations
110 
111  goto_functionst::function_mapt::iterator f_it;
112  f_it=goto_functions.function_map.find(initialize);
113  assert(f_it!=goto_functions.function_map.end());
114 
115  goto_programt &goto_program=f_it->second.body;
116 
117  Forall_goto_program_instructions(i_it, goto_program)
118  {
119  if(i_it->is_assign())
120  {
121  const code_assignt &code_assign=to_code_assign(i_it->code);
122  const symbol_exprt &symbol_expr=to_symbol_expr(code_assign.lhs());
123  const irep_idt id=symbol_expr.get_identifier();
124 
125  if(!has_prefix(id2string(id), CPROVER_PREFIX) &&
126  symbols.find(id)==symbols.end())
127  i_it->make_skip();
128  }
129  }
130 
131  remove_skip(goto_functions);
132  goto_functions.update();
133 }
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:120
Goto Programs with Functions.
Function Call Graphs.
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
void visit(class expr_visitort &visitor)
Definition: expr.cpp:483
exprt & lhs()
Definition: std_code.h:157
std::multimap< irep_idt, irep_idt > grapht
Definition: call_graph.h:30
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
goto_function_templatet< goto_programt > goto_functiont
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
virtual void operator()(const exprt &expr)
Definition: expr.h:179
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
A statement in a programming language.
Definition: std_code.h:19
Program Transformation.
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
void slice_global_inits(const namespacet &ns, goto_functionst &goto_functions)
goto_functionst goto_functions
Definition: goto_model.h:26
Assignment.
Definition: std_code.h:144
grapht graph
Definition: call_graph.h:31