Skip to content

Commit adf685f

Browse files
romainbrenguierromainbrenguier
authored
Merge pull request #5035 from romainbrenguier/clean-up/constraint-generation
Remove preprocessing of CProverString.insert for non-String arguments
2 parents 153a4b9 + 2402773 commit adf685f

File tree

15 files changed

+9
-226
lines changed

15 files changed

+9
-226
lines changed

‎jbmc/lib/java-models-library

‎jbmc/regression/jbmc-strings/java_insert_char/test_insert_char.class

-56 Bytes
Binary file not shown.

‎jbmc/regression/jbmc-strings/java_insert_char/test_insert_char.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ public class test_insert_char
33
public static void main()
44
{
55
StringBuilder sb = new StringBuilder("ac");
6-
org.cprover.CProverString.insert(sb, 1, 'b');
6+
sb.insert(1, 'b');
77
String s = sb.toString();
88
assert(!s.equals("abc"));
99
}

‎jbmc/regression/strings-smoke-tests/java_insert_char/test_insert_char.class

-56 Bytes
Binary file not shown.

‎jbmc/regression/strings-smoke-tests/java_insert_char/test_insert_char.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ public class test_insert_char
33
public static void main()
44
{
55
StringBuilder sb = new StringBuilder("ac");
6-
org.cprover.CProverString.insert(sb, 1, 'b');
6+
sb.insert(1, 'b');
77
String s = sb.toString();
88
assert(s.equals("abc"));
99
}

‎jbmc/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.class

-56 Bytes
Binary file not shown.

‎jbmc/regression/strings-smoke-tests/java_insert_char_array/test_insert_char_array.java

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ public static void insert(StringBuilder sb, int offset, char[] arr)
44
{
55
assert(arr.length<5);
66
for(int i=0; i<arr.length && i<5; i++)
7-
org.cprover.CProverString.insert(sb, offset+i, arr[i]);
7+
sb.insert(offset + i, arr[i]);
88
}
99

1010
public static void main(int i)

‎jbmc/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.class

-81 Bytes
Binary file not shown.

‎jbmc/regression/strings-smoke-tests/java_insert_multiple/test_insert_multiple.java

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ public class test_insert_multiple
33
public static void main()
44
{
55
StringBuilder sb = new StringBuilder("ad");
6-
org.cprover.CProverString.insert(sb, 1, 'c');
7-
org.cprover.CProverString.insert(sb, 1, "b");
6+
sb.insert(1, 'c');
7+
sb.insert(1, "b");
88
String s = sb.toString();
99
assert(s.equals("abcd"));
1010
}

‎jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 0 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -1683,22 +1683,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
16831683
["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
16841684
"StringBuilder;I)Ljava/lang/StringBuilder;"] =
16851685
ID_cprover_string_delete_char_at_func;
1686-
cprover_equivalent_to_java_assign_and_return_function
1687-
["java::org.cprover.CProverString.insert:(Ljava/lang/"
1688-
"StringBuilder;IC)Ljava/lang/StringBuilder;"] =
1689-
ID_cprover_string_insert_char_func;
1690-
cprover_equivalent_to_java_assign_and_return_function
1691-
["java::org.cprover.CProverString.insert:(Ljava/lang/"
1692-
"StringBuilder;IZ)Ljava/lang/StringBuilder;"] =
1693-
ID_cprover_string_insert_bool_func;
1694-
cprover_equivalent_to_java_assign_and_return_function
1695-
["java::org.cprover.CProverString.insert:(Ljava/lang/"
1696-
"StringBuilder;II)Ljava/lang/StringBuilder;"] =
1697-
ID_cprover_string_insert_int_func;
1698-
cprover_equivalent_to_java_assign_and_return_function
1699-
["java::org.cprover.CProverString.insert:(Ljava/lang/"
1700-
"StringBuilder;IJ)Ljava/lang/StringBuilder;"] =
1701-
ID_cprover_string_insert_long_func;
17021686
cprover_equivalent_to_java_assign_and_return_function
17031687
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuilder;ILjava/"
17041688
"lang/String;)Ljava/lang/StringBuilder;"] = ID_cprover_string_insert_func;
@@ -1779,21 +1763,6 @@ void java_string_library_preprocesst::initialize_conversion_table()
17791763
["java::org.cprover.CProverString.deleteCharAt:(Ljava/lang/"
17801764
"StringBufferI)Ljava/lang/StringBuffer;"] =
17811765
ID_cprover_string_delete_char_at_func;
1782-
cprover_equivalent_to_java_assign_and_return_function
1783-
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IC)Ljava/"
1784-
"lang/StringBuffer;"] = ID_cprover_string_insert_char_func;
1785-
cprover_equivalent_to_java_assign_and_return_function
1786-
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;II)Ljava/"
1787-
"lang/StringBuffer;"] = ID_cprover_string_insert_int_func;
1788-
cprover_equivalent_to_java_assign_and_return_function
1789-
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IJ)Ljava/"
1790-
"lang/StringBuffer;"] = ID_cprover_string_insert_long_func;
1791-
cprover_equivalent_to_java_assign_and_return_function
1792-
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;ILjava/"
1793-
"lang/String;)Ljava/lang/StringBuffer;"] = ID_cprover_string_insert_func;
1794-
cprover_equivalent_to_java_assign_and_return_function
1795-
["java::org.cprover.CProverString.insert:(Ljava/lang/StringBuffer;IZ)Ljava/"
1796-
"lang/StringBuffer;"] = ID_cprover_string_insert_bool_func;
17971766
conversion_table
17981767
["java::java.lang.StringBuffer.length:()I"]=
17991768
conversion_table["java::java.lang.String.length:()I"];

