...
 
Commits (4)
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris" { (= "dev.2019-06-26.1.4832f461") | (= "dev") }
"coq-iris" { (= "dev.2019-06-28.2.5b3f7de1") | (= "dev") }
]
......@@ -62,7 +62,7 @@ Tactic Notation "cwp_pure" open_constr(efoc) :=
eapply (tac_cwp_pure _ _ _ _ _ (fill K e'));
[tac_bind_helper (* e = fill K e' *)
|apply _ (* PureExec *)
|try fast_done (* The pure condition for PureExec *)
|try solve_vals_compare_safe (* The pure condition for PureExec *)
|apply _ (* IntoLaters *)
|simpl
])
......
......@@ -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.
......
......@@ -323,9 +323,6 @@ Section properties.
Qed.
Global Instance cloc_to_val_inj : Inj (=) (=) cloc_to_val.
Proof. intros cl1 cl2 Hcl. apply (inj Some). by rewrite -!cloc_of_to_val Hcl. Qed.
Lemma cloc_to_val_for_compare cl :
val_for_compare (cloc_to_val cl) = cloc_to_val cl.
Proof. rewrite /cloc_to_val. unlock. done. Qed.
Lemma to_locking_heap_insert σ cl lv v :
to_locking_heap (<[cl:=(lv,v)]> σ) = <[cl:=(1%Qp, lv, to_agree v)]>(to_locking_heap σ).
......
......@@ -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 :
......
......@@ -396,7 +396,7 @@ Definition dbase_lit_eq (dl1 dl2 : dbase_lit) : dbool :=
| dLitInt _, (dLitUnit | dLitBool _)
| dLitBool _, (dLitInt _ | dLitUnit)
| dLitUnit, (dLitInt _ | dLitBool _) => dBoolKnown false (* different known constructors *)
| _, _ => dBoolUnknown (bool_decide (lit_for_compare (dbase_lit_interp dl1) = lit_for_compare (dbase_lit_interp dl2)))
| _, _ => dBoolUnknown (bool_decide (dbase_lit_interp dl1 = dbase_lit_interp dl2))
end.
Arguments dbase_lit_eq !_ !_ / : simpl nomatch.
......@@ -410,12 +410,30 @@ Fixpoint dval_eq (E : known_locs) (dv1 dv2 : dval) : dbool :=
| dNone, (dLitV _ | dPairV _ _ | dLocV _)
| dPairV _ _, (dNone | dLitV _ | dLocV _)
| dLocV _, (dNone | dLitV _ | dPairV _ _) => dBoolKnown false (* different known constructors *)
| _, _ => dBoolUnknown (bool_decide (val_for_compare (dval_interp E dv1) = val_for_compare (dval_interp E dv2)))
| _, _ => dBoolUnknown (bool_decide (dval_interp E dv1 = dval_interp E dv2))
end.
Arguments dval_eq _ !_ !_ / : simpl nomatch.
Definition dbase_lit_unboxed (dl : dbase_lit) : bool :=
match dl with
| dLitUnknown l => bool_decide (lit_is_unboxed l)
| _ => true
end.
Definition dval_unboxed (dv : dval) : bool :=
match dv with
| dLitV dl => dbase_lit_unboxed dl
| dValUnknown v => bool_decide (val_is_unboxed v)
| _ => false
end.
Definition dbin_op_eval (E : known_locs) (op : bin_op) (dv1 dv2 : dval) : option dval :=
if decide (op = EqOp) then Some $ dLitV $ dLitBool $ dval_eq E dv1 dv2 else
if decide (op = EqOp) then
if dval_unboxed dv1 || dval_unboxed dv2 then
Some $ dLitV $ dLitBool $ dval_eq E dv1 dv2
else
None
else
match dv1, dv2 with
| dLitV (dLitInt di1), dLitV (dLitInt di2) => dLitV <$> dbin_op_eval_int op di1 di2
| dLitV (dLitBool db1), dLitV (dLitBool db2) => dLitV <$> dbin_op_eval_bool op db1 db2
......@@ -568,6 +586,32 @@ Proof.
rewrite H. apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)].
Qed.
Lemma dbase_lit_unboxed_correct dl :
dbase_lit_unboxed dl = true
lit_is_unboxed (dbase_lit_interp dl).
Proof.
destruct dl; intros; simplify_eq/=; [done..|].
eapply bool_decide_true_2. done.
Qed.
Lemma dval_unboxed_correct E dv :
dval_unboxed dv = true
val_is_unboxed (dval_interp E dv).
Proof.
destruct dv; intros; simplify_eq/=.
- exact: dbase_lit_unboxed_correct.
- exact: bool_decide_true_2.
Qed.
Lemma dvals_compare_safe_correct E dv1 dv2 :
dval_unboxed dv1 || dval_unboxed dv2 = true
vals_compare_safe (dval_interp E dv1) (dval_interp E dv2).
Proof.
destruct (dval_unboxed dv1) eqn:Hdv1.
- intros _. left. exact: dval_unboxed_correct.
- simpl. intros Hdv2. right. exact: dval_unboxed_correct.
Qed.
Lemma dbin_op_eval_int_correct op di1 di2 dl :
dbin_op_eval_int op di1 di2 = Some dl
bin_op_eval_int op (dint_interp di1) (dint_interp di2) = Some (dbase_lit_interp dl).
......@@ -588,7 +632,7 @@ Qed.
Lemma dbase_lit_eq_correct dl1 dl2 :
dbool_interp (dbase_lit_eq dl1 dl2) =
bool_decide (lit_for_compare (dbase_lit_interp dl1) = lit_for_compare (dbase_lit_interp dl2)).
bool_decide (dbase_lit_interp dl1 = dbase_lit_interp dl2).
Proof.
destruct dl1, dl2=> //=.
- rewrite dint_eq_correct. apply bool_decide_iff. naive_solver congruence.
......@@ -597,13 +641,13 @@ Qed.
Lemma dval_eq_correct E dv1 dv2 :
dbool_interp (dval_eq E dv1 dv2) =
bool_decide (val_for_compare (dval_interp E dv1) = val_for_compare (dval_interp E dv2)).
bool_decide (dval_interp E dv1 = dval_interp E dv2).
Proof.
revert dv1. induction dv2; intros []=> //=; try by rewrite cloc_to_val_eq.
- rewrite dbase_lit_eq_correct. apply bool_decide_iff. naive_solver congruence.
- rewrite dbool_and_correct. rewrite IHdv2_1 IHdv2_2.
repeat case_bool_decide; intuition congruence.
- rewrite dloc_eq_correct !cloc_to_val_for_compare.
- rewrite dloc_eq_correct.
apply bool_decide_iff; split; [by intros ->|by intros ?%(inj _)].
Qed.
......@@ -611,8 +655,11 @@ Lemma dbin_op_eval_correct E op dv1 dv2 dw :
dbin_op_eval E op dv1 dv2 = Some dw
bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some (dval_interp E dw).
Proof.
rewrite /bin_op_eval /dbin_op_eval=> ?. destruct (decide (op = _)); simplify_eq/=.
{ by rewrite dval_eq_correct. }
rewrite /bin_op_eval /dbin_op_eval=> ?. destruct (decide (op = _)). simplify_eq/=.
{ destruct (dval_unboxed dv1 || dval_unboxed dv2) eqn:Hdv; last done.
rewrite bool_decide_true; last exact: dvals_compare_safe_correct.
simplify_eq/=. by rewrite dval_eq_correct.
}
destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq.
- by erewrite dbin_op_eval_int_correct by done.
- by erewrite dbin_op_eval_bool_correct by done.
......@@ -677,7 +724,9 @@ Lemma dbin_op_eval_Some_wf E dv1 dv2 op dw:
dval_wf E dv1 dval_wf E dv2 dval_wf E dw.
Proof.
rewrite /dbin_op_eval; intros; simplify_option_eq; auto.
destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq; auto.
- destruct (dval_unboxed dv1 || dval_unboxed dv2) eqn:Hdv; last done.
simplify_eq/=. done.
- destruct dv1 as [[]| | | |], dv2 as [[]| | | |]; simplify_option_eq; auto.
Qed.
Lemma dcbin_op_eval_Some_wf E dv1 dv2 op dw:
......