CBMC
parse_float.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Conversion of Expressions
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "parse_float.h"
13 
14 #include <algorithm>
15 #include <cctype>
16 #include <cstring>
17 
18 parse_floatt::parse_floatt(const std::string &src)
19 {
20  // {digits}{dot}{digits}{exponent}?{floatsuffix}?
21  // {digits}{dot}{exponent}?{floatsuffix}?
22  // {dot}{digits}{exponent}?{floatsuffix}?
23  // {digits}{exponent}{floatsuffix}?
24 
25  // Hex format (C99):
26  // 0x{hexdigits}{dot}{hexdigits}[pP]{exponent}{floatsuffix}?
27  // 0x{hexdigits}{dot}[pP]{exponent}{floatsuffix}?
28 
29  // These are case-insensitive, and we handle this
30  // by first converting to lower case.
31 
32  std::string src_lower=src;
33  std::transform(src_lower.begin(), src_lower.end(),
34  src_lower.begin(), ::tolower);
35 
36  const char *p=src_lower.c_str();
37 
38  std::string str_whole_number,
39  str_fraction_part,
40  str_exponent;
41 
42  exponent_base=10;
43 
44  // is this hex?
45 
46  if(src_lower.size()>=2 && src_lower[0]=='0' && src_lower[1]=='x')
47  {
48  // skip the 0x
49  p+=2;
50 
51  exponent_base=2;
52 
53  // get whole number part
54  while(*p!='.' && *p!=0 && *p!='p')
55  {
56  str_whole_number+=*p;
57  p++;
58  }
59 
60  // skip dot
61  if(*p=='.')
62  p++;
63 
64  // get fraction part
65  while(*p!=0 && *p!='p')
66  {
67  str_fraction_part+=*p;
68  p++;
69  }
70 
71  // skip p
72  if(*p=='p')
73  p++;
74 
75  // skip +
76  if(*p=='+')
77  p++;
78 
79  // get exponent
80  while(*p != 0 && *p != 'f' && *p != 'l' && *p != 'w' && *p != 'q' &&
81  *p != 'd' && *p != 'b')
82  {
83  str_exponent+=*p;
84  p++;
85  }
86 
87  std::string str_number=str_whole_number+
88  str_fraction_part;
89 
90  // The significand part is interpreted as a (decimal or hexadecimal)
91  // rational number; the digit sequence in the exponent part is
92  // interpreted as a decimal integer.
93 
94  if(str_number.empty())
95  significand=0;
96  else
97  significand=string2integer(str_number, 16); // hex
98 
99  if(str_exponent.empty())
100  exponent=0;
101  else
102  exponent=string2integer(str_exponent, 10); // decimal
103 
104  // adjust exponent
105  exponent-=str_fraction_part.size()*4; // each digit has 4 bits
106  }
107  else
108  {
109  // get whole number part
110  while(*p!='.' && *p!=0 && *p!='e' &&
111  *p!='f' && *p!='l' &&
112  *p!='w' && *p!='q' && *p!='d' &&
113  *p!='i' && *p!='j')
114  {
115  str_whole_number+=*p;
116  p++;
117  }
118 
119  // skip dot
120  if(*p=='.')
121  p++;
122 
123  // get fraction part
124  while(*p != 0 && *p != 'e' && *p != 'f' && *p != 'l' && *p != 'w' &&
125  *p != 'q' && *p != 'd' && *p != 'i' && *p != 'j' && *p != 'b')
126  {
127  str_fraction_part+=*p;
128  p++;
129  }
130 
131  // skip e
132  if(*p=='e')
133  p++;
134 
135  // skip +
136  if(*p=='+')
137  p++;
138 
139  // get exponent
140  while(*p != 0 && *p != 'f' && *p != 'l' && *p != 'w' && *p != 'q' &&
141  *p != 'd' && *p != 'i' && *p != 'j' && *p != 'b')
142  {
143  str_exponent+=*p;
144  p++;
145  }
146 
147  std::string str_number=str_whole_number+
148  str_fraction_part;
149 
150  if(str_number.empty())
151  significand=0;
152  else
153  significand=string2integer(str_number, 10);
154 
155  if(str_exponent.empty())
156  exponent=0;
157  else
158  exponent=string2integer(str_exponent, 10);
159 
160  // adjust exponent
161  exponent-=str_fraction_part.size();
162  }
163 
164  // get flags
165  is_float=is_long=false;
166  is_imaginary=is_decimal=false;
167  is_float16=false;
168  is_float32=is_float32x=false;
169  is_float64=is_float64x=false;
170  is_float80=false;
172 
173  if(strcmp(p, "f16") == 0 || strcmp(p, "bf16") == 0)
174  is_float16=true;
175  else if(strcmp(p, "f32")==0)
176  is_float32=true;
177  else if(strcmp(p, "f32x")==0)
178  is_float32x=true;
179  else if(strcmp(p, "f64")==0)
180  is_float64=true;
181  else if(strcmp(p, "f64x")==0)
182  is_float64x=true;
183  else if(strcmp(p, "f128")==0)
184  is_float128=true;
185  else if(strcmp(p, "f128x")==0)
186  is_float128x=true;
187  else
188  {
189  while(*p!=0)
190  {
191  if(*p=='f')
192  is_float=true;
193  else if(*p=='l')
194  is_long=true;
195  else if(*p=='i' || *p=='j')
196  is_imaginary=true;
197  // http://gcc.gnu.org/onlinedocs/gcc/Decimal-Float.html
198  else if(*p=='d')
199  // a suffix with just d or D but nothing else is a GCC extension with no
200  // particular effect -- and forbidden by Clang
201  is_decimal=is_decimal || *(p+1)!=0;
202  // http://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
203  else if(*p=='w')
204  is_float80=true;
205  else if(*p=='q')
206  is_float128=true;
207 
208  p++;
209  }
210  }
211 }
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
bool is_imaginary
Definition: parse_float.h:28
unsigned exponent_base
Definition: parse_float.h:23
mp_integer significand
Definition: parse_float.h:22
parse_floatt(const std::string &)
Definition: parse_float.cpp:18
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
int tolower(int c)
Definition: ctype.c:109
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
ANSI-C Conversion / Type Checking.
int strcmp(const char *s1, const char *s2)
Definition: string.c:363