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 
7 \*******************************************************************/
8 
11 
12 #include "expr.h"
13 #include "expr_iterator.h"
14 #include "fixedbv.h"
15 #include "ieee_float.h"
16 #include "rational.h"
17 #include "rational_tools.h"
18 #include "std_expr.h"
19 
20 #include <stack>
21 
23 {
24  operandst &op=operands();
25  op.push_back(static_cast<const exprt &>(get_nil_irep()));
26  op.back().swap(expr);
27 }
28 
30 {
31  operandst &op=operands();
32  #ifndef USE_LIST
33  op.reserve(op.size()+2);
34  #endif
35  op.push_back(static_cast<const exprt &>(get_nil_irep()));
36  op.back().swap(e1);
37  op.push_back(static_cast<const exprt &>(get_nil_irep()));
38  op.back().swap(e2);
39 }
40 
42 {
43  operandst &op=operands();
44  #ifndef USE_LIST
45  op.reserve(op.size()+3);
46  #endif
47  op.push_back(static_cast<const exprt &>(get_nil_irep()));
48  op.back().swap(e1);
49  op.push_back(static_cast<const exprt &>(get_nil_irep()));
50  op.back().swap(e2);
51  op.push_back(static_cast<const exprt &>(get_nil_irep()));
52  op.back().swap(e3);
53 }
54 
55 void exprt::copy_to_operands(const exprt &expr)
56 {
57  operands().push_back(expr);
58 }
59 
60 void exprt::copy_to_operands(const exprt &e1, const exprt &e2)
61 {
62  operandst &op=operands();
63  #ifndef USE_LIST
64  op.reserve(op.size()+2);
65  #endif
66  op.push_back(e1);
67  op.push_back(e2);
68 }
69 
71  const exprt &e1,
72  const exprt &e2,
73  const exprt &e3)
74 {
75  operandst &op=operands();
76  #ifndef USE_LIST
77  op.reserve(op.size()+3);
78  #endif
79  op.push_back(e1);
80  op.push_back(e2);
81  op.push_back(e3);
82 }
83 
84 void exprt::make_typecast(const typet &_type)
85 {
86  typecast_exprt new_expr(*this, _type);
87 
88  swap(new_expr);
89 }
90 
92 {
93  if(is_true())
94  {
95  *this=false_exprt();
96  return;
97  }
98  else if(is_false())
99  {
100  *this=true_exprt();
101  return;
102  }
103 
104  exprt new_expr;
105 
106  if(id()==ID_not && operands().size()==1)
107  {
108  new_expr.swap(operands().front());
109  }
110  else
111  {
112  new_expr=exprt(ID_not, type());
113  new_expr.move_to_operands(*this);
114  }
115 
116  swap(new_expr);
117 }
118 
119 bool exprt::is_constant() const
120 {
121  return id()==ID_constant;
122 }
123 
124 bool exprt::is_true() const
125 {
126  return is_constant() &&
127  type().id()==ID_bool &&
128  get(ID_value)!=ID_false;
129 }
130 
131 bool exprt::is_false() const
132 {
133  return is_constant() &&
134  type().id()==ID_bool &&
135  get(ID_value)==ID_false;
136 }
137 
138 void exprt::make_bool(bool value)
139 {
140  *this=exprt(ID_constant, typet(ID_bool));
141  set(ID_value, value?ID_true:ID_false);
142 }
143 
145 {
146  *this=exprt(ID_constant, typet(ID_bool));
147  set(ID_value, ID_true);
148 }
149 
151 {
152  *this=exprt(ID_constant, typet(ID_bool));
153  set(ID_value, ID_false);
154 }
155 
156 bool exprt::is_boolean() const
157 {
158  return type().id()==ID_bool;
159 }
160 
161 bool exprt::is_zero() const
162 {
163  if(is_constant())
164  {
165  const constant_exprt &constant=to_constant_expr(*this);
166  const irep_idt &type_id=type().id_string();
167 
168  if(type_id==ID_integer || type_id==ID_natural)
169  {
170  return constant.value_is_zero_string();
171  }
172  else if(type_id==ID_rational)
173  {
174  rationalt rat_value;
175  if(to_rational(*this, rat_value))
176  CHECK_RETURN(false);
177  return rat_value.is_zero();
178  }
179  else if(type_id==ID_unsignedbv ||
180  type_id==ID_signedbv ||
181  type_id==ID_c_bool)
182  {
183  return constant.value_is_zero_string();
184  }
185  else if(type_id==ID_fixedbv)
186  {
187  if(fixedbvt(constant)==0)
188  return true;
189  }
190  else if(type_id==ID_floatbv)
191  {
192  if(ieee_floatt(constant)==0)
193  return true;
194  }
195  else if(type_id==ID_pointer)
196  {
197  return constant.value_is_zero_string() ||
198  constant.get_value()==ID_NULL;
199  }
200  }
201 
202  return false;
203 }
204 
205 bool exprt::is_one() const
206 {
207  if(is_constant())
208  {
209  const std::string &value=get_string(ID_value);
210  const irep_idt &type_id=type().id_string();
211 
212  if(type_id==ID_integer || type_id==ID_natural)
213  {
214  mp_integer int_value=string2integer(value);
215  if(int_value==1)
216  return true;
217  }
218  else if(type_id==ID_rational)
219  {
220  rationalt rat_value;
221  if(to_rational(*this, rat_value))
222  CHECK_RETURN(false);
223  return rat_value.is_one();
224  }
225  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
226  {
227  mp_integer int_value=binary2integer(value, false);
228  if(int_value==1)
229  return true;
230  }
231  else if(type_id==ID_fixedbv)
232  {
233  if(fixedbvt(to_constant_expr(*this))==1)
234  return true;
235  }
236  else if(type_id==ID_floatbv)
237  {
238  if(ieee_floatt(to_constant_expr(*this))==1)
239  return true;
240  }
241  }
242 
243  return false;
244 }
245 
247 {
249 
250  if(l.is_not_nil())
251  return l;
252 
253  forall_operands(it, (*this))
254  {
255  const source_locationt &l=it->find_source_location();
256  if(l.is_not_nil())
257  return l;
258  }
259 
260  return static_cast<const source_locationt &>(get_nil_irep());
261 }
262 
264 {
265  std::stack<exprt *> stack;
266 
267  stack.push(this);
268 
269  while(!stack.empty())
270  {
271  exprt &expr=*stack.top();
272  stack.pop();
273 
274  visitor(expr);
275 
276  Forall_operands(it, expr)
277  stack.push(&(*it));
278  }
279 }
280 
281 void exprt::visit(const_expr_visitort &visitor) const
282 {
283  std::stack<const exprt *> stack;
284 
285  stack.push(this);
286 
287  while(!stack.empty())
288  {
289  const exprt &expr=*stack.top();
290  stack.pop();
291 
292  visitor(expr);
293 
294  forall_operands(it, expr)
295  stack.push(&(*it));
296  }
297 }
298 
300 { return depth_iteratort(*this); }
302 { return depth_iteratort(); }
304 { return const_depth_iteratort(*this); }
306 { return const_depth_iteratort(); }
308 { return const_depth_iteratort(*this); }
310 { return const_depth_iteratort(); }
311 depth_iteratort exprt::depth_begin(std::function<exprt &()> mutate_root) const
312 {
313  return depth_iteratort(*this, std::move(mutate_root));
314 }
315 
317 { return const_unique_depth_iteratort(*this); }
319 { return const_unique_depth_iteratort(); }
321 { return const_unique_depth_iteratort(*this); }
323 { return const_unique_depth_iteratort(); }
const irept & get_nil_irep()
Definition: irep.cpp:56
The type of an expression.
Definition: type.h:22
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
bool is_one() const
Definition: rational.h:79
const_unique_depth_iteratort unique_depth_cbegin() const
Definition: expr.cpp:320
bool is_boolean() const
Definition: expr.cpp:156
bool is_not_nil() const
Definition: irep.h:103
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
const_depth_iteratort depth_cbegin() const
Definition: expr.cpp:307
bool to_rational(const exprt &expr, rationalt &rational_value)
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
exprt()
Definition: expr.h:48
bool is_false() const
Definition: expr.cpp:131
const irep_idt & get_value() const
Definition: std_expr.h:4441
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
depth_iteratort depth_begin()
Definition: expr.cpp:299
A constant literal expression.
Definition: std_expr.h:4424
void make_bool(bool value)
Definition: expr.cpp:138
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:245
bool value_is_zero_string() const
Definition: std_expr.cpp:18
void make_true()
Definition: expr.cpp:144
const irep_idt & id() const
Definition: irep.h:189
void visit(class expr_visitort &visitor)
Definition: expr.cpp:263
The boolean constant true.
Definition: std_expr.h:4488
const source_locationt & find_source_location() const
Definition: expr.cpp:246
API to expression classes.
#define forall_operands(it, expr)
Definition: expr.h:17
bool is_zero() const
Definition: rational.h:76
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
The boolean constant false.
Definition: std_expr.h:4499
bool is_constant() const
Definition: expr.cpp:119
std::vector< exprt > operandst
Definition: expr.h:45
const_unique_depth_iteratort unique_depth_cend() const
Definition: expr.cpp:322
void make_not()
Definition: expr.cpp:91
Base class for all expressions.
Definition: expr.h:42
void make_false()
Definition: expr.cpp:150
const source_locationt & source_location() const
Definition: expr.h:125
const_depth_iteratort depth_cend() const
Definition: expr.cpp:309
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const std::string & id_string() const
Definition: irep.h:192
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
bool is_zero() const
Definition: expr.cpp:161
const_unique_depth_iteratort unique_depth_begin() const
Definition: expr.cpp:316
depth_iteratort depth_end()
Definition: expr.cpp:301
operandst & operands()
Definition: expr.h:66
#define stack(x)
Definition: parser.h:144
void make_typecast(const typet &_type)
Definition: expr.cpp:84
const_unique_depth_iteratort unique_depth_end() const
Definition: expr.cpp:318
bool is_one() const
Definition: expr.cpp:205