CBMC
ssa_expr.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_UTIL_SSA_EXPR_H
11 #define CPROVER_UTIL_SSA_EXPR_H
12 
13 #include "std_expr.h"
14 
16 class ssa_exprt:public symbol_exprt
17 {
18 public:
26  explicit ssa_exprt(const exprt &expr);
27 
28  void update_type()
29  {
30  static_cast<exprt &>(add(ID_expression)).type()=type();
31  }
32 
33  const exprt &get_original_expr() const
34  {
35  return static_cast<const exprt &>(find(ID_expression));
36  }
37 
41  void set_expression(exprt expr);
42 
44 
45  const ssa_exprt get_l1_object() const;
46 
48 
50  {
52  return o.get_identifier();
53  }
54 
55  void set_level_0(std::size_t i);
56 
57  void set_level_1(std::size_t i);
58 
59  void set_level_2(std::size_t i);
60 
62 
63  const irep_idt get_level_0() const
64  {
65  return get(ID_L0);
66  }
67 
68  const irep_idt get_level_1() const
69  {
70  return get(ID_L1);
71  }
72 
73  const irep_idt get_level_2() const
74  {
75  return get(ID_L2);
76  }
77 
80  static bool can_build_identifier(const exprt &src);
81 
82  static void check(
83  const exprt &expr,
85  {
86  DATA_CHECK(
87  vm, !expr.has_operands(), "SSA expression should not have operands");
88  DATA_CHECK(
89  vm, expr.id() == ID_symbol, "SSA expression symbols are symbols");
90  DATA_CHECK(vm, expr.get_bool(ID_C_SSA_symbol), "wrong SSA expression ID");
91  // Check that each of the L0, L1 and L2 indices are either absent or are
92  // set to a non-empty value -- otherwise we could have two ssa_exprts that
93  // represent the same value (since get(ID_L0/1/2) will yield an empty string
94  // in both cases), but which do not compare equal (since irept::compare
95  // does not regard a missing key and an empty value as equivalent)
96  const auto &expr_sub = expr.get_named_sub();
97  const auto expr_l0 = expr_sub.find(ID_L0);
98  const auto expr_l1 = expr_sub.find(ID_L1);
99  const auto expr_l2 = expr_sub.find(ID_L2);
100  DATA_CHECK(
101  vm,
102  expr_l0 == expr_sub.end() || !expr_l0->second.id().empty(),
103  "L0 must not be an empty string");
104  DATA_CHECK(
105  vm,
106  expr_l1 == expr_sub.end() || !expr_l1->second.id().empty(),
107  "L1 must not be an empty string");
108  DATA_CHECK(
109  vm,
110  expr_l2 == expr_sub.end() || !expr_l2->second.id().empty(),
111  "L2 must not be an empty string");
112  }
113 
114  static void validate(
115  const exprt &expr,
116  const namespacet &ns,
118  {
119  check(expr, vm);
121  static_cast<const exprt &>(expr.find(ID_expression)), ns, vm);
122  }
123 };
124 
125 inline bool is_ssa_expr(const exprt &expr)
126 {
127  return expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol);
128 }
129 
130 template <>
131 inline bool can_cast_expr<ssa_exprt>(const exprt &base)
132 {
133  return is_ssa_expr(base);
134 }
135 
136 inline void validate_expr(const ssa_exprt &expr)
137 {
138  ssa_exprt::check(expr);
139 }
140 
145 inline const ssa_exprt &to_ssa_expr(const exprt &expr)
146 {
147  ssa_exprt::check(expr);
148  return static_cast<const ssa_exprt &>(expr);
149 }
150 
154 {
155  ssa_exprt::check(expr);
156  return static_cast<ssa_exprt &>(expr);
157 }
158 
161 
162 #endif // CPROVER_UTIL_SSA_EXPR_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:91
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool get_bool(const irep_idt &name) const
Definition: irep.cpp:57
const irept & find(const irep_idt &name) const
Definition: irep.cpp:93
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
named_subt & get_named_sub()
Definition: irep.h:446
const irep_idt & id() const
Definition: irep.h:384
irept & add(const irep_idt &name)
Definition: irep.cpp:103
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
const irep_idt get_level_1() const
Definition: ssa_expr.h:68
const irep_idt get_l1_object_identifier() const
void set_level_1(std::size_t i)
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: ssa_expr.h:114
void set_level_2(std::size_t i)
void remove_level_2()
const ssa_exprt get_l1_object() const
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: ssa_expr.h:82
void update_type()
Definition: ssa_expr.h:28
static bool can_build_identifier(const exprt &src)
Used to determine whether or not an identifier can be built before trying and getting an exception.
void set_expression(exprt expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
const irep_idt get_level_2() const
Definition: ssa_expr.h:73
const irep_idt get_level_0() const
Definition: ssa_expr.h:63
const irep_idt get_original_name() const
Definition: ssa_expr.h:49
void set_level_0(std::size_t i)
ssa_exprt(const exprt &expr)
Constructor.
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
irep_idt get_object_name() const
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:145
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:125
void validate_expr(const ssa_exprt &expr)
Definition: ssa_expr.h:136
bool can_cast_expr< ssa_exprt >(const exprt &base)
Definition: ssa_expr.h:131
ssa_exprt remove_level_2(ssa_exprt ssa)
API to expression classes.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
validation_modet