Byte-Precise Verification of Low-Level List Manipulation
We propose a new approach to shape analysis of programs with linked lists that use low-level memory operations. Such operations include pointer arithmetic, safe usage of invalid pointers, block operations with memory, reinterpretation of the memory contents, address alignment, etc. Our approach is based on a new representation of sets of heaps, which is to some degree inspired by works on separation logic with higher-order list predicates, but it is graph-based and uses a more fine-grained (byte-precise) memory model in order to support the various low-level memory operations. The approach was implemented in the Predator tool and successfully validated on multiple non-trivial case studies that are beyond the capabilities of other current fully automated shape analysis tools.
KeywordsSymbolic Execution Pointer Arithmetic Separation Logic List Node Neighbouring Object
Unable to display preview. Download preview PDF.
- 8.Dudka, K., Peringer, P., Vojnar, T.: Byte-Precise Verification of Low-Level List Manipulation. Technical report FIT-TR-2012-04, FIT BUT (2012), http://www.fit.vutbr.cz/~idudka/pub/FIT-TR-2012-04.pdf
- 13.Reps, T., Horwitz, S., Sagiv, M.: Precise Interprocedural Dataflow Analysis via Graph Reachability. In: Proc. of POPL 1995. ACM Press (1995)Google Scholar
- 14.Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. In: ACM Transactions on Programming Languages and Systems (TOPLAS), 24(3) (2002)Google Scholar
- 15.Tuch, H.: Formal Verification of C Systems Code. Journal of Automated Reasoning 42(2-4) (2009)Google Scholar
- 16.Yang, H., Lee, O., Calcagno, C., Distefano, D., O’Hearn, P.W.: On Scalable Shape Analysis. Technical report RR-07-10, Queen Mary, University of London (2007)Google Scholar