Changeset 2470 for src/joint/Traces.ma
 Timestamp:
 Nov 15, 2012, 7:06:45 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/Traces.ma
r2457 r2470 5 5 { globals: list ident 6 6 ; sparams:> sem_params 7 ; exit: cpointer7 ; exit: program_counter 8 8 ; ev_genv: genv sparams globals 9 9 (* ; io_env : state sparams → ∀o:io_out.res (io_in o) *) 10 10 }. 11 12 axiom is_internal_function_of_program : 13 ∀p:params.joint_program p → ident → Prop. 14 15 axiom is_internal_function_of_program_ok : 16 ∀p.∀prog:joint_program p.∀i.is_internal_function ?? (globalenv_noinit ? prog) i → 17 is_internal_function_of_program p prog i. 11 12 13 (* move elsewhere *) 14 definition is_internal_function_of_program : 15 ∀A,B.program (λvars.fundef (A vars)) B → ident → Prop ≝ 16 λA,B,prog,i.∃ifd.In … (prog_funct ?? prog) 〈i, Internal ? ifd〉. 17 18 lemma opt_elim : ∀A.∀m : option A.∀P : option A → Prop. 19 (m = None ? → P (None ?)) → 20 (∀x.m = Some ? x → P (Some ? x)) → P m. 21 #A * [2: #x] #P #H1 #H2 22 [ @H2  @H1 ] % qed. 23 24 axiom find_funct_ptr_symbol_inversion: 25 ∀F,V,init. ∀p: program F V. 26 ∀id: ident. ∀b: block. ∀f: F ?. 27 find_symbol ? (globalenv ?? init p) id = Some ? b → 28 find_funct_ptr ? (globalenv ?? init p) b = Some ? f → 29 In … (prog_funct ?? p) 〈id, f〉. 30 31 lemma is_internal_function_of_program_ok : 32 ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i. 33 is_internal_function ?? (globalenv ?? init prog) i → 34 is_internal_function_of_program ?? prog i. 35 #A #B #init #prog #i whd in ⊢ (%→%); * #ifn 36 @(opt_elim … (find_symbol … i)) [#_ #ABS normalize in ABS; destruct(ABS) ] 37 #bl #EQbl >m_return_bind #EQfind %{ifn} 38 @(find_funct_ptr_symbol_inversion … EQbl EQfind) 39 qed. 18 40 19 41 record prog_params : Type[1] ≝ 20 42 { prog_spars : sem_params 21 43 ; prog : joint_program prog_spars 22 ; stack_sizes : (Σi.is_internal_function_of_program prog_sparsprog i) → ℕ44 ; stack_sizes : (Σi.is_internal_function_of_program ?? prog i) → ℕ 23 45 (* ; prog_io : state prog_spars → ∀o.res (io_in o) *) 24 46 }. … … 29 51 (* Invariant: a 1 block is unused in common/Globalenvs *) 30 52 let b ≝ mk_block Code (1) in 31 let ptr ≝ mk_p ointer b (mk_offset (bv_zero …))in53 let ptr ≝ mk_program_counter «b, refl …» one in 32 54 let p ≝ prog pars in 33 55 mk_evaluation_params 34 56 (prog_var_names … p) 35 57 (prog_spars pars) 36 «ptr, refl …»58 ptr 37 59 (mk_genv_gen ?? (globalenv_noinit ? p) ? (λi.stack_sizes pars «i, ?»)) 38 60 (* (prog_io pars) *). 39 [ @ is_internal_function_of_program_ok @(pi2 … i)61 [ @(is_internal_function_of_program_ok … (pi2 … i)) 40 62  (* TODO or TOBEFOUND *) 41 63 cases daemon … … 56 78 let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in 57 79 let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in 58 let dummy_pc ≝ mk_p ointer (mk_block Code (1)) (mk_offset (bv_zero …))in80 let dummy_pc ≝ mk_program_counter «mk_block Code (1), refl …» one in 59 81 let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in 60 82 (* let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *) … … 70 92 let main : Σi : ident.is_internal_function ???? ≝ «main, ?» in 71 93 ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ; 72 ! pc' ← eval_internal_call_pc … ge main ;94 let pc' ≝ eval_internal_call_pc … ge main in 73 95 return mk_state_pc … st' pc' 74 96  External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *) 75 97 ] (refl …). 76 [ % 77  @(description_of_internal_function … prf) 98 [ @(description_of_internal_function … prf) 78 99  cases spb normalize // 79 100 ] … … 179 200 qed. 180 201 181 definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.182 *#p1 #EQ1 * #p2 #EQ2 @eq_p ointer_elim202 definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?. 203 *#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim 183 204 [ #EQ destruct % #H % 184 205  * #NEQ % #ABS destruct elim (NEQ ?) % … … 220 241 (* as_execute ≝ *) 221 242 (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2) 222 (* as_pc ≝ *) cpointerDeq243 (* as_pc ≝ *) pcDeq 223 244 (* as_pc_of ≝ *) (pc …) 224 245 (* as_classify ≝ *) (joint_classify p) … … 233 254 (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *) 234 255 ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧ 235 succ_pc p p (pc … s1) nxt = returnpc … s2)256 succ_pc p p (pc … s1) nxt = pc … s2) 236 257 (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?) 237 258 (* as_call_ident ≝ *) (joint_call_ident p).
Note: See TracChangeset
for help on using the changeset viewer.