		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

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.

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.

Subtopics

Check-shadow-statements/blocks/cases/fundefs: Check the additional shadowing constraints on statements, blocks, cases, and function definitions.