Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3

13 files changed, 183 insertions, 80 deletions

diff --git a/backend/Debugvar.v b/backend/Debugvar.v
index 56908855..7806984a 100644
--- a/backend/Debugvar.v
+++ b/backend/Debugvar.v
@@ -92,7 +92,7 @@ Fixpoint remove_state (v: ident) (s: avail) : avail :=
       end
   end.
 
-Fixpoint set_debug_info (v: ident) (info: list (builtin_arg loc)) (s: avail) :=
+Definition set_debug_info (v: ident) (info: list (builtin_arg loc)) (s: avail) :=
   match normalize_debug info with
   | Some a => set_state v a s
   | None   => remove_state v s
diff --git a/backend/Duplicateaux.ml b/backend/Duplicateaux.ml
index 8436863a..c9985dc4 100644
--- a/backend/Duplicateaux.ml
+++ b/backend/Duplicateaux.ml
@@ -115,16 +115,18 @@ let ptree_printbool pt =
 
 (* Looks ahead (until a branch) to see if a node further down verifies
  * the given predicate *)
-let rec look_ahead code node is_loop_header predicate =
+let rec look_ahead_gen (successors: RTL.instruction -> P.t list) code node is_loop_header predicate =
   if (predicate node) then true
-  else match (rtl_successors @@ get_some @@ PTree.get node code) with
+  else match (successors @@ get_some @@ PTree.get node code) with
     | [n] -> if (predicate n) then true
         else (
           if (get_some @@ PTree.get n is_loop_header) then false
-          else look_ahead code n is_loop_header predicate
+          else look_ahead_gen successors code n is_loop_header predicate
         )
     | _ -> false
 
+let look_ahead = look_ahead_gen rtl_successors
+
 (** 
  * Heuristics mostly based on the paper Branch Prediction for Free 
  *)
@@ -545,7 +547,7 @@ let is_a_nop code n =
  * preds: mapping node -> predecessors
  * ptree: the revmap
  * trace: the trace to follow tail duplication on *)
-let tail_duplicate code preds ptree trace =
+let tail_duplicate code preds is_loop_header ptree trace =
   debug "Tail_duplicate on that trace: %a\n" print_trace trace;
   (* next_int: unused integer that can be used for the next duplication *)
   let next_int = ref (next_free_pc code)
@@ -561,8 +563,12 @@ let tail_duplicate code preds ptree trace =
           if is_first then (code, ptree) (* first node is never duplicated regardless of its inputs *)
           else
             let node_preds = ptree_get_some n preds
-            in let node_preds_nolast = List.filter (fun e -> e <> get_some !last_node) node_preds
-            in let node_preds_nolast = List.filter (fun e -> not @@ List.mem e t) node_preds_nolast
+            in let node_preds_nolast = 
+              (* We traverse loop headers without initiating tail duplication 
+               * (see case of two imbricated loops) *)
+              if (get_some @@ PTree.get n is_loop_header) then []
+              else List.filter (fun e -> e <> get_some !last_node) node_preds
+            (* in let node_preds_nolast = List.filter (fun e -> not @@ List.mem e t) node_preds_nolast *)
             in let final_node_preds = match !last_duplicate with
               | None -> node_preds_nolast
               | Some n' -> n' :: node_preds_nolast
@@ -583,12 +589,12 @@ let tail_duplicate code preds ptree trace =
   in let new_code, new_ptree = f code ptree true trace
   in (new_code, new_ptree, !nb_duplicated)
 
-let superblockify_traces code preds traces ptree =
+let superblockify_traces code preds is_loop_header traces ptree =
   let max_nb_duplicated = !Clflags.option_ftailduplicate (* FIXME - should be architecture dependent *)
   in let rec f code ptree = function
     | [] -> (code, ptree, 0)
     | trace :: traces ->
