Changeset 2217


Ignore:
Timestamp:
Jul 19, 2012, 6:13:54 PM (5 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
Files:
3 added
9 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_paolo.ma

    r2214 r2217  
    2525  | ertl_frame_size: register → ertl_seq.
    2626
    27 definition ertl_uns_params ≝ mk_unserialized_params
    28   (mk_step_params
     27definition ERTL_uns ≝ mk_unserialized_params
    2928    (* acc_a_reg ≝ *) register
    3029    (* acc_b_reg ≝ *) register
     
    4241    (* ext_call ≝ *) void
    4342    (* ext_tailcall ≝ *) void
    44   )
    45   (mk_local_params
    46     (mk_funct_params
    47       (* resultT ≝ *) unit
    48       (* paramsT ≝ *) ℕ)
    49       (* localsT ≝ *) register).
     43    (* paramsT ≝ *) ℕ
     44    (* localsT ≝ *) register.
    5045
    51 definition ERTL ≝ mk_graph_params ertl_uns_params.
     46definition ERTL ≝ mk_graph_params ERTL_uns.
    5247definition ertl_program ≝ joint_program ERTL.
    5348
  • src/LIN/joint_LTL_LIN_paolo.ma

    r2214 r2217  
    1313
    1414definition LTL_LIN : unserialized_params ≝ mk_unserialized_params
    15   (mk_step_params
    1615    (* acc_a_reg ≝ *) unit
    1716    (* acc_b_reg ≝ *) unit
     
    2928    (* ext_call ≝ *) void
    3029    (* ext_tailcall ≝ *) void
    31   )
    32   (mk_local_params
    33     (mk_funct_params
    34       (* resultT ≝ *) unit
    35       (* paramsT ≝ *) unit)
    36       (* localsT ≝ *) void).
     30    (* paramsT ≝ *) unit
     31    (* localsT ≝ *) void.
    3732
    3833interpretation "move from acc" 'mov a b = (MOVE ?? (from_acc a b)).
  • src/RTL/RTLToERTL_paolo.ma

    r2214 r2217  
    66
    77include alias "basics/lists/list.ma".
     8
     9definition ertl_fresh_reg:
     10 ∀globals.freshT ERTL globals register ≝
     11  λglobals,def.
     12    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     13    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
    814
    915definition save_hdws :
     
    101107definition allocate_regs :
    102108  ∀globals,rs.rs_set rs →
    103   state_monad (joint_internal_function ERTL globals) (list (register×Register)) ≝
     109  freshT ERTL globals (list (register×Register)) ≝
    104110  λglobals,rs,saved,def.
    105111   let allocate_regs_internal ≝
    106112    λr: Register.
    107113    λdef_sregs.
    108     let 〈def, r'〉 ≝ rtl_ertl_fresh_reg … (\fst def_sregs) in
     114    let 〈def, r'〉 ≝ ertl_fresh_reg … (\fst def_sregs) in
    109115    〈def, 〈r', r〉::\snd def_sregs〉 in
    110116  rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉.
     
    118124  let end_lbl ≝ joint_if_exit … def in
    119125  state_run … def (
    120     ! sral ← rtl_ertl_fresh_reg … ;
    121     ! srah ← rtl_ertl_fresh_reg … ;
     126    ! sral ← ertl_fresh_reg … ;
     127    ! srah ← ertl_fresh_reg … ;
    122128    ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ;
    123     ! prologue' ← bcompile … (rtl_ertl_fresh_reg …) (prologue … params sral srah sregs) ;
     129    ! prologue' ← bcompile … (ertl_fresh_reg …) (prologue … params sral srah sregs) ;
    124130    let epilogue' ≝ epilogue … ret_regs sral srah sregs in
    125131    ! def' ← state_get … ;
     
    258264      graph' entry' exit' in
    259265  let def'' ≝ b_graph_translate …
    260     (rtl_ertl_fresh_reg …)
     266    (ertl_fresh_reg …)
    261267    def'
    262268    (translate_step globals)
  • src/RTL/RTL_paolo.ma

    r2214 r2217  
    1212
    1313definition RTL_uns ≝ mk_unserialized_params
    14   (mk_step_params
    1514    (* acc_a_reg ≝ *) register
    1615    (* acc_b_reg ≝ *) register
     
    2827    (* ext_call ≝ *) rtl_call
    2928    (* ext_tailcall ≝ *) rtl_tailcall
    30   )
    31   (mk_local_params
    32     (mk_funct_params
    33       (* resultT ≝ *) (list register)
    34       (* paramsT ≝ *) (list register))
    35       (* localsT ≝ *) register).
     29    (* paramsT ≝ *) (list register)
     30    (* localsT ≝ *) register.
    3631
    3732definition RTL ≝ mk_graph_params RTL_uns.
     
    9893
    9994definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params
    100   (mk_step_params
    10195    (* acc_a_reg ≝ *) register
    10296    (* acc_b_reg ≝ *) register
     
    114108    (* ext_call ≝ *) rtl_call
    115109    (* ext_tailcall ≝ *) void
    116   )
    117   (mk_local_params
    118     (mk_funct_params
    119       (* resultT ≝ *) (list register)
    120       (* paramsT ≝ *) (list register))
    121       (* localsT ≝ *) register)).
     110    (* paramsT ≝ *) (list register)
     111    (* localsT ≝ *) register).
    122112
    123113definition rtl_ntc_program ≝ joint_program RTL_ntc.
  • src/RTL/semantics_paolo.ma

    r1999 r2217  
    66record frame: Type[0] ≝
    77 { fr_ret_regs: list register
    8  ; fr_pc: address
    9  ; fr_sp: pointer
     8 ; fr_pc: cpointer
     9 ; fr_sp: xpointer
    1010 ; fr_carry: beval
    1111 ; fr_regs: register_env beval
    1212 }.
    1313
    14 definition rtl_sem_state_params : sem_state_params ≝
     14definition RTL_state : sem_state_params ≝
    1515  mk_sem_state_params
    1616    (list frame)
     
    1919    (λ_.empty_map …).
    2020
    21 definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : rtl_argument.
     21definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : psd_argument.
    2222  match a with
    2323  [ Reg r ⇒ reg_retrieve env r
    24   | Imm b ⇒ return (BVByte b)
     24  | Imm b ⇒ return b
    2525  ].
    2626
     
    3030
    3131definition rtl_fetch_ra:
    32  state rtl_sem_state_params → res ((state rtl_sem_state_params) × address) ≝
     32 state RTL_state → res ((state RTL_state) × cpointer) ≝
    3333 λst.
    3434  match st_frms ? st with
     
    3636  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
    3737
    38 definition rtl_init_locals :
    39  list register → register_env beval → register_env beval ≝
    40  λlocals,env.
    41   foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals.
    42 
     38definition rtl_init_local :
     39 register → register_env beval → register_env beval ≝
     40 λlocal,env.add … env local BVundef.
    4341
    4442definition rtl_setup_call:
    45  nat → list register → list rtl_argument → state rtl_sem_state_params → res (state rtl_sem_state_params) ≝
     43 nat → list register → list psd_argument → state RTL_state → res (state RTL_state) ≝
    4644  λstacksize,formal_arg_regs,actual_arg_regs,st.
    4745  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
     
    5351    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
    5452  OK …
    55    (set_regs rtl_sem_state_params new_regs
     53   (set_regs RTL_state new_regs
    5654    (set_m … mem
    57      (set_sp … (mk_pointer XData b ? (mk_offset 0)) st))).
     55     (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))).
    5856cases b * #r #off #E >E %
    5957qed.
    6058
    61 definition rtl_save_frame ≝ λl.λretregs.λst : state rtl_sem_state_params.
     59definition rtl_save_frame ≝ λl.λretregs.λst : state RTL_state.
    6260  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
    63   set_frms rtl_sem_state_params frame st. 
     61  OK … (set_frms RTL_state frame st).
    6462
    6563(*CSC: XXXX, for external functions only*)
    66 axiom rtl_fetch_external_args: external_function → state rtl_sem_state_params → res (list val).
    67 axiom rtl_set_result: list val → state rtl_sem_state_params → res (state rtl_sem_state_params).
    68 
    69 definition rtl_msu_params :
    70   more_sem_unserialized_params rtl_uns_params ≝
    71  mk_more_sem_unserialized_params rtl_uns_params rtl_sem_state_params
    72     reg_store reg_retrieve rtl_arg_retrieve
    73     reg_store reg_retrieve rtl_arg_retrieve
    74     reg_store reg_retrieve rtl_arg_retrieve
    75     reg_store reg_retrieve rtl_arg_retrieve
    76     rtl_arg_retrieve
    77     (λenv,p. let 〈dest,src〉 ≝ p in
    78       ! v ← rtl_arg_retrieve env src ;
    79       reg_store dest v env)
    80     rtl_fetch_ra
    81     rtl_init_locals
    82     rtl_save_frame
    83     rtl_setup_call
    84     rtl_fetch_external_args
    85     rtl_set_result
    86     [ ] [ ] (*dummy*).
    87 
    88 (* alias *)
    89 definition rtl_reg_store : register→beval→state rtl_sem_state_params→
    90     res (state rtl_sem_state_params) ≝ acca_store ? rtl_msu_params.
    91 definition rtl_reg_retrieve : state rtl_sem_state_params→register→res beval ≝
    92     acca_retrieve ? rtl_msu_params.
     64axiom rtl_fetch_external_args: external_function → state RTL_state → res (list val).
     65axiom rtl_set_result: list val → list register → state RTL_state → res (state RTL_state).
     66
     67definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st.
     68definition rtl_reg_retrieve ≝ λst.reg_retrieve (regs RTL_state st).
    9369
    9470definition rtl_read_result :
    95  ∀globals. genv globals rtl_params → state rtl_sem_state_params → res (list beval) ≝
    96  λglobals,ge,st.
    97   ! p ← code_pointer_of_address (pc … st) ;
    98   ! fn ← fetch_function … ge p ;
    99   m_mmap … (rtl_reg_retrieve st) (joint_if_result … fn).
     71 ∀globals.genv RTL globals → list register → state RTL_state → res (list beval) ≝
     72 λglobals,ge,rets,st.
     73 m_list_map … (rtl_reg_retrieve st) rets.
    10074
    10175(*CSC: we could use a dependent type here: the list of return values should have
     
    10377  saves the OutOfBounds exception *)
    10478definition rtl_pop_frame:
    105  ∀globals. genv globals rtl_params → state rtl_sem_state_params
    106   res (state rtl_sem_state_params) ≝
    107  λglobals,ge,st.
    108   do ret_vals ← rtl_read_result … ge st ;
     79 ∀globals. genv RTL globals → list register → state RTL_state
     80  res (state RTL_state) ≝
     81 λglobals,ge,ret,st.
     82  do ret_vals ← rtl_read_result … ge ret st ;
    10983  match st_frms ? st with
    11084  [ nil ⇒ Error ? [MSG EmptyStack]
     
    11791       (OK … st) (fr_ret_regs hd) ;
    11892     OK …
    119       (set_frms rtl_sem_state_params tl
    120         (set_regs rtl_sem_state_params (fr_regs hd)
     93      (set_frms RTL_state tl
     94        (set_regs RTL_state (fr_regs hd)
    12195         (set_sp … (fr_sp hd)
    12296          (set_carry … (fr_carry hd)
    12397           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    12498
    125 
    12699(* This code is quite similar to eval_call_block: can we factorize it out? *)
    127 definition eval_tail_call_block:
    128  ∀globals.genv globals rtl_params → state rtl_sem_state_params →
    129   block → call_args rtl_uns_params → IO io_out io_in (trace×(state rtl_sem_state_params)) ≝
    130  λglobals,ge,st,b,args.
    131   ! 〈next, tr, st〉 ← eval_call_block_preamble ? rtl_params rtl_msu_params ge st b args (None ?) ;
    132   match next with
    133   [ None ⇒ (* Paolo: external tailcall, copied from evaluation of return, is it right? *)
    134     ! 〈st,ra〉 ← fetch_ra … st ;
    135     ! st ← rtl_pop_frame … ge st;
    136     return 〈tr,st〉
    137   | Some lbl ⇒
    138     return 〈tr,st〉
    139   ].
    140 
    141 definition block_of_register_pair: register → register → state rtl_sem_state_params → res block ≝
     100definition eval_tailcall_block:
     101 ∀globals.genv RTL globals → state RTL_state →
     102  block → call_args RTL →
     103  (* this is where the result of the current function should be stored *)
     104  call_dest RTL →
     105  IO io_out io_in
     106    ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×(state RTL_state)) ≝
     107 λglobals,ge,st,b,args,ret.
     108  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
     109    match fd with
     110    [ Internal fd ⇒
     111      return 〈FTailInit ?? (block_id b) fd args, st〉
     112    | External fn ⇒
     113      ! params ← rtl_fetch_external_args … fn st : IO ???;
     114      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     115      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     116      (* CSC: XXX bug here; I think I should split it into Byte-long
     117         components; instead I am making a singleton out of it. To be
     118         fixed once we fully implement external functions. *)
     119      let vs ≝ [mk_val ? evres] in
     120      ! st ← rtl_set_result … vs ret st : IO ???;
     121      return 〈FEnd2 ??, st〉
     122    ].
     123
     124definition block_of_register_pair: register → register → state RTL_state → res block ≝
    142125 λr1,r2,st.
    143126 do v1 ← rtl_reg_retrieve st r1 ;
     
    146129 OK … (pblock ptr). 
    147130
    148 definition rtl_exec_extended:
    149  ∀globals. genv globals rtl_params →
    150   rtl_instruction_extension → state rtl_sem_state_params → address
    151    IO io_out io_in ((option (label)) × trace × (state rtl_sem_state_params)) ≝
    152  λglobals,ge,stm,st,next_addr.
     131definition eval_rtl_seq:
     132 ∀globals. genv RTL globals →
     133  rtl_seq → state RTL_state
     134   IO io_out io_in (state RTL_state) ≝
     135 λglobals,ge,stm,st.
    153136  match stm with
    154    [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
     137   [ rtl_stack_address dreg1 dreg2  ⇒
    155138      let sp ≝ sp ? st in
    156139      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
    157140      ! st ← rtl_reg_store dreg1 dpl st ;
    158       ! st ← rtl_reg_store dreg2 dph st ;
    159       return 〈None label,E0, st〉
    160    | rtl_st_ext_call_ptr r1 r2 args dest ⇒
    161      ! b ← block_of_register_pair r1 r2 st : IO ???;
    162      eval_call_block_preamble ? rtl_params rtl_msu_params
    163                               ge st b args (Some ? 〈dest,next_addr〉) ].
    164 
    165 definition rtl_exec_fin_extended:
    166  ∀globals. genv globals rtl_params →
    167   rtl_statement_extension → state rtl_sem_state_params →
    168    IO io_out io_in (trace × (state rtl_sem_state_params)) ≝
    169    λglobals,ge,stm,st.
     141      rtl_reg_store dreg2 dph st
     142   ].
     143
     144definition eval_rtl_call:
     145 ∀globals. genv RTL globals →
     146  rtl_call → state RTL_state →
     147   IO io_out io_in ((step_flow RTL ? Call)×(state RTL_state)) ≝
     148 λglobals,ge,stm,st.
     149  match stm with
     150  [ rtl_call_ptr r1 r2 args dest ⇒
     151    ! b ← block_of_register_pair r1 r2 st : IO ???;
     152    ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
     153    match fd with
     154    [ Internal fd ⇒
     155      return 〈Init ?? (block_id b) fd args dest, st〉
     156    | External fn ⇒
     157      ! params ← rtl_fetch_external_args … fn st : IO ???;
     158      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     159      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     160      (* CSC: XXX bug here; I think I should split it into Byte-long
     161         components; instead I am making a singleton out of it. To be
     162         fixed once we fully implement external functions. *)
     163      let vs ≝ [mk_val ? evres] in
     164      ! st ← rtl_set_result … vs dest st : IO ???;
     165      return 〈Proceed ???, st〉
     166    ]
     167  ].
     168
     169definition eval_rtl_tailcall:
     170 ∀globals. genv RTL globals →
     171  rtl_tailcall → call_dest RTL → state RTL_state →
     172   IO io_out io_in ((fin_step_flow RTL ? Call)×(state RTL_state)) ≝
     173   λglobals,ge,stm,ret,st.
    170174   match stm with
    171    [ rtl_st_ext_tailcall_id id args ⇒
     175   [ rtl_tailcall_id id args ⇒
    172176      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    173       eval_tail_call_block … ge st b args
    174    | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
     177      eval_tailcall_block … ge st b args ret
     178   | rtl_tailcall_ptr r1 r2 args ⇒
    175179      ! b ← block_of_register_pair r1 r2 st : IO ???;
    176       eval_tail_call_block … ge st b args
     180      eval_tailcall_block … ge st b args ret
    177181   ].
    178182
    179 definition rtl_msg_params : more_sem_genv_params rtl_params ≝
    180   mk_more_sem_genv_params rtl_params rtl_msu_params
     183definition RTL_semantics ≝
     184  mk_more_sem_unserialized_params RTL (joint_internal_function RTL)
     185    RTL_state
     186    reg_store reg_retrieve rtl_arg_retrieve
     187    reg_store reg_retrieve rtl_arg_retrieve
     188    reg_store reg_retrieve rtl_arg_retrieve
     189    reg_store reg_retrieve rtl_arg_retrieve
     190    rtl_arg_retrieve
     191    (λenv,p. let 〈dest,src〉 ≝ p in
     192      ! v ← rtl_arg_retrieve env src ;
     193      reg_store dest v env)
     194    rtl_fetch_ra
     195    rtl_init_local
     196    rtl_save_frame
     197    rtl_setup_call
     198    rtl_fetch_external_args
     199    rtl_set_result
     200    [ ] [ ]
    181201    rtl_read_result
    182     rtl_exec_extended
    183     rtl_exec_fin_extended
    184     rtl_pop_frame.
    185 
    186 
    187 
    188 definition rtl_sem_params : sem_params ≝ make_sem_graph_params … rtl_msg_params.
    189 
    190 definition rtl_fullexec ≝ joint_fullexec … rtl_sem_params.
     202    eval_rtl_seq
     203    eval_rtl_tailcall
     204    eval_rtl_call.
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r2214 r2217  
    88include alias "ASM/BitVector.ma".
    99include alias "arithmetics/nat.ma".
     10
     11definition rtl_fresh_reg:
     12 ∀globals.freshT RTL globals register ≝
     13  λglobals,def.
     14    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     15    〈set_locals ?? (set_runiverse ?? def runiverse)(r::joint_if_locals ?? def), r〉.
     16
     17definition rtl_fresh_reg_no_local :
     18 ∀globals.freshT RTL globals register ≝
     19  λglobals,def.
     20    let 〈r, runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
     21    〈set_runiverse ?? def runiverse, r〉.
     22
    1023definition size_of_sig_type ≝
    1124  λsig.
     
    4861  λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf).
    4962
    50 definition m_fresh : ∀tag.state_monad (universe tag) (identifier tag) ≝
    51 λtag,univ.let pr ≝ fresh … univ in 〈\snd pr, \fst pr〉.
    52 
    53 let rec register_freshes (n: nat) on n :
    54   state_monad (universe RegisterTag) (Σl.|l| = n) ≝
    55   match n return λx.state_monad ? (Σl.|l| = x) with
    56   [ O ⇒ return «[ ],?»
    57   | S n' ⇒
    58     ! r ← m_fresh ?;
    59     ! res ← register_freshes n';
    60     return «r::res,?»
    61   ].[2: cases res -res #res #EQ <EQ] % qed.
    62 
    6363definition initialize_local_env_internal :
    64   (universe RegisterTag × local_env) → (register×typ) → (universe RegisterTag × local_env) ≝
    65   λlenv_runiverse,r_sig.
    66   let 〈runiverse,lenv〉 ≝ lenv_runiverse in
     64  ∀globals.
     65  ((joint_internal_function RTL globals) × local_env) → (register×typ) →
     66  ((joint_internal_function RTL globals) × local_env) ≝
     67  λglobals,def_env,r_sig.
     68  let 〈def,lenv〉 ≝ def_env in
    6769  let 〈r, sig〉 ≝ r_sig in
    6870  let size ≝ size_of_sig_type sig in
    69   let 〈runiverse,rs〉 ≝ register_freshes size runiverse in
    70     〈runiverse,add … lenv r rs〉.
    71 
    72 definition initialize_local_env :
    73   list (register×typ) →
    74   state_monad (universe RegisterTag) local_env ≝
    75   λregisters,runiverse.
    76   foldl … initialize_local_env_internal 〈runiverse,empty_map …〉 registers.
     71  let 〈def,rs〉 ≝ repeat_fresh … (rtl_fresh_reg_no_local globals) size def in
     72    〈def,add … lenv r rs〉.
    7773
    7874include alias "common/Identifiers.ma".
     
    8480  | cons hd tl ⇒ λprf.find_local_env (\fst hd) lenv ? @ map_list_local_env lenv tl ?
    8581  ].cases prf #A #B assumption qed.
     82
     83definition initialize_local_env :
     84  ∀globals.
     85  list (register×typ) →
     86  freshT RTL globals local_env ≝
     87  λglobals,registers,def.
     88  foldl ?? (initialize_local_env_internal globals) 〈def,empty_map …〉 registers.
     89
     90lemma initialize_local_env_in : ∀globals,l,def,r.
     91  Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env globals l def).
     92#globals #l #U #r @(list_elim_left … l)
     93[ *
     94| * #tl #sig #hd #IH #G elim (Exists_append … G) -G
     95  whd in match initialize_local_env; normalize nodelta
     96  >foldl_step change with (initialize_local_env ???) in match (foldl ?????);
     97  [ #H lapply (IH H)
     98  | * [2: *] #EQ destruct(EQ)
     99  ] 
     100  cases (initialize_local_env ???)
     101  #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta
     102  elim (repeat_fresh ??????) #U'' #rs
     103  [ >mem_set_add @orb_Prop_r assumption
     104  | @mem_set_add_id
     105  ]
     106qed.
     107
     108example proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr.
     109// qed-.
     110example proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr.
     111// qed-.
     112
     113definition initialize_locals_params_ret :
     114  ∀globals.
     115  (* locals *) list (register×typ) →
     116  (* params *) list (register×typ) →
     117  (* return *) option (register×typ) →
     118  freshT RTL globals local_env ≝
     119  λglobals,locals,params,ret,def.
     120  let 〈def',lenv〉 as EQ ≝
     121    initialize_local_env globals
     122    ((match ret with
     123     [ Some r_sig ⇒ [r_sig]
     124     | None ⇒ [ ]
     125     ]) @ locals @ params) def in
     126  let locals' ≝ map_list_local_env lenv locals ? in
     127  let params' ≝ map_list_local_env lenv params ? in
     128  let ret' ≝ match ret return λx.ret = x → ? with
     129    [ Some r_sig ⇒ λprf.find_local_env (\fst r_sig) lenv ?
     130    | None ⇒ λ_.[ ]
     131    ] (refl …) in
     132  let def'' ≝
     133    mk_joint_internal_function RTL globals
     134      (joint_if_luniverse … def') (joint_if_runiverse … def') ret'
     135      params' locals' (joint_if_stacksize … def')
     136      (joint_if_code … def') (joint_if_entry … def') (joint_if_exit … def') in
     137   〈def'', lenv〉. @hide_prf
     138[ >(proj2_rewrite ????? EQ)
     139  @initialize_local_env_in >prf %1 %
     140|*: >(proj2_rewrite ????? EQ)
     141  @(All_mp ??? (λpr.initialize_local_env_in ??? (\fst pr)))
     142  [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) params))
     143    [ #a #H @Exists_append_r @Exists_append_r @H
     144    | generalize in match params;
     145    ]
     146  | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) locals))
     147    [ #a #H @Exists_append_r @Exists_append_l @H
     148    | generalize in match locals;
     149    ]
     150  ]
     151  #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G}
     152]
     153qed.
    86154
    87155definition make_addr ≝
     
    834902qed.
    835903
    836 lemma initialize_local_env_in : ∀l,runiverse,r.
    837   Exists ? (λx.\fst x = r) l → r ∈ \snd (initialize_local_env l runiverse).
    838 #l #U #r @(list_elim_left … l)
    839 [ *
    840 | * #tl #sig #hd #IH #G elim (Exists_append … G) -G
    841   whd in match initialize_local_env; normalize nodelta
    842   >foldl_step change with (initialize_local_env ??) in match (foldl ?????);
    843   [ #H lapply (IH H)
    844   | * [2: *] #EQ destruct(EQ)
    845   ] 
    846   cases (initialize_local_env ??)
    847   #U' #env' [#G] whd in match initialize_local_env_internal; normalize nodelta
    848   elim (register_freshes ??) #U'' #rs
    849   [ >mem_set_add @orb_Prop_r assumption
    850   | @mem_set_add_id
    851   ]
    852 qed.
    853 
    854 definition proj1_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → a = \fst pr.
    855 // qed.
    856 definition proj2_rewrite : ∀A,B,a,b.∀pr : A×B.〈a,b〉 = pr → b = \snd pr.
    857 // qed.
    858 
    859 
    860904(* XXX: we use a "hack" here to circumvent the proof obligations required to
    861905   create res, an empty internal_function record.  we insert into our graph
     
    865909  λglobals: list ident.
    866910  λdef.
    867   let runiverse ≝ f_reggen def in
    868   let 〈runiverse',lenv〉 as pr_eq ≝ initialize_local_env
    869     (match f_result def with [ None ⇒ [ ] | Some r_sig ⇒ [r_sig]] @
    870      f_params def @ f_locals def) runiverse in
    871   let params' ≝ map_list_local_env lenv (f_params def) ? in
    872   let locals' ≝ map_list_local_env lenv (f_locals def) ? in
    873   let result' ≝
    874     match (f_result def) return λx.f_result def = x → ? with
    875     [ None ⇒ λ_.[ ]
    876     | Some r_typ ⇒ λEQ.
    877        find_local_env (\fst r_typ) lenv ?
    878     ] (refl …)
    879   in
     911  let runiverse' ≝ f_reggen def in
    880912  let luniverse' ≝ f_labgen def in
    881913  let stack_size' ≝ f_stacksize def in
     
    887919  let graph' ≝ add LabelTag ? graph' exit'
    888920    (RETURN …) in
     921  let init ≝
     922    mk_joint_internal_function RTL globals luniverse' runiverse' [ ] [ ]
     923     [ ] stack_size' graph' (pi1 … entry') (pi1 … exit') in
     924  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
     925    (f_locals def) (f_params def) (f_result def) init in
    889926  let f_trans ≝ λlbl,stmt,def.
    890927    let pr ≝ translate_statement … lenv stmt in
    891     b_adds_graph … (rtl_ertl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
    892   let res ≝
    893     mk_joint_internal_function RTL globals luniverse' runiverse' result' params'
    894      locals' stack_size' graph' (pi1 … entry') (pi1 … exit') in
    895     foldi … f_trans (f_graph def) res. 
    896    
    897 [1,2: >graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add
    898 | >(proj2_rewrite ????? pr_eq)
    899   @initialize_local_env_in >EQ normalize nodelta %1 %
    900 |*: >(proj2_rewrite ????? pr_eq)
    901   @(All_mp ??? (λpr.initialize_local_env_in ?? (\fst pr)))
    902   [ @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_locals def)))
    903     [ #a #H @Exists_append_r @Exists_append_r @H
    904     | generalize in match (f_locals def);
    905     ]
    906   | @(All_mp … (λpr.Exists ? (λx.\fst x = \fst pr) (f_params def)))
    907     [ #a #H @Exists_append_r @Exists_append_l @H
    908     | generalize in match (f_params def);
    909     ]
    910   ]
    911   #l elim l [1,3: %] #hd #tl #IH % [1,3: %1 %] @(All_mp … IH) #x #G %2{G}
    912 ]
     928    b_adds_graph … (rtl_fresh_reg …) (dpi1 … pr) lbl (dpi2 … pr) def in
     929  foldi … f_trans (f_graph def) init'.
     930@hide_prf
     931>graph_code_has_point @map_mem_prop [@graph_add_lookup] @graph_add
    913932qed.
    914933
  • 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.