cprover
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 <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
25#include "goto_functions.h"
26#include "goto_model.h"
27
29 goto_modelt &goto_model,
30 message_handlert &message_handler)
31{
32 // gather all functions reachable from the entry point
33 const irep_idt entry_point=goto_functionst::entry_point();
34 goto_functionst &goto_functions=goto_model.goto_functions;
35
36 if(goto_functions.function_map.count(entry_point) == 0)
37 throw user_input_error_exceptiont("entry point not found");
38
39 // Get the call graph restricted to functions reachable from
40 // the entry point:
41 call_grapht call_graph =
42 call_grapht::create_from_root_function(goto_model, entry_point, false);
43 const auto directed_graph = call_graph.get_directed_graph();
45 !directed_graph.empty(),
46 "at least " + id2string(entry_point) + " should be reachable");
47
48 // gather all symbols used by reachable functions
49
51
52 for(std::size_t node_idx = 0; node_idx < directed_graph.size(); ++node_idx)
53 {
54 const irep_idt &id = directed_graph[node_idx].function;
55 if(id == INITIALIZE_FUNCTION)
56 continue;
57
58 // assume function has no body if it is not in the function map
59 const auto &it = goto_functions.function_map.find(id);
60 if(it == goto_functions.function_map.end())
61 continue;
62
63 for(const auto &i : it->second.body.instructions)
64 {
65 i.apply([&symbols_to_keep](const exprt &expr) {
67 });
68 }
69 }
70
71 goto_functionst::function_mapt::iterator f_it;
72 f_it=goto_functions.function_map.find(INITIALIZE_FUNCTION);
73
74 if(f_it == goto_functions.function_map.end())
75 throw incorrect_goto_program_exceptiont("initialize function not found");
76
77 goto_programt &goto_program=f_it->second.body;
78
79 // add all symbols from right-hand sides of required symbols
80 bool fixed_point_reached = false;
81 // markers for each instruction to avoid repeatedly searching the same
82 // instruction for new symbols; initialized to false, and set to true whenever
83 // an instruction is determined to be irrelevant (not an assignment) or
84 // symbols have been collected from it
85 std::vector<bool> seen(goto_program.instructions.size(), false);
87 {
89
90 std::vector<bool>::iterator seen_it = seen.begin();
91 for(const auto &instruction : goto_program.instructions)
92 {
93 if(!*seen_it && instruction.is_assign())
94 {
95 const irep_idt id =
96 to_symbol_expr(instruction.assign_lhs()).get_identifier();
97
98 // if we are to keep the left-hand side, then we also need to keep all
99 // symbols occurring in the right-hand side
100 if(
102 symbols_to_keep.find(id) != symbols_to_keep.end())
103 {
104 fixed_point_reached = false;
105 find_symbols(instruction.assign_rhs(), symbols_to_keep);
106 *seen_it = true;
107 }
108 }
109 else if(!*seen_it)
110 *seen_it = true;
111
112 ++seen_it;
113 }
114 }
115
116 // now remove unnecessary initializations
117 bool changed = false;
118 for(auto it = goto_model.symbol_table.begin();
119 it != goto_model.symbol_table.end();
120 ++it)
121 {
122 if(
123 it->second.is_static_lifetime && !it->second.is_type &&
124 !it->second.is_macro && it->second.type.id() != ID_code &&
125 !has_prefix(id2string(it->first), CPROVER_PREFIX) &&
126 symbols_to_keep.find(it->first) == symbols_to_keep.end())
127 {
128 symbolt &symbol = it.get_writeable_symbol();
129 symbol.is_extern = true;
130 symbol.value.make_nil();
132 changed = true;
133 }
134 }
135
136 if(changed && goto_model.can_produce_function(INITIALIZE_FUNCTION))
137 recreate_initialize_function(goto_model, message_handler);
138}
Function Call Graphs.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:39
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:420
void make_nil()
Definition irep.h:454
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
bool has_prefix(const std::string &s, const std::string &prefix)
Definition converter.cpp:13
#define CPROVER_PREFIX
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings)
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: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
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:222