-        let new_code, new_ptree, nb_duplicated = tail_duplicate code preds ptree trace
+        let new_code, new_ptree, nb_duplicated = tail_duplicate code preds is_loop_header ptree trace
         in if (nb_duplicated < max_nb_duplicated)
           then (debug "End duplication\n"; f new_code new_ptree traces)
           else (debug "Too many duplicated nodes, aborting tail duplication\n"; (code, ptree, 0))
@@ -617,15 +623,29 @@ type innerLoop = {
   preds: P.t list;
   body: P.t list;
   head: P.t; (* head of the loop *)
-  finals: P.t list (* the final instructions, which loops back to the head *)
+  finals: P.t list; (* the final instructions, which loops back to the head *)
   (* There may be more than one ; for instance if there is an if inside the loop with both
-   * branches leading to a goto backedge *)
+   * branches leading to a goto backedge
+   * Such cases usually happen after a tail-duplication *)
+  sb_final: P.t option; (* if the innerloop wraps a superblock, this is its final instruction *)
+    (* may be None if we predict that we do not loop *)
 }
 
 let print_pset = LICMaux.pp_pset
 
+let print_option_pint oc o =
+  if !debug_flag then
+    match o with
+    | None -> Printf.fprintf oc "None"
+    | Some n -> Printf.fprintf oc "Some %d" (P.to_int n)
+
 let print_inner_loop iloop =
-  debug "{preds: %a, body: %a}" print_intlist iloop.preds print_intlist iloop.body
+  debug "{preds: %a, body: %a, head: %d, finals: %a, sb_final: %a}\n"
+    print_intlist iloop.preds
+    print_intlist iloop.body
+    (P.to_int iloop.head)
+    print_intlist iloop.finals
+    print_option_pint iloop.sb_final
 
 let rec print_inner_loops = function
 | [] -> ()
@@ -694,6 +714,34 @@ let get_inner_loops f code is_loop_header =
   !iloops
   *)
 
+let rtl_successors_pref = function
+| Itailcall _ | Ireturn _ -> []
+| Icall(_,_,_,_,n) | Ibuiltin(_,_,_,n) | Inop n | Iop (_,_,_,n)
+| Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) -> [n]
+| Icond (_,_,n1,n2,p) -> (match p with
+  | Some true -> [n1]
+  | Some false -> [n2]
+  | None -> [n1; n2])
+| Ijumptable (_,ln) -> ln
+
+(* Find the last node of a trace (starting at "node"), until a loop is encountered.
+ * If a non-predicted branch is encountered, returns None *)
+let rec find_last_node_before_loop code node trace is_loop_header =
+  let rtl_succ = rtl_successors @@ get_some @@ PTree.get node code in
+  let headers = List.filter (fun n -> 
+    get_some @@ PTree.get n is_loop_header && HashedSet.PSet.contains trace n) rtl_succ in 
+  match headers with
+  | [] -> (
+      let next_nodes = List.filter (fun n -> HashedSet.PSet.contains trace n)
+        (rtl_successors_pref @@ get_some @@ PTree.get node code) in
+      match next_nodes with
+      | [n] -> find_last_node_before_loop code n trace is_loop_header
+      | _ -> None (* May happen when we predict that a loop is not taken *)
+    )
+  | [h] -> Some node
+  | _ -> failwith "Multiple branches leading to a loop"
+
+(* The computation of sb_final requires to already have branch prediction *)
 let get_inner_loops f code is_loop_header =
   let fake_f = { fn_sig = f.fn_sig; fn_params = f.fn_params; 
     fn_stacksize = f.fn_stacksize; fn_code = code; fn_entrypoint = f.fn_entrypoint } in
@@ -720,7 +768,10 @@ let get_inner_loops f code is_loop_header =
           debug "HEADPREDS: %a\n" print_intlist head_preds;
           filtered
         end in
-      { preds = preds; body = (HashedSet.PSet.elements body); head = head; finals = finals }
+      let sb_final = find_last_node_before_loop code head body is_loop_header in
+      let body = HashedSet.PSet.elements body in
+      { preds = preds; body = body; head = head; finals = finals;
+        sb_final = sb_final; }
     ) 
     (* LICMaux.inner_loops also returns non-inner loops, but with a body of 1 instruction
      * We remove those to get just the inner loops *)
