Changeset 799 for src

Timestamp:

May 13, 2011, 5:35:04 PM (10 years ago)

Author:

mulligan

Message:

more changes.

File:

• src/RTLabs/RTLAbstoRTL.ma (modified) (3 diffs)

src/RTLabs/RTLAbstoRTL.ma

@@ -417 +417 @@
     ] start_lbl start_lbl def.
 
+(*
 let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?)
                       (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝
@@ -693 +694 @@
     | Compare_NotEqual ⇒
       translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
+    | Compare
     | _ ⇒ None ?
     ]
   | _ ⇒ ?
   ].
-
-    | AST.Op_cmp AST.Cmp_ne, _, _, _
-    | AST.Op_cmpu AST.Cmp_ne, _, _, _ ->
-      translate_op2 AST.Op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def
 
     | AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] ->
@@ -776 +774 @@
 
     | _ -> assert false (* wrong number of arguments *)
+*)
+
+definition translate_condcst ≝
+  λcst.
+  λstart_lbl: label.
+  λlbl_true: label.
+  λlbl_false: label.
+  λdef.
+  match cst with
+  [ cast_int i ⇒
+    let 〈def, tmpr〉 ≝ fresh_reg def in
+    adds_graph [
+      rtl_st_int tmpr i start_lbl;
+      rtl_st_cond_acc tmpr lbl_true lbl_false
+    ] start_lbl start_lbl def
+  | cast_addr_symbol x ⇒
+    let 〈def, r1〉 ≝ fresh_reg def in
+    let 〈def, r2〉 ≝ fresh_reg def in
+    let lbl ≝ fresh_label def in
+    match lbl with
+    [ None ⇒ None ?
+    | Some lbl ⇒
+      let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in
+        translate_condptr r1 r2 lbl lbl_true lbl_false def
+    ]
+  | cast_stack_offset off ⇒
+    let 〈def, r1〉 ≝ fresh_reg def in
+    let 〈def, r2〉 ≝ fresh_reg def in
+    let tmp_lbl ≝ fresh_label def in
+    match tmp_lbl with
+    [ None ⇒ None ?
+    | Some tmp_lbl ⇒
+      let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in
+      match def with
+      [ None ⇒ None ?
+      | Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def
+      ]
+    ]
+  | cast_float f ⇒ None ? (* error_float *)
+  ].
+
+definition size_of_op1_ret ≝
+  λop.
+  match op with
+  [ op_cast8_unsigned ⇒ Some ? 1
+  | op_cast8_signed ⇒ Some ? 1
+  | op_cast16_unsigned ⇒ Some ? 1
+  | op_cast16_signed ⇒ Some ? 1
+  | op_neg_int ⇒ Some ? 1
+  | op_not_int ⇒ Some ? 1
+  | op_int_of_ptr ⇒ Some ? 1
+  | op_ptr_of_int ⇒ Some ? 2
+  | op_id ⇒ None ? (* invalid_argument *)
+  | _ ⇒ None ? (* error_float *)
+  ].
+
+definition translate_cond1 ≝
+  λop1.
+  λsrcrs: list register.
+  λstart_lbl: label.
+  λlbl_true: label.
+  λlbl_false: label.
+  λdef.
+  match op1 with
+  [ op_id ⇒
+    let srcr ≝ extract_singleton ? srcrs in
+    match srcr with
+    [ None ⇒
+      let srcr12 ≝ extract_pair ? srcrs in
+      match srcr12 with
+      [ None ⇒ None ?
+      | Some srcr12 ⇒
+        let 〈srcr1, srcr2〉 ≝ srcr12 in
+          translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def
+      ]
+    | Some srcr ⇒
+      adds_graph [
+        rtl_st_cond_acc srcr lbl_true lbl_false
+      ] start_lbl start_lbl def
+    ]
+  | _     ⇒
+    let size ≝ size_of_op1_ret op1 in
+    match size 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 ⇒
+        let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in
+        match def with
+        [ None ⇒ None ?
+        | Some def ⇒
+          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
+                translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def
+            ]
+          | Some destr ⇒
+            adds_graph [
+              rtl_st_cond_acc destr lbl_true lbl_false
+            ] start_lbl start_lbl def
+          ]
+        ]
+      ]
+    ]
+  ].
+
+definition size_of_op2_ret ≝
+  λn: nat.
+  λop2.
+  match op2 with
+  [ op_add ⇒ Some ? 1
+  | op_sub ⇒ Some ? 1
+  | op_mul ⇒ Some ? 1
+  | op_div ⇒ Some ? 1
+  | op_divu ⇒ Some ? 1
+  | op_mod ⇒ Some ? 1
+  | op_modu ⇒ Some ? 1
+  | op_and ⇒ Some ? 1
+  | op_or ⇒ Some ? 1
+  | op_xor ⇒ Some ? 1
+  | op_shl ⇒ Some ? 1
+  | op_shr ⇒ Some ? 1
+  | op_shru ⇒ Some ? 1
+  | op_cmp _ ⇒ Some ? 1
+  | op_cmpu _ ⇒ Some ? 1
+  | op_cmpp _ ⇒ Some ? 1
+  | op_addp ⇒ Some ? 2
+  | op_subp ⇒
+    if eq_nat n 4 then
+      Some ? 1
+    else
+      Some ? 2
+  | _ ⇒ None ? (* error_float *)
+  ].
+
+definition translate_cond2 ≝
+  λop2.
+  λsrcrs1: list register.
+  λsrcrs2: list register.
+  λstart_lbl: label.
+  λlbl_true: label.
+  λlbl_false: label.
+  λdef.
+  match op2 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 (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