		Search-engine friendly clone of the ACL2 documentation.

Java

Atj

ATJ (ACL2 To Java) is a Java code generator for ACL2.

This manual page contains user-level reference documentation for ATJ. If you are new to ATJ, you should start with the tutorial, which provides user-level information on how ATJ works and how to use ATJ effectively. Some of the material in this manual page will likely be moved to the tutorial, which is in progress.

Introduction

ATJ translates ACL2 to Java, enabling ACL2 code to be used in Java code (in the sense explained below).

For instance, ATJ is useful to generate Java code at the end of an APT program synthesis derivation.

This manual page provides reference documentation for ATJ. A separate tutorial in being written, as noted above. See the files under kestrel/java/atj/tests/ for examples of use of ATJ.

Scope

ATJ translates ACL2 named functions to corresponding Java code whose execution mimics the execution of the ACL2 functions.

The ACL2 functions accepted by ATJ may manipulate any ACL2 value: characters, strings, symbols, numbers, and cons pairs. The Java code that corresponds to the ACL2 functions manipulates Java representations of the ACL2 values.

ATJ accepts all the ACL2 functions that (1) have either an unnormalized body or an attachment and (2) either do not have raw Lisp code or have raw Lisp code but belong to a whitelist (but also see the :ignore-whitelist option below). The ACL2 functions with raw Lisp code are the ones for which rawp holds; of these, the ones in the whitelist are the ones for which pure-raw-p holds. The unnormalized body of the functions in the whitelist is functionally equivalent to their raw Lisp code. The Java code that corresponds to the ACL2 functions that satisfy conditions (1) and (2) above, mimics the computations described by their unnormalized body. In the case of functions without an unnormalized body but with an attachment, (a call of) the attached function (on the formal arguments) plays the role of the unnormalized body.

ATJ also accepts the ACL2 function return-last (which has raw Lisp code and is not in the whitelist), but only when its first argument is 'acl2::mbe-raw1 or 'acl2::progn. Calls of the form (return-last 'acl2::mbe1-raw ...) are translated representations of calls of mbe; ATJ translates to Java either the :logic or the :exec part of these calls, as detailed below. Calls of the form (return-last 'acl2::progn ...) are translated representations of calls of prog2$ and progn$; ATJ translates to Java the last argument of these calls, as detailed below.

ATJ also accepts all the ACL2 primitive functions. The Java code that corresponds to these ACL2 functions has the input/output behavior documented for these functions.

ATJ accepts both logic-mode and program-mode functions.

Some ACL2 functions have side effects when executed, e.g. hard-error prints an error message and returns control to the top level. All the ACL2 functions with side effects have raw Lisp code and are not in the whitelist mentioned above. Therefore, the generated Java code does not mimic any of the side effects exhibited by ACL2 functions. In particular, calls of prog2$ and progn$ are accepted (as explained above about return-last with first argument 'acl2::progn) only if their non-last arguments are free of side effects. Support for translating ACL2 functions with side effects to Java code that mimics those side effects may be added in the future.

ATJ does not accept functions that access stobjs. Support for stobjs, and destructive updates of stobjs, may be added in the future.

ATJ does not translate macro definitions to Java code. However, the use of macros in function bodies is fully supported, because ATJ operates on ACL2 translated terms, where macros are expanded.

ATJ does not translate named constant definitions to Java code. However, the use of named constants in function bodies is fully supported, because ATJ operates on ACL2 translated terms, where constants are expanded.

The generated Java code can be called by external Java code, but not vice versa. The ability to have the generated Java code call external Java code may be added in the future; this may involve the use of ACL2 stubs corresponding to the Java code to be invoked by the (Java-translated) ACL2 code.

External Java code can call the generated Java code on (Java representations of) explicit ACL2 values. Access to global variables like state or user-defined stobjs is therefore not supported; in particular, the generated Java code has no access to the ACL2/Lisp environment. Support for global variables, in particular state, may be added in the future.

Approach

ATJ is supported by AIJ, which is a deep embedding in Java of the executable subset of ACL2 (subject to the limitations outlined above).

ATJ translates the target ACL2 functions into Java representations, based on their unnormalized bodies or attachments. It does so recursively, starting from the top-level functions specified by the user and stopping at the ACL2 functions that either are implemented natively in AIJ or (under certain conditions; see below) represent Java primitive operations or primitive array operations. If a function is encountered that is not natively implemented in AIJ and has no unnormalized body and no attachment, ATJ stops with an error. If a function is encountered that has raw Lisp code and is not in the whitelist (except for the treament of return-last explained above), ATJ stops with an error.

ATJ generates Java code with public methods to (1) initialize AIJ's Java representation of the ACL2 environment and (2) call the Java representations of the ACL2 functions (see the `Generated Java Code' section for details). AIJ provides public classes and methods to translate certain Java values to AIJ's Java representations of ACL2 values and vice versa. Thus, by loading into the Java Virtual Machine both AIJ and the Java code generated by ATJ, external Java code can ``use'' ACL2 code. Under some conditions, ATJ can also generate Java code that does not use AIJ, and can be run without AIJ; see below for details.

ATJ generates either deeply embedded or shallowly embedded Java representations of the ACL2 functions. The choice is controlled by a user option.

Deep Embedding

In the deep embedding approach, ATJ generates Java code to build the deeply embedded ACL2 functions, and to call and execute them via AIJ's interpreter.

This deep embedding approach is simple and thus fairly high-assurance. On the other hand, the Java code is not efficient or idiomatic. However, the approach may work well for some simple applications.

Shallow Embedding

In the shallow embedding approach, ATJ generates Java code that mimics the computations of the shallowly embedded ACL2 functions, one Java method for each ACL2 function. These methods are executed without using AIJ's interpreter. However, the shallowly embedded ACL2 functions still use AIJ's representation of the ACL2 values and AIJ's native implementations of ACL2 functions. Under certain conditions, the shallowly embedded ACL2 functions use Java values that are not AIJ's Java representations of ACL2 values; see below for details.

This shallow embedding approach is more complex than the deep embedding approach, but produces code that is more efficient and more idiomatic.

General Form

(atj fn1 ... fnp
     :deep             ...
     :guards           ...
     :no-aij-types     ...
     :java-package     ...
     :java-class       ...
     :output-dir       ...
     :tests            ...
     :ignore-whitelist ...
     :verbose          ...
  )

Inputs

fn1, ..., fnp

Names of the target ACL2 functions to be translated to Java.
Each fni must be a symbol that names a function that either has an unnormalized body and no raw Lisp code (unless it is in the whitelist; but also see the :ignore-whitelist option below), or has an attachment, or is natively implemented in AIJ. Each of these functions must have no input or output stobjs. Each of these functions must transitively call (in the unnormalized body or attachment, if not natively implemented in AIJ) only functions that satisfy the same constraints, except for calls of return-last as described below.
None of the fni functions may be return-last. However, the fni functions may transitively call return-last, under two possible conditions:
The first argument of return-last is 'acl2::mbe-raw1, i.e. the call results from the translation of mbe. Even though Java code is generated for one of the second and third arguments but not for the other one (based on the :guars input; see below), the restrictions on called functions, and in particular the absence of side effects, are enforced on all the argument of the call.
The first argument of return-last is 'acl2::progn, i.e. the call results from the translation of prog2$ or progn$. Even though Java code is generated for the last argument of the call but not for the previous one(s), the restrictions on called functions, and in particular the absence of side effects, are enforced on all the argument of the call.
If the :deep input is nil and the :guards input is t, then none of the fni may be one of the functions listed in *atj-jprim-fns* or one of the functions listed in *atj-jprimarr-fns*. These functions are treated specially in the shallow embedding when guard satisfaction is assumed (see below).
There must be at least one function, i.e. p > 0. All the fni names must be distinct.

:deep — default nil

Chooses the deep or shallow embedding approach described above:
t, for the deep embedding.
nil, for the shallow embedding.

:guards — default t

Specifies whether the generated code should assume that all the guards are satisfied or not:
t, to assume that they are satisfied. In this case, the generated code may run faster; in particular, only the :exec part of mbe is executed. Furthermore, if the :deep input is nil, the Java methods in the generated code have the argument and return types specified via atj-main-function-type and atj-other-function-type (see the `Generated Java Code' section for more information), and the generated Java code may manipulate Java primitive values and Java primitive arrays directly.
nil, to not assume that the guards are satisfied. In this case, the generated code runs ``in the logic''; in particular, only the :logic part of mbe is executed.
Regardless of the value of this input, the generated code never checks guards. The difference is whether guards are ignored altogether (i.e. execution ``in the logic'') or assumed to hold (i.e. possibly faster execution). This input should be t only when generating Java code from guard-verified ACL2 code. Furthermore, external Java code that calls the generated code should do so only with values that satisfy the guards of the called ACL2 functions, if this input is t. Otherwise, erroneous computations may occur.

:no-aij-types — default nil

Specifies whether the generated code should not make use of the AIJ types:
t, to require the code not to use any of the AIJ types, which represent ACL2 values in Java. In other words, the generated code can only use the Java primitive types and the Java primitive array types; this means that the code is generally more idiomatic Java, as opposed to mimicking ACL2 code in Java.
nil, to not require that.
This input can be t only if :deep is nil and :guards is t, because that is the only situation in which the generated Java code may use the Java primitive types and primitive array types. If this input is t, ATJ checks that every function fn translated to Java satisfies the following requirements:
The argument and return types of fn, specified via atj-main-function-type, are all :aboolean, :acharacter, and :j.... Recall that ACL2 booleans and characters are mapped to Java booleans and characters when :deep is nil and :guards is t. The built-in functions equal, if, and not are excepted from this requirement.
The unnormalized body (or attachment, as explained earlier) of fn, after the pre-translation steps that remove code (i.e. atj-pre-translation-remove-return-last, atj-pre-translation-remove-dead-if-branches, and atj-pre-translation-unused-vars), only uses, as an untranslated term:
Variables.
Quoted t and nil, which ATJ maps to the corresponding Java boolean literals when :deep is nil and :guards is t.
Quoted boolean and integer constants used as arguments of functions in *atj-jprim-constr-fns*.
Lambda expressions (i.e. let, including mv-let).
Calls of:
The function fn (as a recursive call).
The other functions translated to Java.
The functions in *atj-jprim-constr-fns*, but only on quoted constants.
The function boolean-value->bool.
The functions in *atj-jprim-unop-fns*.
The functions in *atj-jprim-binop-fns*.
The functions in *atj-jprim-conv-fns*.
The functions in *atj-jprimarr-read-fns*.
The functions in *atj-jprimarr-length-fns*.
The functions in *atj-jprimarr-write-fns*.
The functions in *atj-jprimarr-new-len-fns*.
The functions in *atj-jprimarr-new-init-fns*, but only on arguments that are nested conses (i.e. translated list calls).
The function equal.
The function if.
The function not.
The function cons, but only in translated mv calls that are returned by fn, either at the top level of the function's body or recursively in the `then' or `else' branches of ifs starting at the top level.
If :no-aij-types is t, ATJ also checks that the target functions fn1, ..., fnp do not include equal, if, not, or cons. These functions may only be called, directly or indirectly, by the target functions, but cannot be target functions.

:java-package — default nil

Name of the Java package of the generated Java code.
It must be either an ACL2 string or nil. If it is an ACL2 string, it must be a valid Java package name consisting of only ASCII characters; it must also be distinct from AIJ's Java package name, i.e. edu.kestrel.acl2.aij. If this input is nil, the generated Java code is in an unnamed Java package.

:java-class — default nil

Name of the generated Java class.
It must be either an ACL2 string or nil. If it is an ACL2 string, it must be a valid Java class name consisting of only ASCII characters. If this input is nil, the generated Java class is called Acl2Code.
Unless :no-aij-type is t, an additional auxiliary class is generated, whose name is obtained by appending Environment at the end of the name of the main class. This auxiliary class contains boilerplate code to build a Java representation of the ACL2 environment (i.e. ACL2 package definitions, and also ACL2 function definitions if the :deep input is t).
If the :tests input (see below) is not nil, a third Java class for testing is generated, whose name is obtained by appending Tests at the end of the name of the main class.

:output-dir — default "."

Path of the directory where the generated Java files are created.
It must be an ACL2 string that is a valid path to an existing directory in the file system; the path may be absolute, or relative to the connected book directory. The default is the connected book directory.
If the :java-package input specifies an unnamed package, the generated Java files are written in that directory. If the :java-package input specifies a named package, subdirectories are created in that directory that correspond to the dot-separated identifiers of the package name, and the generated Java files are written in the innermost subdirectory. This directory structure matches the typical organization of Java source files. If the subdirectories do not exist, they are created; if they exist, they are used as they are, without regard to whether they may contain additional files and directories (however, it is recommended that the subdirectories do not contain any such additional files and directories.
One file per class is generated: one file if the :no-aij-types input is t and the :tests input is nil; two files if either the :no-aij-types input is nil and the :tests input is nil, or the :no-aij-types input is t and the :tests input is t; and three files if the :no-aij-types input is nil and the :tests input is t. The name of each generated file is the name of the corresponding class followed by .java. If the file already exists, it is overwritten.

:tests — default nil

Optional tests to generate Java code for.
This input must evaluate to a list of doublets ((name1 term1) ... (nameq termq)), where each namej is a string consisting of only letters and digits, and each termj is an untranslated ground term whose translation is (fn in1 in2 ...), where fn is among the target functions fn1, ..., fnp, fn returns single results (i.e. not multiple results) (support for generating tests for functions that return multiple results will be added in the future), and each in among in1, in2 satisfies the following conditions:
If :deep is t or :guards is nil, then in must be a quoted constant.
If :deep is nil and :guards is t, then requirements on in depend on the type assigned, via atj-main-function-type, to the input of fn corresponding to in:
If the type is :a..., then in must be a quoted constant.
If the type is :jboolean, then in must be a term (java::boolean-value <boolean>) where <boolean> is a quoted boolean (i.e. t or nil).
If the type is :jchar, then in must be a term (java::char-value <char>) where <char> is a quoted unsigned 16-bit integer.
If the type is :jbyte, then in must be a term (java::byte-value <byte>) where <byte> is a quoted signed 8-bit integer.
If the type is :jshort, then in must be a term (java::short-value <short>) where <short> is a quoted signed 16-bit integer.
If the type is :jint, then in must be a term (java::int-value <int>) where <int> is a quoted signed 32-bit integer.
If the type is :jlong, then in must be a term (java::long-value <long>) where <long> is a quoted signed 64-bit integer.
If the type is :jboolean[], then in must be a term (java::boolean-array-new-init <booleans>) where <booleans> is the translation of a term (list <elem1> <elem2> ...) where each <elem> is a term (java::boolean-value <boolean>) as in the case above in which the type is :jboolean.
If the type is :jchar[], then in must be a term (java::char-array-new-init <chars>) where <chars> is the translation of a term (list <elem1> <elem2> ...) where each <elem> is a term (java::char-value <char>) as in the case above in which the type is :jchar.
If the type is :jbyte[], then in must be a term (java::byte-array-new-init <bytes>) where <bytes> is the translation of a term (list <elem1> <elem2> ...) where each <elem> is a term (java::byte-value <byte>) as in the case above in which the type is :jbyte.
If the type is :jshort[], then in must be a term (java::short-array-new-init <short>) where <short> is the translation of a term (list <elem1> <elem2> ...) where each <elem> is a term (java::short-value <short>) as in the case above in which the type is :jshort.
If the type is :jint[], then in must be a term (java::int-array-new-init <ints>) where <ints> is the translation of a term (list <elem1> <elem2> ...) where each <elem> is a term (java::int-value <int>) as in the case above in which the type is :jint.
If the type is :jlong[], then in must be a term (java::long-array-new-init <longs>) where <longs> is the translation of a term (list <elem1> <elem2> ...) where each <elem> is a term (java::long-value <long>) as in the case above in which the type is :jlong.
All the namej strings must be distinct.
Each doublet (namej termj) specifies a test, in which the result of (fn in1 in2 ...) calculated by ACL2 is compared with the result of the same call calculated via the generated Java code for fn. These tests can be run via additional generated Java code (see below).
Note that the :tests input is evaluated.
Test inputs of the form (java::boolean-value <boolean>), (java::char-value <char>), (java::byte-value <byte>), (java::short-value <short>), (java::int-value <int>), (java::long-value <long>), (java::boolean-array-new-init <booleans>), (java::char-array-new-init <chars>), (java::byte-array-new-init <bytes>), (java::short-array-new-init <shorts>), (java::int-array-new-init <ints>), or (java::long-array-new-init <longs>) can be used only for ACL2 functions that have the ATJ type :jboolean, :jchar, :jbyte, :jshort, :jint, :jlong, :jboolean[], :jchar[], :jbyte[], :jshort[], :jint[], or :jlong[] assigned to the corresponding argument via atj-main-function-type.

:ignore-whitelist — default nil.

If t, this tells ATJ to ignore the whitelist of functions with raw Lisp code, i.e. to accept any function with raw Lisp code, provided that it has an unnormalized body. This means that any side effects that happen in ACL2 execution will not happen in the generated Java code. This should be only used in special circumstances, e.g. when the non-whitelisted functions are unreachable under guard verification.

:verbose — default nil

Controls the amount of screen output:
t, to show all the output.
nil, to suppress all the non-error output.

Generated Java Code

ATJ generates a Java file that contains a single public class named as specified by the :java-class input, in the package specified by the :java-package input.

// if :deep is t:
public class <name> {
    ...
    public static void initialize() ...
    public static Acl2Value
        call(Acl2Symbol function, Acl2Value[] arguments) ...
}

// if :deep is nil:
public class <name> {
    ...
    public static void initialize() ...
    public static class <pkg> {
        public static <type> <fn>(<type> ...) ...
    }
    // other public static classes with public static methods
}

This Java class has a public static method initialize to initialize the relevant portions of the ACL2 environment. This public method must be called just once, before calling the other public methods described below. This initialize method should be also called before calling any of the public methods provided by AIJ, because AIJ itself relies on this initialization to work properly. This method is actually empty, but calling it ensures that the class is initialized: it is the class's static initializer that performs the actual initialization. This method is not generated if :no-aij-types is t.

In the deep embedding approach, the Java class also has a public static method call to call an ACL2 function on some ACL2 values. The method takes as arguments the name of the ACL2 function to call and an array of ACL2 values, and returns an ACL2 value. The called ACL2 function must be among fn1, ..., fnp and the functions that they transitively call, or it may be natively implemented in AIJ.

In the shallow embedding approach, the Java class contains public static methods for the functions among fn1, ..., fnp, the functions that they transitively call (except for the functions in *atj-jprim-fns* and *atj-jprimarr-fns*, when :deep is nil and :guards is t) and the ACL2 functions natively implemented in AIJ (the latter are just wrappers of the native implementations). Each method has the same number of parameters as the ACL2 function. If :guards is nil, there is exactly one method for each ACL2 function; that method's arguments all have types Acl2Value, while the return type is either Acl2Value if the function returns a single result or MV_Acl2Value_..._Acl2Value if the function returns multiple results where _Acl2Value is repeated for the number of results. If :guards is t, for each ACL2 function there are as many overloaded methods as the number of function types associated to the function via atj-main-function-type and atj-other-function-type: each of these function types determines the argument and return types of the corresponding overloaded method, with each argument having the corresponding function input type and the return type being either the single output type if the function returns a single result or MV_<type1>_..._<typen> if the function returns multiple results where each <typei> is determined from the corresponding function output type. These methods are declared in nested public classes, one class for each ACL2 package: each function's method is in the corresponding package's class. The mapping between these Java class and method names and the corresponding ACL2 package and function names is displayed if :verbose is t.

If :no-aij-types is nil, ATJ also generates a Java file that contains a single package-private class whose name is the name of the main class (described above) followed by Environment. This additional Java class contains code to initialize the ACL2 environment: this code is executed by invoking the initialize() method of the main class described above.

Optional Test Class

If the :tests input (see above) is not nil, ATJ also generates an additional Java file that contains a single public class named as specified in the description of the :java-class input above, in the package specified by the :java-package input.

public class <name>Tests {
   ...
    public static void main(String[] args) ...
}

This Java class includes code for each test (namej termj) specified via the :tests input (see above). The code for each test prints namej, evaluates the call (fn qc1 1c2 ...) (which termj translates to) in AIJ (via the call public method described above), compares the resulting value with the one that ACL2 returns (which is calculated when ATJ is run), and prints a success or failure message depending on whether the comparison succeeds or fails.

This Java class has a public static main method that calls the initialize public method described above and then executes the code to run the tests described just above. Thus, this test class can be invoked as a Java application. This main method also prints a final message saying whether all the tests pass or there are any failures. If all the tests pass, the method exits the JVM with return code 0; otherwise, it exits the JVM with return code 1, which is an error code when the test class is invoked as a Java application in a shell script.

Java Version

ATJ generates Java 8 code. This means that the code can be compiled using a compiler for Java 8 or later.

Compiling and Running the Java Code

The generated Java code can be compiled and run as any other Java code. The .jar file for AIJ must be in the classpath: this file is at kestrel/java/aij/java/out/artifacts/AIJ_jar/AIJ.jar. The files compile.sh and run.sh under kestrel/java/atj/tests/ contains examples of command to compile and run the code. See the AIJ documentation for instructions on how to generate the .jar file. If :no-aij-types is t, this .jar file is not needed.

When the :deep input is t, (the Java representations of) the ACL2 functions are evaluated via AIJ's recursive interpreter: evaluating recursive ACL2 functions on sufficiently large inputs may cause a stack overflow error in Java. When the :deep input is nil, recursive ACL2 functions are translated to recursive Java methods, except for tail-recursive functions, which are translated to loops: calling these recursive methods on sufficiently large inputs may cause a stack overflow error in Java. These stack overflow issues may be mitigated by passing a larger stack size to the Java Virtual Machine (via the -Xss option to the java command; see the comments in the file kestrel/atj/tests/run.sh), or, when :deep is nil, by making all the recursive ACL2 functions tail-recursive (e.g. via APT's tail recursion transformation) prior to generating Java code.

Subtopics

Atj-implementation: Implementation of atj.
Aij-atj-paper: ACL2-2018 Workshop paper on AIJ and ATJ.
Atj-tutorial: ATJ tutorial.