Renaming-variables
Renaming of variables.
See disambiguator for background.
Here we characterize, relationally, the renaming of variables.
The predicate mentioned in disambiguator,
i.e. the one that relates original and transformed code,
is actually a function that returns success or failure.
More precisely, as with other aspects of Yul,
it is a family of functions,
with a member for each kind of Yul syntactic entity
(expression, statement, etc.);
however, for simplicity below we refer to this family as just a function.
This function cannot just operate on old and new code,
intended as pieces of abstract syntax like expressions and statements.
Since the code may reference variables
defined outside the code being operated upon,
we need, as additional arguments,
information about how the variables in scope
are renamed in the code being operated upon.
This information is calculated
by operating on the enclosing code,
prior to recursively operating on the enclosed code.
Thus, in case of success, in general this function returns
updated renaming information.
Subtopics
- Statements/blocks/cases/fundefs-renamevar
- Mutually recursive ACL2 functions to check if
statements, blocks, cases, and function definitions are
related by variable renaming.
- Renaming-variables-execution
- Proof that variable renaming preserves the execution behavior.
- Expressions-renamevar
- Mutually recursive ACL2 functions to check if expressions are
related by variable renaming.
- Add-var-to-var-renaming
- Add a variable to a variable renaming list.
- Add-vars-to-var-renaming
- Add the variables in a list to a variable renaming list.
- Renaming-variables-safety
- Proof that variable renaming preserves the static safety checks.
- Fundef-list-renamevar
- Check if two lists of function definitions are
related by variable renaming.
- Expression-option-renamevar
- Check if two optional expressions are
related by variable renaming.
- Funcall-option-renamevar
- Check if two optional function calls are
related by variable renaming.
- Path-list-renamevar
- Check if two lists of paths are
related by variable renaming.
- Var-list-renamevar
- Check if two lists of variables are related by variable renaming.
- Var-renamevar
- Check if two variables are related by variable renaming.
- Path-renamevar
- Check if two paths are related by variable renaming.
