Skip to content

Commit

Permalink
verify: start esbmc support
Browse files Browse the repository at this point in the history 
fix for older cbmc (no __CPROVER_loop_invariant)
  • Loading branch information
@rurban
rurban committed Nov 10, 2024
1 parent 15dd6e6 commit 0ce6d1d
Show file tree
Hide file tree
Showing 3 changed files with 47 additions and 23 deletions.
6 changes: 5 additions & 1 deletion GNUmakefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,7 @@ check: all
for t in $(TESTS); do echo $$t rand2 2; $(DRV) ./$(TESTBIN) $$t rand2 2; done
$(DRV) ./$(SELECTBIN) -all block bmh2 bmh4 dfdm sbdm faoso2 blim ssecp
-mv algorithms.lst.bak algorithms.lst
lint: cppcheck clang-tidy sanitizer.log
lint: algocfg cppcheck clang-tidy sanitizer.log
# for newer cppcheck
#CPPCHECK_ARGS="-j4 --enable=warning,portability --inline-suppr --check-level=exhaustive"
CPPCHECK_ARGS = -j4 --enable=warning,portability --inline-suppr
Expand All @@ -164,10 +164,14 @@ good.lst: algocfg
asan.lst: algocfg
./algocfg good 0 | perl -nle'%bad=map{$$_=>1}split/ /;for(split/ /,qx"./algocfg asan"){print $$_ unless $$bad{$$_}}' >$@

