From 40bca65b47ff938f5e19b89505596aef7c58b812 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 3 Feb 2025 11:09:46 +0000
Subject: [PATCH] Field sensitivity: account for array size in all index
 expressions

When code outside the core field-sensitivity implementation produces
index expressions we must not blindly turn such expressions into
ssa_exprt.
---
 regression/cbmc/field-sensitivity17/main.c    |  9 +++
 regression/cbmc/field-sensitivity17/test.desc | 12 ++++
 src/goto-symex/field_sensitivity.cpp          | 68 ++++++++++++++-----
 3 files changed, 72 insertions(+), 17 deletions(-)
 create mode 100644 regression/cbmc/field-sensitivity17/main.c
 create mode 100644 regression/cbmc/field-sensitivity17/test.desc

diff --git a/regression/cbmc/field-sensitivity17/main.c b/regression/cbmc/field-sensitivity17/main.c
new file mode 100644
index 00000000000..d4fe8fffc28
--- /dev/null
+++ b/regression/cbmc/field-sensitivity17/main.c
@@ -0,0 +1,9 @@
+union U
+{
+  unsigned char buf[2];
+} s;
+
+int main()
+{
+  __CPROVER_assert(s.buf[0] == 0, "");
+}
diff --git a/regression/cbmc/field-sensitivity17/test.desc b/regression/cbmc/field-sensitivity17/test.desc
new file mode 100644
index 00000000000..3ed4abdf906
--- /dev/null
+++ b/regression/cbmc/field-sensitivity17/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--max-field-sensitivity-array-size 1
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The test is a minimized version of code generated using Kani. It should pass
+irrespective of whether field sensitivity is applied to the array or not. (The
+original example was unexpectedly failing with an array size of 65, but passed
+with an array size of 64 or less.)
diff --git a/src/goto-symex/field_sensitivity.cpp b/src/goto-symex/field_sensitivity.cpp
index 1b3cd036f5c..0b8c2daa3c8 100644
--- a/src/goto-symex/field_sensitivity.cpp
+++ b/src/goto-symex/field_sensitivity.cpp
@@ -111,34 +111,68 @@ exprt field_sensitivityt::apply(
         const member_exprt member{tmp.get_original_expr(), comp};
         auto recursive_member =
           get_subexpression_at_offset(member, be.offset(), be.type(), ns);
-        if(
-          recursive_member.has_value() &&
-          (recursive_member->id() == ID_member ||
-           recursive_member->id() == ID_index))
+        if(!recursive_member.has_value())
+          continue;
+
+        // We need to inspect the access path as the resulting expression may
+        // involve index expressions. When array field sensitivity is disabled
+        // or the size of the array that is indexed into is larger than
+        // max_field_sensitivity_array_size then only the expression up to (but
+        // excluding) said index expression can be turned into an ssa_exprt.
+        exprt full_exprt = *recursive_member;
+        exprt *for_ssa = &full_exprt;
+        exprt *parent = for_ssa;
+        while(parent->id() == ID_typecast)
+          parent = &to_typecast_expr(*parent).op();
+        while(parent->id() == ID_member || parent->id() == ID_index)
         {
-          tmp.type() = be.type();
-          tmp.set_expression(*recursive_member);
+          if(parent->id() == ID_member)
+          {
+            parent = &to_member_expr(*parent).compound();
+          }
+          else
+          {
+            parent = &to_index_expr(*parent).array();
+#ifdef ENABLE_ARRAY_FIELD_SENSITIVITY
+            if(
+              !to_array_type(parent->type()).size().is_constant() ||
+              numeric_cast_v<mp_integer>(
+                to_constant_expr(to_array_type(parent->type()).size())) >
+                max_field_sensitivity_array_size)
+            {
+              for_ssa = parent;
+            }
+#else
+            for_ssa = parent;
+#endif // ENABLE_ARRAY_FIELD_SENSITIVITY
+          }
+        }
+
+        if(for_ssa->id() == ID_index || for_ssa->id() == ID_member)
+        {
+          tmp.type() = for_ssa->type();
+          tmp.set_expression(*for_ssa);
           if(was_l2)
           {
-            return apply(
-              ns, state, state.rename(std::move(tmp), ns).get(), write);
+            *for_ssa =
+              apply(ns, state, state.rename(std::move(tmp), ns).get(), write);
           }
           else
-            return apply(ns, state, std::move(tmp), write);
+            *for_ssa = apply(ns, state, std::move(tmp), write);
+
+          return full_exprt;
         }
-        else if(
-          recursive_member.has_value() && recursive_member->id() == ID_typecast)
+        else if(for_ssa->id() == ID_typecast)
         {
           if(was_l2)
           {
-            return apply(
-              ns,
-              state,
-              state.rename(std::move(*recursive_member), ns).get(),
-              write);
+            *for_ssa =
+              apply(ns, state, state.rename(*for_ssa, ns).get(), write);
           }
           else
-            return apply(ns, state, std::move(*recursive_member), write);
+            *for_ssa = apply(ns, state, std::move(*for_ssa), write);
+
+          return full_exprt;
         }
       }
     }