Rename get_length to get_or_create_length

Author: Joel Allred

jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp

@@ -95,7 +95,7 @@ refined_string_exprt make_refined_string_exprt(
   array_poolt &array_pool)
 {
   return refined_string_exprt(
-    array_pool.get_length(arr), get_data_pointer(arr));
+    array_pool.get_or_create_length(arr), get_data_pointer(arr));
 }
 
 /// For a constant `string_exprt`, creates a full index set.

src/solvers/strings/array_pool.cpp

@@ -21,13 +21,14 @@ operator()(const irep_idt &prefix, const typet &type)
   return result;
 }
 
-exprt array_poolt::get_length(const array_string_exprt &s)
+exprt array_poolt::get_or_create_length(const array_string_exprt &s)
 {
   if(const auto &if_expr = expr_try_dynamic_cast<if_exprt>((exprt)s))
   {
-    return if_exprt{if_expr->cond(),
-                    get_length(to_array_string_expr(if_expr->true_case())),
-                    get_length(to_array_string_expr(if_expr->false_case()))};
+    return if_exprt{
+      if_expr->cond(),
+      get_or_create_length(to_array_string_expr(if_expr->true_case())),
+      get_or_create_length(to_array_string_expr(if_expr->false_case()))};
   }
 
   auto emplace_result =
@@ -60,7 +61,7 @@ array_poolt::fresh_string(const typet &index_type, const typet &char_type)
     address_of_exprt(index_exprt(str, from_integer(0, index_type))), str);
 
   // add length to length_of_array map
-  get_length(str);
+  get_or_create_length(str);
 
   return str;
 }
@@ -111,7 +112,7 @@ array_string_exprt array_poolt::make_char_array_for_char_pointer(
     arrays_of_pointers.insert({char_pointer, array_sym});
 
   // add length to length_of_array map
-  get_length(array_sym);
+  get_or_create_length(array_sym);
 
   return to_array_string_expr(insert_result.first->second);
 }

src/solvers/strings/array_pool.h

@@ -62,7 +62,7 @@ class array_poolt final
   /// each of the parts.
   /// \param s: array expression representing a string
   /// \return expression for the length of `s`
-  exprt get_length(const array_string_exprt &s);
+  exprt get_or_create_length(const array_string_exprt &s);
 
   /// As opposed to get_length(), do not create a new symbol if the length
   /// of the array_string_exprt does not have one in the array_pool, but instead

src/solvers/strings/string_builtin_function.cpp

@@ -207,12 +207,13 @@ string_constraintst string_concat_char_builtin_functiont::constraints(
   constraints.universal.push_back([&] {
     const symbol_exprt idx =
       generator.fresh_symbol("QA_index_concat_char", result.length_type());
-    const exprt upper_bound = zero_if_negative(array_pool.get_length(input));
+    const exprt upper_bound =
+      zero_if_negative(array_pool.get_or_create_length(input));
     return string_constraintt(
       idx, upper_bound, equal_exprt(input[idx], result[idx]));
   }());
   constraints.existential.push_back(
-    equal_exprt(result[array_pool.get_length(input)], character));
+    equal_exprt(result[array_pool.get_or_create_length(input)], character));
   constraints.existential.push_back(
     equal_exprt(return_code, from_integer(0, return_code.type())));
   return constraints;
