Merge branch 'master' into json_export

Conflicts:
	driver/Driver.ml

4 files changed, 54 insertions, 15 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 3fa7af31..a1d8338a 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -161,7 +161,7 @@ Inductive instruction : Type :=
   | Pcmplwi: ireg -> constant -> instruction                  (**r same, with immediate argument *)
   | Pcmpw: ireg -> ireg -> instruction                        (**r signed integer comparison *)
   | Pcmpwi: ireg -> constant -> instruction                   (**r same, with immediate argument *)
-  | Pcntlz: ireg -> ireg -> instruction                       (**r count leading zeros *)
+  | Pcntlzw: ireg -> ireg -> instruction                       (**r count leading zeros *)
   | Pcreqv: crbit -> crbit -> crbit -> instruction            (**r not-xor between condition bits *)
   | Pcror: crbit -> crbit -> crbit -> instruction             (**r or between condition bits *)
   | Pcrxor: crbit -> crbit -> crbit -> instruction            (**r xor between condition bits *)
@@ -853,7 +853,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   (** The following instructions and directives are not generated directly by Asmgen,
       so we do not model them. *)
   | Pbdnz _
-  | Pcntlz _ _
+  | Pcntlzw _ _
   | Pcreqv _ _ _
   | Pcrxor _ _ _
   | Peieio
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 4c3f9d97..36960821 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -171,7 +171,7 @@ let p_instruction oc ic =
   | Pcmplwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmplwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c
   | Pcmpw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcmpw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pcmpwi (ir,c) -> fprintf oc "{\"Instruction Name\":\"Pcmpwi\",\"Args\":[%a,%a]}" p_ireg ir p_constant c 
-  | Pcntlz (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcntlz\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
+  | Pcntlzw (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pcntlzw\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pcreqv (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcreqv\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3
   | Pcror (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcror\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3
   | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 699c841f..3f4dc94b 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -343,7 +343,7 @@ let expand_builtin_inline name args res =
   | "__builtin_mulhwu", [IR a1; IR a2], [IR res] ->
       emit (Pmulhwu(res, a1, a2))
   | "__builtin_clz", [IR a1], [IR res] ->
-      emit (Pcntlz(res, a1))
+      emit (Pcntlzw(res, a1))
   | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] ->
       emit (Pstwu(a1, Cint _m8, GPR1));
       emit (Pcfi_adjust _8);
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 2d47acb0..1cd7fe37 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -30,8 +30,8 @@ module type SYSTEM =
       val constant: out_channel -> constant -> unit
       val ireg: out_channel -> ireg -> unit
       val freg: out_channel -> freg -> unit
-      val creg: out_channel -> int -> unit
       val name_of_section: section_name -> string
+      val creg: out_channel -> int -> unit
       val print_file_line: out_channel -> string -> int -> unit
       val cfi_startproc: out_channel -> unit
       val cfi_endproc: out_channel -> unit
@@ -40,6 +40,8 @@ module type SYSTEM =
       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
 
 let symbol = elf_symbol
@@ -129,6 +131,11 @@ module Linux_System : SYSTEM =
             s (if wr then "w" else "") (if ex then "x" else "")
       | Section_debug_info -> ".debug_info,\"\",@progbits"
       | Section_debug_abbrev -> ".debug_abbrev,\"\",@progbits"
+    
+    let section oc sec =
+      let name = name_of_section sec in
+      assert (name <> "COMM");
+      fprintf oc "	%s\n" name
 
 
     let print_file_line oc file line =
@@ -148,7 +155,8 @@ module Linux_System : SYSTEM =
     let print_epilogue oc = ()
 
     let print_file_loc _ _ = ()
-  
+        
+    let debug_section _ _ = ()
   end
     
 module Diab_System : SYSTEM =
@@ -202,6 +210,12 @@ module Diab_System : SYSTEM =
       | Section_debug_info -> ".debug_info,,n"
       | Section_debug_abbrev -> ".debug_abbrev,,n"
 
+    let section oc sec =
+      let name = name_of_section sec in
+      assert (name <> "COMM");
+      fprintf oc "	%s\n" name
+
+
     let print_file_line oc file line =
       print_file_line_d2 oc comment file line
 
@@ -232,6 +246,9 @@ module Diab_System : SYSTEM =
 
     let filenum : (string,int) Hashtbl.t = Hashtbl.create 7
 
+    let additional_debug_sections: StringSet.t ref = ref StringSet.empty
+
+
     let print_epilogue oc =
       if !Clflags.option_g then
         begin
@@ -244,12 +261,35 @@ module Diab_System : SYSTEM =
             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"
+          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
+        ()
+            
+
   end
 
 module Target (System : SYSTEM):TARGET =
@@ -296,11 +336,6 @@ module Target (System : SYSTEM):TARGET =
       | FR r -> fprintf oc "f%s" (float_reg_name r)
       | _    -> assert false
 
-    let section oc sec =
-      let name = name_of_section sec in
-      assert (name <> "COMM");
-      fprintf oc "	%s\n" name
-
     let print_location oc loc =
       if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
 
@@ -426,8 +461,8 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	cmpw	%a, %a, %a\n" creg 0 ireg r1 ireg r2
       | Pcmpwi(r1, c) ->
           fprintf oc "	cmpwi	%a, %a, %a\n" creg 0 ireg r1 constant c
-      | Pcntlz(r1, r2) ->
-          fprintf oc "	cntlz	%a, %a\n" ireg r1 ireg r2
+      | Pcntlzw(r1, r2) ->
+          fprintf oc "	cntlzw	%a, %a\n" ireg r1 ireg r2
       | Pcreqv(c1, c2, c3) ->
           fprintf oc "	creqv	%a, %a, %a\n" crbit c1 crbit c2 crbit c3
       | Pcror(c1, c2, c3) ->
@@ -806,7 +841,11 @@ module Target (System : SYSTEM):TARGET =
 
     module DwarfAbbrevs = DwarfUtil.DefaultAbbrevs
 
-    let new_label = new_label
+    let new_label = new_label            
+
+    let section oc sec =
+      section oc sec;
+      debug_section oc sec
 
   end