Asmblockgenproof finished !

2 files changed, 132 insertions, 215 deletions

diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v
index 586286bd..1abcb570 100644
--- a/aarch64/Asmblockgenproof.v
+++ b/aarch64/Asmblockgenproof.v
@@ -77,11 +77,6 @@ Qed.
 Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs),
   Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs.
 
-(*Lemma functions_bound_max_pos: forall fb f,
-  Genv.find_funct_ptr ge fb = Some (Internal f) ->
-  (max_pos next f) <= Ptrofs.max_unsigned.
-Admitted.*)
-
 (** * Proof of semantic preservation *)
 
 (** Semantic preservation is proved using a complex simulation diagram
@@ -881,7 +876,7 @@ exploit builtin_args_match; eauto. intros [vargs' [P Q]].
           eapply preg_vals; eauto.
           all: eauto.
         intros EC.
-        exploit transl_cbranch_correct_true; eauto. intros (rs', H).
+        exploit transl_cbranch_correct_1; eauto. intros (rs', H).
         destruct H as [ES [ECFI]].
         exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC).
         assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. }
@@ -909,7 +904,7 @@ exploit builtin_args_match; eauto. intros [vargs' [P Q]].
           all: eauto.
         intros EC.
 
-        exploit transl_cbranch_correct_false; eauto. intros (rs', H).
+        exploit transl_cbranch_correct_1; eauto. intros (rs', H).
         destruct H as [ES [ECFI]].
         exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC).
         assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. }
diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v
index 870211b8..dd7803cd 100644
--- a/aarch64/Asmblockgenproof1.v
+++ b/aarch64/Asmblockgenproof1.v
@@ -1121,214 +1121,6 @@ Proof.
   destruct r; try contradiction; destruct v1; auto; destruct v2; auto.
 Qed.
 
-Lemma cmpu_bool_some_b: forall n x rs m0 b tbb,
-  Int.eq n Int.zero = true ->
-  Val.cmp_bool Ceq (rs (preg_of m0)) (Vint n) = Some b ->
-  ireg_of m0 = OK x ->
-  Val_cmpu_bool Ceq (incrPC (Ptrofs.repr (size tbb)) rs x) (Vint Int.zero) = Some b.
-Proof.
-  intros.
-  replace (Vint Int.zero) with (Vint n).
-  2: { apply f_equal. apply Int.same_if_eq; auto. }
-  unfold incrPC. Simpl. replace (rs (preg_of m0)) with (rs x) in H0. auto.
-  apply f_equal. symmetry. apply ireg_of_eq; auto.
-Qed.
-
-Lemma transl_cbranch_correct_1:
-  forall cond args lbl c k b m ms sp rs m' tbb bdy,
-  transl_cond_branch cond args lbl k = OK (bdy,c) ->
-  eval_condition cond (List.map ms args) m = Some b ->
-  agree ms sp rs ->
-  Mem.extends m m' ->
-  exists rs',
-     exec_straight_opt ge lk bdy rs m' k rs' m'
-  /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = eval_branch fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m' (Some b)
-  /\ forall r, data_preg r = true -> rs'#r = rs#r.
-Proof.
-  intros until bdy; intros TR EC AG MEMX.
-  set (vl' := map rs (map preg_of args)).
-  assert (EVAL': eval_condition cond vl' m' = Some b).
-  { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. }
-  destruct cond; unfold transl_cond_branch in TR;
-  try unfold transl_cond_branch_default in TR;
-  simpl in TR; destruct args; ArgsInv.
-- (* Ccomp *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_signed_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b).
-  { apply eval_testcond_compare_sint; auto. } rewrite H. auto.
-  destruct r; reflexivity || discriminate.
-- (* Ccompu *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b).
-  { apply eval_testcond_compare_uint; auto. } rewrite H. auto.
-  destruct r; reflexivity || discriminate.
-- (* Ccompimm *)
-admit.
-(*   destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))];
-  destruct c0; try destruct (Int.eq n Int.zero) eqn:IEQ;
-  monadInv TR; try monadInv EQ; econstructor; split;
-  try (econstructor; try apply exec_straight_one);
-  simpl in *; eauto; try (split; intros; auto).
-  all: try (erewrite (cmpu_bool_some_b n x rs m0 b tbb); eauto; assumption).
-  unfold incrPC; Simpl.
-  try (rewrite (cmpu_bool_some_b n x rs m0 b tbb); auto).
-  + monadInv TR; try monadInv EQ. econstructor; split. econstructor; apply exec_straight_one. simpl in *; eauto.
-    split; intros; auto. unfold compare_int, incrPC. Simpl. auto.
-    assert (Val_cmpu_bool Ceq (incrPC (Ptrofs.repr (size tbb)) rs x) (Vint Int.zero) = Some b).
-    { replace (Vint Int.zero) with (Vint n).
-      2: { apply f_equal. apply Int.same_if_eq; auto. }
-      unfold incrPC. Simpl. replace (rs (preg_of m0)) with (rs x) in EVAL'. auto.
-      apply f_equal. symmetry. apply ireg_of_eq; auto. }
-     rewrite H; auto.
-    inv EQ.
-    split; intros; auto. assert (eval_testcond (cond_for_unsigned_cmp c0)
-       (incrPC (Ptrofs.repr (size tbb)) (compare_int rs (rs x) (rs x0))) = Some b).
-  { apply eval_testcond_compare_uint; auto. } rewrite H. auto.
-  destruct r; reflexivity || discriminate.
-  
-  destruct (is_arith_imm32 n); [|destruct (is_arith_imm32 (Int.neg n))].
-+ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
-  split; intros. rewrite Int.repr_unsigned. apply eval_testcond_compare_sint; auto. 
-  destruct r; reflexivity || discriminate.
-+ econstructor; split.
-  apply exec_straight_one. simpl. rewrite Int.repr_unsigned, Int.neg_involutive. eauto. auto.
-  split; intros. apply eval_testcond_compare_sint; auto. 
-  destruct r; reflexivity || discriminate.
-+ exploit (exec_loadimm32 X16 n). intros (rs' & A & B & C).
-  econstructor; split.
-  eapply exec_straight_trans. eexact A. apply exec_straight_one.
-  simpl. rewrite B, C by eauto with asmgen. eauto. auto.
-  split; intros. apply eval_testcond_compare_sint; auto. 
-  transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. *)
-- (* Ccompuimm *)
-  admit.
-- (* Ccompshift *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_signed_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb))
-        (compare_int rs (rs x) (eval_shift_op_int (rs x0) (transl_shift s a)))) = Some b).
-  { apply eval_testcond_compare_sint; auto. rewrite transl_eval_shift; auto. } rewrite H. auto.
-  destruct r; reflexivity || discriminate.
-- (* Ccompushift *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb))
-        (compare_int rs (rs x) (eval_shift_op_int (rs x0) (transl_shift s a)))) = Some b).
-  { apply eval_testcond_compare_uint; auto. rewrite transl_eval_shift; auto. } rewrite H. auto.
-  destruct r; reflexivity || discriminate.
-- (* Cmaskzero *) admit.
-- (* Cmasknotzero *) admit.
-- (* Ccompl *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_signed_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_long rs (rs x) (rs x0))) = Some b).
-  { apply eval_testcond_compare_slong; auto. } rewrite H. auto.
-  destruct r; reflexivity || discriminate.
-- (* Ccomplu *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_long rs (rs x) (rs x0))) = Some b).
-  { apply eval_testcond_compare_ulong; auto. eapply Val_cmplu_bool_correct; eauto. } rewrite H. auto.
-  destruct r; reflexivity || discriminate.
-- (* Ccomplimm *) admit.
-- (* Ccompluimm *) admit.
-- (* Ccomplshift *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_signed_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb))
-        (compare_long rs (rs x) (eval_shift_op_long (rs x0) (transl_shift s a)))) = Some b).
-  { apply eval_testcond_compare_slong; auto. rewrite transl_eval_shiftl; auto. } rewrite H. auto.
-  destruct r; reflexivity || discriminate.
-- (* Ccomplushift *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_unsigned_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb))
-        (compare_long rs (rs x) (eval_shift_op_long (rs x0) (transl_shift s a)))) = Some b).
-  { apply eval_testcond_compare_ulong; auto. rewrite transl_eval_shiftl; auto.
-    eapply Val_cmplu_bool_correct; eauto. } rewrite H. auto.
-  destruct r; reflexivity || discriminate.
-- (* Cmasklzero *) admit.
-- (* Cmasknotzero *) admit.
-- (* Ccompf *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_float_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (rs x0))) = Some b).
-  { apply eval_testcond_compare_float; auto. } rewrite H. auto.
-  destruct r; discriminate || rewrite compare_float_inv; auto.
-- (* Cnotcompf *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_float_not_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (rs x0))) = Some b).
-  { apply eval_testcond_compare_not_float; auto. } rewrite H. auto.
-  destruct r; discriminate || rewrite compare_float_inv; auto.
-- (* Ccompfzero *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_float_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (Vfloat Float.zero))) = Some b).
-  { apply eval_testcond_compare_float; auto. } rewrite H. auto.
-  destruct r; discriminate || rewrite compare_float_inv; auto.
-- (* Cnotcompfzero *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_float_not_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_float rs (rs x) (Vfloat Float.zero))) = Some b).
-  { apply eval_testcond_compare_not_float; auto. } rewrite H. auto.
-  destruct r; discriminate || rewrite compare_float_inv; auto.
-- (* Ccompfs *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_float_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (rs x0))) = Some b).
-  { apply eval_testcond_compare_single; auto. } rewrite H. auto.
-  destruct r; discriminate || rewrite compare_single_inv; auto.
-- (* Cnotcompfs *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_float_not_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (rs x0))) = Some b).
-  { apply eval_testcond_compare_not_single; auto. } rewrite H. auto.
-  destruct r; discriminate || rewrite compare_single_inv; auto.
-- (* Ccompfszero *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_float_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (Vsingle Float32.zero))) = Some b).
-  { apply eval_testcond_compare_single; auto. } rewrite H. auto.
-  destruct r; discriminate || rewrite compare_single_inv; auto.
-- (* Cnotcompfszero *)
-  econstructor; split. econstructor; apply exec_straight_one. simpl; eauto.
-  split; intros. assert (eval_testcond (cond_for_float_not_cmp c0)
-     (incrPC (Ptrofs.repr (size tbb)) (compare_single rs (rs x) (Vsingle Float32.zero))) = Some b).
-  { apply eval_testcond_compare_not_single; auto. } rewrite H. auto.
-  destruct r; discriminate || rewrite compare_single_inv; auto.
-Admitted.
-
-Lemma transl_cbranch_correct_true:
-  forall cond args lbl k c m ms sp rs m' tbb bdy,
-  transl_cond_branch cond args lbl k = OK (bdy,c) ->
-  eval_condition cond (List.map ms args) m = Some true ->
-  agree ms sp rs ->
-  Mem.extends m m' ->
-  exists rs',
-     exec_straight_opt ge lk bdy rs m' k rs' m'
-  /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = goto_label fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m'
-  /\ forall r, data_preg r = true -> rs'#r = rs#r.
-Proof.
-  intros. eapply transl_cbranch_correct_1 with (b := true); eauto.
-Qed.
-
-Lemma transl_cbranch_correct_false:
-  forall cond args lbl k c m ms sp rs m' tbb bdy,
-  transl_cond_branch cond args lbl k = OK (bdy,c) ->
-  eval_condition cond (List.map ms args) m = Some false ->
-  agree ms sp rs ->
-  Mem.extends m m' ->
-  exists rs',
-     exec_straight_opt ge lk bdy rs m' k rs' m'
-  /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m' = Next (incrPC (Ptrofs.repr (size tbb)) rs') m'
-  /\ forall r, data_preg r = true -> rs'#r = rs#r.
-Proof.
-  intros. exploit transl_cbranch_correct_1. all: eauto.
-Qed.
-
 Lemma transl_cond_correct:
   forall cond args k c rs m,
   transl_cond cond args k = OK c ->
