Changeset 2217 for src/joint


Ignore:
Timestamp:
Jul 19, 2012, 6:13:54 PM (7 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
Location:
src/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r2214 r2217  
    2424              |       |    /   
    2525          unserialized_params             
    26             |            \       
    27             |             \     
    28             |         local_params
    29             |              |   
    30     step_params       funct_params
    31 
    32 step_params : types needed to define steps (stmts with a default fallthrough)
     26
     27unserialized_params : things unrelated to serialization (i.e. graph or linear
     28                      form)
    3329stmt_params : adds successor type needed to define statements
    3430funct_params : types of result register and parameters of function
    35 local_params : adds types of local registers
    3631params : adds type of code and related properties *)
    3732
     
    7570definition zero_byte : Byte ≝ bv_zero 8.
    7671
    77 record step_params : Type[1] ≝
     72record unserialized_params : Type[1] ≝
    7873 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
    7974 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
     
    9590 ; ext_tailcall : Type[0]
    9691 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
     92 ; paramsT : Type[0]
     93 ; localsT: Type[0]
    9794 }.
    9895
    99 inductive joint_seq (p:step_params) (globals: list ident): Type[0] ≝
     96inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝
    10097  | COMMENT: String → joint_seq p globals
    10198  | COST_LABEL: costlabel → joint_seq p globals
     
    145142  extension_branch on _s : ext_branch ? to joint_branch ?.*)
    146143
    147 inductive joint_step (p : step_params) (globals : list ident) : Type[0] ≝
     144inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
    148145  | step_seq : joint_seq p globals → joint_step p globals
    149146  | COND: acc_a_reg p → label → joint_step p globals.
     
    170167    ].
    171168
    172 definition step_forall_labels : ∀p : step_params.∀globals.
     169definition step_forall_labels : ∀p.∀globals.
    173170    (label → Prop) → joint_step p globals → Prop ≝
    174171λp,g,P,inst. All … P (step_labels … inst).
    175172
    176173definition step_classifier :
    177   ∀p : step_params.∀globals.
     174  ∀p.∀globals.
    178175    joint_step p globals → status_class ≝ λp,g,s.
    179176  match s with
     
    187184  ].
    188185
    189 record funct_params : Type[1] ≝
    190   { resultT : Type[0]
    191   ; paramsT : Type[0]
    192   }.
    193  
    194 record local_params : Type[1] ≝
    195  { funct_pars :> funct_params
    196  ; localsT: Type[0]
    197  }.
    198 
    199 record unserialized_params : Type[1] ≝
    200  { u_inst_pars :> step_params
    201  ; u_local_pars :> local_params
    202  }.
    203 
    204186record stmt_params : Type[1] ≝
    205187  { uns_pars :> unserialized_params
     
    208190  }.
    209191
    210 inductive joint_fin_step (p: step_params): Type[0] ≝
     192inductive joint_fin_step (p: unserialized_params): Type[0] ≝
    211193  | GOTO: label → joint_fin_step p
    212194  | RETURN: joint_fin_step p
     
    468450    forall_statements_i … (statement_closed … code) code.
    469451
    470 (* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
    471 definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
    472   (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
    473 
    474452record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
    475453{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
     
    478456     following, right? *)
    479457(*  joint_if_sig: signature;  -- dropped in front end *)
    480   joint_if_result   : resultT p;
     458  joint_if_result   : call_dest p;
    481459  joint_if_params   : paramsT p;
    482460  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
  • src/joint/TranslateUtils_paolo.ma

    r2214 r2217  
    11include "joint/Joint_paolo.ma".
    22include "joint/blocks.ma".
     3include "utilities/hide.ma".
    34
    45(* general type of functions generating fresh things *)
    5 (* type T is the syntactic type of the generated things *)
    6 (* (sig for RTLabs registers, unit in others ) *)
    7 definition freshT ≝ λg.λpars : params.state_monad (joint_internal_function pars g).
    8 
    9 definition rtl_ertl_fresh_reg:
    10  ∀inst_pars,funct_pars,globals.
    11   freshT globals (rtl_ertl_params inst_pars funct_pars) register ≝
    12   λinst_pars,var_pars,globals,def.
    13     let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    14     〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
     6definition freshT ≝ λpars : params.λg.state_monad (joint_internal_function pars g).
    157
    168include alias "basics/lists/list.ma".
    17 let rec rtl_ertl_fresh_regs inst_pars funct_pars globals (n : ℕ) on n :
    18   freshT globals (rtl_ertl_params inst_pars funct_pars)
    19     (Σl : list register. |l| = n) ≝
    20   let ret_type ≝ (Σl : list register. |l| = n) in
    21   match n  return λx.x = n → freshT … ret_type with
    22   [ O ⇒ λeq'.return (mk_Sig … [ ] ?)
    23   | S n' ⇒ λeq'.
    24     ! regs' ← rtl_ertl_fresh_regs inst_pars funct_pars globals n';
    25     ! reg ← rtl_ertl_fresh_reg inst_pars funct_pars globals;
    26     return (mk_Sig … (reg :: regs') ?)
    27   ](refl …). <eq' normalize [//] elim regs' #l #eql >eql //
    28   qed.
     9let rec repeat_fresh pars globals A (fresh : freshT pars globals A) (n : ℕ)
     10  on n :
     11  freshT pars globals (Σl : list A. |l| = n) ≝
     12  match n  return λx.freshT … (Σl.|l| = x) with
     13  [ O ⇒ return «[ ], ?»
     14  | S n' ⇒
     15    ! regs' ← repeat_fresh … fresh n';
     16    ! reg ← fresh ;
     17    return «reg::regs',?»
     18  ]. [% | @hide_prf cases regs' #l #EQ normalize >EQ % ] qed.
    2919
    3020definition fresh_label:
     
    126116  ∀globals: list ident.
    127117  (* fresh register creation *)
    128   freshT globals g_pars (localsT … g_pars) →
     118  freshT g_pars globals (localsT … g_pars) →
    129119  ∀b : bind_seq_block g_pars globals (joint_step g_pars globals) +
    130120       bind_seq_block g_pars globals (joint_fin_step g_pars).
     
    147137  ∀globals: list ident.
    148138  (* fresh register creation *)
    149   freshT globals dst_g_pars (localsT dst_g_pars) →
     139  freshT dst_g_pars globals (localsT dst_g_pars) →
    150140  (* initialized function definition with empty graph *)
    151141  joint_internal_function dst_g_pars globals →
  • 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.