Local references in Steel.ST #2664

tahina-pro · 2022-07-27T22:13:24Z

This PR proposes a lexical Steel.ST combinator to handle references local to a code block, and provides its extraction to C via Karamel: for any initial value init and any code block body, Steel.ST.Reference.with_local init body will "stack-allocate" a local variable, initialize it with init, and execute body with that local variable in scope. Thus, this combinator enables lexical handling of local mutable variables in Steel.ST.

Specification

The Steel.ST signature of this combinator:

val with_local
  (#t: Type) (init: t)
  (#pre: vprop) (#ret_t: Type) (#post: ret_t -> vprop)
  (body: (r: ref t) -> STT ret_t
    (pts_to r full_perm init `star` pre)
    (fun v -> exists_ (pts_to r full_perm) `star` post v))
: STF ret_t pre post True (fun _ -> True)

with_local is declared in effect STF instead of ST, so that the pre- and post-resources can be properly inferred by the Steel tactic from the caller's context.

An example of use in EverParse's ongoing Steel experiment, where I managed to seamlessly replace explicit alloc/free with with_local in complex loops going through binary representations of lists (project-everest/everparse@85bd4f0): no additional proof annotation required!

Extraction

Following a suggestion by @msprotz, I manage to extract this combinator to Karamel as:

EPushFrame;
let r = EBufCreate init 1 in
let res = body r in
EPopFrame;
res

To do that, I had to define 3 local primitives in Steel.ST.Reference.fst to be extracted to EPushFrame, EBufCreate and EPopFrame. Since these local primitives are in the .fst, they are hidden behind the interface and so they will not be used directly by users, only by the implementation of with_local. Thus, I can mark the latter inline_for_extraction and benefit from cross-module inlining.

Thus, with_local init body is extracted to C as:

ret_t res;
{
  t r = init;
  res = <body r>;
}

In the EverParse example mentioned above, here is the diff to the corresponding extracted code, where arrays allocated with KRML_HOST_CALLOC are replaced with local variables: tahina-pro/quackyducky@7552898

(FWIW, this PR also provides a similar combinator for ghost local variables, Steel.ST.GhostReference.with_local, but this one does not need any additional primitives for extraction.)

For now this PR handles local references only: no arrays yet. We would extend to arrays only once the design of this PR is validated and it is merged.

aseemr · 2022-07-28T07:06:59Z

Thanks @tahina-pro, this looks great! A few comments:

You could use this combinator to make this a stack allocation?
I did not understand the reasoning of having with_locals in STF ... does it mean that pre and post of with_locals have to match the context, and we can't frame with_locals? (Sorry I haven't seen these effects in a long time, so my question may sound naïve.)
What about variants for working with 2, 3, ... locals? with_locals2, with_locals3, or some funky generic programming (if possible?)?

tahina-pro · 2022-07-28T15:36:51Z

Thank you Aseem for your feedback!

You could use this combinator to make this a stack allocation?

Thank you for your suggestion! Yes, this is exactly the pattern with_local is meant to handle, so if anyone finds any similar pattern in the Steel.ST library, please feel free to point it out here.

I did not understand the reasoning of having with_locals in STF ... does it mean that pre and post of with_locals have to match the context, and we can't frame with_locals? (Sorry I haven't seen these effects in a long time, so my question may sound naïve.)

Yes, that's how I understand effects named SteelF, STF, etc. Of course, anyone please correct us if we are wrong. Then, of course users can still frame inside of the body passed to with_local.

What about variants for working with 2, 3, ... locals? with_locals2, with_locals3, or some funky generic programming (if possible?)?

In general, you can nest with_local as deeply as you want: you would have with_local init1 (fun v1 -> with_local init2 (fun v2 -> ...)) So if you want, I can define inline_for_extraction with_locals2 as nesting of 2 with_local, etc. For more generic programming, we would need a heterogeneous list to initialize locals of different types, and we would need normalization to kick in properly.

…eel_st_with_local

cf. #2664 (comment)

aseemr · 2022-07-29T05:53:06Z

But why not have with_local in ST, rather than STF so that it can be framed outside by the tactic as usual? Wouldn't it be desirable to write a small-footprint spec for the body?

