staticafi / symbiotic Goto Github PK

incorrect answer with and without slicing

This bug is for gathering information about Symbiotic's incorrect answers

• heap-manipulation/dll_of_dll_true-unreach-call.i #27
• loop-invgen/heapsort_true-unreach-call.i #28

• bug in floats #16

We have lib/ and lib32/ directories now, so we can create lib/lib.o lib32/lib.o and reuse it instead of re-compiling it for each benchmark again

strncmp
strcmp (??)
strchr (??)
strstr

mutexes && kfree (will be done by new instrumentation)

remove it...

slicing the code that has been already sliced does not remove anything (that's good), but if we optimize the code after slicing with opt and stuff like constant propagation and such, then the code can be sliced again with a positive number of nodes removed

try if that's worth it at all

recently I discovered, that something like this is evaluated to TRUE:

RESULT: DBG: terminate called after throwing an instance of 'std::bad_alloc'
RESULT: DBG: what(): std::bad_alloc
RESULT: DBG: 0 klee 0x0000000000e5b945 llvm::sys::PrintStackTrace(_IO_FILE*) + 37
RESULT: DBG: 1 klee 0x0000000000e5bd93
RESULT: DBG: 2 libpthread.so.0 0x00007f3e2c7d0340
RESULT: DBG: 3 libc.so.6 0x00007f3e2b76bcc9 gsignal + 57
RESULT: DBG: 4 libc.so.6 0x00007f3e2b76f0d8 abort + 328
RESULT: DBG: 5 libstdc++.so.6 0x00007f3e2c0a678d __gnu_cxx::__verbose_terminate_handler() + 349
RESULT: DBG: 6 libstdc++.so.6 0x00007f3e2c0a47f6
RESULT: DBG: 7 libstdc++.so.6 0x00007f3e2c0a4841
RESULT: DBG: 8 libstdc++.so.6 0x00007f3e2c0a4a58
RESULT: DBG: 9 libstdc++.so.6 0x00007f3e2c0a4f5c
RESULT: DBG: 10 libstdc++.so.6 0x00007f3e2c0a4fb9 operator new[](unsigned long) + 9
RESULT: DBG: 11 klee 0x00000000005f05b7 klee::PathLocation::PathLocation(std::basic_ifstream >&) + 71
RESULT: DBG: 12 klee 0x00000000005f1181 klee::TreeStreamWriter::readStream(unsigned int, std::vector >&) + 1409
RESULT: DBG: 13 klee 0x000000000054e181
RESULT: DBG: 14 klee 0x0000000000555c56 klee::Executor::terminateStateOnExit(klee::ExecutionState&) + 38
RESULT: DBG: 15 klee 0x0000000000561fc6 klee::Executor::executeInstruction(klee::ExecutionState&, klee::KInstruction*) + 13654
RESULT: DBG: 16 klee 0x0000000000563966 klee::Executor::run(klee::ExecutionState&) + 1654
RESULT: DBG: 17 klee 0x0000000000564211 klee::Executor::runFunctionAsMain(llvm::Function*, int, char**, char**) + 1681
RESULT: DBG: 18 klee 0x0000000000537c51 main + 7921
RESULT: DBG: 19 libc.so.6 0x00007f3e2b756ec5 __libc_start_main + 245
RESULT: DBG: 20 klee 0x000000000054b9e1

instead of only matching patterns in klee's output, check even for the return code and say error when somthing like this happens

strlen, strcpy, memset, etc.

file as a bug for klee

  1 #include <assert.h>
  2 #define N 1000000000
  3 
  4 int main(void)
  5 {
  6   int a[N];
  7   int max = 0;
  8   int i = 0;
  9   while (i < N) {
 10     if (a[i] > max)
 11       max = a[i];
 12       ++i;
 13   }
 14 
 15   int x;
 16   for ( x = 0 ; x < N ; x++ )
 17     assert(a[x] <= max);
 18 
 19   return 0;
 20 }

This program makes klee to write out out of bound pointer, while it is perfectly ok. It is due to states overlap (Executor.cpp:3236). Klee does not distinguish between out of bound and overlap -> file it as a bug for klee

how is it with handling POSIX signals? ... it is more or less like threaded application, so nothing for symbiotic now...

  1 int *getelem(int array[10], int idx)
  2 {
  3         __VERIFIER_assert(idx >= 0 && idx < 10);
  4         return &array[idx];
  5 }
  6 
  7 int main(void)
  8 {
  9         int array[10] = { 0 };
 10 
 11         for (int i = 0; i < 1000; ++i) {
 12                 int *p = getelem(array, rand() % 11);
 13                 *p = 1;
 14         }
 15 
 16         doit(array);
 17         return 0;
 18 }

with --optimizations=before-O2,after we get TRUE, without it we get FALSE (correct)

RESULT: KLEE: WARNING: undefined reference to function: __VERIFIER_nondet_int8_t
RESULT: KLEE: WARNING: undefined reference to function: __VERIFIER_nondet_msg_t

https://svn.sosy-lab.org/software/sv-benchmarks/trunk/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c?p=587

last time when I updated slicer, the version file was not updated

strdup can never fail - change libc such that there will be a macro 'MALLOC_NEVER_FAILS' and this macro will cause conditional compilation of lib.c
This way we'll have just one version of __VERIFIER_malloc() function

We don't want that in distribution

• floats-cbmc-regression/float14_true-unreach-call.i prepare odstrani __isinff, bez prepare da klee spravny vysledek
• floats-cbmc-regression/float4_true-unreach-call.i klee vola __isnan a __isinf s argumentem 0 (konkretizoval?)
• floats-cbmc-regression/float4_true-unreach-call.i prepare odstrani volani __isinf - klee bez prepare spadne na nepodporovane instrukci
• floats-cbmc-regression/float-rounding1_true-unreach-call.i prepare odstrani fesetround, ale klee da spatny vysledek jak s prepare tak bez prepare

This code should result in TRUE, but is FALSE with optimizations 'before' (without opts or without slicing it is fine)

#include <assert.h>

int a = 0;
int *p = ((void *) 0); 

void set(void)
{
        if (!a)
                p = &a; 
        else
                p = ((void *) 0); 
}

int main(void)
{
        int b = 2;
        if (a > b) {
                set();
                *p = 3;
        } else {
                set();
                *p = 4;
        }

        assert(a == 4); 
        return 0;
}

We strip the binaries anyway

klee reports TRUE for this code (once we remove the loop, it reports FALSE). It reports TRUE without any optimizations, so there should be no problem with n being unspecified (with opts it gets correct)

#include <assert.h>

int main()
{
        int a;
        int n;

        if( n < 0 ) 
                return 0;

        for(; n < 100; n++) {
        }

        ++n;
        a = 2;
        assert(a == 3); 

        return 0;
}

there are some hard-coded data types, like:
typedef unsigned int size_t

this could break something, fix it! (conditional compilation)

we got TRUE (even without optimizations), without slicing we get FALSE (in like 170 seconds), so I assume the bug is in slicer

on this file: https://github.com/smackers/smack/blob/master/test/basic/func_ptr1.c

normal run: abort
without optimize: true (correct)
without slicing: true (correct)

fsetround uses uninitialized value

Once we reach the assertion, we don't have to go through the other paths. This can lead to timeout or error even when we found the error path

• add verifier missing types (mainly __VERIFIER_nondet_bool)
• slicer sigsegv removing undef - fix the undef!
• when slicer do not find slicing criterion, say TRUE
• add klee_assume() to all malloc + calloc calls (that the pointer is not null)
• make EGENERAL bound to KLEE: ERROR: not to 'now ignoring error on this loca'
• fix truncateToNBits bug in klee

$subj and import them to the main script. The code will be more readable and maintainable. Then we can add even some simple GUI

That is:
what calls to undefined functions has been removed
what happend on error
etc.

There are just few files and the scripts are going to be rewritten into python later, so svc15 will be almost empty

when parsing klee we do while read LINE, but then we dont use the line. I'm surprised it works... Just remove it and let the input go to grep

if slicer breaks the module, say error or unknown (when slicer required) or use the original (when slicer is not required)

RESULT: DBG: = ptrtoint to label
RESULT: DBG: br i1 %26, label , label %30
RESULT: DBG: Broken module found, verification continues.
RESULT: DBG: Instruction does not dominate all uses!

run whole symbiotic in subdirectory, so that we won't mess up file system

directories LLVMSlicer, dg and svc15 are not created during build, build is aborted

We should do something with that

Symbiotic says TRUE.
Without optimizations, it says FALSE
without slicing it says FALSE also

check it!

sv-benchmarks/c/ldv-regression/alias_of_return.c_true-unreach-call.i

this file has no return statement, file the bug upstream

The right fix is to fix the benchmark:
https://github.com/dbeyer/sv-benchmarks/blob/master/c/seq-pthread/cs_lamport_true-unreach-call.c

the check property probably does not work, there is everywhere ERROR instead of UNKNOWN

rename the old to blah-blah-external or something like that and make the new use submodules as it will be easier to fetch and compile them

--debug=all should be the same as --debug=slicer,prepare,compile , but it is just a basic debug

add tests to symbiotic project that will test regressions, like:

__VERIFIER_assert(isdigit('1'))

and similar (this code was not working before)

merge the scripts into one-two scripts and rewrite it all into python/perl

try command update and without update, when the directory is there or is not there

These two benchmarks has 'Prepare phase failed'

ntdrivers/cdaudio_true-unreach-call.i.cil.c
ntdrivers/cdaudio_false-unreach-call.i.cil.c

Undefined globals should be made symbolic, why isn't it working?

KLEE: ERROR: unable to load symbol(xen_xenbus_fops) while initializing globals.
KLEE: ERROR: unable to load symbol(BATERY_GAIN) while initializing globals.

klee (and witness checkers - namely CPAchecker) answers the same if it does not timeout, so maybe bug in benchmark?

if somebody checks for returned value from malloc we say unknown just for that (because we hit abort failure)

if ((mem = malloc(...)) == NULL)
   abort();

we can replace abort with klee_assume()

skipping fork
killing XXX states (over memory cap)

write out when points-to started and similar, so that we know if symbiotic timeouted in slicer (and in what phase) or in klee

This file is false(confirmed) but generating the witness failed: https://github.com/dbeyer/sv-benchmarks/blob/master/c/loop-acceleration/multivar_false-unreach-call1.i