search

SVF-tools / SVF

Static Value-Flow Analysis Framework for Source Code
http://svf-tools.github.io/SVF/
Other
1.35k stars 427 forks source link

Pointer Analysis Types #43

Open mayanez opened 6 years ago

mayanez commented 6 years ago

Hi,

Firstly, Awesome project! Reading through the source code I had a question about this enum: https://github.com/SVF-tools/SVF/blob/3038078e90eb037ea43aa28ff3a28c05d631be5d/include/MemoryModel/PointerAnalysis.h#L58

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 commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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

mayanez commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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 commented 6 years ago

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.