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 exprt make_binary(const exprt &expr)
23 {
24  const exprt::operandst &operands=expr.operands();
25 
26  if(operands.size()<=2)
27  return expr;
28 
29  // types must be identical for make_binary to be safe to use
30  const typet &type=expr.type();
31 
32  exprt previous=operands.front();
33  PRECONDITION(previous.type()==type);
34 
35  for(exprt::operandst::const_iterator
36  it=++operands.begin();
37  it!=operands.end();
38  ++it)
39  {
40  PRECONDITION(it->type()==type);
41 
42  exprt tmp=expr;
43  tmp.operands().clear();
44  tmp.operands().resize(2);
45  tmp.op0().swap(previous);
46  tmp.op1()=*it;
47  previous.swap(tmp);
48  }
49 
50  return previous;
51 }
52 
54 {
55  const exprt::operandst &designator=src.designator();
56  PRECONDITION(!designator.empty());
57 
58  with_exprt result;
59  exprt *dest=&result;
60 
61  forall_expr(it, designator)
62  {
63  with_exprt tmp;
64 
65  if(it->id()==ID_index_designator)
66  {
67  tmp.where()=to_index_designator(*it).index();
68  }
69  else if(it->id()==ID_member_designator)
70  {
71  // irep_idt component_name=
72  // to_member_designator(*it).get_component_name();
73  }
74  else
76 
77  *dest=tmp;
78  dest=&to_with_expr(*dest).new_value();
79  }
80 
81  return result;
82 }
83 
85  const exprt &src,
86  const namespacet &ns)
87 {
88  // We frequently need to check if a numerical type is not zero.
89  // We replace (_Bool)x by x!=0; use ieee_float_notequal for floats.
90  // Note that this returns a proper bool_typet(), not a C/C++ boolean.
91  // To get a C/C++ boolean, add a further typecast.
92 
93  const typet &src_type=
94  src.type().id()==ID_c_enum_tag?
96  ns.follow(src.type());
97 
98  if(src_type.id()==ID_bool) // already there
99  return src; // do nothing
100 
101  irep_idt id=
102  src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
103 
104  exprt zero=from_integer(0, src_type);
105  CHECK_RETURN(zero.is_not_nil());
106 
107  binary_exprt comparison(src, id, zero, bool_typet());
108  comparison.add_source_location()=src.source_location();
109 
110  return comparison;
111 }
112 
114 {
115  if(src.id()==ID_not && src.operands().size()==1)
116  return src.op0();
117  else if(src.is_true())
118  return false_exprt();
119  else if(src.is_false())
120  return true_exprt();
121  else
122  return not_exprt(src);
123 }
124 
126  const exprt &expr,
127  const std::function<bool(const exprt &)> &pred)
128 {
129  const auto it = std::find_if(expr.depth_begin(), expr.depth_end(), pred);
130  return it != expr.depth_end();
131 }
132 
133 bool has_subexpr(const exprt &src, const irep_idt &id)
134 {
135  return has_subexpr(
136  src, [&](const exprt &subexpr) { return subexpr.id() == id; });
137 }
138 
140  const typet &type,
141  const std::function<bool(const typet &)> &pred,
142  const namespacet &ns)
143 {
144  std::vector<std::reference_wrapper<const typet>> stack;
145  std::unordered_set<typet, irep_hash> visited;
146 
147  const auto push_if_not_visited = [&](const typet &t) {
148  if(visited.insert(t).second)
149  stack.emplace_back(t);
150  };
151 
152  push_if_not_visited(type);
153  while(!stack.empty())
154  {
155  const typet &top = stack.back().get();
156  stack.pop_back();
157 
158  if(pred(top))
159  return true;
160  else if(top.id() == ID_symbol)
161  push_if_not_visited(ns.follow(top));
162  else if(top.id() == ID_c_enum_tag)
163  push_if_not_visited(ns.follow_tag(to_c_enum_tag_type(top)));
164  else if(top.id() == ID_struct || top.id() == ID_union)
165  {
166  for(const auto &comp : to_struct_union_type(top).components())
167  push_if_not_visited(comp.type());
168  }
169  else
170  {
171  for(const auto &subtype : top.subtypes())
172  push_if_not_visited(subtype);
173  }
174  }
175 
176  return false;
177 }
178 
179 bool has_subtype(const typet &type, const irep_idt &id, const namespacet &ns)
180 {
181  return has_subtype(
182  type, [&](const typet &subtype) { return subtype.id() == id; }, ns);
183 }
184 
185 if_exprt lift_if(const exprt &src, std::size_t operand_number)
186 {
187  PRECONDITION(operand_number<src.operands().size());
188  PRECONDITION(src.operands()[operand_number].id()==ID_if);
189 
190  const if_exprt if_expr=to_if_expr(src.operands()[operand_number]);
191  const exprt true_case=if_expr.true_case();
192  const exprt false_case=if_expr.false_case();
193 
194  if_exprt result;
195  result.cond()=if_expr.cond();
196  result.type()=src.type();
197  result.true_case()=src;
198  result.true_case().operands()[operand_number]=true_case;
199  result.false_case()=src;
200  result.false_case().operands()[operand_number]=false_case;
201 
202  return result;
203 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
The type of an expression.
Definition: type.h:22
Boolean negation.
Definition: std_expr.h:3230
exprt & true_case()
Definition: std_expr.h:3395
bool is_not_nil() const
Definition: irep.h:103
Symbol table entry.
exprt & op0()
Definition: expr.h:72
Operator to update elements in structs and arrays.
Definition: std_expr.h:3672
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:139
Deprecated expression utility functions.
#define forall_expr(it, expr)
Definition: expr.h:28
exprt::operandst & designator()
Definition: std_expr.h:3710
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:3361
exprt & cond()
Definition: std_expr.h:3385
bool is_true() const
Definition: expr.cpp:124
exprt & new_value()
Definition: std_expr.h:3498
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:245
const typet & follow_tag(const union_tag_typet &) const
Definition: namespace.cpp:74
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:4488
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:84
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:125
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:53
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
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:3583
exprt & false_case()
Definition: std_expr.h:3405
const exprt & index() const
Definition: std_expr.h:3562
The boolean constant false.
Definition: std_expr.h:4499
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:3519
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:185
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:3461
const source_locationt & source_location() const
Definition: expr.h:125
#define UNREACHABLE
Definition: invariant.h:250
void swap(irept &irep)
Definition: irep.h:231
depth_iteratort depth_end()
Definition: expr.cpp:301
exprt & where()
Definition: std_expr.h:3488
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 boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
Definition: expr_util.cpp:113
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:22