intermediatet commit before builtins

1 files changed, 52 insertions, 52 deletions

diff --git a/aarch64/Asmblockprops.v b/aarch64/Asmblockprops.v
index d1015ea9..cef95aad 100644
--- a/aarch64/Asmblockprops.v
+++ b/aarch64/Asmblockprops.v
@@ -39,7 +39,13 @@ Lemma preg_of_data:
 Proof.
   intros. destruct r; reflexivity.
 Qed.
-Hint Resolve preg_of_data: asmgen.
+
+Lemma dreg_of_data:
+  forall r, data_preg (dreg_of r) = true.
+Proof.
+  intros. destruct r; reflexivity.
+Qed.
+Hint Resolve preg_of_data dreg_of_data: asmgen.
 
 Lemma data_diff:
   forall r r',
@@ -55,6 +61,12 @@ Proof.
   intros. apply data_diff; auto with asmgen.
 Qed.
 
+Lemma preg_of_not_SP:
+  forall r, preg_of r <> SP.
+Proof.
+  intros. unfold preg_of; destruct r; simpl; try discriminate.
+Qed.
+
 (*
 Lemma preg_of_not_SP:
   forall r, preg_of r <> SP.
@@ -81,73 +93,61 @@ Lemma nextblock_inv1:
   forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r.
 Proof.
   intros. apply nextblock_inv. red; intro; subst; discriminate.
-Qed.
+Qed.*)
+
+Ltac desif :=
+  repeat match goal with
+  | [ |- context[ if ?f then _ else _ ] ] => destruct f
+  end.
+  
+Ltac decomp :=
+  repeat match goal with
+  | [ |- context[ match (?rs ?r) with | _ => _ end ] ] => destruct (rs r)
+  end.
 
 Ltac Simplif :=
-  ((rewrite nextblock_inv by eauto with asmgen)
-  || (rewrite nextblock_inv1 by eauto with asmgen)
+  ((desif)
+  || (try unfold compare_long)
+  || (try unfold compare_int)
+  || (try unfold compare_float)
+  || (try unfold compare_single)
+  || decomp
   || (rewrite Pregmap.gss)
-  || (rewrite nextblock_pc)
   || (rewrite Pregmap.gso by eauto with asmgen)
   ); auto with asmgen.
 
 Ltac Simpl := repeat Simplif.
 
+Section EPC.
+
+Variable lk: aarch64_linker.
+
 (* For Asmblockgenproof0 *)
 
 Theorem exec_basic_instr_pc:
   forall ge b rs1 m1 rs2 m2,
-  exec_basic_instr ge b rs1 m1 = Next rs2 m2 ->
+  exec_basic lk ge b rs1 m1 = Next rs2 m2 ->
   rs2 PC = rs1 PC.
 Proof.
-  intros. destruct b; try destruct i; try destruct i.
-  all: try (inv H; Simpl).
-  1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
-
-  1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail.
-
-  { (* PLoadQRRO *)
-    unfold  parexec_load_q_offset in H1.
-    destruct (gpreg_q_expand _) as [r0 r1] in H1.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    inv H1. Simpl. }
-  { (* PLoadORRO *)
-    unfold  parexec_load_o_offset in H1.
-    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    destruct (Mem.loadv _ _ _) in H1; try discriminate.
-    inv H1. Simpl. }
-  1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail.
-  1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
-  1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail.
-  
-  { (* PStoreQRRO *)
-    unfold  parexec_store_q_offset in H1.
-    destruct (gpreg_q_expand _) as [r0 r1] in H1.
-    unfold eval_offset in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    inv H1. Simpl. reflexivity. }
-  { (* PStoreORRO *)
-    unfold  parexec_store_o_offset in H1.
-    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
-    unfold eval_offset in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    destruct (Mem.storev _ _ _) in H1; try discriminate.
-    inv H1. Simpl. reflexivity. }
-  - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
-  - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
-    destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.
-  - destruct rs; try discriminate. inv H1. Simpl.
-  - destruct rd; try discriminate. inv H1; Simpl.
-  - reflexivity.
+  intros. destruct b; try destruct i; try destruct i; try destruct ld; try destruct ld;
+  try destruct st; try destruct st; try destruct a.
+  all: try (inv H; simpl in *; auto; Simpl).
+  all: try (try unfold exec_load_rd_a in H1; try destruct (Mem.loadv _ _ _); inv H1; Simpl).
+  all: try (try unfold exec_load_double in H0; destruct (Mem.loadv _ _ _); simpl in *;
+            try destruct (Mem.loadv _ _ _); simpl in *; inv H0; Simpl).
+  all: try (try unfold exec_store_rs_a in H0; try destruct (Mem.storev _ _ _); inv H0; auto; Simpl).
+  all: try (try unfold exec_store_double in H1; destruct (Mem.storev _ _ _); simpl in *;
+            try destruct (Mem.storev _ _ _); simpl in *; inv H1; auto; Simpl).
+  - (* alloc *)
+    destruct (Mem.alloc _ _ _); destruct (Mem.store _ _ _); inv H1; auto; Simpl.
+  - (* free *)
+    destruct (rs1 SP); try discriminate; destruct (Mem.free _ _ _ _); inv H1; Simpl.
 Qed.
 
+End EPC.
+
+(*
+
 (* For PostpassSchedulingproof *)
 
 Lemma regset_double_set: