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 "expr.h"
15 #include "expr_iterator.h"
16 #include "fixedbv.h"
17 #include "ieee_float.h"
18 #include "std_expr.h"
19 #include "symbol.h"
20 #include "namespace.h"
21 #include "arith_tools.h"
22 
23 bool is_lvalue(const exprt &expr)
24 {
25  if(expr.id() == ID_index)
26  return is_lvalue(to_index_expr(expr).array());
27  else if(expr.id() == ID_member)
28  return is_lvalue(to_member_expr(expr).compound());
29  else if(expr.id() == ID_dereference)
30  return true;
31  else if(expr.id() == ID_symbol)
32  return true;
33  else
34  return false;
35 }
36 exprt make_binary(const exprt &expr)
37 {
38  const exprt::operandst &operands=expr.operands();
39 
40  if(operands.size()<=2)
41  return expr;
42 
43  // types must be identical for make_binary to be safe to use
44  const typet &type=expr.type();
45 
46  exprt previous=operands.front();
47  PRECONDITION(previous.type()==type);
48 
49  for(exprt::operandst::const_iterator
50  it=++operands.begin();
51  it!=operands.end();
52  ++it)
53  {
54  PRECONDITION(it->type()==type);
55 
56  exprt tmp=expr;
57  tmp.operands().clear();
58  tmp.operands().resize(2);
59  to_binary_expr(tmp).op0().swap(previous);
60  to_binary_expr(tmp).op1() = *it;
61  previous.swap(tmp);
62  }
63 
64  return previous;
65 }
66 
68 {
69  const exprt::operandst &designator=src.designator();
70  PRECONDITION(!designator.empty());
71 
72  with_exprt result;
73  exprt *dest=&result;
74 
75  forall_expr(it, designator)
76  {
77  with_exprt tmp;
78 
79  if(it->id()==ID_index_designator)
80  {
81  tmp.where()=to_index_designator(*it).index();
82  }
83  else if(it->id()==ID_member_designator)
84  {
85  // irep_idt component_name=
86  // to_member_designator(*it).get_component_name();
87  }
88  else
90 
91  *dest=tmp;
92  dest=&to_with_expr(*dest).new_value();
93  }
94 
95  return result;
96 }
97 
99  const exprt &src,
100  const namespacet &ns)
101 {
102  // We frequently need to check if a numerical type is not zero.
103  // We replace (_Bool)x by x!=0; use ieee_float_notequal for floats.
104  // Note that this returns a proper bool_typet(), not a C/C++ boolean.
105  // To get a C/C++ boolean, add a further typecast.
106 
107  const typet &src_type=
108  src.type().id()==ID_c_enum_tag?
110  ns.follow(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  CHECK_RETURN(zero.is_not_nil());
120 
121  binary_exprt comparison(src, id, zero, bool_typet());
122  comparison.add_source_location()=src.source_location();
123 
124  return std::move(comparison);
125 }
126 
128 {
129  if(src.id() == ID_not)
130  return to_not_expr(src).op();
131  else if(src.is_true())
132  return false_exprt();
133  else if(src.is_false())
134  return true_exprt();
135  else
136  return not_exprt(src);
137 }
138 
140  const exprt &expr,
141  const std::function<bool(const exprt &)> &pred)
142 {
143  const auto it = std::find_if(expr.depth_begin(), expr.depth_end(), pred);
144  return it != expr.depth_end();
145 }
146 
147 bool has_subexpr(const exprt &src, const irep_idt &id)
148 {
149  return has_subexpr(
150  src, [&](const exprt &subexpr) { return subexpr.id() == id; });
151 }
152 
154  const typet &type,
155  const std::function<bool(const typet &)> &pred,
156  const namespacet &ns)
157 {
158  std::vector<std::reference_wrapper<const typet>> stack;
159  std::unordered_set<typet, irep_hash> visited;
160 
161  const auto push_if_not_visited = [&](const typet &t) {
162  if(visited.insert(t).second)
163  stack.emplace_back(t);
164  };
165 
166  push_if_not_visited(type);
167  while(!stack.empty())
168  {
169  const typet &top = stack.back().get();
170  stack.pop_back();
171 
172  if(pred(top))
173  return true;
174  else if(top.id() == ID_symbol)
175  push_if_not_visited(ns.follow(top));
176  else if(top.id() == ID_c_enum_tag)
177  push_if_not_visited(ns.follow_tag(to_c_enum_tag_type(top)));
178  else if(top.id() == ID_struct || top.id() == ID_union)
179  {
180  for(const auto &comp : to_struct_union_type(top).components())
181  push_if_not_visited(comp.type());
182  }
183  else
184  {
185  for(const auto &subtype : to_type_with_subtypes(top).subtypes())
186  push_if_not_visited(subtype);
187  }
188  }
189 
190  return false;
191 }
192 
193 bool has_subtype(const typet &type, const irep_idt &id, const namespacet &ns)
194 {
195  return has_subtype(
196  type, [&](const typet &subtype) { return subtype.id() == id; }, ns);
197 }
198 
199 if_exprt lift_if(const exprt &src, std::size_t operand_number)
200 {
201  PRECONDITION(operand_number<src.operands().size());
202  PRECONDITION(src.operands()[operand_number].id()==ID_if);
203 
204  const if_exprt if_expr=to_if_expr(src.operands()[operand_number]);
205  const exprt true_case=if_expr.true_case();
206  const exprt false_case=if_expr.false_case();
207 
208  if_exprt result;
209  result.cond()=if_expr.cond();
210  result.type()=src.type();
211  result.true_case()=src;
212  result.true_case().operands()[operand_number]=true_case;
213  result.false_case()=src;
214  result.false_case().operands()[operand_number]=false_case;
215 
216  return result;
217 }
218 
219 const exprt &skip_typecast(const exprt &expr)
220 {
221  if(expr.id()!=ID_typecast)
222  return expr;
223 
224  return skip_typecast(to_typecast_expr(expr).op());
225 }
226 
229 bool is_constantt::is_constant(const exprt &expr) const
230 {
231  if(expr.is_constant())
232  return true;
233 
234  if(expr.id() == ID_address_of)
235  {
236  return is_constant_address_of(to_address_of_expr(expr).object());
237  }
238  else if(
239  expr.id() == ID_typecast || expr.id() == ID_array_of ||
240  expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array ||
241  expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
242  // byte_update works, byte_extract may be out-of-bounds
243  expr.id() == ID_byte_update_big_endian ||
244  expr.id() == ID_byte_update_little_endian)
245  {
246  return std::all_of(
247  expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
248  return is_constant(e);
249  });
250  }
251 
252  return false;
253 }
254 
257 {
258  if(expr.id() == ID_symbol)
259  {
260  return true;
261  }
262  else if(expr.id() == ID_index)
263  {
264  const index_exprt &index_expr = to_index_expr(expr);
265 
266  return is_constant_address_of(index_expr.array()) &&
267  is_constant(index_expr.index());
268  }
269  else if(expr.id() == ID_member)
270  {
271  return is_constant_address_of(to_member_expr(expr).compound());
272  }
273  else if(expr.id() == ID_string_constant)
274  return true;
275 
276  return false;
277 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
The type of an expression, extends irept.
Definition: type.h:27
Boolean negation.
Definition: std_expr.h:3308
exprt & true_case()
Definition: std_expr.h:3455
bool is_not_nil() const
Definition: irep.h:173
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:206
Symbol table entry.
exprt & op0()
Definition: expr.h:84
Operator to update elements in structs and arrays.
Definition: std_expr.h:3707
const exprt & op() const
Definition: std_expr.h:371
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:153
Deprecated expression utility functions.
#define forall_expr(it, expr)
Definition: expr.h:31
exprt::operandst & designator()
Definition: std_expr.h:3743
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
const componentst & components() const
Definition: std_types.h:205
The trinary if-then-else operator.
Definition: std_expr.h:3427
exprt & cond()
Definition: std_expr.h:3445
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
subtypest & subtypes()
Definition: type.h:191
exprt & new_value()
Definition: std_expr.h:3552
typet & type()
Return the type of the expression.
Definition: expr.h:68
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: std_expr.h:3282
The Boolean type.
Definition: std_types.h:28
depth_iteratort depth_begin()
Definition: expr.cpp:282
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470
Forward depth-first search iterators These iterators&#39; copy operations are expensive, so use auto&, and avoid std::next(), std::prev() and post-increment iterator.
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
Definition: expr_util.cpp:23
const exprt & compound() const
Definition: std_expr.h:3942
const irep_idt & id() const
Definition: irep.h:259
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:229
The Boolean constant true.
Definition: std_expr.h:4443
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:98
A base class for binary expressions.
Definition: std_expr.h:738
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Definition: expr_util.cpp:256
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:139
API to expression classes.
exprt & op1()
Definition: expr.h:87
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
with_exprt make_with_expr(const update_exprt &src)
converts an update expr into a (possibly nested) with expression
Definition: expr_util.cpp:67
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:3959
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:3627
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
exprt & false_case()
Definition: std_expr.h:3465
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:219
const exprt & index() const
Definition: std_expr.h:3610
The Boolean constant false.
Definition: std_expr.h:4452
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
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:737
std::vector< exprt > operandst
Definition: expr.h:57
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:3569
exprt & index()
Definition: std_expr.h:1631
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:199
Base class for all expressions.
Definition: expr.h:54
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Definition: std_types.h:260
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
const source_locationt & source_location() const
Definition: expr.h:228
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:3328
void swap(irept &irep)
Definition: irep.h:303
depth_iteratort depth_end()
Definition: expr.cpp:284
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:810
exprt & where()
Definition: std_expr.h:3542
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
#define stack(x)
Definition: parser.h:144
exprt & array()
Definition: std_expr.h:1621
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
Definition: expr_util.cpp:127
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:36
Array index operator.
Definition: std_expr.h:1595