Draft
Conversation
fantazio
force-pushed
the
5.3
branch
4 times, most recently
from
7df2f25 to
87f8070
Compare
Open
Naively fix compilation issues. In particular, the use of `cmt_declaration_dependecies` instead of `cmt_value_dependencies` is a simple translation from the latter to the former and is not exactly equivalent because `uid`s may not be found in the `cmt_uid_to_decl` table. This is certainly the root cause of the introduced FP and FN
This will be used in by the state component
If a compilation has a`.mli`, then it has a `.cmti` which is more complete than the `.cmi`. This extra information is useful to fill the state's `file_infos`. However, a `.ml` wihtout a corresponding `.mli` does not have a corresponding `.cmti`. Hence, introducing even more mistakes for now. Now that interfaces are read from `.cmti` instead of `.cmi`, the order in which the files are read is reversed to ensure interfaces (`.cmti`) are read before their corresponding implementation (`.cmt`)
If a `.ml` has a `.mli` then its interface is available as `cmi_infos` in the `.cmti`. Otherwise, there is no `.cmti` and it is available in the`.cmt`. All FN and FP introduced by the previous commit are fixed.
Using information available in the `.cmt`, store locations of uids coming from `include`s in a new state field : `state.signature.uid_to_loc`. Using `.cmt` and `.cmti`, store locations of values' (and patterns in value bindings) uids at the same location for easier lookup. This is done as soon as the files are loaded, before the analysis. The new table tries to be semantically equivalent to the usage of `cmt_value_dependencies` instead of `cmt_declaration_dependencies` before OCaml 5.3. This fixes the FP and FN introduced when moving to OCaml 5.3.
Rather than adding a `signature` field to the state to hold a `uid_to_loc` table to then use in `DeadCode.load_file` to convert uids into locations, to then convert `cmt_declaration_dependencies` into a list of pairs of locations, directly construct that list and store along with the `file_infos`. This move is more consistent with the nature, usage and provenance of the information : it is created using info in `cmt_infos` and `cmti_infos` to replace the `cmt_value_dependencies` field that existed prior to OCaml 5.3, and should only live as long the corresponding `cmt_infos` live.
Only keep useful information from the cm*_infos rather than the whole structure. This makes clearer what is actually used from those and reduces the error surface.
This fixes the remaining FP/FN
This significantly improves the performances (compared to the previous commit) measured on Frama-C : -84% time, same memory. This is still however noticeably less performant than the OCaml 5.2 -compatible version : +246% time, +39% memory.
This replaces the previous local cache in location dependencies computation. This improves the performance measured on Frama-C : -56% time, +10% memory. Compared to the OCaml 5.2 -compatible version :+51% time, +52% memory.
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.
Other than updating the OCaml version to 5.3 and fixing the compilation mistakes, this PR includes 2 important changes :
.cmtifiles are used instead of.cmifiles. Thecmi_infosare now read from either the.cmtiif it exists or the.cmtotherwise. This simplifies a lot the initialization ofState.File_infos.t. This type has evolved to only expose the information used from the variouscm*_infosread. Using.cmtiprovides information used in the next point.the
cmt_infos.cmt_value_dependenciesis recreated (as a list of pairs of locations, to only expose what is actually used). Indeed, it is replaced bycmt_declaration_dependencieswhich exposes a lot more dependencies than only values, and some uids in that list are missing in thecmt_infos.cmt_uid_to_decl. To recreate the value dependencies, the latter field of both the.cmtand.cmtifiles are used, and missing uids' locations are retrieved by opening their corresponding.cmti/.cmt(if provided).This is a first step towards #39