Pointer analysis and separation logic

by Sims, Elodie-Jane

Abstract (Summary)
We are interested in modular static analysis to analyze softwares automatically. We

focus on programs with data structures, and in particular, programs with pointers. The

final goal is to find errors in a program (problems of dereferencing, aliasing, etc) or to prove

that a program is correct (regarding those problems) in an automatic way.

Isthiaq, Pym, O'Hearn and Reynolds have recently developed separation logics, which

are Hoare logics with assertions and predicates language that allow to prove the correctness

of programs that manipulate pointers. The semantics of the logic's triples ({P}C{P'}) is

defined by predicate transformers in the style of weakest preconditions.

We expressed and proved the correctness of those weakest preconditions (wlp) and

strongest postconditions (sp), in particular in the case of while-loops. The advance from

the existing work is that wlp and sp are defined for any formula, while previously existing

rules had syntactic restrictions.

We added fixpoints to the logic as well as a postponed substitution which then allow to

express recursive formula. We expressed wlp and sp in the extended logic and proved their

correctness. The postponed substitution is directly useful to express recursive formula. For

example, [equations removed, still appears in abstract]

describes the set of memory where x points to a list of integers.

Next, the goal was to use separation logic with fixpoints as an interface language for

pointer analysis. That is, translating the domains of those analyses into formula of the

logic (and conversely) and to prove their correctness. One might also use the translations

to prove the correctness of the pointer analysis itself.

We illustrate this approach with a simple pointers-partitioning analysis. We translate

the logic formula into an abstract language we designed which allows us to describe the

type of values registered in the memory (nil, integer, booleans, pointers to pairs of some

types, etc.) as well as the aliasing and non-aliasing relations between variables and locations in the memory. The main contribution is the definition of the abstract language and

its semantics in a concrete domain which is the same as the one for the semantics of formula. In particular, the semantics of the auxiliary variables, which is usually a question

of implementation, is explicit in our language and its semantics. The abstract language is

a partially reduced product of several subdomains and can be parametrised with existing

numerical domains. We created a subdomain which is a tabular data structure to cope with

the imprecision from not having sets of graphs. We expressed and proved the translations

of formula into this abstract language.

Bibliographical Information:


School:Kansas State University

School Location:USA - Kansas

Source Type:Master's Thesis

Keywords:pointers separation logic static analysis abstract interpretation shape computer science 0984


Date of Publication:01/01/2007

© 2009 All Rights Reserved.