cprover
value_set_analysis_fi.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Propagation (Flow Insensitive)
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  CM Wintersteiger
7 
8 \*******************************************************************/
9 
12 
13 #include "value_set_analysis_fi.h"
14 
15 #include <util/prefix.h>
16 #include <util/cprover_prefix.h>
17 #include <util/xml_irep.h>
18 #include <util/symbol_table.h>
19 
20 #include <langapi/language_util.h>
21 
24 {
27 }
28 
30  const goto_functionst &goto_functions)
31 {
32  baset::initialize(goto_functions);
33  add_vars(goto_functions);
34 }
35 
38 {
39  typedef std::list<value_set_fit::entryt> entry_listt;
40 
41  // get the globals
42  entry_listt globals;
43  get_globals(globals);
44 
45  // get the locals
48 
49  // cache the list for the locals to speed things up
50  typedef std::unordered_map<irep_idt, entry_listt> entry_cachet;
51  entry_cachet entry_cache;
52 
54 
55  for(goto_programt::instructionst::const_iterator
56  i_it=goto_program.instructions.begin();
57  i_it!=goto_program.instructions.end();
58  i_it++)
59  {
60  v.add_vars(globals);
61 
62  for(goto_programt::decl_identifierst::const_iterator
63  l_it=locals.begin();
64  l_it!=locals.end();
65  l_it++)
66  {
67  // cache hit?
68  entry_cachet::const_iterator e_it=entry_cache.find(*l_it);
69 
70  if(e_it==entry_cache.end())
71  {
72  const symbolt &symbol=ns.lookup(*l_it);
73 
74  std::list<value_set_fit::entryt> &entries=entry_cache[*l_it];
75  get_entries(symbol, entries);
76  v.add_vars(entries);
77  }
78  else
79  v.add_vars(e_it->second);
80  }
81  }
82 }
83 
85  const symbolt &symbol,
86  std::list<value_set_fit::entryt> &dest)
87 {
88  get_entries_rec(symbol.name, "", symbol.type, dest);
89 }
90 
92  const irep_idt &identifier,
93  const std::string &suffix,
94  const typet &type,
95  std::list<value_set_fit::entryt> &dest)
96 {
97  const typet &t=ns.follow(type);
98 
99  if(t.id()==ID_struct ||
100  t.id()==ID_union)
101  {
102  const struct_union_typet &struct_type=to_struct_union_type(t);
103 
104  const struct_typet::componentst &c=struct_type.components();
105 
106  for(struct_typet::componentst::const_iterator
107  it=c.begin();
108  it!=c.end();
109  it++)
110  {
112  identifier,
113  suffix+"."+it->get_string(ID_name),
114  it->type(),
115  dest);
116  }
117  }
118  else if(t.id()==ID_array)
119  {
120  get_entries_rec(identifier, suffix+"[]", t.subtype(), dest);
121  }
122  else if(check_type(t))
123  {
124  dest.push_back(value_set_fit::entryt(identifier, suffix));
125  }
126 }
127 
129  const goto_functionst &goto_functions)
130 {
131  // get the globals
132  std::list<value_set_fit::entryt> globals;
133  get_globals(globals);
134 
136  v.add_vars(globals);
137 
138  forall_goto_functions(f_it, goto_functions)
139  {
140  // get the locals
141  std::set<irep_idt> locals;
142  get_local_identifiers(f_it->second, locals);
143 
144  for(auto l : locals)
145  {
146  const symbolt &symbol=ns.lookup(l);
147 
148  std::list<value_set_fit::entryt> entries;
149  get_entries(symbol, entries);
150  v.add_vars(entries);
151  }
152  }
153 }
154 
156  std::list<value_set_fit::entryt> &dest)
157 {
158  // static ones
159  for(const auto &symbol_pair : ns.get_symbol_table().symbols)
160  {
161  if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
162  {
163  get_entries(symbol_pair.second, dest);
164  }
165  }
166 }
167 
169 {
170  if(type.id()==ID_pointer)
171  {
172  switch(track_options)
173  {
174  case TRACK_ALL_POINTERS:
175  { return true; break; }
177  {
178  if(type.id()==ID_pointer)
179  {
180  const typet *t = &type;
181  while(t->id()==ID_pointer) t = &(t->subtype());
182 
183  return (t->id()==ID_code);
184  }
185 
186  break;
187  }
188  default: // don't track.
189  break;
190  }
191  }
192  else if(type.id()==ID_struct ||
193  type.id()==ID_union)
194  {
195  const struct_union_typet &struct_type=to_struct_union_type(type);
196 
197  const struct_typet::componentst &components=
198  struct_type.components();
199 
200  for(struct_typet::componentst::const_iterator
201  it=components.begin();
202  it!=components.end();
203  it++)
204  {
205  if(check_type(it->type()))
206  return true;
207  }
208  }
209  else if(type.id()==ID_array)
210  return check_type(type.subtype());
211  else if(type.id()==ID_symbol)
212  return check_type(ns.follow(type));
213 
214  return false;
215 }
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
const symbol_tablet & get_symbol_table() const
Definition: namespace.h:106
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
std::vector< componentt > componentst
Definition: std_types.h:243
const componentst & components() const
Definition: std_types.h:245
void add_vars(const goto_functionst &goto_functions)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void get_entries(const symbolt &symbol, std::list< value_set_fit::entryt > &dest)
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:640
const irep_idt & id() const
Definition: irep.h:189
bool check_type(const typet &type)
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
virtual void initialize(const goto_programt &goto_program)
const typet & follow(const typet &) const
Definition: namespace.cpp:55
Author: Diffblue Ltd.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
const symbolst & symbols
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fit::entryt > &dest)
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
virtual void initialize(const goto_programt &goto_program)
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:162
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
goto_programt & goto_program
Definition: cover.cpp:63
Value Set Propagation (flow insensitive)
const typet & subtype() const
Definition: type.h:33
#define forall_goto_functions(it, functions)
void get_globals(std::list< value_set_fit::entryt > &dest)
void add_vars(const std::list< entryt > &vars)
Definition: value_set_fi.h:250
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130