Skip to content

Commit 8f6431c

Browse files
author
Joel Allred
committed
Introduce more string primitives in JBMC
We replace some java signatures with CProver primitives. This concerns those String, StringBuilder and StringBuffer methods that throw exceptions. We do that to be able to wrap some functionality around the string methods in the library of models, e.g. throwing out of bounds exceptions.
1 parent daab304 commit 8f6431c

File tree

1 file changed

+52
-49
lines changed

1 file changed

+52
-49
lines changed

‎src/java_bytecode/java_string_library_preprocess.cpp

+52-49
Original file line numberDiff line numberDiff line change
@@ -1921,13 +1921,13 @@ void java_string_library_preprocesst::initialize_conversion_table()
19211921
["java::org.cprover.CProverString.charAt:(Ljava/lang/String;I)C"]=
19221922
ID_cprover_string_char_at_func;
19231923
cprover_equivalent_to_java_function
1924-
["java::java.lang.String.codePointAt:(I)I"]=
1924+
["java::org.cprover.CProverString.codePointAt:(Ljava/lang/String;I)I"] =
19251925
ID_cprover_string_code_point_at_func;
19261926
cprover_equivalent_to_java_function
1927-
["java::java.lang.String.codePointBefore:(I)I"]=
1927+
["java::org.cprover.CProverString.codePointBefore:(Ljava/lang/String;I)I"] =
19281928
ID_cprover_string_code_point_before_func;
19291929
cprover_equivalent_to_java_function
1930-
["java::java.lang.String.codePointCount:(II)I"]=
1930+
["java::org.cprover.CProverString.codePointCount:(Ljava/lang/String;II)I"] =
19311931
ID_cprover_string_code_point_count_func;
19321932
cprover_equivalent_to_java_function
19331933
["java::java.lang.String.compareTo:(Ljava/lang/String;)I"]=
@@ -2009,8 +2009,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
20092009
std::placeholders::_2,
20102010
std::placeholders::_3);
20112011
cprover_equivalent_to_java_function
2012-
["java::java.lang.String.offsetByCodePoints:(II)I"]=
2013-
ID_cprover_string_offset_by_code_point_func;
2012+
["java::org.cprover.CProverString.offsetByCodePoints:(Ljava/lang/"
2013+
"String;II)I"] = ID_cprover_string_offset_by_code_point_func;
20142014
cprover_equivalent_to_java_string_returning_function
20152015
["java::java.lang.String.replace:(CC)Ljava/lang/String;"]=
20162016
ID_cprover_string_replace_func;
@@ -2024,8 +2024,8 @@ void java_string_library_preprocesst::initialize_conversion_table()
20242024
["java::java.lang.String.startsWith:(Ljava/lang/String;I)Z"]=
20252025
ID_cprover_string_startswith_func;
20262026
cprover_equivalent_to_java_string_returning_function
2027-
["java::java.lang.String.subSequence:(II)Ljava/lang/CharSequence;"]=
2028-
ID_cprover_string_substring_func;
2027+
["java::org.cprover.CProverString.subSequence:(Ljava/lang/String;II)Ljava/"
2028+
"lang/CharSequence;"] = ID_cprover_string_substring_func;
20292029
// CProverString.substring differs from the Java String.substring in that no
20302030
// exception is raised for the out of bounds case.
20312031
cprover_equivalent_to_java_string_returning_function
@@ -2105,17 +2105,15 @@ void java_string_library_preprocesst::initialize_conversion_table()
21052105
["java::java.lang.StringBuilder.append:(D)Ljava/lang/StringBuilder;"] =
21062106
ID_cprover_string_concat_double_func;
21072107
cprover_equivalent_to_java_assign_and_return_function
2108-
["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;II)"
2109-
"Ljava/lang/StringBuilder;"]=
2110-
ID_cprover_string_concat_func;
2111-
cprover_equivalent_to_java_assign_and_return_function
2112-
["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
2113-
"Ljava/lang/StringBuilder;"]=
2114-
ID_cprover_string_concat_func;
2115-
cprover_equivalent_to_java_assign_and_return_function
2116-
["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
2117-
"Ljava/lang/StringBuilder;"]=
2118-
ID_cprover_string_concat_func;
2108+
["java::org.cprover.CProverString.append:(Ljava/lang/StringBuilder;Ljava/"
2109+
"lang/CharSequence;II)"
2110+
"Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2111+
cprover_equivalent_to_java_assign_and_return_function
2112+
["java::java.lang.StringBuilder.append:(Ljava/lang/CharSequence;)"
2113+
"Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
2114+
cprover_equivalent_to_java_assign_and_return_function
2115+
["java::java.lang.StringBuilder.append:(Ljava/lang/String;)"
2116+
"Ljava/lang/StringBuilder;"] = ID_cprover_string_concat_func;
21192117
cprover_equivalent_to_java_assign_and_return_function
21202118
["java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;"]=
21212119
ID_cprover_string_concat_bool_func;
@@ -2136,27 +2134,32 @@ void java_string_library_preprocesst::initialize_conversion_table()
21362134
["java::java.lang.StringBuilder.codePointCount:(II)I"]=
21372135
ID_cprover_string_code_point_count_func;
21382136
cprover_equivalent_to_java_assign_and_return_function
2139-
["java::java.lang.StringBuilder.delete:(II)Ljava/lang/StringBuilder;"]=
2137+
["java::org.cprover.CProverString.delete:(Ljava/lang/"
2138+
"StringBuilder;II)Ljava/lang/StringBuilder;"] =
21402139
ID_cprover_string_delete_func;
21412140
cprover_equivalent_to_java_assign_and_return_function
2142-
["java::java.lang.StringBuilder.deleteCharAt:(I)Ljava/lang/StringBuilder;"]=
2143-
ID_cprover_string_delete_char_at_func;
2141+
["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
2142+
"StringBuilder;I)Ljava/lang/StringBuilder;"] =
2143+
ID_cprover_string_delete_char_at_func;
21442144
cprover_equivalent_to_java_assign_and_return_function
2145-
["java::java.lang.StringBuilder.insert:(IC)Ljava/lang/StringBuilder;"]=
2146-
ID_cprover_string_insert_char_func;
2145+
["java::org.cprover.CProverString.insert:(Ljava/lang/"
2146+
"StringBuilder;IC)Ljava/lang/StringBuilder;"] =
2147+
ID_cprover_string_insert_char_func;
21472148
cprover_equivalent_to_java_assign_and_return_function
2148-
["java::java.lang.StringBuilder.insert:(IZ)Ljava/lang/StringBuilder;"]=
2149+
["java::org.cprover.CProverString.insert:(Ljava/lang/"
2150+
"StringBuilder;IZ)Ljava/lang/StringBuilder;"] =
21492151
ID_cprover_string_insert_bool_func;
21502152
cprover_equivalent_to_java_assign_and_return_function
2151-
["java::java.lang.StringBuilder.insert:(II)Ljava/lang/StringBuilder;"]=
2153+
["java::org.cprover.CProverString.insert:(Ljava/lang/"
2154+
"StringBuilder;II)Ljava/lang/StringBuilder;"] =
21522155
ID_cprover_string_insert_int_func;
21532156
cprover_equivalent_to_java_assign_and_return_function
2154-
["java::java.lang.StringBuilder.insert:(IJ)Ljava/lang/StringBuilder;"]=
2157+
["java::org.cprover.CProverString.insert:(Ljava/lang/"
2158+
"StringBuilder;IJ)Ljava/lang/StringBuilder;"] =
21552159
ID_cprover_string_insert_long_func;
21562160
cprover_equivalent_to_java_assign_and_return_function
2157-
["java::java.lang.StringBuilder.insert:(ILjava/lang/String;)"
2158-
"Ljava/lang/StringBuilder;"]=
2159-
ID_cprover_string_insert_func;
2161+
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
2162+
"lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
21602163
conversion_table
21612164
["java::java.lang.StringBuilder.length:()I"]=
21622165
std::bind(
@@ -2229,7 +2232,7 @@ void java_string_library_preprocesst::initialize_conversion_table()
22292232
"Ljava/lang/StringBuffer;"]=
22302233
ID_cprover_string_concat_code_point_func;
22312234
cprover_equivalent_to_java_function
2232-
["java::java.lang.StringBuffer.charAt:(I)C"]=
2235+
["java::org.cprover.CProverString.charAt:(Ljava/lang/StringBuffer;I)C"] =
22332236
ID_cprover_string_char_at_func;
22342237
cprover_equivalent_to_java_function
22352238
["java::java.lang.StringBuffer.codePointAt:(I)I"]=
@@ -2241,42 +2244,42 @@ void java_string_library_preprocesst::initialize_conversion_table()
22412244
["java::java.lang.StringBuffer.codePointCount:(II)I"]=
22422245
ID_cprover_string_code_point_count_func;
22432246
cprover_equivalent_to_java_assign_and_return_function
2244-
["java::java.lang.StringBuffer.delete:(II)Ljava/lang/StringBuffer;"]=
2245-
ID_cprover_string_delete_func;
2247+
["java::org.cprover.CProverString.delete:(Ljava/lang/StringBuffer;II)Ljava/"
2248+
"lang/StringBuffer;"] = ID_cprover_string_delete_func;
22462249
cprover_equivalent_to_java_assign_and_return_function
2247-
["java::java.lang.StringBuffer.deleteCharAt:(I)Ljava/lang/StringBuffer;"]=
2250+
["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
2251+
"StringBufferI)Ljava/lang/StringBuffer;"] =
22482252
ID_cprover_string_delete_char_at_func;
22492253
cprover_equivalent_to_java_assign_and_return_function
2250-
["java::java.lang.StringBuffer.insert:(IC)Ljava/lang/StringBuffer;"]=
2251-
ID_cprover_string_insert_char_func;
2254+
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IC)Ljava/"
2255+
"lang/StringBuffer;"] = ID_cprover_string_insert_char_func;
22522256
cprover_equivalent_to_java_assign_and_return_function
2253-
["java::java.lang.StringBuffer.insert:(II)Ljava/lang/StringBuffer;"]=
2254-
ID_cprover_string_insert_int_func;
2257+
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;II)Ljava/"
2258+
"lang/StringBuffer;"] = ID_cprover_string_insert_int_func;
22552259
cprover_equivalent_to_java_assign_and_return_function
2256-
["java::java.lang.StringBuffer.insert:(IJ)Ljava/lang/StringBuffer;"]=
2257-
ID_cprover_string_insert_long_func;
2260+
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IJ)Ljava/"
2261+
"lang/StringBuffer;"] = ID_cprover_string_insert_long_func;
22582262
cprover_equivalent_to_java_assign_and_return_function
2259-
["java::java.lang.StringBuffer.insert:(ILjava/lang/String;)"
2260-
"Ljava/lang/StringBuffer;"]=
2261-
ID_cprover_string_insert_func;
2263+
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;ILjava/"
2264+
"lang/String;)Ljava/lang/StringBuffer;"] = ID_cprover_string_insert_func;
22622265
cprover_equivalent_to_java_assign_and_return_function
2263-
["java::java.lang.StringBuffer.insert:(IZ)Ljava/lang/StringBuffer;"]=
2264-
ID_cprover_string_insert_bool_func;
2266+
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IZ)Ljava/"
2267+
"lang/StringBuffer;"] = ID_cprover_string_insert_bool_func;
22652268
conversion_table
22662269
["java::java.lang.StringBuffer.length:()I"]=
22672270
conversion_table["java::java.lang.String.length:()I"];
22682271
cprover_equivalent_to_java_assign_function
2269-
["java::java.lang.StringBuffer.setCharAt:(IC)V"]=
2272+
["java::org.cprover.CProverString.setCharAt:(Ljava/lang/String;IC)V"] =
22702273
ID_cprover_string_char_set_func;
22712274
cprover_equivalent_to_java_assign_function
2272-
["java::java.lang.StringBuffer.setLength:(I)V"]=
2273-
ID_cprover_string_set_length_func;
2275+
["java::org.cprover.CProverString.setLength:(Ljava/lang/String;I)V"] =
2276+
ID_cprover_string_set_length_func;
22742277
cprover_equivalent_to_java_string_returning_function
22752278
["java::java.lang.StringBuffer.substring:(I)Ljava/lang/String;"]=
22762279
ID_cprover_string_substring_func;
22772280
cprover_equivalent_to_java_string_returning_function
2278-
["java::java.lang.StringBuffer.substring:(II)Ljava/lang/String;"]=
2279-
ID_cprover_string_substring_func;
2281+
["java::org.cprover.CProverString.substring:(Ljava/Lang/"
2282+
"StringBuffer;II)Ljava/lang/String;"] = ID_cprover_string_substring_func;
22802283
conversion_table
22812284
["java::java.lang.StringBuffer.toString:()Ljava/lang/String;"]=
22822285
std::bind(

0 commit comments

Comments
 (0)