Opened 2 months ago

Last modified 2 months ago

#7 new defect

Problems with --symbolic in SV-COMP benchmarks

Reported by: Vladimír Štill Owned by:
Priority: major Milestone:
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 2 months ago.
a modified version of pthread-ext/09_fmaxsym_true-unreach-call.c (for bug 3)

Download all attachments as: .zip

Change History (3)

Changed 2 months 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 2 months 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 2 months ago by Vladimír Štill (previous) (diff)

comment:2 Changed 2 months 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
Note: See TracTickets for help on using tickets.