cprover
invariant_propagation.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Invariant Propagation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "invariant_propagation.h"
13 
14 #include <util/simplify_expr.h>
15 #include <util/base_type.h>
16 #include <util/symbol_table.h>
17 #include <util/std_expr.h>
18 
20 {
21  for(auto &state : state_map)
22  state.second.invariant_set.make_true();
23 }
24 
26 {
27  for(auto &state : state_map)
28  state.second.invariant_set.make_false();
29 }
30 
32  const goto_programt &goto_program)
33 {
34  // get the globals
35  object_listt globals;
36  get_globals(globals);
37 
38  // get the locals
40  goto_program.get_decl_identifiers(locals);
41 
42  // cache the list for the locals to speed things up
43  typedef std::unordered_map<irep_idt, object_listt> object_cachet;
44  object_cachet object_cache;
45 
46  forall_goto_program_instructions(i_it, goto_program)
47  {
48  #if 0
49  invariant_sett &is=(*this)[i_it].invariant_set;
50 
51  is.add_objects(globals);
52  #endif
53 
54  for(const auto &local : locals)
55  {
56  // cache hit?
57  object_cachet::const_iterator e_it=object_cache.find(local);
58 
59  if(e_it==object_cache.end())
60  {
61  const symbolt &symbol=ns.lookup(local);
62 
63  object_listt &objects=object_cache[local];
64  get_objects(symbol, objects);
65  #if 0
66  is.add_objects(objects);
67  #endif
68  }
69  #if 0
70  else
71  is.add_objects(e_it->second);
72  #endif
73  }
74  }
75 }
76 
78  const symbolt &symbol,
79  object_listt &dest)
80 {
81  std::list<exprt> object_list;
82 
83  get_objects_rec(symbol.symbol_expr(), object_list);
84 
85  for(const auto &expr : object_list)
86  dest.push_back(object_store.add(expr));
87 }
88 
90  const exprt &src,
91  std::list<exprt> &dest)
92 {
93  const typet &t=ns.follow(src.type());
94 
95  if(t.id()==ID_struct ||
96  t.id()==ID_union)
97  {
98  const struct_typet &struct_type=to_struct_type(t);
99 
100  for(const auto &component : struct_type.components())
101  {
102  const member_exprt member_expr(
103  src, component.get_name(), component.type());
104  // recursive call
105  get_objects_rec(member_expr, dest);
106  }
107  }
108  else if(t.id()==ID_array)
109  {
110  // get_objects_rec(identifier, suffix+"[]", t.subtype(), dest);
111  // we don't track these
112  }
113  else if(check_type(t))
114  {
115  dest.push_back(src);
116  }
117 }
118 
120  const goto_functionst &goto_functions)
121 {
122  // get the globals
123  object_listt globals;
124  get_globals(globals);
125 
126  forall_goto_functions(f_it, goto_functions)
127  {
128  // get the locals
129  std::set<irep_idt> locals;
130  get_local_identifiers(f_it->second, locals);
131 
132  const goto_programt &goto_program=f_it->second.body;
133 
134  // cache the list for the locals to speed things up
135  typedef std::unordered_map<irep_idt, object_listt> object_cachet;
136  object_cachet object_cache;
137 
138  forall_goto_program_instructions(i_it, goto_program)
139  {
140  #if 0
141  invariant_sett &is=(*this)[i_it].invariant_set;
142 
143  is.add_objects(globals);
144  #endif
145 
146  for(const auto &local : locals)
147  {
148  // cache hit?
149  object_cachet::const_iterator e_it=object_cache.find(local);
150 
151  if(e_it==object_cache.end())
152  {
153  const symbolt &symbol=ns.lookup(local);
154 
155  object_listt &objects=object_cache[local];
156  get_objects(symbol, objects);
157  #if 0
158  is.add_objects(objects);
159  #endif
160  }
161  #if 0
162  else
163  is.add_objects(e_it->second);
164  #endif
165  }
166  }
167  }
168 }
169 
171  object_listt &dest)
172 {
173  // static ones
174  for(const auto &symbol_pair : ns.get_symbol_table().symbols)
175  {
176  if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
177  {
178  get_objects(symbol_pair.second, dest);
179  }
180  }
181 }
182 
184 {
185  if(type.id()==ID_pointer)
186  return true;
187  else if(type.id()==ID_struct ||
188  type.id()==ID_union)
189  return false;
190  else if(type.id()==ID_array)
191  return false;
192  else if(type.id() == ID_symbol_type)
193  return check_type(ns.follow(type));
194  else if(type.id()==ID_unsignedbv ||
195  type.id()==ID_signedbv)
196  return true;
197  else if(type.id()==ID_bool)
198  return true;
199 
200  return false;
201 }
202 
204 {
205  baset::initialize(goto_program);
206 
207  forall_goto_program_instructions(it, goto_program)
208  {
209  invariant_sett &s = (*this)[it].invariant_set;
210 
211  if(it==goto_program.instructions.begin())
212  s.make_true();
213  else
214  s.make_false();
215 
218  s.set_namespace(ns);
219  }
220 
221  add_objects(goto_program);
222 }
223 
225 {
226  baset::initialize(goto_functions);
227 
228  forall_goto_functions(f_it, goto_functions)
229  initialize(f_it->second.body);
230 }
231 
233 {
234  Forall_goto_functions(it, goto_functions)
235  simplify(it->second.body);
236 }
237 
239 {
240  Forall_goto_program_instructions(i_it, goto_program)
241  {
242  if(!i_it->is_assert())
243  continue;
244 
245  // find invariant set
246  const auto &d = (*this)[i_it];
247  if(d.is_bottom())
248  continue;
249 
250  const invariant_sett &invariant_set = d.invariant_set;
251 
252  exprt simplified_guard(i_it->guard);
253 
254  invariant_set.simplify(simplified_guard);
255  ::simplify(simplified_guard, ns);
256 
257  if(invariant_set.implies(simplified_guard).is_true())
258  i_it->guard=true_exprt();
259  }
260 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
invariant_sett::implies
tvt implies(const exprt &expr) const
Definition: invariant_set.cpp:595
invariant_propagationt::object_listt
std::list< unsigned > object_listt
Definition: invariant_propagation.h:56
typet
The type of an expression, extends irept.
Definition: type.h:27
ait< invariant_set_domaint >::state_map
state_mapt state_map
Definition: ai.h:416
invariant_propagationt::ns
const namespacet & ns
Definition: invariant_propagation.h:51
exprt
Base class for all expressions.
Definition: expr.h:54
goto_programt::get_decl_identifiers
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
Definition: goto_program.cpp:222
invariant_sett::set_namespace
void set_namespace(const namespacet &_ns)
Definition: invariant_set.h:158
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
invariant_propagationt::make_all_true
void make_all_true()
Definition: invariant_propagation.cpp:19
invariant_propagationt::initialize
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: invariant_propagation.cpp:203
invariant_propagationt::get_objects
void get_objects(const symbolt &symbol, object_listt &dest)
Definition: invariant_propagation.cpp:77
invariant_propagationt::make_all_false
void make_all_false()
Definition: invariant_propagation.cpp:25
invariant_sett::set_value_sets
void set_value_sets(value_setst &_value_sets)
Definition: invariant_set.h:148
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
inv_object_storet::add
unsigned add(const exprt &expr)
Definition: invariant_set.cpp:64
base_type.h
invariant_propagationt::get_objects_rec
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
Definition: invariant_propagation.cpp:89
invariant_propagationt::add_objects
void add_objects(const goto_programt &goto_program)
Definition: invariant_propagation.cpp:31
invariant_propagationt::check_type
bool check_type(const typet &type) const
Definition: invariant_propagation.cpp:183
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
invariant_propagationt::get_globals
void get_globals(object_listt &globals)
Definition: invariant_propagation.cpp:170
invariant_propagationt::simplify
void simplify(goto_programt &goto_program)
Definition: invariant_propagation.cpp:238
irept::id
const irep_idt & id() const
Definition: irep.h:259
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
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:144
simplify_expr.h
invariant_sett::make_false
void make_false()
Definition: invariant_set.h:124
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
namespacet::get_symbol_table
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:126
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
invariant_sett
Definition: invariant_set.h:77
invariant_propagation.h
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
symbolt
Symbol table entry.
Definition: symbol.h:27
invariant_propagationt::value_sets
value_setst & value_sets
Definition: invariant_propagation.h:52
invariant_propagationt::object_store
inv_object_storet object_store
Definition: invariant_propagation.h:54
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
invariant_sett::simplify
void simplify(exprt &expr) const
Definition: invariant_set.cpp:821
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
invariant_sett::set_object_store
void set_object_store(inv_object_storet &_object_store)
Definition: invariant_set.h:153
symbol_table.h
Author: Diffblue Ltd.
ai_baset::initialize
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:202
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
goto_programt::decl_identifierst
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:680
std_expr.h
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
tvt::is_true
bool is_true() const
Definition: threeval.h:25
invariant_sett::make_true
void make_true()
Definition: invariant_set.h:116