[herd, litmus] Introduce execute bit in PTEs

Author: diaolo01

herd/AArch64Sem.ml

@@ -717,6 +717,7 @@ module Make
         valid_v : V.v;
         el0_v : V.v;
         tagged_v : V.v;
+        x_v : V.v;
       }
 
       let arch_op1 op = M.op1 (Op.ArchOp1 op)
@@ -726,6 +727,7 @@ module Make
       let extract_dbm v = arch_op1 AArch64Op.DBM v
       let extract_valid v = arch_op1 AArch64Op.Valid v
       let extract_el0 v = arch_op1 AArch64Op.EL0 v
+      let extract_x v = arch_op1 AArch64Op.X v
       let extract_oa v = arch_op1 AArch64Op.OA v
       let extract_tagged v = arch_op1 AArch64Op.Tagged v
 
@@ -791,9 +793,10 @@ module Make
         extract_af pte_v >>|
         extract_db pte_v >>|
         extract_dbm pte_v >>|
-        extract_tagged pte_v) >>=
-        (fun ((((((oa_v,el0_v),valid_v),af_v),db_v),dbm_v),tagged_v) ->
-          M.unitT {oa_v; af_v; db_v; dbm_v; valid_v; el0_v; tagged_v})
+        extract_tagged pte_v >>|
+        extract_x pte_v) >>=
+        (fun (((((((oa_v,el0_v),valid_v),af_v),db_v),dbm_v),tagged_v),x_v) ->
+          M.unitT {oa_v; af_v; db_v; dbm_v; valid_v; el0_v; tagged_v; x_v})
 
       let get_oa a_virt mpte =
         (M.op1 Op.Offset a_virt >>| mpte)
@@ -976,6 +979,12 @@ module Make
           if not ii.A.in_handler && is_el0 then
                fun pte_v -> m_op Op.Or (is_zero pte_v.el0_v) (m pte_v)
              else m in
+        let execute_check cond =
+          match domain with
+          | DISide.Instr ->
+              fun pte_v ->
+                m_op Op.Or (cond pte_v) (is_zero pte_v.x_v)
+          | _ -> cond in
 
         let open DirtyBit in
         let tthm = dirty.tthm proc
@@ -985,20 +994,26 @@ module Make
         let mfault (_,ipte) m =
           let open FaultType.AArch64 in
           let open DISide in
+          let transl_fault = M.unitT (Some (MMU (domain, Translation))) in
+          let perm_fault = M.unitT (Some (MMU (domain, Permission))) in
+          let af_fault = M.unitT (Some (MMU (domain, AccessFlag))) in
+          let perm =
+            match domain with
+            | Instr ->
+                (is_zero ipte.x_v) >>=
+                  fun x ->
+                    M.choiceT x perm_fault perm_fault
+            | _ -> perm_fault in
+          let af =
+            if ha then perm
+            else
+              (is_zero ipte.af_v) >>=
+                fun af ->
+                  M.choiceT af af_fault perm in
           (is_zero ipte.valid_v) >>=
-            (fun c ->
-              M.choiceT c
-                (M.unitT (Some (MMU (domain, Translation))))
-                (if ha then
-                   M.unitT (Some (MMU (domain, Permission)))
-                 else begin
-                   (is_zero ipte.af_v) >>=
-                     (fun c ->
-                       M.choiceT c
-                        (M.unitT (Some (MMU (domain, AccessFlag))))
-                         (M.unitT (Some (MMU (domain, Permission)))))
-                   end) >>=
-                fun t -> mfault (get_oa a_virt m) a_virt t)
+            fun v ->
+              M.choiceT v transl_fault af >>= fun t ->
+              mfault (get_oa a_virt m) a_virt t
         and mok (pte_v,ipte) a_pte m a =
           let m =
             let msg =
@@ -1081,13 +1096,15 @@ module Make
               | Dir.W ->
                   fun pte_v ->
                     m_op Op.Or (cond_R pte_v) (is_zero pte_v.db_v) in
+              let cond = execute_check cond in
               check_cond cond
             else if (tthm && ha && not hd) then (* HW managment of AF *)
               let cond = match dir with (* Do not check AF *)
               | Dir.R -> fun pte_v -> is_zero pte_v.valid_v
               | Dir.W ->
                   fun pte_v ->
                     m_op Op.Or (is_zero pte_v.valid_v) (is_zero pte_v.db_v) in
+              let cond = execute_check cond in
               check_cond cond
             else (* HW management of AF and DB *)
               let cond = match dir with (* Do not check AF *)
@@ -1099,6 +1116,7 @@ module Make
                       (is_zero pte_v.valid_v)
                       (m_op Op.And
                          (is_zero pte_v.db_v) (is_zero pte_v.dbm_v)) in
+              let cond = execute_check cond in
               check_cond cond)
           end in
         if pte2 then  mvirt

herd/tests/instructions/AArch64.vmsa+ifetch/A010.litmus

@@ -6,4 +6,4 @@ TTD(P0:Page0)=(oa:PA(P0:Page0),x:0);
 P0          ;
 Page0:      ;
 ADD W0,W0,#1;
