Simplify pointer_offset(constant)

Author: tautschnig

src/util/simplify_expr_pointer.cpp

@@ -375,14 +375,41 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
 
     return false;
   }
-  else if(ptr.id()==ID_constant &&
-          ptr.get(ID_value)==ID_NULL)
+  else if(ptr.id()==ID_constant)
   {
-    expr=from_integer(0, expr.type());
+    constant_exprt &c_ptr=to_constant_expr(ptr);
 
-    simplify_node(expr);
+    if(c_ptr.get_value()==ID_NULL ||
+       c_ptr.value_is_zero_string())
+    {
+      expr=from_integer(0, expr.type());
 
-    return false;
+      simplify_node(expr);
+
+      return false;
+    }
+    else
+    {
+      // this is a pointer, we can't use to_integer
+      mp_integer number=binary2integer(id2string(c_ptr.get_value()), false);
+      // a null pointer would have been caught above, return value 0
+      // will indicate that conversion failed
+      if(number==0)
+        return true;
+
+      // 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);
+
+      expr=from_integer(number, expr.type());
+
+      simplify_node(expr);
+
+      return false;
+    }
+
+    return true;
   }
 
   return true;

unit/Makefile

@@ -5,9 +5,6 @@ SRC = src/expr/require_expr.cpp \
       src/ansi-c/c_to_expr.cpp \
       unit_tests.cpp \
       catch_example.cpp \
-      util/expr_iterator.cpp \
-      analyses/call_graph.cpp \
-      java_bytecode/java_bytecode_convert_class/convert_abstract_class.cpp \
       # Empty last line
 
 # Test source files
@@ -23,8 +20,10 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
        solvers/refinement/string_constraint_generator_valueof/is_digit_with_radix.cpp \
        solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp \
-       solvers/refinement/string_refinement/substitute_array_list.cpp \
        solvers/refinement/string_refinement/concretize_array.cpp \
+       solvers/refinement/string_refinement/substitute_array_list.cpp \
+       util/expr_iterator.cpp \
+       util/simplify_expr.cpp \
        catch_example.cpp \
        # Empty last line
 

unit/util/simplify_expr.cpp

@@ -0,0 +1,56 @@
+/*******************************************************************\
+
+ Module: Unit tests of the expression simplifier
+
+ Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include <catch.hpp>
+
+#include <util/arith_tools.h>
+#include <util/c_types.h>
+#include <util/namespace.h>
+#include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+TEST_CASE("Simplify pointer_offset(address of array index)")
+{
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  array_typet array_type(char_type(), from_integer(2, size_type()));
+  symbol_exprt array("A", array_type);
+  index_exprt index(array, from_integer(1, index_type()));
+  address_of_exprt address_of(index);
+
+  exprt p_o=pointer_offset(address_of);
+
+  exprt simp=simplify_expr(p_o, ns);
+
+  REQUIRE(simp.id()==ID_constant);
+  mp_integer offset_value;
+  REQUIRE(!to_integer(simp, offset_value));
+  REQUIRE(offset_value==1);
+}
+
+TEST_CASE("Simplify const pointer offset")
+{
+  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.id()==ID_constant);
+  mp_integer offset_value;
+  REQUIRE(!to_integer(simp, offset_value));
+  REQUIRE(offset_value==1234);
+}