|
|
|---|
|
|
|
|---|
ATC tutorial: ACL2 representation of C assignments.
In atc-tutorial-local-variables it was described how to represent C local variable declarations and use the variables in C expressions. This tutorial page explains how to represent assignments to these variables in ACL2.
In C, assignments are expressions that may occur at any level, i.e. assignments may be subexpressions of other expressions at any depth. ATC only supports assignments that are full expressions [C:6.8/4], i.e. expressions at the top level, not subexpressions of other expressions. Specifically, ATC supports expression statements [C:6.8.3] whose expression is an assignment: this way, assignments are treated as if they were statements, keeping most expressions pure (i.e. side-effect-free) and thus simplifying the formal model of C and generated proofs.
A C local variable assignment is represented by an ACL2 let that binds a variable already bound, i.e. already in scope, and where the term to which the variable is bound is wrapped by the function assign. For example, 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 c::assign))))) (let* ((|a| (c:;declar (c::bitand-sint-sint |x| |y|))) (|a| (c::assign (c::bitnot-sint |a|)))) (c::gt-sint-sint |a| (c::sint-dec-const 0))))
represents the C function
int f(int x, int y) {
int a = x & y;
a = ~a;
return a > 0;
}Recall that the let* expands to two nested lets. The first one, as explained in atc-tutorial-local-variables, represents the local variable declaration with initializer; the second one represents the assignment, which in this case mentions the variable in the right subexpression, but of course it may contain any expression. The point is that the second let binds an ACL2 variable symbol that is the same as the one bound by the first let. These are two homonymous but different variables in ACL2: the second one shadows the first one. However, we use the homonymy of the two ACL2 variables to represent them as the same variable in C, i.e. to regard the second let as an assignment rather than a declaration. After all, the C scoping rules differ from the ACL2 scoping rules: C disallows a variable declaration with the same name as another variable in the same scope (but it allows shadowing in an inner scope).
The wrapper assign is the identity function, whose sole purpose is to indicate to ATC that the let represents a local variable assignment as opposed to a local variable declaration (described in atc-tutorial-local-variables); this wrapper should be normally enabled in proofs.
In ATC, we can also represent assignments to C function parameters via let that bind variables with the same names as the ACL2 function parameters, and with the terms bound to the variables wrapped with assign. For example, the ACL2 function
(defun |g| (|a| |b|) (declare (xargs :guard (and (c::sintp |a|) (c::sintp |b|) ;; 0 <= a <= 100: (<= 0 (c::integer-from-sint |a|)) (<= (c::integer-from-sint |a|) 100)) :guard-hints (("Goal" :in-theory (enable c::assign c::add-sint-sint-okp c::sint-integerp-alt-def))))) (let ((|a| (c::assign (c::add-sint-sint |a| (c::sint-dec-const 200))))) (c::lt-sint-sint |b| |a|)))
represents the C function
int g(int a, int b) {
a = a + 200;
return b < a;
}Even though the let in the function above is not nested under another let, the fact remains that it binds an ACL2 variable with the same symbol as a variable in the same scope. (An ACL2 function parameter is, in a way, implicitly bound.) Thus, ATC treats that as an assignment instead of a variable declaration.
Previous: ACL2 representation of C local variables