diff --git a/regression/symex-shortest-path/Makefile b/regression/symex-shortest-path/Makefile new file mode 100644 index 0000000..3285ad6 --- /dev/null +++ b/regression/symex-shortest-path/Makefile @@ -0,0 +1,35 @@ +default: tests.log + +test: + @if ! ../../lib/cbmc/regression/test.pl -c "../../../src/symex/symex --shortest-path" ; then \ + ../../lib/cbmc/regression/failed-tests-printer.pl ; \ + exit 1 ; \ + fi + + @if ! ../../lib/cbmc/regression/test.pl -c "../../../src/symex/symex --shortest-path --randomize" ; then \ + ../../lib/cbmc/regression/failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +tests.log: ../test.pl + @if ! ../../lib/cbmc/regression/test.pl -c "../../../src/symex/symex --shortest-path" ; then \ + ../../lib/cbmc/regression/failed-tests-printer.pl ; \ + exit 1 ; \ + fi + + @if ! ../../lib/cbmc/regression/test.pl -c ../../../src/symex/symex "--shortest-path --randomize" ; then \ + ../../lib/cbmc/regression/failed-tests-printer.pl ; \ + exit 1 ; \ + fi + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + find -name '*.gb' -execdir $(RM) '{}' \; + $(RM) tests.log diff --git a/regression/symex-shortest-path/bst-safe/main.c b/regression/symex-shortest-path/bst-safe/main.c new file mode 100644 index 0000000..868a204 --- /dev/null +++ b/regression/symex-shortest-path/bst-safe/main.c @@ -0,0 +1,101 @@ +// This file contains code snippets from "Algorithms in C, Third Edition, +// Parts 1-4," by Robert Sedgewick. +// +// See https://www.cs.princeton.edu/~rs/Algs3.c1-4/code.txt + +#include +#include + +#define N 1000 + + +#ifdef ENABLE_KLEE +#include +#endif + +typedef int Key; +typedef int Item; + +#define eq(A, B) (!less(A, B) && !less(B, A)) +#define key(A) (A) +#define less(A, B) (key(A) < key(B)) +#define NULLitem 0 + +struct STnode; +typedef struct STnode* link; + +struct STnode { Item item; link l, r; int n; }; +static link head, z; + +static link NEW(Item item, link l, link r, int n) { + link x = malloc(sizeof *x); + x->item = item; x->l = l; x->r = r; x->n = n; + return x; +} + +void STinit() { + head = (z = NEW(NULLitem, 0, 0, 0)); +} + +int STcount() { return head->n; } + +static link insertR(link h, Item item) { + Key v = key(item), t = key(h->item); + if (h == z) return NEW(item, z, z, 1); + + if (less(v, t)) + h->l = insertR(h->l, item); + else + h->r = insertR(h->r, item); + + (h->n)++; return h; +} + +void STinsert(Item item) { head = insertR(head, item); } + +static void sortR(link h, void (*visit)(Item)) { + if (h == z) return; + sortR(h->l, visit); + visit(h->item); + sortR(h->r, visit); +} + +void STsort(void (*visit)(Item)) { sortR(head, visit); } + + +static Item a[N]; +static unsigned k = 0; +void sorter(Item item) { + a[k++] = item; +} + +#ifdef ENABLE_CPROVER +int nondet_int(); +#endif + +// Unwind N+1 times +int main() { +#ifdef ENABLE_KLEE + klee_make_symbolic(a, sizeof(a), "a"); +#endif + + STinit(); + + for (unsigned i = 0; i < N; i++) { +#ifdef ENABLE_CPROVER + STinsert(nondet_int()); +#elif ENABLE_KLEE + STinsert(a[i]); + a[i] = NULLitem; +#endif + } + + STsort(sorter); + +#ifndef FORCE_BRANCH + for (unsigned i = 0; i < N - 1; i++) + assert(a[i] <= a[i+1]); +#endif + + return 0; +} diff --git a/regression/symex-shortest-path/bst-safe/test.desc b/regression/symex-shortest-path/bst-safe/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/bst-safe/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/concrete-sum-unsafe/main.c b/regression/symex-shortest-path/concrete-sum-unsafe/main.c new file mode 100644 index 0000000..42feb3f --- /dev/null +++ b/regression/symex-shortest-path/concrete-sum-unsafe/main.c @@ -0,0 +1,18 @@ +#include + +#define N 40000 + +int main(void) { + unsigned n = 1; + unsigned sum = 0; + + while (n <= N) + { + sum = sum + n; + n = n + 1; + } + + assert(sum != ((N * (N + 1)) / 2)); + + return 0; +} diff --git a/regression/symex-shortest-path/concrete-sum-unsafe/test.desc b/regression/symex-shortest-path/concrete-sum-unsafe/test.desc new file mode 100644 index 0000000..510460c --- /dev/null +++ b/regression/symex-shortest-path/concrete-sum-unsafe/test.desc @@ -0,0 +1,6 @@ +CORE +main.c + +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/concrete-sum/concrete-sum-unsafe.c b/regression/symex-shortest-path/concrete-sum/concrete-sum-unsafe.c new file mode 100644 index 0000000..584f997 --- /dev/null +++ b/regression/symex-shortest-path/concrete-sum/concrete-sum-unsafe.c @@ -0,0 +1,16 @@ +#include + +int main(void) { + unsigned n = 1; + unsigned sum = 0; + + while (n <= N) + { + sum = sum + n; + n = n + 1; + } + + assert(sum != ((N * (N + 1)) / 2)); + + return 0; +} diff --git a/regression/symex-shortest-path/concrete-sum/main.c b/regression/symex-shortest-path/concrete-sum/main.c new file mode 100644 index 0000000..163066e --- /dev/null +++ b/regression/symex-shortest-path/concrete-sum/main.c @@ -0,0 +1,21 @@ +#include + +#define N 40000 + +// conservatively safe for N <= 46340 +int main(void) { + unsigned n = 1; + unsigned sum = 0; + + while (n <= N) + { + sum = sum + n; + n = n + 1; + } + +//#ifndef FORCE_BRANCH + assert(sum == ((N * (N + 1)) / 2)); +//#endif + + return 0; +} diff --git a/regression/symex-shortest-path/concrete-sum/test.desc b/regression/symex-shortest-path/concrete-sum/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/concrete-sum/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/counter-unsafe/main.c b/regression/symex-shortest-path/counter-unsafe/main.c new file mode 100644 index 0000000..9094590 --- /dev/null +++ b/regression/symex-shortest-path/counter-unsafe/main.c @@ -0,0 +1,39 @@ +// Similar to SV-COMP'14 (loops/count_up_down_false.c) except +// that we use explicit signedness constraints to support +// benchmarks with tools that are not bit precise. + +#include + +#define N 10 +#define ENABLE_CPROVER + +#ifdef ENABLE_KLEE +#include +#endif + +#ifdef ENABLE_CPROVER +int nondet_int(); +#endif + +// It suffices to unwind N times +int main() { +#ifdef ENABLE_CPROVER + int n = nondet_int(); + __CPROVER_assume(0 <= n && n < N); +#elif ENABLE_KLEE + int n; + klee_make_symbolic(&n, sizeof(n), "n"); + if (0 > n) + return 0; + if (n >= N) + return 0; +#endif + + int x = n, y = 0; + while (x > 0) { + x = x - 1; + y = y + 1; + } + assert(0 <= y && y != n); + return 0; +} diff --git a/regression/symex-shortest-path/counter-unsafe/test.desc b/regression/symex-shortest-path/counter-unsafe/test.desc new file mode 100644 index 0000000..510460c --- /dev/null +++ b/regression/symex-shortest-path/counter-unsafe/test.desc @@ -0,0 +1,6 @@ +CORE +main.c + +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/for-loop/main.c b/regression/symex-shortest-path/for-loop/main.c new file mode 100644 index 0000000..a3ba7e4 --- /dev/null +++ b/regression/symex-shortest-path/for-loop/main.c @@ -0,0 +1,13 @@ +void main() +{ + int i,x,y=0,z=0; + for(i=0;i < 10;++i) + //while(1) + { + if(x) + y++; + else + z++; + } + assert(1); +} diff --git a/regression/symex-shortest-path/for-loop/test.desc b/regression/symex-shortest-path/for-loop/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/for-loop/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/function_pointer1/main.c b/regression/symex-shortest-path/function_pointer1/main.c new file mode 100644 index 0000000..debb8e8 --- /dev/null +++ b/regression/symex-shortest-path/function_pointer1/main.c @@ -0,0 +1,32 @@ +#include + +void (*f_ptr)(void); + +int global; + +void f1(void) +{ + global=1; +} + +void f2(void) +{ + global=2; +} + +int main() +{ + int input; + + f_ptr=f1; + f_ptr(); +// assert(global==1); + + f_ptr=f2; + f_ptr(); +// assert(global==2); + + f_ptr=input?f1:f2; + f_ptr(); + assert(global==(input?1:2)); +} diff --git a/regression/symex-shortest-path/function_pointer1/test.desc b/regression/symex-shortest-path/function_pointer1/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/function_pointer1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/insertion-sort-unsafe/main.c b/regression/symex-shortest-path/insertion-sort-unsafe/main.c new file mode 100644 index 0000000..21960ff --- /dev/null +++ b/regression/symex-shortest-path/insertion-sort-unsafe/main.c @@ -0,0 +1,47 @@ +// This file contains modified code snippets from "Algorithms in C, Third Edition, +// Parts 1-4," by Robert Sedgewick. The code is intentionally buggy! +// +// For the correct code, see https://www.cs.princeton.edu/~rs/Algs3.c1-4/code.txt + +#include + +#define N 5 + + +#ifdef ENABLE_KLEE +#include +#endif + +typedef int Item; +#define key(A) (A) +#define less(A, B) (key(A) < key(B)) +#define exch(A, B) { Item t = A; A = B; B = t; } +#define compexch(A, B) if (less(B, A)) exch(A, B) + +void insertion_sort(Item a[], int l, int r) { + int i; + for (i = l+1; i <= r; i++) compexch(a[l], a[i]); + for (i = l+2; i <= r; i++) { + int j = i; Item v = a[i]; + while (0 < j && less(v, a[j-1])) { + a[j] = a[j]; j--; + // ^ bug due to wrong index (it should be j-1) + } + a[j] = v; + } +} + +// To find bug, let N >= 4. +int main() { + int a[N]; + +#ifdef ENABLE_KLEE + klee_make_symbolic(a, sizeof(a), "a"); +#endif + + insertion_sort(a, 0, N-1); + for (unsigned i = 0; i < N - 1; i++) + assert(a[i] <= a[i+1]); + + return 0; +} diff --git a/regression/symex-shortest-path/insertion-sort-unsafe/test.desc b/regression/symex-shortest-path/insertion-sort-unsafe/test.desc new file mode 100644 index 0000000..510460c --- /dev/null +++ b/regression/symex-shortest-path/insertion-sort-unsafe/test.desc @@ -0,0 +1,6 @@ +CORE +main.c + +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/modulus-safe/main.c b/regression/symex-shortest-path/modulus-safe/main.c new file mode 100644 index 0000000..c2d0d52 --- /dev/null +++ b/regression/symex-shortest-path/modulus-safe/main.c @@ -0,0 +1,38 @@ +#include + +#define N 20 + +#define ENABLE_CPROVER +#ifdef ENABLE_KLEE +#include +#endif + +#ifdef ENABLE_CPROVER +int nondet_int(); +#endif + +int main(void) { +#ifdef ENABLE_CPROVER + int k = nondet_int(); + __CPROVER_assume(0 <= k && k < 7); +#elif ENABLE_KLEE + int k; + klee_make_symbolic(&k, sizeof(k), "k"); + + if (0 > k) + return 0; + if (k >= 7) + return 0; +#endif + + for(int n = 0; n < N; n = n + 1) { + if(k == 7) { + k = 0; + } + k = k + 1; + } + +#ifndef FORCE_BRANCH + assert(k <= 7); +#endif +} diff --git a/regression/symex-shortest-path/modulus-safe/test.desc b/regression/symex-shortest-path/modulus-safe/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/modulus-safe/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/modulus-unsafe/main.c b/regression/symex-shortest-path/modulus-unsafe/main.c new file mode 100644 index 0000000..ebe9be3 --- /dev/null +++ b/regression/symex-shortest-path/modulus-unsafe/main.c @@ -0,0 +1,31 @@ +#include + +#define N 20 + + +#define ENABLE_CPROVER +#ifdef ENABLE_KLEE +#include +#endif + +#ifdef ENABLE_CPROVER +int nondet_int(); +#endif + +int main(void) { +#ifdef ENABLE_CPROVER + int k = nondet_int(); +#elif ENABLE_KLEE + int k; + klee_make_symbolic(&k, sizeof(k), "k"); +#endif + + for(int n = 0; n < N; n = n + 1) { + if(k == 7) { + k = 0; + } + k = k + 1; + } + + assert(k <= 7); +} diff --git a/regression/symex-shortest-path/modulus-unsafe/test.desc b/regression/symex-shortest-path/modulus-unsafe/test.desc new file mode 100644 index 0000000..510460c --- /dev/null +++ b/regression/symex-shortest-path/modulus-unsafe/test.desc @@ -0,0 +1,6 @@ +CORE +main.c + +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/pointer2/main.c b/regression/symex-shortest-path/pointer2/main.c new file mode 100644 index 0000000..bc6f95a --- /dev/null +++ b/regression/symex-shortest-path/pointer2/main.c @@ -0,0 +1,31 @@ +#include + +struct S1 +{ + char ch0, ch1, ch2, ch3; +} my_struct1; + +struct S2 +{ + int i1, i2; +} my_struct2; + +int main() +{ + // a pointer into a struct + int *p=(int *)&my_struct1; + + *p=0x03020100; + + // endianness-dependent + // assert(my_struct1.ch0==0); + // assert(my_struct1.ch1==1); + // assert(my_struct1.ch2==2); + // assert(my_struct1.ch3==3); + + // same bigger + long long int *q=(long long int *)&my_struct2; + *q=0x200000001ull; +// assert(my_struct2.i1==1); + assert(my_struct2.i2==2); +} diff --git a/regression/symex-shortest-path/pointer2/test.desc b/regression/symex-shortest-path/pointer2/test.desc new file mode 100644 index 0000000..9845e70 --- /dev/null +++ b/regression/symex-shortest-path/pointer2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--little-endian +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/pointer3/main.c b/regression/symex-shortest-path/pointer3/main.c new file mode 100644 index 0000000..65ef310 --- /dev/null +++ b/regression/symex-shortest-path/pointer3/main.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int choice; + int x=1, y=2, *p=choice?&x:&y; + + *p=3; + + if(choice) + assert(x==3 && y==2); +// else + // assert(x==1 && y==3); +} diff --git a/regression/symex-shortest-path/pointer3/test.desc b/regression/symex-shortest-path/pointer3/test.desc new file mode 100644 index 0000000..9845e70 --- /dev/null +++ b/regression/symex-shortest-path/pointer3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--little-endian +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/show-trace1/main.c b/regression/symex-shortest-path/show-trace1/main.c new file mode 100644 index 0000000..3b21655 --- /dev/null +++ b/regression/symex-shortest-path/show-trace1/main.c @@ -0,0 +1,15 @@ +int input(); + +int main() +{ + int i, j, k; + + i=input(); // expect 2 + j=input(); // expect 3 + k=input(); // expect 6 + + if(i==2) + if(j==i+1) + if(k==i*j) + __CPROVER_assert(0, ""); +} diff --git a/regression/symex-shortest-path/show-trace1/test.desc b/regression/symex-shortest-path/show-trace1/test.desc new file mode 100644 index 0000000..930f344 --- /dev/null +++ b/regression/symex-shortest-path/show-trace1/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--trace +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +^ i=2 .*$ +^ j=3 .*$ +^ k=6 .*$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/stop-on-fail1/main.c b/regression/symex-shortest-path/stop-on-fail1/main.c new file mode 100644 index 0000000..4c51c77 --- /dev/null +++ b/regression/symex-shortest-path/stop-on-fail1/main.c @@ -0,0 +1,12 @@ +#include + +int main() +{ + assert(0); + unsigned count=0; + while(count!=10) + { + // merry go around + } + +} diff --git a/regression/symex-shortest-path/stop-on-fail1/test.desc b/regression/symex-shortest-path/stop-on-fail1/test.desc new file mode 100644 index 0000000..fef4ac2 --- /dev/null +++ b/regression/symex-shortest-path/stop-on-fail1/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--stop-on-fail +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +^\[main.assertion.1\] assertion 0: FAILURE$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/struct1/main.c b/regression/symex-shortest-path/struct1/main.c new file mode 100644 index 0000000..3664bd6 --- /dev/null +++ b/regression/symex-shortest-path/struct1/main.c @@ -0,0 +1,25 @@ +#include + +struct inner_struct +{ + int a, b, c; +}; + +struct top_level +{ + int x, y, z; + struct inner_struct inner; +}; + +struct top_level my_s = { 1, 2, 3, 4, 5, 6 }; +struct inner_struct my_inner; + +int main() +{ +// assert(my_s.inner.a==4); +// assert(my_inner.a==0); + my_inner.a++; +// assert(my_inner.a==1); + my_s.inner=my_inner; // assigns all of 'inner' + assert(my_s.inner.a==1); +} diff --git a/regression/symex-shortest-path/struct1/test.desc b/regression/symex-shortest-path/struct1/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/struct1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/struct2/main.c b/regression/symex-shortest-path/struct2/main.c new file mode 100644 index 0000000..a0781a6 --- /dev/null +++ b/regression/symex-shortest-path/struct2/main.c @@ -0,0 +1,18 @@ +#include + +struct X +{ + int a, b; +} x; + +int main() +{ + int *p; + + p=&x.a; + *p=10; + p++; + *p=11; + + assert(x.a==10 && x.b==11); +} diff --git a/regression/symex-shortest-path/struct2/test.desc b/regression/symex-shortest-path/struct2/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/struct2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/struct3/main.c b/regression/symex-shortest-path/struct3/main.c new file mode 100644 index 0000000..c4363dc --- /dev/null +++ b/regression/symex-shortest-path/struct3/main.c @@ -0,0 +1,37 @@ +#include + +struct S +{ + char a, b, c, d; +} x, y; + +int main() +{ + int i; + char *p; + + p=&x.a; + + p[0]=1; + p[1]=2; + p[2]=3; + p[3]=4; + +// assert(x.a==1); +// assert(x.b==2); +// assert(x.c==3); +// assert(x.d==4); + + // same again, directly to head of struct + p=(char *)&y; + + p[0]=1; + p[1]=2; + p[2]=3; + p[3]=4; + +// assert(y.a==1); +// assert(y.b==2); +// assert(y.c==3); + assert(y.d==4); +} diff --git a/regression/symex-shortest-path/struct3/test.desc b/regression/symex-shortest-path/struct3/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/struct3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/tp1/main.c b/regression/symex-shortest-path/tp1/main.c new file mode 100644 index 0000000..944569e --- /dev/null +++ b/regression/symex-shortest-path/tp1/main.c @@ -0,0 +1,127 @@ +struct state_element_f{ + unsigned int x; // Mode Variable + unsigned int diff; + unsigned int add; +}; + +unsigned int f(unsigned int t, struct state_element_f stf) +{ + unsigned int m1; + if(t>=1 && t<=5) { + //t=1; //extra logic + stf.diff=1; + m1=1; + } + else if(t>5 && t<=10){ + //t=2; //extra logic + stf.add=1; + m1=0; + } + else if(t > 11 && t <= 20 ){ + t=3; //extra logic + stf.add=0; + m1=1; + } + else { } + return t; +} + +struct state_element_g{ + unsigned int y; // Mode Variable + unsigned int avg; + unsigned int sum; +}; + +void g(unsigned int z, struct state_element_g stg) +{ + unsigned int m2; + if(z >=1 && z <= 5) { + //z=1; //extra logic + stg.avg=1; + m2++; + } + else if(z>5 && z<=10){ + //z=2; //extra logic + stg.sum=1; + m2--; + + // redundant logic + if(m2==1) + m2*=2; + else + m2/=2; + } + else if(z>11 && z <= 20) { + z=3; //extra logic + stg.sum=0; + } + //********** + else {} + //********** +} + +void main() +{ + //******************************************************* + // Total Paths = 19, Feasible Path=3, Infeasible Path=16 + // ****************************************************** + + unsigned int m,n; + // Structures are passed as function arguments to build the harness + struct state_element_f stf; + struct state_element_g stg; + //__CPROVER_assume(0); + // Identify and bind equivalent signals in both design to allow partitioning + /*if(nondet_bool()) + { + m=1; + n=1; + } + else if(nondet_bool()) + { + m=2; + n=2; + } + else if(nondet_bool()) + { + m=3; + n=3; + } + else { + __CPROVER_assume(m==n); + }*/ +// __CPROVER_assume(m==n); + m=nondet_unsigned(); + n=f(m,stf); + //n=m; + g(n,stg); + assert(1); + //**************************************************** + + //***************************************************** + // Total Paths = 16, Feasible Path=16, Infeasible Path=0 + // **************************************************** + /*unsigned int m; + // Structures are passed as function arguments to build the harness + struct state_element_f stf; + struct state_element_g stg; + f(m,stf); + g(m,stg); + assert(1);*/ + //**************************************************** + + //***************************************************************************** + // When the last else of g() contains the extra code of if-else statement, then + // Total Paths = 44, Feasible Path=1, Infeasible Path=43 + // **************************************************************************** + /*unsigned int m; + // Structures are passed as function arguments to build the harness + struct state_element_f stf; + struct state_element_g stg; + // Identify and bind equivalent signals in both design to allow partitioning + __CPROVER_assume(stf.x == 1 && stg.y == 1); + f(m,stf); + g(m,stg); + assert(1);*/ + //**************************************************** +} diff --git a/regression/symex-shortest-path/tp1/test.desc b/regression/symex-shortest-path/tp1/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/tp1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/tp2/main.c b/regression/symex-shortest-path/tp2/main.c new file mode 100644 index 0000000..141cbde --- /dev/null +++ b/regression/symex-shortest-path/tp2/main.c @@ -0,0 +1,57 @@ +struct state_element_f{ + unsigned int x; + unsigned int diff; + unsigned int add; +}; + +unsigned int f(unsigned int t, struct state_element_f stf) +{ + unsigned int m1; + if(t>1) { + stf.x=1; + stf.diff=1; + m1=1; + } + else { + stf.add=1; + m1=0; + } + return t; +} + +struct state_element_g{ + unsigned int y; + unsigned int avg; + unsigned int sum; +}; + +void g(unsigned int k, struct state_element_g stg) +{ + unsigned int m2; + if(k>1) { + stg.y=1; + stg.avg=1; + m2++; + } + else { + stg.sum=1; + m2--; + } +} + +void main() +{ + //***************************************************** + // Total Paths = 2, Feasible Path=2, Infeasible Path=0 + // **************************************************** + unsigned int m, n; + // Structures are passed as function arguments to build the harness + struct state_element_f stf; + struct state_element_g stg; + // Identify and bind equivalent signals in both design to allow partitioning + m=nondet_unsigned(); + n=f(m,stf); + g(n,stg); + assert(1); + //**************************************************** +} diff --git a/regression/symex-shortest-path/tp2/test.desc b/regression/symex-shortest-path/tp2/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/tp2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/tp3/main.c b/regression/symex-shortest-path/tp3/main.c new file mode 100644 index 0000000..3019b11 --- /dev/null +++ b/regression/symex-shortest-path/tp3/main.c @@ -0,0 +1,129 @@ +struct state_element_f{ + unsigned int x; // Mode Variable + unsigned int diff; + unsigned int add; +}; + +unsigned int f(unsigned int t, struct state_element_f stf) +{ + unsigned int m1; + if(t==1) { + //t=1; //extra logic + stf.diff=1; + m1=1; + } + else if(t==2){ + //t=2; //extra logic + stf.add=1; + m1=0; + } + else if(t==3){ + //t=3; //extra logic + stf.add=0; + m1=1; + } + else { }; //t= 4; } + return t; +} + +struct state_element_g{ + unsigned int y; // Mode Variable + unsigned int avg; + unsigned int sum; +}; + +void g(unsigned int z, struct state_element_g stg) +{ + unsigned int m2; + if(z==1) { + z=1; //extra logic + stg.avg=1; + m2++; + } + else if(z==2){ + z=2; //extra logic + stg.sum=1; + m2--; + + // redundant logic + if(m2==1) + m2*=2; + else + m2/=2; + } + else if(z==3) { + z=3; //extra logic + stg.sum=0; + } + //********** + else { + z = 4; + } + //********** +} + +void main() +{ + //******************************************************* + // Total Paths = 19, Feasible Path=3, Infeasible Path=16 + // ****************************************************** + + unsigned int m,n; + // Structures are passed as function arguments to build the harness + struct state_element_f stf; + struct state_element_g stg; + //__CPROVER_assume(0); + // Identify and bind equivalent signals in both design to allow partitioning + /*if(nondet_bool()) + { + m=1; + n=1; + } + else if(nondet_bool()) + { + m=2; + n=2; + } + else if(nondet_bool()) + { + m=3; + n=3; + } + else { + __CPROVER_assume(m==n); + }*/ +// __CPROVER_assume(m==n); + m=nondet_unsigned(); + n=f(m,stf); + //n=m; + g(n,stg); + assert(1); + //**************************************************** + + //***************************************************** + // Total Paths = 16, Feasible Path=16, Infeasible Path=0 + // **************************************************** + /*unsigned int m; + // Structures are passed as function arguments to build the harness + struct state_element_f stf; + struct state_element_g stg; + f(m,stf); + g(m,stg); + assert(1);*/ + //**************************************************** + + //***************************************************************************** + // When the last else of g() contains the extra code of if-else statement, then + // Total Paths = 44, Feasible Path=1, Infeasible Path=43 + // **************************************************************************** + /*unsigned int m; + // Structures are passed as function arguments to build the harness + struct state_element_f stf; + struct state_element_g stg; + // Identify and bind equivalent signals in both design to allow partitioning + __CPROVER_assume(stf.x == 1 && stg.y == 1); + f(m,stf); + g(m,stg); + assert(1);*/ + //**************************************************** +} diff --git a/regression/symex-shortest-path/tp3/test.desc b/regression/symex-shortest-path/tp3/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/tp3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/tp4/main.c b/regression/symex-shortest-path/tp4/main.c new file mode 100644 index 0000000..f41600d --- /dev/null +++ b/regression/symex-shortest-path/tp4/main.c @@ -0,0 +1,60 @@ +struct state_element_f{ + unsigned int x; + unsigned int diff; + unsigned int add; +}; + +unsigned int f(unsigned int t, struct state_element_f stf) +{ + unsigned int m1; + if(t==1) { + //t=1; + stf.x=1; + stf.diff=1; + m1=1; + } + else { + //t=2; + stf.add=1; + m1=0; + } + return t; +} + +struct state_element_g{ + unsigned int y; + unsigned int avg; + unsigned int sum; +}; + +void g(unsigned int k, struct state_element_g stg) +{ + unsigned int m2; + if(k==1) { + stg.y=1; + stg.avg=1; + m2++; + } + else { + stg.sum=1; + m2--; + } +} + +void main() +{ + //***************************************************** + // Total Paths = 2, Feasible Path=2, Infeasible Path=0 + // **************************************************** + unsigned int m, n; + // Structures are passed as function arguments to build the harness + struct state_element_f stf; + struct state_element_g stg; + // Identify and bind equivalent signals in both design to allow partitioning + m=nondet_unsigned(); + //__CPROVER_assume(m==n); + n=f(m,stf); + g(n,stg); + assert(1); + //**************************************************** +} diff --git a/regression/symex-shortest-path/tp4/test.desc b/regression/symex-shortest-path/tp4/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/tp4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/va_args_1/main.c b/regression/symex-shortest-path/va_args_1/main.c new file mode 100644 index 0000000..d877803 --- /dev/null +++ b/regression/symex-shortest-path/va_args_1/main.c @@ -0,0 +1,37 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + + int y = 7; + int u = 2; + m = max(3, y, u, 9); + + assert(m == 9); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex-shortest-path/va_args_1/test.desc b/regression/symex-shortest-path/va_args_1/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/va_args_1/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/va_args_10/main.c b/regression/symex-shortest-path/va_args_10/main.c new file mode 100644 index 0000000..554187f --- /dev/null +++ b/regression/symex-shortest-path/va_args_10/main.c @@ -0,0 +1,41 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + int m2; + int m3; + + m = max(3, 2, 6, 9); + + m2 = max(3, 4, 11, 1); + + m3 = max(2, m, m2); + + assert(m3 == 6); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex-shortest-path/va_args_10/test.desc b/regression/symex-shortest-path/va_args_10/test.desc new file mode 100644 index 0000000..6de7955 --- /dev/null +++ b/regression/symex-shortest-path/va_args_10/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/va_args_11/main.c b/regression/symex-shortest-path/va_args_11/main.c new file mode 100644 index 0000000..d9e0b81 --- /dev/null +++ b/regression/symex-shortest-path/va_args_11/main.c @@ -0,0 +1,29 @@ +#include +#include +#include + +void foo(int n, ...); + +int main() +{ + foo(1, 1u); + foo(2, 2l); + foo(3, 3.0); + return 0; +} + +void foo(int n, ...) +{ + va_list vl; + + va_start(vl,n); + + switch(n) + { + case 1: assert(va_arg(vl, unsigned)==1); break; + case 2: break; + case 3: break; + } + + va_end(vl); +} diff --git a/regression/symex-shortest-path/va_args_11/test.desc b/regression/symex-shortest-path/va_args_11/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/va_args_11/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/va_args_2/main.c b/regression/symex-shortest-path/va_args_2/main.c new file mode 100644 index 0000000..2a35ca4 --- /dev/null +++ b/regression/symex-shortest-path/va_args_2/main.c @@ -0,0 +1,35 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + int y; + m = max(2, y, 8); + + assert(m == 8); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex-shortest-path/va_args_2/test.desc b/regression/symex-shortest-path/va_args_2/test.desc new file mode 100644 index 0000000..6de7955 --- /dev/null +++ b/regression/symex-shortest-path/va_args_2/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/va_args_3/main.c b/regression/symex-shortest-path/va_args_3/main.c new file mode 100644 index 0000000..148d705 --- /dev/null +++ b/regression/symex-shortest-path/va_args_3/main.c @@ -0,0 +1,34 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + m = max(2, 1, 8); + + assert(m == 1); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex-shortest-path/va_args_3/test.desc b/regression/symex-shortest-path/va_args_3/test.desc new file mode 100644 index 0000000..6de7955 --- /dev/null +++ b/regression/symex-shortest-path/va_args_3/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/va_args_4/main.c b/regression/symex-shortest-path/va_args_4/main.c new file mode 100644 index 0000000..4a19acf --- /dev/null +++ b/regression/symex-shortest-path/va_args_4/main.c @@ -0,0 +1,38 @@ +#include +#include +#include + +int max(int n, ...); + +int main() +{ + int m; + m = max(2, 2, 8, 10); + + assert(m == 10); + + return 0; +} + +int max(int repeat,int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + for (i = 0; i < repeat; i++){ + printf("%d. Result is: %d", i, largest); + } + + va_end(vl); + return largest; +} diff --git a/regression/symex-shortest-path/va_args_4/test.desc b/regression/symex-shortest-path/va_args_4/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/va_args_4/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/va_args_5/main.c b/regression/symex-shortest-path/va_args_5/main.c new file mode 100644 index 0000000..a1e4d6a --- /dev/null +++ b/regression/symex-shortest-path/va_args_5/main.c @@ -0,0 +1,35 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int n; + int m; + m = max(7, 7, 8); + + assert(m == 8); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex-shortest-path/va_args_5/test.desc b/regression/symex-shortest-path/va_args_5/test.desc new file mode 100644 index 0000000..b69d21c --- /dev/null +++ b/regression/symex-shortest-path/va_args_5/test.desc @@ -0,0 +1,6 @@ +CORE +main.c + +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/regression/symex-shortest-path/va_args_6/main.c b/regression/symex-shortest-path/va_args_6/main.c new file mode 100644 index 0000000..191435f --- /dev/null +++ b/regression/symex-shortest-path/va_args_6/main.c @@ -0,0 +1,34 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + m = max(8, 2, 7, 8); + + assert(m == 2); + + return 0; +} + +int max (int j, int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex-shortest-path/va_args_6/test.desc b/regression/symex-shortest-path/va_args_6/test.desc new file mode 100644 index 0000000..9431f04 --- /dev/null +++ b/regression/symex-shortest-path/va_args_6/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--unwind 8 +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/regression/symex-shortest-path/va_args_7/main.c b/regression/symex-shortest-path/va_args_7/main.c new file mode 100644 index 0000000..cecc1bf --- /dev/null +++ b/regression/symex-shortest-path/va_args_7/main.c @@ -0,0 +1,23 @@ +#include +#include +#include + +int main () +{ + + int eva_arguments; + int n; + + int init_eva = eva_arguments; + + for (unsigned int i = 0; i < n; i++){ + + eva_arguments++; + } + + if (init_eva == 0){ + assert(eva_arguments == n); + } + + return 0; +} diff --git a/regression/symex-shortest-path/va_args_7/test.desc b/regression/symex-shortest-path/va_args_7/test.desc new file mode 100644 index 0000000..832e94e --- /dev/null +++ b/regression/symex-shortest-path/va_args_7/test.desc @@ -0,0 +1,6 @@ +CORE +main.c +--unwind 8 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/regression/symex-shortest-path/va_args_8/main.c b/regression/symex-shortest-path/va_args_8/main.c new file mode 100644 index 0000000..90e2031 --- /dev/null +++ b/regression/symex-shortest-path/va_args_8/main.c @@ -0,0 +1,37 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + + int y = 7; + int u = 2; + m = max(3, y, u, 9); + + assert(m == 10); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int) + 1; + + for (i=1;ival)?largest:val; + } + + va_end(vl); + return largest; +} diff --git a/regression/symex-shortest-path/va_args_8/test.desc b/regression/symex-shortest-path/va_args_8/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/va_args_8/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/regression/symex-shortest-path/va_args_9/main.c b/regression/symex-shortest-path/va_args_9/main.c new file mode 100644 index 0000000..4c9d52b --- /dev/null +++ b/regression/symex-shortest-path/va_args_9/main.c @@ -0,0 +1,41 @@ +#include +#include +#include + +int max(int n, ...); + +int main () +{ + int m; + int m2; + int m3; + + m = max(3, 2, 6, 9); + m2 = max(3, 4, 11, 1); + + m3 = max(2, m, m2); + + assert(m3 == 11); + + return 0; +} + +int max(int n, ...) +{ + int i,val,largest; + + va_list vl; + + va_start(vl,n); + largest=va_arg(vl,int); + + for (i=1;ival)?largest:val; + } + + va_end(vl); + + return largest; +} diff --git a/regression/symex-shortest-path/va_args_9/test.desc b/regression/symex-shortest-path/va_args_9/test.desc new file mode 100644 index 0000000..9efefbc --- /dev/null +++ b/regression/symex-shortest-path/va_args_9/test.desc @@ -0,0 +1,8 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring diff --git a/src/path-symex/locs.cpp b/src/path-symex/locs.cpp index 8f6dd19..bcd4eaf 100644 --- a/src/path-symex/locs.cpp +++ b/src/path-symex/locs.cpp @@ -82,23 +82,60 @@ void locst::build(const goto_functionst &goto_functions) } } +void locst::output_reachable(std::ostream &out) const +{ + irep_idt function; + int reachable_count = 0; + int unreachable_count = 0; + + for(unsigned l = 0; l < loc_vector.size(); l++) + { + const loct &loc = loc_vector[l]; + if(loc.distance_to_property != -1) + { + reachable_count++; + if(function != loc.function) + { + function = loc.function; + out << "*** " << function << "\n"; + } + + out << " L" << l << ": " << " " << as_string(ns, *loc.target) + << " path length: " << loc_vector[l].distance_to_property << "\n"; + + if(!loc.branch_target.is_nil()) + out << " T: " << loc.branch_target << "\n"; + } + else + unreachable_count++; + } + out << "\n"; + out << "The entry location is L" << entry_loc << ".\n"; + out << "Number of reachable locs " << reachable_count << "\n"; + out << "Number of unreachable locs " << unreachable_count << "\n"; +} + void locst::output(std::ostream &out) const { irep_idt function; - for(unsigned l=0; ltype << " " // << loc.target->location - << " " << as_string(ns, *loc.target) << "\n"; + << " " << as_string(ns, *loc.target); + if(loc_vector[l].distance_to_property + != std::numeric_limits::max()) + out << " path length: " << loc_vector[l].distance_to_property; + out << "\n"; if(!loc.branch_target.is_nil()) out << " T: " << loc.branch_target << "\n"; diff --git a/src/path-symex/locs.h b/src/path-symex/locs.h index a7f54c9..1ec7c97 100644 --- a/src/path-symex/locs.h +++ b/src/path-symex/locs.h @@ -27,11 +27,12 @@ struct loct target(_target), function(_function) { + distance_to_property=std::numeric_limits::max(); } goto_programt::const_targett target; irep_idt function; - + std::size_t distance_to_property; // we only support a single branch target loc_reft branch_target; }; @@ -58,6 +59,7 @@ class locst explicit locst(const namespacet &_ns); void build(const goto_functionst &goto_functions); void output(std::ostream &out) const; + void output_reachable(std::ostream &out) const; loct &operator[] (loc_reft l) { diff --git a/src/path-symex/path_symex_state.h b/src/path-symex/path_symex_state.h index fc3597d..3b042ff 100644 --- a/src/path-symex/path_symex_state.h +++ b/src/path-symex/path_symex_state.h @@ -208,6 +208,11 @@ struct path_symex_statet return depth; } + unsigned get_shortest_path() const + { + return locs.loc_vector[pc().loc_number].distance_to_property; + } + void increase_depth() { depth++; diff --git a/src/symex/Makefile b/src/symex/Makefile index b14e327..3c94eee 100644 --- a/src/symex/Makefile +++ b/src/symex/Makefile @@ -2,6 +2,7 @@ SRC = path_search.cpp \ symex_cover.cpp \ symex_main.cpp \ symex_parse_options.cpp \ + shortest_path_graph.cpp \ # Empty last line OBJ += ../../$(CPROVER_DIR)/src/ansi-c/ansi-c$(LIBEXT) \ diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp index 18106ae..ca3a6a3 100644 --- a/src/symex/path_search.cpp +++ b/src/symex/path_search.cpp @@ -20,6 +20,106 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "shortest_path_graph.h" + +#include + + +void path_searcht::sort_queue() +{ + debug()<< " get shortest path, queue.size = " <::max(); + + std::list::iterator it; + std::list::iterator closest_state; + + for(it=queue.begin(); it!=queue.end(); ++it) + { + if(it->get_shortest_path() < shortest_path) + { + shortest_path = it->get_shortest_path(); + closest_state = it; + } + } + + if(shortest_path != std::numeric_limits::max()) + { + current_distance = shortest_path; + statet tmp = *closest_state; + queue.erase(closest_state); + queue.push_front(tmp); + } + else + { + error() << "all states have shortest path length = MAX_UNSIGNED_INT, " + << "try removing function pointers with goto-instrument next time." + << "randomly picking state instead" + << eom; + shuffle_queue(queue); + } +} + +// We prioritise remaining in the same function, but if there is no choice +// we take the next state with the shortest path +void path_searcht::sort_queue_per_function() +{ + debug()<< " get shortest path, queue.size = " <::max(); + + std::list::iterator it; + std::list::iterator closest_state; + + // pick the first state in the queue that is a direct successor, i.e., + // has a path length 1 less than the current path length + for(it=queue.begin(); it!=queue.end(); ++it) + { + if(it->get_shortest_path()+1 == current_distance) + { + shortest_path = it->get_shortest_path(); + current_distance = shortest_path; + statet tmp = *it; + queue.erase(it); + queue.push_front(tmp); + return; + } + } + + // if we get here there was no direct successor, we revert to + // picking the shortest path + sort_queue(); +} + +void path_searcht::shuffle_queue(queuet &queue) +{ + if(queue.size()<=1) + return; + + INVARIANT(queue.size()::max(), + "Queue size must be less than maximum integer"); + // pick random state and move to front + int rand_i = rand() % queue.size(); + + std::list::iterator it = queue.begin(); + for(int i=0; i::max(); number_of_dropped_states=0; number_of_paths=0; number_of_VCCs=0; @@ -51,6 +175,26 @@ path_searcht::resultt path_searcht::operator()( absolute_timet last_reported_time=start_time; initialize_property_map(goto_functions); + if(search_heuristic == search_heuristict::SHORTEST_PATH || + search_heuristic == search_heuristict::RAN_SHORTEST_PATH ) + { + status()<<"Building shortest path graph" << eom; + shortest_path_grapht shortest_path_graph(goto_functions, locs); + } + else if(search_heuristic == search_heuristict::SHORTEST_PATH_PER_FUNC) + { + status()<<"Building shortest path graph per function" << eom; + per_function_shortest_patht shortest_path_graph(goto_functions, locs); + } + + statet init_state = initial_state(var_map, locs, history); + queue.push_back(init_state); + initial_distance_to_property=init_state.get_shortest_path(); + + time_periodt initialisation_time=current_time()-start_time; + status() << "Initialisation took "<< initialisation_time << "s" << eom; + start_time=current_time(); + last_reported_time=start_time; while(!queue.empty()) { @@ -114,8 +258,13 @@ path_searcht::resultt path_searcht::operator()( << " thread " << state.get_current_thread()+1 << '/' << state.threads.size() << " PC " << state.pc() - << " depth " << state.get_depth() - << " [" << number_of_steps << " steps, " + << " depth " << state.get_depth(); + + if(search_heuristic == search_heuristict::SHORTEST_PATH + || search_heuristic == search_heuristict::RAN_SHORTEST_PATH) + status() << " distance to property " << state.get_shortest_path(); + + status() << " [" << number_of_steps << " steps, " << running_time << "s]" << messaget::eom; } } @@ -142,6 +291,9 @@ path_searcht::resultt path_searcht::operator()( // execute path_symex(state, tmp_queue); + if(search_heuristic == search_heuristict::RAN_DFS) + shuffle_queue(tmp_queue); + // put at head of main queue queue.splice(queue.begin(), tmp_queue); } @@ -208,6 +360,7 @@ void path_searcht::pick_state() switch(search_heuristic) { case search_heuristict::DFS: + case search_heuristict::RAN_DFS: // Picking the first one (most recently added) is a DFS. return; @@ -218,6 +371,18 @@ void path_searcht::pick_state() queue.splice(queue.begin(), queue, --queue.end(), queue.end()); return; + case search_heuristict::RAN_SHORTEST_PATH: + if(number_of_steps%1000==0) + shuffle_queue(queue); + else + sort_queue(); + return; + case search_heuristict::SHORTEST_PATH: + sort_queue(); + return; + case search_heuristict::SHORTEST_PATH_PER_FUNC: + sort_queue_per_function(); + return; case search_heuristict::LOCS: return; } diff --git a/src/symex/path_search.h b/src/symex/path_search.h index 9920723..4a112a8 100644 --- a/src/symex/path_search.h +++ b/src/symex/path_search.h @@ -80,6 +80,8 @@ class path_searcht:public safety_checkert bool stop_on_fail; // statistics + unsigned current_distance; + unsigned initial_distance_to_property; std::size_t number_of_dropped_states; std::size_t number_of_paths; std::size_t number_of_steps; @@ -107,8 +109,15 @@ class path_searcht:public safety_checkert }; void set_dfs() { search_heuristic=search_heuristict::DFS; } + void set_randomized_dfs() { search_heuristic=search_heuristict::RAN_DFS; } void set_bfs() { search_heuristic=search_heuristict::BFS; } void set_locs() { search_heuristic=search_heuristict::LOCS; } + void set_shortest_path() + { search_heuristic=search_heuristict::SHORTEST_PATH; } + void set_ran_shortest_path() + { search_heuristic=search_heuristict::RAN_SHORTEST_PATH; } + void set_shortest_path_per_function() + { search_heuristic=search_heuristict::SHORTEST_PATH_PER_FUNC; } typedef std::map property_mapt; property_mapt property_map; @@ -120,7 +129,13 @@ class path_searcht:public safety_checkert // The states most recently executed are at the head. typedef std::list queuet; queuet queue; - + /// Pick random element of queue and move to front + /// \param queue queue to be shuffled + void shuffle_queue(queuet &queue); + /// Move element with shortest distance to property + /// to the front of the queue + void sort_queue(); + void sort_queue_per_function(); // search heuristic void pick_state(); @@ -151,7 +166,9 @@ class path_searcht:public safety_checkert unsigned unwind_limit; unsigned time_limit; - enum class search_heuristict { DFS, BFS, LOCS } search_heuristic; + enum class search_heuristict + { DFS, RAN_DFS, BFS, LOCS, SHORTEST_PATH, + RAN_SHORTEST_PATH , SHORTEST_PATH_PER_FUNC } search_heuristic; source_locationt last_source_location; }; diff --git a/src/symex/shortest_path_graph.cpp b/src/symex/shortest_path_graph.cpp new file mode 100644 index 0000000..b1b6977 --- /dev/null +++ b/src/symex/shortest_path_graph.cpp @@ -0,0 +1,138 @@ +/*******************************************************************\ + +Module: Shortest path graph + +Author: elizabeth.polgreen@cs.ox.ac.uk + +\*******************************************************************/ + +#include "shortest_path_graph.h" + +#include + +void shortest_path_grapht::get_path_lengths_in_function() +{ + bool found_property = false; + bool found_end = false; + node_indext end_index; + node_indext property_index; + node_indext index = 0; + for(auto &n : nodes) + { + if(n.PC->is_assert()) + { + if(found_property == false) + { + n.is_property = true; + n.shortest_path_to_property = 0; + found_property = true; + property_index = index; + } + else + throw "shortest path search cannot be used with multiple properties"; + } + if(n.PC->is_end_function()) + { + end_index = index; + found_end = true; + } + index++; + } + + if(!found_property) + { + nodes[end_index].shortest_path_to_property = 0; + bfs(end_index); + } + else + bfs(property_index); + + write_lengths_to_locs(); +} + +void per_function_shortest_patht::build(const goto_functionst &goto_functions) +{ + forall_goto_functions(it, goto_functions) + if(it->second.body_available()) + { + shortest_path_grapht path_graph(it->second.body, locs); + } +} + +void shortest_path_grapht::bfs(node_indext property_index) +{ + // does BFS, not Dijkstra + // we hope the graph is sparse + std::vector frontier_set; + + frontier_set.reserve(nodes.size()); + + frontier_set.push_back(property_index); + nodes[property_index].visited = true; + + for(std::size_t d = 1; !frontier_set.empty(); ++d) + { + std::vector new_frontier_set; + + for(const auto &node_index : frontier_set) + { + const nodet &n = nodes[node_index]; + + // do all neighbors + // we go backwards through the graph + for(const auto &edge_in : n.in) + { + node_indext node_in = edge_in.first; + + if(!nodes[node_in].visited) + { + nodes[node_in].shortest_path_to_property = d; + nodes[node_in].visited = true; + new_frontier_set.push_back(node_in); + } + } + } + + frontier_set.swap(new_frontier_set); + } +} + +void shortest_path_grapht::write_lengths_to_locs() +{ + for(const auto &n : nodes) + { + loc_reft l = target_to_loc_map[n.PC]; + locs.loc_vector[l.loc_number].distance_to_property + = n.shortest_path_to_property; + } +} + +void shortest_path_grapht::get_path_lengths_to_property() +{ + node_indext property_index; + bool found_property=false; + for(node_indext n=0; nis_assert()) + { + if(found_property == false) + { + nodes[n].is_property = true; + nodes[n].shortest_path_to_property = 0; + working_set.insert(n); + property_index = n; + found_property = true; + } + else + throw "shortest path search cannot be used for multiple properties"; + } + } + if(!found_property) + throw "unable to find property"; + + bfs(property_index); + + write_lengths_to_locs(); +} + + diff --git a/src/symex/shortest_path_graph.h b/src/symex/shortest_path_graph.h new file mode 100644 index 0000000..9d1547e --- /dev/null +++ b/src/symex/shortest_path_graph.h @@ -0,0 +1,109 @@ +/*******************************************************************\ + +Module: Shortest path graph + +Author: elizabeth.polgreen@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_SYMEX_SHORTEST_PATH_GRAPH_H +#define CPROVER_SYMEX_SHORTEST_PATH_GRAPH_H + +#include +#include +#include +#include + + +struct shortest_path_nodet +{ + bool visited; + std::size_t shortest_path_to_property; + bool is_property; + shortest_path_nodet(): + visited(false), + is_property(false) + { + shortest_path_to_property = std::numeric_limits::max(); + } +}; + +/// \brief constructs a CFG of all program locations. Then computes +/// the shortest path from every program location to a single property. +/// WARNING: if more than one property is present in the graph, we will +/// use the first property found +/// The distances computed for each node are written to the corresponding +/// loct in the locst passed as param to the constructor. This allows us +/// to use these numbers to guide a symex search +/// \param goto functions to create the CFG from, locs struct made from the +/// same goto_functions +class shortest_path_grapht: public cfg_baset +{ +public: + explicit shortest_path_grapht( + const goto_functionst &_goto_functions, locst &_locs): + locs(_locs), + target_to_loc_map(_locs) + { + cfg_baset::operator()(_goto_functions); + get_path_lengths_to_property(); + } + + explicit shortest_path_grapht( + const goto_programt &_goto_program, locst &_locs): + locs(_locs), + target_to_loc_map(_locs) + { + cfg_baset::operator()(_goto_program); + get_path_lengths_in_function(); + } + +protected: + /// \brief writes the computed shortest path for every node + /// in the graph to the corresponding location in locst. + /// This is done so that we can use these numbers to guide + /// a search heuristic for symex + void write_lengths_to_locs(); + /// \brief computes the shortest path from every node in + /// the graph to a single property. WARNING: if more than one property + /// is present, we use the first one discovered. + /// Calls bfs() to do this. + void get_path_lengths_to_property(); + /// \brief computes the shortest path from every node in a + /// graph to the property, or the end of the funciton if + /// there is no property. + /// we assume the graph is a graph of a single function. + void get_path_lengths_in_function(); + /// \brief implements backwards BFS to compute distance from every node in + /// the graph to the node index given as parameter + /// \param destination node index + void bfs(node_indext property_index); + std::set working_set; + locst &locs; + target_to_loc_mapt target_to_loc_map; +}; + +/// \brief class contains CFG of program locations +/// for every function with the shortest distance to a +/// property, or the end of a function, calculated for each location +/// The distances computed for each node are written to the corresponding +/// loct in the locst passed as param to the constructor. This allows us +/// to use these numbers to guide a symex search +/// \param goto functions to create the CFGs from, locs struct made from the +/// same goto_functions +class per_function_shortest_patht +{ +public: + explicit per_function_shortest_patht( + const goto_functionst &_goto_functions, locst &_locs): + locs(_locs) + { + build(_goto_functions); + } + +protected: + locst &locs; + void build(const goto_functionst & goto_functions); +}; + +#endif /* CPROVER_SYMEX_SHORTEST_PATH_GRAPH_H */ diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp index d28b638..8542cb5 100644 --- a/src/symex/symex_parse_options.cpp +++ b/src/symex/symex_parse_options.cpp @@ -58,6 +58,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "path_search.h" +#include "shortest_path_graph.h" symex_parse_optionst::symex_parse_optionst(int argc, const char **argv): parse_options_baset(SYMEX_OPTIONS, argc, argv), @@ -202,6 +203,18 @@ int symex_parse_optionst::doit() return 0; } + if(cmdline.isset("show-distances-to-property")) + { + const namespacet ns(goto_model.symbol_table); + locst locs(ns); + locs.build(goto_model.goto_functions); + + shortest_path_grapht path_search_graph(goto_model.goto_functions, locs); + + locs.output_reachable(std::cout); + return 0; + } + // do actual Symex try @@ -232,7 +245,12 @@ int symex_parse_optionst::doit() safe_string2unsigned(cmdline.get_value("max-search-time"))); if(cmdline.isset("dfs")) - path_search.set_dfs(); + { + if(cmdline.isset("randomize")) + path_search.set_randomized_dfs(); + else + path_search.set_dfs(); + } if(cmdline.isset("bfs")) path_search.set_bfs(); @@ -240,6 +258,17 @@ int symex_parse_optionst::doit() if(cmdline.isset("locs")) path_search.set_locs(); + if(cmdline.isset("shortest-path")) + { + if(cmdline.isset("randomize")) + path_search.set_ran_shortest_path(); + else + path_search.set_shortest_path(); + } + + if(cmdline.isset("shortest-path-per-function")) + path_search.set_shortest_path_per_function(); + if(cmdline.isset("show-vcc")) { path_search.show_vcc=true; @@ -636,8 +665,17 @@ void symex_parse_optionst::help() " --context-bound nr limit number of context switches\n" " --branch-bound nr limit number of branches taken\n" " --max-search-time s limit search to approximately s seconds\n" + " --dfs use depth first search\n" + " --bfs use breadth first search\n" + "--shortest-path use shortest path guided search\n" + "--shortest-path-per-function computes shortest path locally and uses to guide symex search\n" // NOLINT(*) + " --randomize in conjunction with dfs to use randomized dfs\n" // NOLINT(*) + " in conjunction with shortest path to use randomized shortest path guided search\n" // NOLINT(*) + " --eager-infeasibility query solver early to determine whether a path is infeasible before searching it\n" // NOLINT(*) "\n" "Other options:\n" + " --show-distances-to-property\n" + " shows the (context free) shortest path from every reachable program location to a single property" // NOLINT(*) " --version show version and exit\n" " --xml-ui use XML-formatted output\n" " --verbosity # verbosity level\n" diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h index 99fd3f6..e55d6ee 100644 --- a/src/symex/symex_parse_options.h +++ b/src/symex/symex_parse_options.h @@ -40,7 +40,9 @@ class optionst; "(little-endian)(big-endian)" \ "(error-label):(verbosity):(no-library)" \ "(version)" \ - "(bfs)(dfs)(locs)" \ + "(bfs)(dfs)(locs)(shortest-path)" \ + "(shortest-path-per-function)" \ + "(randomize)" \ "(cover):" \ "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \ "(ppc-macos)(unsigned-char)" \ @@ -50,6 +52,7 @@ class optionst; "(show-locs)(show-vcc)(show-properties)(show-symbol-table)" \ "(drop-unused-functions)" \ "(object-bits):" \ + "(show-distances-to-property)" \ OPT_SHOW_GOTO_FUNCTIONS \ "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \ "(no-simplify)(no-unwinding-assertions)(no-propagation)" \