Commit ee7ef68d authored by Paul's avatar Paul
Browse files

try define and customize fields

parent e3ff8f1a
......@@ -170,7 +170,7 @@ struct kvm_pgtable_mm_ops {
[[rc::parameters("pte : Z")]]
[[rc::args("pte @ int<u64>")]]
[[rc::returns("{valid pte} @ boolean<bool_it>")]]
[[rc::returns("{get_field pte_valid pte} @ boolean<bool_it>")]]
[[rc::trust_me]]
static bool kvm_pte_valid(kvm_pte_t pte)
{
......@@ -179,7 +179,7 @@ static bool kvm_pte_valid(kvm_pte_t pte)
[[rc::parameters("pte : Z", "level : nat")]]
[[rc::args("pte @ int<u64>", "level @ int<u32>")]]
[[rc::returns("{bool_decide (level <> 3) && valid pte && table pte} @ boolean<bool_it>")]]
[[rc::returns("{bool_decide (level <> 3%nat) && get_field pte_valid pte && get_field pte_table pte} @ boolean<bool_it>")]]
[[rc::trust_me]]
static bool kvm_pte_table(kvm_pte_t pte, u32 level)
{
......@@ -190,10 +190,9 @@ static bool kvm_pte_table(kvm_pte_t pte, u32 level)
return FIELD_GET(KVM_PTE_TYPE, pte) == KVM_PTE_TYPE_TABLE;
}
[[rc::parameters("pte_old : Z", "p : loc")]]
[[rc::args("p @ &own<pte_old @ int<u64>>")]]
[[rc::exists("pte_new : Z")]]
[[rc::ensures("own p : pte_new @ int<u64>", "{valid pte_new = false}")]]
[[rc::parameters("pte : Z", "p : loc")]]
[[rc::args("p @ &own<pte @ int<u64>>")]]
[[rc::ensures("own p : {put_field pte_valid false pte} @ int<u64>")]]
[[rc::trust_me]]
static void kvm_set_invalid_pte(kvm_pte_t *ptep)
{
......@@ -203,9 +202,7 @@ static void kvm_set_invalid_pte(kvm_pte_t *ptep)
[[rc::parameters("pa : Z")]]
[[rc::args("pa @ int<u64>")]]
[[rc::exists("pte : Z")]]
[[rc::returns("pte @ int<u64>")]]
[[rc::ensures("{pa_pte pa pte}")]]
[[rc::returns("{mask_field pte_addr pa} @ int<u64>")]]
[[rc::trust_me]]
static kvm_pte_t kvm_phys_to_pte(u64 pa)
{
......@@ -225,6 +222,7 @@ static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
pte |= KVM_PTE_VALID;
// WARN_ON(kvm_pte_valid(old)); TODO: assert
// smp_store_release(ptep, pte);
*ptep = pte;
}
static bool kvm_set_valid_leaf_pte(kvm_pte_t *ptep, u64 pa, kvm_pte_t attr,
......@@ -240,6 +238,7 @@ static bool kvm_set_valid_leaf_pte(kvm_pte_t *ptep, u64 pa, kvm_pte_t attr,
if (kvm_pte_valid(old))
return old == pte;
// smp_store_release(ptep, pte);
*ptep = pte;
return true;
}
......
......@@ -17,22 +17,22 @@ Section spec.
(* Specifications for function [kvm_pte_valid]. *)
Definition type_of_kvm_pte_valid :=
fn( pte : Z; (pte @ (int (u64))); True)
() : (), ((valid pte) @ (boolean (bool_it))); True.
() : (), ((get_field pte_valid pte) @ (boolean (bool_it))); True.
(* Specifications for function [kvm_pte_table]. *)
Definition type_of_kvm_pte_table :=
fn( (pte, level) : Z * nat; (pte @ (int (u64))), (level @ (int (u32))); True)
() : (), ((negb (level =? 3) && valid pte && table pte) @ (boolean (bool_it))); True.
() : (), ((bool_decide (level <> 3%nat) && get_field pte_valid pte && get_field pte_table pte) @ (boolean (bool_it))); True.
(* Specifications for function [kvm_set_invalid_pte]. *)
Definition type_of_kvm_set_invalid_pte :=
fn( (pte_old, p) : Z * loc; (p @ (&own (pte_old @ (int (u64))))); True)
pte_new : Z, (void); (p ◁ₗ (pte_new @ (int (u64)))) valid pte_new = false.
fn( (pte, p) : Z * loc; (p @ (&own (pte @ (int (u64))))); True)
() : (), (void); (p ◁ₗ ((put_field pte_valid false pte) @ (int (u64)))).
(* Specifications for function [kvm_phys_to_pte]. *)
Definition type_of_kvm_phys_to_pte :=
fn( pa : Z; (pa @ (int (u64))); True)
pte : Z, (pte @ (int (u64))); pa_pte pa pte.
() : (), ((mask_field pte_addr pa) @ (int (u64))); True.
(* Function [kvm_set_table_pte] has been skipped. *)
......
From refinedc.typing Require Import typing.
(* TODO: pte as record *)
(* TODO: Z (infinite vector) <-> list|vec bool *)
Definition valid (pte : Z) : bool :=
Z.testbit pte 0.
Record field_desc := {
field_offset : nat;
field_len : nat;
field_value_t : Type;
field_encode : field_value_t -> list bool; (* array bool field_len; vec *)
field_decode : list bool -> field_value_t;
}.
Definition table (pte : Z) : bool :=
Z.testbit pte 1.
Fixpoint read_bits (offset len : nat) (bv : Z) : list bool :=
match len with
| O => []
| S n => (Z.testbit offset bv) :: read_bits (S offset) n bv
end.
(* Definition invalidate (pte : Z) : Z := . *)
Definition get_field (fd : field_desc) (bv : Z) : field_value_t fd :=
field_decode fd $ read_bits (field_offset fd) (field_len fd) bv.
Definition pa_pte (pa pte : Z) : Prop :=
i, 12 i 47 -> Z.testbit pa i = Z.testbit pte i.
Fixpoint write_bits (offset : nat) (v : list bool) (bv : Z) : Z :=
match v with
| [] => bv
| true :: bs => Z.setbit offset $ write_bits (S offset) bs bv
| false :: bs => Z.clearbit offset $ write_bits (S offset) bs bv
end.
Definition put_field (fd : field_desc) (v : field_value_t fd) (bv : Z) : Z :=
write_bits (field_offset fd) (field_encode fd v) bv.
Definition mask_field (fd : field_desc) (bv : Z) : Z :=
put_field fd (get_field fd bv) 0.
Definition bool_field_desc (offset : nat) := {|
field_offset := offset;
field_len := 1;
field_value_t := bool;
field_encode := λ b, [b];
field_decode := λ l, match l with [b] => b | _ => false (* impossible *) end;
|}.
Definition enum_field_desc (offset len : nat) (K : Type) `{EqDecision K}
(items : list (K * list bool)) (def : K) := {|
field_offset := offset;
field_len := len;
field_value_t := K;
field_encode := λ k,
let fix f l :=
match l with
| [] => []
| (x, v) :: l' => if bool_decide (x = k) then v else f l'
end
in f items;
field_decode := λ v,
let fix f l :=
match l with
| [] => def
| (k, x) :: l' => if bool_decide (x = v) then k else f l'
end
in f items;
|}.
Definition data_field_desc (offset len : nat) := {|
field_offset := offset;
field_len := len;
field_value_t := list bool;
field_encode := id;
field_decode := id;
|}.
(* pte *)
Definition pte_valid := bool_field_desc 0.
Definition pte_table := bool_field_desc 1.
Definition pte_addr := data_field_desc 12 (47 - 12 + 1).
Markdown is supported
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