Module Llair

LLAIR (Low-Level Analysis Internal Representation) is an IR tailored for static analysis using a low-level model of memory.

module Loc : sig ... end

Source code debug locations

module Typ : sig ... end

Types

module Reg : sig ... end

Variables

module Exp : sig ... end

Expressions

module FuncName : sig ... end

Function names

module Global : sig ... end

Globals

module GlobalDefn : sig ... end

Global variables

val cct_schedule_points : bool Stdlib.ref
module Builtin : sig ... end
module Intrinsic : sig ... end
type inst = private
  1. | Move of {
    1. reg_exps : (Reg.t * Exp.t) NS.iarray;
    2. loc : Loc.t;
    }
    (*

    Move each value exp into corresponding register reg. All of the moves take effect simultaneously.

    *)
  2. | Load of {
    1. reg : Reg.t;
    2. ptr : Exp.t;
    3. len : Exp.t;
    4. loc : Loc.t;
    }
    (*

    Read a len-byte value from the contents of memory at address ptr into reg.

    *)
  3. | Store of {
    1. ptr : Exp.t;
    2. exp : Exp.t;
    3. len : Exp.t;
    4. loc : Loc.t;
    }
    (*

    Write len-byte value exp into memory at address ptr.

    *)
  4. | AtomicRMW of {
    1. reg : Reg.t;
    2. ptr : Exp.t;
    3. exp : Exp.t;
    4. len : Exp.t;
    5. loc : Loc.t;
    }
    (*

    Atomically load a len-byte value val from the contents of memory at address ptr, set reg to val, and store the len-byte value of (λreg. exp) val into memory at address ptr. Note that, unlike other instructions and arguments, occurrences of reg in exp refer to the new, not old, value.

    *)
  5. | AtomicCmpXchg of {
    1. reg : Reg.t;
    2. ptr : Exp.t;
    3. cmp : Exp.t;
    4. exp : Exp.t;
    5. len : Exp.t;
    6. len1 : Exp.t;
    7. loc : Loc.t;
    }
    (*

    Atomically load a len-byte value from the contents of memory at address ptr, compare the value to cmp, and if equal store len-byte value exp into memory at address ptr. Sets reg to the loaded value concatenated to a len1-byte value 1 if the store was performed, otherwise 0.

    *)
  6. | Alloc of {
    1. reg : Reg.t;
    2. num : Exp.t;
    3. len : int;
    4. loc : Loc.t;
    }
    (*

    Allocate a block of memory large enough to store num elements of len bytes each and bind reg to the first address.

    *)
  7. | Free of {
    1. ptr : Exp.t;
    2. loc : Loc.t;
    }
    (*

    Deallocate the previously allocated block at address ptr.

    *)
  8. | Nondet of {
    1. reg : Reg.t option;
    2. msg : string;
    3. loc : Loc.t;
    }
    (*

    Bind reg to an arbitrary value, representing non-deterministic approximation of behavior described by msg.

    *)
  9. | Builtin of {
    1. reg : Reg.t option;
    2. name : Builtin.t;
    3. args : Exp.t NS.iarray;
    4. loc : Loc.t;
    }
    (*

    Bind reg to the value of applying builtin name to args.

    *)

Instructions for memory manipulation or other non-control effects.

type cmnd = inst NS.iarray

A (straight-line) command is a sequence of instructions.

type label = string

A label is a name of a block.

type jump = private {
  1. mutable dst : block;
  2. mutable retreating : bool;
}

A jump to a block.

and call_target = {
  1. mutable func : func;
  2. mutable recursive : bool;
    (*

    Holds unless this call target is definitely not recursive

    *)
}
and icall_target = {
  1. ptr : Exp.t;
    (*

    Dynamically resolved function pointer.

    *)
  2. mutable candidates : call_target NS.iarray;
    (*

    Statically computed over-approximation of possible call targets.

    *)
}
and callee =
  1. | Direct of call_target
    (*

    Statically resolved function

    *)
  2. | Indirect of icall_target
    (*

    Dynamically resolved function

    *)
  3. | Intrinsic of Intrinsic.t
    (*

    Intrinsic implemented in analyzer rather than source code

    *)
and 'a call = {
  1. callee : 'a;
  2. typ : Typ.t;
    (*

    Type of the callee.

    *)
  3. actuals : Exp.t NS.iarray;
    (*

    Actual arguments.

    *)
  4. areturn : Reg.t option;
    (*

    Register to receive return value.

    *)
  5. return : jump;
    (*

    Return destination.

    *)
  6. throw : jump option;
    (*

    Handler destination.

    *)
  7. loc : Loc.t;
}

A call to a function.

and term = private
  1. | Switch of {
    1. key : Exp.t;
    2. tbl : (Exp.t * jump) NS.iarray;
    3. els : jump;
    4. loc : Loc.t;
    }
    (*

    Invoke the jump in tbl associated with the integer expression case which is equal to key, if any, otherwise invoke els.

    *)
  2. | Iswitch of {
    1. ptr : Exp.t;
    2. tbl : jump NS.iarray;
    3. loc : Loc.t;
    }
    (*

    Invoke the jump in tbl whose dst is equal to ptr.

    *)
  3. | Call of callee call
    (*

    Call function with arguments.

    *)
  4. | Return of {
    1. exp : Exp.t option;
    2. loc : Loc.t;
    }
    (*

    Invoke return of the dynamically most recent Call.

    *)
  5. | Throw of {
    1. exc : Exp.t;
    2. loc : Loc.t;
    }
    (*

    Invoke throw of the dynamically most recent Call with throw not None.

    *)
  6. | Abort of {
    1. loc : Loc.t;
    }
    (*

    Trigger abnormal program termination

    *)
  7. | Unreachable
    (*

    Halt as control is assumed to never reach Unreachable.

    *)

Block terminators for function call/return or other control transfers.

and block = private {
  1. lbl : label;
  2. cmnd : cmnd;
  3. term : term;
  4. mutable parent : func;
  5. mutable sort_index : int;
    (*

    Position in a topological order, ignoring retreating edges.

    *)
  6. mutable goal_distance : int;
    (*

    An upper bound on the distance from this block to the end of the current goal trace, measured in blocks.

    *)
}

A block is a destination of a jump with arguments, contains code.

and func = private {
  1. name : FuncName.t;
  2. formals : Reg.t NS.iarray;
    (*

    Formal parameters

    *)
  3. freturn : Reg.t option;
  4. fthrow : Reg.t;
  5. locals : Reg.Set.t;
    (*

    Local registers

    *)
  6. entry : block;
  7. loc : Loc.t;
}

A function is a control-flow graph with distinguished entry block, whose parameters are the function parameters.

type ip
type functions = func FuncName.Map.t
type program = private {
  1. globals : GlobalDefn.t NS.iarray;
    (*

    Global definitions.

    *)
  2. functions : functions;
    (*

    (Global) function definitions.

    *)
}
module Inst : sig ... end
module Jump : sig ... end
module Term : sig ... end
module Block : sig ... end
module IP : sig ... end
module Func : sig ... end
module Program : sig ... end