Changeset 1287 for src/RTLabs


Ignore:
Timestamp:
Oct 3, 2011, 4:55:17 PM (8 years ago)
Author:
mulligan
Message:

about 3/4 of the way through rtlabs to rtl now

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1286 r1287  
    509509(*
    510510definition translate_mul ≝
     511  λglobals: list ident.
    511512  λdestrs: list register.
    512513  λsrcrs1: list register.
     
    514515  λstart_lbl: label.
    515516  λdest_lbl: label.
    516   λdef: rtl_internal_function.
    517   let 〈def, dummy〉 ≝ fresh_reg def in
    518   let 〈def, tmpr〉 ≝ fresh_reg def in
    519   let 〈def, tmp_destrs〉 ≝ fresh_regs def (|destrs|) in
    520   let 〈def, fresh_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
    521   let 〈def, fresh_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
     517  λdef: rtl_internal_function globals.
     518  let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
     519  let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     520  let 〈def, tmp_destrs〉 ≝ fresh_regs rtl_params0 globals def (|destrs|) in
     521  let 〈def, fresh_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
     522  let 〈def, fresh_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
    522523  let insts_init ≝ [
    523     translate_move fresh_srcrs1 srcrs1;
    524     translate_move fresh_srcrs2 srcrs2;
    525     translate_cst (Ointconst I8 (zero ?)) destrs
     524    translate_move globals fresh_srcrs1 srcrs1;
     525    translate_move globals fresh_srcrs2 srcrs2;
     526    translate_cst globals (Ointconst I8 (zero …)) destrs
    526527  ]
    527528  in
    528   let f ≝ λi. translate_muli dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
    529   let insts_mul ≝ foldi ? ? [ ] srcrs2 in ?. [5: check insts_init.
     529  let f ≝ λi. translate_muli globals dummy tmpr destrs tmp_destrs ? fresh_srcrs1 start_lbl i ? in
     530  let insts_mul ≝ foldi [ ] srcrs2 in ?. [5: check insts_init.
    530531    add_translates (insts_init @ insts_mul) start_lbl dest_lbl def.
    531532*)
    532533
    533534definition translate_divumodu8 ≝
     535  λglobals: list ident.
    534536  λorder: bool.
    535537  λdestrs: list register.
     
    538540  λstart_lbl: label.
    539541  λdest_lbl: label.
    540   λdef: rtl_internal_function.
     542  λdef: rtl_internal_function globals.
    541543  match destrs with
    542   [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     544  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
    543545  | cons destr destrs ⇒
    544     let 〈def, dummy〉 ≝ fresh_reg def in
     546    let 〈def, dummy〉 ≝ fresh_reg rtl_params0 globals def in
    545547    let 〈destr1, destr2〉 ≝ match order with [ true ⇒ 〈destr, dummy〉 | _ ⇒ 〈dummy, destr〉 ] in
    546     let inst_div ≝ adds_graph [
    547       rtl_st_opaccs DivuModu destr1 destr2 srcr1 srcr2 start_lbl
     548    let inst_div ≝ adds_graph rtl_params1 globals [
     549      sequential rtl_params_ globals (OPACCS … DivuModu destr1 destr2 srcr1 srcr2)
    548550    ]
    549551    in
    550     let insts_rest ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
    551       add_translates [ inst_div; insts_rest ] start_lbl dest_lbl def
    552   ].
    553 
    554 definition translate_ne: ? → ? → ? → ? → ? → ? → rtl_internal_function ≝
     552    let insts_rest ≝ translate_cst globals (Ointconst I8 (zero ?)) destrs in
     553      add_translates rtl_params1 globals [ inst_div; insts_rest ] start_lbl dest_lbl def
     554  ].
     555
     556definition translate_ne: ∀globals: list ident. ? → ? → ? → ? → ? → ? → rtl_internal_function globals ≝
     557  λglobals: list ident.
    555558  λdestrs: list register.
    556559  λsrcrs1: list register.
     
    558561  λstart_lbl: label.
    559562  λdest_lbl: label.
    560   λdef: rtl_internal_function.
     563  λdef: rtl_internal_function globals.
    561564  match destrs with
    562   [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     565  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
    563566  | cons destr destrs ⇒
    564     let 〈def, tmpr〉 ≝ fresh_reg def in
    565     let 〈def, tmp_zero〉 ≝ fresh_reg def in
    566     let 〈def, tmp_srcrs1〉 ≝ fresh_regs def (|srcrs1|) in
    567     let save_srcrs1 ≝ translate_move tmp_srcrs1 srcrs1 in
    568     let 〈def, tmp_srcrs2〉 ≝ fresh_regs def (|srcrs2|) in
    569     let save_srcrs2 ≝ translate_move tmp_srcrs2 srcrs2 in
     567    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     568    let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params0 globals def in
     569    let 〈def, tmp_srcrs1〉 ≝ fresh_regs rtl_params0 globals def (|srcrs1|) in
     570    let save_srcrs1 ≝ translate_move globals tmp_srcrs1 srcrs1 in
     571    let 〈def, tmp_srcrs2〉 ≝ fresh_regs rtl_params0 globals def (|srcrs2|) in
     572    let save_srcrs2 ≝ translate_move globals tmp_srcrs2 srcrs2 in
    570573    match reduce_strong register register tmp_srcrs1 tmp_srcrs2 with
    571574    [ dp crl their_proof ⇒
     
    576579      let rest ≝ choose_rest ? restl restr ? ? in
    577580      let inits ≝ [
    578         rtl_st_int destr (zero ?) start_lbl;
    579         rtl_st_int tmp_zero (zero ?) start_lbl
     581        sequential … (INT rtl_params_ globals destr (zero …));
     582        sequential … (INT rtl_params_ globals tmp_zero (zero …))
    580583      ]
    581584      in
    582585      let f_common ≝ λtmp_srcr1. λtmp_srcr2. [
    583         rtl_st_clear_carry start_lbl;
    584         rtl_st_op2 Sub tmpr tmp_srcr1 tmp_srcr2 start_lbl;
    585         rtl_st_op2 Or destr destr tmpr start_lbl
     586        sequential … (CLEAR_CARRY …);
     587        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_srcr1 tmp_srcr2);
     588        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
    586589      ]
    587590      in
    588       let insts_common ≝ flatten ? (map2 … f_common commonl commonr ?) in
     591      let insts_common ≝ flatten (map2 … f_common commonl commonr ?) in
    589592      let f_rest ≝ λtmp_srcr. [
    590         rtl_st_clear_carry start_lbl;
    591         rtl_st_op2 Sub tmpr tmp_zero tmp_srcr start_lbl;
    592         rtl_st_op2 Or destr destr tmpr start_lbl
     593        sequential … (CLEAR_CARRY …);
     594        sequential … (OP2 rtl_params_ globals Sub tmpr tmp_zero tmp_srcr);
     595        sequential … (OP2 rtl_params_ globals Or destr destr tmpr)
    593596      ]
    594597      in
    595       let insts_rest ≝ flatten ? (map ? ? f_rest rest) in
     598      let insts_rest ≝ flatten … (map … f_rest rest) in
    596599      let insts ≝ inits @ insts_common @ insts_rest in
    597       let epilogue ≝ translate_cst (Ointconst I8 (zero ?)) destrs in
    598         add_translates [
    599           save_srcrs1; save_srcrs2; adds_graph insts; epilogue
     600      let epilogue ≝ translate_cst globals (Ointconst I8 (zero …)) destrs in
     601        add_translates rtl_params1 globals [
     602          save_srcrs1; save_srcrs2; adds_graph rtl_params1 globals insts; epilogue
    600603        ] start_lbl dest_lbl def
    601604    ]
     
    609612
    610613definition translate_eq_reg ≝
     614  λglobals: list ident.
    611615  λtmp_zero: register.
    612616  λtmp_one: register.
     
    617621  λsrcr12: register × register.
    618622  let 〈srcr1, srcr2〉 ≝ srcr12 in
    619   [ rtl_st_clear_carry dummy_lbl;
    620     rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
    621     rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
    622     rtl_st_op2 Sub tmpr2 srcr2 srcr1 dummy_lbl;
    623     rtl_st_op2 Addc tmpr2 tmp_zero tmp_zero dummy_lbl;
    624     rtl_st_op2 Or tmpr1 tmpr1 tmpr2 dummy_lbl;
    625     rtl_st_op2 Xor tmpr1 tmpr1 tmp_one dummy_lbl;
    626     rtl_st_op2 And destr destr tmpr1 dummy_lbl ].
     623  [ sequential … (CLEAR_CARRY …);
     624    sequential rtl_params_ globals (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
     625    sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
     626    sequential … (OP2 rtl_params_ globals Sub tmpr2 srcr2 srcr1);
     627    sequential … (OP2 rtl_params_ globals Addc tmpr2 tmp_zero tmp_zero);
     628    sequential … (OP2 rtl_params_ globals Or tmpr1 tmpr1 tmpr2);
     629    sequential … (OP2 rtl_params_ globals Xor tmpr1 tmpr1 tmp_one);
     630    sequential … (OP2 rtl_params_ globals And destr destr tmpr1) ].
    627631
    628632definition translate_eq_list ≝
     633  λglobals: list ident.
    629634  λtmp_zero: register.
    630635  λtmp_one: register.
     
    634639  λleq: list (register × register).
    635640  λdummy_lbl: label.
    636   let f ≝ translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
    637     (rtl_st_int destr (bitvector_of_nat ? 1) dummy_lbl) ::
    638       flatten ? (map ? ? f leq).
     641  let f ≝ translate_eq_reg globals tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
     642    (sequential … (INT rtl_params_ globals destr (bitvector_of_nat ? 1))) ::
     643      flatten … (map … f leq).
    639644
    640645definition translate_atom ≝
     646  λglobals: list ident.
    641647  λtmp_zero: register.
    642648  λtmp_one: register.
     
    649655  λsrcr1: register.
    650656  λsrcr2: register.
    651     translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
    652     [ rtl_st_clear_carry dummy_lbl;
    653       rtl_st_op2 Sub tmpr1 srcr1 srcr2 dummy_lbl;
    654       rtl_st_op2 Addc tmpr1 tmp_zero tmp_zero dummy_lbl;
    655       rtl_st_op2 And tmpr3 tmpr3 tmpr1 dummy_lbl;
    656       rtl_st_op2 Or destr destr tmpr3 dummy_lbl ].
     657    translate_eq_list globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl @
     658    [ sequential … (CLEAR_CARRY …);
     659      sequential … (OP2 rtl_params_ globals Sub tmpr1 srcr1 srcr2);
     660      sequential … (OP2 rtl_params_ globals Addc tmpr1 tmp_zero tmp_zero);
     661      sequential … (OP2 rtl_params_ globals And tmpr3 tmpr3 tmpr1);
     662      sequential … (OP2 rtl_params_ globals Or destr destr tmpr3) ].
    657663
    658664definition translate_lt_main ≝
     665  λglobals: list ident.
    659666  λtmp_zero: register.
    660667  λtmp_one: register.
     
    669676  let f ≝ λinsts_leq. λsrcr1. λsrcr2.
    670677    let 〈insts, leq〉 ≝ insts_leq in
    671     let added_insts ≝ translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
     678    let added_insts ≝ translate_atom globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq srcr1 srcr2 in
    672679      〈insts @ added_insts, leq @ [〈srcr1, srcr2〉]〉
    673680  in
    674     \fst (fold_left2 ? ? ? f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
     681    \fst (fold_left2 f 〈[ ], [ ]〉 srcrs1 srcrs2 proof).
    675682
    676683definition fresh_regs_strong:
    677   rtl_internal_function → ∀n: nat. Σfresh: rtl_internal_function × (list register). |\snd fresh| = n ≝
     684  ∀globals. rtl_internal_function globals → ∀n: nat. Σfresh: (rtl_internal_function globals) × (list register). |\snd fresh| = n ≝
     685  λglobals: list ident.
    678686  λdef.
    679687  λn.
    680     fresh_regs def n.
     688    fresh_regs rtl_params0 globals def n.
    681689  @fresh_regs_length
    682690qed.
    683691
    684692definition complete_regs_strong:
    685   rtl_internal_function → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
     693  ∀globals: list ident. rtl_internal_function globals → list register → list register → Σcomplete: (list register) × (list register) × (list register). |\fst (\fst complete)| = |\snd (\fst complete)| ≝
     694  λglobals: list ident.
    686695  λdef.
    687696  λleft.
    688697  λright.
    689     complete_regs def left right.
     698    complete_regs globals def left right.
    690699  @complete_regs_length
    691700qed.
    692701
    693702definition translate_lt ≝
     703  λglobals: list ident.
    694704  λdestrs: list register.
    695705  λprf_destrs: lt 0 (|destrs|).
     
    698708  λstart_lbl: label.
    699709  λdest_lbl: label.
    700   λdef: rtl_internal_function.
     710  λdef: rtl_internal_function globals.
    701711  match destrs with
    702   [ nil ⇒ add_graph start_lbl (rtl_st_skip dest_lbl) def
     712  [ nil ⇒ add_graph rtl_params1 globals start_lbl (GOTO … dest_lbl) def
    703713  | _ ⇒
    704     match fresh_regs_strong def (|destrs|) with
     714    match fresh_regs_strong globals def (|destrs|) with
    705715    [ dp def_tmp_destrs tmp_destrs_proof ⇒
    706716      let def ≝ \fst def_tmp_destrs in
    707717      let tmp_destrs ≝ \snd def_tmp_destrs in
    708718      let tmp_destr ≝ hd_safe ? tmp_destrs ? in
    709       let 〈def, tmp_zero〉 ≝ fresh_reg def in
    710       let 〈def, tmp_one〉 ≝ fresh_reg def in
    711       let 〈def, tmpr1〉 ≝ fresh_reg def in
    712       let 〈def, tmpr2〉 ≝ fresh_reg def in
    713       let 〈def, tmpr3〉 ≝ fresh_reg def in
    714       match complete_regs_strong def srcrs1 srcrs2 with
     719      let 〈def, tmp_zero〉 ≝ fresh_reg rtl_params1 globals def in
     720      let 〈def, tmp_one〉 ≝ fresh_reg rtl_params1 globals def in
     721      let 〈def, tmpr1〉 ≝ fresh_reg rtl_params1 globals def in
     722      let 〈def, tmpr2〉 ≝ fresh_reg rtl_params1 globals def in
     723      let 〈def, tmpr3〉 ≝ fresh_reg rtl_params1 globals def in
     724      match complete_regs_strong globals def srcrs1 srcrs2 with
    715725      [ dp srcrs12_added srcrs12_proof ⇒
    716726        let srcrs1 ≝ \fst (\fst srcrs12_added) in
    717727        let srcrs2 ≝ \snd (\fst srcrs12_added) in
    718728        let added ≝ \snd srcrs12_added in
    719         let srcrs1' ≝ rev ? srcrs1 in
    720         let srcrs2' ≝ rev ? srcrs2 in
     729        let srcrs1' ≝ rev srcrs1 in
     730        let srcrs2' ≝ rev srcrs2 in
    721731        let insts_init ≝ [
    722           translate_cst (Ointconst I8 (zero ?)) tmp_destrs;
    723           translate_cst (Ointconst I8 (zero ?)) added;
    724           adds_graph [
    725             rtl_st_int tmp_zero (zero ?) start_lbl;
    726             rtl_st_int tmp_one (bitvector_of_nat ? 1) start_lbl
     732          translate_cst globals (Ointconst I8 (zero ?)) tmp_destrs;
     733          translate_cst globals (Ointconst I8 (zero ?)) added;
     734          adds_graph rtl_params1 globals [
     735            sequential rtl_params_ globals (INT rtl_params_ globals tmp_zero (zero …));
     736            sequential rtl_params_ globals (INT rtl_params_ globals tmp_one (bitvector_of_nat … 1))
    727737          ]
    728738        ]
    729739        in
    730740        let insts_main ≝
    731           translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
    732           let insts_main ≝ [ adds_graph insts_main ] in
    733           let insts_exit ≝ [ translate_move destrs tmp_destrs ] in
    734             add_translates (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
     741          translate_lt_main globals tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl srcrs1' srcrs2' ? in
     742          let insts_main ≝ [ adds_graph rtl_params1 globals insts_main ] in
     743          let insts_exit ≝ [ translate_move globals destrs tmp_destrs ] in
     744            add_translates rtl_params1 globals (insts_init @ insts_main @ insts_exit) start_lbl dest_lbl def
    735745      ]
    736746    ]
     
    744754
    745755definition add_128_to_last ≝
     756  λglobals: list ident.
    746757  λtmp_128: register.
    747758  λrs.
     
    749760  λstart_lbl: label.
    750761  match rs with
    751   [ nil ⇒ adds_graph [ ] start_lbl
     762  [ nil ⇒ adds_graph rtl_params1 globals [ ] start_lbl
    752763  | _ ⇒
    753     let r ≝ last_safe ? rs prf in
    754       adds_graph [
    755         rtl_st_op2 Add r r tmp_128 start_lbl
     764    let r ≝ last_safe rs prf in
     765      adds_graph rtl_params1 globals [
     766        sequential rtl_params_ globals (OP2 rtl_params_ globals Add r r tmp_128)
    756767      ] start_lbl
    757768  ].
    758769
    759770definition translate_lts ≝
     771  λglobals: list ident.
    760772  λdestrs: list register.
    761773  λdestrs_prf: lt 0 (|destrs|).
     
    766778  λstart_lbl: label.
    767779  λdest_lbl: label.
    768   λdef: rtl_internal_function.
    769   match fresh_regs_strong def (|srcrs1|) with
     780  λdef: rtl_internal_function globals.
     781  match fresh_regs_strong globals def (|srcrs1|) with
    770782  [ dp def_tmp_srcrs1 srcrs1_prf ⇒
    771783    let def ≝ \fst def_tmp_srcrs1 in
    772784    let tmp_srcrs1 ≝ \snd def_tmp_srcrs1 in
    773     match fresh_regs_strong def (|srcrs2|) with
     785    match fresh_regs_strong globals def (|srcrs2|) with
    774786    [ dp def_tmp_srcrs2 srcrs2_prf ⇒
    775787      let def ≝ \fst def_tmp_srcrs2 in
    776788      let tmp_srcrs2 ≝ \snd def_tmp_srcrs2 in
    777       let 〈def, tmp_128〉 ≝ fresh_reg def in
    778         add_translates [
    779           translate_move tmp_srcrs1 srcrs1;
    780           translate_move tmp_srcrs2 srcrs2;
    781           adds_graph [
    782             rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl
     789      let 〈def, tmp_128〉 ≝ fresh_reg rtl_params0 globals def in
     790        add_translates rtl_params1 globals [
     791          translate_move globals tmp_srcrs1 srcrs1;
     792          translate_move globals tmp_srcrs2 srcrs2;
     793          adds_graph rtl_params1 globals [
     794            sequential rtl_params_ globals (INT rtl_params_ globals tmp_128 (bitvector_of_nat ? 128))
    783795          ];
    784           add_128_to_last tmp_128 tmp_srcrs1 ?;
    785           add_128_to_last tmp_128 tmp_srcrs2 ?;
    786           translate_lt destrs destrs_prf tmp_srcrs1 tmp_srcrs2
     796          add_128_to_last globals tmp_128 tmp_srcrs1 ?;
     797          add_128_to_last globals tmp_128 tmp_srcrs2 ?;
     798          translate_lt globals destrs destrs_prf tmp_srcrs1 tmp_srcrs2
    787799        ] start_lbl dest_lbl def
    788800    ]
Note: See TracChangeset for help on using the changeset viewer.