cprover
slice_global_inits.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove initializations of unused global variables
4
5Author: Daniel Poetzl
6
7Date: 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/std_expr.h>
20#include <util/cprover_prefix.h>
21#include <util/prefix.h>
22
24
26#include "goto_functions.h"
27#include "goto_model.h"
28
30 goto_modelt &goto_model,
31 message_handlert &message_handler)
32{
33 // gather all functions reachable from the entry point
34 const irep_idt entry_point=goto_functionst::entry_point();
35 goto_functionst &goto_functions=goto_model.goto_functions;
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();
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;
73 f_it=goto_functions.function_map.find(INITIALIZE_FUNCTION);
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 for(const auto &instruction : goto_program.instructions)
93 {
94 if(!*seen_it && instruction.is_assign())
95 {
96 const irep_idt id =
97 to_symbol_expr(instruction.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(instruction.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 bool changed = false;
119 for(auto &entry : goto_model.symbol_table)
120 {
121 if(
122 entry.second.is_static_lifetime && !entry.second.is_type &&
123 !entry.second.is_macro && entry.second.type.id() != ID_code &&
124 !has_prefix(id2string(entry.first), CPROVER_PREFIX) &&
125 symbols_to_keep.find(entry.first) == symbols_to_keep.end())
126 {
127 symbolt &symbol = goto_model.symbol_table.get_writeable_ref(entry.first);
128 symbol.is_extern = true;
129 symbol.value.make_nil();
130 symbol.value.set(ID_C_no_nondet_initialization, 1);
131 changed = true;
132 }
133 }
134
135 if(
136 changed &&
137 goto_model.goto_functions.function_map.erase(INITIALIZE_FUNCTION) != 0)
138 {
140 goto_model.symbol_table,
144 goto_model.symbol_table,
145 goto_model.goto_functions,
146 message_handler);
147 goto_model.goto_functions.update();
148 }
149}
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:37
Base class for all expressions.
Definition: expr.h:54
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.
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
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:598
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:420
void make_nil()
Definition: irep.h:454
const irep_idt & get_identifier() const
Definition: std_expr.h:109
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Symbol table entry.
Definition: symbol.h:28
bool is_extern
Definition: symbol.h:66
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
exprt value
Initial value of symbol.
Definition: symbol.h:34
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
#define CPROVER_PREFIX
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,...
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:23
void goto_convert(const codet &code, symbol_table_baset &symbol_table, goto_programt &dest, message_handlert &message_handler, const irep_idt &mode)
Goto Programs with Functions.
Goto Programs with Functions.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
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
static optionalt< codet > static_lifetime_init(const irep_idt &identifier, symbol_tablet &symbol_table)
#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:189