cprover
ai_domain.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Abstract Interpretation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "ai_domain.h"
13 
14 #include <util/simplify_expr.h>
15 
17  const
18 {
19  std::ostringstream out;
20  output(out, ai, ns);
21  json_stringt json(out.str());
22  return std::move(json);
23 }
24 
26 {
27  std::ostringstream out;
28  output(out, ai, ns);
29  xmlt xml("abstract_state");
30  xml.data = out.str();
31  return xml;
32 }
33 
43  const
44 {
45  // Care must be taken here to give something that is still writable
46  if(condition.id() == ID_index)
47  {
48  index_exprt ie = to_index_expr(condition);
49  bool no_simplification = ai_simplify(ie.index(), ns);
50  if(!no_simplification)
51  condition = simplify_expr(std::move(ie), ns);
52 
53  return no_simplification;
54  }
55  else if(condition.id() == ID_dereference)
56  {
57  dereference_exprt de = to_dereference_expr(condition);
58  bool no_simplification = ai_simplify(de.pointer(), ns);
59  if(!no_simplification)
60  condition = simplify_expr(std::move(de), ns); // So *(&x) -> x
61 
62  return no_simplification;
63  }
64  else if(condition.id() == ID_member)
65  {
66  member_exprt me = to_member_expr(condition);
67  // Since simplify_ai_lhs is required to return an addressable object
68  // (so remains a valid left hand side), to simplify
69  // `(something_simplifiable).b` we require that `something_simplifiable`
70  // must also be addressable
71  bool no_simplification = ai_simplify_lhs(me.compound(), ns);
72  if(!no_simplification)
73  condition = simplify_expr(std::move(me), ns);
74 
75  return no_simplification;
76  }
77  else
78  return true;
79 }
ai_domain.h
Abstract Interpretation Domain.
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
dereference_exprt
Operator to dereference a pointer.
Definition: std_expr.h:2888
exprt
Base class for all expressions.
Definition: expr.h:53
ai_domain_baset::output_json
virtual jsont output_json(const ai_baset &ai, const namespacet &ns) const
Definition: ai_domain.cpp:16
jsont
Definition: json.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
member_exprt::compound
const exprt & compound() const
Definition: std_expr.h:3446
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:2901
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
ai_domain_baset::ai_simplify_lhs
virtual bool ai_simplify_lhs(exprt &condition, const namespacet &ns) const
Simplifies the expression but keeps it as an l-value.
Definition: ai_domain.cpp:42
irept::id
const irep_idt & id() const
Definition: irep.h:418
ai_domain_baset::output_xml
virtual xmlt output_xml(const ai_baset &ai, const namespacet &ns) const
Definition: ai_domain.cpp:25
xmlt
Definition: xml.h:21
simplify_expr.h
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3405
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3489
index_exprt
Array index operator.
Definition: std_expr.h:1293
ai_domain_baset::ai_simplify
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
Definition: ai_domain.h:167
xmlt::data
std::string data
Definition: xml.h:39
ai_domain_baset::output
virtual void output(std::ostream &, const ai_baset &, const namespacet &) const
Definition: ai_domain.h:126
json_stringt
Definition: json.h:270