Skip to content

Commit eff7310

Browse files
Th0rgalTh0rgal
authored
Add ABI frame lowering layers
Squash merge PR #1947 after review: CI green. The prior returnCodeData underflow finding is stale; current code guards extcodesize before subtracting the code offset.
1 parent ae61860 commit eff7310

28 files changed

Lines changed: 921 additions & 22 deletions

‎Compiler/ABI/Frame.lean‎

Lines changed: 226 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,226 @@
1+
import Compiler.CompilationModel.AbiTypeLayout
2+
import Compiler.Yul.Ast
3+
4+
namespace Compiler.ABI.Frame
5+
6+
open Compiler.CompilationModel
7+
open Compiler.Yul
8+
9+
inductive FrameSource
10+
| calldata
11+
| memory
12+
| code
13+
| storage
14+
deriving Repr, BEq
15+
16+
inductive FramePassMode
17+
| inlineWords
18+
| pointer
19+
deriving Repr, BEq
20+
21+
structure FrameField where
22+
name : String
23+
ty : ParamType
24+
source : FrameSource
25+
sourceBase : String := ""
26+
sourceOffset : Nat := 0
27+
tailBytes : Nat := 0
28+
deriving Repr, BEq
29+
30+
structure FrameLayout where
31+
fields : List FrameField
32+
headWords : Nat
33+
hasDynamic : Bool
34+
mode : FramePassMode
35+
deriving Repr, BEq
36+
37+
def spillThresholdWords : Nat := 4
38+
39+
def fieldHeadWords (field : FrameField) : Nat :=
40+
paramParentHeadWords field.ty
41+
42+
def fieldsHeadWords (fields : List FrameField) : Nat :=
43+
fields.foldl (fun acc field => acc + fieldHeadWords field) 0
44+
45+
def fieldsHaveDynamic (fields : List FrameField) : Bool :=
46+
fields.any (fun field => isDynamicParamType field.ty)
47+
48+
def shouldPassByPointer (fields : List FrameField) : Bool :=
49+
fields.any (fun field => field.source == .code) ||
50+
fieldsHaveDynamic fields || spillThresholdWords < fieldsHeadWords fields
51+
52+
def layout (fields : List FrameField) : FrameLayout :=
53+
let headWords := fieldsHeadWords fields
54+
let hasDynamic := fieldsHaveDynamic fields
55+
{ fields
56+
headWords
57+
hasDynamic
58+
mode := if shouldPassByPointer fields then .pointer else .inlineWords }
59+
60+
def fieldSourceSupported (field : FrameField) : Bool :=
61+
match field.source with
62+
| .memory | .code | .storage => true
63+
| .calldata => true
64+
65+
def fieldLayoutSupported (field : FrameField) : Bool :=
66+
fieldSourceSupported field &&
67+
!isDynamicParamType field.ty
68+
69+
def layoutSourcesSupported (l : FrameLayout) : Bool :=
70+
l.fields.all fieldLayoutSupported
71+
72+
def dynamicTailWords (field : FrameField) : Nat :=
73+
1 + (field.tailBytes + 31) / 32
74+
75+
def fieldPayloadWords (field : FrameField) : Nat :=
76+
fieldHeadWords field + if isDynamicParamType field.ty then dynamicTailWords field else 0
77+
78+
def frameSizeBytes (l : FrameLayout) : Nat :=
79+
l.fields.foldl (fun acc field => acc + fieldPayloadWords field * 32) 0
80+
81+
def frameAllocBytes (l : FrameLayout) : Nat :=
82+
l.fields.foldl (fun acc field => acc + fieldPayloadWords field * 32) 0
83+
84+
def ptrName (base : String) : String :=
85+
"__abi_frame_" ++ base
86+
87+
def fieldWordName (base : String) (field : FrameField) (idx : Nat) : String :=
88+
ptrName base ++ "_" ++ field.name ++ "_" ++ toString idx
89+
90+
def allocateFrame (base : String) (l : FrameLayout) : List YulStmt :=
91+
[ YulStmt.let_ (ptrName base) (YulExpr.call "mload" [YulExpr.lit 64])
92+
, YulStmt.expr (YulExpr.call "mstore"
93+
[ YulExpr.lit 64
94+
, YulExpr.call "add" [YulExpr.ident (ptrName base), YulExpr.lit (frameAllocBytes l)] ])]
95+
96+
def sourceBaseName (field : FrameField) : String :=
97+
if field.sourceBase.isEmpty then field.name else field.sourceBase
98+
99+
private def sourceByteOffset (field : FrameField) (idx : Nat) : YulExpr :=
100+
let byteOffset := field.sourceOffset + idx * 32
101+
if byteOffset == 0 then
102+
YulExpr.ident (sourceBaseName field)
103+
else
104+
YulExpr.call "add" [YulExpr.ident (sourceBaseName field), YulExpr.lit byteOffset]
105+
106+
private def sourceCodeOffset (field : FrameField) (idx : Nat) : YulExpr :=
107+
YulExpr.lit (field.sourceOffset + idx * 32)
108+
109+
private def sourceStorageSlot (field : FrameField) (idx : Nat) : YulExpr :=
110+
if idx == 0 then
111+
YulExpr.ident (sourceBaseName field)
112+
else
113+
YulExpr.call "add" [YulExpr.ident (sourceBaseName field), YulExpr.lit idx]
114+
115+
private def dynamicTailByteOffset (field : FrameField) (idx : Nat) : YulExpr :=
116+
let wordOffset := YulExpr.lit (idx * 32)
117+
match field.source with
118+
| .calldata =>
119+
let head := sourceByteOffset field 0
120+
let base := YulExpr.ident (sourceBaseName field)
121+
YulExpr.call "add" [YulExpr.call "add" [base, YulExpr.call "calldataload" [head]], wordOffset]
122+
| .memory =>
123+
let head := sourceByteOffset field 0
124+
let base := YulExpr.ident (sourceBaseName field)
125+
YulExpr.call "add" [YulExpr.call "add" [base, YulExpr.call "mload" [head]], wordOffset]
126+
| .code => YulExpr.lit (field.sourceOffset + idx * 32)
127+
| .storage => sourceStorageSlot field idx
128+
129+
private def materializeSourceWord (field : FrameField) (idx : Nat) : YulExpr :=
130+
match field.source with
131+
| .calldata => YulExpr.call "calldataload" [sourceByteOffset field idx]
132+
| .memory => YulExpr.call "mload" [sourceByteOffset field idx]
133+
| .code => YulExpr.call "mload" [YulExpr.lit 0]
134+
| .storage => YulExpr.call "sload" [sourceStorageSlot field idx]
135+
136+
private def spillCodeWord (field : FrameField) (dest offset : YulExpr) : YulStmt :=
137+
YulStmt.expr (YulExpr.call "extcodecopy"
138+
[ YulExpr.ident (sourceBaseName field), dest, offset, YulExpr.lit 32 ])
139+
140+
private def spillStaticField (base : String) (headOffsetWords : Nat) (field : FrameField) : List YulStmt :=
141+
(List.range (fieldHeadWords field)).map fun idx =>
142+
let dest := YulExpr.call "add" [YulExpr.ident (ptrName base), YulExpr.lit ((headOffsetWords + idx) * 32)]
143+
match field.source with
144+
| .code => spillCodeWord field dest (sourceCodeOffset field idx)
145+
| _ =>
146+
YulStmt.expr (YulExpr.call "mstore"
147+
[dest, materializeSourceWord field idx])
148+
149+
private def spillDynamicField (base : String) (headOffsetWords tailOffsetWords : Nat) (field : FrameField) : List YulStmt :=
150+
let tailOffsetBytes := tailOffsetWords * 32
151+
let headDest := YulExpr.call "add" [YulExpr.ident (ptrName base), YulExpr.lit (headOffsetWords * 32)]
152+
let head := [YulStmt.expr (YulExpr.call "mstore" [headDest, YulExpr.lit tailOffsetBytes])]
153+
let tailWords := dynamicTailWords field
154+
head ++ (List.range tailWords).map fun idx =>
155+
let dest := YulExpr.call "add" [YulExpr.ident (ptrName base), YulExpr.lit ((tailOffsetWords + idx) * 32)]
156+
match field.source with
157+
| .code => spillCodeWord field dest (dynamicTailByteOffset field idx)
158+
| .storage =>
159+
YulStmt.expr (YulExpr.call "mstore"
160+
[dest, YulExpr.call "sload" [dynamicTailByteOffset field idx]])
161+
| .calldata =>
162+
YulStmt.expr (YulExpr.call "mstore"
163+
[dest, YulExpr.call "calldataload" [dynamicTailByteOffset field idx]])
164+
| .memory =>
165+
YulStmt.expr (YulExpr.call "mstore"
166+
[dest, YulExpr.call "mload" [dynamicTailByteOffset field idx]])
167+
168+
partial def spillFieldsAbi (base : String) (headOffsetWords tailOffsetWords : Nat) : List FrameField → List YulStmt
169+
| [] => []
170+
| field :: rest =>
171+
let headWords := fieldHeadWords field
172+
if isDynamicParamType field.ty then
173+
spillDynamicField base headOffsetWords tailOffsetWords field ++
174+
spillFieldsAbi base (headOffsetWords + headWords) (tailOffsetWords + dynamicTailWords field) rest
175+
else
176+
spillStaticField base headOffsetWords field ++
177+
spillFieldsAbi base (headOffsetWords + headWords) tailOffsetWords rest
178+
179+
/-- Materialize a typed ABI frame into memory before lowering calls/logs/returns.
180+
Large or dynamic payloads are then passed as `(ptr, size)` instead of as a
181+
long list of Yul values. -/
182+
def spillPayloadToMemory (base : String) (l : FrameLayout) : List YulStmt :=
183+
allocateFrame base l ++ spillFieldsAbi base 0 l.headWords l.fields
184+
185+
def pointerArgs (base : String) (l : FrameLayout) : List YulExpr :=
186+
[YulExpr.ident (ptrName base), YulExpr.lit (frameSizeBytes l)]
187+
188+
def inlinePayloadToScratch (words : List YulExpr) : List YulStmt :=
189+
words.zipIdx.map fun (word, idx) =>
190+
YulStmt.expr (YulExpr.call "mstore" [YulExpr.lit (idx * 32), word])
191+
192+
private partial def inlineArgsFrom : List FrameField → List YulExpr
193+
| [] => []
194+
| field :: rest =>
195+
(List.range (fieldHeadWords field)).map (fun wordIdx =>
196+
materializeSourceWord field wordIdx) ++
197+
inlineArgsFrom rest
198+
199+
def inlineArgs (l : FrameLayout) : List YulExpr :=
200+
inlineArgsFrom l.fields
201+
202+
def loweredArgs (base : String) (l : FrameLayout) : List YulExpr :=
203+
match l.mode with
204+
| .pointer => pointerArgs base l
205+
| .inlineWords => inlineArgs l
206+
207+
def materializePayloadToMemory (base : String) (l : FrameLayout) : List YulStmt × List YulExpr :=
208+
match l.mode with
209+
| .pointer =>
210+
(spillPayloadToMemory base l, pointerArgs base l)
211+
| .inlineWords =>
212+
(inlinePayloadToScratch (inlineArgs l), [YulExpr.lit 0, YulExpr.lit (frameSizeBytes l)])
213+
214+
def containsDynamicArrayOrBytes (l : FrameLayout) : Bool :=
215+
l.fields.any fun field =>
216+
match field.ty with
217+
| .array _ | .bytes | .string => true
218+
| _ => isDynamicParamType field.ty
219+
220+
def supportsNestedStructs (l : FrameLayout) : Bool :=
221+
l.fields.any fun field =>
222+
match field.ty with
223+
| .tuple elems => elems.any (fun ty => match ty with | .tuple _ => true | _ => false)
224+
| _ => false
225+
226+
end Compiler.ABI.Frame

