Gagandeep Singh
Markus Püschel
Abstract
Numerical abstract domains such as Polyhedra, Octahedron, Octagon, Interval, and others are an essential component of static program analysis. The choice of domain offers a performance/precision tradeoff ranging from cheap and imprecise (Interval) to expensive and precise (Polyhedra). Recently, significant speedups were achieved for Octagon and Polyhedra by manually decomposing their transformers to work with the Cartesian product of projections associated with partitions of the variable set. While practically useful, this manual process is time consuming, error-prone, and has to be applied from scratch for every domain.
In this paper, we present a generic approach for decomposing the transformers of sub-polyhedra domains along with conditions for checking whether the decomposed transformers lose precision with respect to the original transformers. These conditions are satisfied by most practical transformers, thus our approach is suitable for increasing the performance of these transformers without compromising their precision. Furthermore, our approach is ``black box:'' it does not require changes to the internals of the original non-decomposed transformers or additional manual effort per domain.
We implemented our approach and applied it to the domains of Zones, Octagon, and Polyhedra. We then compared the performance of the decomposed transformers obtained with our generic method versus the state of the art: the (non-decomposed) PPL for Polyhedra and the much faster ELINA (which uses manual decomposition) for Polyhedra and Octagon. Against ELINA we demonstrate finer partitions and an associated speedup of about 2x on average. Our results indicate that the general construction presented in this work is a viable method for improving the performance of sub-polyhedra domains. It enables designers of abstract domains to benefit from decomposition without re-writing all of their transformers from scratch as required by prior work.
Supplemental Material
- ELINA: ETH Library for Numerical Analysis. http://elina.ethz.ch.Google Scholar
- R. Bagnara, P. M. Hill, and E. Zaffanella. The Parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program., 72(1-2):3–21, 2008. Google ScholarDigital Library
- D. Beyer. Reliable and reproducible competition results with benchexec and witnesses (report on sv-comp 2016). In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 887–904, 2016.Google ScholarDigital Library
- B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In Proc. Programming Language Design and Implementation (PLDI), pages 196–207, 2003. Google ScholarDigital Library
- N. Chernikova. Algorithm for discovering the set of all the solutions of a linear programming problem. USSR Computational Mathematics and Mathematical Physics, 8(6):282 – 293, 1968. Google ScholarCross Ref
- R. ClarisÃş and J. Cortadella. The octahedron abstract domain. Science of Computer Programming, 64:115 – 139, 2007. Google ScholarDigital Library
- P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proc. International Symposium on Programming, pages 106–130, 1976.Google Scholar
- P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proc. Principles of Programming Languages (POPL), pages 84–96, 1978. Google ScholarDigital Library
- R. Cousot, R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. Science of Computer Programming, 58(1):28 – 56, 2005.Google Scholar
- P. Ferrara, F. Logozzo, and M. Fähndrich. Safer unsafe code for .net. SIGPLAN Not., 43:329–346, 2008. Google ScholarDigital Library
- G. Gange, J. A. Navas, P. Schachte, H. Søndergaard, and P. J. Stuckey. Exploiting sparsity in difference-bound matrices. In Proc. Static Analysis Symposium (SAS), pages 189–211, 2016. Google ScholarCross Ref
- R. Giacobazzi, F. Ranzato, and F. Scozzari. Making abstract interpretations complete. J. ACM, 47(2):361–416, Mar. 2000. Google ScholarDigital Library
- A. Gurfinkel, T. Kahsai, A. Komuravelli, and J. A. Navas. The seahorn verification framework. In Proc. Computer Aided Verification (CAV), pages 343–361, 2015. Google ScholarCross Ref
- N. Halbwachs, D. Merchat, and C. Parent-Vigouroux. Cartesian factoring of polyhedra in linear relation analysis. In Proc. Static Analysis Symposium (SAS), pages 355–365, 2003. Google ScholarCross Ref
- N. Halbwachs, D. Merchat, and L. Gonnord. Some ways to reduce the space dimension in polyhedra computations. Formal Methods in System Design (FMSD), 29(1):79–95, 2006. Google ScholarDigital Library
- K. Heo, H. Oh, and H. Yang. Learning a variable-clustering strategy for octagon from labeled data generated by a static analysis. In Proc. Static Analysis Symposium (SAS), pages 237–256, 2016. Google ScholarCross Ref
- J. M. Howe and A. King. Logahedra: A new weakly relational domain. In Proc. Automated Technology for Verification and Analysis (ATVA), pages 306–320, 2009. Google ScholarDigital Library
- J.-H. Jourdan. Sparsity preserving algorithms for octagons. Electronic Notes in Theoretical Computer Science, 331:57 – 70, 2017. Workshop on Numerical and Symbolic Abstract Domains (NSAD). Google ScholarCross Ref
- M. Karr. Affine relationships among variables of a program. Acta Informatica, 6:133–151, 1976. Google ScholarDigital Library
- F. Logozzo and M. Fähndrich. Pentagons: A weakly relational abstract domain for the efficient validation of array accesses. In Proc. Symposium on Applied Computing (SCP), pages 184–188, 2008. Google ScholarDigital Library
- J. louis Imbert. Fourier’s elimination: Which to choose? Principles and Practice of Constraint Programming, pages 117–129, 1993.Google Scholar
- A. Maréchal and M. Périn. Efficient elimination of redundancies in polyhedra by raytracing. In Proc. Verification, Model Checking, and Abstract Interpretation, (VMCAI), pages 367–385, 2017. Google ScholarCross Ref
- A. Maréchal, D. Monniaux, and M. Périn. Scalable minimizing-operators on polyhedra via parametric linear programming. In Proc. Static Analysis Symposium (SAS), pages 212–231, 2017. Google ScholarCross Ref
- A. Miné. A few graph-based relational numerical abstract domains. In Proc. Static Analysis Symposium (SAS), pages 117–132, 2002. Google ScholarCross Ref
- A. Miné. The octagon abstract domain. Higher Order and Symbolic Computation, 19(1):31–100, 2006. Google ScholarDigital Library
- A. Miné, E. RodrÃŋguez-Carbonell, and A. Simon. Speeding up polyhedral analysis by identifying common constraints. Electronic Notes in Theoretical Computer Science, 267(1):127 – 138, 2010. Google ScholarDigital Library
- F. Ranzato and F. Tapparo. Strong preservation as completeness in abstract interpretation. In Proc. European Symposium on Programming (ESOP), pages 18–32, 2004. Google ScholarCross Ref
- A. Simon and A. King. Exploiting sparsity in polyhedral analysis. In Proc. Static Analysis Symposium (SAS), pages 336–351, 2005. Google ScholarDigital Library
- A. Simon and A. King. The two variable per inequality abstract domain. Higher Order Symbolic Computation (HOSC), 23: 87–143, 2010. Google ScholarDigital Library
- G. Singh, M. Püschel, and M. Vechev. Making numerical program analysis fast. In Proc. Programming Language Design and Implementation (PLDI), pages 303–313, 2015. Google ScholarDigital Library
- G. Singh, M. Püschel, and M. Vechev. Fast polyhedra abstract domain. In Proc. Principles of Programming Languages (POPL), pages 46–59, 2017. Google ScholarDigital Library
- A. Venet and G. Brat. Precise and efficient static array bound checking for large embedded C programs. In Proc. Programming Language Design and Implementation (PLDI), pages 231–242, 2004. Google ScholarDigital Library
- H. L. Verge. A note on Chernikova’s algorithm. Technical report, 1994.Google Scholar
Index Terms
- A practical construction for decomposing numerical abstract domains
Recommendations
Fast polyhedra abstract domain
POPL '17: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming LanguagesNumerical abstract domains are an important ingredient of modern static analyzers used for verifying critical program properties (e.g., absence of buffer overflow or memory safety). Among the many numerical domains introduced over the years, Polyhedra ...
Learning fast and precise numerical analysis
PLDI 2020: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and ImplementationNumerical abstract domains are a key component of modern static analyzers. Despite recent advances, precise analysis with highly expressive domains remains too costly for many real-world programs. To address this challenge, we introduce a new data-...
Numerical static analysis with Soot
SOAP '13: Proceedings of the 2nd ACM SIGPLAN International Workshop on State Of the Art in Java Program analysisNumerical static analysis computes an approximation of all the possible values that a numeric variable may assume, in any execution of the program. Many numerical static analyses have been proposed exploiting the theory of abstract interpretation, which ...
Comments