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