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 <ansi-c/gcc_types.h>
25 
26 #include "parse_float.h"
27 
28 exprt convert_float_literal(const std::string &src)
29 {
30  parse_floatt parsed_float(src);
31 
32  exprt result=exprt(ID_constant);
33 
34  // In ANSI-C, float literals are double by default,
35  // unless marked with 'f'.
36  // All of these can be complex as well.
37  // This can be overridden with
38  // config.ansi_c.single_precision_constant.
39 
40  if(parsed_float.is_float)
41  result.type()=float_type();
42  else if(parsed_float.is_long)
43  result.type()=long_double_type();
44  else if(parsed_float.is_float16)
45  result.type()=gcc_float16_type();
46  else if(parsed_float.is_float32)
47  result.type()=gcc_float32_type();
48  else if(parsed_float.is_float32x)
49  result.type()=gcc_float32x_type();
50  else if(parsed_float.is_float64)
51  result.type()=gcc_float64_type();
52  else if(parsed_float.is_float64x)
53  result.type()=gcc_float64x_type();
54  else if(parsed_float.is_float80)
55  {
56  result.type()=ieee_float_spect(64, 15).to_type();
57  result.type().set(ID_C_c_type, ID_long_double);
58  }
59  else if(parsed_float.is_float128)
60  result.type()=gcc_float128_type();
61  else if(parsed_float.is_float128x)
62  result.type()=gcc_float128x_type();
63  else
64  {
65  // default
67  result.type()=float_type(); // default
68  else
69  result.type()=double_type(); // default
70  }
71 
72  if(parsed_float.is_decimal)
73  {
74  // TODO - should set ID_gcc_decimal32/ID_gcc_decimal64/ID_gcc_decimal128,
75  // but these aren't handled anywhere
76  }
77 
78  ieee_floatt a(to_floatbv_type(result.type()));
79 
80  if(parsed_float.exponent_base==10)
81  a.from_base10(parsed_float.significand, parsed_float.exponent);
82  else if(parsed_float.exponent_base==2) // hex
83  a.build(parsed_float.significand, parsed_float.exponent);
84  else
86 
87  result.set(
88  ID_value,
89  integer2binary(a.pack(), a.spec.width()));
90 
91  if(parsed_float.is_imaginary)
92  {
93  const complex_typet complex_type(result.type());
94  return complex_exprt(from_integer(0, result.type()), result, complex_type);
95  }
96 
97  return result;
98 }
bitvector_typet gcc_float128_type()
Definition: gcc_types.cpp:58
struct configt::ansi_ct ansi_c
unsigned exponent_base
Definition: parse_float.h:23
void build(const mp_integer &exp, const mp_integer &frac)
Definition: ieee_float.cpp:465
bitvector_typet gcc_float64x_type()
Definition: gcc_types.cpp:49
bool is_float16
Definition: parse_float.h:28
bool single_precision_constant
Definition: config.h:47
bool is_float32
Definition: parse_float.h:28
C Language Conversion.
bitvector_typet double_type()
Definition: c_types.cpp:193
typet & type()
Definition: expr.h:56
bool is_float80
Definition: parse_float.h:28
configt config
Definition: config.cpp:23
bool is_float128
Definition: parse_float.h:28
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
bitvector_typet gcc_float32x_type()
Definition: gcc_types.cpp:31
bitvector_typet float_type()
Definition: c_types.cpp:185
mp_integer exponent
Definition: parse_float.h:22
mp_integer significand
Definition: parse_float.h:22
API to expression classes.
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:134
ANSI-C Conversion / Type Checking.
bitvector_typet long_double_type()
Definition: c_types.cpp:201
Complex numbers made of pair of given subtype.
Definition: std_types.h:1677
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
Base class for all expressions.
Definition: expr.h:42
exprt convert_float_literal(const std::string &src)
bool is_imaginary
Definition: parse_float.h:28
bool is_float128x
Definition: parse_float.h:28
bool is_decimal
Definition: parse_float.h:28
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:67
#define UNREACHABLE
Definition: invariant.h:250
bool is_float64
Definition: parse_float.h:28
std::size_t width() const
Definition: ieee_float.h:54
bitvector_typet gcc_float64_type()
Definition: gcc_types.cpp:40
bitvector_typet gcc_float16_type()
Definition: gcc_types.cpp:14
bool is_float64x
Definition: parse_float.h:28
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bitvector_typet gcc_float128x_type()
Definition: gcc_types.cpp:67
complex constructor from a pair of numbers
Definition: std_expr.h:1861
bitvector_typet gcc_float32_type()
Definition: gcc_types.cpp:22
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
bool is_float32x
Definition: parse_float.h:28