cprover
uninitialized.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Detection for Uninitialized Local Variables
4
5Author: Daniel Kroening
6
7Date: January 2010
8
9\*******************************************************************/
10
13
14#include "uninitialized.h"
15
16#include <util/std_code.h>
17#include <util/symbol_table.h>
18
20
22{
23public:
24 explicit uninitializedt(symbol_tablet &_symbol_table):
25 symbol_table(_symbol_table),
26 ns(_symbol_table)
27 {
28 }
29
30 void add_assertions(
31 const irep_idt &function_identifer,
32 goto_programt &goto_program);
33
34protected:
38
39 // The variables that need tracking,
40 // i.e., are uninitialized and may be read?
41 std::set<irep_idt> tracking;
42
44};
45
48{
49 std::list<exprt> objects=objects_read(*i_it);
50
51 for(const auto &object : objects)
52 {
53 if(object.id() == ID_symbol)
54 {
55 const irep_idt &identifier = to_symbol_expr(object).get_identifier();
56 const std::set<irep_idt> &uninitialized=
57 uninitialized_analysis[i_it].uninitialized;
58 if(uninitialized.find(identifier)!=uninitialized.end())
59 tracking.insert(identifier);
60 }
61 else if(object.id() == ID_dereference)
62 {
63 }
64 }
65}
66
68 const irep_idt &function_identifier,
69 goto_programt &goto_program)
70{
71 uninitialized_analysis(function_identifier, goto_program, ns);
72
73 // find out which variables need tracking
74
75 tracking.clear();
76 forall_goto_program_instructions(i_it, goto_program)
77 get_tracking(i_it);
78
79 // add tracking symbols to symbol table
80 for(std::set<irep_idt>::const_iterator
81 it=tracking.begin();
82 it!=tracking.end();
83 it++)
84 {
85 const symbolt &symbol=ns.lookup(*it);
86
87 symbolt new_symbol;
88 new_symbol.name=id2string(symbol.name)+"#initialized";
89 new_symbol.type=bool_typet();
90 new_symbol.base_name=id2string(symbol.base_name)+"#initialized";
91 new_symbol.location=symbol.location;
92 new_symbol.mode=symbol.mode;
93 new_symbol.module=symbol.module;
94 new_symbol.is_thread_local=true;
95 new_symbol.is_static_lifetime=false;
96 new_symbol.is_file_local=true;
97 new_symbol.is_lvalue=true;
98
99 symbol_table.insert(std::move(new_symbol));
100 }
101
102 Forall_goto_program_instructions(i_it, goto_program)
103 {
104 goto_programt::instructiont &instruction=*i_it;
105
106 if(instruction.is_decl())
107 {
108 // if we track it, add declaration and assignment
109 // for tracking variable!
110
111 const irep_idt &identifier = instruction.decl_symbol().get_identifier();
112
113 if(tracking.find(identifier)!=tracking.end())
114 {
115 const irep_idt new_identifier=
116 id2string(identifier)+"#initialized";
117
118 symbol_exprt symbol_expr(new_identifier, bool_typet());
120 goto_programt::make_decl(symbol_expr, instruction.source_location());
121
123 symbol_expr, false_exprt(), instruction.source_location());
124
126 goto_program.insert_after(i_it, std::move(i1));
127 goto_program.insert_after(i1_it, std::move(i2));
128 i_it++, i_it++;
129 }
130 }
131 else
132 {
133 std::list<exprt> read=objects_read(instruction);
134 std::list<exprt> written=objects_written(instruction);
135
136 // if(instruction.is_function_call())
137 // const code_function_callt &code_function_call=
138 // to_code_function_call(instruction.code);
139
140 const std::set<irep_idt> &uninitialized=
141 uninitialized_analysis[i_it].uninitialized;
142
143 // check tracking variables
144 for(const auto &object : read)
145 {
146 if(object.id() == ID_symbol)
147 {
148 const irep_idt &identifier = to_symbol_expr(object).get_identifier();
149
150 if(uninitialized.find(identifier)!=uninitialized.end())
151 {
152 assert(tracking.find(identifier)!=tracking.end());
153 const irep_idt new_identifier=id2string(identifier)+"#initialized";
154
155 // insert assertion
158 symbol_exprt(new_identifier, bool_typet()),
159 instruction.source_location());
161 "use of uninitialized local variable " + id2string(identifier));
163 "uninitialized local");
164
165 goto_program.insert_before_swap(i_it, assertion);
166 i_it++;
167 }
168 }
169 }
170
171 // set tracking variables
172 for(const auto &object : written)
173 {
174 if(object.id() == ID_symbol)
175 {
176 const irep_idt &identifier = to_symbol_expr(object).get_identifier();
177
178 if(tracking.find(identifier)!=tracking.end())
179 {
180 const irep_idt new_identifier=id2string(identifier)+"#initialized";
181
182 goto_programt::instructiont assignment =
184 symbol_exprt(new_identifier, bool_typet()),
185 true_exprt(),
186 instruction.source_location());
187
188 goto_program.insert_before_swap(i_it, assignment);
189 i_it++;
190 }
191 }
192 }
193 }
194 }
195}
196
198{
199 for(auto &gf_entry : goto_model.goto_functions.function_map)
200 {
201 uninitializedt uninitialized(goto_model.symbol_table);
202
203 uninitialized.add_assertions(gf_entry.first, gf_entry.second.body);
204 }
205}
206
208 const goto_modelt &goto_model,
209 std::ostream &out)
210{
211 const namespacet ns(goto_model.symbol_table);
212
213 for(const auto &gf_entry : goto_model.goto_functions.function_map)
214 {
215 if(gf_entry.second.body_available())
216 {
217 out << "////\n";
218 out << "//// Function: " << gf_entry.first << '\n';
219 out << "////\n\n";
220 uninitialized_analysist uninitialized_analysis;
221 uninitialized_analysis(gf_entry.first, gf_entry.second.body, ns);
222 uninitialized_analysis.output(
223 ns, gf_entry.first, gf_entry.second.body, out);
224 }
225 }
226}
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition: ai.cpp:40
The Boolean type.
Definition: std_types.h:36
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
The Boolean constant false.
Definition: std_expr.h:2865
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:227
source_locationt & source_location_nonconst()
Definition: goto_program.h:337
const source_locationt & source_location() const
Definition: goto_program.h:332
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
instructionst::iterator targett
Definition: goto_program.h:592
instructionst::const_iterator const_targett
Definition: goto_program.h:593
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:684
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:949
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:922
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
void set_comment(const irep_idt &comment)
void set_property_class(const irep_idt &property_class)
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
The symbol table.
Definition: symbol_table.h:14
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
Symbol table entry.
Definition: symbol.h:28
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
bool is_file_local
Definition: symbol.h:66
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
bool is_static_lifetime
Definition: symbol.h:65
bool is_thread_local
Definition: symbol.h:65
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
bool is_lvalue
Definition: symbol.h:66
irep_idt mode
Language mode.
Definition: symbol.h:49
The Boolean constant true.
Definition: std_expr.h:2856
void add_assertions(const irep_idt &function_identifer, goto_programt &goto_program)
std::set< irep_idt > tracking
void get_tracking(goto_programt::const_targett i_it)
which variables need tracking, i.e., are uninitialized and may be read?
uninitialized_analysist uninitialized_analysis
uninitializedt(symbol_tablet &_symbol_table)
symbol_tablet & symbol_table
void objects_read(const exprt &src, std::list< exprt > &dest)
void objects_written(const exprt &src, std::list< exprt > &dest)
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
Author: Diffblue Ltd.
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
Detection for Uninitialized Local Variables.
Detection for Uninitialized Local Variables.