[Bug-Candidate] CONTINUE node to point to the increment EXPRESSION and not BEGINLOOP

[0xalpharush]

TBD: we might want the CONTINUE node to point to the increment EXPRESSION and not STARTLOOP. See visualization here. Will open an issue and fix in a follow-on PR

Originally posted by @0xalpharush in https://github.com/crytic/slither/issues/629#issuecomment-1205565862

[plotchy]

Currently this means that walking along node sons - typically used in explore() fns - would not accurately have continue statements with an increment block amongst its sons. Could lead to inaccurate tainting or visitor logic.

Looks like a good change to me 👍️

[plotchy]

Adding to this discussion, a detector I made for "unreachable code" does flag on this difference with continue not being succeeded by the increment expression.

def _detect(self):  # pylint: disable=too-many-locals,too-many-branches
        results = []

        # Loop through all contracts
        for contract in self.contracts:

            # Next we'll want to loop through all functions defined directly in this contract.
            # need to remove slitherConstructorConstantVariables & slitherConstructorVariables from the list of functions.
            # property f.is_constructor_variables returns a bool directly for this
            functions = [function for function in contract.functions_declared if not function.is_constructor_variables]

            for function in functions:
                func_nodes = function.nodes

                reachable_nodes = set()
                for node in func_nodes:
                    for r_node in reachable(node):
                        reachable_nodes.add(r_node)
                unreachable_nodes = set(func_nodes) - reachable_nodes
                for unreachable_node in unreachable_nodes:
                    if unreachable_node.type != NodeType.ENTRYPOINT:
                        # ENTRYPOINT nodes are false positives, as they cannot be reached inside the fn
                        info = [function, f" Has unreachable code at this node:\n", unreachable_node, "\n"]
                        res = self.generate_result(info)
                        results.append(res)

        return results 

While detecting on Notional deployed contract https://etherscan.io/address/0x5f11e94e0a69ac8490f45eb27a6478dcddb0227e#code

function _mergeAssetIntoArray(
        PortfolioAsset[] memory assetArray,
        uint256 currencyId,
        uint256 maturity,
        uint256 assetType,
        int256 notional
    ) private pure returns (bool) {
        for (uint256 i = 0; i < assetArray.length; i++) {
            PortfolioAsset memory asset = assetArray[i];
            if (
                asset.assetType != assetType ||
                asset.currencyId != currencyId ||
                asset.maturity != maturity
            ) continue;

            // Either of these storage states mean that some error in logic has occurred, we cannot
            // store this portfolio
            require(
                asset.storageState != AssetStorageState.Delete &&
                asset.storageState != AssetStorageState.RevertIfStored
            ); // dev: portfolio handler deleted storage

            int256 newNotional = asset.notional.add(notional);
            // Liquidity tokens cannot be reduced below zero.
            if (AssetHandler.isLiquidityToken(assetType)) {
                require(newNotional >= 0); // dev: portfolio handler negative liquidity token balance
            }

            require(newNotional >= type(int88).min && newNotional <= type(int88).max); // dev: portfolio handler notional overflow

            asset.notional = newNotional;
            asset.storageState = AssetStorageState.Update;

            return true;
        }

        return false;
    }

The i++ is unreachable, although there is a continue statement

[duckki]

This is a duplicate of https://github.com/crytic/slither/issues/435.

[Tiko7454]

To me continue must always point to the IF_LOOP, because it will work for every type of loop, not only for but also while. Also that will fix the inconsistency. Here is an example

contract C {
  function f() public {
    int x  = 2;
    while (x < 100) {
      x++;
      if (x > 10) {
        continue;
      }
      x += 12;
  }
}

Here, x += 12 points to IF_LOOP, but continue points to BEGIN_LOOP. Due to that inconsistency, if someone wanted to run a loop analysis, he will find out two loops, one containing BEGIN_LOOP and the loop itself, the other the nodes, with ids 3, 4, 5, 7 and 8, which is false positive. Changing continue to point to IF_LOOP solves the issue. Here is the cfg.

digraph{
0[label="Node Type: ENTRY_POINT 0
"];
0->1;
1[label="Node Type: NEW VARIABLE 1

EXPRESSION:
x = 2

IRs:
x(int256) := 2(int256)"];
1->2;
2[label="Node Type: BEGIN_LOOP 2
"];
2->3;
3[label="Node Type: IF_LOOP 3

EXPRESSION:
x < 100

IRs:
TMP_0(bool) = x < 100
CONDITION TMP_0"];
3->4[label="True"];
3->9[label="False"];
4[label="Node Type: EXPRESSION 4

EXPRESSION:
x ++

IRs:
TMP_1(int256) := x(int256)
x(int256) = x (c)+ 1"];
4->5;
5[label="Node Type: IF 5

EXPRESSION:
x > 10

IRs:
TMP_2(bool) = x > 10
CONDITION TMP_2"];
5->6[label="True"];
5->7[label="False"];
6[label="Node Type: CONTINUE 6
"];
6->2;
7[label="Node Type: END_IF 7
"];
7->8;
8[label="Node Type: EXPRESSION 8

EXPRESSION:
x += 12

IRs:
x(int256) = x (c)+ 12"];
8->3;
9[label="Node Type: END_LOOP 9
"];
}

[0xalpharush]

We will eventually have some sort of lowering context that stores the current continue destination and it doesn't have to be the same for the various loop constructs rather just correct. The current CFG code serially parses the AST and doesn't have the ability to look ahead and add the proper destination node because it hasn't yet been created sometimes