Fix #674

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

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 ]))]

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

test/bundle/.gitignore

@@ -0,0 +1,2 @@
+dist
+obj

test/bundle/Base.fst

@@ -0,0 +1,4 @@
+module Base
+type test = | Foo | Bar
+
+let f (x: Base.test) : Tot bool = Base.Foo? x

test/bundle/Derived.fst

@@ -0,0 +1,3 @@
+module Derived
+
+let g (x: bool) : Tot bool = Base.f Base.Foo = x

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

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)
+