From e140d162b650bb3f8246d8f614ef16d94b84d846 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 10 Oct 2018 11:00:58 +0000
Subject: [PATCH] Include pointer offset in counterexample output

While the bit-level pointer output would convey the information, the
human-readable expression previously did not consider non-zero offsets except
for null pointers.
---
 .../cbmc/trace_address_arithmetic1/main.c     | 22 ++++++++++++
 .../cbmc/trace_address_arithmetic1/test.desc  | 10 ++++++
 src/solvers/flattening/pointer_logic.cpp      | 36 ++++++++++++-------
 3 files changed, 56 insertions(+), 12 deletions(-)
 create mode 100644 regression/cbmc/trace_address_arithmetic1/main.c
 create mode 100644 regression/cbmc/trace_address_arithmetic1/test.desc

diff --git a/regression/cbmc/trace_address_arithmetic1/main.c b/regression/cbmc/trace_address_arithmetic1/main.c
new file mode 100644
index 00000000000..6419633009a
--- /dev/null
+++ b/regression/cbmc/trace_address_arithmetic1/main.c
@@ -0,0 +1,22 @@
+#include <assert.h>
+
+typedef struct
+{
+  int inta;
+  int intb;
+} struct_t;
+
+typedef union {
+  int intaa;
+  struct_t structbb;
+} union_struct_t;
+
+int main()
+{
+  union_struct_t uuu;
+  char *ptr = (char *)&uuu.structbb.intb;
+  int A[2];
+  int *ip = &A[1];
+  uuu.structbb.intb = 1;
+  assert(0);
+}
diff --git a/regression/cbmc/trace_address_arithmetic1/test.desc b/regression/cbmc/trace_address_arithmetic1/test.desc
new file mode 100644
index 00000000000..e66bc70c19f
--- /dev/null
+++ b/regression/cbmc/trace_address_arithmetic1/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--trace
+^EXIT=10$
+^SIGNAL=0$
+ptr=\(char \*\)&uuu!0@1 \+ 4(l+)? \(.*\)$
+ip=A!0@1 \+ 1(l+)? \(.*\)$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index ac2980e95d0..55872a3ff3b 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -17,6 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
 #include <util/prefix.h>
+#include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
 bool pointer_logict::is_dynamic_object(const exprt &expr) const
@@ -104,29 +105,40 @@ exprt pointer_logict::pointer_expr(
   // https://gcc.gnu.org/onlinedocs/gcc-4.8.0/gcc/Pointer-Arith.html
   if(subtype.id() == ID_empty)
     subtype = char_type();
-  const exprt deep_object =
+  exprt deep_object =
     get_subexpression_at_offset(object_expr, pointer.offset, subtype, ns);
   CHECK_RETURN(deep_object.is_not_nil());
+  simplify(deep_object, ns);
   if(deep_object.id() != byte_extract_id())
-    return address_of_exprt(deep_object, type);
+    return typecast_exprt::conditional_cast(
+      address_of_exprt(deep_object), type);
 
   const byte_extract_exprt &be = to_byte_extract_expr(deep_object);
+  const address_of_exprt base(be.op());
   if(be.offset().is_zero())
-    return address_of_exprt(be.op(), type);
+    return typecast_exprt::conditional_cast(base, type);
 
-  const auto subtype_bytes = pointer_offset_size(subtype, ns);
-  CHECK_RETURN(subtype_bytes.has_value() && *subtype_bytes > 0);
-  if(*subtype_bytes > pointer.offset)
+  const auto object_size = pointer_offset_size(be.op().type(), ns);
+  if(object_size.has_value() && *object_size <= 1)
   {
-    return plus_exprt(
-      address_of_exprt(be.op(), pointer_type(char_type())),
-      from_integer(pointer.offset, index_type()));
+    return typecast_exprt::conditional_cast(
+      plus_exprt(base, from_integer(pointer.offset, pointer_diff_type())),
+      type);
+  }
+  else if(object_size.has_value() && pointer.offset % *object_size == 0)
+  {
+    return typecast_exprt::conditional_cast(
+      plus_exprt(
+        base, from_integer(pointer.offset / *object_size, pointer_diff_type())),
+      type);
   }
   else
   {
-    return plus_exprt(
-      address_of_exprt(be.op(), pointer_type(char_type())),
-      from_integer(pointer.offset / *subtype_bytes, index_type()));
+    return typecast_exprt::conditional_cast(
+      plus_exprt(
+        typecast_exprt(base, pointer_type(char_type())),
+        from_integer(pointer.offset, pointer_diff_type())),
+      type);
   }
 }