(* Bibliothèque pour produire du code MIPS 2008 Jean-Christophe Filliâtre (CNRS) - version initiale 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 *) (** {0 Bibliothèque pour l'écriture de programmes MIPS } *) (** 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 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 : 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 t4 : register val t5 : register val t6 : register val t7 : register val t8 : register val t9 : 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 *) ]} *)