memory

cfamily.Pointer

data Pointer

A pointer: null, into a block (path, index, whether to the object at the path itself), to a byte of an object (a character pointer made from a pointer to an object of another type, C11 6.3.2.3p7: the block, the path to the object whose bytes it ranges over, the byte, the object’s shape and bits), into a string literal, to a file stream (0 is stdin), or made from an integer (numbered, C11 6.3.2.3p5: GCC keeps the integer as the address; nothing the model has is there).

cfamily.Elements.half

def Elements.half (count : Nat) : Nat

The number of elements on the left of an array of count elements: half of them, rounded down.

cfamily.Elements.size

def Elements.size (es : Elements) : Nat

The number of elements in es.

cfamily.Elements.copies

def Elements.copies (count : Nat) (o : Object) : Elements

count copies of the object o, made in one step whatever count is (they split only where written).

cfamily.Elements.get

def Elements.get (es : Elements) (k : Nat) : Option Object

The k-th element of es (none past the end): down the halves, O(log n).

cfamily.Elements.writeCopies

def Elements.writeCopies (fuel : Nat) (count : Nat) (o : Object) (k : Nat) (f : Object -> Object) : Elements

count copies of o with the k-th made f of it: the half with k split further, the other half left as copies. fuel only bounds the recursion for the checker (the depth is log2 count; count itself is enough).

cfamily.Elements.update

def Elements.update (es : Elements) (k : Nat) (f : Object -> Object) : Elements

es with the k-th element made f of it (unchanged past the end): only the path to it is copied, O(log n).

cfamily.Elements.map

def Elements.map (f : Object -> Object) (es : Elements) : Elements

Every element of es made f of it (copies stay copies: f is applied once to their object).

cfamily.Elements.copiesOnto

def Elements.copiesOnto (k : Nat) (o : Object) (onto : List Object) : List Object

k copies of the object o in front of onto, in a loop.

cfamily.Elements.splitList

def Elements.splitList (n : Nat) (xs : List Object) (taken : List Object) : List Object * List Object

The first n objects of xs (in order) and the rest, in a loop: taken holds the ones taken so far, last first.

cfamily.Elements.ofListWithin

def Elements.ofListWithin (fuel : Nat) (count : Nat) (xs : List Object) : Elements

The first count objects of xs as elements, halved the same way writing does. fuel bounds the recursion for the checker (the depth is log2 count).

cfamily.Elements.ofList

def Elements.ofList (xs : List Object) : Elements

The objects of xs as elements.

cfamily.Elements.listOnto

def Elements.listOnto (fuel : Nat) (stack : List Elements) (done : List Object) : List Object

The objects of the pieces on stack (the top first in the result, each piece’s in order) put before done, in a loop that works from the end: a piece’s right half is taken before its left. fuel bounds the steps (one per piece).

cfamily.Elements.toList

def Elements.toList (es : Elements) : List Object

The elements of es as a list, in order (for what needs every element: the bytes, printing).

cfamily.Elements.writeFrom

def Elements.writeFrom (es : Elements) (k : Nat) (xs : List Object) : Elements

es with the objects of xs written one by one from the k-th on, in a loop (an initializer’s elements, the ones realloc moves): O(m log n) for m of them, the rest of es untouched.

cfamily.Elements.sliceOnto

def Elements.sliceOnto (es : Elements) (start : Nat) (count : Nat) (done : List Object) : List Object

The elements of es from the start-th on, at most count of them, in a loop (the ones a pointer ranges over that are shown): each read O(log n), past the end none. done holds the ones read so far, last first.

cfamily.Elements.slice

def Elements.slice (es : Elements) (start : Nat) (count : Nat) : List Object

At most count elements of es from the start-th on.

cfamily.Object.elementList

def Object.elementList (o : Object) : List Object

The elements of the object o as a list, in order (none when o is not an array): what two arrays are compared by, since the same elements may be kept in trees of different shapes (copies not yet written, or split by writes).

