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 
32 
33 protected:
37 
38  // The variables that need tracking,
39  // i.e., are uninitialized and may be read?
40  std::set<irep_idt> tracking;
41 
43 };
44 
47 {
48  std::list<exprt> objects=objects_read(*i_it);
49 
50  for(const auto &object : objects)
51  {
52  if(object.id() == ID_symbol)
53  {
54  const irep_idt &identifier = to_symbol_expr(object).get_identifier();
55  const std::set<irep_idt> &uninitialized=
56  uninitialized_analysis[i_it].uninitialized;
57  if(uninitialized.find(identifier)!=uninitialized.end())
58  tracking.insert(identifier);
59  }
60  else if(object.id() == ID_dereference)
61  {
62  }
63  }
64 }
65 
67 {
69 
70  // find out which variables need tracking
71 
72  tracking.clear();
74  get_tracking(i_it);
75 
76  // add tracking symbols to symbol table
77  for(std::set<irep_idt>::const_iterator
78  it=tracking.begin();
79  it!=tracking.end();
80  it++)
81  {
82  const symbolt &symbol=ns.lookup(*it);
83 
84  symbolt new_symbol;
85  new_symbol.name=id2string(symbol.name)+"#initialized";
86  new_symbol.type=bool_typet();
87  new_symbol.base_name=id2string(symbol.base_name)+"#initialized";
88  new_symbol.location=symbol.location;
89  new_symbol.mode=symbol.mode;
90  new_symbol.module=symbol.module;
91  new_symbol.is_thread_local=true;
92  new_symbol.is_static_lifetime=false;
93  new_symbol.is_file_local=true;
94  new_symbol.is_lvalue=true;
95 
96  symbol_table.insert(std::move(new_symbol));
97  }
98 
100  {
101  goto_programt::instructiont &instruction=*i_it;
102 
103  if(instruction.is_decl())
104  {
105  // if we track it, add declaration and assignment
106  // for tracking variable!
107 
108  const irep_idt &identifier=
109  to_code_decl(instruction.code).get_identifier();
110 
111  if(tracking.find(identifier)!=tracking.end())
112  {
115  i_it++, i_it++;
116 
117  const irep_idt new_identifier=
118  id2string(identifier)+"#initialized";
119 
120  symbol_exprt symbol_expr;
121  symbol_expr.set_identifier(new_identifier);
122  symbol_expr.type()=bool_typet();
123  i1->type=DECL;
124  i1->source_location=instruction.source_location;
125  i1->code=code_declt(symbol_expr);
126 
127  i2->type=ASSIGN;
128  i2->source_location=instruction.source_location;
129  i2->code=code_assignt(symbol_expr, false_exprt());
130  }
131  }
132  else
133  {
134  std::list<exprt> read=objects_read(instruction);
135  std::list<exprt> written=objects_written(instruction);
136 
137  // if(instruction.is_function_call())
138  // const code_function_callt &code_function_call=
139  // to_code_function_call(instruction.code);
140 
141  const std::set<irep_idt> &uninitialized=
142  uninitialized_analysis[i_it].uninitialized;
143 
144  // check tracking variables
145  for(const auto &object : read)
146  {
147  if(object.id() == ID_symbol)
148  {
149  const irep_idt &identifier = to_symbol_expr(object).get_identifier();
150 
151  if(uninitialized.find(identifier)!=uninitialized.end())
152  {
153  assert(tracking.find(identifier)!=tracking.end());
154  const irep_idt new_identifier=id2string(identifier)+"#initialized";
155 
156  // insert assertion
157  goto_programt::instructiont assertion;
158  assertion.type=ASSERT;
159  assertion.guard=symbol_exprt(new_identifier, bool_typet());
160  assertion.source_location=instruction.source_location;
161  assertion.source_location.set_comment(
162  "use of uninitialized local variable");
163  assertion.source_location.set_property_class("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;
183  assignment.type=ASSIGN;
184  assignment.code=code_assignt(
185  symbol_exprt(new_identifier, bool_typet()), true_exprt());
186  assignment.source_location=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  Forall_goto_functions(f_it, goto_model.goto_functions)
200  {
201  uninitializedt uninitialized(goto_model.symbol_table);
202 
203  uninitialized.add_assertions(f_it->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  forall_goto_functions(f_it, goto_model.goto_functions)
214  {
215  if(f_it->second.body_available())
216  {
217  out << "////\n";
218  out << "//// Function: " << f_it->first << '\n';
219  out << "////\n\n";
220  uninitialized_analysist uninitialized_analysis;
221  uninitialized_analysis(f_it->second.body, ns);
222  uninitialized_analysis.output(ns, f_it->second.body, out);
223  }
224  }
225 }
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
irep_idt name
The unique identifier.
Definition: symbol.h:43
Detection for Uninitialized Local Variables.
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:289
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:441
bool is_thread_local
Definition: symbol.h:67
void set_property_class(const irep_idt &property_class)
uninitializedt(symbol_tablet &_symbol_table)
irep_idt mode
Language mode.
Definition: symbol.h:52
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
void get_tracking(goto_programt::const_targett i_it)
which variables need tracking, i.e., are uninitialized and may be read?
void set_comment(const irep_idt &comment)
symbol_tablet & symbol_table
const irep_idt & get_identifier() const
Definition: std_expr.h:128
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:46
typet & type()
Definition: expr.h:56
The proper Booleans.
Definition: std_types.h:34
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void show_uninitialized(const goto_modelt &goto_model, std::ostream &out)
bool is_static_lifetime
Definition: symbol.h:67
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Definition: ai.cpp:92
The boolean constant true.
Definition: std_expr.h:4488
instructionst::iterator targett
Definition: goto_program.h:397
A declaration of a local variable.
Definition: std_code.h:253
API to expression classes.
std::set< irep_idt > tracking
const irep_idt & get_identifier() const
Definition: std_code.cpp:14
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
targett insert_after(const_targett target)
Insertion after the given target.
Definition: goto_program.h:480
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
void objects_read(const exprt &src, std::list< exprt > &dest)
Author: Diffblue Ltd.
Detection for Uninitialized Local Variables.
The boolean constant false.
Definition: std_expr.h:4499
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
source_locationt source_location
The location of the instruction in the source file.
Definition: goto_program.h:182
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
#define Forall_goto_functions(it, functions)
bool is_file_local
Definition: symbol.h:68
void add_uninitialized_locals_assertions(goto_modelt &goto_model)
void objects_written(const exprt &src, std::list< exprt > &dest)
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:123
goto_programt & goto_program
Definition: cover.cpp:63
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
void add_assertions(goto_programt &goto_program)
uninitialized_analysist uninitialized_analysis
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
bool is_lvalue
Definition: symbol.h:68