Changeset 1325 for src/RTLabs/RTLabsToRTL.ma

Timestamp:

Oct 7, 2011, 3:45:13 PM (8 years ago)

Author:

mulligan

Message:

finished implementing the translate constant function

File:

• src/RTLabs/RTLabsToRTL.ma (modified) (5 diffs)

src/RTLabs/RTLabsToRTL.ma

@@ -153 +153 @@
 qed.
 
-let rec translate_cst
-  (globals: list ident) (cst: constant) (destrs: list register)
-    (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals)
-      on cst: rtl_internal_function globals ≝
-  match cst with
-  [ Ointconst size const ⇒
-    match destrs with
-    [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
-    | _   ⇒
-      let size' ≝ size_intsize size in
-        match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with
-        [ true  ⇒ λgood_case.
-          match split_into_bytes size const with
-          [ dp bytes bytes_length_proof ⇒
-            let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
-              adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
-          ]
-        | false ⇒ λbad_case. ?
-        ] (refl … (eqb size' (|destrs|)))
-    ]
-  | Ofloatconst float ⇒ ⊥
-  | Oaddrsymbol id offset ⇒
-    let 〈r1, r2〉 ≝ make_addr … destrs ? in
-      add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def
-  | Oaddrstack offset ⇒
-    let 〈r1, r2〉 ≝ make_addr … destrs ? in
-      ?
-      (* add_graph rtl_params1 globals start_lbl (sequential … (STACK_ADDRESS rtl_params_ globals r1 r2) dest_lbl) def *)
-  ].
-  [1: >bytes_length_proof
-      cut(size' = |destrs|)
-      [1: @eqb_implies_eq
-          assumption
-      |2: #EQ_HYP
-          <EQ_HYP %
-      ]
-  |5: cases not_implemented (* XXX: float, error_float in o'caml *)
-  |*: cases daemon
-  ].
-qed.
-  
-definition translate_move_internal ≝
-  λglobals.
-  λdestr: register.
-  λsrcr: register.
-    sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).
-
-definition translate_move ≝
-  λglobals.
-  λdestrs: list register.
-  λsrcrs: list register.
-  λstart_lbl: label.
-    match reduce_strong register 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 globals in
-      let translate1 ≝ adds_graph rtl_params1 … (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 ≝
-  λglobals.
-  λdestrs.
-  λstart_lbl.
-  λdest_lbl.
-  λdef: joint_internal_function … (rtl_params globals).
-  let 〈def, tmp_zero〉 ≝ fresh_reg … def in
-  let zeros ≝ make … tmp_zero (length … destrs) in
-    add_translates … [
-      adds_graph rtl_params1 … [
-        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))
-        ];
-      translate_move globals destrs zeros
-    ] start_lbl dest_lbl def.
-
-definition translate_cast_signed:
-    ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
-  λglobals: list ident.
-  λ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 ≝ [
-    sequential  … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));
-    sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);
-    sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);
-    sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));
-    sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)
-  ]
-  in
-  let srcrs ≝ make … tmpr (length … destrs) in
-    add_translates rtl_params1 globals [
-      adds_graph rtl_params1 globals insts;
-      translate_move globals destrs srcrs
-    ] start_lbl dest_lbl def.
-
-definition translate_cast ≝
-  λglobals: list ident.
-  λsrc_size: nat.
-  λsrc_sign: signedness.
-  λdest_size: nat.
-  λdestrs: list register.
-  λsrcrs: list register.
-  match |srcrs| return λx. |srcrs| = x → ? with
-  [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]
-  | S n' ⇒ λsucc_prf.
-    if ltb dest_size src_size then
-      translate_move globals destrs srcrs
-    else
-      match reduce_strong register register 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 globals commonl commonr in
-        let sign_reg ≝ last_safe ? srcrs ? in
-        let insts_sign ≝
-          match src_sign with
-          [ Unsigned ⇒ translate_cast_unsigned globals restl
-          | Signed ⇒ translate_cast_signed globals restl sign_reg
-          ]
-        in
-          add_translates rtl_params1 globals [ insts_common; insts_sign ]
-      ]
-  ] (refl ? (|srcrs|)).
-  >succ_prf //
-qed.
-
-definition translate_negint ≝
-  λglobals: list ident.
-  λdestrs: list register.
-  λsrcrs: list register.
-  λstart_lbl: label.
-  λdest_lbl: label.
-  λdef: rtl_internal_function globals.
-  λprf: |destrs| = |srcrs|. (* assert in caml code *)
-  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
-  let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in
-  let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in
-  let insts_init ≝ [
-    sequential … (SET_CARRY …);
-    sequential … (INT rtl_params_ globals tmpr (zero ?))
-  ] in
-  let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in
-  let insts_add ≝ map … f_add destrs in
-    adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
-
-definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
-  λglobals: list ident.
-  λdestrs: list register.
-  λsrcrs: list register.
-  λstart_lbl: label.
-  λdest_lbl: label.
-  λdef: rtl_internal_function globals.
-  match destrs with
-  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def
-  | cons destr destrs ⇒
-    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
-    let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in
-    let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in
-    let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in
-    let f ≝ λtmp_srcr. [
-      sequential … (CLEAR_CARRY rtl_params_ globals);
-      sequential … (INT rtl_params_ globals tmpr (zero ?));
-      sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);
-      sequential … (INT rtl_params_ globals tmpr (zero ?));
-      sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);
-      sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)
-    ] in
-    let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in
-    let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
-      add_translates rtl_params1 globals [
-        save_srcrs; adds_graph rtl_params1 globals insts; epilogue
-      ] start_lbl dest_lbl def
-  ].
-
-(* 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
-   instead infer the size of the cast's destination from the context.  Is
-   this correct?
-*)
-definition translate_op1 ≝
-  λglobals: list ident.
-  λop1: unary_operation.
-  λdestrs: list register.
-  λsrcrs: list register.
-  λprf: |destrs| = |srcrs|.
-  λstart_lbl: label.
-  λdest_lbl: label.
-  λ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 globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
-  | Onegint ⇒
-      translate_negint globals destrs srcrs start_lbl dest_lbl def prf
-  | Onotbool ⇒
-      translate_notbool globals destrs srcrs start_lbl dest_lbl def
-  | Onotint ⇒
-    let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
-    let l ≝ map2 … f destrs srcrs prf in
-      adds_graph rtl_params1 globals l start_lbl dest_lbl def
-  | Optrofint r ⇒
-      translate_move globals destrs srcrs start_lbl dest_lbl def
-  | Ointofptr r ⇒
-      translate_move globals destrs srcrs start_lbl dest_lbl def
-  | Oid ⇒
-      translate_move globals destrs srcrs start_lbl dest_lbl def
-  | _ ⇒ ? (* float operations implemented in runtime *)
-  ].
-  cases not_implemented
-qed.
-  
 definition translate_op: ∀globals. ? → list register → list register → list register →
   label → label → rtl_internal_function globals → rtl_internal_function globals ≝
