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
• Phases

See also

mim::plug::mem

Dependencies

import compile;

Types

%mem.M

This type tracks all kinds of side effects in the given address space.

axm %mem.M: Nat → *;

%mem.Ptr

Pointer type with pointee type T and address space a. At the moment, the address space is not really used and serves as 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 a and yield a new %mem.M a.

%mem.load

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

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

%mem.store

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

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

%mem.remem

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

axm %mem.remem: {a: Nat} → %mem.M a → %mem.M a, normalize_remem;

%mem.alloc

Allocates memory of type T in address space a.

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

%mem.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 %mem.slot: [*, a: Nat] as Ta → Fn %mem.M a → [%mem.M a, %mem.Ptr Ta];

%mem.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 %mem.malloc: [*, a: Nat] as Ta → [%mem.M a, Nat] → [%mem.M a, %mem.Ptr Ta];

%mem.free

Frees memory of type T in address space a.

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

%mem.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 %mem.mslot: [*, a: Nat] as Ta → Fn [%mem.M a, size: Nat] → [%mem.M a, %mem.Ptr Ta];

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; *», a: Nat} → [%mem.Ptr («j: n; Ts#j», a), i: Idx n] → %mem.Ptr (Ts#i, a), normalize_lea;

Phases

• add_mem: threads %mem.M through functions that lack it.
• seo: Symbolic Expression Optimization - SSA construction, expression propagation, and GVN in one fixed point (see mim::plug::mem::phase::SEO).
• remem_repl: removes %mem.remems.
• alloc2malloc_repl: rewrites %mem.alloc / %mem.slot into %mem.malloc / %mem.mslot.

axm %mem.add_mem:           %compile.Phase;
axm %mem.seo:               %compile.Phase;
axm %mem.remem_repl:        %compile.Phase;
axm %mem.alloc2malloc_repl: %compile.Phase;