Merge branch 'debugscopes' into debug_locations

Conflicts:
	debug/CtoDwarf.ml
	debug/DwarfPrinter.ml

7 files changed, 34 insertions, 18 deletions

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/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 2daa2d56..ed0fe524 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -266,6 +266,8 @@ let print_debug_info comment print_line print_preg sp_name oc kind txt args =
       args in
   match kind with
   | 1 ->  (* line number *)
+      fprintf oc "%s debug: current scopes%a\n"
+                 comment print_debug_args args;
       if Str.string_match re_file_line txt 0 then
         print_line oc (Str.matched_group 1 txt)
                       (int_of_string (Str.matched_group 2 txt))
@@ -280,6 +282,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 ->  (* declaration of a local variable *)
+      fprintf oc "%s debug: %s declared in scope%a\n"
+                 comment txt print_debug_args args
   | _ ->
       ()
 					    
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: