Access Kinds

Access kinds define the permitted operations on pointers and memory regions. They are enforced at compile time and affect code generation.

Overview

Every pointer in Clef carries an access kind that specifies what operations are legal:

type Ptr<'T, 'Region, 'Access>
//                     ^^^^^^^ Access kind

Access kinds prevent:

  • Writing to read-only memory (flash, input registers)
  • Reading from write-only memory (output registers)
  • Accidental modification of constants

Access Kind Types

KindReadWriteCMSIS EquivalentUse Case
ReadOnlyYesNo__IInput registers, flash, constants
WriteOnlyNoYes__OOutput registers, write-only buffers
ReadWriteYesYes__IOGeneral mutable access

ReadOnly

Read-only pointers permit load operations only.

let flashData : Ptr<byte, Flash, ReadOnly> = ...
let value = Ptr.read flashData      // OK
Ptr.write flashData 0uy             // ERROR: Cannot write to ReadOnly

Code Generation: No store instructions generated for ReadOnly pointers.

WriteOnly

Write-only pointers permit store operations only.

let outputReg : Ptr<uint32, Peripheral, WriteOnly> = ...
Ptr.write outputReg 0x1234u         // OK
let value = Ptr.read outputReg      // ERROR: Cannot read from WriteOnly

Code Generation: No load instructions generated for WriteOnly pointers.

ReadWrite

Read-write pointers permit both load and store operations.

let gpioReg : Ptr<uint32, Peripheral, ReadWrite> = ...
let current = Ptr.read gpioReg      // OK
Ptr.write gpioReg (current ||| 0x1u) // OK

Compile-Time Enforcement

Access kind violations are type errors:

// ERROR: Cannot write to ReadOnly pointer
let writeFlash (p: Ptr<byte, Flash, ReadOnly>) =
    Ptr.write p 0uy  // Compile error

// ERROR: Cannot read from WriteOnly pointer
let readOutput (p: Ptr<uint32, Peripheral, WriteOnly>) =
    Ptr.read p  // Compile error

Access Kind Coercion

More restrictive access kinds can be coerced to less restrictive:

FromToAllowed
ReadWriteReadOnlyYes (drop write)
ReadWriteWriteOnlyYes (drop read)
ReadOnlyReadWriteNo
WriteOnlyReadWriteNo
ReadOnlyWriteOnlyNo
WriteOnlyReadOnlyNo
let rw : Ptr<int, Stack, ReadWrite> = ...
let ro : Ptr<int, Stack, ReadOnly> = Ptr.asReadOnly rw  // OK
let wo : Ptr<int, Stack, WriteOnly> = Ptr.asWriteOnly rw // OK

Hardware Register Patterns

Access kinds enable type-safe hardware register access:

[<PeripheralDescriptor("GPIO", 0x48000000UL)>]
type GPIO_TypeDef = {
    [<Register("MODER", 0x00u, "rw")>]
    MODER: Ptr<uint32, Peripheral, ReadWrite>
    
    [<Register("IDR", 0x10u, "r")>]
    IDR: Ptr<uint32, Peripheral, ReadOnly>
    
    [<Register("ODR", 0x14u, "rw")>]
    ODR: Ptr<uint32, Peripheral, ReadWrite>
    
    [<Register("BSRR", 0x18u, "w")>]
    BSRR: Ptr<uint32, Peripheral, WriteOnly>
}

Grammar

access-kind :=
    ReadOnly
    WriteOnly
    ReadWrite

ptr-type := Ptr < type , region-type , access-kind >

Diagnostics

CodeMessage
FS8020Cannot write to ReadOnly pointer
FS8021Cannot read from WriteOnly pointer
FS8022Access kind mismatch in assignment

See Also