Changeset 2233 for src/joint


Ignore:
Timestamp:
Jul 23, 2012, 4:51:51 PM (7 years ago)
Author:
tranquil
Message:
  • completed update of ERTL semantics
  • some minor changes in joint semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_paolo.ma

    r2217 r2233  
    3333 ; m: bemem
    3434 }.
     35
     36coercion sem_state_params_to_state nocomposites:
     37  ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0].
    3538
    3639record state_pc (semp : sem_state_params) : Type[0] ≝
     
    134137  (* change of pc must be left to *_flow execution *)
    135138  ; eval_ext_seq: ∀globals.genv_t (fundef (F globals)) → ext_seq uns_pars →
    136       state st_pars → IO io_out io_in (state st_pars)
     139      F globals → state st_pars → IO io_out io_in (state st_pars)
    137140  ; eval_ext_tailcall : ∀globals.genv_t (fundef (F globals)) → ext_tailcall uns_pars →
    138       call_dest uns_pars → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
    139   ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) → ∀s : ext_call uns_pars.
    140       state st_pars →
     141      F globals → state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_pars))
     142  ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) →
     143      ext_call uns_pars → state st_pars →
    141144      IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
    142   ; pop_frame: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → state st_pars → res (state st_pars)
     145  ; pop_frame: ∀globals.genv_t (fundef (F globals)) → F globals → state st_pars → res (state st_pars)
     146  (* do something more in some op2 calculations (e.g. mark a register for correction
     147     with spilled_no in ERTL) *)
     148  ; post_op2 : ∀globals.genv_t (fundef (F globals)) →
     149    Op2 → acc_a_reg uns_pars → acc_a_arg uns_pars → snd_arg uns_pars →
     150    state st_pars → state st_pars
    143151  }.
    144152
     
    407415
    408416definition eval_seq_no_pc :
    409  ∀globals.∀p:sem_params. genv p globals → state p
    410   ∀s:joint_seq p globals.
     417 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals
     418  state p → ∀s:joint_seq p globals.
    411419  IO io_out io_in (state p) ≝
    412  λglobals,p,ge,st,seq.
     420 λp,globals,ge,curr_fn,st,seq.
    413421  match seq return λx.IO ??? with
    414422  [ extension_seq c ⇒
    415     eval_ext_seq … ge c st
     423    eval_ext_seq … ge c curr_fn st
    416424  | LOAD dst addrl addrh ⇒
    417425    ! vaddrh ← dph_arg_retrieve … st addrh ;
     
    447455      let carry ≝ beval_of_bool carry in
    448456    ! st' ← acca_store … dacc_a v' st;
    449     return set_carry … carry st'
     457    return set_carry … carry (post_op2 … p … ge op dacc_a sacc_a src st')
    450458  | CLEAR_CARRY ⇒
    451459    return set_carry … BVfalse st
     
    484492
    485493definition eval_seq_pc :
    486  ∀globals.∀p:sem_params. genv p globals → state p →
     494 ∀p:sem_params.∀globals. genv p globals → state p →
    487495  ∀s:joint_seq p globals.
    488496  IO io_out io_in (step_flow p ? (step_flows … s)) ≝
    489   λg,p,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
     497  λp,g,ge,st,s.match s return λx : joint_seq ??.IO ?? (step_flow ?? (step_flows … x)) with
    490498  [ CALL_ID id args dest ⇒
    491499    ! b ← opt_to_res \ldots  [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
     
    499507
    500508definition eval_step :
    501  ∀globals.∀p:sem_params. genv p globals → state p →
     509 ∀p:sem_params.∀globals. genv p globals →
     510  joint_internal_function p globals → state p →
    502511  ∀s:joint_step p globals.
    503512  IO io_out io_in ((step_flow p ? (step_flows … s))×(state p)) ≝
    504   λglobals,p,ge,st,s.
     513  λp,globals,ge,curr_fn,st,s.
    505514  match s return λx.IO ?? ((step_flow ?? (step_flows … x))×?) with
    506515  [ step_seq s ⇒
    507516    ! flow ← eval_seq_pc ?? ge st s ;
    508     ! st' ← eval_seq_no_pc ?? ge st s ;
     517    ! st' ← eval_seq_no_pc ?? ge curr_fn st s ;
    509518    return 〈flow,st'〉
    510519  | COND src ltrue ⇒
     
    518527  %1 % qed.
    519528
    520 definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv p globals →
    521   (* result registers of current function *) call_dest p → state p → ∀s : joint_fin_step p.
     529definition eval_fin_step_no_pc : ∀p:sem_params.∀globals. genv p globals →
     530  (* current function *) joint_internal_function p globals → state p → ∀s : joint_fin_step p.
    522531  IO io_out io_in (state p) ≝
    523  λglobals,p,ge,ret,st,s.
     532 λp,globals,ge,curr_fn,st,s.
    524533  match s return λx.IO ??? with
    525534    [ tailcall c ⇒
    526       !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
     535      !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
    527536      return st'
    528537    | _ ⇒ return st
     
    530539
    531540definition eval_fin_step_pc :
    532  ∀globals.∀p:sem_params. genv p globals → call_dest p → state p →
     541 ∀p:sem_params.∀globals. genv p globals → joint_internal_function p globals → state p →
    533542  ∀s:joint_fin_step p.
    534543  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
    535   λg,p,ge,ret,st,s.
     544  λp,g,ge,curr_fn,st,s.
    536545  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
    537546  [ tailcall c ⇒
    538     !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
     547    !〈flow,st'〉 ← eval_ext_tailcall … ge c curr_fn st ;
    539548    return flow 
    540549  | GOTO l ⇒ return FRedirect … l
     
    542551  ]. %1 % qed.
    543552
    544 definition do_call : ∀globals: list ident.∀p:sem_params. genv p globals →
     553definition do_call : ∀p:sem_params.∀globals: list ident. genv p globals →
    545554  state p → Z → joint_internal_function p globals → call_args p →
    546555  res (state_pc p) ≝
    547   λglobals,p,ge,st,id,fn,args.
     556  λp,globals,ge,st,id,fn,args.
    548557    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
    549558              args st ;
     
    557566(* The pointer provided is the one to the *next* instruction. *)
    558567definition eval_step_flow :
    559  ∀globals.∀p:sem_params.∀flows.genv p globals →
     568 ∀p:sem_params.∀globals.∀flows.genv p globals →
    560569 state p → cpointer → step_flow p ? flows → res (state_pc p) ≝
    561  λglobals,p,flows,ge,st,nxt,cmd.
     570 λp,globals,flows,ge,st,nxt,cmd.
    562571 match cmd with
    563572  [ Redirect _ l ⇒
     
    570579  ].
    571580
    572 definition eval_fin_step_flow : ∀globals: list ident.∀p:sem_params.∀flows. genv p globals →
     581definition eval_fin_step_flow : ∀p:sem_params.∀globals: list ident.∀flows. genv p globals →
    573582  state p → cpointer → fin_step_flow p ? flows → res (state_pc p) ≝
    574   λglobals,p,lbls,ge,st,curr,cmd.
     583  λp,globals,lbls,ge,st,curr,cmd.
    575584  match cmd with
    576585  [ FRedirect _ l ⇒ goto … ge l st curr
     
    580589    ! 〈st',ra〉 ← fetch_ra … st ;
    581590    ! fn ← fetch_function … ge curr ;
    582     ! st'' ← pop_frame … ge (joint_if_result … fn) st';
     591    ! st'' ← pop_frame … ge fn st';
    583592    return mk_state_pc ? st'' ra
    584593  ].
     
    591600 match stmt with
    592601 [ sequential s nxt ⇒
    593    ! 〈flow,st'〉 ← eval_step … ge st s ;
     602   ! 〈flow,st'〉 ← eval_step … ge curr_fn st s ;
    594603   ! nxtptr ← succ_pc ? p (pc … st) nxt ;
    595604   eval_step_flow … ge st' nxtptr flow
    596605 | final s ⇒
    597    let ret ≝ joint_if_result … curr_fn in
    598    ! st' ← eval_fin_step_no_pc … ge ret st s ;
    599    ! flow ← eval_fin_step_pc … ge ret st s ;
     606   ! st' ← eval_fin_step_no_pc … ge curr_fn st s ;
     607   ! flow ← eval_fin_step_pc … ge curr_fn st s ;
    600608   eval_fin_step_flow … ge st' (pc … st) flow
    601609 ].
Note: See TracChangeset for help on using the changeset viewer.