From 03347eb6a2e168a6e709c0a91f83465d53beaa81 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 28 Jun 2017 10:10:29 +0100
Subject: [PATCH] Expansion of array_replace/array_copy must not drop offsets

---
 regression/cbmc/memset2/main.c    | 22 ++++++++++++++++++++
 regression/cbmc/memset2/test.desc |  8 ++++++++
 src/goto-symex/symex_other.cpp    | 34 +++++++++++++++++++++++++++++--
 3 files changed, 62 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc/memset2/main.c
 create mode 100644 regression/cbmc/memset2/test.desc

diff --git a/regression/cbmc/memset2/main.c b/regression/cbmc/memset2/main.c
new file mode 100644
index 00000000000..c317d161215
--- /dev/null
+++ b/regression/cbmc/memset2/main.c
@@ -0,0 +1,22 @@
+#include <string.h>
+#include <assert.h>
+
+typedef struct {
+  int a;
+  int b;
+} TEST;
+
+static TEST test;
+
+main()
+{
+  test.a = 1;
+  test.b = 2;
+  memset(&test.b, 0, sizeof(test.b));
+  assert(test.a);
+  assert(!test.b);
+  test.b = 2;
+  memset(&test.a, 0, sizeof(test.a));
+  assert(!test.a);
+  assert(test.b);
+}
diff --git a/regression/cbmc/memset2/test.desc b/regression/cbmc/memset2/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/memset2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 8c04ab3a688..b9b2c7fd597 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -94,13 +94,21 @@ void goto_symext::symex_other(
     clean_code.op1()=d1;
 
     clean_expr(clean_code.op0(), state, true);
+    exprt op0_offset=from_integer(0, index_type());
     if(clean_code.op0().id()==byte_extract_id() &&
        clean_code.op0().type().id()==ID_empty)
+    {
+      op0_offset=to_byte_extract_expr(clean_code.op0()).offset();
       clean_code.op0()=clean_code.op0().op0();
+    }
     clean_expr(clean_code.op1(), state, false);
+    exprt op1_offset=from_integer(0, index_type());
     if(clean_code.op1().id()==byte_extract_id() &&
        clean_code.op1().type().id()==ID_empty)
+    {
+      op1_offset=to_byte_extract_expr(clean_code.op1()).offset();
       clean_code.op1()=clean_code.op1().op0();
+    }
 
     process_array_expr(clean_code.op0());
     clean_expr(clean_code.op0(), state, true);
@@ -109,23 +117,45 @@ void goto_symext::symex_other(
 
 
     if(!base_type_eq(clean_code.op0().type(),
-                     clean_code.op1().type(), ns))
+                     clean_code.op1().type(), ns) ||
+       !op0_offset.is_zero() || !op1_offset.is_zero())
     {
       byte_extract_exprt be(byte_extract_id());
-      be.offset()=from_integer(0, index_type());
 
       if(statement==ID_array_copy)
       {
         be.op()=clean_code.op1();
+        be.offset()=op1_offset;
         be.type()=clean_code.op0().type();
         clean_code.op1()=be;
+
+        if(!op0_offset.is_zero())
+        {
+          byte_extract_exprt op0(
+            byte_extract_id(),
+            clean_code.op0(),
+            op0_offset,
+            clean_code.op0().type());
+          clean_code.op0()=op0;
+        }
       }
       else
       {
         // ID_array_replace
         be.op()=clean_code.op0();
+        be.offset()=op0_offset;
         be.type()=clean_code.op1().type();
         clean_code.op0()=be;
+
+        if(!op1_offset.is_zero())
+        {
+          byte_extract_exprt op1(
+            byte_extract_id(),
+            clean_code.op1(),
+            op1_offset,
+            clean_code.op1().type());
+          clean_code.op1()=op1;
+        }
       }
     }