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/symbol_table.h>
16 
18  const goto_programt &goto_program)
19 {
20  baset::initialize(goto_program);
21  add_vars(goto_program);
22 }
23 
25  const goto_functionst &goto_functions)
26 {
27  baset::initialize(goto_functions);
28  add_vars(goto_functions);
29 }
30 
32  const goto_programt &goto_program)
33 {
34  typedef std::list<value_set_fit::entryt> entry_listt;
35 
36  // get the globals
37  entry_listt globals;
38  get_globals(globals);
39 
40  // get the locals
42  goto_program.get_decl_identifiers(locals);
43 
44  // cache the list for the locals to speed things up
45  typedef std::unordered_map<irep_idt, entry_listt> entry_cachet;
46  entry_cachet entry_cache;
47 
49 
50  for(goto_programt::instructionst::const_iterator
51  i_it=goto_program.instructions.begin();
52  i_it!=goto_program.instructions.end();
53  i_it++)
54  {
55  v.add_vars(globals);
56 
57  for(goto_programt::decl_identifierst::const_iterator
58  l_it=locals.begin();
59  l_it!=locals.end();
60  l_it++)
61  {
62  // cache hit?
63  entry_cachet::const_iterator e_it=entry_cache.find(*l_it);
64 
65  if(e_it==entry_cache.end())
66  {
67  const symbolt &symbol=ns.lookup(*l_it);
68 
69  std::list<value_set_fit::entryt> &entries=entry_cache[*l_it];
70  get_entries(symbol, entries);
71  v.add_vars(entries);
72  }
73  else
74  v.add_vars(e_it->second);
75  }
76  }
77 }
78 
80  const symbolt &symbol,
81  std::list<value_set_fit::entryt> &dest)
82 {
83  get_entries_rec(symbol.name, "", symbol.type, dest);
84 }
85 
87  const irep_idt &identifier,
88  const std::string &suffix,
89  const typet &type,
90  std::list<value_set_fit::entryt> &dest)
91 {
92  const typet &t=ns.follow(type);
93 
94  if(t.id()==ID_struct ||
95  t.id()==ID_union)
96  {
97  for(const auto &c : to_struct_union_type(t).components())
98  {
100  identifier, suffix + "." + id2string(c.get_name()), c.type(), dest);
101  }
102  }
103  else if(t.id()==ID_array)
104  {
105  get_entries_rec(identifier, suffix+"[]", t.subtype(), dest);
106  }
107  else if(check_type(t))
108  {
109  dest.push_back(value_set_fit::entryt(identifier, suffix));
110  }
111 }
112 
114  const goto_functionst &goto_functions)
115 {
116  // get the globals
117  std::list<value_set_fit::entryt> globals;
118  get_globals(globals);
119 
121  v.add_vars(globals);
122 
123  for(const auto &gf_entry : goto_functions.function_map)
124  {
125  // get the locals
126  std::set<irep_idt> locals;
127  get_local_identifiers(gf_entry.second, locals);
128 
129  for(auto l : locals)
130  {
131  const symbolt &symbol=ns.lookup(l);
132 
133  std::list<value_set_fit::entryt> entries;
134  get_entries(symbol, entries);
135  v.add_vars(entries);
136  }
137  }
138 }
139 
141  std::list<value_set_fit::entryt> &dest)
142 {
143  // static ones
144  for(const auto &symbol_pair : ns.get_symbol_table().symbols)
145  {
146  if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
147  {
148  get_entries(symbol_pair.second, dest);
149  }
150  }
151 }
152 
154 {
155  if(type.id()==ID_pointer)
156  {
157  switch(track_options)
158  {
159  case TRACK_ALL_POINTERS:
160  { return true; break; }
162  {
163  if(type.id()==ID_pointer)
164  {
165  const typet *t = &type;
166  while(t->id()==ID_pointer) t = &(t->subtype());
167 
168  return (t->id()==ID_code);
169  }
170 
171  break;
172  }
173  default: // don't track.
174  break;
175  }
176  }
177  else if(type.id()==ID_struct ||
178  type.id()==ID_union)
179  {
180  for(const auto &c : to_struct_union_type(type).components())
181  {
182  if(check_type(c.type()))
183  return true;
184  }
185  }
186  else if(type.id()==ID_array)
187  return check_type(type.subtype());
188  else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
189  return check_type(ns.follow(type));
190 
191  return false;
192 }
193 
195  const irep_idt &function_id,
197  const exprt &expr)
198 {
203  state.value_set.from_target_index = l->location_number;
204  state.value_set.to_target_index = l->location_number;
205  return state.value_set.get_value_set(expr, ns);
206 }
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
goto_programt::const_targett locationt
virtual void initialize(const goto_programt &)
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:880
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
const irep_idt & id() const
Definition: irep.h:407
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:49
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:123
number_type number(const key_type &a)
Definition: numbering.h:37
const componentst & components() const
Definition: std_types.h:147
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Symbol table entry.
Definition: symbol.h:28
typet type
Type of symbol.
Definition: symbol.h:31
irep_idt name
The unique identifier.
Definition: symbol.h:40
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
bool check_type(const typet &type)
std::vector< exprt > get_values(const irep_idt &function_id, locationt l, const exprt &expr) override
void get_entries(const symbolt &symbol, std::list< value_set_fit::entryt > &dest)
void add_vars(const goto_functionst &goto_functions)
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fit::entryt > &dest)
void get_globals(std::list< value_set_fit::entryt > &dest)
void initialize(const goto_programt &goto_program) override
static numberingt< irep_idt > function_numbering
Definition: value_set_fi.h:42
void add_vars(const std::list< entryt > &vars)
Definition: value_set_fi.h:245
std::vector< exprt > get_value_set(const exprt &expr, const namespacet &ns) const
unsigned from_function
Definition: value_set_fi.h:39
unsigned to_function
Definition: value_set_fi.h:39
unsigned from_target_index
Definition: value_set_fi.h:40
unsigned to_target_index
Definition: value_set_fi.h:40
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 std::string & id2string(const irep_idt &d)
Definition: irep.h:49
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
Author: Diffblue Ltd.
Value Set Propagation (flow insensitive)