diff --git a/appveyor.yml b/appveyor.yml index 22fd0d6968e..3e35e5e75ab 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -71,11 +71,6 @@ test_script: sed -i "12i mv $name.exe $name.gb" goto-cc-goto-analyzer/chain.sh || true cat goto-cc-goto-analyzer/chain.sh || true - sed -i "s/goto-cc\/goto-cc/goto-cc\/goto-cl/" goto-cc-symex/chain.sh || true - sed -i "11s/.*/$gc $name.c/" goto-cc-symex/chain.sh || true - sed -i "12i mv $name.exe $name.gb" goto-cc-symex/chain.sh || true - cat goto-cc-symex/chain.sh || true - rem HACK disable failing tests rmdir /s /q ansi-c\arch_flags_mcpu_bad rmdir /s /q ansi-c\arch_flags_mcpu_good @@ -113,11 +108,6 @@ test_script: rmdir /s /q cbmc-java\tableswitch2 rmdir /s /q goto-gcc rmdir /s /q goto-instrument\slice08 - rmdir /s /q symex\va_args_10 - rmdir /s /q symex\va_args_2 - rmdir /s /q symex\va_args_3 - rmdir /s /q symex\va_args_5 - rmdir /s /q symex\va_args_6 make test diff --git a/regression/Makefile b/regression/Makefile index d477cd68bdc..243d65a460a 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -7,7 +7,6 @@ DIRS = ansi-c \ goto-analyzer \ goto-cc-cbmc \ goto-cc-goto-analyzer \ - goto-cc-symex \ goto-diff \ goto-gcc \ goto-instrument \ @@ -15,7 +14,6 @@ DIRS = ansi-c \ invariants \ strings \ strings-smoke-tests \ - symex \ test-script \ # Empty last line diff --git a/regression/goto-cc-symex/Makefile b/regression/goto-cc-symex/Makefile deleted file mode 100644 index 18f4d370eb8..00000000000 --- a/regression/goto-cc-symex/Makefile +++ /dev/null @@ -1,32 +0,0 @@ - -default: tests.log - -test: - @if ! ../test.pl -c ../chain.sh ; then \ - ../failed-tests-printer.pl ; \ - exit 1; \ - fi - -tests.log: - pwd - @if ! ../test.pl -c ../chain.sh ; then \ - ../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: - @for dir in *; do \ - rm -f tests.log; \ - if [ -d "$$dir" ]; then \ - cd "$$dir"; \ - rm -f *.out *.gb; \ - cd ..; \ - fi \ - done diff --git a/regression/goto-cc-symex/chain.sh b/regression/goto-cc-symex/chain.sh deleted file mode 100755 index 25217b24e2a..00000000000 --- a/regression/goto-cc-symex/chain.sh +++ /dev/null @@ -1,12 +0,0 @@ -#!/bin/bash - -src=../../../src - -gc=$src/goto-cc/goto-cc -symex=$src/symex/symex - -options=$1 -name=${2%.c} - -$gc $name.c -o $name.gb -$symex $name.gb $options diff --git a/regression/goto-cc-symex/regenerate-entry-function/main.c b/regression/goto-cc-symex/regenerate-entry-function/main.c deleted file mode 100644 index 6a035127022..00000000000 --- a/regression/goto-cc-symex/regenerate-entry-function/main.c +++ /dev/null @@ -1,16 +0,0 @@ -#include - -int fun(int x) -{ - int i; - if(i>=20) - assert(i>=10); -} - -int main(int argc, char** argv) -{ - int i; - - if(i>=5) - assert(i>=10); -} diff --git a/regression/goto-cc-symex/regenerate-entry-function/test.desc b/regression/goto-cc-symex/regenerate-entry-function/test.desc deleted file mode 100644 index c344483d7b9..00000000000 --- a/regression/goto-cc-symex/regenerate-entry-function/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c -"--function fun --show-goto-functions" -fun\(x\);$ -^EXIT=6$ -^SIGNAL=0$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/Makefile b/regression/symex-infeasibility/Makefile deleted file mode 100644 index 120e9a347c0..00000000000 --- a/regression/symex-infeasibility/Makefile +++ /dev/null @@ -1,19 +0,0 @@ -default: tests.log - -test: - @../test.pl -c ../../../src/symex/symex - -tests.log: ../test.pl - @../test.pl -c ../../../src/symex/symex - -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-infeasibility/bst-safe/main.c b/regression/symex-infeasibility/bst-safe/main.c deleted file mode 100644 index 868a2049a0d..00000000000 --- a/regression/symex-infeasibility/bst-safe/main.c +++ /dev/null @@ -1,101 +0,0 @@ -// 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-infeasibility/bst-safe/test.desc b/regression/symex-infeasibility/bst-safe/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/bst-safe/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/concrete-sum-unsafe/main.c b/regression/symex-infeasibility/concrete-sum-unsafe/main.c deleted file mode 100644 index 42feb3f2580..00000000000 --- a/regression/symex-infeasibility/concrete-sum-unsafe/main.c +++ /dev/null @@ -1,18 +0,0 @@ -#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-infeasibility/concrete-sum-unsafe/test.desc b/regression/symex-infeasibility/concrete-sum-unsafe/test.desc deleted file mode 100644 index 510460c939a..00000000000 --- a/regression/symex-infeasibility/concrete-sum-unsafe/test.desc +++ /dev/null @@ -1,6 +0,0 @@ -CORE -main.c - -^VERIFICATION FAILED$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/concrete-sum/concrete-sum-unsafe.c b/regression/symex-infeasibility/concrete-sum/concrete-sum-unsafe.c deleted file mode 100644 index 584f997da09..00000000000 --- a/regression/symex-infeasibility/concrete-sum/concrete-sum-unsafe.c +++ /dev/null @@ -1,16 +0,0 @@ -#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-infeasibility/concrete-sum/main.c b/regression/symex-infeasibility/concrete-sum/main.c deleted file mode 100644 index 163066e57ef..00000000000 --- a/regression/symex-infeasibility/concrete-sum/main.c +++ /dev/null @@ -1,21 +0,0 @@ -#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-infeasibility/concrete-sum/test.desc b/regression/symex-infeasibility/concrete-sum/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/concrete-sum/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/counter-safe/main.c b/regression/symex-infeasibility/counter-safe/main.c deleted file mode 100644 index b6413195b31..00000000000 --- a/regression/symex-infeasibility/counter-safe/main.c +++ /dev/null @@ -1,39 +0,0 @@ -// Similar to SV-COMP'14 (loops/count_up_down_true.c) except -// that we use explicit signedness constraints to support -// benchmarks with tools that are not bit precise. - -#define N 10 -#define ENABLE_CPROVER - -#include - -#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-infeasibility/counter-safe/test.desc b/regression/symex-infeasibility/counter-safe/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/counter-safe/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/counter-unsafe/main.c b/regression/symex-infeasibility/counter-unsafe/main.c deleted file mode 100644 index 909459094cd..00000000000 --- a/regression/symex-infeasibility/counter-unsafe/main.c +++ /dev/null @@ -1,39 +0,0 @@ -// 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-infeasibility/counter-unsafe/test.desc b/regression/symex-infeasibility/counter-unsafe/test.desc deleted file mode 100644 index 510460c939a..00000000000 --- a/regression/symex-infeasibility/counter-unsafe/test.desc +++ /dev/null @@ -1,6 +0,0 @@ -CORE -main.c - -^VERIFICATION FAILED$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/for-loop/main.c b/regression/symex-infeasibility/for-loop/main.c deleted file mode 100644 index a3ba7e40b2c..00000000000 --- a/regression/symex-infeasibility/for-loop/main.c +++ /dev/null @@ -1,13 +0,0 @@ -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-infeasibility/for-loop/test.desc b/regression/symex-infeasibility/for-loop/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/for-loop/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/insertion-sort-safe/main.c b/regression/symex-infeasibility/insertion-sort-safe/main.c deleted file mode 100644 index df01181380b..00000000000 --- a/regression/symex-infeasibility/insertion-sort-safe/main.c +++ /dev/null @@ -1,46 +0,0 @@ -// 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 - -#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-1]; j--; - } - a[j] = v; - } -} - -int main() { - int a[N]; - -#ifdef ENABLE_KLEE - klee_make_symbolic(a, sizeof(a), "a"); -#endif - -#ifndef FORCE_BRANCH - insertion_sort(a, 0, N-1); - for (unsigned i = 0; i < N - 1; i++) - assert(a[i] <= a[i+1]); -#endif - - return 0; -} diff --git a/regression/symex-infeasibility/insertion-sort-safe/test.desc b/regression/symex-infeasibility/insertion-sort-safe/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/insertion-sort-safe/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/insertion-sort-unsafe/main.c b/regression/symex-infeasibility/insertion-sort-unsafe/main.c deleted file mode 100644 index 21960ff19e5..00000000000 --- a/regression/symex-infeasibility/insertion-sort-unsafe/main.c +++ /dev/null @@ -1,47 +0,0 @@ -// 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-infeasibility/insertion-sort-unsafe/test.desc b/regression/symex-infeasibility/insertion-sort-unsafe/test.desc deleted file mode 100644 index 510460c939a..00000000000 --- a/regression/symex-infeasibility/insertion-sort-unsafe/test.desc +++ /dev/null @@ -1,6 +0,0 @@ -CORE -main.c - -^VERIFICATION FAILED$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/modulus-safe/main.c b/regression/symex-infeasibility/modulus-safe/main.c deleted file mode 100644 index c2d0d52a51e..00000000000 --- a/regression/symex-infeasibility/modulus-safe/main.c +++ /dev/null @@ -1,38 +0,0 @@ -#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-infeasibility/modulus-safe/test.desc b/regression/symex-infeasibility/modulus-safe/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/modulus-safe/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/modulus-unsafe/main.c b/regression/symex-infeasibility/modulus-unsafe/main.c deleted file mode 100644 index ebe9be32f01..00000000000 --- a/regression/symex-infeasibility/modulus-unsafe/main.c +++ /dev/null @@ -1,31 +0,0 @@ -#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-infeasibility/modulus-unsafe/test.desc b/regression/symex-infeasibility/modulus-unsafe/test.desc deleted file mode 100644 index 510460c939a..00000000000 --- a/regression/symex-infeasibility/modulus-unsafe/test.desc +++ /dev/null @@ -1,6 +0,0 @@ -CORE -main.c - -^VERIFICATION FAILED$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/path-merge/main.c b/regression/symex-infeasibility/path-merge/main.c deleted file mode 100644 index 1cb5264291d..00000000000 --- a/regression/symex-infeasibility/path-merge/main.c +++ /dev/null @@ -1,59 +0,0 @@ - - #define SIZE 15 - #include - - int main() { - int A[1]; - int x; - int i = 0; - int v1 = 0; - int v2 = 0; - int p1 = 0; - int p2 = 0; - - int N = 8; - int y; - - for(i = 0; i < N; i++) { - if(x) { - p1 = p1 + 1; - } else { - p2 = p2 + 1; - } - } - - - if(x) { - y = y + 1; - } else { - y = y - 1; - } - - if(x) { - y = 1; - } else{ - y = 2; - } - - assert(y == 1 || y == 2); - - for(i = 0; i < N; i++) { - if(x) { - p1 = p1 + 1; - } else { - p2 = p2 + 1; - } - } - - - i = 0; - assert( p1 + p2 == 2*N); - - /* - Results - Normal: 105.656s. 0 SAT. - Runtime: 6.856s total, 1.064s SAT - - 1060 variables, 3801 clauses - */ - } diff --git a/regression/symex-infeasibility/path-merge/test.desc b/regression/symex-infeasibility/path-merge/test.desc deleted file mode 100644 index 57abdc2445b..00000000000 --- a/regression/symex-infeasibility/path-merge/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -main.c - -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/the-adder-pipelined/main.c b/regression/symex-infeasibility/the-adder-pipelined/main.c deleted file mode 100644 index f06c67300c3..00000000000 --- a/regression/symex-infeasibility/the-adder-pipelined/main.c +++ /dev/null @@ -1,115 +0,0 @@ -#include -//#include -#define TRUE 1 -#define FALSE 0 - -struct state_elements_top{ - _Bool done; - unsigned int once; - unsigned short int xsum_in; - unsigned int state; - unsigned int xavg_next; - unsigned int xavg_out; - unsigned int xdiff_out; -}; -struct state_elements_top stop; - -void topc(_Bool clk, _Bool rst, unsigned int ser_in, _Bool *done); - -// *********** Implementation in C ************** - -void topc(_Bool clk, _Bool rst, unsigned int ser_in, _Bool *done) -{ - unsigned int tmp13; - unsigned int tmp12; - unsigned int tmp11; - unsigned int tmp10; - unsigned int tmp9; - unsigned int tmp8; - unsigned int tmp7; - unsigned short int tmp6; - unsigned int tmp5; - unsigned int tmp4; - unsigned short int tmp3; - unsigned int tmp2; - unsigned int tmp1; - unsigned int tmp0; - if(rst) - { - tmp0 = 0; - tmp1 = 0; - tmp2 = 0; - stop.xavg_out = tmp0 & 255; - stop.xdiff_out = tmp1 & 255; - stop.state = tmp2 & 3; - } - - else - { - if(stop.state == 0) - { - tmp3 = (unsigned short int)ser_in; - tmp4 = 1; - tmp5 = 1; - stop.xsum_in = tmp3 & 1023; - stop.state = tmp4 & 3; - stop.once = tmp5; - } - - else - if(stop.state == 1) - { - tmp6 = stop.xsum_in + (unsigned short int)ser_in; - tmp7 = 0; - stop.xsum_in = tmp6 & 1023; - if((_Bool)stop.once) - { - tmp8 = 1; - stop.state = tmp8 & 3; - } - - else - { - tmp9 = 2; - stop.state = tmp9 & 3; - } - stop.once = tmp7; // This update must take place at the end of the current if-else block so as to simulate the effect of reading the old value of stop.once through non-blocking statement - } - - else - { - stop.xavg_next = ((stop.xsum_in + ser_in) >> 2) & 255; - tmp10 = stop.xavg_next; - stop.xavg_out = tmp10 & 255; - if(stop.xavg_next >= ser_in) - { - tmp11 = stop.xavg_next - ser_in; - stop.xdiff_out = tmp11 & 255; - } - - else - { - tmp12 = ser_in - stop.xavg_next; - stop.xdiff_out = tmp12 & 255; - } - tmp13 = 0; - stop.state = tmp13 & 3; - } - } - stop.done = (stop.state == 0); -} - -void main() -{ - int i=0; - _Bool clk; - _Bool rst; - unsigned int ser_in; - _Bool done; - while(i<=100) - { - topc(clk, rst, ser_in, &done); - assert(stop.xavg_out == 0 || stop.xavg_out != 0); - i++; - } -} diff --git a/regression/symex-infeasibility/the-adder-pipelined/test.desc b/regression/symex-infeasibility/the-adder-pipelined/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/the-adder-pipelined/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/the-adder/main.c b/regression/symex-infeasibility/the-adder/main.c deleted file mode 100644 index d7e10ce8849..00000000000 --- a/regression/symex-infeasibility/the-adder/main.c +++ /dev/null @@ -1,149 +0,0 @@ -#include -//#include -#define TRUE 1 -#define FALSE 0 - -// ******** C Implementation of Adder *************// -struct state_elements_top{ - _Bool done; - unsigned int xsum1_in; - unsigned int xsum2_in; - unsigned int state; - unsigned int s0_in; - unsigned int s1_in; - unsigned int s2_in; - unsigned int xavg_next; - unsigned int xavg_out; - unsigned int xdiff_out; -}; -struct state_elements_top stop; - -void topc(_Bool clk, _Bool rst, unsigned int ser_in, _Bool *done) -{ - unsigned int tmp40; - unsigned int tmp30; - unsigned int tmp11; - unsigned int tmp10; - unsigned int tmp9; - unsigned int tmp8; - unsigned int tmp7; - unsigned int tmp6; - unsigned int tmp5; - unsigned int tmp4; - unsigned int tmp3; - unsigned int tmp2; - unsigned int tmp1; - unsigned int tmp0; - if(rst) - { - tmp0 = 0; - tmp1 = 0; - tmp2 = 0; - stop.xavg_out = tmp0 & 255; - stop.xdiff_out = tmp1 & 255; - stop.state = tmp2 & 3; - } - - else - { - if(stop.state == 0) - { - tmp3 = ser_in; - tmp4 = 1; - stop.s0_in = tmp3 & 255; - stop.state = tmp4 & 3; - } - - else - if(stop.state == 1) - { - tmp5 = ser_in; - tmp30 = 2; - stop.s1_in = tmp5 & 255; - stop.state = tmp30 & 3; - - } - - else - if(stop.state == 2) - { - tmp6 = ser_in; - tmp7 = stop.s0_in + stop.s1_in; - tmp40 = 3; - stop.s2_in = tmp6 & 255; - stop.xsum1_in = tmp7 & 1023; - stop.state = tmp40 & 3; - } - - else - { - stop.xsum2_in = (ser_in + stop.s2_in) & 1023; - stop.xavg_next = ((stop.xsum1_in + stop.xsum2_in) >> 2) & 255; - tmp8 = stop.xavg_next; - stop.xavg_out = tmp8 & 255; - if(stop.xavg_next >= ser_in) - { - tmp9 = stop.xavg_next - ser_in; - stop.xdiff_out = tmp9 & 255; - } - - else - { - tmp10 = ser_in - stop.xavg_next; - stop.xdiff_out = tmp10 & 255; - } - tmp11 = 0; - stop.state = tmp11 & 3; - } - } - - stop.done = (stop.state == 0); -} - - -void main() -{ - int i=0; - _Bool clk; - _Bool rst; - unsigned int ser_in; - _Bool done; - while(i<=100) - { - topc(clk, rst, ser_in, &done); - /*assert(stop.xavg_out == 0 && stop.xdiff_out==0); - //printf("%d %d\n",stop.xavg_out, stop.xdiff_out); - topc(clk, 0, 7, &done); - assert(stop.xavg_out == 0 && stop.xdiff_out==0); - //printf("%d %d\n",stop.xavg_out, stop.xdiff_out); - topc(clk, 0, 8, &done); - assert(stop.xavg_out == 0 && stop.xdiff_out==0); - //printf("%d %d\n",stop.xavg_out, stop.xdiff_out); - topc(clk, 0, 8, &done); - assert(stop.xavg_out == 0 && stop.xdiff_out==0); - //printf("%d %d\n",stop.xavg_out, stop.xdiff_out); - topc(clk, 0, 8, &done); - assert(stop.xavg_out == 7 && stop.xdiff_out==1); - //printf("%d %d\n",stop.xavg_out, stop.xdiff_out); - topc(clk, 0, 8, &done); - assert(stop.xavg_out == 7 && stop.xdiff_out==1); - //printf("%d %d\n",stop.xavg_out, stop.xdiff_out); - topc(clk, 0, 7, &done); - assert(stop.xavg_out == 7 && stop.xdiff_out==1); - //printf("%d %d\n",stop.xavg_out, stop.xdiff_out); - topc(clk, 0, 8, &done); - assert(stop.xavg_out == 7 && stop.xdiff_out==1); - //printf("%d %d\n",stop.xavg_out, stop.xdiff_out); - topc(clk, 0, 8, &done); - assert(stop.xavg_out == 7 && stop.xdiff_out==1); - //printf("%d %d\n",stop.xavg_out, stop.xdiff_out); - topc(clk, 0, 8, &done); - assert(stop.xavg_out == 7 && stop.xdiff_out==1); - //printf("%d %d\n",stop.xavg_out, stop.xdiff_out); - topc(clk, 0, 8, &done); - assert(stop.xavg_out == 7 && stop.xdiff_out==1); - //printf("%d %d\n",stop.xavg_out, stop.xdiff_out);*/ - assert(stop.xavg_out == 0 || stop.xavg_out != 0); - i++; - } -} diff --git a/regression/symex-infeasibility/the-adder/test.desc b/regression/symex-infeasibility/the-adder/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/the-adder/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/tp1/main.c b/regression/symex-infeasibility/tp1/main.c deleted file mode 100644 index 944569e3ea2..00000000000 --- a/regression/symex-infeasibility/tp1/main.c +++ /dev/null @@ -1,127 +0,0 @@ -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-infeasibility/tp1/test.desc b/regression/symex-infeasibility/tp1/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/tp1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/tp2/main.c b/regression/symex-infeasibility/tp2/main.c deleted file mode 100644 index 141cbde1f84..00000000000 --- a/regression/symex-infeasibility/tp2/main.c +++ /dev/null @@ -1,57 +0,0 @@ -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-infeasibility/tp2/test.desc b/regression/symex-infeasibility/tp2/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/tp2/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/tp3/main.c b/regression/symex-infeasibility/tp3/main.c deleted file mode 100644 index 3019b1172c1..00000000000 --- a/regression/symex-infeasibility/tp3/main.c +++ /dev/null @@ -1,129 +0,0 @@ -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-infeasibility/tp3/test.desc b/regression/symex-infeasibility/tp3/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/tp3/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/tp4/main.c b/regression/symex-infeasibility/tp4/main.c deleted file mode 100644 index f41600da5cc..00000000000 --- a/regression/symex-infeasibility/tp4/main.c +++ /dev/null @@ -1,60 +0,0 @@ -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-infeasibility/tp4/test.desc b/regression/symex-infeasibility/tp4/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/tp4/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex-infeasibility/tp5/main.c b/regression/symex-infeasibility/tp5/main.c deleted file mode 100644 index b8b2df491fe..00000000000 --- a/regression/symex-infeasibility/tp5/main.c +++ /dev/null @@ -1,25 +0,0 @@ -#include - -int f(int x) { - return 2*x; -} - -int g(int x) { - int y = x; - - while (x--) { - y++; - } - - return y; -} - -int main(void) { - unsigned int x; - - __CPROVER_assume(x < 50); - - if (x >= 0) { - assert(f(x) == g(x)); - } -} diff --git a/regression/symex-infeasibility/tp5/test.desc b/regression/symex-infeasibility/tp5/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex-infeasibility/tp5/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/Makefile b/regression/symex/Makefile deleted file mode 100644 index 006aaf3a346..00000000000 --- a/regression/symex/Makefile +++ /dev/null @@ -1,25 +0,0 @@ -default: tests.log - -test: - @if ! ../test.pl -c ../../../src/symex/symex ; then \ - ../failed-tests-printer.pl ; \ - exit 1 ; \ - fi - -tests.log: ../test.pl - @if ! ../test.pl -c ../../../src/symex/symex ; then \ - ../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/array1/main.c b/regression/symex/array1/main.c deleted file mode 100644 index 6f172867b3a..00000000000 --- a/regression/symex/array1/main.c +++ /dev/null @@ -1,21 +0,0 @@ -#include - -struct some_struct -{ - int x, y, z; -} some_struct_array[10]; - -int some_int_array[10]; - -int main() -{ - int i; - - // zero initialization - assert(some_int_array[1]==0); - if(i>=0 && i<10) assert(some_int_array[i]==0); - - some_int_array[5]=5; - assert(some_int_array[1]==0); - assert(some_int_array[5]==5); -} diff --git a/regression/symex/array1/test.desc b/regression/symex/array1/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex/array1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/function_pointer1/main.c b/regression/symex/function_pointer1/main.c deleted file mode 100644 index 80ed753180c..00000000000 --- a/regression/symex/function_pointer1/main.c +++ /dev/null @@ -1,32 +0,0 @@ -#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/function_pointer1/test.desc b/regression/symex/function_pointer1/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex/function_pointer1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/if1/main.c b/regression/symex/if1/main.c deleted file mode 100644 index ab5dda196d9..00000000000 --- a/regression/symex/if1/main.c +++ /dev/null @@ -1,13 +0,0 @@ -#include - -int main() -{ - int i; - - if(i==1) - assert(i==1); - else - assert(i!=1); - - assert(i!=1); -} diff --git a/regression/symex/if1/test.desc b/regression/symex/if1/test.desc deleted file mode 100644 index 5bd20d96b75..00000000000 --- a/regression/symex/if1/test.desc +++ /dev/null @@ -1,11 +0,0 @@ -CORE -main.c - -^EXIT=10$ -^SIGNAL=0$ -^VERIFICATION FAILED$ -^\[main.assertion.1\] assertion i==1: SUCCESS$ -^\[main.assertion.2\] assertion i!=1: SUCCESS$ -^\[main.assertion.3\] assertion i!=1: FAILURE$ --- -^warning: ignoring diff --git a/regression/symex/malloc1/main.c b/regression/symex/malloc1/main.c deleted file mode 100644 index e5fe1e6f14b..00000000000 --- a/regression/symex/malloc1/main.c +++ /dev/null @@ -1,15 +0,0 @@ -#include -#include - -int main() -{ - int *p; - - p=(int *)malloc(sizeof(int)); - - *p=1; - - assert(*p==1); - - free(p); -} diff --git a/regression/symex/malloc1/test.desc b/regression/symex/malloc1/test.desc deleted file mode 100644 index 9845e70d84b..00000000000 --- a/regression/symex/malloc1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c ---little-endian -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/pointer1/main.c b/regression/symex/pointer1/main.c deleted file mode 100644 index b03fc8e4a9a..00000000000 --- a/regression/symex/pointer1/main.c +++ /dev/null @@ -1,37 +0,0 @@ -#include - -int main() -{ - int *p, i; - char *q; - char ch0, ch1, ch2, ch3; - - // pointer into an integer - q=(char *)&i; - - i=0x03020100; - - // endianness-dependent - ch0=q[0]; - ch1=q[1]; - ch2=q[2]; - ch3=q[3]; - - assert(ch0==0); - assert(ch1==1); - assert(ch2==2); - assert(ch3==3); - - unsigned int *up=(unsigned int *)q; - assert(*up==i); - - // pointer with conditional - int input, x, y; - p=input?&x:&y; - *p=1; - - if(input) - assert(x==1); - else - assert(y==1); -} diff --git a/regression/symex/pointer1/test.desc b/regression/symex/pointer1/test.desc deleted file mode 100644 index 9845e70d84b..00000000000 --- a/regression/symex/pointer1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c ---little-endian -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/pointer2/main.c b/regression/symex/pointer2/main.c deleted file mode 100644 index 4abeb51b8d9..00000000000 --- a/regression/symex/pointer2/main.c +++ /dev/null @@ -1,31 +0,0 @@ -#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/pointer2/test.desc b/regression/symex/pointer2/test.desc deleted file mode 100644 index 9845e70d84b..00000000000 --- a/regression/symex/pointer2/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c ---little-endian -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/pointer3/main.c b/regression/symex/pointer3/main.c deleted file mode 100644 index 29661994a99..00000000000 --- a/regression/symex/pointer3/main.c +++ /dev/null @@ -1,14 +0,0 @@ -#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/pointer3/test.desc b/regression/symex/pointer3/test.desc deleted file mode 100644 index 9845e70d84b..00000000000 --- a/regression/symex/pointer3/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c ---little-endian -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/regenerate-entry-function/main.c b/regression/symex/regenerate-entry-function/main.c deleted file mode 100644 index 6a035127022..00000000000 --- a/regression/symex/regenerate-entry-function/main.c +++ /dev/null @@ -1,16 +0,0 @@ -#include - -int fun(int x) -{ - int i; - if(i>=20) - assert(i>=10); -} - -int main(int argc, char** argv) -{ - int i; - - if(i>=5) - assert(i>=10); -} diff --git a/regression/symex/regenerate-entry-function/test.desc b/regression/symex/regenerate-entry-function/test.desc deleted file mode 100644 index 722900f544e..00000000000 --- a/regression/symex/regenerate-entry-function/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c ---function fun --show-goto-functions -fun\(x\);$ -^EXIT=6$ -^SIGNAL=0$ --- -^warning: ignoring diff --git a/regression/symex/show-trace1/main.c b/regression/symex/show-trace1/main.c deleted file mode 100644 index 3b216553005..00000000000 --- a/regression/symex/show-trace1/main.c +++ /dev/null @@ -1,15 +0,0 @@ -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/show-trace1/test.desc b/regression/symex/show-trace1/test.desc deleted file mode 100644 index 23a9f62e3ae..00000000000 --- a/regression/symex/show-trace1/test.desc +++ /dev/null @@ -1,13 +0,0 @@ -KNOWNBUG -main.c ---trace -^EXIT=10$ -^SIGNAL=0$ -^VERIFICATION FAILED$ -^ i=2 .*$ -^ j=3 .*$ -^ k=6 .*$ --- -^warning: ignoring --- -diffblue/cbmc#1361 \ No newline at end of file diff --git a/regression/symex/struct1/main.c b/regression/symex/struct1/main.c deleted file mode 100644 index 9f9fd8ed87a..00000000000 --- a/regression/symex/struct1/main.c +++ /dev/null @@ -1,25 +0,0 @@ -#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/struct1/test.desc b/regression/symex/struct1/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex/struct1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/struct2/main.c b/regression/symex/struct2/main.c deleted file mode 100644 index a0781a64a3f..00000000000 --- a/regression/symex/struct2/main.c +++ /dev/null @@ -1,18 +0,0 @@ -#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/struct2/test.desc b/regression/symex/struct2/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex/struct2/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/struct3/main.c b/regression/symex/struct3/main.c deleted file mode 100644 index 6f9ac01146a..00000000000 --- a/regression/symex/struct3/main.c +++ /dev/null @@ -1,37 +0,0 @@ -#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/struct3/test.desc b/regression/symex/struct3/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex/struct3/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/va_args_1/main.c b/regression/symex/va_args_1/main.c deleted file mode 100644 index d8778034354..00000000000 --- a/regression/symex/va_args_1/main.c +++ /dev/null @@ -1,37 +0,0 @@ -#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/va_args_1/test.desc b/regression/symex/va_args_1/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex/va_args_1/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/va_args_10/main.c b/regression/symex/va_args_10/main.c deleted file mode 100644 index 554187f64d6..00000000000 --- a/regression/symex/va_args_10/main.c +++ /dev/null @@ -1,41 +0,0 @@ -#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/va_args_10/test.desc b/regression/symex/va_args_10/test.desc deleted file mode 100644 index 6de79559914..00000000000 --- a/regression/symex/va_args_10/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=10$ -^SIGNAL=0$ -^VERIFICATION FAILED$ --- -^warning: ignoring diff --git a/regression/symex/va_args_2/main.c b/regression/symex/va_args_2/main.c deleted file mode 100644 index 2a35ca4bb43..00000000000 --- a/regression/symex/va_args_2/main.c +++ /dev/null @@ -1,35 +0,0 @@ -#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/va_args_2/test.desc b/regression/symex/va_args_2/test.desc deleted file mode 100644 index 6de79559914..00000000000 --- a/regression/symex/va_args_2/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=10$ -^SIGNAL=0$ -^VERIFICATION FAILED$ --- -^warning: ignoring diff --git a/regression/symex/va_args_3/main.c b/regression/symex/va_args_3/main.c deleted file mode 100644 index 148d70521db..00000000000 --- a/regression/symex/va_args_3/main.c +++ /dev/null @@ -1,34 +0,0 @@ -#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/va_args_3/test.desc b/regression/symex/va_args_3/test.desc deleted file mode 100644 index 6de79559914..00000000000 --- a/regression/symex/va_args_3/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=10$ -^SIGNAL=0$ -^VERIFICATION FAILED$ --- -^warning: ignoring diff --git a/regression/symex/va_args_4/main.c b/regression/symex/va_args_4/main.c deleted file mode 100644 index 4a19acfe54a..00000000000 --- a/regression/symex/va_args_4/main.c +++ /dev/null @@ -1,38 +0,0 @@ -#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/va_args_4/test.desc b/regression/symex/va_args_4/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex/va_args_4/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/va_args_5/main.c b/regression/symex/va_args_5/main.c deleted file mode 100644 index a1e4d6a9d70..00000000000 --- a/regression/symex/va_args_5/main.c +++ /dev/null @@ -1,35 +0,0 @@ -#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/va_args_5/test.desc b/regression/symex/va_args_5/test.desc deleted file mode 100644 index b69d21c78ba..00000000000 --- a/regression/symex/va_args_5/test.desc +++ /dev/null @@ -1,6 +0,0 @@ -CORE -main.c - -^EXIT=10$ -^SIGNAL=0$ -^VERIFICATION FAILED$ diff --git a/regression/symex/va_args_6/main.c b/regression/symex/va_args_6/main.c deleted file mode 100644 index 191435ff3e0..00000000000 --- a/regression/symex/va_args_6/main.c +++ /dev/null @@ -1,34 +0,0 @@ -#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/va_args_6/test.desc b/regression/symex/va_args_6/test.desc deleted file mode 100644 index 9431f04e854..00000000000 --- a/regression/symex/va_args_6/test.desc +++ /dev/null @@ -1,6 +0,0 @@ -CORE -main.c ---unwind 8 -^EXIT=10$ -^SIGNAL=0$ -^VERIFICATION FAILED$ diff --git a/regression/symex/va_args_7/main.c b/regression/symex/va_args_7/main.c deleted file mode 100644 index cecc1bf0050..00000000000 --- a/regression/symex/va_args_7/main.c +++ /dev/null @@ -1,23 +0,0 @@ -#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/va_args_7/test.desc b/regression/symex/va_args_7/test.desc deleted file mode 100644 index 832e94ec88a..00000000000 --- a/regression/symex/va_args_7/test.desc +++ /dev/null @@ -1,6 +0,0 @@ -CORE -main.c ---unwind 8 -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ diff --git a/regression/symex/va_args_8/main.c b/regression/symex/va_args_8/main.c deleted file mode 100644 index 90e203170f6..00000000000 --- a/regression/symex/va_args_8/main.c +++ /dev/null @@ -1,37 +0,0 @@ -#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/va_args_8/test.desc b/regression/symex/va_args_8/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex/va_args_8/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/regression/symex/va_args_9/main.c b/regression/symex/va_args_9/main.c deleted file mode 100644 index 4c9d52bb394..00000000000 --- a/regression/symex/va_args_9/main.c +++ /dev/null @@ -1,41 +0,0 @@ -#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/va_args_9/test.desc b/regression/symex/va_args_9/test.desc deleted file mode 100644 index 9efefbc7362..00000000000 --- a/regression/symex/va_args_9/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -CORE -main.c - -^EXIT=0$ -^SIGNAL=0$ -^VERIFICATION SUCCESSFUL$ --- -^warning: ignoring diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 13c6d0045b5..3af2d574f4b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -158,7 +158,6 @@ add_subdirectory(json) add_subdirectory(langapi) add_subdirectory(linking) add_subdirectory(memory-models) -add_subdirectory(path-symex) add_subdirectory(pointer-analysis) add_subdirectory(solvers) add_subdirectory(util) @@ -169,6 +168,5 @@ add_subdirectory(clobber) add_subdirectory(cbmc) add_subdirectory(goto-cc) add_subdirectory(goto-instrument) -add_subdirectory(symex) add_subdirectory(goto-analyzer) add_subdirectory(goto-diff) diff --git a/src/Makefile b/src/Makefile index 78fb1a34cb8..191022c8792 100644 --- a/src/Makefile +++ b/src/Makefile @@ -1,10 +1,10 @@ DIRS = ansi-c big-int cbmc cpp goto-cc goto-instrument goto-programs \ goto-symex langapi pointer-analysis solvers util linking xmllang \ - assembler analyses java_bytecode path-symex \ - json goto-analyzer jsil symex goto-diff clobber \ + assembler analyses java_bytecode \ + json goto-analyzer jsil goto-diff clobber \ memory-models miniz -all: cbmc.dir goto-cc.dir goto-instrument.dir symex.dir goto-analyzer.dir goto-diff.dir +all: cbmc.dir goto-cc.dir goto-instrument.dir goto-analyzer.dir goto-diff.dir ############################################################################### @@ -38,10 +38,6 @@ goto-diff.dir: languages goto-programs.dir pointer-analysis.dir \ goto-cc.dir: languages pointer-analysis.dir goto-programs.dir linking.dir -symex.dir: languages goto-programs.dir pointer-analysis.dir \ - goto-symex.dir linking.dir analyses.dir solvers.dir \ - path-symex.dir goto-instrument.dir - # building for a particular directory $(patsubst %, %.dir, $(DIRS)): diff --git a/src/path-symex/CMakeLists.txt b/src/path-symex/CMakeLists.txt deleted file mode 100644 index c86e9c27a25..00000000000 --- a/src/path-symex/CMakeLists.txt +++ /dev/null @@ -1,7 +0,0 @@ -file(GLOB_RECURSE sources "*.cpp") -file(GLOB_RECURSE headers "*.h") -add_library(path-symex ${sources} ${headers}) - -generic_includes(path-symex) - -target_link_libraries(path-symex util pointer-analysis) diff --git a/src/path-symex/Makefile b/src/path-symex/Makefile deleted file mode 100644 index 111597fb97a..00000000000 --- a/src/path-symex/Makefile +++ /dev/null @@ -1,23 +0,0 @@ -SRC = build_goto_trace.cpp \ - locs.cpp \ - path_replay.cpp \ - path_symex.cpp \ - path_symex_history.cpp \ - path_symex_state.cpp \ - path_symex_state_read.cpp \ - var_map.cpp \ - # Empty last line - -INCLUDES= -I .. - -include ../config.inc -include ../common - -CLEANFILES = path-symex$(LIBEXT) - -all: path-symex$(LIBEXT) - -############################################################################### - -path-symex$(LIBEXT): $(OBJ) - $(LINKLIB) diff --git a/src/path-symex/build_goto_trace.cpp b/src/path-symex/build_goto_trace.cpp deleted file mode 100644 index eefb5361f5c..00000000000 --- a/src/path-symex/build_goto_trace.cpp +++ /dev/null @@ -1,115 +0,0 @@ -/*******************************************************************\ - -Module: Build Goto Trace from State History - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Build Goto Trace from State History - -#include "build_goto_trace.h" - -/// follow state history to build a goto trace -void build_goto_trace( - const path_symex_statet &state, - const decision_proceduret &decision_procedure, - goto_tracet &goto_trace) -{ - // follow the history in the state, - // but in a forwards-fashion - - std::vector steps; - state.history.build_history(steps); - - unsigned step_nr; - - for(step_nr=0; step_nr -#include - -#include "path_symex_state.h" - -void build_goto_trace( - const path_symex_statet &state, - const decision_proceduret &decision_procedure, - goto_tracet &goto_trace); - -#endif // CPROVER_PATH_SYMEX_BUILD_GOTO_TRACE_H diff --git a/src/path-symex/loc_ref.h b/src/path-symex/loc_ref.h deleted file mode 100644 index 56cbb7b19b5..00000000000 --- a/src/path-symex/loc_ref.h +++ /dev/null @@ -1,89 +0,0 @@ -/*******************************************************************\ - -Module: Program Locations - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Program Locations - -#ifndef CPROVER_PATH_SYMEX_LOC_REF_H -#define CPROVER_PATH_SYMEX_LOC_REF_H - -#include - -class loc_reft -{ -public: - unsigned loc_number; - - loc_reft next_loc() const - { - loc_reft tmp=*this; - tmp.increase(); - return tmp; - } - - void increase() - { - loc_number++; - } - - void decrease() - { - loc_number--; - } - - bool is_nil() const - { - return loc_number==nil().loc_number; - } - - loc_reft():loc_number(-1) // ugly conversion - { - } - - static inline loc_reft nil() - { - return loc_reft(); - } - - loc_reft &operator++() // this is pre-increment - { - increase(); - return *this; - } - - loc_reft &operator--() // this is pre-decrement - { - decrease(); - return *this; - } - - bool operator<(const loc_reft other) const - { - return loc_number target_mapt; - - target_mapt target_map; - - forall_goto_functions(f_it, goto_functions) - { - const goto_functionst::goto_functiont &goto_function = f_it->second; - - function_entryt &function_entry=function_map[f_it->first]; - function_entry.type=goto_function.type; - - if(goto_function.body_available()) - { - const loc_reft entry_loc=end(); - function_entry.first_loc=entry_loc; - - forall_goto_program_instructions(i_it, goto_function.body) - { - target_map[i_it]=end(); - loc_vector.push_back(loct(i_it, f_it->first)); - } - } - else - function_entry.first_loc=loc_reft::nil(); - } - - if(function_map.find(goto_functionst::entry_point())== - function_map.end()) - throw "no entry point"; - - entry_loc=function_map[goto_functionst::entry_point()].first_loc; - - // build branch targets - for(unsigned l=0; lsecond; - - if(target.loc_number>=loc_vector.size()) - throw "locst::build: illegal jump target"; - - loc_vector[l].branch_target=target; - } - else - throw "locst does not support more than one branch target"; - } -} - -void locst::output(std::ostream &out) const -{ - irep_idt function; - - for(unsigned l=0; ltype << " " -// << loc.target->location - << " " << as_string(ns, *loc.target) << "\n"; - - if(!loc.branch_target.is_nil()) - out << " T: " << loc.branch_target << "\n"; - } - - out << "\n"; - out << "The entry location is L" << entry_loc << ".\n"; -} diff --git a/src/path-symex/locs.h b/src/path-symex/locs.h deleted file mode 100644 index 67f52da1584..00000000000 --- a/src/path-symex/locs.h +++ /dev/null @@ -1,116 +0,0 @@ -/*******************************************************************\ - -Module: CFG made of Program Locations, built from goto_functionst - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// CFG made of Program Locations, built from goto_functionst - -#ifndef CPROVER_PATH_SYMEX_LOCS_H -#define CPROVER_PATH_SYMEX_LOCS_H - -#include - -#include - -#include "loc_ref.h" - -struct loct -{ -public: - loct( - goto_programt::const_targett _target, - const irep_idt &_function): - target(_target), - function(_function) - { - } - - goto_programt::const_targett target; - irep_idt function; - - // we only support a single branch target - loc_reft branch_target; -}; - -class locst -{ -public: - typedef std::vector loc_vectort; - loc_vectort loc_vector; - loc_reft entry_loc; - - class function_entryt - { - public: - loc_reft first_loc; - code_typet type; - }; - - typedef std::map function_mapt; - function_mapt function_map; - - explicit locst(const namespacet &_ns); - void build(const goto_functionst &goto_functions); - void output(std::ostream &out) const; - - loct &operator[] (loc_reft l) - { - assert(l.loc_numbersecond; - } - -protected: - typedef std::map mapt; - mapt map; -}; - -#endif // CPROVER_PATH_SYMEX_LOCS_H diff --git a/src/path-symex/path_replay.cpp b/src/path-symex/path_replay.cpp deleted file mode 100644 index 6044692839c..00000000000 --- a/src/path-symex/path_replay.cpp +++ /dev/null @@ -1,20 +0,0 @@ -/*******************************************************************\ - -Module: Dense Data Structure for Path Replay - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Dense Data Structure for Path Replay - -#include "path_replay.h" - -void get_branches(path_symex_step_reft history) -{ - // history trees are traversed effectively only backwards - for(; !history.is_nil(); --history) - { - } -} diff --git a/src/path-symex/path_replay.h b/src/path-symex/path_replay.h deleted file mode 100644 index 27b6359af9e..00000000000 --- a/src/path-symex/path_replay.h +++ /dev/null @@ -1,41 +0,0 @@ -/*******************************************************************\ - -Module: Dense Data Structure for Path Replay - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Dense Data Structure for Path Replay - -#ifndef CPROVER_PATH_SYMEX_PATH_REPLAY_H -#define CPROVER_PATH_SYMEX_PATH_REPLAY_H - -#include "path_symex_state.h" - -class path_replayt -{ -public: - path_replayt() - { - } - - explicit path_replayt(const path_symex_statet &src) - { - get_branches(src.history); - } - - void replay(path_symex_statet &); - -protected: - // TODO: consider something even denser, say something like a bitset - typedef std::vector branchest; - branchest branches; - - void get_branches(const path_symex_step_reft history); -}; - -void path_replay(path_symex_step_reft history); - -#endif // CPROVER_PATH_SYMEX_PATH_REPLAY_H diff --git a/src/path-symex/path_symex.cpp b/src/path-symex/path_symex.cpp deleted file mode 100644 index 3beecc4cfdf..00000000000 --- a/src/path-symex/path_symex.cpp +++ /dev/null @@ -1,1144 +0,0 @@ -/*******************************************************************\ - -Module: Concrete Symbolic Transformer - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Concrete Symbolic Transformer - -#include "path_symex.h" - -#include -#include -#include -#include -#include -#include -#include -#include - -#include - -#include - -#include "path_symex_class.h" - -#ifdef DEBUG -#include -#endif - -bool path_symext::propagate(const exprt &src) -{ - // propagate things that are 'simple enough' - if(src.is_constant()) - return true; - else if(src.id()==ID_member) - return propagate(to_member_expr(src).struct_op()); - else if(src.id()==ID_index) - return false; - else if(src.id()==ID_typecast) - return propagate(to_typecast_expr(src).op()); - else if(src.id()==ID_symbol) - return true; - else if(src.id()==ID_address_of) - return true; - else if(src.id()==ID_plus) - { - forall_operands(it, src) - if(!propagate(*it)) - return false; - return true; - } - else if(src.id()==ID_array) - { - forall_operands(it, src) - if(!propagate(*it)) - return false; - return true; - } - else if(src.id()==ID_vector) - { - forall_operands(it, src) - if(!propagate(*it)) - return false; - return true; - } - else if(src.id()==ID_if) - { - const if_exprt &if_expr=to_if_expr(src); - if(!propagate(if_expr.true_case())) - return false; - if(!propagate(if_expr.false_case())) - return false; - return true; - } - else if(src.id()==ID_array_of) - { - return propagate(to_array_of_expr(src).what()); - } - else if(src.id()==ID_union) - { - return propagate(to_union_expr(src).op()); - } - else - { - return false; - } -} - -void path_symext::assign( - path_symex_statet &state, - const exprt &lhs, - const exprt &rhs) -{ - if(rhs.id()==ID_side_effect) // catch side effects on rhs - { - const side_effect_exprt &side_effect_expr=to_side_effect_expr(rhs); - const irep_idt &statement=side_effect_expr.get_statement(); - - if(statement==ID_malloc) - { - symex_malloc(state, lhs, side_effect_expr); - return; - } - else if(statement==ID_nondet) - { - // done in statet:instantiate_rec - } - else if(statement==ID_gcc_builtin_va_arg_next) - { - symex_va_arg_next(state, lhs, side_effect_expr); - return; - } - else - throw "unexpected side-effect on rhs: "+id2string(statement); - } - - // read the address of the lhs, with propagation - exprt lhs_address=state.read(address_of_exprt(lhs)); - - // now SSA the lhs, no propagation - exprt ssa_lhs= - state.read_no_propagate(dereference_exprt(lhs_address)); - - // read the rhs - exprt ssa_rhs=state.read(rhs); - - // start recursion on lhs - exprt::operandst _guard; // start with empty guard - assign_rec(state, _guard, lhs, ssa_lhs, ssa_rhs); -} - -inline static typet c_sizeof_type_rec(const exprt &expr) -{ - const irept &sizeof_type=expr.find(ID_C_c_sizeof_type); - - if(!sizeof_type.is_nil()) - { - return static_cast(sizeof_type); - } - else if(expr.id()==ID_mult) - { - forall_operands(it, expr) - { - typet t=c_sizeof_type_rec(*it); - if(t.is_not_nil()) - return t; - } - } - - return nil_typet(); -} - -void path_symext::symex_malloc( - path_symex_statet &state, - const exprt &lhs, - const side_effect_exprt &code) -{ - if(code.operands().size()!=1) - throw "malloc expected to have one operand"; - - // increment dynamic object counter - unsigned dynamic_count=++state.var_map.dynamic_count; - - exprt size=code.op0(); - typet object_type=nil_typet(); - - { - exprt tmp_size=state.read(size); // to allow constant propagation - - // special treatment for sizeof(T)*x - if(tmp_size.id()==ID_mult && - tmp_size.operands().size()==2 && - tmp_size.op0().find(ID_C_c_sizeof_type).is_not_nil()) - { - object_type=array_typet( - c_sizeof_type_rec(tmp_size.op0()), - tmp_size.op1()); - } - else - { - typet tmp_type=c_sizeof_type_rec(tmp_size); - - if(tmp_type.is_not_nil()) - { - // Did the size get multiplied? - mp_integer elem_size=pointer_offset_size(tmp_type, state.var_map.ns); - mp_integer alloc_size; - if(elem_size<0 || to_integer(tmp_size, alloc_size)) - { - } - else - { - if(alloc_size==elem_size) - object_type=tmp_type; - else - { - mp_integer elements=alloc_size/elem_size; - - if(elements*elem_size==alloc_size) - object_type= - array_typet(tmp_type, from_integer(elements, tmp_size.type())); - } - } - } - } - - if(object_type.is_nil()) - object_type=array_typet(unsigned_char_type(), tmp_size); - - // we introduce a fresh symbol for the size - // to prevent any issues of the size getting ever changed - - if(object_type.id()==ID_array && - !to_array_type(object_type).size().is_constant()) - { - exprt &size=to_array_type(object_type).size(); - - symbolt size_symbol; - - size_symbol.base_name="dynamic_object_size"+std::to_string(dynamic_count); - size_symbol.name="symex::"+id2string(size_symbol.base_name); - size_symbol.is_lvalue=true; - size_symbol.type=tmp_size.type(); - size_symbol.mode=ID_C; - - assign(state, - size_symbol.symbol_expr(), - size); - - size=size_symbol.symbol_expr(); - } - } - - // value - symbolt value_symbol; - - value_symbol.base_name= - "dynamic_object"+std::to_string(state.var_map.dynamic_count); - value_symbol.name="symex_dynamic::"+id2string(value_symbol.base_name); - value_symbol.is_lvalue=true; - value_symbol.type=object_type; - value_symbol.type.set("#dynamic", true); - value_symbol.mode=ID_C; - - exprt rhs; - - if(object_type.id()==ID_array) - { - index_exprt index_expr(value_symbol.type.subtype()); - index_expr.array()=value_symbol.symbol_expr(); - index_expr.index()=from_integer(0, index_type()); - rhs=address_of_exprt( - index_expr, pointer_type(value_symbol.type.subtype())); - } - else - { - rhs=address_of_exprt( - value_symbol.symbol_expr(), pointer_type(value_symbol.type)); - } - - if(rhs.type()!=lhs.type()) - rhs.make_typecast(lhs.type()); - - assign(state, lhs, rhs); -} - - -static irep_idt get_old_va_symbol( - const path_symex_statet &state, - const exprt &src) -{ - if(src.id()==ID_typecast) - return get_old_va_symbol(state, to_typecast_expr(src).op()); - else if(src.id()==ID_address_of) - { - const exprt &op=to_address_of_expr(src).object(); - - if(op.id()==ID_symbol) - return to_symbol_expr(op).get_identifier(); - } - - return irep_idt(); -} - -void path_symext::symex_va_arg_next( - path_symex_statet &state, - const exprt &lhs, - const side_effect_exprt &code) -{ - if(code.operands().size()!=1) - throw "va_arg_next expected to have one operand"; - - if(lhs.is_nil()) - return; // ignore - - exprt tmp=state.read(code.op0()); // constant prop on va_arg parameter - - // Get old symbol of va_arg and modify it to generate a new one. - irep_idt id=get_old_va_symbol(state, tmp); - exprt rhs= - zero_initializer( - lhs.type(), - code.source_location(), - state.var_map.ns); - - if(!id.empty()) - { - // strip last name off id to get function name - std::size_t pos=id2string(id).rfind("::"); - if(pos!=std::string::npos) - { - irep_idt function_identifier=std::string(id2string(id), 0, pos); - std::string base=id2string(function_identifier)+"::va_arg"; - - /* - * Construct the identifier of the va_arg argument such that it - * corresponds to the respective one set upon function call - */ - if(has_prefix(id2string(id), base)) - id=base - +std::to_string( - safe_string2unsigned( - std::string(id2string(id), base.size(), std::string::npos)) - +1); - else - id=base+"0"; - - const var_mapt::var_infot &var_info=state.var_map[id]; - - if(var_info.full_identifier==id) - { - const path_symex_statet::var_statet &var_state - =state.get_var_state(var_info); - const exprt symbol_expr=symbol_exprt(id, var_state.ssa_symbol.type()); - rhs=address_of_exprt(symbol_expr); - rhs.make_typecast(lhs.type()); - } - } - } - - assign(state, lhs, rhs); -} - -void path_symext::assign_rec( - path_symex_statet &state, - exprt::operandst &guard, - const exprt &full_lhs, - const exprt &ssa_lhs, - const exprt &ssa_rhs) -{ - // const typet &ssa_lhs_type=state.var_map.ns.follow(ssa_lhs.type()); - - #ifdef DEBUG - std::cout << "assign_rec: " << ssa_lhs.pretty() << '\n'; - // std::cout << "ssa_lhs_type: " << ssa_lhs_type.id() << '\n'; - #endif - - if(ssa_lhs.id()==ID_symbol) - { - // These are expected to be SSA symbols - assert(ssa_lhs.get_bool(ID_C_SSA_symbol)); - - const symbol_exprt &symbol_expr=to_symbol_expr(ssa_lhs); - const irep_idt &full_identifier=symbol_expr.get(ID_C_full_identifier); - - #ifdef DEBUG - const irep_idt &ssa_identifier=symbol_expr.get_identifier(); - std::cout << "SSA symbol identifier: " << ssa_identifier << '\n'; - std::cout << "full identifier: " << full_identifier << '\n'; - #endif - - var_mapt::var_infot &var_info=state.var_map[full_identifier]; - assert(var_info.full_identifier==full_identifier); - - // increase the SSA counter and produce new SSA symbol expression - var_info.increment_ssa_counter(); - symbol_exprt new_ssa_lhs=var_info.ssa_symbol(); - - #ifdef DEBUG - std::cout << "new_ssa_lhs: " << new_ssa_lhs.get_identifier() << '\n'; - #endif - - // record new state of lhs - { - // reference is not stable - path_symex_statet::var_statet &var_state=state.get_var_state(var_info); - var_state.ssa_symbol=new_ssa_lhs; - } - - // rhs nil means non-det assignment - if(ssa_rhs.is_nil()) - { - path_symex_statet::var_statet &var_state=state.get_var_state(var_info); - var_state.value=nil_exprt(); - } - else - { - // consistency check - if(!base_type_eq(ssa_rhs.type(), new_ssa_lhs.type(), state.var_map.ns)) - { - #ifdef DEBUG - std::cout << "ssa_rhs: " << ssa_rhs.pretty() << '\n'; - std::cout << "new_ssa_lhs: " << new_ssa_lhs.pretty() << '\n'; - #endif - throw "assign_rec got different types"; - } - - // record the step - state.record_step(); - stept &step=*state.history; - - if(!guard.empty()) - step.guard=conjunction(guard); - step.full_lhs=full_lhs; - step.ssa_lhs=new_ssa_lhs; - step.ssa_rhs=ssa_rhs; - - // propagate the rhs? - path_symex_statet::var_statet &var_state=state.get_var_state(var_info); - var_state.value=propagate(ssa_rhs)?ssa_rhs:nil_exprt(); - } - } - else if(ssa_lhs.id()==ID_typecast) - { - // dereferencing might yield a typecast - const exprt &new_ssa_lhs=to_typecast_expr(ssa_lhs).op(); - typecast_exprt new_rhs(ssa_rhs, new_ssa_lhs.type()); - - assign_rec(state, guard, full_lhs, new_ssa_lhs, new_rhs); - } - else if(ssa_lhs.id()==ID_member) - { - #ifdef DEBUG - std::cout << "assign_rec ID_member\n"; - #endif - - const member_exprt &ssa_lhs_member_expr=to_member_expr(ssa_lhs); - const exprt &struct_op=ssa_lhs_member_expr.struct_op(); - - const typet &compound_type= - state.var_map.ns.follow(struct_op.type()); - - if(compound_type.id()==ID_struct) - { - // We flatten the top-level structs, so this one is inside an - // array or a union. - - exprt member_name(ID_member_name); - member_name.set( - ID_component_name, - ssa_lhs_member_expr.get_component_name()); - - with_exprt new_rhs(struct_op, member_name, ssa_rhs); - - assign_rec(state, guard, full_lhs, struct_op, new_rhs); - } - else if(compound_type.id()==ID_union) - { - // rewrite into byte_extract, and do again - exprt offset=from_integer(0, index_type()); - - byte_extract_exprt - new_ssa_lhs(byte_update_id(), struct_op, offset, ssa_rhs.type()); - - assign_rec(state, guard, full_lhs, new_ssa_lhs, ssa_rhs); - } - else - throw "assign_rec: member expects struct or union type"; - } - else if(ssa_lhs.id()==ID_index) - { - #ifdef DEBUG - std::cout << "assign_rec ID_index\n"; - #endif - - throw "unexpected array index on lhs"; - } - else if(ssa_lhs.id()==ID_dereference) - { - #ifdef DEBUG - std::cout << "assign_rec ID_dereference\n"; - #endif - - throw "unexpected dereference on lhs"; - } - else if(ssa_lhs.id()==ID_if) - { - #ifdef DEBUG - std::cout << "assign_rec ID_if\n"; - #endif - - const if_exprt &lhs_if_expr=to_if_expr(ssa_lhs); - exprt cond=lhs_if_expr.cond(); - - // true - guard.push_back(cond); - assign_rec(state, guard, full_lhs, lhs_if_expr.true_case(), ssa_rhs); - guard.pop_back(); - - // false - guard.push_back(not_exprt(cond)); - assign_rec(state, guard, full_lhs, lhs_if_expr.false_case(), ssa_rhs); - guard.pop_back(); - } - else if(ssa_lhs.id()==ID_byte_extract_little_endian || - ssa_lhs.id()==ID_byte_extract_big_endian) - { - #ifdef DEBUG - std::cout << "assign_rec ID_byte_extract\n"; - #endif - - const byte_extract_exprt &byte_extract_expr= - to_byte_extract_expr(ssa_lhs); - - // assignment to byte_extract operators: - // turn into byte_update operator - - irep_idt new_id; - - if(ssa_lhs.id()==ID_byte_extract_little_endian) - new_id=ID_byte_update_little_endian; - else if(ssa_lhs.id()==ID_byte_extract_big_endian) - new_id=ID_byte_update_big_endian; - else - UNREACHABLE; - - byte_update_exprt new_rhs(new_id); - - new_rhs.type()=byte_extract_expr.op().type(); - new_rhs.op()=byte_extract_expr.op(); - new_rhs.offset()=byte_extract_expr.offset(); - new_rhs.value()=ssa_rhs; - - const exprt new_ssa_lhs=byte_extract_expr.op(); - - assign_rec(state, guard, full_lhs, new_ssa_lhs, new_rhs); - } - else if(ssa_lhs.id()==ID_struct) - { - const struct_typet &struct_type= - to_struct_type(state.var_map.ns.follow(ssa_lhs.type())); - const struct_typet::componentst &components= - struct_type.components(); - - // split up into components - const exprt::operandst &operands=ssa_lhs.operands(); - - assert(operands.size()==components.size()); - - if(ssa_rhs.id()==ID_struct && - ssa_rhs.operands().size()==components.size()) - { - exprt::operandst::const_iterator lhs_it=operands.begin(); - forall_operands(it, ssa_rhs) - { - assign_rec(state, guard, full_lhs, *lhs_it, *it); - ++lhs_it; - } - } - else - { - for(std::size_t i=0; i &further_states) -{ - #ifdef DEBUG - std::cout << "function_call_rec: " << function.pretty() << '\n'; - #endif - - if(function.id()==ID_symbol) - { - const irep_idt &function_identifier= - to_symbol_expr(function).get_identifier(); - - // find the function - locst::function_mapt::const_iterator f_it= - state.locs.function_map.find(function_identifier); - - if(f_it==state.locs.function_map.end()) - throw - "failed to find `"+id2string(function_identifier)+"' in function_map"; - - const locst::function_entryt &function_entry=f_it->second; - - loc_reft function_entry_point=function_entry.first_loc; - - // do we have a body? - if(function_entry_point==loc_reft()) - { - // no body - - // this is a skip - if(call.lhs().is_not_nil()) - assign(state, call.lhs(), nil_exprt()); - - state.next_pc(); - return; - } - - // push a frame on the call stack - path_symex_statet::threadt &thread= - state.threads[state.get_current_thread()]; - thread.call_stack.push_back(path_symex_statet::framet()); - thread.call_stack.back().current_function=function_identifier; - thread.call_stack.back().return_location=thread.pc.next_loc(); - thread.call_stack.back().return_lhs=call.lhs(); - thread.call_stack.back().return_rhs=nil_exprt(); - - #if 0 - for(loc_reft l=function_entry_point; ; ++l) - { - if(locs[l].target->is_end_function()) - break; - if(locs[l].target->is_decl()) - { - // make sure we have the local in the var_map - state. - } - } - - // save the locals into the frame - for(locst::local_variablest::const_iterator - it=function_entry.local_variables.begin(); - it!=function_entry.local_variables.end(); - it++) - { - unsigned nr=state.var_map[*it].number; - thread.call_stack.back().saved_local_vars[nr]=thread.local_vars[nr]; - } - #endif - - const code_typet &code_type=function_entry.type; - - const code_typet::parameterst &function_parameters=code_type.parameters(); - - const exprt::operandst &call_arguments=call.arguments(); - - // keep track when va arguments begin. - std::size_t va_args_start_index=0; - - // now assign the argument values to parameters - for(std::size_t i=0; iguard=not_exprt(guard); - function_call_rec( - further_states.back(), call, if_expr.false_case(), further_states); - } - - // do the true-case in 'state' - { - state.record_step(); - state.history->guard=guard; - function_call_rec(state, call, if_expr.true_case(), further_states); - } - } - else if(function.id()==ID_typecast) - { - // ignore - function_call_rec( - state, call, to_typecast_expr(function).op(), further_states); - } - else - // NOLINTNEXTLINE(readability/throw) - throw "TODO: function_call "+function.id_string(); -} - -void path_symext::return_from_function(path_symex_statet &state) -{ - path_symex_statet::threadt &thread=state.threads[state.get_current_thread()]; - - // returning from very last function? - if(thread.call_stack.empty()) - { - state.disable_current_thread(); - } - else - { - // update statistics - state.recursion_map[thread.call_stack.back().current_function]--; - - // set PC to return location - thread.pc=thread.call_stack.back().return_location; - - // assign the return value - if(thread.call_stack.back().return_rhs.is_not_nil() && - thread.call_stack.back().return_lhs.is_not_nil()) - assign(state, thread.call_stack.back().return_lhs, - thread.call_stack.back().return_rhs); - - // restore the local variables - for(path_symex_statet::var_state_mapt::const_iterator - it=thread.call_stack.back().saved_local_vars.begin(); - it!=thread.call_stack.back().saved_local_vars.end(); - it++) - thread.local_vars[it->first]=it->second; - - // kill the frame - thread.call_stack.pop_back(); - } -} - -void path_symext::set_return_value( - path_symex_statet &state, - const exprt &v) -{ - path_symex_statet::threadt &thread= - state.threads[state.get_current_thread()]; - - // returning from very last function? - if(!thread.call_stack.empty()) - thread.call_stack.back().return_rhs=v; -} - -void path_symext::do_goto( - path_symex_statet &state, - std::list &further_states) -{ - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - if(instruction.is_backwards_goto()) - { - // we keep a statistic on how many times we execute backwards gotos - state.unwinding_map[state.pc()]++; - } - - const loct &loc=state.locs[state.pc()]; - assert(!loc.branch_target.is_nil()); - - exprt guard=state.read(instruction.guard); - - if(guard.is_true()) // branch taken always - { - state.record_step(); - state.history->branch=stept::BRANCH_TAKEN; - state.set_pc(loc.branch_target); - return; // we are done - } - - if(!guard.is_false()) - { - // branch taken case - // copy the state into 'further_states' - further_states.push_back(state); - further_states.back().record_step(); - state.history->branch=stept::BRANCH_TAKEN; - further_states.back().set_pc(loc.branch_target); - further_states.back().history->guard=guard; - } - - // branch not taken case - exprt negated_guard=not_exprt(guard); - state.record_step(); - state.history->branch=stept::BRANCH_NOT_TAKEN; - state.next_pc(); - state.history->guard=negated_guard; -} - -void path_symext::do_goto( - path_symex_statet &state, - bool taken) -{ - state.record_step(); - - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - if(instruction.is_backwards_goto()) - { - // we keep a statistic on how many times we execute backwards gotos - state.unwinding_map[state.pc()]++; - } - - exprt guard=state.read(instruction.guard); - - if(taken) - { - // branch taken case - const loct &loc=state.locs[state.pc()]; - assert(!loc.branch_target.is_nil()); - state.set_pc(loc.branch_target); - state.history->guard=guard; - state.history->branch=stept::BRANCH_TAKEN; - } - else - { - // branch not taken case - exprt negated_guard=not_exprt(guard); - state.next_pc(); - state.history->guard=negated_guard; - state.history->branch=stept::BRANCH_NOT_TAKEN; - } -} - -void path_symext::operator()( - path_symex_statet &state, - std::list &further_states) -{ - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - #ifdef DEBUG - std::cout << "path_symext::operator(): " - << state.pc() << " " - << instruction.type - << '\n'; - #endif - - switch(instruction.type) - { - case END_FUNCTION: - // pop the call stack - state.record_step(); - return_from_function(state); - break; - - case RETURN: - // sets the return value - state.record_step(); - state.next_pc(); - - if(instruction.code.operands().size()==1) - set_return_value(state, instruction.code.op0()); - - break; - - case START_THREAD: - { - const loct &loc=state.locs[state.pc()]; - assert(!loc.branch_target.is_nil()); - - state.record_step(); - state.next_pc(); - - // ordering of the following matters due to vector instability - path_symex_statet::threadt &new_thread=state.add_thread(); - path_symex_statet::threadt &old_thread= - state.threads[state.get_current_thread()]; - new_thread.pc=loc.branch_target; - new_thread.local_vars=old_thread.local_vars; - } - break; - - case END_THREAD: - state.record_step(); - state.disable_current_thread(); - break; - - case GOTO: - do_goto(state, further_states); - break; - - case CATCH: - // ignore for now - state.record_step(); - state.next_pc(); - break; - - case THROW: - state.record_step(); - throw "THROW not yet implemented"; // NOLINT(readability/throw) - - case ASSUME: - state.record_step(); - state.next_pc(); - if(instruction.guard.is_false()) - state.disable_current_thread(); - else - { - exprt guard=state.read(instruction.guard); - state.history->guard=guard; - } - break; - - case ASSERT: - case SKIP: - case LOCATION: - case DEAD: - state.record_step(); - state.next_pc(); - break; - - case DECL: - // assigning an RHS of NIL means 'nondet' - assign(state, to_code_decl(instruction.code).symbol(), nil_exprt()); - state.next_pc(); - break; - - case ATOMIC_BEGIN: - if(state.inside_atomic_section) - throw "nested ATOMIC_BEGIN"; - - state.record_step(); - state.next_pc(); - state.inside_atomic_section=true; - break; - - case ATOMIC_END: - if(!state.inside_atomic_section) - throw "ATOMIC_END unmatched"; // NOLINT(readability/throw) - - state.record_step(); - state.next_pc(); - state.inside_atomic_section=false; - break; - - case ASSIGN: - assign(state, to_code_assign(instruction.code)); - state.next_pc(); - break; - - case FUNCTION_CALL: - state.record_step(); - function_call( - state, to_code_function_call(instruction.code), further_states); - break; - - case OTHER: - state.record_step(); - - { - const codet &code=instruction.code; - const irep_idt &statement=code.get_statement(); - - if(statement==ID_expression) - { - // like SKIP - } - else if(statement==ID_printf) - { - // ignore for now (should record stuff printed) - } - else if(statement==ID_asm) - { - // ignore for now - } - else if(statement==ID_fence) - { - // ignore for SC - } - else if(statement==ID_input) - { - // just needs to be recorded - } - else if(statement==ID_output) - { - // just needs to be recorded - } - else - throw "unexpected OTHER statement: "+id2string(statement); - } - - state.next_pc(); - break; - - default: - throw "path_symext: unexpected instruction"; - } -} - -void path_symext::operator()(path_symex_statet &state) -{ - std::list further_states; - operator()(state, further_states); - if(!further_states.empty()) - throw "path_symext got unexpected further states"; -} - -void path_symex( - path_symex_statet &state, - std::list &further_states) -{ - path_symext path_symex; - path_symex(state, further_states); -} - -void path_symex(path_symex_statet &state) -{ - path_symext path_symex; - path_symex(state); -} - -void path_symex_goto( - path_symex_statet &state, - bool taken) -{ - path_symext path_symex; - path_symex.do_goto(state, taken); -} - -void path_symex_assert_fail(path_symex_statet &state) -{ - path_symext path_symex; - path_symex.do_assert_fail(state); -} diff --git a/src/path-symex/path_symex.h b/src/path-symex/path_symex.h deleted file mode 100644 index cc7a8912783..00000000000 --- a/src/path-symex/path_symex.h +++ /dev/null @@ -1,44 +0,0 @@ -/*******************************************************************\ - -Module: Concrete Symbolic Transformer - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Concrete Symbolic Transformer - -// NOLINT(build/header_guard) as this file is also symlinked -#ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_H -#define CPROVER_PATH_SYMEX_PATH_SYMEX_H - -#include "path_symex_state.h" - -// Transform a state by executing a single statement. -// May occasionally yield more than one successor state -// (branches, function calls with ternary operator), -// which are put into "further_states". - -// \pre: "!further_states.empty()" because "state" must -// be stored inside "further_states" -void path_symex( - path_symex_statet &state, - std::list &further_states); - -// Transform a state by executing a single statement. -// Will fail if there is more than one successor state. -void path_symex(path_symex_statet &state); - -// Transforms a state by executing a goto statement; -// the 'taken' argument indicates which way. -void path_symex_goto( - path_symex_statet &state, - bool taken); - -// Transforms a state by executing an assertion statement; -// it is enforced that the assertion fails. -void path_symex_assert_fail( - path_symex_statet &state); - -#endif // CPROVER_PATH_SYMEX_PATH_SYMEX_H diff --git a/src/path-symex/path_symex_class.h b/src/path-symex/path_symex_class.h deleted file mode 100644 index cd67b9c31aa..00000000000 --- a/src/path-symex/path_symex_class.h +++ /dev/null @@ -1,104 +0,0 @@ -/*******************************************************************\ - -Module: Concrete Symbolic Transformer - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Concrete Symbolic Transformer - -#ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_CLASS_H -#define CPROVER_PATH_SYMEX_PATH_SYMEX_CLASS_H - -#include "path_symex.h" - -class path_symext -{ -public: - path_symext() - { - } - - virtual void operator()( - path_symex_statet &state, - std::list &furter_states); - - virtual void operator()(path_symex_statet &state); - - void do_goto( - path_symex_statet &state, - bool taken); - - virtual void do_assert_fail(path_symex_statet &state) - { - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - state.record_step(); - state.next_pc(); - exprt guard=state.read(not_exprt(instruction.guard)); - state.history->guard=guard; - } - - typedef path_symex_stept stept; - -protected: - void do_goto( - path_symex_statet &state, - std::list &further_states); - - void function_call( - path_symex_statet &state, - const code_function_callt &call, - std::list &further_states) - { - exprt f=state.read(call.function()); - function_call_rec(state, call, f, further_states); - } - - void function_call_rec( - path_symex_statet &state, - const code_function_callt &function_call, - const exprt &function, - std::list &further_states); - - void return_from_function(path_symex_statet &state); - - void set_return_value(path_symex_statet &, const exprt &); - - void symex_malloc( - path_symex_statet &state, - const exprt &lhs, - const side_effect_exprt &code); - - void symex_va_arg_next( - path_symex_statet &state, - const exprt &lhs, - const side_effect_exprt &code); - - void assign( - path_symex_statet &state, - const exprt &lhs, - const exprt &rhs); - - void assign( - path_symex_statet &state, - const code_assignt &assignment) - { - assign(state, assignment.lhs(), assignment.rhs()); - } - - void assign_rec( - path_symex_statet &state, - exprt::operandst &guard, // instantiated - const exprt &full_lhs, // not instantiated, no recursion - const exprt &ssa_lhs, // instantiated, recursion here - const exprt &ssa_rhs); // instantiated - - static bool propagate(const exprt &src); -}; - - -#endif // CPROVER_PATH_SYMEX_PATH_SYMEX_CLASS_H diff --git a/src/path-symex/path_symex_history.cpp b/src/path-symex/path_symex_history.cpp deleted file mode 100644 index 618dbbce332..00000000000 --- a/src/path-symex/path_symex_history.cpp +++ /dev/null @@ -1,62 +0,0 @@ -/*******************************************************************\ - -Module: History of path-based symbolic simulator - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// History of path-based symbolic simulator - -#include "path_symex_history.h" - -#include - -#include - -#include - -void path_symex_stept::output(std::ostream &out) const -{ - out << "PCs:"; - -/* - for(pc_vectort::const_iterator p_it=s_it->pc_vector.begin(); - p_it!=pc_vector.end(); - p_it++) - out << " " << *p_it; - */ - out << "\n"; - - out << "Guard: " << from_expr(guard) << "\n"; - out << "Full LHS: " << from_expr(full_lhs) << "\n"; - out << "SSA LHS: " << from_expr(ssa_lhs) << "\n"; - out << "SSA RHS: " << from_expr(ssa_rhs) << "\n"; - out << "\n"; -} - -void path_symex_stept::convert(decision_proceduret &dest) const -{ - if(ssa_rhs.is_not_nil()) - dest << equal_exprt(ssa_lhs, ssa_rhs); - - if(guard.is_not_nil()) - dest << guard; -} - -void path_symex_step_reft::build_history( - std::vector &dest) const -{ - dest.clear(); - - path_symex_step_reft s=*this; - while(!s.is_nil()) - { - dest.push_back(s); - --s; - } - - // the above goes backwards: now need to reverse - std::reverse(dest.begin(), dest.end()); -} diff --git a/src/path-symex/path_symex_history.h b/src/path-symex/path_symex_history.h deleted file mode 100644 index 18b90beffa9..00000000000 --- a/src/path-symex/path_symex_history.h +++ /dev/null @@ -1,182 +0,0 @@ -/*******************************************************************\ - -Module: History for path-based symbolic simulator - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// History for path-based symbolic simulator - -#ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H -#define CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H - -#include -#include - -#include -#include - -#include "loc_ref.h" - -class path_symex_stept; - -// This is a reference to a path_symex_stept, -// and is really cheap to copy. These references are stable, -// even though the underlying vector is not. -class path_symex_step_reft -{ -public: - explicit path_symex_step_reft( - class path_symex_historyt &_history): - index(std::numeric_limits::max()), - history(&_history) - { - } - - path_symex_step_reft(): - index(std::numeric_limits::max()), history(nullptr) - { - } - - bool is_nil() const - { - return index==std::numeric_limits::max(); - } - - path_symex_historyt &get_history() const - { - INVARIANT_STRUCTURED( - history!=nullptr, nullptr_exceptiont, "history is null"); - return *history; - } - - // pre-decrement - path_symex_step_reft &operator--(); - - path_symex_stept &operator*() const { return get(); } - path_symex_stept *operator->() const { return &get(); } - - void generate_successor(); - - // build a forward-traversable version of the history - void build_history(std::vector &dest) const; - -protected: - // we use a vector to store all steps - std::size_t index; - class path_symex_historyt *history; - - path_symex_stept &get() const; -}; - -class decision_proceduret; - -// the actual history node -class path_symex_stept -{ -public: - enum kindt - { - NON_BRANCH, BRANCH_TAKEN, BRANCH_NOT_TAKEN - } branch; - - bool is_branch_taken() const - { - return branch==BRANCH_TAKEN; - } - - bool is_branch_not_taken() const - { - return branch==BRANCH_NOT_TAKEN; - } - - bool is_branch() const - { - return branch==BRANCH_TAKEN || branch==BRANCH_NOT_TAKEN; - } - - path_symex_step_reft predecessor; - - // the thread that did the step - unsigned thread_nr; - - // the instruction that was executed - loc_reft pc; - - exprt guard, ssa_rhs; - exprt full_lhs; - symbol_exprt ssa_lhs; - - bool hidden; - - path_symex_stept(): - branch(NON_BRANCH), - thread_nr(0), - guard(nil_exprt()), - ssa_rhs(nil_exprt()), - full_lhs(nil_exprt()), - hidden(false) - { - } - - // interface to solvers; this converts a single step - void convert(decision_proceduret &dest) const; - - void output(std::ostream &) const; -}; - -// converts the full history -inline decision_proceduret &operator<<( - decision_proceduret &dest, - path_symex_step_reft src) -{ - while(!src.is_nil()) - { - src->convert(dest); - --src; - } - - return dest; -} - -// this stores the forest of histories -class path_symex_historyt -{ -public: - typedef std::vector step_containert; - step_containert step_container; - - // TODO: consider typedefing path_symex_historyt - void clear() - { - step_container.clear(); - } -}; - -inline void path_symex_step_reft::generate_successor() -{ - INVARIANT_STRUCTURED( - history!=nullptr, nullptr_exceptiont, "history is null"); - path_symex_step_reft old=*this; - index=history->step_container.size(); - history->step_container.push_back(path_symex_stept()); - history->step_container.back().predecessor=old; -} - -inline path_symex_step_reft &path_symex_step_reft::operator--() -{ - *this=get().predecessor; - return *this; -} - -inline path_symex_stept &path_symex_step_reft::get() const -{ - INVARIANT_STRUCTURED( - history!=nullptr, nullptr_exceptiont, "history is null"); - assert(!is_nil()); - return history->step_container[index]; -} - -#endif // CPROVER_PATH_SYMEX_PATH_SYMEX_HISTORY_H diff --git a/src/path-symex/path_symex_state.cpp b/src/path-symex/path_symex_state.cpp deleted file mode 100644 index fe663da5b7c..00000000000 --- a/src/path-symex/path_symex_state.cpp +++ /dev/null @@ -1,156 +0,0 @@ -/*******************************************************************\ - -Module: State of path-based symbolic simulator - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// State of path-based symbolic simulator - -#include "path_symex_state.h" - -#include -#include -#include - -#include - -#include - -#include - -#ifdef DEBUG -#include -#include -#endif - -path_symex_statet initial_state( - var_mapt &var_map, - const locst &locs, - path_symex_historyt &path_symex_history) -{ - path_symex_statet s(var_map, locs, path_symex_history); - - // create one new thread - path_symex_statet::threadt &thread=s.add_thread(); - thread.pc=locs.entry_loc; // set its PC - s.set_current_thread(0); - - return s; -} - -void path_symex_statet::output(const threadt &thread, std::ostream &out) const -{ - out << " PC: " << thread.pc << '\n'; - out << " Call stack:"; - for(call_stackt::const_iterator - it=thread.call_stack.begin(); - it!=thread.call_stack.end(); - it++) - out << " " << it->return_location << '\n'; - out << '\n'; -} - -void path_symex_statet::output(std::ostream &out) const -{ - for(unsigned t=0; tthread_nr!=current_thread) - no_thread_interleavings++; - - // update our statistics - depth++; - - if(get_instruction()->is_goto()) - no_branches++; - - // add the step - history.generate_successor(); - stept &step=*history; - - // copy PC - assert(current_thread - -#include "locs.h" -#include "var_map.h" -#include "path_symex_history.h" - -struct path_symex_statet -{ -public: - path_symex_statet( - var_mapt &_var_map, - const locst &_locs, - path_symex_historyt &_path_symex_history): - var_map(_var_map), - locs(_locs), - inside_atomic_section(false), - history(_path_symex_history), - current_thread(0), - no_thread_interleavings(0), - no_branches(0), - depth(0) - { - } - - typedef path_symex_stept stept; - - // These are tied to a particular var_map - // and a particular program. - var_mapt &var_map; - const locst &locs; - - // the value of a variable - struct var_statet - { - // it's a given explicit value or a symbol with given identifier - exprt value; - symbol_exprt ssa_symbol; - - // for uninterpreted functions or arrays we maintain an index set - typedef std::set index_sett; - index_sett index_set; - - var_statet(): - value(nil_exprt()), - ssa_symbol(irep_idt()) - { - } - }; - - // the values of the shared variables - typedef std::vector var_valt; - var_valt shared_vars; - - // save+restore procedure-local variables - typedef std::map var_state_mapt; - - // procedure frame - struct framet - { - irep_idt current_function; - loc_reft return_location; - exprt return_lhs; - exprt return_rhs; - var_state_mapt saved_local_vars; - }; - - // call stack - typedef std::vector call_stackt; - - // the state of a thread - struct threadt - { - public: - loc_reft pc; - call_stackt call_stack; // the call stack - var_valt local_vars; // thread-local variables - bool active; - - threadt():active(true) - { - } - }; - - typedef std::vector threadst; - threadst threads; - - // warning: reference is not stable - var_statet &get_var_state(const var_mapt::var_infot &var_info); - - bool inside_atomic_section; - - unsigned get_current_thread() const - { - return current_thread; - } - - void set_current_thread(unsigned _thread) - { - current_thread=_thread; - } - - goto_programt::const_targett get_instruction() const - { - return locs[pc()].target; - } - - bool is_executable() const - { - return !threads.empty() && - threads[current_thread].active; - } - - // execution history - path_symex_step_reft history; - - // adds an entry to the history - void record_step(); - - // various state transformers - - threadt &add_thread() - { - threads.resize(threads.size()+1); - return threads.back(); - } - - void disable_current_thread() - { - threads[current_thread].active=false; - } - - loc_reft pc() const - { - PRECONDITION(current_threadis_branch(); - } - - bool is_feasible(class decision_proceduret &) const; - - bool check_assertion(class decision_proceduret &); - - // counts how many times we have executed backwards edges - typedef std::map unwinding_mapt; - unwinding_mapt unwinding_map; - - // similar for recursive function calls - typedef std::map recursion_mapt; - recursion_mapt recursion_map; - -protected: - unsigned current_thread; - unsigned no_thread_interleavings; - unsigned no_branches; - unsigned depth; - - exprt read( - const exprt &src, - bool propagate); - - exprt instantiate_rec( - const exprt &src, - bool propagate); - - exprt expand_structs_and_arrays(const exprt &src); - exprt array_theory(const exprt &src, bool propagate); - - exprt instantiate_rec_address( - const exprt &src, - bool propagate); - - exprt read_symbol_member_index( - const exprt &src, - bool propagate); - - bool is_symbol_member_index(const exprt &src) const; -}; - -path_symex_statet initial_state( - var_mapt &var_map, - const locst &locs, - path_symex_historyt &); - -#endif // CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp deleted file mode 100644 index 06a7f10f59d..00000000000 --- a/src/path-symex/path_symex_state_read.cpp +++ /dev/null @@ -1,596 +0,0 @@ -/*******************************************************************\ - -Module: State of path-based symbolic simulator - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// State of path-based symbolic simulator - -#include "path_symex_state.h" - -#include -#include - -#include - -#ifdef DEBUG -#include -#include -#endif - -exprt path_symex_statet::read(const exprt &src, bool propagate) -{ - #ifdef DEBUG - // std::cout << "path_symex_statet::read " << src.pretty() << '\n'; - #endif - - // This has three phases! - // 1. Dereferencing, including propagation of pointers. - // 2. Rewriting to SSA symbols - // 3. Simplifier - - // we force propagation for dereferencing - exprt tmp3=dereference_rec(src, true); - - exprt tmp4=instantiate_rec(tmp3, propagate); - - exprt tmp5=simplify_expr(tmp4, var_map.ns); - - #ifdef DEBUG - // std::cout << " ==> " << tmp.pretty() << '\n'; - #endif - - return tmp5; -} - -exprt path_symex_statet::expand_structs_and_arrays(const exprt &src) -{ - #ifdef DEBUG - std::cout << "expand_structs_and_arrays: " - << from_expr(var_map.ns, "", src) << '\n'; - #endif - - const typet &src_type=var_map.ns.follow(src.type()); - - if(src_type.id()==ID_struct) // src is a struct - { - const struct_typet &struct_type=to_struct_type(src_type); - const struct_typet::componentst &components=struct_type.components(); - - struct_exprt result(src.type()); - result.operands().resize(components.size()); - - // split it up into components - for(unsigned i=0; iid()==ID_symbol) - { - if(current->get_bool(ID_C_SSA_symbol)) - return false; // SSA already - - return true; - } - else if(current->id()==ID_member) - { - const member_exprt &member_expr=to_member_expr(*current); - - const typet &compound_type= - var_map.ns.follow(member_expr.struct_op().type()); - - if(compound_type.id()==ID_struct) - { - // go into next iteration - next=&(member_expr.struct_op()); - } - else - return false; // includes unions, deliberately - } - else if(current->id()==ID_index) - { - const index_exprt &index_expr=to_index_expr(*current); - - // go into next iteration - next=&(index_expr.array()); - } - else - return false; - - // next round - INVARIANT_STRUCTURED(next!=nullptr, nullptr_exceptiont, "next is null"); - current=next; - } -} - -std::string path_symex_statet::array_index_as_string(const exprt &src) const -{ - exprt tmp=simplify_expr(src, var_map.ns); - mp_integer i; - - if(!to_integer(tmp, i)) - return "["+integer2string(i)+"]"; - else - return "[*]"; -} - -exprt path_symex_statet::dereference_rec( - const exprt &src, - bool propagate) -{ - if(src.id()==ID_dereference) - { - const dereference_exprt &dereference_expr=to_dereference_expr(src); - - // read the address to propagate the pointers - exprt address=read(dereference_expr.pointer(), propagate); - - // now hand over to dereference - exprt address_dereferenced=::dereference(address, var_map.ns); - - // the dereferenced address is a mixture of non-SSA and SSA symbols - // (e.g., if-guards and array indices) - return address_dereferenced; - } - - if(!src.has_operands()) - return src; - - exprt src2=src; - - { - // recursive calls on structure of 'src' - Forall_operands(it, src2) - { - exprt tmp_op=dereference_rec(*it, propagate); - *it=tmp_op; - } - } - - return src2; -} - -exprt path_symex_statet::instantiate_rec_address( - const exprt &src, - bool propagate) -{ - #ifdef DEBUG - std::cout << "instantiate_rec_address: " << src.id() << '\n'; - #endif - - if(src.id()==ID_symbol) - { - return src; - } - else if(src.id()==ID_index) - { - assert(src.operands().size()==2); - exprt tmp=src; - tmp.op0()=instantiate_rec_address(src.op0(), propagate); - tmp.op1()=instantiate_rec(src.op1(), propagate); - return tmp; - } - else if(src.id()==ID_dereference) - { - // dereferenct ran before, and this can only be *(type *)integer-address, - // which we simply instantiate as non-address - dereference_exprt tmp=to_dereference_expr(src); - tmp.pointer()=instantiate_rec(tmp.pointer(), propagate); - return tmp; - } - else if(src.id()==ID_member) - { - member_exprt tmp=to_member_expr(src); - tmp.struct_op()=instantiate_rec_address(tmp.struct_op(), propagate); - return tmp; - } - else if(src.id()==ID_string_constant) - { - return src; - } - else if(src.id()==ID_label) - { - return src; - } - else if(src.id()==ID_byte_extract_big_endian || - src.id()==ID_byte_extract_little_endian) - { - assert(src.operands().size()==2); - exprt tmp=src; - tmp.op0()=instantiate_rec_address(src.op0(), propagate); - tmp.op1()=instantiate_rec(src.op1(), propagate); - return tmp; - } - else if(src.id()==ID_if) - { - if_exprt if_expr=to_if_expr(src); - if_expr.true_case()= - instantiate_rec_address(if_expr.true_case(), propagate); - if_expr.false_case()= - instantiate_rec_address(if_expr.false_case(), propagate); - if_expr.cond()=instantiate_rec(if_expr.cond(), propagate); - return if_expr; - } - else - { - // this shouldn't really happen - #ifdef DEBUG - std::cout << "SRC: " << src.pretty() << '\n'; - #endif - throw "address of unexpected `"+src.id_string()+"'"; - } -} diff --git a/src/path-symex/var_map.cpp b/src/path-symex/var_map.cpp deleted file mode 100644 index 96d079c48ff..00000000000 --- a/src/path-symex/var_map.cpp +++ /dev/null @@ -1,127 +0,0 @@ -/*******************************************************************\ - -Module: Variable Numbering - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Variable Numbering - -#include "var_map.h" - -#include - -#include -#include -#include - -var_mapt::var_infot &var_mapt::operator()( - const irep_idt &symbol, - const irep_idt &suffix, - const typet &type) -{ - assert(!symbol.empty()); - - std::string full_identifier= - id2string(symbol)+id2string(suffix); - - std::pair result; - - result=id_map.insert(std::pair( - full_identifier, var_infot())); - - if(result.second) // inserted? - { - result.first->second.full_identifier=full_identifier; - result.first->second.symbol=symbol; - result.first->second.suffix=suffix; - result.first->second.type=type; - init(result.first->second); - } - - return result.first->second; -} - -void var_mapt::var_infot::output(std::ostream &out) const -{ - out << "full_identifier: " << full_identifier << "\n"; - out << "symbol: " << symbol << "\n"; - out << "suffix: " << suffix << "\n"; - - out << "kind: "; - - switch(kind) - { - case PROCEDURE_LOCAL: out << "PROCEDURE_LOCAL"; break; - case THREAD_LOCAL: out << "THREAD_LOCAL"; break; - case SHARED: out << "SHARED"; break; - } - - out << "\n"; - - out << "number: " << number << "\n"; - - out << "type: " << type.pretty() << "\n"; - - out << "\n"; -} - -void var_mapt::init(var_infot &var_info) -{ - if(has_prefix(id2string(var_info.symbol), "symex_dynamic::")) - { - var_info.kind=var_infot::SHARED; - } - else - { - // Check for the presence of va_args - std::size_t found=id2string(var_info.symbol).find("::va_arg"); - if(found != std::string::npos) - { - var_info.kind=var_infot::PROCEDURE_LOCAL; - } - else - { - const symbolt *symbol=nullptr; - if(ns.lookup(var_info.symbol, symbol)) - throw "var_mapt::init identifier \"" - +id2string(var_info.full_identifier) - +"\" lookup in ns failed"; - - if(symbol->is_static_lifetime) - { - if(symbol->is_thread_local) - var_info.kind=var_infot::THREAD_LOCAL; - else - var_info.kind=var_infot::SHARED; - } - else - var_info.kind=var_infot::PROCEDURE_LOCAL; - } - } - - if(var_info.is_shared()) - var_info.number=shared_count++; - else - var_info.number=local_count++; -} - -irep_idt var_mapt::var_infot::ssa_identifier() const -{ - return id2string(full_identifier)+ - "#"+std::to_string(ssa_counter); -} - -void var_mapt::output(std::ostream &out) const -{ - for(id_mapt::const_iterator - it=id_map.begin(); - it!=id_map.end(); - it++) - { - out << it->first << ":\n"; - it->second.output(out); - } -} diff --git a/src/path-symex/var_map.h b/src/path-symex/var_map.h deleted file mode 100644 index 09511174cab..00000000000 --- a/src/path-symex/var_map.h +++ /dev/null @@ -1,114 +0,0 @@ -/*******************************************************************\ - -Module: Variable Numbering - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Variable Numbering - -#ifndef CPROVER_PATH_SYMEX_VAR_MAP_H -#define CPROVER_PATH_SYMEX_VAR_MAP_H - -#include -#include - -#include -#include -#include -#include - -class var_mapt -{ -public: - explicit var_mapt(const namespacet &_ns): - ns(_ns.get_symbol_table(), new_symbols), - shared_count(0), - local_count(0), - nondet_count(0), - dynamic_count(0) - { - } - - struct var_infot - { - enum { SHARED, THREAD_LOCAL, PROCEDURE_LOCAL } kind; - - bool is_shared() const - { - return kind==SHARED; - } - - // the variables are numbered - unsigned number; - - // full_identifier=symbol+suffix - irep_idt full_identifier, symbol, suffix; - - // the type of the identifier (struct member or array) - typet type; - - unsigned ssa_counter; - - var_infot():kind(SHARED), number(0), ssa_counter(0) - { - } - - irep_idt ssa_identifier() const; - - symbol_exprt ssa_symbol() const - { - symbol_exprt s=symbol_exprt(ssa_identifier(), type); - s.set(ID_C_SSA_symbol, true); - s.set(ID_C_full_identifier, full_identifier); - return s; - } - - void increment_ssa_counter() - { - ++ssa_counter; - } - - void output(std::ostream &out) const; - }; - - typedef std::map id_mapt; - id_mapt id_map; - - var_infot &operator()( - const irep_idt &symbol, - const irep_idt &suffix, - const typet &type); - - var_infot &operator[](const irep_idt &full_identifier) - { - return id_map[full_identifier]; - } - - void clear() - { - shared_count=0; - local_count=0; - nondet_count=0; - dynamic_count=0; - id_map.clear(); - } - - void init(var_infot &var_info); - - const namespacet ns; - symbol_tablet new_symbols; - - void output(std::ostream &) const; - -protected: - unsigned shared_count, local_count; - -public: - unsigned nondet_count; // free inputs - unsigned dynamic_count; // memory allocation -}; - -#endif // CPROVER_PATH_SYMEX_VAR_MAP_H diff --git a/src/symex/CMakeLists.txt b/src/symex/CMakeLists.txt deleted file mode 100644 index d4450e79a37..00000000000 --- a/src/symex/CMakeLists.txt +++ /dev/null @@ -1,35 +0,0 @@ -file(GLOB_RECURSE sources "*.cpp") -file(GLOB_RECURSE headers "*.h") -list(REMOVE_ITEM sources - ${CMAKE_CURRENT_SOURCE_DIR}/symex_main.cpp -) -add_library(symex-lib ${sources} ${headers}) - -target_link_libraries(symex-lib - ansi-c - cpp - linking - big-int - goto-programs - analyses - langapi - xml - assembler - solvers - util - goto-symex - pointer-analysis - goto-instrument-lib - path-symex -) - -generic_includes(symex-lib) - -add_if_library(symex-lib bv_refinement) -add_if_library(symex-lib java_bytecode) -add_if_library(symex-lib specc) -add_if_library(symex-lib php) - -add_executable(symex symex_main.cpp) - -target_link_libraries(symex symex-lib) diff --git a/src/symex/Makefile b/src/symex/Makefile deleted file mode 100644 index 46236715d9c..00000000000 --- a/src/symex/Makefile +++ /dev/null @@ -1,56 +0,0 @@ -SRC = path_search.cpp \ - symex_cover.cpp \ - symex_main.cpp \ - symex_parse_options.cpp \ - # Empty last line - -OBJ += ../ansi-c/ansi-c$(LIBEXT) \ - ../cpp/cpp$(LIBEXT) \ - ../java_bytecode/java_bytecode$(LIBEXT) \ - ../linking/linking$(LIBEXT) \ - ../big-int/big-int$(LIBEXT) \ - ../goto-programs/goto-programs$(LIBEXT) \ - ../analyses/analyses$(LIBEXT) \ - ../langapi/langapi$(LIBEXT) \ - ../xmllang/xmllang$(LIBEXT) \ - ../assembler/assembler$(LIBEXT) \ - ../solvers/solvers$(LIBEXT) \ - ../util/util$(LIBEXT) \ - ../goto-symex/adjust_float_expressions$(OBJEXT) \ - ../goto-symex/rewrite_union$(OBJEXT) \ - ../pointer-analysis/dereference$(OBJEXT) \ - ../goto-instrument/cover$(OBJEXT) \ - ../path-symex/path-symex$(LIBEXT) \ - ../miniz/miniz$(OBJEXT) \ - ../json/json$(LIBEXT) - -INCLUDES= -I .. - -LIBS = - -include ../config.inc -include ../common - -CLEANFILES = symex$(EXEEXT) - -all: symex$(EXEEXT) - -ifneq ($(wildcard ../specc/Makefile),) - OBJ += ../specc/specc$(LIBEXT) - CP_CXXFLAGS += -DHAVE_SPECC -endif - -ifneq ($(wildcard ../php/Makefile),) - OBJ += ../php/php$(LIBEXT) - CP_CXXFLAGS += -DHAVE_PHP -endif - -############################################################################### - -symex$(EXEEXT): $(OBJ) - $(LINKBIN) - -.PHONY: symex-mac-signed - -symex-mac-signed: cbmc$(EXEEXT) - strip symex$(EXEEXT) ; codesign -v -s $(OSX_IDENTITY) symex$(EXEEXT) diff --git a/src/symex/path_search.cpp b/src/symex/path_search.cpp deleted file mode 100644 index 6da4eab0856..00000000000 --- a/src/symex/path_search.cpp +++ /dev/null @@ -1,465 +0,0 @@ -/*******************************************************************\ - -Module: Path-based Symbolic Execution - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Path-based Symbolic Execution - -#include "path_search.h" - -#include -#include - -#include -#include - -#include -#include - -path_searcht::resultt path_searcht::operator()( - const goto_functionst &goto_functions) -{ - locst locs(ns); - var_mapt var_map(ns); - - locs.build(goto_functions); - - // this is the container for the history-forest - path_symex_historyt history; - - queue.push_back(initial_state(var_map, locs, history)); - - // set up the statistics - number_of_dropped_states=0; - number_of_paths=0; - number_of_VCCs=0; - number_of_steps=0; - number_of_feasible_paths=0; - number_of_infeasible_paths=0; - number_of_VCCs_after_simplification=0; - number_of_failed_properties=0; - number_of_locs=locs.size(); - - // stop the time - start_time=current_time(); - - initialize_property_map(goto_functions); - - while(!queue.empty()) - { - number_of_steps++; - - // Pick a state from the queue, - // according to some heuristic. - // The state moves to the head of the queue. - pick_state(); - - // move into temporary queue - queuet tmp_queue; - tmp_queue.splice( - tmp_queue.begin(), queue, queue.begin(), ++queue.begin()); - - try - { - statet &state=tmp_queue.front(); - - // record we have seen it - loc_data[state.pc().loc_number].visited=true; - - debug() << "Loc: #" << state.pc().loc_number - << ", queue: " << queue.size() - << ", depth: " << state.get_depth(); - for(const auto &s : queue) - debug() << ' ' << s.get_depth(); - - debug() << eom; - - if(drop_state(state)) - { - number_of_dropped_states++; - number_of_paths++; - continue; - } - - if(!state.is_executable()) - { - number_of_paths++; - continue; - } - - if(eager_infeasibility && - state.last_was_branch() && - !is_feasible(state)) - { - number_of_infeasible_paths++; - number_of_paths++; - continue; - } - - if(number_of_steps%1000==0) - { - time_periodt running_time=current_time()-start_time; - status() << "Queue " << queue.size() - << " thread " << state.get_current_thread()+1 - << '/' << state.threads.size() - << " PC " << state.pc() - << " [" << number_of_steps << " steps, " - << running_time << "s]" << messaget::eom; - } - - // an error, possibly? - if(state.get_instruction()->is_assert()) - { - if(show_vcc) - do_show_vcc(state); - else - { - check_assertion(state); - - // all assertions failed? - if(number_of_failed_properties==property_map.size()) - break; - } - } - - // execute - path_symex(state, tmp_queue); - - // put at head of main queue - queue.splice(queue.begin(), tmp_queue); - } - catch(const std::string &e) - { - error() << e << eom; - number_of_dropped_states++; - } - catch(const char *e) - { - error() << e << eom; - number_of_dropped_states++; - } - catch(int) - { - number_of_dropped_states++; - } - } - - report_statistics(); - - return number_of_failed_properties==0?resultt::SAFE:resultt::UNSAFE; -} - -void path_searcht::report_statistics() -{ - std::size_t number_of_visited_locations=0; - for(const auto &l : loc_data) - if(l.visited) - number_of_visited_locations++; - - #if 0 - for(unsigned l=0; l=2) - // move last to first position - queue.splice(queue.begin(), queue, --queue.end(), queue.end()); - return; - - case search_heuristict::LOCS: - return; - } -} - -void path_searcht::do_show_vcc(statet &state) -{ - // keep statistics - number_of_VCCs++; - - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - mstreamt &out=result(); - - if(instruction.source_location.is_not_nil()) - out << instruction.source_location << '\n'; - - if(instruction.source_location.get_comment()!="") - out << instruction.source_location.get_comment() << '\n'; - - unsigned count=1; - - std::vector steps; - state.history.build_history(steps); - - for(const auto &step_ref : steps) - { - if(step_ref->guard.is_not_nil()) - { - std::string string_value=from_expr(ns, "", step_ref->guard); - out << "{-" << count << "} " << string_value << '\n'; - count++; - } - - if(step_ref->ssa_rhs.is_not_nil()) - { - equal_exprt equality(step_ref->ssa_lhs, step_ref->ssa_rhs); - std::string string_value=from_expr(ns, "", equality); - out << "{-" << count << "} " << string_value << '\n'; - count++; - } - } - - out << "|--------------------------" << '\n'; - - exprt assertion=state.read(instruction.guard); - - out << "{" << 1 << "} " - << from_expr(ns, "", assertion) << '\n'; - - if(!assertion.is_true()) - number_of_VCCs_after_simplification++; - - out << eom; -} - -/// decide whether to drop a state -bool path_searcht::drop_state(const statet &state) -{ - goto_programt::const_targett pc=state.get_instruction(); - - const source_locationt &source_location=pc->source_location; - - if(!source_location.is_nil() && - last_source_location!=source_location) - { - debug() << "SYMEX at file " << source_location.get_file() - << " line " << source_location.get_line() - << " function " << source_location.get_function() - << eom; - - last_source_location=source_location; - } - - // depth limit - if(state.get_depth()>=depth_limit) - return true; - - // context bound - if(state.get_no_thread_interleavings()>=context_bound) - return true; - - // branch bound - if(state.get_no_branches()>=branch_bound) - return true; - - // unwinding limit -- loops - if(unwind_limit!=std::numeric_limits::max() && - pc->is_backwards_goto()) - { - bool stop=false; - - for(const auto &loop_info : state.unwinding_map) - if(loop_info.second>=unwind_limit) - { - stop=true; - break; - } - - const irep_idt id=goto_programt::loop_id(pc); - path_symex_statet::unwinding_mapt::const_iterator entry= - state.unwinding_map.find(state.pc()); - debug() << (stop?"Not unwinding":"Unwinding") - << " loop " << id << " iteration " - << (entry==state.unwinding_map.end()?-1:entry->second) - << " (" << unwind_limit << " max)" - << " " << source_location - << " thread " << state.get_current_thread() << eom; - - if(stop) - return true; - } - - // unwinding limit -- recursion - if(unwind_limit!=std::numeric_limits::max() && - pc->is_function_call()) - { - bool stop=false; - - for(const auto &rec_info : state.recursion_map) - if(rec_info.second>=unwind_limit) - { - stop=true; - break; - } - - exprt function=to_code_function_call(pc->code).function(); - const irep_idt id=function.get(ID_identifier); // could be nil - path_symex_statet::recursion_mapt::const_iterator entry= - state.recursion_map.find(id); - if(entry!=state.recursion_map.end()) - debug() << (stop?"Not unwinding":"Unwinding") - << " recursion " << id << " iteration " - << entry->second - << " (" << unwind_limit << " max)" - << " " << source_location - << " thread " << state.get_current_thread() << eom; - - if(stop) - return true; - } - - // search time limit (--max-search-time) - if(time_limit!=std::numeric_limits::max() && - current_time().get_t()>start_time.get_t()+time_limit*1000) - return true; - - if(pc->is_assume() && - simplify_expr(pc->guard, ns).is_false()) - { - debug() << "aborting path on assume(false) at " - << pc->source_location - << " thread " << state.get_current_thread(); - - const irep_idt &c=pc->source_location.get_comment(); - if(!c.empty()) - debug() << ": " << c; - - debug() << eom; - - return true; - } - - return false; -} - -void path_searcht::check_assertion(statet &state) -{ - // keep statistics - number_of_VCCs++; - - const goto_programt::instructiont &instruction= - *state.get_instruction(); - - irep_idt property_name=instruction.source_location.get_property_id(); - property_entryt &property_entry=property_map[property_name]; - - if(property_entry.status==FAILURE) - return; // already failed - else if(property_entry.status==NOT_REACHED) - property_entry.status=SUCCESS; // well, for now! - - // the assertion in SSA - exprt assertion= - state.read(instruction.guard); - - if(assertion.is_true()) - return; // no error, trivially - - // keep statistics - number_of_VCCs_after_simplification++; - - status() << "Checking property " << property_name << eom; - - // take the time - absolute_timet sat_start_time=current_time(); - - satcheckt satcheck; - bv_pointerst bv_pointers(ns, satcheck); - - satcheck.set_message_handler(get_message_handler()); - bv_pointers.set_message_handler(get_message_handler()); - - if(!state.check_assertion(bv_pointers)) - { - build_goto_trace(state, bv_pointers, property_entry.error_trace); - property_entry.status=FAILURE; - number_of_failed_properties++; - } - - sat_time+=current_time()-sat_start_time; -} - -bool path_searcht::is_feasible(statet &state) -{ - status() << "Feasibility check" << eom; - - // take the time - absolute_timet sat_start_time=current_time(); - - satcheckt satcheck; - bv_pointerst bv_pointers(ns, satcheck); - - satcheck.set_message_handler(get_message_handler()); - bv_pointers.set_message_handler(get_message_handler()); - - bool result=state.is_feasible(bv_pointers); - - sat_time+=current_time()-sat_start_time; - - return result; -} - -void path_searcht::initialize_property_map( - const goto_functionst &goto_functions) -{ - forall_goto_functions(it, goto_functions) - if(!it->second.is_inlined()) - { - const goto_programt &goto_program=it->second.body; - - forall_goto_program_instructions(i_it, goto_program) - { - if(!i_it->is_assert()) - continue; - - const source_locationt &source_location=i_it->source_location; - - irep_idt property_name=source_location.get_property_id(); - - property_entryt &property_entry=property_map[property_name]; - property_entry.status=NOT_REACHED; - property_entry.description=source_location.get_comment(); - property_entry.source_location=source_location; - } - } -} diff --git a/src/symex/path_search.h b/src/symex/path_search.h deleted file mode 100644 index 0959002d163..00000000000 --- a/src/symex/path_search.h +++ /dev/null @@ -1,157 +0,0 @@ -/*******************************************************************\ - -Module: Path-based Symbolic Execution - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Path-based Symbolic Execution - -#ifndef CPROVER_SYMEX_PATH_SEARCH_H -#define CPROVER_SYMEX_PATH_SEARCH_H - -#include -#include - -#include - -#include - -#include - -class path_searcht:public safety_checkert -{ -public: - explicit path_searcht(const namespacet &_ns): - safety_checkert(_ns), - show_vcc(false), - eager_infeasibility(false), - number_of_dropped_states(0), - number_of_paths(0), - number_of_steps(0), - number_of_feasible_paths(0), - number_of_infeasible_paths(0), - number_of_VCCs(0), - number_of_VCCs_after_simplification(0), - number_of_failed_properties(0), - number_of_locs(0), - depth_limit(std::numeric_limits::max()), - context_bound(std::numeric_limits::max()), - branch_bound(std::numeric_limits::max()), - unwind_limit(std::numeric_limits::max()), - time_limit(std::numeric_limits::max()), - search_heuristic(search_heuristict::DFS) - { - } - - virtual resultt operator()( - const goto_functionst &goto_functions); - - void set_depth_limit(int limit) - { - depth_limit=limit; - } - - void set_context_bound(int limit) - { - context_bound=limit; - } - - void set_branch_bound(int limit) - { - branch_bound=limit; - } - - void set_unwind_limit(int limit) - { - unwind_limit=limit; - } - - void set_time_limit(int limit) - { - time_limit=limit; - } - - bool show_vcc; - bool eager_infeasibility; - - // statistics - std::size_t number_of_dropped_states; - std::size_t number_of_paths; - std::size_t number_of_steps; - std::size_t number_of_feasible_paths; - std::size_t number_of_infeasible_paths; - std::size_t number_of_VCCs; - std::size_t number_of_VCCs_after_simplification; - std::size_t number_of_failed_properties; - std::size_t number_of_locs; - absolute_timet start_time; - time_periodt sat_time; - - enum statust { NOT_REACHED, SUCCESS, FAILURE }; - - struct property_entryt - { - statust status; - irep_idt description; - goto_tracet error_trace; - source_locationt source_location; - - bool is_success() const { return status==SUCCESS; } - bool is_failure() const { return status==FAILURE; } - bool is_not_reached() const { return status==NOT_REACHED; } - }; - - void set_dfs() { search_heuristic=search_heuristict::DFS; } - void set_bfs() { search_heuristic=search_heuristict::BFS; } - void set_locs() { search_heuristic=search_heuristict::LOCS; } - - typedef std::map property_mapt; - property_mapt property_map; - -protected: - typedef path_symex_statet statet; - - // State queue. Iterators are stable. - // The states most recently executed are at the head. - typedef std::list queuet; - queuet queue; - - // search heuristic - void pick_state(); - - struct loc_datat - { - bool visited; - loc_datat():visited(false) { } - }; - - expanding_vectort loc_data; - - bool execute(queuet::iterator state); - - void check_assertion(statet &state); - bool is_feasible(statet &state); - void do_show_vcc(statet &state); - - bool drop_state(const statet &state); - - void report_statistics(); - - void initialize_property_map( - const goto_functionst &goto_functions); - - unsigned depth_limit; - unsigned context_bound; - unsigned branch_bound; - unsigned unwind_limit; - unsigned time_limit; - - enum class search_heuristict { DFS, BFS, LOCS } search_heuristic; - - source_locationt last_source_location; -}; - -#endif // CPROVER_SYMEX_PATH_SEARCH_H diff --git a/src/symex/symex_cover.cpp b/src/symex/symex_cover.cpp deleted file mode 100644 index 080425dd87f..00000000000 --- a/src/symex/symex_cover.cpp +++ /dev/null @@ -1,204 +0,0 @@ -/*******************************************************************\ - -Module: Symex Test Suite Generation - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Symex Test Suite Generation - -#include "symex_parse_options.h" - -#include - -#include -#include - -#include -#include - -std::string symex_parse_optionst::get_test(const goto_tracet &goto_trace) -{ - bool first=true; - std::string test; - const namespacet ns(goto_model.symbol_table); - - for(const auto &step : goto_trace.steps) - { - if(step.is_input()) - { - if(first) - first=false; - else - test+=", "; - - test+=id2string(step.io_id)+"="; - - if(step.io_args.size()==1) - test+=from_expr(ns, "", step.io_args.front()); - } - } - return test; -} - -void symex_parse_optionst::report_cover( - const path_searcht::property_mapt &property_map) -{ - // report - unsigned goals_covered=0; - - for(const auto &prop_pair : property_map) - if(prop_pair.second.is_failure()) - goals_covered++; - - switch(get_ui()) - { - case ui_message_handlert::uit::PLAIN: - { - status() << "\n** coverage results:" << eom; - - for(const auto &prop_pair : property_map) - { - const auto &property=prop_pair.second; - - status() << "[" << prop_pair.first << "]"; - - if(property.source_location.is_not_nil()) - status() << ' ' << property.source_location; - - if(!property.description.empty()) - status() << ' ' << property.description; - - status() << ": " << (property.is_failure()?"SATISFIED":"FAILED") - << eom; - } - - status() << '\n'; - - break; - } - - case ui_message_handlert::uit::XML_UI: - { - for(const auto &prop_pair : property_map) - { - const auto &property=prop_pair.second; - - xmlt xml_result("result"); - xml_result.set_attribute("goal", id2string(prop_pair.first)); - xml_result.set_attribute( - "description", id2string(property.description)); - xml_result.set_attribute( - "status", property.is_failure()?"SATISFIED":"FAILED"); - - if(property.source_location.is_not_nil()) - xml_result.new_element()=xml(property.source_location); - - if(property.is_failure()) - { - const namespacet ns(goto_model.symbol_table); - - if(cmdline.isset("trace")) - { - convert(ns, property.error_trace, xml_result.new_element()); - } - else - { - xmlt &xml_test=xml_result.new_element("test"); - - for(const auto &step : property.error_trace.steps) - { - if(step.is_input()) - { - xmlt &xml_input=xml_test.new_element("input"); - xml_input.set_attribute("id", id2string(step.io_id)); - if(step.io_args.size()==1) - xml_input.new_element("value")= - xml(step.io_args.front(), ns); - } - } - } - } - - std::cout << xml_result << "\n"; - } - - break; - } - case ui_message_handlert::uit::JSON_UI: - { - json_objectt json_result; - json_arrayt &result_array=json_result["results"].make_array(); - for(const auto &prop_pair : property_map) - { - const auto &property=prop_pair.second; - - json_objectt &result=result_array.push_back().make_object(); - result["status"]= - json_stringt(property.is_failure()?"satisfied":"failed"); - result["goal"]=json_stringt(id2string(prop_pair.first)); - result["description"]=json_stringt(id2string(property.description)); - - if(property.source_location.is_not_nil()) - result["sourceLocation"]=json(property.source_location); - - if(property.is_failure()) - { - const namespacet ns(goto_model.symbol_table); - - if(cmdline.isset("trace")) - { - jsont &json_trace=result["trace"]; - convert(ns, property.error_trace, json_trace); - } - else - { - json_arrayt &json_test=result["test"].make_array(); - - for(const auto &step : property.error_trace.steps) - { - if(step.is_input()) - { - json_objectt json_input; - json_input["id"]=json_stringt(id2string(step.io_id)); - if(step.io_args.size()==1) - json_input["value"]= - json(step.io_args.front(), ns, ID_unknown); - json_test.push_back(json_input); - } - } - } - } - } - json_result["totalGoals"]= - json_numbert(std::to_string(property_map.size())); - json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered)); - std::cout << ",\n" << json_result; - break; - } - } - - status() << "** " << goals_covered - << " of " << property_map.size() << " covered (" - << std::fixed << std::setw(1) << std::setprecision(1) - << (property_map.empty()? - 100.0:100.0*goals_covered/property_map.size()) - << "%)" - << eom; - - if(get_ui()==ui_message_handlert::uit::PLAIN) - { - std::set tests; - - for(const auto &prop_pair : property_map) - if(prop_pair.second.is_failure()) - tests.insert(get_test(prop_pair.second.error_trace)); - - std::cout << "Test suite:" << '\n'; - - for(const auto &t : tests) - std::cout << t << '\n'; - } -} diff --git a/src/symex/symex_main.cpp b/src/symex/symex_main.cpp deleted file mode 100644 index 8d6f4a2089c..00000000000 --- a/src/symex/symex_main.cpp +++ /dev/null @@ -1,28 +0,0 @@ -/*******************************************************************\ - -Module: Symex Main Module - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Symex Main Module - -#include "symex_parse_options.h" - -#include - -#ifdef _MSC_VER -int wmain(int argc, const wchar_t **argv_wide) -{ - auto vec=narrow_argv(argc, argv_wide); - auto narrow=to_c_str_array(std::begin(vec), std::end(vec)); - auto argv=narrow.data(); -#else -int main(int argc, const char **argv) -{ -#endif - symex_parse_optionst parse_options(argc, argv); - return parse_options.main(); -} diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp deleted file mode 100644 index e85a369340e..00000000000 --- a/src/symex/symex_parse_options.cpp +++ /dev/null @@ -1,613 +0,0 @@ -/*******************************************************************\ - -Module: Symex Command Line Options Processing - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Symex Command Line Options Processing - -#include "symex_parse_options.h" - -#include -#include -#include - -#include -#include -#include -#include -#include -#include - -#include -#include -#include - -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include - -#include -#include - -#include - -#include - -#include - -#include - -#include "path_search.h" - -symex_parse_optionst::symex_parse_optionst(int argc, const char **argv): - parse_options_baset(SYMEX_OPTIONS, argc, argv), - messaget(ui_message_handler), - ui_message_handler(cmdline, "Symex " CBMC_VERSION) -{ -} - -void symex_parse_optionst::eval_verbosity() -{ - // this is our default verbosity - int v=messaget::M_STATISTICS; - - if(cmdline.isset("verbosity")) - { - v=unsafe_string2int(cmdline.get_value("verbosity")); - if(v<0) - v=0; - else if(v>10) - v=10; - } - - ui_message_handler.set_verbosity(v); -} - -void symex_parse_optionst::get_command_line_options(optionst &options) -{ - if(config.set(cmdline)) - { - usage_error(); - exit(1); - } - - if(cmdline.isset("debug-level")) - options.set_option("debug-level", cmdline.get_value("debug-level")); - - if(cmdline.isset("unwindset")) - options.set_option("unwindset", cmdline.get_value("unwindset")); - - // all checks supported by goto_check - PARSE_OPTIONS_GOTO_CHECK(cmdline, options); - - // check assertions - if(cmdline.isset("no-assertions")) - options.set_option("assertions", false); - else - options.set_option("assertions", true); - - // use assumptions - if(cmdline.isset("no-assumptions")) - options.set_option("assumptions", false); - else - options.set_option("assumptions", true); - - // magic error label - if(cmdline.isset("error-label")) - options.set_option("error-label", cmdline.get_values("error-label")); -} - -/// invoke main modules -int symex_parse_optionst::doit() -{ - if(cmdline.isset("version")) - { - std::cout << CBMC_VERSION << '\n'; - return 0; - } - - register_language(new_ansi_c_language); - register_language(new_cpp_language); - register_language(new_java_bytecode_language); - - // - // command line options - // - - optionst options; - get_command_line_options(options); - - eval_verbosity(); - - if(initialize_goto_model(goto_model, cmdline, get_message_handler())) - return 6; - - if(process_goto_program(options)) - return 6; - - label_properties(goto_model); - - if(cmdline.isset("show-properties")) - { - show_properties(goto_model, get_ui()); - return 0; - } - - if(set_properties()) - return 7; - - if(cmdline.isset("show-locs")) - { - const namespacet ns(goto_model.symbol_table); - locst locs(ns); - locs.build(goto_model.goto_functions); - locs.output(std::cout); - return 0; - } - - // do actual Symex - - try - { - const namespacet ns(goto_model.symbol_table); - path_searcht path_search(ns); - - path_search.set_message_handler(get_message_handler()); - - if(cmdline.isset("depth")) - path_search.set_depth_limit( - unsafe_string2unsigned(cmdline.get_value("depth"))); - - if(cmdline.isset("context-bound")) - path_search.set_context_bound( - unsafe_string2unsigned(cmdline.get_value("context-bound"))); - - if(cmdline.isset("branch-bound")) - path_search.set_branch_bound( - unsafe_string2unsigned(cmdline.get_value("branch-bound"))); - - if(cmdline.isset("unwind")) - path_search.set_unwind_limit( - unsafe_string2unsigned(cmdline.get_value("unwind"))); - - if(cmdline.isset("max-search-time")) - path_search.set_time_limit( - safe_string2unsigned(cmdline.get_value("max-search-time"))); - - if(cmdline.isset("dfs")) - path_search.set_dfs(); - - if(cmdline.isset("bfs")) - path_search.set_bfs(); - - if(cmdline.isset("locs")) - path_search.set_locs(); - - if(cmdline.isset("show-vcc")) - { - path_search.show_vcc=true; - path_search(goto_model.goto_functions); - return 0; - } - - path_search.eager_infeasibility= - cmdline.isset("eager-infeasibility"); - - if(cmdline.isset("cover")) - { - // test-suite generation - path_search(goto_model.goto_functions); - report_cover(path_search.property_map); - return 0; - } - else - { - // do actual symex, for assertion checking - switch(path_search(goto_model.goto_functions)) - { - case safety_checkert::resultt::SAFE: - report_properties(path_search.property_map); - report_success(); - return 0; - - case safety_checkert::resultt::UNSAFE: - report_properties(path_search.property_map); - report_failure(); - return 10; - - default: - return 8; - } - } - } - - catch(const std::string error_msg) - { - error() << error_msg << messaget::eom; - return 8; - } - - catch(const char *error_msg) - { - error() << error_msg << messaget::eom; - return 8; - } - - #if 0 - // let's log some more statistics - debug() << "Memory consumption:" << messaget::endl; - memory_info(debug()); - debug() << eom; - #endif -} - -bool symex_parse_optionst::set_properties() -{ - try - { - if(cmdline.isset("property")) - ::set_properties( - goto_model.goto_functions, cmdline.get_values("property")); - } - - catch(const char *e) - { - error() << e << eom; - return true; - } - - catch(const std::string e) - { - error() << e << eom; - return true; - } - - catch(int) - { - return true; - } - - return false; -} - -bool symex_parse_optionst::process_goto_program(const optionst &options) -{ - try - { - // we add the library - link_to_library(goto_model, ui_message_handler); - - // do partial inlining - status() << "Partial Inlining" << eom; - goto_partial_inline(goto_model, ui_message_handler); - - // add generic checks - status() << "Generic Property Instrumentation" << eom; - goto_check(options, goto_model); - - // remove stuff - remove_returns(goto_model); - remove_complex(goto_model); - remove_vector(goto_model); - // remove function pointers - status() << "Removal of function pointers and virtual functions" << eom; - remove_function_pointers( - get_message_handler(), - goto_model, - cmdline.isset("pointer-check")); - // Java virtual functions -> explicit dispatch tables: - remove_virtual_functions(goto_model); - // Java throw and catch -> explicit exceptional return variables: - // This introduces instanceof, so order is important: - remove_exceptions(goto_model); - // Java instanceof -> clsid comparison: - remove_instanceof(goto_model); - rewrite_union(goto_model); - adjust_float_expressions(goto_model); - - // recalculate numbers, etc. - goto_model.goto_functions.update(); - - // add loop ids - goto_model.goto_functions.compute_loop_numbers(); - - if(cmdline.isset("drop-unused-functions")) - { - // Entry point will have been set before and function pointers removed - status() << "Removing unused functions" << eom; - remove_unused_functions(goto_model.goto_functions, ui_message_handler); - } - - // remove skips such that trivial GOTOs are deleted and not considered - // for coverage annotation: - remove_skip(goto_model.goto_functions); - - if(cmdline.isset("cover")) - { - status() << "Instrumenting coverage goals" << eom; - if(instrument_cover_goals(cmdline, goto_model, get_message_handler())) - return true; - } - - // show it? - if(cmdline.isset("show-loops")) - { - show_loop_ids(get_ui(), goto_model); - return true; - } - - // show it? - if(cmdline.isset("show-goto-functions")) - { - show_goto_functions(goto_model, get_ui()); - return true; - } - } - - catch(const char *e) - { - error() << e << eom; - return true; - } - - catch(const std::string e) - { - error() << e << eom; - return true; - } - - catch(int) - { - return true; - } - - catch(std::bad_alloc) - { - error() << "Out of memory" << eom; - return true; - } - - return false; -} - -void symex_parse_optionst::report_properties( - const path_searcht::property_mapt &property_map) -{ - if(get_ui()==ui_message_handlert::uit::PLAIN) - status() << "\n** Results:" << eom; - - for(path_searcht::property_mapt::const_iterator - it=property_map.begin(); - it!=property_map.end(); - it++) - { - if(get_ui()==ui_message_handlert::uit::XML_UI) - { - xmlt xml_result("result"); - xml_result.set_attribute("claim", id2string(it->first)); - - std::string status_string; - - switch(it->second.status) - { - case path_searcht::SUCCESS: status_string="SUCCESS"; break; - case path_searcht::FAILURE: status_string="FAILURE"; break; - case path_searcht::NOT_REACHED: status_string="SUCCESS"; break; - } - - xml_result.set_attribute("status", status_string); - - std::cout << xml_result << "\n"; - } - else - { - status() << "[" << it->first << "] " - << it->second.description << ": "; - switch(it->second.status) - { - case path_searcht::SUCCESS: status() << "SUCCESS"; break; - case path_searcht::FAILURE: status() << "FAILURE"; break; - case path_searcht::NOT_REACHED: status() << "SUCCESS"; break; - } - status() << eom; - } - - if((cmdline.isset("show-trace") || - cmdline.isset("trace")) && - it->second.is_failure()) - show_counterexample(it->second.error_trace); - } - - if(!cmdline.isset("property")) - { - status() << eom; - - unsigned failed=0; - - for(path_searcht::property_mapt::const_iterator - it=property_map.begin(); - it!=property_map.end(); - it++) - if(it->second.is_failure()) - failed++; - - status() << "** " << failed - << " of " << property_map.size() << " failed" - << eom; - } -} - -void symex_parse_optionst::report_success() -{ - result() << "VERIFICATION SUCCESSFUL" << eom; - - switch(get_ui()) - { - case ui_message_handlert::uit::PLAIN: - break; - - case ui_message_handlert::uit::XML_UI: - { - xmlt xml("cprover-status"); - xml.data="SUCCESS"; - std::cout << xml; - std::cout << '\n'; - } - break; - - default: - UNREACHABLE; - } -} - -void symex_parse_optionst::show_counterexample( - const goto_tracet &error_trace) -{ - const namespacet ns(goto_model.symbol_table); - - switch(get_ui()) - { - case ui_message_handlert::uit::PLAIN: - std::cout << '\n' << "Counterexample:" << '\n'; - show_goto_trace(std::cout, ns, error_trace); - break; - - case ui_message_handlert::uit::XML_UI: - { - xmlt xml; - convert(ns, error_trace, xml); - std::cout << xml << std::flush; - } - break; - - default: - UNREACHABLE; - } -} - -void symex_parse_optionst::report_failure() -{ - result() << "VERIFICATION FAILED" << eom; - - switch(get_ui()) - { - case ui_message_handlert::uit::PLAIN: - break; - - case ui_message_handlert::uit::XML_UI: - { - xmlt xml("cprover-status"); - xml.data="FAILURE"; - std::cout << xml; - std::cout << '\n'; - } - break; - - default: - UNREACHABLE; - } -} - -/// display command line help -void symex_parse_optionst::help() -{ - std::cout << - "\n" - "* * Symex " CBMC_VERSION " - Copyright (C) 2013 "; - - std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; - - std::cout << " * *\n"; - - std::cout << - "* * Daniel Kroening * *\n" - "* * University of Oxford * *\n" - "* * kroening@kroening.com * *\n" - "\n" - "Usage: Purpose:\n" - "\n" - " symex [-?] [-h] [--help] show help\n" - " symex file.c ... source file names\n" - "\n" - "Analysis options:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --show-properties show the properties, but don't run analysis\n" - " --property id only check one specific property\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --stop-on-fail stop analysis once a failed property is detected\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --trace give a counterexample trace for failed properties\n" - "\n" - "Frontend options:\n" - " -I path set include path (C/C++)\n" - " -D macro define preprocessor macro (C/C++)\n" - " --preprocess stop after preprocessing\n" - " --16, --32, --64 set width of int\n" - " --LP64, --ILP64, --LLP64,\n" - " --ILP32, --LP32 set width of int, long and pointers\n" - " --little-endian allow little-endian word-byte conversions\n" - " --big-endian allow big-endian word-byte conversions\n" - " --unsigned-char make \"char\" unsigned by default\n" - " --show-parse-tree show parse tree\n" - " --show-symbol-table show symbol table\n" - HELP_SHOW_GOTO_FUNCTIONS - " --drop-unused-functions drop functions trivially unreachable from main function\n" // NOLINT(*) - " --ppc-macos set MACOS/PPC architecture\n" - " --mm model set memory model (default: sc)\n" - " --arch set architecture (default: " - << configt::this_architecture() << ")\n" - " --os set operating system (default: " - << configt::this_operating_system() << ")\n" - #ifdef _WIN32 - " --gcc use GCC as preprocessor\n" - #endif - " --no-arch don't set up an architecture\n" - " --no-library disable built-in abstract C library\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --round-to-nearest IEEE floating point rounding mode (default)\n" - " --round-to-plus-inf IEEE floating point rounding mode\n" - " --round-to-minus-inf IEEE floating point rounding mode\n" - " --round-to-zero IEEE floating point rounding mode\n" - HELP_FUNCTIONS - "\n" - "Java Bytecode frontend options:\n" - JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP - "\n" - "Program instrumentation options:\n" - HELP_GOTO_CHECK - " --no-assertions ignore user assertions\n" - " --no-assumptions ignore user assumptions\n" - " --error-label label check that label is unreachable\n" - "\n" - "Symex options:\n" - " --unwind nr unwind nr times\n" - " --depth nr limit search depth\n" - " --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" - "\n" - "Other options:\n" - " --version show version and exit\n" - " --xml-ui use XML-formatted output\n" - " --verbosity # verbosity level\n" - "\n"; -} diff --git a/src/symex/symex_parse_options.h b/src/symex/symex_parse_options.h deleted file mode 100644 index c2aec7a175b..00000000000 --- a/src/symex/symex_parse_options.h +++ /dev/null @@ -1,89 +0,0 @@ -/*******************************************************************\ - -Module: Command Line Parsing - -Author: Daniel Kroening, kroening@kroening.com - -\*******************************************************************/ - -/// \file -/// Command Line Parsing - -#ifndef CPROVER_SYMEX_SYMEX_PARSE_OPTIONS_H -#define CPROVER_SYMEX_SYMEX_PARSE_OPTIONS_H - -#include -#include - -#include -#include -#include - -#include - -#include - -#include "path_search.h" - -class goto_functionst; -class optionst; - -#define SYMEX_OPTIONS \ - OPT_FUNCTIONS \ - "D:I:" \ - "(depth):(context-bound):(branch-bound):(unwind):(max-search-time):" \ - OPT_GOTO_CHECK \ - "(no-assertions)(no-assumptions)" \ - "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \ - "(little-endian)(big-endian)" \ - "(error-label):(verbosity):(no-library)" \ - "(version)" \ - "(bfs)(dfs)(locs)" \ - "(cover):" \ - "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \ - "(ppc-macos)(unsigned-char)" \ - "(string-abstraction)(no-arch)(arch):(floatbv)(fixedbv)" \ - "(round-to-nearest)(round-to-plus-inf)(round-to-minus-inf)(round-to-zero)" \ - "(show-locs)(show-vcc)(show-properties)" \ - "(drop-unused-functions)" \ - OPT_SHOW_GOTO_FUNCTIONS \ - "(property):(trace)(show-trace)(stop-on-fail)(eager-infeasibility)" \ - "(no-simplify)(no-unwinding-assertions)(no-propagation)" \ - JAVA_BYTECODE_LANGUAGE_OPTIONS - // the last line is for CBMC-regression testing only - -class symex_parse_optionst: - public parse_options_baset, - public messaget -{ -public: - virtual int doit(); - virtual void help(); - - symex_parse_optionst(int argc, const char **argv); - -protected: - ui_message_handlert ui_message_handler; - goto_modelt goto_model; - - void get_command_line_options(optionst &options); - bool process_goto_program(const optionst &options); - bool set_properties(); - - void report_success(); - void report_failure(); - void report_properties(const path_searcht::property_mapt &); - void report_cover(const path_searcht::property_mapt &); - void show_counterexample(const class goto_tracet &); - - void eval_verbosity(); - - std::string get_test(const goto_tracet &goto_trace); - - ui_message_handlert::uit get_ui() const - { - return ui_message_handler.get_ui(); - } -}; - -#endif // CPROVER_SYMEX_SYMEX_PARSE_OPTIONS_H