		Search-engine friendly clone of the ACL2 documentation.

Prove-functions-equivalent

A tool to prove two x86 binary functions equivalent.

Description:

This runs def-unrolled twice, once for each executable, and then tries to prove the two resulting lifted computations equal using rewriting and SMT solving.

General Form:

(prove-functions-equivalent executable1
                            target1
                            inputs1
                            output1
                            executable2
                            target2
                            inputs2
                            output2
                            &key
                            :extra-rules ; default nil
                            :count-hits  ; default :auto
                            :print       ; default :auto
                            )

Inputs:

executable1 — (required)

The first executable. Usually a string (a filename).

target1 — (required)

The target to lift in the first executable. See the :target option of def-unrolled.

inputs1 — (required)

Information about the inputs of the first executable. See the :inputs option of def-unrolled. Corresponding inputs should have the same names in the :inputs2 below.

output1 — (required)

Which output to extract from the first executable. See the :output option of def-unrolled.

executable2 — (required)

The second executable. Usually a string (a filename).

target2 — (required)

The target to lift in the second executable. See the :target option of def-unrolled.

inputs2 — (required)

Information about the inputs of the second executable. See the :inputs option of def-unrolled. Corresponding inputs should have the same names in the :inputs1 above.

output2 — (required)

Which output to extract from the second executable. See the :output option of def-unrolled.

:extra-rules — default nil

Extra rules to use during lifting.

:count-hits — default :auto

Whether to count rewrite rule hits.

:print — default :auto

Verbosity level.