Changeset 2162

Timestamp:

Jul 6, 2012, 5:53:01 PM (7 years ago)

Author:

tranquil

Message:

• yet another correction to joint
• added functions adding prologues and epilogues in TranslateUtils?. Adding a prologue will preserve the invariant of having a cost label at the start of the function, without needing transformations later
• redefined ERTL and rewritten RTLToERTL (with suffix "_paolo")

Location:

src

Files:

• ERTL/ERTL_paolo.ma (added)
• RTL/RTLTailcall_paolo.ma (added)
• RTL/RTLToERTL_paolo.ma (added)
• RTLabs/RTLabsToRTL_paolo.ma (modified) (2 diffs)
• joint/Joint_paolo.ma (modified) (4 diffs)
• joint/TranslateUtils_paolo.ma (modified) (2 diffs)

src/RTLabs/RTLabsToRTL_paolo.ma

@@ -743 +743 @@
       λr. tmpr ← tmpr .Or. r in 
     bret … 〈MOVE rtl_params globals 〈tmpr,srcr〉 ::
-    map ?? f srcrs', (COND ? tmpr lbl_true : joint_step ??) 〉
+    map ?? f srcrs', (COND … tmpr lbl_true : joint_step ??) 〉
   ].
 
@@ -815 +815 @@
     ❬(match retr with
       [ Some retr ⇒
-        CALL_ID rtl_params f (rtl_args args lenv ?) (find_local_env retr lenv ?)
+        CALL_ID rtl_params ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
       | None ⇒
-        CALL_ID rtl_params f (rtl_args args lenv ?) [ ]
+        CALL_ID rtl_params ? f (rtl_args args lenv ?) [ ]
       ] : bind_seq_block ???), lbl'❭
   | St_call_ptr f args retr lbl' ⇒

src/joint/Joint_paolo.ma

@@ -78 +78 @@
   | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
   | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
-  | extension_seq : ext_seq p → joint_seq p globals.
+  | CALL_ID: ident → call_args p → call_dest p → joint_seq p globals
+  | extension_seq : ext_seq p → joint_seq p globals
+  | extension_call : ext_call p → joint_seq p globals.
 
 axiom EmptyString : String.
@@ -96 +98 @@
 interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
 
-coercion extension_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
+coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
   extension_seq on _s : ext_seq ? to joint_seq ??.
-
-inductive joint_call (p : step_params) : Type[0] ≝
-  | CALL_ID: ident → call_args p → call_dest p → joint_call p
-  | extension_call : ext_call p → joint_call p.
-
-coercion extension_to_call : ∀p.∀s : ext_call p.joint_call p ≝
-  extension_call on _s : ext_call ? to joint_call ?.
+coercion extension_call_to_seq : ∀p,globals.∀s : ext_call p.joint_seq p globals ≝
+  extension_call on _s : ext_call ? to joint_seq ??.
   
-inductive joint_branch (p : step_params) : Type[0] ≝
+(* inductive joint_branch (p : step_params) : Type[0] ≝
   | COND: acc_a_reg p → label → joint_branch p
-  (*| extension_branch : ext_branch p → joint_branch p*).
+  | extension_branch : ext_branch p → joint_branch p.*)
 
 (*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝
@@ -115 +112 @@
 inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝
   | step_seq : joint_seq p globals → joint_step p globals
-  | step_call : joint_call p → joint_step p globals
-  | step_branch : joint_branch p → joint_step p globals.
+  | COND: acc_a_reg p → label → joint_step p globals.
 
 coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
   step_seq on _s : joint_seq ?? to joint_step ??.
-coercion call_to_step : ∀p,globals.∀s : joint_call p.joint_step p globals ≝
-  step_call on _s : joint_call ? to joint_step ??.
-coercion branch_to_step : ∀p,globals.∀s : joint_branch p.joint_step p globals ≝
-  step_branch on _s : joint_branch ? to joint_step ??.
 
 definition step_flows ≝ λp,globals.λs : joint_step p globals.
   match s with
-  [ step_seq _ ⇒ Labels … [ ]
-  | step_call _ ⇒ Call
-  | step_branch s ⇒
+  [ step_seq s ⇒
     match s with
-    [ COND _ l ⇒ Labels … [l]
-    (*| extension_branch s' ⇒ Labels … (ext_branch_labels … s')*)
+    [ CALL_ID _ _ _ ⇒ Call
+    | extension_call _ ⇒ Call
+    | _ ⇒ Labels … [ ]
     ]
+  | COND _ l ⇒ Labels … [l]
   ].
 
@@ -151 +143 @@
     joint_step p globals → status_class ≝ λp,g,s.
   match s with
-  [ step_seq _ ⇒ cl_other
-  | step_call _ ⇒ cl_call
-  | step_branch _ ⇒ cl_jump
+  [ step_seq s ⇒
+    match s with
+    [ CALL_ID _ _ _ ⇒ cl_call
+    | extension_call _ ⇒ cl_call
+    | _ ⇒ cl_other
+    ]
+  | COND _ _ ⇒ cl_jump
   ].
 

src/joint/TranslateUtils_paolo.ma

@@ -39 +39 @@
   (globals: list ident)
   (insts: list (joint_seq g_pars globals))
-  (src : label)
-  (def: joint_internal_function … g_pars) on insts 
-  : (joint_internal_function … g_pars) × label ≝
+  (src : label) on insts : state_monad (joint_internal_function … g_pars) label ≝
   match insts with
-  [ nil ⇒ 〈def, src〉
+  [ nil ⇒ return src
   | cons instr others ⇒
-    let 〈def, mid〉 ≝ fresh_label … def in
-    let def ≝ add_graph … src (sequential … instr mid) def in
-    adds_graph_list g_pars globals others mid def
+    ! mid ← fresh_label … ;
+    ! def ← state_get … ;
+    !_ state_set … (add_graph … src (sequential … instr mid) def) ;
+    adds_graph_list g_pars globals others mid
   ].
 
@@ -66 +65 @@
     add_graph … mid (final … (\snd b)) def
   ].
+
+(* preserves first statement if a cost label (should be an invariant) *)
+definition insert_prologue ≝
+  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
+  λdef : joint_internal_function globals g_pars.
+  let entry ≝ joint_if_entry … def in
+  match stmt_at … entry
+  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
+  with
+  [ Some s ⇒ λ_.
+    match s with
+    [ sequential s' next ⇒
+      match s' with
+      [ step_seq s'' ⇒
+        match s'' with
+        [ COST_LABEL _ ⇒
+          adds_graph ?? (inl … (s'' :: insts)) entry next def
+        | _ ⇒
+          let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
+          add_graph … tmp s def'
+        ]
+      | _ ⇒
+        let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
+        add_graph … tmp s def'
+      ]
+    | _ ⇒
+      let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
+      add_graph … tmp s def'
+    ]
+  | None ⇒ Ⓧ
+  ] (pi2 … entry).
+
+definition insert_epilogue ≝
+  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
+  λdef : joint_internal_function globals g_pars.
+  let exit ≝ joint_if_exit … def in
+  match stmt_at … exit
+  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
+  with
+  [ Some s ⇒ λ_.
+    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
+    let def'' ≝ add_graph … tmp s def' in
+    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
+  | None ⇒ Ⓧ
+  ] (pi2 … exit).
+whd in match def''; >graph_code_has_point //
+qed.
 
 definition b_adds_graph :