aseemr · 2022-07-29T05:53:49Z

(And for this repeat_until, we should be able to see the extraction at work in the Zeta code.)

tahina-pro · 2022-07-29T14:00:53Z

But why not have with_local in ST, rather than STF so that it can be framed outside by the tactic as usual? Wouldn't it be desirable to write a small-footprint spec for the body?

ST does not work, in particular if the body is using gen_elim (). The EverParse list example (https://github.com/tahina-pro/quackyducky/blob/7552898b3fe2999b64e9bed70f83e944ea2cec54/src/lowparse/LowParse.SteelST.List.fst#L419 ) succeeds with STF, but fails with ST:

proof-state: State dump @ depth 1 (at the time of failure):
Location: /home/tahina/everest/master/FStar/ulib/experimental/Steel.Effect.Common.fsti(2931,4-2932,63)
Goal 1/22 (Instantiating meta argument in application):
(k: LowParse.Spec.Base.parser_kind), (t: Type), (p: LowParse.Spec.Base.parser k t), (v: LowParse.SteelST.Validate.validator p), (va0: LowParse.SteelST.ArrayPtr.v LowParse.Bytes.byte), (a0: LowParse.SteelST.Parse.byte_array), (len0: LowParse.Steel.StdInt.size_t), (err: Steel.ST.Reference.ref FStar.UInt32.t), (_: Prims.unit), (plen: Steel.ST.Reference.ref LowParse.Steel.StdInt.size_t), (_: FStar.Ghost.erased (LowParse.SteelST.ArrayPtr.t LowParse.Bytes.byte)) |- _ : Prims.squash (Steel.ST.GenElim.Base.gen_elim_prop_placeholder true
      ((*?u1219*) _ _)
      (*?u51*)
      _
      (*?u52*)
      _
      (*?u1216*)
      _)
...
LowParse.SteelST.List.fst(419,10-419,18): (Error 228) user tactic failed: `Could not make progress, no solvable goal found`
1 error was reported (see above)

I suspect the frame is not yet determined by the time gen_elim is being solved.

…eel_st_with_local

tahina-pro · 2022-08-03T16:44:57Z

Following our discussion last week, Jonathan told me we shouldn't need push_frame and pop_frame at all, as soon as we could disable some pass in Karamel, except maybe in some cases related to Karamel hoisting a local variable declaration from within a nested if branch up to the beginning of a function. So, I propose to first merge this PR now as is, and then later, try out a version without push_frame and pop_frame, maybe with some changes in Karamel. @msprotz What do you think?

msprotz · 2022-08-03T16:54:40Z

That sounds good. Here is an untested patch if you want to try without push/pop right away:

diff --git a/src/Karamel.ml b/src/Karamel.ml
index 07c782df..ccd52f60 100644
--- a/src/Karamel.ml
+++ b/src/Karamel.ml
@@ -493,6 +493,7 @@ Supported options:|}
   (* Empty file generated by F*, we provide the missing bits in src/Builtin.ml *)
   let filenames = List.filter (fun f -> Filename.basename f <> "prims.krml") filenames in
   let files = InputAst.read_files filenames in
+  let no_lowstar = List.for_all(fun f -> not (KString.starts_with f "LowStar")) filenames in
 
   (* -djson *)
   if !arg_print_json then
@@ -625,7 +626,7 @@ Supported options:|}
   (* Note: generates let-bindings, so needs to be before simplify2 *)
   let files = Simplify.remove_unused files in
   let files = if !Options.tail_calls then Simplify.tail_calls files else files in
-  let files = Simplify.simplify2 files in
+  let files = Simplify.simplify2 ~no_lowstar files in
   let files = if Options.(!merge_variables <> No) then SimplifyMerge.simplify files else files in
   if !arg_print_structs then
     print PrintAst.print_files files;
diff --git a/src/Simplify.ml b/src/Simplify.ml
index 04977ae2..541edd42 100644
--- a/src/Simplify.ml
+++ b/src/Simplify.ml
@@ -1705,7 +1705,7 @@ let simplify1 (files: file list): file list =
  * allocations and writes are hoisted; where if-then-else is always in statement
  * position; where sequences are not nested. These series of transformations
  * re-establish this invariant. *)
