Check-safe-statement
Check if a statement is safe.
- Signature
(check-safe-statement stmt varset funtab) → varsmodes
- Arguments
- stmt — Guard (statementp stmt).
- varset — Guard (identifier-setp varset).
- funtab — Guard (funtablep funtab).
- Returns
- varsmodes — Type (vars+modes-resultp varsmodes).
If checking is successful, we return an updated variable table
and a set of possible termination modes.
The variable table is updated only via variable declarations,
while the other kinds of statements leave the table unchanged.
The table may be changed in blocks nested in the statement,
but those changes do not surface outside those blocks.
A block is checked via a separate ACL2 function,
which returns a set of modes.
These are joined with the starting variable table,
which is unchanged as expained above.
We use separate ACL2 functions to check declarations and assignments,
as their checking does not involve the mutual recursion.
Declarations and assignments always terminate in regular mode.
For a function call used as a statement,
we check the function call and ensure it returns no results.
A function call always terminates in regular mode.
For an if statement,
we check the test, which must return one result,
and we check the body block.
An if statement may terminate in regular mode
(when the test is false)
or in any of the modes in which the block may terminate
(when the test is true).
For a for statement, we treat the initialization block specially,
because the scope of the initialization block
extends to the whole statement, as explained
in [Yul: Specification of Yul: Scoping Rules].
We extract the statements from the block
and we process them as if they preceded the rest of the for:
we collect the function definitions in the statements,
and then we check the statements,
updating the variable table and obtaining the possible termination modes.
We ensure that no termination in break or continue is possible,
because that is not allowed,
even if the for is in the body of an outer for:
the current, innermost for is the one
that could be broken or continued,
but that can only be done in the body;
thus, the initialization block may only terminate
in regular or leave mode.
We use the updated variable and function tables
to check the other components of the for,
i.e. test, update block, and body block.
We ensure that the update block cannot terminate
in break or continue mode,
for the same reason explained above for the initialization block,
which therefore leaves regular and leave mode
as the only termination possibilities for the update block.
The body is allowed to terminate in any mode.
The possible termination modes of the for loop
are determined as follows:
regular mode is always possible,
which happens when the test is false or if the loop breaks;
leave mode is possible when it is possible for any of the
initialization, update, or body block;
break and continue modes are not possible,
because those could only occur in the body,
which causes regular loop termination of the loop for break
or continuation of the loop for continue.
For a switch statement,
we check the expression, ensuring it returns a single result.
We ensure that there is at least one (literal or default) case
[Yul: Specification of Yul: Restrictions on the Grammar].
The documentation also requires that the default case be absent
when the literal cases are exhaustive;
but that requires knowledge of the type of the target expression,
which for now we do not have, so we leave out that check for now.
We also need to check that all the literals are distinct,
which could be taken to mean as
either syntactically or semantically distinct:
for instance, the literals 1 and 0x1 are
syntactically different but semantically equal.
The Yul team has clarified that it should be semantic difference.
For now we check syntactic difference for simplicity,
but we plan to tighten that to check semantic difference.
Every (literal or default) block is then checked,
along with the literals.
The possible termination modes are those of the cases
and those of the default block.
The treatment of leave, break, and continue
is straightforward: they terminate with the corresponding mode,
and the variable table is unchanged.
For a function definition, the function table is not updated:
as explained in add-funtypes,
the function definitions in a block are collected,
and used to extend the function table,
before processing the statements in a block.
The function definition is checked by a separate ACL2 function,
which returns nothing in case of success,
so here we return the outside variable table unchanged:
a function definition does not modify the variable table.
At run time, a function definition is essentially a no-op,
so the termination mode is always regular.
