Changeset 2942


Ignore:
Timestamp:
Mar 23, 2013, 1:37:22 AM (4 years ago)
Author:
sacerdot
Message:

Many changes:

  1. Coloured graphs are now specified in terms of livebefore
  2. Type of livebefore changed so that it is now a valuation transformer
  3. Several axioms can now be inhabited in ERTLptrToLTLProof

Problems:
ERTLtoERTLptrOK is broken beyond my understanding. This pass should have
been unaffected by the changes, but it is not so. Why?

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2940 r2942  
    862862         (inr ident … 〈c_ptr1,c_ptr2〉)
    863863         (sigma_state_pc prog f_lbls f_regs st2))
    864         [
    865        
    866        generalize in match (block_of_call ?????);
    867        
    868        %
     864         
     865         [ whd in ⊢ (??%%); normalize nodelta
     866         XXX
     867         %
    869868  |*:  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
    870869      @if_elim change with (pc_block(pc … st2)) in match (pc_block ?);
  • src/ERTLptr/ERTLptrToLTL.ma

    r2888 r2942  
    320320
    321321definition translate_step:
    322   ∀globals.nat → ∀after : valuation register_lattice.
    323   coloured_graph after
     322  ∀globals,fn.nat → ∀after : valuation register_lattice.
     323  coloured_graph (livebefore globals fn after)
    324324  ℕ → label → joint_step ERTLptr globals → bind_step_block LTL globals ≝
    325   λglobals,localss,after,grph,stack_sz,lbl,s.
     325  λglobals,fn,localss,after,grph,stack_sz,lbl,s.
    326326  bret … (
    327327  let lookup ≝ λr.colouring … grph (inl … r) in
     
    440440    (* added_prologue ≝ *) [ ]
    441441    (* new_regs ≝ *) [ ]
    442     (* f_step ≝ *) (translate_step ? (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz)
     442    (* f_step ≝ *) (translate_step ? int_fun (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz)
    443443    (* f_fin ≝ *) (translate_fin_step globals)
    444444    ????).
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2940 r2942  
    66include "common/AssocList.ma".
    77
    8 
    9 
    108(* Inefficient, replace with Trie lookup *)
    119definition lookup_stack_cost ≝
     
    2624 
    2725axiom to_be_cleared_sb : 
    28 after : valuation register_lattice. coloured_graph after → clear_sb_type.
     26live_before : valuation register_lattice. coloured_graph live_before → clear_sb_type.
    2927
    3028definition local_clear_fb_type ≝ vertex → bool.
     
    3230
    3331axiom to_be_cleared_fb :
    34 after : valuation register_lattice.clear_fb_type.
     32live_before : valuation register_lattice.clear_fb_type.
    3533
    3634axiom sigma_fb_state:
     
    3937
    4038axiom acc_is_dead : ∀fix_comp.∀prog : ertlptr_program.
    41 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
    42 ∀l.
    43 let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
    44 ¬ lives (inr ? ? RegisterA) (livebefore  … fn l after).
     39 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog). ∀l.
     40 let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in
     41  ¬ lives (inr ? ? RegisterA) (livebefore  … fn after l).
    4542
    4643axiom dead_registers_in_dead :
     
    4946 ∀fn : joint_closed_internal_function ERTLptr (prog_var_names … prog).
    5047 ∀l.
    51  let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     48 let after ≝ analyse_liveness fix_comp (prog_var_names … prog) fn in
    5249 let coloured_graph ≝ build … fn after in
    5350 ∀R : Register.
    54   ¬ lives (inr ? ? R) (livebefore  … fn l after) →
    55    to_be_cleared_sb after coloured_graph l R.
     51  ¬ lives (inr ? ? R) (livebefore  … fn after l) →
     52   to_be_cleared_sb coloured_graph l R.
    5653
    5754axiom sigma_sb_state:
     
    6966 fixpoint_computer → ertlptr_program →
    7067  state_pc ERTLptr_semantics → state_pc ERTLptr_semantics ≝
    71  λfix_comp,prog,st. 
     68 λfix_comp,prog,st.
    7269 let ge ≝ globalenv_noinit … prog in
    7370 let globals ≝ prog_var_names … prog in
     
    7572  [ OK y ⇒
    7673     let pt ≝ point_of_pc ERTLptr_semantics (pc ? st) in
    77      let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
    78      mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb after pt) st) (pc … st) 
     74     let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) (\snd y)) in
     75     let before ≝ livebefore … (\snd y) after in
     76     mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb before pt) st) (pc … st) 
    7977      (last_pop … st)
    8078  | Error e ⇒ dummy_state_pc
     
    9593     let coloured_graph ≝ build … (\snd y) after in
    9694     mk_state_pc ? (sigma_sb_state prog
    97                        (to_be_cleared_sb after coloured_graph pt) st) (pc … st) 
     95                       (to_be_cleared_sb coloured_graph pt) st) (pc … st) 
    9896                   (sigma_stored_pc ERTLptr_semantics LTL_semantics
    9997                                    prog f_lbls (last_pop … st))
     
    107105∃f,fn.fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
    108106let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
     107let before ≝ livebefore … fn after in
    109108let coloured_graph ≝ build … fn after in
    110 (sigma_fb_state prog (to_be_cleared_fb after pc) st1) =
    111 (sigma_sb_state prog (to_be_cleared_sb after coloured_graph pc) st2).
     109(sigma_fb_state prog (to_be_cleared_fb before pc) st1) =
     110(sigma_sb_state prog (to_be_cleared_sb coloured_graph pc) st2).
    112111
    113112axiom write_decision :
     
    250249∀bv.
    251250∀r : register.R st1 st2 →
    252 lives (inl ? ? r) (livebefore  … fn (point_of_pc ERTLptr_semantics (pc … st1)) after) →
     251lives (inl ? ? r) (livebefore  … fn after (point_of_pc ERTLptr_semantics (pc … st1))) →
    253252ps_reg_retrieve (regs … st1) r = return bv →
    254253∃bv'.bv = sigma_beval prog f_lbls bv' ∧
    255 read_arg_decision (colouring after (colour (prog_var_names … prog) fn after)
    256                                             (inl register Register r))
    257                               st2 = bv'.
     254 read_arg_decision
     255  (colouring … (colour (prog_var_names … prog) fn after)
     256   (inl register Register r))
     257  st2 = bv'.
    258258                             
    259259axiom set_member_empty :∀A.∀DEC.∀a.¬set_member A DEC a (set_empty …).   
     
    276276let after ≝ (analyse_liveness fix_comp (prog_var_names … prog) fn) in
    277277eliminable ? (after l) stmt = false →
    278 lives (inl ? ? r)  (livebefore  … fn l after).
     278lives (inl ? ? r)  (livebefore  … fn after l).
    279279#fix_comp #prog #fn #l *
    280280[ * [#c|* [#c_id | #c_ptr] #args #dest | #a #lbl | *
     
    317317%{(refl …)} %{(refl …)} %
    318318qed.
    319 (*
    320 axiom dead_is_to_be_clear :
    321 *)
    322319
    323320(* Cut&paste da un altro file con nome split_on_last_append, unificare*)
     
    347344
    348345axiom sigma_fb_state_insensitive_to_dead_reg:
    349  ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
    350  ∀r: register.
    351  let live ≝
    352   analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
    353  in
    354   set_member (identifier RegisterTag) (eq_identifier RegisterTag) r
    355    (\fst  (livebefore … fn l live)) = false →
     346 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label.
     347 ∀r: register. ∀before.
     348  set_member … (eq_identifier RegisterTag) r (\fst  (before l)) = false →
    356349  sigma_fb_state prog
    357    (to_be_cleared_fb live l)
     350   (to_be_cleared_fb before l)
    358351   (set_regs ERTLptr_semantics
    359352    〈reg_store r bv (\fst  (regs ERTLptr_semantics st)),
    360353    \snd  (regs ERTLptr_semantics st)〉 st)
    361   = sigma_fb_state prog (to_be_cleared_fb live l) st.
     354  = sigma_fb_state prog (to_be_cleared_fb before l) st.
    362355
    363356axiom sigma_fb_state_insensitive_to_dead_Reg:
    364  ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
    365  ∀r: Register.
    366  let live ≝
    367   analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
    368  in
    369   set_member Register eq_Register r (\snd  (livebefore … fn l live)) = false →
     357 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label.
     358 ∀r: Register. ∀before.
     359  set_member … eq_Register r (\snd  (before l)) = false →
    370360  sigma_fb_state prog
    371    (to_be_cleared_fb live l)
     361   (to_be_cleared_fb before l)
    372362   (set_regs ERTLptr_semantics
    373363     〈\fst  (regs ERTLptr_semantics st),
    374364      hwreg_store r bv (\snd  (regs ERTLptr_semantics st))〉
    375365      st)
    376   = sigma_fb_state prog (to_be_cleared_fb live l) st.
     366  = sigma_fb_state prog (to_be_cleared_fb before l) st.
    377367
    378368axiom sigma_fb_state_insensitive_to_dead_carry:
    379  ∀fix_comp,prog,fn,bv. ∀st: state ERTLptr_semantics. ∀l:label.
    380  let live ≝
    381   analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog) fn
    382  in
    383   set_member Register eq_Register RegisterCarry (\snd (livebefore … fn l live)) = false →
    384    sigma_fb_state prog (to_be_cleared_fb live l) (set_carry ERTLptr_semantics bv st) =
    385    sigma_fb_state prog (to_be_cleared_fb live l) st.
     369 ∀prog,bv. ∀st: state ERTLptr_semantics. ∀l:label. ∀before.
     370  set_member Register eq_Register RegisterCarry (\snd (before l)) = false →
     371   sigma_fb_state prog (to_be_cleared_fb before l) (set_carry ERTLptr_semantics bv st) =
     372   sigma_fb_state prog (to_be_cleared_fb before l) st.
    386373
    387374lemma split_orb_false: ∀a,b:bool. orb a b = false → a = false ∧ b = false.
     
    400387
    401388lemma eliminable_step_to_eq_livebefore_liveafter:
    402  ∀fix_comp,colour,prog,fn.
    403  let p_in ≝
    404    mk_prog_params ERTLptr_semantics prog
    405    (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
     389 ∀prog,stackcost,fn.
     390 let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in
    406391 ∀st1: joint_abstract_status p_in.
    407392 ∀stms: joint_seq ERTLptr_semantics (prog_var_names … prog). ∀next.
    408393 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
    409394 stmt_at p_in ? (joint_if_code p_in … fn) pt = return (sequential … stms next) →
    410  let liveafter ≝ analyse_liveness fix_comp (globals p_in) fn in
     395 ∀liveafter.
    411396 eliminable_step (globals p_in) (liveafter (point_of_pc ERTLptr_semantics (pc … st1))) stms = true →
    412   livebefore … fn pt liveafter = liveafter pt.
    413  #fix_comp #colour #prog #fn #st1 #stms #next #stmt_at #Helim
     397  livebefore … fn liveafter pt = liveafter pt.
     398 #prog #stackcost #fn #st1 #stms #next #stmt_at #liveafter #Helim
    414399 whd in ⊢ (??%?); whd in stmt_at:(??%?); cases (lookup ????) in stmt_at;
    415400 normalize nodelta try (#abs whd in abs:(??%%); destruct (abs) @I)
     
    420405lemma sigma_fb_state_insensitive_to_eliminable:
    421406 ∀fix_comp: fixpoint_computer.
    422  ∀colour: coloured_graph_computer.
    423407 ∀prog: ertlptr_program.
    424  let p_in ≝
    425    mk_prog_params ERTLptr_semantics prog
    426    (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog)))) in
     408 ∀stackcost.
     409 let p_in ≝ mk_prog_params ERTLptr_semantics prog stackcost in
    427410 ∀f,fn.
     411 ∀after: valuation ?.
     412 let before ≝ livebefore … fn after in
    428413 ∀st1 : joint_abstract_status p_in.
    429414 let pt ≝ point_of_pc ERTLptr_semantics (pc ? st1) in
     
    434419   (prog_var_names (joint_function ERTLptr_semantics) ℕ prog)
    435420   (ev_genv
    436     (mk_prog_params ERTLptr_semantics prog
    437      (lookup_stack_cost (\snd  (\fst  (ertlptr_to_ltl fix_comp colour prog))))))
     421    (mk_prog_params ERTLptr_semantics prog stackcost))
    438422   f stms (st_no_pc … st1)
    439423   =return st1_no_pc.
    440424 ∀Heliminable:
    441425   eliminable_step (globals p_in)
    442    (analyse_liveness fix_comp (globals p_in) fn
    443     (point_of_pc ERTLptr_semantics (pc p_in st1))) stms
    444    =true.
    445  (sigma_fb_state prog
    446   (to_be_cleared_fb
    447    (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog)
    448     fn) pt)
    449   st1_no_pc
    450   =sigma_fb_state prog
    451    (to_be_cleared_fb
    452     (analyse_liveness fix_comp (prog_var_names (joint_function ERTLptr) ℕ prog)
    453      fn) pt)
    454    (st_no_pc … st1)).
    455 #fix_comp #colour #prog letin p_in ≝ (mk_prog_params ???) #f #fn
     426    (after (point_of_pc ERTLptr_semantics (pc p_in st1))) stms =true.
     427 sigma_fb_state prog (to_be_cleared_fb before pt) st1_no_pc =
     428  sigma_fb_state prog (to_be_cleared_fb before pt) (st_no_pc … st1).
     429#fix_comp #prog #stackcost letin p_in ≝ (mk_prog_params ???) #f #fn #after
    456430#st1 #st1' #stms #next #stmt_at #Heval #Helim
    457 lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at Helim)
     431lapply (eliminable_step_to_eq_livebefore_liveafter … stmt_at Helim)
    458432#EQ_livebefore_after -next
    459433cases stms in Heval Helim;
     
    596570          (read_arg_decision
    597571              (colouring
    598                   (analyse_liveness fix_comp (globals prog_pars_in) fn)
     572                 
    599573                  (colour (globals prog_pars_in) fn
    600574                  (analyse_liveness fix_comp (globals prog_pars_in) fn))
     
    614588                     [2,4: @dead_registers_in_dead @acc_is_dead ]
    615589                     whd >point_of_pc_of_point
     590                     letin after ≝ (analyse_liveness fix_comp … fn)
     591                     letin before ≝ (livebefore … fn after)
    616592                     [ cut
    617                         (analyse_liveness fix_comp … fn ltrue =
    618                           analyse_liveness fix_comp … fn
    619                           (point_of_pc ERTLptr_semantics (pc … st1)))
     593                        (before ltrue =
     594                          before (point_of_pc ERTLptr_semantics (pc … st1)))
    620595                       [ cases daemon (*CSC: Genuine proof obligation! *)
    621596                       | #Hext ]
    622597                     |  cut
    623                         (analyse_liveness fix_comp … fn lfalse =
    624                           analyse_liveness fix_comp … fn
    625                           (point_of_pc ERTLptr_semantics (pc … st1)))
     598                        (before lfalse =
     599                          before (point_of_pc ERTLptr_semantics (pc … st1)))
    626600                       [ cases daemon (*CSC: Genuine proof obligation! *)
    627601                       | #Hext ]]
     
    675649    #EQst1st2 #_ #_
    676650    (* CSC: END *)
    677     <EQst1st2 whd in EQst1_no_pc:(??%%); whd in match (st_no_pc ??);
     651    lapply (sigma_fb_state_insensitive_to_eliminable fix_comp … EQstmt … Heval_seq_no_pc Heliminable)
     652    XXXX
     653    <EQst1st2
     654   
     655    lapply Heval_seq_no_pc; whd in match eval_seq_no_pc; normalize nodelta
     656   
     657     whd in Heval_seq_no_pc:(??%%); whd in match (st_no_pc ??);
    678658
    679659
  • src/ERTLptr/Interference.ma

    r2845 r2942  
    88   prop_colouring 2 and 3 together say that spilled_no is the number of spilled
    99   registers *)
    10 (* Wilmer: the generation of the destruct principle diverges;
    11    Ctr-C make the file pass *)
    12 record coloured_graph (after: valuation register_lattice): Type[1] ≝
     10record coloured_graph (before: valuation register_lattice): Type[1] ≝
    1311{ colouring: vertex → decision
    1412; spilled_no: nat
    1513; prop_colouring: ∀l. ∀v1, v2: vertex.v1 ≠v2 →
    16   lives v1 (after l) → lives v2 (after l) → colouring v1 ≠ colouring v2
     14  lives v1 (before l) → lives v2 (before l) → colouring v1 ≠ colouring v2
    1715; prop_spilled_no: (*CSC: the exist-guarded premise is just to make the proof more general *)
    18    ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (after l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no
     16   ∀v1:vertex. (∃l. bool_to_Prop (lives v1 (before l))) → ∀i. colouring v1 = decision_spill i → i < spilled_no
    1917}.
    2018
    2119definition coloured_graph_computer ≝
    2220 ∀globals.
    23   joint_internal_function ERTLptr globals →
    24    ∀valuation.
    25     coloured_graph valuation.
     21  ∀fn:joint_internal_function ERTLptr globals.
     22   ∀liveafter.
     23    coloured_graph (livebefore globals fn liveafter).
  • src/ERTLptr/liveness.ma

    r2887 r2942  
    232232    rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt).
    233233
    234 definition livebefore ≝
     234definition livebefore:
     235  ∀globals: list ident.
     236   joint_internal_function ERTLptr globals →
     237     valuation register_lattice → valuation register_lattice
     238
    235239  λglobals: list ident.
    236240  λint_fun: joint_internal_function ERTLptr globals.
     241  λliveafter: valuation register_lattice.
    237242  λlabel.
    238   λliveafter: valuation register_lattice.
    239243  match lookup ?? (joint_if_code … int_fun) label with
    240244  [ None      ⇒ rl_bottom
     
    251255  | Some stmt ⇒
    252256    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
    253       (livebefore globals int_fun successor liveafter)
     257      (livebefore globals int_fun liveafter successor)
    254258  ].
    255259
Note: See TracChangeset for help on using the changeset viewer.