diff --git a/docs/abi-spec.rst b/docs/abi-spec.rst index 0c38e0f27..2b0ffbe8e 100644 --- a/docs/abi-spec.rst +++ b/docs/abi-spec.rst @@ -530,12 +530,12 @@ i.e. ``0xcf479181``, ``uint256(0)``, ``uint256(amount)``. The error selectors ``0x00000000`` and ``0xffffffff`` are reserved for future use. .. warning:: - Never trust error data. - The error data by default bubbles up through the chain of external calls, which - means that a contract may receive an error not defined in any of the contracts - it calls directly. - Furthermore, any contract can fake any error by returning data that matches - an error signature, even if the error is not defined anywhere. + Never trust error data. + The error data by default bubbles up through the chain of external calls, which + means that a contract may receive an error not defined in any of the contracts + it calls directly. + Furthermore, any contract can fake any error by returning data that matches + an error signature, even if the error is not defined anywhere. .. _abi_json: @@ -619,24 +619,24 @@ would result in the JSON: .. code-block:: json - [{ - "type":"error", - "inputs": [{"name":"available","type":"uint256"},{"name":"required","type":"uint256"}], - "name":"InsufficientBalance" - }, { - "type":"event", - "inputs": [{"name":"a","type":"uint256","indexed":true},{"name":"b","type":"bytes32","indexed":false}], - "name":"Event" - }, { - "type":"event", - "inputs": [{"name":"a","type":"uint256","indexed":true},{"name":"b","type":"bytes32","indexed":false}], - "name":"Event2" - }, { - "type":"function", - "inputs": [{"name":"a","type":"uint256"}], - "name":"foo", - "outputs": [] - }] + [{ + "type":"error", + "inputs": [{"name":"available","type":"uint256"},{"name":"required","type":"uint256"}], + "name":"InsufficientBalance" + }, { + "type":"event", + "inputs": [{"name":"a","type":"uint256","indexed":true},{"name":"b","type":"bytes32","indexed":false}], + "name":"Event" + }, { + "type":"event", + "inputs": [{"name":"a","type":"uint256","indexed":true},{"name":"b","type":"bytes32","indexed":false}], + "name":"Event2" + }, { + "type":"function", + "inputs": [{"name":"a","type":"uint256"}], + "name":"foo", + "outputs": [] + }] Handling tuple types -------------------- @@ -671,61 +671,61 @@ would result in the JSON: .. code-block:: json - [ - { - "name": "f", - "type": "function", - "inputs": [ - { - "name": "s", - "type": "tuple", - "components": [ - { - "name": "a", - "type": "uint256" - }, - { - "name": "b", - "type": "uint256[]" - }, - { - "name": "c", - "type": "tuple[]", - "components": [ - { - "name": "x", - "type": "uint256" - }, - { - "name": "y", - "type": "uint256" - } - ] - } - ] - }, - { - "name": "t", - "type": "tuple", - "components": [ - { - "name": "x", - "type": "uint256" - }, - { - "name": "y", - "type": "uint256" - } - ] - }, - { - "name": "a", - "type": "uint256" - } - ], - "outputs": [] - } - ] + [ + { + "name": "f", + "type": "function", + "inputs": [ + { + "name": "s", + "type": "tuple", + "components": [ + { + "name": "a", + "type": "uint256" + }, + { + "name": "b", + "type": "uint256[]" + }, + { + "name": "c", + "type": "tuple[]", + "components": [ + { + "name": "x", + "type": "uint256" + }, + { + "name": "y", + "type": "uint256" + } + ] + } + ] + }, + { + "name": "t", + "type": "tuple", + "components": [ + { + "name": "x", + "type": "uint256" + }, + { + "name": "y", + "type": "uint256" + } + ] + }, + { + "name": "a", + "type": "uint256" + } + ], + "outputs": [] + } + ] .. _abi_packed_mode: @@ -786,12 +786,12 @@ for prepending a function selector. Since the encoding is ambiguous, there is no .. warning:: - If you use ``keccak256(abi.encodePacked(a, b))`` and both ``a`` and ``b`` are dynamic types, - it is easy to craft collisions in the hash value by moving parts of ``a`` into ``b`` and - vice-versa. More specifically, ``abi.encodePacked("a", "bc") == abi.encodePacked("ab", "c")``. - If you use ``abi.encodePacked`` for signatures, authentication or data integrity, make - sure to always use the same types and check that at most one of them is dynamic. - Unless there is a compelling reason, ``abi.encode`` should be preferred. + If you use ``keccak256(abi.encodePacked(a, b))`` and both ``a`` and ``b`` are dynamic types, + it is easy to craft collisions in the hash value by moving parts of ``a`` into ``b`` and + vice-versa. More specifically, ``abi.encodePacked("a", "bc") == abi.encodePacked("ab", "c")``. + If you use ``abi.encodePacked`` for signatures, authentication or data integrity, make + sure to always use the same types and check that at most one of them is dynamic. + Unless there is a compelling reason, ``abi.encode`` should be preferred. .. _indexed_event_encoding: diff --git a/docs/contracts/events.rst b/docs/contracts/events.rst index d282499dc..3c34d0d1e 100644 --- a/docs/contracts/events.rst +++ b/docs/contracts/events.rst @@ -124,17 +124,17 @@ The output of the above looks like the following (trimmed): .. code-block:: json - { - "returnValues": { - "_from": "0x1111…FFFFCCCC", - "_id": "0x50…sd5adb20", - "_value": "0x420042" - }, - "raw": { - "data": "0x7f…91385", - "topics": ["0xfd4…b4ead7", "0x7f…1a91385"] - } - } + { + "returnValues": { + "_from": "0x1111…FFFFCCCC", + "_id": "0x50…sd5adb20", + "_value": "0x420042" + }, + "raw": { + "data": "0x7f…91385", + "topics": ["0xfd4…b4ead7", "0x7f…1a91385"] + } + } Additional Resources for Understanding Events ============================================== diff --git a/docs/internals/optimizer.rst b/docs/internals/optimizer.rst index 64c8b1460..aee7c8493 100644 --- a/docs/internals/optimizer.rst +++ b/docs/internals/optimizer.rst @@ -89,21 +89,21 @@ the sequence: .. code-block:: none - PUSH 32 - PUSH 0 - CALLDATALOAD - PUSH 100 - DUP2 - MSTORE - KECCAK256 + PUSH 32 + PUSH 0 + CALLDATALOAD + PUSH 100 + DUP2 + MSTORE + KECCAK256 or the equivalent Yul .. code-block:: yul - let x := calldataload(0) - mstore(x, 100) - let value := keccak256(x, 32) + let x := calldataload(0) + mstore(x, 100) + let value := keccak256(x, 32) In this case, the optimizer tracks the value at a memory location ``calldataload(0)`` and then realizes that the Keccak-256 hash can be evaluated at compile time. This only works if there is no @@ -116,14 +116,14 @@ For example, .. code-block:: yul - let x := calldataload(0) - mstore(x, 100) - // Current knowledge memory location x -> 100 - let y := add(x, 32) - // Does not clear the knowledge that x -> 100, since y does not write to [x, x + 32) - mstore(y, 200) - // This Keccak-256 can now be evaluated - let value := keccak256(x, 32) + let x := calldataload(0) + mstore(x, 100) + // Current knowledge memory location x -> 100 + let y := add(x, 32) + // Does not clear the knowledge that x -> 100, since y does not write to [x, x + 32) + mstore(y, 200) + // This Keccak-256 can now be evaluated + let value := keccak256(x, 32) Therefore, modifications to storage and memory locations, of say location ``l``, must erase knowledge about storage or memory locations which may be equal to ``l``. More specifically, for @@ -239,8 +239,8 @@ for all references to ``tag_f`` leaving it unused, s.t. it can be removed, yield .. code-block:: text - ...body of function f... - ...opcodes after call to f... + ...body of function f... + ...opcodes after call to f... So the call to function ``f`` is inlined and the original definition of ``f`` can be removed. @@ -375,7 +375,7 @@ After this step, a program has the following normal form: .. code-block:: text - { I F... } + { I F... } Where ``I`` is a (potentially empty) block that does not contain any function definitions (not even recursively) and ``F`` is a list of function definitions such that no function contains a function definition. @@ -1053,8 +1053,8 @@ remove the parameter and create a new "linking" function as follows: .. code-block:: yul - function f(a,b) -> x { x := div(a,b) } - function f2(a,b,c) -> x, y { x := f(a,b) } + function f(a,b) -> x { x := div(a,b) } + function f2(a,b,c) -> x, y { x := f(a,b) } and replace all references to ``f`` by ``f2``. The inliner should be run afterwards to make sure that all references to ``f2`` are replaced by diff --git a/docs/layout-of-source-files.rst b/docs/layout-of-source-files.rst index 22624c410..9a54a14ef 100644 --- a/docs/layout-of-source-files.rst +++ b/docs/layout-of-source-files.rst @@ -182,7 +182,7 @@ At a global level, you can use import statements of the following form: :: - import "filename"; + import "filename"; The ``filename`` part is called an *import path*. This statement imports all global symbols from "filename" (and symbols imported there) into the @@ -197,7 +197,7 @@ the global symbols from ``"filename"``: :: - import * as symbolName from "filename"; + import * as symbolName from "filename"; which results in all global symbols being available in the format ``symbolName.symbol``. @@ -215,7 +215,7 @@ the code below creates new global symbols ``alias`` and ``symbol2`` which refere :: - import {symbol1 as alias, symbol2} from "filename"; + import {symbol1 as alias, symbol2} from "filename"; .. index:: virtual filesystem, source unit name, import; path, filesystem path, import callback, Remix IDE @@ -255,12 +255,12 @@ Single-line comments (``//``) and multi-line comments (``/*...*/``) are possible :: - // This is a single-line comment. + // This is a single-line comment. - /* - This is a - multi-line comment. - */ + /* + This is a + multi-line comment. + */ .. note:: A single-line comment is terminated by any unicode line terminator diff --git a/docs/smtchecker.rst b/docs/smtchecker.rst index dff8c8463..a4580ce4d 100644 --- a/docs/smtchecker.rst +++ b/docs/smtchecker.rst @@ -44,23 +44,24 @@ where the default is no engine. Selecting the engine enables the SMTChecker on a .. note:: - Prior to Solidity 0.8.4, the default way to enable the SMTChecker was via - ``pragma experimental SMTChecker;`` and only the contracts containing the - pragma would be analyzed. That pragma has been deprecated, and although it - still enables the SMTChecker for backwards compatibility, it will be removed - in Solidity 0.9.0. Note also that now using the pragma even in a single file - enables the SMTChecker for all files. + Prior to Solidity 0.8.4, the default way to enable the SMTChecker was via + ``pragma experimental SMTChecker;`` and only the contracts containing the + pragma would be analyzed. That pragma has been deprecated, and although it + still enables the SMTChecker for backwards compatibility, it will be removed + in Solidity 0.9.0. Note also that now using the pragma even in a single file + enables the SMTChecker for all files. .. note:: - The lack of warnings for a verification target represents an undisputed - mathematical proof of correctness, assuming no bugs in the SMTChecker and - the underlying solver. Keep in mind that these problems are - *very hard* and sometimes *impossible* to solve automatically in the - general case. Therefore, several properties might not be solved or might - lead to false positives for large contracts. Every proven property should - be seen as an important achievement. For advanced users, see :ref:`SMTChecker Tuning ` - to learn a few options that might help proving more complex - properties. + + The lack of warnings for a verification target represents an undisputed + mathematical proof of correctness, assuming no bugs in the SMTChecker and + the underlying solver. Keep in mind that these problems are + *very hard* and sometimes *impossible* to solve automatically in the + general case. Therefore, several properties might not be solved or might + lead to false positives for large contracts. Every proven property should + be seen as an important achievement. For advanced users, see :ref:`SMTChecker Tuning ` + to learn a few options that might help proving more complex + properties. ******** Tutorial @@ -202,8 +203,9 @@ Note that in this example the SMTChecker will automatically try to prove three p 3. The assertion is always true. .. note:: - The properties involve loops, which makes it *much much* harder than the previous - examples, so beware of loops! + + The properties involve loops, which makes it *much much* harder than the previous + examples, so beware of loops! All the properties are correctly proven safe. Feel free to change the properties and/or add restrictions on the array to see different results. @@ -233,18 +235,18 @@ gives us: .. code-block:: bash - Warning: CHC: Assertion violation happens here. - Counterexample: + Warning: CHC: Assertion violation happens here. + Counterexample: - _a = [0, 0, 0, 0, 0] - = 0 + _a = [0, 0, 0, 0, 0] + = 0 - Transaction trace: - Test.constructor() - Test.max([0, 0, 0, 0, 0]) - --> max.sol:14:4: - | - 14 | assert(m > _a[i]); + Transaction trace: + Test.constructor() + Test.max([0, 0, 0, 0, 0]) + --> max.sol:14:4: + | + 14 | assert(m > _a[i]); State Properties @@ -323,26 +325,26 @@ the SMTChecker tells us exactly *how* to reach (2, 4): .. code-block:: bash - Warning: CHC: Assertion violation happens here. - Counterexample: - x = 2, y = 4 + Warning: CHC: Assertion violation happens here. + Counterexample: + x = 2, y = 4 - Transaction trace: - Robot.constructor() - State: x = 0, y = 0 - Robot.moveLeftUp() - State: x = (- 1), y = 1 - Robot.moveRightUp() - State: x = 0, y = 2 - Robot.moveRightUp() - State: x = 1, y = 3 - Robot.moveRightUp() - State: x = 2, y = 4 - Robot.reach_2_4() - --> r.sol:35:4: - | - 35 | assert(!(x == 2 && y == 4)); - | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ + Transaction trace: + Robot.constructor() + State: x = 0, y = 0 + Robot.moveLeftUp() + State: x = (- 1), y = 1 + Robot.moveRightUp() + State: x = 0, y = 2 + Robot.moveRightUp() + State: x = 1, y = 3 + Robot.moveRightUp() + State: x = 2, y = 4 + Robot.reach_2_4() + --> r.sol:35:4: + | + 35 | assert(!(x == 2 && y == 4)); + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^ Note that the path above is not necessarily deterministic, as there are other paths that could reach (2, 4). The choice of which path is shown @@ -367,36 +369,36 @@ anything, including reenter the caller contract. pragma solidity >=0.8.0; interface Unknown { - function run() external; + function run() external; } contract Mutex { - uint x; - bool lock; + uint x; + bool lock; - Unknown immutable unknown; + Unknown immutable unknown; - constructor(Unknown _u) { - require(address(_u) != address(0)); - unknown = _u; - } + constructor(Unknown _u) { + require(address(_u) != address(0)); + unknown = _u; + } - modifier mutex { - require(!lock); - lock = true; - _; - lock = false; - } + modifier mutex { + require(!lock); + lock = true; + _; + lock = false; + } - function set(uint _x) mutex public { - x = _x; - } + function set(uint _x) mutex public { + x = _x; + } - function run() mutex public { - uint xPre = x; - unknown.run(); - assert(xPre == x); - } + function run() mutex public { + uint xPre = x; + unknown.run(); + assert(xPre == x); + } } The example above shows a contract that uses a mutex flag to forbid reentrancy. @@ -410,20 +412,20 @@ that the assertion fails: .. code-block:: bash - Warning: CHC: Assertion violation happens here. - Counterexample: - x = 1, lock = true, unknown = 1 + Warning: CHC: Assertion violation happens here. + Counterexample: + x = 1, lock = true, unknown = 1 - Transaction trace: - Mutex.constructor(1) - State: x = 0, lock = false, unknown = 1 - Mutex.run() - unknown.run() -- untrusted external call, synthesized as: - Mutex.set(1) -- reentrant call - --> m.sol:32:3: - | - 32 | assert(xPre == x); - | ^^^^^^^^^^^^^^^^^ + Transaction trace: + Mutex.constructor(1) + State: x = 0, lock = false, unknown = 1 + Mutex.run() + unknown.run() -- untrusted external call, synthesized as: + Mutex.set(1) -- reentrant call + --> m.sol:32:3: + | + 32 | assert(xPre == x); + | ^^^^^^^^^^^^^^^^^ .. _smtchecker_options: @@ -494,12 +496,11 @@ which has the following form: .. code-block:: none - contracts - { - "source1.sol": ["contract1"], - "source2.sol": ["contract2", "contract3"] - } - + contracts + { + "source1.sol": ["contract1"], + "source2.sol": ["contract2", "contract3"] + } .. _smtchecker_engines: diff --git a/docs/using-the-compiler.rst b/docs/using-the-compiler.rst index 5f261c165..536a66fdd 100644 --- a/docs/using-the-compiler.rst +++ b/docs/using-the-compiler.rst @@ -136,13 +136,13 @@ key in the ``"settings"`` field: .. code-block:: none - { - "sources": { ... }, - "settings": { - "optimizer": { ... }, - "evmVersion": "" + { + "sources": { ... }, + "settings": { + "optimizer": { ... }, + "evmVersion": "" + } } - } Target Options -------------- @@ -781,7 +781,7 @@ It is recommended to explicitly specify the upgrade modules by using ``--modules .. code-block:: none - $ solidity-upgrade --modules constructor-visibility,now,dotsyntax Source.sol + $ solidity-upgrade --modules constructor-visibility,now,dotsyntax Source.sol The command above applies all changes as shown below. Please review them carefully (the pragmas will have to be updated manually.)