Problems with --symbolic in SV-COMP benchmarks

[Vladimír Štill]

all with SV-COMP benchmarks or modified versions thereof:

1. divine check --symbolic pthread/stack_true-unreach-call.c
   • finds an error which should not be there
   • get SIGSEGV while trying to generate counterexample
2. pthread/queue_false-unreach-call.c: the transformation fails with

   E: .../lart/abstract/util.cpp: 177:
   encountered Unknown callable value
   

3. 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 takes int and lower 32 bits of DIVINE pointers are often 0)

[Vladimír Štill]

a modified version of pthread-ext/09_fmaxsym_true-unreach-call.c (for bug 3)

[Vladimír Štill]

4. 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)
5. divine check --symbolic ~/repo/sv-benchmarks/c/pthread-wmm/mix016_power.opt_false-unreach-call.c -- in debug version of DIVINE fails with

   loading bitcode … LART … divine: /home/xstill/DIVINE/wip/llvm/lib/IR/Instructions.cpp:299: void llvm::CallInst::init(llvm::FunctionType *, llvm::Value *, ArrayRef<llvm::Value *>, ArrayRef<llvm::OperandBundleDef>, const llvm::Twine &): Assertion `(i >= FTy->getNumParams() || FTy->getParamType(i) == Args[i]->getType()) && "Calling a function with a bad signature!"' failed.
   

   in release mode proceeds to verification and then ends with SEGV.
6. divine check --symbolic -C,-I$HOME/repo/sv-benchmarks/c/pthread-driver-races/model ~/repo/sv-benchmarks/c/pthread-driver-races/char_pc8736x_gpio_pc8736x_gpio_open_pc8736x_gpio_configure_true-unreach-call.c

   loading bitcode … LART … E: .../lart/abstract/util.cpp: 177:
     encountered Unknown callable value
   Aborted
   

[Vladimír Štill]

7. The following code (run with divine check --symbolic) fails with spurious FAULT: 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

[Vladimír Štill]

Recap with today's next:

1. fixed
2. same error (encountered Unknown callable value)
3. (with --lart stubs; otherwise linter error), same error (encountered unknown boolean binary operation 34)
4. probably fixed (divine check running for more than 15 minutes)
5. same error
6. same error
7. same error

[Vladimír Štill]

8. 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
   

[Vladimír Štill]

9. 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.

[Henrich Lauko]

1. fixed
2. Unknown callable value fixed, but aborts on:

E: ../bricks/brick-mem: 111:

expected self()._s->block[ b ]

3. probably fixed (timeout)
4. probably fixed (timeout)
5. same error
6. 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."

7. same error
8. 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
9. same error

[Vladimír Štill]

10. 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.

[Vladimír Štill]

3. 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

[Henrich Lauko]

1. fixed
2. fixed
3. probably fixed (timeout - contains while(1) pthread_create)
4. probably fixed (timeout - contains while(1) pthread_create)
5. probably fixed (crashes with stp, else timeouts)
6. probably fixed (crashes with: Function stub called)
7. same error
8. fixed, stops on passing symbolic value to malloc
9. fixed, stops on passing symbolic value to alloca
10. same error

[Vladimír Štill]

the remaining errors (7 & 10) were transfered to #9 & #10.