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.