From fd1300d4dabbaeefc305894bdca21f7ea701928e Mon Sep 17 00:00:00 2001 From: Andrew Appel Date: Fri, 1 Mar 2024 17:30:30 -0500 Subject: [PATCH 1/2] Addressed issues #734 #743 #744 #748 #749 #751 and added a few more user lemmas --- floyd/data_at_lemmas.v | 360 ++++++++++++++++++++++++++++++++++++++ floyd/deadvars.v | 31 ++-- floyd/field_at.v | 35 +++- floyd/forward.v | 8 +- floyd/functional_base.v | 6 + floyd/nested_loadstore.v | 1 - floyd/sc_set_load_store.v | 4 +- floyd/simpl_reptype.v | 4 +- 8 files changed, 421 insertions(+), 28 deletions(-) diff --git a/floyd/data_at_lemmas.v b/floyd/data_at_lemmas.v index b0cd6190e5..25ff272f97 100644 --- a/floyd/data_at_lemmas.v +++ b/floyd/data_at_lemmas.v @@ -1150,6 +1150,314 @@ intros. reflexivity. Qed. + +Section Foo. + +Import predicates_hered predicates_sl res_predicates msl.normalize. + +Lemma address_mapsto_8bytes_aux: + forall (sh : Share.t) + (b0 b1 b2 b3 b4 b5 b6 b7: byte) + (b : block) (i : ptrofs) + (SZ : Ptrofs.unsigned i + 8 < Ptrofs.modulus) + (r : readable_share sh), + +predicates_sl.sepcon + (predicates_sl.sepcon + (predicates_sl.sepcon + (predicates_sl.sepcon + (predicates_sl.sepcon + (predicates_sl.sepcon + (predicates_sl.sepcon + (predicates_hered.allp + (res_predicates.jam + (adr_range_dec (b, Ptrofs.unsigned i) (size_chunk Mint8unsigned)) + (fun loc : address => + res_predicates.yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth (Z.to_nat (snd loc - snd (b, Ptrofs.unsigned i))) + [Byte b0] Undef)) sh loc) res_predicates.noat)) + (predicates_hered.allp + (res_predicates.jam + (adr_range_dec + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 1))) + (size_chunk Mint8unsigned)) + (fun loc : address => + res_predicates.yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth + (Z.to_nat + (snd loc + - snd + (b, + Ptrofs.unsigned + (Ptrofs.add i (Ptrofs.repr 1))))) + [Byte b1] Undef)) sh loc) res_predicates.noat))) + (predicates_hered.allp + (res_predicates.jam + (adr_range_dec (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 2))) + (size_chunk Mint8unsigned)) + (fun loc : address => + res_predicates.yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth + (Z.to_nat + (snd loc + - snd + (b, + Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 2))))) + [Byte b2] Undef)) sh loc) res_predicates.noat))) + (predicates_hered.allp + (res_predicates.jam + (adr_range_dec (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 3))) + (size_chunk Mint8unsigned)) + (fun loc : address => + res_predicates.yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth + (Z.to_nat + (snd loc + - snd + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 3))))) + [Byte b3] Undef)) sh loc) res_predicates.noat))) + (predicates_hered.allp + (res_predicates.jam + (adr_range_dec (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 4))) + (size_chunk Mint8unsigned)) + (fun loc : address => + res_predicates.yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth + (Z.to_nat + (snd loc + - snd (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 4))))) + [Byte b4] Undef)) sh loc) res_predicates.noat))) + (predicates_hered.allp + (res_predicates.jam + (adr_range_dec (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 5))) + (size_chunk Mint8unsigned)) + (fun loc : address => + res_predicates.yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth + (Z.to_nat + (snd loc + - snd (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 5))))) + [Byte b5] Undef)) sh loc) res_predicates.noat))) + (predicates_hered.allp + (res_predicates.jam + (adr_range_dec (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 6))) + (size_chunk Mint8unsigned)) + (fun loc : address => + res_predicates.yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth + (Z.to_nat + (snd loc - snd (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 6))))) + [Byte b6] Undef)) sh loc) res_predicates.noat))) + (predicates_hered.allp + (res_predicates.jam + (adr_range_dec (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 7))) + (size_chunk Mint8unsigned)) + (fun loc : address => + res_predicates.yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth + (Z.to_nat + (snd loc - snd (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 7))))) + [Byte b7] Undef)) sh loc) res_predicates.noat)) = +predicates_hered.allp + (res_predicates.jam (adr_range_dec (b, Ptrofs.unsigned i) (size_chunk Mint64)) + (fun loc : address => + res_predicates.yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth (Z.to_nat (snd loc - snd (b, Ptrofs.unsigned i))) + [Byte b0; Byte b1; Byte b2; Byte b3; Byte b4; Byte b5; Byte b6; Byte b7] + Undef)) sh loc) res_predicates.noat). +Proof. +intros. + + simpl snd. + simpl size_chunk. + repeat match goal with |- context [Ptrofs.add i (Ptrofs.repr ?A)] => + replace (Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr A))) + with (A + Ptrofs.unsigned i) + by (unfold Ptrofs.add; rewrite (Ptrofs.unsigned_repr (Z.pos _)) by rep_lia; + rewrite Ptrofs.unsigned_repr by rep_lia; rep_lia) + end. + change [Byte b0; Byte b1; Byte b2; Byte b3; Byte b4; Byte b5; Byte b6; Byte b7] + with (map Byte [b0;b1;b2;b3;b4;b5;b6;b7]). + + +repeat lazymatch goal with |- _ = ?R => + lazymatch R with context [nth _ (map Byte ?al)] => + lazymatch al with _ :: _ => + let len := constr:(Zlength al) in let len := eval compute in len in + let part1 := constr:(sublist.sublist 0 (len-1) al) in let part1 := eval compute in part1 in + let part2 := constr:(sublist.sublist (len-1) len al) in let part2 := eval compute in part2 in + rewrite (res_predicates.allp_jam_split2 _ _ _ + (fun loc : address => + yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth (Z.to_nat (snd loc - Ptrofs.unsigned i)) + (map Byte al) Undef)) sh loc) + (fun loc : address => + yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth (Z.to_nat (snd loc - Ptrofs.unsigned i)) + (map Byte part1) Undef)) sh loc) + (fun loc : address => + yesat compcert_rmaps.RML.R.NoneP + (compcert_rmaps.VAL + (nth (Z.to_nat (snd loc - ((len-1)+Ptrofs.unsigned i))) + (map Byte part2) Undef)) sh loc) + (adr_range_dec (b, Ptrofs.unsigned i) len) + (adr_range_dec (b, Ptrofs.unsigned i) (len-1)) + (adr_range_dec (b, (len-1) + Ptrofs.unsigned i) 1)); + [ + | eexists; apply res_predicates.is_resource_pred_YES_VAL' + | eexists; apply res_predicates.is_resource_pred_YES_VAL' + | eexists; apply res_predicates.is_resource_pred_YES_VAL' + | clear; split; intros [? ?]; simpl; intuition rep_lia + |intros; f_equal; f_equal; + destruct l; destruct H; subst; simpl snd; + change al with (List.app (sublist.sublist 0 (len-1) al) (sublist.sublist (len-1) len al)); + rewrite map_app, app_nth1 by (simpl; lia); + reflexivity + | intros; f_equal; f_equal; + destruct l; destruct H; subst; simpl snd; + change al with (List.app (sublist.sublist 0 (len-1) al) (sublist.sublist (len-1) len al)); + rewrite map_app, app_nth2 by (simpl; lia);simpl sublist.sublist; + simpl length; + match type of H0 with ?a <= _ < _ => assert (z=a) by lia end; subst z; + rewrite Z.sub_diag; + replace (_ - _) with (len-1) by lia; + reflexivity + |intros; left; destruct H0; hnf in H0; rewrite H0 in H1; clear H0; + destruct l, H; subst; simpl snd in *; + rewrite nth_map' with (d' := Byte.zero) in H1 by (simpl; lia); + inv H1; apply I + ]; + f_equal; (set (jj:= len-1) in *; compute in jj; subst jj) (* really_simplify (len-1) *) + end end end. +Qed. + +Lemma address_mapsto_8bytes_forward: + forall + (AP: Archi.ptr64 = true) (* Perhaps this premise could be eliminated. *) + (sh : Share.t) + (b0 b1 b2 b3 b4 b5 b6 b7 : byte) + (b : block) + (i : ptrofs) + (SZ : Ptrofs.unsigned i + 8 < Ptrofs.modulus) + (AL : (8 | Ptrofs.unsigned i)) + (r : readable_share sh), +predicates_hered.derives + (predicates_sl.sepcon + (predicates_sl.sepcon + (predicates_sl.sepcon + (predicates_sl.sepcon + (predicates_sl.sepcon + (predicates_sl.sepcon + (predicates_sl.sepcon + (res_predicates.address_mapsto Mint8unsigned + (Vubyte b0) sh (b, Ptrofs.unsigned i)) + (res_predicates.address_mapsto Mint8unsigned + (Vubyte b1) sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 1))))) + (res_predicates.address_mapsto Mint8unsigned + (Vubyte b2) sh (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 2))))) + (res_predicates.address_mapsto Mint8unsigned (Vubyte b3) sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 3))))) + (res_predicates.address_mapsto Mint8unsigned (Vubyte b4) sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 4))))) + (res_predicates.address_mapsto Mint8unsigned (Vubyte b5) sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 5))))) + (res_predicates.address_mapsto Mint8unsigned (Vubyte b6) sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 6))))) + (res_predicates.address_mapsto Mint8unsigned (Vubyte b7) sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 7))))) + (res_predicates.address_mapsto Mint64 + (Vlong (Int64.repr (decode_int [b0; b1; b2; b3; b4; b5; b6; b7]))) sh + (b, Ptrofs.unsigned i)). +Proof. +intros. + unfold res_predicates.address_mapsto. rewrite <- !exp_equiv. + repeat change (seplog.exp ?A) with (predicates_hered.exp A). + normalize.normalize. + intros bl7 [A7 [B7 _]] bl6 bl5 bl4 bl3 bl2 bl1 bl0. + normalize.normalize. + destruct H as [A6 [ B6 _]]. + destruct H0 as [A5 [ B5 _]]. + destruct H1 as [A4 [ B4 _]]. + destruct H2 as [A3 [ B3 _]]. + destruct H3 as [A2 [ B2 _]]. + destruct H4 as [A1 [ B1 _]]. + destruct H5 as [A0 [ B0 _]]. + destruct bl0 as [ | c0 [|]]; inv A0; inv B0. + destruct bl1 as [ | c1 [|]]; inv A1; inv B1. + destruct bl2 as [ | c2 [|]]; inv A2; inv B2. + destruct bl3 as [ | c3 [|]]; inv A3; inv B3. + destruct bl4 as [ | c4 [|]]; inv A4; inv B4. + destruct bl5 as [ | c5 [|]]; inv A5; inv B5. + destruct bl6 as [ | c6 [|]]; inv A6; inv B6. + destruct bl7 as [ | c7 [|]]; inv A7; inv B7. + destruct c0; try discriminate H0. + destruct c1; try discriminate H1. + destruct c2; try discriminate H2. + destruct c3; try discriminate H3. + destruct c4; try discriminate H4. + destruct c5; try discriminate H5. + destruct c6; try discriminate H6. + destruct c7; try discriminate H7. + apply decode_val_Vubyte_inj in H0,H1,H2,H3,H4,H5,H6,H7; subst. + apply (predicates_hered.exp_right (map Byte [b0;b1;b2;b3;b4;b5;b6;b7])). + rewrite predicates_hered.prop_true_andp. + 2:{ split3. reflexivity. reflexivity. apply AL. } + rewrite address_mapsto_8bytes_aux; auto. +Qed. + + +Lemma nonlock_permission_8bytes: + forall (sh : Share.t) + (b : block) (i : ptrofs) + (SZ : Ptrofs.unsigned i + 8 < Ptrofs.modulus), +(res_predicates.nonlock_permission_bytes sh (b, Ptrofs.unsigned i) 1 + * res_predicates.nonlock_permission_bytes sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 1))) 1 + * res_predicates.nonlock_permission_bytes sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 2))) 1 + * res_predicates.nonlock_permission_bytes sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 3))) 1 + * res_predicates.nonlock_permission_bytes sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 4))) 1 + * res_predicates.nonlock_permission_bytes sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 5))) 1 + * res_predicates.nonlock_permission_bytes sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 6))) 1 + * res_predicates.nonlock_permission_bytes sh + (b, Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr 7))) 1)%logic = +res_predicates.nonlock_permission_bytes sh (b, Ptrofs.unsigned i) 8. +Proof. +intros. + repeat match goal with |- context [Ptrofs.add i (Ptrofs.repr ?A)] => + replace (Ptrofs.unsigned (Ptrofs.add i (Ptrofs.repr A))) + with (A + Ptrofs.unsigned i) + by (unfold Ptrofs.add; rewrite (Ptrofs.unsigned_repr (Z.pos _)) by rep_lia; + rewrite Ptrofs.unsigned_repr by rep_lia; rep_lia) + end. + rewrite (res_predicates.nonlock_permission_bytes_split2 7 1 8 sh) by lia. + rewrite (res_predicates.nonlock_permission_bytes_split2 6 1 7 sh) by lia. + rewrite (res_predicates.nonlock_permission_bytes_split2 5 1 6 sh) by lia. + rewrite (res_predicates.nonlock_permission_bytes_split2 4 1 5 sh) by lia. + rewrite (res_predicates.nonlock_permission_bytes_split2 3 1 4 sh) by lia. + rewrite (res_predicates.nonlock_permission_bytes_split2 2 1 3 sh) by lia. + rewrite (res_predicates.nonlock_permission_bytes_split2 1 1 2 sh) by lia. + repeat change (predicates_sl.sepcon ?A ?B) with (A * B)%logic. + rewrite !(Z.add_comm (Ptrofs.unsigned i)). + f_equal. +Qed. + Lemma tc_val_Vubyte: forall b, tc_val tuchar (Vubyte b). Proof. intros; red. @@ -1157,6 +1465,58 @@ simpl. rewrite Int.unsigned_repr by rep_lia. rep_lia. Qed. +End Foo. + +Lemma data_at_long_bytes_forward: + forall + (AP: Archi.ptr64 = true) (* Perhaps this premise could be eliminated. *) + sh + (b0 b1 b2 b3 b4 b5 b6 b7: byte) p, + field_compatible tulong [] p -> + (data_at sh tuchar (Vubyte b0) p * + data_at sh tuchar (Vubyte b1) (offset_val 1 p) * + data_at sh tuchar (Vubyte b2) (offset_val 2 p) * + data_at sh tuchar (Vubyte b3) (offset_val 3 p) * + data_at sh tuchar (Vubyte b4) (offset_val 4 p) * + data_at sh tuchar (Vubyte b5) (offset_val 5 p) * + data_at sh tuchar (Vubyte b6) (offset_val 6 p) * + data_at sh tuchar (Vubyte b7) (offset_val 7 p))%logic |-- + data_at sh tulong (Vlong (Int64.repr (decode_int [b0;b1;b2;b3;b4;b5;b6;b7]))) p. +Proof. + intros AP sh b0 b1 b2 b3 b4 b5 b6 b7 p. unfold data_at. unfold field_at. + intro. normalize.normalize. clear - H. simpl. + rewrite (prop_true_andp (field_compatible tulong [] p)) by auto. + destruct H as [H0 [_ [SZ [AL _]]]]. red in SZ. simpl sizeof in SZ. + destruct p; inversion H0. clear H0. + assert (8 | Ptrofs.unsigned i) + by (eapply align_compatible_rec_by_value_inv in AL; [ | reflexivity]; assumption). + clear AL. + Intros. + unfold at_offset. + rewrite !offset_offset_val. rewrite !Z.add_0_r. + simpl offset_val. rewrite !ptrofs_add_repr_0_r. + rewrite !data_at_rec_eq. simpl. + change (unfold_reptype ?x) with x. + unfold mapsto. + simpl access_mode; simpl type_is_volatile; cbv iota. + rewrite !(prop_true_andp _ _ (tc_val_Vubyte _)). + rewrite !(prop_false_andp (_ = _)) by (intro Hx; inv Hx). + rewrite !(prop_true_andp (tc_val tulong _)) by (apply Logic.I). + rewrite ?prop_and_mpred. + rewrite ?(prop_true_andp _ _ (tc_val_tc_val' _ _ (tc_val_Vubyte _))). + rewrite !(prop_true_andp (tc_val' tulong _)) by (apply tc_val_tc_val'; apply Logic.I). + rewrite ?(prop_true_andp _ _ (Z.divide_1_l _)). + rewrite !orp_FF. + rewrite (prop_true_andp (_ | _)) by apply H. + if_tac. +- + rewrite derives_eq. + apply address_mapsto_8bytes_forward; auto. +- rewrite nonlock_permission_8bytes; auto. + apply derives_refl. +Qed. + + Lemma nonlock_permission_4bytes: forall (sh : Share.t) (b : block) (i : ptrofs) diff --git a/floyd/deadvars.v b/floyd/deadvars.v index df73dd5418..c9683e4973 100644 --- a/floyd/deadvars.v +++ b/floyd/deadvars.v @@ -188,11 +188,14 @@ Ltac inhabited_value T := | prod ?A ?B => let x := inhabited_value A in let y := inhabited_value B in constr:(pair x y) - | _ => let t := eval unfold T in T in inhabited_value t + (* delete the old "eval unfold" that was here, and put it below as shown: *) | _ => match goal with | x:T |- _ => x | x := _ : T |- _ => x - | _ => fail 3 "cannot prove that type" T "is inhabited, so cannot compute deadvars. Fix this by asserting (X:"T") above the line" + | _ => let t := eval unfold T in T in + tryif constr_eq t T + then fail 3 "cannot prove that type" T "is inhabited, so cannot compute deadvars. Fix this by asserting (X:"T") above the line" + else inhabited_value t end end. @@ -259,16 +262,16 @@ Ltac find_dead_vars P c Q := let d := eval compute in d in d. -Ltac deadvars := +Ltac deadvars := lazymatch goal with | X := @abbreviate ret_assert ?Q |- semax _ ?P ?c ?Y => check_POSTCONDITION; - constr_eq X Y; + tryif constr_eq X Y then idtac else fail 99 "@abbreviate ret_assert above the line does not match postcondition"; match find_dead_vars P c Q with | nil => idtac | ?d => idtac "Dropping dead vars!"; drop_LOCALs d - end + fail 99 "deadvars failed for an unknown reason" + end | |- semax _ _ _ _ => check_POSTCONDITION; fail "deadvars: Postcondition must be an abbreviated local definition (POSTCONDITION); try abbreviate_semax first" @@ -277,18 +280,20 @@ Ltac deadvars := end. Tactic Notation "deadvars" "!" := - match goal with + lazymatch goal with + | |- semax _ _ _ _ => idtac + | |- _ => fail "deadvars!: the proof goal should be a semax" + end; + lazymatch goal with | X := @abbreviate ret_assert ?Q |- semax _ ?P ?c ?Y => - check_POSTCONDITION; - constr_eq X Y; - match find_dead_vars P c Q with - | nil => fail 2 "deadvars!: Did not find any dead variables" + tryif constr_eq X Y then idtac + else fail "deadvars!: Postcondition must be an abbreviated local definition (POSTCONDITION); try abbreviate_semax first"; + lazymatch find_dead_vars P c Q with + | nil => fail "deadvars!: Did not find any dead variables" | ?d => drop_LOCALs d end | |- semax _ _ _ _ => - check_POSTCONDITION; - fail 1 "deadvars!: Postcondition must be an abbreviated local definition (POSTCONDITION); try abbreviate_semax first" - | |- _ => fail 1 "deadvars!: the proof goal should be a semax" + fail "deadvars!: Postcondition must be an abbreviated local definition (POSTCONDITION); try abbreviate_semax first" end. diff --git a/floyd/field_at.v b/floyd/field_at.v index 13b54dbbeb..efa7219cf1 100644 --- a/floyd/field_at.v +++ b/floyd/field_at.v @@ -3071,9 +3071,9 @@ f_equal. Qed. Lemma data_at_int_or_ptr_int: - forall {CS: compspecs} i p, - data_at Tsh int_or_ptr_type (Vptrofs i) p - = data_at Tsh size_t (Vptrofs i) p. + forall {CS: compspecs} sh i p, + data_at sh int_or_ptr_type (Vptrofs i) p + = data_at sh size_t (Vptrofs i) p. Proof. intros. unfold data_at, field_at. @@ -3095,10 +3095,10 @@ Proof. Qed. Lemma data_at_int_or_ptr_ptr: - forall {CS: compspecs} t v p, + forall {CS: compspecs} sh t v p, isptr v -> - data_at Tsh int_or_ptr_type v p - = data_at Tsh (tptr t) v p. + data_at sh int_or_ptr_type v p + = data_at sh (tptr t) v p. Proof. intros. destruct v; try contradiction. @@ -3138,3 +3138,26 @@ Proof. rewrite N.eqb_refl. rewrite andb_false_r. reflexivity. Qed. + +Lemma nonempty_writable0_glb (shw shr : share) : writable0_share shw -> readable_share shr -> + nonempty_share (Share.glb shw shr). + (* this lemma might be convenient for users *) +Proof. +intros Hshw Hshr. +apply leq_join_sub in Hshw. +apply Share.ord_spec2 in Hshw. +rewrite Share.glb_commute, <- Hshw, Share.distrib1, Share.glb_commute, Share.lub_commute. +apply readable_nonidentity. +apply readable_share_lub. +apply readable_glb. +assumption. +Qed. + +Lemma nonempty_writable_glb (shw shr : share) : writable_share shw -> readable_share shr -> + nonempty_share (Share.glb shw shr). + (* this lemma might be convenient for users *) +Proof. +intros Hshw Hshr. +apply nonempty_writable0_glb; try assumption. +apply writable_writable0; assumption. +Qed. diff --git a/floyd/forward.v b/floyd/forward.v index 3d006c7960..3a03cbd36c 100644 --- a/floyd/forward.v +++ b/floyd/forward.v @@ -2877,15 +2877,15 @@ match goal with | |- semax ?Delta (|> PROPx ?P (LOCALx ?Q (SEPx ?R))) (Ssequence (Sifthenelse ?e ?c1 ?c2) _) _ => tryif (unify (orb (quickflow c1 nofallthrough) (quickflow c2 nofallthrough)) true) then (apply semax_if_seq; forward_if'_new) - else fail "Because your if-statement is followed by another statement, you need to do 'forward_if Post', where Post is a postcondition of type (environ->mpred) or of type Prop" + else fail 1 "Because your if-statement is followed by another statement, you need to do 'forward_if Post', where Post is a postcondition of type (environ->mpred) or of type Prop" | |- semax _ (@exp _ _ _ _) _ _ => - fail "First use Intros ... to take care of the EXistentially quantified variables in the precondition" + fail 1 "First use Intros ... to take care of the EXistentially quantified variables in the precondition" | |- semax _ _ (Sswitch _ _) _ => forward_switch' | |- semax _ _ (Ssequence (Sifthenelse _ _ _) _) _ => - fail "forward_if failed for some unknown reason, perhaps your precondition is not in canonical form" + fail 1 "forward_if failed for some unknown reason, perhaps your precondition is not in canonical form" | |- semax _ _ (Ssequence (Sswitch _ _) _) _ => - fail "Because your switch statement is followed by another statement, you need to do 'forward_if Post', where Post is a postcondition of type (environ->mpred) or of type Prop" + fail 1 "Because your switch statement is followed by another statement, you need to do 'forward_if Post', where Post is a postcondition of type (environ->mpred) or of type Prop" end. Lemma ENTAIL_break_normal: diff --git a/floyd/functional_base.v b/floyd/functional_base.v index 17639b40ee..541017ca20 100644 --- a/floyd/functional_base.v +++ b/floyd/functional_base.v @@ -40,6 +40,12 @@ Create HintDb entailer_rewrite discriminated. Require Import VST.veric.val_lemmas. +Lemma Vlong_inj : forall x y : int64, Vlong x = Vlong y -> x = y. +Proof. +intros. +inv H. auto. +Qed. + Lemma Vint_injective i j (H: Vint i = Vint j): i=j. Proof. inv H; trivial. Qed. diff --git a/floyd/nested_loadstore.v b/floyd/nested_loadstore.v index f5efc45066..cd3666ba72 100644 --- a/floyd/nested_loadstore.v +++ b/floyd/nested_loadstore.v @@ -606,7 +606,6 @@ Qed. Lemma field_at_app {cs: compspecs}: forall sh t gfs1 gfs2 v v' p, - field_compatible t nil p -> JMeq v v' -> field_at sh t (gfs1++gfs2) v p = field_at sh (nested_field_type t gfs2) gfs1 v' (field_address t gfs2 p). diff --git a/floyd/sc_set_load_store.v b/floyd/sc_set_load_store.v index d04f3aab47..a8b9a5cc1b 100644 --- a/floyd/sc_set_load_store.v +++ b/floyd/sc_set_load_store.v @@ -1738,8 +1738,8 @@ Ltac SEP_field_at_strong_unify' gfs := Ltac SEP_field_at_strong_unify gfs := match goal with - | |- data_at_ ?sh ?t ?p = _ /\ _ => - change (data_at_ sh t p) with (data_at sh t (default_val t) p); + | |- @data_at_ ?cs ?sh ?t ?p = _ /\ _ => + change (@data_at_ cs sh t p) with (@data_at cs sh t (default_val t) p); SEP_field_at_strong_unify' gfs | |- field_at_ _ _ _ _ = _ /\ _ => unfold field_at_; SEP_field_at_strong_unify' gfs diff --git a/floyd/simpl_reptype.v b/floyd/simpl_reptype.v index 5fbac24f99..dc471c5ed9 100644 --- a/floyd/simpl_reptype.v +++ b/floyd/simpl_reptype.v @@ -295,7 +295,7 @@ Ltac solve_load_rule_evaluation := | |- JMeq (@proj_reptype ?cs ?t ?gfs ?v) _ => let opaque_v := fresh "opaque_v" in remember v as opaque_v; - change proj_reptype with proj_reptype'; + change @proj_reptype with @proj_reptype'; cbv - [ sublist.Znth Int.repr JMeq myfst mysnd]; change @myfst with @fst; change @mysnd with @snd; @@ -345,7 +345,7 @@ Ltac solve_store_rule_evaluation := let h0 := fresh "h0" in let h1 := fresh "h1" in set (h0:=v0 : @reptype cs t); set (h1:=v1 : @reptype cs (@nested_field_type cs t gfs)); - change (upd_reptype t gfs h0 h1 = rhs); + change (@upd_reptype cs t gfs h0 h1 = rhs); remember_indexes gfs; let j := fresh "j" in match type of h0 with ?J => set (j := J) in h0 end; lazy beta zeta iota delta in j; subst j; From 84d350318938de20c19b22219071e956187ffef4 Mon Sep 17 00:00:00 2001 From: Andrew Appel Date: Mon, 4 Mar 2024 08:53:16 -0500 Subject: [PATCH 2/2] Fix a 32-bit issue --- floyd/data_at_lemmas.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/floyd/data_at_lemmas.v b/floyd/data_at_lemmas.v index 25ff272f97..046ed37648 100644 --- a/floyd/data_at_lemmas.v +++ b/floyd/data_at_lemmas.v @@ -1484,7 +1484,7 @@ Lemma data_at_long_bytes_forward: data_at sh tulong (Vlong (Int64.repr (decode_int [b0;b1;b2;b3;b4;b5;b6;b7]))) p. Proof. intros AP sh b0 b1 b2 b3 b4 b5 b6 b7 p. unfold data_at. unfold field_at. - intro. normalize.normalize. clear - H. simpl. + intro. normalize.normalize. clear - AP H. simpl. rewrite (prop_true_andp (field_compatible tulong [] p)) by auto. destruct H as [H0 [_ [SZ [AL _]]]]. red in SZ. simpl sizeof in SZ. destruct p; inversion H0. clear H0.