Skip to content

fix: soundness recovery for wrapped libs, ppx-runtime, virtual-impl deps#14517

Draft
robinbb wants to merge 2 commits into
robinbb-14492-l4-tight-branchfrom
robinbb-14492-l5-soundness
Draft

fix: soundness recovery for wrapped libs, ppx-runtime, virtual-impl deps#14517
robinbb wants to merge 2 commits into
robinbb-14492-l4-tight-branchfrom
robinbb-14492-l5-soundness

Conversation

@robinbb
Copy link
Copy Markdown
Collaborator

@robinbb robinbb commented May 13, 2026

Layer 5 of 9 of #14492.

Restores correctness for three cases the bare BFS filter mishandles: virtual-impl deps (fall back to glob via has_virtual_impl), wrapped local libs reached through the wrapper name (glob the wrapped lib's Lib.closure), and ppx_runtime_libraries introduced by pps (glob their Lib.closure).

Module_compilation.lib_deps_for_module: reads has_virtual_impl and falls back to glob if true; reads pps_runtime_libs and folds them into direct_libs; computes wrapped_libs_referenced and unions with pps_runtime_libs under Lib.closure to produce must_glob_libs; the classification fold sends every must_glob_set member to the glob path.

Modules.Wrapped.entry_modules returns the wrapper plus every wrapped_compat shim. Modules.entry_modules's wrapped case switches to use it; in transition wrapped libs the index now sees the bare module names consumers can resolve.

Adds 8 new soundness fixtures (cross-lib-instrumentation-barrier.t, cross-lib-preprocess-barrier.t, cross-lib-pps-runtime-no-ocamldep-barrier.t, wrapped-from-vlib-soundness.t, wrapped-transition-soundness.t, mixed-per-module-preprocess.t, mixed-per-module-preprocess-precision.t, cmx-native-tight-deps.t). Lands the changelog (doc/changes/added/14492.md).

The five cram tests broken on layer 4 pass again here.

Stack: rebases on #14516. Next: #14518.

Part of #14492. Related to #4572.

@robinbb robinbb self-assigned this May 13, 2026
@robinbb robinbb force-pushed the robinbb-14492-l4-tight-branch branch from da056f0 to a0893d7 Compare May 14, 2026 00:35
@robinbb robinbb force-pushed the robinbb-14492-l5-soundness branch from c82233e to 0373a72 Compare May 14, 2026 00:35
@robinbb robinbb force-pushed the robinbb-14492-l4-tight-branch branch 3 times, most recently from 4e63363 to 4c95b95 Compare May 15, 2026 01:31
@robinbb robinbb force-pushed the robinbb-14492-l5-soundness branch from 0373a72 to a94a5c6 Compare May 15, 2026 02:57
@RyanJamesStewart
Copy link
Copy Markdown

While going through must_glob_libs against the cases #14516 narrows away, I
think I have a fourth genuinely-needed class that the three recovery branches
(has_virtual_impl, wrapped_libs_referenced, pps_runtime_libs) do not
cover.
It is not a regression in #14517 as it stands; the default build is still
exit 0. It is a soundness incompleteness in the recovery set plus a latent
stale-rebuild hazard, and it becomes a hard default-build regression at the
next layer (#14518). Reproduction first, then the mechanism and the bounding.

Three directories, all (wrapped false) on the intermediate, with the token
that names the third library absent from every source file on both ends:

$ cat > dune-project <<'EOF'
(lang dune 3.23)
EOF
$ mkdir prelude middle consumer
$ cat > prelude/dune <<'EOF'
(library (name prelude) (wrapped false))
EOF
$ cat > prelude/prelude.ml <<'EOF'
type color = Red | Green | Blue
EOF
$ cat > middle/dune <<'EOF'
(library
 (name middle) (libraries prelude) (wrapped false)
 (flags (:standard -open Prelude)))
EOF
$ cat > middle/middle.mli <<'EOF'
val pick : unit -> color
EOF
$ cat > middle/middle.ml <<'EOF'
let pick () = Green
EOF
$ cat > consumer/dune <<'EOF'
(executable (name consumer) (libraries middle prelude))
EOF
$ cat > consumer/consumer.ml <<'EOF'
let () = match Middle.pick () with
  | Green -> print_endline "g"
  | Red | Blue -> print_endline "nb"
EOF
$ dune build --sandbox=copy consumer/consumer.exe

middle.mli surfaces color, which is Prelude.color, but middle is built
with (flags (:standard -open Prelude)) so the token Prelude appears in no
source file under middle/, and consumer never names Prelude either. The
consumer's compile genuinely needs prelude.cmi to resolve the color
constructors, but ocamldep -modules reports Prelude for neither side, so
the per-module BFS in #14516 never reaches prelude, and none of #14517's
three recovery branches re-add it (prelude is not wrapped, not a ppx-runtime
lib, not a virtual-impl).

The --sandbox=copy build is the discriminator here, since a copy sandbox
contains exactly the rule's declared deps. That is the same soundness oracle
the in-stack fixtures use (cross-lib-preprocess-barrier.t,
wrapped-from-vlib-soundness.t). Built from the stack heads:

dune state what this commit is, in plain terms dune build --sandbox=copy consumer/consumer.exe
d57d159 stock, before the per-module dep filter exit 0
4c95b95 #14516 head: the per-module filter on, recovery not yet added exit 1, Error: Unbound constructor "Green"
a94a5c6 #14517 head: filter plus the must_glob_libs recovery exit 1, Error: Unbound constructor "Green"

#14517 fails identically to #14516, so the recovery layer does not close this
class.

Mechanism, from dune rules on the consumer compile action:

The source-level reason the BFS cannot see it: Ocaml_flags .extract_open_module_names parses -open from the consumer's own flags only;
it does not consult the dep library middle's stanza flags, and ocamldep on
middle's source emits nothing for Prelude because it is -open'd away.

One rebuttal worth pre-empting: it is not a missing user declaration. With
consumer/dune set to (executable (name consumer) (libraries middle prelude)) (the dep declared explicitly), #14517 still drops prelude.cmi
from the consumer compile rule and --sandbox=copy still fails Unbound constructor "Green". The library closure is correct; the per-module cmi-dep
derivation is what is incomplete. prelude.cmi is the only supplier of the
color constructors (middle.cmi only references Prelude.color), so this
is a dropped-only-supplier case, not a precision win over a redundant edge.

On scope, to keep this honestly bounded:

One structural note that might be useful for the fixture set rather than the
fix: the existing -open tests (wrapped-reexport-via-open-flag.t,
auto-wrapped-child-reexport.t) put -open on the wrapper/consumer side and
re-export through a module alias via a wrapped lib, both of which the recovery
does handle (exit 0 here, including under --sandbox=copy). Their oracle is
dune build @check plus rebuild-counting, and under that non-sandbox oracle
this fixture is invisible on #14517 (the @check alias build is exit 0).
--sandbox=copy (the stack's own convention in the soundness fixtures) is
what surfaces it.
The unwrapped-intermediate, type-via-.mli-inference, token-absent
conjunction is the shape that slips past both the BFS and the current -open
fixtures.

I have a discriminating cram fixture in the per-module-lib-deps/ style using
the --sandbox=copy convention (fails pre-recovery and still fails on #14517
head; would pass once the class is recovered). Happy to attach it if it is
useful, or to defer entirely on where the recovery belongs.

robinbb added a commit that referenced this pull request May 17, 2026
Closes a soundness gap in the per-module narrowing pipeline missed
by the wrapped / ppx-runtime / virtual-impl recoveries: when a
dependency library's stanza injects [-open M] via [(flags (...))],
its source can reference [M]'s identifiers without naming [M], and
ocamldep emits no token to drive the cross-library walker.

Reported by RyanJamesStewart on #14517 with this fixture: an
unwrapped [middle] depending on unwrapped [prelude] with
[(flags (:standard -open Prelude))], exposing
[val pick : unit -> color] (where [color] resolves through the open
to [Prelude.color]). The consumer pattern-matches the result
against bare constructors. The compile genuinely needs [prelude.cmi]
to resolve the constructors; the BFS over [ocamldep -modules]
cannot reach [prelude] (no syntactic [Prelude] token on either
side); the three existing recoveries do not catch it ([prelude] is
not wrapped, not a ppx-runtime lib, not a virtual-impl).

[Module_compilation.cross_lib_tight_set]:
- Add [~mode] (the consumer's compile mode) so we can expand a dep
  lib's stanza flags via [Ocaml_flags.get].
- Extend [read_entry_deps] to compute [read_stanza_opens] for the
  visited lib and union the result into the BFS frontier. Localised
  in the BFS rather than the initial-frontier computation so the
  reachability rule reads as: a module is reachable iff the consumer
  references it, or some reached module's ocamldep names it, or some
  reached module's owning lib stanza-opens it. Returns empty for
  [Spec.standard] (short-circuits external libs).

[Lib_info]:
- Add [stanza_flags : Dune_lang.Ocaml_flags.Spec.t] field plus
  accessor. Local libs carry their stanza's [conf.buildable.flags];
  external libs ([findlib], [dune_package]) carry [Spec.standard].

Regression test: [cross-lib-open-flag-barrier.t]. Fails on L4 and
L5 head before this patch (Unbound constructor Green under
[--sandbox=copy]); passes after.
@robinbb
Copy link
Copy Markdown
Collaborator Author

robinbb commented May 17, 2026

Thanks for the careful reproduction — the gap is real and now fixed.

The diagnosis matches what I see: ocamldep on middle's source emits no token for Prelude because the -open removes the need to name it, so the BFS cannot reach prelude, and prelude is not wrapped / not a ppx-runtime lib / not a virtual-impl, so none of the three existing must_glob_libs recoveries catch it. Under --sandbox=copy the consumer's compile fails at L5 head; at L6 it becomes a hard default-build regression once filtered_include_flags removes the wide -I that was masking the missing tracked dep.

The fix sits inside the BFS rather than alongside the existing must_glob_libs set: the per-iteration step now extends the frontier with the modules named by each visited library's stanza -open flags, in addition to the entry's impl + intf ocamldep raw refs. The reachability rule becomes a three-way disjunction (consumer references it, or some reached module's ocamldep names it, or some reached module's owning lib stanza-opens it), which closes the gap through the same fixpoint that handles ocamldep-visible references. Chosen over the alternative — extending the BFS's initial referenced set with stanza opens of all cctx libs — because the BFS-internal version is both more precise (only reached libs contribute) and reads more clearly in code.

Regression test landed at test/blackbox-tests/test-cases/per-module-lib-deps/cross-lib-open-flag-barrier.t — same shape as your fixture, asserts dune build --sandbox=copy consumer/consumer.exe succeeds. Fails on L4 and L5 head before this patch (Unbound constructor Green), passes after. The fourth recovery class is also documented in doc/dev/per-module-narrowing.md (the algorithm reference added in L9).

Commit: 34a19142a3 fix: BFS-expand through dep libs' stanza -open modules on L5; the L6..L9 chain has been rebased and #14492 cherry-picked to match.

@robinbb
Copy link
Copy Markdown
Collaborator Author

robinbb commented May 17, 2026

@RyanJamesStewart Please verify whether the cram test that you volunteered to attach is covered by the newly added test cases. Are you an LLM that is running wild, fixing "highly active" PRs? What criteria do you use to find PRs to which to contribute? Does @stuboo monitor your work?

robinbb added a commit that referenced this pull request May 17, 2026
Closes a soundness gap in the per-module narrowing pipeline missed
by the wrapped / ppx-runtime / virtual-impl recoveries: when a
dependency library's stanza injects [-open M] via [(flags (...))],
its source can reference [M]'s identifiers without naming [M], and
ocamldep emits no token to drive the cross-library walker.

Reported by RyanJamesStewart on #14517 with this fixture: an
unwrapped [middle] depending on unwrapped [prelude] with
[(flags (:standard -open Prelude))], exposing
[val pick : unit -> color] (where [color] resolves through the open
to [Prelude.color]). The consumer pattern-matches the result
against bare constructors. The compile genuinely needs [prelude.cmi]
to resolve the constructors; the BFS over [ocamldep -modules]
cannot reach [prelude] (no syntactic [Prelude] token on either
side); the three existing recoveries do not catch it ([prelude] is
not wrapped, not a ppx-runtime lib, not a virtual-impl).

[Module_compilation.cross_lib_tight_set]:
- Add [~mode] (the consumer's compile mode) so we can expand a dep
  lib's stanza flags via [Ocaml_flags.get].
- Extend [read_entry_deps] to compute [read_stanza_opens] for the
  visited lib and union the result into the BFS frontier. Localised
  in the BFS rather than the initial-frontier computation so the
  reachability rule reads as: a module is reachable iff the consumer
  references it, or some reached module's ocamldep names it, or some
  reached module's owning lib stanza-opens it. Returns empty for
  [Spec.standard] (short-circuits external libs).

[Lib_info]:
- Add [stanza_flags : Dune_lang.Ocaml_flags.Spec.t] field plus
  accessor. Local libs carry their stanza's [conf.buildable.flags];
  external libs ([findlib], [dune_package]) carry [Spec.standard].

Regression test: [cross-lib-open-flag-barrier.t]. Fails on L4 and
L5 head before this patch (Unbound constructor Green under
[--sandbox=copy]); passes after.
@robinbb robinbb force-pushed the robinbb-14492-l5-soundness branch from a94a5c6 to 34a1914 Compare May 17, 2026 23:57
Restores correctness for three cases the bare BFS filter mishandles:
- Deps that implement a virtual library: dep-graph through them is
  computed elsewhere ([Dep_rules.imported_vlib_deps]); the per-module
  filter can miss cmi changes. Gate: fall through to glob whenever the
  cctx has [has_virtual_impl].
- Wrapped local libs the consumer references through the wrapper name:
  the ocamldep walk can't see the alias chain into the lib's
  [wrapped_compat] / inner modules. Reach: glob the wrapped lib's
  [Lib.closure].
- [ppx_runtime_libraries] introduced by [pps] in the consumer's
  preprocessor: their modules appear in the post-pp source which
  ocamldep can't see. Reach: glob their [Lib.closure].

[Module_compilation.lib_deps_for_module]:
- After [can_filter], read [Compilation_context.has_virtual_impl]; if
  true, fall back to glob.
- Read [Compilation_context.pps_runtime_libs] and include them in
  [direct_libs] so [Lib.closure] sees them.
- Compute [wrapped_libs_referenced] from the consumer's
  [referenced_modules] (BFS-initial frontier — pre-cross-lib-walk).
  Take the [Lib.closure] of that set union [pps_runtime_libs] to get
  [must_glob_libs]; the classification fold sends every member to the
  glob path.

[Modules]:
- [Wrapped.entry_modules]: new function. Returns the wrapper
  ([lib_interface]) plus every [wrapped_compat] shim. Mirrors what
  [(wrapped (transition ...))] libraries expose to consumers.
- [entry_modules]'s wrapped case switches to use it. Net effect: in
  transition wrapped libs, consumers can resolve any of the bare
  module names the lib exposes; this lifts a false-negative in the
  index that previously hid the consumer's reference to a
  [wrapped_compat] shim from the per-module filter.

Tests (cherry-picked from #14492):
- New soundness fixtures land here:
  [cross-lib-instrumentation-barrier.t], [cross-lib-preprocess-barrier.t],
  [cross-lib-pps-runtime-no-ocamldep-barrier.t],
  [wrapped-from-vlib-soundness.t], [wrapped-transition-soundness.t],
  [mixed-per-module-preprocess.t], [mixed-per-module-preprocess-precision.t],
  [cmx-native-tight-deps.t].
- The five pre-existing tests broken by L4
  ([auto-wrapped-child-reexport.t], [ppx-runtime-libraries.t],
  [virtual-library.t], [wrapped-closure-precision.t],
  [wrapped-reexport-via-open-flag.t]) pass again — soundness
  recovery restores their original behavior; no test file change in
  #14492's diff for them.

Changelog: [doc/changes/added/14492.md] lands now.

Signed-off-by: Robin Bate Boerop <me@robinbb.com>
robinbb added a commit that referenced this pull request May 18, 2026
Closes a soundness gap in the per-module narrowing pipeline missed
by the wrapped / ppx-runtime / virtual-impl recoveries: when a
dependency library's stanza injects [-open M] via [(flags (...))],
its source can reference [M]'s identifiers without naming [M], and
ocamldep emits no token to drive the cross-library walker.

Reported by RyanJamesStewart on #14517 with this fixture: an
unwrapped [middle] depending on unwrapped [prelude] with
[(flags (:standard -open Prelude))], exposing
[val pick : unit -> color] (where [color] resolves through the open
to [Prelude.color]). The consumer pattern-matches the result
against bare constructors. The compile genuinely needs [prelude.cmi]
to resolve the constructors; the BFS over [ocamldep -modules]
cannot reach [prelude] (no syntactic [Prelude] token on either
side); the three existing recoveries do not catch it ([prelude] is
not wrapped, not a ppx-runtime lib, not a virtual-impl).

[Module_compilation.cross_lib_tight_set]:
- Add [~mode] (the consumer's compile mode) so we can expand a dep
  lib's stanza flags via [Ocaml_flags.get].
- Extend [read_entry_deps] to compute [read_stanza_opens] for the
  visited lib and union the result into the BFS frontier. Localised
  in the BFS rather than the initial-frontier computation so the
  reachability rule reads as: a module is reachable iff the consumer
  references it, or some reached module's ocamldep names it, or some
  reached module's owning lib stanza-opens it. Returns empty for
  [Spec.standard] (short-circuits external libs).

[Lib_info]:
- Add [stanza_flags : Dune_lang.Ocaml_flags.Spec.t] field plus
  accessor. Local libs carry their stanza's [conf.buildable.flags];
  external libs ([findlib], [dune_package]) carry [Spec.standard].

Regression test: [cross-lib-open-flag-barrier.t]. Fails on L4 and
L5 head before this patch (Unbound constructor Green under
[--sandbox=copy]); passes after.
@robinbb robinbb force-pushed the robinbb-14492-l5-soundness branch from 34a1914 to a75f81a Compare May 18, 2026 00:07
Closes a soundness gap in the per-module narrowing pipeline missed
by the wrapped / ppx-runtime / virtual-impl recoveries: when a
dependency library's stanza injects [-open M] via [(flags (...))],
its source can reference [M]'s identifiers without naming [M], and
ocamldep emits no token to drive the cross-library walker.

Reported by RyanJamesStewart on #14517 with this fixture: an
unwrapped [middle] depending on unwrapped [prelude] with
[(flags (:standard -open Prelude))], exposing
[val pick : unit -> color] (where [color] resolves through the open
to [Prelude.color]). The consumer pattern-matches the result
against bare constructors. The compile genuinely needs [prelude.cmi]
to resolve the constructors; the BFS over [ocamldep -modules]
cannot reach [prelude] (no syntactic [Prelude] token on either
side); the three existing recoveries do not catch it ([prelude] is
not wrapped, not a ppx-runtime lib, not a virtual-impl).

[Module_compilation.cross_lib_tight_set]:
- Add [~mode] (the consumer's compile mode) so we can expand a dep
  lib's stanza flags via [Ocaml_flags.get].
- Extend [read_entry_deps] to compute [read_stanza_opens] for the
  visited lib and union the result into the BFS frontier. Localised
  in the BFS rather than the initial-frontier computation so the
  reachability rule reads as: a module is reachable iff the consumer
  references it, or some reached module's ocamldep names it, or some
  reached module's owning lib stanza-opens it. Returns empty for
  [Spec.standard] (short-circuits external libs).

[Lib_info]:
- Add [stanza_flags : Dune_lang.Ocaml_flags.Spec.t] field plus
  accessor. Local libs carry their stanza's [conf.buildable.flags];
  external libs ([findlib], [dune_package]) carry [Spec.standard].

Regression test: [cross-lib-open-flag-barrier.t]. Fails on L4 and
L5 head before this patch (Unbound constructor Green under
[--sandbox=copy]); passes after.

Signed-off-by: Robin Bate Boerop <me@robinbb.com>
@robinbb robinbb force-pushed the robinbb-14492-l5-soundness branch from a75f81a to 8655699 Compare May 18, 2026 00:12
@RyanJamesStewart
Copy link
Copy Markdown

On the test: the fixture I offered is the one you have added as cross-lib-open-flag-barrier.t. Same prelude/middle/consumer shape, same (wrapped false) and stanza -open, same --sandbox=copy oracle, so it is covered and a separate attachment would be redundant. The one case it does not pin down is the #14518 layer, where the same construction becomes a hard default-build regression once filtered_include_flags drops the wide -I. If a guard there is useful I am happy to add one.

On the rest: I am not an LLM running wild. I post under my full name and stand behind what I post under my own judgment. My criteria for participating in a PR are deliberately narrow: I sweep open issues and recently merged PRs, look for a load-bearing case the existing patches do not cover, reproduce it myself under the same oracle the in-tree tests use, and only post when the finding is clearly outside what is already addressed. I set aside far more than I send. I have no idea who stuboo is. This is my first contribution here; it will not be the last.

@stuboo
Copy link
Copy Markdown

stuboo commented May 18, 2026

I have no connection to this account or this repository.

@robinbb
Copy link
Copy Markdown
Collaborator Author

robinbb commented May 18, 2026

I sweep open issues and recently merged PRs, look for a load-bearing case the existing patches do not cover, reproduce it myself under the same oracle the in-tree tests use, and only post when the finding is clearly outside what is already addressed. I set aside far more than I send.

That is a lot of work, @RyanJamesStewart! What inspires you to go to such lengths?

(In any case, I appreciate your having found a weakness in this PR.)

@robinbb
Copy link
Copy Markdown
Collaborator Author

robinbb commented May 18, 2026

I have no idea who stuboo is.

@stuboo Is the user who committed the following to your (@RyanJamesStewart's) time tracker repo: RyanJamesStewart/time-tracker@77cfb81

@robinbb
Copy link
Copy Markdown
Collaborator Author

robinbb commented May 18, 2026

I have no connection to this account or this repository.

@stuboo Perhaps a bot has falsely claimed to have made this commit by you: RyanJamesStewart/time-tracker@77cfb81

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants