From 045c6855244016a45aa118bc1bb3ea1ad8123543 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 13 Dec 2023 14:11:16 +0000
Subject: [PATCH] Do not use back-end pointer encoding details in the
 simplifier

The object:offset encoding is an implementation detail that should be
private to the back-end. Expression simplification must not rely on such
details. Partly reverts 4d35274bd0a.
---
 src/util/simplify_expr_pointer.cpp | 18 ------------------
 unit/util/simplify_expr.cpp        | 21 ---------------------
 2 files changed, 39 deletions(-)

diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index b2255cd2e952..c482eb9b9617 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "arith_tools.h"
 #include "c_types.h"
-#include "config.h"
 #include "expr_util.h"
 #include "namespace.h"
 #include "pointer_expr.h"
@@ -400,23 +399,6 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
     {
       return from_integer(0, expr.type());
     }
-    else
-    {
-      // this is a pointer, we can't use to_integer
-      const auto width = to_pointer_type(ptr.type()).get_width();
-      mp_integer number = bvrep2integer(c_ptr.get_value(), width, false);
-      // a null pointer would have been caught above, return value 0
-      // will indicate that conversion failed
-      if(number==0)
-        return unchanged(expr);
-
-      // The constant address consists of OBJECT-ID || OFFSET.
-      mp_integer offset_bits =
-        *pointer_offset_bits(ptr.type(), ns) - config.bv_encoding.object_bits;
-      number%=power(2, offset_bits);
-
-      return from_integer(number, expr.type());
-    }
   }
 
   return unchanged(expr);
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index 756666240a69..8219df4f45f8 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -44,27 +44,6 @@ TEST_CASE("Simplify pointer_offset(address of array index)", "[core][util]")
   REQUIRE(offset_value==1);
 }
 
-TEST_CASE("Simplify const pointer offset", "[core][util]")
-{
-  config.set_arch("none");
-
-  symbol_tablet symbol_table;
-  namespacet ns(symbol_table);
-
-  // build a numeric constant of some pointer type
-  constant_exprt number=from_integer(1234, size_type());
-  number.type()=pointer_type(char_type());
-
-  exprt p_o=pointer_offset(number);
-
-  exprt simp=simplify_expr(p_o, ns);
-
-  REQUIRE(simp.is_constant());
-  const mp_integer offset_value =
-    numeric_cast_v<mp_integer>(to_constant_expr(simp));
-  REQUIRE(offset_value==1234);
-}
-
 TEST_CASE("Simplify byte extract", "[core][util]")
 {
   // this test does require a proper architecture to be set so that byte extract