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 <[email protected]>

Author: tautschnig

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;
+}

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$

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;
       }
     }