summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/mips.ml322
-rw-r--r--src/mips.mli329
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 *)
+ ]}
+*)