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
9#include "boolbv.h"
10
11#include <algorithm>
12
14#include <util/c_types.h>
15#include <util/floatbv_expr.h>
16
18
20{
21 const exprt &op0=expr.op(); // number to convert
22 const exprt &op1=expr.rounding_mode(); // rounding mode
23
24 bvt bv0=convert_bv(op0);
25 bvt bv1=convert_bv(op1);
26
27 const typet &src_type = expr.op0().type();
28 const typet &dest_type = expr.type();
29
30 if(src_type==dest_type) // redundant type cast?
31 return bv0;
32
33 if(src_type.id() == ID_c_bit_field)
34 {
35 // go through underlying type
37 typecast_exprt(op0, to_c_bit_field_type(src_type).underlying_type()),
38 op1,
39 dest_type));
40 }
41
42 float_utilst float_utils(prop);
43
44 float_utils.set_rounding_mode(convert_bv(op1));
45
46 if(src_type.id()==ID_floatbv &&
47 dest_type.id()==ID_floatbv)
48 {
49 float_utils.spec=ieee_float_spect(to_floatbv_type(src_type));
50 return
51 float_utils.conversion(
52 bv0,
54 }
55 else if(src_type.id()==ID_signedbv &&
56 dest_type.id()==ID_floatbv)
57 {
58 float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
59 return float_utils.from_signed_integer(bv0);
60 }
61 else if(src_type.id()==ID_unsignedbv &&
62 dest_type.id()==ID_floatbv)
63 {
64 float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
65 return float_utils.from_unsigned_integer(bv0);
66 }
67 else if(src_type.id()==ID_floatbv &&
68 dest_type.id()==ID_signedbv)
69 {
70 std::size_t dest_width=to_signedbv_type(dest_type).get_width();
71 float_utils.spec=ieee_float_spect(to_floatbv_type(src_type));
72 return float_utils.to_signed_integer(bv0, dest_width);
73 }
74 else if(src_type.id()==ID_floatbv &&
75 dest_type.id()==ID_unsignedbv)
76 {
77 std::size_t dest_width=to_unsignedbv_type(dest_type).get_width();
78 float_utils.spec=ieee_float_spect(to_floatbv_type(src_type));
79 return float_utils.to_unsigned_integer(bv0, dest_width);
80 }
81 else
82 return conversion_failed(expr);
83}
84
86{
87 const exprt &lhs = expr.lhs();
88 const exprt &rhs = expr.rhs();
89 const exprt &rounding_mode = expr.rounding_mode();
90
91 bvt lhs_as_bv = convert_bv(lhs);
92 bvt rhs_as_bv = convert_bv(rhs);
93 bvt rounding_mode_as_bv = convert_bv(rounding_mode);
94
96 lhs.type() == expr.type() && rhs.type() == expr.type(),
97 "both operands of a floating point operator must match the expression type",
99
100 float_utilst float_utils(prop);
101
102 float_utils.set_rounding_mode(rounding_mode_as_bv);
103
104 if(expr.type().id() == ID_floatbv)
105 {
106 float_utils.spec=ieee_float_spect(to_floatbv_type(expr.type()));
107
108 if(expr.id()==ID_floatbv_plus)
109 return float_utils.add_sub(lhs_as_bv, rhs_as_bv, false);
110 else if(expr.id()==ID_floatbv_minus)
111 return float_utils.add_sub(lhs_as_bv, rhs_as_bv, true);
112 else if(expr.id()==ID_floatbv_mult)
113 return float_utils.mul(lhs_as_bv, rhs_as_bv);
114 else if(expr.id()==ID_floatbv_div)
115 return float_utils.div(lhs_as_bv, rhs_as_bv);
116 else
118 }
119 else if(expr.type().id() == ID_complex)
120 {
121 const typet &subtype = to_type_with_subtype(expr.type()).subtype();
122
123 if(subtype.id()==ID_floatbv)
124 {
125 float_utils.spec=ieee_float_spect(to_floatbv_type(subtype));
126
127 std::size_t width = boolbv_width(expr.type());
128 std::size_t sub_width=boolbv_width(subtype);
129
131 sub_width > 0 && width % sub_width == 0,
132 "width of a complex subtype must be positive and evenly divide the "
133 "width of the complex expression");
134
135 std::size_t size=width/sub_width;
136 bvt result_bv;
137 result_bv.resize(width);
138
139 for(std::size_t i=0; i<size; i++)
140 {
141 bvt lhs_sub_bv, rhs_sub_bv, sub_result_bv;
142
143 lhs_sub_bv.assign(
144 lhs_as_bv.begin() + i * sub_width,
145 lhs_as_bv.begin() + (i + 1) * sub_width);
146 rhs_sub_bv.assign(
147 rhs_as_bv.begin() + i * sub_width,
148 rhs_as_bv.begin() + (i + 1) * sub_width);
149
150 if(expr.id()==ID_floatbv_plus)
151 sub_result_bv = float_utils.add_sub(lhs_sub_bv, rhs_sub_bv, false);
152 else if(expr.id()==ID_floatbv_minus)
153 sub_result_bv = float_utils.add_sub(lhs_sub_bv, rhs_sub_bv, true);
154 else if(expr.id()==ID_floatbv_mult)
155 sub_result_bv = float_utils.mul(lhs_sub_bv, rhs_sub_bv);
156 else if(expr.id()==ID_floatbv_div)
157 sub_result_bv = float_utils.div(lhs_sub_bv, rhs_sub_bv);
158 else
160
161 INVARIANT(
162 sub_result_bv.size() == sub_width,
163 "we constructed a new complex of the right size");
164 INVARIANT(
165 i * sub_width + sub_width - 1 < result_bv.size(),
166 "the sub-bitvector fits into the result bitvector");
167 std::copy(
168 sub_result_bv.begin(),
169 sub_result_bv.end(),
170 result_bv.begin() + i * sub_width);
171 }
172
173 return result_bv;
174 }
175 else
176 return conversion_failed(expr);
177 }
178 else
179 return conversion_failed(expr);
180}
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:125
std::size_t get_width() const
Definition std_types.h:876
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:38
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:82
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:99
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:396
const typet & subtype() const
Definition type.h:154
Semantic type conversion.
Definition std_expr.h:2017
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 INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#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:175