tests: rework makefiles

This is part of the new build, but self-contained enough to be merged
before that. It unifies most makefiles in tests/ into a single
mk/test.mk (mk is a new top-level directory for make infra).

It also disconnects examples/ and tests/. The mutually recursive
inclusions are hard to work with.

mk/common.mk

@@ -0,0 +1,92 @@
+# This makefile is included from several other makefiles in the tree.
+
+MAKEFLAGS += --no-builtin-rules
+Q?=@
+SIL?=--silent
+RUNLIM=
+ifneq ($(V),)
+	Q=
+	SIL=
+else
+	MAKEFLAGS += -s
+endif
+
+define NO_RUNLIM_ERR
+runlim not found:
+  To use RESOURCEMONITOR=1, the `runlim` tool must be installed and in your $$PATH.
+  It must also be a recent version supporting the `-p` option.
+  You can get it from: [https://github.com/arminbiere/runlim]
+endef
+
+define msg =
+@printf "   %-14s  %s\n" $(1) $(2)
+endef
+define bold_msg =
+@#-tput bold 2>/dev/null
+@printf -- "  %-15s" $(1)
+@#-tput sgr0 2>/dev/null
+@printf "  %s\n" $(2)
+endef
+
+# Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with
+# information about the time and space taken by each F* invocation.
+ifneq ($(RESOURCEMONITOR),)
+	ifeq ($(shell which runlim),)
+		_ := $(error $(NO_RUNLIM_ERR)))
+	endif
+	ifneq ($(MONID),)
+		MONPREFIX=$(MONID).
+	endif
+	RUNLIM=runlim -p -o $@.$(MONPREFIX)runlim
+endif
+
+# Ensure that any failing rule will not create its target file.
+# In other words, make `make` less insane.
+.DELETE_ON_ERROR:
+
+.DEFAULT_GOAL:=__undef
+.PHONY: __undef
+__undef:
+	$(error "This makefile does not have a default goal")
+
+# Check that a variable is defined. If not, abort with an (optional) error message.
+need =												\
+  $(if $(value $(strip $1)),,									\
+    $(error Need a value for $(strip $1)$(if $2, ("$(strip $2)"))))
+
+# Check that a variable is defined and pointing to an executable.
+# Is there no negation in make...?
+# Wew! this was interesting to write. Especially the override part.
+need_exe =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(wildcard $(value $(strip $1))),							\
+      $(if $(shell test -x $(value $(strip $1)) && echo 1),					\
+        $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+        $(error $(strip $1) ("$(value $(strip $1))") is not executable)),			\
+      $(error $(strip $1) ("$(value $(strip $1))") does not exist (cwd = $(CURDIR)))),		\
+    $(error Need an executable for $(strip $1)$(if $2, ("$(strip $2)"))))			\
+
+need_file =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(wildcard $(value $(strip $1))),							\
+      $(if $(shell test -f $(value $(strip $1)) && echo 1),					\
+        $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+        $(error $(strip $1) ("$(value $(strip $1))") is not executable)),			\
+      $(error $(strip $1) ("$(value $(strip $1))") does not exist (cwd = $(CURDIR)))),		\
+    $(error Need a file path for $(strip $1)$(if $2, ("$(strip $2)"))))				\
+
+need_dir =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(wildcard $(value $(strip $1))),							\
+      $(if $(shell test -d $(value $(strip $1)) && echo 1),					\
+        $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+        $(error $(strip $1) ("$(value $(strip $1))") is not executable)),			\
+      $(error $(strip $1) ("$(value $(strip $1))") is not a directory (cwd = $(CURDIR)))),	\
+    $(error Need an *existing* directory path for $(strip $1)$(if $2, ("$(strip $2)"))))	\
+
+need_dir_mk =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(shell mkdir -p $(value $(strip $1)) && echo 1),					\
+      $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+      $(error $(strip $1) ("$(value $(strip $1))") is not a directory (mkdir failed, cwd = $(CURDIR)))),	\
+    $(error Need a directory path for $(strip $1)$(if $2, ("$(strip $2)"))))			\

mk/test.mk

