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 
17 class ssa_exprt:public symbol_exprt
18 {
19 public:
21  {
22  set(ID_C_SSA_symbol, true);
23  }
24 
28  explicit ssa_exprt(const exprt &expr):
29  symbol_exprt(expr.type())
30  {
31  set(ID_C_SSA_symbol, true);
32  add(ID_expression, expr);
34  }
35 
36  void update_type()
37  {
38  static_cast<exprt &>(add(ID_expression)).type()=type();
39  }
40 
41  const exprt &get_original_expr() const
42  {
43  return static_cast<const exprt &>(find(ID_expression));
44  }
45 
47  {
49  ode.object()=get_original_expr();
51  }
52 
53  const ssa_exprt get_l1_object() const
54  {
56  ode.object()=get_original_expr();
57 
58  ssa_exprt root(ode.root_object());
59  root.set(ID_L0, get(ID_L0));
60  root.set(ID_L1, get(ID_L1));
61  root.update_identifier();
62 
63  return root;
64  }
65 
67  {
68  #if 0
69  return get_l1_object().get_identifier();
70  #else
71  // the above is the clean version, this is the fast one, using
72  // an identifier cached during build_identifier
73  return get(ID_L1_object_identifier);
74  #endif
75  }
76 
78  {
80  return o.get_identifier();
81  }
82 
83  void set_level_0(unsigned i)
84  {
85  set(ID_L0, i);
87  }
88 
89  void set_level_1(unsigned i)
90  {
91  set(ID_L1, i);
93  }
94 
95  void set_level_2(unsigned i)
96  {
97  set(ID_L2, i);
99  }
100 
102  {
103  remove(ID_L2);
105  }
106 
107  const irep_idt get_level_0() const
108  {
109  return get(ID_L0);
110  }
111 
112  const irep_idt get_level_1() const
113  {
114  return get(ID_L1);
115  }
116 
117  const irep_idt get_level_2() const
118  {
119  return get(ID_L2);
120  }
121 
122  void update_identifier();
123 
124  /* Used to determine whether or not an identifier can be built
125  * before trying and getting an exception */
126  static bool can_build_identifier(const exprt &src);
127 
128  static void check(
129  const exprt &expr,
131  {
132  DATA_CHECK(
133  vm, !expr.has_operands(), "SSA expression should not have operands");
134  DATA_CHECK(
135  vm, expr.id() == ID_symbol, "SSA expression symbols are symbols");
136  DATA_CHECK(vm, expr.get_bool(ID_C_SSA_symbol), "wrong SSA expression ID");
137  }
138 
139  static void validate(
140  const exprt &expr,
141  const namespacet &ns,
143  {
144  check(expr, vm);
146  static_cast<const exprt &>(expr.find(ID_expression)), ns, vm);
147  }
148 };
149 
160 inline const ssa_exprt &to_ssa_expr(const exprt &expr)
161 {
162  PRECONDITION(
163  expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol) &&
164  !expr.has_operands());
165  return static_cast<const ssa_exprt &>(expr);
166 }
167 
172 {
173  PRECONDITION(
174  expr.id() == ID_symbol && expr.get_bool(ID_C_SSA_symbol) &&
175  !expr.has_operands());
176  return static_cast<ssa_exprt &>(expr);
177 }
178 
179 inline bool is_ssa_expr(const exprt &expr)
180 {
181  return expr.id()==ID_symbol &&
182  expr.get_bool(ID_C_SSA_symbol);
183 }
184 
185 #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:35
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
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:77
ssa_exprt::remove_level_2
void remove_level_2()
Definition: ssa_expr.h:101
ssa_exprt::get_level_0
const irep_idt get_level_0() const
Definition: ssa_expr.h:107
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:305
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:2136
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:284
exprt
Base class for all expressions.
Definition: expr.h:54
ssa_exprt::get_object_name
irep_idt get_object_name() const
Definition: ssa_expr.h:46
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
ssa_exprt::get_original_expr
const exprt & get_original_expr() const
Definition: ssa_expr.h:41
ssa_exprt
Expression providing an SSA-renamed symbol of expressions.
Definition: ssa_expr.h:17
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
is_ssa_expr
bool is_ssa_expr(const exprt &expr)
Definition: ssa_expr.h:179
ssa_exprt::update_type
void update_type()
Definition: ssa_expr.h:36
ssa_exprt::ssa_exprt
ssa_exprt(const exprt &expr)
Constructor.
Definition: ssa_expr.h:28
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
to_ssa_expr
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
Definition: ssa_expr.h:160
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
ssa_exprt::get_l1_object
const ssa_exprt get_l1_object() const
Definition: ssa_expr.h:53
ssa_exprt::get_level_2
const irep_idt get_level_2() const
Definition: ssa_expr.h:117
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
ssa_exprt::set_level_1
void set_level_1(unsigned i)
Definition: ssa_expr.h:89
validation_modet
validation_modet
Definition: validation_mode.h:12
irept::id
const irep_idt & id() const
Definition: irep.h:259
irept::remove
void remove(const irep_namet &name)
Definition: irep.cpp:269
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:199
ssa_exprt::get_l1_object_identifier
const irep_idt get_l1_object_identifier() const
Definition: ssa_expr.h:66
ssa_exprt::update_identifier
void update_identifier()
Definition: ssa_expr.cpp:103
ssa_exprt::check
static void check(const exprt &expr, const validation_modet vm=validation_modet::INVARIANT)
Definition: ssa_expr.h:128
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
ssa_exprt::set_level_0
void set_level_0(unsigned i)
Definition: ssa_expr.h:83
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
ssa_exprt::get_level_1
const irep_idt get_level_1() const
Definition: ssa_expr.h:112
ssa_exprt::ssa_exprt
ssa_exprt()
Definition: ssa_expr.h:20
ssa_exprt::set_level_2
void set_level_2(unsigned i)
Definition: ssa_expr.h:95
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:88
ssa_exprt::can_build_identifier
static bool can_build_identifier(const exprt &src)
Definition: ssa_expr.cpp:77
object_descriptor_exprt::object
exprt & object()
Definition: std_expr.h:2147
std_expr.h
symbol_exprt::set_identifier
void set_identifier(const irep_idt &identifier)
Definition: std_expr.h:171
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:139