Commit 8fda653f authored by Rodolphe Lepigre's avatar Rodolphe Lepigre Committed by Paul
Browse files

More example simplifications.

parent 1c077e3d
......@@ -20,7 +20,7 @@ typedef uint32_t u32;
(typeof(_mask))(((_reg) & (_mask)) >> __bf_shf(_mask))
// Simplified static check (uses GCC statement-as-expression).
#define FIELD_PREP(_mask, _val) \
#define FIELD_PREP(_mask, _val) \
((typeof(_mask))(_val) << __bf_shf(_mask)) & (_mask)
typedef u64 pte_t;
......@@ -53,12 +53,6 @@ typedef u64 pte_t;
//@rc::inlined_prelude
//@Definition max_level : Z := 4.
//@
//@Definition pte_from_addr (pa : Pte) : Pte :=
//@ zero_Pte <| pte_addr := pte_addr pa |>.
//@
//@Definition pte_pa (pa : Pte) : tm :=
//@ bf_cons (range_of 12 36) (bf_val $ pte_addr pa) bf_nil.
//@rc::end
[[rc::parameters("pte : Pte")]]
......@@ -66,37 +60,32 @@ typedef u64 pte_t;
[[rc::requires("{bitfield_wf pte}")]] // FIXME not necessary.
[[rc::returns("{pte_valid pte} @ boolean<bool_it>")]]
static bool pte_valid(pte_t pte) {
return 0 != (pte & PTE_VALID);
//return (pte & PTE_VALID);
}
[[rc::parameters("pa : Pte")]]
[[rc::args("pa @ bitfield<Pte>")]]
[[rc::returns("{pte_pa pa} @ bitfield_tpd<Pte>")]]
static pte_t phys_to_pte(u64 pa) {
pte_t pte = pa & PTE_ADDR_MASK;
// Simplified away deadcode (fixed PAGE_SHIFT of 12).
return pte;
return 0 != (pte & PTE_VALID); // return pte & PTE_VALID; // FIXME
}
//@rc::inlined_prelude
//@Definition result_pte pa level attr :=
//@ let type := if bool_decide (level = max_level - 1) then pte_type_page else pte_type_block in
//@ (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 |>.
//@Notation "P ? l : r" :=
//@ (if bool_decide P then l else r)
//@ (at level 100, l at next level, r at next level).
//@
//@Definition svl_pte pa level attr :=
//@ let type := level = max_level - 1 ? pte_type_page : pte_type_block in
//@ zero_Pte <| pte_addr := pte_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::end
[[rc::requires("{bitfield_wf old}", "{bitfield_wf pa}", "{bitfield_wf attr}")]] // FIXME not necessary.
[[rc::parameters("p : loc", "old : Pte", "pa : Pte", "attr : Pte", "level : Z")]]
[[rc::args("p @ &own<old @ bitfield<Pte>>", "pa @ bitfield<Pte>", "attr @ bitfield<Pte>", "level @ int<u32>")]]
[[rc::requires("{old.(pte_valid) = false}")]]
[[rc::requires("{bitfield_wf old}", "{bitfield_wf pa}", "{bitfield_wf attr}")]] // FIXME not necessary.
[[rc::returns("{true} @ boolean<bool_it>")]]
[[rc::ensures("own p : {result_pte pa level attr} @ bitfield<Pte>")]]
[[rc::ensures("own p : {svl_pte pa level attr} @ bitfield<Pte>")]]
static bool set_valid_leaf_pte(pte_t *ptep, u64 pa, pte_t attr, u32 level) {
pte_t old = *ptep;
pte_t pte = phys_to_pte(pa);
pte_t pte = pa & PTE_ADDR_MASK; // Inlined function.
u64 type = (level == MAX_LEVEL - 1) ?
PTE_TYPE_PAGE :
PTE_TYPE_BLOCK;
......@@ -104,11 +93,9 @@ static bool set_valid_leaf_pte(pte_t *ptep, u64 pa, pte_t attr, u32 level) {
pte |= FIELD_PREP(PTE_TYPE, type);
pte |= PTE_VALID;
/* Tolerate KVM recreating the exact same mapping. */
if(pte_valid(old))
return old == pte;
// smp_store_release(ptep, pte);
*ptep = pte;
*ptep = pte; // smp_store_release(ptep, pte);
return true;
}
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