@@ -256,15 +257,17 @@ string_constraintst string_set_char_builtin_functiont::constraints(
   constraints.existential.push_back(implies_exprt(
     and_exprt(
       binary_relation_exprt(from_integer(0, position.type()), ID_le, position),
-      binary_relation_exprt(position, ID_lt, array_pool.get_length(result))),
+      binary_relation_exprt(
+        position, ID_lt, array_pool.get_or_create_length(result))),
     equal_exprt(result[position], character)));
   constraints.universal.push_back([&] {
     const symbol_exprt q =
       generator.fresh_symbol("QA_char_set", position.type());
     const equal_exprt a3_body(result[q], input[q]);
     return string_constraintt(
       q,
-      minimum(zero_if_negative(array_pool.get_length(result)), position),
+      minimum(
+        zero_if_negative(array_pool.get_or_create_length(result)), position),
       a3_body);
   }());
   constraints.universal.push_back([&] {
@@ -275,7 +278,7 @@ string_constraintst string_set_char_builtin_functiont::constraints(
     return string_constraintt(
       q2,
       lower_bound,
-      zero_if_negative(array_pool.get_length(result)),
+      zero_if_negative(array_pool.get_or_create_length(result)),
       a4_body);
   }());
   return constraints;
@@ -284,15 +287,18 @@ string_constraintst string_set_char_builtin_functiont::constraints(
 exprt string_set_char_builtin_functiont::length_constraint() const
 {
   const exprt out_of_bounds = or_exprt(
-    binary_relation_exprt(position, ID_ge, array_pool.get_length(input)),
+    binary_relation_exprt(
+      position, ID_ge, array_pool.get_or_create_length(input)),
     binary_relation_exprt(
       position, ID_lt, from_integer(0, input.length_type())));
   const exprt return_value = if_exprt(
     out_of_bounds,
     from_integer(1, return_code.type()),
     from_integer(0, return_code.type()));
   return and_exprt(
-    equal_exprt(array_pool.get_length(result), array_pool.get_length(input)),
+    equal_exprt(
+      array_pool.get_or_create_length(result),
+      array_pool.get_or_create_length(input)),
     equal_exprt(return_code, return_value));
 }
 
@@ -395,7 +401,7 @@ string_constraintst string_to_lower_case_builtin_functiont::constraints(
     }();
     return string_constraintt(
       idx,
-      zero_if_negative(array_pool.get_length(result)),
+      zero_if_negative(array_pool.get_or_create_length(result)),
       conditional_convert);
   }());
   return constraints;
@@ -440,7 +446,7 @@ string_constraintst string_to_upper_case_builtin_functiont::constraints(
       minus_exprt(input[idx], from_integer(0x20, char_type));
     return string_constraintt(
       idx,
-      zero_if_negative(array_pool.get_length(result)),
+      zero_if_negative(array_pool.get_or_create_length(result)),
       equal_exprt(
         result[idx],
         if_exprt(is_lower_case(input[idx]), converted, input[idx])));
@@ -606,7 +612,8 @@ exprt string_of_int_builtin_functiont::length_constraint() const
 
   const exprt size_expr_with_sign = if_exprt(
     negative_arg, plus_exprt(size_expr, from_integer(1, type)), size_expr);
-  return equal_exprt(array_pool.get_length(result), size_expr_with_sign);
+  return equal_exprt(
+    array_pool.get_or_create_length(result), size_expr_with_sign);
 }
 
 string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt(

src/solvers/strings/string_builtin_function.h

@@ -216,7 +216,9 @@ class string_to_lower_case_builtin_functiont
   exprt length_constraint() const override
   {
     return and_exprt(
-      equal_exprt(array_pool.get_length(result), array_pool.get_length(input)),
+      equal_exprt(
+        array_pool.get_or_create_length(result),
+        array_pool.get_or_create_length(input)),
       equal_exprt(return_code, from_integer(0, return_code.type())));
   };
 };
@@ -267,7 +269,9 @@ class string_to_upper_case_builtin_functiont
   exprt length_constraint() const override
   {
     return and_exprt(
-      equal_exprt(array_pool.get_length(result), array_pool.get_length(input)),
+      equal_exprt(
+        array_pool.get_or_create_length(result),
+        array_pool.get_or_create_length(input)),
       equal_exprt(return_code, from_integer(0, return_code.type())));
   };
 };

src/solvers/strings/string_constraint_generator_code_points.cpp

