From 62277541b0ea1c687c64df79a543f776b9f58f29 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 9 Sep 2015 09:47:57 +0200
Subject: Added an builtin for the atomic exchange operation.

The new builtin __builtin_atomic_exchange(int *a, int *b, int *c)
stores *b in *a and sets *c to the old value of *a.
---
 powerpc/Asmexpand.ml | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 3fffc037..749d5afd 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -64,7 +64,7 @@ let expand_annot_val txt targ args res =
    Note that lfd and stfd cannot trap on ill-formed floats. *)
 
 let offset_in_range ofs =
-  Int.eq (Asmgen.high_s ofs) Int.zero
+  Int.eq (Asmgen.high_s ofs) _0
 
 let memcpy_small_arg sz arg tmp =
   match arg with
@@ -276,9 +276,9 @@ let expand_builtin_vstore chunk args =
       assert false
 
 (* Handling of varargs *)
-let linkregister_offset = ref  Int.zero
+let linkregister_offset = ref  _0
 
-let retaddr_offset = ref Int.zero
+let retaddr_offset = ref _0
 
 let current_function_stacksize = ref 0l
 
@@ -485,8 +485,19 @@ let expand_builtin_inline name args res =
       emit (Plwz (res, Cint! retaddr_offset,GPR1))
   (* isel *)
   | "__builtin_isel", [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) ->
-      emit (Pcmpwi (a1,Cint (Int.zero)));
+      emit (Pcmpwi (a1,Cint (_0)));
       emit (Pisel (res,a3,a2,CRbit_2))
+  (* atomic operations *)
+  | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ ->
+      emit (Plwz (GPR10,Cint _0,a2));
+      emit (Psync);
+      let lbl = new_label() in
+      emit (Plabel lbl);
+      emit (Plwarx (GPR11,GPR0,a1));
+      emit (Pstwcx_ (GPR10,GPR0,a1));
+      emit (Pbne lbl);
+      emit (Pisync);
+      emit (Pstw (GPR11,Cint _0,a3))
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
@@ -517,7 +528,7 @@ let expand_instruction instr =
   | Pallocframe(sz, ofs,retofs) ->
       let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in
       let sz = camlint_of_coqint sz in
-      assert (ofs = Int.zero);
+      assert (ofs = _0);
       let sz = if variadic then Int32.add sz 96l else sz in
       let adj = Int32.neg sz in
       if adj >= -0x8000l then
-- 
cgit 


From 2dce91b8e2cae0b49c8870df6c727e25aaa180d8 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 9 Sep 2015 15:36:34 +0200
Subject: Add builtin for atomic load.

Implement the new __builtin_atomic_load(int *a, int *b); which stores
*a in *b. This differs from the atomic_load of the GCC, since the PPC
ISA manual states that you must jump before the load again if it fails.
---
 powerpc/Asmexpand.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 749d5afd..c6bda75c 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -498,6 +498,15 @@ let expand_builtin_inline name args res =
       emit (Pbne lbl);
       emit (Pisync);
       emit (Pstw (GPR11,Cint _0,a3))
+  | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ ->
+      let lbl = new_label() in
+      emit (Psync);
+      emit (Plabel lbl);
+      emit (Plwz (a1,Cint _0,a1));
+      emit (Pcmpw (a1,a1));
+      emit (Pbne lbl);
+      emit (Pisync);
+      emit (Pstw (a1,Cint _0, a2));
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
-- 
cgit 


From 41655f6c8d38270cc50407b0141b443f6ee90100 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 10 Sep 2015 10:20:15 +0200
Subject: Added builtin for atomic compare and exchange.

The new __builtin_atomic_compare_exchange(int *ptr,int *exp,int *dsr);
writes dsr into ptr if ptr is equal to exp and returns true if
ptr is not equal to exp it writes ptr into exp and returns false.
---
 powerpc/Asmexpand.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index beaef42f..8cd123fe 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -527,7 +527,7 @@ let expand_builtin_inline name args res =
       and lblneq = new_label ()
       and lblsucc = new_label () in      
       emit (Plwz (GPR10,Cint _0,exp));
-      emit (Plwz (GPR11,Cint _0,exp));
+      emit (Plwz (GPR11,Cint _0,des));
       emit (Psync);
       emit (Plabel lbls);
       emit (Plwarx (GPR12,GPR0,dst));
-- 
cgit 


From 0de3d126e70dfedfd6f74710da31c4b9636f900a Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 11 Sep 2015 12:05:31 +0200
Subject: Use the gcc version of atomic load.

---
 powerpc/Asmexpand.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 8cd123fe..5e26e8a6 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -499,12 +499,10 @@ let expand_builtin_inline name args res =
       emit (Pisync);
       emit (Pstw (GPR11,Cint _0,a3))
   | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ ->
-      let lbl = new_label() in
       emit (Psync);
-      emit (Plabel lbl);
       emit (Plwz (a1,Cint _0,a1));
       emit (Pcmpw (a1,a1));
-      emit (Pbne lbl);
+      emit (Pbne_rel _4);
       emit (Pisync);
       emit (Pstw (a1,Cint _0, a2));
   | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
-- 
cgit 


From 9dc0dd73f75875b301c886df40087192d0fad386 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 14 Sep 2015 19:41:39 +0200
Subject: Use fix registers for atomic builtins.

In order to avoid clashes during register allocation etc. The
builtins now use fixed registers and mark additional registers as
destroyed for temporaries.
---
 powerpc/Asmexpand.ml | 42 +++++++++++++++++++++++++++++++++---------
 1 file changed, 33 insertions(+), 9 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 5e26e8a6..23c66382 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -506,20 +506,23 @@ let expand_builtin_inline name args res =
       emit (Pisync);
       emit (Pstw (a1,Cint _0, a2));
   | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
-      let tmpres = if a1 = res then
-        GPR11 
-      else
-        res in
       let lbl = new_label() in
       emit (Psync);
       emit (Plabel lbl);
-      emit (Plwarx (tmpres,GPR0,a1));
-      emit (Padd (a2,tmpres,a2));
-      emit (Pstwcx_ (a2,GPR0,a1));
+      emit (Plwarx (res,GPR0,a1));
+      emit (Padd (GPR10,res,a2));
+      emit (Pstwcx_ (GPR10,GPR0,a1));
+      emit (Pbne lbl);
+      emit (Pisync);
+  | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR_none ->
+      let lbl = new_label() in
+      emit (Psync);
+      emit (Plabel lbl);
+      emit (Plwarx (GPR3,GPR0,a1));
+      emit (Padd (GPR10,GPR3,a2));
+      emit (Pstwcx_ (GPR10,GPR0,a1));
       emit (Pbne lbl);
       emit (Pisync);
-      if (tmpres <> res) then
-        emit (Pmr (res,tmpres))
   | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR (IR res) ->
       let lbls = new_label ()
       and lblneq = new_label ()
