Changeset 1286 for src/RTLabs


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

more changes to the rtl abs to rtl pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1285 r1286  
    323323  ].
    324324
    325 (*
    326 
    327325(* TODO: examine this properly.  This is a change from the O'caml code due
    328326   to us dropping the explicit use of a cast destination size field.  We
     
    331329*)
    332330definition translate_op1 ≝
     331  λglobals: list ident.
    333332  λop1: unary_operation.
    334333  λdestrs: list register.
     
    337336  λstart_lbl: label.
    338337  λdest_lbl: label.
    339   λdef: rtl_internal_function.
     338  λdef: rtl_internal_function globals.
    340339  match op1 with
    341340  [ Ocastint src_sign src_size ⇒
    342341    let dest_size ≝ |destrs| * 8 in
    343342    let src_size ≝ bitsize_of_intsize src_size in
    344       translate_cast src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
     343      translate_cast globals src_size src_sign dest_size destrs srcrs start_lbl dest_lbl def
    345344  | Onegint ⇒
    346       translate_negint destrs srcrs start_lbl dest_lbl def prf
     345      translate_negint globals destrs srcrs start_lbl dest_lbl def prf
    347346  | Onotbool ⇒
    348       translate_notbool destrs srcrs start_lbl dest_lbl def
     347      translate_notbool globals destrs srcrs start_lbl dest_lbl def
    349348  | Onotint ⇒
    350     let f ≝ λdestr. λsrcr. rtl_st_op1 Cmpl destr srcr start_lbl in
     349    let f ≝ λdestr. λsrcr. sequential rtl_params_ globals (OP1 … Cmpl destr srcr) in
    351350    let l ≝ map2 … f destrs srcrs prf in
    352       adds_graph l start_lbl dest_lbl def
     351      adds_graph rtl_params1 globals l start_lbl dest_lbl def
    353352  | Optrofint r ⇒
    354       translate_move destrs srcrs start_lbl dest_lbl def
     353      translate_move globals destrs srcrs start_lbl dest_lbl def
    355354  | Ointofptr r ⇒
    356       translate_move destrs srcrs start_lbl dest_lbl def
     355      translate_move globals destrs srcrs start_lbl dest_lbl def
    357356  | Oid ⇒
    358       translate_move destrs srcrs start_lbl dest_lbl def
     357      translate_move globals destrs srcrs start_lbl dest_lbl def
    359358  | _ ⇒ ? (* float operations implemented in runtime *)
    360359  ].
     
    362361qed.
    363362 
    364 definition translate_op ≝
     363definition translate_op: ∀globals. ? → list register → list register → list register →
     364  label → label → rtl_internal_function globals → rtl_internal_function globals ≝
     365  λglobals: list ident.
    365366  λop.
    366   λdestrs.
    367   λsrcrs1.
    368   λsrcrs2.
    369   λstart_lbl.
    370   λdest_lbl.
    371   λdef.
     367  λdestrs: list register.
     368  λsrcrs1: list register.
     369  λsrcrs2: list register.
     370  λstart_lbl: label.
     371  λdest_lbl: label.
     372  λdef: rtl_internal_function globals.
    372373  match reduce_strong register register srcrs1 srcrs2 with
    373374  [ dp reduced first_reduced_proof ⇒
     
    386387        let destrs_rest ≝ \snd (\fst reduced) in
    387388        let srcrs_cted ≝ \fst (\snd reduced) in
    388         let 〈def, tmpr〉 ≝ fresh_reg def in
     389        let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    389390        let insts_init ≝ [
    390           rtl_st_clear_carry start_lbl;
    391           rtl_st_int tmpr (zero ?) start_lbl
     391          sequential … (CLEAR_CARRY …);
     392          sequential … (INT rtl_params_ globals tmpr (zero …))
    392393        ] in
    393         let f_add ≝ λdestr. λsrcr1. λsrcr2. rtl_st_op2 op destr srcr1 srcr2 start_lbl in
    394         let insts_add ≝ map3 f_add destrs_common srcrsl_common srcrsr_common ? ? in
    395         let f_add_cted ≝ λdestr. λsrcr. rtl_st_op2 op destr srcr tmpr start_lbl in
    396         let insts_add_cted ≝ map2 ? ? ? f_add_cted destrs_cted srcrs_cted ? in
    397         let f_rest ≝ λdestr. rtl_st_op2 op destr tmpr tmpr start_lbl in
     394        let f_add ≝ λdestr. λsrcr1. λsrcr2. sequential … (OP2 rtl_params_ globals op destr srcr1 srcr2) in
     395        let insts_add ≝ map3 ? ? ? ? f_add destrs_common srcrsl_common srcrsr_common ? ? in
     396        let f_add_cted ≝ λdestr. λsrcr. sequential … (OP2 rtl_params_ globals op destr srcr tmpr) in
     397        let insts_add_cted ≝ map2 f_add_cted destrs_cted srcrs_cted ? in
     398        let f_rest ≝ λdestr. sequential … (OP2 rtl_params_ globals op destr tmpr tmpr) in
    398399        let insts_rest ≝ map … f_rest destrs_rest in
    399           adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
     400          adds_graph rtl_params1 globals (insts_init @ insts_add @ insts_add_cted @ insts_rest) start_lbl dest_lbl def
    400401      ]
    401402    ]
     
    403404  [1: @third_reduced_proof
    404405  |3: @first_reduced_proof
    405   |*: cases daemon (* TODO *)
     406  |*: cases daemon (* XXX: some of these look like they may be false *)
    406407  ]
    407408qed.
    408409
    409410let rec translate_mul1
    410   (dummy: register) (tmpr: register) (destrs: list register)
    411   (srcrs1: list register) (srcr2: register) (start_lbl: label)
    412     on srcrs1 ≝
     411  (globals: list ident) (dummy: register) (tmpr: register)
     412    (destrs: list register) (srcrs1: list register) (srcr2: register)
     413      (start_lbl: label)
     414        on srcrs1 ≝
    413415  match destrs with
    414   [ nil ⇒ adds_graph [ rtl_st_skip start_lbl ] start_lbl
     416  [ nil ⇒ adds_graph rtl_params1 globals [ GOTO … ] start_lbl
    415417  | cons destr tl ⇒
    416418    match tl with
     
    418420      match srcrs1 with
    419421      [ nil ⇒
    420         adds_graph [
    421           rtl_st_int tmpr (zero ?) start_lbl;
    422           rtl_st_op2 Addc destr destr tmpr start_lbl
     422        adds_graph rtl_params1 globals [
     423          sequential … (INT rtl_params_ globals tmpr (zero …));
     424          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
    423425        ] start_lbl
    424426      | cons srcr1 tl' ⇒
    425         adds_graph [
    426           rtl_st_opaccs Mul tmpr dummy srcr2 srcr1 start_lbl;
    427           rtl_st_op2 Addc destr destr tmpr start_lbl
     427        adds_graph rtl_params1 globals [
     428          sequential … (OPACCS rtl_params_ globals Mul tmpr dummy srcr2 srcr1);
     429          sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
    428430        ] start_lbl
    429431      ]
     
    431433      match srcrs1 with
    432434      [ nil ⇒
    433         add_translates [
    434           adds_graph [
    435             rtl_st_int tmpr (zero ?) start_lbl;
    436             rtl_st_op2 Addc destr destr tmpr start_lbl;
    437             rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
     435        add_translates rtl_params1 globals [
     436          adds_graph rtl_params1 globals [
     437            sequential … (INT rtl_params_ globals tmpr (zero …));
     438            sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
     439            sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
    438440          ];
    439           translate_cst (Ointconst I8 (zero ?)) destrs
     441          translate_cst globals (Ointconst I8 (zero …)) destrs
    440442        ] start_lbl
    441443      | cons srcr1 srcrs1 ⇒
    442444        match destrs with
    443445        [ nil ⇒
    444           add_translates [
    445             adds_graph [
    446               rtl_st_int tmpr (zero ?) start_lbl;
    447               rtl_st_op2 Addc destr destr tmpr start_lbl;
    448               rtl_st_op2 Addc destr2 tmpr tmpr start_lbl
     446          add_translates rtl_params1 globals [
     447            adds_graph rtl_params1 globals [
     448              sequential … (INT rtl_params_ globals tmpr (zero …));
     449              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr);
     450              sequential … (OP2 rtl_params_ globals Addc destr2 tmpr tmpr)
    449451            ];
    450             translate_cst (Ointconst I8 (zero ?)) destrs
     452            translate_cst globals (Ointconst I8 (zero ?)) destrs
    451453          ] start_lbl
    452454        | cons destr2 destrs ⇒
    453           add_translates [
    454             adds_graph [
    455               rtl_st_opaccs Mul tmpr destr2 srcr2 srcr1 start_lbl;
    456               rtl_st_op2 Addc destr destr tmpr start_lbl
     455          add_translates rtl_params1 globals [
     456            adds_graph rtl_params1 globals [
     457              sequential … (OPACCS rtl_params_ globals Mul tmpr destr2 srcr2 srcr1);
     458              sequential … (OP2 rtl_params_ globals Addc destr destr tmpr)
    457459            ];
    458             translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2
     460            translate_mul1 globals dummy tmpr (destr2 :: destrs) srcrs1 srcr2
    459461          ] start_lbl
    460462        ]
     
    464466
    465467definition translate_muli ≝
     468  λglobals: list ident.
    466469  λdummy: register.
    467470  λtmpr: register.
     
    474477  λtranslates: list ?.
    475478  λsrcr2i: register.
    476   let 〈tmp_destrs1, tmp_destrs2〉 ≝ split ? tmp_destrs i i_prf in
     479  let 〈tmp_destrs1, tmp_destrs2〉 ≝ split tmp_destrs i i_prf in
    477480  let tmp_destrs2' ≝
    478481    match tmp_destrs2 with
    479482    [ nil ⇒ [ ]
    480483    | cons tmp_destr2 tmp_destrs2 ⇒ [
    481         adds_graph [
    482           rtl_st_clear_carry dummy_lbl;
    483           rtl_st_int tmp_destr2 (zero ?) dummy_lbl
     484        adds_graph rtl_params1 globals [
     485          sequential rtl_params_ globals (CLEAR_CARRY …);
     486          sequential … (INT rtl_params_ globals tmp_destr2 (zero …))
    484487        ];
    485         translate_mul1 dummy tmpr tmp_destrs2 srcrs1 srcr2i;
    486         translate_cst (Ointconst I8 (zero ?)) tmp_destrs1;
    487         adds_graph [
    488           rtl_st_clear_carry dummy_lbl
     488        translate_mul1 globals dummy tmpr tmp_destrs2 srcrs1 srcr2i;
     489        translate_cst globals (Ointconst I8 (zero …)) tmp_destrs1;
     490        adds_graph rtl_params1 globals [
     491          sequential rtl_params_ globals (CLEAR_CARRY …)
    489492        ];
    490         translate_op Addc destrs destrs tmp_destrs
     493        translate_op globals Addc destrs destrs tmp_destrs
    491494      ]
    492495    ]
     
    495498
    496499axiom translate_mul:
     500  ∀globals: list ident.
    497501  ∀destrs: list register.
    498502  ∀srcrs1: list register.
     
    500504  ∀start_lbl: label.
    501505  ∀dest_lbl: label.
    502   ∀def: rtl_internal_function.
    503     rtl_internal_function.
     506  ∀def: rtl_internal_function globals.
     507    rtl_internal_function globals.
    504508
    505509(*
Note: See TracChangeset for help on using the changeset viewer.