@@ -43,10 +43,11 @@ std::pair<exprt, string_constraintst> add_axioms_for_code_point(
   exprt hex0400 = from_integer(0x0400, type);
 
   binary_relation_exprt small(code_point, ID_lt, hex010000);
-  implies_exprt a1(small, equal_to(array_pool.get_length(res), 1));
+  implies_exprt a1(small, equal_to(array_pool.get_or_create_length(res), 1));
   constraints.existential.push_back(a1);
 
-  implies_exprt a2(not_exprt(small), equal_to(array_pool.get_length(res), 2));
+  implies_exprt a2(
+    not_exprt(small), equal_to(array_pool.get_or_create_length(res), 2));
   constraints.existential.push_back(a2);
 
   typecast_exprt code_point_as_char(code_point, char_type);
@@ -167,9 +168,9 @@ std::pair<exprt, string_constraintst> add_axioms_for_code_point_before(
   string_constraintst constraints;
 
   const exprt &char1 = str[minus_exprt(
-    args[1], from_integer(2, array_pool.get_length(str).type()))];
+    args[1], from_integer(2, array_pool.get_or_create_length(str).type()))];
   const exprt &char2 = str[minus_exprt(
-    args[1], from_integer(1, array_pool.get_length(str).type()))];
+    args[1], from_integer(1, array_pool.get_or_create_length(str).type()))];
   const typecast_exprt char1_as_int(char1, return_type);
   const typecast_exprt char2_as_int(char2, return_type);
 

src/solvers/strings/string_constraint_generator_comparison.cpp

@@ -47,14 +47,17 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals(
 
   // Axiom 1.
   constraints.existential.push_back(implies_exprt(
-    eq, equal_exprt(array_pool.get_length(s1), array_pool.get_length(s2))));
+    eq,
+    equal_exprt(
+      array_pool.get_or_create_length(s1),
+      array_pool.get_or_create_length(s2))));
 
   // Axiom 2.
   constraints.universal.push_back([&] {
     const symbol_exprt qvar = fresh_symbol("QA_equal", index_type);
     return string_constraintt(
       qvar,
-      zero_if_negative(array_pool.get_length(s1)),
+      zero_if_negative(array_pool.get_or_create_length(s1)),
       implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
   }());
 
@@ -63,12 +66,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals(
     const symbol_exprt witness = fresh_symbol("witness_unequal", index_type);
     const exprt zero = from_integer(0, index_type);
     const and_exprt bound_witness(
-      binary_relation_exprt(witness, ID_lt, array_pool.get_length(s1)),
+      binary_relation_exprt(
+        witness, ID_lt, array_pool.get_or_create_length(s1)),
       binary_relation_exprt(witness, ID_ge, zero));
     const and_exprt witnessing(
       bound_witness, notequal_exprt(s1[witness], s2[witness]));
     const and_exprt diff_length(
-      notequal_exprt(array_pool.get_length(s1), array_pool.get_length(s2)),
+      notequal_exprt(
+        array_pool.get_or_create_length(s1),
+        array_pool.get_or_create_length(s2)),
       equal_exprt(witness, from_integer(-1, index_type)));
     return implies_exprt(not_exprt(eq), or_exprt(diff_length, witnessing));
   }());
@@ -148,31 +154,36 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
   const typet index_type = s1.length_type();
 
   const implies_exprt a1(
-    eq, equal_exprt(array_pool.get_length(s1), array_pool.get_length(s2)));
+    eq,
+    equal_exprt(
+      array_pool.get_or_create_length(s1),
+      array_pool.get_or_create_length(s2)));
   constraints.existential.push_back(a1);
 
   const symbol_exprt qvar = fresh_symbol("QA_equal_ignore_case", index_type);
   const exprt constr2 =
     character_equals_ignore_case(s1[qvar], s2[qvar], char_a, char_A, char_Z);
   const string_constraintt a2(
     qvar,
-    zero_if_negative(array_pool.get_length(s1)),
+    zero_if_negative(array_pool.get_or_create_length(s1)),
     implies_exprt(eq, constr2));
   constraints.universal.push_back(a2);
 
   const symbol_exprt witness =
     fresh_symbol("witness_unequal_ignore_case", index_type);
   const exprt zero = from_integer(0, witness.type());
   const and_exprt bound_witness(
-    binary_relation_exprt(witness, ID_lt, array_pool.get_length(s1)),
+    binary_relation_exprt(witness, ID_lt, array_pool.get_or_create_length(s1)),
     binary_relation_exprt(witness, ID_ge, zero));
   const exprt witness_eq = character_equals_ignore_case(
     s1[witness], s2[witness], char_a, char_A, char_Z);
   const not_exprt witness_diff(witness_eq);
   const implies_exprt a3(
     not_exprt(eq),
     or_exprt(
-      notequal_exprt(array_pool.get_length(s1), array_pool.get_length(s2)),
+      notequal_exprt(
+        array_pool.get_or_create_length(s1),
+        array_pool.get_or_create_length(s2)),
       and_exprt(bound_witness, witness_diff)));
   constraints.existential.push_back(a3);
 
