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

check range on int to ptr cast

parent 36366a67
Pipeline #49216 passed with stage
in 18 minutes and 22 seconds
...@@ -231,21 +231,6 @@ Definition alloc_id_alive (aid : alloc_id) (st : heap_state) : Prop := ...@@ -231,21 +231,6 @@ Definition alloc_id_alive (aid : alloc_id) (st : heap_state) : Prop :=
Definition block_alive (l : loc) (st : heap_state) : Prop := Definition block_alive (l : loc) (st : heap_state) : Prop :=
aid, l.1 = ProvAlloc (Some aid) alloc_id_alive aid st. 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 (** 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 allocation that contains [l]. Note that we consider the 1-past-the-end
pointer to be in range of an allocation. *) pointer to be in range of an allocation. *)
...@@ -264,6 +249,33 @@ Definition valid_ptr (l : loc) (st : heap_state) : Prop := ...@@ -264,6 +249,33 @@ Definition valid_ptr (l : loc) (st : heap_state) : Prop :=
Definition addr_in_range_alloc (a : addr) (aid : alloc_id) (st : heap_state) : Prop := Definition addr_in_range_alloc (a : addr) (aid : alloc_id) (st : heap_state) : Prop :=
alloc, st.(hs_allocs) !! aid = Some alloc a alloc. alloc, st.(hs_allocs) !! aid = Some alloc a alloc.
Global Instance allocation_eq_dec : EqDecision (allocation).
Proof. solve_decision. Qed.
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.
Global Instance heap_state_loc_in_bounds_dec l n st : Decision (heap_state_loc_in_bounds l n st).
Proof.
destruct (l.1) as [| [aid|] |] eqn: Hl.
1,3,4: (right => -[?[??]]; destruct l; naive_solver).
destruct (st.(hs_allocs) !! aid) as [al|] eqn:?.
2: right => -[?[?[??]]]; destruct l; naive_solver.
eapply (exists_dec_unique aid); [ destruct l; naive_solver|].
eapply (exists_dec_unique al); [ destruct l; naive_solver|].
apply _.
Qed.
Inductive alloc_new_block : heap_state loc val heap_state Prop := Inductive alloc_new_block : heap_state loc val heap_state Prop :=
| AllocNewBlock σ l aid v: | AllocNewBlock σ l aid v:
let alloc := Allocation l.2 (length v) true in let alloc := Allocation l.2 (length v) true in
......
...@@ -345,7 +345,7 @@ Inductive eval_un_op : un_op → op_type → state → val → val → Prop := ...@@ -345,7 +345,7 @@ Inductive eval_un_op : un_op → op_type → state → val → val → Prop :=
val_to_loc_weak vs it = Some 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. *) (** This is using that the address 0 is never alive. *)
l' = (if bool_decide (block_alive l σ.(st_heap)) then l else l' = (if bool_decide (valid_ptr l σ.(st_heap)) then l else
(if bool_decide (l.2 = 0) then NULL_loc else (ProvAlloc None, l.2))) (if bool_decide (l.2 = 0) then NULL_loc else (ProvAlloc None, l.2)))
eval_un_op (CastOp PtrOp) (IntOp it) σ vs vt eval_un_op (CastOp PtrOp) (IntOp it) σ vs vt
| NegOpI it σ vs vt n: | NegOpI it σ vs vt n:
......
...@@ -389,12 +389,17 @@ Qed. ...@@ -389,12 +389,17 @@ Qed.
Lemma wp_cast_int_ptr_alive Φ v l E it: Lemma wp_cast_int_ptr_alive Φ v l E it:
val_to_loc_weak v it = Some l val_to_loc_weak v it = Some l
loc_in_bounds l 0 -
alloc_alive_loc l Φ (val_of_loc l) - alloc_alive_loc l Φ (val_of_loc l) -
WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}. WP UnOp (CastOp PtrOp) (IntOp it) (Val v) @ E {{ Φ }}.
Proof. Proof.
iIntros (Hv) "HΦ". iIntros (Hv) "#Hlib HΦ".
iApply wp_unop_det. iSplit; [iDestruct "HΦ" as "[HΦ _]" | iDestruct "HΦ" as "[_ $]"]. 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 %?. iIntros (σ ?) "Hctx".
iAssert valid_ptr l σ.(st_heap)%I as %?. {
iSplit; [ |iApply (loc_in_bounds_to_heap_loc_in_bounds with "Hlib Hctx")].
by iApply (alloc_alive_loc_to_block_alive with "[HΦ] Hctx").
}
iPureIntro. split. iPureIntro. split.
- by inversion 1; simplify_eq; case_bool_decide. - by inversion 1; simplify_eq; case_bool_decide.
- move => ->. econstructor; [done..|]. by case_bool_decide. - move => ->. econstructor; [done..|]. by case_bool_decide.
......
...@@ -6,11 +6,12 @@ Section intptr. ...@@ -6,11 +6,12 @@ Section intptr.
Context `{!typeG Σ}. Context `{!typeG Σ}.
Program Definition intptr_inner_type (it : int_type) (p : loc) : type := {| Program Definition intptr_inner_type (it : int_type) (p : loc) : type := {|
ty_own β l := v, val_to_loc_weak v it = Some p l `has_layout_loc` it l [β] v; ty_own β l := v, val_to_loc_weak v it = Some p l `has_layout_loc` it
loc_in_bounds p 0 l [β] v;
|}%I. |}%I.
Next Obligation. Next Obligation.
iIntros (it n l ??) "(%v&%Hv&%Hl&H)". iExists v. iIntros (it n l ??) "(%v&%Hv&%Hl&#?&H)". iExists v.
do 2 (iSplitR; first done). by iApply heap_mapsto_own_state_share. do 3 (iSplitR; first done). by iApply heap_mapsto_own_state_share.
Qed. Qed.
Program Definition intptr (it : int_type) : rtype := {| Program Definition intptr (it : int_type) : rtype := {|
...@@ -19,21 +20,21 @@ Section intptr. ...@@ -19,21 +20,21 @@ Section intptr.
|}. |}.
Global Program Instance rmovable_intptr it : RMovable (intptr it) := {| Global Program Instance rmovable_intptr it : RMovable (intptr it) := {|
rmovable l := {| rmovable p := {|
ty_layout := it_layout it; ty_layout := it_layout it;
ty_own_val v := val_to_loc_weak v it = Some l; ty_own_val v := val_to_loc_weak v it = Some p loc_in_bounds p 0;
|} |}
|}%I. |}%I.
Next Obligation. iIntros (???) "(%&%&$&_)". Qed. Next Obligation. iIntros (???) "(%&%&$&_)". Qed.
Next Obligation. iIntros (??? H) "!%". by apply val_to_loc_weak_length in H. Qed. Next Obligation. iIntros (???) "[% ?] !%". by apply val_to_loc_weak_length in H. Qed.
Next Obligation. iIntros (???) "(%v&%&%&Hl)". eauto with iFrame. Qed. Next Obligation. iIntros (???) "(%v&%&%&Hl&?)". eauto with iFrame. Qed.
Next Obligation. iIntros (??? v ?) "Hl %". iExists v. eauto with iFrame. Qed. Next Obligation. iIntros (??? v ?) "Hl [% ?]". iExists v. eauto with iFrame. Qed.
Next Obligation. iIntros (???). done. Qed. Next Obligation. iIntros (???). done. Qed.
Lemma intptr_loc_in_bounds l β p it: Lemma intptr_loc_in_bounds l β p it:
l ◁ₗ{β} p @ intptr it - loc_in_bounds l (bytes_per_int it). l ◁ₗ{β} p @ intptr it - loc_in_bounds l (bytes_per_int it).
Proof. Proof.
iIntros "(%&%Hv&%&Hl)". move: Hv => /val_to_loc_weak_length <-. iIntros "(%&%Hv&%&?&Hl)". move: Hv => /val_to_loc_weak_length <-.
by iApply heap_mapsto_own_state_loc_in_bounds. by iApply heap_mapsto_own_state_loc_in_bounds.
Qed. Qed.
...@@ -47,7 +48,7 @@ Section intptr. ...@@ -47,7 +48,7 @@ Section intptr.
Lemma ty_own_intptr_in_range l β p it : l ◁ₗ{β} p @ intptr it - p.2 it. Lemma ty_own_intptr_in_range l β p it : l ◁ₗ{β} p @ intptr it - p.2 it.
Proof. Proof.
iIntros "Hl". destruct β. iIntros "Hl". destruct β.
- iDestruct (ty_deref with "Hl") as (?) "[_ %]". - iDestruct (ty_deref with "Hl") as (?) "[_ [% ?]]".
iPureIntro. by eapply val_to_loc_weak_in_range. iPureIntro. by eapply val_to_loc_weak_in_range.
- iDestruct "Hl" as (?) "[% _]". - iDestruct "Hl" as (?) "[% _]".
iPureIntro. by eapply val_to_loc_weak_in_range. iPureIntro. by eapply val_to_loc_weak_in_range.
...@@ -57,9 +58,9 @@ Section intptr. ...@@ -57,9 +58,9 @@ Section intptr.
have to reprove this everytime? *) have to reprove this everytime? *)
Global Program Instance intptr_copyable p it : Copyable (p @ intptr it). Global Program Instance intptr_copyable p it : Copyable (p @ intptr it).
Next Obligation. Next Obligation.
iIntros (?????) "(%v&%Hv&%Hl&Hl)". iIntros (?????) "(%v&%Hv&%Hl&#?&Hl)".
iMod (heap_mapsto_own_state_to_mt with "Hl") as (q) "[_ Hl]" => //. iMod (heap_mapsto_own_state_to_mt with "Hl") as (q) "[_ Hl]" => //.
iSplitR => //. iExists q, v. iFrame. iModIntro. eauto with iFrame. iSplitR => //. iExists q, v. iFrame "∗#". iModIntro. eauto with iFrame.
Qed. Qed.
Global Instance intptr_timeless l p it: Global Instance intptr_timeless l p it:
...@@ -92,7 +93,9 @@ Section programs. ...@@ -92,7 +93,9 @@ Section programs.
{ rewrite bool_decide_true; naive_solver. } { rewrite bool_decide_true; naive_solver. }
iSplit; [by iDestruct "HT" as "[[$ _] _]" | iDestruct "HT" as "[_ HT]"]. iSplit; [by iDestruct "HT" as "[[$ _] _]" | iDestruct "HT" as "[_ HT]"].
iApply ("HΦ" with "[] HT"). iApply ("HΦ" with "[] HT").
iPureIntro. by apply val_to_loc_weak_val_of_loc_n. iSplit.
- iPureIntro. by apply val_to_loc_weak_val_of_loc_n.
- iApply loc_in_bounds_shorten; [|done]. lia.
Qed. Qed.
Global Instance type_cast_ptr_intptr_inst (p : loc) β it ty: Global Instance type_cast_ptr_intptr_inst (p : loc) β it ty:
TypedUnOp p (p ◁ₗ{β} ty)%I (CastOp (IntOp it)) PtrOp := TypedUnOp p (p ◁ₗ{β} ty)%I (CastOp (IntOp it)) PtrOp :=
...@@ -113,7 +116,9 @@ Section programs. ...@@ -113,7 +116,9 @@ Section programs.
{ rewrite bool_decide_true; naive_solver. } { rewrite bool_decide_true; naive_solver. }
iSplit; [by iDestruct "HT" as "[[$ _] _]" | iDestruct "HT" as "[_ HT]"]. iSplit; [by iDestruct "HT" as "[[$ _] _]" | iDestruct "HT" as "[_ HT]"].
iApply ("HΦ" with "[] HT"). iApply ("HΦ" with "[] HT").
iPureIntro. by apply val_to_loc_weak_val_of_loc_n. iSplit.
- iPureIntro. by apply val_to_loc_weak_val_of_loc_n.
- iApply loc_in_bounds_shorten; [|done]. lia.
Qed. Qed.
Global Instance type_cast_ptr_intptr_val_inst (v : val) (p : loc) it (n : nat): Global Instance type_cast_ptr_intptr_val_inst (v : val) (p : loc) it (n : nat):
TypedUnOp v (v ◁ᵥ p @ ptr n)%I (CastOp (IntOp it)) PtrOp := TypedUnOp v (v ◁ᵥ p @ ptr n)%I (CastOp (IntOp it)) PtrOp :=
...@@ -123,7 +128,7 @@ Section programs. ...@@ -123,7 +128,7 @@ Section programs.
((alloc_alive_loc p True) 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. typed_un_op v (v ◁ᵥ p @ intptr it) (CastOp PtrOp) (IntOp it) T.
Proof. Proof.
iIntros "HT" (Hn Φ) "HΦ". iIntros "HT [%Hn #Hlib]" (Φ) "HΦ".
iApply wp_cast_int_ptr_alive => //. iApply wp_cast_int_ptr_alive => //.
iSplit; [by iDestruct "HT" as "[[$ _] _]"| iDestruct "HT" as "[_ HT]"]. iSplit; [by iDestruct "HT" as "[[$ _] _]"| iDestruct "HT" as "[_ HT]"].
iApply ("HΦ" with "[]"); last iApply "HT". done. iApply ("HΦ" with "[]"); last iApply "HT". done.
...@@ -135,7 +140,7 @@ Section programs. ...@@ -135,7 +140,7 @@ Section programs.
Lemma intptr_wand_int v p it: Lemma intptr_wand_int v p it:
v ◁ᵥ p @ intptr it - v ◁ᵥ p.2 @ int it. v ◁ᵥ p @ intptr it - v ◁ᵥ p.2 @ int it.
Proof. Proof.
iPureIntro. rewrite /val_to_loc_weak /val_to_Z_weak. iIntros "[%Hn _]". iPureIntro. move: Hn. rewrite /val_to_loc_weak /val_to_Z_weak.
move => /fmap_Some [i][-> ->]. by destruct i. move => /fmap_Some [i][-> ->]. by destruct i.
Qed. Qed.
...@@ -153,7 +158,7 @@ Section programs. ...@@ -153,7 +158,7 @@ Section programs.
n = p.2 T - n = p.2 T -
subsume (l ◁ₗ{β} p @ intptr it) (l ◁ₗ{β} n @ int it) T. subsume (l ◁ₗ{β} p @ intptr it) (l ◁ₗ{β} n @ int it) T.
Proof. Proof.
iIntros "[-> $]". rewrite /ty_own /=. iIntros "(%v&H&?&?)". iIntros "[-> $]". rewrite /ty_own /=. iIntros "(%v&H&?&?&?)".
iExists v. iFrame. iRevert "H". iPureIntro. iExists v. iFrame. iRevert "H". iPureIntro.
rewrite /val_to_loc_weak /val_to_Z_weak. rewrite /val_to_loc_weak /val_to_Z_weak.
move => /fmap_Some [i][-> ->] /=. by destruct i. move => /fmap_Some [i][-> ->] /=. by destruct i.
......
...@@ -120,7 +120,9 @@ Section tagged_ptr. ...@@ -120,7 +120,9 @@ Section tagged_ptr.
iSplit. iSplit.
{ iDestruct "HT" as "[[HT _] _]". by iApply (alloc_alive_loc_mono with "HT"). } { iDestruct "HT" as "[[HT _] _]". by iApply (alloc_alive_loc_mono with "HT"). }
iDestruct "HT" as "[_ HT]". iApply ("HΦ" with "[] HT"). iDestruct "HT" as "[_ HT]". iApply ("HΦ" with "[] HT").
iPureIntro. by apply val_to_loc_weak_val_of_loc_n. iSplit.
- iPureIntro. by apply val_to_loc_weak_val_of_loc_n.
- iApply (loc_in_bounds_offset with "Hlib") => /=; [done | |]; unfold addr in *; lia.
Qed. Qed.
Global Instance type_cast_tagged_ptr_intptr_val_inst (v : val) (r : loc * Z) β (align : nat) it ty: Global Instance type_cast_tagged_ptr_intptr_val_inst (v : val) (r : loc * Z) β (align : nat) it ty:
TypedUnOp v (v ◁ᵥ r @ tagged_ptr β align ty)%I (CastOp (IntOp it)) PtrOp := TypedUnOp v (v ◁ᵥ r @ tagged_ptr β align ty)%I (CastOp (IntOp it)) PtrOp :=
......
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