SpecialRW instruction

theories/logrel/ftlr/WriteSR.v → theories/logrel/ftlr/SpecialRW.v

@@ -3,7 +3,7 @@ From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Import weakestpre adequacy lifting.
 From stdpp Require Import base.
 From cap_machine Require Import ftlr_base interp_weakening.
-From cap_machine Require Import rules_base rules_WriteSR.
+From cap_machine Require Import rules_base rules_SpecialRW.
 From cap_machine.proofmode Require Import map_simpl register_tactics.
 From cap_machine Require Import stdpp_extra.
 
@@ -26,10 +26,10 @@ Section fundamental.
   Implicit Types w : (leibnizO Word).
   Implicit Types interp : (D).
 
-  Lemma writesr_case (W : WORLD) (C : CmptName) (regs : leibnizO Reg)
+  Lemma specialrw_case (W : WORLD) (C : CmptName) (regs : leibnizO Reg)
     (p p' : Perm) (g : Locality) (b e a : Addr)
-    (w : Word) (ρ : region_type) (dst : SRegName) (src : RegName) (P:D) (cstk : CSTK) (Ws : list WORLD) (Cs : list CmptName) :
-    ftlr_instr W C regs p p' g b e a w (WriteSR dst src) ρ P cstk Ws Cs.
+    (w : Word) (ρ : region_type) (dst : RegName) (csr : SRegName) (src : RegName) (P:D) (cstk : CSTK) (Ws : list WORLD) (Cs : list CmptName) :
+    ftlr_instr W C regs p p' g b e a w (SpecialRW dst csr src) ρ P cstk Ws Cs.
   Proof.
     intros Hp Hsome HcorrectPC Hbae Hfp HO Hpers Hpwl Hregion Hnotrevoked Hi.
     iIntros "#IH #Hinv_interp #Hreg #Hinva #Hrcond #Hwcond #Hmono #HmonoV Hw Hcont %Hframe Hsts Hown Htframe".
@@ -47,17 +47,18 @@ Section fundamental.
       congruence.
     }
 
