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/c_types.h>
17 #include <util/config.h>
18 #include <util/ieee_float.h>
19 #include <util/std_expr.h>
20 #include <util/std_types.h>
21 #include <util/string2int.h>
22 
23 #include <ansi-c/gcc_types.h>
24 
25 #include "parse_float.h"
26 
29 exprt convert_float_literal(const std::string &src)
30 {
31  parse_floatt parsed_float(src);
32 
33  // In ANSI-C, float literals are double by default,
34  // unless marked with 'f' (this can be overridden with
35  // config.ansi_c.single_precision_constant).
36  // Furthermore, floating-point literals can be complex.
37 
38  floatbv_typet type;
39 
40  if(parsed_float.is_float)
41  type = float_type();
42  else if(parsed_float.is_long)
43  type = long_double_type();
44  else if(parsed_float.is_float16)
45  type = gcc_float16_type();
46  else if(parsed_float.is_float32)
47  type = gcc_float32_type();
48  else if(parsed_float.is_float32x)
49  type = gcc_float32x_type();
50  else if(parsed_float.is_float64)
51  type = gcc_float64_type();
52  else if(parsed_float.is_float64x)
53  type = gcc_float64x_type();
54  else if(parsed_float.is_float80)
55  {
56  type = ieee_float_spect(64, 15).to_type();
57  type.set(ID_C_c_type, ID_long_double);
58  }
59  else if(parsed_float.is_float128)
60  type = gcc_float128_type();
61  else if(parsed_float.is_float128x)
62  type = gcc_float128x_type();
63  else
64  {
65  // default
67  type = float_type(); // default
68  else
69  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(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  constant_exprt result = a.to_expr();
88  // ieee_floatt::to_expr gives us the representation, but doesn't preserve the
89  // distinction between bitwise-identical types such as _Float32 vs. float,
90  // so ensure we preserve that here:
91  result.type() = type;
92 
93  if(parsed_float.is_imaginary)
94  {
95  const complex_typet complex_type(type);
96 
97  constant_exprt zero_real_component = ieee_floatt::zero(type).to_expr();
98  // As above, ensure we preserve the exact type of the literal:
99  zero_real_component.type() = type;
100 
101  return complex_exprt(zero_real_component, result, complex_type);
102  }
103 
104  return std::move(result);
105 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
parse_floatt
Definition: parse_float.h:20
ieee_floatt
Definition: ieee_float.h:120
parse_floatt::is_float16
bool is_float16
Definition: parse_float.h:28
parse_float.h
ANSI-C Conversion / Type Checking.
gcc_float32_type
floatbv_typet gcc_float32_type()
Definition: gcc_types.cpp:22
gcc_float64x_type
floatbv_typet gcc_float64x_type()
Definition: gcc_types.cpp:49
gcc_float16_type
floatbv_typet gcc_float16_type()
Definition: gcc_types.cpp:14
gcc_types.h
parse_floatt::is_float64
bool is_float64
Definition: parse_float.h:30
long_double_type
floatbv_typet long_double_type()
Definition: c_types.cpp:201
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1379
parse_floatt::is_float64x
bool is_float64x
Definition: parse_float.h:30
exprt
Base class for all expressions.
Definition: expr.h:53
parse_floatt::is_imaginary
bool is_imaginary
Definition: parse_float.h:28
complex_typet
Complex numbers made of pair of given subtype.
Definition: std_types.h:1790
configt::ansi_c
struct configt::ansi_ct ansi_c
parse_floatt::significand
mp_integer significand
Definition: parse_float.h:22
gcc_float128_type
floatbv_typet gcc_float128_type()
Definition: gcc_types.cpp:58
ieee_float_spect
Definition: ieee_float.h:26
gcc_float64_type
floatbv_typet gcc_float64_type()
Definition: gcc_types.cpp:40
string2int.h
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
parse_floatt::is_float128
bool is_float128
Definition: parse_float.h:32
parse_floatt::is_decimal
bool is_decimal
Definition: parse_float.h:28
convert_float_literal.h
C Language Conversion.
ieee_float_spect::to_type
class floatbv_typet to_type() const
Definition: ieee_float.cpp:25
parse_floatt::is_float32x
bool is_float32x
Definition: parse_float.h:29
std_types.h
Pre-defined types.
float_type
floatbv_typet float_type()
Definition: c_types.cpp:185
convert_float_literal
exprt convert_float_literal(const std::string &src)
build an expression from a floating-point literal
Definition: convert_float_literal.cpp:29
parse_floatt::exponent_base
unsigned exponent_base
Definition: parse_float.h:23
complex_exprt
Complex constructor from a pair of numbers.
Definition: std_expr.h:1672
ieee_floatt::from_base10
void from_base10(const mp_integer &exp, const mp_integer &frac)
compute f * (10^e)
Definition: ieee_float.cpp:482
double_type
floatbv_typet double_type()
Definition: c_types.cpp:193
config
configt config
Definition: config.cpp:24
parse_floatt::is_long
bool is_long
Definition: parse_float.h:25
parse_floatt::is_float32
bool is_float32
Definition: parse_float.h:29
parse_floatt::is_float
bool is_float
Definition: parse_float.h:25
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:442
ieee_float.h
config.h
ieee_floatt::zero
static ieee_floatt zero(const floatbv_typet &type)
Definition: ieee_float.h:184
ieee_floatt::to_expr
constant_exprt to_expr() const
Definition: ieee_float.cpp:698
parse_floatt::is_float128x
bool is_float128x
Definition: parse_float.h:32
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
configt::ansi_ct::single_precision_constant
bool single_precision_constant
Definition: config.h:48
std_expr.h
API to expression classes.
parse_floatt::is_float80
bool is_float80
Definition: parse_float.h:31
parse_floatt::exponent
mp_integer exponent
Definition: parse_float.h:22
c_types.h
gcc_float32x_type
floatbv_typet gcc_float32x_type()
Definition: gcc_types.cpp:31
gcc_float128x_type
floatbv_typet gcc_float128x_type()
Definition: gcc_types.cpp:67
ieee_floatt::build
void build(const mp_integer &exp, const mp_integer &frac)
Definition: ieee_float.cpp:468