Go to the documentation of this file.
28 #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"
39 initialize.
mode=ID_java;
53 initialize.
value=init_code;
55 symbol_table.
add(initialize);
60 if(sym.
type.
id()!=ID_code &&
68 return !sym.
type.
get_bool(ID_C_no_initialization_required);
93 "java::java.lang.Class.cproverInitializeClassLiteral:"
94 "(Ljava/lang/String;ZZZZZZZ)V";
124 bool assume_init_pointers_not_null,
127 bool string_refinement_enabled,
139 exprt my_literal(ID_java_string_literal);
140 my_literal.
set(ID_value, val);
146 string_refinement_enabled);
153 std::list<irep_idt> symbol_names;
154 for(
const auto &entry : symbol_table.
symbols)
155 symbol_names.push_back(entry.first);
157 for(
const auto &symname : symbol_names)
162 if(
const symbolt *class_literal_init_method =
172 exprt name_literal(ID_java_string_literal);
177 name_literal, symbol_table, string_refinement_enabled);
188 class_literal_init_method->symbol_expr(),
212 if(!zero_object.has_value())
215 message.
error() <<
"failed to zero-initialize " << sym.
name
226 code_block.
add(std::move(initializer_call));
230 const bool is_class_model =
234 assume_init_pointers_not_null;
237 if(not_allow_null && !is_class_model)
248 pointer_type_selector,
255 code_block.
add(assignment);
272 bool is_static = !function_type.
has_this();
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;
295 bool assume_init_pointers_not_null,
303 main_arguments.resize(parameters.size());
313 for(std::size_t param_number=0;
314 param_number<parameters.size();
323 bool is_this=(param_number==0) && parameters[param_number].get_this();
327 if(assume_init_pointers_not_null || is_this)
340 const auto alternatives =
343 if(alternatives.empty())
353 pointer_type_selector);
357 INVARIANT(!is_this,
"We cannot have different types for `this` here");
385 main_arguments[param_number] = result_symbol.
symbol_expr();
387 std::vector<codet> cases(alternatives.size());
399 pointer_type_selector);
400 init_code_for_type.
add(
404 return init_code_for_type;
408 alternatives.begin(),
411 initialize_parameter);
424 codet input(ID_input);
431 input.
op1()=main_arguments[param_number];
434 init_code.
add(std::move(input));
437 return main_arguments;
450 result.reserve(parameters.size()+1);
452 bool has_return_value =
458 codet output(ID_output);
472 init_code.
add(std::move(output));
475 for(std::size_t param_number=0;
476 param_number<parameters.size();
480 *symbol_table.
lookup(parameters[param_number].get_identifier());
482 if(p_symbol.
type.
id()==ID_pointer)
485 codet output(ID_output);
492 output.
op1()=main_arguments[param_number];
495 init_code.
add(std::move(output));
500 codet output(ID_output);
513 init_code.
add(std::move(output));
527 std::string main_identifier=
"java::"+
config.
main;
529 std::string error_message;
536 <<
"main symbol resolution failed: " << error_message <<
messaget::eom;
543 "resolve_friendly_method_name should return a symbol-table identifier");
553 if(main_class.
empty())
560 std::string entry_method =
614 bool assume_init_pointers_not_null,
615 bool assert_uncaught_exceptions,
618 bool string_refinement_enabled)
632 assert(symbol.
type.
id()==ID_code);
639 assume_init_pointers_not_null,
640 object_factory_parameters,
641 pointer_type_selector,
642 string_refinement_enabled,
649 assume_init_pointers_not_null,
650 assert_uncaught_exceptions,
651 object_factory_parameters,
652 pointer_type_selector);
670 bool assume_init_pointers_not_null,
671 bool assert_uncaught_exceptions,
680 symbol_tablet::symbolst::const_iterator init_it=
683 if(init_it==symbol_table.
symbols.end())
693 init_code.
add(std::move(call_init));
708 call_main.function().add_source_location()=dloc;
715 return_symbol.
mode=ID_java;
721 symbol_table.
add(return_symbol);
727 exc_symbol.
mode=ID_java;
731 symbol_table.
add(exc_symbol);
745 assume_init_pointers_not_null,
746 object_factory_parameters,
747 pointer_type_selector);
748 call_main.arguments()=main_arguments;
763 irept catch_type_list(ID_exception_list);
764 irept catch_target_list(ID_label);
766 call_block.
add(std::move(push_universal_handler));
769 call_block.
add(std::move(call_main));
773 call_block.
add(std::move(pop_handler));
774 init_code.
add(std::move(call_block));
781 init_code.
add(std::move(toplevel_catch));
782 init_code.
add(std::move(landingpad));
785 init_code.
add(std::move(after_catch));
791 if(assert_uncaught_exceptions)
794 init_code, exc_symbol, symbol.
location);
804 new_symbol.
mode=ID_java;
806 if(!symbol_table.
insert(std::move(new_symbol)).second)
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A codet representing sequential composition of program statements.
#define JAVA_CLASS_MODEL_SUFFIX
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'.
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
virtual symbolt * get_writeable(const irep_idt &name)=0
Find a symbol in the symbol table for read-write access.
reference_typet java_reference_type(const typet &subtype)
#define JAVA_ENTRY_POINT_RETURN_SYMBOL
bool is_java_string_literal_id(const irep_idt &id)
The type of an expression, extends irept.
typet java_boolean_type()
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.
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
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.
typet type
Type of symbol.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
std::vector< parametert > parameterst
Allocate local stacked objects.
std::list< std::string > string_input_values
Force one of finitely many explicitly given input strings.
Base class for all expressions.
bool is_java_array_tag(const irep_idt &tag)
See above.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
irep_idt base_name
Base (non-scoped) name.
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
A struct tag type, i.e., struct_typet with an identifier.
virtual std::set< struct_tag_typet > get_parameter_alternative_types(const irep_idt &function_name, const irep_idt ¶meter_name, const namespacet &ns) const
Get alternative types for a method parameter, e.g., based on the casts in the function body.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Internally generated symbol table entry.
Expression to hold a symbol (variable)
Pops an exception handler from the stack of active handlers (i.e.
bool has_suffix(const std::string &s, const std::string &suffix)
bitvector_typet index_type()
optionalt< exprt > zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns)
Create the equivalent of zero for type type.
const codet & to_code(const exprt &expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
bool get_bool(const irep_namet &name) const
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.
irep_idt mode
Language mode.
const irep_idt & get_base_name() const
irep_idt get_java_class_literal_initializer_signature()
Get the symbol name of java.lang.Class' initializer method.
The null pointer constant.
const std::string & id2string(const irep_idt &d)
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)
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.
codet representation of a goto statement.
codet representation of a label for branch targets.
The symbol table base class interface.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
void java_record_outputs(const symbolt &function, const exprt::operandst &main_arguments, code_blockt &init_code, symbol_table_baset &symbol_table)
#define INITIALIZE_FUNCTION
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...
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
bool is_java_main(const symbolt &function)
Checks whether the given symbol is a valid java main method i.e.
static void create_initialize(symbol_table_baset &symbol_table)
const irep_idt & id() const
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
std::vector< exprt > operandst
void add(const codet &code)
const parameterst & parameters() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
bool remove(const irep_idt &name)
Remove a symbol from the symbol table.
static constant_exprt constant_bool(bool val)
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...
size_t min_null_tree_depth
To force a certain depth of non-null objects.
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_label() const
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
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...
exprt value
Initial value of symbol.
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__...
A codet representing a skip statement.
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.
A statement that catches an exception, assigning the exception in flight to an expression (e....
const irep_idt & get(const irep_namet &name) const
source_locationt location
Source code location of definition of symbol.
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 ...
codet representing a switch statement.
void set(const irep_namet &name, const irep_idt &value)
const irep_idt & get_identifier() const
static bool should_init_symbol(const symbolt &sym)
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...
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
const typet & return_type() const
const code_blockt & to_code_block(const codet &code)
Base class for tree-like data structures with sharing.
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 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...
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
Operator to return the address of an object.
source_locationt & add_source_location()
const java_method_typet & to_java_method_type(const typet &type)
Semantic type conversion.
A codet representing an assignment in the program.
A constant literal expression.
Allocate dynamic objects (using MALLOC)
#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL
irep_idt name
The unique identifier.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
Data structure for representing an arbitrary statement in a program.