Messy progress on exec_exit_simulation_plus

Proves exec_exit_simulation_plus for cf_instruction (as opposed to
builtins)

1 files changed, 27 insertions, 3 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 1412a3a4..b4dc08f6 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -759,13 +759,14 @@ Lemma exec_exit_simulation_plus b ofs f bb s2 t rs m rs' m': forall
   (ATPC: rs PC = Vptr b ofs),
   plus Asm.step tge s2 t (State rs' m').
 Proof.
-  intros. apply plus_one.
+  intros.
   exploit internal_functions_unfold; eauto.
   intros (tc & FINDtf & TRANStf & _).
 
   exploit (find_instr_bblock (size bb - 1)); eauto.
   { generalize (bblock_size_pos bb). omega. }
   intros (i' & NTH & FIND_INSTR).
+
   inv NTH.
   + rewrite last_instruction_cannot_be_label in *. discriminate.
   + destruct (exit bb) as [ctrl |] eqn:NEMPTY_EXIT'. 2: { contradiction. }
@@ -775,11 +776,34 @@ Proof.
        list_length_z (header bb)) with (list_length_z (body bb)) in H by omega.
     rewrite list_nth_z_range_exceeded in H; try omega. discriminate.
   + destruct cfi.
-    * (* controlf low instruction *)
+    * (* control flow instruction *)
+      destruct s2.
+      rewrite H in EXIT. (* exit bb is a cfi *)
+      inv EXIT.
+      (* setup for exec_cfi_simulation *)
+      assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned). {
+        eapply size_of_blocks_bounds; eauto.
+      }
+      assert (size bb <= Ptrofs.max_unsigned). { generalize (Ptrofs.unsigned_range_2 ofs); omega. }
+      rewrite H in MATCHI. simpl in MATCHI.
+      exploit exec_cfi_simulation; eauto; intros.
+      (* extract exec_cfi_simulation's conclusion as separate hypotheses *)
+      destruct H4. destruct H4. destruct H4. rewrite H5.
+      inversion MATCHI.
+      apply plus_one.
+      eapply Asm.exec_step_internal; eauto.
+      - rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. eauto.
+      - simpl. replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))))
+                  with (Ptrofs.unsigned ofs + (size bb - 1)); try assumption.
+        generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros.
+        unfold Ptrofs.add.
+        rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega.
+        rewrite Ptrofs.unsigned_repr; omega.
+    * (* builtin *)
       rewrite H in EXIT.
       inv EXIT.
+      destruct s2.
       admit.
-    * (* builtin *) admit.
 Admitted.
 
 Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall