CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
parse_float.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Conversion of Expressions
4
5Author: 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
18parse_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,
41
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
52
53 // get whole number part
54 while(*p!='.' && *p!=0 && *p!='p')
55 {
57 p++;
58 }
59
60 // skip dot
61 if(*p=='.')
62 p++;
63
64 // get fraction part
65 while(*p!=0 && *p!='p')
66 {
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+
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())
96 else
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 {
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 {
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+
149
150 if(str_number.empty())
151 significand=0;
152 else
154
155 if(str_exponent.empty())
156 exponent=0;
157 else
159
160 // adjust exponent
162 }
163
164 // get flags
165 is_float=is_long=false;
167 is_float16=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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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 &)
mp_integer exponent
Definition parse_float.h:22
bool is_float128x
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