Ignore:
Timestamp:
Jul 19, 2012, 6:13:54 PM (8 years ago)
Author:
tranquil
Message:
  • collapsed step_params, unserialized_params, funct_params and local_params into one (unserialized_params)
  • completed update of RTL, LTL and LIN semantics
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics_paolo.ma

    r2214 r2217  
    8686 λpars,globals,ge,p.function_of_block pars globals ge (pblock p).
    8787
    88 inductive step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝
     88inductive step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
    8989  | Redirect : ∀lbls.(Σl.In ? lbls l) → step_flow p F (Labels lbls) (* used for goto-like flow alteration *)
    9090  | Init     : Z → F → call_args p → call_dest p → step_flow p F Call (* call a function with given id, then proceed *)
    9191  | Proceed  : ∀flows.step_flow p F flows. (* go to implicit successor *)
    9292
    93 inductive fin_step_flow (p : step_params) (F : Type[0]) : possible_flows → Type[0] ≝
     93inductive fin_step_flow (p : unserialized_params) (F : Type[0]) : possible_flows → Type[0] ≝
    9494  | FRedirect : ∀lbls.(Σl.In ? lbls l) → fin_step_flow p F (Labels lbls)
    9595  | FTailInit : Z → F → call_args p → fin_step_flow p F Call
     
    126126  ; fetch_external_args: external_function → state st_pars →
    127127      res (list val)
    128   ; set_result: list val → state st_pars → res (state st_pars)
     128  ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars)
    129129  ; call_args_for_main: call_args uns_pars
    130130  ; call_dest_for_main: call_dest uns_pars
    131131
    132132  (* from now on, parameters that use the type of functions *)
    133   ; read_result: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (list beval)
     133  ; read_result: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → state st_pars → res (list beval)
    134134  (* change of pc must be left to *_flow execution *)
    135135  ; eval_ext_seq: ∀globals.genv_t (fundef (F globals)) → ext_seq uns_pars →
    136136      state st_pars → IO io_out io_in (state st_pars)
    137137  ; eval_ext_tailcall : ∀globals.genv_t (fundef (F globals)) → ext_tailcall uns_pars →
    138       state st_pars → IO io_out io_in ((fin_step_flow uns_pars (F globals) Call)×(state st_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))
    139139  ; eval_ext_call: ∀globals.genv_t (fundef (F globals)) → ∀s : ext_call uns_pars.
    140140      state st_pars →
    141141      IO io_out io_in ((step_flow uns_pars (F globals) Call)×(state st_pars))
    142   ; pop_frame: ∀globals.genv_t (fundef (F globals)) → state st_pars → res (state st_pars)
     142  ; pop_frame: ∀globals.genv_t (fundef (F globals)) → call_dest uns_pars → state st_pars → res (state st_pars)
    143143  }.
    144144
     
    206206         fixed once we fully implement external functions. *)
    207207      let vs ≝ [mk_val ? evres] in
    208       ! st ← set_result … p' vs st : IO ???;
     208      ! st ← set_result … p' vs dest st : IO ???;
    209209      return 〈Proceed ???, st〉
    210210      ].
     
    326326
    327327definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
    328   genv p globals → cpointer → res (joint_statement p globals) ≝
     328  genv p globals → cpointer →
     329  res ((joint_internal_function p globals) × (joint_statement p globals)) ≝
    329330  λp,msp,globals,ge,ptr.
    330331  let pt ≝ point_of_pointer ? msp ptr in
    331332  ! fn ← fetch_function … ge ptr ;
    332   opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
     333  ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt);
     334  return 〈fn, stmt〉.
    333335 
    334336definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
     
    517519
    518520definition eval_fin_step_no_pc : ∀globals: list ident.∀p:sem_params. genv p globals →
    519   state p → ∀s : joint_fin_step p.
     521  (* result registers of current function *) call_dest p → state p → ∀s : joint_fin_step p.
    520522  IO io_out io_in (state p) ≝
    521  λglobals,p,ge,st,s.
     523 λglobals,p,ge,ret,st,s.
    522524  match s return λx.IO ??? with
    523525    [ tailcall c ⇒
    524       !〈flow,st'〉 ← eval_ext_tailcall … ge c st ;
     526      !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
    525527      return st'
    526528    | _ ⇒ return st
     
    528530
    529531definition eval_fin_step_pc :
    530  ∀globals.∀p:sem_params. genv p globals → state p →
     532 ∀globals.∀p:sem_params. genv p globals → call_dest p → state p →
    531533  ∀s:joint_fin_step p.
    532534  IO io_out io_in (fin_step_flow p ? (fin_step_flows … s)) ≝
    533   λg,p,ge,st,s.
     535  λg,p,ge,ret,st,s.
    534536  match s return λx.IO ?? (fin_step_flow ?? (fin_step_flows … x)) with
    535537  [ tailcall c ⇒
    536     !〈flow,st'〉 ← eval_ext_tailcall … ge c st ;
     538    !〈flow,st'〉 ← eval_ext_tailcall … ge c ret st ;
    537539    return flow 
    538540  | GOTO l ⇒ return FRedirect … l
     
    577579  | _ ⇒
    578580    ! 〈st',ra〉 ← fetch_ra … st ;
    579     ! st'' ← pop_frame … ge st;
     581    ! fn ← fetch_function … ge curr ;
     582    ! st'' ← pop_frame … ge (joint_if_result … fn) st';
    580583    return mk_state_pc ? st'' ra
    581584  ].
     
    583586definition eval_statement :
    584587 ∀globals.∀p:sem_params.genv p globals →
    585   state_pc p → joint_statement p globals →
     588  state_pc p → joint_internal_function p globals → joint_statement p globals →
    586589    IO io_out io_in (state_pc p) ≝
    587  λglobals,p,ge,st,stmt.
     590 λglobals,p,ge,st,curr_fn,stmt.
    588591 match stmt with
    589592 [ sequential s nxt ⇒
     
    592595   eval_step_flow … ge st' nxtptr flow
    593596 | final s ⇒
    594    ! st' ← eval_fin_step_no_pc … ge st s ;
    595    ! flow ← eval_fin_step_pc … ge st 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 ;
    596600   eval_fin_step_flow … ge st' (pc … st) flow
    597601 ].
     
    600604  state_pc p → IO io_out io_in (state_pc p) ≝
    601605  λglobals,p,ge,st.
    602   ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
    603   eval_statement … ge st s.
     606  ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???;
     607  eval_statement … ge st fn s.
    604608
    605609(* Paolo: what if in an intermediate language main finishes with an external
     
    609613  genv p globals → cpointer → state_pc p → option int ≝
    610614 λglobals,p,ge,exit,st.res_to_opt ? (
    611   do s ← fetch_statement ? p … ge (pc … st);
     615  do 〈fn,s〉 ← fetch_statement ? p … ge (pc … st);
    612616  match s with
    613617  [ final s' ⇒
    614618    match s' with
    615619    [ RETURN ⇒
    616       do 〈st,ra〉 ← fetch_ra … st;
     620      do 〈st',ra〉 ← fetch_ra … st;
    617621      if eq_pointer ra exit then
    618        do vals ← read_result … ge st ;
     622       do vals ← read_result … ge (joint_if_result … fn) st' ;
    619623       Word_of_list_beval vals
    620624      else
Note: See TracChangeset for help on using the changeset viewer.