cprover
value_set_analysis_fivrns.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Value Set Propagation (Flow Insensitive, Validity Regions)
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  CM Wintersteiger
7 
8 \*******************************************************************/
9 
12 
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_fivrnst::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  v.add_vars(globals);
55 
56  for(auto l : locals)
57  {
58  // cache hit?
59  entry_cachet::const_iterator e_it=entry_cache.find(l);
60 
61  if(e_it==entry_cache.end())
62  {
63  const symbolt &symbol=ns.lookup(l);
64 
65  std::list<value_set_fivrnst::entryt> &entries=entry_cache[l];
66  get_entries(symbol, entries);
67  v.add_vars(entries);
68  }
69  else
70  v.add_vars(e_it->second);
71  }
72 }
73 
75  const symbolt &symbol,
76  std::list<value_set_fivrnst::entryt> &dest)
77 {
78  get_entries_rec(symbol.name, "", symbol.type, dest);
79 }
80 
82  const irep_idt &identifier,
83  const std::string &suffix,
84  const typet &type,
85  std::list<value_set_fivrnst::entryt> &dest)
86 {
87  const typet &t=ns.follow(type);
88 
89  if(t.id()==ID_struct ||
90  t.id()==ID_union)
91  {
92  const struct_typet &struct_type=to_struct_type(t);
93 
94  const struct_typet::componentst &c=struct_type.components();
95 
96  for(struct_typet::componentst::const_iterator
97  it=c.begin();
98  it!=c.end();
99  it++)
100  {
102  identifier,
103  suffix+"."+it->get_string(ID_name),
104  it->type(),
105  dest);
106  }
107  }
108  else if(t.id()==ID_array)
109  {
110  get_entries_rec(identifier, suffix+"[]", t.subtype(), dest);
111  }
112  else if(check_type(t))
113  {
114  dest.push_back(value_set_fivrnst::entryt(identifier, suffix));
115  }
116 }
117 
119  const goto_functionst &goto_functions)
120 {
121  // get the globals
122  std::list<value_set_fivrnst::entryt> globals;
123  get_globals(globals);
124 
126  v.add_vars(globals);
127 
128  forall_goto_functions(f_it, goto_functions)
129  {
130  // get the locals
131  std::set<irep_idt> locals;
132  get_local_identifiers(f_it->second, locals);
133 
134  for(auto l : locals)
135  {
136  const symbolt &symbol=ns.lookup(l);
137 
138  std::list<value_set_fivrnst::entryt> entries;
139  get_entries(symbol, entries);
140  v.add_vars(entries);
141  }
142  }
143 }
144 
146  std::list<value_set_fivrnst::entryt> &dest)
147 {
148  // static ones
149  for(const auto &it : ns.get_symbol_table().symbols)
150  {
151  if(it.second.is_lvalue && it.second.is_static_lifetime)
152  {
153  get_entries(it.second, dest);
154  }
155  }
156 }
157 
159 {
160  if(type.id()==ID_pointer)
161  {
162  switch(track_options)
163  {
164  case TRACK_ALL_POINTERS:
165  { return true; break; }
167  {
168  if(type.id()==ID_pointer)
169  {
170  const typet *t = &type;
171  while(t->id()==ID_pointer) t = &(t->subtype());
172 
173  return (t->id()==ID_code);
174  }
175 
176  break;
177  }
178  default: // don't track.
179  break;
180  }
181  }
182  else if(type.id()==ID_struct ||
183  type.id()==ID_union)
184  {
185  const struct_typet &struct_type=to_struct_type(type);
186 
187  const struct_typet::componentst &components=
188  struct_type.components();
189 
190  for(struct_typet::componentst::const_iterator
191  it=components.begin();
192  it!=components.end();
193  it++)
194  {
195  if(check_type(it->type()))
196  return true;
197  }
198  }
199  else if(type.id()==ID_array)
200  return check_type(type.subtype());
201  else if(type.id()==ID_symbol)
202  return check_type(ns.follow(type));
203 
204  return false;
205 }
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_globals(std::list< value_set_fivrnst::entryt > &dest)
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
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
Structure type.
Definition: std_types.h:297
void get_entries(const symbolt &symbol, std::list< value_set_fivrnst::entryt > &dest)
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:640
const irep_idt & id() const
Definition: irep.h:259
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Author: Diffblue Ltd.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
const symbolst & symbols
void add_vars(const std::list< entryt > &vars)
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
Value Set Analysis (Flow Insensitive, Validity Regions)
virtual void initialize(const goto_programt &goto_program)
virtual void initialize(const goto_programt &)
goto_programt & goto_program
Definition: cover.cpp:63
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrnst::entryt > &dest)
const typet & subtype() const
Definition: type.h:33
#define forall_goto_functions(it, functions)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
void add_vars(const goto_functionst &goto_functions)