‎src/solvers/README.md

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -514,10 +514,7 @@ This is described in more detail \link string_builtin_functiont here. \endlink
514514
* `cprover_string_offset_by_code_point`, `cprover_string_concat_char`,
515515
`cprover_string_concat_int`, `cprover_string_concat_long`,
516516
`cprover_string_concat_bool`, `cprover_string_concat_double`,
517-
`cprover_string_concat_float`, `cprover_string_insert_int`,
518-
`cprover_string_insert_long`, `cprover_string_insert_bool`,
519-
`cprover_string_insert_char`, `cprover_string_insert_double`,
520-
`cprover_string_insert_float` :
517+
`cprover_string_concat_float` :
521518
Should be done in two steps: conversion from primitive type and call
522519
to the string primitive.
523520
* `cprover_string_array_of_char_pointer`, `cprover_string_to_char_array` :

‎src/solvers/strings/string_constraint_generator.h

Lines changed: 0 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -211,29 +211,6 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
211211
symbol_generatort &fresh_symbol,
212212
const function_application_exprt &f,
213213
array_poolt &array_pool);
214-
std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
215-
symbol_generatort &fresh_symbol,
216-
const function_application_exprt &f,
217-
array_poolt &array_pool,
218-
const namespacet &ns);
219-
std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
220-
symbol_generatort &fresh_symbol,
221-
const function_application_exprt &f,
222-
array_poolt &array_pool);
223-
std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
224-
symbol_generatort &fresh_symbol,
225-
const function_application_exprt &f,
226-
array_poolt &array_pool);
227-
std::pair<exprt, string_constraintst> add_axioms_for_insert_float(
228-
symbol_generatort &fresh_symbol,
229-
const function_application_exprt &f,
230-
array_poolt &array_pool,
231-
const namespacet &ns);
232-
std::pair<exprt, string_constraintst> add_axioms_for_insert_double(
233-
symbol_generatort &fresh_symbol,
234-
const function_application_exprt &f,
235-
array_poolt &array_pool,
236-
const namespacet &ns);
237214