@@ -0,0 +1,79 @@
+# Include this makefile for unit tests. It mostly has all you need.
+# This is NOT meant for external consumption. Do not point to this.
+
+ifeq ($(FSTAR_ROOT),)
+  $(error FSTAR_ROOT is not set. Please set it to the root of your F* repository)
+endif
+include $(FSTAR_ROOT)/mk/common.mk
+.DEFAULT_GOAL := all
+
+# Set a default FSTAR_EXE for most clients.
+FSTAR_EXE ?= $(FSTAR_ROOT)/bin/fstar.exe
+
+OCAMLOPT := $(FSTAR_EXE) --ocamlenv ocamlfind opt
+
+HINTS_ENABLED?=--use_hints
+
+# This warning is really useless.
+OTHERFLAGS += --warn_error -321
+OTHERFLAGS += --ext context_pruning
+
+# Set ADMIT=1 to admit queries
+ADMIT ?=
+MAYBE_ADMIT = $(if $(ADMIT),--admit_smt_queries true)
+
+OUTPUT_DIR ?= _output
+CACHE_DIR ?= _cache
+
+FSTAR = $(FSTAR_EXE) $(SIL) 				\
+	--cache_checked_modules				\
+	--odir $(OUTPUT_DIR)				\
+	--cache_dir $(CACHE_DIR)			\
+	--already_cached Prims,FStar			\
+	 $(OTHERFLAGS) $(MAYBE_ADMIT) $(HINTS_ENABLED)
+
+ifeq ($(NODEPEND),)
+FSTAR_FILES ?= $(wildcard *.fst) $(wildcard *.fsti)
+$(call need, FSTAR_FILES, "List of F* files to verify. It defaults to all fst/fsti in the directory (none were found)")
+
+.depend: $(FSTAR_FILES)
+	$(call msg, "DEPEND", $(CURDIR))
+	$(FSTAR) --dep full $(FSTAR_FILES) --output_deps_to $@
+depend: .depend
+include .depend
+endif
+
+%.fst.checked:
+	$(call msg, "CHECK", $(basename $(notdir $@)))
+	$(FSTAR) $<
+	touch -c $@
+
+%.fsti.checked:
+	$(call msg, "CHECK", $(basename $(notdir $@)))
+	$(FSTAR) $<
+	touch -c $@
+
+%.fst.output: %.fst
+	$(call msg, "OUTPUT", $(basename $(notdir $@)))
+	$(FSTAR) --message_format human -f --print_expected_failures $< >$@ 2>&1
+
+%.fsti.output: %.fsti
+	$(call msg, "OUTPUT", $(basename $(notdir $@)))
+	$(FSTAR) --message_format human -f --print_expected_failures $< >$@ 2>&1
+
+%.fst.json_output: %.fst
+	$(call msg, "JSONOUT", $(basename $(notdir $@)))
+	$(FSTAR) --message_format json -f --print_expected_failures $< >$@ 2>&1
+
+%.fsti.json_output: %.fsti
+	$(call msg, "JSONOUT", $(basename $(notdir $@)))
+	$(FSTAR) --message_format json -f --print_expected_failures $< >$@ 2>&1
+
+$(OUTPUT_DIR)/%.ml:
+	$(call msg, "EXTRACT", $(basename $(notdir $@)))
+	$(FSTAR) $(subst .checked,,$(notdir $<)) --codegen OCaml --extract_module $(subst .fst.checked,,$(notdir $<))
+
+verify-all: $(ALL_CHECKED_FILES)
+
+clean:
+	rm -rf $(OUTPUT_DIR) $(CACHE_DIR) .depend

tests/.gitignore

@@ -0,0 +1,2 @@
+_cache
+_output

tests/Cfg.fst.config.json

@@ -0,0 +1,8 @@
+{
+  "fstar_exe": "../bin/fstar.exe",
+  "options": [
+    "--ext", "context_pruning"
+  ],
+  "include_dirs": [
+  ]
+}

tests/Makefile

@@ -1,31 +1,30 @@
-FSTAR_HOME=..
-export OTHERFLAGS += --ext context_pruning
-include ../examples/Makefile.include
+FSTAR_ROOT ?= ..
+# include $(FSTAR_ROOT)/mk/test.mk
+# ^ No need to include this here, we are just descending to other directories
 
 ALL_TEST_DIRS += bug-reports
+ALL_TEST_DIRS += simple_hello
+ALL_TEST_DIRS += dune_hello
+ALL_TEST_DIRS += semiring
 ALL_TEST_DIRS += coercions
 ALL_TEST_DIRS += error-messages
+ALL_TEST_DIRS += tactics
 ALL_TEST_DIRS += friends
 ALL_TEST_DIRS += ide
 ALL_TEST_DIRS += incl
 ALL_TEST_DIRS += machine_integers
 ALL_TEST_DIRS += micro-benchmarks
 ALL_TEST_DIRS += prettyprinting
 ALL_TEST_DIRS += projectors
+ALL_TEST_DIRS += typeclasses
 ALL_TEST_DIRS += restricted_includes
-ALL_TEST_DIRS += semiring
 ALL_TEST_DIRS += struct
-ALL_TEST_DIRS += tactics
-ALL_TEST_DIRS += typeclasses
 ALL_TEST_DIRS += vale
 ALL_TEST_DIRS += hacl
-ALL_TEST_DIRS += simple_hello
-ALL_TEST_DIRS += dune_hello
-HAS_OCAML := $(shell which ocamlfind 2>/dev/null)
+ALL_TEST_DIRS += calc
 
-ifneq (,$(HAS_OCAML))
+# GM: I am unconditionally enabling this.
 ALL_TEST_DIRS += extraction
-endif
 
 all: $(addsuffix .all, $(ALL_TEST_DIRS))
 clean: $(addsuffix .clean, $(ALL_TEST_DIRS))

tests/bug-reports/Makefile

@@ -1,10 +1,11 @@
-FSTAR_HOME=../..
-include $(FSTAR_HOME)/examples/Makefile.include
-include $(FSTAR_HOME)/ulib/ml/Makefile.include
+include Makefile.include
+# ^ stopgap so I don't have to rewrite this entire makefile (yet)
+# but the right thing to do is include /mk/test.mk and rewrite this.
 
 OTHERFLAGS+=--warn_error +240
 
