Changeset 1285 for src/RTLabs


Ignore:
Timestamp:
Oct 3, 2011, 3:08:21 PM (8 years ago)
Author:
mulligan
Message:

more implementation on maps, final push to get rtl abs to rtl working

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1283 r1285  
    216216    ] start_lbl dest_lbl def.
    217217
    218 (*
    219 definition translate_cast_signed
    220   λglobals.
     218definition translate_cast_signed:
     219    ∀globals: list ident. list register → ? → label → label → rtl_internal_function globals → rtl_internal_function globals
     220  λglobals: list ident.
    221221  λdestrs.
    222222  λsrcr.
     
    229229  let 〈def, dummy〉 ≝ fresh_reg … def in
    230230  let insts ≝ [
    231     rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
    232     rtl_st_op2 And tmpr tmp_128 srcr start_lbl;
    233     rtl_st_opaccs DivuModu tmpr dummy tmpr tmp_128 start_lbl;
    234     rtl_st_int tmp_255 (bitvector_of_nat ? 255) start_lbl;
    235     rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
    236   ] in
     231    sequential  … (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128));
     232    sequential … (OP2 rtl_params_ globals And tmpr tmp_128 srcr);
     233    sequential … (OPACCS rtl_params_ globals DivuModu tmpr dummy tmpr tmp_128);
     234    sequential … (INT rtl_params_ globals tmp_255 (bitvector_of_nat ? 255));
     235    sequential … (OPACCS rtl_params_ globals Mul tmpr dummy tmpr tmp_255)
     236  ]
     237  in
    237238  let srcrs ≝ make … tmpr (length … destrs) in
    238     add_translates [
    239       adds_graph insts;
    240       translate_move destrs srcrs
     239    add_translates rtl_params1 globals [
     240      adds_graph rtl_params1 globals insts;
     241      translate_move globals destrs srcrs
    241242    ] start_lbl dest_lbl def.
    242243
    243244definition translate_cast ≝
    244   λsrc_size.
    245   λsrc_sign.
    246   λdest_size.
    247   λdestrs.
    248   λsrcrs.
     245  λglobals: list ident.
     246  λsrc_size: nat.
     247  λsrc_sign: signedness.
     248  λdest_size: nat.
     249  λdestrs: list register.
     250  λsrcrs: list register.
    249251  match |srcrs| return λx. |srcrs| = x → ? with
    250   [ O ⇒ λzero_prf. adds_graph [ ]
     252  [ O ⇒ λzero_prf. adds_graph rtl_params1 globals [ ]
    251253  | S n' ⇒ λsucc_prf.
    252254    if ltb dest_size src_size then
    253       translate_move destrs srcrs
     255      translate_move globals destrs srcrs
    254256    else
    255257      match reduce_strong register register destrs srcrs with
     
    259261        let restl ≝ \snd (\fst crl) in
    260262        let restr ≝ \snd (\snd crl) in
    261         let insts_common ≝ translate_move commonl commonr in
     263        let insts_common ≝ translate_move globals commonl commonr in
    262264        let sign_reg ≝ last_safe ? srcrs ? in
    263265        let insts_sign ≝
    264266          match src_sign with
    265           [ Unsigned ⇒ translate_cast_unsigned restl
    266           | Signed ⇒ translate_cast_signed restl sign_reg
     267          [ Unsigned ⇒ translate_cast_unsigned globals restl
     268          | Signed ⇒ translate_cast_signed globals restl sign_reg
    267269          ]
    268270        in
    269           add_translates [ insts_common; insts_sign ]
     271          add_translates rtl_params1 globals [ insts_common; insts_sign ]
    270272      ]
    271273  ] (refl ? (|srcrs|)).
     
    274276
    275277definition translate_negint ≝
    276   λdestrs.
    277   λsrcrs.
    278   λstart_lbl.
    279   λdest_lbl.
    280   λdef.
    281   λprf: | destrs | = | srcrs |. (* assert in caml code *)
    282   let 〈def, tmpr〉 ≝ fresh_reg def in
    283   let f_cmpl ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
    284   let insts_cmpl ≝ map2 ? ? ? f_cmpl destrs srcrs prf in
     278  λglobals: list ident.
     279  λdestrs: list register.
     280  λsrcrs: list register.
     281  λstart_lbl: label.
     282  λdest_lbl: label.
     283  λdef: rtl_internal_function globals.
     284  λprf: |destrs| = |srcrs|. (* assert in caml code *)
     285  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     286  let f_cmpl ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 rtl_params1 globals Cmpl destr srcr) in
     287  let insts_cmpl ≝ map2 … f_cmpl destrs srcrs prf in
    285288  let insts_init ≝ [
    286     rtl_st_set_carry start_lbl;
    287     rtl_st_int tmpr (zero ?) start_lbl
     289    sequential … (SET_CARRY …);
     290    sequential … (INT rtl_params_ globals tmpr (zero ?))
    288291  ] in
    289   let f_add ≝ λdestr. rtl_st_op2 Addc destr destr tmpr start_lbl in
     292  let f_add ≝ λdestr. sequential … (OP2 rtl_params_ globals Addc destr destr tmpr) in
    290293  let insts_add ≝ map … f_add destrs in
    291     adds_graph (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
    292 
    293 definition translate_notbool ≝
    294   λdestrs.
    295   λsrcrs.
    296   λstart_lbl.
    297   λdest_lbl.
    298   λdef.
     294    adds_graph rtl_params1 globals (insts_cmpl @ insts_init @ insts_add) start_lbl dest_lbl def.
     295
     296definition translate_notbool: ∀globals. list register → list register → label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     297  λglobals: list ident.
     298  λdestrs: list register.
     299  λsrcrs: list register.
     300  λstart_lbl: label.
     301  λdest_lbl: label.
     302  λdef: rtl_internal_function globals.
    299303  match destrs with
    300   [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     304  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … start_lbl) def
    301305  | cons destr destrs ⇒
    302     let 〈def, tmpr〉 ≝ fresh_reg def in
    303     let 〈def, tmp_srcrs〉 ≝ fresh_regs def (length ? srcrs) in
    304     let save_srcrs ≝ translate_move tmp_srcrs srcrs in
    305     let init_destr ≝ rtl_st_int destr (bitvector_of_nat ? 1) start_lbl in
     306    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     307    let 〈def, tmp_srcrs〉 ≝ fresh_regs rtl_params0 globals def (length ? srcrs) in
     308    let save_srcrs ≝ translate_move globals tmp_srcrs srcrs in
     309    let init_destr ≝ sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1)) in
    306310    let f ≝ λtmp_srcr. [
    307       rtl_st_clear_carry start_lbl;
    308       rtl_st_int tmpr (zero ?) start_lbl;
    309       rtl_st_op2 Sub tmpr tmpr tmp_srcr start_lbl;
    310       rtl_st_int tmpr (zero ?) start_lbl;
    311       rtl_st_op2 Addc tmpr tmpr tmpr start_lbl;
    312       rtl_st_op2 Xor destr destr tmpr start_lbl
     311      sequential … (CLEAR_CARRY rtl_params_ globals);
     312      sequential … (INT rtl_params_ globals tmpr (zero ?));
     313      sequential … (OP2 rtl_params_ globals Sub tmpr tmpr tmp_srcr);
     314      sequential … (INT rtl_params_ globals tmpr (zero ?));
     315      sequential … (OP2 rtl_params_ globals Addc tmpr tmpr tmpr);
     316      sequential … (OP2 rtl_params_ globals Xor destr destr tmpr)
    313317    ] in
    314     let insts ≝ init_destr :: (flatten ? (map … f tmp_srcrs)) in
    315     let epilogue ≝ translate_cst (Ointconst I8 (bitvector_of_nat ? 0)) destrs in
    316       add_translates [
    317         save_srcrs; adds_graph insts; epilogue
     318    let insts ≝ init_destr :: (flatten (map … f tmp_srcrs)) in
     319    let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
     320      add_translates rtl_params1 globals [
     321        save_srcrs; adds_graph rtl_params1 globals insts; epilogue
    318322      ] start_lbl dest_lbl def
    319323  ].
     324
     325(*
    320326
    321327(* TODO: examine this properly.  This is a change from the O'caml code due
Note: See TracChangeset for help on using the changeset viewer.