QCP Tutorials Symbolic Execution

In the previously introduced swap function, there are two formal parameters px and py of integer pointer type, which can also be used as local variables within the function body:

void swap(int * px, int * py)
{
}

There are several ways to express "the value stored at address px is x" (where x is a logical variable) using assertions:

* px == x
store_int(px, x)
exists px_37, store_ptr(&px, px_37) * store_int(px_37, x)

Although these three assertions express the same meaning, we recommend that users -- especially beginners of the QCP tool -- use the last of the three. Among these three assertions, only the last one can be called a "QCP basic separation logic assertion." A QCP basic separation logic assertion requires that in an assertion of the following form, P1, P2, etc. are all memory-independent clauses, and the expressions in P1, P2...Pn and Q1, Q2...Qm (where both n and m can be 0) are all memory-independent expressions:

(P1 && P2 && ... && Pn) && (Q1 * Q2 * ... * Qm)

A QCP basic separation logic assertion is a proposition obtained by connecting propositions of the above form using exists or || (it may also have no exists or ||).

In this syntactic rule, the key requirement is that expressions in clauses must be "memory-independent expressions." Here, a "memory-independent expression" means that evaluating the expression does not involve memory reads. In the previous example, px is a program variable and x is a logical variable, so px is a memory-dependent expression, while &px and x are both memory-independent expressions. Furthermore, px + 8 and * px are memory-dependent expressions, whereas x + 1 and &px + 8 are memory-independent expressions.

Basic Separation Logic Assertions and Symbolic Execution of Memory Reads/Writes (1)

Why do we recommend that users use QCP basic separation logic assertions? In particular, why should memory-independent expressions be used in clauses? The main reason is that for beginners, using basic separation logic assertions often makes it easier to write correct assertions (especially loop invariants), and it is also easier to understand QCP's symbolic execution process based on QCP basic separation logic assertions.

Let us consider a more complex property: px and py are equal, and the value of * px (which is also the value of * py) is zero. This can be written as the following three assertions:

px == py && * px == 0
px == py && store_int(px, 0)
exists p, store_ptr(&px, p) * store_ptr(&py, p) * store_int(p, 0)

We now know that although these three assertions express the same meaning, only the third one is a basic separation logic assertion. Now consider the result of executing the program statement px = 0. If the program state before execution satisfies the above property, then the property satisfied by the program state after executing this statement can be described by one of the following three assertions:

px == 0 && * py == 0
px == 0 && store_int(py, int, 0)
exists p, store_ptr(&px, 0) * store_ptr(&py, p) * store_int(p, 0)

As you can see, if the first two assertions are adopted, then during symbolic execution, in addition to changing px == py to px == 0, other clauses (such as * px == 0 and store_int(px, 0)) would also be affected. However, if the third assertion -- the basic separation logic assertion -- is used, then the separating conjunction (i.e., the star "*") guarantees that other clauses are not affected.

Basic Separation Logic Assertions and Symbolic Execution of Memory Reads/Writes (2)

Now let us consider the result of symbolically executing * py = 1 after the previous three assertions.

• After px == py && * px == 0, symbolically executing * py = 1 might yield px == py && * px == 1;
• After px == py && store_int(px, 0), symbolically executing * py = 1 might yield px == py && store_int(px, 1);
• After exists p, store_ptr(&px, p) * store_ptr(&py, p) * store_int(p, 0), symbolically executing * py = 1 yields exists p, store_ptr(&px, p) * store_ptr(&py, p) * store_int(p, 1).

Again, we can see that performing symbolic execution based on the first two assertions makes it nontrivial to correctly identify which clause should be modified. With basic separation logic, however, it is very clear: to write a new value to * py, we first need to obtain the value of py, which means reading a value from the address &py. That value is p (obtained from the clause store_ptr(&py, p)); then we modify the value at address p, which means modifying the clause to store_int(p, 1).

Using Concise Separation Logic Assertions in Simple Cases

In some simple cases, a C program may not involve data structures such as structs, nor involve address-of operations or pointer dereferences. In such cases, even without using QCP basic separation logic assertions, it is possible to accurately and unambiguously describe the properties that the program state should satisfy.

Take the add function as an example (shown below):

int add(int x, int y)
  /*@ Require
        0 <= x && x <= 100 && 
        0 <= y && y <= 100
      Ensure
        __return == x + y
   */
{
  int z = x + y;
  return z;
}

After entering the function body, the system allocates memory for the formal parameters x and y. Expressed using basic separation logic assertions, this is:

exists x_33 y_30,
  0 <= x_33 && x_33 <= 100 && 0 <= y_30 && y_30 <= 100 &&
  store_int(&x, x_33) * store_int(&y, y_30)

Since this program does not involve pointer operations or complex C data structures such as structs, simplifying the above basic separation logic assertion as follows does not introduce ambiguity:

0 <= x && x <= 100 &&  0 <= y && y <= 100

It is worth noting that although this assertion looks literally identical to the Require condition of the add function, x and y are now C variables with allocated memory. Therefore, as an assertion inside the function body, its meaning is subtly different from its meaning as a Require condition.

Next, after declaring the variable z and initializing it, the basic separation logic assertion obtained by symbolic execution should be:

exists x_33 y_30, 0 <= x_33 && x_33 <= 100 && 0 <= y_30 && y_30 <= 100 &&
                  store_int(&x, x_33) * store_int(&y, y_30) *
                  store_int(&z, x_33 + y_30)

This can be abbreviated as:

0 <= x && x <= 100 &&  0 <= y && y <= 100 && z == x + y

QCP can accept both basic separation logic assertions from users and such "concise" separation logic assertions, converting the latter internally into basic separation logic assertions. We recommend that QCP users use basic separation logic assertions in most cases. Of course, when the relevant C program is indeed simple, using concise separation logic assertions is also perfectly fine.