diff --git a/regression/contracts/quantifiers-nested-01/main.c b/regression/contracts/quantifiers-nested-01/main.c new file mode 100644 index 00000000000..7c10be47028 --- /dev/null +++ b/regression/contracts/quantifiers-nested-01/main.c @@ -0,0 +1,24 @@ +// clang-format off +int f1(int *arr) __CPROVER_ensures(__CPROVER_forall { + int i; + __CPROVER_forall + { + int j; + (0 <= i && i < 10 && i <= j && j < 10) ==> arr[i] <= arr[j] + } +}) +// clang-format on +{ + for(int i = 0; i < 10; i++) + { + arr[i] = i; + } + + return 0; +} + +int main() +{ + int arr[10]; + f1(arr); +} diff --git a/regression/contracts/quantifiers-nested-01/test.desc b/regression/contracts/quantifiers-nested-01/test.desc new file mode 100644 index 00000000000..3a6b85c370b --- /dev/null +++ b/regression/contracts/quantifiers-nested-01/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verification: +This test case checks the handling of a forall expression +nested within another forall expression. diff --git a/regression/contracts/quantifiers-nested-02/main.c b/regression/contracts/quantifiers-nested-02/main.c new file mode 100644 index 00000000000..7cfa3051c01 --- /dev/null +++ b/regression/contracts/quantifiers-nested-02/main.c @@ -0,0 +1,19 @@ +// clang-format off +int f1(int *arr) __CPROVER_requires(__CPROVER_forall { + int i; + 0 <= i && i < 9 ==> __CPROVER_forall + { + int j; + (i <= j && j < 10) ==> arr[i] <= arr[j] + } +}) __CPROVER_ensures(__CPROVER_return_value == 0) +// clang-format on +{ + return 0; +} + +int main() +{ + int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}; + f1(arr); +} diff --git a/regression/contracts/quantifiers-nested-02/test.desc b/regression/contracts/quantifiers-nested-02/test.desc new file mode 100644 index 00000000000..218e27b3671 --- /dev/null +++ b/regression/contracts/quantifiers-nested-02/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verification: +This test case checks the handling of a forall expression +nested within an implication. diff --git a/regression/contracts/quantifiers-nested-03/main.c b/regression/contracts/quantifiers-nested-03/main.c new file mode 100644 index 00000000000..7a52ffd4142 --- /dev/null +++ b/regression/contracts/quantifiers-nested-03/main.c @@ -0,0 +1,19 @@ +int f1(int *arr) + __CPROVER_ensures(__CPROVER_return_value == 0 && __CPROVER_exists { + int i; + (0 <= i && i < 10) && arr[i] == i + }) +{ + for(int i = 0; i < 10; i++) + { + arr[i] = i; + } + + return 0; +} + +int main() +{ + int arr[10]; + f1(arr); +} diff --git a/regression/contracts/quantifiers-nested-03/test.desc b/regression/contracts/quantifiers-nested-03/test.desc new file mode 100644 index 00000000000..ceeb1710f4b --- /dev/null +++ b/regression/contracts/quantifiers-nested-03/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verification: +This test case checks the handling of an exists expression +nested within a conjunction. diff --git a/regression/contracts/quantifiers-nested-04/main.c b/regression/contracts/quantifiers-nested-04/main.c new file mode 100644 index 00000000000..82def4f61ce --- /dev/null +++ b/regression/contracts/quantifiers-nested-04/main.c @@ -0,0 +1,21 @@ +// clang-format off +int f1(int *arr) __CPROVER_requires( + __CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 + } || + arr[9] == -1 || + __CPROVER_exists { + int i; + (0 <= i && i < 10) && arr[i] == i + }) __CPROVER_ensures(__CPROVER_return_value == 0) +// clang-format on +{ + return 0; +} + +int main() +{ + int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}; + f1(arr); +} diff --git a/regression/contracts/quantifiers-nested-04/test.desc b/regression/contracts/quantifiers-nested-04/test.desc new file mode 100644 index 00000000000..8bd89966cbb --- /dev/null +++ b/regression/contracts/quantifiers-nested-04/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verification: +This test case checks the handling of both a forall expression +and an exists expression nested within a disjunction. diff --git a/regression/contracts/quantifiers-nested-05/main.c b/regression/contracts/quantifiers-nested-05/main.c new file mode 100644 index 00000000000..6aa20e2cc7f --- /dev/null +++ b/regression/contracts/quantifiers-nested-05/main.c @@ -0,0 +1,15 @@ +// clang-format off +int f1(int *arr) __CPROVER_requires(!__CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 + }) __CPROVER_ensures(__CPROVER_return_value == 0) +// clang-format on +{ + return 0; +} + +int main() +{ + int arr[10] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9}; + f1(arr); +} diff --git a/regression/contracts/quantifiers-nested-05/test.desc b/regression/contracts/quantifiers-nested-05/test.desc new file mode 100644 index 00000000000..ceb27f76675 --- /dev/null +++ b/regression/contracts/quantifiers-nested-05/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verification: +This test case checks the handling of a forall expression +nested within a negation. diff --git a/regression/contracts/quantifiers-nested-06/main.c b/regression/contracts/quantifiers-nested-06/main.c new file mode 100644 index 00000000000..28d2bf24add --- /dev/null +++ b/regression/contracts/quantifiers-nested-06/main.c @@ -0,0 +1,27 @@ +// clang-format off +int f1(int *arr) __CPROVER_requires( + (__CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 + } ? __CPROVER_exists { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 + } : 1 == 0) && + (__CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == i + } ? 1 == 0 : + __CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 + })) __CPROVER_ensures(__CPROVER_return_value == 0) +// clang-format on +{ + return 0; +} + +int main() +{ + int arr[10] = {0, 0, 0, 0, 0, 0, 0, 0, 0, 0}; + f1(arr); +} diff --git a/regression/contracts/quantifiers-nested-06/test.desc b/regression/contracts/quantifiers-nested-06/test.desc new file mode 100644 index 00000000000..c2485334e38 --- /dev/null +++ b/regression/contracts/quantifiers-nested-06/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Verification: +This test case checks the handling of forall and exists expressions +nested within ternary ITE expressions (condition ? true : false). diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index ba671236279..2f0ff44be44 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -26,6 +26,7 @@ Date: February 2016 #include #include #include +#include #include #include #include @@ -168,35 +169,68 @@ void code_contractst::add_quantified_variable( replace_symbolt &replace, irep_idt mode) { - // If the expression is a quantified expression, this function adds - // the quantified variable to the symbol table and to the expression map - - // TODO Currently only works if the contract contains only a single - // quantified formula - // i.e. (1) the top-level element is a quantifier formula - // and (2) there are no inner quantifier formulae - // This TODO is handled in PR #5968 - - if(expression.id() == ID_exists || expression.id() == ID_forall) - { - // get quantified symbol - exprt tuple = expression.operands().front(); - exprt quantified_variable = tuple.operands().front(); - symbol_exprt quantified_symbol = to_symbol_expr(quantified_variable); - - // create fresh symbol - symbolt new_symbol = get_fresh_aux_symbol( - quantified_symbol.type(), - id2string(quantified_symbol.get_identifier()), - "tmp", - quantified_symbol.source_location(), - mode, - symbol_table); - - // add created fresh symbol to expression map - symbol_exprt q( - quantified_symbol.get_identifier(), quantified_symbol.type()); - replace.insert(q, new_symbol.symbol_expr()); + if(expression.id() == ID_not || expression.id() == ID_typecast) + { + // For unary connectives, recursively check for + // nested quantified formulae in the term + const auto &unary_expression = to_unary_expr(expression); + add_quantified_variable(unary_expression.op(), replace, mode); + } + if(expression.id() == ID_notequal || expression.id() == ID_implies) + { + // For binary connectives, recursively check for + // nested quantified formulae in the left and right terms + const auto &binary_expression = to_binary_expr(expression); + add_quantified_variable(binary_expression.lhs(), replace, mode); + add_quantified_variable(binary_expression.rhs(), replace, mode); + } + if(expression.id() == ID_if) + { + // For ternary connectives, recursively check for + // nested quantified formulae in all three terms + const auto &if_expression = to_if_expr(expression); + add_quantified_variable(if_expression.cond(), replace, mode); + add_quantified_variable(if_expression.true_case(), replace, mode); + add_quantified_variable(if_expression.false_case(), replace, mode); + } + if(expression.id() == ID_and || expression.id() == ID_or) + { + // For multi-ary connectives, recursively check for + // nested quantified formulae in all terms + const auto &multi_ary_expression = to_multi_ary_expr(expression); + for(const auto &operand : multi_ary_expression.operands()) + { + add_quantified_variable(operand, replace, mode); + } + } + else if(expression.id() == ID_exists || expression.id() == ID_forall) + { + // When a quantifier expression is found, + // 1. get quantified variables + const auto &quantifier_expression = to_quantifier_expr(expression); + const auto &quantified_variables = quantifier_expression.variables(); + for(const auto &quantified_variable : quantified_variables) + { + // for each quantified variable... + const auto &quantified_symbol = to_symbol_expr(quantified_variable); + + // 1.1 create fresh symbol + symbolt new_symbol = get_fresh_aux_symbol( + quantified_symbol.type(), + id2string(quantified_symbol.get_identifier()), + "tmp", + quantified_symbol.source_location(), + mode, + symbol_table); + + // 1.2 add created fresh symbol to expression map + symbol_exprt q( + quantified_symbol.get_identifier(), quantified_symbol.type()); + replace.insert(q, new_symbol.symbol_expr()); + + // 1.3 recursively check for nested quantified formulae + add_quantified_variable(quantifier_expression.where(), replace, mode); + } } } diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 24720671374..57c893b2b27 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -167,8 +167,10 @@ class code_contractst void add_contract_check(const irep_idt &, const irep_idt &, goto_programt &dest); - /// If the expression is a quantified expression, this function adds - /// the quantified variable to the symbol table and to the expression map + /// This function recursively searches the expression to find nested or + /// non-nested quantified expressions. When a quantified expression is found, + /// the quantified variable is added to the symbol table + /// and to the expression map. void add_quantified_variable( exprt expression, replace_symbolt &replace,