‎Compiler/ABI/FrameTest.lean‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
import Compiler.ABI.Frame
2+
3+
namespace Compiler.ABI.FrameTest
4+
5+
open Compiler.ABI.Frame
6+
open Compiler.CompilationModel
7+
open Compiler.Yul
8+
9+
private def assert (label : String) (ok : Bool) : IO Unit := do
10+
if !ok then
11+
throw (IO.userError s!"frame test failed: {label}")
12+
IO.println s!"ok: {label}"
13+
14+
private def takeFields : List FrameField :=
15+
[ { name := "offer", ty := .tuple [.address, .uint256, .tuple [.bytes32, .uint256]], source := .calldata }
16+
, { name := "units", ty := .uint256, source := .calldata }
17+
, { name := "ratifierData", ty := .bytes, source := .calldata, tailBytes := 96 } ]
18+
19+
private def sourceFields : List FrameField :=
20+
[ { name := "c", ty := .uint256, source := .calldata }
21+
, { name := "m", ty := .bytes32, source := .memory }
22+
, { name := "x", ty := .bytes32, source := .code }
23+
, { name := "s", ty := .uint256, source := .storage } ]
24+
25+
private def inlineFields : List FrameField :=
26+
[ { name := "pair", ty := .tuple [.uint256, .bytes32], source := .calldata }
27+
, { name := "amount", ty := .uint256, source := .calldata } ]
28+
29+
private def dynamicStorageFields : List FrameField :=
30+
[ { name := "blob", ty := .bytes, source := .storage, tailBytes := 64 } ]
31+
32+
private def dynamicMemoryFields : List FrameField :=
33+
[ { name := "payload", ty := .bytes, source := .memory, sourceOffset := 32, tailBytes := 64 } ]
34+
35+
private def unpaddedDynamicFields : List FrameField :=
36+
[ { name := "payload", ty := .bytes, source := .calldata, tailBytes := 33 } ]
37+
38+
private def calldataLoadName? : YulExpr → Option String
39+
| .call "calldataload" [.ident name] => some name
40+
| .call "calldataload" [.call "add" [.ident name, _]] => some name
41+
| _ => none
42+
43+
private def hasExtcodecopy : List YulStmt → Bool :=
44+
fun stmts => stmts.any fun
45+
| .expr (.call "extcodecopy" _) => true
46+
| _ => false
47+
48+
#eval! do
49+
let takeLayout := layout takeFields
50+
assert "nested struct supported" (supportsNestedStructs takeLayout)
51+
assert "dynamic bytes/arrays force pointer mode" (takeLayout.mode == FramePassMode.pointer)
52+
assert "Take frame passes pointer pair" ((loweredArgs "take" takeLayout).length == 2)
53+
assert "dynamic tail contributes to pointer payload size" (frameSizeBytes takeLayout == 320)
54+
assert "dynamic tail contributes to allocated words" (frameAllocBytes takeLayout == 320)
55+
assert "dynamic tail size is padded to full ABI words"
56+
(frameSizeBytes (layout unpaddedDynamicFields) == 128)
57+
assert "dynamic calldata frames are not lowered with static tail sizes"
58+
(!layoutSourcesSupported takeLayout)
59+
let srcLayout := layout sourceFields
60+
assert "calldata/memory/code/storage sources supported" (layoutSourcesSupported srcLayout)
61+
assert "dynamic storage tails are rejected"
62+
(!layoutSourcesSupported (layout dynamicStorageFields))
63+
assert "dynamic memory tails are rejected until runtime-sized ABI frames exist"
64+
(!layoutSourcesSupported (layout dynamicMemoryFields))
65+
assert "dynamic source frame is pointer mode" (srcLayout.mode == FramePassMode.pointer)
66+
assert "code source spills through extcodecopy" (hasExtcodecopy (spillPayloadToMemory "src" srcLayout))
67+
let inlineNames := (inlineArgs (layout inlineFields)).filterMap calldataLoadName?
68+
assert "inline source words are indexed per field"
69+
(inlineNames == ["pair", "pair", "amount"])
70+
71+
end Compiler.ABI.FrameTest

