a16z / halmos

A symbolic testing tool for EVM smart contracts
GNU Affero General Public License v3.0
820 stars 70 forks source link

Contract code, storage #201

Open Bubblecqq opened 1 year ago

Bubblecqq commented 1 year ago

We attempted to customize the code and storage values of a contract by modifying the source code, but encountered some difficulties. The source code modifications were made in the 'deploy_test' and 'setup' functions, where we incorporated information from a JSON file we read. Subsequently, we inserted the account and storage details into the 'sevm.mk_exec()' function within the 'deploy_test' function, such as code={my_code} and storage={my_storage}. If you have any suggestions on how we can customize the code and storage of the contract by modifying the source code, it would be highly valuable to us. Thank you! I will now attach some of my outputs and the modified parts of the source code.

I am testing Storage Test and we want to customize the incoming storage and code by modifying the source code, but we failed. Next, I will attach some of our source code modifications and contract functions。

This is my StorageTest `// SPDX-License-Identifier: AGPL-3.0 pragma solidity >=0.8.0 <0.9.0;

import {SymTest} from "../lib/halmos-cheatcodes/src/SymTest.sol"; import {Test} from "../lib/forge-std/Test.sol"; import "./Storage.sol";

interface IStorage { function retrieve() external view returns (uint256); function my_fuc(uint my_num) external; }

/// @custom:halmos --solver-timeout-assertion 0 contract StorageTest is SymTest, Test {

IStorage storager = IStorage(0x1bA2BFaECa3827F9C5d4b9aD6a30b38eed03fEc6);
//Storage  storager;

function setUp() public {
    //storager = new Storage();
}

// NOTE: currently timeout when --smt-div is enabled, while producing invalid counterexamples when --smt-div is not given
function check_my_fuc() public {
    uint256 tt = svm.createUint256("A1");
    vm.assume(tt <= 0x01);
    storager.my_fuc(tt);
    assert(storager.retrieve() == 0x06); // no counterexample
}

}`

Next is the part where I modified the source code Result printing image

Where to modify the source code at _main function image

image

at my_run_sequential image image

at my_deploy_test image

this is my json

{ "0x008b3b2f992c0e14edaa6e2c662bec549caa8df1": { "balance": "0xc0415e7488259873cc", "nonce": 1 }, "0x1ba2bfaeca3827f9c5d4b9ad6a30b38eed03fec6": { "balance": "0x0", "code": "0x608060405234801561001057600080fd5b50600436106100415760003560e01c8063162acc71146100465780632e64cec1146100625780636057361d14610080575b600080fd5b610060600480360381019061005b9190610105565b61009c565b005b61006a6100b7565b6040516100779190610141565b60405180910390f35b61009a60048036038101906100959190610105565b6100c0565b005b806000808282546100ad919061018b565b9250508190555050565b60008054905090565b8060008190555050565b600080fd5b6000819050919050565b6100e2816100cf565b81146100ed57600080fd5b50565b6000813590506100ff816100d9565b92915050565b60006020828403121561011b5761011a6100ca565b5b6000610129848285016100f0565b91505092915050565b61013b816100cf565b82525050565b60006020820190506101566000830184610132565b92915050565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b6000610196826100cf565b91506101a1836100cf565b92508282019050808211156101b9576101b861015c565b5b9291505056fea264697066735822122081dd81f8c6eae3678a2372ea8c961df2b374ad69f2ba02d9bb7c8ff8d37cb71864736f6c63430008120033", "nonce": 1, "storage": { "0x0000000000000000000000000000000000000000000000000000000000000000": "0x0000000000000000000000000000000000000000000000000000000000000006" } }, "0xd2066ea52b771332d7ac95f30d3005b978e60229": { "balance": "0x55f8ef205d39b76c", "nonce": 109 } }

Bubblecqq commented 1 year ago

@daejunpark @karmacoma-eth If we want to customize the storage in the contract by modifying the source code to achieve the functionality of forking the mainnet, and at the same time, we are using Python to debug_trace the transactions, many of our codes cannot run in Solidity. They can only achieve our goals by modifying the source code of Halmos. Could you provide some ideas for modification? Thank you very much!

daejunpark commented 1 week ago

sorry for the delayed response. is this issue still relevant to your application? would this approach for fork testing work for you? https://github.com/a16z/halmos/wiki/FAQ#does-halmos-provide-support-for-mainnet-forking