Changeset 2866


Ignore:
Timestamp:
Mar 13, 2013, 4:21:43 PM (4 years ago)
Author:
tranquil
Message:

corrected two bugs of the translation: constant translation used wrong endianess, and multibyte adding did not insert correct uses of Addc.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r2823 r2866  
    173173definition split_into_bytes:
    174174  ∀size. ∀int: bvint size. Σbytes: list Byte. |bytes| = size_intsize size ≝
    175 λsize.vrsplit ? (size_intsize size) 8.
     175λsize,int.reverse … (vrsplit ? (size_intsize size) 8 int).
     176>length_reverse @pi2 qed.
    176177
    177178let rec list_inject_All_aux A P (l : list A) on l : All A P l → list (Σx.P x) ≝
     
    180181| cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_inject_All_aux A P tl (proj2 … prf)
    181182].
     183
     184definition translate_op_aux:
     185  ∀globals. Op2 →
     186  ∀dests : list register.
     187  ∀srcrs1 : list psd_argument.
     188  ∀srcrs2 : list psd_argument.
     189  |dests| = |srcrs1| → |srcrs1| = |srcrs2| →
     190  list (joint_seq RTL globals)
     191  ≝
     192  λglobals: list ident.
     193  λop.
     194  λdestrs.
     195  λsrcrs1.
     196  λsrcrs2.
     197  λprf1,prf2.
     198  (* first, clear carry if op relies on it *)
     199  map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2.
    182200
    183201definition translate_op:
     
    194212  λsrcrs1.
    195213  λsrcrs2.
    196   λprf1,prf2.
    197   (* first, clear carry if op relies on it *)
    198214  match op with
    199   [ Addc ⇒ [CLEAR_CARRY ??]
    200   | Sub ⇒ [CLEAR_CARRY ??]
    201   | _ ⇒ [ ]
    202   ] @ map3 ???? (OP2 RTL globals op) destrs srcrs1 srcrs2 prf1 prf2.
     215  [ Add ⇒
     216    match destrs return λdestrs.|destrs| = |srcrs1| → |srcrs1| = |srcrs2| → ? with
     217    [ nil ⇒ λ_.λ_.[ ]
     218    | cons destr destrs' ⇒
     219      match srcrs1 return λsrcrs1.S(|destrs'|) = |srcrs1| → |srcrs1| = |srcrs2| → ? with
     220      [ nil ⇒ λprf1.⊥
     221      | cons srcr1 srcrs1' ⇒
     222        λprf1.
     223        match srcrs2 return λsrcrs2.S(|srcrs1'|) = |srcrs2| → ? with
     224        [ nil ⇒ λprf2.⊥
     225        | cons srcr2 srcrs2' ⇒
     226          λprf2.OP2 ?? Add destr srcr1 srcr2 :: translate_op_aux … Addc destrs' srcrs1' srcrs2' ??
     227        ]
     228      ]
     229    ]
     230  | Sub ⇒ λprf1,prf2.[ CLEAR_CARRY ?? ] @ translate_op_aux … Sub … prf1 prf2
     231  | Addc ⇒ λprf1,prf2.[ CLEAR_CARRY ?? ] @ translate_op_aux … Addc … prf1 prf2
     232  | _ ⇒ translate_op_aux … op destrs srcrs1 srcrs2
     233  ].
     234  normalize in prf1 prf2; destruct assumption qed.
    203235
    204236definition cast_list : ∀A.A → ℕ → list A → list A ≝
     
    249281qed.
    250282
    251 let rec nat_to_args (size : nat) (k : nat) on size : Σl : list psd_argument.|l| = size ≝
    252 match size with
    253 [ O ⇒ [ ]
    254 | S size' ⇒
    255   (byte_of_nat k : psd_argument) :: nat_to_args size' (k ÷ 8)
    256 ]. @hide_prf [ % | cases (nat_to_args ??) #res #EQ  normalize >EQ % ] qed.
     283definition zero_args : ∀size.Σl : list psd_argument.|l| = size ≝
     284λsize.
     285«make_list psd_argument (zero_byte) size, length_make_list …».
     286
     287definition one_args : ∀size.Σl : list psd_argument.|l| = size ≝
     288λsize.match size return λsize.Σl : list psd_argument.|l| = size with
     289[ O ⇒ «[ ], refl …»
     290| S k ⇒ (byte_of_nat 1 : psd_argument) :: zero_args k
     291].
     292whd in ⊢ (??%?); @eq_f @pi2 qed.
    257293
    258294definition size_of_cst ≝ λtyp.λcst : constant typ.match cst with
     
    347383  list register → list (joint_seq RTL globals) ≝
    348384  λglobals,destrs.
    349   match nat_to_args (|destrs|) 0 with
    350   [ mk_Sig res prf ⇒ translate_move ? destrs res ?].
    351   // qed.
     385  translate_move ? destrs (zero_args (|destrs|)) ?.
     386  @sym_eq @pi2 qed.
    352387
    353388let rec last A (l : list A) on l : option A ≝
     
    450485  λprf: |destrs| = |srcrs|. (* assert in caml code *)
    451486  translate_notint … destrs srcrs prf @@
    452   translate_op ? Add destrs (map … (Reg ?) destrs) (nat_to_args (|destrs|) 1) ??.
    453 @hide_prf >length_map [ cases (nat_to_args ??) ] // qed.
     487  translate_op ? Add destrs (map … (Reg ?) destrs) (one_args (|destrs|)) ??.
     488@hide_prf
     489>length_map [ @sym_eq @pi2 | % ] qed.
    454490
    455491definition translate_notbool:
Note: See TracChangeset for help on using the changeset viewer.