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 <iosfwd>
21 #include <map>
22 #include <memory>
23 #include <stack>
24 #include <vector>
25 
28 #include <util/sharing_map.h>
29 #include <util/std_expr.h>
30 
33  std::shared_ptr<variable_sensitivity_object_factoryt>;
34 
36 {
37 public:
38  using map_keyt = irep_idt;
39 
41 
44  : bottom(true), object_factory(std::move(_object_factory))
45  {
46  }
47 
49 
57  eval(const exprt &expr, const namespacet &ns) const;
58 
86  virtual bool assign(
87  const exprt &expr,
88  const abstract_object_pointert &value,
89  const namespacet &ns);
90 
105  virtual bool assume(const exprt &expr, const namespacet &ns);
106 
128  const abstract_object_pointert &lhs,
129  const abstract_object_pointert &rhs,
130  std::stack<exprt> remaining_stack,
131  const namespacet &ns,
132  bool merge_write);
133 
138  void erase(const symbol_exprt &expr);
139 
151  const typet &type,
152  const namespacet &ns,
153  bool top,
154  bool bottom) const;
155 
169  const typet &type,
170  const exprt &e,
171  const namespacet &ns) const;
172 
184  add_object_context(const abstract_object_pointert &abstract_object) const;
185 
191  virtual bool merge(const abstract_environmentt &env);
192 
200  virtual void havoc(const std::string &havoc_string);
201 
203  void make_top();
204 
206  void make_bottom();
207 
209  bool is_bottom() const;
210 
212  bool is_top() const;
213 
219  void output(std::ostream &out, const class ai_baset &ai, const namespacet &ns)
220  const;
221 
224  bool verify() const;
225 
239  static std::vector<abstract_environmentt::map_keyt> modified_symbols(
240  const abstract_environmentt &first,
241  const abstract_environmentt &second);
242 
244 
245 protected:
246  bool bottom;
247 
248  // We may need to break out more of these cases into these
250  eval_expression(const exprt &e, const namespacet &ns) const;
251 
253  resolve_symbol(const exprt &e, const namespacet &ns) const;
254 
256 
257 private:
273  const typet &type,
274  bool top,
275  bool bottom,
276  const exprt &e,
277  const abstract_environmentt &environment,
278  const namespacet &ns) const;
279 
281 };
282 
283 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_ENVIROMENT_H
std::shared_ptr< variable_sensitivity_object_factoryt > variable_sensitivity_object_factory_ptrt
abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual vari...
sharing_ptrt< class abstract_objectt > abstract_object_pointert
Statistics gathering for the variable senstivity domain.
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.
virtual abstract_object_pointert add_object_context(const abstract_object_pointert &abstract_object) const
Wraps an existing object in any configured context object.
abstract_object_pointert resolve_symbol(const exprt &e, const namespacet &ns) const
abstract_environmentt(variable_sensitivity_object_factory_ptrt _object_factory)
virtual bool merge(const abstract_environmentt &env)
Computes the join between "this" and "b".
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...
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
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:120
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
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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:81
The type of an expression, extends irept.
Definition: type.h:28
dstringt irep_idt
Definition: irep.h:37
Sharing map.
API to expression classes.