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 "expr.h"
13 #include "fixedbv.h"
14 #include "ieee_float.h"
15 #include "std_expr.h"
16 #include "symbol.h"
17 #include "namespace.h"
18 #include "arith_tools.h"
19 
21 {
22  Forall_operands(it, expr)
23  make_next_state(*it);
24 
25  if(expr.id()==ID_symbol)
26  expr.id(ID_next_symbol);
27 }
28 
29 exprt make_binary(const exprt &expr)
30 {
31  const exprt::operandst &operands=expr.operands();
32 
33  if(operands.size()<=2)
34  return expr;
35 
36  // types must be identical for make_binary to be safe to use
37  const typet &type=expr.type();
38 
39  exprt previous=operands.front();
40  PRECONDITION(previous.type()==type);
41 
42  for(exprt::operandst::const_iterator
43  it=++operands.begin();
44  it!=operands.end();
45  ++it)
46  {
47  PRECONDITION(it->type()==type);
48 
49  exprt tmp=expr;
50  tmp.operands().clear();
51  tmp.operands().resize(2);
52  tmp.op0().swap(previous);
53  tmp.op1()=*it;
54  previous.swap(tmp);
55  }
56 
57  return previous;
58 }
59 
61 {
62  const exprt::operandst &designator=src.designator();
63  PRECONDITION(!designator.empty());
64 
65  with_exprt result;
66  exprt *dest=&result;
67 
68  forall_expr(it, designator)
69  {
70  with_exprt tmp;
71 
72  if(it->id()==ID_index_designator)
73  {
74  tmp.where()=to_index_designator(*it).index();
75  }
76  else if(it->id()==ID_member_designator)
77  {
78  // irep_idt component_name=
79  // to_member_designator(*it).get_component_name();
80  }
81  else
83 
84  *dest=tmp;
85  dest=&to_with_expr(*dest).new_value();
86  }
87 
88  return result;
89 }
90 
92  const exprt &src,
93  const namespacet &ns)
94 {
95  // We frequently need to check if a numerical type is not zero.
96  // We replace (_Bool)x by x!=0; use ieee_float_notequal for floats.
97  // Note that this returns a proper bool_typet(), not a C/C++ boolean.
98  // To get a C/C++ boolean, add a further typecast.
99 
100  const typet &src_type=
101  src.type().id()==ID_c_enum_tag?
103  ns.follow(src.type());
104 
105  if(src_type.id()==ID_bool) // already there
106  return src; // do nothing
107 
108  irep_idt id=
109  src_type.id()==ID_floatbv?ID_ieee_float_notequal:ID_notequal;
110 
111  exprt zero=from_integer(0, src_type);
112  CHECK_RETURN(zero.is_not_nil());
113 
114  binary_exprt comparison(src, id, zero, bool_typet());
115  comparison.add_source_location()=src.source_location();
116 
117  return comparison;
118 }
119 
121 {
122  if(src.id()==ID_not && src.operands().size()==1)
123  return src.op0();
124  else if(src.is_true())
125  return false_exprt();
126  else if(src.is_false())
127  return true_exprt();
128  else
129  return not_exprt(src);
130 }
131 
132 bool has_subexpr(const exprt &src, const irep_idt &id)
133 {
134  if(src.id()==id)
135  return true;
136 
137  forall_operands(it, src)
138  if(has_subexpr(*it, id))
139  return true;
140 
141  return false;
142 }
143 
144 if_exprt lift_if(const exprt &src, std::size_t operand_number)
145 {
146  PRECONDITION(operand_number<src.operands().size());
147  PRECONDITION(src.operands()[operand_number].id()==ID_if);
148 
149  const if_exprt if_expr=to_if_expr(src.operands()[operand_number]);
150  const exprt true_case=if_expr.true_case();
151  const exprt false_case=if_expr.false_case();
152 
153  if_exprt result;
154  result.cond()=if_expr.cond();
155  result.type()=src.type();
156  result.true_case()=src;
157  result.true_case().operands()[operand_number]=true_case;
158  result.false_case()=src;
159  result.false_case().operands()[operand_number]=false_case;
160 
161  return result;
162 }
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
Definition: std_expr.h:2919
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
Boolean negation.
Definition: std_expr.h:2648
exprt & true_case()
Definition: std_expr.h:2805
bool is_not_nil() const
Definition: irep.h:104
Symbol table entry.
exprt & op0()
Definition: expr.h:84
Operator to update elements in structs and arrays.
Definition: std_expr.h:3039
Deprecated expression utility functions.
#define forall_expr(it, expr)
Definition: expr.h:28
exprt::operandst & designator()
Definition: std_expr.h:3077
bool is_false() const
Definition: expr.cpp:140
The trinary if-then-else operator.
Definition: std_expr.h:2771
exprt & cond()
Definition: std_expr.h:2795
bool is_true() const
Definition: expr.cpp:133
exprt & new_value()
Definition: std_expr.h:2898
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:240
const typet & follow_tag(const union_tag_typet &src) const
Definition: namespace.cpp:83
const irep_idt & id() const
Definition: irep.h:189
The boolean constant true.
Definition: std_expr.h:3742
void make_next_state(exprt &expr)
Definition: expr_util.cpp:20
exprt is_not_zero(const exprt &src, const namespacet &ns)
converts a scalar/float expression to C/C++ Booleans
Definition: expr_util.cpp:91
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:717
A generic base class for binary expressions.
Definition: std_expr.h:471
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
API to expression classes.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
with_exprt make_with_expr(const update_exprt &src)
converts an update expr into a (possibly nested) with expression
Definition: expr_util.cpp:60
#define PRECONDITION(CONDITION)
Definition: invariant.h:225
#define forall_operands(it, expr)
Definition: expr.h:17
exprt & false_case()
Definition: std_expr.h:2815
const exprt & index() const
Definition: std_expr.h:2949
The boolean constant false.
Definition: std_expr.h:3753
bool has_subexpr(const exprt &src, const irep_idt &id)
returns true if the expression has a subexpression with given ID
Definition: expr_util.cpp:132
std::vector< exprt > operandst
Definition: expr.h:49
const index_designatort & to_index_designator(const exprt &expr)
Cast a generic exprt to an index_designatort.
Definition: std_expr.h:2970
if_exprt lift_if(const exprt &src, std::size_t operand_number)
lift up an if_exprt one level
Definition: expr_util.cpp:144
Base class for all expressions.
Definition: expr.h:46
Operator to update elements in structs and arrays.
Definition: std_expr.h:2861
const source_locationt & source_location() const
Definition: expr.h:142
#define UNREACHABLE
Definition: invariant.h:245
void swap(irept &irep)
Definition: irep.h:231
#define Forall_operands(it, expr)
Definition: expr.h:23
exprt & where()
Definition: std_expr.h:2888
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true ...
Definition: expr_util.cpp:120
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:29