@@ -1515,6 +1307,136 @@ Proof.
   destruct r; discriminate || rewrite compare_single_inv; auto.
 Qed.
 
+Lemma transl_cond_correct':
+  forall cond args k c tbb rs m,
+  transl_cond cond args k = OK c ->
+  exists rs',
+     exec_straight ge lk c rs m k rs' m
+  /\ (forall b,
+      eval_condition cond (map rs (map preg_of args)) m = Some b ->
+      eval_testcond (cond_for_cond cond) (incrPC (Ptrofs.repr (size tbb)) rs') = Some b)
+  /\ forall r, data_preg r = true -> rs'#r = rs#r.
+Proof.
+  intros until m; intros TR.
+  eapply transl_cond_correct; eauto.
+Qed.
+  
+Lemma transl_cbranch_correct_1:
+  forall cond args lbl c k b m rs tbb bdy,
+  transl_cond_branch cond args lbl k = OK (bdy,c) ->
+  eval_condition cond (map rs (map preg_of args)) m = Some b ->
+  exists rs',
+     exec_straight_opt ge lk bdy rs m k rs' m
+  /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m =
+        (if b then goto_label fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m else
+        Next (incrPC (Ptrofs.repr (size tbb)) rs') m)
+  /\ forall r, data_preg r = true -> rs'#r = rs#r.
+Proof.
+intros until bdy; intros TR EV.
+  assert (Archi.ptr64 = true) as SF; auto.
+  assert (DFL:
+    transl_cond_branch_default cond args lbl k = OK (bdy,c) ->
+    exists rs',
+       exec_straight_opt ge lk bdy rs m k rs' m
+    /\ exec_cfi ge fn c (incrPC (Ptrofs.repr (size tbb)) rs') m = eval_branch fn lbl (incrPC (Ptrofs.repr (size tbb)) rs') m (Some b)
+    /\ forall r, data_preg r = true -> rs'#r = rs#r).
+  {
+    unfold transl_cond_branch_default; intros. monadInv H.
+    exploit transl_cond_correct'; eauto. intros (rs' & A & B & C).
+    eexists; split.
+    apply exec_straight_opt_intro. eexact A.
+    split; auto. simpl. rewrite (B b) by auto. auto. 
+  }
+Local Opaque transl_cond transl_cond_branch_default.
+  destruct args as [ | a1 args]; simpl in TR; auto.
+  destruct args as [ | a2 args]; simpl in TR; auto.
+  destruct cond; simpl in TR; auto.
+- (* Ccompimm *)
+  destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto; 
+  apply Int.same_if_eq in N0; subst n; ArgsInv.
++ (* Ccompimm Cne 0 *)
+  econstructor; split. econstructor.
+  split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV.
+  unfold incrPC. Simpl. rewrite EQRSX. simpl. auto.
++ (* Ccompimm Ceq 0 *)
+  econstructor; split. econstructor.
+  split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
+  unfold incrPC. Simpl. rewrite EQRSX. simpl.
+  destruct (Int.eq i Int.zero); auto.
+- (* Ccompuimm *)
+  destruct c0; auto; destruct (Int.eq n Int.zero) eqn:N0; auto.
+  apply Int.same_if_eq in N0; subst n; ArgsInv.
++ (* Ccompuimm Cne 0 *)
+  econstructor; split. econstructor.
+  split; auto. simpl. apply Val_cmpu_bool_correct in EV.
+  unfold incrPC. Simpl. rewrite EV. auto.
++ (* Ccompuimm Ceq 0 *)
+  monadInv TR. ArgsInv. simpl in *.
+  econstructor; split. econstructor.
+  split; auto. simpl. unfold incrPC. Simpl.
+  apply Int.same_if_eq in N0; subst.
+  rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cne), EV.
+  destruct b; auto.
+- (* Cmaskzero *)
+  destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv.
+  econstructor; split. econstructor.
+  split; auto. simpl.
+  erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto.
+  unfold incrPC. Simpl.
+  rewrite (Val.negate_cmp_bool Ceq), EV. destruct b; auto.
+- (* Cmasknotzero *)
+  destruct (Int.is_power2 n) as [bit|] eqn:P2; auto. ArgsInv.
+  econstructor; split. econstructor.
+  split; auto. simpl.
+  erewrite <- Int.mul_pow2, Int.mul_commut, Int.mul_one by eauto.
+  unfold incrPC. Simpl.
+  rewrite EV. auto.
+- (* Ccomplimm *)
+  destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto; 
+  apply Int64.same_if_eq in N0; subst n; ArgsInv.
++ (* Ccomplimm Cne 0 *)
+  econstructor; split. econstructor.
+  split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV.
+  unfold incrPC. Simpl. rewrite EQRSX. simpl. auto.
++ (* Ccomplimm Ceq 0 *)
+  econstructor; split. econstructor.
+  split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
+  unfold incrPC. Simpl. rewrite EQRSX. simpl.
+  destruct (Int64.eq i Int64.zero); auto.
+- (* Ccompluimm *)
+  destruct c0; auto; destruct (Int64.eq n Int64.zero) eqn:N0; auto;
+  apply Int64.same_if_eq in N0; subst n; ArgsInv.
++ (* Ccompluimm Cne 0 *)
+  econstructor; split. econstructor.
+  split; auto. simpl. apply Val_cmplu_bool_correct in EV.
+  unfold incrPC. Simpl. rewrite EV. auto.
++ (* Ccompluimm Ceq 0 *)
+  econstructor; split. econstructor.
+  split; auto. simpl. destruct (rs x) eqn:EQRSX; simpl in EV; inv EV. simpl.
+  unfold incrPC. Simpl. rewrite EQRSX. simpl.
+  destruct (Int64.eq i Int64.zero); auto.
+  unfold incrPC. Simpl. rewrite EQRSX. simpl.
+  rewrite SF in *; simpl in *.
+  rewrite Int64.eq_true in *.
+  destruct ((Mem.valid_pointer m b0 (Ptrofs.unsigned i) || Mem.valid_pointer m b0 (Ptrofs.unsigned i - 1))); simpl in *.
+  assert (b = true). { destruct b; try congruence. }
+  rewrite H; auto. discriminate.
+- (* Cmasklzero *)
+  destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv.
+  econstructor; split. econstructor.
+  split; auto.
+  erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto.
+  unfold incrPC. Simpl.
+  rewrite (Val.negate_cmpl_bool Ceq), EV. destruct b; auto.
+- (* Cmasklnotzero *)
+  destruct (Int64.is_power2' n) as [bit|] eqn:P2; auto. ArgsInv.
+  econstructor; split. econstructor.
+  split; auto.
+  erewrite <- Int64.mul_pow2', Int64.mul_commut, Int64.mul_one by eauto.
+  unfold incrPC. Simpl.
+  rewrite EV. auto.
+Qed.
+
 Lemma transl_op_correct:
   forall op args res k (rs: regset) m v c,
   transl_op op args res k = OK c ->