99 open Hints_declaration
147 (** val dpi1__o__Reg_to_dec__o__inject :
148 (I8051.register, 'a1) Types.dPair -> Interference.decision Types.sig0 **)
149 let dpi1__o__Reg_to_dec__o__inject x2 =
150 Interference.Decision_colour x2.Types.dpi1
152 (** val eject__o__Reg_to_dec__o__inject :
153 I8051.register Types.sig0 -> Interference.decision Types.sig0 **)
154 let eject__o__Reg_to_dec__o__inject x2 =
155 Interference.Decision_colour (Types.pi1 x2)
157 (** val reg_to_dec__o__inject :
158 I8051.register -> Interference.decision Types.sig0 **)
159 let reg_to_dec__o__inject x1 =
160 Interference.Decision_colour x1
162 (** val dpi1__o__Reg_to_dec :
163 (I8051.register, 'a1) Types.dPair -> Interference.decision **)
164 let dpi1__o__Reg_to_dec x1 =
165 Interference.Decision_colour x1.Types.dpi1
167 (** val eject__o__Reg_to_dec :
168 I8051.register Types.sig0 -> Interference.decision **)
169 let eject__o__Reg_to_dec x1 =
170 Interference.Decision_colour (Types.pi1 x1)
173 | Arg_decision_colour of I8051.register
174 | Arg_decision_spill of Nat.nat
175 | Arg_decision_imm of BitVector.byte
177 (** val arg_decision_rect_Type4 :
178 (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
179 arg_decision -> 'a1 **)
180 let rec arg_decision_rect_Type4 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
181 | Arg_decision_colour x_19045 -> h_arg_decision_colour x_19045
182 | Arg_decision_spill x_19046 -> h_arg_decision_spill x_19046
183 | Arg_decision_imm x_19047 -> h_arg_decision_imm x_19047
185 (** val arg_decision_rect_Type5 :
186 (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
187 arg_decision -> 'a1 **)
188 let rec arg_decision_rect_Type5 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
189 | Arg_decision_colour x_19052 -> h_arg_decision_colour x_19052
190 | Arg_decision_spill x_19053 -> h_arg_decision_spill x_19053
191 | Arg_decision_imm x_19054 -> h_arg_decision_imm x_19054
193 (** val arg_decision_rect_Type3 :
194 (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
195 arg_decision -> 'a1 **)
196 let rec arg_decision_rect_Type3 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
197 | Arg_decision_colour x_19059 -> h_arg_decision_colour x_19059
198 | Arg_decision_spill x_19060 -> h_arg_decision_spill x_19060
199 | Arg_decision_imm x_19061 -> h_arg_decision_imm x_19061
201 (** val arg_decision_rect_Type2 :
202 (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
203 arg_decision -> 'a1 **)
204 let rec arg_decision_rect_Type2 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
205 | Arg_decision_colour x_19066 -> h_arg_decision_colour x_19066
206 | Arg_decision_spill x_19067 -> h_arg_decision_spill x_19067
207 | Arg_decision_imm x_19068 -> h_arg_decision_imm x_19068
209 (** val arg_decision_rect_Type1 :
210 (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
211 arg_decision -> 'a1 **)
212 let rec arg_decision_rect_Type1 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
213 | Arg_decision_colour x_19073 -> h_arg_decision_colour x_19073
214 | Arg_decision_spill x_19074 -> h_arg_decision_spill x_19074
215 | Arg_decision_imm x_19075 -> h_arg_decision_imm x_19075
217 (** val arg_decision_rect_Type0 :
218 (I8051.register -> 'a1) -> (Nat.nat -> 'a1) -> (BitVector.byte -> 'a1) ->
219 arg_decision -> 'a1 **)
220 let rec arg_decision_rect_Type0 h_arg_decision_colour h_arg_decision_spill h_arg_decision_imm = function
221 | Arg_decision_colour x_19080 -> h_arg_decision_colour x_19080
222 | Arg_decision_spill x_19081 -> h_arg_decision_spill x_19081
223 | Arg_decision_imm x_19082 -> h_arg_decision_imm x_19082
225 (** val arg_decision_inv_rect_Type4 :
226 arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
227 -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
228 let arg_decision_inv_rect_Type4 hterm h1 h2 h3 =
229 let hcut = arg_decision_rect_Type4 h1 h2 h3 hterm in hcut __
231 (** val arg_decision_inv_rect_Type3 :
232 arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
233 -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
234 let arg_decision_inv_rect_Type3 hterm h1 h2 h3 =
235 let hcut = arg_decision_rect_Type3 h1 h2 h3 hterm in hcut __
237 (** val arg_decision_inv_rect_Type2 :
238 arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
239 -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
240 let arg_decision_inv_rect_Type2 hterm h1 h2 h3 =
241 let hcut = arg_decision_rect_Type2 h1 h2 h3 hterm in hcut __
243 (** val arg_decision_inv_rect_Type1 :
244 arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
245 -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
246 let arg_decision_inv_rect_Type1 hterm h1 h2 h3 =
247 let hcut = arg_decision_rect_Type1 h1 h2 h3 hterm in hcut __
249 (** val arg_decision_inv_rect_Type0 :
250 arg_decision -> (I8051.register -> __ -> 'a1) -> (Nat.nat -> __ -> 'a1)
251 -> (BitVector.byte -> __ -> 'a1) -> 'a1 **)
252 let arg_decision_inv_rect_Type0 hterm h1 h2 h3 =
253 let hcut = arg_decision_rect_Type0 h1 h2 h3 hterm in hcut __
255 (** val arg_decision_discr : arg_decision -> arg_decision -> __ **)
256 let arg_decision_discr x y =
257 Logic.eq_rect_Type2 x
259 | Arg_decision_colour a0 -> Obj.magic (fun _ dH -> dH __)
260 | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
261 | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y
263 (** val arg_decision_jmdiscr : arg_decision -> arg_decision -> __ **)
264 let arg_decision_jmdiscr x y =
265 Logic.eq_rect_Type2 x
267 | Arg_decision_colour a0 -> Obj.magic (fun _ dH -> dH __)
268 | Arg_decision_spill a0 -> Obj.magic (fun _ dH -> dH __)
269 | Arg_decision_imm a0 -> Obj.magic (fun _ dH -> dH __)) y
271 (** val dpi1__o__Reg_to_arg_dec__o__inject :
272 (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **)
273 let dpi1__o__Reg_to_arg_dec__o__inject x2 =
274 Arg_decision_colour x2.Types.dpi1
276 (** val eject__o__Reg_to_arg_dec__o__inject :
277 I8051.register Types.sig0 -> arg_decision Types.sig0 **)
278 let eject__o__Reg_to_arg_dec__o__inject x2 =
279 Arg_decision_colour (Types.pi1 x2)
281 (** val reg_to_arg_dec__o__inject :
282 I8051.register -> arg_decision Types.sig0 **)
283 let reg_to_arg_dec__o__inject x1 =
284 Arg_decision_colour x1
286 (** val dpi1__o__Reg_to_arg_dec :
287 (I8051.register, 'a1) Types.dPair -> arg_decision **)
288 let dpi1__o__Reg_to_arg_dec x1 =
289 Arg_decision_colour x1.Types.dpi1
291 (** val eject__o__Reg_to_arg_dec :
292 I8051.register Types.sig0 -> arg_decision **)
293 let eject__o__Reg_to_arg_dec x1 =
294 Arg_decision_colour (Types.pi1 x1)
296 (** val preserve_carry_bit :
297 AST.ident List.list -> Bool.bool -> Joint.joint_seq List.list ->
298 Joint.joint_seq List.list **)
299 let preserve_carry_bit globals do_it steps =
302 List.Cons ((Joint.Extension_seq (Obj.magic Joint_LTL_LIN.SAVE_CARRY)),
303 (List.append steps (List.Cons ((Joint.Extension_seq
304 (Obj.magic Joint_LTL_LIN.RESTORE_CARRY)), List.Nil))))
305 | Bool.False -> steps
307 (** val a : Types.unit0 **)
311 (** val dpi1__o__beval_of_byte__o__inject :
312 (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval Types.sig0 **)
313 let dpi1__o__beval_of_byte__o__inject x2 =
314 ByteValues.BVByte x2.Types.dpi1
316 (** val eject__o__beval_of_byte__o__inject :
317 BitVector.byte Types.sig0 -> ByteValues.beval Types.sig0 **)
318 let eject__o__beval_of_byte__o__inject x2 =
319 ByteValues.BVByte (Types.pi1 x2)
321 (** val beval_of_byte__o__inject :
322 BitVector.byte -> ByteValues.beval Types.sig0 **)
323 let beval_of_byte__o__inject x1 =
326 (** val dpi1__o__beval_of_byte :
327 (BitVector.byte, 'a1) Types.dPair -> ByteValues.beval **)
328 let dpi1__o__beval_of_byte x1 =
329 ByteValues.BVByte x1.Types.dpi1
331 (** val eject__o__beval_of_byte :
332 BitVector.byte Types.sig0 -> ByteValues.beval **)
333 let eject__o__beval_of_byte x1 =
334 ByteValues.BVByte (Types.pi1 x1)
336 (** val set_dp_by_offset :
337 AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
338 let set_dp_by_offset globals off =
339 List.Cons ((Joint.MOVE
340 (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, (Joint.byte_of_nat off))))),
341 (List.Cons ((Joint.OP2 (BackEndOps.Add, (Obj.magic a), (Obj.magic a),
342 (Obj.magic (Joint.hdw_argument_from_reg I8051.registerSPL)))), (List.Cons
344 (Obj.magic (Joint_LTL_LIN.From_acc (I8051.RegisterDPL, a)))), (List.Cons
346 (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, Joint.zero_byte)))), (List.Cons
347 ((Joint.OP2 (BackEndOps.Addc, (Obj.magic a), (Obj.magic a),
348 (Obj.magic (Joint.hdw_argument_from_reg I8051.registerSPH)))), (List.Cons
350 (Obj.magic (Joint_LTL_LIN.From_acc (I8051.RegisterDPH, a)))),
354 AST.ident List.list -> Nat.nat -> I8051.register -> Nat.nat ->
355 Joint.joint_seq List.list **)
356 let get_stack globals localss r off =
357 let off0 = Nat.plus localss off in
358 List.append (set_dp_by_offset globals off0)
359 (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
360 (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
361 (match I8051.eq_Register r I8051.RegisterA with
362 | Bool.True -> List.Nil
364 List.Cons ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.From_acc (r, a)))),
367 (** val set_stack_not_a :
368 AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
369 Joint.joint_seq List.list **)
370 let set_stack_not_a globals localss off r =
371 let off0 = Nat.plus localss off in
372 List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE
373 (Obj.magic (Joint_LTL_LIN.To_acc (a, r)))), (List.Cons ((Joint.STORE
374 ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
377 (** val set_stack_a :
378 AST.ident List.list -> Nat.nat -> Nat.nat -> Joint.joint_seq List.list **)
379 let set_stack_a globals localss off =
380 List.append (List.Cons ((Joint.MOVE
381 (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerST1, a)))), List.Nil))
382 (set_stack_not_a globals localss off I8051.registerST1)
385 AST.ident List.list -> Nat.nat -> Nat.nat -> I8051.register ->
386 Joint.joint_seq List.list **)
387 let set_stack globals localss off r =
388 match I8051.eq_Register r I8051.RegisterA with
389 | Bool.True -> set_stack_a globals localss off
390 | Bool.False -> set_stack_not_a globals localss off r
392 (** val set_stack_int :
393 AST.ident List.list -> Nat.nat -> Nat.nat -> BitVector.byte ->
394 Joint.joint_seq List.list **)
395 let set_stack_int globals localss off int =
396 let off0 = Nat.plus localss off in
397 List.append (set_dp_by_offset globals off0) (List.Cons ((Joint.MOVE
398 (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), (List.Cons
399 ((Joint.STORE ((Obj.magic Types.It), (Obj.magic Types.It),
400 (Obj.magic a))), List.Nil))))
403 AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
404 arg_decision -> Joint.joint_seq List.list **)
405 let move globals localss carry_lives_after dst src =
407 | Interference.Decision_spill dsto ->
409 | Arg_decision_colour srcr ->
410 preserve_carry_bit globals carry_lives_after
411 (set_stack globals localss dsto srcr)
412 | Arg_decision_spill srco ->
413 (match Nat.eqb srco dsto with
414 | Bool.True -> List.Nil
416 preserve_carry_bit globals carry_lives_after
417 (List.append (get_stack globals localss I8051.RegisterA srco)
418 (set_stack globals localss dsto I8051.RegisterA)))
419 | Arg_decision_imm int ->
420 preserve_carry_bit globals carry_lives_after
421 (set_stack_int globals localss dsto int))
422 | Interference.Decision_colour dstr ->
424 | Arg_decision_colour srcr ->
425 (match I8051.eq_Register dstr srcr with
426 | Bool.True -> List.Nil
428 (match I8051.eq_Register dstr I8051.RegisterA with
430 List.Cons ((Joint.MOVE
431 (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), List.Nil)
433 (match I8051.eq_Register srcr I8051.RegisterA with
435 List.Cons ((Joint.MOVE
436 (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil)
438 List.Cons ((Joint.MOVE
439 (Obj.magic (Joint_LTL_LIN.To_acc (a, srcr)))), (List.Cons
441 (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))),
443 | Arg_decision_spill srco ->
444 preserve_carry_bit globals carry_lives_after
445 (get_stack globals localss dstr srco)
446 | Arg_decision_imm int ->
447 List.append (List.Cons ((Joint.MOVE
448 (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, int)))), List.Nil))
449 (match I8051.eq_Register dstr I8051.RegisterA with
450 | Bool.True -> List.Nil
452 List.Cons ((Joint.MOVE
453 (Obj.magic (Joint_LTL_LIN.From_acc (dstr, a)))), List.Nil)))
455 (** val arg_is_spilled : arg_decision -> Bool.bool **)
456 let arg_is_spilled = function
457 | Arg_decision_colour x0 -> Bool.False
458 | Arg_decision_spill x0 -> Bool.True
459 | Arg_decision_imm x0 -> Bool.False
461 (** val is_spilled : Interference.decision -> Bool.bool **)
462 let is_spilled = function
463 | Interference.Decision_spill x0 -> Bool.True
464 | Interference.Decision_colour x0 -> Bool.False
467 AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
468 let newframe globals stack_sz =
469 List.Cons (Joint.CLEAR_CARRY, (List.Cons ((Joint.MOVE
470 (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons
471 ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a),
472 (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))),
473 (List.Cons ((Joint.MOVE
474 (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons
475 ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))),
476 (List.Cons ((Joint.OP2 (BackEndOps.Sub, (Obj.magic a), (Obj.magic a),
477 (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons
479 (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))),
480 List.Nil)))))))))))))
483 AST.ident List.list -> Nat.nat -> Joint.joint_seq List.list **)
484 let delframe globals stack_sz =
485 List.Cons ((Joint.MOVE
486 (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPL)))), (List.Cons
487 ((Joint.OP2 (BackEndOps.Add, (Obj.magic a), (Obj.magic a),
488 (Obj.magic (Joint.hdw_argument_from_byte (Joint.byte_of_nat stack_sz))))),
489 (List.Cons ((Joint.MOVE
490 (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPL, a)))), (List.Cons
491 ((Joint.MOVE (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerSPH)))),
492 (List.Cons ((Joint.OP2 (BackEndOps.Addc, (Obj.magic a), (Obj.magic a),
493 (Obj.magic (Joint.hdw_argument_from_byte Joint.zero_byte)))), (List.Cons
495 (Obj.magic (Joint_LTL_LIN.From_acc (I8051.registerSPH, a)))),
498 (** val commutative : BackEndOps.op2 -> Bool.bool **)
499 let commutative = function
500 | BackEndOps.Add -> Bool.True
501 | BackEndOps.Addc -> Bool.True
502 | BackEndOps.Sub -> Bool.False
503 | BackEndOps.And -> Bool.True
504 | BackEndOps.Or -> Bool.True
505 | BackEndOps.Xor -> Bool.True
507 (** val uses_carry : BackEndOps.op2 -> Bool.bool **)
508 let uses_carry = function
509 | BackEndOps.Add -> Bool.False
510 | BackEndOps.Addc -> Bool.True
511 | BackEndOps.Sub -> Bool.True
512 | BackEndOps.And -> Bool.False
513 | BackEndOps.Or -> Bool.False
514 | BackEndOps.Xor -> Bool.False
516 (** val sets_carry : BackEndOps.op2 -> Bool.bool **)
517 let sets_carry = function
518 | BackEndOps.Add -> Bool.True
519 | BackEndOps.Addc -> Bool.True
520 | BackEndOps.Sub -> Bool.True
521 | BackEndOps.And -> Bool.False
522 | BackEndOps.Or -> Bool.False
523 | BackEndOps.Xor -> Bool.False
525 (** val translate_op2 :
526 AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
527 Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
529 let translate_op2 globals localss carry_lives_after op dst arg1 arg2 =
531 (preserve_carry_bit globals
532 (Bool.andb (uses_carry op)
533 (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2)))
535 (move globals localss Bool.False (Interference.Decision_colour
536 I8051.RegisterB) arg2)
537 (move globals localss Bool.False (Interference.Decision_colour
538 I8051.RegisterA) arg1)))
539 (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a), (Obj.magic a),
540 (Obj.magic (Joint.hdw_argument_from_reg I8051.RegisterB)))), List.Nil))
541 (move globals localss (Bool.andb (sets_carry op) carry_lives_after) dst
542 (Arg_decision_colour I8051.RegisterA)))
544 (** val translate_op2_smart :
545 AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op2 ->
546 Interference.decision -> arg_decision -> arg_decision -> Joint.joint_seq
548 let translate_op2_smart globals localss carry_lives_after op dst arg1 arg2 =
549 preserve_carry_bit globals
550 (Bool.andb (Bool.andb (Bool.notb (sets_carry op)) carry_lives_after)
551 (Bool.orb (Bool.orb (arg_is_spilled arg1) (arg_is_spilled arg2))
554 | Arg_decision_colour arg2r ->
556 (move globals localss (uses_carry op) (Interference.Decision_colour
557 I8051.RegisterA) arg1)
558 (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
559 (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_reg arg2r)))),
561 (move globals localss
562 (Bool.andb (sets_carry op) carry_lives_after) dst
563 (Arg_decision_colour I8051.RegisterA)))
564 | Arg_decision_spill x ->
565 (match commutative op with
568 | Arg_decision_colour arg1r ->
570 (move globals localss (uses_carry op)
571 (Interference.Decision_colour I8051.RegisterA) arg2)
572 (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
574 (Obj.magic (Joint.hdw_argument_from_reg arg1r)))),
576 (move globals localss
577 (Bool.andb (sets_carry op) carry_lives_after) dst
578 (Arg_decision_colour I8051.RegisterA)))
579 | Arg_decision_spill x0 ->
580 translate_op2 globals localss carry_lives_after op dst arg1 arg2
581 | Arg_decision_imm arg1i ->
583 (move globals localss (uses_carry op)
584 (Interference.Decision_colour I8051.RegisterA) arg2)
585 (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
587 (Obj.magic (Joint.hdw_argument_from_byte arg1i)))),
589 (move globals localss
590 (Bool.andb (sets_carry op) carry_lives_after) dst
591 (Arg_decision_colour I8051.RegisterA))))
593 translate_op2 globals localss carry_lives_after op dst arg1 arg2)
594 | Arg_decision_imm arg2i ->
596 (move globals localss (uses_carry op) (Interference.Decision_colour
597 I8051.RegisterA) arg1)
598 (List.append (List.Cons ((Joint.OP2 (op, (Obj.magic a),
599 (Obj.magic a), (Obj.magic (Joint.hdw_argument_from_byte arg2i)))),
601 (move globals localss
602 (Bool.andb (sets_carry op) carry_lives_after) dst
603 (Arg_decision_colour I8051.RegisterA))))
605 (** val dec_to_arg_dec : Interference.decision -> arg_decision **)
606 let dec_to_arg_dec = function
607 | Interference.Decision_spill n -> Arg_decision_spill n
608 | Interference.Decision_colour r -> Arg_decision_colour r
610 (** val reg_to_dec__o__dec_arg_dec__o__inject :
611 I8051.register -> arg_decision Types.sig0 **)
612 let reg_to_dec__o__dec_arg_dec__o__inject x0 =
613 dec_to_arg_dec (Interference.Decision_colour x0)
615 (** val dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject :
616 (I8051.register, 'a1) Types.dPair -> arg_decision Types.sig0 **)
617 let dpi1__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
618 dec_to_arg_dec (dpi1__o__Reg_to_dec x2)
620 (** val eject__o__Reg_to_dec__o__dec_arg_dec__o__inject :
621 I8051.register Types.sig0 -> arg_decision Types.sig0 **)
622 let eject__o__Reg_to_dec__o__dec_arg_dec__o__inject x2 =
623 dec_to_arg_dec (eject__o__Reg_to_dec x2)
625 (** val dpi1__o__dec_arg_dec__o__inject :
626 (Interference.decision, 'a1) Types.dPair -> arg_decision Types.sig0 **)
627 let dpi1__o__dec_arg_dec__o__inject x2 =
628 dec_to_arg_dec x2.Types.dpi1
630 (** val eject__o__dec_arg_dec__o__inject :
631 Interference.decision Types.sig0 -> arg_decision Types.sig0 **)
632 let eject__o__dec_arg_dec__o__inject x2 =
633 dec_to_arg_dec (Types.pi1 x2)
635 (** val dec_arg_dec__o__inject :
636 Interference.decision -> arg_decision Types.sig0 **)
637 let dec_arg_dec__o__inject x1 =
640 (** val reg_to_dec__o__dec_arg_dec : I8051.register -> arg_decision **)
641 let reg_to_dec__o__dec_arg_dec x0 =
642 dec_to_arg_dec (Interference.Decision_colour x0)
644 (** val dpi1__o__Reg_to_dec__o__dec_arg_dec :
645 (I8051.register, 'a1) Types.dPair -> arg_decision **)
646 let dpi1__o__Reg_to_dec__o__dec_arg_dec x1 =
647 dec_to_arg_dec (dpi1__o__Reg_to_dec x1)
649 (** val eject__o__Reg_to_dec__o__dec_arg_dec :
650 I8051.register Types.sig0 -> arg_decision **)
651 let eject__o__Reg_to_dec__o__dec_arg_dec x1 =
652 dec_to_arg_dec (eject__o__Reg_to_dec x1)
654 (** val dpi1__o__dec_arg_dec :
655 (Interference.decision, 'a1) Types.dPair -> arg_decision **)
656 let dpi1__o__dec_arg_dec x1 =
657 dec_to_arg_dec x1.Types.dpi1
659 (** val eject__o__dec_arg_dec :
660 Interference.decision Types.sig0 -> arg_decision **)
661 let eject__o__dec_arg_dec x1 =
662 dec_to_arg_dec (Types.pi1 x1)
664 (** val translate_op1 :
665 AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.op1 ->
666 Interference.decision -> Interference.decision -> Joint.joint_seq
668 let translate_op1 globals localss carry_lives_after op dst arg =
670 Bool.andb carry_lives_after (Bool.orb (is_spilled dst) (is_spilled arg))
672 preserve_carry_bit globals preserve_carry
674 (move globals localss Bool.False (Interference.Decision_colour
675 I8051.RegisterA) (dec_to_arg_dec arg)) (List.Cons ((Joint.OP1 (op,
676 (Obj.magic Types.It), (Obj.magic Types.It))),
677 (move globals localss Bool.False dst (Arg_decision_colour
680 (** val translate_opaccs :
681 AST.ident List.list -> Nat.nat -> Bool.bool -> BackEndOps.opAccs ->
682 Interference.decision -> Interference.decision -> arg_decision ->
683 arg_decision -> Joint.joint_seq List.list **)
684 let translate_opaccs globals localss carry_lives_after op dst1 dst2 arg1 arg2 =
686 (move globals localss Bool.False (Interference.Decision_colour
687 I8051.RegisterB) arg2)
689 (move globals localss Bool.False (Interference.Decision_colour
690 I8051.RegisterA) arg1) (List.Cons ((Joint.OPACCS (op,
691 (Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic Types.It),
692 (Obj.magic Types.It))),
694 (move globals localss Bool.False dst1 (Arg_decision_colour
697 (move globals localss Bool.False dst2 (Arg_decision_colour
699 (match Bool.andb carry_lives_after
700 (Bool.orb (is_spilled dst1) (is_spilled dst2)) with
701 | Bool.True -> List.Cons (Joint.CLEAR_CARRY, List.Nil)
702 | Bool.False -> List.Nil))))))
705 AST.ident List.list -> Nat.nat -> arg_decision -> arg_decision ->
706 Joint.joint_seq List.list **)
707 let move_to_dp globals localss arg1 arg2 =
708 match Bool.notb (arg_is_spilled arg1) with
711 (move globals localss Bool.False (Interference.Decision_colour
712 I8051.RegisterDPH) arg2)
713 (move globals localss Bool.False (Interference.Decision_colour
714 I8051.RegisterDPL) arg1)
716 (match Bool.notb (arg_is_spilled arg2) with
719 (move globals localss Bool.False (Interference.Decision_colour
720 I8051.RegisterDPL) arg1)
721 (move globals localss Bool.False (Interference.Decision_colour
722 I8051.RegisterDPH) arg2)
725 (move globals localss Bool.False (Interference.Decision_colour
726 I8051.RegisterB) arg1)
728 (move globals localss Bool.False (Interference.Decision_colour
729 I8051.RegisterDPH) arg2)
730 (move globals localss Bool.False (Interference.Decision_colour
731 I8051.RegisterDPL) (Arg_decision_colour I8051.RegisterB))))
733 (** val translate_store :
734 AST.ident List.list -> Nat.nat -> Bool.bool -> arg_decision ->
735 arg_decision -> arg_decision -> Joint.joint_seq List.list **)
736 let translate_store globals localss carry_lives_after addr1 addr2 src =
737 preserve_carry_bit globals
738 (Bool.andb carry_lives_after
739 (Bool.orb (Bool.orb (arg_is_spilled addr1) (arg_is_spilled addr1))
740 (arg_is_spilled src)))
741 (let move_to_dptr = move_to_dp globals localss addr1 addr2 in
743 (match arg_is_spilled src with
746 (move globals localss Bool.False (Interference.Decision_colour
747 I8051.registerST0) src)
748 (List.append move_to_dptr (List.Cons ((Joint.MOVE
749 (Obj.magic (Joint_LTL_LIN.To_acc (a, I8051.registerST0)))),
752 List.append move_to_dptr
753 (move globals localss Bool.False (Interference.Decision_colour
754 I8051.RegisterA) src)) (List.Cons ((Joint.STORE
755 ((Obj.magic Types.It), (Obj.magic Types.It), (Obj.magic a))),
758 (** val translate_load :
759 AST.ident List.list -> Nat.nat -> Bool.bool -> Interference.decision ->
760 arg_decision -> arg_decision -> Joint.joint_seq List.list **)
761 let translate_load globals localss carry_lives_after dst addr1 addr2 =
762 preserve_carry_bit globals
763 (Bool.andb carry_lives_after
764 (Bool.orb (Bool.orb (is_spilled dst) (arg_is_spilled addr1))
765 (arg_is_spilled addr1)))
766 (List.append (move_to_dp globals localss addr1 addr2)
767 (List.append (List.Cons ((Joint.LOAD ((Obj.magic a),
768 (Obj.magic Types.It), (Obj.magic Types.It))), List.Nil))
769 (move globals localss Bool.False dst (Arg_decision_colour
772 (** val translate_address :
773 __ List.list -> Nat.nat -> Bool.bool -> __ -> BitVector.word ->
774 Interference.decision -> Interference.decision -> Joint.joint_seq
776 let translate_address globals localss carry_lives_after id off addr1 addr2 =
777 preserve_carry_bit (Obj.magic globals)
778 (Bool.andb carry_lives_after
779 (Bool.orb (is_spilled addr1) (is_spilled addr2))) (List.Cons
780 ((Joint.ADDRESS ((Obj.magic id), off, (Obj.magic Types.It),
781 (Obj.magic Types.It))),
783 (move (Obj.magic globals) localss Bool.False addr1 (Arg_decision_colour
785 (move (Obj.magic globals) localss Bool.False addr2 (Arg_decision_colour
786 I8051.RegisterDPH)))))
788 (** val translate_step :
789 AST.ident List.list -> Joint.joint_internal_function -> Nat.nat ->
790 Fixpoints.valuation -> Interference.coloured_graph -> Nat.nat ->
791 Graphs.label -> Joint.joint_step -> Blocks.bind_step_block **)
792 let translate_step globals fn localss after grph stack_sz lbl s =
794 (let lookup = fun r -> grph.Interference.colouring (Types.Inl r) in
795 let lookup_arg = fun a0 ->
797 | Joint.Reg r -> dec_to_arg_dec (lookup r)
798 | Joint.Imm b -> Arg_decision_imm b
800 let carry_lives_after = Liveness.hlives I8051.RegisterCarry (after lbl)
802 let move0 = move globals localss carry_lives_after in
803 (match Liveness.eliminable_step globals (after lbl) s with
806 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
812 | Joint.COST_LABEL cost_lbl ->
813 { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x ->
814 Joint.COST_LABEL cost_lbl) }; Types.snd = List.Nil }
815 | Joint.CALL (f, n_args, x) ->
818 { Types.fst = { Types.fst = List.Nil; Types.snd = (fun x0 ->
819 Joint.CALL ((Types.Inl f0), n_args, (Obj.magic Types.It))) };
820 Types.snd = List.Nil }
822 let { Types.fst = dpl; Types.snd = dph } = dp in
823 { Types.fst = { Types.fst =
825 (Blocks.add_dummy_variance
826 (move_to_dp globals localss (Obj.magic lookup_arg dpl)
827 (Obj.magic lookup_arg dph))) (List.Cons ((fun l ->
828 let x0 = Joint.Extension_seq
829 (Obj.magic (Joint_LTL_LIN.LOW_ADDRESS (Obj.magic l)))
831 x0), (List.Cons ((fun x0 -> Joint.PUSH (Obj.magic Types.It)),
832 (List.Cons ((fun l -> Joint.Extension_seq
833 (Obj.magic (Joint_LTL_LIN.HIGH_ADDRESS (Obj.magic l)))),
834 (List.Cons ((fun x0 -> Joint.PUSH (Obj.magic Types.It)),
835 (List.Cons ((fun x0 -> Joint.MOVE
836 (Obj.magic (Joint_LTL_LIN.Int_to_acc (a, Joint.zero_byte)))),
837 List.Nil))))))))))); Types.snd = (fun x0 -> Joint.CALL
838 ((Types.Inr { Types.fst = (Obj.magic Types.It); Types.snd =
839 (Obj.magic Types.It) }), n_args, (Obj.magic Types.It))) };
840 Types.snd = List.Nil })
841 | Joint.COND (r, ltrue) ->
842 { Types.fst = { Types.fst =
843 (Blocks.add_dummy_variance
844 (move0 (Interference.Decision_colour I8051.RegisterA)
845 (dec_to_arg_dec (Obj.magic lookup r)))); Types.snd =
846 (fun x -> Joint.COND ((Obj.magic Types.It), ltrue)) };
847 Types.snd = List.Nil }
848 | Joint.Step_seq s' ->
851 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
852 globals (List.Cons ((Joint.COMMENT c), List.Nil))
853 | Joint.MOVE pair_regs ->
854 let lookup_move_dst = fun x ->
856 | ERTL.PSD r -> lookup r
857 | ERTL.HDW r -> Interference.Decision_colour r
859 let dst = lookup_move_dst (Obj.magic pair_regs).Types.fst in
861 match (Obj.magic pair_regs).Types.snd with
862 | Joint.Reg r -> dec_to_arg_dec (lookup_move_dst r)
863 | Joint.Imm b -> Arg_decision_imm b
865 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
866 globals (move0 dst src)
868 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
869 globals (List.Cons ((Joint.POP (Obj.magic a)),
870 (move0 (Obj.magic lookup r) (Arg_decision_colour
873 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
876 (move0 (Interference.Decision_colour I8051.RegisterA)
877 (Obj.magic lookup_arg a0)) (List.Cons ((Joint.PUSH
878 (Obj.magic a)), List.Nil)))
879 | Joint.ADDRESS (lbl0, off, dpl, dph) ->
880 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
882 (translate_address (Obj.magic globals) localss
883 carry_lives_after (Obj.magic lbl0) off
884 (Obj.magic lookup dpl) (Obj.magic lookup dph))
885 | Joint.OPACCS (op, dst1, dst2, arg1, arg2) ->
886 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
888 (translate_opaccs globals localss carry_lives_after op
889 (Obj.magic lookup dst1) (Obj.magic lookup dst2)
890 (Obj.magic lookup_arg arg1) (Obj.magic lookup_arg arg2))
891 | Joint.OP1 (op, dst, arg) ->
892 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
894 (translate_op1 globals localss carry_lives_after op
895 (Obj.magic lookup dst) (Obj.magic lookup arg))
896 | Joint.OP2 (op, dst, arg1, arg2) ->
897 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
899 (translate_op2_smart globals localss carry_lives_after op
900 (Obj.magic lookup dst) (Obj.magic lookup_arg arg1)
901 (Obj.magic lookup_arg arg2))
902 | Joint.CLEAR_CARRY ->
903 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
904 globals (List.Cons (Joint.CLEAR_CARRY, List.Nil))
906 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
907 globals (List.Cons (Joint.SET_CARRY, List.Nil))
908 | Joint.LOAD (dstr, addr1, addr2) ->
909 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
911 (translate_load globals localss carry_lives_after
912 (Obj.magic lookup dstr) (Obj.magic lookup_arg addr1)
913 (Obj.magic lookup_arg addr2))
914 | Joint.STORE (addr1, addr2, srcr) ->
915 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
917 (translate_store globals localss carry_lives_after
918 (Obj.magic lookup_arg addr1) (Obj.magic lookup_arg addr2)
919 (Obj.magic lookup_arg srcr))
920 | Joint.Extension_seq ext ->
921 Blocks.ensure_step_block (Joint.graph_params_to_params LTL.lTL)
923 (match Obj.magic ext with
924 | ERTL.Ertl_new_frame -> newframe globals stack_sz
925 | ERTL.Ertl_del_frame -> delframe globals stack_sz
926 | ERTL.Ertl_frame_size r ->
927 move0 (lookup r) (Arg_decision_imm
928 (Joint.byte_of_nat stack_sz)))))))
930 (** val translate_fin_step :
931 AST.ident List.list -> Graphs.label -> Joint.joint_fin_step ->
932 Blocks.bind_fin_block **)
933 let translate_fin_step globals lbl s =
934 Bind_new.Bret { Types.fst = List.Nil; Types.snd =
936 | Joint.GOTO l -> Joint.GOTO l
937 | Joint.RETURN -> Joint.RETURN
938 | Joint.TAILCALL (x, x0) -> assert false (* absurd case *)) }
940 (** val translate_data :
941 Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
942 AST.ident List.list -> Joint.joint_closed_internal_function ->
943 (Registers.register, TranslateUtils.b_graph_translate_data)
944 Bind_new.bind_new **)
945 let translate_data the_fixpoint build globals int_fun =
947 Liveness.analyse_liveness the_fixpoint globals (Types.pi1 int_fun)
950 build globals (Types.pi1 int_fun)
951 (Fixpoints.fix_lfp Liveness.register_lattice
952 (Liveness.liveafter globals (Types.pi1 int_fun)) after)
955 Nat.plus coloured_graph.Interference.spilled_no
956 (Types.pi1 int_fun).Joint.joint_if_stacksize
958 Bind_new.Bret { TranslateUtils.init_ret = (Obj.magic Types.It);
959 TranslateUtils.init_params = (Obj.magic Types.It);
960 TranslateUtils.init_stack_size = stack_sz; TranslateUtils.added_prologue =
961 List.Nil; TranslateUtils.new_regs = List.Nil; TranslateUtils.f_step =
962 (translate_step globals (Types.pi1 int_fun)
963 (Types.pi1 int_fun).Joint.joint_if_local_stacksize
964 (Fixpoints.fix_lfp Liveness.register_lattice
965 (Liveness.liveafter globals (Types.pi1 int_fun)) after) coloured_graph
966 stack_sz); TranslateUtils.f_fin = (translate_fin_step globals) }
968 (** val ertl_to_ltl :
969 Fixpoints.fixpoint_computer -> Interference.coloured_graph_computer ->
970 ERTL.ertl_program -> ((LTL.ltl_program, Joint.stack_cost_model)
971 Types.prod, Nat.nat) Types.prod **)
972 let ertl_to_ltl the_fixpoint build pr =
974 TranslateUtils.b_graph_transform_program ERTL.eRTL LTL.lTL
975 (fun globals h -> translate_data the_fixpoint build globals h) pr
977 { Types.fst = { Types.fst = ltlprog; Types.snd =
978 (Joint.stack_cost (Joint.graph_params_to_params LTL.lTL) ltlprog) };
981 (Exp.exp (Nat.S (Nat.S Nat.O)) (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
982 (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
983 Nat.O)))))))))))))))))
984 (Joint.globals_stacksize (Joint.graph_params_to_params LTL.lTL) ltlprog)) }