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 
10 #include "expr_util.h"
11 
12 #include <unordered_set>
13 #include "expr.h"
14 #include "expr_iterator.h"
15 #include "fixedbv.h"
16 #include "ieee_float.h"
17 #include "std_expr.h"
18 #include "symbol.h"
19 #include "namespace.h"
20 #include "arith_tools.h"
21 
22 bool is_lvalue(const exprt &expr)
23 {
24  if(expr.id() == ID_index)
25  return is_lvalue(to_index_expr(expr).array());
26  else if(expr.id() == ID_member)
27  return is_lvalue(to_member_expr(expr).compound());
28  else if(expr.id() == ID_dereference)
29  return true;
30  else if(expr.id() == ID_symbol)
31  return true;
32  else
33  return false;
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  tmp.op0().swap(previous);
59  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;
72  exprt *dest=&result;
73 
74  forall_expr(it, designator)
75  {
76  with_exprt tmp;
77 
78  if(it->id()==ID_index_designator)
79  {
80  tmp.where()=to_index_designator(*it).index();
81  }
82  else if(it->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=
107  src.type().id()==ID_c_enum_tag?
109  ns.follow(src.type());
110 
111  if(src_type.id()==ID_bool) // already there
112  return src; // do nothing
113 
114  irep_idt id=
115  src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
116 
117  exprt zero=from_integer(0, src_type);
118  CHECK_RETURN(zero.is_not_nil());
119 
120  binary_exprt comparison(src, id, zero, bool_typet());
121  comparison.add_source_location()=src.source_location();
122 
123  return comparison;
124 }
125 
127 {
128  if(src.id()==ID_not && src.operands().size()==1)
129  return src.op0();
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_symbol)
174  push_if_not_visited(ns.follow(top));
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 || top.id() == ID_union)
178  {
179  for(const auto &comp : to_struct_union_type(top).components())
180  push_if_not_visited(comp.type());
181  }
182  else
183  {
184  for(const auto &subtype : top.subtypes())
185  push_if_not_visited(subtype);
186  }
187  }
188 
189  return false;
190 }
191 
192 bool has_subtype(const typet &type, const irep_idt &id, const namespacet &ns)
193 {
194  return has_subtype(
195  type, [&](const typet &subtype) { return subtype.id() == id; }, ns);
196 }
197 
198 if_exprt lift_if(const exprt &src, std::size_t operand_number)
199 {
200  PRECONDITION(operand_number<src.operands().size());
201  PRECONDITION(src.operands()[operand_number].id()==ID_if);
202 
203  const if_exprt if_expr=to_if_expr(src.operands()[operand_number]);
204  const exprt true_case=if_expr.true_case();
205  const exprt false_case=if_expr.false_case();
206 
207  if_exprt result;
208  result.cond()=if_expr.cond();
209  result.type()=src.type();
210  result.true_case()=src;
211  result.true_case().operands()[operand_number]=true_case;
212  result.false_case()=src;
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 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
The type of an expression.
Definition: type.h:22
Boolean negation.
Definition: std_expr.h:3228
exprt & true_case()
Definition: std_expr.h:3393
bool is_not_nil() const
Definition: irep.h:173
Symbol table entry.
exprt & op0()
Definition: expr.h:72
Operator to update elements in structs and arrays.
Definition: std_expr.h:3670
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.
#define forall_expr(it, expr)
Definition: expr.h:28
exprt::operandst & designator()
Definition: std_expr.h:3708
subtypest & subtypes()
Definition: type.h:58
bool is_false() const
Definition: expr.cpp:131
const componentst & components() const
Definition: std_types.h:245
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & cond()
Definition: std_expr.h:3383
bool is_true() const
Definition: expr.cpp:124
exprt & new_value()
Definition: std_expr.h:3496
typet & type()
Definition: expr.h:56
The proper Booleans.
Definition: std_types.h:34
depth_iteratort depth_begin()
Definition: expr.cpp:299
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:80
bool is_lvalue(const exprt &expr)
Returns true iff the argument is (syntactically) an lvalue.
Definition: expr_util.cpp:22
const exprt & compound() const
Definition: std_expr.h:3920
const irep_idt & id() const
Definition: irep.h:259
The boolean constant true.
Definition: std_expr.h:4486
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:97
A generic base class for binary expressions.
Definition: std_expr.h:649
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
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:74
with_exprt make_with_expr(const update_exprt &src)
converts an update expr into a (possibly nested) with expression
Definition: expr_util.cpp:66
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
Definition: std_expr.h:3953
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const index_designatort & to_index_designator(const exprt &expr)
Cast a generic exprt to an index_designatort.
Definition: std_expr.h:3581
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
exprt & false_case()
Definition: std_expr.h:3403
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
Definition: expr_util.cpp:218
const exprt & index() const
Definition: std_expr.h:3560
The boolean constant false.
Definition: std_expr.h:4497
const c_enum_tag_typet & to_c_enum_tag_type(const typet &type)
Cast a generic typet to a c_enum_tag_typet.
Definition: std_types.h:747
std::vector< exprt > operandst
Definition: expr.h:45
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
Definition: std_expr.h:3517
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:198
Base class for all expressions.
Definition: expr.h:42
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
Definition: std_types.h:280
Operator to update elements in structs and arrays.
Definition: std_expr.h:3459
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:271
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
void swap(irept &irep)
Definition: irep.h:303
depth_iteratort depth_end()
Definition: expr.cpp:301
exprt & where()
Definition: std_expr.h:3486
operandst & operands()
Definition: expr.h:66
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:1486
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
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:35