Changeset 2935


Ignore:
Timestamp:
Mar 21, 2013, 9:37:41 PM (4 years ago)
Author:
tranquil
Message:

separation of RTL semantics in three different versions, and correction of a bug in pop_frame.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_semantics.ma

    r2823 r2935  
    33include alias "common/Identifiers.ma".
    44include alias "ASM/Util.ma".
     5
     6(* we design here three different semantics of RTL, which differ on how stack
     7   is treated.
     8   
     9   1) the first, RTL_semantics_separate, allocates a new stack for each
     10      function call, behaving like RTLabs. Each separate stack is finite
     11      (offsets are bounded by 2^16), but the number of stacks is unbounded
     12   2) the second, RTL_semantics_separate_overflow, behaves like the previous one,
     13      but is defined to fail on stack overflow. The idea is that we use the
     14      hypothesis of not stack overflowing to pass from RTL_semantics_separate to
     15      RTL_semantics_separate_overflow, without having to trasnform the states in
     16      any way
     17   3) the third, RTL_semantics_unique, behaves like ERTL and later languages:
     18      the stack is unique (allocation happens once in make_initial_state, see
     19      joint/Traces.ma). However the proof that allows passing from
     20      RTL_semantics_separate_overflow to RTL_semantics_unique should not
     21      rely on any hypothesis about stack usage
     22
     23*)
     24
     25record reg_sp : Type[0] ≝
     26{ reg_sp_env :> identifier_map RegisterTag beval
     27; stackp : xpointer
     28}.
     29
     30definition reg_sp_store ≝ λreg,v,locals.
     31let locals' ≝ reg_store reg v (reg_sp_env locals) in
     32mk_reg_sp locals' (stackp locals).
     33
     34definition reg_sp_retrieve ≝ λlocals : reg_sp.reg_retrieve locals.
     35
     36definition reg_sp_empty ≝ mk_reg_sp (empty_map …).
     37(*** Store/retrieve on hardware registers ***)
    538
    639record frame: Type[0] ≝
     
    1649    [ ]
    1750    reg_sp
    18     reg_sp_init
     51    reg_sp_empty
    1952    (λenv.OK … (stackp env))
    2053    (λenv.mk_reg_sp env (* coercion*)).
     
    6093      do v ← rtl_arg_retrieve … (regs ? st) src ;
    6194      OK … (reg_sp_store dest v lenv))
    62     (OK … (reg_sp_init sp)) formal_arg_regs actual_arg_regs ;
     95    (OK … (reg_sp_empty sp)) formal_arg_regs actual_arg_regs ;
    6396  OK …
    6497   (set_regs RTL_state_params new_regs
     
    72105qed.
    73106
     107(* move *)
     108axiom StackOverflow : ErrorMessage.
     109
     110definition rtl_setup_call_separate_overflow :
     111 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
     112  λstacksize,formal_arg_regs,actual_arg_regs,st.
     113  (* using nats is highly inefficient... *)
     114  if leb (S (stacksize + stack_usage … st)) (2^16) then
     115    rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
     116  else Error … [MSG StackOverflow].
     117
    74118definition rtl_setup_call_unique :
    75119 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
    76120  λstacksize,formal_arg_regs,actual_arg_regs,st.
    77   (* paolo: this will need to be changed: we want a unified stack in the whole backend *)
    78121  ! sp ← sp … st ; (* always succeeds in RTL *)
    79122  let newsp ≝ neg_shift_pointer … sp (bitvector_of_nat 8 stacksize) in
     
    83126      do v ← rtl_arg_retrieve … (regs ? st) src ;
    84127      OK … (reg_sp_store dest v lenv))
    85     (OK … (reg_sp_init newsp)) formal_arg_regs actual_arg_regs ;
     128    (OK … (reg_sp_empty newsp)) formal_arg_regs actual_arg_regs ;
    86129  OK …
    87130   (set_regs RTL_state_params new_regs st).
     
    128171       compiled programs *)
    129172    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
    130     let st ≝ foldl …
    131       (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
    132       st reg_vals in
    133173    ! sp ← sp … st ;  (* always succeeds in RTL *)
    134174    let st ≝ set_frms RTL_state_params tl
     
    137177            (set_m … (free … (m … st) (pblock sp)) st))) in
    138178    let pc ≝ fr_pc hd in
     179    let st ≝ foldl …
     180      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
     181      st reg_vals in
    139182    return 〈st, pc〉
    140183  ].
     
    155198       compiled programs *)
    156199    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
    157     let st ≝ foldl …
    158       (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
    159       st reg_vals in
    160200    ! sp ← sp … st ;  (* always succeeds in RTL *)
    161201    let st ≝ set_frms RTL_state_params tl
     
    163203          (set_carry RTL_state_params (fr_carry hd) st)) in
    164204    let pc ≝ fr_pc hd in
     205    let st ≝ foldl …
     206      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
     207      st reg_vals in
    165208    return 〈st, pc〉
    166209  ].
     
    188231definition reg_res_store ≝ λr,v,s.OK ? (reg_sp_store r v s).
    189232
    190 (* two different semantics: one with separate stacks for each call,
    191    the other with a unique one *)
    192233definition RTL_semantics_separate ≝
    193234  mk_sem_graph_params RTL
     
    211252      (λ_.λ_.λ_.rtl_pop_frame_separate)).
    212253
     254definition RTL_semantics_separate_overflow ≝
     255  mk_sem_graph_params RTL
     256    (λF.mk_sem_unserialized_params RTL F
     257      RTL_state_params
     258      reg_res_store reg_sp_retrieve rtl_arg_retrieve
     259      reg_res_store reg_sp_retrieve rtl_arg_retrieve
     260      reg_res_store reg_sp_retrieve rtl_arg_retrieve
     261      reg_res_store reg_sp_retrieve rtl_arg_retrieve
     262      rtl_arg_retrieve
     263      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
     264        ! v ← rtl_arg_retrieve env src ;
     265        return reg_sp_store dest v env)
     266      (λ_.rtl_save_frame)
     267      rtl_setup_call_separate_overflow
     268      rtl_fetch_external_args
     269      rtl_set_result
     270      [ ] [ ]
     271      (λ_.λ_.rtl_read_result) 
     272      (λ_.λ_.eval_rtl_seq)
     273      (λ_.λ_.λ_.rtl_pop_frame_separate)).
     274
    213275definition RTL_semantics_unique ≝
    214276  mk_sem_graph_params RTL
     
    231293      (λ_.λ_.eval_rtl_seq)
    232294      (λ_.λ_.λ_.rtl_pop_frame_unique)).
    233 
    234 
Note: See TracChangeset for help on using the changeset viewer.