Skip to content
Draft
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .github/workflows/ci.yml
Original file line number Diff line number Diff line change
@@ -179,6 +179,8 @@ jobs:
steps:
- name: Set up CBMC runner
uses: FreeRTOS/CI-CD-Github-Actions/set_up_cbmc_runner@main
with:
cbmc_version: "6.1.1"
- run: |
git submodule update --init --checkout --recursive --depth 1
- name: Run CBMC
396 changes: 212 additions & 184 deletions test/cbmc/proofs/Makefile.common
Original file line number Diff line number Diff line change
@@ -4,7 +4,7 @@
# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
# SPDX-License-Identifier: MIT-0

CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.5
CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.11

################################################################
# The CBMC Starter Kit depends on the files Makefile.common and
@@ -211,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
@@ -229,40 +232,45 @@ 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_UNWIND ?= --unwind 1
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_UNWIND) $(CBMC_UNWINDSET) $(CBMC_FLAG_FLUSH)
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_MALLOC_MAY_FAIL)
CHECKFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
CHECKFLAGS += $(CBMC_FLAG_BOUNDS_CHECK)
CHECKFLAGS += $(CBMC_FLAG_CONVERSION_CHECK)
CHECKFLAGS += $(CBMC_FLAG_DIV_BY_ZERO_CHECK)
@@ -274,12 +282,6 @@ CHECKFLAGS += $(CBMC_FLAG_POINTER_PRIMITIVE_CHECK)
CHECKFLAGS += $(CBMC_FLAG_SIGNED_OVERFLOW_CHECK)
CHECKFLAGS += $(CBMC_FLAG_UNDEFINED_SHIFT_CHECK)
CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK)
CHECKFLAGS += $(CBMC_FLAG_UNWINDING_ASSERTIONS)

# CBMC flags used for coverage checking

COVERFLAGS += $(CBMC_FLAG_MALLOC_MAY_FAIL)
COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)

# Additional CBMC flag to CBMC control verbosity.
#
@@ -307,10 +309,13 @@ COVERFLAGS += $(CBMC_FLAG_MALLOC_FAIL_NULL)
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
ADD_LIBRARY_FLAG := --add-library

# Preprocessor include paths -I...
INCLUDES ?=

@@ -349,9 +354,9 @@ UNWINDSET ?=
# contracts). To satisfy this requirement, it may be necessary to
# unwind some loops before the function contract and loop invariant
# transformations are applied to the goto program. This variable
# EARLY_UNWINDSET is identical to UNWINDSET, and we assume that the
# loops mentioned in EARLY_UNWINDSET and UNWINDSET are disjoint.
EARLY_UNWINDSET ?=
# CPROVER_LIBRARY_UNWINDSET is identical to UNWINDSET, and we assume that the
# loops mentioned in CPROVER_LIBRARY_UNWINDSET and UNWINDSET are disjoint.
CPROVER_LIBRARY_UNWINDSET ?=

# CBMC function removal (Normally set set in the proof Makefile)
#
@@ -396,30 +401,81 @@ PROOF_SOURCES ?=
# report, making the proof run appear to "hang".
CBMC_TIMEOUT ?= 21600

# CBMC string abstraction
#
# Replace all uses of char * by a struct that carries that string,
# and also the underlying allocation and the C string length.
STRING_ABSTRACTION ?=
ifdef STRING_ABSTRACTION
ifneq ($(strip $(STRING_ABSTRACTION)),)
CBMC_STRING_ABSTRACTION := --string-abstraction
endif
endif

# Optional configuration library flags
OPT_CONFIG_LIBRARY ?=
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
# contexts using the following two variables:
# 1. To check whether one or more function contracts are sound with respect to
# the function implementation, CHECK_FUNCTION_CONTRACTS should be a list of
# function names.
# function names. Use CHECK_FUNCTION_CONTRACTS_REC to check contracts on
# recursive functions.
# 2. To replace calls to certain functions with their correspondent function
# contracts, USE_FUNCTION_CONTRACTS should be a list of function names.
# One must check separately whether a function contract is sound before
# replacing it in calling contexts.
CHECK_FUNCTION_CONTRACTS ?=
CBMC_CHECK_FUNCTION_CONTRACTS := $(patsubst %,--enforce-contract %, $(CHECK_FUNCTION_CONTRACTS))

