Module compare 

Provides various ways to compare crate::encoding::Encodings.

Some of the comparisons require an crate::smt::SmtSolver. You can use the liblisa-z3 crate to import bindings to the Z3 SMT solver.

Modules

summary

A condensed summary of the architecture comparison, suitable for export to a file.

Structs

AddressComparisonOptions

Options for comparing MemoryAccesses.

ComparisonMatrix

A matrix of pairwise comparisons between all architectures.

EncodingComparisonOptions

Options for comparing Encodings.

EncodingGroup

For each architecture, a group of overlapping encodings.

Equivalence

The result of encodings_semantically_equal. Semantics are guaranteed to be equivalent if equal && !timeout holds.

PartIndexMapping

A mapping between part indices of two encodings.

Row

A row in the architecture comparison table.

RowKey

The key for a row in an architecture comparison table. All encodings that have the same RowKey should be grouped into the same row.

Rows

A collection of rows.

Enums

ComparisonResult

The result of a pairwise comparison between two encodings.

ComputationEquivalence

Represents the equivalence between two encodings.

Functions

compute_split_filters

Splits the encoding group into multiple groups, such that each group contains encodings that cover the exact same space. This function is one-to-many. That is, it will generate many smaller groups that each cover a small subset.

encoding_addresses_equal

Compares the MemoryAcesses of the two encodings, and returns whether they are equal.

encoding_dataflows_structurally_equal

Determines if the dataflows of the encodings provided are equal, ignoring the actual computations. Only compares the overlapping parts of the covered instruction space.

encodings_semantically_equal

Determines whether two encodings are semantically equivalent.

encodings_structurally_equal

Only compares the overlapping parts of the covered instruction space.