cprover
convert_float_literal.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C++ Language Conversion
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "convert_float_literal.h"
13 
14 #include <cassert>
15 
16 #include <util/arith_tools.h>
17 #include <util/c_types.h>
18 #include <util/config.h>
19 #include <util/ieee_float.h>
20 #include <util/std_expr.h>
21 #include <util/std_types.h>
22 #include <util/string2int.h>
23 
24 #include "parse_float.h"
25 
26 exprt convert_float_literal(const std::string &src)
27 {
28  mp_integer significand;
29  mp_integer exponent;
30  bool is_float, is_long, is_imaginary;
31  bool is_decimal, is_float80, is_float128; // GCC extensions
32  unsigned base;
33 
35  src,
36  significand,
37  exponent,
38  base,
39  is_float,
40  is_long,
41  is_imaginary,
42  is_decimal,
43  is_float80,
44  is_float128);
45 
46  exprt result=exprt(ID_constant);
47 
48  // In ANSI-C, float literals are double by default,
49  // unless marked with 'f'.
50  // All of these can be complex as well.
51  // This can be overridden with
52  // config.ansi_c.single_precision_constant.
53 
54  if(is_float)
55  result.type()=float_type();
56  else if(is_long)
57  result.type()=long_double_type();
58  else if(is_float80)
59  {
60  result.type()=ieee_float_spect(64, 15).to_type();
61  result.type().set(ID_C_c_type, ID_long_double);
62  }
63  else if(is_float128)
64  {
66  result.type().set(ID_C_c_type, ID_gcc_float128);
67  }
68  else
69  {
70  // default
72  result.type()=float_type(); // default
73  else
74  result.type()=double_type(); // default
75  }
76 
77  if(is_decimal)
78  {
79  // TODO - should set ID_gcc_decimal32/ID_gcc_decimal64/ID_gcc_decimal128,
80  // but these aren't handled anywhere
81  }
82 
84  {
85  unsigned width=result.type().get_int(ID_width);
86  unsigned fraction_bits;
87  const irep_idt integer_bits=result.type().get(ID_integer_bits);
88 
89  assert(width!=0);
90 
91  if(integer_bits==irep_idt())
92  fraction_bits=width/2; // default
93  else
94  fraction_bits=width-std::stoi(id2string(integer_bits));
95 
96  mp_integer factor=mp_integer(1)<<fraction_bits;
97  mp_integer value=significand*factor;
98 
99  if(value!=0)
100  {
101  if(exponent<0)
102  value/=power(base, -exponent);
103  else
104  {
105  value*=power(base, exponent);
106 
107  if(value>=power(2, width-1))
108  {
109  // saturate: use "biggest value"
110  value=power(2, width-1)-1;
111  }
112  else if(value<=-power(2, width-1)-1)
113  {
114  // saturate: use "smallest value"
115  value=-power(2, width-1);
116  }
117  }
118  }
119 
120  result.set(ID_value, integer2binary(value, width));
121  }
122  else
123  {
124  ieee_floatt a(to_floatbv_type(result.type()));
125 
126  if(base==10)
127  a.from_base10(significand, exponent);
128  else if(base==2) // hex
129  a.build(significand, exponent);
130  else
131  assert(false);
132 
133  result.set(
134  ID_value,
135  integer2binary(a.pack(), a.spec.width()));
136  }
137 
138  if(is_imaginary)
139  {
140  complex_typet complex_type;
141  complex_type.subtype()=result.type();
142  exprt complex_expr(ID_complex, complex_type);
143  complex_expr.operands().resize(2);
144  complex_expr.op0()=from_integer(0, result.type());
145  complex_expr.op1()=result;
146  return complex_expr;
147  }
148 
149  return result;
150 }
struct configt::ansi_ct ansi_c
void parse_float(const std::string &src, mp_integer &significand, mp_integer &exponent, unsigned &exponent_base, bool &is_float, bool &is_long, bool &is_imaginary, bool &is_decimal, bool &is_float80, bool &is_float128)
Definition: parse_float.cpp:16
BigInt mp_integer
Definition: mp_arith.h:19
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
exprt & op0()
Definition: expr.h:84
void build(const mp_integer &exp, const mp_integer &frac)
Definition: ieee_float.cpp:465
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:245
bool single_precision_constant
Definition: config.h:46
C Language Conversion.
bitvector_typet double_type()
Definition: c_types.cpp:203
typet & type()
Definition: expr.h:60
configt config
Definition: config.cpp:21
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
bitvector_typet float_type()
Definition: c_types.cpp:184
static ieee_float_spect quadruple_precision()
Definition: ieee_float.h:75
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
Definition: ieee_float.cpp:479
ieee_float_spect spec
Definition: ieee_float.h:123
ANSI-C Conversion / Type Checking.
bool use_fixed_for_float
Definition: config.h:44
bitvector_typet long_double_type()
Definition: c_types.cpp:222
Complex numbers made of pair of given subtype.
Definition: std_types.h:1606
API to type classes.
Base class for all expressions.
Definition: expr.h:46
exprt convert_float_literal(const std::string &src)
mp_integer pack() const
Definition: ieee_float.cpp:367
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
std::size_t width() const
Definition: ieee_float.h:50
dstringt irep_idt
Definition: irep.h:32
const typet & subtype() const
Definition: type.h:31
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
mp_integer power(const mp_integer &base, const mp_integer &exponent)
A multi-precision implementation of the power operator.
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214