CBMC: /home/runner/work/cbmc/cbmc/src/goto-programs/adjust_float_expressions.cpp Source File

CBMC
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
12#include "adjust_float_expressions.h"
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 &&
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 // FMA needs rounding mode added (3 operands -> 4)
57 if(expr.id() == ID_floatbv_fma && expr.operands().size() == 3)
58 return true;
59
60 if(expr.id()==ID_typecast)
61 {
63
64 const typet &src_type=typecast_expr.op().type();
65 const typet &dest_type=typecast_expr.type();
66
67 if(dest_type.id()==ID_floatbv &&
68 src_type.id()==ID_floatbv)
69 return true;
70 else if(
71 dest_type.id() == ID_floatbv &&
72 (src_type.id() == ID_c_bit_field || src_type.id() == ID_signedbv ||
73 src_type.id() == ID_unsignedbv || src_type.id() == ID_c_enum_tag))
74 return true;
75 else if(
76 (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
77 dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
78 src_type.id() == ID_floatbv)
79 return true;
80 }
81
82 for(const auto &op : expr.operands())
83 {
85 return true;
86 }
87
88 return false;
89}
90
91 void adjust_float_expressions(exprt &expr, const exprt &rounding_mode)
92{
94 return;
95
96 // recursive call
97 // Note that we do the recursion twice here; once in
98 // `have_to_adjust_float_expressions` and once here. Presumably this is to
99 // avoid breaking sharing (calling the non-const operands() function breaks
100 // sharing)
101 for(auto &op : expr.operands())
102 adjust_float_expressions(op, rounding_mode);
103
104 const typet &type = expr.type();
105
106 if(
107 type.id() == ID_floatbv ||
108 (type.id() == ID_complex &&
109 to_complex_type(type).subtype().id() == ID_floatbv))
110 {
111 if(
112 expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
113 expr.id() == ID_div)
114 {
116 expr.operands().size() >= 2,
117 "arithmetic operations must have two or more operands");
118
119 // make sure we have binary expressions
120 if(expr.operands().size()>2)
121 {
122 expr=make_binary(expr);
123 CHECK_RETURN(expr.operands().size() == 2);
124 }
125
126 // now add rounding mode
127 expr.id(expr.id()==ID_plus?ID_floatbv_plus:
129 expr.id()==ID_mult?ID_floatbv_mult:
130 expr.id()==ID_div?ID_floatbv_div:
131 irep_idt());
132
133 expr.operands().resize(3);
134 to_ieee_float_op_expr(expr).rounding_mode() = rounding_mode;
135 }
136 }
137
138 // Add rounding mode to FMA
139 if(expr.id() == ID_floatbv_fma && expr.operands().size() == 3)
140 {
141 expr.operands().resize(4);
142 to_floatbv_fma_expr(expr).rounding_mode() = rounding_mode;
143 }
144
145 if(expr.id()==ID_typecast)
146 {
148
149 const typet &src_type=typecast_expr.op().type();
150 const typet &dest_type=typecast_expr.type();
151
152 if(dest_type.id()==ID_floatbv &&
153 src_type.id()==ID_floatbv)
154 {
155 // Casts from bigger to smaller float-type might round.
156 // For smaller to bigger it is strictly redundant but
157 // we leave this optimisation until later to simplify
158 // the representation.
160 expr.operands().resize(2);
161 to_floatbv_typecast_expr(expr).rounding_mode() = rounding_mode;
162 }
163 else if(
164 dest_type.id() == ID_floatbv &&
165 (src_type.id() == ID_signedbv || src_type.id() == ID_unsignedbv ||
166 src_type.id() == ID_c_enum_tag || src_type.id() == ID_c_bit_field))
167 {
168 // casts from integer to float-type might round
170 expr.operands().resize(2);
171 to_floatbv_typecast_expr(expr).rounding_mode() = rounding_mode;
172 }
173 else if(
174 dest_type.id() == ID_floatbv &&
175 (src_type.id() == ID_c_bool || src_type.id() == ID_bool))
176 {
177 // casts from bool or c_bool to float-type do not need rounding
178 }
179 else if(
180 (dest_type.id() == ID_signedbv || dest_type.id() == ID_unsignedbv ||
181 dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_c_bit_field) &&
182 src_type.id() == ID_floatbv)
183 {
184 // In C, casts from float to integer always round to zero,
185 // irrespectively of the rounding mode that is currently set.
186 // We will have to consider other programming languages
187 // eventually.
188
189 /* ISO 9899:1999
190 * 6.3.1.4 Real floating and integer
191 * 1 When a finite value of real floating type is converted
192 * to an integer type other than _Bool, the fractional part
193 * is discarded (i.e., the value is truncated toward zero).
194 */
196 expr.operands().resize(2);
197 to_floatbv_typecast_expr(expr).rounding_mode() =
199 }
200 }
201}
202
204{
206 return;
207
208 symbol_exprt rounding_mode =
209 ns.lookup(rounding_mode_identifier()).symbol_expr();
210
211 rounding_mode.add_source_location() = expr.source_location();
212
213 adjust_float_expressions(expr, rounding_mode);
214}
215
217 goto_functionst::goto_functiont &goto_function,
218 const namespacet &ns)
219{
220 for(auto &i : goto_function.body.instructions)
221 i.transform([&ns](exprt expr) -> std::optional<exprt> {
223 {
224 adjust_float_expressions(expr, ns);
225 return expr;
226 }
227 else
228 return {};
229 });
230}
231
233 goto_functionst &goto_functions,
234 const namespacet &ns)
235{
236 for(auto &gf_entry : goto_functions.function_map)
238}
239
241{
242 namespacet ns(goto_model.symbol_table);
244}
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)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:57
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
const source_locationt & source_location() const
Definition expr.h:236
source_locationt & add_source_location()
Definition expr.h:241
A collection of goto functions.
function_mapt function_map
::goto_functiont goto_functiont
Definition goto_model.h:27
symbol_tablet symbol_table
Symbol table.
Definition goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
@ ROUND_TO_ZERO
Definition ieee_float.h:382
const irep_idt & id() const
Definition irep.h:388
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:134
Expression to hold a symbol (variable)
Definition std_expr.h:132
Semantic type conversion.
Definition std_expr.h:1995
The type of an expression, extends irept.
Definition type.h:29
#define CPROVER_PREFIX
exprt make_binary(const exprt &expr)
splits an expression with >=3 operands into nested binary expressions
Definition expr_util.cpp:38
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:489
const floatbv_fma_exprt & to_floatbv_fma_expr(const exprt &expr)
Definition floatbv_expr.h:626
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.
#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:534
API to expression classes.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2024
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
Definition std_types.h:1048
Symbol table entry.
dstringt irep_idt

AltStyle によって変換されたページ (->オリジナル) /