Changeset 795


Ignore:
Timestamp:
May 13, 2011, 12:29:06 PM (9 years ago)
Author:
mulligan
Message:

Changes from this morning.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r793 r795  
    177177  ].
    178178 
     179(* dpm: had to lift this into option *)
    179180let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
    180181                       (def: ?) on translate_list ≝
     
    183184  | cons hd tl ⇒
    184185    match tl with
    185     [ nil ⇒ Some ? (hd start_lbl dest_lbl def)
     186    [ nil ⇒ hd start_lbl dest_lbl def
    186187    | cons hd' tl' ⇒
    187188      let tmp_lbl ≝ fresh_label def in
     
    189190      [ None ⇒ None ?
    190191      | Some tmp_lbl ⇒
    191         let def ≝ hd start_lbl tmp_lbl def in
    192           add_translates tl tmp_lbl dest_lbl def
     192        match hd start_lbl tmp_lbl def with
     193        [ None ⇒ None ?
     194        | Some def ⇒ add_translates tl tmp_lbl dest_lbl def
     195        ]
    193196      ]
    194197    ]
     
    580583  | op_divf ⇒ None ?
    581584  | op_cmpf _ ⇒ None ?
    582   | op_addp ⇒ ?
     585  | op_addp ⇒
     586    let destr12 ≝ extract_pair ? destrs in
     587    match destr12 with
     588    [ None         ⇒ None ?
     589    | Some destr12 ⇒
     590      let 〈destr1, destr2〉 ≝ destr12 in
     591      let srcr12 ≝ extract_pair ? srcrs1 in
     592      match srcr12 with
     593      [ None ⇒
     594        let srcr2 ≝ extract_singleton ? srcrs1 in
     595        match srcr2 with
     596        [ None ⇒ None ?
     597        | Some srcr2 ⇒
     598          let srcr12 ≝ extract_pair ? srcrs2 in
     599          match srcr12 with
     600          [ None ⇒ None ?
     601          | Some srcr12 ⇒
     602            let 〈srcr11, srcr12〉 ≝ srcr12 in
     603            let 〈def, tmpr1〉 ≝ fresh_reg def in
     604            let 〈def, tmpr2〉 ≝ fresh_reg def in
     605              adds_graph [
     606                rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
     607                rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
     608                rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
     609                rtl_st_move destr1 tmpr1 start_lbl
     610              ] start_lbl dest_lbl def
     611          ]
     612        ]
     613      | Some srcr12 ⇒
     614        let 〈srcr11, srcr12〉 ≝ srcr12 in
     615        let srcr2 ≝ extract_singleton ? srcrs2 in
     616        match srcr2 with
     617        [ None       ⇒ None ?
     618        | Some srcr2 ⇒
     619          let 〈def, tmpr1〉 ≝ fresh_reg def in
     620          let 〈def, tmpr2〉 ≝ fresh_reg def in
     621            adds_graph [
     622              rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
     623              rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
     624              rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
     625              rtl_st_move destr1 tmpr1 start_lbl
     626            ] start_lbl dest_lbl def
     627        ]
     628      ]
     629    ]
     630  | op_subp ⇒
     631    let destr ≝ extract_singleton ? destrs in
     632    match destr with
     633    [ None ⇒
     634      let destr12 ≝ extract_pair ? destrs in
     635      match destr12 with
     636      [ None ⇒ None ?
     637      | Some destr12 ⇒
     638        let 〈destr1, destr2〉 ≝ destr12 in
     639        let srcr12 ≝ extract_pair ? srcrs1 in
     640        match srcr12 with
     641        [ None ⇒ None ?
     642        | Some srcr12 ⇒
     643          let 〈srcr11, srcr12〉 ≝ srcr12 in
     644          let srcr2 ≝ extract_singleton ? srcrs2 in
     645          match srcr2 with
     646          [ None ⇒ None ?
     647          | Some srcr2 ⇒
     648            adds_graph [
     649              rtl_st_clear_carry start_lbl;
     650              rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl;
     651              rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl;
     652              rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl
     653            ] start_lbl dest_lbl def
     654          ]
     655        ]
     656      ]
     657    | Some destr ⇒
     658      match srcrs1 with
     659      [ nil ⇒ None ?
     660      | cons srcr1 tl ⇒
     661        match srcrs2 with
     662        [ nil ⇒ None ?
     663        | cons srcr2 tl' ⇒
     664          let 〈def, tmpr1〉 ≝ fresh_reg def in
     665          let 〈def, tmpr2〉 ≝ fresh_reg def in
     666            adds_graph [
     667              rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl;
     668              rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl;
     669              rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl;
     670              rtl_st_op2 Add destr srcr1 tmpr1 start_lbl
     671            ] start_lbl dest_lbl def
     672        ]
     673      ]
     674    ]
     675  | op_cmp cmp ⇒
     676    match cmp with
     677    [ Compare_Equal ⇒
     678      add_translates [
     679        translate_op2 op_sub destrs srcrs1 srcrs2;
     680        translate_op1 op_not_bool destrs destrs
     681      ] start_lbl dest_lbl def
     682    | Compare_NotEqual ⇒
     683      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     684    | _ ⇒ None ?
     685    ]
     686  | op_cmpu cmp ⇒
     687    match cmp with
     688    [ Compare_Equal ⇒
     689      add_translates [
     690        translate_op2 op_sub destrs srcrs1 srcrs2;
     691        translate_op1 op_not_bool destrs destrs
     692      ] start_lbl dest_lbl def
     693    | Compare_NotEqual ⇒
     694      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
     695    | _ ⇒ None ?
     696    ]
    583697  | _ ⇒ ?
    584698  ].
    585 
    586     | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2]
    587     | AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] ->
    588       let (def, tmpr1) = fresh_reg def in
    589       let (def, tmpr2) = fresh_reg def in
    590       adds_graph
    591         [RTL.St_op2 (I8051.Add, tmpr1, srcr11, srcr2, start_lbl) ;
    592          RTL.St_int (tmpr2, 0, start_lbl) ;
    593          RTL.St_op2 (I8051.Addc, destr2, tmpr2, srcr12, start_lbl) ;
    594          RTL.St_move (destr1, tmpr1, start_lbl)]
    595         start_lbl dest_lbl def
    596 
    597     | AST.Op_subp, [destr], [srcr1 ; _], [srcr2 ; _] ->
    598       let (def, tmpr1) = fresh_reg def in
    599       let (def, tmpr2) = fresh_reg def in
    600       adds_graph
    601         [RTL.St_op1 (I8051.Cmpl, tmpr1, srcr2, start_lbl) ;
    602          RTL.St_int (tmpr2, 1, start_lbl) ;
    603          RTL.St_op2 (I8051.Add, tmpr1, tmpr1, tmpr2, start_lbl) ;
    604          RTL.St_op2 (I8051.Add, destr, srcr1, tmpr1, start_lbl)]
    605         start_lbl dest_lbl def
    606 
    607     | AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
    608       adds_graph
    609         [RTL.St_clear_carry start_lbl ;
    610          RTL.St_op2 (I8051.Sub, destr1, srcr11, srcr2, start_lbl) ;
    611          RTL.St_int (destr2, 0, start_lbl) ;
    612          RTL.St_op2 (I8051.Sub, destr2, srcr12, destr2, start_lbl)]
    613         start_lbl dest_lbl def
    614 
    615     | AST.Op_cmp AST.Cmp_eq, _, _, _
    616     | AST.Op_cmpu AST.Cmp_eq, _, _, _ ->
    617       add_translates
    618         [translate_op2 AST.Op_sub destrs srcrs1 srcrs2 ;
    619          translate_op1 AST.Op_notbool destrs destrs]
    620         start_lbl dest_lbl def
    621699
    622700    | AST.Op_cmp AST.Cmp_ne, _, _, _
  • src/common/AST.ma

    r793 r795  
    517517inductive Compare: Type[0] ≝
    518518  Compare_Equal: Compare
     519| Compare_NotEqual: Compare
    519520| Compare_Less: Compare
    520521| Compare_Greater: Compare
Note: See TracChangeset for help on using the changeset viewer.