Bug #330

Coverage check is flawed for lattice-based regions!

Added by Pavel Shved about 7 years ago. Updated about 6 years ago.

Status:ClosedStart date:08/03/2010
Priority:UrgentDue date:12/02/2010
Assignee:Vadim Mutilin% Done:

0%

Category:-
Target version:2.6
Detected in build:pre-ldv Published in build:5712bcdca3dcb323726f91d2a5d3d080e0a4e93b
Platform:

Description

Currently coverage check is implemented like this.

"Region X is covered if join of all regions in the same location is greater than X"

That is not correct. Assume regions [ a > 1 ; b > 10 ] and [ a > 10 ; b > 1 ]. Join of them will be not less than [ a > 1 ; b > 1 ]. It is greater than region [ a = 5 ; b = 5 ]. So if this region was encountered, it would be considered covered. But this region is not covered by any of the regions above! It is not contained in any of the given regions, while join contains it.

This behavior leads to incorrect analysis. It should be fixed.

latt2.c Magnifier - small example of a driver thta causes bug (591 Bytes) Pavel Shved, 09/21/2010 06:09 pm

latt2.c Magnifier - latt2.c lines shifted (628 Bytes) Vadim Mutilin, 11/11/2010 08:00 pm

stateful.c Magnifier - example which should be unsafe with lattice (927 Bytes) Vadim Mutilin, 12/08/2010 07:50 pm

total.jpg - total (98.4 KB) Vadim Mutilin, 12/10/2010 12:15 pm

cmp_default_with_merge_at_bdd.jpg - cmp_default_with_merge_at_bdd (147 KB) Vadim Mutilin, 12/10/2010 12:15 pm

def_with_bdd_on_2gb_34.png (20.9 KB) Vadim Mutilin, 12/16/2010 07:36 pm

default_with_bdd_on_1gb.png (17.7 KB) Vadim Mutilin, 12/16/2010 07:36 pm

def_1gb_with_def_2gb.png (17 KB) Vadim Mutilin, 12/16/2010 07:36 pm

bdd_1gb_with_bdd_2gb.png (17.6 KB) Vadim Mutilin, 12/16/2010 07:36 pm

def_with_bdd_on_2gb.png (17.7 KB) Vadim Mutilin, 12/16/2010 07:36 pm

def_1gb_with_bdd_2gb.png (20.5 KB) Vadim Mutilin, 12/16/2010 07:36 pm

kernel_times.png - kernel times (106 KB) Vadim Mutilin, 12/21/2010 12:01 pm


Related issues

Related to Linux Driver Verification - Bug #335: BLAST doesn't see the error in drivers/net/irda/ali-ircc.c Closed 08/03/2010
Blocks Linux Driver Verification - Bug #405: Unsafe drivers reported as safe on kb0032 Open 08/30/2010

History

#1 Updated by Pavel Shved about 7 years ago

  • Priority changed from Low to Normal

Rising priority to "Normal" after the discussion that took place today.

#2 Updated by Pavel Shved about 7 years ago

  • Priority changed from Normal to High

#3 Updated by Pavel Shved about 7 years ago

  • Priority changed from High to Urgent

To be done this sprint

#4 Updated by Pavel Shved about 7 years ago

Here's a very simple example of this bug.

Try the attached file latt2.c.

pblast.opt -predH 7 -craig 2 -cldepth 0 -alias "" -cref -devdebug latt2.c
pblast.opt -predH 7 -craig 2 -cldepth 0 -alias "" -cref -devdebug -lattice -include-lattice symb latt2.c

The first will be unsafe, the second—safe. However, the driver is unsafe. If you look at the output of the latter command, you'll notice near the end:

Next iteration of model-check's big while-loop
53
Now processing tree node:
TreeNode(label=Data(id=53; mark=Unprocessed);
         incoming_op=Location: id=1#39 (Artificial)---Skip--->Location: id=1#8
                                                              src="latt2.c"; line=38;
         parent_id=52; children_ids=[])
No error found at this node
This node is covered

This is the bug: the node isn't covered actually.

#5 Updated by Pavel Shved almost 7 years ago

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.

#6 Updated by Pavel Shved almost 7 years ago

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.

#7 Updated by Pavel Shved almost 7 years ago

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).

#8 Updated by Vadim Mutilin almost 7 years ago

#9 Updated by Vadim Mutilin almost 7 years ago

Remarks
  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
bfs search on latt2.c with symb lattice
  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

#10 Updated by Vadim Mutilin almost 7 years ago

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.

