cprover
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 <algorithm>
12 #include <unordered_set>
13 
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 "namespace.h"
20 #include "pointer_expr.h"
21 #include "std_expr.h"
22 #include "symbol.h"
23 
24 bool is_lvalue(const exprt &expr)
25 {
26  if(expr.id() == ID_index)
27  return is_lvalue(to_index_expr(expr).array());
28  else if(expr.id() == ID_member)
29  return is_lvalue(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 exprt make_binary(const exprt &expr)
38 {
39  const exprt::operandst &operands=expr.operands();
40 
41  if(operands.size()<=2)
42  return expr;
43 
44  // types must be identical for make_binary to be safe to use
45  const typet &type=expr.type();
46 
47  exprt previous=operands.front();
48  PRECONDITION(previous.type()==type);
49 
50  for(exprt::operandst::const_iterator
51  it=++operands.begin();
52  it!=operands.end();
53  ++it)
54  {
55  PRECONDITION(it->type()==type);
56 
57  exprt tmp=expr;
58  tmp.operands().clear();
59  tmp.operands().resize(2);
60  to_binary_expr(tmp).op0().swap(previous);
61  to_binary_expr(tmp).op1() = *it;
62  previous.swap(tmp);
63  }
64 
65  return previous;
66 }
67 
69 {
70  const exprt::operandst &designator=src.designator();
71  PRECONDITION(!designator.empty());
72 
73  with_exprt result{exprt{}, exprt{}, exprt{}};
74  exprt *dest=&result;
75 
76  for(const auto &expr : designator)
77  {
78  with_exprt tmp{exprt{}, exprt{}, exprt{}};
79 
80  if(expr.id() == ID_index_designator)
81  {
82  tmp.where() = to_index_designator(expr).index();
83  }
84  else if(expr.id() == ID_member_designator)
85  {
86  // irep_idt component_name=
87  // to_member_designator(*it).get_component_name();
88  }
89  else
91 
92  *dest=tmp;
93  dest=&to_with_expr(*dest).new_value();
94  }
95 
96  return result;
97 }
98 
100  const exprt &src,
101  const namespacet &ns)
102 {
103  // We frequently need to check if a numerical type is not zero.
104  // We replace (_Bool)x by x!=0; use ieee_float_notequal for floats.
105  // Note that this returns a proper bool_typet(), not a C/C++ boolean.
106  // To get a C/C++ boolean, add a further typecast.
107 
108  const typet &src_type = src.type().id() == ID_c_enum_tag
109  ? ns.follow_tag(to_c_enum_tag_type(src.type()))
110  : src.type();
111 
112  if(src_type.id()==ID_bool) // already there
113  return src; // do nothing
114 
115  irep_idt id=
116  src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
117 
118  exprt zero=from_integer(0, src_type);
119  // Use tag type if applicable:
120  zero.type() = src.type();
121 
122  binary_relation_exprt comparison(src, id, std::move(zero));
123  comparison.add_source_location()=src.source_location();
124 
125  return std::move(comparison);
126 }
127 
129 {
130  if(src.id() == ID_not)
131  return to_not_expr(src).op();
132  else if(src.is_true())
133  return false_exprt();
134  else if(src.is_false())
135  return true_exprt();
136  else
137  return not_exprt(src);
138 }
139 
141  const exprt &expr,
142  const std::function<bool(const exprt &)> &pred)
143 {
144  const auto it = std::find_if(expr.depth_begin(), expr.depth_end(), pred);
145  return it != expr.depth_end();
146 }
147 
148 bool has_subexpr(const exprt &src, const irep_idt &id)
149 {
150  return has_subexpr(
151  src, [&](const exprt &subexpr) { return subexpr.id() == id; });
152 }
153 
155  const typet &type,
156  const std::function<bool(const typet &)> &pred,
157  const namespacet &ns)
158 {
159  std::vector<std::reference_wrapper<const typet>> stack;
160  std::unordered_set<typet, irep_hash> visited;
161 
162  const auto push_if_not_visited = [&](const typet &t) {
163  if(visited.insert(t).second)
164  stack.emplace_back(t);
165  };
166 
167  push_if_not_visited(type);
168  while(!stack.empty())
169  {
170  const typet &top = stack.back().get();
171  stack.pop_back();
172 
173  if(pred(top))
174  return true;
175  else if(top.id() == ID_c_enum_tag)
176  push_if_not_visited(ns.follow_tag(to_c_enum_tag_type(top)));
177  else if(top.id() == ID_struct_tag)
178  push_if_not_visited(ns.follow_tag(to_struct_tag_type(top)));
179  else if(top.id() == ID_union_tag)
180  push_if_not_visited(ns.follow_tag(to_union_tag_type(top)));
181  else if(top.id() == ID_struct || top.id() == ID_union)
182  {
183  for(const auto &comp : to_struct_union_type(top).components())
184  push_if_not_visited(comp.type());
185  }
186  else
187  {
188  for(const auto &subtype : to_type_with_subtypes(top).subtypes())
189  push_if_not_visited(subtype);
190  }
191  }
192 
193  return false;
194 }
195 
196 bool has_subtype(const typet &type, const irep_idt &id, const namespacet &ns)
197 {
198  return has_subtype(
199  type, [&](const typet &subtype) { return subtype.id() == id; }, ns);
200 }
201 
202 if_exprt lift_if(const exprt &src, std::size_t operand_number)
203 {
204  PRECONDITION(operand_number<src.operands().size());
205  PRECONDITION(src.operands()[operand_number].id()==ID_if);
206 
207  const if_exprt if_expr=to_if_expr(src.operands()[operand_number]);
208  const exprt true_case=if_expr.true_case();
209  const exprt false_case=if_expr.false_case();
210 
211  if_exprt result(if_expr.cond(), src, src);
212  result.true_case().operands()[operand_number]=true_case;
213  result.false_case().operands()[operand_number]=false_case;
214 
215  return result;
216 }
217 
218 const exprt &skip_typecast(const exprt &expr)
219 {
220  if(expr.id()!=ID_typecast)
221  return expr;
222 
223  return skip_typecast(to_typecast_expr(expr).op());
224 }
225 
228 bool is_constantt::is_constant(const exprt &expr) const
229 {
230  if(expr.is_constant())
231  return true;
232 
233  if(expr.id() == ID_address_of)
234  {
235  return is_constant_address_of(to_address_of_expr(expr).object());
236  }
237  else if(
238  expr.id() == ID_typecast || expr.id() == ID_array_of ||
239  expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array ||
240  expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
241  // byte_update works, byte_extract may be out-of-bounds
242  expr.id() == ID_byte_update_big_endian ||
243  expr.id() == ID_byte_update_little_endian)
244  {
245  return std::all_of(
246  expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
247  return is_constant(e);
248  });
249  }
250 
251  return false;
252 }
253 
256 {
257  if(expr.id() == ID_symbol)
258  {
259  return true;
260  }
261  else if(expr.id() == ID_index)
262  {
263  const index_exprt &index_expr = to_index_expr(expr);
264 
265  return is_constant_address_of(index_expr.array()) &&
266  is_constant(index_expr.index());
267  }
268  else if(expr.id() == ID_member)
269  {
270  return is_constant_address_of(to_member_expr(expr).compound());
271  }
272  else if(expr.id() == ID_dereference)
273  {
274  const dereference_exprt &deref = to_dereference_expr(expr);
275 
276  return is_constant(deref.pointer());
277  }
278  else if(expr.id() == ID_string_constant)
279  return true;
280 
281  return false;
282 }
283 
285 {
286  if(value)
287  return true_exprt();
288  else
289  return false_exprt();
290 }
291 
293 {
294  PRECONDITION(a.type().id() == ID_bool && b.type().id() == ID_bool);
295  if(b.is_constant())
296  {
297  if(b.get(ID_value) == ID_false)
298  return false_exprt{};
299  return a;
300  }
301  if(a.is_constant())
302  {
303  if(a.get(ID_value) == ID_false)
304  return false_exprt{};
305  return b;
306  }
307  if(b.id() == ID_and)
308  {
309  b.add_to_operands(std::move(a));
310  return b;
311  }
312  return and_exprt{std::move(a), std::move(b)};
313 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2173
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:563
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_c_enum_tag_type
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a typet to a c_enum_tag_typet.
Definition: std_types.h:729
make_and
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:292
skip_typecast
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:218
has_subexpr
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:140
arith_tools.h
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:279
to_struct_union_type
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:209
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
typet
The type of an expression, extends irept.
Definition: type.h:28
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2152
dereference_exprt
Operator to dereference a pointer.
Definition: pointer_expr.h:256
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2087
is_constantt::is_constant_address_of
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Definition: expr_util.cpp:255
with_exprt::new_value
exprt & new_value()
Definition: std_expr.h:2203
fixedbv.h
and_exprt
Boolean AND.
Definition: std_expr.h:1835
to_type_with_subtypes
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:198
exprt
Base class for all expressions.
Definition: expr.h:54
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
lift_if
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:202
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:47
make_binary
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:37
namespace.h
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:2124
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:56
to_binary_expr
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:628
expr.h
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
is_constantt::is_constant
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:228
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
has_subtype
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:154
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:269
boolean_negate
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:128
index_designatort::index
const exprt & index() const
Definition: std_expr.h:2260
pointer_expr.h
API to expression classes for Pointers.
index_exprt::index
exprt & index()
Definition: std_expr.h:1269
index_exprt::array
exprt & array()
Definition: std_expr.h:1259
irept::swap
void swap(irept &irep)
Definition: irep.h:452
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:407
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:523
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
false_exprt
The Boolean constant false.
Definition: std_expr.h:2726
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:294
to_with_expr
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2235
update_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2357
update_exprt::designator
exprt::operandst & designator()
Definition: std_expr.h:2383
expr_util.h
Deprecated expression utility functions.
expr_iterator.h
Forward depth-first search iterators These iterators' copy operations are expensive,...
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2114
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2067
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
is_not_zero
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:99
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1815
ieee_float.h
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:40
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2104
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:675
exprt::add_to_operands
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:140
to_member_expr
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2612
make_boolean_expr
constant_exprt make_boolean_expr(bool value)
returns true_exprt if given true and false_exprt otherwise
Definition: expr_util.cpp:284
make_with_expr
with_exprt make_with_expr(const update_exprt &src)
converts an update expr into a (possibly nested) with expression
Definition: expr_util.cpp:68
to_address_of_expr
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:237
exprt::operands
operandst & operands()
Definition: expr.h:96
index_exprt
Array index operator.
Definition: std_expr.h:1243
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
constant_exprt
A constant literal expression.
Definition: std_expr.h:2668
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:281
binary_exprt::op1
exprt & op1()
Definition: expr.h:106
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
binary_exprt::op0
exprt & op0()
Definition: expr.h:103
to_index_designator
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2288
is_lvalue
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
Definition: expr_util.cpp:24
not_exprt
Boolean negation.
Definition: std_expr.h:2042