diff --git a/regression/contracts/function_check_02/test.desc b/regression/contracts/function_check_02/test.desc index 9c4d3556c69..ceed9e16bca 100644 --- a/regression/contracts/function_check_02/test.desc +++ b/regression/contracts/function_check_02/test.desc @@ -1,6 +1,6 @@ -KNOWNBUG +CORE main.c ---check-code-contracts +--enforce-all-contracts ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/quantifiers-exists-both-01/main.c b/regression/contracts/quantifiers-exists-both-01/main.c new file mode 100644 index 00000000000..c123d0c837d --- /dev/null +++ b/regression/contracts/quantifiers-exists-both-01/main.c @@ -0,0 +1,18 @@ +// clang-format off +int f1(int *arr) __CPROVER_requires(__CPROVER_exists { + int i; + (0 <= i && i < 8) ==> arr[i] == 0 +}) __CPROVER_ensures(__CPROVER_exists { + int i; + (0 <= i && i < 8) ==> arr[i] == 0 +}) +// clang-format on +{ + return 0; +} + +int main() +{ + int arr[8]; + f1(arr); +} diff --git a/regression/contracts/quantifiers-exists-both-01/test.desc b/regression/contracts/quantifiers-exists-both-01/test.desc new file mode 100644 index 00000000000..ee6c03641c5 --- /dev/null +++ b/regression/contracts/quantifiers-exists-both-01/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_exists +in a negative context (which is currently not always the case). By using the +--enforce-all-contracts flag, this test assumes the statement in +__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures), +thus, verification should be successful. diff --git a/regression/contracts/quantifiers-exists-both-02/main.c b/regression/contracts/quantifiers-exists-both-02/main.c new file mode 100644 index 00000000000..d5a5655bb3d --- /dev/null +++ b/regression/contracts/quantifiers-exists-both-02/main.c @@ -0,0 +1,18 @@ +// clang-format off +int f1(int *arr, int *len) __CPROVER_requires(__CPROVER_exists { + int i; + (0 <= i && i < len) ==> arr[i] == 0 +}) __CPROVER_ensures(__CPROVER_exists { + int i; + (0 <= i && i < len) ==> arr[i] == 0 +}) +// clang-format on +{ + return 0; +} + +int main() +{ + int len, arr[8]; + f1(arr, len); +} diff --git a/regression/contracts/quantifiers-exists-both-02/test.desc b/regression/contracts/quantifiers-exists-both-02/test.desc new file mode 100644 index 00000000000..a8ecf5ff952 --- /dev/null +++ b/regression/contracts/quantifiers-exists-both-02/test.desc @@ -0,0 +1,19 @@ +KNOWNBUG +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_exists +in a negative context (which is currently not always the case). By using the +--enforce-all-contracts flag, this test assumes the statement in +__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures), +thus, verification should be successful. + +Known bug: +The current implementation cannot handle a structure such as +__CPROVER_assume(__CPROVER_exists(int i; pred(i))), where i is +not explicitly bounded to a predefined range (i.e. if at least +one of its bound is only declared and not defined). diff --git a/regression/contracts/quantifiers-exists-ensures-01/main.c b/regression/contracts/quantifiers-exists-ensures-01/main.c new file mode 100644 index 00000000000..45f066045ba --- /dev/null +++ b/regression/contracts/quantifiers-exists-ensures-01/main.c @@ -0,0 +1,20 @@ +// clang-format off +int f1(int *arr) __CPROVER_ensures(__CPROVER_exists { + int i; + (0 <= i && i < 10) ==> arr[i] == i +}) +// 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-exists-ensures-01/test.desc b/regression/contracts/quantifiers-exists-ensures-01/test.desc new file mode 100644 index 00000000000..f1d037caa5f --- /dev/null +++ b/regression/contracts/quantifiers-exists-ensures-01/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_exists +in __CPROVER_ensures clauses. By using the --enforce-all-contracts flag, +goto-instrument will transform the __CPROVER_ensures clauses into an +assertion and the verification remains sound when using __CPROVER_exists. diff --git a/regression/contracts/quantifiers-exists-ensures-02/main.c b/regression/contracts/quantifiers-exists-ensures-02/main.c new file mode 100644 index 00000000000..ea2a2fa88ac --- /dev/null +++ b/regression/contracts/quantifiers-exists-ensures-02/main.c @@ -0,0 +1,20 @@ +// clang-format off +int f1(int *arr) __CPROVER_ensures(__CPROVER_exists { + int i; + (0 <= i && i < 10) ==> arr[i] != 0 +}) +// clang-format on +{ + for(int i = 0; i < 10; i++) + { + arr[i] = 0; + } + + return 0; +} + +int main() +{ + int arr[10]; + f1(arr); +} diff --git a/regression/contracts/quantifiers-exists-ensures-02/test.desc b/regression/contracts/quantifiers-exists-ensures-02/test.desc new file mode 100644 index 00000000000..1fb79381f6f --- /dev/null +++ b/regression/contracts/quantifiers-exists-ensures-02/test.desc @@ -0,0 +1,19 @@ +KNOWNBUG +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_exists +in __CPROVER_ensures clauses. By using the --enforce-all-contracts flag, +goto-instrument will transform the __CPROVER_ensures clauses into an +assertion and the verification remains sound when using __CPROVER_exists. + +Known Bug: +We expect verification to fail because arr[i] is always equal to 0 for +[0 <= i < 10]. In fact, we expect the (0 <= i && i < 10) statement to act as a +range for i. However, in the current implementation of quantifier handling, +the (0 <= i && i < 10) statement is not interpreted as an explicit range, but +instead, as part of a logic formula, which causes verification to succeed. diff --git a/regression/contracts/quantifiers-exists-requires-01/main.c b/regression/contracts/quantifiers-exists-requires-01/main.c new file mode 100644 index 00000000000..aefde2c93bc --- /dev/null +++ b/regression/contracts/quantifiers-exists-requires-01/main.c @@ -0,0 +1,15 @@ +// clang-format off +int f1(int *arr) __CPROVER_requires(__CPROVER_exists { + int i; + (0 <= i && i < 10) ==> arr[i] == 4 +}) __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-exists-requires-01/test.desc b/regression/contracts/quantifiers-exists-requires-01/test.desc new file mode 100644 index 00000000000..60d164515f5 --- /dev/null +++ b/regression/contracts/quantifiers-exists-requires-01/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_exists +in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts +flag, goto-instrument will transform the __CPROVER_requires clauses into an +assertion and the verification remains sound when using __CPROVER_exists. diff --git a/regression/contracts/quantifiers-exists-requires-02/main.c b/regression/contracts/quantifiers-exists-requires-02/main.c new file mode 100644 index 00000000000..db36c3c41c9 --- /dev/null +++ b/regression/contracts/quantifiers-exists-requires-02/main.c @@ -0,0 +1,15 @@ +// clang-format off +int f1(int *arr) __CPROVER_requires(__CPROVER_exists { + int i; + (0 <= i && i < 10) ==> arr[i] == 1 +}) __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-exists-requires-02/test.desc b/regression/contracts/quantifiers-exists-requires-02/test.desc new file mode 100644 index 00000000000..f00b0c7fdb2 --- /dev/null +++ b/regression/contracts/quantifiers-exists-requires-02/test.desc @@ -0,0 +1,19 @@ +KNOWNBUG +main.c +--replace-all-calls-with-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_exists +in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts +flag, goto-instrument will transform the __CPROVER_requires clauses into an +assertion and the verification remains sound when using __CPROVER_exists. + +Known Bug: +We expect verification to fail because arr[i] is never equal to 1 for +[0 <= i < 10]. In fact, we expect the (0 <= i && i < 10) statement to act as a +range for i. However, in the current implementation of quantifier handling, +the (0 <= i && i < 10) statement is not interpreted as an explicit range, but +instead, as part of a logic formula, which causes verification to succeed. diff --git a/regression/contracts/quantifiers-forall-both-01/main.c b/regression/contracts/quantifiers-forall-both-01/main.c new file mode 100644 index 00000000000..a9533000171 --- /dev/null +++ b/regression/contracts/quantifiers-forall-both-01/main.c @@ -0,0 +1,18 @@ +// clang-format off +int f1(int *arr) __CPROVER_requires(__CPROVER_forall { + int i; + (0 <= i && i < 8) ==> arr[i] == 0 +}) __CPROVER_ensures(__CPROVER_forall { + int i; + (0 <= i && i < 8) ==> arr[i] == 0 +}) +// clang-format on +{ + return 0; +} + +int main() +{ + int arr[8]; + f1(arr); +} diff --git a/regression/contracts/quantifiers-forall-both-01/test.desc b/regression/contracts/quantifiers-forall-both-01/test.desc new file mode 100644 index 00000000000..c7f16fc8c51 --- /dev/null +++ b/regression/contracts/quantifiers-forall-both-01/test.desc @@ -0,0 +1,13 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_forall +in a negative context (which is currently not always the case). By using the +--enforce-all-contracts flag, this test assumes the statement in +__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures), +thus, verification should be successful. diff --git a/regression/contracts/quantifiers-forall-both-02/main.c b/regression/contracts/quantifiers-forall-both-02/main.c new file mode 100644 index 00000000000..d173dba1469 --- /dev/null +++ b/regression/contracts/quantifiers-forall-both-02/main.c @@ -0,0 +1,18 @@ +// clang-format off +int f1(int *arr, int len) __CPROVER_requires(__CPROVER_forall { + int i; + (0 <= i && i < len) ==> arr[i] == 0 +}) __CPROVER_ensures(__CPROVER_forall { + int i; + (0 <= i && i < len) ==> arr[i] == 0 +}) +// clang-format on +{ + return 0; +} + +int main() +{ + int len, arr[8]; + f1(arr, len); +} diff --git a/regression/contracts/quantifiers-forall-both-02/test.desc b/regression/contracts/quantifiers-forall-both-02/test.desc new file mode 100644 index 00000000000..8b2381cfb3f --- /dev/null +++ b/regression/contracts/quantifiers-forall-both-02/test.desc @@ -0,0 +1,19 @@ +KNOWNBUG +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_forall +in a negative context (which is currently not always the case). By using the +--enforce-all-contracts flag, this test assumes the statement in +__CPROVER_requires, then asserts the same statement (in __CPROVER_ensures), +thus, verification should be successful. + +Known bug: +The current implementation cannot handle a structure such as +__CPROVER_assume(__CPROVER_forall(int i; pred(i))), where i is +not explicitly bounded to a predefined range (i.e. if at least +one of its bound is only declared and not defined). diff --git a/regression/contracts/quantifiers-forall-ensures-01/main.c b/regression/contracts/quantifiers-forall-ensures-01/main.c new file mode 100644 index 00000000000..b558cc6aedc --- /dev/null +++ b/regression/contracts/quantifiers-forall-ensures-01/main.c @@ -0,0 +1,20 @@ +// clang-format off +int f1(int *arr) __CPROVER_ensures(__CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == 0 +}) +// clang-format on +{ + for(int i = 0; i < 10; i++) + { + arr[i] = 0; + } + + return 0; +} + +int main() +{ + int arr[10]; + f1(arr); +} diff --git a/regression/contracts/quantifiers-forall-ensures-01/test.desc b/regression/contracts/quantifiers-forall-ensures-01/test.desc new file mode 100644 index 00000000000..44769e5ca27 --- /dev/null +++ b/regression/contracts/quantifiers-forall-ensures-01/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_forall +in __CPROVER_ensures clauses. By using the --enforce-all-contracts +flag, goto-instrument will transform the __CPROVER_ensures clauses into an +assertion and the verification remains sound when using __CPROVER_forall. diff --git a/regression/contracts/quantifiers-forall-ensures-02/main.c b/regression/contracts/quantifiers-forall-ensures-02/main.c new file mode 100644 index 00000000000..7904224f227 --- /dev/null +++ b/regression/contracts/quantifiers-forall-ensures-02/main.c @@ -0,0 +1,23 @@ +// clang-format off +int f1(int *arr) __CPROVER_ensures(__CPROVER_forall { + int i; + (0 <= i && i < 10) ==> arr[i] == i +}) +// clang-format on +{ + for(int i = 0; i < 10; i++) + { + if(i == 0) + arr[i] = -1; + else + arr[i] = i; + } + + return 0; +} + +int main() +{ + int arr[10]; + f1(arr); +} diff --git a/regression/contracts/quantifiers-forall-ensures-02/test.desc b/regression/contracts/quantifiers-forall-ensures-02/test.desc new file mode 100644 index 00000000000..3058ae57fd4 --- /dev/null +++ b/regression/contracts/quantifiers-forall-ensures-02/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--enforce-all-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_forall +in __CPROVER_ensures clauses. By using the --enforce-all-contracts +flag, goto-instrument will transform the __CPROVER_ensures clauses into an +assertion and the verification remains sound when using __CPROVER_forall. diff --git a/regression/contracts/quantifiers-forall-requires-01/main.c b/regression/contracts/quantifiers-forall-requires-01/main.c new file mode 100644 index 00000000000..6470ce98056 --- /dev/null +++ b/regression/contracts/quantifiers-forall-requires-01/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] == 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-forall-requires-01/test.desc b/regression/contracts/quantifiers-forall-requires-01/test.desc new file mode 100644 index 00000000000..cb5fe8567b9 --- /dev/null +++ b/regression/contracts/quantifiers-forall-requires-01/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_forall +in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts +flag, goto-instrument will transform the __CPROVER_requires clauses into an +assertion and the verification remains sound when using __CPROVER_forall. diff --git a/regression/contracts/quantifiers-forall-requires-02/main.c b/regression/contracts/quantifiers-forall-requires-02/main.c new file mode 100644 index 00000000000..b8c4caab137 --- /dev/null +++ b/regression/contracts/quantifiers-forall-requires-02/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] == i +}) __CPROVER_ensures(__CPROVER_return_value == 0) +// clang-format on +{ + return 0; +} + +int main() +{ + int arr[10] = {-1, 1, 2, 3, 4, 5, 6, 7, 8, 9}; + f1(arr); +} diff --git a/regression/contracts/quantifiers-forall-requires-02/test.desc b/regression/contracts/quantifiers-forall-requires-02/test.desc new file mode 100644 index 00000000000..f841a39d8c8 --- /dev/null +++ b/regression/contracts/quantifiers-forall-requires-02/test.desc @@ -0,0 +1,12 @@ +CORE +main.c +--replace-all-calls-with-contracts +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +-- +The purpose of this test is to ensure that we can safely use __CPROVER_forall +in __CPROVER_requires clauses. By using the --replace-all-calls-with-contracts +flag, goto-instrument will transform the __CPROVER_requires clauses into an +assertion and the verification remains sound when using __CPROVER_forall. diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp index c1788326964..ba671236279 100644 --- a/src/goto-instrument/code_contracts.cpp +++ b/src/goto-instrument/code_contracts.cpp @@ -163,6 +163,43 @@ bool code_contractst::has_contract(const irep_idt fun_name) return type.has_contract(); } +void code_contractst::add_quantified_variable( + exprt expression, + 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()); + } +} + bool code_contractst::apply_function_contract( const irep_idt &function_id, goto_programt &goto_program, @@ -243,6 +280,11 @@ bool code_contractst::apply_function_contract( } } + // Add quantified variables in contracts to the symbol map + irep_idt mode = symbol_table.lookup_ref(function).mode; + code_contractst::add_quantified_variable(ensures, replace, mode); + code_contractst::add_quantified_variable(requires, replace, mode); + // Replace expressions in the contract components. replace(assigns); replace(requires); @@ -778,6 +820,12 @@ void code_contractst::add_contract_check( replace.insert(parameter_symbol.symbol_expr(), p); } + // Add quantified variables in contracts to the symbol map + code_contractst::add_quantified_variable( + ensures, replace, function_symbol.mode); + code_contractst::add_quantified_variable( + requires, replace, function_symbol.mode); + // assume(requires) if(requires.is_not_nil()) { diff --git a/src/goto-instrument/code_contracts.h b/src/goto-instrument/code_contracts.h index 402885ecf5e..24720671374 100644 --- a/src/goto-instrument/code_contracts.h +++ b/src/goto-instrument/code_contracts.h @@ -25,6 +25,7 @@ Date: February 2016 #include #include #include +#include class messaget; class assigns_clauset; @@ -165,6 +166,13 @@ 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 + void add_quantified_variable( + exprt expression, + replace_symbolt &replace, + irep_idt mode); }; #define FLAG_REPLACE_CALL "replace-call-with-contract"