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 
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_fit::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 
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  for(const auto &c : to_struct_union_type(t).components())
103  {
105  identifier, suffix + "." + id2string(c.get_name()), c.type(), 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_fit::entryt(identifier, suffix));
115  }
116 }
117 
119  const goto_functionst &goto_functions)
120 {
121  // get the globals
122  std::list<value_set_fit::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_fit::entryt> entries;
139  get_entries(symbol, entries);
140  v.add_vars(entries);
141  }
142  }
143 }
144 
146  std::list<value_set_fit::entryt> &dest)
147 {
148  // static ones
149  for(const auto &symbol_pair : ns.get_symbol_table().symbols)
150  {
151  if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
152  {
153  get_entries(symbol_pair.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  for(const auto &c : to_struct_union_type(type).components())
186  {
187  if(check_type(c.type()))
188  return true;
189  }
190  }
191  else if(type.id()==ID_array)
192  return check_type(type.subtype());
193  else if(type.id() == ID_struct_tag || type.id() == ID_union_tag)
194  return check_type(ns.follow(type));
195 
196  return false;
197 }
198 
200  const irep_idt &function_id,
202  const exprt &expr)
203 {
205  state.value_set.function_numbering.number(function_id);
207  state.value_set.function_numbering.number(function_id);
208  state.value_set.from_target_index = l->location_number;
209  state.value_set.to_target_index = l->location_number;
210  return state.value_set.get_value_set(expr, ns);
211 }
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet::subtype
const typet & subtype() const
Definition: type.h:47
value_set_fit::function_numbering
static hash_numbering< irep_idt, irep_id_hash > function_numbering
Definition: value_set_fi.h:42
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
typet
The type of an expression, extends irept.
Definition: type.h:29
value_set_analysis_fit::get_entries_rec
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fit::entryt > &dest)
Definition: value_set_analysis_fi.cpp:91
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
prefix.h
value_set_fit::entryt
Definition: value_set_fi.h:174
value_set_fit::from_function
unsigned from_function
Definition: value_set_fi.h:39
exprt
Base class for all expressions.
Definition: expr.h:53
xml_irep.h
goto_programt::get_decl_identifiers
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
Definition: goto_program.cpp:229
value_set_domain_fit::value_set
value_set_fit value_set
Definition: value_set_domain_fi.h:23
value_set_fit::from_target_index
unsigned from_target_index
Definition: value_set_fi.h:40
value_set_fit
Definition: value_set_fi.h:30
value_set_fit::to_target_index
unsigned to_target_index
Definition: value_set_fi.h:40
flow_insensitive_analysis_baset::initialize
virtual void initialize(const goto_programt &)
Definition: flow_insensitive_analysis.h:111
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
value_set_analysis_fit::initialize
void initialize(const goto_programt &goto_program) override
Definition: value_set_analysis_fi.cpp:22
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
value_set_fit::get_value_set
void get_value_set(const exprt &expr, std::list< exprt > &dest, const namespacet &ns) const
Definition: value_set_fi.cpp:297
language_util.h
value_set_analysis_fit::get_globals
void get_globals(std::list< value_set_fit::entryt > &dest)
Definition: value_set_analysis_fi.cpp:145
irept::id
const irep_idt & id() const
Definition: irep.h:418
get_local_identifiers
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...
Definition: goto_function.cpp:18
value_set_analysis_fi.h
Value Set Propagation (flow insensitive)
cprover_prefix.h
value_set_analysis_fit::check_type
bool check_type(const typet &type)
Definition: value_set_analysis_fi.cpp:158
flow_insensitive_analysis_baset::ns
const namespacet & ns
Definition: flow_insensitive_analysis.h:156
value_set_analysis_fit::TRACK_FUNCTION_POINTERS
@ TRACK_FUNCTION_POINTERS
Definition: value_set_analysis_fi.h:25
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
flow_insensitive_analysist< value_set_domain_fit >::state
value_set_domain_fit state
Definition: flow_insensitive_analysis.h:256
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
flow_insensitive_analysis_baset::locationt
goto_programt::const_targett locationt
Definition: flow_insensitive_analysis.h:94
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:124
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
value_set_analysis_fit::get_entries
void get_entries(const symbolt &symbol, std::list< value_set_fit::entryt > &dest)
Definition: value_set_analysis_fi.cpp:84
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
value_set_fit::to_function
unsigned to_function
Definition: value_set_fi.h:39
value_set_fit::add_vars
void add_vars(const std::list< entryt > &vars)
Definition: value_set_fi.h:251
value_set_analysis_fit::get_values
void get_values(const irep_idt &function_id, locationt l, const exprt &expr, std::list< exprt > &dest) override
Definition: value_set_analysis_fi.h:62
symbol_table.h
Author: Diffblue Ltd.
value_set_analysis_fit::track_options
track_optionst track_options
Definition: value_set_analysis_fi.h:42
value_set_analysis_fit::add_vars
void add_vars(const goto_functionst &goto_functions)
Definition: value_set_analysis_fi.cpp:118
value_set_analysis_fit::TRACK_ALL_POINTERS
@ TRACK_ALL_POINTERS
Definition: value_set_analysis_fi.h:25
goto_programt::decl_identifierst
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:816
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40