(* Library to generate MIPS code
by 2008 Jean-Christophe Filliâtre (CNRS)
- first version
2013 Kim Nguyen (Université Paris Sud)
- subtypes text and data
- ghost types for oreg and oi
- more ops and directives
- stack management
- ocamldoc xs
2024 Léon Gondelman (AAU)
- just translated to English description
*)
(** {0 Library for writing MIPS programs } *)
(** Module {!Mips} allows to write MIPS code inside OCaml code without
need for a preprocessor. A complete example is given in
{{:#1_Exemple} below in the section example}. *)
type 'a asm
(** abstract type to represent assembly code. The parameter
['a] is used as ghost type. *)
type text = [ `text ] asm
(** type representing assembly code in the section following the text directive. *)
type data = [ `data ] asm
(** type representing assembly code in the section following the data directive. *)
type program = {
text : text;
data : data;
}
(** a program consists of a text zone and data zone *)
val print_program : Format.formatter -> program -> unit
(** [print_program fmt p] pretty-printsthe code of the program [p] in the formatter
[fmt] *)
val print_in_file: file:string -> program -> unit
type register
(** Abstract type for registers *)
val v0 : register
val v1 : register
val a0 : register
val a1 : register
val a2 : register
val a3 : register
val t0 : register
val t1 : register
val t2 : register
val t3 : register
val s0 : register
val s1 : register
val ra : register
val sp : register
val fp : register
val gp : register
val zero : register
(** Constantes representing the registrers. [zero] is fixed to 0 *)
type label = string
(** Address labes are represented by strings. *)
type 'a operand
val oreg : register operand
val oi : int operand
val oi32 : int32 operand
(** abstract type to represent the last operand of an arithmetic expression
as well as 3 constants (either a register, or an integer, or a 32b integer).
*)
(** {1 Arithmetic operations } *)
val li : register -> int -> text
val li32 : register -> int32 -> text
(** Loading integer constants *)
val abs : register -> register -> text
(** [abs r1 r2] stores in r1 the absolute value of r2 *)
val neg : register -> register -> text
(** [neg r1 r2] stores in r1 the opposite of r2 *)
val add : register -> register -> 'a operand -> 'a -> text
val sub : register -> register -> 'a operand -> 'a -> text
val mul : register -> register -> 'a operand -> 'a -> text
val rem : register -> register -> 'a operand -> 'a -> text
val div : register -> register -> 'a operand -> 'a -> text
(** The 5 base arithmetic operations: [add rdst rsrc1 ospec o]
stores destination register rdst the result of operation between source register rscr1 and o.
The constant ospec specifies whether o is an immediate, an immediate over 32 bits or a register.
Example:
[add v0 v1 oreg v2]
[div v0 v1 oi 424]
[sub t0 a0 oi32 2147483647l]
*)
(** {1 Logical Operations } *)
val and_ : register -> register -> register -> text
val or_ : register -> register -> register -> text
val not_ : register -> register -> text
val clz : register -> register -> text
(** Logical operations "and", "or", and "not" manipulating bits pointwise
and "clz" (counting leading zero) *)
(** {1 Comparisons } *)
val seq : register -> register -> register -> text
val sge : register -> register -> register -> text
val sgt : register -> register -> register -> text
val sle : register -> register -> register -> text
val slt : register -> register -> register -> text
val sne : register -> register -> register -> text
(** conditional [sop ra rb rc] sets [ra] to 1 if [rb op rc] and to 0
otherwise (eq : ==, ge : >=, gt : >, le : <=, lt : <=,
ne : !=) *)
(** {1 Jumps } *)
val b : label -> text
(** unconditional jump *)
val beq : register -> register -> label -> text
val bne : register -> register -> label -> text
val bge : register -> register -> label -> text
val bgt : register -> register -> label -> text
val ble : register -> register -> label -> text
val blt : register -> register -> label -> text
(** [bop ra rb label] branches to the label [label] if [ra op rb] *)
val beqz : register -> label -> text
val bnez : register -> label -> text
val bgez : register -> label -> text
val bgtz : register -> label -> text
val blez : register -> label -> text
val bltz : register -> label -> text
(** [bopz ra rb label] branchse to le label [label] if [ra op 0] *)
val jr : register -> text
(** [jr r] Continues the execution at the address specified by the register [r] *)
val jal : label -> text
(** [jal l] Continues the execution at the address specified by the label [l],
and stores the return address in $ra.
*)
val jalr : register -> text
(** [jalr r] Continues the execution at the address specified by the
register [r], and stores the return address in $ra.
*)
(** {1 Reading from / writing to the memory } *)
type 'a address
(** abstract type to represent memory addresses *)
val alab : label address
val areg : (int * register) address
(** The adresses are either given by a label, or by a pair (offset, register) *)
val la : register -> 'a address -> 'a -> text
(** [la reg alab "foo"] stores in [reg] the address of the label "foo"
[la reg1 areg (x, reg2)] stores in [reg1] the address stores in the register
[reg2] at the offset of [x] octets
*)
val lbu : register -> 'a address -> 'a -> text
(** stores the octet at a given address without sign extension (value between 0 and 255) *)
val lw : register -> 'a address -> 'a -> text
(** stores 32bits integer at a given address *)
val sb : register -> 'a address -> 'a -> text
(** writes the 8 least significant bits of a given register at a given address *)
val sw : register -> 'a address -> 'a -> text
(** write the content of the register at a given address *)
val move : register -> register -> text
(** {1 Miscellaneous } *)
val nop : [> ] asm
(** Empty instruction instruction. Can be used both in .text and .data *)
val label : label -> [> ] asm
(** A label. Can be used both in .text and .data *)
val syscall : text
(** System call instruction *)
val comment : string -> [> ] asm
(** Includes a comment in the generated code. Can be used both in .text and .data *)
val align : int -> [> ] asm
(** [align n] alignes the code following an instruction on 2^n octets *)
val asciiz : string -> data
(** places a string value in the data zone *)
val dword : int list -> data
(** places a list of memory words in the data zone *)
val address : label list -> data
(** places a list of adresses (denoted by labels) in data zone *)
val space: int -> data
(** [space n] allocates [n] octets in the data segment *)
val inline: string -> [> ] asm
(** [inline s] copies the string [s] as such in the assembly file *)
val ( ++ ) : ([< `text|`data ] asm as 'a)-> 'a -> 'a
(** concatenates two pieces of code (either text with text, or data with
data) *)
(** {1 Manipulation of the stack} *)
val push : register -> text
(** [push r] stores the content of [r] at the top of the stack
Note : $sp points to the addrees of the last occupied cell of the stack *)
val pop : register -> text
(** [pop r] stores the mot at the top of the stack in [r] et pops the stack head *)
val popn: int -> text
(** [popn n] pops [n] octets from the stack *)
val peek : register -> text
(** [peek r] stores the word at the stack head in [r] without popping the stack head *)
(** {1 Example } *)
(** In the the program below, on the left is pure MIPS code and on the right is
its representation using OCaml commands above. The program loads two
constants, performs a few arithmetic operations and prints the result on
the screen.
{[
.text | { text =
main: | label "main"
#stores 42 in $a0 and 23 in $a1 | ++ comment "stores 42 in $a0 and 23 in $a1"
li $a0, 42 | ++ li a0 42
li $a1, 23 | ++ li a1 23
mul $a0, $a0, $a1 | ++ mul a0 a0 oreg a1 (* we use oreg to indicate that the
| last operand is a register *)
#stores the content of $a0 on the stack | ++ comment "stores the content of $a0 on the stack"
sub $sp, $sp, 4 | ++ sub sp sp oi 4
sw $a0, 0($sp) | ++ sw a0 areg (0, sp)
|
jal print_int | ++ jal "print_int"
|
#termines | ++ comment "termines"
li $v0, 10 | ++ li v0 10
syscall | ++ syscall
|
print_int: | ++ label "print_int"
lw $a0, 0($sp) | ++ lw a0 areg (0, sp)
add $sp, $sp, 4 | ++ add sp sp oi 4
li $v0, 1 | ++ li v0 1
syscall | ++ syscall
la $a0, newline | ++ la a0 alab "newline"
li $v0, 4 | ++ li v0 4
syscall | ++ syscall
jr $ra | ++ jr ra ; (* end the of text label *)
|
.data | data =
newline: | label "newline"
.asciiz "\n" | ++ asciiz "\n" ;
| } (* end of the OCaml record *)
]}
*)