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 
13 #include <util/namespace.h>
14 #include <util/std_types.h>
15 #include <util/std_expr.h>
16 #include <util/symbol.h>
17 #include <util/arith_tools.h>
18 
19 #include <ansi-c/c_qualifiers.h>
20 #include <ansi-c/c_misc.h>
21 #include <ansi-c/expr2c_class.h>
22 
23 #include "java_types.h"
24 
26  const code_function_callt &src,
27  unsigned indent)
28 {
29  if(src.operands().size()!=3)
30  {
31  unsigned precedence;
32  return convert_norep(src, precedence);
33  }
34 
35  std::string dest=indent_str(indent);
36 
37  if(src.lhs().is_not_nil())
38  {
39  unsigned p;
40  std::string lhs_str=convert_with_precedence(src.lhs(), p);
41 
42  dest+=lhs_str;
43  dest+='=';
44  }
45 
46  const code_typet &code_type=
47  to_code_type(src.function().type());
48 
49  bool has_this=code_type.has_this() &&
50  !src.arguments().empty();
51 
52  if(has_this)
53  {
54  unsigned p;
55  std::string this_str=convert_with_precedence(src.arguments()[0], p);
56  dest+=this_str;
57  dest+=" . "; // extra spaces for readability
58  }
59 
60  {
61  unsigned p;
62  std::string function_str=convert_with_precedence(src.function(), p);
63  dest+=function_str;
64  }
65 
66  dest+='(';
67 
68  const exprt::operandst &arguments=src.arguments();
69 
70  bool first=true;
71 
72  forall_expr(it, arguments)
73  {
74  if(has_this && it==arguments.begin())
75  {
76  }
77  else
78  {
79  unsigned p;
80  std::string arg_str=convert_with_precedence(*it, p);
81 
82  if(first)
83  first=false;
84  else
85  dest+=", ";
86  dest+=arg_str;
87  }
88  }
89 
90  dest+=");";
91 
92  return dest;
93 }
94 
96  const exprt &src,
97  unsigned &precedence)
98 {
99  const typet &full_type=ns.follow(src.type());
100 
101  if(full_type.id()!=ID_struct)
102  return convert_norep(src, precedence);
103 
104  const struct_typet &struct_type=to_struct_type(full_type);
105 
106  std::string dest="{ ";
107 
108  const struct_typet::componentst &components=
109  struct_type.components();
110 
111  assert(components.size()==src.operands().size());
112 
113  exprt::operandst::const_iterator o_it=src.operands().begin();
114 
115  bool first=true;
116  size_t last_size=0;
117 
118  for(struct_typet::componentst::const_iterator
119  c_it=components.begin();
120  c_it!=components.end();
121  c_it++)
122  {
123  if(c_it->type().id()==ID_code)
124  {
125  }
126  else
127  {
128  std::string tmp=convert(*o_it);
129  std::string sep;
130 
131  if(first)
132  first=false;
133  else
134  {
135  if(last_size+40<dest.size())
136  {
137  sep=",\n ";
138  last_size=dest.size();
139  }
140  else
141  sep=", ";
142  }
143 
144  dest+=sep;
145  dest+='.';
146  dest+=c_it->get_string(ID_pretty_name);
147  dest+='=';
148  dest+=tmp;
149  }
150 
151  o_it++;
152  }
153 
154  dest+=" }";
155 
156  return dest;
157 }
158 
160  const constant_exprt &src,
161  unsigned &precedence)
162 {
163  if(src.type().id()==ID_c_bool)
164  {
165  if(!src.is_zero())
166  return "true";
167  else
168  return "false";
169  }
170  else if(src.type().id()==ID_bool)
171  {
172  if(src.is_true())
173  return "true";
174  else if(src.is_false())
175  return "false";
176  }
177  else if(src.type().id()==ID_pointer)
178  {
179  // Java writes 'null' for the null reference
180  if(src.is_zero())
181  return "null";
182  }
183  else if(src.type()==java_char_type())
184  {
185  std::string dest;
186  dest.reserve(char_representation_length);
187 
188  mp_integer int_value;
189  if(to_integer(src, int_value))
190  assert(false);
191 
192  dest+="(char)'";
193 
194  if(int_value>=' ' && int_value<127)
195  dest+=static_cast<char>(int_value.to_long());
196  else
197  {
198  std::string hex=integer2string(int_value, 16);
199  while(hex.size()<4) hex='0'+hex;
200  dest+='\\';
201  dest+='u';
202  dest+=hex;
203  }
204 
205  dest+='\'';
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  assert(false);
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  assert(false);
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  assert(false);
234  std::string dest=integer2string(int_value);
235  dest+='L';
236  return dest;
237  }
238 
239  return expr2ct::convert_constant(src, precedence);
240 }
241 
243  const typet &src,
244  const c_qualifierst &qualifiers,
245  const std::string &declarator)
246 {
247  c_qualifierst new_qualifiers(qualifiers);
248  new_qualifiers.read(src);
249 
250  const std::string d=
251  declarator==""?declarator:(" "+declarator);
252 
253  const std::string q=
254  new_qualifiers.as_string();
255 
256  if(src==java_int_type())
257  return q+"int"+d;
258  else if(src==java_long_type())
259  return q+"long"+d;
260  else if(src==java_short_type())
261  return q+"short"+d;
262  else if(src==java_byte_type())
263  return q+"byte"+d;
264  else if(src==java_char_type())
265  return q+"char"+d;
266  else if(src==java_float_type())
267  return q+"float"+d;
268  else if(src==java_double_type())
269  return q+"double"+d;
270  else if(src==java_boolean_type())
271  return q+"boolean"+d;
272  else if(src==java_byte_type())
273  return q+"byte"+d;
274  else if(src.id()==ID_code)
275  {
276  const code_typet &code_type=to_code_type(src);
277 
278  // Java doesn't really have syntax for function types,
279  // so we make one up, loosely inspired by the syntax
280  // of lambda expressions.
281 
282  std::string dest="";
283 
284  dest+='(';
285  const code_typet::parameterst &parameters=code_type.parameters();
286 
287  for(code_typet::parameterst::const_iterator
288  it=parameters.begin();
289  it!=parameters.end();
290  it++)
291  {
292  if(it!=parameters.begin())
293  dest+=", ";
294 
295  dest+=convert(it->type());
296  }
297 
298  if(code_type.has_ellipsis())
299  {
300  if(!parameters.empty())
301  dest+=", ";
302  dest+="...";
303  }
304 
305  dest+=')';
306 
307  const typet &return_type=code_type.return_type();
308  dest+=" -> "+convert(return_type);
309 
310  return dest;
311  }
312  else
313  return expr2ct::convert_rec(src, qualifiers, declarator);
314 }
315 
317  const exprt &src,
318  unsigned precedence)
319 {
320  return "this";
321 }
322 
324  const exprt &src,
325  unsigned precedence)
326 {
327  if(src.operands().size()!=2)
328  {
329  unsigned precedence;
330  return convert_norep(src, precedence);
331  }
332 
333  return convert(src.op0())+" instanceof "+convert(src.op1().type());
334 }
335 
337  const exprt &src,
338  unsigned precedence)
339 {
340  std::string dest;
341 
342  if(src.get(ID_statement)==ID_java_new_array)
343  {
344  dest="new";
345 
346  std::string tmp_size=
347  convert(static_cast<const exprt &>(src.find(ID_size)));
348 
349  dest+=' ';
350  dest+=convert(src.type().subtype());
351  dest+='[';
352  dest+=tmp_size;
353  dest+=']';
354  }
355  else
356  dest="new "+convert(src.type().subtype());
357 
358  return dest;
359 }
360 
362  const exprt &src,
363  unsigned indent)
364 {
365  std::string dest=indent_str(indent)+"delete ";
366 
367  if(src.operands().size()!=1)
368  {
369  unsigned precedence;
370  return convert_norep(src, precedence);
371  }
372 
373  std::string tmp=convert(src.op0());
374 
375  dest+=tmp+";\n";
376 
377  return dest;
378 }
379 
381  const exprt &src,
382  unsigned &precedence)
383 {
384  if(src.id()=="java-this")
385  return convert_java_this(src, precedence=15);
386  if(src.id()==ID_java_instanceof)
387  return convert_java_instanceof(src, precedence=15);
388  else if(src.id()==ID_side_effect &&
389  (src.get(ID_statement)==ID_java_new ||
390  src.get(ID_statement)==ID_java_new_array))
391  return convert_java_new(src, precedence=15);
392  else if(src.id()==ID_side_effect &&
393  src.get(ID_statement)==ID_throw)
394  return convert_function(src, "throw", precedence=16);
395  else if(src.id()==ID_unassigned)
396  return "?";
397  else if(src.id()=="pod_constructor")
398  return "pod_constructor";
399  else if(src.id()==ID_virtual_function)
400  {
401  return "VIRTUAL_FUNCTION(" +
402  id2string(src.get(ID_C_class)) +
403  "." +
404  id2string(src.get(ID_component_name)) +
405  ")";
406  }
407  else if(src.id()==ID_java_string_literal)
408  return '"'+MetaString(src.get_string(ID_value))+'"';
409  else if(src.id()==ID_constant)
410  return convert_constant(to_constant_expr(src), precedence=16);
411  else
412  return expr2ct::convert_with_precedence(src, precedence);
413 }
414 
416  const codet &src,
417  unsigned indent)
418 {
419  const irep_idt &statement=src.get(ID_statement);
420 
421  if(statement==ID_java_new ||
422  statement==ID_java_new_array)
423  return convert_java_new(src, indent);
424 
425  if(statement==ID_function_call)
427 
428  return expr2ct::convert_code(src, indent);
429 }
430 
431 std::string expr2java(const exprt &expr, const namespacet &ns)
432 {
433  expr2javat expr2java(ns);
434  expr2java.get_shorthands(expr);
435  return expr2java.convert(expr);
436 }
437 
438 std::string type2java(const typet &type, const namespacet &ns)
439 {
440  expr2javat expr2java(ns);
441  return expr2java.convert(type);
442 }
The type of an expression.
Definition: type.h:20
std::string type2java(const typet &type, const namespacet &ns)
Definition: expr2java.cpp:438
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
BigInt mp_integer
Definition: mp_arith.h:19
virtual std::string convert_java_new(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:336
Base type of functions.
Definition: std_types.h:734
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
Symbol table entry.
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:104
std::string convert_function(const exprt &src, const std::string &symbol, unsigned precedence)
Definition: expr2c.cpp:1180
typet java_boolean_type()
Definition: java_types.cpp:59
exprt & op0()
Definition: expr.h:84
typet java_double_type()
Definition: java_types.cpp:54
bool has_ellipsis() const
Definition: std_types.h:803
virtual std::string convert_code_java_delete(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:361
typet java_int_type()
Definition: java_types.cpp:19
virtual std::string convert_java_instanceof(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:323
#define forall_expr(it, expr)
Definition: expr.h:28
std::vector< componentt > componentst
Definition: std_types.h:240
bool is_false() const
Definition: expr.cpp:140
std::vector< parametert > parameterst
Definition: std_types.h:829
const componentst & components() const
Definition: std_types.h:242
ANSI-C Misc Utilities.
std::string convert_code(const codet &src)
Definition: expr2c.cpp:3269
bool is_true() const
Definition: expr.cpp:133
typet java_long_type()
Definition: java_types.cpp:29
typet & type()
Definition: expr.h:60
A constant literal expression.
Definition: std_expr.h:3685
Structure type.
Definition: std_types.h:296
virtual std::string convert(const typet &src)
Definition: expr2c.cpp:158
virtual std::string convert_struct(const exprt &src, unsigned &precedence)
Definition: expr2java.cpp:95
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2java.cpp:159
virtual std::string convert_constant(const constant_exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1704
void read(const typet &src)
const irep_idt & id() const
Definition: irep.h:189
argumentst & arguments()
Definition: std_code.h:689
API to expression classes.
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
const namespacet & ns
Definition: expr2c_class.h:35
const std::size_t char_representation_length
Definition: expr2java.h:47
typet java_byte_type()
Definition: java_types.cpp:39
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2java.cpp:380
typet java_short_type()
Definition: java_types.cpp:34
std::vector< exprt > operandst
Definition: expr.h:49
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
virtual std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator)
Definition: expr2c.cpp:163
std::string convert_norep(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:1580
std::string as_string() const
API to type classes.
exprt & function()
Definition: std_code.h:677
Base class for all expressions.
Definition: expr.h:46
const parameterst & parameters() const
Definition: std_types.h:841
bool has_this() const
Definition: std_types.h:808
virtual std::string convert_with_precedence(const exprt &src, unsigned &precedence)
Definition: expr2c.cpp:3363
const std::string & get_string(const irep_namet &name) const
Definition: irep.h:202
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
bool is_zero() const
Definition: expr.cpp:236
std::string MetaString(const std::string &in)
Definition: c_misc.cpp:104
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
virtual std::string convert_code_function_call(const code_function_callt &src, unsigned indent)
Definition: expr2java.cpp:25
virtual std::string convert_code(const codet &src, unsigned indent)
Definition: expr2java.cpp:415
A statement in a programming language.
Definition: std_code.h:19
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
typet java_char_type()
Definition: java_types.cpp:44
const typet & subtype() const
Definition: type.h:31
virtual std::string convert_rec(const typet &src, const c_qualifierst &qualifiers, const std::string &declarator)
Definition: expr2java.cpp:242
operandst & operands()
Definition: expr.h:70
virtual std::string convert_java_this(const exprt &src, unsigned precedence)
Definition: expr2java.cpp:316
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
static std::string indent_str(unsigned indent)
Definition: expr2c.cpp:2377
std::string expr2java(const exprt &expr, const namespacet &ns)
Definition: expr2java.cpp:431
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700