New Pointer Analysis

[xeren]

This PR started as a rework for FieldSensitiveAlias. It now features a third implementation InclusionBasedPointerAnalysis.

• It manages pointer modifiers of the type (int static offset‘,List<Integer> dynamic offsets). This should make its precision robust against optimizations of the following form. (FieldSensitiveAndersen uses (int,int) and thus looses precision there)

      w = x + y
      address = w + z
      ↓
      address = x + y + z

• It stores inclusions, loads, stores and pointer sets in a compact format, such that its memory usage scales better with large arrays.
• Instead of a node for each register or allocated byte, this version manages a node for each complex expression, register writer and phi node. This means this version not only field sensitive, but also flow sensitive (with the exception of assumptions). It now requires a prior Dependency Analysis.
• It implements a unification rule: If a variable has only one include edge, it gets merged into that other variable. This enhances the mustAlias queries.
• It implements an acceleration rule: If a variable directly or indirectly includes itself with a static offset of c != 0, then c is promoted to a dynamic offset. Such cycles propagate at most once in total, instead of at most once per allocated byte. This should also allow the algorithm to terminate even if the program has arrays of unknown/nondeterministic size (if such a feature is ever added in the future).

[hernanponcedeleon]

Does the first bullet point mean the new analysis is always more precise than the old ones?
Do we have any concrete example where we get noticeable better performance?

[ThomasHaas]

@xeren showed me improved results on EBR with substantial speed up.

Btw. I think this PR does not set the new analysis as default, so the CI still runs with the old one.
I think you should put the new analysis as default to catch any problems.

[hernanponcedeleon]

@ThomasHaas would it make sense to add EBR to our CI? IIRC it is supposed to be buggy wrt IMM but correct under hardware models

[ThomasHaas]

@ThomasHaas would it make sense to add EBR to our CI? IIRC it is supposed to be buggy wrt IMM but correct under hardware models

I don't know how much time it takes with Yices2. With Z3, running EBR under multiple models is expensive.

[ThomasHaas]

I have just tested this analysis on RCU tree and with B=1 it terminates in 2 seconds and with B=2 in 20 seconds. The old analysis took multiple hours IIRC.
However, it computes quite a few empty pointer sets. I also cannot tell how precise it is cause the fast termination may be due to imprecision caused by RCU having the whole memory stored in arrays.

[hernanponcedeleon]

It seems that when I rebase the branch, I overwrote the default alias type. It should be fixed by now.

BTW, as Thomas said, the new alias analysis shows to be better than the old one in the benchmarks added in #621, here are the statistics

[20.02.2024] 11:56:47 [INFO] AliasAnalysis.fromConfig - Selected alias analysis: FULL
======== RelationAnalysis summary ======== 
        #Relations: 104
        #Axioms: 4
        #may-edges removed (extended): 86907
        #must-edges added (extended): 156
        total #must|may|exclusive edges: 1689106|2239829|0
        #must|may rf edges: 4|18859
        #must|may co edges: 474|486
===========================================

[20.02.2024] 11:58:00 [INFO] AliasAnalysis.fromConfig - Selected alias analysis: FIELD_SENSITIVE
======== RelationAnalysis summary ======== 
        #Relations: 104
        #Axioms: 4
        #may-edges removed (extended): 94306
        #must-edges added (extended): 156
        total #must|may|exclusive edges: 1686959|2287321|0
        #must|may rf edges: 4|21522
        #must|may co edges: 474|486
===========================================

[ThomasHaas]

It seems that when I rebase the branch, I overwrote the default alias type. It should be fixed by now.

I think the default you think about was not changed by @xeren. We have two defaults and the one you changed was for the UI only I think.

[hernanponcedeleon]

