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