CBMC
Loading...
Searching...
No Matches
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 <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();
43 !directed_graph.empty(),
44 "at least " + id2string(entry_point) + " should be reachable");
45
46 // gather all symbols used by reachable functions
47
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) {
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);
85 {
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();
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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.
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.
instructionst instructions
The list of instructions in the goto program.
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:412
void make_nil()
Definition irep.h:446
virtual iteratort begin() override
virtual iteratort end() override
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, const std::vector< irep_idt > &subs_to_find)
Find identifiers with id ID_symbol of the sub expressions and the subs with ID in subs_to_find consid...
std::unordered_set< irep_idt > find_symbols_sett
Goto Programs with Functions.
Symbol Table + CFG.
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
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