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

add initial support for comparison operators between pointers

parent 82368c75
Pipeline #41915 passed with stage
in 14 minutes and 25 seconds
......@@ -651,3 +651,18 @@ Inductive TCFalse : Prop :=.
Existing Class TCFalse.
Notation TCUnless P := (TCIf P TCFalse TCTrue).
Inductive TCExists {A} (P : A Prop) : list A Prop :=
| TCExists_cons_hd x l : P x TCExists P (x :: l)
| TCExists_cons_tl x l: TCExists P l TCExists P (x :: l).
Existing Class TCExists.
Existing Instance TCExists_cons_hd | 10.
Existing Instance TCExists_cons_tl | 20.
Global Hint Mode TCExists ! ! ! : typeclass_instances.
Lemma TCExists_Exists {A} (P : A Prop) l :
TCExists P l Exists P l.
Proof.
elim: l. { split; inversion 1. }
move => ?? IH. split; inversion 1; simplify_eq; constructor => //; by apply IH.
Qed.
......@@ -61,7 +61,7 @@ Section definitions.
Definition loc_in_bounds_def (l : loc) (n : nat) : iProp Σ :=
id a, l.1 = Some id alloc_start a l.2
l.2 + n alloc_end a in_range_allocation a
l.2 + n alloc_end a allocation_in_range a
allocs_entry id a.
Definition loc_in_bounds_aux : seal (@loc_in_bounds_def). by eexists. Qed.
Definition loc_in_bounds := unseal loc_in_bounds_aux.
......@@ -86,6 +86,15 @@ Section definitions.
Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
seal_eq heap_mapsto_aux.
Definition alloc_alive_def (aid : option alloc_id) : iProp Σ :=
(* TODO: This should probably be defined using some custom ghost
state, e.g. based on a new killed flag in allocations? *)
a q v, length v 0%nat heap_mapsto (aid, a) q v.
Definition alloc_alive_aux : seal (@alloc_alive_def). by eexists. Qed.
Definition alloc_alive := unseal alloc_alive_aux.
Definition alloc_alive_eq : @alloc_alive = @alloc_alive_def :=
seal_eq alloc_alive_aux.
Definition fntbl_entry_def (l : loc) (f: function) : iProp Σ :=
own heap_fntbl_name ( {[ l := to_agree f ]}).
Definition fntbl_entry_aux : seal (@fntbl_entry_def). by eexists. Qed.
......@@ -214,7 +223,7 @@ Section allocs.
Lemma allocs_entry_to_loc_in_bounds l aid (n : nat) a:
l.1 = Some aid
alloc_start a l.2 l.2 + n alloc_end a
in_range_allocation a
allocation_in_range a
allocs_entry aid a - loc_in_bounds l n.
Proof.
iIntros (?[??]?) "?". rewrite loc_in_bounds_eq/loc_in_bounds_def.
......@@ -644,6 +653,38 @@ Section heap.
Qed.
End heap.
Section alloc_alive.
Context `{!heapG Σ}.
Global Instance alloc_alive_timeless a : Timeless (alloc_alive a).
Proof. rewrite alloc_alive_eq. by apply _. Qed.
Lemma heap_mapsto_alive l q v:
length v 0%nat
l {q} v - alloc_alive l.1.
Proof. rewrite alloc_alive_eq => ?. iIntros "Hl". destruct l. iExists _, _, _. by iFrame. Qed.
Lemma alloc_alive_to_heap_alloc_alive a σ:
alloc_alive a - state_ctx σ - aid, a = Some aid heap_block_alive σ.(st_heap) aid.
Proof.
rewrite alloc_alive_eq.
iDestruct 1 as (addr q [|b v] Hv) "Hl" => //. iIntros "(_&Hhctx&_)".
rewrite heap_mapsto_cons_mbyte heap_mapsto_mbyte_eq. iDestruct "Hl" as "[Hmt _]".
iDestruct "Hmt" as (aid ?) "Hmt".
iDestruct (heap_mapsto_mbyte_lookup_q with "Hhctx Hmt") as %[??].
iPureIntro. eexists _. split => //. by eexists _, _, _.
Qed.
Lemma alloc_alive_to_valid_ptr l σ:
loc_in_bounds l 0 - alloc_alive l.1 - state_ctx σ - valid_ptr l σ⌝.
Proof.
iIntros "Hin Ha Hσ".
iDestruct (alloc_alive_to_heap_alloc_alive with "Ha Hσ") as %[?[??]].
iDestruct (loc_in_bounds_to_heap_loc_in_bounds with "Hin Hσ") as %?.
iPureIntro. by eexists _.
Qed.
End alloc_alive.
Section alloc_new_blocks.
Context `{!heapG Σ}.
......
......@@ -708,8 +708,8 @@ Fixpoint heap_at_go l v flk h : Prop :=
Definition heap_at l ly v flk h : Prop :=
is_Some l.1 l `has_layout_loc` ly v `has_layout_val` ly heap_at_go l v flk h.
Definition heap_block_free (h : heap) (aid : alloc_id) : Prop :=
a ha, h !! a = Some ha ha.1.1 aid.
Definition heap_block_alive (h : heap) (aid : alloc_id) : Prop :=
a lk b, h !! a = Some (aid, lk, b).
Definition heap_range_free (h : heap) (a : addr) (n : nat) : Prop :=
a', a a' < a + n h !! a' = None.
......@@ -755,15 +755,17 @@ Definition max_alloc_end : Z := 2 ^ (bytes_per_addr * bits_per_byte) - 2.
Definition to_allocation (off : Z) (len : nat) : allocation :=
Allocation off (off + len).
Definition in_range_allocation (a : allocation) : Prop :=
Definition allocation_in_range (a : allocation) : Prop :=
min_alloc_start a.(alloc_start) a.(alloc_end) max_alloc_end.
Inductive alloc_new_block : state loc val state Prop :=
| AllocNewBlock σ l aid v:
l.1 = Some aid
σ.(st_allocs) !! aid = None
heap_block_free σ.(st_heap) aid
in_range_allocation (to_allocation l.2 (length v))
(* TODO: is the precondition really useful? It should follow from
the previous. *)
¬ heap_block_alive σ.(st_heap) aid
allocation_in_range (to_allocation l.2 (length v))
heap_range_free σ.(st_heap) l.2 (length v)
alloc_new_block σ l v {|
st_heap := heap_upd l v (λ _, RSt 0%nat) σ.(st_heap);
......@@ -819,34 +821,10 @@ Definition subst_function (xs : list (var_name * val)) (f : function) : function
|}.
(*** Evaluation of operations *)
(** Checks that the location [l] is allocated on the heap [h] *)
Definition valid_ptr l h : Prop :=
aid lk b, l.1 = Some aid h !! l.2 = Some (aid, lk, b).
Instance valid_ptr_dec l h : Decision (valid_ptr l h).
Proof.
rewrite /valid_ptr/=. destruct l as [[aid|] a]; [ | right; naive_solver].
destruct (h !! a) as [[[aid' ?]?]|] eqn: Hh; [ | right; naive_solver].
destruct (decide (aid' = aid)); [left | right]; naive_solver.
Qed.
(** Checks whether location [l] is a weak valid pointer in heap [h].
[Some true] means [l] is a valid in bounds pointer, [Some false] means
[l] is a end of block pointer, [None] means [l] is not a valid pointer. *)
Definition weak_valid_ptr l h : option bool :=
if decide (valid_ptr l h) then
Some true
else if decide (valid_ptr (l + -1) h ¬valid_ptr l h) then
Some false
else None.
(** Checks equality between [l1] and [l2]. See
http://compcert.inria.fr/doc/html/compcert.common.Values.html#Val.cmplu_bool
*)
Definition ptr_eq l1 l2 h : option bool :=
eob1 weak_valid_ptr l1 h;
eob2 weak_valid_ptr l2 h;
if decide (l1.1 = l2.1) then
Some (bool_decide (l1 = l2))
else
if eob1 || eob2 then None else Some false.
(** 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 : state) : Prop :=
aid, l.1 = Some aid heap_block_alive st.(st_heap) aid heap_loc_in_bounds l 0 st.
(* evaluation can be non-deterministic for comparing pointers *)
Inductive eval_bin_op : bin_op op_type op_type state val val val Prop :=
......@@ -884,18 +862,21 @@ Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val
val_to_int v2 size_t = Some 0
i2v (Z_of_bool false) i32 = v
eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| EqOpPP v1 v2 σ l1 l2 v b:
| RelOpPP v1 v2 σ l1 l2 v b op:
val_to_loc v1 = Some l1
val_to_loc v2 = Some l2
ptr_eq l1 l2 σ.(st_heap) = Some b
valid_ptr l1 σ valid_ptr l2 σ
match op with
| EqOp => Some (bool_decide (l1.2 = l2.2))
| NeOp => Some (bool_decide (l1.2 l2.2))
| LtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 < l2.2)) else None
| GtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 > l2.2)) else None
| LeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 <= l2.2)) else None
| GeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 >= l2.2)) else None
| _ => None
end = Some b
i2v (Z_of_bool b) i32 = v
eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpPP v1 v2 σ l1 l2 v b:
val_to_loc v1 = Some l1
val_to_loc v2 = Some l2
ptr_eq l1 l2 σ.(st_heap) = Some b
i2v (Z_of_bool (negb b)) i32 = v
eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
eval_bin_op op PtrOp PtrOp σ v1 v2 v
| RelOpII op v1 v2 σ n1 n2 it b:
match op with
| EqOp => Some (bool_decide (n1 = n2))
......
......@@ -376,6 +376,37 @@ Proof.
by iApply wp_value.
Qed.
Lemma wp_ptr_relop Φ op v1 v2 l1 l2 E b:
val_to_loc v1 = Some l1
val_to_loc v2 = Some l2
match op with
| EqOp => Some (bool_decide (l1.2 = l2.2))
| NeOp => Some (bool_decide (l1.2 l2.2))
| LtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 < l2.2)) else None
| GtOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 > l2.2)) else None
| LeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 <= l2.2)) else None
| GeOp => if bool_decide (l1.1 = l2.1) then Some (bool_decide (l1.2 >= l2.2)) else None
| _ => None
end = Some b
loc_in_bounds l1 0 - loc_in_bounds l2 0 -
(alloc_alive l1.1 alloc_alive l2.1 Φ (i2v (Z_of_bool b) i32)) -
WP BinOp op PtrOp PtrOp (Val v1) (Val v2) @ E {{ Φ }}.
Proof.
iIntros (Hv1 Hv2 Hop) "#Hl1 #Hl2 HΦ".
iApply wp_binop. iIntros (σ) "Hσ".
iAssert valid_ptr l1 σ⌝%I as %?. {
iApply (alloc_alive_to_valid_ptr with "Hl1 [HΦ] Hσ").
by iDestruct "HΦ" as "[$ _]".
}
iAssert valid_ptr l2 σ⌝%I as %?. {
iApply (alloc_alive_to_valid_ptr with "Hl2 [HΦ] Hσ").
by iDestruct "HΦ" as "[_ [$ _]]".
}
iSplit; first by iPureIntro; eexists _; econstructor.
iDestruct "HΦ" as "(_&_&HΦ)". iIntros "!>" (v' Hstep). iFrame.
inversion Hstep; simplify_eq => //; by move: Hv1 Hv2 => /val_of_to_loc ?/val_of_to_loc?; subst.
Qed.
Lemma wp_ptr_offset Φ vl l E it o ly vo:
val_to_loc vl = Some l
val_to_int vo it = Some o
......
......@@ -248,14 +248,16 @@ Section array.
λ T, i2p (subsume_array_ptr ly1 ly2 base1 base2 idx1 idx2 len1 len2 l β T).
Lemma simplify_hyp_array_ptr ly l β base idx len T:
((base offset{ly} idx) `has_layout_loc` ly - loc_in_bounds base (ly_size (mk_array_layout ly len)) -
(l = (base offset{ly} idx) -
(base offset{ly} idx) `has_layout_loc` ly -
loc_in_bounds base (ly_size (mk_array_layout ly len)) -
tys, base ◁ₗ{β} array ly tys 0 idx < length tys (
ty, tys !! Z.to_nat idx = Some ty - base ◁ₗ{β} array ly (<[Z.to_nat idx := place l]>tys) -
l ◁ₗ{β} ty - T)) -
simplify_hyp (l ◁ₗ{β} array_ptr ly base idx len) T.
Proof.
iIntros "HT (->&%&?)".
iDestruct ("HT" with "[//] [$]") as (tys) "(Harray&%&HT)".
iDestruct ("HT" with "[//] [//] [$]") as (tys) "(Harray&%&HT)".
have [|ty ?]:= lookup_lt_is_Some_2 tys (Z.to_nat idx). lia.
iDestruct (array_get_type (Z.to_nat idx) with "Harray") as "[Hty Harray]". done.
rewrite Z2Nat.id; [|lia].
......
......@@ -244,6 +244,50 @@ Section own.
TypedCopyAllocId v1 P1 v2 P2 :=
λ T, i2p (type_copy_aid v1 v2 P1 P2 T).
(* TODO: Is it a good idea to have this general rule or would it be
better to have more specialized rules? *)
Lemma type_relop_ptr_ptr op b (l1 l2 : loc) β1 β2 ty1 ty2 T:
match op with
| LtOp => Some (bool_decide (l1.2 < l2.2))
| GtOp => Some (bool_decide (l1.2 > l2.2))
| LeOp => Some (bool_decide (l1.2 <= l2.2))
| GeOp => Some (bool_decide (l1.2 >= l2.2))
| _ => None
end = Some b
(l1 ◁ₗ{β1} ty1 - l2 ◁ₗ{β2} ty2 - l1.1 = l2.1 (
(loc_in_bounds l1 0 True)
(loc_in_bounds l2 0 True)
(alloc_alive l1.1 True)
T (i2v (Z_of_bool b) i32) (t2mt (b @ boolean i32)))) -
typed_bin_op l1 (l1 ◁ₗ{β1} ty1) l2 (l2 ◁ₗ{β2} ty2) op PtrOp PtrOp T.
Proof.
iIntros (?) "HT Hl1 Hl2". iIntros (Φ) "HΦ". iDestruct ("HT" with "Hl1 Hl2") as (Heq) "([#? _]&[#? _]&HT)".
destruct op => //; simplify_eq.
all: iApply wp_ptr_relop; try by [apply val_to_of_loc]; simpl; try done.
all: try by case_bool_decide.
all: iSplit; [ iDestruct "HT" as "[[$ _] _]" |].
all: iSplit; [ rewrite Heq; iDestruct "HT" as "[[$ _] _]"| ].
all: iModIntro; iDestruct "HT" as "[_ HT]".
all: iApply "HΦ" => //; by case_bool_decide.
Qed.
Global Program Instance type_lt_ptr_ptr_inst (l1 l2 : loc) β1 β2 ty1 ty2:
TypedBinOp l1 (l1 ◁ₗ{β1} ty1) l2 (l2 ◁ₗ{β2} ty2) LtOp PtrOp PtrOp :=
λ T, i2p (type_relop_ptr_ptr LtOp (bool_decide (l1.2 < l2.2)) l1 l2 β1 β2 ty1 ty2 T _).
Next Obligation. done. Qed.
Global Program Instance type_gt_ptr_ptr_inst (l1 l2 : loc) β1 β2 ty1 ty2:
TypedBinOp l1 (l1 ◁ₗ{β1} ty1) l2 (l2 ◁ₗ{β2} ty2) GtOp PtrOp PtrOp :=
λ T, i2p (type_relop_ptr_ptr GtOp (bool_decide (l1.2 > l2.2)) l1 l2 β1 β2 ty1 ty2 T _).
Next Obligation. done. Qed.
Global Program Instance type_le_ptr_ptr_inst (l1 l2 : loc) β1 β2 ty1 ty2:
TypedBinOp l1 (l1 ◁ₗ{β1} ty1) l2 (l2 ◁ₗ{β2} ty2) LeOp PtrOp PtrOp :=
λ T, i2p (type_relop_ptr_ptr LeOp (bool_decide (l1.2 <= l2.2)) l1 l2 β1 β2 ty1 ty2 T _).
Next Obligation. done. Qed.
Global Program Instance type_ge_ptr_ptr_inst (l1 l2 : loc) β1 β2 ty1 ty2:
TypedBinOp l1 (l1 ◁ₗ{β1} ty1) l2 (l2 ◁ₗ{β2} ty2) GeOp PtrOp PtrOp :=
λ T, i2p (type_relop_ptr_ptr GeOp (bool_decide (l1.2 >= l2.2)) l1 l2 β1 β2 ty1 ty2 T _).
Next Obligation. done. Qed.
(* Lemma type_roundup_frac_ptr v2 β ty P2 T p: *)
(* (P2 -∗ T (val_of_loc p) (t2mt (p @ frac_ptr β ty))) -∗ *)
(* typed_bin_op p (p ◁ₗ{β} ty) v2 P2 RoundUpOp T. *)
......
......@@ -453,20 +453,30 @@ Section typing.
Global Instance related_to_loc l β ty : RelatedTo (l ◁ₗ{β} ty) := {| rt_fic := FindLoc l |}.
Global Instance related_to_val v ty `{!Movable ty} : RelatedTo (v ◁ᵥ ty) := {| rt_fic := FindValP v |}.
Global Instance related_to_loc_in_bounds l n : RelatedTo (loc_in_bounds l n) := {| rt_fic := FindLocInBounds l |}.
Global Instance related_to_alloc_alive l : RelatedTo (alloc_alive l.1) := {| rt_fic := FindLoc l |}.
Lemma subsume_loc_in_bounds ty β l (n m : nat) `{!LocInBounds ty β m} T :
(l ◁ₗ{β} ty - n m T) -
subsume (l ◁ₗ{β} ty) (loc_in_bounds l n) T.
Proof.
iIntros "HT Hl".
iAssert n m%I as %?. { by iDestruct ("HT" with "Hl") as "[% _]". }
iSplit; last by iDestruct ("HT" with "Hl") as "[_ $]".
iApply loc_in_bounds_shorten; last by iApply loc_in_bounds_in_bounds. lia.
iDestruct (loc_in_bounds_in_bounds with "Hl") as "#?".
iDestruct ("HT" with "Hl") as (?) "$".
iApply loc_in_bounds_shorten; last done. lia.
Qed.
Global Instance subsume_loc_in_bounds_inst ty β l n m `{!LocInBounds ty β m} :
Subsume (l ◁ₗ{β} ty) (loc_in_bounds l n) :=
λ T, i2p (subsume_loc_in_bounds ty β l n m T).
Lemma subsume_alloc_alive ty β l P `{!AllocAlive ty β P} T :
(* You don't get l ◁ₗ{β} ty back because alloc_alive is not persistent. *)
P T -
subsume (l ◁ₗ{β} ty) (alloc_alive l.1) T.
Proof. iIntros "[HP $] Hl". by iApply (alloc_alive_alive with "HP"). Qed.
Global Instance subsume_alloc_alive_inst ty β l P `{!AllocAlive ty β P} :
Subsume (l ◁ₗ{β} ty) (alloc_alive l.1) :=
λ T, i2p (subsume_alloc_alive ty β l P T).
Lemma subsume_loc_in_bounds_leq (l : loc) (n1 n2 : nat) T :
n2 n1%nat T -
subsume (loc_in_bounds l n1) (loc_in_bounds l n2) T.
......
......@@ -161,6 +161,20 @@ Section struct.
constructor. by iIntros (l) "(_&_&?&_)".
Qed.
Global Instance struct_alloc_alive sl tys β P `{!TCExists (λ ty, AllocAlive ty β P) tys} :
AllocAlive (struct sl tys) β P.
Proof.
revert select (TCExists _ _).
rewrite TCExists_Exists Exists_exists => -[x [/(elem_of_list_lookup_1 _ _) [i Hx] ?]].
constructor. iIntros (l) "HP Hl".
iDestruct (struct_focus with "Hl") as "[Hl _]".
iDestruct (big_sepL2_length with "Hl") as %Hlen.
have [|n Hn] := lookup_lt_is_Some_2 (field_names (sl_members sl)) i.
{ rewrite Hlen. by apply: lookup_lt_Some. }
iDestruct (big_sepL2_lookup with "Hl") as "Hl" => //.
by iDestruct (alloc_alive_alive with "HP Hl") as "Hl".
Qed.
Global Instance strip_guarded_struct sl tys tys' E1 E2 β {Hs :StripGuardedLst β E1 E2 tys tys'}:
StripGuarded β E1 E2 (struct sl tys) (struct sl tys').
Proof.
......
......@@ -319,12 +319,35 @@ Section loc_in_bounds.
Qed.
Global Instance movable_loc_in_bounds_inst ty `{!Movable ty}:
LocInBounds ty Own (ly_size (ty_layout ty)).
LocInBounds ty Own (ly_size (ty_layout ty)) | 100.
Proof.
constructor. iIntros (?) "?". by iApply movable_loc_in_bounds.
Qed.
End loc_in_bounds.
Class AllocAlive `{!typeG Σ} (ty : type) (β : own_state) (P : iProp Σ) := {
alloc_alive_alive l : P - ty.(ty_own) β l - alloc_alive l.1
}.
Arguments alloc_alive_alive {_ _} _ _ _ {_} _.
Hint Mode AllocAlive + + + + - : typeclass_instances.
Section alloc_alive.
Context `{!typeG Σ}.
Lemma movable_alloc_alive ty l `{!Movable ty} :
ty.(ty_layout).(ly_size) 0%nat
ty.(ty_own) Own l - alloc_alive l.1.
Proof.
iIntros (?) "Hl". iDestruct (ty_deref with "Hl") as (v) "[Hl Hv]".
iDestruct (ty_size_eq with "Hv") as %Hv.
iApply heap_mapsto_alive => //. by rewrite Hv.
Qed.
Global Instance movable_alloc_alive_inst ty `{!Movable ty}:
AllocAlive ty Own (ly_size (ty_layout ty) 0%nat) | 100.
Proof. constructor. iIntros (??) "?". by iApply movable_alloc_alive. Qed.
End alloc_alive.
Notation "l ◁ₗ{ β } ty" := (ty_own ty β l) (at level 15, format "l ◁ₗ{ β } ty") : bi_scope.
Notation "l ◁ₗ ty" := (ty_own ty Own l) (at level 15) : bi_scope.
Notation "v ◁ᵥ ty" := (ty_own_val ty v) (at level 15) : bi_scope.
......
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