Merge pull request #4609 from allredj/array_string_exprt-length_type

Refactor: Introduce array_string_exprt.length_type() [TG-7439]

Author: Joel Allred

src/solvers/strings/string_builtin_function.cpp

@@ -182,7 +182,7 @@ optionalt<exprt> string_concat_char_builtin_functiont::eval(
   }();
   input_opt.value().push_back(char_val);
   const auto length =
-    from_integer(input_opt.value().size(), result.length().type());
+    from_integer(input_opt.value().size(), result.length_type());
   const array_typet type(result.type().subtype(), length);
   return make_string(input_opt.value(), type);
 }
@@ -200,7 +200,7 @@ string_constraintst string_concat_char_builtin_functiont::constraints(
   constraints.existential.push_back(length_constraint());
   constraints.universal.push_back([&] {
     const symbol_exprt idx =
-      generator.fresh_symbol("QA_index_concat_char", result.length().type());
+      generator.fresh_symbol("QA_index_concat_char", result.length_type());
     const exprt upper_bound = zero_if_negative(input.length());
     return string_constraintt(
       idx, upper_bound, equal_exprt(input[idx], result[idx]));
@@ -228,7 +228,7 @@ optionalt<exprt> string_set_char_builtin_functiont::eval(
   if(0 <= *position_opt && *position_opt < input_opt.value().size())
     input_opt.value()[numeric_cast_v<std::size_t>(*position_opt)] = *char_opt;
   const auto length =
-    from_integer(input_opt.value().size(), result.length().type());
+    from_integer(input_opt.value().size(), result.length_type());
   const array_typet type(result.type().subtype(), length);
   return make_string(input_opt.value(), type);
 }
@@ -275,7 +275,7 @@ 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_lt, from_integer(0, input.length().type())));
+      position, ID_lt, from_integer(0, input.length_type())));
   const exprt return_value = if_exprt(
     out_of_bounds,
     from_integer(1, return_code.type()),
@@ -308,7 +308,7 @@ optionalt<exprt> string_to_lower_case_builtin_functiont::eval(
       c += 0x20;
   }
   const auto length =
-    from_integer(input_opt.value().size(), result.length().type());
+    from_integer(input_opt.value().size(), result.length_type());
   const array_typet type(result.type().subtype(), length);
   return make_string(input_opt.value(), type);
 }
