Skip to content

Commit 41cbc24

Browse files
committed
Adjust proof tooling to support CBMC v6
With CBMC v6, unwinding assertions are enabled by default, and object bits no longer need to be set at compile time. Update various build rules to use the latest template as provided with CBMC starter kit. Also fixes missing function definitions.
1 parent a5cd1c0 commit 41cbc24

File tree

35 files changed

+495
-213
lines changed

35 files changed

+495
-213
lines changed

.github/workflows/ci.yml

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -261,8 +261,7 @@ jobs:
261261
- name: Set up CBMC runner
262262
uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main
263263
with:
264-
cbmc_version: "5.61.0"
265-
cbmc_viewer_version: "3.5"
264+
cbmc_version: "6.3.1"
266265
- name: Install cmake
267266
run: |
268267
sudo apt-get install -y cmake

source/core_pkcs11.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,7 @@
3030
/* C runtime includes. */
3131
#include <stdio.h>
3232
#include <stdint.h>
33+
#include <stdlib.h>
3334
#include <string.h>
3435

3536
/**

test/cbmc/proofs/C_CloseSession/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_CloseSession_harness
99
PROOF_UID = C_CloseSession
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1414

1515
REMOVE_FUNCTION_BODY += C_Finalize
1616
REMOVE_FUNCTION_BODY += C_GetFunctionList

test/cbmc/proofs/C_CreateObject/Makefile

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,11 +25,14 @@ MAX_LABEL_SIZE=32
2525
# Should be one more than the total number of objects in the PKCS stack.
2626
MAX_OBJECT_NUM=2
2727

28+
CBMC_OBJECT_BITS = 9
29+
2830
DEFINES += -DTEMPLATE_SIZE=$(TEMPLATE_SIZE)
2931
DEFINES += -DTEMPLATE_ATTRIBUTE_MAX_SIZE=$(TEMPLATE_ATTRIBUTE_MAX_SIZE)
3032

31-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
3233
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
34+
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
35+
INCLUDES += -I$(SRCDIR)/source/portable/os
3336

3437
REMOVE_FUNCTION_BODY += C_Initialize
3538
REMOVE_FUNCTION_BODY += C_Finalize
@@ -61,5 +64,6 @@ PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
6164
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c
6265
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c
6366
PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c
67+
PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c
6468

6569
include ../Makefile.common

test/cbmc/proofs/C_DestroyObject/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,8 @@ MAX_LABEL_SIZE=32
1616

1717
DEFINES += -DMAX_OBJECT_NUM=$(MAX_OBJECT_NUM)
1818

19-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
2019
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
20+
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
2121

2222
REMOVE_FUNCTION_BODY += C_Finalize
2323
REMOVE_FUNCTION_BODY += C_GetFunctionList

test/cbmc/proofs/C_DigestFinal/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_DigestFinal_harness
99
PROOF_UID = C_DigestFinal
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1414

1515
REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=

test/cbmc/proofs/C_DigestInit/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_DigestInit_harness
99
PROOF_UID = C_DigestInit
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1414

1515
REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=

test/cbmc/proofs/C_DigestUpdate/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_DigestUpdate_harness
99
PROOF_UID = C_DigestUpdate
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1414

1515
REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=

test/cbmc/proofs/C_Finalize/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ HARNESS_FILE = C_Finalize_harness
99
PROOF_UID = C_Finalize
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1414

1515
REMOVE_FUNCTION_BODY +=
1616
UNWINDSET +=

test/cbmc/proofs/C_FindObjects/Makefile

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,20 +9,24 @@ HARNESS_FILE = C_FindObjects_harness
99
PROOF_UID = C_FindObjects
1010

1111
DEFINES +=
12-
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
1312
INCLUDES += -I$(SRCDIR)/source/dependency/3rdparty/mbedtls_utils
13+
INCLUDES += -I$(SRCDIR)/test/build/_deps/mbedtls_2-src/include
14+
INCLUDES += -I$(SRCDIR)/source/portable/os
1415

1516
REMOVE_FUNCTION_BODY += C_Finalize
1617
REMOVE_FUNCTION_BODY += C_GetFunctionList
1718

1819
# This should be similar to the dummy data length in "core_pkcs11_pal_stubs.c" PKCS11_PAL_GetObjectValue
1920
UNWINDSET += __CPROVER_file_local_core_pkcs11_mbedtls_c_prvFindObjectInListByLabel.0:13
21+
UNWINDSET += strncmp.0:20
2022
# This should align with the max object count configured in core_pkcs11_config.h
2123
UNWINDSET += __CPROVER_file_local_core_pkcs11_mbedtls_c_prvAddObjectToList.0:2
2224

2325
PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
2426
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/core_pkcs11_pal_stubs.c
2527
PROOF_SOURCES += $(SRCDIR)/test/cbmc/stubs/mbedtls_stubs.c
2628
PROJECT_SOURCES += $(SRCDIR)/source/portable/mbedtls/core_pkcs11_mbedtls.c
29+
PROJECT_SOURCES += $(SRCDIR)/source/portable/os/posix/core_pkcs11_pal.c
30+
PROJECT_SOURCES += $(SRCDIR)/source/portable/os/core_pkcs11_pal_utils.c
2731

2832
include ../Makefile.common

0 commit comments

Comments
 (0)