cprover
expr2java.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@cs.cmu.edu
6 
7 \*******************************************************************/
8 
9 #include "expr2java.h"
10 
11 #include <cassert>
12 #include <sstream>
13 
14 #include <util/namespace.h>
15 #include <util/std_types.h>
16 #include <util/std_expr.h>
17 #include <util/symbol.h>
18 #include <util/unicode.h>
19 #include <util/arith_tools.h>
20 #include <util/ieee_float.h>
21 
22 #include <ansi-c/c_misc.h>
23 #include <ansi-c/expr2c_class.h>
24 
25 #include "java_qualifiers.h"
26 #include "java_types.h"
27 
28 std::string expr2javat::convert(const typet &src)
29 {
30  return convert_rec(src, java_qualifierst(ns), "");
31 }
32 
33 std::string expr2javat::convert(const exprt &src)
34 {
35  return expr2ct::convert(src);
36 }
37 
39  const code_function_callt &src,
40  unsigned indent)
41 {
42  if(src.operands().size()!=3)
43  {
44  unsigned precedence;
45  return convert_norep(src, precedence);
46  }
47 
48  std::string dest=indent_str(indent);
49 
50  if(src.lhs().is_not_nil())
51  {
52  unsigned p;
53  std::string lhs_str=convert_with_precedence(src.lhs(), p);
54 
55  dest+=lhs_str;
56  dest+='=';
57  }
58 
59  const java_method_typet &method_type =
61 
62  bool has_this = method_type.has_this() && !src.arguments().empty();
63 
64  if(has_this)
65  {
66  unsigned p;
67  std::string this_str=convert_with_precedence(src.arguments()[0], p);
68  dest+=this_str;
69  dest+=" . "; // extra spaces for readability
70  }
71 
72  {
73  unsigned p;
74  std::string function_str=convert_with_precedence(src.function(), p);
75  dest+=function_str;
76  }
77 
78  dest+='(';
79 
80  const exprt::operandst &arguments=src.arguments();
81 
82  bool first=true;
83 
84  forall_expr(it, arguments)
85  {
86  if(has_this && it==arguments.begin())
87  {
88  }
89  else
90  {
91  unsigned p;
92  std::string arg_str=convert_with_precedence(*it, p);
93 
94  if(first)
95  first=false;
96  else
97  dest+=", ";
98  dest+=arg_str;
99  }
100  }
101 
102  dest+=");";
103 
104  return dest;
105 }
106 
108  const exprt &src,
109  unsigned &precedence)
110 {
111  const typet &full_type=ns.follow(src.type());
112 
113  if(full_type.id()!=ID_struct)
114  return convert_norep(src, precedence);
115 
116  const struct_typet &struct_type=to_struct_type(full_type);
117 
118  std::string dest="{ ";
119 
120  const struct_typet::componentst &components=
121  struct_type.components();
122 
123  assert(components.size()==src.operands().size());
124 
125  exprt::operandst::const_iterator o_it=src.operands().begin();
126 
127  bool first=true;
128  size_t last_size=0;
129 
130  for(struct_typet::componentst::const_iterator
131  c_it=components.begin();
132  c_it!=components.end();
133  c_it++)
134  {
135  if(c_it->type().id()==ID_code)
136  {
137  }
138  else
139  {
140  std::string tmp=convert(*o_it);
141  std::string sep;
142 
143  if(first)
144  first=false;
145  else
146  {
147  if(last_size+40<dest.size())
148  {
149  sep=",\n ";
150  last_size=dest.size();
151  }
152  else
153  sep=", ";
154  }
155 
156  dest+=sep;
157  dest+='.';
158  dest+=c_it->get_string(ID_pretty_name);
159  dest+='=';
160  dest+=tmp;
161  }
162 
163  o_it++;
164  }
165 
166  dest+=" }";
167 
168  return dest;
169 }
170 
172  const constant_exprt &src,
173  unsigned &precedence)
174 {
175  if(src.type().id()==ID_c_bool)
176  {
177  if(!src.is_zero())
178  return "true";
179  else
180  return "false";
181  }
182  else if(src.type().id()==ID_bool)
183  {
184  if(src.is_true())
185  return "true";
186  else if(src.is_false())
187  return "false";
188  }
189  else if(src.type().id()==ID_pointer)
190  {
191  // Java writes 'null' for the null reference
192  if(src.is_zero())
193  return "null";
194  }
195  else if(src.type()==java_char_type())
196  {
197  std::string dest;
198  dest.reserve(char_representation_length);
199 
200  mp_integer int_value;
201  if(to_integer(src, int_value))
202  UNREACHABLE;
203 
204  dest += "(char)'" + utf16_native_endian_to_java(int_value.to_long()) + '\'';
205  return dest;
206  }
207  else if(src.type()==java_byte_type())
208  {
209  // No byte-literals in Java, so just cast:
210  mp_integer int_value;
211  if(to_integer(src, int_value))
212  UNREACHABLE;
213  std::string dest="(byte)";
214  dest+=integer2string(int_value);
215  return dest;
216  }
217  else if(src.type()==java_short_type())
218  {
219  // No short-literals in Java, so just cast:
220  mp_integer int_value;
221  if(to_integer(src, int_value))
222  UNREACHABLE;
223  std::string dest="(short)";
224  dest+=integer2string(int_value);
225  return dest;
226  }
227  else if(src.type()==java_long_type())
228  {
229  // long integer literals must have 'L' at the end
230  mp_integer int_value;
231  if(to_integer(src, int_value))
232  UNREACHABLE;
233  std::string dest=integer2string(int_value);
234  dest+='L';
235  return dest;
236  }
237  else if((src.type()==java_float_type()) ||
238  (src.type()==java_double_type()))
239  {
240  // This converts NaNs to the canonical NaN
241  const ieee_floatt ieee_repr(to_constant_expr(src));
242  if(ieee_repr.is_double())
243  return floating_point_to_java_string(ieee_repr.to_double());
244  return floating_point_to_java_string(ieee_repr.to_float());
245  }
246 
247 
248  return expr2ct::convert_constant(src, precedence);
249 }
250 
252  const typet &src,
253  const qualifierst &qualifiers,
254  const std::string &declarator)
255 {
256  std::unique_ptr<qualifierst> clone = qualifiers.clone();
257  qualifierst &new_qualifiers = *clone;
258  new_qualifiers.read(src);
259 
260  const std::string d=
261  declarator==""?declarator:(" "+declarator);
262 
263  const std::string q=
264  new_qualifiers.as_string();
265 
266  if(src==java_int_type())
267  return q+"int"+d;
268  else if(src==java_long_type())
269  return q+"long"+d;
270  else if(src==java_short_type())
271  return q+"short"+d;
272  else if(src==java_byte_type())
273  return q+"byte"+d;
274  else if(src==java_char_type())
275  return q+"char"+d;
276  else if(src==java_float_type())
277  return q+"float"+d;
278  else if(src==java_double_type())
279  return q+"double"+d;
280  else if(src==java_boolean_type())
281  return q+"boolean"+d;
282  else if(src==java_byte_type())
283  return q+"byte"+d;
284  else if(src.id()==ID_code)
285  {
286  const java_method_typet &method_type = to_java_method_type(src);
287 
288  // Java doesn't really have syntax for function types,
289  // so we make one up, loosely inspired by the syntax
290  // of lambda expressions.
291 
292  std::string dest="";
293 
294  dest+='(';
295  const java_method_typet::parameterst &parameters = method_type.parameters();
296 
297  for(java_method_typet::parameterst::const_iterator it = parameters.begin();
298  it != parameters.end();
299  it++)
300  {
301  if(it!=parameters.begin())
302  dest+=", ";
303 
304  dest+=convert(it->type());
305  }
306 
307  if(method_type.has_ellipsis())
308  {
309  if(!parameters.empty())
310  dest+=", ";
311  dest+="...";
312  }
313 
314  dest+=')';
315 
316  const typet &return_type = method_type.return_type();
317  dest+=" -> "+convert(return_type);
318 
319  return q + dest;
320  }
321  else
322  return expr2ct::convert_rec(src, qualifiers, declarator);
323 }
324 
326  const exprt &src,
327  unsigned precedence)
328 {
329  return "this";
330 }
331 
333  const exprt &src,
334  unsigned precedence)
335 {
336  if(src.operands().size()!=2)
337  {
338  unsigned precedence;
339  return convert_norep(src, precedence);
340  }
341 
342  return convert(src.op0())+" instanceof "+convert(src.op1().type());
343 }
344 
346  const exprt &src,
347  unsigned precedence)
348 {
349  std::string dest;
350 
351  if(src.get(ID_statement)==ID_java_new_array ||
352  src.get(ID_statement)==ID_java_new_array_data)
353  {
354  dest="new";
355 
356  std::string tmp_size=
357  convert(static_cast<const exprt &>(src.find(ID_size)));
358 
359  dest+=' ';
360  dest+=convert(src.type().subtype());
361  dest+='[';
362  dest+=tmp_size;
363  dest+=']';
364  }
365  else
366  dest="new "+convert(src.type().subtype());
367 
368  return dest;
369 }
370 
372  const exprt &src,
373  unsigned indent)
374 {
375  std::string dest=indent_str(indent)+"delete ";
376 
377  if(src.operands().size()!=1)
378  {
379  unsigned precedence;
380  return convert_norep(src, precedence);
381  }
382 
383  std::string tmp=convert(src.op0());
384 
385  dest+=tmp+";\n";
386 
387  return dest;
388 }
389 
391  const exprt &src,
392  unsigned &precedence)
393 {
394  if(src.id()=="java-this")
395  return convert_java_this(src, precedence=15);
396  if(src.id()==ID_java_instanceof)
397  return convert_java_instanceof(src, precedence=15);
398  else if(src.id()==ID_side_effect &&
399  (src.get(ID_statement)==ID_java_new ||
400  src.get(ID_statement)==ID_java_new_array ||
401  src.get(ID_statement)==ID_java_new_array_data))
402  return convert_java_new(src, precedence=15);
403  else if(src.id()==ID_side_effect &&
404  src.get(ID_statement)==ID_throw)
405  return convert_function(src, "throw", precedence=16);
406  else if(src.id()==ID_code &&
407  to_code(src).get_statement()==ID_exception_landingpad)
408  {
409  const exprt &catch_expr=
411  return "catch_landingpad("+
412  convert(catch_expr.type())+
413  ' '+
414  convert(catch_expr)+
415  ')';
416  }
417  else if(src.id()==ID_unassigned)
418  return "?";
419  else if(src.id()=="pod_constructor")
420  return "pod_constructor";
421  else if(src.id()==ID_virtual_function)
422  {
423  return "VIRTUAL_FUNCTION(" +
424  id2string(src.get(ID_C_class)) +
425  "." +
426  id2string(src.get(ID_component_name)) +
427  ")";
428  }
429  else if(src.id()==ID_java_string_literal)
430  return '"'+MetaString(src.get_string(ID_value))+'"';
431  else if(src.id()==ID_constant)
432  return convert_constant(to_constant_expr(src), precedence=16);
433  else
434  return expr2ct::convert_with_precedence(src, precedence);
435 }
436 
438  const codet &src,
439  unsigned indent)
440 {
441  const irep_idt &statement=src.get(ID_statement);
442 
443  if(statement==ID_java_new ||
444  statement==ID_java_new_array)
445  return convert_java_new(src, indent);
446 
447  if(statement==ID_function_call)
449 
450  return expr2ct::convert_code(src, indent);
451 }
452 
453 std::string expr2java(const exprt &expr, const namespacet &ns)
454 {
455  expr2javat expr2java(ns);
456  expr2java.get_shorthands(expr);
457  return expr2java.convert(expr);
458 }
459 
460 std::string type2java(const typet &type, const namespacet &ns)
461 {
462  expr2javat expr2java(ns);
463  return expr2java.convert(type);
464 }
Java-specific type qualifiers.
const irep_idt & get_statement() const
Definition: std_code.h:40
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:390
The type of an expression.
Definition: type.h:22
virtual std::string convert_struct(const exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:107
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:460
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:166
BigInt mp_integer
Definition: mp_arith.h:22
std::string convert_java_new(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:345
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
std::vector< parametert > parameterst
Definition: std_types.h:767
Symbol table entry.
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106
std::string convert_function(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1242
typet java_boolean_type()
Definition: java_types.cpp:72
exprt & op0()
Definition: expr.h:72
typet java_double_type()
Definition: java_types.cpp:67
virtual void read(const typet &src)=0
bool has_ellipsis() const
Definition: std_types.h:861
std::string convert_code_java_delete(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:371
typet java_int_type()
Definition: java_types.cpp:32
std::string convert_java_instanceof(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:332
#define forall_expr(it, expr)
Definition: expr.h:28
std::vector< componentt > componentst
Definition: std_types.h:243
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:171
bool is_false() const
Definition: expr.cpp:131
const componentst & components() const
Definition: std_types.h:245
virtual std::string convert_code(const codet &src, unsigned indent) override
Definition: expr2java.cpp:437
ANSI-C Misc Utilities.
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3342
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
Definition: expr2java.cpp:251
bool is_true() const
Definition: expr.cpp:124
typet java_long_type()
Definition: java_types.cpp:42
typet & type()
Definition: expr.h:56
A constant literal expression.
Definition: std_expr.h:4422
Structure type.
Definition: std_types.h:297
std::string floating_point_to_java_string(float_type value)
Convert floating point number to a string without printing unnecessary zeros.
Definition: expr2java.h:59
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:161
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1766
const irep_idt & id() const
Definition: irep.h:259
static void utf16_native_endian_to_java(const wchar_t ch, std::ostringstream &result, const std::locale &loc)
Definition: unicode.cpp:253
argumentst & arguments()
Definition: std_code.h:890
virtual std::unique_ptr< qualifierst > clone() const =0
API to expression classes.
double to_double() const
Note that calling from_double -> to_double can return different bit patterns for NaN.
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A function call.
Definition: std_code.h:858
const namespacet & ns
Definition: expr2c_class.h:35
const std::size_t char_representation_length
Definition: expr2java.h:49
typet java_byte_type()
Definition: java_types.cpp:52
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
typet java_short_type()
Definition: java_types.cpp:47
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
std::vector< exprt > operandst
Definition: expr.h:45
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1642
API to type classes.
virtual std::string convert(const typet &src) override
Definition: expr2java.cpp:28
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:289
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:1693
exprt & function()
Definition: std_code.h:878
virtual std::string as_string() const =0
Base class for all expressions.
Definition: expr.h:42
const parameterst & parameters() const
Definition: std_types.h:905
bool has_this() const
Definition: std_types.h:866
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3436
#define UNREACHABLE
Definition: invariant.h:271
bool is_double() const
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:272
bool is_zero() const
Definition: expr.cpp:161
const codet & to_code(const exprt &expr)
Definition: std_code.h:75
const exprt & catch_expr() const
Definition: std_code.h:1675
std::string MetaString(const std::string &in)
Definition: c_misc.cpp:95
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2java.cpp:38
A statement in a programming language.
Definition: std_code.h:21
typet java_char_type()
Definition: java_types.cpp:57
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
std::string convert_java_this(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:325
typet java_float_type()
Definition: java_types.cpp:62
const irept & find(const irep_namet &name) const
Definition: irep.cpp:285
float to_float() const
Note that calling from_float -> to_float can return different bit patterns for NaN.
const typet & return_type() const
Definition: std_types.h:895
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2439
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:453
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909