Handle non-byte-sized array element types in bounds_check_index

When the array element type has no byte size (e.g., arrays of
__CPROVER_integer), object_descriptor_exprt::build cannot compute byte
offsets. Fall back to a simple index-based lower-bound check instead of
crashing. The upper bound check uses the array size directly and does
not require byte offsets.

A DATA_INVARIANT ensures that arrays with non-byte-sized element types
are not accessed via pointer dereference, making explicit the assumption
that these arise only from internal modeling constructs.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: tautschnig

regression/cbmc/bounds_check_integer_index1/main.c

@@ -0,0 +1,8 @@
+int main()
+{
+  __CPROVER_integer arr[3];
+  __CPROVER_integer i;
+  __CPROVER_assume(i >= 0 && i < 3);
+  __CPROVER_integer x = arr[i];
+  __CPROVER_assert(1, "reachable");
+}

regression/cbmc/bounds_check_integer_index1/smt.desc

@@ -0,0 +1,10 @@
+CORE smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--bounds-check --smt2
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verify that bounds checking arrays with mathematical integer element types
+succeeds when using an SMT backend.

regression/cbmc/bounds_check_integer_index1/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--show-goto-functions
+^[[:space:]]*ASSERT.*lower bound in arr\[.*i\]$
+^[[:space:]]*ASSERT.*upper bound in arr\[.*i\]$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Bounds checking arrays with mathematical integer element types must not crash.
+The element type has no byte size, so the byte-offset-based lower-bound check
+is replaced by a simple index-based check. Both lower and upper bound checks
+must be generated.

regression/cbmc/bounds_check_integer_index1/verify.desc

@@ -0,0 +1,10 @@
+CORE broken-cprover-smt-backend no-new-smt
+main.c
+--bounds-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Verify that bounds checking arrays with mathematical integer element types
+completes verification successfully.

regression/validate-trace-xml-schema/check.py

@@ -71,6 +71,7 @@
     ['Bool', 'bool3.desc'],
     ['Empty_struct3', 'test.desc'],
     # uses show-goto-functions
+    ['bounds_check_integer_index1', 'test.desc'],
     ['reachability-slice', 'test.desc'],
     ['reachability-slice', 'test2.desc'],
     ['reachability-slice', 'test3.desc'],

src/ansi-c/goto-conversion/goto_check_c.cpp

