cprover
Loading...
Searching...
No Matches
adjust_float_expressions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: 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
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 &&
48 to_complex_type(type).subtype().id() == ID_floatbv))
49 {
50 if(
51 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
52 expr.id() == ID_div)
53 return true;
54 }
55
56 if(expr.id()==ID_typecast)
57 {
58 const typecast_exprt &typecast_expr=to_typecast_expr(expr);
59
60 const typet &src_type=typecast_expr.op().type();
61 const typet &dest_type=typecast_expr.type();
62
63 if(dest_type.id()==ID_floatbv &&
64 src_type.id()==ID_floatbv)
65 return true;
66 else if(
67 dest_type.id() == ID_floatbv &&
68 (src_type.id() == ID_c_bit_field || src_type.id() == ID_signedbv ||
69 src_type.id() == ID_unsignedbv || src_type.id() == ID_c_enum_tag))
70 return true;
71 else if(
72 (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
73 dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
74 src_type.id() == ID_floatbv)
75 return true;
76 }
77
78 forall_operands(it, expr)
80 return true;
81
82 return false;
83}
84
85void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
86{
88 return;
89
90 // recursive call
91 // Note that we do the recursion twice here; once in
92 // `have_to_adjust_float_expressions` and once here. Presumably this is to
93 // avoid breaking sharing (calling the non-const operands() function breaks
94 // sharing)
95 for(auto &op : expr.operands())
96 adjust_float_expressions(op, rounding_mode);
97
98 const typet &type = expr.type();
99
100 if(
101 type.id() == ID_floatbv ||
102 (type.id() == ID_complex &&
103 to_complex_type(type).subtype().id() == ID_floatbv))
104 {
105 if(
106 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
107 expr.id() == ID_div)
108 {
110 expr.operands().size() >= 2,
111 "arithmetic operations must have two or more operands");
112
113 // make sure we have binary expressions
114 if(expr.operands().size()>2)
115 {
116 expr=make_binary(expr);
117 CHECK_RETURN(expr.operands().size() == 2);
118 }
119
120 // now add rounding mode
121 expr.id(expr.id()==ID_plus?ID_floatbv_plus:
122 expr.id()==ID_minus?ID_floatbv_minus:
123 expr.id()==ID_mult?ID_floatbv_mult:
124 expr.id()==ID_div?ID_floatbv_div:
125 irep_idt());
126
127 expr.operands().resize(3);
128 to_ieee_float_op_expr(expr).rounding_mode() = rounding_mode;
129 }
130 }
131
132 if(expr.id()==ID_typecast)
133 {
134 const typecast_exprt &typecast_expr=to_typecast_expr(expr);
135
136 const typet &src_type=typecast_expr.op().type();
137 const typet &dest_type=typecast_expr.type();
138
139 if(dest_type.id()==ID_floatbv &&
140 src_type.id()==ID_floatbv)
141 {
142 // Casts from bigger to smaller float-type might round.
143 // For smaller to bigger it is strictly redundant but
144 // we leave this optimisation until later to simplify
145 // the representation.
146 expr.id(ID_floatbv_typecast);
147 expr.operands().resize(2);
148 to_floatbv_typecast_expr(expr).rounding_mode() = rounding_mode;
149 }
150 else if(
151 dest_type.id() == ID_floatbv &&
152 (src_type.id() == ID_signedbv || src_type.id() == ID_unsignedbv ||
153 src_type.id() == ID_c_enum_tag || src_type.id() == ID_c_bit_field))
154 {
155 // casts from integer to float-type might round
156 expr.id(ID_floatbv_typecast);
157 expr.operands().resize(2);
158 to_floatbv_typecast_expr(expr).rounding_mode() = rounding_mode;
159 }
160 else if(
161 dest_type.id() == ID_floatbv &&
162 (src_type.id() == ID_c_bool || src_type.id() == ID_bool))
163 {
164 // casts from bool or c_bool to float-type do not need rounding
165 }
166 else if(
167 (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
168 dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
169 src_type.id() == ID_floatbv)
170 {
171 // In C, casts from float to integer always round to zero,
172 // irrespectively of the rounding mode that is currently set.
173 // We will have to consider other programming languages
174 // eventually.
175
176 /* ISO 9899:1999
177 * 6.3.1.4 Real floating and integer
178 * 1 When a finite value of real floating type is converted
179 * to an integer type other than _Bool, the fractional part
180 * is discarded (i.e., the value is truncated toward zero).
181 */
182 expr.id(ID_floatbv_typecast);
183 expr.operands().resize(2);
186 }
187 }
188}
189
191{
193 return;
194
195 symbol_exprt rounding_mode =
196 ns.lookup(rounding_mode_identifier()).symbol_expr();
197
198 rounding_mode.add_source_location() = expr.source_location();
199
200 adjust_float_expressions(expr, rounding_mode);
201}
202
204 goto_functionst::goto_functiont &goto_function,
205 const namespacet &ns)
206{
207 for(auto &i : goto_function.body.instructions)
208 i.transform([&ns](exprt expr) -> optionalt<exprt> {
210 {
211 adjust_float_expressions(expr, ns);
212 return expr;
213 }
214 else
215 return {};
216 });
217}
218
220 goto_functionst &goto_functions,
221 const namespacet &ns)
222{
223 for(auto &gf_entry : goto_functions.function_map)
224 adjust_float_expressions(gf_entry.second, ns);
225}
226
228{
229 namespacet ns(goto_model.symbol_table);
231}
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
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const source_locationt & source_location() const
Definition: expr.h:230
source_locationt & add_source_location()
Definition: expr.h:235
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:396
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:1920
The type of an expression, extends irept.
Definition: type.h:29
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:35
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:1954
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition: std_types.h:1082
Symbol table entry.