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 
23  const goto_programt &goto_program)
24 {
25  baset::initialize(goto_program);
26  add_vars(goto_program);
27 }
28 
30  const goto_functionst &goto_functions)
31 {
32  baset::initialize(goto_functions);
33  add_vars(goto_functions);
34 }
35 
37  const goto_programt &goto_program)
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
47  goto_program.get_decl_identifiers(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  for(const auto &c : to_struct_union_type(t).components())
93  {
95  identifier, suffix + "." + id2string(c.get_name()), c.type(), dest);
96  }
97  }
98  else if(t.id()==ID_array)
99  {
100  get_entries_rec(identifier, suffix+"[]", t.subtype(), dest);
101  }
102  else if(check_type(t))
103  {
104  dest.push_back(value_set_fivrnst::entryt(identifier, suffix));
105  }
106 }
107 
109  const goto_functionst &goto_functions)
110 {
111  // get the globals
112  std::list<value_set_fivrnst::entryt> globals;
113  get_globals(globals);
114 
116  v.add_vars(globals);
117 
118  forall_goto_functions(f_it, goto_functions)
119  {
120  // get the locals
121  std::set<irep_idt> locals;
122  get_local_identifiers(f_it->second, locals);
123 
124  for(auto l : locals)
125  {
126  const symbolt &symbol=ns.lookup(l);
127 
128  std::list<value_set_fivrnst::entryt> entries;
129  get_entries(symbol, entries);
130  v.add_vars(entries);
131  }
132  }
133 }
134 
136  std::list<value_set_fivrnst::entryt> &dest)
137 {
138  // static ones
139  for(const auto &it : ns.get_symbol_table().symbols)
140  {
141  if(it.second.is_lvalue && it.second.is_static_lifetime)
142  {
143  get_entries(it.second, dest);
144  }
145  }
146 }
147 
149 {
150  if(type.id()==ID_pointer)
151  {
152  switch(track_options)
153  {
154  case TRACK_ALL_POINTERS:
155  { return true; break; }
157  {
158  if(type.id()==ID_pointer)
159  {
160  const typet *t = &type;
161  while(t->id()==ID_pointer) t = &(t->subtype());
162 
163  return (t->id()==ID_code);
164  }
165 
166  break;
167  }
168  default: // don't track.
169  break;
170  }
171  }
172  else if(type.id()==ID_struct ||
173  type.id()==ID_union)
174  {
175  for(const auto &c : to_struct_union_type(type).components())
176  if(check_type(c.type()))
177  return true;
178  }
179  else if(type.id()==ID_array)
180  return check_type(type.subtype());
181  else if(type.id() == ID_symbol_type)
182  return check_type(ns.follow(type));
183 
184  return false;
185 }
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void get_globals(std::list< value_set_fivrnst::entryt > &dest)
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
const componentst & components() const
Definition: std_types.h:205
Symbol table entry.
Definition: symbol.h:27
void get_entries(const symbolt &symbol, std::list< value_set_fivrnst::entryt > &dest)
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:680
const irep_idt & id() const
Definition: irep.h:259
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:126
A collection of goto functions.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
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:72
typet type
Type of symbol.
Definition: symbol.h:31
Value Set Analysis (Flow Insensitive, Validity Regions)
virtual void initialize(const goto_programt &goto_program)
virtual void initialize(const goto_programt &)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
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:38
#define forall_goto_functions(it, functions)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
void add_vars(const goto_functionst &goto_functions)