@@ -1597,63 +1597,137 @@ void goto_check_ct::bounds_check_index(
   std::string name = array_name(expr.array());
 
   const exprt &index = expr.index();
-  object_descriptor_exprt ode;
-  ode.build(expr, ns);
 
-  if(index.type().id() != ID_unsignedbv)
-  {
-    // we undo typecasts to signedbv
+  // When the array element type has no byte size (e.g., __CPROVER_integer or
+  // arrays of unbounded arrays used in heap models),
+  // object_descriptor_exprt::build cannot compute byte offsets and produces an
+  // ID_unknown offset. Fall back to a simple index-based lower-bound check. We
+  // strip typecasts from integer/natural types to bitvector types so that the
+  // resulting assertions stay in the integer domain and can be handled by SMT
+  // solvers.
+  std::optional<object_descriptor_exprt> ode;
+  // effective_index is only used in the non-byte-sized path; it strips
+  // bitvector casts from integer/natural types to keep assertions in the
+  // integer domain.
+  exprt effective_index = index;
+  if(!size_of_expr(expr.type(), ns).has_value())
+  {
+    // Arrays with non-byte-sized element types arise from internal modeling
+    // constructs and should not be accessed via pointer dereference. Walk
+    // through member/index/typecast to find the root object.
+    const exprt *root = &expr.array();
+    while(root->id() == ID_member)
+      root = &to_member_expr(*root).compound();
+    while(root->id() == ID_index)
+      root = &to_index_expr(*root).array();
+    while(root->id() == ID_typecast)
+      root = &to_typecast_expr(*root).op();
+    DATA_INVARIANT(
+      root->id() != ID_dereference,
+      "arrays with non-byte-sized element types should not be accessed via "
+      "pointer dereference");
     if(
-      index.id() == ID_typecast &&
-      to_typecast_expr(index).op().type().id() == ID_unsignedbv)
+      effective_index.id() == ID_typecast &&
+      (to_typecast_expr(effective_index).op().type().id() == ID_integer ||
+       to_typecast_expr(effective_index).op().type().id() == ID_natural))
     {
-      // ok
+      effective_index = to_typecast_expr(effective_index).op();
     }
-    else
-    {
-      const auto i = numeric_cast<mp_integer>(index);
 
-      if(!i.has_value() || *i < 0)
+    if(
+      effective_index.type().id() != ID_unsignedbv &&
+      effective_index.type().id() != ID_natural)
+    {
+      // we undo typecasts to signedbv
+      if(
+        effective_index.id() == ID_typecast &&
+        to_typecast_expr(effective_index).op().type().id() == ID_unsignedbv)
+      {
+        // ok
+      }
+      else
       {
-        exprt effective_offset = ode.offset();
+        const auto i = numeric_cast<mp_integer>(effective_index);
 
-        if(ode.root_object().id() == ID_dereference)
+        if(!i.has_value() || *i < 0)
         {
-          exprt p_offset =
-            pointer_offset(to_dereference_expr(ode.root_object()).pointer());
+          exprt zero = from_integer(0, effective_index.type());
 
-          effective_offset = plus_exprt{
-            p_offset,
-            typecast_exprt::conditional_cast(
-              effective_offset, p_offset.type())};
+          binary_relation_exprt inequality(
+            effective_index, ID_ge, std::move(zero));
+
+          add_guarded_property(
+            inequality,
+            name + " lower bound",
+            "array bounds",
+            true, // fatal
+            expr.find_source_location(),
+            expr,
+            guard);
         }
+      }
+    }
+  }
+  else
+  {
+    ode.emplace();
+    ode->build(expr, ns);
 
-        exprt zero = from_integer(0, effective_offset.type());
+    if(index.type().id() != ID_unsignedbv)
+    {
+      // we undo typecasts to signedbv
+      if(
+        index.id() == ID_typecast &&
+        to_typecast_expr(index).op().type().id() == ID_unsignedbv)
+      {
+        // ok
+      }
+      else
+      {
+        const auto i = numeric_cast<mp_integer>(index);
 
-        // the final offset must not be negative
-        binary_relation_exprt inequality(
-          effective_offset, ID_ge, std::move(zero));
+        if(!i.has_value() || *i < 0)
+        {
+          exprt effective_offset = ode->offset();
 
-        add_guarded_property(
-          inequality,
-          name + " lower bound",
-          "array bounds",
-          true, // fatal
-          expr.find_source_location(),
-          expr,
-          guard);
+          if(ode->root_object().id() == ID_dereference)
+          {
+            exprt p_offset =
+              pointer_offset(to_dereference_expr(ode->root_object()).pointer());
+
+            effective_offset = plus_exprt{
+              p_offset,
+              typecast_exprt::conditional_cast(
+                effective_offset, p_offset.type())};
+          }
+
+          exprt zero = from_integer(0, effective_offset.type());
+
+          // the final offset must not be negative
+          binary_relation_exprt inequality(
+            effective_offset, ID_ge, std::move(zero));
+
+          add_guarded_property(
+            inequality,
+            name + " lower bound",
+            "array bounds",
+            true, // fatal
+            expr.find_source_location(),
+            expr,
+            guard);
+        }
       }
     }
   }
 
-  if(ode.root_object().id() == ID_dereference)
+  if(ode && ode->root_object().id() == ID_dereference)
   {
-    const exprt &pointer = to_dereference_expr(ode.root_object()).pointer();
+    const exprt &pointer = to_dereference_expr(ode->root_object()).pointer();
 
     const plus_exprt effective_offset{
-      ode.offset(),
+      ode->offset(),
       typecast_exprt::conditional_cast(
-        pointer_offset(pointer), ode.offset().type())};
+        pointer_offset(pointer), ode->offset().type())};
 
     binary_relation_exprt inequality{
       effective_offset,
@@ -1664,7 +1738,7 @@ void goto_check_ct::bounds_check_index(
     exprt in_bounds_of_some_explicit_allocation =
       is_in_bounds_of_some_explicit_allocation(
         pointer,
-        plus_exprt{ode.offset(), from_integer(1, ode.offset().type())});
+        plus_exprt{ode->offset(), from_integer(1, ode->offset().type())});
 
     or_exprt precond(
       std::move(in_bounds_of_some_explicit_allocation), inequality);
@@ -1694,7 +1768,7 @@ void goto_check_ct::bounds_check_index(
   {
   }
   else if(
-    expr.array().id() == ID_member &&
+    ode && expr.array().id() == ID_member &&
     (size == 0 || array_type.get_bool(ID_C_flexible_array_member)))
   {
     // a variable sized struct member
@@ -1706,13 +1780,31 @@ void goto_check_ct::bounds_check_index(
     // array (with the same element type) that would not make the structure
     // larger than the object being accessed; [...]
     const auto type_size_opt =
-      pointer_offset_size(ode.root_object().type(), ns);
+      pointer_offset_size(ode->root_object().type(), ns);
     CHECK_RETURN(type_size_opt.has_value());
 
     binary_relation_exprt inequality(
-      ode.offset(),
+      ode->offset(),
+      ID_lt,
+      from_integer(type_size_opt.value(), ode->offset().type()));
+
+    add_guarded_property(
+      inequality,
+      name + " upper bound",
+      "array bounds",
+      true, // fatal
+      expr.find_source_location(),
+      expr,
+      guard);
+  }
+  else if(!ode.has_value())
+  {
+    // non-byte-sized element type: use effective_index (which has bitvector
+    // casts stripped) and cast the size to match
+    binary_relation_exprt inequality{
+      effective_index,
       ID_lt,
-      from_integer(type_size_opt.value(), ode.offset().type()));
+      typecast_exprt::conditional_cast(size, effective_index.type())};
 
     add_guarded_property(
       inequality,