Skip to content

Commit 8bd08a0

Browse files
mkannwischerhanno-becker
mkannwischer
authored and
hanno-becker
committed
CBMC: Use a second solver for 149/215 proofs
A soundness bug in a single SMT solver would silently invalidate every proof discharged by it. To mitigate this risk, we aim to have each proof discharged by at least two solvers. 149 of 215 proofs gain a second solver: 98 bitwuzla, 25 cvc5_arrays_exp, and 26 Z3 profiles alongside a bitwuzla or cvc5 default. The other 66 do not, mostly because bitwuzla timed out or cvc5 returned unknown, either under a local 300s per-proof cap or in CI. Signed-off-by: Matthias J. Kannwischer <matthias@zerorisc.com>
1 parent ac20756 commit 8bd08a0

149 files changed

Lines changed: 447 additions & 149 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎proofs/cbmc/H/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,9 @@ APPLY_LOOP_CONTRACTS=on
3030
USE_DYNAMIC_FRAMES=1
3131

3232
# Supported CBMC configurations
33-
CBMC_SUPPORTED_CONFIGS = LP64:z3
33+
CBMC_SUPPORTED_CONFIGS = \
34+
LP64:z3 \
35+
LP64:bitwuzla
3436
CBMC_DEFAULT_CONFIG = LP64:z3
3537

3638
FUNCTION_NAME = mld_h

‎proofs/cbmc/caddq/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on
2626
USE_DYNAMIC_FRAMES=1
2727

2828
# Supported CBMC configurations
29-
CBMC_SUPPORTED_CONFIGS = LP64:z3
29+
CBMC_SUPPORTED_CONFIGS = \
30+
LP64:z3 \
31+
LP64:bitwuzla
3032
CBMC_DEFAULT_CONFIG = LP64:z3
3133

3234
FUNCTION_NAME = caddq

‎proofs/cbmc/check_pct/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,9 @@ APPLY_LOOP_CONTRACTS=on
2828
USE_DYNAMIC_FRAMES=1
2929

3030
# Supported CBMC configurations
31-
CBMC_SUPPORTED_CONFIGS = LP64:z3
31+
CBMC_SUPPORTED_CONFIGS = \
32+
LP64:z3 \
33+
LP64:bitwuzla
3234
CBMC_DEFAULT_CONFIG = LP64:z3
3335

3436
FUNCTION_NAME = mld_check_pct

‎proofs/cbmc/ct_cmask_neg_i32/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

2727
# Supported CBMC configurations
28-
CBMC_SUPPORTED_CONFIGS = LP64:z3
28+
CBMC_SUPPORTED_CONFIGS = \
29+
LP64:z3 \
30+
LP64:cvc5_arrays_exp
2931
CBMC_DEFAULT_CONFIG = LP64:z3
3032

3133
FUNCTION_NAME = mld_ct_cmask_neg_i32

‎proofs/cbmc/ct_cmask_nonzero_u32/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

2727
# Supported CBMC configurations
28-
CBMC_SUPPORTED_CONFIGS = LP64:z3
28+
CBMC_SUPPORTED_CONFIGS = \
29+
LP64:z3 \
30+
LP64:cvc5_arrays_exp
2931
CBMC_DEFAULT_CONFIG = LP64:z3
3032

3133
FUNCTION_NAME = mld_ct_cmask_nonzero_u32

‎proofs/cbmc/ct_cmask_nonzero_u8/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on
2626
USE_DYNAMIC_FRAMES=1
2727

2828
# Supported CBMC configurations
29-
CBMC_SUPPORTED_CONFIGS = LP64:z3
29+
CBMC_SUPPORTED_CONFIGS = \
30+
LP64:z3 \
31+
LP64:bitwuzla
3032
CBMC_DEFAULT_CONFIG = LP64:z3
3133

3234
FUNCTION_NAME = mld_ct_cmask_nonzero_u8

‎proofs/cbmc/ct_get_optblocker_i64/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

2727
# Supported CBMC configurations
28-
CBMC_SUPPORTED_CONFIGS = LP64:z3
28+
CBMC_SUPPORTED_CONFIGS = \
29+
LP64:z3 \
30+
LP64:bitwuzla
2931
CBMC_DEFAULT_CONFIG = LP64:z3
3032

3133
FUNCTION_NAME = mld_ct_get_optblocker_i64

‎proofs/cbmc/ct_get_optblocker_u32/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

2727
# Supported CBMC configurations
28-
CBMC_SUPPORTED_CONFIGS = LP64:z3
28+
CBMC_SUPPORTED_CONFIGS = \
29+
LP64:z3 \
30+
LP64:bitwuzla
2931
CBMC_DEFAULT_CONFIG = LP64:z3
3032

3133
FUNCTION_NAME = mld_ct_get_optblocker_u32

‎proofs/cbmc/ct_get_optblocker_u8/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,9 @@ APPLY_LOOP_CONTRACTS=on
2525
USE_DYNAMIC_FRAMES=1
2626

2727
# Supported CBMC configurations
28-
CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla
28+
CBMC_SUPPORTED_CONFIGS = \
29+
LP64:bitwuzla \
30+
LP64:z3_smt_only
2931
CBMC_DEFAULT_CONFIG = LP64:bitwuzla
3032

3133
FUNCTION_NAME = mld_ct_get_optblocker_u8

‎proofs/cbmc/ct_memcmp/Makefile‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,9 @@ APPLY_LOOP_CONTRACTS=on
2626
USE_DYNAMIC_FRAMES=1
2727

2828
# Supported CBMC configurations
29-
CBMC_SUPPORTED_CONFIGS = LP64:bitwuzla
29+
CBMC_SUPPORTED_CONFIGS = \
30+
LP64:bitwuzla \
31+
LP64:z3_no_bv_extract
3032
CBMC_DEFAULT_CONFIG = LP64:bitwuzla
3133

3234
FUNCTION_NAME = mld_ct_memcmp

0 commit comments

Comments
 (0)