cprover
Loading...
Searching...
No Matches
expr.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Expression Representation
4
5Author: Daniel Kroening, kroening@kroening.com
6 Joel Allred, joel.allred@diffblue.com
7
8\*******************************************************************/
9
12
13#include "arith_tools.h"
14#include "bitvector_types.h"
15#include "expr_iterator.h"
16#include "fixedbv.h"
17#include "ieee_float.h"
18#include "rational.h"
19#include "rational_tools.h"
20#include "std_expr.h"
21
22#include <stack>
23
27{
28 return id()==ID_constant;
29}
30
33bool exprt::is_true() const
34{
35 return is_constant() &&
36 type().id()==ID_bool &&
37 get(ID_value)!=ID_false;
38}
39
42bool exprt::is_false() const
43{
44 return is_constant() &&
45 type().id()==ID_bool &&
46 get(ID_value)==ID_false;
47}
48
52{
53 return type().id()==ID_bool;
54}
55
64bool exprt::is_zero() const
65{
66 if(is_constant())
67 {
68 const constant_exprt &constant=to_constant_expr(*this);
69 const irep_idt &type_id=type().id_string();
70
71 if(type_id==ID_integer || type_id==ID_natural)
72 {
73 return constant.value_is_zero_string();
74 }
75 else if(type_id==ID_rational)
76 {
77 rationalt rat_value;
78 if(to_rational(*this, rat_value))
79 CHECK_RETURN(false);
80 return rat_value.is_zero();
81 }
82 else if(
83 type_id == ID_unsignedbv || type_id == ID_signedbv ||
84 type_id == ID_c_bool || type_id == ID_c_bit_field)
85 {
86 return constant.value_is_zero_string();
87 }
88 else if(type_id==ID_fixedbv)
89 {
90 if(fixedbvt(constant)==0)
91 return true;
92 }
93 else if(type_id==ID_floatbv)
94 {
95 if(ieee_floatt(constant)==0)
96 return true;
97 }
98 else if(type_id==ID_pointer)
99 {
100 return constant.value_is_zero_string() ||
101 constant.get_value()==ID_NULL;
102 }
103 }
104
105 return false;
106}
107
114bool exprt::is_one() const
115{
116 if(is_constant())
117 {
118 const auto &constant_expr = to_constant_expr(*this);
119 const irep_idt &type_id = type().id();
120
121 if(type_id==ID_integer || type_id==ID_natural)
122 {
123 mp_integer int_value =
124 string2integer(id2string(constant_expr.get_value()));
125 if(int_value==1)
126 return true;
127 }
128 else if(type_id==ID_rational)
129 {
130 rationalt rat_value;
131 if(to_rational(*this, rat_value))
132 CHECK_RETURN(false);
133 return rat_value.is_one();
134 }
135 else if(
136 type_id == ID_unsignedbv || type_id == ID_signedbv ||
137 type_id == ID_c_bool || type_id == ID_c_bit_field)
138 {
139 const auto width = to_bitvector_type(type()).get_width();
140 mp_integer int_value =
141 bvrep2integer(id2string(constant_expr.get_value()), width, false);
142 if(int_value==1)
143 return true;
144 }
145 else if(type_id==ID_fixedbv)
146 {
147 if(fixedbvt(constant_expr) == 1)
148 return true;
149 }
150 else if(type_id==ID_floatbv)
151 {
152 if(ieee_floatt(constant_expr) == 1)
153 return true;
154 }
155 }
156
157 return false;
158}
159
166{
168
169 if(l.is_not_nil())
170 return l;
171
172 forall_operands(it, (*this))
173 {
174 const source_locationt &op_l = it->find_source_location();
175 if(op_l.is_not_nil())
176 return op_l;
177 }
178
179 return static_cast<const source_locationt &>(get_nil_irep());
180}
181
182template <typename T>
183void visit_post_template(std::function<void(T &)> visitor, T *_expr)
184{
185 struct stack_entryt
186 {
187 T *e;
188 bool operands_pushed;
189 explicit stack_entryt(T *_e) : e(_e), operands_pushed(false)
190 {
191 }
192 };
193
194 std::stack<stack_entryt> stack;
195
196 stack.emplace(_expr);
197
198 while(!stack.empty())
199 {
200 auto &top = stack.top();
201 if(top.operands_pushed)
202 {
203 visitor(*top.e);
204 stack.pop();
205 }
206 else
207 {
208 // do modification of 'top' before pushing in case 'top' isn't stable
209 top.operands_pushed = true;
210 for(auto &op : top.e->operands())
211 stack.emplace(&op);
212 }
213 }
214}
215
216void exprt::visit_post(std::function<void(exprt &)> visitor)
217{
218 visit_post_template(visitor, this);
219}
220
221void exprt::visit_post(std::function<void(const exprt &)> visitor) const
222{
223 visit_post_template(visitor, this);
224}
225
226template <typename T>
227static void visit_pre_template(std::function<void(T &)> visitor, T *_expr)
228{
229 std::stack<T *> stack;
230
231 stack.push(_expr);
232
233 while(!stack.empty())
234 {
235 T &expr = *stack.top();
236 stack.pop();
237
238 visitor(expr);
239
240 for(auto &op : expr.operands())
241 stack.push(&op);
242 }
243}
244
245void exprt::visit_pre(std::function<void(exprt &)> visitor)
246{
247 visit_pre_template(visitor, this);
248}
249
250void exprt::visit_pre(std::function<void(const exprt &)> visitor) const
251{
252 visit_pre_template(visitor, this);
253}
254
256{
257 visit_pre([&visitor](exprt &e) { visitor(e); });
258}
259
261{
262 visit_pre([&visitor](const exprt &e) { visitor(e); });
263}
264
266{ return depth_iteratort(*this); }
268{ return depth_iteratort(); }
270{ return const_depth_iteratort(*this); }
272{ return const_depth_iteratort(); }
274{ return const_depth_iteratort(*this); }
276{ return const_depth_iteratort(); }
277depth_iteratort exprt::depth_begin(std::function<exprt &()> mutate_root) const
278{
279 return depth_iteratort(*this, std::move(mutate_root));
280}
281
283{ return const_unique_depth_iteratort(*this); }
287{ return const_unique_depth_iteratort(*this); }
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
std::size_t get_width() const
Definition: std_types.h:864
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
bool value_is_zero_string() const
Definition: std_expr.cpp:16
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
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:165
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:114
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
depth_iteratort depth_end()
Definition: expr.cpp:267
const_depth_iteratort depth_cend() const
Definition: expr.cpp:275
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:284
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:51
depth_iteratort depth_begin()
Definition: expr.cpp:265
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:288
void visit(class expr_visitort &visitor)
These are pre-order traversal visitors, i.e., the visitor is executed on a node before its children h...
Definition: expr.cpp:255
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:245
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
typet & type()
Return the type of the expression.
Definition: expr.h:82
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:273
void visit_post(std::function< void(exprt &)>)
These are post-order traversal visitors, i.e., the visitor is executed on a node after its children h...
Definition: expr.cpp:216
const source_locationt & source_location() const
Definition: expr.h:230
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:286
const_unique_depth_iteratort unique_depth_begin() const
Definition: expr.cpp:282
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
bool is_not_nil() const
Definition: irep.h:380
const std::string & id_string() const
Definition: irep.h:399
const irep_idt & id() const
Definition: irep.h:396
bool is_one() const
Definition: rational.h:77
bool is_zero() const
Definition: rational.h:74
void visit_post_template(std::function< void(T &)> visitor, T *_expr)
Definition: expr.cpp:183
static void visit_pre_template(std::function< void(T &)> visitor, T *_expr)
Definition: expr.cpp:227
#define forall_operands(it, expr)
Definition: expr.h:18
Forward depth-first search iterators These iterators' copy operations are expensive,...
const irept & get_nil_irep()
Definition: irep.cpp:20
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
bool to_rational(const exprt &expr, rationalt &rational_value)
BigInt mp_integer
Definition: smt_terms.h:12
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840