Pointer Analysis Types

[mayanez]

Hi,

Firstly, Awesome project! Reading through the source code I had a question about this enum:

SVF/include/MemoryModel/PointerAnalysis.h

Line 58 in 3038078

enum PTATY {

A number of analysis I'm interested are listed. However, it seems like these are yet to be implemented? Or is there source code available somewhere else that hasn't been merged?

[yuleisui]

Hi Miguel,

The demand-driven analysis (SUPA) is yet to be merged to SVF. We hope we can finish merging in the next few months.

For all other analyses, either they are in the repo, or not implemented.

Thanks,
Yulei

[mayanez]

Thanks for your quick response!

While it is being merged, is the version found here https://github.com/yuleisui/yuleisui.github.io/blob/master/supa/supa.zip working?

[yuleisui]

Yes, it works on an older version of SVF (i.e., LLVM-4.0.0).

[mayanez]

Hi Yulei,

I've been experimenting with SVF and had a few questions.

I'm trying to compare the SVFG graphs between Context-sensitive DDA (ie. ./build/bin/dvf -cxt -dump-svfg cs0.ll) & the flow-sensitive WPA (ie. ./build/bin/wpa -ander -dump-svfg cs0.ll). The MUSTALIAS & NOALIAS asserts are correct as expected. However, I am not seeing any difference in the graph's with the exception of the yellow FormalIn nodes.

I would have expected these two graphs to be different. Am I missing something?

[yuleisui]

Hi Miguel,

The two analyses should produce the same SVFG. DDA (SUPA) decides whether a value-flow (an SVFG edge) is infeasible or not via on-demand graph traversal.

Note that DDA (SUPA) only refines the value-flows rather than deleting SVFG's edges to compute precise points-to results. This is a design choice to make SVFG consistent, but the analysis to will be gradually refined.

[mayanez]

Thank you for the clarification. In the case of DDA (SUPA) is it possible to output the SVFG it computes at the end of its refinement stage? I want to be able to query the graph to diff against a less sensitive points-to analysis.

[yuleisui]

Miguel,

Good question. Unfortunately, for a query-based context-sensitive demand-driven analysis, this does not make too much sense.

For example, if we want to remove a value-flow permanently from SVFG, this value-flow has to be spurious under every calling context. Otherwise, simply removing it will cause unsound results.
However, validating a particular value-flow under all context is almost impossible for a demand-driven analysis since most of the time we just issue some but not exhaustively all queries for all pointers in a program.

Ideally, every value-flow should have a label recording, under which contexts, the value-flow is legitimate or spurious. Again, this is impractical as mentioned as we can't enumerate all possible queries of every pointer.

You may wish to just query a pointer's value to get the precise points-to results for answering a particular query. We believe our current way is a nice solution without constantly updating or invalidating SVFG.