Ignore:
Timestamp:
Nov 6, 2012, 5:00:01 PM (8 years ago)
Author:
tranquil
Message:

generalised calls to calls with pointers

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2422 r2437  
    152152      F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
    153153  ; ext_tailcall_id : ∀globals.genv_gen F globals → ext_tailcall uns_pars →
    154       state st_pars → IO io_out io_in ident
    155   ; eval_ext_call: ∀globals.genv_gen F globals →
    156       ext_call uns_pars → state st_pars →
    157       IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
    158   ; ext_call_id : ∀globals.genv_gen F globals → ext_call uns_pars →
    159154      state st_pars → IO io_out io_in ident
    160155  ; pop_frame: ∀globals.genv_gen F globals → F globals → state st_pars → res (state st_pars)
     
    256251definition save_ra : ∀p. state p → cpointer → res (state p) ≝
    257252 λp,st,l.
    258   ! 〈addrl,addrh〉 ← address_of_pointer l ; (* always succeeds *)
     253  ! 〈addrl,addrh〉 ← beval_pair_of_pointer l ; (* always succeeds *)
    259254  ! st' ← push … st addrl;
    260255  push … st' addrh.
     
    431426axiom BadFunction : String.
    432427axiom SuccessorNotProvided : String.
     428
     429definition block_of_call ≝ λp:sem_params.λglobals.
     430  λge: genv p globals.λst : state p.λf.
     431  match f with
     432  [ inl id ⇒
     433    opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id)
     434  | inr addr ⇒
     435    ! addr_l ← dpl_arg_retrieve … st (\fst addr) ;
     436    ! addr_h ← dph_arg_retrieve … st (\snd addr) ;
     437    ! ptr ← pointer_of_bevals [addr_l ; addr_h] ;
     438    if eq_bv … (bv_zero …) (offv (poff … ptr)) then
     439      return pblock ptr
     440    else Error … [MSG BadFunction]
     441  ].
    433442
    434443definition eval_seq_no_pc :
     
    455464  | ADDRESS id prf ldest hdest ⇒
    456465    let addr ≝ opt_safe ? (find_symbol … ge id) ? in
    457     ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer addr zero_offset) ;
     466    ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer addr zero_offset) ;
    458467    ! st' ← dpl_store … ldest laddr st;
    459468    dph_store … hdest haddr st'
     
    486495  | MOVE dst_src ⇒
    487496    pair_reg_move … st dst_src
    488   | CALL_ID id args dest ⇒
    489     ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
     497  | CALL f args dest ⇒
     498    ! b ← block_of_call … ge st f : IO ???;
    490499    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
    491     return st'
    492   | extension_call s ⇒
    493     !〈flow, st'〉 ← eval_ext_call … ge s st ;
    494500    return st'
    495501  | _ ⇒ return st
     
    507513  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
    508514  λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
    509   [ CALL_ID id args dest ⇒
    510     ! b ← opt_to_res \ldots  [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
     515  [ CALL f args dest ⇒
     516    ! b ← block_of_call … ge st f : IO ???;
    511517    ! 〈flow, st'〉 ← eval_call_block … ge st b args dest ;
    512     return flow
    513   | extension_call s ⇒
    514     !〈flow, st'〉 ← eval_ext_call … ge s st ;
    515518    return flow
    516519  | _ ⇒ return Proceed ???
Note: See TracChangeset for help on using the changeset viewer.