Changeset 1286 for src/RTLabs

Timestamp:

Oct 3, 2011, 4:07:22 PM (8 years ago)

Author:

mulligan

Message:

more changes to the rtl abs to rtl pass

File:

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

src/RTLabs/RTLAbstoRTL.ma

@@ -323 +323 @@
   ].
 
-(*
-
 (* TODO: examine this properly.  This is a change from the O'caml code due
    to us dropping the explicit use of a cast destination size field.  We
@@ -331 +329 @@
 *)
 definition translate_op1 ≝
+  λglobals: list ident.
   λop1: unary_operation.
   λdestrs: list register.
@@ -337 +336 @@
   λstart_lbl: label.
   λdest_lbl: label.
-  λdef: rtl_internal_function.
+  λdef: rtl_internal_function globals.
   match op1 with
   [ Ocastint src_sign src_size ⇒
     let dest_size ≝ |destrs| * 8 in
     let src_size ≝ bitsize_of_intsize src_size in
-      translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
+      translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
   | Onegint ⇒
-      translate_negint destrs srcrs start_lbl dest_lbl def prf
+      translate_negint globals destrs srcrs start_lbl dest_lbl def prf
   | Onotbool ⇒
-      translate_notbool destrs srcrs start_lbl dest_lbl def
+      translate_notbool globals destrs srcrs start_lbl dest_lbl def
   | Onotint ⇒
-    let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
+    let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
     let l ≝ map2 … f destrs srcrs prf in
-      adds_graph l start_lbl dest_lbl def
+      adds_graph rtl_params1 globals l start_lbl dest_lbl def
   | Optrofint r ⇒
-      translate_move destrs srcrs start_lbl dest_lbl def
+      translate_move globals destrs srcrs start_lbl dest_lbl def
   | Ointofptr r ⇒
-      translate_move destrs srcrs start_lbl dest_lbl def
+      translate_move globals destrs srcrs start_lbl dest_lbl def
   | Oid ⇒
-      translate_move destrs srcrs start_lbl dest_lbl def
+      translate_move globals destrs srcrs start_lbl dest_lbl def
   | _ ⇒ ? (* float operations implemented in runtime *)
   ].
@@ -362 +361 @@
 qed.
   
-definition translate_op ≝
+definition translate_op: ∀globals. ? → list register → list register → list register →
+  label → label → rtl_internal_function globals → rtl_internal_function globals ≝
+  λglobals: list ident.
   λop.
-  λdestrs.
-  λsrcrs1.
-  λsrcrs2.
-  λstart_lbl.
-  λdest_lbl.
-  λdef.
+  λdestrs: list register.
+  λsrcrs1: list register.
+  λsrcrs2: list register.
+  λstart_lbl: label.
+  λdest_lbl: label.
+  λdef: rtl_internal_function globals.
   match reduce_strong register register srcrs1 srcrs2 with
   [ dp reduced first_reduced_proof ⇒
@@ -386 +387 @@
         let destrs_rest ≝ \snd (\fst reduced) in
         let srcrs_cted ≝ \fst (\snd reduced) in
-        let 〈def, tmpr〉 ≝ fresh_reg def in
+        let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
         let insts_init ≝ [
-          rtl_st_clear_carry start_lbl;
-          rtl_st_int tmpr (zero ?) start_lbl
+          sequential … (CLEAR_CARRY …);
+          sequential … (INT rtl_params_ globals tmpr (zero …))
         ] in
-        let f_add ≝ λdestr. λsrcr1. λsrcr2. rtl_st_op2 op destr srcr1 srcr2 start_lbl in
-        let insts_add ≝ map3 … f_add destrs_common srcrsl_common srcrsr_common ? ? in
-        let f_add_cted ≝ λdestr. λsrcr. rtl_st_op2 op destr srcr tmpr start_lbl in
-        let insts_add_cted ≝ map2 ? ? ? f_add_cted destrs_cted srcrs_cted ? in
-        let f_rest ≝ λdestr. rtl_st_op2 op destr tmpr tmpr start_lbl in
+        let f_add ≝ λdestr. λsrcr1. λsrcr2. sequential … (OP2 rtl_params_ globals op destr srcr1 srcr2) in
+        let insts_add ≝ map3 ? ? ? ? f_add destrs_common srcrsl_common srcrsr_common ? ? in
+        let f_add_cted ≝ λdestr. λsrcr. sequential … (OP2 rtl_params_ globals op destr srcr tmpr) in
+        let insts_add_cted ≝ map2 … f_add_cted destrs_cted srcrs_cted ? in
+        let f_rest ≝ λdestr. sequential … (OP2 rtl_params_ globals op destr tmpr tmpr) in
         let insts_rest ≝ map … f_rest destrs_rest in
-          adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
+          adds_graph rtl_params1 globals (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
       ]
     ]
@@ -403 +404 @@
   [1: @third_reduced_proof
   |3: @first_reduced_proof
-  |*: cases daemon (* TODO *)
+  |*: cases daemon (* XXX: some of these look like they may be false *)
   ]
 qed.
 
 let rec translate_mul1
-  (dummy: register) (tmpr: register) (destrs: list register)
-  (srcrs1: list register) (srcr2: register) (start_lbl: label)
-    on srcrs1 ≝
+  (globals: list ident) (dummy: register) (tmpr: register)
+    (destrs: list register) (srcrs1: list register) (srcr2: register)
+      (start_lbl: label)
+        on srcrs1 ≝
   match destrs with
-  [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl
+  [ nil ⇒ adds_graph rtl_params1 globals [ GOTO … ] start_lbl
   | cons destr tl ⇒
     match tl with
@@ -418 +420 @@
       match srcrs1 with
       [ nil ⇒
-        adds_graph [
-          rtl_st_int tmpr (zero ?) start_lbl;
-          rtl_st_op2 Addc destr destr tmpr start_lbl
+        adds_graph rtl_params1 globals [
+          sequential … (INT rtl_params_ globals tmpr (zero …));
+          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
         ] start_lbl
       | cons srcr1 tl' ⇒
-        adds_graph [
-          rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;
-          rtl_st_op2 Addc destr destr tmpr start_lbl
+        adds_graph rtl_params1 globals [
+          sequential … (OPACCS rtl_params_ globals Mul tmpr dummy srcr2 srcr1);
+          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
         ] start_lbl
       ]
@@ -431 +433 @@
       match srcrs1 with
       [ nil ⇒
-        add_translates [
-          adds_graph [
-            rtl_st_int tmpr (zero ?) start_lbl;
-            rtl_st_op2 Addc destr destr tmpr start_lbl;
-            rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
+        add_translates rtl_params1 globals [
+          adds_graph rtl_params1 globals [
+            sequential … (INT rtl_params_ globals tmpr (zero …));
+            sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
+            sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
           ];
-          translate_cst (Ointconst I8 (zero ?)) destrs
+          translate_cst globals (Ointconst I8 (zero …)) destrs
         ] start_lbl
       | cons srcr1 srcrs1 ⇒
         match destrs with
         [ nil ⇒
-          add_translates [
-            adds_graph [
-              rtl_st_int tmpr (zero ?) start_lbl;
-              rtl_st_op2 Addc destr destr tmpr start_lbl;
-              rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
+          add_translates rtl_params1 globals [
+            adds_graph rtl_params1 globals [
+              sequential … (INT rtl_params_ globals tmpr (zero …));
+              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
+              sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
             ];
-            translate_cst (Ointconst I8 (zero ?)) destrs
+            translate_cst globals (Ointconst I8 (zero ?)) destrs
           ] start_lbl
         | cons destr2 destrs ⇒
-          add_translates [
-            adds_graph [
-              rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;
-              rtl_st_op2 Addc destr destr tmpr start_lbl
+          add_translates rtl_params1 globals [
+            adds_graph rtl_params1 globals [
+              sequential … (OPACCS rtl_params_ globals Mul tmpr destr2 srcr2 srcr1);
+              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
             ];
-            translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2
+            translate_mul1 globals dummy tmpr (destr2 :: destrs) srcrs1 srcr2
           ] start_lbl
         ]
@@ -464 +466 @@
 
 definition translate_muli ≝
+  λglobals: list ident.
   λdummy: register.
   λtmpr: register.
@@ -474 +477 @@
   λtranslates: list ?.
   λsrcr2i: register.
-  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in
+  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split … tmp_destrs i i_prf in
   let tmp_destrs2' ≝
     match tmp_destrs2 with
     [ nil ⇒ [ ]
     | cons tmp_destr2 tmp_destrs2 ⇒ [
-        adds_graph [
-          rtl_st_clear_carry dummy_lbl;
-          rtl_st_int tmp_destr2 (zero ?) dummy_lbl
+        adds_graph rtl_params1 globals [
+          sequential rtl_params_ globals (CLEAR_CARRY …);
+          sequential … (INT rtl_params_ globals tmp_destr2 (zero …))
         ];
-        translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i;
-        translate_cst (Ointconst I8 (zero ?)) tmp_destrs1;
-        adds_graph [
-          rtl_st_clear_carry dummy_lbl
+        translate_mul1 globals dummy tmpr tmp_destrs2 srcrs1 srcr2i;
+        translate_cst globals (Ointconst I8 (zero …)) tmp_destrs1;
+        adds_graph rtl_params1 globals [
+          sequential rtl_params_ globals (CLEAR_CARRY …)
         ];
-        translate_op Addc destrs destrs tmp_destrs
+        translate_op globals Addc destrs destrs tmp_destrs
       ]
     ]
@@ -495 +498 @@
 
 axiom translate_mul:
+  ∀globals: list ident.
   ∀destrs: list register.
   ∀srcrs1: list register.
@@ -500 +504 @@
   ∀start_lbl: label.
   ∀dest_lbl: label.
-  ∀def: rtl_internal_function.
-    rtl_internal_function.
+  ∀def: rtl_internal_function globals.
+    rtl_internal_function globals.
 
 (*