Handle unsized 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.

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/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/validate-trace-xml-schema/check.py

@@ -70,6 +70,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,42 +1597,23 @@ 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)
+  // When the array element type has no byte size (e.g., 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.
+  std::optional<object_descriptor_exprt> ode;
+  if(!size_of_expr(expr.type(), ns).has_value())
   {
-    // we undo typecasts to signedbv
-    if(
-      index.id() == ID_typecast &&
-      to_typecast_expr(index).op().type().id() == ID_unsignedbv)
-    {
-      // ok
-    }
-    else
+    if(index.type().id() != ID_unsignedbv && index.type().id() != ID_natural)
     {
       const auto i = numeric_cast<mp_integer>(index);
 
       if(!i.has_value() || *i < 0)
       {
-        exprt effective_offset = ode.offset();
-
-        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());
+        exprt zero = from_integer(0, index.type());
 
-        // the final offset must not be negative
-        binary_relation_exprt inequality(
-          effective_offset, ID_ge, std::move(zero));
+        binary_relation_exprt inequality(index, ID_ge, std::move(zero));
 
         add_guarded_property(
           inequality,
@@ -1645,15 +1626,66 @@ void goto_check_ct::bounds_check_index(
       }
     }
   }
+  else
+  {
+    ode.emplace();
+    ode->build(expr, ns);
+
+    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);
+
+        if(!i.has_value() || *i < 0)
+        {
+          exprt effective_offset = ode->offset();
+
+          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 +1696,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 +1726,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 +1738,13 @@ 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()));
+      from_integer(type_size_opt.value(), ode->offset().type()));
 
     add_guarded_property(
       inequality,