Changeset 1568 for Deliverables

Timestamp:

Nov 25, 2011, 7:43:39 PM (8 years ago)

Author:

tranquil

Message:

• Immediates introduced (but not fully used yet in RTLabs to RTL pass)
• translation streamlined
• BUGGY: interpretation fails in LTL, trying to fetch a function with incorrect address

Location:

Deliverables/D2.2/8051/src

Files:

• ASM/ASMInterpret.ml (modified) (4 diffs)
• ASM/I8051.ml (modified) (3 diffs)
• ASM/I8051.mli (modified) (1 diff)
• ERTL/ERTL.mli (modified) (4 diffs)
• ERTL/ERTLInterpret.ml (modified) (4 diffs)
• ERTL/ERTLPrinter.ml (modified) (4 diffs)
• ERTL/ERTLToLTLI.ml (modified) (9 diffs)
• ERTL/build.ml (modified) (2 diffs)
• ERTL/liveness.ml (modified) (6 diffs)
• ERTL/uses.ml (modified) (2 diffs)
• LIN/LIN.mli (modified) (2 diffs)
• LIN/LINInterpret.ml (modified) (2 diffs)
• LIN/LINPrinter.ml (modified) (2 diffs)
• LIN/LINToASM.ml (modified) (2 diffs)
• LTL/LTL.mli (modified) (2 diffs)
• LTL/LTLInterpret.ml (modified) (2 diffs)
• LTL/LTLPrinter.ml (modified) (2 diffs)
• RTL/RTL.mli (modified) (4 diffs)
• RTL/RTLInterpret.ml (modified) (3 diffs)
• RTL/RTLPrinter.ml (modified) (3 diffs)
• RTL/RTLToERTL.ml (modified) (7 diffs)
• RTLabs/RTLabs.mli (modified) (1 diff)
• RTLabs/RTLabsPrinter.ml (modified) (3 diffs)
• RTLabs/RTLabsToRTL.ml (modified) (16 diffs)
• common/intValue.ml (modified) (2 diffs)
• common/intValue.mli (modified) (1 diff)
• common/memory.ml (modified) (1 diff)
• common/value.ml (modified) (2 diffs)
• common/value.mli (modified) (1 diff)

Deliverables/D2.2/8051/src/ASM/ASMInterpret.ml

@@ -1007 +1007 @@
             memory, we must increment by 5, as we added two new instructions. *)
         let to_ljmp = `REL (vect_of_int 2 `Eight) in
-        let offset = 5 in
+        (* let offset = 5 in *)
          let jmp_address, translated_jump =
            match i with
@@ -1452 +1452 @@
 ;;
 
+let unopt = function Some x -> x | None -> invalid_arg "None"
+
 let serial_port_input status in_cont =
       (* Serial port input *)
