		Search-engine friendly clone of the ACL2 documentation.

Lifters

Unroll-java-code

Lift a Java method to create a DAG, unrolling loops as needed.

General Form:

(unroll-java-code defconst-name
                  method-indicator
                  &key
                  :assumptions                   ; default nil
                  :array-length-alist            ; default nil
                  :classes-to-assume-initialized ; default '("java.lang.object" "java.lang.system")
                  :ignore-exceptions             ; default nil
                  :ignore-errors                 ; default nil
                  :vars-for-array-elements       ; default t
                  :param-names                   ; default :auto
                  :output                        ; default :auto
                  :steps                         ; default :auto
                  :rule-alists                   ; default nil
                  :extra-rules                   ; default nil
                  :remove-rules                  ; default nil
                  :normalize-xors                ; default nil
                  :prune-branches-approximately  ; default nil
                  :prune-branches-precisely      ; default nil
                  :call-stp                      ; default nil
                  :memoizep                      ; default t
                  :branches                      ; default :smart
                  :chunkedp                      ; default nil
                  :monitor                       ; default nil
                  :print                         ; default nil
                  :print-interval                ; default nil
                  :produce-theorem               ; default nil
                  :produce-function              ; default nil
                  :local                         ; default t
                  )

Inputs:

defconst-name — (required)

The name of the constant to create. This constant will represent the computation in DAG form. A function may also created (its name is obtained by stripping the stars from the defconst name).

method-indicator — (required)

The Java method to unroll (a string like "java.lang.Object.foo(IB)V"). The descriptor (input and output type) can be omitted if only one method in the given class has the given name.

:assumptions — default nil

Terms to assume true when unrolling. These assumptions can mention the method's parameter names (symbols), the byte-variables and/or bit-variables in the contents of array parameters, and the special variables locals, initial-heap, initial-static-field-map, and initial-intern-table.

:array-length-alist — default nil

An alist pairing array parameter names (symbols) with their lengths.

:classes-to-assume-initialized — default ("java.lang.object" "java.lang.system")

Classes to assume the JVM has already initialized (or :all)

:ignore-exceptions — default nil

Whether to assume exceptions do not happen (e.g., out-of-bounds array accesses)

:ignore-errors — default nil

Whether to assume JVM errors do not happen

:vars-for-array-elements — default t

whether to introduce vars for individual array elements (nil, t, or :bits)

:param-names — default :auto

Names to use for the parameters (e.g., if no debugging information is available), or :auto.

:output — default :auto

An indication of which state component to extract

:steps — default :auto

A number of steps to run, or :auto, meaning run until the method returns. (Consider using :output :all when using :steps, especially if the computation may not complete after that many steps.)

:rule-alists — default nil

If non-nil, rule-alists to use (these completely replace the usual rule sets)

:extra-rules — default nil

Rules to add to the usual set of rules

:remove-rules — default nil

Rules to remove from the usual set of rules

:normalize-xors — default nil

Whether to normalize xor nests (t or nil)

:prune-branches-approximately — default nil

Whether to prune unreachable branches, using approximate contexts, during and after lifting (t, nil, or a dag size threshold). Can be slow but should not cause an exponential blowup.

:prune-branches-precisely — default nil

Whether to prune unreachable branches, using precise contexts, during and after lifting (t, nil, or a dag size threshold). Warning: Can take an exponential amount of time and space for DAGs with extensive sharing!

:call-stp — default nil

whether to call STP when pruning (t, nil, or a number of conflicts before giving up)

:memoizep — default t

Whether to memoize rewrites during unrolling (a boolean).

:branches — default :smart

How to handle branches in the execution. Either :smart (try to merge at join points) or :split (split the execution and don't re-merge).

:chunkedp — default nil

whether to divide the execution into chunks of steps (can help use early tests as assumptions when lifting later code)

:monitor — default nil

Rules to monitor (to help debug failures)

:print — default nil

How much to print (t or nil or :brief, etc.)

:print-interval — default nil

How often to print (number of nodes)

:produce-theorem — default nil

Whether to produce a theorem about the result of the lifting (currently has to be trusted).

:produce-function — default nil

Whether to produce a defun in addition to a DAG, a boolean.

:local — default t

Whether to make the result of unroll-java-code local to the enclosing book (or encapsulate). This prevents a large DAG from being stored in the certificate of the book, but it means that the result of unroll-java-code is not accessible from other books. Usually, the default value of t is appropriate, because the book that calls unroll-java-code is not included by other books.

Description:

Given a Java method, extract an equivalent term in DAG form, by symbolic execution including inlining all functions and unrolling all loops.

This event creates a defconst whose name is given by the defconst-name argument.

To inspect the resulting DAG, you can simply enter its name at the prompt to print it.