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 <util/config.h>
12 #include <util/expr_initializer.h>
14 #include <util/nondet.h>
15 #include <util/suffix.h>
16 
20 
22 
24 #include "java_bytecode_language.h"
25 #include "java_object_factory.h"
26 #include "java_string_literals.h"
27 #include "java_types.h"
28 #include "java_utils.h"
29 
30 #include <cstring>
31 
32 #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"
33 
35  const symbolt &function,
36  const symbol_table_baset &symbol_table);
37 
39  const symbolt &function,
40  const std::vector<exprt> &arguments,
41  const symbol_table_baset &symbol_table);
42 
43 static codet record_exception(
44  const symbolt &function,
45  const symbol_table_baset &symbol_table);
46 
48 {
49  // If __CPROVER_initialize already exists, replace it. It may already exist
50  // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.
51  symbol_table.remove(INITIALIZE_FUNCTION);
52 
53  symbolt initialize;
54  initialize.name=INITIALIZE_FUNCTION;
55  initialize.base_name=INITIALIZE_FUNCTION;
56  initialize.mode=ID_java;
57 
58  initialize.type = java_method_typet({}, java_void_type());
59  symbol_table.add(initialize);
60 }
61 
62 static bool should_init_symbol(const symbolt &sym)
63 {
64  if(sym.type.id()!=ID_code &&
65  sym.is_lvalue &&
66  sym.is_state_var &&
67  sym.is_static_lifetime &&
68  sym.mode==ID_java)
69  {
70  // Consider some sort of annotation indicating a global variable that
71  // doesn't require initialisation?
72  return !sym.type.get_bool(ID_C_no_initialization_required);
73  }
74 
75  return is_java_string_literal_id(sym.name);
76 }
77 
79 {
80  static irep_idt signature =
81  "java::java.lang.Class.cproverInitializeClassLiteral:"
82  "(Ljava/lang/String;ZZZZZZZ)V";
83  return signature;
84 }
85 
92  const symbolt &symbol,
93  const symbol_table_baset &symbol_table)
94 {
95  if(symbol.value.is_not_nil())
96  return nullptr;
97  if(symbol.type != struct_tag_typet("java::java.lang.Class"))
98  return nullptr;
100  return nullptr;
102 }
103 
105 {
106  return from_integer(val ? 1 : 0, java_boolean_type());
107 }
108 
110  symbol_table_baset &symbol_table,
111  const source_locationt &source_location,
112  bool assume_init_pointers_not_null,
113  java_object_factory_parameterst object_factory_parameters,
114  const select_pointer_typet &pointer_type_selector,
115  bool string_refinement_enabled,
116  message_handlert &message_handler)
117 {
118  symbolt &initialize_symbol =
120  PRECONDITION(initialize_symbol.value.is_nil());
121  code_blockt code_block;
122 
123  const symbol_exprt rounding_mode =
125  code_block.add(
126  code_assignt{rounding_mode, from_integer(0, rounding_mode.type())});
127 
128  object_factory_parameters.function_id = initialize_symbol.name;
129 
130  // If there are strings given using --string-input-value, we need to add
131  // them to the symbol table now, so that they appear in __CPROVER_initialize
132  // and we can refer to them later when we initialize input values.
133  for(const auto &val : object_factory_parameters.string_input_values)
134  {
135  // We ignore the return value of the following call, we just need to
136  // make sure the string is in the symbol table.
138  val, symbol_table, string_refinement_enabled);
139  }
140 
141  // We need to zero out all static variables, or nondet-initialize if they're
142  // external. Iterate over a copy of the symtab, as its iterators are
143  // invalidated by object_factory:
144 
145  std::list<irep_idt> symbol_names;
146  for(const auto &entry : symbol_table.symbols)
147  symbol_names.push_back(entry.first);
148 
149  // Don't use a for-each loop here because the loop extends the list, and the
150  // for-each loop may only read `.end()` once.
151  for(
152  auto symbol_it = symbol_names.begin();
153  symbol_it != symbol_names.end();
154  ++symbol_it)
155  {
156  const auto &symname = *symbol_it;
157  const symbolt &sym = symbol_table.lookup_ref(symname);
158  if(should_init_symbol(sym))
159  {
160  if(const symbolt *class_literal_init_method =
161  get_class_literal_initializer(sym, symbol_table))
162  {
163  const std::string &name_str = id2string(sym.name);
164  irep_idt class_name =
165  name_str.substr(0, name_str.size() - strlen(JAVA_CLASS_MODEL_SUFFIX));
166  const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
167 
168  bool class_is_array = is_java_array_tag(sym.name);
169 
170  journalling_symbol_tablet journalling_table =
171  journalling_symbol_tablet::wrap(symbol_table);
172 
174  to_class_type(class_symbol.type).get_tag(),
175  journalling_table,
176  string_refinement_enabled);
177 
178  // If that created any new symbols make sure we initialise those too:
179  const auto &new_symbols = journalling_table.get_inserted();
180  symbol_names.insert(
181  symbol_names.end(), new_symbols.begin(), new_symbols.end());
182 
183  // Call the literal initializer method instead of a nondet initializer:
184 
185  // For arguments we can't parse yet:
187 
188  const auto &java_class_type = to_java_class_type(class_symbol.type);
189 
190  // Argument order is: name, isAnnotation, isArray, isInterface,
191  // isSynthetic, isLocalClass, isMemberClass, isEnum
192 
193  code_function_callt initializer_call(
194  class_literal_init_method->symbol_expr(),
195  {// this:
196  address_of_exprt(sym.symbol_expr()),
197  // name:
198  address_of_exprt(class_name_literal),
199  // isAnnotation:
200  constant_bool(java_class_type.get_is_annotation()),
201  // isArray:
202  constant_bool(class_is_array),
203  // isInterface:
204  constant_bool(java_class_type.get_interface()),
205  // isSynthetic:
206  constant_bool(java_class_type.get_synthetic()),
207  // isLocalClass:
208  nondet_bool,
209  // isMemberClass:
210  nondet_bool,
211  // isEnum:
212  constant_bool(java_class_type.get_is_enumeration())});
213 
214  // First initialize the object as prior to a constructor:
215  namespacet ns(symbol_table);
216 
217  auto zero_object = zero_initializer(sym.type, source_locationt(), ns);
218  if(!zero_object.has_value())
219  {
220  messaget message(message_handler);
221  message.error() << "failed to zero-initialize " << sym.name
222  << messaget::eom;
223  throw 0;
224  }
226  to_struct_expr(*zero_object), ns, to_struct_tag_type(sym.type));
227 
228  code_block.add(
229  std::move(code_assignt(sym.symbol_expr(), *zero_object)));
230 
231  // Then call the init function:
232  code_block.add(std::move(initializer_call));
233  }
234  else if(sym.value.is_nil() && sym.type != java_void_type())
235  {
236  const bool is_class_model =
237  has_suffix(id2string(sym.name), "@class_model");
238  const bool not_allow_null = is_java_string_literal_id(sym.name) ||
240  assume_init_pointers_not_null;
241 
242  java_object_factory_parameterst parameters = object_factory_parameters;
243  if(not_allow_null && !is_class_model)
244  parameters.min_null_tree_depth = 1;
245 
247  sym.symbol_expr(),
248  code_block,
249  symbol_table,
250  source_location,
251  false,
252  lifetimet::STATIC_GLOBAL,
253  parameters,
254  pointer_type_selector,
255  update_in_placet::NO_UPDATE_IN_PLACE,
256  message_handler);
257  }
258  else if(sym.value.is_not_nil())
259  {
260  code_assignt assignment(sym.symbol_expr(), sym.value);
261  assignment.add_source_location()=source_location;
262  code_block.add(assignment);
263  }
264  }
265  }
266  initialize_symbol.value = std::move(code_block);
267 }
268 
274 bool is_java_main(const symbolt &function)
275 {
276  bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD);
277  const java_method_typet &function_type = to_java_method_type(function.type);
278  const auto string_array_type = java_type_from_string("[Ljava/lang/String;");
279  // checks whether the function is static and has a single String[] parameter
280  bool is_static = !function_type.has_this();
281  // this should be implied by the signature
282  const java_method_typet::parameterst &parameters = function_type.parameters();
283  bool has_correct_type = function_type.return_type().id() == ID_empty &&
284  parameters.size() == 1 &&
285  parameters[0].type().full_eq(*string_array_type);
286  bool public_access = function_type.get(ID_access) == ID_public;
287  return named_main && is_static && has_correct_type && public_access;
288 }
289 
290 std::pair<code_blockt, std::vector<exprt>> java_build_arguments(
291  const symbolt &function,
292  symbol_table_baset &symbol_table,
293  bool assume_init_pointers_not_null,
294  java_object_factory_parameterst object_factory_parameters,
295  const select_pointer_typet &pointer_type_selector,
296  message_handlert &message_handler)
297 {
298  const java_method_typet &function_type = to_java_method_type(function.type);
299  const java_method_typet::parameterst &parameters = function_type.parameters();
300 
301  code_blockt init_code;
302  exprt::operandst main_arguments;
303  main_arguments.resize(parameters.size());
304 
305  // certain method arguments cannot be allowed to be null, we set the following
306  // variable to true iff the method under test is the "main" method, which will
307  // be called (by the jvm) with arguments that are never null
308  bool is_main = is_java_main(function);
309 
310  // we iterate through all the parameters of the function under test, allocate
311  // an object for that parameter (recursively allocating other objects
312  // necessary to initialize it), and mark such object using `code_inputt`.
313  for(std::size_t param_number=0;
314  param_number<parameters.size();
315  param_number++)
316  {
317  const java_method_typet::parametert &p = parameters[param_number];
318  const irep_idt base_name=p.get_base_name().empty()?
319  ("argument#"+std::to_string(param_number)):p.get_base_name();
320 
321  // true iff this parameter is the `this` pointer of the method, which cannot
322  // be null
323  bool is_this=(param_number==0) && parameters[param_number].get_this();
324 
325  if(is_this && function_type.get_is_constructor())
326  {
327  const symbol_exprt result = fresh_java_symbol(
328  p.type(),
329  "this_parameter",
330  function.location,
331  function.name,
332  symbol_table)
333  .symbol_expr();
334  main_arguments[param_number] = result;
335  init_code.add(code_declt{result});
336  init_code.add(code_assignt{
337  result,
338  side_effect_exprt{ID_java_new, {}, p.type(), function.location}});
339  continue;
340  }
341 
342  java_object_factory_parameterst factory_parameters =
343  object_factory_parameters;
344  // only pointer must be non-null
345  if(assume_init_pointers_not_null || is_this)
346  factory_parameters.min_null_tree_depth = 1;
347  // in main() also the array elements of the argument must be non-null
348  if(is_main)
349  factory_parameters.min_null_tree_depth = 2;
350 
351  factory_parameters.function_id = goto_functionst::entry_point();
352 
353  namespacet ns(symbol_table);
354 
355  // Generate code to allocate and non-deterministicaly initialize the
356  // argument, if the argument has different possible object types (e.g., from
357  // casts in the function body), then choose one in a non-deterministic way.
358  const auto alternatives =
359  pointer_type_selector.get_parameter_alternative_types(
360  function.name, p.get_identifier(), ns);
361  if(alternatives.empty())
362  {
363  main_arguments[param_number] = object_factory(
364  p.type(),
365  base_name,
366  init_code,
367  symbol_table,
368  factory_parameters,
370  function.location,
371  pointer_type_selector,
372  message_handler);
373  }
374  else
375  {
376  INVARIANT(!is_this, "We cannot have different types for `this` here");
377  // create a non-deterministic switch between all possible values for the
378  // type of the parameter.
379 
380  // the idea is to get a new symbol for the parameter value `tmp`
381 
382  // then add a non-deterministic switch over all possible input types,
383  // construct the object type at hand and assign to `tmp`
384 
385  // switch(...)
386  // {
387  // case obj1:
388  // tmp_expr = object_factory(...)
389  // param = tmp_expr
390  // break
391  // ...
392  // }
393  // method(..., param, ...)
394  //
395 
397  p.type(),
398  "nondet_parameter_" + std::to_string(param_number),
399  function.location,
400  function.name,
401  symbol_table);
402  main_arguments[param_number] = result_symbol.symbol_expr();
403 
404  std::vector<codet> cases;
405  cases.reserve(alternatives.size());
406  for(const auto &type : alternatives)
407  {
408  code_blockt init_code_for_type;
409  exprt init_expr_for_parameter = object_factory(
410  java_reference_type(type),
411  id2string(base_name) + "_alternative_" +
412  id2string(type.get_identifier()),
413  init_code_for_type,
414  symbol_table,
415  factory_parameters,
417  function.location,
418  pointer_type_selector,
419  message_handler);
420  init_code_for_type.add(
421  code_assignt(
423  typecast_exprt(init_expr_for_parameter, p.type())));
424  cases.push_back(init_code_for_type);
425  }
426 
427  init_code.add(
429  id2string(function.name) + "_" + std::to_string(param_number),
430  cases,
431  java_int_type(),
432  ID_java,
433  function.location,
434  symbol_table));
435  }
436 
437  // record as an input
438  init_code.add(
439  code_inputt{base_name, main_arguments[param_number], function.location});
440  }
441 
442  return make_pair(init_code, main_arguments);
443 }
444 
447  const symbolt &function,
448  const exprt::operandst &main_arguments,
449  symbol_table_baset &symbol_table)
450 {
451  code_blockt init_code;
452 
453  if(auto return_value = record_return_value(function, symbol_table))
454  {
455  init_code.add(std::move(*return_value));
456  }
457 
458  init_code.append(
459  record_pointer_parameters(function, main_arguments, symbol_table));
460 
461  init_code.add(record_exception(function, symbol_table));
462 
463  return init_code;
464 }
465 
467  const symbolt &function,
468  const symbol_table_baset &symbol_table)
469 {
470  if(to_java_method_type(function.type).return_type() == java_void_type())
471  return {};
472 
473  const symbolt &return_symbol =
475 
476  return code_outputt{
477  return_symbol.base_name, return_symbol.symbol_expr(), function.location};
478 }
479 
481  const symbolt &function,
482  const std::vector<exprt> &arguments,
483  const symbol_table_baset &symbol_table)
484 {
485  const java_method_typet::parameterst &parameters =
486  to_java_method_type(function.type).parameters();
487 
488  code_blockt init_code;
489 
490  for(std::size_t param_number = 0; param_number < parameters.size();
491  param_number++)
492  {
493  const symbolt &p_symbol =
494  symbol_table.lookup_ref(parameters[param_number].get_identifier());
495 
496  if(!can_cast_type<pointer_typet>(p_symbol.type))
497  continue;
498 
499  init_code.add(code_outputt{
500  p_symbol.base_name, arguments[param_number], function.location});
501  }
502  return init_code;
503 }
504 
506  const symbolt &function,
507  const symbol_table_baset &symbol_table)
508 {
509  // retrieve the exception variable
510  const symbolt &exc_symbol =
512 
513  // record exceptional return variable as output
514  return code_outputt{
515  exc_symbol.base_name, exc_symbol.symbol_expr(), function.location};
516 }
517 
519  const symbol_table_baset &symbol_table,
520  const irep_idt &main_class,
521  message_handlert &message_handler)
522 {
523  messaget message(message_handler);
524 
525  // find main symbol
526  if(config.main.has_value())
527  {
528  std::string error_message;
529  irep_idt main_symbol_id = resolve_friendly_method_name(
530  config.main.value(), symbol_table, error_message);
531 
532  if(main_symbol_id.empty())
533  {
534  message.error()
535  << "main symbol resolution failed: " << error_message << messaget::eom;
537  }
538 
539  const symbolt *symbol = symbol_table.lookup(main_symbol_id);
540  INVARIANT(
541  symbol != nullptr,
542  "resolve_friendly_method_name should return a symbol-table identifier");
543 
544  return *symbol; // Return found function
545  }
546  else
547  {
548  // are we given a main class?
549  if(main_class.empty())
550  {
551  // no, but we allow this situation to output symbol table,
552  // goto functions, etc
554  }
555 
556  std::string entry_method =
557  "java::" + id2string(main_class) + "." + JAVA_MAIN_METHOD;
558  const symbolt *symbol = symbol_table.lookup(entry_method);
559 
560  // has the class a correct main method?
561  if(!symbol || !is_java_main(*symbol))
562  {
563  // no, but we allow this situation to output symbol table,
564  // goto functions, etc
566  }
567 
568  return *symbol;
569  }
570 }
571 
573  symbol_table_baset &symbol_table,
574  const irep_idt &main_class,
575  message_handlert &message_handler,
576  bool assume_init_pointers_not_null,
577  bool assert_uncaught_exceptions,
578  const java_object_factory_parameterst &object_factory_parameters,
579  const select_pointer_typet &pointer_type_selector,
580  bool string_refinement_enabled,
581  const build_argumentst &build_arguments)
582 {
583  // check if the entry point is already there
584  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
585  symbol_table.symbols.end())
586  return false; // silently ignore
587 
588  messaget message(message_handler);
590  get_main_symbol(symbol_table, main_class, message_handler);
591  if(!res.is_success())
592  return true;
593  symbolt symbol=res.main_function;
594 
595  assert(symbol.type.id()==ID_code);
596 
598  symbol,
599  symbol_table,
600  message_handler,
601  assert_uncaught_exceptions,
602  object_factory_parameters,
603  pointer_type_selector,
604  build_arguments);
605 }
606 
608  const symbolt &symbol,
609  symbol_table_baset &symbol_table,
610  message_handlert &message_handler,
611  bool assert_uncaught_exceptions,
612  const java_object_factory_parameterst &object_factory_parameters,
613  const select_pointer_typet &pointer_type_selector,
614  const build_argumentst &build_arguments)
615 {
616  messaget message(message_handler);
617  code_blockt init_code;
618 
619  // build call to initialization function
620  {
621  symbol_tablet::symbolst::const_iterator init_it=
622  symbol_table.symbols.find(INITIALIZE_FUNCTION);
623 
624  if(init_it==symbol_table.symbols.end())
625  {
626  message.error() << "failed to find " INITIALIZE_FUNCTION " symbol"
627  << messaget::eom;
628  return true; // give up with error
629  }
630 
631  code_function_callt call_init(init_it->second.symbol_expr());
632  call_init.add_source_location()=symbol.location;
633 
634  init_code.add(std::move(call_init));
635  }
636 
637  // build call to the main method, of the form
638  // return = main_method(arg1, arg2, ..., argn)
639  // where return is a new variable
640  // and arg1 ... argn are constructed below as well
641 
642  source_locationt loc=symbol.location;
643  loc.set_function(symbol.name);
644  source_locationt &dloc=loc;
645 
646  // function to call
647  code_function_callt call_main(symbol.symbol_expr());
648  call_main.add_source_location()=dloc;
649  call_main.function().add_source_location()=dloc;
650 
651  // if the method return type is not void, store return value in a new variable
652  // named 'return'
654  {
655  auxiliary_symbolt return_symbol;
656  return_symbol.mode=ID_java;
657  return_symbol.is_static_lifetime=false;
658  return_symbol.name=JAVA_ENTRY_POINT_RETURN_SYMBOL;
659  return_symbol.base_name = "return'";
660  return_symbol.type = to_java_method_type(symbol.type).return_type();
661 
662  symbol_table.add(return_symbol);
663  call_main.lhs()=return_symbol.symbol_expr();
664  }
665 
666  // add the exceptional return value
667  auxiliary_symbolt exc_symbol;
668  exc_symbol.mode=ID_java;
670  exc_symbol.base_name=exc_symbol.name;
671  exc_symbol.type = java_reference_type(java_void_type());
672  symbol_table.add(exc_symbol);
673 
674  // Zero-initialise the top-level exception catch variable:
675  init_code.add(code_assignt(
676  exc_symbol.symbol_expr(),
677  null_pointer_exprt(to_pointer_type(exc_symbol.type))));
678 
679  // create code that allocates the objects used as test arguments and
680  // non-deterministically initializes them
681  const std::pair<code_blockt, std::vector<exprt>> main_arguments =
682  build_arguments(symbol, symbol_table);
683  init_code.append(main_arguments.first);
684  call_main.arguments() = main_arguments.second;
685 
686  // Create target labels for the toplevel exception handler:
687  code_labelt toplevel_catch("toplevel_catch", code_skipt());
688  code_labelt after_catch("after_catch", code_skipt());
689 
690  code_blockt call_block;
691 
692  // Push a universal exception handler:
693  // Catch all exceptions:
694  // This is equivalent to catching Throwable, but also works if some of
695  // the class hierarchy is missing so that we can't determine that
696  // the thrown instance is an indirect child of Throwable
697  code_push_catcht push_universal_handler(
698  irep_idt(), toplevel_catch.get_label());
699  irept catch_type_list(ID_exception_list);
700  irept catch_target_list(ID_label);
701 
702  call_block.add(std::move(push_universal_handler));
703 
704  // we insert the call to the method AFTER the argument initialization code
705  call_block.add(std::move(call_main));
706 
707  // Pop the handler:
708  code_pop_catcht pop_handler;
709  call_block.add(std::move(pop_handler));
710  init_code.add(std::move(call_block));
711 
712  // Normal return: skip the exception handler:
713  init_code.add(code_gotot(after_catch.get_label()));
714 
715  // Exceptional return: catch and assign to exc_symbol.
716  code_landingpadt landingpad(exc_symbol.symbol_expr());
717  init_code.add(std::move(toplevel_catch));
718  init_code.add(std::move(landingpad));
719 
720  // Converge normal and exceptional return:
721  init_code.add(std::move(after_catch));
722 
723  // Mark return value, pointer type parameters and the exception as outputs.
724  init_code.append(
725  java_record_outputs(symbol, main_arguments.second, symbol_table));
726 
727  // add uncaught-exception check if requested
728  if(assert_uncaught_exceptions)
729  {
731  init_code, exc_symbol, symbol.location);
732  }
733 
734  // create a symbol for the __CPROVER__start function, associate the code that
735  // we just built and register it in the symbol table
736  symbolt new_symbol;
737 
738  new_symbol.name=goto_functionst::entry_point();
739  new_symbol.type = java_method_typet({}, java_void_type());
740  new_symbol.value.swap(init_code);
741  new_symbol.mode=ID_java;
742 
743  if(!symbol_table.insert(std::move(new_symbol)).second)
744  {
745  message.error() << "failed to move main symbol" << messaget::eom;
746  return true;
747  }
748 
749  return false;
750 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
code_blockt
A codet representing sequential composition of program statements.
Definition: std_code.h:168
JAVA_CLASS_MODEL_SUFFIX
#define JAVA_CLASS_MODEL_SUFFIX
Definition: java_bytecode_language.h:270
symbolt::is_state_var
bool is_state_var
Definition: symbol.h:62
generate_nondet_switch
code_blockt generate_nondet_switch(const irep_idt &name_prefix, const alternate_casest &switch_cases, const typet &int_type, const irep_idt &mode, const source_locationt &source_location, symbol_table_baset &symbol_table)
Pick nondeterministically between imperative actions 'switch_cases'.
Definition: nondet.cpp:90
record_pointer_parameters
static code_blockt record_pointer_parameters(const symbolt &function, const std::vector< exprt > &arguments, const symbol_table_baset &symbol_table)
Definition: java_entry_point.cpp:480
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
java_bytecode_language.h
journalling_symbol_tablet::wrap
static journalling_symbol_tablet wrap(symbol_table_baset &base_symbol_table)
Definition: journalling_symbol_table.h:80
java_reference_type
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:88
source_locationt::set_function
void set_function(const irep_idt &function)
Definition: source_location.h:125
JAVA_ENTRY_POINT_RETURN_SYMBOL
#define JAVA_ENTRY_POINT_RETURN_SYMBOL
Definition: java_entry_point.h:21
is_java_string_literal_id
bool is_java_string_literal_id(const irep_idt &id)
Definition: java_utils.cpp:209
lifetimet::AUTOMATIC_LOCAL
@ AUTOMATIC_LOCAL
Allocate local objects with automatic lifetime.
main_function_resultt::main_function
symbolt main_function
Definition: java_entry_point.h:96
java_string_literals.h
to_class_type
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:381
get_main_symbol
main_function_resultt get_main_symbol(const symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler)
Figures out the entry point of the code to verify.
Definition: java_entry_point.cpp:518
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
object_factory_parameterst::function_id
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Definition: object_factory_parameters.h:79
JAVA_MAIN_METHOD
#define JAVA_MAIN_METHOD
Definition: java_entry_point.cpp:32
configt::main
optionalt< std::string > main
Definition: config.h:260
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:400
java_method_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:541
object_factory_parameterst::string_input_values
std::list< std::string > string_input_values
Force one of finitely many explicitly given input strings.
Definition: object_factory_parameters.h:76
exprt
Base class for all expressions.
Definition: expr.h:54
journalling_symbol_table.h
Author: Diffblue Ltd.
is_java_array_tag
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:231
build_argumentst
std::function< std::pair< code_blockt, std::vector< exprt > >(const symbolt &function, symbol_table_baset &symbol_table)> build_argumentst
Definition: java_entry_point.h:27
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
code_push_catcht
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
Definition: std_code.h:2251
struct_tag_typet
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:449
select_pointer_typet::get_parameter_alternative_types
virtual std::set< struct_tag_typet > get_parameter_alternative_types(const irep_idt &function_name, const irep_idt &parameter_name, const namespacet &ns) const
Get alternative types for a method parameter, e.g., based on the casts in the function body.
Definition: select_pointer_type.cpp:84
irep_idt
dstringt irep_idt
Definition: irep.h:37
main_function_resultt::NotFound
@ NotFound
Definition: java_entry_point.h:94
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
messaget::eom
static eomt eom
Definition: message.h:297
auxiliary_symbolt
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:147
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
get_or_create_string_literal_symbol
symbol_exprt get_or_create_string_literal_symbol(const java_string_literal_exprt &string_expr, symbol_table_baset &symbol_table, bool string_refinement_enabled)
Creates or gets an existing constant global symbol for a given string literal.
Definition: java_string_literals.cpp:38
code_pop_catcht
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:2345
has_suffix
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:17
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1238
can_cast_type< pointer_typet >
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
Definition: pointer_expr.h:49
record_exception
static codet record_exception(const symbolt &function, const symbol_table_baset &symbol_table)
Definition: java_entry_point.cpp:505
code_typet::get_is_constructor
bool get_is_constructor() const
Definition: std_types.h:685
zero_initializer
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
Definition: expr_initializer.cpp:317
main_function_resultt::is_success
bool is_success() const
Definition: java_entry_point.h:111
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
code_outputt
A codet representing the declaration that an output of a particular description has a value which cor...
Definition: std_code.h:722
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1213
irept::get_bool
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:58
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
struct_union_typet::get_tag
irep_idt get_tag() const
Definition: std_types.h:168
set_class_identifier
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const struct_tag_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct.
Definition: class_identifier.cpp:83
result_symbol
static symbolt result_symbol(const irep_idt &identifier, const typet &type, const source_locationt &source_location, symbol_tablet &symbol_table)
Definition: c_typecheck_gcc_polymorphic_builtins.cpp:600
expr_initializer.h
Expression Initialization.
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
messaget::error
mstreamt & error() const
Definition: message.h:399
java_object_factory.h
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
code_typet::parametert::get_base_name
const irep_idt & get_base_name() const
Definition: std_types.h:595
get_java_class_literal_initializer_signature
irep_idt get_java_class_literal_initializer_signature()
Get the symbol name of java.lang.Class' initializer method.
Definition: java_entry_point.cpp:78
record_return_value
static optionalt< codet > record_return_value(const symbolt &function, const symbol_table_baset &symbol_table)
Definition: java_entry_point.cpp:466
null_pointer_exprt
The null pointer constant.
Definition: pointer_expr.h:703
symbol_table_baset::get_writeable_ref
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
Definition: symbol_table_base.h:121
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
java_static_lifetime_init
void java_static_lifetime_init(symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, java_object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
Adds the body to __CPROVER_initialize.
Definition: java_entry_point.cpp:109
code_gotot
codet representation of a goto statement.
Definition: std_code.h:1157
code_labelt
codet representation of a label for branch targets.
Definition: std_code.h:1405
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
INITIALIZE_FUNCTION
#define INITIALIZE_FUNCTION
Definition: static_lifetime_init.h:22
java_entry_point.h
resolve_friendly_method_name
irep_idt resolve_friendly_method_name(const std::string &friendly_name, const symbol_table_baset &symbol_table, std::string &error)
Resolves a user-friendly method name (like packagename.Class.method) into an internal name (like java...
Definition: java_utils.cpp:214
object_factory
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, java_object_factory_parameterst parameters, lifetimet lifetime, const source_locationt &loc, const select_pointer_typet &pointer_type_selector, message_handlert &log)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
Definition: java_object_factory.cpp:1541
is_non_null_library_global
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
Definition: java_utils.cpp:522
select_pointer_typet
Definition: select_pointer_type.h:23
to_pointer_type
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: pointer_expr.h:62
is_java_main
bool is_java_main(const symbolt &function)
Checks whether the given symbol is a valid java main method i.e.
Definition: java_entry_point.cpp:274
irept::swap
void swap(irept &irep)
Definition: irep.h:453
gen_nondet_init
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, lifetimet lifetime, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place, message_handlert &log)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
Definition: java_object_factory.cpp:1624
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
dstringt::empty
bool empty() const
Definition: dstring.h:88
code_blockt::add
void add(const codet &code)
Definition: std_code.h:206
rounding_mode_identifier
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Definition: adjust_float_expressions.cpp:24
java_int_type
signedbv_typet java_int_type()
Definition: java_types.cpp:31
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:655
symbol_table_baset::remove
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
Definition: symbol_table_base.cpp:27
constant_bool
static constant_exprt constant_bool(bool val)
Definition: java_entry_point.cpp:104
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1258
fresh_java_symbol
symbolt & fresh_java_symbol(const typet &type, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &function_name, symbol_table_baset &symbol_table)
Definition: java_utils.cpp:558
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
java_type_from_string
optionalt< typet > java_type_from_string(const std::string &src, const std::string &class_name_prefix)
Transforms a string representation of a Java type into an internal type representation thereof.
Definition: java_types.cpp:559
java_entry_point
bool java_entry_point(symbol_table_baset &symbol_table, const irep_idt &main_class, message_handlert &message_handler, bool assume_init_pointers_not_null, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, const build_argumentst &build_arguments)
Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__...
Definition: java_entry_point.cpp:572
main_function_resultt
Definition: java_entry_point.h:89
java_build_arguments
std::pair< code_blockt, std::vector< exprt > > java_build_arguments(const symbolt &function, symbol_table_baset &symbol_table, bool assume_init_pointers_not_null, java_object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler)
Definition: java_entry_point.cpp:290
code_typet::has_this
bool has_this() const
Definition: std_types.h:616
java_bytecode_instrument_uncaught_exceptions
void java_bytecode_instrument_uncaught_exceptions(code_blockt &init_code, const symbolt &exc_symbol, const source_locationt &source_location)
Instruments the start function with an assertion that checks whether an exception has escaped the ent...
Definition: java_bytecode_instrument.cpp:564
config
configt config
Definition: config.cpp:25
object_factory_parameterst::min_null_tree_depth
size_t min_null_tree_depth
To force a certain depth of non-null objects.
Definition: object_factory_parameters.h:70
source_locationt
Definition: source_location.h:19
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1966
code_labelt::get_label
const irep_idt & get_label() const
Definition: std_code.h:1413
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
get_class_literal_initializer
static const symbolt * get_class_literal_initializer(const symbolt &symbol, const symbol_table_baset &symbol_table)
If symbol is a class literal, and an appropriate initializer method exists, return a pointer to its s...
Definition: java_entry_point.cpp:91
symbolt::value
exprt value
Initial value of symbol.
Definition: symbol.h:34
code_skipt
A codet representing a skip statement.
Definition: std_code.h:268
code_landingpadt
A statement that catches an exception, assigning the exception in flight to an expression (e....
Definition: std_code.h:2382
create_java_initialize
void create_java_initialize(symbol_table_baset &symbol_table)
Adds __cprover_initialize to the symbol_table but does not generate code for it yet.
Definition: java_entry_point.cpp:47
suffix.h
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
symbolt::location
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
code_inputt
A codet representing the declaration that an input of a particular description has a value which corr...
Definition: std_code.h:675
nondet.h
symbolt
Symbol table entry.
Definition: symbol.h:28
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
code_blockt::append
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
Definition: std_code.cpp:89
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
code_typet::parametert::get_identifier
const irep_idt & get_identifier() const
Definition: std_types.h:590
code_typet::parametert
Definition: std_types.h:556
main_function_resultt::Error
@ Error
Definition: java_entry_point.h:93
symbolt::is_static_lifetime
bool is_static_lifetime
Definition: symbol.h:65
goto_functions.h
Goto Programs with Functions.
should_init_symbol
static bool should_init_symbol(const symbolt &sym)
Definition: java_entry_point.cpp:62
config.h
class_identifier.h
Extract class identifier.
java_boolean_type
c_bool_typet java_boolean_type()
Definition: java_types.cpp:79
symbol_table_baset::insert
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:95
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:645
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
symbolt::is_lvalue
bool is_lvalue
Definition: symbol.h:66
to_java_class_type
const java_class_typet & to_java_class_type(const typet &type)
Definition: java_types.h:582
goto_functionst::entry_point
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Definition: goto_functions.h:92
journalling_symbol_tablet::get_inserted
const changesett & get_inserted() const
Definition: journalling_symbol_table.h:146
static_lifetime_init.h
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
java_types.h
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:235
java_record_outputs
static code_blockt java_record_outputs(const symbolt &function, const exprt::operandst &main_arguments, symbol_table_baset &symbol_table)
Mark return value, pointer type parameters and the exception as outputs.
Definition: java_entry_point.cpp:446
to_java_method_type
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:184
java_bytecode_instrument.h
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
java_void_type
empty_typet java_void_type()
Definition: java_types.cpp:37
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:293
adjust_float_expressions.h
Symbolic Execution.
java_utils.h
constant_exprt
A constant literal expression.
Definition: std_expr.h:2753
generate_java_start_function
bool generate_java_start_function(const symbolt &symbol, symbol_table_baset &symbol_table, message_handlert &message_handler, bool assert_uncaught_exceptions, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, const build_argumentst &build_arguments)
Generate a _start function for a specific function.
Definition: java_entry_point.cpp:607
journalling_symbol_tablet
A symbol table wrapper that records which entries have been updated/removedA caller can pass a journa...
Definition: journalling_symbol_table.h:36
java_method_typet
Definition: java_types.h:101
JAVA_ENTRY_POINT_EXCEPTION_SYMBOL
#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL
Definition: java_entry_point.h:22
java_object_factory_parameterst
Definition: java_object_factory_parameters.h:16
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
code_function_callt::function
exprt & function()
Definition: std_code.h:1248
side_effect_exprt
An expression containing a side effect.
Definition: std_code.h:1896
dstringt::size
size_t size() const
Definition: dstring.h:104
to_struct_expr
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1691
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:33