Merge pull request #4544 from romainbrenguier/clean-up/string-constraints1

tautschnig · web-flow · commit f63c394f77f8 · 2019-04-29T13:27:50.000+03:00
Clean up in string solver
diff --git a/src/solvers/strings/array_pool.cpp b/src/solvers/strings/array_pool.cpp
@@ -123,14 +123,6 @@ array_poolt::find(const exprt &pointer, const exprt &length)
   return *created_strings_value.insert(array).first;
 }
 
-const array_string_exprt &char_array_of_pointer(
-  array_poolt &pool,
-  const exprt &pointer,
-  const exprt &length)
-{
-  return pool.find(pointer, length);
-}
-
 array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg)
 {
   const auto string_argument = expr_checked_cast<struct_exprt>(arg);
@@ -141,5 +133,5 @@ array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
 {
   PRECONDITION(is_refined_string_type(expr.type()));
   const refined_string_exprt &str = to_string_expr(expr);
-  return char_array_of_pointer(pool, str.content(), str.length());
+  return pool.find(str.content(), str.length());
 }
diff --git a/src/solvers/strings/array_pool.h b/src/solvers/strings/array_pool.h
@@ -97,13 +97,6 @@ class array_poolt final
 /// are given as a struct containing a length and pointer to an array.
 array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg);
 
-/// Return the array associated to the given pointer or creates a new one
-DEPRECATED("use pool.find(pointer, length) instead")
-const array_string_exprt &char_array_of_pointer(
-  array_poolt &pool,
-  const exprt &pointer,
-  const exprt &length);
-
 /// Fetch the string_exprt corresponding to the given refined_string_exprt
 /// \param pool: pool of arrays representing strings
 /// \param expr: an expression of refined string type
