Changeset 2208 for src/RTL


Ignore:
Timestamp:
Jul 18, 2012, 1:26:43 PM (8 years ago)
Author:
tranquil
Message:
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
Location:
src/RTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLToERTL_paolo.ma

    r2174 r2208  
    1515
    1616definition restore_hdws :
    17   ∀globals.list (rtl_argument×Register) → list (joint_seq ertl_params globals) ≝
     17  ∀globals.list (psd_argument×Register) → list (joint_seq ertl_params globals) ≝
    1818  λglobals.
    1919   let restore_hdws_internal ≝
    20     λdestr_srcr:rtl_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in
     20    λdestr_srcr:psd_argument×?.HDW (\snd destr_srcr) ← \fst destr_srcr in
    2121    map ? ? restore_hdws_internal.
    2222
     
    2626  save_hdws … (zip_pottier … params RegisterParams).
    2727
    28 (* Paolo: The following can probably be done way more efficiently with INC DPTR *)
    29 
    3028definition get_param_stack :
    31   ∀globals.register → register → nat → register →
     29  ∀globals.register → register → register →
    3230  list (joint_seq ertl_params globals) ≝
    33   λglobals,addr1,addr2,off,destr.
    34   let int_offset : Byte ≝ \snd (half_add ? (bitvector_of_nat ? off) int_size) in
    35   [ (ertl_frame_size addr1 : joint_seq ??) ;
    36     CLEAR_CARRY … ;
    37     addr1 ← addr1 .Sub. int_offset ; (* are we sure carry bit is unimportant? *)
    38     PSD destr ← HDW RegisterSPL ;
    39     addr1 ← addr1 .Add. destr ;
    40     PSD addr2 ← HDW RegisterSPH ;
    41     addr2 ← addr2 .Addc. 0 ;
    42     LOAD … destr addr1 addr2
     31  λglobals,addr1,addr2,destr.
     32  (* liveness analysis will erase the last useless ops *)
     33  [ LOAD ?? destr addr1 addr2 ;
     34    addr1 ← addr1 .Add. (int_size : Byte) ;
     35    addr2 ← addr2 .Addc. zero_byte
    4336  ].
    4437
     
    4740  bind_new (localsT ertl_params) (list (joint_seq ertl_params globals)) ≝
    4841  λglobals,params.
    49   νaddr1,addr2 in
    50   flatten … (mapi ?? (get_param_stack globals addr1 addr2) params).
     42  νtmpr,addr1,addr2 in
     43  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
     44  [ (ertl_frame_size tmpr : joint_seq ??) ;
     45    CLEAR_CARRY ?? ;
     46    tmpr ← tmpr .Sub. params_length_byte ; (* will be constant later *)
     47    PSD addr1 ← HDW RegisterSPL ;
     48    PSD addr2 ← HDW RegisterSPH ;
     49    addr1 ← addr1 .Add. tmpr ;
     50    addr2 ← addr2 .Addc. zero_byte ] @   
     51  flatten … (map ?? (get_param_stack globals addr1 addr2) params).
    5152
    5253definition get_params ≝
     
    6667
    6768definition save_return :
    68   ∀globals.list rtl_argument → list (joint_seq ertl_params globals) ≝
     69  ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
    6970  λglobals,ret_regs.
    7071  match reduce_strong ? ? RegisterSTS ret_regs with
     
    7475    let restl ≝ \snd (\fst crl) in
    7576    (* let restr ≝ \snd (\snd crl) in *)
    76     map2 … (λst.λr : rtl_argument.HDW st ← r) commonl commonr crl_proof @
    77     map … (λst.HDW st ← 0) restl
     77    map2 … (λst.λr : psd_argument.HDW st ← r) commonl commonr crl_proof @
     78    map … (λst.HDW st ← zero_byte) restl
    7879  ].
    7980
     
    9192  list (joint_seq ertl_params globals) ≝
    9293  λglobals,ret_regs,sral,srah,sregs.
    93   save_return … (map … Reg ret_regs) @
    94   restore_hdws … (map … (λpr.〈Reg (\fst pr),\snd pr〉) sregs) @
     94  save_return … (map … (Reg ?) ret_regs) @
     95  restore_hdws … (map … (λpr.〈Reg ? (\fst pr),\snd pr〉) sregs) @
    9596  [ PUSH ertl_params ? srah ;
    9697    PUSH … sral ;
     
    128129
    129130definition set_params_hdw :
    130   ∀globals.list rtl_argument → list (joint_seq ertl_params globals) ≝
     131  ∀globals.list psd_argument → list (joint_seq ertl_params globals) ≝
    131132  λglobals,params.
    132133  restore_hdws globals (zip_pottier ? ? params RegisterParams).
     
    135136
    136137definition set_param_stack :
    137   ∀globals.register → register → nat → rtl_argument →
     138  ∀globals.register → register → psd_argument →
    138139  list (joint_seq ertl_params globals) ≝
    139   λglobals,addr1,addr2,off,arg.
    140   let int_off : Byte ≝ \snd (half_add ? (bitvector_of_nat ? off) int_size) in
     140  λglobals,addr1,addr2,arg.
     141  [ STORE … addr1 addr2 arg ;
     142    addr1 ← addr1 .Add. (int_size : Byte) ;
     143    addr2 ← addr2 .Addc. zero_byte
     144  ].
     145
     146definition set_params_stack :
     147  ∀globals.list psd_argument → bind_new (localsT ertl_params) ? ≝
     148  λglobals,params.
     149  νaddr1,addr2 in
     150  let params_length_byte : Byte ≝ bitvector_of_nat ? (|params|) in
    141151  [ PSD addr1 ← HDW RegisterSPL ;
    142     CLEAR_CARRY … ;
    143     addr1 ← addr1 .Sub. int_off ;
    144152    PSD addr2 ← HDW RegisterSPH ;
    145     addr2 ← addr2 .Sub. 0 ;
    146     STORE … addr1 addr2 arg
    147   ].
    148 
    149 definition set_params_stack :
    150   ∀globals.list rtl_argument → bind_new (localsT ertl_params) ? ≝
    151   λglobals,params.
    152   νaddr1,addr2 in
    153   flatten … (mapi … (set_param_stack globals addr1 addr2) params).
     153    CLEAR_CARRY ?? ;
     154    addr1 ← addr1 .Sub. params_length_byte ;
     155    addr2 ← addr2 .Sub. zero_byte
     156  ] @
     157  flatten … (map … (set_param_stack globals addr1 addr2) params).
    154158
    155159definition set_params ≝
     
    186190    [ PUSH _ ⇒ NOOP … (*CSC: XXXX should not be in the syntax *)
    187191    | POP _ ⇒ NOOP …  (*CSC: XXXX should not be in the syntax *)
    188     | MOVE rs ⇒ PSD (\fst rs) ←
    189         match \snd rs with
    190         [ Reg src ⇒ PSD src
    191         | Imm b ⇒ INT b
    192         ]
     192    | MOVE rs ⇒ PSD (\fst rs) ← \snd rs
    193193    | COST_LABEL lbl ⇒
    194194      COST_LABEL … lbl
     
    254254  let def' ≝
    255255    mk_joint_internal_function globals ertl_params
    256       (joint_if_luniverse … def) (joint_if_runiverse … def) (joint_if_result … def) (*CSC: different from OCaml code where joint_if_result is unit*)
     256      (joint_if_luniverse … def) (joint_if_runiverse … def) it (*Paolo: to be checked, unit or list register? *)
    257257      nb_params new_locals ((joint_if_stacksize … def) + added_stacksize)
    258258      graph' entry' exit' in
  • src/RTL/RTL_paolo.ma

    r2186 r2208  
    11include "joint/Joint_paolo.ma".
    2 
    3 inductive rtl_argument : Type[0] ≝
    4   | Reg : register → rtl_argument
    5   | Imm : Byte → rtl_argument.
    6  
    7 coercion reg_to_rtl_argument : ∀r : register.rtl_argument ≝ Reg
    8   on _r : register to rtl_argument.
    9 
    10 coercion byte_to_rtl_argument : ∀b : Byte.rtl_argument ≝ Imm
    11   on _b : Byte to rtl_argument.
    12 
    13 definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n).
    14  
    15 coercion nat_to_rtl_argument : ∀n : nat.rtl_argument ≝ imm_nat
    16   on _n : nat to rtl_argument.
    172
    183inductive rtl_seq : Type[0] ≝
     
    205 
    216inductive rtl_call : Type[0] ≝
    22   | rtl_call_ptr: register → register → list rtl_argument → list register → rtl_call.
     7  | rtl_call_ptr: register → register → list psd_argument → list register → rtl_call.
    238
    249inductive rtl_tailcall : Type[0] ≝
    25   | rtl_tailcall_id: ident → list rtl_argument → rtl_tailcall
    26   | rtl_tailcall_ptr: register → register → list rtl_argument → rtl_tailcall.
     10  | rtl_tailcall_id: ident → list psd_argument → rtl_tailcall
     11  | rtl_tailcall_ptr: register → register → list psd_argument → rtl_tailcall.
    2712
    2813definition rtl_uns_params ≝ mk_unserialized_params
     
    3015    (* acc_a_reg ≝ *) register
    3116    (* acc_b_reg ≝ *) register
    32     (* acc_a_arg ≝ *) rtl_argument
    33     (* acc_b_arg ≝ *) rtl_argument
     17    (* acc_a_arg ≝ *) psd_argument
     18    (* acc_b_arg ≝ *) psd_argument
    3419    (* dpl_reg   ≝ *) register
    3520    (* dph_reg   ≝ *) register
    36     (* dpl_arg   ≝ *) rtl_argument
    37     (* dph_arg   ≝ *) rtl_argument
    38     (* snd_arg   ≝ *) rtl_argument
    39     (* pair_move ≝ *) (register × rtl_argument)
    40     (* call_args ≝ *) (list rtl_argument)
     21    (* dpl_arg   ≝ *) psd_argument
     22    (* dph_arg   ≝ *) psd_argument
     23    (* snd_arg   ≝ *) psd_argument
     24    (* pair_move ≝ *) (register × psd_argument)
     25    (* call_args ≝ *) (list psd_argument)
    4126    (* call_dest ≝ *) (list register)
    4227    (* ext_seq ≝ *) rtl_seq
     
    5944definition rtl_statement ≝ joint_statement rtl_params.
    6045
    61 interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? rtl_argument r a)).
     46interpretation "move" 'mov r a = (MOVE rtl_params ? (mk_Prod ? psd_argument r a)).
    6247
    6348(* aid unification *)
     
    7156unification hint 0 ≔
    7257(*---------------*) ⊢
    73 acc_a_arg rtl_params ≡ rtl_argument.
     58acc_a_arg rtl_params ≡ psd_argument.
    7459unification hint 0 ≔
    7560(*---------------*) ⊢
    76 acc_b_arg rtl_params ≡ rtl_argument.
     61acc_b_arg rtl_params ≡ psd_argument.
    7762unification hint 0 ≔
    7863(*---------------*) ⊢
     
    8368unification hint 0 ≔
    8469(*---------------*) ⊢
    85 dpl_arg rtl_params ≡ rtl_argument.
     70dpl_arg rtl_params ≡ psd_argument.
    8671unification hint 0 ≔
    8772(*---------------*) ⊢
    88 dph_arg rtl_params ≡ rtl_argument.
     73dph_arg rtl_params ≡ psd_argument.
    8974unification hint 0 ≔
    9075(*---------------*) ⊢
    91 snd_arg rtl_params ≡ rtl_argument.
     76snd_arg rtl_params ≡ psd_argument.
    9277unification hint 0 ≔
    9378(*---------------*) ⊢
    94 pair_move rtl_params ≡ register × rtl_argument.
     79pair_move rtl_params ≡ register × psd_argument.
    9580unification hint 0 ≔
    9681(*---------------*) ⊢
    97 call_args rtl_params ≡ list rtl_argument.
     82call_args rtl_params ≡ list psd_argument.
    9883unification hint 0 ≔
    9984(*---------------*) ⊢
     
    120105joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
    121106
    122 coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ Reg
     107coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ psd_argument_from_reg
    123108  on _r : register to snd_arg rtl_params.
    124 coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ Imm
     109coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ psd_argument_from_byte
    125110  on _b : Byte to snd_arg rtl_params.
    126111
     
    132117    (* acc_a_reg ≝ *) register
    133118    (* acc_b_reg ≝ *) register
    134     (* acc_a_arg ≝ *) rtl_argument
    135     (* acc_b_arg ≝ *) rtl_argument
     119    (* acc_a_arg ≝ *) psd_argument
     120    (* acc_b_arg ≝ *) psd_argument
    136121    (* dpl_reg   ≝ *) register
    137122    (* dph_reg   ≝ *) register
    138     (* dpl_arg   ≝ *) rtl_argument
    139     (* dph_arg   ≝ *) rtl_argument
    140     (* snd_arg   ≝ *) rtl_argument
    141     (* pair_move ≝ *) (register × rtl_argument)
    142     (* call_args ≝ *) (list rtl_argument)
     123    (* dpl_arg   ≝ *) psd_argument
     124    (* dph_arg   ≝ *) psd_argument
     125    (* snd_arg   ≝ *) psd_argument
     126    (* pair_move ≝ *) (register × psd_argument)
     127    (* call_args ≝ *) (list psd_argument)
    143128    (* call_dest ≝ *) (list register)
    144129    (* ext_seq ≝ *) rtl_seq
Note: See TracChangeset for help on using the changeset viewer.