Module Assembler.Types

Types

This module contains OCaml types for PISA and PASM instructinos and programs. The Rocq types in the project's theories are mapped to these using an extraction script.

type reg =
  1. | R0
  2. | R1
  3. | R2
  4. | R3
  5. | R4
  6. | R5
  7. | R6
  8. | R7
  9. | R8
  10. | R9
  11. | R10
  12. | R11
  13. | R12
  14. | R13
  15. | R14
  16. | R15
  17. | R16
  18. | R17
  19. | R18
  20. | R19
  21. | R20
  22. | R21
  23. | R22
  24. | R23
  25. | R24
  26. | R25
  27. | R26
  28. | R27
  29. | R28
  30. | R29
  31. | R30
  32. | R31

Registers.

type 'l asm_inst =
  1. | Li of reg * int
    (*

    Load immediate.

    *)
  2. | Ld of reg * reg * int
    (*

    Load.

    *)
  3. | St of reg * reg * int
    (*

    Store.

    *)
  4. | Add of reg * reg * reg
    (*

    Add two registers.

    *)
  5. | Addi of reg * reg * int
    (*

    Add register and immediate.

    *)
  6. | Sub of reg * reg * reg
    (*

    Subtract two registers.

    *)
  7. | And of reg * reg * reg
    (*

    Bitwise and between two registers.

    *)
  8. | Not of reg * reg
    (*

    Bitwise negation of a register.

    *)
  9. | Sl of reg * reg * int
    (*

    Logical Shift Left.

    *)
  10. | Sr of reg * reg * int
    (*

    Logical Shift Right.

    *)
  11. | Beq of reg * reg * 'l
    (*

    Branch if equal-to.

    *)
  12. | Blt of reg * reg * 'l
    (*

    Branch if less-than.

    *)
  13. | Jalr of reg * reg * int
    (*

    Jump and link register.

    *)
  14. | Apc of reg * int
    (*

    Add to PC and store in a register.

    *)
  15. | J of 'l
    (*

    (Unconditional) jump.

    *)
  16. | Label of 'l
    (*

    Define a label.

    *)
  17. | Spin
    (*

    Spin endlessly.

    *)

PASM instructions with labels of type 'l.

type 'l asm_prog = 'l asm_inst list

PASM programs.

type isa_inst =
  1. | I_li of reg * int
  2. | I_ld of reg * reg * int
  3. | I_st of reg * reg * int
  4. | I_add of reg * reg * reg
  5. | I_addi of reg * reg * int
  6. | I_sub of reg * reg * reg
  7. | I_and of reg * reg * reg
  8. | I_not of reg * reg
  9. | I_sl of reg * reg * int
  10. | I_sr of reg * reg * int
  11. | I_beq of reg * reg * int
  12. | I_blt of reg * reg * int
  13. | I_jalr of reg * reg * int
  14. | I_apc of reg * int
  15. | I_j of int

PISA instructions, without labels.

type isa_prog = isa_inst list

PISA programs.

type machine_inst = bool list

Machine instructions.

type machine_prog = machine_inst list

Machine programs.

module Helper : sig ... end

Helper functions to write AST programs.