From 820eb8657bbe225d7c4eae3cc1220e32282c9bcd Mon Sep 17 00:00:00 2001
From: Dhruv Makwana <dc_mak@outlook.com>
Date: Tue, 3 Dec 2024 13:47:08 +0000
Subject: [PATCH] CN VIP: Clarify tests

Some of the tests rely on ignoring the (demonic) address allocation
non-determinism which means that technically that have UB but in
practice they are there to exercise particular bits of the memory
object model.
---
 tests/cn_vip_testsuite/pointer_from_integer_1i.annot.c     | 7 ++++++-
 tests/cn_vip_testsuite/pointer_from_integer_1ie.annot.c    | 7 ++++++-
 tests/cn_vip_testsuite/pointer_from_integer_1ig.annot.c    | 5 +++++
 .../provenance_basic_using_uintptr_t_auto_yx.annot.c       | 5 +++++
 .../provenance_basic_using_uintptr_t_global_yx.annot.c     | 5 +++++
 .../provenance_equality_uintptr_t_auto_yx.pass.c           | 5 +++++
 .../provenance_equality_uintptr_t_global_yx.pass.c         | 5 +++++
 tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c    | 5 +++++
 8 files changed, 42 insertions(+), 2 deletions(-)

diff --git a/tests/cn_vip_testsuite/pointer_from_integer_1i.annot.c b/tests/cn_vip_testsuite/pointer_from_integer_1i.annot.c
index 625f1cbab..88e1fb1c8 100644
--- a/tests/cn_vip_testsuite/pointer_from_integer_1i.annot.c
+++ b/tests/cn_vip_testsuite/pointer_from_integer_1i.annot.c
@@ -6,7 +6,7 @@
 #include "cn_lemmas.h"
 void f(uintptr_t i) {
   int j=5;
-  /*@ apply assert_equal(i, (u64)&j); @*/
+  /*CN_VIP*//*@ apply assert_equal(i, (u64)&j); @*/
 #if defined(ANNOT)
   int *p = copy_alloc_id(i, &j);
 #else
@@ -20,3 +20,8 @@ int main() {
   uintptr_t j = ADDRESS_PFI_1I;
   f(j);
 }
+
+// The evaluation table in the appendix of the VIP paper is misleading.
+// This file has UB under PNVI-ae-udi without annotations because
+// of allocation address non-determinism (demonic).
+// I emulate the same behaviour by asserting the addresses are equal.
diff --git a/tests/cn_vip_testsuite/pointer_from_integer_1ie.annot.c b/tests/cn_vip_testsuite/pointer_from_integer_1ie.annot.c
index 61ddda767..0a2208fe1 100644
--- a/tests/cn_vip_testsuite/pointer_from_integer_1ie.annot.c
+++ b/tests/cn_vip_testsuite/pointer_from_integer_1ie.annot.c
@@ -7,7 +7,7 @@
 void f(uintptr_t i) {
   int j=5;
   uintptr_t k = (uintptr_t)&j;
-  /*@ apply assert_equal(i, k); @*/
+  /*CN_VIP*//*@ apply assert_equal(i, k); @*/
 #if defined(ANNOT)
   int *p = copy_alloc_id(i, &j);
 #else
@@ -21,3 +21,8 @@ int main() {
   uintptr_t j = ADDRESS_PFI_1I;
   f(j);
 }
+
+// The evaluation table in the appendix of the VIP paper is misleading.
+// This file has UB under PNVI-ae-udi without annotations because
+// of allocation address non-determinism (demonic)
+// The desired behaviour can be obtained by asserting the addresses are equal.
diff --git a/tests/cn_vip_testsuite/pointer_from_integer_1ig.annot.c b/tests/cn_vip_testsuite/pointer_from_integer_1ig.annot.c
index f7d60a1a6..6a3eb7622 100644
--- a/tests/cn_vip_testsuite/pointer_from_integer_1ig.annot.c
+++ b/tests/cn_vip_testsuite/pointer_from_integer_1ig.annot.c
@@ -22,3 +22,8 @@ int main() {
   uintptr_t j = ADDRESS_PFI_1IG;
   f(j);
 }
+
+// The evaluation table in the appendix of the VIP paper is misleading.
+// This file has UB under PNVI-ae-udi without annotations because
+// of allocation address non-determinism (demonic)
+// The desired behaviour can be obtained by asserting the addresses are equal.
diff --git a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c
index 367d9aa76..1a0f644f5 100644
--- a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c
+++ b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c
@@ -39,3 +39,8 @@ int main() {
     /*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
   }
 }
+
+// The evaluation table in the appendix of the VIP paper is misleading.
+// This file has UB under PNVI-ae-udi without annotations because
+// of allocation address non-determinism (demonic)
+// The desired behaviour can be obtained by asserting the addresses are adjacent.
diff --git a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c
index 2323bb81b..a303f414b 100644
--- a/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c
+++ b/tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c
@@ -39,3 +39,8 @@ int main()
     /*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
   }
 }
+
+// The evaluation table in the appendix of the VIP paper is misleading.
+// This file has UB under PNVI-ae-udi without annotations because
+// of allocation address non-determinism (demonic)
+// The desired behaviour can be obtained by asserting the addresses are adjacent.
diff --git a/tests/cn_vip_testsuite/provenance_equality_uintptr_t_auto_yx.pass.c b/tests/cn_vip_testsuite/provenance_equality_uintptr_t_auto_yx.pass.c
index 3f9b7f91f..817a07f95 100644
--- a/tests/cn_vip_testsuite/provenance_equality_uintptr_t_auto_yx.pass.c
+++ b/tests/cn_vip_testsuite/provenance_equality_uintptr_t_auto_yx.pass.c
@@ -13,3 +13,8 @@ int main() {
   /*CN_VIP*//*@ assert (b == 1u8); @*/
   return 0;
 }
+
+// The evaluation table in the appendix of the VIP paper is misleading.
+// This file has UB under PNVI-ae-udi without annotations because
+// of allocation address non-determinism (demonic)
+// The desired behaviour can be obtained by asserting the addresses are adjacent.
diff --git a/tests/cn_vip_testsuite/provenance_equality_uintptr_t_global_yx.pass.c b/tests/cn_vip_testsuite/provenance_equality_uintptr_t_global_yx.pass.c
index ca27e4105..4fdf1b27d 100644
--- a/tests/cn_vip_testsuite/provenance_equality_uintptr_t_global_yx.pass.c
+++ b/tests/cn_vip_testsuite/provenance_equality_uintptr_t_global_yx.pass.c
@@ -13,3 +13,8 @@ int main() {
   /*CN_VIP*//*@ assert (b == 1u8); @*/
   return 0;
 }
+
+// The evaluation table in the appendix of the VIP paper is misleading.
+// This file has UB under PNVI-ae-udi without annotations because
+// of allocation address non-determinism (demonic)
+// The desired behaviour can be obtained by asserting the addresses are adjacent.
diff --git a/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c b/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c
index e2c3f3731..5641b3951 100644
--- a/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c
+++ b/tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c
@@ -32,3 +32,8 @@ int main()
     /*CN_VIP*//*@ assert(x == 11i32 && *p == 11i32 && *q == 11i32); @*/
   }
 }
+
+// The evaluation table in the appendix of the VIP paper is misleading.
+// This file has UB under PNVI-ae-udi without annotations because
+// of allocation address non-determinism (demonic)
+// The desired behaviour can be obtained by asserting the addresses are equal.