From a51a4afd8616b6fa796f0b18b75a4e6dad300b8e Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 27 May 2019 21:11:48 +0000
Subject: [PATCH] Fix unbounded recursion in byte-update lowering of structs

The missing update of the type of the byte-update expression caused the
very same procedure to be invoked recursively. Instead we should use
byte-update-of-array.
---
 regression/cbmc/byte_update11/main.c    | 13 +++++++++++++
 regression/cbmc/byte_update11/test.desc |  8 ++++++++
 src/solvers/lowering/byte_operators.cpp |  5 +++++
 3 files changed, 26 insertions(+)
 create mode 100644 regression/cbmc/byte_update11/main.c
 create mode 100644 regression/cbmc/byte_update11/test.desc

diff --git a/regression/cbmc/byte_update11/main.c b/regression/cbmc/byte_update11/main.c
new file mode 100644
index 0000000000..18d0ebc517
--- /dev/null
+++ b/regression/cbmc/byte_update11/main.c
@@ -0,0 +1,13 @@
+struct S
+{
+  int i;
+};
+
+int main()
+{
+  unsigned x;
+  __CPROVER_assume(x % sizeof(int) == 0);
+  struct S A[x];
+  ((char *)A)[x] = 42;
+  __CPROVER_assert((A[x / sizeof(int)].i & 0xFF) == 42, "lowest byte is 42");
+}
diff --git a/regression/cbmc/byte_update11/test.desc b/regression/cbmc/byte_update11/test.desc
new file mode 100644
index 0000000000..9845e70d84
--- /dev/null
+++ b/regression/cbmc/byte_update11/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--little-endian
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp
index dae4ce24dd..9f93823407 100644
--- a/src/solvers/lowering/byte_operators.cpp
+++ b/src/solvers/lowering/byte_operators.cpp
@@ -1787,6 +1787,10 @@ static exprt lower_byte_update_struct(
     }
     else if(!offset_bytes.has_value())
     {
+      // The offset to update is not constant; abort the attempt to update
+      // indiviual struct members and instead turn the operand-to-be-updated
+      // into a byte array, which we know how to update even if the offset is
+      // non-constant.
       const irep_idt extract_opcode = src.id() == ID_byte_update_little_endian
                                         ? ID_byte_extract_little_endian
                                         : ID_byte_extract_big_endian;
@@ -1802,6 +1806,7 @@ static exprt lower_byte_update_struct(
 
       byte_update_exprt bu = src;
       bu.set_op(lower_byte_extract(byte_extract_expr, ns));
+      bu.type() = bu.op().type();
 
       return lower_byte_extract(
         byte_extract_exprt{