Changeset 2208 for src/RTLabs


Ignore:
Timestamp:
Jul 18, 2012, 1:26:43 PM (7 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
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL_paolo.ma

    r2162 r2208  
    88include alias "ASM/BitVector.ma".
    99include alias "arithmetics/nat.ma".
    10 
    1110definition size_of_sig_type ≝
    1211  λsig.
     
    1615      isize' ÷ (nat_of_bitvector ? int_size)
    1716  | ASTfloat _ ⇒ ? (* dpm: not implemented *)
    18   | ASTptr rgn ⇒ nat_of_bitvector ? ptr_size
    19   ].
    20   cases not_implemented;
     17  | ASTptr ⇒ 2 (* rgn ⇒ nat_of_bitvector ? ptr_size *)
     18  ].
     19  cases not_implemented
    2120qed.
    2221
     
    4645qed.
    4746
    48 definition find_local_env_arg
    49   λr,lenv,prf. map … Reg (find_local_env r lenv prf).
     47definition find_local_env_arg : register → local_env → ? → list psd_argument
     48  λr,lenv,prf. map … (Reg ?) (find_local_env r lenv prf).
    5049
    5150definition m_fresh : ∀tag.state_monad (universe tag) (identifier tag) ≝
     
    9796include alias "common/Identifiers.ma".
    9897let rec rtl_args (args : list register) (env : local_env) on args :
    99   All ? (λr.bool_to_Prop (r∈env)) args → list rtl_argument ≝
     98  All ? (λr.bool_to_Prop (r∈env)) args → list psd_argument ≝
    10099  match args return λx.All ?? x → ? with
    101100  [ nil ⇒ λ_.[ ]
     
    131130  ∀globals. Op2 →
    132131  ∀dests : list register.
    133   ∀srcrs1 : list rtl_argument.
    134   ∀srcrs2 : list rtl_argument.
     132  ∀srcrs1 : list psd_argument.
     133  ∀srcrs2 : list psd_argument.
    135134  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
    136135  list (joint_seq rtl_params globals)
     
    149148  ] @ map3 ???? (OP2 rtl_params globals op) destrs srcrs1 srcrs2 prf1 prf2.
    150149
    151 let rec nat_to_args (size : nat) (k : nat) on size : Σl : list rtl_argument.|l| = size ≝
     150let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.|l| = size ≝
    152151match size with
    153152[ O ⇒ [ ]
    154153| S size' ⇒
    155   match nat_to_args size' (k ÷ 8) with
    156   [ mk_Sig res prf ⇒
    157     imm_nat k :: res
    158   ]
    159 ]. normalize // qed.
     154  (byte_of_nat k : psd_argument) :: nat_to_args size' (k ÷ 8)
     155]. [ % | cases (nat_to_args ??) #res #EQ  normalize >EQ % ] qed.
    160156
    161157definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with
     
    168164definition cst_well_defd : ∀ty.list ident → constant ty → Prop ≝ λty,globals,cst.
    169165  match cst with
    170   [ Oaddrsymbol r id offset ⇒ member id (eq_identifier ?) globals
     166  [ Oaddrsymbol id _ ⇒ member id (eq_identifier ?) globals
    171167  | _ ⇒ True
    172168  ].
     
    185181  with
    186182  [ Ointconst size sign const ⇒ λcst_prf,prf.
    187       map2 … (λr.λb : Byte.r ← (b : rtl_argument)) destrs
     183      map2 … (λr.λb : Byte.r ← b) destrs
    188184        (split_into_bytes size const) ?
    189185  | Ofloatconst _ _ ⇒ ?
    190   | Oaddrsymbol r id offset ⇒ λcst_prf,prf.
     186  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
    191187    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    192188    [ADDRESS rtl_params globals id ? r1 r2]
     
    206202  ∀globals.
    207203  ∀destrs: list register.
    208   ∀srcrs: list rtl_argument.
     204  ∀srcrs: list psd_argument.
    209205  |destrs| = |srcrs| → list (joint_seq rtl_params globals) ≝
    210206  λglobals,destrs,srcrs,length_eq.
     
    229225     *)
    230226  λglobals,destr,srcr.
    231   [destr ← srcr .Or. 127 ;
     227  let byte_127 : Byte ≝ false ::: maximum ? in
     228  [destr ← srcr .Or. byte_127 ;
    232229   destr ← .Rl. destr ;
    233230   destr ← .Inc. destr ;
     
    241238  ν tmp in
    242239  (sign_mask ? tmp srcr @
    243   translate_move ? destrs (make_list ? (Reg tmp) (|destrs|)) (make_list_length …)).
     240  translate_move ? destrs (make_list ? (Reg ? tmp) (|destrs|)) (make_list_length …)).
    244241 
    245242definition translate_fill_with_zero :
     
    282279    let dst_rest   ≝ \snd (\snd t) in
    283280    (* first, move the common part *)
    284     translate_move ? src_common (map … Reg dst_common) ? @@
     281    translate_move ? src_common (map … (Reg ?) dst_common) ? @@
    285282    match src_rest return λ_.bind_new ?? with
    286283    [ nil ⇒ (* upcast *)
     
    314311  match nat_to_args (|destrs|) 1 with
    315312  [ mk_Sig res prf' ⇒
    316     translate_op ? Add destrs (map … Reg destrs) res ??
    317   ].
    318 // qed.
     313    translate_op ? Add destrs (map … (Reg ?) destrs) res ??
     314  ].
     315>length_map // qed.
    319316
    320317definition translate_notbool:
     
    328325    translate_fill_with_zero ? destrs' @@
    329326    match srcrs return λ_.bind_new ?? with
    330     [ nil ⇒ [destr ← 0]
     327    [ nil ⇒ [destr ← zero_byte]
    331328    | cons srcr srcrs' ⇒
    332329      (destr ← srcr) :::
     
    336333      (* many uses of 0, better not use immediates *)
    337334      ν tmp in
    338       [tmp ← 0 ;
     335      [tmp ← zero_byte ;
    339336       destr ← tmp .Sub. tmp ;
    340337       (* now carry bit is set iff destr was non-null *)
     
    363360  | Onotint sz sg ⇒ λeq1,eq2.
    364361    translate_notint globals destrs srcrs ?
    365   | Optrofint sz sg r ⇒ λeq1,eq2.
     362  | Optrofint sz sg ⇒ λeq1,eq2.
    366363    translate_cast globals Unsigned destrs srcrs
    367   | Ointofptr sz sg r ⇒ λeq1,eq2.
     364  | Ointofptr sz sg ⇒ λeq1,eq2.
    368365    translate_cast globals Unsigned destrs srcrs
    369366  | Oid t ⇒ λeq1,eq2.
    370       translate_move globals destrs (map … Reg srcrs) ?
     367      translate_move globals destrs (map … (Reg ?) srcrs) ?
    371368  | _ ⇒ λeq1,eq2.? (* float operations implemented in runtime *)
    372369  ] (refl …) (refl …).
    373   [3,4,5,6,7,8,9: cases not_implemented
    374   |*: destruct >prf1 >prf2 //
     370  [3,4,5,6,7,8,9: (* floats *) cases not_implemented
     371  |*: destruct >prf1 >prf2 [3: >length_map ] //
    375372  ]
    376373qed.
     
    401398  (* the temporary destination, with a dummy register at the end *)
    402399  ∀tmp_destrs_dummy : list register.
    403   ∀srcrs1,srcrs2 : list rtl_argument.
     400  ∀srcrs1,srcrs2 : list psd_argument.
    404401  |tmp_destrs_dummy| = S n →
    405402  n = |srcrs1| →
     
    431428         for the bit to be carried. Redundant calculations will be eliminated
    432429         by constant propagation. *)
    433       let args : list rtl_argument ≝
    434         [Reg a;Reg b] @ make_list ? (Imm (zero …)) (n - 1 - k) in
     430      let args : list psd_argument ≝
     431        [Reg ? a;Reg ? b] @ make_list ? (zero_byte : psd_argument) (n - 1 - k) in
    435432      let tmp_destrs_view : list register ≝
    436433        ltl ? tmp_destrs_dummy k in
    437434      ❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?) ::
    438       translate_op … Add tmp_destrs_view (map … Reg tmp_destrs_view) args ?? @
     435      translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @
    439436      acc
    440437    ].
     
    452449    [2: @le_plus_to_minus_r <plus_n_Sm <plus_n_O assumption]
    453450  cut (S n = 2 + (n - 1))
    454     [2: #EQ >EQ //]
     451    [2: #EQ >EQ %]
    455452  >plus_minus_commutative
    456453    [2: @(transitive_le … k_prf) //]
    457454  @sym_eq
    458   @plus_to_minus
    459   <plus_n_Sm
    460   //
     455  @plus_to_minus %
    461456] qed.
    462457
     
    464459λglobals : list ident.
    465460λdestrs : list register.
    466 λsrcrs1 : list rtl_argument.
    467 λsrcrs2 : list rtl_argument.
     461λsrcrs1 : list psd_argument.
     462λsrcrs2 : list psd_argument.
    468463λsrcrs1_prf : |destrs| = |srcrs1|.
    469464λsrcrs2_prf : |srcrs1| = |srcrs2|.
     
    494489foldr … translate_mul_k [ ] (range_strong (|destrs|)) @
    495490(* epilogue: saving the result *)
    496 translate_move … destrs (map … Reg tmp_destrs) ?.
     491translate_move … destrs (map … (Reg ?) tmp_destrs) ?.
    497492[ >length_map >tmp_destrs_prf //
    498493| >length_append <plus_n_Sm <plus_n_O //
     
    505500  λdiv_not_mod: bool.
    506501  λdestrs: list register.
    507   λsrcrs1: list rtl_argument.
    508   λsrcrs2: list rtl_argument.
     502  λsrcrs1: list psd_argument.
     503  λsrcrs2: list psd_argument.
    509504  λsrcrs1_prf : |destrs| = |srcrs1|.
    510505  λsrcrs2_prf : |srcrs1| = |srcrs2|.
     
    551546  λglobals: list ident.
    552547  λdestrs: list register.
    553   λsrcrs1: list rtl_argument.
    554   λsrcrs2: list rtl_argument.
     548  λsrcrs1: list psd_argument.
     549  λsrcrs2: list psd_argument.
    555550  match destrs return λ_.|srcrs1| = |srcrs2| → bind_new ?? with
    556551  [ nil ⇒ λ_.[ ]
     
    558553    translate_fill_with_zero … destrs' @@
    559554    match srcrs1 return λx.|x| = |srcrs2| → bind_new ?? with
    560     [ nil ⇒ λ_.[destr ← 0]
     555    [ nil ⇒ λ_.[destr ← zero_byte]
    561556    | cons srcr1 srcrs1' ⇒
    562557      match srcrs2 return λx.S (|srcrs1'|) = |x| → bind_new ?? with
     
    564559      | cons srcr2 srcrs2' ⇒ λEQ.
    565560        νtmpr in
    566         let f : rtl_argument → rtl_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_params globals) ≝
     561        let f : psd_argument → psd_argument → list (joint_seq rtl_params globals) → list (joint_seq rtl_params globals) ≝
    567562          λs1,s2,acc.
    568563          tmpr  ← s1 .Xor. s2 ::
     
    571566        let epilogue : list (joint_seq rtl_params globals) ≝
    572567          [ CLEAR_CARRY ?? ;
    573             tmpr ← 0 .Sub. destr ;
     568            tmpr ← zero_byte .Sub. destr ;
    574569            (* now carry bit is 1 iff destrs != 0 *)
    575             destr ← 0 .Addc. 0 ] in
     570            destr ← zero_byte .Addc. zero_byte ] in
    576571         destr ← srcr1 .Xor. srcr2 ::
    577572         foldr2 ??? f epilogue srcrs1' srcrs2' ?
     
    593588  ∀globals.
    594589  ∀destrs: list register.
    595   ∀srcrs1: list rtl_argument.
    596   ∀srcrs2: list rtl_argument.
     590  ∀srcrs1: list psd_argument.
     591  ∀srcrs2: list psd_argument.
    597592  |srcrs1| = |srcrs2| →
    598593  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     
    605600    (* I perform a subtraction, but the only interest is in the carry bit *)
    606601    translate_op ? Sub (make_list … tmpr (|srcrs1|)) srcrs1 srcrs2 ? srcrs_prf @
    607     [ destr ← 0 .Addc. 0 ])
     602    [ destr ← zero_byte .Addc. zero_byte ])
    608603  ].
    609604<make_list_length % qed.
     
    613608let rec shift_signed globals
    614609  (tmp : register)
    615   (srcrs : list rtl_argument) on srcrs :
    616   Σt : (list rtl_argument) × (list (joint_seq rtl_params globals)).|\fst t| = |srcrs| ≝
     610  (srcrs : list psd_argument) on srcrs :
     611  Σt : (list psd_argument) × (list (joint_seq rtl_params globals)).|\fst t| = |srcrs| ≝
     612  let byte_128 : Byte ≝ true ::: bv_zero ? in
    617613  match srcrs with
    618614  [ nil ⇒ 〈[ ],[ ]〉
    619615  | cons srcr srcrs' ⇒
    620616    match srcrs' with
    621     [ nil ⇒ 〈[ Reg tmp ], [ tmp ← srcr .Add. 128 ]〉
     617    [ nil ⇒ 〈[ Reg ? tmp ], [ tmp ← srcr .Add. byte_128 ]〉
    622618    | _ ⇒
    623619      let re ≝ shift_signed globals tmp srcrs' in
     
    632628  ∀globals.
    633629  ∀destrs: list register.
    634   ∀srcrs1: list rtl_argument.
    635   ∀srcrs2: list rtl_argument.
     630  ∀srcrs1: list psd_argument.
     631  ∀srcrs2: list psd_argument.
    636632  |srcrs1| = |srcrs2| →
    637633  bind_new (localsT rtl_params) (list (joint_seq rtl_params globals)) ≝
     
    684680  ∀globals.∀ty1,ty2,ty3.∀op : binary_operation ty1 ty2 ty3.
    685681  ∀destrs : list register.
    686   ∀srcrs1,srcrs2 : list rtl_argument.
     682  ∀srcrs1,srcrs2 : list psd_argument.
    687683  |destrs| = size_of_sig_type ty3 →
    688684  |srcrs1| = size_of_sig_type ty1 →
     
    695691  [ Oadd sz sg ⇒ λprf1,prf2,prf3.
    696692    translate_op globals Add destrs srcrs1 srcrs2 ??
    697   | Oaddp sz r ⇒ λprf1,prf2,prf3.
     693  | Oaddp sz ⇒ λprf1,prf2,prf3.
    698694    let is_Oaddp ≝ 0 in
    699695    translate_op globals Add destrs srcrs1 srcrs2 ??
    700696  | Osub sz sg ⇒ λprf1,prf2,prf2.
    701697    translate_op globals Sub destrs srcrs1 srcrs2 ??
    702   | Osubpi sz r ⇒ λprf1,prf2,prf3.
     698  | Osubpi sz ⇒ λprf1,prf2,prf3.
    703699    let is_Osubpi ≝ 0 in
    704700    translate_op globals Sub destrs srcrs1 srcrs2 ??
    705   | Osubpp sz r1 r2 ⇒ λprf1,prf2,prf3.
     701  | Osubpp sz ⇒ λprf1,prf2,prf3.
    706702    let is_Osubpp ≝ 0 in
    707703    translate_op globals Sub destrs srcrs1 srcrs2 ??
     
    722718  | Ocmpu sz sg c ⇒ λprf1,prf2,prf3.
    723719    translate_cmp true globals c destrs srcrs1 srcrs2 ?
    724   | Ocmpp r sg c ⇒ λprf1,prf2,prf3.
     720  | Ocmpp sg c ⇒ λprf1,prf2,prf3.
    725721    let is_Ocmpp ≝ 0 in
    726722    translate_cmp true globals c destrs srcrs1 srcrs2 ?
    727723  | _ ⇒ ⊥ (* assert false, implemented in run time or float op *)
    728   ]. // try @not_implemented
     724  ]. try @not_implemented //
    729725  (* pointer arithmetics is broken at the moment *)
    730726  cases daemon
     
    749745definition translate_load : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝
    750746  λglobals: list ident.
    751   λaddr : list rtl_argument.
     747  λaddr : list psd_argument.
    752748  λaddr_prf: 2 = |addr|.
    753749  λdestrs: list register.
     
    755751  ν tmp_addr_h in
    756752  let f ≝ λdestr : register.λacc : list (joint_seq rtl_params globals).
    757     LOAD rtl_params globals destr (Reg tmp_addr_l) (Reg tmp_addr_h) ::
    758     translate_op Add
     753    LOAD rtl_params globals destr (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) ::
     754    translate_op ? Add
    759755      [tmp_addr_l ; tmp_addr_h]
    760       [Reg tmp_addr_l ; Reg tmp_addr_h]
    761       [imm_nat 0 ; Imm int_size] ? ? @ acc in
     756      [tmp_addr_l ; tmp_addr_h]
     757      [zero_byte ; (int_size : Byte)] ? ? @ acc in
    762758  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
    763759  foldr … f [ ] destrs.
    764 [1: <addr_prf] // qed.
     760[1: <addr_prf
     761] // qed.
    765762 
    766763definition translate_store : ∀globals.?→?→?→bind_new (localsT rtl_params) ? ≝
    767764  λglobals: list ident.
    768   λaddr : list rtl_argument.
     765  λaddr : list psd_argument.
    769766  λaddr_prf: 2 = |addr|.
    770   λsrcrs: list rtl_argument.
     767  λsrcrs: list psd_argument.
    771768  ν tmp_addr_l in
    772769  ν tmp_addr_h in
    773   let f ≝ λsrcr : rtl_argument.λacc : list (joint_seq rtl_params globals).
    774     STORE rtl_params globals (Reg tmp_addr_l) (Reg tmp_addr_h) srcr ::
     770  let f ≝ λsrcr : psd_argument.λacc : list (joint_seq rtl_params globals).
     771    STORE rtl_params globals (Reg ? tmp_addr_l) (Reg ? tmp_addr_h) srcr ::
    775772    translate_op … Add
    776773      [tmp_addr_l ; tmp_addr_h]
    777       [Reg tmp_addr_l ; Reg tmp_addr_h]
    778       [imm_nat 0 ; Imm int_size] ? ? @ acc in
     774      [tmp_addr_l ; tmp_addr_h]
     775      [zero_byte ; (int_size : Byte)] ? ? @ acc in
    779776  translate_move … [tmp_addr_l ; tmp_addr_h] addr ? @@
    780777  foldr … f [ ] srcrs.
Note: See TracChangeset for help on using the changeset viewer.