esbmc
esbmc copied to clipboard
esbmc
[C] ESBMC shows false positive(?) comparing to CBMC
- I am testing a mapping library from rxi/map which I am planning to implement in Solidity
struct map_node_t;
typedef struct map_node_t map_node_t;
typedef struct
{
map_node_t **buckets;
unsigned nbuckets, nnodes;
} map_base_t;
typedef struct
{
unsigned bucketidx;
map_node_t *node;
} map_iter_t;
#define map_t(T) \
struct \
{ \
map_base_t base; \
T *ref; \
T tmp; \
}
#define map_init(m) \
memset(m, 0, sizeof(*(m)))
#define map_deinit(m) \
map_deinit_(&(m)->base)
#define map_get(m, key) \
((m)->ref = map_get_(&(m)->base, key))
#define map_set(m, key, value) \
((m)->tmp = (value), \
map_set_(&(m)->base, key, &(m)->tmp, sizeof((m)->tmp)))
#define map_remove(m, key) \
map_remove_(&(m)->base, key)
#define map_iter(m) \
map_iter_()
#define map_next(m, iter) \
map_next_(&(m)->base, iter)
void map_deinit_(map_base_t *m);
void *map_get_(map_base_t *m, const char *key);
int map_set_(map_base_t *m, const char *key, void *value, int vsize);
void map_remove_(map_base_t *m, const char *key);
map_iter_t map_iter_(void);
const char *map_next_(map_base_t *m, map_iter_t *iter);
typedef map_t(void *) map_void_t;
typedef map_t(char *) map_str_t;
typedef map_t(int) map_int_t;
typedef map_t(char) map_char_t;
struct map_node_t
{
unsigned hash;
void *value;
map_node_t *next;
/* char key[]; */
/* char value[]; */
};
static unsigned map_hash(const char *str)
{
unsigned hash = 5381;
while (*str)
{
hash = ((hash << 5) + hash) ^ *str++;
}
return hash;
}
static map_node_t *map_newnode(const char *key, void *value, int vsize)
{
map_node_t *node;
int ksize = strlen(key) + 1;
int voffset = ksize + ((sizeof(void *) - ksize) % sizeof(void *));
node = malloc(sizeof(*node) + voffset + vsize);
if (!node)
return NULL;
memcpy(node + 1, key, ksize);
node->hash = map_hash(key);
node->value = ((char *)(node + 1)) + voffset;
memcpy(node->value, value, vsize);
return node;
}
static int map_bucketidx(map_base_t *m, unsigned hash)
{
/* If the implementation is changed to allow a non-power-of-2 bucket count,
* the line below should be changed to use mod instead of AND */
return hash & (m->nbuckets - 1);
}
static void map_addnode(map_base_t *m, map_node_t *node)
{
int n = map_bucketidx(m, node->hash);
node->next = m->buckets[n];
m->buckets[n] = node;
}
static int map_resize(map_base_t *m, int nbuckets)
{
map_node_t *nodes, *node, *next;
map_node_t **buckets;
int i;
/* Chain all nodes together */
nodes = NULL;
i = m->nbuckets;
while (i--)
{
node = (m->buckets)[i];
while (node)
{
next = node->next;
node->next = nodes;
nodes = node;
node = next;
}
}
/* Reset buckets */
buckets = realloc(m->buckets, sizeof(*m->buckets) * nbuckets);
if (buckets != NULL)
{
m->buckets = buckets;
m->nbuckets = nbuckets;
}
if (m->buckets)
{
memset(m->buckets, 0, sizeof(*m->buckets) * m->nbuckets);
/* Re-add nodes to buckets */
node = nodes;
while (node)
{
next = node->next;
map_addnode(m, node);
node = next;
}
}
/* Return error code if realloc() failed */
return (buckets == NULL) ? -1 : 0;
}
static map_node_t **map_getref(map_base_t *m, const char *key)
{
unsigned hash = map_hash(key);
map_node_t **next;
if (m->nbuckets > 0)
{
next = &m->buckets[map_bucketidx(m, hash)];
while (*next)
{
if ((*next)->hash == hash && !strcmp((char *)(*next + 1), key))
{
return next;
}
next = &(*next)->next;
}
}
return NULL;
}
void map_deinit_(map_base_t *m)
{
map_node_t *next, *node;
int i;
i = m->nbuckets;
while (i--)
{
node = m->buckets[i];
while (node)
{
next = node->next;
free(node);
node = next;
}
}
free(m->buckets);
}
void *map_get_(map_base_t *m, const char *key)
{
map_node_t **next = map_getref(m, key);
return next ? (*next)->value : NULL;
}
int map_set_(map_base_t *m, const char *key, void *value, int vsize)
{
int n, err;
map_node_t **next, *node;
/* Find & replace existing node */
next = map_getref(m, key);
if (next)
{
memcpy((*next)->value, value, vsize);
return 0;
}
/* Add new node */
node = map_newnode(key, value, vsize);
if (node == NULL)
goto fail;
if (m->nnodes >= m->nbuckets)
{
n = (m->nbuckets > 0) ? (m->nbuckets << 1) : 1;
err = map_resize(m, n);
if (err)
goto fail;
}
map_addnode(m, node);
m->nnodes++;
return 0;
fail:
if (node)
free(node);
return -1;
}
void map_remove_(map_base_t *m, const char *key)
{
map_node_t *node;
map_node_t **next = map_getref(m, key);
if (next)
{
node = *next;
*next = (*next)->next;
free(node);
m->nnodes--;
}
}
map_iter_t map_iter_(void)
{
map_iter_t iter;
iter.bucketidx = -1;
iter.node = NULL;
return iter;
}
const char *map_next_(map_base_t *m, map_iter_t *iter)
{
if (iter->node)
{
iter->node = iter->node->next;
if (iter->node == NULL)
goto nextBucket;
}
else
{
nextBucket:
do
{
if (++iter->bucketidx >= m->nbuckets)
{
return NULL;
}
iter->node = m->buckets[iter->bucketidx];
} while (iter->node == NULL);
}
return (char *)(iter->node + 1);
}
int main()
{
map_int_t m;
map_init(&m);
map_set(&m, "testkey", 123);
int *val = map_get(&m, "testkey");
if (val)
{
assert(1);
}
else
{
assert(0);
}
}
ESBMC: esbmc file.c --unwind 8 --no-unwinding-assertions or esbmc file.c --k-induction
[Counterexample]
State 1 file file.c line 289 column 2 function main thread 0
----------------------------------------------------
m = { .base={ .buckets = 0 }, .ref=INVALID1048576, .tmp=0,
.anon_pad$3=0 }
State 3 file file.c line 291 column 2 function main thread 0
----------------------------------------------------
(&m)->tmp = 123 (00000000 00000000 00000000 01111011)
State 4 file file.c line 102 column 2 function map_newnode thread 0
----------------------------------------------------
node = ( struct map_node_t *)0
State 5 file file.c line 207 column 2 function map_get_ thread 0
----------------------------------------------------
next = 0
State 10 file file.c line 292 column 13 function main thread 0
----------------------------------------------------
(&m)->ref = (signed int *)0
State 11 file file.c line 292 column 2 function main thread 0
----------------------------------------------------
val = m.ref
State 12 file file.c line 299 column 3 function main thread 0
----------------------------------------------------
Violated property:
file file.c line 299 column 3 function main
assertion
(_Bool)0
VERIFICATION FAILED
CBMC: cbmc file.c --pointer-check --pointer-overflow-check --unwind 10 --no-unwinding-assertions
VERIFICATION SUCCESSFUL
According to the program logic, we should reach the assert(1) rather than assert(0). So I assume in this case ESBMC generates a false positive.
The cause might be that, whatever value we set to the key, the return val in ESBMC will always be NULL (assert(val == NULL) always hold).
You can use the option --force-malloc-success to ensure that malloc always succeeds.
You can use the option
--force-malloc-successto ensure that malloc always succeeds.
Thanks for the suggestions. I tried --k-induction --force-malloc-success and --unwind 9 --no-unwinding-assertions --force-malloc-success --no-pointer-check and still get the incorrect result
[Counterexample]
State 1 file file.c line 289 column 2 function main thread 0
----------------------------------------------------
m = { .base = { .buckets = 0 } }
State 2 file file.c line 291 column 2 function main thread 0
----------------------------------------------------
(&m)->tmp = 123 (00000000 00000000 00000000 01111011)
State 3 file file.c line 228 column 3 function map_set_ thread 0
----------------------------------------------------
n = (signed int)(m.base.nbuckets > 0 ? m.base.nbuckets << 1 : 1)
State 4 file file.c line 133 column 2 function map_resize thread 0
----------------------------------------------------
i = (signed int)m.base.nbuckets
State 5 file file.c line 134 column 9 function map_resize thread 0
----------------------------------------------------
i = -1 (11111111 11111111 11111111 11111111)
State 6 file file.c line 146 column 2 function map_resize thread 0
----------------------------------------------------
buckets = ( struct map_node_t * *)0
State 7 file file.c line 149 column 3 function map_resize thread 0
----------------------------------------------------
m->buckets = 0
State 8 file file.c line 150 column 3 function map_resize thread 0
----------------------------------------------------
m->nbuckets = 1 (00000000 00000000 00000000 00000001)
State 9 file file.c line 156 column 3 function map_resize thread 0
----------------------------------------------------
node = 0
State 10 file file.c line 234 column 2 function map_set_ thread 0
----------------------------------------------------
m->nnodes = m.base.nnodes + 1
State 11 file file.c line 174 column 3 function map_getref thread 0
----------------------------------------------------
next = m.base.buckets
State 12 file file.c line 181 column 4 function map_getref thread 0
----------------------------------------------------
next = ( struct map_node_t * *)(0 + 16)
State 13 file file.c line 181 column 4 function map_getref thread 0
----------------------------------------------------
next = ( struct map_node_t * *)(0 + 16)
State 14 file file.c line 181 column 4 function map_getref thread 0
----------------------------------------------------
next = ( struct map_node_t * *)(0 + 16)
State 15 file file.c line 181 column 4 function map_getref thread 0
----------------------------------------------------
next = ( struct map_node_t * *)(0 + 16)
State 16 file file.c line 181 column 4 function map_getref thread 0
----------------------------------------------------
next = ( struct map_node_t * *)(0 + 16)
State 17 file file.c line 181 column 4 function map_getref thread 0
----------------------------------------------------
next = ( struct map_node_t * *)(0 + 16)
State 18 file file.c line 181 column 4 function map_getref thread 0
----------------------------------------------------
next = ( struct map_node_t * *)(0 + 16)
State 19 file file.c line 181 column 4 function map_getref thread 0
----------------------------------------------------
next = ( struct map_node_t * *)(INVALID4294967295 + 16)
State 20 file file.c line 207 column 2 function map_get_ thread 0
----------------------------------------------------
next = 0
State 21 file file.c line 292 column 13 function main thread 0
----------------------------------------------------
(&m)->ref = (signed int *)0
State 22 file file.c line 292 column 2 function main thread 0
----------------------------------------------------
val = m.ref
State 23 file file.c line 299 column 3 function main thread 0
----------------------------------------------------
Violated property:
file file.c line 299 column 3 function main
assertion
(_Bool)0
VERIFICATION FAILED
Bug found (k = 9)
You can use c-reduce to reduce the program so that we can find out the root cause of this issue:
https://github.com/esbmc/esbmc/wiki/Reducing-C-Programs
#!/bin/bash
esbmc race-1_1-join.c --incremental-bmc --context-bound 2 --no-pointer-check --no-bounds-check --no-div-by-zero-check --no-slice --yices --no-por >esbmc_out.txt 2>&1
cbmc race-1_1-join.c >cbmc_out.txt 2>&1
grep 'VERIFICATION FAILED' esbmc_out.txt >/dev/null 2>&1 &&\
grep 'VERIFICATION SUCCESSFUL' cbmc_out.txt >/dev/null 2>&1
typedef struct {
int *a;
} b;
typedef struct {
b base;
} c;
c e;
d(b *i) {
b f = *i;
while (f.a)
;
}
g(b *i) {
b h = *i;
int *a = realloc(h.a, a);
i->a = a;
}
main() {
g(&(&e)->base);
d(&(&e)->base);
assert(0);
}
I further simplified it a little bit
#include <stdlib.h>
#include <assert.h>
typedef struct
{
int *a;
} b;
typedef struct
{
b base;
} c;
c e;
void g(b *i)
{
b h = *i;
int *a = realloc(h.a, a);
assert(a != NULL);
}
int main()
{
g(&(&e)->base);
}
I also compiled and executed the binary, and no assertion failure occurred. CBMC shows SUCCESSFUL, ESBMC shows FAILED.
Further simplified:
#include <stdlib.h>
#include <assert.h>
int main()
{
void *p = realloc(NULL, 0);
assert(p);
}
Related: #1182, #1462.
Edit: Note, for this specific example with new_size being zero, there are (new in C23) caveats:
What is the verdict for this issue here? My view: CBMC defaults to --force-malloc-success (which for us should imply realloc() success as well, I believe), therefore without that flag there would be no discrepancy.
With the flag, and the default C standard (gnu17 for clang-11 through 18), we have a bug in that the pointer returned from realloc() is not valid. That's #1462, right? Is there a case I missed?
What is the verdict for this issue here? My view: CBMC defaults to --force-malloc-success (which for us should imply realloc() success as well, I believe), therefore without that flag there would be no discrepancy.
With the flag, and the default C standard (gnu17 for clang-11 through 18), we have a bug in that the pointer returned from realloc() is not valid. That's #1462, right? Is there a case I missed?
Yes, I believe it is the #1462. In this case, I tried to disable the esbmc pointer-check, and the value of (*p) seems to be a random value.