From a20819f170acc6aad7b5aca2fbe53c7b3ab7e2b8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 16 Nov 2022 14:40:34 +0100 Subject: Automatically generate the Makefile and _CoqProject files in the tests subdirectories --- compiler/SymbolicToPure.ml | 2 ++ tests/coq/Makefile | 22 ++++++++++++++++++++-- tests/coq/betree/Makefile | 1 + tests/coq/betree/_CoqProject | 4 ++-- tests/coq/hashmap/Makefile | 1 + tests/coq/hashmap/_CoqProject | 6 +++--- tests/coq/hashmap_on_disk/Makefile | 1 + tests/coq/hashmap_on_disk/_CoqProject | 4 ++-- tests/coq/misc/Makefile | 1 + tests/coq/misc/_CoqProject | 8 ++++---- tests/fstar/Makefile | 10 +++++++++- tests/fstar/Makefile.template | 3 ++- tests/fstar/betree/Makefile | 1 + tests/fstar/betree_back_stateful/Makefile | 1 + tests/fstar/hashmap/Makefile | 1 + tests/fstar/hashmap_on_disk/Makefile | 1 + tests/fstar/misc/Makefile | 1 + 17 files changed, 53 insertions(+), 15 deletions(-) diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 4ea7071b..9d8724ab 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -1637,6 +1637,8 @@ and translate_expansion (p : S.mplace option) (sv : V.symbolic_value) match branches with | [] -> raise (Failure "Unreachable") | [ (variant_id, svl, branch) ] + (* TODO: always introduce a match, and use micro-passes to turn the + the match into a let *) when not (TypesUtils.ty_is_custom_adt sv.V.sv_ty && !Config.always_deconstruct_adts_with_matches) -> ( diff --git a/tests/coq/Makefile b/tests/coq/Makefile index a9c170f7..8dee394b 100644 --- a/tests/coq/Makefile +++ b/tests/coq/Makefile @@ -1,11 +1,15 @@ -ALL_DIRS ?= $(filter-out Makefile%, $(wildcard *)) +ALL_DIRS ?= $(filter-out %.template, $(filter-out Makefile%, $(wildcard *))) VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS)) CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS)) +COPY_MAKEFILES = $(addprefix copy-makefile-,$(ALL_DIRS)) + +GEN_COQ_PROJECT = $(addprefix gen-coq-project-,$(ALL_DIRS)) + .PHONY: all -all: $(VERIFY_DIRS) +all: $(COPY_MAKEFILES) $(GEN_COQ_PROJECT) $(VERIFY_DIRS) .PHONY: clean clean: $(CLEAN_DIRS) @@ -14,6 +18,20 @@ clean: $(CLEAN_DIRS) verif-%: cd $* && make all +.PHONY: copy-makefile-% +copy-makefile-%: + rm -f $*/Makefile + echo "# This file was automatically generated - modify ../Makefile.template instead" >> $*/Makefile + cat Makefile.template >> $*/Makefile + +.PHONY: gen-coq-project-% +gen-coq-project-%: + rm -f $*/_CoqProject + echo "# This file was automatically generated - see ../Makefile" >> $*/_CoqProject + cat _CoqProject.template >> $*/_CoqProject + echo $(patsubst $*/%,"\n"%,$(wildcard $*/*.v)) >> $*/_CoqProject + sed -i -z "s/ \n/\n/g" $*/_CoqProject + .PHONY: clean-% clean-%: cd $* && make clean diff --git a/tests/coq/betree/Makefile b/tests/coq/betree/Makefile index ff1ccd39..1a5aee4a 100644 --- a/tests/coq/betree/Makefile +++ b/tests/coq/betree/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead # Makefile originally taken from coq-club %: Makefile.coq phony diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject index 3cf45746..42c62421 100644 --- a/tests/coq/betree/_CoqProject +++ b/tests/coq/betree/_CoqProject @@ -1,9 +1,9 @@ +# This file was automatically generated - see ../Makefile -R . Lib -arg -w -arg all +BetreeMain_Types.v Primitives.v - BetreeMain_Funs.v BetreeMain_Opaque.v -BetreeMain_Types.v \ No newline at end of file diff --git a/tests/coq/hashmap/Makefile b/tests/coq/hashmap/Makefile index ff1ccd39..1a5aee4a 100644 --- a/tests/coq/hashmap/Makefile +++ b/tests/coq/hashmap/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead # Makefile originally taken from coq-club %: Makefile.coq phony diff --git a/tests/coq/hashmap/_CoqProject b/tests/coq/hashmap/_CoqProject index 94708adc..7f80afbf 100644 --- a/tests/coq/hashmap/_CoqProject +++ b/tests/coq/hashmap/_CoqProject @@ -1,8 +1,8 @@ +# This file was automatically generated - see ../Makefile -R . Lib -arg -w -arg all -Primitives.v - Hashmap_Types.v -Hashmap_Funs.v \ No newline at end of file +Primitives.v +Hashmap_Funs.v diff --git a/tests/coq/hashmap_on_disk/Makefile b/tests/coq/hashmap_on_disk/Makefile index ff1ccd39..1a5aee4a 100644 --- a/tests/coq/hashmap_on_disk/Makefile +++ b/tests/coq/hashmap_on_disk/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead # Makefile originally taken from coq-club %: Makefile.coq phony diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject index 95b82c41..b78c7b5f 100644 --- a/tests/coq/hashmap_on_disk/_CoqProject +++ b/tests/coq/hashmap_on_disk/_CoqProject @@ -1,9 +1,9 @@ +# This file was automatically generated - see ../Makefile -R . Lib -arg -w -arg all +HashmapMain_Types.v Primitives.v - HashmapMain_Funs.v HashmapMain_Opaque.v -HashmapMain_Types.v \ No newline at end of file diff --git a/tests/coq/misc/Makefile b/tests/coq/misc/Makefile index ff1ccd39..1a5aee4a 100644 --- a/tests/coq/misc/Makefile +++ b/tests/coq/misc/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead # Makefile originally taken from coq-club %: Makefile.coq phony diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index b8590272..c9ee0ff6 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -1,13 +1,13 @@ +# This file was automatically generated - see ../Makefile -R . Lib -arg -w -arg all Primitives.v - -Constants.v External_Funs.v -External_Opaque.v +Constants.v +PoloniusList.v External_Types.v NoNestedBorrows.v +External_Opaque.v Paper.v -PoloniusList.v \ No newline at end of file diff --git a/tests/fstar/Makefile b/tests/fstar/Makefile index a9c170f7..aad3354e 100644 --- a/tests/fstar/Makefile +++ b/tests/fstar/Makefile @@ -4,8 +4,10 @@ VERIFY_DIRS = $(addprefix verif-,$(ALL_DIRS)) CLEAN_DIRS = $(addprefix clean-,$(ALL_DIRS)) +COPY_MAKEFILES = $(addprefix copy-makefile-,$(ALL_DIRS)) + .PHONY: all -all: $(VERIFY_DIRS) +all: $(COPY_MAKEFILES) $(VERIFY_DIRS) .PHONY: clean clean: $(CLEAN_DIRS) @@ -14,6 +16,12 @@ clean: $(CLEAN_DIRS) verif-%: cd $* && make all +.PHONY: copy-makefile-% +copy-makefile-%: + rm -f $*/Makefile + echo "# This file was automatically generated - modify ../Makefile.template instead" >> $*/Makefile + cat Makefile.template >> $*/Makefile + .PHONY: clean-% clean-%: cd $* && make clean diff --git a/tests/fstar/Makefile.template b/tests/fstar/Makefile.template index a16b0edb..14790d6d 100644 --- a/tests/fstar/Makefile.template +++ b/tests/fstar/Makefile.template @@ -8,7 +8,8 @@ FSTAR_OPTIONS = $(FSTAR_HINTS) \ --cache_checked_modules $(FSTAR_INCLUDES) --cmi \ --warn_error '+241@247+285-274' \ -FSTAR_NO_FLAGS = fstar.exe --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj +FSTAR_EXE ?= fstar.exe +FSTAR_NO_FLAGS = $(FSTAR_EXE) --already_cached 'Prims FStar LowStar Steel' --odir obj --cache_dir obj FSTAR = $(FSTAR_NO_FLAGS) $(FSTAR_OPTIONS) diff --git a/tests/fstar/betree/Makefile b/tests/fstar/betree/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/betree/Makefile +++ b/tests/fstar/betree/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) diff --git a/tests/fstar/betree_back_stateful/Makefile b/tests/fstar/betree_back_stateful/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/betree_back_stateful/Makefile +++ b/tests/fstar/betree_back_stateful/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) diff --git a/tests/fstar/hashmap/Makefile b/tests/fstar/hashmap/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/hashmap/Makefile +++ b/tests/fstar/hashmap/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) diff --git a/tests/fstar/hashmap_on_disk/Makefile b/tests/fstar/hashmap_on_disk/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/hashmap_on_disk/Makefile +++ b/tests/fstar/hashmap_on_disk/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) diff --git a/tests/fstar/misc/Makefile b/tests/fstar/misc/Makefile index 14790d6d..fa7d1f36 100644 --- a/tests/fstar/misc/Makefile +++ b/tests/fstar/misc/Makefile @@ -1,3 +1,4 @@ +# This file was automatically generated - modify ../Makefile.template instead INCLUDE_DIRS = . FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) -- cgit v1.2.3