cprover
Loading...
Searching...
No Matches
boolbv_floatbv_op.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
10#include <util/c_types.h>
11#include <util/floatbv_expr.h>
12
14
15#include "boolbv.h"
16
18{
19 const exprt &op0=expr.op(); // number to convert
20 const exprt &op1=expr.rounding_mode(); // rounding mode
21
22 bvt bv0=convert_bv(op0);
23 bvt bv1=convert_bv(op1);
24
25 const typet &src_type = expr.op0().type();
26 const typet &dest_type = expr.type();
27
28 if(src_type==dest_type) // redundant type cast?
29 return bv0;
30
31 if(src_type.id() == ID_c_bit_field)
32 {
33 // go through underlying type
35 typecast_exprt(op0, to_c_bit_field_type(src_type).underlying_type()),
36 op1,
37 dest_type));
38 }
39
40 float_utilst float_utils(prop);
41
42 float_utils.set_rounding_mode(convert_bv(op1));
43
44 if(src_type.id()==ID_floatbv &&
45 dest_type.id()==ID_floatbv)
46 {
47 float_utils.spec=ieee_float_spect(to_floatbv_type(src_type));
48 return
49 float_utils.conversion(
50 bv0,
52 }
53 else if(src_type.id()==ID_signedbv &&
54 dest_type.id()==ID_floatbv)
55 {
56 float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
57 return float_utils.from_signed_integer(bv0);
58 }
59 else if(src_type.id()==ID_unsignedbv &&
60 dest_type.id()==ID_floatbv)
61 {
62 float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
63 return float_utils.from_unsigned_integer(bv0);
64 }
65 else if(src_type.id()==ID_floatbv &&
66 dest_type.id()==ID_signedbv)
67 {
68 std::size_t dest_width=to_signedbv_type(dest_type).get_width();
69 float_utils.spec=ieee_float_spect(to_floatbv_type(src_type));
70 return float_utils.to_signed_integer(bv0, dest_width);
71 }
72 else if(src_type.id()==ID_floatbv &&
73 dest_type.id()==ID_unsignedbv)
74 {
75 std::size_t dest_width=to_unsignedbv_type(dest_type).get_width();
76 float_utils.spec=ieee_float_spect(to_floatbv_type(src_type));
77 return float_utils.to_unsigned_integer(bv0, dest_width);
78 }
79 else
80 return conversion_failed(expr);
81}
82
84{
85 const exprt &lhs = expr.lhs();
86 const exprt &rhs = expr.rhs();
87 const exprt &rounding_mode = expr.rounding_mode();
88
89 bvt lhs_as_bv = convert_bv(lhs);
90 bvt rhs_as_bv = convert_bv(rhs);
91 bvt rounding_mode_as_bv = convert_bv(rounding_mode);
92
94 lhs.type() == expr.type() && rhs.type() == expr.type(),
95 "both operands of a floating point operator must match the expression type",
97
98 float_utilst float_utils(prop);
99
100 float_utils.set_rounding_mode(rounding_mode_as_bv);
101
102 if(expr.type().id() == ID_floatbv)
103 {
104 float_utils.spec=ieee_float_spect(to_floatbv_type(expr.type()));
105
106 if(expr.id()==ID_floatbv_plus)
107 return float_utils.add_sub(lhs_as_bv, rhs_as_bv, false);
108 else if(expr.id()==ID_floatbv_minus)
109 return float_utils.add_sub(lhs_as_bv, rhs_as_bv, true);
110 else if(expr.id()==ID_floatbv_mult)
111 return float_utils.mul(lhs_as_bv, rhs_as_bv);
112 else if(expr.id()==ID_floatbv_div)
113 return float_utils.div(lhs_as_bv, rhs_as_bv);
114 else
116 }
117 else if(expr.type().id() == ID_complex)
118 {
119 const typet &subtype = to_type_with_subtype(expr.type()).subtype();
120
121 if(subtype.id()==ID_floatbv)
122 {
123 float_utils.spec=ieee_float_spect(to_floatbv_type(subtype));
124
125 std::size_t width = boolbv_width(expr.type());
126 std::size_t sub_width=boolbv_width(subtype);
127
129 sub_width > 0 && width % sub_width == 0,
130 "width of a complex subtype must be positive and evenly divide the "
131 "width of the complex expression");
133 sub_width * 2 == width, "a complex type consists of exactly two parts");
134
135 bvt lhs_real{lhs_as_bv.begin(), lhs_as_bv.begin() + sub_width};
136 bvt rhs_real{rhs_as_bv.begin(), rhs_as_bv.begin() + sub_width};
137
138 bvt lhs_imag{lhs_as_bv.begin() + sub_width, lhs_as_bv.end()};
139 bvt rhs_imag{rhs_as_bv.begin() + sub_width, rhs_as_bv.end()};
140
141 bvt result_real, result_imag;
142
143 if(expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus)
144 {
145 result_real = float_utils.add_sub(
146 lhs_real, rhs_real, expr.id() == ID_floatbv_minus);
147 result_imag = float_utils.add_sub(
148 lhs_imag, rhs_imag, expr.id() == ID_floatbv_minus);
149 }
150 else if(expr.id() == ID_floatbv_mult)
151 {
152 // Could be optimised to just three multiplications with more additions
153 // instead, but then we'd have to worry about the impact of possible
154 // overflows. So we use the naive approach for now:
155 result_real = float_utils.add_sub(
156 float_utils.mul(lhs_real, rhs_real),
157 float_utils.mul(lhs_imag, rhs_imag),
158 true);
159 result_imag = float_utils.add_sub(
160 float_utils.mul(lhs_real, rhs_imag),
161 float_utils.mul(lhs_imag, rhs_real),
162 false);
163 }
164 else if(expr.id() == ID_floatbv_div)
165 {
166 bvt numerator_real = float_utils.add_sub(
167 float_utils.mul(lhs_real, rhs_real),
168 float_utils.mul(lhs_imag, rhs_imag),
169 false);
170 bvt numerator_imag = float_utils.add_sub(
171 float_utils.mul(lhs_imag, rhs_real),
172 float_utils.mul(lhs_real, rhs_imag),
173 true);
174
175 bvt denominator = float_utils.add_sub(
176 float_utils.mul(rhs_real, rhs_real),
177 float_utils.mul(rhs_imag, rhs_imag),
178 false);
179
180 result_real = float_utils.div(numerator_real, denominator);
181 result_imag = float_utils.div(numerator_imag, denominator);
182 }
183 else
185
186 bvt result_bv = std::move(result_real);
187 result_bv.reserve(width);
188 result_bv.insert(
189 result_bv.end(),
190 std::make_move_iterator(result_imag.begin()),
191 std::make_move_iterator(result_imag.end()));
192
193 return result_bv;
194 }
195 else
196 return conversion_failed(expr);
197 }
198 else
199 return conversion_failed(expr);
200}
Pre-defined bitvector types.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a typet to a floatbv_typet.
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a typet to an unsignedbv_typet.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
const c_bit_field_typet & to_c_bit_field_type(const typet &type)
Cast a typet to a c_bit_field_typet.
Definition c_types.h:80
exprt & op0()
Definition expr.h:133
std::size_t get_width() const
Definition std_types.h:925
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:39
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition boolbv.cpp:94
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:102
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
void set_rounding_mode(const bvt &)
bvt from_unsigned_integer(const bvt &)
virtual bvt mul(const bvt &src1, const bvt &src2)
bvt to_unsigned_integer(const bvt &src, std::size_t int_width)
virtual bvt div(const bvt &src1, const bvt &src2)
bvt from_signed_integer(const bvt &)
bvt conversion(const bvt &src, const ieee_float_spect &dest_spec)
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
ieee_float_spect spec
Definition float_utils.h:88
bvt to_signed_integer(const bvt &src, std::size_t int_width)
Semantic type conversion from/to floating-point formats.
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
const irep_idt & id() const
Definition irep.h:388
const typet & subtype() const
Definition type.h:187
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
API to expression classes for floating-point arithmetic.
std::vector< literalt > bvt
Definition literal.h:201
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition invariant.h:535
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:208