CHECK_FUNCTION_CONTRACTS_REC ?=
CBMC_CHECK_FUNCTION_CONTRACTS_REC := $(patsubst %,--enforce-contract-rec %, $(CHECK_FUNCTION_CONTRACTS_REC))

USE_FUNCTION_CONTRACTS ?=
CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS))

CODE_CONTRACTS := $(CHECK_FUNCTION_CONTRACTS)$(USE_FUNCTION_CONTRACTS)$(APPLY_LOOP_CONTRACTS)

# Proof writers may also apply function contracts using the Dynamic Frame
# Condition Checking (DFCC) mode. For more information on DFCC,
# please see https://diffblue.github.io/cbmc/contracts-dev-spec-dfcc.html.
USE_DYNAMIC_FRAMES ?=
ifdef USE_DYNAMIC_FRAMES
ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
CBMC_USE_DYNAMIC_FRAMES := $(CBMC_OPT_CONFIG_LIBRARY) --dfcc $(HARNESS_ENTRY) $(CBMC_CHECK_FUNCTION_CONTRACTS_REC)
endif
endif

# Similarly, proof writers could also add loop contracts in their source code
# to obtain unbounded correctness proofs. Unlike function contracts, loop
# contracts are not reusable and thus are checked and used simultaneously.
# These contracts are also ignored by default, but may be enabled by setting
# the APPLY_LOOP_CONTRACTS variable to 1.
APPLY_LOOP_CONTRACTS ?= 0
ifeq ($(APPLY_LOOP_CONTRACTS),1)
CBMC_APPLY_LOOP_CONTRACTS ?= --apply-loop-contracts
# the APPLY_LOOP_CONTRACTS variable.
APPLY_LOOP_CONTRACTS ?=
ifdef APPLY_LOOP_CONTRACTS
ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),)
CBMC_APPLY_LOOP_CONTRACTS := --apply-loop-contracts
endif
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 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
# symex.
ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
ifneq ($(strip $(APPLY_LOOP_CONTRACTS)),)
UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
UNWIND_0500_DESC="$(PROOF_UID): unwinding specified subset of loops"
else
UNWIND_0500_FLAGS=$(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_FLAG_UNWINDING_ASSERTIONS)
UNWIND_0500_DESC="$(PROOF_UID): unwinding all loops"
endif
endif

# Silence makefile output (eg, long litani commands) unless VERBOSE is set.
@@ -442,7 +498,6 @@ GOTO_CC ?= goto-cc
GOTO_INSTRUMENT ?= goto-instrument
CRANGLER ?= crangler
VIEWER ?= cbmc-viewer
MAKE_SOURCE ?= make-source
VIEWER2 ?= cbmc-viewer
CMAKE ?= cmake

@@ -465,26 +520,34 @@ 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)
DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))"

# CI currently assumes cbmc invocation has at most one --unwindset

# UNWINDSET is designed for user code (i.e., proof and project code)
ifdef UNWINDSET
ifneq ($(strip $(UNWINDSET)),"")
ifneq ($(strip $(UNWINDSET)),)
CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET)))
endif
endif
ifdef EARLY_UNWINDSET
ifneq ($(strip $(EARLY_UNWINDSET)),"")
CBMC_EARLY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(EARLY_UNWINDSET)))

# CPROVER_LIBRARY_UNWINDSET is designed for CPROVER library functions
ifdef CPROVER_LIBRARY_UNWINDSET
ifneq ($(strip $(CPROVER_LIBRARY_UNWINDSET)),)
CBMC_CPROVER_LIBRARY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(CPROVER_LIBRARY_UNWINDSET)))
endif
endif

CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY))
CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER))

ifdef RESTRICT_FUNCTION_POINTER
ifneq ($(strip $(RESTRICT_FUNCTION_POINTER)),)
CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER))
endif
endif

################################################################
# Targets for rewriting source files with crangler
@@ -568,7 +631,7 @@ $(REWRITTEN_SOURCES):
# Build targets that make the relevant .goto files

# Compile project sources
$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
$(PROJECT_GOTO)0100.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
$(LITANI) add-job \
--command \
'$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
@@ -580,7 +643,7 @@ $(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES)
--description "$(PROOF_UID): building project binary"

