Skip to content

Commit 670420e

Browse files
dkcummingdkcumming
committed
Added negative tests to demonstrate KMIR errors on UB path
1 parent 02c1126 commit 670420e

2 files changed

Lines changed: 56 additions & 16 deletions

File tree

‎.github/workflows/kmir.yml‎

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ on:
1313

1414
jobs:
1515
run-kmir-proofs:
16-
name: Run supplied KMIR proofs
16+
name: Run KMIR proofs
1717
runs-on: ubuntu-latest
1818
env:
1919
container_name: "kmir-${{ github.run_id }}"
@@ -31,3 +31,23 @@ jobs:
3131
-v $PWD:/home/kmir/workspace \
3232
runtimeverificationinc/kmir:ubuntu-jammy-latest \
3333
kmir-proofs/0011-floats-ints/run-proofs.sh
34+
35+
run-kmir-proofs-negative:
36+
name: Run KMIR negative proofs
37+
runs-on: ubuntu-latest
38+
env:
39+
container_name: "kmir-neg-${{ github.run_id }}"
40+
41+
steps:
42+
- name: Checkout Repository
43+
uses: actions/checkout@v4
44+
45+
- name: Run Challenge 11 Negative Proofs
46+
run: |
47+
docker run --rm -t \
48+
--name ${{ env.container_name }} \
49+
-w /home/kmir/workspace \
50+
-u $(id -u):$(id -g) \
51+
-v $PWD:/home/kmir/workspace \
52+
runtimeverificationinc/kmir:ubuntu-jammy-latest \
53+
kmir-proofs/0011-floats-ints/run-proofs.sh --negative

‎kmir-proofs/0011-floats-ints/run-proofs.sh‎

Lines changed: 35 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
#!/bin/bash
2-
# Run KMIR passing proofs for Challenge 11: Safety of Methods for Numeric Primitive Types
2+
# Run KMIR proofs for Challenge 11: Safety of Methods for Numeric Primitive Types
33
# https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html
4+
#
5+
# Usage: ./run-proofs.sh # run passing proofs
6+
# ./run-proofs.sh --negative # run negative proofs (expect failure)
47

58
set -eux
69

@@ -12,18 +15,35 @@ fi
1215
DIR=$(realpath "$(dirname "$0")")
1316
cd "$DIR"
1417

15-
PROOF_DIR=proofs
16-
rm -rf "$PROOF_DIR"
18+
if [ "${1:-}" = "--negative" ]; then
19+
PROOF_DIR=proofs-fail
20+
rm -rf "$PROOF_DIR"
1721

