Changeset 2556 for src/joint/Traces.ma


Ignore:
Timestamp:
Dec 14, 2012, 2:54:06 PM (8 years ago)
Author:
tranquil
Message:

in joint semantics and traces: added a last popped calling address to state_pc, in order to have a strong enough as_after_return in joint (due to graph languages having one-to-many predecessors)
in lineariseProof: one axiom left (tailcall case)

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Traces.ma

    r2553 r2556  
    55 { globals: list ident
    66 ; sparams:> sem_params
    7  ; exit: program_counter
    87 ; ev_genv: genv sparams globals
    98(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
     
    4746
    4847λpars.
    49 (* Invariant: a -1 block is unused in common/Globalenvs *)
    50 let b ≝ mk_block Code (-1) in
    51 let ptr ≝ mk_program_counter «b, refl …» one in
    5248let p ≝ prog pars in
    5349mk_evaluation_params
    5450  (prog_var_names … p)
    5551  (prog_spars pars)
    56   ptr
    5752  (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars))
    5853 (* (prog_io pars) *).
     
    7671  let m ≝ alloc_mem … p in
    7772  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    78   let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
    79   let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in
    8073  let spp : xpointer ≝
    8174    «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
     
    8477  let main ≝ prog_main … p in
    8578  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
    86   (* use exit sem_globals as ra and call_dest_for_main as dest *)
    87   let st0' ≝ mk_state_pc … (set_sp … spp st0) (exit sem_globals) in
    88   ! st0'' ← save_frame ?? sem_globals true (call_dest_for_main … pars) st0' ;
    89   let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
    90   ! bl ← block_of_call … ge (inl … main) st_pc0;
     79  (* use exit_pc as ra and call_dest_for_main as dest *)
     80  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
     81  ! st0_no_pc ← save_frame ?? sem_globals true (call_dest_for_main … pars) st0' ;
     82  let st0'' ≝ set_no_pc … st0_no_pc st0' in
     83  ! bl ← block_of_call … ge (inl … main) st0'';
    9184  ! 〈i, fn〉 ← fetch_function … ge bl ;
    9285  match fn with
    9386  [ Internal ifn ⇒
    94     ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st_pc0 ;
     87    ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st0'' ;
    9588    let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
    96     return mk_state_pc … st' pc'
     89    return mk_state_pc … st' pc' exit_pc
    9790  | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
    9891  ].
     
    231224  match \snd x with
    232225  [ sequential s next ⇒
     226    last_pop … s2 = pc … s1 ∧
    233227    pc … s2 = succ_pc p (pc … s1) next
    234228  | _ ⇒ False (* never happens *)
     
    374368      ])
    375369   (* as_after_return ≝ *) (joint_after_ret p)
    376    (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
     370   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) exit_pc s ≠ None ?)
    377371   (* as_call_ident ≝ *) (joint_call_ident p)
    378372   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
Note: See TracChangeset for help on using the changeset viewer.