Conversation
|
Interesting changes, but why the changes to the IntervalAnalysis? It was a deliberate choice to make it |
|
You are right, this had nothing to do there. |
|
Do you intend to do more changes in this PR? It is marked as DRAFT after all :) |
|
I needed to add some unit tests before removing the |
| /// This method must not have false negatives, but is allowed to have false positives. | ||
| boolean overlaps(Modifier left, Modifier right); | ||
|
|
||
| /// Checks if for all integers `x` and `y`, `x[smaller]y` must imply `x[larger]y`. | ||
| /// This method must not have false positives, but is allowed to have false negatives. | ||
| boolean includes(Modifier larger, Modifier smaller); |
There was a problem hiding this comment.
Maybe you should include the approximation direction in the name of the methods:
mayOverlap(...) and mustInclude(...).
| /// Intersects `[modifier]` with `{ (x,y) | x <= y < x + objectSize }`. | ||
| /// If this intersection is empty, the associated access must be out-of-bounds. | ||
| /// <p> | ||
| /// This is an unsound strengthening that assumes no out-of-bounds accesses, given a memory object of known size. | ||
| Modifier postProcess(Modifier modifier, int objectSize); |
There was a problem hiding this comment.
The description forces postProcess to have a very concrete semantics despite its very generic name. I would call it bound or restrict or something like that.
|
What is the correlation between the old alias analyses and the inclusion-based one with weaker modifier traits? Also, do you think there are other reasonable instantiations of the |
2 participants
Adds more control over the used lattice in
InclusionBasedPointerAnalysis. More implementations can be added later.--program.analysis.alias=EXPERIMENTAL_FIELD_INSENSITIVEuses the singleton latticeModifierTrait.VoidTrait. It lets the analysis be truely field-insensitive. It is not generally, but mainly, less precise thanFIELD_INSENSITIVEimplemented inAndersenAliasAnalysis.--program.analysis.alias=EXPERIMENTAL_FIELD_SENSITIVEuses the latticeModifierTrait.Offsetsand comparable withFIELD_INSENSITIVEandFIELD_SENSITIVE.--program.analysis.alias=EXPERIMENTAL_LINEAR_1DusesModifierTrait.SdLinear.--program.analysis.alias=FULLremains usingModifierTrait.MdLinear.