# Compile proof sources
$(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
$(PROOF_GOTO)0100.goto: $(PROOF_SOURCES)
$(LITANI) add-job \
--command \
'$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \
@@ -592,7 +655,7 @@ $(PROOF_GOTO)1.goto: $(PROOF_SOURCES)
--description "$(PROOF_UID): building proof binary"

# Remove function bodies from project sources
$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
$(PROJECT_GOTO)0200.goto: $(PROJECT_GOTO)0100.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \
@@ -604,7 +667,7 @@ $(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto
--description "$(PROOF_UID): removing function bodies from project sources"

# Link project and proof sources into the proof harness
$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
$(HARNESS_GOTO)0100.goto: $(PROOF_GOTO)0100.goto $(PROJECT_GOTO)0200.goto
$(LITANI) add-job \
--command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ $(LINK_FLAGS) -o $@' \
--inputs $^ \
@@ -615,10 +678,10 @@ $(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto
--description "$(PROOF_UID): linking project to proof"

# Restrict function pointers
$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
$(HARNESS_GOTO)0200.goto: $(HARNESS_GOTO)0100.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) $^ $@' \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) --remove-function-pointers $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/restrict_function_pointer-log.txt \
@@ -627,7 +690,17 @@ $(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto
--description "$(PROOF_UID): restricting function pointers in project sources"

# Fill static variable with unconstrained values
$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
$(HARNESS_GOTO)0300.goto: $(HARNESS_GOTO)0200.goto
ifneq ($(strip $(CODE_CONTRACTS)),)
$(LITANI) add-job \
--command 'cp $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/nondet_static-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): not setting static variables to nondet (will do during contract instrumentation)"
else
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \
@@ -637,83 +710,102 @@ $(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): setting static variables to nondet"
endif

# Omit unused functions (sharpens coverage calculations)
$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto
# Link CPROVER library if DFCC mode is on
$(HARNESS_GOTO)0400.goto: $(HARNESS_GOTO)0300.goto
ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(ADD_LIBRARY_FLAG) $(CBMC_OPT_CONFIG_LIBRARY) $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
--stdout-file $(LOGDIR)/linking-library-models-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): dropping unused functions"
--description "$(PROOF_UID): linking CPROVER library"
else
$(LITANI) add-job \
--command 'cp $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/linking-library-models-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): not linking CPROVER library"
endif

# Omit initialization of unused global variables (reduces problem size)
$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto
# Early unwind all loops on DFCC mode; otherwise, only unwind loops in proof and project code
$(HARNESS_GOTO)0500.goto: $(HARNESS_GOTO)0400.goto
ifneq ($(strip $(USE_DYNAMIC_FRAMES)),)
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(UNWIND_0500_FLAGS) $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/slice_global_inits-log.txt \
--stdout-file $(LOGDIR)/unwind_loops-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): slicing global initializations"

# Replace function calls with function contracts
# This must be done before enforcing function contracts,
# since contract enforcement inlines all function calls.
$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto
--description $(UNWIND_0500_DESC)
else ifneq ($(strip $(CODE_CONTRACTS)),)
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/use_function_contracts-log.txt \
--stdout-file $(LOGDIR)/unwind_loops-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): replacing function calls with function contracts"
--description "$(PROOF_UID): unwinding loops in proof and project code"
else
$(LITANI) add-job \
--command 'cp $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/unwind_loops-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): not unwinding loops"
endif

# Unwind loops for loop and function contracts
$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto
# Replace function contracts, check function contracts, instrument for loop contracts
$(HARNESS_GOTO)0600.goto: $(HARNESS_GOTO)0500.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_EARLY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \
'$(GOTO_INSTRUMENT) $(CBMC_USE_DYNAMIC_FRAMES) $(NONDET_STATIC) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $(CBMC_USE_FUNCTION_CONTRACTS) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/unwind_loops-log.txt \
--stdout-file $(LOGDIR)/check_function_contracts-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): unwinding loops"
--description "$(PROOF_UID): checking function contracts"

# Apply loop contracts
$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto
# Omit initialization of unused global variables (reduces problem size)
$(HARNESS_GOTO)0700.goto: $(HARNESS_GOTO)0600.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \
--stdout-file $(LOGDIR)/slice_global_inits-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): applying loop contracts"
--description "$(PROOF_UID): slicing global initializations"

