Commit 9f5876ce authored by Michael Sammler's avatar Michael Sammler
Browse files

Make integer to pointer casting rule more realistic

parent 21990cb1
Pipeline #49039 passed with stage
in 17 minutes and 19 seconds
......@@ -231,6 +231,21 @@ Definition alloc_id_alive (aid : alloc_id) (st : heap_state) : Prop :=
Definition block_alive (l : loc) (st : heap_state) : Prop :=
aid, l.1 = ProvAlloc (Some aid) alloc_id_alive aid st.
Global Instance alloc_id_alive_dec aid st : Decision (alloc_id_alive aid st).
Proof.
destruct (st.(hs_allocs) !! aid) as [alloc|] eqn: Haid.
2: { right. move => [?[??]]. simplify_eq. }
destruct (alloc.(al_alive)) eqn:?.
- left. eexists _. naive_solver.
- right. move => [?[??]]. destruct alloc; naive_solver.
Qed.
Global Instance block_alive_dec l st : Decision (block_alive l st).
Proof.
destruct (l.1) as [| [aid|] |] eqn: Hl.
1,3,4: try (right => -[?[??]]; destruct l; naive_solver).
eapply (exists_dec_unique aid); [| apply _]. destruct l; naive_solver.
Qed.
(** The address range between [l] and [l +ₗ n] (included) is in range of the
allocation that contains [l]. Note that we consider the 1-past-the-end
pointer to be in range of an allocation. *)
......
......@@ -337,9 +337,12 @@ Inductive eval_un_op : un_op → op_type → state → val → val → Prop :=
val_of_int_repr (IRLoc l) it = Some vt
block_alive l σ.(st_heap)
eval_un_op (CastOp (IntOp it)) PtrOp σ vs vt
| CastOpIP it σ vs vt l:
| CastOpIP it σ vs vt l l':
val_to_loc_weak vs it = Some l
val_of_loc l = vt
val_of_loc l' = vt
(** This is using that the address 0 is never alive. *)
l' = (if bool_decide (block_alive l σ.(st_heap)) then l else
(if bool_decide (l.2 = 0) then NULL_loc else (ProvAlloc None, l.2)))
eval_un_op (CastOp PtrOp) (IntOp it) σ vs vt
| NegOpI it σ vs vt n:
val_to_Z_weak vs it = Some n
......
......@@ -361,15 +361,30 @@ Proof.
- move => ->. by econstructor.
Qed.
Lemma wp_cast_int_ptr Φ v l E it:
Lemma wp_cast_int_ptr_weak Φ v l E it:
val_to_loc_weak v it = Some l
Φ (val_of_loc l) - WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
( i, Φ (val_of_loc (i, l.2))) -
WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv) "HΦ".
iApply wp_unop_det. iSplit => //.
iIntros (σ ?) "_ !%". split.
- by inversion 1; simplify_eq.
- move => ->. by econstructor.
iApply wp_unop.
iIntros (σ) "Hctx". iSplit; [iPureIntro; eexists _; by econstructor |].
iIntros "!>" (v' Hv'). iFrame.
inversion Hv'; simplify_eq. destruct l; simplify_eq/=; case_bool_decide; [ iApply "HΦ"|].
case_bool_decide; simplify_eq; iApply "HΦ".
Qed.
Lemma wp_cast_int_ptr_alive Φ v l E it:
val_to_loc_weak v it = Some l
alloc_alive_loc l Φ (val_of_loc l) -
WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv) "HΦ".
iApply wp_unop_det. iSplit; [iDestruct "HΦ" as "[HΦ _]" | iDestruct "HΦ" as "[_ $]"].
iIntros (σ ?) "Hctx". iDestruct (alloc_alive_loc_to_block_alive with "HΦ Hctx") as %?.
iPureIntro. split.
- by inversion 1; simplify_eq; case_bool_decide.
- move => ->. econstructor; [done..|]. by case_bool_decide.
Qed.
Lemma wp_copy_alloc_id Φ it a l v1 v2 E:
......
......@@ -823,3 +823,11 @@ Proof.
apply: Z.mod_pos_bound.
by apply: Z.pow_pos_nonneg.
Qed.
Definition exists_dec_unique {A} (x : A) (P : _ Prop) : ( y, P y P x) Decision (P x) Decision ( y, P y).
Proof.
intros Hx Hdec.
refine (cast_if (decide (P x))).
- abstract by eexists _.
- abstract naive_solver.
Defined.
......@@ -120,11 +120,12 @@ Section programs.
λ T, i2p (type_cast_ptr_intptr_val v p it n T).
Lemma type_cast_intptr_ptr p v it T:
(T (val_of_loc p) (t2mt (p @ frac_ptr Own (place p)))) -
((alloc_alive_loc p True) T (val_of_loc p) (t2mt (p @ frac_ptr Own (place p)))) -
typed_un_op v (v ◁ᵥ p @ intptr it) (CastOp PtrOp) (IntOp it) T.
Proof.
iIntros "HT" (Hn Φ) "HΦ".
iApply wp_cast_int_ptr => //.
iApply wp_cast_int_ptr_alive => //.
iSplit; [by iDestruct "HT" as "[[$ _] _]"| iDestruct "HT" as "[_ HT]"].
iApply ("HΦ" with "[]"); last iApply "HT". done.
Qed.
Global Instance type_cast_intptr_ptr_inst p v it:
......
......@@ -207,10 +207,10 @@ Section own.
move: (Hn). rewrite /val_to_Z_weak. move => /fmap_Some [i][Hi ->].
iDestruct ("HT" with "[]") as "HT".
{ iPureIntro. by eapply val_to_int_repr_in_range. }
iApply wp_cast_int_ptr => //. { by rewrite /val_to_loc_weak Hi. }
rewrite /int_repr_to_loc /int_repr_to_Z. destruct i as [z|[id p]]=> /=.
- iApply ("HΦ" with "[]"); last by iApply ("HT" $! (ProvAlloc None)). done.
- iApply ("HΦ" with "[]"); last by iApply ("HT" $! id). done.
iApply wp_cast_int_ptr_weak => //. { by rewrite /val_to_loc_weak Hi. }
iIntros (i') "!>". rewrite /int_repr_to_loc /int_repr_to_Z. destruct i as [z|[id p]]=> /=.
- iApply ("HΦ" with "[]"); last by iApply ("HT"). done.
- iApply ("HΦ" with "[]"); last by iApply ("HT"). done.
Qed.
Global Instance type_cast_int_ptr_inst n v it:
TypedUnOp v (v ◁ᵥ n @ int it)%I (CastOp PtrOp) (IntOp it) :=
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment