Commit 0b431d8e authored by Fengmin Zhu's avatar Fengmin Zhu Committed by Michael Sammler
Browse files

Add record update

parent 0b843fa1
Pipeline #55573 passed with stage
in 22 minutes and 32 seconds
......@@ -220,7 +220,7 @@ static bool kvm_pte_table(kvm_pte_t pte, u32 level)
[[rc::parameters("pte : Pte", "p : loc")]]
[[rc::args("p @ &own<pte @ bitfield<Pte>>")]]
[[rc::requires("{bitfield_wf pte}")]]
[[rc::ensures("own p : {pte_set_invalid pte} @ bitfield<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;
......@@ -246,7 +246,8 @@ static kvm_pte_t kvm_phys_to_pte(u64 pa)
[[rc::requires("{bitfield_wf pte}", "{pte_valid pte}")]]
[[rc::exists("pa : Z")]]
[[rc::ensures("{mm_ops.(virt_to_phys) va = pa}")]]
[[rc::ensures("own p : { {| pte_valid := true; pte_type := pte_type_table; pte_leaf_attr_lo := 0; pte_addr := (addr_of pa); pte_undef := 0; pte_leaf_attr_hi := 0 |} } @ bitfield<Pte>")]]
[[rc::ensures("own p : {mk_pte_addr (addr_of pa) <| 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)
{
......@@ -262,7 +263,8 @@ static void kvm_set_table_pte(kvm_pte_t *ptep, kvm_pte_t *childp,
[[rc::args("p @ &own<pte @ bitfield<Pte>>", "pa @ int<u64>", "attr @ bitfield<Pte>", "level @ int<u32>")]]
[[rc::requires("{bitfield_wf pte}", "{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_valid := true; pte_type := type; pte_leaf_attr_lo := pte_leaf_attr_lo attr; pte_addr := (addr_of pa); pte_undef := 0; pte_leaf_attr_hi := pte_leaf_attr_hi attr |} }")]]
[[rc::requires("{pte1 = mk_pte_addr (addr_of 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 bool_decide (bitfield_repr pte = bitfield_repr pte1) 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,
......
......@@ -2,7 +2,7 @@ From refinedc.typing Require Import typing.
(* pte *)
Record Pte := {
Record Pte := mk_pte {
pte_valid : bool;
pte_type : Z;
pte_leaf_attr_lo : Z;
......@@ -11,24 +11,20 @@ Record Pte := {
pte_leaf_attr_hi : Z;
}.
Definition pte_set_invalid (pte : Pte) : Pte := {|
pte_valid := false;
pte_type := pte_type pte;
pte_leaf_attr_lo := pte_leaf_attr_lo pte;
pte_addr := pte_addr pte;
pte_undef := pte_undef pte;
pte_leaf_attr_hi := pte_leaf_attr_hi pte;
|}.
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 mk_pte_addr (a : Z) : Pte := {|
Definition empty_pte := {|
pte_valid := false;
pte_type := 0;
pte_leaf_attr_lo := 0;
pte_addr := a;
pte_addr := 0;
pte_undef := 0;
pte_leaf_attr_hi := 0;
|}.
Definition mk_pte_addr (a : addr) : Pte := empty_pte <| pte_addr := a |>.
Definition pte_repr (p : Pte) : Z :=
bf_cons 0 1 (Z_of_bool $ pte_valid p) $
bf_cons 1 1 (pte_type p) $
......
......@@ -24,6 +24,7 @@ depends: [
"earley" {= "3.0.0"}
"toml" {= "5.0.0"}
"ubase" {= "0.04"}
"coq-record-update" {= "0.3.0"}
]
build: [
......
......@@ -8,6 +8,9 @@ From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
From stdpp Require Import natmap.
From refinedc.lithium Require Import Z_bitblast.
From RecordUpdate Require Export RecordSet.
Export RecordSetNotations.
Set Default Proof Using "Type".
Export Unset Program Cases.
......@@ -17,6 +20,9 @@ Export Set Keyed Unification.
that at least global hints are annotated. *)
Export Set Warnings "+deprecated-hint-without-locality".
(* ensure that set from RecordUpdate simplifies when it is applied to a concrete value *)
Arguments set _ _ _ _ _ !_ /.
Typeclasses Opaque is_Some.
(* This is necessary since otherwise keyed unification unfolds these definitions *)
Global Opaque rotate_nat_add rotate_nat_sub.
......
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