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