Linux Driver Verification » BLAST

At the Competition on Software Verification 2012, the functions that return a nondetermined value at each call are assumed to have the same behavior as this function:

X __VERIFIER_nondet_X() { X val; return val; }

However, if this definition is actually in the source code, BLAST doesn't think it's undetermined. Instead, it thinks that all invocations of such a function return the same value!

This bug leads to false safes, so it should be fixed. In competition setup we lose 10 points because of this, and could have lost 30 points more if the presence of this definition hadn't made several ssh* tests time out instead of failing with a wrong verdict.

To check for this behavior, I added a test: source:tests/files/nondet_definition.c

How to fix it?¶

According to C standards (as per this StackOverflow answer), a variable inside a function that is uninitialized at declaration gets an undetermined value. However, the function listed above is transformed by CIL to a CFG with one edge with a Return() operation on it. Return operation, by definition, works with Expressions rather than with Lvalues, so it can't be used for updating the Lvalue it returns in our case.

I guess, the proper solution is to update local variable maps at function calls.

And I suddenly recalled that I've already "fixed" something about variable maps at function calls. In bug #1684, there was a functionality that cleared these maps at each function call, but I removed it because it interfered with alias analysis badly.

So, we need to revamp the fix of #1684, and create a consistent approach to local variable mappings that suits both aliases and such cases as in the test linked above. Maybe, we may implement port something from "non-flat" algorithms described in "Abstractions from Proofs"...