From b9cadbb3c865be6da32962b617fb29b55e5cec80 Mon Sep 17 00:00:00 2001 From: gebnermsft Date: Fri, 18 Sep 2026 23:43:27 +0000 Subject: [PATCH] Custard: fold projections of a let-bound constructor Fixes #4548. `let (a, (b, _)) = p` in an inlined callee left the caller building a tuple, naming it and reading it back out. The rewrites were already there -- `iota` on a `match` over a constructor, `unbuild` on a projection out of one -- but F* puts a binding in front of the scrutinee, so neither ever sees a constructor. `reduce` now substitutes a let-bound constructor when every occurrence is destructed on the spot and every field is `reeval`; `unbuild` does the same for the projection-only shape that `depat` leaves behind. `reeval` is bounded, allocation-free and safe to repeat: variables, constants, projections, casts, operators, and constructors over them. A call or an allocation keeps its binding. Documented in section 129. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- doc/ref/custard.md | 105 +++++++++++++++ src/custard/FStarC.Custard.Simplify.fst | 162 ++++++++++++++++++++++-- tests/custard/pulse/LetPatFold.fst | 36 ++++++ tests/custard/pulse/Makefile | 11 ++ 4 files changed, 300 insertions(+), 14 deletions(-) create mode 100644 tests/custard/pulse/LetPatFold.fst diff --git a/doc/ref/custard.md b/doc/ref/custard.md index 3119bafadfa..64a43010487 100644 --- a/doc/ref/custard.md +++ b/doc/ref/custard.md @@ -22157,6 +22157,110 @@ be on the include path of the generated module that names it. `quicksort` also loses the three erased arguments the old driver had to pass, which is the shape §127 was about seen from the other end. +## 129 A constructor that is built to be taken apart + +FStarLang/FStar#4548, reported against a generated file that is meant to +be read. `let (a, (b, _)) = p` in an `inline_for_extraction` callee, and +a caller that builds the tuple: + +```fstar +inline_for_extraction +fn body (p : U32.t & (U32.t & unit)) ... { let (a, (b, _)) = p; U32.add_mod a b } + +fn entry (x : U32.t) ... { body (x, (U32.add_mod x 1ul, ())) } +``` + +came out as + +```c +uint32_t LetPatFold_entry(uint32_t x) { + FStar_Pervasives_Native_tuple2__uint32_tuple2_uint32_unit _letpattern = + (FStar_Pervasives_Native_tuple2__uint32_tuple2_uint32_unit){ + ._1 = x, + ._2 = (FStar_Pervasives_Native_tuple2__uint32_unit){ ._1 = (x + 1) } }; + return (_letpattern._1 + _letpattern._2._1); +} +``` + +where `return (x + (x + 1));` will do. The reporter's numbers are the +reason it matters: across 68 extracted units, 411 such handle bindings, +1113 one-field temporaries and 212 `_letpattern` bindings, in 15 files. +The cost is zero --- they hand-flattened sixteen CUDA kernels and the PTX +was byte-identical --- so this is readability, and readability is the +point of those files. + +### 129.1 The rule that was there, and the binding in front of it + +Custard *does* reduce a `match` on a constructor: `reduce`'s `iota` fires +whenever the scrutinee is one, and `unbuild` does the same for a +projection out of one. Both were in place, and the inlining that the +report notes had already happened --- `body` was inlined and its +projections pushed into the caller. + +What stops them is the binding. F\* compiles `let (a, b) = p` by naming +the scrutinee: `let _letpattern = in match _letpattern with ...`. So +the scrutinee `iota` sees is an `EVar`, never a constructor, and the +rewrite that would fire one step later never gets the chance. + +`reduce`'s `ELet` case now substitutes the constructor into the body, +under two conditions: + +* every occurrence of the variable is *destructed on the spot* --- the + scrutinee of a `match`, or the target of a projection + (`destructed_only`). This is what says the tuple is never used as a + value, so no copy of it survives the substitution; +* every field is `reeval`. + +`unbuild` gained the same case for the projection-only shape, which is +what a `match` turns into once `depat` has run --- past `reduce`, so the +two have to be separate. There the substitution is `psub`, which does +not rename, so the case additionally asks that the body does not rebind +the name. + +### 129.2 `reeval` + +The report's own caveat is the right one: the fold is sound only when the +constructor's *other* arguments can be dropped, since the branch or the +projection discards them. That is purity, and it is the condition +`ctor_args_pure` already asks of a scrutinee that is a constructor +already. + +There is a second condition the immediate case does not need. A field +that *is* read moves to where it is read, and there may be more than one +such place --- so the fold may repeat it, and, worse, may move it into a +loop. `reeval` is that question: variables, constants, projections, +casts, coercions, tag reads and `EOp` applications over them. Bounded, +allocating nothing, and no more expensive to repeat than their operands, +which is `cheap_expr`'s own wording for the same class. A call or an +allocation is *not* in it, and keeps its binding. + +Constructors are in it, which is not a widening for its own sake: the +nested tuple is exactly what `let (a, (b, _)) = p` destructures, and +without it the rule does not fire on the shape it was written for. In C +a constructor is a compound literal and allocates nothing (§103); in +OCaml it would allocate, but the predicate is only ever asked about a +value whose every copy is about to be taken apart again. + +An effectful field never reaches the question, because ANF has already +lifted it into a binding of its own, and the fold moves that binding +nowhere. + +### 129.3 What it does not do + +The report separates the one-field structs that a `unit` tail leaves --- +`{._1 = tmp3}` is `Mktuple2 (tmp3, ())` after the layout pass erases the +unit field --- and asks for them only as a consequence, not as a target. +That is what happens: folding the projections makes those bindings dead +and they disappear, **and no declared type changes**. The one-field +struct is still declared, and a header that is an interface still spells +it. Collapsing the struct itself would be a different and much more +invasive change, and is not done here. + +`tests/custard/pulse/LetPatFold.fst` pins both halves: `body` is a root +of its own, so the tuple type is declared and the test can check that it +still is, while `entry` compiles to `return (x + (x + 1));` and the word +`_letpattern` does not appear. + | M | Deliverable | Notes | | --- | --- | --- | | M0 | `src/custard/` skeleton, `--codegen Custard`, `--custard_entry`, IR types, IR pretty-printer | No extraction yet; `--custard_dump_ir` on an empty program | @@ -22516,3 +22620,4 @@ pass, which is the shape §127 was about seen from the other end. | M10κΙ | **Three test suites the migration broke** (§126.6–§126.8) | Done. CI ran what the local gate had not. `examples/printf` was two coercion bugs in one program: a lambda binder whose type is exactly `TAny` bound nothing, so no use of it was coerced and OCaml inferred a type from the first `match` branch that the second contradicted; and a call that over-applies a head returning `TAny` was coerced only when the expected type was known, so the same call `let`-bound went out with three arguments to a two-argument function. `tests/floats/Test01` loses its `Float32` half, which Custard refuses on OCaml by design (§66.4) and the legacy backend emulated; the coverage moves to `FloatExtract` and `tests/custard/Floats.fst`. `fsharp/tests/{Hello,Test00}` drop their hand-written projects for the one Custard generates, and grow a `main`: .NET has no load-time execution, so a module whose top-level effect prints is a program on OCaml and a library that does nothing on F# | | M10κΚ | **A partial application that became a saturated one** (§127) | Done. The defect that kept `pulse/test/pool` on the old pipeline. `fork_core (f1 ())` passes a thunk, `f1` having two binders and the call supplying one; erasing the second --- a proof-level `loc_id` --- made the call saturated, so the worker loop ran inline in the spawning thread instead of being forked. `Mono.keep_thunk` is the rule for exactly this and its comment already named the hazard, but its second clause asked whether the last binder was *unit-shaped* rather than whether the codomain was impure. It now asks the second, in Custard's sense of impure rather than F*'s (`Mono.impure_codomain`, since a Pulse `fn` is a `Tot` function returning an `stt`), and `Extract`'s `Tm_abs` guard gained the same clause off `body.eff`. Restricted to an *explicit* last binder, because F* instantiates an implicit at every application, so no partial application stops in front of one --- and keeping one gave §80.1's record field an arity its derived projector could not meet. The mirror miscount is fixed alongside: a call through a *variable* deleted the argument for the binder `keep_thunk` had just put back, and now passes `()` for it as a call through a name always did. The cost is a `unit` parameter on a definition whose last binder is erased in front of an impure codomain, which is what the legacy backend keeps anyway | | M10κΛ | **A module that must never be compiled** (§128) | Done. `Pulse.Lib.SpinLock`'s `acquire` loops on a `cas` that is a *specification* --- a read then a write, atomic in Pulse and two accesses once compiled --- so Custard's compiled spin lock locked nothing and the pool example's quicksort raced. The answer is the mechanism §8.2 already had: the module joins `Builtins.realized_modules`, its values become externals under the names the hand-written `Pulse_Lib_SpinLock.ml` and `.c` already use, and nothing of it is compiled. Two defects were hiding behind it. `external_ty` built an external's signature without `keep_thunk`, so `new_lock`, whose one binder is erased, was declared a *value* while every call site emitted `new_lock ()` (§128.1). And `Realized` means hand-written *OCaml*, so the C backends kept the F\* shape --- right for `Prims.list`, and for a lock a `struct { uint32_t *r; }` beside a realization whose header says `pthread_mutex_t *`; `Builtins.c_realized_modules` is the second table, and makes such a type an `Extern` carrying its header (§128.2). The DICE build, the only Custard C build with `-Werror`, also caught §116's overflow guard comparing a `uint32_t` length against `SIZE_MAX`, which `-Wtype-limits` calls always false: the length now goes through a `size_t` temporary, which keeps the check real on a 32-bit target (§128.3). `pulse/test/pool/pulse_task` moves to Custard on top of it and gets shorter: one extraction from one entry point, `fstar.exe --ocamlopt` to link, no `dune` project, no local `Prims.ml` and no `sed` over the output (§128.5) | +| M10κΜ | **A constructor that is built to be taken apart** (§129) | Done. FStarLang/FStar#4548. `let (a, (b, _)) = p` in an inlined callee left the caller building a tuple, naming it and reading it back out; `return (x + (x + 1));` is what it should be, and across the reporter's 68 units there were 411 such bindings. The rewrites were all in place --- `iota` on a `match` over a constructor, `unbuild` on a projection out of one --- and what stopped them was the *binding* F\* puts in front: `let _letpattern = e in match _letpattern with ...`, so the scrutinee `iota` sees is an `EVar`. `reduce` now substitutes a let-bound constructor when every occurrence is destructed on the spot and every field is `reeval`, and `unbuild` does the same for the projection-only shape `depat` leaves behind. `reeval` is the second condition the immediate case never needed: a field that is read *moves*, possibly into a loop and possibly more than once, so it is restricted to the class §103 already calls bounded and allocation-free --- variables, constants, projections, casts, operators, and constructors over them. A call or an allocation keeps its binding, which is the report's own caveat about discarded components. No declared type changes: the one-field struct a `unit` tail leaves is still declared, it is just no longer built | diff --git a/src/custard/FStarC.Custard.Simplify.fst b/src/custard/FStarC.Custard.Simplify.fst index f1f27d897e1..a7bbada54bd 100644 --- a/src/custard/FStarC.Custard.Simplify.fst +++ b/src/custard/FStarC.Custard.Simplify.fst @@ -789,6 +789,58 @@ let forwarder_table (prog:program) : ML (SMap.t (int & int)) = | _ -> ()); t +(* Section 129. May this expression be moved to the places a field of it is + read, however many there are? {!dup_ok} is the same question for a value + that is already a variable or a projection; this widens it by the class + {!cheap_expr}'s comment calls the same class of work as the [ECast] beside + it -- bounded, allocating nothing, and no more expensive to repeat than its + operands. A call or an allocation is *not* in it: re-evaluating one costs, + and moving one into a loop costs a great deal. Purity is required on top, + because the fields that are never read disappear. *) +let rec reeval (e:expr) : ML bool = + is_pure e.eff && + (match e.e with + | EVar _ | EConst _ | EQual _ -> true + | EProj (a, _, _) -> reeval a + | EDiscrim (a, _) -> reeval a + | ECast (a, _) -> reeval a + | ECoerce (a, _) -> reeval a + | EOp (_, es) -> es |> List.for_all reeval + (* A constructor of [reeval] fields is in the class too, by section 103's + argument for {!cheap_expr}: in C it is a compound literal and allocates + nothing. In OCaml it would allocate, but only if it survived, and the + only reason this predicate is asked is that every copy is about to be + taken apart again. It has to be here, because a nested tuple is exactly + what [let (a, (b, _)) = p] destructures. *) + | ECtor (_, es) -> es |> List.for_all reeval + | ETuple es -> es |> List.for_all reeval + | ERecord (_, fs) -> fs |> List.for_all (fun (_, (e:expr)) -> reeval e) + | _ -> false) + +(* An [EProj] out of a value that is right there. The rewrites below leave one + behind wherever a field had to be put back together, and this is what makes + the reconstruction cost nothing in the case that matters -- a projection out + of a field that was itself projected out. *) +(* Section 129. Is every occurrence of [v] taken apart on the spot: the + scrutinee of a [match], or the target of a projection? Then a constructor + bound to [v] may be substituted for it, because [iota] above and + {!unbuild} below take every copy apart again and none of them is ever + built. *) +let rec destructed_only (v:string) (x:expr) : ML bool = + let g = destructed_only v in + let scrut (s:expr) : ML bool = + match s.e with EVar w -> w = v | _ -> g s in + let brs_ok (brs:list branch) : ML bool = + brs |> List.for_all (fun (b:branch) -> + let _, gd, bd = b in + (match gd with Some gd -> g gd | None -> true) && g bd) in + match x.e with + | EVar w -> w <> v + | EProj (e1, _, _) -> (match e1.e with EVar w -> w = v || g e1 | _ -> g e1) + | EMatch (s, brs) -> scrut s && brs_ok brs + | ETry (s, brs) -> g s && brs_ok brs + | _ -> for_all_children g x + let rec reduce (x:expr) : ML expr = match x.e with | EApp (h, args) -> @@ -845,6 +897,27 @@ let rec reduce (x:expr) : ML expr = let sm : subst = SMap.create 5 in SMap.add sm v e1; reduce (sub sm e2) + (* Section 129. A constructor that is bound and then only ever taken + apart. [let (a, b) = p] is exactly this shape --- F* binds the + scrutinee to [_letpattern] and matches it --- and so is any caller that + builds a tuple for an [inline_for_extraction] callee which destructures + it. The binding stops [iota] from ever seeing a constructor, so the + tuple is built, named and read back out in the generated code. + + Substituting it is sound because every field is [reeval]: the ones a + branch keeps may be moved and repeated, and the ones it discards are + pure and so may be dropped --- which is the same pair of conditions + [ctor_args_pure] asks of a scrutinee that is a constructor already. + [sub] renames as it goes, so a binder of the same name inside [e2] + cannot capture. *) + else if (match e1.e with + | ECtor (_, es) | ETuple es -> es |> List.for_all reeval + | ERecord (_, fs) -> fs |> List.for_all (fun (_, (e:expr)) -> reeval e) + | _ -> false) + && destructed_only v e2 then + let sm : subst = SMap.create 5 in + SMap.add sm v e1; + reduce (sub sm e2) else { x with e = ELet (v, ty, e1, reduce e2) } | _ -> map_children reduce x @@ -2331,10 +2404,40 @@ let ex_take (ex:expansion) (e:expr) : ML (option (list expr)) = let strip_inline (c:cty) : cty = match c with TInline c -> c | c -> c -(* An [EProj] out of a value that is right there. The rewrites below leave one - behind wherever a field had to be put back together, and this is what makes - the reconstruction cost nothing in the case that matters -- a projection out - of a field that was itself projected out. *) +(* Is every occurrence of [v] the target of a projection? Then a record built + out of pieces can be substituted for it however many times it is used: + [unbuild] takes every copy apart again and none of them is ever built. *) +let rec only_projected (v:string) (x:expr) : ML bool = + let g = only_projected v in + match x.e with + | EVar w -> w <> v + | EProj (e1, _, _) -> (match e1.e with EVar w -> w = v || g e1 | _ -> g e1) + | _ -> for_all_children g x + +(* Section 129. Does [x] bind [v] again anywhere inside it? Substituting + through a binder of the same name would capture, and {!psub} deliberately + does not rename. The four binding forms are the ones {!lift_lambdas} + lists. *) +let rec rebinds (v:string) (x:expr) : ML bool = + let g = rebinds v in + let rec pv (p:pat) : ML bool = + match p with + | PVar w -> w = v + | PCtor (_, ps) -> ps |> List.existsb pv + | PTuple ps -> ps |> List.existsb pv + | POr ps -> ps |> List.existsb pv + | PRecord (_, fs) -> fs |> List.existsb (fun (_, q) -> pv q) + | _ -> false in + let br (r:branch) : ML bool = + let p, gd, b = r in + pv p || (match gd with Some gd -> g gd | None -> false) || g b in + match x.e with + | ELet (w, _, e1, e2) -> w = v || g e1 || g e2 + | EFun (bs, b) -> (bs |> List.existsb (fun (b:binder) -> b.b_name = v)) || g b + | EMatch (sc, brs) -> g sc || (brs |> List.existsb br) + | ETry (a, brs) -> g a || (brs |> List.existsb br) + | _ -> exists_child g x + let rec unbuild (infos:SMap.t ctor_info) (x:expr) : ML expr = let g = unbuild infos in let pick (fs:list (string & expr)) (f:string) : ML (option expr) = @@ -2358,17 +2461,48 @@ let rec unbuild (infos:SMap.t ctor_info) (x:expr) : ML expr = | None -> alt) | None -> alt) | _ -> alt) - | _ -> map_children g x -(* Is every occurrence of [v] the target of a projection? Then a record built - out of pieces can be substituted for it however many times it is used: - [unbuild] takes every copy apart again and none of them is ever built. *) -let rec only_projected (v:string) (x:expr) : ML bool = - let g = only_projected v in - match x.e with - | EVar w -> w <> v - | EProj (e1, _, _) -> (match e1.e with EVar w -> w = v || g e1 | _ -> g e1) - | _ -> for_all_children g x + (* Section 129. The same fold one binding away: a constructor that is + let-bound and then only ever projected out of. F*'s [let (a, b) = p] + compiles to exactly this, and so does any caller that builds a tuple for + an [inline_for_extraction] callee which immediately takes it apart --- the + projections have already been pushed into the caller by then, and what is + left is a named temporary that nothing else reads. + + Substituting the constructor at each projection is sound because every + field is [reeval]: the ones that are read may be moved and repeated, and + the ones that are not are pure and so may be dropped. A field that is a + call or an allocation keeps the binding, which is the distinction the + discarded-read deletion of section 99 draws as well. + + The [let] itself is then simply gone: [only_projected] says the variable + has no other reader. Nothing here changes a declared type --- a one-field + struct behind an erased [unit] tail is still declared, it is just no + longer built. *) + | ELet (v, t, rhs, b) -> + let rhs = g rhs in + let b = g b in + let alt = { x with e = ELet (v, t, rhs, b) } in + let fields = + match rhs.e with + | ERecord (_, fs) -> Some fs + | ECtor (cn, es) -> + (match SMap.try_find infos (string_of_name cn) with + | Some ci -> + if List.length es = List.length ci.ci_fields + then Some (List.zip (ci.ci_fields |> List.map fst) es) + else None + | None -> None) + | _ -> None in + (match fields with + | Some fs when (fs |> List.for_all (fun (_, (e:expr)) -> reeval e)) + && only_projected v b && not (rebinds v b) -> + let sm : subst = SMap.create 1 in + SMap.add sm v rhs; + g (psub sm b) + | _ -> alt) + + | _ -> map_children g x let inline_fields (vd:verdicts) (prog:program) : ML program = if SMap.keys vd.vd_plans = [] then prog else begin diff --git a/tests/custard/pulse/LetPatFold.fst b/tests/custard/pulse/LetPatFold.fst new file mode 100644 index 00000000000..259726c076b --- /dev/null +++ b/tests/custard/pulse/LetPatFold.fst @@ -0,0 +1,36 @@ +module LetPatFold +#lang-pulse +open Pulse +module U32 = FStar.UInt32 +module SZ = FStar.SizeT + +(* Section 129. [let (a, (b, _)) = p] binds the scrutinee to [_letpattern] + and matches it, so a caller that builds the tuple for an + [inline_for_extraction] callee that immediately takes it apart used to + build it, name it and read it back out. The tuple here is the shape a + type-level fold over a list produces: a [unit] tail, and one pair per + element. *) + +inline_for_extraction +fn body (p : U32.t & (U32.t & unit)) + requires emp + returns _:U32.t + ensures emp +{ + let (a, (b, _)) = p; + U32.add_mod a b +} + +fn entry (x:U32.t) + requires emp + returns _:U32.t + ensures emp +{ + body (x, (U32.add_mod x 1ul, ())) +} + +fn main () returns r:SZ.t +{ + let k = entry 3ul; + if (k = 7ul) { 0sz } else { 1sz } +} diff --git a/tests/custard/pulse/Makefile b/tests/custard/pulse/Makefile index 08bfad22283..ab0973ea4c1 100644 --- a/tests/custard/pulse/Makefile +++ b/tests/custard/pulse/Makefile @@ -360,6 +360,17 @@ CGREP_ExtBuf = "(uint8_t *)extbuf_base" # would emit a (void) cast, which C++ accepts with or without the fix. CGREP_ExtBuf += "uint8_t *" +# Section 129. A constructor that is bound and then only ever taken apart. +C_TESTS += LetPatFold +# [body] is a root of its own so that the tuple type is *declared*: folding +# the projections changes no declared type, which is what makes the rewrite +# safe for a unit whose header is an interface. +EXTRA_LetPatFold = --custard_entry LetPatFold.body +CGREP_LetPatFold += "FStar_Pervasives_Native_tuple2__uint32_tuple2_uint32_unit p" +# [entry] is the point: the tuple it builds for [body] is never built. +CGREP_LetPatFold += "return (x + (x + 1));" +CNOGREP_LetPatFold += "_letpattern" + # Section 116. [len * sizeof(elt)] is computed in size_t and wraps; the # guard is what stops malloc from succeeding with a block too small for the # fill loop that follows it. A constant length needs none -- [main] allocates