Changeset 1060 for src/RTLabs


Ignore:
Timestamp:
Jul 8, 2011, 12:17:14 PM (8 years ago)
Author:
mulligan
Message:

work from this morning and yesterday

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1059 r1060  
    33include "common/AssocList.ma".
    44include "common/Graphs.ma".
    5 include "common/Maps.ma".
    65(* include "common/IntValue.ma". *)
    76include "common/FrontEndOps.ma".
     
    227226  | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
    228227  | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
    229   | rtl_st_opaccs opaccs d s1 s2 _ ⇒ rtl_st_opaccs opaccs d s1 s2 lbl
     228  | rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl
    230229  | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
    231230  | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
     
    238237  | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
    239238  | rtl_st_cond_acc r l1 l2 ⇒ rtl_st_cond_acc r l1 l2
     239  | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl
     240  | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl
    240241  | rtl_st_return r ⇒ rtl_st_return r
    241242  ].
     
    299300  λsrcrs: list register.
    300301  λstart_lbl: label.
     302    match reduce_strong register destrs srcrs with
     303    [ dp crl_crr len_proof ⇒
     304      let commonl ≝ \fst (\fst crl_crr) in
     305      let commonr ≝ \fst (\snd crl_crr) in
     306      let restl ≝ \snd (\fst crl_crr) in
     307      let restr ≝ \snd (\snd crl_crr) in
     308      let f_common ≝ translate_move_internal start_lbl in
     309      let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
     310      let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
     311        add_translates [ translate1 ; translate2 ] start_lbl
     312    ].
     313    @len_proof
     314qed.
     315
     316let rec make
     317  (A: Type[0]) (elt: A) (n: nat) on n ≝
     318  match n with
     319  [ O ⇒ [ ]
     320  | S n' ⇒ elt :: make A elt n'
     321  ].
     322 
     323lemma make_length:
     324  ∀A: Type[0].
     325  ∀elt: A.
     326  ∀n: nat.
     327    n = length ? (make A elt n).
     328  #A #ELT #N
     329  elim N
     330  [ normalize %
     331  | #N #IH
     332    normalize <IH %
     333  ]
     334qed.
     335
     336definition translate_cast_unsigned ≝
     337  λdestrs.
     338  λstart_lbl.
     339  λdest_lbl.
     340  λdef.
     341  let 〈def, tmp_zero〉 ≝ fresh_reg def in
     342  let zeros ≝ make ? tmp_zero (length ? destrs) in
     343    add_translates [
     344      adds_graph [
     345        rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl
     346        ];
     347      translate_move destrs zeros
     348    ] start_lbl dest_lbl def.
     349
     350definition translate_cast_signed ≝
     351  λdestrs.
     352  λsrcr.
     353  λstart_lbl.
     354  λdest_lbl.
     355  λdef.
     356  let 〈def, tmp_128〉 ≝ fresh_reg def in
     357  let 〈def, tmp_255〉 ≝ fresh_reg def in
     358  let 〈def, tmpr〉 ≝ fresh_reg def in
     359  let 〈def, dummy〉 ≝ fresh_reg def in
     360  let insts ≝ [
     361    rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
     362    rtl_st_op2 And tmpr tmp_128 srcr start_lbl;
     363    rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl;
     364    rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl;
     365    rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
     366  ] in
     367  let srcrs ≝ make ? tmpr (length ? destrs) in
     368    add_translates [
     369      adds_graph insts;
     370      translate_move destrs srcrs
     371    ] start_lbl dest_lbl def.
     372
     373definition translate_cast ≝
     374  λsrc_size.
     375  λsrc_sign.
     376  λdest_size.
     377  λdestrs.
     378  λsrcrs.
     379  match | srcrs | return λx. | srcrs | = x → ? with
     380  [ O ⇒ λzero_prf. adds_graph [ ]
     381  | S n' ⇒ λsucc_prf.
     382    if ltb dest_size src_size then
     383      translate_move destrs srcrs
     384    else
     385      match reduce_strong ? destrs srcrs with
     386      [ dp crl len_proof ⇒
     387        let commonl ≝ \fst (\fst crl) in
     388        let commonr ≝ \fst (\snd crl) in
     389        let restl ≝ \snd (\fst crl) in
     390        let restr ≝ \snd (\snd crl) in
     391        let insts_common ≝ translate_move commonl commonr in
     392        let sign_reg ≝ last_safe ? srcrs ? in
     393        let insts_sign ≝
     394          match src_sign with
     395          [ Unsigned ⇒ translate_cast_unsigned restl
     396          | Signed ⇒ translate_cast_signed restl sign_reg
     397          ]
     398        in
     399          add_translates [ insts_common; insts_sign ]
     400      ]
     401  ] (refl ? (|srcrs|)).
     402  >succ_prf //
     403qed.
     404
     405definition translate_negint ≝
     406  λdestrs.
     407  λsrcrs.
     408  λstart_lbl.
     409  λdest_lbl.
     410  λdef.
     411  λprf: | destrs | = | srcrs |. (* assert in caml code *)
     412  let 〈def, tmpr〉 ≝ fresh_reg def in
     413  let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
     414  let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in
     415  let insts_init ≝ [
     416    rtl_st_set_carry start_lbl;
     417    rtl_st_int tmpr (zero ?) start_lbl
     418  ] in
     419  let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in
     420  let insts_add ≝ map … f_add destrs in
     421    adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
     422
     423definition translate_notbool ≝
     424  λdestrs.
     425  λsrcrs.
     426  λstart_lbl.
     427  λdest_lbl.
     428  λdef.
     429  match destrs with
     430  [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     431  | cons destr destrs ⇒
     432    let 〈def, tmpr〉 ≝ fresh_reg def in
     433    let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in
     434    let save_srcrs ≝ translate_move tmp_srcrs srcrs in
     435    let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in
     436    let f ≝ λtmp_srcr. [
     437      rtl_st_clear_carry start_lbl;
     438      rtl_st_int tmpr (zero ?) start_lbl;
     439      rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;
     440      rtl_st_int tmpr (zero ?) start_lbl;
     441      rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;
     442      rtl_st_op2 Xor destr destr tmpr start_lbl
     443    ] in
     444    let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in
     445    let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in
     446      add_translates [
     447        save_srcrs; adds_graph insts; epilogue
     448      ] start_lbl dest_lbl def
     449  ].
     450
     451definition translate_intermediate_op1 ≝
     452  λop1.
     453  λdestrs.
     454  λsrcrs.
     455  λstart_lbl.
     456  λdest_lbl.
     457  λdef.
    301458  λprf: | destrs | = | srcrs |.
    302     let 〈crl, crr〉 ≝ reduce register destrs srcrs in
    303     let 〈commonl, restl〉 ≝ crl in
    304     let 〈commonr, restr〉 ≝ crr in
    305     let f_common ≝ translate_move_internal start_lbl in
    306     let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
    307     let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
    308       add_translates [ translate1 ; translate2 ] start_lbl.
    309    
    310 let rec translate_move destrs srcrs start_lbl =
    311   let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
    312   let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
    313   let translates1 = adds_graph (List.map2 f_common common1 common2) in
    314   let translates2 = translate_cst (AST.Cst_int 0) rest1 in
    315   add_translates [translates1 ; translates2] start_lbl
     459  match op1 with
     460  [ intermediate_op1_cast src_size src_sign dest_size ⇒
     461      translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
     462  | intermediate_op1_negint ⇒
     463      translate_negint destrs srcrs start_lbl dest_lbl def prf
     464  | intermediate_op1_notbool ⇒
     465      translate_notbool destrs srcrs start_lbl dest_lbl def
     466  | intermediate_op1_notint ⇒
     467    let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
     468    let l ≝ map2 … f destrs srcrs prf in
     469      adds_graph l start_lbl dest_lbl def
     470  | intermediate_op1_ptrofint ⇒
     471      translate_move destrs srcrs start_lbl dest_lbl def
     472  | intermediate_op1_intofptr ⇒
     473      translate_move destrs srcrs start_lbl dest_lbl def
     474  | intermediate_op1_id ⇒
     475      translate_move destrs srcrs start_lbl dest_lbl def
     476  ].
    316477
    317478definition filter_and_to_list_local_env_internal ≝
Note: See TracChangeset for help on using the changeset viewer.