@@ -1495 +1497 @@
                            serial_v_in       = Some (`Eight b) }
                      else
-                           (* Warning about incomplete case analysis here, but safe as we've already tested for
-                              None. *)
-                       let Some e = status.serial_epsilon_in in
-                       let Some v = status.serial_v_in in
+                       (* safe as we've already tested for None. *)
+                       let e = unopt status.serial_epsilon_in in
+                       let v = unopt status.serial_v_in in
                        if status.clock >= e then
                          match v with
@@ -1534 +1535 @@
                            serial_v_in       = Some (`Nine (b, b')) }
                      else
-                           (* Warning about incomplete case analysis here, but safe as we've already tested for
-                              None. *)
-                       let Some e = status.serial_epsilon_in in
-                       let Some v = status.serial_v_in in
+                       (* safe as we've already tested for None. *)
+                       let e = unopt status.serial_epsilon_in in
+                       let v = unopt status.serial_v_in in
                        if status.clock >= e then
                          match v with

Deliverables/D2.2/8051/src/ASM/I8051.ml

@@ -11 +11 @@
   | Cmpl
   | Inc
+  (* | Dec *)
+  | Rl
 
 type op2 =
@@ -27 +29 @@
   | Cmpl -> "cmpl"
   | Inc -> "inc"
+  | Rl -> "rotl"
 
 let print_op2 = function
@@ -57 +60 @@
     | Cmpl -> Val.cmpl
     | Inc -> Val.succ
+    | Rl -> Val.rotl
 
   let op2 carry op2 v1 v2 = match op2 with

Deliverables/D2.2/8051/src/ASM/I8051.mli

@@ -9 +9 @@
   | Cmpl
   | Inc
+  (* | Dec *)
+  | Rl
 
 type op2 =

Deliverables/D2.2/8051/src/ERTL/ERTL.mli

@@ -38 +38 @@
 type registers = Register.t list
 
+type argument = RTL.argument
+
 type statement =
 
@@ -63 +65 @@
      are the destination hardware register, the source pseudo register, and the
      label of the next statement. *)
-  | St_set_hdw of I8051.register * Register.t * Label.t
+  | St_set_hdw of I8051.register * argument * Label.t
 
   (* Assign the content of a hardware register to a hardware
@@ -101 +103 @@
   | St_addrL of Register.t * AST.ident * Label.t
 
-  (* Assign an integer constant to a register. Parameters are the destination
-     register, the integer and the label of the next statement. *)
-  | St_int of Register.t * int * Label.t
+  (* (\* Assign an integer constant to a register. Parameters are the destination *)
+  (*    register, the integer and the label of the next statement. *\) *)
+  (* | St_int of Register.t * int * Label.t *)
 
   (* Move the content of a register to another. Parameters are the destination
      register, the source register, and the label of the next statement. *)
-  | St_move of Register.t * Register.t * Label.t
+  | St_move of Register.t * argument * Label.t
 
   (* Apply a binary operation that will later be translated in an operation on
@@ -127 +129 @@
   (* Apply a binary operation. Parameters are the operation, the destination
      register, the source registers, and the label of the next statement. *)
-  | St_op2 of I8051.op2 * Register.t * Register.t * Register.t * Label.t
+  | St_op2 of I8051.op2 * Register.t * Register.t * argument * Label.t
 
   (* Set the carry flag to zero. Parameter is the label of the next

Deliverables/D2.2/8051/src/ERTL/ERTLInterpret.ml

@@ -158 +158 @@
     else error ("Unknown local register " ^ (Register.print r) ^ ".")
 
+let get_arg a st = match a with
+  | RTL.Imm i -> Val.of_int i
+  | RTL.Reg r -> get_reg (Psd r) st
+
 let push st v =
   let mem = Mem.store st.mem chunk st.isp v in
@@ -282 +286 @@
 
     | ERTL.St_set_hdw (destr, srcr, lbl) ->
-      let st = add_reg (Hdw destr) (get_reg (Psd srcr) st) st in
+      let st = add_reg (Hdw destr) (get_arg srcr st) st in
       next_pc st lbl
 
@@ -328 +332 @@
       next_pc st lbl
 
-    | ERTL.St_int (r, i, lbl) ->
+    | ERTL.St_move (r, RTL.Imm i, lbl) ->
       let st = add_reg (Psd r) (Val.of_int i) st in
       next_pc st lbl
 
-    | ERTL.St_move (destr, srcr, lbl) ->
+    | ERTL.St_move (destr, RTL.Reg srcr, lbl) ->
       let st = add_reg (Psd destr) (get_reg (Psd srcr) st) st in
       next_pc st lbl
@@ -361 +365 @@
         Eval.op2 st.carry op2
           (get_reg (Psd srcr1) st)
-          (get_reg (Psd srcr2) st) in
+          (get_arg srcr2 st) in
       let st = change_carry st carry in
       let st = add_reg (Psd destr) v st in

Deliverables/D2.2/8051/src/ERTL/ERTLPrinter.ml

@@ -37 +37 @@
 let print_result rl = print_reg_list "[" "]" " ; " Register.print rl
 
+let print_arg = function
+  | RTL.Imm i -> string_of_int i
+  | RTL.Reg r -> Register.print r
 
 let print_statement = function
@@ -54 +57 @@
   | ERTL.St_set_hdw (r1, r2, lbl) ->
     Printf.sprintf "move %s, %s --> %s"
-      (I8051.print_register r1) (Register.print r2) lbl
+      (I8051.print_register r1) (print_arg r2) lbl
   | ERTL.St_hdw_to_hdw (r1, r2, lbl) ->
     Printf.sprintf "move %s, %s --> %s"
@@ -72 +75 @@
   | ERTL.St_addrL (dstr, id, lbl) ->
     Printf.sprintf "addrL %s, %s --> %s" (Register.print dstr) id lbl
-  | ERTL.St_int (dstr, i, lbl) ->
-    Printf.sprintf "imm %s, %d --> %s" (Register.print dstr) i lbl
+  (* | ERTL.St_int (dstr, i, lbl) -> *)
+  (*   Printf.sprintf "imm %s, %d --> %s" (Register.print dstr) i lbl *)
   | ERTL.St_move (dstr, srcr, lbl) ->
     Printf.sprintf "move %s, %s --> %s"
-      (Register.print dstr) (Register.print srcr) lbl
+      (Register.print dstr) (print_arg srcr) lbl
   | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl) ->
     Printf.sprintf "%sA %s, %s, %s --> %s"
@@ -102 +105 @@
       (Register.print dstr)
       (Register.print srcr1)
-      (Register.print srcr2)
+      (print_arg srcr2)
       lbl
   | ERTL.St_clear_carry lbl ->

Deliverables/D2.2/8051/src/ERTL/ERTLToLTLI.ml

@@ -40 +40 @@
     let l = generate (LTL.St_load l) in
     let l = generate (LTL.St_from_acc (I8051.dph, l)) in
-    let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
+    let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
     let l = generate (LTL.St_int (I8051.a, 0, l)) in
     let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
-    let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
+    let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in
     LTL.St_int (I8051.a, off, l)
 
+  let set_stack_preamble off l =
+    let off = adjust off in
+    let l = generate (LTL.St_from_acc (I8051.dph, l)) in
+    let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
+    let l = generate (LTL.St_int (I8051.a, 0, l)) in
+    let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
+    let l = generate (LTL.St_op2 (I8051.Add, LTL.Reg I8051.spl, l)) in
+    LTL.St_int (I8051.a, off, l)
+
   let set_stack off r l =
-    let off = adjust off in
     let l = generate (LTL.St_store l) in
     let l = generate (LTL.St_to_acc (r, l)) in
-    let l = generate (LTL.St_from_acc (I8051.dph, l)) in
-    let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
-    let l = generate (LTL.St_int (I8051.a, 0, l)) in
-    let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
-    let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
-    LTL.St_int (I8051.a, off, l)
-
-
-  let write (r : Register.t) (l : Label.t) : (I8051.register * Label.t) =
-    match lookup r with
-
-      | Color hwr ->
-        (* Pseudo-register [r] has been mapped to hardware register
-           [hwr]. Just write into [hwr] and branch to [l]. *)
-        (hwr, l)
-
-      | Spill off ->
-        (* Pseudo-register [r] has been mapped to offset [off] in the local zone
-           of the stack. Then, write into [sst] (never allocated) and transfer
-           control to an instruction that copies [sst] in the designated
-           location of the stack before branching to [l]. *)
-        (I8051.sst, generate (set_stack off I8051.sst l))
-
-
-  let read (r : Register.t) (stmt : I8051.register -> LTL.statement) =
-    match lookup r with
-      | Color hwr ->
-        (* Pseudo-register [r] has been mapped to hardware register [hwr]. Just
-           generate statement [stmt] with a reference to register [hwr]. *)
-        generate (stmt hwr)
-
-      | Spill off ->
-        (* Pseudo-register [r] has been mapped to offset [off] in the local zone
-           of the stack. Issue a statement that copies the designated area in
-           the stack into the temporary unallocatable hardware register [sst],
-           then generate statement [stmt] with a reference to register
-           [sst]. *)
-        let temphwr = I8051.sst in
-        let l = generate (stmt temphwr) in
-        generate (get_stack temphwr off l)
+    set_stack_preamble off l
+
+  let set_stack_int off k l =
+    let l = generate (LTL.St_store l) in
+    let l = generate (LTL.St_int (I8051.a, k, l)) in
+    set_stack_preamble off l
+
+  (* let write (r : Register.t) (l : Label.t) : (I8051.register * Label.t) = *)
+  (*   match lookup r with *)
+
+  (*     | Color hwr -> *)
+  (*       (\* Pseudo-register [r] has been mapped to hardware register *)
+  (*          [hwr]. Just write into [hwr] and branch to [l]. *\) *)
+  (*       (hwr, l) *)
+
+  (*     | Spill off -> *)
+  (*       (\* Pseudo-register [r] has been mapped to offset [off] in the local zone *)
+  (*          of the stack. Then, write into [sst] (never allocated) and transfer *)
+  (*          control to an instruction that copies [sst] in the designated *)
+  (*          location of the stack before branching to [l]. *\) *)
+  (*       (I8051.sst, generate (set_stack off I8051.sst l)) *)
+
+
+  (* let read (r : Register.t) (stmt : I8051.register -> LTL.statement) = *)
+  (*   match lookup r with *)
+  (*     | Color hwr -> *)
+  (*       (\* Pseudo-register [r] has been mapped to hardware register [hwr]. Just *)
+  (*          generate statement [stmt] with a reference to register [hwr]. *\) *)
+  (*       generate (stmt hwr) *)
+
+  (*     | Spill off -> *)
+  (*       (\* Pseudo-register [r] has been mapped to offset [off] in the local zone *)
+  (*          of the stack. Issue a statement that copies the designated area in *)
+  (*          the stack into the temporary unallocatable hardware register [sst], *)
+  (*          then generate statement [stmt] with a reference to register *)
+  (*          [sst]. *\) *)
+  (*       let temphwr = I8051.sst in *)
+  (*       let l = generate (stmt temphwr) in *)
+  (*       generate (get_stack temphwr off l) *)
 
 
@@ -100 +107 @@
       | Color desthwr, Color sourcehwr when I8051.eq_reg desthwr sourcehwr ->
         LTL.St_skip l
+      | Color desthwr, Color sourcehwr when I8051.eq_reg desthwr I8051.a ->
+        LTL.St_to_acc (sourcehwr, l)
+      | Color desthwr, Color sourcehwr when I8051.eq_reg sourcehwr I8051.a ->
+        LTL.St_from_acc (desthwr, l)
       | Color desthwr, Color sourcehwr ->
         let l = generate (LTL.St_from_acc (desthwr, l)) in
@@ -119 +130 @@
         get_stack temphwr off2 l
 
+  let move_int (dest : decision) (k : int) l =
+    match dest with
+      | Color desthwr -> LTL.St_int (desthwr, k, l)
+      | Spill off -> set_stack_int off k l
+
+  let op2 op (dest : decision) (src1 : decision) (src2 : decision) l =
+    let l = generate (move dest (Color I8051.a) l) in
+    match op, src1, src2 with
+      | _, _, Color src2hwr ->
+        let l = generate (LTL.St_op2 (op, LTL.Reg src2hwr, l)) in
+        move (Color I8051.a) src1 l
+        (* if op is commutative, we can do as above if first is hwr *)
+      | (Add | Addc | And | Or | Xor), Color src1hwr, _ ->
+        let l = generate (LTL.St_op2 (op, LTL.Reg src1hwr, l)) in
+        move (Color I8051.a) src2 l
+        (* otherwise we have to use b *)
+      | _ ->
+        let l = generate (LTL.St_op2 (op, LTL.Reg I8051.b, l)) in
+        let l = generate (move (Color I8051.a) src1 l) in
+        move (Color I8051.b) src2 l
+
+  let move_to_dptr (addr1 : decision) (addr2 : decision) l =
+    match addr1, addr2 with
+      | Color _, _ ->
+        (* the following does not change dph, as addr1 is hwr *)
+        let l = generate (move (Color I8051.dpl) addr1 l) in
+        move (Color I8051.dph) addr2 l
+      | _, Color _ ->
+        (* the following does not change dph, as addr1 is hwr *)
+        let l = generate (move (Color I8051.dph) addr2 l) in
+        move (Color I8051.dpl) addr1 l
+      | _ ->
+        let l = generate (move (Color I8051.dph) (Color I8051.b) l) in
+        let l = generate (move (Color I8051.dpl) addr1 l) in
+        move (Color I8051.b) addr2 l
+
+  let store addr1 addr2 srcr l =
+    let l = generate (LTL.St_store l) in
+    match srcr with
+      | Color _ ->
+        let l = generate (move (Color I8051.a) srcr l) in
+        move_to_dptr addr1 addr2 l
+      | _ ->
+        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
+        let l = generate (move_to_dptr addr1 addr2 l) in
+        move (Color I8051.st0) srcr l
 
   let newframe l =
@@ -124 +181 @@
     else
       let l = generate (LTL.St_from_acc (I8051.sph, l)) in
-      let l = generate (LTL.St_op2 (I8051.Sub, I8051.dph, l)) in
-      let l = generate (LTL.St_int (I8051.dph, 0, l)) in
+      let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm 0, l)) in
       let l = generate (LTL.St_to_acc (I8051.sph, l)) in
       let l = generate (LTL.St_from_acc (I8051.spl, l)) in
-      let l = generate (LTL.St_op2 (I8051.Sub, I8051.dpl, l)) in
+      let l = generate (LTL.St_op2 (I8051.Sub, LTL.Imm stacksize, l)) in
       let l = generate (LTL.St_clear_carry l) in
-      let l = generate (LTL.St_int (I8051.dpl, stacksize, l)) in
       LTL.St_to_acc (I8051.spl, l)
 
@@ -137 +192 @@
     else
       let l = generate (LTL.St_from_acc (I8051.sph, l)) in
-      let l = generate (LTL.St_op2 (I8051.Addc, I8051.sph, l)) in
+      let l = generate (LTL.St_op2 (I8051.Addc, LTL.Reg I8051.sph, l)) in
       let l = generate (LTL.St_int (I8051.a, 0, l)) in
       let l = generate (LTL.St_from_acc (I8051.spl, l)) in
-      let l = generate (LTL.St_op2 (I8051.Add, I8051.spl, l)) in
-      LTL.St_int (I8051.a, stacksize, l)
+      let l = generate (LTL.St_op2 (I8051.Add, LTL.Imm stacksize, l)) in
+      LTL.St_to_acc (I8051.spl, l)
 
 
@@ -174 +229 @@
         move (lookup destr) (Color sourcehwr) l
 
-      | ERTL.St_set_hdw (desthwr, sourcer, l) ->
+      | ERTL.St_set_hdw (desthwr, RTL.Reg sourcer, l) ->
         move (Color desthwr) (lookup sourcer) l
 
+      | ERTL.St_set_hdw (desthwr, RTL.Imm k, l) ->
+        move_int (Color desthwr) k l
+
       | ERTL.St_hdw_to_hdw (r1, r2, l) ->
-        let l = generate (LTL.St_from_acc (r1, l)) in
-        LTL.St_to_acc (r2, l)
+        move (Color r1) (Color r2) l
 
       | ERTL.St_newframe l ->
@@ -188 +245 @@
 
       | ERTL.St_framesize (r, l) ->
-        let (hdw, l) = write r l in
-        LTL.St_int (hdw, stacksize, l)
+        move_int (lookup r) stacksize l
 
       | ERTL.St_pop (r, l) ->
-        let (hdw, l) = write r l in
-        let l = generate (LTL.St_from_acc (hdw, l)) in
+        let l = generate (move (lookup r) (Color I8051.a) l) in
         LTL.St_pop l
 
       | ERTL.St_push (r, l) ->
         let l = generate (LTL.St_push l) in
-        let l = read r (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        LTL.St_skip l
+        move (Color I8051.a) (lookup r) l
 
       | ERTL.St_addrH (r, x, l) ->
-        let (hdw, l) = write r l in
-        let l = generate (LTL.St_from_acc (hdw, l)) in
-        let l = generate (LTL.St_to_acc (I8051.dph, l)) in
+        let l = generate (move (lookup r) (Color I8051.dph) l) in
         LTL.St_addr (x, l)
 
       | ERTL.St_addrL (r, x, l) ->
-        let (hdw, l) = write r l in
-        let l = generate (LTL.St_from_acc (hdw, l)) in
-        let l = generate (LTL.St_to_acc (I8051.dpl, l)) in
+        let l = generate (move (lookup r) (Color I8051.dpl) l) in
         LTL.St_addr (x, l)
 
-      | ERTL.St_int (r, i, l) ->
-        let (hdw, l) = write r l in
-        LTL.St_int (hdw, i, l)
-
-      | ERTL.St_move (r1, r2, l) ->
+      | ERTL.St_move (r, RTL.Imm i, l) ->
+        move_int (lookup r) i l
+
+      | ERTL.St_move (r1, RTL.Reg r2, l) ->
         move (lookup r1) (lookup r2) l
 
       | ERTL.St_opaccsA (opaccs, destr, srcr1, srcr2, l) ->
-        let (hdw, l) = write destr l in
-        let l = generate (LTL.St_from_acc (hdw, l)) in
+        let l = generate (move (lookup destr) (Color I8051.a) l) in
         let l = generate (LTL.St_opaccs (opaccs, l)) in
-        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        let l = generate (LTL.St_from_acc (I8051.b, l)) in
-        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        LTL.St_skip l
+        let l = generate (move (Color I8051.a) (lookup srcr1) l) in
+        move (Color I8051.b) (lookup srcr2) l
 
       | ERTL.St_opaccsB (opaccs, destr, srcr1, srcr2, l) ->
-        let (hdw, l) = write destr l in
-        let l = generate (LTL.St_from_acc (hdw, l)) in
-        let l = generate (LTL.St_to_acc (I8051.b, l)) in
+        let l = generate (move (lookup destr) (Color I8051.b) l) in
         let l = generate (LTL.St_opaccs (opaccs, l)) in
-        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        let l = generate (LTL.St_from_acc (I8051.b, l)) in
-        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        LTL.St_skip l
+        let l = generate (move (Color I8051.a) (lookup srcr1) l) in
+        move (Color I8051.b) (lookup srcr2) l
 
       | ERTL.St_op1 (op1, destr, srcr, l) ->
-        let (hdw, l) = write destr l in
-        let l = generate (LTL.St_from_acc (hdw, l)) in
+        let l = generate (move (lookup destr) (Color I8051.a) l) in
         let l = generate (LTL.St_op1 (op1, l)) in
-        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        LTL.St_skip l
-
-      | ERTL.St_op2 (op2, destr, srcr1, srcr2, l) ->
-        let (hdw, l) = write destr l in
-        let l = generate (LTL.St_from_acc (hdw, l)) in
-        let l = generate (LTL.St_op2 (op2, I8051.b, l)) in
-        let l = read srcr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        let l = generate (LTL.St_from_acc (I8051.b, l)) in
-        let l = read srcr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        LTL.St_skip l
+        move (Color I8051.a) (lookup srcr) l
+
+      | ERTL.St_op2 (op, destr, srcr1, RTL.Reg srcr2, l) ->
+        op2 op (lookup destr) (lookup srcr1) (lookup srcr2) l
+
+      | ERTL.St_op2 (op2, destr, srcr1, RTL.Imm k, l) ->
+        let l = generate (move (lookup destr) (Color I8051.a) l) in
+        let l = generate (LTL.St_op2 (op2, LTL.Imm k, l)) in
+        move (Color I8051.a) (lookup srcr1) l
 
       | ERTL.St_clear_carry l ->
@@ -261 +300 @@
         LTL.St_set_carry l
 
+      (* act differently on hardware registers? if at least one of
+         the address bytes is hdw use of st0 can be avoided. And in
+         case of non-hdw, the read could actually target a register
+         directly *)
       | ERTL.St_load (destr, addr1, addr2, l) ->
-        let (hdw, l) = write destr l in
-        let l = generate (LTL.St_from_acc (hdw, l)) in
-        let l = generate (LTL.St_load l) in
-        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
-        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
-        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
-        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
-        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        LTL.St_skip l
+        let l = generate (move (lookup destr) (Color I8051.a) l) in
+        let l = generate (LTL.St_load l) in
+        move_to_dptr (lookup addr1) (lookup addr2) l
 
       | ERTL.St_store (addr1, addr2, srcr, l) ->
-        let l = generate (LTL.St_store l) in
-        let l = generate (LTL.St_to_acc (I8051.st1, l)) in
-        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
-        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
-        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
-        let l = read addr1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
-        let l = read addr2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        let l = generate (LTL.St_from_acc (I8051.st1, l)) in
-        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        LTL.St_skip l
+        store (lookup addr1) (lookup addr2) (lookup srcr) l
 
       | ERTL.St_call_id (f, _, l) ->
@@ -291 +317 @@
       | ERTL.St_call_ptr (f1, f2, _, l) ->
         let l = generate (LTL.St_call_ptr l) in
-        let l = generate (LTL.St_from_acc (I8051.dph, l)) in
-        let l = generate (LTL.St_to_acc (I8051.st0, l)) in
-        let l = generate (LTL.St_from_acc (I8051.dpl, l)) in
-        let l = read f1 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        let l = generate (LTL.St_from_acc (I8051.st0, l)) in
-        let l = read f2 (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        LTL.St_skip l
+        move_to_dptr (lookup f1) (lookup f2) l
 
       | ERTL.St_cond (srcr, lbl_true, lbl_false) ->
         let l = generate (LTL.St_condacc (lbl_true, lbl_false)) in
-        let l = read srcr (fun hdw -> LTL.St_to_acc (hdw, l)) in
-        LTL.St_skip l
+        move (Color I8051.a) (lookup srcr) l
 
       | ERTL.St_return _ ->

Deliverables/D2.2/8051/src/ERTL/build.ml

@@ -70 +70 @@
           let exceptions =
             match stmt with
-            | St_move (_, sourcer, _)
-            | St_set_hdw (_, sourcer, _) ->
+            | St_move (_, RTL.Reg sourcer, _)
+            | St_set_hdw (_, RTL.Reg sourcer, _) ->
                  Liveness.L.psingleton sourcer
             | St_get_hdw (_, sourcehwr, _) ->
@@ -103 +103 @@
           let graph =
             match stmt with
-            | St_move (r1, r2, _) ->
+            | St_move (r1, RTL.Reg r2, _) ->
                 mkppp graph r1 r2
             | St_get_hdw (r, hwr, _)
-            | St_set_hdw (hwr, r, _) ->
+            | St_set_hdw (hwr, RTL.Reg r, _) ->
                 mkpph graph r hwr
             | _ ->

Deliverables/D2.2/8051/src/ERTL/liveness.ml

@@ -30 +30 @@
   | St_addrH (_, _, l)
   | St_addrL (_, _, l)
-  | St_int (_, _, l)
+  (* | St_int (_, _, l) *)
   | St_move (_, _, l)
   | St_opaccsA (_, _, _, _, l)
@@ -112 +112 @@
   | St_framesize (r, _)
   | St_pop (r, _)
-  | St_int (r, _, _)
+  (* | St_int (r, _, _) *)
   | St_addrH (r, _, _)
   | St_addrL (r, _, _)
@@ -154 +154 @@
   | St_addrH _
   | St_addrL _
-  | St_int _
+  (* | St_int _ *)
   | St_clear_carry _
-  | St_set_carry _ ->
+  | St_set_carry _
+  | St_set_hdw (_, RTL.Imm _, _)
+  | St_move (_, RTL.Imm _, _) ->
     L.bottom
   | St_call_id (_, nparams, _) ->
@@ -169 +171 @@
   | St_hdw_to_hdw (_, r, _) ->
     L.hsingleton r
-  | St_set_hdw (_, r, _)
+  | St_op2 (I8051.Addc, _, r1, RTL.Reg r2, _) ->
+    L.join (L.join (L.psingleton r1) (L.psingleton r2))
+      (L.hsingleton I8051.carry)
+  | St_op2 (I8051.Addc, _, r1, RTL.Imm _, _) ->
+    L.join (L.psingleton r1) (L.hsingleton I8051.carry)
+  | St_set_hdw (_, RTL.Reg r, _)
   | St_push (r, _)
-  | St_move (_, r, _)
+  | St_move (_, RTL.Reg r, _)
   | St_op1 (_, _, r, _)
+  | St_op2 (_, _, r, RTL.Imm _, _)
   | St_cond (r, _, _) ->
     L.psingleton r
-  | St_op2 (I8051.Addc, _, r1, r2, _) ->
-    L.join (L.join (L.psingleton r1) (L.psingleton r2))
-      (L.hsingleton I8051.carry)
   | St_opaccsA (_, _, r1, r2, _)
   | St_opaccsB (_, _, r1, r2, _)
-  | St_op2 (_, _, r1, r2, _)
+  | St_op2 (_, _, r1, RTL.Reg r2, _)
   | St_load (_, r1, r2, _) ->
     L.join (L.psingleton r1) (L.psingleton r2)
@@ -187 +192 @@
   | St_newframe _
   | St_delframe _ ->
-    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)    
+    L.join (L.hsingleton I8051.spl) (L.hsingleton I8051.sph)
   | St_return _ ->
     Register.Set.empty, I8051.RegisterSet.union I8051.callee_saved ret_regs
@@ -224 +229 @@
   | St_get_hdw (r, _, l)
   | St_framesize (r, l)
-  | St_int (r, _, l)
+  (* | St_int (r, _, l) *)
   | St_addrH (r, _, l)
   | St_addrL (r, _, l)

Deliverables/D2.2/8051/src/ERTL/uses.ml

@@ -23 +23 @@
   | St_ind_inc _
   | St_hdw_to_hdw _
+  | St_set_hdw (_, RTL.Imm _, _)
   | St_newframe _
   | St_delframe _
@@ -31 +32 @@
     uses
   | St_get_hdw (r, _, _)
-  | St_set_hdw (_, r, _)
+  | St_set_hdw (_, RTL.Reg r, _)
   | St_framesize (r, _)
   | St_pop (r, _)
   | St_push (r, _)
-  | St_int (r, _, _)
+  | St_move (r, RTL.Imm _, _)
   | St_addrH (r, _, _)
   | St_addrL (r, _, _)
   | St_cond (r, _, _) ->
     count r uses
-  | St_move (r1, r2, _)
+  | St_move (r1, RTL.Reg r2, _)
   | St_op1 (_, r1, r2, _)
+  | St_op2 (_, r1, r2, RTL.Imm _, _)
   | St_call_ptr (r1, r2, _, _) ->
     count r1 (count r2 uses)
   | St_opaccsA (_, r1, r2, r3, _)
   | St_opaccsB (_, r1, r2, r3, _)
-  | St_op2 (_, r1, r2, r3, _)
+  | St_op2 (_, r1, r2, RTL.Reg r3, _)
   | St_load (r1, r2, r3, _)
   | St_store (r1, r2, r3, _) ->

Deliverables/D2.2/8051/src/LIN/LIN.mli

@@ -1 +1 @@
 
 (** This module defines the abstract syntax tree of [LIN]. *)
+
+type argument = LTL.argument
 
 (** Compared to LTL where functions were graphs, the functions of a LIN program
@@ -55 +57 @@
   (* Apply a binary operation on the A accumulator. Parameters are the
      operation, and the other source register. *)
-  | St_op2 of I8051.op2 * I8051.register
+  | St_op2 of I8051.op2 * argument
 
   (* Set the carry flag to zero. *)

Deliverables/D2.2/8051/src/LIN/LINInterpret.ml

@@ -96 +96 @@
   else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
 
+let get_arg a st = match a with
+  | LTL.Imm i -> Val.of_int i
+  | LTL.Reg r -> get_reg r st
+
 let push st v =
   let mem = Mem.store st.mem chunk st.isp v in
@@ -262 +266 @@
 
     | LIN.St_op2 (op2, srcr) ->
-      let (v, carry) =
-        Eval.op2 st.carry op2
-          (get_reg I8051.a st)
-          (get_reg srcr st) in
+      let (v, carry) = 
+        Eval.op2 st.carry op2
+          (get_reg I8051.a st)
+          (get_arg srcr st) in
       let st = change_carry st carry in
       let st = add_reg I8051.a v st in

Deliverables/D2.2/8051/src/LIN/LINPrinter.ml

@@ -19 +19 @@
 let print_a = print_reg I8051.a
 
+let print_arg = function
+  | LTL.Imm i -> string_of_int i
+  | LTL.Reg r -> print_reg r
 
 let print_statement = function
@@ -51 +54 @@
   | LIN.St_op2 (op2, srcr) ->
     Printf.sprintf "%s %s, %s"
-      (I8051.print_op2 op2) print_a (print_reg srcr)
+      (I8051.print_op2 op2) print_a (print_arg srcr)
   | LIN.St_clear_carry -> "clear CARRY"
   | LIN.St_set_carry -> "set CARRY"

Deliverables/D2.2/8051/src/LIN/LINToASM.ml

@@ -55 +55 @@
 let byte_of_int i = vect_of_int i `Eight
 let data_of_int i = `DATA (byte_of_int i)
+let reg_or_data = function
+  | LTL.Imm k -> data_of_int k
+  | LTL.Reg r -> I8051.reg_addr r
 let data16_of_int i = `DATA16 (vect_of_int i `Sixteen)
 let acc_addr = I8051.reg_addr I8051.a
@@ -95 +98 @@
   | LIN.St_op1 I8051.Inc ->
     [`INC `A]
-  | LIN.St_op2 (I8051.Add, r) ->
-    [`ADD (`A, I8051.reg_addr r)]
-  | LIN.St_op2 (I8051.Addc, r) ->
-    [`ADDC (`A, I8051.reg_addr r)]
-  | LIN.St_op2 (I8051.Sub, r) ->
-    [`SUBB (`A, I8051.reg_addr r)]
+  | LIN.St_op1 I8051.Rl ->
+    [`RL `A]
+  | LIN.St_op2 (I8051.Add, a) ->
+    [`ADD (`A, reg_or_data a)]
+  | LIN.St_op2 (I8051.Addc, a) ->
+    [`ADDC (`A, reg_or_data a)]
+  | LIN.St_op2 (I8051.Sub, a) ->
+    [`SUBB (`A, reg_or_data a)]
   | LIN.St_op2 (I8051.And, r) ->
