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 
30 {
31  operandst &op=operands();
32  op.push_back(static_cast<const exprt &>(get_nil_irep()));
33  op.back().swap(expr);
34 }
35 
41 {
42  operandst &op=operands();
43  #ifndef USE_LIST
44  op.reserve(op.size()+2);
45  #endif
46  op.push_back(static_cast<const exprt &>(get_nil_irep()));
47  op.back().swap(e1);
48  op.push_back(static_cast<const exprt &>(get_nil_irep()));
49  op.back().swap(e2);
50 }
51 
58 {
59  operandst &op=operands();
60  #ifndef USE_LIST
61  op.reserve(op.size()+3);
62  #endif
63  op.push_back(static_cast<const exprt &>(get_nil_irep()));
64  op.back().swap(e1);
65  op.push_back(static_cast<const exprt &>(get_nil_irep()));
66  op.back().swap(e2);
67  op.push_back(static_cast<const exprt &>(get_nil_irep()));
68  op.back().swap(e3);
69 }
70 
74 void exprt::make_typecast(const typet &_type)
75 {
76  typecast_exprt new_expr(*this, _type);
77 
78  swap(new_expr);
79 }
80 
83 bool exprt::is_constant() const
84 {
85  return id()==ID_constant;
86 }
87 
90 bool exprt::is_true() const
91 {
92  return is_constant() &&
93  type().id()==ID_bool &&
94  get(ID_value)!=ID_false;
95 }
96 
99 bool exprt::is_false() const
100 {
101  return is_constant() &&
102  type().id()==ID_bool &&
103  get(ID_value)==ID_false;
104 }
105 
109 void exprt::make_bool(bool value)
110 {
111  *this=exprt(ID_constant, typet(ID_bool));
112  set(ID_value, value?ID_true:ID_false);
113 }
114 
117 bool exprt::is_boolean() const
118 {
119  return type().id()==ID_bool;
120 }
121 
130 bool exprt::is_zero() const
131 {
132  if(is_constant())
133  {
134  const constant_exprt &constant=to_constant_expr(*this);
135  const irep_idt &type_id=type().id_string();
136 
137  if(type_id==ID_integer || type_id==ID_natural)
138  {
139  return constant.value_is_zero_string();
140  }
141  else if(type_id==ID_rational)
142  {
143  rationalt rat_value;
144  if(to_rational(*this, rat_value))
145  CHECK_RETURN(false);
146  return rat_value.is_zero();
147  }
148  else if(
149  type_id == ID_unsignedbv || type_id == ID_signedbv ||
150  type_id == ID_c_bool || type_id == ID_c_bit_field)
151  {
152  return constant.value_is_zero_string();
153  }
154  else if(type_id==ID_fixedbv)
155  {
156  if(fixedbvt(constant)==0)
157  return true;
158  }
159  else if(type_id==ID_floatbv)
160  {
161  if(ieee_floatt(constant)==0)
162  return true;
163  }
164  else if(type_id==ID_pointer)
165  {
166  return constant.value_is_zero_string() ||
167  constant.get_value()==ID_NULL;
168  }
169  }
170 
171  return false;
172 }
173 
180 bool exprt::is_one() const
181 {
182  if(is_constant())
183  {
184  const auto &constant_expr = to_constant_expr(*this);
185  const irep_idt &type_id = type().id();
186 
187  if(type_id==ID_integer || type_id==ID_natural)
188  {
189  mp_integer int_value =
190  string2integer(id2string(constant_expr.get_value()));
191  if(int_value==1)
192  return true;
193  }
194  else if(type_id==ID_rational)
195  {
196  rationalt rat_value;
197  if(to_rational(*this, rat_value))
198  CHECK_RETURN(false);
199  return rat_value.is_one();
200  }
201  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
202  {
203  const auto width = to_bitvector_type(type()).get_width();
204  mp_integer int_value =
205  bvrep2integer(id2string(constant_expr.get_value()), width, false);
206  if(int_value==1)
207  return true;
208  }
209  else if(type_id==ID_fixedbv)
210  {
211  if(fixedbvt(constant_expr) == 1)
212  return true;
213  }
214  else if(type_id==ID_floatbv)
215  {
216  if(ieee_floatt(constant_expr) == 1)
217  return true;
218  }
219  }
220 
221  return false;
222 }
223 
230 {
232 
233  if(l.is_not_nil())
234  return l;
235 
236  forall_operands(it, (*this))
237  {
238  const source_locationt &op_l = it->find_source_location();
239  if(op_l.is_not_nil())
240  return op_l;
241  }
242 
243  return static_cast<const source_locationt &>(get_nil_irep());
244 }
245 
247 {
248  std::stack<exprt *> stack;
249 
250  stack.push(this);
251 
252  while(!stack.empty())
253  {
254  exprt &expr=*stack.top();
255  stack.pop();
256 
257  visitor(expr);
258 
259  Forall_operands(it, expr)
260  stack.push(&(*it));
261  }
262 }
263 
264 void exprt::visit(const_expr_visitort &visitor) const
265 {
266  std::stack<const exprt *> stack;
267 
268  stack.push(this);
269 
270  while(!stack.empty())
271  {
272  const exprt &expr=*stack.top();
273  stack.pop();
274 
275  visitor(expr);
276 
277  forall_operands(it, expr)
278  stack.push(&(*it));
279  }
280 }
281 
283 { return depth_iteratort(*this); }
285 { return depth_iteratort(); }
287 { return const_depth_iteratort(*this); }
289 { return const_depth_iteratort(); }
291 { return const_depth_iteratort(*this); }
293 { return const_depth_iteratort(); }
294 depth_iteratort exprt::depth_begin(std::function<exprt &()> mutate_root) const
295 {
296  return depth_iteratort(*this, std::move(mutate_root));
297 }
298 
300 { return const_unique_depth_iteratort(*this); }
302 { return const_unique_depth_iteratort(); }
304 { return const_unique_depth_iteratort(*this); }
306 { 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:35
ieee_floatt
Definition: ieee_float.h:119
exprt::move_to_operands
void move_to_operands(exprt &expr)
Move the given argument to the end of exprt's operands.
Definition: expr.cpp:29
exprt::depth_cbegin
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:290
rationalt::is_zero
bool is_zero() const
Definition: rational.h:76
const_unique_depth_iteratort
Definition: expr_iterator.h:292
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:284
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:26
arith_tools.h
rational.h
rational_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:27
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
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:235
fixedbv.h
exprt::make_bool
void make_bool(bool value)
Replace the expression by a Boolean expression representing value.
Definition: expr.cpp:109
exprt::exprt
exprt()
Definition: expr.h:60
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:90
exprt::visit
void visit(class expr_visitort &visitor)
Definition: expr.cpp:246
expr_visitort
Definition: expr.h:321
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
expr.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
const_depth_iteratort
Definition: expr_iterator.h:224
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
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:229
irept::id_string
const std::string & id_string() const
Definition: irep.h:262
const_expr_visitort
Definition: expr.h:328
irept::swap
void swap(irept &irep)
Definition: irep.h:303
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
source_locationt
Definition: source_location.h:20
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1117
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:130
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:425
expr_iterator.h
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
exprt::depth_cend
const_depth_iteratort depth_cend() const
Definition: expr.cpp:292
constant_exprt::value_is_zero_string
bool value_is_zero_string() const
Definition: std_expr.cpp:20
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:282
stack
#define stack(x)
Definition: parser.h:144
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
ieee_float.h
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
exprt::unique_depth_cend
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:305
fixedbvt
Definition: fixedbv.h:41
exprt::is_one
bool is_one() const
Return whether the expression is a constant representing 1.
Definition: expr.cpp:180
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:55
exprt::operands
operandst & operands()
Definition: expr.h:78
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
exprt::unique_depth_begin
const_unique_depth_iteratort unique_depth_begin() const
Definition: expr.cpp:299
exprt::unique_depth_cbegin
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:303
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
exprt::unique_depth_end
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:301
exprt::is_boolean
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition: expr.cpp:117
std_expr.h
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:4403
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
rationalt
Definition: rational.h:17
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158
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:4423
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470