# 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