Tunnelingproof: Remove assumption destroyed_by_cond c = nil.

Since commit e5b37a6 (useless conditional branch elimination), the proof of the Tunneling pass was assuming forall c, destroyed_by_cond c = nil.  This is not true for architecture variants that we will support soon.  This commit rewrites the proof so as to remove this assumption.  The old proof was by memory and value equalities, the new one is by memory extensions and "lessdef" values.

1 files changed, 210 insertions, 66 deletions

diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 602c018c..6acf2bbd 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -171,18 +171,6 @@ Proof.
   destruct f; reflexivity.
 Qed.
 
-Lemma find_function_translated:
-  forall ros ls f,
-  find_function ge ros ls = Some f ->
-  find_function tge ros ls = Some (tunnel_fundef f).
-Proof.
-  intros until f. destruct ros; simpl.
-  intro. apply functions_translated; auto.
-  rewrite symbols_preserved. destruct (Genv.find_symbol ge i).
-  apply function_ptr_translated; auto.
-  congruence.
-Qed.
-
 (** The proof of semantic preservation is a simulation argument
   based on diagrams of the following form:
 <<
@@ -200,10 +188,11 @@ Qed.
   "zero transition" case occurs when executing a [Lgoto] instruction
   in the source code that has been removed by tunneling.
 
-  In the definition of [match_states], note that only the control-flow
-  (in particular, the current program point [pc]) is changed:
-  the values of locations and the memory states are identical in the
-  original and transformed codes. *)
+  In the definition of [match_states], what changes between the original and
+  transformed codes is mainly the control-flow
+  (in particular, the current program point [pc]), but also some values
+  and memory states, since some [Vundef] values can become more defined
+  as a consequence of eliminating useless [Lcond] instructions. *)
 
 Definition tunneled_block (f: function) (b: bblock) :=
   tunnel_block (record_gotos f) b.
@@ -211,39 +200,171 @@ Definition tunneled_block (f: function) (b: bblock) :=
 Definition tunneled_code (f: function) :=
   PTree.map1 (tunneled_block f) (fn_code f).
 
+Definition locmap_lessdef (ls1 ls2: locset) : Prop :=
+  forall l, Val.lessdef (ls1 l) (ls2 l).
+
 Inductive match_stackframes: stackframe -> stackframe -> Prop :=
   | match_stackframes_intro:
-      forall f sp ls0 bb,
+      forall f sp ls0 bb tls0,
+      locmap_lessdef ls0 tls0 ->
       match_stackframes
          (Stackframe f sp ls0 bb)
-         (Stackframe (tunnel_function f) sp ls0 (tunneled_block f bb)).
+         (Stackframe (tunnel_function f) sp tls0 (tunneled_block f bb)).
 
 Inductive match_states: state -> state -> Prop :=
   | match_states_intro:
-      forall s f sp pc ls m ts,
-      list_forall2 match_stackframes s ts ->
+      forall s f sp pc ls m ts tls tm
+        (STK: list_forall2 match_stackframes s ts)
+        (LS: locmap_lessdef ls tls)
+        (MEM: Mem.extends m tm),
       match_states (State s f sp pc ls m)
-                   (State ts (tunnel_function f) sp (branch_target f pc) ls m)
+                   (State ts (tunnel_function f) sp (branch_target f pc) tls tm)
   | match_states_block:
-      forall s f sp bb ls m ts,
-      list_forall2 match_stackframes s ts ->
+      forall s f sp bb ls m ts tls tm
+        (STK: list_forall2 match_stackframes s ts)
+        (LS: locmap_lessdef ls tls)
+        (MEM: Mem.extends m tm),
       match_states (Block s f sp bb ls m)
-                   (Block ts (tunnel_function f) sp (tunneled_block f bb) ls m)
+                   (Block ts (tunnel_function f) sp (tunneled_block f bb) tls tm)
   | match_states_interm:
