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 "expr.h"
16 #include "expr_iterator.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 // clang-format on
23 
24 #include <stack>
25 
26 std::size_t exprt::size() const
27 {
28  // Initial size of 1 to count self.
29  std::size_t size = 1;
30  for(const auto &op : operands())
31  {
32  size += op.size();
33  }
34 
35  return size;
36 }
37 
40 bool exprt::is_constant() const
41 {
42  return id()==ID_constant;
43 }
44 
47 bool exprt::is_true() const
48 {
49  return is_constant() &&
50  type().id()==ID_bool &&
51  get(ID_value)!=ID_false;
52 }
53 
56 bool exprt::is_false() const
57 {
58  return is_constant() &&
59  type().id()==ID_bool &&
60  get(ID_value)==ID_false;
61 }
62 
65 bool exprt::is_boolean() const
66 {
67  return type().id()==ID_bool;
68 }
69 
78 bool exprt::is_zero() const
79 {
80  if(is_constant())
81  {
82  const constant_exprt &constant=to_constant_expr(*this);
83  const irep_idt &type_id=type().id_string();
84 
85  if(type_id==ID_integer || type_id==ID_natural)
86  {
87  return constant.value_is_zero_string();
88  }
89  else if(type_id==ID_rational)
90  {
91  rationalt rat_value;
92  if(to_rational(*this, rat_value))
93  CHECK_RETURN(false);
94  return rat_value.is_zero();
95  }
96  else if(
97  type_id == ID_unsignedbv || type_id == ID_signedbv ||
98  type_id == ID_c_bool || type_id == ID_c_bit_field)
99  {
100  return constant.value_is_zero_string();
101  }
102  else if(type_id==ID_fixedbv)
103  {
104  if(fixedbvt(constant)==0)
105  return true;
106  }
107  else if(type_id==ID_floatbv)
108  {
109  if(ieee_floatt(constant)==0)
110  return true;
111  }
112  else if(type_id==ID_pointer)
113  {
114  return constant.value_is_zero_string() ||
115  constant.get_value()==ID_NULL;
116  }
117  }
118 
119  return false;
120 }
121 
128 bool exprt::is_one() const
129 {
130  if(is_constant())
131  {
132  const auto &constant_expr = to_constant_expr(*this);
133  const irep_idt &type_id = type().id();
134 
135  if(type_id==ID_integer || type_id==ID_natural)
136  {
137  mp_integer int_value =
138  string2integer(id2string(constant_expr.get_value()));
139  if(int_value==1)
140  return true;
141  }
142  else if(type_id==ID_rational)
143  {
144  rationalt rat_value;
145  if(to_rational(*this, rat_value))
146  CHECK_RETURN(false);
147  return rat_value.is_one();
148  }
149  else if(
150  type_id == ID_unsignedbv || type_id == ID_signedbv ||
151  type_id == ID_c_bool || type_id == ID_c_bit_field)
152  {
153  const auto width = to_bitvector_type(type()).get_width();
154  mp_integer int_value =
155  bvrep2integer(id2string(constant_expr.get_value()), width, false);
156  if(int_value==1)
157  return true;
158  }
159  else if(type_id==ID_fixedbv)
160  {
161  if(fixedbvt(constant_expr) == 1)
162  return true;
163  }
164  else if(type_id==ID_floatbv)
165  {
166  if(ieee_floatt(constant_expr) == 1)
167  return true;
168  }
169  }
170 
171  return false;
172 }
173 
180 {
182 
183  if(l.is_not_nil())
184  return l;
185 
186  forall_operands(it, (*this))
187  {
188  const source_locationt &op_l = it->find_source_location();
189  if(op_l.is_not_nil())
190  return op_l;
191  }
192 
193  return static_cast<const source_locationt &>(get_nil_irep());
194 }
195 
196 template <typename T>
197 void visit_post_template(std::function<void(T &)> visitor, T *_expr)
198 {
199  struct stack_entryt
200  {
201  T *e;
202  bool operands_pushed;
203  explicit stack_entryt(T *_e) : e(_e), operands_pushed(false)
204  {
205  }
206  };
207 
208  std::stack<stack_entryt> stack;
209 
210  stack.emplace(_expr);
211 
212  while(!stack.empty())
213  {
214  auto &top = stack.top();
215  if(top.operands_pushed)
216  {
217  visitor(*top.e);
218  stack.pop();
219  }
220  else
221  {
222  // do modification of 'top' before pushing in case 'top' isn't stable
223  top.operands_pushed = true;
224  for(auto &op : top.e->operands())
225  stack.emplace(&op);
226  }
227  }
228 }
229 
230 void exprt::visit_post(std::function<void(exprt &)> visitor)
231 {
232  visit_post_template(visitor, this);
233 }
234 
235 void exprt::visit_post(std::function<void(const exprt &)> visitor) const
236 {
237  visit_post_template(visitor, this);
238 }
239 
240 template <typename T>
241 static void visit_pre_template(std::function<void(T &)> visitor, T *_expr)
242 {
243  std::stack<T *> stack;
244 
245  stack.push(_expr);
246 
247  while(!stack.empty())
248  {
249  T &expr = *stack.top();
250  stack.pop();
251 
252  visitor(expr);
253 
254  for(auto &op : expr.operands())
255  stack.push(&op);
256  }
257 }
258 
259 void exprt::visit_pre(std::function<void(exprt &)> visitor)
260 {
261  visit_pre_template(visitor, this);
262 }
263 
264 void exprt::visit_pre(std::function<void(const exprt &)> visitor) const
265 {
266  visit_pre_template(visitor, this);
267 }
268 
270 {
271  visit_pre([&visitor](exprt &e) { visitor(e); });
272 }
273 
274 void exprt::visit(const_expr_visitort &visitor) const
275 {
276  visit_pre([&visitor](const exprt &e) { visitor(e); });
277 }
278 
280 { return depth_iteratort(*this); }
282 { return depth_iteratort(); }
284 { return const_depth_iteratort(*this); }
286 { return const_depth_iteratort(); }
288 { return const_depth_iteratort(*this); }
290 { return const_depth_iteratort(); }
291 depth_iteratort exprt::depth_begin(std::function<exprt &()> mutate_root) const
292 {
293  return depth_iteratort(*this, std::move(mutate_root));
294 }
295 
297 { return const_unique_depth_iteratort(*this); }
299 { return const_unique_depth_iteratort(); }
301 { return const_unique_depth_iteratort(*this); }
303 { 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
std::size_t get_width() const
Definition: std_types.h:1048
A constant literal expression.
Definition: std_expr.h:2668
const irep_idt & get_value() const
Definition: std_expr.h:2676
bool value_is_zero_string() const
Definition: std_expr.cpp:23
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:179
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:128
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
depth_iteratort depth_end()
Definition: expr.cpp:281
const_depth_iteratort depth_cend() const
Definition: expr.cpp:289
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:298
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:65
depth_iteratort depth_begin()
Definition: expr.cpp:279
const source_locationt & source_location() const
Definition: expr.h:234
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:302
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:269
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:78
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:259
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:287
operandst & operands()
Definition: expr.h:96
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:230
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:300
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
const_unique_depth_iteratort unique_depth_begin() const
Definition: expr.cpp:296
const std::string & id_string() const
Definition: irep.h:410
bool is_not_nil() const
Definition: irep.h:391
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
bool is_one() const
Definition: rational.h:79
bool is_zero() const
Definition: rational.h:76
void visit_post_template(std::function< void(T &)> visitor, T *_expr)
Definition: expr.cpp:197
static void visit_pre_template(std::function< void(T &)> visitor, T *_expr)
Definition: expr.cpp:241
#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:26
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
BigInt mp_integer
Definition: mp_arith.h:19
bool to_rational(const exprt &expr, rationalt &rational_value)
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1096