‎Compiler/CompilationModel/Compile.lean‎

Lines changed: 38 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -409,6 +409,44 @@ def compileStmt (fields : List Field) (events : List EventDef := [])
409409
YulExpr.call "add" [YulExpr.lit 64, YulExpr.call "mul" [lenIdent, YulExpr.lit 32]]
410410
])
411411
]
412+
| Stmt.returnCodeData pointer => do
413+
if isInternal then
414+
throw s!"Compilation error: internal functions cannot use returnCodeData"
415+
let pointerExpr ← compileExpr fields dynamicSource pointer
416+
pure [
417+
YulStmt.block [
418+
YulStmt.let_ "__return_code_pointer"
419+
(YulExpr.call "and" [pointerExpr, YulExpr.hex addressMask]),
420+
YulStmt.let_ "__return_code_offset" (YulExpr.lit 1),
421+
YulStmt.let_ "__return_code_extent"
422+
(YulExpr.call "extcodesize" [YulExpr.ident "__return_code_pointer"]),
423+
YulStmt.if_
424+
(YulExpr.call "iszero" [
425+
YulExpr.call "gt" [
426+
YulExpr.ident "__return_code_extent",
427+
YulExpr.ident "__return_code_offset"
428+
]
429+
])
430+
[YulStmt.expr (YulExpr.call "revert" [YulExpr.lit 0, YulExpr.lit 0])],
431+
YulStmt.let_ "__return_code_size"
432+
(YulExpr.call "sub" [
433+
YulExpr.ident "__return_code_extent",
434+
YulExpr.ident "__return_code_offset"
435+
]),
436+
YulStmt.let_ "__return_code_ptr"
437+
(YulExpr.call "mload" [YulExpr.lit freeMemoryPointer]),
438+
YulStmt.expr (YulExpr.call "extcodecopy" [
439+
YulExpr.ident "__return_code_pointer",
440+
YulExpr.ident "__return_code_ptr",
441+
YulExpr.ident "__return_code_offset",
442+
YulExpr.ident "__return_code_size"
443+
]),
444+
YulStmt.expr (YulExpr.call "return" [
445+
YulExpr.ident "__return_code_ptr",
446+
YulExpr.ident "__return_code_size"
447+
])
448+
]
449+
]
412450
| Stmt.mstore offset value => do
413451
pure [YulStmt.expr (YulExpr.call "mstore" [
414452
← compileExpr fields dynamicSource offset,

‎Compiler/CompilationModel/LogicalPurity.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -213,6 +213,8 @@ def stmtContainsUnsafeLogicalCallLike : Stmt → Bool
213213
exprListAnyUnsafeLogicalCallLike args
214214
| Stmt.returnArray _ | Stmt.returnBytes _ | Stmt.returnStorageWords _ =>
215215
false
216+
| Stmt.returnCodeData pointer =>
217+
exprContainsUnsafeLogicalCallLike pointer
216218
| Stmt.mstore offset value =>
217219
exprContainsUnsafeLogicalCallLike offset || exprContainsUnsafeLogicalCallLike value
218220
| Stmt.tstore offset value =>

‎Compiler/CompilationModel/ScopeValidation.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -563,6 +563,9 @@ def validateScopedStmtIdentifiers
563563
pure localScope
564564
else
565565
throw s!"Compilation error: {context} Stmt.returnArray '{name}' requires parameter '{name}' or local bindings '{name}_data_offset' and '{name}_length'"
566+
| Stmt.returnCodeData pointer => do
567+
validateScopedExprIdentifiers context params paramScope dynamicParams localScope constructorArgCount pointer
568+
pure localScope
566569
| Stmt.returnBytes _ | Stmt.returnStorageWords _
567570
| Stmt.revertReturndata | Stmt.stop =>
568571
pure localScope

‎Compiler/CompilationModel/TrustSurface.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -281,6 +281,9 @@ private partial def collectUnguardedLowLevelStmtMechanics : Stmt → List String
281281
| .returnStorageWords _
282282
| .stop =>
283283
[]
284+
| .returnCodeData pointer =>
285+
"runtime introspection: extcodesize/extcodecopy returnCodeData" ::
286+
collectLowLevelExprMechanics pointer
284287

285288
private def collectUnguardedLowLevelMechanicsFromStmts (stmts : List Stmt) : List String :=
286289
dedupPreserve (stmts.flatMap collectUnguardedLowLevelStmtMechanics)

‎Compiler/CompilationModel/Types.lean‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -951,6 +951,7 @@ inductive Stmt
951951
| returnArray (name : String) -- ABI-encode dynamic uint256[] parameter loaded from calldata
952952
| returnBytes (name : String) -- ABI-encode dynamic bytes parameter loaded from calldata
953953
| returnStorageWords (name : String) -- ABI-encode dynamic uint256[] from sload over a dynamic word-array parameter
954+
| returnCodeData (pointer : Expr) -- Return an ABI payload stored as runtime code at `pointer`.
954955
| mstore (offset value : Expr)
955956
| tstore (offset value : Expr)
956957
/-- First-class `calldatacopy(destOffset, sourceOffset, size)` statement. -/
@@ -1060,7 +1061,7 @@ def directMetadata : Stmt → StmtMetadata
10601061
{ subexpressions := [value], termination := .alwaysTerminates, controlFlow := .returns }
10611062
| .returnValues values =>
10621063
{ subexpressions := values, termination := .alwaysTerminates, controlFlow := .returns }
1063-
| .returnArray _ | .returnBytes _ | .returnStorageWords _ =>
1064+
| .returnArray _ | .returnBytes _ | .returnStorageWords _ | .returnCodeData _ =>
10641065
{ termination := .alwaysTerminates, controlFlow := .returns }
10651066
| .mstore offset value =>
10661067
{ subexpressions := [offset, value], lowLevelMechanics := [.mstore] }
@@ -1124,7 +1125,7 @@ partial def controlFlow : Stmt → ControlFlowSummary
11241125
.mayReverting
11251126
| .revertError _ _ | .revertReturndata =>
11261127
.reverts
1127-
| .return _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ =>
1128+
| .return _ | .returnValues _ | .returnArray _ | .returnBytes _ | .returnStorageWords _ | .returnCodeData _ =>
11281129
.returns
11291130
| .stop =>
11301131
.stops

0 commit comments

Comments
 (0)