-      forall s f sp pc bb ls m ts,
-      list_forall2 match_stackframes s ts ->
+      forall s f sp pc bb ls m ts tls tm
+        (STK: list_forall2 match_stackframes s ts)
+        (LS: locmap_lessdef ls tls)
+        (MEM: Mem.extends m tm),
       match_states (Block s f sp (Lbranch pc :: bb) ls m)
-                   (State ts (tunnel_function f) sp (branch_target f pc) ls m)
+                   (State ts (tunnel_function f) sp (branch_target f pc) tls tm)
   | match_states_call:
-      forall s f ls m ts,
-      list_forall2 match_stackframes s ts ->
+      forall s f ls m ts tls tm
+        (STK: list_forall2 match_stackframes s ts)
+        (LS: locmap_lessdef ls tls)
+        (MEM: Mem.extends m tm),
       match_states (Callstate s f ls m)
-                   (Callstate ts (tunnel_fundef f) ls m)
+                   (Callstate ts (tunnel_fundef f) tls tm)
   | match_states_return:
-      forall s ls m ts,
-      list_forall2 match_stackframes s ts ->
+      forall s ls m ts tls tm
+        (STK: list_forall2 match_stackframes s ts)
+        (LS: locmap_lessdef ls tls)
+        (MEM: Mem.extends m tm),
       match_states (Returnstate s ls m)
