[litmus] Fix x -> XN polarity

Author: diaolo01

herd/tests/instructions/AArch64.kvm/A032.litmus

@@ -0,0 +1,17 @@
+AArch64 A032
+Variant=vmsa
+{
+int x=1;
+0:X1=PTE(x);
+[PTE(x)]=(x:0);
+pteval_t 0:X0;
+
+int y=2;
+0:X3=PTE(y);
+[PTE(y)]=(x:1);
+pteval_t 0:X2;
+}
+  P0         ;
+ LDR X0,[X1] ;
+ LDR X2,[X3] ;
+forall 0:X0=(oa:PA(x),x:0) /\ 0:X2=(oa:PA(y),x:1)

herd/tests/instructions/AArch64.kvm/A032.litmus.expected

@@ -0,0 +1,10 @@
+Test A032 Required
+States 1
+0:X0=(oa:PA(x), x:0); 0:X2=(oa:PA(y));
+Ok
+Witnesses
+Positive: 1 Negative: 0
+Condition forall (0:X0=(oa:PA(x), x:0) /\ 0:X2=(oa:PA(y)))
+Observation A032 Always 1 0
+Hash=6cb20add2198be8d9374dc1d759a237a
+

lib/AArch64PteVal.ml

@@ -420,7 +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
+    let p = if is_set m mask_x then { p with x=0; } else p in
     Some p
 
 and andnot2 p m =
@@ -431,7 +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
+    let p = if is_set m mask_x then { p with x=1; } else p in
     Some p
 
 and andop p m =
@@ -452,6 +452,6 @@ and andop p m =
     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
+    if is_set m mask_x && p.x=0
     then Int64.logor r mask_x else r  in
   Some r

litmus/libdir/_aarch64/kvm-headers.h

@@ -108,7 +108,7 @@ static const uint64_t msk_af = 0x400UL;
 static const uint64_t msk_dbm = 0x8000000000000UL;
 static const uint64_t msk_db = 0x80UL;
 static const uint64_t msk_el0 = 0x40UL;
-static const uint64_t msk_x = 0x4000000000000UL;
+static const uint64_t msk_x = 0x40000000000000UL;
 #define  msk_full (msk_valid|msk_af|msk_dbm|msk_db|msk_el0|msk_x)
 
 static inline void unset_el0(pteval_t *p) {
@@ -117,6 +117,7 @@ static inline void unset_el0(pteval_t *p) {
 
 static inline pteval_t litmus_set_pte_flags(pteval_t old,pteval_t flags) {
   flags ^= msk_db; /* inverse dirty bit -> AP[2] */
+  flags ^= msk_x;  /* inverse XN bit */
   old &= ~msk_full ;
   old |= flags ;
   return old ;
@@ -218,7 +219,7 @@ inline static pteval_t pack_pte(int oa,pteval_t v) {
     pack_flag(v ^ msk_db,msk_db,DB_PACKED) |
     pack_flag(v,msk_dbm,DBM_PACKED) |
     pack_flag(v,msk_valid,VALID_PACKED) |
-    pack_flag(v,msk_x,X_PACKED) |
+    pack_flag(v ^ msk_x,msk_x,X_PACKED) |
     pack_flag(v,msk_el0,EL0_PACKED) ;
 }
 
@@ -244,7 +245,7 @@ pack_pack(int oa,int af,int db,int dbm,int valid,int el0,int x) {
   - db set       -> corresponding bit unset
 */
 
-#define NULL_PACKED (pack_pack(NVARS,0,1,0,0,0,0))
+#define NULL_PACKED (pack_pack(NVARS,0,1,0,0,0,1))
 
 inline static int unpack_oa(pteval_t v) {
   return v >> OA_PACKED;