It seems you are right (even if I'm pretty sure I saw field_sensitive in the log when I called dartagnan from the console with no alias options).

We should be able to use Alias.getDefault() similarly to what we do with method, target, ... right?

[ThomasHaas]

We should be able to use Alias.getDefault() similarly to what we do with method, target, ... right?

I think so. Just change the initializer in AliasAnalysis.Config to call Alias.getDefault().

[hernanponcedeleon]

I am testing this branch in some new benchmarks and I get a bunch of warnings like this

[04.03.2024] 00:14:56 [WARN] InclusionBasedPointerAnalysis.postProcess - empty pointer set for bv64 117:r24 = load(*bv64 117:r23)

How should I interpret this @xeren ? It sounds like this load cannot read from anywhere

[ThomasHaas]

Yes, this means the are no possible targets to read from. It could be a bug in the analysis but also a correct result.
For example, this warning also appeared in tree.c but it turned out that the code does indeed access a NULL pointer.

[hernanponcedeleon]

Yes, this means the are no possible targets to read from. It could be a bug in the analysis but also a correct result. For example, this warning also appeared in tree.c but it turned out that the code does indeed access a NULL pointer.

But then this is a bug in the code being analyzed ...

[ThomasHaas]

Yes, this means the are no possible targets to read from. It could be a bug in the analysis but also a correct result. For example, this warning also appeared in tree.c but it turned out that the code does indeed access a NULL pointer.

But then this is a bug in the code being analyzed ...

Yes, it might be if that memory access is reachable. @xeren Can you add source location information into the warning so we can more easily check what is wrong?

[hernanponcedeleon]

@xeren any progress a out this PR? I would like to get this merged soon

[ThomasHaas]

I feel like your newest change has just shifted the variable vs. edge problem, no?
Previously, you used edges that sometimes represented variables. Now you use variables that sometimes represent edges.

[xeren]

I fixed a bug in the analysis, where the communication rule was not correctly implemented.

The rule states that from $(X+o_1\xleftarrow{\text{stores}}W+o_2)$, $(W\supseteq A+o_3)$, $(A+o_4\subseteq R)$, $(R+o_5\xrightarrow{\text{loads}}Y)$ and $((o_2+o_3)\cap(o_4+o_5)\ne\emptyset)$, you can derive $X+o_1\subseteq Y$.

Either $o_2$ or $o_5$ was skipped in the intersection test (depending on where the recently-learned inclusion edge is), resulting in both false positives and false negatives.

I feel like your newest change has just shifted the variable vs. edge problem, no?
Previously, you used edges that sometimes represented variables. Now you use variables that sometimes represent edges.

Maybe you were referring to inclusion edges being typed as DerivedVariable. I have now separated both use cases into separate classes.

[ThomasHaas]

I fixed a bug in the analysis, where the communication rule was not correctly implemented.

The rule states that from (X+o1←storesW+o2), (W⊇A+o3), (A+o4⊆R), (R+o5→loadsY) and ((o2+o3)∩(o4+o5)≠∅), you can derive X+o1⊆Y.

Either o2 or o5 was skipped in the intersection test (depending on where the recently-learned inclusion edge is), resulting in both false positives and false negatives.

Do you know of an instance of wrong behaviour? For example, does this affect qspinlock or ck_epoch or RCU?

I feel like your newest change has just shifted the variable vs. edge problem, no?
Previously, you used edges that sometimes represented variables. Now you use variables that sometimes represent edges.

Maybe you were referring to inclusion edges being typed as DerivedVariable. I have now separated both use cases into separate classes.

Yes, that is what I was referring to.

[ThomasHaas]

Overall, I like this newer version a lot more. I will do a proper review the next week.

[ThomasHaas]

EDIT: I was wrong. The code uses join for sequential composition and addInto for parallel composition.
The latter does not merge edges which contradicts the class description/comment, so the description should get updated.

I think you are conflating parallel joining and sequential joining (composition) in your algorithm. These are two different things with different results and it is just accidental that your algo remains correct because you always join parallel edges where one of them is composed.

For example, parallel joining 2x + 2 and 4x + 2 should result in 2x + 2, i.e., the gcd is used for the dynamic offset and the offsets are not added.
Sequential joining on the other hand would give 2x + 4y + 4 (or 2x + 4 if you combine multiple offsets) because the modifiers just get added. In the case where you would know that both dynamic offsets are the same variable, you would even get 6x + 4

[ThomasHaas]

Did you intentionally revert your recent changes? If so, you also reverted the changes to the handling of unary expressions, so they are still wrong.

[hernanponcedeleon]

I tested this on the libvsync benchmarks and all results look good. Unless there are further comments, I will merge.

[ThomasHaas]

LGTM