From 158bb26e47c4ad15b8071f9b7152a4c6bc7428fe Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 19 Jan 2021 15:26:01 +0000 Subject: [PATCH 01/30] Improve interval_abstract_objectt::expression_transform Reduce number of special cases, and generalise expression evaluation. Special case for ID_plus no longer needed, as a+b+c is still evaluated correctly. Previously incorrectly evaluated expressions such as a*b*c now also evaluated properly. --- .../main.c | 0 .../test.desc | 0 .../main.c | 12 ++ .../test.desc | 11 ++ .../interval_abstract_value.cpp | 106 +++++++----------- 5 files changed, 66 insertions(+), 63 deletions(-) rename regression/goto-analyzer/{variable-sensitivity-interval-values-multiplication => variable-sensitivity-interval-values-multiplication-01}/main.c (100%) rename regression/goto-analyzer/{variable-sensitivity-interval-values-multiplication => variable-sensitivity-interval-values-multiplication-01}/test.desc (100%) create mode 100644 regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/main.c create mode 100644 regression/goto-analyzer/variable-sensitivity-interval-values-multiplication-02/test.desc 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/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index bdd01cf4910..f9bd9fd66ad 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -265,7 +265,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) { @@ -321,23 +320,43 @@ abstract_object_pointert interval_abstract_valuet::expression_transform( if(num_operands == 0) return environment.abstract_object_factory(type, ns, true); - if(expr.id() == ID_plus) + if(expr.id() == ID_if) { - constant_exprt zero = constant_interval_exprt::zero(type); - constant_interval_exprt interval(zero); - INVARIANT(interval.is_zero(), "Starting interval must be zero"); + 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; - for(const auto &iav : interval_operands) + // Check the value of the condition interval + if(condition_interval.is_definitely_false().is_unknown()) { - const constant_interval_exprt &interval_next = iav->interval; - interval = interval.plus(interval_next); + // 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); } - - INVARIANT( - interval.type() == type, - "Type of result interval should match expression type"); - - return environment.abstract_object_factory(type, interval, ns); } else if(num_operands == 1) { @@ -347,8 +366,7 @@ abstract_object_pointert interval_abstract_valuet::expression_transform( { const typecast_exprt &tce = to_typecast_expr(expr); - const constant_interval_exprt &new_interval = - interval.typecast(tce.type()); + const constant_interval_exprt &new_interval = interval.typecast(tce.type()); INVARIANT( new_interval.type() == type, @@ -365,59 +383,21 @@ abstract_object_pointert interval_abstract_valuet::expression_transform( return environment.abstract_object_factory(type, interval_result, ns); } } - else if(num_operands == 2) + else { - const constant_interval_exprt &interval0 = interval_operands[0]->interval; - const constant_interval_exprt &interval1 = interval_operands[1]->interval; + constant_interval_exprt result = interval_operands[0]->interval; - constant_interval_exprt interval = interval0.eval(expr.id(), interval1); + for (size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex) + { + auto &interval_next = interval_operands[opIndex]->interval; + result = result.eval(expr.id(), interval_next); + } INVARIANT( - interval.type() == type, + result.type() == 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(type, result, ns); } return environment.abstract_object_factory(type, ns, true); From 2d925bc3424b9449dd1dde6ea6765671109b86cf Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 19 Jan 2021 16:56:42 +0000 Subject: [PATCH 02/30] value_set_abstract_objectt::set_value must mark not top Without this all operations return top, which is unhelpful. With this change, simple arithmetic starts to work, unary operations, etc. Still more to for multi-value sets. Note - change in behaviour for function pointers. I believe previous behaviour was an error. --- .../main.c | 0 .../test.desc | 3 +- .../main.c | 34 +++++++++++++++++++ .../test.desc | 8 +++++ .../main.c | 5 +++ .../test.desc | 8 +++++ .../main.c | 5 +++ .../test.desc | 8 +++++ .../value_set_abstract_object.h | 1 + 9 files changed, 70 insertions(+), 2 deletions(-) rename regression/goto-analyzer/{value-set-function-pointers-incremented => value-set-function-pointers-incremented-01}/main.c (100%) rename regression/goto-analyzer/{value-set-function-pointers-incremented => value-set-function-pointers-incremented-01}/test.desc (71%) create mode 100644 regression/goto-analyzer/value-set-function-pointers-incremented-02/main.c create mode 100644 regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc create mode 100644 regression/goto-analyzer/variable-sensitivity-value-set-addition-01/main.c create mode 100644 regression/goto-analyzer/variable-sensitivity-value-set-addition-01/test.desc create mode 100644 regression/goto-analyzer/variable-sensitivity-value-set-unary-minus/main.c create mode 100644 regression/goto-analyzer/variable-sensitivity-value-set-unary-minus/test.desc 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..b6a88349701 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..c0abcabb59b --- /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..6780945df81 --- /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/variable-sensitivity-value-set-addition-01/main.c b/regression/goto-analyzer/variable-sensitivity-value-set-addition-01/main.c new file mode 100644 index 00000000000..9bbe413665d --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-value-set-addition-01/main.c @@ -0,0 +1,5 @@ +int main(int argc, char argv[]) { + int p = 1; + + int q = p + 2; +} diff --git a/regression/goto-analyzer/variable-sensitivity-value-set-addition-01/test.desc b/regression/goto-analyzer/variable-sensitivity-value-set-addition-01/test.desc new file mode 100644 index 00000000000..998112e048f --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-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/variable-sensitivity-value-set-unary-minus/main.c b/regression/goto-analyzer/variable-sensitivity-value-set-unary-minus/main.c new file mode 100644 index 00000000000..7d606d5be14 --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-value-set-unary-minus/main.c @@ -0,0 +1,5 @@ +int main(int argc, char argv[]) { + int p = 1; + + int q = -p; +} diff --git a/regression/goto-analyzer/variable-sensitivity-value-set-unary-minus/test.desc b/regression/goto-analyzer/variable-sensitivity-value-set-unary-minus/test.desc new file mode 100644 index 00000000000..8126445625d --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-value-set-unary-minus/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/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 75ce1289fda..0997c6f944e 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -67,6 +67,7 @@ class value_set_abstract_objectt : public abstract_value_objectt void 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(); From e524b04d1d5dac42d910d1ccc5df3337dc9fd212 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 20 Jan 2021 09:29:20 +0000 Subject: [PATCH 03/30] More value-set behaviour tests Covering unary operations and addition with multi-valued sets --- .../main.c | 0 .../test.desc | 0 .../goto-analyzer/value-set-addition-02/main.c | 14 ++++++++++++++ .../goto-analyzer/value-set-addition-02/test.desc | 9 +++++++++ .../value-set-array-constant-access/main.c | 8 ++++++++ .../value-set-array-constant-access/test.desc | 7 +++++++ .../main.c | 0 .../test.desc | 0 .../goto-analyzer/value-set-unary-not-01/main.c | 5 +++++ .../goto-analyzer/value-set-unary-not-01/test.desc | 8 ++++++++ 10 files changed, 51 insertions(+) rename regression/goto-analyzer/{variable-sensitivity-value-set-addition-01 => value-set-addition-01}/main.c (100%) rename regression/goto-analyzer/{variable-sensitivity-value-set-addition-01 => value-set-addition-01}/test.desc (100%) create mode 100644 regression/goto-analyzer/value-set-addition-02/main.c create mode 100644 regression/goto-analyzer/value-set-addition-02/test.desc create mode 100644 regression/goto-analyzer/value-set-array-constant-access/main.c create mode 100644 regression/goto-analyzer/value-set-array-constant-access/test.desc rename regression/goto-analyzer/{variable-sensitivity-value-set-unary-minus => value-set-unary-minus-01}/main.c (100%) rename regression/goto-analyzer/{variable-sensitivity-value-set-unary-minus => value-set-unary-minus-01}/test.desc (100%) create mode 100644 regression/goto-analyzer/value-set-unary-not-01/main.c create mode 100644 regression/goto-analyzer/value-set-unary-not-01/test.desc diff --git a/regression/goto-analyzer/variable-sensitivity-value-set-addition-01/main.c b/regression/goto-analyzer/value-set-addition-01/main.c similarity index 100% rename from regression/goto-analyzer/variable-sensitivity-value-set-addition-01/main.c rename to regression/goto-analyzer/value-set-addition-01/main.c diff --git a/regression/goto-analyzer/variable-sensitivity-value-set-addition-01/test.desc b/regression/goto-analyzer/value-set-addition-01/test.desc similarity index 100% rename from regression/goto-analyzer/variable-sensitivity-value-set-addition-01/test.desc rename to regression/goto-analyzer/value-set-addition-01/test.desc 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..c65ee461c45 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-02/main.c @@ -0,0 +1,14 @@ +int unknown(); + +int main(int argc, char argv[]) { + int p = 1; + int q = 2; + + if (unknown()) + p = 1; + else + p = 2; + + + 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..4c53f7604f8 --- /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: 1, :value-set-end +main::1::q .* value-set-begin: 2, :value-set-end +main::1::t .* value-set-begin: TOP, :value-set-end +-- diff --git a/regression/goto-analyzer/value-set-array-constant-access/main.c b/regression/goto-analyzer/value-set-array-constant-access/main.c new file mode 100644 index 00000000000..41aa58a0e10 --- /dev/null +++ b/regression/goto-analyzer/value-set-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/value-set-array-constant-access/test.desc b/regression/goto-analyzer/value-set-array-constant-access/test.desc new file mode 100644 index 00000000000..0ad483152ed --- /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/variable-sensitivity-value-set-unary-minus/main.c b/regression/goto-analyzer/value-set-unary-minus-01/main.c similarity index 100% rename from regression/goto-analyzer/variable-sensitivity-value-set-unary-minus/main.c rename to regression/goto-analyzer/value-set-unary-minus-01/main.c diff --git a/regression/goto-analyzer/variable-sensitivity-value-set-unary-minus/test.desc b/regression/goto-analyzer/value-set-unary-minus-01/test.desc similarity index 100% rename from regression/goto-analyzer/variable-sensitivity-value-set-unary-minus/test.desc rename to regression/goto-analyzer/value-set-unary-minus-01/test.desc 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..448c8eac5ea --- /dev/null +++ b/regression/goto-analyzer/value-set-unary-not-01/main.c @@ -0,0 +1,5 @@ +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..e6672bee29c --- /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 +-- From ed0b73bc80e1e8b393ee5011c0afadd3e4c888ba Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 20 Jan 2021 12:52:46 +0000 Subject: [PATCH 04/30] value_set_abstract_objectt correctly evaluates n-ary expressions expression_transform correctly creates all combinations of operands, but passed the unmodified expression down for further evaluation. If the expression was something like 2 + p then at the next stage down, we'd look up symbol 'p' and be handed back a value set. The evaluated would then try to convert that value set to a constant which would, naturally, fail. Consequently, the expression would evaluate to top. Now, we rewrite the expression in terms of the evaluated operands. If expression was 2 + p, and p was the set { 2, 3 } the expression is rewritten first as 2 + 2, then as 2 + 3, which we can gather up into our result of { 4, 5 }. The various regression tests in this commit exercise various combinations of constants and value-sets, value-sets of different size, and so on. All the tests use addition, but the operator is immaterial. --- .../goto-analyzer/value-set-addition-02/main.c | 12 ++---------- .../value-set-addition-02/test.desc | 6 +++--- .../goto-analyzer/value-set-addition-03/main.c | 10 ++++++++++ .../value-set-addition-03/test.desc | 7 +++++++ .../goto-analyzer/value-set-addition-04/main.c | 14 ++++++++++++++ .../value-set-addition-04/test.desc | 10 ++++++++++ .../goto-analyzer/value-set-addition-05/main.c | 16 ++++++++++++++++ .../value-set-addition-05/test.desc | 9 +++++++++ .../goto-analyzer/value-set-addition-06/main.c | 17 +++++++++++++++++ .../value-set-addition-06/test.desc | 9 +++++++++ .../goto-analyzer/value-set-addition-07/main.c | 13 +++++++++++++ .../value-set-addition-07/test.desc | 10 ++++++++++ .../goto-analyzer/value-set-addition-08/main.c | 13 +++++++++++++ .../value-set-addition-08/test.desc | 10 ++++++++++ .../value_set_abstract_object.cpp | 6 +++++- 15 files changed, 148 insertions(+), 14 deletions(-) create mode 100644 regression/goto-analyzer/value-set-addition-03/main.c create mode 100644 regression/goto-analyzer/value-set-addition-03/test.desc create mode 100644 regression/goto-analyzer/value-set-addition-04/main.c create mode 100644 regression/goto-analyzer/value-set-addition-04/test.desc create mode 100644 regression/goto-analyzer/value-set-addition-05/main.c create mode 100644 regression/goto-analyzer/value-set-addition-05/test.desc create mode 100644 regression/goto-analyzer/value-set-addition-06/main.c create mode 100644 regression/goto-analyzer/value-set-addition-06/test.desc create mode 100644 regression/goto-analyzer/value-set-addition-07/main.c create mode 100644 regression/goto-analyzer/value-set-addition-07/test.desc create mode 100644 regression/goto-analyzer/value-set-addition-08/main.c create mode 100644 regression/goto-analyzer/value-set-addition-08/test.desc diff --git a/regression/goto-analyzer/value-set-addition-02/main.c b/regression/goto-analyzer/value-set-addition-02/main.c index c65ee461c45..6d625ec38d7 100644 --- a/regression/goto-analyzer/value-set-addition-02/main.c +++ b/regression/goto-analyzer/value-set-addition-02/main.c @@ -1,14 +1,6 @@ -int unknown(); - int main(int argc, char argv[]) { - int p = 1; - int q = 2; - - if (unknown()) - p = 1; - else - p = 2; - + 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 index 4c53f7604f8..941b4db764a 100644 --- a/regression/goto-analyzer/value-set-addition-02/test.desc +++ b/regression/goto-analyzer/value-set-addition-02/test.desc @@ -3,7 +3,7 @@ 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: 2, :value-set-end -main::1::t .* value-set-begin: TOP, :value-set-end +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..f90e4549e4e --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-03/main.c @@ -0,0 +1,10 @@ +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..18ba0dfa400 --- /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..c2d032bfc84 --- /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..78d6f9dbd69 --- /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..473bf471d88 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-05/main.c @@ -0,0 +1,16 @@ +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..316458ead9a --- /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, 12, 8, 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..ee1dc9d0d06 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-06/main.c @@ -0,0 +1,17 @@ +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..301d57be9bf --- /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, 32, 28, 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..74fadd3c2c6 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-07/main.c @@ -0,0 +1,13 @@ +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..246c397e30f --- /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: 37, 32, 42, 28, 38, 33, 27, 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..c86393a0f15 --- /dev/null +++ b/regression/goto-analyzer/value-set-addition-08/main.c @@ -0,0 +1,13 @@ +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..3afd1a0b185 --- /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: 3, 2, 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: 28, 27, 33, 29, 32, 34, :value-set-end +-- diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 061a1bc3198..24f0a38ac49 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -148,8 +148,12 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform( collective_operands, [&resulting_objects, this, &expr, &environment, &ns]( 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)); resulting_objects.insert( - (*values.begin())->expression_transform(expr, ops, environment, ns)); + (*values.begin())->expression_transform(rewritten_expr, ops, environment, ns)); }); return resolve_new_values(resulting_objects); From 59cef522b45aef8ab6898c33ccb8a9f5f93b7034 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 20 Jan 2021 14:58:59 +0000 Subject: [PATCH 05/30] Made resolve_new_values private rather than protected --- .../variable-sensitivity/value_set_abstract_object.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 0997c6f944e..39ae9149157 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -116,6 +116,10 @@ class value_set_abstract_objectt : public abstract_value_objectt protected: CLONE + /// \copydoc abstract_object::merge + abstract_object_pointert merge(abstract_object_pointert other) const override; + +private: /// 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 @@ -124,10 +128,6 @@ class value_set_abstract_objectt : public abstract_value_objectt abstract_object_pointert resolve_new_values(const abstract_object_sett &new_values) const; - /// \copydoc abstract_object::merge - abstract_object_pointert merge(abstract_object_pointert other) const override; - -private: // data abstract_typet my_type; abstract_object_sett values; From b20595e4fcd86e6d53c97dd821a451436801486d Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 20 Jan 2021 14:59:27 +0000 Subject: [PATCH 06/30] Removed get_as_interval() - not used --- .../variable-sensitivity/value_set_abstract_object.h | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 39ae9149157..1dae2684460 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -103,13 +103,6 @@ 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; From 9e90a7cafa98a2b057ef99e62c2be0cf85690c23 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 20 Jan 2021 15:17:39 +0000 Subject: [PATCH 07/30] Moved set_values body into cpp file --- .../variable-sensitivity/value_set_abstract_object.cpp | 9 +++++++++ .../variable-sensitivity/value_set_abstract_object.h | 9 +-------- 2 files changed, 10 insertions(+), 8 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 24f0a38ac49..9bd7693bce8 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -285,6 +285,15 @@ value_set_abstract_objectt::get_type(const abstract_object_pointert &other) return abstract_typet::UNSUPPORTED; } +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(); +} + abstract_object_pointert value_set_abstract_objectt::maybe_extract_single_value( const abstract_object_pointert &maybe_singleton) { diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 1dae2684460..ccce49a627b 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -64,14 +64,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()); - set_not_top(); - 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 From be437f9a2bc6c08df3f24195e95b1ec29e1452af Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 20 Jan 2021 15:32:18 +0000 Subject: [PATCH 08/30] Private static member functions moved to free functions in the cpp --- .../value_set_abstract_object.cpp | 123 +++++++++++++----- .../value_set_abstract_object.h | 41 ------ 2 files changed, 87 insertions(+), 77 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 9bd7693bce8..700b8cc06fa 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -52,6 +52,32 @@ index_range_ptrt make_value_set_index_range( 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); + +/// 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); + + value_set_abstract_objectt::value_set_abstract_objectt(const typet &type) : abstract_value_objectt(type), my_type(type_to_abstract_type(type)) { @@ -268,9 +294,45 @@ 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(); +} + +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"; + } +} + 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)); @@ -285,17 +347,31 @@ value_set_abstract_objectt::get_type(const abstract_object_pointert &other) return abstract_typet::UNSUPPORTED; } -void value_set_abstract_objectt::set_values(const abstract_object_sett &other_values) +value_set_abstract_objectt::abstract_typet +type_to_abstract_type(const typet &type) { - PRECONDITION(!other_values.empty()); - set_not_top(); - my_type = get_type(*other_values.begin()); - values = other_values; - verify(); + using abstract_typet = value_set_abstract_objectt::abstract_typet; + + 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; + } } -abstract_object_pointert value_set_abstract_objectt::maybe_extract_single_value( - const abstract_object_pointert &maybe_singleton) +abstract_object_pointert +maybe_extract_single_value(const abstract_object_pointert &maybe_singleton) { auto const &value_as_set = std::dynamic_pointer_cast( @@ -312,36 +388,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 ccce49a627b..f8315c47756 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -163,47 +163,6 @@ class value_set_abstract_objectt : public abstract_value_objectt 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 From 6595b3bdf18156b2bc5fdde73be6729147a23bf8 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 20 Jan 2021 15:40:49 +0000 Subject: [PATCH 09/30] Private template member functions moved to free template in cpp --- .../value_set_abstract_object.cpp | 36 ++++++++++++++++++ .../value_set_abstract_object.h | 37 ------------------- 2 files changed, 36 insertions(+), 37 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 700b8cc06fa..dd3b1aea851 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -77,6 +77,42 @@ maybe_extract_single_value(const abstract_object_pointert &maybe_singleton); 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)) diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index f8315c47756..257e822470b 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -126,43 +126,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); - } }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VALUE_SET_ABSTRACT_OBJECT_H From 42028f4498a27cc7c03647a69419995d4d9ccf98 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 20 Jan 2021 16:39:20 +0000 Subject: [PATCH 10/30] Pull out a few clarifying functions in value_set_abstract_objectt --- .../value-set-addition-07/test.desc | 2 +- .../value_set_abstract_object.cpp | 99 ++++++++++++------- 2 files changed, 67 insertions(+), 34 deletions(-) diff --git a/regression/goto-analyzer/value-set-addition-07/test.desc b/regression/goto-analyzer/value-set-addition-07/test.desc index 246c397e30f..19904c37066 100644 --- a/regression/goto-analyzer/value-set-addition-07/test.desc +++ b/regression/goto-analyzer/value-set-addition-07/test.desc @@ -6,5 +6,5 @@ main.c 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: 37, 32, 42, 28, 38, 33, 27, 43, :value-set-end +main::1::t .* value-set-begin: 37, 32, 33, 42, 28, 38, 27, 43, :value-set-end -- diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index dd3b1aea851..15b95953ae9 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -16,10 +16,11 @@ #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()) { @@ -47,7 +48,7 @@ class value_set_index_ranget : public index_ranget }; index_range_ptrt make_value_set_index_range( - const value_set_abstract_objectt::abstract_object_sett &vals) + const abstract_object_sett &vals) { return std::make_shared(vals); } @@ -64,6 +65,16 @@ get_type(const abstract_object_pointert &other); 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 @@ -192,30 +203,21 @@ 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); 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 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)); + + auto rewritten_expr = rewrite_expression(expr, ops); resulting_objects.insert( - (*values.begin())->expression_transform(rewritten_expr, ops, environment, ns)); + dispatcher->expression_transform(rewritten_expr, ops, environment, ns)); }); return resolve_new_values(resulting_objects); @@ -246,12 +248,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( @@ -293,8 +290,8 @@ value_set_abstract_objectt::merge(abstract_object_pointert other) const cast_other->get_values().begin(), cast_other->get_values().end()); return resolve_new_values(union_values); } - else - return abstract_objectt::merge(other); + + return abstract_objectt::merge(other); } abstract_object_pointert value_set_abstract_objectt::to_interval( @@ -389,21 +386,57 @@ 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; - } - else if( + + 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()); } - else + + return unwrapped; +} + +abstract_object_sett +unwrap_and_extract_values(const abstract_object_sett &values) +{ + abstract_object_sett unwrapped_values; + for(auto const &value : values) { - return abstract_typet::UNSUPPORTED; + unwrapped_values.insert( + maybe_extract_single_value(maybe_unwrap_context(value))); } + + return unwrapped_values; } abstract_object_pointert From 9a8f37031e3067857640bea18253c05c33628f61 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 20 Jan 2021 16:50:31 +0000 Subject: [PATCH 11/30] Array access with value-sets works! Splendid side-effect of the expression_transform work :) --- .../main.c | 0 .../test.desc | 0 .../main.c | 0 .../test.desc | 0 .../main.c | 33 +++++++++++++++++++ .../test.desc | 9 +++++ 6 files changed, 42 insertions(+) rename regression/goto-analyzer/{variable-sensitivity-interval-values-array-constant-access => variable-sensitivity-array-constant-access}/main.c (100%) rename regression/goto-analyzer/{variable-sensitivity-interval-values-array-constant-access => variable-sensitivity-array-constant-access}/test.desc (100%) rename regression/goto-analyzer/{variable-sensitivity-interval-values-array-interval-access => variable-sensitivity-array-interval-access}/main.c (100%) rename regression/goto-analyzer/{variable-sensitivity-interval-values-array-interval-access => variable-sensitivity-array-interval-access}/test.desc (100%) create mode 100644 regression/goto-analyzer/variable-sensitivity-array-value-set-access/main.c create mode 100644 regression/goto-analyzer/variable-sensitivity-array-value-set-access/test.desc diff --git a/regression/goto-analyzer/variable-sensitivity-interval-values-array-constant-access/main.c b/regression/goto-analyzer/variable-sensitivity-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/variable-sensitivity-array-constant-access/main.c 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/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..f5e0812ef10 --- /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: 4, 1, :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 From 7b7308b97083cae7f004f0f391691c60b9a80547 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 20 Jan 2021 17:02:06 +0000 Subject: [PATCH 12/30] Array read with multi-value value-set index and multi-value value-set array element --- .../main.c | 11 +++++++++++ .../test.desc | 7 +++++++ 2 files changed, 18 insertions(+) create mode 100644 regression/goto-analyzer/variable-sensitivity-array-value-set-access-02/main.c create mode 100644 regression/goto-analyzer/variable-sensitivity-array-value-set-access-02/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..464db0e214f --- /dev/null +++ b/regression/goto-analyzer/variable-sensitivity-array-value-set-access-02/main.c @@ -0,0 +1,11 @@ +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..e49d86dcc6a --- /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: 3, 2, 1, :value-set-end +main::1::p \(\) -> value-set-begin: 0, 1, :value-set-end From 58b39127388e9b3913c8046a74c6b4ca5e0b1fad Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 26 Jan 2021 14:22:36 +0000 Subject: [PATCH 13/30] Factor out interval_abstract_valuet::evaluate_conditional --- .../interval_abstract_value.cpp | 71 +++++++++---------- .../interval_abstract_value.h | 6 ++ 2 files changed, 39 insertions(+), 38 deletions(-) diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index f9bd9fd66ad..1a847a5d811 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -321,44 +321,9 @@ abstract_object_pointert interval_abstract_valuet::expression_transform( return environment.abstract_object_factory(type, ns, true); 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; + return evaluate_conditional(type, interval_operands, environment, ns); - // 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); - } - } - else if(num_operands == 1) + if(num_operands == 1) { const constant_interval_exprt &interval = interval_operands[0]->interval; @@ -396,13 +361,43 @@ abstract_object_pointert interval_abstract_valuet::expression_transform( INVARIANT( result.type() == type, "Type of result interval should match expression type"); - return environment.abstract_object_factory(type, result, ns); } return environment.abstract_object_factory(type, ns, true); } +abstract_object_pointert interval_abstract_valuet::evaluate_conditional( + const typet &type, + std::vector> interval_operands, + const abstract_environmentt &env, + const namespacet &ns) const +{ + auto const &condition_interval = interval_operands[0]->interval; + auto const &true_interval = interval_operands[1]->interval; + auto const &false_interval = interval_operands[2]->interval; + + auto condition_result = condition_interval.is_definitely_true(); + + 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( + 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); + } + + 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); +} + void interval_abstract_valuet::output( std::ostream &out, const ai_baset &ai, diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 8b9bcdc285a..4afdeab0661 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -85,6 +85,12 @@ class interval_abstract_valuet : public abstract_value_objectt meet(const abstract_object_pointert &other) const override; private: + abstract_object_pointert evaluate_conditional( + const typet &type, + std::vector> interval_operands, + const abstract_environmentt &environment, + const namespacet &ns) const; + abstract_object_pointert merge_intervals(interval_abstract_value_pointert other) const; abstract_object_pointert From 837df226b46d87b27e934c27f2b9bc84f9cadff7 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 26 Jan 2021 14:45:56 +0000 Subject: [PATCH 14/30] Value set ternary operator evaluation --- .../ternary-operator-constants/main.c | 19 +++++++++++ .../ternary-operator-constants/test.desc | 12 +++++++ .../ternary-operator-intervals/main.c | 19 +++++++++++ .../ternary-operator-intervals/test.desc | 12 +++++++ .../ternary-operator-value-sets/main.c | 19 +++++++++++ .../ternary-operator-value-sets/test.desc | 12 +++++++ .../value_set_abstract_object.cpp | 34 +++++++++++++++++++ .../value_set_abstract_object.h | 6 ++++ 8 files changed, 133 insertions(+) create mode 100644 regression/goto-analyzer/ternary-operator-constants/main.c create mode 100644 regression/goto-analyzer/ternary-operator-constants/test.desc create mode 100644 regression/goto-analyzer/ternary-operator-intervals/main.c create mode 100644 regression/goto-analyzer/ternary-operator-intervals/test.desc create mode 100644 regression/goto-analyzer/ternary-operator-value-sets/main.c create mode 100644 regression/goto-analyzer/ternary-operator-value-sets/test.desc diff --git a/regression/goto-analyzer/ternary-operator-constants/main.c b/regression/goto-analyzer/ternary-operator-constants/main.c new file mode 100644 index 00000000000..c76542789fd --- /dev/null +++ b/regression/goto-analyzer/ternary-operator-constants/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-constants/test.desc b/regression/goto-analyzer/ternary-operator-constants/test.desc new file mode 100644 index 00000000000..e1066c6b418 --- /dev/null +++ b/regression/goto-analyzer/ternary-operator-constants/test.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-intervals/main.c b/regression/goto-analyzer/ternary-operator-intervals/main.c new file mode 100644 index 00000000000..c76542789fd --- /dev/null +++ b/regression/goto-analyzer/ternary-operator-intervals/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-intervals/test.desc b/regression/goto-analyzer/ternary-operator-intervals/test.desc new file mode 100644 index 00000000000..12fbe2f8c13 --- /dev/null +++ b/regression/goto-analyzer/ternary-operator-intervals/test.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-value-sets/main.c b/regression/goto-analyzer/ternary-operator-value-sets/main.c new file mode 100644 index 00000000000..c76542789fd --- /dev/null +++ b/regression/goto-analyzer/ternary-operator-value-sets/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-value-sets/test.desc b/regression/goto-analyzer/ternary-operator-value-sets/test.desc new file mode 100644 index 00000000000..30bc0e556fa --- /dev/null +++ b/regression/goto-analyzer/ternary-operator-value-sets/test.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: FALSE, TRUE, :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/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 15b95953ae9..2c944dd6ff6 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -207,6 +207,9 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform( 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(); @@ -223,6 +226,37 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform( return resolve_new_values(resulting_objects); } +abstract_object_pointert value_set_abstract_objectt::evaluate_conditional( + const typet &type, + 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(); + } + + if (all_true) + return resolve_new_values(true_result); + if (all_false) + return resolve_new_values(false_result); + + // indeterminate + abstract_object_sett resulting_objects; + resulting_objects.insert(true_result.begin(), true_result.end()); + resulting_objects.insert(false_result.begin(), false_result.end()); + return resolve_new_values(resulting_objects); +} + abstract_object_pointert value_set_abstract_objectt::write( abstract_environmentt &environment, const namespacet &ns, diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 257e822470b..48b322ca04d 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -106,6 +106,12 @@ class value_set_abstract_objectt : public abstract_value_objectt abstract_object_pointert merge(abstract_object_pointert other) const override; private: + abstract_object_pointert evaluate_conditional( + const typet &type, + 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 From c2a8fd0420aec67d1c791cb2f5748350883eda67 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 26 Jan 2021 17:00:51 +0000 Subject: [PATCH 15/30] Make value_set_abstract_objectt compatible with context tracking Do this by ensuring new object we return are created though the factory, rather than instantiated directly. Several regression tests needed updating as a consequence of this change, generally tweaking the regex to allow the context info in place of a hard line end. --- .../value-set-addition-07/test.desc | 2 +- .../value-set-addition-08/test.desc | 2 +- .../test.desc | 8 ++-- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 20 ++++----- .../test.desc | 12 +++--- .../value-set-simple/test_show.desc | 6 +-- .../value-set-structs/test_show.desc | 4 +- .../value_set_abstract_object.cpp | 42 +++++++++++++++---- .../value_set_abstract_object.h | 17 +++++++- .../variable_sensitivity_configuration.cpp | 4 +- 12 files changed, 79 insertions(+), 42 deletions(-) diff --git a/regression/goto-analyzer/value-set-addition-07/test.desc b/regression/goto-analyzer/value-set-addition-07/test.desc index 19904c37066..ce1cf302bbf 100644 --- a/regression/goto-analyzer/value-set-addition-07/test.desc +++ b/regression/goto-analyzer/value-set-addition-07/test.desc @@ -6,5 +6,5 @@ main.c 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: 37, 32, 33, 42, 28, 38, 27, 43, :value-set-end +main::1::t .* value-set-begin: 37, 32, 42, 28, 38, 27, 43, 33, :value-set-end -- diff --git a/regression/goto-analyzer/value-set-addition-08/test.desc b/regression/goto-analyzer/value-set-addition-08/test.desc index 3afd1a0b185..2e759f938bf 100644 --- a/regression/goto-analyzer/value-set-addition-08/test.desc +++ b/regression/goto-analyzer/value-set-addition-08/test.desc @@ -6,5 +6,5 @@ main.c main::1::p .* value-set-begin: 3, 2, 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: 28, 27, 33, 29, 32, 34, :value-set-end +main::1::t .* value-set-begin: 28, 27, 32, 34, 33, 29, :value-set-end -- 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..a6130212eda 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 ->\([fg]\), ptr ->\([fg]\), :value-set-end +^main::1::fun_array3 \(\) -> \{\[0\] = value-set-begin: ptr ->\([fg]\), ptr ->\([fg]\), :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-01/test.desc b/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc index b6a88349701..33fc025930f 100644 --- a/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc @@ -2,7 +2,7 @@ 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 \(\) -> value-set-begin: TOP, :value-set-end$ +^main::1::fun_incremented_show \(\) -> value-set-begin: TOP, :value-set-end ^EXIT=0$ ^SIGNAL=0$ -- 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 index 6780945df81..45a40243fd3 100644 --- a/regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc @@ -2,7 +2,7 @@ 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$ +^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..f45ed80d2b8 100644 --- a/regression/goto-analyzer/value-set-function-pointers-simple/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-simple/test.desc @@ -6,20 +6,20 @@ 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: (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 ^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 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..0dde4f66c88 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 ->\([fg]\), ptr ->\([fg]\), :value-set-end +^main::1::s2 \(\) -> \{\.fptr=value-set-begin: ptr ->\([fg]\), ptr ->\([fg]\), :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..c8795266c77 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: [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 ^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..0942a930690 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: [12]\.0, [12]\.0, :value-set-end @ \[16\], \.str=\{\[0\] = value-set-begin: '[xy]', '[xy]', :value-set-end @ \[16\]\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 @ \[49\], \.str=\{\[0\] = value-set-begin: '[xyz]', '[xyz]', '[xyz]', :value-set-end @ \[49\]\n\[1\] = value-set-begin: '\\n', :value-set-end @ \[49\]\n} @ \[49\]} @ \[49\] ^EXIT=0$ ^SIGNAL=0$ -- diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 2c944dd6ff6..7a8cc0a53f2 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -223,7 +223,7 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform( dispatcher->expression_transform(rewritten_expr, ops, environment, ns)); }); - return resolve_new_values(resulting_objects); + return resolve_new_values(resulting_objects, environment, ns); } abstract_object_pointert value_set_abstract_objectt::evaluate_conditional( @@ -246,15 +246,15 @@ abstract_object_pointert value_set_abstract_objectt::evaluate_conditional( } if (all_true) - return resolve_new_values(true_result); + return resolve_new_values(true_result, env, ns); if (all_false) - return resolve_new_values(false_result); + return resolve_new_values(false_result, env, ns); // indeterminate abstract_object_sett resulting_objects; resulting_objects.insert(true_result.begin(), true_result.end()); resulting_objects.insert(false_result.begin(), false_result.end()); - return resolve_new_values(resulting_objects); + return resolve_new_values(resulting_objects, env, ns); } abstract_object_pointert value_set_abstract_objectt::write( @@ -271,11 +271,38 @@ 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, ns); } abstract_object_pointert value_set_abstract_objectt::resolve_new_values( + const abstract_object_sett &new_values, + const abstract_environmentt &environment, + const namespacet &ns) const +{ + auto result = environment.abstract_object_factory(type(), ns, true); + auto unwrapped = maybe_unwrap_context(result); + const auto const_value_set_ptr = + std::dynamic_pointer_cast(unwrapped); + const auto value_set_ptr = + std::const_pointer_cast(const_value_set_ptr); + resolve_values(new_values, value_set_ptr); + return result; +} + +abstract_object_pointert +value_set_abstract_objectt::resolve_values( const abstract_object_sett &new_values) const +{ + const auto &result = + std::dynamic_pointer_cast(mutable_clone()); + + return resolve_values(new_values, result); +} + +abstract_object_pointert +value_set_abstract_objectt::resolve_values( + const abstract_object_sett &new_values, + const value_set_abstract_object_ptrt &result) const { PRECONDITION(!new_values.empty()); @@ -296,9 +323,6 @@ abstract_object_pointert value_set_abstract_objectt::resolve_new_values( return (*unwrapped_values.begin()); } - const auto &result = - std::dynamic_pointer_cast(mutable_clone()); - if( unwrapped_values.size() > max_value_set_size || new_type == abstract_typet::UNSUPPORTED) @@ -322,7 +346,7 @@ 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); } return abstract_objectt::merge(other); diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 48b322ca04d..ca74963dff1 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< + value_set_abstract_objectt>; + using abstract_object_sett = std::unordered_set< abstract_object_pointert, abstract_hashert, @@ -118,7 +121,19 @@ class value_set_abstract_objectt : public abstract_value_objectt /// \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; + resolve_new_values( + const abstract_object_sett &new_values, + const abstract_environmentt &environment, + const namespacet &ns) const; + + abstract_object_pointert + resolve_values( + const abstract_object_sett &new_values) const; + + abstract_object_pointert + resolve_values( + const abstract_object_sett &new_values, + const value_set_abstract_object_ptrt &result) const; // data abstract_typet my_type; diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp index 6914691afe0..492aa302dde 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp @@ -41,9 +41,7 @@ vsd_configt vsd_configt::from_options(const optionst &options) // 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); + 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 = From e80ee3b25610931b47cf692fdf907590be4d39f8 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 27 Jan 2021 11:24:55 +0000 Subject: [PATCH 16/30] Pass operands vector by ref into value_set evaluate_conditional --- .../value_set_abstract_object.cpp | 15 ++++++--------- .../value_set_abstract_object.h | 2 +- 2 files changed, 7 insertions(+), 10 deletions(-) diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 7a8cc0a53f2..f0bd68c123b 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -228,7 +228,7 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform( abstract_object_pointert value_set_abstract_objectt::evaluate_conditional( const typet &type, - std::vector operands, + const std::vector &operands, const abstract_environmentt &env, const namespacet &ns) const { @@ -244,16 +244,13 @@ abstract_object_pointert value_set_abstract_objectt::evaluate_conditional( all_true = all_true && expr.is_true(); all_false = all_false && expr.is_false(); } + auto indeterminate = !all_true && !all_false; - if (all_true) - return resolve_new_values(true_result, env, ns); - if (all_false) - return resolve_new_values(false_result, env, ns); - - // indeterminate abstract_object_sett resulting_objects; - resulting_objects.insert(true_result.begin(), true_result.end()); - resulting_objects.insert(false_result.begin(), false_result.end()); + 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, ns); } diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index ca74963dff1..7be52a82430 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -111,7 +111,7 @@ class value_set_abstract_objectt : public abstract_value_objectt private: abstract_object_pointert evaluate_conditional( const typet &type, - std::vector operands, + const std::vector &operands, const abstract_environmentt &env, const namespacet &ns) const; From 7f8e7baf936b0e0caee67366b1d4d9357184f106 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 27 Jan 2021 15:38:21 +0000 Subject: [PATCH 17/30] Reworked object creation in variable_sensitivity_object_factoryt Reduce duplication, separated object create from the context object that may wrap it. --- .../variable_sensitivity_object_factory.cpp | 77 +++++++++---------- 1 file changed, 37 insertions(+), 40 deletions(-) diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp index 6cfe844e1cc..86759309d3d 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp @@ -9,8 +9,18 @@ #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 +29,27 @@ 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 abstract_object_pointert( + new abstract_object_classt { type, top, bottom }); + + PRECONDITION(type == ns.follow(e.type())); + return abstract_object_pointert( + new abstract_object_classt { 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< + data_dependency_contextt>(abstract_object); + + if(configuration.context_tracking.last_write_context) + return create_context_abstract_object< + write_location_contextt>(abstract_object); + + return abstract_object; } /// Function: variable_sensitivity_object_factoryt::initialize_abstract_object @@ -62,28 +77,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 From 37c32e3cf9bc066d0aaf1743e605ba7cd65cf5ab Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 27 Jan 2021 16:01:55 +0000 Subject: [PATCH 18/30] Ensure returned value_set objects have correct context I'm not super thrilled about how I've done this, because ideally all object creation should go through the object factory. However, in this particular case a large value set could be converted to an interval. If we hand off to the factory it'll just create another value-set, so we need to explicitly create the interval. However, when we do that we don't have the context wrapper (write location or data dependency). Consequently, I've added variable_sensitivity_object_factoryt::wrap_with_context and exposed it through abstract_environment so we can add the appropriate context wrapper should we need it. --- .../abstract_environment.cpp | 6 ++++ .../abstract_environment.h | 13 ++++++++ .../value_set_abstract_object.cpp | 33 +++++-------------- .../value_set_abstract_object.h | 8 +---- .../variable_sensitivity_object_factory.cpp | 7 ++++ .../variable_sensitivity_object_factory.h | 3 ++ 6 files changed, 39 insertions(+), 31 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index 299b0e470b4..b023751c63a 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -279,6 +279,12 @@ abstract_object_pointert abstract_environmentt::abstract_object_factory( type, top, bottom, 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) { // for each entry in the incoming environment we need to either add it diff --git a/src/analyses/variable-sensitivity/abstract_environment.h b/src/analyses/variable-sensitivity/abstract_environment.h index 42b39bc3d23..31c12c987eb 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.h +++ b/src/analyses/variable-sensitivity/abstract_environment.h @@ -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/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index f0bd68c123b..85636f021a1 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -223,7 +223,7 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform( dispatcher->expression_transform(rewritten_expr, ops, environment, ns)); }); - return resolve_new_values(resulting_objects, environment, ns); + return resolve_new_values(resulting_objects, environment); } abstract_object_pointert value_set_abstract_objectt::evaluate_conditional( @@ -251,7 +251,7 @@ abstract_object_pointert value_set_abstract_objectt::evaluate_conditional( 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, ns); + return resolve_new_values(resulting_objects, env); } abstract_object_pointert value_set_abstract_objectt::write( @@ -268,38 +268,20 @@ 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, environment, ns); + 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 namespacet &ns) const + const abstract_environmentt &environment) const { - auto result = environment.abstract_object_factory(type(), ns, true); - auto unwrapped = maybe_unwrap_context(result); - const auto const_value_set_ptr = - std::dynamic_pointer_cast(unwrapped); - const auto value_set_ptr = - std::const_pointer_cast(const_value_set_ptr); - resolve_values(new_values, value_set_ptr); - return result; + 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 -{ - const auto &result = - std::dynamic_pointer_cast(mutable_clone()); - - return resolve_values(new_values, result); -} - -abstract_object_pointert -value_set_abstract_objectt::resolve_values( - const abstract_object_sett &new_values, - const value_set_abstract_object_ptrt &result) const { PRECONDITION(!new_values.empty()); @@ -320,6 +302,9 @@ value_set_abstract_objectt::resolve_values( return (*unwrapped_values.begin()); } + auto result = + std::dynamic_pointer_cast(mutable_clone()); + if( unwrapped_values.size() > max_value_set_size || new_type == abstract_typet::UNSUPPORTED) diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 7be52a82430..1f95b8260bd 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -123,18 +123,12 @@ class value_set_abstract_objectt : public abstract_value_objectt abstract_object_pointert resolve_new_values( const abstract_object_sett &new_values, - const abstract_environmentt &environment, - const namespacet &ns) const; + const abstract_environmentt &environment) const; abstract_object_pointert resolve_values( const abstract_object_sett &new_values) const; - abstract_object_pointert - resolve_values( - const abstract_object_sett &new_values, - const value_set_abstract_object_ptrt &result) const; - // data abstract_typet my_type; abstract_object_sett values; diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp index 86759309d3d..ab24ed87483 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp @@ -185,3 +185,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..269556b08be 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; From 4366e75ea1451976548a38a4f84ad3c49435a889 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 27 Jan 2021 16:14:52 +0000 Subject: [PATCH 19/30] Large value-sets are converted to intervals --- .../value-set-convert-to-interval/main.c | 37 +++++++++++++++++++ .../value-set-convert-to-interval/test.desc | 9 +++++ .../value_set_abstract_object.cpp | 2 +- .../value_set_abstract_object.h | 6 +++ 4 files changed, 53 insertions(+), 1 deletion(-) create mode 100644 regression/goto-analyzer/value-set-convert-to-interval/main.c create mode 100644 regression/goto-analyzer/value-set-convert-to-interval/test.desc 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..d537acd587a --- /dev/null +++ b/regression/goto-analyzer/value-set-convert-to-interval/main.c @@ -0,0 +1,37 @@ +#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..7f804fdb2a5 --- /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: 3, 1, 6, 0, 2, 5, 4, :value-set-end @ \[1, 12, 15, 18, 21, 24, 26\] +main::1::b .* value-set-begin: 23, 21, 20, 22, 24, :value-set-end @ \[3, 13, 16, 19, 22\] +main::1::c .* \[14, 1E\] @ \[30\] +-- \ No newline at end of file diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 85636f021a1..5ec9e75e93c 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -349,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)); diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index 1f95b8260bd..b4941e6a1a0 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -118,6 +118,7 @@ class value_set_abstract_objectt : public abstract_value_objectt /// 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 @@ -125,6 +126,11 @@ class value_set_abstract_objectt : public abstract_value_objectt const abstract_object_sett &new_values, const abstract_environmentt &environment) 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 + /// \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; From 50bb92ea9b4590108c2ce9322f453df0c0b38e7f Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 27 Jan 2021 16:44:49 +0000 Subject: [PATCH 20/30] Use make_shared - preferable to constructing by hand --- regression/goto-analyzer/value-set-addition-07/test.desc | 2 +- regression/goto-analyzer/value-set-addition-08/test.desc | 2 +- .../variable_sensitivity_object_factory.cpp | 6 ++---- 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/regression/goto-analyzer/value-set-addition-07/test.desc b/regression/goto-analyzer/value-set-addition-07/test.desc index ce1cf302bbf..7c2cbd7513c 100644 --- a/regression/goto-analyzer/value-set-addition-07/test.desc +++ b/regression/goto-analyzer/value-set-addition-07/test.desc @@ -6,5 +6,5 @@ main.c 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: 37, 32, 42, 28, 38, 27, 43, 33, :value-set-end +main::1::t .* value-set-begin: 37, 32, 42, 27, 43, 28, 38, 33, :value-set-end -- diff --git a/regression/goto-analyzer/value-set-addition-08/test.desc b/regression/goto-analyzer/value-set-addition-08/test.desc index 2e759f938bf..11432175f09 100644 --- a/regression/goto-analyzer/value-set-addition-08/test.desc +++ b/regression/goto-analyzer/value-set-addition-08/test.desc @@ -6,5 +6,5 @@ main.c main::1::p .* value-set-begin: 3, 2, 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: 28, 27, 32, 34, 33, 29, :value-set-end +main::1::t .* value-set-begin: 28, 27, 34, 32, 33, 29, :value-set-end -- diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp index ab24ed87483..e45513f7b93 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp @@ -29,12 +29,10 @@ abstract_object_pointert create_abstract_object( const namespacet &ns) { if(top || bottom) - return abstract_object_pointert( - new abstract_object_classt { type, top, bottom }); + return std::make_shared(type, top, bottom); PRECONDITION(type == ns.follow(e.type())); - return abstract_object_pointert( - new abstract_object_classt { e, environment, ns }); + return std::make_shared(e, environment, ns); } abstract_object_pointert wrap_with_context_object( From d245ab9ab3b8bbeaefef0e585e7d918d3b935ccd Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Fri, 29 Jan 2021 15:06:58 +0000 Subject: [PATCH 21/30] Simplifiy interval_abstract_valuet::expression_transform Tidy up evaluate_conditional and pull out evaluate_unary_expr --- .../interval_abstract_value.cpp | 90 +++++++++---------- .../interval_abstract_value.h | 13 ++- 2 files changed, 54 insertions(+), 49 deletions(-) diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 1a847a5d811..3f3231f4cd2 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) { @@ -315,63 +315,34 @@ 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); if(expr.id() == ID_if) - return evaluate_conditional(type, interval_operands, environment, ns); + return evaluate_conditional(expr, interval_operands, environment, ns); if(num_operands == 1) - { - const constant_interval_exprt &interval = interval_operands[0]->interval; - - if(expr.id() == ID_typecast) - { - const typecast_exprt &tce = to_typecast_expr(expr); - - const constant_interval_exprt &new_interval = interval.typecast(tce.type()); + return evaluate_unary_expr(expr, interval_operands, environment, ns); - INVARIANT( - new_interval.type() == type, - "Type of result interval should match expression type"); + constant_interval_exprt result = interval_operands[0]->interval; - 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); - } - } - else + for (size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex) { - constant_interval_exprt result = interval_operands[0]->interval; - - for (size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex) - { - auto &interval_next = interval_operands[opIndex]->interval; - result = result.eval(expr.id(), interval_next); - } - - INVARIANT( - result.type() == type, - "Type of result interval should match expression type"); - return environment.abstract_object_factory(type, result, ns); + auto &interval_next = interval_operands[opIndex]->interval; + result = result.eval(expr.id(), interval_next); } - return environment.abstract_object_factory(type, ns, true); + INVARIANT( + result.type() == expr.type(), + "Type of result interval should match expression type"); + return environment.abstract_object_factory(expr.type(), result, ns); } abstract_object_pointert interval_abstract_valuet::evaluate_conditional( - const typet &type, - std::vector> interval_operands, + const exprt &expr, + const std::vector& interval_operands, const abstract_environmentt &env, - const namespacet &ns) const + const namespacet &ns) { auto const &condition_interval = interval_operands[0]->interval; auto const &true_interval = interval_operands[1]->interval; @@ -384,7 +355,7 @@ abstract_object_pointert interval_abstract_valuet::evaluate_conditional( // 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( - type, + expr.type(), constant_interval_exprt( constant_interval_exprt::get_min( true_interval.get_lower(), false_interval.get_lower()), @@ -398,6 +369,35 @@ abstract_object_pointert interval_abstract_valuet::evaluate_conditional( : 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 typecast_exprt &tce = to_typecast_expr(expr); + + const constant_interval_exprt &new_interval = operand_expr.typecast(tce.type()); + + INVARIANT( + new_interval.type() == expr.type(), + "Type of result interval should match expression type"); + + return environment.abstract_object_factory(tce.type(), new_interval, ns); + } + + 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( std::ostream &out, const ai_baset &ai, diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 4afdeab0661..97e9ff2fb57 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -85,11 +85,16 @@ class interval_abstract_valuet : public abstract_value_objectt meet(const abstract_object_pointert &other) const override; private: - abstract_object_pointert evaluate_conditional( - const typet &type, - std::vector> interval_operands, + static abstract_object_pointert evaluate_conditional( + const exprt &expr, + const std::vector& interval_operands, const abstract_environmentt &environment, - const namespacet &ns) const; + 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; From 0e06d2a8607552d3b9f0afe1b217489766ede33c Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Fri, 29 Jan 2021 15:20:59 +0000 Subject: [PATCH 22/30] Clean up warnings in interval_abstract_valuet --- .../interval_abstract_value.cpp | 58 +++++++++---------- .../interval_abstract_value.h | 11 ++-- 2 files changed, 34 insertions(+), 35 deletions(-) diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 3f3231f4cd2..1c172f91c74 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -218,22 +218,46 @@ 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) - : abstract_value_objectt(t), interval(t) +interval_abstract_valuet::interval_abstract_valuet(const typet &t) + : abstract_value_objectt(t), interval(t), merge_count(0) { } -interval_abstract_valuet::interval_abstract_valuet(typet t, bool tp, bool bttm) - : abstract_value_objectt(t, tp, bttm), interval(t) +interval_abstract_valuet::interval_abstract_valuet(const typet &t, bool tp, bool bttm) + : abstract_value_objectt(t, tp, bttm), interval(t), merge_count(0) { } interval_abstract_valuet::interval_abstract_valuet( - const constant_interval_exprt e) + const constant_interval_exprt &e) : interval_abstract_valuet(e, 0) { } +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) +{ +} + +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()))) +{ +} + exprt interval_abstract_valuet::to_constant() const { // Attempt to reduce this interval to a constant expression @@ -535,30 +559,6 @@ abstract_object_pointert interval_abstract_valuet::meet_intervals( } } -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 97e9ff2fb57..2919f071d40 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -27,15 +27,14 @@ 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 constant_interval_exprt &e, int merge_count); interval_abstract_valuet( - const exprt e, + const exprt &e, const abstract_environmentt &environment, const namespacet &ns); From 033acbbb22a56f0517d11dcc073c57b94ff239e7 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Fri, 29 Jan 2021 15:26:56 +0000 Subject: [PATCH 23/30] Clean up warnings in constant_abstract_valuet --- .../variable-sensitivity/constant_abstract_value.cpp | 8 ++++---- .../variable-sensitivity/constant_abstract_value.h | 12 +++++------- 2 files changed, 9 insertions(+), 11 deletions(-) diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.cpp b/src/analyses/variable-sensitivity/constant_abstract_value.cpp index 0a6ced0c39b..8715ac6fa5d 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/constant_abstract_value.cpp @@ -33,18 +33,18 @@ 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) @@ -209,7 +209,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; }; From 7fed62238a4a1af08b1688e01a6c200ba9db8440 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Fri, 29 Jan 2021 15:55:53 +0000 Subject: [PATCH 24/30] Remove default arguments from abstract_environmentt::abstract_object_factory Default arguments on a virtual function aren't safe. Even through this function isn't overriden anywhere now, it's a latent bug waiting for the future. --- src/analyses/variable-sensitivity/abstract_environment.cpp | 4 ++-- src/analyses/variable-sensitivity/abstract_environment.h | 4 ++-- src/analyses/variable-sensitivity/abstract_object.cpp | 4 ++-- .../variable-sensitivity/constant_abstract_value.cpp | 2 +- .../variable-sensitivity/full_array_abstract_object.cpp | 2 +- .../variable-sensitivity/full_struct_abstract_object.cpp | 4 ++-- .../variable-sensitivity/interval_abstract_value.cpp | 4 ++-- .../variable-sensitivity/variable_sensitivity_domain.cpp | 6 +++--- 8 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index b023751c63a..f7631bf3b29 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.cpp +++ b/src/analyses/variable-sensitivity/abstract_environment.cpp @@ -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); } } @@ -389,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 31c12c987eb..108bf202afe 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.h +++ b/src/analyses/variable-sensitivity/abstract_environment.h @@ -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 /// 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 8715ac6fa5d..666faa5dcf7 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/constant_abstract_value.cpp @@ -159,7 +159,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(); 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..5537ab9bc82 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,7 @@ 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 1c172f91c74..65919456401 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -304,7 +304,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); @@ -340,7 +340,7 @@ abstract_object_pointert interval_abstract_valuet::expression_transform( } if(num_operands == 0) - return environment.abstract_object_factory(expr.type(), ns, true); + return environment.abstract_object_factory(expr.type(), ns, true, false); if(expr.id() == ID_if) return evaluate_conditional(expr, interval_operands, environment, ns); 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); } } From 6d0085cb009f720683e07766e1c0991989186309 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Fri, 29 Jan 2021 16:11:39 +0000 Subject: [PATCH 25/30] Small fixes in abstract_environmentt Avoid shadowing member variable, make single-arg constructor explicit --- .../variable-sensitivity/abstract_environment.cpp | 12 ++++++------ .../variable-sensitivity/abstract_environment.h | 4 ++-- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp index f7631bf3b29..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); } @@ -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,13 @@ 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( diff --git a/src/analyses/variable-sensitivity/abstract_environment.h b/src/analyses/variable-sensitivity/abstract_environment.h index 108bf202afe..04c3f69e766 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)) { } From a488b3c043176ccb9620d80fb3c7c1a7040e893f Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sat, 30 Jan 2021 11:25:44 +0000 Subject: [PATCH 26/30] Sort value-set output value-set ordering is unstable in the face of code changes, which made tests fragile. Sorting output fixes that and is also easier on the human eye too. We're sorting string representations, so the output isn't a true numerical sort but it's good enough. --- .../ternary-operator-value-sets/test.desc | 12 ++++----- .../value-set-addition-01/main.c | 3 ++- .../value-set-addition-01/test.desc | 4 +-- .../value-set-addition-02/main.c | 3 ++- .../value-set-addition-02/test.desc | 6 ++--- .../value-set-addition-03/main.c | 3 ++- .../value-set-addition-03/test.desc | 2 +- .../value-set-addition-04/main.c | 3 ++- .../value-set-addition-04/test.desc | 8 +++--- .../value-set-addition-05/test.desc | 6 ++--- .../value-set-addition-06/main.c | 10 +++++--- .../value-set-addition-06/test.desc | 6 ++--- .../value-set-addition-07/main.c | 3 ++- .../value-set-addition-07/test.desc | 8 +++--- .../value-set-addition-08/main.c | 3 ++- .../value-set-addition-08/test.desc | 8 +++--- .../value-set-array-constant-access/test.desc | 4 +-- .../value-set-convert-to-interval/main.c | 3 ++- .../value-set-convert-to-interval/test.desc | 6 ++--- .../test.desc | 4 +-- .../test.desc | 2 +- .../test.desc | 2 +- .../test.desc | 8 +++--- .../test.desc | 6 ++--- .../value-set-simple/test_show.desc | 6 ++--- .../value-set-structs/test_show.desc | 4 +-- .../value-set-unary-minus-01/test.desc | 4 +-- .../value-set-unary-minus-02/main.c | 19 ++++++++++++++ .../value-set-unary-minus-02/test.desc | 8 ++++++ .../value-set-unary-not-01/main.c | 3 ++- .../value-set-unary-not-01/test.desc | 4 +-- .../value-set-unary-not-02/main.c | 20 +++++++++++++++ .../value-set-unary-not-02/test.desc | 8 ++++++ .../main.c | 3 ++- .../test.desc | 4 +-- .../test.desc | 8 +++--- .../value_set_abstract_object.cpp | 25 ++++++++++++++++--- 37 files changed, 162 insertions(+), 77 deletions(-) create mode 100644 regression/goto-analyzer/value-set-unary-minus-02/main.c create mode 100644 regression/goto-analyzer/value-set-unary-minus-02/test.desc create mode 100644 regression/goto-analyzer/value-set-unary-not-02/main.c create mode 100644 regression/goto-analyzer/value-set-unary-not-02/test.desc diff --git a/regression/goto-analyzer/ternary-operator-value-sets/test.desc b/regression/goto-analyzer/ternary-operator-value-sets/test.desc index 30bc0e556fa..12aee4014f7 100644 --- a/regression/goto-analyzer/ternary-operator-value-sets/test.desc +++ b/regression/goto-analyzer/ternary-operator-value-sets/test.desc @@ -3,10 +3,10 @@ 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: FALSE, TRUE, :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 +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 index 9bbe413665d..09e0576a6b8 100644 --- a/regression/goto-analyzer/value-set-addition-01/main.c +++ b/regression/goto-analyzer/value-set-addition-01/main.c @@ -1,4 +1,5 @@ -int main(int argc, char argv[]) { +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 index 998112e048f..ada7f6bfeb0 100644 --- a/regression/goto-analyzer/value-set-addition-01/test.desc +++ b/regression/goto-analyzer/value-set-addition-01/test.desc @@ -3,6 +3,6 @@ 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 +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 index 6d625ec38d7..81ba7771978 100644 --- a/regression/goto-analyzer/value-set-addition-02/main.c +++ b/regression/goto-analyzer/value-set-addition-02/main.c @@ -1,4 +1,5 @@ -int main(int argc, char argv[]) { +int main(int argc, char argv[]) +{ int p = 2; int q = 3; diff --git a/regression/goto-analyzer/value-set-addition-02/test.desc b/regression/goto-analyzer/value-set-addition-02/test.desc index 941b4db764a..073cb355e34 100644 --- a/regression/goto-analyzer/value-set-addition-02/test.desc +++ b/regression/goto-analyzer/value-set-addition-02/test.desc @@ -3,7 +3,7 @@ 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 +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 index f90e4549e4e..1c900c8d5e1 100644 --- a/regression/goto-analyzer/value-set-addition-03/main.c +++ b/regression/goto-analyzer/value-set-addition-03/main.c @@ -1,6 +1,7 @@ int unknown(); -int main(int argc, char argv[]) { +int main(int argc, char argv[]) +{ int p = 2; if (unknown()) diff --git a/regression/goto-analyzer/value-set-addition-03/test.desc b/regression/goto-analyzer/value-set-addition-03/test.desc index 18ba0dfa400..87854babafa 100644 --- a/regression/goto-analyzer/value-set-addition-03/test.desc +++ b/regression/goto-analyzer/value-set-addition-03/test.desc @@ -3,5 +3,5 @@ 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 +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 index c2d032bfc84..b3c6007b3c4 100644 --- a/regression/goto-analyzer/value-set-addition-04/main.c +++ b/regression/goto-analyzer/value-set-addition-04/main.c @@ -1,6 +1,7 @@ int unknown(); -int main(int argc, char argv[]) { +int main(int argc, char argv[]) +{ int p = 2; int q = 3; diff --git a/regression/goto-analyzer/value-set-addition-04/test.desc b/regression/goto-analyzer/value-set-addition-04/test.desc index 78d6f9dbd69..3942e26c036 100644 --- a/regression/goto-analyzer/value-set-addition-04/test.desc +++ b/regression/goto-analyzer/value-set-addition-04/test.desc @@ -3,8 +3,8 @@ 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 +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/test.desc b/regression/goto-analyzer/value-set-addition-05/test.desc index 316458ead9a..3bb38335e0e 100644 --- a/regression/goto-analyzer/value-set-addition-05/test.desc +++ b/regression/goto-analyzer/value-set-addition-05/test.desc @@ -3,7 +3,7 @@ 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, 12, 8, 13, :value-set-end +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 index ee1dc9d0d06..8af527ff5c2 100644 --- a/regression/goto-analyzer/value-set-addition-06/main.c +++ b/regression/goto-analyzer/value-set-addition-06/main.c @@ -1,14 +1,18 @@ int unknown(); -int main(int argc, char argv[]) { +int main(int argc, char argv[]) +{ int p; int q; int r = 20; - if (unknown()) { + if (unknown()) + { p = 2; q = 5; - } else { + } + else + { p = 3; q = 10; } diff --git a/regression/goto-analyzer/value-set-addition-06/test.desc b/regression/goto-analyzer/value-set-addition-06/test.desc index 301d57be9bf..9a3fdbad0ff 100644 --- a/regression/goto-analyzer/value-set-addition-06/test.desc +++ b/regression/goto-analyzer/value-set-addition-06/test.desc @@ -3,7 +3,7 @@ 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, 32, 28, 33, :value-set-end +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 index 74fadd3c2c6..51214339456 100644 --- a/regression/goto-analyzer/value-set-addition-07/main.c +++ b/regression/goto-analyzer/value-set-addition-07/main.c @@ -1,6 +1,7 @@ int unknown(); -int main(int argc, char argv[]) { +int main(int argc, char argv[]) +{ int p; int q; int r = 20; diff --git a/regression/goto-analyzer/value-set-addition-07/test.desc b/regression/goto-analyzer/value-set-addition-07/test.desc index 7c2cbd7513c..0c58d85105b 100644 --- a/regression/goto-analyzer/value-set-addition-07/test.desc +++ b/regression/goto-analyzer/value-set-addition-07/test.desc @@ -3,8 +3,8 @@ 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: 37, 32, 42, 27, 43, 28, 38, 33, :value-set-end +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 index c86393a0f15..e5e8546bea1 100644 --- a/regression/goto-analyzer/value-set-addition-08/main.c +++ b/regression/goto-analyzer/value-set-addition-08/main.c @@ -1,6 +1,7 @@ int unknown(); -int main(int argc, char argv[]) { +int main(int argc, char argv[]) +{ int p; int q; int r = 20;; diff --git a/regression/goto-analyzer/value-set-addition-08/test.desc b/regression/goto-analyzer/value-set-addition-08/test.desc index 11432175f09..e8d5452334c 100644 --- a/regression/goto-analyzer/value-set-addition-08/test.desc +++ b/regression/goto-analyzer/value-set-addition-08/test.desc @@ -3,8 +3,8 @@ main.c --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -main::1::p .* value-set-begin: 3, 2, 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: 28, 27, 34, 32, 33, 29, :value-set-end +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/value-set-array-constant-access/test.desc b/regression/goto-analyzer/value-set-array-constant-access/test.desc index 0ad483152ed..a45804d54ba 100644 --- a/regression/goto-analyzer/value-set-array-constant-access/test.desc +++ b/regression/goto-analyzer/value-set-array-constant-access/test.desc @@ -3,5 +3,5 @@ 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 +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 index d537acd587a..cc3790378d2 100644 --- a/regression/goto-analyzer/value-set-convert-to-interval/main.c +++ b/regression/goto-analyzer/value-set-convert-to-interval/main.c @@ -6,7 +6,8 @@ int main(void) { int a = 0; int b = 20; - switch (x) { + switch (x) + { case 1: a = 1; b = 21; diff --git a/regression/goto-analyzer/value-set-convert-to-interval/test.desc b/regression/goto-analyzer/value-set-convert-to-interval/test.desc index 7f804fdb2a5..45b4d120bd1 100644 --- a/regression/goto-analyzer/value-set-convert-to-interval/test.desc +++ b/regression/goto-analyzer/value-set-convert-to-interval/test.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-values set-of-constants --show ^EXIT=0$ ^SIGNAL=0$ -main::1::a .* value-set-begin: 3, 1, 6, 0, 2, 5, 4, :value-set-end @ \[1, 12, 15, 18, 21, 24, 26\] -main::1::b .* value-set-begin: 23, 21, 20, 22, 24, :value-set-end @ \[3, 13, 16, 19, 22\] +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\] --- \ No newline at end of file +-- 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 a6130212eda..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,8 +3,8 @@ 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$ -- diff --git a/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc b/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc index 33fc025930f..d1ff293516a 100644 --- a/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-incremented-01/test.desc @@ -2,7 +2,7 @@ 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 \(\) -> value-set-begin: TOP, :value-set-end +^main::1::fun_incremented_show \(\) -> value-set-begin: TOP :value-set-end ^EXIT=0$ ^SIGNAL=0$ -- 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 index 45a40243fd3..1cb8f3ff001 100644 --- a/regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-incremented-02/test.desc @@ -2,7 +2,7 @@ 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 +^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 f45ed80d2b8..2a5eecf32e9 100644 --- a/regression/goto-analyzer/value-set-function-pointers-simple/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-simple/test.desc @@ -7,10 +7,10 @@ main.c ^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::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$ -- 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 0dde4f66c88..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,9 +4,9 @@ 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 @ \[23, 25\]} @ \[23, 25\] -^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$ -- diff --git a/regression/goto-analyzer/value-set-simple/test_show.desc b/regression/goto-analyzer/value-set-simple/test_show.desc index c8795266c77..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 0942a930690..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 @ \[16\], \.str=\{\[0\] = value-set-begin: '[xy]', '[xy]', :value-set-end @ \[16\]\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 @ \[49\], \.str=\{\[0\] = value-set-begin: '[xyz]', '[xyz]', '[xyz]', :value-set-end @ \[49\]\n\[1\] = value-set-begin: '\\n', :value-set-end @ \[49\]\n} @ \[49\]} @ \[49\] +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/test.desc b/regression/goto-analyzer/value-set-unary-minus-01/test.desc index 8126445625d..2aeb3f68be8 100644 --- a/regression/goto-analyzer/value-set-unary-minus-01/test.desc +++ b/regression/goto-analyzer/value-set-unary-minus-01/test.desc @@ -3,6 +3,6 @@ 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 +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..289d9cee1db --- /dev/null +++ b/regression/goto-analyzer/value-set-unary-minus-02/main.c @@ -0,0 +1,19 @@ +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 index 448c8eac5ea..db3365e9aa8 100644 --- a/regression/goto-analyzer/value-set-unary-not-01/main.c +++ b/regression/goto-analyzer/value-set-unary-not-01/main.c @@ -1,4 +1,5 @@ -int main(int argc, char argv[]) { +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 index e6672bee29c..bae2f5d14b1 100644 --- a/regression/goto-analyzer/value-set-unary-not-01/test.desc +++ b/regression/goto-analyzer/value-set-unary-not-01/test.desc @@ -3,6 +3,6 @@ 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 +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..aed1173a2d6 --- /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-value-set-access-02/main.c b/regression/goto-analyzer/variable-sensitivity-array-value-set-access-02/main.c index 464db0e214f..6e1dbad65d2 100644 --- 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 @@ -1,6 +1,7 @@ int unknown(); -int main(int argc, char argv[]) { +int main(int argc, char argv[]) +{ int array[2] = { 1, 2 }; int 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 index e49d86dcc6a..e96f8afd270 100644 --- 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 @@ -3,5 +3,5 @@ main.c --show --variable-sensitivity --vsd-values set-of-constants --vsd-arrays every-element ^EXIT=0$ ^SIGNAL=0$ -main::1::t \(\) -> value-set-begin: 3, 2, 1, :value-set-end -main::1::p \(\) -> value-set-begin: 0, 1, :value-set-end +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/test.desc b/regression/goto-analyzer/variable-sensitivity-array-value-set-access/test.desc index f5e0812ef10..ec83e23bc98 100644 --- a/regression/goto-analyzer/variable-sensitivity-array-value-set-access/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-array-value-set-access/test.desc @@ -3,7 +3,7 @@ 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: 4, 1, :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 +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/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index 5ec9e75e93c..d0ed7ccb699 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -15,6 +15,7 @@ #include #include #include +#include using abstract_object_sett = value_set_abstract_objectt::abstract_object_sett; @@ -376,6 +377,15 @@ void value_set_abstract_objectt::set_values(const abstract_object_sett &other_va 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, @@ -392,12 +402,19 @@ void value_set_abstract_objectt::output( else { out << "value-set-begin: "; - for(auto const &value : values) + + std::vector output_values; + for(const auto &value : values) { - value->output(out, ai, ns); - out << ", "; + std::ostringstream ss; + value->output(ss, ai, ns); + output_values.emplace_back(ss.str()); } - out << ":value-set-end"; + std::sort(output_values.begin(), output_values.end(), by_length); + + join_strings(out, output_values.begin(), output_values.end(), ", "); + + out << " :value-set-end"; } } From bf90f7593e1f6e600983431281c94e8af18f4f38 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Sat, 30 Jan 2021 11:50:38 +0000 Subject: [PATCH 27/30] clang-format fixes --- .../value-set-addition-01/main.c | 2 +- .../value-set-addition-02/main.c | 2 +- .../value-set-addition-03/main.c | 6 +-- .../value-set-addition-04/main.c | 5 +-- .../value-set-addition-05/main.c | 10 +++-- .../value-set-addition-06/main.c | 8 ++-- .../value-set-addition-07/main.c | 17 ++++++-- .../value-set-addition-08/main.c | 18 +++++--- .../value-set-convert-to-interval/main.c | 2 +- .../main.c | 4 +- .../value-set-unary-minus-01/main.c | 3 +- .../value-set-unary-minus-02/main.c | 5 ++- .../value-set-unary-not-02/main.c | 2 +- .../main.c | 10 +++-- .../abstract_environment.h | 4 +- .../constant_abstract_value.cpp | 5 ++- .../full_struct_abstract_object.cpp | 3 +- .../interval_abstract_value.cpp | 35 ++++++++------- .../interval_abstract_value.h | 4 +- .../value_set_abstract_object.cpp | 43 +++++++++---------- .../value_set_abstract_object.h | 10 ++--- .../variable_sensitivity_object_factory.cpp | 18 ++++---- .../variable_sensitivity_object_factory.h | 4 +- 23 files changed, 125 insertions(+), 95 deletions(-) diff --git a/regression/goto-analyzer/value-set-addition-01/main.c b/regression/goto-analyzer/value-set-addition-01/main.c index 09e0576a6b8..cfd9dd731f0 100644 --- a/regression/goto-analyzer/value-set-addition-01/main.c +++ b/regression/goto-analyzer/value-set-addition-01/main.c @@ -1,4 +1,4 @@ -int main(int argc, char argv[]) +int main(int argc, char argv[]) { int p = 1; diff --git a/regression/goto-analyzer/value-set-addition-02/main.c b/regression/goto-analyzer/value-set-addition-02/main.c index 81ba7771978..fa292d90ee4 100644 --- a/regression/goto-analyzer/value-set-addition-02/main.c +++ b/regression/goto-analyzer/value-set-addition-02/main.c @@ -1,4 +1,4 @@ -int main(int argc, char argv[]) +int main(int argc, char argv[]) { int p = 2; int q = 3; diff --git a/regression/goto-analyzer/value-set-addition-03/main.c b/regression/goto-analyzer/value-set-addition-03/main.c index 1c900c8d5e1..afbb59a6f0c 100644 --- a/regression/goto-analyzer/value-set-addition-03/main.c +++ b/regression/goto-analyzer/value-set-addition-03/main.c @@ -1,11 +1,11 @@ int unknown(); -int main(int argc, char argv[]) +int main(int argc, char argv[]) { int p = 2; - if (unknown()) + if(unknown()) p += 2; else - p += 3; + p += 3; } diff --git a/regression/goto-analyzer/value-set-addition-04/main.c b/regression/goto-analyzer/value-set-addition-04/main.c index b3c6007b3c4..fd056b21e9b 100644 --- a/regression/goto-analyzer/value-set-addition-04/main.c +++ b/regression/goto-analyzer/value-set-addition-04/main.c @@ -1,15 +1,14 @@ int unknown(); -int main(int argc, char argv[]) +int main(int argc, char argv[]) { int p = 2; int q = 3; - if (unknown()) + if(unknown()) p += 2; else p += 3; - int t = p + q; } diff --git a/regression/goto-analyzer/value-set-addition-05/main.c b/regression/goto-analyzer/value-set-addition-05/main.c index 473bf471d88..7b0de1f0d91 100644 --- a/regression/goto-analyzer/value-set-addition-05/main.c +++ b/regression/goto-analyzer/value-set-addition-05/main.c @@ -1,13 +1,17 @@ int unknown(); -int main(int argc, char argv[]) { +int main(int argc, char argv[]) +{ int p; int q; - if (unknown()) { + if(unknown()) + { p = 2; q = 5; - } else { + } + else + { p = 3; q = 10; } diff --git a/regression/goto-analyzer/value-set-addition-06/main.c b/regression/goto-analyzer/value-set-addition-06/main.c index 8af527ff5c2..e2428b6df6b 100644 --- a/regression/goto-analyzer/value-set-addition-06/main.c +++ b/regression/goto-analyzer/value-set-addition-06/main.c @@ -1,17 +1,17 @@ int unknown(); -int main(int argc, char argv[]) +int main(int argc, char argv[]) { int p; int q; int r = 20; - if (unknown()) + if(unknown()) { p = 2; q = 5; - } - else + } + else { p = 3; q = 10; diff --git a/regression/goto-analyzer/value-set-addition-07/main.c b/regression/goto-analyzer/value-set-addition-07/main.c index 51214339456..eb29cffa9f0 100644 --- a/regression/goto-analyzer/value-set-addition-07/main.c +++ b/regression/goto-analyzer/value-set-addition-07/main.c @@ -1,14 +1,23 @@ int unknown(); -int main(int argc, char argv[]) +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; + 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-08/main.c b/regression/goto-analyzer/value-set-addition-08/main.c index e5e8546bea1..1029400202a 100644 --- a/regression/goto-analyzer/value-set-addition-08/main.c +++ b/regression/goto-analyzer/value-set-addition-08/main.c @@ -1,14 +1,22 @@ int unknown(); -int main(int argc, char argv[]) +int main(int argc, char argv[]) { int p; int q; - int r = 20;; + int r = 20; + ; - if (unknown()) p = 2; else p = 3; - if (unknown()) p = 4; - if (unknown()) q = 5; else q = 10; + 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-convert-to-interval/main.c b/regression/goto-analyzer/value-set-convert-to-interval/main.c index cc3790378d2..9e4c5e55c1b 100644 --- a/regression/goto-analyzer/value-set-convert-to-interval/main.c +++ b/regression/goto-analyzer/value-set-convert-to-interval/main.c @@ -6,7 +6,7 @@ int main(void) { int a = 0; int b = 20; - switch (x) + switch(x) { case 1: a = 1; 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 index c0abcabb59b..d2ebc3f380b 100644 --- a/regression/goto-analyzer/value-set-function-pointers-incremented-02/main.c +++ b/regression/goto-analyzer/value-set-function-pointers-incremented-02/main.c @@ -25,9 +25,9 @@ int main(void) // function pointer incremented should be top fptr_t fun_incremented = f; - if (i) + if(i) ++fun_incremented; - else + else fun_incremented = h; fun_incremented(5); fptr_t fun_incremented_show = fun_incremented; diff --git a/regression/goto-analyzer/value-set-unary-minus-01/main.c b/regression/goto-analyzer/value-set-unary-minus-01/main.c index 7d606d5be14..9f33f9fe745 100644 --- a/regression/goto-analyzer/value-set-unary-minus-01/main.c +++ b/regression/goto-analyzer/value-set-unary-minus-01/main.c @@ -1,4 +1,5 @@ -int main(int argc, char argv[]) { +int main(int argc, char argv[]) +{ int p = 1; int q = -p; diff --git a/regression/goto-analyzer/value-set-unary-minus-02/main.c b/regression/goto-analyzer/value-set-unary-minus-02/main.c index 289d9cee1db..906bfa29e39 100644 --- a/regression/goto-analyzer/value-set-unary-minus-02/main.c +++ b/regression/goto-analyzer/value-set-unary-minus-02/main.c @@ -1,8 +1,9 @@ -int main(int argc, char argv[]) { +int main(int argc, char argv[]) +{ int unknown; int p; - switch (unknown) + switch(unknown) { case 0: p = 0; diff --git a/regression/goto-analyzer/value-set-unary-not-02/main.c b/regression/goto-analyzer/value-set-unary-not-02/main.c index aed1173a2d6..6e8b9a5c57c 100644 --- a/regression/goto-analyzer/value-set-unary-not-02/main.c +++ b/regression/goto-analyzer/value-set-unary-not-02/main.c @@ -3,7 +3,7 @@ int main(int argc, char argv[]) int unknown; int p; - switch (unknown) + switch(unknown) { case 0: p = 0; 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 index 6e1dbad65d2..4660efed1e9 100644 --- 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 @@ -2,11 +2,15 @@ int unknown(); int main(int argc, char argv[]) { - int array[2] = { 1, 2 }; + int array[2] = {1, 2}; int p; - if (unknown()) p = 0; else p = 1; - if (unknown()) array[0] = 3; + if(unknown()) + p = 0; + else + p = 1; + if(unknown()) + array[0] = 3; int t = array[p]; } diff --git a/src/analyses/variable-sensitivity/abstract_environment.h b/src/analyses/variable-sensitivity/abstract_environment.h index 04c3f69e766..974da0f93f9 100644 --- a/src/analyses/variable-sensitivity/abstract_environment.h +++ b/src/analyses/variable-sensitivity/abstract_environment.h @@ -180,8 +180,8 @@ class abstract_environmentt /// 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; + virtual abstract_object_pointert + add_object_context(const abstract_object_pointert &abstract_object) const; /// Computes the join between "this" and "b" /// diff --git a/src/analyses/variable-sensitivity/constant_abstract_value.cpp b/src/analyses/variable-sensitivity/constant_abstract_value.cpp index 666faa5dcf7..7c409e73e1d 100644 --- a/src/analyses/variable-sensitivity/constant_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/constant_abstract_value.cpp @@ -38,7 +38,10 @@ constant_abstract_valuet::constant_abstract_valuet(const typet &t) { } -constant_abstract_valuet::constant_abstract_valuet(const 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() { } diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp index 5537ab9bc82..51d3535e71f 100644 --- a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp @@ -100,7 +100,8 @@ abstract_object_pointert full_struct_abstract_objectt::read_component( } else { - return environment.abstract_object_factory(member_expr.type(), ns, true, false); + 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 65919456401..7bbc67eaf8f 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -223,7 +223,10 @@ interval_abstract_valuet::interval_abstract_valuet(const typet &t) { } -interval_abstract_valuet::interval_abstract_valuet(const 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), merge_count(0) { } @@ -238,9 +241,9 @@ 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()), + e.type(), + e.is_top() || merge_count > 10, + e.is_bottom()), interval(e), merge_count(merge_count) { @@ -251,10 +254,10 @@ interval_abstract_valuet::interval_abstract_valuet( 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()))) + represents_interval(e) + ? make_interval_expr(e) + : (e.operands().size() == 2 ? interval_from_relation(e) + : constant_interval_exprt(e.type()))) { } @@ -350,7 +353,7 @@ abstract_object_pointert interval_abstract_valuet::expression_transform( constant_interval_exprt result = interval_operands[0]->interval; - for (size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex) + for(size_t opIndex = 1; opIndex != interval_operands.size(); ++opIndex) { auto &interval_next = interval_operands[opIndex]->interval; result = result.eval(expr.id(), interval_next); @@ -364,7 +367,7 @@ abstract_object_pointert interval_abstract_valuet::expression_transform( abstract_object_pointert interval_abstract_valuet::evaluate_conditional( const exprt &expr, - const std::vector& interval_operands, + const std::vector &interval_operands, const abstract_environmentt &env, const namespacet &ns) { @@ -389,13 +392,15 @@ abstract_object_pointert interval_abstract_valuet::evaluate_conditional( } 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); + ? 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 std::vector &interval_operands, const abstract_environmentt &environment, const namespacet &ns) { @@ -405,7 +410,8 @@ abstract_object_pointert interval_abstract_valuet::evaluate_unary_expr( { const typecast_exprt &tce = to_typecast_expr(expr); - const constant_interval_exprt &new_interval = operand_expr.typecast(tce.type()); + const constant_interval_exprt &new_interval = + operand_expr.typecast(tce.type()); INVARIANT( new_interval.type() == expr.type(), @@ -421,7 +427,6 @@ abstract_object_pointert interval_abstract_valuet::evaluate_unary_expr( return environment.abstract_object_factory(expr.type(), interval_result, ns); } - void interval_abstract_valuet::output( std::ostream &out, const ai_baset &ai, diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 2919f071d40..98a44001591 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -86,12 +86,12 @@ class interval_abstract_valuet : public abstract_value_objectt private: static abstract_object_pointert evaluate_conditional( const exprt &expr, - const std::vector& interval_operands, + 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 std::vector &interval_operands, const abstract_environmentt &environment, const namespacet &ns); diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp index d0ed7ccb699..d15453b2e25 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.cpp @@ -48,8 +48,7 @@ class value_set_index_ranget : public index_ranget abstract_object_sett::const_iterator next; }; -index_range_ptrt make_value_set_index_range( - const abstract_object_sett &vals) +index_range_ptrt make_value_set_index_range(const abstract_object_sett &vals) { return std::make_shared(vals); } @@ -74,7 +73,7 @@ std::vector unwrap_operands(const std::vector &operands); abstract_object_sett -unwrap_and_extract_values(const abstract_object_sett & values); +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 @@ -209,7 +208,8 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform( auto collective_operands = unwrap_operands(operands); if(expr.id() == ID_if) - return evaluate_conditional(expr.type(), collective_operands, environment, ns); + return evaluate_conditional( + expr.type(), collective_operands, environment, ns); abstract_object_sett resulting_objects; @@ -218,7 +218,6 @@ abstract_object_pointert value_set_abstract_objectt::expression_transform( collective_operands, [&resulting_objects, &dispatcher, &expr, &environment, &ns]( const std::vector &ops) { - auto rewritten_expr = rewrite_expression(expr, ops); resulting_objects.insert( dispatcher->expression_transform(rewritten_expr, ops, environment, ns)); @@ -240,7 +239,8 @@ abstract_object_pointert value_set_abstract_objectt::evaluate_conditional( auto all_true = true; auto all_false = true; - for (auto v : condition) { + for(auto v : condition) + { auto expr = v->to_constant(); all_true = all_true && expr.is_true(); all_false = all_false && expr.is_false(); @@ -248,9 +248,9 @@ abstract_object_pointert value_set_abstract_objectt::evaluate_conditional( auto indeterminate = !all_true && !all_false; abstract_object_sett resulting_objects; - if (all_true || indeterminate) + if(all_true || indeterminate) resulting_objects.insert(true_result.begin(), true_result.end()); - if (all_false || indeterminate) + if(all_false || indeterminate) resulting_objects.insert(false_result.begin(), false_result.end()); return resolve_new_values(resulting_objects, env); } @@ -280,8 +280,7 @@ abstract_object_pointert value_set_abstract_objectt::resolve_new_values( return environment.add_object_context(result); } -abstract_object_pointert -value_set_abstract_objectt::resolve_values( +abstract_object_pointert value_set_abstract_objectt::resolve_values( const abstract_object_sett &new_values) const { PRECONDITION(!new_values.empty()); @@ -368,7 +367,8 @@ bool value_set_abstract_objectt::verify() const return true; } -void value_set_abstract_objectt::set_values(const abstract_object_sett &other_values) +void value_set_abstract_objectt::set_values( + const abstract_object_sett &other_values) { PRECONDITION(!other_values.empty()); set_not_top(); @@ -379,9 +379,9 @@ void value_set_abstract_objectt::set_values(const abstract_object_sett &other_va bool by_length(const std::string &lhs, const std::string &rhs) { - if (lhs.size() < rhs.size()) + if(lhs.size() < rhs.size()) return true; - if (lhs.size() > rhs.size()) + if(lhs.size() > rhs.size()) return false; return lhs < rhs; } @@ -445,11 +445,11 @@ type_to_abstract_type(const typet &type) if(type.id() == ID_pointer) return abstract_typet::POINTER; - if( + 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) + 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; @@ -459,18 +459,17 @@ exprt rewrite_expression( const exprt &expr, const std::vector &ops) { - auto operands_expr = exprt::operandst { }; - for (auto v : 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) +unwrap_operands(const std::vector &operands) { - auto unwrapped = - std::vector{}; + auto unwrapped = std::vector{}; for(const auto &op : operands) { diff --git a/src/analyses/variable-sensitivity/value_set_abstract_object.h b/src/analyses/variable-sensitivity/value_set_abstract_object.h index b4941e6a1a0..242b2108366 100644 --- a/src/analyses/variable-sensitivity/value_set_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_abstract_object.h @@ -19,8 +19,8 @@ class value_set_abstract_objectt : public abstract_value_objectt { public: - using value_set_abstract_object_ptrt = std::shared_ptr< - value_set_abstract_objectt>; + using value_set_abstract_object_ptrt = + std::shared_ptr; using abstract_object_sett = std::unordered_set< abstract_object_pointert, @@ -121,8 +121,7 @@ class value_set_abstract_objectt : public abstract_value_objectt /// \param environment: the abstract environment /// \return the abstract object representing \p new_values (either 'this' or /// something new) - abstract_object_pointert - resolve_new_values( + abstract_object_pointert resolve_new_values( const abstract_object_sett &new_values, const abstract_environmentt &environment) const; @@ -132,8 +131,7 @@ class value_set_abstract_objectt : public abstract_value_objectt /// \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; + resolve_values(const abstract_object_sett &new_values) const; // data abstract_typet my_type; diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp index e45513f7b93..dadbc072842 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp @@ -10,13 +10,11 @@ #include "value_set_abstract_value.h" template -abstract_object_pointert create_context_abstract_object( - const abstract_object_pointert &abstract_object) +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() - }); + return abstract_object_pointert( + new context_classt{abstract_object, abstract_object->type()}); } template @@ -40,12 +38,12 @@ abstract_object_pointert wrap_with_context_object( const vsd_configt &configuration) { if(configuration.context_tracking.data_dependency_context) - return create_context_abstract_object< - data_dependency_contextt>(abstract_object); + return create_context_abstract_object( + abstract_object); if(configuration.context_tracking.last_write_context) - return create_context_abstract_object< - write_location_contextt>(abstract_object); + return create_context_abstract_object( + abstract_object); return abstract_object; } diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h index 269556b08be..52d7a183500 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h @@ -71,8 +71,8 @@ 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; + abstract_object_pointert + wrap_with_context(const abstract_object_pointert &abstract_object) const; variable_sensitivity_object_factoryt() = delete; variable_sensitivity_object_factoryt( From 5ad0c9d82b9e6f0ec7e3856ac070ed81e04a3684 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 2 Feb 2021 13:50:12 +0000 Subject: [PATCH 28/30] value-set and data-dependencies is a valid combination value-sets and the data-dependency configuration can be safely combined --- .../variable_sensitivity_configuration.cpp | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.cpp index 492aa302dde..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,8 +29,7 @@ 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 + // 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"); From f9b2f9335c5967dbf4883fb94d928ec95e7c1a01 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Tue, 2 Feb 2021 14:26:01 +0000 Subject: [PATCH 29/30] Combine all the ternary-operator tests into one directory --- .../ternary-operator-intervals/main.c | 19 ------------------- .../ternary-operator-value-sets/main.c | 19 ------------------- .../main.c | 0 .../test-constants.desc} | 0 .../test-intervals.desc} | 0 .../test-value-sets.desc} | 0 .../test.desc | 3 --- 7 files changed, 41 deletions(-) delete mode 100644 regression/goto-analyzer/ternary-operator-intervals/main.c delete mode 100644 regression/goto-analyzer/ternary-operator-value-sets/main.c rename regression/goto-analyzer/{ternary-operator-constants => ternary-operator}/main.c (100%) rename regression/goto-analyzer/{ternary-operator-constants/test.desc => ternary-operator/test-constants.desc} (100%) rename regression/goto-analyzer/{ternary-operator-intervals/test.desc => ternary-operator/test-intervals.desc} (100%) rename regression/goto-analyzer/{ternary-operator-value-sets/test.desc => ternary-operator/test-value-sets.desc} (100%) diff --git a/regression/goto-analyzer/ternary-operator-intervals/main.c b/regression/goto-analyzer/ternary-operator-intervals/main.c deleted file mode 100644 index c76542789fd..00000000000 --- a/regression/goto-analyzer/ternary-operator-intervals/main.c +++ /dev/null @@ -1,19 +0,0 @@ -#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-value-sets/main.c b/regression/goto-analyzer/ternary-operator-value-sets/main.c deleted file mode 100644 index c76542789fd..00000000000 --- a/regression/goto-analyzer/ternary-operator-value-sets/main.c +++ /dev/null @@ -1,19 +0,0 @@ -#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-constants/main.c b/regression/goto-analyzer/ternary-operator/main.c similarity index 100% rename from regression/goto-analyzer/ternary-operator-constants/main.c rename to regression/goto-analyzer/ternary-operator/main.c diff --git a/regression/goto-analyzer/ternary-operator-constants/test.desc b/regression/goto-analyzer/ternary-operator/test-constants.desc similarity index 100% rename from regression/goto-analyzer/ternary-operator-constants/test.desc rename to regression/goto-analyzer/ternary-operator/test-constants.desc diff --git a/regression/goto-analyzer/ternary-operator-intervals/test.desc b/regression/goto-analyzer/ternary-operator/test-intervals.desc similarity index 100% rename from regression/goto-analyzer/ternary-operator-intervals/test.desc rename to regression/goto-analyzer/ternary-operator/test-intervals.desc diff --git a/regression/goto-analyzer/ternary-operator-value-sets/test.desc b/regression/goto-analyzer/ternary-operator/test-value-sets.desc similarity index 100% rename from regression/goto-analyzer/ternary-operator-value-sets/test.desc rename to regression/goto-analyzer/ternary-operator/test-value-sets.desc 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 2a5eecf32e9..604658c3d80 100644 --- a/regression/goto-analyzer/value-set-function-pointers-simple/test.desc +++ b/regression/goto-analyzer/value-set-function-pointers-simple/test.desc @@ -21,6 +21,3 @@ main.c ^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. From f363e38b3a74ba23e8c9d4da959c67a15993ef26 Mon Sep 17 00:00:00 2001 From: Jez Higgins Date: Wed, 3 Feb 2021 12:42:27 +0000 Subject: [PATCH 30/30] Remove interval_abstract_objectt::merge_count See https://github.com/diffblue/cbmc/pull/5793#discussion_r569368166 --- .../interval_abstract_value.cpp | 33 +++++-------------- .../interval_abstract_value.h | 3 -- 2 files changed, 9 insertions(+), 27 deletions(-) diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.cpp b/src/analyses/variable-sensitivity/interval_abstract_value.cpp index 7bbc67eaf8f..5a9fa38dc96 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.cpp +++ b/src/analyses/variable-sensitivity/interval_abstract_value.cpp @@ -219,7 +219,7 @@ static inline constant_interval_exprt interval_from_relation(const exprt &e) } interval_abstract_valuet::interval_abstract_valuet(const typet &t) - : abstract_value_objectt(t), interval(t), merge_count(0) + : abstract_value_objectt(t), interval(t) { } @@ -227,25 +227,13 @@ interval_abstract_valuet::interval_abstract_valuet( const typet &t, bool tp, bool bttm) - : abstract_value_objectt(t, tp, bttm), interval(t), merge_count(0) + : abstract_value_objectt(t, tp, bttm), interval(t) { } interval_abstract_valuet::interval_abstract_valuet( const constant_interval_exprt &e) - : interval_abstract_valuet(e, 0) -{ -} - -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) + : abstract_value_objectt(e.type(), e.is_top(), e.is_bottom()), interval(e) { } @@ -506,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()))); } } @@ -559,8 +545,7 @@ 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)); } } diff --git a/src/analyses/variable-sensitivity/interval_abstract_value.h b/src/analyses/variable-sensitivity/interval_abstract_value.h index 98a44001591..9b1d3faf884 100644 --- a/src/analyses/variable-sensitivity/interval_abstract_value.h +++ b/src/analyses/variable-sensitivity/interval_abstract_value.h @@ -31,7 +31,6 @@ class interval_abstract_valuet : public abstract_value_objectt interval_abstract_valuet(const typet &t, bool tp, bool bttm); explicit interval_abstract_valuet(const constant_interval_exprt &e); - interval_abstract_valuet(const constant_interval_exprt &e, int merge_count); interval_abstract_valuet( const exprt &e, @@ -101,8 +100,6 @@ class interval_abstract_valuet : public abstract_value_objectt meet_intervals(interval_abstract_value_pointert other) const; constant_interval_exprt interval; - - int merge_count; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_INTERVAL_ABSTRACT_VALUE_H