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/symbol_table.h>
16 #include <util/std_expr.h>
17 
20  : public ai_domain_factoryt<invariant_set_domaint>
21 {
22 public:
24  {
25  }
26 
27  std::unique_ptr<statet> make(locationt l) const override
28  {
29  auto p = util_make_unique<invariant_set_domaint>(
31  CHECK_RETURN(p->is_bottom());
32 
33  return std::unique_ptr<statet>(p.release());
34  }
35 
36 private:
38 };
39 
41  const namespacet &_ns,
42  value_setst &_value_sets)
45  ns(_ns),
46  value_sets(_value_sets),
47  object_store(_ns)
48 {
49 }
50 
52 {
53  for(auto &state :
54  static_cast<location_sensitive_storaget &>(*storage).internal())
55  static_cast<invariant_set_domaint &>(*(state.second))
57 }
58 
60 {
61  for(auto &state :
62  static_cast<location_sensitive_storaget &>(*storage).internal())
63  static_cast<invariant_set_domaint &>(*(state.second))
65 }
66 
68  const goto_programt &goto_program)
69 {
70  // get the globals
71  object_listt globals;
72  get_globals(globals);
73 
74  // get the locals
76  goto_program.get_decl_identifiers(locals);
77 
78  // cache the list for the locals to speed things up
79  typedef std::unordered_map<irep_idt, object_listt> object_cachet;
80  object_cachet object_cache;
81 
82  forall_goto_program_instructions(i_it, goto_program)
83  {
84  #if 0
85  invariant_sett &is=(*this)[i_it].invariant_set;
86 
87  is.add_objects(globals);
88  #endif
89 
90  for(const auto &local : locals)
91  {
92  // cache hit?
93  object_cachet::const_iterator e_it=object_cache.find(local);
94 
95  if(e_it==object_cache.end())
96  {
97  const symbolt &symbol=ns.lookup(local);
98 
99  object_listt &objects=object_cache[local];
100  get_objects(symbol, objects);
101  #if 0
102  is.add_objects(objects);
103  #endif
104  }
105  #if 0
106  else
107  is.add_objects(e_it->second);
108  #endif
109  }
110  }
111 }
112 
114  const symbolt &symbol,
115  object_listt &dest)
116 {
117  std::list<exprt> object_list;
118 
119  get_objects_rec(symbol.symbol_expr(), object_list);
120 
121  for(const auto &expr : object_list)
122  dest.push_back(object_store.add(expr));
123 }
124 
126  const exprt &src,
127  std::list<exprt> &dest)
128 {
129  const typet &t = src.type();
130 
131  if(
132  t.id() == ID_struct || t.id() == ID_union || t.id() == ID_struct_tag ||
133  t.id() == ID_union_tag)
134  {
135  const struct_union_typet &struct_type = to_struct_union_type(ns.follow(t));
136 
137  for(const auto &component : struct_type.components())
138  {
139  const member_exprt member_expr(
140  src, component.get_name(), component.type());
141  // recursive call
142  get_objects_rec(member_expr, dest);
143  }
144  }
145  else if(t.id()==ID_array)
146  {
147  // get_objects_rec(identifier, suffix+"[]", t.subtype(), dest);
148  // we don't track these
149  }
150  else if(check_type(t))
151  {
152  dest.push_back(src);
153  }
154 }
155 
157  const goto_functionst &goto_functions)
158 {
159  // get the globals
160  object_listt globals;
161  get_globals(globals);
162 
163  forall_goto_functions(f_it, goto_functions)
164  {
165  // get the locals
166  std::set<irep_idt> locals;
167  get_local_identifiers(f_it->second, locals);
168 
169  const goto_programt &goto_program=f_it->second.body;
170 
171  // cache the list for the locals to speed things up
172  typedef std::unordered_map<irep_idt, object_listt> object_cachet;
173  object_cachet object_cache;
174 
175  forall_goto_program_instructions(i_it, goto_program)
176  {
177  #if 0
178  invariant_sett &is=(*this)[i_it].invariant_set;
179 
180  is.add_objects(globals);
181  #endif
182 
183  for(const auto &local : locals)
184  {
185  // cache hit?
186  object_cachet::const_iterator e_it=object_cache.find(local);
187 
188  if(e_it==object_cache.end())
189  {
190  const symbolt &symbol=ns.lookup(local);
191 
192  object_listt &objects=object_cache[local];
193  get_objects(symbol, objects);
194  #if 0
195  is.add_objects(objects);
196  #endif
197  }
198  #if 0
199  else
200  is.add_objects(e_it->second);
201  #endif
202  }
203  }
204  }
205 }
206 
208  object_listt &dest)
209 {
210  // static ones
211  for(const auto &symbol_pair : ns.get_symbol_table().symbols)
212  {
213  if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
214  {
215  get_objects(symbol_pair.second, dest);
216  }
217  }
218 }
219 
221 {
222  if(type.id()==ID_pointer)
223  return true;
224  else if(
225  type.id() == ID_struct || type.id() == ID_union ||
226  type.id() == ID_struct_tag || type.id() == ID_union_tag)
227  return false;
228  else if(type.id()==ID_array)
229  return false;
230  else if(type.id()==ID_unsignedbv ||
231  type.id()==ID_signedbv)
232  return true;
233  else if(type.id()==ID_bool)
234  return true;
235 
236  return false;
237 }
238 
240  const irep_idt &function,
241  const goto_programt &goto_program)
242 {
243  baset::initialize(function, goto_program);
244 
245  add_objects(goto_program);
246 }
247 
249 {
250  Forall_goto_functions(it, goto_functions)
251  simplify(it->second.body);
252 }
253 
255 {
256  Forall_goto_program_instructions(i_it, goto_program)
257  {
258  if(!i_it->is_assert())
259  continue;
260 
261  // find invariant set
262  const auto &d = (*this)[i_it];
263  if(d.is_bottom())
264  continue;
265 
266  const invariant_sett &invariant_set = d.invariant_set;
267 
268  exprt simplified_guard(i_it->get_condition());
269 
270  invariant_set.simplify(simplified_guard);
271  ::simplify(simplified_guard, ns);
272 
273  if(invariant_set.implies(simplified_guard).is_true())
274  i_it->set_condition(true_exprt());
275  }
276 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
invariant_set_domaint
Definition: invariant_set_domain.h:21
invariant_sett::implies
tvt implies(const exprt &expr) const
Definition: invariant_set.cpp:580
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
invariant_propagationt::object_listt
std::list< unsigned > object_listt
Definition: invariant_propagation.h:58
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
struct_union_typet
Base type for structs and unions.
Definition: std_types.h:57
invariant_set_domain_factoryt
Pass the necessary arguments to the invariant_set_domaint's when constructed.
Definition: invariant_propagation.cpp:21
location_sensitive_storaget::internal
state_mapt & internal(void)
Definition: ai_storage.h:164
invariant_propagationt::ns
const namespacet & ns
Definition: invariant_propagation.h:53
invariant_set_domain_factoryt::make
std::unique_ptr< statet > make(locationt l) const override
Definition: invariant_propagation.cpp:27
exprt
Base class for all expressions.
Definition: expr.h:53
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:558
goto_programt::get_decl_identifiers
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
Definition: goto_program.cpp:229
component
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
Definition: std_expr.cpp:192
invariant_propagationt::make_all_true
void make_all_true()
Definition: invariant_propagation.cpp:51
invariant_propagationt::get_objects
void get_objects(const symbolt &symbol, object_listt &dest)
Definition: invariant_propagation.cpp:113
invariant_propagationt::make_all_false
void make_all_false()
Definition: invariant_propagation.cpp:59
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
inv_object_storet::add
unsigned add(const exprt &expr)
Definition: invariant_set.cpp:64
invariant_propagationt::get_objects_rec
void get_objects_rec(const exprt &src, std::list< exprt > &dest)
Definition: invariant_propagation.cpp:125
invariant_propagationt::add_objects
void add_objects(const goto_programt &goto_program)
Definition: invariant_propagation.cpp:67
invariant_propagationt::check_type
bool check_type(const typet &type) const
Definition: invariant_propagation.cpp:220
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
invariant_propagationt::invariant_propagationt
invariant_propagationt(const namespacet &_ns, value_setst &_value_sets)
Definition: invariant_propagation.cpp:40
invariant_propagationt::get_globals
void get_globals(object_listt &globals)
Definition: invariant_propagation.cpp:207
invariant_propagationt::simplify
void simplify(goto_programt &goto_program)
Definition: invariant_propagation.cpp:254
irept::id
const irep_idt & id() const
Definition: irep.h:418
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
invariant_set_domain_factoryt::invariant_set_domain_factoryt
invariant_set_domain_factoryt(invariant_propagationt &_ip)
Definition: invariant_propagation.cpp:23
location_sensitive_storaget
The most conventional storage; one domain per location.
Definition: ai_storage.h:150
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
invariant_set_domain_factoryt::ip
invariant_propagationt & ip
Definition: invariant_propagation.cpp:37
simplify_expr.h
invariant_sett::make_false
void make_false()
Definition: invariant_set.h:122
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
ai_baset::initialize
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:190
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
ai_domain_factoryt
Definition: ai_domain.h:218
invariant_set_domaint::invariant_set
invariant_sett invariant_set
Definition: invariant_set_domain.h:32
value_setst
Definition: value_sets.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:124
invariant_sett
Definition: invariant_set.h:75
invariant_propagation.h
Invariant Propagation.
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
symbolt
Symbol table entry.
Definition: symbol.h:28
invariant_propagationt::value_sets
value_setst & value_sets
Definition: invariant_propagation.h:54
invariant_propagationt::object_store
inv_object_storet object_store
Definition: invariant_propagation.h:56
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
invariant_sett::simplify
void simplify(exprt &expr) const
Definition: invariant_set.cpp:809
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
ai_domain_factory_baset::locationt
ai_domain_baset::locationt locationt
Definition: ai_domain.h:192
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:122
invariant_propagationt
Definition: invariant_propagation.h:24
symbol_table.h
Author: Diffblue Ltd.
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
goto_programt::decl_identifierst
std::set< irep_idt > decl_identifierst
Definition: goto_program.h:816
invariant_propagationt::initialize
void initialize(const irep_idt &function, const goto_programt &goto_program) override
Initialize all the abstract states for a single function.
Definition: invariant_propagation.cpp:239
std_expr.h
API to expression classes.
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
tvt::is_true
bool is_true() const
Definition: threeval.h:25
invariant_sett::make_true
void make_true()
Definition: invariant_set.h:114