Makefile.proof

PROOF_MODE ?= all

jobs ?= 4

$(foreach dep,$($(name)-deplibs), \
	$(eval SPARKFLAGS += -aP=$($(dep)-dir)))

SPARKFLAGS += -j$(jobs)
SPARKFLAGS += -k
SPARKFLAGS += -m
SPARKFLAGS += --mode=$(PROOF_MODE)
SPARKFLAGS += --report=fail
SPARKFLAGS += --warnings=error
SPARKFLAGS += --no-inlining
SPARKFLAGS += --prover=z3 --steps=500 --timeout=2	# FIXME: timeout used because steps seems broken

quote-list = $(subst $(space),$(comma),$(patsubst %,"%",$(1)))

$(name)-exclude-srcs = \
	$(filter-out \
		$(sort $(notdir $($(name)-proof) \
			$($(name)-srcs) $($(name)-gens) $($(name)-extra-specs) $($(name)-extra-gens))), \
		$(sort $(notdir \
			$(wildcard $(addsuffix *.ad[sb],$($(name)-proof-dirs))))))

# Has to reside in the working directory. gnatprove takes paths relative
# to the directory wher it's placed and reports internal errors if used
# with absolute paths.
gpr := $(name).gpr
gpr-name = $(subst -,_,$(subst .,_,$(basename $(notdir $@))))

# Will be installed for inclusion
libgpr := $(obj)/lib$(name).gpr

.SECONDEXPANSION:

$(gpr):
	@printf "    GENERATE   $(subst $(obj)/,,$@)\n"
	printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@
	echo 'library project $(gpr-name) is'			>>$@
	echo '   for Library_Name use "$(name)";'		>>$@
	echo '   for Library_Dir use "$(obj)/adalib";'		>>$@
	echo '   for Source_Dirs use' \
		'($(call quote-list,$($(name)-proof-dirs)));'	>>$@
	echo '   for Object_Dir use "$(obj)";'			>>$@
	echo '   package Builder is'				>>$@
	echo '      for Global_Configuration_Pragmas use' \
		'"$(abspath $(libhw-dir)/spark.adc)";'		>>$@
	echo '   end Builder;'					>>$@
	echo '   for Excluded_Source_Files use' \
		'($(call quote-list,$($(name)-exclude-srcs)));' >>$@
	echo 'end $(gpr-name);'					>>$@

.INTERMEDIATE: $(gpr)

$(libgpr): $$(MAKEFILE_LIST)
	@printf "    GENERATE   $(subst $(obj)/,,$@)\n"
	printf '$(if $($(name)-deplibs),with "%s";\n)' $($(name)-deplibs) >$@
	echo 'library project lib$(name) is'			>>$@
	echo '   for Library_Name use "$(name)";'		>>$@
	echo '   for Library_Dir use "lib";'			>>$@
	echo '   for Library_ALI_Dir use "lib";'		>>$@
	echo '   for Source_Dirs use ("proof");'		>>$@
	echo '   for Object_Dir use external ("obj", "build");'	>>$@
	echo 'end lib$(name);'					>>$@

# We want to filter gnatprove's command-line output through `sed`,
# and *also* capture its return value. Not that easy, we'll pipe the
# return code through file descriptor #3.
#
# 1: command w/ return value
# 2: filter command, ignore return value
#
filter-output = { { { { $(1); } 2>&1; echo $$? >&3; } | $(2) >&2; } 3>&1 | { read ret; exit $${ret}; }; } 2>&1

$(obj)/gnatprove/gnatprove.out: $$($(name)-srcs) $$($(name)-gens)
$(obj)/gnatprove/gnatprove.out: $$($(name)-extra-specs) $$($(name)-extra-gens)
$(obj)/gnatprove/gnatprove.out: $(gpr) $(obj)/proofmode
	$(call filter-output, \
	  $(MAKE) -j$(jobs) && gnatprove -P$< $(SPARKFLAGS) -Xobj=$(abspath $(obj)), \
	  sed $(foreach file,$^,-e 's|$(notdir $(file)):[0-9]\+:[0-9]\+:|$(dir $(file))&|'))
proof:
	if [ "$(PROOF_MODE)" != "$$(cat $(obj)/proofmode 2>/dev/null)" ]; then \
		echo "$(PROOF_MODE)" >$(obj)/proofmode; \
	fi
	$(MAKE) $(obj)/gnatprove/gnatprove.out

check: export override PROOF_MODE=check
check: proof

flow: export override PROOF_MODE=flow
flow: proof

full: export override PROOF_MODE=all
full: proof

allconfigs = $(wildcard configs/*)
allconfigs-targets = $(addprefix allconfigs-,$(notdir $(allconfigs)))

$(allconfigs-targets): jobs=1
$(allconfigs-targets): allconfigs-%: configs/%
	rm -rf proof-allconfigs/$* $(name)_$*.gpr
	mkdir -p proof-allconfigs/$*
	echo "$(PROOF_MODE)" >proof-allconfigs/$*/proofmode
	$(call filter-output, \
	  $(MAKE) obj=proof-allconfigs/$* cnf=configs/$* gpr=$(name)_$*.gpr jobs=$(jobs) \
		  proof-allconfigs/$*/gnatprove/gnatprove.out, \
	  sed 's/^[^[:space:]]\+:[0-9]\+:[0-9]\+:/$*::&/')

proof-allconfigs: $(allconfigs-targets)

clean::
	rm -rf proof-allconfigs/

.PHONY: proof check flow full $(allconfigs-targets) proof-allconfigs