-    [`ANL (`U1 (`A, I8051.reg_addr r))]
+    [`ANL (`U1 (`A, reg_or_data r))]
   | LIN.St_op2 (I8051.Or, r) ->
-    [`ORL (`U1 (`A, I8051.reg_addr r))]
+    [`ORL (`U1 (`A, reg_or_data r))]
   | LIN.St_op2 (I8051.Xor, r) ->
-    [`XRL (`U1 (`A, I8051.reg_addr r))]
+    [`XRL (`U1 (`A, reg_or_data r))]
   | LIN.St_clear_carry ->
     [`CLR `C]

Deliverables/D2.2/8051/src/LTL/LTL.mli

@@ -7 +7 @@
     algorithm. Actually, this coloring algorithm relies on the result of a
     liveness analysis that will also allow to remove dead code. *)
+
+type argument =
+  | Reg of I8051.register
+  | Imm of int
 
 type statement =
@@ -58 +62 @@
 
   (* Apply a binary operation on the A accumulator. Parameters are the
-     operation, the other source register, and the label of the next
+     operation, the other argument, and the label of the next
      statement. *)
-  | St_op2 of I8051.op2 * I8051.register * Label.t
+  | St_op2 of I8051.op2 * argument * Label.t
 
   (* Set the carry flag to zero. Parameter is the label of the next

Deliverables/D2.2/8051/src/LTL/LTLInterpret.ml

@@ -123 +123 @@
   else error ("Unknown hardware register " ^ (I8051.print_register r) ^ ".")
 
+let get_arg a st = match a with
+  | LTL.Imm i -> Val.of_int i
+  | LTL.Reg r -> get_reg r st
+
 let push st v =
   let mem = Mem.store st.mem chunk st.isp v in
@@ -294 +298 @@
         Eval.op2 st.carry op2
           (get_reg I8051.a st)
-          (get_reg srcr st) in
+          (get_arg srcr st) in
       let st = change_carry st carry in
       let st = add_reg I8051.a v st in

Deliverables/D2.2/8051/src/LTL/LTLPrinter.ml

@@ -18 +18 @@
 
 let print_a = print_reg I8051.a
+
+let print_arg = function
+  | LTL.Imm i -> string_of_int i
+  | LTL.Reg r -> print_reg r
 
 
@@ -50 +54 @@
   | LTL.St_op2 (op2, srcr, lbl) ->
     Printf.sprintf "%s %s, %s --> %s"
-      (I8051.print_op2 op2) print_a (print_reg srcr) lbl
+      (I8051.print_op2 op2) print_a (print_arg srcr) lbl
   | LTL.St_clear_carry lbl ->
     Printf.sprintf "clear CARRY --> %s" lbl

Deliverables/D2.2/8051/src/RTL/RTL.mli

@@ -9 +9 @@
 type registers = Register.t list
 
+(* arguments to certain operations: either registers or immediate args *)
+type argument =
+  | Reg of Register.t
+  | Imm of int
+
 type statement =
 
@@ -17 +22 @@
   | St_cost of CostLabel.t * Label.t
 
-  (* Reset to 0 a loop index *) 
+  (* Reset to 0 a loop index *)
   | St_ind_0 of CostLabel.index * Label.t
 
@@ -32 +37 @@
   | St_stackaddr of Register.t * Register.t * Label.t
 
-  (* Assign an integer constant to a register. Parameters are the destination
-     register, the integer and the label of the next statement. *)
-  | St_int of Register.t * int * Label.t
+  (* (\* Assign an integer constant to a register. Parameters are the destination *)
+  (*    register, the integer and the label of the next statement. *\) *)
+  (* | St_int of Register.t * int * Label.t *)
 
   (* Move the content of a register to another. Parameters are the destination
-     register, the source register, and the label of the next statement. *)
-  | St_move of Register.t * Register.t * Label.t
+     register, the source argument, and the label of the next statement. *)
+  | St_move of Register.t * argument * Label.t
 
   (* Apply a binary operation that will later be translated in an operation on
@@ -52 +57 @@
 
   (* Apply a binary operation. Parameters are the operation, the destination
-     register, the source registers, and the label of the next statement. *)
-  | St_op2 of I8051.op2 * Register.t * Register.t * Register.t * Label.t
+     register, the source arguments, and the label of the next statement. *)
+  | St_op2 of I8051.op2 * Register.t * Register.t * argument * Label.t
 
   (* Set the carry flag to zero. Parameter is the label of the next

Deliverables/D2.2/8051/src/RTL/RTLInterpret.ml

@@ -89 +89 @@
   if Register.Map.mem r lenv then Register.Map.find r lenv
   else error ("Unknown local register \"" ^ (Register.print r) ^ "\".")
+
+let get_local_arg_value (lenv : local_env) : RTL.argument -> Val.t = function
+  | RTL.Reg r -> get_local_value lenv r
+  | RTL.Imm i -> Val.of_int i
+
 let get_arg_values lenv args = List.map (get_local_value lenv) args
 
@@ -159 +164 @@
         assign_state sfrs graph lbl sp lenv carry mem inds trace [r1 ; r2] sp
 
-      | RTL.St_int (r, i, lbl) ->
-        assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i]
+      (* | RTL.St_int (r, i, lbl) -> *)
+      (*   assign_state sfrs graph lbl sp lenv carry mem inds trace [r] [Val.of_int i] *)
 
       | RTL.St_move (destr, srcr, lbl) ->
         assign_state sfrs graph lbl sp lenv carry mem inds trace [destr]
