On new CFL-r solver integration

[gsvgit]

We are working on integration of the solver proposed by Ilia Muravev in "Universal High-Performance CFL-Reachability via Matrix Multiplication" (SOAP 2025). Are there any design principles we should follow?

Particularly

• It looks like we should add yet another solver to CFLSplver.cpp that implements CFLSolver. Isn't it?
• How to use our solver for analysis? What specific analysis would be most interesting to evaluate the new solver?
• How should we test new solver? What kind of tests should be added?
• Is there benchmarking infrastructure to compare different solvers?

Thanks!

[yuleisui]

Thanks for the contribution. Yes, it would be good to add another solver.

CFLAlias is a subclass of the pointer analysis BVDataPTAImpl, hence any clients like SVFG, memory error detection, and abstract execution could use your CFL points-to results.

The benchmarks can be found at SVF-tools/Test-Suite here. You could also re-use all andersen's analysis benchmarks too, or your own handwritten tests.

[Aleksey2509]

Hello!
I will be working on integrating the new solver. I have a couple of follow-up questions:

1. The new solver is implemented in https://github.com/GraphBLAS/LAGraph. How should the library itself be integrated into SVF build process? I see two main ways:

   • Add it as a prebuilt package (the same way LLVM and Z3 dependancies are handled)
   • Add it as a dependancy via CMake FetchContent in CMakeLists.txt

   Which one do you find better? Or there is another more preferable way?

2. As far as I understand, integrating a new solver into CFLAlias means initializing the "solver" field of it with a new solver, which inherits from CFLSolver class. Is that it, or something more should be done to integrate a new CFL solver?

[yuleisui]

1. It is not recommended to include additional packages or dependencies if they do not have an official release, as this would make the SVF build more complicated and fragile. If you could implement the solver directly under SVF's CFL, it would be better.

2. Would be good to follow the CFLSolver implementation style (e.g. by creating a new MMCFLSolver, not necessarily inherited from the current CFLSolver as you wish), and to introduce a new subclass of CFLAlias (e.g. MMCFLAlias) for any customised points-to or alias APIs intended for external application use.

[Aleksey2509]

1. It is not recommended to include additional packages or dependencies if they do not have an official release, as this would make the SVF build more complicated and fragile. If you could implement the solver directly under SVF's CFL, it would be better.

The algorithm to be integrated relies heavily on the LAGraph and SuiteSparse:GraphBLAS libraries, which are large linear-algebra codebases. Trying to copy the necessary functionality from those libraries will be a big codebase by itself, so it will not be much different from adding the projects via CMake FetchContent from the amount of new code point of view. Those libraries do have releases and a stable branch, so those can be used for creating prebuilt-binaries or pulling them via FetchContent

2. Would be good to follow the CFLSolver implementation style (e.g. by creating a new MMCFLSolver, not necessarily inherited from the current CFLSolver as you wish), and to introduce a new subclass of CFLAlias (e.g. MMCFLAlias) for any customised points-to or alias APIs intended for external application use.

Thanks for the guidance!

[yuleisui]

1. It is not recommended to include additional packages or dependencies if they do not have an official release, as this would make the SVF build more complicated and fragile. If you could implement the solver directly under SVF's CFL, it would be better.

The algorithm to be integrated relies heavily on the LAGraph and SuiteSparse:GraphBLAS libraries, which are large linear-algebra codebases. Trying to copy the necessary functionality from those libraries will be a big codebase by itself, so it will not be much different from adding the projects via CMake FetchContent from the amount of new code point of view. Those libraries do have releases and a stable branch, so those can be used for creating prebuilt-binaries or pulling them via FetchContent

2. Would be good to follow the CFLSolver implementation style (e.g. by creating a new MMCFLSolver, not necessarily inherited from the current CFLSolver as you wish), and to introduce a new subclass of CFLAlias (e.g. MMCFLAlias) for any customised points-to or alias APIs intended for external application use.

Thanks for the guidance!

If they have pre-built binaries, you could include them in the build.sh file, similar as pre-built-llvm binaries.

[gsvgit]

Hello @yuleisui . We have several questions on grammars used for analysis.

1. Is there more or less formal description of this two grammars: PAGGrammar and PEGGrammar Detailed meaning of these grammars is not obvious.
2. We are slightly confused with rules of PAGGrammar. copy is declared as a terminal, but it occurs in left hand side of rules (e.g. copy -> vgep;). The same for gep_1: gep is declared as a terminal (we suppose it means that all gep_i are terminals) but it occurs in rule's LHS (gep_1 -> gep_0 F vgep | gep_0 F gep_1;). Additionally, gepbarpath, gepbar_i, copybar looks like terminals, but not listed in terminals and some of them are in LHS of some rules. Can you clarify how it works?

Thanks.

[yuleisui]

@TalbenXu could you help clarify the implementation?