Bug #418
closedSmt Solver error on driver usblp.o.i with double locks model
0%
Description
In development build of BLAST, usblp.o.i
driver has several issues. One of them is a syntax error reported by CVC3. Here's the query that caused it:
SMT solver query: ( benchmark Blast_query_91 :logic AUFLIA :extrafuns ((Address Int Int )) :extrafuns ((BitAnd Int Int Int :assoc :comm)) :extrafuns ((And Int Int Int :assoc :comm)) :extrafuns ((offset Int Int Int )) :extrafuns ((Foffset Int Int Int )) :assumption (forall (?x Int) (?y Int) (?d1 Int) (implies (= (Foffset ?x ?d1) (Foffset ?y ?d1)) (= ?x ?y))) :extrafuns((S16 Int )) :extrafuns((S19 Int )) :extrafuns((S9 Int )) :extrafuns((S11 Int )) :extrafuns((S25 Int )) :extrafuns((S3 Int )) :extrafuns((S27 Int )) :extrafuns((S13 Int )) :extrafuns((S30 Int )) :extrafuns((S2 Int )) :extrafuns((S7 Int )) :extrafuns((S14 Int )) :extrafuns((S31 Int )) :extrafuns((S28 Int )) :extrafuns((S24 Int )) :extrafuns((S12 Int )) :extrafuns((S15 Int )) :extrafuns((S32 Int )) :extrafuns((S6 Int )) :extrafuns((S23 Int )) :extrafuns((S4 Int )) :extrafuns((S5 Int )) :extrafuns((S21 Int )) :extrafuns((S10 Int )) :extrafuns((S29 Int )) :extrafuns((S22 Int )) :extrafuns((S17 Int )) :extrafuns((S26 Int )) :extrafuns((S1 Int )) :extrafuns((S18 Int )) :extrafuns((S8 Int )) :extrafuns((S20 Int )) :formula (and true true true (and true (= S2 (not (not (BitAnd S1 2048)))) (= S4 S3)) true (not (= 512 1)) (not (= 512 2)) (not (= 512 4)) (not (= 512 8)) true true (= S6 S5) true (and true (= S7 S6) (= S8 0) (= S10 (Address S9 )) (= S11 0) (= S12 0) (= S13 0)) true true true (not (= 512 1)) (not (= 512 2)) (not (= 512 4)) (not (= 512 8)) true true (= S14 S5) true (and true (= S15 512) (= S17 (Foffset S14 S16)) (= S18 1)) (not (= S15 1)) (not (= S15 2)) (not (= S15 4)) (not (= S15 8)) (= 0 0) true true (= S20 (Foffset S4 S19)) (= S21 0) (= S23 S22) true (= S23 0) (= S24 0) (= S25 (~ 4)) (= S26 S25) true true (and true (= S27 S2) (= S28 S4)) (= S29 0) (= S30 (~ 19)) (= S31 S30) true (= S32 (Foffset S4 S19)) (= S24 0) true true ) ) block_at hits exceptionFailure("SMT sovler answer is strange: *** Parse Error: stdin:41: syntax error") bs_reset Dumping Abstraction Predicate Dependancy Table Writing out .abs file: usblp.abs Maximum #preds/loc: 0 Average #preds/loc: 0 Done writing .abs file Exception raised :(Failure("SMT sovler answer is strange: *** Parse Error: stdin:41: syntax error") Stopping CSIsat process... CSIsat stopped. Stopping SMT solver process... SMT solver stopped. Ack! The gremlins again!: Failure("SMT sovler answer is strange: *** Parse Error: stdin:41: syntax error") Ack! The gremlins again!: Failure("SMT sovler answer is strange: *** Parse Error: stdin:41: syntax error") Fatal error: exception Failure("SMT sovler answer is strange: *** Parse Error: stdin:41: syntax error")
Something should be fixed, I guess... The file is attached. Blast was run with:
pblast.opt -predH 7 -craig 2 -ignoredupfn -nosserr -main ldv_main0 -L LDV_ERROR -cldepth 0 -alias "" -cref -const -smt -noinitialize -bddprint 2>&1 -nomusts -devdebug 2>&1 usblp.o.i
Files
Updated by Vadim Mutilin about 14 years ago
Also appeares in drivers of general test set (default env model plain_sorted_withcheck):
kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--usb--class--usblp.c.tar.bz2
kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--watchdog--pcwd_usb.c.tar.bz2
Updated by Pavel Shved about 14 years ago
- Priority changed from Normal to High
Rising this to consider fixing at the nearest sprint. I feel that we'll encounter more and more errors of that sort as our tools improve!
Updated by Vadim Mutilin about 14 years ago
- Status changed from New to Open
In progress...
Mikhail is working on it
Updated by Vadim Mutilin about 14 years ago
- File drivers-kbdrivers-0032-2.6.31.6-test-0032-2.6.31.6-verdict-unsafe-drivers--usb--class--usblp.c-usblp.c.common.i drivers-kbdrivers-0032-2.6.31.6-test-0032-2.6.31.6-verdict-unsafe-drivers--usb--class--usblp.c-usblp.c.common.i added
- File drivers-kbdrivers-0032-2.6.31.6-test-0032-2.6.31.6-verdict-unsafe-drivers--watchdog--pcwd_usb.c-pcwd_usb.c.common.i drivers-kbdrivers-0032-2.6.31.6-test-0032-2.6.31.6-verdict-unsafe-drivers--watchdog--pcwd_usb.c-pcwd_usb.c.common.i added
Updated by Evgeny Novikov about 14 years ago
Hmmm, it seems that this was already classified as rcv/blast problem:/SMT sovler answer is strange: \*\*\* Parse Error: stdin:29: syntax error/i and print "CVC3 Solver parse error"
("29" was changed with "\d+" by Alexey elsewhere)
Remember about this!
Updated by Pavel Shved about 14 years ago
Eugene Novikov wrote:
Hmmm, it seems that this was already classified as rcv/blast problem:
/SMT sovler answer is strange: \*\*\* Parse Error: stdin:29: syntax error/i and print "CVC3 Solver parse error"
("29" was changed with "\d+" by Alexey elsewhere)
Remember about this!
Elsewhere, but not in master. I've committed a fix that changes the number with .*
(commit:b65aa9b).
Probably, if it was committed earlier, the problem would get much more traction.
Updated by Vadim Mutilin about 14 years ago
- Assignee changed from Pavel Shved to Mikhail Mandrykin
The fix for BLAST is commited to blast repo: 91d5de187311cfbc08e2b71213a596b685cf8189
TODO:
1. regression testing on small(ldv-tests/regr-tests/test-sets/small/regr-task-small) and medium(ldv-tests/regr-tests/test-sets/medium/regr-task-medium) test sets
2. add small test which demonstrates the error to regr-tests small set
Updated by Vadim Mutilin about 14 years ago
Medium regression test results¶
Degradation from safe status:- driver=kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--char--nozomi.c.tar.bz2;origin=external;kernel=linux-2.6.31.6;model=32_1;module=drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--char--nozomi.c/nozomi.ko;main=ldv_main0_plain_sorted_withcheck;verdict=unknown;RCV_status=fail;problems=Out_of_memory
- driver=kbdrivers--0039-2.6.31.6--test-0039-2.6.31.6-verdict-unsafe-drivers--char--epca.c.tar.bz2;origin=external;kernel=linux-2.6.31.6;model=39_1;module=drivers/kbdrivers/0039-2.6.31.6/test-0039-2.6.31.6-verdict-unsafe-drivers--char--epca.c/epca.ko;main=ldv_main0_plain_sorted_withcheck;verdict=unknown;RCV_status=fail;problems=Out_of_memory
- driver=kbdrivers--0032-2.6.31.6--test-0032-2.6.31.6-verdict-unsafe-drivers--watchdog--pcwd_usb.c.tar.bz2;origin=external;kernel=linux-2.6.31.6;model=32_1;module=drivers/kbdrivers/0032-2.6.31.6/test-0032-2.6.31.6-verdict-unsafe-drivers--watchdog--pcwd_usb.c/pcwd_usb.ko;main=ldv_main0_plain_sorted_withcheck;verdict=unknown;RCV_status=fail;problems=CVC3 Solver parse error,Exception
- driver=kbdrivers--0068-2.6.31.6--test-0068-2.6.31.6-verdict-unsafe-drivers--watchdog--pcwd_usb.c.tar.bz2;origin=external;kernel=linux-2.6.31.6;model=68_1;module=drivers/kbdrivers/0068-2.6.31.6/test-0068-2.6.31.6-verdict-unsafe-drivers--watchdog--pcwd_usb.c/pcwd_usb.ko;main=ldv_main0_plain_sorted_withcheck;verdict=unknown;RCV_status=fail;problems=CVC3 Solver parse error,Exception
Updated by Vadim Mutilin almost 14 years ago
- Status changed from Open to Closed
- Published in build set to 8595ebc7713d0c923c1aab8d6411dfb77974569f
Fixed.
Updated by Pavel Shved about 13 years ago
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)