@@ -838,31 +889,36 @@ let unroll_inner_loops_single f code revmap =
     (!code', !revmap')
   end
 
+let is_some o = match o with Some _ -> true | None -> false
+
 (* Unrolls the body of the inner loop once - duplicating the exit condition as well 
  * 1) Clones body into body'
- * 2) Links the last instruction of body into the first of body' 
+ * 2) Links the last instruction of body (sb_final) into the first of body' 
  * 3) Links the last instruction of body' into the first of body
  *)
 let unroll_inner_loop_body code revmap iloop =
+  debug "iloop = "; print_inner_loop iloop;
   let body = iloop.body in
   let limit = !Clflags.option_funrollbody in
   if count_ignore_nops code body > limit then begin
     debug "Too many nodes in the loop body (%d > %d)" (List.length body) limit;
     (code, revmap)
+  end else if not @@ is_some iloop.sb_final then begin
+    debug "The loop body does not form a superblock OR we have predicted that we do not loop";
+    (code, revmap)
   end else
     let (code2, revmap2, dupbody, fwmap) = clone code revmap body in
     let code' = ref code2 in
     let head' = apply_map fwmap (iloop.head) in
     let finals' = apply_map_list fwmap (iloop.finals) in
     begin
-      code' := change_pointers !code' iloop.head head' iloop.finals;
+      code' := change_pointers !code' iloop.head head' [get_some @@ iloop.sb_final];
       code' := change_pointers !code' head' iloop.head finals'; 
       (!code', revmap2)
     end
 
 let unroll_inner_loops_body f code revmap =
   let is_loop_header = get_loop_headers code (f.fn_entrypoint) in
-  (* debug_flag := true; *)
   let inner_loops = get_inner_loops f code is_loop_header in
   debug "Number of loops found: %d\n" (List.length inner_loops);
   let code' = ref code in
@@ -872,7 +928,7 @@ let unroll_inner_loops_body f code revmap =
     List.iter (fun iloop ->
       let (new_code, new_revmap) = unroll_inner_loop_body !code' !revmap' iloop in
       code' := new_code; revmap' := new_revmap
-    ) inner_loops; (* debug_flag := false; *)
+    ) inner_loops;
     (!code', !revmap')
   end
 
@@ -968,6 +1024,7 @@ let tail_duplicate f =
     if !Clflags.option_ftailduplicate > 0 then
       let traces = select_traces code entrypoint in
       let preds = get_predecessors_rtl code in
-      superblockify_traces code preds traces revmap
+      let is_loop_header = get_loop_headers code entrypoint in
+      superblockify_traces code preds is_loop_header traces revmap
     else (code, revmap) in
   ((code, entrypoint), revmap)
diff --git a/backend/IRC.ml b/backend/IRC.ml
index 785b0a2d..29d224c8 100644
--- a/backend/IRC.ml
+++ b/backend/IRC.ml
@@ -102,7 +102,7 @@ after IRC elimination, when assigning a stack slot to a spilled variable. *)
 
 let name_of_loc = function
   | R r ->
-      begin match Machregsaux.name_of_register r with
+      begin match Machregsnames.name_of_register r with
                 | None -> "fixed-reg"
                 | Some s -> s
       end
@@ -247,12 +247,10 @@ let class_of_loc = function
 
 let no_spill_class = 2
 
-let reserved_registers = ref ([]: mreg list)
-
 let rec remove_reserved = function
   | [] -> []
   | hd :: tl ->
-      if List.mem hd !reserved_registers
+      if List.mem hd !CPragmas.reserved_registers
       then remove_reserved tl
       else hd :: remove_reserved tl
 
