From 33b412b8afb9dbd835752c236e97fb58321f8b46 Mon Sep 17 00:00:00 2001 From: ArenBabikian Date: Mon, 22 Mar 2021 18:39:56 +0000 Subject: [PATCH] Add support for nested quantifiers in function contracts This adds support for nested quantifiers in funtion contracts. We recursively handle quantifiers that are nested within other quantifiers or within Boolean connectives. --- .../contracts/quantifiers-nested-01/main.c | 24 +++++ .../contracts/quantifiers-nested-01/test.desc | 11 +++ .../contracts/quantifiers-nested-02/main.c | 19 ++++ .../contracts/quantifiers-nested-02/test.desc | 11 +++ .../contracts/quantifiers-nested-03/main.c | 19 ++++ .../contracts/quantifiers-nested-03/test.desc | 11 +++ .../contracts/quantifiers-nested-04/main.c | 21 +++++ .../contracts/quantifiers-nested-04/test.desc | 11 +++ .../contracts/quantifiers-nested-05/main.c | 15 +++ .../contracts/quantifiers-nested-05/test.desc | 11 +++ .../contracts/quantifiers-nested-06/main.c | 27 ++++++ .../contracts/quantifiers-nested-06/test.desc | 11 +++ src/goto-instrument/code_contracts.cpp | 92 +++++++++++++------ src/goto-instrument/code_contracts.h | 6 +- 14 files changed, 258 insertions(+), 31 deletions(-) create mode 100644 regression/contracts/quantifiers-nested-01/main.c create mode 100644 regression/contracts/quantifiers-nested-01/test.desc create mode 100644 regression/contracts/quantifiers-nested-02/main.c create mode 100644 regression/contracts/quantifiers-nested-02/test.desc create mode 100644 regression/contracts/quantifiers-nested-03/main.c create mode 100644 regression/contracts/quantifiers-nested-03/test.desc create mode 100644 regression/contracts/quantifiers-nested-04/main.c create mode 100644 regression/contracts/quantifiers-nested-04/test.desc create mode 100644 regression/contracts/quantifiers-nested-05/main.c create mode 100644 regression/contracts/quantifiers-nested-05/test.desc create mode 100644 regression/contracts/quantifiers-nested-06/main.c create mode 100644 regression/contracts/quantifiers-nested-06/test.desc 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,