Meilleur module Mips

1 files changed, 278 insertions, 51 deletions

diff --git a/src/mips.mli b/src/mips.mli
index 551df62..a42f1ce 100644
--- a/src/mips.mli
+++ b/src/mips.mli
@@ -1,64 +1,291 @@
 
-type register =
-  | ZERO | A0 | A1 | A2 | V0 | T0 | T1 | T2 | S0 | RA | SP | FP
+(* Bibliothèque pour produire du code MIPS
 
-type address =
-  | Alab of string
-  | Areg of int * register
+   2008 Jean-Christophe Filliâtre (CNRS)
+   - version initiale
 
-type operand =
-  | Oimm of int
-  | Oreg of register
+   2013 Kim Nguyen (Université Paris Sud)
+   - sous-types text et data
+   - types fantômes pour oreg et oi
+   - plus d'opérations et de directives
+   - manipulation de la pile
+   - ocamldoc
+*)
 
-type arith = Add | Sub | Mul | Div | Rem
+(** {0 Bibliothèque pour l'écriture de programmes MIPS } *)
 
-type condition = Eq | Ne | Le | Lt | Ge | Gt
 
-type label = string
+(** Le module {!Mips} permet l'écriture de code MIPS dans du code
+    OCaml, sans utiliser un préprocesseur.  Un exemple complet est
+    donné {{:#1_Exemple}ci-dessous, dans la section exemple}. *)
+
+type 'a asm
+(** type abstrait pour représenter du code assembleur. Le paramètre
+    ['a] est utilisé comme type fantôme. *)
 
-type instruction =
-  | Move of register * register
-  | Li of register * int
-  | Li32 of register * int32
-  | La of register * label
-  | Lw of register * address
-  | Sw of register * address
-  | Lb of register * address
-  | Sb of register * address
-  | Arith of arith * register * register * operand
-  | Neg of register * register
-  | Set of condition * register * register * operand
-  | B of label
-  | Beq of register * register * label
-  | Beqz of register * label
-  | Bnez of register * label
-  | J of string
-  | Jal of string
-  | Jr of register
-  | Jalr of register
-  | Syscall
-  | Label of string
-  | Inline of string
-
-type code
-
-val nop : code
-val mips : instruction list -> code
-val inline : string -> code
-val (++) : code -> code -> code
-
-type word = Wint of int | Waddr of string
-
-type data =
-  | Asciiz of string * string
-  | Word of string * word list
-  | Space of string * int
-  | Align of int
+type text = [ `text ] asm
+(** type représentant du code assembleur se trouvant dans la zone de
+    texte *)
+
+type data = [ `data ] asm
+(** type représentant du code assembleur se trouvant dans la zone de
+    données *)
 
 type program = {
-  text : code;
-  data : data list;
+  text : text;
+  data : data;
 }
+(** un programme est constitué d'une zone de texte et d'une zone de
+    donnée *)
 
 val print_program : Format.formatter -> program -> unit
+  (** [print_program fmt p] imprime le code du programme [p] dans le
+      formatter [fmt] *)
+
+val print_in_file: file:string -> program -> unit
+
+type register
+(** Type abstrait pour les registres *)
+
+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 représentant les registres manipulables. [zero] est
+    cablé à 0 *)
+
+
+type label = string
+(** Les étiquettes d'addresses sont des chaines de caractères *)
+
+type 'a operand
+val oreg : register operand
+val oi : int operand
+val oi32 : int32 operand
+
+(** type abstrait pour représenter la dernière opérande d'une
+    expression arithmétique ainsi que 3 constantes (soit un registre,
+    soit un entier, soit un entier 32 bits)
+*)
+
+
+
+(** {1 Opérations arithmétiques } *)
+
+
+val li : register -> int -> text
+val li32 : register -> int32 -> text
+(** Chargement des constantes entières *)
+
+val abs : register -> register -> text
+(** [abs r1 r2] stocke dans r1 la valeur absolue de r2 *)
+
+val neg : register -> register -> text
+(** [neg r1 r2] stocke dans r1 l'opposé de 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
+
+(** Les 5 opérations arithmétique de base: [add rdst rsrc1 ospec o]
+   stocke dans rdst le résultat de l'opération entre rsrc1 et o. La
+   constant ospec spécifie si o est un immédiat, immédiat sur 32 bits
+   ou un registre.
+   Exemple:
+
+   [add v0 v1 oreg v2]
+
+   [div v0 v1 oi 424]
+
+   [sub t0 a0 oi32 2147483647l]
+ *)
+
+(** {1 Opérations logiques } *)
+
+val and_ : register -> register -> register -> text
+val or_ : register -> register -> register -> text
+val not_ : register -> register -> text
+val clz : register -> register -> text
+(** Opérations de manipulation de bits. "et" bit à bit, "ou" bit à
+    bit, "not" bit à bit et clz (count leading zero) *)
+
+
+(** {1 Comparaisons } *)
+
+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
+  (** conditionnelles [sop ra rb rc] met [ra] à 1 si [rb op rc] et à 0
+      dans le cas contraire (eq : ==, ge : >=, gt : >, le : <=, lt : <=,
+      ne : !=) *)
+
+(** {1 Sauts } *)
+
+val b : label -> text
+(** saut inconditionnel *)
+
+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] branche vers le label [label] si [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] branche vers le label [label] si [ra op 0] *)
+
+
+val jr : register -> text
+(** [jr r] Continue l'exécution à l'adresse spécifiée dans le registre
+    [r] *)
+val jal : label -> text
+(** [jal l] Continue l'exécution à l'adresse spécifiée par le label [l],
+    sauve l'adresse de retour dans $ra.
+*)
+val jalr : register -> text
+(** [jalr r] Continue l'exécution à l'adresse spécifiée par le
+    registre [r], sauve l'adresse de retour dans $ra.
+*)
+
+(** {1 Lecture / écriture en mémoire } *)
+
+type 'a address
+(** type abstrait pour représenter des adresses *)
+
+val alab : label address
+val areg : (int * register) address
+(** Les adresses sont soit données par un label, soit par une paire
+    décalage, registre *)
+
+val la : register -> 'a address -> 'a -> text
+(** [la reg alab "foo"] charge dans [reg] l'adresse du label "foo"
+    [la reg1 areg (x, reg2)] charge dans [reg1] l'adresse contenue dans
+    [reg2] décallée de [x] octets
+ *)
+
+val lbu : register -> 'a address -> 'a -> text
+(** charge l'octet à l'adresse donnée sans extension de signe (valeur
+    entre 0 et 255) *)
+val lw : register -> 'a address -> 'a -> text
+(** charge l'entier 32bits à l'adresse donnée *)
+val sb : register -> 'a address -> 'a -> text
+(** écrit les 8 bits de poid faible du registre donnée à l'adresse
+    donnée *)
+val sw : register -> 'a address -> 'a -> text
+(** écrit le contenu du registre à l'adresse donnée *)
+val move : register -> register -> text
+
+(** {1 Divers } *)
+
+val nop : [> ] asm
+(** l'instruction vide. Peut se trouver dans du text ou du data *)
+
+val label : label ->  [> ] asm
+(** un label. Peut se retrouver dans du text ou du data *)
+
+val syscall : text
+(** l'instruction syscall *)
+
+val comment : string -> [> ] asm
+(** place un commentaire dans le code généré. Peut se retrouver dans
+    du text ou du data *)
+
+val align : int ->  [> ] asm
+(** [align n] aligne le code suivant l'instruction sur 2^n octets *)
+
+val asciiz : string -> data
+(** place une constante chaîne de carctères (terminées par 0) dans a
+    zone data *)
+
+val dword : int list -> data
+(** place une liste de mots mémoires dans la zone data *)
+
+val address : label list -> data
+(** place une liste d'adresses (dénotées par des labels) dans la zone
+    data *)
+
+val ( ++ ) : ([< `text|`data ] asm as 'a)-> 'a -> 'a
+(** concatène deux bouts de codes (soit text avec text, soit data avec
+    data) *)
+
+(** {1 Manipulation de la pile} *)
+
+val push : register -> text
+(** [push r] place le contenu de [r] au sommet de la pile.
+    Rappel : $sp pointe sur l'adresse de la dernière case occupée *)
+
+val pop : register -> text
+(** [pop r] place le mot en sommet de pile dans [r] et dépile *)
+
+val popn: int -> text
+(** [popn n] dépile [n] octets *)
+
+val peek : register -> text
+(** [peek r] place le mot en sommet de pile dans [r] sans dépiler *)
+
+(** {1 Exemple } *)
+
+(** Le programme ci-dessous, donné à gauche en pur MIPS et à droite en
+    OCaml, charge deux constantes, effectue quelques opérations
+    arithétiques et affiche le résultat à l'écran
 
+    {[
+        .text                                                |  { text =
+        main:                                                |        label "main"
+         #charge 42 dans $a0 et 23 dans $a1                  |    ++  comment "charge 42 dans $a0 et 23 dans $a1"
+         li $a0,  42                                         |    ++  li  a0 42
+         li $a1,  23                                         |    ++  li  a1 23
+         mul $a0, $a0, $a1                                   |    ++  mul a0 a0 oreg a1 (* on utilise oreg pour dire que la dernière
+                                                             |                             operande est un registre *)
+         #place le contenu de $a0 sur la pile                |    ++  comment "place le contenu de $a0 sur la pile"
+         sub $sp, $sp, 4                                     |    ++  sub sp sp oi 4
+         sw  $a0,  0($sp)                                    |    ++  sw a0 areg (0, sp)
+                                                             |
+         #appelle une routine d'affichage                    |    ++  comment "appelle la routine d'affichage"
+         jal print_int                                       |    ++  jal "print_int"
+                                                             |
+         #termine                                            |    ++  comment "termine"
+         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
+         #affiche un retour chariot                          |    ++  comment "affiche un retour chariot"
+         la $a0, newline                                     |    ++  la a0 alab "newline"
+         li $v0, 4                                           |    ++  li v0  4
+         syscall                                             |    ++  syscall
+         jr $ra                                              |    ++  jr ra  ; (* fin du label text *)
+                                                             |
+        .data                                                |    data =
+       newline:                                              |        label "newline"
+        .asciiz  "\n"                                        |    ++  asciiz "\n" ;
+                                                             |  } (* fin du record *)
+    ]}
+*)