The following three C functions are all potential implementations of computing the absolute value. Here we merely illustrate the verification of a simple property: if the argument passed to them is not INT_MIN, then they can execute safely, and their return value is non-negative.
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 if Statements
Taking the symbolic execution of the abs0 function as an example, its symbolic execution starts from "entering the function body." The assertion generated by this initial step is:
INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, x_30)
If the value of x changes later, then x_30 can be regarded as x@pre. If the value of x has not yet changed, then x_30 is both the initial value and the current value of x.
Next, the if statement is to be symbolically executed. The condition of this statement is the expression x < 0. The symbolic execution module of QCP determines that when x_30 < 0, this condition is true, and when x_30 >= 0, this condition is false. Therefore, the symbolic executor generates one assertion for each of the two branches of the if statement. The if-true branch yields the assertion:
x_30 < 0 && INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, x_30)
while the if-false branch (i.e., the else branch) yields the assertion:
x_30 >= 0 && INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, x_30)
In the IDE, when the cursor is placed at the beginning of the if-true branch, pressing the Ctrl+Right shortcut key shows the symbolic execution result for the current branch:
Symbolic Execution of return Statements
In the if-true branch, the abs function returns - x. The value of this C expression - x is - x_30. The symbolic execution module of QCP completes the symbolic execution of this return statement in two steps. First, it symbolically 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)
Second, 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 represents 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
It is worth noting that when the IDE provides feedback, the right panel lists this assertion as a Return assertion, rather than the Normal assertion we have seen previously. This means that the function body execution is about to exit in a program state satisfying this assertion, rather than continuing execution of the program after the current cursor position.
Symbolic Execution Entering the if-false Branch
In the IDE, when the cursor is placed at the beginning of the if-false branch, pressing the Ctrl+Right shortcut key shows the symbolic execution result for the current branch:
At this point, the IDE simultaneously displays the Normal assertion for the current branch and the Return assertion from the previous branch. As mentioned earlier, the Normal assertion for the current branch can be expressed using basic separation logic assertions and concise separation logic assertions respectively 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 the return x statement on this basis yields:
x@pre >= 0 && INT_MIN < x@pre && x@pre <= INT_MAX && _return == x@pre
This is also a Return assertion. The IDE then collects and displays both Return assertions together.
After the if Statement Ends
In the abs0 function, both branches of the if statement are return statements, so the program would never execute past the if statement (and indeed, there are no other statements after this if statement). Accordingly, if you view the symbolic execution result after the if statement ends, it contains only two Return assertions and no Normal assertion.
Conditions Checked When Exiting the Function Body
When exiting the function body, QCP checks whether all Return assertions can entail the Ensure condition. For abs0, the following two properties need to be proved:
x_30 < 0 && INT_MIN < x_30 && x_30 <= INT_MAX && __return == - x_30 |-- __return >= 0
x_30 >= 0 && INT_MIN < x_30 && x_30 <= INT_MAX && __return == x_30 |-- __return >= 0
QCP confirms that both of these mathematical derivations indeed hold. With this, QCP completes the verification of the abs0 function.
Symbolic Execution of the abs1 Function
The abs1 function differs slightly from abs0. Its if statement has only one branch, and it contains only an ordinary assignment statement without a return statement.
int abs1(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
Ensure __return >= 0 */
{
if (x < 0) {
x = - x;
}
return x;
}
When QCP's symbolic execution reaches the end of the if-true branch, the result is a Normal assertion, rather than the Return assertion we saw in abs0. It can be expressed using basic separation logic assertions and concise separation logic assertions respectively as follows (where x_30, as before, corresponds to x@pre):
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
In the tool, the following feedback is displayed:
After the if statement ends, QCP's symbolic execution collects the two Normal assertions (including the implicit if-false branch assertion). Written using basic separation logic assertions:
x_30 < 0 && INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, - x_30)
x_30 >= 0 && INT_MIN < x_30 && x_30 <= INT_MAX && store_int(&x, x_30)
Written using concise separation logic assertions:
x@pre < 0 && INT_MIN < x@pre && x@pre <= INT_MAX && x == - x@pre
x@pre >= 0 && INT_MIN < x@pre && x@pre <= INT_MAX && x == x@pre
Of course, if you want the IDE to display these symbolic execution results in the tool, there is a minor complication. The reason is that the if statement of abs1 has no else branch, but when the cursor is at the end of the if-true branch, the tool does not know whether there will be a subsequent else branch. Therefore, the QCP tool will only display the end condition of the if-true branch at that point.
To have the tool display the symbolic execution results of both branches simultaneously (equivalent to the symbolic execution result of the entire if statement), you can manually add an empty else branch.
Of course, regardless of whether this empty else branch is written out, QCP will continue subsequent reasoning based on the combined results of both branches. For the abs1 function, when QCP derives the symbolic execution result of return x, it produces two Return assertions based on the two preceding Normal assertions.
Naturally, both Return assertions can entail the Ensure condition, and with this QCP also completes the verification of abs1.
Symbolic Execution of the abs2 Function
The abs2 function differs from the previous two functions.
int abs2(int x)
/*@ Require INT_MIN < x && x <= INT_MAX
Ensure __return >= 0 */
{
if (x > 0) {
return x;
}
return - x;
}
Its if-true branch is a return statement, and its symbolic execution produces a Return assertion. It has no if-false branch, which is equivalent to that branch being empty, producing a Normal assertion. To view the symbolic execution result of the entire if statement in the tool, you need to manually add an empty else branch as before.
Of these two assertions, only the Normal assertion is subject to symbolic execution of subsequent statements. Finally, the symbolic execution result after return - x is as follows:
