Skip to content

Small fixes to kevm-pyk library #1462

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

Merged
merged 5 commits into from
Nov 23, 2022
Merged

Small fixes to kevm-pyk library #1462

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
4a400d7
kevm-pyk/kevm: correct klabel name
ehildenb Nov 23, 2022
6addde9
.github/solc_to_k: correct klabel usage
ehildenb Nov 23, 2022
38bcd7e
kevm-pyk/{kevm,solc-to-k}: correct some KTokens and fill in details
ehildenb Nov 5, 2022
f3b98ea
Merge remote-tracking branch 'upstream/master' into foundry-fixes
ehildenb Nov 23, 2022
2755643
kevm-pyk/solc_to_k: more KToken => KApply corrections
ehildenb Nov 23, 2022
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
14 changes: 13 additions & 1 deletion kevm-pyk/src/kevm_pyk/kevm.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -368,14 +368,26 @@ def _patch_symbol_table(symbol_table: Dict[str, Any]) -> None:

@staticmethod
def success(s: KInner, dst: KInner, r: KInner, c: KInner) -> KApply:
return KApply('foundry_success ', [s, dst, r, c])
return KApply('foundry_success', [s, dst, r, c])

@staticmethod
def fail(s: KInner, dst: KInner, r: KInner, c: KInner) -> KApply:
return notBool(Foundry.success(s, dst, r, c))

# address(uint160(uint256(keccak256("foundry default caller"))))

@staticmethod
def loc_FOUNDRY_FAILED() -> KApply: # noqa: N802
return KEVM.loc(
KApply(
'contract_access_field',
[
KApply('FoundryCheat_FOUNDRY-ACCOUNTS_FoundryContract'),
KApply('Failed_FOUNDRY-ACCOUNTS_FoundryField'),
],
)
)

@staticmethod
def address_CALLER() -> KToken: # noqa: N802
return intToken(0x1804C8AB1F12E6BBF3894D4083F33E07309D1F38)
Expand Down
34 changes: 11 additions & 23 deletions kevm-pyk/src/kevm_pyk/solc_to_k.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,17 +10,7 @@
from pyk.cterm import CTerm
from pyk.kast.inner import KApply, KAtt, KInner, KLabel, KRewrite, KSequence, KSort, KVariable, build_assoc
from pyk.kast.manip import abstract_term_safely, substitute
from pyk.kast.outer import (
KFlatModule,
KImport,
KNonTerminal,
KProduction,
KProductionItem,
KRule,
KSentence,
KTerminal,
KToken,
)
from pyk.kast.outer import KFlatModule, KImport, KNonTerminal, KProduction, KProductionItem, KRule, KSentence, KTerminal
from pyk.kcfg import KCFG
from pyk.prelude.kbool import FALSE, TRUE, andBool, notBool
from pyk.prelude.kint import intToken
Expand Down Expand Up @@ -337,11 +327,10 @@ def method_to_cfg(empty_config: KInner, contract: Contract, method: Contract.Met


def _init_cterm(init_term: KInner) -> CTerm:
key_dst = KEVM.loc(KToken('FoundryCheat . Failed', 'ContractAccess'))
dst_failed_prev = KEVM.lookup(KVariable('CHEATCODE_STORAGE'), key_dst)
dst_failed_prev = KEVM.lookup(KVariable('CHEATCODE_STORAGE'), Foundry.loc_FOUNDRY_FAILED())
init_cterm = CTerm(init_term)
init_cterm = KEVM.add_invariant(init_cterm)
init_cterm = init_cterm.add_constraint(mlEqualsTrue(KApply('_==Int_', [dst_failed_prev, KToken('0', 'Int')])))
init_cterm = init_cterm.add_constraint(mlEqualsTrue(KApply('_==Int_', [dst_failed_prev, intToken(0)])))
return init_cterm


Expand Down Expand Up @@ -389,10 +378,10 @@ def _init_term(
),
),
'LOCALMEM_CELL': KApply('.Memory_EVM-TYPES_Memory'),
'PREVCALLER_CELL': KToken('.Account', 'K'),
'PREVORIGIN_CELL': KToken('.Account', 'K'),
'NEWCALLER_CELL': KToken('.Account', 'K'),
'NEWORIGIN_CELL': KToken('.Account', 'K'),
'PREVCALLER_CELL': KApply('.Account_EVM-TYPES_Account'),
'PREVORIGIN_CELL': KApply('.Account_EVM-TYPES_Account'),
'NEWCALLER_CELL': KApply('.Account_EVM-TYPES_Account'),
'NEWORIGIN_CELL': KApply('.Account_EVM-TYPES_Account'),
'ACTIVE_CELL': FALSE,
'STATIC_CELL': FALSE,
'MEMORYUSED_CELL': intToken(0),
Expand All @@ -412,10 +401,10 @@ def _init_term(
'SINGLECALL_CELL': FALSE,
'EXPECTEDREVERT_CELL': FALSE,
'ISOPCODEEXPECTED_CELL': FALSE,
'EXPECTEDADDRESS_CELL': KToken('.Account', 'K'),
'EXPECTEDADDRESS_CELL': KApply('.Account_EVM-TYPES_Account'),
'EXPECTEDVALUE_CELL': intToken(0),
'EXPECTEDDATA_CELL': KToken('.ByteArray', 'K'),
'OPCODETYPE_CELL': KToken('.OpcodeType', 'K'),
'EXPECTEDDATA_CELL': KApply('.ByteArray_EVM-TYPES_ByteArray'),
'OPCODETYPE_CELL': KApply('.OpcodeType_FOUNDRY-CHEAT-CODES_OpcodeType'),
}

if calldata is not None:
Expand All @@ -429,8 +418,7 @@ def _init_term(

def _final_cterm(empty_config: KInner, contract_name: str, *, failing: bool, is_test: bool = True) -> CTerm:
final_term = _final_term(empty_config, contract_name)
key_dst = KEVM.loc(KToken('FoundryCheat . Failed', 'ContractAccess'))
dst_failed_post = KEVM.lookup(KVariable('CHEATCODE_STORAGE_FINAL'), key_dst)
dst_failed_post = KEVM.lookup(KVariable('CHEATCODE_STORAGE_FINAL'), Foundry.loc_FOUNDRY_FAILED())
foundry_success = Foundry.success(
KVariable('STATUSCODE_FINAL'),
dst_failed_post,
Expand Down