Various static analysis problems are reformulated as instances of the Context-Free Language Reachability (CFL-r) problem. One promising way to make solving CFL-r more practical for large-scale interprocedural graphs is to reduce CFL-r to linear algebra operations on sparse matrices, as they are efficiently executed on modern hardware. In this work, we present five optimizations for a matrix-based CFL-r algorithm that utilize the specific properties of both the underlying semiring and the widely-used linear algebra library SuiteSparse:GraphBlas. Our experimental results show that these optimizations result in orders of magnitude speedup, with the optimized matrix-based CFL-r algorithm consistently outperforming state-of-the-art CFL-r solvers across four considered static analyses.
翻译:各类静态分析问题被重新表述为上下文无关语言可达性(CFL-r)问题的实例。将CFL-r问题转化为稀疏矩阵的线性代数运算是一种有前景的方法,能够提高其在大型过程间图中求解的实用性,因为这类运算在现代硬件上可高效执行。本文针对基于矩阵的CFL-r算法提出了五种优化策略,这些优化充分利用了底层半环域的性质以及广泛使用的线性代数库SuiteSparse:GraphBlas的特性。实验结果表明,这些优化实现了数量级的加速,优化的基于矩阵的CFL-r算法在四种静态分析任务中均持续优于现有最优的CFL-r求解器。