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 
33 {
34  // get the globals
35  object_listt globals;
36  get_globals(globals);
37 
38  // get the 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 
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 
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)
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 {
206 
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 
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 {
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.
Definition: type.h:22
std::list< unsigned > object_listt
const symbol_tablet & get_symbol_table() const
Definition: namespace.h:106
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
void get_objects(const symbolt &symbol, object_listt &dest)
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
Structure type.
Definition: std_types.h:297
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
Extract member of struct or union.
Definition: std_expr.h:3869
bool check_type(const typet &type) const
tvt implies(const exprt &expr) const
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:640
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:111
virtual void initialize(const goto_programt &goto_program)
The boolean constant true.
Definition: std_expr.h:4486
void add_objects(const goto_programt &goto_program)
void set_value_sets(value_setst &_value_sets)
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
API to expression classes.
void get_globals(object_listt &globals)
unsigned add(const exprt &expr)
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
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:70
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:42
#define Forall_goto_functions(it, functions)
virtual void initialize(const goto_programt &)
Definition: ai.cpp:202
state_mapt state_map
Definition: ai.h:345
goto_programt & goto_program
Definition: cover.cpp:63
inv_object_storet object_store
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Base Type Computation.
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:136
void set_namespace(const namespacet &_ns)