QCP Tutorials Symbolic Execution

int abs0(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
    Ensure __return >= 0 */
{
  if (x < 0) {
    return - x;
  }
  else {
    return x;
  }
}

int abs1(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
    Ensure __return >= 0 */
{
  if (x < 0) {
    x = - x;
  }
  return x;
}

int abs2(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
    Ensure __return >= 0 */
{
  if (x > 0) {
    return x;
  }
  return - x;
}

Symbolic Execution of abs0

For abs0, symbolic execution starts by entering the function body. The initial assertion is:

INT_MIN < x_30 &&
x_30 <= INT_MAX &&
store_int(&x, x_30)

If x changes later, x_30 can be viewed as x@pre. If x has not changed, x_30 is both the initial value and the current value of x.

Symbolic Execution of the if Statement

The next statement to symbolically execute is the if statement with condition x < 0. QCP determines that the condition is true when x_30 < 0 and false when x_30 >= 0. Therefore it generates one assertion for each branch. The if-true branch obtains:

x_30 < 0 &&
INT_MIN < x_30 &&
x_30 <= INT_MAX &&
store_int(&x, x_30)

The if-false branch, namely the else branch, obtains:

x_30 >= 0 &&
INT_MIN < x_30 &&
x_30 <= INT_MAX &&
store_int(&x, x_30)

When the cursor is at the beginning of the if-true branch in the IDE, pressing Ctrl+Right shows the current symbolic execution result:

Symbolic Execution of return

In the if-true branch, abs0 returns - x. The value of this expression is - x_30. QCP symbolically executes this return statement in two steps. First it computes the value to be returned:

x_30 < 0 &&
INT_MIN < x_30 &&
x_30 <= INT_MAX &&
__return == - x_30 &&
store_int(&x, x_30)

Then it releases the memory occupied by local variables, including formal parameters:

x_30 < 0 &&
INT_MIN < x_30 &&
x_30 <= INT_MAX &&
__return == - x_30

Since x_30 is the initial value of the formal parameter x, this return assertion can also be written as:

x@pre < 0 &&
INT_MIN < x@pre &&
x@pre <= INT_MAX &&
__return == - x@pre

In IDE feedback, this assertion is listed under Return rather than Normal. This means that execution is about to leave the function body in a state satisfying this assertion, rather than continuing after the current cursor position.

Entering the if-false Branch

When the cursor is at the beginning of the if-false branch, the IDE shows the Normal assertion for the current branch and the Return assertion already produced by the earlier branch.

The current branch assertion can be written in basic separation-logic notation and concise notation as:

x_30 >= 0 &&
INT_MIN < x_30 &&
x_30 <= INT_MAX &&
store_int(&x, x_30)

x@pre >= 0 &&
INT_MIN < x@pre &&
x@pre <= INT_MAX &&
x == x@pre

Symbolically executing return x from this state yields another Return assertion:

x@pre >= 0 &&
INT_MIN < x@pre &&
x@pre <= INT_MAX &&
__return == x@pre

The IDE then displays the two collected Return assertions together.

Why the Function Body Is Verified by Combining Branches

The two branches of abs0 produce two return assertions:

x@pre < 0 &&
INT_MIN < x@pre &&
x@pre <= INT_MAX &&
__return == - x@pre

x@pre >= 0 &&
INT_MIN < x@pre &&
x@pre <= INT_MAX &&
__return == x@pre

To verify the Ensure condition __return >= 0, QCP checks that each branch's return assertion implies the postcondition. The first branch relies on INT_MIN < x@pre to ensure that -x@pre is a valid signed integer and is nonnegative. The second branch directly has x@pre >= 0.

Symbolic Execution of abs1

The function abs1 does not return inside the if statement. Instead, it modifies x in the true branch and then returns after the if.

int abs1(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
    Ensure __return >= 0 */
{
  if (x < 0) {
    x = - x;
  }
  return x;
}

After symbolically executing the true branch assignment, QCP obtains a Normal assertion describing the state where x has become -x@pre.

After the false branch, QCP obtains a Normal assertion describing the state where x remains x@pre.

After the whole if statement, the two Normal assertions are collected as possible states before the final return.

Symbolically executing the final return x converts these normal states into return states, and QCP checks each of them against the Ensure condition.

Symbolic Execution of abs2

The function abs2 has one explicit return inside the if statement and another return after the if.

int abs2(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
    Ensure __return >= 0 */
{
  if (x > 0) {
    return x;
  }
  return - x;
}

When the condition x > 0 is true, symbolic execution produces a Return assertion for return x.

When the condition is false, symbolic execution continues after the if statement with a Normal assertion for the state x@pre <= 0.

The final return - x then produces another Return assertion.

At the end of the function body, QCP collects all return paths and checks that every one of them implies the postcondition.

This is the general pattern for symbolic execution with branches and control flow: Normal assertions describe states that continue executing, while Return, Break, and Continue assertions describe states that leave the current control-flow context.