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 
25 {
26  return CPROVER_PREFIX "rounding_mode";
27 }
28 
32 static bool have_to_adjust_float_expressions(const exprt &expr)
33 {
34  if(expr.id()==ID_floatbv_plus ||
35  expr.id()==ID_floatbv_minus ||
36  expr.id()==ID_floatbv_mult ||
37  expr.id()==ID_floatbv_div ||
38  expr.id()==ID_floatbv_div ||
39  expr.id()==ID_floatbv_rem ||
40  expr.id()==ID_floatbv_typecast)
41  return false;
42 
43  const typet &type = expr.type();
44 
45  if(
46  type.id() == ID_floatbv ||
47  (type.id() == ID_complex && type.subtype().id() == ID_floatbv))
48  {
49  if(
50  expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
51  expr.id() == ID_div)
52  return true;
53  }
54 
55  if(expr.id()==ID_typecast)
56  {
57  const typecast_exprt &typecast_expr=to_typecast_expr(expr);
58 
59  const typet &src_type=typecast_expr.op().type();
60  const typet &dest_type=typecast_expr.type();
61 
62  if(dest_type.id()==ID_floatbv &&
63  src_type.id()==ID_floatbv)
64  return true;
65  else if(
66  dest_type.id() == ID_floatbv &&
67  (src_type.id() == ID_c_bit_field || src_type.id() == ID_signedbv ||
68  src_type.id() == ID_unsignedbv || src_type.id() == ID_c_enum_tag))
69  return true;
70  else if(
71  (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
72  dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
73  src_type.id() == ID_floatbv)
74  return true;
75  }
76 
77  forall_operands(it, expr)
79  return true;
80 
81  return false;
82 }
83 
84 void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
85 {
87  return;
88 
89  // recursive call
90  // Note that we do the recursion twice here; once in
91  // `have_to_adjust_float_expressions` and once here. Presumably this is to
92  // avoid breaking sharing (calling the non-const operands() function breaks
93  // sharing)
94  for(auto &op : expr.operands())
95  adjust_float_expressions(op, rounding_mode);
96 
97  const typet &type = expr.type();
98 
99  if(
100  type.id() == ID_floatbv ||
101  (type.id() == ID_complex && type.subtype().id() == ID_floatbv))
102  {
103  if(
104  expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
105  expr.id() == ID_div)
106  {
108  expr.operands().size() >= 2,
109  "arithmetic operations must have two or more operands");
110 
111  // make sure we have binary expressions
112  if(expr.operands().size()>2)
113  {
114  expr=make_binary(expr);
115  CHECK_RETURN(expr.operands().size() == 2);
116  }
117 
118  // now add rounding mode
119  expr.id(expr.id()==ID_plus?ID_floatbv_plus:
120  expr.id()==ID_minus?ID_floatbv_minus:
121  expr.id()==ID_mult?ID_floatbv_mult:
122  expr.id()==ID_div?ID_floatbv_div:
123  irep_idt());
124 
125  expr.operands().resize(3);
126  to_ieee_float_op_expr(expr).rounding_mode() = rounding_mode;
127  }
128  }
129 
130  if(expr.id()==ID_typecast)
131  {
132  const typecast_exprt &typecast_expr=to_typecast_expr(expr);
133 
134  const typet &src_type=typecast_expr.op().type();
135  const typet &dest_type=typecast_expr.type();
136 
137  if(dest_type.id()==ID_floatbv &&
138  src_type.id()==ID_floatbv)
139  {
140  // Casts from bigger to smaller float-type might round.
141  // For smaller to bigger it is strictly redundant but
142  // we leave this optimisation until later to simplify
143  // the representation.
144  expr.id(ID_floatbv_typecast);
145  expr.operands().resize(2);
146  to_floatbv_typecast_expr(expr).rounding_mode() = rounding_mode;
147  }
148  else if(
149  dest_type.id() == ID_floatbv &&
150  (src_type.id() == ID_signedbv || src_type.id() == ID_unsignedbv ||
151  src_type.id() == ID_c_enum_tag || src_type.id() == ID_c_bit_field))
152  {
153  // casts from integer to float-type might round
154  expr.id(ID_floatbv_typecast);
155  expr.operands().resize(2);
156  to_floatbv_typecast_expr(expr).rounding_mode() = rounding_mode;
157  }
158  else if(
159  dest_type.id() == ID_floatbv &&
160  (src_type.id() == ID_c_bool || src_type.id() == ID_bool))
161  {
162  // casts from bool or c_bool to float-type do not need rounding
163  }
164  else if(
165  (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
166  dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
167  src_type.id() == ID_floatbv)
168  {
169  // In C, casts from float to integer always round to zero,
170  // irrespectively of the rounding mode that is currently set.
171  // We will have to consider other programming languages
172  // eventually.
173 
174  /* ISO 9899:1999
175  * 6.3.1.4 Real floating and integer
176  * 1 When a finite value of real floating type is converted
177  * to an integer type other than _Bool, the fractional part
178  * is discarded (i.e., the value is truncated toward zero).
179  */
180  expr.id(ID_floatbv_typecast);
181  expr.operands().resize(2);
183  from_integer(ieee_floatt::ROUND_TO_ZERO, rounding_mode.type());
184  }
185  }
186 }
187 
189 {
191  return;
192 
193  symbol_exprt rounding_mode =
194  ns.lookup(rounding_mode_identifier()).symbol_expr();
195 
196  rounding_mode.add_source_location() = expr.source_location();
197 
198  adjust_float_expressions(expr, rounding_mode);
199 }
200 
202  goto_functionst::goto_functiont &goto_function,
203  const namespacet &ns)
204 {
205  for(auto &i : goto_function.body.instructions)
206  i.transform([&ns](exprt expr) -> optionalt<exprt> {
208  {
209  adjust_float_expressions(expr, ns);
210  return expr;
211  }
212  else
213  return {};
214  });
215 }
216 
218  goto_functionst &goto_functions,
219  const namespacet &ns)
220 {
221  for(auto &gf_entry : goto_functions.function_map)
222  adjust_float_expressions(gf_entry.second, ns);
223 }
224 
226 {
227  namespacet ns(goto_model.symbol_table);
229 }
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...
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
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:235
const source_locationt & source_location() const
Definition: expr.h:230
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
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:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Expression to hold a symbol (variable)
Definition: std_expr.h:80
Semantic type conversion.
Definition: std_expr.h:1866
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:293
#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:34
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:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:1900
Symbol table entry.