From 002af82e1f3d5ee64b1b1100814e8e61feb060c5 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Wed, 7 Sep 2016 13:18:35 +0100
Subject: [PATCH 1/2] Add array-byte-update tests

---
 regression/cbmc/byte_update1/main.c    | 24 ++++++++++++++++
 regression/cbmc/byte_update1/test.desc |  8 ++++++
 regression/cbmc/byte_update2/main.c    | 39 ++++++++++++++++++++++++++
 regression/cbmc/byte_update2/test.desc |  8 ++++++
 regression/cbmc/byte_update3/main.c    | 31 ++++++++++++++++++++
 regression/cbmc/byte_update3/test.desc |  8 ++++++
 regression/cbmc/byte_update4/main.c    | 36 ++++++++++++++++++++++++
 regression/cbmc/byte_update4/test.desc |  8 ++++++
 regression/cbmc/byte_update5/main.c    | 31 ++++++++++++++++++++
 regression/cbmc/byte_update5/test.desc |  8 ++++++
 regression/cbmc/byte_update6/main.c    | 39 ++++++++++++++++++++++++++
 regression/cbmc/byte_update6/test.desc |  8 ++++++
 regression/cbmc/byte_update7/main.c    | 39 ++++++++++++++++++++++++++
 regression/cbmc/byte_update7/test.desc |  8 ++++++
 14 files changed, 295 insertions(+)
 create mode 100644 regression/cbmc/byte_update1/main.c
 create mode 100644 regression/cbmc/byte_update1/test.desc
 create mode 100644 regression/cbmc/byte_update2/main.c
 create mode 100644 regression/cbmc/byte_update2/test.desc
 create mode 100644 regression/cbmc/byte_update3/main.c
 create mode 100644 regression/cbmc/byte_update3/test.desc
 create mode 100644 regression/cbmc/byte_update4/main.c
 create mode 100644 regression/cbmc/byte_update4/test.desc
 create mode 100644 regression/cbmc/byte_update5/main.c
 create mode 100644 regression/cbmc/byte_update5/test.desc
 create mode 100644 regression/cbmc/byte_update6/main.c
 create mode 100644 regression/cbmc/byte_update6/test.desc
 create mode 100644 regression/cbmc/byte_update7/main.c
 create mode 100644 regression/cbmc/byte_update7/test.desc

