Go to the documentation of this file.
14 #ifndef CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
15 #define CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
27 #include <unordered_set>
33 #define MAX_FORMAT_ARGS 10
101 typedef std::function<
codet(
108 typedef std::unordered_map<irep_idt, irep_idt>
id_mapt;
134 const std::array<id_mapt *, 5>
id_maps = std::array<id_mapt *, 5>
218 const exprt &array_pointer,
266 const exprt &rhs_array,
267 const exprt &rhs_length,
285 const std::string &s,
347 const exprt &pointer,
361 const exprt &pointer,
368 #endif // CPROVER_JAVA_BYTECODE_JAVA_STRING_LIBRARY_PREPROCESS_H
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.
code_blockt make_copy_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for a function which copies a string object to a new string object.
code_returnt make_string_length_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for the String.length method.
std::unordered_map< irep_idt, irep_idt > id_mapt
id_mapt cprover_equivalent_to_java_assign_and_return_function
A codet representing sequential composition of program statements.
java_string_library_preprocesst()
symbol_exprt fresh_array(const typet &type, const source_locationt &loc, symbol_tablet &symbol_table)
add a symbol in the table with static lifetime and name containing cprover_string_array and given typ...
The type of an expression, extends irept.
exprt make_nondet_infinite_char_array(symbol_table_baset &symbol_table, const source_locationt &loc, const irep_idt &function_id, code_blockt &code)
Declare a fresh symbol of type array of character with infinite size.
friend refined_string_exprt convert_exprt_to_string_exprt_unit_test(java_string_library_preprocesst &preprocess, const exprt &deref, const source_locationt &loc, symbol_tablet &symbol_table, code_blockt &init_code)
std::vector< parametert > parameterst
Operator to dereference a pointer.
void add_pointer_to_array_association(const exprt &pointer, const exprt &array, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that pointer points to the first char...
id_mapt cprover_equivalent_to_java_function
id_mapt cprover_equivalent_to_java_string_returning_function
code_blockt make_function_from_call(const irep_idt &function_name, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Provide code for a function that calls a function from the solver and simply returns it.
code_blockt make_string_returning_function_from_call(const irep_idt &function_name, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Provide code for a function that calls a function from the solver and return the string_expr result a...
id_mapt cprover_equivalent_to_java_constructor
Base class for all expressions.
bool implements_function(const irep_idt &function_id) const
code_blockt make_assign_and_return_function_from_call(const irep_idt &function_name, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Call a cprover internal function, assign the result to object this and return it.
void initialize_known_type_table()
static bool is_java_char_sequence_pointer_type(const typet &type)
Expression to hold a symbol (variable)
void code_assign_java_string_to_string_expr(const refined_string_exprt &lhs, const exprt &rhs, const source_locationt &loc, const symbol_table_baset &symbol_table, code_blockt &code)
static bool is_java_string_builder_type(const typet &type)
struct_exprt make_argument_for_format(const exprt &argv, std::size_t index, const struct_typet &structured_type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
Helper for format function.
std::vector< irep_idt > get_string_type_base_classes(const irep_idt &class_name)
Gets the base classes for known String and String-related types, or returns an empty list for other t...
refined_string_exprt string_literal_to_string_expr(const std::string &s, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Create a string expression whose value is given by a literal.
Struct constructor from list of elements.
void add_string_type(const irep_idt &class_name, symbol_tablet &symbol_table)
Add to the symbol table type declaration for a String-like Java class.
code_blockt make_object_get_class_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Used to provide our own implementation of the java.lang.Object.getClass() function.
codet representation of a function call statement.
exprt::operandst process_parameters(const java_method_typet::parameterst ¶ms, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
calls string_refine_preprocesst::process_operands with a list of parameters.
std::function< codet(const java_method_typet &, const source_locationt &, const irep_idt &, symbol_table_baset &)> conversion_functiont
exprt::operandst process_equals_function_operands(const exprt::operandst &operands, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
Converts the operands of the equals function to string expressions and outputs these conversions.
std::unordered_map< irep_idt, conversion_functiont > conversion_table
refined_string_exprt convert_exprt_to_string_exprt(const exprt &deref, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
Creates a string_exprt from the input exprt representing a char sequence.
refined_string_exprt decl_string_expr(const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Add declaration of a refined string expr whose content and length are fresh symbols.
code_blockt make_copy_constructor_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Generates code for a constructor of a string object from another string object.
refined_string_exprt string_expr_of_function(const irep_idt &function_name, const exprt::operandst &arguments, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Create a refined_string_exprt str whose content and length are fresh symbols, calls the string primit...
The symbol table base class interface.
void get_all_function_names(std::unordered_set< irep_idt > &methods) const
static bool is_java_char_array_type(const typet &type)
codet replace_character_call(code_function_callt call)
refined_string_exprt make_nondet_string_expr(const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
add symbols with prefix cprover_string_length and cprover_string_data and construct a string_expr fro...
codet code_for_function(const symbolt &symbol, symbol_table_baset &symbol_table)
Should be called to provide code for string functions that are used in the code but for which no impl...
optionalt< symbol_exprt > get_primitive_value_of_object(const exprt &object, irep_idt type_name, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
Adds to the code an assignment of the form.
pointer_typet pointer_type(const typet &subtype)
id_mapt cprover_equivalent_to_java_assign_function
static bool implements_java_char_sequence(const typet &type)
static bool is_java_char_sequence_type(const typet &type)
exprt::operandst process_operands(const exprt::operandst &operands, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &init_code)
for each expression that is of a type implementing strings, we declare a new cprover_string whose con...
std::vector< exprt > operandst
codet code_return_function_application(const irep_idt &function_name, const exprt::operandst &arguments, const typet &type, symbol_table_baset &symbol_table)
return the result of a function call
symbol_exprt fresh_string(const typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
add a symbol with static lifetime and name containing cprover_string and given type
code_blockt make_init_function_from_call(const irep_idt &function_name, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table, bool is_constructor=true)
Generate the goto code for string initialization.
nonstd::optional< T > optionalt
static bool java_type_matches_tag(const typet &type, const std::string &tag)
character_refine_preprocesst character_preprocess
code_blockt make_string_format_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Used to provide code for the Java String.format function.
static bool is_java_char_array_pointer_type(const typet &type)
code_blockt make_float_to_string_code(const java_method_typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table)
Provide code for the String.valueOf(F) function.
static bool is_java_string_buffer_type(const typet &type)
Structure type, corresponds to C style structs.
codet representation of a "return from a function" statement.
void add_array_to_length_association(const exprt &array, const exprt &length, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver, letting it know that the actual length of array is le...
const refined_string_typet refined_string_type
codet code_assign_components_to_java_string(const exprt &lhs, const exprt &rhs_array, const exprt &rhs_length, const symbol_table_baset &symbol_table, bool is_constructor)
Produce code for an assignment of a string expr to a Java string.
static bool is_java_string_buffer_pointer_type(const typet &type)
const std::array< id_mapt *, 5 > id_maps
static bool implements_java_char_sequence_pointer(const typet &type)
void add_character_set_constraint(const exprt &pointer, const exprt &length, const irep_idt &char_set, symbol_table_baset &symbol_table, const source_locationt &loc, code_blockt &code)
Add a call to a primitive of the string solver which ensures all characters belong to the character s...
bool is_known_string_type(irep_idt class_name)
Check whether a class name is known as a string type.
exprt allocate_fresh_string(const typet &type, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, code_blockt &code)
declare a new String and allocate it
void initialize_conversion_table()
fill maps with correspondence from java method names to conversion functions
dereference_exprt get_object_at_index(const exprt &argv, std::size_t index)
Helper for format function.
code_blockt make_assign_function_from_call(const irep_idt &function_name, const java_method_typet &type, const source_locationt &loc, symbol_table_baset &symbol_table)
Call a cprover internal function and assign the result to object this.
static bool is_constructor(const irep_idt &method_name)
static bool is_java_string_pointer_type(const typet &type)
codet code_assign_string_expr_to_java_string(const exprt &lhs, const refined_string_exprt &rhs, const symbol_table_baset &symbol_table, bool is_constructor)
Produce code for an assignemnt of a string expr to a Java string.
codet replace_character_call(const code_function_callt &call) const
replace function calls to functions of the Character by an affectation if possible,...
std::unordered_set< irep_idt > string_types
static bool is_java_string_type(const typet &type)
static bool is_java_string_builder_pointer_type(const typet &type)
refined_string_exprt replace_char_array(const exprt &array_pointer, const source_locationt &loc, symbol_table_baset &symbol_table, code_blockt &code)
we declare a new cprover_string whose contents is deduced from the char array.
Data structure for representing an arbitrary statement in a program.