238215
std::pair<exprt, string_constraintst> add_axioms_for_cprover_string(
239216
symbol_generatort &fresh_symbol,

‎src/solvers/strings/string_constraint_generator_insert.cpp

Lines changed: 2 additions & 144 deletions
Original file line numberDiff line numberDiff line change
@@ -117,154 +117,12 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
117117
symbol_generatort &fresh_symbol,
118118
const function_application_exprt &f,
119119
array_poolt &array_pool)
120-
{
121-
PRECONDITION(f.arguments().size() == 5 || f.arguments().size() == 7);
122-
array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
123-
array_string_exprt s2 = get_string_expr(array_pool, f.arguments()[4]);
124-
array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]);
125-
const exprt &offset = f.arguments()[3];
126-
if(f.arguments().size() == 7)
127-
{
128-
const exprt &start = f.arguments()[5];
129-
const exprt &end = f.arguments()[6];
130-
const typet &char_type = s1.content().type().subtype();
131-
const typet &index_type = s1.length_type();
132-
const array_string_exprt substring =
133-
array_pool.fresh_string(index_type, char_type);
134-
return combine_results(
135-
add_axioms_for_substring(
136-
fresh_symbol, substring, s2, start, end, array_pool),
137-
add_axioms_for_insert(
138-
fresh_symbol, res, s1, substring, offset, array_pool));
139-
}
140-
else // 5 arguments
141-
{
142-
return add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool);
143-
}
144-
}
145-
146-
/// add axioms corresponding to the StringBuilder.insert(I) java function
147-
/// \deprecated should convert the value to string and call insert
148-
/// \param fresh_symbol: generator of fresh symbols
149-
/// \param f: function application with three arguments: a string, an
150-
/// integer offset, and an integer
151-
/// \param array_pool: pool of arrays representing strings
152-
/// \param ns: namespace
153-
/// \return an expression
154-
DEPRECATED(SINCE(2017, 10, 5, "convert the value to string and call insert"))
155-
std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
156-
symbol_generatort &fresh_symbol,
157-
const function_application_exprt &f,
158-
array_poolt &array_pool,
159-
const namespacet &ns)
160-
{
161-
PRECONDITION(f.arguments().size() == 5);
162-
const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
163-
const array_string_exprt res =
164-
array_pool.find(f.arguments()[1], f.arguments()[0]);
165-
const exprt &offset = f.arguments()[3];
166-
const typet &index_type = s1.length_type();
167-
const typet &char_type = s1.content().type().subtype();
168-
const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
169-
return combine_results(
170-
add_axioms_for_string_of_int(s2, f.arguments()[4], 0, ns, array_pool),
171-
add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
172-
}
173-
174-
/// add axioms corresponding to the StringBuilder.insert(Z) java function
175-
/// \deprecated should convert the value to string and call insert
176-
/// \param fresh_symbol: generator of fresh symbols
177-
/// \param f: function application with three arguments: a string, an
178-
/// integer offset, and a Boolean
179-
/// \param array_pool: pool of arrays representing strings
180-
/// \return a new string expression
181-
DEPRECATED(SINCE(2017, 10, 5, "convert the value to string and call insert"))
182-
std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
183-
symbol_generatort &fresh_symbol,
184-
const function_application_exprt &f,
185-
array_poolt &array_pool)
186-
{
187-
PRECONDITION(f.arguments().size() == 5);
188-
const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[0]);
189-
const array_string_exprt res =
190-
array_pool.find(f.arguments()[1], f.arguments()[0]);
191-
const exprt &offset = f.arguments()[3];
192-
const typet &index_type = s1.length_type();
193-
const typet &char_type = s1.content().type().subtype();
194-
const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
195-
return combine_results(
196-
add_axioms_from_bool(s2, f.arguments()[4], array_pool),
197-
add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
198-
}
199-
200-
/// Add axioms corresponding to the StringBuilder.insert(C) java function
201-
/// \todo This should be merged with add_axioms_for_insert.
202-
/// \param fresh_symbol: generator of fresh symbols
203-
/// \param f: function application with three arguments: a string, an
204-
/// integer offset, and a character
205-
/// \param array_pool: pool of arrays representing strings
206-
/// \return an expression
207-
std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
208-
symbol_generatort &fresh_symbol,
209-
const function_application_exprt &f,
210-
array_poolt &array_pool)
211120
{
212121
PRECONDITION(f.arguments().size() == 5);
213-
const array_string_exprt res =
214-
array_pool.find(f.arguments()[1], f.arguments()[0]);
215122
const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
216-
const exprt &offset = f.arguments()[3];
217-
const typet &index_type = s1.length_type();
218-
const typet &char_type = s1.content().type().subtype();
219-
const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
220-
return combine_results(
221-
add_axioms_from_char(s2, f.arguments()[4], array_pool),
222-
add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
223-
}
224-
225-
/// add axioms corresponding to the StringBuilder.insert(D) java function
226-
/// \deprecated should convert the value to string and call insert
227-
/// \param fresh_symbol: generator of fresh symbols
228-
/// \param f: function application with three arguments: a string, an
229-
/// integer offset, and a double
230-
/// \param array_pool: pool of arrays representing strings
231-
/// \param ns: namespace
232-
/// \return a string expression
233-
DEPRECATED(SINCE(2017, 10, 5, "convert the value to string and call insert"))
234-
std::pair<exprt, string_constraintst> add_axioms_for_insert_double(
235-
symbol_generatort &fresh_symbol,
236-
const function_application_exprt &f,
237-
array_poolt &array_pool,
238-
const namespacet &ns)
239-
{
240-
PRECONDITION(f.arguments().size() == 5);
123+
const array_string_exprt s2 = get_string_expr(array_pool, f.arguments()[4]);
241124
const array_string_exprt res =
242125
array_pool.find(f.arguments()[1], f.arguments()[0]);
243-
const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
244126
const exprt &offset = f.arguments()[3];
245-
const typet &index_type = s1.length_type();
246-
const typet &char_type = s1.content().type().subtype();
247-
const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
248-
return combine_results(
249-
add_axioms_for_string_of_float(
250-
fresh_symbol, s2, f.arguments()[4], array_pool, ns),
251-
add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool));
252-
}
253-
254-
/// Add axioms corresponding to the StringBuilder.insert(F) java function
255-
/// \deprecated should convert the value to string and call insert
256-
/// \param fresh_symbol: generator of fresh symbols
257-
/// \param f: function application with three arguments: a string, an
258-
/// integer offset, and a float
259-
/// \param array_pool: pool of arrays representing strings
260-
/// \param ns: namespace
261-
/// \return a new string expression
262-
DEPRECATED(SINCE(2017, 10, 5, "convert the value to string and call insert"))
263-
std::pair<exprt, string_constraintst> add_axioms_for_insert_float(
264-
symbol_generatort &fresh_symbol,
265-
const function_application_exprt &f,
266-
array_poolt &array_pool,
267-
const namespacet &ns)
268-
{
269-
return add_axioms_for_insert_double(fresh_symbol, f, array_pool, ns);
127+
return add_axioms_for_insert(fresh_symbol, res, s1, s2, offset, array_pool);
270128
}

