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_assignable(const exprt &expr)
22 {
23  if(expr.id() == ID_index)
24  return is_assignable(to_index_expr(expr).array());
25  else if(expr.id() == ID_member)
26  return is_assignable(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 
35 exprt make_binary(const exprt &expr)
36 {
37  const exprt::operandst &operands=expr.operands();
38 
39  if(operands.size()<=2)
40  return expr;
41 
42  // types must be identical for make_binary to be safe to use
43  const typet &type=expr.type();
44 
45  exprt previous=operands.front();
46  PRECONDITION(previous.type()==type);
47 
48  for(exprt::operandst::const_iterator
49  it=++operands.begin();
50  it!=operands.end();
51  ++it)
52  {
53  PRECONDITION(it->type()==type);
54 
55  exprt tmp=expr;
56  tmp.operands().clear();
57  tmp.operands().resize(2);
58  to_binary_expr(tmp).op0().swap(previous);
59  to_binary_expr(tmp).op1() = *it;
60  previous.swap(tmp);
61  }
62 
63  return previous;
64 }
65 
67 {
68  const exprt::operandst &designator=src.designator();
69  PRECONDITION(!designator.empty());
70 
71  with_exprt result{exprt{}, exprt{}, exprt{}};
72  exprt *dest=&result;
73 
74  for(const auto &expr : designator)
75  {
76  with_exprt tmp{exprt{}, exprt{}, exprt{}};
77 
78  if(expr.id() == ID_index_designator)
79  {
80  tmp.where() = to_index_designator(expr).index();
81  }
82  else if(expr.id() == ID_member_designator)
83  {
84  // irep_idt component_name=
85  // to_member_designator(*it).get_component_name();
86  }
87  else
89 
90  *dest=tmp;
91  dest=&to_with_expr(*dest).new_value();
92  }
93 
94  return result;
95 }
96 
98  const exprt &src,
99  const namespacet &ns)
100 {
101  // We frequently need to check if a numerical type is not zero.
102  // We replace (_Bool)x by x!=0; use ieee_float_notequal for floats.
103  // Note that this returns a proper bool_typet(), not a C/C++ boolean.
104  // To get a C/C++ boolean, add a further typecast.
105 
106  const typet &src_type = src.type().id() == ID_c_enum_tag
107  ? ns.follow_tag(to_c_enum_tag_type(src.type()))
108  : src.type();
109 
110  if(src_type.id()==ID_bool) // already there
111  return src; // do nothing
112 
113  irep_idt id=
114  src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
115 
116  exprt zero=from_integer(0, src_type);
117  // Use tag type if applicable:
118  zero.type() = src.type();
119 
120  binary_relation_exprt comparison(src, id, std::move(zero));
121  comparison.add_source_location()=src.source_location();
122 
123  return std::move(comparison);
124 }
125 
127 {
128  if(src.id() == ID_not)
129  return to_not_expr(src).op();
130  else if(src.is_true())
131  return false_exprt();
132  else if(src.is_false())
133  return true_exprt();
134  else
135  return not_exprt(src);
136 }
137 
139  const exprt &expr,
140  const std::function<bool(const exprt &)> &pred)
141 {
142  const auto it = std::find_if(expr.depth_begin(), expr.depth_end(), pred);
143  return it != expr.depth_end();
144 }
145 
146 bool has_subexpr(const exprt &src, const irep_idt &id)
147 {
148  return has_subexpr(
149  src, [&](const exprt &subexpr) { return subexpr.id() == id; });
150 }
151 
153  const typet &type,
154  const std::function<bool(const typet &)> &pred,
155  const namespacet &ns)
156 {
157  std::vector<std::reference_wrapper<const typet>> stack;
158  std::unordered_set<typet, irep_hash> visited;
159 
160  const auto push_if_not_visited = [&](const typet &t) {
161  if(visited.insert(t).second)
162  stack.emplace_back(t);
163  };
164 
165  push_if_not_visited(type);
166  while(!stack.empty())
167  {
168  const typet &top = stack.back().get();
169  stack.pop_back();
170 
171  if(pred(top))
172  return true;
173  else if(top.id() == ID_c_enum_tag)
174  push_if_not_visited(ns.follow_tag(to_c_enum_tag_type(top)));
175  else if(top.id() == ID_struct_tag)
176  push_if_not_visited(ns.follow_tag(to_struct_tag_type(top)));
177  else if(top.id() == ID_union_tag)
178  push_if_not_visited(ns.follow_tag(to_union_tag_type(top)));
179  else if(top.id() == ID_struct || top.id() == ID_union)
180  {
181  for(const auto &comp : to_struct_union_type(top).components())
182  push_if_not_visited(comp.type());
183  }
184  else
185  {
186  for(const auto &subtype : to_type_with_subtypes(top).subtypes())
187  push_if_not_visited(subtype);
188  }
189  }
190 
191  return false;
192 }
193 
194 bool has_subtype(const typet &type, const irep_idt &id, const namespacet &ns)
195 {
196  return has_subtype(
197  type, [&](const typet &subtype) { return subtype.id() == id; }, ns);
198 }
199 
200 if_exprt lift_if(const exprt &src, std::size_t operand_number)
201 {
202  PRECONDITION(operand_number<src.operands().size());
203  PRECONDITION(src.operands()[operand_number].id()==ID_if);
204 
205  const if_exprt if_expr=to_if_expr(src.operands()[operand_number]);
206  const exprt true_case=if_expr.true_case();
207  const exprt false_case=if_expr.false_case();
208 
209  if_exprt result(if_expr.cond(), src, src);
210  result.true_case().operands()[operand_number]=true_case;
211  result.false_case().operands()[operand_number]=false_case;
212 
213  return result;
214 }
215 
216 const exprt &skip_typecast(const exprt &expr)
217 {
218  if(expr.id()!=ID_typecast)
219  return expr;
220 
221  return skip_typecast(to_typecast_expr(expr).op());
222 }
223 
226 bool is_constantt::is_constant(const exprt &expr) const
227 {
228  if(expr.is_constant())
229  return true;
230 
231  if(expr.id() == ID_address_of)
232  {
233  return is_constant_address_of(to_address_of_expr(expr).object());
234  }
235  else if(
236  expr.id() == ID_typecast || expr.id() == ID_array_of ||
237  expr.id() == ID_plus || expr.id() == ID_mult || expr.id() == ID_array ||
238  expr.id() == ID_with || expr.id() == ID_struct || expr.id() == ID_union ||
239  expr.id() == ID_empty_union ||
240  // byte_update works, byte_extract may be out-of-bounds
241  expr.id() == ID_byte_update_big_endian ||
242  expr.id() == ID_byte_update_little_endian)
243  {
244  return std::all_of(
245  expr.operands().begin(), expr.operands().end(), [this](const exprt &e) {
246  return is_constant(e);
247  });
248  }
249 
250  return false;
251 }
252 
255 {
256  if(expr.id() == ID_symbol)
257  {
258  return true;
259  }
260  else if(expr.id() == ID_index)
261  {
262  const index_exprt &index_expr = to_index_expr(expr);
263 
264  return is_constant_address_of(index_expr.array()) &&
265  is_constant(index_expr.index());
266  }
267  else if(expr.id() == ID_member)
268  {
269  return is_constant_address_of(to_member_expr(expr).compound());
270  }
271  else if(expr.id() == ID_dereference)
272  {
273  const dereference_exprt &deref = to_dereference_expr(expr);
274 
275  return is_constant(deref.pointer());
276  }
277  else if(expr.id() == ID_string_constant)
278  return true;
279 
280  return false;
281 }
282 
284 {
285  if(value)
286  return true_exprt();
287  else
288  return false_exprt();
289 }
290 
292 {
293  PRECONDITION(a.type().id() == ID_bool && b.type().id() == ID_bool);
294  if(b.is_constant())
295  {
296  if(b.get(ID_value) == ID_false)
297  return false_exprt{};
298  return a;
299  }
300  if(a.is_constant())
301  {
302  if(a.get(ID_value) == ID_false)
303  return false_exprt{};
304  return b;
305  }
306  if(b.id() == ID_and)
307  {
308  b.add_to_operands(std::move(a));
309  return b;
310  }
311  return and_exprt{std::move(a), std::move(b)};
312 }
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:202
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:344
Boolean AND.
Definition: std_expr.h:1974
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:2807
Operator to dereference a pointer.
Definition: pointer_expr.h:648
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:2865
The trinary if-then-else operator.
Definition: std_expr.h:2226
exprt & true_case()
Definition: std_expr.h:2253
exprt & false_case()
Definition: std_expr.h:2263
exprt & cond()
Definition: std_expr.h:2243
const exprt & index() const
Definition: std_expr.h:2399
Array index operator.
Definition: std_expr.h:1328
exprt & array()
Definition: std_expr.h:1353
exprt & index()
Definition: std_expr.h:1363
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:45
const irep_idt & id() const
Definition: irep.h:396
void swap(irept &irep)
Definition: irep.h:442
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
Definition: expr_util.cpp:226
virtual bool is_constant_address_of(const exprt &) const
this function determines which reference-typed expressions are constant
Definition: expr_util.cpp:254
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:2181
The Boolean constant true.
Definition: std_expr.h:2856
The type of an expression, extends irept.
Definition: type.h:29
const exprt & op() const
Definition: std_expr.h:293
Operator to update elements in structs and arrays.
Definition: std_expr.h:2496
exprt::operandst & designator()
Definition: std_expr.h:2522
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
exprt & new_value()
Definition: std_expr.h:2342
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:283
with_exprt make_with_expr(const update_exprt &src)
converts an update expr into a (possibly nested) with expression
Definition: expr_util.cpp:66
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:97
bool is_assignable(const exprt &expr)
Returns true iff the argument is one of the following:
Definition: expr_util.cpp:21
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:35
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:216
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:138
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:200
exprt make_and(exprt a, exprt b)
Conjunction of two expressions.
Definition: expr_util.cpp:291
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Definition: expr_util.cpp:126
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:152
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:704
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Definition: pointer_expr.h:398
#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:2427
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2291
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1954
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2206
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
Definition: std_expr.h:2374
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:2751
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1391
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:221