Commit b09eb8c0 authored by Robbert Krebbers's avatar Robbert Krebbers

Use custom comparison function instead of heap-lang's `=` in membership functions.

parent 8caf5c0d
Pipeline #18067 failed with stage
in 9 minutes and 54 seconds
......@@ -7,6 +7,10 @@ From iris_c.lib Require Import mset flock list.
Notation "♯ l" := (c_ret (LitV l%Z%V)) (at level 8, format "♯ l").
Notation "♯ₗ l" := (c_ret (cloc_to_val l)) (at level 8, format "♯ₗ l") : expr_scope.
Definition loc_nonnull_cmp : val := λ: "l1" "l2",
(Fst "l1" = Fst "l2") && (Snd "l1" = Snd "l2").
Definition is_loc_nonnull (v : val) := is_Some (cloc_of_val (SOMEV v)).
Definition c_alloc : val := λ: "x1" "x2",
"vv" ←ᶜ "x1" ||| "x2" ;;
let: "n" := Fst "vv" in
......@@ -20,7 +24,7 @@ Definition c_free_check : val :=
rec: "go" "env" "l" "n" :=
if: "n" = #0 then #() else
let: "n" := "n" - #1 in
assert: (mset_member ("l", "n") "env" = #false);;
assert: (mset_member loc_nonnull_cmp ("l", "n") "env" = #false);;
"go" "env" "l" "n".
Definition c_free : val := λ: "x",
......@@ -59,7 +63,7 @@ Definition c_store : val := λ: "x1" "x2",
let: "l" := Fst "li" in
let: "i" := Snd "li" in
let: "v" := Snd "vv" in
mset_add ("l", "i") "env" ;;
mset_add loc_nonnull_cmp ("l", "i") "env" ;;
match: !"l" with
NONE => assert: #false (* store after free *)
| SOME "kll" => "l" <- SOME (Fst "kll", linsert "i" "v" (Snd "kll")) ;; "v"
......@@ -76,7 +80,7 @@ Definition c_load : val := λ: "x",
| SOME "li" =>
let: "l" := Fst "li" in
let: "i" := Snd "li" in
assert: (mset_member ("l", "i") "env" = #false);;
assert: (mset_member loc_nonnull_cmp ("l", "i") "env" = #false);;
match: !"l" with
NONE => assert: #false (* load after free *)
| SOME "kll" => llookup "i" (Snd "kll")
......@@ -235,6 +239,14 @@ Notation "e1 +∗=ᶜ e2" := (c_pre_bin_op PtrPlusOp e1%E e2%E) (at level 80) :
Section proofs.
Context `{cmonadG Σ}.
Global Instance loc_nonnull_cmp_spec : CmpSpec is_loc_nonnull loc_nonnull_cmp.
Proof.
iIntros (v1 v2 Ψ [[cl1 Hcl1%cloc_to_of_val] [cl2 Hcl2%cloc_to_of_val]]) "HΨ".
move: Hcl1 Hcl2. rewrite /cloc_to_val -!lock=> -[<-] [<-]. wp_lam; wp_pures.
iSpecialize ("HΨ" with "[//]").
repeat (case_bool_decide; wp_pures); simplify_eq/=; auto with congruence.
Qed.
Lemma cwp_alloc R Φ Ψ1 Ψ2 e1 e2 :
CWP e1 @ R {{ Ψ1 }} -
CWP e2 @ R {{ Ψ2 }} -
......@@ -297,7 +309,9 @@ Section proofs.
{ wp_lam; wp_pures. by iApply "HΨ". }
wp_lam; wp_pures. wp_apply wp_assert.
rewrite Nat2Z.inj_succ Z.sub_1_r Z.pred_succ.
wp_apply (mset_member_spec with "Hlocks"); first done.
wp_apply (mset_member_spec with "Hlocks").
{ intros v Hv. rewrite /is_loc_nonnull. destruct (HX v Hv) as (cl'&->&?); eauto. }
{ rewrite /is_loc_nonnull /=; eauto. }
iIntros "Hlocks"; case_bool_decide.
{ destruct (HX (#(cloc_base cl), #n)%V) as (cl'&[= <-]&?); first done.
destruct (Hlocked n); first by (apply lookup_lt_is_Some_2; lia).
......@@ -337,7 +351,10 @@ Section proofs.
{ intros Hcl. destruct (HX _ Hcl) as (cl'&[=]%cloc_to_of_val&?). naive_solver. }
iMod (full_locking_heap_store_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]".
wp_pures. rewrite cloc_to_val_eq. wp_pures.
wp_apply (mset_add_spec with "[$]"); [done..|].
wp_apply (mset_add_spec with "[$]").
{ intros v Hv. rewrite /is_loc_nonnull. destruct (HX v Hv) as (cl'&->&?); eauto. }
{ rewrite /is_loc_nonnull /=; eauto. }
{ done. }
iIntros "Hlocks /="; wp_pures.
wp_load; wp_pures.
iEval (rewrite -(Z2Nat.id (cloc_offset cl)) //).
......@@ -368,7 +385,9 @@ Section proofs.
{ intros Hcl. destruct (HX _ Hcl) as (?&[=]%cloc_to_of_val&?); naive_solver. }
iMod (full_locking_heap_load_upd with "Hσ Hl") as (k ll vs Hl Hi) "[Hl Hclose]".
wp_pures. rewrite cloc_to_val_eq. wp_pures.
wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks"); [done..|].
wp_apply wp_assert. wp_apply (mset_member_spec with "Hlocks").
{ intros v Hv'. rewrite /is_loc_nonnull. destruct (HX v Hv') as (cl'&->&?); eauto. }
{ rewrite /is_loc_nonnull /=; eauto. }
iIntros "Hlocks /=".
rewrite bool_decide_false //.
wp_op. iSplit; first done. iNext; wp_seq.
......
......@@ -39,13 +39,17 @@ Definition lreplicate : val :=
if: "n" = #0 then lnil #() else
let: "l" := "go" ("n" - #1) "x" in lcons "x" "l".
Class CmpSpec `{heapG Σ} (R : val Prop) (cmp : val) :=
cmp_spec w1 w2 :
{{{ R w1 R w2 }}} cmp w1 w2 {{{ RET #(bool_decide (w1 = w2)); True }}}.
Definition llist_member : val :=
rec: "go" "x" "l" :=
rec: "go" "cmp" "x" "l" :=
match: "l" with
NONE => #false
| SOME "p" =>
if: Fst "p" = "x" then #true
else let: "l" := (Snd "p") in "go" "x" "l"
if: "cmp" (Fst "p") "x" then #true
else let: "l" := (Snd "p") in "go" "cmp" "x" "l"
end.
Definition llength : val :=
......@@ -106,19 +110,21 @@ Proof.
by wp_apply (lcons_spec with "[//]").
Qed.
Lemma llist_member_spec hd vs v :
Lemma llist_member_spec `{!CmpSpec R cmp} hd vs v :
Forall R vs R v
{{{ is_list hd vs }}}
llist_member v hd
{{{ RET #(bool_decide (val_for_compare v (val_for_compare <$> vs))); True }}}.
llist_member cmp v hd
{{{ RET #(bool_decide (v vs)); True }}}.
Proof.
iIntros (Φ Hl) "HΦ".
iInduction vs as [|v' vs] "IH" forall (hd Hl); simplify_eq/=.
iIntros (Hvs Hv Φ Hl) "HΦ".
iInduction Hvs as [|v' vs] "IH" forall (hd Hl); simplify_eq/=.
{ wp_lam; wp_pures. by iApply "HΦ". }
destruct Hl as (hd'&->&?). wp_lam; wp_pures.
destruct (bool_decide_reflect (val_for_compare v' = val_for_compare v)) as [->|?]; wp_if.
wp_apply (cmp_spec with "[]"); [auto|]; iIntros (_).
iEval (rewrite bool_decide_decide). destruct (decide _) as [->|?]; wp_if.
{ rewrite (bool_decide_true (_ _ :: _)); last by left. by iApply "HΦ". }
wp_proj. wp_let. iApply ("IH" with "[//]").
destruct (bool_decide_reflect (val_for_compare v (val_for_compare <$> vs))).
destruct (bool_decide_reflect (v vs)).
- by rewrite bool_decide_true; last by right.
- by rewrite bool_decide_false ?elem_of_cons; last naive_solver.
Qed.
......
......@@ -4,30 +4,22 @@ From iris_c.lib Require Import list.
Definition is_mset `{heapG Σ} (v : val) (X : gset val) : iProp Σ :=
( (l : loc) hd vs,
v = #l X = list_to_set (val_for_compare <$> vs) is_list hd vs NoDup vs l hd)%I.
v = #l X = list_to_set vs is_list hd vs NoDup vs l hd)%I.
Definition mset_create : val := λ: <>, ref (lnil #()).
Definition mset_member : val := λ: "x" "xs",
Definition mset_member : val := λ: "cmp" "x" "xs",
let: "l" := !"xs" in
llist_member "x" "l".
llist_member "cmp" "x" "l".
Definition mset_add : val := λ: "x" "xs",
Definition mset_add : val := λ: "cmp" "x" "xs",
let: "l" := !"xs" in
assert: (llist_member "x" "l" = #false);;
assert: (llist_member "cmp" "x" "l" = #false);;
"xs" <- lcons "x" "l".
Definition mset_clear : val := λ: "xs",
"xs" <- lnil #().
Lemma val_for_compare_in_set v vs :
val_for_compare v list_to_set (C:=gset val) (val_for_compare <$> vs)
v vs.
Proof.
intros Hnin Hin. apply Hnin. rewrite elem_of_list_to_set.
eapply elem_of_list_fmap. eauto.
Qed.
Section mset.
Context `{heapG Σ}.
Implicit Types x v : val.
......@@ -40,37 +32,35 @@ Section mset.
iExists l, _, []. iFrame "Hl". by rewrite /= NoDup_nil.
Qed.
Lemma mset_member_spec x e v X :
IntoVal e v
val_for_compare v = v
Lemma mset_member_spec `{!CmpSpec R cmp} x v X :
set_Forall R X R v
{{{ is_mset x X }}}
mset_member e x
mset_member cmp v x
{{{ RET #(bool_decide (v X)); is_mset x X }}}.
Proof.
iIntros (<- Hvc Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
iIntros (HX Hv Φ) "Hmut HΦ".
iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl". apply set_Forall_list_to_set in HX.
wp_lam; wp_pures. wp_load. wp_let.
wp_apply (llist_member_spec with "[//]"). iIntros "_".
rewrite (bool_decide_iff _ (v val_for_compare <$> vs)); last set_solver.
rewrite Hvc. iApply "HΦ". iExists l, hd, vs; auto.
wp_apply (llist_member_spec with "[//]"); iIntros "// _".
rewrite (bool_decide_iff _ (v vs)); last set_solver.
iApply "HΦ". iExists l, hd, vs; auto.
Qed.
Lemma mset_add_spec x e v X :
IntoVal e v
val_for_compare v = v
Lemma mset_add_spec `{!CmpSpec R cmp} x v X :
set_Forall R X R v
v X
{{{ is_mset x X }}}
mset_add e x
mset_add cmp v x
{{{ RET #(); is_mset x ({[v]} X) }}}.
Proof.
iIntros (<- Hvc ? Φ) "Hmut HΦ". iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl".
iIntros (HX Hv ? Φ) "Hmut HΦ".
iDestruct "Hmut" as (l hd vs (->&->&?&?)) "Hl". apply set_Forall_list_to_set in HX.
wp_lam. wp_pures. wp_load. wp_let. wp_apply wp_assert.
wp_apply (llist_member_spec with "[//]"); iIntros "_".
rewrite Hvc bool_decide_false /=; last set_solver. wp_op; iSplit=> //; iIntros "!>".
wp_apply (llist_member_spec with "[//]"); iIntros "// _".
rewrite bool_decide_false /=; last set_solver. wp_op; iSplit=> //; iIntros "!>".
wp_seq. wp_apply (lcons_spec with "[//]"); iIntros (hd' ?). wp_store.
iApply "HΦ". iExists l, hd', (v :: vs). iFrame "Hl".
rewrite NoDup_cons fmap_cons Hvc. assert (v vs).
{ eapply val_for_compare_in_set. rewrite Hvc. done. }
iPureIntro; set_solver.
rewrite NoDup_cons. iPureIntro; set_solver.
Qed.
Lemma mset_clear_spec x X :
......
Markdown is supported
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