Skip to content

Commit

Permalink
Pretty print function arguments in calldata (#878)
Browse files Browse the repository at this point in the history 
* remove abstract_term calls

* update expected output

* update symboliv argument prefix

* update expected output

* update expected output cse
  • Loading branch information
@anvacaru
anvacaru authored Nov 8, 2024
1 parent dca7853 commit a8beada
Show file tree
Hide file tree
Showing 30 changed files with 18,107 additions and 4,027 deletions.
21 changes: 5 additions & 16 deletions src/kontrol/solc_to_k.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,6 @@
from kevm_pyk.kevm import KEVM
from pyk.kast.att import Atts, KAtt
from pyk.kast.inner import KApply, KLabel, KRewrite, KSort, KVariable
from pyk.kast.manip import abstract_term_safely
from pyk.kast.outer import KDefinition, KFlatModule, KImport, KNonTerminal, KProduction, KRequire, KRule, KTerminal
from pyk.kdist import kdist
from pyk.prelude.kbool import TRUE, andBool
Expand Down Expand Up @@ -77,7 +76,8 @@ class Input:

@cached_property
def arg_name(self) -> str:
return f'V{self.idx}_{self.name.replace("-", "_")}'
prefix = f'KV{self.idx}_' if self.name and self.name[0].isalpha() else f'KV{self.idx}'
return f'{prefix}{self.name}'

@staticmethod
def from_dict(input: dict, idx: int = 0, natspec_lengths: dict | None = None) -> Input:
Expand Down Expand Up @@ -425,11 +425,7 @@ def digest(self) -> str:

@cached_property
def callvalue_cell(self) -> KInner:
return (
intToken(0)
if not self.payable
else abstract_term_safely(KVariable('_###CALLVALUE###_'), base_name='CALLVALUE')
)
return intToken(0) if not self.payable else KVariable('CALLVALUE')

def encoded_args(self, enums: dict[str, int]) -> tuple[KInner, list[KInner]]:
args: list[KInner] = []
Expand Down Expand Up @@ -742,11 +738,7 @@ def rule(

@cached_property
def callvalue_cell(self) -> KInner:
return (
intToken(0)
if not self.payable
else abstract_term_safely(KVariable('_###CALLVALUE###_'), base_name='CALLVALUE')
)
return intToken(0) if not self.payable else KVariable('CALLVALUE')

def calldata_cell(self, contract: Contract) -> KInner:
return KApply(contract.klabel_method, [KApply(contract.klabel), self.application])
Expand All @@ -755,10 +747,7 @@ def calldata_cell(self, contract: Contract) -> KInner:
def application(self) -> KInner:
klabel = self.klabel
assert klabel is not None
args = [
abstract_term_safely(KVariable('_###SOLIDITY_ARG_VAR###_'), base_name=f'V{name}')
for name in self.arg_names
]
args = [KVariable(name) for name in self.arg_names]
return klabel(args)

_name: str
Expand Down
30 changes: 15 additions & 15 deletions src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@
┃ (branch)
┣━━┓ subst: .Subst
┃ ┃ constraint:
┃ ┃ VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) )
┃ ┃ KV0_x:Int <=Int ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) )
┃ │
┃ ├─ 8
┃ │ k: #execute ~> CONTINUATION:K
Expand Down Expand Up @@ -42,7 +42,7 @@
┃
┗━━┓ subst: .Subst
┃ constraint:
┃ ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) <Int VV0_x_114b9705:Int
┃ ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) <Int KV0_x:Int
│
├─ 9
│ k: #execute ~> CONTINUATION:K
Expand Down Expand Up @@ -96,7 +96,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
<ethereum>
<evm>
<output>
( _OUTPUT_CELL => #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) ) )
( _OUTPUT_CELL => #buf ( 32 , ( KV0_x:Int +Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) ) )
</output>
<statusCode>
( _STATUSCODE => EVMC_SUCCESS )
Expand All @@ -109,7 +109,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
CALLER_ID:Int
</caller>
<callData>
b"i\xab\xff\xa1" +Bytes #buf ( 32 , VV0_x_114b9705:Int )
b"i\xab\xff\xa1" +Bytes #buf ( 32 , KV0_x:Int )
</callData>
<callValue>
0
Expand All @@ -118,7 +118,7 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
( .WordStack => ( selector ( "applyOp(uint256)" ) : .WordStack ) )
</wordStack>
<localMem>
( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( VV0_x_114b9705:Int +Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) ) )
( b"" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( KV0_x:Int +Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) ) )
</localMem>
<memoryUsed>
0
Expand Down Expand Up @@ -228,11 +228,11 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
</traceData>
</KEVMTracing>
</foundry>
requires ( 0 <=Int CALLER_ID:Int
requires ( 0 <=Int KV0_x:Int
andBool ( 0 <=Int CALLER_ID:Int
andBool ( 0 <=Int ORIGIN_ID:Int
andBool ( 0 <=Int C_ADDCONST_ID:Int
andBool ( 0 <=Int C_ADDCONST_BAL:Int
andBool ( 0 <=Int VV0_x_114b9705:Int
andBool ( 0 <=Int C_ADDCONST_NONCE:Int
andBool ( pow24 <Int NUMBER_CELL:Int
andBool ( NUMBER_CELL:Int <Int pow32
Expand All @@ -245,15 +245,15 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
andBool ( CALLER_ID:Int <Int pow160
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( C_ADDCONST_ID:Int <Int pow160
andBool ( KV0_x:Int <Int pow256
andBool ( C_ADDCONST_BAL:Int <Int pow256
andBool ( VV0_x_114b9705:Int <Int pow256
andBool ( ( notBool <acctID>
C_ADDCONST_ID:Int
</acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < C_ADDCONST_ID:Int <= 9 ) )
andBool ( VV0_x_114b9705:Int <=Int ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) )
andBool ( KV0_x:Int <=Int ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) )
))))))))))))))))))))))))
[priority(20), label(BASIC-BLOCK-8-TO-6)]

