-- | Primitives for constructing and destructing 32-bit heap objects. -- -- IMPORTANT: Only one of 'Object64' or 'Object32' is linked into the DDC -- runtime system. It is also the /only/ module that knows about the layout -- of heap objects. All access to heap objects must go through the interface -- provided by this module. -- -- All 32-bit heap objects start with a 32-bit word containing the constructor -- tag of the object and a format field in the least-significant byte. -- -- OBJECT -- ~~~~~~ -- byte 3 2 1 0 (in MSB order) -- TAG2 TAG1 TAG0 FORMAT ... -- -- -- FORMAT field -- ~~~~~~~~~~~~ -- bit 7 6 5 4 3 2 1 0 -- -- arg --- -- obj --- -- X X X X X X 0 0 -- Forward / Broken-Heart -- X X X X a X X X -- Anchor flag -- 0 0 0 1 a 0 0 1 -- Thunk -- 0 0 1 0 a 0 0 1 -- DataBoxed -- 0 0 1 1 a 0 0 1 -- DataRaw -- 0 1 0 0 a 0 0 1 -- DataMixed -- 0 1 0 1 a 0 0 1 -- SuspIndir -- -- size -- a 0 1 1 -- DataRawSmall -- -- Data GC Forwarding / Broken-Heart pointers. -- During garbage collection, after the GC copies an object to the -- "to-space" its header in the "from-space" is overwritten with a pointer -- to where the "to-space" version of the object is. -- -- We can identify these pointers because their lowest 2 bits are always 00. -- This is because objects in the heap are always 4-byte aligned. -- -- For all other values of the format field, we ensure the lowest two bits -- are not 00. -- -- Data Anchor flag -- If bit 3 in the format field is set then the GC is not permitted to move -- the object. This is useful when the object has been allocated by malloc -- and exists outside the DDC runtime's garbage collected heap. -- -- Data Data{Boxed, Mixed, Raw, RawSmall} -- There are four data object formats: -- DataBoxed: A boxed object containing pointers to more heap objects. -- DataMixed: Some heap pointers, and some raw data. -- DataRaw: Contains raw data and no pointers. -- DataRawSmall: Contains raw data where the size is small enough to -- encode directly in the format field. -- -- The -obj- (object mode) portion of the format field can be used to -- determine if the object is a forwarding pointer, has a fixed value for -- its format field, or is a DataRS object. -- -- Note: 64-bit floats. -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -- The various object formats always contain an even number of 32-bit words -- in the header portion, before the payload. This ensures that the payloads -- of all heap objects are 8-byte aligned. We do this to support architectures -- that cannot load misaligned double precision floats (Float64). Architectures -- that can load them typically suffer a penalty, so it is good to align heap -- objects anyway. -- module Object export value getTag : [r : Region]. Ptr# r Obj -> Tag# allocBoxed : [r : Region]. Tag# -> Nat# -> Ptr# r Obj getFieldOfBoxed : [r : Region]. [a : Data]. Ptr# r Obj -> Nat# -> a setFieldOfBoxed : [r : Region]. [a : Data]. Ptr# r Obj -> Nat# -> a -> Void# allocMixed : [r : Region]. Tag# -> Nat# -> Nat# -> Ptr# r Obj fieldOfMixed : [r : Region]. Ptr# r Obj -> Nat# -> Ptr# r Obj payloadOfMixed : [r : Region]. Ptr# r Obj -> Ptr# r Word8# allocRaw : [r : Region]. Tag# -> Nat# -> Ptr# r Obj payloadOfRaw : [r : Region]. Ptr# r Obj -> Ptr# r Word8# allocRawSmall : [r : Region]. Tag# -> Nat# -> Ptr# r Obj payloadOfRawSmall : [r : Region]. Ptr# r Obj -> Ptr# r Word8# with letrec -- | Get the constructor tag of an object. getTag [r : Region] (obj : Ptr# r Obj) : Tag# = do ptr = castPtr# obj header = peek# ptr 0# tag32 = shr# header 8w32# promote# tag32 -- Boxed ---------------------------------------------------------------------- -- | Allocate a Boxed Data Object. -- The payload contains pointers to other heap objects. -- -- typedef struct -- { uint32_t tagFormat; // Constructor tag and format field. -- uint32_t arity; // Arity of the data constructor. -- // (The number of pointers in the payload) -- ObjData payload[]; -- } DataBoxed; -- allocBoxed [r : Region] (tag : Tag#) (arity : Nat#) : Ptr# r Obj = do -- multiply arity by 4 bytes-per-pointer to get size of payload. bytesPayload = shl# arity (size2# [Ptr# r Obj]) bytesObj = add# 8# bytesPayload case check# bytesObj of True# -> allocBoxed_ok tag arity bytesObj False# -> fail# allocBoxed_ok [r : Region] (tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj tag32 = promote# tag format = 0b00100001w32# header = bor# (shl# tag32 8w32#) format write# [Word32#] addr 0# header arity32 = promote# arity write# [Word32#] addr 4# arity32 makePtr# addr ---- | Get one of the pointers from a boxed data object. getFieldOfBoxed [r1 : Region] [a : Data] (obj : Ptr# r1 Obj) (index : Nat#) : a = read# [a] (takePtr# obj) (add# 8# (shl# index 2#)) -- | Set one of the pointers from a boxed data object. setFieldOfBoxed [r1 : Region] [a : Data] (obj : Ptr# r1 Obj) (index : Nat#) (val : a) : Void# = write# (takePtr# obj) (add# 8# (shl# index 2#)) val -- Mixed ---------------------------------------------------------------------- -- | Allocate a Mixed Data Object. -- The payload contains some pointers followed by raw data. -- -- typedef struct -- { uint32_t tagFormat; -- uint32_t padding; // Padding to ensure payload is 8 byte aligned. -- uint32_t size; // Size of the whole object, in bytes. -- uint32_t ptrCount; // Number of pointers at the start of the payload. -- ObjData payload[]; // Contains ptrCount pointers, then raw data. -- } DataMixed; -- allocMixed [r : Region] (tag : Tag#) (arity : Nat#) (bytesRaw : Nat#) : Ptr# r Obj = do bytesPtrs = shl# arity 2# bytesObj = add# 16# (add# bytesPtrs bytesRaw) case check# bytesObj of True# -> allocMixed_ok tag arity bytesRaw bytesObj False# -> fail# allocMixed_ok [r : Region] (tag : Tag#) (arity : Nat#) (bytesRaw : Nat#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj tag32 = promote# tag format = 0b01000001w32# header = bor# (shl# tag32 8w32#) format write# [Word32#] addr 0# header write# [Word32#] addr 4# 0w32# bytesObj32 = promote# bytesObj write# [Word32#] addr 8# bytesObj32 arity32 = promote# arity write# [Word32#] addr 12# arity32 makePtr# [r] [Obj] addr -- | Get one of the pointers from a mixed data object. fieldOfMixed [r : Region] (obj : Ptr# r Obj) (index : Nat#) : Ptr# r Obj = do offset = add# 16# (shl# index 2#) plusPtr# obj offset -- | Get the address of the raw data payload from a mixed object. payloadOfMixed [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8# = plusPtr# (castPtr# obj) 16# -- Raw ------------------------------------------------------------------------ -- | A Raw Data Object. -- A raw data object does not contain heap pointers that need to be traced -- by the garbage collector. -- -- typedef struct -- { uint32_t tagFormat; // Constructor tag and format field. -- uint32_t size; // Size of the whole object, in bytes. -- uint8_t payload[]; // Raw data that does not contain heap pointers. -- } DataRaw; -- allocRaw [r : Region] (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj = do bytesObj = add# 8# bytesPayload case check# bytesObj of True# -> allocRaw_ok [r] tag bytesPayload bytesObj False# -> fail# allocRaw_ok [r : Region] (tag : Tag#) (bytesPayload : Nat#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj tag32 = promote# tag format = 0b00110001w32# header = bor# (shl# tag32 8w32#) format write# [Word32#] addr 0# header bytesObj32 = promote# bytesObj write# [Word32#] addr 4# bytesObj32 makePtr# addr -- | Get the payload data from a raw object. payloadOfRaw [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8# = plusPtr# (castPtr# obj) 8# -- RawSmall ------------------------------------------------------------------- -- | A Small Raw object. -- The object size is encoded as part of format field. -- This saves us from needing to include a separate arity field. -- -- typedef struct -- { uint32_t tagFormat; // Constructor tag and format field. -- uint8_t payload[]; // Raw data that does not contain heap pointers. -- } DataRawSmall; -- allocRawSmall [r : Region] (tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj = do bytesObj = add# 4# bytesPayload case check# bytesObj of True# -> allocRawSmall_ok tag bytesPayload bytesObj False# -> fail# allocRawSmall_ok [r : Region] (tag : Tag#) (bytesPayload : Nat#) (bytesObj : Nat#) : Ptr# r Obj = do addr = alloc# bytesObj tag32 = promote# tag bytesPayload32 = truncate# bytesPayload wordsPayload32 = shr# bytesPayload32 2w32# format = 0b0011w32# header = bor# (shl# tag32 8w32#) (bor# (shl# wordsPayload32 4w32#) format) write# [Word32#] addr 0# header makePtr# addr -- | Get the payload data from a raw small object. payloadOfRawSmall [r : Region] (obj : Ptr# r Obj) : Ptr# r Word8# = plusPtr# (castPtr# obj) 4#