#19: Brute force state split generation

Back on the update-horse.

tl;dr

Although we've neglected to write an update for the past two months, Xr0 has been moving. We've implemented brute-force range splitting to handle indexing into constant-size arrays with an index that can take on a range of values, changed the evaluation of the decidability of expressions in our splitting logic to use ranges instead of "props"¹, normalised the setup execution process to use the new stack based execution model and implemented declaration-initialisation of scalar types with constant values.

Details

Brute force range-splitting

The situation we are solving for is that of detecting invalid accesses to a constant size array by an index that can take on a finite range of values.

Consider the code below.

foo(int index) ~ [ setup: index = [0?2]; ]
{
        int arr[2];
        arr[0] = 3;
        arr[index] = 4;
        arr[0] = arr[1]; /* potentially uninitialised */
}

In the abstract of the function foo, the value of index is conditioned to be in the range $[0, 2)$ by the setup statement; this means that Xr0 should statically enforce that callers of foo cannot pass in an index that isn't guaranteed to be within that range.

Moving on to the body of the function. On the first line, we declare arr to be an array of type int with a size of 2. The next line assigns the value of 3 to arr[0], so far so good.

It gets interesting when we reach arr[index] = 2; because index can be one of two possible values at runtime according to the setup. Therefore, there are two scenarios to consider.

1. If index is 1 at runtime, arr[0] will continue to contain 3 from the previous assignment and arr[1] will be assigned 4.

2. If index is 0 at runtime, arr[0] value of 3 gets overwritten with 4. and arr[1] remains uninitialised after the assignment statement runs.

This is the point at which the "brute-force splitting" comes in. When evaluating arr[index] = 4;, Xr0 will generate all possible single values of index and create parallel split states in which index takes on each of them.

This means that when we reach and execute the line arr[0] = arr[1]; for the state in which index is 0, we will detect the uninitialised memory access. This can be seen by the snapshot of the Xr0's internal state before detecting the error.

phase:  ACTUAL

text:
-->     *(arr+0) = *(arr+1);

rconst:
        $0: int:{?}     "index"
        #0: int:{0}     "foo:0"

stack:
        ---------------------------- inter
        0: |1| {0:<rconst:#0>} (int index, π)
        1: |2| {0:<int:{4}>}   (int[2] arr)
        ---------------------------- foo | #0 ∈ {0}

(0db) s
tests/11-bounds-cbvi/121-FAIL-binary-index-split-constant-first.x:6:24: undefined memory access: *(arr+1) has no value (foo | #0 ∈ {0})

Note that we are in a split state in which index (rconst #0) has taken on a value of 0 during the execution of the statement arr[index] = 4;. Therefore value of arr[0] is 4 and there is no value for arr[1]. Xr0 therefore detects this undefined memory access by the following line:

tests/11-bounds-cbvi/121-FAIL-binary-index-split-constant-first.x:6:24: undefined memory access: *(arr+1) has no value (foo | #0 ∈ {0})

Although brute-force splitting is practical for small ranges, it becomes infeasible with larger ranges due to the sheer number of possible states. For example, an int on a 32-bit machine can range from -2,147,483,648 to 2,147,483,647, making it impractical to generate all possible states.

Despite its impracticality for larger ranges, embracing intermediate solutions as a path to progress helps move Xr0's internal structures toward handling the more general cases without having to address all the complexity upfront.

Using ranges instead of props for splitting logic

We initially introduced the concept of "props" (propositions) to facilitate the splitting² of the state when an undecidable condition is encountered in a selection statement. We implemented this concept as an array of expressions (see here) for which the presence of an expression within the array meant that it was true in the particular split of the state i.e. that the first branch of the selection statement would "run".

Detecting out-of-bounds memory accesses is heavily based on being able to reason about ranges; essentially we want to know at compile-time whether the value of an index used to access an array falls within the bounds of said array. It therefore felt reasonable to replace the concept of props in our splitting logic with the concept of ranges which are truer to the semantics of C since the evaluation of expressions in conditions is defined with respect to the whether the value is non-zero (and not its presence in an arbitrary array).

The move to ranges has simplified other areas of the code base. For example, we were able to remove the unwieldy pf_reduce (parameter-form reduce) logic (see here) that was enabling the splitting of the state on more complex conditions in selection statements such as calls with arguments.

Normalised setup execution across phases

For the evaluation of setups we previously followed the old execution model in which we would simply loop through statements and execute them against the state.

Now we've given the setup its own execution phase that extracts the relevant setup statements and pushes them onto the stack, which makes them visible from user space when using the debugger. Most importantly, it means the same machine logic that handles the abstract and actual execution phases can handle the setup one, enabling things like splitting to work seamlessly in setups.

Return values of non-void functions

Previously we had a function called call_to_computed_value (see here) that would — in order to compute an return value rconst³ in the absence of an abstract — first evaluate the arguments of a particular function call and then stringify the results and create and return a new rconst based on this string representation. This was only useful with the old splitting logic.

We have removed this in favour of inspecting the return type of the function to generate a default return value in the absence of an abstract. This default return value for a scalar return type is an rconst with the range of values instances of the type can take on, for example an int would be range of [INT_MIN, INT_MAX). The default return value for a composite type like a struct would be its’ members recursively initialised down to scalar types of the range of values they can take on.

Next up

We are working on implementing the ability to split the state on the evaluation of relational operators. The following is an example of the kinds of functions that we would be able to verify.

bar(int i) ~ [ setup: i = [0?5]; ]
{
        int arr[2];
        if (i < 2) {
                arr[i] = 0;
        }
}

Once this works, we intend to frame our existing logic for the evaluation of equality in terms of this logic for the evaluation of relational operators. The reason for doing so is that by building up these concepts recursively from each other we can maintain logically coherent comparison logic for less than, greater than, and equality.

We hope to be more consistent in posting these updates, so see you soon.