diff --git a/regression/cbmc/byte_update1/main.c b/regression/cbmc/byte_update1/main.c
new file mode 100644
index 00000000000..9171d793281
--- /dev/null
+++ b/regression/cbmc/byte_update1/main.c
@@ -0,0 +1,24 @@
+#include <stdio.h>
+#include <assert.h>
+
+struct A {
+  int x;
+};
+
+int main(int argc, char** argv) {
+
+  struct A a;
+  int i;
+  struct A* a_addr=&a;
+
+  if(argc != 2)
+    return;
+
+  void** ptrs[argc];
+  for(i = 0; i < 2; ++i)
+    ptrs[i] = (void*)0;
+
+  ((struct A**)ptrs)[1]=&a;
+  assert(ptrs[1] == (void*)&a);
+
+}
diff --git a/regression/cbmc/byte_update1/test.desc b/regression/cbmc/byte_update1/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/byte_update1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/byte_update2/main.c b/regression/cbmc/byte_update2/main.c
new file mode 100644
index 00000000000..12493e4267c
--- /dev/null
+++ b/regression/cbmc/byte_update2/main.c
@@ -0,0 +1,39 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 2)
+    return 0;
+
+  unsigned long x[argc];
+  x[0]=0x0102030405060708;
+  x[1]=0x1112131415161718;
+
+  unsigned char* alias=(unsigned short*)(((char*)x)+5);
+  *alias=0xed;
+
+  unsigned char* alias2=(unsigned char*)x;
+  /*
+  for(int i = 0; i < 16; ++i)
+    printf("%02hhx\n",alias2[i]);
+  */
+
+  assert(alias2[0]==0x08);
+  assert(alias2[1]==0x07);
+  assert(alias2[2]==0x06);
+  assert(alias2[3]==0x05);
+  assert(alias2[4]==0x04);
+  assert(alias2[5]==0xed);
+  assert(alias2[6]==0x02);
+  assert(alias2[7]==0x01);
+  assert(alias2[8]==0x18);
+  assert(alias2[9]==0x17);
+  assert(alias2[10]==0x16);
+  assert(alias2[11]==0x15);
+  assert(alias2[12]==0x14);
+  assert(alias2[13]==0x13);
+  assert(alias2[14]==0x12);
+  assert(alias2[15]==0x11);
+
+}
diff --git a/regression/cbmc/byte_update2/test.desc b/regression/cbmc/byte_update2/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/byte_update2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/byte_update3/main.c b/regression/cbmc/byte_update3/main.c
new file mode 100644
index 00000000000..6d9b3c293c0
--- /dev/null
+++ b/regression/cbmc/byte_update3/main.c
@@ -0,0 +1,31 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 5)
+    return 0;
+
+  short x[argc];
+  x[0]=0x0102;
+  x[1]=0x0304;
+  x[2]=0x0506;
+  x[3]=0x0708;
+  x[4]=0x090a;
+
+  unsigned long* alias=(unsigned long*)(((char*)x)+0);
+  *alias=0xf1f2f3f4f5f6f7f8;
+
+  unsigned char* alias2=(unsigned char*)x;
+  assert(alias2[0]==0xf8);
+  assert(alias2[1]==0xf7);
+  assert(alias2[2]==0xf6);
+  assert(alias2[3]==0xf5);
+  assert(alias2[4]==0xf4);
+  assert(alias2[5]==0xf3);
+  assert(alias2[6]==0xf2);
+  assert(alias2[7]==0xf1);
+  assert(alias2[8]==0x0a);
+  assert(alias2[9]==0x09);
+
+}
diff --git a/regression/cbmc/byte_update3/test.desc b/regression/cbmc/byte_update3/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/byte_update3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/byte_update4/main.c b/regression/cbmc/byte_update4/main.c
new file mode 100644
index 00000000000..0285f3058fe
--- /dev/null
+++ b/regression/cbmc/byte_update4/main.c
@@ -0,0 +1,36 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 10)
+    return 0;
+
+  unsigned char x[argc];
+  x[0]=0x01;
+  x[1]=0x02;
+  x[2]=0x03;
+  x[3]=0x04;
+  x[4]=0x05;
+  x[5]=0x06;
+  x[6]=0x07;
+  x[7]=0x08;
+  x[8]=0x09;
+  x[9]=0x0a;
+
+  unsigned long* alias=(unsigned long*)(((char*)x)+1);
+  *alias=0xf1f2f3f4f5f6f7f8;
+
+  unsigned char* alias2=(unsigned char*)x;
+  assert(alias2[0]==0x01);
+  assert(alias2[1]==0xf8);
+  assert(alias2[2]==0xf7);
+  assert(alias2[3]==0xf6);
+  assert(alias2[4]==0xf5);
+  assert(alias2[5]==0xf4);
+  assert(alias2[6]==0xf3);
+  assert(alias2[7]==0xf2);
+  assert(alias2[8]==0xf1);
+  assert(alias2[9]==0x0a);
+
+}
diff --git a/regression/cbmc/byte_update4/test.desc b/regression/cbmc/byte_update4/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/byte_update4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/byte_update5/main.c b/regression/cbmc/byte_update5/main.c
new file mode 100644
index 00000000000..e2f9da4defc
--- /dev/null
+++ b/regression/cbmc/byte_update5/main.c
@@ -0,0 +1,31 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 5)
+    return 0;
+
+  short x[argc];
+  x[0]=0x0102;
+  x[1]=0x0304;
+  x[2]=0x0506;
+  x[3]=0x0708;
+  x[4]=0x090a;
+
+  unsigned long* alias=(unsigned long*)(((char*)x)+1);
+  *alias=0xf1f2f3f4f5f6f7f8;
+
+  unsigned char* alias2=(unsigned char*)x;
+  assert(alias2[0]==0x02);
+  assert(alias2[1]==0xf8);
+  assert(alias2[2]==0xf7);
+  assert(alias2[3]==0xf6);
+  assert(alias2[4]==0xf5);
+  assert(alias2[5]==0xf4);
+  assert(alias2[6]==0xf3);
+  assert(alias2[7]==0xf2);
+  assert(alias2[8]==0xf1);
+  assert(alias2[9]==0x09);
+
+}
diff --git a/regression/cbmc/byte_update5/test.desc b/regression/cbmc/byte_update5/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/byte_update5/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/byte_update6/main.c b/regression/cbmc/byte_update6/main.c
new file mode 100644
index 00000000000..cb92364572d
--- /dev/null
+++ b/regression/cbmc/byte_update6/main.c
@@ -0,0 +1,39 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 2)
+    return 0;
+
+  unsigned long x[argc];
+  x[0]=0x0102030405060708;
+  x[1]=0x1112131415161718;
+
+  unsigned short* alias=(unsigned short*)(((char*)x)+8);
+  *alias=0xedcb;
+
+  unsigned char* alias2=(unsigned char*)x;
+  /*
+  for(int i = 0; i < 16; ++i)
+    printf("%02hhx\n",alias2[i]);
+  */
+
+  assert(alias2[0]==0x08);
+  assert(alias2[1]==0x07);
+  assert(alias2[2]==0x06);
+  assert(alias2[3]==0x05);
+  assert(alias2[4]==0x04);
+  assert(alias2[5]==0x03);
+  assert(alias2[6]==0x02);
+  assert(alias2[7]==0x01);
+  assert(alias2[8]==0xcb);
+  assert(alias2[9]==0xed);
+  assert(alias2[10]==0x16);
+  assert(alias2[11]==0x15);
+  assert(alias2[12]==0x14);
+  assert(alias2[13]==0x13);
+  assert(alias2[14]==0x12);
+  assert(alias2[15]==0x11);
+
+}
diff --git a/regression/cbmc/byte_update6/test.desc b/regression/cbmc/byte_update6/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/byte_update6/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/byte_update7/main.c b/regression/cbmc/byte_update7/main.c
new file mode 100644
index 00000000000..599df60afd7
--- /dev/null
+++ b/regression/cbmc/byte_update7/main.c
@@ -0,0 +1,39 @@
+#include <stdio.h>
+#include <assert.h>
+
+int main(int argc, char** argv) {
+
+  if(argc != 2)
+    return 0;
+
+  unsigned long x[argc];
+  x[0]=0x0102030405060708;
+  x[1]=0x1112131415161718;
+
+  unsigned short* alias=(unsigned short*)(((char*)x)+7);
+  *alias=0xedcb;
+
+  unsigned char* alias2=(unsigned char*)x;
+  /*
+  for(int i = 0; i < 16; ++i)
+    printf("%02hhx\n",alias2[i]);
+  */
+
+  assert(alias2[0]==0x08);
+  assert(alias2[1]==0x07);
+  assert(alias2[2]==0x06);
+  assert(alias2[3]==0x05);
+  assert(alias2[4]==0x04);
+  assert(alias2[5]==0x03);
+  assert(alias2[6]==0x02);
+  assert(alias2[7]==0xcb);
+  assert(alias2[8]==0xed);
+  assert(alias2[9]==0x17);
+  assert(alias2[10]==0x16);
+  assert(alias2[11]==0x15);
+  assert(alias2[12]==0x14);
+  assert(alias2[13]==0x13);
+  assert(alias2[14]==0x12);
+  assert(alias2[15]==0x11);
+
+}
diff --git a/regression/cbmc/byte_update7/test.desc b/regression/cbmc/byte_update7/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/byte_update7/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

