ddc-code-0.3.1.1: salt/runtime64/Object.dcs
-- | Primitives for constructing and destructing 64-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 64-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
--
-- * 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.
--
-- * 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{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
exports
getTag :: [r : %]. Ptr# r Obj -> Tag#
allocBoxed :: [r : %]. Tag# -> Nat# -> Ptr# r Obj
getFieldOfBoxed :: [r : %]. [a : *]. Ptr# r Obj -> Nat# -> a
setFieldOfBoxed :: [r : %]. [a : *]. Ptr# r Obj -> Nat# -> a -> Void#
allocMixed :: [r : %]. Tag# -> Nat# -> Nat# -> Ptr# r Obj
fieldOfMixed :: [r : %]. Ptr# r Obj -> Nat# -> Ptr# r Obj
payloadOfMixed :: [r : %]. Ptr# r Obj -> Ptr# r Word8#
allocRaw :: [r : %]. Tag# -> Nat# -> Ptr# r Obj
payloadOfRaw :: [r : %]. Ptr# r Obj -> Ptr# r Word8#
allocRawSmall :: [r : %]. Tag# -> Nat# -> Ptr# r Obj
payloadOfRawSmall :: [r : %]. Ptr# r Obj -> Ptr# r Word8#
with letrec
-- | Get the constructor tag of an object.
getTag [r : %] (obj : Ptr# r Obj) : Tag#
= do
ptr = castPtr# [r] [Word32#] [Obj] obj
header = peek# [r] [Word32#] ptr 0#
tag32 = shr# [Word32#] header 8w32#
promote# [Tag#] [Word32#] tag32
-- Boxed ----------------------------------------------------------------------
-- | Allocate a Boxed Data Object.
-- The payload contains pointers to other heap objects.
--
-- The arity must be no greater than 2^32, else undefined.
-- This object type is typically used for algebraic data, which won't have
-- more than 2^32 fields.
--
-- 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)
-- Obj* payload[];
-- } DataBoxed;
--
allocBoxed
[r : %]
(tag : Tag#) (arity : Nat#) : Ptr# r Obj
= do
-- Multiple arity by 8 bytes-per-pointer to get size of payload.
bytesPayload = shl# [Nat#] arity (size2# [Addr#])
bytesObj = add# [Nat#] (size# [Word32#])
(add# [Nat#] (size# [Word32#])
bytesPayload)
case check# bytesObj of
True# -> allocBoxed_ok [r] tag arity bytesObj
False# -> fail# [Ptr# r Obj]
allocBoxed_ok
[r : %]
(tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj
= do
addr = alloc# bytesObj
tag32 = promote# [Word32#] [Tag#] tag
format = 0b00100001w32#
header = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format
write# [Word32#] addr 0# header
-- Truncate arity to 32-bits.
arity32 = truncate# [Word32#] [Nat#] arity
write# [Word32#] addr 4# arity32
makePtr# [r] [Obj] addr
---- | Get one of the pointers from a boxed data object.
getFieldOfBoxed
[r1 : %] [a : *]
(obj : Ptr# r1 Obj) (index : Nat#)
: a
= read# [a] (takePtr# [r1] [Obj] obj)
(add# [Nat#] 8#
(shl# [Nat#] index (size2# [Addr#])))
-- | Set one of the pointers from a boxed data object.
setFieldOfBoxed
[r1 : %] [a : *]
(obj : Ptr# r1 Obj) (index : Nat#)
(val : a)
: Void#
= write# [a] (takePtr# [r1] [Obj] obj)
(add# [Nat#] 8#
(shl# [Nat#] index (size2# [Addr#])))
val
-- Mixed ----------------------------------------------------------------------
-- | Allocate a Mixed Data Object.
-- The payload contains some pointers followed by raw data.
--
-- The arity (ptrCount) must be no greater than 2^32, else undefined.
-- The payload can have length up to 2^64.
--
-- typedef struct
-- { uint32_t tagFormat;
-- uint32_t ptrCount; // Number of pointers at the start of the payload.
-- uint64_t size; // Size of the whole object, in bytes.
-- Obj* payload[]; // Contains ptrCount pointers, then raw data.
-- } DataMixed;
--
allocMixed
[r : %]
(tag : Tag#) (arity : Nat#) (bytesRaw : Nat#) : Ptr# r Obj
= do
bytesPtrs = shl# [Nat#] arity 3#
bytesObj = add# [Nat#] (size# [Word32#])
(add# [Nat#] (size# [Word32#])
(add# [Nat#] (size# [Word64#])
(add# [Nat#] bytesPtrs bytesRaw)))
case check# bytesObj of
True# -> allocMixed_ok [r] tag arity bytesObj
False# -> fail# [Ptr# r Obj]
allocMixed_ok
[r : %]
(tag : Tag#) (arity : Nat#) (bytesObj : Nat#) : Ptr# r Obj
= do
addr = alloc# bytesObj
tag32 = promote# [Word32#] [Tag#] tag
format = 0b01000001w32#
header = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format
write# [Word32#] addr 0# header
arity32 = truncate# [Word32#] [Nat#] arity
write# [Word32#] addr 4# arity32
bytesObj32 = promote# [Word64#] [Nat#] bytesObj
write# [Word64#] addr 8# bytesObj32
makePtr# [r] [Obj] addr
-- | Get one of the pointers from a mixed data object.
fieldOfMixed [r : %] (obj : Ptr# r Obj) (index : Nat#) : Ptr# r Obj
= do
offset = add# [Nat#] 16#
(shl# [Nat#] index (size2# [Addr#]))
plusPtr# [r] [Obj] obj offset
-- | Get the address of the raw data payload from a mixed object.
payloadOfMixed [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#
= plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] 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.
--
-- The payload size must be no greater than (2^32 - 8), else undefined.
--
-- 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 : %]
(tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj
= do
bytesObj = add# [Nat#] (size# [Word32#])
(add# [Nat#] (size# [Word32#])
bytesPayload)
case check# bytesObj of
True# -> allocRaw_ok [r] tag bytesObj
False# -> fail# [Ptr# r Obj]
allocRaw_ok
[r : %]
(tag : Tag#) (bytesObj : Nat#) : Ptr# r Obj
= do
addr = alloc# bytesObj
tag32 = promote# [Word32#] [Tag#] tag
format = 0b00110001w32#
header = bor# [Word32#] (shl# [Word32#] tag32 8w32#) format
write# [Word32#] addr 0# header
bytesObj32 = truncate# [Word32#] [Nat#] bytesObj
write# [Word32#] addr 4# bytesObj32
makePtr# [r] [Obj] addr
-- | Get the payload data from a raw object.
payloadOfRaw [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#
= plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] 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.
--
-- The payload size must be no greater than 16, else undefined.
--
-- typedef struct
-- { uint32_t tagFormat; // Constructor tag and format field.
-- uint8_t payload[]; // Raw data that does not contain heap pointers.
-- } DataRawSmall;
--
allocRawSmall
[r : %]
(tag : Tag#) (bytesPayload : Nat#) : Ptr# r Obj
= do
bytesObj = add# [Nat#] 4# bytesPayload
case check# bytesObj of
True# -> allocRawSmall_ok [r] tag bytesPayload bytesObj
False# -> fail# [Ptr# r Obj]
allocRawSmall_ok
[r : %]
(tag : Tag#) (bytesPayload : Nat#) (bytesObj : Nat#) : Ptr# r Obj
= do
addr = alloc# bytesObj
tag32 = promote# [Word32#] [Tag#] tag
bytesPayload32 = truncate# [Word32#] [Nat#] bytesPayload
wordsPayload32 = shr# [Word32#] bytesPayload32 2w32#
format = 0b0011w32#
header = bor# [Word32#] (shl# [Word32#] tag32 8w32#)
(bor# [Word32#] (shl# [Word32#] wordsPayload32 4w32#)
format)
write# [Word32#] addr 0# header
makePtr# [r] [Obj] addr
-- | Get the payload data from a raw small object.
payloadOfRawSmall [r : %] (obj : Ptr# r Obj) : Ptr# r Word8#
= plusPtr# [r] [Word8#] (castPtr# [r] [Word8#] [Obj] obj) 4#