Changeset 1293 for src/RTLabs

Timestamp:

Oct 5, 2011, 2:47:19 PM (9 years ago)

Author:

mulligan

Message:

finished rtl abs to rtl transformation subject to closing some axioms that hopefully can be closed by establishing just what is happening in translate_op

File:

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

src/RTLabs/RTLAbstoRTL.ma

@@ -13 +13 @@
      let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
       〈r::res,runiverse〉 ].
-
-definition choose_rest ≝
-  λA: Type[0].
-  λleft, right: list A.
-  λprfl: 0 < |left|.
-  λprfr: 0 < |right|.
-  match left return λx. 0 < |x| → list A with
-  [ nil ⇒ λnil_prf.
-    match right return λx. 0 < |x| → list A with
-    [ nil ⇒ λnil_nil_absrd. ?
-    | _ ⇒ λnil_cons_prf. right
-    ] prfr
-  | _ ⇒ λcons_prf. right
-  ] prfl.
-  normalize in nil_prf;
-  cases(not_le_Sn_O 0)
-  #HYP
-  cases(HYP nil_prf)
-qed.
 
 definition complete_regs ≝
@@ -377 +358 @@
     let srcrsl_rest ≝ \snd (\fst reduced) in
     let srcrsr_rest ≝ \snd (\snd reduced) in
-    let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in
+    let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in
     match reduce_strong register register destrs srcrsl_common with
     [ dp reduced second_reduced_proof ⇒
@@ -577 +558 @@
       let restl ≝ \snd (\snd crl) in
       let restr ≝ \snd (\snd crl) in
-      let rest ≝ choose_rest ? restl restr ? ? in
+      let rest ≝ restl @ restr in
       let inits ≝ [
         sequential … (INT rtl_params_ globals destr (zero …));
@@ -604 +585 @@
     ]
   ].
-  [1: @their_proof
-  |*: cases not_implemented (* choose rest requires non-emptiness proofs but
-                               these appear impossible to obtain, similar proof
-                               to above *)
-  ]
+  @their_proof
 qed.
 
@@ -1032 +1009 @@
 qed.
 
+axiom fake_label: label.
+
+(* XXX: following conversation with CSC about the mix up in extension statements
+        and extension instructions in RTL *)
 definition translate_stmt ≝
   λglobals: list ident.
@@ -1040 +1021 @@
   match stmt with
   [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
-  | St_cost cost_lbl lbl' ⇒ add_graph lbl (sequential rtl_params_ globals (COST_LABEL … cost_lbl lbl')) def
+  | St_cost cost_lbl lbl' ⇒ add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (COST_LABEL rtl_params_ globals cost_lbl) lbl') def
   | St_const destr cst lbl' ⇒
-    translate_cst cst (find_local_env destr lenv) lbl lbl' def
+    translate_cst globals cst (find_local_env destr lenv) lbl lbl' def
   | St_op1 op1 destr srcr lbl' ⇒
-    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
+    translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
   | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
-    translate_op2 op2 (find_local_env destr lenv) … (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
+    translate_op2 globals op2 (find_local_env destr lenv) … (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
   | St_load ignore addr destr lbl' ⇒
-    translate_load (find_local_env addr lenv) … (find_local_env destr lenv) lbl lbl' def
+    translate_load globals (find_local_env addr lenv) … (find_local_env destr lenv) lbl lbl' def
   | St_store ignore addr srcr lbl' ⇒
-    translate_store (find_local_env addr lenv) … (find_local_env srcr lenv) lbl lbl' def
+    translate_store globals (find_local_env addr lenv) … (find_local_env srcr lenv) lbl lbl' def
   | St_call_id f args retr lbl' ⇒
     match retr with
     [ Some retr ⇒
-      add_graph rtl_params1 globals lbl (sequential … (CALL_ID … f (rtl_args args lenv) (find_local_env retr lenv) lbl')) def
-    | None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID … f (rtl_args args lenv) [ ] lbl')) def
+      add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) (find_local_env retr lenv)) lbl') def
+    | None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) [ ]) lbl') def
     ]
   | St_call_ptr f args retr lbl' ⇒
@@ -1061 +1042 @@
     [ None ⇒
       let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
-        add_graph lbl rtl_params1 globals (sequential … (extension … (rtl_st_ext_call_ptr … f1 f2 (rtl_args args lenv) [ ] lbl'))) def
+        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])) lbl') def
     | Some retr ⇒
       let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
-        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl'))) def
+        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv))) lbl') def
     ]
   | St_tailcall_id f args ⇒
-    add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) lbl) def
+    add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) fake_label) def
   | St_tailcall_ptr f args ⇒
     let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
-      add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params1 globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) lbl) def
+      add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params1 globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) fake_label) def
   | St_cond r lbl_true lbl_false ⇒
     translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def
@@ -1086 +1067 @@
    skip instructions at these nodes. *)
 definition translate_internal ≝
-  λglobals,def.
+  λglobals: list ident.
+  λdef.
   let runiverse ≝ f_reggen def in
   let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
@@ -1108 +1090 @@
   let entry' ≝ f_entry def in
   let exit' ≝ f_exit def in
-  let graph' ≝ add … (empty_map ? ?) entry' (GOTO … entry') in
-  let graph' ≝ add … graph' exit' (GOTO … exit') in
+  let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params_ globals entry') in
+  let graph' ≝ add LabelTag ? graph' exit' (GOTO rtl_params_ globals exit') in
   let res ≝
     mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
      locals' stack_size' graph' ? ? in
-    foldi … (translate_stmt … lenv) (f_graph def) res.
+    foldi … (translate_stmt globals … lenv) (f_graph def) res.
 [ % [@entry' | @graph_add_lookup @graph_add]
 | % [@exit'  | @graph_add]]
@@ -1120 +1102 @@
 (*CSC: here we are not doing any alignment on variables, like it is done in OCaml
   because of CompCert heritage *)
-definition rtlabs_to_rtl : RTLabs_program → rtl_program ≝
- λp. transform_program ??? p (transf_fundef … (translate_internal (prog_var_names …))).
+definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝
+ λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).