diff --git a/regression/Makefile b/regression/Makefile index 296f583cc5e..71e3494e073 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -12,3 +12,10 @@ DIRS = ansi-c \ test: $(foreach var,$(DIRS), $(MAKE) -C $(var) test || exit 1;) + +clean: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + $(MAKE) -C "$$dir" clean; \ + fi; \ + done; diff --git a/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c b/regression/goto-analyzer/constant_propagation_01/main.c similarity index 84% rename from regression/goto-analyzer/constant_propagation_01/constant_propagation1.c rename to regression/goto-analyzer/constant_propagation_01/main.c index 801a21535a9..6689d8d4562 100644 --- a/regression/goto-analyzer/constant_propagation_01/constant_propagation1.c +++ b/regression/goto-analyzer/constant_propagation_01/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index 1eb849c3c7a..a4a79f28ab1 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -1,9 +1,9 @@ -FUTURE -constant_propagation1.c ---constants --simplify out.goto +CORE +main.c +--constants --simplify out.gb ^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$ +^Simplified: assert: 1, assume: 0, goto: 1, 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/main.c similarity index 81% rename from regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c rename to regression/goto-analyzer/constant_propagation_02/main.c index ff139437bd8..db0c8dc3f3e 100644 --- a/regression/goto-analyzer/constant_propagation_02/constant_propagation_02.c +++ b/regression/goto-analyzer/constant_propagation_02/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_02/original b/regression/goto-analyzer/constant_propagation_02/original deleted file mode 100644 index 13a9e245c81..00000000000 --- a/regression/goto-analyzer/constant_propagation_02/original +++ /dev/null @@ -1,3 +0,0 @@ -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 deleted file mode 100644 index 6c722a607de..00000000000 --- a/regression/goto-analyzer/constant_propagation_02/simplified +++ /dev/null @@ -1,81 +0,0 @@ -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 index 20cc5fcf86e..6a28820a4b0 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -1,9 +1,9 @@ -FUTURE -constant_propagation_02.c ---constants --simplify out.goto +CORE +main.c +--constants --simplify out.gb ^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$ +^Simplified: assert: 1, assume: 0, goto: 1, 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/main.c similarity index 81% rename from regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c rename to regression/goto-analyzer/constant_propagation_03/main.c index f08f6020d82..09a5434dead 100644 --- a/regression/goto-analyzer/constant_propagation_03/constant_propagation_03.c +++ b/regression/goto-analyzer/constant_propagation_03/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index 2225c1a666e..ffe6d41d638 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_03.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^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$ +^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/main.c similarity index 81% rename from regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c rename to regression/goto-analyzer/constant_propagation_04/main.c index ca003ccd2b8..2c6c3f39db1 100644 --- a/regression/goto-analyzer/constant_propagation_04/constant_propagation_04.c +++ b/regression/goto-analyzer/constant_propagation_04/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index 2510b3f8a5e..ffe6d41d638 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_04.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^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$ +^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/main.c similarity index 81% rename from regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c rename to regression/goto-analyzer/constant_propagation_05/main.c index 037fbbe0632..b740fc135c0 100644 --- a/regression/goto-analyzer/constant_propagation_05/constant_propagation_05.c +++ b/regression/goto-analyzer/constant_propagation_05/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/constant_propagation_05/test.desc b/regression/goto-analyzer/constant_propagation_05/test.desc index ddb22cc3616..e84fdb08b4f 100644 --- a/regression/goto-analyzer/constant_propagation_05/test.desc +++ b/regression/goto-analyzer/constant_propagation_05/test.desc @@ -1,8 +1,8 @@ FUTURE -constant_propagation_05.c +main.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)$ +^\[main.assertion.1\] file main.c line 12 function main, assertion j!=3: Failure (if reachable)$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_06/main.c b/regression/goto-analyzer/constant_propagation_06/main.c new file mode 100644 index 00000000000..6290aa89e6b --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_06/main.c @@ -0,0 +1,13 @@ + +int main() +{ + int i=0, j=2; + + while (i<50) + { + i++; + j++; + } + assert(i<51); +} + diff --git a/regression/goto-analyzer/constant_propagation_06/test.desc b/regression/goto-analyzer/constant_propagation_06/test.desc index 2c2596fe092..77a7349569f 100644 --- a/regression/goto-analyzer/constant_propagation_06/test.desc +++ b/regression/goto-analyzer/constant_propagation_06/test.desc @@ -1,15 +1,8 @@ -FUTURE -constant_propagation_06.c ---intervals --verify +CORE +main.c +--constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_06.c line 8 function main, assertion i>=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$ +^\[main.assertion.1\] file main.c line 11 function main, assertion i\s*<\s*51: Unknown$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c b/regression/goto-analyzer/constant_propagation_07/main.c similarity index 87% rename from regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c rename to regression/goto-analyzer/constant_propagation_07/main.c index 169f7965b9d..1fb6fee8e15 100644 --- a/regression/goto-analyzer/constant_propagation_10/constant_propagation_10.c +++ b/regression/goto-analyzer/constant_propagation_07/main.c @@ -1,10 +1,10 @@ -#include + int main() { signed int i; signed int j; i = 0; - if(!(i >= 2)) + if(!(i >= 2)) { j = j + 1; i = i + 1; diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 615893d4f78..c4b03cd8738 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -1,8 +1,9 @@ FUTURE -constant_propagation_07.c ---constants --verify +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_07.c line 12 function main, assertion i<51: UNKNOWN$ +^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_08/main.c similarity index 87% rename from regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c rename to regression/goto-analyzer/constant_propagation_08/main.c index 3022a4f0f19..295e23c636d 100644 --- a/regression/goto-analyzer/constant_propagation_11/constant_propagation_11.c +++ b/regression/goto-analyzer/constant_propagation_08/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]; diff --git a/regression/goto-analyzer/constant_propagation_08/test.desc b/regression/goto-analyzer/constant_propagation_08/test.desc index 994c2c532df..07a97596c15 100644 --- a/regression/goto-analyzer/constant_propagation_08/test.desc +++ b/regression/goto-analyzer/constant_propagation_08/test.desc @@ -1,10 +1,9 @@ FUTURE -constant_propagation_08.c ---intervals --verify +main.c +--constants --simplify out.gb ^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$ +^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_09/main.c similarity index 82% rename from regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c rename to regression/goto-analyzer/constant_propagation_09/main.c index 55ea9ac7fc2..9bd38159f67 100644 --- a/regression/goto-analyzer/constant_propagation_12/constant_propagation_12.c +++ b/regression/goto-analyzer/constant_propagation_09/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_09/test.desc b/regression/goto-analyzer/constant_propagation_09/test.desc index 6a1b75f0c1b..eebfe27dd49 100644 --- a/regression/goto-analyzer/constant_propagation_09/test.desc +++ b/regression/goto-analyzer/constant_propagation_09/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_09.c ---intervals --verify +main.c +--constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -******** Function main -^\[main.assertion.1\] file constant_propagation_09.c line 12 function main, assertion j<52: UNKNOWN$ +^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_10/main.c similarity index 84% rename from regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c rename to regression/goto-analyzer/constant_propagation_10/main.c index ac5933e9177..217faa4c9a7 100644 --- a/regression/goto-analyzer/constant_propagation_13/constant_propagation_13.c +++ b/regression/goto-analyzer/constant_propagation_10/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_10/test.desc b/regression/goto-analyzer/constant_propagation_10/test.desc index 52d98cb611b..527325b84bb 100644 --- a/regression/goto-analyzer/constant_propagation_10/test.desc +++ b/regression/goto-analyzer/constant_propagation_10/test.desc @@ -1,9 +1,8 @@ FUTURE -constant_propagation_10.c ---constants --simplify out.goto +main.c +--constants --verify ^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$ +^\[main.assertion.1\] file main.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_11/main.c similarity index 84% rename from regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c rename to regression/goto-analyzer/constant_propagation_11/main.c index 124d1e30a20..cefa0c479ab 100644 --- a/regression/goto-analyzer/constant_propagation_14/constant_propagation_14.c +++ b/regression/goto-analyzer/constant_propagation_11/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc index 7c849326cf6..4e9c8715429 100644 --- a/regression/goto-analyzer/constant_propagation_11/test.desc +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_11.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^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$ +^Simplified: assert: 1, assume: 0, goto: 0$ +^Unmodified: 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_12/main.c similarity index 80% rename from regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c rename to regression/goto-analyzer/constant_propagation_12/main.c index 9a7e7692d62..a8379b64712 100644 --- a/regression/goto-analyzer/constant_propagation_15/constant_propagation_15.c +++ b/regression/goto-analyzer/constant_propagation_12/main.c @@ -1,4 +1,4 @@ -#include + int main() { int i=0, y; diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index ca5803363ad..208b235ccd5 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_12.c ---constants --simplify out.goto +main.c +--constants --simplify out.gb ^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$ +^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_13/main.c similarity index 80% rename from regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c rename to regression/goto-analyzer/constant_propagation_13/main.c index 102cfd7f812..a4307c4d431 100644 --- a/regression/goto-analyzer/constant_propagation_16/constant_propagation_16.c +++ b/regression/goto-analyzer/constant_propagation_13/main.c @@ -1,4 +1,4 @@ -#include + int main() { int i=0, y; diff --git a/regression/goto-analyzer/constant_propagation_13/test.desc b/regression/goto-analyzer/constant_propagation_13/test.desc index 22f10d125e3..2d2e078a424 100644 --- a/regression/goto-analyzer/constant_propagation_13/test.desc +++ b/regression/goto-analyzer/constant_propagation_13/test.desc @@ -1,8 +1,8 @@ FUTURE -constant_propagation_13.c +main.c --constants --verify ^EXIT=0$ ^SIGNAL=0$ -^\[main.assertion.1\] file constant_propagation_13.c line 10 function main, assertion a\[0\]==2: FAILURE$ +^\[main.assertion.1\] file main.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_14/main.c similarity index 88% rename from regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c rename to regression/goto-analyzer/constant_propagation_14/main.c index 8b426fe84b5..7a659b87c60 100644 --- a/regression/goto-analyzer/constant_propagation_17/constant_propagation_17.c +++ b/regression/goto-analyzer/constant_propagation_14/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_14/test.desc b/regression/goto-analyzer/constant_propagation_14/test.desc index a39a1f66cda..fc3be910670 100644 --- a/regression/goto-analyzer/constant_propagation_14/test.desc +++ b/regression/goto-analyzer/constant_propagation_14/test.desc @@ -1,9 +1,9 @@ FUTURE -constant_propagation_14.c ---constants --simplify out.goto +main.c +--constants --verify ^EXIT=0$ ^SIGNAL=0$ -^SIMPLIFIED: assert: 1, assume: 0, goto: 0$ -^UNKNOWN: assert: 0, assume: 0, goto: 0$ +^\[main.assertion.1\] file main.c line 11 function main, assertion a\[0\]==1 || a\[0\]==2: Success$ +^\[main.assertion.2\] file main.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_15/main.c similarity index 82% rename from regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c rename to regression/goto-analyzer/constant_propagation_15/main.c index 6639f9b5c81..e3dd672831d 100644 --- a/regression/goto-analyzer/constant_propagation_18/constant_propagation_18.c +++ b/regression/goto-analyzer/constant_propagation_15/main.c @@ -1,4 +1,4 @@ -#include + int main() { int a[2]={0,0}; diff --git a/regression/goto-analyzer/constant_propagation_15/test.desc b/regression/goto-analyzer/constant_propagation_15/test.desc index 20d36183eb0..aba11ba0c06 100644 --- a/regression/goto-analyzer/constant_propagation_15/test.desc +++ b/regression/goto-analyzer/constant_propagation_15/test.desc @@ -1,9 +1,8 @@ FUTURE -constant_propagation_15.c ---constants --simplify out.goto +main.c +--constants --verify ^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$ +^\[main.assertion.1\] file main.c line 9 function main, assertion a\[0\]==2: Failure$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_16/main.c b/regression/goto-analyzer/constant_propagation_16/main.c new file mode 100644 index 00000000000..22fbac6a427 --- /dev/null +++ b/regression/goto-analyzer/constant_propagation_16/main.c @@ -0,0 +1,13 @@ + +void func() +{ + while(1) {} +} + +int main() +{ + func(); + + return 0; +} + diff --git a/regression/goto-analyzer/constant_propagation_16/test.desc b/regression/goto-analyzer/constant_propagation_16/test.desc index b56c871deb4..ef4ab9321a2 100644 --- a/regression/goto-analyzer/constant_propagation_16/test.desc +++ b/regression/goto-analyzer/constant_propagation_16/test.desc @@ -1,8 +1,7 @@ -FUTURE -constant_propagation_16.c ---constants --verify +CORE +main.c +--show --constants ^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_07/constant_propagation_07.c b/regression/goto-analyzer/constant_propagation_17/main.c similarity index 100% rename from regression/goto-analyzer/constant_propagation_07/constant_propagation_07.c rename to regression/goto-analyzer/constant_propagation_17/main.c diff --git a/regression/goto-analyzer/constant_propagation_17/test.desc b/regression/goto-analyzer/constant_propagation_17/test.desc index acecb91eb0a..76dc0fca897 100644 --- a/regression/goto-analyzer/constant_propagation_17/test.desc +++ b/regression/goto-analyzer/constant_propagation_17/test.desc @@ -1,9 +1,8 @@ -FUTURE -constant_propagation_17.c +CORE +main.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$ +^\[main.assertion.1\] file main.c line 12 function main, assertion i\s*<\s*51: (Unknown|Failure \(if reachable\))$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_18/test.desc b/regression/goto-analyzer/constant_propagation_18/test.desc deleted file mode 100644 index 7ea74c4d264..00000000000 --- a/regression/goto-analyzer/constant_propagation_18/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -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/test.desc b/regression/goto-analyzer/intervals1/test.desc deleted file mode 100644 index 5a9802eeb20..00000000000 --- a/regression/goto-analyzer/intervals1/test.desc +++ /dev/null @@ -1,15 +0,0 @@ -KNOWNBUG -intervals1.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals1.c line 8 function main, assertion i>=10: SUCCESS$ -^\[main.assertion.2\] file intervals1.c line 11 function main, assertion i!=30: SUCCESS$ -^\[main.assertion.3\] file intervals1.c line 14 function main, assertion i!=15: UNKNOWN$ -^\[main.assertion.4\] file intervals1.c line 17 function main, assertion 0: SUCCESS$ -^\[main.assertion.5\] file intervals1.c line 20 function main, assertion j>=10: SUCCESS$ -^\[main.assertion.6\] file intervals1.c line 23 function main, assertion i>=j: UNKNOWN$ -^\[main.assertion.7\] file intervals1.c line 26 function main, assertion i>=11: SUCCESS$ -^\[main.assertion.8\] file intervals1.c line 29 function main, assertion j<100: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals10/test.desc b/regression/goto-analyzer/intervals10/test.desc deleted file mode 100644 index 794198505f1..00000000000 --- a/regression/goto-analyzer/intervals10/test.desc +++ /dev/null @@ -1,12 +0,0 @@ -FUTURE -intervals10.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals10.c line 8 function main, assertion j<=100: SUCCESS$ -^\[main.assertion.2\] file intervals10.c line 11 function main, assertion j<101: SUCCESS$ -^\[main.assertion.3\] file intervals10.c line 14 function main, assertion j>100: 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/test.desc b/regression/goto-analyzer/intervals11/test.desc deleted file mode 100644 index 039cbffbeb0..00000000000 --- a/regression/goto-analyzer/intervals11/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -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/test.desc b/regression/goto-analyzer/intervals12/test.desc deleted file mode 100644 index 59a724c28b5..00000000000 --- a/regression/goto-analyzer/intervals12/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -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/test.desc b/regression/goto-analyzer/intervals2/test.desc deleted file mode 100644 index 65aae030db1..00000000000 --- a/regression/goto-analyzer/intervals2/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals2.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals2.c line 7 function main, assertion x > -10 && x < 100: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals3/test.desc b/regression/goto-analyzer/intervals3/test.desc deleted file mode 100644 index 69ded2182ee..00000000000 --- a/regression/goto-analyzer/intervals3/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals3.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals3.c line 7 function main, assertion x > -10 || x < 100: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals4/test.desc b/regression/goto-analyzer/intervals4/test.desc deleted file mode 100644 index 2b725180e3f..00000000000 --- a/regression/goto-analyzer/intervals4/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals4.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals4.c line 9 function main, assertion i >= 1 && i <= 2: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals5/test.desc b/regression/goto-analyzer/intervals5/test.desc deleted file mode 100644 index eb64fbc13d1..00000000000 --- a/regression/goto-analyzer/intervals5/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -intervals5.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[main.assertion.1\] file intervals5.c line 9 function main, assertion i >= 1 || i <= 2: SUCCESS$ --- -^warning: ignoring diff --git a/regression/goto-analyzer/intervals6/test.desc b/regression/goto-analyzer/intervals6/test.desc deleted file mode 100644 index 6e36b7948d2..00000000000 --- a/regression/goto-analyzer/intervals6/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -intervals6.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[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 deleted file mode 100644 index 6a42b4a30ec..00000000000 --- a/regression/goto-analyzer/intervals7/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -FUTURE -intervals7.c ---intervals --verify -^EXIT=0$ -^SIGNAL=0$ -^\[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/test.desc b/regression/goto-analyzer/intervals8/test.desc deleted file mode 100644 index 7500059a717..00000000000 --- a/regression/goto-analyzer/intervals8/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -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/test.desc b/regression/goto-analyzer/intervals9/test.desc deleted file mode 100644 index 37c33b97288..00000000000 --- a/regression/goto-analyzer/intervals9/test.desc +++ /dev/null @@ -1,8 +0,0 @@ -KNOWNBUG -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/regression/goto-analyzer/intervals1/intervals1.c b/regression/goto-analyzer/intervals_01/main.c similarity index 93% rename from regression/goto-analyzer/intervals1/intervals1.c rename to regression/goto-analyzer/intervals_01/main.c index cdec490fe6d..aeb37b99e07 100644 --- a/regression/goto-analyzer/intervals1/intervals1.c +++ b/regression/goto-analyzer/intervals_01/main.c @@ -1,9 +1,8 @@ -#include int main() { int i, j=20; - + if(i>=20) assert(i>=10); diff --git a/regression/goto-analyzer/intervals_01/test.desc b/regression/goto-analyzer/intervals_01/test.desc new file mode 100644 index 00000000000..af3180985b5 --- /dev/null +++ b/regression/goto-analyzer/intervals_01/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: Success$ +^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: Success$ +^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: Unknown$ +^\[main.assertion.4\] file main.c line 16 function main, assertion 0: Success$ +^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: Success$ +^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: Unknown$ +^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: Success$ +^\[main.assertion.8]\ file main.c line 28 function main, assertion j\s*<\s*100: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals2/intervals2.c b/regression/goto-analyzer/intervals_02/main.c similarity index 67% rename from regression/goto-analyzer/intervals2/intervals2.c rename to regression/goto-analyzer/intervals_02/main.c index d542854bb6a..00659353325 100644 --- a/regression/goto-analyzer/intervals2/intervals2.c +++ b/regression/goto-analyzer/intervals_02/main.c @@ -1,11 +1,8 @@ -#include int main(){ int x; if (x > 0 && x < 20) { - //if (x < 20) { assert(x > -10 && x < 100); - //} } return 0; } diff --git a/regression/goto-analyzer/intervals_02/test.desc b/regression/goto-analyzer/intervals_02/test.desc new file mode 100644 index 00000000000..fa4f926287f --- /dev/null +++ b/regression/goto-analyzer/intervals_02/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 && x < 100: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals3/intervals3.c b/regression/goto-analyzer/intervals_03/main.c similarity index 84% rename from regression/goto-analyzer/intervals3/intervals3.c rename to regression/goto-analyzer/intervals_03/main.c index bbaa3ce4e1e..de8c1eead32 100644 --- a/regression/goto-analyzer/intervals3/intervals3.c +++ b/regression/goto-analyzer/intervals_03/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_03/test.desc b/regression/goto-analyzer/intervals_03/test.desc new file mode 100644 index 00000000000..79042c334de --- /dev/null +++ b/regression/goto-analyzer/intervals_03/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x > -10 || x < 100: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals4/intervals4.c b/regression/goto-analyzer/intervals_04/main.c similarity index 80% rename from regression/goto-analyzer/intervals4/intervals4.c rename to regression/goto-analyzer/intervals_04/main.c index 790a5f1379f..1ca11e32143 100644 --- a/regression/goto-analyzer/intervals4/intervals4.c +++ b/regression/goto-analyzer/intervals_04/main.c @@ -1,4 +1,3 @@ -//#include int main() { diff --git a/regression/goto-analyzer/intervals_04/test.desc b/regression/goto-analyzer/intervals_04/test.desc new file mode 100644 index 00000000000..5bb03255f37 --- /dev/null +++ b/regression/goto-analyzer/intervals_04/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 && i <= 2: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals5/intervals5.c b/regression/goto-analyzer/intervals_05/main.c similarity index 80% rename from regression/goto-analyzer/intervals5/intervals5.c rename to regression/goto-analyzer/intervals_05/main.c index ed19ba71590..2cd79130dc9 100644 --- a/regression/goto-analyzer/intervals5/intervals5.c +++ b/regression/goto-analyzer/intervals_05/main.c @@ -1,4 +1,3 @@ -//#include int main() { diff --git a/regression/goto-analyzer/intervals_05/test.desc b/regression/goto-analyzer/intervals_05/test.desc new file mode 100644 index 00000000000..5c9af29a2b1 --- /dev/null +++ b/regression/goto-analyzer/intervals_05/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i >= 1 || i <= 2: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals6/intervals6.c b/regression/goto-analyzer/intervals_06/main.c similarity index 84% rename from regression/goto-analyzer/intervals6/intervals6.c rename to regression/goto-analyzer/intervals_06/main.c index e93240e7573..0e8a1f37c13 100644 --- a/regression/goto-analyzer/intervals6/intervals6.c +++ b/regression/goto-analyzer/intervals_06/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_06/test.desc b/regression/goto-analyzer/intervals_06/test.desc new file mode 100644 index 00000000000..2dc8d29a3b6 --- /dev/null +++ b/regression/goto-analyzer/intervals_06/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion x < -10 || x > 100: Failure (if reachable)$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals7/intervals7.c b/regression/goto-analyzer/intervals_07/main.c similarity index 84% rename from regression/goto-analyzer/intervals7/intervals7.c rename to regression/goto-analyzer/intervals_07/main.c index c893c413ad5..75da9413b97 100644 --- a/regression/goto-analyzer/intervals7/intervals7.c +++ b/regression/goto-analyzer/intervals_07/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_07/test.desc b/regression/goto-analyzer/intervals_07/test.desc new file mode 100644 index 00000000000..aa3962f39de --- /dev/null +++ b/regression/goto-analyzer/intervals_07/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.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/intervals_08/main.c similarity index 83% rename from regression/goto-analyzer/intervals8/intervals8.c rename to regression/goto-analyzer/intervals_08/main.c index 4128ac07ce5..3bcb7fe69c7 100644 --- a/regression/goto-analyzer/intervals8/intervals8.c +++ b/regression/goto-analyzer/intervals_08/main.c @@ -1,4 +1,3 @@ -#include int main(){ int x; diff --git a/regression/goto-analyzer/intervals_08/test.desc b/regression/goto-analyzer/intervals_08/test.desc new file mode 100644 index 00000000000..7b83ecd0f21 --- /dev/null +++ b/regression/goto-analyzer/intervals_08/test.desc @@ -0,0 +1,8 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.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/intervals_09/main.c similarity index 82% rename from regression/goto-analyzer/intervals9/intervals9.c rename to regression/goto-analyzer/intervals_09/main.c index 27739c7aa28..73b8e73dc85 100644 --- a/regression/goto-analyzer/intervals9/intervals9.c +++ b/regression/goto-analyzer/intervals_09/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_09/test.desc b/regression/goto-analyzer/intervals_09/test.desc new file mode 100644 index 00000000000..83776b8ae34 --- /dev/null +++ b/regression/goto-analyzer/intervals_09/test.desc @@ -0,0 +1,8 @@ +KNOWNBUG +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 9 function main, assertion i>=1 && i<=2: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals10/intervals10.c b/regression/goto-analyzer/intervals_10/main.c similarity index 92% rename from regression/goto-analyzer/intervals10/intervals10.c rename to regression/goto-analyzer/intervals_10/main.c index b27cc6f2001..b245b3f5b7c 100644 --- a/regression/goto-analyzer/intervals10/intervals10.c +++ b/regression/goto-analyzer/intervals_10/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_10/test.desc b/regression/goto-analyzer/intervals_10/test.desc new file mode 100644 index 00000000000..468ce13a550 --- /dev/null +++ b/regression/goto-analyzer/intervals_10/test.desc @@ -0,0 +1,12 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 8 function main, assertion j<=100: Success$ +^\[main.assertion.2\] file main.c line 11 function main, assertion j<101: Success$ +^\[main.assertion.3\] file main.c line 14 function main, assertion j>100: Failure (if reachable)$ +^\[main.assertion.4\] file main.c line 17 function main, assertion j<99: Unknown$ +^\[main.assertion.5\] file main.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/intervals_11/main.c similarity index 97% rename from regression/goto-analyzer/intervals11/intervals11.c rename to regression/goto-analyzer/intervals_11/main.c index 2f061cd554d..a6496ef764d 100644 --- a/regression/goto-analyzer/intervals11/intervals11.c +++ b/regression/goto-analyzer/intervals_11/main.c @@ -1,4 +1,4 @@ -#include + const int xLen = 10; const int Alen = 2; const int Blen = 1; diff --git a/regression/goto-analyzer/intervals_11/test.desc b/regression/goto-analyzer/intervals_11/test.desc new file mode 100644 index 00000000000..799ad36f64f --- /dev/null +++ b/regression/goto-analyzer/intervals_11/test.desc @@ -0,0 +1,9 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 30 function main, assertion y\[i\]>=-1.0f && y\[i\]<=1.0f: Unknown$ +^\[main.assertion.2\] file main.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/intervals_12/main.c similarity index 87% rename from regression/goto-analyzer/intervals12/intervals12.c rename to regression/goto-analyzer/intervals_12/main.c index 15d865adf80..506e118f898 100644 --- a/regression/goto-analyzer/intervals12/intervals12.c +++ b/regression/goto-analyzer/intervals_12/main.c @@ -1,4 +1,3 @@ -#include int main (void) { int i; diff --git a/regression/goto-analyzer/intervals_12/test.desc b/regression/goto-analyzer/intervals_12/test.desc new file mode 100644 index 00000000000..ffdf46857de --- /dev/null +++ b/regression/goto-analyzer/intervals_12/test.desc @@ -0,0 +1,9 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^[main.assertion.1] file main.c line 8 function main, assertion j < 0: Success$ +^[main.assertion.2] file main.c line 11 function main, assertion j < 0: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c b/regression/goto-analyzer/intervals_13/main.c similarity index 95% rename from regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c rename to regression/goto-analyzer/intervals_13/main.c index d1d29427250..b631969e8f6 100644 --- a/regression/goto-analyzer/constant_propagation_06/constant_propagation_06.c +++ b/regression/goto-analyzer/intervals_13/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_13/test.desc b/regression/goto-analyzer/intervals_13/test.desc new file mode 100644 index 00000000000..8d9720faf63 --- /dev/null +++ b/regression/goto-analyzer/intervals_13/test.desc @@ -0,0 +1,15 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 7 function main, assertion i\s*>=\s*10: Success$ +^\[main.assertion.2\] file main.c line 10 function main, assertion i\s*!=\s*30: Success$ +^\[main.assertion.3\] file main.c line 13 function main, assertion i\s*!=\s*15: Unknown$ +^\[main.assertion.4\] file main.c line 16 function main, assertion 0: Success$ +^\[main.assertion.5\] file main.c line 19 function main, assertion j\s*>=\s*10: Success$ +^\[main.assertion.6\] file main.c line 22 function main, assertion i\s*>=\s*j: Unknown$ +^\[main.assertion.7\] file main.c line 25 function main, assertion i\s*>=\s*11: Success$ +^\[main.assertion.8\] file main.c line 28 function main, assertion j\s*<\s*100: Success$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c b/regression/goto-analyzer/intervals_14/main.c similarity index 86% rename from regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c rename to regression/goto-analyzer/intervals_14/main.c index 3909e3889e4..7e4d53d5e06 100644 --- a/regression/goto-analyzer/constant_propagation_08/constant_propagation_08.c +++ b/regression/goto-analyzer/intervals_14/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_14/test.desc b/regression/goto-analyzer/intervals_14/test.desc new file mode 100644 index 00000000000..20a01bf3e12 --- /dev/null +++ b/regression/goto-analyzer/intervals_14/test.desc @@ -0,0 +1,10 @@ +FUTURE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 12 function main, assertion i<50: Unknown$ +^\[main.assertion.2\] file main.c line 13 function main, assertion i<51: Unknown$ +^\[main.assertion.3\] file main.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/intervals_15/main.c similarity index 82% rename from regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c rename to regression/goto-analyzer/intervals_15/main.c index 002e9063228..52ef248b772 100644 --- a/regression/goto-analyzer/constant_propagation_09/constant_propagation_09.c +++ b/regression/goto-analyzer/intervals_15/main.c @@ -1,4 +1,3 @@ -#include int main() { diff --git a/regression/goto-analyzer/intervals_15/test.desc b/regression/goto-analyzer/intervals_15/test.desc new file mode 100644 index 00000000000..e61667afcd4 --- /dev/null +++ b/regression/goto-analyzer/intervals_15/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: Unknown$ +-- +^warning: ignoring diff --git a/regression/goto-analyzer/intervals_16/main.c b/regression/goto-analyzer/intervals_16/main.c new file mode 100644 index 00000000000..52ef248b772 --- /dev/null +++ b/regression/goto-analyzer/intervals_16/main.c @@ -0,0 +1,13 @@ + +int main() +{ + int i=0, j=2; + + while (i<=50) + { + i++; + j++; + } + assert(j<52); +} + diff --git a/regression/goto-analyzer/intervals_16/test.desc b/regression/goto-analyzer/intervals_16/test.desc new file mode 100644 index 00000000000..c23e2bcf4f5 --- /dev/null +++ b/regression/goto-analyzer/intervals_16/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--intervals --verify +^EXIT=0$ +^SIGNAL=0$ +^\[main.assertion.1\] file main.c line 11 function main, assertion j\s*<\s*52: (Unknown|Failure \(if reachable\))$ +-- +^warning: ignoring diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 690b119e83c..9be0609687f 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -22,7 +22,6 @@ SRC = ai.cpp \ locals.cpp \ natural_loops.cpp \ reaching_definitions.cpp \ - replace_symbol_ext.cpp \ static_analysis.cpp \ uninitialized_domain.cpp \ # Empty last line diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp index 45d4b83c92c..36991b63c96 100644 --- a/src/analyses/ai.cpp +++ b/src/analyses/ai.cpp @@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include #include @@ -18,6 +19,51 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ +Function: ai_domain_baset::output_json + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +jsont ai_domain_baset::output_json( + const ai_baset &ai, + const namespacet &ns) const +{ + std::ostringstream out; + output(out, ai, ns); + json_stringt json(out.str()); + return json; +} + +/*******************************************************************\ + +Function: ai_domain_baset::output_xml + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +xmlt ai_domain_baset::output_xml( + const ai_baset &ai, + const namespacet &ns) const +{ + std::ostringstream out; + output(out, ai, ns); + xmlt xml("abstract_state"); + xml.data=out.str(); + return xml; +} + +/*******************************************************************\ + Function: ai_baset::output Inputs: @@ -139,7 +185,7 @@ jsont ai_baset::output_json( json_numbert(std::to_string(i_it->location_number)); location["sourceLocation"]= json_stringt(i_it->source_location.as_string()); - location["domain"]=find_state(i_it).output_json(*this, ns); + location["abstractState"]=find_state(i_it).output_json(*this, ns); // Ideally we need output_instruction_json std::ostringstream out; @@ -526,7 +572,12 @@ bool ai_baset::do_function_call( assert(l_end->is_end_function()); // do edge from end of function to instruction after call - std::unique_ptr tmp_state(make_temporary_state(get_state(l_end))); + const statet &end_state=get_state(l_end); + + if(end_state.is_bottom()) + return false; // function exit point not reachable + + std::unique_ptr tmp_state(make_temporary_state(end_state)); tmp_state->transform(l_end, l_return, *this, ns); // Propagate those diff --git a/src/analyses/ai.h b/src/analyses/ai.h index 2894cde3b10..d7393c8d9ef 100644 --- a/src/analyses/ai.h +++ b/src/analyses/ai.h @@ -11,10 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include #include +#include #include @@ -40,9 +40,9 @@ class ai_domain_baset // how function calls are treated: // a) there is an edge from each call site to the function head - // b) there is an edge from the last instruction (END_FUNCTION) - // of the function to the instruction _following_ the call site - // (this also needs to set the LHS, if applicable) + // b) there is an edge from the last instruction (END_FUNCTION) of + // the function to the instruction _following_ the call site (this + // also needs to set the LHS, if applicable) virtual void transform( locationt from, @@ -59,24 +59,11 @@ 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; - } + const namespacet &ns) const; 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; - } + const namespacet &ns) const; // no states virtual void make_bottom()=0; @@ -88,12 +75,31 @@ class ai_domain_baset // a reasonable entry-point state virtual void make_entry()=0; + virtual bool is_bottom() const=0; + + // the analysis doesn't use this, + // and domains may refuse to implement it. + virtual bool is_top() const=0; + // also add // // bool merge(const T &b, locationt from, locationt to); // // This computes the join between "this" and "b". // Return true if "this" has changed. + + // This method allows an expression to be simplified / evaluated using the + // current state. It is used to evaluate assertions and in program + // simplification + + // return true if unchanged + virtual bool ai_simplify( + exprt &condition, + const namespacet &ns, + const bool lhs=false) const + { + return true; + } }; // don't use me -- I am just a base class @@ -208,7 +214,6 @@ class ai_baset return output_json(ns, goto_function.body, ""); } - virtual xmlt output_xml( const namespacet &ns, const goto_functionst &goto_functions) const; diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp index 6735d558cc3..81d3fbb062c 100644 --- a/src/analyses/constant_propagator.cpp +++ b/src/analyses/constant_propagator.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Constant Propagation +Module: Constant propagation Author: Peter Schrammel @@ -13,66 +13,12 @@ Author: Peter Schrammel #include #include #include +#include #include "constant_propagator.h" /*******************************************************************\ -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: @@ -85,73 +31,23 @@ Function: constant_propagator_domaint::assign_rec void constant_propagator_domaint::assign_rec( valuest &values, - const exprt &lhs, const exprt &rhs, + 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()); + if(lhs.id()!=ID_symbol) + return; -#ifdef DEBUG - std::cout << "assign: " << from_expr(ns, "", lhs) - << " := " << from_type(ns, "", rhs_type) << std::endl; -#endif + const symbol_exprt &s=to_symbol_expr(lhs); - 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); + exprt tmp=rhs; + values.replace_const(tmp); + simplify(tmp, ns); - 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) - { - if(values.is_constant(rhs)) - assign(values, to_symbol_expr(lhs), rhs, ns); - 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 - { - } -#endif + if(tmp.is_constant()) + values.set_to(s, tmp); + else + values.set_to_top(s); } /*******************************************************************\ @@ -172,16 +68,37 @@ void constant_propagator_domaint::transform( ai_baset &ai, const namespacet &ns) { - #ifdef DEBUG +#ifdef DEBUG + std::cout << "Transform from/to:\n"; std::cout << from->location_number << " --> " << to->location_number << '\n'; - #endif +#endif #ifdef DEBUG - std::cout << "before:\n"; + std::cout << "Before:\n"; output(std::cout, ai, ns); #endif + // When the domain is used with constant_propagator_ait, + // information about dirty variables and config flags are + // available. Otherwise, the below will be null and we use default + // values + const constant_propagator_ait *cp= + dynamic_cast(&ai); + + bool have_dirty=false; + bool ignore_unresolved_calls=false; + + if(cp!=nullptr) + { + have_dirty=true; + ignore_unresolved_calls=cp->ignore_unresolved_calls; + } + + // assert(!values.is_bottom); + if(values.is_bottom) + return; + if(from->is_decl()) { const code_declt &code_decl=to_code_decl(from->code); @@ -191,8 +108,8 @@ void constant_propagator_domaint::transform( else if(from->is_assign()) { const code_assignt &assignment=to_code_assign(from->code); - const exprt &lhs = assignment.lhs(); - const exprt &rhs = assignment.rhs(); + const exprt &lhs=assignment.lhs(); + const exprt &rhs=assignment.rhs(); assign_rec(values, lhs, rhs, ns); } else if(from->is_assume()) @@ -204,19 +121,16 @@ void constant_propagator_domaint::transform( exprt g; if(from->get_target()==to) - g = simplify_expr(from->guard, ns); + g=simplify_expr(from->guard, ns); else - g = simplify_expr(not_exprt(from->guard), ns); + g=simplify_expr(not_exprt(from->guard), ns); - if (g.is_false()) + 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); + two_way_propagate_rec(g, ns); + assert(!values.is_bottom); // for now } } else if(from->is_dead()) @@ -226,35 +140,102 @@ void constant_propagator_domaint::transform( } else if(from->is_function_call()) { - const exprt &function=to_code_function_call(from->code).function(); + const code_function_callt &function_call=to_code_function_call(from->code); + const exprt &function=function_call.function(); + + locationt next=from; + next++; if(function.id()==ID_symbol) { - const irep_idt &identifier=to_symbol_expr(function).get_identifier(); - - if(identifier=="__CPROVER_set_must" || - identifier=="__CPROVER_get_must" || - identifier=="__CPROVER_set_may" || - identifier=="__CPROVER_get_may" || - identifier=="__CPROVER_cleanup" || - identifier=="__CPROVER_clear_may" || - identifier=="__CPROVER_clear_must") + // called function identifier + const symbol_exprt &symbol_expr=to_symbol_expr(function); + const irep_idt id=symbol_expr.get_identifier(); + + if(to==next) { + if(id==CPROVER_PREFIX "set_must" || + id==CPROVER_PREFIX "get_must" || + id==CPROVER_PREFIX "set_may" || + id==CPROVER_PREFIX "get_may" || + id==CPROVER_PREFIX "cleanup" || + id==CPROVER_PREFIX "clear_may" || + id==CPROVER_PREFIX "clear_must") + { + // no effect on constants + } + else + { + if(!ignore_unresolved_calls) + { + if(have_dirty) + values.set_dirty_to_top(cp->dirty, ns); + else + values.set_to_top(); + } + } } else - values.set_to_top(); + { + // we have an actual call + + // parameters of called function + const symbolt &symbol=ns.lookup(id); + const code_typet &code_type=to_code_type(symbol.type); + const code_typet::parameterst ¶meters=code_type.parameters(); + + const code_function_callt::argumentst &arguments= + function_call.arguments(); + + code_typet::parameterst::const_iterator p_it=parameters.begin(); + for(const auto &arg : arguments) + { + if(p_it==parameters.end()) + break; + + const symbol_exprt parameter_expr(p_it->get_identifier(), arg.type()); + assign_rec(values, parameter_expr, arg, ns); + + ++p_it; + } + } } else - values.set_to_top(); + { + // unresolved call + + assert(to==next); + + if(!ignore_unresolved_calls) + { + if(have_dirty) + values.set_dirty_to_top(cp->dirty, ns); + else + values.set_to_top(); + } + } + } + else if(from->is_end_function()) + { + // erase parameters + + const irep_idt id=from->function; + const symbolt &symbol=ns.lookup(id); + + const code_typet &type=to_code_type(symbol.type); + + for(const auto ¶m : type.parameters()) + values.set_to_top(param.get_identifier()); } + assert(from->is_goto() || !values.is_bottom); + #ifdef DEBUG - std::cout << "after:\n"; + std::cout << "After:\n"; output(std::cout, ai, ns); #endif } - /*******************************************************************\ Function: constant_propagator_domaint::two_way_propagate_rec @@ -274,8 +255,11 @@ bool constant_propagator_domaint::two_way_propagate_rec( #ifdef DEBUG std::cout << "two_way_propagate_rec: " << from_expr(ns, "", expr) << '\n'; #endif - bool change = false; + bool change=false; + + // this seems to be buggy at present +#if 0 if(expr.id()==ID_and) { // need a fixed point here to get the most out of it @@ -285,74 +269,63 @@ bool constant_propagator_domaint::two_way_propagate_rec( forall_operands(it, expr) if(two_way_propagate_rec(*it, ns)) - change = true; + change=true; } while(change); } else if(expr.id()==ID_equal) { - const exprt &lhs = expr.op0(); - const exprt &rhs = expr.op1(); + const exprt &lhs=expr.op0(); + const exprt &rhs=expr.op1(); // two-way propagation - valuest copy_values = values; + valuest copy_values=values; assign_rec(copy_values, lhs, rhs, ns); if(!values.is_constant(rhs) || values.is_constant(lhs)) - assign_rec(values, rhs, lhs, ns); - change = values.meet(copy_values); + assign_rec(values, rhs, lhs, ns); + change=values.meet(copy_values); } +#endif #ifdef DEBUG std::cout << "two_way_propagate_rec: " << change << '\n'; #endif - return change; -} - -/*******************************************************************\ -Function: constant_propagator_domaint::assign - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void constant_propagator_domaint::assign( - valuest &dest, - const symbol_exprt &lhs, - exprt rhs, - const namespacet &ns) const -{ - values.replace_const(rhs); - rhs = simplify_expr(rhs, ns); - dest.set_to(lhs, rhs); + return change; } /*******************************************************************\ -Function: constant_propagator_domaint::is_array_constant +Function: constant_propagator_domaint::simplify - Inputs: + Inputs: The condition to simplify and its namespace. - Outputs: + Outputs: The simplified condition. - Purpose: + Purpose: Simplify the condition given context-sensitive knowledge + from the abstract state. \*******************************************************************/ -bool constant_propagator_domaint::valuest::is_array_constant(const exprt &expr) const +bool constant_propagator_domaint::ai_simplify( + exprt &condition, + const namespacet &ns, + const bool lhs) const { - exprt new_expr = concatenate_array_id(expr.op0(), - expr.op1(), expr.type()); + if(lhs) + { + // For now do not simplify the left hand sides of assignments + return true; + } + else + { + bool b; - if (replace_const.expr_map.find(to_symbol_expr(new_expr).get_identifier()) == - replace_const.expr_map.end()) - return false; + b=values.replace_const.replace(condition); + b&=simplify(condition, ns); - return true; + return b; + } } /*******************************************************************\ @@ -378,12 +351,12 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const return false; if(expr.id()==ID_symbol) - if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier()) == + if(replace_const.expr_map.find(to_symbol_expr(expr).get_identifier())== replace_const.expr_map.end()) return false; - if (expr.id()==ID_index) - return is_array_constant(expr); + if(expr.id()==ID_index) + return false; if(expr.id()==ID_address_of) return is_constant_address_of(to_address_of_expr(expr).object()); @@ -434,25 +407,52 @@ Function: constant_propagator_domaint::valuest::set_to_top Outputs: - Purpose: Do not call this when iterating over replace_const.expr_map! + Purpose: Do not call when iterating over replace_const.expr_map! \*******************************************************************/ bool constant_propagator_domaint::valuest::set_to_top(const irep_idt &id) { - bool result = false; + replace_symbolt::expr_mapt::size_type n_erased= + replace_const.expr_map.erase(id); + + assert(n_erased==0 || !is_bottom); + + return n_erased>0; +} + +/*******************************************************************\ + +Function: constant_propagator_domaint::valuest::set_dirty_to_top + + Inputs: + + Outputs: + + Purpose: - replace_symbolt::expr_mapt::iterator r_it = - replace_const.expr_map.find(id); +\*******************************************************************/ - if(r_it != replace_const.expr_map.end()) +void constant_propagator_domaint::valuest::set_dirty_to_top( + const dirtyt &dirty, + const namespacet &ns) +{ + typedef replace_symbolt::expr_mapt expr_mapt; + expr_mapt &expr_map=replace_const.expr_map; + + for(expr_mapt::iterator it=expr_map.begin(); + it!=expr_map.end();) { - assert(!is_bottom); - replace_const.expr_map.erase(r_it); - result = true; - } + const irep_idt id=it->first; + + const symbolt &symbol=ns.lookup(id); - return result; + if((!symbol.is_procedure_local() || dirty(id)) && + !symbol.type.get_bool(ID_C_constant)) + it=expr_map.erase(it); + else + it++; + } } /*******************************************************************\ @@ -474,11 +474,23 @@ void constant_propagator_domaint::valuest::output( out << "const map:\n"; if(is_bottom) + { out << " bottom\n"; + assert(replace_const.expr_map.empty()); + return; + } + + assert(!is_bottom); + if(replace_const.expr_map.empty()) + { + out << "top\n"; + return; + } - for(const auto &replace_pair : replace_const.expr_map) - out << ' ' << replace_pair.first << "=" - << from_expr(ns, "", replace_pair.second) << '\n'; + for(const auto &p : replace_const.expr_map) + { + out << ' ' << p.first << "=" << from_expr(ns, "", p.second) << '\n'; + } } /*******************************************************************\ @@ -522,38 +534,62 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src) // just copy if(is_bottom) { - replace_const = src.replace_const; - is_bottom = src.is_bottom; + assert(!src.is_bottom); + replace_const=src.replace_const; // copy + is_bottom=false; return true; } - bool changed = false; + assert(!is_bottom && !src.is_bottom); + + 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(); - ) // no it++ + replace_symbolt::expr_mapt &expr_map=replace_const.expr_map; + const replace_symbolt::expr_mapt &src_expr_map=src.replace_const.expr_map; + + // handle top + if(src_expr_map.empty()) { - const replace_symbolt::expr_mapt::const_iterator - b_it=src.replace_const.expr_map.find(it->first); + // change if it was not top + changed=!expr_map.empty(); + + set_to_top(); - if(b_it==src.replace_const.expr_map.end()) + return changed; + } + + // remove those that are + // - different in src + // - do not exist in src + for(replace_symbolt::expr_mapt::iterator it=expr_map.begin(); + it!=expr_map.end();) + { + const irep_idt id=it->first; + const exprt &expr=it->second; + + replace_symbolt::expr_mapt::const_iterator s_it; + s_it=src_expr_map.find(id); + + if(s_it!=src_expr_map.end()) { - //cannot use set_to_top here - replace_const.expr_map.erase(it); - changed = true; - break; + // check value + const exprt &src_expr=s_it->second; + + if(expr!=src_expr) + { + it=expr_map.erase(it); + changed=true; + } + else + it++; } else { - const exprt previous=it->second; - replace_const.expr_map[b_it->first]=b_it->second; - if (it->second != previous) changed = true; - - it++; + it=expr_map.erase(it); + changed=true; } } + return changed; } @@ -574,16 +610,16 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src) if(src.is_bottom || is_bottom) return false; - bool changed = false; + bool changed=false; - for(const auto &src_replace_pair : src.replace_const.expr_map) + for(const auto &m : src.replace_const.expr_map) { - replace_symbolt::expr_mapt::iterator c_it= - replace_const.expr_map.find(src_replace_pair.first); + replace_symbolt::expr_mapt::iterator + c_it=replace_const.expr_map.find(m.first); if(c_it!=replace_const.expr_map.end()) { - if(c_it->second!=src_replace_pair.second) + if(c_it->second!=m.second) { set_to_bottom(); changed=true; @@ -592,7 +628,7 @@ bool constant_propagator_domaint::valuest::meet(const valuest &src) } else { - set_to(src_replace_pair.first, src_replace_pair.second); + set_to(m.first, m.second); changed=true; } } @@ -642,34 +678,6 @@ 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: @@ -686,9 +694,9 @@ void constant_propagator_ait::replace( { Forall_goto_program_instructions(it, goto_function.body) { - state_mapt::iterator s_it = state_map.find(it); + state_mapt::iterator s_it=state_map.find(it); - if(s_it == state_map.end()) + if(s_it==state_map.end()) continue; replace_types_rec(s_it->second.values.replace_const, it->code); @@ -696,32 +704,32 @@ 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); + simplify(it->guard, ns); } else if(it->is_assign()) { - exprt &rhs = to_code_assign(it->code).rhs(); + 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) + simplify(rhs, ns); + if(rhs.id()==ID_constant) rhs.add_source_location()=it->code.op0().source_location(); } else if(it->is_function_call()) { s_it->second.values.replace_const( to_code_function_call(it->code).function()); - simplify_expr(to_code_function_call(it->code).function(), ns); - exprt::operandst &args = + simplify(to_code_function_call(it->code).function(), ns); + + exprt::operandst &args= to_code_function_call(it->code).arguments(); - for(exprt::operandst::iterator o_it = args.begin(); - o_it != args.end(); ++o_it) + for(exprt::operandst::iterator o_it=args.begin(); + o_it!=args.end(); ++o_it) { s_it->second.values.replace_const(*o_it); - *o_it = simplify_expr(*o_it, ns); + simplify(*o_it, ns); } } else if(it->is_other()) diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h index 0766b458f7d..c2118752294 100644 --- a/src/analyses/constant_propagator.h +++ b/src/analyses/constant_propagator.h @@ -9,89 +9,138 @@ Author: Peter Schrammel #ifndef CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H #define CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H -#include "ai.h" +#include +#include -#include "replace_symbol_ext.h" +#include "ai.h" +#include "dirty.h" class constant_propagator_domaint:public ai_domain_baset { public: - void transform( - locationt, - locationt, - ai_baset &, - const namespacet &) final; - void output( - std::ostream &, - const ai_baset &, - const namespacet &) const final; - void make_top() final { values.set_to_top(); } - void make_bottom() final { values.set_to_bottom(); } - void make_entry() final { values.set_to_top(); } - bool merge(const constant_propagator_domaint &, locationt, locationt); + virtual void transform( + locationt from, + locationt to, + ai_baset &ai_base, + const namespacet &ns) final override; + + virtual void output( + std::ostream &out, + const ai_baset &ai_base, + const namespacet &ns) const override; + + bool merge( + const constant_propagator_domaint &other, + locationt from, + locationt to); + + virtual bool ai_simplify( + exprt &condition, + const namespacet &ns, + const bool lhs=false) const final override; + + virtual void make_bottom() final override + { + values.set_to_bottom(); + } + + virtual void make_top() final override + { + values.set_to_top(); + } + + virtual void make_entry() final override + { + make_top(); + } + + virtual bool is_bottom() const final override + { + return values.is_bot(); + } + + virtual bool is_top() const final override + { + return values.is_top(); + } struct valuest { public: - valuest():is_bottom(true) { } + valuest():is_bottom(true) {} // maps variables to constants - replace_symbol_extt replace_const; + replace_symbolt replace_const; bool is_bottom; - void output(std::ostream &, const namespacet &) const; - bool merge(const valuest &src); bool meet(const valuest &src); + // set whole state + void set_to_bottom() { replace_const.clear(); - is_bottom = true; + is_bottom=true; } - void set_to(const irep_idt &lhs_id, const exprt &rhs_val) + void set_to_top() { - replace_const.expr_map[lhs_id] = rhs_val; - is_bottom = false; + replace_const.clear(); + is_bottom=false; } - void set_to(const symbol_exprt &lhs, const exprt &rhs_val) + bool is_bot() const { - set_to(lhs.get_identifier(), rhs_val); + return is_bottom && replace_const.empty(); } - 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); + bool is_top() const + { + return !is_bottom && replace_const.empty(); + } + + // set single identifier + + void set_to(const irep_idt &lhs, const exprt &rhs) + { + replace_const.expr_map[lhs]=rhs; + is_bottom=false; + } + + void set_to(const symbol_exprt &lhs, const exprt &rhs) + { + set_to(lhs.get_identifier(), rhs); + } bool set_to_top(const symbol_exprt &expr) { return set_to_top(expr.get_identifier()); } - void set_to_top() + bool set_to_top(const irep_idt &id); + + void set_dirty_to_top(const dirtyt &dirty, const namespacet &ns); + + 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 is_empty() const { - replace_const.clear(); - is_bottom = false; + assert(replace_const.type_map.empty()); + return replace_const.expr_map.empty(); } + void output(std::ostream &out, const namespacet &ns) const; }; valuest values; -private: - void assign( - valuest &dest, - const symbol_exprt &lhs, - exprt rhs, - const namespacet &ns) const; - +protected: void assign_rec( valuest &values, - const exprt &lhs, - const exprt &rhs, + const exprt &lhs, const exprt &rhs, const namespacet &ns); bool two_way_propagate_rec( @@ -102,9 +151,17 @@ class constant_propagator_domaint:public ai_domain_baset class constant_propagator_ait:public ait { public: + explicit constant_propagator_ait( + const goto_functionst &goto_functions, + const bool ignore_unresolved_calls=false) : + dirty(goto_functions), + ignore_unresolved_calls(ignore_unresolved_calls) + { + } + constant_propagator_ait( goto_functionst &goto_functions, - const namespacet &ns) + const namespacet &ns) : dirty(goto_functions) { operator()(goto_functions, ns); replace(goto_functions, ns); @@ -112,18 +169,18 @@ class constant_propagator_ait:public ait constant_propagator_ait( goto_functionst::goto_functiont &goto_function, - const namespacet &ns) + const namespacet &ns) : dirty(goto_function) { operator()(goto_function, ns); replace(goto_function, ns); } + dirtyt dirty; + bool ignore_unresolved_calls; + protected: friend class constant_propagator_domaint; - void replace_array_symbol( - exprt &expr); - void replace( goto_functionst::goto_functiont &, const namespacet &); @@ -135,7 +192,6 @@ class constant_propagator_ait:public ait void replace_types_rec( const replace_symbolt &replace_const, exprt &expr); - }; #endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H diff --git a/src/analyses/custom_bitvector_analysis.h b/src/analyses/custom_bitvector_analysis.h index ceb2ba691be..e141988761e 100644 --- a/src/analyses/custom_bitvector_analysis.h +++ b/src/analyses/custom_bitvector_analysis.h @@ -32,32 +32,44 @@ class custom_bitvector_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final; + const namespacet &ns) const final override; - void make_bottom() final + void make_bottom() final override { may_bits.clear(); must_bits.clear(); has_values=tvt(false); } - void make_top() final + void make_top() final override { may_bits.clear(); must_bits.clear(); has_values=tvt(true); } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_bottom() const final override + { + assert(!has_values.is_false() || (may_bits.empty() && must_bits.empty())); + return has_values.is_false(); + } + + bool is_top() const final override + { + assert(!has_values.is_true() || (may_bits.empty() && must_bits.empty())); + return has_values.is_true(); + } + bool merge( const custom_bitvector_domaint &b, locationt from, diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp index 93588e209a7..686aecf6b4d 100644 --- a/src/analyses/dependence_graph.cpp +++ b/src/analyses/dependence_graph.cpp @@ -11,6 +11,9 @@ Date: August 2013 #include +#include +#include + #include "goto_rw.h" #include "dependence_graph.h" @@ -347,6 +350,46 @@ 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(const auto &cd : control_deps) + { + json_objectt &link=graph.push_back().make_object(); + link["locationNumber"]= + json_numbert(std::to_string(cd->location_number)); + link["sourceLocation"]=json(cd->source_location); + link["type"]=json_stringt("control"); + } + + for(const auto &dd : data_deps) + { + json_objectt &link=graph.push_back().make_object(); + link["locationNumber"]= + json_numbert(std::to_string(dd->location_number)); + link["sourceLocation"]=json(dd->source_location); + json_stringt(dd->source_location.as_string()); + link["type"]=json_stringt("data"); + } + + return graph; +} + +/*******************************************************************\ + Function: dependence_grapht::add_dep Inputs: diff --git a/src/analyses/dependence_graph.h b/src/analyses/dependence_graph.h index 8b627dd36b0..e03a78df68e 100644 --- a/src/analyses/dependence_graph.h +++ b/src/analyses/dependence_graph.h @@ -86,14 +86,18 @@ class dep_graph_domaint:public ai_domain_baset goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final; + const namespacet &ns) const final override; - void make_top() final + jsont output_json( + const ai_baset &ai, + const namespacet &ns) const override; + + void make_top() final override { assert(node_id!=std::numeric_limits::max()); @@ -102,7 +106,7 @@ class dep_graph_domaint:public ai_domain_baset data_deps.clear(); } - void make_bottom() final + void make_bottom() final override { assert(node_id!=std::numeric_limits::max()); @@ -111,11 +115,31 @@ class dep_graph_domaint:public ai_domain_baset data_deps.clear(); } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_top() const final override + { + assert(node_id!=std::numeric_limits::max()); + + assert(!has_values.is_true() || + (control_deps.empty() && data_deps.empty())); + + return has_values.is_true(); + } + + bool is_bottom() const final override + { + assert(node_id!=std::numeric_limits::max()); + + assert(!has_values.is_false() || + (control_deps.empty() && data_deps.empty())); + + return has_values.is_false(); + } + void set_node_id(node_indext id) { node_id=id; diff --git a/src/analyses/escape_analysis.h b/src/analyses/escape_analysis.h index 948bed3fea8..834a9031a34 100644 --- a/src/analyses/escape_analysis.h +++ b/src/analyses/escape_analysis.h @@ -37,33 +37,45 @@ class escape_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final; + const namespacet &ns) const final override; bool merge( const escape_domaint &b, locationt from, locationt to); - void make_bottom() final + void make_bottom() final override { cleanup_map.clear(); aliases.clear(); has_values=tvt(false); } - void make_top() final + void make_top() final override { cleanup_map.clear(); aliases.clear(); has_values=tvt(true); } - void make_entry() final + bool is_bottom() const override final + { + assert(!has_values.is_false() || (cleanup_map.empty() && aliases.empty())); + return has_values.is_false(); + } + + bool is_top() const override final + { + assert(!has_values.is_true() || (cleanup_map.empty() && aliases.empty())); + return has_values.is_true(); + } + + void make_entry() override final { make_top(); } diff --git a/src/analyses/global_may_alias.h b/src/analyses/global_may_alias.h index 2f4a49b2d0a..9ed5b5ed78d 100644 --- a/src/analyses/global_may_alias.h +++ b/src/analyses/global_may_alias.h @@ -37,35 +37,47 @@ class global_may_alias_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final; + const namespacet &ns) const final override; bool merge( const global_may_alias_domaint &b, locationt from, locationt to); - void make_bottom() final + void make_bottom() final override { aliases.clear(); has_values=tvt(false); } - void make_top() final + void make_top() final override { aliases.clear(); has_values=tvt(true); } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_bottom() const final override + { + assert(!has_values.is_false() || aliases.empty()); + return has_values.is_false(); + } + + bool is_top() const final override + { + assert(!has_values.is_true() || aliases.empty()); + return has_values.is_true(); + } + typedef union_find aliasest; aliasest aliases; diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 1faf8c52364..18befbfe182 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; @@ -157,8 +155,8 @@ bool interval_domaint::merge( for(int_mapt::iterator it=int_map.begin(); it!=int_map.end(); ) // no it++ { - //search for the variable that needs to be merged - //containers have different size and variable order + // 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()) { @@ -527,3 +525,61 @@ exprt interval_domaint::make_expression(const symbol_exprt &src) const else return true_exprt(); } + +/*******************************************************************\ + +Function: interval_domaint::simplify + + Inputs: The expression to simplify. + + Outputs: A simplified version of the expression. + + Purpose: Uses the abstract state to simplify a given expression + using context-specific information. + +\*******************************************************************/ + +bool interval_domaint::ai_simplify( + exprt &condition, + const namespacet &ns, + const bool lhs) const +{ + bool unchanged=true; + + if(lhs) + { + // For now do not simplify the left hand side of assignments + return true; + } + + 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); + + if(!a.join(d)) + { + unchanged=condition.is_true(); + condition.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()) + { + unchanged=condition.is_true(); + condition.make_true(); + } + } + + return unchanged; +} diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index 7e95c65e9de..d081ea2d9a8 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -33,20 +33,25 @@ class interval_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final; + const namespacet &ns) const override; + + bool join(const interval_domaint &b); bool merge( const interval_domaint &b, locationt from, - locationt to); + locationt to) + { + return join(b); + } // no states - void make_bottom() final + void make_bottom() final override { int_map.clear(); float_map.clear(); @@ -54,18 +59,30 @@ class interval_domaint:public ai_domain_baset } // all states - void make_top() final + void make_top() final override { int_map.clear(); float_map.clear(); bottom=false; } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_bottom() const override final + { + // assert(!bottom || (int_map.empty() && float_map.empty())); + + return bottom; + } + + bool is_top() const override final + { + return !bottom && int_map.empty() && float_map.empty(); + } + exprt make_expression(const symbol_exprt &) const; void assume(const exprt &, const namespacet &); @@ -80,12 +97,12 @@ class interval_domaint:public ai_domain_baset return src.id()==ID_floatbv; } - bool is_bottom() const - { - return bottom; - } + virtual bool ai_simplify( + exprt &condition, + const namespacet &ns, + const bool lhs=false) const override final; -private: +protected: bool bottom; typedef std::map int_mapt; diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h index 2e231524cbb..3031ac8d867 100644 --- a/src/analyses/invariant_set_domain.h +++ b/src/analyses/invariant_set_domain.h @@ -41,7 +41,7 @@ class invariant_set_domaint:public ai_domain_baset void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final + const namespacet &ns) const final override { if(has_values.is_known()) out << has_values.to_string() << '\n'; @@ -53,25 +53,35 @@ class invariant_set_domaint:public ai_domain_baset locationt from_l, locationt to_l, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; - void make_top() final + void make_top() final override { invariant_set.make_true(); has_values=tvt(true); } - void make_bottom() final + void make_bottom() final override { invariant_set.make_false(); has_values=tvt(false); } - void make_entry() final + void make_entry() final override { invariant_set.make_true(); has_values=tvt(true); } + + bool is_top() const override final + { + return has_values.is_true(); + } + + bool is_bottom() const override final + { + return has_values.is_false(); + } }; #endif // CPROVER_ANALYSES_INVARIANT_SET_DOMAIN_H diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index 905cd6b91ac..9567b343517 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -29,10 +29,7 @@ class is_threaded_domaint:public ai_domain_baset locationt from, locationt to) { - // assert(src.reachable); - - if(!src.reachable) - return false; + assert(src.reachable); bool old_reachable=reachable; bool old_is_threaded=is_threaded; @@ -48,34 +45,43 @@ class is_threaded_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final + const namespacet &ns) final override { - // assert(reachable); - - if(!reachable) - return; + assert(reachable); if(from->is_start_thread()) is_threaded=true; } - void make_bottom() final + void make_bottom() final override { reachable=false; is_threaded=false; } - void make_top() final + void make_top() final override { reachable=true; is_threaded=true; } - void make_entry() final + void make_entry() final override { reachable=true; is_threaded=false; } + + bool is_bottom() const override final + { + assert(reachable || !is_threaded); + + return !reachable; + } + + bool is_top() const override final + { + return reachable && is_threaded; + } }; /*******************************************************************\ diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index a48a271a9a6..a08963bd379 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -112,17 +112,17 @@ class rd_range_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, - const namespacet &ns) const final + const namespacet &ns) const final override { output(out); } - void make_top() final + void make_top() final override { values.clear(); if(bv_container) @@ -130,7 +130,7 @@ class rd_range_domaint:public ai_domain_baset has_values=tvt(true); } - void make_bottom() final + void make_bottom() final override { values.clear(); if(bv_container) @@ -138,11 +138,23 @@ class rd_range_domaint:public ai_domain_baset has_values=tvt(false); } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_top() const override final + { + assert(!has_values.is_true() || values.empty()); + return has_values.is_true(); + } + + bool is_bottom() const override final + { + assert(!has_values.is_false() || values.empty()); + return has_values.is_false(); + } + // returns true iff there is s.th. new bool merge( const rd_range_domaint &other, @@ -248,9 +260,9 @@ class reaching_definitions_analysist: virtual ~reaching_definitions_analysist(); virtual void initialize( - const goto_functionst &goto_functions); + const goto_functionst &goto_functions) override; - virtual statet &get_state(goto_programt::const_targett l) + virtual statet &get_state(goto_programt::const_targett l) override { statet &s=concurrency_aware_ait::get_state(l); diff --git a/src/analyses/replace_symbol_ext.cpp b/src/analyses/replace_symbol_ext.cpp deleted file mode 100644 index 568ea45e090..00000000000 --- a/src/analyses/replace_symbol_ext.cpp +++ /dev/null @@ -1,84 +0,0 @@ -/*******************************************************************\ - -Module: Modified expression replacement for constant propagator - -Author: Peter Schrammel - -\*******************************************************************/ - -#include -#include - -#include "replace_symbol_ext.h" - -/*******************************************************************\ - -Function: replace_symbol_extt::replace - - Inputs: - - Outputs: - - Purpose: does not replace object in address_of expressions - -\*******************************************************************/ - -bool replace_symbol_extt::replace(exprt &dest) const -{ - bool result=true; - - // first look at type - - if(have_to_replace(dest.type())) - if(!replace_symbolt::replace(dest.type())) - result=false; - - // now do expression itself - - if(!have_to_replace(dest)) - return result; - - // do not replace object in address_of expressions - if(dest.id()==ID_address_of) - { - const exprt &object = to_address_of_expr(dest).object(); - if(object.id()==ID_symbol) - { - expr_mapt::const_iterator it= - expr_map.find(object.get(ID_identifier)); - - if(it!=expr_map.end()) - return false; - } - } - else if(dest.id()==ID_symbol) - { - expr_mapt::const_iterator it= - expr_map.find(dest.get(ID_identifier)); - - if(it!=expr_map.end()) - { - dest=it->second; - return false; - } - } - - Forall_operands(it, dest) - if(!replace(*it)) - result=false; - - const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type); - - if(c_sizeof_type.is_not_nil() && - !replace_symbolt::replace( - static_cast(dest.add(ID_C_c_sizeof_type)))) - result=false; - - const irept &va_arg_type=dest.find(ID_C_va_arg_type); - - if(va_arg_type.is_not_nil() && - !replace_symbolt::replace(static_cast(dest.add(ID_C_va_arg_type)))) - result=false; - - return result; -} diff --git a/src/analyses/replace_symbol_ext.h b/src/analyses/replace_symbol_ext.h deleted file mode 100644 index 5a2152db17f..00000000000 --- a/src/analyses/replace_symbol_ext.h +++ /dev/null @@ -1,20 +0,0 @@ -/*******************************************************************\ - -Module: Modified expression replacement for constant propagator - -Author: Peter Schrammel - -\*******************************************************************/ - -#ifndef CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H -#define CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H - -#include - -class replace_symbol_extt:public replace_symbolt -{ -public: - virtual bool replace(exprt &dest) const; -}; - -#endif // CPROVER_ANALYSES_REPLACE_SYMBOL_EXT_H diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h index 6ca27f341b0..7323f08af80 100644 --- a/src/analyses/uninitialized_domain.h +++ b/src/analyses/uninitialized_domain.h @@ -30,30 +30,42 @@ class uninitialized_domaint:public ai_domain_baset locationt from, locationt to, ai_baset &ai, - const namespacet &ns) final; + const namespacet &ns) final override; void output( std::ostream &out, const ai_baset &ai, const namespacet &ns) const final; - void make_top() final + void make_top() final override { uninitialized.clear(); has_values=tvt(true); } - void make_bottom() final + void make_bottom() final override { uninitialized.clear(); has_values=tvt(false); } - void make_entry() final + void make_entry() final override { make_top(); } + bool is_top() const override final + { + assert(!has_values.is_true() || uninitialized.empty()); + return has_values.is_true(); + } + + bool is_bottom() const override final + { + assert(!has_values.is_false() || uninitialized.empty()); + return has_values.is_false(); + } + // returns true iff there is s.th. new bool merge( const uninitialized_domaint &other, diff --git a/src/goto-analyzer/Makefile b/src/goto-analyzer/Makefile index 9eb45165f9c..f582145e85e 100644 --- a/src/goto-analyzer/Makefile +++ b/src/goto-analyzer/Makefile @@ -4,6 +4,8 @@ SRC = goto_analyzer_main.cpp \ taint_analysis.cpp \ taint_parser.cpp \ unreachable_instructions.cpp \ + static_simplifier.cpp \ + static_show_domain.cpp \ # Empty last line 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 5f889ff99d7..641f58f6a58 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -1,6 +1,6 @@ /*******************************************************************\ -Module: Goto-Analyser Command Line Option Processing +Module: Goto-Analyzer Command Line Option Processing Author: Daniel Kroening, kroening@kroening.com @@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -32,6 +33,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include +#include #include #include @@ -48,6 +51,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" /*******************************************************************\ @@ -137,7 +142,7 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) exit(1); } - #if 0 +#if 0 if(cmdline.isset("c89")) config.ansi_c.set_c89(); @@ -155,9 +160,9 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) if(cmdline.isset("cpp11")) config.cpp.set_cpp11(); - #endif +#endif - #if 0 +#if 0 // check assertions if(cmdline.isset("no-assertions")) options.set_option("assertions", false); @@ -173,7 +178,109 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options) // magic error label if(cmdline.isset("error-label")) options.set_option("error-label", cmdline.get_values("error-label")); - #endif +#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 + options.set_option("flow-sensitive", true); + + // 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); + } + + if(cmdline.isset("ignore-unresolved-calls")) + options.set_option("ignore-unresolved-calls", true); } /*******************************************************************\ @@ -190,177 +297,240 @@ Function: goto_analyzer_parse_optionst::doit int goto_analyzer_parse_optionst::doit() { - if(cmdline.isset("version")) + try { - std::cout << CBMC_VERSION << std::endl; - return 0; - } + if(cmdline.isset("version")) + { + std::cout << CBMC_VERSION << std::endl; + return 0; + } - // - // command line options - // + // + // command line options + // + optionst options; + get_command_line_options(options); + eval_verbosity(); - optionst options; - get_command_line_options(options); - eval_verbosity(); + // + // Print a banner + // + status() << "GOTO-ANALYZER version " CBMC_VERSION " " + << sizeof(void *)*8 << "-bit " + << config.this_architecture() << " " + << config.this_operating_system() << eom; - // - // Print a banner - // - status() << "GOTO-ANALYSER version " CBMC_VERSION " " - << sizeof(void *)*8 << "-bit " - << config.this_architecture() << " " - << config.this_operating_system() << eom; + register_languages(); - register_languages(); + goto_model.set_message_handler(get_message_handler()); - goto_model.set_message_handler(get_message_handler()); + if(goto_model(cmdline)) + return 6; - if(goto_model(cmdline)) - return 6; + goto_functionst::function_mapt::const_iterator f_it= + goto_model.goto_functions.function_map.find( + goto_functionst::entry_point()); - if(process_goto_program(options)) - return 6; + if(f_it==goto_model.goto_functions.function_map.end()) + { + error() << "Entry point not found" << eom; + return 6; + } - if(cmdline.isset("taint")) - { - std::string taint_file=cmdline.get_value("taint"); + if(process_goto_program(options)) + return 6; - if(cmdline.isset("show-taint")) + status() << "Starting analysis" << eom; + + if(cmdline.isset("taint")) { - taint_analysis(goto_model, taint_file, get_message_handler(), true, ""); - return 0; + std::string taint_file=cmdline.get_value("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; + } } - else + + if(cmdline.isset("unreachable-instructions")) { - 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; - } - } + const std::string json_file=cmdline.get_value("json"); - if(cmdline.isset("unreachable-instructions")) - { - 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); + } - if(json_file.empty()) - unreachable_instructions(goto_model, false, std::cout); - else if(json_file=="-") - unreachable_instructions(goto_model, true, std::cout); - else + return 0; + } + + if(cmdline.isset("unreachable-functions")) { - std::ofstream ofs(json_file); - if(!ofs) + const std::string json_file=cmdline.get_value("json"); + + if(json_file.empty()) + unreachable_functions(goto_model, false, std::cout); + else if(json_file=="-") + unreachable_functions(goto_model, true, std::cout); + else { - error() << "Failed to open json output `" - << json_file << "'" << eom; - return 6; + std::ofstream ofs(json_file); + if(!ofs) + { + error() << "Failed to open json output `" + << json_file << "'" << eom; + return 6; + } + + unreachable_functions(goto_model, true, ofs); } - unreachable_instructions(goto_model, true, ofs); + return 0; } - return 0; - } + if(cmdline.isset("reachable-functions")) + { + const std::string json_file=cmdline.get_value("json"); - if(cmdline.isset("unreachable-functions")) - { - const std::string json_file=cmdline.get_value("json"); + if(json_file.empty()) + reachable_functions(goto_model, false, std::cout); + else if(json_file=="-") + reachable_functions(goto_model, true, std::cout); + else + { + std::ofstream ofs(json_file); + if(!ofs) + { + error() << "Failed to open json output `" + << json_file << "'" << eom; + return 6; + } + + reachable_functions(goto_model, true, ofs); + } - if(json_file.empty()) - unreachable_functions(goto_model, false, std::cout); - else if(json_file=="-") - unreachable_functions(goto_model, true, std::cout); - else + return 0; + } + + if(cmdline.isset("show-local-may-alias")) { - std::ofstream ofs(json_file); - if(!ofs) + namespacet ns(goto_model.symbol_table); + + forall_goto_functions(it, goto_model.goto_functions) { - error() << "Failed to open json output `" - << json_file << "'" << eom; - return 6; + 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'; } - unreachable_functions(goto_model, true, ofs); + return 0; } - return 0; - } + label_properties(goto_model); - if(cmdline.isset("reachable-functions")) - { - const std::string json_file=cmdline.get_value("json"); + if(cmdline.isset("show-properties")) + { + show_properties(goto_model, get_ui()); + return 0; + } + + if(set_properties()) + return 7; - if(json_file.empty()) - reachable_functions(goto_model, false, std::cout); - else if(json_file=="-") - reachable_functions(goto_model, true, std::cout); + // 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) + if(options.get_bool_option("simplify")) + out=new std::ofstream(outfile, std::ios::binary); + else + out=new std::ofstream(outfile); + + if(!*out) { - error() << "Failed to open json output `" - << json_file << "'" << eom; + error() << "Failed to open output file `" << outfile << "'" << eom; return 6; } - - reachable_functions(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; - } - - label_properties(goto_model); + if(out!=&std::cout) + delete out; - if(cmdline.isset("show-properties")) + return result?10:0; + } + catch(const char *e) { - show_properties(goto_model, get_ui()); - return 0; + error() << e << eom; + return 6; } - - if(set_properties()) - return 7; - - if(cmdline.isset("show-intervals")) + catch(const std::string e) { - show_intervals(goto_model, std::cout); - return 0; + error() << e << eom; + return 6; } - - if(cmdline.isset("non-null") || - cmdline.isset("intervals")) + catch(int x) { - 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; + return x; + } + catch(std::bad_alloc) + { + error() << "Out of memory" << eom; + return 6; } - - error() << "no analysis option given -- consider reading --help" - << eom; - return 6; } /*******************************************************************\ @@ -382,19 +552,16 @@ bool goto_analyzer_parse_optionst::set_properties() if(cmdline.isset("property")) ::set_properties(goto_model, 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; @@ -475,24 +642,20 @@ bool goto_analyzer_parse_optionst::process_goto_program( 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; @@ -518,7 +681,7 @@ void goto_analyzer_parse_optionst::help() { std::cout << "\n" - "* * GOTO-ANALYSER " CBMC_VERSION " - Copyright (C) 2016 "; + "* * GOTO-ANALYZER " CBMC_VERSION " - Copyright (C) 2017 "; std::cout << "(" << (sizeof(void *)*8) << "-bit version)"; @@ -533,8 +696,31 @@ 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 display the abstract domains\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --verify use the abstract domains to check assertions\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --simplify file_name use the abstract domains to simplify the program\n" + "\n" + "Abstract interpreter options:\n" + " --flow-sensitive use flow-sensitive abstract interpreter\n" + " --concurrent use concurrency-aware abstract interpreter\n" "\n" + "Domain options:\n" + " --constants constant domain\n" + " --intervals interval domain\n" + " --non-null non-null domain\n" + " --dependence-graph data and control dependencies between instructions\n" // NOLINT(*) + "\n" + "Output options:\n" + " --text file_name output results in plain text to given file\n" + // NOLINTNEXTLINE(whitespace/line_length) + " --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" // NOLINTNEXTLINE(whitespace/line_length) " --taint file_name perform taint analysis using rules in given file\n" " --unreachable-instructions list dead code\n" @@ -542,13 +728,6 @@ void goto_analyzer_parse_optionst::help() " --unreachable-functions list functions unreachable from the entry point\n" // NOLINTNEXTLINE(whitespace/line_length) " --reachable-functions list functions reachable from the entry point\n" - " --intervals interval analysis\n" - " --non-null non-null analysis\n" - "\n" - "Analysis options:\n" - // NOLINTNEXTLINE(whitespace/line_length) - " --json file_name output results in JSON format to given file\n" - " --xml file_name output results in XML format to given file\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 a72dd9ca76a..36fca9b9d8c 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.h +++ b/src/goto-analyzer/goto_analyzer_parse_options.h @@ -38,11 +38,17 @@ class optionst; "(gcc)(arch):" \ "(taint):(show-taint)" \ "(show-local-may-alias)" \ - "(json):(xml):" \ + "(json):(xml):(text):(dot):" \ "(unreachable-instructions)(unreachable-functions)" \ "(reachable-functions)" \ "(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)" \ + "(ignore-unresolved-calls)" 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 1168cff1a73..9d23ee81407 100644 --- a/src/goto-analyzer/static_analyzer.cpp +++ b/src/goto-analyzer/static_analyzer.cpp @@ -8,25 +8,29 @@ Author: Daniel Kroening, kroening@kroening.com #include -#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 +40,41 @@ 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() << "Computing abstract states" << eom; + domain(goto_functions, ns); + + status() << "Checking assertions" << eom; - 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,39 +83,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; @@ -127,51 +113,59 @@ void static_analyzert::plain_text_report() if(!i_it->is_assert()) continue; - tvt r=eval(i_it); + exprt e(i_it->guard); + domain[i_it].ai_simplify(e, ns); result() << '[' << i_it->source_location.get_property_id() << ']' << ' '; result() << i_it->source_location; + 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"; - else - result() << "UNKNOWN"; - result() << eom; - if(r.is_true()) + if(e.is_true()) + { + result() << "Success"; pass++; - else if(r.is_false()) + } + else if(e.is_false()) + { + result() << "Failure (if reachable)"; fail++; + } else + { + result() << "Unknown"; unknown++; + } + + result() << eom; } 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; @@ -188,49 +182,39 @@ void static_analyzert::json_report(const std::string &file_name) if(!i_it->is_assert()) continue; - tvt r=eval(i_it); + exprt e(i_it->guard); + domain[i_it].ai_simplify(e, ns); json_objectt &j=json_result.push_back().make_object(); - if(r.is_true()) + if(e.is_true()) j["status"]=json_stringt("SUCCESS"); - else if(r.is_false()) - j["status"]=json_stringt("FAILURE"); + else if(e.is_false()) + j["status"]=json_stringt("FAILURE (if reachable)"); else j["status"]=json_stringt("UNKNOWN"); - j["file"]=json_stringt(id2string(i_it->source_location.get_file())); - j["line"]=json_numbert(id2string(i_it->source_location.get_line())); - j["description"]=json_stringt(id2string( - i_it->source_location.get_comment())); + j["sourceLocation"]=json(i_it->source_location); } } - - 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; @@ -247,33 +231,27 @@ void static_analyzert::xml_report(const std::string &file_name) if(!i_it->is_assert()) continue; - tvt r=eval(i_it); + exprt e(i_it->guard); + domain[i_it].ai_simplify(e, ns); xmlt &x=xml_result.new_element("result"); - if(r.is_true()) + if(e.is_true()) x.set_attribute("status", "SUCCESS"); - else if(r.is_false()) - x.set_attribute("status", "FAILURE"); + else if(e.is_false()) + x.set_attribute("status", "FAILURE (if reachable)"); else x.set_attribute("status", "UNKNOWN"); x.set_attribute("file", id2string(i_it->source_location.get_file())); x.set_attribute("line", id2string(i_it->source_location.get_line())); x.set_attribute( - "description", id2string(i_it->source_location.get_comment())); + "description", + id2string(i_it->source_location.get_comment())); } } - 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; } @@ -281,40 +259,59 @@ 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) + message_handlert &message_handler, + std::ostream &out) { - return static_analyzert( - goto_model, options, message_handler)(); -} - -/*******************************************************************\ + messaget m(message_handler); + m.status() << "Selecting abstract domain" << messaget::eom; -Function: show_intervals + if(options.get_bool_option("flow-sensitive")) + { + if(options.get_bool_option("constants")) + return static_analyzert> + (goto_model, options, message_handler, out)(); - Inputs: + else if(options.get_bool_option("intervals")) + return static_analyzert> + (goto_model, options, message_handler, out)(); - Outputs: + // else if(options.get_bool_option("non-null")) + // return static_analyzert > + // (goto_model, options, message_handler, out)(); + } + 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)(); +#endif + } - Purpose: + m.status() << "Task / Interpreter / Domain combination not supported" + << messaget::eom; -\*******************************************************************/ - -void show_intervals( - const goto_modelt &goto_model, - std::ostream &out) -{ - ait interval_analysis; - interval_analysis(goto_model); - interval_analysis.output(goto_model, out); + return true; } diff --git a/src/goto-analyzer/static_analyzer.h b/src/goto-analyzer/static_analyzer.h index 3d964a2964a..fc320ad734b 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 // CPROVER_GOTO_ANALYZER_STATIC_ANALYZER_H diff --git a/src/goto-analyzer/static_show_domain.cpp b/src/goto-analyzer/static_show_domain.cpp new file mode 100644 index 00000000000..b39e1a244af --- /dev/null +++ b/src/goto-analyzer/static_show_domain.cpp @@ -0,0 +1,115 @@ +/*******************************************************************\ + +Module: + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +// #define DEBUG + +#ifdef DEBUG +#include +#endif + +#include +#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=nullptr; + + namespacet ns(goto_model.symbol_table); + messaget m(message_handler); + + m.status() << "Selecting abstract domain" << messaget::eom; + + if(options.get_bool_option("flow-sensitive")) + { + if(options.get_bool_option("constants")) + { + domain= + new constant_propagator_ait( + goto_model.goto_functions, + options.get_bool_option("ignore-unresolved-calls")); + } + else if(options.get_bool_option("intervals")) + 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==nullptr) + { + m.status() << "Task / Interpreter / Domain combination not supported" + << messaget::eom; + return true; + } + + m.status() << "Computing abstract states" << messaget::eom; + (*domain)(goto_model); + + m.status() << "Outputting abstract states" << messaget::eom; + + 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..bedb1e7faed --- /dev/null +++ b/src/goto-analyzer/static_show_domain.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H +#define CPROVER_GOTO_ANALYZER_STATIC_SHOW_DOMAIN_H + +#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..b28e7501c0a --- /dev/null +++ b/src/goto-analyzer/static_simplifier.cpp @@ -0,0 +1,284 @@ +/*******************************************************************\ + +Module: + +Author: Lucas Cordeiro, lucas.cordeiro@cs.ox.ac.uk + +\*******************************************************************/ + +// #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); + bool 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() << "Computing abstract states" << 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); // Removes goto false + goto_functions.update(); + + remove_unreachable(goto_functions); // Convert 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_program + + Inputs: None. + + Outputs: None. + + Purpose: Simplifies the program using the information in the abstract + domain. + +\*******************************************************************/ + +template +void static_simplifiert::simplify_program() +{ + struct counterst + { + counterst() : + asserts(0), + assumes(0), + gotos(0), + assigns(0), + function_calls(0) {} + + unsigned asserts; + unsigned assumes; + unsigned gotos; + unsigned assigns; + unsigned function_calls; + }; + + counterst simplified; + counterst unmodified; + + Forall_goto_functions(f_it, goto_functions) + { + Forall_goto_program_instructions(i_it, f_it->second.body) + { + if(i_it->is_assert()) + { + bool unchanged=domain[i_it].ai_simplify(i_it->guard, ns); + + if(unchanged) + unmodified.asserts++; + else + simplified.asserts++; + } + else if(i_it->is_assume()) + { + bool unchanged=domain[i_it].ai_simplify(i_it->guard, ns); + + if(unchanged) + unmodified.assumes++; + else + simplified.assumes++; + } + else if(i_it->is_goto()) + { + bool unchanged=domain[i_it].ai_simplify(i_it->guard, ns); + + if(unchanged) + unmodified.gotos++; + else + simplified.gotos++; + } + 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. + + bool unchanged_lhs= + domain[i_it].ai_simplify(assign.lhs(), ns, true); + + bool unchanged_rhs= + domain[i_it].ai_simplify(assign.rhs(), ns, false); + + if(unchanged_lhs && unchanged_rhs) + unmodified.assigns++; + else + simplified.assigns++; + } + else if(i_it->is_function_call()) + { + code_function_callt &fcall=to_code_function_call(i_it->code); + + bool unchanged=domain[i_it].ai_simplify(fcall.function(), ns); + + exprt::operandst &args=fcall.arguments(); + + for(auto &o : args) + unchanged&=domain[i_it].ai_simplify(o, ns); + + if(unchanged) + unmodified.function_calls++; + else + simplified.function_calls++; + } + } + } + + // 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) +{ + messaget m(message_handler); + m.status() << "Selecting abstract domain" << messaget::eom; + + 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 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< + concurrency_aware_ait> + (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)(); +#endif + } + + 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..61bb77dad1d --- /dev/null +++ b/src/goto-analyzer/static_simplifier.h @@ -0,0 +1,25 @@ +/*******************************************************************\ + +Module: + +Author: Lucas Cordeiro, lucas.cordeiro@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_ANALYZER_STATIC_SIMPLIFIER_H +#define CPROVER_GOTO_ANALYZER_STATIC_SIMPLIFIER_H + +#include + +#include +#include + +#include + +bool static_simplifier( + goto_modelt &, + const optionst &, + message_handlert &, + std::ostream &); + +#endif diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 66421b2e1e1..a30fdd4c92a 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -507,17 +507,7 @@ int goto_instrument_parse_optionst::doit() reaching_definitions_analysist rd_analysis(ns); rd_analysis(goto_functions, ns); - forall_goto_functions(f_it, goto_functions) - { - if(f_it->second.body_available()) - { - std::cout << "////" << std::endl; - std::cout << "//// Function: " << f_it->first << std::endl; - std::cout << "////" << std::endl; - std::cout << std::endl; - rd_analysis.output(ns, f_it->second.body, std::cout); - } - } + rd_analysis.output(ns, goto_functions, std::cout); return 0; } @@ -530,18 +520,7 @@ int goto_instrument_parse_optionst::doit() dependence_grapht dependence_graph(ns); dependence_graph(goto_functions, ns); - forall_goto_functions(f_it, goto_functions) - { - if(f_it->second.body_available()) - { - std::cout << "////" << std::endl; - std::cout << "//// Function: " << f_it->first << std::endl; - std::cout << "////" << std::endl; - std::cout << std::endl; - dependence_graph.output(ns, f_it->second.body, std::cout); - } - } - + dependence_graph.output(ns, goto_functions, std::cout); dependence_graph.output_dot(std::cout); return 0; diff --git a/src/goto-programs/remove_unreachable.cpp b/src/goto-programs/remove_unreachable.cpp index 14f92e97be1..ac6df4261a8 100644 --- a/src/goto-programs/remove_unreachable.cpp +++ b/src/goto-programs/remove_unreachable.cpp @@ -55,3 +55,9 @@ void remove_unreachable(goto_programt &goto_program) it->make_skip(); } } + +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 694cd8c0af8..4fd423641f1 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 // CPROVER_GOTO_PROGRAMS_REMOVE_UNREACHABLE_H diff --git a/src/util/replace_symbol.cpp b/src/util/replace_symbol.cpp index 4dce48d8b93..c81a80fe7cc 100644 --- a/src/util/replace_symbol.cpp +++ b/src/util/replace_symbol.cpp @@ -74,9 +74,11 @@ Function: replace_symbolt::replace \*******************************************************************/ -bool replace_symbolt::replace(exprt &dest) const +bool replace_symbolt::replace( + exprt &dest, + const bool replace_with_const) const { - bool result=true; + bool result=true; // unchanged // first look at type @@ -89,33 +91,75 @@ bool replace_symbolt::replace(exprt &dest) const if(!have_to_replace(dest)) return result; - if(dest.id()==ID_symbol) + if(dest.id()==ID_member) + { + member_exprt &me=to_member_expr(dest); + + if(!replace(me.struct_op(), replace_with_const)) + result=false; + } + else if(dest.id()==ID_index) + { + index_exprt &ie=to_index_expr(dest); + + if(!replace(ie.array(), replace_with_const)) + result=false; + + if(!replace(ie.index())) + result=false; + } + else if(dest.id()==ID_address_of) + { + address_of_exprt &aoe=to_address_of_expr(dest); + + if(!replace(aoe.object(), false)) + result=false; + } + else if(dest.id()==ID_symbol) { + const symbol_exprt &s=to_symbol_expr(dest); + expr_mapt::const_iterator it= - expr_map.find(dest.get(ID_identifier)); + expr_map.find(s.get_identifier()); if(it!=expr_map.end()) { - dest=it->second; + const exprt &e=it->second; + + if(!replace_with_const && e.is_constant()) + return true; + + dest=e; + return false; } } - - Forall_operands(it, dest) - if(!replace(*it)) - result=false; + else + { + Forall_operands(it, dest) + if(!replace(*it)) + result=false; + } const irept &c_sizeof_type=dest.find(ID_C_c_sizeof_type); - if(c_sizeof_type.is_not_nil() && - !replace(static_cast(dest.add(ID_C_c_sizeof_type)))) - result=false; + if(c_sizeof_type.is_not_nil()) + { + typet &type=static_cast(dest.add(ID_C_c_sizeof_type)); + + if(!replace(type)) + result=false; + } const irept &va_arg_type=dest.find(ID_C_va_arg_type); - if(va_arg_type.is_not_nil() && - !replace(static_cast(dest.add(ID_C_va_arg_type)))) - result=false; + if(va_arg_type.is_not_nil()) + { + typet &type=static_cast(dest.add(ID_C_va_arg_type)); + + if(!replace(type)) + result=false; + } return result; } diff --git a/src/util/replace_symbol.h b/src/util/replace_symbol.h index f26c8eb067a..8a1e9b8e22e 100644 --- a/src/util/replace_symbol.h +++ b/src/util/replace_symbol.h @@ -37,7 +37,10 @@ class replace_symbolt type_map.insert(std::pair(identifier, type)); } - virtual bool replace(exprt &dest) const; + virtual bool replace( + exprt &dest, + const bool replace_with_const=true) const; + virtual bool replace(typet &dest) const; void operator()(exprt &dest) const @@ -56,6 +59,11 @@ class replace_symbolt type_map.clear(); } + bool empty() const + { + return expr_map.empty() && type_map.empty(); + } + replace_symbolt(); virtual ~replace_symbolt();