SMT2: disambiguate element-address functions by index type

regression/cprover/element_address_index_type/main.c

@@ -0,0 +1,20 @@
+int a[10];
+
+int main()
+{
+  int i, j;
+
+  // Two element_address expressions that share a result (pointer) type. The
+  // SMT2 helper function emitted for ID_element_address is named after both
+  // the result type and the index type, so the index type must appear in the
+  // declare-fun name. This guards the disambiguation: without it the name
+  // would be keyed on the result type alone, and two such expressions with
+  // differing index sorts would reuse one name with mismatched argument
+  // sorts, which a solver rejects.
+  int x = a[i];
+  int y = a[j];
+
+  __CPROVER_assert(x == y, "x equals y");
+
+  return 0;
+}

regression/cprover/element_address_index_type/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--smt2 --inline
+^EXIT=0$
+^SIGNAL=0$
+^\(declare-fun element-address-p\d+_s\d+ \(
+--
+^\(declare-fun element-address-p\d+ \(

src/solvers/smt2/smt2_conv.cpp

@@ -1163,8 +1163,14 @@ std::string smt2_convt::type2id(const typet &type) const
   {
     return "A" + type2id(to_array_type(type).element_type());
   }
+  else if(type.id() == ID_c_enum)
+  {
+    // mirror convert_type, which uses the underlying bitvector type
+    return type2id(to_c_enum_type(type).underlying_type());
+  }
   else if(type.id() == ID_integer)
   {
+    // unbounded mathematical integers map to the SMT `Int` sort
     return "Int";
   }
   else if(type.id() == ID_real)
@@ -1248,6 +1254,18 @@ void smt2_convt::convert_string_literal(const std::string &s)
   out << '"';
 }
 
+/// True if \p type is an integer-sorted index type for which the
+/// element-address size/offset arithmetic can be carried out directly. This is
+/// the single source of truth shared by the application site (convert_expr) and
+/// the declaration site (find_symbols) for ID_element_address, so that the
+/// element-size argument sort cannot drift between the two.
+static bool is_integer_index_type(const typet &type)
+{
+  return type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+         type.id() == ID_bv || type.id() == ID_integer ||
+         type.id() == ID_c_enum || type.id() == ID_c_enum_tag;
+}
+
 void smt2_convt::convert_expr(const exprt &expr)
 {
   // try hash table first
@@ -1956,15 +1974,31 @@ void smt2_convt::convert_expr(const exprt &expr)
 
     auto element_size_expr_opt =
       ::size_of_expr(element_address_expr.element_type(), ns);
-    CHECK_RETURN(element_size_expr_opt.has_value());
-
-    out << "(element-address-" << type2id(expr.type()) << ' ';
+    // The element-size argument must have an integer sort for the offset
+    // arithmetic to type-check. Two independent adjustments are made so that
+    // mathematical or non-integer-indexed heap arrays (as emitted by the
+    // Strata encoding) can still be expressed:
+    //   - the size *value* falls back to 1 when the element type has no
+    //     computable byte size (e.g. an incomplete or mathematical type);
+    //   - the size *sort* falls back to c_index_type() when the index type is
+    //     not itself an integer sort, rather than using the index type.
+    // Both adjustments are mirrored in the declaration in find_symbols().
+    const typet &idx_t = element_address_expr.index().type();
+    const typet size_target =
+      is_integer_index_type(idx_t) ? idx_t : c_index_type();
+    const exprt element_size_expr =
+      element_size_expr_opt.has_value()
+        ? *element_size_expr_opt
+        : static_cast<exprt>(from_integer(1, size_target));
+
+    out << "(element-address-" << type2id(expr.type()) << '_' << type2id(idx_t)
+        << ' ';
     convert_expr(element_address_expr.base());
     out << ' ';
     convert_expr(element_address_expr.index());
     out << ' ';
-    convert_expr(typecast_exprt::conditional_cast(
-      *element_size_expr_opt, element_address_expr.index().type()));
+    convert_expr(
+      typecast_exprt::conditional_cast(element_size_expr, size_target));
     out << ')';
   }
   else if(expr.id() == ID_field_address)
@@ -3505,6 +3539,40 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
       convert_expr(src);
       out <<" 1 0)";
     }
+    else if(
+      src_type.id() == ID_unsignedbv || src_type.id() == ID_c_bool ||
+      src_type.id() == ID_bv)
+    {
+      // unsigned bit-vector to integer: bv2nat gives the unsigned value
+      out << "(bv2nat ";
+      convert_expr(src);
+      out << ')';
+    }
+    else if(src_type.id() == ID_signedbv)
+    {
+      // signed bit-vector to integer: bv2nat gives the unsigned value; when
+      // the sign bit is set, subtract 2^width to obtain the signed value.
+      const std::size_t width = to_signedbv_type(src_type).get_width();
+      out << "(let ((?bvtoint ";
+      convert_expr(src);
+      out << ")) (- (bv2nat ?bvtoint) (* (bv2nat ((_ extract " << width - 1
+          << ' ' << width - 1 << ") ?bvtoint)) " << power(2, width) << ")))";
+    }
+    else if(src_type.id() == ID_c_enum)
+    {
+      // convert via the underlying (bit-vector) type
+      convert_typecast(typecast_exprt{
+        typecast_exprt{src, to_c_enum_type(src_type).underlying_type()},
+        dest_type});
+    }
+    else if(src_type.id() == ID_c_enum_tag)
+    {
+      // convert via the underlying (bit-vector) type
+      convert_typecast(typecast_exprt{
+        typecast_exprt{
+          src, ns.follow_tag(to_c_enum_tag_type(src_type)).underlying_type()},
+        dest_type});
+    }
     else
       UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> integer");
   }
@@ -6250,7 +6318,8 @@ void smt2_convt::find_symbols(const exprt &expr)
   }
   else if(expr.id() == ID_element_address)
   {
-    irep_idt function = "element-address-" + type2id(expr.type());
+    irep_idt function = "element-address-" + type2id(expr.type()) + "_" +
+                        type2id(to_element_address_expr(expr).index().type());
 
     if(state_fkt_declared.insert(function).second)
     {
@@ -6259,7 +6328,13 @@ void smt2_convt::find_symbols(const exprt &expr)
       out << ' ';
       convert_type(to_element_address_expr(expr).index().type());
       out << ' '; // repeat, for the element size
-      convert_type(to_element_address_expr(expr).index().type());
+      // The element-size argument sort must match the one chosen at the
+      // application site in convert_expr(): for non-integer index types we
+      // emit c_index_type() rather than the index type itself.
+      convert_type(
+        is_integer_index_type(to_element_address_expr(expr).index().type())
+          ? to_element_address_expr(expr).index().type()
+          : c_index_type());
       out << ") ";
       convert_type(expr.type()); // return type
       out << ")\n";              // declare-fun

unit/solvers/smt2/smt2_conv.cpp

@@ -7,19 +7,23 @@
 #include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/message.h>
 #include <util/namespace.h>
+#include <util/pointer_expr.h>
 #include <util/std_expr.h>
 #include <util/symbol_table.h>
 
 #include <solvers/smt2/smt2_conv.h>
 #include <solvers/smt2/smt2_dec.h>
 #include <testing-utils/use_catch.h>
 
+#include <vector>
+
 TEST_CASE(
   "smt2_convt::convert_identifier character escaping.",
   "[core][solvers][smt2]")
@@ -615,3 +619,111 @@ TEST_CASE(
   REQUIRE(operands_map.size() == 1);
   REQUIRE(operands_map.count(-1) == 1);
 }
+
+/// Collect every "(declare-fun element-address-... )" name emitted while
+/// converting \p expr.
+static std::vector<std::string> element_address_declarations(const exprt &expr)
+{
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+  std::ostringstream out;
+  smt2_convt conv(
+    ns, "test", "", "QF_AUFBV", smt2_convt::solvert::GENERIC, out);
+  conv.set_to(expr, true);
+
+  std::vector<std::string> names;
+  const std::string &s = out.str();
+  const std::string marker = "(declare-fun element-address-";
+  for(std::size_t pos = s.find(marker); pos != std::string::npos;
+      pos = s.find(marker, pos + 1))
+  {
+    const std::size_t name_start = pos + std::string("(declare-fun ").size();
+    const std::size_t name_end = s.find(' ', name_start);
+    names.push_back(s.substr(name_start, name_end - name_start));
+  }
+  return names;
+}
+
+/// Full SMT2 emitted while converting \p expr.
+static std::string element_address_smt2(const exprt &expr)
+{
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+  std::ostringstream out;
+  smt2_convt conv(
+    ns, "test", "", "QF_AUFBV", smt2_convt::solvert::GENERIC, out);
+  conv.set_to(expr, true);
+  return out.str();
+}
+
+TEST_CASE(
+  "smt2_convt element-address disambiguation by index type",
+  "[core][solvers][smt2]")
+{
+  // Two element_address expressions that share a result (pointer) type but
+  // differ in index type must be declared as two distinct functions, so that
+  // the declared and applied argument sorts never disagree.
+  config.ansi_c.mode = configt::ansi_ct::flavourt::GCC;
+  config.ansi_c.set_arch_spec_x86_64(); // populate type widths (pointer etc.)
+  const pointer_typet result_type = pointer_type(signedbv_typet{32});
+  const symbol_exprt base{"b", result_type};
+
+  SECTION("distinct bit-vector index widths yield distinct names")
+  {
+    const element_address_exprt ea32{
+      base, symbol_exprt{"i32", signedbv_typet{32}}, result_type};
+    const element_address_exprt ea64{
+      base, symbol_exprt{"i64", signedbv_typet{64}}, result_type};
+
+    const auto names = element_address_declarations(equal_exprt{ea32, ea64});
+
+    REQUIRE(names.size() == 2);
+    REQUIRE(names[0] != names[1]);
+    // the index type is part of the name (suffix after the result type)
+    const bool has_s32 = names[0].find("_s32") != std::string::npos ||
+                         names[1].find("_s32") != std::string::npos;
+    const bool has_s64 = names[0].find("_s64") != std::string::npos ||
+                         names[1].find("_s64") != std::string::npos;
+    REQUIRE(has_s32);
+    REQUIRE(has_s64);
+  }
+
+  SECTION("mathematical integer index is supported (Strata path)")
+  {
+    // An unbounded-integer index with a mathematical element type is exactly
+    // the case the size fallback targets: size_of() yields nothing, so a unit
+    // size is built directly in the integer index type. type2id must render
+    // the integer index type for the name rather than aborting via
+    // UNREACHABLE.
+    const pointer_typet math_result_type = pointer_type(integer_typet{});
+    const element_address_exprt ea_int_i{
+      base, symbol_exprt{"i", integer_typet{}}, math_result_type};
+    const element_address_exprt ea_int_j{
+      base, symbol_exprt{"j", integer_typet{}}, math_result_type};
+
+    const auto names =
+      element_address_declarations(equal_exprt{ea_int_i, ea_int_j});
+
+    // both share the index type, so a single function is declared for them
+    REQUIRE(names.size() == 1);
+    REQUIRE(names[0].find("_Int") != std::string::npos);
+  }
+
+  SECTION("integer index with a bit-vector-sized element uses bv2nat")
+  {
+    // An integer index combined with a bit-vector element type: size_of()
+    // yields a bit-vector byte size that must be converted to the integer
+    // size sort. This exercises the bit-vector -> Int typecast (bv2nat); it
+    // previously aborted in convert_typecast.
+    const element_address_exprt ea_i{
+      base, symbol_exprt{"i", integer_typet{}}, result_type};
+    const element_address_exprt ea_j{
+      base, symbol_exprt{"j", integer_typet{}}, result_type};
+
+    const std::string smt2 = element_address_smt2(equal_exprt{ea_i, ea_j});
+
+    // the byte size (a bit-vector) is converted to the integer index sort
+    REQUIRE(smt2.find("bv2nat") != std::string::npos);
+    REQUIRE(smt2.find("(declare-fun element-address-") != std::string::npos);
+  }
+}