Advertisement

Invertible Linear Transforms of Numerical Abstract Domains

  • Francesco RanzatoEmail author
  • Marco Zanella
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11002)

Abstract

We study systematic changes of numerical domains in abstract interpretation through invertible linear transforms of the Euclidean vector space, namely, through invertible real square matrices. We provide a full generalization, including abstract transfer functions, of the parallelotopes abstract domain, which turns out to be an instantiation of an invertible linear transform to the interval abstraction. Given an invertible square matrix M and a numerical abstraction A, we show that for a linear program P (i.e., using linear assignments and linear tests only), the analysis using the linearly transformed domain M(A) can be obtained by analysing on the original domain A a linearly transformed program \(P^M\). We also investigate completeness of abstract domains for invertible linear transforms. In particular, we show that, perhaps counterintuitively, octagons are not complete for \(45^{\circ }\) rotations and, additionally, cannot be derived as a complete refinement of intervals for some family of invertible linear transforms.

Notes

Acknowledgments

We are grateful to the anonymous referees for their helpful remarks. The doctoral fellowship of Marco Zanella is funded by Fondazione Bruno Kessler (FBK), Trento, Italy.

References

  1. 1.
    Amato, G., Parton, M., Scozzari, F.: Deriving numerical abstract domains via principal component analysis. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 134–150. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15769-1_9CrossRefzbMATHGoogle Scholar
  2. 2.
    Amato, G., Parton, M., Scozzari, F.: Discovering invariants via simple component analysis. J. Symb. Comput. 47, 1533–1560 (2012)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Amato, G., Rubino, M., Scozzari, F.: Inferring linear invariants with parallelotopes. Sci. Comput. Program. 148, 161–188 (2017)CrossRefGoogle Scholar
  4. 4.
    Amato, G., Scozzari, F.: The abstract domain of parallelotopes. In: Proceedings of 4th International Workshop on Numerical and Symbolic Abstract Domains (NSAD 2012) (2012). ENTCS 287, 17–28Google Scholar
  5. 5.
    Bourdoncle, F.: Abstract debugging of higher-order imperative languages. In: Proceedings ACM Internationl Conference on Programming Languages Design and Implementation (PLDI 1993), pp. 46–55. ACM Press (1993)Google Scholar
  6. 6.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixed points. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages (POPL 1977), pp. 238–252. ACM Press (1977)Google Scholar
  7. 7.
    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of programming languages, pp. 269–282. ACM (1979)Google Scholar
  8. 8.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th ACM Symposium on Principles of Programming Languages (POPL 1978), pp. 84–97. ACM (1978)Google Scholar
  9. 9.
    Filé, G., Giacobazzi, R., Ranzato, F.: A unifying view of abstract domain design. ACM Comput. Surv. 28(2), 333–336 (1996)CrossRefGoogle Scholar
  10. 10.
    Filé, G., Ranzato, F.: The powerset operator on abstract interpretations. Theor. Comput. Sci. 222(1), 77–111 (1999)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Giacobazzi, R., Ranzato, F.: Refining and compressing abstract domains. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 771–781. Springer, Heidelberg (1997).  https://doi.org/10.1007/3-540-63165-8_230CrossRefzbMATHGoogle Scholar
  12. 12.
    Giacobazzi, R., Ranzato, F.: The reduced relative power operation on abstract domains. Theor. Comput. Sci. 216(1–2), 159–211 (1999)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000)MathSciNetCrossRefGoogle Scholar
  14. 14.
    Karr, M.: Affine relationships among variables of a program. Acta Informatica 6, 133–151 (1976)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of the 1st ACM Symposium on Principles of Programming Languages (POPL 1973), pp. 194–206. ACM (1973)Google Scholar
  16. 16.
    Miné, A.: Weakly relational numerical abstract domains. Ph.D. thesis, École Normale Supérieure, Paris, France (2004)Google Scholar
  17. 17.
    Miné, A.: The octagon abstract domain. High. Order Symb. Comput. 19(1), 31–100 (2006)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Miné, A.: Tutorial on static inference of numeric invariants by abstract interpretation. Found. Trends Program. Lang. 4(3–4), 120–372 (2017)CrossRefGoogle Scholar
  19. 19.
    Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-30579-8_2CrossRefGoogle Scholar
  20. 20.
    Seladji, Y.: Finding relevant templates via the principal component analysis. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 483–499. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-52234-0_26CrossRefGoogle Scholar
  21. 21.
    Zhan, X.: Matrix Theory. American Mathematical Society, Providence (2013)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Dipartimento di MatematicaUniversity of PadovaPadovaItaly

Personalised recommendations