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.

Author: dc-mak

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.

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.

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.

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.

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.

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.

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.

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.