Value-set based dereferencing must consider possible index expressions

Value-set based dereferencing must not take an access path through an
object that precludes a subsequent index expression from accessing a
different part of the object. Such a situation can arise when the value
set has a known (constant) offset for the pointer that would identify
one particular element in an array (within that object). The code using
value-set based dereferencing, however, may be trying to resolve a
subexpression of an index expression, where said index expression would
lead to a different element that may itself be part of a different array
within the same overall object.

Fixes: #8570

Author: tautschnig

regression/cbmc/Pointer_array7/main.c

@@ -18,8 +18,8 @@ int main()
   uint16_t x[2];
   x[0] = 1;
   x[1] = 2;
-  uint8_t *y = (uint8_t *)x;
-  uint16_t z = *((uint16_t *)(y + 1));
+  uint8_t *y = (uint8_t *)x + 1;
+  uint16_t z = *((uint16_t *)(y));
 
 #ifdef USE_BIG_ENDIAN
   assert(z == 256u);

regression/cbmc/Pointer_array8/main.c

@@ -0,0 +1,18 @@
+typedef struct __attribute__((packed))
+{
+  int data[2];
+} arr;
+
+typedef struct __attribute__((packed))
+{
+  arr vec[2];
+} arrvec;
+
+int main()
+{
+  arrvec A;
+  arrvec *x = &A;
+  __CPROVER_assume(x->vec[1].data[0] < 42);
+  unsigned k;
+  __CPROVER_assert(k != 2 || ((int *)x)[k] < 42, "");
+}

regression/cbmc/Pointer_array8/test.desc

@@ -0,0 +1,8 @@
+CORE no-new-smt
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/goto-programs/rewrite_union.cpp

@@ -159,6 +159,7 @@ static bool restore_union_rec(exprt &expr, const namespacet &ns)
             member_exprt{be.op(), comp.get_name(), comp.type()},
             be.offset(),
             be.type(),
