From 7c8b89353a1a38dfc6acbfa780171e804f6d649c Mon Sep 17 00:00:00 2001
From: Saswat Padhi <saspadhi@amazon.com>
Date: Thu, 30 Sep 2021 15:35:55 +0000
Subject: [PATCH] Validity checking of `void` pointers in contracts

---
 .../contracts/assigns_enforce_21/main.c       | 21 +++++++++++++++++++
 .../contracts/assigns_enforce_21/test.desc    |  9 ++++++++
 src/goto-instrument/contracts/utils.cpp       | 13 ++++++++++--
 src/util/pointer_predicates.cpp               |  5 ++++-
 4 files changed, 45 insertions(+), 3 deletions(-)
 create mode 100644 regression/contracts/assigns_enforce_21/main.c
 create mode 100644 regression/contracts/assigns_enforce_21/test.desc

diff --git a/regression/contracts/assigns_enforce_21/main.c b/regression/contracts/assigns_enforce_21/main.c
new file mode 100644
index 00000000000..98c6b049b12
--- /dev/null
+++ b/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;
+}
diff --git a/regression/contracts/assigns_enforce_21/test.desc b/regression/contracts/assigns_enforce_21/test.desc
new file mode 100644
index 00000000000..c39a52fb755
--- /dev/null
+++ b/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.
diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp
index 4f4d772988a..84e3b336fab 100644
--- a/src/goto-instrument/contracts/utils.cpp
+++ b/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(
@@ -59,8 +60,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));
+  {
+    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));
diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp
index a78c48f7712..39e562fcb36 100644
--- a/src/util/pointer_predicates.cpp
+++ b/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)};