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
43
44 float_utils.set_rounding_mode(convert_bv(op1));
45
46 if(src_type.id()==ID_floatbv &&
48 {
50 return
51 float_utils.conversion(
52 bv0,
54 }
55 else if(src_type.id()==ID_signedbv &&
57 {
59 return float_utils.from_signed_integer(bv0);
60 }
61 else if(src_type.id()==ID_unsignedbv &&
63 {
65 return float_utils.from_unsigned_integer(bv0);
66 }
67 else if(src_type.id()==ID_floatbv &&
69 {
70 std::size_t dest_width=to_signedbv_type(dest_type).get_width();
72 return float_utils.to_signed_integer(bv0, dest_width);
73 }
74 else if(src_type.id()==ID_floatbv &&
76 {
77 std::size_t dest_width=to_unsignedbv_type(dest_type).get_width();
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
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
101
102 float_utils.set_rounding_mode(rounding_mode_as_bv);
103
104 if(expr.type().id() == ID_floatbv)
105 {
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 {
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 {
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)
152 else if(expr.id()==ID_floatbv_minus)
154 else if(expr.id()==ID_floatbv_mult)
156 else if(expr.id()==ID_floatbv_div)
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
exprt & op0()
Definition expr.h:125
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
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
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