1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
|
(* 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 *)
]}
*)
|
