Changeset 2561 for src/joint


Ignore:
Timestamp:
Dec 18, 2012, 5:03:29 PM (7 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
Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2547 r2561  
    107107  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
    108108  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
    109   | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_seq p globals
    110109  | extension_seq : ext_seq p → joint_seq p globals.
    111110
     
    138137inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
    139138  | step_seq : joint_seq p globals → joint_step p globals
     139  | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_step p globals
    140140  | COND: acc_a_reg p → label → joint_step p globals.
    141141
     
    152152    ]
    153153  | COND _ l ⇒ [l]
     154  | CALL _ _ _ ⇒ [ ]
    154155  ].
    155156
  • src/joint/Traces.ma

    r2556 r2561  
    7979  (* use exit_pc as ra and call_dest_for_main as dest *)
    8080  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' ;
     81  ! st0_no_pc ← save_frame ?? sem_globals call_id (call_dest_for_main … pars) st0' ;
    8282  let st0'' ≝ set_no_pc … st0_no_pc st0' in
    8383  ! bl ← block_of_call … ge (inl … main) st0'';
     
    9191  ].
    9292
    93 definition joint_classify_seq :
    94   ∀p : evaluation_params.state p → joint_seq p (globals … p) → status_class ≝
     93definition joint_classify_step :
     94  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
    9595  λp,st,stmt.
    9696  match stmt with
    97   [ CALL f args dest ⇒
     97  [ step_seq _ ⇒ cl_other
     98  | CALL f args dest ⇒
    9899    match (! bl ← block_of_call … (ev_genv p) f st ;
    99100            fetch_function … (ev_genv p) bl) with
     
    105106    | Error _ ⇒ cl_other
    106107    ]
    107   | _ ⇒ cl_other
    108   ].
    109 
    110 definition joint_classify_step :
    111   ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
    112   λp,st,stmt.
    113   match stmt with
    114   [ step_seq s ⇒ joint_classify_seq p st s
    115108  | COND _ _ ⇒ cl_jump
    116109  ].
     
    144137  ].
    145138
    146 definition no_call : ∀p,g.joint_seq p g → Prop ≝
    147   λp,g,s.match s with
    148   [ CALL _ _ _ ⇒ False
    149   | _ ⇒ True
    150   ].
    151 
    152139definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝
    153140  λp,g,s.match s with
     
    155142  | _ ⇒ True
    156143  ].
    157 
    158 lemma no_call_advance : ∀p : evaluation_params.
    159 ∀s,nxt.∀st : state_pc p.
    160 no_call p (globals p) s →
    161 eval_seq_advance p (globals p) (ev_genv p) s nxt st = return next … nxt st.
    162 #p * // #f #args #dest #nxt #st *
    163 qed.
    164 
    165 lemma no_call_other : ∀p : evaluation_params.∀st,s.
    166 no_call p (globals p) s →
    167 joint_classify_seq … st s = cl_other.
    168 #p #st * // #f #args #dest *
    169 qed.
    170 
    171 lemma cond_call_other :
    172   ∀p,globals.∀P : joint_step p globals → Prop.
    173   (∀a,lbltrue.P (COND … a lbltrue)) →
    174   (∀f,args,dest.P (CALL … f args dest)) →
    175   (∀s.no_call ?? s → P s) →
    176   ∀s.P s.
    177 #p #globals #P #H1 #H2 #H3 * // * /2 by / qed.
    178144
    179145lemma joint_classify_call : ∀p : evaluation_params.∀st.
     
    194160    normalize nodelta ]
    195161  #ABS destruct(ABS) ]
    196 @cond_call_other [ #a #lbl | #f' #args #dest | #s #s_no_call ] #nxt #fetch >m_return_bind
     162* [ #s | #f' #args #dest | #a #lbl ] #nxt #fetch >m_return_bind
    197163normalize nodelta
    198 [ normalize in ⊢ (%→?); #ABS destruct(ABS)
    199 |3: whd in match joint_classify_step;
    200   normalize nodelta >(no_call_other … s_no_call) #ABS destruct(ABS)
    201 ]
    202 whd in match joint_classify_step; whd in match joint_classify_seq;
     164[1,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ]
     165whd in match joint_classify_step;
    203166normalize nodelta
    204167inversion (block_of_call ?????)
  • 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.