Bug #2287
opencdc_eem.ko had correct unsafe verdict and became unknown in BLAST 2.7.1
0%
Description
Night tests result.
linux-2.6.31.6 68_1 drivers/kbdrivers/0068-2.6.31.6/test-0068-2.6.31.6-verdict-unsafe-drivers--net--usb--cdc_eem.c/cdc_eem.ko ldv_main0_sequence_infinite_withcheck_stateful
Was correct BLAST verdict. Became NoNewPredicates
Files
Updated by Pavel Shved almost 13 years ago
I can't reproduce the original unsafe you refer to. I tried 533acf that was used in ldv tools, but it shows that there's no new predicates either. Here's the command line I used:
pblast.opt bug2287/cdc_eem.i -main ldv_main0_sequence_infinite_withcheck_stateful -L LDV_ERROR -lattice -include-lattice symb
where cdc_eem.i is the *.i file extracted from the archive. I still can't make ldv-tools work due to some bugs with ruby gem handling, so could you verify the options please? Or, at least, provide the correct error trace?
Updated by Pavel Shved almost 13 years ago
Hm, after I turned aliases off (which should be done for older BLASTs), it started showing FociInterface.SAT at iteration 3860 (that was integer <-> real arithmetics problem). I used the correct command line this time.
pblast.opt bug2287/cdc_eem.i -alias "" -cldepth 0 -predH 7 -craig 2 -ignoredupfn -nosserr -enable-recursion -main ldv_main0_sequence_infinite_withcheck_stateful -L LDV_ERROR -lattice -include-lattice symb
But that unsafe was a "bad" one :-) To reproduce it with the latest one, turn off the "incremental closure" by supplying -no-iclos options. So, this yields "unsafe" even with blast 2.7.1:
pblast.opt bug2287/cdc_eem.i -alias "" -cldepth 0 -no-iclos -main ldv_main0_sequence_infinite_withcheck_stateful -L LDV_ERROR -lattice -include-lattice symb
Anyway, this is the trace that makes BLAST into a loop it's stuck in:
Conflicting Blocks [INF0] 35 : 205: Pred(header@eem_rx_fixup & 1 << 15 != 0) [INF0] 81 : 196: FunctionCall(header@eem_rx_fixup = get_unaligned_le16(p@get_unaligned_le16 = (* (skb@eem_rx_fixup)).data,)) [INF0] 82 : 9: FunctionCall(tmp@get_unaligned_le16 = __le16_to_cpup(p@__le16_to_cpup = p@get_unaligned_le16,)) [INF0] 83 : 65: Block(__retres2@__le16_to_cpup = * (p@__le16_to_cpup );) [INF0] 84 : 63: Block(Return(__retres2@__le16_to_cpup);) [INF0] 86 : 9: Block(Return(tmp@get_unaligned_le16);) [INF0] 90 : 205: Pred(header@eem_rx_fixup & 1 << 15 == 0)
It uses bit masks, which is not checkable by BLAST sometimes. I can see that the predicate is not "turned on" at forward exploration after the very first block here.
So the reason why it now throws NoNewPredicates exception is that better "closure" algorithms lure BLAST into the different path, where it stucks.
P.S. By the way, you should turn aliases on with BLAST 2.7.1.
Updated by Pavel Shved almost 13 years ago
I took a closer look and found out why this block set is not proven by blast. See bug #2307 for details.
Still, this is only one bug, there may be more in this file.
This should be easy to fix, but I'm too tired today.
Updated by Vadim Mutilin almost 13 years ago
P.S. By the way, you should turn aliases on with BLAST 2.7.1.
You can see options passed to BLAST 2.7.1 in the log
/all/qaserver-work/nighttests/inst/2012-01-25-00-00-02/bin/../dscv/rcv/backends/blast/bin/pblast.opt /all/qaserver-work/nighttests/work/2012-01-25-00-00-02/launcher-working-dir/ldv-manager-work-dir/work/current--X--kbdrivers--0068-2.6.31.6--test-0068-2.6.31.6-verdict-unsafe-drivers--net--usb--cdc_eem.c.tar.bz2--X--2012-01-25-00-00-02linux-2.6.31.6--X--68_1/linux-2.6.31.6/csd_deg_dscv/2/dscv_tempdir/dscv/rcv/68_1/main-ldv_main0_sequence_infinite_withcheck_stateful/preprocess/1-cpp/drivers-kbdrivers-0068-2.6.31.6-test-0068-2.6.31.6-verdict-unsafe-drivers--net--usb--cdc_eem.c-cdc_eem.c.common.i -predH 7 -craig 2 -ignoredupfn -nosserr -enable-recursion -main ldv_main0_sequence_infinite_withcheck_stateful -L LDV_ERROR -cldepth 0 -alias -lattice -include-lattice symb -stop-sep -merge bdd
Do we need to change something?
Updated by Pavel Shved almost 13 years ago
Vadim Mutilin wrote:
[...]
You can see options passed to BLAST 2.7.1 in the log
[...]
Do we need to change something?
Yes. Some of the options you specified are default or ineffective now, so the command line above may be shortened to this:
pblast.opt -ignoredupfn -nosserr -enable-recursion -main ... -L ... -lattice -include-lattice symb -alias ""
I would also add -cref -alias bdd instead of -alias "". There's an if statement in blast frontend that controls it. It does very little harm as alias analyzer is still very incomplete, but may help (or introduce some bugs like this one :-)).
Updated by Pavel Shved almost 13 years ago
- Status changed from New to Open
- Assignee set to Pavel Shved
The updated BLAST (after fixing #2307) says that the driver is safe. The "unsafe" trace, obtained with -no-iclos contains a subtrace shown in the comment #3, which means that the trace is actually not feasible. Exploring the driver further, BLAST fails to find the good trace.
Is it a real error at all?
Updated by Vadim Mutilin almost 13 years ago
Why the trace is infeasible?
I didn't find the loop in eem_rx_fixup with condition
header@eem_rx_fixup & 1 << 15 == 0
or similar.
Updated by Pavel Shved almost 13 years ago
Vadim Mutilin wrote:
I didn't find the loop in eem_rx_fixup with condition
[...]
or similar.
This condition is in the middle of the do...while loop, which is nearly as large as the eem_rx_fixup function itself (lines 35483-35618 of the .i file).
Updated by Vadim Mutilin almost 13 years ago
That loop may be exited in several ways and they seem to be feasible
1. skb->len < 2
2. skb->len < len
3. is_last
4. skb->len == 0
Updated by Vadim Mutilin almost 13 years ago
After calling eem_linkcmd (where URB is alloced but not freed) BLAST can not go out of the do-while loop.
It happens because the loop exit conditions do not change:
1. skb->len is changed in skb_pull which is kernel core function with undefined body.
2. BLAST can not go to is_last check because it is located on the else branch of the if statement which also does not change (header & (1UL << (15))) as far as changes of header == skb->data is not visible.