Use CBMC 6.0.0 (#1128)

**Issue:** The proofs broke unexpectedly when CBMC 6.0.0 was released, since we were using "latest". We pinned the version back to 5.95.1 in a [recent PR](#1124) to get CI working again. **Description of changes:** - Upgrade to CBMC 6.0.0 - For all tools used in proofs, stop using "latest". Pin the exact version, so we're not caught off-guard by unexpected upgrades again in the future - Fix proof code to work with CBMC 6
awslabs · Jun 19, 2024 · 957c760 · 957c760
1 parent 7f3b33e
commit 957c760
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 7 deletions.
diff --git a/.github/workflows/proof_ci_resources/config.yaml b/.github/workflows/proof_ci_resources/config.yaml
@@ -1,7 +1,8 @@
-cadical-tag: latest
-cbmc-version: "5.95.1"
-cbmc-viewer-version: latest
-kissat-tag: latest
-litani-version: latest
+# Use exact versions (instead of "latest") so we're not broken by surprise upgrades.
+cadical-tag: "rel-2.0.0" # tag of latest release: https://github.com/arminbiere/cadical/releases
+cbmc-version: "6.0.0" # semver of latest release: https://github.com/diffblue/cbmc/releases
+cbmc-viewer-version: "3.8" # semver of latest release: https://github.com/model-checking/cbmc-viewer/releases
+kissat-tag: "rel-3.1.1" # tag of latest release: https://github.com/arminbiere/kissat/releases
+litani-version: "1.29.0" # semver of latest release: https://github.com/awslabs/aws-build-accumulator/releases
 proofs-dir: verification/cbmc/proofs
 run-cbmc-proofs-command: ./run-cbmc-proofs.py
diff --git a/verification/cbmc/proofs/Makefile.common b/verification/cbmc/proofs/Makefile.common
@@ -465,7 +465,6 @@ COMMA :=,
 # Set C compiler defines
 
 CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
-COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS)
 
 DEFINES += -DCBMC=1
 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)

diff --git a/verification/cbmc/sources/utils.c b/verification/cbmc/sources/utils.c
@@ -170,4 +170,7 @@ uint64_t uninterpreted_hasher(const void *a) {
     return __CPROVER_uninterpreted_hasher(a);
 }
 
-bool uninterpreted_predicate_fn(uint8_t value);
+bool __CPROVER_uninterpreted_predicate_uint8_t(uint8_t);
+bool uninterpreted_predicate_fn(uint8_t value) {
+    return __CPROVER_uninterpreted_predicate_uint8_t(value);
+}