Skip to content

Files

Jump to bottom
Andrew Brown edited this page Mar 31, 2026 · 6 revisions

bin/

lifter/

Managing the intake of a binary file.

lifter_ir.ml

The IR and basic utilities.

type var = Memory of var | Add of var * int64 | Register of int | PC | SP | PSTATE

This enables us to handle memory-at-SP+8 (a common pattern) as a single variable. In theory it should probably be some sort of nested type

type register = Register of int | PC | SP | PSTATE
type var = Deref of register * int64 | Access of register

as this would make it intrinsic to the type that you can't have "R0+1" as a top-level variable, but it would also require more pattern matching most of the time in order to get through inner layers.

type instruction = {
  read : var list;
  write : var list;
  fence : bool;

  semantics : ASLp stmt list;
  readable : string;

  block : string;
  index : int;
}

The type for one lifted instruction. Read/write are all for particular accesses of variables. Loads and stores are considered to be reads and writes where the top-level 'var' is a Memory (see above).

type edge = Linear | Branch
type block = {
  name : string;
  offset : int;
  edges : (string * edge) list;
  instructions : instruction (Map.s with type key = int).t;
}
type blocks = block (Map.s with type key = string).t;

The type for the control-flow-graph of the function under investigation. A block is a series of sequential (except for reordering...) instructions. Blocks have edges to other blocks, a base64 uuid 'name', and an offset. The offset is useful for working out the absolute address of an instruction within the binary (for human-readable output).

lifter_elf.ml

GTIRB input. Reads through GTIRB files to find all basic blocks from the desired function.

Notably, the function-discovery is very overapproximate. A good improvement here would be to investigate how GDB, objdump, or other GNU tools perform their identification of what constitutes one function.

lifter_disassembly.ml

Takes GTIRB code blocks and feeds them to ASLp. Outputs types from lifter_ir.

A good improvement here would be to lift to a subset of bincaml IR and carry that around rather than carrying ASLp.

lifter.ml

val parse (filename : string) (component : string) : IR

Takes a filename, opens it, locates the function named "component", finds all of its instructions, lifts them via ASLp, and generates summaries of which vars are read/written/loaded/stored.

spec/

Managing the intake of the spec from the command-line.

spec_lang.ml

The language for the spec.

A good improvement here would be to just wholesale utilise bincaml's spec datastructures.

spec_parse.ml

An angstrom parser for the spec language.

spec_analysis.ml

Basic analysis for the spec. Ensures the spec isn't cyclic. Not much else.

spec.ml

Exposes

val input (commandline : string * string) : spec * spec

Takes two strings (from the commandline) and generates two specs.

solver/

solver_state.ml

Custom state type, enables resolving lots of the evaluation at an OCaml level.

  • state is a map of aliasing (string to string), a map of terms (string to term), and some constraints (string to string to term). Aliasing is stuff like "x" -> "MR0", terms are stuff like "MR0" -> actual term, and constraints are stuff like "locked" -> "x" -> true.

  • state_function is state -> string -> term option. Instructions and rely-conditions are lifted to state_functions to be applied.

  • state_constraints is state -> state -> Term.term option list Guarantee-conditions are lifted to state_constraints of two states to be added to cvc5.

This file also defines some functions to utilise these types:

  • initialise, reinitialise, link_aliases, add_preconditions: setting up and generating states
  • apply_inst applies an instruction
  • apply_pred applies a rely-condition (each of these have different behaviour: relies can be nondeterministic, which requires introducing new variables.
  • constrain_eq constrains that everything in two states that is named identically is actually equal
  • assert_over does an apply_inst, but it also adds state_constraints between the two functions.
  • find_opt and get_predicate enable other modules to get info out of a state
  • dump prints things

solver_utils.ml

Some pretty-printing for ASLp semantics, some pretty-printing for cvc5 objects, some generic setup routines that aren't dependent on a particular state.

solver_instruction.ml

Turns ASLp semantics into a state_function.

solver_spec.ml

Turns relies into a state_function and guarantees into state_constraints.

solver.ml

Exposes

val solve_all (...) (pairs : (instruction * instruction) list) : failure list

This takes a bunch of parameters, but the core behaviour is to filter alist of possibly-reorderable instruction pairs down to a list of specific failure conditions.

This involves taking all pairs, setting up the solver, then for each pair, generating all the states, then for each state, checking if it fails. This info then bubbles back up and we output only the list of states where things fail.

datalog.ml & reorderRules.dl

Files that interact with Datalog. reorderRules.dl defines the memory model itself, based on RISC-V. datalog.ml has code to read and process those rules.

There are lots of improvements here, related generally to some broad, structural improvements.

  • Datalog is the most "exponential" thing so far. With many instructions, the number of rules grows very quickly, which slows things down.
  • In combination with the ELF-lifting stuff, this is technically unsound, as programs may reorder cross-function.
  • Technically speaking, some aspects of reordering may occur on a sub-instruction basis, i.e. it may be the two underlying memory writes that reorder rather than the two instructions that contain memory writes.

Suggested improved approach: use a partial-evaluation approach. Beginning at the start of the desired function, partially evaluate the code and collect possibly-reorderable memory operations within some sliding window of instructions (pipeline size + extra space to capture cache behaviour).

main.ml

Read command-line flags and call into everything else.

lib/

External-ish stuff.

gtirb/

Submodule of the main GTIRB repo https://github.com/GrammaTech/gtirb Holds the relevant protobuf definitions.

ocaml_cvc5/

Submodule of some cvc5 OCaml bindings https://github.com/formalsec/ocaml-cvc5 Mostly just lets OCaml call into C++ to access CVC5. Very easy to extend.

llvm_disass/

Code taken from https://github.com/UQ-PAC/gtirb-semantics/pull/6 Hooks into LLVM to provide human-readable disassembly. Very useful for outputting "failures" to a user.

option.ml

Adds one helper to Option types that's just get but with a non-generic error message (i.e. instead of Invalid_argument it throws Failure(GTIRB IR does not exist) or something.)

Clone this wiki locally