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' &&
81  *p!='w' && *p!='q' && *p!='d')
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' &&
125  *p!='f' && *p!='l' &&
126  *p!='w' && *p!='q' && *p!='d' &&
127  *p!='i' && *p!='j')
128  {
129  str_fraction_part+=*p;
130  p++;
131  }
132 
133  // skip e
134  if(*p=='e')
135  p++;
136 
137  // skip +
138  if(*p=='+')
139  p++;
140 
141  // get exponent
142  while(*p!=0 && *p!='f' && *p!='l' &&
143  *p!='w' && *p!='q' && *p!='d' &&
144  *p!='i' && *p!='j')
145  {
146  str_exponent+=*p;
147  p++;
148  }
149 
150  std::string str_number=str_whole_number+
151  str_fraction_part;
152 
153  if(str_number.empty())
154  significand=0;
155  else
156  significand=string2integer(str_number, 10);
157 
158  if(str_exponent.empty())
159  exponent=0;
160  else
161  exponent=string2integer(str_exponent, 10);
162 
163  // adjust exponent
164  exponent-=str_fraction_part.size();
165  }
166 
167  // get flags
168  is_float=is_long=false;
169  is_imaginary=is_decimal=false;
170  is_float16=false;
171  is_float32=is_float32x=false;
172  is_float64=is_float64x=false;
173  is_float80=false;
175 
176  if(strcmp(p, "f16")==0)
177  is_float16=true;
178  else if(strcmp(p, "f32")==0)
179  is_float32=true;
180  else if(strcmp(p, "f32x")==0)
181  is_float32x=true;
182  else if(strcmp(p, "f64")==0)
183  is_float64=true;
184  else if(strcmp(p, "f64x")==0)
185  is_float64x=true;
186  else if(strcmp(p, "f128")==0)
187  is_float128=true;
188  else if(strcmp(p, "f128x")==0)
189  is_float128x=true;
190  else
191  {
192  while(*p!=0)
193  {
194  if(*p=='f')
195  is_float=true;
196  else if(*p=='l')
197  is_long=true;
198  else if(*p=='i' || *p=='j')
199  is_imaginary=true;
200  // http://gcc.gnu.org/onlinedocs/gcc/Decimal-Float.html
201  else if(*p=='d')
202  // a suffix with just d or D but nothing else is a GCC extension with no
203  // particular effect -- and forbidden by Clang
204  is_decimal=is_decimal || *(p+1)!=0;
205  // http://gcc.gnu.org/onlinedocs/gcc/Floating-Types.html
206  else if(*p=='w')
207  is_float80=true;
208  else if(*p=='q')
209  is_float128=true;
210 
211  p++;
212  }
213  }
214 }
parse_floatt::is_float16
bool is_float16
Definition: parse_float.h:28
parse_float.h
transform
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
Definition: abstract_value_object.cpp:159
parse_floatt::is_float64
bool is_float64
Definition: parse_float.h:30
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
parse_floatt::is_float64x
bool is_float64x
Definition: parse_float.h:30
parse_floatt::is_imaginary
bool is_imaginary
Definition: parse_float.h:28
parse_floatt::significand
mp_integer significand
Definition: parse_float.h:22
parse_floatt::parse_floatt
parse_floatt(const std::string &)
Definition: parse_float.cpp:18
parse_floatt::is_float128
bool is_float128
Definition: parse_float.h:32
parse_floatt::is_decimal
bool is_decimal
Definition: parse_float.h:28
parse_floatt::is_float32x
bool is_float32x
Definition: parse_float.h:29
parse_floatt::exponent_base
unsigned exponent_base
Definition: parse_float.h:23
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
parse_floatt::is_float128x
bool is_float128x
Definition: parse_float.h:32
parse_floatt::is_float80
bool is_float80
Definition: parse_float.h:31
parse_floatt::exponent
mp_integer exponent
Definition: parse_float.h:22