Ignore:
Timestamp:
Dec 18, 2012, 5:03:29 PM (8 years ago)
Author:
tranquil
Message:
  • moved CALL as different case than joint_seq: lots of broken code now
  • changed save_frame flag from bool to more descriprive variant type call_kind
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2556 r2561  
    151151 | _ ⇒ Error … [MSG BadFunction]
    152152 ].
     153
     154inductive call_kind : Type[0] ≝
     155| call_ptr : call_kind
     156| call_id : call_kind.
     157
     158definition kind_of_call :
     159  ∀p.(ident + (dpl_arg p × (dph_arg p))) → call_kind ≝
     160  λp,f.match f with [ inl _ ⇒ call_id | inr _ ⇒ call_ptr ].
    153161
    154162record sem_unserialized_params
     
    174182  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
    175183  ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars
    176   ; save_frame: bool (* ident or ptr *) → call_dest uns_pars → state_pc st_pars → res (state st_pars)
     184  ; save_frame: call_kind → call_dest uns_pars → state_pc st_pars → res (state st_pars)
    177185   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    178186     type of arguments. To be fixed using a dependent type *)
     
    378386
    379387axiom NoSuccessor : String.
    380 definition next_of_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) →
     388definition next_of_call_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) →
    381389  program_counter → res (succ p) ≝
    382390λp,globals,ge,pc.
     
    385393  [ sequential s nxt ⇒
    386394    match s with
    387     [ step_seq _ => return nxt
    388     | COND _ _ => Error … [MSG NoSuccessor]
     395    [ CALL _ _ _ ⇒ return nxt
     396    | _ ⇒ Error … [MSG NoSuccessor]
    389397    ]
    390398  | _ ⇒ Error … [MSG NoSuccessor]
     
    510518definition is_inl : ∀A,B.A+B → bool ≝ λA,B,x.match x with [ inl _ ⇒ true | _ ⇒ false ].
    511519
    512 definition eval_seq_call ≝
     520definition eval_call ≝
    513521λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt.
    514522λst : state_pc p.
     
    517525match fd with
    518526[ Internal ifd ⇒
    519   ! st' ← save_frame … (is_inl … f) dest st ;
     527  ! st' ← save_frame … (kind_of_call … f) dest st ;
    520528  ! st'' ← eval_internal_call p globals ge i ifd args st' ;
    521529  let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in
     
    525533  return mk_state_pc … st' (succ_pc p (pc … st) nxt) (last_pop … st)
    526534].
    527 
    528 definition eval_seq_advance :
    529  ∀p:sem_params.∀globals.∀ge:genv p globals.
    530   joint_seq p globals → succ p → state_pc p →
    531   IO io_out io_in (state_pc p) ≝
    532   λp,globals,ge,s,nxt,st.
    533   match s with
    534   [ CALL f args dest ⇒
    535     eval_seq_call … ge f args dest nxt st
    536   | _ ⇒ return next … nxt st
    537   ].
    538535
    539536definition eval_statement_no_pc :
     
    546543    match s with
    547544    [ step_seq s ⇒ eval_seq_no_pc … ge curr_id curr_fn s st
    548     | COND a l ⇒ return st
     545    | _ ⇒ return st
    549546    ]
    550547  | _ ⇒ return st
     
    556553λst : state p.
    557554! st' ← pop_frame … ge curr_id curr_fn st ;
    558 ! nxt ← next_of_pc … ge (pc … st') ;
     555! nxt ← next_of_call_pc … ge (pc … st') ;
    559556return
    560557  set_last_pop … (pc … st') (next … nxt st') (* now address pushed on stack are calling ones! *).
     
    586583  [ sequential s nxt ⇒
    587584    match s return λ_.IO ??? with
    588     [ step_seq s ⇒
    589       eval_seq_advance … ge s nxt st
     585    [ step_seq s ⇒ return next … nxt st
    590586    | COND a l ⇒
    591587      ! v ← acca_retrieve … st a ;
     
    595591      else
    596592        return next … nxt st
     593    | CALL f args dest ⇒
     594      eval_call … ge f args dest nxt st
    597595    ]
    598596  | final s ⇒
Note: See TracChangeset for help on using the changeset viewer.