diff --git a/backend/IRC.mli b/backend/IRC.mli
index f7bbf9c5..254f27ff 100644
--- a/backend/IRC.mli
+++ b/backend/IRC.mli
@@ -13,7 +13,6 @@
 (* Iterated Register Coalescing: George and Appel's graph coloring algorithm *)
 
 open Registers
-open Machregs
 open Locations
 open XTL
 
@@ -39,8 +38,5 @@ val add_pref: graph -> var -> var -> unit
 (* Color the graph.  Return an assignment of locations to variables. *)
 val coloring: graph -> (var -> loc)
 
-(* Machine registers that are reserved and not available for allocation. *)
-val reserved_registers: mreg list ref
-
 (* Auxiliaries to deal with register classes *)
 val class_of_loc: loc -> int
diff --git a/backend/Machregsnames.ml b/backend/Machregsnames.ml
new file mode 100644
index 00000000..fdcbd0e5
--- /dev/null
+++ b/backend/Machregsnames.ml
@@ -0,0 +1,24 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+let register_names : (Machregs.mreg, string) Hashtbl.t = Hashtbl.create 31
+
+let _ =
+  List.iter
+    (fun (s, r) -> Hashtbl.add register_names r (Camlcoq.camlstring_of_coqstring s))
+    Machregs.register_names
+
+let name_of_register r =
+  Hashtbl.find_opt register_names r
+
+let register_by_name s =
+  Machregs.register_by_name (Camlcoq.coqstring_uppercase_ascii_of_camlstring s)
diff --git a/backend/Machregsnames.mli b/backend/Machregsnames.mli
new file mode 100644
index 00000000..1b600d35
--- /dev/null
+++ b/backend/Machregsnames.mli
@@ -0,0 +1,16 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Auxiliary functions on machine registers *)
+
+val name_of_register: Machregs.mreg -> string option
+val register_by_name: string -> Machregs.mreg option
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 3c2d8e20..d9e9e025 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -47,7 +47,7 @@ Definition iagree (p q mask: int) : Prop :=
   forall i, 0 <= i < Int.zwordsize -> Int.testbit mask i = true ->
             Int.testbit p i = Int.testbit q i.
 
-Fixpoint vagree (v w: val) (x: nval) {struct x}: Prop :=
+Definition vagree (v w: val) (x: nval) : Prop :=
   match x with
   | Nothing => True
   | I m =>
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 7fa10aee..5cb693af 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -297,8 +297,8 @@ let print_inline_asm print_preg oc txt sg args res =
 
 let print_version_and_options oc comment =
   let version_string =
-    if Version.buildnr <> "" && Version.tag <> "" then
-      sprintf "Release: %s, Build: %s, Tag: %s" Version.version Version.buildnr Version.tag
+    if Version.buildnr <> "" && Version.tag <> "" && Version.branch <> "" then
+      sprintf "Release: %s, Build: %s, Tag: %s, Branch: %s" Version.version Version.buildnr Version.tag Version.branch
     else
       Version.version in
   fprintf oc "%s File generated by CompCert %s\n" comment version_string;
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index 8259297b..87e8a1fc 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -22,7 +22,7 @@ open PrintAST
 open PrintOp
 
 let mreg pp r =
-  match Machregsaux.name_of_register r with
+  match Machregsnames.name_of_register r with
   | Some s -> fprintf pp "%s" s
   | None -> fprintf pp "<unknown machreg>"
 
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index 70e65832..3481421b 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -16,12 +16,11 @@ open Printf
 open Camlcoq
 open Datatypes
 open AST
-open Machregsaux
 open Mach
 open PrintAST
 
 let reg pp r =
-  match name_of_register r with
+  match Machregsnames.name_of_register r with
   | Some s -> fprintf pp "%s" s
   | None -> fprintf pp "<unknown reg>"
 
diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml
index d1b79623..6f2b1df9 100644
--- a/backend/PrintXTL.ml
+++ b/backend/PrintXTL.ml
@@ -22,7 +22,7 @@ open PrintOp
 open XTL
 
 let mreg pp r =
-  match Machregsaux.name_of_register r with
+  match Machregsnames.name_of_register r with
   | Some s -> fprintf pp "%s" s
   | None -> fprintf pp "<unknown machreg>"
 
