cprover
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(const exprt &expr);
42 
43  irep_idt get_object_name() const;
44 
45  const ssa_exprt get_l1_object() const;
46 
47  const irep_idt get_l1_object_identifier() const;
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 
61  void remove_level_2();
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 
78  DEPRECATED(SINCE(2019, 05, 29, "Should only be used internally"))
79  void update_identifier();
80 
83  static bool can_build_identifier(const exprt &src);
84 
85  static void check(
86  const exprt &expr,
88  {
89  DATA_CHECK(
90  vm, !expr.has_operands(), "SSA expression should not have operands");
91  DATA_CHECK(
92  vm, expr.id() == ID_symbol, "SSA expression symbols are symbols");
93  DATA_CHECK(vm, expr.get_bool(ID_C_SSA_symbol), "wrong SSA expression ID");
94  // Check that each of the L0, L1 and L2 indices are either absent or are
95  // set to a non-empty value -- otherwise we could have two ssa_exprts that
96  // represent the same value (since get(ID_L0/1/2) will yield an empty string
97  // in both cases), but which do not compare equal (since irept::compare
98  // does not regard a missing key and an empty value as equivalent)
99  const auto &expr_sub = expr.get_named_sub();
100  const auto expr_l0 = expr_sub.find(ID_L0);
101  const auto expr_l1 = expr_sub.find(ID_L1);
102  const auto expr_l2 = expr_sub.find(ID_L2);
103  DATA_CHECK(
104  vm,
105  expr_l0 == expr_sub.end() || !expr_l0->second.id().empty(),
106  "L0 must not be an empty string");
107  DATA_CHECK(
108  vm,
109  expr_l1 == expr_sub.end() || !expr_l1->second.id().empty(),
110  "L1 must not be an empty string");
111  DATA_CHECK(
112  vm,
113  expr_l2 == expr_sub.end() || !expr_l2->second.id().empty(),
114  "L2 must not be an empty string");
115  }
116 
117  static void validate(
118  const exprt &expr,
119  const namespacet &ns,
121  {
122  check(expr, vm);
124  static_cast<const exprt &>(expr.find(ID_expression)), ns, vm);
125  }
126 };
127 
128 inline bool is_ssa_expr(const exprt &expr)
129 {
130  return expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol);
131 }
132 
133 template <>
134 inline bool can_cast_expr<ssa_exprt>(const exprt &base)
135 {
136  return is_ssa_expr(base);
137 }
138 
139 inline void validate_expr(const ssa_exprt &expr)
140 {
141  ssa_exprt::check(expr);
142 }
143 
148 inline const ssa_exprt &to_ssa_expr(const exprt &expr)
149 {
150  ssa_exprt::check(expr);
151  return static_cast<const ssa_exprt &>(expr);
152 }
153 
157 {
158  ssa_exprt::check(expr);
159  return static_cast<ssa_exprt &>(expr);
160 }
161 
164 
165 #endif // CPROVER_UTIL_SSA_EXPR_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
can_cast_expr< ssa_exprt >
bool can_cast_expr< ssa_exprt >(const exprt &base)
Definition: ssa_expr.h:134
ssa_exprt::set_level_0
void set_level_0(std::size_t i)
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
ssa_exprt::get_original_name
const irep_idt get_original_name() const
Definition: ssa_expr.h:49
validate_expr
void validate_expr(const ssa_exprt &expr)
Definition: ssa_expr.h:139
ssa_exprt::remove_level_2
void remove_level_2()
ssa_exprt::get_level_0
const irep_idt get_level_0() const
Definition: ssa_expr.h:63
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:113
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
exprt
Base class for all expressions.
Definition: expr.h:52
ssa_exprt::get_object_name
irep_idt get_object_name() const
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:33
ssa_exprt::set_level_1
void set_level_1(std::size_t i)
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:16
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:64
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:128
ssa_exprt::update_type
void update_type()
Definition: ssa_expr.h:28
ssa_exprt::can_build_identifier
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.
ssa_exprt::ssa_exprt
ssa_exprt(const exprt &expr)
Constructor.
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:148
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
ssa_exprt::get_l1_object
const ssa_exprt get_l1_object() const
ssa_exprt::get_level_2
const irep_idt get_level_2() const
Definition: ssa_expr.h:73
validation_modet
validation_modet
Definition: validation_mode.h:12
irept::id
const irep_idt & id() const
Definition: irep.h:418
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
ssa_exprt::get_l1_object_identifier
const irep_idt get_l1_object_identifier() const
ssa_exprt::set_level_2
void set_level_2(std::size_t i)
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
ssa_exprt::set_expression
void set_expression(const exprt &expr)
Replace the underlying, original expression by expr while maintaining SSA indices.
remove_level_2
ssa_exprt remove_level_2(ssa_exprt ssa)
ssa_exprt::update_identifier
void update_identifier()
ssa_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: ssa_expr.h:85
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
ssa_exprt::get_level_1
const irep_idt get_level_1() const
Definition: ssa_expr.h:68
validate_full_expr
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...
Definition: validate_expressions.cpp:96
std_expr.h
validation_modet::INVARIANT
ssa_exprt::validate
static void validate(const exprt &expr, const namespacet &ns, const validation_modet vm=validation_modet::INVARIANT)
Definition: ssa_expr.h:117