diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/main.c b/regression/goto-analyzer/variable-sensitivity-array-access/main.c new file mode 100644 index 00000000000..de801d29732 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-access/main.c @@ -0,0 +1,11 @@ +int main(void) +{ + int arr[] = {1, 2, 3, 4, 5}; + arr[2] = 99; + int arr_0_after_write = arr[0]; + int arr_1_after_write = arr[1]; + int arr_2_after_write = arr[2]; + int arr_3_after_write = arr[3]; + int arr_4_after_write = arr[4]; + return 0; +} diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-every-element.desc new file mode 100644 index 00000000000..a26400f042b --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-every-element.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values constants --vsd-arrays every-element +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_0_after_write \(\) -> 1 +main::1::arr_1_after_write \(\) -> 2 +main::1::arr_2_after_write \(\) -> 99 +main::1::arr_3_after_write \(\) -> 4 +main::1::arr_4_after_write \(\) -> 5 diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-smash.desc new file mode 100644 index 00000000000..f90ca664c29 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-smash.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values constants --vsd-arrays smash +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_0_after_write \(\) -> TOP +main::1::arr_1_after_write \(\) -> TOP +main::1::arr_2_after_write \(\) -> TOP +main::1::arr_3_after_write \(\) -> TOP +main::1::arr_4_after_write \(\) -> TOP diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-up-to-3-elements.desc new file mode 100644 index 00000000000..e998ec846a1 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-access/test-constants-up-to-3-elements.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3 +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_0_after_write \(\) -> 1 +main::1::arr_1_after_write \(\) -> 2 +main::1::arr_2_after_write \(\) -> TOP +main::1::arr_3_after_write \(\) -> TOP +main::1::arr_4_after_write \(\) -> TOP diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-every-element.desc new file mode 100644 index 00000000000..b08cccf785f --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-every-element.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_0_after_write \(\) -> \[1, 1\] +main::1::arr_1_after_write \(\) -> \[2, 2\] +main::1::arr_2_after_write \(\) -> \[63, 63\] +main::1::arr_3_after_write \(\) -> \[4, 4\] +main::1::arr_4_after_write \(\) -> \[5, 5\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-smash.desc new file mode 100644 index 00000000000..9624b4dd66a --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-smash.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values intervals --vsd-arrays smash +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_0_after_write \(\) -> \[1, 63\] +main::1::arr_1_after_write \(\) -> \[1, 63\] +main::1::arr_2_after_write \(\) -> \[1, 63\] +main::1::arr_3_after_write \(\) -> \[1, 63\] +main::1::arr_4_after_write \(\) -> \[1, 63\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-up-to-3-elements.desc new file mode 100644 index 00000000000..17b0aeb1961 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-access/test-intervals-up-to-3-elements.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3 +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_0_after_write \(\) -> \[1, 1\] +main::1::arr_1_after_write \(\) -> \[2, 2\] +main::1::arr_2_after_write \(\) -> \[3, 63\] +main::1::arr_3_after_write \(\) -> \[3, 63\] +main::1::arr_4_after_write \(\) -> \[3, 63\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-every-element.desc new file mode 100644 index 00000000000..46a90e200d0 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-every-element.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_0_after_write \(\) -> value-set-begin: 1 :value-set-end +main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end +main::1::arr_2_after_write \(\) -> value-set-begin: 99 :value-set-end +main::1::arr_3_after_write \(\) -> value-set-begin: 4 :value-set-end +main::1::arr_4_after_write \(\) -> value-set-begin: 5 :value-set-end diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-smash.desc new file mode 100644 index 00000000000..f0224775409 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-smash.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays smash +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_0_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end +main::1::arr_1_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end +main::1::arr_2_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end +main::1::arr_3_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end +main::1::arr_4_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end diff --git a/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-up-to-3-elements.desc new file mode 100644 index 00000000000..1853e917225 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-access/test-value-sets-up-to-3-elements.desc @@ -0,0 +1,10 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3 +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_0_after_write \(\) -> value-set-begin: 1 :value-set-end +main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end +main::1::arr_2_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end +main::1::arr_3_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end +main::1::arr_4_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :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 deleted file mode 100644 index 41aa58a0e10..00000000000 --- a/regression/goto-analyzer/variable-sensitivity-array-constant-access/main.c +++ /dev/null @@ -1,8 +0,0 @@ -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-array-constant-access/test.desc b/regression/goto-analyzer/variable-sensitivity-array-constant-access/test.desc deleted file mode 100644 index 7529dc0db14..00000000000 --- a/regression/goto-analyzer/variable-sensitivity-array-constant-access/test.desc +++ /dev/null @@ -1,7 +0,0 @@ -CORE -main.c ---show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element -^EXIT=0$ -^SIGNAL=0$ -main::1::second_value \(\) -> \[2, 2\] @ \[3\] -main::1::second_value_after_write \(\) -> \[A, A\] @ \[6\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-interval-access/main.c b/regression/goto-analyzer/variable-sensitivity-array-interval-access/main.c deleted file mode 100644 index 12756805712..00000000000 --- a/regression/goto-analyzer/variable-sensitivity-array-interval-access/main.c +++ /dev/null @@ -1,33 +0,0 @@ -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-interval-access/test.desc b/regression/goto-analyzer/variable-sensitivity-array-interval-access/test.desc deleted file mode 100644 index cda03981764..00000000000 --- a/regression/goto-analyzer/variable-sensitivity-array-interval-access/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -CORE -main.c ---show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element -^EXIT=0$ -^SIGNAL=0$ -main::1::arr_at_ix \(\) -> \[1, 3\] @ \[9\] -main::1::arr_0_after_write \(\) -> \[1, 4\] @ \[18\] -main::1::arr_1_after_write \(\) -> \[2, 4\] @ \[20\] -main::1::arr_2_after_write \(\) -> \[3, 3\] @ \[22\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-value-set-access/main.c b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/main.c similarity index 68% rename from regression/goto-analyzer/variable-sensitivity-array-value-set-access/main.c rename to regression/goto-analyzer/variable-sensitivity-array-nondet-access/main.c index 12756805712..0b97acb0cbc 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-value-set-access/main.c +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/main.c @@ -1,6 +1,6 @@ int main(void) { - int arr[] = {1, 2, 3}; + int arr[] = {1, 2, 3, 4, 5}; int ix; if(ix) { @@ -10,9 +10,11 @@ int main(void) { 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) { @@ -20,14 +22,13 @@ int main(void) } else { - write_ix = 1; + write_ix = 4; } - arr[write_ix] = 4; + arr[write_ix] = 99; 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]; + int arr_3_after_write = arr[3]; + int arr_4_after_write = arr[4]; return 0; } diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc new file mode 100644 index 00000000000..879c0c1bcac --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-every-element.desc @@ -0,0 +1,11 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values constants --vsd-arrays every-element +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_at_ix \(\) -> TOP @ \[9\] +main::1::arr_0_after_write \(\) -> TOP @ \[18\] +main::1::arr_1_after_write \(\) -> TOP @ \[20\] +main::1::arr_2_after_write \(\) -> TOP @ \[22\] +main::1::arr_3_after_write \(\) -> TOP @ \[24\] +main::1::arr_4_after_write \(\) -> TOP @ \[26\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc new file mode 100644 index 00000000000..deacba9c6e6 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-smash.desc @@ -0,0 +1,11 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values constants --vsd-arrays smash +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_at_ix \(\) -> TOP @ \[9\] +main::1::arr_0_after_write \(\) -> TOP +main::1::arr_1_after_write \(\) -> TOP +main::1::arr_2_after_write \(\) -> TOP +main::1::arr_3_after_write \(\) -> TOP +main::1::arr_4_after_write \(\) -> TOP diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc new file mode 100644 index 00000000000..3fb6c82d79c --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-constants-up-to-3-elements.desc @@ -0,0 +1,11 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3 +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_at_ix \(\) -> TOP @ \[9\] +main::1::arr_0_after_write \(\) -> TOP +main::1::arr_1_after_write \(\) -> TOP +main::1::arr_2_after_write \(\) -> TOP +main::1::arr_3_after_write \(\) -> TOP +main::1::arr_4_after_write \(\) -> TOP diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc new file mode 100644 index 00000000000..710fdd3d18e --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-every-element.desc @@ -0,0 +1,11 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values intervals --vsd-arrays every-element +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_at_ix \(\) -> \[1, 3\] @ \[9\] +main::1::arr_0_after_write \(\) -> \[1, 63\] @ \[18\] +main::1::arr_1_after_write \(\) -> \[2, 63\] @ \[20\] +main::1::arr_2_after_write \(\) -> \[3, 63\] @ \[22\] +main::1::arr_3_after_write \(\) -> \[4, 63\] @ \[24\] +main::1::arr_4_after_write \(\) -> \[5, 63\] @ \[26\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc new file mode 100644 index 00000000000..e7f601c1223 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-smash.desc @@ -0,0 +1,11 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values intervals --vsd-arrays smash +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\] +main::1::arr_0_after_write \(\) -> \[1, 63\] +main::1::arr_1_after_write \(\) -> \[1, 63\] +main::1::arr_2_after_write \(\) -> \[1, 63\] +main::1::arr_3_after_write \(\) -> \[1, 63\] +main::1::arr_4_after_write \(\) -> \[1, 63\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc new file mode 100644 index 00000000000..86ab2641d45 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-intervals-up-to-3-elements.desc @@ -0,0 +1,11 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values intervals --vsd-arrays up-to-n-elements --vsd-array-max-elements 3 +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_at_ix \(\) -> \[1, 5\] @ \[9\] +main::1::arr_0_after_write \(\) -> \[1, 63\] +main::1::arr_1_after_write \(\) -> \[2, 63\] +main::1::arr_2_after_write \(\) -> \[3, 63\] +main::1::arr_3_after_write \(\) -> \[3, 63\] +main::1::arr_4_after_write \(\) -> \[3, 63\] diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-every-element.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-every-element.desc new file mode 100644 index 00000000000..fab9274c012 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-every-element.desc @@ -0,0 +1,11 @@ +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, 99 :value-set-end +main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end +main::1::arr_2_after_write \(\) -> value-set-begin: 3 :value-set-end +main::1::arr_3_after_write \(\) -> value-set-begin: 4 :value-set-end +main::1::arr_4_after_write \(\) -> value-set-begin: 5, 99 :value-set-end diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-smash.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-smash.desc new file mode 100644 index 00000000000..ffaaedd6cd0 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-smash.desc @@ -0,0 +1,11 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays smash +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_at_ix \(\) -> value-set-begin: 1, 2, 3, 4, 5 :value-set-end +main::1::arr_0_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end +main::1::arr_1_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end +main::1::arr_2_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end +main::1::arr_3_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end +main::1::arr_4_after_write \(\) -> value-set-begin: 1, 2, 3, 4, 5, 99 :value-set-end diff --git a/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-up-to-3-elements.desc b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-up-to-3-elements.desc new file mode 100644 index 00000000000..081c19c949e --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-nondet-access/test-value-sets-up-to-3-elements.desc @@ -0,0 +1,11 @@ +CORE +main.c +--show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays up-to-n-elements --vsd-array-max-elements 3 +^EXIT=0$ +^SIGNAL=0$ +main::1::arr_at_ix \(\) -> value-set-begin: 1, 3, 4, 5 :value-set-end +main::1::arr_0_after_write \(\) -> value-set-begin: 1, 99 :value-set-end +main::1::arr_1_after_write \(\) -> value-set-begin: 2 :value-set-end +main::1::arr_2_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end +main::1::arr_3_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end +main::1::arr_4_after_write \(\) -> value-set-begin: 3, 4, 5, 99 :value-set-end 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 deleted file mode 100644 index ec83e23bc98..00000000000 --- a/regression/goto-analyzer/variable-sensitivity-array-value-set-access/test.desc +++ /dev/null @@ -1,9 +0,0 @@ -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/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index d4ea02735f0..9e9807e6591 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -337,10 +337,9 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory( type, top, bttm, e, environment, ns); } -abstract_object_pointert abstract_environmentt::add_object_context( - const abstract_object_pointert &abstract_object) const +const vsd_configt &abstract_environmentt::configuration() const { - return object_factory->wrap_with_context(abstract_object); + return object_factory->config(); } bool abstract_environmentt::merge( diff --git a/src/analyses/variable-sensitivity/abstract_environment.h b/src/analyses/variable-sensitivity/abstract_environment.h index cd02699c2b2..ec3bdd0add9 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.h +++ b/src/analyses/variable-sensitivity/abstract_environment.h @@ -35,6 +35,8 @@ enum class widen_modet could_widen }; +struct vsd_configt; + class abstract_environmentt { public: @@ -174,18 +176,8 @@ 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; + /// Exposes the environment configuration + const vsd_configt &configuration() const; /// Computes the join between "this" and "b" /// diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp index b0b47e9f0bc..8fcdcc3f6db 100644 --- a/src/analyses/variable-sensitivity/full_array_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_array_abstract_object.cpp @@ -9,6 +9,7 @@ #include #include +#include #include #include #include @@ -18,11 +19,21 @@ #include "location_update_visitor.h" #include "map_visit.h" -bool eval_index( - const exprt &index, +struct eval_index_resultt +{ + bool is_good; + mp_integer value; + bool overrun; +}; + +static eval_index_resultt eval_index( + const exprt &expr, const abstract_environmentt &env, - const namespacet &ns, - mp_integer &out_index); + const namespacet &ns); +static eval_index_resultt eval_index( + const mp_integer &index, + const abstract_environmentt &env, + const namespacet &ns); template abstract_object_pointert apply_to_index_range( @@ -76,11 +87,12 @@ full_array_abstract_objectt::full_array_abstract_objectt( { if(expr.id() == ID_array) { - int index = 0; + mp_integer i = 0; for(const exprt &entry : expr.operands()) { - map.insert(mp_integer(index), environment.eval(entry, ns)); - ++index; + auto index = eval_index(i, environment, ns); + map_put(index.value, environment.eval(entry, ns), index.overrun); + ++i; } set_not_top(); } @@ -205,33 +217,26 @@ abstract_object_pointert full_array_abstract_objectt::read_element( const namespacet &ns) const { PRECONDITION(!is_bottom()); - mp_integer index_value; - if(eval_index(expr, env, ns, index_value)) - { - // Here we are assuming it is always in bounds - auto const value = map.find(index_value); - if(value.has_value()) - return value.value(); - return get_top_entry(env, ns); - } - else - { - // Although we don't know where we are reading from, and therefore - // we should be returning a TOP value, we may still have useful - // additional information in elements of the array - such as write - // histories so we merge all the known array elements with TOP and return - // that. + auto index = eval_index(expr, env, ns); - // Create a new TOP value of the appropriate element type - abstract_object_pointert result = get_top_entry(env, ns); + if(index.is_good) + return map_find_or_top(index.value, env, ns); - // Merge each known element into the TOP value - for(const auto &element : map.get_view()) - result = - abstract_objectt::merge(result, element.second, widen_modet::no).object; + // Although we don't know where we are reading from, and therefore + // we should be returning a TOP value, we may still have useful + // additional information in elements of the array - such as write + // histories so we merge all the known array elements with TOP and return + // that. - return result; - } + // Create a new TOP value of the appropriate element type + auto result = get_top_entry(env, ns); + + // Merge each known element into the TOP value + for(const auto &element : map.get_view()) + result = + abstract_objectt::merge(result, element.second, widen_modet::no).object; + + return result; } abstract_object_pointert full_array_abstract_objectt::write_element( @@ -266,29 +271,17 @@ abstract_object_pointert full_array_abstract_objectt::write_sub_element( const auto &result = std::dynamic_pointer_cast(mutable_clone()); - mp_integer index_value; - bool good_index = eval_index(expr, environment, ns, index_value); + auto index = eval_index(expr, environment, ns); - if(good_index) + if(index.is_good) { // We were able to evaluate the index to a value, which we // assume is in bounds... - auto const old_value = map.find(index_value); - - if(old_value.has_value()) - { - result->map.replace( - index_value, - environment.write(old_value.value(), value, stack, ns, merging_write)); - } - else - { - result->map.insert( - index_value, - environment.write( - get_top_entry(environment, ns), value, stack, ns, merging_write)); - } - + auto const existing_value = map_find_or_top(index.value, environment, ns); + result->map_put( + index.value, + environment.write(existing_value, value, stack, ns, merging_write), + index.overrun); result->set_not_top(); DATA_INVARIANT(result->verify(), "Structural invariants maintained"); return result; @@ -321,10 +314,9 @@ abstract_object_pointert full_array_abstract_objectt::write_leaf_element( const auto &result = std::dynamic_pointer_cast(mutable_clone()); - mp_integer index_value; - bool good_index = eval_index(expr, environment, ns, index_value); + auto index = eval_index(expr, environment, ns); - if(good_index) + if(index.is_good) { // We were able to evaluate the index expression to a constant if(merging_write) @@ -337,11 +329,11 @@ abstract_object_pointert full_array_abstract_objectt::write_leaf_element( INVARIANT(!result->map.empty(), "If not top, map cannot be empty"); - auto old_value = result->map.find(index_value); + auto old_value = result->map.find(index.value); if(old_value.has_value()) // if not found it's top, so nothing to merge { result->map.replace( - index_value, + index.value, abstract_objectt::merge(old_value.value(), value, widen_modet::no) .object); } @@ -351,14 +343,9 @@ abstract_object_pointert full_array_abstract_objectt::write_leaf_element( } else { - auto old_value = result->map.find(index_value); - - if(old_value.has_value()) - result->map.replace(index_value, value); - else - result->map.insert(index_value, value); - + result->map_put(index.value, value, index.overrun); result->set_not_top(); + DATA_INVARIANT(result->verify(), "Structural invariants maintained"); return result; } @@ -370,6 +357,39 @@ abstract_object_pointert full_array_abstract_objectt::write_leaf_element( environment, ns, std::stack(), expr, value, merging_write); } +void full_array_abstract_objectt::map_put( + mp_integer index_value, + const abstract_object_pointert &value, + bool overrun) +{ + auto old_value = map.find(index_value); + + if(!old_value.has_value()) + map.insert(index_value, value); + else + { + // if we're over the max_index, merge with existing value + auto replacement_value = + overrun + ? abstract_objectt::merge(old_value.value(), value, widen_modet::no) + .object + : value; + + map.replace(index_value, replacement_value); + } +} + +abstract_object_pointert full_array_abstract_objectt::map_find_or_top( + mp_integer index_value, + const abstract_environmentt &env, + const namespacet &ns) const +{ + auto value = map.find(index_value); + if(value.has_value()) + return value.value(); + return get_top_entry(env, ns); +} + abstract_object_pointert full_array_abstract_objectt::get_top_entry( const abstract_environmentt &env, const namespacet &ns) const @@ -438,20 +458,33 @@ void full_array_abstract_objectt::statistics( statistics.objects_memory_usage += memory_sizet::from_bytes(sizeof(*this)); } -bool eval_index( +static eval_index_resultt eval_index( const exprt &expr, const abstract_environmentt &env, - const namespacet &ns, - mp_integer &out_index) + const namespacet &ns) { - const index_exprt &index = to_index_expr(expr); - abstract_object_pointert index_abstract_object = env.eval(index.index(), ns); - exprt value = index_abstract_object->to_constant(); + const auto &index_expr = to_index_expr(expr); + auto index_abstract_object = env.eval(index_expr.index(), ns); + auto value = index_abstract_object->to_constant(); if(!value.is_constant()) - return false; + return {false}; + + mp_integer out_index; + bool result = to_integer(to_constant_expr(value), out_index); + if(result) + return {false}; + + return eval_index(out_index, env, ns); +} + +static eval_index_resultt eval_index( + const mp_integer &index, + const abstract_environmentt &env, + const namespacet &ns) +{ + auto max_array_index = env.configuration().maximum_array_index; + bool overrun = (index >= max_array_index); - constant_exprt constant_index = to_constant_expr(value); - bool result = to_integer(constant_index, out_index); - return !result; + return {true, overrun ? max_array_index : index, overrun}; } diff --git a/src/analyses/variable-sensitivity/full_array_abstract_object.h b/src/analyses/variable-sensitivity/full_array_abstract_object.h index 19a825aa99e..3cfd2757e1b 100644 --- a/src/analyses/variable-sensitivity/full_array_abstract_object.h +++ b/src/analyses/variable-sensitivity/full_array_abstract_object.h @@ -203,6 +203,15 @@ class full_array_abstract_objectt : public abstract_aggregate_objectt< shared_array_mapt map; + void map_put( + mp_integer index, + const abstract_object_pointert &value, + bool overrun); + abstract_object_pointert map_find_or_top( + mp_integer index, + const abstract_environmentt &env, + const namespacet &ns) const; + /// Short hand method for creating a top element of the array /// /// \param env: the abstract environment diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp index 9ed528bf52f..888dc038780 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp @@ -10,8 +10,13 @@ /// domain abstractions are used, flow sensitivity, etc #include "variable_sensitivity_configuration.h" +#include #include +static void check_one_of_options( + const optionst &options, + const std::vector &names); + vsd_configt vsd_configt::from_options(const optionst &options) { vsd_configt config{}; @@ -36,11 +41,14 @@ vsd_configt vsd_configt::from_options(const optionst &options) config.context_tracking.data_dependency_context = options.get_bool_option("data-dependencies"); config.context_tracking.liveness = options.get_bool_option("liveness"); + check_one_of_options(options, {"data-dependencies", "liveness"}); config.flow_sensitivity = (options.get_bool_option("flow-insensitive")) ? flow_sensitivityt::insensitive : flow_sensitivityt::sensitive; + config.maximum_array_index = configure_max_array_size(options); + return config; } @@ -52,6 +60,7 @@ vsd_configt vsd_configt::constant_domain() config.pointer_abstract_type = POINTER_SENSITIVE; config.struct_abstract_type = STRUCT_SENSITIVE; config.array_abstract_type = ARRAY_SENSITIVE; + config.maximum_array_index = std::numeric_limits::max(); return config; } @@ -62,6 +71,7 @@ vsd_configt vsd_configt::value_set() config.pointer_abstract_type = VALUE_SET_OF_POINTERS; config.struct_abstract_type = STRUCT_SENSITIVE; config.array_abstract_type = ARRAY_SENSITIVE; + config.maximum_array_index = std::numeric_limits::max(); return config; } @@ -73,6 +83,7 @@ vsd_configt vsd_configt::intervals() config.pointer_abstract_type = POINTER_SENSITIVE; config.struct_abstract_type = STRUCT_SENSITIVE; config.array_abstract_type = ARRAY_SENSITIVE; + config.maximum_array_index = std::numeric_limits::max(); return config; } @@ -92,15 +103,25 @@ const vsd_configt::option_mappingt vsd_configt::struct_option_mappings = { const vsd_configt::option_mappingt vsd_configt::array_option_mappings = { {"top-bottom", ARRAY_INSENSITIVE}, + {"smash", ARRAY_SENSITIVE}, + {"up-to-n-elements", ARRAY_SENSITIVE}, {"every-element", ARRAY_SENSITIVE}}; +const vsd_configt::option_size_mappingt + vsd_configt::array_option_size_mappings = { + {"top-bottom", 0}, + {"smash", 0}, + {"up-to-n-elements", 10}, + {"every-element", std::numeric_limits::max()}}; + const vsd_configt::option_mappingt vsd_configt::union_option_mappings = { {"top-bottom", UNION_INSENSITIVE}}; -invalid_command_line_argument_exceptiont vsd_configt::invalid_argument( +template +invalid_command_line_argument_exceptiont invalid_argument( const std::string &option_name, const std::string &bad_argument, - const option_mappingt &mapping) + const mappingt &mapping) { auto option = "--vsd-" + option_name; auto choices = std::string(""); @@ -132,3 +153,56 @@ ABSTRACT_OBJECT_TYPET vsd_configt::option_to_abstract_type( } return selected->second; } + +size_t vsd_configt::configure_max_array_size(const optionst &options) +{ + if(options.get_option("arrays") == "up-to-n-elements") + { + size_t max_elements = options.get_unsigned_int_option("array-max-elements"); + if(max_elements != 0) + return max_elements - 1; + } + return option_to_size(options, "arrays", array_option_size_mappings); +} + +size_t vsd_configt::option_to_size( + const optionst &options, + const std::string &option_name, + const option_size_mappingt &mapping) +{ + const size_t def = std::numeric_limits::max(); + const auto argument = options.get_option(option_name); + + if(argument.empty()) + return def; + + auto selected = mapping.find(argument); + if(selected == mapping.end()) + { + throw invalid_argument(option_name, argument, mapping); + } + return selected->second; +} + +void check_one_of_options( + const optionst &options, + const std::vector &names) +{ + int how_many = 0; + for(auto &name : names) + how_many += options.get_bool_option(name); + + if(how_many <= 1) + return; + + auto choices = std::string(""); + for(auto &name : names) + { + choices += (!choices.empty() ? "|" : ""); + auto option = "--vsd-" + name; + choices += option; + } + + throw invalid_command_line_argument_exceptiont{"Conflicting arguments", + "Can only use of " + choices}; +} diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h index 172035c4e52..d3b21795207 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h @@ -51,6 +51,8 @@ struct vsd_configt flow_sensitivityt flow_sensitivity; + size_t maximum_array_index = 0; + struct { bool liveness; @@ -58,11 +60,6 @@ struct vsd_configt bool last_write_context; } context_tracking; - struct - { - bool new_value_set; - } advanced_sensitivities; - static vsd_configt from_options(const optionst &options); static vsd_configt constant_domain(); @@ -76,13 +73,13 @@ struct vsd_configt array_abstract_type{ARRAY_INSENSITIVE}, union_abstract_type{UNION_INSENSITIVE}, flow_sensitivity{flow_sensitivityt::sensitive}, - context_tracking{false, true}, - advanced_sensitivities{false} + context_tracking{false, true} { } private: using option_mappingt = std::map; + using option_size_mappingt = std::map; static ABSTRACT_OBJECT_TYPET option_to_abstract_type( const optionst &options, @@ -90,15 +87,18 @@ struct vsd_configt const option_mappingt &mapping, ABSTRACT_OBJECT_TYPET default_type); - static invalid_command_line_argument_exceptiont invalid_argument( + static size_t configure_max_array_size(const optionst &options); + + static size_t option_to_size( + const optionst &options, const std::string &option_name, - const std::string &bad_argument, - const option_mappingt &mapping); + const option_size_mappingt &mapping); static const option_mappingt value_option_mappings; static const option_mappingt pointer_option_mappings; static const option_mappingt struct_option_mappings; static const option_mappingt array_option_mappings; + static const option_size_mappingt array_option_size_mappings; static const option_mappingt union_option_mappings; }; diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h index c8a4d74de47..e8978978c42 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.h @@ -75,6 +75,7 @@ "(vsd-values):" \ "(vsd-structs):" \ "(vsd-arrays):" \ + "(vsd-array-max-elements):" \ "(vsd-pointers):" \ "(vsd-unions):" \ "(vsd-flow-insensitive)" \ @@ -88,7 +89,9 @@ " --vsd-structs struct field sensitive analysis - " \ "top-bottom|every-field\n" /* NOLINT(whitespace/line_length) */ \ " --vsd-arrays array entry sensitive analysis - " \ - "top-bottom|every-element\n" /* NOLINT(whitespace/line_length) */ \ + "top-bottom|smash|up-to-n-elements|every-element\n" /* NOLINT(whitespace/line_length) */ \ + " --vsd-array-max-elements the n in --vsd-arrays up-to-n-elements - " \ + "defaults 10 if not given" /* NOLINT(whitespace/line_length) */ \ " --vsd-pointers pointer sensitive analysis - " \ "top-bottom|constants|value-set\n" /* NOLINT(whitespace/line_length) */ \ " --vsd-unions union sensitive analysis - top-bottom\n" \ @@ -102,6 +105,7 @@ options.set_option("values", cmdline.get_value("vsd-values")); \ options.set_option("pointers", cmdline.get_value("vsd-pointers")); \ options.set_option("arrays", cmdline.get_value("vsd-arrays")); \ + options.set_option("array-max-elements", cmdline.get_value("vsd-array-max-elements")); /* NOLINT(whitespace/line_length) */ \ options.set_option("structs", cmdline.get_value("vsd-structs")); \ options.set_option("unions", cmdline.get_value("vsd-unions")); \ options.set_option("flow-insensitive", cmdline.isset("vsd-flow-insensitive")); /* NOLINT(whitespace/line_length) */ \ diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h index 2d4a1143892..8a9f0701eca 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h @@ -77,6 +77,11 @@ class variable_sensitivity_object_factoryt variable_sensitivity_object_factoryt( const variable_sensitivity_object_factoryt &) = delete; + const vsd_configt &config() const + { + return configuration; + } + private: /// Decide which abstract object type to use for the variable in question. /// diff --git a/unit/Makefile b/unit/Makefile index 68a16dc3b0e..957280b17ce 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -22,6 +22,7 @@ SRC += analyses/ai/ai.cpp \ analyses/variable-sensitivity/constant_abstract_value/to_predicate.cpp \ analyses/variable-sensitivity/constant_pointer_abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp \ + analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp \ analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \ analyses/variable-sensitivity/full_array_abstract_object/to_predicate.cpp \ analyses/variable-sensitivity/eval.cpp \ diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp index da2d6c0b4ee..9b68d9e30f5 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.cpp @@ -10,6 +10,7 @@ #include #include #include +#include #include full_array_abstract_objectt::full_array_pointert build_array( @@ -26,15 +27,17 @@ full_array_abstract_objectt::full_array_pointert build_array( abstract_environmentt &environment, const namespacet &ns) { + const typet type = signedbv_typet(32); + const array_typet array_type( - integer_typet(), from_integer(array.size(), integer_typet())); + integer_typet(), from_integer(array.size(), type)); exprt::operandst element_ops; for(auto element : array) { if(element != TOP_MEMBER) - element_ops.push_back(from_integer(element, integer_typet())); + element_ops.push_back(from_integer(element, type)); else element_ops.push_back(nil_exprt()); } @@ -56,13 +59,3 @@ full_array_abstract_objectt::full_array_pointert build_bottom_array() array_typet(integer_typet(), from_integer(3, integer_typet())); return std::make_shared(array_type, false, true); } - -exprt read_index( - full_array_abstract_objectt::full_array_pointert array_object, - const index_exprt &index, - abstract_environmentt &environment, - const namespacet &ns) -{ - return array_object->expression_transform(index, {}, environment, ns) - ->to_constant(); -} diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h index d36cae3cd83..5569a7527e1 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/array_builder.h @@ -25,10 +25,4 @@ full_array_abstract_objectt::full_array_pointert build_top_array(); full_array_abstract_objectt::full_array_pointert build_bottom_array(); -exprt read_index( - full_array_abstract_objectt::full_array_pointert array_object, - const index_exprt &index, - abstract_environmentt &environment, - const namespacet &ns); - #endif diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp new file mode 100644 index 00000000000..046219e105d --- /dev/null +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/maximum_length.cpp @@ -0,0 +1,176 @@ +/*******************************************************************\ + + Module: Tests for full_array_abstract_objectt maximum length + + Author: Jez Higgins + +\*******************************************************************/ + +#include "array_builder.h" +#include +#include +#include +#include +#include +#include + +using abstract_object_ptrt = std::shared_ptr; + +static abstract_object_ptrt write_array( + const abstract_object_ptrt &array, + int index, + int new_value, + abstract_environmentt &env, + namespacet &ns) +{ + const typet type = signedbv_typet(32); + + return array->write( + env, + ns, + std::stack(), + index_exprt(nil_exprt(), from_integer(index, type)), + env.eval(from_integer(new_value, type), ns), + false); +} + +SCENARIO( + "arrays have maximum length", + "[core][analyses][variable-sensitivity][full_array_abstract_object][max_" + "array]") +{ + for(size_t max_array_index = 10; max_array_index <= 20; max_array_index += 10) + { + auto configuration = vsd_configt::value_set(); + configuration.maximum_array_index = max_array_index; + + auto object_factory = + variable_sensitivity_object_factoryt::configured_with(configuration); + abstract_environmentt environment(object_factory); + environment.make_top(); + symbol_tablet symbol_table; + namespacet ns(symbol_table); + WHEN("maximum size is " + std::to_string(max_array_index)) + { + WHEN("array = {1, 2, 3}, writes under maximum size") + { + WHEN("array[3] = 4") + { + auto array = build_array({1, 2, 3}, environment, ns); + + auto updated = write_array(array, 3, 4, environment, ns); + + THEN("array equals {1, 2, 3, 4}") + { + EXPECT_INDEX(updated, 0, 1, environment, ns); + EXPECT_INDEX(updated, 1, 2, environment, ns); + EXPECT_INDEX(updated, 2, 3, environment, ns); + EXPECT_INDEX(updated, 3, 4, environment, ns); + } + } + WHEN("a[0] = 99") + { + auto array = build_array({1, 2, 3}, environment, ns); + + auto updated = write_array(array, 0, 99, environment, ns); + + THEN("array equals {99, 2, 3}") + { + EXPECT_INDEX(updated, 0, 99, environment, ns); + EXPECT_INDEX(updated, 1, 2, environment, ns); + EXPECT_INDEX(updated, 2, 3, environment, ns); + } + } + WHEN("a[5] = 99") + { + auto array = build_array({1, 2, 3}, environment, ns); + + auto updated = write_array(array, 5, 99, environment, ns); + + THEN("array equals {1, 2, 3, , , 99}") + { + EXPECT_INDEX(updated, 0, 1, environment, ns); + EXPECT_INDEX(updated, 1, 2, environment, ns); + EXPECT_INDEX(updated, 2, 3, environment, ns); + EXPECT_INDEX_TOP(updated, 3, environment, ns); + EXPECT_INDEX_TOP(updated, 4, environment, ns); + EXPECT_INDEX(updated, 5, 99, environment, ns); + } + } + } + WHEN("array = {1, 2, 3}, writes beyond maximum size mapped to max_size") + { + WHEN("array[99] = 4") + { + auto array = build_array({1, 2, 3}, environment, ns); + + auto updated = write_array(array, 99, 4, environment, ns); + + THEN( + "array equals {1, 2, 3, ..., [" + std::to_string(max_array_index) + + "] = 4}") + { + EXPECT_INDEX(updated, 0, 1, environment, ns); + EXPECT_INDEX(updated, 1, 2, environment, ns); + EXPECT_INDEX(updated, 2, 3, environment, ns); + EXPECT_INDEX(updated, max_array_index, 4, environment, ns); + } + } + } + WHEN("array = {1, 2, 3}, reads beyond maximum size mapped to max_size") + { + WHEN("a[max] = 4") + { + auto array = build_array({1, 2, 3}, environment, ns); + + auto updated = + write_array(array, max_array_index, 4, environment, ns); + + for(size_t i = max_array_index; i <= max_array_index * 3; i += 5) + THEN("array[" + std::to_string(i) + "] = 4}") + { + EXPECT_INDEX(updated, i, 4, environment, ns); + } + } + } + WHEN("array = {1, 2, 3}, writes beyond maximum size are merged") + { + WHEN("array[98] = 3, array[99] = 4") + { + auto array = build_array({1, 2, 3}, environment, ns); + + auto updated = write_array(array, 99, 4, environment, ns); + updated = write_array(updated, 98, 3, environment, ns); + + THEN( + "array equals {1, 2, 3, ..., [" + std::to_string(max_array_index) + + "] = TOP}") + { + EXPECT_INDEX(updated, 0, 1, environment, ns); + EXPECT_INDEX(updated, 1, 2, environment, ns); + EXPECT_INDEX(updated, 2, 3, environment, ns); + EXPECT_INDEX(updated, max_array_index, {3, 4}, environment, ns); + } + } + WHEN("array[99] = 3, array[99] = 4, array[100] = 5") + { + auto array = build_array({1, 2, 3}, environment, ns); + + auto updated = write_array(array, 100, 5, environment, ns); + updated = write_array(updated, 99, 4, environment, ns); + updated = write_array(updated, 98, 3, environment, ns); + + THEN( + "array equals {1, 2, 3, ..., [" + std::to_string(max_array_index) + + "] = TOP}") + { + EXPECT_INDEX(updated, 0, 1, environment, ns); + EXPECT_INDEX(updated, 1, 2, environment, ns); + EXPECT_INDEX(updated, 2, 3, environment, ns); + EXPECT_INDEX(updated, max_array_index, {3, 4, 5}, environment, ns); + } + } + } + } + } +} diff --git a/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp index f934dfeb6f4..6589b444d3d 100644 --- a/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp +++ b/unit/analyses/variable-sensitivity/full_array_abstract_object/merge.cpp @@ -16,6 +16,7 @@ #include #include +#include #include #include #include @@ -24,22 +25,21 @@ SCENARIO( "merge_constant_array_abstract_object", "[core]" - "[analyses][variable-sensitivity][constant_array_abstract_object][merge]") + "[analyses][variable-sensitivity][full_array_abstract_object][merge]") { GIVEN("Two arrays of size 3, whose first elements are the same") { + const typet type = signedbv_typet(32); + // int val2[3] = {1, 2, 3} auto val1 = std::vector{1, 2, 3}; // int val2[3] = {1, 4, 5} auto val2 = std::vector{1, 4, 5}; // index_exprt for reading from an array - const index_exprt i0 = - index_exprt(nil_exprt(), from_integer(0, integer_typet())); - const index_exprt i1 = - index_exprt(nil_exprt(), from_integer(1, integer_typet())); - const index_exprt i2 = - index_exprt(nil_exprt(), from_integer(2, integer_typet())); + const index_exprt i0 = index_exprt(nil_exprt(), from_integer(0, type)); + const index_exprt i1 = index_exprt(nil_exprt(), from_integer(1, type)); + const index_exprt i2 = index_exprt(nil_exprt(), from_integer(2, type)); auto object_factory = variable_sensitivity_object_factoryt::configured_with( vsd_configt::constant_domain()); @@ -55,24 +55,14 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); THEN("The original constant array AO should be returned") { - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); - // Correctness of merge REQUIRE_FALSE(result.modified); - REQUIRE_FALSE(cast_result->is_top()); - REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE( - read_index(cast_result, i0, environment, ns) == to_expr(val1[0])); - REQUIRE( - read_index(cast_result, i1, environment, ns) == to_expr(val1[1])); - REQUIRE( - read_index(cast_result, i2, environment, ns) == to_expr(val1[2])); + REQUIRE_FALSE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); + for(int i = 0; i != 3; ++i) + EXPECT_INDEX(result.object, i, val1[i], environment, ns); // Is optimal REQUIRE(result.object == op1); @@ -85,25 +75,17 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); - THEN( "A new constant array AO whose first value is the same and " "the other two are top") { - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); - // Correctness of merge REQUIRE(result.modified); - REQUIRE_FALSE(cast_result->is_top()); - REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE( - read_index(cast_result, i0, environment, ns) == to_expr(val1[0])); - REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); - REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); + REQUIRE_FALSE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); + EXPECT_INDEX(result.object, 0, val1[0], environment, ns); + EXPECT_INDEX_TOP(result.object, 1, environment, ns); + EXPECT_INDEX_TOP(result.object, 1, environment, ns); // Since it has modified, we definitely shouldn't be reusing the pointer REQUIRE_FALSE(result.object == op1); @@ -118,21 +100,14 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); THEN("A new constant array AO set to top should be returned") { - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); - // Correctness of merge REQUIRE(result.modified); - REQUIRE(cast_result->is_top()); - REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(read_index(cast_result, i0, environment, ns) == nil_exprt()); - REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); - REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); + for(int i = 0; i != 3; ++i) + EXPECT_INDEX_TOP(result.object, i, environment, ns); // We can't reuse the abstract object as the value has changed REQUIRE(result.object != op1); @@ -147,24 +122,14 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); THEN("The original const AO should be returned") { - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); - // Correctness of merge REQUIRE_FALSE(result.modified); - REQUIRE_FALSE(cast_result->is_top()); - REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE( - read_index(cast_result, i0, environment, ns) == to_expr(val1[0])); - REQUIRE( - read_index(cast_result, i1, environment, ns) == to_expr(val1[1])); - REQUIRE( - read_index(cast_result, i2, environment, ns) == to_expr(val1[2])); + REQUIRE_FALSE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); + for(int i = 0; i != 3; ++i) + EXPECT_INDEX(result.object, i, val1[i], environment, ns); // Is optimal REQUIRE(result.object == op1); @@ -179,21 +144,14 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); THEN("The original constant array AO should be returned") { - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); - // Correctness of merge REQUIRE_FALSE(result.modified); - REQUIRE(cast_result->is_top()); - REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(read_index(cast_result, i0, environment, ns) == nil_exprt()); - REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); - REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); + for(int i = 0; i != 3; ++i) + EXPECT_INDEX_TOP(result.object, i, environment, ns); // Is optimal REQUIRE(result.object == op1); @@ -208,21 +166,14 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); THEN("The original constant array AO should be returned") { - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); - // Correctness of merge REQUIRE_FALSE(result.modified); - REQUIRE(cast_result->is_top()); - REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(read_index(cast_result, i0, environment, ns) == nil_exprt()); - REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); - REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); + for(int i = 0; i != 3; ++i) + EXPECT_INDEX_TOP(result.object, i, environment, ns); // Is optimal REQUIRE(result.object == op1); @@ -237,21 +188,14 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); THEN("The original constant array AO should be returned") { - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); - // Correctness of merge REQUIRE_FALSE(result.modified); - REQUIRE(cast_result->is_top()); - REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(read_index(cast_result, i0, environment, ns) == nil_exprt()); - REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); - REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); + for(int i = 0; i != 3; ++i) + EXPECT_INDEX_TOP(result.object, i, environment, ns); // Is optimal REQUIRE(result.object == op1); @@ -266,24 +210,14 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); THEN("A new AO should be returned with op2s valuee") { - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); - // Correctness of merge REQUIRE(result.modified); - REQUIRE_FALSE(cast_result->is_top()); - REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE( - read_index(cast_result, i0, environment, ns) == to_expr(val1[0])); - REQUIRE( - read_index(cast_result, i1, environment, ns) == to_expr(val1[1])); - REQUIRE( - read_index(cast_result, i2, environment, ns) == to_expr(val1[2])); + REQUIRE_FALSE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); + for(int i = 0; i != 3; ++i) + EXPECT_INDEX(result.object, i, val1[i], environment, ns); // Is optimal REQUIRE(result.object != op1); @@ -298,21 +232,14 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); THEN("A new constant array AO should be returned set to top ") { - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); - // Correctness of merge REQUIRE(result.modified); - REQUIRE(cast_result->is_top()); - REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE(read_index(cast_result, i0, environment, ns) == nil_exprt()); - REQUIRE(read_index(cast_result, i1, environment, ns) == nil_exprt()); - REQUIRE(read_index(cast_result, i2, environment, ns) == nil_exprt()); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); + for(int i = 0; i != 3; ++i) + EXPECT_INDEX_TOP(result.object, i, environment, ns); // Is optimal REQUIRE(result.object != op1); @@ -327,18 +254,12 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); THEN("The original bottom AO should be returned") { - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); - // Correctness of merge REQUIRE_FALSE(result.modified); - REQUIRE_FALSE(cast_result->is_top()); - REQUIRE(cast_result->is_bottom()); + REQUIRE_FALSE(result.object->is_top()); + REQUIRE(result.object->is_bottom()); // Is optimal REQUIRE(result.object == op1); @@ -354,19 +275,15 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); - THEN("We should get a new AO of the same type but set to top") { // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); + REQUIRE(result.object); // Correctness of merge REQUIRE(result.modified); - REQUIRE(cast_result->is_top()); - REQUIRE_FALSE(cast_result->is_bottom()); + REQUIRE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); // Since it has modified, we definitely shouldn't be reusing the pointer REQUIRE_FALSE(result.object == op1); @@ -382,24 +299,14 @@ SCENARIO( auto result = abstract_objectt::merge(op1, op2, widen_modet::no); - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); THEN("We should get the same constant array AO back") { - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); - // Correctness of merge REQUIRE_FALSE(result.modified); - REQUIRE_FALSE(cast_result->is_top()); - REQUIRE_FALSE(cast_result->is_bottom()); - REQUIRE( - read_index(cast_result, i0, environment, ns) == to_expr(val1[0])); - REQUIRE( - read_index(cast_result, i1, environment, ns) == to_expr(val1[1])); - REQUIRE( - read_index(cast_result, i2, environment, ns) == to_expr(val1[2])); + REQUIRE_FALSE(result.object->is_top()); + REQUIRE_FALSE(result.object->is_bottom()); + for(int i = 0; i != 3; ++i) + EXPECT_INDEX(result.object, i, val1[i], environment, ns); // Is optimal REQUIRE(result.object == op1); @@ -424,13 +331,6 @@ SCENARIO( // Is optimal REQUIRE(result.object == op1); - - // Is type still correct - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); } } WHEN( @@ -451,13 +351,6 @@ SCENARIO( // Is optimal REQUIRE(result.object == op1); - - // Is type still correct - const auto &cast_result = - std::dynamic_pointer_cast( - result.object); - // Though we may become top or bottom, the type should be unchanged - REQUIRE(cast_result); } } WHEN( diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp index 08db37edfc6..b3a4e2c236f 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp @@ -140,7 +140,8 @@ as_interval(const abstract_object_pointert &aop) std::shared_ptr as_value_set(const abstract_object_pointert &aop) { - return std::dynamic_pointer_cast(aop); + return std::dynamic_pointer_cast( + aop->unwrap_context()); } bool set_contains(const std::vector &set, const exprt &val) @@ -272,10 +273,7 @@ void EXPECT( REQUIRE(values.size() == expected_values.size()); for(auto &ev : expected_values) - { - INFO("Expect " + value_string + " to match " + expected_string); REQUIRE(set_contains(values, ev)); - } } void EXPECT( @@ -294,6 +292,60 @@ void EXPECT( } } +void EXPECT_INDEX( + std::shared_ptr &result, + int index, + int expected, + abstract_environmentt &environment, + namespacet &ns) +{ + auto type = signedbv_typet(32); + auto index_expr = index_exprt(nil_exprt(), from_integer(index, type)); + auto expr = result->expression_transform(index_expr, {}, environment, ns) + ->to_constant(); + + auto expected_expr = from_integer(expected, type); + INFO( + "Expect array[" + std::to_string(index) + + "] == " + std::to_string(expected)); + REQUIRE(expr_to_str(expr) == expr_to_str(expected_expr)); +} + +void EXPECT_INDEX( + std::shared_ptr &result, + int index, + std::vector expected, + abstract_environmentt &environment, + namespacet &ns) +{ + auto type = signedbv_typet(32); + auto index_expr = index_exprt(nil_exprt(), from_integer(index, type)); + auto value = + as_value_set(result->expression_transform(index_expr, {}, environment, ns)); + + auto expected_exprs = std::vector{}; + for(int e : expected) + expected_exprs.push_back(from_integer(e, type)); + INFO( + "Expect array[" + std::to_string(index) + + "] == " + exprs_to_str(expected_exprs)); + EXPECT(value, expected_exprs); +} + +void EXPECT_INDEX_TOP( + std::shared_ptr &result, + int index, + abstract_environmentt &environment, + namespacet &ns) +{ + auto type = signedbv_typet(32); + auto index_expr = index_exprt(nil_exprt(), from_integer(index, type)); + auto value = result->expression_transform(index_expr, {}, environment, ns); + + INFO("Expect array[" + std::to_string(index) + "] to be TOP"); + REQUIRE(value->is_top()); +} + void EXPECT_UNMODIFIED( std::shared_ptr &result, bool modified) diff --git a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h index fe0e067fb66..3b5dda14dee 100644 --- a/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h +++ b/unit/analyses/variable-sensitivity/variable_sensitivity_test_helpers.h @@ -84,6 +84,24 @@ void EXPECT( const std::vector &values, const std::vector &expected_values); +void EXPECT_INDEX( + std::shared_ptr &result, + int index, + int expected, + abstract_environmentt &environment, + namespacet &ns); +void EXPECT_INDEX( + std::shared_ptr &result, + int index, + std::vector expected, + abstract_environmentt &environment, + namespacet &ns); +void EXPECT_INDEX_TOP( + std::shared_ptr &result, + int index, + abstract_environmentt &environment, + namespacet &ns); + void EXPECT_TOP(std::shared_ptr result); void EXPECT_TOP(abstract_objectt::combine_result const &result);