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_constant() const
28 {
29  return id()==ID_constant;
30 }
31 
34 bool exprt::is_true() const
35 {
36  return is_constant() &&
37  type().id()==ID_bool &&
38  get(ID_value)!=ID_false;
39 }
40 
43 bool exprt::is_false() const
44 {
45  return is_constant() &&
46  type().id()==ID_bool &&
47  get(ID_value)==ID_false;
48 }
49 
52 bool exprt::is_boolean() const
53 {
54  return type().id()==ID_bool;
55 }
56 
65 bool exprt::is_zero() const
66 {
67  if(is_constant())
68  {
69  const constant_exprt &constant=to_constant_expr(*this);
70  const irep_idt &type_id=type().id_string();
71 
72  if(type_id==ID_integer || type_id==ID_natural)
73  {
74  return constant.value_is_zero_string();
75  }
76  else if(type_id==ID_rational)
77  {
78  rationalt rat_value;
79  if(to_rational(*this, rat_value))
80  CHECK_RETURN(false);
81  return rat_value.is_zero();
82  }
83  else if(
84  type_id == ID_unsignedbv || type_id == ID_signedbv ||
85  type_id == ID_c_bool || type_id == ID_c_bit_field)
86  {
87  return constant.value_is_zero_string();
88  }
89  else if(type_id==ID_fixedbv)
90  {
91  if(fixedbvt(constant)==0)
92  return true;
93  }
94  else if(type_id==ID_floatbv)
95  {
96  if(ieee_floatt(constant)==0)
97  return true;
98  }
99  else if(type_id==ID_pointer)
100  {
101  return is_null_pointer(constant);
102  }
103  }
104 
105  return false;
106 }
107 
114 bool 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  for(const auto &op : operands())
173  {
174  const source_locationt &op_l = op.find_source_location();
175  if(op_l.is_not_nil())
176  return op_l;
177  }
178 
179  return source_locationt::nil();
180 }
181 
182 template <typename T>
183 void 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 
216 void exprt::visit_post(std::function<void(exprt &)> visitor)
217 {
218  visit_post_template(visitor, this);
219 }
220 
221 void exprt::visit_post(std::function<void(const exprt &)> visitor) const
222 {
223  visit_post_template(visitor, this);
224 }
225 
226 template <typename T>
227 static 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 
245 void exprt::visit_pre(std::function<void(exprt &)> visitor)
246 {
247  visit_pre_template(visitor, this);
248 }
249 
250 void 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 
260 void exprt::visit(const_expr_visitort &visitor) const
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(); }
277 depth_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); }
285 { return const_unique_depth_iteratort(); }
287 { return const_unique_depth_iteratort(*this); }
289 { 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:876
A constant literal expression.
Definition: std_expr.h:2942
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:39
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: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:34
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:52
depth_iteratort depth_begin()
Definition: expr.cpp:265
const source_locationt & source_location() const
Definition: expr.h:211
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:43
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:65
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:245
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.cpp:27
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:273
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:216
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:44
const std::string & id_string() const
Definition: irep.h:399
bool is_not_nil() const
Definition: irep.h:380
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
static const source_locationt & nil()
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
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:356
Deprecated expression utility functions.
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:18
#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:2992