Changeset 2940


Ignore:
Timestamp:
Mar 22, 2013, 7:16:17 PM (4 years ago)
Author:
sacerdot
Message:
  1. StatusSimulationHelper? changed to allow to use status_rel that depends on the pc (necessary for ERTLptrToLTL)
  2. partial repairing of ERTLToERTLptrOK.ma, still in progress
  3. some progress in ERTLptrToLTLProof, but: a) some axioms were wrong, once fixed we now see some proof obligations

related to liveness analysis. Example: the variables live before and
after a COND must be the same. I have put daemons for the time being.

b) I strongly suspect that Interference should be changed to use livebefore,

in the correctness conditions (now it uses liveafter, the two sets
are probably equivalent for correct programs, but one is simpler to use:
which one?)

c) to_be_cleared_* must consult livebefore, but it is now passed liveafter.

Passing liveafter is necessary to typechek the graph, unless we do
b) first. Passing only the set computed by livebefore would be so much
better.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2898 r2940  
    165165definition state_rel ≝ λprog : ertl_program.λf_lbls.
    166166λf_regs : (block → label → list register).
    167 λbl,st1,st2.∃f,fn.
     167λbl.λ_:label.λst1,st2.∃f,fn.
    168168fetch_internal_function ? (globalenv_noinit … prog) bl = return 〈f,fn〉 ∧
    169169let added ≝ added_registers ERTL (prog_var_names … prog) fn (f_regs bl) in
     
    236236  whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind
    237237  normalize nodelta #H @('bind_inversion H) -H #st1_no_pc' #EQst1_no_pc'
    238   whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (%→?); #EQ destruct(EQ)
     238  whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     239  whd in match (succ_pc ???); normalize nodelta
     240  whd in match (set_no_pc ???); normalize nodelta
     241  whd in ⊢ (%→?); #EQ destruct(EQ)
    239242  whd in match sigma_state_pc in EQst1_no_pc'; normalize  nodelta in EQst1_no_pc';
    240243  cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
     
    838841       >EQcall in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta
    839842       >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
    840        >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); %
     843       >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); normalize nodelta
     844       
     845       [cut (block_of_call
     846        (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
     847        (globals
     848         (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size))
     849        (ev_genv
     850         (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size))
     851        (inr ident … 〈c_ptr1,c_ptr2〉)
     852        (set_regs ERTL_state
     853         〈add RegisterTag beval (\fst  (regs ERTLptr_semantics st2)) r
     854          (\snd  (beval_pair_of_pc
     855                       (pc_of_point ERTLptr_semantics
     856                        (pc_block (pc ERTLptr_semantics st2)) mid1))),
     857         \snd  (regs ERTLptr_semantics st2)〉
     858         st_no_pc_pre_call) =
     859         block_of_call (mk_prog_params ERTL_semantics prog stack_size)
     860         (globals (mk_prog_params ERTL_semantics prog stack_size))
     861         (ev_genv (mk_prog_params ERTL_semantics prog stack_size))
     862         (inr ident … 〈c_ptr1,c_ptr2〉)
     863         (sigma_state_pc prog f_lbls f_regs st2))
     864        [
     865       
     866       generalize in match (block_of_call ?????);
     867       
     868       %
    841869  |*:  whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
    842870      @if_elim change with (pc_block(pc … st2)) in match (pc_block ?);
  • src/ERTLptr/ERTLptrToLTLProof.ma

    r2938 r2940  
    530530qed.
    531531
     532axiom to_be_cleared_sb_respects_equal_valuations:
     533 ∀live,coloured,l1,l2.
     534  live l1 = live l2 →
     535   to_be_cleared_sb live coloured l1 = to_be_cleared_sb live coloured l2.
     536
     537axiom to_be_cleared_fb_respects_equal_valuations:
     538 ∀live,l1,l2.
     539  live l1 = live l2 →
     540   to_be_cleared_fb live l1 = to_be_cleared_fb live l2.
     541
    532542lemma make_ERTLptr_To_LTL_good_state_relation :
    533543∀fix_comp,colour,prog.
     
    601611                     normalize nodelta #EQ cases(state_pc_eq … EQ) *
    602612                     #EQst1st2 #_ #_ whd %{f} %{fn} %{EQfn}
    603                      <(insensitive_to_be_cleared_sb … prog f_lbls f_regs … st2 …
    604                                           (point_of_pc ERTLptr_semantics (pc … st2)))
     613                     <(insensitive_to_be_cleared_sb prog … st2)
    605614                     [2,4: @dead_registers_in_dead @acc_is_dead ]
    606                      assumption
     615                     whd >point_of_pc_of_point
     616                     [ cut
     617                        (analyse_liveness fix_comp … fn ltrue =
     618                          analyse_liveness fix_comp … fn
     619                          (point_of_pc ERTLptr_semantics (pc … st1)))
     620                       [ cases daemon (*CSC: Genuine proof obligation! *)
     621                       | #Hext ]
     622                     |  cut
     623                        (analyse_liveness fix_comp … fn lfalse =
     624                          analyse_liveness fix_comp … fn
     625                          (point_of_pc ERTLptr_semantics (pc … st1)))
     626                       [ cases daemon (*CSC: Genuine proof obligation! *)
     627                       | #Hext ]]
     628                     >(to_be_cleared_sb_respects_equal_valuations …
     629                        (colour … fn …) … Hext) <EQst1st2
     630                     >(to_be_cleared_fb_respects_equal_valuations … Hext) %
    607631                 ]
    608632            |*: %
  • src/joint/StatusSimulationHelper.ma

    r2939 r2940  
    150150                                   (st_no_pc ? st2)
    151151            = return st2_pre_mid_no_pc ∧
    152             st_no_pc_rel (pc_block(pc … st1))
    153              (point_of_pc P_in … (pc … st1)) (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
     152            st_no_pc_rel (pc_block(pc … st1'))
     153             (point_of_pc P_in … (pc … st1')) (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
    154154            joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
    155155                                ((\snd (\fst blp)) mid)  = cl_jump ∧
     
    187187           repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
    188188              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
    189            st_no_pc_rel (pc_block (pc … st1))
    190             (point_of_pc P_in … (pc … st1))
     189           st_no_pc_rel (pc_block (pc … st1'))
     190            (point_of_pc P_in … (pc … st1'))
    191191            (st_no_pc … st1') st2_fin_no_pc
    192192      ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
     
    272272*)
    273273
     274(*
    274275(*CSC: Isn't this already proved somewhere else??? *)
    275276lemma point_of_pc_pc_of_point:
     
    279280     (pc_block (pc P_in st)) l) = l.
    280281 #P * //
    281 qed.
     282qed.*)
    282283
    283284lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
     
    298299∀a,ltrue,lfalse.
    299300st_rel st1 st2 →
    300     let cond ≝ (COND P_in ? a ltrue) in
    301  fetch_statement P_in …
    302   (globalenv_noinit ? prog) (pc … st1) =
    303     return 〈f, fn,  sequential … cond lfalse〉 →
    304  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
    305             st1 = return st1' →
     301 let cond ≝ (COND P_in ? a ltrue) in
     302  fetch_statement P_in …
     303   (globalenv_noinit ? prog) (pc … st1) =
     304     return 〈f, fn,  sequential … cond lfalse〉 →
     305 eval_state P_in (prog_var_names … ℕ prog)
     306  (ev_genv … prog_pars_in) st1 = return st1' →
    306307as_costed (joint_abstract_status prog_pars_in) st1' →
    307308∃ st2'. st_rel st1' st2' ∧
     
    349350[1,3: @(st_rel_def … goodR … f fn ?)
    350351      [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
    351       |2,5: >point_of_pc_pc_of_point assumption
     352      |2,5: assumption
    352353      |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
    353354      ]
     
    408409∀stmt,nxt.
    409410st_rel st1 st2 →
    410     let seq ≝ (step_seq P_in ? stmt) in
    411  fetch_statement P_in …
    412   (globalenv_noinit ? prog) (pc … st1) =
    413     return 〈f, fn,  sequential ?? seq nxt〉 →
     411 let seq ≝ (step_seq P_in ? stmt) in
     412  fetch_statement P_in …
     413   (globalenv_noinit ? prog) (pc … st1) =
     414     return 〈f, fn,  sequential ?? seq nxt〉 →
    414415 eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in)
    415             st1 = return st1' →
     416  st1 = return st1' →
    416417∃st2'. st_rel st1' st2' ∧           
    417418∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.           
Note: See TracChangeset for help on using the changeset viewer.