diff --git a/lib/AstToCStar.ml b/lib/AstToCStar.ml index 168b1e72..9137a8a4 100644 --- a/lib/AstToCStar.ml +++ b/lib/AstToCStar.ml @@ -674,7 +674,7 @@ and mk_stmts env e ret_type = | EAbort (_, s) -> env, CStar.Abort (Option.value ~default:"" s) :: comment e.meta @ acc - | ESwitch (e, branches) -> + | ESwitch (e0, branches) -> let default, branches = List.partition (function (SWild, _) -> true | _ -> false) branches in @@ -683,14 +683,14 @@ and mk_stmts env e ret_type = | [] -> None | _ -> failwith "impossible" in - env, CStar.Switch (mk_expr env false false e, + env, CStar.Switch (mk_expr env false false e0, List.map (fun (lid, e) -> (match lid with | SConstant k -> `Int k - | SEnum lid -> `Ident lid + | SEnum lid -> `Ident (GlobalNames.mangle_enum lid e0.typ) | _ -> failwith "impossible"), mk_block env return_pos e - ) branches, default) :: comment e.meta @ acc + ) branches, default) :: comment e0.meta @ acc | EReturn e -> mk_as_return env e (comment e.meta @ acc) Must diff --git a/lib/CStarToC11.ml b/lib/CStarToC11.ml index b186fa23..d089c739 100644 --- a/lib/CStarToC11.ml +++ b/lib/CStarToC11.ml @@ -1401,7 +1401,7 @@ let mk_type_or_external m (w: where) ?(is_inline_static=false) (d: decl): C.decl else failwith "TODO: support for negative enum values" in - let cases = List.map (fun (lid, v) -> to_c_name m (lid, Macro), v) cases in + let cases = List.map (fun (lid, v) -> to_c_name m (lid, Other), v) cases in wrap_verbatim name flags (Text (enum_as_macros cases)) @ let qs, spec, decl = mk_spec_and_declarator_t m name (Int t) in [ Decl ([], (qs, spec, None, Some Typedef, { maybe_unused = false; target = None }, [ decl, None, None ]))] diff --git a/test/Makefile b/test/Makefile index 9079492c..208b6615 100644 --- a/test/Makefile +++ b/test/Makefile @@ -85,7 +85,7 @@ FSTAR = $(FSTAR_EXE) \ --trivial_pre_for_unannotated_effectful_fns false \ --cmi --warn_error -274 -all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test rust-val-test +all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test rust-val-test bundle-test # Needs node wasm: $(WASM_FILES) @@ -291,6 +291,10 @@ sepcomp-test: +$(MAKE) -C sepcomp .PHONY: sepcomp-test +bundle-test: + +$(MAKE) -C bundle +.PHONY: bundle-test + rust-val-test: +$(MAKE) -C rust-val .PHONY: rust-val-test diff --git a/test/bundle/.gitignore b/test/bundle/.gitignore new file mode 100644 index 00000000..78e15dff --- /dev/null +++ b/test/bundle/.gitignore @@ -0,0 +1,2 @@ +dist +obj diff --git a/test/bundle/Base.fst b/test/bundle/Base.fst new file mode 100644 index 00000000..d9660640 --- /dev/null +++ b/test/bundle/Base.fst @@ -0,0 +1,4 @@ +module Base +type test = | Foo | Bar + +let f (x: Base.test) : Tot bool = Base.Foo? x diff --git a/test/bundle/Derived.fst b/test/bundle/Derived.fst new file mode 100644 index 00000000..d115ca8f --- /dev/null +++ b/test/bundle/Derived.fst @@ -0,0 +1,3 @@ +module Derived + +let g (x: bool) : Tot bool = Base.f Base.Foo = x diff --git a/test/bundle/Makefile b/test/bundle/Makefile new file mode 100644 index 00000000..1c721332 --- /dev/null +++ b/test/bundle/Makefile @@ -0,0 +1,179 @@ +include ../../Makefile.common + +############################# +# This is the main Makefile # +############################# + +# This tutorial assumes you have a degree of familiarity with GNU make, +# including automatic variables such as $@, $< and $^. Some mandatory reading if +# you are not fluent in GNU make: +# - https://www.gnu.org/software/make/manual/html_node/Automatic-Variables.html#Automatic-Variables +# - https://www.gnu.org/software/make/manual/html_node/Pattern-Intro.html#Pattern-Intro +# - https://www.gnu.org/software/make/manual/html_node/Pattern_002dspecific.html#Pattern_002dspecific + +# I usually prefer to rule out OSX make on the basis that it doesn't have the +# shortest stem rule, which is incredibly useful. +ifeq (3.81,$(MAKE_VERSION)) + $(error You seem to be using the OSX antiquated Make version. Hint: brew \ + install make, then invoke gmake instead of make) +endif + + +# Main entry points (first one is default) +# ---------------------------------------- + +all: dist/Derived.o + +include Makefile.include + +# Definition of F* flags +# ---------------------- + +# Some reasonable flags to turn on: +# - 247: checked file not written because some of its dependencies... +# - 285: missing or file not found, almost always something to act on +# - 241: stale dependencies, almost always a sign that the build is incorrect +# +# But also: +# - --cmi, for cross-module inlining, a must-have for anyone who relies on +# inline_for_extraction in the presence of interfaces +# - --cache_dir, to place checked files there + +FSTAR_EXE ?= fstar.exe +FSTAR_NO_FLAGS = $(FSTAR_EXE) \ + --odir obj $(FSTAR_INCLUDES) --cmi \ + --already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \ + --cache_dir obj + +# Initial dependency analysis +# --------------------------- + +# Important to wildcard both fst and fsti since there are fstis without fsts, +# etc. Note that I'm using wildcard rather than assume $(SHELL) is bash and has +# fancy globbing rules -- particularly true on Windows. +FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \ + $(wildcard $(addsuffix /*.fst,$(SOURCE_DIRS))) \ + + +# This is the only bulletproof way that I know of forcing a regeneration of the +# .depend file every single time. Why, you may ask? Well, it's frequent enough +# to add a new file that you don't want to decipher a cryptic error only to +# remember you should run `make depend`. Also, if you move files around, it's +# good to force regeneration even though .depend may be more recent than the +# mtime of the moved files. +ifndef MAKE_RESTARTS +obj/.depend: .FORCE + mkdir -p obj + $(call run-with-log,\ + $(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@\ + ,[BUNDLE_DEPEND],obj/.depend) + +.PHONY: .FORCE +.FORCE: +endif + +include obj/.depend + +# Verification +# ------------ + +# Everest-specific idiom: all makefiles accept OTHERFLAGS, for instance, if one +# wants to rebuild with OTHERFLAGS="--admit_smt_queries true". We just don't +# pass such flags to the dependency analysis. +FSTAR = $(FSTAR_NO_FLAGS) $(OTHERFLAGS) + +# Creating these directories via a make rule, rather than rely on F* creating +# them, as two calls to F* might race. +obj: + mkdir $@ + +# We allow some specific pattern rules to be added here, relying on the shortest +# stem rule for them to take precedence. For instance, you may want to do: +# +# obj/Bignum.Impl.fst.checked: FSTAR_FLAGS = "--query_stats" +# +# (Note: for options that control the SMT encoding, such as +# --smtencoding.nl_arith_repr native, please make sure you also define them in +# Makefile.common for %.fst-in otherwise you'll observe different behaviors +# between interactive and batch modes.) +# +# By default, however, variables are inherited through the dependencies, meaning +# that the example above would normally set these FSTAR_FLAGS for any .checked +# that is rebuilt because it's a dependency of Bignum.Impl.fst.checked. +# +# To avoid this unpleasant behavior, the most general pattern rule (longest +# stem) also defines a suitable default value for FSTAR_FLAGS. +%.checked: FSTAR_FLAGS= + +# Note: F* will not change the mtime of a checked file if it is +# up-to-date (checksum matches, file unchanged), but this will confuse +# make and result in endless rebuilds. So, we touch that file. +%.checked: | obj + $(call run-with-log,\ + $(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@\ + ,[BUNDLE_VERIFY] $(basename $*),$*) + +# Extraction +# ---------- + +# By default, krml extraction in F* will extract every module into a +# single out.krml file. Make sure to extract the single module we want +# to get a single-properly named file. +.PRECIOUS: obj/%.krml +obj/%.krml: + $(call run-with-log,\ + $(FSTAR) $< --codegen krml \ + --extract_module $(basename $(notdir $(subst .checked,,$<))) \ + -o $@\ + ,[BUNDLE_EXTRACT_KRML] $(basename $*),$*) + +# F* --> C +# -------- + +KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) + +# Note: the implementation of the intrinsic uses external linkage, but you could +# easily turn this file into a .h, use -add-include '"Impl_Bignum_Intrinsics.h"' +# and pass -static-header Impl.Bignum.Intrinsics as described in the +# documentation. +HAND_WRITTEN_C_FILES = + +# This is now the preferred and recommended way to compile C code with KaRaMeL. +# +# KaRaMeL (via -skip-compilation) only generates a stub Makefile in dist/, +# instead of acting as a C compilation driver like it did before. The Makefile +# that is generated by KaRaMeL is basic, but takes into account: +# - the -o option to determine what is being built +# - the C files passed on the command line, which will be linked together +# - C compiler flags passed to KaRaMeL via -ccopts +# +# This Makefile is called Makefile.basic and should be enough for all your basic +# needs. If you need something more fancy, you can easily author your own custom +# dist/Makefile, which includes Makefile.basic, then proceeds to redefine / +# tweak some variables. +# +# Note that you are of course more than welcome to define your own +# CMakeLists.txt or whatever your favorite build system is: this tutorial only +# describes the supported canonical way of compiling code. +# +# See the advanced topics section for an in-depth explanation of how the -bundle +# option works. We also use -minimal. +dist/Derived.h: $(filter-out %prims.krml,$(ALL_KRML_FILES)) + mkdir -p $(dir $@) + $(KRML) -tmpdir $(dir $@) -skip-compilation \ + $(filter %.krml,$^) \ + -warn-error @4@5@18 \ + -record-renamings \ + -fparentheses \ + -bundle 'FStar.*,LowStar.*,Prims[rename=SHOULDNOTBETHERE]' \ + -bundle 'Derived=Base' + ! test -e dist/Base.c + ! test -e dist/SHOULDNOTBETHERE.h + +dist/Derived.o: dist/Derived.h + +$(MAKE) -C $(dir $@) -f Makefile.basic $(notdir $@) + +clean: + rm -rf obj dist *~ + +.PHONY: all clean diff --git a/test/bundle/Makefile.include b/test/bundle/Makefile.include new file mode 100644 index 00000000..d3d6df61 --- /dev/null +++ b/test/bundle/Makefile.include @@ -0,0 +1,39 @@ +# This Makefile may be included from any sub-directory, provided PROJECT_HOME is +# suitably defined, in order to define the %.fst-in and %.fsti-in targets for +# computing the arguments to the interactive mode. + +PROJECT_HOME ?= . + +ifeq (,$(KRML_HOME)) + # assuming test/bundle + KRML_HOME := $(realpath $(CURDIR)/../..) +endif +ifeq ($(OS),Windows_NT) + KRML_HOME := $(shell cygpath -m "$(KRML_HOME)") +endif +export KRML_HOME + +# I prefer to always check all fst files in the source directories; otherwise, +# it's too easy to add a new file only to find out later that it's not being +# checked. Note the usage of PROJECT_HOME +SOURCE_DIRS = $(PROJECT_HOME) + +# We want our source tree on the include path, along with pre-built ulib and +# krmllib so that F* can reuse these build artifacts rather than reverify F* and +# krmllib as part of this build (which would be doomed to fail since there's a +# lot of trickery involved in building ulib -- better leave it up to the F* +# build!). +# +# Also note that we have our own directory on the include path for the sake of +# the interactive mode, for finding checked files for our own F* files. +INCLUDE_DIRS = \ + $(SOURCE_DIRS) \ + $(KRML_HOME)/krmllib \ + $(PROJECT_HOME)/obj + + +FSTAR_INCLUDES = $(addprefix --include ,$(INCLUDE_DIRS)) + +%.fst-in %.fsti-in: + @echo $(FSTAR_INCLUDES) +