Revised renumbering of nodes and registers so that main function is not shifted by 1

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2346 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 114 insertions, 48 deletions

diff --git a/backend/Inlining.v b/backend/Inlining.v
index 683d190..c6df3de 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -143,9 +143,9 @@ Qed.
 
 Program Definition add_instr (i: instruction): mon node :=
   fun s =>
-    let pc := Psucc s.(st_nextnode) in
+    let pc := s.(st_nextnode) in
     R pc
-      (mkstate s.(st_nextreg) pc (PTree.set pc i s.(st_code)) s.(st_stksize))
+      (mkstate s.(st_nextreg) (Psucc pc) (PTree.set pc i s.(st_code)) s.(st_stksize))
       _.
 Next Obligation.
   intros; constructor; simpl; xomega.
@@ -213,9 +213,11 @@ Record context: Type := mkcontext {
 
 (** The following functions "shift" (relocate) PCs, registers, operations, etc. *)
 
-Definition spc (ctx: context) (pc: node) := Pplus pc ctx.(dpc).
+Definition shiftpos (p amount: positive) := Ppred (Pplus p amount).
 
-Definition sreg (ctx: context) (r: reg) := Pplus r ctx.(dreg).
+Definition spc (ctx: context) (pc: node) := shiftpos pc ctx.(dpc).
+
+Definition sreg (ctx: context) (r: reg) := shiftpos r ctx.(dreg).
 
 Definition sregs (ctx: context) (rl: list reg) := List.map (sreg ctx) rl.
 
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 15d0b28..8e20442 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -72,23 +72,33 @@ Qed.
 (** ** Properties of contexts and relocations *)
 
 Remark sreg_below_diff:
-  forall ctx r r', Ple r' ctx.(dreg) -> sreg ctx r <> r'.
+  forall ctx r r', Plt r' ctx.(dreg) -> sreg ctx r <> r'.
 Proof.
-  intros. unfold sreg. xomega. 
+  intros. zify. unfold sreg; rewrite shiftpos_eq. xomega. 
 Qed.
 
 Remark context_below_diff:
   forall ctx1 ctx2 r1 r2,
   context_below ctx1 ctx2 -> Ple r1 ctx1.(mreg) -> sreg ctx1 r1 <> sreg ctx2 r2.
 Proof.
-  intros. red in H. unfold sreg. xomega. 
+  intros. red in H. zify. unfold sreg; rewrite ! shiftpos_eq. xomega.
 Qed.
 
+Remark context_below_lt:
+  forall ctx1 ctx2 r, context_below ctx1 ctx2 -> Ple r ctx1.(mreg) -> Plt (sreg ctx1 r) ctx2.(dreg).
+Proof.
+  intros. red in H. unfold Plt; zify. unfold sreg; rewrite shiftpos_eq. 
+  xomega.
+Qed.
+
+(*
 Remark context_below_le:
   forall ctx1 ctx2 r, context_below ctx1 ctx2 -> Ple r ctx1.(mreg) -> Ple (sreg ctx1 r) ctx2.(dreg).
 Proof.
-  intros. red in H. unfold sreg. xomega.
+  intros. red in H. unfold Ple; zify. unfold sreg; rewrite shiftpos_eq. 
+  xomega.
 Qed.
+*)
 
 (** ** Agreement between register sets before and after inlining. *)
 
@@ -145,7 +155,7 @@ Proof.
   unfold agree_regs; intros. destruct H. split; intros.
   repeat rewrite Regmap.gsspec. 
   destruct (peq r0 r). subst r0. rewrite peq_true. auto.
-  rewrite peq_false. auto. unfold sreg; xomega. 
+  rewrite peq_false. auto. apply shiftpos_diff; auto. 
   rewrite Regmap.gso. auto. xomega. 
 Qed.
 
@@ -157,7 +167,7 @@ Proof.
   unfold agree_regs; intros. destruct H. split; intros.
   repeat rewrite Regmap.gsspec. 
   destruct (peq r0 r). subst r0. rewrite peq_true. auto.
-  rewrite peq_false. auto. unfold sreg; xomega.
+  rewrite peq_false. auto. apply shiftpos_diff; auto. 
   rewrite Regmap.gsspec. destruct (peq r0 r); auto. 
 Qed.
 
@@ -175,11 +185,13 @@ Qed.
 Lemma agree_regs_invariant:
   forall F ctx rs rs1 rs2,
   agree_regs F ctx rs rs1 ->
-  (forall r, Plt ctx.(dreg) r -> Ple r (ctx.(dreg) + ctx.(mreg)) -> rs2#r = rs1#r) ->
+  (forall r, Ple ctx.(dreg) r -> Plt r (ctx.(dreg) + ctx.(mreg)) -> rs2#r = rs1#r) ->
   agree_regs F ctx rs rs2.
 Proof.
   unfold agree_regs; intros. destruct H. split; intros.
-  rewrite H0. auto. unfold sreg; xomega. unfold sreg; xomega. 
+  rewrite H0. auto. 
+  apply shiftpos_above.
+  eapply Plt_le_trans. apply shiftpos_below. xomega.
   apply H1; auto.
 Qed.
 
@@ -222,7 +234,7 @@ Lemma tr_moves_init_regs:
     star step tge (State stk f sp pc1 rs1 m)
                E0 (State stk f sp pc2 rs2 m)
   /\ agree_regs F ctx2 (init_regs vl rdsts) rs2
-  /\ forall r, Ple r ctx2.(dreg) -> rs2#r = rs1#r.
+  /\ forall r, Plt r ctx2.(dreg) -> rs2#r = rs1#r.
 Proof.
   induction rdsts; simpl; intros.
 (* rdsts = nil *)
@@ -236,7 +248,7 @@ Proof.
   split. eapply star_right. eauto. eapply exec_Iop; eauto. traceEq.
   split. destruct H3 as [[P Q] | [P Q]].
   subst a1. eapply agree_set_reg_undef; eauto.
-  eapply agree_set_reg; eauto. rewrite C; auto. apply context_below_le; auto.
+  eapply agree_set_reg; eauto. rewrite C; auto.  apply context_below_lt; auto.
   intros. rewrite Regmap.gso. auto. apply sym_not_equal. eapply sreg_below_diff; eauto.
   destruct H2; discriminate.
 Qed.
@@ -502,7 +514,7 @@ with match_stacks_inside_invariant:
   forall stk stk' f' ctx sp' rs1, 
   match_stacks_inside F m m' stk stk' f' ctx sp' rs1 ->
   forall rs2
-         (RS: forall r, Ple r ctx.(dreg) -> rs2#r = rs1#r)
+         (RS: forall r, Plt r ctx.(dreg) -> rs2#r = rs1#r)
          (INJ: forall b1 b2 delta, 
                F1 b1 = Some(b2, delta) -> Ple b2 sp' -> F b1 = Some(b2, delta))
          (PERM1: forall b1 b2 delta ofs,
@@ -585,7 +597,7 @@ Lemma match_stacks_inside_set_reg:
   match_stacks_inside F m m' stk stk' f' ctx sp' (rs'#(sreg ctx r) <- v).
 Proof.
   intros. eapply match_stacks_inside_invariant; eauto. 
-  intros. apply Regmap.gso. unfold sreg. xomega. 
+  intros. apply Regmap.gso. zify. unfold sreg; rewrite shiftpos_eq. xomega.
 Qed.
 
 (** Preservation by a memory store *)
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index f41f376..0fc4613 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -127,6 +127,55 @@ Proof.
   eapply Ple_trans. 2: eapply Pmax_r. eauto. 
 Qed.
 
+(** ** Properties of shifting *)
+
+Lemma shiftpos_eq: forall x y, Zpos (shiftpos x y) = (Zpos x + Zpos y) - 1.
+Proof.
+  intros. unfold shiftpos. zify.  rewrite Pos2Z.inj_sub. auto.
+  zify. omega.
+Qed.
+
+Lemma shiftpos_inj: 
+  forall x y n, shiftpos x n = shiftpos y n -> x = y.
+Proof.
+  intros.
+  assert (Zpos (shiftpos x n) = Zpos (shiftpos y n)) by congruence.
+  rewrite ! shiftpos_eq in H0. 
+  assert (Z.pos x = Z.pos y) by omega.
+  congruence.
+Qed.
+
+Lemma shiftpos_diff:
+  forall x y n, x <> y -> shiftpos x n <> shiftpos y n.
+Proof.
+  intros; red; intros. elim H. eapply shiftpos_inj; eauto.
+Qed.
+
+Lemma shiftpos_above:
+  forall x n, Ple n (shiftpos x n).
+Proof.
+  intros. unfold Ple; zify. rewrite shiftpos_eq. xomega. 
+Qed.
+
+Lemma shiftpos_not_below:
+  forall x n, Plt (shiftpos x n) n -> False.
+Proof.
+  intros. generalize (shiftpos_above x n). xomega. 
+Qed.
+
+Lemma shiftpos_below:
+  forall x n, Plt (shiftpos x n) (Pplus x n).
+Proof.
+  intros. unfold Plt; zify. rewrite shiftpos_eq. omega. 
+Qed.
+
+Lemma shiftpos_le:
+  forall x y n, Ple x y -> Ple (shiftpos x n) (shiftpos y n).
+Proof.
+  intros. unfold Ple in *; zify. rewrite ! shiftpos_eq. omega. 
+Qed.
+
+
 (** ** Working with the state monad *)
 
 Remark bind_inversion:
@@ -223,7 +272,7 @@ Inductive tr_moves (c: code) : node -> list reg -> list reg -> node -> Prop :=
 Lemma add_moves_unchanged:
   forall srcs dsts pc2 s pc1 s' i pc,
   add_moves srcs dsts pc2 s = R pc1 s' i ->
-  Ple pc s.(st_nextnode) \/ Plt s'.(st_nextnode) pc ->
+  Plt pc s.(st_nextnode) \/ Ple s'.(st_nextnode) pc ->
   s'.(st_code)!pc = s.(st_code)!pc.
 Proof.
   induction srcs; simpl; intros. 
@@ -237,7 +286,7 @@ Qed.
 Lemma add_moves_spec:
   forall srcs dsts pc2 s pc1 s' i c,
   add_moves srcs dsts pc2 s = R pc1 s' i ->
-  (forall pc, Plt s.(st_nextnode) pc -> Ple pc s'.(st_nextnode) -> c!pc = s'.(st_code)!pc) ->
+  (forall pc, Ple s.(st_nextnode) pc -> Plt pc s'.(st_nextnode) -> c!pc = s'.(st_code)!pc) ->
   tr_moves c pc1 srcs dsts pc2.
 Proof.
   induction srcs; simpl; intros. 
@@ -360,7 +409,7 @@ Hypothesis rec_unchanged:
   forall fe' (L: (size_fenv fe' < size_fenv fe)%nat) ctx f s x s' i pc,
   rec fe' L ctx f s = R x s' i ->
   Ple ctx.(dpc) s.(st_nextnode) ->
-  Ple pc ctx.(dpc) ->
+  Plt pc ctx.(dpc) ->
   s'.(st_code)!pc = s.(st_code)!pc.
 
 Remark set_instr_other:
@@ -385,7 +434,7 @@ Lemma expand_instr_unchanged:
   forall ctx pc instr s x s' i pc',
   expand_instr fe rec ctx pc instr s = R x s' i ->
   Ple ctx.(dpc) s.(st_nextnode) ->
-  Ple pc' s.(st_nextnode) ->
+  Plt pc' s.(st_nextnode) ->
   pc' <> spc ctx pc ->
   s'.(st_code)!pc' = s.(st_code)!pc'.
 Proof.
@@ -420,7 +469,7 @@ Lemma iter_expand_instr_unchanged:
   forall ctx pc l s x s' i,
   mlist_iter2 (expand_instr fe rec ctx) l s = R x s' i ->
   Ple ctx.(dpc) s.(st_nextnode) ->
-  Ple pc s.(st_nextnode) ->
+  Plt pc s.(st_nextnode) ->
   ~In pc (List.map (spc ctx) (List.map (@fst _ _) l)) ->
   list_norepet (List.map (@fst _ _) l) ->
   s'.(st_code)!pc = s.(st_code)!pc.
@@ -440,7 +489,7 @@ Lemma expand_cfg_rec_unchanged:
   forall ctx f s x s' i pc,
   expand_cfg_rec fe rec ctx f s = R x s' i ->
   Ple ctx.(dpc) s.(st_nextnode) ->
-  Ple pc ctx.(dpc) ->
+  Plt pc ctx.(dpc) ->
   s'.(st_code)!pc = s.(st_code)!pc.
 Proof.
   intros. unfold expand_cfg_rec in H. monadInv H. inversion EQ.
@@ -450,7 +499,7 @@ Proof.
     subst s0; auto. 
     subst s0; simpl. xomega.
     red; intros. exploit list_in_map_inv; eauto. intros [pc1 [A B]]. 
-    subst pc. unfold spc in H1. xomega.
+    subst pc. unfold spc in H1. eapply shiftpos_not_below; eauto. 
     apply PTree.elements_keys_norepet.
   subst s0; auto.
 Qed.
@@ -461,13 +510,13 @@ Hypothesis rec_spec:
   fenv_agree fe' ->
   Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) ->
   ctx.(mreg) = max_def_function f ->
-  Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
+  Ple (Pplus ctx.(dreg) ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 -> 
   ctx.(mstk) = Zmax (fn_stacksize f) 0 ->
   (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
   ctx.(dstk) >= 0 ->
   s'.(st_stksize) <= stacksize ->
-  (forall pc, Plt ctx.(dpc) pc -> Ple pc s'.(st_nextnode) -> c!pc = s'.(st_code)!pc) ->
+  (forall pc, Ple ctx.(dpc) pc -> Plt pc s'.(st_nextnode) -> c!pc = s'.(st_code)!pc) ->
   tr_funbody ctx f c.
 
 Remark min_alignment_pos:
@@ -487,11 +536,11 @@ Lemma expand_instr_spec:
   forall ctx pc instr s x s' i c,
   expand_instr fe rec ctx pc instr s = R x s' i ->
   Ple (max_def_instr instr) ctx.(mreg) ->
-  Ple (spc ctx pc) s.(st_nextnode) ->
+  Plt (spc ctx pc) s.(st_nextnode) ->
   Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 -> ctx.(dstk) >= 0 ->
   s'.(st_stksize) <= stacksize ->
-  (forall pc', Plt s.(st_nextnode) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
+  (forall pc', Ple s.(st_nextnode) pc' -> Plt pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
   c!(spc ctx pc) = s'.(st_code)!(spc ctx pc) ->
   tr_instr ctx pc instr c.
 Proof.
@@ -511,7 +560,8 @@ Proof.
   apply tr_call_inlined with (pc1 := x0) (ctx' := ctx') (f := f); auto.
   eapply BASE; eauto. 
   eapply add_moves_spec; eauto.
-    intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. xomega. xomega.
+    intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega.
+    xomega. xomega.
   eapply rec_spec; eauto.
     red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto.
     simpl. subst s2; simpl in *; xomega.
@@ -523,7 +573,7 @@ Proof.
     intros. simpl in H. rewrite S1.
     transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega.
     eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. 
-  red; simpl. subst s2; simpl in *; xomega.
+  red; simpl. subst s2; simpl in *. xomega. 
   red; simpl. split. auto. apply align_le. apply min_alignment_pos.
 (* tailcall *)
   destruct (can_inline fe s1) as [|id f P Q].
@@ -544,7 +594,7 @@ Proof.
     intros. rewrite S1. eapply set_instr_other; eauto. unfold node; xomega. xomega. xomega.
   eapply rec_spec; eauto.
     red; intros. rewrite PTree.grspec in H. destruct (PTree.elt_eq id0 id); try discriminate. auto.
-    simpl. subst s2; simpl in *; xomega.
+    simpl. subst s3; simpl in *. subst s2; simpl in *. xomega.
     simpl. subst s3; simpl in *; xomega.
     simpl. xomega.
     simpl. apply align_divides. apply min_alignment_pos.
@@ -553,7 +603,8 @@ Proof.
     intros. simpl in H. rewrite S1.
     transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega.
     eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. 
-  red; simpl. subst s2; simpl in *; xomega.
+  red; simpl. 
+subst s2; simpl in *; xomega.
   red; auto.
 (* return *)
   destruct (retinfo ctx) as [[rpc rreg] | ] eqn:?. 
@@ -568,11 +619,11 @@ Lemma iter_expand_instr_spec:
   mlist_iter2 (expand_instr fe rec ctx) l s = R x s' i ->
   list_norepet (List.map (@fst _ _) l) ->
   (forall pc instr, In (pc, instr) l -> Ple (max_def_instr instr) ctx.(mreg)) ->
-  (forall pc instr, In (pc, instr) l -> Ple (spc ctx pc) s.(st_nextnode)) ->
+  (forall pc instr, In (pc, instr) l -> Plt (spc ctx pc) s.(st_nextnode)) ->
   Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 -> ctx.(dstk) >= 0 ->
   s'.(st_stksize) <= stacksize ->
-  (forall pc', Plt s.(st_nextnode) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
+  (forall pc', Ple s.(st_nextnode) pc' -> Plt pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
   (forall pc instr, In (pc, instr) l -> c!(spc ctx pc) = s'.(st_code)!(spc ctx pc)) ->
   forall pc instr, In (pc, instr) l -> tr_instr ctx pc instr c.
 Proof.
@@ -582,7 +633,8 @@ Proof.
   (* inductive case *)
   destruct a as [pc1 instr1]; simpl in *. inv H0. monadInv H. inv_incr.
   assert (A: Ple ctx.(dpc) s0.(st_nextnode)).
-    assert (B: Ple (spc ctx pc) (st_nextnode s)) by eauto. unfold spc in B; xomega.
+    assert (B: Plt (spc ctx pc) (st_nextnode s)) by eauto. 
+    unfold spc in B. generalize (shiftpos_above pc (dpc ctx)). xomega.
   destruct H9. inv H.
   (* same pc *)
   eapply expand_instr_spec; eauto.
@@ -593,18 +645,18 @@ Proof.
     eapply iter_expand_instr_unchanged; eauto. 
     red; intros. rewrite list_map_compose in H9. exploit list_in_map_inv; eauto. 
     intros [[pc0 instr0] [P Q]]. simpl in P. 
-    assert (Ple (spc ctx pc0) (st_nextnode s)) by eauto. xomega.
+    assert (Plt (spc ctx pc0) (st_nextnode s)) by eauto. xomega.
   transitivity ((st_code s')!(spc ctx pc)). 
     eapply H8; eauto. 
     eapply iter_expand_instr_unchanged; eauto. 
-    assert (Ple (spc ctx pc) (st_nextnode s)) by eauto. xomega.
+    assert (Plt (spc ctx pc) (st_nextnode s)) by eauto. xomega.
     red; intros. rewrite list_map_compose in H. exploit list_in_map_inv; eauto. 
-    intros [[pc0 instr0] [P Q]]. simpl in P. unfold spc in P. 
-    assert (pc = pc0) by (unfold node; xomega). subst pc0.
+    intros [[pc0 instr0] [P Q]]. simpl in P.
+    assert (pc = pc0) by (eapply shiftpos_inj; eauto). subst pc0.
     elim H12. change pc with (fst (pc, instr0)). apply List.in_map; auto.
   (* older pc *)
   inv_incr. eapply IHl; eauto. 
-  intros. eapply Ple_trans; eauto. 
+  intros. eapply Plt_le_trans. eapply H2. right; eauto. xomega.
   intros; eapply Ple_trans; eauto.
   intros. apply H7; auto. xomega.
 Qed.
@@ -620,7 +672,7 @@ Lemma expand_cfg_rec_spec:
   (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
   ctx.(dstk) >= 0 ->
   s'.(st_stksize) <= stacksize ->
-  (forall pc', Plt ctx.(dpc) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
+  (forall pc', Ple ctx.(dpc) pc' -> Plt pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
   tr_funbody ctx f c.
 Proof.
   intros. unfold expand_cfg_rec in H. monadInv H. inversion EQ. 
@@ -633,14 +685,14 @@ Proof.
     eapply PTree.elements_complete; eauto.
   intros.
     assert (Ple pc0 (max_pc_function f)).
-      eapply max_pc_function_sound. eapply PTree.elements_complete; eauto.  
-    unfold spc. subst s0; simpl; xomega.
+      eapply max_pc_function_sound. eapply PTree.elements_complete; eauto.
+      eapply Plt_le_trans. apply shiftpos_below. subst s0; simpl; xomega.
   subst s0; simpl; auto.
   intros. apply H8; auto. subst s0; simpl in H11; xomega.
-  intros. apply H8. unfold spc; xomega. 
-    assert (Ple pc0 (max_pc_function f)).
-      eapply max_pc_function_sound. eapply PTree.elements_complete; eauto.  
-    unfold spc. inversion i; xomega.
+  intros. apply H8. apply shiftpos_above. 
+  assert (Ple pc0 (max_pc_function f)).
+    eapply max_pc_function_sound. eapply PTree.elements_complete; eauto.  
+  eapply Plt_le_trans. apply shiftpos_below. inversion i; xomega. 
   apply PTree.elements_correct; auto.
   auto. auto. auto.
   inversion INCR0. subst s0; simpl in STKSIZE; xomega.
@@ -652,7 +704,7 @@ Lemma expand_cfg_unchanged:
   forall fe ctx f s x s' i pc,
   expand_cfg fe ctx f s = R x s' i ->
   Ple ctx.(dpc) s.(st_nextnode) ->
-  Ple pc ctx.(dpc) ->
+  Plt pc ctx.(dpc) ->
   s'.(st_code)!pc = s.(st_code)!pc.
 Proof.
   intros fe0; pattern fe0. apply well_founded_ind with (R := ltof _ size_fenv).
@@ -673,7 +725,7 @@ Lemma expand_cfg_spec:
   (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
   ctx.(dstk) >= 0 ->
   s'.(st_stksize) <= stacksize ->
-  (forall pc', Plt ctx.(dpc) pc' -> Ple pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
+  (forall pc', Ple ctx.(dpc) pc' -> Plt pc' s'.(st_nextnode) -> c!pc' = s'.(st_code)!pc') ->
   tr_funbody ctx f c.
 Proof.
   intros fe0; pattern fe0. apply well_founded_ind with (R := ltof _ size_fenv).