cfamily.Block

record Block (L : Constructs)

A block: the type of its object, the object, and how it came to exist.

cfamily.Memory

def Memory (L : Constructs) : Type

The memory: blocks by number, none once a block’s lifetime has ended.

cfamily.Memory.empty

def Memory.empty {L : Constructs} : Memory L

No blocks.

cfamily.Memory.block

def Memory.block {L : Constructs} (m : Memory L) (b : Nat) : Option (Block L)

The block with the number, if it is alive.

cfamily.Memory.allocate

def Memory.allocate {L : Constructs} (m : Memory L) (c : Block L) : Memory L

A new block at the end; its number is the memory’s size before.

cfamily.Memory.next

def Memory.next {L : Constructs} (m : Memory L) : Nat

The number the next block will have.

cfamily.Memory.write

def Memory.write {L : Constructs} (m : Memory L) (b : Nat) (c : Block L) : Memory L

The block replaced.

cfamily.Memory.release

def Memory.release {L : Constructs} (m : Memory L) (b : Nat) : Memory L

The block’s lifetime ended.

cfamily.Pointer.samePath

def Pointer.samePath (xs : List Nat) (ys : List Nat) : Bool

Whether two paths are the same.

cfamily.ObjectBit.ofNumber

def ObjectBit.ofNumber (count : Nat) (n : Nat) : List ObjectBit

The bits of a number, the low bit first.

cfamily.ObjectBit.number

def ObjectBit.number (bits : List ObjectBit) : Option Nat

The number bits stand for, low bit first, if every bit is 0 or 1.

cfamily.ObjectBit.unknownOnto

def ObjectBit.unknownOnto (count : Nat) (onto : List ObjectBit) : List ObjectBit

Indeterminate bits in front of others, in a loop (an object’s bits may be millions: a recursion that deep runs out of the browser’s stack).

cfamily.ObjectBit.unknown

def ObjectBit.unknown (count : Nat) : List ObjectBit

Indeterminate bits.

cfamily.ObjectBit.fitted

def ObjectBit.fitted (count : Nat) (bits : List ObjectBit) : List ObjectBit

Bits padded with indeterminate ones, or cut, to a count.

cfamily.ObjectBit.splice

def ObjectBit.splice (offset : Nat) (others : List ObjectBit) (bits : List ObjectBit) : List ObjectBit

Bits with the ones from an offset on replaced by others (as many as there are).

cfamily.ObjectBit.pointerFrom

def ObjectBit.pointerFrom (v : Value) (k : Nat) (count : Nat) : List ObjectBit

The bits of a pointer from the k-th on.

cfamily.Pointer.identical

def Pointer.identical (p : Pointer) (q : Pointer) : Bool

Whether two pointers are the same pointer, part by part (what its bits keep).

cfamily.Value.identicalPointer

def Value.identicalPointer (v : Value) (w : Value) : Bool

Whether two values are the same pointer or the same function.

cfamily.ObjectBit.pointerRest

def ObjectBit.pointerRest (v : Value) (k : Nat) (bits : List ObjectBit) : Bool

Whether bits are the k-th bit of a pointer on, in order.

cfamily.ObjectBit.pointer

def ObjectBit.pointer (bits : List ObjectBit) : Option Value

The pointer bits stand for: null if every bit is 0, a pointer if they are all of its bits in order.

cfamily.Pointer.isNull

def Pointer.isNull (p : Pointer) : Bool

Whether a pointer is null.

cfamily.Shape.ofValue

def Shape.ofValue (s : Shape) (count : Nat) (v : Value) : List ObjectBit

The count bits of a scalar value v of the shape s: an integer’s bits by its width, a floating value’s encoding (the padding after it indeterminate: x87’s last 48 bits), a pointer’s own bits (null is all 0); a value not of the shape is indeterminate.

cfamily.Shape.valueOf

