From 6ac8ebbb294452d5adc53aa78b6d04223d0fca95 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 11 May 2021 00:40:49 +0000
Subject: [PATCH] Value sets: fix byte extracts from structs

Pointers may be contained in any member that's included in the byte
range being extracted, not just the one right at the offset that the
byte extract starts from.

Co-Authored-By: Petr Bauch <petr.bauch@gmail.com>
---
 regression/cbmc/Pointer_byte_extract8/main.c  | 58 +++++++++++++++++++
 .../cbmc/Pointer_byte_extract8/test.desc      |  9 +++
 src/pointer-analysis/value_set.cpp            | 43 +++++++++-----
 3 files changed, 95 insertions(+), 15 deletions(-)
 create mode 100644 regression/cbmc/Pointer_byte_extract8/main.c
 create mode 100644 regression/cbmc/Pointer_byte_extract8/test.desc

diff --git a/regression/cbmc/Pointer_byte_extract8/main.c b/regression/cbmc/Pointer_byte_extract8/main.c
new file mode 100644
index 00000000000..d6fd4b2072b
--- /dev/null
+++ b/regression/cbmc/Pointer_byte_extract8/main.c
@@ -0,0 +1,58 @@
+#include <assert.h>
+#include <stdlib.h>
+
+#ifdef _MSC_VER
+#  define _Static_assert(x, m) static_assert(x, m)
+#endif
+
+struct list;
+
+typedef struct list list_nodet;
+
+list_nodet fill_node(signed int depth_tag_list);
+
+struct list
+{
+  int datum;
+  struct list *next;
+};
+
+int max_depth = 2;
+
+list_nodet *build_node(int depth)
+{
+  if(max_depth < depth)
+    return ((list_nodet *)NULL);
+  else
+  {
+    _Static_assert(sizeof(list_nodet) == 16, "");
+    list_nodet *result = malloc(16);
+
+    if(result)
+    {
+      *result = fill_node(depth + 1);
+    }
+    return result;
+  }
+}
+
+list_nodet fill_node(int depth)
+{
+  list_nodet result;
+  result.datum = depth;
+  result.next = build_node(depth);
+  return result;
+}
+
+int main()
+{
+  list_nodet *node = build_node(0);
+  int i = 0;
+  list_nodet *list_walker = node;
+  for(; list_walker; list_walker = list_walker->next)
+  {
+    i = i + 1;
+  }
+  assert(i == 3);
+  return 0;
+}
diff --git a/regression/cbmc/Pointer_byte_extract8/test.desc b/regression/cbmc/Pointer_byte_extract8/test.desc
new file mode 100644
index 00000000000..adcea6ed3e2
--- /dev/null
+++ b/regression/cbmc/Pointer_byte_extract8/test.desc
@@ -0,0 +1,9 @@
+CORE
+main.c
+--64 --unwind 4 --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^CONVERSION ERROR$
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 009b6549ea0..972027af251 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -891,34 +891,47 @@ void value_sett::get_value_set_rec(
 
     bool found=false;
 
-    exprt op1 = byte_extract_expr.op1();
-    if(eval_pointer_offset(op1, ns))
-      simplify(op1, ns);
-
-    const auto op1_offset = numeric_cast<mp_integer>(op1);
     const typet &op_type = ns.follow(byte_extract_expr.op().type());
-    if(op1_offset.has_value() && op_type.id() == ID_struct)
+    if(op_type.id() == ID_struct)
     {
+      exprt offset = byte_extract_expr.offset();
+      if(eval_pointer_offset(offset, ns))
+        simplify(offset, ns);
+
+      const auto offset_int = numeric_cast<mp_integer>(offset);
+      const auto type_size = pointer_offset_size(expr.type(), ns);
+
       const struct_typet &struct_type = to_struct_type(op_type);
 
       for(const auto &c : struct_type.components())
       {
         const irep_idt &name = c.get_name();
 
-        auto comp_offset = member_offset(struct_type, name, ns);
-
-        if(!comp_offset.has_value())
-          continue;
-        else if(*comp_offset > *op1_offset)
-          break;
-        else if(*comp_offset != *op1_offset)
-          continue;
+        if(offset_int.has_value())
+        {
+          auto comp_offset = member_offset(struct_type, name, ns);
+          if(comp_offset.has_value())
+          {
+            if(
+              type_size.has_value() && *offset_int + *type_size <= *comp_offset)
+            {
+              break;
+            }
+
+            auto member_size = pointer_offset_size(c.type(), ns);
+            if(
+              member_size.has_value() &&
+              *offset_int >= *comp_offset + *member_size)
+            {
+              continue;
+            }
+          }
+        }
 
         found=true;
 
         member_exprt member(byte_extract_expr.op(), c);
         get_value_set_rec(member, dest, suffix, original_type, ns);
-        break;
       }
     }