Optimize symbolic execution using depth-based call graphs

[anvacaru]

Description

The idea is to use a depth-based call graph of the Foundry test suite in order to manage how we do symbolic execution. Instead of starting symbolic execution from the top of the test, you would create a dependency list of functions, then execute them starting with the functions at the lowest level/highest depth and generate simplification lemmas for them. Next, you would execute the next functions up the call graph tree, importing the simplification lemmas for the dependent functions.

Example:

Given this Solidity smart contract

contract BranchingDepthExecutionExample {

    // State variables
    uint256 public countA = 0;
    uint256 public countB = 0;
    uint256 public countC = 0;
    bool public branchCondition = false;

    // Set the branch condition
    function setBranchCondition(bool _condition) public {
        branchCondition = _condition;
    }



    // Function A: Calls both B and C, but B's call is conditional based on branchCondition
    function A() public {
        countA++;
        if(branchCondition) {
            B();
        }
        C();
    }

    // Function B: Calls C
    function B() public {
        countB++;
        C();
    }

    // Function C: A basic function with no further calls
    function C() public {
        countC++;
    }
}

And a test contract

contract BranchingDepthTest is Test, KEVMCheats {
    BranchingDepthExecutionExample c;
    function setUp() public {
        c = new BranchingDepthExecutionExample();
    }
    function testExample(bool branchCondition) external {
        kevm.infiniteGas();
        vm.assume(branchCondition == true);
        c.setBranchCondition(branchCondition);
        c.A();
        c.B();
        c.C();
        assertEq(c.countA(), 1);
        assertEq(c.countB(), 2);
        assertEq(c.countC(), 4);
        
    }
}

With our current symbolic execution, the order of the functions looks like:

And by using the call graph and lemma generation we could have:

Plan:

1. When building the Foundry object in kevm-pyk during kontrol foundry-kompile, generate the call graph of the test functions in the test suite. The call graph depth should start at 0, representing the level of the test function.
2. When foundry-prove --test MyContract.test1 --test MyContract.test2 ... is called, generate a list of the functions that need to be tested: [MyContract.test1, MyContract.test2].
3. For each test function MyContract.f in the list, parse the call graph and append all the functions that MyContract.f would call to the list. This list should then be sorted by the depth level such that the functions with the highest depth (or the most low-level functions) are first.
4. Start to execute the functions in the list symbolically. Functions on the same depth layer/level should be executed in parallel.
5. When the proof execution is finished, generate a simplification lemma for the function and store it locally.
6. After all the functions from the highest depth layer are finished, go to the next layer. Import simplification lemmas generated at 5. only for the calls executed inside the function.

This should improve the symbolic execution process considerably, avoiding execution for duplicated calls.

[ehildenb]

@anvacaru and @PetarMax let's please flesh out a workplan for this one? It's critical for performance and for some of our engagements.

[anvacaru]

CSE - Workplan

Goals: Have Kontrol use compositional symbolic execution of functions by automatically generating function summaries that can be soundly reused at call sites instead of executing the function body.

In Kontrol (Semantics-related changes)

When executing a function, we expect a final node on all branches.
Success, Revert, and Exceptional states are accepted.
In the case of loops, the number of iterations always has to be bounded by a constraint.
Given a function f, To avoid the execution of unfinished branches (such as unbounded loops), we need to add stronger constraints in all the configurations (the lower depth levels) that invoke f using an external call.

• Create the depth call graph of the Solidity functions/tests (In progress - Store external calls as subproofs #62 )
• Identify a given function's initial state(precondition) (In progress - CSE for EVM investigation).
• Automatically generate the initial state (precondition/kcfg with only the init node).
• After symbolically executing the precondition, we generate the summary. The summary consists of a set of CALL rules that skip the execution of the CALL opcode and apply the effect of the summarized function to the current state based on existing preconditions.
• Some indirect changes had to be made to KEVM and Kontrol semantics to streamline the symbolic execution process of a given function:
  1. Refactor expectRevert and prank cheat codes to avoid duplicating CALL rules, causing unnecessary branches when executing a function in a symbolic state (Move expectRevert check outside of CALL*/CREATE*logic #179, Small refactor to pranks. #218).
  2. Implement a no-gas mode for kontrol([DRAFT] Implement no-gas mode #211)
  3. (Ensure #checkCall branch exploration evm-semantics#2194)

In pyk (Semantics-agnostic changes)

• read proof information for a given function that has been invoked in an external call
• How to integrate the subproof information in the current proof process?
  1. Start a new kore-exec instance that includes the summary-generated module that contains the CALL rules with a higher priority
  2. Use the add-module endpoint

[anvacaru]

Next steps

1. Modify how foundry_prove generates the initial state when executing a contract method.
2. Refactor kontrol show --to-module file_path to:
   • avoid writing the kcfg in the file_path
   • generate a valid module name (currently includes invalid characters in the module name, i.e.module SUMMARY-CSE.F(UINT256,UINT160,BOOL):0)
   • generate rewrite rules only from the initial node towards the terminal nodes/leaves.
3. Have the ability to include a module using the add_module endpoint in foundry_prove()

[anvacaru]

Subsumed by #284 and #340.