QCP Tutorials Symbolic Execution

Symbolic Execution with an Added Assertion in swap

Consider the swap function again.

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;
}

After the first assignment, the program state satisfies the following assertion, which is also the strongest postcondition obtained by QCP:

store_int(&t, x) *
store_ptr(&px, px_37) *
store_ptr(&py, py_40) *
store_int(px_37, x) *
store_int(py_40, y)

Here px_37 and py_40 represent the initial values px@pre and py@pre. Looking at the rest of the program, we know that the current value stored at *px is no longer needed. At this program point we can assert a weaker property:

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;
  /*@ Assert
        store_int(&t, x) *
        store_ptr(&px, px@pre) *
        store_ptr(&py, py@pre) *
        has_int_permission(px@pre) *
        store(py@pre, y) */
  * px = * py;
  * py = t;
}

Adding this assertion means that whenever execution reaches this point, the program state must satisfy the stated property. Subsequent verification then relies only on this property. Even if the stronger original property is true, later verification does not need to use it. QCP therefore generates the following VC and continues symbolic execution from the user-provided assertion.

store_int(&t, x) *
store_ptr(&px, px_37) *
store_ptr(&py, py_40) *
store_int(px_37, x) *
store_int(py_40, y)
|-- store_int(&t, x) *
    store_ptr(&px, px_37) *
    store_ptr(&py, py_40) *
    has_int_permission(px_37) *
    store_int(py_40, y)

The following two screenshots compare the symbolic execution state before and after executing this assertion. After the assertion is processed, the Normal assertion list contains the has_permission predicate introduced by the annotation.

Assertion Annotations After Symbolically Executing an if Statement

The following max3 function computes the maximum of three integers.

int max3(int x, int y, int z)
/*@ Require emp
    Ensure __return >= x &&
           __return >= y &&
           __return >= z */
{
  int t;
  if (x < y) {
    t = y;
  }
  else {
    t = x;
  }
  /*@ Assert t >= x@pre && t >= y@pre &&
             x == x@pre && y == y@pre && z == z@pre */
  if (t < z) {
    return z;
  }
  else {
    return t;
  }
}

This function contains two if statements. As before, after symbolically executing the first if, QCP obtains two Normal assertions.

If QCP then symbolically executes the assertion annotation after this if, it generates two VCs: each of the two Normal assertions must imply the manually inserted assertion. Written in basic separation-logic notation, the two VCs are:

x_54 < y_51 &&
store_int(&t, y_51) *
store_int(&x, x_54) *
store_int(&y, y_51) *
store_int(&z, z_48)
|--
exists t_64,
t_64 >= x_54 &&
t_64 >= y_51 &&
store_int(&t, t64) *
store_int(&x, x_54) *
store_int(&y, y_51) *
store_int(&z, z_48)

x_54 >= y_51 &&
store_int(&t, y_51) *
store_int(&x, x_54) *
store_int(&y, y_51) *
store_int(&z, z_48)
|--
exists t_64,
t_64 >= x_54 &&
t_64 >= y_51 &&
store_int(&t, t64) *
store_int(&x, x_54) *
store_int(&y, y_51) *
store_int(&z, z_48)

In the IDE, after the assertion is processed, the two branch assertions are merged into the user-provided assertion, and symbolic execution proceeds from there.