Changeset 2940 for src/joint


Ignore:
Timestamp:
Mar 22, 2013, 7:16:17 PM (7 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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.