|
|
|---|
|
|
|
|---|
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.
The non-shadowing of outer variables in the same function 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).
The non-shadowing of outer variables in different functions is not needed for safe execution, because when the body of a function is executed, a new variable scope is started, and the function has no access to outside variables. 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.