		Search-engine friendly clone of the ACL2 documentation.

Exec

Exec-statement

Execute a statement.

Signature
(exec-statement stmt cstate funenv limit) → outcome
Arguments: stmt — Guard (statementp stmt).; cstate — Guard (cstatep cstate).; funenv — Guard (funenvp funenv).; limit — Guard (natp limit).
Returns: outcome — Type (soutcome-resultp outcome).

Executing a block statement reduces to the execution of the block, which is handled by a separate ACL2 function.

In a single variable declaration with an initializing expression, the expression must yield exactly one value; if there is no initializing expression, the default value is 0. In a multiple variable declaration with an initializing function call, the funcion call may yield any number of values, which must match the number of variables (this is checked in add-vars-values), which must be two or more; if there is no initializing function call, the default value is 0 for each variable. In both kinds of assignments, we extend the computation state with the new variable(s).

For a single variable assignment, we ensure that the path is a singleton, we execute the expression, which must return a single value, and we write to the variable. For a multiple variable assignment, we ensure that each path is a singleton and that there are at least two variables, we execute the function call, which must return the same number of values as the variables (this is checked in write-vars-values, and we write to the variables.

For a function call statement, we execute the function call (for side effects), which must return no values.

For a conditional, we first execute the condition. Given that our current model of Yul does not include boolean, and also based on discussions on Gitter, we consider 0 to be false and any non-0 value to be true. If the condition is true, we execute the body; otherwise we terminate regularly.

A leave, break, or continue statement leaves the computation state unchanged and returns the corresponding mode.

For a switch statement, we execute the target, ensuring it returns a single value. Then we delegate the rest to a separate ACL2 function.

For a loop statement, we start by saving (the names of) the variables before the loop, similarly to exec-block. The initialization block of a loop statement is not treated like other blocks: its scope extends to the rest of the loop statement. Thus, instead of executing the initialization block as a block, we take the statements in the block, extend the function environment with any function declared there, and execute the statements, which may result in new and updated variables. We defensively stop with an error if the initialization block terminates with break or continue; if it terminates with leave, we also terminate with leave, removing extra variables and restoring the function environment. We delegate the execution of the loop iterations to another ACL2 function. We take the result of that ACL2 function, and remove the variables added by the loop (similarly to exec-block).

A function definition does not change the computation state and terminates regularly. It is like a no-op when it is encountered as a statement. The function definitions in a block are incorporated into the function environment of the computation state prior to starting to execute the statements in the block.