		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                 ; 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 — default nil

whether to aggressively prune unreachable branches in the result

: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 unrolling all loops.

This event creates a defconst whose name is defconst-name.

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