diff options
| -rw-r--r-- | src/mips.ml | 322 | ||||
| -rw-r--r-- | src/mips.mli | 329 |
2 files changed, 425 insertions, 226 deletions
diff --git a/src/mips.ml b/src/mips.ml index f2ef3db..5fe310c 100644 --- a/src/mips.ml +++ b/src/mips.ml @@ -1,186 +1,158 @@ +(* Bibliothèque pour produire du code MIPS -type register = - | ZERO | A0 | A1 | A2 | V0 | T0 | T1 | T2 | S0 | RA | SP | FP + 2008 Jean-Christophe Filliâtre (CNRS) + 2013 Kim Nguyen (Université Paris Sud) +*) -type address = - | Alab of string - | Areg of int * register - -type operand = - | Oimm of int - | Oreg of register - -type arith = Add | Sub | Mul | Div | Rem +open Format -type condition = Eq | Ne | Le | Lt | Ge | Gt +type register = string +let v0 : register = "$v0" +let v1 : register = "$v1" +let a0 : register = "$a0" +let a1 : register = "$a1" +let a2 : register = "$a2" +let a3 : register = "$a3" +let t0 : register = "$t0" +let t1 : register = "$t1" +let t2 : register = "$t2" +let t3 : register = "$t3" +let s0 : register = "$s0" +let s1 : register = "$s1" +let ra : register = "$ra" +let sp : register = "$sp" +let fp : register = "$fp" +let gp : register = "$gp" +let zero : register = "$zero" type label = string - -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 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 code = - | Clist of instruction list - | Capp of code * code - -let nop = Clist [] - -let mips l = Clist l - -let inline s = Clist [Inline s] - -let (++) c1 c2 = Capp (c1, c2) +type 'a address = formatter -> 'a -> unit +let alab : label address = fun fmt (s : label) -> fprintf fmt "%s" s +let areg : (int * register) address = fun fmt (x, y) -> fprintf fmt "%i(%s)" x y +type 'a operand = formatter -> 'a -> unit +let oreg : register operand = fun fmt (r : register) -> fprintf fmt "%s" r +let oi : int operand = fun fmt i -> fprintf fmt "%i" i +let oi32 : int32 operand = fun fmt i -> fprintf fmt "%li" i + +type 'a asm = + | Nop + | S of string + | Cat of 'a asm * 'a asm + +type text = [`text ] asm +type data = [`data ] asm + +let buf = Buffer.create 17 +let fmt = formatter_of_buffer buf +let ins x = + Buffer.add_char buf '\t'; + kfprintf (fun fmt -> + fprintf fmt "\n"; + pp_print_flush fmt (); + let s = Buffer.contents buf in + Buffer.clear buf; + S s + ) fmt x + +let pr_list fmt pr = function + | [] -> () + | [i] -> pr fmt i + | i :: ll -> pr fmt i; List.iter (fun i -> fprintf fmt ", %a" pr i) ll + +let pr_ilist fmt l = + pr_list fmt (fun fmt i -> fprintf fmt "%i" i) l + +let pr_alist fmt l = + pr_list fmt (fun fmt (a : label) -> fprintf fmt "%s" a) l + +let abs a b = ins "abs %s, %s" a b +let add a b (o : 'a operand) x = ins "add %s, %s, %a" a b o x +let clz a b = ins "clz %s, %s" a b +let and_ a b c = ins "and %s, %s, %s" a b c +let div a b (o : 'a operand) x = ins "div %s, %s, %a" a b o x +let mul a b (o : 'a operand) x = ins "mul %s, %s, %a" a b o x +let or_ a b c = ins "or %s, %s, %s" a b c +let not_ a b = ins "not %s, %s" a b +let rem a b (o : 'a operand) x = ins "rem %s, %s, %a" a b o x +let neg a b = ins "neg %s, %s" a b +let sub a b (o : 'a operand) = ins "sub %s, %s, %a" a b o +let li a b = ins "li %s, %i" a b +let li32 a b = ins "li %s, %li" a b +let seq a b c = ins "seq %s, %s, %s" a b c +let sge a b c = ins "sge %s, %s, %s" a b c +let sgt a b c = ins "sgt %s, %s, %s" a b c +let sle a b c = ins "sle %s, %s, %s" a b c +let slt a b c = ins "slt %s, %s, %s" a b c +let sne a b c = ins "sne %s, %s, %s" a b c +let b (z : label) = ins "b %s" z +let beq x y (z : label) = ins "beq %s, %s, %s" x y z +let bne x y (z : label) = ins "bne %s, %s, %s" x y z +let bge x y (z : label) = ins "bge %s, %s, %s" x y z +let bgt x y (z : label) = ins "bgt %s, %s, %s" x y z +let ble x y (z : label) = ins "ble %s, %s, %s" x y z +let blt x y (z : label) = ins "blt %s, %s, %s" x y z + +let beqz x (z : label) = ins "beqz %s, %s" x z +let bnez x (z : label) = ins "bnez %s, %s" x z +let bgez x (z : label) = ins "bgez %s, %s" x z +let bgtz x (z : label) = ins "bgtz %s, %s" x z +let blez x (z : label) = ins "blez %s, %s" x z +let bltz x (z : label) = ins "bltz %s, %s" x z + +let jr a = ins "jr %s" a +let jal (z : label) = ins "jal %s" z +let jalr (z : register) = ins "jalr %s" z +let la x (p : 'a address) = ins "la %s, %a" x p +let lb x (p : 'a address) = ins "lb %s, %a" x p +let lbu x (p : 'a address) = ins "lbu %s, %a" x p +let lw x (p : 'a address) = ins "lw %s, %a" x p +let sb x (p : 'a address) = ins "sb %s, %a" x p +let sw x (p : 'a address) = ins "sw %s, %a" x p +let move a b = ins "move %s, %s" a b +let nop = Nop +let label (s : label) = S (s ^ ":\n") +let syscall = S "\tsyscall\n" +let comment s = S ("#" ^ s ^ "\n") +let align n = ins ".align %i" n +let asciiz s = ins ".asciiz %S" s +let dword l = ins ".word %a" pr_ilist l +let address l = ins ".word %a" pr_alist l +let (++) x y = Cat (x, y) + + +let push r = + sub sp sp oi 4 ++ + sw r areg (0, sp) + +let peek r = + lw r areg (0, sp) + +let pop r = + peek r ++ + add sp sp oi 4 + +let popn n = + add sp sp oi n type program = { - text : code; - data : data list; + text : [ `text ] asm; + data : [ `data ] asm; } -open Format - -let print_register fmt = function - | ZERO -> pp_print_string fmt "$0" - | A0 -> pp_print_string fmt "$a0" - | A1 -> pp_print_string fmt "$a1" - | A2 -> pp_print_string fmt "$a2" - | V0 -> pp_print_string fmt "$v0" - | T0 -> pp_print_string fmt "$t0" - | T1 -> pp_print_string fmt "$t1" - | T2 -> pp_print_string fmt "$t2" - | S0 -> pp_print_string fmt "$s0" - | RA -> pp_print_string fmt "$ra" - | SP -> pp_print_string fmt "$sp" - | FP -> pp_print_string fmt "$fp" - -let print_arith fmt = function - | Add -> pp_print_string fmt "add" - | Sub -> pp_print_string fmt "sub" - | Mul -> pp_print_string fmt "mul" - | Div -> pp_print_string fmt "div" - | Rem -> pp_print_string fmt "rem" - -let print_condition fmt = function - | Eq -> pp_print_string fmt "seq" - | Ne -> pp_print_string fmt "sne" - | Lt -> pp_print_string fmt "slt" - | Le -> pp_print_string fmt "sle" - | Gt -> pp_print_string fmt "sgt" - | Ge -> pp_print_string fmt "sge" - -let print_address fmt = function - | Alab s -> pp_print_string fmt s - | Areg (ofs, r) -> fprintf fmt "%d(%a)" ofs print_register r - -let print_operand fmt = function - | Oimm i -> pp_print_int fmt i - | Oreg r -> print_register fmt r - -let print_instruction fmt = function - | Move (dst, src) -> - fprintf fmt "\tmove %a, %a\n" print_register dst print_register src - | Li (r, i) -> - fprintf fmt "\tli %a, %d\n" print_register r i - | Li32 (r, i) -> - fprintf fmt "\tli %a, %ld\n" print_register r i - | La (r, s) -> - fprintf fmt "\tla %a, %s\n" print_register r s - | Lw (r, a) -> - fprintf fmt "\tlw %a, %a\n" print_register r print_address a - | Sw (r, a) -> - fprintf fmt "\tsw %a, %a\n" print_register r print_address a - | Lb (r, a) -> - fprintf fmt "\tlb %a, %a\n" print_register r print_address a - | Sb (r, a) -> - fprintf fmt "\tsb %a, %a\n" print_register r print_address a - | Arith (a, dst, src, op) -> - fprintf fmt "\t%a %a, %a, %a\n" - print_arith a print_register dst print_register src print_operand op - | Neg (dst, src) -> - fprintf fmt "\tneg %a, %a\n" print_register dst print_register src - | Set (cond, dst, src, op) -> - fprintf fmt "\t%a %a, %a, %a\n" - print_condition cond print_register dst print_register src - print_operand op - | B l -> - fprintf fmt "\tb %s\n" l - | Beq (r1, r2, l) -> - fprintf fmt "\tbeq %a, %a, %s\n" print_register r1 print_register r2 l - | Beqz (r, l) -> - fprintf fmt "\tbeqz %a, %s\n" print_register r l - | Bnez (r, l) -> - fprintf fmt "\tbnez %a, %s\n" print_register r l - | J s -> - fprintf fmt "\tj %s\n" s - | Jal s -> - fprintf fmt "\tjal %s\n" s - | Jalr r -> - fprintf fmt "\tjalr %a\n" print_register r - | Jr r -> - fprintf fmt "\tjr %a\n" print_register r - | Syscall -> - fprintf fmt "\tsyscall\n" - | Label s -> - fprintf fmt "%s:\n" s - | Inline s -> - fprintf fmt "%s" s - -let rec print_code fmt = function - | Clist l -> List.iter (print_instruction fmt) l - | Capp (c1, c2) -> print_code fmt c1; print_code fmt c2 - -let print_word fmt = function - | Wint n -> pp_print_int fmt n - | Waddr s -> pp_print_string fmt s - -let rec print_list print fmt = function - | [] -> () - | [x] -> print fmt x - | x :: r -> fprintf fmt "%a, %a" print x (print_list print) r - -let print_data fmt = function - | Asciiz (l, s) -> - fprintf fmt "%s:\n\t.asciiz %S\n" l s - | Word (l, n) -> - fprintf fmt "%s:\n\t.word %a\n" l (print_list print_word) n - | Space (l, n) -> - fprintf fmt "%s:\n\t.space %d\n" l n - | Align n -> - fprintf fmt "\t.align %d\n" n +let rec pr_asm fmt = function + | Nop -> () + | S s -> fprintf fmt "%s" s + | Cat (a1, a2) -> pr_asm fmt a1; pr_asm fmt a2 let print_program fmt p = - fprintf fmt "\t.text\n"; - print_code fmt p.text; - fprintf fmt "\t.data\n"; - List.iter (print_data fmt) p.data; - fprintf fmt "@." - - + fprintf fmt ".text\n"; + pr_asm fmt p.text; + fprintf fmt ".data\n"; + pr_asm fmt p.data; + pp_print_flush fmt () + +let print_in_file ~file p = + let c = open_out file in + let fmt = formatter_of_out_channel c in + print_program fmt p; + close_out c 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 *) + ]} +*) |