CBMC
expr_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "expr_util.h"
10 
11 #include "arith_tools.h"
12 #include "bitvector_expr.h"
13 #include "byte_operators.h"
14 #include "c_types.h"
15 #include "config.h"
16 #include "expr_iterator.h"
17 #include "namespace.h"
18 #include "pointer_expr.h"
19 #include "pointer_offset_size.h"
20 
21 #include <algorithm>
22 #include <unordered_set>
23 
24 bool is_assignable(const exprt &expr)
25 {
26  if(expr.id() == ID_index)
27  return is_assignable(to_index_expr(expr).array());
28  else if(expr.id() == ID_member)
29  return is_assignable(to_member_expr(expr).compound());
30  else if(expr.id() == ID_dereference)
31  return true;
32  else if(expr.id() == ID_symbol)
33  return true;
34  else
35  return false;
36 }
37 
38 exprt make_binary(const exprt &expr)
39 {
40  const exprt::operandst &operands=expr.operands();
41 
42  if(operands.size()<=2)
43  return expr;
44 
45  // types must be identical for make_binary to be safe to use
46  const typet &type=expr.type();
47 
48  exprt previous=operands.front();
49  PRECONDITION(previous.type()==type);
50 
51  for(exprt::operandst::const_iterator
52  it=++operands.begin();
53  it!=operands.end();
54  ++it)
55  {
56  PRECONDITION(it->type()==type);
57 
58  exprt tmp=expr;
59  tmp.operands().clear();
60  tmp.operands().resize(2);
61  to_binary_expr(tmp).op0().swap(previous);
62  to_binary_expr(tmp).op1() = *it;
63  previous.swap(tmp);
64  }
65 
66  return previous;
67 }
68 
70 {
71  return src.make_with_expr();
72 }
73 
75  const exprt &src,
76  const namespacet &ns)
77 {
78  // We frequently need to check if a numerical type is not zero.
79  // We replace (_Bool)x by x!=0; use ieee_float_notequal for floats.
80  // Note that this returns a proper bool_typet(), not a C/C++ boolean.
81  // To get a C/C++ boolean, add a further typecast.
82 
83  const typet &src_type = src.type().id() == ID_c_enum_tag
85  : src.type();
86 
87  if(src_type.id()==ID_bool) // already there
88  return src; // do nothing
89 
90  irep_idt id=
91  src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
92 
93  exprt zero=from_integer(0, src_type);
94  // Use tag type if applicable:
95  zero.type() = src.type();
96 
97  binary_relation_exprt comparison(src, id, std::move(zero));
98  comparison.add_source_location()=src.source_location();
99 
100  return std::move(comparison);
101 }
102 
104 {
105  if(src.id() == ID_not)
106  return to_not_expr(src).op();
107  else if(src.is_true())
108  return false_exprt();
109  else if(src.is_false())
110  return true_exprt();
111  else
112  return not_exprt(src);
113 }
114 
116  const exprt &expr,
117  const std::function<bool(const exprt &)> &pred)
118 {
119  const auto it = std::find_if(expr.depth_begin(), expr.depth_end(), pred);
120  return it != expr.depth_end();
121 }
122 
123 bool has_subexpr(const exprt &src, const irep_idt &id)
124 {
125  return has_subexpr(
126  src, [&](const exprt &subexpr) { return subexpr.id() == id; });
127 }
128 
130  const typet &type,
131  const std::function<bool(const typet &)> &pred,
132  const namespacet &ns)
133 {
134  std::vector<std::reference_wrapper<const typet>> stack;
135  std::unordered_set<typet, irep_hash> visited;
136 
137  const auto push_if_not_visited = [&](const typet &t) {
138  if(visited.insert(t).second)
139  stack.emplace_back(t);
140  };
141 
142  push_if_not_visited(type);
143  while(!stack.empty())
144  {
145  const typet &top = stack.back().get();
146  stack.pop_back();
147 
148  if(pred(top))
149  return true;
150  else if(top.id() == ID_c_enum_tag)
151  push_if_not_visited(ns.follow_tag(to_c_enum_tag_type(top)));
152  else if(top.id() == ID_struct_tag)
153  push_if_not_visited(ns.follow_tag(to_struct_tag_type(top)));
154  else if(top.id() == ID_union_tag)
155  push_if_not_visited(ns.follow_tag(to_union_tag_type(top)));
156  else if(top.id() == ID_struct || top.id() == ID_union)
157  {
158  for(const auto &comp : to_struct_union_type(top).components())
159  push_if_not_visited(comp.type());
160  }
161  else
162  {
163  for(const auto &subtype : to_type_with_subtypes(top).subtypes())
164  push_if_not_visited(subtype);
165  }
166  }
167 
168  return false;
169 }
170 
171 bool has_subtype(const typet &type, const irep_idt &id, const namespacet &ns)
172 {
173  return has_subtype(
174  type, [&](const typet &subtype) { return subtype.id() == id; }, ns);
175 }
176 
177 if_exprt lift_if(const exprt &src, std::size_t operand_number)
178 {
179  PRECONDITION(operand_number<src.operands().size());
180  PRECONDITION(src.operands()[operand_number].id()==ID_if);
181 
182  const if_exprt if_expr=to_if_expr(src.operands()[operand_number]);
183  const exprt true_case=if_expr.true_case();
184  const exprt false_case=if_expr.false_case();
185 
186  if_exprt result(if_expr.cond(), src, src);
187  result.true_case().operands()[operand_number]=true_case;
188  result.false_case().operands()[operand_number]=false_case;
189 
190  return result;
191 }
192 
193 const exprt &skip_typecast(const exprt &expr)
194 {
195  if(expr.id()!=ID_typecast)
196  return expr;
197 
198  return skip_typecast(to_typecast_expr(expr).op());
199 }
200 
204 {
205  if(
206  expr.id() == ID_symbol || expr.id() == ID_nondet_symbol ||
207  expr.id() == ID_side_effect)
208  {
209  return false;
210  }
211 
212  if(expr.id() == ID_address_of)
213  {
214  return is_constant_address_of(to_address_of_expr(expr).object());
215  }
216  else if(auto index = expr_try_dynamic_cast<index_exprt>(expr))
217  {
218  if(!is_constant(index->array()) || !index->index().is_constant())
219  return false;
220 
221  const auto &array_type = to_array_type(index->array().type());
222  if(!array_type.size().is_constant())
223  return false;
224 
225  const mp_integer size =
226  numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
227  const mp_integer index_int =
228  numeric_cast_v<mp_integer>(to_constant_expr(index->index()));
229 
230  return index_int >= 0 && index_int < size;
231  }
232  else if(auto be = expr_try_dynamic_cast<byte_extract_exprt>(expr))
233  {
234  if(!is_constant(be->op()) || !be->offset().is_constant())
235  return false;
236 
237  const auto op_bits = pointer_offset_bits(be->op().type(), ns);
238  if(!op_bits.has_value())
239  return false;
240 
241  const auto extract_bits = pointer_offset_bits(be->type(), ns);
242  if(!extract_bits.has_value())
243  return false;
244 
245  const mp_integer offset_bits =
246  numeric_cast_v<mp_integer>(to_constant_expr(be->offset())) *
247  be->get_bits_per_byte();
248 
249  return offset_bits >= 0 && offset_bits + *extract_bits <= *op_bits;
250  }
251  else if(auto eb = expr_try_dynamic_cast<extractbits_exprt>(expr))
252  {
253  if(!is_constant(eb->src()) || !eb->index().is_constant())
254  {
255  return false;
256  }
257 
258  const auto eb_bits = pointer_offset_bits(eb->type(), ns);
259  if(!eb_bits.has_value())
260  return false;
261 
262  const auto src_bits = pointer_offset_bits(eb->src().type(), ns);
263  if(!src_bits.has_value())
264  return false;
265 
266  const mp_integer lower_bound =
267  numeric_cast_v<mp_integer>(to_constant_expr(eb->index()));
268  const mp_integer upper_bound = lower_bound + eb_bits.value() - 1;
269 
270  return lower_bound >= 0 && lower_bound <= upper_bound &&
271  upper_bound < src_bits.value();
272  }
273  else
274  {
275  // std::all_of returns true when there are no operands
276  return std::all_of(
277  expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
278  return is_constant(e);
279  });
280  }
281 }
282 
285 {
286  if(expr.id() == ID_symbol)
287  {
288  return true;
289  }
290  else if(expr.id() == ID_index)
291  {
292  const index_exprt &index_expr = to_index_expr(expr);
293 
294  return is_constant_address_of(index_expr.array()) &&
295  is_constant(index_expr.index());
296  }
297  else if(expr.id() == ID_member)
298  {
299  return is_constant_address_of(to_member_expr(expr).compound());
300  }
301  else if(expr.id() == ID_dereference)
302  {
303  const dereference_exprt &deref = to_dereference_expr(expr);
304 
305  return is_constant(deref.pointer());
306  }
307  else if(expr.id() == ID_string_constant)
308  return true;
309 
310  return false;
311 }
312 
314 {
315  if(value)
316  return true_exprt();
317  else
318  return false_exprt();
319 }
320 
322 {
323  PRECONDITION(a.is_boolean() && b.is_boolean());
324  if(b.is_constant())
325  {
326  if(b.get(ID_value) == ID_false)
327  return false_exprt{};
328  return a;
329  }
330  if(a.is_constant())
331  {
332  if(a.get(ID_value) == ID_false)
333  return false_exprt{};
334  return b;
335  }
336  if(b.id() == ID_and)
337  {
338  b.add_to_operands(std::move(a));
339  return b;
340  }
341  return and_exprt{std::move(a), std::move(b)};
342 }
343 
345 {
346  return expr.is_null_pointer();
347 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
API to expression classes for bitvectors.
Expression classes for byte-level operators.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:224
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: c_types.h:377
Boolean AND.
Definition: std_expr.h:2120
exprt & op1()
Definition: expr.h:136
exprt & op0()
Definition: expr.h:133
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Definition: expr_util.cpp:284
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:203
const namespacet & ns
Definition: expr_util.h:104
A constant literal expression.
Definition: std_expr.h:2990
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Definition: std_expr.cpp:25
Operator to dereference a pointer.
Definition: pointer_expr.h:834
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
std::vector< exprt > operandst
Definition: expr.h:58
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
source_locationt & add_source_location()
Definition: expr.h:236
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
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
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
operandst & operands()
Definition: expr.h:94
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:170
The Boolean constant false.
Definition: std_expr.h:3072
The trinary if-then-else operator.
Definition: std_expr.h:2370
exprt & true_case()
Definition: std_expr.h:2397
exprt & false_case()
Definition: std_expr.h:2407
exprt & cond()
Definition: std_expr.h:2387
Array index operator.
Definition: std_expr.h:1465
exprt & array()
Definition: std_expr.h:1495
exprt & index()
Definition: std_expr.h:1505
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
const irep_idt & id() const
Definition: irep.h:388
void swap(irept &irep)
Definition: irep.h:434
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Boolean negation.
Definition: std_expr.h:2327
The Boolean constant true.
Definition: std_expr.h:3063
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:391
Operator to update elements in structs and arrays.
Definition: std_expr.h:2655
with_exprt make_with_expr() const
converts an update expr into a (possibly nested) with expression
Definition: std_expr.cpp:194
Operator to update elements in structs and arrays.
Definition: std_expr.h:2471
Forward depth-first search iterators These iterators' copy operations are expensive,...
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:313
with_exprt make_with_expr(const update_exprt &src)
converts an update expr into a (possibly nested) with expression
Definition: expr_util.cpp:69
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:74
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition: expr_util.cpp:24
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:38
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:193
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Definition: expr_util.cpp:115
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:177
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:321
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:103
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:344
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Definition: expr_util.cpp:129
Deprecated expression utility functions.
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:890
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:577
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Pointer Logic.
BigInt mp_integer
Definition: smt_terms.h:17
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2450
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3045
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2102
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2352
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:715
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2936
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:214
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:518
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:252