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 
16 #include "../floatbv/float_utils.h"
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());
91 
92  if(op0.type()!=type || op1.type()!=type)
93  {
94  std::cerr << expr.pretty() << '\n';
95  throw "float op with mixed types";
96  }
97 
98  float_utilst float_utils(prop);
99 
100  float_utils.set_rounding_mode(bv2);
101 
102  if(type.id()==ID_floatbv)
103  {
104  float_utils.spec=ieee_float_spect(to_floatbv_type(expr.type()));
105 
106  if(expr.id()==ID_floatbv_plus)
107  return float_utils.add_sub(bv0, bv1, false);
108  else if(expr.id()==ID_floatbv_minus)
109  return float_utils.add_sub(bv0, bv1, true);
110  else if(expr.id()==ID_floatbv_mult)
111  return float_utils.mul(bv0, bv1);
112  else if(expr.id()==ID_floatbv_div)
113  return float_utils.div(bv0, bv1);
114  else if(expr.id()==ID_floatbv_rem)
115  return float_utils.rem(bv0, bv1);
116  else
117  throw "unexpected operator "+expr.id_string();
118  }
119  else if(type.id()==ID_vector || type.id()==ID_complex)
120  {
121  const typet &subtype=ns.follow(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(type);
128  std::size_t sub_width=boolbv_width(subtype);
129 
130  if(sub_width==0 || width%sub_width!=0)
131  throw "convert_floatbv_op: unexpected vector operand width";
132 
133  std::size_t size=width/sub_width;
134  bvt bv;
135  bv.resize(width);
136 
137  for(std::size_t i=0; i<size; i++)
138  {
139  bvt tmp_bv0, tmp_bv1, tmp_bv;
140 
141  tmp_bv0.assign(bv0.begin()+i*sub_width, bv0.begin()+(i+1)*sub_width);
142  tmp_bv1.assign(bv1.begin()+i*sub_width, bv1.begin()+(i+1)*sub_width);
143 
144  if(expr.id()==ID_floatbv_plus)
145  tmp_bv=float_utils.add_sub(tmp_bv0, tmp_bv1, false);
146  else if(expr.id()==ID_floatbv_minus)
147  tmp_bv=float_utils.add_sub(tmp_bv0, tmp_bv1, true);
148  else if(expr.id()==ID_floatbv_mult)
149  tmp_bv=float_utils.mul(tmp_bv0, tmp_bv1);
150  else if(expr.id()==ID_floatbv_div)
151  tmp_bv=float_utils.div(tmp_bv0, tmp_bv1);
152  else
153  assert(false);
154 
155  assert(tmp_bv.size()==sub_width);
156  assert(i*sub_width+sub_width-1<bv.size());
157  std::copy(tmp_bv.begin(), tmp_bv.end(), bv.begin()+i*sub_width);
158  }
159 
160  return bv;
161  }
162  else
163  return conversion_failed(expr);
164  }
165  else
166  return conversion_failed(expr);
167 }
The type of an expression.
Definition: type.h:20
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
exprt & op0()
Definition: expr.h:84
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:60
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
virtual bvt rem(const bvt &src1, const bvt &src2)
const irep_idt & id() const
Definition: irep.h:189
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
bvt to_unsigned_integer(const bvt &src, std::size_t int_width)
Definition: float_utils.cpp:75
virtual bvt mul(const bvt &src1, const bvt &src2)
exprt & rounding_mode()
Definition: std_expr.h:1808
bvt conversion(const bvt &src, const ieee_float_spect &dest_spec)
virtual bvt convert_floatbv_op(const exprt &expr)
exprt & op1()
Definition: expr.h:87
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const namespacet & ns
virtual bvt div(const bvt &src1, const bvt &src2)
const unsignedbv_typet & to_unsignedbv_type(const typet &type)
Cast a generic typet to an unsignedbv_typet.
Definition: std_types.h:1154
virtual bvt add_sub(const bvt &src1, const bvt &src2, bool subtract)
std::size_t get_width() const
Definition: std_types.h:1030
std::vector< exprt > operandst
Definition: expr.h:49
void set_rounding_mode(const bvt &)
Definition: float_utils.cpp:16
ieee_float_spect spec
Definition: float_utils.h:86
bvt from_unsigned_integer(const bvt &)
Definition: float_utils.cpp:51
API to type classes.
semantic type conversion from/to floating-point formats
Definition: std_expr.h:1783
Base class for all expressions.
Definition: expr.h:46
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
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:90
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
std::vector< literalt > bvt
Definition: literal.h:197