-forall Fault(P0:Page0,MMU:Permission)
+forall Fault(P0:Page0,I-MMU:Permission)

herd/tests/instructions/AArch64.vmsa+ifetch/A010.litmus.expected

@@ -0,0 +1,10 @@
+Test A010 Required
+States 1
+ Fault(P0:Page0,label:"P0:Page0",I-MMU:Permission);
+Ok
+Witnesses
+Positive: 1 Negative: 0
+Flag combining-vmsa-and-ifetch-is-not-supported
+Condition forall (fault(P0:Page0,I-MMU:Permission))
+Observation A008 Always 1 0
+Hash=cb0a8561acabcc5a329a5e61f8d9d457

herd/tests/instructions/AArch64.vmsa+ifetch/A010.litmus.expected-failure

@@ -0,0 +1,10 @@
+Test A011 Required
+States 1
+0:X0=1;
+Ok
+Witnesses
+Positive: 1 Negative: 0
+Flag combining-vmsa-and-ifetch-is-not-supported
+Condition forall (0:X0=1)
+Observation A007 Always 1 0
+Hash=664b4fb6731a307c4de1b8e71c757cb3

herd/tests/instructions/AArch64.vmsa+ifetch/A011.litmus.expected

@@ -22,6 +22,7 @@ type 'op1 unop =
   | DBM (* get DBM from PTE entry *)
   | Valid (* get Valid bit from PTE entry *)
   | EL0 (* get EL0 bit from PTE entry *)
+  | X (* get execute permission bit from PTE entry *)
   | OA (* get OA from PTE entry *)
   | SetOA (* store OA into PAR_EL1 *)
   | SetF (* set F to 1 in PAR_EL1 *)
@@ -71,6 +72,7 @@ module
       | DBM -> "DBM"
       | Valid -> "Valid"
       | EL0 -> "EL0"
+      | X -> "X"
       | OA -> "OA"
       | SetOA -> "SetOA"
       | SetF -> "SetF"
@@ -137,6 +139,7 @@ module
     let getvalid = op_get_pteval (fun p -> p.valid <> 0)
 
     let getel0 = op_get_pteval (fun p -> p.el0 <> 0)
+    let getx = op_get_pteval (fun p -> p.x <> 0)
 
     let gettagged = op_get_pteval (fun p -> Attrs.is_tagged p.attrs)
 
@@ -215,6 +218,7 @@ module
       | DBM -> getdbm
       | Valid -> getvalid
       | EL0 -> getel0
+      | X -> getx
       | OA -> getoa
       | SetOA -> setoa
       | SetF -> setf

herd/tests/instructions/AArch64.vmsa+ifetch/A011.litmus.expected-failure

@@ -187,6 +187,7 @@ type t = {
   db : int;
   dbm : int;
   el0 : int;
+  x : int;
   attrs: Attrs.t;
   }
 
@@ -199,6 +200,7 @@ let eq_props p1 p2 =
   Misc.int_eq p1.dbm p2.dbm &&
   Misc.int_eq p1.valid p2.valid &&
   Misc.int_eq p1.el0 p2.el0 &&
+  Misc.int_eq p1.x p2.x &&
   Attrs.eq p1.attrs p2.attrs
 
 (* Let us abstract... *)
@@ -217,7 +219,7 @@ let get_attrs {attrs;_ } = Attrs.as_list attrs
 
 let prot_default =
   { oa=OutputAddress.PHY "";
-    valid=1; af=1; db=1; dbm=0; el0=1; attrs=Attrs.default; }
+    valid=1; af=1; db=1; dbm=0; el0=1; x=1; attrs=Attrs.default; }
 
 let default s = { prot_default with  oa=OutputAddress.PHY s; }
 
@@ -240,6 +242,7 @@ and pp_af hexa ok = pp_int_field hexa ok "af" (fun p -> p.af)
 and pp_db hexa ok = pp_int_field hexa ok "db" (fun p -> p.db)
 and pp_dbm hexa ok = pp_int_field hexa ok "dbm" (fun p -> p.dbm)
 and pp_el0 hexa ok = pp_int_field hexa ok "el0" (fun p -> p.el0)
+and pp_x hexa ok = pp_int_field hexa ok "x" (fun p -> p.x)
 and pp_attrs compat ok = pp_field ok
     (fun a -> sprintf (if compat then "%s" else "attrs:(%s)") (Attrs.pp a)) Attrs.eq (fun p -> p.attrs)
 
@@ -254,6 +257,7 @@ let is_default_attrs t = Attrs.is_default t.attrs
    (2) Fields from el0 (included) are printed if non-default. *)
 
 let pp_fields hexa showall p k =
+  let k = pp_x hexa false p k in
   let k = pp_el0 hexa false p k in
   let k = pp_valid hexa showall p k in
   let k = pp_dbm hexa showall p k in
@@ -291,6 +295,7 @@ let add_field k v p =
   | "dbm" -> { p with dbm = my_int_of_string k v }
   | "valid" -> { p with valid = my_int_of_string k v }
   | "el0" -> { p with el0 = my_int_of_string k v }
