Update cbmc 6.3.1 (#150)

* Update NIX config and Makefile.common for CBMC 6.3.1 Signed-off-by: Rod Chapman <[email protected]> * Update CBMC patch in Nix flake Signed-off-by: Hanno Becker <[email protected]> --------- Signed-off-by: Rod Chapman <[email protected]> Signed-off-by: Hanno Becker <[email protected]> Co-authored-by: Rod Chapman <[email protected]>
pq-code-package · Sep 23, 2024 · 9beb961 · 9beb961
1 parent 58076a5
commit 9beb961
Show file tree

Hide file tree

Showing 4 changed files with 56 additions and 35 deletions.
diff --git a/cbmc/0001-Do-not-download-sources-in-cmake.patch b/cbmc/0001-Do-not-download-sources-in-cmake.patch
@@ -9,8 +9,8 @@ index 003a0d957b..79751ef8b2 100644
 
 -        download_project(PROJ cadical
 -            URL https://github.com/arminbiere/cadical/archive/rel-2.0.0.tar.gz
--            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/../scripts/cadical-2.0.0-patch
--            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/../scripts/cadical_CMakeLists.txt CMakeLists.txt
+-            PATCH_COMMAND patch -p1 -i ${CBMC_SOURCE_DIR}/scripts/cadical-2.0.0-patch
+-            COMMAND cmake -E copy ${CBMC_SOURCE_DIR}/scripts/cadical_CMakeLists.txt CMakeLists.txt
 -            COMMAND ./configure
 -            URL_MD5 9fc2a66196b86adceb822a583318cc35
 -        )
@@ -28,4 +28,3 @@ index 003a0d957b..79751ef8b2 100644
          )
 
          target_link_libraries(solvers cadical)
-
diff --git a/cbmc/default.nix b/cbmc/default.nix
@@ -6,12 +6,12 @@
 }:
 builtins.attrValues {
   cbmc = cbmc.overrideAttrs (old: rec {
-    version = "6.2.0"; # remember to adjust this in ../flake.nix too
+    version = "6.3.1"; # remember to adjust this in ../flake.nix too
     src = fetchFromGitHub {
       owner = "diffblue";
       repo = old.pname;
       rev = "${old.pname}-${version}";
-      hash = "sha256-WktGmkQpd7OXYEPgv0v7/+vwhTm1rERrjXIe6dzelFA=";
+      hash = "sha256-y3avPsVxtxSV+WB8TBbvnaNZ4WZltGRTcD+GPwTlp2E=";
     };
     patches = [
       ./0001-Do-not-download-sources-in-cmake.patch

diff --git a/cbmc/proofs/Makefile.common b/cbmc/proofs/Makefile.common
@@ -1,12 +1,10 @@
-# SPDX-License-Identifier: Apache-2.0
-
 # -*- mode: makefile -*-
 # The first line sets the emacs major mode to Makefile
 
 # Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
-# SPDX-License-Identifier: MIT-0 AND Apache-2.0
+# SPDX-License-Identifier: MIT-0
 
-CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.10
+CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.11
 
 ################################################################
 # The CBMC Starter Kit depends on the files Makefile.common and
@@ -213,10 +211,13 @@ CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER)
 
 ifeq ($(strip $(ENABLE_POOLS)),)
   POOL =
+  INIT_POOLS =
 else ifeq ($(strip $(EXPENSIVE)),)
   POOL =
+  INIT_POOLS =
 else
   POOL = --pool expensive
+  INIT_POOLS = --pools expensive:1
 endif
 
 # Similar to the pool feature above. If Litani is new enough, enable
@@ -231,36 +232,43 @@ endif
 #
 # Each variable below controls a specific property checking flag
 # within CBMC. If desired, a property flag can be disabled within
-# a particular proof by nulling the corresponding variable. For
-# instance, the following line:
+# a particular proof by nulling the corresponding variable when CBMC's default
+# is not to perform such checks, or setting to --no-<CHECK>-check when CBMC's
+# default is to perform such checks. For instance, the following lines:
 #
-#     CHECK_FLAG_POINTER_CHECK =
+#     CBMC_FLAG_POINTER_CHECK = --no-pointer-check
+#     CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK =
 #
-# would disable the --pointer-check CBMC flag within:
+# would disable pointer checks and unsigned overflow checks with CBMC flag
+# within:
 #   * an entire project when added to Makefile-project-defines
 #   * a specific proof when added to the harness Makefile
 
-CBMC_FLAG_MALLOC_MAY_FAIL ?= --malloc-may-fail
-CBMC_FLAG_MALLOC_FAIL_NULL ?= --malloc-fail-null
-CBMC_FLAG_BOUNDS_CHECK ?= --bounds-check
+CBMC_FLAG_MALLOC_MAY_FAIL ?= # set to --no-malloc-may-fail to disable
+CBMC_FLAG_BOUNDS_CHECK ?= # set to --no-bounds-check to disable
 CBMC_FLAG_CONVERSION_CHECK ?= --conversion-check
-CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check
+CBMC_FLAG_DIV_BY_ZERO_CHECK ?= # set to --no-div-by-zero-check to disable
 CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check
 CBMC_FLAG_NAN_CHECK ?= --nan-check
-CBMC_FLAG_POINTER_CHECK ?= --pointer-check
+CBMC_FLAG_POINTER_CHECK ?= #set to --no-pointer-check to disable
 CBMC_FLAG_POINTER_OVERFLOW_CHECK ?= --pointer-overflow-check
-CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= --pointer-primitive-check
-CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= --signed-overflow-check
-CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= --undefined-shift-check
+CBMC_FLAG_POINTER_PRIMITIVE_CHECK ?= # set to --no-pointer-primitive-check to disable
+CBMC_FLAG_SIGNED_OVERFLOW_CHECK ?= # set to --no-signed-overflow-check to disable
+CBMC_FLAG_UNDEFINED_SHIFT_CHECK ?= # set to --no-undefined-shift-check to disable
 CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check
-CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions
+CBMC_FLAG_UNWINDING_ASSERTIONS ?= # set to --no-unwinding-assertions to disable
 CBMC_DEFAULT_UNWIND ?= --unwind 1
 CBMC_FLAG_FLUSH ?= --flush
 
 # CBMC flags used for property checking and coverage checking
 
 CBMCFLAGS += $(CBMC_FLAG_FLUSH)
 
+# CBMC 6.0.0 enables all standard checks by default, which can make coverage analysis
+# very slow. See https://github.com/diffblue/cbmc/issues/8389
+# For now, we disable these checks when generating coverage info.
+COVERFLAGS ?= --no-standard-checks --malloc-may-fail --malloc-fail-null
+
 # CBMC flags used for property checking
 
 CHECKFLAGS += $(CBMC_FLAG_BOUNDS_CHECK)
@@ -301,8 +309,8 @@ CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK)
 NONDET_STATIC ?=
 
 # Flags to pass to goto-cc for compilation and linking
-COMPILE_FLAGS ?= -Wall
-LINK_FLAGS ?= -Wall
+COMPILE_FLAGS ?= -Wall -Werror
+LINK_FLAGS ?= -Wall -Werror
 EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols
 
 # During instrumentation, it adds models of C library functions
@@ -409,7 +417,7 @@ endif
 
 # Optional configuration library flags
 OPT_CONFIG_LIBRARY ?=
-CBMC_OPT_CONFIG_LIBRARY := $(CBMC_FLAG_MALLOC_MAY_FAIL) $(CBMC_FLAG_MALLOC_FAIL_NULL) $(CBMC_STRING_ABSTRACTION)
+CBMC_OPT_CONFIG_LIBRARY := $(CBMC_FLAG_MALLOC_MAY_FAIL) $(CBMC_STRING_ABSTRACTION)
 
 # Proof writers could add function contracts in their source code.
 # These contracts are ignored by default, but may be enabled in two distinct
@@ -458,7 +466,7 @@ endif
 # The default unwind should only be used in DFCC mode without loop contracts.
 # When loop contracts are applied, we only unwind specified loops.
 # If any loops remain after loop contracts have been applied, CBMC might try
-# to unwind the program indefinetly, because we do not pass default unwind
+# to unwind the program indefinitely, because we do not pass default unwind
 # (i.e., --unwind 1) to CBMC when in DFCC mode.
 # We must not use a default unwind command in DFCC mode, because contract instrumentation
 # introduces loops encoding write set inclusion checks that must be dynamically unwound during
@@ -516,9 +524,6 @@ COMMA :=,
 
 CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS)
 
-# --object_bits is removed in goto-cc 6.0.0
-# COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS)
-
 DEFINES += -DCBMC=1
 DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS)
 DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))"
