32 #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V"
40 const std::vector<exprt> &arguments,
56 initialize.
mode=ID_java;
59 symbol_table.
add(initialize);
64 if(sym.
type.
id()!=ID_code &&
72 return !sym.
type.
get_bool(ID_C_no_initialization_required);
81 "java::java.lang.Class.cproverInitializeClassLiteral:"
82 "(Ljava/lang/String;ZZZZZZZ)V";
112 bool assume_init_pointers_not_null,
115 bool string_refinement_enabled,
138 val, symbol_table, string_refinement_enabled);
145 std::list<irep_idt> symbol_names;
146 for(
const auto &entry : symbol_table.
symbols)
147 symbol_names.push_back(entry.first);
152 auto symbol_it = symbol_names.begin();
153 symbol_it != symbol_names.end();
156 const auto &symname = *symbol_it;
160 if(
const symbolt *class_literal_init_method =
176 string_refinement_enabled);
179 const auto &new_symbols = journalling_table.
get_inserted();
181 symbol_names.end(), new_symbols.begin(), new_symbols.end());
194 class_literal_init_method->symbol_expr(),
196 address_of_exprt(sym.symbol_expr()),
198 address_of_exprt(class_name_literal),
200 constant_bool(java_class_type.get_is_annotation()),
202 constant_bool(class_is_array),
204 constant_bool(java_class_type.get_interface()),
206 constant_bool(java_class_type.get_synthetic()),
212 constant_bool(java_class_type.get_is_enumeration())});
218 if(!zero_object.has_value())
221 message.
error() <<
"failed to zero-initialize " << sym.
name
232 code_block.
add(std::move(initializer_call));
236 const bool is_class_model =
240 assume_init_pointers_not_null;
243 if(not_allow_null && !is_class_model)
254 pointer_type_selector,
262 code_block.
add(assignment);
266 initialize_symbol.
value = std::move(code_block);
280 bool is_static = !function_type.
has_this();
283 bool has_correct_type = function_type.
return_type().
id() == ID_empty &&
284 parameters.
size() == 1 &&
285 parameters[0].type().full_eq(*string_array_type);
286 bool public_access = function_type.
get(ID_access) == ID_public;
287 return named_main && is_static && has_correct_type && public_access;
293 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();
334 main_arguments[param_number] = result;
343 object_factory_parameters;
345 if(assume_init_pointers_not_null || is_this)
358 const auto alternatives =
361 if(alternatives.empty())
371 pointer_type_selector,
376 INVARIANT(!is_this,
"We cannot have different types for `this` here");
404 std::vector<codet> cases;
405 cases.reserve(alternatives.size());
406 for(
const auto &type : alternatives)
418 pointer_type_selector,
420 init_code_for_type.
add(
424 cases.push_back(init_code_for_type);
439 code_inputt{base_name, main_arguments[param_number],
function.location});
442 return make_pair(init_code, main_arguments);
455 init_code.
add(std::move(*return_value));
482 const std::vector<exprt> &arguments,
490 for(std::size_t param_number = 0; param_number < parameters.size();
494 symbol_table.
lookup_ref(parameters[param_number].get_identifier());
500 p_symbol.
base_name, arguments[param_number],
function.location});
528 std::string error_message;
530 config.
main.value(), symbol_table, error_message);
532 if(main_symbol_id.
empty())
535 <<
"main symbol resolution failed: " << error_message <<
messaget::eom;
542 "resolve_friendly_method_name should return a symbol-table identifier");
549 if(main_class.
empty())
556 std::string entry_method =
576 bool assume_init_pointers_not_null,
577 bool assert_uncaught_exceptions,
580 bool string_refinement_enabled,
595 assert(symbol.
type.
id()==ID_code);
601 assert_uncaught_exceptions,
602 object_factory_parameters,
603 pointer_type_selector,
611 bool assert_uncaught_exceptions,
621 symbol_tablet::symbolst::const_iterator init_it=
624 if(init_it==symbol_table.
symbols.end())
634 init_code.
add(std::move(call_init));
656 return_symbol.
mode=ID_java;
662 symbol_table.
add(return_symbol);
668 exc_symbol.
mode=ID_java;
672 symbol_table.
add(exc_symbol);
681 const std::pair<code_blockt, std::vector<exprt>> main_arguments =
682 build_arguments(symbol, symbol_table);
683 init_code.
append(main_arguments.first);
684 call_main.
arguments() = main_arguments.second;
699 irept catch_type_list(ID_exception_list);
700 irept catch_target_list(ID_label);
702 call_block.
add(std::move(push_universal_handler));
705 call_block.
add(std::move(call_main));
709 call_block.
add(std::move(pop_handler));
710 init_code.
add(std::move(call_block));
717 init_code.
add(std::move(toplevel_catch));
718 init_code.
add(std::move(landingpad));
721 init_code.
add(std::move(after_catch));
728 if(assert_uncaught_exceptions)
731 init_code, exc_symbol, symbol.
location);
741 new_symbol.
mode=ID_java;
743 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_tablet &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 an assignment in the program.
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 codet representing the declaration of a local variable.
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 codet representing the declaration that an output of a particular description has a value which cor...
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.
optionalt< 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_namet &name) const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) 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.
optionalt< 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 optionalt< codet > record_return_value(const symbolt &function, const symbol_table_baset &symbol_table)
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 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()
optionalt< 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'.
nonstd::optional< T > optionalt
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 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.
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)