cprover
expr.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Expression Representation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6  Joel Allred, joel.allred@diffblue.com
7 
8 \*******************************************************************/
9 
12 
13 // clang-format off
14 #include "arith_tools.h"
15 #include "bitvector_types.h"
16 #include "expr.h"
17 #include "expr_iterator.h"
18 #include "fixedbv.h"
19 #include "ieee_float.h"
20 #include "rational.h"
21 #include "rational_tools.h"
22 #include "std_expr.h"
23 // clang-format on
24 
25 #include <stack>
26 
29 std::size_t exprt::bounded_size(std::size_t count, std::size_t limit) const
30 {
31  const auto &ops = operands();
32  count += ops.size();
33  for(const auto &op : ops)
34  {
35  if(count >= limit)
36  {
37  return count;
38  }
39  count = op.bounded_size(count, limit);
40  }
41  return count;
42 }
43 
46 std::size_t exprt::bounded_size(std::size_t limit) const
47 {
48  return bounded_size(1, limit);
49 }
50 
53 bool exprt::is_constant() const
54 {
55  return id()==ID_constant;
56 }
57 
60 bool exprt::is_true() const
61 {
62  return is_constant() &&
63  type().id()==ID_bool &&
64  get(ID_value)!=ID_false;
65 }
66 
69 bool exprt::is_false() const
70 {
71  return is_constant() &&
72  type().id()==ID_bool &&
73  get(ID_value)==ID_false;
74 }
75 
78 bool exprt::is_boolean() const
79 {
80  return type().id()==ID_bool;
81 }
82 
91 bool exprt::is_zero() const
92 {
93  if(is_constant())
94  {
95  const constant_exprt &constant=to_constant_expr(*this);
96  const irep_idt &type_id=type().id_string();
97 
98  if(type_id==ID_integer || type_id==ID_natural)
99  {
100  return constant.value_is_zero_string();
101  }
102  else if(type_id==ID_rational)
103  {
104  rationalt rat_value;
105  if(to_rational(*this, rat_value))
106  CHECK_RETURN(false);
107  return rat_value.is_zero();
108  }
109  else if(
110  type_id == ID_unsignedbv || type_id == ID_signedbv ||
111  type_id == ID_c_bool || type_id == ID_c_bit_field)
112  {
113  return constant.value_is_zero_string();
114  }
115  else if(type_id==ID_fixedbv)
116  {
117  if(fixedbvt(constant)==0)
118  return true;
119  }
120  else if(type_id==ID_floatbv)
121  {
122  if(ieee_floatt(constant)==0)
123  return true;
124  }
125  else if(type_id==ID_pointer)
126  {
127  return constant.value_is_zero_string() ||
128  constant.get_value()==ID_NULL;
129  }
130  }
131 
132  return false;
133 }
134 
141 bool exprt::is_one() const
142 {
143  if(is_constant())
144  {
145  const auto &constant_expr = to_constant_expr(*this);
146  const irep_idt &type_id = type().id();
147 
148  if(type_id==ID_integer || type_id==ID_natural)
149  {
150  mp_integer int_value =
151  string2integer(id2string(constant_expr.get_value()));
152  if(int_value==1)
153  return true;
154  }
155  else if(type_id==ID_rational)
156  {
157  rationalt rat_value;
158  if(to_rational(*this, rat_value))
159  CHECK_RETURN(false);
160  return rat_value.is_one();
161  }
162  else if(
163  type_id == ID_unsignedbv || type_id == ID_signedbv ||
164  type_id == ID_c_bool || type_id == ID_c_bit_field)
165  {
166  const auto width = to_bitvector_type(type()).get_width();
167  mp_integer int_value =
168  bvrep2integer(id2string(constant_expr.get_value()), width, false);
169  if(int_value==1)
170  return true;
171  }
172  else if(type_id==ID_fixedbv)
173  {
174  if(fixedbvt(constant_expr) == 1)
175  return true;
176  }
177  else if(type_id==ID_floatbv)
178  {
179  if(ieee_floatt(constant_expr) == 1)
180  return true;
181  }
182  }
183 
184  return false;
185 }
186 
193 {
195 
196  if(l.is_not_nil())
197  return l;
198 
199  forall_operands(it, (*this))
200  {
201  const source_locationt &op_l = it->find_source_location();
202  if(op_l.is_not_nil())
203  return op_l;
204  }
205 
206  return static_cast<const source_locationt &>(get_nil_irep());
207 }
208 
209 template <typename T>
210 void visit_post_template(std::function<void(T &)> visitor, T *_expr)
211 {
212  struct stack_entryt
213  {
214  T *e;
215  bool operands_pushed;
216  explicit stack_entryt(T *_e) : e(_e), operands_pushed(false)
217  {
218  }
219  };
220 
221  std::stack<stack_entryt> stack;
222 
223  stack.emplace(_expr);
224 
225  while(!stack.empty())
226  {
227  auto &top = stack.top();
228  if(top.operands_pushed)
229  {
230  visitor(*top.e);
231  stack.pop();
232  }
233  else
234  {
235  // do modification of 'top' before pushing in case 'top' isn't stable
236  top.operands_pushed = true;
237  for(auto &op : top.e->operands())
238  stack.emplace(&op);
239  }
240  }
241 }
242 
243 void exprt::visit_post(std::function<void(exprt &)> visitor)
244 {
245  visit_post_template(visitor, this);
246 }
247 
248 void exprt::visit_post(std::function<void(const exprt &)> visitor) const
249 {
250  visit_post_template(visitor, this);
251 }
252 
253 template <typename T>
254 static void visit_pre_template(std::function<void(T &)> visitor, T *_expr)
255 {
256  std::stack<T *> stack;
257 
258  stack.push(_expr);
259 
260  while(!stack.empty())
261  {
262  T &expr = *stack.top();
263  stack.pop();
264 
265  visitor(expr);
266 
267  for(auto &op : expr.operands())
268  stack.push(&op);
269  }
270 }
271 
272 void exprt::visit_pre(std::function<void(exprt &)> visitor)
273 {
274  visit_pre_template(visitor, this);
275 }
276 
277 void exprt::visit_pre(std::function<void(const exprt &)> visitor) const
278 {
279  visit_pre_template(visitor, this);
280 }
281 
283 {
284  visit_pre([&visitor](exprt &e) { visitor(e); });
285 }
286 
287 void exprt::visit(const_expr_visitort &visitor) const
288 {
289  visit_pre([&visitor](const exprt &e) { visitor(e); });
290 }
291 
293 { return depth_iteratort(*this); }
295 { return depth_iteratort(); }
297 { return const_depth_iteratort(*this); }
299 { return const_depth_iteratort(); }
301 { return const_depth_iteratort(*this); }
303 { return const_depth_iteratort(); }
304 depth_iteratort exprt::depth_begin(std::function<exprt &()> mutate_root) const
305 {
306  return depth_iteratort(*this, std::move(mutate_root));
307 }
308 
310 { return const_unique_depth_iteratort(*this); }
312 { return const_unique_depth_iteratort(); }
314 { return const_unique_depth_iteratort(*this); }
316 { return const_unique_depth_iteratort(); }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ieee_floatt
Definition: ieee_float.h:120
exprt::depth_cbegin
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:300
rationalt::is_zero
bool is_zero() const
Definition: rational.h:76
const_unique_depth_iteratort
Definition: expr_iterator.h:287
arith_tools.h
rational.h
rational_tools.h
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:292
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
to_rational
bool to_rational(const exprt &expr, rationalt &rational_value)
Definition: rational_tools.cpp:27
depth_iteratort
Definition: expr_iterator.h:230
fixedbv.h
exprt
Base class for all expressions.
Definition: expr.h:54
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:60
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: bitvector_types.h:32
exprt::visit
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:282
expr_visitort
Definition: expr.h:374
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:69
expr.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
const_depth_iteratort
Definition: expr_iterator.h:219
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
exprt::visit_post
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:243
exprt::find_source_location
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:192
bitvector_types.h
Pre-defined bitvector types.
exprt::bounded_size
std::size_t bounded_size(std::size_t limit) const
Amount of nodes in this expression tree approximately bounded by limit.
Definition: expr.cpp:46
irept::id_string
const std::string & id_string() const
Definition: irep.h:410
visit_post_template
void visit_post_template(std::function< void(T &)> visitor, T *_expr)
Definition: expr.cpp:210
const_expr_visitort
Definition: expr.h:381
irept::id
const irep_idt & id() const
Definition: irep.h:407
visit_pre_template
static void visit_pre_template(std::function< void(T &)> visitor, T *_expr)
Definition: expr.cpp:254
source_locationt
Definition: source_location.h:20
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:837
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:91
bvrep2integer
mp_integer bvrep2integer(const irep_idt &src, std::size_t width, bool is_signed)
convert a bit-vector representation (possibly signed) to integer
Definition: arith_tools.cpp:402
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
exprt::depth_cend
const_depth_iteratort depth_cend() const
Definition: expr.cpp:302
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:23
ieee_float.h
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:53
exprt::unique_depth_cend
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:315
exprt::visit_pre
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:272
fixedbvt
Definition: fixedbv.h:42
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:141
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:26
exprt::operands
operandst & operands()
Definition: expr.h:96
exprt::unique_depth_begin
const_unique_depth_iteratort unique_depth_begin() const
Definition: expr.cpp:309
exprt::unique_depth_cbegin
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:313
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
exprt::unique_depth_end
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:311
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:294
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:78
std_expr.h
API to expression classes.
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:2675
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:238
rationalt
Definition: rational.h:18
rationalt::is_one
bool is_one() const
Definition: rational.h:79
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700