Changeset 2674 for src/ERTLptr


Ignore:
Timestamp:
Feb 18, 2013, 5:48:19 PM (8 years ago)
Author:
tranquil
Message:
  • another change in block definition
  • RTLabs -> RTL and ERTL -> ERTLptr passes fixed, others stil broken
Location:
src/ERTLptr
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptr.ma

    r2645 r2674  
    2020    (* call_dest ≝ *) unit
    2121    (* ext_seq ≝ *) ertlptr_seq
    22     (* ext_seq_labels ≝ *) (λ_.[])
     22    (* ext_seq_labels ≝ *)
     23      (λs.match s with [ LOW_ADDRESS _ l ⇒ [l] | HIGH_ADDRESS _ l ⇒ [l] | _ ⇒ [ ]])
    2324    (* has_tailcall ≝ *) false
    2425    (* paramsT ≝ *) ℕ.
  • src/ERTLptr/ERTLtoERTLptr.ma

    r2604 r2674  
    3535|STORE arg1 arg2 reg ⇒ STORE ERTLptr … arg1 arg2 reg
    3636|extension_seq s ⇒ extension_seq ERTLptr … (ertlptr_ertl s)
    37 ]. 
     37].
    3838
    39 
    40 (* PAOLO: implement the b_graph_translate2 that expects functions that
    41    return not (list instr * instr) but (list (label → instr) * instr) *)
    4239definition translate_step:
    4340 ∀globals.
     
    4845match s return λ_.bind_step_block ERTLptr globals with
    4946[ CALL called args dest ⇒
    50     match called with
    51     [inl id ⇒ bret … [CALL ERTLptr ? (inl … id) args dest]
    52     |inr dest1 ⇒ νreg in bret … «[λl.(extension_seq ERTLptr ? (LOW_ADDRESS reg l) : joint_step ??);
    53                                   λ_.PUSH ERTLptr … (Reg … reg);
    54                                   λl.extension_seq ERTLptr ? (HIGH_ADDRESS reg l);
    55                                   λ_.PUSH ERTLptr … (Reg … reg) ;
    56                                   λ_.CALL ERTLptr ? (inr … dest1) args dest], ?»
     47    match called return λ_.bind_step_block ERTLptr globals with
     48    [inl id ⇒ bret … 〈[ ], λ_.CALL ERTLptr ? (inl … id) args dest, [ ]〉
     49    |inr dest1 ⇒ νreg in bret ? (step_block ERTLptr globals)
     50      〈[λl.(LOW_ADDRESS reg l : joint_seq ??);
     51        λ_.PUSH ERTLptr … (Reg … reg);
     52        λl.HIGH_ADDRESS reg l;
     53        λ_.PUSH ERTLptr … (Reg … reg)],
     54        λ_.CALL ERTLptr ? (inr … dest1) args dest, [ ]〉
    5755    ]
    58 | COND reg l ⇒ bret … [COND ERTLptr ? reg l]
     56| COND reg l ⇒ bret … 〈[ ], λ_.COND ERTLptr ? reg l, [ ]〉
    5957| step_seq x ⇒ bret … [seq_embed … x]
    60 ]. @I qed.
     58].
    6159
    6260definition fin_step_embed: joint_fin_step ERTL → joint_fin_step ERTLptr ≝
     
    8078  λglobals,int_fun.
    8179  (* initialize internal function *)
    82   let init ≝ init_graph_if ERTLptr globals
    83     (joint_if_luniverse … int_fun)
    84     (joint_if_runiverse … int_fun)
     80  b_graph_translate ERTL ERTLptr globals
    8581    (joint_if_result … int_fun)
    8682    (joint_if_params … int_fun)
    8783    (joint_if_stacksize … int_fun)
    88     (joint_if_entry … int_fun) in
    89   b_graph_translate …
    90     init
    9184    (translate_step …)
    9285    (translate_fin_step …)
Note: See TracChangeset for help on using the changeset viewer.