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, irep_id_hash>
44  object_cachet;
45  object_cachet object_cache;
46 
47  forall_goto_program_instructions(i_it, goto_program)
48  {
49  #if 0
50  invariant_sett &is=(*this)[i_it].invariant_set;
51 
52  is.add_objects(globals);
53  #endif
54 
55  for(const auto &local : locals)
56  {
57  // cache hit?
58  object_cachet::const_iterator e_it=object_cache.find(local);
59 
60  if(e_it==object_cache.end())
61  {
62  const symbolt &symbol=ns.lookup(local);
63 
64  object_listt &objects=object_cache[local];
65  get_objects(symbol, objects);
66  #if 0
67  is.add_objects(objects);
68  #endif
69  }
70  #if 0
71  else
72  is.add_objects(e_it->second);
73  #endif
74  }
75  }
76 }
77 
79  const symbolt &symbol,
80  object_listt &dest)
81 {
82  std::list<exprt> object_list;
83 
84  get_objects_rec(symbol.symbol_expr(), object_list);
85 
86  for(const auto &expr : object_list)
87  dest.push_back(object_store.add(expr));
88 }
89 
91  const exprt &src,
92  std::list<exprt> &dest)
93 {
94  const typet &t=ns.follow(src.type());
95 
96  if(t.id()==ID_struct ||
97  t.id()==ID_union)
98  {
99  const struct_typet &struct_type=to_struct_type(t);
100 
101  const struct_typet::componentst &c=struct_type.components();
102 
103  exprt member_expr(ID_member);
104  member_expr.copy_to_operands(src);
105 
106  for(const auto &component : c)
107  {
108  member_expr.set(ID_component_name, component.get_name());
109  member_expr.type()=component.type();
110  // recursive call
111  get_objects_rec(member_expr, dest);
112  }
113  }
114  else if(t.id()==ID_array)
115  {
116  // get_objects_rec(identifier, suffix+"[]", t.subtype(), dest);
117  // we don't track these
118  }
119  else if(check_type(t))
120  {
121  dest.push_back(src);
122  }
123 }
124 
126  const goto_functionst &goto_functions)
127 {
128  // get the globals
129  object_listt globals;
130  get_globals(globals);
131 
132  forall_goto_functions(f_it, goto_functions)
133  {
134  // get the locals
135  std::set<irep_idt> locals;
136  get_local_identifiers(f_it->second, locals);
137 
138  const goto_programt &goto_program=f_it->second.body;
139 
140  // cache the list for the locals to speed things up
141  typedef std::unordered_map<irep_idt, object_listt, irep_id_hash>
142  object_cachet;
143  object_cachet object_cache;
144 
145  forall_goto_program_instructions(i_it, goto_program)
146  {
147  #if 0
148  invariant_sett &is=(*this)[i_it].invariant_set;
149 
150  is.add_objects(globals);
151  #endif
152 
153  for(const auto &local : locals)
154  {
155  // cache hit?
156  object_cachet::const_iterator e_it=object_cache.find(local);
157 
158  if(e_it==object_cache.end())
159  {
160  const symbolt &symbol=ns.lookup(local);
161 
162  object_listt &objects=object_cache[local];
163  get_objects(symbol, objects);
164  #if 0
165  is.add_objects(objects);
166  #endif
167  }
168  #if 0
169  else
170  is.add_objects(e_it->second);
171  #endif
172  }
173  }
174  }
175 }
176 
178  object_listt &dest)
179 {
180  // static ones
182  if(it->second.is_lvalue &&
183  it->second.is_static_lifetime)
184  get_objects(it->second, dest);
185 }
186 
188 {
189  if(type.id()==ID_pointer)
190  return true;
191  else if(type.id()==ID_struct ||
192  type.id()==ID_union)
193  return false;
194  else if(type.id()==ID_array)
195  return false;
196  else if(type.id()==ID_symbol)
197  return check_type(ns.follow(type));
198  else if(type.id()==ID_unsignedbv ||
199  type.id()==ID_signedbv)
200  return true;
201  else if(type.id()==ID_bool)
202  return true;
203 
204  return false;
205 }
206 
208 {
209  baset::initialize(goto_program);
210 
211  forall_goto_program_instructions(it, goto_program)
212  {
213  invariant_sett &s=state_map[it].invariant_set;
214 
215  if(it==goto_program.instructions.begin())
216  s.make_true();
217  else
218  s.make_false();
219 
222  s.set_namespace(ns);
223  }
224 
225  add_objects(goto_program);
226 }
227 
229 {
230  baset::initialize(goto_functions);
231 
232  forall_goto_functions(f_it, goto_functions)
233  initialize(f_it->second.body);
234 }
235 
237 {
238  Forall_goto_functions(it, goto_functions)
239  simplify(it->second.body);
240 }
241 
243 {
244  Forall_goto_program_instructions(i_it, goto_program)
245  {
246  if(!i_it->is_assert())
247  continue;
248 
249  // find invariant set
250  state_mapt::const_iterator s_it=state_map.find(i_it);
251  if(s_it==state_map.end())
252  continue;
253 
254  const invariant_sett &invariant_set=s_it->second.invariant_set;
255 
256  exprt simplified_guard(i_it->guard);
257 
258  invariant_set.simplify(simplified_guard);
259  ::simplify(simplified_guard, ns);
260 
261  if(invariant_set.implies(simplified_guard).is_true())
262  i_it->guard=true_exprt();
263  }
264 }
The type of an expression.
Definition: type.h:20
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
std::list< unsigned > object_listt
#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 copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
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
void get_objects(const symbolt &symbol, object_listt &dest)
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
Structure type.
Definition: std_types.h:296
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
bool check_type(const typet &type) const
tvt implies(const exprt &expr) const
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:64
const irep_idt & id() const
Definition: irep.h:189
Invariant Propagation.
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
virtual void initialize(const goto_programt &goto_program)
The boolean constant true.
Definition: std_expr.h:3742
symbolst symbols
Definition: symbol_table.h:57
void add_objects(const goto_programt &goto_program)
void set_value_sets(value_setst &_value_sets)
API to expression classes.
void get_globals(object_listt &globals)
unsigned add(const exprt &expr)
Symbol table.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
bool is_true() const
Definition: threeval.h:25
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
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:46
#define Forall_goto_functions(it, functions)
virtual void initialize(const goto_programt &)
Definition: ai.cpp:269
state_mapt state_map
Definition: ai.h:378
inv_object_storet object_store
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Base Type Computation.
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
void set_namespace(const namespacet &_ns)