Commit 8aef71bf authored by Michael Sammler's avatar Michael Sammler Committed by Paul
Browse files

fix x86_pgtable case study

parent df080dd4
From refinedc.typing Require Import typing.
From refinedc.mask_core Require Import typecheck.
Record pte := mk_pte {
pg_present : bool;
pg_write : bool;
pg_user : bool;
pg_pwt : bool;
pg_pcd : bool;
pg_accessed : bool;
pg_dirty : bool;
pg_pse : bool;
pg_global : bool;
pg_special : bool;
pg_uffd_wp : bool;
pg_soft_dirty : bool;
(*****)
pg_dev_map : bool;
pg_no_exec : bool;
}.
Global Instance pte_settable : Settable _ := settable! mk_pte
<pg_present; pg_write; pg_user; pg_pwt; pg_pcd;
pg_accessed; pg_dirty; pg_pse; pg_global; pg_special;
pg_uffd_wp; pg_soft_dirty;
pg_dev_map; pg_no_exec>.
Definition pte_repr (f : pte) : tm :=
bf_cons (range_of 0 1) (bf_val $ Z_of_bool $ pg_present f) $
bf_cons (range_of 1 1) (bf_val $ Z_of_bool $ pg_write f) $
bf_cons (range_of 2 1) (bf_val $ Z_of_bool $ pg_user f) $
bf_cons (range_of 3 1) (bf_val $ Z_of_bool $ pg_pwt f) $
bf_cons (range_of 4 1) (bf_val $ Z_of_bool $ pg_pcd f) $
bf_cons (range_of 5 1) (bf_val $ Z_of_bool $ pg_accessed f) $
bf_cons (range_of 6 1) (bf_val $ Z_of_bool $ pg_dirty f) $
bf_cons (range_of 7 1) (bf_val $ Z_of_bool $ pg_pse f) $
bf_cons (range_of 8 1) (bf_val $ Z_of_bool $ pg_global f) $
bf_cons (range_of 9 1) (bf_val $ Z_of_bool $ pg_special f) $
bf_cons (range_of 10 1) (bf_val $ Z_of_bool $ pg_uffd_wp f) $
bf_cons (range_of 11 1) (bf_val $ Z_of_bool $ pg_soft_dirty f) $
bf_cons (range_of 58 1) (bf_val $ Z_of_bool $ pg_dev_map f) $
bf_cons (range_of 63 1) (bf_val $ Z_of_bool $ pg_no_exec f) $
bf_nil.
Arguments pte_repr _/.
Coercion pte_repr : pte >-> tm.
Definition pte_wf (f : pte) : Prop :=
0 Z_of_bool $ pg_present f < 2^1
0 Z_of_bool $ pg_write f < 2^1
0 Z_of_bool $ pg_user f < 2^1
0 Z_of_bool $ pg_pwt f < 2^1
0 Z_of_bool $ pg_pcd f < 2^1
0 Z_of_bool $ pg_accessed f < 2^1
0 Z_of_bool $ pg_dirty f < 2^1
0 Z_of_bool $ pg_pse f < 2^1
0 Z_of_bool $ pg_global f < 2^1
0 Z_of_bool $ pg_special f < 2^1
0 Z_of_bool $ pg_uffd_wp f < 2^1
0 Z_of_bool $ pg_soft_dirty f < 2^1
0 Z_of_bool $ pg_dev_map f < 2^1
0 Z_of_bool $ pg_no_exec f < 2^1.
(* 0 ≤ f < 2^64. *)
Global Program Instance pte_Bitfield_Desc : BitfieldDesc pte := {|
bitfield_it := u64;
bitfield_repr := pte_repr;
bitfield_wf := pte_wf;
bitfield_sig := {|
sig_bits := 64;
sig_ranges := [# (range_of 0 1); (range_of 1 1); (range_of 2 1); (range_of 3 1); (range_of 4 1);
(range_of 5 1); (range_of 6 1); (range_of 7 1); (range_of 8 1); (range_of 9 1); (range_of 10 1);
(range_of 11 1); (range_of 58 1); (range_of 63 1)];
|}
|}.
Next Obligation. solve_ranges_monotone. Qed.
Next Obligation. sig_max_range_bounded. Qed.
Next Obligation. done. Qed.
Lemma pte_repr_tpd r :
check_has_ty (pte_repr r) (bv bitfield_sig).
Proof. done. Qed.
Definition pte_present (p : pte) : bool := pg_present p || pg_global p.
Arguments pte_present _/.
//@rc::import x86_pgtable_lemmas from refinedc.linux.casestudies.x86_pgtable
#include <stdbool.h>
#include "bits.h"
//@rc::bitfields pte as u64
//@ pte_present : bool[0]
//@ pte_write : bool[1]
//@ pte_user : bool[2]
//@ pte_pwt : bool[3]
//@ pte_pcd : bool[4]
//@ pte_accessed : bool[5]
//@ pte_dirty : bool[6]
//@ pte_pse : bool[7]
//@ pte_global : bool[8]
//@ pte_special : bool[9]
//@ pte_uffd_wp : bool[10]
//@ pte_soft_dirty : bool[11]
//@ pte_dev_map : bool[58]
//@ pte_no_exec : bool[63]
//@rc::end
//@rc::inlined_prelude
//@Definition pte_present_or_global (p : pte) : bool := pte_present p || pte_global p.
//@Arguments pte_present_or_global _/.
//@rc::end
// arch/x86/include/asm/page_64_types.h
#define __PHYSICAL_MASK_SHIFT 52
......@@ -20,8 +44,8 @@ typedef u64 phys_addr_t;
// arch/x86/include/asm/pgtable_64_types.h
typedef unsigned long pteval_t;
typedef struct [[rc::refined_by("v : tm")]] pte_t {
[[rc::field("v @ bitfield_raw<u64>")]]
typedef struct [[rc::refined_by("v : pte")]] pte_t {
[[rc::field("v @ bitfield<pte>")]]
pteval_t pte;
} pte_t;
......@@ -29,14 +53,14 @@ typedef struct [[rc::refined_by("v : tm")]] pte_t {
[[rc::parameters("p : pte")]]
[[rc::args("p @ pte_t")]]
[[rc::returns("p @ bitfield_raw<u64>")]]
[[rc::returns("p @ bitfield<pte>")]]
static inline pteval_t native_pte_val(pte_t pte)
{
return pte.pte;
}
[[rc::parameters("v : tm")]]
[[rc::args("v @ bitfield_raw<u64>")]]
[[rc::parameters("v : pte")]]
[[rc::args("v @ bitfield<pte>")]]
[[rc::returns("v @ pte_t")]]
static inline pte_t native_make_pte(pteval_t val)
{
......@@ -118,7 +142,7 @@ static inline pteval_t pte_flags(pte_t pte)
[[rc::requires("{bitfield_wf p}")]]
INPUT_PTE
[[rc::returns("{pte_present p} @ boolean<bool_it>")]]
[[rc::returns("{pte_present_or_global p} @ boolean<bool_it>")]]
static inline bool pte_present(pte_t a)
{
// TODO: remove 0 != once issue #45 is fixed
......@@ -134,7 +158,7 @@ static inline bool pte_present(pte_t a)
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_dirty p} @ boolean<bool_it>")]]
[[rc::returns("{pte_dirty p} @ boolean<bool_it>")]]
static inline bool pte_dirty(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_DIRTY);
......@@ -142,7 +166,7 @@ static inline bool pte_dirty(pte_t pte)
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_accessed p} @ boolean<bool_it>")]]
[[rc::returns("{pte_accessed p} @ boolean<bool_it>")]]
static inline bool pte_young(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_ACCESSED);
......@@ -150,7 +174,7 @@ static inline bool pte_young(pte_t pte)
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_write p} @ boolean<bool_it>")]]
[[rc::returns("{pte_write p} @ boolean<bool_it>")]]
static inline bool pte_write(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_RW);
......@@ -158,7 +182,7 @@ static inline bool pte_write(pte_t pte)
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_pse p} @ boolean<bool_it>")]]
[[rc::returns("{pte_pse p} @ boolean<bool_it>")]]
static inline bool pte_huge(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_PSE);
......@@ -166,7 +190,7 @@ static inline bool pte_huge(pte_t pte)
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_global p} @ boolean<bool_it>")]]
[[rc::returns("{pte_global p} @ boolean<bool_it>")]]
static inline bool pte_global(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_GLOBAL);
......@@ -174,7 +198,7 @@ static inline bool pte_global(pte_t pte)
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{negb (pg_no_exec p)} @ boolean<bool_it>")]]
[[rc::returns("{negb (pte_no_exec p)} @ boolean<bool_it>")]]
[[rc::trust_me]] // TODO: Z_of_bool (negb _) bound
static inline bool pte_exec(pte_t pte)
{
......@@ -183,25 +207,27 @@ static inline bool pte_exec(pte_t pte)
INPUT_PTE
IF_PTE_PRESENT
[[rc::returns("{pg_special p} @ boolean<bool_it>")]]
[[rc::returns("{pte_special p} @ boolean<bool_it>")]]
static inline bool pte_special(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_SPECIAL);
}
[[rc::parameters("p : pte", "m : tm")]]
[[rc::args("p @ pte_t", "m @ bitfield_raw<u64>")]]
[[rc::returns("{bf_or p m} @ pte_t")]]
/* [[rc::parameters("p : pte", "m : tm")]] */
/* [[rc::args("p @ pte_t", "m @ bitfield_raw<u64>")]] */
/* [[rc::returns("{bf_or p m} @ pte_t")]] */
[[rc::inlined]]
static inline pte_t pte_set_flags(pte_t pte, pteval_t set)
{
pteval_t v = native_pte_val(pte);
return native_make_pte(v | set);
}
[[rc::parameters("p : pte", "m : tm")]]
[[rc::args("p @ pte_t", "m @ bitfield_raw<u64>")]]
/* [[rc::parameters("p : pte", "m : tm")]] */
/* [[rc::args("p @ pte_t", "m @ bitfield_raw<u64>")]] */
// [[rc::requires("{normalize_bitfield_eq (Z.land p (Z_lunot 64 m)) res}")]]
[[rc::returns("{bf_and_neg p m} @ pte_t")]]
/* [[rc::returns("{bf_and_neg p m} @ pte_t")]] */
[[rc::inlined]]
static inline pte_t pte_clear_flags(pte_t pte, pteval_t clear)
{
pteval_t v = native_pte_val(pte);
......@@ -210,138 +236,138 @@ static inline pte_t pte_clear_flags(pte_t pte, pteval_t clear)
// #ifdef CONFIG_HAVE_ARCH_USERFAULTFD_WP
INPUT_PTE
[[rc::returns("{pg_uffd_wp p} @ boolean<bool_it>")]]
[[rc::returns("{pte_uffd_wp p} @ boolean<bool_it>")]]
static inline bool pte_uffd_wp(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_UFFD_WP);
}
// bitfield in struct: subsume val eq
// INPUT_PTE
// [[rc::returns("{p <| pg_uffd_wp := true |>} @ pte_t")]]
// static inline pte_t pte_mkuffd_wp(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_UFFD_WP);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_uffd_wp := false |>} @ pte_t")]]
// static inline pte_t pte_clear_uffd_wp(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_UFFD_WP);
// }
// // #endif
// INPUT_PTE
// [[rc::returns("{p <| pg_dirty := false |>} @ pte_t")]]
// static inline pte_t pte_mkclean(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_DIRTY);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_accessed := false |>} @ pte_t")]]
// static inline pte_t pte_mkold(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_ACCESSED);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_write := false |>} @ pte_t")]]
// static inline pte_t pte_wrprotect(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_RW);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_no_exec := false |>} @ pte_t")]]
// static inline pte_t pte_mkexec(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_NX);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_dirty := true |> <| pg_soft_dirty := true |>} @ pte_t")]]
// static inline pte_t pte_mkdirty(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_DIRTY | _PAGE_SOFT_DIRTY);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_accessed := true |>} @ pte_t")]]
// static inline pte_t pte_mkyoung(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_ACCESSED);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_write := true |>} @ pte_t")]]
// static inline pte_t pte_mkwrite(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_RW);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_pse := true |>} @ pte_t")]]
// static inline pte_t pte_mkhuge(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_PSE);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_pse := false |>} @ pte_t")]]
// static inline pte_t pte_clrhuge(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_PSE);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_global := true |>} @ pte_t")]]
// static inline pte_t pte_mkglobal(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_GLOBAL);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_global := false |>} @ pte_t")]]
// static inline pte_t pte_clrglobal(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_GLOBAL);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_special := true |>} @ pte_t")]]
// static inline pte_t pte_mkspecial(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_SPECIAL);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_special := true |> <| pg_dev_map := true |>} @ pte_t")]]
// static inline pte_t pte_mkdevmap(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_SPECIAL | _PAGE_DEVMAP);
// }
// // #ifdef CONFIG_HAVE_ARCH_SOFT_DIRTY
// INPUT_PTE
// [[rc::returns("{pg_soft_dirty p} @ boolean<bool_it>")]]
// static inline bool pte_soft_dirty(pte_t pte)
// {
// return 0 != (pte_flags(pte) & _PAGE_SOFT_DIRTY);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_soft_dirty := true |>} @ pte_t")]]
// static inline pte_t pte_mksoft_dirty(pte_t pte)
// {
// return pte_set_flags(pte, _PAGE_SOFT_DIRTY);
// }
// INPUT_PTE
// [[rc::returns("{p <| pg_soft_dirty := false |>} @ pte_t")]]
// static inline pte_t pte_clear_soft_dirty(pte_t pte)
// {
// return pte_clear_flags(pte, _PAGE_SOFT_DIRTY);
// }
// // #endif
INPUT_PTE
[[rc::returns("{p <| pte_uffd_wp := true |>} @ pte_t")]]
static inline pte_t pte_mkuffd_wp(pte_t pte)
{
return pte_set_flags(pte, _PAGE_UFFD_WP);
}
INPUT_PTE
[[rc::returns("{p <| pte_uffd_wp := false |>} @ pte_t")]]
static inline pte_t pte_clear_uffd_wp(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_UFFD_WP);
}
// #endif
INPUT_PTE
[[rc::returns("{p <| pte_dirty := false |>} @ pte_t")]]
static inline pte_t pte_mkclean(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pte_accessed := false |>} @ pte_t")]]
static inline pte_t pte_mkold(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_ACCESSED);
}
INPUT_PTE
[[rc::returns("{p <| pte_write := false |>} @ pte_t")]]
static inline pte_t pte_wrprotect(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_RW);
}
INPUT_PTE
[[rc::returns("{p <| pte_no_exec := false |>} @ pte_t")]]
static inline pte_t pte_mkexec(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_NX);
}
INPUT_PTE
[[rc::returns("{p <| pte_dirty := true |> <| pte_soft_dirty := true |>} @ pte_t")]]
static inline pte_t pte_mkdirty(pte_t pte)
{
return pte_set_flags(pte, _PAGE_DIRTY | _PAGE_SOFT_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pte_accessed := true |>} @ pte_t")]]
static inline pte_t pte_mkyoung(pte_t pte)
{
return pte_set_flags(pte, _PAGE_ACCESSED);
}
INPUT_PTE
[[rc::returns("{p <| pte_write := true |>} @ pte_t")]]
static inline pte_t pte_mkwrite(pte_t pte)
{
return pte_set_flags(pte, _PAGE_RW);
}
INPUT_PTE
[[rc::returns("{p <| pte_pse := true |>} @ pte_t")]]
static inline pte_t pte_mkhuge(pte_t pte)
{
return pte_set_flags(pte, _PAGE_PSE);
}
INPUT_PTE
[[rc::returns("{p <| pte_pse := false |>} @ pte_t")]]
static inline pte_t pte_clrhuge(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_PSE);
}
INPUT_PTE
[[rc::returns("{p <| pte_global := true |>} @ pte_t")]]
static inline pte_t pte_mkglobal(pte_t pte)
{
return pte_set_flags(pte, _PAGE_GLOBAL);
}
INPUT_PTE
[[rc::returns("{p <| pte_global := false |>} @ pte_t")]]
static inline pte_t pte_clrglobal(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_GLOBAL);
}
INPUT_PTE
[[rc::returns("{p <| pte_special := true |>} @ pte_t")]]
static inline pte_t pte_mkspecial(pte_t pte)
{
return pte_set_flags(pte, _PAGE_SPECIAL);
}
INPUT_PTE
[[rc::returns("{p <| pte_special := true |> <| pte_dev_map := true |>} @ pte_t")]]
static inline pte_t pte_mkdevmap(pte_t pte)
{
return pte_set_flags(pte, _PAGE_SPECIAL | _PAGE_DEVMAP);
}
// #ifdef CONFIG_HAVE_ARCH_SOFT_DIRTY
INPUT_PTE
[[rc::returns("{pte_soft_dirty p} @ boolean<bool_it>")]]
static inline bool pte_soft_dirty(pte_t pte)
{
return 0 != (pte_flags(pte) & _PAGE_SOFT_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pte_soft_dirty := true |>} @ pte_t")]]
static inline pte_t pte_mksoft_dirty(pte_t pte)
{
return pte_set_flags(pte, _PAGE_SOFT_DIRTY);
}
INPUT_PTE
[[rc::returns("{p <| pte_soft_dirty := false |>} @ pte_t")]]
static inline pte_t pte_clear_soft_dirty(pte_t pte)
{
return pte_clear_flags(pte, _PAGE_SOFT_DIRTY);
}
// #endif
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