CBMC
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 #include "arith_tools.h"
14 #include "bitvector_types.h"
15 #include "expr_iterator.h"
16 #include "expr_util.h"
17 #include "fixedbv.h"
18 #include "ieee_float.h"
19 #include "rational.h"
20 #include "rational_tools.h"
21 #include "std_expr.h"
22 
23 #include <stack>
24 
27 bool exprt::is_true() const
28 {
29  return is_constant() && is_boolean() && get(ID_value) != ID_false;
30 }
31 
34 bool exprt::is_false() const
35 {
36  return is_constant() && is_boolean() && get(ID_value) == ID_false;
37 }
38 
47 bool exprt::is_zero() const
48 {
49  if(is_constant())
50  {
51  const constant_exprt &constant=to_constant_expr(*this);
52  const irep_idt &type_id=type().id_string();
53 
54  if(type_id==ID_integer || type_id==ID_natural)
55  {
56  return constant.value_is_zero_string();
57  }
58  else if(type_id==ID_rational)
59  {
60  rationalt rat_value;
61  if(to_rational(*this, rat_value))
62  CHECK_RETURN(false);
63  return rat_value.is_zero();
64  }
65  else if(
66  type_id == ID_unsignedbv || type_id == ID_signedbv ||
67  type_id == ID_c_bool || type_id == ID_c_bit_field)
68  {
69  return constant.value_is_zero_string();
70  }
71  else if(type_id==ID_fixedbv)
72  {
73  if(fixedbvt(constant)==0)
74  return true;
75  }
76  else if(type_id==ID_floatbv)
77  {
78  if(ieee_floatt(constant)==0)
79  return true;
80  }
81  else if(type_id==ID_pointer)
82  {
83  return is_null_pointer(constant);
84  }
85  }
86 
87  return false;
88 }
89 
96 bool exprt::is_one() const
97 {
98  if(is_constant())
99  {
100  const auto &constant_expr = to_constant_expr(*this);
101  const irep_idt &type_id = type().id();
102 
103  if(type_id==ID_integer || type_id==ID_natural)
104  {
105  mp_integer int_value =
106  string2integer(id2string(constant_expr.get_value()));
107  if(int_value==1)
108  return true;
109  }
110  else if(type_id==ID_rational)
111  {
112  rationalt rat_value;
113  if(to_rational(*this, rat_value))
114  CHECK_RETURN(false);
115  return rat_value.is_one();
116  }
117  else if(
118  type_id == ID_unsignedbv || type_id == ID_signedbv ||
119  type_id == ID_c_bool || type_id == ID_c_bit_field)
120  {
121  const auto width = to_bitvector_type(type()).get_width();
122  mp_integer int_value =
123  bvrep2integer(id2string(constant_expr.get_value()), width, false);
124  if(int_value==1)
125  return true;
126  }
127  else if(type_id==ID_fixedbv)
128  {
129  if(fixedbvt(constant_expr) == 1)
130  return true;
131  }
132  else if(type_id==ID_floatbv)
133  {
134  if(ieee_floatt(constant_expr) == 1)
135  return true;
136  }
137  }
138 
139  return false;
140 }
141 
148 {
150 
151  if(l.is_not_nil())
152  return l;
153 
154  for(const auto &op : operands())
155  {
156  const source_locationt &op_l = op.find_source_location();
157  if(op_l.is_not_nil())
158  return op_l;
159  }
160 
161  return source_locationt::nil();
162 }
163 
164 template <typename T>
165 void visit_post_template(std::function<void(T &)> visitor, T *_expr)
166 {
167  struct stack_entryt
168  {
169  T *e;
170  bool operands_pushed;
171  explicit stack_entryt(T *_e) : e(_e), operands_pushed(false)
172  {
173  }
174  };
175 
176  std::stack<stack_entryt> stack;
177 
178  stack.emplace(_expr);
179 
180  while(!stack.empty())
181  {
182  auto &top = stack.top();
183  if(top.operands_pushed)
184  {
185  visitor(*top.e);
186  stack.pop();
187  }
188  else
189  {
190  // do modification of 'top' before pushing in case 'top' isn't stable
191  top.operands_pushed = true;
192  for(auto &op : top.e->operands())
193  stack.emplace(&op);
194  }
195  }
196 }
197 
198 void exprt::visit_post(std::function<void(exprt &)> visitor)
199 {
200  visit_post_template(visitor, this);
201 }
202 
203 void exprt::visit_post(std::function<void(const exprt &)> visitor) const
204 {
205  visit_post_template(visitor, this);
206 }
207 
208 template <typename T>
209 static void visit_pre_template(std::function<void(T &)> visitor, T *_expr)
210 {
211  std::stack<T *> stack;
212 
213  stack.push(_expr);
214 
215  while(!stack.empty())
216  {
217  T &expr = *stack.top();
218  stack.pop();
219 
220  visitor(expr);
221 
222  for(auto &op : expr.operands())
223  stack.push(&op);
224  }
225 }
226 
227 void exprt::visit_pre(std::function<void(exprt &)> visitor)
228 {
229  visit_pre_template(visitor, this);
230 }
231 
232 void exprt::visit_pre(std::function<void(const exprt &)> visitor) const
233 {
234  visit_pre_template(visitor, this);
235 }
236 
238 {
239  visit_pre([&visitor](exprt &e) { visitor(e); });
240 }
241 
242 void exprt::visit(const_expr_visitort &visitor) const
243 {
244  visit_pre([&visitor](const exprt &e) { visitor(e); });
245 }
246 
248 { return depth_iteratort(*this); }
250 { return depth_iteratort(); }
252 { return const_depth_iteratort(*this); }
254 { return const_depth_iteratort(); }
256 { return const_depth_iteratort(*this); }
258 { return const_depth_iteratort(); }
259 depth_iteratort exprt::depth_begin(std::function<exprt &()> mutate_root) const
260 {
261  return depth_iteratort(*this, std::move(mutate_root));
262 }
263 
265 { return const_unique_depth_iteratort(*this); }
267 { return const_unique_depth_iteratort(); }
269 { return const_unique_depth_iteratort(*this); }
271 { return const_unique_depth_iteratort(); }
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:920
A constant literal expression.
Definition: std_expr.h:2987
bool value_is_zero_string() const
Definition: std_expr.cpp:18
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
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:147
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:96
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
depth_iteratort depth_end()
Definition: expr.cpp:249
const_depth_iteratort depth_cend() const
Definition: expr.cpp:257
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:266
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.h:224
depth_iteratort depth_begin()
Definition: expr.cpp:247
const source_locationt & source_location() const
Definition: expr.h:231
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:270
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:237
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:47
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:227
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:255
operandst & operands()
Definition: expr.h:94
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:198
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:268
const_unique_depth_iteratort unique_depth_begin() const
Definition: expr.cpp:264
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
const std::string & id_string() const
Definition: irep.h:387
bool is_not_nil() const
Definition: irep.h:368
const irep_idt & id() const
Definition: irep.h:384
bool is_one() const
Definition: rational.h:77
bool is_zero() const
Definition: rational.h:74
static const source_locationt & nil()
void visit_post_template(std::function< void(T &)> visitor, T *_expr)
Definition: expr.cpp:165
static void visit_pre_template(std::function< void(T &)> visitor, T *_expr)
Definition: expr.cpp:209
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition: expr_util.cpp:369
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
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:17
#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:3037