From 710346d2efd8020918f38bedc3e1aa7c041d7213 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Wed, 13 Apr 2022 15:33:34 +0200 Subject: [PATCH 1/5] Extract Steel loops --- src/Simplify.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/Simplify.ml b/src/Simplify.ml index 7ac22576e..881514744 100644 --- a/src/Simplify.ml +++ b/src/Simplify.ml @@ -1544,6 +1544,10 @@ let combinators = object(self) when KString.starts_with s "for_loop" -> self#mk_for start finish body K.UInt32 + | EQualified (["Steel"; "Loops"], s), [ start; finish; _inv; { node = EFun (_, body, _); _ } ] + when KString.starts_with s "for_loop" -> + self#mk_for start finish body K.UInt32 + | EQualified ("C" :: (["Loops"]|["Compat";"Loops"]), s), [ _measure; _inv; tcontinue; body; init ] when KString.starts_with s "total_while_gen" -> @@ -1622,6 +1626,13 @@ let combinators = object(self) EWhile (DeBruijn.subst Helpers.eunit 0 (self#visit_expr_w () test), DeBruijn.subst Helpers.eunit 0 (self#visit_expr_w () body)) + | EQualified (["Steel"; "Loops"], s), [ _inv; + { node = EFun (_, test, _); _ }; + { node = EFun (_, body, _); _ } ] + when KString.starts_with s "while_loop" -> + EWhile (DeBruijn.subst Helpers.eunit 0 (self#visit_expr_w () test), + DeBruijn.subst Helpers.eunit 0 (self#visit_expr_w () body)) + | EQualified ("C" :: (["Loops"]|["Compat";"Loops"]), s), [ { node = EFun (_, body, _); _ } ] when KString.starts_with s "do_while" -> EWhile (etrue, with_unit ( From 4af6f8fbe47a273f0e18cbc175121730c9326e10 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 10 May 2022 18:09:01 +0200 Subject: [PATCH 2/5] Add test for Steel loops extraction --- test/SteelLoops.fst | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 test/SteelLoops.fst diff --git a/test/SteelLoops.fst b/test/SteelLoops.fst new file mode 100644 index 000000000..3efe855c2 --- /dev/null +++ b/test/SteelLoops.fst @@ -0,0 +1,28 @@ +module SteelLoops + +open Steel.Effect.Atomic +open Steel.Effect +open Steel.Reference +open Steel.Loops + +let sum_to_n_for (r:ref UInt32.t) : SteelT unit (vptr r) (fun _ -> vptr r) = + for_loop + 0ul + 10ul + (fun _ -> vptr r) + (fun _ -> let x = read r in write r (x `FStar.UInt32.add_mod` 1ul)) + +let sum_to_n_while (r:ref UInt32.t) : SteelT unit (vptr r) (fun _ -> vptr r) = + intro_exists (Ghost.hide true) (fun _ -> vptr r); + while_loop + (fun _ -> vptr r) + (fun _ -> + let _ = witness_exists () in + let n = read r in + FStar.UInt32.lt n 10ul + ) + (fun _ -> + let n = read r in + write r (n `FStar.UInt32.add_mod` 1ul); + intro_exists (Ghost.hide true) (fun _ -> vptr r) + ) From f0e1c3273885e8d83d3af9d459a0004fddbd0216 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 10 May 2022 18:32:03 +0200 Subject: [PATCH 3/5] Update list of filtered Steel krml files --- test/Makefile | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/test/Makefile b/test/Makefile index be4a5900b..f4ee40443 100644 --- a/test/Makefile +++ b/test/Makefile @@ -78,7 +78,15 @@ endif include .depend # AF: The Steel files should not be extracted by KaRaMeL, they are filtered out -FILTERED_KRML_FILES = $(filter-out $(OUTPUT_DIR)/FStar_NMST.krml $(OUTPUT_DIR)/Steel_%.krml,$(ALL_KRML_FILES)) +FILTERED_STEEL_FILES = \ + $(OUTPUT_DIR)/FStar_MSTTotal.krml \ + $(OUTPUT_DIR)/FStar_NMSTTotal.krml \ + $(OUTPUT_DIR)/FStar_NMST.krml \ + $(OUTPUT_DIR)/FStar_MST.krml \ + $(OUTPUT_DIR)/Steel_Effect.krml \ + $(OUTPUT_DIR)/Steel_Effect_Atomic.krml \ + $(OUTPUT_DIR)/Steel_Semantics_Hoare_MST.krml +FILTERED_KRML_FILES = $(filter-out $(FILTERED_STEEL_FILES), $(ALL_KRML_FILES)) $(HINTS_DIR): mkdir -p $@ From 9e45a285125f2615566c22172d849497053248a6 Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 10 May 2022 18:51:52 +0200 Subject: [PATCH 4/5] More Steel krml filtering + add main for SteelLoops --- test/Makefile | 2 ++ test/SteelLoops.fst | 7 +++++++ 2 files changed, 9 insertions(+) diff --git a/test/Makefile b/test/Makefile index f4ee40443..24ce7790a 100644 --- a/test/Makefile +++ b/test/Makefile @@ -85,6 +85,8 @@ FILTERED_STEEL_FILES = \ $(OUTPUT_DIR)/FStar_MST.krml \ $(OUTPUT_DIR)/Steel_Effect.krml \ $(OUTPUT_DIR)/Steel_Effect_Atomic.krml \ + $(OUTPUT_DIR)/Steel_HigherReference.krml \ + $(OUTPUT_DIR)/Steel_Reference.krml \ $(OUTPUT_DIR)/Steel_Semantics_Hoare_MST.krml FILTERED_KRML_FILES = $(filter-out $(FILTERED_STEEL_FILES), $(ALL_KRML_FILES)) diff --git a/test/SteelLoops.fst b/test/SteelLoops.fst index 3efe855c2..83a03c2a5 100644 --- a/test/SteelLoops.fst +++ b/test/SteelLoops.fst @@ -26,3 +26,10 @@ let sum_to_n_while (r:ref UInt32.t) : SteelT unit (vptr r) (fun _ -> vptr r) = write r (n `FStar.UInt32.add_mod` 1ul); intro_exists (Ghost.hide true) (fun _ -> vptr r) ) + +let main () : SteelT Int32.t emp (fun _ -> emp) = + let r = malloc 0ul in + sum_to_n_for r; + sum_to_n_while r; + free r; + return 0l From 2b17f28bfd42e4de6f9db91448ce4e97d03ae5cc Mon Sep 17 00:00:00 2001 From: Aymeric Fromherz Date: Tue, 10 May 2022 23:04:25 +0200 Subject: [PATCH 5/5] More filtering of Steel modules --- test/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Makefile b/test/Makefile index 22185d1b8..f4c0f4396 100644 --- a/test/Makefile +++ b/test/Makefile @@ -69,7 +69,7 @@ ifndef NODEPEND # AF: The Steel files should not be extracted by KaRaMeL, they are filtered out .depend: .FORCE $(FSTAR) --dep full $(subst .wasm-test,.fst,$(WASM_FILES)) $(subst .test,.fst,$(FILES)) \ - $(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims,-FStar.MSTTotal,-FStar.NMSTTotal,-FStar.MST,-FStar.NMST,-Steel' > $@ + $(BROKEN) ../runtime/WasmSupport.fst --extract 'krml:*,-Prims,-FStar.MSTTotal,-FStar.NMSTTotal,-FStar.MST,-FStar.NMST,-Steel.Effect,-Steel.Effect.Atomic,-Steel.HigherReference,-Steel.Reference,-Steel.Semantics.Hoare.MST' > $@ .PHONY: .FORCE .FORCE: