cprover
adjust_float_expressions.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/cprover_prefix.h>
15 #include <util/expr_util.h>
16 #include <util/std_expr.h>
17 #include <util/symbol.h>
18 #include <util/ieee_float.h>
19 #include <util/arith_tools.h>
20 
21 #include "goto_model.h"
22 
26 static bool have_to_adjust_float_expressions(const exprt &expr)
27 {
28  if(expr.id()==ID_floatbv_plus ||
29  expr.id()==ID_floatbv_minus ||
30  expr.id()==ID_floatbv_mult ||
31  expr.id()==ID_floatbv_div ||
32  expr.id()==ID_floatbv_div ||
33  expr.id()==ID_floatbv_rem ||
34  expr.id()==ID_floatbv_typecast)
35  return false;
36 
37  const typet &type = expr.type();
38 
39  if(
40  type.id() == ID_floatbv ||
41  (type.id() == ID_complex && type.subtype().id() == ID_floatbv))
42  {
43  if(expr.id()==ID_plus || expr.id()==ID_minus ||
44  expr.id()==ID_mult || expr.id()==ID_div ||
45  expr.id()==ID_rem)
46  return true;
47  }
48 
49  if(expr.id()==ID_typecast)
50  {
51  const typecast_exprt &typecast_expr=to_typecast_expr(expr);
52 
53  const typet &src_type=typecast_expr.op().type();
54  const typet &dest_type=typecast_expr.type();
55 
56  if(dest_type.id()==ID_floatbv &&
57  src_type.id()==ID_floatbv)
58  return true;
59  else if(
60  dest_type.id() == ID_floatbv &&
61  (src_type.id() == ID_c_bit_field || src_type.id() == ID_signedbv ||
62  src_type.id() == ID_unsignedbv || src_type.id() == ID_c_enum_tag))
63  return true;
64  else if(
65  (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
66  dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
67  src_type.id() == ID_floatbv)
68  return true;
69  }
70 
71  forall_operands(it, expr)
73  return true;
74 
75  return false;
76 }
77 
78 void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
79 {
81  return;
82 
83  // recursive call
84  // Note that we do the recursion twice here; once in
85  // `have_to_adjust_float_expressions` and once here. Presumably this is to
86  // avoid breaking sharing (calling the non-const operands() function breaks
87  // sharing)
88  for(auto &op : expr.operands())
89  adjust_float_expressions(op, rounding_mode);
90 
91  const typet &type = expr.type();
92 
93  if(
94  type.id() == ID_floatbv ||
95  (type.id() == ID_complex && type.subtype().id() == ID_floatbv))
96  {
97  if(expr.id()==ID_plus || expr.id()==ID_minus ||
98  expr.id()==ID_mult || expr.id()==ID_div ||
99  expr.id()==ID_rem)
100  {
102  expr.operands().size() >= 2,
103  "arithmetic operations must have two or more operands");
104 
105  // make sure we have binary expressions
106  if(expr.operands().size()>2)
107  {
108  expr=make_binary(expr);
109  CHECK_RETURN(expr.operands().size() == 2);
110  }
111 
112  // now add rounding mode
113  expr.id(expr.id()==ID_plus?ID_floatbv_plus:
114  expr.id()==ID_minus?ID_floatbv_minus:
115  expr.id()==ID_mult?ID_floatbv_mult:
116  expr.id()==ID_div?ID_floatbv_div:
117  expr.id()==ID_rem?ID_floatbv_rem:
118  irep_idt());
119 
120  expr.operands().resize(3);
121  to_ieee_float_op_expr(expr).rounding_mode() = rounding_mode;
122  }
123  }
124 
125  if(expr.id()==ID_typecast)
126  {
127  const typecast_exprt &typecast_expr=to_typecast_expr(expr);
128 
129  const typet &src_type=typecast_expr.op().type();
130  const typet &dest_type=typecast_expr.type();
131 
132  if(dest_type.id()==ID_floatbv &&
133  src_type.id()==ID_floatbv)
134  {
135  // Casts from bigger to smaller float-type might round.
136  // For smaller to bigger it is strictly redundant but
137  // we leave this optimisation until later to simplify
138  // the representation.
139  expr.id(ID_floatbv_typecast);
140  expr.operands().resize(2);
141  to_floatbv_typecast_expr(expr).rounding_mode() = rounding_mode;
142  }
143  else if(
144  dest_type.id() == ID_floatbv &&
145  (src_type.id() == ID_signedbv || src_type.id() == ID_unsignedbv ||
146  src_type.id() == ID_c_enum_tag || src_type.id() == ID_c_bit_field))
147  {
148  // casts from integer to float-type might round
149  expr.id(ID_floatbv_typecast);
150  expr.operands().resize(2);
151  to_floatbv_typecast_expr(expr).rounding_mode() = rounding_mode;
152  }
153  else if(
154  dest_type.id() == ID_floatbv &&
155  (src_type.id() == ID_c_bool || src_type.id() == ID_bool))
156  {
157  // casts from bool or c_bool to float-type do not need rounding
158  }
159  else if(
160  (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
161  dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
162  src_type.id() == ID_floatbv)
163  {
164  // In C, casts from float to integer always round to zero,
165  // irrespectively of the rounding mode that is currently set.
166  // We will have to consider other programming languages
167  // eventually.
168 
169  /* ISO 9899:1999
170  * 6.3.1.4 Real floating and integer
171  * 1 When a finite value of real floating type is converted
172  * to an integer type other than _Bool, the fractional part
173  * is discarded (i.e., the value is truncated toward zero).
174  */
175  expr.id(ID_floatbv_typecast);
176  expr.operands().resize(2);
178  from_integer(ieee_floatt::ROUND_TO_ZERO, rounding_mode.type());
179  }
180  }
181 }
182 
184 {
186  return;
187 
188  symbol_exprt rounding_mode =
189  ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
190 
191  rounding_mode.add_source_location() = expr.source_location();
192 
193  adjust_float_expressions(expr, rounding_mode);
194 }
195 
197  goto_functionst::goto_functiont &goto_function,
198  const namespacet &ns)
199 {
200  for(auto &i : goto_function.body.instructions)
201  i.transform([&ns](exprt expr) -> optionalt<exprt> {
203  {
204  adjust_float_expressions(expr, ns);
205  return expr;
206  }
207  else
208  return {};
209  });
210 }
211 
214  const namespacet &ns)
215 {
217  adjust_float_expressions(it->second, ns);
218 }
219 
221 {
222  namespacet ns(goto_model.symbol_table);
224 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
make_binary
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition: expr_util.cpp:36
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
to_ieee_float_op_expr
const ieee_float_op_exprt & to_ieee_float_op_expr(const exprt &expr)
Cast an exprt to an ieee_float_op_exprt.
Definition: std_expr.h:3851
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:418
have_to_adjust_float_expressions
static bool have_to_adjust_float_expressions(const exprt &expr)
Iterate over an expression and check it or any of its subexpressions are floating point operations th...
Definition: adjust_float_expressions.cpp:26
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
cprover_prefix.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
Forall_goto_functions
#define Forall_goto_functions(it, functions)
Definition: goto_functions.h:117
goto_functionst::goto_functiont
::goto_functiont goto_functiont
Definition: goto_functions.h:25
expr_util.h
Deprecated expression utility functions.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
ieee_float_op_exprt::rounding_mode
exprt & rounding_mode()
Definition: std_expr.h:3821
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
floatbv_typecast_exprt::rounding_mode
exprt & rounding_mode()
Definition: std_expr.h:2088
to_floatbv_typecast_expr
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast an exprt to a floatbv_typecast_exprt.
Definition: std_expr.h:2116
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
to_typecast_expr
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2047
ieee_float.h
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
adjust_float_expressions
void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
Replaces arithmetic operations and typecasts involving floating point numbers with their equivalent f...
Definition: adjust_float_expressions.cpp:78
exprt::operands
operandst & operands()
Definition: expr.h:95
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:259
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
adjust_float_expressions.h
Symbolic Execution.
std_expr.h
API to expression classes.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
ieee_floatt::ROUND_TO_ZERO
@ ROUND_TO_ZERO
Definition: ieee_float.h:128