Changeset 2217 for src/RTL


Ignore:
Timestamp:
Jul 19, 2012, 6:13:54 PM (9 years ago)
Author:
tranquil
Message:
  • collapsed step_params, unserialized_params, funct_params and local_params into one (unserialized_params)
  • completed update of RTL, LTL and LIN semantics
Location:
src/RTL
Files:
3 edited

Legend:

Unmodified
Added
Removed

  • src/RTL/RTLToERTL_paolo.ma

    r2214 r2217  
    66
    77include alias "basics/lists/list.ma".
     8
     9definition ertl_fresh_reg:
     10 ∀globals.freshT ERTL globals register ≝
     11  λglobals,def.
     12    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     13    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
    814
    915definition save_hdws :
    … …  
    101107definition allocate_regs :
    102108  ∀globals,rs.rs_set rs →
    103   state_monad (joint_internal_function ERTL globals) (list (register×Register)) ≝
     109  freshT ERTL globals (list (register×Register)) ≝
    104110  λglobals,rs,saved,def.
    105111   let allocate_regs_internal ≝
    106112    λr: Register.
    107113    λdef_sregs.
    108     let 〈def, r'〉 ≝ rtl_ertl_fresh_reg … (\fst def_sregs) in
     114    let 〈def, r'〉 ≝ ertl_fresh_reg … (\fst def_sregs) in
    109115    〈def, 〈r', r〉::\snd def_sregs〉 in
    110116  rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉.
    … …  
    118124  let end_lbl ≝ joint_if_exit … def in
    119125  state_run … def (
    120     ! sral ← rtl_ertl_fresh_reg … ;
    121     ! srah ← rtl_ertl_fresh_reg … ;
     126    ! sral ← ertl_fresh_reg … ;
     127    ! srah ← ertl_fresh_reg … ;
    122128    ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ;
    123     ! prologue' ← bcompile … (rtl_ertl_fresh_reg …) (prologue … params sral srah sregs) ;
     129    ! prologue' ← bcompile … (ertl_fresh_reg …) (prologue … params sral srah sregs) ;
    124130    let epilogue' ≝ epilogue … ret_regs sral srah sregs in
    125131    ! def' ← state_get … ;
    … …  
    258264      graph' entry' exit' in
    259265  let def'' ≝ b_graph_translate …
    260     (rtl_ertl_fresh_reg …)
     266    (ertl_fresh_reg …)
    261267    def'
    262268    (translate_step globals)

  • src/RTL/RTL_paolo.ma

    r2214 r2217  
    1212
    1313definition RTL_uns ≝ mk_unserialized_params
    14   (mk_step_params
    1514    (* acc_a_reg ≝ *) register
    1615    (* acc_b_reg ≝ *) register
    … …  
    2827    (* ext_call ≝ *) rtl_call
    2928    (* ext_tailcall ≝ *) rtl_tailcall
    30   )
    31   (mk_local_params
    32     (mk_funct_params
    33       (* resultT ≝ *) (list register)
    34       (* paramsT ≝ *) (list register))
    35       (* localsT ≝ *) register).
     29    (* paramsT ≝ *) (list register)
     30    (* localsT ≝ *) register.
    3631
    3732definition RTL ≝ mk_graph_params RTL_uns.
    … …  
    9893
    9994definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params
    100   (mk_step_params
    10195    (* acc_a_reg ≝ *) register
    10296    (* acc_b_reg ≝ *) register
    … …  
    114108    (* ext_call ≝ *) rtl_call
    115109    (* ext_tailcall ≝ *) void
    116   )
    117   (mk_local_params
    118     (mk_funct_params
    119       (* resultT ≝ *) (list register)
    120       (* paramsT ≝ *) (list register))
    121       (* localsT ≝ *) register)).
     110    (* paramsT ≝ *) (list register)
     111    (* localsT ≝ *) register).
    122112
    123113definition rtl_ntc_program ≝ joint_program RTL_ntc.

  • src/RTL/semantics_paolo.ma

    r1999 r2217  
    66record frame: Type[0] ≝
    77 { fr_ret_regs: list register
    8  ; fr_pc: address
    9  ; fr_sp: pointer
     8 ; fr_pc: cpointer
     9 ; fr_sp: xpointer
    1010 ; fr_carry: beval
    1111 ; fr_regs: register_env beval
    1212 }.
    1313
    14 definition rtl_sem_state_params : sem_state_params ≝
     14definition RTL_state : sem_state_params ≝
    1515  mk_sem_state_params
    1616    (list frame)
    … …  
    1919    (λ_.empty_map …).
    2020
    21 definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : rtl_argument.
     21definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : psd_argument.
    2222  match a with
    2323  [ Reg r ⇒ reg_retrieve env r
    24   | Imm b ⇒ return (BVByte b)
     24  | Imm b ⇒ return b
    2525  ].
    2626
    … …  
    3030
    3131definition rtl_fetch_ra:
    32  state rtl_sem_state_params → res ((state rtl_sem_state_params) × address) ≝
     32 state RTL_state → res ((state RTL_state) × cpointer) ≝
    3333 λst.
    3434  match st_frms ? st with
    … …  
    3636  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
    3737
    38 definition rtl_init_locals :
    39  list register → register_env beval → register_env beval ≝
    40  λlocals,env.
    41   foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals.
    42 
     38definition rtl_init_local :
     39 register → register_env beval → register_env beval ≝
     40 λlocal,env.add … env local BVundef.
    4341
    4442definition rtl_setup_call:
    45  nat → list register → list rtl_argument → state rtl_sem_state_params → res (state rtl_sem_state_params) ≝
     43 nat → list register → list psd_argument → state RTL_state → res (state RTL_state) ≝
    4644  λstacksize,formal_arg_regs,actual_arg_regs,st.
    4745  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
    … …  
    5351    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
    5452  OK …
    55    (set_regs rtl_sem_state_params new_regs
     53   (set_regs RTL_state new_regs
    5654    (set_m … mem
    57      (set_sp … (mk_pointer XData b ? (mk_offset 0)) st))).
     55     (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))).
    5856cases b * #r #off #E >E %
    5957qed.
    6058
    61 definition rtl_save_frame ≝ λl.λretregs.λst : state rtl_sem_state_params.
     59definition rtl_save_frame ≝ λl.λretregs.λst : state RTL_state.
    6260  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. 
     61  OK … (set_frms RTL_state frame st).
    6462
    6563(*CSC: XXXX, for external functions only*)
    66 axiom rtl_fetch_external_args: external_function → state rtl_sem_state_params → res (list val).
    67 axiom rtl_set_result: list val → state rtl_sem_state_params → res (state rtl_sem_state_params).
    68 
    69 definition rtl_msu_params :
    70   more_sem_unserialized_params rtl_uns_params ≝
    71  mk_more_sem_unserialized_params rtl_uns_params rtl_sem_state_params
    72     reg_store reg_retrieve rtl_arg_retrieve
    73     reg_store reg_retrieve rtl_arg_retrieve
    74     reg_store reg_retrieve rtl_arg_retrieve
    75     reg_store reg_retrieve rtl_arg_retrieve
    76     rtl_arg_retrieve
    77     (λenv,p. let 〈dest,src〉 ≝ p in
    78       ! v ← rtl_arg_retrieve env src ;
    79       reg_store dest v env)
    80     rtl_fetch_ra
    81     rtl_init_locals
    82     rtl_save_frame
    83     rtl_setup_call
    84     rtl_fetch_external_args
    85     rtl_set_result
    86     [ ] [ ] (*dummy*).
    87 
    88 (* alias *)
    89 definition rtl_reg_store : register→beval→state rtl_sem_state_params→
    90     res (state rtl_sem_state_params) ≝ acca_store ? rtl_msu_params.
    91 definition rtl_reg_retrieve : state rtl_sem_state_params→register→res beval ≝
    92     acca_retrieve ? rtl_msu_params.
     64axiom rtl_fetch_external_args: external_function → state RTL_state → res (list val).
     65axiom rtl_set_result: list val → list register → state RTL_state → res (state RTL_state).
     66
     67definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st.
     68definition rtl_reg_retrieve ≝ λst.reg_retrieve (regs RTL_state st).
    9369
    9470definition rtl_read_result :
    95  ∀globals. genv globals rtl_params → state rtl_sem_state_params → res (list beval) ≝
    96  λglobals,ge,st.
    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).
     71 ∀globals.genv RTL globals → list register → state RTL_state → res (list beval) ≝
     72 λglobals,ge,rets,st.
     73 m_list_map … (rtl_reg_retrieve st) rets.
    10074
    10175(*CSC: we could use a dependent type here: the list of return values should have
    … …  
    10377  saves the OutOfBounds exception *)
    10478definition rtl_pop_frame:
    105  ∀globals. genv globals rtl_params → state rtl_sem_state_params →
    106   res (state rtl_sem_state_params) ≝
    107  λglobals,ge,st.
    108   do ret_vals ← rtl_read_result … ge st ;
     79 ∀globals. genv RTL globals → list register → state RTL_state →
     80  res (state RTL_state) ≝
     81 λglobals,ge,ret,st.
     82  do ret_vals ← rtl_read_result … ge ret st ;
    10983  match st_frms ? st with
    11084  [ nil ⇒ Error ? [MSG EmptyStack]
    … …  
    11791       (OK … st) (fr_ret_regs hd) ;
    11892     OK …
    119       (set_frms rtl_sem_state_params tl
    120         (set_regs rtl_sem_state_params (fr_regs hd)
     93      (set_frms RTL_state tl
     94        (set_regs RTL_state (fr_regs hd)
    12195         (set_sp … (fr_sp hd)
    12296          (set_carry … (fr_carry hd)
    12397           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    12498
    125 
    12699(* This code is quite similar to eval_call_block: can we factorize it out? *)
    127 definition 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 
    141 definition block_of_register_pair: register → register → state rtl_sem_state_params → res block ≝
     100definition eval_tailcall_block:
     101 ∀globals.genv RTL globals → state RTL_state →
     102  block → call_args RTL →
     103  (* this is where the result of the current function should be stored *)
     104  call_dest RTL →
     105  IO io_out io_in
     106    ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×(state RTL_state)) ≝
     107 λglobals,ge,st,b,args,ret.
     108  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
     109    match fd with
     110    [ Internal fd ⇒
     111      return 〈FTailInit ?? (block_id b) fd args, st〉
     112    | External fn ⇒
     113      ! params ← rtl_fetch_external_args … fn st : IO ???;
     114      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     115      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     116      (* CSC: XXX bug here; I think I should split it into Byte-long
     117         components; instead I am making a singleton out of it. To be
     118         fixed once we fully implement external functions. *)
     119      let vs ≝ [mk_val ? evres] in
     120      ! st ← rtl_set_result … vs ret st : IO ???;
     121      return 〈FEnd2 ??, st〉
     122    ].
     123
     124definition block_of_register_pair: register → register → state RTL_state → res block ≝
    142125 λr1,r2,st.
    143126 do v1 ← rtl_reg_retrieve st r1 ;
    … …  
    146129 OK … (pblock ptr). 
    147130
    148 definition rtl_exec_extended:
    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.
     131definition eval_rtl_seq:
     132 ∀globals. genv RTL globals →
     133  rtl_seq → state RTL_state →
     134   IO io_out io_in (state RTL_state) ≝
     135 λglobals,ge,stm,st.
    153136  match stm with
    154    [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
     137   [ rtl_stack_address dreg1 dreg2  ⇒
    155138      let sp ≝ sp ? st in
    156139      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
    157140      ! st ← rtl_reg_store dreg1 dpl st ;
    158       ! st ← rtl_reg_store dreg2 dph st ;
    159       return 〈None label,E0, st〉
    160    | rtl_st_ext_call_ptr r1 r2 args dest ⇒
    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 
    165 definition 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.
     141      rtl_reg_store dreg2 dph st
     142   ].
     143
     144definition eval_rtl_call:
     145 ∀globals. genv RTL globals →
     146  rtl_call → state RTL_state →
     147   IO io_out io_in ((step_flow RTL ? Call)×(state RTL_state)) ≝
     148 λglobals,ge,stm,st.
     149  match stm with
     150  [ rtl_call_ptr r1 r2 args dest ⇒
     151    ! b ← block_of_register_pair r1 r2 st : IO ???;
     152    ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
     153    match fd with
     154    [ Internal fd ⇒
     155      return 〈Init ?? (block_id b) fd args dest, st〉
     156    | External fn ⇒
     157      ! params ← rtl_fetch_external_args … fn st : IO ???;
     158      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     159      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     160      (* CSC: XXX bug here; I think I should split it into Byte-long
     161         components; instead I am making a singleton out of it. To be
     162         fixed once we fully implement external functions. *)
     163      let vs ≝ [mk_val ? evres] in
     164      ! st ← rtl_set_result … vs dest st : IO ???;
     165      return 〈Proceed ???, st〉
     166    ]
     167  ].
     168
     169definition eval_rtl_tailcall:
     170 ∀globals. genv RTL globals →
     171  rtl_tailcall → call_dest RTL → state RTL_state →
     172   IO io_out io_in ((fin_step_flow RTL ? Call)×(state RTL_state)) ≝
     173   λglobals,ge,stm,ret,st.
    170174   match stm with
    171    [ rtl_st_ext_tailcall_id id args ⇒
     175   [ rtl_tailcall_id id args ⇒
    172176      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    173       eval_tail_call_block … ge st b args
    174    | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
     177      eval_tailcall_block … ge st b args ret
     178   | rtl_tailcall_ptr r1 r2 args ⇒
    175179      ! b ← block_of_register_pair r1 r2 st : IO ???;
    176       eval_tail_call_block … ge st b args
     180      eval_tailcall_block … ge st b args ret
    177181   ].
    178182
    179 definition rtl_msg_params : more_sem_genv_params rtl_params ≝
    180   mk_more_sem_genv_params rtl_params rtl_msu_params
     183definition RTL_semantics ≝
     184  mk_more_sem_unserialized_params RTL (joint_internal_function RTL)
     185    RTL_state
     186    reg_store reg_retrieve rtl_arg_retrieve
     187    reg_store reg_retrieve rtl_arg_retrieve
     188    reg_store reg_retrieve rtl_arg_retrieve
     189    reg_store reg_retrieve rtl_arg_retrieve
     190    rtl_arg_retrieve
     191    (λenv,p. let 〈dest,src〉 ≝ p in
     192      ! v ← rtl_arg_retrieve env src ;
     193      reg_store dest v env)
     194    rtl_fetch_ra
     195    rtl_init_local
     196    rtl_save_frame
     197    rtl_setup_call
     198    rtl_fetch_external_args
     199    rtl_set_result
     200    [ ] [ ]
    181201    rtl_read_result
    182     rtl_exec_extended
    183     rtl_exec_fin_extended
    184     rtl_pop_frame.
    185 
    186 
    187 
    188 definition rtl_sem_params : sem_params ≝ make_sem_graph_params … rtl_msg_params.
    189 
    190 definition rtl_fullexec ≝ joint_fullexec … rtl_sem_params.
     202    eval_rtl_seq
     203    eval_rtl_tailcall
     204    eval_rtl_call.
Note: See TracChangeset for help on using the changeset viewer.