From b8c6b400cc56416fa50dd9590e36f4b86e87c0be Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 30 Jan 2025 11:50:35 +0000
Subject: [PATCH 1/2] Value-set based dereferencing: fix simplified handling of
 *(p + i)

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
---
 regression/cbmc/Pointer_array8/main.c         | 21 +++++++++++++++++++
 regression/cbmc/Pointer_array8/test.desc      |  8 +++++++
 .../cbmc/array-cell-sensitivity15/test.desc   |  3 +--
 .../value_set_dereference.cpp                 |  1 +
 4 files changed, 31 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc/Pointer_array8/main.c
 create mode 100644 regression/cbmc/Pointer_array8/test.desc

diff --git a/regression/cbmc/Pointer_array8/main.c b/regression/cbmc/Pointer_array8/main.c
new file mode 100644
index 00000000000..af34389773c
--- /dev/null
+++ b/regression/cbmc/Pointer_array8/main.c
@@ -0,0 +1,21 @@
+#pragma pack(push)
+#pragma pack(1)
+typedef struct
+{
+  int data[2];
+} arr;
+
+typedef struct
+{
+  arr vec[2];
+} arrvec;
+#pragma pack(pop)
+
+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, "");
+}
diff --git a/regression/cbmc/Pointer_array8/test.desc b/regression/cbmc/Pointer_array8/test.desc
new file mode 100644
index 00000000000..1c039664a91
--- /dev/null
+++ b/regression/cbmc/Pointer_array8/test.desc
@@ -0,0 +1,8 @@
+CORE no-new-smt
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/array-cell-sensitivity15/test.desc b/regression/cbmc/array-cell-sensitivity15/test.desc
index 84c4b927b7c..aa3f0c590da 100644
--- a/regression/cbmc/array-cell-sensitivity15/test.desc
+++ b/regression/cbmc/array-cell-sensitivity15/test.desc
@@ -3,9 +3,8 @@ access.c
 --program-only
 ^EXIT=0$
 ^SIGNAL=0$
-s!0@1#2\.\.n == \{ s!0@1#1\.\.n\[\[0\]\], s!0@1#1\.\.n\[\[1\]\], s!0@1#1\.\.n\[\[2\]\], s!0@1#1\.\.n\[\[3\]\] } WITH \[\(.*\)i!0@1#2:=k!0@1#1\]
+s!0@1#2\.\.n ==.*\{ s!0@1#1\.\.n\[\[0\]\], s!0@1#1\.\.n\[\[1\]\], s!0@1#1\.\.n\[\[2\]\], s!0@1#1\.\.n\[\[3\]\] \}
 --
-byte_update
 --
 This tests applying field-sensitivity to a pointer to an array that is part of a struct. See cbmc issue #5397 and PR #5418 for more detail.
 Disabled for paths-lifo mode, which does not support --program-only.
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 3af8d4b72b1..dd17eced5e6 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -196,6 +196,7 @@ exprt value_set_dereferencet::dereference(
 
     if(
       can_cast_type<pointer_typet>(pointer_expr.type()) &&
+      pointer_expr.id() != ID_typecast &&
       !can_cast_type<pointer_typet>(offset_expr.type()) &&
       !can_cast_expr<constant_exprt>(offset_expr))
     {

From 164407fa49153536a77ad59ca4eec18f5adae0bc Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 9 Feb 2025 14:32:06 +0100
Subject: [PATCH 2/2] get_subexpression_at_offset: remove infeasible branch

The outer decision already ensures that types match, so replacing types
cannot be necessary.
---
 src/util/pointer_offset_size.cpp | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index 22c9acba5b6..e39b355fd86 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -564,14 +564,7 @@ std::optional<exprt> get_subexpression_at_offset(
   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 &&