proof of exec_header_simulation

1 files changed, 91 insertions, 10 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 2f05355f..4a1f4de4 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -89,6 +89,26 @@ Proof.
   eauto.
 Qed.
 
+Lemma internal_functions_unfold:
+  forall b f,
+  Genv.find_funct_ptr ge b = Some (Internal f) ->
+  exists tc,
+  Genv.find_funct_ptr tge b = Some (Internal (Asm.mkfunction (fn_sig f) tc))
+  /\ unfold (fn_blocks f) = OK tc
+  /\ list_length_z tc <= Ptrofs.max_unsigned.
+Proof.
+  intros.
+  exploit internal_functions_translated; eauto.
+  intros (tf & FINDtf & TRANStf).
+  unfold transf_function in TRANStf.
+  monadInv TRANStf.
+  destruct (zlt _ _); try congruence.
+  inv EQ. inv EQ0.
+  eexists; intuition eauto.
+  omega.
+Qed.
+
+
 Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop :=
   | is_nth_label l:
      list_nth_z (header bb) n = Some l ->
@@ -104,7 +124,7 @@ Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop :=
      i = control_to_instruction cfi ->
      is_nth_inst bb n i.
 
-Lemma find_instr_bblock pos n lb tlb bb:
+Lemma find_instr_bblock n pos lb tlb bb:
   find_bblock pos lb = Some bb ->
   unfold lb = OK tlb ->
   0 <= n < size bb ->
@@ -233,6 +253,7 @@ Proof.
   unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; omega.
 Qed.
 
+(* NB: does not seem useful anymore, with the [exec_header_simulation] proof below 
 Lemma match_internal_exec_label:
   forall n rs1 m1 rs2 m2 l fb f tf,
   Genv.find_funct_ptr ge fb = Some (Internal f) ->
@@ -260,6 +281,7 @@ Proof.
       * apply Z.ge_le; assumption.
       * rewrite <- functions_bound_max_pos; eauto; omega.
 Qed.
+*)
 
 Lemma incrPC_agree_but_pc:
   forall rs r ofs,
@@ -463,16 +485,82 @@ Proof.
   - left. discriminate.
 Qed.
 
+Lemma list_length_z_aux_increase A (l: list A): forall acc, 
+  list_length_z_aux l acc >= acc.
+Proof.
+  induction l; simpl; intros.
+  - omega.
+  - generalize (IHl (Z.succ acc)). omega.
+Qed.
+
+Lemma bblock_size_aux_pos bb: list_length_z (body bb) + Z.of_nat (length_opt (exit bb)) >= 1.
+Admitted. (* NB: from bblock_non_empty *)
+
 Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)).
 Admitted.
 
+Lemma bblock_size_pos bb: size bb >= 1.
+Proof.
+  rewrite (bblock_size_aux bb).
+  generalize (bblock_size_aux_pos bb).
+  generalize (list_length_z_pos (header bb)).
+  omega.
+Qed.
+
+Lemma size_header b pos f bb: forall
+  (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
+  (FINDBB: find_bblock pos (fn_blocks f) = Some bb),
+  list_length_z (header bb) <= 1.
+Admitted.
+
+Lemma list_nth_z_neg A (l: list A): forall n,
+  n < 0 -> list_nth_z l n = None.
+Proof.
+  induction l; simpl; auto.
+  intros n H; destruct (zeq _ _); (try eapply IHl); omega.
+Qed.
+
+
 Lemma exec_header_simulation b ofs f bb rs m: forall
   (ATPC: rs PC = Vptr b ofs)
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
   (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb),
   exists s', star Asm.step tge (State rs m) E0 s'
              /\ match_internal (list_length_z (header bb)) (State rs m) s'.
-Admitted.
+Proof.
+  intros.
+  exploit internal_functions_unfold; eauto.
+  intros (tc & FINDtf & TRANStf & _).
+  assert (BNDhead: list_length_z (header bb) <= 1). { eapply size_header; eauto. }
+  destruct (header bb) as [|l[|]] eqn: EQhead.
+  + (* header nil *)
+    eexists; split.
+    - eapply star_refl.
+    - split; eauto.
+      unfold list_length_z; rewrite !ATPC; simpl.
+      rewrite Ptrofs.add_zero; auto.
+  + (* header one *)
+    assert (Lhead: list_length_z (header bb) = 1). { rewrite EQhead; unfold list_length_z; simpl. auto. }
+    exploit (find_instr_bblock 0); eauto. 
+    { generalize (bblock_size_pos bb). omega. }
+    intros (i & NTH & FIND_INSTR).
+    inv NTH.
+    * rewrite EQhead in H; simpl in H. inv H.
+      cutrewrite (Ptrofs.unsigned ofs + 0 = Ptrofs.unsigned ofs) in FIND_INSTR; try omega.
+      eexists. split.
+      - eapply star_one. 
+        eapply Asm.exec_step_internal; eauto.
+        simpl; eauto.
+      - unfold list_length_z; simpl. split; eauto.
+        intros r; destruct r; simpl; congruence || auto.
+    * (* absurd case *)
+      erewrite list_nth_z_neg in * |-; [ congruence | rewrite Lhead; omega].
+    * (* absurd case *)
+      rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). omega.
+  + (* absurd case *)
+    unfold list_length_z in BNDhead. simpl in *.
+    generalize (list_length_z_aux_increase _ l1 2); omega.
+Qed.
 
 Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall
   (ATPC: rs PC = Vptr b ofs)
@@ -550,21 +638,14 @@ Proof.
     subst; eapply star_refl; eauto.
 Qed.
 
-Lemma exec_bblock_simulation b ofs f tf bb t rs m rs' m': forall
+Lemma exec_bblock_simulation b ofs f bb t rs m rs' m': forall
   (ATPC: rs PC = Vptr b ofs)
   (FINDF: Genv.find_funct_ptr ge b = Some (Internal f))
   (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb)
-  (FINDtf : Genv.find_funct_ptr tge b = Some (Internal tf))
-  (TRANSf : transf_function f = OK tf)
   (EXECBB: exec_bblock lk ge f bb rs m t rs' m'),
   plus Asm.step tge (State rs m) t (State rs' m').
 Proof.
   intros; destruct EXECBB as (rs1 & m1 & BODY & CTL).
-  generalize TRANSf.
-  intros TRANS.
-  monadInv TRANS.
-  destruct (zlt _ _); try congruence.
-  inv EQ. inv EQ0.
   exploit exec_header_simulation; eauto.
   intros (s0 & STAR & MATCH0).
   eapply star_plus_trans; traceEq || eauto.