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