QCP Tutorials Memory and Assertions

A key feature of C programs is their ability to read from and write to memory directly via memory addresses. For example, the following C program swaps the values at two addresses.

void swap(int * px, int * py)
{
  int t;
  t = * px;
  * px = * py;
  * py = t;
}

QCP requires that specifications involving memory operations strictly distinguish between the cases where memory addresses are the same and where they are different. Here we only consider the more common case where px and py are different addresses -- in other words, the memory regions they point to are disjoint. Under this assumption, we can state: for any values x and y, if initially x is stored at address px and y is stored at address py, then after executing swap, y is stored at address px and x is stored at address py. In QCP, this specification can be written as follows:

void swap(int * px, int * py)
/*@ With x y
    Require store_int(px, x) * store_int(py, y)
    Ensure store_int(px, y) * store_int(py, x) */
{
  int t;
  t = * px;
  * px = * py;
  * py = t;
}

The syntactic elements of this specification are explained one by one below.

The With Clause

The With x y in the specification means "for all x and y" the following specification holds. It is worth noting that x and y here are not program variables -- they are logical variables, used solely to help write assertions or specifications.

Predicates such as store_int

store_int(px, x) states that we own the memory pointed to by address px, that the content at address px has been initialized, and that it stores a signed 32-bit integer value x. Here, because px is a C variable of type int *, QCP can infer that the memory it points to is typically a region storing a signed 32-bit integer. Therefore, when writing assertions you may also omit the type and simply write store(px, x). In cases where QCP cannot perform such automatic inference, or where you want to make the type explicit in the assertion, you can write store_int(px, x) or store(px, int, x) as in the example above. Additionally, if you own read/write permission to a given address but the data at that address is uninitialized or it is unknown whether it has been initialized (note that reading a value from such an address is undefined behavior under the C standard and is not permitted!), you can use the has_permission predicate. has_permission(px) states that we have read/write permission for address px, but it does not guarantee that the data at that address has been initialized. In other words, store(px, x) implies has_permission(px), but conversely, has_permission(px) holding does not mean there exists a value v such that store(px, v). In QCP, has_permission can also specify a type, for example has_permission(px, int) or has_int_permission(px).

It is worth noting that the has_permission and store families of predicates can only be used with basic types such as the integer types listed below, their pointer types, or pointer-to-pointer types, and cannot be used with compound types such as struct, union, or arrays.

The Separating Conjunction Operator (Star) in Assertions

The star "*" in assertions is the separating conjunction connective from separation logic. "P * Q" states that the current memory can be divided into two disjoint parts, one satisfying P and the other satisfying Q. From this, it is clear that store_int(px, x) * store_int(py, y) implies that px and py are different addresses.

When writing specifications for C programs, we often write the separating conjunction of multiple (three or more) clauses, not just two. Taking three clauses as an example, "(P * Q) * R" states that memory can be divided into two disjoint parts, where the first part can be further divided into two smaller disjoint parts -- that is, three pairwise disjoint parts satisfying properties P, Q, and R respectively. It is therefore easy to see that the separating conjunction (the star "*" in QCP) is both commutative and associative. For example, the assertion store(px, x) * store(py, y) * store(pz, z) means "px, py, and pz are three mutually distinct memory addresses, and the values stored at these three addresses are x, y, and z." When writing such assertions, there is no need to add extra parentheses around either the first or second star.