-    iApply (wp_WriteSR with "[$Ha $Hmap]"); eauto.
+    iApply (wp_SpecialRW with "[$Ha $Hmap]"); eauto.
     { simplify_map_eq; auto. }
     { rewrite /subseteq /map_subseteq. intros rr _.
       apply elem_of_dom. apply lookup_insert_is_Some'; eauto. }
     { by rewrite HpXRS. }
 
     iIntros "!>" (regs' retv). iDestruct 1 as (HSpec) "[Ha Hmap]".
-    destruct HSpec; cycle 1.
+    destruct HSpec; cycle 2.
     - iApply wp_pure_step_later; auto. iNext; iIntros "_".
       iApply wp_value; auto.
     - simplify_map_eq; congruence.
+    - simplify_map_eq; congruence.
   Qed.
 
 End fundamental.

theories/logrel/fundamental.v

@@ -1,6 +1,6 @@
 From cap_machine Require Export
   Jmp Jnz Jalr Mov Load Store BinOp Restrict
-  Subseg Get Lea Seal UnSeal ReadSR WriteSR.
+  Subseg Get Lea Seal UnSeal SpecialRW.
 From cap_machine Require Export ftlr_base.
 From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Import weakestpre adequacy lifting.
@@ -316,15 +316,8 @@ Section fundamental.
                [$Hw] [$Hcont] [//] [$Hsts] [$Hown] [$Hframe]
                [$Hr] [$Hstate] [$Ha] [$HPC] [Hmreg]")
       ;eauto.
-    + (* ReadSR *)
-      iApply (readsr_case with
-               "[$IH] [$Hinv_interp] [$Hreg] [$Hrela]
-               [$Hrcond] [$Hwcond]  [$HmonoR] [$HmonoV]
-               [$Hw] [$Hcont] [//] [$Hsts] [$Hown] [$Hframe]
-               [$Hr] [$Hstate] [$Ha] [$HPC] [Hmreg]")
-      ;eauto.
-    + (* WriteSR *)
-      iApply (writesr_case with
+    + (* SpecialRW *)
+      iApply (specialrw_case with
                "[$IH] [$Hinv_interp] [$Hreg] [$Hrela]
                [$Hrcond] [$Hwcond]  [$HmonoR] [$HmonoV]
                [$Hw] [$Hcont] [//] [$Hsts] [$Hown] [$Hframe]

theories/opsem/assembler.v

@@ -66,8 +66,7 @@ Module Asm_Griotte.
   | GetOType (dst r: RegName)
   | Seal (dst : RegName) (r1 r2: RegName)
   | UnSeal (dst : RegName) (r1 r2: RegName)
-  | ReadSR (dst: RegName) (src: SRegName)
-  | WriteSR (dst: SRegName) (src: RegName)
+  | SpecialRW (dst: RegName) (csr: SRegName) (src: RegName)
   | Fail
   | Halt.
 
@@ -207,10 +206,8 @@ Module Asm_Griotte.
         Some (Seal dst r1 r2)
     | UnSeal dst r1 r2 =>
         Some (UnSeal dst r1 r2)
-    | ReadSR dst src =>
-        Some (ReadSR dst src)
-    | WriteSR dst src =>
-        Some (WriteSR dst src)
+    | SpecialRW dst csr src =>
+        Some (SpecialRW dst csr src)
     | Fail=>
         Some (Fail)
     | Halt=>
@@ -354,10 +351,8 @@ Module Asm_Griotte.
         Some (machine_base.Seal dst r1 r2)
     | UnSeal dst r1 r2 =>
         Some (machine_base.UnSeal dst r1 r2)
-    | ReadSR dst src =>
-        Some (machine_base.ReadSR dst src)
-    | WriteSR dst src =>
-        Some (machine_base.WriteSR dst src)
+    | SpecialRW dst csr src =>
+        Some (machine_base.SpecialRW dst csr src)
     | Fail=>
         Some (machine_base.Fail)
     | Halt=>
@@ -572,12 +567,10 @@ Module Asm_Griotte.
         let r1 := revert_regs r1 in
         let r2 := revert_regs r2 in
         (machine_base.UnSeal dst r1 r2)
-    | machine_base.ReadSR dst src =>
+    | machine_base.SpecialRW dst csr src =>
         let dst := revert_regs dst in
-        (machine_base.ReadSR dst src)
-    | machine_base.WriteSR dst src =>
         let src := revert_regs src in
-        (machine_base.WriteSR dst src)
+        (machine_base.SpecialRW dst csr src)
     | machine_base.Fail=>
         (machine_base.Fail)
     | machine_base.Halt=>
@@ -638,10 +631,14 @@ Module Asm_Griotte.
   Definition getotype dst src := (ASM_Instr (GetOType dst src)).
   Definition seal dst r1 r2 := (ASM_Instr (Seal dst r1 r2)).
   Definition unseal dst r1 r2 := (ASM_Instr (UnSeal dst r1 r2)).
-  Definition readsr dst src := (ASM_Instr (ReadSR dst src)).
-  Definition writesr dst src := (ASM_Instr (WriteSR dst src)).
+  Definition specialrw dst csr src := (ASM_Instr (SpecialRW dst csr src)).
   Definition fail:= (ASM_Instr Fail).
   Definition halt:= (ASM_Instr Halt).
   Notation "# s" := (ASM_Label s) (at level 50).
 
+  (** Aliases *)
+  Definition readsr dst csr := specialrw dst csr cnull.
+  Definition writesr csr src := specialrw cnull csr src.
+  Definition ret rsrc := jalr cnull rsrc.
+
 End Asm_Griotte.

theories/opsem/cap_lang.v

@@ -410,13 +410,15 @@ Section opsem.
         else None
     | _,_ => None
     end
-  | ReadSR dst src =>
+  | SpecialRW dst csr src =>
       if has_sreg_access plevel
-      then tomov ← (sreg φ) !! src; updatePC (update_reg φ dst tomov)
-      else None
-  | WriteSR dst src =>
-      if has_sreg_access plevel
-      then tomov ← (reg φ) !!ᵣ src; updatePC (update_sreg φ dst tomov)
+      then
+        csr_val ← (sreg φ) !! csr;
+        if (decide (src = cnull))
+        then updatePC (update_reg φ dst csr_val)
+        else
+          src_val ← (reg φ) !!ᵣ src;
+          updatePC (update_reg (update_sreg φ csr src_val) dst csr_val)
       else None
   end.
 

theories/opsem/machine_base.v

@@ -146,8 +146,7 @@ Inductive instr: Type :=
 | Seal (dst : RegName) (r1 r2: RegName)
 | UnSeal (dst : RegName) (r1 r2: RegName)
 (* Separate SpecialRW into 2 instructions *)
-| ReadSR (dst: RegName) (src: SRegName)
-| WriteSR (dst: SRegName) (src: RegName)
+| SpecialRW (dst: RegName) (csr : SRegName) (src: RegName)
 | Fail
 | Halt.
 
@@ -1528,16 +1527,15 @@ Proof.
 
       | Seal dst r1 r2 => GenNode 18 [GenLeaf (inl (inl dst)); GenLeaf (inl (inl r1)); GenLeaf (inl (inl r2))]
       | UnSeal dst r1 r2 => GenNode 19 [GenLeaf (inl (inl dst)); GenLeaf (inl (inl r1)); GenLeaf (inl (inl r2))]
-      | ReadSR dst src => GenNode 20 [GenLeaf (inl (inl dst)); GenLeaf (inl (inr src))]
-      | WriteSR dst src => GenNode 21 [GenLeaf (inl (inr dst)); GenLeaf (inl (inl src))]
-      | Fail => GenNode 22 []
-      | Halt => GenNode 23 []
-      | Mul dst r1 r2 => GenNode 24 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
-      | LAnd dst r1 r2 => GenNode 25 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
-      | LOr dst r1 r2 => GenNode 26 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
-      | LShiftL dst r1 r2 => GenNode 27 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
-      | LShiftR dst r1 r2 => GenNode 28 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
-      | Jalr dst src => GenNode 29 [GenLeaf (inl (inl dst));GenLeaf (inl (inl src))]
+      | SpecialRW dst csr src => GenNode 20 [GenLeaf (inl (inl dst)); GenLeaf (inl (inr csr)); GenLeaf (inl (inl src))]
+      | Fail => GenNode 21 []
+      | Halt => GenNode 22 []
+      | Mul dst r1 r2 => GenNode 23 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
+      | LAnd dst r1 r2 => GenNode 24 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
+      | LOr dst r1 r2 => GenNode 25 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
+      | LShiftL dst r1 r2 => GenNode 26 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
+      | LShiftR dst r1 r2 => GenNode 27 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)]
+      | Jalr dst src => GenNode 28 [GenLeaf (inl (inl dst));GenLeaf (inl (inl src))]
       end).
   set (dec := fun e =>
       match e with
@@ -1563,16 +1561,16 @@ Proof.
 
       | GenNode 18 [GenLeaf (inl (inl dst)); GenLeaf (inl (inl r1)); GenLeaf (inl (inl r2))] => Seal dst r1 r2
       | GenNode 19 [GenLeaf (inl (inl dst)); GenLeaf (inl (inl r1)); GenLeaf (inl (inl r2))] => UnSeal dst r1 r2
-      | GenNode 20 [GenLeaf (inl (inl dst)); GenLeaf (inl (inr src))] => ReadSR dst src
-      | GenNode 21 [GenLeaf (inl (inr dst)); GenLeaf (inl (inl src))] => WriteSR dst src
-      | GenNode 22 [] => Fail
-      | GenNode 23 [] => Halt
-      | GenNode 24 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => Mul dst r1 r2
-      | GenNode 25 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LAnd dst r1 r2
-      | GenNode 26 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LOr dst r1 r2
-      | GenNode 27 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LShiftL dst r1 r2
-      | GenNode 28 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LShiftR dst r1 r2
-      | GenNode 29 [GenLeaf (inl (inl dst));GenLeaf (inl (inl src))] => Jalr dst src
+      | GenNode 20 [GenLeaf (inl (inl dst)); GenLeaf (inl (inr csr)); GenLeaf (inl (inl src))]
+        => SpecialRW dst csr src
+      | GenNode 21 [] => Fail
+      | GenNode 22 [] => Halt
+      | GenNode 23 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => Mul dst r1 r2
+      | GenNode 24 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LAnd dst r1 r2
+      | GenNode 25 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LOr dst r1 r2
+      | GenNode 26 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LShiftL dst r1 r2
+      | GenNode 27 [GenLeaf (inl (inl dst)); GenLeaf (inr r1); GenLeaf (inr r2)] => LShiftR dst r1 r2
+      | GenNode 28 [GenLeaf (inl (inl dst));GenLeaf (inl (inl src))] => Jalr dst src
       | _ => Fail (* dummy *)
       end).
   refine (inj_countable' enc dec _).

theories/program_logic/rules.v

@@ -5,7 +5,7 @@ From cap_machine Require Export
      rules_Lea rules_Mov rules_Restrict rules_Subseg
      rules_Jmp rules_Jnz rules_Jalr
      rules_Seal rules_UnSeal
-     rules_ReadSR rules_WriteSR.
+     rules_SpecialRW.
 
 (* Program specifications