26 #define JAVA_MAIN_METHOD "main:([Ljava/lang/String;)V" 37 initialize.
mode=ID_java;
51 initialize.
value=init_code;
53 symbol_table.
add(initialize);
58 if(sym.
type.
id()!=ID_code &&
66 return !sym.
type.
get_bool(ID_C_no_initialization_required);
91 "java::java.lang.Class.cproverInitializeClassLiteral:" 92 "(Ljava/lang/String;ZZZZZZZ)V";
122 bool assume_init_pointers_not_null,
125 bool string_refinement_enabled,
136 std::list<irep_idt> symbol_names;
137 for(
const auto &entry : symbol_table.
symbols)
138 symbol_names.push_back(entry.first);
140 for(
const auto &symname : symbol_names)
145 if(
const symbolt *class_literal_init_method =
155 exprt name_literal(ID_java_string_literal);
160 name_literal, symbol_table, string_refinement_enabled);
171 initializer_call.
function() = class_literal_init_method->symbol_expr();
191 args.push_back(nondet_bool);
193 args.push_back(nondet_bool);
215 const bool is_class_model =
219 assume_init_pointers_not_null;
222 if(not_allow_null && !is_class_model)
233 pointer_type_selector,
240 code_block.
add(assignment);
257 bool is_static = !function_type.
has_this();
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;
280 bool assume_init_pointers_not_null,
288 main_arguments.resize(parameters.size());
298 for(std::size_t param_number=0;
299 param_number<parameters.size();
308 bool is_this=(param_number==0) && parameters[param_number].get_this();
312 if(assume_init_pointers_not_null || is_this)
330 pointer_type_selector);
333 codet input(ID_input);
334 input.operands().resize(2);
340 input.op1()=main_arguments[param_number];
341 input.add_source_location()=
function.location;
343 init_code.move_to_operands(input);
346 return main_arguments;
359 result.reserve(parameters.size()+1);
361 bool has_return_value =
367 codet output(ID_output);
384 for(std::size_t param_number=0;
385 param_number<parameters.size();
389 *symbol_table.
lookup(parameters[param_number].get_identifier());
391 if(p_symbol.
type.
id()==ID_pointer)
394 codet output(ID_output);
401 output.
op1()=main_arguments[param_number];
409 codet output(ID_output);
436 std::string main_identifier=
"java::"+
config.
main;
438 std::string error_message;
445 <<
"main symbol resolution failed: " << error_message <<
messaget::eom;
452 "resolve_friendly_method_name should return a symbol-table identifier");
462 if(main_class.
empty())
469 std::string entry_method =
523 bool assume_init_pointers_not_null,
524 bool assert_uncaught_exceptions,
527 bool string_refinement_enabled)
541 assert(symbol.
type.
id()==ID_code);
548 assume_init_pointers_not_null,
549 object_factory_parameters,
550 pointer_type_selector,
551 string_refinement_enabled,
558 assume_init_pointers_not_null,
559 assert_uncaught_exceptions,
560 object_factory_parameters,
561 pointer_type_selector);
581 bool assume_init_pointers_not_null,
582 bool assert_uncaught_exceptions,
591 symbol_tablet::symbolst::const_iterator init_it=
594 if(init_it==symbol_table.
symbols.end())
604 call_init.
function()=init_it->second.symbol_expr();
630 return_symbol.
mode=ID_java;
636 symbol_table.
add(return_symbol);
642 exc_symbol.
mode=ID_java;
646 symbol_table.
add(exc_symbol);
661 assume_init_pointers_not_null,
662 object_factory_parameters,
663 pointer_type_selector);
679 irept catch_type_list(ID_exception_list);
680 irept catch_target_list(ID_label);
707 if(assert_uncaught_exceptions)
710 init_code, exc_symbol, symbol.
location);
720 new_symbol.
mode=ID_java;
722 if(!symbol_table.
insert(std::move(new_symbol)).second)
#define JAVA_ENTRY_POINT_EXCEPTION_SYMBOL
The type of an expression.
irep_idt name
The unique identifier.
irep_idt function_id
Function id, used as a prefix for identifiers of temporaries.
const std::string & id2string(const irep_idt &d)
std::vector< parametert > parameterst
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
typet java_boolean_type()
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)
This module is responsible for the synthesis of code (in the form of a sequence of codet statements) ...
irep_idt mode
Language mode.
bool is_java_string_literal_id(const irep_idt &id)
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)
#define JAVA_ENTRY_POINT_RETURN_SYMBOL
void copy_to_operands(const exprt &expr)
Pushes an exception handler, of the form: exception_tag1 -> label1 exception_tag2 -> label2 ...
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)
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
The null pointer constant.
Allocate local stacked objects.
exprt value
Initial value of symbol.
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.
Pops an exception handler from the stack of active handlers (i.e.
exprt::operandst argumentst
const class_typet & to_class_type(const typet &type)
Cast a generic typet to a class_typet.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
A constant literal expression.
static mstreamt & eom(mstreamt &m)
bool get_bool(const irep_namet &name) const
bool is_java_array_tag(const irep_idt &tag)
See above.
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...
#define INVARIANT(CONDITION, REASON)
Expression Initialization.
const irep_idt & id() const
const irep_idt & get_base_name() const
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...
void add(const codet &code)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
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 ...
A reference into the symbol table.
irep_idt get_java_class_literal_initializer_signature()
Get the symbol name of java.lang.Class' initializer method.
#define INITIALIZE_FUNCTION
const irep_idt & get(const irep_namet &name) const
Internally generated symbol table entryThis is a symbol generated as part of translation to or modifi...
A label for branch targets.
A side effect that returns a non-deterministically chosen value.
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.
bool is_java_main(const symbolt &function)
Checks whether the given symbol is a valid java main method i.e.
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...
bitvector_typet index_type()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Operator to return the address of an object.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
bool is_non_null_library_global(const irep_idt &symbolid)
Check if a symbol is a well-known non-null global.
exprt zero_initializer(const typet &type, const source_locationt &source_location, const namespacet &ns, message_handlert &message_handler)
std::vector< exprt > operandst
static constant_exprt constant_bool(bool val)
typet type
Type of symbol.
source_locationt location
Source code location of definition of symbol.
const java_method_typet & to_java_method_type(const typet &type)
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.
Base class for all expressions.
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
irep_idt base_name
Base (non-scoped) name.
The symbol table base class interface.
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.
source_locationt & add_source_location()
const codet & to_code(const exprt &expr)
const irep_idt & get_label() const
Expression to hold a symbol (variable)
const code_blockt & to_code_block(const codet &code)
bool has_suffix(const std::string &s, const std::string &suffix)
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.
goto_programt coverage_criteriont message_handlert & message_handler
A statement in a programming language.
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.
static bool should_init_symbol(const symbolt &sym)
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
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)
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...