Wiki

Clone wiki

llStar / Formulas

Function specifications and logic rules are written using separation logic formulas. Here we briefly describe their syntax. You can also find more technical information in this draft.

General syntax

Formulas in llStar consist of disjunctions || and spatial conjunctions * of predicates, according to the following grammar:

A ::= False | P | S | A1||A2 | A1*A2

Above, False is the formula that is never true, P stands for a pure predicate, and S for a spatial predicate. A disjunction A1 || A2 has the classical meaning that A1 or A2 is true. Spatial conjunction is inherited from separation logic, and A1 * A2 means that the current memory state can be split into two disjoint memory states (in the sense that they have disjoint sets of memory locations) such that the two substates satisfy the corresponding two subformulas.

Spatial predicates

The base spatial predicates understood by llStar are of three kinds:

S ::= pointer(?x, ?t, ?v) | malloced(?x, ?s) | user

In this grammar, ?x, ?t, etc. stand for any llStar expression, such as bvadd.64(z,bv_const("64", "2")) or pointer_type(integer_type("32")). Let us go through the predicates above one by one.

Pointer predicate

The basic ingredient of llStar formulas are pointer predicates, which indicate that certain regions of the memory are allocated, and can be accessed using a certain type. More precisely, the pointer(?x, ?t, ?v) predicate asserts that ?x is a valid memory location that contains a value ?v of type ?t. The size of the corresponding memory region corresponds to the size of ?t. This predicate is *precise* in the sense that it also asserts that the memory contains nothing else but this region. Memore regions can then be combined using the * connective of separation logic, as described above.

Heap allocation predicate

Some regions of memory are allocated on the stack (using alloca, while others are allocated on the heap (typically using malloc from the standard C library). The first kind of memory is automatically reclaimed at exit points of functions, while the latter should be reclaimed manually, or garbage collected. Since llStar also tries to prove the absence of memory leaks, this distinction is important.

Having two kinds of pointer predicates to reflect this situation would be extremely cumbersome, as e.g. many functions do not care what kind of pointers they are passed as long as they valid, and having different kinds of pointers would mean having to write several nearly-identical specs for these functions. Instead, llStar uses an additional predicate malloced(?x, ?s) to indicate that memory locations ?x to ?x + ?s - 1 have been allocated on the heap, and thus can be disposed, e.g. by calling free(?x).

User-defined predicates

Any predicate of the form name(?e1, ..., ?en) where name is a valid identifier is a spatial predicate. However, the base logic of llStar is only able to reason about pointer and malloced predicates. To support more predicates, additional reasoning rules can be added to llStar. There is builtin support to define additional types of data structure nodes as well.

Pure predicates

Pure predicates are generally solely concerned with values, and do not describe the contents of the memory. In particular, the * conjunction between pure predicates coincides with the regular conjunction "and" of classical logic. Pure predicates (except for equality and disequality) start with !. By default, llStar knows how to reason about the following predicates:

P ::= ?x = ?y | ?x != ?y
    | !bvult(?n1, ?n2) | !bvule(?n1, ?n2) | !bvugt(?n1, ?n2) | !bvuge(?n1, ?n2)
    | !bvslt(?n1, ?n2) | !bvsle(?n1, ?n2) | !bvsgt(?n1, ?n2) | !bvsge(?n1, ?n2)

Expressions can be compared for equality and disequality using respectively = and !=. The rest of the pure predicates are comparisons between bitvector expressions, and are, in order, unsigned less than, unsigned lesser or equal, unsigned greater than, unsigned greater or equal, and their signed counterparts.

As for spatial predicates, llStar supports arbitrary user-defined pure predicates, of the form !name(?e1, ..., ?en) where name is a valid identifier.

Updated