From 50436ed0332d6111cc874cf121528c24543005e7 Mon Sep 17 00:00:00 2001 From: Luc Maranget Date: Mon, 25 Mar 2024 17:48:02 +0100 Subject: [PATCH] [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 | 7 +- herd/AArch64ASLSem.ml | 4 +- herd/ASLSem.ml | 10 +-- herd/libdir/asl-pseudocode/patches.asl | 91 +++++++++++++++++++++++++- 4 files changed, 103 insertions(+), 9 deletions(-) diff --git a/asllib/Interpreter.ml b/asllib/Interpreter.ml index 7935a6bc3..18e1405e5 100644 --- a/asllib/Interpreter.ml +++ b/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 diff --git a/herd/AArch64ASLSem.ml b/herd/AArch64ASLSem.ml index bf26dd359..a0340d48d 100644 --- a/herd/AArch64ASLSem.ml +++ b/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 diff --git a/herd/ASLSem.ml b/herd/ASLSem.ml index 9b394bd11..3cf1c2fed 100644 --- a/herd/ASLSem.ml +++ b/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 diff --git a/herd/libdir/asl-pseudocode/patches.asl b/herd/libdir/asl-pseudocode/patches.asl index a2e2ddc86..8dbe38dbe 100644 --- a/herd/libdir/asl-pseudocode/patches.asl +++ b/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() // =================