From 728888d8a3f70afd526f6c4454327f52ea4c4746 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 7 Jan 2021 17:47:55 +0100 Subject: Val_cmp* -> Val.mxcmp* --- aarch64/Asmblockgenproof1.v | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) (limited to 'aarch64/Asmblockgenproof1.v') diff --git a/aarch64/Asmblockgenproof1.v b/aarch64/Asmblockgenproof1.v index 754b49d6..61d77881 100644 --- a/aarch64/Asmblockgenproof1.v +++ b/aarch64/Asmblockgenproof1.v @@ -896,8 +896,8 @@ Ltac TranslOpBase := Lemma compare_int_spec: forall rs v1 v2, let rs' := compare_int rs v1 v2 in rs'#CN = (Val.negative (Val.sub v1 v2)) - /\ rs'#CZ = (Val_cmpu Ceq v1 v2) - /\ rs'#CC = (Val_cmpu Cge v1 v2) + /\ rs'#CZ = (Val.mxcmpu Ceq v1 v2) + /\ rs'#CC = (Val.mxcmpu Cge v1 v2) /\ rs'#CV = (Val.sub_overflow v1 v2). Proof. intros; unfold rs'; auto. @@ -912,7 +912,7 @@ Proof. unfold eval_testcond; rewrite B, C, D, E. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. - unfold Val_cmpu; simpl. destruct c; simpl. + unfold Val.mxcmpu; simpl. destruct c; simpl. - destruct (Int.eq i i0); auto. - destruct (Int.eq i i0); auto. - rewrite Int.lt_sub_overflow. destruct (Int.lt i i0); auto. @@ -924,7 +924,7 @@ Proof. Qed. Lemma eval_testcond_compare_uint: forall c v1 v2 b rs, - Val_cmpu_bool c v1 v2 = Some b -> + Val.mxcmpu_bool c v1 v2 = Some b -> eval_testcond (cond_for_unsigned_cmp c) (compare_int rs v1 v2) = Some b. Proof. intros. generalize (compare_int_spec rs v1 v2). @@ -932,7 +932,7 @@ Proof. unfold eval_testcond; rewrite B, C, D, E. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. - unfold Val_cmpu; simpl. destruct c; simpl. + unfold Val.mxcmpu; simpl. destruct c; simpl. - destruct (Int.eq i i0); auto. - destruct (Int.eq i i0); auto. - destruct (Int.ltu i i0); auto. @@ -944,8 +944,8 @@ Qed. Lemma compare_long_spec: forall rs v1 v2, let rs' := compare_long rs v1 v2 in rs'#CN = (Val.negativel (Val.subl v1 v2)) - /\ rs'#CZ = (Val_cmplu Ceq v1 v2) - /\ rs'#CC = (Val_cmplu Cge v1 v2) + /\ rs'#CZ = (Val.mxcmplu Ceq v1 v2) + /\ rs'#CC = (Val.mxcmplu Cge v1 v2) /\ rs'#CV = (Val.subl_overflow v1 v2). Proof. intros; unfold rs'; auto. @@ -977,7 +977,7 @@ Proof. unfold eval_testcond; rewrite B, C, D, E. destruct v1; try discriminate; destruct v2; try discriminate. simpl in H; inv H. - unfold Val_cmplu; simpl. destruct c; simpl. + unfold Val.mxcmplu; simpl. destruct c; simpl. - destruct (Int64.eq i i0); auto. - destruct (Int64.eq i i0); auto. - rewrite int64_sub_overflow. destruct (Int64.lt i i0); auto. @@ -989,12 +989,12 @@ Proof. Qed. Lemma eval_testcond_compare_ulong: forall c v1 v2 b rs, - Val_cmplu_bool c v1 v2 = Some b -> + Val.mxcmplu_bool c v1 v2 = Some b -> eval_testcond (cond_for_unsigned_cmp c) (compare_long rs v1 v2) = Some b. Proof. intros. generalize (compare_long_spec rs v1 v2). set (rs' := compare_long rs v1 v2). intros (B & C & D & E). - unfold eval_testcond; rewrite B, C, D, E; unfold Val_cmplu. + unfold eval_testcond; rewrite B, C, D, E; unfold Val.mxcmplu. destruct v1; try discriminate; destruct v2; try discriminate; simpl in H. - (* int-int *) inv H. destruct c; simpl. @@ -1207,7 +1207,7 @@ Proof. - (* Ccomplu *) econstructor; split. apply exec_straight_one. simpl; eauto. split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. + erewrite Val.mxcmplu_bool_correct; eauto. destruct r; reflexivity || discriminate. - (* Ccomplimm *) destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. @@ -1228,19 +1228,19 @@ Proof. destruct (is_arith_imm64 n); [|destruct (is_arith_imm64 (Int64.neg n))]. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros. rewrite Int64.repr_unsigned. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. + erewrite Val.mxcmplu_bool_correct; eauto. destruct r; reflexivity || discriminate. + econstructor; split. apply exec_straight_one. simpl. rewrite Int64.repr_unsigned, Int64.neg_involutive. eauto. split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. + erewrite Val.mxcmplu_bool_correct; eauto. destruct r; reflexivity || discriminate. + exploit (exec_loadimm64 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. split; intros. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. + erewrite Val.mxcmplu_bool_correct; eauto. transitivity (rs' r). destruct r; reflexivity || discriminate. auto with asmgen. - (* Ccomplshift *) econstructor; split. apply exec_straight_one. simpl; eauto. @@ -1249,7 +1249,7 @@ Proof. - (* Ccomplushift *) econstructor; split. apply exec_straight_one. simpl; eauto. split; intros. rewrite transl_eval_shiftl. apply eval_testcond_compare_ulong; auto. - erewrite Val_cmplu_bool_correct; eauto. + erewrite Val.mxcmplu_bool_correct; eauto. destruct r; reflexivity || discriminate. - (* Cmasklzero *) destruct (is_logical_imm64 n). @@ -1368,7 +1368,7 @@ Local Opaque transl_cond transl_cond_branch_default. 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. + split; auto. simpl. apply Val.mxcmpu_bool_correct in EV. unfold incrPC. Simpl. rewrite EV. auto. + (* Ccompuimm Ceq 0 *) monadInv TR. ArgsInv. simpl in *. @@ -1408,7 +1408,7 @@ Local Opaque transl_cond transl_cond_branch_default. 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. + split; auto. simpl. apply Val.mxcmplu_bool_correct in EV. unfold incrPC. Simpl. rewrite EV. auto. + (* Ccompluimm Ceq 0 *) econstructor; split. econstructor. -- cgit