diff --git a/backend/Selection.v b/backend/Selection.v
index 342bd8ca..8667922f 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -251,10 +251,16 @@ Function sel_known_builtin (bf: builtin_function) (args: exprlist) :=
       Some (sel_select ty a1 a2 a3)
   | BI_standard BI_fabs, a1 ::: Enil =>
       Some (SelectOp.absf a1)
+  | BI_standard BI_fabsf, a1 ::: Enil =>
+      Some (SelectOp.absfs a1)
   | _, _ =>
       None
   end.
 
+(** A CminorSel statement that does nothing, like [Sskip], but reduces. *)
+
+Definition Sno_op := Sseq Sskip Sskip.
+
 (** Builtin functions in general *)
 
 Definition sel_builtin_default (optid: option ident) (ef: external_function)
@@ -264,17 +270,22 @@ Definition sel_builtin_default (optid: option ident) (ef: external_function)
 
 Definition sel_builtin (optid: option ident) (ef: external_function)
                                (args: list Cminor.expr) :=
-  match optid, ef with
-  | Some id, EF_builtin name sg =>
+  match ef with
+  | EF_builtin name sg =>
       match lookup_builtin_function name sg with
       | Some bf =>
-          match sel_known_builtin bf (sel_exprlist args) with
-          | Some a => Sassign id a
-          | None => sel_builtin_default optid ef args
+          match optid with
+          | Some id =>
+              match sel_known_builtin bf (sel_exprlist args) with
+              | Some a => Sassign id a
+              | None => sel_builtin_default optid ef args
+              end
+          | None =>
+              Sno_op   (**r builtins with semantics are pure *)
           end
       | None => sel_builtin_default optid ef args
       end
-  | _, _ =>
+  | _ =>
       sel_builtin_default optid ef args
   end.
 
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 955c45a4..4d075f4a 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -396,13 +396,10 @@ Proof.
   inv ARGS; try discriminate. inv H0; try discriminate.
   inv SEL.  
   simpl in SEM; inv SEM. apply eval_absf; auto.
-  (* + (* expect *)
-  inv ARGS; try discriminate.
-  inv H0; try discriminate.
-  inv H2; try discriminate.
-  simpl in SEM. inv SEM. inv SEL.
-  destruct v1; destruct v0.
-  all: econstructor; split; eauto. *)
++ (* fabsf *)
+  inv ARGS; try discriminate. inv H0; try discriminate.
+  inv SEL.  
+  simpl in SEM; inv SEM. apply eval_absfs; auto.
 - eapply eval_platform_builtin; eauto.
 Qed.
 
@@ -852,8 +849,8 @@ Lemma sel_builtin_default_correct:
   external_call ef ge vl m1 t v m2 ->
   env_lessdef e1 e1' -> Mem.extends m1 m1' ->
   exists e2' m2',
-     step tge (State f (sel_builtin_default optid ef al) k sp e1' m1')
-            t (State f Sskip k sp e2' m2')
+     plus step tge (State f (sel_builtin_default optid ef al) k sp e1' m1')
+                 t (State f Sskip k sp e2' m2')
   /\ env_lessdef (set_optvar optid v e1) e2'
   /\ Mem.extends m2 m2'.
 Proof.