diff --git a/src/solvers/strings/string_constraint_generator_code_points.cpp b/src/solvers/strings/string_constraint_generator_code_points.cpp
@@ -196,7 +196,6 @@ std::pair<exprt, string_constraintst> add_axioms_for_code_point_count(
 {
   PRECONDITION(f.arguments().size() == 3);
   string_constraintst constraints;
-  const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
   const exprt &begin = f.arguments()[1];
   const exprt &end = f.arguments()[2];
   const typet &return_type = f.type();
diff --git a/src/solvers/strings/string_constraint_generator_concat.cpp b/src/solvers/strings/string_constraint_generator_concat.cpp
@@ -147,7 +147,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
 {
   PRECONDITION(f.arguments().size() == 4);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
   const typet &char_type = s1.content().type().subtype();
   const typet &index_type = s1.length().type();
diff --git a/src/solvers/strings/string_constraint_generator_constants.cpp b/src/solvers/strings/string_constraint_generator_constants.cpp
@@ -117,8 +117,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_literal(
 {
   const function_application_exprt::argumentst &args = f.arguments();
   PRECONDITION(args.size() == 3); // Bad args to string literal?
-  const array_string_exprt res =
-    char_array_of_pointer(array_pool, args[1], args[0]);
+  const array_string_exprt res = array_pool.find(args[1], args[0]);
   return add_axioms_for_cprover_string(
     fresh_symbol, res, args[2], true_exprt());
 }
diff --git a/src/solvers/strings/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp
@@ -165,8 +165,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
   const namespacet &ns)
 {
   PRECONDITION(f.arguments().size() == 3);
-  array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+  array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]);
   return add_axioms_for_string_of_float(
     fresh_symbol, res, f.arguments()[2], array_pool, ns);
 }
@@ -551,7 +550,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
 {
   PRECONDITION(f.arguments().size() == 3);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   const exprt &arg = f.arguments()[2];
   return add_axioms_from_float_scientific_notation(
     fresh_symbol, res, arg, array_pool, ns);
diff --git a/src/solvers/strings/string_constraint_generator_format.cpp b/src/solvers/strings/string_constraint_generator_format.cpp
@@ -603,7 +603,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
 {
   PRECONDITION(f.arguments().size() >= 3);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
 
   if(s1.length().id() == ID_constant && s1.content().id() == ID_array)
diff --git a/src/solvers/strings/string_constraint_generator_insert.cpp b/src/solvers/strings/string_constraint_generator_insert.cpp
@@ -111,8 +111,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
   PRECONDITION(f.arguments().size() == 5 || f.arguments().size() == 7);
   array_string_exprt s1 = get_string_expr(pool, f.arguments()[2]);
   array_string_exprt s2 = get_string_expr(pool, f.arguments()[4]);
-  array_string_exprt res =
-    char_array_of_pointer(pool, f.arguments()[1], f.arguments()[0]);
+  array_string_exprt res = pool.find(f.arguments()[1], f.arguments()[0]);
   const exprt &offset = f.arguments()[3];
   if(f.arguments().size() == 7)
   {
@@ -150,7 +149,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
   PRECONDITION(f.arguments().size() == 5);
   const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   const exprt &offset = f.arguments()[3];
   const typet &index_type = s1.length().type();
   const typet &char_type = s1.content().type().subtype();
@@ -176,7 +175,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
   PRECONDITION(f.arguments().size() == 5);
   const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[0]);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   const exprt &offset = f.arguments()[3];
   const typet &index_type = s1.length().type();
   const typet &char_type = s1.content().type().subtype();
@@ -200,7 +199,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
 {
   PRECONDITION(f.arguments().size() == 5);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
   const exprt &offset = f.arguments()[3];
   const typet &index_type = s1.length().type();
@@ -228,7 +227,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_double(
 {
   PRECONDITION(f.arguments().size() == 5);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
   const exprt &offset = f.arguments()[3];
   const typet &index_type = s1.length().type();
diff --git a/src/solvers/strings/string_constraint_generator_main.cpp b/src/solvers/strings/string_constraint_generator_main.cpp
@@ -173,8 +173,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_constrain_characters(
   PRECONDITION(args[2].type().id() == ID_string);
   PRECONDITION(args[2].id() == ID_constant);
 
-  const array_string_exprt s =
-    char_array_of_pointer(array_pool, args[1], args[0]);
+  const array_string_exprt s = array_pool.find(args[1], args[0]);
   const irep_idt &char_set_string = to_constant_expr(args[2]).get_value();
   const exprt &start =
     args.size() >= 4 ? args[3] : from_integer(0, s.length().type());
@@ -340,8 +339,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_copy(
 {
   const auto &args = f.arguments();
   PRECONDITION(args.size() == 3 || args.size() == 5);
-  const array_string_exprt res =
-    char_array_of_pointer(array_pool, args[1], args[0]);
+  const array_string_exprt res = array_pool.find(args[1], args[0]);
   const array_string_exprt str = get_string_expr(array_pool, args[2]);
   const typet &index_type = str.length().type();
   const exprt offset = args.size() == 3 ? from_integer(0, index_type) : args[3];
diff --git a/src/solvers/strings/string_constraint_generator_transformation.cpp b/src/solvers/strings/string_constraint_generator_transformation.cpp
@@ -43,7 +43,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_set_length(
   PRECONDITION(f.arguments().size() == 4);
   string_constraintst constraints;
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
   const exprt &k = f.arguments()[3];
   const typet &index_type = s1.length().type();
@@ -100,8 +100,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_substring(
   const function_application_exprt::argumentst &args = f.arguments();
   PRECONDITION(args.size() == 4 || args.size() == 5);
   const array_string_exprt str = get_string_expr(array_pool, args[2]);
-  const array_string_exprt res =
-    char_array_of_pointer(array_pool, args[1], args[0]);
+  const array_string_exprt res = array_pool.find(args[1], args[0]);
   const exprt &i = args[3];
   const exprt j = args.size() == 5 ? args[4] : str.length();
   return add_axioms_for_substring(fresh_symbol, res, str, i, j);
@@ -190,7 +189,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_trim(
   string_constraintst constraints;
   const array_string_exprt &str = get_string_expr(array_pool, f.arguments()[2]);
   const array_string_exprt &res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   const typet &index_type = str.length().type();
   const typet &char_type = str.content().type().subtype();
   const symbol_exprt idx = fresh_symbol("index_trim", index_type);
@@ -302,8 +301,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_replace(
   PRECONDITION(f.arguments().size() == 5);
   string_constraintst constraints;
   array_string_exprt str = get_string_expr(array_pool, f.arguments()[2]);
-  array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+  array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]);
   if(
     const auto maybe_chars =
       to_char_pair(f.arguments()[3], f.arguments()[4], [&](const exprt &e) {
@@ -342,7 +340,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_delete_char_at(
 {
   PRECONDITION(f.arguments().size() == 4);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   const array_string_exprt str = get_string_expr(array_pool, f.arguments()[2]);
   exprt index_one = from_integer(1, str.length().type());
   return add_axioms_for_delete(
@@ -414,7 +412,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_delete(
 {
   PRECONDITION(f.arguments().size() == 5);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   const array_string_exprt arg = get_string_expr(array_pool, f.arguments()[2]);
   return add_axioms_for_delete(
     fresh_symbol, res, arg, f.arguments()[3], f.arguments()[4], array_pool);
diff --git a/src/solvers/strings/string_constraint_generator_valueof.cpp b/src/solvers/strings/string_constraint_generator_valueof.cpp
@@ -50,7 +50,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_long(
 {
   PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   if(f.arguments().size() == 4)
     return add_axioms_for_string_of_int_with_radix(
       res, f.arguments()[2], f.arguments()[3], 0, ns);
@@ -70,7 +70,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_bool(
 {
   PRECONDITION(f.arguments().size() == 3);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   return add_axioms_from_bool(res, f.arguments()[2]);
 }
 
@@ -275,7 +275,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_int_hex(
 {
   PRECONDITION(f.arguments().size() == 3);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   return add_axioms_from_int_hex(res, f.arguments()[2]);
 }
 
@@ -296,7 +296,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_char(
 {
   PRECONDITION(f.arguments().size() == 3);
   const array_string_exprt res =
-    char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
+    array_pool.find(f.arguments()[1], f.arguments()[0]);
   return add_axioms_from_char(res, f.arguments()[2]);
 }
 
diff --git a/src/solvers/strings/string_constraint_instantiation.cpp b/src/solvers/strings/string_constraint_instantiation.cpp
diff --git a/src/solvers/strings/string_constraint_instantiation.h b/src/solvers/strings/string_constraint_instantiation.h
diff --git a/src/solvers/strings/string_refinement.cpp b/src/solvers/strings/string_refinement.cpp

Original file line number	Diff line number	Diff line change
`@@ -123,14 +123,6 @@ array_poolt::find(const exprt &pointer, const exprt &length)`
`123`	`123`	`return *created_strings_value.insert(array).first;`
`124`	`124`	`}`
`125`	`125`
`126`		`-const array_string_exprt &char_array_of_pointer(`
`127`		`- array_poolt &pool,`
`128`		`- const exprt &pointer,`
`129`		`- const exprt &length)`
`130`		`-{`
`131`		`- return pool.find(pointer, length);`
`132`		`-}`
`133`		`-`
`134`	`126`	`array_string_exprt of_argument(array_poolt &array_pool, const exprt &arg)`
`135`	`127`	`{`
`136`	`128`	`const auto string_argument = expr_checked_cast<struct_exprt>(arg);`
`@@ -141,5 +133,5 @@ array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)`
`141`	`133`	`{`
`142`	`134`	`PRECONDITION(is_refined_string_type(expr.type()));`
`143`	`135`	`const refined_string_exprt &str = to_string_expr(expr);`
`144`		`- return char_array_of_pointer(pool, str.content(), str.length());`
	`136`	`+ return pool.find(str.content(), str.length());`
`145`	`137`	`}`
Original file line number	Diff line number	Diff line change
`@@ -196,7 +196,6 @@ std::pair<exprt, string_constraintst> add_axioms_for_code_point_count(`
`196`	`196`	`{`
`197`	`197`	`PRECONDITION(f.arguments().size() == 3);`
`198`	`198`	`string_constraintst constraints;`
`199`		`- const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);`
`200`	`199`	`const exprt &begin = f.arguments()[1];`
`201`	`200`	`const exprt &end = f.arguments()[2];`
`202`	`201`	`const typet &return_type = f.type();`
Original file line number	Diff line number	Diff line change
`@@ -147,7 +147,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(`
`147`	`147`	`{`
`148`	`148`	`PRECONDITION(f.arguments().size() == 4);`
`149`	`149`	`const array_string_exprt res =`
`150`		`- char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);`
	`150`	`+ array_pool.find(f.arguments()[1], f.arguments()[0]);`
`151`	`151`	`const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);`
`152`	`152`	`const typet &char_type = s1.content().type().subtype();`
`153`	`153`	`const typet &index_type = s1.length().type();`
Original file line number	Diff line number	Diff line change
`@@ -117,8 +117,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_literal(`
`117`	`117`	`{`
`118`	`118`	`const function_application_exprt::argumentst &args = f.arguments();`
`119`	`119`	`PRECONDITION(args.size() == 3); // Bad args to string literal?`
`120`		`- const array_string_exprt res =`
`121`		`- char_array_of_pointer(array_pool, args[1], args[0]);`
	`120`	`+ const array_string_exprt res = array_pool.find(args[1], args[0]);`
`122`	`121`	`return add_axioms_for_cprover_string(`
`123`	`122`	`fresh_symbol, res, args[2], true_exprt());`
`124`	`123`	`}`
Original file line number	Diff line number	Diff line change
`@@ -165,8 +165,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(`
`165`	`165`	`const namespacet &ns)`
`166`	`166`	`{`
`167`	`167`	`PRECONDITION(f.arguments().size() == 3);`
`168`		`- array_string_exprt res =`
`169`		`- char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);`
	`168`	`+ array_string_exprt res = array_pool.find(f.arguments()[1], f.arguments()[0]);`
`170`	`169`	`return add_axioms_for_string_of_float(`
`171`	`170`	`fresh_symbol, res, f.arguments()[2], array_pool, ns);`
`172`	`171`	`}`
`@@ -551,7 +550,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(`
`551`	`550`	`{`
`552`	`551`	`PRECONDITION(f.arguments().size() == 3);`
`553`	`552`	`const array_string_exprt res =`
`554`		`- char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);`
	`553`	`+ array_pool.find(f.arguments()[1], f.arguments()[0]);`
`555`	`554`	`const exprt &arg = f.arguments()[2];`
`556`	`555`	`return add_axioms_from_float_scientific_notation(`
`557`	`556`	`fresh_symbol, res, arg, array_pool, ns);`
Original file line number	Diff line number	Diff line change
`@@ -603,7 +603,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(`
`603`	`603`	`{`
`604`	`604`	`PRECONDITION(f.arguments().size() >= 3);`
`605`	`605`	`const array_string_exprt res =`
`606`		`- char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);`
	`606`	`+ array_pool.find(f.arguments()[1], f.arguments()[0]);`
`607`	`607`	`const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);`
`608`	`608`
`609`	`609`	`if(s1.length().id() == ID_constant && s1.content().id() == ID_array)`
Original file line number	Diff line number	Diff line change
`@@ -50,7 +50,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_long(`
`50`	`50`	`{`
`51`	`51`	`PRECONDITION(f.arguments().size() == 3 \|\| f.arguments().size() == 4);`
`52`	`52`	`const array_string_exprt res =`
`53`		`- char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);`
	`53`	`+ array_pool.find(f.arguments()[1], f.arguments()[0]);`
`54`	`54`	`if(f.arguments().size() == 4)`
`55`	`55`	`return add_axioms_for_string_of_int_with_radix(`
`56`	`56`	`res, f.arguments()[2], f.arguments()[3], 0, ns);`
`@@ -70,7 +70,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_bool(`
`70`	`70`	`{`
`71`	`71`	`PRECONDITION(f.arguments().size() == 3);`
`72`	`72`	`const array_string_exprt res =`
`73`		`- char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);`
	`73`	`+ array_pool.find(f.arguments()[1], f.arguments()[0]);`
`74`	`74`	`return add_axioms_from_bool(res, f.arguments()[2]);`
`75`	`75`	`}`
`76`	`76`
`@@ -275,7 +275,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_int_hex(`
`275`	`275`	`{`
`276`	`276`	`PRECONDITION(f.arguments().size() == 3);`
`277`	`277`	`const array_string_exprt res =`
`278`		`- char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);`
	`278`	`+ array_pool.find(f.arguments()[1], f.arguments()[0]);`
`279`	`279`	`return add_axioms_from_int_hex(res, f.arguments()[2]);`
`280`	`280`	`}`
`281`	`281`
`@@ -296,7 +296,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_char(`
`296`	`296`	`{`
`297`	`297`	`PRECONDITION(f.arguments().size() == 3);`
`298`	`298`	`const array_string_exprt res =`
`299`		`- char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);`
	`299`	`+ array_pool.find(f.arguments()[1], f.arguments()[0]);`
`300`	`300`	`return add_axioms_from_char(res, f.arguments()[2]);`
`301`	`301`	`}`
`302`	`302`