diff options
Diffstat (limited to 'src/mips.mli')
| -rw-r--r-- | src/mips.mli | 329 |
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 *) + ]} +*) |