def Shape.valueOf (s : Shape) (bits : List ObjectBit) : Option Value

The value of the scalar shape s the bits stand for, if they stand for one: an integer whose bits past its width are 0 (a bool is 0 or 1), a floating value (its padding bits not read), a pointer.

cfamily.Shape.elementsBelow

def Shape.elementsBelow (s : Shape) (width : Nat) (k : Nat) (onto : List Placed) : List Placed

The places of an array’s first k elements in front of others, in a loop (from the last one down).

cfamily.Shape.children

def Shape.children (s : Shape) : List Placed

The places of a shape’s children (an array’s elements, the members); a scalar has none.

cfamily.Shape.child

def Shape.child (s : Shape) (k : Nat) : Option Placed

The place of a shape’s k-th child, if it has one (an array’s element directly: listing a large array’s places for each access was linear).

cfamily.Placed.locate

def Placed.locate (p : Placed) (path : List Nat) : Option Placed

Where the subobject at a path below a place is.

cfamily.ObjectBit.repeatedOnto

def ObjectBit.repeatedOnto (bits : List ObjectBit) (times : Nat) (onto : List ObjectBit) : List ObjectBit

times copies of bits one after another in front of onto, in a loop (the bits of a run of equal elements).

cfamily.Placed.encode

def Placed.encode (p : Placed) (o : Object) : List ObjectBit

The bits of an object at a place (its own bits only).

cfamily.Placed.decode

def Placed.decode (p : Placed) (bits : List ObjectBit) : Object

The object at a place in bits.

cfamily.Placed.count

def Placed.count (p : Placed) : Nat

How many bits a place takes.

cfamily.Shape.keptIn

def Shape.keptIn (s : Shape) (bits : List ObjectBit) : Object

The object of a shape bits stand for, keeping a scalar’s bits that stand for no value when some are known (written through a character pointer, a pointer’s bits copied one byte at a time).

cfamily.Placed.holds

def Placed.holds (b : Nat) (e : Nat) (p : Placed) : Bool

Whether a place holds the bits from b up to (not including) e.

cfamily.Object.unionWith

def Object.unionWith (p : Placed) (active : Nat) (xs : List Object) : Object

A union kept as bits with a member active: its members’ places, and the member’s bits (the rest indeterminate).

cfamily.Object.children

def Object.children (o : Object) : Option (List Object)

The children of the object o (its elements or members), if it has any.

cfamily.Object.child

def Object.child (o : Object) (k : Nat) : Option Object

The k-th child of an object (of a union kept as bits, the member its bits stand for).

cfamily.Object.at

def Object.at (o : Object) (path : List Nat) : Option Object

The object at a path down the tree.

cfamily.Object.inWrittenUnion

def Object.inWrittenUnion (o : Object) (path : List Nat) : Bool

Whether the path goes into a union kept as bits that has had a member written: a scalar there whose bits stand for no value has an unspecified one (the bytes of another member, C11 6.2.6.1p7; a pointer’s bits read as an integer), not an indeterminate one.

cfamily.Object.readsInactive

def Object.readsInactive (o : Object) (path : List Nat) : Bool

Whether the path reads a member of a union kept as bits other than the one last written (the reinterpretation C defines and C++ leaves undefined).

cfamily.Memory.objectIn

def Memory.objectIn {L : Constructs} (m : Memory L) (b : Nat) (path : List Nat) : Option Object

The object at a path in a block, if the block is alive and the path is in its object.

cfamily.Object.eraseAll

def Object.eraseAll (xs : List Object) : List Object

Every object erased.

cfamily.Object.replaceAt

def Object.replaceAt (xs : List Object) (k : Nat) (path : List Nat) (v : Object) : List Object

The children with the k-th’s object at the path replaced.

cfamily.Object.span

def Object.span (o : Object) (whole : Bool) : Nat

The length a pointer may range over in an object: an array’s, else 1.

cfamily.Object.ofValue

