From dc45d0c9cb7d5968795167f55ac556c07722c496 Mon Sep 17 00:00:00 2001 From: Angelo Nakos Date: Wed, 13 Jul 2022 12:29:14 -0400 Subject: [PATCH] Update files related to CBMC starter kit --- test/cbmc/include/README.md | 7 +- test/cbmc/proofs/Makefile.common | 1000 ++++++++++++++++++++++++++- test/cbmc/proofs/README.md | 28 +- test/cbmc/proofs/lib/__init__.py | 0 test/cbmc/proofs/lib/summarize.py | 92 +++ test/cbmc/proofs/run-cbmc-proofs.py | 415 ++++++++++- test/cbmc/sources/README.md | 7 +- test/cbmc/stubs/README.md | 7 +- 8 files changed, 1550 insertions(+), 6 deletions(-) mode change 120000 => 100644 test/cbmc/include/README.md mode change 120000 => 100644 test/cbmc/proofs/Makefile.common mode change 120000 => 100644 test/cbmc/proofs/README.md create mode 100644 test/cbmc/proofs/lib/__init__.py create mode 100644 test/cbmc/proofs/lib/summarize.py mode change 120000 => 100755 test/cbmc/proofs/run-cbmc-proofs.py mode change 120000 => 100644 test/cbmc/sources/README.md mode change 120000 => 100644 test/cbmc/stubs/README.md diff --git a/test/cbmc/include/README.md b/test/cbmc/include/README.md deleted file mode 120000 index 4086b9eb8..000000000 --- a/test/cbmc/include/README.md +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/include/README.md \ No newline at end of file diff --git a/test/cbmc/include/README.md b/test/cbmc/include/README.md new file mode 100644 index 000000000..36bdd94e6 --- /dev/null +++ b/test/cbmc/include/README.md @@ -0,0 +1,6 @@ +CBMC proof include files +======================== + +This directory contains include files written for CBMC proof. It is +common to write some code to model aspects of the system under test, +and the header files for this code go here. diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common deleted file mode 120000 index 69d247eb6..000000000 --- a/test/cbmc/proofs/Makefile.common +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/proofs/Makefile.common \ No newline at end of file diff --git a/test/cbmc/proofs/Makefile.common b/test/cbmc/proofs/Makefile.common new file mode 100644 index 000000000..1c05c2ef4 --- /dev/null +++ b/test/cbmc/proofs/Makefile.common @@ -0,0 +1,999 @@ +# -*- mode: makefile -*- +# The first line sets the emacs major mode to Makefile + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: MIT-0 + +CBMC_STARTER_KIT_VERSION = CBMC starter kit 2.5 + +################################################################ +# The CBMC Starter Kit depends on the files Makefile.common and +# run-cbmc-proofs.py. They are installed by the setup script +# cbmc-starter-kit-setup and updated to the latest version by the +# update script cbmc-starter-kit-update. For more information about +# the starter kit and these files and these scripts, see +# https://model-checking.github.io/cbmc-starter-kit +# +# Makefile.common implements what we consider to be some best +# practices for using cbmc for software verification. +# +# Section I gives default values for a large number of Makefile +# variables that control +# * how your code is built (include paths, etc), +# * what program transformations are applied to your code (loop +# unwinding, etc), and +# * what properties cbmc checks for in your code (memory safety, etc). +# +# These variables are defined below with definitions of the form +# VARIABLE ?= DEFAULT_VALUE +# meaning VARIABLE is set to DEFAULT_VALUE if VARIABLE has not already +# been given a value. +# +# For your project, you can override these default values with +# project-specific definitions in Makefile-project-defines. +# +# For any individual proof, you can override these default values and +# project-specific values with proof-specific definitions in the +# Makefile for your proof. +# +# The definitions in the proof Makefile override definitions in the +# project Makefile-project-defines which override definitions in this +# Makefile.common. +# +# Section II uses the values defined in Section I to build your code, run +# your proof, and build a report of your results. You should not need +# to modify or override anything in Section II, but you may want to +# read it to understand how the values defined in Section I control +# things. +# +# To use Makefile.common, set variables as described above as needed, +# and then for each proof, +# +# * Create a subdirectory . +# * Write a proof harness (a function) with the name +# in a file with the name /.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 +# +# * Change directory to and run make +# +# The proof setup script cbmc-starter-kit-setup-proof from the CBMC +# Starter Kit will do most of this for, creating a directory and +# writing a basic Makefile and proof harness into it that you can edit +# as described above. +# +# Warning: If you get results that are hard to explain, consider +# running "make clean" or "make veryclean" before "make" if you get +# results that are hard to explain. Dependency handling in this +# Makefile.common may not be perfect. + +SHELL=/bin/bash + +default: report + +################################################################ +################################################################ +## Section I: This section gives common variable definitions. +## +## Override these definitions in Makefile-project-defines or +## your proof Makefile. +## +## Remember that Makefile.common and Makefile-project-defines are +## included into the proof Makefile in your proof directory, so all +## relative pathnames defined there should be relative to your proof +## directory. + +################################################################ +# Define the layout of the source tree and the proof subtree +# +# Generally speaking, +# +# SRCDIR = the root of the repository +# CBMC_ROOT = /srcdir/cbmc +# PROOF_ROOT = /srcdir/cbmc/proofs +# PROOF_SOURCE = /srcdir/cbmc/sources +# PROOF_INCLUDE = /srcdir/cbmc/include +# PROOF_STUB = /srcdir/cbmc/stubs +# PROOFDIR = the directory containing the Makefile for your proof +# +# The path /srcdir/cbmc used in the example above is determined by the +# setup script cbmc-starter-kit-setup. Projects usually create a cbmc +# directory somewhere in the source tree, and run the setup script in +# that directory. The value of CBMC_ROOT becomes the absolute path to +# that directory. +# +# The location of that cbmc directory in the source tree affects the +# definition of SRCDIR, which is defined in terms of the relative path +# from a proof directory to the repository root. The definition is +# usually determined by the setup script cbmc-starter-kit-setup and +# written to Makefile-template-defines, but you can override it for a +# project in Makefile-project-defines and for a specific proof in the +# Makefile for the proof. + +# 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_SOURCE = $(CBMC_ROOT)/sources +PROOF_INCLUDE = $(CBMC_ROOT)/include +PROOF_STUB = $(CBMC_ROOT)/stubs + +# Project-specific definitions to override default definitions below +# * Makefile-project-defines will never be overwritten +# * Makefile-template-defines may be overwritten when the starter +# kit is updated +sinclude $(PROOF_ROOT)/Makefile-project-defines +sinclude $(PROOF_ROOT)/Makefile-template-defines + +# SRCDIR is the path to the root of the source tree +# This is a default definition that is frequently overridden in +# another Makefile, see the discussion of SRCDIR above. +SRCDIR ?= $(abspath ../..) + +# PROOFDIR is the path to the directory containing the proof harness +PROOFDIR ?= $(abspath .) + +################################################################ +# Define how to run CBMC + +# 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_FLAG_UNWIND ?= --unwind 1 +CBMC_FLAG_FLUSH ?= --flush + +# CBMC flags used for property checking and coverage checking + +CBMCFLAGS += $(CBMC_FLAG_UNWIND) $(CBMC_UNWINDSET) $(CBMC_FLAG_FLUSH) + +# 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 ?= -Wall +LINK_FLAGS ?= -Wall +EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols + +# 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 early loop unwinding (Normally set in the proof Makefile) +# +# Most users can ignore this variable. +# +# This variable exists to support the use of loop and function +# contracts, two features under development for CBMC. Checking the +# assigns clause for function contracts and loop invariants currently +# assumes loop-free bodies for loops and functions with contracts +# (possibly after replacing nested loops with their own loop +# contracts). To satisfy this requirement, it may be necessary to +# unwind some loops before the function contract and loop invariant +# transformations are applied to the goto program. This variable +# EARLY_UNWINDSET is identical to UNWINDSET, and we assume that the +# loops mentioned in EARLY_UNWINDSET and UNWINDSET are disjoint. +EARLY_UNWINDSET ?= + +# 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 ?= + +# CBMC function pointer restriction (Normally set in the proof Makefile) +# +# RESTRICT_FUNCTION_POINTER is a list of function pointer restriction +# instructions of the form: +# +# .function_pointer_call./[,]* +# +# The function pointer call number in the specified function gets +# rewritten to a case switch over a finite list of functions. +# If some possible target functions are omitted from the list a counter +# example trace will be found by CBMC, i.e. the transformation is sound. +# If the target functions are file-local symbols, then mangled names must +# be used. +RESTRICT_FUNCTION_POINTER ?= + +# 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 +ifeq ($(APPLY_LOOP_CONTRACTS),1) + CBMC_APPLY_LOOP_CONTRACTS ?= --apply-loop-contracts +endif + +# Silence makefile output (eg, long litani commands) unless VERBOSE is set. +ifndef VERBOSE + MAKEFLAGS := $(MAKEFLAGS) -s +endif + +################################################################ +################################################################ +## 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 +CRANGLER ?= crangler +VIEWER ?= cbmc-viewer +MAKE_SOURCE ?= make-source +VIEWER2 ?= cbmc-viewer +CMAKE ?= cmake + +GOTODIR ?= $(PROOFDIR)/gotos +LOGDIR ?= $(PROOFDIR)/logs + +PROJECT ?= project +PROOF ?= proof + +HARNESS_GOTO ?= $(GOTODIR)/$(HARNESS_FILE) +PROJECT_GOTO ?= $(GOTODIR)/$(PROJECT) +PROOF_GOTO ?= $(GOTODIR)/$(PROOF) + +################################################################ +# Useful macros for values that are hard to reference +SPACE :=$() $() +COMMA :=, + +################################################################ +# Set C compiler defines + +CBMCFLAGS += --object-bits $(CBMC_OBJECT_BITS) +COMPILE_FLAGS += --object-bits $(CBMC_OBJECT_BITS) + +DEFINES += -DCBMC=1 +DEFINES += -DCBMC_OBJECT_BITS=$(CBMC_OBJECT_BITS) +DEFINES += -DCBMC_MAX_OBJECT_SIZE="(SIZE_MAX>>(CBMC_OBJECT_BITS+1))" + +# CI currently assumes cbmc invocation has at most one --unwindset +ifdef UNWINDSET + ifneq ($(strip $(UNWINDSET)),"") + CBMC_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(UNWINDSET))) + endif +endif +ifdef EARLY_UNWINDSET + ifneq ($(strip $(EARLY_UNWINDSET)),"") + CBMC_EARLY_UNWINDSET := --unwindset $(subst $(SPACE),$(COMMA),$(strip $(EARLY_UNWINDSET))) + endif +endif + +CBMC_REMOVE_FUNCTION_BODY := $(patsubst %,--remove-function-body %, $(REMOVE_FUNCTION_BODY)) +CBMC_RESTRICT_FUNCTION_POINTER := $(patsubst %,--restrict-function-pointer %, $(RESTRICT_FUNCTION_POINTER)) + +################################################################ +# Targets for rewriting source files with crangler + +# Construct crangler configuration files +# +# REWRITTEN_SOURCES is a list of crangler output files source.i. +# This target assumes that for each source.i +# * source.i_SOURCE is the path to a source file, +# * source.i_FUNCTIONS is a list of functions (may be empty) +# * source.i_OBJECTS is a list of variables (may be empty) +# This target constructs the crangler configuration file source.i.json +# of the form +# { +# "sources": [ "/proj/code.c" ], +# "includes": [ "/proj/include" ], +# "defines": [ "VAR=1" ], +# "functions": [ {"function_name": ["remove static"]} ], +# "objects": [ {"variable_name": ["remove static"]} ], +# "output": "source.i" +# } +# to remove the static attribute from function_name and variable_name +# in the source file source.c and write the result to source.i. +# +# This target assumes that filenames include no spaces and that +# the INCLUDES and DEFINES variables include no spaces after -I +# and -D. For example, use "-DVAR=1" and not "-D VAR=1". +# +# Define *_SOURCE, *_FUNCTIONS, and *_OBJECTS in the proof Makefile. +# The string source.i is usually an absolute path $(PROOFDIR)/code.i +# to a file in the proof directory that contains the proof Makefile. +# The proof Makefile usually includes the definitions +# $(PROOFDIR)/code.i_SOURCE = /proj/code.c +# $(PROOFDIR)/code.i_FUNCTIONS = function_name +# $(PROOFDIR)/code.i_OBJECTS = variable_name +# Because these definitions refer to PROOFDIR that is defined in this +# Makefile.common, these definitions must appear after the inclusion +# of Makefile.common in the proof Makefile. +# +$(foreach rs,$(REWRITTEN_SOURCES),$(eval $(rs).json: $($(rs)_SOURCE))) +$(foreach rs,$(REWRITTEN_SOURCES),$(rs).json): + echo '{'\ + '"sources": ['\ + '"$($(@:.json=)_SOURCE)"'\ + '],'\ + '"includes": ['\ + '$(subst $(SPACE),$(COMMA),$(patsubst -I%,"%",$(strip $(INCLUDES))))' \ + '],'\ + '"defines": ['\ + '$(subst $(SPACE),$(COMMA),$(patsubst -D%,"%",$(subst ",\",$(strip $(DEFINES)))))' \ + '],'\ + '"functions": ['\ + '{'\ + '$(subst ~, ,$(subst $(SPACE),$(COMMA),$(patsubst %,"%":["remove~static"],$($(@:.json=)_FUNCTIONS))))' \ + '}'\ + '],'\ + '"objects": ['\ + '{'\ + '$(subst ~, ,$(subst $(SPACE),$(COMMA),$(patsubst %,"%":["remove~static"],$($(@:.json=)_OBJECTS))))' \ + '}'\ + '],'\ + '"output": "$(@:.json=)"'\ + '}' > $@ + +# Rewrite source files with crangler +# +$(foreach rs,$(REWRITTEN_SOURCES),$(eval $(rs): $(rs).json)) +$(REWRITTEN_SOURCES): + $(LITANI) add-job \ + --command \ + '$(CRANGLER) $@.json' \ + --inputs $($@_SOURCE) \ + --outputs $@ \ + --stdout-file $(LOGDIR)/crangler-$(subst /,_,$(subst .,_,$@))-log.txt \ + --interleave-stdout-stderr \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): removing static" + +################################################################ +# Build targets that make the relevant .goto files + +# Compile project sources +$(PROJECT_GOTO)1.goto: $(PROJECT_SOURCES) $(REWRITTEN_SOURCES) + $(LITANI) add-job \ + --command \ + '$(GOTO_CC) $(CBMC_VERBOSITY) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/project_sources-log.txt \ + --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) $(COMPILE_FLAGS) $(EXPORT_FILE_LOCAL_SYMBOLS) $(INCLUDES) $(DEFINES) $^ -o $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/proof_sources-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): building proof binary" + +# Remove function bodies from project sources +$(PROJECT_GOTO)2.goto: $(PROJECT_GOTO)1.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_REMOVE_FUNCTION_BODY) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/remove_function_body-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): removing function bodies from project sources" + +# Link project and proof sources into the proof harness +$(HARNESS_GOTO)1.goto: $(PROOF_GOTO)1.goto $(PROJECT_GOTO)2.goto + $(LITANI) add-job \ + --command '$(GOTO_CC) $(CBMC_VERBOSITY) --function $(HARNESS_ENTRY) $^ $(LINK_FLAGS) -o $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/link_proof_project-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): linking project to proof" + +# Restrict function pointers +$(HARNESS_GOTO)2.goto: $(HARNESS_GOTO)1.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_RESTRICT_FUNCTION_POINTER) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/restrict_function_pointer-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): restricting function pointers in project sources" + +# Fill static variable with unconstrained values +$(HARNESS_GOTO)3.goto: $(HARNESS_GOTO)2.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(NONDET_STATIC) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/nondet_static-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): setting static variables to nondet" + +# Omit unused functions (sharpens coverage calculations) +$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --drop-unused-functions $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/drop_unused_functions-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): dropping unused functions" + +# Omit initialization of unused global variables (reduces problem size) +$(HARNESS_GOTO)5.goto: $(HARNESS_GOTO)4.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) --slice-global-inits $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/slice_global_inits-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): slicing global initializations" + +# Replace function calls with function contracts +# This must be done before enforcing function contracts, +# since contract enforcement inlines all function calls. +$(HARNESS_GOTO)6.goto: $(HARNESS_GOTO)5.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_USE_FUNCTION_CONTRACTS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/use_function_contracts-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): replacing function calls with function contracts" + +# Unwind loops for loop and function contracts +$(HARNESS_GOTO)7.goto: $(HARNESS_GOTO)6.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_EARLY_UNWINDSET) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/unwind_loops-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): unwinding loops" + +# Apply loop contracts +$(HARNESS_GOTO)8.goto: $(HARNESS_GOTO)7.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_APPLY_LOOP_CONTRACTS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/apply_loop_contracts-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): applying loop contracts" + +# Check function contracts +$(HARNESS_GOTO)9.goto: $(HARNESS_GOTO)8.goto + $(LITANI) add-job \ + --command \ + '$(GOTO_INSTRUMENT) $(CBMC_VERBOSITY) $(CBMC_CHECK_FUNCTION_CONTRACTS) $^ $@' \ + --inputs $^ \ + --outputs $@ \ + --stdout-file $(LOGDIR)/check_function_contracts-log.txt \ + --pipeline-name "$(PROOF_UID)" \ + --ci-stage build \ + --description "$(PROOF_UID): checking function contracts" + +# Final name for proof harness +$(HARNESS_GOTO).goto: $(HARNESS_GOTO)9.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 the analysis commands + +$(LOGDIR)/result.txt: $(HARNESS_GOTO).goto + $(LITANI) add-job \ + $(POOL) \ + --command \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(CHECKFLAGS) --trace $<' \ + --inputs $^ \ + --outputs $@ \ + --ci-stage test \ + --stdout-file $@ \ + $(MEMORY_PROFILING) \ + --ignore-returns 10 \ + --timeout $(CBMC_TIMEOUT) \ + --pipeline-name "$(PROOF_UID)" \ + --tags "stats-group:safety checks" \ + --stderr-file $(LOGDIR)/result-err-log.txt \ + --description "$(PROOF_UID): checking safety properties" + +$(LOGDIR)/result.xml: $(HARNESS_GOTO).goto + $(LITANI) add-job \ + $(POOL) \ + --command \ + '$(CBMC) $(CBMC_VERBOSITY) $(CBMCFLAGS) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(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) $(CBMC_FLAG_UNWINDING_ASSERTIONS) $(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 \ + --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 \ + --config $(PROOFDIR)/cbmc-viewer.json +endef +export VIEWER2_CMD + +# Omit logs/source.json from report generation until make-sources +# works correctly with Makefiles that invoke the compiler with +# mutliple source files at once. +$(PROOFDIR)/report: $(LOGDIR)/result.xml $(LOGDIR)/property.xml $(LOGDIR)/coverage.xml + $(LITANI) add-job \ + --command "$$VIEWER2_CMD" \ + --inputs $^ \ + --outputs $(PROOFDIR)/report \ + --pipeline-name "$(PROOF_UID)" \ + --stdout-file $(LOGDIR)/viewer-log.txt \ + --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: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _goto + @ echo Running 'litani build' + $(LITANI) run-build + +_result: $(LOGDIR)/result.txt +result: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _result + @ echo Running 'litani build' + $(LITANI) run-build + +_property: $(LOGDIR)/property.xml +property: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _property + @ echo Running 'litani build' + $(LITANI) run-build + +_coverage: $(LOGDIR)/coverage.xml +coverage: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _coverage + @ echo Running 'litani build' + $(LITANI) run-build + +# Choose the invocation of cbmc-viewer depending on which version of +# cbmc-viewer is installed. The --version flag is not implemented in +# version 1 --- it is an "unrecognized argument" --- but it is +# implemented in version 2. +_report1: $(PROOFDIR)/html +_report2: $(PROOFDIR)/report +_report: + (cbmc-viewer --version 2>&1 | grep "unrecognized argument" > /dev/null) && \ + $(MAKE) -B _report1 || $(MAKE) -B _report2 + +report report1 report2: + @ echo Running 'litani init' + $(LITANI) init --project $(PROJECT_NAME) + @ echo Running 'litani add-job' + $(MAKE) -B _report + @ echo Running 'litani build' + $(LITANI) run-build + +################################################################ +# Targets to clean up after ourselves +clean: + -$(RM) $(DEPENDENT_GOTOS) + -$(RM) TAGS* + -$(RM) *~ \#* + -$(RM) $(REWRITTEN_SOURCES) $(foreach rs,$(REWRITTEN_SOURCES),$(rs).json) + +veryclean: clean + -$(RM) -r html report + -$(RM) -r $(LOGDIR) $(GOTODIR) + +.PHONY: \ + _coverage \ + _goto \ + _property \ + _report \ + _report2 \ + _result \ + 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 deleted file mode 120000 index cac5275bf..000000000 --- a/test/cbmc/proofs/README.md +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/proofs/README.md \ No newline at end of file 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/lib/__init__.py b/test/cbmc/proofs/lib/__init__.py new file mode 100644 index 000000000..e69de29bb diff --git a/test/cbmc/proofs/lib/summarize.py b/test/cbmc/proofs/lib/summarize.py new file mode 100644 index 000000000..154634b4e --- /dev/null +++ b/test/cbmc/proofs/lib/summarize.py @@ -0,0 +1,92 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: MIT-0 + +import json +import logging + + +def _get_max_length_per_column_list(data): + ret = [len(item) + 1 for item in data[0]] + for row in data[1:]: + for idx, item in enumerate(row): + ret[idx] = max(ret[idx], len(item) + 1) + return ret + + +def _get_table_header_separator(max_length_per_column_list): + line_sep = "" + for max_length_of_word_in_col in max_length_per_column_list: + line_sep += "|" + "-" * (max_length_of_word_in_col + 1) + line_sep += "|\n" + return line_sep + + +def _get_entries(max_length_per_column_list, row_data): + entries = [] + for row in row_data: + entry = "" + for idx, word in enumerate(row): + max_length_of_word_in_col = max_length_per_column_list[idx] + space_formatted_word = (max_length_of_word_in_col - len(word)) * " " + entry += "| " + word + space_formatted_word + entry += "|\n" + entries.append(entry) + return entries + + +def _get_rendered_table(data): + table = [] + max_length_per_column_list = _get_max_length_per_column_list(data) + entries = _get_entries(max_length_per_column_list, data) + for idx, entry in enumerate(entries): + if idx == 1: + line_sep = _get_table_header_separator(max_length_per_column_list) + table.append(line_sep) + table.append(entry) + table.append("\n") + return "".join(table) + + +def _get_status_and_proof_summaries(run_dict): + """Parse a dict representing a Litani run and create lists summarizing the + proof results. + + Parameters + ---------- + run_dict + A dictionary representing a Litani run. + + Returns + ------- + A list of 2 lists. + The first sub-list maps a status to the number of proofs with that status. + The second sub-list maps each proof to its status. + """ + count_statuses = {} + proofs = [["Proof", "Status"]] + for proof_pipeline in run_dict["pipelines"]: + status_pretty_name = proof_pipeline["status"].title().replace("_", " ") + try: + count_statuses[status_pretty_name] += 1 + except KeyError: + count_statuses[status_pretty_name] = 1 + proof = proof_pipeline["name"] + proofs.append([proof, status_pretty_name]) + statuses = [["Status", "Count"]] + for status, count in count_statuses.items(): + statuses.append([status, str(count)]) + return [statuses, proofs] + + +def print_proof_results(out_file): + """ + Print 2 strings that summarize the proof results. + When printing, each string will render as a GitHub flavored Markdown table. + """ + try: + with open(out_file, encoding='utf-8') as run_json: + run_dict = json.load(run_json) + for summary in _get_status_and_proof_summaries(run_dict): + print(_get_rendered_table(summary)) + except Exception as ex: # pylint: disable=broad-except + logging.critical("Could not print results. Exception: %s", str(ex)) diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py deleted file mode 120000 index 126c3bc0d..000000000 --- a/test/cbmc/proofs/run-cbmc-proofs.py +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/proofs/run-cbmc-proofs.py \ No newline at end of file diff --git a/test/cbmc/proofs/run-cbmc-proofs.py b/test/cbmc/proofs/run-cbmc-proofs.py new file mode 100755 index 000000000..4274709fe --- /dev/null +++ b/test/cbmc/proofs/run-cbmc-proofs.py @@ -0,0 +1,414 @@ +#!/usr/bin/env python3 +# +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: MIT-0 + + +import argparse +import asyncio +import json +import logging +import math +import os +import pathlib +import re +import subprocess +import sys +import tempfile + +from lib.summarize import print_proof_results + + +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", + "--no-print-directory", + "-f", "Makefile.common", + "echo-project-name", + ] + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE, check=False) + 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": ["--fail-on-proof-failure"], + "action": "store_true", + "help": "exit with return code `10' if any proof failed" + " (default: exit 0)", + }, { + "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": ["--marker-file"], + "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": ["--debug"], + "action": "store_true", + "help": "debug output", + }, { + "flags": ["--summarize"], + "action": "store_true", + "help": "summarize proof results with two tables on stdout", + }, { + "flags": ["--version"], + "action": "version", + "version": "CBMC starter kit 2.5", + "help": "display version and exit" + }]: + 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): + # pylint: disable=consider-using-f-string + print("\rConfiguring CBMC proofs: " + "{complete:{width}} / {total:{width}}".format(**counter), end="", file=sys.stderr) + + +def get_proof_dirs(proof_root, proof_list, marker_file): + 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 root != str(proof_root) and ".litani_cache_dir" in fyles: + pathlib.Path(f"{root}/.litani_cache_dir").unlink() + 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 marker_file 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, fail_on_proof_failure, summarize): + cmd = [str(litani), "run-build"] + if jobs: + cmd.extend(["-j", str(jobs)]) + if fail_on_proof_failure: + cmd.append("--fail-on-pipeline-failure") + if summarize: + out_file = pathlib.Path(tempfile.gettempdir(), "run.json").resolve() + cmd.extend(["--out-file", str(out_file)]) + + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, check=False) + + if proc.returncode and not fail_on_proof_failure: + logging.critical("Failed to run litani run-build") + sys.exit(1) + + if summarize: + print_proof_results(out_file) + out_file.unlink() + + if proc.returncode: + logging.error("One or more proofs failed") + sys.exit(10) + +def get_litani_path(proof_root): + cmd = [ + "make", + "--no-print-directory", + f"PROOF_ROOT={proof_root}", + "-f", "Makefile.common", + "litani-path", + ] + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, universal_newlines=True, stdout=subprocess.PIPE, check=False) + 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, check=False) + 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: + match = re.match(r"^PROOF_UID\s*=\s*(?P\w+)", line) + if not match: + continue + if match["uid"] not in proof_uids: + proof_uids[match["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[match["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( # pylint: disable=too-many-arguments + queue, counter, proof_uids, enable_pools, enable_memory_profiling, debug): + 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 [] + + # Allow interactive tasks to preempt proof configuration + proc = await asyncio.create_subprocess_exec( + "nice", "-n", "15", "make", *pools, + *profiling, "-B", "_report", "" if debug else "--quiet", cwd=path, + stdout=asyncio.subprocess.PIPE, stderr=asyncio.subprocess.PIPE) + stdout, stderr = await proc.communicate() + logging.debug("returncode: %s", str(proc.returncode)) + logging.debug("stdout:") + for line in stdout.decode().splitlines(): + logging.debug(line) + logging.debug("stderr:") + for line in stderr.decode().splitlines(): + logging.debug(line) + + counter["fail" if proc.returncode else "pass"].append(path) + counter["complete"] += 1 + + print_counter(counter) + queue.task_done() + + +async def main(): # pylint: disable=too-many-locals + args = get_args() + set_up_logging(args.verbose) + + proof_root = pathlib.Path(os.getcwd()) + 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, + "--no-print-out-dir", + ] + + 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 ", + out_index, "\n") + + logging.debug(" ".join(cmd)) + proc = subprocess.run(cmd, check=False) + if proc.returncode: + logging.critical("Failed to run litani init") + sys.exit(1) + + proof_dirs = list(get_proof_dirs( + proof_root, args.proofs, args.marker_file)) + 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, args.debug)) + 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, args.fail_on_proof_failure, args.summarize) + + +if __name__ == "__main__": + asyncio.run(main()) diff --git a/test/cbmc/sources/README.md b/test/cbmc/sources/README.md deleted file mode 120000 index 969d1dee3..000000000 --- a/test/cbmc/sources/README.md +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/sources/README.md \ No newline at end of file diff --git a/test/cbmc/sources/README.md b/test/cbmc/sources/README.md new file mode 100644 index 000000000..4f706b23d --- /dev/null +++ b/test/cbmc/sources/README.md @@ -0,0 +1,6 @@ +CBMC proof source code +====================== + +This directory contains source code written for CBMC proofs. It is +common to write some code to model aspects of the system under test, +and this code goes here. diff --git a/test/cbmc/stubs/README.md b/test/cbmc/stubs/README.md deleted file mode 120000 index 327d6f6b7..000000000 --- a/test/cbmc/stubs/README.md +++ /dev/null @@ -1 +0,0 @@ -../aws-templates-for-cbmc-proofs/template-for-repository/stubs/README.md \ No newline at end of file diff --git a/test/cbmc/stubs/README.md b/test/cbmc/stubs/README.md new file mode 100644 index 000000000..3b7823dd6 --- /dev/null +++ b/test/cbmc/stubs/README.md @@ -0,0 +1,6 @@ +CBMC proof stubs +====================== + +This directory contains the stubs written for CBMC proofs. It is +common to stub out functionality like network send and receive methods +when writing a CBMC proof, and the code for these stubs goes here.