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 }
The type of an expression, extends irept.
Definition: type.h:27
std::list< unsigned > object_listt
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...
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:173
void get_objects(const symbolt &symbol, object_listt &dest)
const componentst & components() const
Definition: std_types.h:205
typet & type()
Return the type of the expression.
Definition: expr.h:68
Symbol table entry.
Definition: symbol.h:27
Structure type, corresponds to C style structs.
Definition: std_types.h:276
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
Extract member of struct or union.
Definition: std_expr.h:3890
bool check_type(const typet &type) const
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:202
tvt implies(const exprt &expr) const
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:680
const irep_idt & id() const
Definition: irep.h:259
Invariant Propagation.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
The Boolean constant true.
Definition: std_expr.h:4443
void add_objects(const goto_programt &goto_program)
void set_value_sets(value_setst &_value_sets)
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
Definition: namespace.h:126
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
API to expression classes.
void get_globals(object_listt &globals)
unsigned add(const exprt &expr)
A collection of goto functions.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
Author: Diffblue Ltd.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
const symbolst & symbols
bool is_true() const
Definition: threeval.h:25
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
void simplify(exprt &expr) const
void set_object_store(inv_object_storet &_object_store)
void simplify(goto_programt &goto_program)
Base class for all expressions.
Definition: expr.h:54
#define Forall_goto_functions(it, functions)
state_mapt state_map
Definition: ai.h:416
inv_object_storet object_store
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
Base Type Computation.
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
void set_namespace(const namespacet &_ns)