15.6  Translation to ACL2

Translation of a C++ model to ACL2 is performed in two steps: (1) the parser generates a representation of the model as a set of S-expressions, and (2) an ACL2 program converts this representation to an ACL2 program.

Most of the recognized C primitives correspond naturally either to to built-in ACL2 functions or to functions defined in Part I. The rest are implemented by a set of functions defined in the RTL library book "lib/masc", which is included in any book generated by the translator.

Two of these functions pertain to bit manipulation:

A number of functions are required for the translation of the boolean-valued operators of C, in which values are compared with 0, to ACL2, in which values are compared with NIL. For example,

Arrays (as well as structures) are represented in ACL2 as alists. The pair corresponding to an array entry associates its index with its value. The following primitives are defined in the ACL2 book "misc/records":

The S-expression generated by the parser for a function definition has the form

(DEFUNC name ( $ \mathit{arg}_1$ $ \ldots$ $ \mathit{arg}_k$) body)
where name is the name of the function, $ \mathit{arg}_1, \ldots, \mathit{arg}_k$ are its formal parameters, and body is an S-expression derived from its body, which is assumed to be a statement block. The parser generates an S-expression for each statement as follows:

Note that variable types are not explicitly preserved in the translation. Instead, they are used by the parser to inform the translation of terms. Consider, for example, the statement block
{ sf8i2 x = -145;
  ui8 y = 100, z = 3;
  z = y[4:2] * x; }
In the evaluation of the expression on the right side of the final assignment, the type of x dictates that its value is interpreted as a signed rational with 6 fractional bits, and according to the type y and z, their assigned values must be truncated to 8 integer bits. Thus, the C++ program that generates the above code also generates the following S-expression:
(BLOCK (DECLARE X (BITS (* -145 (EXPT 2 6)) 7 0))
       (LIST (DECLARE Y (BITS 100 7 0))
             (DECLARE Z (BITS 3 7 0)))
       (ASSIGN Z
               (BITS (FL (* (BITS Y 4 2)
                            (/ (SI 8 X) (EXPT 2 6))))
                     7 0)))

The ACL2 program that operates on the output of the parser resides in "books/masc/lisp/translate.lisp". The overall strategy of this program is to convert the body of a function to a nest of LET, LET*, and MV-LET terms. For each statement in the body, the translator generates the following:

Each statement except the last corresponds to a level of the nest in which the variables of outs are bound to the value of term, except that as an optimization to improve readability, adjacent LETs are combined into a single LET or LET* whenever possible. The term of the final statement of the body becomes the body of the nest.

As a trivial (and nonsensical) example, the C++ code that generates the pretty-printed function

uint foo(uint x, uint y, uint z) {
  uint u = y + z, v = u * x;
  <x, y, z> = bar(u, v);
  y = x > y ? 2 * u : v;
  if (x >= 0) {
    u = 2*u;
  }
  else {
    v = 3 * u;
  }
  if (x < y) {
    return u;
  }
  else {
  return y + v;
  }  
}
also generates the corresponding ACL2 function
(DEFUN FOO (X Y Z)
       (LET* ((U (+ Y Z)) (V (* U X)))
             (MV-LET (X Y Z) (BAR U V)
                     (LET ((Y (IF1 (LOG> X Y) (* 2 U) V)))
                          (MV-LET (V U)
                                  (IF1 (LOG>= X 0) 
                                       (MV V (* 2 U))
                                       (MV (* 3 U) U))
                                  (IF1 (LOG< X Y) U (+ Y V)))))))

Assertions, which do not affect any program variables, are handled specially. An assertion (ASSERT fn term) results in a binding of the dummy variable ASSERT to the value (IN-FUNCTION fn term), where IN-FUNCTION is a macro, defined in "lib/masc.lisp", that throws an error if the value of term is 0, with a message indicating the function in which the error occurred.

In addition to the top-level ACL2 function corresponding to a C++ function, a separate recursive function is generated for each for loop. Its returned values are those of the non-local variables that are assigned within the loop. Its arguments include these variables, along with any variables that are required in the execution of the loop, as well as any variables that occur in the loop initialization or test. The construction of this function is similar to that of the top-level function, but the final statement of the loop body is not treated specially. Instead, the body of the nest of bindings is a recursive call in which the loop variable is replaced by its updated value. The resulting term becomes the left branch of an IF expression, of which the right branch is simply the returned variable (if there is only one) or a multiple value consisting of the returned variables (if there are more than one). The test of the IF is the test of the loop.

For example, the function

uint baz(uint x, uint y, uint z) {
  uint u = y + z, v = u * x;
  for (uint i=0; i<u && u < v; i+=2) {
    v--;
    for (int j=5; j>=-3; j--) {
      assert(v > 0);
      u = x + 3 * u;
    }
  }
  return u + v;
}
generates three ACL2 functions:
(DEFUN BAZ-LOOP-0 (J V X U)
       (DECLARE (XARGS :MEASURE (NFIX (- J (1- -3)))))
       (IF (AND (INTEGERP J) (>= J -3))
           (LET ((ASSERT (IN-FUNCTION BAZ (> V 0)))
                 (U (+ X (* 3 U))))
                (BAZ-LOOP-0 (- J 1) V X U))
           U))

(DEFUN BAZ-LOOP-1 (I X V U)
       (DECLARE (XARGS :MEASURE (NFIX (- U I))))
       (IF (AND (INTEGERP I) (INTEGERP U) (INTEGERP V)
                (AND (< I U) (< U V)))
           (LET* ((V (- V 1)) (U (BAZ-LOOP-0 5 V X U)))
                 (BAZ-LOOP-1 (+ I 2) X V U))
           (MV V U)))

(DEFUN BAZ (X Y Z)
       (LET* ((U (+ Y Z)) (V (* U X)))
             (MV-LET (V U)
                     (BAZ-LOOP-1 0 X V U)
                     (+ U V))))

David Russinoff 2017-08-01