Skip to content

Commit a330424

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

16 files changed

+95
-60
lines changed

‎.github/workflows/ci.yml

+8
Original file line numberDiff line numberDiff line change
@@ -127,6 +127,14 @@ jobs:
127127
cd tests; USE_OPAM='' ./run-cn-test-gen.sh
128128
cd ..
129129
130+
- name: Run CN VIP CI tests
131+
run: |
132+
opam switch ${{ matrix.version }}
133+
eval $(opam env --switch=${{ matrix.version }})
134+
cd tests; USE_OPAM='' ./run-cn-vip.sh
135+
cd ..
136+
137+
130138
- name: Install Cerberus-CHERI
131139
if: ${{ matrix.version == '4.14.1' }}
132140
run: |

‎tests/cn_vip_testsuite/pointer_arith_algebraic_properties_2_global.annot.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ int main()
77
/*@ accesses x; @*/
88
{
99
/*CN_VIP*//*@ extract Owned<int>, 1u64; @*/
10-
#if defined(ANNOT)
10+
#ifdef ANNOT
1111
int *p= copy_alloc_id(
1212
(((uintptr_t)&(x[0])) +
1313
(((uintptr_t)&(y[1]))-((uintptr_t)&(y[0]))))
@@ -17,8 +17,8 @@ int main()
1717
int *p=(int*)(((uintptr_t)&(x[0])) +
1818
(((uintptr_t)&(y[1]))-((uintptr_t)&(y[0]))));
1919
#endif
20-
*p = 11; // is this free of undefined behaviour?
21-
/*CN_VIP*//*@ assert(x[1u64] == 11i32 && *p == 11i32); @*/
20+
*p = 11; // CN VIP UB (no annot)
2221
//CN_VIP printf("x[1]=%d *p=%d\n",x[1],*p);
22+
/*CN_VIP*//*@ assert(x[1u64] == 11i32 && *p == 11i32); @*/
2323
return 0;
2424
}

‎tests/cn_vip_testsuite/pointer_arith_algebraic_properties_3_global.annot.c

+2-2
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,9 @@ int main()
1818
(((uintptr_t)&(x[0])) + ((uintptr_t)&(y[1])))
1919
-((uintptr_t)&(y[0])) );
2020
#endif
21-
*p = 11; // is this free of undefined behaviour?
21+
*p = 11; // CN VIP UB (no annot)
2222
//(equivalent to the &x[0]+(&(y[1])-&(y[0])) version?)
23-
/*CN_VIP*//*@ assert(x[1u64] == 11i32 && *p == 11i32); @*/
2423
//CN_VIP printf("x[1]=%d *p=%d\n",x[1],*p);
24+
/*CN_VIP*//*@ assert(x[1u64] == 11i32 && *p == 11i32); @*/
2525
return 0;
2626
}

‎tests/cn_vip_testsuite/pointer_copy_user_ctrlflow_bitwise.annot.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -33,12 +33,12 @@ int main()
3333
else
3434
j = j;
3535
}
36-
#if defined(ANNOT)
36+
#ifdef ANNOT
3737
q = copy_alloc_id(j, &x);
3838
#else
3939
q = (int *)j;
4040
#endif
41-
*q = 11; // is this free of undefined behaviour?
42-
/*CN_VIP*//*@ assert(*p == 11i32 && *q == 11i32); @*/
41+
*q = 11; // CN VIP UB (no annot)
4342
//CN_VIP printf("*p=%d *q=%d\n",*p,*q);
43+
/*CN_VIP*//*@ assert(*p == 11i32 && *q == 11i32); @*/
4444
}

‎tests/cn_vip_testsuite/pointer_from_integer_1ig.annot.c

