		Search-engine friendly clone of the ACL2 documentation.

Atc-tutorial

Atc-tutorial-local-variables

ATC tutorial: ACL2 representation of C local variables.

So far this tutorial has shown ACL2 representations of C functions that operate on their parameters. This tutorial page explains how to represent C functions that introduce and operate on local variables.

A C local variable declaration is represented by an ACL2 let where the term to which the variable is bound is wrapped with declar to indicate a variable declaration. For examples, the ACL2 function

(defun |f| (|x| |y|)
  (declare (xargs :guard (and (c::sintp |x|) (c::sintp |y|))
                  :guard-hints (("Goal" :in-theory (enable c::declar)))))
  (let ((|z| (c::declar (c::lt-sint-sint |x| |y|))))
    (c::lognot-sint |z|)))

represents the C function

int f(int x, int y) {
    int z = x < y;
    return !z;
}

The let must bind a single variable, which must be distinct from the function's parameters and from any other let variable in scope (the latter restriction is an over-approximation, that is adequate to this tutorial page but is refined in subsequent tutorial pages). That is, it must be a new variable. Its name must satisfy the constraints described in atc-tutorial-identifiers. The type of the local variable, int in this case, is not explicitly represented in ACL2, but it is inferred by ATC based on the term that the variable is bound to. The declar wrapper is an identity function whose only purpose is to indicate to ATC that the let represents a local variable declaration as opposed to a local variable assignment (described in atc-tutorial-assignments); this wrapper should be normally enabled in proofs.

This is not limited to a single let. There may be nested lets, which represent local variables in a sequence. For instance, the ACL2 function

(defun |g| (|x| |y|)
  (declare (xargs :guard (and (c::sintp |x|) (c::sintp |y|))
                  :guard-hints (("Goal" :in-theory (enable c::declar)))))
  (let ((|x_lt_y| (c::declar (c::lt-sint-sint |x| |y|))))
    (let ((|x_eq_y| (c::declar (c::eq-sint-sint |x| |y|))))
      (let ((|x_le_y| (c::declar (c::bitior-sint-sint |x_lt_y| |x_eq_y|))))
        (c::lognot-sint |x_le_y|)))))

represents the C function

int g(int x, int y) {
    int x_lt_y = x < y;
    int x_eq_y = x == y;
    int x_le_y = x_lt_y || x_eq_y;
    return !x_le_y;
}

The C function above is equivalently represented by the ACL2 function

(defun |g| (|x| |y|)
  (declare (xargs :guard (and (c::sintp |x|) (c::sintp |y|))
                  :guard-hints (("Goal" :in-theory (enable c::declar)))))
  (let* ((|x_lt_y| (c::declar (c::lt-sint-sint |x| |y|)))
         (|x_eq_y| (c::declar (c::eq-sint-sint |x| |y|)))
         (|x_le_y| (c::declar (c::bitior-sint-sint |x_lt_y| |x_eq_y|))))
    (c::lognot-sint |x_le_y|)))

This form may be more readable: the variables are not indented, but they are at the same visual level, like the corresponding C variables. Internally, let* expands into nested lets; ATC examines ACL2 function bodies in translated form, where macros like let* are expanded.

Since let bindings in ACL2 always bind some term to the variable, only C variable declarations with initializers may be represented. This may be relaxed in the future, as C allows uninitialized local variables; for instance, these could be represented as let bindings that bind variables to terms that do not return C values.

Previous: ACL2 events generated by ATC

Next: ACL2 representation of C assignments