diff --git a/regression/goto-analyzer/ternary-operator/main.c b/regression/goto-analyzer/ternary-operator/main.c new file mode 100644 index 00000000000..c76542789fd --- /dev/null +++ b/regression/goto-analyzer/ternary-operator/main.c @@ -0,0 +1,19 @@ +#include + +extern int x; + +int main(void) +{ + bool b1; + bool b2; + + b1 = true; + b2 = !b1; + + bool b3 = x ? true : false; + int i = b1 ? 10 : 20; + int j = b2 ? 10 : 20; + int k = b3 ? 10 : 20; + + return 0; +} diff --git a/regression/goto-analyzer/ternary-operator/test-constants.desc b/regression/goto-analyzer/ternary-operator/test-constants.desc new file mode 100644 index 00000000000..e1066c6b418 --- /dev/null +++ b/regression/goto-analyzer/ternary-operator/test-constants.desc @@ -0,0 +1,12 @@ +CORE +main.c +--variable-sensitivity --vsd-values constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::b1 \(\) -> TRUE @ \[2\] +main::1::b2 \(\) -> FALSE @ \[3\] +main::1::b3 \(\) -> TOP @ \[5\] +main::1::i \(\) -> 10 @ \[7\] +main::1::j \(\) -> 20 @ \[9\] +main::1::k \(\) -> TOP @ \[11\] +-- diff --git a/regression/goto-analyzer/ternary-operator/test-intervals.desc b/regression/goto-analyzer/ternary-operator/test-intervals.desc new file mode 100644 index 00000000000..12fbe2f8c13 --- /dev/null +++ b/regression/goto-analyzer/ternary-operator/test-intervals.desc @@ -0,0 +1,12 @@ +CORE +main.c +--variable-sensitivity --vsd-values intervals --show +^EXIT=0$ +^SIGNAL=0$ +main::1::b1 \(\) -> \[1, 1\] @ \[2\] +main::1::b2 \(\) -> \[0, 0\] @ \[3\] +main::1::b3 \(\) -> \[0, 1\] @ \[5\] +main::1::i \(\) -> \[A, A\] @ \[7\] +main::1::j \(\) -> \[14, 14\] @ \[9\] +main::1::k \(\) -> \[A, 14\] @ \[11\] +-- diff --git a/regression/goto-analyzer/ternary-operator/test-value-sets.desc b/regression/goto-analyzer/ternary-operator/test-value-sets.desc new file mode 100644 index 00000000000..12aee4014f7 --- /dev/null +++ b/regression/goto-analyzer/ternary-operator/test-value-sets.desc @@ -0,0 +1,12 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::b1 \(\) -> value-set-begin: TRUE :value-set-end +main::1::b2 \(\) -> value-set-begin: FALSE :value-set-end +main::1::b3 \(\) -> value-set-begin: TRUE, FALSE :value-set-end +main::1::i \(\) -> value-set-begin: 10 :value-set-end +main::1::j \(\) -> value-set-begin: 20 :value-set-end +main::1::k \(\) -> value-set-begin: 10, 20 :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-addition-01/main.c b/regression/goto-analyzer/value-set-addition-01/main.c new file mode 100644 index 00000000000..cfd9dd731f0 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-01/main.c @@ -0,0 +1,6 @@ +int main(int argc, char argv[]) +{ + int p = 1; + + int q = p + 2; +} diff --git a/regression/goto-analyzer/value-set-addition-01/test.desc b/regression/goto-analyzer/value-set-addition-01/test.desc new file mode 100644 index 00000000000..ada7f6bfeb0 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-01/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 1 :value-set-end +main::1::q .* value-set-begin: 3 :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-addition-02/main.c b/regression/goto-analyzer/value-set-addition-02/main.c new file mode 100644 index 00000000000..fa292d90ee4 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-02/main.c @@ -0,0 +1,7 @@ +int main(int argc, char argv[]) +{ + int p = 2; + int q = 3; + + int t = p + q; +} diff --git a/regression/goto-analyzer/value-set-addition-02/test.desc b/regression/goto-analyzer/value-set-addition-02/test.desc new file mode 100644 index 00000000000..073cb355e34 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-02/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 2 :value-set-end +main::1::q .* value-set-begin: 3 :value-set-end +main::1::t .* value-set-begin: 5 :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-addition-03/main.c b/regression/goto-analyzer/value-set-addition-03/main.c new file mode 100644 index 00000000000..afbb59a6f0c --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-03/main.c @@ -0,0 +1,11 @@ +int unknown(); + +int main(int argc, char argv[]) +{ + int p = 2; + + if(unknown()) + p += 2; + else + p += 3; +} diff --git a/regression/goto-analyzer/value-set-addition-03/test.desc b/regression/goto-analyzer/value-set-addition-03/test.desc new file mode 100644 index 00000000000..87854babafa --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-03/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 4, 5 :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-addition-04/main.c b/regression/goto-analyzer/value-set-addition-04/main.c new file mode 100644 index 00000000000..fd056b21e9b --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-04/main.c @@ -0,0 +1,14 @@ +int unknown(); + +int main(int argc, char argv[]) +{ + int p = 2; + int q = 3; + + if(unknown()) + p += 2; + else + p += 3; + + int t = p + q; +} diff --git a/regression/goto-analyzer/value-set-addition-04/test.desc b/regression/goto-analyzer/value-set-addition-04/test.desc new file mode 100644 index 00000000000..3942e26c036 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-04/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 2 :value-set-end +main::1::q .* value-set-begin: 3 :value-set-end +main::1::p .* value-set-begin: 4, 5 :value-set-end +main::1::t .* value-set-begin: 7, 8 :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-addition-05/main.c b/regression/goto-analyzer/value-set-addition-05/main.c new file mode 100644 index 00000000000..7b0de1f0d91 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-05/main.c @@ -0,0 +1,20 @@ +int unknown(); + +int main(int argc, char argv[]) +{ + int p; + int q; + + if(unknown()) + { + p = 2; + q = 5; + } + else + { + p = 3; + q = 10; + } + + int t = p + q; +} diff --git a/regression/goto-analyzer/value-set-addition-05/test.desc b/regression/goto-analyzer/value-set-addition-05/test.desc new file mode 100644 index 00000000000..3bb38335e0e --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-05/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 2, 3 :value-set-end +main::1::q .* value-set-begin: 5, 10 :value-set-end +main::1::t .* value-set-begin: 7, 8, 12, 13 :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-addition-06/main.c b/regression/goto-analyzer/value-set-addition-06/main.c new file mode 100644 index 00000000000..e2428b6df6b --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-06/main.c @@ -0,0 +1,21 @@ +int unknown(); + +int main(int argc, char argv[]) +{ + int p; + int q; + int r = 20; + + if(unknown()) + { + p = 2; + q = 5; + } + else + { + p = 3; + q = 10; + } + + int t = p + q + r; +} diff --git a/regression/goto-analyzer/value-set-addition-06/test.desc b/regression/goto-analyzer/value-set-addition-06/test.desc new file mode 100644 index 00000000000..9a3fdbad0ff --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-06/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 2, 3 :value-set-end +main::1::q .* value-set-begin: 5, 10 :value-set-end +main::1::t .* value-set-begin: 27, 28, 32, 33 :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-addition-07/main.c b/regression/goto-analyzer/value-set-addition-07/main.c new file mode 100644 index 00000000000..eb29cffa9f0 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-07/main.c @@ -0,0 +1,23 @@ +int unknown(); + +int main(int argc, char argv[]) +{ + int p; + int q; + int r = 20; + + if(unknown()) + p = 2; + else + p = 3; + if(unknown()) + q = 5; + else + q = 10; + if(unknown()) + r = 20; + else + r = 30; + + int t = p + q + r; +} diff --git a/regression/goto-analyzer/value-set-addition-07/test.desc b/regression/goto-analyzer/value-set-addition-07/test.desc new file mode 100644 index 00000000000..0c58d85105b --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-07/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 2, 3 :value-set-end +main::1::q .* value-set-begin: 5, 10 :value-set-end +main::1::r .* value-set-begin: 20, 30 :value-set-end +main::1::t .* value-set-begin: 27, 28, 32, 33, 37, 38, 42, 43 :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-addition-08/main.c b/regression/goto-analyzer/value-set-addition-08/main.c new file mode 100644 index 00000000000..1029400202a --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-08/main.c @@ -0,0 +1,22 @@ +int unknown(); + +int main(int argc, char argv[]) +{ + int p; + int q; + int r = 20; + ; + + if(unknown()) + p = 2; + else + p = 3; + if(unknown()) + p = 4; + if(unknown()) + q = 5; + else + q = 10; + + int t = p + q + r; +} diff --git a/regression/goto-analyzer/value-set-addition-08/test.desc b/regression/goto-analyzer/value-set-addition-08/test.desc new file mode 100644 index 00000000000..e8d5452334c --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-08/test.desc @@ -0,0 +1,10 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 2, 3, 4 :value-set-end +main::1::q .* value-set-begin: 5, 10 :value-set-end +main::1::r .* value-set-begin: 20 :value-set-end +main::1::t .* value-set-begin: 27, 28, 29, 32, 33, 34 :value-set-end +-- diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-array-constant-access/main.c b/regression/goto-analyzer/value-set-array-constant-access/main.c similarity index 100% rename from regression/goto-analyzer/variable-sensitivity-interval-values-array-constant-access/main.c rename to regression/goto-analyzer/value-set-array-constant-access/main.c diff --git a/regression/goto-analyzer/value-set-array-constant-access/test.desc b/regression/goto-analyzer/value-set-array-constant-access/test.desc new file mode 100644 index 00000000000..a45804d54ba --- /dev/null +++ b/regression/goto-analyzer/value-set-array-constant-access/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element +^EXIT=0$ +^SIGNAL=0$ +main::1::second_value \(\) -> value-set-begin: 2 :value-set-end +main::1::second_value_after_write \(\) -> value-set-begin: 10 :value-set-end diff --git a/regression/goto-analyzer/value-set-convert-to-interval/main.c b/regression/goto-analyzer/value-set-convert-to-interval/main.c new file mode 100644 index 00000000000..9e4c5e55c1b --- /dev/null +++ b/regression/goto-analyzer/value-set-convert-to-interval/main.c @@ -0,0 +1,38 @@ +#include + +extern int x; + +int main(void) +{ + int a = 0; + int b = 20; + switch(x) + { + case 1: + a = 1; + b = 21; + break; + case 2: + a = 2; + b = 22; + break; + case 3: + a = 3; + b = 23; + break; + case 4: + a = 4; + b = 24; + break; + case 5: + a = 5; + break; + case 6: + a = 6; + break; + } + + int c = a + b; + + return 0; +} diff --git a/regression/goto-analyzer/value-set-convert-to-interval/test.desc b/regression/goto-analyzer/value-set-convert-to-interval/test.desc new file mode 100644 index 00000000000..45b4d120bd1 --- /dev/null +++ b/regression/goto-analyzer/value-set-convert-to-interval/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::a .* value-set-begin: 0, 1, 2, 3, 4, 5, 6 :value-set-end @ \[1, 12, 15, 18, 21, 24, 26\] +main::1::b .* value-set-begin: 20, 21, 22, 23, 24 :value-set-end @ \[3, 13, 16, 19, 22\] +main::1::c .* \[14, 1E\] @ \[30\] +-- diff --git a/regression/goto-analyzer/value-set-function-pointers-arrays/test.desc b/regression/goto-analyzer/value-set-function-pointers-arrays/test.desc index e8a483abf4c..3eca46105ab 100644 --- a/regression/goto-analyzer/value-set-function-pointers-arrays/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-arrays/test.desc @@ -3,11 +3,11 @@ main.c --variable-sensitivity --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --vsd-values set-of-constants --show --pointer-check --three-way-merge ^file main.c line 29 function main: replacing function pointer by 2 possible targets$ ^file main.c line 40 function main: replacing function pointer by 2 possible targets$ -^main::1::fun1 \(\) -> value-set-begin: ptr ->\([fg]\), ptr ->\([fg]\), :value-set-end$ -^main::1::fun_array3 \(\) -> \{\[0\] = value-set-begin: ptr ->\([fg]\), ptr ->\([fg]\), :value-set-end$ +^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end +^main::1::fun_array3 \(\) -> \{\[0\] = value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^main::1::fun1 \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end$ -^main::1::fun_array3 \(\) -> \{\[0\] = value-set-begin: .*ptr ->\(h\).* :value-set-end$ +^main::1::fun1 \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end +^main::1::fun_array3 \(\) -> \{\[0\] = value-set-begin: .*ptr ->\(h\).* :value-set-end diff --git a/regression/goto-analyzer/value-set-function-pointers-incremented/main.c b/regression/goto-analyzer/value-set-function-pointers-incremented-01/main.c similarity index 100% rename from regression/goto-analyzer/value-set-function-pointers-incremented/main.c rename to regression/goto-analyzer/value-set-function-pointers-incremented-01/main.c diff --git a/regression/goto-analyzer/value-set-function-pointers-incremented/test.desc b/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc similarity index 71% rename from regression/goto-analyzer/value-set-function-pointers-incremented/test.desc rename to regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc index 00a474a9cfb..d1ff293516a 100644 --- a/regression/goto-analyzer/value-set-function-pointers-incremented/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc @@ -2,9 +2,8 @@ CORE main.c --variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check ^file main.c line 28 function main: replacing function pointer by 2 possible targets$ -^main::1::fun_incremented_show \(\) -> TOP$ +^main::1::fun_incremented_show \(\) -> value-set-begin: TOP :value-set-end ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^main::1::fun_incremented_show \(\) -> value-set-begin: .* :value-set-end$ diff --git a/regression/goto-analyzer/value-set-function-pointers-incremented-02/main.c b/regression/goto-analyzer/value-set-function-pointers-incremented-02/main.c new file mode 100644 index 00000000000..d2ebc3f380b --- /dev/null +++ b/regression/goto-analyzer/value-set-function-pointers-incremented-02/main.c @@ -0,0 +1,34 @@ +#include + +typedef int (*fptr_t)(int); +fptr_t fun_global, fun_global_show; + +int f(int x) +{ + return x + 1; +} +int g(int x) +{ + return x; +} +int h(int x) +{ + return x - 1; +} + +int main(void) +{ + int i; + // This line is needed so that g is considered as a possibility for the TOP + // value + fptr_t dummy = g; + + // function pointer incremented should be top + fptr_t fun_incremented = f; + if(i) + ++fun_incremented; + else + fun_incremented = h; + fun_incremented(5); + fptr_t fun_incremented_show = fun_incremented; +} diff --git a/regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc b/regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc new file mode 100644 index 00000000000..1cb8f3ff001 --- /dev/null +++ b/regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check +^file main.c line 32 function main: replacing function pointer by 3 possible targets$ +^main::1::fun_incremented_show \(\) -> value-set-begin: TOP, ptr ->\(h\) :value-set-end +^EXIT=0$ +^SIGNAL=0$ +-- diff --git a/regression/goto-analyzer/value-set-function-pointers-simple/test.desc b/regression/goto-analyzer/value-set-function-pointers-simple/test.desc index b3eb0fb681c..604658c3d80 100644 --- a/regression/goto-analyzer/value-set-function-pointers-simple/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-simple/test.desc @@ -6,21 +6,18 @@ main.c ^file main.c line 33 function main: replacing function pointer by 2 possible targets$ ^file main.c line 41 function main: replacing function pointer by 2 possible targets$ ^file main.c line 49 function main: replacing function pointer by 2 possible targets$ -^main::1::fun0 \(\) -> TOP$ -^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\), :value-set-end$ -^main::1::fun2_show \(\) -> value-set-begin: (TOP, )?ptr ->\([fg]\), (TOP, )?ptr ->\([fg]\), (TOP, )?:value-set-end$ -^main::1::fun3_show \(\) -> value-set-begin: ptr ->\([fg]\), ptr ->\([fg]\), :value-set-end$ -^fun_global_show \(\) -> value-set-begin: (TOP, )?ptr ->\([fg]\), (TOP, )?ptr ->\([fg]\), (TOP, )?:value-set-end$ +^main::1::fun0 \(\) -> TOP +^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\) :value-set-end +^main::1::fun2_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end +^main::1::fun3_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end +^fun_global_show \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^main::1::fun0_show \(\) -> value-set-begin: .* :value-set-end$ -^main::1::fun1_show \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end$ -^main::1::fun2_show \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end$ -^main::1::fun3_show \(\) -> \{\[0\] = value-set-begin: .*ptr ->\(h\).* :value-set-end$ -^fun_global_show \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end$ +^main::1::fun0_show \(\) -> value-set-begin: .* :value-set-end +^main::1::fun1_show \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end +^main::1::fun2_show \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end +^main::1::fun3_show \(\) -> \{\[0\] = value-set-begin: .*ptr ->\(h\).* :value-set-end +^fun_global_show \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end -- -These TOP values in the sets shouldn't exist. -They're caused by a quirk in the implementation, see -https://github.com/diffblue/cbmc/issues/5307 which has been filed to fix this bug. diff --git a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc b/regression/goto-analyzer/value-set-function-pointers-structs/test.desc index 2b02202706c..d56acd449f3 100644 --- a/regression/goto-analyzer/value-set-function-pointers-structs/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-structs/test.desc @@ -4,13 +4,13 @@ main.c ^file main.c line 38 function main: replacing function pointer by 2 possible targets$ ^file main.c line 46 function main: replacing function pointer by 2 possible targets$ ^file main.c line 54 function main: replacing function pointer by 2 possible targets$ -^main::1::fun1 \(\) -> value-set-begin: ptr ->\([fg]\), ptr ->\([fg]\), :value-set-end$ -^main::1::s2 \(\) -> \{\.fptr=value-set-begin: ptr ->\([fg]\), ptr ->\([fg]\), :value-set-end\}$ -^main::1::fun2 \(\) -> value-set-begin: ptr ->\(g\), :value-set-end$ +^main::1::fun1 \(\) -> value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end +^main::1::s2 \(\) -> \{\.fptr=value-set-begin: ptr ->\(f\), ptr ->\(g\) :value-set-end @ \[23, 25\]} @ \[23, 25\] +^main::1::fun2 \(\) -> value-set-begin: ptr ->\(g\) :value-set-end ^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring -^main::1::fun1 \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end$ -^main::1::s2 \(\) -> \{\.fptr=value-set-begin: .*ptr ->\(h\).* :value-set-end\}$ -^main::1::fun2 \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end$ +^main::1::fun1 \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end +^main::1::s2 \(\) -> \{\.fptr=value-set-begin: .*ptr ->\(h\).* :value-set-end\} +^main::1::fun2 \(\) -> value-set-begin: .*ptr ->\(h\).* :value-set-end diff --git a/regression/goto-analyzer/value-set-simple/test_show.desc b/regression/goto-analyzer/value-set-simple/test_show.desc index 4697a0fd092..e6aa0638e84 100644 --- a/regression/goto-analyzer/value-set-simple/test_show.desc +++ b/regression/goto-analyzer/value-set-simple/test_show.desc @@ -1,9 +1,9 @@ CORE main.c --variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check -^global_int_show \(\) -> value-set-begin: [12], [12], :value-set-end$ -^main::1::local_double_show \(\) -> value-set-begin: [12]\.0, [12]\.0, :value-set-end$ -^main::1::local_double_ptr_show \(\) -> value-set-begin: ptr ->\(main::1::d[12]\), ptr ->\(main::1::d[12]\), :value-set-end$ +^global_int_show \(\) -> value-set-begin: 1, 2 :value-set-end +^main::1::local_double_show \(\) -> value-set-begin: 1\.0, 2\.0 :value-set-end +^main::1::local_double_ptr_show \(\) -> value-set-begin: ptr ->\(main::1::d1\), ptr ->\(main::1::d2\) :value-set-end ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/value-set-structs/test_show.desc b/regression/goto-analyzer/value-set-structs/test_show.desc index 259d478b77f..e6e45d576d0 100644 --- a/regression/goto-analyzer/value-set-structs/test_show.desc +++ b/regression/goto-analyzer/value-set-structs/test_show.desc @@ -2,8 +2,8 @@ CORE main.c --variable-sensitivity --vsd-values set-of-constants --vsd-structs every-field --vsd-arrays every-element --vsd-pointers value-set --show --pointer-check activate-multi-line-match -main::1::s_show \(\) -> \{\.d=value-set-begin: [12]\.0, [12]\.0, :value-set-end, \.str=\{\[0\] = value-set-begin: '[xy]', '[xy]', :value-set-end\n\[1\] = value-set-begin: '\\n', :value-set-end -main::1::u_show \(\) -> \{\.d=value-set-begin: [123]\.0, [123].0, [123]\.0, :value-set-end, \.str=\{\[0\] = value-set-begin: '[xyz]', '[xyz]', '[xyz]', :value-set-end\n\[1\] = value-set-begin: '\\n', :value-set-end +main::1::s_show \(\) -> \{\.d=value-set-begin: 1\.0, 2\.0 :value-set-end @ \[16\], \.str=\{\[0\] = value-set-begin: 'x', 'y' :value-set-end @ \[16\]\n\[1\] = value-set-begin: '\\n' :value-set-end +main::1::u_show \(\) -> \{\.d=value-set-begin: 1\.0, 2\.0, 3\.0 :value-set-end @ \[..\], \.str=\{\[0\] = value-set-begin: 'x', 'y', 'z' :value-set-end @ \[..\]\n\[1\] = value-set-begin: '\\n' :value-set-end @ \[..\]\n} @ \[..\]} @ \[..\] ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/regression/goto-analyzer/value-set-unary-minus-01/main.c b/regression/goto-analyzer/value-set-unary-minus-01/main.c new file mode 100644 index 00000000000..9f33f9fe745 --- /dev/null +++ b/regression/goto-analyzer/value-set-unary-minus-01/main.c @@ -0,0 +1,6 @@ +int main(int argc, char argv[]) +{ + int p = 1; + + int q = -p; +} diff --git a/regression/goto-analyzer/value-set-unary-minus-01/test.desc b/regression/goto-analyzer/value-set-unary-minus-01/test.desc new file mode 100644 index 00000000000..2aeb3f68be8 --- /dev/null +++ b/regression/goto-analyzer/value-set-unary-minus-01/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 1 :value-set-end +main::1::q .* value-set-begin: -1 :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-unary-minus-02/main.c b/regression/goto-analyzer/value-set-unary-minus-02/main.c new file mode 100644 index 00000000000..906bfa29e39 --- /dev/null +++ b/regression/goto-analyzer/value-set-unary-minus-02/main.c @@ -0,0 +1,20 @@ +int main(int argc, char argv[]) +{ + int unknown; + int p; + + switch(unknown) + { + case 0: + p = 0; + break; + case 1: + p = 1; + break; + default: + p = -1; + break; + } + + int q = -p; +} diff --git a/regression/goto-analyzer/value-set-unary-minus-02/test.desc b/regression/goto-analyzer/value-set-unary-minus-02/test.desc new file mode 100644 index 00000000000..4a29e9894f6 --- /dev/null +++ b/regression/goto-analyzer/value-set-unary-minus-02/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 0, 1, -1 :value-set-end +main::1::q .* value-set-begin: 0, 1, -1 :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-unary-not-01/main.c b/regression/goto-analyzer/value-set-unary-not-01/main.c new file mode 100644 index 00000000000..db3365e9aa8 --- /dev/null +++ b/regression/goto-analyzer/value-set-unary-not-01/main.c @@ -0,0 +1,6 @@ +int main(int argc, char argv[]) +{ + int p = 1; + + int q = !p; +} diff --git a/regression/goto-analyzer/value-set-unary-not-01/test.desc b/regression/goto-analyzer/value-set-unary-not-01/test.desc new file mode 100644 index 00000000000..bae2f5d14b1 --- /dev/null +++ b/regression/goto-analyzer/value-set-unary-not-01/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 1 :value-set-end +main::1::q .* value-set-begin: 0 :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-unary-not-02/main.c b/regression/goto-analyzer/value-set-unary-not-02/main.c new file mode 100644 index 00000000000..6e8b9a5c57c --- /dev/null +++ b/regression/goto-analyzer/value-set-unary-not-02/main.c @@ -0,0 +1,20 @@ +int main(int argc, char argv[]) +{ + int unknown; + int p; + + switch(unknown) + { + case 0: + p = 0; + break; + case 1: + p = 1; + break; + default: + p = -1; + break; + } + + int q = !p; +} diff --git a/regression/goto-analyzer/value-set-unary-not-02/test.desc b/regression/goto-analyzer/value-set-unary-not-02/test.desc new file mode 100644 index 00000000000..40c88c6d97e --- /dev/null +++ b/regression/goto-analyzer/value-set-unary-not-02/test.desc @@ -0,0 +1,8 @@ +CORE +main.c +--variable-sensitivity --vsd-values set-of-constants --show +^EXIT=0$ +^SIGNAL=0$ +main::1::p .* value-set-begin: 0, 1, -1 :value-set-end +main::1::q .* value-set-begin: 0, 1 :value-set-end +-- diff --git a/regression/goto-analyzer/variable-sensitivity-array-constant-access/main.c b/regression/goto-analyzer/variable-sensitivity-array-constant-access/main.c new file mode 100644 index 00000000000..41aa58a0e10 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-constant-access/main.c @@ -0,0 +1,8 @@ +int main(void) +{ + int arr[] = {1, 2, 3}; + int second_value = arr[1]; + arr[1] = 10; + int second_value_after_write = arr[1]; + return 0; +} diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-array-constant-access/test.desc b/regression/goto-analyzer/variable-sensitivity-array-constant-access/test.desc similarity index 100% rename from regression/goto-analyzer/variable-sensitivity-interval-values-array-constant-access/test.desc rename to regression/goto-analyzer/variable-sensitivity-array-constant-access/test.desc diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-array-interval-access/main.c b/regression/goto-analyzer/variable-sensitivity-array-interval-access/main.c similarity index 100% rename from regression/goto-analyzer/variable-sensitivity-interval-values-array-interval-access/main.c rename to regression/goto-analyzer/variable-sensitivity-array-interval-access/main.c diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-array-interval-access/test.desc b/regression/goto-analyzer/variable-sensitivity-array-interval-access/test.desc similarity index 100% rename from regression/goto-analyzer/variable-sensitivity-interval-values-array-interval-access/test.desc rename to regression/goto-analyzer/variable-sensitivity-array-interval-access/test.desc diff --git a/regression/goto-analyzer/variable-sensitivity-array-value-set-access-02/main.c b/regression/goto-analyzer/variable-sensitivity-array-value-set-access-02/main.c new file mode 100644 index 00000000000..4660efed1e9 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-value-set-access-02/main.c @@ -0,0 +1,16 @@ +int unknown(); + +int main(int argc, char argv[]) +{ + int array[2] = {1, 2}; + int p; + + if(unknown()) + p = 0; + else + p = 1; + if(unknown()) + array[0] = 3; + + int t = array[p]; +} diff --git a/regression/goto-analyzer/variable-sensitivity-array-value-set-access-02/test.desc b/regression/goto-analyzer/variable-sensitivity-array-value-set-access-02/test.desc new file mode 100644 index 00000000000..e96f8afd270 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-value-set-access-02/test.desc @@ -0,0 +1,7 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element +^EXIT=0$ +^SIGNAL=0$ +main::1::t \(\) -> value-set-begin: 1, 2, 3 :value-set-end +main::1::p \(\) -> value-set-begin: 0, 1 :value-set-end diff --git a/regression/goto-analyzer/variable-sensitivity-array-value-set-access/main.c b/regression/goto-analyzer/variable-sensitivity-array-value-set-access/main.c new file mode 100644 index 00000000000..12756805712 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-value-set-access/main.c @@ -0,0 +1,33 @@ +int main(void) +{ + int arr[] = {1, 2, 3}; + int ix; + if(ix) + { + ix = 0; + } + else + { + ix = 2; + } + // ix is between 0 and 2 + // so this is between 1 and 3 + int arr_at_ix = arr[ix]; + int write_ix; + if(write_ix) + { + write_ix = 0; + } + else + { + write_ix = 1; + } + arr[write_ix] = 4; + int arr_0_after_write = arr[0]; + int arr_1_after_write = arr[1]; + // We can't write to arr[2] + // because write_ix is between 0 and 1 + // so this should be unchanged + int arr_2_after_write = arr[2]; + return 0; +} diff --git a/regression/goto-analyzer/variable-sensitivity-array-value-set-access/test.desc b/regression/goto-analyzer/variable-sensitivity-array-value-set-access/test.desc new file mode 100644 index 00000000000..ec83e23bc98 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-value-set-access/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_at_ix \(\) -> value-set-begin: 1, 3 :value-set-end +main::1::arr_0_after_write \(\) -> value-set-begin: 1, 4 :value-set-end +main::1::arr_1_after_write \(\) -> value-set-begin: 2, 4 :value-set-end +main::1::arr_2_after_write \(\) -> value-set-begin: 3 :value-set-end diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication/main.c b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/main.c similarity index 100% rename from regression/goto-analyzer/variable-sensitivity-interval-values-multiplication/main.c rename to regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/main.c diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/test.desc similarity index 100% rename from regression/goto-analyzer/variable-sensitivity-interval-values-multiplication/test.desc rename to regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-01/test.desc diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/main.c b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/main.c new file mode 100644 index 00000000000..335e9516008 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/main.c @@ -0,0 +1,12 @@ +extern int g_in; + +void main(void) +{ + int r = 2; + int s = 3; + int t = 4; + + int x = 3 * s; + int y = s * t; + int z = r * s * t; +} diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc new file mode 100644 index 00000000000..1067c2bedf6 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--variable-sensitivity --vsd-values intervals --show +^EXIT=0$ +^SIGNAL=0$ +main::1::r \(\) -> \[2, 2\] @ \[1\] +main::1::s \(\) -> \[3, 3\] @ \[3\] +main::1::t \(\) -> \[4, 4\] @ \[5\] +main::1::x \(\) -> \[9, 9\] @ \[7\] +main::1::y \(\) -> \[C, C\] @ \[9\] +main::1::z \(\) -> \[18, 18\] @ \[11\] diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index 299b0e470b4..0d07c2d715b 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -66,7 +66,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const // No special handling required by the abstract environment // delegate to the abstract object - if(simplified_expr.operands().size() > 0) + if(!simplified_expr.operands().empty()) { return eval_expression(simplified_expr, ns); } @@ -74,7 +74,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const { // It is important that this is top as the abstract object may not know // how to handle the expression - return abstract_object_factory(simplified_expr.type(), ns, true); + return abstract_object_factory(simplified_expr.type(), ns, true, false); } } @@ -146,7 +146,7 @@ bool abstract_environmentt::assign( // to be none of that. if(s.id() != ID_symbol) { - throw "invalid l-value"; + throw std::runtime_error("invalid l-value"); } // We can assign the AO directly to the symbol final_value = value; @@ -252,11 +252,11 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory( const typet &type, const namespacet &ns, bool top, - bool bottom) const + bool bttm) const { exprt empty_constant_expr = nil_exprt(); return abstract_object_factory( - type, top, bottom, empty_constant_expr, *this, ns); + type, top, bttm, empty_constant_expr, *this, ns); } abstract_object_pointert abstract_environmentt::abstract_object_factory( @@ -270,13 +270,19 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory( abstract_object_pointert abstract_environmentt::abstract_object_factory( const typet &type, bool top, - bool bottom, + bool bttm, const exprt &e, const abstract_environmentt &environment, const namespacet &ns) const { return object_factory->get_abstract_object( - type, top, bottom, e, environment, ns); + type, top, bttm, e, environment, ns); +} + +abstract_object_pointert abstract_environmentt::add_object_context( + const abstract_object_pointert &abstract_object) const +{ + return object_factory->wrap_with_context(abstract_object); } bool abstract_environmentt::merge(const abstract_environmentt &env) @@ -383,7 +389,7 @@ abstract_object_pointert abstract_environmentt::eval_expression( // The value of the temporary abstract object is ignored, its // purpose is just to dispatch the expression transform call to // a concrete subtype of abstract_objectt. - auto eval_obj = abstract_object_factory(e.type(), ns, true); + auto eval_obj = abstract_object_factory(e.type(), ns, true, false); auto operands = eval_operands(e, *this, ns); return eval_obj->expression_transform(e, operands, *this, ns); diff --git a/src/analyses/variable-sensitivity/abstract_environment.h b/src/analyses/variable-sensitivity/abstract_environment.h index 42b39bc3d23..974da0f93f9 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.h +++ b/src/analyses/variable-sensitivity/abstract_environment.h @@ -39,9 +39,9 @@ class abstract_environmentt abstract_environmentt() = delete; - abstract_environmentt( + explicit abstract_environmentt( variable_sensitivity_object_factory_ptrt _object_factory) - : bottom(true), object_factory(_object_factory) + : bottom(true), object_factory(std::move(_object_factory)) { } @@ -150,8 +150,8 @@ class abstract_environmentt virtual abstract_object_pointert abstract_object_factory( const typet &type, const namespacet &ns, - bool top = true, - bool bottom = false) const; + bool top, + bool bottom) const; /// For converting constants in the program /// @@ -170,6 +170,19 @@ class abstract_environmentt const exprt &e, const namespacet &ns) const; + /// Wraps an existing object in any configured context object + /// + /// \param abstract_object: The object to be wrapped + /// + /// \return The wrapped abstract object + /// + /// Look at the configuration context dependency, and constructs + /// the appropriate wrapper object around the supplied object + /// If no such configuration is enabled, the supplied object will be + /// returned unchanged + virtual abstract_object_pointert + add_object_context(const abstract_object_pointert &abstract_object) const; + /// Computes the join between "this" and "b" /// /// \param env: the other environment diff --git a/src/analyses/variable-sensitivity/abstract_object.cpp b/src/analyses/variable-sensitivity/abstract_object.cpp index 5574d9335af..b045f324f91 100644 --- a/src/analyses/variable-sensitivity/abstract_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_object.cpp @@ -129,7 +129,7 @@ abstract_object_pointert abstract_objectt::expression_transform( if(const_op.is_nil()) { - return environment.abstract_object_factory(copy.type(), ns, true); + return environment.abstract_object_factory(copy.type(), ns, true, false); } } @@ -144,7 +144,7 @@ abstract_object_pointert abstract_objectt::write( const abstract_object_pointert &value, bool merging_write) const { - return environment.abstract_object_factory(type(), ns, true); + return environment.abstract_object_factory(type(), ns, true, false); } bool abstract_objectt::is_top() const diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.cpp b/src/analyses/variable-sensitivity/constant_abstract_value.cpp index 0a6ced0c39b..7c409e73e1d 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/constant_abstract_value.cpp @@ -33,18 +33,21 @@ index_range_ptrt make_constant_index_range(const exprt &val) return std::make_shared(val); } -constant_abstract_valuet::constant_abstract_valuet(typet t) +constant_abstract_valuet::constant_abstract_valuet(const typet &t) : abstract_value_objectt(t), value() { } -constant_abstract_valuet::constant_abstract_valuet(typet t, bool tp, bool bttm) +constant_abstract_valuet::constant_abstract_valuet( + const typet &t, + bool tp, + bool bttm) : abstract_value_objectt(t, tp, bttm), value() { } constant_abstract_valuet::constant_abstract_valuet( - const exprt e, + const exprt &e, const abstract_environmentt &environment, const namespacet &ns) : abstract_value_objectt(e.type(), false, false), value(e) @@ -159,7 +162,7 @@ constant_abstract_valuet::try_transform_expr_with_all_rounding_modes( auto current = possible_result->to_constant(); if(current.is_nil() || current != first) { - return environment.abstract_object_factory(expr.type(), ns); + return environment.abstract_object_factory(expr.type(), ns, true, false); } } return possible_results.front(); @@ -209,7 +212,7 @@ constant_abstract_valuet::merge(abstract_object_pointert other) const } abstract_object_pointert constant_abstract_valuet::merge_constant_constant( - constant_abstract_value_pointert other) const + const constant_abstract_value_pointert &other) const { if(is_bottom()) { diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.h b/src/analyses/variable-sensitivity/constant_abstract_value.h index dd58d0b4d66..24dc6b53455 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.h +++ b/src/analyses/variable-sensitivity/constant_abstract_value.h @@ -24,16 +24,14 @@ class constant_abstract_valuet : public abstract_value_objectt constant_abstract_value_pointert; public: - explicit constant_abstract_valuet(typet t); - constant_abstract_valuet(typet t, bool tp, bool bttm); + explicit constant_abstract_valuet(const typet &t); + constant_abstract_valuet(const typet &t, bool tp, bool bttm); constant_abstract_valuet( - const exprt e, + const exprt &e, const abstract_environmentt &environment, const namespacet &ns); - virtual ~constant_abstract_valuet() - { - } + ~constant_abstract_valuet() override = default; index_range_ptrt index_range(const namespacet &ns) const override; @@ -107,7 +105,7 @@ class constant_abstract_valuet : public abstract_value_objectt /// unless the merge is the same as this abstract object, in which /// case it returns this. abstract_object_pointert - merge_constant_constant(constant_abstract_value_pointert other) const; + merge_constant_constant(const constant_abstract_value_pointert &other) const; exprt value; }; diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp index 5dc618f8264..4b75017b6fb 100644 --- a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp @@ -168,7 +168,7 @@ abstract_object_pointert full_array_abstract_objectt::read_component( const namespacet &ns) const { if(is_top()) - return environment.abstract_object_factory(expr.type(), ns, true); + return environment.abstract_object_factory(expr.type(), ns, true, false); auto read_element_fn = [this, &environment, &ns](const index_exprt &index_expr) { diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp index 867730ec32b..51d3535e71f 100644 --- a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp @@ -83,7 +83,7 @@ abstract_object_pointert full_struct_abstract_objectt::read_component( if(is_top()) { - return environment.abstract_object_factory(expr.type(), ns, true); + return environment.abstract_object_factory(expr.type(), ns, true, false); } else { @@ -100,7 +100,8 @@ abstract_object_pointert full_struct_abstract_objectt::read_component( } else { - return environment.abstract_object_factory(member_expr.type(), ns, true); + return environment.abstract_object_factory( + member_expr.type(), ns, true, false); } } } diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index bdd01cf4910..5a9fa38dc96 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -54,7 +54,7 @@ class interval_index_ranget : public index_ranget const namespacet &ns; }; -index_range_ptrt make_interval_index_range( +static index_range_ptrt make_interval_index_range( const constant_interval_exprt &interval, const namespacet &n) { @@ -218,19 +218,34 @@ static inline constant_interval_exprt interval_from_relation(const exprt &e) the_constant_part_of_the_relation, the_constant_part_of_the_relation); } -interval_abstract_valuet::interval_abstract_valuet(typet t) +interval_abstract_valuet::interval_abstract_valuet(const typet &t) : abstract_value_objectt(t), interval(t) { } -interval_abstract_valuet::interval_abstract_valuet(typet t, bool tp, bool bttm) +interval_abstract_valuet::interval_abstract_valuet( + const typet &t, + bool tp, + bool bttm) : abstract_value_objectt(t, tp, bttm), interval(t) { } interval_abstract_valuet::interval_abstract_valuet( - const constant_interval_exprt e) - : interval_abstract_valuet(e, 0) + const constant_interval_exprt &e) + : abstract_value_objectt(e.type(), e.is_top(), e.is_bottom()), interval(e) +{ +} + +interval_abstract_valuet::interval_abstract_valuet( + const exprt &e, + const abstract_environmentt &environment, + const namespacet &ns) + : interval_abstract_valuet( + represents_interval(e) + ? make_interval_expr(e) + : (e.operands().size() == 2 ? interval_from_relation(e) + : constant_interval_exprt(e.type()))) { } @@ -265,7 +280,6 @@ abstract_object_pointert interval_abstract_valuet::expression_transform( PRECONDITION(operands.size() == num_operands); std::vector> interval_operands; - interval_operands.reserve(num_operands); for(const auto &op : operands) { @@ -281,7 +295,7 @@ abstract_object_pointert interval_abstract_valuet::expression_transform( if(op_as_constant.is_nil()) { auto top_object = - environment.abstract_object_factory(expr.type(), ns, true); + environment.abstract_object_factory(expr.type(), ns, true, false); auto top_context_object = std::dynamic_pointer_cast( top_object); @@ -316,111 +330,89 @@ abstract_object_pointert interval_abstract_valuet::expression_transform( interval_operands.push_back(iav); } - const typet &type = expr.type(); - if(num_operands == 0) - return environment.abstract_object_factory(type, ns, true); + return environment.abstract_object_factory(expr.type(), ns, true, false); - if(expr.id() == ID_plus) - { - constant_exprt zero = constant_interval_exprt::zero(type); - constant_interval_exprt interval(zero); - INVARIANT(interval.is_zero(), "Starting interval must be zero"); + if(expr.id() == ID_if) + return evaluate_conditional(expr, interval_operands, environment, ns); - for(const auto &iav : interval_operands) - { - const constant_interval_exprt &interval_next = iav->interval; - interval = interval.plus(interval_next); - } + if(num_operands == 1) + return evaluate_unary_expr(expr, interval_operands, environment, ns); - INVARIANT( - interval.type() == type, - "Type of result interval should match expression type"); + constant_interval_exprt result = interval_operands[0]->interval; - return environment.abstract_object_factory(type, interval, ns); - } - else if(num_operands == 1) + for(size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex) { - const constant_interval_exprt &interval = interval_operands[0]->interval; + auto &interval_next = interval_operands[opIndex]->interval; + result = result.eval(expr.id(), interval_next); + } - if(expr.id() == ID_typecast) - { - const typecast_exprt &tce = to_typecast_expr(expr); + INVARIANT( + result.type() == expr.type(), + "Type of result interval should match expression type"); + return environment.abstract_object_factory(expr.type(), result, ns); +} - const constant_interval_exprt &new_interval = - interval.typecast(tce.type()); +abstract_object_pointert interval_abstract_valuet::evaluate_conditional( + const exprt &expr, + const std::vector &interval_operands, + const abstract_environmentt &env, + const namespacet &ns) +{ + auto const &condition_interval = interval_operands[0]->interval; + auto const &true_interval = interval_operands[1]->interval; + auto const &false_interval = interval_operands[2]->interval; - INVARIANT( - new_interval.type() == type, - "Type of result interval should match expression type"); + auto condition_result = condition_interval.is_definitely_true(); - return environment.abstract_object_factory(tce.type(), new_interval, ns); - } - else - { - const constant_interval_exprt &interval_result = interval.eval(expr.id()); - INVARIANT( - interval_result.type() == type, - "Type of result interval should match expression type"); - return environment.abstract_object_factory(type, interval_result, ns); - } + if(condition_result.is_unknown()) + { + // Value of the condition is both true and false, so + // combine the intervals of both the true and false expressions + return env.abstract_object_factory( + expr.type(), + constant_interval_exprt( + constant_interval_exprt::get_min( + true_interval.get_lower(), false_interval.get_lower()), + constant_interval_exprt::get_max( + true_interval.get_upper(), false_interval.get_upper())), + ns); } - else if(num_operands == 2) + + return condition_result.is_true() + ? env.abstract_object_factory( + true_interval.type(), true_interval, ns) + : env.abstract_object_factory( + false_interval.type(), false_interval, ns); +} + +abstract_object_pointert interval_abstract_valuet::evaluate_unary_expr( + const exprt &expr, + const std::vector &interval_operands, + const abstract_environmentt &environment, + const namespacet &ns) +{ + const constant_interval_exprt &operand_expr = interval_operands[0]->interval; + + if(expr.id() == ID_typecast) { - const constant_interval_exprt &interval0 = interval_operands[0]->interval; - const constant_interval_exprt &interval1 = interval_operands[1]->interval; + const typecast_exprt &tce = to_typecast_expr(expr); - constant_interval_exprt interval = interval0.eval(expr.id(), interval1); + const constant_interval_exprt &new_interval = + operand_expr.typecast(tce.type()); INVARIANT( - interval.type() == type, + new_interval.type() == expr.type(), "Type of result interval should match expression type"); - return environment.abstract_object_factory(type, interval, ns); - } - else if(num_operands == 3) - { - if(expr.id() == ID_if) - { - const constant_interval_exprt &condition_interval = - interval_operands[0]->interval; - const constant_interval_exprt &true_interval = - interval_operands[1]->interval; - const constant_interval_exprt &false_interval = - interval_operands[2]->interval; - - // Check the value of the condition interval - if(condition_interval.is_definitely_false().is_unknown()) - { - // Value of the condition is both true and false, so - // combine the intervals of both the true and false expressions - return environment.abstract_object_factory( - type, - constant_interval_exprt( - constant_interval_exprt::get_min( - true_interval.get_lower(), false_interval.get_lower()), - constant_interval_exprt::get_max( - true_interval.get_upper(), false_interval.get_upper())), - ns); - } - if(condition_interval.is_definitely_false().is_true()) - { - // The condition is definitely false, so return only - // the interval from the 'false' expression - return environment.abstract_object_factory( - false_interval.type(), false_interval, ns); - } - if(condition_interval.is_definitely_true().is_true()) - { - // The condition is definitely true, so return only - // the interval from the 'true' expression - return environment.abstract_object_factory( - true_interval.type(), true_interval, ns); - } - } + return environment.abstract_object_factory(tce.type(), new_interval, ns); } - return environment.abstract_object_factory(type, ns, true); + const constant_interval_exprt &interval_result = operand_expr.eval(expr.id()); + INVARIANT( + interval_result.type() == expr.type(), + "Type of result interval should match expression type"); + return environment.abstract_object_factory(expr.type(), interval_result, ns); } void interval_abstract_valuet::output( @@ -502,13 +494,11 @@ abstract_object_pointert interval_abstract_valuet::merge_intervals( } else { - return std::make_shared( - constant_interval_exprt( - constant_interval_exprt::get_min( - interval.get_lower(), other->interval.get_lower()), - constant_interval_exprt::get_max( - interval.get_upper(), other->interval.get_upper())), - std::max(merge_count, other->merge_count) + 1); + return std::make_shared(constant_interval_exprt( + constant_interval_exprt::get_min( + interval.get_lower(), other->interval.get_lower()), + constant_interval_exprt::get_max( + interval.get_upper(), other->interval.get_upper()))); } } @@ -555,35 +545,10 @@ abstract_object_pointert interval_abstract_valuet::meet_intervals( return std::make_shared( interval.type(), false, true); return std::make_shared( - constant_interval_exprt(lower_bound, upper_bound), - std::max(merge_count, other->merge_count) + 1); + constant_interval_exprt(lower_bound, upper_bound)); } } -interval_abstract_valuet::interval_abstract_valuet( - const exprt e, - const abstract_environmentt &environment, - const namespacet &ns) - : interval_abstract_valuet( - represents_interval(e) - ? make_interval_expr(e) - : (e.operands().size() == 2 ? interval_from_relation(e) - : constant_interval_exprt(e.type()))) -{ -} - -interval_abstract_valuet::interval_abstract_valuet( - const constant_interval_exprt e, - int merge_count) - : abstract_value_objectt( - e.type(), - e.is_top() || merge_count > 10, - e.is_bottom()), - interval(e), - merge_count(merge_count) -{ -} - index_range_ptrt interval_abstract_valuet::index_range(const namespacet &ns) const { diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 8b9bcdc285a..9b1d3faf884 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -27,15 +27,13 @@ class interval_abstract_valuet : public abstract_value_objectt interval_abstract_value_pointert; public: - explicit interval_abstract_valuet(typet t); - interval_abstract_valuet(typet t, bool tp, bool bttm); + explicit interval_abstract_valuet(const typet &t); + interval_abstract_valuet(const typet &t, bool tp, bool bttm); - interval_abstract_valuet(const constant_interval_exprt e, int merge_count); - - explicit interval_abstract_valuet(const constant_interval_exprt e); + explicit interval_abstract_valuet(const constant_interval_exprt &e); interval_abstract_valuet( - const exprt e, + const exprt &e, const abstract_environmentt &environment, const namespacet &ns); @@ -85,14 +83,23 @@ class interval_abstract_valuet : public abstract_value_objectt meet(const abstract_object_pointert &other) const override; private: + static abstract_object_pointert evaluate_conditional( + const exprt &expr, + const std::vector &interval_operands, + const abstract_environmentt &environment, + const namespacet &ns); + static abstract_object_pointert evaluate_unary_expr( + const exprt &expr, + const std::vector &interval_operands, + const abstract_environmentt &environment, + const namespacet &ns); + abstract_object_pointert merge_intervals(interval_abstract_value_pointert other) const; abstract_object_pointert meet_intervals(interval_abstract_value_pointert other) const; constant_interval_exprt interval; - - int merge_count; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 061a1bc3198..d15453b2e25 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -15,11 +15,13 @@ #include #include #include +#include + +using abstract_object_sett = value_set_abstract_objectt::abstract_object_sett; class value_set_index_ranget : public index_ranget { public: - typedef value_set_abstract_objectt::abstract_object_sett abstract_object_sett; explicit value_set_index_ranget(const abstract_object_sett &vals) : values(vals), cur(), next(values.begin()) { @@ -46,12 +48,83 @@ class value_set_index_ranget : public index_ranget abstract_object_sett::const_iterator next; }; -index_range_ptrt make_value_set_index_range( - const value_set_abstract_objectt::abstract_object_sett &vals) +index_range_ptrt make_value_set_index_range(const abstract_object_sett &vals) { return std::make_shared(vals); } +/// Determine abstract-type of an abstract object \p other. +/// \param other: the abstract object to get the type of +/// \return the abstract-type of \p other +value_set_abstract_objectt::abstract_typet +get_type(const abstract_object_pointert &other); + +/// Determine abstract-type of an expression-type \p type. +/// \param type: the expression type to get the abstract-type of +/// \return the abstract-type of \p type +value_set_abstract_objectt::abstract_typet +type_to_abstract_type(const typet &type); + +exprt rewrite_expression( + const exprt &expr, + const std::vector &ops); + +std::vector +unwrap_operands(const std::vector &operands); + +abstract_object_sett +unwrap_and_extract_values(const abstract_object_sett &values); + +/// Helper for converting singleton value sets into its only value. +/// \p maybe_singleton: either a set of abstract values or a single value +/// \return an abstract value without context +abstract_object_pointert +maybe_extract_single_value(const abstract_object_pointert &maybe_singleton); + +/// Helper for converting context objects into its abstract-value children +/// \p maybe_wrapped: either an abstract value (or a set of those) or one +/// wrapped in a context +/// \return an abstract value without context (though it might be as set) +abstract_object_pointert +maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped); + +/// Recursively construct a combination \p sub_con from \p super_con and once +/// constructed call \p f. +/// \param super_con: vector of some containers storing the values +/// \param sub_con: the one combination being currently constructed +/// \param f: callable with side-effects +template +void apply_comb( + const std::vector &super_con, + std::vector &sub_con, + F f) +{ + size_t n = sub_con.size(); + if(n == super_con.size()) + f(sub_con); + else + { + for(const auto &value : super_con[n]) + { + sub_con.push_back(value); + apply_comb(super_con, sub_con, f); + sub_con.pop_back(); + } + } +} + +/// Call the function \p f on every combination of elements in \p super_con. +/// Hence the arity of \p f is `super_con.size()`. <{1,2},{1},{1,2,3}> -> +/// f(1,1,1), f(1,1,2), f(1,1,3), f(2,1,1), f(2,1,2), f(2,1,3). +/// \param super_con: vector of some containers storing the values +/// \param f: callable with side-effects +template +void for_each_comb(const std::vector &super_con, F f) +{ + std::vector sub_con; + apply_comb(super_con, sub_con, f); +} + value_set_abstract_objectt::value_set_abstract_objectt(const typet &type) : abstract_value_objectt(type), my_type(type_to_abstract_type(type)) { @@ -130,29 +203,56 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform( const abstract_environmentt &environment, const namespacet &ns) const { - std::size_t num_operands = expr.operands().size(); - PRECONDITION(operands.size() == num_operands); + PRECONDITION(operands.size() == expr.operands().size()); - std::vector collective_operands; - collective_operands.reserve(num_operands); - for(const auto &op : operands) - { - auto vsab = std::dynamic_pointer_cast( - maybe_unwrap_context(op)); - INVARIANT(vsab, "should be a value set abstract object"); - collective_operands.push_back(vsab->get_values()); - } + auto collective_operands = unwrap_operands(operands); + + if(expr.id() == ID_if) + return evaluate_conditional( + expr.type(), collective_operands, environment, ns); abstract_object_sett resulting_objects; + + auto dispatcher = *values.begin(); for_each_comb( collective_operands, - [&resulting_objects, this, &expr, &environment, &ns]( + [&resulting_objects, &dispatcher, &expr, &environment, &ns]( const std::vector &ops) { + auto rewritten_expr = rewrite_expression(expr, ops); resulting_objects.insert( - (*values.begin())->expression_transform(expr, ops, environment, ns)); + dispatcher->expression_transform(rewritten_expr, ops, environment, ns)); }); - return resolve_new_values(resulting_objects); + return resolve_new_values(resulting_objects, environment); +} + +abstract_object_pointert value_set_abstract_objectt::evaluate_conditional( + const typet &type, + const std::vector &operands, + const abstract_environmentt &env, + const namespacet &ns) const +{ + auto const condition = operands[0]; + + auto const true_result = operands[1]; + auto const false_result = operands[2]; + + auto all_true = true; + auto all_false = true; + for(auto v : condition) + { + auto expr = v->to_constant(); + all_true = all_true && expr.is_true(); + all_false = all_false && expr.is_false(); + } + auto indeterminate = !all_true && !all_false; + + abstract_object_sett resulting_objects; + if(all_true || indeterminate) + resulting_objects.insert(true_result.begin(), true_result.end()); + if(all_false || indeterminate) + resulting_objects.insert(false_result.begin(), false_result.end()); + return resolve_new_values(resulting_objects, env); } abstract_object_pointert value_set_abstract_objectt::write( @@ -169,10 +269,18 @@ abstract_object_pointert value_set_abstract_objectt::write( new_values.insert( st_value->write(environment, ns, stack, specifier, value, merging_write)); } - return resolve_new_values(new_values); + return resolve_new_values(new_values, environment); } abstract_object_pointert value_set_abstract_objectt::resolve_new_values( + const abstract_object_sett &new_values, + const abstract_environmentt &environment) const +{ + auto result = resolve_values(new_values); + return environment.add_object_context(result); +} + +abstract_object_pointert value_set_abstract_objectt::resolve_values( const abstract_object_sett &new_values) const { PRECONDITION(!new_values.empty()); @@ -180,12 +288,7 @@ abstract_object_pointert value_set_abstract_objectt::resolve_new_values( if(new_values == values) return shared_from_this(); - abstract_object_sett unwrapped_values; - for(auto const &value : new_values) - { - unwrapped_values.insert( - maybe_extract_single_value(maybe_unwrap_context(value))); - } + auto unwrapped_values = unwrap_and_extract_values(new_values); abstract_typet new_type = get_type(*unwrapped_values.begin()); if( @@ -199,7 +302,7 @@ abstract_object_pointert value_set_abstract_objectt::resolve_new_values( return (*unwrapped_values.begin()); } - const auto &result = + auto result = std::dynamic_pointer_cast(mutable_clone()); if( @@ -225,10 +328,10 @@ value_set_abstract_objectt::merge(abstract_object_pointert other) const auto union_values = values; union_values.insert( cast_other->get_values().begin(), cast_other->get_values().end()); - return resolve_new_values(union_values); + return resolve_values(union_values); } - else - return abstract_objectt::merge(other); + + return abstract_objectt::merge(other); } abstract_object_pointert value_set_abstract_objectt::to_interval( @@ -246,7 +349,7 @@ abstract_object_pointert value_set_abstract_objectt::to_interval( { const auto &value_expr = value->to_constant(); lower_expr = constant_interval_exprt::get_min(lower_expr, value_expr); - upper_expr = constant_interval_exprt::get_min(upper_expr, value_expr); + upper_expr = constant_interval_exprt::get_max(upper_expr, value_expr); } return std::make_shared( constant_interval_exprt(lower_expr, upper_expr)); @@ -264,9 +367,62 @@ bool value_set_abstract_objectt::verify() const return true; } +void value_set_abstract_objectt::set_values( + const abstract_object_sett &other_values) +{ + PRECONDITION(!other_values.empty()); + set_not_top(); + my_type = get_type(*other_values.begin()); + values = other_values; + verify(); +} + +bool by_length(const std::string &lhs, const std::string &rhs) +{ + if(lhs.size() < rhs.size()) + return true; + if(lhs.size() > rhs.size()) + return false; + return lhs < rhs; +} + +void value_set_abstract_objectt::output( + std::ostream &out, + const ai_baset &ai, + const namespacet &ns) const +{ + if(is_top()) + { + out << "TOP"; + } + else if(is_bottom()) + { + out << "BOTTOM"; + } + else + { + out << "value-set-begin: "; + + std::vector output_values; + for(const auto &value : values) + { + std::ostringstream ss; + value->output(ss, ai, ns); + output_values.emplace_back(ss.str()); + } + std::sort(output_values.begin(), output_values.end(), by_length); + + join_strings(out, output_values.begin(), output_values.end(), ", "); + + out << " :value-set-end"; + } +} + value_set_abstract_objectt::abstract_typet -value_set_abstract_objectt::get_type(const abstract_object_pointert &other) +get_type(const abstract_object_pointert &other) { + using abstract_typet = value_set_abstract_objectt::abstract_typet; + PRECONDITION( !std::dynamic_pointer_cast(other)); PRECONDITION(!std::dynamic_pointer_cast(other)); @@ -281,8 +437,66 @@ value_set_abstract_objectt::get_type(const abstract_object_pointert &other) return abstract_typet::UNSUPPORTED; } -abstract_object_pointert value_set_abstract_objectt::maybe_extract_single_value( - const abstract_object_pointert &maybe_singleton) +value_set_abstract_objectt::abstract_typet +type_to_abstract_type(const typet &type) +{ + using abstract_typet = value_set_abstract_objectt::abstract_typet; + + if(type.id() == ID_pointer) + return abstract_typet::POINTER; + + if( + type.id() == ID_signedbv || type.id() == ID_unsignedbv || + type.id() == ID_fixedbv || type.id() == ID_c_bool || type.id() == ID_bool || + type.id() == ID_integer || type.id() == ID_c_bit_field || + type.id() == ID_floatbv) + return abstract_typet::CONSTANT; + + return abstract_typet::UNSUPPORTED; +} + +exprt rewrite_expression( + const exprt &expr, + const std::vector &ops) +{ + auto operands_expr = exprt::operandst{}; + for(auto v : ops) + operands_expr.push_back(v->to_constant()); + auto rewritten_expr = exprt(expr.id(), expr.type(), std::move(operands_expr)); + return rewritten_expr; +} + +std::vector +unwrap_operands(const std::vector &operands) +{ + auto unwrapped = std::vector{}; + + for(const auto &op : operands) + { + auto vsab = std::dynamic_pointer_cast( + maybe_unwrap_context(op)); + INVARIANT(vsab, "should be a value set abstract object"); + unwrapped.push_back(vsab->get_values()); + } + + return unwrapped; +} + +abstract_object_sett +unwrap_and_extract_values(const abstract_object_sett &values) +{ + abstract_object_sett unwrapped_values; + for(auto const &value : values) + { + unwrapped_values.insert( + maybe_extract_single_value(maybe_unwrap_context(value))); + } + + return unwrapped_values; +} + +abstract_object_pointert +maybe_extract_single_value(const abstract_object_pointert &maybe_singleton) { auto const &value_as_set = std::dynamic_pointer_cast( @@ -299,36 +513,11 @@ abstract_object_pointert value_set_abstract_objectt::maybe_extract_single_value( return maybe_singleton; } -abstract_object_pointert value_set_abstract_objectt::maybe_unwrap_context( - const abstract_object_pointert &maybe_wrapped) +abstract_object_pointert +maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped) { auto const &context_value = std::dynamic_pointer_cast(maybe_wrapped); return context_value ? context_value->unwrap_context() : maybe_wrapped; } - -void value_set_abstract_objectt::output( - std::ostream &out, - const ai_baset &ai, - const namespacet &ns) const -{ - if(is_top()) - { - out << "TOP"; - } - else if(is_bottom()) - { - out << "BOTTOM"; - } - else - { - out << "value-set-begin: "; - for(auto const &value : values) - { - value->output(out, ai, ns); - out << ", "; - } - out << ":value-set-end"; - } -} diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 75ce1289fda..242b2108366 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -19,6 +19,9 @@ class value_set_abstract_objectt : public abstract_value_objectt { public: + using value_set_abstract_object_ptrt = + std::shared_ptr; + using abstract_object_sett = std::unordered_set< abstract_object_pointert, abstract_hashert, @@ -64,13 +67,7 @@ class value_set_abstract_objectt : public abstract_value_objectt /// Setter for updating the stored values /// \param other_values: the new (non-empty) set of values - void set_values(const abstract_object_sett &other_values) - { - PRECONDITION(!other_values.empty()); - my_type = get_type(*other_values.begin()); - values = other_values; - verify(); - } + void set_values(const abstract_object_sett &other_values); /// Distinguish the type of abstract objects stored in this value-set. enum class abstract_typet @@ -102,31 +99,40 @@ class value_set_abstract_objectt : public abstract_value_objectt const abstract_object_pointert &value, bool merging_write) const override; - /// Enforce casting to interval. - /// \return the stored values abstracted to an interval - abstract_object_pointert get_as_interval() const - { - return to_interval(values); - } - void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override; protected: CLONE + /// \copydoc abstract_object::merge + abstract_object_pointert merge(abstract_object_pointert other) const override; + +private: + abstract_object_pointert evaluate_conditional( + const typet &type, + const std::vector &operands, + const abstract_environmentt &env, + const namespacet &ns) const; + /// Update the set of stored values to \p new_values. Build a new abstract /// object of the right type if necessary. /// \param new_values: potentially new set of values + /// \param environment: the abstract environment /// \return the abstract object representing \p new_values (either 'this' or /// something new) - abstract_object_pointert - resolve_new_values(const abstract_object_sett &new_values) const; + abstract_object_pointert resolve_new_values( + const abstract_object_sett &new_values, + const abstract_environmentt &environment) const; - /// \copydoc abstract_object::merge - abstract_object_pointert merge(abstract_object_pointert other) const override; + /// Update the set of stored values to \p new_values. Build a new abstract + /// object of the right type if necessary. + /// \param new_values: potentially new set of values + /// \return the abstract object representing \p new_values (either 'this' or + /// something new) + abstract_object_pointert + resolve_values(const abstract_object_sett &new_values) const; -private: // data abstract_typet my_type; abstract_object_sett values; @@ -139,84 +145,6 @@ class value_set_abstract_objectt : public abstract_value_objectt /// \copydoc abstract_objectt::verify bool verify() const override; - - /// Recursively construct a combination \p sub_con from \p super_con and once - /// constructed call \p f. - /// \param super_con: vector of some containers storing the values - /// \param sub_con: the one combination being currently constructed - /// \param f: callable with side-effects - template - void apply_comb( - const std::vector &super_con, - std::vector &sub_con, - F f) const - { - size_t n = sub_con.size(); - if(n == super_con.size()) - f(sub_con); - else - { - for(const auto &value : super_con[n]) - { - sub_con.push_back(value); - apply_comb(super_con, sub_con, f); - sub_con.pop_back(); - } - } - } - - /// Call the function \p f on every combination of elements in \p super_con. - /// Hence the arity of \p f is `super_con.size()`. <{1,2},{1},{1,2,3}> -> - /// f(1,1,1), f(1,1,2), f(1,1,3), f(2,1,1), f(2,1,2), f(2,1,3). - /// \param super_con: vector of some containers storing the values - /// \param f: callable with side-effects - template - void for_each_comb(const std::vector &super_con, F f) const - { - std::vector sub_con; - apply_comb(super_con, sub_con, f); - } - - /// Determine abstract-type of an abstract object \p other. - /// \param other: the abstract object to get the type of - /// \return the abstract-type of \p other - static abstract_typet get_type(const abstract_object_pointert &other); - - /// Determine abstract-type of an expression-type \p type. - /// \param type: the expression type to get the abstract-type of - /// \return the abstract-type of \p type - static abstract_typet type_to_abstract_type(const typet &type) - { - if(type.id() == ID_pointer) - { - return abstract_typet::POINTER; - } - else if( - type.id() == ID_signedbv || type.id() == ID_unsignedbv || - type.id() == ID_fixedbv || type.id() == ID_c_bool || - type.id() == ID_bool || type.id() == ID_integer || - type.id() == ID_c_bit_field || type.id() == ID_floatbv) - { - return abstract_typet::CONSTANT; - } - else - { - return abstract_typet::UNSUPPORTED; - } - } - - /// Helper for converting singleton value sets into its only value. - /// \p maybe_singleton: either a set of abstract values or a single value - /// \return an abstract value without context - static abstract_object_pointert - maybe_extract_single_value(const abstract_object_pointert &maybe_singleton); - - /// Helper for converting context objects into its abstract-value children - /// \p maybe_wrapped: either an abstract value (or a set of those) or one - /// wrapped in a context - /// \return an abstract value without context (though it might be as set) - static abstract_object_pointert - maybe_unwrap_context(const abstract_object_pointert &maybe_wrapped); }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp index 6914691afe0..33a96fc70fb 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp @@ -14,16 +14,6 @@ vsd_configt vsd_configt::from_options(const optionst &options) { vsd_configt config{}; - if( - options.get_bool_option("value-set") && - options.get_bool_option("data-dependencies")) - { - throw invalid_command_line_argument_exceptiont{ - "Value set is not currently supported with data dependency analysis", - "--value-set --data-dependencies", - "--data-dependencies"}; - } - config.value_abstract_type = option_to_abstract_type(options, "values", value_option_mappings, CONSTANT); @@ -39,11 +29,8 @@ vsd_configt vsd_configt::from_options(const optionst &options) config.union_abstract_type = option_to_abstract_type( options, "unions", union_option_mappings, UNION_INSENSITIVE); - // This should always be on (for efficeny with 3-way merge) - // Does not work with value set - config.context_tracking.last_write_context = - (config.value_abstract_type != VALUE_SET) && - (config.pointer_abstract_type != VALUE_SET); + // This should always be on (for efficiency with 3-way merge) + config.context_tracking.last_write_context = true; config.context_tracking.data_dependency_context = options.get_bool_option("data-dependencies"); config.advanced_sensitivities.new_value_set = diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp index 544c319ea38..768b2d47083 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp @@ -46,7 +46,7 @@ void variable_sensitivity_domaint::transform( abstract_object_pointert top_object = abstract_state .abstract_object_factory( - to_code_decl(instruction.code).symbol().type(), ns, true) + to_code_decl(instruction.code).symbol().type(), ns, true, false) ->update_location_context(write_location, true); abstract_state.assign( to_code_decl(instruction.code).symbol(), top_object, ns); @@ -318,7 +318,7 @@ void variable_sensitivity_domaint::transform_function_call( std::stack(), nil_exprt(), abstract_state.abstract_object_factory( - called_arg.type().subtype(), ns, true), + called_arg.type().subtype(), ns, true, false), false); } } @@ -331,7 +331,7 @@ void variable_sensitivity_domaint::transform_function_call( abstract_state.assign( symbol_exprt(symbol.first, symbol.second.type), abstract_state.abstract_object_factory( - symbol.second.type, ns, true), + symbol.second.type, ns, true, false), ns); } } diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp index 6cfe844e1cc..dadbc072842 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp @@ -9,8 +9,16 @@ #include "full_array_abstract_object.h" #include "value_set_abstract_value.h" -template -abstract_object_pointert initialize_context_abstract_object( +template +abstract_object_pointert +create_context_abstract_object(const abstract_object_pointert &abstract_object) +{ + return abstract_object_pointert( + new context_classt{abstract_object, abstract_object->type()}); +} + +template +abstract_object_pointert create_abstract_object( const typet type, bool top, bool bottom, @@ -19,22 +27,25 @@ abstract_object_pointert initialize_context_abstract_object( const namespacet &ns) { if(top || bottom) - { - return abstract_object_pointert(new context_classt{ - abstract_object_pointert(new abstract_object_classt{type, top, bottom}), - type, - top, - bottom}); - } - else - { - PRECONDITION(type == ns.follow(e.type())); - return abstract_object_pointert(new context_classt{ - abstract_object_pointert(new abstract_object_classt{e, environment, ns}), - e, - environment, - ns}); - } + return std::make_shared(type, top, bottom); + + PRECONDITION(type == ns.follow(e.type())); + return std::make_shared(e, environment, ns); +} + +abstract_object_pointert wrap_with_context_object( + const abstract_object_pointert &abstract_object, + const vsd_configt &configuration) +{ + if(configuration.context_tracking.data_dependency_context) + return create_context_abstract_object( + abstract_object); + + if(configuration.context_tracking.last_write_context) + return create_context_abstract_object( + abstract_object); + + return abstract_object; } /// Function: variable_sensitivity_object_factoryt::initialize_abstract_object @@ -62,28 +73,10 @@ abstract_object_pointert initialize_abstract_object( const namespacet &ns, const vsd_configt &configuration) { - if(configuration.context_tracking.data_dependency_context) - return initialize_context_abstract_object< - abstract_object_classt, - data_dependency_contextt>(type, top, bottom, e, environment, ns); - if(configuration.context_tracking.last_write_context) - return initialize_context_abstract_object< - abstract_object_classt, - write_location_contextt>(type, top, bottom, e, environment, ns); - else - { - if(top || bottom) - { - return abstract_object_pointert( - new abstract_object_classt{type, top, bottom}); - } - else - { - PRECONDITION(type == ns.follow(e.type())); - return abstract_object_pointert( - new abstract_object_classt{e, environment, ns}); - } - } + auto abstract_object = create_abstract_object( + type, top, bottom, e, environment, ns); + + return wrap_with_context_object(abstract_object, configuration); } ABSTRACT_OBJECT_TYPET @@ -188,3 +181,10 @@ variable_sensitivity_object_factoryt::get_abstract_object( followed_type, top, bottom, e, environment, ns, configuration); } } + +abstract_object_pointert +variable_sensitivity_object_factoryt::wrap_with_context( + const abstract_object_pointert &abstract_object) const +{ + return wrap_with_context_object(abstract_object, configuration); +} diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h index 9ebb4052acf..52d7a183500 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h @@ -71,6 +71,9 @@ class variable_sensitivity_object_factoryt const abstract_environmentt &environment, const namespacet &ns) const; + abstract_object_pointert + wrap_with_context(const abstract_object_pointert &abstract_object) const; + variable_sensitivity_object_factoryt() = delete; variable_sensitivity_object_factoryt( const variable_sensitivity_object_factoryt &) = delete;