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
44
45 float_utils.set_rounding_mode(convert_bv(op1));
46
47 if(src_type.id()==ID_floatbv &&
49 {
51 return
52 float_utils.conversion(
53 bv0,
55 }
56 else if(src_type.id()==ID_signedbv &&
58 {
60 return float_utils.from_signed_integer(bv0);
61 }
62 else if(src_type.id()==ID_unsignedbv &&
64 {
66 return float_utils.from_unsigned_integer(bv0);
67 }
68 else if(src_type.id()==ID_floatbv &&
70 {
73 return float_utils.to_signed_integer(bv0, dest_width);
74 }
75 else if(src_type.id()==ID_floatbv &&
77 {
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
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
102
103 float_utils.set_rounding_mode(rounding_mode_as_bv);
104
105 if(expr.type().id() == ID_floatbv)
106 {
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 {
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 {
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)
153 else if(expr.id()==ID_floatbv_minus)
155 else if(expr.id()==ID_floatbv_mult)
157 else if(expr.id()==ID_floatbv_div)
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
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
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