@@ -542,6 +545,27 @@ let expand_builtin_inline name args res =
       emit (Pstw (GPR12,(Cint _0),exp));
       emit (Plabel lblsucc);
       emit (Pmr (res,dst));
+  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR_none ->
+      let lbls = new_label ()
+      and lblneq = new_label ()
+      and lblsucc = new_label () in      
+      emit (Plwz (GPR10,Cint _0,exp));
+      emit (Plwz (GPR11,Cint _0,des));
+      emit (Psync);
+      emit (Plabel lbls);
+      emit (Plwarx (GPR12,GPR0,dst));
+      emit (Pcmpw (GPR12,GPR10));
+      emit (Pbne lblneq);
+      emit (Pstwcx_ (GPR11,GPR0,dst));
+      emit (Pbne lbls);
+      emit (Plabel lblneq);
+      emit (Pisync);
+      emit (Pmfcr dst);
+      emit (Prlwinm (dst,dst,(Z.of_uint 3),_1));
+      emit (Pcmpwi (dst,(Cint _0)));
+      emit (Pbne lblsucc);
+      emit (Pstw (GPR12,(Cint _0),exp));
+      emit (Plabel lblsucc);
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
-- 
cgit 


From fb9578680d1cd88650e7e6aa9bf1e1ffd8b32f49 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 15 Sep 2015 12:32:09 +0200
Subject: Removed usage of bne and removed duplicated code for return values of
 atomics.

Instead of introducing a new bne instruction in Asm.v and the TargetPrinter.ml
I use the equivalent bf instruction. The duplicated code is due to unused return
values of builtins. Now we only emit the additional code for the return value if
the return value is used instead of duplicating the whole emiting sequence.
---
 powerpc/Asmexpand.ml | 58 +++++++++++++++++-----------------------------------
 1 file changed, 19 insertions(+), 39 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 23c66382..098eb49d 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -495,57 +495,32 @@ let expand_builtin_inline name args res =
       emit (Plabel lbl);
       emit (Plwarx (GPR11,GPR0,a1));
       emit (Pstwcx_ (GPR10,GPR0,a1));
-      emit (Pbne lbl);
+      emit (Pbf (CRbit_2,lbl));
       emit (Pisync);
       emit (Pstw (GPR11,Cint _0,a3))
   | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ ->
+      let lbl = new_label () in
       emit (Psync);
       emit (Plwz (a1,Cint _0,a1));
       emit (Pcmpw (a1,a1));
-      emit (Pbne_rel _4);
+      emit (Pbf (CRbit_2,lbl));
+      emit (Plabel lbl);
       emit (Pisync);
       emit (Pstw (a1,Cint _0, a2));
-  | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
+  | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], res ->
       let lbl = new_label() in
+      let res = (match res with
+      | BR (IR res) -> res
+      | BR_none -> GPR3
+      | _ ->   raise (Error ("unrecognized builtin " ^ name))) in
       emit (Psync);
       emit (Plabel lbl);
       emit (Plwarx (res,GPR0,a1));
       emit (Padd (GPR10,res,a2));
       emit (Pstwcx_ (GPR10,GPR0,a1));
-      emit (Pbne lbl);
-      emit (Pisync);
-  | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR_none ->
-      let lbl = new_label() in
-      emit (Psync);
-      emit (Plabel lbl);
-      emit (Plwarx (GPR3,GPR0,a1));
-      emit (Padd (GPR10,GPR3,a2));
-      emit (Pstwcx_ (GPR10,GPR0,a1));
-      emit (Pbne lbl);
+      emit (Pbf (CRbit_2, lbl));
       emit (Pisync);
-  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR (IR res) ->
-      let lbls = new_label ()
-      and lblneq = new_label ()
-      and lblsucc = new_label () in      
-      emit (Plwz (GPR10,Cint _0,exp));
-      emit (Plwz (GPR11,Cint _0,des));
-      emit (Psync);
-      emit (Plabel lbls);
-      emit (Plwarx (GPR12,GPR0,dst));
-      emit (Pcmpw (GPR12,GPR10));
-      emit (Pbne lblneq);
-      emit (Pstwcx_ (GPR11,GPR0,dst));
-      emit (Pbne lbls);
-      emit (Plabel lblneq);
-      emit (Pisync);
-      emit (Pmfcr dst);
-      emit (Prlwinm (dst,dst,(Z.of_uint 3),_1));
-      emit (Pcmpwi (dst,(Cint _0)));
-      emit (Pbne lblsucc);
-      emit (Pstw (GPR12,(Cint _0),exp));
-      emit (Plabel lblsucc);
-      emit (Pmr (res,dst));
-  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR_none ->
+  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], res ->
       let lbls = new_label ()
       and lblneq = new_label ()
       and lblsucc = new_label () in      
@@ -555,17 +530,22 @@ let expand_builtin_inline name args res =
       emit (Plabel lbls);
       emit (Plwarx (GPR12,GPR0,dst));
       emit (Pcmpw (GPR12,GPR10));
-      emit (Pbne lblneq);
+      emit (Pbf (CRbit_2,lblneq));
       emit (Pstwcx_ (GPR11,GPR0,dst));
-      emit (Pbne lbls);
+      emit (Pbf (CRbit_2,lbls));
       emit (Plabel lblneq);
       emit (Pisync);
       emit (Pmfcr dst);
       emit (Prlwinm (dst,dst,(Z.of_uint 3),_1));
       emit (Pcmpwi (dst,(Cint _0)));
-      emit (Pbne lblsucc);
+      emit (Pbf (CRbit_2,lblsucc));
       emit (Pstw (GPR12,(Cint _0),exp));
       emit (Plabel lblsucc);
+      (match res with
+      | BR_none -> ()
+      | BR (IR res) ->
+          emit (Pmr (res,dst))
+      | _ ->raise (Error ("unrecognized builtin " ^ name)))
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
-- 
cgit 


From 435dc0e6fe74f0ab06737360e1dc49b42b95f1e4 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 17 Sep 2015 19:20:57 +0200
Subject: Integrated the fix of commit de40fce9c16ced8d23389cbcfc55ef6d99466fe8
 for the atomics.

---
 powerpc/Asmexpand.ml | 14 +++-----------
 1 file changed, 3 insertions(+), 11 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 098eb49d..702b6a76 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -507,12 +507,8 @@ let expand_builtin_inline name args res =
       emit (Plabel lbl);
       emit (Pisync);
       emit (Pstw (a1,Cint _0, a2));
-  | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], res ->
+  | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
       let lbl = new_label() in
-      let res = (match res with
-      | BR (IR res) -> res
-      | BR_none -> GPR3
-      | _ ->   raise (Error ("unrecognized builtin " ^ name))) in
       emit (Psync);
       emit (Plabel lbl);
       emit (Plwarx (res,GPR0,a1));
@@ -520,7 +516,7 @@ let expand_builtin_inline name args res =
       emit (Pstwcx_ (GPR10,GPR0,a1));
       emit (Pbf (CRbit_2, lbl));
       emit (Pisync);
