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_expr.h"
26 #include "java_qualifiers.h"
28 #include "java_types.h"
29 
30 std::string expr2javat::convert(const typet &src)
31 {
32  return convert_rec(src, java_qualifierst(ns), "");
33 }
34 
35 std::string expr2javat::convert(const exprt &src)
36 {
37  return expr2ct::convert(src);
38 }
39 
41  const code_function_callt &src,
42  unsigned indent)
43 {
44  if(src.operands().size()!=3)
45  {
46  unsigned precedence;
47  return convert_norep(src, precedence);
48  }
49 
50  std::string dest=indent_str(indent);
51 
52  if(src.lhs().is_not_nil())
53  {
54  unsigned p;
55  std::string lhs_str=convert_with_precedence(src.lhs(), p);
56 
57  dest+=lhs_str;
58  dest+='=';
59  }
60 
61  const java_method_typet &method_type =
63 
64  bool has_this = method_type.has_this() && !src.arguments().empty();
65 
66  if(has_this)
67  {
68  unsigned p;
69  std::string this_str=convert_with_precedence(src.arguments()[0], p);
70  dest+=this_str;
71  dest+=" . "; // extra spaces for readability
72  }
73 
74  {
75  unsigned p;
76  std::string function_str=convert_with_precedence(src.function(), p);
77  dest+=function_str;
78  }
79 
80  dest+='(';
81 
82  const exprt::operandst &arguments=src.arguments();
83 
84  bool first=true;
85 
86  forall_expr(it, arguments)
87  {
88  if(has_this && it==arguments.begin())
89  {
90  }
91  else
92  {
93  unsigned p;
94  std::string arg_str=convert_with_precedence(*it, p);
95 
96  if(first)
97  first=false;
98  else
99  dest+=", ";
100  dest+=arg_str;
101  }
102  }
103 
104  dest+=");";
105 
106  return dest;
107 }
108 
110  const exprt &src,
111  unsigned &precedence)
112 {
113  const typet &full_type=ns.follow(src.type());
114 
115  if(full_type.id()!=ID_struct)
116  return convert_norep(src, precedence);
117 
118  const struct_typet &struct_type=to_struct_type(full_type);
119 
120  std::string dest="{ ";
121 
122  const struct_typet::componentst &components=
123  struct_type.components();
124 
125  assert(components.size()==src.operands().size());
126 
127  exprt::operandst::const_iterator o_it=src.operands().begin();
128 
129  bool first=true;
130  size_t last_size=0;
131 
132  for(const auto &c : components)
133  {
134  if(c.type().id() != ID_code)
135  {
136  std::string tmp=convert(*o_it);
137  std::string sep;
138 
139  if(first)
140  first=false;
141  else
142  {
143  if(last_size+40<dest.size())
144  {
145  sep=",\n ";
146  last_size=dest.size();
147  }
148  else
149  sep=", ";
150  }
151 
152  dest+=sep;
153  dest+='.';
154  irep_idt field_name = c.get_pretty_name();
155  if(field_name.empty())
156  field_name = c.get_name();
157  dest += id2string(field_name);
158  dest+='=';
159  dest+=tmp;
160  }
161 
162  o_it++;
163  }
164 
165  dest+=" }";
166 
167  return dest;
168 }
169 
171  const constant_exprt &src,
172  unsigned &precedence)
173 {
174  if(src.type().id()==ID_c_bool)
175  {
176  if(!src.is_zero())
177  return "true";
178  else
179  return "false";
180  }
181  else if(src.type().id()==ID_bool)
182  {
183  if(src.is_true())
184  return "true";
185  else if(src.is_false())
186  return "false";
187  }
188  else if(src.type().id()==ID_pointer)
189  {
190  // Java writes 'null' for the null reference
191  if(src.is_zero())
192  return "null";
193  }
194  else if(src.type()==java_char_type())
195  {
196  std::string dest;
197  dest.reserve(char_representation_length);
198 
199  const char16_t int_value = numeric_cast_v<char16_t>(src);
200 
201  // Character literals in Java have type 'char', thus no cast is needed.
202  // This is different from C, where charater literals have type 'int'.
203  dest += '\'' + utf16_native_endian_to_java(int_value) + '\'';
204  return dest;
205  }
206  else if(src.type()==java_byte_type())
207  {
208  // No byte-literals in Java, so just cast:
209  const mp_integer int_value = numeric_cast_v<mp_integer>(src);
210  std::string dest="(byte)";
211  dest+=integer2string(int_value);
212  return dest;
213  }
214  else if(src.type()==java_short_type())
215  {
216  // No short-literals in Java, so just cast:
217  const mp_integer int_value = numeric_cast_v<mp_integer>(src);
218  std::string dest="(short)";
219  dest+=integer2string(int_value);
220  return dest;
221  }
222  else if(src.type()==java_long_type())
223  {
224  // long integer literals must have 'L' at the end
225  const mp_integer int_value = numeric_cast_v<mp_integer>(src);
226  std::string dest=integer2string(int_value);
227  dest+='L';
228  return dest;
229  }
230  else if((src.type()==java_float_type()) ||
231  (src.type()==java_double_type()))
232  {
233  // This converts NaNs to the canonical NaN
234  const ieee_floatt ieee_repr(to_constant_expr(src));
235  if(ieee_repr.is_double())
236  return floating_point_to_java_string(ieee_repr.to_double());
237  return floating_point_to_java_string(ieee_repr.to_float());
238  }
239 
240 
241  return expr2ct::convert_constant(src, precedence);
242 }
243 
245  const typet &src,
246  const qualifierst &qualifiers,
247  const std::string &declarator)
248 {
249  std::unique_ptr<qualifierst> clone = qualifiers.clone();
250  qualifierst &new_qualifiers = *clone;
251  new_qualifiers.read(src);
252 
253  const std::string d = declarator.empty() ? declarator : (" " + declarator);
254 
255  const std::string q=
256  new_qualifiers.as_string();
257 
258  if(src==java_int_type())
259  return q+"int"+d;
260  else if(src==java_long_type())
261  return q+"long"+d;
262  else if(src==java_short_type())
263  return q+"short"+d;
264  else if(src==java_byte_type())
265  return q+"byte"+d;
266  else if(src==java_char_type())
267  return q+"char"+d;
268  else if(src==java_float_type())
269  return q+"float"+d;
270  else if(src==java_double_type())
271  return q+"double"+d;
272  else if(src==java_boolean_type())
273  return q+"boolean"+d;
274  else if(src==java_byte_type())
275  return q+"byte"+d;
276  else if(src.id()==ID_code)
277  {
278  const java_method_typet &method_type = to_java_method_type(src);
279 
280  // Java doesn't really have syntax for function types,
281  // so we make one up, loosely inspired by the syntax
282  // of lambda expressions.
283 
284  std::string dest;
285 
286  dest+='(';
287  const java_method_typet::parameterst &parameters = method_type.parameters();
288 
289  for(java_method_typet::parameterst::const_iterator it = parameters.begin();
290  it != parameters.end();
291  it++)
292  {
293  if(it!=parameters.begin())
294  dest+=", ";
295 
296  dest+=convert(it->type());
297  }
298 
299  if(method_type.has_ellipsis())
300  {
301  if(!parameters.empty())
302  dest+=", ";
303  dest+="...";
304  }
305 
306  dest+=')';
307 
308  const typet &return_type = method_type.return_type();
309  dest+=" -> "+convert(return_type);
310 
311  return q + dest;
312  }
313  else
314  return expr2ct::convert_rec(src, qualifiers, declarator);
315 }
316 
318 {
319  return id2string(ID_this);
320 }
321 
323 {
324  const auto &instanceof_expr = to_java_instanceof_expr(src);
325 
326  return convert(instanceof_expr.tested_expr()) + " instanceof " +
327  convert(instanceof_expr.target_type());
328 }
329 
330 std::string expr2javat::convert_code_java_new(const exprt &src, unsigned indent)
331 {
332  return indent_str(indent) + convert_java_new(src) + ";\n";
333 }
334 
335 std::string expr2javat::convert_java_new(const exprt &src)
336 {
337  std::string dest;
338 
339  if(src.get(ID_statement)==ID_java_new_array ||
340  src.get(ID_statement)==ID_java_new_array_data)
341  {
342  dest="new";
343 
344  std::string tmp_size=
345  convert(static_cast<const exprt &>(src.find(ID_size)));
346 
347  dest+=' ';
348  dest+=convert(src.type().subtype());
349  dest+='[';
350  dest+=tmp_size;
351  dest+=']';
352  }
353  else
354  dest="new "+convert(src.type().subtype());
355 
356  return dest;
357 }
358 
360  const exprt &src,
361  unsigned indent)
362 {
363  std::string dest=indent_str(indent)+"delete ";
364 
365  if(src.operands().size()!=1)
366  {
367  unsigned precedence;
368  return convert_norep(src, precedence);
369  }
370 
371  std::string tmp = convert(to_unary_expr(src).op());
372 
373  dest+=tmp+";\n";
374 
375  return dest;
376 }
377 
379  const exprt &src,
380  unsigned &precedence)
381 {
382  if(src.id()=="java-this")
383  {
384  precedence = 15;
385  return convert_java_this();
386  }
387  if(src.id()==ID_java_instanceof)
388  {
389  precedence = 15;
390  return convert_java_instanceof(src);
391  }
392  else if(src.id()==ID_side_effect &&
393  (src.get(ID_statement)==ID_java_new ||
394  src.get(ID_statement)==ID_java_new_array ||
395  src.get(ID_statement)==ID_java_new_array_data))
396  {
397  precedence = 15;
398  return convert_java_new(src);
399  }
400  else if(src.id()==ID_side_effect &&
401  src.get(ID_statement)==ID_throw)
402  {
403  precedence = 16;
404  return convert_function(src, "throw");
405  }
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  const class_method_descriptor_exprt &virtual_function =
425  return "CLASS_METHOD_DESCRIPTOR(" + id2string(virtual_function.class_id()) +
426  "." + id2string(virtual_function.mangled_method_name()) + ")";
427  }
428  else if(
429  const auto &literal = expr_try_dynamic_cast<java_string_literal_exprt>(src))
430  {
431  return '"' + MetaString(id2string(literal->value())) + '"';
432  }
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_code_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 }
MetaString
std::string MetaString(const std::string &in)
Definition: c_misc.cpp:95
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
ieee_floatt::is_double
bool is_double() const
Definition: ieee_float.cpp:1174
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:813
ieee_floatt
Definition: ieee_float.h:120
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
typet::subtype
const typet & subtype() const
Definition: type.h:47
expr2javat::convert_java_new
std::string convert_java_new(const exprt &src)
Definition: expr2java.cpp:335
class_method_descriptor_exprt::mangled_method_name
const irep_idt & mangled_method_name() const
The method name after mangling it by combining it with the descriptor.
Definition: std_expr.h:4545
arith_tools.h
expr2javat::convert_java_this
std::string convert_java_this()
Definition: expr2java.cpp:317
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
typet
The type of an expression, extends irept.
Definition: type.h:29
java_long_type
signedbv_typet java_long_type()
Definition: java_types.cpp:44
expr2javat::convert
virtual std::string convert(const typet &src) override
Definition: expr2java.cpp:30
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
expr2ct::convert_constant
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1682
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
ieee_floatt::to_float
float to_float() const
Note that calling from_float -> to_float can return different bit patterns for NaN.
Definition: ieee_float.cpp:1217
java_string_literal_expr.h
Representation of a constant Java string.
java_method_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:738
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
java_expr.h
Java-specific exprt subclasses.
expr2ct::convert_code
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3252
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
qualifierst::read
virtual void read(const typet &src)=0
qualifierst
Definition: c_qualifiers.h:19
namespace.h
expr2javat::convert_java_instanceof
std::string convert_java_instanceof(const exprt &src)
Definition: expr2java.cpp:322
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1208
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
to_code
const codet & to_code(const exprt &expr)
Definition: std_code.h:155
class_method_descriptor_exprt
An expression describing a method on a class.
Definition: std_expr.h:4508
expr2javat::convert_with_precedence
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:378
ieee_floatt::to_double
double to_double() const
Note that calling from_double -> to_double can return different bit patterns for NaN.
Definition: ieee_float.cpp:1186
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1183
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
expr2ct::convert
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:182
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
expr2ct::indent_str
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2365
expr2ct::convert_function
std::string convert_function(const exprt &src, const std::string &symbol)
Definition: expr2c.cpp:1177
qualifierst::clone
virtual std::unique_ptr< qualifierst > clone() const =0
expr2javat::convert_code_function_call
std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2java.cpp:40
std_types.h
Pre-defined types.
c_misc.h
ANSI-C Misc Utilities.
expr2javat::convert_rec
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator) override
Definition: expr2java.cpp:244
expr2c_class.h
symbol.h
Symbol table entry.
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1294
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
dstringt::empty
bool empty() const
Definition: dstring.h:88
expr2javat::convert_code_java_delete
std::string convert_code_java_delete(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:359
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:32
floating_point_to_java_string
std::string floating_point_to_java_string(float_type value)
Convert floating point number to a string without printing unnecessary zeros.
Definition: expr2java.h:62
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:857
expr2javat
Definition: expr2java.h:22
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1228
java_short_type
signedbv_typet java_short_type()
Definition: java_types.cpp:50
code_landingpadt::catch_expr
const exprt & catch_expr() const
Definition: std_code.h:2391
expr2javat::convert_constant
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:170
code_typet::has_this
bool has_this() const
Definition: std_types.h:818
expr2javat::convert_struct
virtual std::string convert_struct(const exprt &src, unsigned &precedence) override
Definition: expr2java.cpp:109
java_byte_type
signedbv_typet java_byte_type()
Definition: java_types.cpp:56
java_qualifierst
Definition: java_qualifiers.h:13
expr2ct::convert_norep
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1569
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:132
expr2ct::ns
const namespacet & ns
Definition: expr2c_class.h:48
to_code_landingpad
static code_landingpadt & to_code_landingpad(codet &code)
Definition: std_code.h:2415
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
java_double_type
floatbv_typet java_double_type()
Definition: java_types.cpp:74
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:51
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
to_class_method_descriptor_expr
const class_method_descriptor_exprt & to_class_method_descriptor_expr(const exprt &expr)
Cast an exprt to a class_method_descriptor_exprt.
Definition: std_expr.h:4598
to_java_instanceof_expr
const java_instanceof_exprt & to_java_instanceof_expr(const exprt &expr)
Cast an exprt to a java_instanceof_exprt.
Definition: java_expr.h:86
expr2javat::convert_code
virtual std::string convert_code(const codet &src, unsigned indent) override
Definition: expr2java.cpp:439
ieee_float.h
java_char_type
unsignedbv_typet java_char_type()
Definition: java_types.cpp:62
type2java
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:462
unicode.h
expr2java
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:455
class_method_descriptor_exprt::class_id
const irep_idt & class_id() const
Unique identifier in the symbol table, of the compile time type of the class which this expression is...
Definition: std_expr.h:4553
java_boolean_type
c_bool_typet java_boolean_type()
Definition: java_types.cpp:80
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:847
exprt::operands
operandst & operands()
Definition: expr.h:95
expr2java.h
forall_expr
#define forall_expr(it, expr)
Definition: expr.h:29
java_types.h
expr2ct::convert_rec
virtual std::string convert_rec(const typet &src, const qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:187
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:186
utf16_native_endian_to_java
static void utf16_native_endian_to_java(const wchar_t ch, std::ostringstream &result, const std::locale &loc)
Escapes non-printable characters, whitespace except for spaces, double- and single-quotes and backsla...
Definition: unicode.cpp:318
qualifierst::as_string
virtual std::string as_string() const =0
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
expr2ct::convert_with_precedence
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3338
expr2javat::char_representation_length
const std::size_t char_representation_length
Definition: expr2java.h:52
std_expr.h
API to expression classes.
java_method_typet
Definition: java_types.h:103
java_qualifiers.h
Java-specific type qualifiers.
code_function_callt::function
exprt & function()
Definition: std_code.h:1218
java_float_type
floatbv_typet java_float_type()
Definition: java_types.cpp:68
expr2javat::convert_code_java_new
std::string convert_code_java_new(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:330
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:35
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106