-
Notifications
You must be signed in to change notification settings - Fork 262
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
CONTRACTS: add function-contract mapping to the CLI
Enables checking or replacing a contract against a function of a different name as long as signatures are compatible.
- Loading branch information
Remi Delmas
committed
Dec 20, 2022
1 parent
c159cba
commit 7d0ebd5
Showing
13 changed files
with
255 additions
and
50 deletions.
There are no files selected for viewing
40 changes: 40 additions & 0 deletions
40
regression/contracts-dfcc/function-contract-mapping/main.c
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
#include <stdbool.h> | ||
#include <stdlib.h> | ||
|
||
bool my_contract(char *arr, size_t size, char *out) | ||
// clang-format off | ||
__CPROVER_requires(__CPROVER_is_fresh(arr, size)) | ||
__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out))) | ||
__CPROVER_assigns((size > 0) : arr[0], *out) | ||
__CPROVER_ensures( | ||
(size > 0) ==> __CPROVER_return_value && | ||
(arr[0] == 0) && | ||
(*out == __CPROVER_old(arr[0]))) | ||
__CPROVER_ensures( | ||
(size == 0) ==> !__CPROVER_return_value) | ||
// clang-format on | ||
; | ||
|
||
bool bar(char *arr, size_t size, char *out) | ||
{ | ||
if(size > 0) | ||
{ | ||
*out = arr[0]; | ||
arr[0] = 0; | ||
return true; | ||
} | ||
return false; | ||
} | ||
|
||
bool foo(char *arr, size_t size, char *out) | ||
{ | ||
return bar(arr, size, out); | ||
} | ||
|
||
void main() | ||
{ | ||
char *arr; | ||
size_t size; | ||
char *out; | ||
foo(arr, size, out); | ||
} |
10 changes: 10 additions & 0 deletions
10
regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-contract.desc
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
CORE | ||
main.c | ||
--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/ _ --pointer-check --pointer-primitive-check --pointer-overflow-check | ||
^Invalid function-contract mapping$ | ||
^Reason: couldn't find contract name after '/' in 'foo/'$ | ||
^EXIT=(10|6)$ | ||
^SIGNAL=0$ | ||
-- | ||
-- | ||
Checks that when the contract name is missing an error is triggered. |
10 changes: 10 additions & 0 deletions
10
regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-function.desc
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
CORE | ||
main.c | ||
--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract /my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check | ||
^Invalid function-contract mapping$ | ||
^Reason: couldn't find function name before '/' in '/my_contract'$ | ||
^EXIT=(10|6)$ | ||
^SIGNAL=0$ | ||
-- | ||
-- | ||
Checks that when the function name is missing an error is triggered. |
10 changes: 10 additions & 0 deletions
10
regression/contracts-dfcc/function-contract-mapping/test-enforce-fail-too-many.desc
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
CORE | ||
main.c | ||
--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/bar/my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check | ||
^Invalid function-contract mapping$ | ||
^Reason: couldn't parse 'foo/bar/my_contract'$ | ||
^EXIT=(10|6)$ | ||
^SIGNAL=0$ | ||
-- | ||
-- | ||
Checks that when the function name is missing an error is triggered. |
10 changes: 10 additions & 0 deletions
10
regression/contracts-dfcc/function-contract-mapping/test-enforce-pass.desc
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
CORE | ||
main.c | ||
--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
-- | ||
-- | ||
This test demonstrates the ability to specify a function_name/contract_name | ||
mapping for contract checking. |
13 changes: 13 additions & 0 deletions
13
regression/contracts-dfcc/function-contract-mapping/test-enforce-replace-pass.desc
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
CORE | ||
main.c | ||
--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/my_contract --replace-call-with-contract bar/my_contract _ --pointer-check --pointer-primitive-check --pointer-overflow-check | ||
^EXIT=0$ | ||
^SIGNAL=0$ | ||
^VERIFICATION SUCCESSFUL$ | ||
-- | ||
-- | ||
This test demonstrates the ability to check specify a function_name/contract_name | ||
mapping for contract checking and contract replacement. | ||
|
||
The same contract `my_contract` is used for both `foo` and `bar` functions in | ||
checking and replacement mode, respectively. |
11 changes: 11 additions & 0 deletions
11
regression/contracts-dfcc/function-contract-mapping/test-enforce-warning-not-found.desc
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
CORE | ||
main.c | ||
--malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo/my_contractt _ --pointer-check --pointer-primitive-check --pointer-overflow-check | ||
^Contract 'my_contractt' not found, deriving empty pure contract 'contract::my_contractt' from function 'foo'$ | ||
^VERIFICATION FAILED$ | ||
^EXIT=10$ | ||
^SIGNAL=0$ | ||
-- | ||
-- | ||
Checks that we get a warning that a default contract is derived from the | ||
signature of the function being checked when specifying a non-existing contract. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.