Read string length from array pool

Replace calls to str.length() by calls to array_pool.get_length(str).

Author: Joel Allred

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

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

src/solvers/strings/string_builtin_function.cpp

@@ -207,12 +207,12 @@ 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(input.length());
+    const exprt upper_bound = zero_if_negative(array_pool.get_length(input));
     return string_constraintt(
       idx, upper_bound, equal_exprt(input[idx], result[idx]));
   }());
   constraints.existential.push_back(
-    equal_exprt(result[input.length()], character));
+    equal_exprt(result[array_pool.get_length(input)], character));
   constraints.existential.push_back(
     equal_exprt(return_code, from_integer(0, return_code.type())));
   return constraints;
@@ -256,38 +256,43 @@ 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, result.length())),
+      binary_relation_exprt(position, ID_lt, array_pool.get_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(result.length()), position), a3_body);
+      q,
+      minimum(zero_if_negative(array_pool.get_length(result)), position),
+      a3_body);
   }());
   constraints.universal.push_back([&] {
     const symbol_exprt q2 =
       generator.fresh_symbol("QA_char_set2", position.type());
     const plus_exprt lower_bound(position, from_integer(1, position.type()));
     const equal_exprt a4_body(result[q2], input[q2]);
     return string_constraintt(
-      q2, lower_bound, zero_if_negative(result.length()), a4_body);
+      q2,
+      lower_bound,
+      zero_if_negative(array_pool.get_length(result)),
+      a4_body);
   }());
   return constraints;
 }
 
 exprt string_set_char_builtin_functiont::length_constraint() const
 {
   const exprt out_of_bounds = or_exprt(
-    binary_relation_exprt(position, ID_ge, input.length()),
+    binary_relation_exprt(position, ID_ge, array_pool.get_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(result.length(), input.length()),
+    equal_exprt(array_pool.get_length(result), array_pool.get_length(input)),
     equal_exprt(return_code, return_value));
 }
 
@@ -389,7 +394,9 @@ string_constraintst string_to_lower_case_builtin_functiont::constraints(
       return if_exprt(is_upper_case(input[idx]), converted, non_converted);
     }();
     return string_constraintt(
-      idx, zero_if_negative(result.length()), conditional_convert);
+      idx,
+      zero_if_negative(array_pool.get_length(result)),
+      conditional_convert);
   }());
   return constraints;
 }
@@ -433,7 +440,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(result.length()),
+      zero_if_negative(array_pool.get_length(result)),
       equal_exprt(
         result[idx],
         if_exprt(is_lower_case(input[idx]), converted, input[idx])));
@@ -599,7 +606,7 @@ 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(result.length(), size_expr_with_sign);
+  return equal_exprt(array_pool.get_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,7 @@ class string_to_lower_case_builtin_functiont
   exprt length_constraint() const override
   {
     return and_exprt(
-      equal_exprt(result.length(), input.length()),
+      equal_exprt(array_pool.get_length(result), array_pool.get_length(input)),
       equal_exprt(return_code, from_integer(0, return_code.type())));
   };
 };
@@ -267,7 +267,7 @@ class string_to_upper_case_builtin_functiont
   exprt length_constraint() const override
   {
     return and_exprt(
-      equal_exprt(result.length(), input.length()),
+      equal_exprt(array_pool.get_length(result), array_pool.get_length(input)),
       equal_exprt(return_code, from_integer(0, return_code.type())));
   };
 };

src/solvers/strings/string_constraint_generator_code_points.cpp

@@ -43,10 +43,10 @@ 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(res.length(), 1));
+  implies_exprt a1(small, equal_to(array_pool.get_length(res), 1));
   constraints.existential.push_back(a1);
 
-  implies_exprt a2(not_exprt(small), equal_to(res.length(), 2));
+  implies_exprt a2(not_exprt(small), equal_to(array_pool.get_length(res), 2));
   constraints.existential.push_back(a2);
 
   typecast_exprt code_point_as_char(code_point, char_type);