-  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], res ->
+  | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)],  BR (IR res) ->
       let lbls = new_label ()
       and lblneq = new_label ()
       and lblsucc = new_label () in      
@@ -541,11 +537,7 @@ let expand_builtin_inline name args res =
       emit (Pbf (CRbit_2,lblsucc));
       emit (Pstw (GPR12,(Cint _0),exp));
       emit (Plabel lblsucc);
-      (match res with
-      | BR_none -> ()
-      | BR (IR res) ->
-          emit (Pmr (res,dst))
-      | _ ->raise (Error ("unrecognized builtin " ^ name)))
+      emit (Pmr (res,dst))
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
-- 
cgit 


From 469badb1eb88b187ff39c9847b3b2316225fd421 Mon Sep 17 00:00:00 2001
From: Michael Schmidt <mschmidt@absint.com>
Date: Fri, 18 Sep 2015 12:39:05 +0200
Subject: correct error message for __builtin_dcbtls

---
 powerpc/Asmexpand.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 3fffc037..b9fe1d7f 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -441,7 +441,7 @@ let expand_builtin_inline name args res =
       emit (Picbi(GPR0,a1))
   | "__builtin_dcbtls", [BA (IR a1); BA_int loc],_ ->
       if not ((Int.eq loc _0) || (Int.eq loc _2)) then
-        raise (Error "the second argument of __builtin_dcbtls must be a constant between 0 and 2");
+        raise (Error "the second argument of __builtin_dcbtls must be 0 or 2");
       emit (Pdcbtls (loc,GPR0,a1))    
   | "__builtin_dcbtls",_,_ ->
       raise (Error "the second argument of __builtin_dcbtls must be a constant")
-- 
cgit 


From bc1fbdd0baaab41aa048b3214ec71bb0cc04dfcc Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 21 Sep 2015 16:17:44 +0200
Subject: Applied a few simplification for temporary registers.

---
 powerpc/Asmexpand.ml | 27 ++++++++++++++-------------
 1 file changed, 14 insertions(+), 13 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 702b6a76..9a3804a0 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -493,27 +493,27 @@ let expand_builtin_inline name args res =
       emit (Psync);
       let lbl = new_label() in
       emit (Plabel lbl);
-      emit (Plwarx (GPR11,GPR0,a1));
+      emit (Plwarx (GPR0,GPR0,a1));
       emit (Pstwcx_ (GPR10,GPR0,a1));
       emit (Pbf (CRbit_2,lbl));
       emit (Pisync);
-      emit (Pstw (GPR11,Cint _0,a3))
+      emit (Pstw (GPR0,Cint _0,a3))
   | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ ->
       let lbl = new_label () in
       emit (Psync);
-      emit (Plwz (a1,Cint _0,a1));
-      emit (Pcmpw (a1,a1));
+      emit (Plwz (GPR0,Cint _0,a1));
+      emit (Pcmpw (GPR0,GPR0));
       emit (Pbf (CRbit_2,lbl));
       emit (Plabel lbl);
       emit (Pisync);
-      emit (Pstw (a1,Cint _0, a2));
+      emit (Pstw (GPR0,Cint _0, a2))
   | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) ->
       let lbl = new_label() in
       emit (Psync);
       emit (Plabel lbl);
       emit (Plwarx (res,GPR0,a1));
-      emit (Padd (GPR10,res,a2));
-      emit (Pstwcx_ (GPR10,GPR0,a1));
+      emit (Padd (GPR0,res,a2));
+      emit (Pstwcx_ (GPR0,GPR0,a1));
       emit (Pbf (CRbit_2, lbl));
       emit (Pisync);
   | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)],  BR (IR res) ->
@@ -524,18 +524,19 @@ let expand_builtin_inline name args res =
       emit (Plwz (GPR11,Cint _0,des));
       emit (Psync);
       emit (Plabel lbls);
-      emit (Plwarx (GPR12,GPR0,dst));
-      emit (Pcmpw (GPR12,GPR10));
+      emit (Plwarx (GPR0,GPR0,dst));
+      emit (Pcmpw (GPR0,GPR10));
       emit (Pbf (CRbit_2,lblneq));
       emit (Pstwcx_ (GPR11,GPR0,dst));
       emit (Pbf (CRbit_2,lbls));
       emit (Plabel lblneq);
+      (* Here, CR2 is true if the exchange succeeded, false if it failed *)
       emit (Pisync);
       emit (Pmfcr dst);
-      emit (Prlwinm (dst,dst,(Z.of_uint 3),_1));
-      emit (Pcmpwi (dst,(Cint _0)));
-      emit (Pbf (CRbit_2,lblsucc));
-      emit (Pstw (GPR12,(Cint _0),exp));
+      emit (Prlwinm (res,res,(Z.of_uint 3),_1));
+      (* Update exp with the current value of dst if the exchange failed *)
+      emit (Pbt (CRbit_2,lblsucc));
+      emit (Pstw (GPR0,Cint _0,exp));
       emit (Plabel lblsucc);
       emit (Pmr (res,dst))
   (* Catch-all *)
-- 
cgit 


From 3174d685154a1e0febf305d305fc79422a1adcd3 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 21 Sep 2015 17:49:22 +0200
Subject: Removed unnecessary move register and use the correct register as
 base value for the rlwinm.

---
 powerpc/Asmexpand.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 9a3804a0..23704feb 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -533,12 +533,11 @@ let expand_builtin_inline name args res =
       (* Here, CR2 is true if the exchange succeeded, false if it failed *)
       emit (Pisync);
       emit (Pmfcr dst);
-      emit (Prlwinm (res,res,(Z.of_uint 3),_1));
+      emit (Prlwinm (res,dest,(Z.of_uint 3),_1));
       (* Update exp with the current value of dst if the exchange failed *)
       emit (Pbt (CRbit_2,lblsucc));
       emit (Pstw (GPR0,Cint _0,exp));
-      emit (Plabel lblsucc);
-      emit (Pmr (res,dst))
+      emit (Plabel lblsucc)
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
-- 
cgit 


From a972e8ecbc011a48201279f446218676c15126ef Mon Sep 17 00:00:00 2001
From: Michael Schmidt <github@mschmidt.me>
Date: Tue, 22 Sep 2015 11:08:38 +0200
Subject: Fix typo dest -> dst

---
 powerpc/Asmexpand.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 1b9740b9..0dfebc13 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -41,7 +41,7 @@ let emit_addimm rd rs n =
   List.iter emit (Asmgen.addimm rd rs n [])
 
 
-			    
+
 (* Handling of annotations *)
 
 let expand_annot_val txt targ args res =
@@ -79,7 +79,7 @@ let memcpy_small_arg sz arg tmp =
       assert false
 
 let expand_builtin_memcpy_small sz al src dst =
-  let (tsrc, tdst) = 
+  let (tsrc, tdst) =
     if dst <> BA (IR GPR11) then (GPR11, GPR12) else (GPR12, GPR11) in
   let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
   let (rdst, odst) = memcpy_small_arg sz dst tdst in
