The Xr0 Blog

Jan 27, 2024 · Xr0 Team

#11: One Last thing?

We achieved our goal (#24) from last week of verifying the case where the value of one of the returned fields of a returned structure determines whether or not an allocation will take place.

We now have one function left to verify in parse.x, main. The challenge we’ve run into with it is evaluating all the scenarios that can occur due to the complexity of parse’s abstract¹. Xr0 handles selection statements by generating all the possible execution paths given a function’s abstract and body. For example, from

void *
foo(int x)
{
    if (x) {
        return malloc(1);
    }
    return NULL;
} 

it identifies two paths corresponding to whether the body of the if-statement is entered. The problem is that until now this “splitting” process has been entirely syntactical, because this allowed us to generate all the possible paths through a function at the beginning of our verification procedure.

With the way that main calls parse, however, we have to account for the possibilities that come from the various selection statements in parse’s abstract. This can plainly no longer be syntactical only, because at the very least we have to move from the call

l = parse(file);

to a consideration of parse’s abstract. We have therefore been reworking the “splitting” process, integrating it into the verification procedure. In the new approach we’ve taken the various paths are generated whenever we encounter a line of code that is splitting, such as a selection statement but also any calls of functions with selection statements in their abstracts.

We will explain this in more detail soon, but for now it’s back to building.

Next up §

Our goal for this week (to 3rd) is getting the new splitting procedure to work and establishing whether or not it will help us verify main [#25].

Stretch goal: - Simplify map and array data structures [#13].

Subscribe via email.