-          [get_local_value lenv srcr]
+          [get_local_arg_value lenv srcr]
 
       | RTL.St_opaccs (opaccs, destr1, destr2, srcr1, srcr2, lbl) ->
@@ -182 +187 @@
           Eval.op2 carry op2
             (get_local_value lenv srcr1)
-            (get_local_value lenv srcr2) in
+            (get_local_arg_value lenv srcr2) in
         assign_state sfrs graph lbl sp lenv carry mem inds trace [destr] [v]
 

Deliverables/D2.2/8051/src/RTL/RTLPrinter.ml

@@ -16 +16 @@
 
 let print_reg = Register.print
+
+let print_arg = function
+  | RTL.Reg r -> print_reg r
+  | RTL.Imm i -> string_of_int i
 
 let reg_set_to_list rs =
@@ -44 +48 @@
   | RTL.St_cost (cost_lbl, lbl) ->
     let cost_lbl = CostLabel.string_of_cost_label ~pretty:true cost_lbl in
-    Printf.sprintf "emit %s --> %s" cost_lbl lbl
+    Printf.sprintf "_emit %s --> %s" cost_lbl lbl
   | RTL.St_ind_0 (i, lbl) ->
-    Printf.sprintf "index %d --> %s" i lbl
+    Printf.sprintf "_index %d --> %s" i lbl
   | RTL.St_ind_inc (i, lbl) ->
-    Printf.sprintf "increment %d --> %s" i lbl
+    Printf.sprintf "_increment %d --> %s" i lbl
   | RTL.St_addr (dstr1, dstr2, id, lbl) ->
-    Printf.sprintf "imm (%s, %s), %s --> %s"
+    Printf.sprintf "move (%s, %s), %s --> %s"
       (print_reg dstr1) (print_reg dstr2) id lbl
   | RTL.St_stackaddr (dstr1, dstr2, lbl) ->
-    Printf.sprintf "imm (%s, %s), STACK --> %s"
+    Printf.sprintf "move (%s, %s), STACK --> %s"
       (print_reg dstr1) (print_reg dstr2) lbl
-  | RTL.St_int (dstr, i, lbl) ->
-    Printf.sprintf "imm %s, %d --> %s" (print_reg dstr) i lbl
+  (* | RTL.St_int (dstr, i, lbl) -> *)
+  (*   Printf.sprintf "imm %s, %d --> %s" (print_reg dstr) i lbl *)
   | RTL.St_move (dstr, srcr, lbl) ->
     Printf.sprintf "move %s, %s --> %s"
-      (print_reg dstr) (print_reg srcr) lbl
+      (print_reg dstr) (print_arg srcr) lbl
   | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, lbl) ->
     Printf.sprintf "%s (%s, %s) %s, %s --> %s"
@@ -76 +80 @@
       (print_reg dstr)
       (print_reg srcr1)
