Changeset 2917


Ignore:
Timestamp:
Mar 20, 2013, 1:20:48 PM (4 years ago)
Author:
tranquil
Message:

made it so that a 0 offset does not generate adding ops when accessing global and stack addresses.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2916 r2917  
     1    if eqb offset 0 then [ ] else
    12include "RTLabs/RTLabs_syntax.ma".
    23include "RTL/RTL.ma".
     
    205206  ∀srcrs2 : list psd_argument.
    206207  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
    207   bind_new register (list (joint_seq RTL globals))
     208  list (joint_seq RTL globals)
    208209  ≝
    209210  λglobals: list ident.
     
    270271definition translate_op_asym_unsigned :
    271272  ∀globals.Op2 → list register → list psd_argument → list psd_argument →
    272   bind_new register (list (joint_seq RTL globals)) ≝
     273  list (joint_seq RTL globals) ≝
    273274  λglobals,op,destrs,srcrs1,srcrs2.
    274275  let l ≝ |destrs| in
     
    302303  | _ ⇒ True
    303304  ].
    304  
     305
    305306definition translate_cst :
    306307  ∀ty.
     
    320321  | Oaddrsymbol id offset ⇒ λcst_prf,prf.
    321322    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    322     [ADDRESS RTL globals id ? r1 r2 ;
    323      r1 ← r1 .Add. byte_of_nat … offset ;
    324      r2 ← r2 .Addc. zero_byte ]
     323    ADDRESS RTL globals id ? r1 r2 ::
     324    if eqb offset 0 then [ ] else
     325    translate_op … Add
     326      [r1 ; r2 ] [ r1 ; r2 ] [ byte_of_nat … offset ; zero_byte ]
     327      (refl …) (refl …)
    325328  | Oaddrstack offset ⇒ λcst_prf,prf.
    326329    let 〈r1, r2〉 ≝ make_addr … destrs ? in
    327     [(rtl_stack_address r1 r2 : joint_seq RTL globals);
    328      r1 ← r1 .Add. byte_of_nat … offset ;
    329      r2 ← r2 .Addc. zero_byte ]
     330    (rtl_stack_address r1 r2 : joint_seq RTL globals) ::
     331    if eqb offset 0 then [ ] else
     332    translate_op … Add
     333      [r1 ; r2 ] [ r1 ; r2 ] [ byte_of_nat … offset ; zero_byte ]
     334      (refl …) (refl …)
    330335  ] (pi2 … cst_sig).
    331336  @hide_prf
     
    479484  map2 ??? (OP1 RTL globals Cmpl) destrs srcrs prf.
    480485
    481 definition translate_negint : ∀globals.? → ? → ? → bind_new register (list (joint_seq RTL globals)) ≝
     486definition translate_negint : ∀globals.? → ? → ? → list (joint_seq RTL globals) ≝
    482487  λglobals: list ident.
    483488  λdestrs: list register.
    484489  λsrcrs: list register.
    485490  λprf: |destrs| = |srcrs|. (* assert in caml code *)
    486   translate_notint … destrs srcrs prf @@
     491  translate_notint … destrs srcrs prf @
    487492  translate_op ? Add destrs (map … (Reg ?) destrs) (one_args (|destrs|)) ??.
    488493@hide_prf
     
    567572  (Σi.i<S k) →
    568573  (* the accumulator *)
    569   bind_new register (list (joint_seq RTL globals)) →
    570     bind_new register (list (joint_seq RTL globals)) ≝
     574  list (joint_seq RTL globals) →
     575    list (joint_seq RTL globals) ≝
    571576  λglobals,a,b,n,tmp_destrs_dummy,srcrs1,srcrs2,
    572577    tmp_destrs_dummy_prf,srcrs1_prf,srcrs2_prf,k,k_prf,i_sig,acc.
     
    589594      let tmp_destrs_view : list register ≝
    590595        ltl ? tmp_destrs_dummy k in
    591       [❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?)] @@
    592       translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @@
     596      [❮a, b❯ ← (nth_safe ? i srcrs1 ?) .Mul. (nth_safe ? (k - i) srcrs2 ?)] @
     597      translate_op … Add tmp_destrs_view (map … (Reg ?) tmp_destrs_view) args ?? @
    593598      acc
    594599    ].
     
    625630(* the step calculating all products with least significant byte going in the
    626631   k-th position of the result *)
    627 let translate_mul_k : (Σk.k<|destrs|) → bind_new register (list (joint_seq RTL globals)) →
    628   bind_new register (list (joint_seq RTL globals)) ≝
     632let translate_mul_k : (Σk.k<|destrs|) → list (joint_seq RTL globals) →
     633  list (joint_seq RTL globals) ≝
    629634  λk_sig,acc.match k_sig with
    630635  [ mk_Sig k k_prf ⇒
     
    635640(* initializing tmp_destrs to zero
    636641   dummy is intentionally uninitialized *)
    637 translate_fill_with_zero … tmp_destrs @@
     642translate_fill_with_zero … tmp_destrs @
    638643(* the main body, roughly:
    639644   for k in 0 ... n-1 do
    640645     for i in 0 ... k do
    641646       translate_mul_i … k … i *)
    642 foldr … translate_mul_k [ ] (range_strong (|destrs|)) @@
     647foldr … translate_mul_k [ ] (range_strong (|destrs|)) @
    643648(* epilogue: saving the result *)
    644649translate_move … destrs (map … (Reg ?) tmp_destrs) ?.
Note: See TracChangeset for help on using the changeset viewer.