Linux Driver Verification » BLAST

The issue with the coverage is not what we described it to be.

Assume three paths converge in one point. The first comes with [a = 10; b=1] lattice, the second—with [a=10; b=2] lattice, the third—with [a=10; b=3] lattice. When the algorithm iterates into the node, it updates the lattice region by joining the one being posted and the one already in the node, and it continues the traversal with the lattice region set to the result of the join.

As a result, when iteration reach the convergence point with the 2nd lattice, the joined result is [a=10]. Thought imprecisely, this reguon is a superset of the set of possible values. But after the 3rd path posts its lattice to the same region, it becomes [a=10; b=3], because in [a=10] region there is no information that we knew something about b.

A solution would be to make the region look as [a=10; b=⊤] after joining 1st and 2nd paths, which is really the result one could expect. Then, when the third path joins, the region would still look like [a=10; b=⊤], and this would be correct. The thing is in BLAST's lattice implementation, such "tops" are explicitly withdrawn; perhaps, for performance reasons.

I also suppressed reasoning about coverage based on lattice regions. Assume that you came to the convergence point along these three paths. Then, at the node after the convergence point, the 2nd and the 3rd paths would have the same lattice regions, and one node would cover the other. This will result in a cutting of the whole program path, along which there may be an error. Lattice coverage is inherently imprecise, and that's an unimprovable property of lattice checkers.

So, I suppressed lattice-based coverage checking and the explicit withdrawal of tops, and ran generic tests.

I observed a drastic performance degradation. Instead of completing tests in one night, they had been working for 3.5 days when I stopped them. Indeed, a significant amount of drivers timed out (and the funny thing is that the most timeouts were BLAST's native, not imposed by the timeout script). However, in those drivers, whose checking finished, there was a precision improvement.

More work on this issue is required.

It didn't work either.

It happened that I turned off the whole coverage procedure, not just its lattice part. Hence the results: an enormous runtime and never-ending checking for programs with loops :-)

But even before I fixed it, I understood that turning off lattice's coverage checks doesn't help either. Assume the following program:

  if (nondet()){
    //L1
    a = 1;
  }else{
    //L2
    call();
    some();
    useless();
    functions();
  }
  // L3
  if (a==2) error();

The error would be missed, since the checker would first find L1-L3 path, and at the location L3 the lattice would be [a=1]. This wouldn't allow checker to find an error, since the error path would be cut.

When the checker then traverse along L2-L3 path, at L3 location, the non-lattice regions is covered by the first node at L3 (both regions are sets of all possible variables). This would lead to missing the error.

The attempt to fix this bug is located in the lattice-top-cover-fix in the BLAST local repository.

Middle regression tests run faster, but the errors found are completely random (most drivers are verified less correct than the original BLAST does, but some drivers are more correct).

1. On the theory described in the paper Configurable software verification
   1. There is no proof but the theorem looks sound
   2. It does not describe refinement phase and lazy model checking case
2. On CPAchecker implementation
   1. All algorithms including locations, callstack, ART, predicates, refinement are implemented as lattices very close to the theory
   2. There is no SymbolicStore lattice (they say that it is in progress)
3. On SymbolicStore implementation in BLAST
   1. union(join) works correctly on latt2.c example. Absence of element means Top
   2. leq(coverage) works correctly too
4. On configurable model checking in BLAST
   1. I didn't understand what for Region.cap and meet
   2. Description of the missing error is as follows

