[asl] Partition PSTATE accesses.

Accesses to PSTATE get partitioned:
  + Accesses to the N,Z,C and V fields are to variable `_NZCV`.
  + Other accesses and to the variable `_PSTATE`.

We use the previous reduction of some get and set fields to
function calls. Overall the trick works but remains quite brittle.
  1. _NZCV is targetted when all fields are in {N,Z,C,V}.
  2. Getters are setters are defined only up to four bit accesses.

asllib/Interpreter.ml

@@ -199,8 +199,13 @@ module Make (B : Backend.S) (C : Config) = struct
                 | None, Some t -> base_value env t
               in
               let* () =
+(*
+ * Those identifiers are initialised to their current value
+ * before executing each instruction. Hence, we discard
+ * the initial values from `.asl` files.
+ *)
                 match name with
-                | "PSTATE" | "RESADDR" -> return ()
+                | "RESADDR" | "_NZCV" -> return ()
                 | _ -> B.on_write_identifier name Scope_Global v
               in
               IEnv.declare_global name v env |> return

herd/AArch64ASLSem.ml

@@ -808,12 +808,12 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
               | _ -> st)
             ASLS.A.state_empty ASLBase.gregs
         in
-        let nzcv = AArch64Base.NZCV and pstate = global_loc "PSTATE" in
+        let nzcv = AArch64Base.NZCV and _nzcv = global_loc "_NZCV" in
         let st =
           match A.look_reg nzcv ii.A.env.A.regs with
           | Some v ->
               let v = aarch64_to_asl_bv v in
-              ASLS.A.state_add st pstate v
+              ASLS.A.state_add st _nzcv v
           | _ -> st
         in
         let regq = AArch64Base.ResAddr and resaddr = global_loc "RESADDR" in

herd/ASLSem.ml

@@ -309,17 +309,17 @@ module Make (C : Config) = struct
             let* v1 = m1 () and* v2 = m2 () and* v = to_int_signed v in
             M.op3 Op.If v v1 v2
 
-    (* Any access to PSTATE emits an access to NZCV.
+    (* Any access to `_NZCV` emits an access to NZCV.
      * Notice that the value is casted into an integer.
      *)
-    let is_pstate x scope =
-      match (x, scope) with "PSTATE", AST.Scope_Global -> true | _ -> false
+    let is_nzcv x scope =
+      match (x, scope) with "_NZCV", AST.Scope_Global -> true | _ -> false
 
     let is_resaddr x scope =
       match (x, scope) with "RESADDR", AST.Scope_Global -> true | _ -> false
 
     let loc_of_scoped_id ii x scope =
-      if is_pstate x scope then
+      if is_nzcv x scope then
         A.Location_reg (ii.A.proc, ASLBase.ArchReg AArch64Base.NZCV)
       else if is_resaddr x scope then
         A.Location_reg (ii.A.proc, ASLBase.ArchReg AArch64Base.ResAddr)
@@ -331,7 +331,7 @@ module Make (C : Config) = struct
         let action = Act.Access (dir, loc, v, MachSize.Quad, aneutral) in
         M.mk_singleton_es action (use_ii_with_poi ii poi)
       in
-      if is_pstate x scope then M.op1 (Op.ArchOp1 ASLOp.ToIntU) v >>= m else m v
+      if is_nzcv x scope then M.op1 (Op.ArchOp1 ASLOp.ToIntU) v >>= m else m v
 
     let on_write_identifier = on_access_identifier Dir.W
     and on_read_identifier = on_access_identifier Dir.R

herd/libdir/asl-pseudocode/patches.asl

@@ -89,7 +89,96 @@ type ProcState of bits(64) {
     [47:42] M         // Mode field                         [AArch32 only]
 };
 
-var PSTATE : ProcState;
+var _PSTATE : ProcState;
+var _NZCV : ProcState;
+
+func isNZCV(n:integer) => boolean
+begin
+  return 0 <= n && n < 4 ;
+end
+
+getter PSTATE[] => ProcState
+begin
+ return _PSTATE;
+end
+
+setter PSTATE[] = v : ProcState
+begin
+  _PSTATE = v;
+end
+
+getter PSTATE[n:integer] => bits(1)
+begin
+  if isNZCV(n) then
+    return _NZCV[n];
+  else
+    return _PSTATE[n];
+  end
+end
+
+setter PSTATE[n:integer] = v : bits(1)
+begin
+  if isNZCV(n) then
+    _NZCV[n] = v;
+  else
+    _PSTATE[n] = v;
+  end
+end
+
+
+getter PSTATE[n:integer,m:integer] => bits(2)
+begin
+  if isNZCV(n) && isNZCV(m) then
+    return _NZCV[n,m];
+  else
+    return _PSTATE[n,m];
+  end
+end
+
+setter PSTATE[n:integer,m:integer] = v : bits(2)
+begin
+  if isNZCV(n) && isNZCV(m) then
+    _NZCV[n,m] = v;
+  else
+    _PSTATE[n,m] = v;
+  end
+end
+
+getter PSTATE[n:integer,m:integer,o:integer] => bits(3)
+begin
+  if isNZCV(n) && isNZCV(m) && isNZCV(o) then
+    return _NZCV[n,m,o];
+  else
+    return _PSTATE[n,m,o];
+  end
+end
+
+setter PSTATE[n:integer,m:integer,o:integer] = v : bits(3)
+begin
+  if isNZCV(n) && isNZCV(m) && isNZCV(o) then
+    _NZCV[n,m,o] = v;
+  else
+    _PSTATE[n,m,o] = v;
+  end
+end
+
+getter PSTATE[n:integer,m:integer,o:integer,p:integer] => bits(4)
+begin
+  if isNZCV(n) && isNZCV(m) && isNZCV(o) && isNZCV(p) then
+    return _NZCV[n,m,o,p];
+  else
+    return _PSTATE[n,m,o,p];
+  end
+end
+
+setter PSTATE[n:integer,m:integer,o:integer,p:integer] = v : bits(4)
+begin
+  if isNZCV(n) && isNZCV(m) && isNZCV(o) && isNZCV(p) then
+    _NZCV[n,m,o,p] = v;
+  else
+    _PSTATE[n,m,o,p] = v;
+  end
+end
 
 // GenerateAddress()
 // =================