Skip to content

Commit d80f4eb

Browse files
dc-makdc-mak
committed
CN VIP: Update failures tests to use byte rep
1 parent 8e1a836 commit d80f4eb

13 files changed

+112
-174
lines changed

‎backend/cn/lib/check.ml

+2-1
Original file line numberDiff line numberDiff line change
@@ -1406,9 +1406,10 @@ let rec check_expr labels (e : BT.t Mu.expr) (k : IT.t -> unit m) : unit m =
14061406
| Array (item_ty, _) -> Memory.size_of_ctype item_ty
14071407
| ct -> Memory.size_of_ctype ct
14081408
in
1409+
let ub = CF.Undefined.UB048_disjoint_array_pointers_subtraction in
1410+
let@ () = check_both_eq_alloc loc arg1 arg2 ub in
14091411
let ub_unspec = CF.Undefined.UB_unspec_pointer_sub in
14101412
let ub = CF.Undefined.(UB_CERB004_unspecified ub_unspec) in
1411-
let@ () = check_both_eq_alloc loc arg1 arg2 ub in
14121413
let@ () =
14131414
check_live_alloc_bounds `Ptr_diff loc arg1 ub (both_in_bounds arg1 arg2)
14141415
in

‎tests/cn_vip_testsuite/cheri_03_ii.error.c

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ int main() {
33
int x[2];
44
int *p = &x[0];
55
//is this free of undefined behaviour?
6-
int *q = p + 11;
6+
int *q = p + 11; // CN VIP UB
77
q = q - 10;
88
*q = 1;
99
//CN_VIP printf("x[1]=%i *q=%i\n",x[1],*q);

‎tests/cn_vip_testsuite/cn_lemmas.h

-96
Original file line numberDiff line numberDiff line change
@@ -1,98 +1,3 @@
1-
unsigned char* block_int_ptr_to_block_uchar_arr(int **addr_p)
2-
/*@
3-
trusted;
4-
5-
requires
6-
take P = Block<int*>(addr_p);
7-
8-
ensures
9-
ptr_eq(return, addr_p);
10-
take B = Block<unsigned char[sizeof(int*)]>(return);
11-
@*/
12-
{
13-
return (unsigned char*)addr_p;
14-
}
15-
unsigned char* owned_int_ptr_to_owned_uchar_arr(int **addr_p)
16-
/*@
17-
trusted;
18-
19-
requires
20-
take P = Owned<int*>(addr_p);
21-
22-
ensures
23-
ptr_eq(return, addr_p);
24-
take B = Owned<unsigned char[(sizeof(int*))]>(return);
25-
(u64) P == shift_left((u64)B[7u64], 56u64)
26-
+ shift_left((u64)B[6u64], 48u64)
27-
+ shift_left((u64)B[5u64], 40u64)
28-
+ shift_left((u64)B[4u64], 32u64)
29-
+ shift_left((u64)B[3u64], 24u64)
30-
+ shift_left((u64)B[2u64], 16u64)
31-
+ shift_left((u64)B[1u64], 8u64)
32-
+ (u64)B[0u64];
33-
@*/
34-
{
35-
return (unsigned char*)addr_p;
36-
}
37-
38-
unsigned char* owned_uintptr_t_to_owned_uchar_arr(uintptr_t *addr_p)
39-
/*@
40-
trusted;
41-
42-
requires
43-
take P = Owned<uintptr_t>(addr_p);
44-
45-
ensures
46-
ptr_eq(return, addr_p);
47-
take B = Owned<unsigned char[(sizeof(uintptr_t))]>(return);
48-
(u64) P == shift_left((u64)B[7u64], 56u64)
49-
+ shift_left((u64)B[6u64], 48u64)
50-
+ shift_left((u64)B[5u64], 40u64)
51-
+ shift_left((u64)B[4u64], 32u64)
52-
+ shift_left((u64)B[3u64], 24u64)
53-
+ shift_left((u64)B[2u64], 16u64)
54-
+ shift_left((u64)B[1u64], 8u64)
55-
+ (u64)B[0u64];
56-
@*/
57-
{
58-
return (unsigned char*)addr_p;
59-
}
60-
/*@
61-
lemma byte_ptr_to_int_ptr_ptr(pointer addr_p)
62-
63-
requires
64-
take B = Owned<unsigned char[(sizeof(int*))]>(addr_p);
65-
66-
ensures
67-
take P = Owned<int*>(addr_p);
68-
(u64) P == shift_left((u64)B[7u64], 56u64)
69-
+ shift_left((u64)B[6u64], 48u64)
70-
+ shift_left((u64)B[5u64], 40u64)
71-
+ shift_left((u64)B[4u64], 32u64)
72-
+ shift_left((u64)B[3u64], 24u64)
73-
+ shift_left((u64)B[2u64], 16u64)
74-
+ shift_left((u64)B[1u64], 8u64)
75-
+ (u64)B[0u64];
76-
@*/
77-
78-
/*@
79-
lemma byte_ptr_to_uintptr_t(pointer addr_p)
80-
81-
requires
82-
take B = Owned<unsigned char[(sizeof(uintptr_t))]>(addr_p);
83-
84-
ensures
85-
take P = Owned<uintptr_t>(addr_p);
86-
(u64) P == shift_left((u64)B[7u64], 56u64)
87-
+ shift_left((u64)B[6u64], 48u64)
88-
+ shift_left((u64)B[5u64], 40u64)
89-
+ shift_left((u64)B[4u64], 32u64)
90-
+ shift_left((u64)B[3u64], 24u64)
91-
+ shift_left((u64)B[2u64], 16u64)
92-
+ shift_left((u64)B[1u64], 8u64)
93-
+ (u64)B[0u64];
94-
@*/
95-
961
/*@
972
lemma byte_arrays_equal(pointer x, pointer y, u64 n)
983
@@ -151,4 +56,3 @@ requires
15156
ensures
15257
x == y;
15358
@*/
154-

‎tests/cn_vip_testsuite/pointer_copy_user_dataflow_direct_bytewise.unprovable.c ‎tests/cn_vip_testsuite/pointer_copy_user_dataflow_direct_bytewise.c

File renamed without changes.

‎tests/cn_vip_testsuite/pointer_from_int_disambiguation_3.error.c

+22-11
Original file line numberDiff line numberDiff line change
@@ -13,20 +13,31 @@ int main()
1313
int *q = &y;
1414
uintptr_t i = (uintptr_t)p;
1515
uintptr_t j = (uintptr_t)q;
16-
/*CN_VIP*/unsigned char* p_bytes = owned_int_ptr_to_owned_uchar_arr(&p);
17-
/*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
18-
/*CN_VIP*/int result = _memcmp(p_bytes, q_bytes, sizeof(p));
19-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(p_bytes); @*/
20-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
16+
/*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
17+
/*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
18+
/*CN_VIP*/int result = _memcmp((unsigned char*)&p, (unsigned char*)&q, sizeof(p));
19+
/*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
20+
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
21+
#ifdef NO_ROUND_TRIP
22+
/*CN_VIP*/p = copy_alloc_id((uintptr_t)p, &x);
23+
/*CN_VIP*/q = copy_alloc_id((uintptr_t)q, &y);
24+
#endif
2125
if (result == 0) {
22-
#if defined(ANNOT)
23-
int *r = copy_alloc_id(i, q);
24-
#else
26+
#ifdef ANNOT
27+
int *r = copy_alloc_id(i, q); // CN VIP UB if ¬NO_ROUND_TRIP & ANNOT
28+
# else
2529
int *r = (int *)i;
30+
#ifdef NO_ROUND_TRIP
31+
/*CN_VIP*/r = copy_alloc_id((uintptr_t)r, p);
32+
#endif
2633
#endif
27-
*r=11;
28-
r=r-1; // is this free of UB?
29-
*r=12; // and this?
34+
*r=11; // CN VIP UB if ¬ANNOT
35+
r=r-1; // CN VIP UB if NO_ROUND TRIP && ANNOT
36+
*r=12;
3037
//CN_VIP printf("x=%d y=%d *q=%d *r=%d\n",x,y,*q,*r);
3138
}
3239
}
40+
41+
/* NOTE: see tests/pvni_testsuite for why what
42+
vip_artifact/evaluation_cerberus/results.pdf expects for this test is probably
43+
wrong. */

‎tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_xy.error.c

+10-7
Original file line numberDiff line numberDiff line change
@@ -7,15 +7,18 @@ int main() {
77
int x=1, y=2;
88
int *p = &x;
99
int *q = &y;
10-
ptrdiff_t offset = q - p;
10+
ptrdiff_t offset = q - p; // CN VIP UB
1111
int *r = p + offset;
12-
/*CN_VIP*/unsigned char* r_bytes = owned_int_ptr_to_owned_uchar_arr(&r);
13-
/*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
14-
/*CN_VIP*/int result = _memcmp(r_bytes, q_bytes, sizeof(r));
15-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(r_bytes); @*/
16-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
12+
/*CN_VIP*//*@ to_bytes Owned<int*>(&r); @*/
13+
/*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
14+
/*CN_VIP*/int result = _memcmp((unsigned char*)&r, (unsigned char*)&q, sizeof(r));
15+
/*CN_VIP*//*@ from_bytes Owned<int*>(&r); @*/
16+
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
17+
#ifdef NO_ROUND_TRIP
18+
/*CN_VIP*/r = __cerbvar_copy_alloc_id((uintptr_t)r, &x);
19+
#endif
1720
if (result == 0) {
18-
*r = 11; // is this free of UB?
21+
*r = 11;
1922
//CN_VIP printf("y=%d *q=%d *r=%d\n",y,*q,*r);
2023
}
2124
}

‎tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_auto_yx.error.c

+10-7
Original file line numberDiff line numberDiff line change
@@ -7,15 +7,18 @@ int main() {
77
int y=2, x=1;
88
int *p = &x;
99
int *q = &y;
10-
ptrdiff_t offset = q - p;
10+
ptrdiff_t offset = q - p; // CN VIP UB
1111
int *r = p + offset;
12-
/*CN_VIP*/unsigned char* r_bytes = owned_int_ptr_to_owned_uchar_arr(&r);
13-
/*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
14-
/*CN_VIP*/int result = _memcmp(r_bytes, q_bytes, sizeof(r));
15-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(r_bytes); @*/
16-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
12+
/*CN_VIP*//*@ to_bytes Owned<int*>(&r); @*/
13+
/*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
14+
/*CN_VIP*/int result = _memcmp((unsigned char*)&r, (unsigned char*)&q, sizeof(r));
15+
/*CN_VIP*//*@ from_bytes Owned<int*>(&r); @*/
16+
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
17+
#ifdef NO_ROUND_TRIP
18+
/*CN_VIP*/r = __cerbvar_copy_alloc_id((uintptr_t)r, &x);
19+
#endif
1720
if (result == 0) {
18-
*r = 11; // is this free of UB?
21+
*r = 11;
1922
//CN_VIP printf("y=%d *q=%d *r=%d\n",y,*q,*r);
2023
}
2124
}

‎tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_xy.error.c

+10-7
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,20 @@
55
#include "cn_lemmas.h"
66
int x=1, y=2;
77
int main()
8-
/*CN_VIP*//*@ accesses y; @*/
8+
/*CN_VIP*//*@ accesses x; accesses y; @*/
99
{
1010
int *p = &x;
1111
int *q = &y;
12-
ptrdiff_t offset = q - p;
12+
ptrdiff_t offset = q - p; // CN VIP UB
1313
int *r = p + offset;
14-
/*CN_VIP*/unsigned char* r_bytes = owned_int_ptr_to_owned_uchar_arr(&r);
15-
/*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
16-
/*CN_VIP*/int result = _memcmp(r_bytes, q_bytes, sizeof(r));
17-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(r_bytes); @*/
18-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
14+
/*CN_VIP*//*@ to_bytes Owned<int*>(&r); @*/
15+
/*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
16+
/*CN_VIP*/int result = _memcmp((unsigned char*)&r, (unsigned char*)&q, sizeof(r));
17+
/*CN_VIP*//*@ from_bytes Owned<int*>(&r); @*/
18+
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
19+
#ifdef NO_ROUND_TRIP
20+
/*CN_VIP*/r = __cerbvar_copy_alloc_id((uintptr_t)r, &x);
21+
#endif
1922
if (result == 0) {
2023
*r = 11; // is this free of UB?
2124
//CN_VIP printf("y=%d *q=%d *r=%d\n",y,*q,*r);

‎tests/cn_vip_testsuite/pointer_offset_from_ptr_subtraction_global_yx.error.c

+10-7
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,20 @@
55
#include "cn_lemmas.h"
66
int y=2, x=1;
77
int main()
8-
/*CN_VIP*//*@ accesses y; @*/
8+
/*CN_VIP*//*@ accesses x; accesses y; @*/
99
{
1010
int *p = &x;
1111
int *q = &y;
12-
ptrdiff_t offset = q - p;
12+
ptrdiff_t offset = q - p; // CN VIP UB
1313
int *r = p + offset;
14-
/*CN_VIP*/unsigned char* r_bytes = owned_int_ptr_to_owned_uchar_arr(&r);
15-
/*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
16-
/*CN_VIP*/int result = _memcmp(r_bytes, q_bytes, sizeof(r));
17-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(r_bytes); @*/
18-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
14+
/*CN_VIP*//*@ to_bytes Owned<int*>(&r); @*/
15+
/*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
16+
/*CN_VIP*/int result = _memcmp((unsigned char*)&r, (unsigned char*)&q, sizeof(r));
17+
/*CN_VIP*//*@ from_bytes Owned<int*>(&r); @*/
18+
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
19+
#ifdef NO_ROUND_TRIP
20+
/*CN_VIP*/r = __cerbvar_copy_alloc_id((uintptr_t)r, &x);
21+
#endif
1922
if (result == 0) {
2023
*r = 11; // is this free of UB?
2124
//CN_VIP printf("y=%d *q=%d *r=%d\n",y,*q,*r);

‎tests/cn_vip_testsuite/provenance_basic_auto_yx.error.c

+9-6
Original file line numberDiff line numberDiff line change
@@ -7,13 +7,16 @@ int main() {
77
int *p = &x + 1;
88
int *q = &y;
99
//CN_VIP printf("Addresses: p=%p q=%p\n",(void*)p,(void*)q);
10-
/*CN_VIP*/unsigned char* p_bytes = owned_int_ptr_to_owned_uchar_arr(&p);
11-
/*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
12-
/*CN_VIP*/int result = _memcmp(p_bytes, q_bytes, sizeof(p));
13-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(p_bytes); @*/
14-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
10+
/*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
11+
/*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
12+
/*CN_VIP*/int result = _memcmp((unsigned char*)&p, (unsigned char*)&q, sizeof(p));
13+
/*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
14+
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
15+
#ifdef NO_ROUND_TRIP
16+
/*CN_VIP*/p = __cerbvar_copy_alloc_id((uintptr_t)p, &x);
17+
#endif
1518
if (result == 0) {
16-
*p = 11; // does this have undefined behaviour?
19+
*p = 11; // CN VIP UB
1720
//CN_VIP printf("x=%d y=%d *p=%d *q=%d\n",x,y,*p,*q);
1821
}
1922
}

‎tests/cn_vip_testsuite/provenance_basic_global_yx.error.c

+10-7
Original file line numberDiff line numberDiff line change
@@ -4,18 +4,21 @@
44
#include "cn_lemmas.h"
55
int y=2, x=1;
66
int main()
7-
/*CN_VIP*//*@ accesses y; @*/
7+
/*CN_VIP*//*@ accesses x; accesses y; @*/
88
{
99
int *p = &x + 1;
1010
int *q = &y;
1111
//CN_VIP printf("Addresses: p=%p q=%p\n",(void*)p,(void*)q);
12-
/*CN_VIP*/unsigned char* p_bytes = owned_int_ptr_to_owned_uchar_arr(&p);
13-
/*CN_VIP*/unsigned char* q_bytes = owned_int_ptr_to_owned_uchar_arr(&q);
14-
/*CN_VIP*/int result = _memcmp(p_bytes, q_bytes, sizeof(p));
15-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(p_bytes); @*/
16-
/*CN_VIP*//*@ apply byte_ptr_to_int_ptr_ptr(q_bytes); @*/
12+
/*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
13+
/*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
14+
/*CN_VIP*/int result = _memcmp((unsigned char *)&p, (unsigned char*)&q, sizeof(p));
15+
/*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
16+
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
17+
#ifdef NO_ROUND_TRIP
18+
/*CN_VIP*/p = __cerbvar_copy_alloc_id((uintptr_t)p, &x);
19+
#endif
1720
if (result == 0) {
18-
*p = 11; // does this have undefined behaviour?
21+
*p = 11; // CN_VIP UB
1922
//CN_VIP printf("x=%d y=%d *p=%d *q=%d\n",x,y,*p,*q);
2023
}
2124
}

‎tests/pnvi_testsuite/pointer_from_int_disambiguation_3.c

+17
Original file line numberDiff line numberDiff line change
@@ -22,3 +22,20 @@ int main() {
2222
printf("x=%d y=%d *q=%d *r=%d\n",x,y,*q,*r);
2323
}
2424
}
25+
26+
/* NOTE: vip_artifact/evaluation_cerberus/results.pdf expects for this test:
27+
28+
|----------------------+----------------------+--------------+--------------|
29+
| PNVI-ae-udi no annot | PNVI-ae-udi w/ annot | VIP no annot | VIP w/ annot |
30+
|----------------------+----------------------+--------------+--------------|
31+
| UB: line 19 | UB: line 19 | UB: line 19 | UB: line 20 |
32+
|----------------------+----------------------+--------------+--------------|
33+
34+
This doesn't make sense, because (a) comments don't line up with numbers and (b)
35+
36+
PNVI-ae-udi no annot: prov is symbolic (one-past int to pointer),
37+
collapses to q on store, so UB on line 20
38+
PNVI-ae-udi w/ annot: prov is copy_alloc_id to @q, so UB on line 20
39+
VIP no annot: prov is round-trip preserved to @p, so UB on line 19
40+
VIP w/ annot: prov is copy_alloc_id @q, so UB on line 20
41+
*/

0 commit comments

Comments
 (0)