Skip to content

Cleanup in string preprocessing #2374

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Oct 18, 2018
Merged

Cleanup in string preprocessing #2374

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
6d86626
Update jbmc/lib/java-models-library to java-models-library#9 (String …
romainbrenguier Aug 9, 2018
bd292f7
Stop preprocessing for unsupported functions
romainbrenguier Jun 20, 2018
f6c3023
Remove unused functions
romainbrenguier Jun 20, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion jbmc/lib/java-models-library
Open in desktop
Submodule java-models-library updated 3 files
+23 −2 src/main/java/java/lang/String.java
+8 −6 src/main/java/java/lang/StringBuilder.java
+22 −0 src/main/java/org/cprover/CProverString.java
97 changes: 0 additions & 97 deletions jbmc/src/java_bytecode/java_string_library_preprocess.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -168,18 +168,6 @@ bool java_string_library_preprocesst::is_java_char_array_pointer_type(
return false;
}

/// \param symbol_table: a symbol_table containing an entry for java Strings
/// \return the type of data fields in java Strings.
typet string_data_type(const symbol_tablet &symbol_table)
{
symbolt sym=*symbol_table.lookup("java::java.lang.String");
typet concrete_type=sym.type;
struct_typet struct_type=to_struct_type(concrete_type);
std::size_t index=struct_type.component_number("data");
typet data_type=struct_type.components()[index].type();
return data_type;
}

/// \return the type of the length field in java Strings.
typet string_length_type()
{
Expand Down Expand Up @@ -589,26 +577,6 @@ exprt java_string_library_preprocesst::allocate_fresh_string(
return str;
}

/// declare a new character array and allocate it
/// \param type: a type for string
/// \param loc: a location in the program
/// \param symbol_table: symbol table
/// \param code: code block to which allocation instruction will be added
/// \return a new array
exprt java_string_library_preprocesst::allocate_fresh_array(
const typet &type,
const source_locationt &loc,
const irep_idt &function_id,
symbol_tablet &symbol_table,
code_blockt &code)
{
exprt array=fresh_array(type, loc, symbol_table);
code.add(code_declt(array), loc);
allocate_dynamic_object_with_decl(
array, symbol_table, loc, function_id, code);
return array;
}

/// assign the result of a function call
/// \param lhs: an expression
/// \param function_name: the name of the function
Expand Down Expand Up @@ -1719,55 +1687,6 @@ codet java_string_library_preprocesst::make_copy_constructor_code(
return code;
}

/// Used to provide code for constructor from a char array.
/// The implementation is similar to substring except the 3rd argument is a
/// count instead of end index
/// \param type: type of the function call
/// \param loc: location in the program_invocation_name
/// \param function_id: unused
/// \param symbol_table: symbol table
/// \return code implementing String intitialization from a char array and
/// arguments offset and end.
codet java_string_library_preprocesst::make_init_from_array_code(
const java_method_typet &type,
const source_locationt &loc,
const irep_idt &function_id,
symbol_table_baset &symbol_table)
{
(void)function_id;

// Code for the output
code_blockt code;

java_method_typet::parameterst params = type.parameters();
PRECONDITION(params.size() == 4);
exprt::operandst args =
process_parameters(type.parameters(), loc, symbol_table, code);
INVARIANT(
args.size() == 4, "process_parameters preserves number of arguments");

/// \todo this assumes the array to be constant between all calls to
/// string primitives, which may not be true in general.
refined_string_exprt string_arg = to_string_expr(args[1]);

// The third argument is `count`, whereas the third argument of substring
// is `end` which corresponds to `offset+count`
refined_string_exprt string_expr = string_expr_of_function(
ID_cprover_string_substring_func,
{args[1], args[2], plus_exprt(args[2], args[3])},
loc,
symbol_table,
code);

// Assign string_expr to `this` object
symbol_exprt arg_this(params[0].get_identifier(), params[0].type());
code.add(
code_assign_string_expr_to_java_string(arg_this, string_expr, symbol_table),
loc);

return code;
}

/// Generates code for the String.length method
/// \param type: type of the function
/// \param loc: location in the source
Expand Down Expand Up @@ -1922,13 +1841,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
std::placeholders::_2,
std::placeholders::_3,
std::placeholders::_4);
conversion_table["java::java.lang.String.<init>:([CII)V"] = std::bind(
&java_string_library_preprocesst::make_init_from_array_code,
this,
std::placeholders::_1,
std::placeholders::_2,
std::placeholders::_3,
std::placeholders::_4);
cprover_equivalent_to_java_constructor
["java::java.lang.String.<init>:()V"]=
ID_cprover_string_empty_string_func;
Expand Down Expand Up @@ -1956,12 +1868,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
cprover_equivalent_to_java_function
["java::java.lang.String.contains:(Ljava/lang/CharSequence;)Z"]=
ID_cprover_string_contains_func;
cprover_equivalent_to_java_string_returning_function
["java::java.lang.String.copyValueOf:([CII)Ljava/lang/String;"]=
ID_cprover_string_copy_func;
cprover_equivalent_to_java_string_returning_function
["java::java.lang.String.copyValueOf:([C)Ljava/lang/String;"]=
ID_cprover_string_copy_func;
cprover_equivalent_to_java_function
["java::java.lang.String.endsWith:(Ljava/lang/String;)Z"]=
ID_cprover_string_endswith_func;
Expand Down Expand Up @@ -2108,9 +2014,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
cprover_equivalent_to_java_assign_and_return_function
["java::java.lang.StringBuilder.append:(C)Ljava/lang/StringBuilder;"]=
ID_cprover_string_concat_char_func;
cprover_equivalent_to_java_assign_and_return_function
["java::java.lang.StringBuilder.append:([C)Ljava/lang/StringBuilder;"] =
ID_cprover_string_concat_func;
cprover_equivalent_to_java_assign_and_return_function
["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] =
ID_cprover_string_concat_double_func;
Expand Down
20 changes: 0 additions & 20 deletions jbmc/src/java_bytecode/java_string_library_preprocess.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -43,7 +43,6 @@ class java_string_library_preprocesst:public messaget

void initialize_known_type_table();
void initialize_conversion_table();
void initialize_refined_string_type();

bool implements_function(const irep_idt &function_id) const;
void get_all_function_names(std::unordered_set<irep_idt> &methods) const;
Expand Down Expand Up @@ -151,12 +150,6 @@ class java_string_library_preprocesst:public messaget
const irep_idt &function_id,
symbol_table_baset &symbol_table);

codet make_string_to_char_array_code(
const java_method_typet &type,
const source_locationt &loc,
const irep_idt &function_id,
symbol_tablet &symbol_table);

codet make_string_format_code(
const java_method_typet &type,
const source_locationt &loc,
Expand Down Expand Up @@ -254,13 +247,6 @@ class java_string_library_preprocesst:public messaget
symbol_table_baset &symbol_table,
code_blockt &code);

exprt allocate_fresh_array(
const typet &type,
const source_locationt &loc,
const irep_idt &function_id,
symbol_tablet &symbol_table,
code_blockt &code);

codet code_return_function_application(
const irep_idt &function_name,
const exprt::operandst &arguments,
Expand Down Expand Up @@ -346,12 +332,6 @@ class java_string_library_preprocesst:public messaget
code_blockt &code);

exprt get_object_at_index(const exprt &argv, std::size_t index);

codet make_init_from_array_code(
const java_method_typet &type,
const source_locationt &loc,
const irep_idt &function_id,
symbol_table_baset &symbol_table);
};

exprt make_nondet_infinite_char_array(
Expand Down