Skip to content

Commit 9e5dd9d

Browse files
dkcummingdkcumming
committed
Added parallel execution of 2 for run-proofs.sh
2 should be fine for a public github runner. I attempted to interleave the proofs that are different so that the expensive `llvm-kompile` calls will happen at different times.
1 parent be2c7e9 commit 9e5dd9d

1 file changed

Lines changed: 13 additions & 62 deletions

File tree

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

Lines changed: 13 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
# Run KMIR passing 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
44

5-
set -eu
5+
set -eux
66

77
if ! command -v kmir &> /dev/null; then
88
echo "ERROR: kmir not found on PATH"
@@ -15,64 +15,15 @@ cd "$DIR"
1515
PROOF_DIR=proofs
1616
rm -rf "$PROOF_DIR"
1717

18-
FAILED_FILES=""
19-
20-
kmir prove unchecked_add.rs --terminate-on-thunk --proof-dir "$PROOF_DIR" \
21-
--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 \
22-
|| FAILED_FILES="$FAILED_FILES unchecked_add"
23-
24-
kmir prove unchecked_sub.rs --terminate-on-thunk --proof-dir "$PROOF_DIR" \
25-
--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 \
26-
|| FAILED_FILES="$FAILED_FILES unchecked_sub"
27-
28-
kmir prove unchecked_mul.rs --terminate-on-thunk --proof-dir "$PROOF_DIR" \
29-
--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 \
30-
|| FAILED_FILES="$FAILED_FILES unchecked_mul"
31-
32-
kmir prove unchecked_shl.rs --terminate-on-thunk --proof-dir "$PROOF_DIR" \
33-
--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 \
34-
|| FAILED_FILES="$FAILED_FILES unchecked_shl"
35-
36-
kmir prove unchecked_shr.rs --terminate-on-thunk --proof-dir "$PROOF_DIR" \
37-
--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 \
38-
|| FAILED_FILES="$FAILED_FILES unchecked_shr"
39-
40-
kmir prove unchecked_neg.rs --terminate-on-thunk --proof-dir "$PROOF_DIR" \
41-
--start-symbol unchecked_neg_i8,unchecked_neg_i16,unchecked_neg_i32,unchecked_neg_i64,unchecked_neg_i128 \
42-
|| FAILED_FILES="$FAILED_FILES unchecked_neg"
43-
44-
kmir prove wrapping_shl.rs --terminate-on-thunk --proof-dir "$PROOF_DIR" \
45-
--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 \
46-
|| FAILED_FILES="$FAILED_FILES wrapping_shl"
47-
48-
kmir prove wrapping_shr.rs --terminate-on-thunk --proof-dir "$PROOF_DIR" \
49-
--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 \
50-
|| FAILED_FILES="$FAILED_FILES wrapping_shr"
51-
52-
kmir prove widening_mul.rs --terminate-on-thunk --proof-dir "$PROOF_DIR" \
53-
--start-symbol widening_mul_u8,widening_mul_u16,widening_mul_u32,widening_mul_u64 \
54-
|| FAILED_FILES="$FAILED_FILES widening_mul"
55-
56-
kmir prove carrying_mul.rs --terminate-on-thunk --proof-dir "$PROOF_DIR" \
57-
--start-symbol carrying_mul_u8,carrying_mul_u16,carrying_mul_u32,carrying_mul_u64 \
58-
|| FAILED_FILES="$FAILED_FILES carrying_mul"
59-
60-
echo ""
61-
echo "========================================="
62-
echo "SUMMARY"
63-
echo "========================================="
64-
65-
if [ -n "$FAILED_FILES" ]; then
66-
echo ""
67-
echo "FAILED:$FAILED_FILES"
68-
echo ""
69-
echo -e "\033[31m=========================================\033[0m"
70-
echo -e "\033[31mSOME PROOFS FAILED\033[0m"
71-
echo -e "\033[31m=========================================\033[0m"
72-
exit 1
73-
fi
74-
75-
echo ""
76-
echo -e "\033[32m=========================================\033[0m"
77-
echo -e "\033[32mALL PROOFS PASSED\033[0m"
78-
echo -e "\033[32m=========================================\033[0m"
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 '{}'

0 commit comments

Comments
 (0)