# Check function contracts
$(HARNESS_GOTO)9.goto: $(HARNESS_GOTO)8.goto
# Omit unused functions (sharpens coverage calculations)
$(HARNESS_GOTO)0800.goto: $(HARNESS_GOTO)0700.goto
$(LITANI) add-job \
--command \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $^ $@' \
'$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \
--inputs $^ \
--outputs $@ \
--stdout-file $(LOGDIR)/check_function_contracts-log.txt \
--stdout-file $(LOGDIR)/drop_unused_functions-log.txt \
--pipeline-name "$(PROOF_UID)" \
--ci-stage build \
--description "$(PROOF_UID): checking function contracts"
--description "$(PROOF_UID): dropping unused functions"

# Final name for proof harness
$(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.goto
$(HARNESS_GOTO).goto: $(HARNESS_GOTO)0800.goto
$(LITANI) add-job \
--command 'cp $< $@' \
--inputs $^ \
@@ -725,11 +817,19 @@ $(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.goto
################################################################
# Targets to run the analysis commands

$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
ifdef CBMCFLAGS
ifeq ($(strip $(CODE_CONTRACTS)),)
CBMCFLAGS += $(CBMC_UNWINDSET) $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_DEFAULT_UNWIND) $(CBMC_OPT_CONFIG_LIBRARY)
else ifeq ($(strip $(USE_DYNAMIC_FRAMES)),)
CBMCFLAGS += $(CBMC_CPROVER_LIBRARY_UNWINDSET) $(CBMC_OPT_CONFIG_LIBRARY)
endif
endif

$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
$(LITANI) add-job \
$(POOL) \
--command \
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \
--inputs $^ \
--outputs $@ \
--ci-stage test \
@@ -742,11 +842,11 @@ $(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
--stderr-file $(LOGDIR)/result-err-log.txt \
--description "$(PROOF_UID): checking safety properties"

$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto
$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto
$(LITANI) add-job \
$(POOL) \
--command \
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace --xml-ui $<' \
'$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \
--inputs $^ \
--outputs $@ \
--ci-stage test \
@@ -789,54 +889,19 @@ $(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto
--stderr-file $(LOGDIR)/coverage-err-log.txt \
--description "$(PROOF_UID): calculating coverage"

define VIEWER_CMD
$(VIEWER) \
--result $(LOGDIR)/result.txt \
--block $(LOGDIR)/coverage.xml \
--property $(LOGDIR)/property.xml \
--srcdir $(SRCDIR) \
--goto $(HARNESS_GOTO).goto \
--htmldir $(PROOFDIR)/html
endef
export VIEWER_CMD

$(PROOFDIR)/html: $(LOGDIR)/result.txt $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
$(LITANI) add-job \
--command "$$VIEWER_CMD" \
--inputs $^ \
--outputs $(PROOFDIR)/html \
--pipeline-name "$(PROOF_UID)" \
--ci-stage report \
--stdout-file $(LOGDIR)/viewer-log.txt \
--description "$(PROOF_UID): generating report"

COVERAGE ?= $(LOGDIR)/coverage.xml
VIEWER_COVERAGE_FLAG ?= --coverage $(COVERAGE)

# Caution: run make-source before running property and coverage checking
# The current make-source script removes the goto binary
$(LOGDIR)/source.json:
mkdir -p $(dir $@)
$(RM) -r $(GOTODIR)
$(MAKE_SOURCE) --srcdir $(SRCDIR) --wkdir $(PROOFDIR) > $@
$(RM) -r $(GOTODIR)

define VIEWER2_CMD
$(VIEWER2) \
--result $(LOGDIR)/result.xml \
--coverage $(LOGDIR)/coverage.xml \
--property $(LOGDIR)/property.xml \
--srcdir $(SRCDIR) \
--goto $(HARNESS_GOTO).goto \
--reportdir $(PROOFDIR)/report \
--config $(PROOFDIR)/cbmc-viewer.json
endef
export VIEWER2_CMD

# Omit logs/source.json from report generation until make-sources
# works correctly with Makefiles that invoke the compiler with
# mutliple source files at once.
$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml
$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(COVERAGE)
$(LITANI) add-job \
--command "$$VIEWER2_CMD" \
--command " $(VIEWER) \
--result $(LOGDIR)/result.xml \
$(VIEWER_COVERAGE_FLAG) \
--property $(LOGDIR)/property.xml \
--srcdir $(SRCDIR) \
--goto $(HARNESS_GOTO).goto \
--reportdir $(PROOFDIR)/report \
--config $(PROOFDIR)/cbmc-viewer.json" \
--inputs $^ \
--outputs $(PROOFDIR)/report \
--pipeline-name "$(PROOF_UID)" \
@@ -859,7 +924,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'
@@ -868,7 +933,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'
@@ -877,7 +942,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'
@@ -886,30 +951,26 @@ 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'
$(LITANI) run-build

# Choose the invocation of cbmc-viewer depending on which version of
# cbmc-viewer is installed. The --version flag is not implemented in
# version 1 --- it is an "unrecognized argument" --- but it is
# implemented in version 2.
_report1: $(PROOFDIR)/html
_report2: $(PROOFDIR)/report
_report:
(cbmc-viewer --version 2>&1 | grep "unrecognized argument" > /dev/null) && \
$(MAKE) -B _report1 || $(MAKE) -B _report2

report report1 report2:
_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'
$(LITANI) run-build

_report_no_coverage:
$(MAKE) COVERAGE="" VIEWER_COVERAGE_FLAG="" _report
report-no-coverage:
$(MAKE) COVERAGE="" VIEWER_COVERAGE_FLAG=" " report

################################################################
# Targets to clean up after ourselves
clean:
@@ -919,23 +980,22 @@ clean:
-$(RM) $(REWRITTEN_SOURCES) $(foreach rs,$(REWRITTEN_SOURCES),$(rs).json)

veryclean: clean
-$(RM) -r html report
-$(RM) -r report
-$(RM) -r $(LOGDIR) $(GOTODIR)

.PHONY: \
_coverage \
_goto \
_property \
_report \
_report2 \
_result \
_report_no_coverage \
clean \
coverage \
goto \
litani-path \
property \
report \
report2 \
report-no-coverage \
result \
setup_dependencies \
testdeps \
@@ -944,38 +1004,6 @@ veryclean: clean

################################################################

# Rule for generating cbmc-batch.yaml, used by the CI at
# https://github.com/awslabs/aws-batch-cbmc/

JOB_OS ?= ubuntu16
JOB_MEMORY ?= 32000

# Proofs that are expected to fail should set EXPECTED to
# "FAILED" in their Makefile. Values other than SUCCESSFUL
# or FAILED will cause a CI error.
EXPECTED ?= SUCCESSFUL

define yaml_encode_options
"$(shell echo $(1) | sed 's/ ,/ /g' | sed 's/ /;/g')"
endef

CI_FLAGS = $(CBMCFLAGS) $(CHECKFLAGS) $(COVERFLAGS)

cbmc-batch.yaml:
@$(RM) $@
@echo 'build_memory: $(JOB_MEMORY)' > $@
@echo 'cbmcflags: $(strip $(call yaml_encode_options,$(CI_FLAGS)))' >> $@
@echo 'coverage_memory: $(JOB_MEMORY)' >> $@
@echo 'expected: $(EXPECTED)' >> $@
@echo 'goto: $(HARNESS_GOTO).goto' >> $@
@echo 'jobos: $(JOB_OS)' >> $@
@echo 'property_memory: $(JOB_MEMORY)' >> $@
@echo 'report_memory: $(JOB_MEMORY)' >> $@

.PHONY: cbmc-batch.yaml

################################################################

# Run "make echo-proof-uid" to print the proof ID of a proof. This can be
# used by scripts to ensure that every proof has an ID, that there are
# no duplicates, etc.
6 changes: 4 additions & 2 deletions test/cbmc/proofs/stringBuilder/Makefile
Original file line number Diff line number Diff line change
@@ -10,9 +10,11 @@ DEFINES +=
INCLUDES +=

REMOVE_FUNCTION_BODY +=
UNWINDSET +=
UNWINDSET += stringBuilder_harness.0:10
UNWINDSET += stringBuilder_harness.1:10
UNWINDSET += stringBuilder.0:10

CBMC_FLAG_UNWINDING_ASSERTIONS =
CBMC_FLAG_UNWINDING_ASSERTIONS = --no-unwinding-assertions

PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c
PROJECT_SOURCES += $(SRCDIR)/source/ota_mqtt.c