Changeset 795 for src

Timestamp:

May 13, 2011, 12:29:06 PM (10 years ago)

Author:

mulligan

Message:

Changes from this morning.

Location:

src

Files:

• RTLabs/RTLAbstoRTL.ma (modified) (4 diffs)
• common/AST.ma (modified) (1 diff)

src/RTLabs/RTLAbstoRTL.ma

@@ -177 +177 @@
   ].
   
+(* dpm: had to lift this into option *)
 let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
                        (def: ?) on translate_list ≝
@@ -183 +184 @@
   | cons hd tl ⇒
     match tl with
-    [ nil ⇒ Some ? (hd start_lbl dest_lbl def)
+    [ nil ⇒ hd start_lbl dest_lbl def
     | cons hd' tl' ⇒
       let tmp_lbl ≝ fresh_label def in
@@ -189 +190 @@
       [ None ⇒ None ?
       | Some tmp_lbl ⇒
-        let def ≝ hd start_lbl tmp_lbl def in
-          add_translates tl tmp_lbl dest_lbl def
+        match hd start_lbl tmp_lbl def with
+        [ None ⇒ None ?
+        | Some def ⇒ add_translates tl tmp_lbl dest_lbl def
+        ]
       ]
     ]
@@ -580 +583 @@
   | op_divf ⇒ None ?
   | op_cmpf _ ⇒ None ?
-  | op_addp ⇒ ?
+  | op_addp ⇒
+    let destr12 ≝ extract_pair ? destrs in
+    match destr12 with
+    [ None         ⇒ None ?
+    | Some destr12 ⇒
+      let 〈destr1, destr2〉 ≝ destr12 in
+      let srcr12 ≝ extract_pair ? srcrs1 in
+      match srcr12 with
+      [ None ⇒
+        let srcr2 ≝ extract_singleton ? srcrs1 in
+        match srcr2 with
+        [ None ⇒ None ?
+        | Some srcr2 ⇒
+          let srcr12 ≝ extract_pair ? srcrs2 in
+          match srcr12 with
+          [ None ⇒ None ?
+          | Some srcr12 ⇒
+            let 〈srcr11, srcr12〉 ≝ srcr12 in
+            let 〈def, tmpr1〉 ≝ fresh_reg def in
+            let 〈def, tmpr2〉 ≝ fresh_reg def in
+              adds_graph [
+                rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
+                rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
+                rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
+                rtl_st_move destr1 tmpr1 start_lbl
+              ] start_lbl dest_lbl def
+          ]
+        ]
+      | Some srcr12 ⇒
+        let 〈srcr11, srcr12〉 ≝ srcr12 in
+        let srcr2 ≝ extract_singleton ? srcrs2 in
+        match srcr2 with
+        [ None       ⇒ None ?
+        | Some srcr2 ⇒
+          let 〈def, tmpr1〉 ≝ fresh_reg def in
+          let 〈def, tmpr2〉 ≝ fresh_reg def in
+            adds_graph [
+              rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl;
+              rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl;
+              rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl;
+              rtl_st_move destr1 tmpr1 start_lbl
+            ] start_lbl dest_lbl def
+        ]
+      ]
+    ]
+  | op_subp ⇒
+    let destr ≝ extract_singleton ? destrs in
+    match destr with
+    [ None ⇒
+      let destr12 ≝ extract_pair ? destrs in
+      match destr12 with
+      [ None ⇒ None ?
+      | Some destr12 ⇒
+        let 〈destr1, destr2〉 ≝ destr12 in
+        let srcr12 ≝ extract_pair ? srcrs1 in
+        match srcr12 with
+        [ None ⇒ None ?
+        | Some srcr12 ⇒
+          let 〈srcr11, srcr12〉 ≝ srcr12 in
+          let srcr2 ≝ extract_singleton ? srcrs2 in
+          match srcr2 with
+          [ None ⇒ None ?
+          | Some srcr2 ⇒
+            adds_graph [
+              rtl_st_clear_carry start_lbl;
+              rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl;
+              rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl;
+              rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl
+            ] start_lbl dest_lbl def
+          ]
+        ] 
+      ]
+    | Some destr ⇒
+      match srcrs1 with
+      [ nil ⇒ None ?
+      | cons srcr1 tl ⇒
+        match srcrs2 with
+        [ nil ⇒ None ?
+        | cons srcr2 tl' ⇒
+          let 〈def, tmpr1〉 ≝ fresh_reg def in
+          let 〈def, tmpr2〉 ≝ fresh_reg def in
+            adds_graph [
+              rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl;
+              rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl;
+              rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl;
+              rtl_st_op2 Add destr srcr1 tmpr1 start_lbl
+            ] start_lbl dest_lbl def
+        ]
+      ]
+    ]
+  | op_cmp cmp ⇒
+    match cmp with
+    [ Compare_Equal ⇒
+      add_translates [
+        translate_op2 op_sub destrs srcrs1 srcrs2;
+        translate_op1 op_not_bool destrs destrs
+      ] start_lbl dest_lbl def
+    | Compare_NotEqual ⇒
+      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
+    | _ ⇒ None ?
+    ]
+  | op_cmpu cmp ⇒
+    match cmp with
+    [ Compare_Equal ⇒
+      add_translates [
+        translate_op2 op_sub destrs srcrs1 srcrs2;
+        translate_op1 op_not_bool destrs destrs
+      ] start_lbl dest_lbl def
+    | Compare_NotEqual ⇒
+      translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
+    | _ ⇒ None ?
+    ]
   | _ ⇒ ?
   ].
-
-    | AST.Op_addp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2]
-    | AST.Op_addp, [destr1 ; destr2], [srcr2], [srcr11 ; srcr12] ->
-      let (def, tmpr1) = fresh_reg def in
-      let (def, tmpr2) = fresh_reg def in
-      adds_graph
-        [RTL.St_op2 (I8051.Add, tmpr1, srcr11, srcr2, start_lbl) ;
-         RTL.St_int (tmpr2, 0, start_lbl) ;
-         RTL.St_op2 (I8051.Addc, destr2, tmpr2, srcr12, start_lbl) ;
-         RTL.St_move (destr1, tmpr1, start_lbl)]
-        start_lbl dest_lbl def
-
-    | AST.Op_subp, [destr], [srcr1 ; _], [srcr2 ; _] ->
-      let (def, tmpr1) = fresh_reg def in
-      let (def, tmpr2) = fresh_reg def in
-      adds_graph
-        [RTL.St_op1 (I8051.Cmpl, tmpr1, srcr2, start_lbl) ;
-         RTL.St_int (tmpr2, 1, start_lbl) ;
-         RTL.St_op2 (I8051.Add, tmpr1, tmpr1, tmpr2, start_lbl) ;
-         RTL.St_op2 (I8051.Add, destr, srcr1, tmpr1, start_lbl)]
-        start_lbl dest_lbl def
-
-    | AST.Op_subp, [destr1 ; destr2], [srcr11 ; srcr12], [srcr2] ->
-      adds_graph
-        [RTL.St_clear_carry start_lbl ;
-         RTL.St_op2 (I8051.Sub, destr1, srcr11, srcr2, start_lbl) ;
-         RTL.St_int (destr2, 0, start_lbl) ;
-         RTL.St_op2 (I8051.Sub, destr2, srcr12, destr2, start_lbl)]
-        start_lbl dest_lbl def
-
-    | AST.Op_cmp AST.Cmp_eq, _, _, _
-    | AST.Op_cmpu AST.Cmp_eq, _, _, _ ->
-      add_translates
-        [translate_op2 AST.Op_sub destrs srcrs1 srcrs2 ;
-         translate_op1 AST.Op_notbool destrs destrs]
-        start_lbl dest_lbl def
 
     | AST.Op_cmp AST.Cmp_ne, _, _, _

src/common/AST.ma

@@ -517 +517 @@
 inductive Compare: Type[0] ≝
   Compare_Equal: Compare
+| Compare_NotEqual: Compare
 | Compare_Less: Compare
 | Compare_Greater: Compare