@@ -166,10 +166,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_code_point_before(
   array_string_exprt str = get_string_expr(array_pool, args[0]);
   string_constraintst constraints;
 
-  const exprt &char1 =
-    str[minus_exprt(args[1], from_integer(2, str.length().type()))];
-  const exprt &char2 =
-    str[minus_exprt(args[1], from_integer(1, str.length().type()))];
+  const exprt &char1 = str[minus_exprt(
+    args[1], from_integer(2, array_pool.get_length(str).type()))];
+  const exprt &char2 = str[minus_exprt(
+    args[1], from_integer(1, array_pool.get_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

@@ -46,15 +46,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals(
   typet index_type = s1.length_type();
 
   // Axiom 1.
-  constraints.existential.push_back(
-    implies_exprt(eq, equal_exprt(s1.length(), s2.length())));
+  constraints.existential.push_back(implies_exprt(
+    eq, equal_exprt(array_pool.get_length(s1), array_pool.get_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(s1.length()),
+      zero_if_negative(array_pool.get_length(s1)),
       implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
   }());
 
@@ -63,12 +63,12 @@ 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, s1.length()),
+      binary_relation_exprt(witness, ID_lt, array_pool.get_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(s1.length(), s2.length()),
+      notequal_exprt(array_pool.get_length(s1), array_pool.get_length(s2)),
       equal_exprt(witness, from_integer(-1, index_type)));
     return implies_exprt(not_exprt(eq), or_exprt(diff_length, witnessing));
   }());
@@ -147,29 +147,32 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
   const exprt char_Z = from_integer('Z', char_type);
   const typet index_type = s1.length_type();
 
-  const implies_exprt a1(eq, equal_exprt(s1.length(), s2.length()));
+  const implies_exprt a1(
+    eq, equal_exprt(array_pool.get_length(s1), array_pool.get_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(s1.length()), implies_exprt(eq, constr2));
+    qvar,
+    zero_if_negative(array_pool.get_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, s1.length()),
+    binary_relation_exprt(witness, ID_lt, array_pool.get_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(s1.length(), s2.length()),
+      notequal_exprt(array_pool.get_length(s1), array_pool.get_length(s2)),
       and_exprt(bound_witness, witness_diff)));
   constraints.existential.push_back(a3);
 
@@ -203,12 +206,14 @@ 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(it.first.length(), str.length());
+    const notequal_exprt c2(
+      array_pool.get_length(it.first), array_pool.get_length(str));
     const and_exprt c3(
-      equal_exprt(it.first.length(), str.length()),
+      equal_exprt(array_pool.get_length(it.first), array_pool.get_length(str)),
       and_exprt(
         notequal_exprt(str[i], it.first[i]),
-        and_exprt(greater_than(str.length(), i), is_positive(i))));
+        and_exprt(
+          greater_than(array_pool.get_length(str), i), is_positive(i))));
     hash_constraints.existential.push_back(or_exprt(c1, or_exprt(c2, c3)));
   }
   return {hash, std::move(hash_constraints)};
@@ -250,13 +255,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_compare_to(
   const typet &index_type = s1.length_type();
 
   const equal_exprt res_null(res, from_integer(0, return_type));
-  const implies_exprt a1(res_null, equal_exprt(s1.length(), s2.length()));
+  const implies_exprt a1(
+    res_null,
+    equal_exprt(array_pool.get_length(s1), array_pool.get_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(s1.length()),
+    zero_if_negative(array_pool.get_length(s1)),
     implies_exprt(res_null, equal_exprt(s1[i], s2[i])));
   constraints.universal.push_back(a2);
 
@@ -268,20 +275,24 @@ std::pair<exprt, string_constraintst> add_axioms_for_compare_to(
   const equal_exprt ret_length_diff(
     res,
     minus_exprt(
-      typecast_exprt(s1.length(), return_type),
-      typecast_exprt(s2.length(), return_type)));
+      typecast_exprt(array_pool.get_length(s1), return_type),
+      typecast_exprt(array_pool.get_length(s2), return_type)));
   const or_exprt guard1(
     and_exprt(
-      less_than_or_equal_to(s1.length(), s2.length()),
-      greater_than(s1.length(), x)),
+      less_than_or_equal_to(
+        array_pool.get_length(s1), array_pool.get_length(s2)),
+      greater_than(array_pool.get_length(s1), x)),
     and_exprt(
-      greater_or_equal_to(s1.length(), s2.length()),
-      greater_than(s2.length(), x)));
+      greater_or_equal_to(array_pool.get_length(s1), array_pool.get_length(s2)),
+      greater_than(array_pool.get_length(s2), x)));
   const and_exprt cond1(ret_char_diff, guard1);
   const or_exprt guard2(
-    and_exprt(greater_than(s2.length(), s1.length()), equal_to(s1.length(), x)),
     and_exprt(
-      greater_than(s1.length(), s2.length()), equal_to(s2.length(), x)));
+      greater_than(array_pool.get_length(s2), array_pool.get_length(s1)),
+      equal_to(array_pool.get_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)));
   const and_exprt cond2(ret_length_diff, guard2);
 
   const implies_exprt a3(

src/solvers/strings/string_constraint_generator_concat.cpp

@@ -48,7 +48,8 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
   string_constraintst constraints;
   const typet &index_type = start_index.type();
   const exprt start1 = maximum(start_index, from_integer(0, index_type));
-  const exprt end1 = maximum(minimum(end_index, s2.length()), start1);
+  const exprt end1 =
+    maximum(minimum(end_index, array_pool.get_length(s2)), start1);
 
   // Axiom 1.
   constraints.existential.push_back(length_constraint_for_concat_substr(
@@ -58,16 +59,20 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
   constraints.universal.push_back([&] {
     const symbol_exprt idx = fresh_symbol("QA_index_concat", res.length_type());
     return string_constraintt(
-      idx, zero_if_negative(s1.length()), equal_exprt(s1[idx], res[idx]));
+      idx,
+      zero_if_negative(array_pool.get_length(s1)),
+      equal_exprt(s1[idx], res[idx]));
   }());
 
   // Axiom 3.
   constraints.universal.push_back([&] {
     const symbol_exprt idx2 =
       fresh_symbol("QA_index_concat2", res.length_type());
     const equal_exprt res_eq(
-      res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start1, idx2)]);
-    const minus_exprt upper_bound(res.length(), s1.length());
+      res[plus_exprt(idx2, array_pool.get_length(s1))],
+      s2[plus_exprt(start1, idx2)]);
+    const minus_exprt upper_bound(
+      array_pool.get_length(res), array_pool.get_length(s1));
     return string_constraintt(idx2, zero_if_negative(upper_bound), res_eq);
   }());
 