@@ -207,13 +218,17 @@ string_constraint_generatort::add_axioms_for_hash_code(
     const symbol_exprt i = fresh_symbol("index_hash", index_type);
     const equal_exprt c1(it.second, hash);
     const notequal_exprt c2(
-      array_pool.get_length(it.first), array_pool.get_length(str));
+      array_pool.get_or_create_length(it.first),
+      array_pool.get_or_create_length(str));
     const and_exprt c3(
-      equal_exprt(array_pool.get_length(it.first), array_pool.get_length(str)),
+      equal_exprt(
+        array_pool.get_or_create_length(it.first),
+        array_pool.get_or_create_length(str)),
       and_exprt(
         notequal_exprt(str[i], it.first[i]),
         and_exprt(
-          greater_than(array_pool.get_length(str), i), is_positive(i))));
+          greater_than(array_pool.get_or_create_length(str), i),
+          is_positive(i))));
     hash_constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3)));
   }
   return {hash, std::move(hash_constraints)};
@@ -257,13 +272,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_compare_to(
   const equal_exprt res_null(res, from_integer(0, return_type));
   const implies_exprt a1(
     res_null,
-    equal_exprt(array_pool.get_length(s1), array_pool.get_length(s2)));
+    equal_exprt(
+      array_pool.get_or_create_length(s1),
+      array_pool.get_or_create_length(s2)));
   constraints.existential.push_back(a1);
 
   const symbol_exprt i = fresh_symbol("QA_compare_to", index_type);
   const string_constraintt a2(
     i,
-    zero_if_negative(array_pool.get_length(s1)),
+    zero_if_negative(array_pool.get_or_create_length(s1)),
     implies_exprt(res_null, equal_exprt(s1[i], s2[i])));
   constraints.universal.push_back(a2);
 
@@ -275,24 +292,31 @@ std::pair<exprt, string_constraintst> add_axioms_for_compare_to(
   const equal_exprt ret_length_diff(
     res,
     minus_exprt(
-      typecast_exprt(array_pool.get_length(s1), return_type),
-      typecast_exprt(array_pool.get_length(s2), return_type)));
+      typecast_exprt(array_pool.get_or_create_length(s1), return_type),
+      typecast_exprt(array_pool.get_or_create_length(s2), return_type)));
   const or_exprt guard1(
     and_exprt(
       less_than_or_equal_to(
-        array_pool.get_length(s1), array_pool.get_length(s2)),
-      greater_than(array_pool.get_length(s1), x)),
+        array_pool.get_or_create_length(s1),
+        array_pool.get_or_create_length(s2)),
+      greater_than(array_pool.get_or_create_length(s1), x)),
     and_exprt(
-      greater_or_equal_to(array_pool.get_length(s1), array_pool.get_length(s2)),
-      greater_than(array_pool.get_length(s2), x)));
+      greater_or_equal_to(
+        array_pool.get_or_create_length(s1),
+        array_pool.get_or_create_length(s2)),
+      greater_than(array_pool.get_or_create_length(s2), x)));
   const and_exprt cond1(ret_char_diff, guard1);
   const or_exprt guard2(
     and_exprt(
-      greater_than(array_pool.get_length(s2), array_pool.get_length(s1)),
-      equal_to(array_pool.get_length(s1), x)),
+      greater_than(
+        array_pool.get_or_create_length(s2),
+        array_pool.get_or_create_length(s1)),
+      equal_to(array_pool.get_or_create_length(s1), x)),
     and_exprt(
-      greater_than(array_pool.get_length(s1), array_pool.get_length(s2)),
-      equal_to(array_pool.get_length(s2), x)));
+      greater_than(
+        array_pool.get_or_create_length(s1),
+        array_pool.get_or_create_length(s2)),
+      equal_to(array_pool.get_or_create_length(s2), x)));
   const and_exprt cond2(ret_length_diff, guard2);
 
   const implies_exprt a3(