Addressed issues #734 #743 #744 #748 #749 #751 and added a few more u…

…ser lemmas

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.
 

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.

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:

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. 
 

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).

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

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;