@@ -861,6 +858,7 @@ Proof.
   exploit sel_builtin_args_correct; eauto. intros (vl' & A & B).
   exploit external_call_mem_extends; eauto. intros (v' & m2' & D & E & F & _).
   econstructor; exists m2'; split.
+  apply plus_one.
   econstructor. eexact A. eapply external_call_symbols_preserved. eexact senv_preserved. eexact D.
   split; auto. apply sel_builtin_res_correct; auto.
 Qed. 
@@ -871,8 +869,8 @@ Lemma sel_builtin_correct:
   external_call ef ge vl m1 t v m2 ->
   env_lessdef e1 e1' -> Mem.extends m1 m1' ->
   exists e2' m2',
-     step tge (State f (sel_builtin optid ef al) k sp e1' m1')
-            t (State f Sskip k sp e2' m2')
+     plus step tge (State f (sel_builtin optid ef al) k sp e1' m1')
+                 t (State f Sskip k sp e2' m2')
   /\ env_lessdef (set_optvar optid v e1) e2'
   /\ Mem.extends m2 m2'.
 Proof.
@@ -880,15 +878,18 @@ Proof.
   exploit sel_exprlist_correct; eauto. intros (vl' & A & B).
   exploit external_call_mem_extends; eauto. intros (v' & m2' & D & E & F & _).
   unfold sel_builtin.
-  destruct optid as [id|]; eauto using sel_builtin_default_correct.
   destruct ef; eauto using sel_builtin_default_correct.
   destruct (lookup_builtin_function name sg) as [bf|] eqn:LKUP; eauto using sel_builtin_default_correct.
-  destruct (sel_known_builtin bf (sel_exprlist al)) as [a|] eqn:SKB; eauto using sel_builtin_default_correct.
   simpl in D. red in D. rewrite LKUP in D. inv D.
+  destruct optid as [id|]; eauto using sel_builtin_default_correct.
+- destruct (sel_known_builtin bf (sel_exprlist al)) as [a|] eqn:SKB; eauto using sel_builtin_default_correct.
   exploit eval_sel_known_builtin; eauto. intros (v'' & U & V).
   econstructor; exists m2'; split.
-  econstructor. eexact U.
+  apply plus_one. econstructor. eexact U.
   split; auto. apply set_var_lessdef; auto. apply Val.lessdef_trans with v'; auto.
+- exists e1', m2'; split.
+  eapply plus_two. constructor. constructor. auto.
+  simpl; auto.  
 Qed.
 
 (** If-conversion *)
@@ -1179,8 +1180,8 @@ Remark sel_builtin_nolabel:
   forall (hf: helper_functions) optid ef args, nolabel' (sel_builtin optid ef args).
 Proof.
   unfold sel_builtin; intros; red; intros.
-  destruct optid; auto. destruct ef; auto. destruct lookup_builtin_function; auto.
-  destruct sel_known_builtin; auto. 
+  destruct ef; auto. destruct lookup_builtin_function; auto.
+  destruct optid; auto. destruct sel_known_builtin; auto. 
 Qed. 
 
 Remark find_label_commut:
@@ -1243,34 +1244,34 @@ Definition measure (s: Cminor.state) : nat :=
 Lemma sel_step_correct:
   forall S1 t S2, Cminor.step ge S1 t S2 ->
   forall T1, match_states S1 T1 -> wt_state S1 ->
-  (exists T2, step tge T1 t T2 /\ match_states S2 T2)
+  (exists T2, plus step tge T1 t T2 /\ match_states S2 T2)
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat
   \/ (exists S3 T2, star Cminor.step ge S2 E0 S3 /\ step tge T1 t T2 /\ match_states S3 T2).
 Proof.
   induction 1; intros T1 ME WTS; inv ME; try (monadInv TS).
 - (* skip seq *)
-  inv MC. left; econstructor; split. econstructor. econstructor; eauto.
+  inv MC. left; econstructor; split. apply plus_one; econstructor. econstructor; eauto.
   inv H.
 - (* skip block *)
-  inv MC. left; econstructor; split. econstructor. econstructor; eauto.
+  inv MC. left; econstructor; split. apply plus_one; econstructor. econstructor; eauto.
   inv H.
 - (* skip call *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]].
   left; econstructor; split.
-  econstructor. eapply match_is_call_cont; eauto.
+  apply plus_one; econstructor. eapply match_is_call_cont; eauto.
   erewrite stackspace_function_translated; eauto.
   econstructor; eauto. eapply match_is_call_cont; eauto.
 - (* assign *)
   exploit sel_expr_correct; eauto. intros [v' [A B]].
   left; econstructor; split.
-  econstructor; eauto.
+  apply plus_one; econstructor; eauto.
   econstructor; eauto. apply set_var_lessdef; auto.
 - (* store *)
   exploit sel_expr_correct. try apply LINK. try apply HF. eexact H. eauto. eauto. intros [vaddr' [A B]].
   exploit sel_expr_correct. try apply LINK. try apply HF. eexact H0. eauto. eauto. intros [v' [C D]].
   exploit Mem.storev_extends; eauto. intros [m2' [P Q]].
   left; econstructor; split.
-  eapply eval_store; eauto.
+  apply plus_one; eapply eval_store; eauto.
   econstructor; eauto.
 - (* Scall *)
   exploit classify_call_correct; eauto.
@@ -1280,7 +1281,7 @@ Proof.
   exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
   exploit functions_translated; eauto. intros (cunit' & fd' & U & V & W).
   left; econstructor; split.
-  econstructor; eauto. econstructor; eauto.
+  apply plus_one; econstructor; eauto. econstructor; eauto.
   eapply sig_function_translated; eauto.
   eapply match_callstate with (cunit := cunit'); eauto.
   eapply match_cont_call with (cunit := cunit) (hf := hf); eauto.
@@ -1289,7 +1290,7 @@ Proof.
   exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
   exploit functions_translated; eauto. intros (cunit' & fd' & X & Y & Z).
   left; econstructor; split.
-  econstructor; eauto.
+  apply plus_one; econstructor; eauto.
   subst vf. econstructor; eauto. rewrite symbols_preserved; eauto.
   eapply sig_function_translated; eauto.
   eapply match_callstate with (cunit := cunit'); eauto.
@@ -1304,6 +1305,7 @@ Proof.
   exploit sel_exprlist_correct; eauto. intros [vargs' [C D]].
   exploit functions_translated; eauto. intros (cunit' & fd' & E & F & G).
   left; econstructor; split.
+  apply plus_one.
   exploit classify_call_correct. eexact LINK. eauto. eauto.
   destruct (classify_call (prog_defmap cunit)) as [ | id | ef]; intros.
   econstructor; eauto. econstructor; eauto. eapply sig_function_translated; eauto.
@@ -1317,7 +1319,7 @@ Proof.
   left; econstructor; split. eexact P. econstructor; eauto.
 - (* Seq *)
   left; econstructor; split.
-  constructor.
+  apply plus_one; constructor.
   econstructor; eauto. constructor; auto.
 - (* Sifthenelse *)
   simpl in TS. destruct (if_conversion (known_id f) env a s1 s2) as [s|] eqn:IFC; monadInv TS.
@@ -1329,21 +1331,21 @@ Proof.
 + exploit sel_expr_correct; eauto. intros [v' [A B]].
   assert (Val.bool_of_val v' b). inv B. auto. inv H0.
   left; exists (State f' (if b then x else x0) k' sp e' m'); split.
-  econstructor; eauto. eapply eval_condexpr_of_expr; eauto.
+  apply plus_one; econstructor; eauto. eapply eval_condexpr_of_expr; eauto.
   econstructor; eauto. destruct b; auto.
 - (* Sloop *)
-  left; econstructor; split. constructor. econstructor; eauto.
+  left; econstructor; split. apply plus_one; constructor. econstructor; eauto.
   constructor; auto. simpl; rewrite EQ; auto.
 - (* Sblock *)
-  left; econstructor; split. constructor. econstructor; eauto. constructor; auto.
+  left; econstructor; split. apply plus_one; constructor. econstructor; eauto. constructor; auto.
 - (* Sexit seq *)
-  inv MC. left; econstructor; split. constructor. econstructor; eauto.
+  inv MC. left; econstructor; split. apply plus_one; constructor. econstructor; eauto.
   inv H.
 - (* Sexit0 block *)
-  inv MC. left; econstructor; split. constructor. econstructor; eauto.
+  inv MC. left; econstructor; split. apply plus_one; constructor. econstructor; eauto.
   inv H.
 - (* SexitS block *)
-  inv MC. left; econstructor; split. constructor. econstructor; eauto.
+  inv MC. left; econstructor; split. apply plus_one; constructor. econstructor; eauto.
   inv H.
 - (* Sswitch *)
   inv H0; simpl in TS.
@@ -1351,29 +1353,29 @@ Proof.
   destruct (validate_switch Int.modulus default cases ct) eqn:VALID; inv TS.
   exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B.
   left; econstructor; split.
-  econstructor. eapply sel_switch_int_correct; eauto.
+  apply plus_one; econstructor. eapply sel_switch_int_correct; eauto.
   econstructor; eauto.
 + set (ct := compile_switch Int64.modulus default cases) in *.
   destruct (validate_switch Int64.modulus default cases ct) eqn:VALID; inv TS.
   exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B.
   left; econstructor; split.
-  econstructor. eapply sel_switch_long_correct; eauto.
+  apply plus_one; econstructor. eapply sel_switch_long_correct; eauto.
   econstructor; eauto.
 - (* Sreturn None *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
   erewrite <- stackspace_function_translated in P by eauto.
   left; econstructor; split.
-  econstructor. simpl; eauto.
+  apply plus_one; econstructor. simpl; eauto.
   econstructor; eauto. eapply call_cont_commut; eauto.
 - (* Sreturn Some *)
   exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]].
   erewrite <- stackspace_function_translated in P by eauto.
   exploit sel_expr_correct; eauto. intros [v' [A B]].
   left; econstructor; split.
-  econstructor; eauto.
+  apply plus_one; econstructor; eauto.
   econstructor; eauto. eapply call_cont_commut; eauto.
 - (* Slabel *)
-  left; econstructor; split. constructor. econstructor; eauto.
+  left; econstructor; split. apply plus_one; constructor. econstructor; eauto.
 - (* Sgoto *)
   assert (sel_stmt (prog_defmap cunit) (known_id f) env (Cminor.fn_body f) = OK (fn_body f')).
   { monadInv TF; simpl. congruence. }
@@ -1384,7 +1386,7 @@ Proof.
   as [[s'' k'']|] eqn:?; intros; try contradiction.
   destruct H1.
   left; econstructor; split.
-  econstructor; eauto.
+  apply plus_one; econstructor; eauto.
   econstructor; eauto.
 - (* internal function *)
   destruct TF as (hf & HF & TF). 
@@ -1392,7 +1394,7 @@ Proof.
   exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
   intros [m2' [A B]].
   left; econstructor; split.
-  econstructor; simpl; eauto.
+  apply plus_one; econstructor; simpl; eauto.
   econstructor; simpl; eauto.
   apply match_cont_other; auto.
   apply set_locals_lessdef. apply set_params_lessdef; auto.
@@ -1402,7 +1404,7 @@ Proof.
   exploit external_call_mem_extends; eauto.
   intros [vres' [m2 [A [B [C D]]]]].
   left; econstructor; split.
-  econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  apply plus_one; econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
 - (* external call turned into a Sbuiltin *)
   exploit sel_builtin_correct; eauto. intros (e2' & m2' & P & Q & R).
@@ -1410,7 +1412,7 @@ Proof.
 - (* return *)
   inv MC.
   left; econstructor; split.
-  econstructor.
+  apply plus_one; econstructor.
   econstructor; eauto. destruct optid; simpl; auto. apply set_var_lessdef; auto.
 - (* return of an external call turned into a Sbuiltin *)
   right; left; split. simpl; omega. split. auto. econstructor; eauto.
@@ -1453,7 +1455,7 @@ Proof.
   unfold MS.
   exploit sel_step_correct; eauto.
   intros [(T2 & D & E) | [(D & E & F) | (S3 & T2 & D & E & F)]].
-+ exists S2, T2. intuition auto using star_refl, plus_one.
++ exists S2, T2. intuition auto using star_refl.
 + subst t. exists S2, T1. intuition auto using star_refl.
 + assert (wt_state S3) by (eapply subject_reduction_star; eauto using wt_prog).
   exists S3, T2. intuition auto using plus_one.