Merge branch 'master' into ppc64

Resolved conflicts in:configure	powerpc/Asmexpand.ml

5 files changed, 207 insertions, 107 deletions

diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index d82b9730..9d480ed5 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -337,9 +337,11 @@ let p_section oc = function
   | Section_string -> fprintf oc "{\"Section Name\":\"String\"}"
   | Section_literal -> fprintf oc "{\"Section Name\":\"Literal\"}"
   | Section_jumptable -> fprintf oc "{\"Section Name\":\"Jumptable\"}"
-  | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":%s,\"Writable\":%B,\"Executable\":%B}" s w e
-  | Section_debug_info 
-  | Section_debug_abbrev -> () (* There should be no info in the debug sections *)
+  | Section_user (s,w,e) -> fprintf oc "{\"Section Name\":\"%s\",\"Writable\":%B,\"Executable\":%B}" s w e
+  | Section_debug_info _
+  | Section_debug_abbrev 
+  | Section_debug_line _
+  | Section_debug_loc -> () (* There should be no info in the debug sections *)
 
 let p_int_opt oc = function
   | None -> fprintf oc "0"
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 49f796ca..9e22e4e0 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -48,7 +48,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 =
@@ -71,7 +71,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
@@ -86,7 +86,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
@@ -124,7 +124,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;
@@ -192,7 +192,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
@@ -246,7 +246,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));
@@ -283,9 +283,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
 
@@ -448,8 +448,8 @@ 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");
-      emit (Pdcbtls (loc,GPR0,a1))    
+        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")
   | "__builtin_icbtls", [BA (IR a1); BA_int loc],_ ->
@@ -482,7 +482,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)))
@@ -510,6 +510,57 @@ let expand_builtin_inline name args res =
         end;
         emit (Por (res, res, GPR0))
       end
+  (* 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 (GPR0,GPR0,a1));
+      emit (Pstwcx_ (GPR10,GPR0,a1));
+      emit (Pbf (CRbit_2,lbl));
+      emit (Pisync);
+      emit (Pstw (GPR0,Cint _0,a3))
+  | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ ->
+      let lbl = new_label () in
+      emit (Psync);
+      emit (Plwz (GPR0,Cint _0,a1));
+      emit (Pcmpw (GPR0,GPR0));
+      emit (Pbf (CRbit_2,lbl));
+      emit (Plabel lbl);
+      emit (Pisync);
+      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 (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) ->
+      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 (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 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));
+      emit (Plabel lblsucc)
   (* Catch-all *)
   | _ ->
       raise (Error ("unrecognized builtin " ^ name))
@@ -540,7 +591,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
@@ -635,17 +686,49 @@ let expand_instruction instr =
   | _ ->
       emit instr
 
-let expand_function fn =
+(* 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 = function
+   | IR r -> int_reg_to_dwarf r
+   | FR r -> float_reg_to_dwarf r
+   | _ -> assert false
+
+
+let expand_function id fn =
   try
     set_current_function fn;
-    List.iter expand_instruction fn.fn_code;
+    if !Clflags.option_g then
+      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 ())
   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
@@ -653,4 +736,4 @@ let expand_fundef = function
       Errors.OK (External ef)
 
 let expand_program (p: Asm.program) : Asm.program Errors.res =
-  AST.transform_partial_program expand_fundef p
+  AST.transform_partial_ident_program expand_fundef p
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 1bb8c6f7..a9e4f5e3 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -118,7 +118,16 @@ let builtins = {
       (TPtr (TVoid [],[]),[],false);
     (* isel *)
     "__builtin_isel",
-      (TInt (IInt, []),[TInt(IBool, []);TInt(IInt, []);TInt(IInt, [])],false)
+      (TInt (IInt, []),[TInt(IBool, []);TInt(IInt, []);TInt(IInt, [])],false);
+    (* atomic operations *)
+    "__builtin_atomic_exchange",
+      (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false);
+    "__builtin_atomic_load",
+      (TVoid [], [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false);
+    "__builtin_atomic_compare_exchange",
+      (TInt (IBool, []), [TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[]);TPtr (TInt(IInt, []),[])],false);
+    "__builtin_sync_fetch_and_add",
+      (TInt (IInt, []),  [TPtr (TInt(IInt, []),[]);TInt(IInt, [])],false);
   ]
 }
 
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index e4006523..20bec532 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -160,9 +160,16 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
       end
   end.
 
+Definition builtin_atomic_exchange := ident_of_string "__builtin_atomic_exchange".
+Definition builtin_sync_and_fetch := ident_of_string "__builtin_sync_fetch_and_add".
+Definition builtin_atomic_compare_exchange := ident_of_string "__builtin_atomic_compare_exchange".
+
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
-  | EF_builtin _ _ => F13 :: nil
+  | EF_builtin id sg =>
+    if ident_eq id builtin_atomic_exchange then R10::nil
+    else if ident_eq id builtin_atomic_compare_exchange then R10::R11::nil
+    else F13 :: nil
   | EF_vload _ => R11 :: nil
   | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil
   | EF_vstore _ => R11 :: R12 :: nil
