Changeset 2162


Ignore:
Timestamp:
Jul 6, 2012, 5:53:01 PM (5 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:
3 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r2155 r2162  
    743743      λr. tmpr ← tmpr .Or. r in
    744744    bret … 〈MOVE rtl_params globals 〈tmpr,srcr〉 ::
    745     map ?? f srcrs', (COND ? tmpr lbl_true : joint_step ??) 〉
     745    map ?? f srcrs', (COND tmpr lbl_true : joint_step ??) 〉
    746746  ].
    747747
     
    815815    ❬(match retr with
    816816      [ Some retr ⇒
    817         CALL_ID rtl_params f (rtl_args args lenv ?) (find_local_env retr lenv ?)
     817        CALL_ID rtl_params ? f (rtl_args args lenv ?) (find_local_env retr lenv ?)
    818818      | None ⇒
    819         CALL_ID rtl_params f (rtl_args args lenv ?) [ ]
     819        CALL_ID rtl_params ? f (rtl_args args lenv ?) [ ]
    820820      ] : bind_seq_block ???), lbl'❭
    821821  | St_call_ptr f args retr lbl' ⇒
  • src/joint/Joint_paolo.ma

    r2155 r2162  
    7878  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
    7979  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
    80   | extension_seq : ext_seq p → joint_seq p globals.
     80  | CALL_ID: ident → call_args p → call_dest p → joint_seq p globals
     81  | extension_seq : ext_seq p → joint_seq p globals
     82  | extension_call : ext_call p → joint_seq p globals.
    8183
    8284axiom EmptyString : String.
     
    9698interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
    9799
    98 coercion extension_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
     100coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
    99101  extension_seq on _s : ext_seq ? to joint_seq ??.
    100 
    101 inductive joint_call (p : step_params) : Type[0] ≝
    102   | CALL_ID: ident → call_args p → call_dest p → joint_call p
    103   | extension_call : ext_call p → joint_call p.
    104 
    105 coercion extension_to_call : ∀p.∀s : ext_call p.joint_call p ≝
    106   extension_call on _s : ext_call ? to joint_call ?.
     102coercion extension_call_to_seq : ∀p,globals.∀s : ext_call p.joint_seq p globals ≝
     103  extension_call on _s : ext_call ? to joint_seq ??.
    107104 
    108 inductive joint_branch (p : step_params) : Type[0] ≝
     105(* inductive joint_branch (p : step_params) : Type[0] ≝
    109106  | COND: acc_a_reg p → label → joint_branch p
    110   (*| extension_branch : ext_branch p → joint_branch p*).
     107  | extension_branch : ext_branch p → joint_branch p.*)
    111108
    112109(*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝
     
    115112inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝
    116113  | step_seq : joint_seq p globals → joint_step p globals
    117   | step_call : joint_call p → joint_step p globals
    118   | step_branch : joint_branch p → joint_step p globals.
     114  | COND: acc_a_reg p → label → joint_step p globals.
    119115
    120116coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
    121117  step_seq on _s : joint_seq ?? to joint_step ??.
    122 coercion call_to_step : ∀p,globals.∀s : joint_call p.joint_step p globals ≝
    123   step_call on _s : joint_call ? to joint_step ??.
    124 coercion branch_to_step : ∀p,globals.∀s : joint_branch p.joint_step p globals ≝
    125   step_branch on _s : joint_branch ? to joint_step ??.
    126118
    127119definition step_flows ≝ λp,globals.λs : joint_step p globals.
    128120  match s with
    129   [ step_seq _ ⇒ Labels … [ ]
    130   | step_call _ ⇒ Call
    131   | step_branch s ⇒
     121  [ step_seq s ⇒
    132122    match s with
    133     [ COND _ l ⇒ Labels … [l]
    134     (*| extension_branch s' ⇒ Labels … (ext_branch_labels … s')*)
     123    [ CALL_ID _ _ _ ⇒ Call
     124    | extension_call _ ⇒ Call
     125    | _ ⇒ Labels … [ ]
    135126    ]
     127  | COND _ l ⇒ Labels … [l]
    136128  ].
    137129
     
    151143    joint_step p globals → status_class ≝ λp,g,s.
    152144  match s with
    153   [ step_seq _ ⇒ cl_other
    154   | step_call _ ⇒ cl_call
    155   | step_branch _ ⇒ cl_jump
     145  [ step_seq s ⇒
     146    match s with
     147    [ CALL_ID _ _ _ ⇒ cl_call
     148    | extension_call _ ⇒ cl_call
     149    | _ ⇒ cl_other
     150    ]
     151  | COND _ _ ⇒ cl_jump
    156152  ].
    157153
  • src/joint/TranslateUtils_paolo.ma

    r2155 r2162  
    3939  (globals: list ident)
    4040  (insts: list (joint_seq g_pars globals))
    41   (src : label)
    42   (def: joint_internal_function … g_pars) on insts
    43   : (joint_internal_function … g_pars) × label ≝
     41  (src : label) on insts : state_monad (joint_internal_function … g_pars) label ≝
    4442  match insts with
    45   [ nil ⇒ 〈def, src〉
     43  [ nil ⇒ return src
    4644  | cons instr others ⇒
    47     let 〈def, mid〉 ≝ fresh_label … def in
    48     let def ≝ add_graph … src (sequential … instr mid) def in
    49     adds_graph_list g_pars globals others mid def
     45    ! mid ← fresh_label … ;
     46    ! def ← state_get … ;
     47    !_ state_set … (add_graph … src (sequential … instr mid) def) ;
     48    adds_graph_list g_pars globals others mid
    5049  ].
    5150
     
    6665    add_graph … mid (final … (\snd b)) def
    6766  ].
     67
     68(* preserves first statement if a cost label (should be an invariant) *)
     69definition insert_prologue ≝
     70  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
     71  λdef : joint_internal_function globals g_pars.
     72  let entry ≝ joint_if_entry … def in
     73  match stmt_at … entry
     74  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
     75  with
     76  [ Some s ⇒ λ_.
     77    match s with
     78    [ sequential s' next ⇒
     79      match s' with
     80      [ step_seq s'' ⇒
     81        match s'' with
     82        [ COST_LABEL _ ⇒
     83          adds_graph ?? (inl … (s'' :: insts)) entry next def
     84        | _ ⇒
     85          let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     86          add_graph … tmp s def'
     87        ]
     88      | _ ⇒
     89        let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     90        add_graph … tmp s def'
     91      ]
     92    | _ ⇒
     93      let 〈def', tmp〉 ≝ adds_graph_list ?? insts entry def in
     94      add_graph … tmp s def'
     95    ]
     96  | None ⇒ Ⓧ
     97  ] (pi2 … entry).
     98
     99definition insert_epilogue ≝
     100  λg_pars:graph_params.λglobals.λinsts : list (joint_seq g_pars globals).
     101  λdef : joint_internal_function globals g_pars.
     102  let exit ≝ joint_if_exit … def in
     103  match stmt_at … exit
     104  return λx.match x with [None ⇒ false | Some _ ⇒ true] → ?
     105  with
     106  [ Some s ⇒ λ_.
     107    let 〈def', tmp〉 as prf ≝ adds_graph_list ?? insts exit def in
     108    let def'' ≝ add_graph … tmp s def' in
     109    set_joint_code … def'' (joint_if_code … def'') (joint_if_entry … def'') tmp
     110  | None ⇒ Ⓧ
     111  ] (pi2 … exit).
     112whd in match def''; >graph_code_has_point //
     113qed.
    68114
    69115definition b_adds_graph :
Note: See TracChangeset for help on using the changeset viewer.