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.
Formulas in llStar consist of disjunctions
|| and spatial conjunctions
* of predicates, according to the following grammar:
A ::= False | P | S | A1||A2 | A1*A2
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
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.
The base spatial predicates understood by llStar are of three kinds:
S ::= pointer(?x, ?t, ?v) | malloced(?x, ?s) | user
In this grammar,
?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.
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 + ?s - 1 have been allocated on the heap, and thus can be disposed, e.g. by calling
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
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 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
!=. 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.