Do not report elements of code defined in module types - #92
Open
fantazio wants to merge 10 commits into
Open
Conversation
The new module documents the function's parameters. This is preliminary work to implement 2 collectors: - one for cmti files (relying on `Typedtree.signature`) - one for cmt files (relying on a mix of cmi and cmt info)
This is a naive translation of the existing `collect_export`, that works on `Typedtree.signature` instead of `Types.sig_item`. The intent is to use this new function on cmti files' signatures instead of the other on their cmi infos. A new function `Utils.typedtree_signature_of_modtype` is added, and is also a naive translation of `Utils.signature_of_modtype` to work on `Typedtree` types instead of `Types`'s.
In `State.File_infos.t`, update `smi_sign` to `cm_sign` and its type to the new `signature option`. It now stores either the cmti signature when available (found `cmt_infos.cmt_annots`), or the `cmi_infos.cmi_sign` as fallaback (old behavior). When collecting exports, use the collector corresponding to the cm_sign, using `collect_export_from_typedtree` for cmti signature. This fixes the modtype limitation when a .mli is provided for all constructs but optional arguments.
Unlike manipulating Types.signature, manipulating Typedtree.signature does not require the identification of content within module types. This is because module types attached to modules are more precise in the Typedtree and, in particular, disintiguishes explicit signatures from module types with constraints. In Types, those module types with constraints are represented uniformly with, thus undistinguishable from, explicit signatures.
fantazio
marked this pull request as ready for review
August 5, 2026 08:36
fantazio
marked this pull request as draft
August 5, 2026 09:22
Collaborator
Author
|
Noticed a few undesired changes in results on opam 2.5.1. I suspect this is due to an Update: the construct is now documented in the limitations |
fantazio
marked this pull request as ready for review
August 5, 2026 12:12
This fixes the false positives related to the `modtype` limitation. The process is simple : - When processing signatures (either `Types` or `Typedtree`), mark content coming from Types' module types as such. This is necessary for optional arguments. In the case of a Typedtree.signature, elements to be marked are detected via a mismatch between the Typedtree and the Types module type signatures (the first is implicit while the second is explicit). - When processing a .cmt file without corresponding .cmti file, if a module type signature mismatches between the Typedtree and Types representation (same as above), then its elements are unexported, and the marked as belonging to a module type. Thus, this is a correction a posteriori.
The modtype limitation was used as an exemple for false positives that did not follow the semantics on module types. Now that these false positives are fixed, the exemples are used to describe the module type semantics (still considered a limitation) as a whole.
This value only stores "implicit re-declarations" which appear as regular new declarations in `Types.signature`. In addition, this stock is only useful to filter out opt args related to such implicit re-declarations so it is only filled out if opt args are enabled. Finally, because it is only related to opt args, it is not used anymore to avoid "wronfully" exporting values that were implicit re-declarations. These values are identified and corrected by `DeadSign.correct_export`.
The new limitation is a corollary of the one on module types. Corresponding examples (derived from `modtype`'s) are added in `examples/docs/limitations/modtype_of`.
`correct_export` is first defined without guard in order to be used during `collect_export_from_typedtree` traversal. Then redefined with guard to avoid correcting Typedtree signatures during the structure analysis. This function is used instead of `collect_export`. This avoids the risk of not storing the desired locs in `implicit_decs`. As a result, `implicit_decs` does not need to be a "stock" anymore and is only used to store locations (the table's values are units).
3 functions `export_value, `export_type`, and `export_class` are defined to share logic between `collect_export` and `collect_export_from_typedtree`. `collect_export` is flattened. The `should_export` logic is simplified to ignore the substitution case because it is now handled by `correct_export`. As a result, `context` does not include `In_modtyp` anymore, and `DeadCommon.implicit_decs` does not need to resemble a stock (now use `unit` as value).
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
1 participant
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.
Fixes #64
Partial solution for #55 in case
include module type ofis used (e.g. in the presence of a .mli)##Context
Since #52, the analyzer must not report values declared in module types.
However, in the
cmi_signused to gather all exports, the use of module types would be replaced inline by their signature in some cases. This was leading to the analyzer to believe the elements declared were "new" declarations when they were actually implicit re-declarations. As a result, theexamples/docs/limitations/modtypeexamples would produce a lot of false positives.Solution
With .mli
In order to reduce the risk of gathering "wrongful" exports, when a .cmti file is available, then its signature is used instead of the one found in
cmi_sign. Indeed, .cmti holds aTypedtree.signaturewhich is more precise thanTypes.signature. In particular, theTypedtree'ssignature_item_descandmodule_type_descare able to represent more precisely the actual code found in .mli files than theirTypescounterparts. As a result, we are able to avoid implicits re-exports due to module type inclusions and constraints.Without .mli
If there is no .mli file then there is no .cmti available. Thus we are forced to fallback into the imprecise
cmi_sign.Because we cannot distinguish if an element is actually a new declaration or implicitly re-declared, we need to use extra information. This information is found in the .cmt, which contains a
Typedtree.structure. There is no .mli and the .cmt corresponds to the .ml, so it contains the same declarations as those found in thecmi_sign, with more precision.Thus, we can rely on it to correct a posteriori the wrongful exports, during the collection of uses.
Note
The correction is done during the this phase to avoid a second traversal of the structure, but it could be worth trying another approach with a traversal before collecting exports, that would temporarily collect the locations of future "wrongful" exportations. Those locations would then be used during the collection of exports to disambiguate actual new declarations from implicit re-declarations.
Alternatively, we could probably avoid collecting exports from the
cmi_signin general and only rely on theTypedtree.structurein this phase. This is left for a future exploration.Optional arguments
Optional arguments are handled a little bit differently from other constructs. Rather than collecting their declarations, and at report time looking for the uses of declared elements, their declarations are entirely ignored and a pre-report analysis is applied on the gathered uses.
During this analysis, all the uses of optional arguments connected to values outside analyzed files are discarded. This filter now also discards the uses connected to elements that are identified as "wrongful" exports.
The identification of "wrongful" exports in the previous section is done by comparing a
Typedtree.module_typewith its correspondingTypes.signature. If the former does not contain an explicit signature while the latter does, then the content of the latter is actually implicitly re-declared.When a "wrongful" export is identified, its location is stored in
DeadCommon.implicit_decs, to later be matched against during the pre-report analysis of optional arguments.Tests
All the false positives of
examples/docs/limitations/modtypeare fixed.The false positive in
examples/using_make/advanced/func.mliis fixed.Benchmarks on Frama-C and Opam show that this new version does not impact performances negatively. The changes in results on those projects are coherent.
Docs
The documentation is updated to reflect the fix of the "Module type with and inclusion" limitation. The
modtypeexamples are now related to theModule typelimitation.A new limitation is documented : "Module type of" (with corresponding
modtype_ofexamples). This is a consequence of the modtype limitation: the module type semantics is applied to modules whose module type is recovered viamodule type of.