create a Rust interface test

test/Makefile

@@ -83,7 +83,7 @@ FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
   --trivial_pre_for_unannotated_effectful_fns false \
   --cmi --warn_error -274
 
-all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test
+all: $(FILES) rust $(WASM_FILES) $(CUSTOM) ctypes-test sepcomp-test rust-val-test
 
 # Needs node
 wasm: $(WASM_FILES)
@@ -266,6 +266,10 @@ sepcomp-test:
 	+$(MAKE) -C sepcomp
 .PHONY: sepcomp-test
 
+rust-val-test:
+	+$(MAKE) -C rust-val
+.PHONY: rust-val-test
+
 CTYPES_HAND_WRITTEN_FILES=Client.ml Makefile
 
 .PHONY: $(LOWLEVEL_DIR)/Client.native

test/rust-val/.gitignore

@@ -0,0 +1,3 @@
+*.exe
+*.krml
+rusttest.rs

test/rust-val/AuxA.fsti

@@ -0,0 +1,4 @@
+module AuxA
+
+val foo : bool -> bool
+

test/rust-val/Makefile

@@ -0,0 +1,65 @@
+RECENT_GCC	= $(shell [ "$$(gcc -dumpversion | cut -c -1)" -ge 5 ] && echo yes)
+
+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
+
+FSTAR_EXE ?= fstar.exe
+
+TEST_OPTS	= -warn-error @4 -verbose -skip-makefiles
+KRML_BIN	= ../../_build/default/src/Karamel.exe
+KRML		= $(KRML_BIN) -fstar $(FSTAR_EXE) $(KOPTS) $(TEST_OPTS)
+CACHE_DIR	= .cache
+FSTAR		= $(FSTAR_EXE) --cache_checked_modules \
+  --cache_dir $(CACHE_DIR) \
+  --include ../../krmllib/compat --include ../../krmllib/obj \
+  --include ../../krmllib --include ../../runtime \
+  --ext context_pruning \
+  --already_cached 'Prims FStar C TestLib Spec.Loops -C.Compat -C.Nullity LowStar WasmSupport' \
+  --trivial_pre_for_unannotated_effectful_fns false \
+  --cmi --warn_error -274
+SED=$(shell which gsed >/dev/null 2>&1 && echo gsed || echo sed)
+
+all: rusttest.rust-test
+
+FSTAR_FILES=$(wildcard *.fst *.fsti)
+
+.PRECIOUS: %.krml
+
+# Use F*'s dependency mechanism and fill out the missing rules.
+
+ifndef MAKE_RESTARTS
+ifndef NODEPEND
+.depend: .FORCE
+	$(FSTAR) --dep full $(FSTAR_FILES) --extract 'krml:*,-Prims' --output_deps_to $@
+
+.PHONY: .FORCE
+.FORCE:
+endif
+endif
+
+include .depend
+
+$(CACHE_DIR)/%.checked: | .depend
+	$(FSTAR) $(OTHERFLAGS) $< && \
+	touch $@
+
+%.krml: | .depend
+	$(FSTAR) $(OTHERFLAGS) --codegen krml \
+	  --extract_module $(basename $(notdir $(subst .checked,,$<))) \
+	  $(notdir $(subst .checked,,$<))
+
+########
+# Rust #
+########
+
+.PRECIOUS: %.rs
+%.rs: $(ALL_KRML_FILES) $(KRML_BIN)
+	$(KRML) -minimal -bundle $(notdir $(subst rust,Rust,$*))=\* \
+	  -backend rust $(EXTRA) -tmpdir $(dir $@) $(filter %.krml,$^)
+	$(SED) -i 's/\(patterns..\)/\1\nmod auxa; mod lowstar { pub mod ignore { pub fn ignore<T>(_x: T) {}}}\n/' $@
+	echo 'fn main () { let r = main_ (); if r != 0 { println!("main_ returned: {}\\n", r); panic!() } }' >> $@
+
+%.rust-test: %.rs
+	rustc $< -o $*.exe && ./$*.exe

test/rust-val/Rusttest.fst

@@ -0,0 +1,22 @@
+module Rusttest
+
+module B = LowStar.Buffer
+module HST = FStar.HyperStack.ST
+module I32 = FStar.Int32
+
+let test2 (b: B.buffer bool) : HST.Stack bool
+  (fun h -> B.live h b /\ B.length b == 1)
+  (fun _ _ _ -> True)
+=
+  let x = B.index b C._zero_for_deref in
+  AuxA.foo x
+
+let main_ () : HST.Stack I32.t
+  (fun _ -> True)
+  (fun _ _ _ -> True)
+= 
+  HST.push_frame ();
+  let b = B.alloca true 1ul in
+  let _ = test2 b in
+  HST.pop_frame ();
+  0l

test/rust-val/auxa.rs

@@ -0,0 +1,10 @@
+#![allow(non_snake_case)]
+#![allow(non_upper_case_globals)]
+#![allow(non_camel_case_types)]
+#![allow(unused_assignments)]
+#![allow(unreachable_patterns)]
+
+pub fn foo(x: bool) -> bool
+{
+    return !x;
+}