1. First of all we reach branch with the arc 1#6 -- a=10, b=1 --> 1#8. At 1#8(end of ifs) we have region {bdd=true, lattice=[a=10, b=1]}
2. We goto the location 1#10(after pred a==1) where lattice is bottom, because pred a==1 and [a=1] contradict.
3. Then we reach branch 1#19 -- a=1, b=10 --> 1#8
4. At 1#8(end of ifs) we merge {bdd=true, lattice=[a=1, b=10]} with the previous region and get {bdd=true, lattice=[]}
5. We merge 1#9, 1#15,1#16
6. At 1#12(error call) we reach error with the region {bdd=true, lattice=[]}
7. The path is unreachable and we add predicate b>=10 at 1#19
8. During refinement at 1#8 get new refined region {bdd=[b>=10] lattice=[a=1, b=10]}
9. We merge it with {bdd=true, lattice=[a=10, b=1]} and get {bdd=true, lattice=[]}
10. This region is successfully added to reached Union of regions
11. But to the ART tree BLAST adds the node with the region {{bdd=[b>=10] lattice=[]}. Only lattice parts are merged! It contradicts to the region stored in the reached Union.
12. It reaches error location 1#12 with bdd=false, because pred b==1 contradicts to bdd=[b>=10].
13. Next we reach branch with the arcs 1#20 -- a=1, b=1 --> 1#22 -- ...useless funcs... --> 1#8
14. At 1#8(end of ifs) we have region {bdd=true, lattice=[a=1,b=1]}. It is covered by the region {bdd=true, lattice=[]} stored in reached Union. So this path is not considered anymore and the real error is missed.

• Command line: pblast.opt -predH 7 -craig 2 -cldepth 0 -smt -lattice -include-lattice symb latt2.c -devdebug -tree-dot ART.dot -debug -checktree
• Changes are in lattice_experiments branch

Notes on
11. But to the ART tree BLAST adds the node with the region {{bdd=[b>=10] lattice=[]}. Only lattice parts are merged!
It does not contradicts to theory in general. Because theoretically merge may return any result greater or equal to the merging element $$e_2 \subseteq merge(e_1,e_2), where e_2 is a new merging element$$. In particular it may not merge at all. So the contratiction is that regions stored in the reached Union and in the ART node are different.

Вадим Мутилин wrote:

So the contratiction is that regions stored in the reached Union and in the ART node are different.

I still don't get it...
ART and Union are the same thing in BLAST. Aren't they? Could you describe the contradiction more carefully?

Reached Union (as I call it) is a parameter of Region.leq (abs-region.ml). I don't know where it is stored.
Region.cup changes it. ART node stores different value produced by playing with Region.cap.

Looking at the code I think reached Unoin is stored in

!reached_region

Thanks to Pavel, after discussion I understood the root cause of the bug.
Reached Union (R) In BLAST is used for coverage check. For optimization they store in the R for each location a joined region and consider that some region is covered if it is covered by joined region in R. But this can be done only if regions are powerset domain i.e.
$[[e_1 \sqcup e_2]] = [[e_1]] \cup [[e_2]]$, where [[.]] returns a set of concrete states. For the regions with lattices it is not true, because join may introduce addtional concrete states.

In the paper Dirk et.al. presents two coverage checks
General case: $stop^{sep}(e,R) = (\exists e' \in R : e \sqsubseteq e')$ -- checks that there are exists element e' in R which covers e.
Powerset domain case: $stop^{join}(e,R) = (e \ sqsubseteq \sqcup_{e'\in R} e')$ -- checks that the join of elements in R covers e

After discussion we work out two solutions:

1. A
   • fix coverage to check stop^{sep}, i.e. check that one of the regions cover the given one, without joining reached region R
   • use one of three options for merge
     1. merge bdd and lattice at equal locations
     2. merge lattice at equal locations and bdds
     3. don't merge
2. B
   • join lattice part at equal locations
   • apply the resulting lattice to all regions with the same location
   • rebuild subtrees of changes regions

• shved-default
• shved-no BLAST_OPTIONS="-stop-sep -merge no"
• joker-bdd BLAST_OPTIONS="-stop-sep -merge bdd"
• valdus-lattice BLAST_OPTIONS="-stop-sep -merge location"
• misha_bear-expnolattice BLAST_EXP_NOLATTICE=1

commit 29cecb7a8194f21497a21951b40a6cb1ee3b44f9 contains fix of NoNewPredicatesExcption in cpa merge with stop-sep