#7 closed defect (fixed)
Problems with --symbolic in SV-COMP benchmarks
Reported by: | Vladimír Štill | Owned by: | |
---|---|---|---|
Priority: | major | Milestone: | 4.2 |
Component: | DiOS | Keywords: | sym, sv-comp |
Cc: |
Description
all with SV-COMP benchmarks or modified versions thereof:
- divine check --symbolic pthread/stack_true-unreach-call.c
- finds an error which should not be there
- get SIGSEGV while trying to generate counterexample
- pthread/queue_false-unreach-call.c: the transformation fails with
E: .../lart/abstract/util.cpp: 177: encountered Unknown callable value
- a modified version of pthread-ext/09_fmaxsym_true-unreach-call.i (attached), fails with
E: .../divine/smt/builder.cpp: 453: encountered unknown boolean binary operation 34
the original version does not fail in this way, therefore I assume it is related to the insertion of double negation into the assumes (a work-around for the fact that assume takesint
and lower 32 bits of DIVINE pointers are often 0)
Attachments (1)
Change History (13)
Changed 6 years ago by
comment:1 Changed 6 years ago by
divine check -C,-fgnu89-inline --svcomp --symbolic ~/repo/sv-benchmarks/c/pthread-ext/39_rand_lock_p0_vs_true-unreach-call.c
-- there is a (probably) spurious memory error on line 46 (invalid dereference, the line manipulates only global and local variables, not allocated variables)
comment:2 Changed 6 years ago by
- The following code (run with
divine check --symbolic
) fails with spuriousFAULT: null pointer dereference: [global* 0 2 ddn]
:#include <assert.h> unsigned long __VERIFIER_nondet_ulong( void ); void *foo() { return __VERIFIER_nondet_ulong(); } int main() { _Bool b = foo(); assert( !b ); } error trace: | FAULT: null pointer dereference: [global* 0 2 ddn] [0] FATAL: memory error in userspace active stack: - symbol: void __dios::Fault<__dios::Scheduler<__dios::MachineParams<__dios::MonitorManager<__dios::BaseContext> > > >::handler<__dios::fs::VFS<__dios::ProcessManager<__dios::Fault<__dios::Scheduler<__dios::MachineParams<__dios::MonitorManager<__dios::BaseContext> > > > > > >(_VM_Fault, _VM_Frame*, void (*)()) location: /dios/include/dios/sys/fault.hpp:193 - symbol: __sym_zext location: /dios/include/sys/lart.h:277 - symbol: lart.sym.zext.i1.i8 location: (unknown location) - symbol: main location: sym-bool.c:9 - symbol: _start location: /dios/src/libc/sys/start.cpp:87
however, if the cast to pointer is removed, the result is OK:
#include <assert.h> unsigned long __VERIFIER_nondet_ulong( void ); unsigned long foo() { return __VERIFIER_nondet_ulong(); } int main() { _Bool b = foo(); assert( !b ); } error trace: | ASSUME (= ((_ extract 0 0) (ite (not (= var_0 #x0000000000000000)) #x01 #x00)) #b1) (0) Assertion failed: !b, file sym-bool.c, line 10. [0] FATAL: assertion failure in userspace
comment:3 Changed 6 years ago by
Recap with today's next:
- fixed
- same error (encountered Unknown callable value)
- (with --lart stubs; otherwise linter error), same error (encountered unknown boolean binary operation 34)
- probably fixed (divine check running for more than 15 minutes)
- same error
- same error
- same error
comment:4 Changed 6 years ago by
-
divine check --svcomp --symbolic ~/repo/sv-benchmarks/c/pthread-memsafety/fillarray_true-valid-memsafety.c compiling /home/xstill/repo/sv-benchmarks/c/pthread-memsafety/fillarray_true-valid-memsafety.c loading bitcode … LART … E: .../lart/abstract/vpa.cpp: 29: expected idx < fn->arg_size() but got 2 >= 1
comment:5 Changed 6 years ago by
divine check --svcomp --symbolic ~/repo/sv-benchmarks/c/array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.c
There is a spurious memory error, probably due to the fact that SYM transformation fails to detect that it is sending symbolic value to alloca
, which results in alloca allocating based on the current explicit value in the variable (which is 0, resulting in allocation size 1). I suggest this problem is for now resolved by an UNREACHABLE
in SYM transformation.
comment:6 Changed 6 years ago by
- fixed
- Unknown callable value fixed, but aborts on:
E: ../bricks/brick-mem: 111:
expected self()._s->block[ b ]
- probably fixed (timeout)
- probably fixed (timeout)
- same error
- Unknown callable value fixed, aborts on unknown function:
ERROR: Program::insert: Unresolved symbol (function): nsc_gpio_dump
Adding --lart stubs makes LART sad:
E: .../lart/abstract/stash.cpp: 127:
expected rets.size() == 1 && "No single return instruction found."
- same error
- partially fixed, programs contains an allocation of symbolic size - finds a spurious error (similar to case 9)
- we need to check for tainted value inside of malloc
- same error
comment:7 Changed 6 years ago by
divine check --lart leak-check --symbolic ~/repo/sv-benchmarks/c/memsafety-ext3/freeAlloca_false-valid-free.c
(Whith patches from ~xstill/DIVINE/svc-2019, namely the leak-check patch.)
There is a spurious memory leak, probably related to --symbolic. A minimal example of the same error:
int __VERIFIER_nondet_int(); int main() { int x = __VERIFIER_nondet_int(); int y = __VERIFIER_nondet_int(); return 0; }
As a sanity check, the previous minimal example with --lart svc-undef-nondet
instead of --symbolic
(this causes __VERIFIER_nondet_*
to return undefined value) does not have any memory leaks.
comment:8 Changed 6 years ago by
- does not work again:
$ /var/obj/xstill-divine-svc-2019/semidbg/tools/divine check --symbolic --lart stubs model.c compiling model.c loading bitcode … LART … setting up pass: stubs, options = INFO: stubbed 1 declarations E: .../lart/abstract/stash.cpp: 163: encountered Unsupported unstash of constant expression. Aborted
comment:9 Changed 6 years ago by
- fixed
- fixed
- probably fixed (timeout - contains while(1) pthread_create)
- probably fixed (timeout - contains while(1) pthread_create)
- probably fixed (crashes with stp, else timeouts)
- probably fixed (crashes with: Function stub called)
- same error
- fixed, stops on passing symbolic value to malloc
- fixed, stops on passing symbolic value to alloca
- same error
comment:11 Changed 6 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
comment:12 Changed 6 years ago by
Milestone: | → 4.2 |
---|
a modified version of pthread-ext/09_fmaxsym_true-unreach-call.c (for bug 3)