cprover
boolbv_floatbv_op.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <algorithm>
12 #include <iostream>
13 
14 #include <util/std_types.h>
15 
17 
19 {
20  const exprt &op0=expr.op(); // number to convert
21  const exprt &op1=expr.rounding_mode(); // rounding mode
22 
23  bvt bv0=convert_bv(op0);
24  bvt bv1=convert_bv(op1);
25 
26  const typet &src_type=ns.follow(expr.op0().type());
27  const typet &dest_type=ns.follow(expr.type());
28 
29  if(src_type==dest_type) // redundant type cast?
30  return bv0;
31 
32  float_utilst float_utils(prop);
33 
34  float_utils.set_rounding_mode(convert_bv(op1));
35 
36  if(src_type.id()==ID_floatbv &&
37  dest_type.id()==ID_floatbv)
38  {
39  float_utils.spec=ieee_float_spect(to_floatbv_type(src_type));
40  return
41  float_utils.conversion(
42  bv0,
43  ieee_float_spect(to_floatbv_type(dest_type)));
44  }
45  else if(src_type.id()==ID_signedbv &&
46  dest_type.id()==ID_floatbv)
47  {
48  float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
49  return float_utils.from_signed_integer(bv0);
50  }
51  else if(src_type.id()==ID_unsignedbv &&
52  dest_type.id()==ID_floatbv)
53  {
54  float_utils.spec=ieee_float_spect(to_floatbv_type(dest_type));
55  return float_utils.from_unsigned_integer(bv0);
56  }
57  else if(src_type.id()==ID_floatbv &&
58  dest_type.id()==ID_signedbv)
59  {
60  std::size_t dest_width=to_signedbv_type(dest_type).get_width();
61  float_utils.spec=ieee_float_spect(to_floatbv_type(src_type));
62  return float_utils.to_signed_integer(bv0, dest_width);
63  }
64  else if(src_type.id()==ID_floatbv &&
65  dest_type.id()==ID_unsignedbv)
66  {
67  std::size_t dest_width=to_unsignedbv_type(dest_type).get_width();
68  float_utils.spec=ieee_float_spect(to_floatbv_type(src_type));
69  return float_utils.to_unsigned_integer(bv0, dest_width);
70  }
71  else
72  return conversion_failed(expr);
73 }
74 
76 {
77  const exprt::operandst &operands=expr.operands();
78 
79  if(operands.size()!=3)
80  throw "operator "+expr.id_string()+" takes three operands";
81 
82  const exprt &op0=expr.op0(); // first operand
83  const exprt &op1=expr.op1(); // second operand
84  const exprt &op2=expr.op2(); // rounding mode
85 
86  bvt bv0=convert_bv(op0);
87  bvt bv1=convert_bv(op1);
88  bvt bv2=convert_bv(op2);
89 
90  const typet &type=ns.follow(expr.type());
92  op0.type() == type && op1.type() == type,
93  "float op with mixed types:\n" + expr.pretty());
94 
95  float_utilst float_utils(prop);
96 
97  float_utils.set_rounding_mode(bv2);
98 
99  if(type.id()==ID_floatbv)
100  {
101  float_utils.spec=ieee_float_spect(to_floatbv_type(expr.type()));
102 
103  if(expr.id()==ID_floatbv_plus)
104  return float_utils.add_sub(bv0, bv1, false);
105  else if(expr.id()==ID_floatbv_minus)
106  return float_utils.add_sub(bv0, bv1, true);
107  else if(expr.id()==ID_floatbv_mult)
108  return float_utils.mul(bv0, bv1);
109  else if(expr.id()==ID_floatbv_div)
110  return float_utils.div(bv0, bv1);
111  else if(expr.id()==ID_floatbv_rem)
112  return float_utils.rem(bv0, bv1);
113  else
114  throw "unexpected operator "+expr.id_string();
115  }
116  else if(type.id()==ID_vector || type.id()==ID_complex)
117  {
118  const typet &subtype=ns.follow(type.subtype());
119 
120  if(subtype.id()==ID_floatbv)
121  {
122  float_utils.spec=ieee_float_spect(to_floatbv_type(subtype));
123 
124  std::size_t width=boolbv_width(type);
125  std::size_t sub_width=boolbv_width(subtype);
126 
127  if(sub_width==0 || width%sub_width!=0)
128  throw "convert_floatbv_op: unexpected vector operand width";
129 
130  std::size_t size=width/sub_width;
131  bvt bv;
132  bv.resize(width);
133 
134  for(std::size_t i=0; i<size; i++)
135  {
136  bvt tmp_bv0, tmp_bv1, tmp_bv;
137 
138  tmp_bv0.assign(bv0.begin()+i*sub_width, bv0.begin()+(i+1)*sub_width);
139  tmp_bv1.assign(bv1.begin()+i*sub_width, bv1.begin()+(i+1)*sub_width);
140 
141  if(expr.id()==ID_floatbv_plus)
142  tmp_bv=float_utils.add_sub(tmp_bv0, tmp_bv1, false);
143  else if(expr.id()==ID_floatbv_minus)
144  tmp_bv=float_utils.add_sub(tmp_bv0, tmp_bv1, true);
145  else if(expr.id()==ID_floatbv_mult)
146  tmp_bv=float_utils.mul(tmp_bv0, tmp_bv1);
147  else if(expr.id()==ID_floatbv_div)
148  tmp_bv=float_utils.div(tmp_bv0, tmp_bv1);
149  else
150  assert(false);
151 
152  assert(tmp_bv.size()==sub_width);
153  assert(i*sub_width+sub_width-1<bv.size());
154  std::copy(tmp_bv.begin(), tmp_bv.end(), bv.begin()+i*sub_width);
155  }
156 
157  return bv;
158  }
159  else
160  return conversion_failed(expr);
161  }
162  else
163  return conversion_failed(expr);
164 }
The type of an expression.
Definition: type.h:22
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1287
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
boolbv_widtht boolbv_width
Definition: boolbv.h:90
bvt to_signed_integer(const bvt &src, std::size_t int_width)
Definition: float_utils.cpp:68
typet & type()
Definition: expr.h:56
const irep_idt & id() const
Definition: irep.h:189
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
bvt to_unsigned_integer(const bvt &src, std::size_t int_width)
Definition: float_utils.cpp:75
exprt & rounding_mode()
Definition: std_expr.h:2200
bvt conversion(const bvt &src, const ieee_float_spect &dest_spec)
virtual bvt convert_floatbv_op(const exprt &expr)
exprt & op1()
Definition: expr.h:75
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const namespacet & ns
const typet & follow(const typet &) const
Definition: namespace.cpp:55
std::size_t get_width() const
Definition: std_types.h:1129
std::vector< exprt > operandst
Definition: expr.h:45
void set_rounding_mode(const bvt &)
Definition: float_utils.cpp:16
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1245
ieee_float_spect spec
Definition: float_utils.h:86
bvt from_unsigned_integer(const bvt &)
Definition: float_utils.cpp:51
API to type classes.
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1373
semantic type conversion from/to floating-point formats
Definition: std_expr.h:2176
Base class for all expressions.
Definition: expr.h:42
const std::string & id_string() const
Definition: irep.h:192
bvt from_signed_integer(const bvt &)
Definition: float_utils.cpp:33
exprt & op2()
Definition: expr.h:78
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
operandst & operands()
Definition: expr.h:66
std::vector< literalt > bvt
Definition: literal.h:200