Commit 72a909ed authored by Paul's avatar Paul
Browse files

failure attempt

parent 1011b46c
Pipeline #58244 canceled with stage
in 25 seconds
......@@ -41,7 +41,7 @@ typedef u64 kvm_pgtable_prot;
* @phys_to_virt: Convert a physical address into a virtual address.
* @virt_to_phys: Convert a virtual address into a physical address.
*/
struct [[rc::refined_by("mm_ops : mm_callbacks")]] kvm_pgtable_mm_ops {
struct [[rc::refined_by("mm_ops : mm_callbacks", "s : stage")]] kvm_pgtable_mm_ops {
// void* (*zalloc_page)(void *arg);
// void* (*zalloc_pages_exact)(size_t size);
// void (*free_pages_exact)(void *addr, size_t size);
......@@ -49,7 +49,7 @@ struct [[rc::refined_by("mm_ops : mm_callbacks")]] kvm_pgtable_mm_ops {
// void (*put_page)(void *addr);
// int (*page_count)(void *addr);
// void* (*phys_to_virt)(phys_addr_t phys);
[[rc::field("function_ptr<{fn(∀ (p, a) : loc * Z; p @ &own (a @ int u64); True) → ∃ () : (), (mm_ops.(virt_to_phys) a) @ bitfield Pte; True}>")]]
[[rc::field("function_ptr<{fn(∀ (p, a) : loc * Z; p @ &own (a @ int u64); True) → ∃ () : (), (virt_to_phys mm_ops a s) @ bitfield (Pte s); True}>")]]
phys_addr_t (*virt_to_phys)(void *addr);
};
......@@ -86,52 +86,11 @@ struct [[rc::refined_by("mm_ops : mm_callbacks")]] kvm_pgtable_mm_ops {
#define KVM_PTE_LEAF_ATTR_HI_S1_XN BIT(54)
// #define KVM_PTE_LEAF_ATTR_HI_S2_XN BIT(54)
//@rc::bitfields Pte as u64
//@ pte_valid : bool[0]
//@ pte_type : integer[1]
//@ pte_leaf_attr_lo: integer[2 ..11]
//@ pte_addr : integer[12..47]
//@ pte_undef : integer[48..50]
//@ pte_leaf_attr_hi: integer[51..63]
//@rc::end
//@rc::import pgtable_lemmas from refinedc.linux.casestudies.pgtable
//@rc::bitfields Attr as u64
//@ attr_lo_s1_attridx : integer[2..4]
//@ attr_lo_s1_ap : integer[6..7]
//@ attr_lo_s1_sh : integer[8..9]
//@ attr_lo_s1_af : bool[10]
//@ attr_hi_s1_xn : bool[54]
//@rc::end
//@rc::bitfields Prot as u64
//@ prot_x : bool[0]
//@ prot_w : bool[1]
//@ prot_r : bool[2]
//@ prot_device : bool[3]
//@rc::end
//@rc::inlined_prelude
//@Definition pte_from_addr (pa : Pte) : Pte :=
//@ zero_Pte <| pte_addr := pte_addr pa |>.
//@
//@Record mm_callbacks := {
//@ virt_to_phys : Z → Pte;
//@}.
//@
//@Definition max_level : Z := 4.
//@Definition mtype_device : Z := 5.
//@Definition mtype_normal : Z := 0.
//@Definition pte_type_block : Z := 0.
//@Definition pte_type_page : Z := 1.
//@Definition pte_type_table : Z := 1.
//@Definition ap_rw : Z := 1.
//@Definition ap_ro : Z := 3.
//@Definition sh_is : Z := 3.
//@Definition err_code : Z := 22.
//@rc::end
[[rc::parameters("pte : Pte")]]
[[rc::args("pte @ bitfield<Pte>")]]
[[rc::parameters("s : stage")]]
[[rc::parameters("pte : {Pte s}")]]
[[rc::args("pte @ bitfield<{Pte s}>")]]
[[rc::requires("{bitfield_wf pte}")]]
[[rc::returns("{pte_valid pte} @ boolean<bool_it>")]]
static bool kvm_pte_valid(kvm_pte_t pte)
......@@ -140,127 +99,127 @@ static bool kvm_pte_valid(kvm_pte_t pte)
return 0 != (pte & KVM_PTE_VALID);
}
[[rc::parameters("pte : Pte", "level : Z")]]
[[rc::args("pte @ bitfield<Pte>", "level @ int<u32>")]]
[[rc::requires("{bitfield_wf pte}")]]
[[rc::returns("{if bool_decide (level = max_level - 1) then false \
else if negb (pte_valid pte) then false \
else bool_decide (pte_type pte = pte_type_table)} @ boolean<bool_it>")]]
static bool kvm_pte_table(kvm_pte_t pte, u32 level)
{
if (level == KVM_PGTABLE_MAX_LEVELS - 1)
return false;
if (!kvm_pte_valid(pte))
return false;
return FIELD_GET(KVM_PTE_TYPE, pte) == KVM_PTE_TYPE_TABLE;
}
[[rc::parameters("pte : Pte", "p : loc")]]
[[rc::args("p @ &own<pte @ bitfield<Pte>>")]]
[[rc::requires("{bitfield_wf pte}")]]
[[rc::ensures("own p : {pte <| pte_valid := false |>} @ bitfield<Pte>")]]
static void kvm_set_invalid_pte(kvm_pte_t *ptep)
{
kvm_pte_t pte = *ptep;
WRITE_ONCE(*ptep, pte & ~KVM_PTE_VALID);
}
[[rc::inlined]]
static kvm_pte_t kvm_phys_to_pte(u64 pa)
{
kvm_pte_t pte = pa & KVM_PTE_ADDR_MASK;
if (PAGE_SHIFT == 16) // always false given PAGE_SHIFT == 12
pte |= FIELD_PREP(KVM_PTE_ADDR_51_48, pa >> 48);
return pte;
}
[[rc::parameters("p : loc", "q : loc", "o : loc", "pte : Pte", "va : Z", "mm_ops : mm_callbacks")]]
[[rc::args("p @ &own<pte @ bitfield<Pte>>", "q @ &own<va @ int<u64>>",
"o @ &own<mm_ops @ kvm_pgtable_mm_ops>")]]
[[rc::requires("{bitfield_wf pte}", "{pte_valid pte}")]]
[[rc::ensures("own p : {(pte_from_addr (mm_ops.(virt_to_phys) va)) <| pte_type := pte_type_table |>"
"<| pte_valid := true |>} @ bitfield<Pte>")]]
static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
struct kvm_pgtable_mm_ops *mm_ops)
{
kvm_pte_t old = *ptep, pte = kvm_phys_to_pte(mm_ops->virt_to_phys(childp));
pte |= FIELD_PREP(KVM_PTE_TYPE, KVM_PTE_TYPE_TABLE);
pte |= KVM_PTE_VALID;
WARN_ON(kvm_pte_valid(old));
// smp_store_release(ptep, pte);
*ptep = pte;
}
[[rc::parameters("p : loc", "pte : Pte", "pa : Pte", "attr : Pte", "level : Z", "type : Z", "pte1 : Pte")]]
[[rc::args("p @ &own<pte @ bitfield<Pte>>", "pa @ bitfield<Pte>", "attr @ bitfield<Pte>", "level @ int<u32>")]]
[[rc::requires("{bitfield_wf pte}", "{bitfield_wf pa}", "{bitfield_wf attr}")]]
[[rc::requires("{type = (if bool_decide (level = max_level - 1) then pte_type_page else pte_type_block)}")]]
[[rc::requires("{pte1 = (pte_from_addr pa) <| pte_valid := true |> <| pte_type := type |>"
"<| pte_leaf_attr_lo := pte_leaf_attr_lo attr |> <| pte_leaf_attr_hi := pte_leaf_attr_hi attr |>}")]]
[[rc::returns("{if pte_valid pte then bf_eqb (bitfield_repr pte) (bitfield_repr pte1) bitfield_it else true} @ boolean<bool_it>")]]
[[rc::ensures("own p : {if pte_valid pte then pte else pte1} @ bitfield<Pte>")]]
static bool kvm_set_valid_leaf_pte(kvm_pte_t *ptep, u64 pa, kvm_pte_t attr,
u32 level)
{
kvm_pte_t old = *ptep, pte = kvm_phys_to_pte(pa);
u64 type = (level == KVM_PGTABLE_MAX_LEVELS - 1) ? KVM_PTE_TYPE_PAGE :
KVM_PTE_TYPE_BLOCK;
pte |= attr & (KVM_PTE_LEAF_ATTR_LO | KVM_PTE_LEAF_ATTR_HI);
pte |= FIELD_PREP(KVM_PTE_TYPE, type);
pte |= KVM_PTE_VALID;
/* Tolerate KVM recreating the exact same mapping. */
if (kvm_pte_valid(old))
return old == pte;
// smp_store_release(ptep, pte);
*ptep = pte;
return true;
}
struct [[rc::refined_by("phys : Z", "attr : Attr", "mm_ops : mm_callbacks", "o : loc")]] hyp_map_data {
[[rc::field("phys @ int<u64>")]]
u64 phys;
[[rc::field("attr @ bitfield<Attr>")]]
kvm_pte_t attr;
[[rc::field("o @ &own<mm_ops @ kvm_pgtable_mm_ops>")]]
struct kvm_pgtable_mm_ops *mm_ops;
};
// [[rc::parameters("pte : Pte", "level : Z")]]
// [[rc::args("pte @ bitfield<Pte>", "level @ int<u32>")]]
// [[rc::requires("{bitfield_wf pte}")]]
// [[rc::returns("{if bool_decide (level = max_level - 1) then false \
// else if negb (pte_valid pte) then false \
// else bool_decide (pte_type pte = pte_type_table)} @ boolean<bool_it>")]]
// static bool kvm_pte_table(kvm_pte_t pte, u32 level)
// {
// if (level == KVM_PGTABLE_MAX_LEVELS - 1)
// return false;
// if (!kvm_pte_valid(pte))
// return false;
// return FIELD_GET(KVM_PTE_TYPE, pte) == KVM_PTE_TYPE_TABLE;
// }
// [[rc::parameters("pte : Pte", "p : loc")]]
// [[rc::args("p @ &own<pte @ bitfield<Pte>>")]]
// [[rc::requires("{bitfield_wf pte}")]]
// [[rc::ensures("own p : {pte <| pte_valid := false |>} @ bitfield<Pte>")]]
// static void kvm_set_invalid_pte(kvm_pte_t *ptep)
// {
// kvm_pte_t pte = *ptep;
// WRITE_ONCE(*ptep, pte & ~KVM_PTE_VALID);
// }
// [[rc::inlined]]
// static kvm_pte_t kvm_phys_to_pte(u64 pa)
// {
// kvm_pte_t pte = pa & KVM_PTE_ADDR_MASK;
// if (PAGE_SHIFT == 16) // always false given PAGE_SHIFT == 12
// pte |= FIELD_PREP(KVM_PTE_ADDR_51_48, pa >> 48);
// return pte;
// }
// [[rc::parameters("p : loc", "q : loc", "o : loc", "pte : Pte", "va : Z", "mm_ops : mm_callbacks")]]
// [[rc::args("p @ &own<pte @ bitfield<Pte>>", "q @ &own<va @ int<u64>>",
// "o @ &own<mm_ops @ kvm_pgtable_mm_ops>")]]
// [[rc::requires("{bitfield_wf pte}", "{pte_valid pte}")]]
// [[rc::ensures("own p : {(pte_from_addr (mm_ops.(virt_to_phys) va)) <| pte_type := pte_type_table |>"
// "<| pte_valid := true |>} @ bitfield<Pte>")]]
// static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
// struct kvm_pgtable_mm_ops *mm_ops)
// {
// kvm_pte_t old = *ptep, pte = kvm_phys_to_pte(mm_ops->virt_to_phys(childp));
// pte |= FIELD_PREP(KVM_PTE_TYPE, KVM_PTE_TYPE_TABLE);
// pte |= KVM_PTE_VALID;
// WARN_ON(kvm_pte_valid(old));
// // smp_store_release(ptep, pte);
// *ptep = pte;
// }
// [[rc::parameters("p : loc", "pte : Pte", "pa : Pte", "attr : Pte", "level : Z", "type : Z", "pte1 : Pte")]]
// [[rc::args("p @ &own<pte @ bitfield<Pte>>", "pa @ bitfield<Pte>", "attr @ bitfield<Pte>", "level @ int<u32>")]]
// [[rc::requires("{bitfield_wf pte}", "{bitfield_wf pa}", "{bitfield_wf attr}")]]
// [[rc::requires("{type = (if bool_decide (level = max_level - 1) then pte_type_page else pte_type_block)}")]]
// [[rc::requires("{pte1 = (pte_from_addr pa) <| pte_valid := true |> <| pte_type := type |>"
// "<| pte_leaf_attr_lo := pte_leaf_attr_lo attr |> <| pte_leaf_attr_hi := pte_leaf_attr_hi attr |>}")]]
// [[rc::returns("{if pte_valid pte then bf_eqb (bitfield_repr pte) (bitfield_repr pte1) bitfield_it else true} @ boolean<bool_it>")]]
// [[rc::ensures("own p : {if pte_valid pte then pte else pte1} @ bitfield<Pte>")]]
// static bool kvm_set_valid_leaf_pte(kvm_pte_t *ptep, u64 pa, kvm_pte_t attr,
// u32 level)
// {
// kvm_pte_t old = *ptep, pte = kvm_phys_to_pte(pa);
// u64 type = (level == KVM_PGTABLE_MAX_LEVELS - 1) ? KVM_PTE_TYPE_PAGE :
// KVM_PTE_TYPE_BLOCK;
// pte |= attr & (KVM_PTE_LEAF_ATTR_LO | KVM_PTE_LEAF_ATTR_HI);
// pte |= FIELD_PREP(KVM_PTE_TYPE, type);
// pte |= KVM_PTE_VALID;
// /* Tolerate KVM recreating the exact same mapping. */
// if (kvm_pte_valid(old))
// return old == pte;
// // smp_store_release(ptep, pte);
// *ptep = pte;
// return true;
// }
// struct [[rc::refined_by("phys : Z", "attr : Attr", "mm_ops : mm_callbacks", "o : loc")]] hyp_map_data {
// [[rc::field("phys @ int<u64>")]]
// u64 phys;
// [[rc::field("attr @ bitfield<Attr>")]]
// kvm_pte_t attr;
// [[rc::field("o @ &own<mm_ops @ kvm_pgtable_mm_ops>")]]
// struct kvm_pgtable_mm_ops *mm_ops;
// };
[[rc::parameters("prot : Prot", "phys : Z", "a : Attr", "attr : Attr",
"mtype : Z", "ap : Z", "xn : bool", "err : bool",
"mm_ops : mm_callbacks", "o : loc", "d : loc")]]
[[rc::args("prot @ bitfield<Prot>", "d @ &own<{(phys, a, mm_ops, o)} @ hyp_map_data>")]]
[[rc::requires("{bitfield_wf prot}")]]
[[rc::requires("{mtype = (if prot_device prot then mtype_device else mtype_normal)}")]]
[[rc::requires("{ap = (if prot_w prot then ap_rw else ap_ro)}")]]
[[rc::requires("{xn = negb (prot_x prot)}")]]
[[rc::requires("{err = negb (prot_r prot) || (prot_x prot && (prot_w prot || prot_device prot))}")]]
[[rc::requires("{attr = {| attr_lo_s1_attridx := mtype; attr_lo_s1_ap := ap; attr_lo_s1_sh := sh_is; attr_lo_s1_af := true; attr_hi_s1_xn := xn |} }")]]
[[rc::returns("{if err then -err_code else 0} @ int<i32>")]]
[[rc::ensures("own d : {if err then (phys, a, mm_ops, o) else (phys, attr, mm_ops, o)} @ hyp_map_data")]]
static int hyp_map_set_prot_attr(kvm_pgtable_prot prot, struct hyp_map_data *data)
{
// TODO: remove 0 != once issue #45 is fixed
bool device = 0 != (prot & KVM_PGTABLE_PROT_DEVICE);
u32 mtype = device ? MT_DEVICE_nGnRE : MT_NORMAL;
kvm_pte_t attr = FIELD_PREP(KVM_PTE_LEAF_ATTR_LO_S1_ATTRIDX, mtype);
u32 sh = KVM_PTE_LEAF_ATTR_LO_S1_SH_IS;
u32 ap = (prot & KVM_PGTABLE_PROT_W) ? KVM_PTE_LEAF_ATTR_LO_S1_AP_RW :
KVM_PTE_LEAF_ATTR_LO_S1_AP_RO;
if (!(prot & KVM_PGTABLE_PROT_R))
return -EINVAL;
if (prot & KVM_PGTABLE_PROT_X) {
if (prot & KVM_PGTABLE_PROT_W)
return -EINVAL;
if (device)
return -EINVAL;
} else {
attr |= KVM_PTE_LEAF_ATTR_HI_S1_XN;
}
attr |= FIELD_PREP(KVM_PTE_LEAF_ATTR_LO_S1_AP, ap);
attr |= FIELD_PREP(KVM_PTE_LEAF_ATTR_LO_S1_SH, sh);
attr |= KVM_PTE_LEAF_ATTR_LO_S1_AF;
data->attr = attr;
return 0;
}
// [[rc::parameters("prot : Prot", "phys : Z", "a : Attr", "attr : Attr",
// "mtype : Z", "ap : Z", "xn : bool", "err : bool",
// "mm_ops : mm_callbacks", "o : loc", "d : loc")]]
// [[rc::args("prot @ bitfield<Prot>", "d @ &own<{(phys, a, mm_ops, o)} @ hyp_map_data>")]]
// [[rc::requires("{bitfield_wf prot}")]]
// [[rc::requires("{mtype = (if prot_device prot then mtype_device else mtype_normal)}")]]
// [[rc::requires("{ap = (if prot_w prot then ap_rw else ap_ro)}")]]
// [[rc::requires("{xn = negb (prot_x prot)}")]]
// [[rc::requires("{err = negb (prot_r prot) || (prot_x prot && (prot_w prot || prot_device prot))}")]]
// [[rc::requires("{attr = {| attr_lo_s1_attridx := mtype; attr_lo_s1_ap := ap; attr_lo_s1_sh := sh_is; attr_lo_s1_af := true; attr_hi_s1_xn := xn |} }")]]
// [[rc::returns("{if err then -err_code else 0} @ int<i32>")]]
// [[rc::ensures("own d : {if err then (phys, a, mm_ops, o) else (phys, attr, mm_ops, o)} @ hyp_map_data")]]
// static int hyp_map_set_prot_attr(kvm_pgtable_prot prot, struct hyp_map_data *data)
// {
// // TODO: remove 0 != once issue #45 is fixed
// bool device = 0 != (prot & KVM_PGTABLE_PROT_DEVICE);
// u32 mtype = device ? MT_DEVICE_nGnRE : MT_NORMAL;
// kvm_pte_t attr = FIELD_PREP(KVM_PTE_LEAF_ATTR_LO_S1_ATTRIDX, mtype);
// u32 sh = KVM_PTE_LEAF_ATTR_LO_S1_SH_IS;
// u32 ap = (prot & KVM_PGTABLE_PROT_W) ? KVM_PTE_LEAF_ATTR_LO_S1_AP_RW :
// KVM_PTE_LEAF_ATTR_LO_S1_AP_RO;
// if (!(prot & KVM_PGTABLE_PROT_R))
// return -EINVAL;
// if (prot & KVM_PGTABLE_PROT_X) {
// if (prot & KVM_PGTABLE_PROT_W)
// return -EINVAL;
// if (device)
// return -EINVAL;
// } else {
// attr |= KVM_PTE_LEAF_ATTR_HI_S1_XN;
// }
// attr |= FIELD_PREP(KVM_PTE_LEAF_ATTR_LO_S1_AP, ap);
// attr |= FIELD_PREP(KVM_PTE_LEAF_ATTR_LO_S1_SH, sh);
// attr |= KVM_PTE_LEAF_ATTR_LO_S1_AF;
// data->attr = attr;
// return 0;
// }
From refinedc.typing Require Import typing.
From refinedc.lang Require Import builtins_specs.
Set Default Proof Using "Type".
(* S1 specific *)
Record Pte_S1_attr_lo := {
attr_lo_s1_attridx : Z;
attr_lo_s1_ap : Z;
attr_lo_s1_sh : Z;
attr_lo_s1_af : bool;
}.
Definition Pte_S1_attr_lo_ctm (r : Pte_S1_attr_lo) : ctm := [
(range_of 2 3, fv_int $ attr_lo_s1_attridx r);
(range_of 6 2, fv_int $ attr_lo_s1_ap r);
(range_of 8 2, fv_int $ attr_lo_s1_sh r);
(range_of 10 1, fv_bool $ attr_lo_s1_af r)
].
Definition Pte_S1_attr_lo_wf (r : Pte_S1_attr_lo) : Prop :=
0 attr_lo_s1_attridx r < 2^3
0 attr_lo_s1_ap r < 2^2
0 attr_lo_s1_sh r < 2^2
0 Z_of_bool $ attr_lo_s1_af r < 2^1
True.
Definition Pte_S1_attr_lo_data (r : Pte_S1_attr_lo) : Z :=
eval 10 (ctm_to_tm (Pte_S1_attr_lo_ctm r)).
Definition Pte_S1_attr_lo_sig_ranges := [#
(range_of 2 3); (range_of 6 2); (range_of 8 2); (range_of 10 1)].
Record Pte_S1_attr_hi := {
attr_hi_s1_xn : bool;
}.
Definition Pte_S1_attr_hi_ctm (r : Pte_S1_attr_hi) : ctm := [
(range_of 54 1, fv_bool $ attr_hi_s1_xn r)
].
Definition Pte_S1_attr_hi_wf (r : Pte_S1_attr_hi) : Prop :=
0 Z_of_bool $ attr_hi_s1_xn r < 2^1
True.
Definition Pte_S1_attr_hi_data (r : Pte_S1_attr_hi) : Z :=
eval 13 (ctm_to_tm (Pte_S1_attr_hi_ctm r)).
Definition Pte_S1_attr_hi_sig_ranges := [# (range_of 54 1)].
(* S2 specific *)
Record Pte_S2_attr_lo := {
attr_lo_s2_memattr : Z;
attr_lo_s2_ap_r : bool;
attr_lo_s2_ap_w : bool;
attr_lo_s2_sh : Z;
attr_lo_s2_af : bool;
}.
Definition Pte_S2_attr_lo_ctm (r : Pte_S2_attr_lo) : ctm := [
(range_of 2 3, fv_int $ attr_lo_s2_memattr r);
(range_of 6 1, fv_bool $ attr_lo_s2_ap_r r);
(range_of 7 1, fv_bool $ attr_lo_s2_ap_w r);
(range_of 8 2, fv_int $ attr_lo_s2_sh r);
(range_of 10 1, fv_bool $ attr_lo_s2_af r)
].
Definition Pte_S2_attr_lo_wf (r : Pte_S2_attr_lo) : Prop :=
0 attr_lo_s2_memattr r < 2^3
0 Z_of_bool $ attr_lo_s2_ap_r r < 2^1
0 Z_of_bool $ attr_lo_s2_ap_w r < 2^1
0 attr_lo_s2_sh r < 2^2
0 Z_of_bool $ attr_lo_s2_af r < 2^1
True.
Definition Pte_S2_attr_lo_data (r : Pte_S2_attr_lo) : Z :=
eval 10 (ctm_to_tm (Pte_S2_attr_lo_ctm r)).
Definition Pte_S2_attr_lo_sig_ranges := [#
(range_of 2 3); (range_of 6 1); (range_of 7 1); (range_of 8 2); (range_of 10 1)].
Record Pte_S2_attr_hi := {
attr_hi_s2_xn : bool;
}.
Definition Pte_S2_attr_hi_ctm (r : Pte_S2_attr_hi) : ctm := [
(range_of 54 1, fv_bool $ attr_hi_s2_xn r)
].
Definition Pte_S2_attr_hi_wf (r : Pte_S2_attr_hi) : Prop :=
0 Z_of_bool $ attr_hi_s2_xn r < 2^1
True.
Definition Pte_S2_attr_hi_data (r : Pte_S2_attr_hi) : Z :=
eval 13 (ctm_to_tm (Pte_S2_attr_hi_ctm r)).
Definition Pte_S2_attr_hi_sig_ranges := [# (range_of 54 1)].
(* Pte<stage> *)
Inductive stage : Type := S1 | S2.
Record Pte (s : stage) := {
pte_valid : bool;
pte_type : Z;
pte_leaf_attr_lo :
match s with S1 => Pte_S1_attr_lo | S2 => Pte_S2_attr_lo end;
pte_addr : Z;
pte_undef : Z;
pte_leaf_attr_hi :
match s with S1 => Pte_S1_attr_hi | S2 => Pte_S2_attr_hi end;
}.
Arguments pte_valid {_}.
Arguments pte_type {_}.
Arguments pte_leaf_attr_lo {_}.
Arguments pte_addr {_}.
Arguments pte_undef {_}.
Arguments pte_leaf_attr_hi {_}.
Definition pte_leaf_attr_lo_data {t : stage} (r : Pte t) : Z :=
(match t with
| S1 => λ r : Pte S1, Pte_S1_attr_lo_data (pte_leaf_attr_lo r)
| S2 => λ r : Pte S2, Pte_S2_attr_lo_data (pte_leaf_attr_lo r)
end) r.
Definition pte_leaf_attr_hi_data {t : stage} (r : Pte t) : Z :=
(match t with
| S1 => λ r : Pte S1, Pte_S1_attr_hi_data (pte_leaf_attr_hi r)
| S2 => λ r : Pte S2, Pte_S2_attr_hi_data (pte_leaf_attr_hi r)
end) r.
Global Program Instance Pte_S1_bd : BitfieldDesc (Pte S1) := {|
bitfield_it := u64;
bitfield_wf r :=
0 Z_of_bool $ pte_valid r < 2^1
0 pte_type r < 2^1
Pte_S1_attr_lo_wf (pte_leaf_attr_lo r)
0 pte_addr r < 2^36
0 pte_undef r < 2^3
Pte_S1_attr_hi_wf (pte_leaf_attr_hi r)
True;
bitfield_ctm r := [
(range_of 0 1, fv_bool $ pte_valid r);
(range_of 1 1, fv_int $ pte_type r)
] ++ Pte_S1_attr_lo_ctm (pte_leaf_attr_lo r) ++ [
(range_of 12 36, fv_int $ pte_addr r);
(range_of 48 3, fv_int $ pte_undef r)
] ++ Pte_S1_attr_hi_ctm (pte_leaf_attr_hi r);
bitfield_sig := {|
sig_bits := 64;
sig_ranges :=
[# (range_of 0 1); (range_of 1 1)] +++
Pte_S1_attr_lo_sig_ranges +++
[# (range_of 48 3)] +++
Pte_S1_attr_hi_sig_ranges
|}
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Global Program Instance Pte_S2_bd : BitfieldDesc (Pte S2) := {|
bitfield_it := u64;
bitfield_wf r :=
0 Z_of_bool $ pte_valid r < 2^1
0 pte_type r < 2^1
Pte_S2_attr_lo_wf (pte_leaf_attr_lo r)
0 pte_addr r < 2^36
0 pte_undef r < 2^3
Pte_S2_attr_hi_wf (pte_leaf_attr_hi r)
True;
bitfield_ctm r := [
(range_of 0 1, fv_bool $ pte_valid r);
(range_of 1 1, fv_int $ pte_type r)
] ++ Pte_S2_attr_lo_ctm (pte_leaf_attr_lo r) ++ [
(range_of 12 36, fv_int $ pte_addr r);
(range_of 48 3, fv_int $ pte_undef r)
] ++ Pte_S2_attr_hi_ctm (pte_leaf_attr_hi r);
bitfield_sig := {|
sig_bits := 64;
sig_ranges :=
[# (range_of 0 1); (range_of 1 1)] +++
Pte_S2_attr_lo_sig_ranges +++
[# (range_of 48 3)] +++
Pte_S2_attr_hi_sig_ranges
|}
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Global Program Instance Pte_bd t : BitfieldDesc (Pte t) := {|
bitfield_it := u64;
bitfield_wf r :=
0 Z_of_bool $ pte_valid r < 2^1
0 pte_type r < 2^1
0 pte_leaf_attr_lo_data r < 2^10
0 pte_addr r < 2^36
0 pte_undef r < 2^3
0 pte_leaf_attr_hi_data r < 2^13
True;
bitfield_ctm r := [
(range_of 0 1, fv_bool $ pte_valid r);
(range_of 1 1, fv_int $ pte_type r);
(range_of 2 10, fv_int $ pte_leaf_attr_lo_data r);
(range_of 12 36, fv_int $ pte_addr r);
(range_of 48 3, fv_int $ pte_undef r);
(range_of 51 13, fv_int $ pte_leaf_attr_hi_data r)
];
bitfield_sig := {|
sig_bits := 64;
sig_ranges := [#
(range_of 0 1); (range_of 1 1); (range_of 2 10); (range_of 12 36); (range_of 48 3); (range_of 51 13)
];
|}
|}.
Next Obligation. intros; solve_ranges_monotone. Qed.
Next Obligation. intros; sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
(* Global Instance Pte_settable : Settable _ := settable! mk_Pte *)
(* <pte_valid; pte_type; pte_leaf_attr_lo; pte_addr; pte_undef; pte_leaf_attr_hi>. *)
(*Definition zero_Pte := {|
pte_valid := false;
pte_type := 0;
pte_leaf_attr_lo := None;
pte_addr := 0;
pte_undef := 0;
pte_leaf_attr_hi := 0;
|}.*)
Global Instance simpl_exist_Pte t P : SimplExist (Pte t) P (
pte_valid pte_type pte_leaf_attr_lo pte_addr pte_undef pte_leaf_attr_hi, P {|
pte_valid := pte_valid;
pte_type := pte_type;
pte_leaf_attr_lo := pte_leaf_attr_lo;
pte_addr := pte_addr;
pte_undef := pte_undef;
pte_leaf_attr_hi := pte_leaf_attr_hi;
|}
).
Proof. unfold SimplExist. naive_solver. Qed.
Global Instance simpl_forall_Pte t P : SimplForall (Pte t) 6 P (
pte_valid pte_type pte_leaf_attr_lo pte_addr pte_undef pte_leaf_attr_hi, P {|
pte_valid := pte_valid;
pte_type := pte_type;
pte_leaf_attr_lo := pte_leaf_attr_lo;
pte_addr := pte_addr;
pte_undef := pte_undef;
pte_leaf_attr_hi := pte_leaf_attr_hi;
|}
).
Proof. unfold SimplForall => ? []. naive_solver. Qed.
(*
Record Attr := mk_Attr {
attr_lo_s1_attridx : Z;