From 0bbf4088859569bec64a24b577057cd8929f8e7a Mon Sep 17 00:00:00 2001 From: bujain Date: Wed, 4 Aug 2021 23:32:12 +0000 Subject: [PATCH 01/29] Add CBMC-proofs infrastructure --- .gitmodules | 6 + test/cbmc/aws-templates-for-cbmc-proofs | 1 + test/cbmc/litani | 1 + test/cbmc/proofs/Makefile-project-defines | 37 + test/cbmc/proofs/Makefile-project-targets | 10 + test/cbmc/proofs/Makefile-project-testing | 11 + test/cbmc/proofs/Makefile.common | 862 ++++++++++++++++++++++ test/cbmc/proofs/README.md | 27 + test/cbmc/proofs/prepare.py | 54 ++ test/cbmc/proofs/run-cbmc-proofs.py | 365 +++++++++ 10 files changed, 1374 insertions(+) create mode 160000 test/cbmc/aws-templates-for-cbmc-proofs create mode 160000 test/cbmc/litani create mode 100644 test/cbmc/proofs/Makefile-project-defines create mode 100644 test/cbmc/proofs/Makefile-project-targets create mode 100644 test/cbmc/proofs/Makefile-project-testing create mode 100644 test/cbmc/proofs/Makefile.common create mode 100644 test/cbmc/proofs/README.md create mode 100644 test/cbmc/proofs/prepare.py create mode 100755 test/cbmc/proofs/run-cbmc-proofs.py diff --git a/.gitmodules b/.gitmodules index 3bd7e7735..bfe815c15 100644 --- a/.gitmodules +++ b/.gitmodules @@ -8,3 +8,9 @@ path = test/unit-test/CMock url = https://github.com/ThrowTheSwitch/CMock.git update = none +[submodule "test/cbmc/aws-templates-for-cbmc-proofs"] + path = test/cbmc/aws-templates-for-cbmc-proofs + url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git +[submodule "test/cbmc/litani"] + path = test/cbmc/litani + url = https://github.com/awslabs/aws-build-accumulator.git diff --git a/test/cbmc/aws-templates-for-cbmc-proofs b/test/cbmc/aws-templates-for-cbmc-proofs new file mode 160000 index 000000000..0bfb2d7b1 --- /dev/null +++ b/test/cbmc/aws-templates-for-cbmc-proofs @@ -0,0 +1 @@ +Subproject commit 0bfb2d7b1aad0fedd39a1d7a5006a3f84d264175 diff --git a/test/cbmc/litani b/test/cbmc/litani new file mode 160000 index 000000000..bba4c8248 --- /dev/null +++ b/test/cbmc/litani @@ -0,0 +1 @@ +Subproject commit bba4c8248e9b62f8e99998268571d3e0acb5a0ee diff --git a/test/cbmc/proofs/Makefile-project-defines b/test/cbmc/proofs/Makefile-project-defines new file mode 100644 index 000000000..f6f7681f7 --- /dev/null +++ b/test/cbmc/proofs/Makefile-project-defines @@ -0,0 +1,37 @@ +# -*- 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: Apache-2.0 + +################################################################ +# Use this file to give project-specific definitions of the command +# line arguments to pass to CBMC tools like goto-cc to build the goto +# binaries and cbmc to do the property and coverage checking. +# +# Use this file to override most default definitions of variables in +# Makefile.common. +################################################################ + +# Flags to pass to goto-cc for compilation (typically those passed to gcc -c) +# COMPILE_FLAGS = + +# Flags to pass to goto-cc for linking (typically those passed to gcc) +# LINK_FLAGS = + +# Preprocessor include paths -I... +# Consider adding +# INCLUDES += -I$(CBMC_ROOT)/include +# You will want to decide what order that comes in relative to the other +# include directories in your project. +# +# INCLUDES = + +# Preprocessor definitions -D... +# DEFINES = + +# Path to arpa executable +# ARPA = + +# Flags to pass to cmake for building the project +# ARPA_CMAKE_FLAGS = diff --git a/test/cbmc/proofs/Makefile-project-targets b/test/cbmc/proofs/Makefile-project-targets new file mode 100644 index 000000000..2d4d4602a --- /dev/null +++ b/test/cbmc/proofs/Makefile-project-targets @@ -0,0 +1,10 @@ +# -*- 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: Apache-2.0 + +################################################################ +# Use this file to give project-specific targets, including targets +# that may depend on targets defined in Makefile.common. +################################################################ diff --git a/test/cbmc/proofs/Makefile-project-testing b/test/cbmc/proofs/Makefile-project-testing new file mode 100644 index 000000000..dc0c20971 --- /dev/null +++ b/test/cbmc/proofs/Makefile-project-testing @@ -0,0 +1,11 @@ +# -*- 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: Apache-2.0 + +################################################################ +# Use this file to define project-specific targets and definitions for +# unit testing or continuous integration that may depend on targets +# defined in Makefile.common +################################################################ diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common new file mode 100644 index 000000000..fb0844b70 --- /dev/null +++ b/test/cbmc/proofs/Makefile.common @@ -0,0 +1,862 @@ +# -*- 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: Apache-2.0 + +################################################################ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Licensed under the Apache License, Version 2.0 (the "License"). You +# may not use this file except in compliance with the License. A copy +# of the License is located at +# +# http://aws.amazon.com/apache2.0/ +# +# or in the "license" file accompanying this file. This file is +# distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF +# ANY KIND, either express or implied. See the License for the +# specific language governing permissions and limitations under the +# License. + +################################################################ +# This file Makefile.common defines the basic work flow for cbmc proofs. +# +# The intention is that the goal of your project is to write proofs +# for a collection of functions in a source tree. +# +# To use this file +# 1. Edit the variable definitions in Section I below as appropriate for +# your project, your proofs, and your source tree. +# 2. For each function for which you are writing a proof, +# a. Create a subdirectory . +# b. Write a proof harness (a function) with the name +# in a file with the name /.c +# c. Write a makefile with the name /Makefile that looks +# something like +# +# HARNESS_FILE= +# HARNESS_ENTRY= +# PROOF_UID= +# +# PROJECT_SOURCES += $(SRCDIR)/libraries/api_1.c +# PROJECT_SOURCES += $(SRCDIR)/libraries/api_2.c +# +# PROOF_SOURCES += $(PROOFDIR)/harness.c +# PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_a.c +# PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_b.c +# +# UNWINDSET += foo.0:3 +# UNWINDSET += bar.1:6 +# +# REMOVE_FUNCTION_BODY += api_stub_a +# REMOVE_FUNCTION_BODY += api_stub_b +# +# DEFINES = -DDEBUG=0 +# +# include ../Makefile.common +# +# d. Change directory to and run make +# +# Dependency handling in this file may not be perfect. Consider +# running "make clean" or "make veryclean" before "make report" if you +# get results that are hard to explain. + +SHELL=/bin/bash + +default: report + +################################################################ +################################################################ +## Section I: This section gives common variable definitions. +## +## Feel free to edit these definitions for your project. +## +## Definitions specific to a proof (generally definitions defined +## below with ?= like PROJECT_SOURCES listing the project source files +## required by the proof) should be defined in the proof Makefile. +## +## Remember that this Makefile is intended to be included from the +## Makefile in your proof directory, so all relative pathnames should +## be relative to your proof directory. +## + +# Absolute path to the directory containing this Makefile.common +# See https://ftp.gnu.org/old-gnu/Manuals/make-3.80/html_node/make_17.html +# +# Note: We compute the absolute paths to the makefiles in MAKEFILE_LIST +# before we filter the list of makefiles for %/Makefile.common. +# Otherwise an invocation of the form "make -f Makefile.common" will set +# MAKEFILE_LIST to "Makefile.common" which will fail to match the +# pattern %/Makefile.common. +# +MAKEFILE_PATHS = $(foreach makefile,$(MAKEFILE_LIST),$(abspath $(makefile))) +PROOF_ROOT = $(dir $(filter %/Makefile.common,$(MAKEFILE_PATHS))) + +CBMC_ROOT = $(shell dirname $(PROOF_ROOT)) +PROOF_STUB = $(CBMC_ROOT)/stubs +PROOF_SOURCE = $(CBMC_ROOT)/sources + +# Project-specific definitions to override default definitions below +# * Makefile-project-defines will never be overwritten +# * Makefile-template-defines will be overwritten each time the +# proof templates are updated +sinclude $(PROOF_ROOT)/Makefile-project-defines +sinclude $(PROOF_ROOT)/Makefile-template-defines + +# SRCDIR is the path to the root of the source tree +SRCDIR ?= $(abspath ../..) + +# PROOFDIR is the path to the directory containing the proof harness +PROOFDIR ?= $(abspath .) + +# Path to the root of the cbmc project. +# +# Projects generally have a directory $(CBMCDIR) with subdirectories +# $(CBMCDIR)/proofs containing the proofs and maybe $(CBMCDIR)/stubs +# containing the stubs used in the proof. This Makefile is generally +# at $(CBMCDIR)/proofs/Makefile.common. +CBMCDIR ?= $(PROOF_ROOT)/cbmc + +# Default CBMC flags used for property checking and coverage checking +CBMCFLAGS += --unwind 1 $(CBMC_UNWINDSET) --flush + +# Do property checking with the external SAT solver given by +# EXTERNAL_SAT_SOLVER. Do coverage checking with the default solver, +# since coverage checking requires the use of an incremental solver. +# The EXTERNAL_SAT_SOLVER variable is typically set (if it is at all) +# as an environment variable or as a makefile variable in +# Makefile-project-defines. +# +# For a particular proof, if the default solver is faster, do property +# checking with the default solver by including this definition in the +# proof Makefile: +# USE_EXTERNAL_SAT_SOLVER = +# +ifneq ($(strip $(EXTERNAL_SAT_SOLVER)),) + USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver $(EXTERNAL_SAT_SOLVER) +endif +CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER) + +# Job pools +# For version of Litani that are new enough (where `litani print-capabilities` +# prints "pools"), proofs for which `EXPENSIVE = true` is set can be added to a +# "job pool" that restricts how many expensive proofs are run at a time. All +# other proofs will be built in parallel as usual. +# +# In more detail: all compilation, instrumentation, and report jobs are run with +# full parallelism as usual, even for expensive proofs. The CBMC jobs for +# non-expensive proofs are also run in parallel. The only difference is that the +# CBMC safety checks and coverage checks for expensive proofs are run with a +# restricted parallelism level. At any one time, only N of these jobs are run at +# once, amongst all the proofs. +# +# To configure N, Litani needs to be initialized with a pool called "expensive". +# For example, to only run two CBMC safety/coverage jobs at a time from amongst +# all the proofs, you would initialize litani like +# litani init --pools expensive:2 +# The run-cbmc-proofs.py script takes care of this initialization through the +# --expensive-jobs-parallelism flag. +# +# To enable this feature, set +# the ENABLE_POOLS variable when running Make, like +# `make ENABLE_POOLS=true report` +# The run-cbmc-proofs.py script takes care of this through the +# --restrict-expensive-jobs flag. + +ifeq ($(strip $(ENABLE_POOLS)),) + POOL = +else ifeq ($(strip $(EXPENSIVE)),) + POOL = +else + POOL = --pool expensive +endif + +# Similar to the pool feature above. If Litani is new enough, enable +# profiling CBMC's memory use. +ifeq ($(strip $(ENABLE_MEMORY_PROFILING)),) + MEMORY_PROFILING = +else + MEMORY_PROFILING = --profile-memory +endif + +# Property checking flags +# +# 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: +# +# CHECK_FLAG_POINTER_CHECK = +# +# would disable the --pointer-check 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_CONVERSION_CHECK ?= --conversion-check +CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check +CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check +CBMC_FLAG_NAN_CHECK ?= --nan-check +CBMC_FLAG_POINTER_CHECK ?= --pointer-check +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_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check +CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions + +# 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) +CHECKFLAGS += $(CBMC_FLAG_FLOAT_OVERFLOW_CHECK) +CHECKFLAGS += $(CBMC_FLAG_NAN_CHECK) +CHECKFLAGS += $(CBMC_FLAG_POINTER_CHECK) +CHECKFLAGS += $(CBMC_FLAG_POINTER_OVERFLOW_CHECK) +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. +# +# Meaningful values are +# 0 none +# 1 only errors +# 2 + warnings +# 4 + results +# 6 + status/phase information +# 8 + statistical information +# 9 + progress information +# 10 + debug info +# +# Uncomment the following line or set in Makefile-project-defines +# CBMC_VERBOSITY ?= --verbosity 4 + +# Additional CBMC flag to control how CBMC treats static variables. +# +# NONDET_STATIC is a list of flags of the form --nondet-static +# and --nondet-static-exclude VAR. The --nondet-static flag causes +# CBMC to initialize static variables with unconstrained value +# (ignoring initializers and default zero-initialization). The +# --nondet-static-exclude VAR excludes VAR for the variables +# initialized with unconstrained values. +NONDET_STATIC ?= "" + +# Flags to pass to goto-cc for compilation and linking +COMPILE_FLAGS ?= +LINK_FLAGS ?= + +# Preprocessor include paths -I... +INCLUDES ?= + +# Preprocessor definitions -D... +DEFINES ?= + +# CBMC object model +# +# CBMC_OBJECT_BITS is the number of bits in a pointer CBMC uses for +# the id of the object to which a pointer is pointing. CBMC uses 8 +# bits for the object id by default. The remaining bits in the pointer +# are used for offset into the object. This limits the size of the +# objects that CBMC can model. This Makefile defines this bound on +# object size to be CBMC_MAX_OBJECT_SIZE. You are likely to get +# unexpected results if you try to malloc an object larger than this +# bound. +CBMC_OBJECT_BITS ?= 8 + +# CBMC loop unwinding (Normally set in the proof Makefile) +# +# UNWINDSET is a list of pairs of the form foo.1:4 meaning that +# CBMC should unwind loop 1 in function foo no more than 4 times. +# For historical reasons, the number 4 is one more than the number +# of times CBMC actually unwinds the loop. +UNWINDSET ?= + +# CBMC function removal (Normally set set in the proof Makefile) +# +# REMOVE_FUNCTION_BODY is a list of function names. CBMC will "undefine" +# the function, and CBMC will treat the function as having no side effects +# and returning an unconstrained value of the appropriate return type. +# The list should include the names of functions being stubbed out. +REMOVE_FUNCTION_BODY ?= + +# The project source files (Normally set set in the proof Makefile) +# +# PROJECT_SOURCES is the list of project source files to compile, +# including the source file defining the function under test. +PROJECT_SOURCES ?= + +# The proof source files (Normally set in the proof Makefile) +# +# PROOF_SOURCES is the list of proof source files to compile, including +# the proof harness, and including any function stubs being used. +PROOF_SOURCES ?= + +# The number of seconds that CBMC should be allowed to run for before +# being forcefully terminated. Currently, this is set to be less than +# the time limit for a CodeBuild job, which is eight hours. If a proof +# run takes longer than the time limit of the CI environment, the +# environment will halt the proof run without updating the Litani +# report, making the proof run appear to "hang". +CBMC_TIMEOUT ?= 21600 + +# 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. +# 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)) + +USE_FUNCTION_CONTRACTS ?= "" +CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS)) + +# 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 + +################################################################ +################################################################ +## Section II: This section is for project-specific definitions + + +################################################################ +################################################################ +## Section II: This section defines the process of running a proof +## +## There should be no reason to edit anything below this line. + +################################################################ +# Paths + +CBMC ?= cbmc +GOTO_ANALYZER ?= goto-analyzer +GOTO_CC ?= goto-cc +GOTO_INSTRUMENT ?= goto-instrument +VIEWER ?= cbmc-viewer +MAKE_SOURCE ?= make-source +VIEWER2 ?= cbmc-viewer +CMAKE ?= cmake +ARPA ?= @echo "You must set ARPA in Makefile-project-defines to run arpa in this project"; false + +GOTODIR ?= $(PROOFDIR)/gotos +LOGDIR ?= $(PROOFDIR)/logs + +PROJECT ?= project +PROOF ?= proof + +HARNESS_GOTO ?= $(GOTODIR)/$(HARNESS_FILE) +PROJECT_GOTO ?= $(GOTODIR)/$(PROJECT) +PROOF_GOTO ?= $(GOTODIR)/$(PROOF) + +ARPA_BLDDIR ?= $(abspath $(PROOFDIR)/arpa_cmake) +ARPA_COMP_CMDS ?= $(ARPA_BLDDIR)/compile_commands.json + +################################################################ +# Useful macros for values that are hard to reference +SPACE :=$() $() +COMMA :=, + +################################################################ +# Set C compiler defines + +CBMCFLAGS += --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 +ifdef UNWINDSET + ifneq ($(strip $(UNWINDSET)),"") + CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET))) + endif +endif +CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY)) + +################################################################ +# Build targets that make the relevant .goto files + +# Compile project sources +$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) + $(LITANI) add-job \ + --command \ + '$(GOTO_CC) $(CBMC_VERBOSITY) --export-file-local-symbols $(COMPILE_FLAGS) $(INCLUDES) $(DEFINES) $^ -o $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/project_sources-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): building project binary" + +# Compile proof sources +$(PROOF_GOTO)1.goto: $(PROOF_SOURCES) + $(LITANI) add-job \ + --command \ + '$(GOTO_CC) $(CBMC_VERBOSITY) --export-file-local-symbols $(COMPILE_FLAGS) $(INCLUDES) $(DEFINES) $^ -o $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/proof_sources-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): building proof binary" + +# Optionally remove function bodies from project sources +$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto +ifeq ($(REMOVE_FUNCTION_BODY),"") + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not removing function bodies from project sources" +else + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/remove_function_body-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): removing function bodies from project sources" +endif + +# Link project and proof sources into the proof harness +$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto + $(LITANI) add-job \ + --command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ -o $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/link_proof_project-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): linking project to proof" + +# Optionally check function contracts +$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto +ifeq ($(CHECK_FUNCTION_CONTRACTS),"") + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not checking function contracts" +else + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/check_function_contracts-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): checking function contracts" +endif + +# Optionally replace function calls with function contracts +$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto +ifeq ($(USE_FUNCTION_CONTRACTS),"") + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not replacing function calls with function contracts" +else + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/use_function_contracts-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): replacing function calls with function contracts" +endif + +# Optionally apply loop contracts +$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto +ifneq ($(APPLY_LOOP_CONTRACTS),1) + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not applying loop contracts" +else + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --apply-loop-contracts $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): applying loop contracts" +endif + +# Optionally fill static variable with unconstrained values +$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto +ifeq ($(NONDET_STATIC),"") + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not setting static variables to nondet" +else + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/nondet_static-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): setting static variables to nondet" +endif + +# Omit unused functions (sharpens coverage calculations) +$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): dropping unused functions" + +# Omit initialization of unused global variables (reduces problem size) +$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/slice_global_inits-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): slicing global initializations" + +# Final name for proof harness +$(HARNESS_GOTO).goto: $(HARNESS_GOTO)7.goto + $(LITANI) add-job \ + --command 'cp $< $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): copying final goto-binary" + +################################################################ +# Targets to run Arpa + +$(ARPA_BLDDIR): + $(CMAKE) $(ARPA_CMAKE_FLAGS) \ + -DCMAKE_EXPORT_COMPILE_COMMANDS=1 \ + -B $(ARPA_BLDDIR) \ + -S $(SRCDIR) + +arpa: $(ARPA_BLDDIR) + $(ARPA) run -cc $(ARPA_COMP_CMDS) -r $(SRCDIR) + +################################################################ +# Targets to run the analysis commands + +$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto + $(LITANI) add-job \ + $(POOL) \ + --command \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(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)/result.xml: $(HARNESS_GOTO).goto + $(LITANI) add-job \ + $(POOL) \ + --command \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CHECKFLAGS) --trace --xml-ui $<' \ + --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 \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CHECKFLAGS) --show-properties --xml-ui $<' \ + --inputs $^ \ + --outputs $@ \ + --ci-stage test \ + --stdout-file $@ \ + --ignore-returns 10 \ + --pipeline-name "$(PROOF_UID)" \ + --stderr-file $(LOGDIR)/property-err-log.txt \ + --description "$(PROOF_UID): printing safety properties" + +$(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto + $(LITANI) add-job \ + $(POOL) \ + --command \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(COVERFLAGS) --cover location --xml-ui $<' \ + --inputs $^ \ + --outputs $@ \ + --ci-stage test \ + --stdout-file $@ \ + $(MEMORY_PROFILING) \ + --ignore-returns 10 \ + --timeout $(CBMC_TIMEOUT) \ + --pipeline-name "$(PROOF_UID)" \ + --tags "stats-group:coverage computation" \ + --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 \ + --interleave-stdout-stderr \ + --description "$(PROOF_UID): generating report" + + +# 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 +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 + $(LITANI) add-job \ + --command "$$VIEWER2_CMD" \ + --inputs $^ \ + --outputs $(PROOFDIR)/report \ + --pipeline-name "$(PROOF_UID)" \ + --stdout-file $(LOGDIR)/viewer-log.txt \ + --interleave-stdout-stderr \ + --ci-stage report \ + --description "$(PROOF_UID): generating report" + +litani-path: + @echo $(LITANI) + +# ############################################################## +# Phony Rules +# +# These rules provide a convenient way to run a single proof up to a +# certain stage. Users can browse into a proof directory and run +# "make -Bj 3 report" to generate a report for just that proof, or +# "make goto" to build the goto binary. Under the hood, this runs litani +# for just that proof. + +_goto: $(HARNESS_GOTO).goto +goto: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _goto + $(LITANI) run-build + +_result: $(LOGDIR)/result.txt +result: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _result + $(LITANI) run-build + +_property: $(LOGDIR)/property.xml +property: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _property + $(LITANI) run-build + +_coverage: $(LOGDIR)/coverage.xml +coverage: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _coverage + $(LITANI) run-build + +_report: $(PROOFDIR)/html +report: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _report + $(LITANI) run-build + +_report2: $(PROOFDIR)/report +report2: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _report2 + $(LITANI) run-build + + +################################################################ +# Targets to clean up after ourselves +clean: + -$(RM) $(DEPENDENT_GOTOS) + -$(RM) TAGS* + -$(RM) *~ \#* + -$(RM) Makefile.arpa + -$(RM) -r $(ARPA_BLDDIR) + +veryclean: clean + -$(RM) -r html report + -$(RM) -r $(LOGDIR) $(GOTODIR) + +.PHONY: \ + _coverage \ + _goto \ + _property \ + _report \ + _report2 \ + _result \ + arpa \ + clean \ + coverage \ + goto \ + litani-path \ + property \ + report \ + report2 \ + result \ + setup_dependencies \ + testdeps \ + veryclean \ + # + +################################################################ + +# 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. + +.PHONY: echo-proof-uid +echo-proof-uid: + @echo $(PROOF_UID) + +.PHONY: echo-project-name +echo-project-name: + @echo $(PROJECT_NAME) + +################################################################ + +# Project-specific targets requiring values defined above +sinclude $(PROOF_ROOT)/Makefile-project-targets + +# CI-specific targets to drive cbmc in CI +sinclude $(PROOF_ROOT)/Makefile-project-testing + +################################################################ diff --git a/test/cbmc/proofs/README.md b/test/cbmc/proofs/README.md new file mode 100644 index 000000000..5e22aa01a --- /dev/null +++ b/test/cbmc/proofs/README.md @@ -0,0 +1,27 @@ +CBMC proofs +=========== + +This directory contains the CBMC proofs. Each proof is in its own +directory. + +This directory includes four Makefiles. + +One Makefile describes the basic workflow for building and running proofs: + +* Makefile.common: + * make: builds the goto binary, does the cbmc property checking + and coverage checking, and builds the final report. + * make goto: builds the goto binary + * make result: does cbmc property checking + * make coverage: does cbmc coverage checking + * make report: builds the final report + +Three included Makefiles describe project-specific settings and can override +definitions in Makefile.common: + +* Makefile-project-defines: definitions like compiler flags + required to build the goto binaries, and definitions to override + definitions in Makefile.common. +* Makefile-project-targets: other make targets needed for the project +* Makefile-project-testing: other definitions and targets needed for + unit testing or continuous integration. diff --git a/test/cbmc/proofs/prepare.py b/test/cbmc/proofs/prepare.py new file mode 100644 index 000000000..d58805cad --- /dev/null +++ b/test/cbmc/proofs/prepare.py @@ -0,0 +1,54 @@ +#!/usr/bin/env python3 + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + + +"""Prepare the source tree for proofs in continuous integration.""" + + +import os +import subprocess + + +MAKEFILE = "Makefile" +CBMC_BATCH_YAML = "cbmc-batch.yaml" + + +def create_cbmc_batch_yaml(folder): + """Run make to create cbmc-batch.yaml in folder.""" + + try: + subprocess.run( + ["make", "-B", CBMC_BATCH_YAML], + cwd=folder, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + universal_newlines=True, + check=True + ) + except subprocess.CalledProcessError as error: + raise UserWarning("Failed to create {} in {}: " + "command was '{}': " + "error was '{}'" + .format(CBMC_BATCH_YAML, folder, + ' '.join(error.cmd), + error.stderr.strip())) from None + + +def create_cbmc_batch_yaml_files(root='.'): + """Create cbmc-batch.yaml in all directories under root.""" + + for folder, _, files in os.walk(root): + if CBMC_BATCH_YAML in files and MAKEFILE in files: + create_cbmc_batch_yaml(folder) + + +def prepare(): + """Prepare the source tree for proofs in continuous integration.""" + + create_cbmc_batch_yaml_files() + + +if __name__ == "__main__": + prepare() diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py new file mode 100755 index 000000000..33d0f778f --- /dev/null +++ b/test/cbmc/proofs/run-cbmc-proofs.py @@ -0,0 +1,365 @@ +#!/usr/bin/env python3 +# +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + + +import argparse +import asyncio +import json +import logging +import math +import os +import pathlib +import re +import subprocess +import sys + + +DESCRIPTION = "Configure and run all CBMC proofs in parallel" + +# Keep the epilog hard-wrapped at 70 characters, as it gets printed +# verbatim in the terminal. 70 characters stops here --------------> | +EPILOG = """ +This tool automates the process of running `make report` in each of +the CBMC proof directories. The tool calculates the dependency graph +of all tasks needed to build, run, and report on all the proofs, and +executes these tasks in parallel. + +The tool is roughly equivalent to doing this: + + litani init --project "my-cool-project"; + + find . -name cbmc-proof.txt | while read -r proof; do + pushd $(dirname ${proof}); + + # The `make _report` rule adds a single proof to litani + # without running it + make _report; + + popd; + done + + litani run-build; + +except that it is much faster and provides some convenience options. +The CBMC CI runs this script with no arguments to build and run all +proofs in parallel. The value of "my-cool-project" is taken from the +PROJECT_NAME variable in Makefile-project-defines. + +The --no-standalone argument omits the `litani init` and `litani +run-build`; use it when you want to add additional proof jobs, not +just the CBMC ones. In that case, you would run `litani init` +yourself; then run `run-cbmc-proofs --no-standalone`; add any +additional jobs that you want to execute with `litani add-job`; and +finally run `litani run-build`. + +The litani dashboard will be written under the `output` directory; the +cbmc-viewer reports remain in the `$PROOF_DIR/report` directory. The +HTML dashboard from the latest Litani run will always be symlinked to +`output/latest/html/index.html`, so you can keep that page open in +your browser and reload the page whenever you re-run this script. +""" +# 70 characters stops here ----------------------------------------> | + + +def get_project_name(): + cmd = [ + "make", + "-f", "Makefile.common", + "echo-project-name", + ] + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE) + if proc.returncode: + logging.critical("could not run make to determine project name") + sys.exit(1) + if not proc.stdout.strip(): + logging.warning( + "project name has not been set; using generic name instead. " + "Set the PROJECT_NAME value in Makefile-project-defines to " + "remove this warning") + return "" + return proc.stdout.strip() + + +def get_args(): + pars = argparse.ArgumentParser( + description=DESCRIPTION, epilog=EPILOG, + formatter_class=argparse.RawDescriptionHelpFormatter) + for arg in [{ + "flags": ["-j", "--parallel-jobs"], + "type": int, + "metavar": "N", + "help": "run at most N proof jobs in parallel", + }, { + "flags": ["--no-standalone"], + "action": "store_true", + "help": "only configure proofs: do not initialize nor run", + }, { + "flags": ["-p", "--proofs"], + "nargs": "+", + "metavar": "DIR", + "help": "only run proof in directory DIR (can pass more than one)", + }, { + "flags": ["--project-name"], + "metavar": "NAME", + "default": get_project_name(), + "help": "project name for report. Default: %(default)s", + }, { + "flags": ["--proof-marker"], + "metavar": "FILE", + "default": "cbmc-proof.txt", + "help": ( + "name of file that marks proof directories. Default: " + "%(default)s"), + }, { + "flags": ["--no-memory-profile"], + "action": "store_true", + "help": "disable memory profiling, even if Litani supports it" + }, { + "flags": ["--no-expensive-limit"], + "action": "store_true", + "help": "do not limit parallelism of 'EXPENSIVE' jobs", + }, { + "flags": ["--expensive-jobs-parallelism"], + "metavar": "N", + "default": 1, + "type": int, + "help": ( + "how many proof jobs marked 'EXPENSIVE' to run in parallel. " + "Default: %(default)s"), + }, { + "flags": ["--verbose"], + "action": "store_true", + "help": "verbose output", + }]: + flags = arg.pop("flags") + pars.add_argument(*flags, **arg) + return pars.parse_args() + + +def set_up_logging(verbose): + if verbose: + level = logging.DEBUG + else: + level = logging.WARNING + logging.basicConfig( + format="run-cbmc-proofs: %(message)s", level=level) + + +def task_pool_size(): + ret = os.cpu_count() + if ret is None or ret < 3: + return 1 + return ret - 2 + + +def print_counter(counter): + print( + "\rConfiguring CBMC proofs: " + "{complete:{width}} / {total:{width}}".format( + **counter), end="", file=sys.stderr) + + +def get_proof_dirs(proof_root, proof_list, proof_marker): + if proof_list is not None: + proofs_remaining = list(proof_list) + else: + proofs_remaining = [] + + for root, _, fyles in os.walk(proof_root): + proof_name = str(pathlib.Path(root).name) + if proof_list and proof_name not in proof_list: + continue + if proof_list and proof_name in proofs_remaining: + proofs_remaining.remove(proof_name) + if proof_marker in fyles: + yield root + + if proofs_remaining: + logging.critical( + "The following proofs were not found: %s", + ", ".join(proofs_remaining)) + sys.exit(1) + + +def run_build(litani, jobs): + cmd = [str(litani), "run-build"] + if jobs: + cmd.extend(["-j", str(jobs)]) + + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd) + if proc.returncode: + logging.critical("Failed to run litani run-build") + sys.exit(1) + + +def get_litani_path(proof_root): + cmd = [ + "make", + "PROOF_ROOT=%s" % proof_root, + "-f", "Makefile.common", + "litani-path", + ] + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE) + if proc.returncode: + logging.critical("Could not determine path to litani") + sys.exit(1) + return proc.stdout.strip() + + +def get_litani_capabilities(litani_path): + cmd = [litani_path, "print-capabilities"] + proc = subprocess.run( + cmd, text=True, stdout=subprocess.PIPE, stderr=subprocess.DEVNULL) + if proc.returncode: + return [] + try: + return json.loads(proc.stdout) + except RuntimeError: + logging.warning("Could not load litani capabilities: '%s'", proc.stdout) + return [] + + +def check_uid_uniqueness(proof_dir, proof_uids): + with (pathlib.Path(proof_dir) / "Makefile").open() as handle: + for line in handle: + m = re.match(r"^PROOF_UID\s*=\s*(?P\w+)", line) + if not m: + continue + if m["uid"] not in proof_uids: + proof_uids[m["uid"]] = proof_dir + return + + logging.critical( + "The Makefile in directory '%s' should have a different " + "PROOF_UID than the Makefile in directory '%s'", + proof_dir, proof_uids[m["uid"]]) + sys.exit(1) + + logging.critical( + "The Makefile in directory '%s' should contain a line like", proof_dir) + logging.critical("PROOF_UID = ...") + logging.critical("with a unique identifier for the proof.") + sys.exit(1) + + +def should_enable_memory_profiling(litani_caps, args): + if args.no_memory_profile: + return False + return "memory_profile" in litani_caps + + +def should_enable_pools(litani_caps, args): + if args.no_expensive_limit: + return False + return "pools" in litani_caps + + +async def configure_proof_dirs( + queue, counter, proof_uids, enable_pools, enable_memory_profiling): + while True: + print_counter(counter) + path = str(await queue.get()) + + check_uid_uniqueness(path, proof_uids) + + pools = ["ENABLE_POOLS=true"] if enable_pools else [] + profiling = [ + "ENABLE_MEMORY_PROFILING=true"] if enable_memory_profiling else [] + + proc = await asyncio.create_subprocess_exec( + # Allow interactive tasks to preempt proof configuration + "nice", "-n", "15", "make", *pools, *profiling, "-B", "--quiet", + "_report", cwd=path) + await proc.wait() + counter["fail" if proc.returncode else "pass"].append(path) + counter["complete"] += 1 + + print_counter(counter) + queue.task_done() + + +async def main(): + args = get_args() + set_up_logging(args.verbose) + + proof_root = pathlib.Path(__file__).resolve().parent + litani = get_litani_path(proof_root) + + litani_caps = get_litani_capabilities(litani) + enable_pools = should_enable_pools(litani_caps, args) + init_pools = [ + "--pools", f"expensive:{args.expensive_jobs_parallelism}" + ] if enable_pools else [] + + if not args.no_standalone: + cmd = [str(litani), "init", *init_pools, "--project", args.project_name] + + if "output_directory_flags" in litani_caps: + out_prefix = proof_root / "output" + out_symlink = out_prefix / "latest" + out_index = out_symlink / "html" / "index.html" + cmd.extend([ + "--output-prefix", str(out_prefix), + "--output-symlink", str(out_symlink), + ]) + print( + "\nFor your convenience, the output of this run will be " + "symbolically linked to %s\n" % str(out_index)) + + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd) + if proc.returncode: + logging.critical("Failed to run litani init") + sys.exit(1) + + proof_dirs = list(get_proof_dirs( + proof_root, args.proofs, args.proof_marker)) + if not proof_dirs: + logging.critical("No proof directories found") + sys.exit(1) + + proof_queue = asyncio.Queue() + for proof_dir in proof_dirs: + proof_queue.put_nowait(proof_dir) + + counter = { + "pass": [], + "fail": [], + "complete": 0, + "total": len(proof_dirs), + "width": int(math.log10(len(proof_dirs))) + 1 + } + + proof_uids = {} + tasks = [] + + enable_memory_profiling = should_enable_memory_profiling(litani_caps, args) + + for _ in range(task_pool_size()): + task = asyncio.create_task(configure_proof_dirs( + proof_queue, counter, proof_uids, enable_pools, + enable_memory_profiling)) + tasks.append(task) + + await proof_queue.join() + + print_counter(counter) + print("", file=sys.stderr) + + if counter["fail"]: + logging.critical( + "Failed to configure the following proofs:\n%s", "\n".join( + [str(f) for f in counter["fail"]])) + sys.exit(1) + + if not args.no_standalone: + run_build(litani, args.parallel_jobs) + + +if __name__ == "__main__": + asyncio.run(main()) From 95529f8832c66188650ea3bb17612f10ec6c2678 Mon Sep 17 00:00:00 2001 From: Bhaumik Jain <86116186+Bujain@users.noreply.github.com> Date: Wed, 4 Aug 2021 19:32:47 -0700 Subject: [PATCH 02/29] Add CBMC-proofs infrastructure (#242) --- .gitmodules | 6 + test/cbmc/aws-templates-for-cbmc-proofs | 1 + test/cbmc/litani | 1 + test/cbmc/proofs/Makefile-project-defines | 37 + test/cbmc/proofs/Makefile-project-targets | 10 + test/cbmc/proofs/Makefile-project-testing | 11 + test/cbmc/proofs/Makefile.common | 862 ++++++++++++++++++++++ test/cbmc/proofs/README.md | 27 + test/cbmc/proofs/prepare.py | 54 ++ test/cbmc/proofs/run-cbmc-proofs.py | 365 +++++++++ 10 files changed, 1374 insertions(+) create mode 160000 test/cbmc/aws-templates-for-cbmc-proofs create mode 160000 test/cbmc/litani create mode 100644 test/cbmc/proofs/Makefile-project-defines create mode 100644 test/cbmc/proofs/Makefile-project-targets create mode 100644 test/cbmc/proofs/Makefile-project-testing create mode 100644 test/cbmc/proofs/Makefile.common create mode 100644 test/cbmc/proofs/README.md create mode 100644 test/cbmc/proofs/prepare.py create mode 100755 test/cbmc/proofs/run-cbmc-proofs.py diff --git a/.gitmodules b/.gitmodules index 3bd7e7735..bfe815c15 100644 --- a/.gitmodules +++ b/.gitmodules @@ -8,3 +8,9 @@ path = test/unit-test/CMock url = https://github.com/ThrowTheSwitch/CMock.git update = none +[submodule "test/cbmc/aws-templates-for-cbmc-proofs"] + path = test/cbmc/aws-templates-for-cbmc-proofs + url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git +[submodule "test/cbmc/litani"] + path = test/cbmc/litani + url = https://github.com/awslabs/aws-build-accumulator.git diff --git a/test/cbmc/aws-templates-for-cbmc-proofs b/test/cbmc/aws-templates-for-cbmc-proofs new file mode 160000 index 000000000..0bfb2d7b1 --- /dev/null +++ b/test/cbmc/aws-templates-for-cbmc-proofs @@ -0,0 +1 @@ +Subproject commit 0bfb2d7b1aad0fedd39a1d7a5006a3f84d264175 diff --git a/test/cbmc/litani b/test/cbmc/litani new file mode 160000 index 000000000..bba4c8248 --- /dev/null +++ b/test/cbmc/litani @@ -0,0 +1 @@ +Subproject commit bba4c8248e9b62f8e99998268571d3e0acb5a0ee diff --git a/test/cbmc/proofs/Makefile-project-defines b/test/cbmc/proofs/Makefile-project-defines new file mode 100644 index 000000000..f6f7681f7 --- /dev/null +++ b/test/cbmc/proofs/Makefile-project-defines @@ -0,0 +1,37 @@ +# -*- 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: Apache-2.0 + +################################################################ +# Use this file to give project-specific definitions of the command +# line arguments to pass to CBMC tools like goto-cc to build the goto +# binaries and cbmc to do the property and coverage checking. +# +# Use this file to override most default definitions of variables in +# Makefile.common. +################################################################ + +# Flags to pass to goto-cc for compilation (typically those passed to gcc -c) +# COMPILE_FLAGS = + +# Flags to pass to goto-cc for linking (typically those passed to gcc) +# LINK_FLAGS = + +# Preprocessor include paths -I... +# Consider adding +# INCLUDES += -I$(CBMC_ROOT)/include +# You will want to decide what order that comes in relative to the other +# include directories in your project. +# +# INCLUDES = + +# Preprocessor definitions -D... +# DEFINES = + +# Path to arpa executable +# ARPA = + +# Flags to pass to cmake for building the project +# ARPA_CMAKE_FLAGS = diff --git a/test/cbmc/proofs/Makefile-project-targets b/test/cbmc/proofs/Makefile-project-targets new file mode 100644 index 000000000..2d4d4602a --- /dev/null +++ b/test/cbmc/proofs/Makefile-project-targets @@ -0,0 +1,10 @@ +# -*- 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: Apache-2.0 + +################################################################ +# Use this file to give project-specific targets, including targets +# that may depend on targets defined in Makefile.common. +################################################################ diff --git a/test/cbmc/proofs/Makefile-project-testing b/test/cbmc/proofs/Makefile-project-testing new file mode 100644 index 000000000..dc0c20971 --- /dev/null +++ b/test/cbmc/proofs/Makefile-project-testing @@ -0,0 +1,11 @@ +# -*- 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: Apache-2.0 + +################################################################ +# Use this file to define project-specific targets and definitions for +# unit testing or continuous integration that may depend on targets +# defined in Makefile.common +################################################################ diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common new file mode 100644 index 000000000..fb0844b70 --- /dev/null +++ b/test/cbmc/proofs/Makefile.common @@ -0,0 +1,862 @@ +# -*- 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: Apache-2.0 + +################################################################ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# +# Licensed under the Apache License, Version 2.0 (the "License"). You +# may not use this file except in compliance with the License. A copy +# of the License is located at +# +# http://aws.amazon.com/apache2.0/ +# +# or in the "license" file accompanying this file. This file is +# distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF +# ANY KIND, either express or implied. See the License for the +# specific language governing permissions and limitations under the +# License. + +################################################################ +# This file Makefile.common defines the basic work flow for cbmc proofs. +# +# The intention is that the goal of your project is to write proofs +# for a collection of functions in a source tree. +# +# To use this file +# 1. Edit the variable definitions in Section I below as appropriate for +# your project, your proofs, and your source tree. +# 2. For each function for which you are writing a proof, +# a. Create a subdirectory . +# b. Write a proof harness (a function) with the name +# in a file with the name /.c +# c. Write a makefile with the name /Makefile that looks +# something like +# +# HARNESS_FILE= +# HARNESS_ENTRY= +# PROOF_UID= +# +# PROJECT_SOURCES += $(SRCDIR)/libraries/api_1.c +# PROJECT_SOURCES += $(SRCDIR)/libraries/api_2.c +# +# PROOF_SOURCES += $(PROOFDIR)/harness.c +# PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_a.c +# PROOF_SOURCES += $(SRCDIR)/cbmc/proofs/stub_b.c +# +# UNWINDSET += foo.0:3 +# UNWINDSET += bar.1:6 +# +# REMOVE_FUNCTION_BODY += api_stub_a +# REMOVE_FUNCTION_BODY += api_stub_b +# +# DEFINES = -DDEBUG=0 +# +# include ../Makefile.common +# +# d. Change directory to and run make +# +# Dependency handling in this file may not be perfect. Consider +# running "make clean" or "make veryclean" before "make report" if you +# get results that are hard to explain. + +SHELL=/bin/bash + +default: report + +################################################################ +################################################################ +## Section I: This section gives common variable definitions. +## +## Feel free to edit these definitions for your project. +## +## Definitions specific to a proof (generally definitions defined +## below with ?= like PROJECT_SOURCES listing the project source files +## required by the proof) should be defined in the proof Makefile. +## +## Remember that this Makefile is intended to be included from the +## Makefile in your proof directory, so all relative pathnames should +## be relative to your proof directory. +## + +# Absolute path to the directory containing this Makefile.common +# See https://ftp.gnu.org/old-gnu/Manuals/make-3.80/html_node/make_17.html +# +# Note: We compute the absolute paths to the makefiles in MAKEFILE_LIST +# before we filter the list of makefiles for %/Makefile.common. +# Otherwise an invocation of the form "make -f Makefile.common" will set +# MAKEFILE_LIST to "Makefile.common" which will fail to match the +# pattern %/Makefile.common. +# +MAKEFILE_PATHS = $(foreach makefile,$(MAKEFILE_LIST),$(abspath $(makefile))) +PROOF_ROOT = $(dir $(filter %/Makefile.common,$(MAKEFILE_PATHS))) + +CBMC_ROOT = $(shell dirname $(PROOF_ROOT)) +PROOF_STUB = $(CBMC_ROOT)/stubs +PROOF_SOURCE = $(CBMC_ROOT)/sources + +# Project-specific definitions to override default definitions below +# * Makefile-project-defines will never be overwritten +# * Makefile-template-defines will be overwritten each time the +# proof templates are updated +sinclude $(PROOF_ROOT)/Makefile-project-defines +sinclude $(PROOF_ROOT)/Makefile-template-defines + +# SRCDIR is the path to the root of the source tree +SRCDIR ?= $(abspath ../..) + +# PROOFDIR is the path to the directory containing the proof harness +PROOFDIR ?= $(abspath .) + +# Path to the root of the cbmc project. +# +# Projects generally have a directory $(CBMCDIR) with subdirectories +# $(CBMCDIR)/proofs containing the proofs and maybe $(CBMCDIR)/stubs +# containing the stubs used in the proof. This Makefile is generally +# at $(CBMCDIR)/proofs/Makefile.common. +CBMCDIR ?= $(PROOF_ROOT)/cbmc + +# Default CBMC flags used for property checking and coverage checking +CBMCFLAGS += --unwind 1 $(CBMC_UNWINDSET) --flush + +# Do property checking with the external SAT solver given by +# EXTERNAL_SAT_SOLVER. Do coverage checking with the default solver, +# since coverage checking requires the use of an incremental solver. +# The EXTERNAL_SAT_SOLVER variable is typically set (if it is at all) +# as an environment variable or as a makefile variable in +# Makefile-project-defines. +# +# For a particular proof, if the default solver is faster, do property +# checking with the default solver by including this definition in the +# proof Makefile: +# USE_EXTERNAL_SAT_SOLVER = +# +ifneq ($(strip $(EXTERNAL_SAT_SOLVER)),) + USE_EXTERNAL_SAT_SOLVER ?= --external-sat-solver $(EXTERNAL_SAT_SOLVER) +endif +CHECKFLAGS += $(USE_EXTERNAL_SAT_SOLVER) + +# Job pools +# For version of Litani that are new enough (where `litani print-capabilities` +# prints "pools"), proofs for which `EXPENSIVE = true` is set can be added to a +# "job pool" that restricts how many expensive proofs are run at a time. All +# other proofs will be built in parallel as usual. +# +# In more detail: all compilation, instrumentation, and report jobs are run with +# full parallelism as usual, even for expensive proofs. The CBMC jobs for +# non-expensive proofs are also run in parallel. The only difference is that the +# CBMC safety checks and coverage checks for expensive proofs are run with a +# restricted parallelism level. At any one time, only N of these jobs are run at +# once, amongst all the proofs. +# +# To configure N, Litani needs to be initialized with a pool called "expensive". +# For example, to only run two CBMC safety/coverage jobs at a time from amongst +# all the proofs, you would initialize litani like +# litani init --pools expensive:2 +# The run-cbmc-proofs.py script takes care of this initialization through the +# --expensive-jobs-parallelism flag. +# +# To enable this feature, set +# the ENABLE_POOLS variable when running Make, like +# `make ENABLE_POOLS=true report` +# The run-cbmc-proofs.py script takes care of this through the +# --restrict-expensive-jobs flag. + +ifeq ($(strip $(ENABLE_POOLS)),) + POOL = +else ifeq ($(strip $(EXPENSIVE)),) + POOL = +else + POOL = --pool expensive +endif + +# Similar to the pool feature above. If Litani is new enough, enable +# profiling CBMC's memory use. +ifeq ($(strip $(ENABLE_MEMORY_PROFILING)),) + MEMORY_PROFILING = +else + MEMORY_PROFILING = --profile-memory +endif + +# Property checking flags +# +# 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: +# +# CHECK_FLAG_POINTER_CHECK = +# +# would disable the --pointer-check 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_CONVERSION_CHECK ?= --conversion-check +CBMC_FLAG_DIV_BY_ZERO_CHECK ?= --div-by-zero-check +CBMC_FLAG_FLOAT_OVERFLOW_CHECK ?= --float-overflow-check +CBMC_FLAG_NAN_CHECK ?= --nan-check +CBMC_FLAG_POINTER_CHECK ?= --pointer-check +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_UNSIGNED_OVERFLOW_CHECK ?= --unsigned-overflow-check +CBMC_FLAG_UNWINDING_ASSERTIONS ?= --unwinding-assertions + +# 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) +CHECKFLAGS += $(CBMC_FLAG_FLOAT_OVERFLOW_CHECK) +CHECKFLAGS += $(CBMC_FLAG_NAN_CHECK) +CHECKFLAGS += $(CBMC_FLAG_POINTER_CHECK) +CHECKFLAGS += $(CBMC_FLAG_POINTER_OVERFLOW_CHECK) +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. +# +# Meaningful values are +# 0 none +# 1 only errors +# 2 + warnings +# 4 + results +# 6 + status/phase information +# 8 + statistical information +# 9 + progress information +# 10 + debug info +# +# Uncomment the following line or set in Makefile-project-defines +# CBMC_VERBOSITY ?= --verbosity 4 + +# Additional CBMC flag to control how CBMC treats static variables. +# +# NONDET_STATIC is a list of flags of the form --nondet-static +# and --nondet-static-exclude VAR. The --nondet-static flag causes +# CBMC to initialize static variables with unconstrained value +# (ignoring initializers and default zero-initialization). The +# --nondet-static-exclude VAR excludes VAR for the variables +# initialized with unconstrained values. +NONDET_STATIC ?= "" + +# Flags to pass to goto-cc for compilation and linking +COMPILE_FLAGS ?= +LINK_FLAGS ?= + +# Preprocessor include paths -I... +INCLUDES ?= + +# Preprocessor definitions -D... +DEFINES ?= + +# CBMC object model +# +# CBMC_OBJECT_BITS is the number of bits in a pointer CBMC uses for +# the id of the object to which a pointer is pointing. CBMC uses 8 +# bits for the object id by default. The remaining bits in the pointer +# are used for offset into the object. This limits the size of the +# objects that CBMC can model. This Makefile defines this bound on +# object size to be CBMC_MAX_OBJECT_SIZE. You are likely to get +# unexpected results if you try to malloc an object larger than this +# bound. +CBMC_OBJECT_BITS ?= 8 + +# CBMC loop unwinding (Normally set in the proof Makefile) +# +# UNWINDSET is a list of pairs of the form foo.1:4 meaning that +# CBMC should unwind loop 1 in function foo no more than 4 times. +# For historical reasons, the number 4 is one more than the number +# of times CBMC actually unwinds the loop. +UNWINDSET ?= + +# CBMC function removal (Normally set set in the proof Makefile) +# +# REMOVE_FUNCTION_BODY is a list of function names. CBMC will "undefine" +# the function, and CBMC will treat the function as having no side effects +# and returning an unconstrained value of the appropriate return type. +# The list should include the names of functions being stubbed out. +REMOVE_FUNCTION_BODY ?= + +# The project source files (Normally set set in the proof Makefile) +# +# PROJECT_SOURCES is the list of project source files to compile, +# including the source file defining the function under test. +PROJECT_SOURCES ?= + +# The proof source files (Normally set in the proof Makefile) +# +# PROOF_SOURCES is the list of proof source files to compile, including +# the proof harness, and including any function stubs being used. +PROOF_SOURCES ?= + +# The number of seconds that CBMC should be allowed to run for before +# being forcefully terminated. Currently, this is set to be less than +# the time limit for a CodeBuild job, which is eight hours. If a proof +# run takes longer than the time limit of the CI environment, the +# environment will halt the proof run without updating the Litani +# report, making the proof run appear to "hang". +CBMC_TIMEOUT ?= 21600 + +# 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. +# 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)) + +USE_FUNCTION_CONTRACTS ?= "" +CBMC_USE_FUNCTION_CONTRACTS := $(patsubst %,--replace-call-with-contract %, $(USE_FUNCTION_CONTRACTS)) + +# 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 + +################################################################ +################################################################ +## Section II: This section is for project-specific definitions + + +################################################################ +################################################################ +## Section II: This section defines the process of running a proof +## +## There should be no reason to edit anything below this line. + +################################################################ +# Paths + +CBMC ?= cbmc +GOTO_ANALYZER ?= goto-analyzer +GOTO_CC ?= goto-cc +GOTO_INSTRUMENT ?= goto-instrument +VIEWER ?= cbmc-viewer +MAKE_SOURCE ?= make-source +VIEWER2 ?= cbmc-viewer +CMAKE ?= cmake +ARPA ?= @echo "You must set ARPA in Makefile-project-defines to run arpa in this project"; false + +GOTODIR ?= $(PROOFDIR)/gotos +LOGDIR ?= $(PROOFDIR)/logs + +PROJECT ?= project +PROOF ?= proof + +HARNESS_GOTO ?= $(GOTODIR)/$(HARNESS_FILE) +PROJECT_GOTO ?= $(GOTODIR)/$(PROJECT) +PROOF_GOTO ?= $(GOTODIR)/$(PROOF) + +ARPA_BLDDIR ?= $(abspath $(PROOFDIR)/arpa_cmake) +ARPA_COMP_CMDS ?= $(ARPA_BLDDIR)/compile_commands.json + +################################################################ +# Useful macros for values that are hard to reference +SPACE :=$() $() +COMMA :=, + +################################################################ +# Set C compiler defines + +CBMCFLAGS += --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 +ifdef UNWINDSET + ifneq ($(strip $(UNWINDSET)),"") + CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET))) + endif +endif +CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY)) + +################################################################ +# Build targets that make the relevant .goto files + +# Compile project sources +$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) + $(LITANI) add-job \ + --command \ + '$(GOTO_CC) $(CBMC_VERBOSITY) --export-file-local-symbols $(COMPILE_FLAGS) $(INCLUDES) $(DEFINES) $^ -o $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/project_sources-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): building project binary" + +# Compile proof sources +$(PROOF_GOTO)1.goto: $(PROOF_SOURCES) + $(LITANI) add-job \ + --command \ + '$(GOTO_CC) $(CBMC_VERBOSITY) --export-file-local-symbols $(COMPILE_FLAGS) $(INCLUDES) $(DEFINES) $^ -o $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/proof_sources-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): building proof binary" + +# Optionally remove function bodies from project sources +$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto +ifeq ($(REMOVE_FUNCTION_BODY),"") + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not removing function bodies from project sources" +else + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/remove_function_body-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): removing function bodies from project sources" +endif + +# Link project and proof sources into the proof harness +$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto + $(LITANI) add-job \ + --command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ -o $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/link_proof_project-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): linking project to proof" + +# Optionally check function contracts +$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto +ifeq ($(CHECK_FUNCTION_CONTRACTS),"") + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not checking function contracts" +else + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/check_function_contracts-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): checking function contracts" +endif + +# Optionally replace function calls with function contracts +$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto +ifeq ($(USE_FUNCTION_CONTRACTS),"") + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not replacing function calls with function contracts" +else + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/use_function_contracts-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): replacing function calls with function contracts" +endif + +# Optionally apply loop contracts +$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto +ifneq ($(APPLY_LOOP_CONTRACTS),1) + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not applying loop contracts" +else + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --apply-loop-contracts $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): applying loop contracts" +endif + +# Optionally fill static variable with unconstrained values +$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto +ifeq ($(NONDET_STATIC),"") + $(LITANI) add-job \ + --command 'cp $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): not setting static variables to nondet" +else + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/nondet_static-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): setting static variables to nondet" +endif + +# Omit unused functions (sharpens coverage calculations) +$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): dropping unused functions" + +# Omit initialization of unused global variables (reduces problem size) +$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/slice_global_inits-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): slicing global initializations" + +# Final name for proof harness +$(HARNESS_GOTO).goto: $(HARNESS_GOTO)7.goto + $(LITANI) add-job \ + --command 'cp $< $@' \ + --inputs $^ \ + --outputs $@ \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): copying final goto-binary" + +################################################################ +# Targets to run Arpa + +$(ARPA_BLDDIR): + $(CMAKE) $(ARPA_CMAKE_FLAGS) \ + -DCMAKE_EXPORT_COMPILE_COMMANDS=1 \ + -B $(ARPA_BLDDIR) \ + -S $(SRCDIR) + +arpa: $(ARPA_BLDDIR) + $(ARPA) run -cc $(ARPA_COMP_CMDS) -r $(SRCDIR) + +################################################################ +# Targets to run the analysis commands + +$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto + $(LITANI) add-job \ + $(POOL) \ + --command \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(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)/result.xml: $(HARNESS_GOTO).goto + $(LITANI) add-job \ + $(POOL) \ + --command \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CHECKFLAGS) --trace --xml-ui $<' \ + --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 \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CHECKFLAGS) --show-properties --xml-ui $<' \ + --inputs $^ \ + --outputs $@ \ + --ci-stage test \ + --stdout-file $@ \ + --ignore-returns 10 \ + --pipeline-name "$(PROOF_UID)" \ + --stderr-file $(LOGDIR)/property-err-log.txt \ + --description "$(PROOF_UID): printing safety properties" + +$(LOGDIR)/coverage.xml: $(HARNESS_GOTO).goto + $(LITANI) add-job \ + $(POOL) \ + --command \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(COVERFLAGS) --cover location --xml-ui $<' \ + --inputs $^ \ + --outputs $@ \ + --ci-stage test \ + --stdout-file $@ \ + $(MEMORY_PROFILING) \ + --ignore-returns 10 \ + --timeout $(CBMC_TIMEOUT) \ + --pipeline-name "$(PROOF_UID)" \ + --tags "stats-group:coverage computation" \ + --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 \ + --interleave-stdout-stderr \ + --description "$(PROOF_UID): generating report" + + +# 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 +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 + $(LITANI) add-job \ + --command "$$VIEWER2_CMD" \ + --inputs $^ \ + --outputs $(PROOFDIR)/report \ + --pipeline-name "$(PROOF_UID)" \ + --stdout-file $(LOGDIR)/viewer-log.txt \ + --interleave-stdout-stderr \ + --ci-stage report \ + --description "$(PROOF_UID): generating report" + +litani-path: + @echo $(LITANI) + +# ############################################################## +# Phony Rules +# +# These rules provide a convenient way to run a single proof up to a +# certain stage. Users can browse into a proof directory and run +# "make -Bj 3 report" to generate a report for just that proof, or +# "make goto" to build the goto binary. Under the hood, this runs litani +# for just that proof. + +_goto: $(HARNESS_GOTO).goto +goto: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _goto + $(LITANI) run-build + +_result: $(LOGDIR)/result.txt +result: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _result + $(LITANI) run-build + +_property: $(LOGDIR)/property.xml +property: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _property + $(LITANI) run-build + +_coverage: $(LOGDIR)/coverage.xml +coverage: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _coverage + $(LITANI) run-build + +_report: $(PROOFDIR)/html +report: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _report + $(LITANI) run-build + +_report2: $(PROOFDIR)/report +report2: + $(LITANI) init --project $(PROJECT_NAME) + $(MAKE) -B _report2 + $(LITANI) run-build + + +################################################################ +# Targets to clean up after ourselves +clean: + -$(RM) $(DEPENDENT_GOTOS) + -$(RM) TAGS* + -$(RM) *~ \#* + -$(RM) Makefile.arpa + -$(RM) -r $(ARPA_BLDDIR) + +veryclean: clean + -$(RM) -r html report + -$(RM) -r $(LOGDIR) $(GOTODIR) + +.PHONY: \ + _coverage \ + _goto \ + _property \ + _report \ + _report2 \ + _result \ + arpa \ + clean \ + coverage \ + goto \ + litani-path \ + property \ + report \ + report2 \ + result \ + setup_dependencies \ + testdeps \ + veryclean \ + # + +################################################################ + +# 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. + +.PHONY: echo-proof-uid +echo-proof-uid: + @echo $(PROOF_UID) + +.PHONY: echo-project-name +echo-project-name: + @echo $(PROJECT_NAME) + +################################################################ + +# Project-specific targets requiring values defined above +sinclude $(PROOF_ROOT)/Makefile-project-targets + +# CI-specific targets to drive cbmc in CI +sinclude $(PROOF_ROOT)/Makefile-project-testing + +################################################################ diff --git a/test/cbmc/proofs/README.md b/test/cbmc/proofs/README.md new file mode 100644 index 000000000..5e22aa01a --- /dev/null +++ b/test/cbmc/proofs/README.md @@ -0,0 +1,27 @@ +CBMC proofs +=========== + +This directory contains the CBMC proofs. Each proof is in its own +directory. + +This directory includes four Makefiles. + +One Makefile describes the basic workflow for building and running proofs: + +* Makefile.common: + * make: builds the goto binary, does the cbmc property checking + and coverage checking, and builds the final report. + * make goto: builds the goto binary + * make result: does cbmc property checking + * make coverage: does cbmc coverage checking + * make report: builds the final report + +Three included Makefiles describe project-specific settings and can override +definitions in Makefile.common: + +* Makefile-project-defines: definitions like compiler flags + required to build the goto binaries, and definitions to override + definitions in Makefile.common. +* Makefile-project-targets: other make targets needed for the project +* Makefile-project-testing: other definitions and targets needed for + unit testing or continuous integration. diff --git a/test/cbmc/proofs/prepare.py b/test/cbmc/proofs/prepare.py new file mode 100644 index 000000000..d58805cad --- /dev/null +++ b/test/cbmc/proofs/prepare.py @@ -0,0 +1,54 @@ +#!/usr/bin/env python3 + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + + +"""Prepare the source tree for proofs in continuous integration.""" + + +import os +import subprocess + + +MAKEFILE = "Makefile" +CBMC_BATCH_YAML = "cbmc-batch.yaml" + + +def create_cbmc_batch_yaml(folder): + """Run make to create cbmc-batch.yaml in folder.""" + + try: + subprocess.run( + ["make", "-B", CBMC_BATCH_YAML], + cwd=folder, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + universal_newlines=True, + check=True + ) + except subprocess.CalledProcessError as error: + raise UserWarning("Failed to create {} in {}: " + "command was '{}': " + "error was '{}'" + .format(CBMC_BATCH_YAML, folder, + ' '.join(error.cmd), + error.stderr.strip())) from None + + +def create_cbmc_batch_yaml_files(root='.'): + """Create cbmc-batch.yaml in all directories under root.""" + + for folder, _, files in os.walk(root): + if CBMC_BATCH_YAML in files and MAKEFILE in files: + create_cbmc_batch_yaml(folder) + + +def prepare(): + """Prepare the source tree for proofs in continuous integration.""" + + create_cbmc_batch_yaml_files() + + +if __name__ == "__main__": + prepare() diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py new file mode 100755 index 000000000..33d0f778f --- /dev/null +++ b/test/cbmc/proofs/run-cbmc-proofs.py @@ -0,0 +1,365 @@ +#!/usr/bin/env python3 +# +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + + +import argparse +import asyncio +import json +import logging +import math +import os +import pathlib +import re +import subprocess +import sys + + +DESCRIPTION = "Configure and run all CBMC proofs in parallel" + +# Keep the epilog hard-wrapped at 70 characters, as it gets printed +# verbatim in the terminal. 70 characters stops here --------------> | +EPILOG = """ +This tool automates the process of running `make report` in each of +the CBMC proof directories. The tool calculates the dependency graph +of all tasks needed to build, run, and report on all the proofs, and +executes these tasks in parallel. + +The tool is roughly equivalent to doing this: + + litani init --project "my-cool-project"; + + find . -name cbmc-proof.txt | while read -r proof; do + pushd $(dirname ${proof}); + + # The `make _report` rule adds a single proof to litani + # without running it + make _report; + + popd; + done + + litani run-build; + +except that it is much faster and provides some convenience options. +The CBMC CI runs this script with no arguments to build and run all +proofs in parallel. The value of "my-cool-project" is taken from the +PROJECT_NAME variable in Makefile-project-defines. + +The --no-standalone argument omits the `litani init` and `litani +run-build`; use it when you want to add additional proof jobs, not +just the CBMC ones. In that case, you would run `litani init` +yourself; then run `run-cbmc-proofs --no-standalone`; add any +additional jobs that you want to execute with `litani add-job`; and +finally run `litani run-build`. + +The litani dashboard will be written under the `output` directory; the +cbmc-viewer reports remain in the `$PROOF_DIR/report` directory. The +HTML dashboard from the latest Litani run will always be symlinked to +`output/latest/html/index.html`, so you can keep that page open in +your browser and reload the page whenever you re-run this script. +""" +# 70 characters stops here ----------------------------------------> | + + +def get_project_name(): + cmd = [ + "make", + "-f", "Makefile.common", + "echo-project-name", + ] + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE) + if proc.returncode: + logging.critical("could not run make to determine project name") + sys.exit(1) + if not proc.stdout.strip(): + logging.warning( + "project name has not been set; using generic name instead. " + "Set the PROJECT_NAME value in Makefile-project-defines to " + "remove this warning") + return "" + return proc.stdout.strip() + + +def get_args(): + pars = argparse.ArgumentParser( + description=DESCRIPTION, epilog=EPILOG, + formatter_class=argparse.RawDescriptionHelpFormatter) + for arg in [{ + "flags": ["-j", "--parallel-jobs"], + "type": int, + "metavar": "N", + "help": "run at most N proof jobs in parallel", + }, { + "flags": ["--no-standalone"], + "action": "store_true", + "help": "only configure proofs: do not initialize nor run", + }, { + "flags": ["-p", "--proofs"], + "nargs": "+", + "metavar": "DIR", + "help": "only run proof in directory DIR (can pass more than one)", + }, { + "flags": ["--project-name"], + "metavar": "NAME", + "default": get_project_name(), + "help": "project name for report. Default: %(default)s", + }, { + "flags": ["--proof-marker"], + "metavar": "FILE", + "default": "cbmc-proof.txt", + "help": ( + "name of file that marks proof directories. Default: " + "%(default)s"), + }, { + "flags": ["--no-memory-profile"], + "action": "store_true", + "help": "disable memory profiling, even if Litani supports it" + }, { + "flags": ["--no-expensive-limit"], + "action": "store_true", + "help": "do not limit parallelism of 'EXPENSIVE' jobs", + }, { + "flags": ["--expensive-jobs-parallelism"], + "metavar": "N", + "default": 1, + "type": int, + "help": ( + "how many proof jobs marked 'EXPENSIVE' to run in parallel. " + "Default: %(default)s"), + }, { + "flags": ["--verbose"], + "action": "store_true", + "help": "verbose output", + }]: + flags = arg.pop("flags") + pars.add_argument(*flags, **arg) + return pars.parse_args() + + +def set_up_logging(verbose): + if verbose: + level = logging.DEBUG + else: + level = logging.WARNING + logging.basicConfig( + format="run-cbmc-proofs: %(message)s", level=level) + + +def task_pool_size(): + ret = os.cpu_count() + if ret is None or ret < 3: + return 1 + return ret - 2 + + +def print_counter(counter): + print( + "\rConfiguring CBMC proofs: " + "{complete:{width}} / {total:{width}}".format( + **counter), end="", file=sys.stderr) + + +def get_proof_dirs(proof_root, proof_list, proof_marker): + if proof_list is not None: + proofs_remaining = list(proof_list) + else: + proofs_remaining = [] + + for root, _, fyles in os.walk(proof_root): + proof_name = str(pathlib.Path(root).name) + if proof_list and proof_name not in proof_list: + continue + if proof_list and proof_name in proofs_remaining: + proofs_remaining.remove(proof_name) + if proof_marker in fyles: + yield root + + if proofs_remaining: + logging.critical( + "The following proofs were not found: %s", + ", ".join(proofs_remaining)) + sys.exit(1) + + +def run_build(litani, jobs): + cmd = [str(litani), "run-build"] + if jobs: + cmd.extend(["-j", str(jobs)]) + + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd) + if proc.returncode: + logging.critical("Failed to run litani run-build") + sys.exit(1) + + +def get_litani_path(proof_root): + cmd = [ + "make", + "PROOF_ROOT=%s" % proof_root, + "-f", "Makefile.common", + "litani-path", + ] + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE) + if proc.returncode: + logging.critical("Could not determine path to litani") + sys.exit(1) + return proc.stdout.strip() + + +def get_litani_capabilities(litani_path): + cmd = [litani_path, "print-capabilities"] + proc = subprocess.run( + cmd, text=True, stdout=subprocess.PIPE, stderr=subprocess.DEVNULL) + if proc.returncode: + return [] + try: + return json.loads(proc.stdout) + except RuntimeError: + logging.warning("Could not load litani capabilities: '%s'", proc.stdout) + return [] + + +def check_uid_uniqueness(proof_dir, proof_uids): + with (pathlib.Path(proof_dir) / "Makefile").open() as handle: + for line in handle: + m = re.match(r"^PROOF_UID\s*=\s*(?P\w+)", line) + if not m: + continue + if m["uid"] not in proof_uids: + proof_uids[m["uid"]] = proof_dir + return + + logging.critical( + "The Makefile in directory '%s' should have a different " + "PROOF_UID than the Makefile in directory '%s'", + proof_dir, proof_uids[m["uid"]]) + sys.exit(1) + + logging.critical( + "The Makefile in directory '%s' should contain a line like", proof_dir) + logging.critical("PROOF_UID = ...") + logging.critical("with a unique identifier for the proof.") + sys.exit(1) + + +def should_enable_memory_profiling(litani_caps, args): + if args.no_memory_profile: + return False + return "memory_profile" in litani_caps + + +def should_enable_pools(litani_caps, args): + if args.no_expensive_limit: + return False + return "pools" in litani_caps + + +async def configure_proof_dirs( + queue, counter, proof_uids, enable_pools, enable_memory_profiling): + while True: + print_counter(counter) + path = str(await queue.get()) + + check_uid_uniqueness(path, proof_uids) + + pools = ["ENABLE_POOLS=true"] if enable_pools else [] + profiling = [ + "ENABLE_MEMORY_PROFILING=true"] if enable_memory_profiling else [] + + proc = await asyncio.create_subprocess_exec( + # Allow interactive tasks to preempt proof configuration + "nice", "-n", "15", "make", *pools, *profiling, "-B", "--quiet", + "_report", cwd=path) + await proc.wait() + counter["fail" if proc.returncode else "pass"].append(path) + counter["complete"] += 1 + + print_counter(counter) + queue.task_done() + + +async def main(): + args = get_args() + set_up_logging(args.verbose) + + proof_root = pathlib.Path(__file__).resolve().parent + litani = get_litani_path(proof_root) + + litani_caps = get_litani_capabilities(litani) + enable_pools = should_enable_pools(litani_caps, args) + init_pools = [ + "--pools", f"expensive:{args.expensive_jobs_parallelism}" + ] if enable_pools else [] + + if not args.no_standalone: + cmd = [str(litani), "init", *init_pools, "--project", args.project_name] + + if "output_directory_flags" in litani_caps: + out_prefix = proof_root / "output" + out_symlink = out_prefix / "latest" + out_index = out_symlink / "html" / "index.html" + cmd.extend([ + "--output-prefix", str(out_prefix), + "--output-symlink", str(out_symlink), + ]) + print( + "\nFor your convenience, the output of this run will be " + "symbolically linked to %s\n" % str(out_index)) + + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd) + if proc.returncode: + logging.critical("Failed to run litani init") + sys.exit(1) + + proof_dirs = list(get_proof_dirs( + proof_root, args.proofs, args.proof_marker)) + if not proof_dirs: + logging.critical("No proof directories found") + sys.exit(1) + + proof_queue = asyncio.Queue() + for proof_dir in proof_dirs: + proof_queue.put_nowait(proof_dir) + + counter = { + "pass": [], + "fail": [], + "complete": 0, + "total": len(proof_dirs), + "width": int(math.log10(len(proof_dirs))) + 1 + } + + proof_uids = {} + tasks = [] + + enable_memory_profiling = should_enable_memory_profiling(litani_caps, args) + + for _ in range(task_pool_size()): + task = asyncio.create_task(configure_proof_dirs( + proof_queue, counter, proof_uids, enable_pools, + enable_memory_profiling)) + tasks.append(task) + + await proof_queue.join() + + print_counter(counter) + print("", file=sys.stderr) + + if counter["fail"]: + logging.critical( + "Failed to configure the following proofs:\n%s", "\n".join( + [str(f) for f in counter["fail"]])) + sys.exit(1) + + if not args.no_standalone: + run_build(litani, args.parallel_jobs) + + +if __name__ == "__main__": + asyncio.run(main()) From 21ee448b512bfe648bf7d8ba5323221111363e4e Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 5 Aug 2021 10:30:48 +0000 Subject: [PATCH 03/29] Added value to not update the submodule --- .gitmodules | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.gitmodules b/.gitmodules index bfe815c15..de2986481 100644 --- a/.gitmodules +++ b/.gitmodules @@ -11,6 +11,8 @@ [submodule "test/cbmc/aws-templates-for-cbmc-proofs"] path = test/cbmc/aws-templates-for-cbmc-proofs url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git + update = none [submodule "test/cbmc/litani"] path = test/cbmc/litani url = https://github.com/awslabs/aws-build-accumulator.git + update = none \ No newline at end of file From 4b189aa8bc35bcce0420f9418ca5845e82854301 Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 5 Aug 2021 11:08:25 +0000 Subject: [PATCH 04/29] Added Include paths and preprocessor defines --- test/cbmc/proofs/Makefile.common | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common index fb0844b70..3e9c0b05d 100644 --- a/test/cbmc/proofs/Makefile.common +++ b/test/cbmc/proofs/Makefile.common @@ -260,10 +260,10 @@ COMPILE_FLAGS ?= LINK_FLAGS ?= # Preprocessor include paths -I... -INCLUDES ?= +INCLUDES += -I$(SRCDIR)/source/include/ # Preprocessor definitions -D... -DEFINES ?= +DEFINES += -DOTA_DO_NOT_USE_CUSTOM_CONFIG # CBMC object model # @@ -860,3 +860,4 @@ sinclude $(PROOF_ROOT)/Makefile-project-targets sinclude $(PROOF_ROOT)/Makefile-project-testing ################################################################ + From ae17c099ef0158df7b75a9f33d9dec08f8b0fa05 Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 5 Aug 2021 11:29:02 +0000 Subject: [PATCH 05/29] Added template define file --- test/cbmc/proofs/Makefile-template-defines | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test/cbmc/proofs/Makefile-template-defines diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines new file mode 100644 index 000000000..5b09353ac --- /dev/null +++ b/test/cbmc/proofs/Makefile-template-defines @@ -0,0 +1,11 @@ + +# Absolute path to the root of the source tree. +# +SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..) + + +# Absolute path to the litani script. +# +LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani) +PROJECT_NAME = "AWS IoT Over-the-air Update Library" + From 4a2ed43c36c1b18be3adb9d51097c7ea6c569c80 Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 5 Aug 2021 11:36:42 +0000 Subject: [PATCH 06/29] Updated to ignore the output files on git push --- test/cbmc/.gitignore | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 test/cbmc/.gitignore diff --git a/test/cbmc/.gitignore b/test/cbmc/.gitignore new file mode 100644 index 000000000..1e5826a7b --- /dev/null +++ b/test/cbmc/.gitignore @@ -0,0 +1,24 @@ +# Emitted when running CBMC proofs +proofs/**/logs +proofs/**/gotos +proofs/**/report +proofs/**/html +proofs/output + +# Emitted by CBMC Viewer +TAGS-* + +# Emitted by Arpa +arpa_cmake/ +arpa-validation-logs/ +Makefile.arpa + +# Emitted by litani +.ninja_deps +.ninja_log +.litani_cache_dir + +# These files should be overwritten whenever prepare.py runs +cbmc-batch.yaml + +__pycache__/ From 6c5d6f5c547fd0188c8b6ab2d59d375c7744a8b6 Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 5 Aug 2021 11:47:15 +0000 Subject: [PATCH 07/29] Added words --- tools/lexicon.txt | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/tools/lexicon.txt b/tools/lexicon.txt index df311aafa..c9252ccc3 100644 --- a/tools/lexicon.txt +++ b/tools/lexicon.txt @@ -28,6 +28,7 @@ bitmaplen bitmask blockbitmapmaxsize blockbitmapsize +blockid blockindex blockindex blockoffset @@ -47,6 +48,7 @@ bytestosend c89 c90 ca +cbmc cbor cborarray cborerror @@ -98,6 +100,7 @@ cwd datablock datacallback datalength +decodeandstoredatablock decodemem decodememmaxsize decodememorysize @@ -113,6 +116,7 @@ destlen destoffset developerguide didn +div dns docmodel docparam @@ -548,6 +552,7 @@ pfilepath pfinalfile pformat phostname +phttp pjobdocjson pjobid pjobname @@ -702,6 +707,7 @@ sendtimeout sendtimeoutms serverfileid serverinfo +setcontrolinterface setdatainterface setimagestate setplatformimagestate @@ -715,6 +721,7 @@ snihostname sockaddr sockets_invalid_parameter socketstatus +spdx srand src ssl @@ -801,6 +808,7 @@ urlsize useraborthandler ustopiclen utils +validateandstartjob validatedatablock valuelength verifyactivejobstatus From b4a774c19cfd4342e4584d880ee64f56bc745cee Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 5 Aug 2021 12:00:06 +0000 Subject: [PATCH 08/29] Updated Project Name --- test/cbmc/proofs/Makefile-template-defines | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines index 5b09353ac..a9e99859d 100644 --- a/test/cbmc/proofs/Makefile-template-defines +++ b/test/cbmc/proofs/Makefile-template-defines @@ -1,11 +1,19 @@ # Absolute path to the root of the source tree. # -SRCDIR ?= $(abspath $(PROOF_ROOT)/../../..) +SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../ota-for-aws-iot-emebedded-sdk) # Absolute path to the litani script. # LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani) + + +# Name of this proof project, displayed in proof reports. For example, +# "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots, +# this may be overridden on the command-line to Make, for example +# +# make PROJECT_NAME="FreeRTOS MQTT" report +# PROJECT_NAME = "AWS IoT Over-the-air Update Library" From db409b71cef47072f2382862d55178c0da22d13b Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 5 Aug 2021 12:31:55 +0000 Subject: [PATCH 09/29] Updated source directory path --- test/cbmc/proofs/Makefile-template-defines | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines index a9e99859d..0c8a3c391 100644 --- a/test/cbmc/proofs/Makefile-template-defines +++ b/test/cbmc/proofs/Makefile-template-defines @@ -1,7 +1,7 @@ # Absolute path to the root of the source tree. # -SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../ota-for-aws-iot-emebedded-sdk) +SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../ota-for-aws-iot-embedded-sdk/) # Absolute path to the litani script. From 92b5b005b95bc60a48bcef4899b47b96068b257b Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Thu, 5 Aug 2021 09:25:19 -0700 Subject: [PATCH 10/29] Update ci.yml --- .github/workflows/ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8b98744ef..383b68fd5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -7,6 +7,7 @@ on: branches: - main - development + - cbmc-proof workflow_dispatch: jobs: From 62ddec4f502b2d27278d2f889252792828f6bd25 Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Thu, 5 Aug 2021 09:26:17 -0700 Subject: [PATCH 11/29] Add checks on the branch --- .github/workflows/ci.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8b98744ef..383b68fd5 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -7,6 +7,7 @@ on: branches: - main - development + - cbmc-proof workflow_dispatch: jobs: From 67ad6b0fb286e263992d7658abd9e94483f5710c Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 5 Aug 2021 16:33:53 +0000 Subject: [PATCH 12/29] Updated Submodule update value --- .gitmodules | 1 - 1 file changed, 1 deletion(-) diff --git a/.gitmodules b/.gitmodules index de2986481..04bdf5d8e 100644 --- a/.gitmodules +++ b/.gitmodules @@ -15,4 +15,3 @@ [submodule "test/cbmc/litani"] path = test/cbmc/litani url = https://github.com/awslabs/aws-build-accumulator.git - update = none \ No newline at end of file From 3bda16abcd0cf4719896abcb16c3d36285ead9f2 Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 5 Aug 2021 16:46:47 +0000 Subject: [PATCH 13/29] Added litani submodule update --- .gitmodules | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitmodules b/.gitmodules index 04bdf5d8e..de2986481 100644 --- a/.gitmodules +++ b/.gitmodules @@ -15,3 +15,4 @@ [submodule "test/cbmc/litani"] path = test/cbmc/litani url = https://github.com/awslabs/aws-build-accumulator.git + update = none \ No newline at end of file From 2c7f2eee2df4b4e072e58f2ecfccc7aec647c12f Mon Sep 17 00:00:00 2001 From: Bhaumik Jain <86116186+Bujain@users.noreply.github.com> Date: Thu, 5 Aug 2021 09:51:09 -0700 Subject: [PATCH 14/29] Update Project name Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> --- test/cbmc/proofs/Makefile-template-defines | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines index 0c8a3c391..a4fcaa007 100644 --- a/test/cbmc/proofs/Makefile-template-defines +++ b/test/cbmc/proofs/Makefile-template-defines @@ -13,7 +13,6 @@ LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani) # "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots, # this may be overridden on the command-line to Make, for example # -# make PROJECT_NAME="FreeRTOS MQTT" report +# make PROJECT_NAME="AWS IoT Over-the-air Update Library" report # PROJECT_NAME = "AWS IoT Over-the-air Update Library" - From e88c8c02d940e62bee9919b1870622e84c23f4d4 Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 5 Aug 2021 16:52:43 +0000 Subject: [PATCH 15/29] Added new line in the end of the file --- .gitmodules | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.gitmodules b/.gitmodules index de2986481..a53db1696 100644 --- a/.gitmodules +++ b/.gitmodules @@ -15,4 +15,5 @@ [submodule "test/cbmc/litani"] path = test/cbmc/litani url = https://github.com/awslabs/aws-build-accumulator.git - update = none \ No newline at end of file + update = none + \ No newline at end of file From d274f81a503e530b3b1251f1223b408c4660a40d Mon Sep 17 00:00:00 2001 From: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> Date: Thu, 5 Aug 2021 09:54:41 -0700 Subject: [PATCH 16/29] Remove whitespace --- .gitmodules | 1 - 1 file changed, 1 deletion(-) diff --git a/.gitmodules b/.gitmodules index a53db1696..89f9e83c9 100644 --- a/.gitmodules +++ b/.gitmodules @@ -16,4 +16,3 @@ path = test/cbmc/litani url = https://github.com/awslabs/aws-build-accumulator.git update = none - \ No newline at end of file From a085b6a8d4987e6d911a3abf48a7eadf6e27d9d1 Mon Sep 17 00:00:00 2001 From: Bhaumik Jain <86116186+Bujain@users.noreply.github.com> Date: Thu, 5 Aug 2021 16:24:02 -0700 Subject: [PATCH 17/29] Addition to CBMC infrastructure (#243) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * Added new line in the end of the file * Remove whitespace Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> --- .gitmodules | 2 ++ test/cbmc/.gitignore | 24 ++++++++++++++++++++++ test/cbmc/proofs/Makefile-template-defines | 18 ++++++++++++++++ test/cbmc/proofs/Makefile.common | 4 ++-- tools/lexicon.txt | 8 ++++++++ 5 files changed, 54 insertions(+), 2 deletions(-) create mode 100644 test/cbmc/.gitignore create mode 100644 test/cbmc/proofs/Makefile-template-defines diff --git a/.gitmodules b/.gitmodules index bfe815c15..89f9e83c9 100644 --- a/.gitmodules +++ b/.gitmodules @@ -11,6 +11,8 @@ [submodule "test/cbmc/aws-templates-for-cbmc-proofs"] path = test/cbmc/aws-templates-for-cbmc-proofs url = https://github.com/awslabs/aws-templates-for-cbmc-proofs.git + update = none [submodule "test/cbmc/litani"] path = test/cbmc/litani url = https://github.com/awslabs/aws-build-accumulator.git + update = none diff --git a/test/cbmc/.gitignore b/test/cbmc/.gitignore new file mode 100644 index 000000000..1e5826a7b --- /dev/null +++ b/test/cbmc/.gitignore @@ -0,0 +1,24 @@ +# Emitted when running CBMC proofs +proofs/**/logs +proofs/**/gotos +proofs/**/report +proofs/**/html +proofs/output + +# Emitted by CBMC Viewer +TAGS-* + +# Emitted by Arpa +arpa_cmake/ +arpa-validation-logs/ +Makefile.arpa + +# Emitted by litani +.ninja_deps +.ninja_log +.litani_cache_dir + +# These files should be overwritten whenever prepare.py runs +cbmc-batch.yaml + +__pycache__/ diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines new file mode 100644 index 000000000..a4fcaa007 --- /dev/null +++ b/test/cbmc/proofs/Makefile-template-defines @@ -0,0 +1,18 @@ + +# Absolute path to the root of the source tree. +# +SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../ota-for-aws-iot-embedded-sdk/) + + +# Absolute path to the litani script. +# +LITANI ?= $(abspath $(PROOF_ROOT)/../litani/litani) + + +# Name of this proof project, displayed in proof reports. For example, +# "s2n" or "Amazon FreeRTOS". For projects with multiple proof roots, +# this may be overridden on the command-line to Make, for example +# +# make PROJECT_NAME="AWS IoT Over-the-air Update Library" report +# +PROJECT_NAME = "AWS IoT Over-the-air Update Library" diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common index fb0844b70..92d6b0edf 100644 --- a/test/cbmc/proofs/Makefile.common +++ b/test/cbmc/proofs/Makefile.common @@ -260,10 +260,10 @@ COMPILE_FLAGS ?= LINK_FLAGS ?= # Preprocessor include paths -I... -INCLUDES ?= +INCLUDES += -I$(SRCDIR)/source/include/ # Preprocessor definitions -D... -DEFINES ?= +DEFINES += -DOTA_DO_NOT_USE_CUSTOM_CONFIG # CBMC object model # diff --git a/tools/lexicon.txt b/tools/lexicon.txt index df311aafa..c9252ccc3 100644 --- a/tools/lexicon.txt +++ b/tools/lexicon.txt @@ -28,6 +28,7 @@ bitmaplen bitmask blockbitmapmaxsize blockbitmapsize +blockid blockindex blockindex blockoffset @@ -47,6 +48,7 @@ bytestosend c89 c90 ca +cbmc cbor cborarray cborerror @@ -98,6 +100,7 @@ cwd datablock datacallback datalength +decodeandstoredatablock decodemem decodememmaxsize decodememorysize @@ -113,6 +116,7 @@ destlen destoffset developerguide didn +div dns docmodel docparam @@ -548,6 +552,7 @@ pfilepath pfinalfile pformat phostname +phttp pjobdocjson pjobid pjobname @@ -702,6 +707,7 @@ sendtimeout sendtimeoutms serverfileid serverinfo +setcontrolinterface setdatainterface setimagestate setplatformimagestate @@ -715,6 +721,7 @@ snihostname sockaddr sockets_invalid_parameter socketstatus +spdx srand src ssl @@ -801,6 +808,7 @@ urlsize useraborthandler ustopiclen utils +validateandstartjob validatedatablock valuelength verifyactivejobstatus From fcb1efe7f630b319e836a7023f8d164fa740d332 Mon Sep 17 00:00:00 2001 From: Bhaumik Jain <86116186+Bujain@users.noreply.github.com> Date: Fri, 6 Aug 2021 16:20:15 -0700 Subject: [PATCH 18/29] Added CBMC proof of setDataInterface function (#245) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for setDataInterface function * removed unnecessary variables * Updated documentation * Uncrustified * Updated year in copyright notice Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> --- test/cbmc/proofs/Makefile-template-defines | 3 +- test/cbmc/proofs/setDataInterface/Makefile | 25 ++++++++++ test/cbmc/proofs/setDataInterface/README.md | 20 ++++++++ .../proofs/setDataInterface/cbmc-proof.txt | 2 + .../proofs/setDataInterface/cbmc-viewer.json | 6 +++ .../setDataInterface_harness.c | 49 +++++++++++++++++++ 6 files changed, 103 insertions(+), 2 deletions(-) create mode 100644 test/cbmc/proofs/setDataInterface/Makefile create mode 100644 test/cbmc/proofs/setDataInterface/README.md create mode 100644 test/cbmc/proofs/setDataInterface/cbmc-proof.txt create mode 100644 test/cbmc/proofs/setDataInterface/cbmc-viewer.json create mode 100644 test/cbmc/proofs/setDataInterface/setDataInterface_harness.c diff --git a/test/cbmc/proofs/Makefile-template-defines b/test/cbmc/proofs/Makefile-template-defines index a4fcaa007..a4673d1a2 100644 --- a/test/cbmc/proofs/Makefile-template-defines +++ b/test/cbmc/proofs/Makefile-template-defines @@ -1,8 +1,7 @@ # Absolute path to the root of the source tree. # -SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../../ota-for-aws-iot-embedded-sdk/) - +SRCDIR ?= $(abspath $(PROOF_ROOT)/../../../) # Absolute path to the litani script. # diff --git a/test/cbmc/proofs/setDataInterface/Makefile b/test/cbmc/proofs/setDataInterface/Makefile new file mode 100644 index 000000000..5c1616df7 --- /dev/null +++ b/test/cbmc/proofs/setDataInterface/Makefile @@ -0,0 +1,25 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY = setDataInterface_harness +HARNESS_FILE = $(HARNESS_ENTRY) + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = setDataInterface + +DEFINES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/source/ota_interface.c + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +include ../Makefile.common diff --git a/test/cbmc/proofs/setDataInterface/README.md b/test/cbmc/proofs/setDataInterface/README.md new file mode 100644 index 000000000..48169f993 --- /dev/null +++ b/test/cbmc/proofs/setDataInterface/README.md @@ -0,0 +1,20 @@ +setDataInterface proof +============== + +This directory contains a memory safety proof for setDataInterface. + +To run the proof. +------------- + +* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` + to your path. +* Run `make`. +* Open html/index.html in a web browser. + +To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +------------- + +* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. +* Use Makefile.arpa as the starting point for your proof Makefile by: + 1. Modifying Makefile.arpa (if required). + 2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`). diff --git a/test/cbmc/proofs/setDataInterface/cbmc-proof.txt b/test/cbmc/proofs/setDataInterface/cbmc-proof.txt new file mode 100644 index 000000000..0639406e3 --- /dev/null +++ b/test/cbmc/proofs/setDataInterface/cbmc-proof.txt @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# This file is required by the run-cbmc-proofs.py to differentiate between a proof directory from a normal directory. \ No newline at end of file diff --git a/test/cbmc/proofs/setDataInterface/cbmc-viewer.json b/test/cbmc/proofs/setDataInterface/cbmc-viewer.json new file mode 100644 index 000000000..13f4418c3 --- /dev/null +++ b/test/cbmc/proofs/setDataInterface/cbmc-viewer.json @@ -0,0 +1,6 @@ +{ "expected-missing-functions": + [ + ], + "proof-name": "setDataInterface", + "proof-root": "test/cbmc/proofs" +} diff --git a/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c b/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c new file mode 100644 index 000000000..445d40130 --- /dev/null +++ b/test/cbmc/proofs/setDataInterface/setDataInterface_harness.c @@ -0,0 +1,49 @@ +/* + * AWS IoT Over-the-air Update v3.0.0 + * Copyright (C) 2021 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file setDataInterface_harness.c + * @brief Implements the proof harness for setDataInterface function. + */ +/* Ota interface includes. */ +#include "ota_interface_private.h" + +void setDataInterface_harness() +{ + OtaDataInterface_t * pDataInterface; + OtaDataInterface_t dataInterface; + OtaErr_t err; + + /* The input to the setDataInterface is a buffer statically initialized in the + * source code with its size defined by OTA_PROTOCOL_BUFFER_SIZE. This macro is + * not user configurable and thus the input does not require any constraint. */ + uint8_t pProtocol[ OTA_PROTOCOL_BUFFER_SIZE ]; + + pDataInterface = &dataInterface; + + err = setDataInterface( pDataInterface, pProtocol ); + + /* The function return can only be either of two values i.e OtaErrNone or + * OtaErrInvalidDataProtocol. */ + __CPROVER_assert( ( err == OtaErrInvalidDataProtocol ) || ( err == OtaErrNone ), + "The function return can be either of those values." ); +} From 76eebdda1d966d0f849f98d3f37c5d98dbc64523 Mon Sep 17 00:00:00 2001 From: bujain Date: Mon, 9 Aug 2021 20:17:04 +0000 Subject: [PATCH 19/29] Added CBMC-proof files of stringBuilder function --- test/cbmc/proofs/stringBuilder/Makefile | 28 +++++++ test/cbmc/proofs/stringBuilder/README.md | 20 +++++ test/cbmc/proofs/stringBuilder/cbmc-proof.txt | 1 + .../proofs/stringBuilder/cbmc-viewer.json | 6 ++ .../stringBuilder/stringBuilder_harness.c | 73 +++++++++++++++++++ 5 files changed, 128 insertions(+) create mode 100644 test/cbmc/proofs/stringBuilder/Makefile create mode 100644 test/cbmc/proofs/stringBuilder/README.md create mode 100644 test/cbmc/proofs/stringBuilder/cbmc-proof.txt create mode 100644 test/cbmc/proofs/stringBuilder/cbmc-viewer.json create mode 100644 test/cbmc/proofs/stringBuilder/stringBuilder_harness.c diff --git a/test/cbmc/proofs/stringBuilder/Makefile b/test/cbmc/proofs/stringBuilder/Makefile new file mode 100644 index 000000000..5a6026de9 --- /dev/null +++ b/test/cbmc/proofs/stringBuilder/Makefile @@ -0,0 +1,28 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY = stringBuilder_harness +HARNESS_FILE = $(HARNESS_ENTRY) + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = stringBuilder + +DEFINES += +INCLUDES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +CBMC_FLAG_UNWINDING_ASSERTIONS = + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/source/ota_mqtt.c + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +include ../Makefile.common diff --git a/test/cbmc/proofs/stringBuilder/README.md b/test/cbmc/proofs/stringBuilder/README.md new file mode 100644 index 000000000..a3f94c8a2 --- /dev/null +++ b/test/cbmc/proofs/stringBuilder/README.md @@ -0,0 +1,20 @@ +stringBuilder proof +============== + +This directory contains a memory safety proof for stringBuilder. + +To run the proof. +------------- + +* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` + to your path. +* Run `make`. +* Open html/index.html in a web browser. + +To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +------------- + +* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. +* Use Makefile.arpa as the starting point for your proof Makefile by: + 1. Modifying Makefile.arpa (if required). + 2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`). diff --git a/test/cbmc/proofs/stringBuilder/cbmc-proof.txt b/test/cbmc/proofs/stringBuilder/cbmc-proof.txt new file mode 100644 index 000000000..6ed46f125 --- /dev/null +++ b/test/cbmc/proofs/stringBuilder/cbmc-proof.txt @@ -0,0 +1 @@ +# This file marks this directory as containing a CBMC proof. diff --git a/test/cbmc/proofs/stringBuilder/cbmc-viewer.json b/test/cbmc/proofs/stringBuilder/cbmc-viewer.json new file mode 100644 index 000000000..6348a1c4a --- /dev/null +++ b/test/cbmc/proofs/stringBuilder/cbmc-viewer.json @@ -0,0 +1,6 @@ +{ "expected-missing-functions": + [ + ], + "proof-name": "<__FUNCTION_NAME__>", + "proof-root": "<__PATH_TO_PROOF_ROOT__>" +} diff --git a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c new file mode 100644 index 000000000..56806c28a --- /dev/null +++ b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c @@ -0,0 +1,73 @@ +/* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. */ +/* SPDX-License-Identifier: Apache-2.0 */ + +/* + * Insert copyright notice + */ + +/** + * @file stringBuilder_harness.c + * @brief Implements the proof harness for stringBuilder function. + */ + +/* + * Insert project header files that + * - include the declaration of the function + * - include the types needed to declare function arguments + */ +#include "ota_mqtt_private.h" + +size_t __CPROVER_file_local_ota_mqtt_c_stringBuilder( char * pBuffer, + size_t bufferSizeBytes, + const char * strings[] ); + +void stringBuilder_harness() +{ + /* Insert argument declarations */ + char * pBuffer; + size_t bufferSizeBytes; + char ** strings; + + size_t numStrings; + size_t stringSize; + size_t i; + + /* The size of the pBuffer is always equal to the bufferSizeBytes. */ + pBuffer = ( char * ) malloc( bufferSizeBytes ); + + /* pBuffer can never be NULL since it it always initialized by a null character. */ + __CPROVER_assume( pBuffer != NULL ); + + /* The minimum and the maximum number of strings inside the numStrings is 11. */ + __CPROVER_assume( numStrings > 0 && numStrings < 13 ); + + /* Initializing an array of strings. */ + strings = ( char ** ) malloc( numStrings * sizeof( char * ) ); + + /* The strings array cannot be NULL as it is always initialized before + * passing to the function. */ + __CPROVER_assume( strings != NULL ); + + /* Assuming that the size of the strings can never be NULL. */ + __CPROVER_assume( stringSize > 0 && stringSize < 1500 ); + + for( i = 0; i < numStrings; ++i ) + { + strings[ i ] = ( char * ) malloc( stringSize ); + } + + /* Strings array is always passed with a NULL string at the end. */ + __CPROVER_assume( strings[ numStrings - 1 ] == NULL ); + + __CPROVER_file_local_ota_mqtt_c_stringBuilder( pBuffer, bufferSizeBytes, strings ); + + /* Free the allocated memory. */ + free( pBuffer ); + + for( i = 0; i < numStrings; ++i ) + { + free( strings[ i ] ); + } + + free( strings ); +} From 46208788c538cbfa9edf52e9357715017f9b49ff Mon Sep 17 00:00:00 2001 From: bujain Date: Wed, 11 Aug 2021 18:22:46 +0000 Subject: [PATCH 20/29] Updated assumptions --- .../proofs/stringBuilder/stringBuilder_harness.c | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c index 56806c28a..38a12ab69 100644 --- a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c +++ b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c @@ -17,6 +17,7 @@ */ #include "ota_mqtt_private.h" +/* Declaration of the mangled name function generated by CBMC for static functions. */ size_t __CPROVER_file_local_ota_mqtt_c_stringBuilder( char * pBuffer, size_t bufferSizeBytes, const char * strings[] ); @@ -39,27 +40,26 @@ void stringBuilder_harness() __CPROVER_assume( pBuffer != NULL ); /* The minimum and the maximum number of strings inside the numStrings is 11. */ - __CPROVER_assume( numStrings > 0 && numStrings < 13 ); + __CPROVER_assume( numStrings > 0 && numStrings < UINT32_MAX); - /* Initializing an array of strings. */ + /* Initializing an array of strings with size numStrings. */ strings = ( char ** ) malloc( numStrings * sizeof( char * ) ); /* The strings array cannot be NULL as it is always initialized before * passing to the function. */ __CPROVER_assume( strings != NULL ); - /* Assuming that the size of the strings can never be NULL. */ - __CPROVER_assume( stringSize > 0 && stringSize < 1500 ); - for( i = 0; i < numStrings; ++i ) - { + { strings[ i ] = ( char * ) malloc( stringSize ); } /* Strings array is always passed with a NULL string at the end. */ __CPROVER_assume( strings[ numStrings - 1 ] == NULL ); - __CPROVER_file_local_ota_mqtt_c_stringBuilder( pBuffer, bufferSizeBytes, strings ); + i = __CPROVER_file_local_ota_mqtt_c_stringBuilder( pBuffer, bufferSizeBytes, strings ); + + assert(i == ((numStrings - 1)*stringSize)); /* Free the allocated memory. */ free( pBuffer ); From 69d28c634bc7a1afcc619da0631fcc08aefbd508 Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 12 Aug 2021 17:12:45 +0000 Subject: [PATCH 21/29] Updated assumptions' --- test/cbmc/proofs/stringBuilder/stringBuilder_harness.c | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c index 38a12ab69..7a17c480a 100644 --- a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c +++ b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c @@ -32,8 +32,10 @@ void stringBuilder_harness() size_t numStrings; size_t stringSize; size_t i; + size_t stringLength; - /* The size of the pBuffer is always equal to the bufferSizeBytes. */ + /* The pBuffer is always statically allocated with a size greater than 0. */ + __CPROVER_assume(bufferSizeBytes > 0); pBuffer = ( char * ) malloc( bufferSizeBytes ); /* pBuffer can never be NULL since it it always initialized by a null character. */ @@ -49,7 +51,7 @@ void stringBuilder_harness() * passing to the function. */ __CPROVER_assume( strings != NULL ); - for( i = 0; i < numStrings; ++i ) + for( i = 0; i < numStrings-1; ++i ) { strings[ i ] = ( char * ) malloc( stringSize ); } @@ -57,9 +59,7 @@ void stringBuilder_harness() /* Strings array is always passed with a NULL string at the end. */ __CPROVER_assume( strings[ numStrings - 1 ] == NULL ); - i = __CPROVER_file_local_ota_mqtt_c_stringBuilder( pBuffer, bufferSizeBytes, strings ); - - assert(i == ((numStrings - 1)*stringSize)); + __CPROVER_file_local_ota_mqtt_c_stringBuilder( pBuffer, bufferSizeBytes, strings ); /* Free the allocated memory. */ free( pBuffer ); From 4013be05e29f45a878853d838c35272ed186fc95 Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 12 Aug 2021 18:29:40 +0000 Subject: [PATCH 22/29] Removed copyright notice --- .../cbmc/proofs/stringBuilder/stringBuilder_harness.c | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c index 7a17c480a..7b83bd5a4 100644 --- a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c +++ b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c @@ -1,20 +1,9 @@ /* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. */ /* SPDX-License-Identifier: Apache-2.0 */ - -/* - * Insert copyright notice - */ - /** * @file stringBuilder_harness.c * @brief Implements the proof harness for stringBuilder function. */ - -/* - * Insert project header files that - * - include the declaration of the function - * - include the types needed to declare function arguments - */ #include "ota_mqtt_private.h" /* Declaration of the mangled name function generated by CBMC for static functions. */ From e6840333f7a7b4e0e10b4c2045019675f53a19c7 Mon Sep 17 00:00:00 2001 From: Bhaumik Jain <86116186+Bujain@users.noreply.github.com> Date: Thu, 12 Aug 2021 15:12:54 -0700 Subject: [PATCH 23/29] Added CBMC proof of OTA_HTTP_strerror function (#252) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * Added new line in the end of the file * Remove whitespace * Add CBMC proof of OTA_HTTP_strerror function * Removed extra line and updated error log * Updated error log Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> --- test/cbmc/proofs/OTA_HTTP_strerror/Makefile | 25 +++++++++++ .../OTA_HTTP_strerror_harness.c | 42 +++++++++++++++++++ test/cbmc/proofs/OTA_HTTP_strerror/README.md | 20 +++++++++ .../proofs/OTA_HTTP_strerror/cbmc-proof.txt | 2 + .../proofs/OTA_HTTP_strerror/cbmc-viewer.json | 6 +++ 5 files changed, 95 insertions(+) create mode 100644 test/cbmc/proofs/OTA_HTTP_strerror/Makefile create mode 100644 test/cbmc/proofs/OTA_HTTP_strerror/OTA_HTTP_strerror_harness.c create mode 100644 test/cbmc/proofs/OTA_HTTP_strerror/README.md create mode 100644 test/cbmc/proofs/OTA_HTTP_strerror/cbmc-proof.txt create mode 100644 test/cbmc/proofs/OTA_HTTP_strerror/cbmc-viewer.json diff --git a/test/cbmc/proofs/OTA_HTTP_strerror/Makefile b/test/cbmc/proofs/OTA_HTTP_strerror/Makefile new file mode 100644 index 000000000..aff49c0af --- /dev/null +++ b/test/cbmc/proofs/OTA_HTTP_strerror/Makefile @@ -0,0 +1,25 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY = OTA_HTTP_strerror_harness +HARNESS_FILE = $(HARNESS_ENTRY) + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = OTA_HTTP_strerror + +DEFINES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/source/ota_http.c + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +include ../Makefile.common diff --git a/test/cbmc/proofs/OTA_HTTP_strerror/OTA_HTTP_strerror_harness.c b/test/cbmc/proofs/OTA_HTTP_strerror/OTA_HTTP_strerror_harness.c new file mode 100644 index 000000000..934ca48db --- /dev/null +++ b/test/cbmc/proofs/OTA_HTTP_strerror/OTA_HTTP_strerror_harness.c @@ -0,0 +1,42 @@ +/* + * AWS IoT Over-the-air Update v3.0.0 + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file OTA_HTTP_strerror_harness.c + * @brief Implements the proof harness for OTA_HTTP_strerror function. + */ + +/* http interface includes. */ +#include "ota_http_private.h" + +void OTA_HTTP_strerror_harness() +{ + OtaHttpStatus_t status; + const char * pErrorMsg = NULL; + + pErrorMsg = OTA_HTTP_strerror( status ); + + /* The function returns a string which is never a NULL. If it does, then + * there is a problem. */ + __CPROVER_assert( pErrorMsg != NULL, + "Invalid return value from OTA_MQTT_strerror: Expected a non-null value." ); +} diff --git a/test/cbmc/proofs/OTA_HTTP_strerror/README.md b/test/cbmc/proofs/OTA_HTTP_strerror/README.md new file mode 100644 index 000000000..11353c7dd --- /dev/null +++ b/test/cbmc/proofs/OTA_HTTP_strerror/README.md @@ -0,0 +1,20 @@ +OTA_HTTP_strerror proof +============== + +This directory contains a memory safety proof for OTA_HTTP_strerror. + +To run the proof. +------------- + +* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` + to your path. +* Run `make`. +* Open html/index.html in a web browser. + +To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +------------- + +* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. +* Use Makefile.arpa as the starting point for your proof Makefile by: + 1. Modifying Makefile.arpa (if required). + 2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`). diff --git a/test/cbmc/proofs/OTA_HTTP_strerror/cbmc-proof.txt b/test/cbmc/proofs/OTA_HTTP_strerror/cbmc-proof.txt new file mode 100644 index 000000000..0639406e3 --- /dev/null +++ b/test/cbmc/proofs/OTA_HTTP_strerror/cbmc-proof.txt @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# This file is required by the run-cbmc-proofs.py to differentiate between a proof directory from a normal directory. \ No newline at end of file diff --git a/test/cbmc/proofs/OTA_HTTP_strerror/cbmc-viewer.json b/test/cbmc/proofs/OTA_HTTP_strerror/cbmc-viewer.json new file mode 100644 index 000000000..0dfd56995 --- /dev/null +++ b/test/cbmc/proofs/OTA_HTTP_strerror/cbmc-viewer.json @@ -0,0 +1,6 @@ +{ "expected-missing-functions": + [ + ], + "proof-name": "OTA_HTTP_strerror", + "proof-root": "test/cbmc/proofs" +} From 08fa29e6bf8ab8ed3f47dbba6e77c897e9c67d4b Mon Sep 17 00:00:00 2001 From: Bhaumik Jain <86116186+Bujain@users.noreply.github.com> Date: Thu, 12 Aug 2021 15:13:33 -0700 Subject: [PATCH 24/29] Add CBMC proofs for RequestdataBlock_Http function (#248) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * Added new line in the end of the file * Remove whitespace * Added CBMC Proof of requestDataBlock_Http function * Removed extra line * Update Comments Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> --- .../proofs/requestDataBlock_Http/Makefile | 25 +++++++ .../proofs/requestDataBlock_Http/README.md | 20 ++++++ .../requestDataBlock_Http/cbmc-proof.txt | 2 + .../requestDataBlock_Http/cbmc-viewer.json | 6 ++ .../requestDataBlock_Http_harness.c | 68 +++++++++++++++++++ 5 files changed, 121 insertions(+) create mode 100644 test/cbmc/proofs/requestDataBlock_Http/Makefile create mode 100644 test/cbmc/proofs/requestDataBlock_Http/README.md create mode 100644 test/cbmc/proofs/requestDataBlock_Http/cbmc-proof.txt create mode 100644 test/cbmc/proofs/requestDataBlock_Http/cbmc-viewer.json create mode 100644 test/cbmc/proofs/requestDataBlock_Http/requestDataBlock_Http_harness.c diff --git a/test/cbmc/proofs/requestDataBlock_Http/Makefile b/test/cbmc/proofs/requestDataBlock_Http/Makefile new file mode 100644 index 000000000..0de3c953b --- /dev/null +++ b/test/cbmc/proofs/requestDataBlock_Http/Makefile @@ -0,0 +1,25 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY = requestDataBlock_Http_harness +HARNESS_FILE = $(HARNESS_ENTRY) + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = requestDataBlock_Http + +DEFINES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/source/ota_http.c + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +include ../Makefile.common diff --git a/test/cbmc/proofs/requestDataBlock_Http/README.md b/test/cbmc/proofs/requestDataBlock_Http/README.md new file mode 100644 index 000000000..eda7955a1 --- /dev/null +++ b/test/cbmc/proofs/requestDataBlock_Http/README.md @@ -0,0 +1,20 @@ +requestDataBlock_Http proof +============== + +This directory contains a memory safety proof for requestDataBlock_Http. + +To run the proof. +------------- + +* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` + to your path. +* Run `make`. +* Open html/index.html in a web browser. + +To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +------------- + +* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. +* Use Makefile.arpa as the starting point for your proof Makefile by: + 1. Modifying Makefile.arpa (if required). + 2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`). diff --git a/test/cbmc/proofs/requestDataBlock_Http/cbmc-proof.txt b/test/cbmc/proofs/requestDataBlock_Http/cbmc-proof.txt new file mode 100644 index 000000000..0639406e3 --- /dev/null +++ b/test/cbmc/proofs/requestDataBlock_Http/cbmc-proof.txt @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# This file is required by the run-cbmc-proofs.py to differentiate between a proof directory from a normal directory. \ No newline at end of file diff --git a/test/cbmc/proofs/requestDataBlock_Http/cbmc-viewer.json b/test/cbmc/proofs/requestDataBlock_Http/cbmc-viewer.json new file mode 100644 index 000000000..210cfadae --- /dev/null +++ b/test/cbmc/proofs/requestDataBlock_Http/cbmc-viewer.json @@ -0,0 +1,6 @@ +{ "expected-missing-functions": + [ + ], + "proof-name": "requestDataBlock_Http", + "proof-root": "/test/cbmc/proofs" +} diff --git a/test/cbmc/proofs/requestDataBlock_Http/requestDataBlock_Http_harness.c b/test/cbmc/proofs/requestDataBlock_Http/requestDataBlock_Http_harness.c new file mode 100644 index 000000000..518fb43d4 --- /dev/null +++ b/test/cbmc/proofs/requestDataBlock_Http/requestDataBlock_Http_harness.c @@ -0,0 +1,68 @@ +/* + * AWS IoT Over-the-air Update v3.0.0 + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file requestDataBlock_Http_harness.c + * @brief Implements the proof harness for requestDataBlock_Http function. + */ +/* Http interface includes. */ +#include "ota_http_private.h" + +/* Stub required for the proof. */ +OtaHttpStatus_t request( uint32_t rangeStart, + uint32_t rangeEnd ) +{ + OtaHttpStatus_t status; + + return status; +} +/*-----------------------------------------------------------*/ + +void requestDataBlock_Http_harness() +{ + OtaAgentContext_t * pAgentCtx; + OtaFileContext_t fileContext; + OtaHttpInterface_t http; + OtaInterfaces_t interface; + OtaErr_t err; + OtaAgentContext_t agent; + + pAgentCtx = &agent; + + /* Initialize the file context field in the Agent context. */ + pAgentCtx->fileContext = fileContext; + http.request = request; + interface.http = http; + + /* requestDataBlock_Http assumes that the file size is not zero. + * This is enforced by the validateAndStartJob function, which is + * always called before the requestDataBlock_Http function.*/ + __CPROVER_assume( pAgentCtx->fileContext.fileSize != 0 ); + + pAgentCtx->pOtaInterface = &interface; + + err = requestDataBlock_Http( pAgentCtx ); + + /* Assert to check if the return from the function is of expected values. */ + __CPROVER_assert( ( err == OtaErrNone ) || ( err == OtaErrRequestFileBlockFailed ), + "The function return should be either of these values" ); +} From 5a72e200726539c05627d080f0084d21332dea38 Mon Sep 17 00:00:00 2001 From: Bhaumik Jain <86116186+Bujain@users.noreply.github.com> Date: Thu, 12 Aug 2021 15:13:52 -0700 Subject: [PATCH 25/29] Added CBMC proofs for OTA_MQTT_strerror function (#247) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for OTA_MQTT_strerror function * Removed extra line * Updated comments * Fixed formatting errors * Updated error log Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> --- test/cbmc/proofs/OTA_MQTT_strerror/Makefile | 25 ++++++++++++ .../OTA_MQTT_strerror_harness.c | 40 +++++++++++++++++++ test/cbmc/proofs/OTA_MQTT_strerror/README.md | 20 ++++++++++ .../proofs/OTA_MQTT_strerror/cbmc-proof.txt | 2 + .../proofs/OTA_MQTT_strerror/cbmc-viewer.json | 6 +++ 5 files changed, 93 insertions(+) create mode 100644 test/cbmc/proofs/OTA_MQTT_strerror/Makefile create mode 100644 test/cbmc/proofs/OTA_MQTT_strerror/OTA_MQTT_strerror_harness.c create mode 100644 test/cbmc/proofs/OTA_MQTT_strerror/README.md create mode 100644 test/cbmc/proofs/OTA_MQTT_strerror/cbmc-proof.txt create mode 100644 test/cbmc/proofs/OTA_MQTT_strerror/cbmc-viewer.json diff --git a/test/cbmc/proofs/OTA_MQTT_strerror/Makefile b/test/cbmc/proofs/OTA_MQTT_strerror/Makefile new file mode 100644 index 000000000..8abf00d15 --- /dev/null +++ b/test/cbmc/proofs/OTA_MQTT_strerror/Makefile @@ -0,0 +1,25 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY = OTA_MQTT_strerror_harness +HARNESS_FILE = $(HARNESS_ENTRY) + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = OTA_MQTT_strerror + +DEFINES += + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/source/ota_mqtt.c + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +include ../Makefile.common diff --git a/test/cbmc/proofs/OTA_MQTT_strerror/OTA_MQTT_strerror_harness.c b/test/cbmc/proofs/OTA_MQTT_strerror/OTA_MQTT_strerror_harness.c new file mode 100644 index 000000000..19e0091e5 --- /dev/null +++ b/test/cbmc/proofs/OTA_MQTT_strerror/OTA_MQTT_strerror_harness.c @@ -0,0 +1,40 @@ +/* + * AWS IoT Over-the-air Update v3.0.0 + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file OTA_MQTT_strerror_harness.c + * @brief Implements the proof harness for OTA_MQTT_strerror function. + */ + +#include "ota_mqtt_private.h" + +void OTA_MQTT_strerror_harness() +{ + OtaMqttStatus_t status; + const char * pErrorMsg; + + pErrorMsg = OTA_MQTT_strerror( status ); + + /* The caller of this function assumes that the return value is never NULL. */ + __CPROVER_assert( pErrorMsg != NULL, + "Invalid return value from OTA_MQTT_strerror: Expected a non-null value." ); +} diff --git a/test/cbmc/proofs/OTA_MQTT_strerror/README.md b/test/cbmc/proofs/OTA_MQTT_strerror/README.md new file mode 100644 index 000000000..fcbe70d66 --- /dev/null +++ b/test/cbmc/proofs/OTA_MQTT_strerror/README.md @@ -0,0 +1,20 @@ +OTA_MQTT_strerror proof +============== + +This directory contains a memory safety proof for OTA_MQTT_strerror. + +To run the proof. +------------- + +* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` + to your path. +* Run `make`. +* Open html/index.html in a web browser. + +To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +------------- + +* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. +* Use Makefile.arpa as the starting point for your proof Makefile by: + 1. Modifying Makefile.arpa (if required). + 2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`). diff --git a/test/cbmc/proofs/OTA_MQTT_strerror/cbmc-proof.txt b/test/cbmc/proofs/OTA_MQTT_strerror/cbmc-proof.txt new file mode 100644 index 000000000..0639406e3 --- /dev/null +++ b/test/cbmc/proofs/OTA_MQTT_strerror/cbmc-proof.txt @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# This file is required by the run-cbmc-proofs.py to differentiate between a proof directory from a normal directory. \ No newline at end of file diff --git a/test/cbmc/proofs/OTA_MQTT_strerror/cbmc-viewer.json b/test/cbmc/proofs/OTA_MQTT_strerror/cbmc-viewer.json new file mode 100644 index 000000000..50ad7ff38 --- /dev/null +++ b/test/cbmc/proofs/OTA_MQTT_strerror/cbmc-viewer.json @@ -0,0 +1,6 @@ +{ "expected-missing-functions": + [ + ], + "proof-name": "OTA_MQTT_strerror", + "proof-root": "test/cbmc/proofs" +} From d470ee5ea7b682ea7ecca2dcbae217bdf2d7bfc9 Mon Sep 17 00:00:00 2001 From: Bhaumik Jain <86116186+Bujain@users.noreply.github.com> Date: Thu, 12 Aug 2021 16:49:58 -0700 Subject: [PATCH 26/29] Added CBMC proofs for setControlInterface function (#246) * Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for setControlInterface function * Removed extra line * Added macro for the function * Fix formating errors * Fix spell check errors * Added preprocessor definition for setControlInterface function Co-authored-by: Aniruddha Kanhere <60444055+AniruddhaKanhere@users.noreply.github.com> --- test/cbmc/proofs/setControlInterface/Makefile | 25 ++++++++++++ .../cbmc/proofs/setControlInterface/README.md | 20 ++++++++++ .../proofs/setControlInterface/cbmc-proof.txt | 2 + .../setControlInterface/cbmc-viewer.json | 6 +++ .../setControlInterface_harness.c | 40 +++++++++++++++++++ 5 files changed, 93 insertions(+) create mode 100644 test/cbmc/proofs/setControlInterface/Makefile create mode 100644 test/cbmc/proofs/setControlInterface/README.md create mode 100644 test/cbmc/proofs/setControlInterface/cbmc-proof.txt create mode 100644 test/cbmc/proofs/setControlInterface/cbmc-viewer.json create mode 100644 test/cbmc/proofs/setControlInterface/setControlInterface_harness.c diff --git a/test/cbmc/proofs/setControlInterface/Makefile b/test/cbmc/proofs/setControlInterface/Makefile new file mode 100644 index 000000000..9ce489c4c --- /dev/null +++ b/test/cbmc/proofs/setControlInterface/Makefile @@ -0,0 +1,25 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +HARNESS_ENTRY = setControlInterface_harness +HARNESS_FILE = $(HARNESS_ENTRY) + +# This should be a unique identifier for this proof, and will appear on the +# Litani dashboard. It can be human-readable and contain spaces if you wish. +PROOF_UID = setControlInterface + +DEFINES += -DconfigENABLED_CONTROL_PROTOCOL=OTA_CONTROL_OVER_MQTT + +REMOVE_FUNCTION_BODY += +UNWINDSET += + +PROOF_SOURCES += $(PROOFDIR)/$(HARNESS_FILE).c +PROJECT_SOURCES += $(SRCDIR)/source/ota_interface.c + +# If this proof is found to consume huge amounts of RAM, you can set the +# EXPENSIVE variable. With new enough versions of the proof tools, this will +# restrict the number of EXPENSIVE CBMC jobs running at once. See the +# documentation in Makefile.common under the "Job Pools" heading for details. +# EXPENSIVE = true + +include ../Makefile.common diff --git a/test/cbmc/proofs/setControlInterface/README.md b/test/cbmc/proofs/setControlInterface/README.md new file mode 100644 index 000000000..367930992 --- /dev/null +++ b/test/cbmc/proofs/setControlInterface/README.md @@ -0,0 +1,20 @@ +setControlInterface proof +============== + +This directory contains a memory safety proof for setControlInterface. + +To run the proof. +------------- + +* Add `cbmc`, `goto-cc`, `goto-instrument`, `goto-analyzer`, and `cbmc-viewer` + to your path. +* Run `make`. +* Open html/index.html in a web browser. + +To use [`arpa`](https://github.com/awslabs/aws-proof-build-assistant) to simplify writing Makefiles. +------------- + +* Run `make arpa` to generate a Makefile.arpa that contains relevant build information for the proof. +* Use Makefile.arpa as the starting point for your proof Makefile by: + 1. Modifying Makefile.arpa (if required). + 2. Including Makefile.arpa into the existing proof Makefile (add `sinclude Makefile.arpa` at the bottom of the Makefile, right before `include ../Makefile.common`). diff --git a/test/cbmc/proofs/setControlInterface/cbmc-proof.txt b/test/cbmc/proofs/setControlInterface/cbmc-proof.txt new file mode 100644 index 000000000..0639406e3 --- /dev/null +++ b/test/cbmc/proofs/setControlInterface/cbmc-proof.txt @@ -0,0 +1,2 @@ +# This file marks this directory as containing a CBMC proof. +# This file is required by the run-cbmc-proofs.py to differentiate between a proof directory from a normal directory. \ No newline at end of file diff --git a/test/cbmc/proofs/setControlInterface/cbmc-viewer.json b/test/cbmc/proofs/setControlInterface/cbmc-viewer.json new file mode 100644 index 000000000..79cbe01eb --- /dev/null +++ b/test/cbmc/proofs/setControlInterface/cbmc-viewer.json @@ -0,0 +1,6 @@ +{ "expected-missing-functions": + [ + ], + "proof-name": "setControlInterface", + "proof-root": "test/cbmc/proofs" +} diff --git a/test/cbmc/proofs/setControlInterface/setControlInterface_harness.c b/test/cbmc/proofs/setControlInterface/setControlInterface_harness.c new file mode 100644 index 000000000..bffc7d476 --- /dev/null +++ b/test/cbmc/proofs/setControlInterface/setControlInterface_harness.c @@ -0,0 +1,40 @@ +/* + * AWS IoT Over-the-air Update v3.0.0 + * Copyright (C) 2020 Amazon.com, Inc. or its affiliates. All Rights Reserved. + * + * Permission is hereby granted, free of charge, to any person obtaining a copy of + * this software and associated documentation files (the "Software"), to deal in + * the Software without restriction, including without limitation the rights to + * use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of + * the Software, and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be included in all + * copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS + * FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR + * COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER + * IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +/** + * @file setControlInterface_harness.c + * @brief Implements the proof harness for setControlInterface function. + */ +/* Ota interface includes. */ +#include "ota_interface_private.h" + +void setControlInterface_harness() +{ + OtaControlInterface_t * pControlInterface; + OtaControlInterface_t controlInterface; + + /* Initialize the control interface. The control interface can never + * be NULL as it is declared statically in ota.c source file. */ + pControlInterface = &controlInterface; + + setControlInterface( pControlInterface ); +} From a44ccc8c39eda58c685e82b2b0df805c595cc5c9 Mon Sep 17 00:00:00 2001 From: bujain Date: Tue, 17 Aug 2021 16:51:38 +0000 Subject: [PATCH 27/29] Updated comments --- test/cbmc/proofs/stringBuilder/stringBuilder_harness.c | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c index 7b83bd5a4..5d81f4ef0 100644 --- a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c +++ b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c @@ -13,7 +13,6 @@ size_t __CPROVER_file_local_ota_mqtt_c_stringBuilder( char * pBuffer, void stringBuilder_harness() { - /* Insert argument declarations */ char * pBuffer; size_t bufferSizeBytes; char ** strings; @@ -23,11 +22,11 @@ void stringBuilder_harness() size_t i; size_t stringLength; - /* The pBuffer is always statically allocated with a size greater than 0. */ + /* The pBuffer is statically allocated with a non-zero size before passing it to the stringBuilder function.*/ __CPROVER_assume(bufferSizeBytes > 0); pBuffer = ( char * ) malloc( bufferSizeBytes ); - /* pBuffer can never be NULL since it it always initialized by a null character. */ + /* pBuffer can never be NULL since it it always initialized before passing it to the stringBuilder function. */ __CPROVER_assume( pBuffer != NULL ); /* The minimum and the maximum number of strings inside the numStrings is 11. */ From 27b1a186e358ebdfd4bb1e0b34251cc4e4fccfc9 Mon Sep 17 00:00:00 2001 From: bujain Date: Tue, 17 Aug 2021 19:25:02 +0000 Subject: [PATCH 28/29] Fix spell check and formatting errors --- .../cbmc/proofs/stringBuilder/stringBuilder_harness.c | 11 ++++++----- tools/lexicon.txt | 2 ++ 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c index 5d81f4ef0..696e52ee8 100644 --- a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c +++ b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c @@ -1,5 +1,6 @@ /* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. */ /* SPDX-License-Identifier: Apache-2.0 */ + /** * @file stringBuilder_harness.c * @brief Implements the proof harness for stringBuilder function. @@ -23,14 +24,14 @@ void stringBuilder_harness() size_t stringLength; /* The pBuffer is statically allocated with a non-zero size before passing it to the stringBuilder function.*/ - __CPROVER_assume(bufferSizeBytes > 0); + __CPROVER_assume( bufferSizeBytes > 0 ); pBuffer = ( char * ) malloc( bufferSizeBytes ); /* pBuffer can never be NULL since it it always initialized before passing it to the stringBuilder function. */ __CPROVER_assume( pBuffer != NULL ); /* The minimum and the maximum number of strings inside the numStrings is 11. */ - __CPROVER_assume( numStrings > 0 && numStrings < UINT32_MAX); + __CPROVER_assume( numStrings > 0 && numStrings < UINT32_MAX ); /* Initializing an array of strings with size numStrings. */ strings = ( char ** ) malloc( numStrings * sizeof( char * ) ); @@ -38,9 +39,9 @@ void stringBuilder_harness() /* The strings array cannot be NULL as it is always initialized before * passing to the function. */ __CPROVER_assume( strings != NULL ); - - for( i = 0; i < numStrings-1; ++i ) - { + + for( i = 0; i < numStrings - 1; ++i ) + { strings[ i ] = ( char * ) malloc( stringSize ); } diff --git a/tools/lexicon.txt b/tools/lexicon.txt index c9252ccc3..1310d64c4 100644 --- a/tools/lexicon.txt +++ b/tools/lexicon.txt @@ -328,6 +328,7 @@ numjobparams nummodelparams numofblocksrequested numofblockstoreceive +numstrings ok onlinepubs opengroup @@ -739,6 +740,7 @@ streamname streamnamemaxsize streamnamesize strerror +stringbuilder strlength struct structs From 6d32385055214106c6e4d89e2542e8edecd3d153 Mon Sep 17 00:00:00 2001 From: bujain Date: Thu, 2 Sep 2021 17:29:27 +0000 Subject: [PATCH 29/29] Added null terminator to every string --- .../proofs/stringBuilder/stringBuilder_harness.c | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c index 696e52ee8..1520e5dff 100644 --- a/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c +++ b/test/cbmc/proofs/stringBuilder/stringBuilder_harness.c @@ -30,12 +30,16 @@ void stringBuilder_harness() /* pBuffer can never be NULL since it it always initialized before passing it to the stringBuilder function. */ __CPROVER_assume( pBuffer != NULL ); - /* The minimum and the maximum number of strings inside the numStrings is 11. */ + /* The minimum and the maximum number of strings inside the numStrings are 0 and 11. */ __CPROVER_assume( numStrings > 0 && numStrings < UINT32_MAX ); /* Initializing an array of strings with size numStrings. */ strings = ( char ** ) malloc( numStrings * sizeof( char * ) ); + /* The size of each string inside the strings array passed to the stringBuilder + * function is greater than 0. */ + __CPROVER_assume( stringSize > 0 ); + /* The strings array cannot be NULL as it is always initialized before * passing to the function. */ __CPROVER_assume( strings != NULL ); @@ -43,6 +47,11 @@ void stringBuilder_harness() for( i = 0; i < numStrings - 1; ++i ) { strings[ i ] = ( char * ) malloc( stringSize ); + + /* The strings inside the strings array are defined before passing it to + * the stringBuilder function. */ + __CPROVER_assume( strings[ i ] != NULL ); + strings[ i ][ stringSize - 1 ] = '\0'; } /* Strings array is always passed with a NULL string at the end. */ @@ -53,7 +62,7 @@ void stringBuilder_harness() /* Free the allocated memory. */ free( pBuffer ); - for( i = 0; i < numStrings; ++i ) + for( i = 0; i < numStrings - 1; ++i ) { free( strings[ i ] ); }