Changeset 3255 for src/RTL/RTLToERTL.ma


Ignore:
Timestamp:
May 8, 2013, 4:53:31 PM (7 years ago)
Author:
tranquil
Message:
  • dropped newframe and delframe (to be integrated in calls and returns

in the semantics), as they were too wild for the proof of ERTL to LTL

  • ERTL now has a policy on what hardware registers can be written or

read

  • Rearranged special hardware registers: dropped STS, ST2 and ST3, and

moved DPL and DPH out of RegistersRets?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL.ma

    r3145 r3255  
    99
    1010definition save_hdws :
    11   ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝
     11  ∀globals.list (register×(Σr.ertl_hdw_readable r∧ertl_hdw_writable r)) → list (joint_seq ERTL globals) ≝
    1212 λglobals.
    13   let save_hdws_internal
    14    λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in
     13  let save_hdws_internal : (register×(Σr.?)) → ?
     14     λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in
    1515  map ?? save_hdws_internal.
     16[ @(π1 (pi2 ?? (\snd destr_srcr))) | @I ] qed.
    1617
    1718definition restore_hdws :
    18   ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝
     19  ∀globals.list (psd_argument×(Σr.ertl_hdw_readable r∧ertl_hdw_writable r)) → list (joint_seq ERTL globals) ≝
    1920  λglobals.
    2021   let restore_hdws_internal ≝
    21     λdestr_srcr:psd_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in
     22    λdestr_srcr:psd_argument×(Σr.?).HDW (\snd destr_srcr) ← \fst destr_srcr in
    2223    map ? ? restore_hdws_internal.
     24  @(π2 (pi2 ?? (\snd destr_srcr))) qed.
     25 
     26definition RegisterParamsSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
     27[Register30; Register31; Register32; Register33; Register34; Register35;
     28   Register36; Register37]. %% qed.
     29
     30definition RegisterCalleeSavedSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
     31[Register20; Register21; Register22; Register23; Register24; Register25;
     32   Register26; Register27]. %% qed.
     33
     34definition RegisterRetsSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
     35 [Register00; Register01; Register02; Register03]. %% qed.
    2336
    2437definition get_params_hdw :
    2538  ∀globals.list register → list (joint_seq ERTL globals) ≝
    2639  λglobals,params.
    27   save_hdws … (zip_pottier … params RegisterParams).
     40  save_hdws … (zip_pottier … params RegisterParamsSig).
    2841
    2942definition get_param_stack :
     
    5063    addr1 ← addr1 .Add. tmpr ;
    5164    addr2 ← addr2 .Addc. zero_byte ] @   
    52   flatten … (map ?? (get_param_stack globals addr1 addr2) params).
     65  flatten … (map ?? (get_param_stack globals addr1 addr2) params). % qed.
    5366
    5467definition get_params ≝
     
    5871  get_params_hdw globals hdw_params @ get_params_stack … tmpr addr1 addr2 stack_params.
    5972
     73(*
    6074definition save_return :
    61   ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
     75  ∀globals.list register → list (joint_seq ERTL globals) ≝
    6276  λglobals,ret_regs.
    6377  match reduce_strong ? ? RegisterSTS ret_regs with
     
    6781    let restl ≝ \snd (\fst crl) in
    6882    (* let restr ≝ \snd (\snd crl) in *)
    69     map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @
    70     map … (λst.HDW st ← zero_byte) restl
    71   ].
    72 
    73 definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝
    74   λglobals.
    75   match reduce_strong ?? RegisterRets RegisterSTS with
     83    map2 … (λst : Σr.?.λr : register.HDW st ← r) commonl commonr crl_proof @
     84    map … (λst : Σr.?.HDW st ← zero_byte) restl
     85  ]. @(pi2 ?? st) qed.
     86*)
     87
     88
     89definition assign_result : ∀globals.
     90  list register → list (joint_seq ERTL globals) ≝
     91  λglobals,ret_regs.
     92  match reduce_strong ?? RegisterRetsSig ret_regs with
    7693  [ mk_Sig crl crl_proof ⇒
    7794    let commonl ≝ \fst (\fst crl) in
    7895    let commonr ≝ \fst (\snd crl) in
    79     map2 … (λret,st.HDW ret ← HDW st) commonl commonr crl_proof
    80   ].
     96    let restl ≝ \snd (\fst crl) in
     97    map2 … (λR : Σr.?.λr : register.HDW R ← PSD r) commonl commonr crl_proof @
     98    map … (λR : Σr.?.HDW R ← zero_byte) restl
     99  ]. [ @I |*: @(π2 (pi2 ?? R)) ] qed.
    81100
    82101lemma All_map2 : ∀A,B,C,P,R,f,l1,l2,prf.
     
    101120
    102121definition epilogue :
    103   ∀globals.list register → register → register → list (register × Register) →
     122  ∀globals.list register → register → register → list (register × (Σr.?)) →
    104123  Σl : list (joint_seq ERTL globals).
    105124  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
    106125  λglobals,ret_regs,sral,srah,sregs.
    107   save_return … (map … (Reg ?) ret_regs) @
    108   restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
     126  restore_hdws … (map ?? (λx.〈Reg ? (\fst x), \snd x〉) sregs) @
     127  assign_result globals ret_regs @
    109128  [ PUSH ERTL ? sral ;
    110     PUSH … srah ;
    111     ertl_del_frame ] @
    112   assign_result globals.
     129    PUSH … srah ].
    113130@hide_prf
    114131@All_append
    115 [ whd in match save_return; normalize nodelta
    116   cases (reduce_strong ????) ** #a #b * #c #d #prf normalize nodelta
    117   @All_append
    118   [ @(All_map2 … (All2_True … prf)) #x #y #_ %
    119   | @(All_map … (All_True …)) #x #_ %
    120   ]
     132[ @(All_map … (All_True …)) #x #_ %
    121133| @All_append
    122   [ @(All_map … (All_True …)) #x #_ %
    123   | %{(refl …)} %{(refl …)} %{(refl …)}
    124     whd in match assign_result;
     134  [ whd in match assign_result;
    125135    generalize in match reduce_strong; #f normalize nodelta
    126136    cases (f ????) #l #prf normalize nodelta
    127     @(All_map2 … (All2_True … prf)) #x #y #_ %
     137    @All_append
     138    [ @(All_map2 … (All2_True … prf)) #x #y #_ %
     139    | @(All_map … (All_True …)) #x #_ %
     140    ]
     141  | %%%
    128142  ]
    129143]
     
    132146definition prologue :
    133147  ∀globals.list register → register → register → register → register → register →
    134   list (register×Register) →
     148  list (register×(Σr.?)) →
    135149  bind_new register (list (joint_seq ERTL globals)) ≝
    136150  λglobals,params,sral,srah,tmpr,addr1,addr2,sregs.
    137   [ (ertl_new_frame : joint_seq ??) ;
    138     POP … srah ;
     151  [ POP … srah ;
    139152    POP … sral
    140153  ] @ save_hdws … sregs @ get_params … tmpr addr1 addr2 params.
     
    143156  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
    144157  λglobals,params.
    145   restore_hdws globals (zip_pottier ? ? params RegisterParams).
    146 
    147 (* Paolo: The following can probably be done way more efficiently with INC DPTR *)
     158  restore_hdws globals (zip_pottier ? ? params RegisterParamsSig).
    148159
    149160definition set_param_stack :
     
    167178    addr2 ← addr2 .Sub. zero_byte
    168179  ] @
    169   flatten … (map … (set_param_stack globals addr1 addr2) params).
     180  flatten … (map … (set_param_stack globals addr1 addr2) params). % qed.
    170181
    171182definition set_params :
     
    174185  BindNewP … (All (joint_seq ??) (λs.step_labels … s = [ ])) b ≝
    175186  λglobals,params.
    176   let n ≝ min (|params|) (|RegisterParams|) in
     187  let n ≝ min (|params|) (|RegisterParamsSig|) in
    177188  let hdw_stack_params ≝ split ? params n in
    178189  let hdw_params ≝ \fst hdw_stack_params in
     
    197208  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
    198209  λglobals,ret_regs.
    199   match reduce_strong ?? RegisterSTS RegisterRets with
     210  match reduce_strong ?? ret_regs RegisterRetsSig with
    200211  [ mk_Sig crl crl_proof ⇒
    201212    let commonl ≝ \fst (\fst crl) in
    202213    let commonr ≝ \fst (\snd crl) in
    203     map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @
    204     match reduce_strong ?? ret_regs RegisterSTS with
    205     [ mk_Sig crl crl_proof ⇒
    206       let commonl ≝ \fst (\fst crl) in
    207       let commonr ≝ \fst (\snd crl) in
    208       map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof
    209     ]
     214    map2 … (λr.λR : Σr.?.PSD r ← HDW R) commonl commonr crl_proof
    210215  ].
    211 @hide_prf
    212 @All_append
    213 [ @(All_map2 … (All2_True … crl_proof)) #x #y #_ %
    214 | cases (reduce_strong ????) #l #prf normalize nodelta
    215   @(All_map2 … (All2_True … prf)) #x #y #_ %
    216 ]
     216@hide_prf [2: % |3: @(π1 (pi2 … R)) ]
     217@(All_map2 … (All2_True … crl_proof)) #x #y #_ %
    217218qed.
    218219
     
    260261  | COND r ltrue ⇒
    261262    bret … 〈[ ], λ_.COND ERTL ? r ltrue, [ ]〉
    262   ].
     263  ]. % qed.
    263264
    264265definition translate_fin_step :
    265   ∀globals.list register → register → register → list (register × Register) →
     266  ∀globals.list register → register → register → list (register × (Σr.?)) →
    266267    label → joint_fin_step RTL →
    267268    bind_fin_block ERTL globals ≝
     
    275276definition allocate_regs :
    276277  ∀X : Type[0].
    277   (list (register×Register) → bind_new register X) →
     278  (list (register×(Σr.?)) → bind_new register X) →
    278279  bind_new register X ≝
    279280  λX,f.
    280281  let allocate_regs_internal ≝
    281     λacc : bind_new register (list (register × Register)).
    282     λr: Register.
     282    λacc : bind_new register (list (register × (Σr.?))).
     283    λr: Σr.?.
    283284    ! tl ← acc ;
    284285    νr' in return (〈r', r〉 :: tl) in
    285   ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSaved ;
     286  ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSavedSig ;
    286287  f to_save.
    287288
     
    314315  try #a try #b try #c try #d try #e try #f destruct
    315316  cases a in b; #a1 #a2 normalize nodelta #EQ destruct
    316 | #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2
    317 % (* XXX: FAILS, unintentional list reversal??? *)
     317| #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 %
    318318]
    319319(* #l *
Note: See TracChangeset for help on using the changeset viewer.