Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add a test for etch to a symbolic address #844

Open
wants to merge 9 commits into
base: master
Choose a base branch
from
Open

Add a test for etch to a symbolic address #844

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
2a58e7b
Add a test for `etch` to symbolic address
palinatolmach Oct 1, 2024
b345b39
Merge branch 'master' into symbolic-etch-test
palinatolmach Oct 1, 2024
5925207
Update expected output
palinatolmach Oct 1, 2024
4f66240
Update `AccountParamsTest` function names
palinatolmach Oct 1, 2024
0621b42
Add symbolic address assumption to `testEtchSymbolicAddress`
palinatolmach Oct 2, 2024
fe30cb4
Update trace expected output
palinatolmach Oct 2, 2024
038983e
Merge branch 'master' into symbolic-etch-test
palinatolmach Oct 7, 2024
023e6ba
Merge branch 'master' into symbolic-etch-test
PetarMax Oct 10, 2024
f5ee2c2
Merge branch 'master' into symbolic-etch-test
ehildenb Oct 15, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/tests/integration/test-data/foundry-prove-all
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
AccountParamsTest.testDealConcrete()
AccountParamsTest.testDealSymbolic(uint256)
AccountParamsTest.testEtchConcrete()
AccountParamsTest.testEtchSymbolic(bytes)
AccountParamsTest.testEtchConcreteCode()
AccountParamsTest.testEtchSymbolicAddress()
AccountParamsTest.testEtchSymbolicCode(bytes)
AccountParamsTest.testFail_GetNonce_false()
AccountParamsTest.testFail_GetNonce_true()
AccountParamsTest.test_GetNonce_false()
Expand Down
5 changes: 3 additions & 2 deletions src/tests/integration/test-data/foundry-prove-skip-legacy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
AccountParamsTest.testDealConcrete()
AccountParamsTest.testDealSymbolic(uint256)
AccountParamsTest.testEtchConcrete()
AccountParamsTest.testEtchSymbolic(bytes)
AccountParamsTest.testEtchConcreteCode()
AccountParamsTest.testEtchSymbolicAddress()
AccountParamsTest.testEtchSymbolicCode(bytes)
AccountParamsTest.testFail_GetNonce_false()
AccountParamsTest.testFail_GetNonce_true()
AccountParamsTest.test_GetNonce_false()
Expand Down
25 changes: 22 additions & 3 deletions src/tests/integration/test-data/foundry/test/AccountParamsTest.t.sol
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,15 @@
pragma solidity =0.8.13;

import "forge-std/Test.sol";
import "kontrol-cheatcodes/KontrolCheats.sol";

