symbiotic
symbiotic copied to clipboard
Consecutive `malloc` allocations are not modelled correctly
The following piece of code contains an error but Symbiotic does not see it:
#include <assert.h>
#include <stdlib.h>
int main(void)
{
void* a = malloc(sizeof(int));
void* b = malloc(sizeof(int));
if (a != NULL && b != NULL)
assert(a != b);
free(b);
void* c = malloc(sizeof(int));
if (a != NULL && c != NULL)
assert(a != c);
assert(b != c); /* can fail */
}
Output:
$ symbiotic symbiotic-mallocs.c
8.0.0-pre-llvm-12.0.1-symbiotic:13ca9347-dg:0b1ada38-sbt-slicer:b0864a5b-sbt-instrumentation:648fabcc-klee:6ecf91e2
INFO: Looking for reachability of calls to __assert_fail,__VERIFIER_error
INFO: Optimizations time: 0.01961374282836914
INFO: Starting slicing
INFO: Total slicing time: 0.02277660369873047
INFO: Optimizations time: 0.020235300064086914
INFO: After-slicing optimizations and transformations time: 2.1457672119140625e-05
INFO: Starting verification
KLEE: WARNING: undefined reference to function: klee_make_nondet
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled. Using alignment of 8.
No error found.
NOTE: In the future, the result is going to be reported in SV-COMP format only with --report=sv-comp switch
RESULT: true
INFO: Total time elapsed: 0.3934328556060791
My machine:
$ cc symbiotic-mallocs.c && ./a.out
a.out: symbiotic-mallocs.c:17: main: Assertion `b != c' failed.
Note that this example is very similar to issue #89.
It works without slicing, so the problem may be in the data dependence analysis.
Yep, the problem is that the slicer removes the call to free
as it does not consider such a case witch comparing pointers could happen.