Changeset 2946 for src/joint/Traces.ma


Ignore:
Timestamp:
Mar 24, 2013, 11:29:01 AM (7 years ago)
Author:
tranquil
Message:

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2932 r2946  
    1 include "joint/joint_semantics.ma".
     1include "joint/semanticsUtils.ma".
    22include "common/StructuredTraces.ma".
    33
     
    3939
    4040lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l.
    41 #A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed.
     41#A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed.
     42
     43lemma lookup_remove_elim : ∀tag,A.∀P : option A → Prop.
     44∀m,i,j.
     45(i = j → P (None ?)) →
     46(i ≠ j → P (lookup tag A m i)) →
     47P (lookup tag A (remove tag A m j) i).
     48#tag #A #P #m #i #j #H1 #H2
     49@(eq_identifier_elim … i j) #H destruct
     50[ >lookup_remove_hit @H1 % | >lookup_remove_miss try @H2 assumption ]
     51qed.
    4252
    4353definition make_global : prog_params → evaluation_params
     
    4656let p ≝ prog pars in
    4757let spars ≝ prog_spars pars in
    48 let genv ≝ globalenv_noinit ? p in
     58let genv ≝ joint_globalenv spars p in
    4959let get_pc_lbl ≝ λid,lbl.
    5060  ! bl ← block_of_funct_id … spars genv id ;
     
    5666 (* (prog_io pars) *).
    5767#s #H
    58 elim (find_symbol_exists … p s ?)
    59 [ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
     68elim (find_symbol_exists … (λx.x) … p s ?)
     69[ #bl #EQ %
     70  whd in match genv; whd in match find_symbol; whd in match drop_fn; normalize nodelta
     71  @lookup_add_elim #H
     72  [2: @lookup_remove_elim [ #EQ >EQ in H; * #ABS cases (ABS ?) % ]
     73    #_ change with (find_symbol ? (globalenv … (λx.x) p) s = ? → ?) >EQ ]
     74  #ABS destruct(ABS) ]
    6075@Exists_append_r
    6176@(Exists_mp … H) //
     
    6681
    6782definition make_initial_state :
    68  ∀pars: prog_params.res (state_pc pars)
     83 ∀pars: prog_params.state_pc pars
    6984λpars.let p ≝ prog pars in
    7085  let sem_globals : evaluation_params ≝ pars in
    7186  let ge ≝ ev_genv sem_globals in
    72   let m0 ≝ alloc_mem … p in
     87  (* this is going to change shortly: globals will not reside in globalenv anymore *)
     88  let m0 ≝ \snd (globalenv_allocmem … (λx.x) p) in
    7389  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
    7490  let globals_size ≝ globals_stacksize … p in
     
    8197(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
    8298  let main ≝ prog_main … p in
    83   let st0 ≝ mk_state pars (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … spp) m in
    84   (* use exit_pc as ra and call_dest_for_main as dest *)
    85   let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
    86   ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) st0' ;
    87   let st0'' ≝ set_no_pc … st0_no_pc st0' in
    88   ! bl ← block_of_call … ge (inl … main) st0'';
    89   ! 〈i, fn〉 ← fetch_function … ge bl ;
    90   match fn with
    91   [ Internal ifn ⇒
    92     ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st0'' ;
    93     let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
    94     return mk_state_pc … st' pc' exit_pc
    95   | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
    96   ].
     99  let st ≝ mk_state pars (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … spp) m globals_size in
     100  mk_state_pc ? (set_sp … spp st) init_pc (null_pc one).
    97101cases m0 in H; #m1 #m2 #m3 #H
    98102whd in H:(???%); destruct whd in ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥
     
    197201    match s with
    198202    [ CALL f' args dest ⇒
    199         match
    200           (! bl ← block_of_call … (ev_genv p) f' st;
    201            fetch_internal_function … (ev_genv p) bl) with
    202         [ OK i_f ⇒ \fst i_f
    203         | _ ⇒ dummy
    204         ]
     203      match
     204        (! bl ← block_of_call … (ev_genv p) f' st;
     205         fetch_internal_function … (ev_genv p) bl) with
     206      [ OK i_f ⇒ \fst i_f
    205207      | _ ⇒ dummy
    206208      ]
     209    | _ ⇒ dummy
     210    ]
    207211  | _ ⇒ dummy
    208212  ]
     
    270274      ]).
    271275
     276(* the prime is to render obsolete old definition of exit_pc, remove when all is corrected *)
     277definition exit_pc' : program_counter ≝
     278mk_program_counter «mk_block (-1), refl …» (p1 one).
     279
     280definition joint_final: ∀p: sem_params.∀globals.
     281  genv p globals → state_pc p → option int ≝
     282 λp,globals,ge,st.
     283 if eq_program_counter (pc … st) exit_pc' then
     284   let ret ≝ call_dest_for_main ?? p in
     285   res_to_opt … (! vals ← read_result … ge ret st ;
     286               Word_of_list_beval vals)
     287 else None ?.
     288
    272289definition joint_abstract_status :
    273290 ∀p : prog_params.
     
    284301   (* as_label_of_pc ≝ *) (joint_label_of_pc p)
    285302   (* as_after_return ≝ *) (joint_after_ret p)
    286    (* as_result ≝ *) (is_final p  (globals ?) (ev_genv p) exit_pc)
     303   (* as_result ≝ *) (joint_final p  (globals ?) (ev_genv p))
    287304   (* as_call_ident ≝ *) (λst.joint_call_ident p st)
    288305   (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident p st).
Note: See TracChangeset for help on using the changeset viewer.