Merge branch 'master' into ppc64

Resolved conflicts in:configure	powerpc/Asmexpand.ml

10 files changed, 232 insertions, 121 deletions

diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 6ce6c005..25be9be3 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -55,3 +55,93 @@ let get_current_function () =
   let fn = !current_function in
   set_current_function dummy_function;
   {fn with fn_code = c}
+
+(* Expand function for debug information *)
+
+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 translate_annot sp preg_to_dwarf annot = 
+  let rec aux = function
+    | BA x -> Some (sp,BA (preg_to_dwarf x))
+    | BA_int _
+    | BA_long _
+    | BA_float _
+    | BA_single _
+    | BA_loadglobal _
+    | BA_addrglobal _
+    | BA_loadstack _ -> None
+    | BA_addrstack ofs -> Some (sp,BA_addrstack ofs)
+    | BA_splitlong (hi,lo) -> 
+        begin
+          match (aux hi,aux lo) with
+          | Some (_,hi) ,Some (_,lo) -> Some (sp,BA_splitlong (hi,lo))
+          | _,_ -> None
+        end in
+  (match annot with
+  | [] -> None
+  | a::_ -> aux a)
+    
+
+let expand_debug id sp preg simple 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 sp preg args with
+               | Some a ->
+                   let lbl = get_lbl lbl in
+                   Debug.start_live_range (id,txt) lbl 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 sp preg args with
+                | Some a->
+                    Debug.stack_variable (id,txt) 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 -> 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))
diff --git a/backend/Constprop.v b/backend/Constprop.v
index cd844d30..8f4cb76d 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -144,9 +144,9 @@ Fixpoint debug_strength_reduction (ae: AE.t) (al: list (builtin_arg reg)) :=
   | a :: al =>
       let a' := builtin_arg_reduction ae a in
       let al' := a :: debug_strength_reduction ae al in
