Changeset 1643 for src/RTL


Ignore:
Timestamp:
Jan 13, 2012, 12:23:30 PM (8 years ago)
Author:
tranquil
Message:
  • some changes in everything
  • separated extensions in sequential and final, to accomodate tailcalls
  • finished RTL's semantics
Location:
src/RTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_paolo.ma

    r1641 r1643  
    1919  are not sequential. Thus there is a dummy label at the moment in the code.
    2020  To be fixed once we understand exactly what to do with tail calls. *)
    21 inductive rtl_statement_extension: Type[0] ≝
    22   | rtl_st_ext_stack_address: register → register → rtl_statement_extension
    23   | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_statement_extension
     21inductive rtl_instruction_extension: Type[0] ≝
     22  | rtl_st_ext_stack_address: register → register → rtl_instruction_extension
     23  | rtl_st_ext_call_ptr: register → register → list rtl_argument → list register → rtl_instruction_extension.
     24
     25inductive rtl_statement_extension : Type[0] ≝
    2426  | rtl_st_ext_tailcall_id: ident → list rtl_argument → rtl_statement_extension
    2527  | rtl_st_ext_tailcall_ptr: register → register → list rtl_argument → rtl_statement_extension.
     
    3941    (* call_args ≝ *) (list rtl_argument)
    4042    (* call_dest ≝ *) (list register)
    41     (* extend_statements ≝ *) rtl_statement_extension
    42     (* ext_forall_labels ≝ *) (λP.λes.True))
     43    (* ext_instruction ≝ *) rtl_instruction_extension
     44    (* ext_forall_labels ≝ *) (λP.λes.True)
     45    (* ext_fin_instruction ≝ *) rtl_statement_extension
     46    (* ext_fin_forall_labels ≝ *) (λP.λes.True))
    4347  (mk_local_params
    4448    (mk_funct_params
     
    122126    (* call_dest ≝ *) (list register)
    123127    (* extend_statements ≝ *) rtlntc_statement_extension
    124     (* ext_forall_labels ≝ *) (λP.λes.True))
     128    (* ext_forall_labels ≝ *) (λP.λes.True)
     129    void (λP,es.True))
    125130  (mk_local_params
    126131    (mk_funct_params
  • src/RTL/semantics_paolo.ma

    r1641 r1643  
    4242
    4343
    44 definition rtl_call_function:
     44definition rtl_setup_call:
    4545 nat → list register → list rtl_argument → state rtl_sem_state_params → res (state rtl_sem_state_params) ≝
    4646  λstacksize,formal_arg_regs,actual_arg_regs,st.
     
    5959qed.
    6060
    61 definition rtl_save_frame:
    62  address → nat → list register → list rtl_argument → list register →
    63   state rtl_sem_state_params → res (state rtl_sem_state_params) ≝
    64  λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st.
    65   let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st) in
    66   let st ≝ set_frms rtl_sem_state_params frame st in
    67   rtl_call_function stacksize formal_arg_regs actual_arg_regs st.
     61definition rtl_save_frame ≝ λl.λretregs.λst : state rtl_sem_state_params.
     62  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
     63  set_frms rtl_sem_state_params frame st. 
    6864
    6965(*CSC: XXXX, for external functions only*)
     
    7167axiom rtl_set_result: list val → state rtl_sem_state_params → res (state rtl_sem_state_params).
    7268
    73 definition rtl_more_sem_unserialized_params :
     69definition rtl_msu_params :
    7470  more_sem_unserialized_params rtl_uns_params ≝
    7571 mk_more_sem_unserialized_params rtl_uns_params rtl_sem_state_params
     
    8581    rtl_init_locals
    8682    rtl_save_frame
     83    rtl_setup_call
    8784    rtl_fetch_external_args
    8885    rtl_set_result
    8986    [ ] [ ] (*dummy*).
    9087
    91 (* Paolo: got until here *)
     88(* alias *)
     89definition rtl_reg_store : register→beval→state rtl_sem_state_params→
     90    res (state rtl_sem_state_params) ≝ acca_store ? rtl_msu_params.
     91definition rtl_reg_retrieve : state rtl_sem_state_params→register→res beval ≝
     92    acca_retrieve ? rtl_msu_params.
    9293
    93 definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
    94 
    95 definition rtl_result_regs:
    96  ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list register) ≝
     94definition rtl_read_result :
     95 ∀globals. genv globals rtl_params → state rtl_sem_state_params → res (list beval) ≝
    9796 λglobals,ge,st.
    98   do fn ← graph_fetch_function … globals ge st ;
    99   OK … (joint_if_result … fn).
     97  ! p ← code_pointer_of_address (pc … st) ;
     98  ! fn ← fetch_function … ge p ;
     99  m_mmap … (rtl_reg_retrieve st) (joint_if_result … fn).
    100100
    101101(*CSC: we could use a dependent type here: the list of return values should have
     
    103103  saves the OutOfBounds exception *)
    104104definition rtl_pop_frame:
    105  ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     105 ∀globals. genv globals rtl_params → state rtl_sem_state_params →
     106  res (state rtl_sem_state_params) ≝
    106107 λglobals,ge,st.
    107   do ret_regs ← rtl_result_regs … ge st ;
    108   do ret_vals ← mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_regs ;
     108  do ret_vals ← rtl_read_result … ge st ;
    109109  match st_frms ? st with
    110110  [ nil ⇒ Error ? [MSG EmptyStack]
    111111  | cons hd tl ⇒
    112112     do st ←
    113       mfold_left_i ??
     113      mfold_left_i
    114114       (λi.λst.λreg.
    115115         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
    116          greg_store rtl_sem_params reg v st)
     116         rtl_reg_store reg v st)
    117117       (OK … st) (fr_ret_regs hd) ;
    118118     OK …
    119       (set_frms rtl_sem_params tl
    120         (set_regs rtl_sem_params (fr_regs hd)
     119      (set_frms rtl_sem_state_params tl
     120        (set_regs rtl_sem_state_params (fr_regs hd)
    121121         (set_sp … (fr_sp hd)
    122122          (set_carry … (fr_carry hd)
    123123           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    124124
    125 definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
    126  λglobals.
    127   mk_more_sem_params1 … rtl_more_sem_params graph_succ_p (graph_pointer_of_label …)
    128    (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
    129    rtl_init_locals rtl_save_frame (rtl_pop_frame …)
    130    rtl_fetch_external_args rtl_set_result.
    131 definition rtl_sem_params1: ∀globals. sem_params1 … globals ≝
    132  λglobals. mk_sem_params1 … (rtl_more_sem_params1 globals).
    133125
    134 definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
     126(* This code is quite similar to eval_call_block: can we factorize it out? *)
     127definition eval_tail_call_block:
     128 ∀globals.genv globals rtl_params → state rtl_sem_state_params →
     129  block → call_args rtl_uns_params → IO io_out io_in (trace×(state rtl_sem_state_params)) ≝
     130 λglobals,ge,st,b,args.
     131  ! 〈next, tr, st〉 ← eval_call_block_preamble ? rtl_params rtl_msu_params ge st b args (None ?) ;
     132  match next with
     133  [ None ⇒ (* Paolo: external tailcall, copied from evaluation of return, is it right? *)
     134    ! 〈st,ra〉 ← fetch_ra … st ;
     135    ! st ← rtl_pop_frame … ge st;
     136    return 〈tr,st〉
     137  | Some lbl ⇒
     138    return 〈tr,st〉
     139  ].
     140
     141definition block_of_register_pair: register → register → state rtl_sem_state_params → res block ≝
    135142 λr1,r2,st.
    136  do v1 ← greg_retrieve rtl_sem_params st r1 ;
    137  do v2 ← greg_retrieve rtl_sem_params st r2 ;
     143 do v1 ← rtl_reg_retrieve st r1 ;
     144 do v2 ← rtl_reg_retrieve st r2 ;
    138145 do ptr ← pointer_of_address 〈v1,v2〉 ;
    139146 OK … (pblock ptr). 
    140147
    141 (* This code is quite similar to eval_call_block: can we factorize it out? *)
    142 definition eval_tail_call_block:
    143  ∀globals.genv … (rtl_params globals) → state rtl_sem_params →
    144   block → call_args rtl_sem_params → IO io_out io_in (trace×(state rtl_sem_params)) ≝
    145  λglobals,ge,st,b,args.
    146   ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b);
    147     match fd with
    148     [ Internal fn ⇒
    149       let st ≝ set_m … (free … (m … st) (pblock (sp … st))) st in
    150       ! st ← rtl_call_function (joint_if_stacksize … fn) (joint_if_params … fn) args st ;
    151       let regs ≝ rtl_init_locals … (joint_if_locals … fn) (regs … st) in
    152       let l' ≝ joint_if_entry … fn in
    153       ! st ← next … (rtl_sem_params1 …) l' (set_regs rtl_sem_params regs st) ;
    154        ret ? 〈 E0, st〉
    155     | External fn ⇒ ?(*
    156       ! params ← fetch_external_args … fn st;
    157       ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    158       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    159       (* CSC: XXX bug here; I think I should split it into Byte-long
    160          components; instead I am making a singleton out of it. To be
    161          fixed once we fully implement external functions. *)
    162         let vs ≝ [mk_val ? evres] in
    163       ! st ← set_result … vs st;
    164       let st ≝ set_pc … ra st in
    165         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉 *)
    166      ].
    167 cases daemon (*CSC: XXX tailcall to external function not implemented yet;
    168                     it needs alls other functions on external calls *)
    169 qed.
    170 
    171148definition rtl_exec_extended:
    172  ∀globals. genv globals (rtl_params globals)
    173   rtl_statement_extension → label → state rtl_sem_params →
    174    IO io_out io_in (trace × (state rtl_sem_params)) ≝
    175  λglobals,ge,stm,l,st.
     149 ∀globals. genv globals rtl_params
     150  rtl_instruction_extension → state rtl_sem_state_params → address →
     151   IO io_out io_in ((option (label)) × trace × (state rtl_sem_state_params)) ≝
     152 λglobals,ge,stm,st,next_addr.
    176153  match stm with
    177154   [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
    178155      let sp ≝ sp ? st in
    179156      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
    180       ! st ← greg_store rtl_sem_params dreg1 dpl st ;
    181       ! st ← greg_store rtl_sem_params dreg2 dph st ;
    182       ! st ← next … (rtl_sem_params1 globals) l st ;
    183        ret ? 〈E0, st〉
     157      ! st ← rtl_reg_store dreg1 dpl st ;
     158      ! st ← rtl_reg_store dreg2 dph st ;
     159      return 〈None label,E0, st〉
    184160   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
    185       ! b ← block_of_register_pair r1 r2 st ;
    186       ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) ;
    187       eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
    188        ge st b args dest ra
    189    | rtl_st_ext_tailcall_id id args ⇒
    190       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     161     ! b ← block_of_register_pair r1 r2 st : IO ???;
     162     eval_call_block_preamble ? rtl_params rtl_msu_params
     163                              ge st b args (Some ? 〈dest,next_addr〉) ].
     164
     165definition rtl_exec_fin_extended:
     166 ∀globals. genv globals rtl_params →
     167  rtl_statement_extension → state rtl_sem_state_params →
     168   IO io_out io_in (trace × (state rtl_sem_state_params)) ≝
     169   λglobals,ge,stm,st.
     170   match stm with
     171   [ rtl_st_ext_tailcall_id id args ⇒
     172      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
    191173      eval_tail_call_block … ge st b args
    192    | rtl_st_ext_tailcall_ptr r1 r2 args ⇒ 
    193       ! b ← block_of_register_pair r1 r2 st ;
     174   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
     175      ! b ← block_of_register_pair r1 r2 st : IO ???;
    194176      eval_tail_call_block … ge st b args
    195177   ].
    196178
    197 definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
    198  λglobals. mk_more_sem_params2 … (rtl_more_sem_params1 globals) (rtl_exec_extended …).
     179definition rtl_msg_params : more_sem_genv_params rtl_params ≝
     180  mk_more_sem_genv_params rtl_params rtl_msu_params
     181    rtl_read_result
     182    rtl_exec_extended
     183    rtl_exec_fin_extended
     184    rtl_pop_frame.
    199185
    200 definition rtl_fullexec ≝
    201  joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
     186
     187
     188definition rtl_sem_params : sem_params ≝ make_sem_graph_params … rtl_msg_params.
     189
     190definition rtl_fullexec ≝ joint_fullexec … rtl_sem_params.
Note: See TracChangeset for help on using the changeset viewer.