As previously introduced, symbolic execution computes the assertion that holds after a program statement executes, based on the assertion that held before it. Symbolic execution is one of the core modules of the QCP tool. Below, we use the swap function to illustrate the symbolic execution results for various program statements in QCP. The following is the swap function and its specification, which were introduced earlier. The QCP tool can automatically verify that the swap function indeed implements the functionality described by its specification.
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;
}
Entering the Function Body
In the C function header, px and py are the formal parameters of the swap function. From the perspective of C program execution, if a piece of code calls the swap function (for example, the statement below), then from outside swap, the call process first evaluates the values of swap's two arguments, then passes these two values to swap for its use, after which swap modifies the program state based on these two values. From this external perspective of the swap function, there is no process of allocating extra memory for the formal parameters px and py. Therefore, in QCP specifications, px and py represent the values of these two formal parameters, rather than C program variables that occupy memory.
Conversely, if we examine the execution process from inside swap, it is easy to see that when program execution enters the swap function body, px and py become local variables, and the system allocates two extra memory locations to store their values. It is worth noting that these two extra memory locations are necessarily independent of the previously allocated memory; the clauses describing them should be connected to the previous clauses with the separating conjunction "*". In other words, after entering the function body, the program state should satisfy the following assertion:
store_ptr(&px, int *, px_37) *
store_ptr(&py, int *, py_40) *
store_int(px_37, int, x) *
store_int(py_40, int, y)
Here, px_37 and py_40 are logical variables automatically introduced by the QCP system. As you can see, they represent the values of the two formal parameters px and py at the time swap is called. In a sense, they correspond to px@pre and py@pre. Therefore, if px@pre and py@pre are used in subsequent assertion annotations within the swap function, or if px and py are used in its Ensure condition, QCP will internally replace them with px_37 and py_40.
Variable Declaration
According to the rules of C program behavior, after the first C statement int t;, the system needs to allocate a new memory location for the variable t, so after symbolic execution, a new separating conjunction clause has_int_permission(&t) is added to the assertion. The symbolic execution result of this statement is:
has_int_permission(&t) *
store_ptr(&px, px_37) *
store_ptr(&py, py_40) *
store_int(px_37, x) *
store_int(py_40, y)
As mentioned earlier, has_int_permission(&t) indicates that the local variable t has an address, but because this variable has not yet been assigned a value, the memory at that address is uninitialized. Currently, you can only write a new value to that address but cannot read a value from it.
Computation and Assignment
The next statement in the swap function is t = * px;. The symbolic execution module of QCP first performs symbolic computation of the expression on the right-hand side of this statement. To compute the value of * px, two steps are needed:
- Read the value of
pxfrom the address&px; - Read the value of
* pxfrom the addresspx.
From the previous assertion, we know that the value of px is px_37 (because of store_ptr(&px, px_37)), and further, the value of * px is x (because of store_int(px_37, x)).
At the same time, the symbolic execution module of QCP computes the address corresponding to the lvalue expression on the left-hand side of the statement. This is straightforward: the address to write to is &x.
At this point, the QCP tool searches for a has_permission or store predicate about &t in the previous assertion and modifies this clause to obtain the new assertion. Here, the clause found by the QCP symbolic execution module is has_permission(&t), and after symbolically executing the assignment statement, it becomes store_int(&t, x). Therefore, the assertion obtained from symbolically executing t = * px; is:
store_int(&t, x) *
store_ptr(&px, px_37) *
store_ptr(&py, py_40) *
store_int(px_37, x) *
store_int(py_40, y)
Why is this transformation valid? The key lies in the fact that all five clauses are connected by the separating conjunction (i.e., the star "*"). Therefore, modifying the value at one address does not affect the data stored at other addresses, and the other clauses of the assertion remain unaffected.
After the above transformation, symbolically executing * px = * py; and * py = t; in sequence yields the following two assertions respectively:
store_int(&t, x) *
store_ptr(&px, px_37) *
store_ptr(&py, py_40) *
store_int(px_37, y) *
store_int(py_40, y)
store_int(&t, x) *
store_ptr(&px, px_37) *
store_ptr(&py, py_40) *
store_int(px_37, y) *
store_int(py_40, x)
When QCP symbolically executes an assignment statement, the symbolic execution may fail. The most typical case is when reading from or writing to a memory address and no memory permission represented by a store or has_permission predicate can be found. Such symbolic execution failures directly cause verification failure, and QCP displays a red error message. During symbolic execution, some complex situations in expression evaluation need to be handled: sometimes it is necessary to prove that an operation does not exceed the range of signed integers, and sometimes it is necessary to prove that a divisor is not zero. If QCP cannot automatically complete these proofs, it issues a yellow warning, although this does not cause symbolic execution to fail or abort.
Leaving the Function Body
When leaving the function body, the memory occupied by the three program variables px, py, and t must first be released. The QCP symbolic executor removes the relevant store predicates or has_permission predicates from the assertion (if they cannot be found, QCP reports an error), yielding the following assertion:
store_int(px_37, y) *
store_int(py_40, x)
Finally, QCP checks whether the above assertion can entail the Ensure condition. This is the Ensure condition:
store_int(px, y) * store_int(py, x)
As mentioned earlier, px and py in the Ensure condition are internally replaced by px_37 and py_40 within QCP, because the Ensure condition is part of the program specification and its px and py refer to the values of the swap formal parameters. Therefore, the conclusion QCP needs to verify here is:
store_int(px_37, y) *
store_int(py_40, x)
|--
store_int(px_37, y) *
store_int(py_40, x)
This obviously holds. With this, QCP completes the verification of the swap function.
Errors and Warnings in Symbolic Execution
If we modify the previous swap program as shown below so that it attempts to read the value of an uninitialized variable, QCP's symbolic execution will report an error and exit.
void swap_wrong(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 t1, t2;
t2 = t1;
t1 = * px;
t2 = * py;
* px = t2;
* py = t1;
}
The error screen is shown below:
In the following example, the program contains a division, but it cannot be automatically inferred that the divisor is not zero. In this case, symbolic execution will issue a warning.
int arith(int x, int y)
/*@ Require 0 <= x && x <= 100 && 0 <= y && y <= 100
Ensure __return == x + y */
{
int t;
t = 1000 / x;
y = x + y - t;
return y + t;
}
The warning screen is shown below:
Yellow warnings differ from red errors: yellow warnings do not affect subsequent symbolic execution. In the figure above, QCP still generates new assertions through symbolic execution and displays them in the right panel.