-      match a' with
-      | BA_int _ | BA_long _ | BA_float _ | BA_single _ => a' :: al'
-      | _ => al'
+      match a, a' with
+      | BA _, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => a' :: al'
+      | _, _ => al'
       end
   end.
 
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index d9005f5e..eafefed5 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -243,7 +243,11 @@ Proof.
   induction 2; simpl.
 - exists (@nil val); constructor.
 - destruct IHlist_forall2 as (vl' & A).
-  destruct (builtin_arg_reduction ae a1); repeat (eauto; econstructor). 
+  assert (eval_builtin_args ge (fun r => rs#r) sp m
+             (a1 :: debug_strength_reduction ae al) (b1 :: vl'))
+  by (constructor; eauto).
+  destruct a1; try (econstructor; eassumption).
+  destruct (builtin_arg_reduction ae (BA x)); repeat (eauto; econstructor). 
 Qed.
 
 Lemma builtin_strength_reduction_correct:
diff --git a/backend/Fileinfo.ml b/backend/Fileinfo.ml
new file mode 100644
index 00000000..0490def0
--- /dev/null
+++ b/backend/Fileinfo.ml
@@ -0,0 +1,80 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*          Bernhard Schommer, AbsInt Angewandte Informatik GmbH       *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+open Printf
+
+(* Printing annotations in asm syntax *)
+
+let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t
+                  = Hashtbl.create 7
+
+let last_file = ref ""
+
+let reset_filenames () =
+  Hashtbl.clear filename_info; last_file := ""
+
+let close_filenames () =
+  Hashtbl.iter
+    (fun file (num, fb) ->
+       match fb with Some b -> Printlines.close b | None -> ())
+    filename_info;
+  reset_filenames()
+
+let enter_filename f =
+  let num = Hashtbl.length filename_info + 1 in
+  let filebuf =
+    if !Clflags.option_S || !Clflags.option_dasm then begin
+      try Some (Printlines.openfile f)
+      with Sys_error _ -> None
+    end else None in
+  Hashtbl.add filename_info f (num, filebuf);
+  (num, filebuf)
+
+(* Add file and line debug location, using GNU assembler-style DWARF2
+   directives *)
+let print_file oc file =
+  try
+    Hashtbl.find filename_info file
+  with Not_found ->
+    let (filenum, filebuf as res) = enter_filename file in
+    fprintf oc "	.file	%d %S\n" filenum file;
+    res
+
+let print_file_line oc pref file line =
+  if !Clflags.option_g && file <> "" then begin
+    let (filenum, filebuf) = print_file oc file in
+    fprintf oc "	.loc	%d %d\n" filenum line;
+    match filebuf with
+    | None -> ()
+    | Some fb -> Printlines.copy oc pref fb line line
+  end
+
+(* Add file and line debug location, using DWARF2 directives in the style
+   of Diab C 5 *)
+
+let print_file_line_d2 oc pref file line =
+  if !Clflags.option_g && file <> "" then begin
+    let (_, filebuf) =
+      try
+        Hashtbl.find filename_info file
+      with Not_found ->
+        enter_filename file in
+    if file <> !last_file then begin
+      fprintf oc "	.d2file	%S\n" file;
+      last_file := file
+    end;
+    fprintf oc "	.d2line	%d\n" line;
+    match filebuf with
+    | None -> ()
+    | Some fb -> Printlines.copy oc pref fb line line
+  end
diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml
index f3c80f3e..594b43b7 100644
--- a/backend/PrintAsm.ml
+++ b/backend/PrintAsm.ml
@@ -24,14 +24,11 @@ open TargetPrinter
 module Printer(Target:TARGET) =
   struct
 
-    let addr_mapping: (string, (int * int)) Hashtbl.t = Hashtbl.create 7
-
     let get_fun_addr name =
-      let name = extern_atom name in
-      let start_addr = new_label ()
-      and end_addr = new_label () in
-      Hashtbl.add addr_mapping name (start_addr,end_addr);
-      start_addr,end_addr
+      let s = Target.new_label ()
+      and e = Target.new_label () in
+      Debug.add_fun_addr name (e,s);
+      s,e
 
     let print_debug_label oc l =
       if !Clflags.option_g && Configuration.advanced_debug then
@@ -39,7 +36,6 @@ module Printer(Target:TARGET) =
       else
         ()
 
-
     let print_location oc loc =
       if loc <> Cutil.no_loc then Target.print_file_line oc (fst loc) (snd loc)
           
@@ -67,7 +63,9 @@ module Printer(Target:TARGET) =
       print_debug_label oc e;
       Target.print_fun_info oc name;
       Target.emit_constants oc lit;
-      Target.print_jumptable oc jmptbl
+      Target.print_jumptable oc jmptbl;
+      if !Clflags.option_g then
+        Hashtbl.iter (fun p i -> Debug.add_label name p i) current_function_labels
     
     let print_init_data oc name id =
       if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
@@ -81,10 +79,11 @@ module Printer(Target:TARGET) =
       match v.gvar_init with
       | [] -> ()
       | _  ->
+          Debug.variable_printed (extern_atom name);
           let sec =
             match C2C.atom_sections name with
             | [s] -> s
-        |  _  -> Section_data true
+            |  _  -> Section_data true
           and align =
             match C2C.atom_alignof name with
             | Some a -> a
@@ -102,8 +101,7 @@ module Printer(Target:TARGET) =
             let sz =
               match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
             Target.print_comm_symb oc sz name align
-              
-              
+                            
     let print_globdef oc (name,gdef) =
       match gdef with
       | Gfun (Internal code) -> print_function oc name code
@@ -113,33 +111,34 @@ module Printer(Target:TARGET) =
     module DwarfTarget: DwarfTypes.DWARF_TARGET =
       struct
         let label = Target.label
+        let section = Target.section
         let name_of_section = Target.name_of_section
-        let print_file_loc = Target.print_file_loc
-        let get_start_addr = Target.get_start_addr   
-        let get_end_addr = Target.get_end_addr
-        let get_stmt_list_addr = Target.get_stmt_list_addr
-        let name_of_section = Target.name_of_section
-        let get_fun_addr s = try Some (Hashtbl.find addr_mapping s) with Not_found -> None
+        let symbol = Target.symbol
       end
 
-    module DebugPrinter = DwarfPrinter (DwarfTarget) (Target.DwarfAbbrevs)
-      
-     
+    module DebugPrinter = DwarfPrinter (DwarfTarget)     
   end
 
 let print_program oc p db =
   let module Target = (val (sel_target ()):TARGET) in
   let module Printer = Printer(Target) in
-  reset_filenames ();
+  Fileinfo.reset_filenames ();
   print_version_and_options oc Target.comment;
   Target.print_prologue oc;
   List.iter (Printer.print_globdef oc) p.prog_defs;
   Target.print_epilogue oc;
-  close_filenames ();
   if !Clflags.option_g && Configuration.advanced_debug then
     begin
-      match db with
+      let atom_to_s s =
+        let s = C2C.atom_sections s in
+        match s with
+        | [] -> Target.name_of_section Section_text
+        | (Section_user (n,_,_))::_ -> n
+        | a::_ ->
+            Target.name_of_section a in
+      match Debug.generate_debug_info atom_to_s (Target.name_of_section Section_text) with
       | None -> ()
       | Some db ->
           Printer.DebugPrinter.print_debug oc db
-    end
+    end;
+  Fileinfo.close_filenames ()
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 67e53aea..78399c04 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -14,7 +14,6 @@
 open AST
 open Asm
 open Camlcoq
-open DwarfTypes
 open Datatypes
 open Memdata
 open Printf
@@ -45,13 +44,8 @@ module type TARGET =
       val comment: string
       val symbol: out_channel -> P.t -> unit
       val default_falignment: int
-      val get_start_addr: unit -> int
-      val get_end_addr: unit -> int
-      val get_stmt_list_addr: unit -> int
       val new_label: unit -> int
       val label: out_channel -> int -> unit
-      val print_file_loc: out_channel -> file_loc -> unit
-      module DwarfAbbrevs:  DWARF_ABBREVS
     end
 
 (* On-the-fly label renaming *)
@@ -139,77 +133,6 @@ let cfi_rel_offset =
 let coqint oc n =
   fprintf oc "%ld" (camlint_of_coqint n)
 
-(* Printing annotations in asm syntax *)
-(** All files used in the debug entries *)
-module StringSet = Set.Make(String)
-let all_files : StringSet.t ref = ref StringSet.empty
-let add_file file =
-  all_files := StringSet.add file !all_files
-
-
-let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t
-                  = Hashtbl.create 7
-
-let last_file = ref ""
-
-let reset_filenames () =
-  Hashtbl.clear filename_info; last_file := ""
-
-let close_filenames () =
-  Hashtbl.iter
-    (fun file (num, fb) ->
-       match fb with Some b -> Printlines.close b | None -> ())
-    filename_info;
-  reset_filenames()
-
-let enter_filename f =
-  let num = Hashtbl.length filename_info + 1 in
-  let filebuf =
-    if !Clflags.option_S || !Clflags.option_dasm then begin
-      try Some (Printlines.openfile f)
-      with Sys_error _ -> None
-    end else None in
-  Hashtbl.add filename_info f (num, filebuf);
-  (num, filebuf)
-
-(* Add file and line debug location, using GNU assembler-style DWARF2
-   directives *)
-
-let print_file_line oc pref file line =
-  if !Clflags.option_g && file <> "" then begin
-    let (filenum, filebuf) =
-      try
-        Hashtbl.find filename_info file
-      with Not_found ->
-        let (filenum, filebuf as res) = enter_filename file in
-        fprintf oc "	.file	%d %S\n" filenum file;
-        res in
-    fprintf oc "	.loc	%d %d\n" filenum line;
-    match filebuf with
-    | None -> ()
-    | Some fb -> Printlines.copy oc pref fb line line
-  end
-
-(* Add file and line debug location, using DWARF2 directives in the style
-   of Diab C 5 *)
-
-let print_file_line_d2 oc pref file line =
-  if !Clflags.option_g && file <> "" then begin
-    let (_, filebuf) =
-      try
-        Hashtbl.find filename_info file
-      with Not_found ->
-        enter_filename file in
-    if file <> !last_file then begin
-      fprintf oc "	.d2file	%S\n" file;
-      last_file := file
-    end;
-    fprintf oc "	.d2line	%d\n" line;
-    match filebuf with
-    | None -> ()
-    | Some fb -> Printlines.copy oc pref fb line line
-  end
-
 (** Programmer-supplied annotations (__builtin_annot). *)
 
 let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
@@ -283,6 +206,9 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args =
   | 5 ->  (* local variable preallocated in stack *)
       fprintf oc "%s debug: %s resides at%a\n"
                  comment txt print_debug_args args
+  | 6 ->  (* scope annotations *)
+      fprintf oc "%s debug: current scopes%a\n"
+                 comment print_debug_args args;
   | _ ->
       ()
 					    
@@ -330,7 +256,12 @@ let print_inline_asm print_preg oc txt sg args res =
 (** Print CompCert version and command-line as asm comment *)
 
 let print_version_and_options oc comment =
-  fprintf oc "%s File generated by CompCert %s\n" comment Version.version;
+  let version_string =  
+    if Version.buildnr <> "" && Version.tag <> "" then
+      sprintf "%s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag
+    else
+      Version.version in
+  fprintf oc "%s File generated by CompCert %s\n" comment version_string;
   fprintf oc "%s Command line:" comment;
   for i = 1 to Array.length Sys.argv - 1 do
     fprintf oc " %s" Sys.argv.(i)
diff --git a/backend/RTL.v b/backend/RTL.v
index 56a5efeb..3cd4335d 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -104,8 +104,7 @@ Record function: Type := mkfunction {
     for its stack-allocated activation record.  [fn_params] is the list
     of registers that are bound to the values of arguments at call time.
     [fn_entrypoint] is the node of the first instruction of the function
-    in the CFG.  [fn_code_wf] asserts that all instructions of the function
-    have nodes no greater than [fn_nextpc]. *)
+    in the CFG. *)
 
 Definition fundef := AST.fundef function.
 
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index d818de58..3da961c6 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -415,11 +415,12 @@ Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list
       a1' :: convert_builtin_args al rl1
   end.
 
-Definition convert_builtin_res (map: mapping) (r: builtin_res ident) : mon (builtin_res reg) :=
-  match r with
-  | BR id => do r <- find_var map id; ret (BR r)
-  | BR_none => ret BR_none
-  | _ => error (Errors.msg "RTLgen: bad builtin_res")
+Definition convert_builtin_res (map: mapping) (oty: option typ) (r: builtin_res ident) : mon (builtin_res reg) :=
+  match r, oty with
+  | BR id, _ => do r <- find_var map id; ret (BR r)
+  | BR_none, None => ret BR_none
+  | BR_none, Some _ => do r <- new_reg; ret (BR r)
+  | _, _ => error (Errors.msg "RTLgen: bad builtin_res")
   end.
 
 (** Translation of an expression.  [transl_expr map a rd nd]
@@ -598,7 +599,7 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       let al := exprlist_of_expr_list (params_of_builtin_args args) in
       do rargs <- alloc_regs map al;
       let args' := convert_builtin_args args rargs in
-      do res' <- convert_builtin_res map res;
+      do res' <- convert_builtin_res map (sig_res (ef_sig ef)) res;
       do n1 <- add_instr (Ibuiltin ef args' res' nd);
          transl_exprlist map al rargs n1
   | Sseq s1 s2 =>
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 559ab3a2..19f6f1f4 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -234,6 +234,7 @@ Proof.
   intros. inv H1; simpl.
 - eapply match_env_update_var; eauto.
 - auto.
+- eapply match_env_update_temp; eauto.
 Qed.
 
 (** Matching and [let]-bound variables. *)
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 41b5016f..1e665002 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -814,7 +814,10 @@ Inductive tr_builtin_res: mapping -> builtin_res ident -> builtin_res reg -> Pro
       map.(map_vars)!id = Some r ->
       tr_builtin_res map (BR id) (BR r)
   | tr_builtin_res_none: forall map,
-      tr_builtin_res map BR_none BR_none.
+      tr_builtin_res map BR_none BR_none
+  | tr_builtin_res_fresh: forall map r,
+      ~reg_in_map map r ->
+      tr_builtin_res map BR_none (BR r).
 
 (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c],
   starting at node [ns], contains instructions that perform the Cminor
@@ -1214,14 +1217,17 @@ Proof.
 Qed.
 
 Lemma convert_builtin_res_charact:
-  forall map res s res' s' INCR
-    (TR: convert_builtin_res map res s = OK res' s' INCR)
+  forall map oty res s res' s' INCR
+    (TR: convert_builtin_res map oty res s = OK res' s' INCR)
     (WF: map_valid map s),
   tr_builtin_res map res res'.
 Proof.
-  destruct res; simpl; intros; monadInv TR. 
-- constructor.  unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto.
-- constructor.
+  destruct res; simpl; intros.
+- monadInv TR. constructor.  unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto.
+- destruct oty; monadInv TR.
++ constructor. eauto with rtlg. 
++ constructor.
+- monadInv TR.
 Qed.
 
 Lemma transl_stmt_charact: