Project

General

Profile

Bug #5105

inconsistency of HIFROG with CBMC

Added by Sepideh Asadi about 7 years ago. Updated almost 7 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Karine Even Mendoza
Start date:
02/05/2017
Due date:
% Done:

100%

Estimated time:

Description

./ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c

HiFROG --theoref --unwind 10 --bitwidh 32 is UNSAT 6.612

CBMC is SAT 14.92

History

#1 Updated by Karine Even Mendoza about 7 years ago

  • Status changed from New to In Progress
  • Assignee set to Antti Hyvärinen

In master with no-itp version, I get:

Case 349 : Could not resolve struct
member * type: pointer * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 3047 * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog
0: code * return_type: empty * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 3047 * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * parameters:
0: parameter * type: pointer * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 3047 * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog
0: symbol * identifier: tag-virtio_device * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 3047 * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 3047 * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 3047 * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * component_name: del_vqs * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 4273 * function: virtblk_remove * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * #lvalue: 1
0: dereference * type: symbol * identifier: tag-virtio_config_ops * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 3024 * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 4273 * function: virtblk_remove * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * #lvalue: 1
0: member * type: pointer * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 3024 * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog
0: symbol * identifier: tag-virtio_config_ops * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 3024 * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * component_name: config * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 4273 * function: virtblk_remove * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * #lvalue: 1
0: dereference * type: symbol * identifier: tag-virtio_device * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 4250 * function: * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 4273 * function: virtblk_remove * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * #lvalue: 1
0: symbol * type: pointer * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 4250 * function: * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog
0: symbol * identifier: tag-virtio_device * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 4250 * function: * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * identifier: virtblk_remove::vdev * #source_location: * file: ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c * line: 4273 * function: virtblk_remove * working_directory: /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog * #lvalue: 1
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c line 4273 function virtblk_remove: replacing function pointer by 4 possible targets

with valgrind:
13095 Process terminating with default action of signal 6 (SIGABRT)
13095 at 0x602DC37: raise (raise.c:56)
13095 by 0x6031027: abort (abort.c:89)
13095 by 0x6026BF5: __assert_fail_base (assert.c:92)
13095 by 0x6026CA1: __assert_fail (assert.c:101)
13095 by 0x5B163D: RegionAllocator<unsigned int>::operator[](unsigned int) (in /home/karinek/workspace/tools/hifrog_test/hifrog/trunk/cprover/src/funfrog/hifrog)
13095 by 0x4F85625: PtermAllocator::operator[](PTRef) (Pterm.h:346)
13095 by 0x4F857CB: PtStore::operator[](PTRef) (PtStore.h:143)
13095 by 0x4F85816: Logic::getPterm(PTRef) (Logic.h:260)
13095 by 0x50320BC: Logic::mkConst(SRef, char const*) (Logic.C:903)
13095 by 0x502D73F: Logic::Logic(SMTConfig&) (Logic.C:101)
13095 by 0x5053AAB: CUFLogic::CUFLogic(SMTConfig&) (CUFLogic.C:103)
13095 by 0x5056FE0: BVLogic::BVLogic(SMTConfig&, int) (BVLogic.C:86)

I guess that there is some mkconst that is been called with 0 instead of '0'

Antti can you please have a look?

#2 Updated by Karine Even Mendoza almost 7 years ago

  • Assignee changed from Antti Hyvärinen to Karine Even Mendoza

Seems to work now, but with still the wrong result.
Need to check the result in prop

#3 Updated by Karine Even Mendoza almost 7 years ago

  • Status changed from In Progress to Closed
  • % Done changed from 0 to 100

It seems like it checks only the first claim, which is UNSAT, but the second claim is SAT.
I think we must state the claim number in cuf.

COMPARING MORE CAREFULLY:

1.
output from cbmc:
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
358511 variables, 220874 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
358511 variables, 602 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
358511 variables, 0 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime decision procedure: 0.594s

  • Results:
    [] : SUCCESS
    [ldv_error.assertion.1] : FAILURE
    [ldv_error.assertion.2] : FAILURE
    [ldv_error.assertion.3] : SUCCESS
  • 2 of 4 failed (3 iterations)
    VERIFICATION FAILED

Which are:
Property ldv_error.assertion.1:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c line 4414 function ldv_error
assertion
FALSE

Property ldv_error.assertion.2:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c line 4414 function ldv_error
assertion
FALSE

Property ldv_error.assertion.3:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c line 4414 function ldv_error
assertion
FALSE

2.
output from Hifrog
Claim 1: UNSAT
VERIFICATION SUCCESSFUL
TOTAL TIME FOR CHECKING THIS CLAIM: 0.386

Checked Assertion:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c line 4414 function ldv_error
assertion
FALSE

Claim 2: SAT
(Cannot refine due to 16 unsupported operators;e.g., pointer)

VERIFICATION FAILED
TOTAL TIME FOR CHECKING THIS CLAIM: 46.353

Checked Assertion:
file ../../../../../../hi-bench/challenge-bench/sv-comp16/c/ldv-commit-tester/m0_false-unreach-call_drivers-block-virtio_blk-ko--101_1a--39a1d13-1.c line 4414 function ldv_error
assertion
FALSE
#X: Done.

  • In Hifrog there is no claim 3 ** - I guess CBMC added auto-asserts in the cbmc version.

Also available in: Atom PDF