@@ -183,8 +190,16 @@ Definition temp_for_parent_frame: mreg :=
 Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
   (nil, None).
 
+
 Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (option mreg) :=
-  (nil, nil).
+  match ef with
+    | EF_builtin id sg =>
+      if ident_eq id builtin_atomic_exchange then ((Some R3)::(Some R4)::(Some R5)::nil,nil)
+      else if ident_eq id builtin_sync_and_fetch then ((Some R4)::(Some R5)::nil,(Some R3)::nil)
+      else if ident_eq id builtin_atomic_compare_exchange then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil)
+      else (nil, nil)
+    | _ => (nil, nil)
+  end.
 
 Global Opaque
     destroyed_by_op destroyed_by_load destroyed_by_store
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index bc990de5..250686be 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -13,6 +13,7 @@
 (* Printing PPC assembly code in asm syntax *)
 
 open Printf
+open Fileinfo
 open Datatypes
 open Maps
 open Camlcoq
@@ -39,7 +40,6 @@ module type SYSTEM =
       val cfi_rel_offset: out_channel -> string -> int32 -> unit
       val print_prologue: out_channel -> unit
       val print_epilogue: out_channel -> unit
-      val print_file_loc: out_channel -> DwarfTypes.file_loc -> unit
       val section: out_channel -> section_name -> unit
       val debug_section: out_channel -> section_name -> unit
     end
@@ -72,12 +72,6 @@ let float_reg_name = function
   | FPR24 -> "24" | FPR25 -> "25" | FPR26 -> "26" | FPR27 -> "27"
   | FPR28 -> "28" | FPR29 -> "29" | FPR30 -> "30" | FPR31 -> "31"
 
-let start_addr = ref (-1)
-
-let end_addr = ref (-1)
-
-let stmt_list_addr = ref (-1)
-
 let label = elf_label
 
 module Linux_System : SYSTEM =
@@ -129,9 +123,12 @@ module Linux_System : SYSTEM =
       | Section_user(s, wr, ex) ->
           sprintf ".section	\"%s\",\"a%s%s\",@progbits"
             s (if wr then "w" else "") (if ex then "x" else "")
-      | Section_debug_info -> ".debug_info,\"\",@progbits"
-      | Section_debug_abbrev -> ".debug_abbrev,\"\",@progbits"
-    
+      | Section_debug_info _ -> ".section	.debug_info,\"\",@progbits"
+      | Section_debug_abbrev -> ".section	.debug_abbrev,\"\",@progbits"
+      | Section_debug_loc -> ".section	.debug_loc,\"\",@progbits"
+      | Section_debug_line _ ->  ".section	.debug_line,\"\",@progbits\n"
+
+
     let section oc sec =
       let name = name_of_section sec in
       assert (name <> "COMM");
@@ -150,12 +147,25 @@ module Linux_System : SYSTEM =
               
     let cfi_rel_offset = cfi_rel_offset
 
-    let print_prologue oc = ()
+    let print_prologue oc = 
+      if !Clflags.option_g then  begin
+          section oc Section_text;
+          let low_pc = new_label () in
+          Debug.add_compilation_section_start ".text" low_pc;
+          fprintf oc "%a:\n" label low_pc;
+          fprintf oc "	.cfi_sections	.debug_frame\n"
+        end
 
-    let print_epilogue oc = ()
+    let print_epilogue oc =
+      if !Clflags.option_g then
+        begin
+          let high_pc = new_label () in
+          Debug.add_compilation_section_end ".text" high_pc;
+          Debug.compute_gnu_file_enum (fun f -> ignore (print_file oc f));
+          section oc Section_text;
+          fprintf oc "%a:\n" label high_pc
+        end
 
-    let print_file_loc _ _ = ()
-        
     let debug_section _ _ = ()
   end
     
@@ -207,14 +217,21 @@ module Diab_System : SYSTEM =
             | true, false -> 'd'                (* data *)
             | false, true -> 'c'                (* text *)
             | false, false -> 'r')              (* const *)
-      | Section_debug_info -> ".debug_info,,n"
-      | Section_debug_abbrev -> ".debug_abbrev,,n"
+      | Section_debug_info s -> sprintf ".section	.debug_info%s,,n" (if s <> ".text" then s else "")
+      | Section_debug_abbrev -> ".section	.debug_abbrev,,n"
+      | Section_debug_loc -> ".section	.debug_loc,,n"
+      | Section_debug_line s -> sprintf ".section	.debug_line.%s,,n\n" s
 
     let section oc sec =
       let name = name_of_section sec in
       assert (name <> "COMM");
