Track type equivalences - #97
Open
fantazio wants to merge 10 commits into
Open
Conversation
fantazio
force-pushed
the
eq_types
branch
2 times, most recently
from
August 21, 2026 10:11
0b8f21b to
3d17f4d
Compare
In addition to documentation, examples are written and expected results are updated accordingly. This adds a lot of false positives in the tests, and as many false negatives (misplacements) for the threshold test scenarios
The tracking is very naive (using an assoc list), and equivalent classes are only resolved at the end in the new `DeadType.prepare_report` function. The role of this new function is to merge all the references of an equivalent class and propagate the result back to its members. As a result, the FP/FN related to type equations are now resolved. The code still needs to be cleaned up but gives the direction to fix the other FP/FN in the `equal_types` limitation.
When an include is encountered, all the type components defined in the included module and in the ucrrent compilation unit are considered equivalent. Although the equivalence is not necessarily true (e.g. the current implementation could redefine the same type explicitly and without equation right after the include), this is a good effort towards actionable results in the presence of type equalities. This fixes include-related FP and FN in the `equal_types` limitation.
This requires more changes than anticipated. The module types available in the .cmt where the aliasing occurs ar Mty_alias, and the surrounding Env.t do not help retrieving a more detailed information. Thus, we recreate in `DeadSign.exported_modules` what we hoped to find in environments : the association from path to module type. With this information, we are able to process a module alias's types and fill out our equivalences list. This fixes the remaining FP and FN (related to module aliases) of limitation `equal_types`.
This specific example tests the handling of type equivalences within a single compilation unit, with only one of the types exported. All the internal types are equivalent, by means of eqcplicit equations, hidden equations, module alias and include.
This relies on the use of the available env to retrieve the module types of local aliases. Internal type equivalences are stored with all the other equivalences and resolved at the end. This fixes the FP/FN of eq_types' all_internal examples.
fantazio
force-pushed
the
eq_types
branch
2 times, most recently
from
August 26, 2026 17:23
6cfb262 to
5ea60bd
Compare
- Remove `DeadMod.defined`, it was filled up but never used; - Paths are now represented using `string list` instead of `Ident.t list`. This results in less conversions (some dummy Ident.t were created only to be used as strings later) - Wrap some `DeadType` functions to avoid storing and processing useless information when fields and ctor reports are disabled. Also protect `DeadSign.collect_eq_from_module_alias` and `DeadSign.collect_from_include` from traversing trees and possibly loading an env when related sections are disabled.
The load_path setup is very expensive time-wise. Instead of systematically doing it in case we need to load envs from summaries, we prepare the setup when reading a new file, but only actually apply it the first time we need to load an env. As a result, the performance impact is of <30% time increase on Frama-C instead of >75%.
The limitation is now fixed. The associated code constrcuts have their own documentation page. The tests have been moved accordingly, and the expected results updated as well.
fantazio
marked this pull request as ready for review
August 27, 2026 20:04
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.
Fix #79, #80, #81, #82
Context
The aforementioned issues are all related to the same pitfall : if a module re-exports a type as its own (no explicit link with the original one), then the analyzer believes that it is indeed a new type definition.
Consequently, if a constructor/field is used via one type but not another equivalent, then it is reported as unused for the latter.
Solution
We introduce a new associative list
DeadType.equivalencesto keep track of explicit equivalences (type t2 = t1 = ...) found in implementations, and implicit ones (due to includes and module aliases).The list is later used in post-analysis and pre-report (in
DeadType.prepare_report), to resolve all the equivalences and propagate uses of each member of an equivalence class to all the other members. As a result, ifA.t = B.tbut both are exported as new definitions, the reported components of both types are the same.This sort of breaks the "independence" of the reports (i.e. each report line can be processed independently) because we report the same component multiple times (at different locations). A future improvement could be to only report the components of the original type. I.e. if
t2 = t1andt3 = t2, only report the components oft1.In addition to this associative list, we also remember temporarily (per compilation unit) the types of exported module types (in
DeadSign.exported_modules, reset viaDeadSign.eof). This is necessary to associate exported type components with a module alias because the module types on module aliases are reduced toMty_aliaswithout further info than the alias.We fallback on relying on the available
Env.tto find such module types if they are not found inexported_modules.During
DeadSIgn.collect_from_include, we also rely on the availableEnv.tto retrieve the more explicit module type of anMty_alias.Tests
Tests for the corresponding issues have been introduced and the results show that they are now working as expected.
The changes in results on Opam and Frama-C are coherent.
However, there is an non-negligeable impact on performance (almost 30% slower on
-a -T allon Frama-C and almost 20% on Opam), mostly related to setting up the load paths forEnv.tmanipulations. This impact could be countered by the use of a proper scheduler, ensuring a compilation unit is analyzed after its dependencies, so all the relevant content could be stored and available without relying on theEnv.t.Docs
The documentation is updated to reflect the newly handled construct.