33 #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"
41 const std::vector<exprt> &arguments,
58 symbol_table.
add(initialize);
63 if(sym.
type.
id()!=ID_code &&
71 return !sym.
type.
get_bool(ID_C_no_initialization_required);
80 "java::java.lang.Class.cproverInitializeClassLiteral:"
81 "(Ljava/lang/String;ZZZZZZZ)V";
113 bool assume_init_pointers_not_null,
116 bool string_refinement_enabled,
119 std::unordered_set<irep_idt> additional_symbols;
122 const symbolt *class_literal_init_method =
138 string_refinement_enabled);
154 class_literal_init_method->symbol_expr(),
156 address_of_exprt(sym.symbol_expr()),
158 address_of_exprt(class_name_literal),
160 constant_bool(java_class_type.get_is_annotation()),
162 constant_bool(class_is_array),
164 constant_bool(java_class_type.get_interface()),
166 constant_bool(java_class_type.get_synthetic()),
172 constant_bool(java_class_type.get_is_enumeration())});
178 if(!zero_object.has_value())
181 message.
error() <<
"failed to zero-initialize " << sym.
name
192 code_block.
add(std::move(initializer_call));
199 assume_init_pointers_not_null;
202 if(not_allow_null && !is_class_model)
213 pointer_type_selector,
221 code_block.
add(assignment);
224 return additional_symbols;
230 bool assume_init_pointers_not_null,
233 bool string_refinement_enabled,
256 val, symbol_table, string_refinement_enabled);
264 std::set<std::string> symbol_names;
265 for(
const auto &entry : symbol_table.
symbols)
266 symbol_names.insert(
id2string(entry.first));
268 std::set<std::string> additional_symbols;
269 while(!symbol_names.empty() || !additional_symbols.empty())
271 if(!additional_symbols.empty())
272 symbol_names.swap(additional_symbols);
274 for(
const auto &symbol_name : symbol_names)
284 assume_init_pointers_not_null,
285 object_factory_parameters,
286 pointer_type_selector,
287 string_refinement_enabled,
289 for(
const auto &new_symbol_name : new_symbols)
290 additional_symbols.insert(
id2string(new_symbol_name));
294 symbol_names.clear();
297 initialize_symbol.
value = std::move(code_block);
311 bool is_static = !function_type.
has_this();
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;
324 bool assume_init_pointers_not_null,
334 main_arguments.resize(parameters.size());
344 for(std::size_t param_number=0;
345 param_number<parameters.size();
354 bool is_this=(param_number==0) && parameters[param_number].get_this();
365 main_arguments[param_number] = result;
374 object_factory_parameters;
376 if(assume_init_pointers_not_null || is_this)
389 const auto alternatives =
392 if(alternatives.empty())
402 pointer_type_selector,
407 INVARIANT(!is_this,
"We cannot have different types for `this` here");
435 std::vector<codet> cases;
436 cases.reserve(alternatives.size());
437 for(
const auto &type : alternatives)
449 pointer_type_selector,
454 cases.push_back(init_code_for_type);
469 code_inputt{base_name, main_arguments[param_number],
function.location});
472 return make_pair(init_code, main_arguments);
485 init_code.
add(std::move(*return_value));
512 const std::vector<exprt> &arguments,
520 for(std::size_t param_number = 0; param_number < parameters.size();
524 symbol_table.
lookup_ref(parameters[param_number].get_identifier());
530 p_symbol.
base_name, arguments[param_number],
function.location});
558 std::string error_message;
560 config.
main.value(), symbol_table, error_message);
562 if(main_symbol_id.
empty())
565 <<
"main symbol resolution failed: " << error_message <<
messaget::eom;
572 "resolve_friendly_method_name should return a symbol-table identifier");
579 if(main_class.
empty())
586 std::string entry_method =
606 bool assume_init_pointers_not_null,
607 bool assert_uncaught_exceptions,
610 bool string_refinement_enabled,
631 assert_uncaught_exceptions,
632 object_factory_parameters,
633 pointer_type_selector,
641 bool assert_uncaught_exceptions,
651 symbol_table_baset::symbolst::const_iterator init_it =
654 if(init_it==symbol_table.
symbols.end())
664 init_code.
add(std::move(call_init));
686 return_symbol.
mode=ID_java;
692 symbol_table.
add(return_symbol);
698 exc_symbol.
mode=ID_java;
702 symbol_table.
add(exc_symbol);
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;
729 irept catch_type_list(ID_exception_list);
730 irept catch_target_list(ID_label);
732 call_block.
add(std::move(push_universal_handler));
735 call_block.
add(std::move(call_main));
739 call_block.
add(std::move(pop_handler));
740 init_code.
add(std::move(call_block));
747 init_code.
add(std::move(toplevel_catch));
748 init_code.
add(std::move(landingpad));
751 init_code.
add(std::move(after_catch));
758 if(assert_uncaught_exceptions)
761 init_code, exc_symbol, symbol.
location);
771 new_symbol.value.swap(init_code);
773 if(!symbol_table.
insert(std::move(new_symbol)).second)
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
@ DYNAMIC
Allocate dynamic objects (using ALLOCATE)
@ STATIC_GLOBAL
Allocate global objects with static lifetime.
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...
A codet representing sequential composition of program statements.
void append(const code_blockt &extra_block)
Add all the codets from extra_block to the current code_blockt.
void add(const codet &code)
A goto_instruction_codet representing the declaration of a local variable.
A codet representing an assignment in the program.
goto_instruction_codet representation of a function call statement.
codet representation of a goto statement.
codet representation of a label for branch targets.
const irep_idt & get_label() const
A statement that catches an exception, assigning the exception in flight to an expression (e....
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.
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ....
A codet representing a skip statement.
const irep_idt & get_base_name() const
const irep_idt & get_identifier() const
const typet & return_type() const
bool get_is_constructor() const
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
std::optional< std::string > main
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
source_locationt & add_source_location()
typet & type()
Return the type of the expression.
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.
bool get_bool(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
const irep_idt & id() const
std::vector< parametert > parameterst
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'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The null pointer constant.
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.
A side_effect_exprt that returns a non-deterministically chosen value.
An expression containing a side effect.
void set_function(const irep_idt &function)
A struct tag type, i.e., struct_typet with an identifier.
Expression to hold a symbol (variable)
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.
irep_idt base_name
Base (non-scoped) name.
source_locationt location
Source code location of definition of symbol.
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
exprt value
Initial value of symbol.
irep_idt mode
Language mode.
Semantic type conversion.
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)
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)
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()
empty_typet java_void_type()
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.
reference_typet java_reference_type(const typet &subtype)
c_bool_typet java_boolean_type()
bool is_java_array_tag(const irep_idt &tag)
See above.
const java_class_typet & to_java_class_type(const typet &type)
const java_method_typet & to_java_method_type(const typet &type)
bool is_java_string_literal_id(const irep_idt &id)
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
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)
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...
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'.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define INITIALIZE_FUNCTION
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const class_typet & to_class_type(const typet &type)
Cast a typet to a class_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
size_t strlen(const char *s)
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)