-      fprintf oc "	%s\n" name
-
+      match sec with
+      | Section_debug_info s ->
+          fprintf oc "	%s\n" name;
+          if s <> ".text" then
+            fprintf oc "	.sectionlink	.debug_info\n"
+      | _ ->
+          fprintf oc "	%s\n" name
 
     let print_file_line oc file line =
       print_file_line_d2 oc comment file line
@@ -227,68 +244,51 @@ module Diab_System : SYSTEM =
     let cfi_adjust oc delta = ()
 
     let cfi_rel_offset oc reg ofs = ()
+
+    let debug_section oc sec =
+      match sec with
+      | Section_debug_abbrev 
+      | Section_debug_info _
+      | Section_debug_loc -> ()
+      | sec ->
+          let name = match sec with
+          | Section_user (name,_,_) -> name
+          | _ -> name_of_section sec in
+          if not (Debug.exists_section name) then 
+            let line_start = new_label ()
+            and low_pc = new_label ()
+            and debug_info = new_label () in
+            Debug.add_diab_info name (line_start,debug_info,name_of_section sec);
+            Debug.add_compilation_section_start name low_pc;
+            let line_name = ".debug_line" ^(if name <> ".text" then name else "") in 
+            fprintf oc "	.section	%s,,n\n" line_name;
+            if name <> ".text" then
+              fprintf oc "	.sectionlink	.debug_line\n";
+            fprintf oc "%a:\n" label line_start;
+            section oc sec;
+            fprintf oc "%a:\n" label low_pc;
+            fprintf oc "	.0byte	%a\n" label debug_info;
+            fprintf oc "	.d2_line_start	%s\n" line_name
+          else
+            ()
         
     let print_prologue oc =
       fprintf oc "	.xopt	align-fill-text=0x60000000\n";
-      if !Clflags.option_g then
-        begin
-          fprintf oc "	.text\n";
-          fprintf oc "	.section	.debug_line,,n\n";
-          let label_line_start = new_label () in
-          stmt_list_addr := label_line_start;
-          fprintf oc "%a:\n" label label_line_start;
-          fprintf oc "	.text\n";
-          let label_start = new_label () in
-          start_addr := label_start;
-          fprintf oc "%a:\n" label label_start;
-          fprintf oc "	.d2_line_start	.debug_line\n";
-        end
-
-    let filenum : (string,int) Hashtbl.t = Hashtbl.create 7
-
-    let additional_debug_sections: StringSet.t ref = ref StringSet.empty
-
+      debug_section oc Section_text
 
     let print_epilogue oc =
-      if !Clflags.option_g then
-        begin
-          fprintf oc "\n";
-          let label_end = new_label () in
-          end_addr := label_end;
-          fprintf oc "%a:\n" label label_end;
-          fprintf oc "	.text\n";
-          StringSet.iter (fun file ->
-            let label = new_label () in
-            Hashtbl.add filenum file label;
-            fprintf oc ".L%d:	.d2filenum \"%s\"\n" label file) !all_files;
-          fprintf oc "	.d2_line_end\n";
-          StringSet.iter (fun s ->
-            fprintf oc "	%s\n" s;
-            fprintf oc "	.d2_line_end\n") !additional_debug_sections
-        end
-
-    let print_file_loc oc (file,col) =
-      fprintf oc "	.4byte		%a\n" label (Hashtbl.find filenum file);
-      fprintf oc "	.uleb128	%d\n" col
-
-    let debug_section oc sec =
-      if !Clflags.option_g && Configuration.advanced_debug then
-        match sec with
-        | Section_user (name,_,_)  ->
-            let sec_name = name_of_section sec in
-            if not (StringSet.mem sec_name !additional_debug_sections) then
-              begin
-                let name = ".debug_line"^name in
-                additional_debug_sections := StringSet.add sec_name !additional_debug_sections;
-                fprintf oc "	.section	%s,,n\n" name;
-                fprintf oc "	.sectionlink	.debug_line\n";
-                section oc sec;
-                fprintf oc "	.d2_line_start	%s\n" name
-              end
-        | _ -> () (* Only the case of a user section is interresting *)
-      else
-        ()
-            
+      let end_label sec = 
+        fprintf oc "\n";
+        fprintf oc "	%s\n" sec;
+        let label_end = new_label () in
+        fprintf oc "%a:\n" label label_end;
+        label_end 
+      and entry_label f =
+        let label = new_label () in
+        fprintf oc ".L%d:	.d2filenum \"%s\"\n" label f;
+        label
+      and end_line () =   fprintf oc "	.d2_line_end\n" in
+      Debug.compute_diab_file_enum end_label entry_label end_line
 
   end
 
@@ -865,21 +865,12 @@ module Target (System : SYSTEM):TARGET =
       end
 
     let default_falignment = 4
-        
-    let get_start_addr () = !start_addr
-
-    let get_end_addr () = !end_addr
-
-    let get_stmt_list_addr () = !stmt_list_addr
-
-    module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs
 
     let new_label = new_label            
 
     let section oc sec =
       section oc sec;
       debug_section oc sec
-
   end
 
 let sel_target () =