@@ -89,11 +94,13 @@ exprt length_constraint_for_concat_substr(
 {
   PRECONDITION(res.length_type().id() == ID_signedbv);
   const exprt start1 = maximum(start, from_integer(0, start.type()));
-  const exprt end1 = maximum(minimum(end, s2.length()), start1);
-  const plus_exprt res_length(s1.length(), minus_exprt(end1, start1));
+  const exprt end1 = maximum(minimum(end, array_pool.get_length(s2)), start1);
+  const plus_exprt res_length(
+    array_pool.get_length(s1), minus_exprt(end1, start1));
   const exprt overflow = sum_overflows(res_length);
   const exprt max_int = to_signedbv_type(res.length_type()).largest_expr();
-  return equal_exprt(res.length(), if_exprt(overflow, max_int, res_length));
+  return equal_exprt(
+    array_pool.get_length(res), if_exprt(overflow, max_int, res_length));
 }
 
 /// Add axioms enforcing that the length of `res` is that of the concatenation
@@ -104,7 +111,9 @@ exprt length_constraint_for_concat(
   const array_string_exprt &s2,
   array_poolt &array_pool)
 {
-  return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
+  return equal_exprt(
+    array_pool.get_length(res),
+    plus_exprt(array_pool.get_length(s1), array_pool.get_length(s2)));
 }
 
 /// Add axioms enforcing that the length of `res` is that of the concatenation
@@ -115,7 +124,8 @@ exprt length_constraint_for_concat_char(
   array_poolt &array_pool)
 {
   return equal_exprt(
-    res.length(), plus_exprt(s1.length(), from_integer(1, s1.length_type())));
+    array_pool.get_length(res),
+    plus_exprt(array_pool.get_length(s1), from_integer(1, s1.length_type())));
 }
 
 /// Add axioms enforcing that `res` is equal to the concatenation of `s1` and

src/solvers/strings/string_constraint_generator_constants.cpp

@@ -28,7 +28,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_constant(
   const exprt &guard)
 {
   string_constraintst constraints;
-  const typet &index_type = res.length().type();
+  const typet index_type = array_pool.get_length(res).type();
   const typet &char_type = res.content().type().subtype();
   std::string c_str = id2string(sval);
   std::wstring str;
@@ -53,7 +53,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_constant(
   const exprt s_length = from_integer(str.size(), index_type);
 
   constraints.existential.push_back(
-    implies_exprt(guard, equal_exprt(res.length(), s_length)));
+    implies_exprt(guard, equal_exprt(array_pool.get_length(res), s_length)));
   return {from_integer(0, get_return_code_type()), std::move(constraints)};
 }