Messy progress on builtin-case of exec_exit_simulation_plus

1 files changed, 25 insertions, 10 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index b4dc08f6..0288f11c 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -775,20 +775,19 @@ Proof.
     replace (list_length_z (header bb) + list_length_z (body bb) + 1 - 1 -
        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.
+  + 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. }
+    destruct cfi.
     * (* 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.
+      destruct H3. destruct H3. destruct H3. rewrite H5.
       inversion MATCHI.
       apply plus_one.
       eapply Asm.exec_step_internal; eauto.
@@ -800,10 +799,26 @@ Proof.
         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.
+      rewrite H in EXIT.
+      rewrite H in MATCHI. simpl in MATCHI.
+      simpl in FIND_INSTR.
+      inversion EXIT.
+      apply plus_one.
+      eapply external_call_symbols_preserved in H10; try (apply senv_preserved).
+      eapply eval_builtin_args_preserved in H6; try (apply symbols_preserved).
+      eapply Asm.exec_step_builtin; eauto.
+      - inv MATCHI. rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. eauto.
+      - (* XXX copy-paste from case above *)
+        simpl. replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))))
+                  with (Ptrofs.unsigned ofs + (size bb - 1)); eauto.
+        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.
+      - simpl. (* TODO something like eval_builtin_args_match *) admit.
+      - inv MATCHI; eauto.
+      - rewrite H11. (* TODO lemmas for set_res, undef_regs ... *) admit.
 Admitted.
 
 Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall