cprover
value_set_analysis_fivr.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 
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_fivrt::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, irep_id_hash> 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_fivrt::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_fivrt::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_fivrt::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_fivrt::entryt(identifier, suffix));
115  }
116 }
117 
119  const goto_functionst &goto_functions)
120 {
121  // get the globals
122  std::list<value_set_fivrt::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_fivrt::entryt> entries;
139  get_entries(symbol, entries);
140  v.add_vars(entries);
141  }
142  }
143 }
144 
146  std::list<value_set_fivrt::entryt> &dest)
147 {
148  // static ones
150  if(it->second.is_lvalue &&
151  it->second.is_static_lifetime)
152  get_entries(it->second, dest);
153 }
154 
156 {
157  if(type.id()==ID_pointer)
158  {
159  switch(track_options)
160  {
161  case TRACK_ALL_POINTERS:
162  { return true; break; }
164  {
165  if(type.id()==ID_pointer)
166  {
167  const typet *t = &type;
168  while(t->id()==ID_pointer) t = &(t->subtype());
169 
170  return (t->id()==ID_code);
171  }
172 
173  break;
174  }
175  default: // don't track.
176  break;
177  }
178  }
179  else if(type.id()==ID_struct ||
180  type.id()==ID_union)
181  {
182  const struct_typet &struct_type=to_struct_type(type);
183 
184  const struct_typet::componentst &components=
185  struct_type.components();
186 
187  for(struct_typet::componentst::const_iterator
188  it=components.begin();
189  it!=components.end();
190  it++)
191  {
192  if(check_type(it->type()))
193  return true;
194  }
195  }
196  else if(type.id()==ID_array)
197  return check_type(type.subtype());
198  else if(type.id()==ID_symbol)
199  return check_type(ns.follow(type));
200 
201  return false;
202 }
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
virtual void initialize(const goto_programt &goto_program)
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
const symbol_tablet & get_symbol_table() const
Definition: namespace.h:91
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fivrt::entryt > &dest)
void get_local_identifiers(const goto_function_templatet< goto_programt > &goto_function, std::set< irep_idt > &dest)
std::vector< componentt > componentst
Definition: std_types.h:240
const componentst & components() const
Definition: std_types.h:242
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
Structure type.
Definition: std_types.h:296
void add_vars(const goto_functionst &goto_functions)
bool check_type(const typet &type)
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:64
const irep_idt & id() const
Definition: irep.h:189
symbolst symbols
Definition: symbol_table.h:57
virtual void initialize(const goto_programt &goto_program)
void add_vars(const std::list< entryt > &vars)
Symbol table.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
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
void get_globals(std::list< value_set_fivrt::entryt > &dest)
const typet & subtype() const
Definition: type.h:31
void get_entries(const symbolt &symbol, std::list< value_set_fivrt::entryt > &dest)
#define forall_goto_functions(it, functions)
Value Set Propagation.