#instructions #smt-solver #x86-64 #analysis #cpu #discovery #encoding

nightly liblisa

A tool for automated discovery and analysis of the ISA of a CPU

2 releases

0.1.1 Sep 2, 2024
0.1.0 Aug 30, 2024

#515 in Algorithms

Download history 123/week @ 2024-08-26 164/week @ 2024-09-02

287 downloads per month
Used in 4 crates

AGPL-3.0-only

1.5MB
36K SLoC

libLISA is a library for automated discovery and analysis of CPU instructions. This crate is the core library that can be used to load and manipulate already-analyzed datasets. Several separate crates are available for enumeration, synthesis and architecture support:

Loading semantics from disk

Encodings support serde, and can be serialized and deserialized by any library that supports serde. By default, libLISA uses JSON. You can import these semantics as follows:

use std::fs::File;
use std::io::BufReader;
use std::path::PathBuf;

use liblisa::encoding::Encoding;
use liblisa::semantics::default::computation::SynthesizedComputation;
use liblisa::arch::x64::X64Arch;

let file = File::open("semantics.json").unwrap();
let reader = BufReader::new(file);
let semantics: Vec<Encoding<X64Arch, SynthesizedComputation>> =
    serde_json::from_reader(reader).unwrap();

See encoding::Encoding for how these semantics can be used.

Features

  • z3: adds the z3 crate as a dependency, and enables the Z3 implementation for smt::SmtSolver.
  • x64-undef: enables the arch::x64::undef namespace, which uses the XED disassembler library to provide definitions for undefined behavior.

Dependencies

~30MB
~603K SLoC