+  | "x" -> { p with x = my_int_of_string k v }
   | _ ->
       Warn.user_error "Illegal AArch64 page table entry property %s" k
 
@@ -326,17 +331,19 @@ let compare =
     lex_compare (fun p1 p2 -> OutputAddress.compare p1.oa p2.oa) cmp in
   let cmp =
     lex_compare (fun p1 p2 -> Attrs.compare p1.attrs p2.attrs) cmp in
+  let cmp =
+    lex_compare (fun p1 p2 -> Misc.int_compare p1.x p2.x) cmp in
   cmp
 
 let eq p1 p2 = OutputAddress.eq p1.oa p2.oa && eq_props p1 p2
 
 (* For litmus *)
 
 (* Those lists must of course match one with the other *)
-let fields = ["af";"db";"dbm";"valid";"el0";]
+let fields = ["af";"db";"dbm";"valid";"el0";"x";]
 and default_fields =
   let p = prot_default in
-  let ds = [p.af; p.db; p.dbm; p.valid;p.el0;] in
+  let ds = [p.af; p.db; p.dbm; p.valid; p.el0; p.x;] in
   List.map (Printf.sprintf "%i") ds
 
 let norm =
@@ -361,9 +368,9 @@ let norm =
 
 let dump_pack pp_oa p =
   sprintf
-    "pack_pack(%s,%d,%d,%d,%d,%d)"
+    "pack_pack(%s,%d,%d,%d,%d,%d,%d)"
     (pp_oa (OutputAddress.pp_old p.oa))
-    p.af p.db p.dbm p.valid p.el0
+    p.af p.db p.dbm p.valid p.el0 p.x
 
 let as_physical p = OutputAddress.as_physical p.oa
 
@@ -376,7 +383,8 @@ let as_flags p =
         (add p.valid "msk_valid"
            (add p.af "msk_af"
               (add p.dbm "msk_dbm"
-                 (add p.db "msk_db" [])))) in
+                 (add p.db "msk_db"
+                    (add p.x "msk_x" []))))) in
     let msk = String.concat "|" msk in
     Some msk
 
@@ -392,12 +400,14 @@ let mask_el0 = Int64.shift_left 1L 6
 let mask_db = Int64.shift_left 1L 7
 let mask_af = Int64.shift_left 1L 10
 let mask_dbm = Int64.shift_left 1L 51
+let mask_x = Int64.shift_left 1L 54
 let mask_all_neg =
   Int64.lognot
-    (Int64.logor mask_el0
-       (Int64.logor
-          (Int64.logor mask_valid  mask_db)
-          (Int64.logor  mask_af  mask_dbm)))
+    (Int64.logor mask_x
+       (Int64.logor mask_el0
+          (Int64.logor
+              (Int64.logor mask_valid  mask_db)
+              (Int64.logor  mask_af  mask_dbm))))
 
 let is_zero v = Int64.equal 0L v
 let is_set v m = not (is_zero (Int64.logand v m))
@@ -410,6 +420,7 @@ let orop p m =
     let p = if is_set m mask_db then { p with db=0; } else p in
     let p = if is_set m mask_af then { p with af=1; } else p in
     let p = if is_set m mask_dbm then { p with dbm=1; } else p in
+    let p = if is_set m mask_x then { p with x=1; } else p in
     Some p
 
 and andnot2 p m =
@@ -420,6 +431,7 @@ and andnot2 p m =
     let p = if is_set m mask_db then { p with db=1; } else p in
     let p = if is_set m mask_af then { p with af=0; } else p in
     let p = if is_set m mask_dbm then { p with dbm=0; } else p in
+    let p = if is_set m mask_x then { p with x=0; } else p in
     Some p
 
 and andop p m =
@@ -439,4 +451,7 @@ and andop p m =
   let r =
     if is_set m mask_dbm && p.dbm=1
     then Int64.logor r mask_dbm else r  in
+  let r =
+    if is_set m mask_x && p.x=1
+    then Int64.logor r mask_x else r  in
   Some r

lib/AArch64Op.ml

@@ -35,6 +35,7 @@ type t = {
   db : int;
   dbm : int;
   el0 : int;
+  x : int;
   attrs : Attrs.t;
   }
 

lib/AArch64PteVal.ml

@@ -219,12 +219,15 @@ let do_op op c1 c2 =
               | [10] ->
                   let af = ASLScalar.bit_of_bv s2 in
                   Constant.PteVal { pte with AArch64PteVal.af;} |> return
-              | [7] ->
-                  let db = 1-ASLScalar.bit_of_bv s2 in
-                  Constant.PteVal { pte with AArch64PteVal.db;} |> return
-              | _ ->
-                  set_slice positions c1 c2
-            end
+            | [7] ->
+                let db = 1-ASLScalar.bit_of_bv s2 in
+                Constant.PteVal { pte with AArch64PteVal.db;} |> return
+            | [54] ->
+                let x = ASLScalar.bit_of_bv s2 in
+                Constant.PteVal { pte with AArch64PteVal.x;} |> return
+            | _ ->
+                set_slice positions c1 c2
+          end
         | _ -> set_slice positions c1 c2
 
 let do_op1 op cst =