checking in in-progress translation of Shaked's handwritten sail1 ARM model to sail2

1 files changed, 599 insertions, 0 deletions

diff --git a/aarch64_small/aarch64_regfp.sail b/aarch64_small/aarch64_regfp.sail
new file mode 100644
index 00000000..0bb79f8f
--- /dev/null
+++ b/aarch64_small/aarch64_regfp.sail
@@ -0,0 +1,599 @@
+/*========================================================================*/
+/*                                                                        */
+/*  Copyright (c) 2015-2017 Shaked Flur                                   */
+/*  Copyright (c) 2015-2017 Kathyrn Gray                                  */
+/*  All rights reserved.                                                  */
+/*                                                                        */
+/*  This software was developed by the University of Cambridge Computer   */
+/*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  */
+/*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   */
+/*                                                                        */
+/*  Redistribution and use in source and binary forms, with or without    */
+/*  modification, are permitted provided that the following conditions    */
+/*  are met:                                                              */
+/*  1. Redistributions of source code must retain the above copyright     */
+/*     notice, this list of conditions and the following disclaimer.      */
+/*  2. Redistributions in binary form must reproduce the above copyright  */
+/*     notice, this list of conditions and the following disclaimer in    */
+/*     the documentation and/or other materials provided with the         */
+/*     distribution.                                                      */
+/*                                                                        */
+/*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    */
+/*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     */
+/*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       */
+/*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   */
+/*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          */
+/*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      */
+/*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      */
+/*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   */
+/*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    */
+/*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    */
+/*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    */
+/*  SUCH DAMAGE.                                                          */
+/*========================================================================*/
+
+val rmem_kind : (AccType, bool) -> instruction_kind 
+function rmem_kind (acctype, exclusive) =
+  if exclusive then
+    match acctype {
+      AccType_ATOMIC   => IK_mem_read(Read_exclusive),
+      AccType_ORDERED  => IK_mem_read(Read_exclusive_acquire),
+      _  => { not_implemented("unimplemented memory access");
+                  IK_mem_read(Read_exclusive); }
+    }
+  else
+    match acctype {
+      AccType_NORMAL   => IK_mem_read(Read_plain),
+      AccType_ATOMIC   => IK_mem_read(Read_plain),
+      AccType_STREAM   => IK_mem_read(Read_stream),
+      AccType_UNPRIV   => IK_mem_read(Read_plain),
+      AccType_ORDERED  => IK_mem_read(Read_acquire)
+    }
+
+
+function instruction_kind wmem_kind (acctype : (AccType), exclusive : (bool)) =
+  if exclusive then {
+    match acctype {
+      AccType_ATOMIC   => IK_mem_write(Write_exclusive),
+      AccType_ORDERED  => IK_mem_write(Write_exclusive_release),
+      _  => { not_implemented("unimplemented memory access");
+                  IK_mem_write(Write_exclusive); }
+    }
+  } else {
+    match acctype {
+      AccType_NORMAL   => IK_mem_write(Write_plain),
+      AccType_STREAM   => IK_mem_write(Write_plain),
+      AccType_UNPRIV   => IK_mem_write(Write_plain),
+      AccType_ORDERED  => IK_mem_write(Write_release),
+      _  => { not_implemented("unimplemented memory access");
+                  IK_mem_write(Write_plain) }
+    };
+  }
+
+
+let _Rs : vector(31,dec,string) =
+  ["R30","R29","R28","R27","R26","R25","R24","R23","R22","R21",
+   "R20","R19","R18","R17","R16","R15","R14","R13","R12","R11",
+   "R10","R9" ,"R8" ,"R7" ,"R6" ,"R5" ,"R4" ,"R3" ,"R2" ,"R1" ,
+   "R0"]
+
+let TxNestingLevelfp  = RFull("TxNestingLevel")
+let TXIDR_EL0_DEPTHfp = RField("TXIDR_EL0","DEPTH")
+
+let PSTATE_Nfp  = RField("NZCV","N")
+let PSTATE_Zfp  = RField("NZCV","Z")
+let PSTATE_Cfp  = RField("NZCV","C")
+let PSTATE_Vfp  = RField("NZCV","V")
+let PSTATE_Dfp  = RField("DAIF","D")
+let PSTATE_Afp  = RField("DAIF","A")
+let PSTATE_Ifp  = RField("DAIF","I")
+let PSTATE_Ffp  = RField("DAIF","F")
+let PSTATE_ELfp = RFull("CurrentEL")
+let PSTATE_SPfp = RField("SPSel","SP")
+let _PCfp       = RFull("_PC")
+
+let NZCVfp = [| PSTATE_Nfp, PSTATE_Zfp, PSTATE_Cfp, PSTATE_Vfp |]
+
+function regfps xFP(n : (reg_index)) =
+  if n != 31 then [|RFull(_Rs[n])|] else [| |]
+
+
+/* check if this is still what we want */
+function BranchToFP forall 'N, 'N in {32,64}.  (iR,oR) -> (regfps,regfps) =
+  (if UsingAArch32() then iR else PSTATE_ELfp :: iR, _PCfp :: oR)
+
+function regfps ConditionHoldsIFP(_cond : (bits(4))) =
+  match _cond[3..1] {
+    0b000  => [| PSTATE_Zfp |],
+    0b001  => [| PSTATE_Cfp |],
+    0b010  => [| PSTATE_Nfp |],
+    0b011  => [| PSTATE_Vfp |],
+    0b100  => [| PSTATE_Cfp, PSTATE_Zfp |],
+    0b101  => [| PSTATE_Nfp, PSTATE_Vfp |],
+    0b110  => [| PSTATE_Nfp, PSTATE_Vfp, PSTATE_Zfp |],
+    0b111  => [| |]
+  }
+
+/* for iR if rSPFP, for oR if wSPFP */
+let rSPIFP = 
+  /* TODO: actually this depends on runtime data: PSTATE_SP and PSTATE_EL */
+  [| PSTATE_SPfp, RFull("SP_EL0") |]
+
+let wSPFP = 
+  /* TODO: actually this depends on runtime data: PSTATE_SP and PSTATE_EL */
+  ([| PSTATE_SPfp |],
+   [| RFull("SP_EL0") |])
+
+
+let CheckSPAlignmentIFP = PSTATE_ELfp :: rSPIFP
+
+let BigEndianIFP =
+  if UsingAArch32() then [| RFull("PSTATE_E") |] else [| PSTATE_ELfp |] 
+
+let wMem'IFP = BigEndianIFP 
+let wMemIFP = wMem'IFP
+
+function initial_analysis (instr) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = {
+  iR = [| |];
+  oR = [| |];
+  aR = [| |];
+  Nias = [| NIAFP_successor |];
+  Dia = DIAFP_none;
+  ik = IK_simple;
+
+  match instr {
+    (TMStart(t))  => {
+      iR = TxNestingLevelfp :: TXIDR_EL0_DEPTHfp :: iR;
+      /* TODO: whether the following applies depends on runtime data:
+         ~(TxNestingLevel >= TXIDR_EL0.DEPTH) */
+      oR = TxNestingLevelfp :: append(oR,xFP(t));
+      ik = IK_trans(Transaction_start);
+    },
+    (TMCommit)  => {
+      iR = TxNestingLevelfp :: iR;
+      oR = TxNestingLevelfp :: oR;
+      ik = IK_trans(Transaction_commit);
+    },
+    (TMAbort(retry,reason))  => {
+      iR = TxNestingLevelfp :: iR;
+      ik = IK_trans(Transaction_abort);
+    },
+    (TMTest)  => {
+      iR = TxNestingLevelfp :: iR;
+      oR = RFull("NZCV") :: oR;
+    },
+    (CompareAndBranch(t,datasize,iszero,offset))  => {
+      iR = append(iR,xFP(t));
+      /* TODO: whether the following applies depends on runtime data:
+         IsZero(operand1) */
+      let (i,o) = BranchToFP(iR,oR) in {iR = i; oR = o};
+      nia' : (bits(64)) = rPC() + offset;
+      Nias = [| NIAFP_successor, NIAFP_concrete_address(nia') |];
+      ik = IK_branch;
+    },
+    (BranchConditional(offset,condition))  => {
+      iR = append(iR,ConditionHoldsIFP(condition));
+      /* TODO: whether the following applies depends on runtime data:
+         ConditionHolds(condition) */
+      let (i,o) = BranchToFP(iR,oR) in {iR = i; oR = o};
+      Nias = [| NIAFP_successor, NIAFP_concrete_address(rPC() + offset) |];
+      ik = IK_branch;
+    },
+    (GenerateExceptionEL1(imm))  => not_implemented("GenerateExceptionEL1"),
+    (GenerateExceptionEL2(imm))  => not_implemented("GenerateExceptionEL2"),
+    (GenerateExceptionEL3(imm))  => not_implemented("GenerateExceptionEL3"),
+    (DebugBreakpoint(comment))  => not_implemented("DebugBreakpoint"),
+    (ExternalDebugBreakpoint)  => not_implemented("ExternalDebugBreakpoint"),
+    (DebugSwitchToExceptionLevel(target_level))  => not_implemented("DebugSwitchToExceptionLevel"),
+    (MoveSystemImmediate(operand,field))  =>
+      match field {
+        PSTATEField_SP  => oR = PSTATE_SPfp :: oR,
+        PSTATEField_DAIFSet  => {
+          iR = append(iR, [| PSTATE_Dfp, PSTATE_Afp, PSTATE_Ifp, PSTATE_Ffp |]);
+          oR = append(oR, [| PSTATE_Dfp, PSTATE_Afp, PSTATE_Ifp, PSTATE_Ffp |]);
+        },
+        PSTATEField_DAIFClr  => {
+          iR = append(iR, [| PSTATE_Dfp, PSTATE_Afp, PSTATE_Ifp, PSTATE_Ffp |]);
+          oR = append(oR, [| PSTATE_Dfp, PSTATE_Afp, PSTATE_Ifp, PSTATE_Ffp |]);
+        }
+      },
+    (Hint(op))  => 
+      match op {
+        SystemHintOp_YIELD  => (),
+        SystemHintOp_WFE  => {
+          if EventRegistered() then () /* ClearEventRegister */
+          else {
+            /* the execute code for this case always fails because of
+               WaitForEvent, declared as extern but not defined */
+            not_implemented("Hint(SystemHintOp_WFE);") 
+          }
+        },
+        SystemHintOp_WFI  => {
+            /* the execute code for this case always fails because of
+               InterruptPending, declared as extern but not defined */
+            not_implemented("Hint(SystemHintOp_WFI);") 
+        },
+        SystemHintOp_SEV  => (), /*SendEvent*/
+        SystemHintOp_SEVL  =>
+            /* the execute code for this case always fails because of
+               EventRegisterSet, declared as extern but not defined */
+            not_implemented("Hint(SystemHintOp_SEVL);"),
+        _  => () /* do nothing */ 
+      },
+    (ClearExclusiveMonitor(imm))  => (), /*ClearExclusiveLocal*/
+    (Barrier(op,domain,types))  => {
+      ik = match op {
+        MemBarrierOp_DSB  =>
+          match types {
+            MBReqTypes_Reads   => IK_barrier(Barrier_DSB_LD),
+            MBReqTypes_Writes  => IK_barrier(Barrier_DSB_ST),
+            MBReqTypes_All     => IK_barrier(Barrier_DSB)
+          },
+        MemBarrierOp_DMB  => 
+          match types {
+            MBReqTypes_Reads   => IK_barrier(Barrier_DMB_LD),
+            MBReqTypes_Writes  => IK_barrier(Barrier_DMB_ST),
+            MBReqTypes_All     => IK_barrier(Barrier_DMB)
+          },
+        MemBarrierOp_ISB  =>
+          IK_barrier(Barrier_ISB)
+      };
+    },
+    (System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result))  => {
+      oR = append(oR,xFP(t));
+      not_implemented("System"); /* because SysOp_R and SysOp_W */
+    },
+    (MoveSystemRegister(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read))  => {
+      if read then {
+        oR = append(oR,xFP(t));
+        match (sys_op0,sys_op1,sys_crn,sys_crm,sys_op2) { /* System_Get */
+          (3,3,4,2,0)  => iR = RFull("NZCV") :: iR,
+          (3,3,4,2,1)  => iR = RFull("DAIF") :: iR,
+          (3, 3, 13, 0, 2)  => iR = RFull("TPIDR_EL0") :: iR
+        /* TODO FIXME: higher EL TPIDRs */
+        }
+      } 
+      else {
+        iR = append(iR,xFP(t));
+        match (sys_op0,sys_op1,sys_crn,sys_crm,sys_op2) { /* System_Put */
+          (3,3,4,2,0)  => oR = RFull("NZCV") :: oR,
+          (3,3,4,2,1)  => oR = RFull("DAIF") :: oR,
+          (3, 3, 13, 0, 2)  => oR = RFull("TPIDR_EL0") :: oR
+        /* TODO FIXME: higher EL TPIDRs */
+        }
+      }
+    },
+    (ImplementationDefinedTestBeginEnd(isEnd))  => (),
+    (ImplementationDefinedStopFetching)  => (),
+    (ImplementationDefinedThreadStart)  => (),
+    (TestBitAndBranch(t,datasize,bit_pos,bit_val,offset))  => {
+      iR = append(xFP(t),iR);
+      /* TODO: whether the following applies depends on runtime data:
+         operand[bit_pos] == bit_val */
+      let (i,o) = BranchToFP(iR,oR) in {iR = i; oR = o}; 
+      Nias = [| NIAFP_successor, NIAFP_concrete_address(rPC() + offset) |];
+      ik = IK_branch;
+    },
+    (BranchImmediate(branch_type,offset))  => {
+      if branch_type == BranchType_CALL
+      then {iR = _PCfp :: iR; oR = append(xFP(30),oR)};
+      let (i,o) = BranchToFP(iR,oR) in {iR = i; oR = o}; 
+      Nias = [| NIAFP_concrete_address(rPC() + offset) |];
+      ik = IK_branch
+    },
+    (BranchRegister(n,branch_type))  => {
+      iR = append(iR,xFP(n));
+      if branch_type == BranchType_CALL
+      then {iR = _PCfp :: iR; oR = append(xFP(30),oR)};
+      let (i,o) = BranchToFP(iR,oR) in {iR = i; oR = o};
+      Nias = if n ==31
+              then [| NIAFP_concrete_address(0) |]
+              else [| NIAFP_indirect_address |];
+      ik = IK_branch
+    },
+    (ExceptionReturn)  => not_implemented("ExceptionReturn"),
+    (DebugRestorePState)  => not_implemented("DebugRestorePState"),
+    (LoadLiteral(t,memop,_signed,size,offset,datasize))  => {
+      /* assuming rMem doesn't touch other registers */
+      iR = _PCfp :: iR;
+      oR = append(xFP(t),oR);
+      aR = _PCfp :: aR;
+      match memop {
+        MemOp_LOAD  => ik = IK_mem_read(Read_plain),
+        MemOp_PREFETCH  => {ik = IK_simple; aR = [| |]}
+      }
+    },
+    (LoadStoreAcqExc(n,t,t2,s,acctype,excl,pair,memop,elsize,regsize,datasize))  => {
+      rt_unknown : (boolean) = false;
+      rn_unknown : (boolean) = false;
+      if n==31 then {
+        iR = append(CheckSPAlignmentIFP,iR);
+        iR = append(rSPIFP,iR);
+        aR = append(rSPIFP,aR);
+      }
+      else if rn_unknown then ()
+      else {
+        iR = append(xFP(n),iR);
+        aR = append(xFP(n),aR);
+      };
+      match memop {
+        MemOp_STORE  => {
+          if rt_unknown then ()
+          else if pair then iR = append(xFP(t),append(xFP(t2),iR))
+          else iR = append(xFP(t),iR);
+          if excl then {
+            /* TODO: the command below depends on runtime data:
+               AArch64_ExclusiveMonitorsPass(address, dbytes) */
+            iR = append(iR,wMemIFP);
+            oR = append(xFP(s),oR);
+            ik = wmem_kind(acctype,true);
+          }
+          else {
+            iR = append(iR,wMemIFP);
+            ik = wmem_kind(acctype,false);
+          }
+        },
+        MemOp_LOAD  => {
+          if pair then {
+            if rt_unknown then
+              oR = append(xFP(t),oR)
+            else if elsize == 32 then {
+              iR = append(iR,BigEndianIFP);
+              oR = append(xFP(t),append(xFP(t2),oR));
+            }
+            else {
+              oR = append(xFP(t),append(xFP(t2),oR))
+            };
+            ik = rmem_kind(acctype,true);
+          }
+          else {
+            oR = append(xFP(t),oR);
+            ik = rmem_kind(acctype,excl);
+          }
+          
+        },
+        MemOp_PREFETCH  => aR = [| |]
+      }
+    },
+    (LoadStorePairNonTemp(wback,postindex,n,t,t2,acctype,memop,scale,datasize,offset))  => {
+      rt_unknown : (boolean) = false;
+      if n == 31 then {
+        iR = append(CheckSPAlignmentIFP,iR);
+        iR = append(rSPIFP,iR);
+        aR = append(rSPIFP,aR);
+      }
+      else {
+        iR = append(xFP(n),iR);
+        aR = append(xFP(n),aR);
+      };
+      if wback then {
+        if n == 31 then
+          let (i,o) = wSPFP in {
+            iR = append(i,iR);
+            oR = append(o,oR);
+          }
+        else
+          oR = append(xFP(n),oR);
+      };
+      match memop {
+        MemOp_STORE  => {
+          if rt_unknown & t == n then ()
+          else iR = append(xFP(t),iR);
+          if rt_unknown & t2 == n then ()
+          else iR = append(xFP(t2),iR);
+          iR = append(wMemIFP,iR);
+          ik = wmem_kind(acctype,false);
+        },
+        MemOp_LOAD  => {
+          oR = append(xFP(t),append(xFP(t2),oR));
+          ik = rmem_kind(acctype,false);
+        }
+      }
+    },
+    (LoadImmediate(n,t,acctype,memop,_signed,wback,postindex,offset,regsize,datasize))  => {
+      wb_unknown : (boolean) = false;
+      rt_unknown : (boolean) = false;
+      if n == 31 then {
+        iR = append(CheckSPAlignmentIFP,iR);
+        iR = append(rSPIFP,iR);
+        aR = append(rSPIFP,aR);
+      }
+      else {
+        iR = append(xFP(n),iR);
+        aR = append(xFP(n),aR);
+      };
+      if wback then {
+        if n == 31 then
+          let (i,o) = wSPFP in {iR = append(i,iR); oR = append(o,oR)}
+        else oR = append(xFP(n),oR);
+      };
+      match memop {
+        MemOp_STORE  => {
+          if rt_unknown then ()
+          else iR = append(xFP(t),iR);
+          iR = append(wMemIFP,iR);
+          ik = wmem_kind(acctype,false);
+        },
+        MemOp_LOAD  => {
+          oR = append(xFP(t),oR);
+          ik = rmem_kind(acctype,false);
+        },
+        MemOp_PREFETCH  => aR = [| |]
+      }
+    },
+    (LoadRegister(n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize,datasize))  => {
+      iR = append(xFP(m),iR);
+      aR = append(xFP(m),aR);
+      wb_unknown : (boolean) = false;
+      rt_unknown : (boolean) = false;
+      if n == 31 then {
+        iR = append(CheckSPAlignmentIFP,iR);
+        iR = append(rSPIFP,iR);
+        aR = append(rSPIFP,aR);
+      }
+      else {
+        iR = append(xFP(n),iR);
+        aR = append(xFP(n),aR);
+      };
+      if wback then {
+        if n == 31 then let (i,o) = wSPFP in {iR = append(i,iR); oR = append(o,oR)}
+        else oR = append(xFP(n),oR);
+      };
+      match memop {
+        MemOp_STORE  => {
+          if rt_unknown then ()
+          else iR = append(xFP(t),iR);
+          iR = append(wMemIFP,iR);
+          ik = wmem_kind(acctype,false);
+        },
+        MemOp_LOAD  => {
+          oR = append(xFP(t),oR);
+          ik = rmem_kind(acctype,false);
+        },
+        MemOp_PREFETCH  => aR = [| |]
+      }
+    },
+    (LoadStorePair(wback,postindex,n,t,t2,acctype,memop,_signed,datasize,offset))  => {
+      rt_unknown : (boolean) = false;
+      wb_unknown : (boolean) = false;
+      if n == 31 then {
+        iR = append(CheckSPAlignmentIFP,iR);
+        iR = append(rSPIFP,iR);
+        aR = append(rSPIFP,aR);
+      }
+      else {
+        iR = append(xFP(n),iR);
+        aR = append(xFP(n),aR);
+      };
+      if wback then {
+        if n == 31 then let (i,o) = wSPFP in {iR = append(i,iR); oR = append(o,oR)}
+        else oR = append(xFP(n),oR);
+      };
+      match memop {
+        MemOp_STORE  => {
+          if rt_unknown & t == n then ()
+          else iR = append(xFP(t),iR);
+          if rt_unknown & t2 == n then ()
+          else iR = append(xFP(t2),iR);
+          iR = append(wMemIFP,iR);
+          ik = wmem_kind(acctype,false);
+        },
+        MemOp_LOAD  => {
+          oR = append(xFP(t),oR);
+          oR = append(xFP(t2),oR);
+          ik = rmem_kind(acctype,false);
+        }
+      }
+    },
+    (AddSubImmediate(d,n,datasize,sub_op,setflags,imm))  => {
+      iR = append(if n == 31 then rSPIFP else xFP(n),iR);
+      if setflags then oR = append(NZCVfp,oR);
+      if d ==31 & ~(setflags) then
+        let (i,o) = wSPFP in
+        { iR = append(i,iR);
+          oR = append(o,oR) }
+      else oR = append(xFP(d),oR)
+    },
+    (BitfieldMove(d,n,datasize,inzero,extend,R,S,wmask,tmask))  => {
+      if inzero then () else iR= append(xFP(d),iR);
+      iR = append(xFP(n),iR);
+      oR = append(xFP(d),oR);
+    },
+    (ExtractRegister(d,n,m,datasize,lsb))  => {
+      iR = append(xFP(n),append(xFP(m),iR));
+      oR = append(xFP(d),oR);
+    },
+    (LogicalImmediate(d,n,datasize,setflags,op,imm))  => {
+      iR = append(xFP(n),iR);
+      if setflags then oR = append(NZCVfp,oR);
+      if d ==31 & ~(setflags) then let (i,o) = wSPFP in
+      { iR = append(i,iR); oR = append(o,oR) }
+      else oR = append(xFP(d),oR)
+    },
+    (MoveWide(d,datasize,imm,pos,opcode))  => {
+      if opcode == MoveWideOp_K then iR = append(xFP(d),iR);
+      oR = append(xFP(d),oR);
+    },
+    (Address(d,page,imm))  => {
+      iR = _PCfp :: iR;
+      oR = append(xFP(d),oR);
+    },
+    (AddSubExtendRegister(d,n,m,datasize,sub_op,setflags,extend_type,shift))  => {
+      iR = append(if n == 31 then rSPIFP else xFP(n),iR);
+      iR = append(xFP(m),iR);
+      if setflags then oR = append(NZCVfp,oR);
+      if d ==31 & ~(setflags) then let (i,o) = wSPFP in
+      { iR = append(i,iR); oR = append(o,oR) }
+      else oR = append(xFP(d),oR)
+    },
+    (AddSubShiftedRegister(d,n,m,datasize,sub_op,setflags,shift_type,shift_amount))  => {
+      iR = append(xFP(n),append(xFP(m),iR));
+      if setflags then oR = append(NZCVfp,oR);
+      oR = append(xFP(d),oR);
+    },
+    (AddSubCarry(d,n,m,datasize,sub_op,setflags))  => {
+      iR = append(xFP(n),append(xFP(m),iR));
+      iR = PSTATE_Cfp :: iR;
+      if setflags then oR = append(NZCVfp,oR);
+      oR = append(xFP(d),oR);
+    },
+    (ConditionalCompareImmediate(n,datasize,sub_op,condition,flags,imm))  => {
+      iR = append(xFP(n),iR);
+      iR = append(ConditionHoldsIFP(condition),iR);
+      oR = append(NZCVfp,oR);
+    },
+    (ConditionalCompareRegister(n,m,datasize,sub_op,condition,flags))  => {
+      iR = append(xFP(n),append(xFP(m),iR));
+      iR = append(ConditionHoldsIFP(condition),iR);
+      oR = append(NZCVfp,oR);      
+    },
+    (ConditionalSelect(d,n,m,datasize,condition,else_inv,else_inc))  => {
+      iR = append(xFP(n),append(xFP(m),iR));
+      iR = append(ConditionHoldsIFP(condition),iR);
+      oR = append(xFP(d),oR);
+    },
+    (Reverse(d,n,datasize,op))  => {
+      iR = append(xFP(n),iR);
+      oR = append(xFP(d),oR);
+    },
+    (CountLeading(d,n,datasize,opcode))  => {
+      iR = append(xFP(n),iR);
+      oR = append(xFP(d),oR);
+    },
+    (Division(d,n,m,datasize,_unsigned))  => {
+      iR = append(xFP(n),append(xFP(m),iR));
+      oR = append(xFP(d),oR);
+    },
+    (Shift(d,n,m,datasize,shift_type))  => {
+      iR = append(xFP(m),iR);
+      iR = append(xFP(n),iR);
+      oR = append(xFP(d),oR);
+    },
+    (CRC(d,n,m,size,crc32c))  => {
+      iR = append(xFP(n),append(xFP(m),iR));
+      oR = append(xFP(d),oR);
+    },
+    (MultiplyAddSub(d,n,m,a,destsize,datasize,sub_op))  => {
+      iR = append(xFP(n),iR);
+      iR = append(xFP(m),iR);
+      iR = append(xFP(a),iR);
+      oR = append(xFP(d),oR);
+    },
+    (MultiplyAddSubLong(d,n,m,a,destsize,datasize,sub_op,_unsigned))  => {
+      iR = append(xFP(n),iR);
+      iR = append(xFP(m),iR);
+      iR = append(xFP(a),iR);
+      oR = append(xFP(d),oR);      
+    },
+    (MultiplyHigh(d,n,m,a,destsize,datasize,_unsigned))  => {
+      iR = append(xFP(n),append(xFP(m),iR));
+      oR = append(xFP(d),oR);
+    },
+    (LogicalShiftedRegister(d,n,m,datasize,setflags,op,shift_type,shift_amount,invert))  => {
+      iR = append(xFP(n),append(xFP(m),iR));
+      if setflags then oR = append(NZCVfp,oR);
+      oR = append(xFP(d),oR);
+    }
+  };
+  (iR,oR,aR,Nias,Dia,ik)
+}