-      (print_reg srcr2)
+      (print_arg srcr2)
       lbl
   | RTL.St_clear_carry lbl ->

Deliverables/D2.2/8051/src/RTL/RTLToERTL.ml

@@ -34 +34 @@
   | ERTL.St_addrH (r, id, _) -> ERTL.St_addrH (r, id, lbl)
   | ERTL.St_addrL (r, id, _) -> ERTL.St_addrL (r, id, lbl)
-  | ERTL.St_int (r, i, _) -> ERTL.St_int (r, i, lbl)
-  | ERTL.St_move (r1, r2, _) -> ERTL.St_move (r1, r2, lbl)
+  | ERTL.St_move (r1, a, _) -> ERTL.St_move (r1, a, lbl)
   | ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, _) ->
     ERTL.St_opaccsA (opaccs, dstr, srcr1, srcr2, lbl)
@@ -102 +101 @@
 let restore_hdws l =
   let f (destr, srcr) start_lbl =
-    adds_graph [ERTL.St_set_hdw (destr, srcr, start_lbl)] start_lbl in
+    adds_graph [ERTL.St_set_hdw (destr, RTL.Reg srcr, start_lbl)] start_lbl in
   List.map f (List.map (fun (x, y) -> (y, x)) l)
 
@@ -118 +117 @@
   adds_graph
     [ERTL.St_framesize (addr1, start_lbl) ;
-     ERTL.St_int (tmpr, off+I8051.int_size, start_lbl) ;
-     ERTL.St_op2 (I8051.Sub, addr1, addr1, tmpr, start_lbl) ;
+     ERTL.St_op2 (I8051.Sub, addr1, addr1, RTL.Imm (off+I8051.int_size),
+                  start_lbl) ;
      ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
-     ERTL.St_op2 (I8051.Add, addr1, addr1, tmpr, start_lbl) ;
-     ERTL.St_int (addr2, 0, start_lbl) ;
+     ERTL.St_op2 (I8051.Add, addr1, addr1, RTL.Reg tmpr, start_lbl) ;
      ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
-     ERTL.St_op2 (I8051.Addc, addr2, addr2, tmpr, start_lbl) ;
+     ERTL.St_op2 (I8051.Addc, addr2, tmpr, RTL.Imm 0, start_lbl) ;
      ERTL.St_load (destr, addr1, addr2, start_lbl)]
     start_lbl dest_lbl def
@@ -176 +174 @@
 
 let save_return ret_regs start_lbl dest_lbl def =
-  let (def, tmpr) = fresh_reg def in
   let ((common1, rest1), (common2, _)) =
     MiscPottier.reduce I8051.sts ret_regs in
-  let init_tmpr = ERTL.St_int (tmpr, 0, start_lbl) in
-  let f_save st r = ERTL.St_set_hdw (st, r, start_lbl) in
+  let f_save st r = ERTL.St_set_hdw (st, RTL.Reg r, start_lbl) in
   let saves = List.map2 f_save common1 common2 in
-  let f_default st = ERTL.St_set_hdw (st, tmpr, start_lbl) in
+  let f_default st = ERTL.St_set_hdw (st, RTL.Imm 0, start_lbl) in
   let defaults = List.map f_default rest1 in
