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