Changeset 2286 for src/RTL


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

Location:
src/RTL
Files:
4 deleted
4 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1348 r2286  
    11include "joint/Joint.ma".
    22
    3 (*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
    4   are not sequential. Thus there is a dummy label at the moment in the code.
    5   To be fixed once we understand exactly what to do with tail calls. *)
    6 inductive rtl_statement_extension: Type[0] ≝
    7   | rtl_st_ext_stack_address: register → register → rtl_statement_extension
    8   | rtl_st_ext_call_ptr: register → register → list register → list register → rtl_statement_extension
    9   | rtl_st_ext_tailcall_id: ident → list register → rtl_statement_extension
    10   | rtl_st_ext_tailcall_ptr: register → register → list register → rtl_statement_extension.
     3inductive rtl_seq : Type[0] ≝
     4  | rtl_stack_address: register → register → rtl_seq.
     5 
     6inductive rtl_call : Type[0] ≝
     7  | rtl_call_ptr: register → register → list psd_argument → list register → rtl_call.
    118
    12 definition rtl_params__: params__ ≝
    13  mk_params__ register register register register (register × register) register
    14   (list register) (list register) rtl_statement_extension.
    15 definition rtl_params_: params_ ≝ graph_params_ rtl_params__.
    16 definition rtl_params0: params0 ≝ mk_params0 rtl_params__ (list register) (list register).
    17 definition rtl_params1: params1 ≝ rtl_ertl_params1 rtl_params0.
    18 definition rtl_params: ∀globals. params globals ≝ rtl_ertl_params rtl_params0.
     9inductive rtl_tailcall : Type[0] ≝
     10  | rtl_tailcall_id: ident → list psd_argument → rtl_tailcall
     11  | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall.
    1912
    20 definition rtl_statement ≝ joint_statement rtl_params_.
     13definition RTL_uns ≝ mk_unserialized_params
     14    (* acc_a_reg ≝ *) register
     15    (* acc_b_reg ≝ *) register
     16    (* acc_a_arg ≝ *) psd_argument
     17    (* acc_b_arg ≝ *) psd_argument
     18    (* dpl_reg   ≝ *) register
     19    (* dph_reg   ≝ *) register
     20    (* dpl_arg   ≝ *) psd_argument
     21    (* dph_arg   ≝ *) psd_argument
     22    (* snd_arg   ≝ *) psd_argument
     23    (* pair_move ≝ *) (register × psd_argument)
     24    (* call_args ≝ *) (list psd_argument)
     25    (* call_dest ≝ *) (list register)
     26    (* ext_seq ≝ *) rtl_seq
     27    (* ext_call ≝ *) rtl_call
     28    (* ext_tailcall ≝ *) rtl_tailcall
     29    (* paramsT ≝ *) (list register)
     30    (* localsT ≝ *) register.
    2131
    22 definition rtl_internal_function ≝
    23   λglobals. joint_internal_function … (rtl_params globals).
     32definition RTL ≝ mk_graph_params RTL_uns.
     33definition rtl_program ≝ joint_program RTL.
    2434
    25 definition rtl_program ≝ joint_program rtl_params.
     35interpretation "move" 'mov r a = (MOVE RTL ? (mk_Prod ? psd_argument r a)).
     36
     37(* aid unification *)
     38include "hints_declaration.ma".
     39unification hint 0 ≔
     40(*---------------*) ⊢
     41acc_a_reg RTL ≡ register.
     42unification hint 0 ≔
     43(*---------------*) ⊢
     44acc_b_reg RTL ≡ register.
     45unification hint 0 ≔
     46(*---------------*) ⊢
     47acc_a_arg RTL ≡ psd_argument.
     48unification hint 0 ≔
     49(*---------------*) ⊢
     50acc_b_arg RTL ≡ psd_argument.
     51unification hint 0 ≔
     52(*---------------*) ⊢
     53dpl_reg RTL ≡ register.
     54unification hint 0 ≔
     55(*---------------*) ⊢
     56dph_reg RTL ≡ register.
     57unification hint 0 ≔
     58(*---------------*) ⊢
     59dpl_arg RTL ≡ psd_argument.
     60unification hint 0 ≔
     61(*---------------*) ⊢
     62dph_arg RTL ≡ psd_argument.
     63unification hint 0 ≔
     64(*---------------*) ⊢
     65snd_arg RTL ≡ psd_argument.
     66unification hint 0 ≔
     67(*---------------*) ⊢
     68pair_move RTL ≡ register × psd_argument.
     69unification hint 0 ≔
     70(*---------------*) ⊢
     71call_args RTL ≡ list psd_argument.
     72unification hint 0 ≔
     73(*---------------*) ⊢
     74call_dest RTL ≡ list register.
     75
     76unification hint 0 ≔
     77(*---------------*) ⊢
     78ext_seq RTL ≡ rtl_seq.
     79unification hint 0 ≔
     80(*---------------*) ⊢
     81ext_call RTL ≡ rtl_call.
     82unification hint 0 ≔
     83(*---------------*) ⊢
     84ext_tailcall RTL ≡ rtl_tailcall.
     85
     86coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg RTL ≝ psd_argument_from_reg
     87  on _r : register to snd_arg RTL.
     88coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
     89  on _b : Byte to snd_arg RTL.
     90
    2691
    2792(************ Same without tail calls ****************)
    2893
    29 (*CSC: XXX PROBLEM HERE. Tailcalls are not instructions, but statements since they
    30   are not sequential. Thus there is a dummy label at the moment in the code.
    31   To be fixed once we understand exactly what to do with tail calls. *)
    32 inductive rtlntc_statement_extension: Type[0] ≝
    33   | rtlntc_st_ext_stack_address: register → register → rtlntc_statement_extension
    34   | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
     94definition RTL_ntc ≝ mk_graph_params (mk_unserialized_params
     95    (* acc_a_reg ≝ *) register
     96    (* acc_b_reg ≝ *) register
     97    (* acc_a_arg ≝ *) psd_argument
     98    (* acc_b_arg ≝ *) psd_argument
     99    (* dpl_reg   ≝ *) register
     100    (* dph_reg   ≝ *) register
     101    (* dpl_arg   ≝ *) psd_argument
     102    (* dph_arg   ≝ *) psd_argument
     103    (* snd_arg   ≝ *) psd_argument
     104    (* pair_move ≝ *) (register × psd_argument)
     105    (* call_args ≝ *) (list psd_argument)
     106    (* call_dest ≝ *) (list register)
     107    (* ext_seq ≝ *) rtl_seq
     108    (* ext_call ≝ *) rtl_call
     109    (* ext_tailcall ≝ *) void
     110    (* paramsT ≝ *) (list register)
     111    (* localsT ≝ *) register).
    35112
    36 definition rtlntc_params__: params__ ≝
    37  mk_params__ register register register register (register × register) register
    38   (list register) (list register) rtlntc_statement_extension.
    39 definition rtlntc_params_: params_ ≝ graph_params_ rtlntc_params__.
    40 definition rtlntc_params0: params0 ≝ mk_params0 rtlntc_params__ (list register) (list register).
    41 definition rtlntc_params1: params1 ≝ rtl_ertl_params1 rtlntc_params0.
    42 definition rtlntc_params: ∀globals. params globals ≝ rtl_ertl_params rtlntc_params0.
    43 
    44 definition rtlntc_statement ≝ joint_statement rtlntc_params_.
    45 
    46 definition rtlntc_internal_function ≝
    47   λglobals. joint_internal_function … (rtlntc_params globals).
    48 
    49 definition rtlntc_program ≝ joint_program rtlntc_params.
     113definition rtl_ntc_program ≝ joint_program RTL_ntc.
  • src/RTL/RTLTailcall.ma

    r2103 r2286  
    55  λexit: label.
    66  λlbl: label.
    7   λstmt: rtl_statement globals.
    8   λgraph: codeT … (rtlntc_params globals).
     7  λstmt: joint_statement RTL globals.
     8  λgraph: codeT RTL_ntc globals.
    99  match stmt with
    10   [ sequential seq DUMMY
    11      match seq with
    12       [ extension ext ⇒
     10  [ final fin
     11     match fin with
     12      [ tailcall ext ⇒
    1313         match ext with
    14           [ rtl_st_ext_tailcall_id f args ⇒
    15               add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit)
    16           | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
    17               add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
    18           | _ ⇒ graph ]
     14          [ rtl_tailcall_id f args ⇒
     15              add … graph lbl (sequential … (CALL_ID RTL_ntc ? f args [ ]) exit)
     16          | rtl_tailcall_ptr f1 f2 args ⇒
     17              add … graph lbl (sequential RTL_ntc ? (rtl_call_ptr f1 f2 args [ ] : ext_call RTL_ntc) exit)
     18          ]
    1919      | _ ⇒ graph ]
    2020  | _ ⇒ graph ].
     
    2323  λglobals.
    2424  λexit: label.
    25   λgraph: codeT … (rtl_params globals).
     25  λgraph: codeT RTL globals.
    2626    foldi ? ? ? (simplify_stmt globals exit) graph (empty_map …).
    2727
    2828axiom simplify_graph_preserves_labels:
    2929  ∀globals.
    30   ∀g: codeT … (rtl_params globals).
    31   ∀l: label.
     30  ∀g: codeT RTL globals.
    3231  ∀exit: label.
    33     lookup ? ? g l ≠ None ? → lookup ? ? (simplify_graph globals exit g) l ≠ None ?.
     32  ∀l: label.l ∈ g → l ∈ simplify_graph globals exit g.
    3433   
    3534definition simplify_internal :
    3635 ∀globals.
    37   joint_internal_function … (rtl_params globals)
    38    joint_internal_function … (rtlntc_params globals)
     36  joint_internal_function RTL globals
     37   joint_internal_function RTL_ntc globals
    3938
    4039  λglobals,def.
     
    4948qed.
    5049
    51 definition tailcall_simplify : rtl_program → rtlntc_program ≝
     50definition tailcall_simplify : rtl_program → rtl_ntc_program ≝
    5251 λp. transform_program … p (λvarnames. transf_fundef … (simplify_internal varnames)).
  • src/RTL/RTLToERTL.ma

    r2103 r2286  
    77include alias "basics/lists/list.ma".
    88
    9 definition save_hdws ≝
    10  λglobals,l.
     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〉.
     14
     15definition save_hdws :
     16  ∀globals.list (register×Register) → list (joint_seq ERTL globals) ≝
     17 λglobals.
    1118  let save_hdws_internal ≝
    12    λdestr_srcr.λstart_lbl.
    13     let 〈destr, srcr〉 ≝ destr_srcr in
    14      adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] start_lbl
    15   in
    16    map ? ? save_hdws_internal l.
    17 
    18 definition restore_hdws ≝
    19   λglobals,l.
     19   λdestr_srcr.PSD (\fst destr_srcr) ← HDW (\snd destr_srcr) in
     20  map ?? save_hdws_internal.
     21
     22definition restore_hdws :
     23  ∀globals.list (psd_argument×Register) → list (joint_seq ERTL globals) ≝
     24  λglobals.
    2025   let restore_hdws_internal ≝
    21     λsrcr_destr: register × Register.
    22     λstart_lbl: label.
    23      let 〈srcr, destr〉 ≝ srcr_destr in
    24      adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] start_lbl
    25    in
    26     map ? ? restore_hdws_internal l.
    27 
    28 definition get_params_hdw ≝
    29   λglobals.
    30   λparams: list register.
    31   match params with
    32   [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] start_lbl]
    33   | _ ⇒
    34     let l ≝ zip_pottier ? ? params RegisterParams in
    35       save_hdws globals l ].
    36 
    37 definition get_param_stack ≝
    38   λglobals.
    39   λoff: nat.
    40   λdestr.
    41   λstart_lbl, dest_lbl: label.
    42   λdef.
    43   let 〈def, addr1〉 ≝ fresh_reg … def in
    44   let 〈def, addr2〉 ≝ fresh_reg … def in
    45   let 〈def, tmpr〉 ≝ fresh_reg … def in
    46   let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
    47   adds_graph ertl_params1 globals [
    48     sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1));
    49     sequential ertl_params_ … (INT … tmpr int_offset);
    50     sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr);
    51     sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
    52     sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr);
    53     sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0));
    54     sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
    55     sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr);
    56     sequential ertl_params_ … (LOAD … destr addr1 addr2)
    57   ] start_lbl dest_lbl def.
    58  
    59 definition get_params_stack ≝
    60   λglobals,params.
    61   match params with
    62   [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ]
    63   | _ ⇒ mapi ? ? (get_param_stack globals) params ].
     26    λdestr_srcr:psd_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in
     27    map ? ? restore_hdws_internal.
     28
     29definition get_params_hdw :
     30  ∀globals.list register → list (joint_seq ERTL globals) ≝
     31  λglobals,params.
     32  save_hdws … (zip_pottier … params RegisterParams).
     33
     34definition get_param_stack :
     35  ∀globals.register → register → register →
     36  list (joint_seq ERTL globals) ≝
     37  λglobals,addr1,addr2,destr.
     38  (* liveness analysis will erase the last useless ops *)
     39  [ LOAD ?? destr addr1 addr2 ;
     40    addr1 ← addr1 .Add. (int_size : Byte) ;
     41    addr2 ← addr2 .Addc. zero_byte
     42  ].
     43
     44definition get_params_stack :
     45  ∀globals.list register →
     46  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
     47  λglobals,params.
     48  νtmpr,addr1,addr2 in
     49  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
     50  [ (ertl_frame_size tmpr : joint_seq ??) ;
     51    CLEAR_CARRY ?? ;
     52    tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *)
     53    PSD addr1 ← HDW RegisterSPL ;
     54    PSD addr2 ← HDW RegisterSPH ;
     55    addr1 ← addr1 .Add. tmpr ;
     56    addr2 ← addr2 .Addc. zero_byte ] @   
     57  flatten … (map ?? (get_param_stack globals addr1 addr2) params).
    6458
    6559definition get_params ≝
     
    6761  let n ≝ min (length … params) (length … RegisterParams) in
    6862  let 〈hdw_params, stack_params〉 ≝ list_split … n params in
    69   let hdw_params ≝ get_params_hdw globals hdw_params in
    70     hdw_params @ (get_params_stack … stack_params).
    71 
    72 definition add_prologue ≝
    73   λglobals.
    74   λparams: list register.
    75   λsral.
    76   λsrah.
    77   λsregs.
    78   λdef.
    79   let start_lbl ≝ joint_if_entry … (ertl_params globals) def in
    80   let 〈tmp_lbl, def〉 ≝ fresh_label … def in
    81   match lookup … (joint_if_code … def) start_lbl
    82     return λx. x ≠ None ? → ertl_internal_function globals with
    83   [ None ⇒ λnone_absrd. ⊥
    84   | Some last_stmt ⇒ λsome_prf.
    85     let def ≝
    86       add_translates …
    87          ((adds_graph ertl_params1 … [
    88                      sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame)
    89                    ]) ::
    90          (adds_graph ertl_params1 … [
    91                       sequential ertl_params_ … (POP … sral);
    92                       sequential ertl_params_ … (POP … srah)
    93                    ]) ::
    94          (save_hdws … sregs) @
    95          (get_params … params))
    96         start_lbl tmp_lbl def
    97     in
    98       add_graph … tmp_lbl last_stmt def
    99   ] ?.
    100 [ cases start_lbl #x #H cases daemon (* @H *) (*CSC: XXXX, no Russell *)
    101 | cases (none_absrd) /2/ ]
    102 qed.
    103 
    104 definition save_return ≝
    105   λglobals.
    106   λret_regs.
    107   λstart_lbl: label.
    108   λdest_lbl: label.
    109   λdef: ertl_internal_function globals.
    110   let 〈def, tmpr〉 ≝ fresh_reg … def in
     63  get_params_hdw globals hdw_params @@ get_params_stack … stack_params.
     64
     65definition prologue :
     66  ∀globals.list register → register → register → list (register×Register) →
     67  bind_new (localsT ERTL) (list (joint_seq ERTL globals)) ≝
     68  λglobals,params,sral,srah,sregs.
     69  [ (ertl_new_frame : joint_seq ??) ;
     70    POP … sral ;
     71    POP … srah
     72  ] @@ save_hdws … sregs @@ get_params … params.
     73
     74definition save_return :
     75  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
     76  λglobals,ret_regs.
    11177  match reduce_strong ? ? RegisterSTS ret_regs with
    11278  [ mk_Sig crl crl_proof ⇒
     
    11480    let commonr ≝ \fst (\snd crl) in
    11581    let restl ≝ \snd (\fst crl) in
    116     let restr ≝ \snd (\snd crl) in
    117     let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in
    118     let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in
    119     let saves ≝ map2 … f_save commonl commonr crl_proof in
    120     let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) in
    121     let defaults ≝ map … f_default restl in
    122       adds_graph ertl_params1 ? (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
    123   ].
    124 
    125 definition assign_result ≝
    126   λglobals.λstart_lbl: label.
    127   match reduce_strong ? ? RegisterRets RegisterSTS with
     82    (* let restr ≝ \snd (\snd crl) in *)
     83    map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @
     84    map … (λst.HDW st ← zero_byte) restl
     85  ].
     86
     87definition assign_result : ∀globals.list (joint_seq ERTL globals) ≝
     88  λglobals.
     89  match reduce_strong ?? RegisterRets RegisterSTS with
    12890  [ mk_Sig crl crl_proof ⇒
    12991    let commonl ≝ \fst (\fst crl) in
    13092    let commonr ≝ \fst (\snd crl) in
    131     let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in
    132     let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
    133       adds_graph ertl_params1 … insts start_lbl
    134   ].
    135 
    136 definition add_epilogue ≝
    137   λglobals.
    138   λret_regs.
    139   λsral.
    140   λsrah.
    141   λsregs.
    142   λdef.
    143   let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
    144   let 〈tmp_lbl, def〉 ≝ fresh_label … def in
    145   match lookup … (joint_if_code … def) start_lbl
    146     return λx. x ≠ None ? → ertl_internal_function globals with
    147   [ None ⇒ λnone_absrd. ⊥
    148   | Some last_stmt ⇒ λsome_prf.
    149     let def ≝
    150       add_translates ertl_params1 … (
    151         [save_return globals ret_regs] @
    152         restore_hdws … sregs @
    153         [adds_graph ertl_params1 … [
    154           sequential ertl_params_ … (PUSH … srah);
    155           sequential ertl_params_ … (PUSH … sral)
    156         ]] @
    157         [adds_graph ertl_params1 … [
    158           sequential ertl_params_ … (extension … ertl_st_ext_del_frame)
    159         ]] @
    160         [assign_result globals]
    161       ) start_lbl tmp_lbl def
    162     in
    163     let def' ≝ add_graph … tmp_lbl last_stmt def in
    164       set_joint_if_exit … tmp_lbl def' ?
    165   ] ?.
    166 [ cases start_lbl #x #H cases daemon (* @H *) (* CSC: XXXX *)
    167 | cases (none_absrd) /2/
    168 | cases daemon (* CSC: XXXXX *)
    169 ]
    170 qed.
    171  
    172 
    173 definition allocate_regs ≝
    174   λglobals.
    175   λrs.
    176   λsaved: rs_set rs.
    177   λdef.
     93    map2 … (λret,st.HDW ret ← HDW st) commonl commonr crl_proof
     94  ].
     95
     96definition epilogue :
     97  ∀globals.list register → register → register → list (register × Register) →
     98  list (joint_seq ERTL globals) ≝
     99  λglobals,ret_regs,sral,srah,sregs.
     100  save_return … (map … (Reg ?) ret_regs) @
     101  restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
     102  [ PUSH ERTL ? srah ;
     103    PUSH … sral ;
     104    ertl_del_frame ] @
     105  assign_result globals.
     106
     107definition allocate_regs :
     108  ∀globals,rs.rs_set rs →
     109  freshT ERTL globals (list (register×Register)) ≝
     110  λglobals,rs,saved,def.
    178111   let allocate_regs_internal ≝
    179112    λr: Register.
    180113    λdef_sregs.
    181     let 〈def, sregs〉 ≝ def_sregs in
    182     let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in
    183       〈def, 〈r', r〉 :: sregs〉
    184    in
    185     rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
    186    
    187 definition add_pro_and_epilogue ≝
    188   λglobals.
    189   λparams.
    190   λret_regs.
    191   λdef.
    192   match fresh_regs_strong … globals def 2 with
    193   [ mk_Sig def_sra def_sra_proof ⇒
    194     let def ≝ \fst def_sra in
    195     let sra ≝ \snd def_sra in
    196     let sral ≝ nth_safe ? 0 sra ? in
    197     let srah ≝ nth_safe ? 1 sra ? in
    198     let 〈def, sregs〉 ≝ allocate_regs … register_list_set RegisterCalleeSaved def in
    199     let def ≝ add_prologue … params sral srah sregs def in
    200     let def ≝ add_epilogue … ret_regs sral srah sregs def in
    201       def
    202   ].
    203 >def_sra_proof //
    204 qed.
    205 
    206 definition set_params_hdw ≝
    207   λglobals,params.
    208   match params with
    209   [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl]
    210   | _ ⇒
    211     let l ≝ zip_pottier ? ? params RegisterParams in
    212       restore_hdws globals l
    213   ].
    214 
    215 definition set_param_stack ≝
    216   λglobals.
    217   λoff.
    218   λsrcr.
    219   λstart_lbl: label.
    220   λdest_lbl: label.
    221   λdef: ertl_internal_function globals.
    222   let 〈def, addr1〉 ≝ fresh_reg … def in
    223   let 〈def, addr2〉 ≝ fresh_reg … def in
    224   let 〈def, tmpr〉 ≝ fresh_reg … def in
    225   let 〈ignore, int_off〉 ≝ half_add ? off int_size in
    226     adds_graph ertl_params1 … [
    227       sequential ertl_params_ … (INT … addr1 int_off);
    228       sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
    229       sequential ertl_params_ … (CLEAR_CARRY …);
    230       sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1);
    231       sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
    232       sequential ertl_params_ … (INT … addr2 (zero ?));
    233       sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2);
    234       sequential ertl_params_ … (STORE … addr1 addr2 srcr)
    235     ] start_lbl dest_lbl def.   
    236 
    237 definition set_params_stack ≝
    238   λglobals,params.
    239   match params with
    240   [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] start_lbl]
    241   | _ ⇒
    242     let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
    243       mapi ? ? f params].
     114    let 〈def, r'〉 ≝ ertl_fresh_reg … (\fst def_sregs) in
     115    〈def, 〈r', r〉::\snd def_sregs〉 in
     116  rs_fold ?? allocate_regs_internal saved 〈def, [ ]〉.
     117
     118definition add_pro_and_epilogue :
     119  ∀globals.list register → list register →
     120  joint_internal_function ERTL globals →
     121  joint_internal_function ERTL globals ≝
     122  λglobals,params,ret_regs,def.
     123  let start_lbl ≝ joint_if_entry … def in
     124  let end_lbl ≝ joint_if_exit … def in
     125  state_run … def (
     126    ! sral ← ertl_fresh_reg … ;
     127    ! srah ← ertl_fresh_reg … ;
     128    ! sregs ← allocate_regs … register_list_set RegisterCalleeSaved ;
     129    ! prologue' ← bcompile … (ertl_fresh_reg …) (prologue … params sral srah sregs) ;
     130    let epilogue' ≝ epilogue … ret_regs sral srah sregs in
     131    ! def' ← state_get … ;
     132    let def'' ≝ insert_prologue … prologue' def' in
     133    return insert_epilogue … epilogue' def''
     134  ).
     135
     136definition set_params_hdw :
     137  ∀globals.list psd_argument → list (joint_seq ERTL globals) ≝
     138  λglobals,params.
     139  restore_hdws globals (zip_pottier ? ? params RegisterParams).
     140
     141(* Paolo: The following can probably be done way more efficiently with INC DPTR *)
     142
     143definition set_param_stack :
     144  ∀globals.register → register → psd_argument →
     145  list (joint_seq ERTL globals) ≝
     146  λglobals,addr1,addr2,arg.
     147  [ STORE … addr1 addr2 arg ;
     148    addr1 ← addr1 .Add. (int_size : Byte) ;
     149    addr2 ← addr2 .Addc. zero_byte
     150  ].
     151
     152definition set_params_stack :
     153  ∀globals.list psd_argument → bind_new (localsT ERTL) ? ≝
     154  λglobals,params.
     155  νaddr1,addr2 in
     156  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
     157  [ PSD addr1 ← HDW RegisterSPL ;
     158    PSD addr2 ← HDW RegisterSPH ;
     159    CLEAR_CARRY ?? ;
     160    addr1 ← addr1 .Sub. params_length_byte ;
     161    addr2 ← addr2 .Sub. zero_byte
     162  ] @
     163  flatten … (map … (set_param_stack globals addr1 addr2) params).
    244164
    245165definition set_params ≝
     
    249169  let hdw_params ≝ \fst hdw_stack_params in
    250170  let stack_params ≝ \snd hdw_stack_params in
    251     set_params_hdw globals hdw_params @ set_params_stack globals stack_params.
    252 
    253 definition fetch_result ≝
    254   λglobals.
    255   λret_regs.
    256   λstart_lbl: label.
    257   match reduce_strong ? ? RegisterSTS RegisterRets with
    258   [ mk_Sig crl first_crl_proof ⇒
     171  set_params_hdw globals hdw_params @@ set_params_stack globals stack_params.
     172
     173definition fetch_result :
     174  ∀globals.list register → list (joint_seq ERTL globals) ≝
     175  λglobals,ret_regs.
     176  match reduce_strong ?? RegisterSTS RegisterRets with
     177  [ mk_Sig crl crl_proof ⇒
    259178    let commonl ≝ \fst (\fst crl) in
    260179    let commonr ≝ \fst (\snd crl) in
    261     let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) in
    262     let saves ≝ map2 ? ? ? f_save commonl commonr ? in
    263     match reduce_strong ? ? ret_regs RegisterSTS with
    264     [ mk_Sig crl second_crl_proof ⇒
     180    map2 … (λst,r.HDW st ← HDW r) commonl commonr crl_proof @
     181    match reduce_strong ?? ret_regs RegisterSTS with
     182    [ mk_Sig crl crl_proof ⇒
    265183      let commonl ≝ \fst (\fst crl) in
    266184      let commonr ≝ \fst (\snd crl) in
    267       let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) in
    268       let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
    269         adds_graph ertl_params1 … (saves @ restores) start_lbl]].
    270 [@second_crl_proof | @first_crl_proof]
    271 qed.
    272 
    273 definition translate_call_id ≝
    274   λglobals,f.
    275   λargs.
    276   λret_regs.
    277   λstart_lbl.
    278   λdest_lbl.
    279   λdef.
    280   let nb_args ≝ |args| in
    281     add_translates ertl_params1 globals (
    282       set_params … args @ [
    283       adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ];
    284       fetch_result … ret_regs
     185      map2 … (λret,st.PSD ret ← HDW st) commonl commonr crl_proof
     186    ]
     187  ].
     188
     189definition translate_step :
     190  ∀globals.label → joint_step RTL_ntc globals →
     191    bind_seq_block ERTL globals (joint_step ERTL globals) ≝
     192  λglobals.λ_.λs.
     193  match s return λ_.bind_seq_block ?? (joint_step ??) with
     194  [ step_seq s ⇒
     195    match s return λ_.bind_seq_block ?? (joint_step ??) with
     196    [ PUSH _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *)
     197    | POP _ ⇒ NOOP …  (*CSC: XXXX should not be in the syntax *)
     198    | MOVE rs ⇒ PSD (\fst rs) ← \snd rs
     199    | COST_LABEL lbl ⇒
     200      COST_LABEL … lbl
     201    | ADDRESS x prf r1 r2 ⇒
     202      ADDRESS ERTL ? x prf r1 r2
     203    | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
     204      OPACCS ERTL ? op destr1 destr2 srcr1 srcr2 
     205    | OP1 op1 destr srcr ⇒
     206      OP1 ERTL ? op1 destr srcr
     207    | OP2 op2 destr srcr1 srcr2 ⇒
     208      OP2 ERTL ? op2 destr srcr1 srcr2
     209    | CLEAR_CARRY ⇒
     210      CLEAR_CARRY …
     211    | SET_CARRY ⇒
     212      SET_CARRY …
     213    | LOAD destr addr1 addr2 ⇒
     214      LOAD ERTL ? destr addr1 addr2
     215    | STORE addr1 addr2 srcr ⇒
     216      STORE ERTL ? addr1 addr2 srcr
     217    | COMMENT msg ⇒
     218      COMMENT … msg
     219    | extension_seq ext ⇒
     220      match ext with
     221      [ rtl_stack_address addr1 addr2 ⇒
     222        [ PSD addr1 ← HDW RegisterSPL ; PSD addr2 ← HDW RegisterSPH ]
    285223      ]
    286     ) start_lbl dest_lbl def.
    287 
    288 definition translate_stmt :
    289  ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals
    290  ≝
    291   λglobals.
    292   λlbl.
    293   λstmt.
    294   λdef.
    295   match stmt with
    296   [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def
    297   | RETURN ⇒ add_graph … lbl (RETURN …) def
    298   | sequential seq lbl' ⇒
    299      match seq with
    300       [ PUSH _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    301       | POP _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    302       | CALL_ID f args ret_regs ⇒
    303          translate_call_id … f args ret_regs lbl lbl' def
    304       | MOVE rs ⇒
    305          let 〈r1,r2〉 ≝ rs in
    306          let rs ≝ 〈pseudo r1, pseudo r2〉 in
    307           add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def
    308       | extension ext ⇒
    309          match ext with
    310           [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
    311           | rtlntc_st_ext_stack_address r1 r2 ⇒
    312              adds_graph ertl_params1 … [
    313               sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉);
    314               sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉)
    315              ] lbl lbl' def]
    316       (*CSC: everything is just copied to re-type it from now on;
    317         the problem is call_id that takes different parameters, but that is pattern-matched
    318         above. It could be made nicer at the cost of making all the rest of the code uglier *)
    319       | COST_LABEL cost_lbl ⇒ add_graph ertl_params1 … lbl (sequential … (COST_LABEL … cost_lbl) lbl') def
    320       | ADDRESS x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (sequential … (ADDRESS … x prf r1 r2) lbl') def
    321       | INT r i ⇒  add_graph ertl_params1 … lbl (sequential … (INT … r i) lbl') def
    322       | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
    323           add_graph ertl_params1 … lbl (sequential … (OPACCS … op destr1 destr2 srcr1 srcr2) lbl') def
    324       | OP1 op1 destr srcr ⇒
    325         add_graph ertl_params1 … lbl (sequential … (OP1 … op1 destr srcr) lbl') def
    326       | OP2 op2 destr srcr1 srcr2 ⇒
    327         add_graph ertl_params1 … lbl (sequential … (OP2 … op2 destr srcr1 srcr2) lbl') def
    328       | CLEAR_CARRY ⇒
    329         add_graph ertl_params1 … lbl (sequential … (CLEAR_CARRY …) lbl') def
    330       | SET_CARRY ⇒
    331         add_graph ertl_params1 … lbl (sequential … (SET_CARRY …) lbl') def
    332       | LOAD destr addr1 addr2 ⇒
    333         add_graph ertl_params1 … lbl (sequential … (LOAD … destr addr1 addr2) lbl') def
    334       | STORE addr1 addr2 srcr ⇒
    335         add_graph ertl_params1 … lbl (sequential … (STORE … addr1 addr2 srcr) lbl') def
    336       | COND srcr lbl_true ⇒
    337         add_graph ertl_params1 … lbl (sequential … (COND … srcr lbl_true) lbl') def
    338       | COMMENT msg ⇒
    339         add_graph ertl_params1 … lbl (sequential … (COMMENT … msg) lbl') def
    340       ]].
    341   @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
    342 qed.
     224    | CALL_ID f args ret_regs ⇒
     225      set_params ? args @@
     226      CALL_ID ERTL ? f (|args|) it :::
     227      fetch_result ? ret_regs
     228    | extension_call c ⇒
     229      match c with
     230      [ rtl_call_ptr f1 f2 args dest ⇒
     231        ?
     232      ]
     233    ]
     234  | COND r ltrue ⇒
     235    COND ERTL ? r ltrue
     236  ]. cases daemon (* pointer call to be ported yet *) qed.
     237
     238definition translate_fin_step :
     239  ∀globals.label → joint_fin_step RTL_ntc →
     240    bind_seq_block ERTL globals (joint_fin_step ERTL) ≝
     241  λglobals.λ_.λs.
     242  match s with
     243  [ GOTO lbl' ⇒ GOTO … lbl'
     244  | RETURN ⇒ RETURN ?
     245  | tailcall abs ⇒ match abs in void with [ ]
     246  ].
    343247
    344248(* hack with empty graphs used here *)
    345 definition translate_funct_internal ≝
    346   λglobals.λdef:rtlntc_internal_function globals.
     249definition translate_funct :
     250  ∀globals.joint_internal_function RTL_ntc globals →
     251    joint_internal_function ERTL globals ≝
     252  λglobals,def.
    347253  let nb_params ≝ |joint_if_params ?? def| in
    348254  let added_stacksize ≝ max 0 (minus nb_params (|RegisterParams|)) in
    349255  let new_locals ≝ nub_by ? (eq_identifier ?) ((joint_if_locals … def) @ (joint_if_params … def)) in
    350   let entry' ≝ joint_if_entry … def in
    351   let exit' ≝ joint_if_exit … def in
    352   let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in
    353   let graph' ≝ add ? ? graph' exit' (GOTO … exit') in
    354   let def' ≝
    355     mk_joint_internal_function globals (ertl_params globals)
    356       (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*)
     256  let entry' ≝ pi1 … (joint_if_entry … def) in
     257  let exit' ≝ pi1 … (joint_if_exit … def) in
     258  let def' ≝ init_graph_if ERTL globals
     259      (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
    357260      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
    358       graph' ? ? in
    359   let def' ≝ foldi ? ? ? (translate_stmt globals) (joint_if_code … def) def' in
    360    add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
    361 whd in match ertl_params; (* CSC: Matita's bug here; not enough/too much reduction
    362                                  makes the next application fail. Why? *)   
    363 %
    364  [ @entry' | @graph_add_lookup @graph_add
    365  | @exit'  | @graph_add ]
    366 qed.
    367 
     261      entry' exit' in
     262  let def'' ≝ b_graph_translate …
     263    (ertl_fresh_reg …)
     264    def'
     265    (translate_step globals)
     266    (translate_fin_step globals)
     267    def in
     268  add_pro_and_epilogue ? (joint_if_params ?? def) (joint_if_result ?? def) def'.
     269
     270(* removing this because of how insert_prologue is now defined
    368271definition generate ≝
    369272  λglobals.
    370273  λstmt.
    371   λdef: joint_internal_function … (ertl_params globals).
     274  λdef: joint_internal_function globals ERTL.
    372275  let 〈entry, def〉 ≝ fresh_label … def in
    373276  let graph ≝ add … (joint_if_code … def) entry stmt in
    374    set_joint_if_graph … (ertl_params globals) graph def ??.
     277   set_joint_if_graph … (ERTL globals) graph def ??.
    375278  [ (*% [ @entry | @graph_add ]*) cases daemon (*CSC: XXX *)
    376279  | (*cases (joint_if_exit … def) #LBL #LBL_PRF % [ @LBL | @graph_add_lookup @LBL_PRF
     
    392295         match inst with
    393296          [ COST_LABEL cost_lbl ⇒
    394              〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
     297             〈Some … cost_lbl, add_graph ERTL1 globals lbl (GOTO … lbl) def〉
    395298          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
    396299      | RETURN ⇒ 〈None …, def〉
     
    407310  match cost_label with
    408311  [ None ⇒ def
    409   | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
     312  | Some cost_label ⇒ generate … (sequential ERTL_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
    410313  ].
    411314
    412315definition translate_funct ≝ λglobals,def. (move_first_cost_label_up_internal … (translate_funct_internal globals def)).
     316*)
    413317
    414318definition rtl_to_ertl : rtl_program → ertl_program ≝
  • src/RTL/semantics.ma

    r2176 r2286  
    66record frame: Type[0] ≝
    77 { fr_ret_regs: list register
    8  ; fr_pc: address
    9  ; fr_sp: pointer
    10  ; fr_carry: beval
     8 ; fr_pc: cpointer
     9 ; fr_sp: xpointer
     10 ; fr_carry: bebit
    1111 ; fr_regs: register_env beval
    1212 }.
    1313
    14 definition rtl_more_sem_params: more_sem_params rtl_params_ :=
    15  mk_more_sem_params rtl_params_
    16   (list frame) [] (register_env beval) (λ_.empty_map …) [] [](*dummy*)
    17    reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
    18     reg_store reg_retrieve reg_store reg_retrieve
    19      (λlocals,dest_src.
    20        do v ← reg_retrieve locals (\snd dest_src) ;
    21        reg_store (\fst dest_src) v locals).
    22 definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
    23 
    24 definition rtl_init_locals :
    25  list register → register_env beval → register_env beval ≝
    26  λlocals,env.
    27   foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals.
     14definition RTL_state : sem_state_params ≝
     15  mk_sem_state_params
     16    (list frame)
     17    [ ]
     18    (register_env beval)
     19    (λ_.empty_map …).
     20
     21definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : psd_argument.
     22  match a with
     23  [ Reg r ⇒ reg_retrieve env r
     24  | Imm b ⇒ return b
     25  ].
    2826
    2927(*CSC: could we use here a dependent type to avoid the Error case? *)
     
    3230
    3331definition rtl_fetch_ra:
    34  state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝
     32 RTL_state → res (RTL_state × cpointer) ≝
    3533 λst.
    3634  match st_frms ? st with
     
    3836  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
    3937
    40 definition rtl_result_regs:
    41  ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list register) ≝
    42  λglobals,ge,st.
    43   do fn ← graph_fetch_function … globals ge st ;
    44   OK … (joint_if_result … fn).
    45 
    46 (*CSC: we could use a dependent type here: the list of return values should have
    47   the same length of the list of return registers that store the values. This
    48   saves the OutOfBounds exception *)
    49 definition rtl_pop_frame:
    50  ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝
    51  λglobals,ge,st.
    52   do ret_regs ← rtl_result_regs … ge st ;
    53   do ret_vals ← mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_regs ;
    54   match st_frms ? st with
    55   [ nil ⇒ Error ? [MSG EmptyStack]
    56   | cons hd tl ⇒
    57      do st ←
    58       mfold_left_i ??
    59        (λi.λst.λreg.
    60          do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
    61          greg_store rtl_sem_params reg v st)
    62        (OK … st) (fr_ret_regs hd) ;
    63      OK …
    64       (set_frms rtl_sem_params tl
    65         (set_regs rtl_sem_params (fr_regs hd)
    66          (set_sp … (fr_sp hd)
    67           (set_carry … (fr_carry hd)
    68            (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    69 
    70 definition rtl_call_function:
    71  nat → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     38definition rtl_init_local :
     39 register → register_env beval → register_env beval ≝
     40 λlocal,env.add … env local BVundef.
     41
     42definition rtl_setup_call:
     43 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
    7244  λstacksize,formal_arg_regs,actual_arg_regs,st.
    7345  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
     
    7547   mfold_left2 …
    7648    (λlenv,dest,src.
    77       do v ← greg_retrieve … st src ;
     49      do v ← rtl_arg_retrieve … (regs ? st) src ;
    7850      OK … (add … lenv dest v))
    7951    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
    8052  OK …
    81    (set_regs rtl_sem_params new_regs
     53   (set_regs RTL_state new_regs
    8254    (set_m … mem
    83      (set_sp … (mk_pointer b (mk_offset 0)) st))).
    84 (*cases b * #r #off #E >E %
    85 qed.*)
    86 
    87 definition rtl_save_frame:
    88  address → nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
    89  λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st.
    90   let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st) in
    91   let st ≝ set_frms rtl_sem_params frame st in
    92   rtl_call_function stacksize formal_arg_regs actual_arg_regs st.
     55     (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))).
     56cases b * #r #off #E >E %
     57qed.
     58
     59definition rtl_save_frame ≝ λl.λretregs.λst : RTL_state.
     60  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
     61  OK … (set_frms RTL_state frame st).
    9362
    9463(*CSC: XXXX, for external functions only*)
    95 axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
    96 axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
    97 
    98 definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
    99  λglobals.
    100   mk_more_sem_params1 … rtl_more_sem_params graph_succ_p (graph_pointer_of_label …)
    101    (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
    102    rtl_init_locals rtl_save_frame (rtl_pop_frame …)
    103    rtl_fetch_external_args rtl_set_result.
    104 definition rtl_sem_params1: ∀globals. sem_params1 … globals ≝
    105  λglobals. mk_sem_params1 … (rtl_more_sem_params1 globals).
    106 
    107 definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
    108  λr1,r2,st.
    109  do v1 ← greg_retrieve rtl_sem_params st r1 ;
    110  do v2 ← greg_retrieve rtl_sem_params st r2 ;
    111  do ptr ← pointer_of_address 〈v1,v2〉 ;
    112  OK … (pblock ptr). 
     64axiom rtl_fetch_external_args: external_function → RTL_state → res (list val).
     65axiom rtl_set_result: list val → list register → RTL_state → res 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).
     69
     70definition rtl_read_result :
     71 ∀globals.genv RTL globals → list register → RTL_state → res (list beval) ≝
     72 λglobals,ge,rets,st.
     73 m_list_map … (rtl_reg_retrieve st) rets.
     74
     75(*CSC: we could use a dependent type here: the list of return values should have
     76  the same length of the list of return registers that store the values. This
     77  saves the OutOfBounds exception *)
     78definition rtl_pop_frame:
     79 ∀globals. genv RTL globals → joint_internal_function RTL globals → RTL_state →
     80  res RTL_state ≝
     81 λglobals,ge,curr_fn,st.
     82  let ret ≝ joint_if_result … curr_fn in
     83  do ret_vals ← rtl_read_result … ge ret st ;
     84  match st_frms ? st with
     85  [ nil ⇒ Error ? [MSG EmptyStack]
     86  | cons hd tl ⇒
     87     do st ←
     88      mfold_left_i …
     89       (λi.λst.λreg.
     90         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
     91         rtl_reg_store reg v st)
     92       (OK … st) (fr_ret_regs hd) ;
     93     OK …
     94      (set_frms RTL_state tl
     95        (set_regs RTL_state (fr_regs hd)
     96         (set_sp … (fr_sp hd)
     97          (set_carry … (fr_carry hd)
     98           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    11399
    114100(* This code is quite similar to eval_call_block: can we factorize it out? *)
    115 definition eval_tail_call_block:
    116  ∀globals.genv … (rtl_params globals) → state rtl_sem_params →
    117   block → call_args rtl_sem_params → IO io_out io_in (trace×(state rtl_sem_params)) ≝
    118  λglobals,ge,st,b,args.
    119   ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr … ge b);
     101definition eval_tailcall_block:
     102 ∀globals.genv RTL globals → RTL_state →
     103  block → call_args RTL →
     104  (* this is where the result of the current function should be stored *)
     105  call_dest RTL →
     106  IO io_out io_in
     107    ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×RTL_state) ≝
     108 λglobals,ge,st,b,args,ret.
     109  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    120110    match fd with
    121     [ Internal fn ⇒
    122       let st ≝ set_m … (free … (m … st) (pblock (sp … st))) st in
    123       ! st ← rtl_call_function (joint_if_stacksize … fn) (joint_if_params … fn) args st ;
    124       let regs ≝ rtl_init_locals … (joint_if_locals … fn) (regs … st) in
    125       let l' ≝ joint_if_entry … fn in
    126       ! st ← next … (rtl_sem_params1 …) l' (set_regs rtl_sem_params regs st) ;
    127        return 〈 E0, st〉
    128     | External fn ⇒ ?(*
    129       ! params ← fetch_external_args … fn st;
    130       ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     111    [ Internal fd ⇒
     112      return 〈FTailInit ?? (block_id b) fd args, st〉
     113    | External fn ⇒
     114      ! params ← rtl_fetch_external_args … fn st : IO ???;
     115      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    131116      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    132117      (* CSC: XXX bug here; I think I should split it into Byte-long
    133118         components; instead I am making a singleton out of it. To be
    134119         fixed once we fully implement external functions. *)
    135         let vs ≝ [mk_val ? evres] in
    136       ! st ← set_result … vs st;
    137       let st ≝ set_pc … ra st in
    138         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉 *)
    139      ].
    140 cases daemon (*CSC: XXX tailcall to external function not implemented yet;
    141                     it needs alls other functions on external calls *)
    142 qed.
    143 
    144 definition rtl_exec_extended:
    145  ∀globals. genv globals (rtl_params globals) →
    146   rtl_statement_extension → label → state rtl_sem_params →
    147    IO io_out io_in (trace × (state rtl_sem_params)) ≝
    148  λglobals,ge,stm,l,st.
     120      let vs ≝ [mk_val ? evres] in
     121      ! st ← rtl_set_result … vs ret st : IO ???;
     122      return 〈FEnd2 ??, st〉
     123    ].
     124
     125definition block_of_register_pair: register → register → RTL_state → res block ≝
     126 λr1,r2,st.
     127 do v1 ← rtl_reg_retrieve st r1 ;
     128 do v2 ← rtl_reg_retrieve st r2 ;
     129 do ptr ← pointer_of_address 〈v1,v2〉 ;
     130 OK … (pblock ptr). 
     131
     132definition eval_rtl_seq:
     133 ∀globals. genv RTL globals →
     134  rtl_seq → joint_internal_function RTL globals → RTL_state →
     135   IO io_out io_in RTL_state ≝
     136 λglobals,ge,stm,curr_fn,st.
    149137  match stm with
    150    [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
     138   [ rtl_stack_address dreg1 dreg2  ⇒
    151139      let sp ≝ sp ? st in
    152140      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
    153       ! st ← greg_store rtl_sem_params dreg1 dpl st ;
    154       ! st ← greg_store rtl_sem_params dreg2 dph st ;
    155       ! st ← next … (rtl_sem_params1 globals) l st ;
    156        return 〈E0, st〉
    157    | rtl_st_ext_call_ptr r1 r2 args dest ⇒
    158       ! b ← block_of_register_pair r1 r2 st : IO ??? ;
    159       ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) : IO ??? ;
    160       eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
    161        ge st b args dest ra
    162    | rtl_st_ext_tailcall_id id args ⇒
     141      ! st ← rtl_reg_store dreg1 dpl st ;
     142      rtl_reg_store dreg2 dph st
     143   ].
     144
     145definition eval_rtl_call:
     146 ∀globals. genv RTL globals →
     147  rtl_call → RTL_state →
     148   IO io_out io_in ((step_flow RTL ? Call)×RTL_state) ≝
     149 λglobals,ge,stm,st.
     150  match stm with
     151  [ rtl_call_ptr r1 r2 args dest ⇒
     152    ! b ← block_of_register_pair r1 r2 st : IO ???;
     153    ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
     154    match fd with
     155    [ Internal fd ⇒
     156      return 〈Init ?? (block_id b) fd args dest, st〉
     157    | External fn ⇒
     158      ! params ← rtl_fetch_external_args … fn st : IO ???;
     159      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     160      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     161      (* CSC: XXX bug here; I think I should split it into Byte-long
     162         components; instead I am making a singleton out of it. To be
     163         fixed once we fully implement external functions. *)
     164      let vs ≝ [mk_val ? evres] in
     165      ! st ← rtl_set_result … vs dest st : IO ???;
     166      return 〈Proceed ???, st〉
     167    ]
     168  ].
     169
     170definition eval_rtl_tailcall:
     171 ∀globals. genv RTL globals →
     172  rtl_tailcall → joint_internal_function RTL globals → RTL_state →
     173   IO io_out io_in ((fin_step_flow RTL ? Call)×RTL_state) ≝
     174   λglobals,ge,stm,curr_fn,st.
     175   let ret ≝ joint_if_result … curr_fn in
     176   match stm with
     177   [ rtl_tailcall_id id args ⇒
    163178      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    164       eval_tail_call_block … ge st b args
    165    | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
     179      eval_tailcall_block … ge st b args ret
     180   | rtl_tailcall_ptr r1 r2 args ⇒
    166181      ! b ← block_of_register_pair r1 r2 st : IO ???;
    167       eval_tail_call_block … ge st b args
     182      eval_tailcall_block … ge st b args ret
    168183   ].
    169184
    170 definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
    171  λglobals. mk_more_sem_params2 … (rtl_more_sem_params1 globals) (rtl_exec_extended …).
    172 
    173 definition rtl_fullexec ≝
    174  joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
     185definition RTL_semantics ≝
     186  make_sem_graph_params RTL
     187    (mk_more_sem_unserialized_params ??
     188      RTL_state
     189      reg_store reg_retrieve rtl_arg_retrieve
     190      reg_store reg_retrieve rtl_arg_retrieve
     191      reg_store reg_retrieve rtl_arg_retrieve
     192      reg_store reg_retrieve rtl_arg_retrieve
     193      rtl_arg_retrieve
     194      (λenv,p. let 〈dest,src〉 ≝ p in
     195        ! v ← rtl_arg_retrieve env src ;
     196        reg_store dest v env)
     197      rtl_fetch_ra
     198      rtl_init_local
     199      rtl_save_frame
     200      rtl_setup_call
     201      rtl_fetch_external_args
     202      rtl_set_result
     203      [ ] [ ]
     204      rtl_read_result
     205      eval_rtl_seq
     206      eval_rtl_tailcall
     207      eval_rtl_call
     208      rtl_pop_frame
     209      (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)).
Note: See TracChangeset for help on using the changeset viewer.