cprover
abstract_environment.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Thomas Kiley, thomas.kiley@diffblue.com
6
7\*******************************************************************/
8
16
17#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H
18#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H
19
20#include <memory>
21
23
25bool is_ptr_diff(const exprt &expr);
26bool is_ptr_comparison(const exprt &expr);
27
30 std::shared_ptr<variable_sensitivity_object_factoryt>;
31
32enum class widen_modet
33{
34 no,
36};
37
38struct vsd_configt;
39
41{
42public:
44
46
49 : bottom(true), object_factory(std::move(_object_factory))
50 {
51 }
52
54
62 eval(const exprt &expr, const namespacet &ns) const;
63
91 virtual bool assign(
92 const exprt &expr,
93 const abstract_object_pointert &value,
94 const namespacet &ns);
95
110 virtual bool assume(const exprt &expr, const namespacet &ns);
111 exprt do_assume(const exprt &e, const namespacet &ns);
112
134 const abstract_object_pointert &lhs,
135 const abstract_object_pointert &rhs,
136 std::stack<exprt> remaining_stack,
137 const namespacet &ns,
138 bool merge_write);
139
144 void erase(const symbol_exprt &expr);
145
157 const typet &type,
158 const namespacet &ns,
159 bool top,
160 bool bottom) const;
161
175 const typet &type,
176 const exprt &e,
177 const namespacet &ns) const;
178
180 const vsd_configt &configuration() const;
181
189 virtual bool merge(
190 const abstract_environmentt &env,
191 const goto_programt::const_targett &merge_location,
192 widen_modet widen_mode);
193
201 virtual void havoc(const std::string &havoc_string);
202
204 void make_top();
205
207 void make_bottom();
208
210 bool is_bottom() const;
211
213 bool is_top() const;
214
220 void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
221 const;
222
227 exprt to_predicate() const;
228
231 bool verify() const;
232
246 static std::vector<abstract_environmentt::map_keyt> modified_symbols(
247 const abstract_environmentt &first,
248 const abstract_environmentt &second);
249
251
252protected:
253 bool bottom;
254
255 // We may need to break out more of these cases into these
257 eval_expression(const exprt &e, const namespacet &ns) const;
258
260 resolve_symbol(const exprt &e, const namespacet &ns) const;
261
263
264private:
280 const typet &type,
281 bool top,
282 bool bottom,
283 const exprt &e,
284 const abstract_environmentt &environment,
285 const namespacet &ns) const;
286
288};
289
290#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H
exprt simplify_vsd_expr(exprt src, const namespacet &ns)
bool is_ptr_comparison(const exprt &expr)
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
bool is_ptr_diff(const exprt &expr)
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
sharing_ptrt< class abstract_objectt > abstract_object_pointert
virtual bool assume(const exprt &expr, const namespacet &ns)
Reduces the domain based on a condition.
void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
Print out all the values in the abstract object map.
bool is_bottom() const
Gets whether the domain is bottom.
abstract_object_pointert resolve_symbol(const exprt &e, const namespacet &ns) const
exprt to_predicate() const
Gives a boolean condition that is true for all values represented by the environment.
abstract_environmentt(variable_sensitivity_object_factory_ptrt _object_factory)
void make_top()
Set the domain to top (i.e. everything)
virtual abstract_object_pointert eval(const exprt &expr, const namespacet &ns) const
These three are really the heart of the method.
void erase(const symbol_exprt &expr)
Delete a symbol from the map.
static std::vector< abstract_environmentt::map_keyt > modified_symbols(const abstract_environmentt &first, const abstract_environmentt &second)
For our implementation of variable sensitivity domains, we need to be able to efficiently find symbol...
bool verify() const
Check the structural invariants are maintained.
virtual void havoc(const std::string &havoc_string)
This should be used as a default case / everything else has failed The string is so that I can easily...
exprt do_assume(const exprt &e, const namespacet &ns)
const vsd_configt & configuration() const
Exposes the environment configuration.
variable_sensitivity_object_factory_ptrt object_factory
virtual abstract_object_pointert write(const abstract_object_pointert &lhs, const abstract_object_pointert &rhs, std::stack< exprt > remaining_stack, const namespacet &ns, bool merge_write)
Used within assign to do the actual dispatch.
abstract_object_statisticst gather_statistics(const namespacet &ns) const
virtual bool merge(const abstract_environmentt &env, const goto_programt::const_targett &merge_location, widen_modet widen_mode)
Computes the join between "this" and "b".
void make_bottom()
Set the domain to top (i.e. no possible states / unreachable)
bool is_top() const
Gets whether the domain is top.
virtual abstract_object_pointert abstract_object_factory(const typet &type, const namespacet &ns, bool top, bool bottom) const
Look at the configuration for the sensitivity and create an appropriate abstract_object.
virtual abstract_object_pointert eval_expression(const exprt &e, const namespacet &ns) const
abstract_environmentt()=delete
virtual bool assign(const exprt &expr, const abstract_object_pointert &value, const namespacet &ns)
Assign a value to an expression.
sharing_mapt< map_keyt, abstract_object_pointert > map
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
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
instructionst::const_iterator const_targett
Definition: goto_program.h:593
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
A map implemented as a tree where subtrees can be shared between different maps.
Definition: sharing_map.h:190
Expression to hold a symbol (variable)
Definition: std_expr.h:80
The type of an expression, extends irept.
Definition: type.h:29
dstringt irep_idt
Definition: irep.h:37
STL namespace.