		Search-engine friendly clone of the ACL2 documentation.

Atc-tutorial

Atc-tutorial-conditional-statements

ATC tutorial: ACL2 representation of C conditional statements.

Previous tutorial pages have shown how to represent C functions whose bodies consists of return statements and possibly local variable declarations and assignments (including assignments to the function parameters). This tutorial page explains how to represent C functions whose bodies are (possibly nested) conditional statements.

If the body of an ACL2 function is an if, the body of the corresponding C function is an if-else statement, whose test is derived from the if's first argument and whose branches are derived from the if's second and third arguments. If any of the second or third arguments is also an if, the corresponding branch is a nested if-else statement.

However, note that if tests in ACL2 are (generalized) booleans, i.e. they must return non-nil for true and nil for false, while if tests in C are scalars (e.g. integers), i.e. they must return non-zero for true and zero for false. Since nil is different from the ACL2 model of any C scalar zero, and also t is different from the ACL2 model of any C scalar non-zero, ACL2 if tests cannot directly represent C if tests. The community book kestrel/c/atc/signed-ints.lisp, mentioned in atc-tutorial-int-representation, provides a function boolean-from-sint the converts (the ACL2 representation of) a C int into an ACL2 boolean: it returns t if the int is not 0; it returns nil if the int is 0. This boolean-from-sint must be used as the test of an ACL2 if, applied to an ACL2 term representing an int expression: it represents a C if test consisting of the argument expression.

For example, the ACL2 function

(defun |f| (|x| |y| |z|)
  (declare (xargs :guard (and (c::sintp |x|)
                              (c::sintp |y|)
                              (c::sintp |z|))))
  (if (c::boolean-from-sint |x|)
      |y|
    |z|))

represents the C function

int f(int x, int y, int z) {
    if (x) {
        return y;
    } else {
        return z;
    }
}

As another example, the ACL2 function

(defun |g| (|e|)
  (declare (xargs :guard (c::sintp |e|)))
  (if (c::boolean-from-sint (c::ge-sint-sint |e| (c::sint-dec-const 0)))
      (if (c::boolean-from-sint
           (c::lt-sint-sint |e| (c::sint-dec-const 1000)))
          (c::sint-dec-const 1)
        (c::sint-dec-const 2))
    (c::sint-dec-const 3)))
   )

represents the C function

int g(int e) {
    if (e >= 0) {
        if (e < 1000) {
            return 1;
        } else {
            return 2;
        }
    } else {
        return 3;
    }
}

The arguments of boolean-from-sint in if tests may be the same ones used to describe the expressions returned by int-valued functions. The boolean-from-sint just serves to turn C ints into ACL2 booleans; it is not explicitly represented in the C code, as shown in the examples above.

Previous: ACL2 representation of C assignments

Next: ACL2 representation of C conditional expressions