@@ -444 +198 @@
   |*: cases daemon (* XXX: some of these look like they may be false *)
   ]
+qed.
+
+let rec translate_cst
+  (globals: list ident) (cst: constant) (destrs: list register)
+    (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function globals)
+      on cst: rtl_internal_function globals ≝
+  match cst with
+  [ Ointconst size const ⇒
+    match destrs with
+    [ nil ⇒ add_graph … start_lbl (GOTO … dest_lbl) def
+    | _   ⇒
+      let size' ≝ size_intsize size in
+        match eqb size' (|destrs|) return λx. (eqb size' (|destrs|)) = x → rtl_internal_function globals with
+        [ true  ⇒ λgood_case.
+          match split_into_bytes size const with
+          [ dp bytes bytes_length_proof ⇒
+            let mapped ≝ map2 … (λd. λb. (sequential … (INT rtl_params_ globals d b))) destrs bytes ? in
+              adds_graph rtl_params1 globals mapped start_lbl dest_lbl def
+          ]
+        | false ⇒ λbad_case. ?
+        ] (refl … (eqb size' (|destrs|)))
+    ]
+  | Ofloatconst float ⇒ ⊥
+  | Oaddrsymbol id offset ⇒
+    let 〈r1, r2〉 ≝ make_addr … destrs ? in
+    let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (ADDRESS rtl_params_ globals id ? r1 r2) dest_lbl) def in
+    let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in
+      def
+  | Oaddrstack offset ⇒
+    let 〈r1, r2〉 ≝ make_addr … destrs ? in
+    let def ≝ add_graph rtl_params1 globals start_lbl (sequential … (extension rtl_params_ globals (rtl_st_ext_address r1 r2)) dest_lbl) def in
+    let def ≝ translate_op globals Addc [r1] [r1] [r2] start_lbl dest_lbl def in
+      def
+  ].
+  [1: >bytes_length_proof
+      cut(size' = |destrs|)
+      [1: @eqb_implies_eq
+          assumption
+      |2: #EQ_HYP
+          <EQ_HYP %
+      ]
+  |2: cases daemon (* XXX: bad case where destrs is of the wrong length *)
+  |3: cases not_implemented (* XXX: float, error_float in o'caml *)
+  |*: cases daemon (* XXX: various proofs to be filled in *)
+  ].
+qed.
+  
+definition translate_move_internal ≝
+  λglobals.
+  λdestr: register.
+  λsrcr: register.
+    sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).
+
+definition translate_move ≝
+  λglobals.
+  λdestrs: list register.
+  λsrcrs: list register.
+  λstart_lbl: label.
+    match reduce_strong register 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 globals in
+      let translate1 ≝ adds_graph rtl_params1 … (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 ≝
+  λglobals.
+  λdestrs.
+  λstart_lbl.
+  λdest_lbl.
+  λdef: joint_internal_function … (rtl_params globals).
+  let 〈def, tmp_zero〉 ≝ fresh_reg … def in
+  let zeros ≝ make … tmp_zero (length … destrs) in
+    add_translates … [
+      adds_graph rtl_params1 … [
+        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))
+        ];
+      translate_move globals destrs zeros
+    ] start_lbl dest_lbl def.
+
+definition translate_cast_signed:
+    ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
+  λglobals: list ident.
+  λ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 ≝ [
+    sequential  … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));
+    sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);
+    sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);
+    sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));
+    sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)
+  ]
+  in
+  let srcrs ≝ make … tmpr (length … destrs) in
+    add_translates rtl_params1 globals [
+      adds_graph rtl_params1 globals insts;
+      translate_move globals destrs srcrs
+    ] start_lbl dest_lbl def.
+
+definition translate_cast ≝
+  λglobals: list ident.
+  λsrc_size: nat.
+  λsrc_sign: signedness.
+  λdest_size: nat.
+  λdestrs: list register.
+  λsrcrs: list register.
+  match |srcrs| return λx. |srcrs| = x → ? with
+  [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]
+  | S n' ⇒ λsucc_prf.
+    if ltb dest_size src_size then
+      translate_move globals destrs srcrs
+    else
+      match reduce_strong register register 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 globals commonl commonr in
+        let sign_reg ≝ last_safe ? srcrs ? in
+        let insts_sign ≝
+          match src_sign with
+          [ Unsigned ⇒ translate_cast_unsigned globals restl
+          | Signed ⇒ translate_cast_signed globals restl sign_reg
+          ]
+        in
+          add_translates rtl_params1 globals [ insts_common; insts_sign ]
+      ]
+  ] (refl ? (|srcrs|)).
+  >succ_prf //
+qed.
+
+definition translate_negint ≝
+  λglobals: list ident.
+  λdestrs: list register.
+  λsrcrs: list register.
+  λstart_lbl: label.
+  λdest_lbl: label.
+  λdef: rtl_internal_function globals.
+  λprf: |destrs| = |srcrs|. (* assert in caml code *)
+  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
+  let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in
+  let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in
+  let insts_init ≝ [
+    sequential … (SET_CARRY …);
+    sequential … (INT rtl_params_ globals tmpr (zero ?))
+  ] in
+  let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in
+  let insts_add ≝ map … f_add destrs in
+    adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
+
+definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
+  λglobals: list ident.
+  λdestrs: list register.
+  λsrcrs: list register.
+  λstart_lbl: label.
+  λdest_lbl: label.
+  λdef: rtl_internal_function globals.
+  match destrs with
+  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def
+  | cons destr destrs ⇒
+    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
+    let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in
+    let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in
+    let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in
+    let f ≝ λtmp_srcr. [
+      sequential … (CLEAR_CARRY rtl_params_ globals);
+      sequential … (INT rtl_params_ globals tmpr (zero ?));
+      sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);
+      sequential … (INT rtl_params_ globals tmpr (zero ?));
+      sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);
+      sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)
+    ] in
+    let insts ≝ init_destr :: (flatten … (map … f tmp_srcrs)) in
+    let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
+      add_translates rtl_params1 globals [
+        save_srcrs; adds_graph rtl_params1 globals insts; epilogue
+      ] start_lbl dest_lbl def
+  ].
+
+(* 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
+   instead infer the size of the cast's destination from the context.  Is
+   this correct?
+*)
+definition translate_op1 ≝
+  λglobals: list ident.
+  λop1: unary_operation.
+  λdestrs: list register.
+  λsrcrs: list register.
+  λprf: |destrs| = |srcrs|.
+  λstart_lbl: label.
+  λdest_lbl: label.
+  λ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 globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
+  | Onegint ⇒
+      translate_negint globals destrs srcrs start_lbl dest_lbl def prf
+  | Onotbool ⇒
+      translate_notbool globals destrs srcrs start_lbl dest_lbl def
+  | Onotint ⇒
+    let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
+    let l ≝ map2 … f destrs srcrs prf in
+      adds_graph rtl_params1 globals l start_lbl dest_lbl def
+  | Optrofint r ⇒
+      translate_move globals destrs srcrs start_lbl dest_lbl def
+  | Ointofptr r ⇒
+      translate_move globals destrs srcrs start_lbl dest_lbl def
+  | Oid ⇒
+      translate_move globals destrs srcrs start_lbl dest_lbl def
+  | _ ⇒ ? (* float operations implemented in runtime *)
+  ].
+  cases not_implemented
 qed.
 
@@ -512 +516 @@
   λdummy_lbl: label.
   λi: nat.
-  λi_prf.
+  λi_prf: i ≤ |tmp_destrs|.
   λtranslates: list ?.
   λsrcr2i: register.
@@ -535 +539 @@
     translates @ tmp_destrs2'.
 
-axiom translate_mul:
-  ∀globals: list ident.
-  ∀destrs: list register.
-  ∀srcrs1: list register.
-  ∀srcrs2: list register.
-  ∀start_lbl: label.
-  ∀dest_lbl: label.
-  ∀def: rtl_internal_function globals.
-    rtl_internal_function globals.
-
 (*
 definition translate_mul ≝
@@ -569 +563 @@
     add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
 *)
+
+axiom translate_mul:
+  ∀globals: list ident.
+  ∀destrs: list register.
+  ∀srcrs1: list register.
+  ∀srcrs2: list register.
+  ∀start_lbl: label.
+  ∀dest_lbl: label.
+  ∀def: rtl_internal_function globals.
+    rtl_internal_function globals.
 
 definition translate_divumodu8 ≝