[gen] use rfi for translating lmrs, previously lrs, since PosWR is more restrictive.

Author: Shale Xiong

gen/libdir/forbidden.conf

@@ -96,13 +96,13 @@
 # `[DpAddrs* Pos*W]` are stronger than `Pos*W` as the former are a read followed by a write to the same location.
 #-safe [DpAddrs* Pos*W]
 
-# let dob = addr; [Exp & M]; lrs; [Exp & R | Imp & Tag & R]
-# let lrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R]
--safe [DpAddr*W PosWR]
+# let dob = addr; [Exp & M]; lmrs; [Exp & R | Imp & Tag & R]
+# let lmrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R]
+-safe [DpAddr*W Rfi]
 
-# let dob = data; [Exp & M]; lrs; [Exp & R | Imp & Tag & R]
-# let lrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R]
--safe [DpData*W PosWR]
+# let dob = data; [Exp & M]; lmrs; [Exp & R | Imp & Tag & R]
+# let lmrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R]
+-safe [DpData*W Rfi]
 
 # let ctrl = [Exp & R]; basic-dep; [BCC]; po
 # let IFB-ob = [Exp & R]; ctrl; [IFB]; po
@@ -238,10 +238,10 @@
 -safe LxSx Amo.Swp Amo.Cas
 
 # TODO
-# le aob = [Exp & M]; rmw; lrs; [A | Q]
-# let lrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R]
--safe [LxSx PosWR A] [Amo.Swp PosWR A] [Amo.Cas PosWR A]
--safe [LxSx PosWR Q] [Amo.Swp PosWR Q] [Amo.Cas PosWR Q]
+# le aob = [Exp & M]; rmw; lmrs; [A | Q]
+# let lmrs = [W]; ((po & same-loc) & ~(intervening(W,(po & same-loc)))); [R]
+-safe [LxSx Rfi A] [Amo.Swp Rfi A] [Amo.Cas Rfi A]
+-safe [LxSx Rfi Q] [Amo.Swp Rfi Q] [Amo.Cas Rfi Q]
 
 # TODO
 #let bob = [range([A];amo;[L])]; po; [Exp & M | Imp & Tag & R | MMU & FAULT]