Linux Driver Verification » BLAST

Two programs, good_s3.c and bad_s3.c differ only in implementation of undetermined-value pure function: one uses BLAST's internal capability of marking each extern function as such, and the other uses int foo() {int x; return x;}. The results should not differ.

However, the first program, at one of its error traces (namely, the one at 6368), shows the following regions:

Op: 52  :1330 :: 1330:   Skip :: 1332
post-reg: And [,(* (s@ssl3_accept)).state<=8496,(* (s@ssl3_accept)).state==8496,blastFlag@ssl3_accept<=1,true]
Op: 53  :1332 :: 1332:   FunctionCall(ret@ssl3_accept = __VERIFIER_nondet_int()) :: -1
post-reg: And [,(* (s@ssl3_accept)).state<=8496,(* (s@ssl3_accept)).state==8496,blastFlag@ssl3_accept<=1,true]
Op: 54  :-1 :: -1:   Skip :: 1333
post-reg: And [,(* (s@ssl3_accept)).state<=8496,(* (s@ssl3_accept)).state==8496,blastFlag@ssl3_accept<=1,true]

The second, however, loses conditions on s->state at the same point (iter. 4996):

Op: 52  :1330 :: 1330:   Skip :: 1332                     
post-reg: And [,(* (s@ssl3_accept)).state<=8496,(* (s@ssl3_accept)).state==8496,blastFlag@ssl3_accept<=1,true]
Op: 53  :1332 :: 1332:   FunctionCall(ret@ssl3_accept = __VERIFIER_nondet_int()) :: -1
post-reg: blastFlag@ssl3_accept<=1
Op: 54  :5 :: 5:   Block(Return(x@__VERIFIER_nondet_int);) :: -1
post-reg: blastFlag@ssl3_accept<=1
Op: 55  :-1 :: -1:   Skip :: 1333
post-reg: blastFlag@ssl3_accept<=1

This discrepancy makes the subsequent useful-block binary-search algorithm fail.

The reason for this is that, in the first case, at the forward exploration, BLAST should propagate the local predicates from line 1332 to line 1333, as the location at line 1333 doesn't have any predicates assigned. However, in the second case, it doesn't directly jump to 1333, and jumps to the function instead; this function already has some predicates assigned, and that's why the old predicates are not transferred.

This should not be very harmful, as the second trace should be unsatisfiable anyway. The useful-block algorithm considers both preconditions and regions for interpolation. In this case, it nominates the block with the region similar to that of the line 1332 as "useful", the meaningful condition being s->state <= 8496. After the trace analysis, it adds this predicate to the set of "local" predicates of the __VERIFIER_nondet_int function, and correctly considers this error trace spurious.

However, as you noticed, it requires two forward explorations of ART instead of one.

What role do the functions play here? If a function has a body, then it's used in a number of different contexts (let's define context as stack trace), but all these contexts (at the current state of art, and with the default options) share the same set of local predicates. I think it is not right, and "local" predicates should be context-sensitive.

I think this corresponds with the theory in AbstractionsFromProofs2004 paper, but I should check.

Currently, I'm running the larger runs (I'll start with 6 hours time limit, and increase it to 48 if it doesn't work) of bad_s3. If my hypothesis is correct, the run should finish, but require considerably more time.

(I would greatly appreciate your help in running this with time limits of 72 hours, if you have an unoccupied machine. Please, build a release from release-2.7.1 branch).

The options used are competition-like:

pblast.opt -alias bdd -cref -lattice -include-lattice symb -sv-comp -enable-recursion bad_s3.c