@@ -846,6 +851,23 @@ $(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
 	  --stderr-file $(LOGDIR)/result-err-log.txt \
 	  --description "$(PROOF_UID): checking safety properties"
 
+$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
+	$(LITANI) add-job \
+	  $(POOL) \
+	  --command \
+	    '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
+	  --inputs $^ \
+	  --outputs $@ \
+	  --ci-stage test \
+	  --stdout-file $@ \
+	  $(MEMORY_PROFILING) \
+	  --ignore-returns 10 \
+	  --timeout $(CBMC_TIMEOUT) \
+	  --pipeline-name "$(PROOF_UID)" \
+	  --tags "stats-group:safety checks" \
+	  --stderr-file $(LOGDIR)/result-err-log.txt \
+	  --description "$(PROOF_UID): checking safety properties"
+
 $(LOGDIR)/property.xml: $(HARNESS_GOTO).goto
 	$(LITANI) add-job \
 	  --command \
@@ -911,7 +933,7 @@ litani-path:
 _goto: $(HARNESS_GOTO).goto
 goto:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _goto
 	@ echo Running 'litani build'
@@ -920,7 +942,7 @@ goto:
 _result: $(LOGDIR)/result.txt
 result:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _result
 	@ echo Running 'litani build'
@@ -929,7 +951,7 @@ result:
 _property: $(LOGDIR)/property.xml
 property:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _property
 	@ echo Running 'litani build'
@@ -938,7 +960,7 @@ property:
 _coverage: $(LOGDIR)/coverage.xml
 coverage:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _coverage
 	@ echo Running 'litani build'
@@ -947,7 +969,7 @@ coverage:
 _report: $(PROOFDIR)/report
 report:
 	@ echo Running 'litani init'
-	$(LITANI) init --project $(PROJECT_NAME)
+	$(LITANI) init $(INIT_POOLS) --project $(PROJECT_NAME)
 	@ echo Running 'litani add-job'
 	$(MAKE) -B _report
 	@ echo Running 'litani build'

diff --git a/flake.nix b/flake.nix
@@ -18,7 +18,7 @@
       systems = [ "x86_64-linux" "aarch64-linux" "aarch64-darwin" "x86_64-darwin" ];
       perSystem = { pkgs, ... }:
         let
-          cbmcpkg = pkgs.callPackage ./cbmc { }; # 6.2.0
+          cbmcpkg = pkgs.callPackage ./cbmc { }; # 6.3.1
 
           linters = builtins.attrValues {
             astyle = pkgs.astyle.overrideAttrs (old: rec {