Changeset 1060 for src/RTLabs

Timestamp:

Jul 8, 2011, 12:17:14 PM (8 years ago)

Author:

mulligan

Message:

work from this morning and yesterday

File:

• src/RTLabs/RTLAbstoRTL.ma (modified) (4 diffs)

src/RTLabs/RTLAbstoRTL.ma

@@ -3 +3 @@
 include "common/AssocList.ma".
 include "common/Graphs.ma".
-include "common/Maps.ma".
 (* include "common/IntValue.ma". *)
 include "common/FrontEndOps.ma".
@@ -227 +226 @@
   | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
   | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
-  | rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2 lbl
+  | rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl
   | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
   | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
@@ -238 +237 @@
   | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
   | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
+  | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl
+  | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl
   | rtl_st_return r ⇒ rtl_st_return r
   ].
@@ -299 +300 @@
   λsrcrs: list register.
   λstart_lbl: label.
+    match reduce_strong register destrs srcrs with
+    [ dp crl_crr len_proof ⇒
+      let commonl ≝ \fst (\fst crl_crr) in
+      let commonr ≝ \fst (\snd crl_crr) in
+      let restl ≝ \snd (\fst crl_crr) in
+      let restr ≝ \snd (\snd crl_crr) in
+      let f_common ≝ translate_move_internal start_lbl in
+      let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
+      let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
+        add_translates [ translate1 ; translate2 ] start_lbl
+    ].
+    @len_proof
+qed.
+
+let rec make
+  (A: Type[0]) (elt: A) (n: nat) on n ≝
+  match n with
+  [ O ⇒ [ ]
+  | S n' ⇒ elt :: make A elt n'
+  ].
+  
+lemma make_length:
+  ∀A: Type[0].
+  ∀elt: A.
+  ∀n: nat.
+    n = length ? (make A elt n).
+  #A #ELT #N
+  elim N
+  [ normalize %
+  | #N #IH
+    normalize <IH %
+  ]
+qed.
+
+definition translate_cast_unsigned ≝
+  λdestrs.
+  λstart_lbl.
+  λdest_lbl.
+  λdef.
+  let 〈def, tmp_zero〉 ≝ fresh_reg def in
+  let zeros ≝ make ? tmp_zero (length ? destrs) in
+    add_translates [
+      adds_graph [
+        rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl
+        ];
+      translate_move destrs zeros
+    ] start_lbl dest_lbl def.
+
+definition translate_cast_signed ≝
+  λdestrs.
+  λsrcr.
+  λstart_lbl.
+  λdest_lbl.
+  λdef.
+  let 〈def, tmp_128〉 ≝ fresh_reg def in
+  let 〈def, tmp_255〉 ≝ fresh_reg def in
+  let 〈def, tmpr〉 ≝ fresh_reg def in
+  let 〈def, dummy〉 ≝ fresh_reg def in
+  let insts ≝ [
+    rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
+    rtl_st_op2 And tmpr tmp_128 srcr start_lbl;
+    rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl;
+    rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl;
+    rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
+  ] in
+  let srcrs ≝ make ? tmpr (length ? destrs) in
+    add_translates [
+      adds_graph insts;
+      translate_move destrs srcrs
+    ] start_lbl dest_lbl def.
+
+definition translate_cast ≝
+  λsrc_size.
+  λsrc_sign.
+  λdest_size.
+  λdestrs.
+  λsrcrs.
+  match | srcrs | return λx. | srcrs | = x → ? with
+  [ O ⇒ λzero_prf. adds_graph [ ]
+  | S n' ⇒ λsucc_prf.
+    if ltb dest_size src_size then
+      translate_move destrs srcrs
+    else
+      match reduce_strong ? destrs srcrs with
+      [ dp crl len_proof ⇒
+        let commonl ≝ \fst (\fst crl) in
+        let commonr ≝ \fst (\snd crl) in
+        let restl ≝ \snd (\fst crl) in
+        let restr ≝ \snd (\snd crl) in
+        let insts_common ≝ translate_move commonl commonr in
+        let sign_reg ≝ last_safe ? srcrs ? in
+        let insts_sign ≝
+          match src_sign with
+          [ Unsigned ⇒ translate_cast_unsigned restl
+          | Signed ⇒ translate_cast_signed restl sign_reg
+          ]
+        in
+          add_translates [ insts_common; insts_sign ]
+      ]
+  ] (refl ? (|srcrs|)).
+  >succ_prf //
+qed.
+
+definition translate_negint ≝
+  λdestrs.
+  λsrcrs.
+  λstart_lbl.
+  λdest_lbl.
+  λdef.
+  λprf: | destrs | = | srcrs |. (* assert in caml code *)
+  let 〈def, tmpr〉 ≝ fresh_reg def in
+  let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
+  let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in
+  let insts_init ≝ [
+    rtl_st_set_carry start_lbl;
+    rtl_st_int tmpr (zero ?) start_lbl
+  ] in
+  let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in
+  let insts_add ≝ map … f_add destrs in
+    adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
+
+definition translate_notbool ≝
+  λdestrs.
+  λsrcrs.
+  λstart_lbl.
+  λdest_lbl.
+  λdef.
+  match destrs with
+  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
+  | cons destr destrs ⇒
+    let 〈def, tmpr〉 ≝ fresh_reg def in
+    let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in
+    let save_srcrs ≝ translate_move tmp_srcrs srcrs in
+    let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in
+    let f ≝ λtmp_srcr. [
+      rtl_st_clear_carry start_lbl;
+      rtl_st_int tmpr (zero ?) start_lbl;
+      rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;
+      rtl_st_int tmpr (zero ?) start_lbl;
+      rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;
+      rtl_st_op2 Xor destr destr tmpr start_lbl
+    ] in
+    let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in
+    let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in
+      add_translates [
+        save_srcrs; adds_graph insts; epilogue
+      ] start_lbl dest_lbl def
+  ].
+
+definition translate_intermediate_op1 ≝
+  λop1.
+  λdestrs.
+  λsrcrs.
+  λstart_lbl.
+  λdest_lbl.
+  λdef.
   λprf: | destrs | = | srcrs |.
-    let 〈crl, crr〉 ≝ reduce register destrs srcrs in
-    let 〈commonl, restl〉 ≝ crl in
-    let 〈commonr, restr〉 ≝ crr in
-    let f_common ≝ translate_move_internal start_lbl in
-    let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
-    let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
-      add_translates [ translate1 ; translate2 ] start_lbl.
-    
-let rec translate_move destrs srcrs start_lbl =
-  let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
-  let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
-  let translates1 = adds_graph (List.map2 f_common common1 common2) in
-  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
-  add_translates [translates1 ; translates2] start_lbl
+  match op1 with
+  [ intermediate_op1_cast src_size src_sign dest_size ⇒
+      translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
+  | intermediate_op1_negint ⇒
+      translate_negint destrs srcrs start_lbl dest_lbl def prf
+  | intermediate_op1_notbool ⇒
+      translate_notbool destrs srcrs start_lbl dest_lbl def
+  | intermediate_op1_notint ⇒
+    let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
+    let l ≝ map2 … f destrs srcrs prf in
+      adds_graph l start_lbl dest_lbl def
+  | intermediate_op1_ptrofint ⇒
+      translate_move destrs srcrs start_lbl dest_lbl def
+  | intermediate_op1_intofptr ⇒
+      translate_move destrs srcrs start_lbl dest_lbl def
+  | intermediate_op1_id ⇒
+      translate_move destrs srcrs start_lbl dest_lbl def
+  ].
 
 definition filter_and_to_list_local_env_internal ≝