contract AccountParamsTest is Test {
contract EtchTest {
function testEtch() public pure returns (bool) {
return true;
}
}

contract AccountParamsTest is Test, KontrolCheats {
function testDealConcrete() public {
vm.deal(address(505), 256);
assertEq(address(505).balance, 256);
Expand All @@ -15,17 +21,30 @@ contract AccountParamsTest is Test {
assertEq(address(328).balance, value);
}

function testEtchConcrete() public {
function testEtchConcreteCode() public {
bytes memory code = bytes("this should be EVM bytecode");
vm.etch(address(124), code);
assertEq(address(124).code, code);
}

function testEtchSymbolic(bytes calldata code) public {
function testEtchSymbolicCode(bytes calldata code) public {
vm.etch(address(124), code);
assertEq(address(124).code, code);
}

function testEtchSymbolicAddress() public {
address etchAddr = kevm.freshAddress();
// `etchAddr` is not 0 or precompiled address
vm.assume(etchAddr > address(9));

bytes memory etchCode = bytes(hex"6080604052348015600f57600080fd5b506004361060285760003560e01c80631a9f8ff714602d575b600080fd5b604080516001815290519081900360200190f3fea2646970667358221220c2310c11ffdfaaecbc61aff49cac6de28e626e3aef1fcf4857565c0e6a87715c64736f6c634300080d0033");

vm.etch(etchAddr, etchCode);

bool result = EtchTest(etchAddr).testEtch();
assertTrue(result);
}

function testNonceSymbolic(uint64 newNonce) public {
uint64 oldNonce = vm.getNonce(address(this));
vm.assume(newNonce > oldNonce);
Expand Down
5 changes: 3 additions & 2 deletions src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected
View file
Open in desktop

Large diffs are not rendered by default.

47 changes: 41 additions & 6 deletions src/tests/integration/test-data/show/contracts.k.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,8 @@ module S2KtestZModAccountParamsTest-CONTRACT

syntax S2KtestZModAccountParamsTestMethod ::= "S2Kfailed" "(" ")" [symbol("method_test%AccountParamsTest_S2Kfailed_")]

syntax S2KtestZModAccountParamsTestMethod ::= "S2Kkevm" "(" ")" [symbol("method_test%AccountParamsTest_S2Kkevm_")]

syntax S2KtestZModAccountParamsTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol("method_test%AccountParamsTest_S2KtargetArtifactSelectors_")]

syntax S2KtestZModAccountParamsTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol("method_test%AccountParamsTest_S2KtargetArtifacts_")]
Expand All @@ -52,9 +54,11 @@ module S2KtestZModAccountParamsTest-CONTRACT

syntax S2KtestZModAccountParamsTestMethod ::= "S2KtestDealSymbolic" "(" Int ":" "uint256" ")" [symbol("method_test%AccountParamsTest_S2KtestDealSymbolic_uint256")]

syntax S2KtestZModAccountParamsTestMethod ::= "S2KtestEtchConcrete" "(" ")" [symbol("method_test%AccountParamsTest_S2KtestEtchConcrete_")]
syntax S2KtestZModAccountParamsTestMethod ::= "S2KtestEtchConcreteCode" "(" ")" [symbol("method_test%AccountParamsTest_S2KtestEtchConcreteCode_")]

syntax S2KtestZModAccountParamsTestMethod ::= "S2KtestEtchSymbolicAddress" "(" ")" [symbol("method_test%AccountParamsTest_S2KtestEtchSymbolicAddress_")]

syntax S2KtestZModAccountParamsTestMethod ::= "S2KtestEtchSymbolic" "(" Bytes ":" "bytes" ")" [symbol("method_test%AccountParamsTest_S2KtestEtchSymbolic_bytes")]
syntax S2KtestZModAccountParamsTestMethod ::= "S2KtestEtchSymbolicCode" "(" Bytes ":" "bytes" ")" [symbol("method_test%AccountParamsTest_S2KtestEtchSymbolicCode_bytes")]

syntax S2KtestZModAccountParamsTestMethod ::= "S2KtestFailZUndGetNonceZUndfalse" "(" ")" [symbol("method_test%AccountParamsTest_S2KtestFailZUndGetNonceZUndfalse_")]

Expand Down Expand Up @@ -87,6 +91,9 @@ module S2KtestZModAccountParamsTest-CONTRACT
rule ( S2KtestZModAccountParamsTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) )


rule ( S2KtestZModAccountParamsTest . S2Kkevm ( ) => #abiCallData ( "kevm" , .TypedArgs ) )


rule ( S2KtestZModAccountParamsTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) )


Expand All @@ -109,10 +116,13 @@ module S2KtestZModAccountParamsTest-CONTRACT
ensures #rangeUInt ( 256 , V0_value )


rule ( S2KtestZModAccountParamsTest . S2KtestEtchConcrete ( ) => #abiCallData ( "testEtchConcrete" , .TypedArgs ) )
rule ( S2KtestZModAccountParamsTest . S2KtestEtchConcreteCode ( ) => #abiCallData ( "testEtchConcreteCode" , .TypedArgs ) )


rule ( S2KtestZModAccountParamsTest . S2KtestEtchSymbolicAddress ( ) => #abiCallData ( "testEtchSymbolicAddress" , .TypedArgs ) )


rule ( S2KtestZModAccountParamsTest . S2KtestEtchSymbolic ( V0_code : bytes ) => #abiCallData ( "testEtchSymbolic" , ( #bytes ( V0_code ) , .TypedArgs ) ) )
rule ( S2KtestZModAccountParamsTest . S2KtestEtchSymbolicCode ( V0_code : bytes ) => #abiCallData ( "testEtchSymbolicCode" , ( #bytes ( V0_code ) , .TypedArgs ) ) )
ensures #rangeUInt ( 64 , lengthBytes ( V0_code ) )


Expand Down Expand Up @@ -157,6 +167,9 @@ module S2KtestZModAccountParamsTest-CONTRACT
rule ( selector ( "failed()" ) => 3124842406 )


rule ( selector ( "kevm()" ) => 3601001590 )


rule ( selector ( "targetArtifactSelectors()" ) => 1725540768 )


Expand All @@ -178,10 +191,13 @@ module S2KtestZModAccountParamsTest-CONTRACT
rule ( selector ( "testDealSymbolic(uint256)" ) => 2584982624 )


rule ( selector ( "testEtchConcrete()" ) => 807503996 )
rule ( selector ( "testEtchConcreteCode()" ) => 1609952251 )


rule ( selector ( "testEtchSymbolic(bytes)" ) => 2109411263 )
rule ( selector ( "testEtchSymbolicAddress()" ) => 4275836419 )


rule ( selector ( "testEtchSymbolicCode(bytes)" ) => 2871126377 )


rule ( selector ( "testFail_GetNonce_false()" ) => 2393877859 )
Expand All @@ -208,6 +224,25 @@ module S2KtestZModAccountParamsTest-CONTRACT
rule ( selector ( "test_getNonce_unknownSymbolic(address)" ) => 3941547284 )


endmodule

module S2KtestZModEtchTest-CONTRACT
imports public FOUNDRY

syntax Contract ::= S2KtestZModEtchTestContract

syntax S2KtestZModEtchTestContract ::= "S2KtestZModEtchTest" [symbol("contract_test%EtchTest")]

syntax Bytes ::= S2KtestZModEtchTestContract "." S2KtestZModEtchTestMethod [function, symbol("method_test%EtchTest")]

syntax S2KtestZModEtchTestMethod ::= "S2KtestEtch" "(" ")" [symbol("method_test%EtchTest_S2KtestEtch_")]

rule ( S2KtestZModEtchTest . S2KtestEtch ( ) => #abiCallData ( "testEtch" , .TypedArgs ) )


rule ( selector ( "testEtch()" ) => 446664695 )


endmodule

module S2KtestZModAddrTest-CONTRACT
Expand Down
8 changes: 8 additions & 0 deletions src/tests/integration/test-data/show/foundry.k.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@ requires "requires/no_stack_checks.md"
module FOUNDRY-MAIN
imports public S2KsrcZModduplicatesZMod2ZModDuplicateName-VERIFICATION
imports public S2KtestZModAccountParamsTest-VERIFICATION
imports public S2KtestZModEtchTest-VERIFICATION
imports public S2KtestZModAddrTest-VERIFICATION
imports public S2KtestZModAllowChangesTest-VERIFICATION
imports public S2KtestZModValueStore-VERIFICATION
Expand Down Expand Up @@ -188,6 +189,13 @@ module S2KtestZModAccountParamsTest-VERIFICATION



endmodule

module S2KtestZModEtchTest-VERIFICATION
imports public S2KtestZModEtchTest-CONTRACT



endmodule

module S2KtestZModAddrTest-VERIFICATION
Expand Down
Loading