Commit 909c2a19 authored by Michael Sammler's avatar Michael Sammler
Browse files

Updated early alloc example

parent 328a67c1
Pipeline #49754 passed with stage
in 16 minutes and 35 seconds
......@@ -3,27 +3,38 @@
* Copyright (C) 2020 Google LLC
* Author: Quentin Perret <qperret@google.com>
*/
//#include <asm/kvm_pgtable.h>
//
//#include <nvhe/early_alloc.h>
//#include <nvhe/memory.h>
#include <asm/page-def.h>
#include <stddef.h>
#include <stdint.h>
#include <refinedc.h>
//@rc::import instances from refinedc.linux.pkvm.early_alloc (for proofs only)
//struct kvm_pgtable_mm_ops hyp_early_alloc_mm_ops;
//s64 __ro_after_init hyp_physvirt_offset;
//
//static unsigned long base;
//static unsigned long end;
//static unsigned long cur;
struct
[[rc::refined_by("base : loc", "given : Z", "remaining : Z")]]
[[rc::let("z_cur : Z = {(base.2 + given * PAGE_SIZE)%Z}")]]
[[rc::let("z_end : Z = {(base.2 + (given + remaining) * PAGE_SIZE)%Z}")]]
[[rc::constraints("{0 ≤ given}", "{0 ≤ remaining}", "[alloc_global base]",
"{base.2 + (given + remaining) * PAGE_SIZE <= max_int u64}")]]
[[rc::constraints("{0 ≤ given}", "{0 ≤ remaining}", "[alloc_global base]")]]
[[rc::constraints("{base.2 + (given + remaining) * PAGE_SIZE max_int u64}")]]
region {
[[rc::field("z_end @ int<uintptr_t>")]] uintptr_t end;
[[rc::field("z_cur @ int<uintptr_t>")]] uintptr_t cur;
[[rc::field("z_end @ int<u64>")]]
unsigned long end;
[[rc::field("z_cur @ int<u64>")]]
unsigned long cur;
[[rc::field("own_constrained<nonshr_constraint<"
"{(base.1, z_cur) ◁ₗ uninit (PAGES (Z.to_nat remaining))}>, "
"base @ ptr<{Z.to_nat ((given + remaining) * PAGE_SIZE)}>>"
)]] unsigned char* base;
"base @ intptr<u64>>")]]
unsigned long base;
};
static struct region mem;
......@@ -32,21 +43,23 @@ static struct region mem;
#define end (mem.end)
#define cur (mem.cur)
[[rc::parameters("p : loc", "n : Z")]]
[[rc::args("&own<place<p>>", "{0} @ int<u8>", "n @ int<u64>")]]
[[rc::requires("own p : uninit<{ly_with_align (Z.to_nat n) (Z.to_nat PAGE_SIZE)}>")]]
[[rc::ensures("own p : zeroed<{ly_with_align (Z.to_nat n) (Z.to_nat PAGE_SIZE)}>")]]
extern void memset(void *to, unsigned char c, unsigned long size);
[[rc::parameters("base : loc", "given : Z", "remaining : Z")]]
[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
[[rc::returns("given @ int<size_t>")]]
[[rc::ensures("global mem : {(base, given, remaining)} @ region")]]
[[rc::tactics("all: rewrite 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;
unsigned long hyp_early_alloc_nr_used_pages(void)
{
return (cur - base) >> PAGE_SHIFT;
}
[[rc::parameters("p : loc")]]
[[rc::args("p @ &own<uninit<PAGE>>")]]
[[rc::ensures("own p : zeroed<PAGE>")]]
extern void clear_page(void *to);
[[rc::parameters("base : loc", "given : Z", "remaining : Z", "n : Z")]]
[[rc::args("n @ int<u32>")]]
[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
......@@ -55,56 +68,48 @@ extern void clear_page(void *to);
[[rc::ensures("global mem : {(base, given + n, remaining - n)%Z} @ region")]]
[[rc::tactics("all: try rewrite -> Z.shiftl_mul_pow2 in *; try lia.")]]
[[rc::tactics("all: rewrite ?ly_offset_PAGES; try solve_goal.")]]
void *hyp_early_alloc_contig(unsigned int nr_pages){
uintptr_t ret = cur, p;
unsigned int i;
void *hyp_early_alloc_contig(unsigned int nr_pages)
{
unsigned long size = (nr_pages << PAGE_SHIFT);
void *ret = copy_alloc_id(cur, (void*) base);
if (!nr_pages)
return NULL;
rc_unfold(base);
cur += nr_pages << PAGE_SHIFT;
if (cur > end) {
cur = ret;
if (end - cur < size)
return NULL;
}
[[rc::exists("i : nat")]]
[[rc::inv_vars("i: i @ int<u32>")]]
[[rc::inv_vars("p: uninit<uintptr_t>")]]
[[rc::inv_vars("ret: {base.2 + given * PAGE_SIZE} @ int<uintptr_t>")]]
[[rc::constraints("[(base +ₗ given * PAGE_SIZE) ◁ₗ zeroed (PAGES i)]")]]
[[rc::constraints("[(base +ₗ (given + i) * PAGE_SIZE) ◁ₗ uninit (PAGES (Z.to_nat n - i)%nat)]")]]
[[rc::constraints("global mem : {(base, given + n, remaining - n)%Z} @ region")]]
[[rc::constraints("{i ≤ n}", "{0 ≤ given}")]]
for (i = 0; i < nr_pages; i++) {
rc_unfold(base);
p = ret + (i << PAGE_SHIFT);
clear_page(copy_alloc_id(p, base));
}
cur += size;
memset(ret, 0, size);
return copy_alloc_id(ret, base);
return ret;
}
[[rc::parameters("base : loc", "given : Z", "remaining : Z")]]
[[rc::args("uninit<void*>")]]
[[rc::requires("global mem : {(base, given, remaining)} @ region")]]
[[rc::requires("{0 remaining}")]]
[[rc::requires("{0 < remaining}")]]
[[rc::returns("&own<zeroed<PAGE>>")]]
[[rc::ensures("global mem : {(base, given + 1, remaining - 1)} @ region")]]
void *hyp_early_alloc_page(void *arg){
rc_unfold(base);
void *hyp_early_alloc_page(void *arg)
{
return hyp_early_alloc_contig(1);
}
[[rc::parameters("l : loc", "n : Z", "s : Z")]]
[[rc::args("l @ &own<uninit<PAGES<{Z.to_nat n}>>>", "s @ int<u32>")]]
[[rc::args("l @ &own<uninit<PAGES<{Z.to_nat n}>>>", "s @ int<u64>")]]
[[rc::requires("{s = (n * PAGE_SIZE)%Z}", "[alloc_global l]")]]
[[rc::requires("global mem : uninit<struct_region>")]]
[[rc::ensures("global mem : {(l, 0, n)} @ region")]]
[[rc::tactics("all: rewrite -> ly_size_PAGES in *; solve_goal.")]]
void hyp_early_alloc_init(unsigned char* virt, unsigned int size){
base = virt;
end = (uintptr_t) ((uintptr_t) virt + size);
cur = (uintptr_t) virt;
void hyp_early_alloc_init(void *virt, unsigned long size)
{
//base = cur = (unsigned long)virt;
base = (unsigned long)virt;
cur = base;
end = base + size;
//hyp_early_alloc_mm_ops.zalloc_page = hyp_early_alloc_page;
//hyp_early_alloc_mm_ops.phys_to_virt = hyp_phys_to_virt;
//hyp_early_alloc_mm_ops.virt_to_phys = hyp_virt_to_phys;
}
......@@ -9,34 +9,20 @@ 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) :
Lemma type_hyp_early_alloc_contig (global_mem global_memset : 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.
global_memset ◁ᵥ global_memset @ function_ptr type_of_memset -
typed_function (impl_hyp_early_alloc_contig global_mem global_memset) 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.
start_function "hyp_early_alloc_contig" ([[[base given] remaining] n]) => arg_nr_pages local_size local_ret.
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
0 given
]> $
)%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: try rewrite -> Z.shiftl_mul_pow2 in *; try lia.
all: rewrite ?ly_offset_PAGES; try solve_goal.
......
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.
Set Default Proof Using "Type".
(* Generated from [linux/pkvm/early_alloc.c]. *)
Section proof_hyp_early_alloc_init.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [hyp_early_alloc_init]. *)
Lemma type_hyp_early_alloc_init (global_mem : loc) :
global_locs !! "mem" = Some global_mem →
⊢ typed_function (impl_hyp_early_alloc_init global_mem) type_of_hyp_early_alloc_init.
Proof.
Open Scope printing_sugar.
start_function "hyp_early_alloc_init" ([[l n] s]) => arg_virt arg_size.
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
liInst Hevar0 l.2. assert ((l.1, l.2) = l) as -> by by destruct l.
repeat liRStep; liShow.
all: print_typesystem_goal "hyp_early_alloc_init" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+ by etransitivity.
+ transitivity max_alloc_end; last done.
rewrite /ly_size /= in H1. lia.
all: print_sidecondition_goal "hyp_early_alloc_init".
Qed.
End proof_hyp_early_alloc_init.
......@@ -5,26 +5,26 @@ 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_nr_pages.
Section proof_hyp_early_alloc_nr_used_pages.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [hyp_early_alloc_nr_pages]. *)
Lemma type_hyp_early_alloc_nr_pages (global_mem : loc) :
(* Typing proof for [hyp_early_alloc_nr_used_pages]. *)
Lemma type_hyp_early_alloc_nr_used_pages (global_mem : loc) :
global_locs !! "mem" = Some global_mem
typed_function (impl_hyp_early_alloc_nr_pages global_mem) type_of_hyp_early_alloc_nr_pages.
typed_function (impl_hyp_early_alloc_nr_used_pages global_mem) type_of_hyp_early_alloc_nr_used_pages.
Proof.
Open Scope printing_sugar.
start_function "hyp_early_alloc_nr_pages" ([[base given] remaining]).
start_function "hyp_early_alloc_nr_used_pages" ([[base given] remaining]).
split_blocks ((
)%I : gmap label (iProp Σ)) ((
)%I : gmap label (iProp Σ)).
- repeat liRStep; liShow.
all: print_typesystem_goal "hyp_early_alloc_nr_pages" "#0".
all: print_typesystem_goal "hyp_early_alloc_nr_used_pages" "#0".
Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
all: rewrite 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".
all: print_sidecondition_goal "hyp_early_alloc_nr_used_pages".
Qed.
End proof_hyp_early_alloc_nr_pages.
End proof_hyp_early_alloc_nr_used_pages.
......@@ -9,10 +9,9 @@ Section proof_hyp_early_alloc_page.
Context `{!typeG Σ} `{!globalG Σ}.
(* Typing proof for [hyp_early_alloc_page]. *)
Lemma type_hyp_early_alloc_page (global_mem global_hyp_early_alloc_contig : loc) :
global_locs !! "mem" = Some global_mem
Lemma type_hyp_early_alloc_page (global_hyp_early_alloc_contig : loc) :
global_hyp_early_alloc_contig ◁ᵥ global_hyp_early_alloc_contig @ function_ptr type_of_hyp_early_alloc_contig -
typed_function (impl_hyp_early_alloc_page global_mem global_hyp_early_alloc_contig) type_of_hyp_early_alloc_page.
typed_function (impl_hyp_early_alloc_page global_hyp_early_alloc_contig) type_of_hyp_early_alloc_page.
Proof.
Open Scope printing_sugar.
start_function "hyp_early_alloc_page" ([[base given] remaining]) => arg_arg.
......
......@@ -25,14 +25,14 @@ Section spec.
let z_cur : Z := (base.2 + given * PAGE_SIZE)%Z in
let z_end : Z := (base.2 + (given + remaining) * PAGE_SIZE)%Z in
constrained (struct struct_region [@{type}
(z_end @ (int (uintptr_t))) ;
(z_cur @ (int (uintptr_t))) ;
(own_constrained (nonshr_constraint ((base.1, z_cur) ◁ₗ uninit (PAGES (Z.to_nat remaining)))) (base @ (ptr (Z.to_nat ((given + remaining) * PAGE_SIZE)))))
(z_end @ (int (u64))) ;
(z_cur @ (int (u64))) ;
(own_constrained (nonshr_constraint ((base.1, z_cur) ◁ₗ uninit (PAGES (Z.to_nat remaining)))) (base @ (intptr (u64))))
]) (
0 given
0 remaining
(alloc_global base)
base.2 + (given + remaining) * PAGE_SIZE <= max_int u64
base.2 + (given + remaining) * PAGE_SIZE max_int u64
)
)%I.
Typeclasses Opaque region_rec.
......@@ -53,14 +53,14 @@ Section spec.
let z_cur : Z := (base.2 + given * PAGE_SIZE)%Z in
let z_end : Z := (base.2 + (given + remaining) * PAGE_SIZE)%Z in
constrained (struct struct_region [@{type}
(z_end @ (int (uintptr_t))) ;
(z_cur @ (int (uintptr_t))) ;
(own_constrained (nonshr_constraint ((base.1, z_cur) ◁ₗ uninit (PAGES (Z.to_nat remaining)))) (base @ (ptr (Z.to_nat ((given + remaining) * PAGE_SIZE)))))
(z_end @ (int (u64))) ;
(z_cur @ (int (u64))) ;
(own_constrained (nonshr_constraint ((base.1, z_cur) ◁ₗ uninit (PAGES (Z.to_nat remaining)))) (base @ (intptr (u64))))
]) (
0 given
0 remaining
(alloc_global base)
base.2 + (given + remaining) * PAGE_SIZE <= max_int u64
base.2 + (given + remaining) * PAGE_SIZE max_int u64
)
)%I.
Proof. by rewrite {1}/with_refinement/=fixp_unfold. Qed.
......@@ -88,16 +88,16 @@ Section spec.
(* Type definitions. *)
(* Specifications for function [hyp_early_alloc_nr_pages]. *)
Definition type_of_hyp_early_alloc_nr_pages :=
(* Specifications for function [memset]. *)
Definition type_of_memset :=
fn( (p, n) : loc * Z; (&own (place (p))), ((0) @ (int (u8))), (n @ (int (u64))); (p ◁ₗ (uninit (ly_with_align (Z.to_nat n) (Z.to_nat PAGE_SIZE)))))
() : (), (void); (p ◁ₗ (zeroed (ly_with_align (Z.to_nat n) (Z.to_nat PAGE_SIZE)))).
(* Specifications for function [hyp_early_alloc_nr_used_pages]. *)
Definition type_of_hyp_early_alloc_nr_used_pages :=
fn( (base, given, remaining) : loc * Z * Z; (global_with_type "mem" Own (((base, given, remaining)) @ (region))))
() : (), (given @ (int (size_t))); (global_with_type "mem" Own (((base, given, remaining)) @ (region))).
(* Specifications for function [clear_page]. *)
Definition type_of_clear_page :=
fn( p : loc; (p @ (&own (uninit (PAGE)))); True)
() : (), (void); (p ◁ₗ (zeroed (PAGE))).
(* Specifications for function [hyp_early_alloc_contig]. *)
Definition type_of_hyp_early_alloc_contig :=
fn( (base, given, remaining, n) : loc * Z * Z * Z; (n @ (int (u32))); (global_with_type "mem" Own (((base, given, remaining)) @ (region))) 0 < n remaining n PAGE_SHIFT max_int u32)
......@@ -105,12 +105,12 @@ Section spec.
(* Specifications for function [hyp_early_alloc_page]. *)
Definition type_of_hyp_early_alloc_page :=
fn( (base, given, remaining) : loc * Z * Z; (uninit (void*)); (global_with_type "mem" Own (((base, given, remaining)) @ (region))) 0 remaining)
fn( (base, given, remaining) : loc * Z * Z; (uninit (void*)); (global_with_type "mem" Own (((base, given, remaining)) @ (region))) 0 < remaining)
() : (), (&own (zeroed (PAGE))); (global_with_type "mem" Own (((base, given + 1, remaining - 1)) @ (region))).
(* Specifications for function [hyp_early_alloc_init]. *)
Definition type_of_hyp_early_alloc_init :=
fn( (l, n, s) : loc * Z * Z; (l @ (&own (uninit (PAGES (Z.to_nat n))))), (s @ (int (u32))); s = (n * PAGE_SIZE)%Z (alloc_global l) (global_with_type "mem" Own (uninit (struct_region))))
fn( (l, n, s) : loc * Z * Z; (l @ (&own (uninit (PAGES (Z.to_nat n))))), (s @ (int (u64))); s = (n * PAGE_SIZE)%Z (alloc_global l) (global_with_type "mem" Own (uninit (struct_region))))
() : (), (void); (global_with_type "mem" Own (((l, 0, n)) @ (region))).
End spec.
......
......@@ -2,6 +2,11 @@ From refinedc.typing Require Import typing.
From refinedc.linux.pkvm.early_alloc Require Import generated_spec.
Set Default Proof Using "Type".
Lemma shift_12_eq_mul_4096 n :
(n 12) = n * 4096.
Proof. by rewrite Z.shiftl_mul_pow2. Qed.
Hint Rewrite shift_12_eq_mul_4096 : lithium_rewrite.
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.
......
generated_proof_clear_page.v
generated_proof_hyp_early_alloc_contig.v
generated_proof_hyp_early_alloc_init.v
generated_proof_hyp_early_alloc_nr_pages.v
generated_proof_hyp_early_alloc_nr_used_pages.v
generated_proof_hyp_early_alloc_page.v
generated_proof_memset.v
......@@ -26,6 +26,7 @@ Arguments N.shiftl : simpl never.
Arguments N.shiftr : simpl never.
Arguments Pos.shiftl : simpl never.
Arguments Pos.shiftr : simpl never.
Global Opaque Z.shiftl Z.shiftr.
Notation "'[@{' A '}' x ; y ; .. ; z ]" := (@cons A x (@cons A y .. (@cons A z (@nil A)) ..)) (only parsing) : list_scope.
Notation "'[@{' A '}' x ]" := (@cons A x nil) (only parsing) : list_scope.
......
......@@ -40,6 +40,14 @@ Section own_constrained.
constructor. iIntros (l) "[Hl _]". by iApply loc_in_bounds_in_bounds.
Qed.
Lemma copy_as_own_constrained l β P `{!OwnConstraint P} ty {HC: CopyAs l β ty} T:
(P β - (HC T).(i2p_P)) - copy_as l β (own_constrained P ty) T.
Proof.
iIntros "HT [Hty HP]". iDestruct (i2p_proof with "(HT HP)") as "HT". by iApply "HT".
Qed.
Global Instance copy_as_own_constrained_inst l β P `{!OwnConstraint P} ty {HC: CopyAs l β ty}:
CopyAs l β (own_constrained P ty) := λ T, i2p (copy_as_own_constrained l β P ty T).
Lemma simplify_hyp_place_own_constrained P l β ty T `{!OwnConstraint P}:
(P β - l ◁ₗ{β} ty - T) - simplify_hyp (l◁ₗ{β} own_constrained P ty) T.
Proof. iIntros "HT [Hl HP]". by iApply ("HT" with "HP"). Qed.
......
......@@ -480,7 +480,7 @@ Section optionalO.
all: iExists _, _; iFrame.
Qed.
End optionalO.
Notation "optionalO< ty , optty >" := (optional ty optty)
Notation "optionalO< ty , optty >" := (optionalO ty optty)
(only printing, format "'optionalO<' ty , optty '>'") : printing_sugar.
Section int_optional.
......
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