Changeset 2470 for src/joint/Traces.ma


Ignore:
Timestamp:
Nov 15, 2012, 7:06:45 PM (8 years ago)
Author:
tranquil
Message:

completely separated program counters from code pointers in joint languages: the advantage is program counters with an unbounded offset in Pos

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2457 r2470  
    55 { globals: list ident
    66 ; sparams:> sem_params
    7  ; exit: cpointer
     7 ; exit: program_counter
    88 ; ev_genv: genv sparams globals
    99(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
    1010 }.
    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 *)
     14definition 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
     18lemma 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
     24axiom 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
     31lemma 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)
     39qed.
    1840
    1941record prog_params : Type[1] ≝
    2042 { prog_spars : sem_params
    2143 ; prog : joint_program prog_spars
    22  ; stack_sizes : (Σi.is_internal_function_of_program prog_spars prog i) → ℕ
     44 ; stack_sizes : (Σi.is_internal_function_of_program ?? prog i) → ℕ
    2345(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
    2446 }.
     
    2951(* Invariant: a -1 block is unused in common/Globalenvs *)
    3052let b ≝ mk_block Code (-1) in
    31 let ptr ≝ mk_pointer b (mk_offset (bv_zero …)) in
     53let ptr ≝ mk_program_counter «b, refl …» one in
    3254let p ≝ prog pars in
    3355mk_evaluation_params
    3456  (prog_var_names … p)
    3557  (prog_spars pars)
    36   «ptr, refl …»
     58  ptr
    3759  (mk_genv_gen ?? (globalenv_noinit ? p) ? (λi.stack_sizes pars «i, ?»))
    3860 (* (prog_io pars) *).
    39 [ @is_internal_function_of_program_ok @(pi2 … i)
     61[ @(is_internal_function_of_program_ok … (pi2 … i))
    4062| (* TODO or TOBEFOUND *)
    4163  cases daemon
     
    5678  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    5779  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    58   let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in
     80  let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in
    5981  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
    6082(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
     
    7092    let main : Σi : ident.is_internal_function ???? ≝ «main, ?» in
    7193    ! 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
    7395    return mk_state_pc … st' pc'
    7496  | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
    7597  ] (refl …).
    76   [ %
    77   | @(description_of_internal_function … prf)
     98  [ @(description_of_internal_function … prf)
    7899  | cases spb normalize //
    79100  ]
     
    179200qed.
    180201
    181 definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
    182 *#p1 #EQ1 * #p2 #EQ2 @eq_pointer_elim
     202definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
     203*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
    183204[ #EQ destruct % #H %
    184205| * #NEQ % #ABS destruct elim (NEQ ?) %
     
    220241   (* as_execute ≝ *)
    221242    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2)
    222    (* as_pc ≝ *) cpointerDeq
     243   (* as_pc ≝ *) pcDeq
    223244   (* as_pc_of ≝ *) (pc …)
    224245   (* as_classify ≝ *) (joint_classify p)
     
    233254      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
    234255      ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧
    235       succ_pc p p (pc … s1) nxt = return pc … s2)
     256      succ_pc p p (pc … s1) nxt = pc … s2)
    236257   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
    237258   (* as_call_ident ≝ *) (joint_call_ident p).
Note: See TracChangeset for help on using the changeset viewer.