Some progress in Asmblockgenproof

1 files changed, 211 insertions, 12 deletions

diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v
index bc4302ca..870211b8 100644
--- a/aarch64/Asmblockgenproof1.v
+++ b/aarch64/Asmblockgenproof1.v
@@ -1121,32 +1121,213 @@ Proof.
   destruct r; try contradiction; destruct v1; auto; destruct v2; auto.
 Qed.
 
-Lemma transl_cbranch_correct:
-  forall cond args lbl k c m ms b sp rs m' bdy t ofs,
-  transl_cond_branch cond args lbl k = OK (bdy, c) ->
+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' m' rs'' m'',
-     exec_body lk ge bdy rs m = Next rs' m'
-  /\ exec_exit ge fn ofs rs' m' (Some c) t rs'' 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' bdy,
-  transl_cond_branch cond args lbl k = OK (bdy, c) ->
+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', exists insn,
+  exists rs',
      exec_straight_opt ge lk bdy rs m' k rs' m'
-  /\ exec_cfi ge fn insn (nextinstr rs') m' = goto_label fn lbl (nextinstr 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.  *)
+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,
@@ -1727,6 +1908,24 @@ Proof.
   split. Simpl. intros; Simpl.
 Qed.
 
+Lemma storeptr_correct: forall (base: iregsp) ofs (src: ireg) k m m' (rs: regset),
+  Mem.storev Mint64 m (Val.offset_ptr rs#base ofs) rs#src = Some m' ->
+  preg_of_iregsp base <> IR X16 ->
+  (DR (IR (RR1 src))) <> (DR (IR (RR1 X16))) ->
+  exists rs',
+     exec_straight ge lk (storeptr_bc src base ofs k) rs m k rs' m'
+  /\ forall r, r <> PC -> r <> X16 -> rs' r = rs r.
+Proof.
+  intros. 
+  destruct (Val.offset_ptr rs#base ofs) eqn:V; try discriminate.
+  exploit indexed_memory_access_correct; eauto. intros (ad & rs' & A & B & C). 
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A.
+  apply exec_straight_one. simpl. unfold exec_store_rs_a. rewrite B, C, H. eauto.
+  discriminate. auto.
+  intros; Simpl. rewrite C; auto.
+Qed.
+
 Lemma loadind_correct:
   forall (base: iregsp) ofs ty dst k c (rs: regset) m v,
   loadind base ofs ty dst k = OK c ->