QCP Tutorials Symbolic Execution

Verification Conditions for Ensure Assertions

The swap Function

Here is the swap function introduced earlier.

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

When QCP verifies this C function, symbolic execution processes entering the function body, variable declaration, assignment statements, and leaving the function body in order. At the end it obtains the following assertion:

store_int(px_37, y) *
store_int(py_40, x)

Here px_37 and py_40 correspond to the initial values of px and py. The Ensure condition is also:

store_int(px_37, y) *
store_int(py_40, x)

At this point the QCP symbolic executor generates the following VC. If this VC is valid, then the swap function satisfies the specification described by its Require and Ensure assertions.

store_int(px_37, y) *
store_int(py_40, x)
|--
store_int(px_37, y) *
store_int(py_40, x)

A Weaker Version of swap

If we change the Ensure condition of swap as follows:

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

then the specification describes a weaker safety property: after swap, the function still owns read/write permission for the addresses px and py, but it no longer guarantees whether the values stored there are initialized.

Because the Require condition is unchanged, symbolic execution still obtains the same assertion as before. Therefore QCP generates this VC:

store_int(px_37, y) *
store_int(py_40, x)
|--
has_int_permission(px_37) *
has_int_permission(py_40)

This VC is valid, so QCP can confirm that swap satisfies the weakened specification.

Additional Conditions for Expression Evaluation

C does not guarantee that every expression can be safely evaluated in every situation. Examples include null-pointer dereference, dangling-pointer dereference, array out-of-bounds access, and division by zero. QCP checks C programs to ensure that these cases do not occur.

QCP performs these checks during symbolic execution. Some errors directly prevent symbolic execution from continuing. For example, for the assignment t = * px, if QCP cannot find a matching store predicate in the current assertion, then it cannot describe the program state after the statement. If a C expression contains a null or dangling pointer dereference, the symbolic executor necessarily fails to find the corresponding store predicate, reports a red error, and stops.

Not every safety issue stops symbolic execution immediately. Consider the following program with division operations.

int arith(int x, int y)
/*@ Require 0 < x && x <= 100 && 0 < y && y <= 100 
    Ensure __return == x + y */
{
  int t;
  t = 1000 / x;
  t = 10001 / (1001 - t * x);
  y = x + y - t;
  return y + t;
}

Every division must be checked to ensure that its divisor is nonzero. In the first division, the divisor is x; because the Require condition assumes 0 < x, the divisor is clearly nonzero. QCP can automatically prove this simple fact. Even if QCP could not prove it automatically, the rest of symbolic execution could still continue, because QCP can represent the symbolic result of t = 1000 / x:

0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
store_int(&t, 1000 / x_58) *
store_int(&x, x_58) *
store_int(&y, y_55)

Here x_58 and y_55 are the initial values of x and y on entry to the function body. Checking that the divisor is nonzero becomes this VC:

0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
has_permission(&t) *
store_int(&x, x_58) *
store_int(&y, y_55) *
|--
x_58 != 0

In concise assertion notation, this can be written as:

0 < x@pre &&
x@pre <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
t == 1000 / x@pre &&
x == x@pre &&
y == y@pre
|--
x@pre != 0

QCP can automatically prove simple VCs like this, but not every valid VC is automatically solved. For the second division in the program above, safety requires this VC:

0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
store_int(&t, 1000 / x_58) *
store_int(&x, x_58) *
store_int(&y, y_55) *
|--
1001 - (1000 / x_58) * x_58 != 0

This is the second VC generated by QCP. QCP cannot automatically prove it, so it emits a yellow warning, but symbolic execution can still proceed.

The C standard has many detailed rules about arithmetic validity, and some are counterintuitive even to experienced developers. A representative example is that signed integer overflow is undefined behavior. QCP follows the C standard when checking program safety. Therefore, when symbolically executing t = 1001 / (1001 - t * x), QCP actually generates three VCs: one for the division, one for subtraction, and one for multiplication.

0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
store_int(&t, 1000 / x_58) *
store_int(&x, x_58) *
store_int(&y, y_55) *
|--
(10001 != -2147483648 || 1001 - 1000 / x_58 * x_58 != -1) &&
1001 - 1000 / x_58 * x_58 != 0

0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
store_int(&t, 1000 / x_58) *
store_int(&x, x_58) *
store_int(&y, y_55) *
|--
1001 - 1000 / x_58 * x_58 <= 2147483647 &&
-2147483648 <= 1001 - 1000 / x_58 * x_58

0 < x_58 &&
x_58 <= 100 &&
0 < y_55 &&
y_55 <= 100 &&
store_int(&t, 1000 / x_58) *
store_int(&x, x_58) *
store_int(&y, y_55) *
|--
1000 / x_58 * x_58 <= 2147483647 &&
-2147483648 <= 1000 / x_58 * x_58

These VCs state, respectively, that the division, subtraction, and multiplication in t = 1001 / (1001 - t * x) are legal C operations.