From 8c07428d52b9a337a9ca2d5132cb703f7806cddc Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Mon, 5 Sep 2016 17:40:00 +0100
Subject: [PATCH 2/2] Fix byte-update flattening

This fixes byte update when applied to arrays with elements larger than a byte, which was previously unsound.
---
 .../flattening/flatten_byte_operators.cpp     | 141 +++++++++++++-----
 .../flattening/flatten_byte_operators.h       |   3 +-
 2 files changed, 106 insertions(+), 38 deletions(-)

diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp
index 3bc06ea6b1e..5e621fc803d 100644
--- a/src/solvers/flattening/flatten_byte_operators.cpp
+++ b/src/solvers/flattening/flatten_byte_operators.cpp
@@ -190,7 +190,8 @@ Function: flatten_byte_update
 
 exprt flatten_byte_update(
   const byte_update_exprt &src,
-  const namespacet &ns)
+  const namespacet &ns,
+  bool negative_offset)
 {
   assert(src.operands().size()==3);
 
@@ -265,44 +266,95 @@ exprt flatten_byte_update(
       {
         exprt result=src.op0();
 
-        for(mp_integer i=0; i<element_size; ++i)
+        // Number of potentially affected array cells:
+        mp_integer num_elements=
+          element_size/sub_size+((element_size%sub_size==0)?1:2);
+
+        const auto& offset_type=ns.follow(src.op1().type());
+        exprt zero_offset=from_integer(0, offset_type);
+
+        exprt sub_size_expr=from_integer(sub_size, offset_type);
+        exprt element_size_expr=from_integer(element_size, offset_type);
+
+        // First potentially affected cell:
+        div_exprt first_cell(src.op1(), sub_size_expr);
+
+        for(mp_integer i=0; i<num_elements; ++i)
         {
-          exprt new_value;
+          plus_exprt cell_index(first_cell, from_integer(i, offset_type));
+          mult_exprt cell_offset(cell_index, sub_size_expr);
+          index_exprt old_cell_value(src.op0(), cell_index, subtype);
+          bool is_first_cell=i==0;
+          bool is_last_cell=i==num_elements-1;
 
-          if(element_size==1)
+          exprt new_value;
+          exprt stored_value_offset;
+          if(element_size<=sub_size)
+          {
             new_value=src.op2();
+            stored_value_offset=zero_offset;
+          }
           else
           {
-            exprt i_expr=from_integer(i, ns.follow(src.op1().type()));
-
+            // Offset to retrieve from the stored value: make sure not to
+            // ask for anything out of range; in the first- or last-cell cases
+            // we will adjust the offset in the byte_update call below.
+            if(is_first_cell)
+              stored_value_offset=zero_offset;
+            else if(is_last_cell)
+              stored_value_offset=
+                from_integer(element_size-sub_size, offset_type);
+            else
+              stored_value_offset=minus_exprt(cell_offset, src.op1());
+
+            auto extract_opcode=
+              src.id()==ID_byte_update_little_endian ?
+              ID_byte_extract_little_endian :
+              src.id()==ID_byte_update_big_endian ?
+              ID_byte_extract_big_endian :
+              throw "unexpected src.id() in flatten_byte_update";
             byte_extract_exprt byte_extract_expr(
-              src.id()==ID_byte_update_little_endian?ID_byte_extract_little_endian:
-              src.id()==ID_byte_update_big_endian?ID_byte_extract_big_endian:
-              throw "unexpected src.id() in flatten_byte_update",
-              array_type.subtype());
+              extract_opcode,
+              element_size<sub_size ? src.op2().type() : subtype);
 
             byte_extract_expr.op()=src.op2();
-            byte_extract_expr.offset()=i_expr;
+            byte_extract_expr.offset()=stored_value_offset;
 
-            new_value=byte_extract_expr;
+            new_value=flatten_byte_extract(byte_extract_expr, ns);
           }
 
-          div_exprt div_offset(src.op1(), from_integer(sub_size, src.op1().type()));
-          mod_exprt mod_offset(src.op1(), from_integer(sub_size, src.op1().type()));
-
-          index_exprt index_expr(src.op0(), div_offset, array_type.subtype());
+          // Where does the value we just extracted align in this cell?
+          // This value might be negative, indicating only the most-significant
+          // bytes should be written, to the least-significant bytes of the
+          // target array cell.
+          exprt overwrite_offset;
+          if(is_first_cell)
+            overwrite_offset=mod_exprt(src.op1(), sub_size_expr);
+          else if(is_last_cell)
+          {
+            // This is intentionally negated; passing is_last_cell
+            // to flatten below leads to it being negated again later.
+            overwrite_offset=
+              minus_exprt(
+                minus_exprt(cell_offset, src.op1()),
+                stored_value_offset);
+          }
+          else
+            overwrite_offset=zero_offset;
 
-          byte_update_exprt byte_update_expr(src.id(), array_type.subtype());
-          byte_update_expr.op()=index_expr;
-          byte_update_expr.offset()=mod_offset;
-          byte_update_expr.value()=new_value;
+          byte_update_exprt byte_update_expr(
+            src.id(),
+            old_cell_value,
+            overwrite_offset,
+            new_value);
 
-          // Call recurisvely, the array is gone!
+          // Call recursively, the array is gone!
+          // The last parameter indicates that the
           exprt flattened_byte_update_expr=
-            flatten_byte_update(byte_update_expr, ns);
+            flatten_byte_update(byte_update_expr, ns, is_last_cell);
 
           with_exprt with_expr(
-            result, div_offset, flattened_byte_update_expr);
+            result, cell_index, flattened_byte_update_expr);
 
           result=with_expr;
         }
@@ -332,17 +384,7 @@ exprt flatten_byte_update(
 
     // build mask
     exprt mask=
-      bitnot_exprt(
-        from_integer(power(2, element_size*8)-1, unsignedbv_typet(width)));
-
-    const typet &offset_type=ns.follow(src.op1().type());
-    mult_exprt offset_times_eight(src.op1(), from_integer(8, offset_type));
-
-    // shift the mask
-    shl_exprt shl_expr(mask, offset_times_eight);
-
-    // do the 'AND'
-    bitand_exprt bitand_expr(src.op0(), mask);
+      from_integer(power(2, element_size*8)-1, unsignedbv_typet(width));
 
     // zero-extend the value, but only if needed
     exprt value_extended;
@@ -354,10 +396,35 @@ exprt flatten_byte_update(
     else
       value_extended=src.op2();
 
-    // shift the value
-    shl_exprt value_shifted(value_extended, offset_times_eight);
+    const typet &offset_type=ns.follow(src.op1().type());
+    mult_exprt offset_times_eight(src.op1(), from_integer(8, offset_type));
+
+    binary_predicate_exprt offset_ge_zero(
+      offset_times_eight,
+      ID_ge,
+      from_integer(0, offset_type));
+
+    // Shift the mask and value.
+    // Note either shift might discard some of the new value's bits.
+    exprt mask_shifted;
+    exprt value_shifted;
+    if(negative_offset)
+    {
+      // In this case we shift right, to mask out higher addresses
+      // rather than left to mask out lower ones as usual.
+      mask_shifted=lshr_exprt(mask, offset_times_eight);
+      value_shifted=lshr_exprt(value_extended, offset_times_eight);
+    }
+    else
+    {
+      mask_shifted=shl_exprt(mask, offset_times_eight);
+      value_shifted=shl_exprt(value_extended, offset_times_eight);
+    }
+
+    // original_bits &= ~mask
+    bitand_exprt bitand_expr(src.op0(), bitnot_exprt(mask_shifted));
 
-    // do the 'OR'
+    // original_bits |= newvalue
     bitor_exprt bitor_expr(bitand_expr, value_shifted);
 
     return bitor_expr;
diff --git a/src/solvers/flattening/flatten_byte_operators.h b/src/solvers/flattening/flatten_byte_operators.h
index 0a615198b9d..2730598f699 100644
--- a/src/solvers/flattening/flatten_byte_operators.h
+++ b/src/solvers/flattening/flatten_byte_operators.h
@@ -20,7 +20,8 @@ exprt flatten_byte_extract(
 
 exprt flatten_byte_update(
   const byte_update_exprt &src,
-  const namespacet &ns);
+  const namespacet &ns,
+  bool negative_offset=false);
 
 exprt flatten_byte_operators(const exprt &src, const namespacet &ns);