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