cprover
java_types.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "java_types.h"
10 
11 #include <cassert>
12 #include <cctype>
13 
14 #include <util/std_types.h>
15 #include <util/c_types.h>
16 #include <util/std_expr.h>
17 #include <util/ieee_float.h>
18 
20 {
21  return signedbv_typet(32);
22 }
23 
25 {
26  return void_typet();
27 }
28 
30 {
31  return signedbv_typet(64);
32 }
33 
35 {
36  return signedbv_typet(16);
37 }
38 
40 {
41  return signedbv_typet(8);
42 }
43 
45 {
46  return unsignedbv_typet(16);
47 }
48 
50 {
52 }
53 
55 {
57 }
58 
60 {
61  // The Java standard doesn't really prescribe the width
62  // of a boolean. However, JNI suggests that it's 8 bits.
63  // http://docs.oracle.com/javase/7/docs/technotes/guides/jni/spec/types.html
64  return c_bool_typet(8);
65 }
66 
68 {
69  return to_reference_type(reference_type(subtype));
70 }
71 
73 {
74  return java_reference_type(symbol_typet("java::java.lang.Object"));
75 }
76 
77 reference_typet java_array_type(const char subtype)
78 {
79  std::string subtype_str;
80 
81  switch(subtype)
82  {
83  case 'b': subtype_str="byte"; break;
84  case 'f': subtype_str="float"; break;
85  case 'd': subtype_str="double"; break;
86  case 'i': subtype_str="int"; break;
87  case 'c': subtype_str="char"; break;
88  case 's': subtype_str="short"; break;
89  case 'z': subtype_str="boolean"; break;
90  case 'v': subtype_str="void"; break;
91  case 'j': subtype_str="long"; break;
92  case 'l': subtype_str="long"; break;
93  case 'a': subtype_str="reference"; break;
94  default: assert(false);
95  }
96 
97  irep_idt class_name="array["+subtype_str+"]";
98 
99  symbol_typet symbol_type("java::"+id2string(class_name));
100  symbol_type.set(ID_C_base_name, class_name);
101  symbol_type.set(ID_C_element_type, java_type_from_char(subtype));
102 
103  return java_reference_type(symbol_type);
104 }
105 
106 bool is_reference_type(const char t)
107 {
108  return 'a' == t;
109 }
110 
112 {
113  switch(t)
114  {
115  case 'i': return java_int_type();
116  case 'j': return java_long_type();
117  case 'l': return java_long_type();
118  case 's': return java_short_type();
119  case 'b': return java_byte_type();
120  case 'c': return java_char_type();
121  case 'f': return java_float_type();
122  case 'd': return java_double_type();
123  case 'z': return java_boolean_type();
124  case 'a': return java_reference_type(void_typet());
125  default: assert(false); return nil_typet();
126  }
127 }
128 
131 {
132  if(type==java_boolean_type() ||
133  type==java_char_type() ||
134  type==java_byte_type() ||
135  type==java_short_type())
136  return java_int_type();
137 
138  return type;
139 }
140 
143 {
144  typet new_type=java_bytecode_promotion(expr.type());
145 
146  if(new_type==expr.type())
147  return expr;
148  else
149  return typecast_exprt(expr, new_type);
150 }
151 
152 typet java_type_from_string(const std::string &src)
153 {
154  if(src.empty())
155  return nil_typet();
156 
157  switch(src[0])
158  {
159  case '(': // function type
160  {
161  std::size_t e_pos=src.rfind(')');
162  if(e_pos==std::string::npos)
163  return nil_typet();
164 
165  code_typet result;
166 
167  result.return_type()=
168  java_type_from_string(std::string(src, e_pos+1, std::string::npos));
169 
170  for(std::size_t i=1; i<src.size() && src[i]!=')'; i++)
171  {
173 
174  size_t start=i;
175 
176  while(i<src.size())
177  {
178  if(src[i]=='L')
179  {
180  i=src.find(';', i); // ends on ;
181  break;
182  }
183  else if(src[i]=='[')
184  i++;
185  else
186  break;
187  }
188 
189  std::string sub_str=src.substr(start, i-start+1);
190  param.type()=java_type_from_string(sub_str);
191 
192  if(param.type().id()==ID_symbol)
193  param.type()=java_reference_type(param.type());
194 
195  result.parameters().push_back(param);
196  }
197 
198  return result;
199  }
200 
201  case '[': // array type
202  {
203  // If this is a reference array, we generate a plain array[reference]
204  // with void* members, but note the real type in ID_C_element_type.
205  if(src.size()<=1)
206  return nil_typet();
207  char subtype_letter=src[1];
208  const typet subtype=
209  java_type_from_string(src.substr(1, std::string::npos));
210  if(subtype_letter=='L' || // [L denotes a reference array of some sort.
211  subtype_letter=='[') // Array-of-arrays
212  subtype_letter='A';
213  typet tmp=java_array_type(std::tolower(subtype_letter));
214  tmp.subtype().set(ID_C_element_type, subtype);
215  return tmp;
216  }
217 
218  case 'B': return java_byte_type();
219  case 'F': return java_float_type();
220  case 'D': return java_double_type();
221  case 'I': return java_int_type();
222  case 'C': return java_char_type();
223  case 'S': return java_short_type();
224  case 'Z': return java_boolean_type();
225  case 'V': return java_void_type();
226  case 'J': return java_long_type();
227 
228  case 'L':
229  {
230  // ends on ;
231  if(src[src.size()-1]!=';')
232  return nil_typet();
233  std::string class_name=src.substr(1, src.size()-2);
234 
235  for(unsigned i=0; i<class_name.size(); i++)
236  if(class_name[i]=='/')
237  class_name[i]='.';
238 
239  std::string identifier="java::"+class_name;
240 
241  reference_typet result;
242  result.subtype()=symbol_typet(identifier);
243  result.subtype().set(ID_C_base_name, class_name);
244  return result;
245  }
246 
247  default:
248  return nil_typet();
249  }
250 }
251 
252 char java_char_from_type(const typet &type)
253 {
254  const irep_idt &id=type.id();
255 
256  if(id==ID_signedbv)
257  {
258  const size_t width=to_signedbv_type(type).get_width();
259  if(to_signedbv_type(java_int_type()).get_width()==width)
260  return 'i';
261  else if(to_signedbv_type(java_long_type()).get_width()==width)
262  return 'l';
263  else if(to_signedbv_type(java_short_type()).get_width()==width)
264  return 's';
265  else if(to_signedbv_type(java_byte_type()).get_width()==width)
266  return 'b';
267  }
268  else if(id==ID_unsignedbv)
269  return 'c';
270  else if(id==ID_floatbv)
271  {
272  const size_t width(to_floatbv_type(type).get_width());
273  if(to_floatbv_type(java_float_type()).get_width()==width)
274  return 'f';
275  else if(to_floatbv_type(java_double_type()).get_width()==width)
276  return 'd';
277  }
278  else if(id==ID_c_bool)
279  return 'z';
280 
281  return 'a';
282 }
283 
284 // java/lang/Object -> java.lang.Object
285 static std::string slash_to_dot(const std::string &src)
286 {
287  std::string result=src;
288  for(std::string::iterator it=result.begin(); it!=result.end(); it++)
289  if(*it=='/')
290  *it='.';
291  return result;
292 }
293 
294 symbol_typet java_classname(const std::string &id)
295 {
296  if(!id.empty() && id[0]=='[')
297  return to_symbol_type(java_type_from_string(id).subtype());
298 
299  std::string class_name=id;
300 
301  class_name=slash_to_dot(class_name);
302  irep_idt identifier="java::"+class_name;
303  symbol_typet symbol_type(identifier);
304  symbol_type.set(ID_C_base_name, class_name);
305 
306  return symbol_type;
307 }
The void type.
Definition: std_types.h:63
The type of an expression.
Definition: type.h:20
Fixed-width bit-vector with unsigned binary interpretation.
Definition: std_types.h:1125
semantic type conversion
Definition: std_expr.h:1725
Base type of functions.
Definition: std_types.h:734
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
typet java_boolean_type()
Definition: java_types.cpp:59
typet java_double_type()
Definition: java_types.cpp:54
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:67
typet java_int_type()
Definition: java_types.cpp:19
typet java_long_type()
Definition: java_types.cpp:29
typet & type()
Definition: expr.h:60
reference_typet java_array_type(const char subtype)
Definition: java_types.cpp:77
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Definition: std_types.h:1286
reference_typet java_lang_object_type()
Definition: java_types.cpp:72
static ieee_float_spect double_precision()
Definition: ieee_float.h:69
class floatbv_typet to_type() const
Definition: ieee_float.cpp:26
const irep_idt & id() const
Definition: irep.h:189
typet java_type_from_string(const std::string &src)
Definition: java_types.cpp:152
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:142
A reference into the symbol table.
Definition: std_types.h:109
reference_typet reference_type(const typet &subtype)
Definition: c_types.cpp:301
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1171
typet java_type_from_char(char t)
Definition: java_types.cpp:111
API to expression classes.
static ieee_float_spect single_precision()
Definition: ieee_float.h:63
typet java_byte_type()
Definition: java_types.cpp:39
typet java_short_type()
Definition: java_types.cpp:34
bool is_reference_type(const char t)
Definition: java_types.cpp:106
std::size_t get_width() const
Definition: std_types.h:1030
The reference type.
Definition: std_types.h:1394
const reference_typet & to_reference_type(const typet &type)
Cast a generic typet to a reference_typet.
Definition: std_types.h:1426
API to type classes.
static std::string slash_to_dot(const std::string &src)
Definition: java_types.cpp:285
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1200
The NIL type.
Definition: std_types.h:43
typet java_void_type()
Definition: java_types.cpp:24
typet java_bytecode_promotion(const typet &type)
Java does not support byte/short return types. These are always promoted.
Definition: java_types.cpp:130
typet java_char_type()
Definition: java_types.cpp:44
The C/C++ Booleans.
Definition: std_types.h:1450
const typet & subtype() const
Definition: type.h:31
symbol_typet java_classname(const std::string &id)
Definition: java_types.cpp:294
typet java_float_type()
Definition: java_types.cpp:49
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
const typet & return_type() const
Definition: std_types.h:831
char java_char_from_type(const typet &type)
Definition: java_types.cpp:252
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214