Add makefiles to test the F* files

7 files changed, 283 insertions, 6 deletions

diff --git a/Makefile b/Makefile
index 1e62dfd5..58919a7b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,4 +1,4 @@
-all: build-test
+all: build-test-verify
 
 CHARON_HOME = ../charon
 CHARON_EXEC = $(CHARON_HOME)/charon
@@ -19,21 +19,26 @@ TRANS_OPTIONS := -test-trans-units $(OPTIONS)
 SUBDIR :=
 
 # Build the project and test it
-.PHONY: build-test
-build-test: build test
+.PHONY: build-test-verify
+build-test-verify: build test verify
 
 # Build the project
 .PHONY: build
 build:
 	dune build src/main.exe
 
-# Test the project
+# Test the project by translating test files to F*
 .PHONY: test
 test: build trans-no_nested_borrows trans-paper \
 	trans-hashmap trans-hashmap_main \
 	trans-external trans-nll-betree_nll \
 	trans-nll-betree_main
 
+# Verify the translated F* files
+.PHONY: verify
+verify: build test
+	cd tests && make all
+
 # Add specific options to some tests
 trans-no_nested_borrows trans-paper: \
 	TRANS_OPTIONS += -test-units -no-split-files -no-state -no-decreases-clauses
diff --git a/tests/Makefile b/tests/Makefile
new file mode 100644
index 00000000..a9c170f7
--- /dev/null
+++ b/tests/Makefile
@@ -0,0 +1,19 @@
+ALL_DIRS ?= $(filter-out Makefile%, $(wildcard *))
+
+VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS))
+
+CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS))
+
+.PHONY: all
+all: $(VERIFY_DIRS)
+
+.PHONY: clean
+clean: $(CLEAN_DIRS)
+
+.PHONY: verif-%
+verif-%:
+	cd $* && make all
+
+.PHONY: clean-%
+clean-%:
+	cd $* && make clean
diff --git a/tests/Makefile.template b/tests/Makefile.template
new file mode 100644
index 00000000..fed1a280
--- /dev/null
+++ b/tests/Makefile.template
@@ -0,0 +1,51 @@
+INCLUDE_DIRS = .
+
+FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
+
+FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
+
+FSTAR_OPTIONS = $(FSTAR_HINTS) \
+  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --warn_error '+241@247+285-274' \
+  --cache_dir obj
+
+FSTAR_NO_FLAGS = fstar.exe
+
+FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
+
+# The F* roots are used to compute the dependency graph, and generate the .depend file
+FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
+
+# This is the right way to ensure the .depend file always gets re-built.
+ifeq (,$(filter %-in,$(MAKECMDGOALS)))
+ifndef NODEPEND
+ifndef MAKE_RESTARTS
+.depend: .FORCE
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \
+	    --extract 'krml:*' \
+	    --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \
+	    > $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+endif
+
+# For the interactive mode
+%.fst %.fsti:
+	$(FSTAR) $@
+
+# Generete the .checked files in bash mode
+%.checked:
+	$(FSTAR) $(FSTAR_FLAGS) $* && \
+	touch -c $*
+
+# Build all the files
+all: $(ALL_CHECKED_FILES)
+
+.PHONY: clean
+clean:
+	rm -f obj/*
diff --git a/tests/betree/Makefile b/tests/betree/Makefile
new file mode 100644
index 00000000..fed1a280
--- /dev/null
+++ b/tests/betree/Makefile
@@ -0,0 +1,51 @@
+INCLUDE_DIRS = .
+
+FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
+
+FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
+
+FSTAR_OPTIONS = $(FSTAR_HINTS) \
+  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --warn_error '+241@247+285-274' \
+  --cache_dir obj
+
+FSTAR_NO_FLAGS = fstar.exe
+
+FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
+
+# The F* roots are used to compute the dependency graph, and generate the .depend file
+FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
+
+# This is the right way to ensure the .depend file always gets re-built.
+ifeq (,$(filter %-in,$(MAKECMDGOALS)))
+ifndef NODEPEND
+ifndef MAKE_RESTARTS
+.depend: .FORCE
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \
+	    --extract 'krml:*' \
+	    --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \
+	    > $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+endif
+
+# For the interactive mode
+%.fst %.fsti:
+	$(FSTAR) $@
+
+# Generete the .checked files in bash mode
+%.checked:
+	$(FSTAR) $(FSTAR_FLAGS) $* && \
+	touch -c $*
+
+# Build all the files
+all: $(ALL_CHECKED_FILES)
+
+.PHONY: clean
+clean:
+	rm -f obj/*
diff --git a/tests/hashmap/Makefile b/tests/hashmap/Makefile
new file mode 100644
index 00000000..fed1a280
--- /dev/null
+++ b/tests/hashmap/Makefile
@@ -0,0 +1,51 @@
+INCLUDE_DIRS = .
+
+FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
+
+FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
+
+FSTAR_OPTIONS = $(FSTAR_HINTS) \
+  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --warn_error '+241@247+285-274' \
+  --cache_dir obj
+
+FSTAR_NO_FLAGS = fstar.exe
+
+FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
+
+# The F* roots are used to compute the dependency graph, and generate the .depend file
+FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
+
+# This is the right way to ensure the .depend file always gets re-built.
+ifeq (,$(filter %-in,$(MAKECMDGOALS)))
+ifndef NODEPEND
+ifndef MAKE_RESTARTS
+.depend: .FORCE
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \
+	    --extract 'krml:*' \
+	    --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \
+	    > $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+endif
+
+# For the interactive mode
+%.fst %.fsti:
+	$(FSTAR) $@
+
+# Generete the .checked files in bash mode
+%.checked:
+	$(FSTAR) $(FSTAR_FLAGS) $* && \
+	touch -c $*
+
+# Build all the files
+all: $(ALL_CHECKED_FILES)
+
+.PHONY: clean
+clean:
+	rm -f obj/*
diff --git a/tests/hashmap_on_disk/Makefile b/tests/hashmap_on_disk/Makefile
new file mode 100644
index 00000000..fed1a280
--- /dev/null
+++ b/tests/hashmap_on_disk/Makefile
@@ -0,0 +1,51 @@
+INCLUDE_DIRS = .
+
+FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
+
+FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
+
+FSTAR_OPTIONS = $(FSTAR_HINTS) \
+  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --warn_error '+241@247+285-274' \
+  --cache_dir obj
+
+FSTAR_NO_FLAGS = fstar.exe
+
+FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
+
+# The F* roots are used to compute the dependency graph, and generate the .depend file
+FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
+
+# This is the right way to ensure the .depend file always gets re-built.
+ifeq (,$(filter %-in,$(MAKECMDGOALS)))
+ifndef NODEPEND
+ifndef MAKE_RESTARTS
+.depend: .FORCE
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \
+	    --extract 'krml:*' \
+	    --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \
+	    > $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+endif
+
+# For the interactive mode
+%.fst %.fsti:
+	$(FSTAR) $@
+
+# Generete the .checked files in bash mode
+%.checked:
+	$(FSTAR) $(FSTAR_FLAGS) $* && \
+	touch -c $*
+
+# Build all the files
+all: $(ALL_CHECKED_FILES)
+
+.PHONY: clean
+clean:
+	rm -f obj/*
diff --git a/tests/misc/Makefile b/tests/misc/Makefile
index 5153d201..fed1a280 100644
--- a/tests/misc/Makefile
+++ b/tests/misc/Makefile
@@ -1,2 +1,51 @@
-%.fst-in %.fsti-in:
-	@echo --include ../hashmap
+INCLUDE_DIRS = .
+
+FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS))
+
+FSTAR_HINTS ?= --use_hints --use_hint_hashes --record_hints
+
+FSTAR_OPTIONS = $(FSTAR_HINTS) \
+  --odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
+  --warn_error '+241@247+285-274' \
+  --cache_dir obj
+
+FSTAR_NO_FLAGS = fstar.exe
+
+FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS)
+
+# The F* roots are used to compute the dependency graph, and generate the .depend file
+FSTAR_ROOTS ?= $(wildcard *.fst *.fsti)
+
+# This is the right way to ensure the .depend file always gets re-built.
+ifeq (,$(filter %-in,$(MAKECMDGOALS)))
+ifndef NODEPEND
+ifndef MAKE_RESTARTS
+.depend: .FORCE
+	$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) \
+	    --extract 'krml:*' \
+	    --extract 'OCaml:-* +FStar.Krml.Endianness +Vale.Arch +Vale.X64 -Vale.X64.MemoryAdapters +Vale.Def +Vale.Lib +Vale.Bignum.X64 -Vale.Lib.Tactics +Vale.Math +Vale.Transformers +Vale.AES +Vale.Interop +Vale.Arch.Types +Vale.Arch.BufferFriend +Vale.Lib.X64 +Vale.SHA.X64 +Vale.SHA.SHA_helpers +Vale.Curve25519.X64 +Vale.Poly1305.X64 +Vale.Inline +Vale.AsLowStar +Vale.Test +Spec +Lib -Lib.IntVector +C' \
+	    > $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+endif
+
+# For the interactive mode
+%.fst %.fsti:
+	$(FSTAR) $@
+
+# Generete the .checked files in bash mode
+%.checked:
+	$(FSTAR) $(FSTAR_FLAGS) $* && \
+	touch -c $*
+
+# Build all the files
+all: $(ALL_CHECKED_FILES)
+
+.PHONY: clean
+clean:
+	rm -f obj/*