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 4d35274.

Author: tautschnig

src/util/simplify_expr_pointer.cpp

@@ -10,7 +10,6 @@ Author: Daniel Kroening, [email protected]
 
 #include "arith_tools.h"
 #include "c_types.h"
-#include "config.h"
 #include "expr_util.h"
 #include "namespace.h"
 #include "pointer_expr.h"
@@ -403,23 +402,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);

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