+            true,
             ns);
           if(result.has_value())
           {

src/goto-symex/field_sensitivity.cpp

@@ -110,7 +110,7 @@ exprt field_sensitivityt::apply(
         tmp.remove_level_2();
         const member_exprt member{tmp.get_original_expr(), comp};
         auto recursive_member =
-          get_subexpression_at_offset(member, be.offset(), be.type(), ns);
+          get_subexpression_at_offset(member, be.offset(), be.type(), true, ns);
         if(
           recursive_member.has_value() &&
           (recursive_member->id() == ID_member ||

src/memory-analyzer/analyze_symbol.cpp

@@ -327,6 +327,7 @@ exprt gdb_value_extractort::get_pointer_to_member_value(
     struct_symbol_expr,
     member_offset,
     to_pointer_type(expr.type()).base_type(),
+    true,
     ns);
   DATA_INVARIANT(
     maybe_member_expr.has_value(), "structure doesn't have member");
@@ -554,7 +555,11 @@ exprt gdb_value_extractort::get_pointer_value(
     if(target_expr.type().id() == ID_array)
     {
       const auto result_indexed_expr = get_subexpression_at_offset(
-        target_expr, 0, to_pointer_type(zero_expr.type()).base_type(), ns);
+        target_expr,
+        0,
+        to_pointer_type(zero_expr.type()).base_type(),
+        true,
+        ns);
       CHECK_RETURN(result_indexed_expr.has_value());
       if(result_indexed_expr->type() == zero_expr.type())
         return *result_indexed_expr;

src/pointer-analysis/value_set_dereference.cpp

@@ -643,11 +643,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       }
     }
 
-    // try to build a member/index expression - do not use byte_extract
+    // Try to build a member/index expression instead of using byte_extract;
+    // don't recurse into aggregate types as the caller's expression may be
+    // within an index expression, i.e., a further offset beyond o.offset() may
+    // get added on to it.
     auto subexpr = get_subexpression_at_offset(
-      root_object, o.offset(), dereference_type, ns);
-    if(subexpr.has_value())
-      simplify(subexpr.value(), ns);
+      root_object, o.offset(), dereference_type, false, ns);
     if(
       subexpr.has_value() &&
       subexpr.value().id() != ID_byte_extract_little_endian &&

src/solvers/flattening/pointer_logic.cpp

@@ -115,7 +115,7 @@ exprt pointer_logict::pointer_expr(
     }
   }
   auto deep_object_opt =
-    get_subexpression_at_offset(object_expr, pointer.offset, subtype, ns);
+    get_subexpression_at_offset(object_expr, pointer.offset, subtype, true, ns);
   CHECK_RETURN(deep_object_opt.has_value());
   exprt deep_object = deep_object_opt.value();
   simplify(deep_object, ns);

src/util/pointer_offset_size.cpp

@@ -561,17 +561,11 @@ std::optional<exprt> get_subexpression_at_offset(
   const exprt &expr,
   const mp_integer &offset_bytes,
   const typet &target_type_raw,
+  bool recurse_into_arrays,
   const namespacet &ns)
 {
   if(offset_bytes == 0 && expr.type() == target_type_raw)
-  {
-    exprt result = expr;
-
-    if(expr.type() != target_type_raw)
-      result.type() = target_type_raw;
-
-    return result;
-  }
+    return expr;
 
   if(
     offset_bytes == 0 && expr.type().id() == ID_pointer &&
@@ -611,6 +605,7 @@ std::optional<exprt> get_subexpression_at_offset(
           member,
           offset_bytes - m_offset_bits / config.ansi_c.char_width,
           target_type_raw,
+          recurse_into_arrays,
           ns);
       }
 
@@ -638,9 +633,18 @@ std::optional<exprt> get_subexpression_at_offset(
       const auto offset_inside_elem = offset_bytes % elem_size_bytes;
       const auto target_size_bytes =
         *target_size_bits / config.ansi_c.char_width;
-      // only recurse if the cell completely contains the target
       if(
-        index < array_size &&
+        index < array_size && array_type.element_type() == target_type_raw &&
+        offset_inside_elem == 0)
+      {
+        return index_exprt{
+          expr,
+          from_integer(
+            offset_bytes / elem_size_bytes, array_type.index_type())};
+      }
+      // only recurse if the cell completely contains the target
+      else if(
+        recurse_into_arrays && index < array_size &&
         offset_inside_elem + target_size_bytes <= elem_size_bytes)
       {
         return get_subexpression_at_offset(
@@ -650,6 +654,7 @@ std::optional<exprt> get_subexpression_at_offset(
               offset_bytes / elem_size_bytes, array_type.index_type())),
           offset_inside_elem,
           target_type_raw,
+          recurse_into_arrays,
           ns);
       }
     }
@@ -676,7 +681,7 @@ std::optional<exprt> get_subexpression_at_offset(
       {
         const member_exprt member(expr, component.get_name(), component.type());
         return get_subexpression_at_offset(
-          member, offset_bytes, target_type_raw, ns);
+          member, offset_bytes, target_type_raw, recurse_into_arrays, ns);
       }
     }
   }
@@ -689,12 +694,16 @@ std::optional<exprt> get_subexpression_at_offset(
   const exprt &expr,
   const exprt &offset,
   const typet &target_type,
+  bool recurse_into_arrays,
   const namespacet &ns)
 {
   const auto offset_bytes = numeric_cast<mp_integer>(offset);
 
   if(!offset_bytes.has_value())
     return {};
   else
-    return get_subexpression_at_offset(expr, *offset_bytes, target_type, ns);
+  {
+    return get_subexpression_at_offset(
+      expr, *offset_bytes, target_type, recurse_into_arrays, ns);
+  }
 }

src/util/pointer_offset_size.h

@@ -56,12 +56,14 @@ std::optional<exprt> get_subexpression_at_offset(
   const exprt &expr,
   const mp_integer &offset,
   const typet &target_type,
+  bool recurse_into_arrays,
   const namespacet &ns);
 
 std::optional<exprt> get_subexpression_at_offset(
   const exprt &expr,
   const exprt &offset,
   const typet &target_type,
+  bool recurse_into_arrays,
   const namespacet &ns);
 
 #endif // CPROVER_UTIL_POINTER_OFFSET_SIZE_H