Support for missing EVM opcodes

[karmacoma-eth]

Opcodes to support:

• [x] CREATE (#21)
• [x] CREATE2 (#163)
• [x] DELEGATECALL (#159)
• [x] CALLCODE (#159)
• [ ] EXTCODECOPY
• [x] MSIZE (#38)
• [x] ADDMOD (#101)
• [x] MULMOD (#101)
• [x] SIGNEXTEND (#41)
• [ ] SELFDESTRUCT
• [x] INVALID (#60)

[distributedstatemachine]

I am not sure if this is related , but tried running halmos on our repo and got the following error:

Skipped Errors.json due to parsing failure: KeyError: 'metadata'
Skipped Token.json due to parsing failure: KeyError: 'metadata'
Skipped DiamondErrors.json due to parsing failure: KeyError: 'metadata'
Skipped LibNexusABI.json due to parsing failure: KeyError: 'metadata'
Skipped Create2Lib.json due to parsing failure: KeyError: 'metadata'

Running 5 tests for test/AssetReserves.t.sol:AssetReservesTest
Warning: setUp() execution encountered an issue at STATICCALL: Unsupported cheat code: calldata = 0xffa186490000000000000000000000000000000000000000000000000000000000000001
Error: setUp() failed: ValueError: No successful path found in setUp()
Symbolic test result: 0 passed; 5 failed; time: 0.02s

Running 5 tests for test/BridgeFacet.t.sol:BridgeFacetTest
Warning: setUp() execution encountered an issue at CALL: External call encountered an issue at DELEGATECALL: 
Error: setUp() failed: ValueError: No successful path found in setUp()
Symbolic test result: 0 passed; 5 failed; time: 0.90s

Running 3 tests for test/HyperlaneAdapter.t.sol:HyperlaneAdapterTest
[FAIL] test_handle_Access() (paths: 0/2, time: 0.10s, bounds: [])
Not supported: CALL: Unsupported cheat code: calldata = 0xc31eb0e070fcdd1d00000000000000000000000000000000000000000000000000000000
[FAIL] test_relayMessage_Access() (paths: 0/2, time: 0.10s, bounds: [])
Not supported: CALL: Unsupported cheat code: calldata = 0xc31eb0e02f6cf8e800000000000000000000000000000000000000000000000000000000
[FAIL] test_relayMessage_handle() (paths: 0/2, time: 0.88s, bounds: [])
Not supported: CALL: Unsupported cheat code: calldata = 0x86b9620d00000000000000000000000000000000000000000000000000000000aaaa0007
Symbolic test result: 0 passed; 3 failed; time: 1.41s

Running 3 tests for test/InterchainLiquidity.t.sol:InterchainLiquidityHubWrapperTest
Warning: setUp() execution encountered an issue at CALL: Unsupported cheat code: calldata = 0x266cf109
Error: setUp() failed: ValueError: No successful path found in setUp()
Symbolic test result: 0 passed; 3 failed; time: 5.57s

Running 6 tests for test/KaiLiquidityAggregator.t.sol:KaiLiquidityAggregatorTest
Warning: setUp() execution encountered an issue at STATICCALL: Unsupported cheat code: calldata = 0xffa186490000000000000000000000000000000000000000000000000000000000000001
Error: setUp() failed: ValueError: No successful path found in setUp()
Symbolic test result: 0 passed; 6 failed; time: 0.03s

Running 5 tests for test/LiquidityAggregator.t.sol:LiquidityAggregatorTest
Warning: setUp() execution encountered an issue at STATICCALL: Unsupported cheat code: calldata = 0xffa186490000000000000000000000000000000000000000000000000000000000000001
Error: setUp() failed: ValueError: No successful path found in setUp()
Symbolic test result: 0 passed; 5 failed; time: 0.02s

Running 4 tests for test/LiquidityProjector.t.sol:LiquidityProjectorTest
Warning: setUp() execution encountered an issue at STATICCALL: Unsupported cheat code: calldata = 0xffa186490000000000000000000000000000000000000000000000000000000000000001
Error: setUp() failed: ValueError: No successful path found in setUp()
Symbolic test result: 0 passed; 4 failed; time: 0.02s

[karmacoma-eth]

@samtvlabs you are running into multiple missing cheatcodes:

0xffa18649 is vm.addr(uint256) (see https://github.com/a16z/halmos/issues/149) 0xc31eb0e0 is vm.expectRevert(bytes4) 0x266cf109 is vm.record() 0x86b9620d is expectEmit(address)

and also into DELEGATECALL, which hasn't been implemented yet

[QGarchery]

Would it makes sense to implementing the functionality to revert to previous snapshots ? This is very useful in tests, to compare effect on storage of 2 different functions/code, but I'm not sure how feasible it is to add that to Halmos.

0x9711715a is the signature of vm.snapshot() 0x44d7f0a4 is the signature of vm.revertTo(uint256)