-all: verify iverify not-verify extract
+all: verify iverify not-verify # extract
+.DEFAULT_GOAL := all
 
 ##################
 # Positive tests #
@@ -177,6 +178,9 @@ Bug1383.verify: OTHERFLAGS += --warn_error @275 #Z3 warnings are fatal
 Bug1694.verify: OTHERFLAGS += --codegen OCaml
 Bug2210.verify: OTHERFLAGS += --codegen OCaml
 
+# Disable hints, see #3572
+Bug1614a.verify: HINTS_ENABLED =
+
 Bug2684a.verify: OTHERFLAGS += --cache_checked_modules
 Bug2684b.verify: OTHERFLAGS += --cache_checked_modules
 Bug2684c.verify: OTHERFLAGS += --cache_checked_modules

tests/bug-reports/Makefile.include

@@ -0,0 +1,12 @@
+FSTAR_EXE ?= ../../bin/fstar.exe
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/common.mk
+include $(FSTAR_ROOT)/ulib/gmake/fstar.mk
+
+# we ignore the return result in benchmark runs because we can have micro-benchmarks which
+# produce error asserts when executed with '--admit_smt_queries true'
+%.uver: %.fst
+	$(Q)$(BENCHMARK_PRE) $(FSTAR)  $^
+
+%.fail-uver: %.fst
+	(! $(FSTAR) $^ >/dev/null 2>&1) || (echo "NEGATIVE TEST FAILED ($@)!" ; false)

tests/calc/Makefile

@@ -0,0 +1,3 @@
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
+all: verify-all

tests/coercions/Makefile

@@ -1,14 +1,3 @@
-FSTAR_HOME=../..
-
-FSTAR_FILES = $(wildcard *.fst)
-
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
 all: verify-all
-
-include $(FSTAR_HOME)/examples/Makefile.common
-
-verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES)))
-
-clean:
-	rm -f .depend
-	rm -rf _cache
-	rm -rf _output

tests/error-messages/Makefile

@@ -1,19 +1,13 @@
-FSTAR_HOME=../..
-all: check-all
-
-FSTAR_FILES=$(wildcard *.fst)
+FSTAR_ROOT ?= ../..
+include $(FSTAR_ROOT)/mk/test.mk
+all: $(if $(ACCEPT),accept,check-all)
 
 # This so that we don't get warnings about:
 # 241: "unable to load checked file"
 # 247: "checked file was not written"
 # 333: "unable to read hints"
 OTHERFLAGS+=--warn_error -241-247-333-274+240
 
-# Sorry, without this we can get noise in error locations.
-# See issue #1993. Also, warnings from dependencies would
-# pollute the output.
-OTHERFLAGS+=--already_cached 'Prims FStar'
-
 # Remove --query_stats and --hint_info from this subdir, since
 # they output timing info.
 OTHERFLAGS := $(filter-out --query_stats, $(OTHERFLAGS))
@@ -53,7 +47,6 @@ TuplePat.fst.output      : OTHERFLAGS+=--dump_module TuplePat
 Monoid.fst.json_output   : OTHERFLAGS+=--dump_module Monoid
 Monoid.fst.output        : OTHERFLAGS+=--dump_module Monoid
 
-include $(FSTAR_HOME)/examples/Makefile.common
 
 .PHONY: %.human_check
 %.human_check: %.expected %.output

tests/extraction/Makefile

@@ -1,12 +1,12 @@
-FSTAR_EXAMPLES=$(realpath ../../examples)
-include $(FSTAR_EXAMPLES)/Makefile.include
-include $(FSTAR_ULIB)/ml/Makefile.include
+FSTAR_ROOT ?= ../..
+NODEPEND=1
+include $(FSTAR_ROOT)/mk/test.mk
 
 all: inline_let all_cmi Eta_expand.test Div.test ExtractAs.test
 
-%.exe: %.fst | out
-	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml $<
-	$(OCAMLOPT) out/$(patsubst %.fst,%.ml,$<) -o $@
+%.exe: %.fst
+	$(FSTAR) --codegen OCaml $<
+	$(OCAMLOPT) -package fstar.lib -linkpkg $(OUTPUT_DIR)/$(patsubst %.fst,%.ml,$<) -o $@
 
 %.test: %.exe
 	$(call msg,RUN,$<)
@@ -22,19 +22,15 @@ Div.test: Div.exe
 
 inline_let: InlineLet.fst
 	$(FSTAR) --codegen OCaml InlineLet.fst
-	egrep -A 10 test InlineLet.ml | grep -qs "17"
+	egrep -A 10 test $(OUTPUT_DIR)/InlineLet.ml | grep -qs "17"
 	@touch $@
 
 all_cmi:
 	+$(MAKE) -C cmi all
 
-out:
-	mkdir -p out
-
 clean:
 	rm -rf out
 	rm -f *.exe
 	rm -f *~
 	rm -f *.exe *.test
 	rm -f inline_let
-