Given a Java method, define a function that represents the (unrolled) effect of the given method on the JVM state (under the given assumptions). This uses symbolic execution including unrolling all loops.
(unroll-java-code2 fn method-indicator &key :array-length-alist ; default nil :assumptions ; default nil :classes-to-assume-initialized ; default :all :classes-to-assume-uninitialized ; default nil :ignore-exceptions ; default nil :ignore-errors ; default nil :extra-rules ; default nil :remove-rules ; default nil :rule-alists ; default nil :monitor ; default nil :prove-with-acl2 ; default t :print ; default :brief :abstract-state-components ; default nil :prune-branches ; default t :call-stp ; default nil :param-names ; default :auto :extra-proof-rules ; default nil :print-interval ; default 1000 :steps ; default :auto )
The name of the function to create
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.
An alist pairing array parameters with their sizes
Assumptions about the initial state, S.
Classes to assume the JVM has already initialized, or :all
Classes to assume the JVM has not 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
Rules to add to the usual set of rules
Rules to remove from the usual set of rules
If non-nil, rule-sets to use to completely replace the usual rule sets
Rules to monitor (to help debug failures)
Attempt to sanity check the result by proving it with ACL2
Verbosity level (passed to the Axe rewriter)
Whether to define functions abstracting how the state components are updated
whether to aggressively prune unreachable branches in the result
whether to call STP when pruning (t, nil, or a number of conflicts before giving up)
Names to use for the parameters (e.g., if no debugging information is available), or :auto.
Extra rules to support proving the result with ACL2
Number of DAG nodes to create before printing intermediate results (or nil for no limit).
A number of steps to run. A natural number (for debugging only), or :auto, meaning run until the method returns.
This uses lifting theorems for subroutine calls that have already been lifted. Otherwise, it effectively inlines the subroutine call.
To inspect the resulting form, you can use