diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile index 5701431a37e..2c534c8749a 100644 --- a/regression/goto-analyzer/Makefile +++ b/regression/goto-analyzer/Makefile @@ -12,3 +12,9 @@ show: vim -o "$$dir/*.java" "$$dir/*.out"; \ fi; \ done; + +clean: + find . -name *.*~ | xargs rm -f + find . -name *.out | xargs rm -f + find . -name *.goto | xargs rm -f + rm -f tests.log diff --git a/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c b/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c new file mode 100644 index 00000000000..801a21535a9 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int i, j=20; + + if (j==20) + { + int x=1,y=2,z; + z=x+y; + assert(z==3); + } + +} diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc new file mode 100644 index 00000000000..7e9cac6056b --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation1.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 12, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c b/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c new file mode 100644 index 00000000000..ff139437bd8 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + int i=0, j=2; + + if (i==0) + { + i++; + j++; + } + assert(j!=3); +} diff --git a/regression/goto-analyzer/constant_propagation_02/original b/regression/goto-analyzer/constant_propagation_02/original new file mode 100644 index 00000000000..13a9e245c81 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_02/original @@ -0,0 +1,3 @@ +Task defaults to --show +Domain defaults to --constants +GOTO-ANALYSER version 5.5 64-bit x86_64 linux diff --git a/regression/goto-analyzer/constant_propagation_02/simplified b/regression/goto-analyzer/constant_propagation_02/simplified new file mode 100644 index 00000000000..6c722a607de --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_02/simplified @@ -0,0 +1,81 @@ +Reading GOTO program from `out.goto' +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +main /* main */ + // 0 file constant_propagation_02.c line 5 function main + signed int i; + // 1 file constant_propagation_02.c line 5 function main + i = 0; + // 2 file constant_propagation_02.c line 5 function main + signed int j; + // 3 file constant_propagation_02.c line 5 function main + j = 2; + // 4 file constant_propagation_02.c line 7 function main + IF FALSE THEN GOTO 1 + // 5 file constant_propagation_02.c line 9 function main + 0 = 1; + // 6 file constant_propagation_02.c line 10 function main + 2 = 3; + // 7 no location + 1: SKIP + // 8 file constant_propagation_02.c line 12 function main + ASSERT FALSE // assertion j!=3 + // 9 file constant_propagation_02.c line 12 function main + GOTO 2 + // 10 file constant_propagation_02.c line 12 function main + (void)0; + // 11 no location + 2: SKIP + // 12 file constant_propagation_02.c line 13 function main + dead j; + // 13 file constant_propagation_02.c line 13 function main + dead i; + // 14 file constant_propagation_02.c line 13 function main + main#return_value = NONDET(signed int); + // 15 file constant_propagation_02.c line 13 function main + END_FUNCTION +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +_start /* _start */ + // 16 no location + __CPROVER_initialize(); + // 17 file constant_propagation_02.c line 3 + main(); + // 18 file constant_propagation_02.c line 3 + return' = main#return_value; + // 19 file constant_propagation_02.c line 3 + dead main#return_value; + // 20 file constant_propagation_02.c line 3 + OUTPUT("return", return'); + // 21 no location + END_FUNCTION +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +__CPROVER_initialize /* __CPROVER_initialize */ + // 22 no location + // Labels: __CPROVER_HIDE + SKIP + // 23 file line 39 + __CPROVER_dead_object = NULL; + // 24 file line 38 + __CPROVER_deallocated = NULL; + // 25 file line 42 + __CPROVER_malloc_is_new_array = FALSE; + // 26 file line 40 + __CPROVER_malloc_object = NULL; + // 27 file line 41 + __CPROVER_malloc_size = 0ul; + // 28 file line 43 + __CPROVER_memory_leak = NULL; + // 29 file line 31 + __CPROVER_next_thread_id = 0ul; + // 30 file line 85 + __CPROVER_pipe_count = 0u; + // 31 file line 65 + __CPROVER_rounding_mode = 0; + // 32 file line 29 + __CPROVER_thread_id = 0ul; + // 33 file line 30 + __CPROVER_threads_exited = ARRAY_OF(FALSE); + // 34 no location + END_FUNCTION diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc new file mode 100644 index 00000000000..635f7dcf620 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation_02.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c b/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c new file mode 100644 index 00000000000..f08f6020d82 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + int i=0, j=2; + + if (i==0) + { + i++; + j++; + } + assert(j==3); +} diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc new file mode 100644 index 00000000000..37962658987 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation_03.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c b/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c new file mode 100644 index 00000000000..ca003ccd2b8 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + int i=0, j=2; + + if (i<50) + { + i++; + j++; + } + assert(j==3); +} diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc new file mode 100644 index 00000000000..2b23ac224f7 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation_04.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 6, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c b/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c new file mode 100644 index 00000000000..037fbbe0632 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c @@ -0,0 +1,13 @@ +#include + +int main() +{ + int i=0, j=2; + + if (i<50) + { + i++; + j++; + } + assert(j!=3); +} diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc new file mode 100644 index 00000000000..84712b085da --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_05/test.desc @@ -0,0 +1,8 @@ +CORE +constant_propagation_05.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_05.c line 12 function main, assertion j!=3: FAILURE (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c b/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c new file mode 100644 index 00000000000..d1d29427250 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c @@ -0,0 +1,30 @@ +#include + +int main() +{ + int i, j=20; + + if(i>=20) + assert(i>=10); // success + + if(i>=10 && i<=20) + assert(i!=30); // success + + if(i>=10 && i<=20) + assert(i!=15); // fails + + if(i<1 && i>10) + assert(0); // success + + if(i>=10 && j>=i) + assert(j>=10); // success + + if(i>=j) + assert(i>=j); // unknown + + if(i>10) + assert(i>=11); // success + + if(i<=100 && j=10: SUCCESS$ +^\[main.assertion.2\] file constant_propagation_06.c line 11 function main, assertion i!=30: SUCCESS$ +^\[main.assertion.3\] file constant_propagation_06.c line 14 function main, assertion i!=15: UNKNOWN$ +^\[main.assertion.4\] file constant_propagation_06.c line 17 function main, assertion 0: SUCCESS$ +^\[main.assertion.5\] file constant_propagation_06.c line 20 function main, assertion j>=10: SUCCESS$ +^\[main.assertion.6\] file constant_propagation_06.c line 23 function main, assertion i>=j: UNKNOWN$ +^\[main.assertion.7\] file constant_propagation_06.c line 26 function main, assertion i>=11: SUCCESS$ +^\[main.assertion.8\] file constant_propagation_06.c line 29 function main, assertion j<100: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c b/regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c new file mode 100644 index 00000000000..40b04edfdd0 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int i=0, j=2; + + while (i<50) + { + i++; + j++; + } + assert(i<51); +} + diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc new file mode 100644 index 00000000000..7494eafcd54 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -0,0 +1,8 @@ +CORE +constant_propagation_07.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c b/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c new file mode 100644 index 00000000000..3909e3889e4 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c @@ -0,0 +1,16 @@ +#include + +int main() +{ + int i=0, j=2; + + while (i<=50) + { + i++; + j++; + } + assert(i<50); + assert(i<51); + assert(i<52); +} + diff --git a/regression/goto-analyzer/constant_propagation_08/test.desc b/regression/goto-analyzer/constant_propagation_08/test.desc new file mode 100644 index 00000000000..994c2c532df --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_08/test.desc @@ -0,0 +1,10 @@ +FUTURE +constant_propagation_08.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_08.c line 12 function main, assertion i<50: UNKNOWN$ +^\[main.assertion.2\] file constant_propagation_08.c line 13 function main, assertion i<51: UNKNOWN$ +^\[main.assertion.3\] file constant_propagation_08.c line 14 function main, assertion i<52: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c b/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c new file mode 100644 index 00000000000..002e9063228 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c @@ -0,0 +1,14 @@ +#include + +int main() +{ + int i=0, j=2; + + while (i<=50) + { + i++; + j++; + } + assert(j<52); +} + diff --git a/regression/goto-analyzer/constant_propagation_09/test.desc b/regression/goto-analyzer/constant_propagation_09/test.desc new file mode 100644 index 00000000000..8cb0ec6a003 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_09/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation_09.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +******** Function main +^\[main.assertion.1\] file constant_propagation_09.c line 12 function main, assertion j<52: UNKNOWN$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c b/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c new file mode 100644 index 00000000000..169f7965b9d --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c @@ -0,0 +1,25 @@ +#include +int main() +{ + signed int i; + signed int j; + i = 0; + if(!(i >= 2)) + { + j = j + 1; + i = i + 1; + if(!(i >= 2)) + { + j = j + 1; + i = i + 1; + if(!(i >= 2)) + { + j = j + 1; + i = i + 1; + } + assert(!(i < 2)); + } + } + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc new file mode 100644 index 00000000000..7b78521a13d --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_10/test.desc @@ -0,0 +1,9 @@ +CORE +constant_propagation_10.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 4, assigns: 10, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c b/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c new file mode 100644 index 00000000000..3022a4f0f19 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c @@ -0,0 +1,17 @@ +#include +int main() +{ + int a[2]; + int i; + i = 0; + + if (i==0) + a[0]=1; + else + a[1]=2; + + assert(a[0]==1 || a[1]==2); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc new file mode 100644 index 00000000000..7c849326cf6 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -0,0 +1,9 @@ +FUTURE +constant_propagation_11.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 4, assigns: 13, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c b/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c new file mode 100644 index 00000000000..55ea9ac7fc2 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c @@ -0,0 +1,13 @@ +#include +int main() +{ + int a[2]={0,0}; + + if (a[0]==0) + a[0]=1; + + assert(a[0]==0); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc new file mode 100644 index 00000000000..ca5803363ad --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -0,0 +1,9 @@ +FUTURE +constant_propagation_12.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 0, assigns: 11, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c b/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c new file mode 100644 index 00000000000..ac5933e9177 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c @@ -0,0 +1,14 @@ +#include +int main() +{ + int a[2]={0,0}; + int i, y; + + if (a[0]==0) + a[0]=1; + + assert(a[0]==2); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc new file mode 100644 index 00000000000..22f10d125e3 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_13/test.desc @@ -0,0 +1,8 @@ +FUTURE +constant_propagation_13.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_13.c line 10 function main, assertion a\[0\]==2: FAILURE$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c b/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c new file mode 100644 index 00000000000..124d1e30a20 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c @@ -0,0 +1,13 @@ +#include +int main() +{ + int a[2]={0,0}; + + if (a[0]==0) + a[0]=1; + + assert(a[0]==1 /*|| a[0]==2*/); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc new file mode 100644 index 00000000000..a39a1f66cda --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_14/test.desc @@ -0,0 +1,9 @@ +FUTURE +constant_propagation_14.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 0$ +^UNKNOWN: assert: 0, assume: 0, goto: 0$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c b/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c new file mode 100644 index 00000000000..9a7e7692d62 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c @@ -0,0 +1,13 @@ +#include +int main() +{ + int i=0, y; + + if (i==0) + y=1; + + assert(y==1); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc new file mode 100644 index 00000000000..20d36183eb0 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_15/test.desc @@ -0,0 +1,9 @@ +FUTURE +constant_propagation_15.c +--constants --simplify out.goto +^EXIT=0$ +^SIGNAL=0$ +^SIMPLIFIED: assert: 1, assume: 0, goto: 1, assigns: 4, function calls: 0$ +^UNMODIFIED: assert: 0, assume: 0, goto: 2, assigns: 11, function calls: 2$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c b/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c new file mode 100644 index 00000000000..102cfd7f812 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c @@ -0,0 +1,13 @@ +#include +int main() +{ + int i=0, y; + + if (i==0) + y=1; + + assert(y==0); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_16/test.desc b/regression/goto-analyzer/constant_propagation_16/test.desc new file mode 100644 index 00000000000..b56c871deb4 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_16/test.desc @@ -0,0 +1,8 @@ +FUTURE +constant_propagation_16.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_16.c line 9 function main, assertion y==0: FAILURE (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c b/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c new file mode 100644 index 00000000000..8b426fe84b5 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c @@ -0,0 +1,16 @@ +#include +int main() +{ + int a[2]={0,0}; + + if (a[0]==0) + a[0]=1; + else + a[0]=2; + + assert(a[0]==1 || a[0]==2); + assert(a[0]==1 && a[0]==2); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_17/test.desc b/regression/goto-analyzer/constant_propagation_17/test.desc new file mode 100644 index 00000000000..acecb91eb0a --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_17/test.desc @@ -0,0 +1,9 @@ +FUTURE +constant_propagation_17.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_17.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: SUCCESS$ +^\[main.assertion.2\] file constant_propagation_17.c line 12 function main, assertion a\[0\]==1 && a\[0\]==2: FAILURE$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c b/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c new file mode 100644 index 00000000000..6639f9b5c81 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c @@ -0,0 +1,13 @@ +#include +int main() +{ + int a[2]={0,0}; + + if (a[0]==0) + a[0]=1; + + assert(a[0]==2); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_18/test.desc b/regression/goto-analyzer/constant_propagation_18/test.desc new file mode 100644 index 00000000000..7ea74c4d264 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_18/test.desc @@ -0,0 +1,8 @@ +FUTURE +constant_propagation_18.c +--constants --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file constant_propagation_18.c line 9 function main, assertion a\[0\]==2: FAILURE$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals1/intervals1.c b/regression/goto-analyzer/intervals1/intervals1.c index 026e572f8ef..cdec490fe6d 100644 --- a/regression/goto-analyzer/intervals1/intervals1.c +++ b/regression/goto-analyzer/intervals1/intervals1.c @@ -2,11 +2,11 @@ int main() { - int i, j; + int i, j=20; if(i>=20) assert(i>=10); - + if(i>=10 && i<=20) assert(i!=30); diff --git a/regression/goto-analyzer/intervals1/test.desc b/regression/goto-analyzer/intervals1/test.desc index 3e81f14023a..7aca700f7a5 100644 --- a/regression/goto-analyzer/intervals1/test.desc +++ b/regression/goto-analyzer/intervals1/test.desc @@ -1,6 +1,6 @@ CORE intervals1.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.1\] file intervals1.c line 8 function main, assertion i>=10: SUCCESS$ diff --git a/regression/goto-analyzer/intervals10/intervals10.c b/regression/goto-analyzer/intervals10/intervals10.c new file mode 100644 index 00000000000..b27cc6f2001 --- /dev/null +++ b/regression/goto-analyzer/intervals10/intervals10.c @@ -0,0 +1,21 @@ +#include + +int main() +{ + int i, j; + + if(i<=100 && j100); // fails + + if(i<=100 && j100: FAILURE (if reachable)$ +^\[main.assertion.4\] file intervals10.c line 17 function main, assertion j<99: UNKNOWN$ +^\[main.assertion.5\] file intervals10.c line 20 function main, assertion j==100: FAILURE (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals11/intervals11.c b/regression/goto-analyzer/intervals11/intervals11.c new file mode 100644 index 00000000000..2f061cd554d --- /dev/null +++ b/regression/goto-analyzer/intervals11/intervals11.c @@ -0,0 +1,43 @@ +#include +const int xLen = 10; +const int Alen = 2; +const int Blen = 1; +float nondet_float(); +int main() { + float A[] = {1.0f,-0.5f}; + float B[] = {1.0f}; + int i,j; + float x[xLen]; + float x_aux[xLen]; + float y[xLen]; + float y_aux[xLen]; + float total=0; + for (i=0;i=-1 && x[i]<=1); + x_aux[i]=0; + y_aux[i]=0; + } + for(i=0;i=1;j--) + x_aux[j] = x_aux[j-1]; + x_aux[0] = x[i]; + /* Num, x values */ + for (j = 0; j < Blen; j++) { + y[i] = y[i] + B[j]*x_aux[j]; + assert(y[i]>=-1.0f && y[i]<=1.0f); //success + } + /* Den, y values */ + for(j=0;j=-1.0f && y[i]<=1.0f); //fails + } + /* Update past y values */ + for(j=Alen-2;j>=1;j--) + y_aux[j] = y_aux[j-1]; + y_aux[0] = y[i]; + } +} + diff --git a/regression/goto-analyzer/intervals11/test.desc b/regression/goto-analyzer/intervals11/test.desc new file mode 100644 index 00000000000..039cbffbeb0 --- /dev/null +++ b/regression/goto-analyzer/intervals11/test.desc @@ -0,0 +1,9 @@ +FUTURE +intervals11.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals11.c line 30 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: UNKNOWN$ +^\[main.assertion.2\] file intervals11.c line 35 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: UNKNOWN$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals12/intervals12.c b/regression/goto-analyzer/intervals12/intervals12.c new file mode 100644 index 00000000000..15d865adf80 --- /dev/null +++ b/regression/goto-analyzer/intervals12/intervals12.c @@ -0,0 +1,16 @@ +#include + +int main (void) { + int i; + int j; + + if (i <= 0 && j < i) + assert(j < 0); + + if (j < i && i <= 0) + assert(j < 0); + + return 0; +} + + diff --git a/regression/goto-analyzer/intervals12/test.desc b/regression/goto-analyzer/intervals12/test.desc new file mode 100644 index 00000000000..59a724c28b5 --- /dev/null +++ b/regression/goto-analyzer/intervals12/test.desc @@ -0,0 +1,9 @@ +FUTURE +intervals12.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^[main.assertion.1] file intervals12.c line 8 function main, assertion j < 0: SUCCESS$ +^[main.assertion.2] file intervals12.c line 11 function main, assertion j < 0: SUCCESS$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals2/intervals2.c b/regression/goto-analyzer/intervals2/intervals2.c index d1eaf25240e..d542854bb6a 100644 --- a/regression/goto-analyzer/intervals2/intervals2.c +++ b/regression/goto-analyzer/intervals2/intervals2.c @@ -2,10 +2,10 @@ int main(){ int x; - if (x > 0) { - if (x < 20) { + if (x > 0 && x < 20) { + //if (x < 20) { assert(x > -10 && x < 100); - } + //} } return 0; } diff --git a/regression/goto-analyzer/intervals2/test.desc b/regression/goto-analyzer/intervals2/test.desc index 0c017f6b333..3341c4cd069 100644 --- a/regression/goto-analyzer/intervals2/test.desc +++ b/regression/goto-analyzer/intervals2/test.desc @@ -1,6 +1,6 @@ CORE intervals2.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.1\] file intervals2.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$ diff --git a/regression/goto-analyzer/intervals3/test.desc b/regression/goto-analyzer/intervals3/test.desc index 5db07df08a4..dceec17bc81 100644 --- a/regression/goto-analyzer/intervals3/test.desc +++ b/regression/goto-analyzer/intervals3/test.desc @@ -1,6 +1,6 @@ CORE intervals3.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.1\] file intervals3.c line 7 function main, assertion x > -10 || x < 100: SUCCESS$ diff --git a/regression/goto-analyzer/intervals4/test.desc b/regression/goto-analyzer/intervals4/test.desc index 9f56ff02403..92724fd69ee 100644 --- a/regression/goto-analyzer/intervals4/test.desc +++ b/regression/goto-analyzer/intervals4/test.desc @@ -1,6 +1,6 @@ CORE intervals4.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.1\] file intervals4.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$ diff --git a/regression/goto-analyzer/intervals5/test.desc b/regression/goto-analyzer/intervals5/test.desc index 42554724e2d..0213e7b3297 100644 --- a/regression/goto-analyzer/intervals5/test.desc +++ b/regression/goto-analyzer/intervals5/test.desc @@ -1,6 +1,6 @@ CORE intervals5.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ ^\[main.assertion.1\] file intervals5.c line 9 function main, assertion i >= 1 || i <= 2: SUCCESS$ diff --git a/regression/goto-analyzer/intervals6/test.desc b/regression/goto-analyzer/intervals6/test.desc index 14fd64f33dd..6e36b7948d2 100644 --- a/regression/goto-analyzer/intervals6/test.desc +++ b/regression/goto-analyzer/intervals6/test.desc @@ -1,8 +1,8 @@ -CORE +FUTURE intervals6.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: UNKNOWN$ +^\[main.assertion.1\] file intervals6.c line 7 function main, assertion x < -10 || x > 100: FAILURE (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals7/test.desc b/regression/goto-analyzer/intervals7/test.desc index aeeb24bd0a9..6a42b4a30ec 100644 --- a/regression/goto-analyzer/intervals7/test.desc +++ b/regression/goto-analyzer/intervals7/test.desc @@ -1,8 +1,8 @@ -CORE +FUTURE intervals7.c ---intervals +--intervals --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: UNKNOWN$ +^\[main.assertion.1\] file intervals7.c line 7 function main, assertion x < -10 && x > 100: FAILURE (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/intervals8/intervals8.c b/regression/goto-analyzer/intervals8/intervals8.c new file mode 100644 index 00000000000..4128ac07ce5 --- /dev/null +++ b/regression/goto-analyzer/intervals8/intervals8.c @@ -0,0 +1,9 @@ +#include + +int main(){ + int x; + if (x > 0 && x < 20) { + assert(x < -10 && x < 100); + } + return 0; +} diff --git a/regression/goto-analyzer/intervals8/test.desc b/regression/goto-analyzer/intervals8/test.desc new file mode 100644 index 00000000000..7500059a717 --- /dev/null +++ b/regression/goto-analyzer/intervals8/test.desc @@ -0,0 +1,8 @@ +FUTURE +intervals8.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals8.c line 6 function main, assertion x < -10 && x < 100: FAILURE (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals9/intervals9.c b/regression/goto-analyzer/intervals9/intervals9.c new file mode 100644 index 00000000000..27739c7aa28 --- /dev/null +++ b/regression/goto-analyzer/intervals9/intervals9.c @@ -0,0 +1,12 @@ +#include + +int main() +{ + int i; + + if(i>0) + if(i<3) + assert(i>=1 && i<=2); + + return 0; +} diff --git a/regression/goto-analyzer/intervals9/test.desc b/regression/goto-analyzer/intervals9/test.desc new file mode 100644 index 00000000000..33f92abcdb2 --- /dev/null +++ b/regression/goto-analyzer/intervals9/test.desc @@ -0,0 +1,8 @@ +CORE +intervals9.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file intervals9.c line 9 function main, assertion i>=1 && i<=2: SUCCESS$ +-- +^warning: ignoring diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index dd976334aae..721ed0de1fe 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -85,6 +85,153 @@ void ai_baset::output( /*******************************************************************\ +Function: ai_baset::output_json + + Inputs: The namespace and goto_functions + + Outputs: The JSON object + + Purpose: Output the domains for the whole program as JSON + +\*******************************************************************/ + +jsont ai_baset::output_json( + const namespacet &ns, + const goto_functionst &goto_functions) const +{ + json_objectt result; + + for(goto_functionst::function_mapt::const_iterator + f_it=goto_functions.function_map.begin(); + f_it!=goto_functions.function_map.end(); + f_it++) + { + if(f_it->second.body_available()) + { + result[as_string(f_it->first)] = output_json(ns, f_it->second.body, f_it->first); + } else { + result[as_string(f_it->first)] = json_arrayt(); + } + } + + return result; +} + +/*******************************************************************\ + +Function: ai_baset::output_json + + Inputs: The namespace, goto_program and it's identifier + + Outputs: The JSON object + + Purpose: Output the domains for a single function as JSON + +\*******************************************************************/ + +jsont ai_baset::output_json( + const namespacet &ns, + const goto_programt &goto_program, + const irep_idt &identifier) const +{ + json_arrayt contents; + + forall_goto_program_instructions(i_it, goto_program) + { + json_objectt location; + location["location_number"] = json_numbert(std::to_string(i_it->location_number)); + location["source_location"] = json_stringt(i_it->source_location.as_string()); + location["domain"] = find_state(i_it).output_json(*this, ns); + + // Ideally we need output_instruction_json + std::ostringstream out; + goto_program.output_instruction(ns, identifier, out, i_it); + location["instruction"] = json_stringt(out.str()); + + contents.push_back(location); + } + + return contents; +} + +/*******************************************************************\ + +Function: ai_baset::output_xml + + Inputs: The namespace and goto_functions + + Outputs: The XML object + + Purpose: Output the domains for the whole program as XML + +\*******************************************************************/ + +xmlt ai_baset::output_xml( + const namespacet &ns, + const goto_functionst &goto_functions) const +{ + xmlt program("program"); + + for(goto_functionst::function_mapt::const_iterator + f_it=goto_functions.function_map.begin(); + f_it!=goto_functions.function_map.end(); + f_it++) + { + xmlt function("function"); + function.set_attribute("name", as_string(f_it->first)); + function.set_attribute("body_available", f_it->second.body_available() ? "true" : "false"); + + if(f_it->second.body_available()) + { + function.new_element(output_xml(ns, f_it->second.body, f_it->first)); + } + + program.new_element(function); + } + + return program; +} + +/*******************************************************************\ + +Function: ai_baset::output_xml + + Inputs: The namespace, goto_program and it's identifier + + Outputs: The XML object + + Purpose: Output the domains for a single function as XML + +\*******************************************************************/ + +xmlt ai_baset::output_xml( + const namespacet &ns, + const goto_programt &goto_program, + const irep_idt &identifier) const +{ + xmlt function_body; + + forall_goto_program_instructions(i_it, goto_program) + { + xmlt location; + location.set_attribute("location_number", std::to_string(i_it->location_number)); + location.set_attribute("source_location", i_it->source_location.as_string()); + + location.new_element(find_state(i_it).output_xml(*this, ns)); + + // Ideally we need output_instruction_xml + std::ostringstream out; + goto_program.output_instruction(ns, identifier, out, i_it); + location.set_attribute("instruction", out.str()); + + function_body.new_element(location); + } + + return function_body; +} + +/*******************************************************************\ + Function: ai_baset::entry_state Inputs: diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 5265830c1e0..5db2e933661 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -11,6 +11,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + +#include +#include +#include #include @@ -53,6 +58,27 @@ class ai_domain_baset { } + virtual jsont output_json( + const ai_baset &ai, + const namespacet &ns) const + { + std::ostringstream out; + output(out, ai, ns); + json_stringt json(out.str()); + return json; + } + + virtual xmlt output_xml( + const ai_baset &ai, + const namespacet &ns) const + { + std::ostringstream out; + output(out, ai, ns); + xmlt xml("domain"); + xml.data = out.str(); + return xml; + } + // no states virtual void make_bottom() { @@ -74,6 +100,13 @@ class ai_domain_baset // // This computes the join between "this" and "b". // Return true if "this" has changed. + + // Used to evaluate or simplify conditions with respect to the domain + virtual exprt domain_simplify (const exprt &condition, + const namespacet &ns, + const bool lhs = false) const { + return condition; + } }; // don't use me -- I am just a base class @@ -162,6 +195,58 @@ class ai_baset output(ns, goto_function.body, "", out); } + + virtual jsont output_json( + const namespacet &ns, + const goto_functionst &goto_functions) const; + + inline jsont output_json( + const goto_modelt &goto_model) const + { + const namespacet ns(goto_model.symbol_table); + return output_json(ns, goto_model.goto_functions); + } + + inline jsont output_json( + const namespacet &ns, + const goto_programt &goto_program) const + { + return output_json(ns, goto_program, ""); + } + + inline jsont output_json( + const namespacet &ns, + const goto_functionst::goto_functiont &goto_function) const + { + return output_json(ns, goto_function.body, ""); + } + + + virtual xmlt output_xml( + const namespacet &ns, + const goto_functionst &goto_functions) const; + + inline xmlt output_xml( + const goto_modelt &goto_model) const + { + const namespacet ns(goto_model.symbol_table); + return output_xml(ns, goto_model.goto_functions); + } + + inline xmlt output_xml( + const namespacet &ns, + const goto_programt &goto_program) const + { + return output_xml(ns, goto_program, ""); + } + + inline xmlt output_xml( + const namespacet &ns, + const goto_functionst::goto_functiont &goto_function) const + { + return output_xml(ns, goto_function.body, ""); + } + protected: // overload to add a factory virtual void initialize(const goto_programt &); @@ -177,6 +262,17 @@ class ai_baset const irep_idt &identifier, std::ostream &out) const; + virtual jsont output_json( + const namespacet &ns, + const goto_programt &goto_program, + const irep_idt &identifier) const; + + virtual xmlt output_xml( + const namespacet &ns, + const goto_programt &goto_program, + const irep_idt &identifier) const; + + // the work-queue is sorted by location number typedef std::map working_sett; diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 7e66937efee..921d0458b9d 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -20,6 +20,61 @@ Author: Peter Schrammel /*******************************************************************\ +Function: concatenate_array_id + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +exprt concatenate_array_id( + const exprt &array, const exprt &index, + const typet &type) +{ + std::string a, idx, identifier; + a = array.get_string(ID_identifier); + + if (index.id()==ID_typecast) + idx = index.op0().get_string(ID_value); + else + idx = index.get_string(ID_value); + + mp_integer i=string2integer(idx); + identifier=a+"["+integer2string(i)+"]"; + symbol_exprt new_expr(identifier, type); + + return new_expr; +} + +/*******************************************************************\ + +Function: concatenate_array_id + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +exprt concatenate_array_id( + const exprt &array, const mp_integer &index, + const typet &type) +{ + std::string a, identifier; + a = array.get_string(ID_identifier); + identifier=a+"["+integer2string(index)+"]"; + symbol_exprt new_expr(identifier, type); + + return new_expr; +} + +/*******************************************************************\ + Function: constant_propagator_domaint::assign_rec Inputs: @@ -35,6 +90,7 @@ void constant_propagator_domaint::assign_rec( const exprt &lhs, const exprt &rhs, const namespacet &ns) { + const typet & lhs_type = ns.follow(lhs.type()); const typet & rhs_type = ns.follow(rhs.type()); #ifdef DEBUG @@ -42,7 +98,28 @@ void constant_propagator_domaint::assign_rec( << " := " << from_type(ns, "", rhs_type) << std::endl; #endif - if(lhs.id()==ID_symbol && rhs_type.id()!=ID_array + if(lhs.id()==ID_symbol && rhs.id()==ID_if) + { + exprt cond=rhs.op0(); + assert(cond.operands().size()==2); + if(values.is_constant(cond.op0()) + && values.is_constant(cond.op1())) + { + if(cond.op0().id()==ID_index) + { + exprt index=cond.op0(); + exprt new_expr=concatenate_array_id(index.op0(), index.op1(), index.type()); + values.replace_const(new_expr); + cond.op0()=new_expr; + cond = simplify_expr(cond,ns); + } + else + assert(0); + + assign(values, to_symbol_expr(lhs), cond, ns); + } + } + else if(lhs.id()==ID_symbol && rhs_type.id()!=ID_array && rhs_type.id()!=ID_struct && rhs_type.id()!=ID_union) { @@ -51,6 +128,27 @@ void constant_propagator_domaint::assign_rec( else values.set_to_top(to_symbol_expr(lhs)); } + else if(lhs.id()==ID_symbol && lhs_type.id()==ID_array + && rhs_type.id()==ID_array) + { + exprt new_expr; + mp_integer idx=0; + forall_operands(it, rhs) + { + new_expr=concatenate_array_id(lhs, idx, it->type()); + assign(values, to_symbol_expr(new_expr), *it, ns); + idx = idx +1; + } + } + else if (lhs.id()==ID_index) + { + if (values.is_constant(lhs.op1()) + && values.is_constant(rhs)) + { + exprt new_expr=concatenate_array_id(lhs.op0(), lhs.op1(), rhs.type()); + assign(values, to_symbol_expr(new_expr), rhs, ns); + } + } #if 0 else //TODO: could make field or array element-sensitive { @@ -85,7 +183,7 @@ void constant_propagator_domaint::transform( std::cout << "before:\n"; output(std::cout,ai,ns); #endif - + if(from->is_decl()) { const code_declt &code_decl=to_code_decl(from->code); @@ -105,13 +203,22 @@ void constant_propagator_domaint::transform( } else if(from->is_goto()) { - exprt g; + exprt g; if(from->get_target()==to) g = simplify_expr(from->guard, ns); else g = simplify_expr(not_exprt(from->guard), ns); - two_way_propagate_rec(g, ns); + if (g.is_false()) + values.set_to_bottom(); + else + { + //TODO: we need to support widening! + if (g.is_constant()) + values.set_to_top(); + else + two_way_propagate_rec(g, ns); + } } else if(from->is_dead()) { @@ -141,6 +248,7 @@ void constant_propagator_domaint::transform( else values.set_to_top(); } + #ifdef DEBUG std::cout << "after:\n"; output(std::cout,ai,ns); @@ -226,6 +334,56 @@ void constant_propagator_domaint::assign( /*******************************************************************\ +Function: constant_propagator_domaint::domain_simplify + + Inputs: The condition to simplify and its namespace. + + Outputs: The simplified condition. + + Purpose: Simplify the condition given context-sensitive knowledge from the domain. + +\*******************************************************************/ + +exprt constant_propagator_domaint::domain_simplify (const exprt &condition, + const namespacet &ns, + const bool lhs) const +{ + if (lhs) { + // For now do not simplify the left hand sides of assignments + return condition; + } else { + exprt e(condition); + values.replace_const(e); + return simplify_expr(e, ns); + } +} + +/*******************************************************************\ + +Function: constant_propagator_domaint::is_array_constant + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +bool constant_propagator_domaint::valuest::is_array_constant(const exprt &expr) const +{ + exprt new_expr = concatenate_array_id(expr.op0(), + expr.op1(), expr.type()); + + if (replace_const.expr_map.find(to_symbol_expr(new_expr).get_identifier()) == + replace_const.expr_map.end()) + return false; + + return true; +} + +/*******************************************************************\ + Function: constant_propagator_domaint::valuest::is_constant Inputs: @@ -251,6 +409,9 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const replace_const.expr_map.end()) return false; + if (expr.id()==ID_index) + return is_array_constant(expr); + if(expr.id()==ID_address_of) return is_constant_address_of(to_address_of_expr(expr).object()); @@ -397,47 +558,29 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) bool changed = false; - //set everything to top that is not in src - for(replace_symbolt::expr_mapt::const_iterator - it=replace_const.expr_map.begin(); - it!=replace_const.expr_map.end(); - ) + for(replace_symbolt::expr_mapt::iterator + it=replace_const.expr_map.begin(); + it!=replace_const.expr_map.end(); ) // no it++ { - if(src.replace_const.expr_map.find(it->first) == - src.replace_const.expr_map.end()) + const replace_symbolt::expr_mapt::const_iterator + b_it=src.replace_const.expr_map.find(it->first); + + if(b_it==src.replace_const.expr_map.end()) { //cannot use set_to_top here - replace_const.expr_map.erase(it++); + replace_const.expr_map.erase(it); changed = true; + break; } - else ++it; - } - - for(replace_symbolt::expr_mapt::const_iterator - it=src.replace_const.expr_map.begin(); - it!=src.replace_const.expr_map.end(); - ++it) - { - replace_symbolt::expr_mapt::iterator - c_it = replace_const.expr_map.find(it->first); - - if(c_it != replace_const.expr_map.end()) + else { - // values are different, set to top - if(c_it->second != it->second) - { - changed = set_to_top(it->first); - assert(changed); - } + const exprt previous=it->second; + replace_const.expr_map[b_it->first]=b_it->second; + if (it->second != previous) changed = true; + + it++; } - // is not in "this", ignore - else { } } - -#ifdef DEBUG - std::cout << "merged: " << changed << '\n'; -#endif - return changed; } @@ -529,6 +672,34 @@ void constant_propagator_ait::replace( /*******************************************************************\ +Function: constant_propagator_ait::replace_array_symbol + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void constant_propagator_ait::replace_array_symbol(exprt &expr) +{ + if (expr.id()==ID_index) + expr = concatenate_array_id(expr.op0(), + expr.op1(), expr.type()); + + Forall_operands(it, expr) + { + if (it->id()==ID_equal) + replace_array_symbol(it->op0()); + else if (it->id()==ID_index) + replace_array_symbol(expr.op0()); + } + +} + +/*******************************************************************\ + Function: constant_propagator_ait::replace Inputs: @@ -555,6 +726,7 @@ void constant_propagator_ait::replace( if(it->is_goto() || it->is_assume() || it->is_assert()) { + replace_array_symbol(it->guard); s_it->second.values.replace_const(it->guard); it->guard = simplify_expr(it->guard, ns); } @@ -563,6 +735,8 @@ void constant_propagator_ait::replace( exprt &rhs = to_code_assign(it->code).rhs(); s_it->second.values.replace_const(rhs); rhs = simplify_expr(rhs, ns); + if (rhs.id()==ID_constant) + rhs.add_source_location()=it->code.op0().source_location(); } else if(it->is_function_call()) { diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 7c7d7086373..a8540906914 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -19,6 +19,7 @@ class constant_propagator_domaint:public ai_domain_baset virtual void transform(locationt, locationt, ai_baset &, const namespacet &); virtual void output(std::ostream &, const ai_baset &, const namespacet &) const; bool merge(const constant_propagator_domaint &, locationt, locationt); + virtual exprt domain_simplify (const exprt &condition, const namespacet &ns, const bool lhs = false) const; struct valuest { @@ -52,6 +53,7 @@ class constant_propagator_domaint:public ai_domain_baset } bool is_constant(const exprt &expr) const; + bool is_array_constant(const exprt &expr) const; bool is_constant_address_of(const exprt &expr) const; bool set_to_top(const irep_idt &id); @@ -65,6 +67,7 @@ class constant_propagator_domaint:public ai_domain_baset replace_const.clear(); is_bottom = false; } + }; valuest values; @@ -106,6 +109,9 @@ class constant_propagator_ait:public ait protected: friend class constant_propagator_domaint; + void replace_array_symbol( + exprt &expr); + void replace( goto_functionst::goto_functiont &, const namespacet &); @@ -117,6 +123,7 @@ class constant_propagator_ait:public ait void replace_types_rec( const replace_symbolt &replace_const, exprt &expr); + }; #endif diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 44bcf2211eb..f237a97cb19 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -11,6 +11,8 @@ Date: August 2013 #include +#include + #include "goto_rw.h" #include "dependence_graph.h" @@ -351,6 +353,50 @@ void dep_graph_domaint::output( } } +/*******************************************************************\ + +Function: dep_graph_domaint::output_json + + Inputs: The abstract interpreter and the namespace. + + Outputs: The domain, formatted as a JSON object. + + Purpose: Outputs the current value of the domain. + +\*******************************************************************/ + + +jsont dep_graph_domaint::output_json( + const ai_baset &ai, + const namespacet &ns) const +{ + json_arrayt graph; + + for(dep_graph_domaint::depst::const_iterator cdi=control_deps.begin(); + cdi!=control_deps.end(); + ++cdi) + { + json_objectt &link=graph.push_back().make_object(); + link["location_number"] = json_numbert(std::to_string((*cdi)->location_number)); + link["source_location"] = json_stringt((*cdi)->source_location.as_string()); + link["type"]=json_stringt("control"); + } + + for(dep_graph_domaint::depst::const_iterator ddi=data_deps.begin(); + ddi!=data_deps.end(); + ++ddi) + { + json_objectt &link=graph.push_back().make_object(); + link["location_number"] = json_numbert(std::to_string((*ddi)->location_number)); + link["source_location"] = json_stringt((*ddi)->source_location.as_string()); + link["type"]=json_stringt("data"); + } + + return graph; +} + + + /*******************************************************************\ Function: dependence_grapht::add_dep diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 1b07b4ec140..c0d255ea662 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -43,6 +43,10 @@ class dep_graph_domaint:public ai_domain_baset const ai_baset &ai, const namespacet &ns) const; + virtual jsont output_json( + const ai_baset &ai, + const namespacet &ns) const; + void set_node_id(unsigned id) { node_id=id; diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 4f8aca54d4b..d6b1ac9e6b3 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -129,7 +129,7 @@ void interval_domaint::transform( /*******************************************************************\ -Function: interval_domaint::merge +Function: interval_domaint::join Inputs: @@ -139,10 +139,8 @@ Function: interval_domaint::merge \*******************************************************************/ -bool interval_domaint::merge( - const interval_domaint &b, - locationt from, - locationt to) +bool interval_domaint::join( + const interval_domaint &b) { if(b.bottom) return false; if(bottom) { *this=b; return true; } @@ -152,7 +150,9 @@ bool interval_domaint::merge( for(int_mapt::iterator it=int_map.begin(); it!=int_map.end(); ) // no it++ { - const int_mapt::const_iterator b_it=b.int_map.begin(); + //search for the variable that needs to be merged + //containers have different size and variable order + const int_mapt::const_iterator b_it=b.int_map.find(it->first); if(b_it==b.int_map.end()) { it=int_map.erase(it); @@ -500,3 +500,61 @@ exprt interval_domaint::make_expression(const symbol_exprt &src) const else return true_exprt(); } + +/*******************************************************************\ + +Function: interval_domaint::domain_simplify + + Inputs: The expression to simplify. + + Outputs: A simplified version of the expression. + + Purpose: Uses the domain to simplify a given expression using context-specific information. + +\*******************************************************************/ + +exprt interval_domaint::domain_simplify (const exprt &condition, + const namespacet &ns, + const bool lhs) const +{ + if (lhs) { + // For now do not simplify the left hand side of assignments + return condition; + } + + interval_domaint d(*this); + + //merge intervals to properly handle conjunction + if (condition.id()==ID_and) + { + interval_domaint a; + a.make_top(); + a.assume(condition,ns); + +#ifdef DEBUG + a.output(std::cout, interval_analysis, ns); + d.output(std::cout, interval_analysis, ns); +#endif + + if (!a.join(d)) + goto make_true; + } + else if (condition.id()==ID_symbol) + { + //TODO: we have to handle symbol expression + } + else + { + d.assume(not_exprt(condition), ns); + if(d.is_bottom()) + goto make_true; + } + + return condition; + + make_true: + exprt e; + e.make_true(); + return e; +} + diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index 0c3d9aa68c9..2d4bd7f7117 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -36,10 +36,15 @@ class interval_domaint:public ai_domain_baset const ai_baset &ai, const namespacet &ns) const; + bool join(const interval_domaint &b); + bool merge( const interval_domaint &b, locationt from, - locationt to); + locationt to) + { + return join(b); + } // no states virtual void make_bottom() @@ -75,7 +80,11 @@ class interval_domaint:public ai_domain_baset { return bottom; } - + + virtual exprt domain_simplify (const exprt &condition, + const namespacet &ns, + const bool lhs = false) const; + protected: bool bottom; diff --git a/src/analyses/is_threaded.h b/src/analyses/is_threaded.h index 88a785a71b9..38c36f8ad28 100644 --- a/src/analyses/is_threaded.h +++ b/src/analyses/is_threaded.h @@ -29,6 +29,11 @@ class is_threadedt return is_threaded_set.find(t)!=is_threaded_set.end(); } + inline bool operator()(void) const + { + return !is_threaded_set.empty(); + } + protected: typedef std::set is_threaded_sett; is_threaded_sett is_threaded_set; diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index fb58884a559..7d27be382e4 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -1,5 +1,6 @@ SRC = goto_analyzer_main.cpp goto_analyzer_parse_options.cpp \ taint_parser.cpp taint_analysis.cpp static_analyzer.cpp \ + static_show_domain.cpp static_simplifier.cpp \ unreachable_instructions.cpp OBJ += ../ansi-c/ansi-c$(LIBEXT) \ diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 5f5efcf942e..82ca1992c0e 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -30,6 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -47,6 +48,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "taint_analysis.h" #include "unreachable_instructions.h" #include "static_analyzer.h" +#include "static_show_domain.h" +#include "static_simplifier.h" /*******************************************************************\ @@ -218,6 +221,114 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("error-label")) options.set_option("error-label", cmdline.get_values("error-label")); #endif + + + // Output format choice + options.set_option("text", false); + options.set_option("json", false); + options.set_option("xml", false); + options.set_option("dot", false); + options.set_option("outfile", "-"); + + if (cmdline.isset("text")) + { + options.set_option("text", true); + options.set_option("outfile", cmdline.get_value("text")); + } + else if (cmdline.isset("json")) + { + options.set_option("json", true); + options.set_option("outfile", cmdline.get_value("json")); + } + else if (cmdline.isset("xml")) + { + options.set_option("xml", true); + options.set_option("outfile", cmdline.get_value("xml")); + } + else if (cmdline.isset("dot")) + { + options.set_option("dot", true); + options.set_option("outfile", cmdline.get_value("dot")); + } + else + { + options.set_option("text", true); + } + + + // Task options + options.set_option( "show", false); + options.set_option( "verify", false); + options.set_option("simplify", false); + + if (cmdline.isset("show") || + cmdline.isset("show-intervals") || + cmdline.isset("show-non-null")) + options.set_option("show", true); + else if (cmdline.isset("verify")) + options.set_option("verify", true); + else if (cmdline.isset("simplify")) + { + options.set_option("simplify", true); + options.set_option("outfile", cmdline.get_value("simplify")); + } + + if (!(options.get_bool_option("show") || + options.get_bool_option("verify") || + options.get_bool_option("simplify"))) + { + status() << "Task defaults to --show" << eom; + options.set_option("show", true); + } + + // For development allow slicing to be disabled in the simplify task + options.set_option("simplify-slicing", !(cmdline.isset("no-simplify-slicing"))); + + + // Abstract interpreter choice + options.set_option("flow-sensitive", false); + options.set_option("concurrent", false); + + if (cmdline.isset("flow-sensitive")) + options.set_option("flow-sensitive", true); + else if (cmdline.isset("concurrent")) + options.set_option("concurrent", true); + else + { + is_threadedt is_threaded(goto_model.goto_functions); + bool contains_concurrent_code = is_threaded(); + + options.set_option("flow-sensitive", !contains_concurrent_code); + options.set_option("concurrent", contains_concurrent_code); + } + + + // Domain choice + options.set_option("constants", false); + options.set_option("intervals", false); + options.set_option("non-null", false); + options.set_option("dependence-graph", false); + + if (cmdline.isset("intervals") || + cmdline.isset("show-intervals")) + options.set_option("intervals", true); + else if (cmdline.isset("non-null") || + cmdline.isset("show-non-null")) + options.set_option("non-null", true); + else if (cmdline.isset("constants")) + options.set_option("constants", true); + else if (cmdline.isset("dependence-graph")) + options.set_option("dependence-graph", true); + + if (!(options.get_bool_option("constants") || + options.get_bool_option("intervals") || + options.get_bool_option("non-null") || + options.get_bool_option("dependence-graph"))) + { + status() << "Domain defaults to --constants" << eom; + options.set_option("constants", true); + } + } /*******************************************************************\ @@ -234,128 +345,179 @@ Function: goto_analyzer_parse_optionst::doit int goto_analyzer_parse_optionst::doit() { - if(cmdline.isset("version")) - { - std::cout << CBMC_VERSION << std::endl; - return 0; - } - - // - // command line options - // - - optionst options; - get_command_line_options(options); - eval_verbosity(); - - // - // Print a banner - // - status() << "GOTO-ANALYSER version " CBMC_VERSION " " - << sizeof(void *)*8 << "-bit " - << config.this_architecture() << " " - << config.this_operating_system() << eom; - - register_languages(); + try + { + + if(cmdline.isset("version")) + { + std::cout << CBMC_VERSION << std::endl; + return 0; + } - goto_model.set_message_handler(get_message_handler()); - - if(goto_model(cmdline.args)) - return 6; + // + // command line options + // - if(process_goto_program(options)) - return 6; + optionst options; + get_command_line_options(options); + eval_verbosity(); + + // + // Print a banner + // + status() << "GOTO-ANALYSER version " CBMC_VERSION " " + << sizeof(void *)*8 << "-bit " + << config.this_architecture() << " " + << config.this_operating_system() << eom; + + register_languages(); + + goto_model.set_message_handler(get_message_handler()); + + if(goto_model(cmdline.args)) + return 6; + + if(process_goto_program(options)) + return 6; - if(cmdline.isset("taint")) - { - std::string taint_file=cmdline.get_value("taint"); + if(cmdline.isset("taint")) + { + std::string taint_file=cmdline.get_value("taint"); - if(cmdline.isset("show-taint")) + if(cmdline.isset("show-taint")) + { + taint_analysis(goto_model, taint_file, get_message_handler(), true, ""); + return 0; + } + else + { + std::string json_file=cmdline.get_value("json"); + bool result= + taint_analysis(goto_model, taint_file, get_message_handler(), false, json_file); + return result?10:0; + } + } + + if(cmdline.isset("unreachable-instructions")) { - taint_analysis(goto_model, taint_file, get_message_handler(), true, ""); + const std::string json_file=cmdline.get_value("json"); + + if(json_file.empty()) + unreachable_instructions(goto_model, false, std::cout); + else if(json_file=="-") + unreachable_instructions(goto_model, true, std::cout); + else + { + std::ofstream ofs(json_file); + if(!ofs) + { + error() << "Failed to open json output `" + << json_file << "'" << eom; + return 6; + } + + unreachable_instructions(goto_model, true, ofs); + } + return 0; } - else + + if(cmdline.isset("show-local-may-alias")) { - std::string json_file=cmdline.get_value("json"); - bool result= - taint_analysis(goto_model, taint_file, get_message_handler(), false, json_file); - return result?10:0; + namespacet ns(goto_model.symbol_table); + + forall_goto_functions(it, goto_model.goto_functions) + { + std::cout << ">>>>\n"; + std::cout << ">>>> " << it->first << '\n'; + std::cout << ">>>>\n"; + local_may_aliast local_may_alias(it->second); + local_may_alias.output(std::cout, it->second, ns); + std::cout << '\n'; + } + + return 0; } - } - if(cmdline.isset("unreachable-instructions")) - { - const std::string json_file=cmdline.get_value("json"); + label_properties(goto_model); + + if(cmdline.isset("show-properties")) + { + show_properties(goto_model, get_ui()); + return 0; + } - if(json_file.empty()) - unreachable_instructions(goto_model, false, std::cout); - else if(json_file=="-") - unreachable_instructions(goto_model, true, std::cout); + if(set_properties()) + return 7; + + + // Output file factory + std::ostream *out; + const std::string outfile = options.get_option("outfile"); + if (outfile == "-") + out = &std::cout; else { - std::ofstream ofs(json_file); - if(!ofs) + out = new std::ofstream(outfile); + if(!*out) { - error() << "Failed to open json output `" - << json_file << "'" << eom; - return 6; + error() << "Failed to open output file `" + << outfile << "'" << eom; + return 6; } - - unreachable_instructions(goto_model, true, ofs); } - return 0; - } - if(cmdline.isset("show-local-may-alias")) - { - namespacet ns(goto_model.symbol_table); - - forall_goto_functions(it, goto_model.goto_functions) + // Run the analysis + bool result = true; + if (options.get_bool_option("show")) + result = static_show_domain(goto_model, options, get_message_handler(), *out); + + else if (options.get_bool_option("verify")) + result = static_analyzer(goto_model, options, get_message_handler(), *out); + + else if (options.get_bool_option("simplify")) + result = static_simplifier(goto_model, options, get_message_handler(), *out); + else { - std::cout << ">>>>\n"; - std::cout << ">>>> " << it->first << '\n'; - std::cout << ">>>>\n"; - local_may_aliast local_may_alias(it->second); - local_may_alias.output(std::cout, it->second, ns); - std::cout << '\n'; + error() << "No task given" << eom; + return 6; } - - return 0; + + if (out != &std::cout) + delete out; + + return result?10:0; + + // Final defensive error case + error() << "no analysis option given -- consider reading --help" + << eom; + return 6; + } - - label_properties(goto_model); - - if(cmdline.isset("show-properties")) + catch(const char *e) { - show_properties(goto_model, get_ui()); - return 0; + error() << e << eom; + return 6; } - if(set_properties()) - return 7; + catch(const std::string e) + { + error() << e << eom; + return 6; + } - if(cmdline.isset("show-intervals")) + catch(int x) { - show_intervals(goto_model, std::cout); - return 0; + return x; } - - if(cmdline.isset("non-null") || - cmdline.isset("intervals")) + + catch(std::bad_alloc) { - optionst options; - options.set_option("json", cmdline.get_value("json")); - options.set_option("xml", cmdline.get_value("xml")); - bool result= - static_analyzer(goto_model, options, get_message_handler()); - return result?10:0; + error() << "Out of memory" << eom; + return 6; } - error() << "no analysis option given -- consider reading --help" - << eom; - return 6; } /*******************************************************************\ @@ -526,16 +688,30 @@ void goto_analyzer_parse_optionst::help() " goto-analyzer [-h] [--help] show help\n" " goto-analyzer file.c ... source file names\n" "\n" - "Analyses:\n" + "Task options:\n" + " --show run abstract interpreter and display domains\n" + " --verify run abstract interpreter and check assertions\n" + " --simplify file_name run abstract interpreter and simplify program\n" "\n" - " --taint file_name perform taint analysis using rules in given file\n" - " --unreachable-instructions list dead code\n" - " --intervals interval analysis\n" - " --non-null non-null analysis\n" + "Abstract interpreter options:\n" + " --flow-sensitive use flow-sensitive abstract interpreter\n" + " --concurrent use concurrent abstract interpreter\n" + "\n" + "Domain options:\n" + " --constants constant abstraction\n" + " --intervals interval abstraction\n" + " --non-null non-null abstraction\n" + " --dependence-graph dependency relation between instructions\n" "\n" - "Analysis options:\n" + "Output options:\n" + " --text file_name output results in plain text to given file\n" " --json file_name output results in JSON format to given file\n" " --xml file_name output results in XML format to given file\n" + " --dot file_name output results in DOT format to given file\n" + "\n" + "Other analyses:\n" + " --taint file_name perform taint analysis using rules in given file\n" + " --unreachable-instructions list dead code\n" "\n" "C/C++ frontend options:\n" " -I path set include path (C/C++)\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h index 7eba4c7b247..34d04be182f 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -33,10 +33,15 @@ class optionst; "(gcc)(arch):" \ "(taint):(show-taint)" \ "(show-local-may-alias)" \ - "(json):(xml):" \ + "(json):(xml):(text):(dot):" \ "(unreachable-instructions)" \ "(intervals)(show-intervals)" \ - "(non-null)(show-non-null)" + "(non-null)(show-non-null)" \ + "(constants)" \ + "(dependence-graph)" \ + "(show)(verify)(simplify):" \ + "(flow-sensitive)(concurrent)" \ + "(no-simplify-slicing)" class goto_analyzer_parse_optionst: public parse_options_baset, diff --git a/src/goto-analyzer/static_analyzer.cpp b/src/goto-analyzer/static_analyzer.cpp index 89e511288af..ce43c624952 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/src/goto-analyzer/static_analyzer.cpp @@ -8,25 +8,28 @@ Author: Daniel Kroening, kroening@kroening.com #include -#include #include #include #include +#include #include "static_analyzer.h" +template class static_analyzert:public messaget { public: static_analyzert( const goto_modelt &_goto_model, const optionst &_options, - message_handlert &_message_handler): + message_handlert &_message_handler, + std::ostream &_out): messaget(_message_handler), goto_functions(_goto_model.goto_functions), ns(_goto_model.symbol_table), - options(_options) + options(_options), + out(_out) { } @@ -36,38 +39,39 @@ class static_analyzert:public messaget const goto_functionst &goto_functions; const namespacet ns; const optionst &options; + std::ostream &out; // analyses - ait interval_analysis; + analyzerT domain; void plain_text_report(); - void json_report(const std::string &); - void xml_report(const std::string &); - - tvt eval(goto_programt::const_targett); + void json_report(); + void xml_report(); }; /*******************************************************************\ -Function: static_analyzert::operator() +Function: static_analyzert::operator() - Inputs: + Inputs: None. - Outputs: + Outputs: false on success, true on failure. - Purpose: + Purpose: Run the analysis, check the assertions and report in the correct format. \*******************************************************************/ -bool static_analyzert::operator()() +template +bool static_analyzert::operator()() { - status() << "performing interval analysis" << eom; - interval_analysis(goto_functions, ns); + status() << "Performing analysis" << eom; + domain(goto_functions, ns); - if(!options.get_option("json").empty()) - json_report(options.get_option("json")); - else if(!options.get_option("xml").empty()) - xml_report(options.get_option("xml")); + + if(options.get_bool_option("json")) + json_report(); + else if(options.get_bool_option("xml")) + xml_report(); else plain_text_report(); @@ -76,38 +80,18 @@ bool static_analyzert::operator()() /*******************************************************************\ -Function: static_analyzert::eval - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -tvt static_analyzert::eval(goto_programt::const_targett t) -{ - exprt guard=t->guard; - interval_domaint d=interval_analysis[t]; - d.assume(not_exprt(guard), ns); - if(d.is_bottom()) return tvt(true); - return tvt::unknown(); -} - -/*******************************************************************\ - -Function: static_analyzert::plain_text_report +Function: static_analyzert::plain_text_report - Inputs: + Inputs: None. - Outputs: + Outputs: Text report via out. - Purpose: + Purpose: Check the assertions and give results as text. \*******************************************************************/ -void static_analyzert::plain_text_report() +template +void static_analyzert::plain_text_report() { unsigned pass=0, fail=0, unknown=0; @@ -123,8 +107,8 @@ void static_analyzert::plain_text_report() forall_goto_program_instructions(i_it, f_it->second.body) { if(!i_it->is_assert()) continue; - - tvt r=eval(i_it); + + exprt simplified = domain[i_it].domain_simplify(i_it->guard, ns); result() << '[' << i_it->source_location.get_property_id() << ']' << ' '; @@ -133,45 +117,40 @@ void static_analyzert::plain_text_report() if(!i_it->source_location.get_comment().empty()) result() << ", " << i_it->source_location.get_comment(); result() << ": "; - if(r.is_true()) - result() << "SUCCESS"; - else if(r.is_false()) - result() << "FAILURE"; + if(simplified.is_true()) + { result() << "SUCCESS"; pass++; } + else if(simplified.is_false()) + { result() << "FAILURE (if reachable)"; fail++; } else - result() << "UNKNOWN"; + { result() << "UNKNOWN"; unknown++; } result() << eom; - if(r.is_true()) - pass++; - else if(r.is_false()) - fail++; - else - unknown++; } status() << '\n'; } - status() << "SUMMARY: " << pass << " pass, " << fail << " fail, " + status() << "SUMMARY: " << pass << " pass, " << fail << " fail if reachable, " << unknown << " unknown\n"; } /*******************************************************************\ -Function: static_analyzert::json_report +Function: static_analyzert::json_report - Inputs: + Inputs: None. - Outputs: + Outputs: JSON report via out. - Purpose: + Purpose: Check the assertions and give results as JSON. \*******************************************************************/ -void static_analyzert::json_report(const std::string &file_name) +template +void static_analyzert::json_report() { json_arrayt json_result; - + forall_goto_functions(f_it, goto_functions) { if(!f_it->second.body.has_assertion()) continue; @@ -182,15 +161,15 @@ void static_analyzert::json_report(const std::string &file_name) forall_goto_program_instructions(i_it, f_it->second.body) { if(!i_it->is_assert()) continue; - - tvt r=eval(i_it); + + exprt simplified = domain[i_it].domain_simplify(i_it->guard, ns); json_objectt &j=json_result.push_back().make_object(); - if(r.is_true()) + if(simplified.is_true()) j["status"]=json_stringt("SUCCESS"); - else if(r.is_false()) - j["status"]=json_stringt("FAILURE"); + else if(simplified.is_false()) + j["status"]=json_stringt("FAILURE (if reachable)"); else j["status"]=json_stringt("UNKNOWN"); @@ -200,32 +179,25 @@ void static_analyzert::json_report(const std::string &file_name) i_it->source_location.get_comment())); } } - - std::ofstream out(file_name); - if(!out) - { - error() << "failed to open JSON output file `" - << file_name << "'" << eom; - return; - } - status() << "Writing report to `" << file_name << "'" << eom; + status() << "Writing JSON report" << eom; out << json_result; } /*******************************************************************\ -Function: static_analyzert::xml_report +Function: static_analyzert::xml_report - Inputs: + Inputs: None. - Outputs: + Outputs: XML report via out. - Purpose: + Purpose: Check the assertions and give results as XML. \*******************************************************************/ -void static_analyzert::xml_report(const std::string &file_name) +template +void static_analyzert::xml_report() { xmlt xml_result; @@ -240,14 +212,14 @@ void static_analyzert::xml_report(const std::string &file_name) { if(!i_it->is_assert()) continue; - tvt r=eval(i_it); + exprt simplified = domain[i_it].domain_simplify(i_it->guard, ns); xmlt &x=xml_result.new_element("result"); - if(r.is_true()) + if(simplified.is_true()) x.set_attribute("status", "SUCCESS"); - else if(r.is_false()) - x.set_attribute("status", "FAILURE"); + else if(simplified.is_false()) + x.set_attribute("status", "FAILURE (if reachable)"); else x.set_attribute("status", "UNKNOWN"); @@ -257,15 +229,7 @@ void static_analyzert::xml_report(const std::string &file_name) } } - std::ofstream out(file_name); - if(!out) - { - error() << "failed to open XML output file `" - << file_name << "'" << eom; - return; - } - - status() << "Writing report to `" << file_name << "'" << eom; + status() << "Writing XML report" << eom; out << xml_result; } @@ -273,40 +237,64 @@ void static_analyzert::xml_report(const std::string &file_name) Function: static_analyzer - Inputs: + Inputs: The goto_model to check, options giving the domain and output, + the message handler and output stream. - Outputs: + Outputs: Report via out. - Purpose: + Purpose: Runs the analyzer, check assertions and generate a report. \*******************************************************************/ bool static_analyzer( const goto_modelt &goto_model, const optionst &options, - message_handlert &message_handler) -{ - return static_analyzert( - goto_model, options, message_handler)(); -} - -/*******************************************************************\ - -Function: show_intervals - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void show_intervals( - const goto_modelt &goto_model, + message_handlert &message_handler, std::ostream &out) { - ait interval_analysis; - interval_analysis(goto_model); - interval_analysis.output(goto_model, out); + if (options.get_bool_option("flow-sensitive")) + { + if (options.get_bool_option("constants")) + return static_analyzert > + (goto_model, options, message_handler, out)(); + + else if (options.get_bool_option("intervals")) + return static_analyzert > + (goto_model, options, message_handler, out)(); + + //else if (options.get_bool_option("non-null")) + // return static_analyzert > + // (goto_model, options, message_handler, out)(); + + else + goto fail; + } + else if (options.get_bool_option("concurrent")) + { + // Constant and interval don't have merge_shared yet +#if 0 + if (options.get_bool_option("constants")) + return static_analyzert > + (goto_model, options, message_handler, out)(); + + else if (options.get_bool_option("intervals")) + return static_analyzert > + (goto_model, options, message_handler, out)(); + + //else if (options.get_bool_option("non-null")) + // return static_analyzert > + // (goto_model, options, message_handler, out)(); + + else +#endif + goto fail; + } + else + goto fail; + + + fail : + messaget m(message_handler); + m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom; + return true; } diff --git a/src/goto-analyzer/static_analyzer.h b/src/goto-analyzer/static_analyzer.h index 02fa064ab11..72c6555d777 100644 --- a/src/goto-analyzer/static_analyzer.h +++ b/src/goto-analyzer/static_analyzer.h @@ -20,10 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com bool static_analyzer( const goto_modelt &, const optionst &, - message_handlert &); - -void show_intervals( - const goto_modelt &, + message_handlert &, std::ostream &); #endif diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp new file mode 100644 index 00000000000..df519f054cf --- /dev/null +++ b/src/goto-analyzer/static_show_domain.cpp @@ -0,0 +1,102 @@ +/*******************************************************************\ + +Module: + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#include + +#include +#include +#include + +#include +#include +#include + +#include "static_show_domain.h" + +/*******************************************************************\ + +Function: static_show_domain + + Inputs: The goto_model to analyze, options giving the domain and output, + the message handler and output stream. + + Outputs: The abstract domain via out. + + Purpose: Runs the analyzer and then prints out the domain. + +\*******************************************************************/ + +bool static_show_domain( + const goto_modelt &goto_model, + const optionst &options, + message_handlert &message_handler, + std::ostream &out) +{ + ai_baset *domain = NULL; + namespacet ns(goto_model.symbol_table); + + if (options.get_bool_option("flow-sensitive")) + { + if (options.get_bool_option("constants")) + domain = new ait(); + + else if (options.get_bool_option("intervals")) + domain = new ait(); + + //else if (options.get_bool_option("non-null")) + // domain = new ait(); + + else if (options.get_bool_option("dependence-graph")) + domain = new dependence_grapht(ns); + + } + else if (options.get_bool_option("concurrent")) + { + // Constant and interval don't have merge_shared yet +#if 0 + if (options.get_bool_option("constants")) + domain = new concurrency_aware_ait(); + + else if (options.get_bool_option("intervals")) + domain = new concurrency_aware_ait(); + + //else if (options.get_bool_option("non-null")) + // domain = new concurrency_aware_ait(); +#endif + } + + if (domain == NULL) + { + messaget m(message_handler); + m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom; + return true; + } + + //status() << "Performing analysis" << eom; + (*domain)(goto_model); + + + if(options.get_bool_option("json")) + out << domain->output_json(goto_model); + else if(options.get_bool_option("xml")) + out << domain->output_xml(goto_model); + else if(options.get_bool_option("dot") && options.get_bool_option("dependence-graph")) + { + dependence_grapht *d = dynamic_cast(domain); + assert(d != NULL); + + out << "digraph g {\n"; + d->output_dot(out); + out << "}\n"; + } + else + domain->output(goto_model, out); + + delete domain; + return false; +} diff --git a/src/goto-analyzer/static_show_domain.h b/src/goto-analyzer/static_show_domain.h new file mode 100644 index 00000000000..66681adf5e6 --- /dev/null +++ b/src/goto-analyzer/static_show_domain.h @@ -0,0 +1,26 @@ +/*******************************************************************\ + +Module: + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_STATIC_SHOW_DOMAIN_H +#define CPROVER_STATIC_SHOW_DOMAIN_H + +#include + +#include +#include +#include + +#include + +bool static_show_domain( + const goto_modelt &, + const optionst &, + message_handlert &, + std::ostream &); + +#endif diff --git a/src/goto-analyzer/static_simplifier.cpp b/src/goto-analyzer/static_simplifier.cpp new file mode 100644 index 00000000000..093d5ddf985 --- /dev/null +++ b/src/goto-analyzer/static_simplifier.cpp @@ -0,0 +1,307 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +//#define DEBUG + +#ifdef DEBUG +#include +#endif + +#include + +#include + +#include +#include + +#include +#include + +#include "static_simplifier.h" + +template +class static_simplifiert:public messaget +{ +public: + static_simplifiert( + goto_modelt &_goto_model, + const optionst &_options, + message_handlert &_message_handler, + std::ostream &_out): + messaget(_message_handler), + goto_functions(_goto_model.goto_functions), + ns(_goto_model.symbol_table), + options(_options), + out(_out) + { + } + + bool operator()(void); + +protected: + goto_functionst &goto_functions; + const namespacet ns; + const optionst &options; + std::ostream &out; + + // analyses + analyzerT domain; + + void simplify_program(void); + unsigned simplify_guard(goto_programt::instructionst::iterator &i_it); +}; + +/*******************************************************************\ + +Function: static_simplifiert::operator() + + Inputs: None. + + Outputs: false on success, true on failure. + + Purpose: Run the analysis, check the assertions and report in the correct format. + +\*******************************************************************/ + +template +bool static_simplifiert::operator()(void) +{ + status() << "Performing analysis" << eom; + domain(goto_functions, ns); + + status() << "Simplifying program" << eom; + simplify_program(); + + // Remove obviously unreachable things and (now) unconditional branches + if (options.get_bool_option("simplify-slicing")) + { + status() << "Removing unreachable instructions" << eom; + + remove_skip(goto_functions); // Remove goto false + goto_functions.update(); + + remove_unreachable(goto_functions); // Unconvert unreachable to skips + goto_functions.update(); + + remove_skip(goto_functions); // Remove all of the new skips + goto_functions.update(); + } + + status() << "Writing goto binary" << eom; + return write_goto_binary(out, ns.get_symbol_table(), goto_functions); +} + + +/*******************************************************************\ + +Function: static_simplifiert::simplify_guard + + Inputs: An iterator pointing to an instruction. + + Outputs: 1 if simplified, 0 if not. + + Purpose: Simplifies the instruction's guard using the information in the abstract domain. + +\*******************************************************************/ + +template +unsigned static_simplifiert::simplify_guard(goto_programt::instructionst::iterator &i_it) +{ + exprt simplified = domain[i_it].domain_simplify(i_it->guard, ns); + unsigned return_value = (simplified == i_it->guard) ? 0 : 1; + i_it->guard = simplified; + return return_value; +} + +/*******************************************************************\ + +Function: static_simplifiert::simplify_program + + Inputs: None. + + Outputs: None. + + Purpose: Simplifies the program using the information in the abstract domain. + +\*******************************************************************/ + +template +void static_simplifiert::simplify_program() +{ + struct counters { + unsigned asserts; + unsigned assumes; + unsigned gotos; + unsigned assigns; + unsigned function_calls; + }; + + counters simplified = {0,0,0,0,0}; + counters unmodified = {0,0,0,0,0}; + + Forall_goto_functions(f_it, goto_functions) + { + Forall_goto_program_instructions(i_it, f_it->second.body) + { + if (i_it->is_assert()) + { + unsigned result = simplify_guard(i_it); + simplified.asserts += result; + unmodified.asserts += (1 - result); + } + else if (i_it->is_assume()) + { + unsigned result = simplify_guard(i_it); + simplified.assumes += result; + unmodified.assumes += (1 - result); + } + else if (i_it->is_goto()) + { + unsigned result = simplify_guard(i_it); + simplified.gotos += result; + unmodified.gotos += (1 - result); + } + else if (i_it->is_assign()) + { + code_assignt assign(to_code_assign(i_it->code)); + + /* + ** Simplification needs to be aware of which side of the + ** expression it is handling as: + ** i = j + ** should simplify to i = 1, not to 0 = 1. + */ + + exprt simplified_lhs = domain[i_it].domain_simplify(assign.lhs(), ns, true); + exprt simplified_rhs = domain[i_it].domain_simplify(assign.rhs(), ns, false); + + unsigned result = (simplified_lhs == assign.lhs() && + simplified_rhs == assign.rhs()) ? 0 : 1; + simplified.assigns += result; + unmodified.assigns += (1 - result); + + assign.lhs() = simplified_lhs; + assign.rhs() = simplified_rhs; + i_it->code = assign; + } + else if (i_it->is_function_call()) + { + unsigned result = 0; + code_function_callt fcall(to_code_function_call(i_it->code)); + + exprt new_function = domain[i_it].domain_simplify(fcall.function(), ns); + result |= (new_function == fcall.function()) ? 0 : 1; + fcall.function() = new_function; + + exprt::operandst &args = fcall.arguments(); + + for(exprt::operandst::iterator o_it = args.begin(); + o_it != args.end(); ++o_it) + { + exprt new_arg = domain[i_it].domain_simplify(*o_it, ns); + result |= (new_arg == *o_it) ? 0 : 1; + *o_it = new_arg; + } + + i_it->code = fcall; + + simplified.function_calls += result; + unmodified.function_calls += (1 - result); + } + } + } + + //make sure the references are correct + goto_functions.update(); + + + status() << "SIMPLIFIED: " + << " assert: " << simplified.asserts + << ", assume: " << simplified.assumes + << ", goto: " << simplified.gotos + << ", assigns: " << simplified.assigns + << ", function calls: " << simplified.function_calls + << "\n" + << "UNMODIFIED: " + << " assert: " << unmodified.asserts + << ", assume: " << unmodified.assumes + << ", goto: " << unmodified.gotos + << ", assigns: " << unmodified.assigns + << ", function calls: " << unmodified.function_calls + << eom; + + return; +} + + + + +/*******************************************************************\ + +Function: static_simplifier + + Inputs: The goto_model to analyze and simplify, options giving the domain, + the message handler and output stream. + + Outputs: The simplified goto binary via out. + + Purpose: Runs the analyzer, simplifies and then outputs. + +\*******************************************************************/ + +bool static_simplifier( + goto_modelt &goto_model, + const optionst &options, + message_handlert &message_handler, + std::ostream &out) +{ + if (options.get_bool_option("flow-sensitive")) + { + if (options.get_bool_option("constants")) + return static_simplifiert > + (goto_model, options, message_handler, out)(); + + else if (options.get_bool_option("intervals")) + return static_simplifiert > + (goto_model, options, message_handler, out)(); + + //else if (options.get_bool_option("non-null")) + // return static_simplifiert > + // (goto_model, options, message_handler, out)(); + + else + goto fail; + } + else if (options.get_bool_option("concurrent")) + { + // Constant and interval don't have merge_shared yet +#if 0 + if (options.get_bool_option("constants")) + return static_simplifiert > + (goto_model, options, message_handler, out)(); + + else if (options.get_bool_option("intervals")) + return static_simplifiert > + (goto_model, options, message_handler, out)(); + + //else if (options.get_bool_option("non-null")) + // return static_simplifiert > + // (goto_model, options, message_handler, out)(); + + else +#endif + goto fail; + } + else + goto fail; + + fail : + messaget m(message_handler); + m.status() << "Task / Interpreter / Domain combination not supported" << messaget::eom; + return true; +} diff --git a/src/goto-analyzer/static_simplifier.h b/src/goto-analyzer/static_simplifier.h new file mode 100644 index 00000000000..0db31efea72 --- /dev/null +++ b/src/goto-analyzer/static_simplifier.h @@ -0,0 +1,26 @@ +/*******************************************************************\ + +Module: + +Author: Lucas Cordeiro, lucas.cordeiro@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_STATIC_SIMPLIFIER_H +#define CPROVER_STATIC_SIMPLIFIER_H + +#include + +#include +#include +#include + +#include + +bool static_simplifier( + goto_modelt &, + const optionst &, + message_handlert &, + std::ostream &); + +#endif diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp index 9f36259c83e..d9bee26e1ec 100644 --- a/src/goto-programs/remove_unreachable.cpp +++ b/src/goto-programs/remove_unreachable.cpp @@ -61,3 +61,9 @@ void remove_unreachable(goto_programt &goto_program) } } +void remove_unreachable(goto_functionst &goto_functions) +{ + Forall_goto_functions(f_it, goto_functions) + remove_unreachable(f_it->second.body); +} + diff --git a/src/goto-programs/remove_unreachable.h b/src/goto-programs/remove_unreachable.h index c40b0ded93f..603f7db8808 100644 --- a/src/goto-programs/remove_unreachable.h +++ b/src/goto-programs/remove_unreachable.h @@ -12,5 +12,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_functions.h" void remove_unreachable(goto_programt &goto_program); +void remove_unreachable(goto_functionst &goto_functions); #endif