diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c9b5c3d8..2204ddfc 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1609,9 +1609,21 @@ jobs: # had to pass. When it was finally run on 2026-09-24 it was RED: # int_width_boundary, added to the parity suite for a different question, # differs by construction on a 32-bit target. - - name: rv_exec (the RISC-V backend against the C backend, hosted side) + - name: rv_exec_partition (all-mode and CI partition invocations agree) + if: ${{ !cancelled() && matrix.group == 'containers' }} + run: python3 scripts/rv_exec_partition_check.py + + - name: rv_exec contracts (hosted boundaries at both widths) if: ${{ !cancelled() && matrix.group == 'riscv' }} - run: MEMU="$RUNNER_TEMP/downstream/memu" sh scripts/rv_exec_check.sh + run: MEMU="$RUNNER_TEMP/downstream/memu" sh scripts/rv_exec_check.sh --contracts + + - name: rv_exec corpus32 (the full corpus against C) + if: ${{ !cancelled() && matrix.group == 'coroutines' }} + run: MEMU="$RUNNER_TEMP/downstream/memu" sh scripts/rv_exec_check.sh --corpus32 + + - name: rv_exec corpus64 (the full corpus against C) + if: ${{ !cancelled() && matrix.group == 'riscv-ownership' }} + run: MEMU="$RUNNER_TEMP/downstream/memu" sh scripts/rv_exec_check.sh --corpus64 - name: rv_vec_owner (logical threads own Vecs, RV32 and RV64 against C) if: ${{ !cancelled() && matrix.group == 'riscv-ownership' }} diff --git a/README.md b/README.md index 61415de0..fd640717 100644 --- a/README.md +++ b/README.md @@ -109,7 +109,7 @@ source tree is needed to build or run an app. It **self-hosts** — the Mere-in-Mere compiler, compiled by itself and run as Wasm, emits byte-identical output to the reference. The RISC-V backend (RV32IM, and RV64IM since v0.1.394) emits a flat binary with no external assembler or linker, and `--bare` hands the program the machine instead of a host; on that there is a kernel, a scheduler and a shell written in Mere, and the self-hosted compiler runs there as a user process — on a RISC-V CPU also written in Mere — emitting WAT byte-identical to the native one. See [docs/bare-metal.md](docs/bare-metal.md). -- **2946 tests passing** (`dune test` with the full CI toolchain), plus cross-backend parity (248 programs) and integration and differential checks against external oracles in CI. The test total includes optional Wasm checks and depends on the installed tools. The full-suite and parity counts are re-derived by `scripts/first_run_check.sh`. +- **2946 tests passing** (`dune test` with the full CI toolchain), plus cross-backend parity (250 programs) and integration and differential checks against external oracles in CI. The test total includes optional Wasm checks and depends on the installed tools. The full-suite and parity counts are re-derived by `scripts/first_run_check.sh`. - **🏆 Bootstrap fixpoint — truly self-hosting** (v0.1.10, 2026-07-12): the Mere-in-Mere compiler, **compiled by itself and run as wasm, produces byte-identical output to the reference** — and that output runs correctly. Compiling a program with (A) the compiler under the interpreter and (B) the compiler compiled by itself yields the same WAT, byte for byte (CI-verified by a permanent fixpoint regression test). Getting there required guaranteed tail calls in the self-host codegen (`return_call_indirect`, Stage 55f) and fixing three latent self-compilation bugs (an eager pattern-check payload dereference, pointer-equality string compares in the untyped self-host codegen, and a missing `\r` lexer escape — Stage 55g). See [docs/changelog.md](docs/changelog.md). - **🏗️ A fifth backend, and an operating system on top of it** (v0.1.134–198): `mere -rv` emits a flat RV32IM binary with no external assembler or linker, and `--bare` hands the program the machine instead of a host — raw memory arrives as an unforgeable window capability, traps as ordinary Mere closures. On that: a preemptive scheduler, a shell, a syscall boundary, and finally **Mere's own self-hosted compiler running as a user process on a Mere kernel, on a CPU written in Mere**, emitting WAT byte-identical to the native interpreter. `mere -rvg` then emits a debug map beside the binary — from the same item list the assembler consumes, so it describes the bytes that actually ran — which is what lets [riscv-dbg](https://github.com/284km/memu/tree/main/riscv-dbg) break on Mere **source lines**, print a backtrace, and step **backwards**. `mere -rv64` (v0.1.394) is the same backend at twice the width: an RV64IM binary from the same code generator. See [docs/bare-metal.md](docs/bare-metal.md). - **🛰️ gRPC and GraphQL, against real clients** (v0.1.280–283): `contrib/proto` (protobuf wire both ways, `FileDescriptorSet`, and a code generator from `.proto`), `contrib/http2` (framing + HPACK + an h2c server with flow control in both directions and a worker pool), and `contrib/graphql` (lexer / parser / printer / SDL / executor with null propagation, introspection, and 21 of the specification's 32 validation rules). `grpcurl` and `graphql-js` are the oracles, and interfaces and unions resolve from `__typename` the way graphql-js's default `resolveType` does. See [contrib/proto/README.md](contrib/proto/README.md), [contrib/http2/README.md](contrib/http2/README.md), [contrib/graphql/README.md](contrib/graphql/README.md). diff --git a/RUNBOOK.md b/RUNBOOK.md index 84d24a7c..36646086 100644 --- a/RUNBOOK.md +++ b/RUNBOOK.md @@ -262,9 +262,19 @@ This covers direct source entries and the runner's `apt-mirrors.txt` or Repository suites, components, signing keys and other mirrors are preserved. The setup action's opam cache remains enabled. Compare actual setup step durations and cache-hit messages when measuring changes: a cache hit does not -avoid the action's system-package installation. All 188 gates and all four +avoid the action's system-package installation. All 191 gates and all four build configurations remain required. +The hosted RISC-V execution sweep has three required partitions: +`rv_exec_check.sh --corpus32` in coroutines, `--corpus64` in RISC-V ownership, +and `--contracts` in RISC-V. The default `--all` still runs both corpora and +every boundary case. Split modes require their emulator runners. The +partition audit in the containers group compares compiler invocations with +all-mode, including a refused C reference and a refused RV32 program. This is +a routing check; the three real emulator jobs retain the output comparisons, +known-difference freshness checks, bounds and named refusals. Compare complete +job durations when measuring the split; setup time is part of the result. + ## Binary releases `release-build.yml` is shared by the distribution CI jobs and tagged diff --git a/docs/changelog.md b/docs/changelog.md index b6166c6a..81a77e8a 100644 --- a/docs/changelog.md +++ b/docs/changelog.md @@ -4,6 +4,35 @@ Major implementation milestones recorded per-slice (newest first). See `git log` --- +## Unreleased + +Wasm now specializes a factory value whose uses settle on one concrete return +type, including aliases and nested scopes. Native C emits factory adapters +before the function bodies that reference them, and `with` bindings use the +same mangled name and lexical type environment as their body references. +The new factory parity fixture covers Vec, Map and OwnedVec factories. + +`snapshot value` obtains an independent immutable plain value through the +existing region-result copier. Arguments run once before the scratch region +opens. Nested containers, functions, borrows and capabilities are refused; +unresolved wrapper types remain monomorphic so their bound cannot be bypassed. +Parity covers Map/Vec compaction and recycling, nested data, binary bytes, +argument effects and shadowing. The lifetime gate also checks ASan/UBSan, +removes a copy to expose use-after-free, and checks plain-value refusals on +the interpreter, checker and all four compiled targets. + +The hosted RISC-V sweep is split into RV32 and RV64 corpora and a shared +boundary partition. All cases, known-difference freshness checks and refusal +checks remain in the default all-mode; an invocation audit checks their union +against the three CI modes. Required CI checks increase from 188 to 191: +two additional execution partitions and the partition audit. The nine groups, +four build configurations and existing required-check name are preserved. + +The resumed-pinner lifetime negative control now forces reclamation under its +recorded running pinner. Merely removing the running-pinner guard could leave +the arena protected by incidental conservative pins and miss the intended +fault; the revised control tests the reclamation boundary directly. + ## v0.1.711 — 2026-11-07 Native C and LLVM programs gain addressed UDP send and receive through diff --git a/docs/codegen.md b/docs/codegen.md index b0a50f38..bb065121 100644 --- a/docs/codegen.md +++ b/docs/codegen.md @@ -174,8 +174,9 @@ Builtin values are supported when the backend implements the operation and its use has a concrete callable type. Factory values such as `vec_new` and `map_new` are supported when their return type is concrete, as in [factory_value.mere](../examples/factory_value.mere). An unconstrained -`let make = vec_new` may retain a polymorphic return type; annotate it or -pass the builtin to a concretely typed parameter. Wrapping a call in `fn` +`let make = vec_new` is specialized on unreleased main when it has one concrete use type, +including through aliases; unresolved uses still need an annotation or a +concretely typed parameter. Wrapping a call in `fn` remains useful when an operation has a backend-specific restriction. See the standard-library reference for individual APIs. diff --git a/docs/host-matrix.md b/docs/host-matrix.md index f06f13dc..0de5a323 100644 --- a/docs/host-matrix.md +++ b/docs/host-matrix.md @@ -199,6 +199,7 @@ machine rather than a host. | `sign` | yes | yes | yes | yes | | `sin` | yes | yes | yes | yes | | `sleep_ms` | yes | yes | yes | yes | +| `snapshot` | yes | yes | yes | yes | | `spawn` | yes | yes | yes | yes | | `sqrt` | yes | yes | yes | yes | | `square` | yes | yes | yes | yes | diff --git a/docs/stdlib-reference.md b/docs/stdlib-reference.md index 3fc43f07..42e1ddbd 100644 --- a/docs/stdlib-reference.md +++ b/docs/stdlib-reference.md @@ -1843,6 +1843,28 @@ protects stopped stacks separately. The [suffix fixture](../test/parity/map_set_suffix.mere) checks a copied list snapshot across replacement and compaction. +**`snapshot : 'a -> 'a` (unreleased) copies an immutable plain value** into the enclosing +allocation scope, using the same deep copy as a region result. It supports +scalars, strings, bytes, SIMD values, tuples, and records/variants/lists whose +contents are also plain. Containers, functions, borrows and capabilities are +refused, including when hidden in a record or variant. The argument is +evaluated once in the caller's scope before copying; ordinary container read +ownership checks still apply. + +```mere +let saved = snapshot (map_get m key); +let _ = map_compact m; +// saved's immutable contents remain usable here +``` + +Use it similarly with `vec_get`. Direct calls may snapshot different types. +A wrapper or alias whose snapshot argument type is unresolved is kept +monomorphic, so later uses cannot bypass the plain-value bound. Use separate +wrappers when several argument types are needed. The interpreter keeps its +immutable GC-managed value; C, LLVM, Wasm and RISC-V use region-result copying. +The [snapshot fixture](../test/parity/snapshot.mere) checks copies across +compaction and recycling, nested data, argument effects and lexical shadowing. + **`OwnedVec`**: `owned_vec_get : OwnedVec[T] -> int -> T` joins `owned_vec_new` / `push` / `len` / `to_vec`, which are in language-reference. diff --git a/docs/tutorial.md b/docs/tutorial.md index 29fd7a94..7b85ba8d 100644 --- a/docs/tutorial.md +++ b/docs/tutorial.md @@ -657,9 +657,12 @@ node scripts/run_wasm.js v.wasm Builtin factories can also be used as values on interpreter, C, LLVM and Wasm when the factory has a concrete return type, for example `let make = (vec_new : unit -> Vec[__heap, int]) in ...`. -An unconstrained `let make = vec_new` can retain a polymorphic return type -and be refused by codegen; use an annotation or pass it to a concretely typed -parameter, as in [factory_value.mere](../examples/factory_value.mere). +On unreleased main, `let make = vec_new` also works when all uses settle on one concrete return +type, including aliases. An annotation or a concretely typed parameter remains +useful when the return type would otherwise stay unresolved, as in +[factory_value.mere](../examples/factory_value.mere). The +[factory inference fixture](../test/parity/factory_inference.mere) checks the +unannotated form across interpreter, C, LLVM and Wasm. Other builtin values follow the operation's backend support; [builtin_as_value.mere](../test/parity/builtin_as_value.mere) is an executable example. diff --git a/lib/ast.ml b/lib/ast.ml index ecf6bd38..9580bb47 100644 --- a/lib/ast.ml +++ b/lib/ast.ml @@ -1473,6 +1473,47 @@ let rec rv_map_scoped ~(shadow : string list) (f : string list -> expr -> expr o | Field_get (a, fl) -> { e with node = Field_get (g shadow a, fl) } | Record_update (a, fs) -> { e with node = Record_update (g shadow a, List.map (fun (fl, x) -> (fl, g shadow x)) fs) } +(* Lower a typed snapshot to the existing region-result copier before backend + analysis. Evaluate the argument once, outside the scratch region, so an + argument's allocation and mutation effects stay in their original scope. + A value-position use becomes an ordinary closure with the same operation. *) +let snapshot_region_name = "__snapshot_region" + +let lower_snapshots (prog : program) : program = + let copied loc ty value = + let name = "__snapshot_value" in + let read = { loc; ty; node = Var name } in + let block = { loc; ty; node = Region_block (snapshot_region_name, read) } in + { loc; ty; node = Let ({ ploc = loc; pnode = P_var name }, value, block) } + in + let rec rewrite shadow e = rv_map_scoped ~shadow replace e + and replace shadow e = + match e.node with + | App ({ node = Var "snapshot"; _ }, arg) when not (List.mem "snapshot" shadow) -> + Some (copied e.loc e.ty (rewrite shadow arg)) + | Var "snapshot" when not (List.mem "snapshot" shadow) -> + (match Option.map walk e.ty with + | Some (TyArrow (a, b)) -> + let name = "__snapshot_arg" in + let arg = { loc = e.loc; ty = Some a; node = Var name } in + Some { e with node = Fun (name, Some a, copied e.loc (Some b) arg) } + | _ -> None) + | _ -> None + in + let shadow = ref [] in + let decls = List.map (function + | Top_let (p, v) -> + let v = rewrite !shadow v in + shadow := pattern_vars p @ !shadow; + Top_let (p, v) + | Top_let_rec bs -> + shadow := List.map rb_name bs @ !shadow; + Top_let_rec (List.map (fun (n, l, v) -> n, l, rewrite !shadow v) bs) + | (Top_forward (n, _, _) | Top_extern (n, _)) as d -> + shadow := n :: !shadow; d + | d -> d) prog.decls in + { decls; main = rewrite !shadow prog.main } + (* A structural copy with every `ty` cleared: `expr.ty` is mutable and set by the typer, so a subtree the pass places twice (the bound in a guard, an atomic argument in both branches of a dispatch) gets its own nodes. *) diff --git a/lib/codegen_c.ml b/lib/codegen_c.ml index a414b473..aaf99638 100644 --- a/lib/codegen_c.ml +++ b/lib/codegen_c.ml @@ -2615,7 +2615,16 @@ let rec emit_expr (e : Ast.expr) : string = The close field is a `unit -> unit` closure; dispatch via the closure struct's `.fn(.env, 0)`. *) let value_c = emit_expr value in - let body_c = emit_expr body in + let prev_types = !current_var_types in + let prev_subst = !current_env_subst in + current_var_types := VtMap.add name (Option.value value.Ast.ty ~default:Ast.TyUnit) prev_types; + current_env_subst := List.filter (fun (n, _) -> n <> name) prev_subst; + let body_c = + Fun.protect (fun () -> emit_expr body) ~finally:(fun () -> + current_var_types := prev_types; + current_env_subst := prev_subst) + in + let name = c_safe_name name in let close_call = match value.Ast.ty with | Some t -> @@ -5033,6 +5042,8 @@ let rec emit_expr (e : Ast.expr) : string = in "((" ^ struct_name ^ "){" ^ String.concat ", " init_fields ^ "})" | Ast.Region_block (name, body) -> + if name = Ast.snapshot_region_name then + Option.iter (Typer.check_snapshot_bound e.Ast.loc) e.Ast.ty; (* Allocate a region buffer, evaluate body, free. The region's C local name is `__region_` — accessed by Ref/`&R v` when emitting `R.alloc(...)` calls inside body. Default cap 1 MB. @@ -15873,6 +15884,7 @@ let emit_c_header (prog : Ast.program) : string = String.concat "\n" lines ^ "\n" let emit_program ?(main_ty = Ast.TyInt) (prog : Ast.program) : string = + let prog = Ast.lower_snapshots prog in (* Q-127: SETTLE EVERY UNDECIDED CONTAINER REGION BEFORE ANYTHING READS ONE. A slot can hold a variable up to here, so that a call site inside a `region` block can decide it; what is left means nobody did, and it becomes `__heap`. @@ -18007,7 +18019,6 @@ let emit_program ?(main_ty = Ast.TyInt) (prog : Ast.program) : string = @ (if top_global_decls = [] then [] else "/* Phase 30.2: top-level non-fn let values as file-scope globals */" :: top_global_decls @ [""]) - @ (if fn_defs = [] then [] else fn_defs @ [""]) @ (let eta_lines = Hashtbl.fold (fun adapter (builtin, ret_ty) acc -> (* Generate static adapter fn + const value for the eta-wrapped @@ -18052,6 +18063,9 @@ let emit_program ?(main_ty = Ast.TyInt) (prog : Ast.program) : string = if eta_lines = [] then [] else "/* Phase 35.1: nullary factory builtins as first-class values */" :: eta_lines @ [""]) + (* Lifted function bodies can reference a factory value. Its declaration + must precede those bodies, just as its runtime helpers precede it. *) + @ (if fn_defs = [] then [] else fn_defs @ [""]) @ (if !lib_mode then lib_boundary_parts else let run_lines = [ (* the stack bounds are read here, where the program's first frame is diff --git a/lib/codegen_llvm.ml b/lib/codegen_llvm.ml index ba0fc235..6817ad8e 100644 --- a/lib/codegen_llvm.ml +++ b/lib/codegen_llvm.ml @@ -8721,6 +8721,8 @@ let rec emit_expr (env : env) (e : Ast.expr) : string = emit_instr (Printf.sprintf " call void @__lang_region_block_release(ptr %s)" rv); out | Ast.Region_block (name, body) -> + if name = Ast.snapshot_region_name then + Option.iter (Typer.check_snapshot_bound e.Ast.loc) e.Ast.ty; (* Allocate a fresh region locally, run body within it, free at exit. The region's SSA ptr is pushed onto current_regions so Ref / view constructions inside body find it by name. *) @@ -18574,6 +18576,7 @@ let rewrite_of_json (prog : Ast.program) : Ast.program = { Ast.main; decls = decls0 @ List.rev !decls } let emit_program ?(main_ty = Ast.TyInt) (prog : Ast.program) : string = + let prog = Ast.lower_snapshots prog in let prog = rewrite_read_lines prog in let prog = rewrite_of_json prog in (* Q-127: SETTLE EVERY UNDECIDED CONTAINER REGION BEFORE ANYTHING READS ONE. diff --git a/lib/codegen_riscv.ml b/lib/codegen_riscv.ml index eae0943a..f6245935 100644 --- a/lib/codegen_riscv.ml +++ b/lib/codegen_riscv.ml @@ -2724,7 +2724,10 @@ and compile_node (env : env) (e : Ast.expr) : unit = emit (LoadAddr (a0, label)) (* a0 = &block *) (* v0.1.658: see compile_region *) | Ast.Region_loop (_, x, body) -> compile_region env e body (Some x) - | Ast.Region_block (_, body) -> compile_region env e body None + | Ast.Region_block (name, body) -> + if name = Ast.snapshot_region_name then + Option.iter (Typer.check_snapshot_bound e.Ast.loc) e.Ast.ty; + compile_region env e body None | Ast.Float_lit f -> let b = Int64.bits_of_float f in (* v0.1.656: on RV64 the halves are stored as the arithmetic stores them @@ -8666,6 +8669,7 @@ let prepare_main (prog : Ast.program) : Ast.expr = | Monomorph.Error (loc, msg) -> err loc msg let build_items_sized (prog : Ast.program) : item list = + let prog = Ast.lower_snapshots prog in let full = prepare_main prog in code_span := 0x200000; let rec settle round items = diff --git a/lib/codegen_wasm.ml b/lib/codegen_wasm.ml index 4977cea8..76234608 100644 --- a/lib/codegen_wasm.ml +++ b/lib/codegen_wasm.ml @@ -5103,7 +5103,9 @@ and emit_expr (e : Ast.expr) : unit = emit_instr "end"; emit_instr (Printf.sprintf "local.get %d" res_slot); wasm_tail_pos := saved_tail - | Ast.Region_block (_, body) -> + | Ast.Region_block (name, body) -> + if name = Ast.snapshot_region_name then + Option.iter (Typer.check_snapshot_bound e.Ast.loc) e.Ast.ty; (* v0.1.37: regions RECLAIM again — the safe version of the save / restore that Phase 16.4 removed as unsound. Three parts make it sound where the old version was not: @@ -11430,6 +11432,7 @@ let rewrite_read_lines (prog : Ast.program) : Ast.program = | other -> other) prog.Ast.decls } let emit_program ?(main_ty = Ast.TyInt) ?(component = false) (prog : Ast.program) : string = + let prog = Ast.lower_snapshots prog in let prog = rewrite_read_lines prog in (* Q-127: SETTLE EVERY UNDECIDED CONTAINER REGION BEFORE ANYTHING READS ONE. A slot can hold a variable up to here, so that a call site inside a `region` block @@ -11701,6 +11704,12 @@ let emit_program ?(main_ty = Ast.TyInt) ?(component = false) (prog : Ast.program walk root in resolve_vec_let_types main_expr; + (* A generalized factory value may have one concrete use after its result + container is resolved. Propagate that use back to the binding before + creating its eta adapter, as the native backends do. *) + (* Wasm already handles polymorphic functions; only specialize value + bindings here, avoiding a new per-function scope scan. *) + Monomorph.specialize_single_use_local_fns ~functions:false main_expr; (* Phase 32.4 (C1 FFI): walk prog.decls to register extern fn names. *) Hashtbl.reset extern_fn_decls_wasm; List.iter (fun decl -> diff --git a/lib/eval.ml b/lib/eval.ml index 42fefbc6..e4f72853 100644 --- a/lib/eval.ml +++ b/lib/eval.ml @@ -4178,6 +4178,22 @@ let builtin_vec_of_bytes = let initial_env : env = [ ("print", ref builtin_print); + ("snapshot", ref (V_builtin ("snapshot", fun value -> + (* Plain interpreter values are immutable and GC-managed. Check the + runtime shape as well, since declarations can execute before a + deferred type obligation is discharged. *) + let rec plain = function + | [] -> true + | (V_int _ | V_float _ | V_bool _ | V_str _ | V_bytes _ | V_unit + | V_f64x2 _ | V_f32x4 _ | V_u8x16 _) :: rest -> plain rest + | V_constr (_, None) :: rest -> plain rest + | V_constr (_, Some v) :: rest -> plain (v :: rest) + | V_tuple vs :: rest -> plain (vs @ rest) + | V_record (_, fs) :: rest -> plain (List.map snd fs @ rest) + | _ -> false + in + if plain [value] then value + else failwith "snapshot cannot copy a container, function, borrow or capability"))); (* bytes builtins *) ("bytes_len", ref builtin_bytes_len); ("bytes_get", ref builtin_bytes_get); diff --git a/lib/monomorph.ml b/lib/monomorph.ml index c2f619ae..f3b29f68 100644 --- a/lib/monomorph.ml +++ b/lib/monomorph.ml @@ -723,7 +723,7 @@ let has_unresolved_use_of (name : string) (exprs : Ast.expr list) : bool = in List.iter go exprs; !found -let specialize_single_use_local_fns (root : Ast.expr) : unit = +let specialize_single_use_local_fns ?(functions = true) (root : Ast.expr) : unit = let changed = ref true in let specialize vty t = try @@ -735,7 +735,7 @@ let specialize_single_use_local_fns (root : Ast.expr) : unit = (match e.Ast.node with | Ast.Let ({ Ast.pnode = Ast.P_var n; _ }, ({ Ast.node = Ast.Fun _; ty = Some vty; _ } as value), body) - when not (ty_is_concrete (Ast.walk vty)) -> + when functions && not (ty_is_concrete (Ast.walk vty)) -> (match find_all_concrete_arrows_in ~scope_lets:true n [body] with | [arrow] when not (has_unresolved_use_of n [body]) -> specialize vty arrow @@ -754,7 +754,7 @@ let specialize_single_use_local_fns (root : Ast.expr) : unit = | [t] when not (has_unresolved_use_of n [body]) -> specialize vty t | _ -> ()) - | Ast.Let_rec (bindings, body) -> + | Ast.Let_rec (bindings, body) when functions -> (* Single-use specialization for a local `let rec` group, RESTRICTED to trait-constrained members (a dictionary-taking fn produced by trait_elab, whose first parameter is a `__dict` record). This diff --git a/lib/typer.ml b/lib/typer.ml index e2fafd06..4964d04c 100644 --- a/lib/typer.ml +++ b/lib/typer.ml @@ -355,9 +355,16 @@ let env_free_vars env = a !Send value cannot be smuggled through a polymorphic wrapper (it would either fail the discharge check or fail to unify across two uses). *) let pending_send : (Ast.ty * Loc.t) list ref = ref [] -let reset_send_constraints () = pending_send := [] -let pending_send_ids () = - List.fold_left (fun acc (ty, _) -> collect_free_vars ty acc) [] !pending_send +let pending_snapshot : (Ast.ty * Loc.t) list ref = ref [] +let active_snapshot : (Ast.ty * Loc.t) list ref = ref [] +let reset_send_constraints () = + pending_send := []; pending_snapshot := []; active_snapshot := [] +let pending_bound_ids () = + (* Keep all obligations for final validation, but stop rescanning concrete + snapshot types at every later binding. A sequence of N copies stays O(N). *) + active_snapshot := List.filter (fun (t, _) -> collect_free_vars t [] <> []) !active_snapshot; + List.fold_left (fun acc (ty, _) -> collect_free_vars ty acc) [] + (!pending_send @ !active_snapshot) (* A trait obligation recorded during inference. The `Ast.expr` is the exact Var node (matched later by physical identity) that must be rewritten by the @@ -1071,9 +1078,9 @@ let freshen_annot t = let generalize env t = - let send_ids = pending_send_ids () in + let send_ids = pending_bound_ids () in (* A variable is generalizable when it was created inside this binding and is - not pinned by a pending Send obligation. + not pinned by a pending Send or snapshot obligation. This used to ask the environment instead: collect every free variable of every scheme in scope and quantify what was not among them. That is the @@ -1856,6 +1863,38 @@ let record_send_bound loc (t : Ast.ty) = resolved to a concrete type must be Send. Elements still mentioning type variables are left alone (they were kept monomorphic, so a later concrete use would either satisfy this or fail to unify). *) +(* A snapshot has no mutable identity, borrow or hidden closure environment. + Look through nominal fields too: hiding a Vec in a record does not copy it. + Unresolved variables are pinned by the same generalization rule as Send. *) +let rec snapshot_refusal visiting t = + let first ts = List.find_map (snapshot_refusal visiting) ts in + match Ast.walk t with + | Ast.TyArrow _ -> Some "function" + | Ast.TyRef _ -> Some "borrow" + | Ast.TyParam _ -> Some "unresolved type parameter" + | Ast.TyTuple ts -> first ts + | Ast.TyCon (n, _) when + List.mem n region_parameterised_names || n = "OwnedVec" + || Hashtbl.mem drop_types n || Hashtbl.mem local_types n + || Hashtbl.mem sync_types n -> Some n + | Ast.TyCon (n, args) when List.mem n visiting -> first args + | Ast.TyCon (n, args) -> + (match nominal_contents n args with + | Some ts -> List.find_map (snapshot_refusal (n :: visiting)) ts + | None -> Some n) + | _ -> None + +let check_snapshot_bound loc t = + match snapshot_refusal [] t with + | None -> () + | Some what -> raise (Type_error (loc, + "snapshot cannot copy " ^ what ^ ": use an immutable plain value, without containers, functions, borrows or capabilities")) + +let record_snapshot_bound loc t = + check_snapshot_bound loc t; + pending_snapshot := (t, loc) :: !pending_snapshot; + active_snapshot := (t, loc) :: !active_snapshot + let discharge_send_constraints () = List.iter (fun (t, loc) -> if collect_free_vars t [] = [] && not (is_send t) then @@ -1863,7 +1902,8 @@ let discharge_send_constraints () = Printf.sprintf "`%s` is not Send — a value of this type cannot cross a thread \ boundary" (Ast.pp_ty t))) - ) !pending_send + ) !pending_send; + List.iter (fun (t, loc) -> check_snapshot_bound loc t) !pending_snapshot (* Instantiate a constructor for a single use: pick fresh TyVars for params, substitute them into the arg type and result type. *) @@ -2964,8 +3004,14 @@ let map_iter_scheme = let () = Hashtbl.replace types "Map" 3 +let snapshot_scheme = + let a = fresh_var () in + let id = match a with Ast.TyVar v -> v.id | _ -> assert false in + { constraints = []; quantified = [id]; body = Ast.TyArrow (a, a) } + let initial_env : env = [ ("print", mono (Ast.TyArrow (Ast.TyStr, Ast.TyUnit))); + ("snapshot", snapshot_scheme); (* Q-012 step 3a: concurrency primitives *) ("spawn", spawn_scheme); ("join", join_scheme); @@ -3618,6 +3664,12 @@ and infer_node (env : env) (e : Ast.expr) : Ast.ty = | None -> false) -> Deprecated.note row e.Ast.loc | _ -> ()); let ity, mapping = instantiate_with_map sch in + (if name = "snapshot" && sch == snapshot_scheme then begin + saw_region_block := true; + match Ast.walk ity with + | Ast.TyArrow (a, _) -> record_snapshot_bound e.Ast.loc a + | _ -> assert false + end); (* Q-127: this reference is being evaluated HERE, so whatever it allocates is allocated here -- see `bind_instantiated_alloc_regions`. *) bind_instantiated_alloc_regions mapping; diff --git a/scripts/ci_gate_check.rb b/scripts/ci_gate_check.rb index e4b702da..9f3a3e66 100644 --- a/scripts/ci_gate_check.rb +++ b/scripts/ci_gate_check.rb @@ -10,13 +10,18 @@ class Invalid < StandardError; end # Update deliberately when adding or removing checks. A deleted step must # not silently reduce the coverage while every remaining group is green. - EXPECTED_CHECKS = 188 + EXPECTED_CHECKS = 191 PREFLIGHT = "tool_preflight (a gate that did not run is not a gate that passed)" FULL_TESTS = "Run tests (full, with the wasm toolchain present)" CHECKOUT = "Check out the dogfood repositories" CACHE = "Restore the downstream compile cache" PACKAGES = "Install package dependencies" CHECKOUT_GROUPS = %w[coroutines downstream riscv riscv-ownership].freeze + RV_EXEC = { + "rv_exec contracts (hosted boundaries at both widths)" => ["riscv", "--contracts"], + "rv_exec corpus32 (the full corpus against C)" => ["coroutines", "--corpus32"], + "rv_exec corpus64 (the full corpus against C)" => ["riscv-ownership", "--corpus64"] + }.freeze RISCV_TOOLS = ["Install qemu-system-riscv32 (optional gate)", "Install binutils-riscv64 (optional gate — oracle for mere -rvd)"].freeze @@ -110,6 +115,8 @@ def self.check(workflow) "required tool preflight must inspect the active group's gates") checks = steps[(start + 1)..] require!(checks.map { |s| s["name"] }.uniq.length == checks.length, "check names must be unique") + require!(RV_EXEC.keys.all? { |n| checks.count { |s| s["name"] == n } == 1 }, + "all three RISC-V execution partitions must run once") require!(checks.count { |s| s["name"] == FULL_TESTS } == 1, "the full toolchain unit suite must run once") require!(checks.count { |s| s["name"] == CHECKOUT } == 1, "downstream checkouts must be present") require!(checks.count { |s| s["name"] == CACHE } == 1, "the downstream compile cache must be present") @@ -135,6 +142,13 @@ def self.check(workflow) "every RISC-V oracle group must require memu") when CACHE require!(selected == ["downstream"], "only downstream may write the compile cache") + when *RV_EXEC.keys + group, mode = RV_EXEC.fetch(name) + require!(selected == [group], "#{name}: wrong execution group") + require!(!step["continue-on-error"], "#{name}: execution failures must fail the group") + require!(step["run"] == "MEMU=\"$RUNNER_TEMP/downstream/memu\" sh scripts/rv_exec_check.sh #{mode}", + "#{name}: the assigned partition must execute") + assigned.fetch(group) << name else require!(selected.length == 1, "#{name}: each check must run in exactly one group") require!(!step["continue-on-error"] && !step.fetch("run", "").empty?, "#{name}: check failures must fail the group") @@ -170,6 +184,11 @@ def self.self_test(workflow) "unknown group" => ->(c) { c[:poison]["if"] = "${{ !cancelled() && matrix.group == 'typo' }}" }, "duplicated check" => ->(c) { c[:poison]["if"] = "${{ !cancelled() && (matrix.group == 'compiler' || matrix.group == 'runtime') }}" }, "deleted check" => ->(c) { c[:steps].delete(c[:poison]) }, + "missing RV64 partition" => ->(c) { c[:steps].reject! { |s| s["name"] == RV_EXEC.keys.last } }, + "duplicate RV32 work" => ->(c) { c[:steps].find { |s| s["name"] == RV_EXEC.keys.last }["run"].sub!("--corpus64", "--corpus32") }, + "unpartitioned RV work" => ->(c) { c[:steps].find { |s| s["name"] == RV_EXEC.keys.first }["run"].sub!("--contracts", "--all") }, + "optional RV partition" => ->(c) { c[:steps].find { |s| s["name"] == RV_EXEC.keys.first }["continue-on-error"] = true }, + "RV corpus in wrong group" => ->(c) { c[:steps].find { |s| s["name"] == RV_EXEC.keys.last }["if"] = "${{ !cancelled() && matrix.group == 'riscv' }}" }, "duplicate group" => ->(c) { c[:matrix]["group"] << "compiler" }, "empty group" => ->(c) { c[:matrix]["group"] << "unused" }, "excluded group" => ->(c) { c[:matrix]["exclude"] = [{"group" => "compiler"}] }, diff --git a/scripts/host_matrix.sh b/scripts/host_matrix.sh index 85212023..aebe2efb 100755 --- a/scripts/host_matrix.sh +++ b/scripts/host_matrix.sh @@ -77,6 +77,7 @@ trap 'rm -rf "$TMP"' EXIT cat > "$TMP/overrides" <<'CASES' print_bytes|let _ = print_bytes (bytes_of_str "x"); 0 +snapshot|snapshot 42 read_file|let s = read_file "/dev/null"; str_len s write_file|let _ = write_file "/dev/null" "x"; 0 read_file_bytes|let v = read_file_bytes "/dev/null"; vec_len v diff --git a/scripts/region_uaf_check.sh b/scripts/region_uaf_check.sh index 8a13aca5..f19df7ab 100755 --- a/scripts/region_uaf_check.sh +++ b/scripts/region_uaf_check.sh @@ -80,6 +80,10 @@ run_bin() { perl -e 'alarm 20; exec @ARGV' "$1" 2>&1; } # allocator prints about it is not the program's. run_poisoned() { env MallocScribble=1 MALLOC_PERTURB_=85 perl -e 'alarm 20; exec @ARGV' "$1" 2>&1 | grep -v 'malloc: enabling scribbling'; } +# The resumed-pinner control forces reclamation when a recorded pinner is +# running. Removing just its keep flag could leave an incidental conservative +# pin on another stack, hiding the fault despite identical emitted code. + build() { # $1 = program, $2 = c|ll, [$3 = sed expression] -> $T/bin, or prints why not "$MERE" "-$2" "$FX/$1.mere" > "$T/g.$2" 2>"$T/emit.err" || { echo "EMITFAIL $(head -1 "$T/emit.err")"; return 1; } if [ -n "${3:-}" ]; then @@ -160,7 +164,7 @@ channel_from_block|ll|the message is sent as the pointer|s/= call ptr @__mcopy_s recycled_escape|c|only the moved storage is kept, not where the struct lives|s/ __lang_region_keep(v->home, r); / / recycle_dedicated|c|a recycle claims 4 KB on the block it kept|s/^ r->cap = b->pad;$/ r->cap = 4096;/ coro_pin_reach|c|the pin reads the stack and not what it points at|s/^ __lang_pin_reach(c);$// -coro_pin_resumed|c|a retired arena is tried while its pinner runs|s/if (o.by\[j\] == curh) keep = 1;// +coro_pin_resumed|c|a retired arena is freed while its pinner runs|perl:s/if \(o.by\[j\] == curh\) keep = 1;/if (o.by[j] == curh) keep = 2;/; s/if \(keep\) __lang_retired\[w\+\+\] = o;/if (keep == 2) { free(o.by); __lang_region_free(o.r); free(o.r); } else if (keep) __lang_retired[w++] = o;/ vec_recycle_pin|c|vec_recycle asks the pin about the growth only, as map_recycle does|s/__lang_region_pinned(v->region, 0)) {/__lang_region_pinned(v->region, 1) \&\& v->region->blocks->prev) {/ channel_xthread|c|a message region goes on the list of the thread that made it|s/__lang_region_init_x(mr, 256, 1)/__lang_region_init_x(mr, 256, 0)/' printf '%s\n' "$POISONS" | while IFS='|' read -r f be what expr; do @@ -174,5 +178,8 @@ channel_xthread|c|a message region goes on the list of the thread that made it|s [ -f "$T/pfailed" ] && { echo "region_uaf --poison: FAILED"; exit 1; } fi +if [ "$MODE" != --rv-only ]; then + MERE="$MERE" python3 "$ROOT/scripts/snapshot_check.py" || exit 1 +fi if [ "$fail" != 0 ]; then echo "region_uaf: FAILED"; exit 1; fi if [ "$MODE" = --poison ]; then echo "region_uaf --poison: ok (the gate can go red)$rvnote"; else echo "region_uaf: ok$rvnote"; fi diff --git a/scripts/rv_exec_check.sh b/scripts/rv_exec_check.sh index 2e918900..ad9a011c 100755 --- a/scripts/rv_exec_check.sh +++ b/scripts/rv_exec_check.sh @@ -23,10 +23,25 @@ # sh scripts/rv_exec_check.sh # MEMU=/path/to/memu sh scripts/rv_exec_check.sh set -u +MODE="${1:---all}" +case "$MODE:$#" in + --all:0|--all:1|--corpus32:1|--corpus64:1|--contracts:1) ;; + *) echo "usage: rv_exec_check.sh [--all | --corpus32 | --corpus64 | --contracts]" >&2; exit 2 ;; +esac +echo "rv_exec: mode $MODE" ROOT="$(cd "$(dirname "$0")/.." && pwd)" -MERE="$ROOT/_build/default/bin/mere.exe" +MERE="${MERE:-$ROOT/_build/default/bin/mere.exe}" CC="${CC:-cc}" [ -x "$MERE" ] || { echo "rv_exec_check: $MERE not found — run 'dune build'" >&2; exit 1; } +if [ "$MODE" != --all ]; then + for width in 32 64; do + [ "$MODE" = --corpus32 ] && [ "$width" = 64 ] && continue + [ "$MODE" = --corpus64 ] && [ "$width" = 32 ] && continue + [ -n "${MEMU:-}" ] && [ -f "$MEMU/riscv-runc/rv${width}i_run.mere" ] || { + echo "rv_exec: RV$width runner required" >&2; exit 2; + } + done +fi TMP=$(mktemp -d) trap 'rm -rf "$TMP"' EXIT rc=0; pass=0; fail=0 @@ -81,7 +96,7 @@ KNOWN_DIFF="float_edges region_growth int_width_boundary bytes_file_roundtrip ra # (map_compact sat here until v0.1.614, when a Map got an arena to measure) RVRUN="" -if [ -n "${MEMU:-}" ]; then +if [ "$MODE" != --corpus64 ] && [ -n "${MEMU:-}" ]; then [ -f "$MEMU/riscv-runc/rv32i_run.mere" ] || { echo "FAIL rv_exec: no rv32i_run.mere under MEMU=$MEMU"; exit 1; } "$MERE" -c "$MEMU/riscv-runc/rv32i_run.mere" > "$TMP/rvrun.c" 2>"$TMP/err" || { echo "FAIL rv_exec: the emulator did not compile"; head -5 "$TMP/err"; exit 1; } @@ -90,6 +105,7 @@ if [ -n "${MEMU:-}" ]; then fi echoed=0; known=0; nocref=0; refused=0; refused_names="" +if [ "$MODE" = --all ] || [ "$MODE" = --corpus32 ]; then for p in "$ROOT"/test/parity/*.mere; do name=$(basename "$p" .mere) if "$MERE" -c "$p" > "$TMP/ref.c" 2>/dev/null && $CC -O1 -w -o "$TMP/ref" "$TMP/ref.c" 2>/dev/null; then @@ -141,6 +157,9 @@ for p in "$ROOT"/test/parity/*.mere; do fi done +fi + +if [ "$MODE" = --all ] || [ "$MODE" = --contracts ]; then # test/rv/ holds programs that cannot sit in the parity corpus because some # OTHER backend refuses them. region_map_escape: Wasm refuses a map mutation # inside a region at compile time (it rolls the whole block back); this backend @@ -216,6 +235,8 @@ else printf ' FAIL %s (-rv refused it)\n' "$name"; head -3 "$TMP/rverr"; fail=$((fail+1)); rc=1 fi +fi + # --- the same corpus, at 64 bits --------------------------------------------- # rvrun64 is the RV64IM core; the reference stays the C backend, whose int is # also 64 bits -- so the width-related known-differences of the 32-bit column @@ -240,7 +261,7 @@ case "$(uname -m)" in x86_64|amd64) KNOWN_DIFF64="$KNOWN_DIFF64 float_bits" ;; e # strbuf is concat-backed: 200k chars = GBs of dead heap. # The fix is a real byte-buffer strbuf, recorded work. RVRUN64="" -if [ -n "${MEMU:-}" ] && [ -f "$MEMU/riscv-runc/rv64i_run.mere" ]; then +if [ "$MODE" != --corpus32 ] && [ -n "${MEMU:-}" ] && [ -f "$MEMU/riscv-runc/rv64i_run.mere" ]; then if "$MERE" -c "$MEMU/riscv-runc/rv64i_run.mere" > "$TMP/rvrun64.c" 2>"$TMP/err" \ && $CC -O2 -w -o "$TMP/rvrun64" "$TMP/rvrun64.c" 2>"$TMP/err"; then RVRUN64="$TMP/rvrun64" @@ -249,7 +270,7 @@ if [ -n "${MEMU:-}" ] && [ -f "$MEMU/riscv-runc/rv64i_run.mere" ]; then fi fi pass64=0; fail64=0; known64=0; refused64=0; refused64_names="" -if [ -n "$RVRUN64" ]; then +if { [ "$MODE" = --all ] || [ "$MODE" = --corpus64 ]; } && [ -n "$RVRUN64" ]; then for p in "$ROOT"/test/parity/*.mere; do name=$(basename "$p" .mere) if "$MERE" -c "$p" > "$TMP/ref.c" 2>/dev/null && $CC -O1 -w -o "$TMP/ref" "$TMP/ref.c" 2>/dev/null; then @@ -290,6 +311,15 @@ if [ -n "$RVRUN64" ]; then echo "" fi +# Split CI modes require their execution oracle; compile-only success is +# reserved for the developer's default --all mode. +case "$MODE" in + --corpus32) [ -n "$RVRUN" ] || { echo "rv_exec: RV32 runner required" >&2; exit 2; } ;; + --corpus64) [ -n "$RVRUN64" ] || { echo "rv_exec: RV64 runner required" >&2; exit 2; } ;; + --contracts) [ -n "$RVRUN" ] && [ -n "$RVRUN64" ] || { echo "rv_exec: both runners required" >&2; exit 2; } ;; +esac + +if [ "$MODE" = --all ] || [ "$MODE" = --contracts ]; then # print_bytes and the machine a refusal names, at both widths. Written-out # expectations, like extern_catchable: the interpreter has no RV32I/RV64I to # name. The NUL is shown as `@` so the comparison is on text. @@ -622,14 +652,17 @@ else fi echo "rv_exec: $wfpass passed, $wffail failed for write_file/read_stdin (both widths, and --bare still refuses)" +fi -if [ -z "$RVRUN" ]; then - echo "rv_exec: $pass built, $fail failed — nothing RAN; set MEMU= for that half" -else - echo "rv_exec: $pass passed, $fail failed, $known known-different (C backend vs RV32I on the Mere-written CPU)" - echo "rv_exec: $echoed of those matched except the program's own final value, which only a compiled-in main prints" - echo "rv_exec: $refused of the corpus refused by -rv at compile time (not run here; host_matrix names the reasons):" - echo "$refused_names" | tr ' ' '\n' | grep -v '^$' | sort | tr '\n' ' ' | sed 's/^/rv_exec: /;s/ $//' - echo "" +if [ "$MODE" != --corpus64 ]; then + if [ -z "$RVRUN" ]; then + echo "rv_exec: $pass built, $fail failed — nothing RAN; set MEMU= for that half" + else + echo "rv_exec: $pass passed, $fail failed, $known known-different (C backend vs RV32I on the Mere-written CPU)" + echo "rv_exec: $echoed of those matched except the program's own final value, which only a compiled-in main prints" + echo "rv_exec: $refused of the corpus refused by -rv at compile time (not run here; host_matrix names the reasons):" + echo "$refused_names" | tr ' ' '\n' | grep -v '^$' | sort | tr '\n' ' ' | sed 's/^/rv_exec: /;s/ $//' + echo "" + fi fi exit $rc diff --git a/scripts/rv_exec_partition_check.py b/scripts/rv_exec_partition_check.py new file mode 100644 index 00000000..331bfc31 --- /dev/null +++ b/scripts/rv_exec_partition_check.py @@ -0,0 +1,92 @@ +#!/usr/bin/env python3 +"""Audit compiler invocations in all-mode versus the three CI partitions. + +The stubs deliberately have no program semantics. This checks shell routing; +the real emulator gates remain responsible for values, refusals and failures. +""" +from collections import Counter +from pathlib import Path +import os +import shlex +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent.parent + + +def main(): + with tempfile.TemporaryDirectory(prefix="rv-partition-") as d: + tmp = Path(d) + memu = tmp / "memu/riscv-runc" + memu.mkdir(parents=True) + for width in [32, 64]: + (memu / f"rv{width}i_run.mere").touch() + mere = tmp / "mere" + mere.write_text("""#!/bin/sh +printf '%s\\t' "$@" >> "$MERE_TRACE" +printf '\\n' >> "$MERE_TRACE" +case "$*" in *str_edges.mere*) [ "$1" = -c ] && exit 1 ;; esac +case "$*" in *float_edges.mere*) [ "$1" = -rv ] && exit 1 ;; esac +printf 'stub\\n' +""") + cc = tmp / "cc" + cc.write_text("""#!/bin/sh +while [ "$#" -gt 0 ]; do + if [ "$1" = -o ]; then shift; out=$1; break; fi + shift +done +printf '#!/bin/sh\\nexit 0\\n' > "$out" +chmod +x "$out" +""") + mere.chmod(0o755) + cc.chmod(0o755) + source = (ROOT / "scripts/rv_exec_check.sh").read_text() + + def audit(source, mode, label): + script = tmp / (label + ".sh") + # Keep the real corpus, despite placing the instrumented shell in tmp. + source = source.replace('ROOT="$(cd "$(dirname "$0")/.." && pwd)"', + "ROOT=" + shlex.quote(str(ROOT))) + source = source.replace('MERE="$ROOT/_build/default/bin/mere.exe"', + 'MERE="${MERE:-$ROOT/_build/default/bin/mere.exe}"') + script.write_text(source) + trace = tmp / (label + ".trace") + env = dict(os.environ, MERE=str(mere), CC=str(cc), MEMU=str(memu.parent), MERE_TRACE=str(trace)) + result = subprocess.run(["sh", script, *mode], env=env, capture_output=True, timeout=300) + if result.returncode not in [0, 1]: + raise RuntimeError(result.stderr.decode()) + if mode == ["--corpus64"]: + output = result.stdout.decode() + assert "C backend vs RV64 on the Mere-written CPU" in output + assert "nothing RAN" not in output and "C backend vs RV32I" not in output + records = [] + for line in trace.read_text().splitlines(): + args = tuple(a.replace(str(ROOT) + "/", "") for a in line.rstrip("\t").split("\t")) + if not any("/riscv-runc/" in a for a in args): + records.append(args) + return Counter(records) + + whole = audit(source, [], "all") + parts = Counter() + for mode in ["--corpus32", "--corpus64", "--contracts"]: + part = audit(source, [mode], mode[2:]) + assert part, mode + parts += part + assert whole == parts, ("partition mismatch", whole - parts, parts - whole) + for width in [32, 64]: + flag = "-rv" if width == 32 else "-rv64" + assert any(flag in a and a[-1].startswith("test/parity/") for a in whole) + assert any(flag in a and a[-1].startswith("test/rv/") for a in whole) + if len(sys.argv) == 3 and sys.argv[1] == "--baseline": + baseline = audit(Path(sys.argv[2]).read_text(), [], "baseline") + assert baseline == whole, ("baseline mismatch", baseline - whole, whole - baseline) + for mode in ["--corpus32", "--corpus64", "--contracts", "--typo"]: + r = subprocess.run(["sh", ROOT / "scripts/rv_exec_check.sh", mode], + env=dict(os.environ, MERE=str(mere), MEMU=""), capture_output=True) + assert r.returncode == 2, mode + print(f"rv_exec_partition: {sum(whole.values())} fixture compiler invocations retained; three complementary partitions; missing runners and invalid modes refused") + + +if __name__ == "__main__": + main() diff --git a/scripts/snapshot_check.py b/scripts/snapshot_check.py new file mode 100644 index 00000000..8aec6dc7 --- /dev/null +++ b/scripts/snapshot_check.py @@ -0,0 +1,66 @@ +#!/usr/bin/env python3 +"""Check snapshot lifetimes, the necessity of copying, and plain-value bounds.""" +from pathlib import Path +import os +import subprocess +import tempfile + +ROOT = Path(__file__).resolve().parent.parent +MERE = Path(os.environ.get("MERE", ROOT / "_build/default/bin/mere.exe")) +EXPECTED = b"before 6\n610062\nonce\n1\noutside\n30\n70\n50\nopt 7\n42\n43\n" +NEGATIVE = { + "vec": "snapshot (vec_new ())", + "tuple": "snapshot (1, vec_new ())", + "wrapper": "let f = fn x -> snapshot x; f (vec_new ())", + "alias": "let f = snapshot; f (vec_new ())", + "record": "type Box = { v: Vec[__heap, int] }; let v = vec_new (); let _ = vec_push v 1; snapshot (Box { v = v })", + "variant": "type Box = Empty | Full of Vec[__heap, int]; snapshot Empty", + "nested_recursive": "type 'a Nest = End of 'a | More of Vec[__heap, 'a] Nest; let f = fn (v: int Nest) -> snapshot v; 0", + "function": "snapshot (fn x -> x)", + "borrow": "region R { let b = snapshot (&R 1) in () }", + "file": "let f = fn (v: File) -> snapshot v; 0", + "opaque": "extern type Handle; let f = fn (v: Handle) -> snapshot v; 0", + "forward_wrapper": "let fn snap: 'a -> 'a; let snap = fn x -> snapshot x; snap (vec_new ())", +} + + +def run(args, directory, check=True): + r = subprocess.run([str(a) for a in args], cwd=directory, capture_output=True, timeout=60) + if check and (r.returncode or r.stderr): + raise RuntimeError(f"{Path(str(args[0])).name} failed: {r.stderr.decode(errors='replace')[:1000]}") + return r + + +def main(): + with tempfile.TemporaryDirectory(prefix="snapshot-check-") as d: + tmp = Path(d) + source = (ROOT / "test/parity/snapshot.mere").read_text() + case = tmp / "probe.mere" + case.write_text(source) + code = run([MERE, "-c", case], tmp).stdout + (tmp / "probe.c").write_bytes(code) + for optimization in ["-O0", "-O2"]: + run(["clang", optimization, "-w", "-fsanitize=address,undefined", "-fno-sanitize-recover=all", + "probe.c", "-o", "probe", "-lm", "-lpthread"], tmp) + assert run([tmp / "probe"], tmp).stdout == EXPECTED + marker = 'snapshot (map_get m "k")' + assert source.count(marker) == 1 + case.write_text(source.replace(marker, '(map_get m "k")')) + (tmp / "probe.c").write_bytes(run([MERE, "-c", case], tmp).stdout) + run(["clang", "-O2", "-w", "-fsanitize=address,undefined", "probe.c", "-o", "probe", "-lm", "-lpthread"], tmp) + poisoned = run([tmp / "probe"], tmp, check=False) + assert poisoned.returncode and b"heap-use-after-free" in poisoned.stderr + print("snapshot: O0/O2 ASan/UBSan passed; removing the copy exposes heap-use-after-free", flush=True) + checks = 0 + for name, text in NEGATIVE.items(): + case.write_text(text + "\n") + for flag in [None, "check", "-c", "-ll", "-w", "-rv", "-rv64"]: + args = [MERE, case] if flag is None else [MERE, flag, case] + r = run(args, tmp, check=False) + assert r.returncode and b"snapshot cannot copy" in r.stderr, (name, flag, r.stderr[:500]) + checks += 1 + print(f"snapshot: {checks} plain-value refusal checks passed", flush=True) + + +if __name__ == "__main__": + main() diff --git a/test/parity/factory_inference.mere b/test/parity/factory_inference.mere new file mode 100644 index 00000000..365d94fd --- /dev/null +++ b/test/parity/factory_inference.mere @@ -0,0 +1,24 @@ +// Unannotated factory values acquire one concrete return type from their +// uses, including through aliases and a nested scope with the same name. +let make = vec_new; +let alias = make; +let v = alias (); +let _ = vec_push v 42; +let again = make (); +let _ = vec_push again 43; +let _ = print_int (vec_get v 0); +let _ = print_int (vec_get again 0); +let make_map = map_new; +let m = make_map (); +let _ = map_set m "answer" "forty-four"; +let _ = print (map_get m "answer"); +let nested = fn () -> + let make = vec_new in + let v = make () in + let _ = vec_push v "forty-five" in + vec_get v 0; +let _ = print (nested ()); +let make_owned = owned_vec_new; +with owned = make_owned () in +let _ = owned_vec_push owned 46 in +print_int (owned_vec_get owned 0) diff --git a/test/parity/snapshot.mere b/test/parity/snapshot.mere new file mode 100644 index 00000000..fe2378c3 --- /dev/null +++ b/test/parity/snapshot.mere @@ -0,0 +1,43 @@ +// Snapshots have their own immutable data, even after explicit reclamation. +type Item = { label: str, numbers: int list }; +let m = map_new (); +let _ = map_set m "k" (Item { label = "before", numbers = [1, 2, 3] }); +let _ = map_compact m; +let saved = snapshot (map_get m "k"); +let _ = map_set m "k" (Item { label = "after", numbers = [4, 5] }); +let _ = map_compact m; +let _ = map_recycle m; +let _ = print (saved.label ++ " " ++ str_of_int (list_sum saved.numbers)); +let v = vec_new (); +let _ = vec_push v (bytes_of_str ("a" ++ chr 0 ++ "b")); +let _ = vec_compact v; +let saved_bytes = snapshot (vec_get v 0); +let _ = vec_recycle v; +let _ = vec_push v (bytes_of_str (str_repeat "x" 200)); +let _ = vec_push v (bytes_of_str (str_repeat "y" 200)); +let _ = vec_push v (bytes_of_str (str_repeat "z" 200)); +let _ = vec_push v (bytes_of_str (str_repeat "w" 200)); +let _ = print (hex_of_bytes saved_bytes); +// Argument effects run once in the caller's scope, before copying. +let count = vec_new (); +let _ = vec_push count 0; +let source = fn () -> + let _ = vec_set count 0 (vec_get count 0 + 1) in "once"; +let _ = print (snapshot (source ())); +let _ = print_int (vec_get count 0); +let builder = lb_new (); +let built = snapshot (let _ = lb_push builder "outside" in lb_to_list builder); +let _ = print (str_join "," built); +let copy = snapshot; +let _ = print_int (list_sum (copy [10, 20])); +let _ = print_int (region Outer { list_sum (snapshot [30, 40]) }); +type 'a Box = { value: 'a }; +let boxed = snapshot (Box { value = [20, 30] }); +let _ = print_int (list_sum boxed.value); +let option = snapshot (Some ("opt", [3, 4])); +let _ = print (match option with None -> "missing" | Some (label, xs) -> label ++ " " ++ str_of_int (list_sum xs)); +// Ordinary lexical shadowing still applies to the builtin name. +let f = fn snapshot -> snapshot 41; +let _ = print_int (f (fn x -> x + 1)); +let snapshot = fn x -> x + 2; +print_int (snapshot 41) diff --git a/test/test_basic.ml b/test/test_basic.ml index 2dcc9f94..7a691a63 100644 --- a/test/test_basic.ml +++ b/test/test_basic.ml @@ -4703,20 +4703,20 @@ let () = "typeof(__ref_v)*"; (* --- C codegen: `with` Drop execution (Phase 4.18) --- *) - assert_c "codegen: with binding emit" + assert_c "codegen: with binding uses a C-safe name" (codegen_with_decls "drop type CgConn = { id: int, close: unit -> unit };\n\ let mk = fn id ->\n\ CgConn { id = id, close = fn () -> () } in\n\ with c = mk 1 in c.id") - "__auto_type c ="; + "__auto_type mu_c ="; assert_c "codegen: with calls close field at scope end" (codegen_with_decls "drop type CgConn2 = { id: int, close: unit -> unit };\n\ let mk = fn id ->\n\ CgConn2 { id = id, close = fn () -> () } in\n\ with c = mk 1 in c.id") - "c.mu_close.fn(c.mu_close.env, 0)"; + "mu_c.mu_close.fn(mu_c.mu_close.env, 0)"; assert_c "codegen: with on Drop type without close field omits call" (codegen_with_decls "drop type CgRes = { v: int };\n\