Project

General

Profile

Bug #5327

time out in disk.c

Added by Sepideh Asadi almost 7 years ago. Updated over 6 years ago.

Status:
Feedback
Priority:
Normal
Assignee:
Antti Hyvärinen
Start date:
19/06/2017
Due date:
% Done:

0%

Estimated time:

Description

for e.g claim 15, 16,...

gets timeout with 32, 64 bit unwind 10,...

History

#1 Updated by Karine Even Mendoza almost 7 years ago

1. This shall be run properly with 64 bits,there are many error messages saying it shall better be run in 64 because of the SSA encoding is in 64 bit for this benchmark
2. It is a very heavy code. We always run it with --unwind 1. But for this to run in CUF we need to work much on the performance in Opensmt...
3. there are some issues with the SSA parsing of this code.
4. It works with heuristic 4 (that's why we did it hahaha)

No support for "big" (> 32 bit) integers so far.

Data -8(width 64) is not in between -4294967296 and 4294967295
; theory refiner query time so far: 0.000000
  Weak statement encodings (1) found

Refinement successful
(1 / 548 expressions bit-blasted)
Command-line options to double-check: --theoref --custom 1,

(Warning: Result holds ONLY in this bound (!) Initial unwinding bound: 10)

ASSERTION HOLDS

VERIFICATION SUCCESSFUL
TOTAL TIME FOR CHECKING THIS CLAIM: 6.518

Main Checked Assertion:
file ../../../../../../hi-bench/main-bench/Funfrog15_bench/disk.c line 4425 function IofCompleteRequest
assertion
byte_extract_little_endian(pirp->Tail, 0l, KAPC).ApcListEntry.Blink == (struct _LIST_ENTRY *)byte_extract_little_endian(pirp->Tail, 0l, KAPC).SystemArgument2
#X: Done.
karinek@karinek-VirtualBox:~/workspace/tools/hifrog_lra_lattice/hifrog/trunk/cprover/src/funfrog$ ./hifrog ../../../../../../hi-bench/main-bench/Funfrog15_bench/disk.c --theoref --bitwidth 32 --type-byte-constraints 2 --unwind 10 --claim 15 --heuristic 4

#2 Updated by Karine Even Mendoza over 6 years ago

  • Status changed from New to Feedback
  • Assignee changed from Sepideh Asadi to Antti Hyvärinen
  • Can be a candidate for performance issues once using bithwidth 64 (4=>timeout, 5=>UNSAT)

Currently, there are few new changes from opensmt, but it seems to work fine with 32 or 64 bits (but the proper way to run it is still with 64 bits). ================================== 32 bit
All SSA steps: 6637
Ignored SSA steps after slice: 4146
SLICER TIME: 0.007
CONVERSION TIME: 0.145
; theory refiner query time so far: 0.000000
; 0 | 0 0 | 6.368 s | 160.926 MB
SOLVER TIME: 0.518
RESULT: SAT - doesn't hold

Trying to refine with CUF+BitBlast
(driven by iterative CE-analysis)

; Warning: disabling SATElite preprocessing to track proof
; Forward dependency checker query time so far: 0.000000
; 0 | 0 0 | 6.608 s | 208.766 MB

No support for "big" (> 32 bit) integers so far.

Data 8(width 64) is not in between -4294967296 and 4294967295
; Forward dependency checker query time so far: 0.000000
; ------------------------
; STATISTICS FOR SAT SOLVER
; -------------------------
; Restarts.................: 1
; Conflicts................: 0
; Decisions................: 34
; Propagations.............: 162
; Conflict literals........: 0
; T-Lemmata learnt.........: 0
; T-Lemmata perm learnt....: 0
; Conflicts learnt.........: 0
; T-conflicts learnt.......: 0
; Average learnts size.....: nan
; Top level literals.......: 98
; Search time..............: 0 s
; TSolvers time............: 0 s
; Init clauses.............: 64
; Variables................: 162
; ------------------------
; STATISTICS FOR EUF SOLVER
; -------------------------
; Satisfiable calls........: 0
; Unsatisfiable calls......: 0
; egraph time..............: 0 s
; backtrack time...........: 0 s
; explain time.............: 0 s
; # eq classes at the end..: 0
; -------------------------
; STATISTICS FOR LOGICS
; -------------------------
; Substitutions............: 0

No support for "big" (> 32 bit) integers so far.

Data -8(width 64) is not in between -4294967296 and 4294967295
; Added 1 equalities for bind
; theory refiner query time so far: 0.000000
  Weak statement encodings (1) found

Refinement successful
(1 / 548 expressions bit-blasted)
Command-line options to double-check: --theoref --custom 1,

(Warning: Result holds ONLY in this bound (!) Initial unwinding bound: 10)

ASSERTION HOLDS

VERIFICATION SUCCESSFUL
TOTAL TIME FOR CHECKING THIS CLAIM: 6.368

Main Checked Assertion:
file ../../../../../../hi-bench/main-bench/Funfrog15_bench/disk.c line 4425 function IofCompleteRequest
assertion
byte_extract_little_endian(pirp->Tail, 0l, KAPC).ApcListEntry.Blink (struct _LIST_ENTRY *)byte_extract_little_endian(pirp->Tail, 0l, KAPC).SystemArgument2

===========64 bit
Added 15 equalities for bind
; theory refiner query time so far: 0.000000
Weak statement encodings (1) found
Weak statement encodings (5) found
Weak statement encodings (2) found

Refinement successful
(8 / 548 expressions bit-blasted)
Command-line options to double-check: --theoref --custom 525,531,532,533,534,535,536,542,

(Warning: Result holds ONLY in this bound (!) Initial unwinding bound: 10)

ASSERTION HOLDS

VERIFICATION SUCCESSFUL
TOTAL TIME FOR CHECKING THIS CLAIM: 7.914

Main Checked Assertion:
file ../../../../../../hi-bench/main-bench/Funfrog15_bench/disk.c line 4425 function IofCompleteRequest
assertion
byte_extract_little_endian(pirp->Tail, 0l, KAPC).ApcListEntry.Blink == (struct _LIST_ENTRY *)byte_extract_little_endian(pirp->Tail, 0l, KAPC).SystemArgument2
./hifrog ../../../../../../hi-bench/main-bench/Funfrog15_bench/disk.c --theoref --bitwidth 32 --type-byte-constraints 2 --unwind 10 --claim 15 --heuristic 5

Also available in: Atom PDF