18-
printf '%s\n' \
19-
"kmir prove carrying_mul.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol carrying_mul_u8,carrying_mul_u16,carrying_mul_u32,carrying_mul_u64" \
20-
"kmir prove unchecked_add.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_add_u8,unchecked_add_u16,unchecked_add_u32,unchecked_add_u64,unchecked_add_u128,unchecked_add_i8,unchecked_add_i16,unchecked_add_i32,unchecked_add_i64,unchecked_add_i128" \
21-
"kmir prove widening_mul.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol widening_mul_u8,widening_mul_u16,widening_mul_u32,widening_mul_u64" \
22-
"kmir prove unchecked_sub.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_sub_u8,unchecked_sub_u16,unchecked_sub_u32,unchecked_sub_u64,unchecked_sub_u128,unchecked_sub_i8,unchecked_sub_i16,unchecked_sub_i32,unchecked_sub_i64,unchecked_sub_i128" \
23-
"kmir prove unchecked_neg.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_neg_i8,unchecked_neg_i16,unchecked_neg_i32,unchecked_neg_i64,unchecked_neg_i128" \
24-
"kmir prove unchecked_mul.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_mul_u8,unchecked_mul_u16,unchecked_mul_u32,unchecked_mul_u64,unchecked_mul_u128,unchecked_mul_i8,unchecked_mul_i16,unchecked_mul_i32,unchecked_mul_i64,unchecked_mul_i128" \
25-
"kmir prove unchecked_shl.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_shl_u8,unchecked_shl_u16,unchecked_shl_u32,unchecked_shl_u64,unchecked_shl_u128,unchecked_shl_i8,unchecked_shl_i16,unchecked_shl_i32,unchecked_shl_i64,unchecked_shl_i128" \
26-
"kmir prove unchecked_shr.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_shr_u8,unchecked_shr_u16,unchecked_shr_u32,unchecked_shr_u64,unchecked_shr_u128,unchecked_shr_i8,unchecked_shr_i16,unchecked_shr_i32,unchecked_shr_i64,unchecked_shr_i128" \
27-
"kmir prove wrapping_shl.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol wrapping_shl_u8,wrapping_shl_u16,wrapping_shl_u32,wrapping_shl_u64,wrapping_shl_u128,wrapping_shl_i8,wrapping_shl_i16,wrapping_shl_i32,wrapping_shl_i64,wrapping_shl_i128" \
28-
"kmir prove wrapping_shr.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol wrapping_shr_u8,wrapping_shr_u16,wrapping_shr_u32,wrapping_shr_u64,wrapping_shr_u128,wrapping_shr_i8,wrapping_shr_i16,wrapping_shr_i32,wrapping_shr_i64,wrapping_shr_i128" \
29-
| xargs -P 2 -I{} bash -xc '{}'
22+
# Negative tests: proofs should FAIL as KMIR detects UB.
23+
# If any proof unexpectedly passes, the script exits non-zero.
24+
printf '%s\n' \
25+
"kmir prove unchecked_add-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_add_u8,unchecked_add_u16,unchecked_add_u32,unchecked_add_u64,unchecked_add_u128,unchecked_add_i8,unchecked_add_i16,unchecked_add_i32,unchecked_add_i64,unchecked_add_i128" \
26+
"kmir prove unchecked_sub-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_sub_u8,unchecked_sub_u16,unchecked_sub_u32,unchecked_sub_u64,unchecked_sub_u128,unchecked_sub_i8,unchecked_sub_i16,unchecked_sub_i32,unchecked_sub_i64,unchecked_sub_i128" \
27+
"kmir prove unchecked_mul-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_mul_u8,unchecked_mul_u16,unchecked_mul_u32,unchecked_mul_u64,unchecked_mul_u128,unchecked_mul_i8,unchecked_mul_i16,unchecked_mul_i32,unchecked_mul_i64,unchecked_mul_i128" \
28+
"kmir prove unchecked_shl-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_shl_u8,unchecked_shl_u16,unchecked_shl_u32,unchecked_shl_u64,unchecked_shl_u128,unchecked_shl_i8,unchecked_shl_i16,unchecked_shl_i32,unchecked_shl_i64,unchecked_shl_i128" \
29+
"kmir prove unchecked_shr-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_shr_u8,unchecked_shr_u16,unchecked_shr_u32,unchecked_shr_u64,unchecked_shr_u128,unchecked_shr_i8,unchecked_shr_i16,unchecked_shr_i32,unchecked_shr_i64,unchecked_shr_i128" \
30+
"kmir prove unchecked_neg-fail.rs --terminate-on-thunk --fail-fast --proof-dir $PROOF_DIR --start-symbol unchecked_neg_i8,unchecked_neg_i16,unchecked_neg_i32,unchecked_neg_i64,unchecked_neg_i128" \
31+
| xargs -P 2 -I{} bash -xc 'if {}; then echo "ERROR: expected failure but passed: {}"; exit 1; fi'
32+
else
33+
PROOF_DIR=proofs
34+
rm -rf "$PROOF_DIR"
35+
36+
# Positive tests: proofs should PASS
37+
printf '%s\n' \
38+
"kmir prove carrying_mul.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol carrying_mul_u8,carrying_mul_u16,carrying_mul_u32,carrying_mul_u64" \
39+
"kmir prove unchecked_add.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_add_u8,unchecked_add_u16,unchecked_add_u32,unchecked_add_u64,unchecked_add_u128,unchecked_add_i8,unchecked_add_i16,unchecked_add_i32,unchecked_add_i64,unchecked_add_i128" \
40+
"kmir prove widening_mul.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol widening_mul_u8,widening_mul_u16,widening_mul_u32,widening_mul_u64" \
41+
"kmir prove unchecked_sub.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_sub_u8,unchecked_sub_u16,unchecked_sub_u32,unchecked_sub_u64,unchecked_sub_u128,unchecked_sub_i8,unchecked_sub_i16,unchecked_sub_i32,unchecked_sub_i64,unchecked_sub_i128" \
42+
"kmir prove unchecked_neg.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_neg_i8,unchecked_neg_i16,unchecked_neg_i32,unchecked_neg_i64,unchecked_neg_i128" \
43+
"kmir prove unchecked_mul.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_mul_u8,unchecked_mul_u16,unchecked_mul_u32,unchecked_mul_u64,unchecked_mul_u128,unchecked_mul_i8,unchecked_mul_i16,unchecked_mul_i32,unchecked_mul_i64,unchecked_mul_i128" \
44+
"kmir prove unchecked_shl.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_shl_u8,unchecked_shl_u16,unchecked_shl_u32,unchecked_shl_u64,unchecked_shl_u128,unchecked_shl_i8,unchecked_shl_i16,unchecked_shl_i32,unchecked_shl_i64,unchecked_shl_i128" \
45+
"kmir prove unchecked_shr.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol unchecked_shr_u8,unchecked_shr_u16,unchecked_shr_u32,unchecked_shr_u64,unchecked_shr_u128,unchecked_shr_i8,unchecked_shr_i16,unchecked_shr_i32,unchecked_shr_i64,unchecked_shr_i128" \
46+
"kmir prove wrapping_shl.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol wrapping_shl_u8,wrapping_shl_u16,wrapping_shl_u32,wrapping_shl_u64,wrapping_shl_u128,wrapping_shl_i8,wrapping_shl_i16,wrapping_shl_i32,wrapping_shl_i64,wrapping_shl_i128" \
47+
"kmir prove wrapping_shr.rs --terminate-on-thunk --proof-dir $PROOF_DIR --start-symbol wrapping_shr_u8,wrapping_shr_u16,wrapping_shr_u32,wrapping_shr_u64,wrapping_shr_u128,wrapping_shr_i8,wrapping_shr_i16,wrapping_shr_i32,wrapping_shr_i64,wrapping_shr_i128" \
48+
| xargs -P 2 -I{} bash -xc '{}'
49+
fi

0 commit comments

Comments
 (0)