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/semantics.ma

    r2551 r2556  
    6868  { st_no_pc :> state semp
    6969  ; pc : program_counter
     70  (* for correctness reasons: pc of last popped calling address (exit_pc at the start) *)
     71  ; last_pop : program_counter
    7072  }.
     73
     74(* special program counter that is guaranteed to not correspond to anything *)
     75definition exit_pc : program_counter ≝
     76  mk_program_counter «mk_block Code (-1), refl …» one.
    7177
    7278definition set_m: ∀p. bemem → state p → state p ≝
     
    8793
    8894definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
    89  λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
     95 λp,pc,st. mk_state_pc … (st_no_pc … st) pc (last_pop … st).
    9096
    9197definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
    92  λp,s,st. mk_state_pc … s (pc … st).
     98 λp,s,st. mk_state_pc … s (pc … st) (last_pop … st).
     99
     100definition set_last_pop: ∀p. ? → state_pc p → state_pc p ≝
     101 λp,s,st. mk_state_pc … (st_no_pc … st) (pc … st) s.
    93102
    94103definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
     
    356365 λp,globals,ge,l,st.
    357366  ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ;
    358   return mk_state_pc … st newpc.
     367  return set_pc … newpc st.
    359368
    360369(*
     
    366375 λp,l,st.
    367376 let newpc ≝ succ_pc … (pc … st) l in
    368  mk_state_pc … st newpc.
     377 set_pc … newpc st.
    369378
    370379axiom NoSuccessor : String.
     
    374383  ! 〈id_fn, stmt〉 ← fetch_statement … ge pc ;
    375384  match stmt with
    376   [ sequential _ nxt ⇒ return nxt
     385  [ sequential s nxt ⇒
     386    match s with
     387    [ step_seq _ => return nxt
     388    | COND _ _ => Error … [MSG NoSuccessor]
     389    ]
    377390  | _ ⇒ Error … [MSG NoSuccessor]
    378391  ].
     
    493506! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    494507! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
    495 return allocate_locals … p (joint_if_locals … fn) st.
     508return allocate_locals … p (joint_if_locals … fn) st'.
    496509
    497510definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
     
    507520  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    508521  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
    509   return mk_state_pc … st'' pc
     522  return mk_state_pc … st'' pc (last_pop … st)
    510523| External efd ⇒
    511524  ! st' ← eval_external_call … efd args dest st ;
    512   return mk_state_pc … st' (succ_pc p (pc … st) nxt)
     525  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
    513526].
    514527
     
    544557! st' ← pop_frame … ge curr_id curr_fn st ;
    545558! nxt ← next_of_pc … ge (pc … st') ;
    546 return next … nxt st' (* now address pushed on stack are calling ones! *).
     559return
     560  set_last_pop … (pc … st') (next … nxt st') (* now address pushed on stack are calling ones! *).
    547561
    548562definition eval_tailcall ≝
     
    556570  ! st' ← eval_internal_call p globals ge i ifd args st ;
    557571  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
    558   return mk_state_pc … st' pc
     572  return mk_state_pc … st' pc (last_pop … st)
    559573| External efd ⇒
    560574  let curr_dest ≝ joint_if_result ?? curr_fn in
     
    604618  ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???;
    605619  ! st' ← eval_statement_no_pc … ge id fn s st : IO ???;
    606   let st'' ≝ mk_state_pc … st' (pc … st) in
     620  let st'' ≝ set_no_pc … st' st in
    607621  eval_statement_advance … ge id fn s st''.
    608622
Note: See TracChangeset for help on using the changeset viewer.