-  adds_graph (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
+  adds_graph (saves @ defaults) start_lbl dest_lbl def
 
 let assign_result start_lbl =
@@ -252 +248 @@
   let (def, tmpr) = fresh_reg def in
   adds_graph
-    [ERTL.St_int (addr1, off+I8051.int_size, start_lbl) ;
-     ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
+    [ERTL.St_get_hdw (tmpr, I8051.spl, start_lbl) ;
      ERTL.St_clear_carry start_lbl ;
-     ERTL.St_op2 (I8051.Sub, addr1, tmpr, addr1, start_lbl) ;
+     ERTL.St_op2 (I8051.Sub, addr1, tmpr, RTL.Imm (off+I8051.int_size),
+                  start_lbl) ;
      ERTL.St_get_hdw (tmpr, I8051.sph, start_lbl) ;
-     ERTL.St_int (addr2, 0, start_lbl) ;
-     ERTL.St_op2 (I8051.Sub, addr2, tmpr, addr2, start_lbl) ;
+     ERTL.St_op2 (I8051.Sub, addr2, tmpr, RTL.Imm 0, start_lbl) ;
      ERTL.St_store (addr1, addr2, srcr, start_lbl)]
     start_lbl dest_lbl def
@@ -338 +333 @@
       lbl lbl' def
 
-  | RTL.St_int (r, i, lbl') ->
-    add_graph lbl (ERTL.St_int (r, i, lbl')) def
+  (* | RTL.St_int (r, i, lbl') -> *)
+  (*   add_graph lbl (ERTL.St_int (r, i, lbl')) def *)
 
   | RTL.St_move (r1, r2, lbl') ->
@@ -444 +439 @@
     | ERTL.St_set_hdw (_, _, lbl) | ERTL.St_hdw_to_hdw (_, _, lbl)
     | ERTL.St_pop (_, lbl) | ERTL.St_push (_, lbl) | ERTL.St_addrH (_, _, lbl)
-    | ERTL.St_addrL (_, _, lbl) | ERTL.St_int (_, _, lbl)
+    | ERTL.St_addrL (_, _, lbl) (* | ERTL.St_int (_, _, lbl) *)
     | ERTL.St_move (_, _, lbl) | ERTL.St_opaccsA (_, _, _, _, lbl)
     | ERTL.St_opaccsB (_, _, _, _, lbl)

Deliverables/D2.2/8051/src/RTLabs/RTLabs.mli

@@ -11 +11 @@
 
 
+(* arguments to certain operations: either registers or immediate args *)
 type argument =
   | Reg of Register.t

Deliverables/D2.2/8051/src/RTLabs/RTLabsPrinter.ml

@@ -168 +168 @@
         lbl
   | RTLabs.St_load (q, addr, destr, lbl) ->
-      Printf.sprintf "%s := *(%s) %s --> %s"
+      Printf.sprintf "%s := (%s) *%s --> %s"
         (print_reg destr)
         (Memory.string_of_quantity q)
@@ -174 +174 @@
         lbl
   | RTLabs.St_store (q, addr, srcr, lbl) ->
-      Printf.sprintf "*(%s)%s := %s --> %s"
+      Printf.sprintf "*%s := (%s)%s --> %s"
+        (print_arg addr)
         (Memory.string_of_quantity q)
-        (print_arg addr)
         (print_arg srcr)
         lbl
@@ -216 +216 @@
         (Primitive.print_sig sg)
   | RTLabs.St_cond (r, lbl_true, lbl_false) ->
-      Printf.sprintf "%s? --> %s, %s"
+      Printf.sprintf "if %s --> %s else --> %s"
         (print_reg r)
         lbl_true

Deliverables/D2.2/8051/src/RTLabs/RTLabsToRTL.ml

@@ -97 +97 @@
   | RTL.St_addr (r1, r2, id, _) -> RTL.St_addr (r1, r2, id, lbl)
   | RTL.St_stackaddr (r1, r2, _) -> RTL.St_stackaddr (r1, r2, lbl)
-  | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl)
+  (* | RTL.St_int (r, i, _) -> RTL.St_int (r, i, lbl) *)
   | RTL.St_move (r1, r2, _) -> RTL.St_move (r1, r2, lbl)
   | RTL.St_opaccs (opaccs, dstr1, dstr2, srcr1, srcr2, _) ->
@@ -204 +204 @@
     let module M = IntValue.Make (struct let size = size end) in
     let is = List.map M.to_int (M.break (M.of_int i) size) in
-    let f r i = RTL.St_int (r, i, dest_lbl) in
+    let f r i = RTL.St_move (r, RTL.Imm i, dest_lbl) in
     let l = List.map2 f destrs is in
     adds_graph l start_lbl dest_lbl def
@@ -229 +229 @@
 let rec translate_move destrs srcrs start_lbl =
   let ((common1, rest1), (common2, rest2)) = MiscPottier.reduce destrs srcrs in
-  let f_common destr srcr = RTL.St_move (destr, srcr, start_lbl) in
+  let f_common destr srcr = RTL.St_move (destr, RTL.Reg srcr, start_lbl) in
   let translates1 = adds_graph (List.map2 f_common common1 common2) in
   let translates2 = translate_cst (AST.Cst_int 0) rest1 in
   add_translates [translates1 ; translates2] start_lbl
 
+let rec translate_imm destrs vals start_lbl =
+  let ((common1, rest1), (common2, _)) = MiscPottier.reduce destrs vals in
+  let f_common destr srcr = RTL.St_move (destr, RTL.Imm srcr, start_lbl) in
+  let translates1 = adds_graph (List.map2 f_common common1 common2) in
+  let translates2 = translate_cst (AST.Cst_int 0) rest1 in
+  add_translates [translates1 ; translates2] start_lbl
+
 
 let translate_cast_unsigned destrs start_lbl dest_lbl def =
-  let (def, tmp_zero) = fresh_reg def in
-  let zeros = MiscPottier.make tmp_zero (List.length destrs) in
-  add_translates
-    [adds_graph [RTL.St_int (tmp_zero, 0, start_lbl)] ;
-     translate_move destrs zeros]
-    start_lbl dest_lbl def
+  translate_cst (AST.Cst_int 0) destrs start_lbl dest_lbl def
 
 let translate_cast_signed destrs srcr start_lbl dest_lbl def =
-  let (def, tmp_128) = fresh_reg def in
-  let (def, tmp_255) = fresh_reg def in
   let (def, tmpr) = fresh_reg def in
-  let (def, dummy) = fresh_reg def in
   let insts =
-    [RTL.St_int (tmp_128, 128, start_lbl) ;
-     RTL.St_op2 (I8051.And, tmpr, tmp_128, srcr, start_lbl) ;
-     RTL.St_opaccs (I8051.DivuModu, tmpr, dummy, tmpr, tmp_128, start_lbl) ;
-     RTL.St_int (tmp_255, 255, start_lbl) ;
-     RTL.St_opaccs (I8051.Mul, tmpr, dummy, tmpr, tmp_255, start_lbl)] in
+    (* this sets tmpr to 0xFF if s is neg, 0x00 o.w. Done like that:
+       byte in tmpr if srcr is: neg   |  pos
+       tmpr ← srcr | 127       11...1 | 01...1
+       tmpr ← tmpr <rot< 1     1...11 | 1...10
+       tmpr ← INC tmpr         0....0 | 1....1
+       tmpr ← CPL tmpr         1....1 | 0....0
+
+     *)
+    [RTL.St_op2 (I8051.Or, tmpr, srcr, RTL.Imm 127, start_lbl) ;
+     RTL.St_op1 (I8051.Rl, tmpr, tmpr, start_lbl) ;
+     RTL.St_op1 (I8051.Inc, tmpr, tmpr, start_lbl) ;
+     RTL.St_op1 (I8051.Cmpl, tmpr, tmpr, start_lbl) ] in
   let srcrs = MiscPottier.make tmpr (List.length destrs) in
   add_translates [adds_graph insts ; translate_move destrs srcrs]
@@ -273 +279 @@
 
 let translate_negint destrs srcrs start_lbl dest_lbl def =
-  assert (List.length destrs = List.length srcrs) ;
-  let (def, tmpr) = fresh_reg def in
+  assert (List.length destrs = List.length srcrs && List.length destrs > 0) ;
   let f_cmpl destr srcr = RTL.St_op1 (I8051.Cmpl, destr, srcr, start_lbl) in
   let insts_cmpl = List.map2 f_cmpl destrs srcrs in
-  let insts_init =
-    [RTL.St_set_carry start_lbl ;
-     RTL.St_int (tmpr, 0, start_lbl)] in
-  let f_add destr = RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl) in
-  let insts_add = List.map f_add destrs in
-  adds_graph (insts_cmpl @ insts_init @ insts_add)
+  let first, rest = List.hd destrs, List.tl destrs in
+  let inst_init =
+    RTL.St_op2 (I8051.Add, first, first, RTL.Imm 0, start_lbl) in
+  let f_add destr =
+    RTL.St_op2 (I8051.Addc, destr, destr, RTL.Imm 0, start_lbl) in
+  let insts_add = List.map f_add rest in
+  adds_graph (insts_cmpl @ inst_init :: insts_add)
     start_lbl dest_lbl def
 
 
-let translate_notbool destrs srcrs start_lbl dest_lbl def = match destrs with
-  | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
-  | destr :: destrs ->
-    let (def, tmpr) = fresh_reg def in
-    let (def, tmp_srcrs) = fresh_regs def (List.length srcrs) in
-    let save_srcrs = translate_move tmp_srcrs srcrs in
-    let init_destr = RTL.St_int (destr, 1, start_lbl) in
-    let f tmp_srcr =
-      [RTL.St_clear_carry start_lbl ;
-       RTL.St_int (tmpr, 0, start_lbl) ;
-       RTL.St_op2 (I8051.Sub, tmpr, tmpr, tmp_srcr, start_lbl) ;
-       RTL.St_int (tmpr, 0, start_lbl) ;
-       RTL.St_op2 (I8051.Addc, tmpr, tmpr, tmpr, start_lbl) ;
-       RTL.St_op2 (I8051.Xor, destr, destr, tmpr, start_lbl)] in
-    let insts = init_destr :: (List.flatten (List.map f tmp_srcrs)) in
-    let epilogue = translate_cst (AST.Cst_int 0) destrs in
-    add_translates [save_srcrs ; adds_graph insts ; epilogue]
-      start_lbl dest_lbl def
+let translate_notbool destrs srcrs start_lbl dest_lbl def =
+  match destrs,srcrs with
+    | [], _ -> adds_graph [] start_lbl dest_lbl def
+    | destr :: destrs, srcr :: srcrs ->
+      let (def, tmpr) = fresh_reg def in
+      let init_destr = RTL.St_move (destr, RTL.Reg srcr, start_lbl) in
+      let f r =
+        RTL.St_op2 (I8051.Or, destr, destr, RTL.Reg r, start_lbl) in
+      let big_or = List.map f srcrs in
+      let finalize_destr =
+        [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
+         RTL.St_clear_carry start_lbl ;
+         RTL.St_op2 (I8051.Sub, tmpr, tmpr, RTL.Reg destr, start_lbl) ;
+         (* carry bit is set iff destr is non-zero iff destrs was non-zero *)
+         RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
+         RTL.St_op2 (I8051.Addc, destr, tmpr, RTL.Reg tmpr, start_lbl) ;
+         (* destr = carry bit = bigor of old destrs *)
+         RTL.St_op2 (I8051.Xor, destr, destr, RTL.Imm 1, start_lbl)] in
+      let epilogue = translate_cst (AST.Cst_int 0) destrs in
+      add_translates [adds_graph (init_destr :: big_or @ finalize_destr) ;
+                      epilogue]
+        start_lbl dest_lbl def
+    | destr :: destrs, [] ->
+      translate_cst (AST.Cst_int 1) destrs start_lbl dest_lbl def
 
 
@@ -336 +348 @@
     MiscPottier.reduce destrs_rest srcrs_rest in
   let (def, tmpr) = fresh_reg def in
-  let insts_init =
-    [RTL.St_clear_carry start_lbl ;
-     RTL.St_int (tmpr, 0, start_lbl)] in
+  let carry_init = match op with
+    | I8051.Addc | I8051.Sub ->
+      (* depend on carry bit *)
+      [RTL.St_clear_carry start_lbl]
+    | I8051.Add -> assert false (* should not call with add, not correct *)
+    | _ -> [] in
+  let inst_init = RTL.St_move (tmpr, RTL.Imm 0, start_lbl) :: carry_init in
   let f_add destr srcr1 srcr2 =
-    RTL.St_op2 (op, destr, srcr1, srcr2, start_lbl) in
+    RTL.St_op2 (op, destr, srcr1, RTL.Reg srcr2, start_lbl) in
   let insts_add =
     MiscPottier.map3 f_add destrs_common srcrs1_common srcrs2_common in
   let f_add_cted destr srcr =
-    RTL.St_op2 (op, destr, srcr, tmpr, start_lbl) in
+    RTL.St_op2 (op, destr, srcr, RTL.Reg tmpr, start_lbl) in
   let insts_add_cted = List.map2 f_add_cted destrs_cted srcrs_cted in
   let f_rest destr =
-    RTL.St_op2 (op, destr, tmpr, tmpr, start_lbl) in
+    RTL.St_op2 (op, destr, tmpr, RTL.Reg tmpr, start_lbl) in
   let insts_rest = List.map f_rest destrs_rest in
-  adds_graph (insts_init @ insts_add @ insts_add_cted @ insts_rest)
+  adds_graph (inst_init @ insts_add @ insts_add_cted @ insts_rest)
     start_lbl dest_lbl def
 
@@ -357 +373 @@
     | [], _ -> adds_graph [RTL.St_skip start_lbl] start_lbl
     | [destr], [] ->
-      adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
-                  RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
+      adds_graph [RTL.St_op2 (I8051.Addc, destr, destr, RTL.Imm 0, start_lbl)]
         start_lbl
     | destr1 :: destr2 :: destrs, [] ->
       add_translates
-        [adds_graph [RTL.St_int (tmpr, 0, start_lbl) ;
-                     RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl) ;
-                     RTL.St_op2 (I8051.Addc, destr2, tmpr, tmpr, start_lbl)] ;
+        [adds_graph
+            [RTL.St_move (tmpr, RTL.Imm 0, start_lbl) ;
+             RTL.St_op2 (I8051.Addc, destr1, destr1, RTL.Imm 0, start_lbl) ;
+             RTL.St_op2 (I8051.Addc, destr2, tmpr, RTL.Imm 0, start_lbl)] ;
          translate_cst (AST.Cst_int 0) destrs]
         start_lbl
@@ -370 +386 @@
       adds_graph
         [RTL.St_opaccs (I8051.Mul, tmpr, dummy, srcr2, srcr1, start_lbl) ;
-         RTL.St_op2 (I8051.Addc, destr, destr, tmpr, start_lbl)]
+         RTL.St_op2 (I8051.Addc, destr, destr, RTL.Reg tmpr, start_lbl)]
         start_lbl
     | destr1 :: destr2 :: destrs, srcr1 :: srcrs1 ->
@@ -377 +393 @@
             [RTL.St_opaccs
                 (I8051.Mul, tmpr, destr2, srcr2, srcr1, start_lbl) ;
-             RTL.St_op2 (I8051.Addc, destr1, destr1, tmpr, start_lbl)] ;
+             RTL.St_op2 (I8051.Addc, destr1, destr1, RTL.Reg tmpr, start_lbl)] ;
          translate_mul1 dummy tmpr (destr2 :: destrs) srcrs1 srcr2]
         start_lbl
@@ -389 +405 @@
       | tmp_destr2 :: tmp_destrs2 ->
         [adds_graph [RTL.St_clear_carry dummy_lbl ;
-                     RTL.St_int (tmp_destr2, 0, dummy_lbl)] ;
+                     RTL.St_move (tmp_destr2, RTL.Imm 0, dummy_lbl)] ;
          translate_mul1 dummy tmpr (tmp_destr2 :: tmp_destrs2) srcrs1 srcr2i ;
          translate_cst (AST.Cst_int 0) tmp_destrs1 ;
-         adds_graph [RTL.St_clear_carry dummy_lbl] ;
          translate_op I8051.Addc destrs destrs tmp_destrs])
 
@@ -422 +437 @@
       add_translates [inst_div ; insts_rest] start_lbl dest_lbl def
 
-
 let translate_ne destrs srcrs1 srcrs2 start_lbl dest_lbl def =
   match destrs with
-    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
+    | [] -> adds_graph [] start_lbl dest_lbl def
     | destr :: destrs ->
       let (def, tmpr) = fresh_reg def in
-      let (def, tmp_zero) = fresh_reg def in
-      let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
-      let save_srcrs1 = translate_move tmp_srcrs1 srcrs1 in
-      let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
-      let save_srcrs2 = translate_move tmp_srcrs2 srcrs2 in
       let ((common1, rest1), (common2, rest2)) =
-        MiscPottier.reduce tmp_srcrs1 tmp_srcrs2 in
+        MiscPottier.reduce srcrs1 srcrs2 in
       let rest = choose_rest rest1 rest2 in
-      let inits =
-        [RTL.St_int (destr, 0, start_lbl) ;
-         RTL.St_int (tmp_zero, 0, start_lbl)] in
-      let f_common tmp_srcr1 tmp_srcr2 =
-        [RTL.St_clear_carry start_lbl ;
-         RTL.St_op2 (I8051.Sub, tmpr, tmp_srcr1, tmp_srcr2, start_lbl) ;
-         RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in
-      let insts_common = List.flatten (List.map2 f_common common1 common2) in
+      let firsts = match common1, common2 with
+        | c1hd :: c1tl, c2hd :: c2tl ->
+          let init =
+            RTL.St_op2 (I8051.Xor, destr, c1hd, RTL.Reg c2hd, start_lbl) in
+          let f_common tmp_srcr1 tmp_srcr2 =
+            [RTL.St_op2 (I8051.Xor, tmpr, tmp_srcr1,
+                         RTL.Reg tmp_srcr2, start_lbl) ;
+             RTL.St_op2 (I8051.Or, destr, destr, RTL.Reg tmpr, start_lbl)] in
+          let insts_common = List.flatten (List.map2 f_common c1tl c2tl) in
+          init :: insts_common
+        | [], [] ->
+          [RTL.St_move (destr, RTL.Imm 0, start_lbl)]
+        (* common1 and common2 have the same length *)
+        | _ -> assert false in
       let f_rest tmp_srcr =
-        [RTL.St_clear_carry start_lbl ;
-         RTL.St_op2 (I8051.Sub, tmpr, tmp_zero, tmp_srcr, start_lbl) ;
-         RTL.St_op2 (I8051.Or, destr, destr, tmpr, start_lbl)] in
-      let insts_rest = List.flatten (List.map f_rest rest) in
-      let insts = inits @ insts_common @ insts_rest in
+        RTL.St_op2 (I8051.Xor, destr, destr, RTL.Reg tmp_srcr, start_lbl) in
+      let insts_rest = List.map f_rest rest in
+      let insts = firsts @ insts_rest in
       let epilogue = translate_cst (AST.Cst_int 0) destrs in
-      add_translates [save_srcrs1 ; save_srcrs2 ; adds_graph insts ; epilogue]
-        start_lbl dest_lbl def
-
-
-let translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl
-    (srcr1, srcr2) =
-  [RTL.St_clear_carry dummy_lbl ;
-   RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
-   RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
-   RTL.St_op2 (I8051.Sub, tmpr2, srcr2, srcr1, dummy_lbl) ;
-   RTL.St_op2 (I8051.Addc, tmpr2, tmp_zero, tmp_zero, dummy_lbl) ;
-   RTL.St_op2 (I8051.Or, tmpr1, tmpr1, tmpr2, dummy_lbl) ;
-   RTL.St_op2 (I8051.Xor, tmpr1, tmpr1, tmp_one, dummy_lbl) ;
-   RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)]
-
-let translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 destr leq dummy_lbl =
-  let f = translate_eq_reg tmp_zero tmp_one tmpr1 tmpr2 destr dummy_lbl in
-  (RTL.St_int (destr, 1, dummy_lbl)) :: (List.flatten (List.map f leq))
-
-let translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq
-    srcr1 srcr2 =
-  (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @
-  [RTL.St_clear_carry dummy_lbl ;
-   RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ;
-   RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ;
-   RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ;
-   RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)]
-
-let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl
-    srcrs1 srcrs2 =
-  let f (insts, leq) srcr1 srcr2 =
-    let added_insts =
-      translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq
-        srcr1 srcr2 in
-    (insts @ added_insts, leq @ [(srcr1, srcr2)]) in
-  fst (List.fold_left2 f ([], []) srcrs1 srcrs2)
-
-let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def =
+      add_translates [ adds_graph insts ; epilogue] start_lbl dest_lbl def
+
+(* this requires destrs to be either 0 or 1 to be truly correct
+   to be used after translations that ensure this *)
+let translate_toggle_bool destrs start_lbl =
   match destrs with
-    | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def
-    | _ ->
-      let (def, tmp_destrs) = fresh_regs def (List.length destrs) in
-      let tmp_destr = List.hd tmp_destrs in
-      let (def, tmp_zero) = fresh_reg def in
-      let (def, tmp_one) = fresh_reg def in
-      let (def, tmpr1) = fresh_reg def in
-      let (def, tmpr2) = fresh_reg def in
-      let (def, tmpr3) = fresh_reg def in
-      let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in
-      let srcrs1 = List.rev srcrs1 in
-      let srcrs2 = List.rev srcrs2 in
-      let insts_init =
-        [translate_cst (AST.Cst_int 0) tmp_destrs ;
-         translate_cst (AST.Cst_int 0) added ;
-         adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ;
-                     RTL.St_int (tmp_one, 1, start_lbl)]] in
-      let insts_main =
-        translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl
-          srcrs1 srcrs2 in
-      let insts_main = [adds_graph insts_main] in
-      let insts_exit = [translate_move destrs tmp_destrs] in
-      add_translates (insts_init @ insts_main @ insts_exit )
-        start_lbl dest_lbl def
-
-
-let add_128_to_last tmp_128 rs start_lbl = match rs with
-  | [] -> adds_graph [] start_lbl
-  | _ ->
-    let r = MiscPottier.last rs in
-    adds_graph [RTL.St_op2 (I8051.Add, r, r, tmp_128, start_lbl)] start_lbl
-
+    | [] -> adds_graph [] start_lbl
+    | destr :: _ ->
+      adds_graph [RTL.St_op1 (I8051.Cmpl, destr, destr, start_lbl)] start_lbl
+
+
+
+(* let translate_eq_reg tmp_zero tmpr destr dummy_lbl *)
+(*     (srcr1, srcr2) = *)
+(*   [RTL.St_op2 (I8051.Xor, tmpr, srcr1, srcr2, dummy_lbl) ; *)
+(*    (\* now tmpr = 0 iff srcr1 = srcr2 *\) *)
+(*    RTL.St_clear_carry dummy_lbl ; *)
+(*    RTL.St_op2 (I8051.Sub, tmpr, tmp_zero, tmpr, dummy_lbl) ; *)
+(*    (\* now carry bit = (old tmpr is not zero) = (srcr1 != srcr2) *\) *)
+(*    RTL.St_op2 (I8051.Addc, tmpr, tmp_zero, tmp_zero, dummy_lbl) ; *)
+(*    (\* now tmpr = old carry bit = (srcr1 != srcr2) *\) *)
+(*    RTL.St_op1 (I8051.Cpl, tmpr, tmpr, dummy_lbl)] *)
+
+(* let translate_eq_list tmp_zero tmpr destr leq dummy_lbl = match leq with *)
+(*   | leqhd :: leqtl -> *)
+(*     let init = translate_eq_reg tmp_zero destr dummy_lbl leqhd in *)
+(*     let f p = translate_eq_reg tmp_zero tmpr destr dummy_lbl p @ *)
+(*       [RTL.St_op2 (I8051.And, destr, destr, tmpr1, dummy_lbl)] in *)
+(*     init @ List.flatten (List.map f leqtl) *)
+(*   | _ -> [RTL.St_move (destr, RTL.Imm 1, dummy_lbl)] *)
+
+(* let translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq *)
+(*     srcr1 srcr2 = *)
+(*   (translate_eq_list tmp_zero tmp_one tmpr1 tmpr2 tmpr3 leq dummy_lbl) @ *)
+(*   [RTL.St_clear_carry dummy_lbl ; *)
+(*    RTL.St_op2 (I8051.Sub, tmpr1, srcr1, srcr2, dummy_lbl) ; *)
+(*    RTL.St_op2 (I8051.Addc, tmpr1, tmp_zero, tmp_zero, dummy_lbl) ; *)
+(*    RTL.St_op2 (I8051.And, tmpr3, tmpr3, tmpr1, dummy_lbl) ; *)
+(*    RTL.St_op2 (I8051.Or, destr, destr, tmpr3, dummy_lbl)] *)
+
+(* let translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl *)
+(*     srcrs1 srcrs2 = *)
+(*   let f (insts, leq) srcr1 srcr2 = *)
+(*     let added_insts = *)
+(*       translate_atom tmp_zero tmp_one tmpr1 tmpr2 tmpr3 destr dummy_lbl leq *)
+(*      srcr1 srcr2 in *)
+(*     (insts @ added_insts, leq @ [(srcr1, srcr2)]) in *)
+(*   fst (List.fold_left2 f ([], []) srcrs1 srcrs2) *)
+
+(* let translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def = *)
+(*   match destrs with *)
+(*     | [] -> add_graph start_lbl (RTL.St_skip dest_lbl) def *)
+(*     | _ -> *)
+(*       let (def, tmp_destrs) = fresh_regs def (List.length destrs) in *)
+(*       let tmp_destr = List.hd tmp_destrs in *)
+(*       let (def, tmp_zero) = fresh_reg def in *)
+(*       let (def, tmp_one) = fresh_reg def in *)
+(*       let (def, tmpr1) = fresh_reg def in *)
+(*       let (def, tmpr2) = fresh_reg def in *)
+(*       let (def, tmpr3) = fresh_reg def in *)
+(*       let (srcrs1, srcrs2, added) = complete_regs def srcrs1 srcrs2 in *)
+(*       let srcrs1 = List.rev srcrs1 in *)
+(*       let srcrs2 = List.rev srcrs2 in *)
+(*       let insts_init = *)
+(*      [translate_cst (AST.Cst_int 0) tmp_destrs ; *)
+(*       translate_cst (AST.Cst_int 0) added ; *)
+(*       adds_graph [RTL.St_int (tmp_zero, 0, start_lbl) ; *)
+(*                   RTL.St_int (tmp_one, 1, start_lbl)]] in *)
+(*       let insts_main = *)
+(*      translate_lt_main tmp_zero tmp_one tmpr1 tmpr2 tmpr3 tmp_destr start_lbl *)
+(*        srcrs1 srcrs2 in *)
+(*       let insts_main = [adds_graph insts_main] in *)
+(*       let insts_exit = [translate_move destrs tmp_destrs] in *)
+(*       add_translates (insts_init @ insts_main @ insts_exit ) *)
+(*      start_lbl dest_lbl def *)
+
+let rec pad_with p l1 l2 = match l1, l2 with
+  | [], [] -> ([], [])
+  | x :: xs, y :: ys ->
+    let (xs', ys') = pad_with p xs ys in
+    (x :: xs', y :: ys')
+  | [], _ -> (MiscPottier.make p (List.length l2), l2)
+  | _, [] -> (l1, MiscPottier.make p (List.length l1))
+
+let translate_ltu desrtrs srcrs1 srcrs2 start_lbl dest_lbl def =
+  match desrtrs with
+    | [] -> adds_graph [] start_lbl dest_lbl def
+    | destr :: destrs ->
+      let (def, tmpr_zero) = fresh_reg def in
+      let (srcrs1, srcrs2) = pad_with tmpr_zero srcrs1 srcrs2 in
+      let init =
+        [RTL.St_move (tmpr_zero, RTL.Imm 0, start_lbl) ;
+         RTL.St_clear_carry start_lbl] in
+      let f srcr1 srcr2 =
+        RTL.St_op2 (I8051.Sub, destr, srcr1, RTL.Reg srcr2, start_lbl) in
+      (* not interested in result, just the carry bit
+         the following is safe even if destrs = srcrsi *)
+      let iter_sub = List.map2 f srcrs1 srcrs2 in
+      let extract_carry =
+        [RTL.St_op2 (I8051.Addc, destr, tmpr_zero,
+                     RTL.Reg tmpr_zero, start_lbl)] in
+      let epilogue = translate_cst (AST.Cst_int 0) destrs in
+      add_translates [adds_graph (init @ iter_sub @ extract_carry);
+                      epilogue] start_lbl dest_lbl def
+
+let rec add_128_to_last
+    (tmp_128 : Register.t)
+    (last_subst : Register.t)
+    (rs : Register.t list)
+    (dummy_lbl : Label.t) = match rs with
+  | [] -> ([], adds_graph [])
+  | [last] ->
+    let insts =
+      [RTL.St_move (last_subst, RTL.Reg last, dummy_lbl) ;
+       RTL.St_op2 (I8051.Add, last_subst, last_subst,
+                   RTL.Reg tmp_128, dummy_lbl)] in
+    ([last_subst], adds_graph insts)
+  | hd :: tail ->
+    let (tail', trans) = add_128_to_last tmp_128 last_subst tail dummy_lbl in
+    (hd :: tail', trans)
+
+(* what happens if srcrs1 and srcrs2 have different length? seems to me
+   128 is added at the wrong place then *)
 let translate_lts destrs srcrs1 srcrs2 start_lbl dest_lbl def =
-  let (def, tmp_srcrs1) = fresh_regs def (List.length srcrs1) in
-  let (def, tmp_srcrs2) = fresh_regs def (List.length srcrs2) in
+  let (def, tmp_last_srcr1) = fresh_reg def in
+  let (def, tmp_last_srcr2) = fresh_reg def in
   let (def, tmp_128) = fresh_reg def in
+  (* I save just the last registers *)
+  let (srcrs1, add_128_to_srcrs1) =
+    add_128_to_last tmp_128 tmp_last_srcr1 srcrs1 start_lbl in
+  let (srcrs2, add_128_to_srcrs2) =
+    add_128_to_last tmp_128 tmp_last_srcr2 srcrs2 start_lbl in
   add_translates
-    [translate_move tmp_srcrs1 srcrs1 ;
-     translate_move tmp_srcrs2 srcrs2 ;
-     adds_graph [RTL.St_int (tmp_128, 128, start_lbl)] ;
-     add_128_to_last tmp_128 tmp_srcrs1 ;
-     add_128_to_last tmp_128 tmp_srcrs2 ;
-     translate_lt destrs tmp_srcrs1 tmp_srcrs2]
+    [adds_graph [RTL.St_move (tmp_128, RTL.Imm 128, start_lbl)] ;
+     add_128_to_srcrs1;
+     add_128_to_srcrs2;
+     translate_ltu destrs srcrs1 srcrs2]
     start_lbl dest_lbl def
 
 
-let rec translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
+let translate_op2 op2 destrs srcrs1 srcrs2 start_lbl dest_lbl def =
   match op2 with
 
@@ -569 +637 @@
     | AST.Op_cmpp AST.Cmp_eq ->
       add_translates
-        [translate_op2 (AST.Op_cmpu AST.Cmp_ne) destrs srcrs1 srcrs2 ;
-         translate_op1 AST.Op_notbool destrs destrs]
-        start_lbl dest_lbl def
+        [translate_ne destrs srcrs1 srcrs2 ;
+         translate_toggle_bool destrs] start_lbl dest_lbl def
 
     | AST.Op_cmp AST.Cmp_ne
@@ -582 +649 @@
 
     | AST.Op_cmpu AST.Cmp_lt | AST.Op_cmpp AST.Cmp_lt ->
-      translate_lt destrs srcrs1 srcrs2 start_lbl dest_lbl def
+      translate_ltu destrs srcrs1 srcrs2 start_lbl dest_lbl def
 
     | AST.Op_cmp AST.Cmp_le ->
       add_translates
-        [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
-         translate_op1 AST.Op_notbool destrs destrs]
-        start_lbl dest_lbl def
-
-    | AST.Op_cmpu AST.Cmp_le ->
+        [translate_lts destrs srcrs2 srcrs1 ;
+         translate_toggle_bool destrs] start_lbl dest_lbl def
+
+    | AST.Op_cmpu AST.Cmp_le | AST.Op_cmpp AST.Cmp_le ->
       add_translates
-        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs2 srcrs1 ;
-         translate_op1 AST.Op_notbool destrs destrs]
-        start_lbl dest_lbl def
-
-    | AST.Op_cmpp AST.Cmp_le ->
-      add_translates
-        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs2 srcrs1 ;
-         translate_op1 AST.Op_notbool destrs destrs]
-        start_lbl dest_lbl def
+        [translate_ltu destrs srcrs2 srcrs1 ;
+         translate_toggle_bool destrs] start_lbl dest_lbl def
 
     | AST.Op_cmp AST.Cmp_gt ->
-      translate_op2 (AST.Op_cmp AST.Cmp_lt)
-        destrs srcrs2 srcrs1 start_lbl dest_lbl def
-
-    | AST.Op_cmpu AST.Cmp_gt ->
-      translate_op2 (AST.Op_cmpu AST.Cmp_lt)
-        destrs srcrs2 srcrs1 start_lbl dest_lbl def
-
-    | AST.Op_cmpp AST.Cmp_gt ->
-      translate_op2 (AST.Op_cmpp AST.Cmp_lt)
-        destrs srcrs2 srcrs1 start_lbl dest_lbl def
+      translate_lts destrs srcrs2 srcrs1 start_lbl dest_lbl def
+
+    | AST.Op_cmpu AST.Cmp_gt | AST.Op_cmpp AST.Cmp_gt ->
+      translate_ltu destrs srcrs2 srcrs1 start_lbl dest_lbl def
 
     | AST.Op_cmp AST.Cmp_ge ->
       add_translates
-        [translate_op2 (AST.Op_cmp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
-         translate_op1 AST.Op_notbool destrs destrs]
-        start_lbl dest_lbl def
-
-    | AST.Op_cmpu AST.Cmp_ge ->
+        [translate_lts destrs srcrs1 srcrs2 ;
+         translate_toggle_bool destrs] start_lbl dest_lbl def
+
+    | AST.Op_cmpu AST.Cmp_ge | AST.Op_cmpp AST.Cmp_ge ->
       add_translates
-        [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ;
-         translate_op1 AST.Op_notbool destrs destrs]
-        start_lbl dest_lbl def
-
-    | AST.Op_cmpp AST.Cmp_ge ->
-      add_translates
-        [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ;
-         translate_op1 AST.Op_notbool destrs destrs]
-        start_lbl dest_lbl def
+        [translate_ltu destrs srcrs1 srcrs2 ;
+         translate_toggle_bool destrs] start_lbl dest_lbl def
 
     | AST.Op_div | AST.Op_divu | AST.Op_modu | AST.Op_mod | AST.Op_shl
@@ -639 +684 @@
 
 let translate_cond srcrs start_lbl lbl_true lbl_false def =
-  let (def, tmpr) = fresh_reg def in
-  let tmp_lbl = fresh_label def in
-  let init = RTL.St_int (tmpr, 0, start_lbl) in
-  let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, srcr, start_lbl) in
-  let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
-  add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
+  match srcrs with
+    | [] -> add_graph start_lbl (RTL.St_skip lbl_false) def
+    | srcr :: srcrs ->
+      let (def, tmpr) = fresh_reg def in
+      let tmp_lbl = fresh_label def in
+      let init = RTL.St_move (tmpr, RTL.Reg srcr, start_lbl) in
+      let f srcr = RTL.St_op2 (I8051.Or, tmpr, tmpr, RTL.Reg srcr, start_lbl) in
+      let def = adds_graph (init :: (List.map f srcrs)) start_lbl tmp_lbl def in
+      add_graph tmp_lbl (RTL.St_cond (tmpr, lbl_true, lbl_false)) def
 
 
@@ -656 +704 @@
     let translates =
       translates @
-        [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
+        [adds_graph [RTL.St_move (tmpr, RTL.Imm off, start_lbl)] ;
          translate_op2 AST.Op_addp tmp_addr save_addr [tmpr] ;
          adds_graph [RTL.St_load (r, tmp_addr1, tmp_addr2, dest_lbl)]] in
@@ -671 +719 @@
     let translates =
       translates @
-        [adds_graph [RTL.St_int (tmpr, off, start_lbl)] ;
+        [adds_graph [RTL.St_move (tmpr, RTL.Imm off, start_lbl)] ;
          translate_op2 AST.Op_addp tmp_addr addr [tmpr] ;
          adds_graph [RTL.St_store (tmp_addr1, tmp_addr2, srcr, dest_lbl)]] in
@@ -747 +795 @@
   | RTLabs.St_return (Some r) ->
     add_graph lbl (RTL.St_return (find_local_env r lenv)) def
-                
+
   | _ -> assert false (*not possible because of previous removal of immediates*)
 

Deliverables/D2.2/8051/src/common/intValue.ml

@@ -66 +66 @@
   val logxor  : t -> t -> t
   val shl     : t -> t -> t
+  val rotl    : t -> t
   val shr     : t -> t -> t
   val shrl    : t -> t -> t
@@ -176 +177 @@
     let pow = power_int_positive_big_int 2 (cast b) in
     cast (mult_big_int a pow)
+
+  let rotl a =
+    if ge_big_int a half_bound then
+      cast (add_big_int (mult_big_int a two) one)
+    else
+      cast (mult_big_int a two)
 
   let shr a b =

Deliverables/D2.2/8051/src/common/intValue.mli

@@ -62 +62 @@
   val logxor  : t -> t -> t
   val shl     : t -> t -> t
+  val rotl    : t -> t
   val shr     : t -> t -> t
   val shrl    : t -> t -> t

Deliverables/D2.2/8051/src/common/memory.ml

@@ -8 +8 @@
 
 let error_prefix = "Memory"
-let error s = Error.global_error error_prefix s
+let error s = invalid_arg (error_prefix ^ s)
 
 

Deliverables/D2.2/8051/src/common/value.ml

@@ -113 +113 @@
   val xor        : t -> t -> t
   val shl        : t -> t -> t
+  val rotl       : t -> t
   val shr        : t -> t -> t
   val shru       : t -> t -> t
@@ -376 +377 @@
   let xor    = binary_int_op ValInt.logxor
   let shl    = binary_int_op ValInt.shl
+  let rotl   = unary_int_op ValInt.rotl
   let shr    = binary_int_op ValInt.shr
   let shru   = binary_int_op ValInt.shrl

Deliverables/D2.2/8051/src/common/value.mli

@@ -105 +105 @@
   val xor        : t -> t -> t
   val shl        : t -> t -> t
+  val rotl       : t -> t
   val shr        : t -> t -> t
   val shru       : t -> t -> t