Changeset 2806 for src


Ignore:
Timestamp:
Mar 7, 2013, 2:51:40 PM (7 years ago)
Author:
tranquil
Message:

new b_graph_translate obligations

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToERTLptr.ma

    r2696 r2806  
    8282    (* init_stack_size ≝ *) (joint_if_stacksize … def)
    8383    (* added_prologue ≝ *) [ ]
     84    (* new_regs ≝ *) [ ]
    8485    (* f_step ≝ *) (translate_step globals)
    8586    (* f_fin ≝ *) (translate_fin_step globals)
    86     ???).
     87    ????).
    8788@hide_prf
    88 [ #l #c % ]
     89[ #l * [ #c' | * #f #args #dest | #a #ltrue | #s ] #c whd
     90  [3: #r1 ] #l' #EQ destruct try %
     91  cases s in EQ; whd in match ensure_step_block; normalize nodelta
     92  try #a try #b try #c try #d try #e try #f destruct
     93| #l #c %
     94]
    8995#l *
    90 [ #l whd %{I} %{I} %1 %
    91 | whd %{I I}
    92 | #abs #called #args whd %{I I}
    93 | #c %{I} %{I} #l %
     96[ #l' whd %{I} %{I} %{I} %2 % %
     97| whd %{I} %{I I}
     98| #abs #called #args whd %{I} %{I I}
     99| #c #l' whd %{I} %{I} %{I} %
    94100| * #called #args #dest whd in match translate_step; normalize nodelta whd
    95   [ %{I} %{I} #l %
    96   | #r whd %{I} %{(λ_.I)} % [| % [| % [| %{I} ]]] #l
    97     [1,3: %{I} %1 %
    98     |*: %
    99     ]
     101  [ #l' %{I} %{I} %{I} %
     102  | #r #l' whd %{I} % [2: %{I I} ] % [2: % [2: % [2: %{I} ]]] % try @I %{I} %1 %
    100103  ]
    101 | #a #l_true whd %{I} %{I} #l %{I} %2 %1 %
    102 | #s whd %{I} %{I} #l whd @(All_mp … (In ? (step_labels … s)))
    103   [ #l' #H %2{H} ] cases s -s //
     104| #a #l_true whd #l %{I} %{I} % %{I} [ %2 ] %1 %
     105| #s whd #l %{I} %{I} whd %
     106  [ @(All_mp … (In ? (step_labels … s))) [ #l' #H %2{H} ] cases s -s // ]
     107  cut (∀X,l1,l2.l1 = l2 → All X (In X l1) l2)
     108  [ #X #l1 #l2 #EQ destruct elim l2 [ % ] #hd #tl #IH % [ %1 % ] @(All_mp … IH) #x #H %2{H} ]
     109  #aux @aux cases s //
    104110]
    105111qed.
  • src/ERTLptr/ERTLptrToLTL.ma

    r2774 r2806  
    435435    (* init_stack_size ≝ *) stack_sz
    436436    (* added_prologue ≝ *) [ ]
     437    (* new_regs ≝ *) [ ]
    437438    (* f_step ≝ *) (translate_step … coloured_graph stack_sz)
    438439    (* f_fin ≝ *) (translate_fin_step globals)
    439     ???).
     440    ????).
    440441@hide_prf
    441 [ #l #c % ]
     442[
     443| #l #c % ]
    442444cases daemon (* TODO *)
    443445qed.
  • src/RTL/RTLToERTL.ma

    r2689 r2806  
    3737
    3838definition get_params_stack :
    39   ∀globals.list register →
    40   bind_new register (list (joint_seq ERTL globals)) ≝
    41   λglobals,params.
    42   νtmpr,addr1,addr2 in
     39  ∀globals.register → register → register → list register →
     40  list (joint_seq ERTL globals) ≝
     41  λglobals.
     42  λtmpr,addr1,addr2,params.
    4343  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
    4444  [ (ertl_frame_size tmpr : joint_seq ??) ;
     
    5252
    5353definition get_params ≝
    54   λglobals,params.
     54  λglobals,tmpr,addr1,addr2,params.
    5555  let n ≝ min (length … params) (length … RegisterParams) in
    5656  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
    57   get_params_hdw globals hdw_params @@ get_params_stack … stack_params.
     57  get_params_hdw globals hdw_params @ get_params_stack … tmpr addr1 addr2 stack_params.
    5858
    5959definition save_return :
     
    130130
    131131definition prologue :
    132   ∀globals.list register → register → register → list (register×Register) →
     132  ∀globals.list register → register → register → register → register → register →
     133  list (register×Register) →
    133134  bind_new register (list (joint_seq ERTL globals)) ≝
    134   λglobals,params,sral,srah,sregs.
     135  λglobals,params,sral,srah,tmpr,addr1,addr2,sregs.
    135136  [ (ertl_new_frame : joint_seq ??) ;
    136137    POP … sral ;
    137138    POP … srah
    138   ] @@ save_hdws … sregs @@ get_params … params.
     139  ] @ save_hdws … sregs @ get_params … tmpr addr1 addr2 params.
    139140
    140141definition set_params_hdw :
     
    221222  match s return λ_.bind_step_block ?? with
    222223  [ step_seq s ⇒
    223     match s return λ_.bind_step_block ?? with
    224     [ PUSH _ ⇒ bret … [ ] (*CSC: XXXX should not be in the syntax *)
    225     | POP _ ⇒ bret … [ ] (*CSC: XXXX should not be in the syntax *)
    226     | MOVE rs ⇒ bret … [PSD (\fst rs) ← \snd rs]
     224    bret … match s return λ_.step_block ?? with
     225    [ PUSH _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
     226    | POP _ ⇒ [ ] (*CSC: XXXX should not be in the syntax *)
     227    | MOVE rs ⇒ [PSD (\fst rs) ← \snd rs]
    227228    | ADDRESS x prf r1 r2 ⇒
    228       bret … [ADDRESS ERTL ? x prf r1 r2]
     229      [ADDRESS ERTL ? x prf r1 r2]
    229230    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
    230       bret … [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
     231      [OPACCS ERTL ? op destr1 destr2 srcr1 srcr2]
    231232    | OP1 op1 destr srcr ⇒
    232       bret … [OP1 ERTL ? op1 destr srcr]
     233      [OP1 ERTL ? op1 destr srcr]
    233234    | OP2 op2 destr srcr1 srcr2 ⇒
    234       bret … [OP2 ERTL ? op2 destr srcr1 srcr2]
     235      [OP2 ERTL ? op2 destr srcr1 srcr2]
    235236    | CLEAR_CARRY ⇒
    236       bret … [CLEAR_CARRY ??]
     237      [CLEAR_CARRY ??]
    237238    | SET_CARRY ⇒
    238       bret … [SET_CARRY ??]
     239      [SET_CARRY ??]
    239240    | LOAD destr addr1 addr2 ⇒
    240       bret … [LOAD ERTL ? destr addr1 addr2]
     241      [LOAD ERTL ? destr addr1 addr2]
    241242    | STORE addr1 addr2 srcr ⇒
    242       bret … [STORE ERTL ? addr1 addr2 srcr]
     243      [STORE ERTL ? addr1 addr2 srcr]
    243244    | COMMENT msg ⇒
    244       bret … [COMMENT … msg]
     245      [COMMENT … msg]
    245246    | extension_seq ext ⇒
    246       match ext return λ_.bind_step_block ?? with
     247      match ext return λ_.step_block ?? with
    247248      [ rtl_stack_address addr1 addr2 ⇒
    248         bret … [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
     249        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
    249250      ]
    250251    ]
     
    273274definition allocate_regs :
    274275  ∀X : Type[0].
    275   (register → register → list (register×Register) → bind_new register X) →
     276  (list (register×Register) → bind_new register X) →
    276277  bind_new register X ≝
    277278  λX,f.
    278   νral,rah in
    279279  let allocate_regs_internal ≝
    280280    λacc : bind_new register (list (register × Register)).
     
    283283    νr' in return (〈r', r〉 :: tl) in
    284284  ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSaved ;
    285   f ral rah to_save.
     285  f to_save.
    286286
    287287definition translate_data :
    288288 ∀globals.joint_closed_internal_function RTL globals →
    289  bind_new register (b_graph_translate_data RTL ERTL globals)
     289 bound_b_graph_translate_data RTL ERTL globals
    290290λglobals,def.
    291291let params ≝ joint_if_params … def in
    292292let new_stacksize ≝
    293293  joint_if_stacksize … def + (|params| - |RegisterParams|) in
    294 allocate_regs …
    295   (λral,rah,to_save.
    296     ! prologue ← prologue globals params ral rah to_save ;
     294allocate_regs ?
     295  (λto_save.
     296    νral,rah,tmpr,addr1,addr2 in
     297    ! prologue ← prologue globals params ral rah tmpr addr1 addr2 to_save ;
    297298    return mk_b_graph_translate_data RTL ERTL globals
    298299    (* init_ret ≝ *) it
     
    300301    (* init_stack_size ≝ *) new_stacksize
    301302    (* added_prologue ≝ *) prologue
     303    (* new_regs ≝ *) (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save)
    302304    (* f_step ≝ *) (translate_step globals)
    303305    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save)
    304     ???).
     306    ????).
    305307@hide_prf
    306 [ #l #c % ]
    307 #l *
     308[1,2: cases daemon (* TODO *)
     309| #l #c %
     310| #l * [ #c' | #f #args #dest | #a #ltrue | #s ] #c whd
     311  [2: #r1 #r2 ] whd #l' #EQ destruct try %
     312  cases s in EQ; whd in match ensure_step_block; normalize nodelta
     313  try #a try #b try #c try #d try #e try #f destruct
     314  cases a in b; #a1 #a2 normalize nodelta #EQ destruct
     315| #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 %
     316]
     317(* #l *
    308318[ #l whd %{I} %{I} %1 %
    309319| whd %{I} cases (epilogue ?????) @All_mp #s #EQ whd >EQ %
     
    320330  try (%{I} %{I} #l %)
    321331  cases a -a #a #b whd %{I} % [ %{I} ] #l %
    322 ]
     332]*)
    323333qed.
    324334
  • src/joint/TranslateUtils.ma

    r2723 r2806  
    355355*)
    356356
    357 definition partial_partition : ∀X.∀Y : DeqSet.(X → option (list Y)) → Prop ≝
    358 λX,Y,f.
    359 (∀x.opt_All … (λys.bool_to_Prop (uniqueb … ys)) (f x)) ∧
    360 (∀x1,x2.
    361   opt_All …
    362     (λys1.
    363       opt_All …
    364       (λys2.
    365         ∀y.y ∈ ys1 → y ∈ ys2 → x1 = x2)
    366       (f x2))
    367     (f x1)).
    368 
    369357lemma opt_All_intro : ∀X,P,o.
    370358(∀x.o = Some ? x → P x) → opt_All X P o. #X #P * [//] #x #H @H % qed.
     
    385373@hide_prf cases pt -pt #pt whd in ⊢ (?%→?); #H % #G >G in H; * qed.
    386374*)
     375
     376let rec bind_new_P' R X (P : list R → X → Prop) (m : bind_new R X) on m : Prop ≝
     377match m with
     378[ bret x ⇒ P [ ] x
     379| bnew f ⇒
     380  ∀r.bind_new_P' R X (λl.P (l @ [r])) (f r)
     381].
     382
     383definition step_registers :  ∀p : uns_params.∀globals.
     384  joint_step p globals → list register ≝
     385λp,globals,s.get_used_registers_from_step … (functs … p) s.
     386
     387definition step_forall_registers : ∀p : uns_params.∀globals.
     388  (register → Prop) → joint_step p globals → Prop ≝
     389λp,globals,P,s.All … P (step_registers … s).
     390
     391definition fin_step_registers :  ∀p : uns_params.
     392  joint_fin_step p → list register ≝
     393λp,s.match s with [ TAILCALL _ _ r ⇒ f_call_args … (functs … p) r | _ ⇒ [ ] ].
     394
     395definition fin_step_forall_registers : ∀p : uns_params.
     396  (register → Prop) → joint_fin_step p → Prop ≝
     397λp,P,s.All … P (fin_step_registers … s).
     398
     399definition fin_step_forall_labels : ∀p : uns_params.
     400  (label → Prop) → joint_fin_step p → Prop ≝
     401λp,P,s.All … P (fin_step_labels … s).
     402
     403definition step_labels_and_registers_in : ∀p : uns_params.∀globals.
     404  list label → list register → joint_step p globals → Prop ≝
     405λp,g,allowed_l,allowed_r,s.
     406  step_forall_labels … (In ? allowed_l) s ∧
     407  step_forall_registers … (In ? allowed_r) s.
     408
     409definition fin_step_labels_and_registers_in : ∀p : uns_params.
     410  list label → list register → joint_fin_step p → Prop ≝
     411λp,allowed_l,allowed_r,s.
     412  fin_step_forall_labels … (In ? allowed_l) s ∧
     413  fin_step_forall_registers … (In ? allowed_r) s.
    387414
    388415record b_graph_translate_data
     
    393420; init_stack_size : ℕ
    394421; added_prologue : list (joint_seq dst globals)
     422; new_regs : list register (* new registers added globally *)
    395423; f_step : label → joint_step src globals → bind_step_block dst globals
    396424; f_fin : label → joint_fin_step src → bind_fin_block dst globals
    397 ; good_f_step_good :
    398   ∀l,s.bind_new_P ??
    399     (λblock.let 〈pref, op, post〉 ≝ block in
     425; good_f_step :
     426  ∀l,s.bind_new_P' ??
     427    (λlocal_new_regs,block.let 〈pref, op, post〉 ≝ block in
     428       ∀l.
     429       let allowed_labels ≝ l :: step_labels … s in
     430       let allowed_registers ≝ new_regs @ local_new_regs @ step_registers … s in
    400431       All (label → joint_seq ??)
    401          (λs'.∀l.step_forall_labels … (In ? (l :: step_labels … s)) (s' l))
     432         (λs'.step_labels_and_registers_in … allowed_labels allowed_registers (step_seq dst globals (s' l)))
    402433         pref ∧
    403        (∀l.step_forall_labels … (In ? (l :: step_labels … s)) (op l)) ∧
    404        All (joint_seq ??) (step_forall_labels … (In ? (step_labels … s))) post)
     434       step_labels_and_registers_in … allowed_labels allowed_registers (op l) ∧
     435       All (joint_seq ??) (step_labels_and_registers_in … allowed_labels allowed_registers) post)
    405436    (f_step l s)
    406437; good_f_fin :
    407   ∀l,s.bind_new_P ??
    408     (λblock.let 〈pref, op〉 ≝ block in
    409        All (joint_seq ??) (step_forall_labels … (In ? (fin_step_labels … s))) pref ∧
    410        All … (In ? (fin_step_labels … s)) (fin_step_labels … op))
     438  ∀l,s.bind_new_P' ??
     439    (λlocal_new_regs,block.let 〈pref, op〉 ≝ block in
     440       let allowed_labels ≝ l :: fin_step_labels … s in
     441       let allowed_registers ≝ new_regs @ local_new_regs @ fin_step_registers … s in
     442       All (joint_seq ??) (λs.step_labels_and_registers_in … allowed_labels allowed_registers s) pref ∧
     443       fin_step_labels_and_registers_in … allowed_labels allowed_registers op)
    411444    (f_fin l s)
    412445; f_step_on_cost :
    413446  ∀l,c.f_step l (COST_LABEL … c) =
    414447    bret ? (step_block ??) 〈[ ], λ_.COST_LABEL dst globals c, [ ]〉
     448; cost_in_f_step :
     449  ∀l,s,c.
     450  bind_new_P ??
     451    (λblock.∀l'.\snd (\fst block) l' = COST_LABEL dst globals c →
     452       s = COST_LABEL … c) (f_step l s)
    415453}.
     454
     455definition bound_b_graph_translate_data ≝
     456λsrc,dst,globals.
     457Σd : bind_new register (b_graph_translate_data src dst globals).
     458bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d.
     459
     460unification hint 0 ≔ src,dst,globals ⊢
     461bound_b_graph_translate_data src dst globals ≡
     462Sig (bind_new register (b_graph_translate_data src dst globals)) (λd.bind_new_P' ?? (λregs,data.new_regs ??? data = regs) d).
    416463
    417464definition get_first_costlabel : ∀p,g.
     
    436483qed.
    437484
     485definition partial_partition : ∀X.∀Y : DeqSet.(X → list Y) → Prop ≝
     486λX,Y,f.
     487(∀x.bool_to_Prop (uniqueb … (f x))) ∧
     488(∀x1,x2,y.y ∈ f x1 → y ∈ f x2 → x1 = x2).
     489
    438490record b_graph_translate_props
    439491  (src_g_pars, dst_g_pars : graph_params)
    440492  (globals: list ident)
    441493  (data : b_graph_translate_data src_g_pars dst_g_pars globals)
    442   (data_regs : list register)
    443494  (def_in : joint_closed_internal_function src_g_pars globals)
    444495  (def_out : joint_closed_internal_function dst_g_pars globals)
    445   (f_lbls : label → option (list label))
    446   (f_regs : label → option (list register)) : Prop ≝
     496  (f_lbls : label → list label)
     497  (f_regs : label → list register) : Prop ≝
    447498{ res_def_out_eq :
    448499           joint_if_result … def_out = init_ret … data
     
    456507; partition_regs : partial_partition … f_regs
    457508; freshness_lbls :
    458   (∀l.opt_All … (All …
     509  (∀l.All …
    459510    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
    460            fresh_for_univ … lbl (joint_if_luniverse … def_out))) (f_lbls l))
     511           fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls l))
    461512; freshness_regs :
    462   (∀l.opt_All … (All …
     513  (∀l.All …
    463514    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
    464            fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l))
     515           fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs l))
    465516; freshness_data_regs :
    466517  All … (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
    467                fresh_for_univ … reg (joint_if_runiverse … def_out)) data_regs
    468 ; data_regs_disjoint : ∀l.opt_All … (λregs.∀r.r ∈ regs → r ∈ data_regs → False) (f_regs l)
     518               fresh_for_univ … reg (joint_if_runiverse … def_out)) (new_regs … data)
     519; data_regs_disjoint : ∀l,r.r ∈ f_regs l → r ∈ new_regs … data → False
    469520; multi_fetch_ok :
    470521  ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s →
    471   ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧
     522  let lbls ≝ f_lbls l in let regs ≝ f_regs l in
    472523  match s with
    473524  [ sequential s' nxt ⇒
     
    501552  ∀globals: list ident.
    502553  (* initialization info *)
    503   ∀data : bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals).
     554  ∀data : bound_b_graph_translate_data src_g_pars dst_g_pars globals.
    504555  (* source function *)
    505556  ∀def_in : joint_closed_internal_function src_g_pars globals.
     
    507558  Σdef_out : joint_closed_internal_function dst_g_pars globals.
    508559  ∃data',regs,f_lbls,f_regs.
    509     bind_new_instantiates … data' data regs ∧
    510     b_graph_translate_props … data' regs def_in def_out f_lbls f_regs
     560    bind_new_instantiates ?? data' data regs ∧ (* so new_regs … data = regs *)
     561    b_graph_translate_props … data' def_in def_out f_lbls f_regs
    511562   ≝
    512563  λsrc_g_pars,dst_g_pars,globals,data,def.
     
    545596  (* initialization *)
    546597  (∀globals.joint_closed_internal_function src_g_pars globals →
    547     bind_new register (b_graph_translate_data src_g_pars dst_g_pars globals)) →
     598    bound_b_graph_translate_data src_g_pars dst_g_pars globals) →
    548599  joint_program src_g_pars →
    549600  joint_program dst_g_pars ≝
Note: See TracChangeset for help on using the changeset viewer.