Commit c74a834f authored by Rodolphe Lepigre's avatar Rodolphe Lepigre
Browse files

Finished [early_alloc.c].

parent 8b97fc2c
Pipeline #42281 passed with stage
in 31 minutes and 32 seconds
......@@ -35,8 +35,8 @@ static struct region mem;
[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
[[rc::returns("given @ int<size_t>")]]
[[rc::ensures("global mem : {(base, given, remaining)} @ region")]]
[[rc::tactics("rewrite Z.add_simpl_l /PAGE_SIZE. solve_goal.")]]
[[rc::tactics("rewrite /PAGE_SIZE Z.add_simpl_l Z.shiftr_div_pow2 //= Z.div_mul //=.")]]
[[rc::tactics("all: rewrite /PAGE_SIZE Z.add_simpl_l; try solve_goal.")]]
[[rc::tactics("all: rewrite Z.shiftr_div_pow2 //= Z.div_mul //=.")]]
size_t hyp_early_alloc_nr_pages(void){
return (cur - (uintptr_t) base) >> PAGE_SHIFT;
}
......@@ -53,13 +53,12 @@ extern void clear_page(void *to);
[[rc::returns("&own<zeroed<PAGES<{Z.to_nat n}>>>")]]
[[rc::ensures("global mem : {(base, given + n, remaining - n)%Z} @ region")]]
[[rc::tactics("all: unfold PAGE_SIZE, PAGE_SHIFT in *; try solve_goal.")]]
[[rc::tactics("assert (0 ≤ n ≪ 12); last by lia. by apply Z.shiftl_nonneg.")]]
[[rc::tactics("transitivity max_alloc_end; last done; etransitivity; last exact H10; "
"rewrite Z.shiftl_mul_pow2 -?Z.add_assoc => //=; apply -> Z.add_le_mono_l; lia.")]]
[[rc::tactics("rewrite Z.shiftl_mul_pow2 in H18 => //. lia.")]]
[[rc::tactics("rewrite Z.shiftl_mul_pow2 //=. lia.")]]
[[rc::tactics("apply: has_layout_loc_trans' => //. by rewrite ly_offset_PAGES.")]]
[[rc::trust_me]]
[[rc::tactics("all: rewrite -> Z.shiftl_mul_pow2 in *; try lia.")]]
[[rc::tactics("all: try apply: has_layout_loc_trans' => //.")]]
[[rc::tactics("all: rewrite ?ly_offset_PAGES; try solve_goal.")]]
[[rc::tactics("all: transitivity max_alloc_end; last done.")]]
[[rc::tactics("all: etransitivity; last eassumption.")]]
[[rc::tactics("all: rewrite -?Z.add_assoc => //=; apply -> Z.add_le_mono_l; lia.")]]
void *hyp_early_alloc_contig(unsigned int nr_pages){
uintptr_t ret = cur, p;
unsigned int i;
......@@ -83,6 +82,7 @@ void *hyp_early_alloc_contig(unsigned int nr_pages){
[[rc::constraints("global mem : {(base, given + n, remaining - n)%Z} @ region")]]
[[rc::constraints("{i ≤ n}")]]
for (i = 0; i < nr_pages; i++) {
rc_unfold(base);
p = ret + (i << PAGE_SHIFT);
clear_page(rc_copy_alloc_id((void *)(p), base));
}
......
(* Let's skip that, you seem to have some faith. *)
From refinedc.typing Require Import typing.
From refinedc.linux.pkvm.early_alloc Require Import generated_code.
From refinedc.linux.pkvm.early_alloc Require Import generated_spec.
From refinedc.linux.pkvm.early_alloc Require Import instances.
Set Default Proof Using "Type".
(* Generated from [linux/pkvm/early_alloc.c]. *)
Section proof_hyp_early_alloc_contig.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [hyp_early_alloc_contig]. *)
Lemma type_hyp_early_alloc_contig (global_mem global_clear_page : loc) :
global_locs !! "mem" = Some global_mem
global_clear_page ◁ᵥ global_clear_page @ function_ptr type_of_clear_page -
typed_function (impl_hyp_early_alloc_contig global_mem global_clear_page) type_of_hyp_early_alloc_contig.
Proof.
Open Scope printing_sugar.
start_function "hyp_early_alloc_contig" ([[[base given] remaining] n]) => arg_nr_pages local_i local_ret local_p.
split_blocks ((
<[ "#3" :=
i : nat,
arg_nr_pages ◁ₗ (n @ (int (u32)))
local_i ◁ₗ (i @ (int (u32)))
local_p ◁ₗ (uninit (uintptr_t))
local_ret ◁ₗ ((base.2 + given * PAGE_SIZE) @ (int (uintptr_t)))
((base + given * PAGE_SIZE) ◁ₗ zeroed (PAGES i))
((base + (given + i) * PAGE_SIZE) ◁ₗ uninit (PAGES (Z.to_nat n - i)%nat))
(global_with_type "mem" Own (((base, given + n, remaining - n)%Z) @ (region)))
i n
]> $
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "hyp_early_alloc_contig" "#0".
- repeat liRStep; liShow.
all: print_typesystem_goal "hyp_early_alloc_contig" "#3".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: unfold PAGE_SIZE, PAGE_SHIFT in *; try solve_goal.
all: rewrite -> Z.shiftl_mul_pow2 in *; try lia.
all: try apply: has_layout_loc_trans' => //.
all: rewrite ?ly_offset_PAGES; try solve_goal.
all: transitivity max_alloc_end; last done.
all: etransitivity; last eassumption.
all: rewrite -?Z.add_assoc => //=; apply -> Z.add_le_mono_l; lia.
all: print_sidecondition_goal "hyp_early_alloc_contig".
Qed.
End proof_hyp_early_alloc_contig.
......@@ -23,8 +23,8 @@ Section proof_hyp_early_alloc_nr_pages.
- repeat liRStep; liShow.
all: print_typesystem_goal "hyp_early_alloc_nr_pages" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+ rewrite Z.add_simpl_l /PAGE_SIZE. solve_goal.
+ rewrite /PAGE_SIZE Z.add_simpl_l Z.shiftr_div_pow2 //= Z.div_mul //=.
all: rewrite /PAGE_SIZE Z.add_simpl_l; try solve_goal.
all: rewrite Z.shiftr_div_pow2 //= Z.div_mul //=.
all: print_sidecondition_goal "hyp_early_alloc_nr_pages".
Qed.
End proof_hyp_early_alloc_nr_pages.
......@@ -43,14 +43,39 @@ Instance simpl_loc_extra4 l n1 n2:
SimplLoc (l + (n1 + 0%nat) * n2) (l + (n1 * n2)).
Proof. f_equal. lia. Qed.
Instance simpl_loc_extra5 l n1 n2 n3 n4:
SimplLoc (l + (n1 + (n2 + n3)%nat) * n4) (l + (n1 + n2 + n3) * n4).
Proof. f_equal. lia. Qed.
(*** Things about PAGES ***)
Lemma ly_size_PAGES i : ly_size (PAGES i) = (i * Z.to_nat PAGE_SIZE)%nat.
Proof. by rewrite /PAGES /ly_with_align /ly_size. Qed.
Lemma ly_offset_PAGES n m:
(ly_offset (PAGES n) (ly_size (PAGES m))) = PAGES (n - m).
Proof.
rewrite ly_size_PAGES /ly_offset /PAGES /ly_with_align /ly_size /PAGE_SIZE /=.
f_equal; first lia. rewrite min_l // /factor2 /factor2' /=. case_match => //=.
assert (p = Pos.of_nat m * (2 ^ 12))%positive as ->. { simpl. lia. }
rewrite Pos_factor2_mult Pos_factor2_pow. lia.
Qed.
Global Instance simpl_ly_size_page_le i j:
SimplBothRel ()%nat (PAGES i).(ly_size) (PAGES j).(ly_size) (i j)%nat.
Proof. rewrite /PAGES /ly_with_align /ly_size /PAGE_SIZE /=. split; lia. Qed.
Lemma ly_size_PAGES i : ly_size (PAGES i) = (i * Z.to_nat PAGE_SIZE)%nat.
Proof. by rewrite /PAGES /ly_with_align /ly_size. Qed.
Global Instance simpl_ly_size_page_eq i j:
SimplBothRel (=) (PAGES i).(ly_size) (PAGES j).(ly_size) (i = j).
Proof. rewrite !ly_size_PAGES /PAGE_SIZE. split; lia. Qed.
Global Instance simpl_extra1 k m n:
SimplBoth (k = ly_size (ly_offset (PAGES n) (ly_size (PAGES m)))) (k = ly_size (PAGES (n - m))).
Proof. by rewrite ly_offset_PAGES. Qed.
Global Instance simpl_extra2 k m n:
SimplBoth (ly_size (ly_offset (PAGES n) (ly_size (PAGES m))) = k) (ly_size (PAGES (n - m)) = k).
Proof. by rewrite ly_offset_PAGES. Qed.
Section instances.
Context `{!typeG Σ}.
......@@ -107,41 +132,6 @@ Section instances.
SimplifyHyp ((l + (n1 + (Z.to_nat n2 - 0)%nat) * PAGE_SIZE) ◁ₗ{β} ty) (Some 0%N) :=
λ T, i2p (simplify_hyp_place_PAGE_SIZE_stuff_other l β n1 n2 ty T).
Lemma type_cast_ptr_int_val (v : val) (p : loc) (n : nat) T:
(min_alloc_start p.2 p.2 + n max_alloc_end -
v ◁ᵥ p @ ptr n - T (i2v p.2 size_t) (t2mt (p.2 @ int uintptr_t))) -
typed_un_op v (v ◁ᵥ p @ ptr n) (CastOp (IntOp uintptr_t)) PtrOp T.
Proof.
iIntros "HT Hp" (Φ) "HΦ".
iDestruct "Hp" as "[-> #Hlib]".
iDestruct (loc_in_bounds_in_range_uintptr_t with "Hlib") as %[? H]%val_of_int_is_some.
iDestruct (loc_in_bounds_ptr_in_range with "Hlib") as %?.
iDestruct ("HT" with "[] []") as "HT"; first done. { by iFrame "Hlib". }
iApply wp_cast_ptr_int => //=; first by rewrite val_to_of_loc.
rewrite /i2v H /=. iApply ("HΦ" with "[] [HT]"); last done. done.
Qed.
Global Instance type_cast_ptr_int_val_inst (v : val) (p : loc) n:
TypedUnOp v (v ◁ᵥ p @ ptr n)%I (CastOp (IntOp uintptr_t)) PtrOp :=
λ T, i2p (type_cast_ptr_int_val v p n T).
Lemma subsume_own_ptr p l1 l2 ty n T:
l1 = l2 (l1 ◁ₗ ty - loc_in_bounds l1 n T) -
subsume (p ◁ₗ l1 @ &own ty)%I (p ◁ₗ l2 @ ptr n)%I T.
Proof.
iIntros "[-> HT] Hp".
iDestruct (ty_aligned with "Hp") as %?.
iDestruct (ty_deref with "Hp") as (v) "[Hp [-> Hl]]".
iDestruct ("HT" with "Hl") as "[#Hlib $]".
iFrame "Hp Hlib". done.
Qed.
Global Instance subsume_own_ptr_inst p l1 l2 ty n:
Subsume (p ◁ₗ l1 @ &own ty)%I (p ◁ₗ l2 @ ptr n)%I :=
λ T, i2p (subsume_own_ptr p l1 l2 ty n T).
Global Instance intro_persistent_loc_in_bounds l n:
IntroPersistent (loc_in_bounds l n) (loc_in_bounds l n).
Proof. constructor. by iIntros "#H !>". Qed.
Lemma simplify_hyp_loc_in_bounds_ptr_in_range l (n : nat) T:
(min_alloc_start l.2 l.2 + n max_alloc_end - loc_in_bounds l n - T) -
simplify_hyp (loc_in_bounds l n) T.
......@@ -154,39 +144,7 @@ Section instances.
Global Instance simplify_hyp_loc_in_bounds_ptr_in_range_inst l n `{!TCUnless (FastDone (min_alloc_start l.2))}:
SimplifyHyp (loc_in_bounds l n) (Some 0%N) :=
λ T, i2p (simplify_hyp_loc_in_bounds_ptr_in_range l n T).
Lemma ly_offset_PAGES n m:
(ly_offset (PAGES n) (ly_size (PAGES m))) = PAGES (n - m).
Proof.
rewrite ly_size_PAGES /ly_offset /PAGES /ly_with_align /ly_size /PAGE_SIZE /=.
f_equal; first lia. rewrite min_l // /factor2 /factor2' /=. case_match => //=.
assert (p = Pos.of_nat m * (2 ^ 12))%positive as ->. { simpl. lia. }
rewrite Pos_factor2_mult Pos_factor2_pow. lia.
Qed.
Lemma subsume_zeroed_zeroed_PAGES p n1 n2 (T : iProp Σ) `{!CanSolve (n1 n2)%nat}:
((p + ly_size (PAGES n2)) ◁ₗ zeroed (PAGES (n1 - n2)) - T) -
subsume (p ◁ₗ zeroed (PAGES n1))%I (p ◁ₗ zeroed (PAGES n2))%I T.
Proof.
revert select (CanSolve _) => Hle. unfold CanSolve in Hle.
iIntros "HT Hp".
Admitted.
Global Instance subsume_zeroed_zeroed_PAGES_inst p n1 n2 `{!CanSolve (n1 n2)%nat}:
Subsume (p ◁ₗ zeroed (PAGES n1))%I (p ◁ₗ zeroed (PAGES n2))%I :=
λ T, i2p (subsume_zeroed_zeroed_PAGES p n1 n2 T).
Lemma subsume_zeroed_zeroed_PAGES_lt p n1 n2 (T : iProp Σ) `{!CanSolve (n2 n1)%nat}:
(p + ly_size (PAGES n1)) ◁ₗ zeroed (PAGES (n2 - n1)) T -
subsume (p ◁ₗ zeroed (PAGES n1))%I (p ◁ₗ zeroed (PAGES n2))%I T.
Admitted.
Global Instance subsume_zeroed_zeroed_PAGES_lt_inst p n1 n2 `{!CanSolve (n2 n1)%nat}:
Subsume (p ◁ₗ zeroed (PAGES n1))%I (p ◁ₗ zeroed (PAGES n2))%I :=
λ T, i2p (subsume_zeroed_zeroed_PAGES_lt p n1 n2 T).
End instances.
Typeclasses Opaque FindLocInBounds.
Typeclasses Opaque PAGES.
Global Opaque PAGES.
(* Typeclasses Opaque PAGE_SIZE PAGE_SHIFT. *)
......@@ -427,6 +427,37 @@ Section ptr.
Global Instance simplify_ptr_hyp_val_inst (v : val) (p : loc) n `{!TCUnless (FastDone (v = p))}:
SimplifyHypVal v (p @ ptr n)%I (Some 0%N) :=
λ T, i2p (simplify_ptr_hyp_val v p n T).
Lemma subsume_own_ptr p l1 l2 ty n T:
l1 = l2 (l1 ◁ₗ ty - loc_in_bounds l1 n T) -
subsume (p ◁ₗ l1 @ &own ty)%I (p ◁ₗ l2 @ ptr n)%I T.
Proof.
iIntros "[-> HT] Hp".
iDestruct (ty_aligned with "Hp") as %?.
iDestruct (ty_deref with "Hp") as (v) "[Hp [-> Hl]]".
iDestruct ("HT" with "Hl") as "[#Hlib $]".
iFrame "Hp Hlib". done.
Qed.
Global Instance subsume_own_ptr_inst p l1 l2 ty n:
Subsume (p ◁ₗ l1 @ &own ty)%I (p ◁ₗ l2 @ ptr n)%I :=
λ T, i2p (subsume_own_ptr p l1 l2 ty n T).
Lemma type_cast_ptr_int_val (v : val) (p : loc) (n : nat) T:
(min_alloc_start p.2 p.2 + n max_alloc_end -
v ◁ᵥ p @ ptr n - T (i2v p.2 size_t) (t2mt (p.2 @ int uintptr_t))) -
typed_un_op v (v ◁ᵥ p @ ptr n) (CastOp (IntOp uintptr_t)) PtrOp T.
Proof.
iIntros "HT Hp" (Φ) "HΦ".
iDestruct "Hp" as "[-> #Hlib]".
iDestruct (loc_in_bounds_in_range_uintptr_t with "Hlib") as %[? H]%val_of_int_is_some.
iDestruct (loc_in_bounds_ptr_in_range with "Hlib") as %?.
iDestruct ("HT" with "[] []") as "HT"; first done. { by iFrame "Hlib". }
iApply wp_cast_ptr_int => //=; first by rewrite val_to_of_loc.
rewrite /i2v H /=. iApply ("HΦ" with "[] [HT]"); last done. done.
Qed.
Global Instance type_cast_ptr_int_val_inst (v : val) (p : loc) n:
TypedUnOp v (v ◁ᵥ p @ ptr n)%I (CastOp (IntOp uintptr_t)) PtrOp :=
λ T, i2p (type_cast_ptr_int_val v p n T).
End ptr.
Section null.
......
......@@ -323,6 +323,10 @@ Section loc_in_bounds.
Proof.
constructor. iIntros (?) "?". by iApply movable_loc_in_bounds.
Qed.
Global Instance intro_persistent_loc_in_bounds l n:
IntroPersistent (loc_in_bounds l n) (loc_in_bounds l n).
Proof. constructor. by iIntros "#H !>". Qed.
End loc_in_bounds.
Class AllocAlive `{!typeG Σ} (ty : type) (β : own_state) (P : iProp Σ) := {
......
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