From 5a235199883dc01c54d17ae4f97794e5b156ed14 Mon Sep 17 00:00:00 2001 From: Russell O'Connor Date: Wed, 1 Feb 2023 16:34:56 -0500 Subject: [PATCH] Investigating alternate definition of Val.of_bool --- atomics/verif_lock.v | 2 +- compcert/common/Values.v | 2 +- compcert_new/common/Values.v | 2 +- floyd/compare_lemmas.v | 4 ++-- floyd/forward.v | 18 +++++++++--------- progs64/verif_strlib.v | 6 +++--- veric/binop_lemmas3.v | 12 ++++++------ 7 files changed, 23 insertions(+), 23 deletions(-) diff --git a/atomics/verif_lock.v b/atomics/verif_lock.v index db282683bf..0a87789b2f 100644 --- a/atomics/verif_lock.v +++ b/atomics/verif_lock.v @@ -121,7 +121,7 @@ Section PROOFS. unfold inv_for_lock. do 2 (apply allp_right; intros). eapply derives_trans, now_later. - Exists true; simpl; cancel. apply derives_refl. } + Exists true; simpl; cancel. } simpl. forward. simpl; Exists (p, i, g); unfold atomic_lock_inv; entailer!. diff --git a/compcert/common/Values.v b/compcert/common/Values.v index 891c9a88a8..21c08d8576 100644 --- a/compcert/common/Values.v +++ b/compcert/common/Values.v @@ -270,7 +270,7 @@ Definition notint (v: val) : val := | _ => Vundef end. -Definition of_bool (b: bool): val := if b then Vtrue else Vfalse. +Definition of_bool (b: bool): val := Vint (Int.repr (Z.b2z b)). Definition boolval (v: val) : val := match v with diff --git a/compcert_new/common/Values.v b/compcert_new/common/Values.v index a51a390f52..0375d6f75c 100644 --- a/compcert_new/common/Values.v +++ b/compcert_new/common/Values.v @@ -252,7 +252,7 @@ Definition notint (v: val) : val := | _ => Vundef end. -Definition of_bool (b: bool): val := if b then Vtrue else Vfalse. +Definition of_bool (b: bool): val := Vint (Int.repr (Z.b2z b)). Definition boolval (v: val) : val := match v with diff --git a/floyd/compare_lemmas.v b/floyd/compare_lemmas.v index 305c84f96d..c0937e702a 100644 --- a/floyd/compare_lemmas.v +++ b/floyd/compare_lemmas.v @@ -53,9 +53,9 @@ intros. apply prop_derives; intro. unfold tptr in H; simpl in H. unfold sem_binary_operation' in H. simpl in H. rewrite !andb_false_r in H. - destruct (v rho); inv H. + destruct (v rho); try discriminate. unfold sem_cmp_pp, strict_bool_val, nullval in *. - destruct Archi.ptr64 eqn:Hp; simpl in H1; + destruct Archi.ptr64 eqn:Hp; simpl in H; inv H; try solve [inv H1]; try solve [pose proof (Int64.eq_spec i Int64.zero); destruct (Int64.eq i Int64.zero); inv H1; auto]; diff --git a/floyd/forward.v b/floyd/forward.v index d93a9b693c..3eeb724ea5 100644 --- a/floyd/forward.v +++ b/floyd/forward.v @@ -1676,7 +1676,7 @@ Lemma typed_true_Cne_neq: forall x y, typed_true tint (force_val (sem_cmp_pp Cne x y)) -> x <> y. Proof. - intros. hnf in H. destruct x, y; try inversion H. + intros. hnf in H. destruct x, y; try discriminate H. - unfold sem_cmp_pp, strict_bool_val, Val.cmplu_bool, Val.cmpu_bool in H. destruct Archi.ptr64 eqn:Hp; simpl in H; try destruct (Int64.eq i i0) eqn:?; @@ -1697,7 +1697,7 @@ Proof. subst b i. inversion H. * intro. inversion H0. subst i. - pose proof (Ptrofs.eq_spec i0 i0). rewrite Heqb1 in H2. + pose proof (Ptrofs.eq_spec i0 i0). rewrite Heqb1 in H1. contradiction. + intro. inversion H0. subst b. contradiction. Qed. @@ -1706,7 +1706,7 @@ Lemma typed_true_Ceq_eq: forall x y, typed_true tint (force_val (sem_cmp_pp Ceq x y)) -> x = y. Proof. - intros. hnf in H. destruct x, y; try inversion H. + intros. hnf in H. destruct x, y; try discriminate H. - unfold sem_cmp_pp, strict_bool_val, Val.cmplu_bool, Val.cmpu_bool in H; destruct Archi.ptr64 eqn:Hp; simpl in H; try destruct (Int64.eq i i0) eqn:?; @@ -1740,7 +1740,7 @@ Lemma typed_false_Cne_eq: forall x y, typed_false tint (force_val (sem_cmp_pp Cne x y)) -> x = y. Proof. - intros. hnf in H. destruct x, y; try inversion H. + intros. hnf in H. destruct x, y; try discriminate H. - unfold sem_cmp_pp, strict_bool_val, Val.cmplu_bool, Val.cmpu_bool in H; destruct Archi.ptr64 eqn:Hp; simpl in H; try destruct (Int64.eq i i0) eqn:?; @@ -1773,7 +1773,7 @@ Lemma typed_false_Ceq_neq: forall x y, typed_false tint (force_val (sem_cmp_pp Ceq x y)) -> x <> y. Proof. - intros. hnf in H. destruct x, y; try inversion H. + intros. hnf in H. destruct x, y; try discriminate H. - unfold sem_cmp_pp, strict_bool_val, Val.cmplu_bool, Val.cmpu_bool in H. destruct Archi.ptr64 eqn:Hp; simpl in H; try destruct (Int64.eq i i0) eqn:?; @@ -1793,7 +1793,7 @@ Proof. * simpl in H. pose proof (Ptrofs.eq_spec i i0). rewrite Heqb1 in H0. subst b i. inversion H. * intro. inversion H0. subst b i. pose proof (Ptrofs.eq_spec i0 i0). - rewrite Heqb1 in H2. contradiction. + rewrite Heqb1 in H1. contradiction. + intro. inversion H0. contradiction. Qed. @@ -1935,9 +1935,9 @@ Lemma typed_true_negb_bool_val_p: (bool_val_p p))) -> p = nullval. Proof. -intros. destruct p; inv H. +intros. destruct p; try discriminate H; simpl in H. destruct Archi.ptr64 eqn:Hp; -(simpl in H1; +(simpl in H; inv H; try (pose proof (Int64.eq_spec i Int64.zero); destruct (Int64.eq i Int64.zero); inv H1; auto); try (pose proof (Int.eq_spec i Int.zero); @@ -1953,7 +1953,7 @@ Lemma typed_false_negb_bool_val_p: (bool_val_p p))) -> isptr p. Proof. -intros. destruct p; try solve [inv H0]; auto; rename H0 into H1. +intros. destruct p; try solve [discriminate H0]; auto; rename H0 into H1. simpl in H. simpl. destruct Archi.ptr64 eqn:Hp; diff --git a/progs64/verif_strlib.v b/progs64/verif_strlib.v index b375efef95..8f7fcad514 100644 --- a/progs64/verif_strlib.v +++ b/progs64/verif_strlib.v @@ -291,7 +291,6 @@ forward_loop (EX i : Z, forward. fold_Vbyte. forward_if (temp _t'1 (Val.of_bool (Z.eqb i (Zlength ls1) && Z.eqb i (Zlength ls2)))). { forward. - simpl force_val. rewrite Hs1 in *. destruct (Byte.eq_dec (Znth i (ls2 ++ [Byte.zero])) Byte.zero). + rewrite e; simpl force_val. @@ -300,8 +299,8 @@ forward_loop (EX i : Z, rewrite (proj2 (Z.eqb_eq i (Zlength ls1)) H6). rewrite (proj2 (Z.eqb_eq i (Zlength ls2)) H7). entailer!. - + - rewrite Int.eq_false. + + simpl (Z.b2z _). + rewrite (Int.eq_false (Int.repr (Byte.signed (Znth i (ls2 ++ [Byte.zero]))))). rewrite (proj2 (Z.eqb_eq i (Zlength ls1)) H6). rewrite Hs2 in n. rewrite (proj2 (Z.eqb_neq i (Zlength ls2))) by auto. @@ -529,6 +528,7 @@ forward_loop (EX i : Z, (* these two parts are not much simplified *) { forward. cstring1. entailer!. rewrite (proj2 (Z.eqb_eq _ _)) by auto. + simpl. destruct (Int.eq (Int.repr (Byte.signed (Znth (Zlength ls1) (ls2 ++ [Byte.zero])))) (Int.repr 0)) eqn:Heqb; do_repr_inj Heqb. (* utilize this internal tactic *) - rewrite (proj2 (Z.eqb_eq _ _)) by cstring. diff --git a/veric/binop_lemmas3.v b/veric/binop_lemmas3.v index 82ef812127..37a7b5ab77 100644 --- a/veric/binop_lemmas3.v +++ b/veric/binop_lemmas3.v @@ -240,13 +240,13 @@ Lemma int_type_tc_val_of_bool: forall t b, is_int_type t = true -> tc_val t (Val.of_bool b). Proof. intros. - destruct t as [| [| | |] [|] | | | | | | |]; + destruct t as [| [| | |] [|] | | | | | | |]; try discriminate; hnf; auto; clear H; - destruct b; simpl; auto; -change (Int.signed Int.one) with 1; -change (Int.signed Int.zero) with 0; -change (Int.unsigned Int.one) with 1; -change (Int.unsigned Int.zero) with 0; + destruct b; cbn; auto; try discriminate; +change (Int.signed (Int.repr 1)) with 1; +change (Int.signed (Int.repr 0)) with 0; +change (Int.unsigned (Int.repr 1)) with 1; +change (Int.unsigned (Int.repr 0)) with 0; change Byte.min_signed with (-128); change Byte.max_signed with 127; change Byte.max_unsigned with 255;