The mem Plugin

See also

mim::plug::mem

Dependencies

import compile;
plugin core;

Types

M

The effect token core.M.

anx M = core.M;

Ptr

The pointer type core.Ptr.

anx Ptr = core.Ptr;
 
anx lam Ptr0 (T: *): * = Ptr (T, 0);

Char & Str

A character and a pointer to a string of n of them.

anx let Char = I8;
anx lam Str (n: Nat): * = Ptr0 «n; Char»;

Operations w/ Side Effects

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

load

Loads the pointee of type T from a pointer of type mem.Ptr (T, a).

axm load: {T: *, a: Nat} as Ta → [M a, Ptr Ta] → [M a, T], normalize_load;

store

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

axm store: {T: *, a: Nat} as Ta → [M a, Ptr Ta, T] → M a, normalize_store;

fresh

Passes a fresh mem.M a for address space a to its return continuation: ret mem = mem.fresh $ 0. Conversion-only phases (e.g. tensor.lower_to_mem) emit memory operations before memory has been threaded. Each call site's return continuation is a distinct mutable, so the received memories are distinct by construction - hash-consing cannot collapse two otherwise identical memory operations into one. mem.add_mem resolves each call by jumping to the continuation with the memory that is current at that point.

axm fresh: Fn [a: Nat] → M a;

alloc

Allocates memory of type T in address space a.

axm alloc: [*, a: Nat] as Ta → [M a] → [M a, Ptr Ta];

slot

Reserves a stack slot for type T in address space a. The slot is passed to the continuation and its lifetime is scoped to that continuation.

axm slot: [*, a: Nat] as Ta → Fn M a → [M a, Ptr Ta];

malloc

Allocates memory of type T in address space a. The difference to mem.alloc is that the size is passed explicitly (in bytes) instead of being derived from T.

axm malloc: [*, a: Nat] as Ta → [M a, Nat] → [M a, Ptr Ta];

free

Frees memory of type T in address space a.

axm free: {*, a: Nat} as Ta → [M a, Ptr Ta] → M a;

mslot

Reserves a stack slot for type T in address space a. The reserved slot will be size bytes large. The slot is passed to the continuation and its lifetime is scoped to that continuation.

axm mslot: [*, a: Nat] as Ta → Fn [M a, size: Nat] → [M a, Ptr Ta];

Operations w/o Side Effects

lea

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

axm lea: {n: Nat, Ts: «n; *», a: Nat} → [Ptr («j: n; Ts#j», a), i: Idx n] → Ptr (Ts#i, a), normalize_lea;

decay

Pointer to the first element of an array, akin to C's array-to-pointer decay.

anx lam decay {n: Nat, T: *, a: Nat} (p: Ptr («n; T», a)): Ptr (T, a) = lea (p, 0:(Idx n));

assume

Views p as a pointer to an array of n elements.

Warning

This is unchecked: the caller vouches for the length, e.g. for memory a C function hands over.

axm assume: {T: *, a: Nat} as Ta → [Ptr Ta, n: Nat] → Ptr («n; T», a);

cstr

Views a NUL-terminated C string p as an array of its n characters, excluding the NUL.

Warning

This is unchecked: p must actually point to a NUL-terminated string.

anx fun cstr (m: M 0, p: Ptr0 Char): [M 0, n: Nat, Str n] =
    loop (m, 0)
    where
        con loop (m: M 0, i: Nat) =
            let n      = core.nat.add (i, 1);
            let (m, c) = load (m, lea (assume (p, n), core.idx 0 n i));
            (next, done)#(core.icmp.e (c, 0I8)) m
            where
                con next (m: M 0) = loop (m, n);
                con done (m: M 0) = return (m, i, assume (p, i));
            end
    end;

Phases

add_mem

Threads mem.M through functions that lack it.

axm add_mem: compile.Phase;

free_locals

Frees the memory a function allocates but does not let escape (see mim::plug::mem::EscapeAnalysis).

axm free_locals: compile.Phase;

heap2stack

Turns a small mem.alloc that does not escape its function into a mem.slot (see mim::plug::mem::phase::Heap2Stack). -X mem:heap2stack=<n> sets the maximum number of elements to stack-allocate; 0 disables it.

axm heap2stack: compile.Phase;

seo

Symbolic Expression Optimization — SSA construction, expression propagation, and GVN in one fixed point (see mim::plug::mem::phase::SEO).

axm seo: compile.Phase;

alloc2malloc_repl

Rewrites mem.alloc / mem.slot into mem.malloc / mem.mslot.

axm alloc2malloc_repl: compile.Phase;