Automated verification of pointer programs in pointer logic

Abstract

Reasoning about pointer programs is difficult and challenging, while their safety is critical in software engineering. Storeless semantics pioneered by Jonkers provides a method to reason about pointer programs. However, the representation of memory states in Jonkers’ model is costly and redundant. This paper presents a new framework under a more efficient storeless model for automatically verifying properties of pointer programs related to the correct use of dynamically allocated memory such as absence of null dereferences, absence of dangling dereferences, absence of memory leaks, and preservation of structural invariants. The introduced logic – Pointer Logic, is developed to achieve such goals. To demonstrate that Pointer Logic is a useful storeless approach to verification, the Schorr-Waite tree-traversal algorithm which is always considered as a key test for pointer formalizations was verified via our analysis. Moreover, an experimental tool – plcc was implemented to automatically verify a number of non-trivial pointer programs.

References

1. O'Hearn P, Reynolds J, Yang H . Local reasoning about programs that alter data structures. In: Proceedings of the 15th International Workshopon Computer Science Logic. London: Springer, 2001, 1–19
2. Reynolds J . Separationlogic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in ComputerScience. Washington: IEEE Computer Society, 2002, 55–74
3. Jonkers H B M . Abstract storage structures. In: de Bakker, van. Vllet, eds. Algorithmic Languages. 1981, 321–343
4. Deutsch A . Astoreless model of aliasing and its abstractions using finite representationsof right-regular equivalence relations. In: Proceedings of the 1992 International Conference on Computer Languages. California: IEEE Computer Society, 1992, 2–13
5. Venet A . Automaticanalysis of pointer aliasing for untyped programs. Science of Computer Programming. 1999, 35(2):223–248. doi:10.1016/S0167-6423(99)00012-X
6. Bozga M, Iosif R, Laknech Y . Storeless semantics and alias logic. In: Proceedings of the 2003 ACM SIGPLAN workshop on Partial evaluationand semantics-based program manipulation. New York: ACM Press, 2003, 55–65
7. Rinetzky N, Bauer J, Reps T, et al.. A semantics for procedure local heaps and itsabstractions. In: Proceedings of the 32ndACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM Press, 2005, 296–309
8. Chen Y, Ge L, Hua B, et al.. Design of a certifying compiler supporting proofof program safety. In: Proceedings of the1st Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering. Washington: IEEE Computer Society, 2007, 117–126
9. Chen Y, Ge L, Hua B, et al.. A pointer logic and certifying compiler. Frontiers of Computer Science in China. 2007, 1(3):297–312. doi:10.1007/s11704-007-0029-9
10. Deutsch A . Interproceduralmay-alias analysis for pointers: beyond k-limiting. In: Proceedings of the ACMSIGPLAN'94 Conference on Programing language Design and Implementation. New York: ACM Press, 1994, 230–241
11. Bornat R . Provingpointer programs in hoare logic. In: Proceedingsof the 5th International Conference on Mathematics of Program Construction. London: Springer, 2000, 102–126
12. Topor R . Thecorrectness of the Schorr-Waite list marking algorithm. Acta Informatica. 1979, 11: 211–221. doi:10.1007/BF00289067
13. Yang H . Anexample of local reasoning in BI pointer logic: the Schorr-Waite graphmarking algorithm. In: Henglein F, Hughes J, MakholmH, et al.. eds. SPACE 2001: InformalProceedings of Workshop on Semantics, Program Analysis and ComputingEnvironments for Memory Management. IT University of Copenhagen, 2001, 41–68
14. Mehta F, Nipkow T . Proving pointer programsin higher-order logic. Information andComputation. 2005, 199(1–2): 200–227. doi:10.1016/j.ic.2004.10.007
15. Hubert T, Marché C . A case study of C sourcecode verification: the Schorr-Waite algorithm. In: Proceedings of the 3rd IEEE International Conference on SoftwareEngineering and Formal Methods. Washington: IEEE Computer Society, 2005, 190–199
16. Nipkow T, Paulson L, Wenzel M . Isabelle/HOL: A proof assistant for higher-order logic. Computer Science. London: Springer, 2002, 259–278
17. Bornat R, Sufrin B . Animating formal proofs atthe surface: the Jape proof calculator. The Computer Journal. 1999, 43: 177–192. doi:10.1093/comjnl/42.3.177
18. Loginov A, Reps T, Sagiv M . Automated verification of the Deutsch-Schorr-Waite tree-traversalalgorithm. In: Proceedings of the 13thInternational Static Analysis Symposium. London: Springer, 2006, 261–279
19. Cooper D C . Theorem proving in arithmetic without multiplication.In: Meltzer B, MichieD, eds, Machine Intelligence. 1972, 91–100
20. Hoare C A R . An axiomatic basis for computer programming. Communications of the ACM. 1969, 12(10): 576–583. doi:10.1145/363235.363259
21. Hoare C A R, He J . A trace model for pointersand objects. In: Proceedings of the 13thEuropean Conference on Object-Oriented Programming. London: Springer-Verlag, 1999, 1–17
22. Lahiri S K, Qadeer S . Verifying properties of well-foundedlinked lists. In: Proceedings of the 33thannual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York: ACM press, 2006, 115–126
23. Chatterjee S, Lahiri S K, Qadeer S, et al.. A reachability predicate for analyzing low-levelsoftware. In: Proceedings of the 13th InternationalConference on Tools and Algorithms for the Construction and Analysisof Systems. London: Springer, 2007, 19–33
24. Lahiri S K, Qadeer S . Back to the future: revisitingprecise program verification using SMT solvers. In: Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principlesof programming languages. NewYork: ACM press, 2008, 171–182
25. Møeller A, Schwartzbach M I . The pointer assertion logicengine. In: Proceedings of the ACM SIGPLAN2001 conference on Programming language design and implementation. New York: ACM Press, 2001, 221–231
26. Sagiv M, Reps T, Wilhelm R . Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems. 2002, 24(3): 217–298. doi:10.1145/514188.514190
27. Walker D, Morrisett G . Alias types for recursivedata structures. In: Selected papers fromthe 3rd International Workshop on Types in Compilation. London: Springer-Verlag, 2001, 177–206
28. Xi H . Appliedtype system (extended abstract). In: thepost-workshop proceedings of TYPES 2003. Berlin: Springer, 2004, 394–408
29. Chen C, Xi H . Combining programming withtheorem proving. In: Proceedings of the10th ACM SIGPLAN international conference on Functional programming. New York: ACM press, 2005, 66–77
30. Berdine J, Calcagno C, O'Hearn P W . Smallfoot: modular automatic assertion checking withseparation logic. In: Proceedings of the4th International Symposium on Formal Methods for Components and Objects. London: Springer, 2005, 115–137
31. Ireland A . TowardsAutomatic Assertion Refinement for Separation Logic. In: Proceedings of the 21st IEEE/ACM International Conference on AutomatedSoftware Engineering. Washington: IEEE Computer Society, 2006, 309–312
32. Nguyen H H, David C, Qin S, et al.. Automated verification of shape and size propertiesvia separation logic. In: Proceedings ofeighth International Conference on Verification, Model Checking andAbstract Interpretation. Berlin: Springer, 2007, 251–266
33. Berdine J, Calcagno C, O'Hearn P W . Symbolic execution with separation logic.In: Proceedings of the 3rd Asian Symposium on ProgrammingLanguages and Systems. London: Springer-Verlag, 2005, 52–68