InSPECtor

Source code for "InSPECtor: Improving SLEIGH Processor Specification Veracity via Proxy"

Quickstart

First, ensure that the required dependencies are installed including:

• rustup
• Docker
• Optional Nu Shell

GenSYS

GenSYS is a tool for generating test cases for a given SLEIGH specification using symbolic execution. More information about how to use it, and instructions on generating paper data related to test case generation, is avaliable under its readme here.

Usage: gensys [OPTIONS] <COMMAND>

Commands:
  generate        Generate instructions that cover every possible constructor (subject to the selected filtering strategy)
  generate-state  Generate states for the instructions stored in `dir`
  list            List all languages supported by the generator
  info            Display information about a specific SLEIGH language ID
  paper-data      Generate results for all Gensys configurations and compute final coverage statistics
  debug           Run an internal command used for testing
  help            Print this message or the help of the given subcommand(s)

Options:
      --ghidra-src <GHIDRA_SRC>  The ghidra directory to use for generation/testing [env: GHIDRA_SRC=] [default: ../ghidra/]
  -h, --help                     Print help

Juxtaplayer

Juxtaplayer is a tool for executing individual instructions and comparing the results between two different implementations. More information about how to use it is avaliable under its readme here.

Usage: juxtaplayer [OPTIONS] <COMMAND>

Commands:
  test        Evaluate the behavior of a set of instruction on a specific target
  test-one    Execute a single testcase parsed from the arguments
  diff        Compute the differences between two test results
  diff-one    Execute a single test case on two targets computing a diff of the final state
  paper-data  Commands for generating and evaluating data for the Inspector paper
  debug       Commands used for development and testing. Not intended for public use
  help        Print this message or the help of the given subcommand(s)

Options:
      --instr-addr <INSTR_ADDR>  The base address to use for testing
      --ghidra-src <GHIDRA_SRC>  The ghidra directory to use for generation/testing [env: GHIDRA_SRC=] [default: ../ghidra/]
  -t, --threads <THREADS>        The maximum number of threads to use for execution. If `0` then the runtime will use the number of logical threads supported by the processor [default: 0]
  -v, --verbose                  Run with verbose output
  -h, --help                     Print help

Generating Graphs

Once the paper data or ablation study data has been generated for both GenSYS and JuxtaPlayer the graphs can be generated with the helper scripts.

nu ./scripts/inspector.nu generation-table
nu ./scripts/inspector.nu ablation-study

License

Inspector is dual-licensed under either:

• MIT License (LICENSE-MIT)
• OR Apache License, Version 2.0 (LICENSE-APACHE)