ATC tutorial: ACL2 representation of C conditional statements followed by more code.
The preceding tutorial pages show how to represent C code whose flow of control is ``tree-shaped'': a function body is a return statement, or a local variable declaration followed by more code, or an assignment followed by more code, or a conditional statement whose branches have recursively the same form. Thus, each conditional statement forks the tree, while declarations and assignments extend the current tree branch, and nested conditional statements fork subtrees. Each path in the tree eventually concludes the execution of the function, via a return statement. This code structure excludes conditional statements whose branches do not return, but instead continue execution of subsequent code.
The execution of a C conditional statement that does not return (but instead continues execution with the code after the statement) generally causes side effects, such as updating local variables or function parameters; these are the only side effects of interest to us for now. In a functional language like ACL2, these side effects must be explicit: the representation of the conditional statement must yield something, which must be used in the representation of the code after the statement. We use let and mv-let for this purpose: the former if one local variable or function parameter is updated; the latter if multiple ones are updated. These lets are disinguished from the ones that represent local variable declarations and assignments because the term to which the variable is bound does not have the declar or assign wrapper. Consistently with that, the terms to which the mv-let variables are bound do not have any wrapper either.
For example, the ACL2 function
(defun |j| (|x|) (declare (xargs :guard (c::sintp |x|) :guard-hints (("Goal" :in-theory (enable c::declar c::assign))))) (let ((|y| (c::declar (c::sint-dec-const 0)))) (let ((|y| (if (c::boolean-from-sint (c::lt-sint-sint |x| (c::sint-dec-const 100))) (let ((|y| (c::assign (c::bitior-sint-sint |y| (c::sint-dec-const 6666))))) |y|) (let ((|y| (c::assign (c::bitxor-sint-sint |y| (c::sint-dec-const 7777))))) |y|)))) (c::bitand-sint-sint |x| |y|))))
represents the C function
int j(int x) { int y = 0; if (x < 100) { y = y | 6666; } else { y = y ^ 7777; } return x & y; }
The first let represents a local variable declaration as explained in atc-tutorial-local-variables, but the second let binds a homonymous variable to an if that represents a side-effecting conditional statement. The binding represents the side effects of the conditional statement, and the body of the second let (i.e. the bitand-sint-sint call) ``sees'' those side effects by referencing the bound variable. The variable bound in the second let must be one in scope; as also in the representation of assignments, it is a distinct shadowing variable in ACL2, but it represents the same variable in C. Indeed, the execution of a side-effecting conditional statement is a bit like an assignment to the variable, but performed via a statement instead of via an expression. It is required that both branches of the if end with the variable bound to the if: this is why both branches have a let that represents an assignment that modifies the variable. The function
(defun |j| (|x|) (declare (xargs :guard (c::sintp |x|) :guard-hints (("Goal" :in-theory (enable c::declar c::assign))))) (let ((|y| (c::declar (c::sint-dec-const 0)))) (let ((|y| (if (c::boolean-from-sint (c::lt-sint-sint |x| (c::sint-dec-const 100))) (c::bitior-sint-sint |y| (c::sint-dec-const 6666)) (c::bitxor-sint-sint |y| (c::sint-dec-const 7777))))) (c::bitand-sint-sint |x| |y|))))
is equivalent to the one above in ACL2 but is rejected by ATC. Requiring the branches to end with the bound variable forces the assignment to be made explicit in the ACL2 representation, thus simplifying ATC's task. As already explained, ATC is meant to be used in conjunction with APT; transformations could explicate these assignments automatically.
It is important to note that
lets that represent local variable declarations or assignments
cannot bind the variable (directly) to an if,
but only to a term that represents a C expression,
wrapped with declar or assign.
(The term may have the form
As another example, the ACL2 function
(defun |k| (|x| |y|) (declare (xargs :guard (and (c::sintp |x|) (c::sintp |y|)) :guard-hints (("Goal" :in-theory (enable c::declar c::assign))))) (let* ((|a| (c::declar (c::lognot-sint |x|))) (|b| (c::declar (c::bitnot-sint |x|)))) (mv-let (|a| |b|) (if (c::boolean-from-sint |y|) (let ((|a| (c::assign (c::bitnot-sint |a|)))) (mv |a| |b|)) (let* ((|b| (c::assign (c::sint-dec-const 2))) (|a| (c::assign (c::sint-dec-const 14)))) (mv |a| |b|))) (c::bitxor-sint-sint |a| |b|))))
represents the C function
int k(int x, int y) { int a = !x; int b = ~x; if (y) { a = ~a; } else { b = 2; a = 14; } return a ^ b; }
The structure is the same as the previous example, but the side effects involve two variables, and therefore we use an mv-let instead of a let. The first two lets (to which the let* expands) just represent local variable declarations, but the mv-let represents a conditional statement that side-effects two variables followed by more code (a return statement in this case). Similarly to the one-variable let case, both branches of the if are required to end with an mv of the bound variables, in the same order. Again, this facilitates ATC's task, and APT transformations could automatically produce terms of this form.
Note that, in this example, one branch modifies only one variable, while the other branch modifies both variables. However, each branch must return all the variables; for the first branch, only one is actually modified.
The above structures can be nested, in a way that should be obvious. For instance, a branch of a conditional could itself contain side-effecting conditionals. The ability to represent side-effecting conditional statements greatly expands the range of C code generable by ATC.
A branch that just returns the variable(s) without modification
represents an empty branch.
When that happens for the `else' branch,
ATC could generate an