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 code_typet &code_type=
60  to_code_type(src.function().type());
61 
62  bool has_this=code_type.has_this() &&
63  !src.arguments().empty();
64 
65  if(has_this)
66  {
67  unsigned p;
68  std::string this_str=convert_with_precedence(src.arguments()[0], p);
69  dest+=this_str;
70  dest+=" . "; // extra spaces for readability
71  }
72 
73  {
74  unsigned p;
75  std::string function_str=convert_with_precedence(src.function(), p);
76  dest+=function_str;
77  }
78 
79  dest+='(';
80 
81  const exprt::operandst &arguments=src.arguments();
82 
83  bool first=true;
84 
85  forall_expr(it, arguments)
86  {
87  if(has_this && it==arguments.begin())
88  {
89  }
90  else
91  {
92  unsigned p;
93  std::string arg_str=convert_with_precedence(*it, p);
94 
95  if(first)
96  first=false;
97  else
98  dest+=", ";
99  dest+=arg_str;
100  }
101  }
102 
103  dest+=");";
104 
105  return dest;
106 }
107 
109  const exprt &src,
110  unsigned &precedence)
111 {
112  const typet &full_type=ns.follow(src.type());
113 
114  if(full_type.id()!=ID_struct)
115  return convert_norep(src, precedence);
116 
117  const struct_typet &struct_type=to_struct_type(full_type);
118 
119  std::string dest="{ ";
120 
121  const struct_typet::componentst &components=
122  struct_type.components();
123 
124  assert(components.size()==src.operands().size());
125 
126  exprt::operandst::const_iterator o_it=src.operands().begin();
127 
128  bool first=true;
129  size_t last_size=0;
130 
131  for(struct_typet::componentst::const_iterator
132  c_it=components.begin();
133  c_it!=components.end();
134  c_it++)
135  {
136  if(c_it->type().id()==ID_code)
137  {
138  }
139  else
140  {
141  std::string tmp=convert(*o_it);
142  std::string sep;
143 
144  if(first)
145  first=false;
146  else
147  {
148  if(last_size+40<dest.size())
149  {
150  sep=",\n ";
151  last_size=dest.size();
152  }
153  else
154  sep=", ";
155  }
156 
157  dest+=sep;
158  dest+='.';
159  dest+=c_it->get_string(ID_pretty_name);
160  dest+='=';
161  dest+=tmp;
162  }
163 
164  o_it++;
165  }
166 
167  dest+=" }";
168 
169  return dest;
170 }
171 
173  const constant_exprt &src,
174  unsigned &precedence)
175 {
176  if(src.type().id()==ID_c_bool)
177  {
178  if(!src.is_zero())
179  return "true";
180  else
181  return "false";
182  }
183  else if(src.type().id()==ID_bool)
184  {
185  if(src.is_true())
186  return "true";
187  else if(src.is_false())
188  return "false";
189  }
190  else if(src.type().id()==ID_pointer)
191  {
192  // Java writes 'null' for the null reference
193  if(src.is_zero())
194  return "null";
195  }
196  else if(src.type()==java_char_type())
197  {
198  std::string dest;
199  dest.reserve(char_representation_length);
200 
201  mp_integer int_value;
202  if(to_integer(src, int_value))
203  UNREACHABLE;
204 
205  dest += "(char)'" + utf16_little_endian_to_java(int_value.to_long()) + '\'';
206  return dest;
207  }
208  else if(src.type()==java_byte_type())
209  {
210  // No byte-literals in Java, so just cast:
211  mp_integer int_value;
212  if(to_integer(src, int_value))
213  UNREACHABLE;
214  std::string dest="(byte)";
215  dest+=integer2string(int_value);
216  return dest;
217  }
218  else if(src.type()==java_short_type())
219  {
220  // No short-literals in Java, so just cast:
221  mp_integer int_value;
222  if(to_integer(src, int_value))
223  UNREACHABLE;
224  std::string dest="(short)";
225  dest+=integer2string(int_value);
226  return dest;
227  }
228  else if(src.type()==java_long_type())
229  {
230  // long integer literals must have 'L' at the end
231  mp_integer int_value;
232  if(to_integer(src, int_value))
233  UNREACHABLE;
234  std::string dest=integer2string(int_value);
235  dest+='L';
236  return dest;
237  }
238  else if((src.type()==java_float_type()) ||
239  (src.type()==java_double_type()))
240  {
241  // This converts NaNs to the canonical NaN
242  const ieee_floatt ieee_repr(to_constant_expr(src));
243  if(ieee_repr.is_double())
244  return floating_point_to_java_string(ieee_repr.to_double());
245  return floating_point_to_java_string(ieee_repr.to_float());
246  }
247 
248 
249  return expr2ct::convert_constant(src, precedence);
250 }
251 
253  const typet &src,
254  const qualifierst &qualifiers,
255  const std::string &declarator)
256 {
257  std::unique_ptr<qualifierst> clone = qualifiers.clone();
258  qualifierst &new_qualifiers = *clone;
259  new_qualifiers.read(src);
260 
261  const std::string d=
262  declarator==""?declarator:(" "+declarator);
263 
264  const std::string q=
265  new_qualifiers.as_string();
266 
267  if(src==java_int_type())
268  return q+"int"+d;
269  else if(src==java_long_type())
270  return q+"long"+d;
271  else if(src==java_short_type())
272  return q+"short"+d;
273  else if(src==java_byte_type())
274  return q+"byte"+d;
275  else if(src==java_char_type())
276  return q+"char"+d;
277  else if(src==java_float_type())
278  return q+"float"+d;
279  else if(src==java_double_type())
280  return q+"double"+d;
281  else if(src==java_boolean_type())
282  return q+"boolean"+d;
283  else if(src==java_byte_type())
284  return q+"byte"+d;
285  else if(src.id()==ID_code)
286  {
287  const code_typet &code_type=to_code_type(src);
288 
289  // Java doesn't really have syntax for function types,
290  // so we make one up, loosely inspired by the syntax
291  // of lambda expressions.
292 
293  std::string dest="";
294 
295  dest+='(';
296  const code_typet::parameterst &parameters=code_type.parameters();
297 
298  for(code_typet::parameterst::const_iterator
299  it=parameters.begin();
300  it!=parameters.end();
301  it++)
302  {
303  if(it!=parameters.begin())
304  dest+=", ";
305 
306  dest+=convert(it->type());
307  }
308 
309  if(code_type.has_ellipsis())
310  {
311  if(!parameters.empty())
312  dest+=", ";
313  dest+="...";
314  }
315 
316  dest+=')';
317 
318  const typet &return_type=code_type.return_type();
319  dest+=" -> "+convert(return_type);
320 
321  return q + dest;
322  }
323  else
324  return expr2ct::convert_rec(src, qualifiers, declarator);
325 }
326 
328  const exprt &src,
329  unsigned precedence)
330 {
331  return "this";
332 }
333 
335  const exprt &src,
336  unsigned precedence)
337 {
338  if(src.operands().size()!=2)
339  {
340  unsigned precedence;
341  return convert_norep(src, precedence);
342  }
343 
344  return convert(src.op0())+" instanceof "+convert(src.op1().type());
345 }
346 
348  const exprt &src,
349  unsigned precedence)
350 {
351  std::string dest;
352 
353  if(src.get(ID_statement)==ID_java_new_array ||
354  src.get(ID_statement)==ID_java_new_array_data)
355  {
356  dest="new";
357 
358  std::string tmp_size=
359  convert(static_cast<const exprt &>(src.find(ID_size)));
360 
361  dest+=' ';
362  dest+=convert(src.type().subtype());
363  dest+='[';
364  dest+=tmp_size;
365  dest+=']';
366  }
367  else
368  dest="new "+convert(src.type().subtype());
369 
370  return dest;
371 }
372 
374  const exprt &src,
375  unsigned indent)
376 {
377  std::string dest=indent_str(indent)+"delete ";
378 
379  if(src.operands().size()!=1)
380  {
381  unsigned precedence;
382  return convert_norep(src, precedence);
383  }
384 
385  std::string tmp=convert(src.op0());
386 
387  dest+=tmp+";\n";
388 
389  return dest;
390 }
391 
393  const exprt &src,
394  unsigned &precedence)
395 {
396  if(src.id()=="java-this")
397  return convert_java_this(src, precedence=15);
398  if(src.id()==ID_java_instanceof)
399  return convert_java_instanceof(src, precedence=15);
400  else if(src.id()==ID_side_effect &&
401  (src.get(ID_statement)==ID_java_new ||
402  src.get(ID_statement)==ID_java_new_array ||
403  src.get(ID_statement)==ID_java_new_array_data))
404  return convert_java_new(src, precedence=15);
405  else if(src.id()==ID_side_effect &&
406  src.get(ID_statement)==ID_throw)
407  return convert_function(src, "throw", precedence=16);
408  else if(src.id()==ID_code &&
409  to_code(src).get_statement()==ID_exception_landingpad)
410  {
411  const exprt &catch_expr=
413  return "catch_landingpad("+
414  convert(catch_expr.type())+
415  ' '+
416  convert(catch_expr)+
417  ')';
418  }
419  else if(src.id()==ID_unassigned)
420  return "?";
421  else if(src.id()=="pod_constructor")
422  return "pod_constructor";
423  else if(src.id()==ID_virtual_function)
424  {
425  return "VIRTUAL_FUNCTION(" +
426  id2string(src.get(ID_C_class)) +
427  "." +
428  id2string(src.get(ID_component_name)) +
429  ")";
430  }
431  else if(src.id()==ID_java_string_literal)
432  return '"'+MetaString(src.get_string(ID_value))+'"';
433  else if(src.id()==ID_constant)
434  return convert_constant(to_constant_expr(src), precedence=16);
435  else
436  return expr2ct::convert_with_precedence(src, precedence);
437 }
438 
440  const codet &src,
441  unsigned indent)
442 {
443  const irep_idt &statement=src.get(ID_statement);
444 
445  if(statement==ID_java_new ||
446  statement==ID_java_new_array)
447  return convert_java_new(src, indent);
448 
449  if(statement==ID_function_call)
451 
452  return expr2ct::convert_code(src, indent);
453 }
454 
455 std::string expr2java(const exprt &expr, const namespacet &ns)
456 {
457  expr2javat expr2java(ns);
458  expr2java.get_shorthands(expr);
459  return expr2java.convert(expr);
460 }
461 
462 std::string type2java(const typet &type, const namespacet &ns)
463 {
464  expr2javat expr2java(ns);
465  return expr2java.convert(type);
466 }
Java-specific type qualifiers.
const irep_idt & get_statement() const
Definition: std_code.h:39
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:392
The type of an expression.
Definition: type.h:22
virtual std::string convert_struct(const exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:108
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:462
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:347
Base type of functions.
Definition: std_types.h:764
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
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:1262
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:373
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
typet java_int_type()
Definition: java_types.cpp:32
std::string convert_java_instanceof(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:334
#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:172
bool is_false() const
Definition: expr.cpp:131
std::vector< parametert > parameterst
Definition: std_types.h:767
const componentst & components() const
Definition: std_types.h:245
virtual std::string convert_code(const codet &src, unsigned indent) override
Definition: expr2java.cpp:439
ANSI-C Misc Utilities.
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3362
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
Definition: expr2java.cpp:252
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:4424
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:1786
const irep_idt & id() const
Definition: irep.h:189
argumentst & arguments()
Definition: std_code.h:860
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:828
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
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:4465
std::vector< exprt > operandst
Definition: expr.h:45
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1662
API to type classes.
virtual std::string convert(const typet &src) override
Definition: expr2java.cpp:28
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:1607
static void utf16_little_endian_to_java(const wchar_t ch, std::ostringstream &result, const std::locale &loc)
Definition: unicode.cpp:291
exprt & function()
Definition: std_code.h:848
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:3456
#define UNREACHABLE
Definition: invariant.h:250
bool is_double() const
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
bool is_zero() const
Definition: expr.cpp:161
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
const exprt & catch_expr() const
Definition: std_code.h:1589
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:327
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:2459
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:455
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:879