Static-shadowing-checking
Static shadowing checking of Yul.
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.
For instance, consider the following Yul code:
function f () {
let x
function g () {
let y
// here
}
}At the point marked as `here',
x is visible but not accessible,
while y is both visible and accessible.
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 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 static-safety-checking.
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.
Subtopics
- Check-shadow-statements/blocks/cases/fundefs
- Check the additional shadowing constraints on
statements, blocks, cases, and function definitions.
