Track type equivalences - #97
Draft
fantazio wants to merge 7 commits into
Draft
Conversation
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.
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 (as long as we analyze a 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.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, the performance is very negatively impacted (more than 70% slower on some benchmarks). Some cleanup and debugging is still expected.
Docs
Not up to date