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>
13 #include <util/string_constant.h>
14 #include <util/suffix.h>
15 
18 
20 
22 #include "java_object_factory.h"
23 #include "java_string_literals.h"
24 #include "java_utils.h"
25 #include <util/fresh_symbol.h>
26 #include <util/nondet.h>
27 
28 #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"
29 
30 static void create_initialize(symbol_table_baset &symbol_table)
31 {
32  // If __CPROVER_initialize already exists, replace it. It may already exist
33  // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.
34  symbol_table.remove(INITIALIZE_FUNCTION);
35 
36  symbolt initialize;
37  initialize.name=INITIALIZE_FUNCTION;
38  initialize.base_name=INITIALIZE_FUNCTION;
39  initialize.mode=ID_java;
40 
41  initialize.type = java_method_typet({}, empty_typet());
42 
43  code_blockt init_code;
44 
45  namespacet ns(symbol_table);
46 
47  symbol_exprt rounding_mode=
48  ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
49 
50  init_code.add(
51  code_assignt(rounding_mode, from_integer(0, rounding_mode.type())));
52 
53  initialize.value=init_code;
54 
55  symbol_table.add(initialize);
56 }
57 
58 static bool should_init_symbol(const symbolt &sym)
59 {
60  if(sym.type.id()!=ID_code &&
61  sym.is_lvalue &&
62  sym.is_state_var &&
63  sym.is_static_lifetime &&
64  sym.mode==ID_java)
65  {
66  // Consider some sort of annotation indicating a global variable that
67  // doesn't require initialisation?
68  return !sym.type.get_bool(ID_C_no_initialization_required);
69  }
70 
71  return is_java_string_literal_id(sym.name);
72 }
73 
91 {
92  static irep_idt signature =
93  "java::java.lang.Class.cproverInitializeClassLiteral:"
94  "(Ljava/lang/String;ZZZZZZZ)V";
95  return signature;
96 }
97 
104  const symbolt &symbol,
105  const symbol_table_baset &symbol_table)
106 {
107  if(symbol.value.is_not_nil())
108  return nullptr;
109  if(symbol.type != struct_tag_typet("java::java.lang.Class"))
110  return nullptr;
112  return nullptr;
114 }
115 
117 {
118  return from_integer(val ? 1 : 0, java_boolean_type());
119 }
120 
122  symbol_table_baset &symbol_table,
123  const source_locationt &source_location,
124  bool assume_init_pointers_not_null,
125  java_object_factory_parameterst object_factory_parameters,
126  const select_pointer_typet &pointer_type_selector,
127  bool string_refinement_enabled,
128  message_handlert &message_handler)
129 {
130  symbolt &initialize_symbol=*symbol_table.get_writeable(INITIALIZE_FUNCTION);
131  code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
132  object_factory_parameters.function_id = initialize_symbol.name;
133 
134  // If there are strings given using --string-input-value, we need to add
135  // them to the symbol table now, so that they appear in __CPROVER_initialize
136  // and we can refer to them later when we initialize input values.
137  for(const auto &val : object_factory_parameters.string_input_values)
138  {
139  exprt my_literal(ID_java_string_literal);
140  my_literal.set(ID_value, val);
141  // We ignore the return value of the following call, we just need to
142  // make sure the string is in the symbol table.
144  my_literal,
145  symbol_table,
146  string_refinement_enabled);
147  }
148 
149  // We need to zero out all static variables, or nondet-initialize if they're
150  // external. Iterate over a copy of the symtab, as its iterators are
151  // invalidated by object_factory:
152 
153  std::list<irep_idt> symbol_names;
154  for(const auto &entry : symbol_table.symbols)
155  symbol_names.push_back(entry.first);
156 
157  for(const auto &symname : symbol_names)
158  {
159  const symbolt &sym=*symbol_table.lookup(symname);
160  if(should_init_symbol(sym))
161  {
162  if(const symbolt *class_literal_init_method =
163  get_class_literal_initializer(sym, symbol_table))
164  {
165  const std::string &name_str = id2string(sym.name);
166  irep_idt class_name =
167  name_str.substr(0, name_str.size() - strlen(JAVA_CLASS_MODEL_SUFFIX));
168  const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
169 
170  bool class_is_array = is_java_array_tag(sym.name);
171 
172  exprt name_literal(ID_java_string_literal);
173  name_literal.set(ID_value, to_class_type(class_symbol.type).get_tag());
174 
175  symbol_exprt class_name_literal =
177  name_literal, symbol_table, string_refinement_enabled);
178 
179  // Call the literal initializer method instead of a nondet initializer:
180 
181  // For arguments we can't parse yet:
183 
184  // Argument order is: name, isAnnotation, isArray, isInterface,
185  // isSynthetic, isLocalClass, isMemberClass, isEnum
186 
187  code_function_callt initializer_call(
188  class_literal_init_method->symbol_expr(),
189  {// this:
191  // name:
192  address_of_exprt(class_name_literal),
193  // isAnnotation:
194  constant_bool(class_symbol.type.get_bool(ID_is_annotation)),
195  // isArray:
196  constant_bool(class_is_array),
197  // isInterface:
198  constant_bool(class_symbol.type.get_bool(ID_interface)),
199  // isSynthetic:
200  constant_bool(class_symbol.type.get_bool(ID_synthetic)),
201  // isLocalClass:
202  nondet_bool,
203  // isMemberClass:
204  nondet_bool,
205  // isEnum:
206  constant_bool(class_symbol.type.get_bool(ID_enumeration))});
207 
208  // First initialize the object as prior to a constructor:
209  namespacet ns(symbol_table);
210 
211  auto zero_object = zero_initializer(sym.type, source_locationt(), ns);
212  if(!zero_object.has_value())
213  {
214  messaget message(message_handler);
215  message.error() << "failed to zero-initialize " << sym.name
216  << messaget::eom;
217  throw 0;
218  }
220  to_struct_expr(*zero_object), ns, to_struct_tag_type(sym.type));
221 
222  code_block.add(
223  std::move(code_assignt(sym.symbol_expr(), *zero_object)));
224 
225  // Then call the init function:
226  code_block.add(std::move(initializer_call));
227  }
228  else if(sym.value.is_nil() && sym.type!=empty_typet())
229  {
230  const bool is_class_model =
231  has_suffix(id2string(sym.name), "@class_model");
232  const bool not_allow_null = is_java_string_literal_id(sym.name) ||
234  assume_init_pointers_not_null;
235 
236  java_object_factory_parameterst parameters = object_factory_parameters;
237  if(not_allow_null && !is_class_model)
238  parameters.min_null_tree_depth = 1;
239 
241  sym.symbol_expr(),
242  code_block,
243  symbol_table,
244  source_location,
245  false,
247  parameters,
248  pointer_type_selector,
250  }
251  else if(sym.value.is_not_nil())
252  {
253  code_assignt assignment(sym.symbol_expr(), sym.value);
254  assignment.add_source_location()=source_location;
255  code_block.add(assignment);
256  }
257  }
258  }
259 }
260 
266 bool is_java_main(const symbolt &function)
267 {
268  bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD);
269  const java_method_typet &function_type = to_java_method_type(function.type);
270  const typet &string_array_type = java_type_from_string("[Ljava/lang/String;");
271  // checks whether the function is static and has a single String[] parameter
272  bool is_static = !function_type.has_this();
273  // this should be implied by the signature
274  const java_method_typet::parameterst &parameters = function_type.parameters();
275  bool has_correct_type = function_type.return_type().id() == ID_empty &&
276  parameters.size() == 1 &&
277  parameters[0].type().full_eq(string_array_type);
278  bool public_access = function_type.get(ID_access) == ID_public;
279  return named_main && is_static && has_correct_type && public_access;
280 }
281 
292  const symbolt &function,
293  code_blockt &init_code,
294  symbol_table_baset &symbol_table,
295  bool assume_init_pointers_not_null,
296  java_object_factory_parameterst object_factory_parameters,
297  const select_pointer_typet &pointer_type_selector)
298 {
299  const java_method_typet::parameterst &parameters =
300  to_java_method_type(function.type).parameters();
301 
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 declare such object as an ID_input
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  java_object_factory_parameterst parameters = object_factory_parameters;
326  // only pointer must be non-null
327  if(assume_init_pointers_not_null || is_this)
328  parameters.min_null_tree_depth = 1;
329  // in main() also the array elements of the argument must be non-null
330  if(is_main)
331  parameters.min_null_tree_depth = 2;
332 
334 
335  namespacet ns(symbol_table);
336 
337  // Generate code to allocate and non-deterministicaly initialize the
338  // argument, if the argument has different possible object types (e.g., from
339  // casts in the function body), then choose one in a non-deterministic way.
340  const auto alternatives =
341  pointer_type_selector.get_parameter_alternative_types(
342  function.name, p.get_identifier(), ns);
343  if(alternatives.empty())
344  {
345  main_arguments[param_number] = object_factory(
346  p.type(),
347  base_name,
348  init_code,
349  symbol_table,
350  parameters,
352  function.location,
353  pointer_type_selector);
354  }
355  else
356  {
357  INVARIANT(!is_this, "We cannot have different types for `this` here");
358  // create a non-deterministic switch between all possible values for the
359  // type of the parameter.
360  code_switcht code_switch;
361 
362  // the idea is to get a new symbol for the parameter value `tmp`
363 
364  // then add a non-deterministic switch over all possible input types,
365  // construct the object type at hand and assign to `tmp`
366 
367  // switch(...)
368  // {
369  // case obj1:
370  // tmp_expr = object_factory(...)
371  // param = tmp_expr
372  // break
373  // ...
374  // }
375  // method(..., param, ...)
376  //
377 
378  const symbolt result_symbol = get_fresh_aux_symbol(
379  p.type(),
380  id2string(function.name),
381  "nondet_parameter_" + std::to_string(param_number),
382  function.location,
383  ID_java,
384  symbol_table);
385  main_arguments[param_number] = result_symbol.symbol_expr();
386 
387  std::vector<codet> cases(alternatives.size());
388  const auto initialize_parameter = [&](const struct_tag_typet &type) {
389  code_blockt init_code_for_type;
390  exprt init_expr_for_parameter = object_factory(
391  java_reference_type(type),
392  id2string(base_name) + "_alternative_" +
393  id2string(type.get_identifier()),
394  init_code_for_type,
395  symbol_table,
396  parameters,
398  function.location,
399  pointer_type_selector);
400  init_code_for_type.add(
401  code_assignt(
402  result_symbol.symbol_expr(),
403  typecast_exprt(init_expr_for_parameter, p.type())));
404  return init_code_for_type;
405  };
406 
407  std::transform(
408  alternatives.begin(),
409  alternatives.end(),
410  cases.begin(),
411  initialize_parameter);
412 
413  init_code.add(
415  id2string(function.name) + "_" + std::to_string(param_number),
416  cases,
417  java_int_type(),
418  ID_java,
419  function.location,
420  symbol_table));
421  }
422 
423  // record as an input
424  codet input(ID_input);
425  input.operands().resize(2);
426  input.op0()=
428  index_exprt(
429  string_constantt(base_name),
430  from_integer(0, index_type())));
431  input.op1()=main_arguments[param_number];
432  input.add_source_location()=function.location;
433 
434  init_code.add(std::move(input));
435  }
436 
437  return main_arguments;
438 }
439 
441  const symbolt &function,
442  const exprt::operandst &main_arguments,
443  code_blockt &init_code,
444  symbol_table_baset &symbol_table)
445 {
446  const java_method_typet::parameterst &parameters =
447  to_java_method_type(function.type).parameters();
448 
449  exprt::operandst result;
450  result.reserve(parameters.size()+1);
451 
452  bool has_return_value =
453  to_java_method_type(function.type).return_type() != empty_typet();
454 
455  if(has_return_value)
456  {
457  // record return value
458  codet output(ID_output);
459  output.operands().resize(2);
460 
461  const symbolt &return_symbol=
462  *symbol_table.lookup(JAVA_ENTRY_POINT_RETURN_SYMBOL);
463 
464  output.op0()=
466  index_exprt(
467  string_constantt(return_symbol.base_name),
468  from_integer(0, index_type())));
469  output.op1()=return_symbol.symbol_expr();
470  output.add_source_location()=function.location;
471 
472  init_code.add(std::move(output));
473  }
474 
475  for(std::size_t param_number=0;
476  param_number<parameters.size();
477  param_number++)
478  {
479  const symbolt &p_symbol=
480  *symbol_table.lookup(parameters[param_number].get_identifier());
481 
482  if(p_symbol.type.id()==ID_pointer)
483  {
484  // record as an output
485  codet output(ID_output);
486  output.operands().resize(2);
487  output.op0()=
489  index_exprt(
490  string_constantt(p_symbol.base_name),
491  from_integer(0, index_type())));
492  output.op1()=main_arguments[param_number];
493  output.add_source_location()=function.location;
494 
495  init_code.add(std::move(output));
496  }
497  }
498 
499  // record exceptional return variable as output
500  codet output(ID_output);
501  output.operands().resize(2);
502 
503  // retrieve the exception variable
504  const symbolt exc_symbol=*symbol_table.lookup(
506 
507  output.op0()=address_of_exprt(
509  from_integer(0, index_type())));
510  output.op1()=exc_symbol.symbol_expr();
511  output.add_source_location()=function.location;
512 
513  init_code.add(std::move(output));
514 }
515 
517  const symbol_table_baset &symbol_table,
518  const irep_idt &main_class,
519  message_handlert &message_handler)
520 {
521  messaget message(message_handler);
522 
523  // find main symbol
524  if(config.main!="")
525  {
526  // Add java:: prefix
527  std::string main_identifier="java::"+config.main;
528 
529  std::string error_message;
530  irep_idt main_symbol_id=
531  resolve_friendly_method_name(config.main, symbol_table, error_message);
532 
533  if(main_symbol_id==irep_idt())
534  {
535  message.error()
536  << "main symbol resolution failed: " << error_message << messaget::eom;
538  }
539 
540  const symbolt *symbol = symbol_table.lookup(main_symbol_id);
541  INVARIANT(
542  symbol != nullptr,
543  "resolve_friendly_method_name should return a symbol-table identifier");
544 
545  return *symbol; // Return found function
546  }
547  else
548  {
549  // no function given, we look for the main class
550  assert(config.main=="");
551 
552  // are we given a main class?
553  if(main_class.empty())
554  {
555  // no, but we allow this situation to output symbol table,
556  // goto functions, etc
558  }
559 
560  std::string entry_method =
561  "java::" + id2string(main_class) + "." + JAVA_MAIN_METHOD;
562  const symbolt *symbol = symbol_table.lookup(entry_method);
563 
564  // has the class a correct main method?
565  if(!symbol || !is_java_main(*symbol))
566  {
567  // no, but we allow this situation to output symbol table,
568  // goto functions, etc
570  }
571 
572  return *symbol;
573  }
574 }
575 
611  symbol_table_baset &symbol_table,
612  const irep_idt &main_class,
613  message_handlert &message_handler,
614  bool assume_init_pointers_not_null,
615  bool assert_uncaught_exceptions,
616  const java_object_factory_parameterst &object_factory_parameters,
617  const select_pointer_typet &pointer_type_selector,
618  bool string_refinement_enabled)
619 {
620  // check if the entry point is already there
621  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
622  symbol_table.symbols.end())
623  return false; // silently ignore
624 
625  messaget message(message_handler);
627  get_main_symbol(symbol_table, main_class, message_handler);
628  if(!res.is_success())
629  return true;
630  symbolt symbol=res.main_function;
631 
632  assert(symbol.type.id()==ID_code);
633 
634  create_initialize(symbol_table);
635 
637  symbol_table,
638  symbol.location,
639  assume_init_pointers_not_null,
640  object_factory_parameters,
641  pointer_type_selector,
642  string_refinement_enabled,
643  message_handler);
644 
646  symbol,
647  symbol_table,
648  message_handler,
649  assume_init_pointers_not_null,
650  assert_uncaught_exceptions,
651  object_factory_parameters,
652  pointer_type_selector);
653 }
654 
667  const symbolt &symbol,
668  symbol_table_baset &symbol_table,
669  message_handlert &message_handler,
670  bool assume_init_pointers_not_null,
671  bool assert_uncaught_exceptions,
672  const java_object_factory_parameterst &object_factory_parameters,
673  const select_pointer_typet &pointer_type_selector)
674 {
675  messaget message(message_handler);
676  code_blockt init_code;
677 
678  // build call to initialization function
679  {
680  symbol_tablet::symbolst::const_iterator init_it=
681  symbol_table.symbols.find(INITIALIZE_FUNCTION);
682 
683  if(init_it==symbol_table.symbols.end())
684  {
685  message.error() << "failed to find " INITIALIZE_FUNCTION " symbol"
686  << messaget::eom;
687  return true; // give up with error
688  }
689 
690  code_function_callt call_init(init_it->second.symbol_expr());
691  call_init.add_source_location()=symbol.location;
692 
693  init_code.add(std::move(call_init));
694  }
695 
696  // build call to the main method, of the form
697  // return = main_method(arg1, arg2, ..., argn)
698  // where return is a new variable
699  // and arg1 ... argn are constructed below as well
700 
702  loc.set_function(symbol.name);
703  source_locationt &dloc=loc;
704 
705  // function to call
706  code_function_callt call_main(symbol.symbol_expr());
707  call_main.add_source_location()=dloc;
708  call_main.function().add_source_location()=dloc;
709 
710  // if the method return type is not void, store return value in a new variable
711  // named 'return'
713  {
714  auxiliary_symbolt return_symbol;
715  return_symbol.mode=ID_java;
716  return_symbol.is_static_lifetime=false;
717  return_symbol.name=JAVA_ENTRY_POINT_RETURN_SYMBOL;
718  return_symbol.base_name="return";
719  return_symbol.type = to_java_method_type(symbol.type).return_type();
720 
721  symbol_table.add(return_symbol);
722  call_main.lhs()=return_symbol.symbol_expr();
723  }
724 
725  // add the exceptional return value
726  auxiliary_symbolt exc_symbol;
727  exc_symbol.mode=ID_java;
729  exc_symbol.base_name=exc_symbol.name;
730  exc_symbol.type=java_reference_type(empty_typet());
731  symbol_table.add(exc_symbol);
732 
733  // Zero-initialise the top-level exception catch variable:
734  init_code.add(code_assignt(
735  exc_symbol.symbol_expr(),
736  null_pointer_exprt(to_pointer_type(exc_symbol.type))));
737 
738  // create code that allocates the objects used as test arguments and
739  // non-deterministically initializes them
740  exprt::operandst main_arguments=
742  symbol,
743  init_code,
744  symbol_table,
745  assume_init_pointers_not_null,
746  object_factory_parameters,
747  pointer_type_selector);
748  call_main.arguments()=main_arguments;
749 
750  // Create target labels for the toplevel exception handler:
751  code_labelt toplevel_catch("toplevel_catch", code_skipt());
752  code_labelt after_catch("after_catch", code_skipt());
753 
754  code_blockt call_block;
755 
756  // Push a universal exception handler:
757  // Catch all exceptions:
758  // This is equivalent to catching Throwable, but also works if some of
759  // the class hierarchy is missing so that we can't determine that
760  // the thrown instance is an indirect child of Throwable
761  code_push_catcht push_universal_handler(
762  irep_idt(), toplevel_catch.get_label());
763  irept catch_type_list(ID_exception_list);
764  irept catch_target_list(ID_label);
765 
766  call_block.add(std::move(push_universal_handler));
767 
768  // we insert the call to the method AFTER the argument initialization code
769  call_block.add(std::move(call_main));
770 
771  // Pop the handler:
772  code_pop_catcht pop_handler;
773  call_block.add(std::move(pop_handler));
774  init_code.add(std::move(call_block));
775 
776  // Normal return: skip the exception handler:
777  init_code.add(code_gotot(after_catch.get_label()));
778 
779  // Exceptional return: catch and assign to exc_symbol.
780  code_landingpadt landingpad(exc_symbol.symbol_expr());
781  init_code.add(std::move(toplevel_catch));
782  init_code.add(std::move(landingpad));
783 
784  // Converge normal and exceptional return:
785  init_code.add(std::move(after_catch));
786 
787  // declare certain (which?) variables as test outputs
788  java_record_outputs(symbol, main_arguments, init_code, symbol_table);
789 
790  // add uncaught-exception check if requested
791  if(assert_uncaught_exceptions)
792  {
794  init_code, exc_symbol, symbol.location);
795  }
796 
797  // create a symbol for the __CPROVER__start function, associate the code that
798  // we just built and register it in the symbol table
799  symbolt new_symbol;
800 
801  new_symbol.name=goto_functionst::entry_point();
802  new_symbol.type = java_method_typet({}, empty_typet());
803  new_symbol.value.swap(init_code);
804  new_symbol.mode=ID_java;
805 
806  if(!symbol_table.insert(std::move(new_symbol)).second)
807  {
808  message.error() << "failed to move main symbol" << messaget::eom;
809  return true;
810  }
811 
812  return false;
813 }
#define loc()
#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL
The type of an expression, extends irept.
Definition: type.h:27
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Semantic type conversion.
Definition: std_expr.h:2277
codet representing a switch statement.
Definition: std_code.h:705
bool is_nil() const
Definition: irep.h:172
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
std::vector< parametert > parameterst
Definition: std_types.h:754
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
typet java_boolean_type()
Definition: java_types.cpp:72
exprt & op0()
Definition: expr.h:84
#define CPROVER_PREFIX
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
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)
Given the symbol_table and the main_class to test, this function generates a new function __CPROVER__...
irep_idt mode
Language mode.
Definition: symbol.h:49
bool is_java_string_literal_id(const irep_idt &id)
Definition: java_utils.cpp:111
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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.
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
typet java_int_type()
Definition: java_types.cpp:32
#define JAVA_ENTRY_POINT_RETURN_SYMBOL
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
Definition: std_code.h:1845
Goto Programs with Functions.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
Fresh auxiliary symbol creation.
The null pointer constant.
Definition: std_expr.h:4471
Allocate local stacked objects.
exprt value
Initial value of symbol.
Definition: symbol.h:34
A struct tag type, i.e., struct_typet with an identifier.
Definition: std_types.h:517
codet representation of a goto statement.
Definition: std_code.h:983
typet & type()
Return the type of the expression.
Definition: expr.h:68
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:1933
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
Definition: std_types.h:409
Allocate global objects.
Symbol table entry.
Definition: symbol.h:27
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...
A constant literal expression.
Definition: std_expr.h:4384
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:239
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:173
configt config
Definition: config.cpp:24
std::list< std::string > string_input_values
Force one of finitely many explicitly given input strings.
#define JAVA_MAIN_METHOD
bool is_static_lifetime
Definition: symbol.h:65
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function &#39;invariant_violated_string&#39;.
Definition: invariant.h:400
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...
static 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)
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:259
const irep_idt & get_base_name() const
Definition: std_types.h:833
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
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:492
void add(const codet &code)
Definition: std_code.h:189
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
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 &#39;switch_cases&#39;.
Definition: nondet.cpp:87
irep_idt get_java_class_literal_initializer_signature()
Get the symbol name of java.lang.Class&#39; initializer method.
The empty type.
Definition: std_types.h:48
std::string main
Definition: config.h:172
#define INITIALIZE_FUNCTION
exprt & op1()
Definition: expr.h:87
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:148
mstreamt & error() const
Definition: message.h:386
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
codet representation of a label for branch targets.
Definition: std_code.h:1256
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
void java_record_outputs(const symbolt &function, const exprt::operandst &main_arguments, code_blockt &init_code, symbol_table_baset &symbol_table)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
Base class for tree-like data structures with sharing.
Definition: irep.h:156
codet representation of a function call statement.
Definition: std_code.h:1036
bool is_java_main(const symbolt &function)
Checks whether the given symbol is a valid java main method i.e.
size_t size() const
Definition: dstring.h:91
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
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:116
bitvector_typet index_type()
Definition: c_types.cpp:16
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
Operator to return the address of an object.
Definition: std_expr.h:3255
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Definition: std_expr.h:1942
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:410
const symbolst & symbols
size_t min_null_tree_depth
To force a certain depth of non-null objects.
std::vector< exprt > operandst
Definition: expr.h:57
static eomt eom
Definition: message.h:284
static constant_exprt constant_bool(bool val)
typet type
Type of symbol.
Definition: symbol.h:31
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:37
Allocate dynamic objects (using MALLOC)
const java_method_typet & to_java_method_type(const typet &type)
Definition: java_types.h:338
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
bool generate_java_start_function(const symbolt &symbol, symbol_table_baset &symbol_table, 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)
Generate a _start function for a specific function.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
Base class for all expressions.
Definition: expr.h:54
bool is_state_var
Definition: symbol.h:61
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...
const parameterst & parameters() const
Definition: std_types.h:893
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
The symbol table base class interface.
bool has_this() const
Definition: std_types.h:854
#define JAVA_CLASS_MODEL_SUFFIX
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, allocation_typet alloc_type, const source_locationt &loc, const select_pointer_typet &pointer_type_selector)
Similar to gen_nondet_init below, but instead of allocating and non-deterministically initializing th...
symbol_exprt get_or_create_string_literal_symbol(const 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.
exprt::operandst java_build_arguments(const symbolt &function, code_blockt &init_code, 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)
Extends init_code with code that allocates the objects used as test arguments for the function under ...
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...
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
void gen_nondet_init(const exprt &expr, code_blockt &init_code, symbol_table_baset &symbol_table, const source_locationt &loc, bool skip_classid, allocation_typet alloc_type, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, update_in_placet update_in_place)
Initializes a primitive-typed or reference-typed object tree rooted at expr, allocating child objects...
void swap(irept &irep)
Definition: irep.h:303
source_locationt & add_source_location()
Definition: expr.h:233
A codet representing sequential composition of program statements.
Definition: std_code.h:150
const codet & to_code(const exprt &expr)
Definition: std_code.h:136
const irep_idt & get_label() const
Definition: std_code.h:1279
A codet representing a skip statement.
Definition: std_code.h:237
Expression to hold a symbol (variable)
Definition: std_expr.h:143
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:224
bool has_suffix(const std::string &s, const std::string &suffix)
Definition: suffix.h:15
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Extract class identifier.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
Definition: std_types.h:1544
dstringt irep_idt
Definition: irep.h:32
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
irep_idt get_tag() const
Definition: std_types.h:226
operandst & operands()
Definition: expr.h:78
static void create_initialize(symbol_table_baset &symbol_table)
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static bool should_init_symbol(const symbolt &sym)
const irep_idt & get_identifier() const
Definition: std_types.h:828
bool empty() const
Definition: dstring.h:75
const typet & return_type() const
Definition: std_types.h:883
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
A codet representing an assignment in the program.
Definition: std_code.h:256
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
A statement that catches an exception, assigning the exception in flight to an expression (e...
Definition: std_code.h:1964
bool is_lvalue
Definition: symbol.h:66
Array index operator.
Definition: std_expr.h:1595