CBMC
convert_integer_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 
13 
14 #include <cctype>
15 
16 #include <util/arith_tools.h>
17 #include <util/config.h>
18 #include <util/std_expr.h>
19 #include <util/string2int.h>
20 
21 exprt convert_integer_literal(const std::string &src)
22 {
23  bool is_unsigned=false, is_imaginary=false;
24  unsigned long_cnt=0;
25  unsigned width_suffix=0;
26  unsigned base=10;
27 
28  for(unsigned i=0; i<src.size(); i++)
29  {
30  char ch=src[i];
31 
32  if(ch=='u' || ch=='U')
33  is_unsigned=true;
34  else if(ch=='l' || ch=='L')
35  long_cnt++;
36  else if(ch=='i' || ch=='I')
37  {
38  // This can be "1i128" in MS mode,
39  // and "10i" (imaginary) for GCC.
40  // If it's followed by a number, we do MS mode.
41  if((i+1)<src.size() && isdigit(src[i+1]))
42  width_suffix=unsafe_string2unsigned(src.substr(i+1));
43  else
44  is_imaginary=true;
45  }
46  else if(ch=='j' || ch=='J')
47  is_imaginary=true;
48  }
49 
50  mp_integer value;
51 
52  if(src.size()>=2 && src[0]=='0' && tolower(src[1])=='x')
53  {
54  // hex; strip "0x"
55  base=16;
56  std::string without_prefix(src, 2, std::string::npos);
57  value=string2integer(without_prefix, 16);
58  }
59  else if(src.size()>=2 && src[0]=='0' && tolower(src[1])=='b')
60  {
61  // binary; strip "0x"
62  // see http://gcc.gnu.org/onlinedocs/gcc/Binary-constants.html
63  base=2;
64  std::string without_prefix(src, 2, std::string::npos);
65  value=string2integer(without_prefix, 2);
66  }
67  else if(src.size()>=2 && src[0]=='0' && isdigit(src[1]))
68  {
69  // octal
70  base=8;
71  value=string2integer(src, 8);
72  }
73  else
74  {
75  // The default is base 10.
76  value=string2integer(src, 10);
77  }
78 
79  if(width_suffix!=0)
80  {
81  // this is a Microsoft extension
82  irep_idt c_type;
83 
84  if(width_suffix<=config.ansi_c.int_width)
85  c_type=is_unsigned?ID_unsigned_int:ID_signed_int;
86  else if(width_suffix<=config.ansi_c.long_int_width)
87  c_type=is_unsigned?ID_unsigned_long_int:ID_signed_long_int;
88  else
89  c_type=is_unsigned?ID_unsigned_long_long_int:ID_signed_long_long_int;
90 
91  bitvector_typet type(
92  is_unsigned ? ID_unsignedbv : ID_signedbv, width_suffix);
93  type.set(ID_C_c_type, c_type);
94 
95  exprt result=from_integer(value, type);
96 
97  return result;
98  }
99 
100  mp_integer value_abs=value;
101 
102  if(value<0)
103  value_abs.negate();
104 
105  bool is_hex_or_oct_or_bin=(base==8) || (base==16) || (base==2);
106 
107  #define FITS(width, signed) \
108  ((signed?!is_unsigned:(is_unsigned || is_hex_or_oct_or_bin)) && \
109  (power(2, signed?width-1:width)>value_abs))
110 
111  unsigned width;
112  bool is_signed=false;
113  irep_idt c_type;
114 
115  if(FITS(config.ansi_c.int_width, true) && long_cnt==0) // int
116  {
117  width=config.ansi_c.int_width;
118  is_signed=true;
119  c_type=ID_signed_int;
120  }
121  else if(FITS(config.ansi_c.int_width, false) && long_cnt==0) // unsigned int
122  {
123  width=config.ansi_c.int_width;
124  is_signed=false;
125  c_type=ID_unsigned_int;
126  }
127  else if(FITS(config.ansi_c.long_int_width, true) && long_cnt!=2) // long int
128  {
130  is_signed=true;
131  c_type=ID_signed_long_int;
132  }
133  // unsigned long int
134  else if(FITS(config.ansi_c.long_int_width, false) && long_cnt!=2)
135  {
137  is_signed=false;
138  c_type=ID_unsigned_long_int;
139  }
140  else if(FITS(config.ansi_c.long_long_int_width, true)) // long long int
141  {
143  is_signed=true;
144  c_type=ID_signed_long_long_int;
145  }
146  // unsigned long long int
147  else if(FITS(config.ansi_c.long_long_int_width, false))
148  {
150  is_signed=false;
151  c_type=ID_unsigned_long_long_int;
152  }
153  else
154  {
155  // Way too large. Should consider issuing a warning.
157 
158  if(is_unsigned)
159  {
160  is_signed=false;
161  c_type=ID_unsigned_long_long_int;
162  }
163  else
164  c_type=ID_signed_long_long_int;
165  }
166 
167  bitvector_typet type(is_signed ? ID_signedbv : ID_unsignedbv, width);
168  type.set(ID_C_c_type, c_type);
169 
170  exprt result;
171 
172  if(is_imaginary)
173  {
174  result = complex_exprt(
175  from_integer(0, type), from_integer(value, type), complex_typet(type));
176  }
177  else
178  {
179  result=from_integer(value, type);
180  result.set(ID_C_base, base);
181  }
182 
183  return result;
184 }
configt config
Definition: config.cpp:25
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Base class of fixed-width bit-vector types.
Definition: std_types.h:909
Complex constructor from a pair of numbers.
Definition: std_expr.h:1916
Complex numbers made of pair of given subtype.
Definition: std_types.h:1130
struct configt::ansi_ct ansi_c
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
void set(const irep_idt &name, const irep_idt &value)
Definition: irep.h:412
#define FITS(width, signed)
exprt convert_integer_literal(const std::string &src)
C++ Language Conversion.
int isdigit(int c)
Definition: ctype.c:24
int tolower(int c)
Definition: ctype.c:109
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
BigInt mp_integer
Definition: smt_terms.h:17
API to expression classes.
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:35
std::size_t long_long_int_width
Definition: config.h:142
std::size_t long_int_width
Definition: config.h:138
std::size_t int_width
Definition: config.h:137
bool is_signed(const typet &t)
Convenience function – is the type signed?
Definition: util.cpp:45
bool is_unsigned(const typet &t)
Convenience function – is the type unsigned?
Definition: util.cpp:52