		Search-engine friendly clone of the ACL2 documentation.

Def-unrolled

A tool to lift RISC-V binary code into logic, unrolling loops as needed.

Description:

Lift some risc-v 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
              &key
              :target                ; default :entry-point
              :executable            ; default :none
              :output                ; default :all
              :extra-assumptions     ; default nil
              :stack-slots           ; default 100
              :existing-stack-slots  ; default :auto
              :position-independent  ; default nil
              :prune-precise         ; default 1000
              :prune-approx          ; default t
              :extra-rules           ; default nil
              :remove-rules          ; default nil
              :step-limit            ; default 1000000
              :step-increment        ; default 100
              :memoizep              ; default t
              :monitor               ; default nil
              :normalize-xors        ; default nil
              :count-hits            ; default nil
              :print                 ; default :brief
              :print-base            ; default 10
              :max-printed-term-size ; default 10000
              :untranslatep          ; default t
              )

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.

:target — default :entry-point

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

:executable — default :none

The RISC-V binary executable that contains the target function. Usually this is a string representing the file name/path of the executable. However, it can instead be a parsed executable (satisfying parsed-executablep).

:output — default :all

An indication of which state component(s) will hold the result of the computation being lifted. After lifting, the indicated result is projected out so that the result of lifting only represented the indicated state component. The value supplied for this option can be :all (meaning return the whole state) or one of the values allowed by wrap-in-normal-output-extractor.

:extra-assumptions — default nil

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

:stack-slots — default 100

How much unused stack space to assume is available, in terms of the number of stack slots, which are 4 bytes for 32-bit executables and 8 bytes for 64-bit executables. The stack will expand into this space during (symbolic) execution.

:existing-stack-slots — default :auto

How much available stack space to assume exists. Usually at least 1, for the saved return address.

:position-independent — default nil

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

: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.

: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.

: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.

:max-printed-term-size — default 10000

Max term-size of a DAG that is allowed to be printed as a term. Larger DAGs will be printed as DAGs, not terms.

:untranslatep — default t

Whether to untranslate terms when printing.