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(goto_programt &goto_program);
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  forall_expr_list(o_it, objects)
51  {
52  if(o_it->id()==ID_symbol)
53  {
54  const irep_idt &identifier=to_symbol_expr(*o_it).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(o_it->id()==ID_dereference)
61  {
62  }
63  }
64 }
65 
67 {
68  uninitialized_analysis(goto_program, ns);
69 
70  // find out which variables need tracking
71 
72  tracking.clear();
73  forall_goto_program_instructions(i_it, goto_program)
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.move(new_symbol);
97  }
98 
99  Forall_goto_program_instructions(i_it, goto_program)
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  {
113  goto_programt::targett i1=goto_program.insert_after(i_it);
114  goto_programt::targett i2=goto_program.insert_after(i1);
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  forall_expr_list(it, read)
146  {
147  if(it->id()==ID_symbol)
148  {
149  const irep_idt &identifier=to_symbol_expr(*it).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  forall_expr_list(it, written)
173  {
174  if(it->id()==ID_symbol)
175  {
176  const irep_idt &identifier=to_symbol_expr(*it).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 
199  goto_functionst &goto_functions)
200 {
201  Forall_goto_functions(f_it, goto_functions)
202  {
203  uninitializedt uninitialized(symbol_table);
204 
205  uninitialized.add_assertions(f_it->second.body);
206  }
207 }
208 
210  const class symbol_tablet &symbol_table,
211  const goto_functionst &goto_functions,
212  std::ostream &out)
213 {
214  const namespacet ns(symbol_table);
215 
216  forall_goto_functions(f_it, goto_functions)
217  {
218  if(f_it->second.body_available())
219  {
220  out << "////\n";
221  out << "//// Function: " << f_it->first << '\n';
222  out << "////\n\n";
224  uninitialized_analysis(f_it->second.body, ns);
225  uninitialized_analysis.output(ns, f_it->second.body, out);
226  }
227  }
228 }
irep_idt name
The unique identifier.
Definition: symbol.h:46
Detection for Uninitialized Local Variables.
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_thread_local
Definition: symbol.h:70
void show_uninitialized(const class symbol_tablet &symbol_table, const goto_functionst &goto_functions, std::ostream &out)
uninitializedt(symbol_tablet &_symbol_table)
irep_idt mode
Language mode.
Definition: symbol.h:55
void get_tracking(goto_programt::const_targett i_it)
which variables need tracking, i.e., are uninitialized and may be read?
symbol_tablet & symbol_table
const irep_idt & get_identifier() const
Definition: std_expr.h:120
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:49
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
bool is_static_lifetime
Definition: symbol.h:70
void add_uninitialized_locals_assertions(symbol_tablet &symbol_table, goto_functionst &goto_functions)
virtual void output(const namespacet &ns, const goto_functionst &goto_functions, std::ostream &out) const
Definition: ai.cpp:92
instructionst::const_iterator const_targett
The boolean constant true.
Definition: std_expr.h:3742
A declaration of a local variable.
Definition: std_code.h:192
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:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void objects_read(const exprt &src, std::list< exprt > &dest)
targett insert_after(const_targett target)
Insertion after the given target.
Symbol table.
#define forall_expr_list(it, expr)
Definition: expr.h:36
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
Detection for Uninitialized Local Variables.
The boolean constant false.
Definition: std_expr.h:3753
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#define Forall_goto_functions(it, functions)
bool is_file_local
Definition: symbol.h:71
void objects_written(const exprt &src, std::list< exprt > &dest)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:115
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
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:68
Assignment.
Definition: std_code.h:144
bool is_lvalue
Definition: symbol.h:71