		Search-engine friendly clone of the ACL2 documentation.

Def-unrolled

A tool to lift x86 binary code into logic, unrolling loops as needed.

Description:

Lift some x86 binary code into an ACL2 representation, by symbolic execution including inlining all functions and unrolling all loops.

Usually, def-unrolled creates both a function representing the lifted code (in term or DAG form, depending on the size) and a defconst whose value is the corresponding DAG (or, rarely, a quoted constant). The function's name is lifted-name and the defconst's name is created by adding stars around lifted-name.

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

General Form:

(def-unrolled lifted-name
              executable
              &key
              :target                          ; default :entry-point
              :inputs                          ; default :skip
              :output                          ; default :all
              :extra-assumptions               ; default nil
              :suppress-assumptions            ; default nil
              :inputs-disjoint-from            ; default :code
              :stack-slots                     ; default 100
              :position-independent            ; default :auto
              :type-assumptions-for-array-vars ; default t
              :use-internal-contextsp          ; default t
              :prune-precise                   ; default 1000
              :prune-approx                    ; default t
              :extra-rules                     ; default nil
              :remove-rules                    ; default nil
              :extra-assumption-rules          ; default nil
              :remove-assumption-rules         ; default nil
              :step-limit                      ; default 1000000
              :step-increment                  ; default 100
              :stop-pcs                        ; default nil
              :memoizep                        ; default t
              :monitor                         ; default nil
              :normalize-xors                  ; default nil
              :count-hits                      ; default nil
              :print                           ; default :brief
              :print-base                      ; default 10
              :untranslatep                    ; default t
              :produce-function                ; default t
              :non-executable                  ; default :auto
              :produce-theorem                 ; default nil
              :prove-theorem                   ; default nil
              :restrict-theory                 ; default t
              :bvp                             ; default nil
              )

Inputs:

lifted-name — (required)

A symbol, the name to use for the generated function. The name of the generated constant is created by adding stars to the front and back of this symbol.

executable — (required)

The x86 binary executable that contains the target function. Usually a string (a filename), or this can be a parsed executable of the form created by defconst-x86.

:target — default :entry-point

Where to start lifting (a numeric offset, the name of a subroutine (a string), or the symbol :entry-point)

:inputs — default :skip

Either the special value :skip (meaning generate no additional assumptions on the input) or a doublet list pairing input names with types. Types include things like u32, u32*, and u32[2].

:output — default :all

An indication of which state component(s) will hold the result of the computation being lifted. See output-indicatorp.

:extra-assumptions — default nil

Extra assumptions for lifting, in addition to the standard-assumptions

:suppress-assumptions — default nil

Whether to suppress the standard assumptions. This does not suppress any assumptions generated about the :inputs.

:inputs-disjoint-from — default :code

What to assume about the inputs (specified using the :inputs option) being disjoint from the sections/segments in the executable. The value :all means assume the inputs are disjoint from all sections/segments. The value :code means assume the inputs are disjoint from the code/text section. The value nil means do not include any assumptions of this kind.

:stack-slots — default 100

How much available stack space to assume exists.

:position-independent — default :auto

Whether to attempt the lifting without assuming that the binary is loaded at a particular position.

:type-assumptions-for-array-vars — default t

Whether to put in type assumptions for the variables that represent elements of input arrays.

:use-internal-contextsp — default t

Whether to use contextual information from ovararching conditionals when simplifying DAG nodes.

:prune-precise — default 1000

Whether to prune DAGs using precise contexts. Either t or nil or a natural number representing the smallest dag size that we deem too large for pruning (where here the size is the number of nodes in the corresponding term). This kind of pruning can blow up if attempted for DAGs that represent huge terms.

:prune-approx — default t

Whether to prune DAGs using approximate contexts. Either t or nil or a natural number representing the smallest dag size that we deem too large for pruning (where here the size is the number of nodes in the corresponding term). This kind of pruning should not blow up but doesn't use fully precise contextual information.

:extra-rules — default nil

Rules to use in addition to (unroller-rules32) or (unroller-rules64) plus a few others.

:remove-rules — default nil

Rules to turn off.

:extra-assumption-rules — default nil

Extra rules to be used when simplifying assumptions.

:remove-assumption-rules — default nil

Rules to be removed when simplifying assumptions.

:step-limit — default 1000000

Limit on the total number of symbolic executions steps to allow (total number of steps over all branches, if the simulation splits).

:step-increment — default 100

Number of model steps to allow before pausing to simplify the DAG and remove unused nodes.

:stop-pcs — default nil

A list of program counters (natural numbers) at which to stop the execution, for debugging.

:memoizep — default t

Whether to memoize during rewriting (when not using contextual information -- as doing both would be unsound).

:monitor — default nil

Rule names (symbols) to be monitored when rewriting.

:normalize-xors — default nil

Whether to normalize BITXOR and BVXOR nodes when rewriting (t, nil, or :compact).

:count-hits — default nil

Whether to count rule hits during rewriting (t means count hits for every rule, :total means just count the total number of hits, nil means don't count hits)

:print — default :brief

Verbosity level.

:print-base — default 10

Base to use when printing during lifting. Must be either 10 or 16.

:untranslatep — default t

Whether to untranslate term when printing.

:produce-function — default t

Whether to produce a function, not just a constant DAG, representing the result of the lifting.

:non-executable — default :auto

Whether to make the generated function non-executable, e.g., because stobj updates are not properly let-bound. Either t or nil or :auto.

:produce-theorem — default nil

Whether to try to produce a theorem (possibly skip-proofed) about the result of the lifting.

:prove-theorem — default nil

Whether to try to prove the theorem with ACL2 (rarely works, since Axe's Rewriter is different and more scalable than ACL2's rewriter).

:restrict-theory — default t

To be deprecated...

:bvp — default nil

Whether to use new-style, BV-friendly assumptions.