# -*- 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 <DIR>.
#      b. Write a proof harness (a function) with the name <HARNESS_ENTRY>
#         in a file with the name <DIR>/<HARNESS_FILE>.c
#      c. Write a makefile with the name <DIR>/Makefile that looks
#         something like
#
#         HARNESS_FILE=<HARNESS_FILE>
#         HARNESS_ENTRY=<HARNESS_ENTRY>
#         PROOF_UID=<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 <DIR> 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

# 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 or loop invariants in
# CBMC proofs. They should follow three distinct processes:
# 1. Check whether a function contract is sound, where CHECK_FUNCTION_CONTRACTS
#    contains the list of functions with contracts to be checked.
# 2. Replace function calls with their correspondent function contracts,
#    where USE_FUNCTION_CONTRACTS contains the list of functions with
#    contracts to be replaced. One must check separately whether a function
#    contract is sound before replacing it.
# 3. Apply loop invariants during verification, where APPLY_LOOP_INVARIANTS
#    contains the list of functions with loop invariants to be applied.
#    This option is currently unavailable.
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))

################################################################
################################################################
## 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)/code_contracts.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)/code_contracts.txt \
	  --interleave-stdout-stderr \
	  --pipeline-name "$(PROOF_UID)" \
	  --ci-stage build \
	  --description "$(PROOF_UID): replacing function calls with function contracts"
endif

# Optionally fill static variable with unconstrained values
$(HARNESS_GOTO)4.goto: $(HARNESS_GOTO)3.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)5.goto: $(HARNESS_GOTO)4.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)6.goto: $(HARNESS_GOTO)5.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)6.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 $@ \
	  --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 $@ \
	  --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 $@ \
	  --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 \
	  --tags "stats-group:report generation" \
	  --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 \
	  --tags "stats-group:report generation" \
	  --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

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