-                   (Returnstate ts ls m).
+                   (Returnstate ts tls tm).
+
+(** Properties of [locmap_lessdef] *)
+
+Lemma reglist_lessdef:
+  forall rl ls1 ls2,
+  locmap_lessdef ls1 ls2 -> Val.lessdef_list (reglist ls1 rl) (reglist ls2 rl).
+Proof.
+  induction rl; simpl; intros; auto.
+Qed.
+
+Lemma locmap_set_lessdef:
+  forall ls1 ls2 v1 v2 l,
+  locmap_lessdef ls1 ls2 -> Val.lessdef v1 v2 -> locmap_lessdef (Locmap.set l v1 ls1) (Locmap.set l v2 ls2).
+Proof.
+  intros; red; intros l'. unfold Locmap.set. destruct (Loc.eq l l').
+- destruct l; auto using Val.load_result_lessdef.
+- destruct (Loc.diff_dec l l'); auto.
+Qed.
+
+Lemma locmap_set_undef_lessdef:
+  forall ls1 ls2 l,
+  locmap_lessdef ls1 ls2 -> locmap_lessdef (Locmap.set l Vundef ls1) ls2.
+Proof.
+  intros; red; intros l'. unfold Locmap.set. destruct (Loc.eq l l').
+- destruct l; auto. destruct ty; auto. 
+- destruct (Loc.diff_dec l l'); auto.
+Qed.
+
+Lemma locmap_undef_regs_lessdef:
+  forall rl ls1 ls2,
+  locmap_lessdef ls1 ls2 -> locmap_lessdef (undef_regs rl ls1) (undef_regs rl ls2).
+Proof.
+  induction rl as [ | r rl]; intros; simpl. auto. apply locmap_set_lessdef; auto. 
+Qed.
+
+Lemma locmap_undef_regs_lessdef_1:
+  forall rl ls1 ls2,
+  locmap_lessdef ls1 ls2 -> locmap_lessdef (undef_regs rl ls1) ls2.
+Proof.
+  induction rl as [ | r rl]; intros; simpl. auto. apply locmap_set_undef_lessdef; auto. 
+Qed.
+
+(*
+Lemma locmap_undef_lessdef:
+  forall ll ls1 ls2,
+  locmap_lessdef ls1 ls2 -> locmap_lessdef (Locmap.undef ll ls1) (Locmap.undef ll ls2).
+Proof.
+  induction ll as [ | l ll]; intros; simpl. auto. apply IHll. apply locmap_set_lessdef; auto. 
+Qed.
+
+Lemma locmap_undef_lessdef_1:
+  forall ll ls1 ls2,
+  locmap_lessdef ls1 ls2 -> locmap_lessdef (Locmap.undef ll ls1) ls2.
+Proof.
+  induction ll as [ | l ll]; intros; simpl. auto. apply IHll. apply locmap_set_undef_lessdef; auto. 
+Qed.
+*)
+
+Lemma locmap_getpair_lessdef:
+  forall p ls1 ls2,
+  locmap_lessdef ls1 ls2 -> Val.lessdef (Locmap.getpair p ls1) (Locmap.getpair p ls2).
+Proof.
+  intros; destruct p; simpl; auto using Val.longofwords_lessdef.
+Qed.
+
+Lemma locmap_getpairs_lessdef:
+  forall pl ls1 ls2,
+  locmap_lessdef ls1 ls2 ->
+  Val.lessdef_list (map (fun p => Locmap.getpair p ls1) pl) (map (fun p => Locmap.getpair p ls2) pl).
+Proof.
+  intros. induction pl; simpl; auto using locmap_getpair_lessdef.
+Qed.
+
+Lemma locmap_setpair_lessdef:
+  forall p ls1 ls2 v1 v2,
+  locmap_lessdef ls1 ls2 -> Val.lessdef v1 v2 -> locmap_lessdef (Locmap.setpair p v1 ls1) (Locmap.setpair p v2 ls2).
+Proof.
+  intros; destruct p; simpl; auto using locmap_set_lessdef, Val.loword_lessdef, Val.hiword_lessdef.
+Qed.
+
+Lemma locmap_setres_lessdef:
+  forall res ls1 ls2 v1 v2,
+  locmap_lessdef ls1 ls2 -> Val.lessdef v1 v2 -> locmap_lessdef (Locmap.setres res v1 ls1) (Locmap.setres res v2 ls2).
+Proof.
+  induction res; intros; simpl; auto using locmap_set_lessdef, Val.loword_lessdef, Val.hiword_lessdef.
+Qed.
+
+Lemma find_function_translated:
+  forall ros ls tls fd,
+  locmap_lessdef ls tls ->
+  find_function ge ros ls = Some fd ->
+  find_function tge ros tls = Some (tunnel_fundef fd).
+Proof.
+  intros. destruct ros; simpl in *.
+- assert (E: tls (R m) = ls (R m)).
+  { exploit Genv.find_funct_inv; eauto. intros (b & EQ). 
+    generalize (H (R m)). rewrite EQ. intros LD; inv LD. auto. }
+  rewrite E. apply functions_translated; auto.
+- rewrite symbols_preserved. destruct (Genv.find_symbol ge i); inv H0. 
+  apply function_ptr_translated; auto.
+Qed.
+
+Lemma call_regs_lessdef:
+  forall ls1 ls2, locmap_lessdef ls1 ls2 -> locmap_lessdef (call_regs ls1) (call_regs ls2).
+Proof.
+  intros; red; intros. destruct l as [r | [] ofs ty]; simpl; auto.
+Qed.
+
+Lemma return_regs_lessdef:
+  forall caller1 callee1 caller2 callee2,
+  locmap_lessdef caller1 caller2 ->
+  locmap_lessdef callee1 callee2 ->
+  locmap_lessdef (return_regs caller1 callee1) (return_regs caller2 callee2).
+Proof.
+  intros; red; intros. destruct l; simpl.
+- destruct (Conventions1.is_callee_save r); auto.
+- auto.
+Qed. 
 
 (** To preserve non-terminating behaviours, we show that the transformed
   code cannot take an infinity of "zero transition" cases.
@@ -262,9 +383,11 @@ Definition measure (st: state) : nat :=
 Lemma match_parent_locset:
   forall s ts,
   list_forall2 match_stackframes s ts ->
-  parent_locset ts = parent_locset s.
+  locmap_lessdef (parent_locset s) (parent_locset ts).
 Proof.
-  induction 1; simpl. auto. inv H; auto.
+  induction 1; simpl.
+- red; auto.
+- inv H; auto.
 Qed.
 
 Lemma tunnel_step_correct:
@@ -278,7 +401,7 @@ Proof.
 - (* entering a block *)
   assert (DEFAULT: branch_target f pc = pc ->
     (exists st2' : state,
-     step tge (State ts (tunnel_function f) sp (branch_target f pc) rs m) E0 st2'
+     step tge (State ts (tunnel_function f) sp (branch_target f pc) tls tm) E0 st2'
      /\ match_states (Block s f sp bb rs m) st2')).
   { intros. rewrite H0. econstructor; split.
     econstructor. simpl. rewrite PTree.gmap1. rewrite H. simpl. eauto.
@@ -292,53 +415,63 @@ Proof.
   rewrite B. econstructor; eauto.
 
 - (* Lop *)
+  exploit eval_operation_lessdef. apply reglist_lessdef; eauto. eauto. eauto. 
+  intros (tv & EV & LD).
   left; simpl; econstructor; split.
-  eapply exec_Lop with (v := v); eauto.
-  rewrite <- H. apply eval_operation_preserved. exact symbols_preserved.
-  econstructor; eauto.
+  eapply exec_Lop with (v := tv); eauto.
+  rewrite <- EV. apply eval_operation_preserved. exact symbols_preserved.
+  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
 - (* Lload *)
+  exploit eval_addressing_lessdef. apply reglist_lessdef; eauto. eauto. 
+  intros (ta & EV & LD).
+  exploit Mem.loadv_extends. eauto. eauto. eexact LD. 
+  intros (tv & LOAD & LD').
   left; simpl; econstructor; split.
-  eapply exec_Lload with (a := a).
-  rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Lload with (a := ta).
+  rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved.
   eauto. eauto.
-  econstructor; eauto.
+  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
 - (* Lgetstack *)
   left; simpl; econstructor; split.
   econstructor; eauto.
-  econstructor; eauto.
+  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
 - (* Lsetstack *)
   left; simpl; econstructor; split.
   econstructor; eauto.
-  econstructor; eauto.
+  econstructor; eauto using locmap_set_lessdef, locmap_undef_regs_lessdef.
 - (* Lstore *)
+  exploit eval_addressing_lessdef. apply reglist_lessdef; eauto. eauto. 
+  intros (ta & EV & LD).
+  exploit Mem.storev_extends. eauto. eauto. eexact LD. apply LS.  
+  intros (tm' & STORE & MEM').
   left; simpl; econstructor; split.
-  eapply exec_Lstore with (a := a).
-  rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
+  eapply exec_Lstore with (a := ta).
+  rewrite <- EV. apply eval_addressing_preserved. exact symbols_preserved.
   eauto. eauto.
-  econstructor; eauto.
+  econstructor; eauto using locmap_undef_regs_lessdef.
 - (* Lcall *)
   left; simpl; econstructor; split.
   eapply exec_Lcall with (fd := tunnel_fundef fd); eauto.
-  apply find_function_translated; auto.
+  eapply find_function_translated; eauto.
   rewrite sig_preserved. auto.
   econstructor; eauto.
   constructor; auto.
   constructor; auto.
 - (* Ltailcall *)
+  exploit Mem.free_parallel_extends. eauto. eauto. intros (tm' & FREE & MEM'). 
   left; simpl; econstructor; split.
   eapply exec_Ltailcall with (fd := tunnel_fundef fd); eauto.
-  erewrite match_parent_locset; eauto.
-  apply find_function_translated; auto.
+  eapply find_function_translated; eauto using return_regs_lessdef, match_parent_locset.
   apply sig_preserved.
-  erewrite <- match_parent_locset; eauto.
-  econstructor; eauto.
+  econstructor; eauto using return_regs_lessdef, match_parent_locset.
 - (* Lbuiltin *)
+  exploit eval_builtin_args_lessdef. eexact LS. eauto. eauto. intros (tvargs & EVA & LDA).
+  exploit external_call_mem_extends; eauto. intros (tvres & tm' & A & B & C & D).
   left; simpl; econstructor; split.
   eapply exec_Lbuiltin; eauto.
-  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. 
   eapply external_call_symbols_preserved. apply senv_preserved. eauto.
-  econstructor; eauto.
-
+  econstructor; eauto using locmap_setres_lessdef, locmap_undef_regs_lessdef.
 - (* Lbranch (preserved) *)
   left; simpl; econstructor; split.
   eapply exec_Lbranch; eauto.
@@ -352,32 +485,40 @@ Proof.
   destruct (peq s1 s2).
 + left; econstructor; split.
   eapply exec_Lbranch. 
-  destruct b. constructor; auto. rewrite e. constructor; auto.
+  destruct b.
+* constructor; eauto using locmap_undef_regs_lessdef_1.
+* rewrite e. constructor; eauto using locmap_undef_regs_lessdef_1.
 + left; econstructor; split.
-  eapply exec_Lcond; eauto.
-  destruct b; econstructor; eauto.
+  eapply exec_Lcond; eauto. eapply eval_condition_lessdef; eauto using reglist_lessdef.
+  destruct b; econstructor; eauto using locmap_undef_regs_lessdef.
 
 - (* Ljumptable *)
+  assert (tls (R arg) = Vint n).
+  { generalize (LS (R arg)); rewrite H; intros LD; inv LD; auto. }
   left; simpl; econstructor; split.
   eapply exec_Ljumptable.
   eauto. rewrite list_nth_z_map. change U.elt with node. rewrite H0. reflexivity. eauto.
-  econstructor; eauto.
+  econstructor; eauto using locmap_undef_regs_lessdef.
 - (* Lreturn *)
+  exploit Mem.free_parallel_extends. eauto. eauto. intros (tm' & FREE & MEM'). 
   left; simpl; econstructor; split.
   eapply exec_Lreturn; eauto.
-  erewrite <- match_parent_locset; eauto.
-  constructor; auto.
+  constructor; eauto using return_regs_lessdef, match_parent_locset.
 - (* internal function *)
+  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. 
+  intros (tm' & ALLOC & MEM'). 
   left; simpl; econstructor; split.
   eapply exec_function_internal; eauto.
-  simpl. econstructor; eauto.
+  simpl. econstructor; eauto using locmap_undef_regs_lessdef, call_regs_lessdef.
 - (* external function *)
+  exploit external_call_mem_extends; eauto using locmap_getpairs_lessdef.
+  intros (tvres & tm' & A & B & C & D).
   left; simpl; econstructor; split.
   eapply exec_function_external; eauto.
   eapply external_call_symbols_preserved; eauto. apply senv_preserved.
-  simpl. econstructor; eauto.
+  simpl. econstructor; eauto using locmap_setpair_lessdef.
 - (* return *)
-  inv H3. inv H1.
+  inv STK. inv H1.
   left; econstructor; split.
   eapply exec_return; eauto.
   constructor; auto.
@@ -395,14 +536,17 @@ Proof.
   rewrite symbols_preserved. eauto.
   apply function_ptr_translated; auto.
   rewrite <- H3. apply sig_preserved.
-  constructor. constructor.
+  constructor. constructor. red; simpl; auto. apply Mem.extends_refl.
 Qed.
 
 Lemma transf_final_states:
   forall st1 st2 r,
   match_states st1 st2 -> final_state st1 r -> final_state st2 r.
 Proof.
-  intros. inv H0. inv H. inv H5. econstructor; eauto.
+  intros. inv H0. inv H. inv STK.
+  set (p := map_rpair R (Conventions1.loc_result signature_main)) in *.
+  generalize (locmap_getpair_lessdef p _ _ LS). rewrite H1; intros LD; inv LD.
+  econstructor; eauto.
 Qed.
 
 Theorem transf_program_correct: