Changeset 1045 for src/RTLabs

Timestamp:

Jun 29, 2011, 10:47:39 AM (10 years ago)

Author:

mulligan

Message:

resolved conflict in rtlabs

Location:

src/RTLabs

Files:

• RTLAbstoRTL.ma (modified) (3 diffs)
• syntax.ma (modified) (1 diff)

src/RTLabs/RTLAbstoRTL.ma

@@ -27 +27 @@
     match fresh LabelTag (rtl_if_luniverse def) with
     [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
-    | Error ⇒ None ?
+    | Error _ ⇒ None ?
     ].
 
@@ -917 +917 @@
   ].
 
+axiom translate_op2:
+  op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function.
+
 definition translate_cond2 ≝
   λop2.
@@ -926 +929 @@
   λdef.
   match op2 with
+  [ op_cmp cmp ⇒
+    match cmp with
+    [ Compare_Equal ⇒
+      let srcr1 ≝ extract_singleton ? srcrs1 in
+      match srcr1 with
+      [ None ⇒ None ?
+      | Some srcr1 ⇒
+        let srcr2 ≝ extract_singleton ? srcrs2 in
+        match srcr2 with
+        [ None ⇒ None ?
+        | Some srcr2 ⇒
+          let 〈def, tmpr〉 ≝ fresh_reg def in
+          adds_graph [
+            rtl_st_clear_carry start_lbl;
+            rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl;
+            rtl_st_cond_acc tmpr lbl_false lbl_true
+          ] start_lbl start_lbl def
+        ]
+      ]
+    | _ ⇒
+      let n ≝ length ? srcrs1 + length ? srcrs2 in
+      match size_of_op2_ret n op2 with
+      [ None ⇒ None ?
+      | Some size ⇒
+        let 〈def, destrs〉 ≝ fresh_regs def size in
+        let lbl ≝ fresh_label def in
+        match lbl with
+        [ None ⇒ None ?
+        | Some lbl ⇒
+          match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
+          [ None ⇒ None ?
+          | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
+          ]
+        ]
+      ]
+    ]
+  | _ ⇒
+    let n ≝ length ? srcrs1 + length ? srcrs2 in
+    match size_of_op2_ret n op2 with
+    [ None ⇒ None ?
+    | Some size ⇒
+      let 〈def, destrs〉 ≝ fresh_regs def size in
+      let lbl ≝ fresh_label def in
+      match lbl with
+      [ None ⇒ None ?
+      | Some lbl ⇒
+        match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with
+        [ None ⇒ None ?
+        | Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def
+        ]
+      ]
+    ]
+  ].
+
+let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?)
+                           (destr2: ?) (start_lbl: label)
+                           (dest_lbl: label) (def: rtl_internal_function) ≝
+  let destrs ≝ [ destr1; destr2 ] in
+  match mode with
+  [ Aindexed off ⇒
+    let srcr12 ≝ extract_singleton ? args in
+    match srcr12 with
+    [ None ⇒ None ?
+    | Some srcr12 ⇒
+      let srcr12 ≝ extract_pair ? srcr12 in
+      match srcr12 with
+      [ None ⇒ None ?
+      | Some srcr12 ⇒
+        let 〈srcr1, srcr2〉 ≝ srcr12 in
+        let 〈def, tmpr〉 ≝ fresh_reg def in
+        add_translates [
+          adds_graph [
+            rtl_st_int tmpr off start_lbl
+          ];
+          translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr]
+        ] start_lbl dest_lbl def
+      ]
+    ]
+  | Aindexed2 ⇒
+    let args_pair ≝ extract_pair ? args in
+    match args_pair with
+    [ None ⇒ None ?
+    | Some args_pair ⇒
+      let 〈lft, rgt〉 ≝ args_pair in
+      let srcr1112 ≝ extract_pair ? lft in
+      let srcr2 ≝ extract_singleton ? rgt in
+      match srcr1112 with
+      [ None ⇒
+        let srcr2 ≝ extract_singleton ? rgt in
+        let srcr1112 ≝ extract_pair ? lft in
+        match srcr2 with
+        [ None ⇒ None ?
+        | Some srcr2 ⇒
+          match srcr1112 with
+          [ None ⇒ None ?
+          | Some srcr1112 ⇒
+            let 〈srcr11, srcr12〉 ≝ srcr1112 in
+            translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
+          ]
+        ]
+      | Some srcr1112 ⇒
+        let 〈srcr11, srcr12〉 ≝ srcr1112 in
+        match srcr2 with
+        [ None ⇒ None ?
+        | Some srcr2 ⇒
+          translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def
+        ]
+      ]
+    ]
+  | Aglobal x off ⇒ 
+    let 〈def, tmpr〉 ≝ fresh_reg def in
+    add_translates [
+      adds_graph [
+        rtl_st_int tmpr off start_lbl;
+        rtl_st_addr destr1 destr2 x start_lbl
+      ];
+      translate_op2 op_addp destrs destrs [ tmpr ]
+    ] start_lbl dest_lbl def
+  | Abased x off ⇒
+    let srcrs ≝ extract_singleton ? args in
+    match srcrs with
+    [ None ⇒ None ?
+    | Some srcrs ⇒
+      let 〈def, tmpr1〉 ≝ fresh_reg def in
+      let 〈def, tmpr2〉 ≝ fresh_reg def in
+      (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *)
+      (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *)
+      let address_unfold ≝
+        let 〈def, tmpr〉 ≝ fresh_reg def in
+          add_translates [
+            adds_graph [
+              rtl_st_int tmpr off start_lbl;
+              rtl_st_addr tmpr1 tmpr2 x start_lbl
+           ];
+            translate_op2 op_addp destrs destrs [ tmpr ]
+         ]
+      in
+      add_translates [
+        address_unfold;
+        translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs
+      ] start_lbl dest_lbl def
+    ]
+  | Ainstack off ⇒
+    let 〈def, tmpr〉 ≝ fresh_reg def in
+    add_translates [
+      adds_graph [
+        rtl_st_int tmpr off start_lbl;
+        rtl_st_stack_addr destr1 destr2 start_lbl
+      ];
+      translate_op2 op_addp destrs destrs [ tmpr ]
+    ] start_lbl dest_lbl def
+  | _ ⇒ None ? (* wrong number of arguments *)
+  ].
+
+definition translate_load ≝
+  λq.
+  λmode.
+  λargs.
+  λdestrs.
+  λstart_lbl: label.
+  λdest_lbl: label.
+  λdef.
+  match q with
   [
-  ]
-
-let translate_cond2 op2 srcrs1 srcrs2 start_lbl lbl_true lbl_false def =
-  match op2, srcrs1, srcrs2 with
-
-    | AST.Op_cmp AST.Cmp_eq, [srcr1], [srcr2] ->
+  ].
+
+let translate_load q mode args destrs start_lbl dest_lbl def =
+  match q, destrs with
+
+    | Memory.QInt 1, [destr] ->
+      let (def, addr1) = fresh_reg def in
+      let (def, addr2) = fresh_reg def in
+      add_translates
+        [addressing_pointer mode args addr1 addr2 ;
+         adds_graph [RTL.St_load (destr, addr1, addr2, start_lbl)]]
+        start_lbl dest_lbl def
+
+    | Memory.QPtr, [destr1 ; destr2] ->
+      let (def, addr1) = fresh_reg def in
+      let (def, addr2) = fresh_reg def in
+      let addr = [addr1 ; addr2] in
       let (def, tmpr) = fresh_reg def in
-      adds_graph
-        [RTL.St_clear_carry start_lbl ;
-         RTL.St_op2 (I8051.Sub, tmpr, srcr1, srcr2, start_lbl) ;
-         RTL.St_condacc (tmpr, lbl_false, lbl_true)]
-        start_lbl start_lbl def
-
-    | _, _, _ ->
-      let n = (List.length srcrs1) + (List.length srcrs2) in
-      let (def, destrs) = fresh_regs def (size_of_op2_ret n op2) in
-      let lbl = fresh_label def in
-      let def = translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def in
-      translate_cond1 AST.Op_id destrs lbl lbl_true lbl_false def
+      add_translates
+        [addressing_pointer mode args addr1 addr2 ;
+         adds_graph [RTL.St_load (destr1, addr1, addr2, start_lbl) ;
+                     RTL.St_int (tmpr, 1, start_lbl)] ;
+         translate_op2 AST.Op_addp addr addr [tmpr] ;
+         adds_graph [RTL.St_load (destr2, addr1, addr2, start_lbl)]]
+        start_lbl dest_lbl def
+
+    | _ -> error "Size error in load."

src/RTLabs/syntax.ma

@@ -10 +10 @@
 include "common/Graphs.ma".
 
-(* Statements, including the label of successor(s). *)
+definition immediate : Type[0] ≝ Byte.
+
+(* Addressing modes *)
+
+inductive addressing : Type[0] ≝
+(* dpm: changed from int to Byte *)
+| Aindexed  : immediate → addressing         (* r1 + offset *)
+| Aindexed2 : addressing                     (* r1 + r2 *)
+| Aglobal   : ident → immediate → addressing (* global + offset *)
+| Abased    : ident → immediate → addressing (* global + offset + r1 *)
+| Ainstack  : immediate → addressing         (* stack + offset *)
+.
+
+definition addr_mode_args : addressing → nat ≝
+λa. match a with
+[ Aindexed _  ⇒ 1
+| Aindexed2   ⇒ 2
+| Aglobal _ _ ⇒ 0
+| Abased _ _  ⇒ 1
+| Ainstack _  ⇒ 0
+].
+
+definition addr ≝ λm.Vector register (addr_mode_args m).
 
 inductive statement : Type[0] ≝