Shape analysis algorithms statically infer deep properties of the runtime heap, such as whether a variable points to a cyclic or acyclic linked list. Previous shape analyses have tended to avoid features of low-level programming languages, such as memory disposal and pointer arithmetic. Yet, these features are used in many important programs, particularly systems programs.
In this talk I will describe how shape analysis for low-level code can be done with separation logic. A crucial element of the approach is the way it negotiates a transit between a low-level RAM view of memory and a higher, fictional, view that abstracts from the representation of nodes and linked structures as certain configurations of the RAM. The analysis algorithm can be seen as conducting a proof search in separation logic, and I will show how this provides a flexible way of exploring non-standard optimizations, while maintaining soundness.