• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
    • Axe
      • R1cs-verification-with-axe
      • Prove-equal-with-axe
      • Dags
      • Stp
      • Lifters
        • Unroll-java-code
        • Unroll-java-code2
      • Read-jar
      • Read-class
    • Execloader
  • Math
  • Testing-utilities

• Lifters

Unroll-java-code2

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.

General Form:

(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
                   )

Inputs:

fn — (required)

The name of the function to create

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.

:array-length-alist — default nil

An alist pairing array parameters with their sizes

:assumptions — default nil

Assumptions about the initial state, S.

:classes-to-assume-initialized — default :all

Classes to assume the JVM has already initialized, or :all

:classes-to-assume-uninitialized — default nil

Classes to assume the JVM has not 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

: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

:rule-alists — default nil

If non-nil, rule-sets to use to completely replace the usual rule sets

:monitor — default nil

Rules to monitor (to help debug failures)

:prove-with-acl2 — default t

Attempt to sanity check the result by proving it with ACL2

:print — default :brief

Verbosity level (passed to the Axe rewriter)

:abstract-state-components — default nil

Whether to define functions abstracting how the state components are updated

:prune-branches — default t

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)

:param-names — default :auto

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

:extra-proof-rules — default nil

Extra rules to support proving the result with ACL2

:print-interval — default 1000

Number of DAG nodes to create before printing intermediate results (or nil for no limit).

:steps — default :auto

A number of steps to run. A natural number (for debugging only), or :auto, meaning run until the method returns.

Description:

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 print-list on the generated defconst.