Lift a Java method to create a DAG, unrolling loops as needed.
(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 )
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).
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.
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.
An alist pairing array parameter names (symbols) with their lengths.
Classes to assume the JVM has already initialized (or :all)
Whether to assume exceptions do not happen (e.g., out-of-bounds array accesses)
Whether to assume JVM errors do not happen
whether to introduce vars for individual array elements (nil, t, or :bits)
Names to use for the parameters (e.g., if no debugging information is available), or :auto.
An indication of which state component to extract
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.)
If non-nil, rule-alists to use (these completely replace the usual rule sets)
Rules to add to the usual set of rules
Rules to remove from the usual set of rules
Whether to normalize xor nests (t or 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.
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!
whether to call STP when pruning (t, nil, or a number of conflicts before giving up)
Whether to memoize rewrites during unrolling (a boolean).
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).
whether to divide the execution into chunks of steps (can help use early tests as assumptions when lifting later code)
Rules to monitor (to help debug failures)
How much to print (t or nil or :brief, etc.)
How often to print (number of nodes)
Whether to produce a theorem about the result of the lifting (currently has to be trusted).
Whether to produce a defun in addition to a DAG, a boolean.
Whether to make the result of
unroll-java-codelocal 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-codeis not accessible from other books. Usually, the default value of tis appropriate, because the book that calls unroll-java-codeis not included by other books.
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
To inspect the resulting DAG, you can simply enter its name at the prompt to print it.