Commit edadb0e7 authored by Michael Sammler's avatar Michael Sammler
Browse files

split out heap_loc_eq

parent 8e8dd5a8
Pipeline #51712 passed with stage
in 14 minutes and 12 seconds
......@@ -242,6 +242,10 @@ Definition heap_state_loc_in_bounds (l : loc) (n : nat) (st : heap_state) : Prop
al.(al_start) l.2
l.2 + n al_end al.
Lemma heap_state_loc_in_bounds_has_alloc_id l n σ:
heap_state_loc_in_bounds l n σ aid, l.1 = ProvAlloc (Some aid).
Proof. rewrite /heap_state_loc_in_bounds. naive_solver. Qed.
(** Checks that the location [l] is inbounds of its allocation
(one-past-the-end is allowed) and this allocation is still alive *)
Definition valid_ptr (l : loc) (st : heap_state) : Prop :=
......@@ -251,6 +255,10 @@ Lemma valid_ptr_in_allocation_range l σ:
valid_ptr l σ min_alloc_start l.2 max_alloc_end.
Proof. move => [_][?][?][]?[]?[[]]???. lia. Qed.
Lemma valid_ptr_has_alloc_id l σ:
valid_ptr l σ aid, l.1 = ProvAlloc (Some aid).
Proof. rewrite /valid_ptr => ?. apply: heap_state_loc_in_bounds_has_alloc_id. naive_solver. Qed.
Definition addr_in_range_alloc (a : addr) (aid : alloc_id) (st : heap_state) : Prop :=
alloc, st.(hs_allocs) !! aid = Some alloc a alloc.
......@@ -281,6 +289,74 @@ Proof.
apply _.
Qed.
(** ** Comparing pointers
[heap_loc_eq l1 l2] returns whether two pointers compare equal.
None means that the comparison is undefined. *)
Definition heap_loc_eq (l1 l2 : loc) (st : heap_state) : option bool :=
(* null pointers are equal *)
if bool_decide (l1 = NULL_loc l2 = NULL_loc) then
Some true
(* function pointers are different from NULL pointers
TODO: Check that the address of the function pointer is not 0?*)
else if bool_decide ((l1 = NULL_loc l2.1 = ProvFnPtr) (l1.1 = ProvFnPtr l2 = NULL_loc)) then
Some false
(* Allocations are different from NULL pointers. But the comparison
is only defined if the location is in bounds of its allocation. *)
else if bool_decide (l1 = NULL_loc) then
guard (heap_state_loc_in_bounds l2 0 st);
Some false
else if bool_decide (l2 = NULL_loc) then
guard (heap_state_loc_in_bounds l1 0 st);
Some false
(* Two function pointers compare equal if their address is equal. *)
else if bool_decide (l1.1 = ProvFnPtr l2.1 = ProvFnPtr) then
Some (bool_decide (l1.2 = l2.2))
else
(* Two allocations can be compared if they are both alive and in
bounds (it is ok if they have different provenances). Comparison
compares the addresses. *)
guard (valid_ptr l1 st);
guard (valid_ptr l2 st);
Some (bool_decide (l1.2 = l2.2)).
Lemma heap_loc_eq_symmetric l1 l2 st:
heap_loc_eq l1 l2 st = heap_loc_eq l2 l1 st.
Proof.
rewrite /heap_loc_eq.
repeat case_bool_decide=> //; repeat case_option_guard => //; naive_solver.
Qed.
Lemma heap_loc_eq_NULL_NULL st:
heap_loc_eq NULL_loc NULL_loc st = Some true.
Proof. rewrite /heap_loc_eq. case_bool_decide; naive_solver. Qed.
Lemma heap_loc_eq_alloc_NULL l st:
heap_state_loc_in_bounds l 0 st
heap_loc_eq l NULL_loc st = Some false.
Proof.
move => Hlib. move: (Hlib) => /heap_state_loc_in_bounds_has_alloc_id[??]. rewrite /heap_loc_eq.
do 3 (case_bool_decide; [naive_solver|]). case_bool_decide => //. by rewrite option_guard_True.
Qed.
Lemma heap_loc_eq_fnptr_NULL l st:
l.1 = ProvFnPtr
heap_loc_eq l NULL_loc st = Some false.
Proof.
rewrite /heap_loc_eq => ?. do 3 (case_bool_decide; [naive_solver|]). naive_solver.
Qed.
Lemma heap_loc_eq_alloc_alloc l1 l2 st:
valid_ptr l1 st
valid_ptr l2 st
heap_loc_eq l1 l2 st = Some (bool_decide (l1.2 = l2.2)).
Proof.
move => Hv1 Hv2. move: (Hv1) => /valid_ptr_has_alloc_id[??]. move: (Hv2) => /valid_ptr_has_alloc_id[??].
destruct l1, l2; simplify_eq/=.
rewrite /heap_loc_eq.
do 5 (case_bool_decide; [naive_solver|]).
by rewrite !option_guard_True.
Qed.
(** ** MemCast: Transforming bytes read from memory.
[mem_cast] is corresponds to the [abst] function in the VIP paper.
......@@ -430,14 +506,6 @@ Inductive free_blocks : heap_state → list (loc * layout) → heap_state → Pr
free_blocks σ' ls σ''
free_blocks σ ((l, ly) :: ls) σ''.
Lemma heap_state_loc_in_bounds_has_alloc_id l n σ:
heap_state_loc_in_bounds l n σ aid, l.1 = ProvAlloc (Some aid).
Proof. rewrite /heap_state_loc_in_bounds. naive_solver. Qed.
Lemma valid_ptr_has_alloc_id l σ:
valid_ptr l σ aid, l.1 = ProvAlloc (Some aid).
Proof. rewrite /valid_ptr => ?. apply: heap_state_loc_in_bounds_has_alloc_id. naive_solver. Qed.
Lemma free_block_inj hs l ly hs1 hs2:
free_block hs l ly hs1 free_block hs l ly hs2 hs1 = hs2.
Proof. destruct l. inversion 1; simplify_eq. by inversion 1; simplify_eq/=. Qed.
......
......@@ -250,67 +250,30 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
valid_ptr l2 σ.(st_heap)
val_of_Z ((l1.2 - l2.2) `div` ly.(ly_size)) ptrdiff_t None = Some v
eval_bin_op (PtrDiffOp ly) PtrOp PtrOp σ v1 v2 v
| RelOpPNull v1 v2 σ l v op b p a rit:
val_to_loc v1 = Some l
l = (ProvAlloc p, a)
v2 = NULL
heap_state_loc_in_bounds l 0%nat σ.(st_heap)
match op with
| EqOp rit => Some (false, rit)
| NeOp rit => Some (true, rit)
| _ => None
end = Some (b, rit)
val_of_Z (Z_of_bool b) rit None = Some v
eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpNullP v1 v2 σ l v op b p a rit:
v1 = NULL
val_to_loc v2 = Some l
l = (ProvAlloc p, a)
heap_state_loc_in_bounds l 0%nat σ.(st_heap)
match op with
| EqOp rit => Some (false, rit)
| NeOp rit => Some (true, rit)
| _ => None
end = Some (b, rit)
val_of_Z (Z_of_bool b) rit None = Some v
eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpNullNull v1 v2 σ v op b rit:
v1 = NULL
v2 = NULL
match op with
| EqOp rit => Some (true, rit)
| NeOp rit => Some (false, rit)
| _ => None
end = Some (b, rit)
val_of_Z (Z_of_bool b) rit None = Some v
eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpPP v1 v2 σ l1 l2 p1 p2 a1 a2 v b op rit:
| CmpOpPP v1 v2 σ l1 l2 v op e b rit:
val_to_loc v1 = Some l1
val_to_loc v2 = Some l2
(* Note that this is technically redundant due to the valid_ptr,
but we still have it for clarity. *)
l1 = (ProvAlloc p1, a1)
l2 = (ProvAlloc p2, a2)
valid_ptr l1 σ.(st_heap) valid_ptr l2 σ.(st_heap)
heap_loc_eq l1 l2 σ.(st_heap) = Some e
match op with
| EqOp rit => Some (bool_decide (a1 = a2), rit)
| NeOp rit => Some (bool_decide (a1 a2), rit)
| LtOp rit => if bool_decide (p1 = p2) then Some (bool_decide (a1 < a2), rit) else None
| GtOp rit => if bool_decide (p1 = p2) then Some (bool_decide (a1 > a2), rit) else None
| LeOp rit => if bool_decide (p1 = p2) then Some (bool_decide (a1 <= a2), rit) else None
| GeOp rit => if bool_decide (p1 = p2) then Some (bool_decide (a1 >= a2), rit) else None
| EqOp rit => Some (e, rit)
| NeOp rit => Some (negb e, rit)
| _ => None
end = Some (b, rit)
val_of_Z (Z_of_bool b) rit None = Some v
eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpFnPP v1 v2 σ l1 l2 a1 a2 v b op rit:
| RelOpPP v1 v2 σ l1 l2 p a1 a2 v b op rit:
val_to_loc v1 = Some l1
val_to_loc v2 = Some l2
l1 = (ProvFnPtr, a1)
l2 = (ProvFnPtr, a2)
(* Note that this enforces that the locations have the same provenance. *)
l1 = (ProvAlloc p, a1)
l2 = (ProvAlloc p, a2)
valid_ptr l1 σ.(st_heap) valid_ptr l2 σ.(st_heap)
(* Equal comparison is handled by heap_loc_eq *)
match op with
| EqOp rit => Some (bool_decide (a1 = a2), rit)
| NeOp rit => Some (bool_decide (a1 a2), rit)
| LtOp rit => Some (bool_decide (a1 < a2), rit)
| GtOp rit => Some (bool_decide (a1 > a2), rit)
| LeOp rit => Some (bool_decide (a1 <= a2), rit)
| GeOp rit => Some (bool_decide (a1 >= a2), rit)
| _ => None
end = Some (b, rit)
val_of_Z (Z_of_bool b) rit None = Some v
......@@ -493,13 +456,13 @@ comparing pointers? (see lambda rust) *)
val_to_loc v2 = Some l
valid_ptr (l.1, a) σ.(st_heap)
expr_step (CopyAllocId (IntOp it) (Val v1) (Val v2)) σ [] (Val (val_of_loc (l.1, a))) σ []
| IfES v it e1 e2 n σ:
| IfESI v it e1 e2 n σ:
val_to_Z v it = Some n
expr_step (IfE (IntOp it) (Val v) e1 e2) σ [] (if bool_decide (n 0) then e1 else e2) σ []
| IfESP v e1 e2 l σ:
| IfESP v e1 e2 l σ b:
val_to_loc v = Some l
(if bool_decide (l NULL_loc) then heap_state_loc_in_bounds l 0%nat σ.(st_heap) else True)
expr_step (IfE PtrOp (Val v) e1 e2) σ [] (if bool_decide (l NULL_loc) then e1 else e2) σ []
heap_loc_eq l NULL_loc σ.(st_heap) = Some b
expr_step (IfE PtrOp (Val v) e1 e2) σ [] (if b then e2 else e1) σ []
(* no rule for StuckE *)
.
......@@ -514,13 +477,13 @@ Inductive stmt_step : stmt → runtime_function → state → list Empty_set →
v2 `has_layout_val` (ot_layout ot)
heap_at l (ot_layout ot) v' start_st σ.(st_heap).(hs_heap)
stmt_step (Assign o ot (Val v1) (Val v2) s) rf σ [] (to_rtstmt rf end_stmt) (heap_fmap (heap_upd l end_val end_st) σ) []
| IfSS it v s1 s2 rf σ n:
| IfSSI it v s1 s2 rf σ n:
val_to_Z v it = Some n
stmt_step (IfS (IntOp it) (Val v) s1 s2) rf σ [] (to_rtstmt rf ((if bool_decide (n 0) then s1 else s2))) σ []
| IfSSP v s1 s2 rf σ l:
| IfSSP v s1 s2 rf σ l b:
val_to_loc v = Some l
(if bool_decide (l NULL_loc) then heap_state_loc_in_bounds l 0%nat σ.(st_heap) else True)
stmt_step (IfS PtrOp (Val v) s1 s2) rf σ [] (to_rtstmt rf ((if bool_decide (l NULL_loc) then s1 else s2))) σ []
heap_loc_eq l NULL_loc σ.(st_heap) = Some b
stmt_step (IfS PtrOp (Val v) s1 s2) rf σ [] (to_rtstmt rf ((if b then s2 else s1))) σ []
| SwitchS rf σ v n m bs s def it :
val_to_Z v it = Some n
( i : nat, m !! n = Some i is_Some (bs !! i))
......
......@@ -507,13 +507,15 @@ Proof.
by iMod (alloc_alive_loc_to_valid_ptr with "Hl2 Ha Hσ") as %?.
}
iApply fupd_mask_intro; [done|]. iIntros "HE".
destruct l1, l2; simplify_eq/=. iSplit.
{ iPureIntro. destruct op; eexists _; apply: RelOpPP => //; repeat case_bool_decide; naive_solver. }
destruct l1, l2; simplify_eq/=. iSplit. {
iPureIntro. destruct op; simplify_eq/=; eexists _; try by apply: RelOpPP => //; repeat case_bool_decide; naive_solver.
all: apply: CmpOpPP => //; by rewrite ?heap_loc_eq_alloc_alloc//= negb_bool_decide_eq.
}
iDestruct "HΦ" as "(_&_&HΦ)". iIntros "!>" (v' Hstep). iMod "HE". iModIntro. iFrame.
inversion Hstep; simplify_eq => //.
all: try rewrite val_to_of_loc in Hv1; simplify_eq.
all: try rewrite val_to_of_loc in Hv2; simplify_eq.
destruct op; repeat case_bool_decide; by simplify_eq.
- revert select (heap_loc_eq _ _ _ = _). rewrite heap_loc_eq_alloc_alloc // => ?. simplify_eq.
destruct op; simplify_eq/= => //. by repeat case_bool_decide => //; simplify_eq/=.
- destruct op; repeat case_bool_decide; by simplify_eq.
Qed.
Lemma wp_ptr_offset Φ vl l E it o ly vo:
......@@ -632,34 +634,58 @@ Lemma wp_offset_of_union Φ ul m E:
Φ (i2v 0 size_t) - WP OffsetOfUnion ul m @ E {{ Φ }}.
Proof. by iApply @wp_value. Qed.
Lemma wp_if Φ it v e1 e2 n:
Lemma wp_if_int Φ it v e1 e2 n:
val_to_Z v it = Some n
(if bool_decide (n 0) then WP e1 {{ Φ }} else WP e2 {{ Φ }}) -
WP IfE (IntOp it) (Val v) e1 e2 {{ Φ }}.
Proof.
iIntros (?) "HΦ".
iApply wp_lift_expr_step; auto.
iIntros (σ1) "?". iModIntro. iSplit; first by eauto 8 using IfES.
iIntros (σ1) "?". iModIntro. iSplit; first by eauto 8 using IfESI.
iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
iSplit => //. iFrame. by case_bool_decide.
Qed.
Definition wp_if_precond (l : loc) : iProp Σ :=
match l.1 with | ProvNull => l = NULL_loc | ProvAlloc _ => loc_in_bounds l 0 | _ => True end.
Lemma wp_if_precond_null:
wp_if_precond NULL_loc.
Proof. rewrite /wp_if_precond/=. by iPureIntro. Qed.
Lemma wp_if_precond_alloc l:
loc_in_bounds l 0 -
wp_if_precond l.
Proof.
iIntros "Hlib". rewrite /wp_if_precond.
by iDestruct (loc_in_bounds_has_alloc_id with "Hlib") as %[? ->].
Qed.
Lemma wp_if_precond_heap_loc_eq l σ:
wp_if_precond l -
state_ctx σ -
heap_loc_eq l NULL_loc σ.(st_heap) = Some (bool_decide (l = NULL_loc)).
Proof.
rewrite/wp_if_precond. iIntros "Hlib Hσ". case_match.
- iDestruct "Hlib" as %?; simplify_eq. iPureIntro. rewrite heap_loc_eq_NULL_NULL. by case_bool_decide.
- iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hlib Hσ") as %Hlib. iPureIntro.
rewrite heap_loc_eq_alloc_NULL //. case_bool_decide => //; simplify_eq.
- iPureIntro. rewrite heap_loc_eq_fnptr_NULL //. case_bool_decide => //; simplify_eq.
Qed.
Lemma wp_if_ptr Φ v e1 e2 l:
val_to_loc v = Some l
(if bool_decide (l NULL_loc) then loc_in_bounds l 0 else True) -
wp_if_precond l -
(if bool_decide (l NULL_loc) then WP e1 {{ Φ }} else WP e2 {{ Φ }}) -
WP IfE PtrOp (Val v) e1 e2 {{ Φ }}.
Proof.
iIntros (?) "Hlib HΦ".
iApply wp_lift_expr_step; auto.
iIntros (σ1) "Hσ1". iModIntro. case_bool_decide.
- iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hlib Hσ1") as %Hlib.
iSplit. { iPureIntro; repeat eexists _; apply IfESP; rewrite ?bool_decide_true //. }
iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
iSplit => //. iFrame. by case_bool_decide.
- iSplit. { iPureIntro; repeat eexists _; apply IfESP; rewrite ?bool_decide_false //. eauto. }
iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
iSplit => //. iFrame. by case_bool_decide.
iIntros (σ1) "Hσ1". iModIntro.
iDestruct (wp_if_precond_heap_loc_eq with "Hlib Hσ1") as %?.
iSplit; first by eauto 8 using IfESP.
iIntros (? ? σ2 efs Hst ?) "!> !>". inv_expr_step.
iSplit => //. iFrame. by repeat case_bool_decide.
Qed.
Lemma wp_skip Φ v E:
......@@ -984,29 +1010,26 @@ Lemma wps_if Q Ψ it v s1 s2 n:
Proof.
iIntros (Hn) "Hs". rewrite !stmt_wp_eq. iIntros (?? ->) "?".
iApply wp_lift_stmt_step. iIntros (?) "Hσ".
iModIntro. iSplit; first by eauto 8 using IfSS.
iModIntro. iSplit; first by eauto 8 using IfSSI.
iIntros (???? Hstep ?) "!> !>". inv_stmt_step. iSplit; first done.
iFrame "Hσ". case_bool_decide; by iApply "Hs".
Qed.
Lemma wps_if_ptr Q Ψ v s1 s2 l:
val_to_loc v = Some l
(if bool_decide (l NULL_loc) then loc_in_bounds l 0 else True) -
wp_if_precond l -
(if bool_decide (l NULL_loc) then WPs s1 {{ Q, Ψ }} else WPs s2 {{ Q, Ψ }}) -
WPs (if{PtrOp}: (Val v) then s1 else s2) {{ Q , Ψ }}.
Proof.
iIntros (Hl) "Hlib Hs". rewrite !stmt_wp_eq. iIntros (?? ->) "?".
iApply wp_lift_stmt_step. iIntros (σ1) "Hσ1". case_bool_decide.
- iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hlib Hσ1") as %Hlib.
iModIntro. iSplit. { iPureIntro; repeat eexists _; apply IfSSP; rewrite ?bool_decide_true //. }
iIntros (???? Hstep ?) "!> !>". inv_stmt_step. iSplit; first done.
iFrame "Hσ1". rewrite bool_decide_true; last done. by iApply "Hs".
- iModIntro. iSplit. { iPureIntro; repeat eexists _; apply IfSSP; rewrite ?bool_decide_false //. eauto. }
iIntros (???? Hstep ?) "!> !>". inv_stmt_step. iSplit; first done.
iFrame "Hσ1". rewrite bool_decide_false; last eauto. by iApply "Hs".
iApply wp_lift_stmt_step. iIntros (σ1) "Hσ1 !>".
iDestruct (wp_if_precond_heap_loc_eq with "Hlib Hσ1") as %?.
iSplit; first by eauto 8 using IfSSP.
iIntros (???? Hstep ?) "!> !>". inv_stmt_step. iSplit; first done.
iFrame "Hσ1". do 2 case_bool_decide => //; by iApply "Hs".
Qed.
Lemma wps_assert Q Ψ it v s n:
Lemma wps_assert_int Q Ψ it v s n:
val_to_Z v it = Some n n 0
WPs s {{ Q, Ψ }} -
WPs (assert{IntOp it}: Val v; s) {{ Q , Ψ }}.
......@@ -1017,12 +1040,12 @@ Qed.
Lemma wps_assert_ptr Q Ψ v s l:
val_to_loc v = Some l l NULL_loc
loc_in_bounds l 0 -
wp_if_precond l -
WPs s {{ Q, Ψ }} -
WPs (assert{PtrOp}: Val v; s) {{ Q , Ψ }}.
Proof.
iIntros (Hv Hl) "#Hlib Hs". rewrite /notation.Assert.
iApply wps_if_ptr; rewrite ?bool_decide_true => //.
iIntros (Hv Hl) "Hlib Hs". rewrite /notation.Assert.
iApply (wps_if_ptr with "Hlib"); by rewrite ?bool_decide_true.
Qed.
Definition wps_block (P : iProp Σ) (b : label) (Q : gmap label stmt) (Ψ : val iProp Σ) : iProp Σ :=
......
......@@ -152,6 +152,9 @@ Proof. by case_bool_decide. Qed.
Lemma if_bool_decide_eq_branches {A} P `{!Decision P} (x : A) :
(if bool_decide P then x else x) = x.
Proof. by case_bool_decide. Qed.
Lemma negb_bool_decide_eq {A} (x y : A) `{!EqDecision A} :
negb (bool_decide (x = y)) = bool_decide (x y).
Proof. by repeat case_bool_decide. Qed.
(** * apply_dfun *)
(* TODO: does something like this exist in Iris? *)
......
......@@ -187,37 +187,36 @@ Section own.
TypedUnOp p (p ◁ₗ{β} ty)%I (CastOp PtrOp) PtrOp :=
λ T, i2p (type_cast_ptr_ptr p β ty T).
Lemma type_if_ptr l β ty T1 T2 n `{!LocInBounds ty β n}:
(l ◁ₗ{β} ty - T1) -
Lemma type_if_ptr_own l β ty T1 T2:
(l ◁ₗ{β} ty - (loc_in_bounds l 0 True) T1) -
typed_if PtrOp l (l ◁ₗ{β} ty) T1 T2.
Proof.
iIntros "HT1 Hl".
iDestruct (loc_in_bounds_in_bounds with "Hl") as "#Hlib".
iDestruct ("HT1" with "Hl") as "[[#Hlib _] HT]".
iDestruct (loc_in_bounds_has_alloc_id with "Hlib") as %[? H].
iExists l. iSplit; first by rewrite val_to_of_loc.
rewrite bool_decide_true; last by move: l H => [??] /= -> //.
iSplit. { iApply loc_in_bounds_shorten; last done. lia. }
by iApply "HT1".
iSplitR. { by iApply wp_if_precond_alloc. }
by rewrite bool_decide_true; last by move: l H => [??] /= -> //.
Qed.
Global Instance type_if_ptr_inst (l : loc) β ty n `{!LocInBounds ty β n}:
Global Instance type_if_ptr_own_inst (l : loc) β ty:
TypedIf PtrOp l (l ◁ₗ{β} ty)%I :=
λ T1 T2, i2p (type_if_ptr l β ty T1 T2 n).
λ T1 T2, i2p (type_if_ptr_own l β ty T1 T2).
Lemma type_assert_ptr l β ty n `{!LocInBounds ty β n} s fn ls R Q:
(l ◁ₗ{β} ty - typed_stmt s fn ls R Q) -
Lemma type_assert_ptr_own l β ty s fn ls R Q:
(l ◁ₗ{β} ty - (loc_in_bounds l 0 True) typed_stmt s fn ls R Q) -
typed_assert PtrOp l (l ◁ₗ{β} ty) s fn ls R Q.
Proof.
iIntros "HT Hl".
iDestruct (loc_in_bounds_in_bounds with "Hl") as "#Hlib".
iIntros "HT1 Hl".
iDestruct ("HT1" with "Hl") as "[[#Hlib _] HT]".
iDestruct (loc_in_bounds_has_alloc_id with "Hlib") as %[? H].
iExists l. iSplit; first by rewrite val_to_of_loc.
iSplit. { iPureIntro. move: l H => [??] /= -> //. }
iSplit. { iApply loc_in_bounds_shorten; last done. lia. }
iSplitR. { by iApply wp_if_precond_alloc. }
by iApply "HT".
Qed.
Global Instance type_assert_ptr_inst (l : loc) β ty n `{!LocInBounds ty β n}:
Global Instance type_assert_ptr_own_inst (l : loc) β ty:
TypedAssert PtrOp l (l ◁ₗ{β} ty)%I :=
λ s fn ls R Q, i2p (type_assert_ptr l β ty n s fn ls R Q).
λ s fn ls R Q, i2p (type_assert_ptr_own l β ty s fn ls R Q).
Lemma type_place_cast_ptr_ptr K l ty β T:
typed_place K l β ty T -
......@@ -527,39 +526,15 @@ Section null.
by iIntros "_".
Qed.
Lemma eval_bin_op_ptr_null (b : bool) op h (p : loc) v:
heap_state_loc_in_bounds p 0 h.(st_heap)
(if b then op = NeOp i32 else op = EqOp i32)
eval_bin_op op PtrOp PtrOp h p NULL v
val_of_Z (Z_of_bool b) i32 None = Some v.
Lemma eval_bin_op_ptr_cmp l1 l2 op h v b it:
match op with | EqOp it' | NeOp it' => it' = it | _ => False end
heap_loc_eq l1 l2 h.(st_heap) = Some b
eval_bin_op op PtrOp PtrOp h l1 l2 v
val_of_Z (Z_of_bool (if op is EqOp _ then b else negb b)) it None = Some v.
Proof.
move => Hlib ?. have [??]:= heap_state_loc_in_bounds_has_alloc_id _ _ _ Hlib.
destruct p; simplify_eq/=. destruct b => //; split => Heq; subst.
1, 3: inversion Heq; unfold NULL in *; rewrite ->?val_to_of_loc in *; simplify_eq; done.
all: eapply RelOpPNull => //; rewrite val_to_of_loc //.
Qed.
Lemma eval_bin_op_null_ptr (b : bool) op h (p : loc) v:
heap_state_loc_in_bounds p 0 h.(st_heap)
(if b then op = NeOp i32 else op = EqOp i32)
eval_bin_op op PtrOp PtrOp h NULL p v
val_of_Z (Z_of_bool b) i32 None = Some v.
Proof.
move => Hlib ?. have [??]:= heap_state_loc_in_bounds_has_alloc_id _ _ _ Hlib.
destruct p; simplify_eq/=. destruct b => //; split => Heq; subst.
1, 3: inversion Heq; unfold NULL in *; rewrite ->?val_to_of_loc in *; simplify_eq; done.
all: eapply RelOpNullP => //; rewrite val_to_of_loc //.
Qed.
Lemma eval_bin_op_null_null (b : bool) op h v:
(if b then op = EqOp i32 else op = NeOp i32)
eval_bin_op op PtrOp PtrOp h NULL NULL v
val_of_Z (Z_of_bool b) i32 None = Some v.
Proof.
move => ?.
destruct b => //; split => Heq; subst.
1, 3: inversion Heq; unfold NULL in *; rewrite ->?val_to_of_loc in *; simplify_eq => //.
all: econstructor => //; rewrite /i2v Heq.
move => ??. split.
- inversion 1; rewrite ->?val_to_of_loc in *; simplify_eq/= => //; destruct op => //; simplify_eq; done.
- move => ?. apply: CmpOpPP; rewrite ?val_to_of_loc //. destruct op => //; simplify_eq; done.
Qed.
Lemma type_binop_null_null v1 v2 op T:
......@@ -568,10 +543,9 @@ Section null.
typed_bin_op v1 (v1 ◁ᵥ null) v2 (v2 ◁ᵥ null) op PtrOp PtrOp T.
Proof.
iIntros "[% HT]" (-> -> Φ) "HΦ".
have ?:= val_of_Z_bool (if op is EqOp i32 then true else false) i32.
have Hz:= val_of_Z_bool (if op is EqOp i32 then true else false) i32.
iApply (wp_binop_det_pure (i2v (Z_of_bool (if op is EqOp i32 then true else false)) i32)). {
move => ??.
rewrite (eval_bin_op_null_null (if op is EqOp i32 then true else false)); destruct op => //; naive_solver.
move => ??. rewrite eval_bin_op_ptr_cmp // ?heap_loc_eq_NULL_NULL //= Hz. naive_solver.
}
iApply "HΦ" => //. by destruct op.
Qed.
......@@ -587,14 +561,13 @@ Section null.
iIntros "[% HT] Hl" (-> Φ) "HΦ".
iDestruct (loc_in_bounds_in_bounds with "Hl") as "#Hb".
iDestruct (loc_in_bounds_shorten _ _ 0 with "Hb") as "#Hb0"; first by lia.
have ?:= val_of_Z_bool (if op is EqOp i32 then false else true) i32.
have Hz:= val_of_Z_bool (if op is EqOp i32 then false else true) i32.
iApply (wp_binop_det (i2v (Z_of_bool (if op is EqOp i32 then false else true)) i32)).
iIntros (σ) "Hctx". iApply fupd_mask_intro; [set_solver|]. iIntros "HE".
iSplit. {
iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hb0 Hctx") as %?.
iPureIntro => ?.
rewrite (eval_bin_op_ptr_null (if op is EqOp i32 then false else true)); destruct op => //; naive_solver.
}
iDestruct (loc_in_bounds_has_alloc_id with "Hb") as %[??].
iDestruct (wp_if_precond_heap_loc_eq with "[] Hctx") as %?. { by iApply wp_if_precond_alloc. }
iSplit.
{ iPureIntro => ?. rewrite eval_bin_op_ptr_cmp //. case_bool_decide => //; simplify_eq. naive_solver. }
iModIntro. iMod "HE". iModIntro. iFrame.
iApply