Modest optimization of leaf functions

Leaf functions are functions that do not call any other function.  For leaf functions, it is not necessary to save the LR register on function entry nor to reload LR on function return, since LR contains the correct return address throughout the function's execution.

This commit suppresses the reloading of LR before returning from a leaf function.  LR is still saved on the stack on function entry, because doing otherwise would require extensive changes in the Stacking pass of CompCert.  However, preliminary experiments indicate that we get good speedups by avoiding to reload LR, while avoiding to save LR makes little difference in speed.

To support this optimization and its proof:
- Mach is extended with a `is_leaf_function` Boolean function and a `wf_state` predicate to provide the semantic characterization.
- Asmgenproof* is extended with a `important_preg` Boolean function that means "data register or LR".  A number of lemmas that used to show preservation of data registers now show preservation of LR as well.

4 files changed, 241 insertions, 46 deletions

diff --git a/backend/Mach.v b/backend/Mach.v
index 212088f3..839a25bd 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -189,13 +189,19 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
   | i1 :: il => if is_label lbl i1 then Some il else find_label lbl il
   end.
 
-Lemma find_label_incl:
-  forall lbl c c', find_label lbl c = Some c' -> incl c' c.
+Lemma find_label_tail:
+  forall lbl c c', find_label lbl c = Some c' -> is_tail c' c.
 Proof.
   induction c; simpl; intros. discriminate.
   destruct (is_label lbl a). inv H. auto with coqlib. eauto with coqlib.
 Qed.
 
+Lemma find_label_incl:
+  forall lbl c c', find_label lbl c = Some c' -> incl c' c.
+Proof.
+  intros; red; intros. eapply is_tail_incl; eauto. eapply find_label_tail; eauto.
+Qed.
+
 Section RELSEM.
 
 Variable return_address_offset: function -> code -> ptrofs -> Prop.
@@ -426,3 +432,70 @@ Inductive final_state: state -> int -> Prop :=
 
 Definition semantics (rao: function -> code -> ptrofs -> Prop) (p: program) :=
   Semantics (step rao) (initial_state p) final_state (Genv.globalenv p).
+
+(** * Leaf functions *)
+
+(** A leaf function is a function that contains no [Mcall] instruction. *)
+
+Definition is_leaf_function (f: function) : bool :=
+  List.forallb
+    (fun i => match i with Mcall _ _ => false | _ => true end)
+    f.(fn_code).  
+
+(** Semantic characterization of leaf functions: 
+    functions in the call stack are never leaf functions. *)
+
+Section WF_STATES.
+
+Variable rao: function -> code -> ptrofs -> Prop.
+
+Variable ge: genv.
+
+Inductive wf_frame: stackframe -> Prop :=
+  | wf_stackframe_intro: forall fb sp ra c f
+        (CODE: Genv.find_funct_ptr ge fb = Some (Internal f))
+        (LEAF: is_leaf_function f = false)
+        (TAIL: is_tail c f.(fn_code)),
+      wf_frame (Stackframe fb sp ra c).
+
+Inductive wf_state: state -> Prop :=
+  | wf_normal_state: forall s fb sp c rs m f
+        (STACK: Forall wf_frame s)
+        (CODE: Genv.find_funct_ptr ge fb = Some (Internal f))
+        (TAIL: is_tail c f.(fn_code)),
+      wf_state (State s fb sp c rs m)
+  | wf_call_state: forall s fb rs m
+        (STACK: Forall wf_frame s),
+      wf_state (Callstate s fb rs m)
+  | wf_return_state: forall s rs m
+        (STACK: Forall wf_frame s),
+      wf_state (Returnstate s rs m).
+
+Lemma wf_step:
+  forall S1 t S2, step rao ge S1 t S2 -> wf_state S1 -> wf_state S2.
+Proof.
+  induction 1; intros WF; inv WF; try (econstructor; now eauto with coqlib).
+- (* call *)
+  assert (f0 = f) by congruence. subst f0.
+  constructor.
+  constructor; auto. econstructor; eauto with coqlib.
+  destruct (is_leaf_function f) eqn:E; auto.
+  unfold is_leaf_function in E; rewrite forallb_forall in E. 
+  symmetry. apply (E (Mcall sig ros)). eapply is_tail_in; eauto.
+- (* goto *)
+  assert (f0 = f) by congruence. subst f0. econstructor; eauto using find_label_tail.  
+- (* cond *)
+  assert (f0 = f) by congruence. subst f0. econstructor; eauto using find_label_tail.  
+- (* jumptable *)
+  assert (f0 = f) by congruence. subst f0. econstructor; eauto using find_label_tail.  
+- (* return *)
+  inv STACK. inv H1. econstructor; eauto.
+Qed.
+
+End WF_STATES.
+
+Lemma wf_initial:
+  forall p S, initial_state p S -> wf_state (Genv.globalenv p) S.
+Proof.
+  intros. inv H. fold ge. constructor. constructor.
+Qed.
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index fc04b15d..774f58f9 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -672,10 +672,14 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
       do r <- ireg_of arg;
       OK (Pbtbl r tbl :: k)
   | Mreturn =>
