1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
|
; Yul Library
;
; Copyright (C) 2025 Kestrel Institute (http://www.kestrel.edu)
;
; License: A 3-clause BSD license. See the LICENSE file distributed with ACL2.
;
; Author: Alessandro Coglio (www.alessandrocoglio.info)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "YUL")
(include-book "abstract-syntax")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defxdoc+ static-shadowing-checking
:parents (static-semantics)
:short "Static shadowing checking of Yul."
:long
(xdoc::topstring
(xdoc::p
"According to [Yul: Specification of Yul: Scoping Rules],
a variable declaration cannot shadow a variable
that is visible at the point in which the variable declaration occurs.
The notion of `visible' applies
not only to variables declared in outer blocks in the same function,
but also to variables declared in blocks in outer functions:
the former variables are accessible, while the latter are not.")
(xdoc::p
"For instance, consider the following Yul code:")
(xdoc::codeblock
"function f () {"
" let x"
" function g () {"
" let y"
" // here"
" }"
"}"
)
(xdoc::p
"At the point marked as `here',
@('x') is visible but not accessible,
while @('y') is both visible and accessible.")
(xdoc::p
"The non-shadowing of outer variables in the same function
(e.g. the non-shadowing of @('y') in function @('g'))
is checked as part of the safety checks
formalized in @(see static-safety-checking).
This is necessary for safety,
because the dynamic semantics has
a single variable scope (not a stack of scopes),
as formalized in @(see static-safety-checking).")
(xdoc::p
"The non-shadowing of outer variables in different functions
(e.g. the non-shadowing of @('x') in function @('g'))
is not needed for safe execution,
because when the body of a function (e.g. @('g')) is executed,
a new variable scope is started,
and the function has no access to outside variables (e.g. to @('x')).
Nonetheless, it is part of the Yul static semantics:
the Yul team has explained that its purpose is
just to prevent human error.
Thus, we formalize these checks here,
separately from the safety checks.")
(xdoc::p
"The shadowing restrictions formalized here
only apply to variables, not to functions.
Variables and functions are subject to
different visibility and accessibility rules;
all the rules that apply to functions
are parts of the safety checks."))
:order-subtopics t
:default-parent t)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defines check-shadow-statements/blocks/cases/fundefs
:short "Check the additional shadowing constraints on
statements, blocks, cases, and function definitions."
:long
(xdoc::topstring
(xdoc::p
"We recursively visit statements, blocks, etc.,
accumulating all the variables declared so far,
which form all the visible variables,
both accessible and inaccessble.
We check that each declared variable is not already visible.")
(xdoc::p
"Note that these checks overlap with the safety checks,
for what concerns visible and accessible variables,
while they are additional checks
for what concerns visible but inaccessible variables.
Restricting the checks to just visible but inaccessible variables
would be more complicated than checking all the visible variables."))
(define check-shadow-statement ((stmt statementp) (vars identifier-setp))
:returns (new-vars identifier-set-resultp)
:short "Check variable shadowing in a statement."
:long
(xdoc::topstring
(xdoc::p
"If the check is successful,
we return a possibly updated set of visible variables.
The set is actually updated only by variable declarations.")
(xdoc::p
"Since the scope of a loop's initialization block
extends to the whole loop,
we first check the list of statments of the initialization block,
obtaining a possibly updated set of visible variables,
which is used to check the update and body blocks of the loop."))
(statement-case
stmt
:block (b* (((okf &) (check-shadow-block stmt.get vars)))
(identifier-set-fix vars))
:variable-single (if (set::in stmt.name (identifier-set-fix vars))
(reserrf (list :shadowed-var stmt.name))
(set::insert stmt.name (identifier-set-fix vars)))
:variable-multi (b* ((declared (set::mergesort stmt.names))
(shadowed (set::intersect declared
(identifier-set-fix vars))))
(if (set::emptyp shadowed)
(set::union declared (identifier-set-fix vars))
(reserrf (list :shadowed-vars shadowed))))
:assign-single (identifier-set-fix vars)
:assign-multi (identifier-set-fix vars)
:funcall (identifier-set-fix vars)
:if (b* (((okf &) (check-shadow-block stmt.body vars)))
(identifier-set-fix vars))
:for (b* ((stmts (block->statements stmt.init))
((okf vars1) (check-shadow-statement-list stmts vars))
((okf &) (check-shadow-block stmt.update vars1))
((okf &) (check-shadow-block stmt.body vars1)))
(identifier-set-fix vars))
:switch (b* (((okf &) (check-shadow-swcase-list stmt.cases vars))
((okf &) (check-shadow-block-option stmt.default vars)))
(identifier-set-fix vars))
:leave (identifier-set-fix vars)
:break (identifier-set-fix vars)
:continue (identifier-set-fix vars)
:fundef (b* (((okf &) (check-shadow-fundef stmt.get vars)))
(identifier-set-fix vars)))
:measure (statement-count stmt))
(define check-shadow-statement-list ((stmts statement-listp)
(vars identifier-setp))
:returns (new-vars identifier-set-resultp)
:short "Check variable shadowing in a list of statements."
(b* (((when (endp stmts)) (identifier-set-fix vars))
((okf vars) (check-shadow-statement (car stmts) vars))
((okf vars) (check-shadow-statement-list (cdr stmts) vars)))
vars)
:measure (statement-list-count stmts))
(define check-shadow-block ((block blockp) (vars identifier-setp))
:returns (_ reserr-optionp)
:short "Check variable shadowing in a block."
:long
(xdoc::topstring
(xdoc::p
"We return no information in case of success,
because the variables declared in a block
are not visible after the block."))
(b* (((okf &) (check-shadow-statement-list (block->statements block) vars)))
nil)
:measure (block-count block))
(define check-shadow-block-option ((block? block-optionp)
(vars identifier-setp))
:returns (_ reserr-optionp)
:short "Check variable shadowing in an optional block."
(block-option-case
block?
:none nil
:some (check-shadow-block block?.val vars))
:measure (block-option-count block?))
(define check-shadow-swcase ((case swcasep) (vars identifier-setp))
:returns (_ reserr-optionp)
:short "Check variable shadowing in a case."
(check-shadow-block (swcase->body case) vars)
:measure (swcase-count case))
(define check-shadow-swcase-list ((cases swcase-listp) (vars identifier-setp))
:returns (_ reserr-optionp)
:short "Check variable shadowing in a list of cases."
(b* (((when (endp cases)) nil)
((okf &) (check-shadow-swcase (car cases) vars))
((okf &) (check-shadow-swcase-list (cdr cases) vars)))
nil)
:measure (swcase-list-count cases))
(define check-shadow-fundef ((fundef fundefp) (vars identifier-setp))
:returns (_ reserr-optionp)
:short "Check variable shadowing in a function definition."
:long
(xdoc::topstring
(xdoc::p
"First we ensure that the function's inputs and outputs
are not already visible.
We add them to the visible variables,
and we check the body."))
(b* ((inputs (fundef->inputs fundef))
(outputs (fundef->outputs fundef))
(declared (set::mergesort (append inputs outputs)))
(shadowed (set::intersect declared (identifier-set-fix vars)))
((unless (set::emptyp shadowed))
(reserrf (list :shadowed-vars shadowed)))
(vars (set::union (identifier-set-fix vars) declared)))
(check-shadow-block (fundef->body fundef) vars))
:measure (fundef-count fundef))
:verify-guards nil ; done below
///
(verify-guards check-shadow-statement)
(fty::deffixequiv-mutual check-shadow-statements/blocks/cases/fundefs))
|
