The mem Plugin

Table of Contents

• Dependencies
• Types
  • %mem.M
  • %mem.Ptr
• Operations w/ Side Effects
  • %mem.load
  • %mem.store
  • %mem.remem
  • %mem.alloc
  • %mem.slot
  • %mem.malloc
  • %mem.free
  • %mem.mslot
• Operations w/o Side Effects
  • %mem.lea
  • %mem.create/destroy
• Passes and Phases
  • Misc
  • Passes
  • Phases

See also

mim::plug::mem

Dependencies

import compile;

Types

%mem.M

This type tracks all kind of side-effects.

axm %mem.M: *;

%mem.Ptr

Pointer type with pointee type T and address space as. At the moment, the address space is not really used and a placeholder for future work.

axm %mem.Ptr: [*, Nat] → *;
 
lam %mem.Ptr0(T: *): * = %mem.Ptr (T, 0);

Operations w/ Side Effects

The following operations have side effects. For this reason, they consume a %mem.M and yield a new %mem.M.

%mem.load

Loads from a pointer of type %mem.Ptr (T, as) the pointed value of type T.

axm %mem.load: {T: *, Nat}::Tas [%mem.M, %mem.Ptr Tas] → [%mem.M, T], normalize_load;

%mem.store

Stores a value of type T to the location pointed to by a pointer of type %mem.Ptr (T, as),

axm %mem.store: {T: *, Nat}::Tas [%mem.M, %mem.Ptr Tas, T] → %mem.M, normalize_store;

%mem.remem

Creates a new dummy %mem.M-typed value in order to acknowledge the fact that some unspecified side-effect happened.

axm %mem.remem: %mem.M → %mem.M, normalize_remem;

%mem.alloc

Allocates memory of type T in address space as.

axm %mem.alloc: [*, Nat]::Tas [%mem.M] → [%mem.M, %mem.Ptr Tas];

%mem.slot

Reserves a memory slot for type T in address space as. id has to be provided a unique id.

axm %mem.slot: [*, Nat]::Tas [%mem.M, id: Nat] → [%mem.M, %mem.Ptr Tas];

%mem.malloc

Allocates memory of type T in address space as. The difference to %mem.alloc is that the size is automatically inferred.

axm %mem.malloc: [*, Nat]::Tas [%mem.M, Nat] → [%mem.M, %mem.Ptr Tas];

%mem.free

Frees memory of type T in address space as.

axm %mem.free: {*, Nat}::Tas [%mem.M, %mem.Ptr Tas] → %mem.M;

%mem.mslot

Reserves a memory slot for type T in address space as. The reserved slot will be size bytes large. id has to be provided an unique id.

axm %mem.mslot: [*, Nat]::Tas [%mem.M, size: Nat, id: Nat] → [%mem.M, %mem.Ptr Tas];

Operations w/o Side Effects

%mem.lea

Load effective address. Performs address computation by offsetting the passed pointer with index i.

axm %mem.lea: [n: Nat, Ts: «n; *», as: Nat][%mem.Ptr («j: n; Ts#j», as), i: Idx n] → %mem.Ptr (Ts#i, as), normalize_lea;

%mem.create/destroy

Create side effect out of thin or pretend that the side effect does not exists.

Warning

Use with caution since you completely remove the %mem.M dependency.

let %mem.m = ⊤:%mem.M;
lam %mem.ignore {O: *} (_: %mem.M, o: O): O = o;
lam %mem.rm (n: Nat, Is: «n; *», O: *)
             (f: [%mem.M, «i: n; Is#i»] → [%mem.M, O])
             (is: «i: n; Is#i»): O
    = %mem.ignore (f (%mem.m, is));

Passes and Phases

Misc

Reshape mode enum.

axm %mem.reshape_mode: *;
axm %mem.reshape_flat: %mem.reshape_mode;
axm %mem.reshape_arg:  %mem.reshape_mode;

Passes

SSA pass expects eta expansion as argument

axm %mem.ssa_pass: %compile.Pass → %compile.Pass;

Copy propagation expects beta reduction and eta expansion as argument.

axm %mem.copy_prop_pass:    [%compile.Pass, %compile.Pass, Bool] → %compile.Pass;
axm %mem.remem_elim_pass:   %compile.Pass;
axm %mem.alloc2malloc_pass: %compile.Pass;
axm %mem.reshape_pass:      %mem.reshape_mode → %compile.Pass;

Phases

axm %mem.add_mem_phase: %compile.Phase;
 
let mem_opt_pass_list =
    let beta_red = %compile.beta_red_pass;
    let eta_red  = %compile.eta_red_pass;
    let eta_exp  = %compile.eta_exp_pass eta_red;
    %compile.pass_list
        beta_red
        eta_red
        eta_exp
        (%mem.ssa_pass eta_exp)
        (%mem.copy_prop_pass (beta_red, eta_exp, ff));
 
let mem_opt_phase  = %compile.pass_phase mem_opt_pass_list;
let mem_prep_phase = %compile.passes_to_phase (⊤:Nat) (%mem.remem_elim_pass, %mem.alloc2malloc_pass);