-      OK (Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 ::
-          Pmtlr GPR0 ::
-          Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
-          Pblr :: k)
+      if is_leaf_function f then
+        OK (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
+            Pblr :: k)
+      else
+        OK (Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 ::
+            Pmtlr GPR0 ::
+            Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
+            Pblr :: k)
   end.
 
 (** Translation of a code sequence *)
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 6f0390b9..68c19db0 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -385,7 +385,8 @@ Inductive match_states: Mach.state -> Asm.state -> Prop :=
         (MEXT: Mem.extends m m')
         (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc)
         (AG: agree ms sp rs)
-        (DXP: ep = true -> rs#GPR11 = parent_sp s),
+        (DXP: ep = true -> rs#GPR11 = parent_sp s)
+        (LEAF: is_leaf_function f = true -> rs#LR = parent_ra s),
       match_states (Mach.State s fb sp c ms m)
                    (Asm.State rs m')
   | match_states_call:
@@ -412,20 +413,22 @@ Lemma exec_straight_steps:
   Mem.extends m2 m2' ->
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
   transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
+  (is_leaf_function f = true -> rs1#LR = parent_ra s) ->
   (forall k c (TR: transl_instr f i ep k = OK c),
    exists rs2,
        exec_straight tge tf c rs1 m1' k rs2 m2'
     /\ agree ms2 sp rs2
-    /\ (it1_is_parent ep i = true -> rs2#GPR11 = parent_sp s)) ->
+    /\ (it1_is_parent ep i = true -> rs2#GPR11 = parent_sp s)
+    /\ rs2#LR = rs1#LR) ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
   match_states (Mach.State s fb sp c ms2 m2) st'.
 Proof.
-  intros. inversion H2. subst. monadInv H7.
-  exploit H3; eauto. intros [rs2 [A [B C]]].
+  intros. inversion H2. subst. monadInv H8.
+  exploit H4; eauto. intros (rs2 & A & B & C & D).
   exists (State rs2 m2'); split.
   eapply exec_straight_exec; eauto.
-  econstructor; eauto. eapply exec_straight_at; eauto.
+  econstructor; eauto. eapply exec_straight_at; eauto. rewrite D; auto.
 Qed.
 
 Lemma exec_straight_steps_goto:
@@ -436,19 +439,21 @@ Lemma exec_straight_steps_goto:
   Mach.find_label lbl f.(Mach.fn_code) = Some c' ->
   transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc ->
   it1_is_parent ep i = false ->
+  (is_leaf_function f = true -> rs1#LR = parent_ra s) ->
   (forall k c (TR: transl_instr f i ep k = OK c),
    exists jmp, exists k', exists rs2,
        exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2'
     /\ agree ms2 sp rs2
-    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') ->
+    /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2'
+    /\ rs2#LR = rs1#LR) ->
   exists st',
   plus step tge (State rs1 m1') E0 st' /\
   match_states (Mach.State s fb sp c' ms2 m2) st'.
 Proof.
-  intros. inversion H3. subst. monadInv H9.
-  exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]].
-  generalize (functions_transl _ _ _ H7 H8); intro FN.
-  generalize (transf_function_no_overflow _ _ H8); intro NOOV.
+  intros. inversion H3. subst. monadInv H10.
+  exploit H6; eauto. intros (jmp & k' & rs2 & A & B & C & D).
+  generalize (functions_transl _ _ _ H8 H9); intro FN.
+  generalize (transf_function_no_overflow _ _ H9); intro NOOV.
   exploit exec_straight_steps_2; eauto.
   intros [ofs' [PC2 CT2]].
   exploit find_label_goto_label; eauto.
@@ -463,6 +468,7 @@ Proof.
   econstructor; eauto.
   apply agree_exten with rs2; auto with asmgen.
   congruence.
+  intros. rewrite OTH by congruence. rewrite D. auto.
 Qed.
 
 (** We need to show that, in the simulation diagram, we cannot
@@ -490,7 +496,7 @@ Qed.
 
 Theorem step_simulation:
   forall S1 t S2, Mach.step return_address_offset ge S1 t S2 ->
-  forall S1' (MS: match_states S1 S1'),
+  forall S1' (MS: match_states S1 S1') (WF: wf_state ge S1),
   (exists S2', plus step tge S1' t S2' /\ match_states S2 S2')
   \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat.
 Proof.
@@ -499,7 +505,9 @@ Proof.
 - (* Mlabel *)
   left; eapply exec_straight_steps; eauto; intros.
   monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split. apply agree_nextinstr; auto. simpl; congruence.
+  split. apply agree_nextinstr; auto. 
+  split. simpl; congruence.
+  auto with asmgen.
 
 - (* Mgetstack *)
   unfold load_stack in H.
@@ -509,7 +517,8 @@ Proof.
   exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q R]]].
   exists rs'; split. eauto.
   split. eapply agree_set_mreg; eauto with asmgen. congruence.
-  simpl; congruence.
+  split. simpl; congruence.
+  apply R; auto with asmgen.
 
 - (* Msetstack *)
   unfold store_stack in H.
@@ -520,7 +529,8 @@ Proof.
   exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
   exists rs'; split. eauto.
   split. eapply agree_undef_regs; eauto with asmgen.
-  simpl; intros. rewrite Q; auto with asmgen.
+  split. simpl; intros. rewrite Q; auto with asmgen.
+  rewrite Q; auto with asmgen.
 
 - (* Mgetparam *)
   assert (f0 = f) by congruence; subst f0.
@@ -539,8 +549,9 @@ Opaque loadind.
   intros [rs1 [P [Q R]]].
   exists rs1; split. eauto.
   split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen.
-  simpl; intros. rewrite R; auto with asmgen.
+  split. simpl; intros. rewrite R; auto with asmgen.
   apply preg_of_not_GPR11; auto.
+  apply R; auto with asmgen.
 (* GPR11 does not contain parent *)
   monadInv TR.
   exploit loadind_correct. eexact EQ0. eauto. congruence. intros [rs1 [P [Q R]]]. simpl in Q.
@@ -551,8 +562,9 @@ Opaque loadind.
   instantiate (1 := rs1#GPR11 <- (rs2#GPR11)). intros.
   rewrite Pregmap.gso; auto with asmgen.
   congruence. intros. unfold Pregmap.set. destruct (PregEq.eq r' GPR11). congruence. auto with asmgen.
-  simpl; intros. rewrite U; auto with asmgen.
+  split. simpl; intros. rewrite U; auto with asmgen.
   apply preg_of_not_GPR11; auto.
+  rewrite U; auto with asmgen.
 
 - (* Mop *)
   assert (eval_operation tge sp op rs##args m = Some v).
@@ -562,10 +574,11 @@ Opaque loadind.
   left; eapply exec_straight_steps; eauto; intros. simpl in TR.
   exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]].
   exists rs2; split. eauto. split. auto.
-  destruct op; simpl; try discriminate. intros.
+  split. destruct op; simpl; try discriminate. intros.
   destruct (andb_prop _ _ H1); clear H1.
   rewrite R; auto. apply preg_of_not_GPR11; auto.
   change (destroyed_by_op Omove) with (@nil mreg). simpl; auto.
+  apply R; auto with asmgen. 
 
 - (* Mload *)
   assert (eval_addressing tge sp addr rs##args = Some a).
@@ -578,7 +591,8 @@ Opaque loadind.
   exists rs2; split. eauto.
   split. eapply agree_set_undef_mreg; eauto. congruence.
   intros; auto with asmgen.
-  simpl; congruence.
+  split. simpl; congruence.
+  apply R; auto with asmgen.
 
 - (* Mstore *)
   assert (eval_addressing tge sp addr rs##args = Some a).
@@ -591,7 +605,8 @@ Opaque loadind.
   intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]].
   exists rs2; split. eauto.
   split. eapply agree_undef_regs; eauto with asmgen.
-  simpl; congruence.
+  split. simpl; congruence.
+  apply Q; auto with asmgen.
 
 - (* Mcall *)
   assert (f0 = f) by congruence.  subst f0.
@@ -757,6 +772,8 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   apply agree_nextinstr. eapply agree_set_res; auto.
   eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto.
   congruence.
+  intros. Simpl. rewrite set_res_other by auto.
+  rewrite undef_regs_other_2; auto with asmgen.
 
 - (* Mgoto *)
   assert (f0 = f) by congruence. subst f0.
@@ -770,6 +787,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   econstructor; eauto.
   eapply agree_exten; eauto with asmgen.
   congruence.
+  rewrite INV by congruence; auto.
 
 - (* Mcond true *)
   assert (f0 = f) by congruence. subst f0.
@@ -782,11 +800,13 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   (* Pbt, taken *)
   econstructor; econstructor; econstructor; split. eexact A.
   split. eapply agree_exten; eauto with asmgen.
-  simpl. rewrite B. reflexivity.
+  split. simpl. rewrite B. reflexivity.
+  auto with asmgen.
   (* Pbf, taken *)
   econstructor; econstructor; econstructor; split. eexact A.
   split. eapply agree_exten; eauto with asmgen.
-  simpl. rewrite B. reflexivity.
+  split. simpl. rewrite B. reflexivity.
+  auto with asmgen.
 
 - (* Mcond false *)
   exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC.
@@ -800,7 +820,8 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   apply exec_straight_one. simpl. rewrite B. reflexivity. auto.
   split. eapply agree_exten; eauto with asmgen.
   intros; Simpl.
-  simpl. congruence.
+  split. simpl. congruence.
+  Simpl. 
 
 - (* Mjumptable *)
   assert (f0 = f) by congruence. subst f0.
@@ -822,6 +843,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
 Local Transparent destroyed_by_jumptable.
   simpl. intros. rewrite C; auto with asmgen. Simpl.
   congruence.
+  intros. rewrite C by auto with asmgen. Simpl. 
 
 - (* Mreturn *)
   assert (f0 = f) by congruence. subst f0.
@@ -834,7 +856,36 @@ Local Transparent destroyed_by_jumptable.
   exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]].
   exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D.
   exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]].
-  monadInv H6.
+  monadInv H6. destruct (is_leaf_function f) eqn:ISLEAF; monadInv EQ0.
++ (* leaf function *)
+  set (rs2 := nextinstr (rs0#GPR1 <- (parent_sp s))).
+  set (rs3 := rs2#PC <- (parent_ra s)).
+  assert (exec_straight tge tf
+           (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pblr :: x) rs0 m'0
+           (Pblr :: x) rs2 m2').
+  simpl. apply exec_straight_one. 
+  simpl. rewrite A.
+  rewrite <- (sp_val _ _ _ AG). rewrite E. auto.
+  auto.
+  left; exists (State rs3 m2'); split.
+  (* execution *)
+  apply plus_right' with E0 (State rs2 m2') E0.
+  eapply exec_straight_exec; eauto.
+  econstructor.
+  change (rs2 PC) with (Val.offset_ptr (rs0 PC) Ptrofs.one).
+  rewrite <- H3. simpl. eauto.
+  eapply functions_transl; eauto.
+  eapply find_instr_tail.
+  eapply code_tail_next_int; eauto.
+  simpl. change (rs2 LR) with (rs0 LR). rewrite LEAF by auto. reflexivity. 
+  traceEq.
+  (* match states *)
+  econstructor; eauto.
+  assert (AG2: agree rs (parent_sp s) rs2).
+    unfold rs2. apply agree_nextinstr. eapply agree_change_sp; eauto.
+    eapply parent_sp_def; eauto.
+  unfold rs3; auto with asmgen.
++ (* non-leaf function *)
   set (rs2 := nextinstr (rs0#GPR0 <- (parent_ra s))).
   set (rs3 := nextinstr (rs2#LR <- (parent_ra s))).
   set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))).
@@ -949,7 +1000,9 @@ Local Transparent destroyed_by_jumptable.
   inv STACKS. simpl in *.
   right. split. omega. split. auto.
   rewrite <- ATPC in H5.
-  econstructor; eauto. congruence.
+  econstructor; eauto.
+  congruence.
+  inv WF. inv STACK. inv H1. congruence.
 Qed.
 
 Lemma transf_initial_states:
@@ -984,11 +1037,17 @@ Qed.
 Theorem transf_program_correct:
   forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
 Proof.
-  eapply forward_simulation_star with (measure := measure).
-  apply senv_preserved.
-  eexact transf_initial_states.
-  eexact transf_final_states.
-  exact step_simulation.
+  eapply forward_simulation_star with
+     (measure := measure)
+     (match_states := fun S1 S2 => match_states S1 S2 /\ wf_state ge S1).
+- apply senv_preserved.
+- simpl; intros. exploit transf_initial_states; eauto. intros (s2 & A & B).
+  exists s2; intuition auto. apply wf_initial; auto. 
+- simpl; intros. destruct H as [MS WF]. eapply transf_final_states; eauto.
+- simpl; intros. destruct H0 as [MS WF]. 
+  exploit step_simulation; eauto. intros [ (s2' & A & B) | (A & B & C) ].
++ left; exists s2'; intuition auto. eapply wf_step; eauto. 
++ right; intuition auto. eapply wf_step; eauto.
 Qed.
 
 End PRESERVATION.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index a7dcf41e..fe496825 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -110,6 +110,49 @@ Proof.
   intros. rewrite Val.add_assoc. rewrite low_high_half. apply add_zero_symbol_address.
 Qed.
 
+(** * Useful properties of registers *)
+
+(** [important_preg] extends [data_preg] by tracking the LR register as well.
+    It is used to state that a code sequence modifies no data registers
+    and does not modify LR either. *)
+
+Definition important_preg (r: preg) : bool :=
+  match r with
+  | IR GPR0 => false
+  | PC => false    | CTR => false
+  | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false
+  | CARRY => false
+  | _ => true
+  end.
+
+Lemma important_diff:
+  forall r r',
+  important_preg r = true -> important_preg r' = false -> r <> r'.
+Proof.
+  congruence.
+Qed.
+Hint Resolve important_diff: asmgen.
+
+Lemma important_data_preg_1:
+  forall r, data_preg r = true -> important_preg r = true.    
+Proof.
+  destruct r; simpl; auto; discriminate.
+Qed.
+
+Lemma important_data_preg_2:
+  forall r, important_preg r = false -> data_preg r = false.
+Proof.
+  intros. destruct (data_preg r) eqn:E; auto. apply important_data_preg_1 in E. congruence.
+Qed.  
+
+Hint Resolve important_data_preg_1 important_data_preg_2: asmgen.
+
+Lemma nextinstr_inv2:
+  forall r rs, important_preg r = true -> (nextinstr rs)#r = rs#r.
+Proof.
+  intros. apply nextinstr_inv. red; intro; subst; discriminate.
+Qed.
+
 (** Useful properties of the GPR0 registers. *)
 
 Lemma gpr_or_zero_not_zero:
@@ -138,11 +181,27 @@ Proof.
 Qed.
 Hint Resolve ireg_of_not_GPR0': asmgen.
 
+(** Useful properties of the LR register *)
+
+Lemma preg_of_not_LR:
+  forall r, LR <> preg_of r.
+Proof.
+  intros. auto using sym_not_equal with asmgen.
+Qed.
+
+Lemma preg_notin_LR:
+  forall rl, preg_notin LR rl.
+Proof.
+  intros. rewrite preg_notin_charact. intros. apply preg_of_not_LR. 
+Qed.
+
+Hint Resolve preg_of_not_LR preg_notin_LR: asmgen.
+      
 (** Useful simplification tactic *)
 
 Ltac Simplif :=
   ((rewrite nextinstr_inv by eauto with asmgen)
-  || (rewrite nextinstr_inv1 by eauto with asmgen)
+  || (rewrite nextinstr_inv2 by eauto with asmgen)
   || (rewrite Pregmap.gss)
   || (rewrite nextinstr_pc)
   || (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen.
@@ -291,7 +350,7 @@ Lemma andimm_base_correct:
      exec_straight ge fn (andimm_base r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = v
   /\ rs'#CR0_2 = Val.cmp Ceq v Vzero
-  /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
+  /\ forall r', important_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
 Proof.
   intros. unfold andimm_base.
   case (Int.eq (high_u n) Int.zero).
@@ -336,7 +395,7 @@ Lemma andimm_correct:
   exists rs',
      exec_straight ge fn (andimm r1 r2 n k) rs m  k rs' m
   /\ rs'#r1 = Val.and rs#r2 (Vint n)
-  /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
+  /\ forall r', important_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
 Proof.
   intros. unfold andimm. destruct (is_rlw_mask n).
   (* turned into rlw *)
@@ -416,7 +475,7 @@ Lemma rolm_correct:
   exists rs',
      exec_straight ge fn (rolm r1 r2 amount mask k) rs m  k rs' m
   /\ rs'#r1 = Val.rolm rs#r2 amount mask
-  /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
+  /\ forall r', important_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'.
 Proof.
   intros. unfold rolm. destruct (is_rlw_mask mask).
   (* rlwinm *)
@@ -610,7 +669,7 @@ Lemma transl_cond_correct_1:
        (if snd (crbit_for_cond cond)
         then Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)
         else Val.notbool (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)))
-  /\ forall r, data_preg r = true -> rs'#r = rs#r.
+  /\ forall r, important_preg r = true -> rs'#r = rs#r.
 Proof.
   intros.
 Opaque Int.eq.
@@ -708,7 +767,7 @@ Lemma transl_cond_correct_2:
        (if snd (crbit_for_cond cond)
         then Val.of_bool b
         else Val.notbool (Val.of_bool b))
-  /\ forall r, data_preg r = true -> rs'#r = rs#r.
+  /\ forall r, important_preg r = true -> rs'#r = rs#r.
 Proof.
   intros.
   replace (Val.of_bool b)
@@ -735,7 +794,7 @@ Proof.
   exploit transl_cond_correct_2. eauto.
     eapply eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto.
   intros [rs' [A [B C]]].
-  exists rs'; split. eauto. split. auto. apply agree_exten with rs; auto.
+  exists rs'; split. eauto. split. auto. apply agree_exten with rs; auto with asmgen.
 Qed.
 
 (** Translation of condition operators *)
@@ -792,7 +851,7 @@ Lemma transl_cond_op_correct:
   exists rs',
      exec_straight ge fn c rs m k rs' m
   /\ rs'#(preg_of r) = Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)
-  /\ forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r'.
+  /\ forall r', important_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r'.
 Proof.
   intros until args. unfold transl_cond_op.
   destruct (classify_condition cond args); intros; monadInv H; simpl;
@@ -857,7 +916,7 @@ Lemma transl_op_correct_aux:
   exists rs',
      exec_straight ge fn c rs m k rs' m
   /\ Val.lessdef v rs'#(preg_of res)
-  /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r.
+  /\ forall r, important_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r.
 Proof.
   assert (SAME: forall v1 v2, v1 = v2 -> Val.lessdef v2 v1). { intros; subst; auto. }
 Opaque Int.eq.
@@ -1000,14 +1059,14 @@ Lemma transl_op_correct:
   exists rs',
      exec_straight ge fn c rs m' k rs' m'
   /\ agree (Regmap.set res v (Mach.undef_regs (destroyed_by_op op) ms)) sp rs'
-  /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r.
+  /\ forall r, important_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r.
 Proof.
   intros.
   exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto.
   intros [v' [A B]].  rewrite (sp_val _ _ _ H0) in A.
   exploit transl_op_correct_aux; eauto. intros [rs' [P [Q R]]].
   exists rs'; split. eexact P.
-  split. apply agree_set_undef_mreg with rs; auto. eapply Val.lessdef_trans; eauto.
+  split. apply agree_set_undef_mreg with rs; auto with asmgen. eapply Val.lessdef_trans; eauto.
   auto.
 Qed.