Changeset 1059 for src/RTLabs

Timestamp:

Jul 6, 2011, 6:09:39 PM (8 years ago)

Author:

mulligan

Message:

work from today, bit of a mess at the moment

File:

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

src/RTLabs/RTLAbstoRTL.ma

@@ -4 +4 @@
 include "common/Graphs.ma".
 include "common/Maps.ma".
-include "common/IntValue.ma".
+(* include "common/IntValue.ma". *)
+include "common/FrontEndOps.ma".
 
 definition add_graph ≝
@@ -280 +281 @@
     rtl_st_int r i dest_lbl.
 
-definition translate_cst ≝
-  λcst.
-  λdestrs.
-  λstart_lbl.
-  λdest_lbl.
-  λdef.
-  match cst with
-  [ cast_int i ⇒
-    match destrs with
-    [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
-    | _ ⇒
-      (* this case needs changing when Z is added to stdlib as we are using
-         nats instead of ints here! *)
-      let size ≝ length ? destrs in
-      let is ≝ map … (to_int size) (break size (of_int size (nat_of_bitvector ? i)) size) in
-      let is' ≝ map … (bitvector_of_nat ?) is in
-      let l ≝ map2 … (translate_cst_int_internal dest_lbl) destrs is' ? in
-        adds_graph l start_lbl dest_lbl def
-    ]
-  | cast_addrsymbol id ⇒
-    let 〈r1, r2〉 ≝ make_addr ? destrs ? in
-      add_graph start_lbl (rtl_st_addr r1 r2 id dest_lbl) def
-  | _ ⇒ ?
-  ].
-  | cast_addrsymbol id ⇒
-    match destrs with
-    [ nil ⇒ None ?
-    | cons hd tl ⇒
-      match tl with
-      [ nil ⇒ None ?
-      | cons hd' tl' ⇒
-        Some ? (add_graph start_lbl (rtl_st_addr hd hd' id dest_lbl) def)
-      ]
-    ]
-  | cast_offset off ⇒
-    match destrs with
-    [ nil ⇒ None ?
-    | cons hd tl ⇒
-      match tl with
-      [ nil ⇒ None ?
-      | cons hd' tl' ⇒
-        let 〈def, tmpr〉 ≝ fresh_reg def in
-        adds_graph [
-          rtl_st_stack_addr hd hd' start_lbl;
-          rtl_st_int tmpr off start_lbl;
-          rtl_st_op2 Add hd hd tmpr start_lbl;
-          rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl;
-          rtl_st_op2 Addc hd' hd' tmpr start_lbl
-        ] start_lbl dest_lbl def
-      ]
-    ]
-  | cast_stack ⇒ ?
-  | cast_sizeof size ⇒ ?
-  (* | cast_float f ⇒ None ? *) (* what are we doing with floats? *)
-  ].
-
-let rec translate_cst cst destrs start_lbl dest_lbl def = match cst with
-
-  | AST.Cst_stack ->
-    let (r1, r2) = make_addr destrs in
-    add_graph start_lbl (RTL.St_stackaddr (r1, r2, dest_lbl)) def
-
-  | AST.Cst_offset off ->
-    let i = concrete_offset off in
-    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
-
-  | AST.Cst_sizeof size ->
-    let i = concrete_size size in
-    translate_cst (AST.Cst_int i) destrs start_lbl dest_lbl def
+axiom translate_cst:
+  ∀cst: constant.
+  ∀destrs: list register.
+  ∀start_lbl: label.
+  ∀dest_lbl: label.
+  ∀def: rtl_internal_function.
+    rtl_internal_function.
+
+definition translate_move_internal ≝
+  λstart_lbl: label.
+  λdestr: register.
+  λsrcr: register.
+    rtl_st_move destr srcr start_lbl.
+
+definition translate_move ≝
+  λdestrs: list register.
+  λsrcrs: list register.
+  λstart_lbl: label.
+  λ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
 
 definition filter_and_to_list_local_env_internal ≝