cerc-io/solidity
10
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #8747 from ethereum/smt_chc_docs_internal_calls

Browse Source 
Add internal function calls to CHC docs
This commit is contained in:
chriseth 2020-04-23 12:14:54 +02:00 committed by GitHub
commit 393f922081
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 20 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
docs/security-considerations.rst
View File

@ -491,7 +491,8 @@ Horn clauses, where the lifecycle of the contract is represented by a loop
that can visit every public/external function non-deterministically. This way, that can visit every public/external function non-deterministically. This way,
the behavior of the entire contract over an unbounded number of transactions the behavior of the entire contract over an unbounded number of transactions
is taken into account when analyzing any function. Loops are fully supported is taken into account when analyzing any function. Loops are fully supported
by this engine. Function calls are currently unsupported. by this engine. Internal function calls are supported, but external function
calls are currently unsupported.
The CHC engine is much more powerful than BMC in terms of what it can prove, The CHC engine is much more powerful than BMC in terms of what it can prove,
and might require more computing resources. and might require more computing resources.
@ -505,10 +506,16 @@ erasing knowledge or using a non-precise type). If it determines that a
verification target is safe, it is indeed safe, that is, there are no false verification target is safe, it is indeed safe, that is, there are no false
negatives (unless there is a bug in the SMTChecker). negatives (unless there is a bug in the SMTChecker).
Function calls to the same contract (or base contracts) are inlined when In the BMC engine, function calls to the same contract (or base contracts) are
possible, that is, when their implementation is available. inlined when possible, that is, when their implementation is available. Calls
Calls to functions in other contracts are not inlined even if their code is to functions in other contracts are not inlined even if their code is
available, since we cannot guarantee that the actual deployed code is the same. available, since we cannot guarantee that the actual deployed code is the same.
The CHC engine creates nonlinear Horn clauses that use summaries of the called
functions to support internal function calls. The same approach can and will be
used for external function calls, but the latter requires more work regarding
the entire state of the blockchain and is still unimplemented.
Complex pure functions are abstracted by an uninterpreted function (UF) over Complex pure functions are abstracted by an uninterpreted function (UF) over
the arguments. the arguments.
@ -519,11 +526,14 @@ the arguments.
+-----------------------------------+--------------------------------------+ +-----------------------------------+--------------------------------------+
|``require`` |Assumption | |``require`` |Assumption |
+-----------------------------------+--------------------------------------+ +-----------------------------------+--------------------------------------+
|internal |Inline function call | |internal |BMC: Inline function call |
| |CHC: Function summaries |
+-----------------------------------+--------------------------------------+ +-----------------------------------+--------------------------------------+
|external |Inline function call | |external |BMC: Inline function call or |
| |Erase knowledge about state variables | | |erase knowledge about state variables |
| |and local storage references | | |and local storage references. |
| |CHC: Function summaries and erase |
| |state knowledge. |
+-----------------------------------+--------------------------------------+ +-----------------------------------+--------------------------------------+
|``gasleft``, ``blockhash``, |Abstracted with UF | |``gasleft``, ``blockhash``, |Abstracted with UF |
|``keccak256``, ``ecrecover`` | | |``keccak256``, ``ecrecover`` | |
@ -534,8 +544,8 @@ the arguments.
|implementation (external or | | |implementation (external or | |
|complex) | | |complex) | |
+-----------------------------------+--------------------------------------+ +-----------------------------------+--------------------------------------+
|external functions without |Unsupported | |external functions without |BMC: Unsupported |
|implementation | | |implementation |CHC: Nondeterministic summary |
+-----------------------------------+--------------------------------------+ +-----------------------------------+--------------------------------------+
|others |Currently unsupported | |others |Currently unsupported |
+-----------------------------------+--------------------------------------+ +-----------------------------------+--------------------------------------+