Changeset 1412 for src/RTL


Ignore:
Timestamp:
Oct 19, 2011, 2:22:31 PM (8 years ago)
Author:
sacerdot
Message:

Tailcalls (via ids or pointers) to internal functions implemented.
Tailcalls to external function left as a daemon.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1411 r1412  
    6969           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    7070
    71 definition rtl_save_frame:
    72  address → nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
    73  λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st.
     71definition rtl_call_function:
     72 nat → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     73  λstacksize,formal_arg_regs,actual_arg_regs,st.
    7474  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
    7575  do new_regs ←
     
    8080    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
    8181  OK …
    82    (set_frms rtl_sem_params
    83     (mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st))
    84      (set_regs rtl_sem_params new_regs
    85       (set_m … mem
    86        (set_sp … (mk_pointer XData b ? (mk_offset 0)) st)))).
     82   (set_regs rtl_sem_params new_regs
     83    (set_m … mem
     84     (set_sp … (mk_pointer XData b ? (mk_offset 0)) st))).
    8785cases b * #r #off #E >E %
    8886qed.
     87
     88definition rtl_save_frame:
     89 address → nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     90 λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st.
     91  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st) in
     92  let st ≝ set_frms rtl_sem_params frame st in
     93  rtl_call_function stacksize formal_arg_regs actual_arg_regs st.
    8994
    9095(*CSC: XXXX, for external functions only*)
     
    106111 OK … (pblock ptr). 
    107112
     113(* This code is quite similar to eval_call_block: can we factorize it out? *)
     114definition eval_tail_call_block:
     115 ∀globals.genv … (rtl_params globals) → state rtl_sem_params →
     116  block → call_args rtl_sem_params → IO io_out io_in (trace×(state rtl_sem_params)) ≝
     117 λglobals,ge,st,b,args.
     118  ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b);
     119    match fd with
     120    [ Internal fn ⇒
     121      let st ≝ set_m … (free … (m … st) (pblock (sp … st))) st in
     122      ! st ← rtl_call_function (joint_if_stacksize … fn) (joint_if_params … fn) args st ;
     123      let regs ≝ rtl_init_locals … (joint_if_locals … fn) (regs … st) in
     124      let l' ≝ joint_if_entry … fn in
     125       ret ? 〈 E0, goto … l' (set_regs rtl_sem_params regs st)〉
     126    | External fn ⇒ ?(*
     127      ! params ← fetch_external_args … fn st;
     128      ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     129      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     130      (* CSC: XXX bug here; I think I should split it into Byte-long
     131         components; instead I am making a singleton out of it. To be
     132         fixed once we fully implement external functions. *)
     133        let vs ≝ [mk_val ? evres] in
     134      ! st ← set_result … vs st;
     135      let st ≝ set_pc … ra st in
     136        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉 *)
     137     ].
     138cases daemon (*CSC: XXX tailcall to external function not implemented yet;
     139                    it needs alls other functions on external calls *)
     140qed.
     141
    108142definition rtl_exec_extended:
    109143 ∀globals. genv globals (rtl_params globals) →
     
    123157      eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
    124158       ge st b args dest ra
    125    | rtl_st_ext_tailcall_id id regs ⇒ ?
     159   | rtl_st_ext_tailcall_id id args ⇒
     160      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     161      eval_tail_call_block … ge st b args
    126162   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
    127163      ! b ← block_of_register_pair r1 r2 st ;
    128       ?
     164      eval_tail_call_block … ge st b args
    129165   ].
    130 [1,2: cases not_implemented ] (*CSC: tailcall semantics not implemented ATM *)
    131 qed.
    132166
    133167definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
Note: See TracChangeset for help on using the changeset viewer.