Skip to content

Commit

Permalink
Extraction.Krml: properly detect mem type, it does not have an argument
Browse files Browse the repository at this point in the history
Previous to this patch, extracting this snippet to kmrl:

	module B = LowStar.Buffer
	module HST = FStar.HyperStack.ST
	module U32 = FStar.UInt32

	let test2 (a : B.buffer U32.t) :
	  HST.ST unit
	    (requires fun h -> B.live h a /\ B.freeable a /\ B.length a > 0)
	    (ensures fun _ _ _ -> True)
	=
	  B.upd a 0ul 42ul

Would result in:

	$ fstar.exe Inline.fst --codegen krml --krmloutput x.krml && fstar.exe --read_krml_file x.krml
	[...]
	Inline:
	  DFunction (None, [], 0, TInt UInt32, (["Inline"], "test"), [{name = "a"; typ = TBuf TInt UInt32; mut = false; meta = []}], ELet ({name = "x"; typ = TInt UInt32; mut = false; meta = [CInline]}, EBufRead (EBound 0, EConstant (UInt32, "0")), ESequence [EBufFree EBound 1, EBound 0]))
	  DFunction (None, [], 0, TUnit, (["Inline"], "test2"), [{name = "a"; typ = TBuf TInt UInt32; mut = false; meta = []}], ELet ({name = "h"; typ = TQualified (["FStar", "Monotonic", "HyperStack"], "mem"); mut = false; meta = []}, EUnit, EBufWrite (EBound 1, EConstant (UInt32, "0"), EConstant (UInt32, "42"))))

Note the binding for `h` at type `FStar.Monotonic.HyperStack.mem`,
defined as `EUnit`. This comes from the definition of `upd` as wrapper:

	val upd'
	  (#a:Type0) (#rrel #rel:srel a)
	  (b:mbuffer a rrel rel)
	  (i:U32.t)
	  (v:a)
	  :HST.Stack unit (requires (fun h -> live h b /\ U32.v i < length b /\
					   rel (as_seq h b) (Seq.upd (as_seq h b) (U32.v i) v)))
			  (ensures  (fun h _ h' -> h' == g_upd b (U32.v i) v h))

	inline_for_extraction
	let upd
	  (#a:Type0) (#rrel #rel:srel a)
	  (b:mbuffer a rrel rel)
	  (i:U32.t)
	  (v:a)
	  : HST.Stack unit (requires (fun h -> live h b /\ U32.v i < length b /\
					    rel (as_seq h b) (Seq.upd (as_seq h b) (U32.v i) v)))
			   (ensures (fun h _ h' -> (not (g_is_null b)) /\
						modifies (loc_buffer b) h h' /\
						live h' b /\
						as_seq h' b == Seq.upd (as_seq h b) (U32.v i) v))
	  = let h = HST.get () in
	    upd' b i v;
	    g_upd_seq_as_seq b (Seq.upd (as_seq h b) (U32.v i) v) h

Now, if we try to actually extract C code, it works fine, but apparently
only since karamel knows the definition of the `mem`, since it is in the
krml file, and erases it. Tightening the `--extract` makes it fail with
a type mismatch, and the function is skipped.

	$ rm -f *.checked *.c *.h *.ml && fstar.exe Inline.fst --codegen krml --extract '-*,Inline' && krml Inline.krml -skip-compilation
	Extracted module Inline
	Attempting to translate module Inline
	Verified module: Inline
	All verification conditions discharged successfully
	make: Entering directory '/home/guido/r/gpu/main/karamel'
	dune build
	ln -sf _build/default/src/Karamel.exe krml
	make: Leaving directory '/home/guido/r/gpu/main/karamel'
	Cannot re-check Inline.test2 as valid Low* and will not extract it.  If
	Inline.test2 is not meant to be extracted, consider marking it as Ghost,
	noextract, or using a bundle. If it is meant to be extracted, use -dast
	for further debugging.

	Warning 4: in the definition of h, in top-level declaration
	Inline.test2, in file Inline: Malformed input:
	subtype mismatch:
	  () (a.k.a. ()) vs:
	  FStar_Monotonic_HyperStack_mem (a.k.a. FStar_Monotonic_HyperStack_mem)
	--------------------------------------------------------------------------------

	⚠ [Monomorphization] ⏱️ 2ms
	✔ [Inlining] ⏱️ 2ms
	✔ [Pattern matches compilation] ⏱️ 2ms
	✔ [Structs + Simplify 2] ⏱️ 3ms
	✔ [Drop] ⏱️ <1ms
	✔ [AstToCStar] ⏱️ <1ms
	✔ [CStarToC] ⏱️ <1ms
	⚙ KaRaMeL auto-detecting tools. Here's what we found:
	readlink is: readlink
	KaRaMeL called via: ./karamel/krml
	KaRaMeL home is: /home/guido/r/karamel
	⚙ KaRaMeL will drive F*. Here's what we found:
	read FSTAR_HOME via the environment
	fstar is on branch master
	fstar is: /home/guido/r/fstar/master/bin/fstar.exe
	/home/guido/r/karamel/runtime/WasmSupport.fst
	/home/guido/r/fstar/master/ulib/FStar.UInt128.fst --trace_error
	--expose_interfaces --include /home/guido/r/karamel/krmllib --include
	/home/guido/r/karamel/include
	✔ [PrettyPrinting] ⏱️ 4ms
	KaRaMeL: wrote out .c files for
	KaRaMeL: wrote out .h files for

	$ ls *.c
	ls: cannot access '*.c': No such file or directory
  • Loading branch information
mtzguido committed Sep 9, 2024
1 parent c7a1cf5 commit d1d8633
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
4 changes: 2 additions & 2 deletions ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion src/extraction/FStar.Extraction.Krml.fst
Original file line number Diff line number Diff line change
Expand Up @@ -660,7 +660,7 @@ let rec translate_type_without_decay' env t: typ =
TInt (must (mk_width m))
| MLTY_Named ([], ([ "FStar"; m ], "t'")) when is_machine_int m ->
TInt (must (mk_width m))
| MLTY_Named ([arg], p) when (Syntax.string_of_mlpath p = "FStar.Monotonic.HyperStack.mem") ->
| MLTY_Named ([], p) when (Syntax.string_of_mlpath p = "FStar.Monotonic.HyperStack.mem") ->
TUnit

| MLTY_Named ([_; arg; _], p) when
Expand Down

0 comments on commit d1d8633

Please sign in to comment.