Advertisement

Volume-Based Merge Heuristics for Disjunctive Numeric Domains

  • Andrew RuefEmail author
  • Kesha Hietala
  • Arlen Cox
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

Static analysis of numeric programs allows proving important properties of programs such as a lack of buffer overflows, division by zero, or integer overflow. By using convex numeric abstractions, such as polyhedra, octagons, or intervals, representations of program states are concise and the analysis operations are efficient. Unfortunately, many sets of program states can only be very imprecisely represented with a single convex numeric abstraction. This means that many important properties cannot be proven using only these abstractions. One solution to this problem is to use powerset abstractions where a set of convex numeric abstractions represents the union rather than the hull of those state sets. This leads to a new challenge: when to merge elements of the powerset and when to keep them separate. We present a new methodology for determining when to merge based on counting and volume arguments. Unlike previous techniques, this heuristic directly represents losses in precision through hull computations. In this paper we develop these techniques and show their utility on a number of programs from the SV-COMP and WCET benchmark suites.

References

  1. 1.
    Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 337–354. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-44898-5_19CrossRefGoogle Scholar
  2. 2.
    Bagnara, R., Hill, P.M., Zaffanella, E.: Exact join detection for convex polyhedra and other numerical abstractions. Comput. Geom. 43(5), 453–473 (2010)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Balakrishnan, G., Sankaranarayanan, S., Ivančić, F., Gupta, A.: Refining the control structure of loops using static analysis. In: EMSOFT (2009)Google Scholar
  4. 4.
    Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI (2001)Google Scholar
  5. 5.
    Barvinok, A.I.: A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed. Math. Oper. Res. 19(4), 769–779 (1994)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses (report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887–904. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_55CrossRefGoogle Scholar
  7. 7.
    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI (2007)Google Scholar
  8. 8.
    Blanchet, B., et al.: Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In: Mogensen, T.Æ., Schmidt, D.A., Sudborough, I.H. (eds.) The Essence of Computation. LNCS, vol. 2566, pp. 85–108. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-36377-7_5CrossRefGoogle Scholar
  9. 9.
    Boneh, A., Golan, A.: Constraints’ redundancy and feasible region boundedness by random feasible point generator (RFPG). In: Third European Congress on Operations Research, EURO III (1979)Google Scholar
  10. 10.
    Bromberger, M., Weidenbach, C.: Computing a complete basis for equalities implied by a system of LRA constraints. In: SMT, vol. 1617, pp. 15–30 (2016)Google Scholar
  11. 11.
    Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: ISOP (1976)Google Scholar
  12. 12.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)Google Scholar
  13. 13.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL (1979)Google Scholar
  14. 14.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL (1978)Google Scholar
  15. 15.
    Dutertre, B., De Moura, L.: The Yices SMT solver 2(2), pp. 1–2 (2006). Tool paper http://yices.csl.sri.com/tool-paper.pdf
  16. 16.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006).  https://doi.org/10.1007/11817963_11CrossRefGoogle Scholar
  17. 17.
    Dyer, M., Frieze, A., Kannan, R.: A random polynomial-time algorithm for approximating the volume of convex bodies. J. ACM 38(1), 1–17 (1991)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: PLDI (2009)Google Scholar
  19. 19.
    Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI (2010)Google Scholar
  20. 20.
    Gurfinkel, A., Chaki, S.: Boxes: a symbolic abstract domain of boxes. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 287–303. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15769-1_18CrossRefGoogle Scholar
  21. 21.
    Gustafsson, J., Betts, A., Ermedahl, A., Lisper, B.: The mälardalen wcet benchmarks: Past, present and future. In: OASIcs-OpenAccess Series in Informatics. vol. 15. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2010)Google Scholar
  22. 22.
    Handjieva, M., Tzolovski, S.: Refining static analyses by trace-based partitioning using control flow. In: Levi, G. (ed.) SAS 1998. LNCS, vol. 1503, pp. 200–214. Springer, Heidelberg (1998).  https://doi.org/10.1007/3-540-49727-7_12CrossRefGoogle Scholar
  23. 23.
    Henry, J., Monniaux, D., Moy, M.: Succinct representations for abstract interpretation. In: Miné, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 283–299. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-33125-1_20CrossRefGoogle Scholar
  24. 24.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL (2002)Google Scholar
  25. 25.
    Jeannet, B.: Dynamic partitioning in linear relation analysis: application to the verification of reactive systems. Formal Methods Syst. Des. 23(1), 5–37 (2003)CrossRefGoogle Scholar
  26. 26.
    Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_52CrossRefGoogle Scholar
  27. 27.
    Kannan, R., Lovász, L., Simonovits, M.: Random walks and an o*(n5) volume algorithm for convex bodies. Random Struct. Algorithms 11(1), 1–50 (1997)CrossRefGoogle Scholar
  28. 28.
    Kroese, D.P., Taimre, T., Botev, Z.I.: Markov Chain Monte Carlo, Chap. 6, pp. 225–280. Wiley, New York (2011)Google Scholar
  29. 29.
    Lattner, C.: Macroscopic data structure analysis and optimization. Ph.D. thesis, UIUC (2005)Google Scholar
  30. 30.
    Loechner, V.: Polylib: A library for manipulating parameterized polyhedra. Technical report, Université Louis Pasteur de Strasbourg (1999)Google Scholar
  31. 31.
    Miné, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31–100 (2006)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Navas, J.A.: CRAB: a language-agnostic library for static analysis (2018). https://github.com/seahorn/crab
  33. 33.
    Pak, I., Panova, G.: On the complexity of computing Kronecker coefficients. Comput. Complex. 26(1), 1–36 (2017)MathSciNetCrossRefGoogle Scholar
  34. 34.
    Popeea, C., Chin, W.-N.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 331–345. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-77505-8_26CrossRefGoogle Scholar
  35. 35.
    Rival, X., Mauborgne, L.: The trace partitioning abstract domain. TOPLAS 29(5), 26 (2007)CrossRefGoogle Scholar
  36. 36.
    Sankaranarayanan, S., Ivančić, F., Shlyakhter, I., Gupta, A.: Static analysis in disjunctive numerical domains. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 3–17. Springer, Heidelberg (2006).  https://doi.org/10.1007/11823230_2CrossRefzbMATHGoogle Scholar
  37. 37.
    Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop invariant generation using splitter predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 703–719. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_57CrossRefGoogle Scholar
  38. 38.
    Smith, R.L.: Monte Carlo procedures for generating random feasible solutions to mathematical programs. In: ORSA/TIMS Conference, May 1980Google Scholar
  39. 39.
    Sotin, P., Jeannet, B., Védrine, F., Goubault, E.: Policy iteration within logico-numerical abstract domains. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 290–305. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-24372-1_21CrossRefGoogle Scholar
  40. 40.
    Sweet, I., Trilla, J.M.C., Scherrer, C., Hicks, M., Magill, S.: What’s the over/under? Probabilistic bounds on information leakage. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 3–27. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89722-6_1CrossRefGoogle Scholar
  41. 41.
    Verdoolaege, S., Seghir, R., Beyls, K., Loechner, V., Bruynooghe, M.: Counting integer points in parametric polytopes using Barvinok’s rational functions. Algorithmica 48(1), 37–66 (2007)MathSciNetCrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.University of MarylandCollege ParkUSA
  2. 2.Center for Computing SciencesInstitute for Defense AnalysesBowieUSA

Personalised recommendations