@@ -117,7 +117,7 @@ let expand_builtin_memcpy_big sz al src dst =
   assert (sz >= 4);
   emit_loadimm GPR0 (Z.of_uint (sz / 4));
   emit (Pmtctr GPR0);
-  let (s, d) = 
+  let (s, d) =
     if dst <> BA (IR GPR11) then (GPR11, GPR12) else (GPR12, GPR11) in
   memcpy_big_arg src s;
   memcpy_big_arg dst d;
@@ -185,7 +185,7 @@ let rec expand_builtin_vload_common chunk base offset res =
             emit (Plwz(lo, offset', base));
             emit (Plwz(hi, offset, base))
           end
-      | None ->      
+      | None ->
           emit (Paddi(GPR11, base, offset));
           expand_builtin_vload_common chunk GPR11 (Cint _0) res
       end
@@ -239,7 +239,7 @@ let expand_builtin_vstore_common chunk base offset src =
       | Some offset' ->
           emit (Pstw(hi, offset, base));
           emit (Pstw(lo, offset', base))
-      | None ->      
+      | None ->
           let tmp = temp_for_vstore src in
           emit (Paddi(tmp, base, offset));
           emit (Pstw(hi, Cint _0, tmp));
@@ -442,7 +442,7 @@ let expand_builtin_inline name args res =
   | "__builtin_dcbtls", [BA (IR a1); BA_int loc],_ ->
       if not ((Int.eq loc _0) || (Int.eq loc _2)) then
         raise (Error "the second argument of __builtin_dcbtls must be 0 or 2");
-      emit (Pdcbtls (loc,GPR0,a1))    
+      emit (Pdcbtls (loc,GPR0,a1))
   | "__builtin_dcbtls",_,_ ->
       raise (Error "the second argument of __builtin_dcbtls must be a constant")
   | "__builtin_icbtls", [BA (IR a1); BA_int loc],_ ->
@@ -475,7 +475,7 @@ let expand_builtin_inline name args res =
       raise (Error "the first argument of __builtin_set_spr must be a constant")
   (* Frame and return address *)
   | "__builtin_call_frame", _,BR (IR res) ->
-      let sz = !current_function_stacksize 
+      let sz = !current_function_stacksize
       and ofs = !linkregister_offset in
       if sz < 0x8000l then
         emit (Paddi(res, GPR1, Cint(coqint_of_camlint sz)))
@@ -519,7 +519,7 @@ let expand_builtin_inline name args res =
   | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)],  BR (IR res) ->
       let lbls = new_label ()
       and lblneq = new_label ()
-      and lblsucc = new_label () in      
+      and lblsucc = new_label () in
       emit (Plwz (GPR10,Cint _0,exp));
       emit (Plwz (GPR11,Cint _0,des));
       emit (Psync);
@@ -533,7 +533,7 @@ let expand_builtin_inline name args res =
       (* Here, CR2 is true if the exchange succeeded, false if it failed *)
       emit (Pisync);
       emit (Pmfcr dst);
-      emit (Prlwinm (res,dest,(Z.of_uint 3),_1));
+      emit (Prlwinm (res,dst,(Z.of_uint 3),_1));
       (* Update exp with the current value of dst if the exchange failed *)
       emit (Pbt (CRbit_2,lblsucc));
       emit (Pstw (GPR0,Cint _0,exp));
-- 
cgit 


From c212ab7a8adea516db72f17d818393629dbde1b3 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Tue, 22 Sep 2015 13:25:57 +0200
Subject: Use R10 in atomic compare and exchange for the rlwinm.

---
 powerpc/Asmexpand.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 0dfebc13..fc0fc44e 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -532,8 +532,8 @@ let expand_builtin_inline name args res =
       emit (Plabel lblneq);
       (* Here, CR2 is true if the exchange succeeded, false if it failed *)
       emit (Pisync);
-      emit (Pmfcr dst);
-      emit (Prlwinm (res,dst,(Z.of_uint 3),_1));
+      emit (Pmfcr GPR10);
+      emit (Prlwinm (res,GPR10,(Z.of_uint 3),_1));
       (* Update exp with the current value of dst if the exchange failed *)
       emit (Pbt (CRbit_2,lblsucc));
       emit (Pstw (GPR0,Cint _0,exp));
-- 
cgit 


From fc8afb9287ab7b1607e5a7d2a03b0078fd9867d0 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 24 Sep 2015 20:11:48 +0200
Subject: Added placing labels for live ranges etc.

In order to avoid the usage of too many labels we replace the
debug statements during the Asmexpand phase.
---
 powerpc/Asmexpand.ml | 109 ++++++++++++++++++++++++++++++++++++++++++++++++---
 1 file changed, 103 insertions(+), 6 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index b9fe1d7f..d4675e5f 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -512,7 +512,7 @@ let num_crbit = function
   | CRbit_3 -> 3
   | CRbit_6 -> 6
 
-let expand_instruction instr =
+let expand_instruction_simple instr =
   match instr with
   | Pallocframe(sz, ofs,retofs) ->
       let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in
@@ -586,22 +586,119 @@ let expand_instruction instr =
   | _ ->
       emit instr
 
-let expand_function fn =
+let preg_to_string p =
+  ""
+
+let rec translate_annot a =
+  match a with
+  | BA x -> BA (preg_to_string x)
+  | BA_int n -> BA_int n
+  | BA_long n -> BA_long n
+  | BA_float n -> BA_float n
+  | BA_single n -> BA_single n
+  | BA_loadstack (chunk,ofs) -> BA_loadstack (chunk,ofs)
+  | BA_addrstack ofs -> BA_addrstack ofs
+  | BA_loadglobal (chunk,id,ofs) -> BA_loadglobal (chunk,id,ofs) 
+  | BA_addrglobal (id,ofs) -> BA_addrglobal  (id,ofs)
+  | BA_splitlong (hi,lo) -> BA_splitlong (translate_annot hi,translate_annot lo)
+
+let expand_stack_loc txt = function
+  | [a] -> Debug.stack_variable txt (translate_annot a)
+  | _ -> assert false
+
+let expand_start_live_range txt lbl = function
+  | [a] -> Debug.start_live_range txt lbl (translate_annot a)
+  | _ -> assert false
+
+let expand_end_live_range =
+  Debug.end_live_range
+
+let expand_scope id lbl oldscopes newscopes =
+  let opening = List.filter (fun a -> List.mem a oldscopes) newscopes
+  and closing = List.filter (fun a -> List.mem a newscopes) oldscopes in
+  List.iter (fun i -> Debug.open_scope id i lbl) opening;
+  List.iter (fun i -> Debug.close_scope id i lbl) closing
+
+let expand_instruction id l =
+  let get_lbl = function
+    | None -> 
+        let lbl = new_label () in
+        emit (Plabel lbl);
+        lbl
+    | Some lbl -> lbl in
+  let rec aux lbl scopes = function
+    | [] -> ()
+    | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
+        let kind = (P.to_int kind) in
+        begin
+          match kind with
+          | 1 -> 
+              emit i; aux lbl scopes rest
+          | 2 ->
+              aux  lbl scopes rest
+          | 3 ->
+              let lbl = get_lbl lbl in
+              expand_start_live_range txt lbl args;
+              aux (Some lbl) scopes rest
+          | 4 ->
+              let lbl = get_lbl lbl in
+              expand_end_live_range txt lbl;
+              aux (Some lbl) scopes rest
+          | 5 -> 
+              expand_stack_loc txt args;
+              aux lbl scopes rest
+          | 6 ->
+              let lbl = get_lbl lbl in
+              let scopes' = List.map (function BA_int x -> Int32.to_int (camlint_of_coqint x) | _ -> assert false) args in
+              expand_scope id lbl scopes scopes';
+              aux (Some lbl) scopes' rest
+          | _ ->
+              emit i; aux None scopes rest
+        end
+    | i::rest -> expand_instruction_simple i; aux None scopes rest in
+  aux None [] l
+      
+
+let expand_function id fn =
   try
     set_current_function fn;
-    List.iter expand_instruction fn.fn_code;
+    if !Clflags.option_g then
+      expand_instruction id fn.fn_code
+    else
+      List.iter expand_instruction_simple fn.fn_code;
     Errors.OK (get_current_function ())
   with Error s ->
     Errors.Error (Errors.msg (coqstring_of_camlstring s))
 
-let expand_fundef = function
+let expand_fundef id = function
   | Internal f ->
-      begin match expand_function f with
+      begin match expand_function id f with
       | Errors.OK tf -> Errors.OK (Internal tf)
       | Errors.Error msg -> Errors.Error msg
       end
   | External ef ->
       Errors.OK (External ef)
 
+let rec transform_partial_prog transfun p =
+  match p with
+  | [] -> Errors.OK []
+  | (id,Gvar v)::l ->
+      (match transform_partial_prog transfun l with
+      | Errors.OK x -> Errors.OK ((id,Gvar v)::x)
+      | Errors.Error msg -> Errors.Error msg)
+  | (id,Gfun f)::l ->
+      (match transfun id f with
+      | Errors.OK tf ->
+          (match transform_partial_prog transfun l with
+          | Errors.OK x -> Errors.OK ((id,Gfun tf)::x)
+          | Errors.Error msg -> Errors.Error msg)
+      | Errors.Error msg ->
+          Errors.Error ((Errors.MSG (coqstring_of_camlstring "In function"))::((Errors.CTX
+          id) :: (Errors.MSG (coqstring_of_camlstring ": ") :: msg))))
+
 let expand_program (p: Asm.program) : Asm.program Errors.res =
-  AST.transform_partial_program expand_fundef p
+  match transform_partial_prog expand_fundef p.prog_defs with
+  | Errors.OK x-> 
+      Errors.OK { prog_defs = x; prog_public = p.prog_public; prog_main =
+      p.prog_main }
+  | Errors.Error msg -> Errors.Error msg
-- 
cgit 


From aff813685455559f6d6a88158dd3d605893ba3a3 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 25 Sep 2015 16:43:18 +0200
Subject: Added support for the locations of stack allocated local variables.

This commit adds furher support for location information for local
variables and starts with the implementation of the debug_loc section.
---
 powerpc/Asmexpand.ml | 112 +++++++++++++++++++++++++++++++++------------------
 1 file changed, 72 insertions(+), 40 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index d4675e5f..d44f709e 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -586,36 +586,57 @@ let expand_instruction_simple instr =
   | _ ->
       emit instr
 
-let preg_to_string p =
-  ""
-
-let rec translate_annot a =
-  match a with
-  | BA x -> BA (preg_to_string x)
-  | BA_int n -> BA_int n
-  | BA_long n -> BA_long n
-  | BA_float n -> BA_float n
-  | BA_single n -> BA_single n
-  | BA_loadstack (chunk,ofs) -> BA_loadstack (chunk,ofs)
-  | BA_addrstack ofs -> BA_addrstack ofs
-  | BA_loadglobal (chunk,id,ofs) -> BA_loadglobal (chunk,id,ofs) 
-  | BA_addrglobal (id,ofs) -> BA_addrglobal  (id,ofs)
-  | BA_splitlong (hi,lo) -> BA_splitlong (translate_annot hi,translate_annot lo)
-
-let expand_stack_loc txt = function
-  | [a] -> Debug.stack_variable txt (translate_annot a)
-  | _ -> assert false
-
-let expand_start_live_range txt lbl = function
-  | [a] -> Debug.start_live_range txt lbl (translate_annot a)
-  | _ -> assert false
-
-let expand_end_live_range =
-  Debug.end_live_range
+(* Translate to the integer identifier of the register as
+   the EABI specifies *)
+
+let int_reg_to_dwarf = function
+   | GPR0 -> 0  | GPR1 -> 1  | GPR2 -> 2  | GPR3 -> 3
+   | GPR4 -> 4  | GPR5 -> 5  | GPR6 -> 6  | GPR7 -> 7
+   | GPR8 -> 8  | GPR9 -> 9  | GPR10 -> 10 | GPR11 -> 11
+   | GPR12 -> 12 | GPR13 -> 13 | GPR14 -> 14 | GPR15 -> 15
+   | GPR16 -> 16 | GPR17 -> 17 | GPR18 -> 18 | GPR19 -> 19
+   | GPR20 -> 20 | GPR21 -> 21 | GPR22 -> 22 | GPR23 -> 23
+   | GPR24 -> 24 | GPR25 -> 25 | GPR26 -> 26 | GPR27 -> 27
+   | GPR28 -> 28 | GPR29 -> 29 | GPR30 -> 30 | GPR31 -> 31
+
+let float_reg_to_dwarf = function
+   | FPR0 -> 32  | FPR1 -> 33  | FPR2 -> 34  | FPR3 -> 35
+   | FPR4 -> 36  | FPR5 -> 37  | FPR6 -> 38  | FPR7 -> 39
+   | FPR8 -> 40  | FPR9 -> 41  | FPR10 -> 42 | FPR11 -> 43
+   | FPR12 -> 44 | FPR13 -> 45 | FPR14 -> 46 | FPR15 -> 47
+   | FPR16 -> 48 | FPR17 -> 49 | FPR18 -> 50 | FPR19 -> 51
+   | FPR20 -> 52 | FPR21 -> 53 | FPR22 -> 54| FPR23 -> 55
+   | FPR24 -> 56 | FPR25 -> 57 | FPR26 -> 58 | FPR27 -> 59
+   | FPR28 -> 60 | FPR29 -> 61 | FPR30 -> 62 | FPR31 -> 63
+
+let preg_to_dwarf_int = function
+   | IR r -> int_reg_to_dwarf r
+   | FR r -> float_reg_to_dwarf r
+   | _ -> assert false
+
+
+let translate_annot a =
+  let rec aux = function
+    | BA x -> Some (BA (preg_to_dwarf_int x))
+    | BA_int _
+    | BA_long _
+    | BA_float _
+    | BA_single _
+    | BA_loadglobal _
+    | BA_addrglobal _
+    | BA_loadstack _ -> None
+    | BA_addrstack ofs -> Some (BA_addrstack ofs)
+    | BA_splitlong (hi,lo) -> 
+        begin
+          match (aux hi,aux lo) with
+          | Some hi ,Some lo -> Some (BA_splitlong (hi,lo))
+          | _,_ -> None
+        end in
+  aux (List.hd a)
 
 let expand_scope id lbl oldscopes newscopes =
-  let opening = List.filter (fun a -> List.mem a oldscopes) newscopes
-  and closing = List.filter (fun a -> List.mem a newscopes) oldscopes in
+  let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes
+  and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in
   List.iter (fun i -> Debug.open_scope id i lbl) opening;
   List.iter (fun i -> Debug.close_scope id i lbl) closing
 
@@ -627,31 +648,42 @@ let expand_instruction id l =
         lbl
     | Some lbl -> lbl in
   let rec aux lbl scopes = function
-    | [] -> ()
+    | [] -> let lbl = get_lbl lbl in
+      Debug.function_end id lbl
     | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
         let kind = (P.to_int kind) in
         begin
           match kind with
-          | 1 -> 
-              emit i; aux lbl scopes rest
+          | 1-> 
+              aux lbl scopes rest
           | 2 ->
               aux  lbl scopes rest
           | 3 ->
-              let lbl = get_lbl lbl in
-              expand_start_live_range txt lbl args;
-              aux (Some lbl) scopes rest
+             begin 
+               match translate_annot args with
+               | Some a ->
+                   let lbl = get_lbl lbl in
+                   Debug.start_live_range txt lbl (1,a);
+                   aux (Some lbl) scopes rest
+               | None -> aux lbl scopes rest
+             end
           | 4 ->
               let lbl = get_lbl lbl in
-              expand_end_live_range txt lbl;
+              Debug.end_live_range txt lbl;
               aux (Some lbl) scopes rest
-          | 5 -> 
-              expand_stack_loc txt args;
-              aux lbl scopes rest
-          | 6 ->
+          | 5 ->
+              begin
+                match translate_annot args with
+                | Some a->
+                    Debug.stack_variable txt (1,a);
+                    aux lbl scopes rest
+                | _ -> aux lbl scopes rest
+              end
+          | 6  ->
               let lbl = get_lbl lbl in
               let scopes' = List.map (function BA_int x -> Int32.to_int (camlint_of_coqint x) | _ -> assert false) args in
               expand_scope id lbl scopes scopes';
-              aux (Some lbl) scopes' rest
+              emit i;aux (Some lbl) scopes' rest
           | _ ->
               emit i; aux None scopes rest
         end
-- 
cgit 


From 3e070cae6a316b7e3363c8159096c3bbc4bf21b2 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 25 Sep 2015 21:12:48 +0200
Subject: Added translation of the range lists to location entries.

---
 powerpc/Asmexpand.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index d44f709e..b40a9e53 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -683,7 +683,7 @@ let expand_instruction id l =
               let lbl = get_lbl lbl in
               let scopes' = List.map (function BA_int x -> Int32.to_int (camlint_of_coqint x) | _ -> assert false) args in
               expand_scope id lbl scopes scopes';
-              emit i;aux (Some lbl) scopes' rest
+              aux (Some lbl) scopes' rest
           | _ ->
               emit i; aux None scopes rest
         end
-- 
cgit 


From f2350a3a112950bea11af821754d8f674dda9f9e Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Sun, 27 Sep 2015 20:31:56 +0200
Subject: Added back again the emitting of the debuging annotations for
 debuging purpose.

---
 powerpc/Asmexpand.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index b40a9e53..013d3f0a 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -652,6 +652,7 @@ let expand_instruction id l =
       Debug.function_end id lbl
     | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
         let kind = (P.to_int kind) in
+        emit i;
         begin
           match kind with
           | 1-> 
@@ -665,7 +666,7 @@ let expand_instruction id l =
                    let lbl = get_lbl lbl in
                    Debug.start_live_range txt lbl (1,a);
                    aux (Some lbl) scopes rest
-               | None -> aux lbl scopes rest
+               | None ->  aux lbl scopes rest
              end
           | 4 ->
               let lbl = get_lbl lbl in
@@ -677,7 +678,7 @@ let expand_instruction id l =
                 | Some a->
                     Debug.stack_variable txt (1,a);
                     aux lbl scopes rest
-                | _ -> aux lbl scopes rest
+                | _ ->  aux lbl scopes rest
               end
           | 6  ->
               let lbl = get_lbl lbl in
@@ -685,7 +686,7 @@ let expand_instruction id l =
               expand_scope id lbl scopes scopes';
               aux (Some lbl) scopes' rest
           | _ ->
-              emit i; aux None scopes rest
+              aux None scopes rest
         end
     | i::rest -> expand_instruction_simple i; aux None scopes rest in
   aux None [] l
-- 
cgit 


From 5492b5b55afa68e3d628da07ff583a0cac79b7e3 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 28 Sep 2015 13:36:53 +0200
Subject: Added location for the formal parameters and move the end of all
 scopes before the last statement.

---
 powerpc/Asmexpand.ml | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 013d3f0a..80aa333e 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -647,7 +647,7 @@ let expand_instruction id l =
         emit (Plabel lbl);
         lbl
     | Some lbl -> lbl in
-  let rec aux lbl scopes = function
+  let rec  aux lbl scopes = function
     | [] -> let lbl = get_lbl lbl in
       Debug.function_end id lbl
     | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
@@ -689,7 +689,13 @@ let expand_instruction id l =
               aux None scopes rest
         end
     | i::rest -> expand_instruction_simple i; aux None scopes rest in
-  aux None [] l
+  (* We need to move all closing debug annotations before the last real statement *)
+  let rec move_debug acc = function
+    | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
+        move_debug (i::acc) rest (* Move the debug annotations forward *)
+    | b::rest -> List.rev (b::(List.rev acc)@rest) (* We found the first non debug location *)
+    | [] -> List.rev acc (* This actually can never happen *) in
+  aux None [] (move_debug [] (List.rev l))
       
 
 let expand_function id fn =
-- 
cgit 


From ee76d81e0e7d8a76cd31bf0d01a532d248dca45a Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Wed, 30 Sep 2015 12:43:49 +0200
Subject: Fixed minor issue with parameters that get put on the stack, made the
 code more robust and added indentation for convertCompositeDef

---
 powerpc/Asmexpand.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 80aa333e..050380ae 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -615,7 +615,7 @@ let preg_to_dwarf_int = function
    | _ -> assert false
 
 
-let translate_annot a =
+let translate_annot annot = 
   let rec aux = function
     | BA x -> Some (BA (preg_to_dwarf_int x))
     | BA_int _
@@ -632,7 +632,9 @@ let translate_annot a =
           | Some hi ,Some lo -> Some (BA_splitlong (hi,lo))
           | _,_ -> None
         end in
-  aux (List.hd a)
+  (match annot with
+  | [] -> None
+  | a::_ -> aux a)
 
 let expand_scope id lbl oldscopes newscopes =
   let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes
-- 
cgit 


From 36892f59ced6dd06d6a9cfc6e8af49db8721dd65 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 1 Oct 2015 13:28:14 +0200
Subject: Do not move the line directives.

---
 powerpc/Asmexpand.ml | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 5a365123..efd6cc0d 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -743,12 +743,16 @@ let expand_instruction id l =
         end
     | i::rest -> expand_instruction_simple i; aux None scopes rest in
   (* We need to move all closing debug annotations before the last real statement *)
-  let rec move_debug acc = function
-    | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
-        move_debug (i::acc) rest (* Move the debug annotations forward *)
-    | b::rest -> List.rev (b::(List.rev acc)@rest) (* We found the first non debug location *)
+  let rec move_debug acc bcc = function
+    | (Pbuiltin(EF_debug (kind,_,_),_,_) as i)::rest ->
+        let kind = (P.to_int kind) in
+        if kind = 1 then
+          move_debug acc (i::bcc) rest (* Do not move debug line *)
+        else
+          move_debug (i::acc) bcc rest (* Move the debug annotations forward *)
+    | b::rest -> List.rev ((List.rev (b::bcc)@List.rev acc)@rest) (* We found the first non debug location *)
     | [] -> List.rev acc (* This actually can never happen *) in
-  aux None [] (move_debug [] (List.rev l))
+  aux None [] (move_debug [] [] (List.rev l))
       
 
 let expand_function id fn =
-- 
cgit 


From 886f5550616272d899745d62ec3076fb63a71054 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 1 Oct 2015 14:27:35 +0200
Subject: Use also fucntion id for local variables since atom is not unique.

---
 powerpc/Asmexpand.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index efd6cc0d..16d6326e 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -717,19 +717,19 @@ let expand_instruction id l =
                match translate_annot args with
                | Some a ->
                    let lbl = get_lbl lbl in
-                   Debug.start_live_range txt lbl (1,a);
+                   Debug.start_live_range (id,txt) lbl (1,a);
                    aux (Some lbl) scopes rest
                | None ->  aux lbl scopes rest
              end
           | 4 ->
               let lbl = get_lbl lbl in
-              Debug.end_live_range txt lbl;
+              Debug.end_live_range (id,txt) lbl;
               aux (Some lbl) scopes rest
           | 5 ->
               begin
                 match translate_annot args with
                 | Some a->
-                    Debug.stack_variable txt (1,a);
+                    Debug.stack_variable (id,txt) (1,a);
                     aux lbl scopes rest
                 | _ ->  aux lbl scopes rest
               end
-- 
cgit 


From efd453afac8fcfb741f06166af0379ec8178650f Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 1 Oct 2015 17:09:41 +0200
Subject: Removed the debug output for the debug information.

---
 powerpc/Asmexpand.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 16d6326e..a2cfb136 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -705,11 +705,10 @@ let expand_instruction id l =
       Debug.function_end id lbl
     | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
         let kind = (P.to_int kind) in
-        emit i;
         begin
           match kind with
           | 1-> 
-              aux lbl scopes rest
+              emit i;aux lbl scopes rest
           | 2 ->
               aux  lbl scopes rest
           | 3 ->
-- 
cgit 


From ed1f32134283d3cd4f939a26dfd99992ec48da86 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 8 Oct 2015 13:27:50 +0200
Subject: Moved expandation of debug information to Asmexpandaux.

The function is generalized to work for all backends and takes as
additional arguments functions for the printing of the simple
instructions and the translation function for the arguments.
---
 powerpc/Asmexpand.ml | 71 ++++------------------------------------------------
 1 file changed, 5 insertions(+), 66 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index a2cfb136..878c7e5d 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -668,7 +668,7 @@ let preg_to_dwarf_int = function
 
 let translate_annot annot = 
   let rec aux = function
-    | BA x -> Some (BA (preg_to_dwarf_int x))
+    | BA x -> Some (1,BA (preg_to_dwarf_int x))
     | BA_int _
     | BA_long _
     | BA_float _
@@ -676,11 +676,11 @@ let translate_annot annot =
     | BA_loadglobal _
     | BA_addrglobal _
     | BA_loadstack _ -> None
-    | BA_addrstack ofs -> Some (BA_addrstack ofs)
+    | BA_addrstack ofs -> Some (1,BA_addrstack ofs)
     | BA_splitlong (hi,lo) -> 
         begin
           match (aux hi,aux lo) with
-          | Some hi ,Some lo -> Some (BA_splitlong (hi,lo))
+          | Some (_,hi) ,Some (_,lo) -> Some (1,BA_splitlong (hi,lo))
           | _,_ -> None
         end in
   (match annot with
@@ -692,73 +692,12 @@ let expand_scope id lbl oldscopes newscopes =
   and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in
   List.iter (fun i -> Debug.open_scope id i lbl) opening;
   List.iter (fun i -> Debug.close_scope id i lbl) closing
-
-let expand_instruction id l =
-  let get_lbl = function
-    | None -> 
-        let lbl = new_label () in
-        emit (Plabel lbl);
-        lbl
-    | Some lbl -> lbl in
-  let rec  aux lbl scopes = function
-    | [] -> let lbl = get_lbl lbl in
-      Debug.function_end id lbl
-    | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
-        let kind = (P.to_int kind) in
-        begin
-          match kind with
-          | 1-> 
-              emit i;aux lbl scopes rest
-          | 2 ->
-              aux  lbl scopes rest
-          | 3 ->
-             begin 
-               match translate_annot args with
-               | Some a ->
-                   let lbl = get_lbl lbl in
-                   Debug.start_live_range (id,txt) lbl (1,a);
-                   aux (Some lbl) scopes rest
-               | None ->  aux lbl scopes rest
-             end
-          | 4 ->
-              let lbl = get_lbl lbl in
-              Debug.end_live_range (id,txt) lbl;
-              aux (Some lbl) scopes rest
-          | 5 ->
-              begin
-                match translate_annot args with
-                | Some a->
-                    Debug.stack_variable (id,txt) (1,a);
-                    aux lbl scopes rest
-                | _ ->  aux lbl scopes rest
-              end
-          | 6  ->
-              let lbl = get_lbl lbl in
-              let scopes' = List.map (function BA_int x -> Int32.to_int (camlint_of_coqint x) | _ -> assert false) args in
-              expand_scope id lbl scopes scopes';
-              aux (Some lbl) scopes' rest
-          | _ ->
-              aux None scopes rest
-        end
-    | i::rest -> expand_instruction_simple i; aux None scopes rest in
-  (* We need to move all closing debug annotations before the last real statement *)
-  let rec move_debug acc bcc = function
-    | (Pbuiltin(EF_debug (kind,_,_),_,_) as i)::rest ->
-        let kind = (P.to_int kind) in
-        if kind = 1 then
-          move_debug acc (i::bcc) rest (* Do not move debug line *)
-        else
-          move_debug (i::acc) bcc rest (* Move the debug annotations forward *)
-    | b::rest -> List.rev ((List.rev (b::bcc)@List.rev acc)@rest) (* We found the first non debug location *)
-    | [] -> List.rev acc (* This actually can never happen *) in
-  aux None [] (move_debug [] [] (List.rev l))
-      
-
+    
 let expand_function id fn =
   try
     set_current_function fn;
     if !Clflags.option_g then
-      expand_instruction id fn.fn_code
+      expand_debug id translate_annot expand_instruction_simple fn.fn_code
     else
       List.iter expand_instruction_simple fn.fn_code;
     Errors.OK (get_current_function ())
-- 
cgit 


From f0a5038b4e4220300637d3e9e918d9ec31623108 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Thu, 8 Oct 2015 15:33:47 +0200
Subject: Added versions of the tranform_* functions in AST to work with
 functions taking the ident as argument.

This functions are currently not used inside the proven part but it
is nice to have them already there, when they are used by some future
pass. They also come equiped with the corresponding proofs.
---
 powerpc/Asmexpand.ml | 23 +----------------------
 1 file changed, 1 insertion(+), 22 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 878c7e5d..bf7e4c3e 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -713,26 +713,5 @@ let expand_fundef id = function
   | External ef ->
       Errors.OK (External ef)
 
-let rec transform_partial_prog transfun p =
-  match p with
-  | [] -> Errors.OK []
-  | (id,Gvar v)::l ->
-      (match transform_partial_prog transfun l with
-      | Errors.OK x -> Errors.OK ((id,Gvar v)::x)
-      | Errors.Error msg -> Errors.Error msg)
-  | (id,Gfun f)::l ->
-      (match transfun id f with
-      | Errors.OK tf ->
-          (match transform_partial_prog transfun l with
-          | Errors.OK x -> Errors.OK ((id,Gfun tf)::x)
-          | Errors.Error msg -> Errors.Error msg)
-      | Errors.Error msg ->
-          Errors.Error ((Errors.MSG (coqstring_of_camlstring "In function"))::((Errors.CTX
-          id) :: (Errors.MSG (coqstring_of_camlstring ": ") :: msg))))
-
 let expand_program (p: Asm.program) : Asm.program Errors.res =
-  match transform_partial_prog expand_fundef p.prog_defs with
-  | Errors.OK x-> 
-      Errors.OK { prog_defs = x; prog_public = p.prog_public; prog_main =
-      p.prog_main }
-  | Errors.Error msg -> Errors.Error msg
+  AST.transform_partial_ident_program expand_fundef p
-- 
cgit 


From 0ffd562ae1941e37471ac0c2b8f93bed1de26441 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 9 Oct 2015 11:06:24 +0200
Subject: Filled in the rest of the funciton needed for thte debug info under
 arm.

The name_of_section function no returns the correct name for the
debug sections, the prologue and epilogue directives are added and
the labels for the live ranges are introduced in the Asmexpand pass.
---
 powerpc/Asmexpand.ml | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index bf7e4c3e..fb569a00 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -563,7 +563,7 @@ let num_crbit = function
   | CRbit_3 -> 3
   | CRbit_6 -> 6
 
-let expand_instruction_simple instr =
+let expand_instruction instr =
   match instr with
   | Pallocframe(sz, ofs,retofs) ->
       let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in
@@ -687,19 +687,13 @@ let translate_annot annot =
   | [] -> None
   | a::_ -> aux a)
 
-let expand_scope id lbl oldscopes newscopes =
-  let opening = List.filter (fun a -> not (List.mem a oldscopes)) newscopes
-  and closing = List.filter (fun a -> not (List.mem a newscopes)) oldscopes in
-  List.iter (fun i -> Debug.open_scope id i lbl) opening;
-  List.iter (fun i -> Debug.close_scope id i lbl) closing
-    
 let expand_function id fn =
   try
     set_current_function fn;
     if !Clflags.option_g then
-      expand_debug id translate_annot expand_instruction_simple fn.fn_code
+      expand_debug id translate_annot expand_instruction fn.fn_code
     else
-      List.iter expand_instruction_simple fn.fn_code;
+      List.iter expand_instruction fn.fn_code;
     Errors.OK (get_current_function ())
   with Error s ->
     Errors.Error (Errors.msg (coqstring_of_camlstring s))
-- 
cgit 


From b0c47e12f2bbff0905ad853b90169df16d87f6be Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 9 Oct 2015 16:36:16 +0200
Subject: Filled in missing functions for debug information on ia32.

Like for arm and ppc the functions for section names and start and
end addresses of compilation units are defined and the print_annot
function is moved to Asmexpandaux.ml.
---
 powerpc/Asmexpand.ml | 25 ++-----------------------
 1 file changed, 2 insertions(+), 23 deletions(-)

(limited to 'powerpc/Asmexpand.ml')

diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index fb569a00..00234f9b 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -660,38 +660,17 @@ let float_reg_to_dwarf = function
    | FPR24 -> 56 | FPR25 -> 57 | FPR26 -> 58 | FPR27 -> 59
    | FPR28 -> 60 | FPR29 -> 61 | FPR30 -> 62 | FPR31 -> 63
 
-let preg_to_dwarf_int = function
+let preg_to_dwarf = function
    | IR r -> int_reg_to_dwarf r
    | FR r -> float_reg_to_dwarf r
    | _ -> assert false
 
 
-let translate_annot annot = 
-  let rec aux = function
-    | BA x -> Some (1,BA (preg_to_dwarf_int x))
-    | BA_int _
-    | BA_long _
-    | BA_float _
-    | BA_single _
-    | BA_loadglobal _
-    | BA_addrglobal _
-    | BA_loadstack _ -> None
-    | BA_addrstack ofs -> Some (1,BA_addrstack ofs)
-    | BA_splitlong (hi,lo) -> 
-        begin
-          match (aux hi,aux lo) with
-          | Some (_,hi) ,Some (_,lo) -> Some (1,BA_splitlong (hi,lo))
-          | _,_ -> None
-        end in
-  (match annot with
-  | [] -> None
-  | a::_ -> aux a)
-
 let expand_function id fn =
   try
     set_current_function fn;
     if !Clflags.option_g then
-      expand_debug id translate_annot expand_instruction fn.fn_code
+      expand_debug id 2 preg_to_dwarf expand_instruction fn.fn_code
     else
       List.iter expand_instruction fn.fn_code;
     Errors.OK (get_current_function ())
-- 
cgit