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 
26 #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"
27 
28 static void create_initialize(symbol_table_baset &symbol_table)
29 {
30  // If __CPROVER_initialize already exists, replace it. It may already exist
31  // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.
32  symbol_table.remove(INITIALIZE_FUNCTION);
33 
34  symbolt initialize;
35  initialize.name=INITIALIZE_FUNCTION;
36  initialize.base_name=INITIALIZE_FUNCTION;
37  initialize.mode=ID_java;
38 
39  initialize.type = code_typet({}, empty_typet());
40 
41  code_blockt init_code;
42 
43  namespacet ns(symbol_table);
44 
45  symbol_exprt rounding_mode=
46  ns.lookup(CPROVER_PREFIX "rounding_mode").symbol_expr();
47 
48  init_code.add(
49  code_assignt(rounding_mode, from_integer(0, rounding_mode.type())));
50 
51  initialize.value=init_code;
52 
53  symbol_table.add(initialize);
54 }
55 
56 static bool should_init_symbol(const symbolt &sym)
57 {
58  if(sym.type.id()!=ID_code &&
59  sym.is_lvalue &&
60  sym.is_state_var &&
61  sym.is_static_lifetime &&
62  sym.mode==ID_java)
63  {
64  // Consider some sort of annotation indicating a global variable that
65  // doesn't require initialisation?
66  return !sym.type.get_bool(ID_C_no_initialization_required);
67  }
68 
69  return is_java_string_literal_id(sym.name);
70 }
71 
89 {
90  static irep_idt signature =
91  "java::java.lang.Class.cproverInitializeClassLiteral:"
92  "(Ljava/lang/String;ZZZZZZZ)V";
93  return signature;
94 }
95 
102  const symbolt &symbol,
103  const symbol_table_baset &symbol_table)
104 {
105  if(symbol.value.is_not_nil())
106  return nullptr;
107  if(symbol.type != symbol_typet("java::java.lang.Class"))
108  return nullptr;
110  return nullptr;
112 }
113 
115 {
116  return from_integer(val ? 1 : 0, java_boolean_type());
117 }
118 
120  symbol_table_baset &symbol_table,
121  const source_locationt &source_location,
122  bool assume_init_pointers_not_null,
123  object_factory_parameterst object_factory_parameters,
124  const select_pointer_typet &pointer_type_selector,
125  bool string_refinement_enabled,
127 {
128  symbolt &initialize_symbol=*symbol_table.get_writeable(INITIALIZE_FUNCTION);
129  code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
130  object_factory_parameters.function_id = initialize_symbol.name;
131 
132  // We need to zero out all static variables, or nondet-initialize if they're
133  // external. Iterate over a copy of the symtab, as its iterators are
134  // invalidated by object_factory:
135 
136  std::list<irep_idt> symbol_names;
137  for(const auto &entry : symbol_table.symbols)
138  symbol_names.push_back(entry.first);
139 
140  for(const auto &symname : symbol_names)
141  {
142  const symbolt &sym=*symbol_table.lookup(symname);
143  if(should_init_symbol(sym))
144  {
145  if(const symbolt *class_literal_init_method =
146  get_class_literal_initializer(sym, symbol_table))
147  {
148  const std::string &name_str = id2string(sym.name);
149  irep_idt class_name =
150  name_str.substr(0, name_str.size() - strlen(JAVA_CLASS_MODEL_SUFFIX));
151  const symbolt &class_symbol = symbol_table.lookup_ref(class_name);
152 
153  bool class_is_array = is_java_array_tag(sym.name);
154 
155  exprt name_literal(ID_java_string_literal);
156  name_literal.set(ID_value, to_class_type(class_symbol.type).get_tag());
157 
158  symbol_exprt class_name_literal =
160  name_literal, symbol_table, string_refinement_enabled);
161 
162  // Call the literal initializer method instead of a nondet initializer:
163 
164  // For arguments we can't parse yet:
166 
167  // Argument order is: name, isAnnotation, isArray, isInterface,
168  // isSynthetic, isLocalClass, isMemberClass, isEnum
169 
170  code_function_callt initializer_call;
171  initializer_call.function() = class_literal_init_method->symbol_expr();
172 
173  code_function_callt::argumentst &args = initializer_call.arguments();
174 
175  // this:
176  args.push_back(address_of_exprt(sym.symbol_expr()));
177  // name:
178  args.push_back(address_of_exprt(class_name_literal));
179  // isAnnotation:
180  args.push_back(
181  constant_bool(class_symbol.type.get_bool(ID_is_annotation)));
182  // isArray:
183  args.push_back(constant_bool(class_is_array));
184  // isInterface:
185  args.push_back(
186  constant_bool(class_symbol.type.get_bool(ID_interface)));
187  // isSynthetic:
188  args.push_back(
189  constant_bool(class_symbol.type.get_bool(ID_synthetic)));
190  // isLocalClass:
191  args.push_back(nondet_bool);
192  // isMemberClass:
193  args.push_back(nondet_bool);
194  // isEnum:
195  args.push_back(
196  constant_bool(class_symbol.type.get_bool(ID_enumeration)));
197 
198  // First initialize the object as prior to a constructor:
199  namespacet ns(symbol_table);
200 
201  exprt zero_object =
205  to_struct_expr(zero_object), ns, to_symbol_type(sym.type));
206 
207  code_block.copy_to_operands(
208  code_assignt(sym.symbol_expr(), zero_object));
209 
210  // Then call the init function:
211  code_block.move_to_operands(initializer_call);
212  }
213  else if(sym.value.is_nil() && sym.type!=empty_typet())
214  {
215  const bool is_class_model =
216  has_suffix(id2string(sym.name), "@class_model");
217  const bool not_allow_null = is_java_string_literal_id(sym.name) ||
219  assume_init_pointers_not_null;
220 
221  object_factory_parameterst parameters = object_factory_parameters;
222  if(not_allow_null && !is_class_model)
223  parameters.max_nonnull_tree_depth = 1;
224 
226  sym.symbol_expr(),
227  code_block,
228  symbol_table,
229  source_location,
230  false,
232  parameters,
233  pointer_type_selector,
235  }
236  else if(sym.value.is_not_nil())
237  {
238  code_assignt assignment(sym.symbol_expr(), sym.value);
239  assignment.add_source_location()=source_location;
240  code_block.add(assignment);
241  }
242  }
243  }
244 }
245 
251 bool is_java_main(const symbolt &function)
252 {
253  bool named_main = has_suffix(id2string(function.name), JAVA_MAIN_METHOD);
254  const code_typet &function_type = to_code_type(function.type);
255  const typet &string_array_type = java_type_from_string("[Ljava/lang/String;");
256  // checks whether the function is static and has a single String[] parameter
257  bool is_static = !function_type.has_this();
258  // this should be implied by the signature
259  const code_typet::parameterst &parameters = function_type.parameters();
260  bool has_correct_type = function_type.return_type().id() == ID_empty &&
261  parameters.size() == 1 &&
262  parameters[0].type().full_eq(string_array_type);
263  bool public_access = function_type.get(ID_access) == ID_public;
264  return named_main && is_static && has_correct_type && public_access;
265 }
266 
277  const symbolt &function,
278  code_blockt &init_code,
279  symbol_table_baset &symbol_table,
280  bool assume_init_pointers_not_null,
281  object_factory_parameterst object_factory_parameters,
282  const select_pointer_typet &pointer_type_selector)
283 {
284  const code_typet::parameterst &parameters=
285  to_code_type(function.type).parameters();
286 
287  exprt::operandst main_arguments;
288  main_arguments.resize(parameters.size());
289 
290  // certain method arguments cannot be allowed to be null, we set the following
291  // variable to true iff the method under test is the "main" method, which will
292  // be called (by the jvm) with arguments that are never null
293  bool is_main = is_java_main(function);
294 
295  // we iterate through all the parameters of the function under test, allocate
296  // an object for that parameter (recursively allocating other objects
297  // necessary to initialize it), and declare such object as an ID_input
298  for(std::size_t param_number=0;
299  param_number<parameters.size();
300  param_number++)
301  {
302  const code_typet::parametert &p=parameters[param_number];
303  const irep_idt base_name=p.get_base_name().empty()?
304  ("argument#"+std::to_string(param_number)):p.get_base_name();
305 
306  // true iff this parameter is the `this` pointer of the method, which cannot
307  // be null
308  bool is_this=(param_number==0) && parameters[param_number].get_this();
309 
310  object_factory_parameterst parameters = object_factory_parameters;
311  // only pointer must be non-null
312  if(assume_init_pointers_not_null || is_this)
313  parameters.max_nonnull_tree_depth = 1;
314  // in main() also the array elements of the argument must be non-null
315  if(is_main)
316  parameters.max_nonnull_tree_depth = 2;
317 
319 
320  // generate code to allocate and non-deterministicaly initialize the
321  // argument
322  main_arguments[param_number] = object_factory(
323  p.type(),
324  base_name,
325  init_code,
326  symbol_table,
327  parameters,
329  function.location,
330  pointer_type_selector);
331 
332  // record as an input
333  codet input(ID_input);
334  input.operands().resize(2);
335  input.op0()=
337  index_exprt(
338  string_constantt(base_name),
339  from_integer(0, index_type())));
340  input.op1()=main_arguments[param_number];
341  input.add_source_location()=function.location;
342 
343  init_code.move_to_operands(input);
344  }
345 
346  return main_arguments;
347 }
348 
350  const symbolt &function,
351  const exprt::operandst &main_arguments,
352  code_blockt &init_code,
353  symbol_table_baset &symbol_table)
354 {
355  const code_typet::parameterst &parameters=
356  to_code_type(function.type).parameters();
357 
358  exprt::operandst result;
359  result.reserve(parameters.size()+1);
360 
361  bool has_return_value=
362  to_code_type(function.type).return_type()!=empty_typet();
363 
364  if(has_return_value)
365  {
366  // record return value
367  codet output(ID_output);
368  output.operands().resize(2);
369 
370  const symbolt &return_symbol=
371  *symbol_table.lookup(JAVA_ENTRY_POINT_RETURN_SYMBOL);
372 
373  output.op0()=
375  index_exprt(
376  string_constantt(return_symbol.base_name),
377  from_integer(0, index_type())));
378  output.op1()=return_symbol.symbol_expr();
379  output.add_source_location()=function.location;
380 
381  init_code.move_to_operands(output);
382  }
383 
384  for(std::size_t param_number=0;
385  param_number<parameters.size();
386  param_number++)
387  {
388  const symbolt &p_symbol=
389  *symbol_table.lookup(parameters[param_number].get_identifier());
390 
391  if(p_symbol.type.id()==ID_pointer)
392  {
393  // record as an output
394  codet output(ID_output);
395  output.operands().resize(2);
396  output.op0()=
398  index_exprt(
399  string_constantt(p_symbol.base_name),
400  from_integer(0, index_type())));
401  output.op1()=main_arguments[param_number];
402  output.add_source_location()=function.location;
403 
404  init_code.move_to_operands(output);
405  }
406  }
407 
408  // record exceptional return variable as output
409  codet output(ID_output);
410  output.operands().resize(2);
411 
412  // retrieve the exception variable
413  const symbolt exc_symbol=*symbol_table.lookup(
415 
416  output.op0()=address_of_exprt(
418  from_integer(0, index_type())));
419  output.op1()=exc_symbol.symbol_expr();
420  output.add_source_location()=function.location;
421 
422  init_code.move_to_operands(output);
423 }
424 
426  const symbol_table_baset &symbol_table,
427  const irep_idt &main_class,
429 {
430  messaget message(message_handler);
431 
432  // find main symbol
433  if(config.main!="")
434  {
435  // Add java:: prefix
436  std::string main_identifier="java::"+config.main;
437 
438  std::string error_message;
439  irep_idt main_symbol_id=
440  resolve_friendly_method_name(config.main, symbol_table, error_message);
441 
442  if(main_symbol_id==irep_idt())
443  {
444  message.error()
445  << "main symbol resolution failed: " << error_message << messaget::eom;
447  }
448 
449  const symbolt *symbol = symbol_table.lookup(main_symbol_id);
450  INVARIANT(
451  symbol != nullptr,
452  "resolve_friendly_method_name should return a symbol-table identifier");
453 
454  return *symbol; // Return found function
455  }
456  else
457  {
458  // no function given, we look for the main class
459  assert(config.main=="");
460 
461  // are we given a main class?
462  if(main_class.empty())
463  {
464  // no, but we allow this situation to output symbol table,
465  // goto functions, etc
467  }
468 
469  std::string entry_method =
470  "java::" + id2string(main_class) + "." + JAVA_MAIN_METHOD;
471  const symbolt *symbol = symbol_table.lookup(entry_method);
472 
473  // has the class a correct main method?
474  if(!symbol || !is_java_main(*symbol))
475  {
476  // no, but we allow this situation to output symbol table,
477  // goto functions, etc
479  }
480 
481  return *symbol;
482  }
483 }
484 
520  symbol_table_baset &symbol_table,
521  const irep_idt &main_class,
523  bool assume_init_pointers_not_null,
524  bool assert_uncaught_exceptions,
525  const object_factory_parameterst &object_factory_parameters,
526  const select_pointer_typet &pointer_type_selector,
527  bool string_refinement_enabled)
528 {
529  // check if the entry point is already there
530  if(symbol_table.symbols.find(goto_functionst::entry_point())!=
531  symbol_table.symbols.end())
532  return false; // silently ignore
533 
534  messaget message(message_handler);
536  get_main_symbol(symbol_table, main_class, message_handler);
537  if(!res.is_success())
538  return true;
539  symbolt symbol=res.main_function;
540 
541  assert(symbol.type.id()==ID_code);
542 
543  create_initialize(symbol_table);
544 
546  symbol_table,
547  symbol.location,
548  assume_init_pointers_not_null,
549  object_factory_parameters,
550  pointer_type_selector,
551  string_refinement_enabled,
553 
555  symbol,
556  symbol_table,
558  assume_init_pointers_not_null,
559  assert_uncaught_exceptions,
560  object_factory_parameters,
561  pointer_type_selector);
562 }
563 
578  const symbolt &symbol,
579  symbol_table_baset &symbol_table,
581  bool assume_init_pointers_not_null,
582  bool assert_uncaught_exceptions,
583  const object_factory_parameterst &object_factory_parameters,
584  const select_pointer_typet &pointer_type_selector)
585 {
586  messaget message(message_handler);
587  code_blockt init_code;
588 
589  // build call to initialization function
590  {
591  symbol_tablet::symbolst::const_iterator init_it=
592  symbol_table.symbols.find(INITIALIZE_FUNCTION);
593 
594  if(init_it==symbol_table.symbols.end())
595  {
596  message.error() << "failed to find " INITIALIZE_FUNCTION " symbol"
597  << messaget::eom;
598  return true; // give up with error
599  }
600 
601  code_function_callt call_init;
602  call_init.lhs().make_nil();
603  call_init.add_source_location()=symbol.location;
604  call_init.function()=init_it->second.symbol_expr();
605 
606  init_code.move_to_operands(call_init);
607  }
608 
609  // build call to the main method, of the form
610  // return = main_method(arg1, arg2, ..., argn)
611  // where return is a new variable
612  // and arg1 ... argn are constructed below as well
613 
614  code_function_callt call_main;
615 
617  loc.set_function(symbol.name);
618  source_locationt &dloc=loc;
619 
620  // function to call
621  call_main.add_source_location()=dloc;
622  call_main.function()=symbol.symbol_expr();
623  call_main.function().add_source_location()=dloc;
624 
625  // if the method return type is not void, store return value in a new variable
626  // named 'return'
627  if(to_code_type(symbol.type).return_type()!=empty_typet())
628  {
629  auxiliary_symbolt return_symbol;
630  return_symbol.mode=ID_java;
631  return_symbol.is_static_lifetime=false;
632  return_symbol.name=JAVA_ENTRY_POINT_RETURN_SYMBOL;
633  return_symbol.base_name="return";
634  return_symbol.type=to_code_type(symbol.type).return_type();
635 
636  symbol_table.add(return_symbol);
637  call_main.lhs()=return_symbol.symbol_expr();
638  }
639 
640  // add the exceptional return value
641  auxiliary_symbolt exc_symbol;
642  exc_symbol.mode=ID_java;
644  exc_symbol.base_name=exc_symbol.name;
645  exc_symbol.type=java_reference_type(empty_typet());
646  symbol_table.add(exc_symbol);
647 
648  // Zero-initialise the top-level exception catch variable:
649  init_code.copy_to_operands(
650  code_assignt(
651  exc_symbol.symbol_expr(),
652  null_pointer_exprt(to_pointer_type(exc_symbol.type))));
653 
654  // create code that allocates the objects used as test arguments and
655  // non-deterministically initializes them
656  exprt::operandst main_arguments=
658  symbol,
659  init_code,
660  symbol_table,
661  assume_init_pointers_not_null,
662  object_factory_parameters,
663  pointer_type_selector);
664  call_main.arguments()=main_arguments;
665 
666  // Create target labels for the toplevel exception handler:
667  code_labelt toplevel_catch("toplevel_catch", code_skipt());
668  code_labelt after_catch("after_catch", code_skipt());
669 
670  code_blockt call_block;
671 
672  // Push a universal exception handler:
673  // Catch all exceptions:
674  // This is equivalent to catching Throwable, but also works if some of
675  // the class hierarchy is missing so that we can't determine that
676  // the thrown instance is an indirect child of Throwable
677  code_push_catcht push_universal_handler(
678  irep_idt(), toplevel_catch.get_label());
679  irept catch_type_list(ID_exception_list);
680  irept catch_target_list(ID_label);
681 
682  call_block.move_to_operands(push_universal_handler);
683 
684  // we insert the call to the method AFTER the argument initialization code
685  call_block.move_to_operands(call_main);
686 
687  // Pop the handler:
688  code_pop_catcht pop_handler;
689  call_block.move_to_operands(pop_handler);
690  init_code.move_to_operands(call_block);
691 
692  // Normal return: skip the exception handler:
693  init_code.copy_to_operands(code_gotot(after_catch.get_label()));
694 
695  // Exceptional return: catch and assign to exc_symbol.
696  code_landingpadt landingpad(exc_symbol.symbol_expr());
697  init_code.copy_to_operands(toplevel_catch);
698  init_code.move_to_operands(landingpad);
699 
700  // Converge normal and exceptional return:
701  init_code.move_to_operands(after_catch);
702 
703  // declare certain (which?) variables as test outputs
704  java_record_outputs(symbol, main_arguments, init_code, symbol_table);
705 
706  // add uncaught-exception check if requested
707  if(assert_uncaught_exceptions)
708  {
710  init_code, exc_symbol, symbol.location);
711  }
712 
713  // create a symbol for the __CPROVER__start function, associate the code that
714  // we just built and register it in the symbol table
715  symbolt new_symbol;
716 
717  new_symbol.name=goto_functionst::entry_point();
718  new_symbol.type = code_typet({}, empty_typet());
719  new_symbol.value.swap(init_code);
720  new_symbol.mode=ID_java;
721 
722  if(!symbol_table.insert(std::move(new_symbol)).second)
723  {
724  message.error() << "failed to move main symbol" << messaget::eom;
725  return true;
726  }
727 
728  return false;
729 }
#define loc()
#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL
The type of an expression.
Definition: type.h:22
irep_idt name
The unique identifier.
Definition: symbol.h:43
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
Base type of functions.
Definition: std_types.h:764
bool is_nil() const
Definition: irep.h:102
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
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
static void java_static_lifetime_init(symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, object_factory_parameterst object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
exprt & op0()
Definition: expr.h:72
#define CPROVER_PREFIX
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
irep_idt mode
Language mode.
Definition: symbol.h:52
bool is_java_string_literal_id(const irep_idt &id)
Definition: java_utils.cpp:116
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.
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
Definition: std_types.h:987
reference_typet java_reference_type(const typet &subtype)
Definition: java_types.cpp:80
#define JAVA_ENTRY_POINT_RETURN_SYMBOL
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:55
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
Definition: std_code.h:1458
Goto Programs with Functions.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
void move_to_operands(exprt &expr)
Definition: expr.cpp:22
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
Definition: std_types.h:139
The null pointer constant.
Definition: std_expr.h:4520
std::vector< parametert > parameterst
Definition: std_types.h:767
Allocate local stacked objects.
exprt value
Initial value of symbol.
Definition: symbol.h:37
A ‘goto’ instruction.
Definition: std_code.h:774
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 object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector)
Generate a _start function for a specific function.
typet & type()
Definition: expr.h:56
Pops an exception handler from the stack of active handlers (i.e.
Definition: std_code.h:1546
exprt::operandst argumentst
Definition: std_code.h:858
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
Definition: std_types.h:435
Allocate global objects.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
A constant literal expression.
Definition: std_expr.h:4424
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
bool get_bool(const irep_namet &name) const
Definition: irep.cpp:240
bool is_java_array_tag(const irep_idt &tag)
See above.
Definition: java_types.cpp:137
configt config
Definition: config.cpp:23
#define JAVA_MAIN_METHOD
void set_class_identifier(struct_exprt &expr, const namespacet &ns, const symbol_typet &class_type)
If expr has its components filled in then sets the @class_identifier member of the struct...
bool is_static_lifetime
Definition: symbol.h:67
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
Expression Initialization.
const irep_idt & id() const
Definition: irep.h:189
const irep_idt & get_base_name() const
Definition: std_types.h:845
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:428
void add(const codet &code)
Definition: std_code.h:111
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
exprt::operandst java_build_arguments(const symbolt &function, code_blockt &init_code, symbol_table_baset &symbol_table, bool assume_init_pointers_not_null, 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 ...
argumentst & arguments()
Definition: std_code.h:860
A reference into the symbol table.
Definition: std_types.h:110
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:54
std::string main
Definition: config.h:163
#define INITIALIZE_FUNCTION
exprt & op1()
Definition: expr.h:75
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
Definition: symbol.h:135
mstreamt & error() const
Definition: message.h:302
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A label for branch targets.
Definition: std_code.h:947
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
void java_record_outputs(const symbolt &function, const exprt::operandst &main_arguments, code_blockt &init_code, symbol_table_baset &symbol_table)
Base class for tree-like data structures with sharing.
Definition: irep.h:86
A function call.
Definition: std_code.h:828
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:77
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:121
bitvector_typet index_type()
Definition: c_types.cpp:16
Operator to return the address of an object.
Definition: std_expr.h:3170
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
Definition: std_expr.h:1838
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:421
const symbolst & symbols
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
std::vector< exprt > operandst
Definition: expr.h:45
static constant_exprt constant_bool(bool val)
typet type
Type of symbol.
Definition: symbol.h:34
source_locationt location
Source code location of definition of symbol.
Definition: symbol.h:40
static irep_idt entry_point()
exprt object_factory(const typet &type, const irep_idt base_name, code_blockt &init_code, symbol_table_baset &symbol_table, 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...
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
exprt & function()
Definition: std_code.h:848
Base class for all expressions.
Definition: expr.h:42
bool is_state_var
Definition: symbol.h:63
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:905
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:49
The symbol table base class interface.
bool has_this() const
Definition: std_types.h:866
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 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...
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define JAVA_CLASS_MODEL_SUFFIX
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.
virtual std::pair< symbolt &, bool > insert(symbolt symbol)=0
Move or copy a new symbol to the symbol table.
void make_nil()
Definition: irep.h:243
void swap(irept &irep)
Definition: irep.h:231
source_locationt & add_source_location()
Definition: expr.h:130
Sequential composition.
Definition: std_code.h:88
const codet & to_code(const exprt &expr)
Definition: std_code.h:74
const irep_idt & get_label() const
Definition: std_code.h:969
Skip.
Definition: std_code.h:178
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const code_blockt & to_code_block(const codet &code)
Definition: std_code.h:164
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 generic typet to a pointer_typet.
Definition: std_types.h:1450
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
dstringt irep_idt
Definition: irep.h:31
A statement in a programming language.
Definition: std_code.h:21
irep_idt get_tag() const
Definition: std_types.h:266
operandst & operands()
Definition: expr.h:66
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)
bool empty() const
Definition: dstring.h:61
void java_bytecode_instrument_uncaught_exceptions(codet &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...
const typet & return_type() const
Definition: std_types.h:895
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
Definition: namespace.cpp:130
Assignment.
Definition: std_code.h:195
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:214
size_t max_nonnull_tree_depth
To force a certain depth of non-null objects.
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 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__...
A statement that catches an exception, assigning the exception in flight to an expression (e...
Definition: std_code.h:1577
bool is_lvalue
Definition: symbol.h:68
array index operator
Definition: std_expr.h:1462