From 9b114bdfa1f5d2d6a95d9b26efa33198ec1a4efc Mon Sep 17 00:00:00 2001 From: "Brian G. Milnes" Date: Tue, 15 Oct 2024 22:29:49 -0700 Subject: [PATCH] Two changes: 1) __FL__ lexeme in FStarC_Parser_LexFStar.ml 2) tests/validation-time with a Test.LexemeFL.fst that checks __FL__ --- ocaml/fstar-lib/FStarC_Parser_LexFStar.ml | 1 + tests/Makefile | 1 + tests/validation-time/Makefile | 22 ++++++++++++++++++++++ tests/validation-time/README.md | 5 +++++ tests/validation-time/Test.LexemeFL.fst | 13 +++++++++++++ 5 files changed, 42 insertions(+) create mode 100644 tests/validation-time/Makefile create mode 100644 tests/validation-time/README.md create mode 100644 tests/validation-time/Test.LexemeFL.fst diff --git a/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml b/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml index e4ef505d01f..5943d01b513 100644 --- a/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml +++ b/ocaml/fstar-lib/FStarC_Parser_LexFStar.ml @@ -473,6 +473,7 @@ match%sedlex lexbuf with | "#print-effects-graph" -> PRAGMA_PRINT_EFFECTS_GRAPH | "__SOURCE_FILE__" -> STRING (L.source_file lexbuf) | "__LINE__" -> INT (string_of_int (L.current_line lexbuf), false) + | "__FL__" -> STRING ((L.source_file lexbuf) ^ "(" ^ (string_of_int (L.current_line lexbuf)) ^ ")") | Plus anywhite -> token lexbuf | newline -> L.new_line lexbuf; token lexbuf diff --git a/tests/Makefile b/tests/Makefile index e864166662f..5476766c02b 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -21,6 +21,7 @@ ALL_TEST_DIRS += vale ALL_TEST_DIRS += hacl ALL_TEST_DIRS += simple_hello ALL_TEST_DIRS += dune_hello +ALL_TEST_DIRS += validation-time HAS_OCAML := $(shell which ocamlfind 2>/dev/null) ifneq (,$(HAS_OCAML)) diff --git a/tests/validation-time/Makefile b/tests/validation-time/Makefile new file mode 100644 index 00000000000..01483aa279a --- /dev/null +++ b/tests/validation-time/Makefile @@ -0,0 +1,22 @@ +# +# This does nothing but the default validation as these are validation time test modules. +# Most are let _ = assert(...) which is extremely cool to test at validation time! +# + +WARN_ERROR=--warn_error -321 +FSTAR_HOME=../.. +FSTAR_FILES=$(wildcard *.fst) +FSTAR_EXAMPLES=$(realpath ../../examples) +include $(FSTAR_EXAMPLES)/Makefile.include + +all: verify-all + +include $(FSTAR_HOME)/examples/Makefile.common + +verify-all: $(CACHE_DIR) $(addsuffix .checked, $(addprefix $(CACHE_DIR)/, $(FSTAR_FILES))) + +clean: + $(call msg, "CLEAN") + $(Q)rm -f .depend + $(Q)rm -rf _cache + $(Q)rm -rf _output diff --git a/tests/validation-time/README.md b/tests/validation-time/README.md new file mode 100644 index 00000000000..a0b516b2772 --- /dev/null +++ b/tests/validation-time/README.md @@ -0,0 +1,5 @@ + + This directory contains tests that run on Make all which only validate F* files. + This allows validation time tests. If any validation fails, the file's tests fail. + + Tests for an F* module FStar.M can be named Test.FStar.M.fst by default. diff --git a/tests/validation-time/Test.LexemeFL.fst b/tests/validation-time/Test.LexemeFL.fst new file mode 100644 index 00000000000..9c2b311db43 --- /dev/null +++ b/tests/validation-time/Test.LexemeFL.fst @@ -0,0 +1,13 @@ +/// A new lexeme __FL__ has been added to show file and line (file(line)) to make writing tests easier. +/// This file is line sensitive any edit will change the value of __FL__. +module Test.LexemeFL +open FStar.Tactics.V2 +open FStar.String +module LT = FStar.List.Tot +// Kinda funky to get a good validation time test, added Strings in other PR will fix this. +// The lexer is sending back some strange character that we have to adjust. +let fl = __FL__ +let _ = assert(fl <> "") +let fl' = string_of_list (list_of_string "Test.LexemFL.fst(11)") +let _ = assert((strlen fl') = 20) by compute() +let _ = assert(fl' = "Test.LexemFL.fst(11)") by compute()