		Search-engine friendly clone of the ACL2 documentation.

Atc-tutorial

Atc-tutorial-multiple-functions

ATC tutorial: ACL2 representation and generation of multiple C functions.

As mentioned in atc-tutorial-int-programs, there is a one-to-one representational correspondence between ACL2 functions and C functions. This tutorial page explains in more details and exemplifies the representation and generation of multiple functions.

Consider a C program consisting of multiple functions:

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

int g (int z) {
    return f(z, ~z);
}

int h (int a, int b) {
    return g(a & b);
}

(We have chosen C operations that are well-defined over all ints to avoid guards that constrain the ranges of the function parameter.)

[C17:6.2.1] disallows forward references among function definitions. Specifically, [C17:6.2.1/4] says that an external declaration (i.e. one that is not inside any block), which includes function definitions, has a file scope that terminates at the end of the file; it seems implicit in this that the scope starts with the definition, and includes the function's body to make (singly) recursive calls possible. Mutually recursive C function definitions, and generally C function definitions that call functions defined later in a file, are allowed via function declarations (e.g. through header files) that are not function definitions, where the scope of the non-definition declaration starts before the definition. However, currently ATC only generates C files without header files or function declarations that are not definitions. Thus, the generated C functions cannot have forward references.

These restrictions mean that the C functions exemplified above must appear exactly in that order in the generated C file. This order matches ACL2's event order. The C program above is represented by the following three ACL2 functions:

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

(defun |g| (|z|)
  (declare (xargs :guard (c::sintp |z|)))
  (|f| |z| (c::bitnot-sint |z|)))

(defun |h| (|a| |b|)
  (declare (xargs :guard (and (c::sintp |a|) (c::sintp |b|))))
  (|g| (c::bitand-sint-sint |a| |b|)))

These three functions must necessarily appear in this order, but of course they do not have to be contiguous events in the ACL2 world, i.e. there may be any number of events between them.

The ACL2 functions to be translated to C functions must be always supplied to ATC in order (i.e. their order in the ACL2 world and in the C file). ATC checks that each supplied function only calls earlier functions in the list. This excludes any form of recursion, mutual or single. (This restriction may be eventually lifted, but for now it applies.)

For the example above, ATC must be called as follows:

(c::atc |f| |g| |h| :output-file ...)

Since each function listed only calls earlier functions in the list, this list is accepted by ATC, and the C program above is generated.

As mentioned above, currently ATC generates a single C file. As seen in previous examples, this is specified by the :output-file option, which must be present. The file should have extension .c, but ATC does not currently enforce that. In technical terms, the generated C file is a translation unit [C17:5.1.1.1]. More precisely, the file is a source file, which is read (by a C implementation, e.g. compiler) into a preprocessing translation unit, which becomes a translation unit after preprocessing. Since ATC currently generates files without preprocessing directives, preprocessing translation units coincide with translation units as far as the C code generated by ATC is concerned.

Previous: ACL2 representation of C identifiers

Next: ACL2 events generated by ATC