Skip to content

GitLab

Commit dc744bb2 authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files
Options

Check allocation range with new ghost state (MR !3, Fixes #20).

parent 6e747174
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 965 additions and 406 deletions
examples/proofs/malloc1/generated_code.v
View file @ dc744bb2
......@@ -109,20 +109,20 @@ Section code.
Definition loc_104 : location_info := LocationInfo file_0 59 8 59 9.
Definition loc_105 : location_info := LocationInfo file_0 59 19 59 33.
Definition loc_108 : location_info := LocationInfo file_0 81 4 81 27.
Definition loc_109 : location_info := LocationInfo file_0 85 4 85 22.
Definition loc_110 : location_info := LocationInfo file_0 86 4 86 16.
Definition loc_111 : location_info := LocationInfo file_0 86 4 86 11.
Definition loc_112 : location_info := LocationInfo file_0 86 4 86 5.
Definition loc_113 : location_info := LocationInfo file_0 86 4 86 5.
Definition loc_114 : location_info := LocationInfo file_0 86 14 86 15.
Definition loc_115 : location_info := LocationInfo file_0 86 14 86 15.
Definition loc_116 : location_info := LocationInfo file_0 85 4 85 11.
Definition loc_117 : location_info := LocationInfo file_0 85 4 85 5.
Definition loc_118 : location_info := LocationInfo file_0 85 4 85 5.
Definition loc_119 : location_info := LocationInfo file_0 85 14 85 21.
Definition loc_120 : location_info := LocationInfo file_0 85 14 85 21.
Definition loc_121 : location_info := LocationInfo file_0 85 14 85 15.
Definition loc_122 : location_info := LocationInfo file_0 85 14 85 15.
Definition loc_109 : location_info := LocationInfo file_0 83 4 83 22.
Definition loc_110 : location_info := LocationInfo file_0 84 4 84 16.
Definition loc_111 : location_info := LocationInfo file_0 84 4 84 11.
Definition loc_112 : location_info := LocationInfo file_0 84 4 84 5.
Definition loc_113 : location_info := LocationInfo file_0 84 4 84 5.
Definition loc_114 : location_info := LocationInfo file_0 84 14 84 15.
Definition loc_115 : location_info := LocationInfo file_0 84 14 84 15.
Definition loc_116 : location_info := LocationInfo file_0 83 4 83 11.
Definition loc_117 : location_info := LocationInfo file_0 83 4 83 5.
Definition loc_118 : location_info := LocationInfo file_0 83 4 83 5.
Definition loc_119 : location_info := LocationInfo file_0 83 14 83 21.
Definition loc_120 : location_info := LocationInfo file_0 83 14 83 21.
Definition loc_121 : location_info := LocationInfo file_0 83 14 83 15.
Definition loc_122 : location_info := LocationInfo file_0 83 14 83 15.
Definition loc_123 : location_info := LocationInfo file_0 81 25 81 26.
Definition loc_124 : location_info := LocationInfo file_0 81 25 81 26.
......
theories/lang/base.v
View file @ dc744bb2
......@@ -66,6 +66,31 @@ Lemma entails_eq {PROP : bi} (P1 P2 : PROP) :
P1 = P2 → P1 -∗ P2.
Proof. move => ->. reflexivity. Qed.
Section theorems.
Context `{FinMapDom K M D}.
Lemma dom_list_to_map {A} (l : list (K * A)) :
dom D (list_to_map (M:=M A) l) ≡ list_to_set l.*1.
Proof using Type*.
elim: l => /=. { by apply dom_empty. }
move => ? l <-. by apply dom_insert.
Qed.
Lemma dom_list_to_map_L {A} (l : list (K * A)) `{!LeibnizEquiv D}:
dom D (list_to_map (M:=M A) l) = list_to_set l.*1.
Proof using Type*. unfold_leibniz. apply: dom_list_to_map. Qed.
End theorems.
Section list_to_map.
Context `{FinMap K M}.
Lemma list_to_map_app {A} (l1 l2 : list (K * A)):
list_to_map (M := M A) (l1 ++ l2) = list_to_map l1 ∪ list_to_map l2.
Proof using Type*.
elim: l1 => /=. { by rewrite left_id. }
move => [??] ? IH /=. by rewrite IH insert_union_l.
Qed.
End list_to_map.
Inductive TCOneIsSome {A} : option A → option A → Prop :=
| tc_one_is_some_left n1 o2 : TCOneIsSome (Some n1) o2
......
theories/lang/heap.v
View file @ dc744bb2
This diff is collapsed.
theories/lang/lang.v
View file @ dc744bb2
......@@ -225,7 +225,13 @@ Inductive lock_state := WSt | RSt (n : nat).
Definition heap := gmap loc (lock_state * mbyte).
Definition blocks := gset block_id.
Record allocation :=
Allocation {
alloc_start : Z; (* First valid address. *)
alloc_end : Z; (* One-past-the-end address. *)
}.
Definition blocks := gmap block_id allocation.
......@@ -425,7 +431,7 @@ Proof.
+ rewrite /int_modulus /bits_per_int. lia.
+ rewrite /int_half_modulus in HM.
transitivity (2 ^ (bits_per_int it -1)); first lia.
rewrite /bits_per_int /bytes_per_int /bits_per_byte /=.
rewrite /bits_per_int /bytes_per_int /bits_per_byte /=.
apply Z.pow_lt_mono_r; try lia.
+ rewrite /int_modulus /bits_per_int in HM. lia.
Qed.
......@@ -565,6 +571,14 @@ Qed.
(*** Helper functions for accessing the heap *)
(* 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. *)
Definition heap_loc_in_bounds (l : loc) (n : nat) (st : state) : Prop :=
∃ alloc, st.(st_used_blocks) !! l.1 = Some alloc ∧
alloc.(alloc_start) ≤ l.2 ∧
l.2 + n ≤ alloc.(alloc_end).
Fixpoint heap_at_go l v flk h : Prop :=
match v with
| [] => True
......@@ -658,51 +672,53 @@ Definition ptr_eq l1 l2 h : option bool :=
(* evaluation can be non-deterministic for comparing pointers *)
(* TODO: implement *)
Inductive eval_bin_op : bin_op → op_type → op_type → heap → val → val → val → Prop :=
| AddOpPI v1 v2 h o l:
Inductive eval_bin_op : bin_op → op_type → op_type → state → val → val → val → Prop :=
| AddOpPI v1 v2 σ o l:
val_to_loc v1 = Some l →
val_to_int v2 size_t = Some o →
eval_bin_op AddOp PtrOp (IntOp size_t) h v1 v2 (val_of_loc (l +ₗ o))
| PtrOffsetOpIP v1 v2 h o l ly it:
eval_bin_op AddOp PtrOp (IntOp size_t) σ v1 v2 (val_of_loc (l +ₗ o))
| PtrOffsetOpIP v1 v2 σ o l ly it:
val_to_int v1 it = Some o →
val_to_loc v2 = Some l →
(* TODO: should we have an alignment check here? *)
0 ≤ o →
eval_bin_op (PtrOffsetOp ly) (IntOp it) PtrOp h v1 v2 (val_of_loc (l offset{ly}ₗ o))
| EqOpPNull v1 v2 h l v:
eval_bin_op (PtrOffsetOp ly) (IntOp it) PtrOp σ v1 v2 (val_of_loc (l offset{ly}ₗ o))
| EqOpPNull v1 v2 σ l v:
heap_loc_in_bounds l 0%nat σ →
val_to_loc v1 = Some l →
val_to_int v2 size_t = Some 0 →
(* TODO ( see below ): Should we really hard code i32 here because of C? *)
i2v (Z_of_bool false) i32 = v →
eval_bin_op EqOp PtrOp PtrOp h v1 v2 v
| NeOpPNull v1 v2 h l v:
eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpPNull v1 v2 σ l v:
heap_loc_in_bounds l 0%nat σ →
val_to_loc v1 = Some l →
val_to_int v2 size_t = Some 0 →
i2v (Z_of_bool true) i32 = v →
eval_bin_op NeOp PtrOp PtrOp h v1 v2 v
| EqOpNullNull v1 v2 h v:
eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| EqOpNullNull v1 v2 σ v:
val_to_int v1 size_t = Some 0 →
val_to_int v2 size_t = Some 0 →
i2v (Z_of_bool true) i32 = v →
eval_bin_op EqOp PtrOp PtrOp h v1 v2 v
| NeOpNullNull v1 v2 h v:
eval_bin_op EqOp PtrOp PtrOp σ v1 v2 v
| NeOpNullNull v1 v2 σ v:
val_to_int v1 size_t = Some 0 →
val_to_int v2 size_t = Some 0 →
i2v (Z_of_bool false) i32 = v →
eval_bin_op NeOp PtrOp PtrOp h v1 v2 v
| EqOpPP v1 v2 h l1 l2 v b:
eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| EqOpPP v1 v2 σ l1 l2 v b:
val_to_loc v1 = Some l1 →
val_to_loc v2 = Some l2 →
ptr_eq l1 l2 h = Some b →
ptr_eq l1 l2 σ.(st_heap) = Some b →
i2v (Z_of_bool b) i32 = v →
eval_bin_op EqOp PtrOp PtrOp h v1 v2 v
| NeOpPP v1 v2 h l1 l2 v b:
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 h = Some b →
ptr_eq l1 l2 σ.(st_heap) = Some b →
i2v (Z_of_bool (negb b)) i32 = v →
eval_bin_op NeOp PtrOp PtrOp h v1 v2 v
| RelOpII op v1 v2 h n1 n2 it b:
eval_bin_op NeOp PtrOp PtrOp σ v1 v2 v
| RelOpII op v1 v2 σ n1 n2 it b:
match op with
| EqOp => Some (bool_decide (n1 = n2))
| NeOp => Some (bool_decide (n1 ≠ n2))
......@@ -716,10 +732,10 @@ Inductive eval_bin_op : bin_op → op_type → op_type → heap → val → val
val_to_int v2 it = Some n2 →
(* TODO: What is the right int type of the result here? C seems to
use i32 but maybe we don't want to hard code that. *)
eval_bin_op op (IntOp it) (IntOp it) h v1 v2 (i2v (Z_of_bool b) i32)
eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 (i2v (Z_of_bool b) i32)
(* This defines checked versions of the arithmetic operations which
are UB if the result is out of bounds for it. *)
| ArithOpII op v1 v2 h n1 n2 it n v:
| ArithOpII op v1 v2 σ n1 n2 it n v:
match op with
| AddOp => Some (n1 + n2)
| SubOp => Some (n1 - n2)
......@@ -740,23 +756,23 @@ are UB if the result is out of bounds for it. *)
val_to_int v1 it = Some n1 →
val_to_int v2 it = Some n2 →
val_of_int n it = Some v →
eval_bin_op op (IntOp it) (IntOp it) h v1 v2 v
eval_bin_op op (IntOp it) (IntOp it) σ v1 v2 v
.
Inductive eval_un_op : un_op → op_type → heap → val → val → Prop :=
| CastOpII itt its h vs vt n:
Inductive eval_un_op : un_op → op_type → state → val → val → Prop :=
| CastOpII itt its σ vs vt n:
val_to_int vs its = Some n →
val_of_int n itt = Some vt →
eval_un_op (CastOp (IntOp itt)) (IntOp its) h vs vt
| CastOpPP h vs vt l:
eval_un_op (CastOp (IntOp itt)) (IntOp its) σ vs vt
| CastOpPP σ vs vt l:
val_to_loc vs = Some l →
val_of_loc l = vt →
eval_un_op (CastOp PtrOp) PtrOp h vs vt
| NegOpI it h vs vt n:
eval_un_op (CastOp PtrOp) PtrOp σ vs vt
| NegOpI it σ vs vt n:
val_to_int vs it = Some n →
val_of_int (-n) it = Some vt →
eval_un_op NegOp (IntOp it) h vs vt
eval_un_op NegOp (IntOp it) σ vs vt
.
(*** Evaluation of Expressions *)
......@@ -765,10 +781,10 @@ Inductive expr_step : expr → state → list Empty_set → expr → state → l
| SkipES v σ:
expr_step (SkipE (Val v)) σ [] (Val v) σ []
| UnOpS op v σ v' ot:
eval_un_op op ot σ.(st_heap) v v' →
eval_un_op op ot σ v v' →
expr_step (UnOp op ot (Val v)) σ [] (Val v') σ []
| BinOpS op v1 v2 σ v' ot1 ot2:
eval_bin_op op ot1 ot2 σ.(st_heap) v1 v2 v' →
eval_bin_op op ot1 ot2 σ v1 v2 v' →
expr_step (BinOp op ot1 ot2 (Val v1) (Val v2)) σ [] (Val v') σ []
| DerefS o v l ly v' σ:
let start_st st := ∃ n, st = if o is Na2Ord then RSt (S n) else RSt n in
......@@ -960,6 +976,9 @@ Definition subst_function (xs : list var_name) (vs : list val) (f : function) :
f_args := f.(f_args); f_init := f.(f_init); f_local_vars := f.(f_local_vars);
|}.
Definition to_allocation (off : Z) (len : nat) : allocation :=
Allocation off (off + len).
(*** Evaluation of statements *)
Inductive stmt_step : thread_state → state → list Empty_set → thread_state → state → list thread_state → Prop :=
| StmtExprS ts σ σ' Ks e e' os efs:
......@@ -1007,8 +1026,8 @@ Inductive stmt_step : thread_state → state → list Empty_set → thread_state
Forall (heap_block_free σ.(st_heap)) lsa →
Forall (heap_block_free σ.(st_heap)) lsv →
(* ensure that ls blocks are unused *)
Forall (λ l, l.1 ∉ σ.(st_used_blocks)) lsa →
Forall (λ l, l.1 ∉ σ.(st_used_blocks)) lsv →
Forall (λ l, σ.(st_used_blocks) !! l.1 = None) lsa →
Forall (λ l, σ.(st_used_blocks) !! l.1 = None) lsv →
(* ensure that locations are aligned *)
Forall2 has_layout_loc lsa fn.(f_args).*2 →
Forall2 has_layout_loc lsv fn.(f_local_vars).*2 →
......@@ -1018,7 +1037,8 @@ Inductive stmt_step : thread_state → state → list Empty_set → thread_state
heap_upd_list lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) (λ _, RSt 0%nat) σ.(st_heap) = h' →
(* initialize the arguments with the supplied values *)
heap_upd_list lsa vs (λ _, RSt 0%nat) h' = h'' →
σ.(st_used_blocks) ∪ list_to_set (lsa ++ lsv).*1 = ub' →
(* add used blocks allocations *)
list_to_map (zip (lsa.*1 ++ lsv.*1) (zip_with to_allocation (lsa.*2 ++ lsv.*2) (ly_size <$> (fn.(f_args).*2 ++ fn.(f_local_vars).*2)))) ∪ σ.(st_used_blocks) = ub' →
rf = {| rf_fn := fn'; rf_locs := zip lsa fn.(f_args).*2 ++ zip lsv fn.(f_local_vars).*2; rf_stmt := Goto fn'.(f_init); |} →
co = {| c_rfn := (update_stmt ts s).(ts_rfn); c_rvar := ret |} →
stmt_step ts σ [] {| ts_conts := co::ts.(ts_conts); ts_rfn := rf |}
......@@ -1140,16 +1160,15 @@ Lemma heap_at_inj_val l ly h v v' flk1 flk2:
heap_at l ly v flk1 h → heap_at l ly v' flk2 h → v = v'.
Proof. move => [_ [Hv1 H1]] [_ [Hv2 H2]]. apply: heap_at_go_inj_val => //. congruence. Qed.
Lemma heap_fresh_blocks n (ub : gset Z) lys :
Lemma heap_fresh_blocks n (ub : blocks) lys :
length lys = n →
∃ ls, length ls = n ∧ Forall (λ l : loc, l.1 ∉ ub) ls ∧ NoDup ls.*1 ∧ Forall2 has_layout_loc ls lys.
∃ ls, length ls = n ∧ Forall (λ l : loc, ub !! l.1 = None) ls ∧ NoDup ls.*1 ∧ Forall2 has_layout_loc ls lys.
Proof.
eexists ((λ x, (x, 0)) <$> fresh_list n ub). rewrite fmap_length fresh_list_length.
split_and! => //.
- apply Forall_forall => l. move => /elem_of_list_fmap[?[->?]]/=.
by apply: fresh_list_is_fresh.
- rewrite -list_fmap_compose. eapply (NoDup_proper _ (fresh_list n ub)); last by apply NoDup_fresh_list.
elim: (fresh_list n ub); naive_solver.
eexists ((λ x, (x, 0)) <$> fresh_list n (dom (gset block_id) ub)). split_and!.
- rewrite fmap_length fresh_list_length //.
- apply Forall_forall => l. move => /elem_of_list_fmap[?[->He]]/=.
by apply fresh_list_is_fresh, not_elem_of_dom in He.
- rewrite -list_fmap_compose NoDup_fmap. by apply NoDup_fresh_list.
- rewrite Forall2_fmap_l. apply Forall2_true; last by rewrite fresh_list_length.
move => ?? /=. by apply Z.divide_0_r.
Qed.
......@@ -1227,6 +1246,7 @@ Canonical Structure locO := leibnizO loc.
Canonical Structure layoutO := leibnizO layout.
Canonical Structure valO := leibnizO val.
Canonical Structure exprO := leibnizO expr.
Canonical Structure allocationO := leibnizO allocation.
(*** Tests *)
......
theories/lang/lifting.v
View file @ dc744bb2
......@@ -50,48 +50,60 @@ Proof. rewrite /Use. solve_atomic. Qed.
Section expr_lifting.
Context `{!refinedcG Σ}.
Lemma wp_binop v' v1 v2 Φ op E ot1 ot2:
(∀ h, eval_bin_op op ot1 ot2 h v1 v2 v') →
▷ (∀ v h, ⌜eval_bin_op op ot1 ot2 h v1 v2 v⌝ -∗ Φ v) -∗
WP BinOp op ot1 ot2 (Val v1) (Val v2) @ E {{ Φ }}.
Lemma wp_binop v1 v2 Φ op E ot1 ot2:
(∀ σ, state_ctx σ -∗
⌜∃ v', eval_bin_op op ot1 ot2 σ v1 v2 v'⌝ ∗
▷ (∀ v', ⌜eval_bin_op op ot1 ot2 σ v1 v2 v'⌝ -∗ state_ctx σ ∗ Φ v')) -∗
WP BinOp op ot1 ot2 (Val v1) (Val v2) @ E {{ Φ }}.
Proof.
iIntros (Hop) "HΦ".
iIntros "HΦ".
iApply wp_lift_atomic_head_step; auto.
iIntros (σ1 ???) "[Hhctx Hfctx]".
iModIntro. iSplit; first by eauto using BinOpS.
iIntros (σ1 ???) "Hctx !>".
iDestruct ("HΦ" with "Hctx") as ([v' Heval]) "HΦ".
iSplit; first by eauto using BinOpS.
iIntros "!#" (e2 σ2 efs Hst). inv_expr_step.
iFrame. iModIntro. iSplitL => //. by iApply "HΦ".
iModIntro. rewrite right_id. by iApply "HΦ".
Qed.
Lemma wp_binop_det v' v1 v2 Φ op E ot1 ot2:
(∀ h v, eval_bin_op op ot1 ot2 h v1 v2 v ↔ v = v') →
▷ Φ v' -∗ WP BinOp op ot1 ot2 (Val v1) (Val v2) @ E {{ Φ }}.
(∀ σ v, state_ctx σ -∗ ⌜eval_bin_op op ot1 ot2 σ v1 v2 v ↔ v = v'⌝) ∧ ▷ Φ v' -∗
WP BinOp op ot1 ot2 (Val v1) (Val v2) @ E {{ Φ }}.
Proof.
iIntros (Hop) "HΦ".
iApply (wp_binop v'). by move => h; apply Hop.
iIntros "!#" (v h). rewrite Hop. iIntros (?). subst. by iApply "HΦ".
iIntros "H".
iApply wp_binop. iIntros (σ) "Hctx". iSplit.
{ iExists v'. iDestruct "H" as "[Hσ _]". by iDestruct ("Hσ" with "Hctx") as %->. }
iIntros "!>" (v Hbinop). iAssert (⌜v = v'⌝)%I as %->.
{ iDestruct "H" as "[Hσ _]". iDestruct ("Hσ" with "Hctx") as %Hvv'.
iPureIntro. naive_solver. }
by iDestruct "H" as "[_ $]".
Qed.
Lemma wp_unop v' v1 Φ op E ot:
(∀ h, eval_un_op op ot h v1 v') →
▷ (∀ v h, ⌜eval_un_op op ot h v1 v⌝ -∗ Φ v) -∗
Lemma wp_unop v1 Φ op E ot:
(∀ σ, state_ctx σ -∗
⌜∃ v', eval_un_op op ot σ v1 v'⌝ ∗
▷ (∀ v', ⌜eval_un_op op ot σ v1 v'⌝ -∗ state_ctx σ ∗ Φ v')) -∗
WP UnOp op ot (Val v1) @ E {{ Φ }}.
Proof.
iIntros (Hop) "HΦ".
iIntros "HΦ".
iApply wp_lift_atomic_head_step; auto.
iIntros (σ1 ???) "[Hhctx Hfctx]".
iModIntro. iSplit; first by eauto using UnOpS.
iIntros (σ1 ???) "Hctx !>".
iDestruct ("HΦ" with "Hctx") as ([v' Heval]) "HΦ".
iSplit; first by eauto using UnOpS.
iIntros "!#" (e2 σ2 efs Hst). inv_expr_step.
iFrame. iModIntro. iSplitL => //. by iApply "HΦ".
iModIntro. rewrite right_id. by iApply "HΦ".
Qed.
Lemma wp_unop_det v' v1 Φ op E ot:
(∀ h v, eval_un_op op ot h v1 v ↔ v = v') →
▷ Φ v' -∗ WP UnOp op ot (Val v1) @ E {{ Φ }}.
(∀ σ v, state_ctx σ -∗ ⌜eval_un_op op ot σ v1 v ↔ v = v'⌝) ∧ ▷ Φ v' -∗
WP UnOp op ot (Val v1) @ E {{ Φ }}.
Proof.
iIntros (Hop) "HΦ".
iApply (wp_unop v'). by move => h; apply Hop.
iIntros "!#" (v h). rewrite Hop. iIntros (?). subst. by iApply "HΦ".
iIntros "H".
iApply wp_unop. iIntros (σ) "Hctx". iSplit.
{ iExists v'. iDestruct "H" as "[Hσ _]". by iDestruct ("Hσ" with "Hctx") as %->. }
iIntros "!>" (v Hbinop). iAssert (⌜v = v'⌝)%I as %->.
{ iDestruct "H" as "[Hσ _]". iDestruct ("Hσ" with "Hctx") as %Hvv'.
iPureIntro. naive_solver. }
by iDestruct "H" as "[_ $]".
Qed.
Lemma wp_deref v Φ vl l ly q E o:
......@@ -117,13 +129,13 @@ Proof.
iSplit; first by eauto 7 using DerefS.
iIntros "!#" (e2 σ2 efs Hst). inv_expr_step. iMod "Hclose" as "$". iModIntro. unfold end_st, end_expr.
have <- : (v = v') by apply: heap_at_inj_val.
iFrame => /=. iSplit; first by eauto 7 using block_used_agree_heap_upd.
iFrame => /=. iSplit; first by eauto 7 using blocks_used_agree_heap_upd.
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros ([h2 fn2] ???) "(%&Hhctx&Hfctx)". iMod ("Hσclose" with "Hhctx") as (?) "(Hσ & Hv)".
iModIntro; iSplit; first by eauto 7 using DerefS.
iIntros "!#" (e2 σ2 efs Hst) "!#". inv_expr_step.
have <- : (v = v'0) by apply: heap_at_inj_val.
iFrame. iSplitR => //=. iSplit; first by eauto 7 using block_used_agree_heap_upd.
iFrame. iSplitR => //=. iSplit; first by eauto 7 using blocks_used_agree_heap_upd.
by iApply "HΦ".
Qed.
......@@ -153,7 +165,7 @@ Proof.
have ? : (length ve0 = length vo0) by congruence.
iMod (heap_write with "Hhctx Hl2") as "[$ Hl2]" => //.
iFrame. iModIntro. rewrite right_id /=.
iSplit; first by eauto using block_used_agree_heap_upd.
iSplit; first by eauto using blocks_used_agree_heap_upd.
by iApply ("HΦ" with "Hl1").
Qed.
......@@ -183,7 +195,7 @@ Proof.
have ? : (length vo0 = length vd) by congruence.
iMod (heap_write with "Hhctx Hl1") as "[$ Hmt]" => //.
iFrame. iModIntro. rewrite right_id /=.
iSplit; first by eauto using block_used_agree_heap_upd.
iSplit; first by eauto using blocks_used_agree_heap_upd.
by iApply ("HΦ" with "Hmt").
Qed.
......@@ -193,8 +205,10 @@ Lemma wp_neg_int Φ v v' n E it:
▷ Φ (v') -∗ WP UnOp NegOp (IntOp it) (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv Hv') "HΦ".
iApply wp_unop; first eauto using NegOpI.
iIntros "!#" (v2 h Hop). by inversion Hop; simplify_eq.
iApply wp_unop_det. iSplit => //.
iIntros (σ v2) "_ !%". split.
- by inversion 1; simplify_eq.
- move => ->. by econstructor.
Qed.
Lemma wp_cast_int Φ v v' n E its itt:
......@@ -203,8 +217,10 @@ Lemma wp_cast_int Φ v v' n E its itt:
▷ Φ (v') -∗ WP UnOp (CastOp (IntOp itt)) (IntOp its) (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv Hv') "HΦ".
iApply wp_unop; first eauto using CastOpII.
iIntros "!#" (v2 h Hop). by inversion Hop; simplify_eq.
iApply wp_unop_det. iSplit => //.
iIntros (σ v2) "_ !%". split.
- by inversion 1; simplify_eq.
- move => ->. by econstructor.
Qed.
Lemma wp_cast_loc Φ v l E:
......@@ -212,8 +228,10 @@ Lemma wp_cast_loc Φ v l E:
▷ Φ (val_of_loc l) -∗ WP UnOp (CastOp PtrOp) PtrOp (Val v) @ E {{ Φ }}.
Proof.
iIntros (Hv) "HΦ".
iApply wp_unop; first eauto using CastOpPP.
iIntros "!#" (v2 h Hop). by inversion Hop; simplify_eq.
iApply wp_unop_det. iSplit => //.
iIntros (σ v2) "_ !%". split.
- by inversion 1; simplify_eq.
- move => ->. by econstructor.
Qed.
Lemma wp_ptr_offset Φ vl l E it o ly vo:
......@@ -223,8 +241,10 @@ Lemma wp_ptr_offset Φ vl l E it o ly vo:
▷ Φ (val_of_loc (l offset{ly}ₗ o)) -∗ WP Val vl at_offset{ ly , PtrOp, IntOp it} Val vo @ E {{ Φ }}.
Proof.
iIntros (Hvl Hvo Ho) "HΦ".
iApply wp_binop; first eauto using PtrOffsetOpIP.
iIntros "!#" (v h Hbop). by inversion Hbop; simplify_eq.
iApply wp_binop_det. iSplit; last done.
iIntros (σ v) "_ !%". split.
- inversion 1. by simplify_eq.
- move => ->. by apply PtrOffsetOpIP.
Qed.
Lemma wp_get_member Φ vl l sl n E:
......@@ -239,8 +259,10 @@ Proof.
by apply offset_of_bound.
}
rewrite Hs /=. move: Hs => /val_to_of_int Hs.
iApply wp_binop; first eauto using AddOpPI.
iIntros "!#" (v h Hbop). by inversion Hbop; simplify_eq.
iApply wp_binop_det. iSplit; last done.
iIntros (σ v) "_ !%". split.
- inversion 1. by simplify_eq.
- move => ->. by apply AddOpPI.
Qed.
Lemma wp_get_member_union Φ vl l ul n E:
......@@ -426,12 +448,13 @@ Lemma wps_call Q Ψ r vf vl s f fn:
) -∗
WPs (r <- Val vf with Val <$> vl; s) {{ Q , Ψ }}.
Proof.
rewrite (stmt_wp_unfold (Call _ _ _ _)).
move => Hf Hly. iIntros "Hf HWP" (ts Φ ->) "HΨ".
move: (Hly) => /Forall2_length. rewrite fmap_length => ?.
iApply wp_lift_step => /=. 1: by apply stmt_to_val_non_ret.
iIntros (σ1 κ _ _) "(H&Hhctx&Hfctx)". iDestruct "H" as %Hub.
rewrite (stmt_wp_unfold (Call _ _ _ _)) => Hf Hly.
move: (Hly) => /Forall2_length; rewrite fmap_length => Hlen_vs.
iIntros "Hf HWP" (ts Φ ->) "HΨ".
iApply wp_lift_step => /=; first by apply stmt_to_val_non_ret.
iIntros (σ1 κ _ _) "(H&Hhctx&Hbctx&Hfctx)". iDestruct "H" as %Hub.
iDestruct (fntbl_entry_lookup with "Hfctx Hf") as %Hfn.
iMod (fupd_intro_mask' _ ∅) as "HE"; first set_solver. iModIntro. iSplit. {
have [|ls [Hlen [Hfree [HND Hlys]]]] := heap_fresh_blocks (length fn.(f_args) + length fn.(f_local_vars)) σ1.(st_used_blocks) ((f_args fn).*2 ++ (f_local_vars fn).*2). by rewrite !app_length !fmap_length.
have [lsa [lsv [? [Ha Hv]]]] : (∃ lsa lsv, ls = lsa ++ lsv ∧ length lsa = length fn.(f_args) ∧ length lsv = length fn.(f_local_vars)). {
......@@ -441,29 +464,71 @@ Proof.
subst ls. move: Hfree => /Forall_app[/Forall_forall ? /Forall_forall?].
move: Hlys => /Forall2_app_inv[|??]. by rewrite fmap_length.
iPureIntro. eexists _, _, _, _; simpl.
eapply (CallS lsa lsv) => //; apply/Forall_forall => ??; try apply Hub;set_solver. }
eapply (CallS lsa lsv) => //;apply/Forall_forall => ??; try apply Hub; set_solver.
}
iIntros "!#" (e2 σ2 efs Hst). inv_stmt_step.
match goal with | H : NoDup _ |- _ => rewrite ->fmap_app, NoDup_app in H; revert H end.
move => [? [? ?]].
iMod (heap_alloc_list lsv (((λ p, replicate (ly_size p.2) ☠%V) <$> f_local_vars fn)) with "Hhctx") as "[Hhctx Hv]" => //.
repeat match goal with | H : Forall (fun l => _ !! _ = None) _ |- _ => move/Forall_forall in H end.
revert select (length lsa = _) => Hlena.
revert select (length lsv = _) => Hlenv.
(* Allocate new allocation blocks for the local variables. *)
iMod (allocs_alloc_list lsv (((λ p, replicate (ly_size p.2) ☠%V) <$> f_local_vars fn))
with "Hbctx") as "[Hbctx Hblsv]" => //.
{ apply elem_of_disjoint => id Hdom Hin. move: Hdom. apply/not_elem_of_dom. set_solver. }
{ by rewrite fmap_length. }