Expand Down Expand Up @@ -288,13 +288,13 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
CALLER_ID:Int
</caller>
<callData>
b"i\xab\xff\xa1" +Bytes #buf ( 32 , VV0_x_114b9705:Int )
b"i\xab\xff\xa1" +Bytes #buf ( 32 , KV0_x:Int )
</callData>
<callValue>
0
</callValue>
<wordStack>
( .WordStack => ( 0 : ( VV0_x_114b9705:Int : ( #lookup ( C_ADDCONST_STORAGE:Map , 0 ) : ( 118 : ( 0 : ( VV0_x_114b9705:Int : ( 70 : ( selector ( "applyOp(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) )
( .WordStack => ( 0 : ( KV0_x:Int : ( #lookup ( C_ADDCONST_STORAGE:Map , 0 ) : ( 118 : ( 0 : ( KV0_x:Int : ( 70 : ( selector ( "applyOp(uint256)" ) : .WordStack ) ) ) ) ) ) ) ) )
</wordStack>
<localMem>
( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x11\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
Expand Down Expand Up @@ -407,11 +407,11 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
</traceData>
</KEVMTracing>
</foundry>
requires ( 0 <=Int CALLER_ID:Int
requires ( 0 <=Int KV0_x:Int
andBool ( 0 <=Int CALLER_ID:Int
andBool ( 0 <=Int ORIGIN_ID:Int
andBool ( 0 <=Int C_ADDCONST_ID:Int
andBool ( 0 <=Int C_ADDCONST_BAL:Int
andBool ( 0 <=Int VV0_x_114b9705:Int
andBool ( 0 <=Int C_ADDCONST_NONCE:Int
andBool ( pow24 <Int NUMBER_CELL:Int
andBool ( NUMBER_CELL:Int <Int pow32
Expand All @@ -424,15 +424,15 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
andBool ( CALLER_ID:Int <Int pow160
andBool ( ORIGIN_ID:Int <Int pow160
andBool ( C_ADDCONST_ID:Int <Int pow160
andBool ( KV0_x:Int <Int pow256
andBool ( C_ADDCONST_BAL:Int <Int pow256
andBool ( VV0_x_114b9705:Int <Int pow256
andBool ( ( notBool <acctID>
C_ADDCONST_ID:Int
</acctID> in_keys ( ACCOUNTS_REST:AccountCellMap ) )
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < C_ADDCONST_ID:Int <= 9 ) )
andBool ( ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) <Int VV0_x_114b9705:Int
andBool ( ( maxUInt256 -Int #lookup ( C_ADDCONST_STORAGE:Map , 0 ) ) <Int KV0_x:Int
))))))))))))))))))))))))
[priority(20), label(BASIC-BLOCK-9-TO-7)]

Expand Down
Loading

0 comments on commit a8beada

Please sign in to comment.