×

A sparse evaluation technique for detailed semantic analyses. (English) Zbl 1308.68043

Summary: We present a sparse evaluation technique that is effectively applicable to a set of elaborate semantic-based static analyses. Existing sparse evaluation techniques are effective only when the underlying analyses have comparably low precision. For example, if a pointer analysis precision is not affected by numeric statements like \(x:=1\) then existing sparse evaluation techniques can remove the statement, but otherwise, the statement cannot be removed. Our technique, which is a fine-grained sparse evaluation technique, is effectively applicable even to elaborate analyses. A key insight of our technique is that, even though a statement is relevant to an analysis, it is typical that analyzing the statement involves only a tiny subset of its input abstract memory and the most are irrelevant. By exploiting this sparsity, our technique transforms the original analysis into a form that does not involve the fine-grained irrelevant semantic behaviors. We formalize our technique within the abstract interpretation framework. In experiments with a C static analyzer, our technique improved the analysis speed by on average \(14\times\).

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Octagon
Full Text: DOI

References:

[7] Cousot, P.; Cousot, R.; Feret, J.; Mauborgne, L.; Miné, A.; Rival, X., Why does astrée scale up?, Form Methods Syst Des, 35, December (3), 229-264 (2009) · Zbl 1185.68241
[9] Cousot, Patrick; Cousot, Radhia, Abstract interpretation frameworks, J Logic Comput, 2, 4, 511-547 (1992) · Zbl 0783.68073
[10] Cytron, Ron; Ferrante, Jeanne; Rosen, Barry K.; Wegman, Mark N.; Zadeck, F. Kenneth, Efficiently computing static single assignment form and the control dependence graph, ACM Trans Program Lang Syst, 13, October (4), 451-490 (1991)
[11] Cytron, Ron K.; Ferrante, Jeanne, Efficiently computing \(ϕ\)-nodes on-the-fly, ACM Trans Program Lang Syst, 17, May, 487-506 (1995)
[13] Ferrante, Jeanne; Ottenstein, Karl J.; Warren, Joe D., The program dependence graph and its use in optimization, ACM Trans Program Lang Syst, 9, July (3), 319-349 (1987) · Zbl 0623.68012
[19] Mauborgne, Laurent; Rival, Xavier, Trace partitioning in abstract interpretation based static analyzers, (Sagiv, M., Proceedings of European symposium on programming. Lecture notes in computer science, vol. 3444 (2005), Springer-Verlag: Springer-Verlag London, UK), 5-20 · Zbl 1108.68427
[20] Miné, A., The octagon abstract domain, Higher-Order Symb Comput, 19, 1, 31-100 (2006) · Zbl 1105.68069
[26] Pingali, Keshav; Bilardi, Gianfranco, Optimal control dependence computation and the roman chariots problem, ACM Trans Program Lang Syst, 19, May, 462-491 (1997)
[27] Ramalingam, G., On sparse evaluation representations, Theor Comput Sci, 277, 1-2, 119-147 (2002) · Zbl 0996.68131
[29] Sagiv, Mooly; Reps, Thomas; Horwitz, Susan, Precise interprocedural dataflow analysis with applications to constant propagation, Theor Comput Sci, 167, October (1-2), 131-170 (1996) · Zbl 0874.68133
[32] Wegman, Mark N.; Zadeck, F. Kenneth, Constant propagation with conditional branches, ACM Trans Program Lang Syst, 13, April, 181-210 (1991)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.