@@ -371,7 +371,7 @@ string_constraintst string_to_lower_case_builtin_functiont::constraints(
   constraints.existential.push_back(length_constraint());
   constraints.universal.push_back([&] {
     const symbol_exprt idx =
-      generator.fresh_symbol("QA_lower_case", result.length().type());
+      generator.fresh_symbol("QA_lower_case", result.length_type());
     const exprt conditional_convert = [&] {
       // The difference between upper-case and lower-case for the basic
       // latin and latin-1 supplement is 0x20.
@@ -400,7 +400,7 @@ optionalt<exprt> string_to_upper_case_builtin_functiont::eval(
       c -= 0x20;
   }
   const auto length =
-    from_integer(input_opt.value().size(), result.length().type());
+    from_integer(input_opt.value().size(), result.length_type());
   const array_typet type(result.type().subtype(), length);
   return make_string(input_opt.value(), type);
 }
@@ -421,7 +421,7 @@ string_constraintst string_to_upper_case_builtin_functiont::constraints(
   constraints.existential.push_back(length_constraint());
   constraints.universal.push_back([&] {
     const symbol_exprt idx =
-      fresh_symbol("QA_upper_case", result.length().type());
+      fresh_symbol("QA_upper_case", result.length_type());
     const typet &char_type = input.content().type().subtype();
     const exprt converted =
       minus_exprt(input[idx], from_integer(0x20, char_type));
@@ -480,7 +480,7 @@ optionalt<exprt> string_insertion_builtin_functiont::eval(
     });
 
   const auto result_value = eval(*input1_value, *input2_value, arg_values);
-  const auto length = from_integer(result_value.size(), result.length().type());
+  const auto length = from_integer(result_value.size(), result.length_type());
   const array_typet type(result.type().subtype(), length);
   return make_string(result_value, type);
 }
@@ -552,7 +552,7 @@ optionalt<exprt> string_of_int_builtin_functiont::eval(
     right_to_left_characters.emplace_back('-');
 
   const auto length = right_to_left_characters.size();
-  const auto length_expr = from_integer(length, result.length().type());
+  const auto length_expr = from_integer(length, result.length_type());
   const array_typet type(result.type().subtype(), length_expr);
   return make_string(
     right_to_left_characters.rbegin(), right_to_left_characters.rend(), type);
@@ -569,7 +569,7 @@ string_constraintst string_of_int_builtin_functiont::constraints(
 
 exprt string_of_int_builtin_functiont::length_constraint() const
 {
-  const typet &type = result.length().type();
+  const typet &type = result.length_type();
   const auto radix_opt = numeric_cast<std::size_t>(radix);
   const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2;
   const std::size_t upper_bound =

src/solvers/strings/string_constraint_generator_code_points.cpp

@@ -131,7 +131,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_code_point_at(
   const exprt &pos = f.arguments()[1];
 
   const symbol_exprt result = fresh_symbol("char", return_type);
-  const exprt index1 = from_integer(1, str.length().type());
+  const exprt index1 = from_integer(1, str.length_type());
   const exprt &char1 = str[pos];
   const exprt &char2 = str[plus_exprt(pos, index1)];
   const typecast_exprt char1_as_int(char1, return_type);

src/solvers/strings/string_constraint_generator_comparison.cpp

@@ -43,7 +43,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals(
   symbol_exprt eq = fresh_symbol("equal");
   typecast_exprt tc_eq(eq, f.type());
 
-  typet index_type = s1.length().type();
+  typet index_type = s1.length_type();
 
   // Axiom 1.
   constraints.existential.push_back(
@@ -145,7 +145,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_equals_ignore_case(
   const exprt char_a = from_integer('a', char_type);
   const exprt char_A = from_integer('A', char_type);
   const exprt char_Z = from_integer('Z', char_type);
-  const typet index_type = s1.length().type();
+  const typet index_type = s1.length_type();
 
   const implies_exprt a1(eq, equal_exprt(s1.length(), s2.length()));
   constraints.existential.push_back(a1);
@@ -193,7 +193,7 @@ string_constraint_generatort::add_axioms_for_hash_code(
   string_constraintst hash_constraints;
   const array_string_exprt str = get_string_expr(array_pool, f.arguments()[0]);
   const typet &return_type = f.type();
-  const typet &index_type = str.length().type();
+  const typet &index_type = str.length_type();
 
   auto pair = hash_code_of_string.insert(
     std::make_pair(str, fresh_symbol("hash", return_type)));
@@ -247,7 +247,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_compare_to(
   const array_string_exprt &s1 = get_string_expr(array_pool, f.arguments()[0]);
   const array_string_exprt &s2 = get_string_expr(array_pool, f.arguments()[1]);
   const symbol_exprt res = fresh_symbol("compare_to", return_type);
-  const typet &index_type = s1.length().type();
+  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()));

src/solvers/strings/string_constraint_generator_concat.cpp

@@ -54,16 +54,15 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_substr(
 
   // Axiom 2.
   constraints.universal.push_back([&] {
-    const symbol_exprt idx =
-      fresh_symbol("QA_index_concat", res.length().type());
+    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]));
   }());
 
   // Axiom 3.
   constraints.universal.push_back([&] {
     const symbol_exprt idx2 =
-      fresh_symbol("QA_index_concat2", res.length().type());
+      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());
@@ -85,12 +84,12 @@ exprt length_constraint_for_concat_substr(
   const exprt &start,
   const exprt &end)
 {
-  PRECONDITION(res.length().type().id() == ID_signedbv);
+  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 overflow = sum_overflows(res_length);
-  const exprt max_int = to_signedbv_type(res.length().type()).largest_expr();
+  const exprt max_int = to_signedbv_type(res.length_type()).largest_expr();
   return equal_exprt(res.length(), if_exprt(overflow, max_int, res_length));
 }
 
@@ -111,7 +110,7 @@ exprt length_constraint_for_concat_char(
   const array_string_exprt &s1)
 {
   return equal_exprt(
-    res.length(), plus_exprt(s1.length(), from_integer(1, s1.length().type())));
+    res.length(), plus_exprt(s1.length(), from_integer(1, s1.length_type())));
 }
 
 /// Add axioms enforcing that `res` is equal to the concatenation of `s1` and
@@ -129,7 +128,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat(
   const array_string_exprt &s1,
   const array_string_exprt &s2)
 {
-  exprt index_zero = from_integer(0, s2.length().type());
+  exprt index_zero = from_integer(0, s2.length_type());
   return add_axioms_for_concat_substr(
     fresh_symbol, res, s1, s2, index_zero, s2.length());
 }
@@ -150,7 +149,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_concat_code_point(
     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();
+  const typet &index_type = s1.length_type();
   const array_string_exprt code_point =
     array_pool.fresh_string(index_type, char_type);
   return combine_results(

src/solvers/strings/string_constraint_generator_float.cpp

@@ -210,7 +210,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_string_of_float(
   const floatbv_typet &type = to_floatbv_type(f.type());
   const ieee_float_spect float_spec(type);
   const typet &char_type = res.content().type().subtype();
-  const typet &index_type = res.length().type();
+  const typet &index_type = res.length_type();
 
   // We will look at the first 5 digits of the fractional part.
   // shifted is floor(f * 1e5)
@@ -264,7 +264,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
   string_constraintst constraints;
   const typet &type = int_expr.type();
   const typet &char_type = res.content().type().subtype();
-  const typet &index_type = res.length().type();
+  const typet &index_type = res.length_type();
   const exprt ten = from_integer(10, type);
   const exprt zero_char = from_integer('0', char_type);
   const exprt nine_char = from_integer('9', char_type);
@@ -292,7 +292,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
   {
     // after_end is |res| <= j
     binary_relation_exprt after_end(
-      res.length(), ID_le, from_integer(j, res.length().type()));
+      res.length(), ID_le, from_integer(j, res.length_type()));
     mult_exprt ten_sum(sum, ten);
 
     // sum = 10 * sum + after_end ? 0 : (res[j]-'0')
@@ -311,7 +311,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_fractional_part(
     if(j > 1)
     {
       not_exprt no_trailing_zero(and_exprt(
-        equal_exprt(res.length(), from_integer(j + 1, res.length().type())),
+        equal_exprt(res.length(), from_integer(j + 1, res.length_type())),
         equal_exprt(res[j], zero_char)));
       digit_constraints.push_back(no_trailing_zero);
     }
@@ -355,7 +355,7 @@ std::pair<exprt, string_constraintst> add_axioms_from_float_scientific_notation(
   const ieee_float_spect float_spec = ieee_float_spect::single_precision();
   const typet float_type = float_spec.to_type();
   const signedbv_typet int_type(32);
-  const typet &index_type = res.length().type();
+  const typet &index_type = res.length_type();
   const typet &char_type = res.content().type().subtype();
 
   // This is used for rounding float to integers.

src/solvers/strings/string_constraint_generator_format.cpp

@@ -245,12 +245,11 @@ static std::vector<format_elementt> parse_format_string(std::string s)
 static exprt is_null(const array_string_exprt &string)
 {
   return and_exprt{
-    equal_exprt{string.length(), from_integer(4, string.length().type())},
-    and_exprt{
-      equal_exprt{string[0], from_integer('n', string[0].type())},
-      equal_exprt{string[1], from_integer('u', string[0].type())},
-      equal_exprt{string[2], from_integer('l', string[0].type())},
-      equal_exprt{string[3], from_integer('l', string[0].type())}}};
+    equal_exprt{string.length(), from_integer(4, string.length_type())},
+    and_exprt{equal_exprt{string[0], from_integer('n', string[0].type())},
+              equal_exprt{string[1], from_integer('u', string[0].type())},
+              equal_exprt{string[2], from_integer('l', string[0].type())},
+              equal_exprt{string[3], from_integer('l', string[0].type())}}};
 }
 
 /// Parse `s` and add axioms ensuring the output corresponds to the output of
@@ -457,7 +456,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_format(
   std::vector<array_string_exprt> intermediary_strings;
   std::size_t arg_count = 0;
   const typet &char_type = res.content().type().subtype();
-  const typet &index_type = res.length().type();
+  const typet &index_type = res.length_type();
 
   for(const format_elementt &fe : format_strings)
   {

src/solvers/strings/string_constraint_generator_indexof.cpp

@@ -42,7 +42,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of(
   const exprt &from_index)
 {
   string_constraintst constraints;
-  const typet &index_type = str.length().type();
+  const typet &index_type = str.length_type();
   symbol_exprt index = fresh_symbol("index_of", index_type);
   symbol_exprt contains = fresh_symbol("contains_in_index_of");
 
@@ -115,7 +115,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
   const exprt &from_index)
 {
   string_constraintst constraints;
-  const typet &index_type = haystack.length().type();
+  const typet &index_type = haystack.length_type();
   symbol_exprt offset = fresh_symbol("index_of", index_type);
   symbol_exprt contains = fresh_symbol("contains_substring");
 
@@ -208,7 +208,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
   const exprt &from_index)
 {
   string_constraintst constraints;
-  const typet &index_type = haystack.length().type();
+  const typet &index_type = haystack.length_type();
   symbol_exprt offset = fresh_symbol("index_of", index_type);
   symbol_exprt contains = fresh_symbol("contains_substring");
 
@@ -295,7 +295,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_index_of(
   PRECONDITION(args.size() == 2 || args.size() == 3);
   const array_string_exprt str = get_string_expr(array_pool, args[0]);
   const exprt &c = args[1];
-  const typet &index_type = str.length().type();
+  const typet &index_type = str.length_type();
   const typet &char_type = str.content().type().subtype();
   PRECONDITION(f.type() == index_type);
   const exprt from_index =
@@ -349,7 +349,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
   const exprt &from_index)
 {
   string_constraintst constraints;
-  const typet &index_type = str.length().type();
+  const typet &index_type = str.length_type();
   const symbol_exprt index = fresh_symbol("last_index_of", index_type);
   const symbol_exprt contains = fresh_symbol("contains_in_last_index_of");
 
@@ -420,7 +420,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
   PRECONDITION(args.size() == 2 || args.size() == 3);
   const array_string_exprt str = get_string_expr(array_pool, args[0]);
   const exprt c = args[1];
-  const typet &index_type = str.length().type();
+  const typet &index_type = str.length_type();
   const typet &char_type = str.content().type().subtype();
   PRECONDITION(f.type() == index_type);
 

src/solvers/strings/string_constraint_generator_insert.cpp

@@ -38,10 +38,10 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
   const array_string_exprt &s2,
   const exprt &offset)
 {
-  PRECONDITION(offset.type() == s1.length().type());
+  PRECONDITION(offset.type() == s1.length_type());
 
   string_constraintst constraints;
-  const typet &index_type = s1.length().type();
+  const typet &index_type = s1.length_type();
   const exprt offset1 =
     maximum(from_integer(0, index_type), minimum(s1.length(), offset));
 
@@ -118,7 +118,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert(
     const exprt &start = f.arguments()[5];
     const exprt &end = f.arguments()[6];
     const typet &char_type = s1.content().type().subtype();
-    const typet &index_type = s1.length().type();
+    const typet &index_type = s1.length_type();
     const array_string_exprt substring =
       array_pool.fresh_string(index_type, char_type);
     return combine_results(
@@ -151,7 +151,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_int(
   const array_string_exprt res =
     array_pool.find(f.arguments()[1], f.arguments()[0]);
   const exprt &offset = f.arguments()[3];
-  const typet &index_type = s1.length().type();
+  const typet &index_type = s1.length_type();
   const typet &char_type = s1.content().type().subtype();
   const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
   return combine_results(
@@ -177,7 +177,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_bool(
   const array_string_exprt res =
     array_pool.find(f.arguments()[1], f.arguments()[0]);
   const exprt &offset = f.arguments()[3];
-  const typet &index_type = s1.length().type();
+  const typet &index_type = s1.length_type();
   const typet &char_type = s1.content().type().subtype();
   const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
   return combine_results(
@@ -202,7 +202,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
     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();
+  const typet &index_type = s1.length_type();
   const typet &char_type = s1.content().type().subtype();
   const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
   return combine_results(
@@ -230,7 +230,7 @@ std::pair<exprt, string_constraintst> add_axioms_for_insert_double(
     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();
+  const typet &index_type = s1.length_type();
   const typet &char_type = s1.content().type().subtype();
   const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
   return combine_results(