×

Automatically proving termination and memory safety for programs with pointer arithmetic. (English) Zbl 1409.68077

Summary: While automated verification of imperative programs has been studied intensively, proving termination of programs with explicit pointer arithmetic fully automatically was still an open problem. To close this gap, we introduce a novel abstract domain that can track allocated memory in detail. We use it to automatically construct a symbolic execution graph that over-approximates all possible runs of a program and that can be used to prove memory safety. This graph is then transformed into an integer transition system, whose termination can be proved by standard techniques. We implemented this approach in the automated termination prover AProVE and demonstrate its capability of analyzing C programs with pointer arithmetic that existing tools cannot handle.

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q42 Grammars and rewriting systems
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Albarghouthi, A., Li, Y., Gurfinkel, A., Chechik, M.: Ufo: A framework for abstraction- and interpolation-based software verification. In: Proceedings of CAV’12 · Zbl 1325.68145
[2] Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java Bytecode. In: Proceedings of FMOODS’08 · Zbl 1236.68042
[3] AProVE. http://aprove.informatik.rwth-aachen.de/eval/PointerJournal/ · Zbl 1325.68145
[4] Berdine, J., Cook, B., Distefano, D., O’Hearn, P.W.: Automatic termination proofs for programs with shape-shifting heaps. In: Proceedings of CAV’06 · Zbl 1188.68109
[5] Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O’Hearn, P.W.: Variance analyses from invariance analyses. In: Proceedings of POPL’07 · Zbl 1295.68076
[6] Berdine, J., Cook, B., Ishtiaq, S.: SLAyer: Memory safety for systems-level code. In: Proceedings of CAV’11
[7] Bertot, Y., Castéran, P.: CoqArt. Springer, 2004
[8] Blanqui, F., Koprowski, A.: CoLoR: A Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Math. Struct. Comput. Sci. 4, 827-859 (2011) · Zbl 1223.68101 · doi:10.1017/S0960129511000120
[9] Bodin, M., Jensen, T., Schmitt, A.: Certified abstract interpretation with pretty-big-step semantics. In: Proceedings of CPP’15 · Zbl 1464.68071
[10] Bouajjani, A., Bozga, M., Habermehl, P., Iosif, R., Moro, P., Vojnar, T.: Programs with lists are counter automata. Formal Methods Syst. Design 38(2), 158-192 (2011) · Zbl 1217.68059 · doi:10.1007/s10703-011-0111-7
[11] Brockschmidt, M., Otto, C., von Essen, C., Giesl, J.: Termination graphs for Java Bytecode. In: Verification, Induction, Termination Analysis, LNAI 6463, (2010) · Zbl 1309.68038
[12] Brockschmidt, M., Otto, C., Giesl, J.: Modular termination proofs of recursive Java Bytecode programs by term rewriting. In: Proceedings of RTA’11 · Zbl 1236.68036
[13] Brockschmidt, M., Ströder, T., Otto, C., Giesl, J.: Automated detection of non-termination and NullPointerExceptions for Java Bytecode. In: Proceedings of FoVeOOS’11
[14] Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: Proceedings of CAV’12
[15] Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Proceedings of CAV’13
[16] Brotherston, J., Gorogiannis, N.: Cyclic abduction of inductively defined safety and termination preconditions. In: Proceedings of SAS’14
[17] Cachera, D., Pichardie, D.: A certified denotational abstract interpreter. In: Proceedings of ITP’10 · Zbl 1291.68331
[18] Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of OSDI’08
[19] Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Beyond reachability: Shape abstraction in the presence of pointer arithmetic. In: Proceedings of SAS’06 · Zbl 1225.68069
[20] Calcagno, C., Distefano, D., O’Hearn, P.W., Yang, H.: Space invading systems code. In: Proceedings of LOPSTR’08
[21] Calcagno, C., Distefano, D.: Infer: An automatic program verifier for memory safety of C programs. In: Proceedings of NFM’11
[22] Chen, H.Y., David, C., Kroening, D., Schrammel, P., Wächter, N.: Synthesising interprocedural bit-precise termination proofs. In: Proceedings of ASE’15
[23] Clang compiler. http://clang.llvm.org
[24] Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752-794 (2003) · Zbl 1325.68145 · doi:10.1145/876638.876643
[25] Contejean, E., Courtieu, P., Forest, J., Pons, O., Urbain, X.: Automated certified proofs with CiME3. In: Proceedings of RTA’11 · Zbl 1236.68219
[26] Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Proceedings of SAS’05 · Zbl 1141.68365
[27] Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of PLDI’06 · Zbl 1141.68365
[28] Cook, B., Podelski, A., Rybalchenko, A.: Summarization for termination: no return!. Formal Methods Syst. Design 35(3), 369-387 (2009) · Zbl 1185.68412 · doi:10.1007/s10703-009-0087-8
[29] Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Proceedings of POPL’78 · Zbl 1217.68059
[30] David, C., Kroening, D., Lewis, M.: Unrestricted termination and non-termination arguments for bit-vector programs. In: Proceedings of ESOP’15 · Zbl 1335.68050
[31] de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Proceedings of TACAS’08 · Zbl 1213.68578
[32] D’Silva, V., Urban, C.: Conflict-driven conditional termination. In: Proceedings of CAV’15 · Zbl 1381.68155
[33] Dudka, K., Peringer, P., Vojnar, T.: Predator: A shape analyzer based on symbolic memory graphs (competition contribution). In: Proceedings of TACAS’14
[34] Dutertre, B., de Moura, L.: The Yices SMT solver. Tool paper at http://yices.csl.sri.com/tool-paper.pdf
[35] Falke, S., Kapur, D., Sinz. C.: Termination analysis of C programs using compiler intermediate languages. In: Proceedings of RTA’11 · Zbl 1236.68040
[36] Falke, S., Merz, F., Sinz, C.: LLBMC: Improved bounded model checking of C using LLVM (competition contribution). In: Proceedings of TACAS’13
[37] Fuhs, C., Giesl, J., Plücker, M., Schneider-Kamp, P., Falke, S.: Proving termination of integer term rewriting. In: Proceedings of RTA’09 · Zbl 1242.68131
[38] Giesl, J., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Otto, C., Plücker, M., Schneider-Kamp, P., Ströder, T., Swiderski, S., Thiemann, R.: Proving termination of programs automatically with AProVE. In: Proceedings of IJCAR’14 · Zbl 1409.68256
[39] Gonnord, L., Monniaux, D., Radanne, G.: Synthesis of ranking functions using extremal counterexamples. In: Proceedings of PLDI’15
[40] Gulwani, S., Tiwari, A.: An abstract domain for analyzing heap-manipulating low-level software. In: Proceedings of CAV’07 · Zbl 1135.68366
[41] Habermehl, P., Iosif, R., Rogalewicz, A., Vojnar, T.: Proving termination of tree manipulating programs. In: Proceedings of ATVA’07 · Zbl 1141.68469
[42] Harris, W.R., Lal, A., Nori, A., Rajamani, S.K.: Alternation for termination. In: Proceedings of SAS’10 · Zbl 1306.68027
[43] Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: Proceedings of ATVA’13 · Zbl 1410.68086
[44] Hensel, J., Giesl, J., Frohn, F., Ströder, T.: Proving termination of programs with bitvector arithmetic by symbolic execution. In: Proceedings of SEFM’16 · Zbl 1390.68181
[45] Iosif, R., Rogalewicz, A.: Automata-based termination proofs. Comput. Inf. 32(4), 739-775 (2013) · Zbl 1248.68148
[46] Jourdan, J.-H., Laporte, V., Blazy, S., Leroy, X., Pichardie, D.: A formally-verified C static analyzer. In: Proceedings of POPL’15
[47] Kop, C., Nishida, N.: Automatic constrained rewriting induction towards verifying procedural programs. In: Proceedings of APLAS’14 · Zbl 1453.68050
[48] Kop, C., Nishida, N.: Constrained Term Rewriting tooL. In: Proceedings of LPAR’15 · Zbl 1471.68110
[49] Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C. M.: Termination analysis with compositional transition invariants. In: Proceedings of CAV’10 · Zbl 1315.68106
[50] Larraz, D., Oliveras, A., Rodríguez-Carbonell, E., Rubio A.: Proving termination of imperative programs using Max-SMT. In: Proceedings of FMCAD’13 · Zbl 1452.68046
[51] Lattner, C., Adve V.S.: LLVM: A compilation framework for lifelong program analysis & transformation. In: Proceedings of CGO’04
[52] Le, T.C., Qin, S., Chin, W.: Termination and non-termination specification inference. In: Proceedings of PLDI’15
[53] LLVM reference manual. http://llvm.org/docs/LangRef.html
[54] Löwe, S., Mandrykin, M., Wendler, P.: CPAchecker with sequential combination of explicit-value analyses and predicate analyses (competition contribution). In: Proceedings of TACAS’14
[55] Magill, S.: Instrumentation Analysis: An Automated Method for Producing Numeric Abstractions of Heap-Manipulating Programs. Ph.D. thesis, CMU, Pittsburgh, PA (2010). Available at http://www.cs.cmu.edu/ smagill/papers/thesis.pdf
[56] Magill, S., Tsai, M., Lee, P., Tsay, Y.: Automatic numeric abstractions for heap-manipulating programs. In: Proceedings of POPL’10 · Zbl 1312.68063
[57] Miné, A.: The octagon abstract domain. Higher-Order and Symbolic Computation 19(1), 31-100 (2006) · Zbl 1105.68069 · doi:10.1007/s10990-006-8609-1
[58] Moy, Y., Marché, C.: Modular inference of subprogram contracts for safety checking. J. Symb. Comput., 45(11), 2010 · Zbl 1213.68385
[59] Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM, 53(6), 2006 · Zbl 1326.68164
[60] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic. Springer, 2002 · Zbl 0994.68131
[61] O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Proceedings of CSL’01 · Zbl 0999.68045
[62] http://fxr.watson.org/fxr/source/lib/libsa/strlen.c?v=OPENBSD
[63] Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proceedings of RTA’10 · Zbl 1236.68145
[64] Podelski, A., Rybalchenko, A.: ARMC: The logical choice for software model checking with abstraction refinement. In: Proceedings of PADL’07
[65] Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: Proceedings of POPL’95 · Zbl 0874.68133
[66] Spoto, F., Mesnard, F., Payet, É.: A termination analyser for Java Bytecode based on path-length. ACM TOPLAS, 32(3), 2010
[67] Ströder, T., Giesl, J., Brockschmidt, M., Frohn, F., Fuhs, C., Hensel, J., Schneider-Kamp, P.: Proving termination and memory safety for programs with pointer arithmetic. In: Proceedings of IJCAR’14 · Zbl 1423.68110
[68] Ströder, T., Aschermann, C., Frohn, F., Hensel, J., Giesl, J.: AProVE: Termination and memory safety of C programs (competition contribution). In: Proceedings of TACAS’15 · Zbl 1409.68254
[69] Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Proceedings of TPHOLs’09 · Zbl 1252.68265
[70] Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop summarization and termination analysis. In: Proceedings of TACAS’11 · Zbl 1315.68106
[71] Urban, C., Gurfinkel, A., Kahsai, T.: Synthesizing ranking functions from bits and pieces. In: Proceedings of TACAS’16
[72] Wikibooks C Programming. http://en.wikibooks.org/wiki/C_Programming/
[73] Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formalizing the LLVM IR for verified program transformations. In: Proceedings of POPL’12 · Zbl 1321.68207
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.