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/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 ?);
Note: See TracChangeset for help on using the changeset viewer.