SVF icon indicating copy to clipboard operation
SVF copied to clipboard

Questions about PtType

Open Minnnnnnnnnt opened this issue 2 years ago • 3 comments

Hi I have some questions about Options::PtType. When detecting a library of openssl(libcrypto) by using saber of SVF2.5, I chose different PtTypes. The size of bc file is 10M after mem2reg. PointsTo::Type::SBV takes about 20 minutes to complete the analysis, but PointsTo::Type::CBV and PointsTo::Type::CBV both take more than 4 hours. I would like to know what is the reason for this and what situation does these three options apply to? Thank you very much.

Minnnnnnnnnt avatar Nov 10 '22 03:11 Minnnnnnnnnt

The details of the three points-to data structures are here: https://yuleisui.github.io/publications/oopsla21.pdf

@mbarbar could you give some hints why CBV is so slow in his case?

yuleisui avatar Nov 10 '22 05:11 yuleisui

Barring the possibility of a bug, I suspect a terrible object-to-identifier mapping.

This can happen by "chance" (we have no heuristic for mapping; open for research I think) or by some property of the program, like a specific object being in every single points-to set.

If this is FSPTA, cluster-fs can fix this for the flow-sensitive part. It may not be enough in some cases though, e.g., imagine a program with 20000 objects and a particular object is in every points-to set, you'll end up with points-to sets like {10000, 20000, ...}, {10000, 18000, ...}, {10000, 500, ...}, etc. which are bad for a non-sparse implementation.

I think cluster-fs will print stats of how many machine words are required to represent all points-to sets using BVs, CBVs, and SBVs.

mbarbar avatar Nov 10 '22 13:11 mbarbar

@Minnnnnnnnnt can you try the upstream of SVF (the current commit)? I remember that there might be a fix for this. Otherwise, insights from @mbarbar's reply might be helpful.

yuleisui avatar Nov 10 '22 13:11 yuleisui