+2-3
Original file line numberDiff line numberDiff line change
@@ -10,11 +10,10 @@ void f(uintptr_t i) {
1010
#if defined(ANNOT)
1111
int *p = copy_alloc_id(i, &j);
1212
#else
13-
int *p = (int*)i;
13+
int *p = (int*)i; // not even round-trip can save this
1414
#endif
15-
/*CN_VIP*//*@ assert ((alloc_id) p == (alloc_id) &j);@*/
1615
if (p==&j) {
17-
*p=7;
16+
*p=7; // CN VIP UB (no annot)
1817
/*CN_VIP*//*@ assert (j == 7i32); @*/
1918
}
2019
//CN_VIP printf("j=%d &j=%p\n",j,(void*)&j);

‎tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_xy.annot.c

+5-3
Original file line numberDiff line numberDiff line change
@@ -24,12 +24,14 @@ int main() {
2424
/*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
2525
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
2626
#ifdef NO_ROUND_TRIP
27-
/*CN_VIP*/p = copy_alloc_id((uintptr_t)p, &y);
27+
#ifdef ANNOT
28+
/*CN_VIP*/p = copy_alloc_id((uintptr_t)p, &y); // p has empty prov outside of annot
29+
#endif
2830
/*CN_VIP*/q = copy_alloc_id((uintptr_t)q, &y); // for *q in assertion
2931
#endif
3032
if (result == 0) {
31-
*p = 11; // is this free of UB?
32-
/*CN_VIP*//*@ assert (x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
33+
*p = 11; // CN VIP UB (no annot)
3334
//CN_VIP printf("x=%d y=%d *p=%d *q=%d\n",x,y,*p,*q);
35+
/*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
3436
}
3537
}

‎tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_auto_yx.annot.c

+6-4
Original file line numberDiff line numberDiff line change
@@ -20,16 +20,18 @@ int main() {
2020
int *q = &y;
2121
/*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
2222
/*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
23-
int result = _memcmp((unsigned char*)&p, (unsigned char*)&q, sizeof(p));
23+
/*CN_VIP*/int result = _memcmp((unsigned char *)&p, (unsigned char *)&q, sizeof(p));
2424
/*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
2525
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
2626
#ifdef NO_ROUND_TRIP
27-
/*CN_VIP*/p = copy_alloc_id((uintptr_t)p, &y);
27+
#ifdef ANNOT
28+
/*CN_VIP*/p = copy_alloc_id((uintptr_t)p, &y); // p has empty prov outside of annot
29+
#endif
2830
/*CN_VIP*/q = copy_alloc_id((uintptr_t)q, &y); // for *q in assertion
2931
#endif
3032
if (result == 0) {
31-
*p = 11; // is this free of UB?
33+
*p = 11; // CN VIP UB (no annot)
3234
//CN_VIP printf("x=%d y=%d *p=%d *q=%d\n",x,y,*p,*q);
33-
/*CN_VIP*/ /*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
35+
/*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
3436
}
3537
}

‎tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_xy.annot.c

+6-4
Original file line numberDiff line numberDiff line change
@@ -22,16 +22,18 @@ int main()
2222
int *q = &y;
2323
/*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
2424
/*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
25-
/*CN_VIP*/int result = _memcmp((unsigned char*)&p, (unsigned char*)&q, sizeof(p));
25+
/*CN_VIP*/int result = _memcmp((unsigned char *)&p, (unsigned char *)&q, sizeof(p));
2626
/*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
2727
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
2828
#ifdef NO_ROUND_TRIP
29-
/*CN_VIP*/p = copy_alloc_id((uintptr_t)p, &y);
29+
#ifdef ANNOT
30+
/*CN_VIP*/p = copy_alloc_id((uintptr_t)p, &y); // p has empty prov outside of annot
31+
#endif
3032
/*CN_VIP*/q = copy_alloc_id((uintptr_t)q, &y); // for *q in assertion
3133
#endif
3234
if (result == 0) {
33-
*p = 11; // is this free of UB?
35+
*p = 11; // CN VIP UB (no annot)
3436
//CN_VIP printf("x=%d y=%d *p=%d *q=%d\n",x,y,*p,*q);
35-
/*@ assert (x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
37+
/*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
3638
}
3739
}

‎tests/cn_vip_testsuite/pointer_offset_from_int_subtraction_global_yx.annot.c

+6-5
Original file line numberDiff line numberDiff line change
@@ -20,19 +20,20 @@ int main()
2020
int *p = (int *)(ux + offset);
2121
#endif
2222
int *q = &y;
23-
2423
/*CN_VIP*//*@ to_bytes Owned<int*>(&p); @*/
2524
/*CN_VIP*//*@ to_bytes Owned<int*>(&q); @*/
26-
/*CN_VIP*/int result = _memcmp((unsigned char*)&p, (unsigned char*)&q, sizeof(p));
25+
/*CN_VIP*/int result = _memcmp((unsigned char *)&p, (unsigned char *)&q, sizeof(p));
2726
/*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
2827
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
2928
#ifdef NO_ROUND_TRIP
30-
/*CN_VIP*/p = copy_alloc_id((uintptr_t)p, &y);
29+
#ifdef ANNOT
30+
/*CN_VIP*/p = copy_alloc_id((uintptr_t)p, &y); // p has empty prov outside of annot
31+
#endif
3132
/*CN_VIP*/q = copy_alloc_id((uintptr_t)q, &y); // for *q in assertion
3233
#endif
3334
if (result == 0) {
34-
*p = 11; // is this free of UB?
35+
*p = 11; // CN VIP UB (no annot)
3536
//CN_VIP printf("x=%d y=%d *p=%d *q=%d\n",x,y,*p,*q);
36-
/*CN_VIP*/ /*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
37+
/*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
3738
}
3839
}

‎tests/cn_vip_testsuite/pointer_offset_xor_auto.annot.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,11 @@ int main() {
1313
#if defined(ANNOT)
1414
int *r = copy_alloc_id(l, q);
1515
#else
16-
int *r = (int *)l;
16+
int *r = (int *)l; // VIP roundtrip provenance is not preserved via operations
1717
#endif
1818
// are r and q now equivalent?
19-
*r = 11; // does this have defined behaviour?
19+
*r = 11; // CN VIP UB (no annot)
2020
_Bool b = (r==q);
21-
/*CN_VIP*//*@ assert (x == 1i32 && y == 11i32 && *r == 11i32 && b == 1u8); @*/
2221
//CN_VIP printf("x=%i y=%i *r=%i (r==p)=%s\n",x,y,*r, b?"true":"false");
22+
/*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *r == 11i32 && b == 1u8); @*/
2323
}

‎tests/cn_vip_testsuite/pointer_offset_xor_global.annot.c

+2-2
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,8 @@ int main()
1919
int *r = (int *)l;
2020
#endif
2121
// are r and q now equivalent?
22-
*r = 11; // does this have defined behaviour?
22+
*r = 11; // CN VIP UB (no annot)
2323
_Bool b = (r==q);
24-
/*CN_VIP*//*@ assert (x == 1i32 && y == 11i32 && *r == 11i32 && b == 1u8); @*/
2524
//CN_VIP printf("x=%i y=%i *r=%i (r==p)=%s\n",x,y,*r, b?"true":"false");
25+
/*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *r == 11i32 && b == 1u8); @*/
2626
}

‎tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_auto_yx.annot.c

+6-2
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@
77
#include "cn_lemmas.h"
88
int main() {
99
int y=2, x=1;
10+
11+
1012
uintptr_t ux = (uintptr_t)&x;
1113
uintptr_t uy = (uintptr_t)&y;
1214
uintptr_t offset = 4;
@@ -26,12 +28,14 @@ int main() {
2628
/*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
2729
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
2830
#ifdef NO_ROUND_TRIP
31+
#ifdef ANNOT
2932
/*CN_VIP*/p = copy_alloc_id((uintptr_t)p, &y);
33+
#endif
3034
/*CN_VIP*/q = copy_alloc_id((uintptr_t)q, &y); // for *q in assertion
3135
#endif
3236
if (result == 0) {
33-
*p = 11; // does this have undefined behaviour?
34-
/*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
37+
*p = 11; // CN VIP UB (no annot)
3538
//CN_VIP printf("x=%d y=%d *p=%d *q=%d\n",x,y,*p,*q);
39+
/*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
3640
}
3741
}

‎tests/cn_vip_testsuite/provenance_basic_using_uintptr_t_global_yx.annot.c

+5-3
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ int main()
1414
uintptr_t offset = 4;
1515
ux = ux + offset;
1616
/*@ apply assert_equal((u64) ux, uy); @*/
17-
#if defined(ANNOT)
17+
#ifdef ANNOT
1818
int *p = copy_alloc_id(ux, &y);
1919
#else
2020
int *p = (int *)ux; // does this have undefined behaviour?
@@ -28,12 +28,14 @@ int main()
2828
/*CN_VIP*//*@ from_bytes Owned<int*>(&p); @*/
2929
/*CN_VIP*//*@ from_bytes Owned<int*>(&q); @*/
3030
#ifdef NO_ROUND_TRIP
31+
#ifdef ANNOT
3132
/*CN_VIP*/p = copy_alloc_id((uintptr_t)p, &y);
33+
#endif
3234
/*CN_VIP*/q = copy_alloc_id((uintptr_t)q, &y); // for *q in assertion
3335
#endif
3436
if (result == 0) {
35-
*p = 11; // does this have undefined behaviour?
36-
/*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
37+
*p = 11; // CN VIP UB (no annot)
3738
//CN_VIP printf("x=%d y=%d *p=%d *q=%d\n",x,y,*p,*q);
39+
/*CN_VIP*//*@ assert(x == 1i32 && y == 11i32 && *p == 11i32 && *q == 11i32); @*/
3840
}
3941
}

‎tests/cn_vip_testsuite/provenance_lost_escape_1.annot.c

+3-3
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ int main()
1414
uintptr_t i2 = i1 & 0x00000000FFFFFFFF;//
1515
uintptr_t i3 = i2 & 0xFFFFFFFF00000000;// (@1,0x0)
1616
uintptr_t i4 = i3 + ADDR_PLE_1; // (@1,ADDR_PLE_1)
17-
/*@ apply assert_equal(i4, (u64)&x); @*/
17+
/*CN_VIP*//*@ apply assert_equal(i4, (u64)&x); @*/
1818
#ifdef ANNOT
1919
int *q = copy_alloc_id(i4, p);
2020
#else
@@ -27,8 +27,8 @@ int main()
2727
/*CN_VIP*//*@ from_bytes Owned<uintptr_t>(&i1); @*/
2828
/*CN_VIP*//*@ from_bytes Owned<uintptr_t>(&i4); @*/
2929
if (result == 0) {
30-
*q = 11; // does this have defined behaviour?
31-
/*CN_VIP*//*@ assert(x == 11i32 && *p == 11i32 && *q == 11i32); @*/
30+
*q = 11; // CN VIP UB (no annot)
3231
//CN_VIP printf("x=%d *p=%d *q=%d\n",x,*p,*q);
32+
/*CN_VIP*//*@ assert(x == 11i32 && *p == 11i32 && *q == 11i32); @*/
3333
}
3434
}

‎tests/cn_vip_testsuite/provenance_tag_bits_via_uintptr_t_1.annot.c

+4-4
Original file line numberDiff line numberDiff line change
@@ -17,22 +17,22 @@ int main()
1717
// construct an integer like &x with low-order bit set
1818
i = i | 1u;
1919
// cast back to a pointer
20-
#if defined(ANNOT)
20+
#ifdef ANNOT
2121
int *q = copy_alloc_id(i, p);
2222
#else
2323
int *q = (int *) i; // does this have defined behaviour?
2424
#endif
2525
// cast to integer and mask out the low-order two bits
2626
uintptr_t j = ((uintptr_t)q) & ~((uintptr_t)3u);
2727
// cast back to a pointer
28-
#if defined(ANNOT)
28+
#ifdef ANNOT
2929
int *r = copy_alloc_id(j, p);
3030
#else
3131
int *r = (int *) j;
3232
#endif
3333
// are r and p now equivalent?
34-
*r = 11; // does this have defined behaviour?
34+
*r = 11; // CN VIP UB (no annot)
3535
_Bool b = (r==p); // is this true?
36-
/*CN_VIP*//*@ assert (x == 11i32 && *r == 11i32 && b == 1u8); @*/
3736
//CN_VIP printf("x=%i *r=%i (r==p)=%s\n",x,*r,b?"true":"false");
37+
/*CN_VIP*//*@ assert(x == 11i32 && *r == 11i32 && b == 1u8); @*/
3838
}

‎tests/run-cn-vip.sh

+31-16
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ function exits_with_code() {
3333
local -a expected_exit_codes=$3
3434

3535
printf "[$file]...\n"
36-
timeout 15 ${action} "$file"
36+
timeout 35 ${action} "$file" &> /dev/null
3737
local result=$?
3838

3939
for code in "${expected_exit_codes[@]}"; do
@@ -51,32 +51,48 @@ DIRNAME=$(dirname "$0")
5151

5252
SUCC=$(
5353
find $DIRNAME/cn_vip_testsuite -name '*.c' \
54+
\! -name '*union*.c' \
55+
\! -name '*.unprovable.c' \
5456
\! -name '*.annot.c' \
5557
\! -name '*.error.c' \
5658
)
57-
FAIL=$(find $DIRNAME/cn_vip_testsuite -name '*.error.c')
59+
UNION=$(find $DIRNAME/cn_vip_testsuite -name '*union*.c')
60+
UNPROV=$(find $DIRNAME/cn_vip_testsuite -name '*.unprovable.c' \
61+
\! -name 'pointer_copy_user_ctrlflow_bytewise.unprovable.c')
62+
# this test hits a CN performance bug
63+
FAIL=$(find $DIRNAME/cn_vip_testsuite -name '*.error.c' \! -name '*union*.c')
5864
ANNOT=$(find $DIRNAME/cn_vip_testsuite -name '*.annot.c')
5965

6066
FAILED=''
6167

62-
# for TEST in ${SUCC} ${ANNOT}; do
63-
# if ! exits_with_code "cn verify -DVIP -DANNOT -DNO_ROUND_TRIP --solver-type=cvc5" "${TEST}" 0; then
64-
# FAILED+=" ${TEST}"
65-
# fi
66-
# done
67-
68-
# TODO add below with both -DNON_DET_TRUE and -DNON_DET_FALSE
69-
# provenance_equality_auto_yx.c
70-
# provenance_equality_global_fn_yx.c
71-
# provenance_equality_global_yx.c
68+
for TEST in ${SUCC} ${ANNOT}; do
69+
if ! exits_with_code "cn verify -DVIP -DANNOT -DNO_ROUND_TRIP --solver-type=cvc5" "${TEST}" 0; then
70+
FAILED+=" ${TEST}"
71+
fi
72+
done
7273

73-
for TEST in $FAIL $ANNOT
74-
do
75-
if ! exits_with_code "cn verify -DNO_ROUND_TRIP --solver-type=cvc5" "${TEST}" 1; then
74+
for TEST in $FAIL $ANNOT $UNPROV; do
75+
if ! exits_with_code "cn verify -DVIP -DNO_ROUND_TRIP --solver-type=cvc5" "${TEST}" 1; then
7676
FAILED+=" ${TEST}"
7777
fi
7878
done
7979

80+
81+
NON_DET=(
82+
$DIRNAME/provenance_equality_auto_yx.c \
83+
$DIRNAME/provenance_equality_global_fn_yx.c \
84+
$DIRNAME/provenance_equality_global_yx.c \
85+
)
86+
87+
for TEST in $NON_DET; do
88+
if ! exits_with_code "cn verify -DVIP -DNO_ROUND_TRIP -DNON_DET_TRUE --solver-type=cvc5" "${TEST}" 1; then
89+
FAILED+=" ${TEST} (nd. true)"
90+
fi
91+
if ! exits_with_code "cn verify -DVIP -DNO_ROUND_TRIP -DNON_DET_FALSE --solver-type=cvc5" "${TEST}" 1; then
92+
FAILED+=" ${TEST} (nd. false)"
93+
fi
94+
done
95+
8096
if [ -z "${FAILED}" ]; then
8197
exit 0
8298
else
@@ -85,4 +101,3 @@ else
85101
fi
86102

87103

88-

0 commit comments

Comments
 (0)