Changeset 3255


Ignore:
Timestamp:
May 8, 2013, 4:53:31 PM (4 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?

Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r2645 r3255  
    102102
    103103(* dpm: registers for stack manipulation *)
    104 definition RegisterSST ≝ Register10.
    105 definition RegisterST0 ≝ Register02.
    106 definition RegisterST1 ≝ Register03.
    107 definition RegisterST2 ≝ Register04.
    108 definition RegisterST3 ≝ Register05.
    109 definition RegisterSTS ≝ [RegisterST0; RegisterST1; RegisterST2; RegisterST3].
     104definition RegisterRets ≝ [Register00; Register01; Register02; Register03 ].
     105definition RegisterST0 ≝ Register04.
     106definition RegisterST1 ≝ Register05.
    110107definition RegisterSPL ≝ Register06.
    111108definition RegisterSPH ≝ Register07.
     
    121118   Register31; Register32; Register33; Register34; Register35;
    122119   Register36; Register37; RegisterA; RegisterB; RegisterDPL;
    123    RegisterDPH; RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
    124    RegisterSST].
    125 definition RegisterRets ≝ [RegisterDPL; RegisterDPH; Register00; Register01].
     120   RegisterDPH ].
    126121definition RegisterCallerSaved ≝
    127122  [Register00; Register01; Register02; Register03; Register04;
     
    135130definition RegistersForbidden ≝
    136131  [RegisterA; RegisterB; RegisterDPL; RegisterDPH;
    137    RegisterSPL; RegisterSPH; RegisterST0; RegisterST1;
    138    RegisterST2; RegisterST3; RegisterSST].
    139 (* registers minus forbidden *)
    140 definition RegistersAllocatable ≝
    141   [Register00; Register01; Register02; Register03; Register04;
    142    Register05; Register06; Register07; Register10; Register11;
    143    Register12; Register13; Register14; Register15; Register16;
    144    Register17; Register20; Register21; Register22; Register23;
    145    Register24; Register25; Register26; Register27; Register30;
    146    Register31; Register32; Register33; Register34; Register35;
    147    Register36; Register37].
     132   RegisterSPL; RegisterSPH; RegisterST0; RegisterST1 ].
     133(* all registers, as in fact interference with forbidden registers will
     134   disallow use of them for allocation *)
     135definition RegistersAllocatable ≝ Registers.
  • src/ERTL/ERTL.ma

    r3037 r3255  
    11include "joint/Joint.ma".
    22
    3 inductive move_dst: Type[0] ≝
    4   | PSD: register → move_dst
    5   | HDW: Register → move_dst.
     3inductive psd_or_hdw : Type[0] ≝
     4  | PSD: register → psd_or_hdw
     5  | HDW: Register → psd_or_hdw.
    66
    7 definition move_src ≝ argument move_dst.
     7definition ertl_hdw_readable : Register → Prop ≝
     8λR.match R with
     9  [ RegisterA ⇒ False
     10  | RegisterB ⇒ False
     11  | RegisterDPL ⇒ False
     12  | RegisterDPH ⇒ False
     13  | Register04 (* = RegisterST0 *) ⇒ False
     14  | Register05 (* = RegisterST1 *) ⇒ False
     15  | _ ⇒ True
     16  ].
    817
    9 definition move_src_from_dst : move_dst → move_src ≝ Reg move_dst.
    10 coercion move_dst_to_src : ∀r : move_dst.move_src ≝ move_src_from_dst on _r : move_dst to move_src.
     18definition ertl_readable ≝
     19λR.match R with
     20[ HDW R ⇒ ertl_hdw_readable R
     21| _ ⇒ True
     22].
     23
     24definition ertl_hdw_writable : Register → Prop ≝
     25λR.match R with
     26  [ Register06 (* = RegisterSPL *) ⇒ False
     27  | Register07 (* = RegisterSPH *) ⇒ False
     28  | _ ⇒ True
     29  ].
     30 
     31definition ertl_writable : psd_or_hdw → Prop ≝
     32λR.match R with
     33[ HDW R ⇒ ertl_hdw_writable R
     34| _ ⇒ True
     35].
     36
     37definition move_dst ≝ Σr : psd_or_hdw.ertl_writable r.
     38unification hint 0 ≔ ⊢ move_dst ≡ Sig psd_or_hdw (λr.ertl_writable r).
     39
     40definition move_src ≝ argument (Σr : psd_or_hdw.ertl_readable r).
     41
     42definition move_src_from_reg :
     43  (Σr.ertl_readable r) → move_src ≝ Reg ?.
     44coercion reg_to_move_src :
     45  ∀r : (Σr : psd_or_hdw.ertl_readable r).move_src ≝
     46  move_src_from_reg on _r : Sig psd_or_hdw ? to move_src.
    1147
    1248definition psd_argument_move_src : psd_argument → move_src ≝
    13   λarg.match arg with
     49  λarg.match arg return λ_.move_src with
    1450  [ Imm b ⇒ Imm ? b
    1551  | Reg r ⇒ Reg ? (PSD r)
    16   ].
     52  ]. @I qed.
    1753coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝
    1854  psd_argument_move_src on _a : psd_argument to move_src.
    1955
    2056inductive ertl_seq : Type[0] ≝
    21   | ertl_new_frame: ertl_seq
    22   | ertl_del_frame: ertl_seq
    2357  | ertl_frame_size: register → ertl_seq.
    2458
  • src/ERTL/ERTLToLTL.ma

    r3145 r3255  
    304304definition translate_step:
    305305  ∀globals,fn.nat → ∀after : valuation register_lattice.
    306   coloured_graph (livebefore globals fn after) →
     306  coloured_graph (interferes globals fn after) →
    307307  ℕ → label → joint_step ERTL globals → bind_step_block LTL globals ≝
    308308  λglobals,fn,localss,after,grph,stack_sz,lbl,s.
     
    313313    | Imm b ⇒ arg_decision_imm b
    314314    ] in
    315   let carry_lives_after ≝ hlives RegisterCarry (after lbl) in
     315  let carry_lives_after ≝ h_in_lattice RegisterCarry (after lbl) in
    316316  let move ≝ move globals localss carry_lives_after in
    317317  if eliminable_step … (after lbl) s then ([ ] : step_block LTL globals) else
     
    368368    | extension_seq ext ⇒
    369369      match ext with
    370       [ ertl_new_frame ⇒ newframe ? stack_sz
    371       | ertl_del_frame ⇒ delframe ? stack_sz
    372       | ertl_frame_size r ⇒
     370      [ ertl_frame_size r ⇒
    373371        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    374372      ]
     
    395393
    396394definition translate_fin_step:
    397   ∀globals.label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
    398   λglobals,lbl,s.
    399   bret … (〈[ ],
    400   match s with
    401   [ RETURN ⇒ RETURN ?
    402   | GOTO l ⇒ GOTO ? l
     395  ∀globals.ℕ → label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
     396  λglobals,stack_sz,lbl,s.
     397  bret … (match s with
     398  [ RETURN ⇒ 〈delframe ? stack_sz, RETURN ?〉
     399  | GOTO l ⇒ 〈[ ], GOTO ? l〉
    403400  | TAILCALL abs _ _ ⇒ Ⓧabs
    404   ]).
     401  ]).
    405402
    406403definition translate_data :
     
    420417    (* init_params ≝ *) it
    421418    (* init_stack_size ≝ *) stack_sz
    422     (* added_prologue ≝ *) [ ]
     419    (* added_prologue ≝ *) (newframe ? stack_sz)
    423420    (* new_regs ≝ *) [ ]
    424421    (* f_step ≝ *) (translate_step ? int_fun (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz)
    425     (* f_fin ≝ *) (translate_fin_step globals)
     422    (* f_fin ≝ *) (translate_fin_step globals stack_sz)
    426423    ????).
    427424@hide_prf
  • src/ERTL/Interference.ma

    r3014 r3255  
    55  | decision_colour: Register → decision.
    66
     7definition DeqRegister : DeqSet ≝
     8mk_DeqSet Register eq_Register ?.
     9#x #y % [2: #EQ destruct cases y % ]
     10cases x -x try (cases y -y normalize #EQ destruct %)
     11qed.
     12
     13unification hint 0 ≔ ⊢ Register ≡ carr DeqRegister.
     14
     15definition is_src_of_move :
     16∀globals.joint_statement ERTL globals → vertex → bool ≝
     17λglobals,s,v.
     18match s with
     19[ sequential s _ ⇒
     20  match s with
     21  [ step_seq s ⇒
     22    match s with
     23    [ MOVE pr ⇒
     24      match \snd pr with
     25      [ Reg r ⇒
     26        match r with
     27        [ PSD r ⇒ match v with [ inl r' ⇒ eq_identifier … r r' | _ ⇒ false ]
     28        | HDW r ⇒ match v with [ inr r' ⇒ eq_Register r r' | _ ⇒ false ]
     29        ]
     30      | _ ⇒ false
     31      ]
     32    | _ ⇒ false
     33    ]
     34  | _ ⇒ false
     35  ]
     36| _ ⇒ false
     37].
     38
     39definition interferes_asym :
     40  ∀globals.joint_internal_function ERTL globals →
     41  valuation register_lattice →
     42  label → vertex → vertex → bool ≝
     43λglobals,fn,liveafter,l,v1,v2.
     44match v1 with
     45[ inr R ⇒
     46  match v2 with [ inl _ ⇒ R ∈ RegistersForbidden | _ ⇒ false ]
     47| _ ⇒ false ]
     48
     49match stmt_at … (joint_if_code … fn) l with
     50[ None ⇒ false
     51| Some s ⇒
     52  in_lattice v1 (defined … s) ∧ in_lattice v2 (liveafter l) ∧
     53  ¬is_src_of_move … s v2
     54].
     55
     56definition interferes ≝ λglobals,fn,liveafter,label,v1,v2.
     57interferes_asym globals fn liveafter label v1 v2 ∨
     58interferes_asym globals fn liveafter label v2 v1.
     59
    760(* prop_colouring is the non interferece
    861   prop_colouring 2 and 3 together say that spilled_no is the number of spilled
    962   registers *)
    10 record coloured_graph (before: valuation register_lattice): Type[1] ≝
     63record coloured_graph (interferes : label → vertex → vertex → bool) : Type[1] ≝
    1164{ colouring: vertex → decision
    1265; spilled_no: nat
    13 ; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 →
    14   lives v1 (before l) → lives v2 (before l) → colouring v1 ≠ colouring v2
    15 ; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *)
    16    ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (before l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no
     66; prop_colouring: ∀l. ∀v1, v2: vertex.
     67  interferes l v1 v2 → colouring v1 = colouring v2 → v1 = v2
     68; prop_spilled_no: ∀v1:vertex.∀i.colouring v1 = decision_spill i → i < spilled_no
     69; hdw_same_colouring : ∀R.colouring (inr … R) = decision_colour R
    1770}.
    1871
     
    2174  ∀fn:joint_internal_function ERTL globals.
    2275   ∀liveafter.
    23     coloured_graph (livebefore globals fn liveafter).
     76    coloured_graph (interferes … fn liveafter).
  • src/ERTL/liveness.ma

    r3037 r3255  
    7474      | extension_seq ext ⇒
    7575        match ext with
    76          [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    77          | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    78          | ertl_frame_size r ⇒ rl_psingleton r
     76         [ ertl_frame_size r ⇒ rl_psingleton r
    7977         ]
    8078      (* Potentially destroys all caller-save hardware registers. *)
     
    131129      | extension_seq ext ⇒
    132130        match ext with
    133          [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    134          | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    135          | ertl_frame_size r ⇒ rl_bottom ]
     131         [ ertl_frame_size r ⇒ rl_bottom ]
    136132      (* Reads the hardware registers that are used to pass parameters. *)
    137133      | _ ⇒ rl_bottom
     
    190186  | extension_seq ext ⇒
    191187    match ext with
    192      [ ertl_new_frame ⇒ false
    193      | ertl_del_frame ⇒ false
    194      | ertl_frame_size r ⇒
     188     [ ertl_frame_size r ⇒
    195189       ¬set_member ? (eq_identifier RegisterTag) r pliveafter
    196190     ]
     
    253247definition vertex ≝ register + Register.
    254248
    255 definition plives : register → register_lattice → bool ≝
     249definition p_in_lattice : register → register_lattice → bool ≝
    256250  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
    257 definition hlives : Register → register_lattice → bool ≝
     251definition h_in_lattice : Register → register_lattice → bool ≝
    258252  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
    259253
    260 definition lives : vertex → register_lattice → bool ≝
     254definition in_lattice : vertex → register_lattice → bool ≝
    261255  λvertex.
    262256  match vertex with
    263   [ inl v ⇒ plives v
    264   | inr v ⇒ hlives v
    265   ].
     257  [ inl v ⇒ p_in_lattice v
     258  | inr v ⇒ h_in_lattice v
     259  ].
  • 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.