-let simplify2 (files: file list): file list =
+let simplify2 ~no_lowstar (files: file list): file list =
   let files = sequence_to_let#visit_files () files in
   (* Quality of hoisting is WIDELY improved if we remove un-necessary
    * let-bindings. *)
@@ -1713,7 +1713,7 @@ let simplify2 (files: file list): file list =
   let files = if !Options.wasm then files else fixup_while_tests#visit_files () files in
   let files = hoist#visit_files [] files in
   let files = if !Options.c89_scope then SimplifyC89.hoist_lets#visit_files (ref []) files else files in
-  let files = if !Options.wasm then files else hoist_bufcreate#visit_files () files in
+  let files = if !Options.wasm || no_lowstar then files else hoist_bufcreate#visit_files () files in
   let files = if !Options.wasm then files else fixup_hoist#visit_files () files in
   let files = if !Options.wasm then files else let_if_to_assign#visit_files () files in
   let files = misc_cosmetic#visit_files () files in

tahina-pro · 2022-08-03T17:34:56Z

Thanks Jonathan! I'll merge this PR now and I'll open a follow-up issue on Karamel.

cf. FStarLang/FStar#2664 (comment)

tahina-pro added 3 commits July 27, 2022 11:44

Steel.ST.(Ghost)Reference.with_local

ccc334c

local primitives extracting to krml's EPushFrame, EPopFrame

015154e

snap

e6104db

tahina-pro added the Steel Issues related to a Concurrent Resource Typing label Jul 27, 2022

tahina-pro requested review from aseemr, nikswamy, R1kM and msprotz July 27, 2022 22:13

Merge branch 'master' into _taramana_steel_st_with_local

c486f27

tahina-pro added 2 commits July 28, 2022 08:39

Merge branch 'master' of github.com:FStarLang/FStar into _taramana_st…

99777b7

…eel_st_with_local

handle local in repeat_until (suggested by @aseemr)

4adaafe

cf. #2664 (comment)

tahina-pro added 3 commits August 1, 2022 16:53

Merge branch 'master' of github.com:FStarLang/FStar into _taramana_st…

6d06290

…eel_st_with_local

with_named_local, to set the name of the local in the extracted C code

f742831

Merge branch 'master' of github.com:FStarLang/FStar into _taramana_st…

edd08f2

…eel_st_with_local

tahina-pro merged commit 36103a9 into master Aug 3, 2022

tahina-pro mentioned this pull request Aug 3, 2022

Simplify Steel.ST.Reference.with_local without EPushFrame/EPopFrame FStarLang/karamel#276

Open

tahina-pro deleted the _taramana_steel_st_with_local branch August 8, 2022 15:46

tahina-pro added a commit to FStarLang/steel that referenced this pull request May 23, 2023

handle local in repeat_until (suggested by @aseemr)

2a44e26

cf. FStarLang/FStar#2664 (comment)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Local references in Steel.ST #2664

Local references in Steel.ST #2664

tahina-pro commented Jul 27, 2022

aseemr commented Jul 28, 2022

tahina-pro commented Jul 28, 2022 •

edited

Loading

aseemr commented Jul 29, 2022

aseemr commented Jul 29, 2022

tahina-pro commented Jul 29, 2022 •

edited

Loading

tahina-pro commented Aug 3, 2022

msprotz commented Aug 3, 2022

tahina-pro commented Aug 3, 2022 •

edited

Loading

Local references in Steel.ST #2664

Local references in Steel.ST #2664

Conversation

tahina-pro commented Jul 27, 2022

Specification

Extraction

aseemr commented Jul 28, 2022

tahina-pro commented Jul 28, 2022 • edited Loading

aseemr commented Jul 29, 2022

aseemr commented Jul 29, 2022

tahina-pro commented Jul 29, 2022 • edited Loading

tahina-pro commented Aug 3, 2022

msprotz commented Aug 3, 2022

tahina-pro commented Aug 3, 2022 • edited Loading

tahina-pro commented Jul 28, 2022 •

edited

Loading

tahina-pro commented Jul 29, 2022 •

edited

Loading

tahina-pro commented Aug 3, 2022 •

edited

Loading