Changeset 1275 for src/RTL/RTLtoERTL.ma

Timestamp:

Sep 26, 2011, 6:07:47 PM (10 years ago)

Author:

sacerdot

Message:

RTL ported to joint syntax, but:

1. bug discovered: opaccs should have taken four registers
2. push/pop should not be present in RTL :-(

ERTLToLTL and RTLtoERTL not working ATM

File:

• src/RTL/RTLtoERTL.ma (modified) (4 diffs)

src/RTL/RTLtoERTL.ma

@@ -369 +369 @@
     ) start_lbl dest_lbl def.
 
-axiom translate_stmt :
- ∀globals: list ident. label → rtl_statement globals → ertl_internal_function globals → ertl_internal_function globals.
-(*
+definition translate_stmt :
+ ∀globals: list ident. label → rtl_statement globals → ertl_internal_function globals → ertl_internal_function globals
  ≝
   λglobals.
@@ -378 +377 @@
   λdef.
   match stmt with
-  [ rtl_st_skip lbl' ⇒ add_graph … lbl (ertl_st_skip lbl') def
-  | rtl_st_cost cost_lbl lbl' ⇒ add_graph … lbl (ertl_st_cost cost_lbl lbl') def
-  | rtl_st_addr r1 r2 x lbl' ⇒ add_graph … lbl (ertl_st_addr r1 r2 x lbl') def
-  | rtl_st_stack_addr r1 r2 lbl' ⇒
-    adds_graph … [
-      ertl_st_get_hdw r1 RegisterSPL lbl;
-      ertl_st_get_hdw r2 RegisterSPH lbl
-    ] lbl lbl' def
-  | rtl_st_int r i lbl' ⇒  add_graph … lbl (ertl_st_int r i lbl') def
-  | rtl_st_move r1 r2 lbl' ⇒ add_graph … lbl (ertl_st_move r1 r2 lbl') def
-  | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
-      add_graph … lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def
-  | rtl_st_op1 op1 destr srcr lbl' ⇒
-    add_graph … lbl (ertl_st_op1 op1 destr srcr lbl') def
-  | rtl_st_op2 op2 destr srcr1 srcr2 lbl' ⇒
-    add_graph … lbl (ertl_st_op2 op2 destr srcr1 srcr2 lbl') def
-  | rtl_st_clear_carry lbl' ⇒
-    add_graph … lbl (ertl_st_clear_carry lbl') def
-  | rtl_st_set_carry lbl' ⇒
-    add_graph … lbl (ertl_st_set_carry lbl') def
-  | rtl_st_load destr addr1 addr2 lbl' ⇒
-    add_graph … lbl (ertl_st_load destr addr1 addr2 lbl') def
-  | rtl_st_store addr1 addr2 srcr lbl' ⇒
-    add_graph … lbl (ertl_st_store addr1 addr2 srcr lbl') def
-  | rtl_st_call_id f args ret_regs lbl' ⇒
-    translate_call_id … f args ret_regs lbl lbl' def
-  | rtl_st_cond srcr lbl_true lbl_false ⇒
-    add_graph … lbl (ertl_st_cond srcr lbl_true lbl_false) def
-  | rtl_st_return ⇒
-    add_graph … lbl ertl_st_return def
-  | _ ⇒ ? (* assert false: not implemented or should not happen *)
-  ].
+  [ joint_st_goto lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
+  | joint_st_return ⇒ add_graph … lbl (joint_st_return …) def
+  | joint_st_sequential seq lbl' ⇒
+     match seq with
+      [ joint_instr_call_id f args ret_regs ⇒
+         translate_call_id … f args ret_regs lbl lbl' def
+      | joint_instr_move rs ⇒
+         let 〈r1,r2〉 ≝ rs in
+         let rs ≝ 〈pseudo r1, pseudo r2〉 in
+          add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_move … rs) lbl') def
+      | joint_instr_extension ext ⇒
+         match ext with
+          [ rtl_st_ext_call_ptr _ _ _ _ ⇒ ? (*CSC: XXXX not implemented in OCaml too *)
+          | rtl_st_ext_address r1 r2 ⇒
+             adds_graph … [
+              joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl;
+              joint_st_sequential … (joint_instr_move … 〈pseudo r2, hardware RegisterSPH〉) lbl
+             ] lbl lbl' def
+          (*| _ ⇒ ? (* assert false: not implemented or should not happen *)*)
+          ]
+      (*CSC: everything is just copied to re-type it from now on;
+        the problem is call_id that takes different parameters, but that is pattern-matched
+        above. It could be made nicer at the cost of making all the rest of the code uglier *)
+      | joint_instr_cost_label cost_lbl ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cost_label … cost_lbl) lbl') def
+      | joint_instr_address x prf r1 r2 ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_address … x prf r1 r2) lbl') def
+      | joint_instr_int r i ⇒  add_graph … lbl (joint_st_sequential ertl_params_ globals (joint_instr_int … r i) lbl') def
+      | joint_instr_opaccs op destr1 destr2 srcr1 srcr2 ⇒
+          add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def
+      | joint_instr_op1 op1 destr srcr ⇒
+        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op1 … op1 destr srcr) lbl') def
+      | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
+        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def
+      | joint_instr_clear_carry ⇒
+        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_clear_carry …) lbl') def
+      | joint_instr_set_carry ⇒
+        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_set_carry …) lbl') def
+      | joint_instr_load destr addr1 addr2 ⇒
+        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_load … destr addr1 addr2) lbl') def
+      | joint_instr_store addr1 addr2 srcr ⇒
+        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_store … addr1 addr2 srcr) lbl') def
+      | joint_instr_cond srcr lbl_true ⇒
+        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cond … srcr lbl_true) lbl') def
+      | joint_instr_comment msg ⇒
+        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_comment … msg) lbl') def
+      | joint_instr_push _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
+      | joint_instr_pop _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
+      ]].
   cases not_implemented
-qed.*)  
+qed.
 
 (* hack with empty graphs used here *)
@@ -429 +443 @@
       graph' ? ? in
   let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
-  let def' ≝ add_pro_and_epilogue … (joint_if_params … def) (joint_if_result … def) def' in
-    def'.
+   add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
 whd in match ertl_params (* CSC: Matita's bug here; not enough/too much reduction
                                  makes the next application fail. Why? *)    
@@ -485 +498 @@
 definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
 
-(*
-definition move_first_cost_label_up ≝
-  λglobals.
-  λA: Type[0].
-  λid_def: A × ?.
-  let 〈id, def〉 ≝ id_def in
-  let def' ≝
-    match def with
-    [ Internal int_fun ⇒ Internal ? (move_first_cost_label_up_internal … (translate_funct_internal globals int_fun))
-    | External ext ⇒ External … ext
-    ]
-  in
-    〈id, def'〉.
-
-definition translate ≝
-  λp.
-  let p ≝ tailcall_simplify p in (* tailcall simplification here *)
-  let f ≝ λfunct. move_first_cost_label_up ? funct in
-  let vars ≝ map ? ? f (rtl_pr_functs p) in
-    mk_ertl_program (rtl_pr_vars p) vars (rtl_pr_main p).
-*)
-
 definition translate : rtl_program → ertl_program ≝
  λp.
   let p ≝ tailcall_simplify p in (* tailcall simplification here *)
-    transform_program ??? p (transf_fundef ?? translate_funct).
+    transform_program ??? p (transf_fundef ?? (translate_funct …)).