def Object.ofValue (v : Value) : Object

The object a value is stored as: a whole object as itself, a scalar value in a scalar.

cfamily.Address

data Address

An address: a block and the path to an object in it, a byte of the object at a path (its shape and bits), or a byte of a string literal.

cfamily.Object.ofByte

def Object.ofByte (bits : List ObjectBit) : Object

A byte as an object of a character type: its number when its bits are all known, else its bits as they are (a pointer’s, indeterminate ones).

cfamily.Object.byteOf

def Object.byteOf (o : Object) : List ObjectBit

The bits of a byte an object of a character type holds (its value’s low eight bits).

cfamily.Placed.shape

def Placed.shape (p : Placed) : Shape

The shape at a place.

cfamily.Placed.bytes

def Placed.bytes (p : Placed) : Nat

How many bytes an object at a place takes.

cfamily.Placed.align

def Placed.align (p : Platform) (x : Placed) : Nat

The alignment of the object at a place.

cfamily.Pointer.literalLength

def Pointer.literalLength (text : String) : Nat

The length of a string literal’s array, with the null.

cfamily.Pointer.below

def Pointer.below (i : Int) (n : Nat) : Bool

Whether i is in [0, n).

cfamily.Pointer.upTo

def Pointer.upTo (i : Int) (n : Nat) : Bool

Whether i is in [0, n].

cfamily.Pointer.fullPath

def Pointer.fullPath (path : List Nat) (i : Int) (whole : Bool) : List Nat

The full path of the object a pointer into a block designates.

cfamily.Followed

data Followed

Following a pointer: the address it designates, or why it designates none.

cfamily.Pointer.dereference

def Pointer.dereference {L : Constructs} (m : Memory L) (p : Pointer) : Followed

Following a pointer: null (C11 6.5.3.2p4), a file stream (an incomplete type), a block whose lifetime has ended (6.2.4p2), a path that is not in the object, one past the end (6.5.6p8).

cfamily.Pointer.splitLast

def Pointer.splitLast (xs : List Nat) : Option (List Nat * Nat)

The last of a list and the ones before it.

cfamily.Pointer.ofAddress

def Pointer.ofAddress {L : Constructs} (m : Memory L) (a : Address) : Pointer

The pointer &lvalue gives for an address: an element of the array above it, else the object itself.

cfamily.Pointer.first

def Pointer.first (a : Address) : Pointer

The pointer to the first element of the array at an address (an array’s value decays to it).

cfamily.Moved

data Moved

Moving a pointer: where it moved to, or why it cannot.

cfamily.Pointer.add

def Pointer.add {L : Constructs} (m : Memory L) (p : Pointer) (k : Int) : Moved

p + k: within the same array or one past its end (C11 6.5.6p8); null and streams have no arithmetic, and a block whose lifetime has ended has no array left.

cfamily.Pointer.sameArray

def Pointer.sameArray (p : Pointer) (q : Pointer) : Bool

Whether two pointers point into the same array (or object), so that their difference and order are defined.

cfamily.Pointer.index

def Pointer.index (p : Pointer) : Int

The index of a pointer within its array.

cfamily.Pointer.same

def Pointer.same (p : Pointer) (q : Pointer) : Bool

Whether two pointers are equal: both null, or the same place (C11 6.5.9p6).

cfamily.Pointer.isLive

def Pointer.isLive {L : Constructs} (m : Memory L) (p : Pointer) : Bool

Whether a pointer’s block is alive (a pointer to a dead block is indeterminate, C11 6.2.4p2).

cfamily.Memory.objectAt

def Memory.objectAt {L : Constructs} (m : Memory L) (a : Address) : Option Object

The object at an address in the memory.

cfamily.Memory.store

def Memory.store {L : Constructs} (m : Memory L) (a : Address) (o : Object) : Option (Memory L)

The memory with the object at an address replaced (a literal cannot be written, C11 6.4.5p7).