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 "c_types.h"
16 #include "expr_iterator.h"
17 #include "namespace.h"
18 #include "pointer_expr.h"
19 #include "std_expr.h"
20 
21 bool is_lvalue(const exprt &expr)
22 {
23  if(expr.id() == ID_index)
24  return is_lvalue(to_index_expr(expr).array());
25  else if(expr.id() == ID_member)
26  return is_lvalue(to_member_expr(expr).compound());
27  else if(expr.id() == ID_dereference)
28  return true;
29  else if(expr.id() == ID_symbol)
30  return true;
31  else
32  return false;
33 }
34 exprt make_binary(const exprt &expr)
35 {
36  const exprt::operandst &operands=expr.operands();
37 
38  if(operands.size()<=2)
39  return expr;
40 
41  // types must be identical for make_binary to be safe to use
42  const typet &type=expr.type();
43 
44  exprt previous=operands.front();
45  PRECONDITION(previous.type()==type);
46 
47  for(exprt::operandst::const_iterator
48  it=++operands.begin();
49  it!=operands.end();
50  ++it)
51  {
52  PRECONDITION(it->type()==type);
53 
54  exprt tmp=expr;
55  tmp.operands().clear();
56  tmp.operands().resize(2);
57  to_binary_expr(tmp).op0().swap(previous);
58  to_binary_expr(tmp).op1() = *it;
59  previous.swap(tmp);
60  }
61 
62  return previous;
63 }
64 
66 {
67  const exprt::operandst &designator=src.designator();
68  PRECONDITION(!designator.empty());
69 
70  with_exprt result{exprt{}, exprt{}, exprt{}};
71  exprt *dest=&result;
72 
73  for(const auto &expr : designator)
74  {
75  with_exprt tmp{exprt{}, exprt{}, exprt{}};
76 
77  if(expr.id() == ID_index_designator)
78  {
79  tmp.where() = to_index_designator(expr).index();
80  }
81  else if(expr.id() == ID_member_designator)
82  {
83  // irep_idt component_name=
84  // to_member_designator(*it).get_component_name();
85  }
86  else
88 
89  *dest=tmp;
90  dest=&to_with_expr(*dest).new_value();
91  }
92 
93  return result;
94 }
95 
97  const exprt &src,
98  const namespacet &ns)
99 {
100  // We frequently need to check if a numerical type is not zero.
101  // We replace (_Bool)x by x!=0; use ieee_float_notequal for floats.
102  // Note that this returns a proper bool_typet(), not a C/C++ boolean.
103  // To get a C/C++ boolean, add a further typecast.
104 
105  const typet &src_type = src.type().id() == ID_c_enum_tag
106  ? ns.follow_tag(to_c_enum_tag_type(src.type()))
107  : src.type();
108 
109  if(src_type.id()==ID_bool) // already there
110  return src; // do nothing
111 
112  irep_idt id=
113  src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
114 
115  exprt zero=from_integer(0, src_type);
116  // Use tag type if applicable:
117  zero.type() = src.type();
118 
119  binary_relation_exprt comparison(src, id, std::move(zero));
120  comparison.add_source_location()=src.source_location();
121 
122  return std::move(comparison);
123 }
124 
126 {
127  if(src.id() == ID_not)
128  return to_not_expr(src).op();
129  else if(src.is_true())
130  return false_exprt();
131  else if(src.is_false())
132  return true_exprt();
133  else
134  return not_exprt(src);
135 }
136 
138  const exprt &expr,
139  const std::function<bool(const exprt &)> &pred)
140 {
141  const auto it = std::find_if(expr.depth_begin(), expr.depth_end(), pred);
142  return it != expr.depth_end();
143 }
144 
145 bool has_subexpr(const exprt &src, const irep_idt &id)
146 {
147  return has_subexpr(
148  src, [&](const exprt &subexpr) { return subexpr.id() == id; });
149 }
150 
152  const typet &type,
153  const std::function<bool(const typet &)> &pred,
154  const namespacet &ns)
155 {
156  std::vector<std::reference_wrapper<const typet>> stack;
157  std::unordered_set<typet, irep_hash> visited;
158 
159  const auto push_if_not_visited = [&](const typet &t) {
160  if(visited.insert(t).second)
161  stack.emplace_back(t);
162  };
163 
164  push_if_not_visited(type);
165  while(!stack.empty())
166  {
167  const typet &top = stack.back().get();
168  stack.pop_back();
169 
170  if(pred(top))
171  return true;
172  else if(top.id() == ID_c_enum_tag)
173  push_if_not_visited(ns.follow_tag(to_c_enum_tag_type(top)));
174  else if(top.id() == ID_struct_tag)
175  push_if_not_visited(ns.follow_tag(to_struct_tag_type(top)));
176  else if(top.id() == ID_union_tag)
177  push_if_not_visited(ns.follow_tag(to_union_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(if_expr.cond(), src, src);
209  result.true_case().operands()[operand_number]=true_case;
210  result.false_case().operands()[operand_number]=false_case;
211 
212  return result;
213 }
214 
215 const exprt &skip_typecast(const exprt &expr)
216 {
217  if(expr.id()!=ID_typecast)
218  return expr;
219 
220  return skip_typecast(to_typecast_expr(expr).op());
221 }
222 
225 bool is_constantt::is_constant(const exprt &expr) const
226 {
227  if(expr.is_constant())
228  return true;
229 
230  if(expr.id() == ID_address_of)
231  {
232  return is_constant_address_of(to_address_of_expr(expr).object());
233  }
234  else if(
235  expr.id() == ID_typecast || expr.id() == ID_array_of ||
236  expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array ||
237  expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
238  // byte_update works, byte_extract may be out-of-bounds
239  expr.id() == ID_byte_update_big_endian ||
240  expr.id() == ID_byte_update_little_endian)
241  {
242  return std::all_of(
243  expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
244  return is_constant(e);
245  });
246  }
247 
248  return false;
249 }
250 
253 {
254  if(expr.id() == ID_symbol)
255  {
256  return true;
257  }
258  else if(expr.id() == ID_index)
259  {
260  const index_exprt &index_expr = to_index_expr(expr);
261 
262  return is_constant_address_of(index_expr.array()) &&
263  is_constant(index_expr.index());
264  }
265  else if(expr.id() == ID_member)
266  {
267  return is_constant_address_of(to_member_expr(expr).compound());
268  }
269  else if(expr.id() == ID_dereference)
270  {
271  const dereference_exprt &deref = to_dereference_expr(expr);
272 
273  return is_constant(deref.pointer());
274  }
275  else if(expr.id() == ID_string_constant)
276  return true;
277 
278  return false;
279 }
280 
282 {
283  if(value)
284  return true_exprt();
285  else
286  return false_exprt();
287 }
288 
290 {
291  PRECONDITION(a.type().id() == ID_bool && b.type().id() == ID_bool);
292  if(b.is_constant())
293  {
294  if(b.get(ID_value) == ID_false)
295  return false_exprt{};
296  return a;
297  }
298  if(a.is_constant())
299  {
300  if(a.get(ID_value) == ID_false)
301  return false_exprt{};
302  return b;
303  }
304  if(b.id() == ID_and)
305  {
306  b.add_to_operands(std::move(a));
307  return b;
308  }
309  return and_exprt{std::move(a), std::move(b)};
310 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
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:317
Boolean AND.
Definition: std_expr.h:1920
exprt & op1()
Definition: expr.h:102
exprt & op0()
Definition: expr.h:99
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
A constant literal expression.
Definition: std_expr.h:2753
Operator to dereference a pointer.
Definition: pointer_expr.h:628
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
depth_iteratort depth_end()
Definition: expr.cpp:267
source_locationt & add_source_location()
Definition: expr.h:235
depth_iteratort depth_begin()
Definition: expr.cpp:265
const source_locationt & source_location() const
Definition: expr.h:230
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:42
typet & type()
Return the type of the expression.
Definition: expr.h:82
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:26
operandst & operands()
Definition: expr.h:92
void add_to_operands(const exprt &expr)
Add the given argument to the end of exprt's operands.
Definition: expr.h:136
The Boolean constant false.
Definition: std_expr.h:2811
The trinary if-then-else operator.
Definition: std_expr.h:2172
exprt & true_case()
Definition: std_expr.h:2199
exprt & false_case()
Definition: std_expr.h:2209
exprt & cond()
Definition: std_expr.h:2189
const exprt & index() const
Definition: std_expr.h:2345
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1344
exprt & index()
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:407
void swap(irept &irep)
Definition: irep.h:453
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:225
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Definition: expr_util.cpp:252
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:91
Boolean negation.
Definition: std_expr.h:2127
The Boolean constant true.
Definition: std_expr.h:2802
The type of an expression, extends irept.
Definition: type.h:28
const exprt & op() const
Definition: std_expr.h:293
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
exprt::operandst & designator()
Definition: std_expr.h:2468
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
exprt & new_value()
Definition: std_expr.h:2288
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:281
with_exprt make_with_expr(const update_exprt &src)
converts an update expr into a (possibly nested) with expression
Definition: expr_util.cpp:65
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:96
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:34
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:215
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:137
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:199
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:289
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:125
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:151
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
Definition: expr_util.cpp:21
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:684
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:378
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
API to expression classes.
const index_designatort & to_index_designator(const exprt &expr)
Cast an exprt to an index_designatort.
Definition: std_expr.h:2373
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2237
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2152
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2320
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
Definition: std_expr.h:627
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
Definition: std_expr.h:2697
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
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:474
const type_with_subtypest & to_type_with_subtypes(const typet &type)
Definition: type.h:198