cprover
java_entry_point.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_entry_point.h"
10 
11 #include <algorithm>
12 #include <set>
13 #include <iostream>
14 
15 #include <util/arith_tools.h>
16 #include <util/prefix.h>
17 #include <util/std_types.h>
18 #include <util/std_code.h>
19 #include <util/std_expr.h>
20 #include <util/cprover_prefix.h>
21 #include <util/message.h>
22 #include <util/config.h>
23 #include <util/namespace.h>
25 #include <util/suffix.h>
26 
27 #include <util/c_types.h>
28 #include <ansi-c/string_constant.h>
29 
31 
32 #include "java_object_factory.h"
33 #include "java_types.h"
34 
35 #define INITIALIZE CPROVER_PREFIX "initialize"
36 
37 static void create_initialize(symbol_tablet &symbol_table)
38 {
39  symbolt initialize;
40  initialize.name=INITIALIZE;
41  initialize.base_name=INITIALIZE;
42  initialize.mode=ID_java;
43 
44  code_typet type;
45  type.return_type()=empty_typet();
46  initialize.type=type;
47 
48  code_blockt init_code;
49 
50  namespacet ns(symbol_table);
51 
52  symbol_exprt rounding_mode=
53  ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
54 
55  init_code.add(
56  code_assignt(rounding_mode, from_integer(0, rounding_mode.type())));
57 
58  initialize.value=init_code;
59 
60  if(symbol_table.add(initialize))
61  throw "failed to add "+std::string(INITIALIZE);
62 }
63 
64 
65 static bool should_init_symbol(const symbolt &sym)
66 {
67  if(sym.type.id()!=ID_code &&
68  sym.is_lvalue &&
69  sym.is_state_var &&
70  sym.is_static_lifetime &&
71  sym.mode==ID_java)
72  return true;
73 
74  return has_prefix(id2string(sym.name), "java::java.lang.String.Literal");
75 }
76 
78  symbol_tablet &symbol_table,
79  const source_locationt &source_location,
80  bool assume_init_pointers_not_null,
81  unsigned max_nondet_array_length)
82 {
83  symbolt &initialize_symbol=symbol_table.lookup(INITIALIZE);
84  code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
85 
86  // We need to zero out all static variables, or nondet-initialize if they're
87  // external. Iterate over a copy of the symtab, as its iterators are
88  // invalidated by object_factory:
89 
90  std::list<irep_idt> symbol_names;
91  for(const auto &entry : symbol_table.symbols)
92  symbol_names.push_back(entry.first);
93 
94  for(const auto &symname : symbol_names)
95  {
96  const symbolt &sym=symbol_table.lookup(symname);
97  if(should_init_symbol(sym))
98  {
99  if(sym.value.is_nil() && sym.type!=empty_typet())
100  {
101  bool allow_null=!assume_init_pointers_not_null;
102  if(allow_null)
103  {
104  std::string namestr=id2string(sym.symbol_expr().get_identifier());
105  const std::string suffix="@class_model";
106  // Static '.class' fields are always non-null.
107  if(has_suffix(namestr, suffix))
108  allow_null=false;
109  if(allow_null && has_prefix(
110  namestr,
111  "java::java.lang.String.Literal"))
112  allow_null=false;
113  }
114  auto newsym=object_factory(
115  sym.type,
116  symname,
117  code_block,
118  allow_null,
119  symbol_table,
120  max_nondet_array_length,
121  source_location);
122  code_assignt assignment(sym.symbol_expr(), newsym);
123  code_block.add(assignment);
124  }
125  else if(sym.value.is_not_nil())
126  {
127  code_assignt assignment(sym.symbol_expr(), sym.value);
128  assignment.add_source_location()=source_location;
129  code_block.add(assignment);
130  }
131  }
132  }
133 
134  // we now need to run all the <clinit> methods
135 
136  for(symbol_tablet::symbolst::const_iterator
137  it=symbol_table.symbols.begin();
138  it!=symbol_table.symbols.end();
139  it++)
140  {
141  if(it->second.base_name=="<clinit>" &&
142  it->second.type.id()==ID_code &&
143  it->second.mode==ID_java)
144  {
145  code_function_callt function_call;
146  function_call.lhs()=nil_exprt();
147  function_call.function()=it->second.symbol_expr();
148  function_call.add_source_location()=source_location;
149  code_block.add(function_call);
150  }
151  }
152 }
153 
155  const symbolt &function,
156  code_blockt &init_code,
157  symbol_tablet &symbol_table,
158  bool assume_init_pointers_not_null,
159  unsigned max_nondet_array_length)
160 {
161  const code_typet::parameterst &parameters=
162  to_code_type(function.type).parameters();
163 
164  exprt::operandst main_arguments;
165  main_arguments.resize(parameters.size());
166 
167  for(std::size_t param_number=0;
168  param_number<parameters.size();
169  param_number++)
170  {
171  bool is_this=(param_number==0) &&
172  parameters[param_number].get_this();
173  bool is_default_entry_point(config.main.empty());
174  bool is_main=is_default_entry_point;
175  if(!is_main)
176  {
177  bool named_main=has_suffix(config.main, ".main");
178  const typet &string_array_type=
179  java_type_from_string("[Ljava.lang.String;");
180  bool has_correct_type=
181  to_code_type(function.type).return_type().id()==ID_empty &&
182  (!to_code_type(function.type).has_this()) &&
183  parameters.size()==1 &&
184  parameters[0].type().full_eq(string_array_type);
185  is_main=(named_main && has_correct_type);
186  }
187 
188  const code_typet::parametert &p=parameters[param_number];
189  const irep_idt base_name=p.get_base_name().empty()?
190  ("argument#"+std::to_string(param_number)):p.get_base_name();
191 
192  bool allow_null=(!is_main) && (!is_this) && !assume_init_pointers_not_null;
193 
194  main_arguments[param_number]=
196  p.type(),
197  base_name,
198  init_code,
199  allow_null,
200  symbol_table,
201  max_nondet_array_length,
202  function.location);
203 
204  // record as an input
205  codet input(ID_input);
206  input.operands().resize(2);
207  input.op0()=
209  index_exprt(
210  string_constantt(base_name),
211  from_integer(0, index_type())));
212  input.op1()=main_arguments[param_number];
213  input.add_source_location()=function.location;
214 
215  init_code.move_to_operands(input);
216  }
217 
218  return main_arguments;
219 }
220 
222  const symbolt &function,
223  const exprt::operandst &main_arguments,
224  code_blockt &init_code,
225  symbol_tablet &symbol_table)
226 {
227  const code_typet::parameterst &parameters=
228  to_code_type(function.type).parameters();
229 
230  exprt::operandst result;
231  result.reserve(parameters.size()+1);
232 
233  bool has_return_value=
234  to_code_type(function.type).return_type()!=empty_typet();
235 
236  if(has_return_value)
237  {
238  // record return value
239  codet output(ID_output);
240  output.operands().resize(2);
241 
242  const symbolt &return_symbol=symbol_table.lookup("return'");
243 
244  output.op0()=
246  index_exprt(
247  string_constantt(return_symbol.base_name),
248  from_integer(0, index_type())));
249  output.op1()=return_symbol.symbol_expr();
250  output.add_source_location()=function.location;
251 
252  init_code.move_to_operands(output);
253  }
254 
255  for(std::size_t param_number=0;
256  param_number<parameters.size();
257  param_number++)
258  {
259  const symbolt &p_symbol=
260  symbol_table.lookup(parameters[param_number].get_identifier());
261 
262  if(p_symbol.type.id()==ID_pointer)
263  {
264  // record as an output
265  codet output(ID_output);
266  output.operands().resize(2);
267  output.op0()=
269  index_exprt(
270  string_constantt(p_symbol.base_name),
271  from_integer(0, index_type())));
272  output.op1()=main_arguments[param_number];
273  output.add_source_location()=function.location;
274 
275  init_code.move_to_operands(output);
276  }
277  }
278 
279  // record exceptional return variable as output
280  codet output(ID_output);
281  output.operands().resize(2);
282 
283  assert(symbol_table.has_symbol(id2string(function.name)+EXC_SUFFIX));
284 
285  // retrieve the exception variable
286  const symbolt exc_symbol=symbol_table.lookup(
287  id2string(function.name)+EXC_SUFFIX);
288 
289  output.op0()=address_of_exprt(
290  index_exprt(string_constantt(exc_symbol.base_name),
291  from_integer(0, index_type())));
292  output.op1()=exc_symbol.symbol_expr();
293  output.add_source_location()=function.location;
294 
295  init_code.move_to_operands(output);
296 }
297 
299  symbol_tablet &symbol_table,
300  const irep_idt &main_class,
301  message_handlert &message_handler,
302  bool allow_no_body)
303 {
304  symbolt symbol;
306 
307  messaget message(message_handler);
308 
309  // find main symbol
310  if(config.main!="")
311  {
312  // Add java:: prefix
313  std::string main_identifier="java::"+config.main;
314 
315  symbol_tablet::symbolst::const_iterator s_it;
316 
317  // Does it have a type signature? (':' suffix)
318  if(config.main.rfind(':')==std::string::npos)
319  {
320  std::string prefix=main_identifier+':';
321  std::set<irep_idt> matches;
322 
323  for(const auto &s : symbol_table.symbols)
324  if(has_prefix(id2string(s.first), prefix) &&
325  s.second.type.id()==ID_code)
326  matches.insert(s.first);
327 
328  if(matches.empty())
329  {
330  message.error() << "main symbol `" << config.main
331  << "' not found" << messaget::eom;
332  res.main_function=symbol;
333  res.error_found=true;
334  res.stop_convert=true;
335  return res;
336  }
337  else if(matches.size()==1)
338  {
339  s_it=symbol_table.symbols.find(*matches.begin());
340  assert(s_it!=symbol_table.symbols.end());
341  }
342  else
343  {
344  message.error() << "main symbol `" << config.main
345  << "' is ambiguous:\n";
346 
347  for(const auto &s : matches)
348  message.error() << " " << s << '\n';
349 
350  message.error() << messaget::eom;
351  res.main_function=symbol;
352  res.error_found=true;
353  res.stop_convert=true;
354  return res;
355  }
356  }
357  else
358  {
359  // just look it up
360  s_it=symbol_table.symbols.find(main_identifier);
361 
362  if(s_it==symbol_table.symbols.end())
363  {
364  message.error() << "main symbol `" << config.main
365  << "' not found" << messaget::eom;
366  res.main_function=symbol;
367  res.error_found=true;
368  res.stop_convert=true;
369  return res;
370  }
371  }
372  // function symbol
373  symbol=s_it->second;
374 
375  if(symbol.type.id()!=ID_code)
376  {
377  message.error() << "main symbol `" << config.main
378  << "' not a function" << messaget::eom;
379  res.main_function=symbol;
380  res.error_found=true;
381  res.stop_convert=true;
382  return res;
383  }
384 
385  // check if it has a body
386  if(symbol.value.is_nil() && !allow_no_body)
387  {
388  message.error() << "main method `" << main_class
389  << "' has no body" << messaget::eom;
390  res.main_function=symbol;
391  res.error_found=true;
392  res.stop_convert=true;
393  return res;
394  }
395  }
396  else
397  {
398  // no function given, we look for the main class
399  assert(config.main=="");
400 
401  // are we given a main class?
402  if(main_class.empty())
403  {
404  res.main_function=symbol;
405  res.error_found=false;
406  res.stop_convert=true;
407  return res; // silently ignore
408  }
409 
410  std::string entry_method=
411  id2string(main_class)+".main";
412 
413  std::string prefix="java::"+entry_method+":";
414 
415  // look it up
416  std::set<irep_idt> matches;
417 
418  for(symbol_tablet::symbolst::const_iterator
419  s_it=symbol_table.symbols.begin();
420  s_it!=symbol_table.symbols.end();
421  s_it++)
422  {
423  if(s_it->second.type.id()==ID_code &&
424  has_prefix(id2string(s_it->first), prefix))
425  matches.insert(s_it->first);
426  }
427 
428  if(matches.empty())
429  {
430  // Not found, silently ignore
431  res.main_function=symbol;
432  res.error_found=false;
433  res.stop_convert=true;
434  return res;
435  }
436 
437  if(matches.size()>=2)
438  {
439  message.error() << "main method in `" << main_class
440  << "' is ambiguous" << messaget::eom;
441  res.main_function=symbolt();
442  res.error_found=true;
443  res.stop_convert=true;
444  return res; // give up with error, no main
445  }
446 
447  // function symbol
448  symbol=symbol_table.symbols.find(*matches.begin())->second;
449 
450  // check if it has a body
451  if(symbol.value.is_nil() && !allow_no_body)
452  {
453  message.error() << "main method `" << main_class
454  << "' has no body" << messaget::eom;
455  res.main_function=symbol;
456  res.error_found=true;
457  res.stop_convert=true;
458  return res; // give up with error
459  }
460  }
461 
462  res.main_function=symbol;
463  res.error_found=false;
464  res.stop_convert=false;
465  return res; // give up with error
466 }
467 
477  symbol_tablet &symbol_table,
478  const irep_idt &main_class,
479  message_handlert &message_handler,
480  bool assume_init_pointers_not_null,
481  size_t max_nondet_array_length)
482 {
483  // check if the entry point is already there
484  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
485  symbol_table.symbols.end())
486  return false; // silently ignore
487 
488  messaget message(message_handler);
490  get_main_symbol(symbol_table, main_class, message_handler);
491  if(res.stop_convert)
492  return res.stop_convert;
493  symbolt symbol=res.main_function;
494 
495  assert(!symbol.value.is_nil());
496  assert(symbol.type.id()==ID_code);
497 
498  create_initialize(symbol_table);
499 
501  symbol_table,
502  symbol.location,
503  assume_init_pointers_not_null,
504  max_nondet_array_length);
505 
506  code_blockt init_code;
507 
508  // build call to initialization function
509  {
510  symbol_tablet::symbolst::iterator init_it=
511  symbol_table.symbols.find(INITIALIZE);
512 
513  if(init_it==symbol_table.symbols.end())
514  {
515  message.error() << "failed to find " INITIALIZE " symbol"
516  << messaget::eom;
517  return true; // give up with error
518  }
519 
520  code_function_callt call_init;
521  call_init.lhs().make_nil();
522  call_init.add_source_location()=symbol.location;
523  call_init.function()=init_it->second.symbol_expr();
524 
525  init_code.move_to_operands(call_init);
526  }
527 
528  // build call to the main method
529 
530  code_function_callt call_main;
531 
533  loc.set_function(symbol.name);
534  source_locationt &dloc=loc;
535 
536  call_main.add_source_location()=dloc;
537  call_main.function()=symbol.symbol_expr();
538  call_main.function().add_source_location()=dloc;
539 
540  if(to_code_type(symbol.type).return_type()!=empty_typet())
541  {
542  auxiliary_symbolt return_symbol;
543  return_symbol.mode=ID_C;
544  return_symbol.is_static_lifetime=false;
545  return_symbol.name="return'";
546  return_symbol.base_name="return";
547  return_symbol.type=to_code_type(symbol.type).return_type();
548 
549  symbol_table.add(return_symbol);
550  call_main.lhs()=return_symbol.symbol_expr();
551  }
552 
553  // add the exceptional return value
554  auxiliary_symbolt exc_symbol;
555  exc_symbol.mode=ID_C;
556  exc_symbol.is_static_lifetime=false;
557  exc_symbol.name=id2string(symbol.name)+EXC_SUFFIX;
558  exc_symbol.base_name=id2string(symbol.name)+EXC_SUFFIX;
559  exc_symbol.type=java_reference_type(empty_typet());
560  symbol_table.add(exc_symbol);
561 
562  exprt::operandst main_arguments=
564  symbol,
565  init_code,
566  symbol_table,
567  assume_init_pointers_not_null,
568  max_nondet_array_length);
569  call_main.arguments()=main_arguments;
570 
571  init_code.move_to_operands(call_main);
572 
573  java_record_outputs(symbol, main_arguments, init_code, symbol_table);
574 
575  // add "main"
576  symbolt new_symbol;
577 
578  code_typet main_type;
579  main_type.return_type()=empty_typet();
580 
581  new_symbol.name=goto_functionst::entry_point();
582  new_symbol.type.swap(main_type);
583  new_symbol.value.swap(init_code);
584  new_symbol.mode=ID_java;
585 
586  if(symbol_table.move(new_symbol))
587  {
588  message.error() << "failed to move main symbol" << messaget::eom;
589  return true;
590  }
591 
592  return false;
593 }
#define loc()
exprt::operandst java_build_arguments(const symbolt &function, code_blockt &init_code, symbol_tablet &symbol_table, bool assume_init_pointers_not_null, unsigned max_nondet_array_length)
The type of an expression.
Definition: type.h:20
irep_idt name
The unique identifier.
Definition: symbol.h:46
void set_function(const irep_idt &function)
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
symbolt & lookup(const irep_idt &identifier)
Find a symbol in the symbol table.
Base type of functions.
Definition: std_types.h:734
bool is_nil() const
Definition: irep.h:103
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
Remove function exceptional returns.
exprt & op0()
Definition: expr.h:84
#define CPROVER_PREFIX
irep_idt mode
Language mode.
Definition: symbol.h:55
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:67
const irep_idt & get_identifier() const
Definition: std_expr.h:120
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
std::vector< parametert > parameterst
Definition: std_types.h:829
exprt value
Initial value of symbol.
Definition: symbol.h:40
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, bool allow_null, symbol_tablet &symbol_table, size_t max_nondet_array_length, const source_locationt &loc)
typet & type()
Definition: expr.h:60
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
configt config
Definition: config.cpp:21
bool java_entry_point(symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, size_t max_nondet_array_length)
find entry point and create initialization code for function symbol_table main class message_handler ...
bool is_static_lifetime
Definition: symbol.h:70
const irep_idt & id() const
Definition: irep.h:189
const irep_idt & get_base_name() const
Definition: std_types.h:787
void add(const codet &code)
Definition: std_code.h:81
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:191
typet java_type_from_string(const std::string &src)
Definition: java_types.cpp:152
argumentst & arguments()
Definition: std_code.h:689
symbolst symbols
Definition: symbol_table.h:57
The NIL expression.
Definition: std_expr.h:3764
The empty type.
Definition: std_types.h:53
std::string main
Definition: config.h:147
API to expression classes.
exprt & op1()
Definition: expr.h:87
The symbol table.
Definition: symbol_table.h:52
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:137
TO_BE_DOCUMENTED.
Definition: namespace.h:62
static void create_initialize(symbol_tablet &symbol_table)
void java_record_outputs(const symbolt &function, const exprt::operandst &main_arguments, code_blockt &init_code, symbol_tablet &symbol_table)
A function call.
Definition: std_code.h:657
size_t size() const
Definition: dstring.h:77
bitvector_typet index_type()
Definition: c_types.cpp:15
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Operator to return the address of an object.
Definition: std_expr.h:2593
main_function_resultt get_main_symbol(symbol_tablet &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool allow_no_body)
bool move(symbolt &symbol, symbolt *&new_symbol)
Move a symbol into the symbol table.
std::vector< exprt > operandst
Definition: expr.h:49
bool has_prefix(const std::string &s, const std::string &prefix)
Definition: converter.cpp:13
Pointer Logic.
typet type
Type of symbol.
Definition: symbol.h:37
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:43
API to type classes.
#define EXC_SUFFIX
exprt & function()
Definition: std_code.h:677
bool is_state_var
Definition: symbol.h:66
const parameterst & parameters() const
Definition: std_types.h:841
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:52
bool has_this() const
Definition: std_types.h:808
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:884
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
bool has_symbol(const irep_idt &name) const
Definition: symbol_table.h:87
mstreamt & error()
Definition: message.h:223
source_locationt & add_source_location()
Definition: expr.h:147
Sequential composition.
Definition: std_code.h:63
const codet & to_code(const exprt &expr)
Definition: std_code.h:49
Expression to hold a symbol (variable)
Definition: std_expr.h:82
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:120
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
A statement in a programming language.
Definition: std_code.h:19
void java_static_lifetime_init(symbol_tablet &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, unsigned max_nondet_array_length)
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static bool should_init_symbol(const symbolt &sym)
bool empty() const
Definition: dstring.h:61
#define INITIALIZE
const typet & return_type() const
Definition: std_types.h:831
Assignment.
Definition: std_code.h:144
bool is_lvalue
Definition: symbol.h:71
array index operator
Definition: std_expr.h:1170