From 470747aba0b94f6e327725d4461f0141af76b5da Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sun, 30 Nov 2025 13:57:30 +0000
Subject: [PATCH] Support reordered pointer operands in
 local_bitvector_analysis

`local_bitvector_analysist` previously assumed that pointer arithmetic
expressions with 3+ operands always have the pointer operand at position
`op0()`. We do not, however, have such a requirement anywhere, and even
if front-ends construct expressions this way then simplification may
re-order the operands.

Fixes: #2689
---
 .../local_bitvector_simplify/main.c           | 20 +++++++++++++++
 .../local_bitvector_simplify/test.desc        |  7 ++++++
 src/analyses/local_bitvector_analysis.cpp     | 25 ++++++++++++++++---
 3 files changed, 48 insertions(+), 4 deletions(-)
 create mode 100644 regression/goto-instrument/local_bitvector_simplify/main.c
 create mode 100644 regression/goto-instrument/local_bitvector_simplify/test.desc

diff --git a/regression/goto-instrument/local_bitvector_simplify/main.c b/regression/goto-instrument/local_bitvector_simplify/main.c
new file mode 100644
index 00000000000..c825ccfc14a
--- /dev/null
+++ b/regression/goto-instrument/local_bitvector_simplify/main.c
@@ -0,0 +1,20 @@
+// Test case for issue #2689
+// This test verifies that goto-instrument can analyze binaries
+// generated by goto-analyzer --simplify without assertion failures
+// in local_bitvector_analysis.cpp
+
+int array[10];
+
+int main()
+{
+  int *p = array;
+  // Pointer arithmetic that may be simplified in various ways
+  int *q = p + 1 + 2;     // This could be simplified to p + 3
+  int *r = p + 1 + 2 + 3; // Multiple additions
+
+  // Access through computed pointer
+  *q = 42;
+  *r = 43;
+
+  return 0;
+}
diff --git a/regression/goto-instrument/local_bitvector_simplify/test.desc b/regression/goto-instrument/local_bitvector_simplify/test.desc
new file mode 100644
index 00000000000..72c6002ba58
--- /dev/null
+++ b/regression/goto-instrument/local_bitvector_simplify/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--show-local-bitvector-analysis
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/src/analyses/local_bitvector_analysis.cpp b/src/analyses/local_bitvector_analysis.cpp
index 74f4137cbf0..7cd40f29536 100644
--- a/src/analyses/local_bitvector_analysis.cpp
+++ b/src/analyses/local_bitvector_analysis.cpp
@@ -173,10 +173,27 @@ local_bitvector_analysist::flagst local_bitvector_analysist::get_rec(
 
     if(plus_expr.operands().size() >= 3)
     {
-      DATA_INVARIANT(
-        plus_expr.op0().type().id() == ID_pointer,
-        "pointer in pointer-typed sum must be op0");
-      return get_rec(plus_expr.op0(), loc_info_src) | flagst::mk_uses_offset();
+      // In pointer arithmetic with 3+ operands, typically the pointer is op0,
+      // but simplification may reorder operands. Search for the pointer
+      // operand.
+      if(plus_expr.op0().type().id() == ID_pointer)
+      {
+        return get_rec(plus_expr.op0(), loc_info_src) |
+               flagst::mk_uses_offset();
+      }
+      else
+      {
+        // Search for pointer operand in remaining operands
+        for(const auto &op : plus_expr.operands())
+        {
+          if(op.type().id() == ID_pointer)
+          {
+            return get_rec(op, loc_info_src) | flagst::mk_uses_offset();
+          }
+        }
+        // No pointer operand found
+        return flagst::mk_unknown();
+      }
     }
     else if(plus_expr.operands().size() == 2)
     {