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:

*setbits*is the result of replacing the bit slice of the bit vector of width with .*setbitn*is*setbits*.

*log<*) is 1 if and 0 if not.*LREF(masc,if1,if1*) is if and if not.

*ag*is the value of the array at index .*as*is the result of setting the value of the array at index to .

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

(`DEFUNC` *name* (
) *body*)

where

- Statement block: (
`BLOCK`). - Sinple assignment: (
`ASSIGN`*var**term*). - Multiple-value assignment: (
`MV-ASSIGN`( )*term*), where*term*corresponds to a call to a multiple-valued function. - Variable or constant declaration: (
`DECLARE`*var**term*) or (`ARRAY`*var**term*), where*term*is optional. - Conditional branch: (
`IF`*term**left**right*), where*left*is a block and*right*is either a block or`NIL`. - Return statement : (
`RETURN`*term*). - For loop: (
`FOR`(*init test update*)*body*), where*init*is a declaration or an assignment,*test*is a term,*update*is an assignment, and*body*is a statement block. - Switch statement: (
`switch`*test*( . ) ( . )), where is either an integer or a list of integers and is a list of statements. - Assertion: (
`ASSERT`*fn term*), where*fn*is the name of the function in which the assertion occurs and*term*is a term that is expected to have a non-zero value.

{ 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

(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:

*ins*: a list of the variables whose values (prior to execution of the statement) are read by the statement;*outs*: a list of the variables (non-local to the statement) that are written by the statement;*term*: an expression of which (a) the unbound variables are*ins*, and (b) the value is a multiple value consisting of the updated values of the variables of*outs*, or a single value if*outs*is a singleton.

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