ifeq (esbmc, $(CBMC))
CBMC_ARGS = -Isource/algos -DCBMC -DESBMC
else
CBMC_ARGS = -Isource/algos -DCBMC --bounds-check --pointer-check --memory-leak-check \
--div-by-zero-check --signed-overflow-check --unsigned-overflow-check \
--pointer-overflow-check --conversion-check --undefined-shift-check \
--float-overflow-check --nan-check --enum-range-check
endif
#CBMC_VERSION := $(shell cbmc --version | cut -c1-3)
#CBMC_ARGS += $(shell if test "`echo "$$CBMC_VERSION >= 5.13" | bc`" = 1; then \
# echo "--pointer-primitive-check"; fi)
Expand Down
11 changes: 9 additions & 2 deletions source/algocfg.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -455,11 +455,18 @@ int main(int argc, char **argv) {
else if (strcmp(cfg, "timeout") == 0)
printf("%d\n", ALGOCFGS[id].timeout_min);
else if (strcmp(cfg, "cbmc") == 0) {
char *cbmc = getenv("CBMC");
if (!cbmc)
cbmc = "cbmc";
// cmbc 5.12 has too high default verbosity 8, we want 6 + unwind summaries
if (ALGOCFGS[id].timeout_min)
printf("timeout %dm cbmc --verbosity 7 ", ALGOCFGS[id].timeout_min);
printf("timeout %dm %s --verbosity 7 ", ALGOCFGS[id].timeout_min, cbmc);
else
printf("timeout 4m cbmc --verbosity 7 ");
printf("timeout 4m %s --verbosity 7 ", cbmc);
if (strcmp(cbmc, "esbmc") == 0) {
printf("\n");
return 0;
}
if (ALGOCFGS[id].depth)
printf("--depth %d ", ALGOCFGS[id].depth);
if (ALGOCFGS[id].unwind)
Expand Down
53 changes: 33 additions & 20 deletions source/algos/include/cbmc.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,14 +13,27 @@
#define XSIZE MAX_M
#define YSIZE MAX_N

#ifndef ESBMC
#define __VERIFIER_assume(x) __CPROVER_assume(x)
#define __VERIFIER_assert(x) __CPROVER_assert(x)
#define __VERIFIER_nondet_uchar nondet_uchar
#define __VERIFIER_nondet_int nondet_int
#else
void __VERIFIER_assert(int cond);
#define __VERIFIER_input(a,b)
#define __VERIFIER_output(a,b)
#endif
// not needed, and would need cbmc > 5.12
#define __CPROVER_loop_invariant(cond)

/* the brute force algorithm used for comparing occurrences */
static inline int bf_search(unsigned char *x, int m, unsigned char *y, int n) {
assert(m < MAX_M);
assert(n < MAX_N);
int count = 0;
for (int j = 0; j <= n - m; ++j)
__CPROVER_loop_invariant(j <= MAX_N - MAX_M)
__CPROVER_loop_invariant(j >= __CPROVER_loop_entry(j))
__CPROVER_loop_invariant(j >= __VERIFIER_loop_entry(j))
{
if (memcmp(x, &y[j], m) == 0)
count++;
Expand All @@ -38,7 +51,7 @@ static inline int bf_search_large(unsigned char *x, int m, unsigned char *y, int
int count = 0;
for (int j = 0; j <= n - m; ++j)
__CPROVER_loop_invariant(j <= n - MAX_M)
__CPROVER_loop_invariant(j >= __CPROVER_loop_entry(j))
__CPROVER_loop_invariant(j >= __VERIFIER_loop_entry(j))
{
if (memcmp(x, &y[j], m) == 0)
count++;
Expand All @@ -50,22 +63,22 @@ static inline int bf_search_large(unsigned char *x, int m, unsigned char *y, int
return count;
}

unsigned char nondet_uchar();
int nondet_int();
unsigned char __VERIFIER_nondet_uchar();
int __VERIFIER_nondet_int();

int main(void) {
#define RANDCH(c) \
{ \
c = nondet_uchar(); \
__CPROVER_assume(c > 0 && c <= 255); \
c = __VERIFIER_nondet_uchar(); \
__VERIFIER_assume(c > 0 && c <= 255); \
}
int m = MAX_M; // nondet_int();
int m = MAX_M; // __VERIFIER_nondet_int();
#ifdef MIN_M
__CPROVER_assume(m > MIN_M && m < MAX_M);
__VERIFIER_assume(m > MIN_M && m < MAX_M);
#else
__CPROVER_assume(m > 0 && m < MAX_M);
__VERIFIER_assume(m > 0 && m < MAX_M);
#endif
int n = MAX_N; // nondet_int();
int n = MAX_N; // __VERIFIER_nondet_int();
unsigned char P[32];
unsigned char T[256];
for (int i = 0; i < MAX_M; i++)
Expand All @@ -74,29 +87,29 @@ int main(void) {
for (int i = 0; i < MAX_N; i++)
__CPROVER_loop_invariant(i < MAX_N)
RANDCH(T[i]);
__CPROVER_input("P", P);
//__CPROVER_input("m", m);
__CPROVER_input("T", T);
//__CPROVER_input("n", n);
__VERIFIER_input("P", P);
//__VERIFIER_input("m", m);
__VERIFIER_input("T", T);
//__VERIFIER_input("n", n);
int occ, ref;

#define M_N_LOOP(m, n) \
T[n] = '\0'; \
P[m] = '\0'; \
occ = search(P, m, T, n); \
__CPROVER_output("occ", occ); \
__VERIFIER_output("occ", occ); \
ref = bf_search(P, m, T, n); \
__CPROVER_output("ref", ref); \
__CPROVER_assert(ref == occ, "ref == occ")
__VERIFIER_output("ref", ref); \
__VERIFIER_assert(ref == occ)

#define M_N_LOOP_LARGE(m, n) \
T[n] = '\0'; \
P[m] = '\0'; \
occ = search(P, m, T, n); \
__CPROVER_output("occ", occ); \
__VERIFIER_output("occ", occ); \
ref = bf_search(P, m, T, n); \
__CPROVER_output("ref", ref); \
__CPROVER_assert(ref == occ, "ref == occ")
__VERIFIER_output("ref", ref); \
__VERIFIER_assert(ref == occ)

#if MIN_M == 0
M_N_LOOP(0, MAX_N-1);
Expand Down

0 comments on commit 0ce6d1d

Please sign in to comment.