CSE with merging node

[Stevengre]

merging node during CSE. Goal:

• The summary only includes two branches: success & revert; & generate only two rules for one function;
• The verification results with / without CSE is the same;
• the KCFG with CSE using less rewriting steps than the KCFG without CSE (summaries successfully applied);
• the structure of the KCFG with CSE is as expected;

Way to validate the result

• if is a summary, then
  • At most two branches from the root: success and revert
  • At most two rules generated: one for success and one for revert
• if is a test
  • the step number of CSE should be 1;
  • the number of CSE steps should match the expected number of CSE steps

Answered Questions

• ArithmeticContract.add_sub_external(uint256,uint256,uint256) should have 2 CSE steps, but got 0 since we minimized the KCFG.
  • fixed using foundryup --version nightly-a0a002020be4c40946fe122fe6ff752b21cb2885
• CallableStorageTest.test_str() is failed to apply the generated rule for CSE. Additionally, CallableStorageContract.str() should be explored. Moreover, the KCFG for CallableStorageTest.test_str() looks weird and can be improved.
  • fixed. But we don't support for assertEq for strings now. And the behavior is different between the CI foundry version and latest foundry version.
• ContractFieldTest.testEscrowToken() is similar to ConstructorTest.test_str(), then why it is passed?
  • Because that cheatcode is supported.
• Why there are two possibilities of SUCCESS in ImportedContract.set(uint256)?
  • There is a if block in the function.

Questions with uncertain anwser

• How can we equivalent the outcome of Enum.enum_storage_range() and Enum.enum_argument_range(uint8)?
• How can we equivalent the outcome of Identity.applyOp(uint256) and Identity.identity(uint256)?

My guess: It is caused by the different process ways provided by the compiler.

• What is Enum.init? The construction of Enum? Also ConstructorTest.init and ImportedContract.init?

  • These functions is alreay used by the kontrol. We just need to store the configuration and use the post-state of the kcfg. BTW, what's the current implementation for this?

• MergeKCFGTest.test_branch_merge(uint256,uint256,bool) is passed but I don't know why it applied 3 times of CSE rather than 2?

  • Branches.applyOp(uint256,uint256,bool).cse.expected is not correct. It has 6 rules rather than 1.

Things can be improved latter

• ConstructorTest.test_contract_call() utilizes concrete values which cannot validate the CSE efficiently.
• Use separate tests for CSE.

PY Script to check the CSE application for tests

#! /usr/bin/env python3

# input: path to a kcfg file
# output: cse steps

import re
import sys

if __name__ == "__main__":
    kcfg_path = sys.argv[1]
    
    with open(kcfg_path, "r") as f:
        prev_node_id = None
        curr_node_id = None
        is_calling = False
        is_callee = False
        counter = 0
        for line in f:
            # after the ┌─, ├─, └─ is the node id
            for match in re.finditer(r"[┌└├]─ (\d+)", line):
                prev_node_id = curr_node_id
                curr_node_id = match.group(1)
                if is_callee:
                    print(f'{prev_node_id} -> {curr_node_id}')
                    is_callee = False
                    counter += 1
            # if the line has "k: #execute ~> #return", then it tries to call a function
            if "k: #execute ~> #return" in line:
                is_calling = True
            # if is_calling and the line has "(\d+ step)"
            if is_calling and re.search(r"\d+ step", line):
                is_calling = False
                steps = int(re.search(r"(\d+) step", line).group(1))
                if steps == 1:
                    is_callee = True
    print(f"Total CSE Steps: {counter}")

Results

Test Name	Type	Passed	Expected CSE Steps
AddConst.applyOp(uint256)	Summary	T	0
ArithmeticCallTest.test_double_add(uint256,uint256)	Test	T	4
ArithmeticCallTest.test_double_add_double_sub(uint256,uint256)	Test	T	8
ArithmeticCallTest.test_double_add_sub_external(uint256,uint256,uint256)	Test	T	4
ArithmeticContract.add(uint256,uint256)	Summary	T	0
ArithmeticContract.add_sub_external(uint256,uint256,uint256)	Summary	T	0
CallableStorageContract.str()	Summary	T	0
CallableStorageTest.test_str()	Test	F => T	1
CSETest.test_add_const(uint256,uint256)	Test	T	2
CSETest.test_identity(uint256,uint256)	Test	T	3
ConstructorTest.test_contract_call()	Test	T	5
ContractFieldTest.testEscrowToken()	Test	T	1
Enum.enum_argument_range(uint8)	Summary	T	0
Enum.enum_storage_range()	Summary	T	0
Enum.init	Summary	T	0
TGovernance.getEscrowTokenTotalSupply()	Summary	T	0
Identity.applyOp(uint256)	Summary	T	0
Identity.identity(uint256)	Summary	T	0
ImportedContract.set(uint256)	Summary	T	0
ImportedContract.add(uint256)	Summary	T	0
ImportedContract.count()	Summary	T	0
InterfaceTagTest.testInterface()	Test	T	1
ConstructorTest.init	?	?	?
ImportedContract.init	?	?	?
StaticCallContract.set(uint256)	Summary	T	0
MergeKCFGTest.test_branch_merge(uint256,uint256,bool)	Test	T	3
Branches.applyOp(uint256,uint256,bool)	Summary	T	0

Updated: 2024/12/11

[Stevengre]

change the options to review the effects easily.

[Stevengre]

CSE with merging node