Abstract
We present a new modular way to structure abstract interpreters. Modular means that new analysis domains may be plugged-in. These abstract domains can communicate through different means to achieve maximal precision. First, all abstractions work cooperatively to emit alarms that exclude the undesirable behaviors of the program. Second, the state abstract domains may exchange information through abstractions of the possible value for expressions. Those value abstractions are themselves extensible, should two domains require a novel form of cooperation. We used this approach to design \({\textsc {eva}}\), an abstract interpreter for C implemented within the \(\textsc {Frama}\text {-}\textsc {C}\) framework. We present the domains that are available so far within \({\textsc {eva}}\), and show that this communication mechanism is able to handle them seamlessly.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Directory src/plugins/value/ of the \(\textsc {Frama}\text {-}\textsc {C}\) source files, available at http://frama-c.com/download.html.
- 2.
Bitfields, flexible array members and some GNU extensions are supported. Support for dynamic allocation is preliminary. Recursion, \(\texttt {{setjmp}/}{} \texttt {{longjmp}}\), \(\texttt {complex}\) types, \(\texttt {alloca}\) and variable-length arrays are not supported.
- 3.
These are not undefined behaviors w.r.t. the ISO C99 or IEEE 754 specifications, but we choose to report them as undesirable errors.
References
Balakrishnan, G., Reps, T.: Recency-abstraction for heap-allocated storage. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 221–239. Springer, Heidelberg (2006). doi:10.1007/11823230_15
Beyer, D., Henzinger, T.A., Théoduloz, G.: Program analysis with dynamic precision adjustment. In: ASE, pp. 29–38 (2008)
Bonichon, R., Cuoq, P.: A mergeable interval map. Stud. Inform. Univ. 9(1), 5–37 (2011)
Boulanger, J.-L. (ed.): Static Analysis of Software: The Abstract Interpretation. Wiley-ISTE, New York (2011)
Brat, G., Navas, J.A., Shi, N., Venet, A.: IKOS: A framework for static analysis based on abstract interpretation. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 271–277. Springer, Cham (2014). doi:10.1007/978-3-319-10431-7_20
Cortesi, A., Le Charlier, B., Van Hentenryck, P.: Combinations of abstract domains for logic programming: open product and generic pattern construction. Sci. Comput. Program. 38(1–3), 27–71 (2000)
Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. In: Essays Dedicated to D. Schmidt on the Occasion of his 60th Birthday, pp. 325–336 (2013)
Cousot, P.: The calculational design of a generic abstract interpreter. In: Calculational System Design. NATO ASI Series F. IOS Press (1999)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Principles of Programming Languages, pp. 269–282 (1979)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Combination of abstractions in the ASTRÉE static analyzer. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol. 4435, pp. 272–300. Springer, Heidelberg (2007). doi:10.1007/978-3-540-77505-8_23
Cuoq, P., Hilsenkopf, P., Kirchner, F., Labbé, S., Thuy, N., Yakobowski, B.: Formal verification of software important to safety using the Frama-C tool suite. In: NPIC & HMIT (2012)
Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Berlin (2011). doi:10.1007/978-3-642-18070-5_2
International Organization for Standardization (ISO). International Standard ISO/IEC 9899: 1999 - Programming languages - C. Technical Corrigendum 3 (2007)
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, Berlin (2009). doi:10.1007/978-3-642-02658-4_52
Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: Principles of Programming Language, pp. 247–259 (2015)
Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: A software analysis perspective. Formal Asp. Comput. 27(3), 573–609 (2015)
Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 5–20. Springer, Berlin (2005). doi:10.1007/978-3-540-31987-0_2
Miné, A.: The octagon abstract domain. In: Burd, E., Aiken, P., Koschke, R. (eds.) Proceedings of the Eighth Working Conference on Reverse Engineering, WCRE 2001, Stuttgart, Germany, 2–5 October 2001, p. 310. IEEE Computer Society (2001)
Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: LCTES, pp. 54–63. ACM (2006)
Miné, A.: Symbolic methods to enhance the precision of numerical abstract domains. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 348–363. Springer, Heidelberg (2005). doi:10.1007/11609773_23
Venet, A.J.: The gauge domain: scalable analysis of linear inequality invariants. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 139–154. Springer, Berlin (2012). doi:10.1007/978-3-642-31424-7_15
Yakobowski, B.: Fast whole-program verification using on-the-fly summarization. In: Workshop on Tools for Automatic Program Analysis (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Blazy, S., Bühler, D., Yakobowski, B. (2017). Structuring Abstract Interpreters Through State and Value Abstractions. In: Bouajjani, A., Monniaux, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2017. Lecture Notes in Computer Science(), vol 10145. Springer, Cham. https://doi.org/10.1007/978-3-319-52234-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-52234-0_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-52233-3
Online ISBN: 978-3-319-52234-0
eBook Packages: Computer ScienceComputer Science (R0)