Opened 6 years ago

Closed 5 years ago

Last modified 5 years ago

#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:

  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)

Attachments (1)

model.c (883 bytes) - added by Vladimír Štill 6 years ago.
a modified version of pthread-ext/09_fmaxsym_true-unreach-call.c (for bug 3)

Download all attachments as: .zip

Change History (13)

Changed 6 years ago by Vladimír Štill

Attachment: model.c added

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

comment:1 Changed 6 years ago by Vladimír Štill

  1. 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)
  2. 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.
  3. 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
    
Last edited 6 years ago by Vladimír Štill (previous) (diff)

comment:2 Changed 6 years ago by Vladimír Štill

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

comment:3 Changed 5 years ago by 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

comment:4 Changed 5 years ago by Vladimír Štill

  1. 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 5 years ago by Vladimír Štill

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

Last edited 5 years ago by Vladimír Štill (previous) (diff)

comment:6 Changed 5 years ago by Henrich Lauko

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

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

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

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


  1. same error
  2. 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
  3. same error
Last edited 5 years ago by Henrich Lauko (previous) (diff)

comment:7 Changed 5 years ago by Vladimír Štill

  1. 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 5 years ago by Vladimír Štill

  1. 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 5 years ago by 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

comment:10 Changed 5 years ago by Vladimír Štill

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

comment:11 Changed 5 years ago by Vladimír Štill

Resolution: fixed
Status: newclosed

comment:12 Changed 5 years ago by mornfall

Milestone: 4.2
Note: See TracTickets for help on using tickets.