#11 Updated by Pavel Shved almost 7 years ago

Вадим Мутилин 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?

#12 Updated by Vadim Mutilin almost 7 years ago

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.

#13 Updated by Vadim Mutilin almost 7 years ago

Looking at the code I think reached Unoin is stored in

!reached_region

variable.

#14 Updated by Vadim Mutilin almost 7 years ago

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

#15 Updated by Vadim Mutilin almost 7 years ago

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

#16 Updated by Pavel Shved almost 7 years ago

  • Due date set to 12/02/2010

Alright, so we're going to fix it as in Example A.

We need to fix the region type (and fix a lot of code that creates new regions) and implement region cup and leq functions.

#17 Updated by Vadim Mutilin almost 7 years ago

NoNewPredicates was caused by mistake in my merge function. I used leq for checking equivalence of bdd :) which is obviously wrong. I debugged it on the example stateful.c attached.
pblast.opt -stop-sep -merge bdd -predH 7 -craig 2 -cldepth 0 -smt -lattice -include-lattice symb stateful.c

#18 Updated by Vadim Mutilin almost 7 years ago

Results of prev runs are in ftp://shved/upload/lattice_fix_1
description of runs
  • 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

#19 Updated by Vadim Mutilin almost 7 years ago

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

#20 Updated by Vadim Mutilin almost 7 years ago

total

  • Merge at location - too many NoNewPredicates (20) and rather big total time 8 063,72
  • No merge - too many time 40 944,48 (like without lattice) and many outofmemory(37) and timelimits(18)
  • Merge at bdd:
    • Total time is not big 3 896,50 in comparison with default(2 721,03) and small in comparison with no lattice(40 180,22)
    • 20 new correct usafes which was previously safe. Actually, they should be unsafes in current input to the BLAST. The bugs #616, #617 in input preparation discovered.
    • 2 correct unknown->safe
    • Not much(3) safe->unknown, actually they should be unsafes and previous verdicts(safe) are wrong

Comparision of "shved, default" with "joker, merge at bdd fixed"

cmp_default_with_merge_at_bdd

#21 Updated by Vadim Mutilin almost 7 years ago

Comparison results of default (old lattice with error) and bdd (fixed stopsep lattice with merge at equiv bdds) on linux kernels

Comparing default and bdd on 2.6.31.6 with 1gb memory limit:
we have one new unsafe, six new safes, and six previously safe (possibly incorrect due to bug in lattice) which became unknown. The good news is that we didn't lose any unsafe.

Trying to extend memory limit to 2gb leads to the improvement on both default and bdd. The improvement is very similar.

Default finds 1 new unsafe and proves 43 safes.

Bdd finds 2 new unsafes and proves 39 safes.

So on 2gb the difference of bdd and default is similar to the difference on 1gb.

But if we compare default on 1gb with bdd on 2 gb we will see much difference :)

On linux 2.6.34 with 2gb bdd finds about two times more unsafes (12/7) and does not lose any unsafe found by default.

For generic test set increasing memory limit didn't give any substansial improvement.
For default we have +2 safes. For bdd we have +1 unsafe, +1 safe, and lose 2 old unsafe (degradation!). The cause of degradation may be different machines running the tests (shved and joker).

#22 Updated by Vadim Mutilin almost 7 years ago

  • Status changed from Open to Resolved
  • Assignee deleted (Pavel Shved)
  • Published in build set to 5712bcdca3dcb323726f91d2a5d3d080e0a4e93b

Fixed in 5712bcdca3dcb323726f91d2a5d3d080e0a4e93b

#23 Updated by Vadim Mutilin almost 7 years ago

kernel times:
  • joker, with 1Gb on 2.6.31.6: bdd 37 112 / default 37 165
  • shved, with 2gb on 2.6.31.6: bdd 54 313 / default 53 893
  • valdus, with 2gb on 2.6.34: bdd 112 196 / default 116 600

kernel times

#24 Updated by Pavel Shved over 6 years ago

  • Status changed from Resolved to Closed

Since we didn't have any issues with this (aside from the anticipated 1.5x runtime increase), I'm closing this.

#25 Updated by Pavel Shved over 6 years ago

  • Assignee set to Vadim Mutilin

it was you!

#26 Updated by Pavel Shved about 6 years ago

  • Project changed from Linux Driver Verification to BLAST
  • Category deleted (BLAST)

#27 Updated by Pavel Shved about 6 years ago

  • Target version set to 2.6

Also available in: Atom PDF