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, irep_id_hash> 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  const struct_union_typet &struct_type=to_struct_union_type(t);
103 
104  const struct_typet::componentst &c=struct_type.components();
105 
106  for(struct_typet::componentst::const_iterator
107  it=c.begin();
108  it!=c.end();
109  it++)
110  {
112  identifier,
113  suffix+"."+it->get_string(ID_name),
114  it->type(),
115  dest);
116  }
117  }
118  else if(t.id()==ID_array)
119  {
120  get_entries_rec(identifier, suffix+"[]", t.subtype(), dest);
121  }
122  else if(check_type(t))
123  {
124  dest.push_back(value_set_fit::entryt(identifier, suffix));
125  }
126 }
127 
129  const goto_functionst &goto_functions)
130 {
131  // get the globals
132  std::list<value_set_fit::entryt> globals;
133  get_globals(globals);
134 
136  v.add_vars(globals);
137 
138  forall_goto_functions(f_it, goto_functions)
139  {
140  // get the locals
141  std::set<irep_idt> locals;
142  get_local_identifiers(f_it->second, locals);
143 
144  for(auto l : locals)
145  {
146  const symbolt &symbol=ns.lookup(l);
147 
148  std::list<value_set_fit::entryt> entries;
149  get_entries(symbol, entries);
150  v.add_vars(entries);
151  }
152  }
153 }
154 
156  std::list<value_set_fit::entryt> &dest)
157 {
158  // static ones
160  if(it->second.is_lvalue &&
161  it->second.is_static_lifetime)
162  get_entries(it->second, dest);
163 }
164 
166 {
167  if(type.id()==ID_pointer)
168  {
169  switch(track_options)
170  {
171  case TRACK_ALL_POINTERS:
172  { return true; break; }
174  {
175  if(type.id()==ID_pointer)
176  {
177  const typet *t = &type;
178  while(t->id()==ID_pointer) t = &(t->subtype());
179 
180  return (t->id()==ID_code);
181  }
182 
183  break;
184  }
185  default: // don't track.
186  break;
187  }
188  }
189  else if(type.id()==ID_struct ||
190  type.id()==ID_union)
191  {
192  const struct_union_typet &struct_type=to_struct_union_type(type);
193 
194  const struct_typet::componentst &components=
195  struct_type.components();
196 
197  for(struct_typet::componentst::const_iterator
198  it=components.begin();
199  it!=components.end();
200  it++)
201  {
202  if(check_type(it->type()))
203  return true;
204  }
205  }
206  else if(type.id()==ID_array)
207  return check_type(type.subtype());
208  else if(type.id()==ID_symbol)
209  return check_type(ns.follow(type));
210 
211  return false;
212 }
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
#define forall_symbols(it, expr)
Definition: symbol_table.h:28
const symbol_tablet & get_symbol_table() const
Definition: namespace.h:91
instructionst instructions
The list of instructions in the goto program.
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
void add_vars(const goto_functionst &goto_functions)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:277
void get_entries(const symbolt &symbol, std::list< value_set_fit::entryt > &dest)
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:64
const irep_idt & id() const
Definition: irep.h:189
bool check_type(const typet &type)
symbolst symbols
Definition: symbol_table.h:57
virtual void initialize(const goto_programt &goto_program)
Symbol table.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
void get_entries_rec(const irep_idt &identifier, const std::string &suffix, const typet &type, std::list< value_set_fit::entryt > &dest)
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
virtual void initialize(const goto_programt &goto_program)
Base type of C structs and unions, and C++ classes.
Definition: std_types.h:159
Value Set Propagation (flow insensitive)
const typet & subtype() const
Definition: type.h:31
#define forall_goto_functions(it, functions)
void get_globals(std::list< value_set_fit::entryt > &dest)
void add_vars(const std::list< entryt > &vars)
Definition: value_set_fi.h:221