3D: --hoist_locals, --init_locals, --goto_for_early_return, --use_error_handler_macro, etc.#290
Open
tahina-pro wants to merge 77 commits into
Open
3D: --hoist_locals, --init_locals, --goto_for_early_return, --use_error_handler_macro, etc.#290tahina-pro wants to merge 77 commits into
--hoist_locals, --init_locals, --goto_for_early_return, --use_error_handler_macro, etc.#290tahina-pro wants to merge 77 commits into
Conversation
When --hoist_locals is passed, 3d adds -fhoist-locals -fmerge prefix to the KaRaMeL command line, hoisting local variable declarations to the top of each C function and merging variables that share a common name prefix. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When --init_locals is passed with a value (c23, c99, or c89), 3d passes -finitialize-locals <value> to KaRaMeL, initializing all local variable declarations with zero values using the specified C standard's syntax. By default (when --init_locals is not set), -finitialize-locals no is passed to disable initialization. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The --init_locals and --hoist_locals options were only being passed to
KaRaMeL for F*-extracted C code. The C files directly generated by 3d
(notably *Wrapper.c) were not honoring these options.
With --init_locals, uninitialized local variable declarations now get
zero initializers: = { 0 } for structs (c99/c89), = { } (c23), and
= 0 for scalars/pointers.
With --hoist_locals, all local variable declarations are hoisted to
the top of each function body, with initializers separated into
assignment statements.
When both options are used together, hoisted declarations get zero
initializers.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…aramana_krml_hoist_locals
Pass -goto_for_early_return to KaRaMeL when generating C code, following the same pattern as --hoist_locals. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…into _taramana_20260423
The proof in this module needed a higher z3rlimit to verify successfully. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…ept for Docker image
Pass -fblank-lines and -fline-comments to Karamel when the corresponding 3D command-line options are set. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Step 1: Only generate wrapper entry points that users explicitly declare. - Probe-only types get only probe wrappers in the header - Plain-only types get only the main Check wrapper - Both can be declared together for full set of wrappers - Internal main wrapper is always generated (static when not public) Step 2: Named entrypoints via entrypoint(Name) syntax. - entrypoint(Foo) generates the main wrapper named 'Foo' - entrypoint(Bar) probe ... generates the probe wrapper named 'Bar' - Without a name, auto-generated names are used as before - Probe wrappers call the main wrapper by its effective name Updated files: - Ast.fst: Extended Entrypoint attribute with optional name parameter - Binding.fst: Allow plain + probe entrypoints to coexist - Target.fst/fsti: Conditional wrapper generation with custom naming - TranslateForInterpreter.fst: Propagate entrypoint names to Target IR - Desugar.fst, Simplify.fst, Deps.fst: Updated pattern matches - parser.mly: Grammar rules for entrypoint(Name) syntax - Tests: Added test cases demonstrating both features Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Updated 3d-lang.rst to document selective entrypoint generation: only explicitly declared entry points appear in the public header - Updated 3d-lang.rst to document named entrypoints (entrypoint(Name) syntax) - Added examples to doc/Probe.3d with SNIPPET markers for RST inclusion - Updated 3d-snapshot/ files to reflect new behavior: - ProbeCheckIndirect removed (only probe entrypoint declared) - ProbeCheckMultiProbe removed (only probe entrypoints declared) - New examples: ProbeOnly, BothEntrypoints, NamedPlainEp, NamedProbeEp, NamedBothEp - Updated existing documentation for Indirect and MultiProbe examples to match new selective generation behavior Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
When --goto_for_early_return is passed to 3d, the generated wrapper code now uses the single-exit-point goto pattern, consistent with what KaRaMeL generates for the main validator code: - Main (buffer) wrappers: BOOLEAN result__ = FALSE; ... goto exit; ... result__ = TRUE; exit: return result__; - Probe wrappers: uint32_t result__ = ...; ... result__ = ERROR; goto exit; ... result__ = EVERPARSE_SUCCESS; exit: return result__; Also fixes a pre-existing bug where the validation call in probe wrappers was missing a closing parenthesis. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Adds src/3d/tests/goto_return/ with: - GotoReturn.3d: minimal test with plain entrypoint + probe entrypoint - snapshot/: expected output when --goto_for_early_return is passed - Makefile: generates and diffs against snapshot Run with: make -C src/3d/tests/goto_return Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Selective entrypoint generation and named entrypoints for the 3d compiler
Add a new `--use_error_handler_macro` 3D CLI option (default off).
When set, the generated F* and C code uses a C macro
`EVERPARSE_ERROR_HANDLER_MACRO` (from a user-supplied header,
typically wired via --add_include) for error reporting, instead of
the dynamic error-handler callback parameter that is normally threaded
through every validator.
Implementation:
* EverParse3d.Actions.Base.fst{i}, Actions.All.fsti, Interpreter.fst:
thread a `use_error_handler:bool` parameter through the prelude.
The error-handler field is typed
`if use_error_handler then error_handler else unit`, and
combinators dispatch at runtime to either the dynamic handler or
the `[@@cmacro] assume val error_handler_macro: error_handler`.
* InterpreterTarget.fst: the 3D frontend emits a literal `true`/`false`
for the bool when generating F* code, so KaRaMeL specialises and
C extraction drops the unused handler argument entirely. The literal
is the negation of `Options.get_use_error_handler_macro ()`.
* Target.fst: when the option is set, the generated C wrapper omits
the static `DefaultErrorHandler` and the `&DefaultErrorHandler`
argument from the validator call, to match the dropped parameter.
* Options.fst{i}: register `--use_error_handler_macro` and expose
`get_use_error_handler_macro`.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add tests/use_error_handler_macro, a small standalone test that exercises the new --use_error_handler_macro option end-to-end: * src/Test.3d defines a tiny format with a refinement constraint, so the generated validator triggers the error path on both not-enough-data and constraint-failed inputs. * src/MyErrorHandlerMacro.h is a handwritten header defining EVERPARSE_ERROR_HANDLER_MACRO; it is injected into every generated .c/.h file via --add_include. * src/main.c links against the EverParse-generated wrapper and feeds it three inputs (valid, constraint-violating, too short), checking that the macro is invoked on the latter two. * Makefile drives 3d.exe with --use_error_handler_macro and the --add_include flag, builds with the generated EverParse.Makefile, and runs the test program. Wired into src/3d/tests/Makefile so 'make 3d-test' exercises it. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…total_zero_parser' The proof of validate_dep_pair_with_refinement_and_action_total_zero_parser' (introduced in the use_error_handler_macro changes) needs ifuel 2 to discharge its post-condition. Without it, F* reports 'Could not prove post-condition' with 'incomplete quantifiers' even at high rlimit. Diagnosed via --split_queries always: queries project-everest#42 and project-everest#57 fail at the default ifuel 1 and succeed at ifuel 2. Add --ifuel 2 to the surrounding push-options to stabilize the proof. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The 'let eh : error_handler = error_handler_fn' pattern (introduced to
coerce error_handler_fn out of its dependent type
'if use_error_handler then error_handler else unit') was being extracted
to KaRaMeL as a local C variable per call site, e.g.
'EVERPARSE_ERROR_HANDLER eh = ErrorHandlerFn; eh(...)'.
Annotate each such let-binding with [@inline_let] so KaRaMeL inlines it,
restoring the previous code shape ('ErrorHandlerFn(...)' direct call).
Verified by regenerating the 3d-doc-snapshot: no diff against the
pre-existing snapshot.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The default `if: success()` on a job evaluates over the transitive upstream needs chain, so when `only_build_3d` was checked, the `test-interop-*`, `test-docker`, `ci-*`, and macOS/Linux `build-*` jobs would be skipped and the `success()` propagation would then implicitly skip `push-release` (and `delete-release`, `push-release-branch`) even though their direct dependency `push-tag` ran successfully via its own `!cancelled() && !failure()` opt-in. Give `push-release` and `delete-release` the same `!cancelled() && !failure()` opt-in so they run as soon as `push-tag` succeeds, regardless of whether transitive ancestors were skipped. This also publishes a Windows-only 3D prerelease for `only_build_3d` runs. `push-release-branch` is intentionally left alone so the `_release` branch is not advanced by 3D-only builds. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…m/tahina-pro/quackyducky into _taramana_20260429
Add a 'version' text input so users can specify a version number manually instead of relying on the auto-computed date-based default. When left empty, the existing vYYYY.MM.DD computation is used. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…l/ subdir When the only reference to EverParse3d.Actions.Common.error_handler is in a function body (e.g., in tests built with --use_error_handler_macro, where validators no longer take an error_handler parameter), Karamel's visibility fixpoint leaves error_handler at Internal and emits it to internal/EverParse.h. By marking EverParse3d.Actions.Common as the API of the EverParse bundle, its decls skip the mark_private step (Bundles.ml:79: `is_api` branch) and stay Public. Karamel then emits the typedef into EverParse.h instead of internal/EverParse.h, and no internal/ subdirectory is created. The handwritten src/3d/prelude/buffer/EverParse.h already provides the same typedefs (EVERPARSE_ERROR_HANDLER, EVERPARSE_ELOC, EVERPARSE_APP_CTXT, EVERPARSE_APP_CTXT_ERROR_PRE), and with_preserved_everparse_h preserves it across Karamel runs, so the public header content is unchanged for all tests. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The bundle change in 070b0f14b ("3d: include EverParse3d.Actions.Common as
bundle API to avoid internal/ subdir") promotes EverParse3d.Actions.Common
to the bundle API, which keeps all of its public decls visible to Karamel.
This means that decls representing Low* memory locations (eloc, eloc_none,
app_loc) and spec-only logical propositions (app_ctxt_error_pre) would
otherwise leak into the extracted EverParse.h as opaque void * typedefs.
Mark them `noextract [@@noextract_to "krml"]` so Karamel skips them.
The runtime-relevant decls (app_ctxt, input_buffer_t, error_handler) are
left untouched.
Verified with `make -j 16 3d`; the three prelude EverParse.h files
(buffer, extern, static) are byte-identical to before.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Following the same pattern as the previous commit, mark the remaining
spec-only logical propositions that were extracted as opaque `void *`
typedefs in the prelude EverParse.h files:
- EverParse3d.CopyBuffer.inv (`HS.mem -> prop`)
=> EVERPARSE_INV in buffer/, extern/, static/ EverParse.h
- EverParse3d.CopyBuffer.liveness_preserved (`prop`)
=> EVERPARSE_LIVENESS_PRESERVED in buffer/, extern/, static/ EverParse.h
- EverParse3d.InputStream.Buffer.Aux._live (`Tot prop`)
=> EVERPARSE__LIVE in buffer/ EverParse.h
All three are bundle-API decls (CopyBuffer is in every bundle;
InputStream.Buffer.Aux is in the buffer bundle), so without
`noextract [@@noextract_to "krml"]` Karamel keeps them Public and
emits them as void * typedefs.
After this change, the three generated prelude EverParse.h files
contain no remaining `typedef void *` declarations.
Verified with `make -j 16 3d`.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…-pro/quackyducky into _taramana_20260429
This reverts commit 52e0196.
…aramana_3d_202606
…aramana_3d_202606
validate_pair's constant-size fast path fuses constant-size, total,
action-free fields into a single length check, erasing their per-field
error handlers. As a result, failures of length-only structs (and of a
constant-size suffix following a variable-size prefix) were not reported
to the error handler. Re-wrap the fused check with
validate_with_error_handler so such failures report their type/field
name; the innermost handler still wins via the fill-once error frame, so
no redundant reports are produced for non-length-only types.
Also stabilize two validator proofs that regressed with the F*/Karamel
upgrade (validate_dep_pair_with_refinement{,_and_action}_total_zero_parser'):
their VCs are provable per-subgoal but too large as a single monolithic
query, so guard them with --split_queries always (each subgoal uses < 10
rlimit).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…aramana_3d_202606_error_reporting
This reverts commit 33e603c.
…aramana_3d_202606
…dler_macro works with type-specialized/coerce probes Under `--use_error_handler_macro`, validators drop the dynamic `EVERPARSE_ERROR_HANDLER` function-pointer argument and instead invoke the `EVERPARSE_ERROR_HANDLER_MACRO` C macro directly. The probe monad (`EverParse3d.ProbeActions.probe_m`) did not follow this convention: it always baked the error handler in as a first-class `error_handler` value. For plain probes this was harmless because `run_probe_m` is fully inlined (so the macro is always applied, never passed as a value), but for type-specialized (`specialize`) and coerce probes the probe functions are extracted as standalone, shared functions that take the handler as a function-pointer parameter. Passing the `[@@cmacro]` `error_handler_macro` as a value then emitted a bare `EVERPARSE_ERROR_HANDLER_MACRO` identifier, which does not compile ("undeclared identifier"). Align the probe actions with the validators by parameterizing the probe monad by `use_error_handler`, exactly as `validate_with_action_t` and `action` already are: - Move `error_handler_macro` to EverParse3d.Actions.Common so it is reachable from EverParse3d.ProbeActions (Base already opens Common). - Index `probe_m` by `use_error_handler`; the handler parameter becomes `(if use_error_handler then error_handler else unit)`, so KaRaMeL erases it in macro mode. Thread the index through every combinator and add a `handle_probe_error` helper that dispatches to the callback or the macro at each error-reporting site. - Thread `use_error_handler` through the interpreter probe layer (`probe_m_unit`, `probe_action`, `atomic_probe_action_as_probe_m`, `probe_action_as_probe_m`, `t_probe_then_validate[_alt]`, `Action_probe_then_validate`) and update `probe_then_validate` in EverParse3d.Actions.Base to forward the indexed handler to `run_probe_m`. - Emit the compile-time boolean in the generated code: `Target.print_typ` applies `probe_m_unit` to it, and the `Probe_function` emitter fixes it on `probe_action_as_probe_m`. In dynamic mode the generated C is unchanged; in macro mode the probe helpers now drop the handler parameter and call `EVERPARSE_ERROR_HANDLER_MACRO` directly, just like the validators. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add a regression test that builds the type-specialized/coerce probe
example (../specialize_test) with `--use_error_handler_macro`. Before
the accompanying probe-actions fix, the generated core validator failed
to compile because the specialized probe helpers took the error handler
as a function-pointer argument and were handed the
`EVERPARSE_ERROR_HANDLER_MACRO` macro as a bare value. The test now
compiles and runs ("All tests passed").
Enable it from src/3d/tests/Makefile (all, dedicated target, and clean).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The z3 test-case generator (Z3TestGen.fst) hand-writes a C test harness (testcases.c) that calls the generated validators. It unconditionally defined a `TestErrorHandler` callback and passed `&TestErrorHandler` as an argument to every validator call. Under `--use_error_handler_macro`, however, the generated validators drop the `EVERPARSE_ERROR_HANDLER` parameter (they invoke the `EVERPARSE_ERROR_HANDLER_MACRO` C macro directly), so the harness failed to compile with "too many arguments to function". Make the harness respect the option, across all three generation modes (--z3_test, --z3_diff_test, --test_checker): - Omit the `&TestErrorHandler` argument from validator calls in macro mode (keeping the `&context` / Ctxt argument), via a shared `test_error_handler_call_arg` helper, in both the witness-call printer and the standalone test-checker's mmap main. - Split the harness preamble so the `TestErrorHandler` definition is emitted only in dynamic mode (otherwise it would be an unused function), while the always-needed `witness_layer_t` typedef is kept. The harness verdict (ACCEPTED/REJECTED) is derived from the validator's return value, so it is unaffected; in macro mode the per-witness error diagnostics are produced by the user-provided EVERPARSE_ERROR_HANDLER_MACRO instead of TestErrorHandler. Dynamic-mode output is unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add a test that exercises the z3 test-case-generation modes under `--use_error_handler_macro`. It is a copy of ../probe adapted to build with the macro option (src/MyErrorHandlerMacro.h, injected via --add_include), and it drives all three Z3TestGen modes: - `testgen` (--z3_test) - `difftest` (--z3_diff_test, via an added namedPlainVariant type) - `checkertest` (--test_checker) - `eprobetest` (--z3_test on an `entrypoint probe` type) plus the core validator `test`. src/Makefile additionally runs the batch z3-testgen in macro mode. Together with the accompanying Z3TestGen fix, all of these now compile and run: in macro mode the harness omits the `&TestErrorHandler` argument and the validators call EVERPARSE_ERROR_HANDLER_MACRO directly. Enable it from src/3d/tests/Makefile (all, dedicated target passing 3D_Z3_EXECUTABLE, and clean). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
1. New 3D command‑line options
Six new options were added to
src/3d/Options.fst{,i}. For each one we listthe 3D‑side commits, the wiring in
src/3d/ocaml/Batch.ml, and the matchingKaramel commits between
5b438411anddcba036e.This PR switches the Karamel branch to
everparse-2026.061.1
--hoist_localsfunction (
--batchonly)".fadf621ac"Add--hoist_localsoption to 3d" — registers the option inOptions.fst{,i}and, inBatch.ml, prepends-fhoist-locals -fmerge prefixto the KaRaMeL command line (the
-fmerge prefixpart was later dropped).66e216c0a"do not rely on krml -fmerge" —Batch.mlno longer relies onKaRaMeL's
-fmerge(after upstream changes the merge pass is integrateddifferently).
d54f9ac6b"3d: honor--init_localsand--hoist_localsin generatedC files" — propagate the option to wrapper generation in
Target.fst.lib/, mostlyHoistLocals.ml,MarkMaybeUnused.ml, plus tests undertest/):76e630eb"Add-fhoist-localspass to hoist local declarations tofunction top".
6fed2a38"HoistLocals: preserve comment ordering, hoist from blocks andarrays".
b9f7c172"AddMarkMaybeUnusedpass for hoisted locals in#ifbranches".
f0ba3dd1"MarkMaybeUnused: insert markers inside#if/#elsebranches".5fd824c3"Fix missingGoto/Labelcases inMarkMaybeUnused.vars_of_stmt".867a130b"run hoist-locals, initialize-locals tests".24894467"revert krmllib changes".1.2
--init_locals(c23|c99|c89)0e189f292"Add--init_localsoption to 3d" — registers the option inOptions.fst{,i}(string option restricted toc23/c99/c89), and inBatch.mlpasses-finitialize-locals <c23|c99|c89|no>to KaRaMeL.d54f9ac6b(same commit as for--hoist_locals) propagates the option towrapper generation in
Target.fst.d55c7155"Add-finitialize-localspass with c23/c99/c89 modes".5012ed6c"Add test suite for-finitialize-locals".867a130b"run hoist-locals, initialize-locals tests".1.3
--goto_for_early_returngotofor early return in generated C code (--batchonly)".
60985e931"3D: add--goto_for_early_returncommand-line option" —registers the option in
Options.fst{,i}and, inBatch.ml, passes-goto_for_early_returnto KaRaMeL.7f05951c3"feat(3d): Support--goto_for_early_returnin generatedwrappers" — emit wrappers with a single exit‑via‑goto control flow when
the option is set (
Target.fst).df634c7ab"test(3d): Add snapshot test for--goto_for_early_return"— new
src/3d/tests/goto_return/directory (GotoReturn.3d,Makefile,snapshot/GotoReturnWrapper.{c,h}).a9391fa97"wrapper.c:DECLARE frame; frame =->DECLARE frame ="(small wrapper tweak to align with the new KaRaMeL output).
b313cd3a"Add-goto_for_early_returntransformation".8933e3a0"Label with payload statement in C11" (needed to express agoto‑target labelled statement).f129cf9f"Remove redundant trailing goto before exit label".578f3f69"Add Pulse test case to GotoReturn".ab6ea241"Refactor: movecollect_namestoCStar.ml, move test topulse dir".
1.4
--blank_linesin generated C code (
--batchonly)".5dc7521da"Add--blank_linesand--line_comments3D options" —registers the option in
Options.fst{,i}and, inBatch.ml, passes-fblank-linesto KaRaMeL when the option is set.4807cb409"Add blank line beforeexit:label in generated wrappers",f454edb9e"Add blank lines before and after comment blocks inwrappers",
89fde5bda"Add blank line between#includeblock anddeclarations in wrappers",
71a4f5772"Format generated wrappers tomatch KaRaMeL style" — adjust the 3D wrapper printer (
Target.fst) sothat wrapper code matches the new KaRaMeL output style.
f721ab10"Add-fblank-linesoption for readable C output".25c4e489"Blank line before labels; fuse adjacent line comments".46474e0d"Add test coverage for-fline-commentsand-fblank-lines".1.5
--line_comments// ...) instead of block comments(
/* ... */) in generated C code (--batchonly)".5dc7521da(same commit as--blank_lines) — inBatch.ml, passes-fline-commentsto KaRaMeL.a42e24fce"Use KaRaMeL-fline-commentsstyle for wrapper comments" —adjust the 3D wrapper printer in
Target.fst.bbd523d3"Add-fline-commentsoption for C line comment style".25c4e489"Blank line before labels; fuse adjacent line comments".6d386864"Add test for adjacent comment fusion with-fline-comments".46474e0d"Add test coverage for-fline-commentsand-fblank-lines".1.6
--use_error_handler_macroEverParse3dErrorHandlerMacroinstead ofthe dynamic error handler".
c95e67531"3d: add--use_error_handler_macrooption" — major change:thread a fresh
use_error_handler : boolparameter through the prelude(
EverParse3d.Actions.Base.fst{,i},Actions.All.fsti,Interpreter.fst); the field isif use_error_handler then error_handler else unit; combinators dispatch at runtime to either the dynamic handleror a
[@@CMacro] assume val error_handler_macro: error_handler. The 3Dfrontend (
InterpreterTarget.fst) emits the bool as a literal so KaRaMeLspecializes away the handler argument;
Target.fstomitsDefaultErrorHandlerfrom generated C wrappers when the option is set.1eea34c9e"the error handler function type shall no longer beinline_for_extraction" (EverParse3d.Actions.Common.fst).5da1b69af"exposeEVERPARSE_ERROR_HANDLERas a typedef inEverParse.h": addsEverParse3d.Actions.Commonto the EverParse bundleAPI in
src/3d/prelude/{buffer,extern}/Makefile, and insrc/3d/ocaml/Batch.mlpasses-no-inline-type-abbrev EverParse3d.Actions.Common.error_handlerto KaRaMeL.
81144fe5c"3d: includeEverParse3d.Actions.Commonas bundle API toavoid
internal/subdir".8091fa111and6d493a3ed"3d/prelude: mark spec-only defs inActions.Common/ remaining asnoextract".e30561c61"3d: inline let-bindings forerror_handlercoercion".6e9d8b9a3"3d: test for--use_error_handler_macro" — new testdirectory
src/3d/tests/use_error_handler_macro/withMakefile,src/Test.3d,src/MyErrorHandlerMacro.h,src/main.c,.gitignore.dcba036e"SupportCMacroattribute onassume valdeclarations" —extends
[@ CMacro]handling inlib/AstToCStar.mlso thatassume val f : ...decorated withCMacrois treated as a macroinvocation (uppercased name, no
externemitted). This is what makes theerror_handler_macromechanism work end‑to‑end.23893654"Add-no-inline-type-abbrevto preserve type abbreviations"— implements the new KaRaMeL flag used by
Batch.ml, so theerror_handlertype abbreviation survives extraction and is emitted asthe
EVERPARSE_ERROR_HANDLERtypedef inEverParse.h. Also changeslib/Output.mlso that a dep‑derived include is dropped if an explicit-add-includealready requests it (preserving the order requested bythe 3D driver).
2. Other
src/3d/changesSource‑level (not CLI) changes:
c58dd0764"feat(3d): Selective entrypoint generation and namedentrypoints" — extends the 3D
entrypointattribute with optional naming(
entrypoint(Foo)) and only generates the wrappers actually declared by theuser (probe‑only, plain‑only, or both). Touches
Ast.fst,Binding.fst,Desugar.fst,Simplify.fst,Deps.fst,Target.fst{,i},TranslateForInterpreter.fst,ocaml/parser.mly, and adds test cases undersrc/3d/tests/probe/src/Probe.3d.c37dfc70a"Rename validator result toep_status, use result forwrapper return value" (
Target.fst).3a49674b8"UseEVERPARSE_PROBE_FAILURE_INITinstead of undefinedEVERPARSE_PROBE_FAILURE_UNIMPLEMENTED" (Target.fst).0aeea5131"do not require--batch" (Options.fst).4d24eb8cf"refactor: replaceU64.ltewithU64.gte(operands swapped)in 3d prelude".
1c9ba7ee0"3d: bumpifuelto 2 forvalidate_dep_pair_with_refinement_and_action_total_zero_parser'".437b36ac9"reorder 3d tests in Makefile to avoid a merge conflict".The huge churn in
src/3d/Target.fst(≈ 3441 lines changed) andsrc/3d/prelude/EverParse3d.Interpreter.fst(≈ 526 lines) is mainlyre‑indentation and re‑factoring driven by
--use_error_handler_macro,selective entrypoints, and the wrapper formatting cleanups listed above.
3.
.github/changesOnly
.github/workflows/release.ymlwas modified (+37/−2 lines). Thecommits are:
162dab1a6(PR copilot) "Add 'Only build 3D' checkbox to release workflow"— new
only_build_3dworkflow_dispatchboolean input. When set, therelease pipeline skips
build/test-macos,build/test-linux,test-interop-*,build/test-docker,ci-linux,ci-macos,push-docker,delete-dockerand passesEVERPARSE_ONLY_3D=1to theWindows packaging step.
1e619479c"release workflow: add optional version input toworkflow_dispatch" — new
versionstring input; when empty, the existingvYYYY.MM.DDdefault is computed.9067f6e60"EVERPARSE_NO_DIFF->EVERPARSE_CHECK_DIFF; check diff forrelease except for Docker image" —
ci-linuxandci-macosnow run withEVERPARSE_CHECK_DIFF=1.f989e333"release.yml: runpush-release/delete-releasewhenpush-tagsucceeds" — givepush-release,delete-release,delete-branch,push-docker,delete-docker,push-tagan explicitif: !cancelled() && !failure()so that the post‑tag jobs run even whenthe
only_build_3dmode skipped most of their transitive dependencies;also add
test-windowsto thepush-tagneedslist.4. Karamel changes between
5b438411anddcba036eFor completeness, the full list of non‑merge Karamel commits in that range
that are not listed above (these are unrelated to any new 3D CLI option,
but they are part of what the new Karamel branch picked up):
7a759ff4"Add unit test for ETApp handling in SimplifyMerge".24d74f9c"Fix ETApp crash in SimplifyMerge".373ebda2"Fix UInt8/UInt16 bitwise NOT (lognot) not masked (#690)".5fd8ab45"Fix UInt8/UInt16 comparison after wrapping arithmetic (#694)".bd71b9de"Two improvements to Rust code-gen, related to loops".c96d44be"GenCTypes: Use ppxlib stable AST builder, fixed build withOCaml 5.4.0".
29b5b443"ci: make sure to use OCaml 5.3.0 in all jobs".4dad2cc9,c64c756d,07fcbe9e,9dc9097a,f62043c5— Pulse testinfrastructure (
test/pulse/).4494c624,761dc42c,a2811dac— minor CI /Utils.mltweaks.In total, 48 commits were added on top of the ancestor
5b438411, of which≈ 14 directly implement the KaRaMeL side of the new 3D CLI options
(
-fhoist-locals,-finitialize-locals,-goto_for_early_return,-fblank-lines,-fline-comments,-no-inline-type-abbrev, and theCMacroextension forassume val).