Validity checking of void pointers in contracts

Author: SaswatPadhi

regression/contracts/assigns_enforce_21/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int x = 0;
+
+void foo(void *y) __CPROVER_assigns(*y) __CPROVER_assigns(x)
+{
+  x = 2;
+  int *bar = (int *)y;
+  *bar = 2;
+}
+
+int main()
+{
+  int *y = malloc(sizeof(*y));
+  *y = 0;
+  foo(y);
+  assert(x == 2);
+  assert(*y == 2);
+  return 0;
+}

regression/contracts/assigns_enforce_21/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--enforce-contract foo _ --pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+--
+Checks whether contract enforcement does not try to dereference void pointers.

src/goto-instrument/contracts/utils.cpp

@@ -11,6 +11,7 @@ Date: September 2021
 #include "utils.h"
 
 #include <util/pointer_expr.h>
+#include <util/pointer_offset_size.h>
 #include <util/pointer_predicates.h>
 
 static void append_safe_havoc_code_for_expr(
@@ -58,9 +59,16 @@ exprt all_dereferences_are_valid(const exprt &expr, const namespacet &ns)
 {
   exprt::operandst validity_checks;
 
-  if(expr.id() == ID_dereference)
-    validity_checks.push_back(
-      good_pointer_def(to_dereference_expr(expr).pointer(), ns));
+  if(expr.id() == ID_dereference) {
+    const auto &pointer = to_dereference_expr(expr).pointer();
+    const auto opt_size_of_deref =
+      size_of_expr(to_pointer_type(pointer.type()).subtype(), ns);
+
+    if(opt_size_of_deref.has_value())
+      validity_checks.push_back(good_pointer_def(pointer, ns));
+    else
+      validity_checks.push_back(false_exprt());
+  }
 
   for(const auto &op : expr.operands())
     validity_checks.push_back(all_dereferences_are_valid(op, ns));

src/util/pointer_predicates.cpp

@@ -89,7 +89,10 @@ exprt good_pointer_def(
   const typet &dereference_type=pointer_type.subtype();
 
   const auto size_of_expr_opt = size_of_expr(dereference_type, ns);
-  CHECK_RETURN(size_of_expr_opt.has_value());
+  PRECONDITION_WITH_DIAGNOSTICS(
+    size_of_expr_opt.has_value(),
+    "Could not compute sizeof on pointer's dereference type. "
+    "It may be a void pointer.");
 
   const exprt good_dynamic = not_exprt{deallocated(pointer, ns)};