Merge pull request #6107 from tautschnig/value-set-byte_extract

Value sets: fix byte extracts from structs

Author: NlightNFotis

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