‎src/solvers/strings/string_constraint_generator_main.cpp

Lines changed: 0 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -264,18 +264,6 @@ string_constraint_generatort::add_axioms_for_function_application(
264264
return add_axioms_for_concat_code_point(fresh_symbol, expr, array_pool);
265265
else if(id == ID_cprover_string_insert_func)
266266
return add_axioms_for_insert(fresh_symbol, expr, array_pool);
267-
else if(id == ID_cprover_string_insert_int_func)
268-
return add_axioms_for_insert_int(fresh_symbol, expr, array_pool, ns);
269-
else if(id == ID_cprover_string_insert_long_func)
270-
return add_axioms_for_insert_int(fresh_symbol, expr, array_pool, ns);
271-
else if(id == ID_cprover_string_insert_bool_func)
272-
return add_axioms_for_insert_bool(fresh_symbol, expr, array_pool);
273-
else if(id == ID_cprover_string_insert_char_func)
274-
return add_axioms_for_insert_char(fresh_symbol, expr, array_pool);
275-
else if(id == ID_cprover_string_insert_double_func)
276-
return add_axioms_for_insert_double(fresh_symbol, expr, array_pool, ns);
277-
else if(id == ID_cprover_string_insert_float_func)
278-
return add_axioms_for_insert_float(fresh_symbol, expr, array_pool, ns);
279267
else if(id == ID_cprover_string_substring_func)
280268
return add_axioms_for_substring(fresh_symbol, expr, array_pool);
281269
else if(id == ID_cprover_string_trim_func)

‎src/util/irep_ids.def

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -611,12 +611,6 @@ IREP_ID_ONE(cprover_string_endswith_func)
611611
IREP_ID_ONE(cprover_string_format_func)
612612
IREP_ID_ONE(cprover_string_index_of_func)
613613
IREP_ID_ONE(cprover_string_insert_func)
614-
IREP_ID_ONE(cprover_string_insert_int_func)
615-
IREP_ID_ONE(cprover_string_insert_long_func)
616-
IREP_ID_ONE(cprover_string_insert_bool_func)
617-
IREP_ID_ONE(cprover_string_insert_char_func)
618-
IREP_ID_ONE(cprover_string_insert_float_func)
619-
IREP_ID_ONE(cprover_string_insert_double_func)
620614
IREP_ID_ONE(cprover_string_is_prefix_func)
621615
IREP_ID_ONE(cprover_string_is_suffix_func)
622616
IREP_ID_ONE(cprover_string_is_empty_func)

0 commit comments

Comments
 (0)