summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--aarch64_small/aarch64_regfp.sail454
-rw-r--r--aarch64_small/armV8.sail355
-rw-r--r--aarch64_small/armV8_common_lib.sail9
-rw-r--r--aarch64_small/prelude.sail1
4 files changed, 409 insertions, 410 deletions
diff --git a/aarch64_small/aarch64_regfp.sail b/aarch64_small/aarch64_regfp.sail
index 0bb79f8f..4d2051ba 100644
--- a/aarch64_small/aarch64_regfp.sail
+++ b/aarch64_small/aarch64_regfp.sail
@@ -32,7 +32,7 @@
/* SUCH DAMAGE. */
/*========================================================================*/
-val rmem_kind : (AccType, bool) -> instruction_kind
+val rmem_kind : (AccType, bool) -> instruction_kind effect {escape}
function rmem_kind (acctype, exclusive) =
if exclusive then
match acctype {
@@ -47,11 +47,12 @@ function rmem_kind (acctype, exclusive) =
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)
+ AccType_ORDERED => IK_mem_read(Read_acquire),
+ _ => exit()
}
-function instruction_kind wmem_kind (acctype : (AccType), exclusive : (bool)) =
+function wmem_kind (acctype : (AccType), exclusive : (bool)) -> instruction_kind =
if exclusive then {
match acctype {
AccType_ATOMIC => IK_mem_write(Write_exclusive),
@@ -92,17 +93,17 @@ 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 |]
+let NZCVfp : regfps = [| PSTATE_Nfp, PSTATE_Zfp, PSTATE_Cfp, PSTATE_Vfp |]
-function regfps xFP(n : (reg_index)) =
+function xFP(n : (reg_index)) -> regfps =
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) =
+function BranchToFP (iR : regfps, oR : regfps) -> (regfps,regfps) =
(if UsingAArch32() then iR else PSTATE_ELfp :: iR, _PCfp :: oR)
-function regfps ConditionHoldsIFP(_cond : (bits(4))) =
+function ConditionHoldsIFP(_cond : (bits(4))) -> regfps =
match _cond[3..1] {
0b000 => [| PSTATE_Zfp |],
0b001 => [| PSTATE_Cfp |],
@@ -115,41 +116,41 @@ function regfps ConditionHoldsIFP(_cond : (bits(4))) =
}
/* for iR if rSPFP, for oR if wSPFP */
-let rSPIFP =
+let rSPIFP : regfps =
/* TODO: actually this depends on runtime data: PSTATE_SP and PSTATE_EL */
[| PSTATE_SPfp, RFull("SP_EL0") |]
-let wSPFP =
+let wSPFP : (regfps, regfps) =
/* TODO: actually this depends on runtime data: PSTATE_SP and PSTATE_EL */
([| PSTATE_SPfp |],
[| RFull("SP_EL0") |])
-let CheckSPAlignmentIFP = PSTATE_ELfp :: rSPIFP
+let CheckSPAlignmentIFP : regfps = PSTATE_ELfp :: rSPIFP
-let BigEndianIFP =
+let BigEndianIFP : regfps =
if UsingAArch32() then [| RFull("PSTATE_E") |] else [| PSTATE_ELfp |]
-let wMem'IFP = BigEndianIFP
-let wMemIFP = wMem'IFP
+let wMem'IFP : regfps = BigEndianIFP
+let wMemIFP : regfps = 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;
+function initial_analysis (instr:ast) -> (regfps,regfps,regfps,niafps,diafp,instruction_kind) = {
+ iR : regfps = [| |];
+ oR : regfps = [| |];
+ aR : regfps = [| |];
+ Nias : niafps = [| NIAFP_successor() |];
+ Dia : diafp = DIAFP_none();
+ ik : instruction_kind = 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));
+ oR = TxNestingLevelfp :: appendL(oR,xFP(t));
ik = IK_trans(Transaction_start);
},
- (TMCommit) => {
+ (TMCommit()) => {
iR = TxNestingLevelfp :: iR;
oR = TxNestingLevelfp :: oR;
ik = IK_trans(Transaction_commit);
@@ -158,43 +159,43 @@ function initial_analysis (instr) -> (regfps,regfps,regfps,niafps,diafp,instruct
iR = TxNestingLevelfp :: iR;
ik = IK_trans(Transaction_abort);
},
- (TMTest) => {
+ (TMTest()) => {
iR = TxNestingLevelfp :: iR;
oR = RFull("NZCV") :: oR;
},
- (CompareAndBranch(t,datasize,iszero,offset)) => {
- iR = append(iR,xFP(t));
+ (CompareAndBranch((t,datasize,iszero,offset))) => {
+ iR = appendL(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;
+ Nias = [| NIAFP_successor(), NIAFP_concrete_address(nia') |];
+ ik = IK_branch();
},
(BranchConditional(offset,condition)) => {
- iR = append(iR,ConditionHoldsIFP(condition));
+ iR = appendL(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;
+ 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"),
+ (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 |]);
+ iR = appendL(iR, [| PSTATE_Dfp, PSTATE_Afp, PSTATE_Ifp, PSTATE_Ffp |]);
+ oR = appendL(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 |]);
+ iR = appendL(iR, [| PSTATE_Dfp, PSTATE_Afp, PSTATE_Ifp, PSTATE_Ffp |]);
+ oR = appendL(oR, [| PSTATE_Dfp, PSTATE_Afp, PSTATE_Ifp, PSTATE_Ffp |]);
}
},
(Hint(op)) =>
@@ -240,114 +241,117 @@ function initial_analysis (instr) -> (regfps,regfps,regfps,niafps,diafp,instruct
};
},
(System(t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result)) => {
- oR = append(oR,xFP(t));
+ oR = appendL(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));
+ oR = appendL(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
+ (3, 3, 13, 0, 2) => iR = RFull("TPIDR_EL0") :: iR,
/* TODO FIXME: higher EL TPIDRs */
+ _ => exit()
}
}
else {
- iR = append(iR,xFP(t));
+ iR = appendL(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
+ (3, 3, 13, 0, 2) => oR = RFull("TPIDR_EL0") :: oR,
/* TODO FIXME: higher EL TPIDRs */
+ _ => exit()
}
}
},
(ImplementationDefinedTestBeginEnd(isEnd)) => (),
- (ImplementationDefinedStopFetching) => (),
- (ImplementationDefinedThreadStart) => (),
- (TestBitAndBranch(t,datasize,bit_pos,bit_val,offset)) => {
- iR = append(xFP(t),iR);
+ (ImplementationDefinedStopFetching()) => (),
+ (ImplementationDefinedThreadStart()) => (),
+ (TestBitAndBranch((t,datasize,bit_pos,bit_val,offset))) => {
+ iR = appendL(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;
+ 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)};
+ then {iR = _PCfp :: iR; oR = appendL(xFP(30),oR)};
let (i,o) = BranchToFP(iR,oR) in {iR = i; oR = o};
Nias = [| NIAFP_concrete_address(rPC() + offset) |];
- ik = IK_branch
+ ik = IK_branch()
},
(BranchRegister(n,branch_type)) => {
- iR = append(iR,xFP(n));
+ iR = appendL(iR,xFP(n));
if branch_type == BranchType_CALL
- then {iR = _PCfp :: iR; oR = append(xFP(30),oR)};
+ then {iR = _PCfp :: iR; oR = appendL(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)) => {
+ Nias = if n == 31
+ then [| NIAFP_concrete_address(Zeros()) |]
+ 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);
+ oR = appendL(xFP(t),oR);
aR = _PCfp :: aR;
match memop {
MemOp_LOAD => ik = IK_mem_read(Read_plain),
- MemOp_PREFETCH => {ik = IK_simple; aR = [| |]}
+ MemOp_PREFETCH => {ik = IK_simple(); aR = [| |]},
+ _ => exit()
}
},
- (LoadStoreAcqExc(n,t,t2,s,acctype,excl,pair,memop,elsize,regsize,datasize)) => {
+ (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);
+ iR = appendL(CheckSPAlignmentIFP,iR);
+ iR = appendL(rSPIFP,iR);
+ aR = appendL(rSPIFP,aR);
}
else if rn_unknown then ()
else {
- iR = append(xFP(n),iR);
- aR = append(xFP(n),aR);
+ iR = appendL(xFP(n),iR);
+ aR = appendL(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);
+ else if pair then iR = appendL(xFP(t),appendL(xFP(t2),iR))
+ else iR = appendL(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);
+ iR = appendL(iR,wMemIFP);
+ oR = appendL(xFP(s),oR);
ik = wmem_kind(acctype,true);
}
else {
- iR = append(iR,wMemIFP);
+ iR = appendL(iR,wMemIFP);
ik = wmem_kind(acctype,false);
}
},
MemOp_LOAD => {
if pair then {
if rt_unknown then
- oR = append(xFP(t),oR)
+ oR = appendL(xFP(t),oR)
else if elsize == 32 then {
- iR = append(iR,BigEndianIFP);
- oR = append(xFP(t),append(xFP(t2),oR));
+ iR = appendL(iR,BigEndianIFP);
+ oR = appendL(xFP(t),appendL(xFP(t2),oR));
}
else {
- oR = append(xFP(t),append(xFP(t2),oR))
+ oR = appendL(xFP(t),appendL(xFP(t2),oR))
};
ik = rmem_kind(acctype,true);
}
else {
- oR = append(xFP(t),oR);
+ oR = appendL(xFP(t),oR);
ik = rmem_kind(acctype,excl);
}
@@ -355,244 +359,246 @@ function initial_analysis (instr) -> (regfps,regfps,regfps,niafps,diafp,instruct
MemOp_PREFETCH => aR = [| |]
}
},
- (LoadStorePairNonTemp(wback,postindex,n,t,t2,acctype,memop,scale,datasize,offset)) => {
+ (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);
+ iR = appendL(CheckSPAlignmentIFP,iR);
+ iR = appendL(rSPIFP,iR);
+ aR = appendL(rSPIFP,aR);
}
else {
- iR = append(xFP(n),iR);
- aR = append(xFP(n),aR);
+ iR = appendL(xFP(n),iR);
+ aR = appendL(xFP(n),aR);
};
if wback then {
if n == 31 then
let (i,o) = wSPFP in {
- iR = append(i,iR);
- oR = append(o,oR);
+ iR = appendL(i,iR);
+ oR = appendL(o,oR);
}
else
- oR = append(xFP(n),oR);
+ oR = appendL(xFP(n),oR);
};
match memop {
MemOp_STORE => {
if rt_unknown & t == n then ()
- else iR = append(xFP(t),iR);
+ else iR = appendL(xFP(t),iR);
if rt_unknown & t2 == n then ()
- else iR = append(xFP(t2),iR);
- iR = append(wMemIFP,iR);
+ else iR = appendL(xFP(t2),iR);
+ iR = appendL(wMemIFP,iR);
ik = wmem_kind(acctype,false);
},
MemOp_LOAD => {
- oR = append(xFP(t),append(xFP(t2),oR));
+ oR = appendL(xFP(t),appendL(xFP(t2),oR));
ik = rmem_kind(acctype,false);
- }
+ },
+ _ => exit()
}
},
- (LoadImmediate(n,t,acctype,memop,_signed,wback,postindex,offset,regsize,datasize)) => {
+ (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);
+ iR = appendL(CheckSPAlignmentIFP,iR);
+ iR = appendL(rSPIFP,iR);
+ aR = appendL(rSPIFP,aR);
}
else {
- iR = append(xFP(n),iR);
- aR = append(xFP(n),aR);
+ iR = appendL(xFP(n),iR);
+ aR = appendL(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);
+ let (i,o) = wSPFP in {iR = appendL(i,iR); oR = appendL(o,oR)}
+ else oR = appendL(xFP(n),oR);
};
match memop {
MemOp_STORE => {
if rt_unknown then ()
- else iR = append(xFP(t),iR);
- iR = append(wMemIFP,iR);
+ else iR = appendL(xFP(t),iR);
+ iR = appendL(wMemIFP,iR);
ik = wmem_kind(acctype,false);
},
MemOp_LOAD => {
- oR = append(xFP(t),oR);
+ oR = appendL(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);
+ (LoadRegister((n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize,datasize))) => {
+ iR = appendL(xFP(m),iR);
+ aR = appendL(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);
+ iR = appendL(CheckSPAlignmentIFP,iR);
+ iR = appendL(rSPIFP,iR);
+ aR = appendL(rSPIFP,aR);
}
else {
- iR = append(xFP(n),iR);
- aR = append(xFP(n),aR);
+ iR = appendL(xFP(n),iR);
+ aR = appendL(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);
+ if n == 31 then let (i,o) = wSPFP in {iR = appendL(i,iR); oR = appendL(o,oR)}
+ else oR = appendL(xFP(n),oR);
};
match memop {
MemOp_STORE => {
if rt_unknown then ()
- else iR = append(xFP(t),iR);
- iR = append(wMemIFP,iR);
+ else iR = appendL(xFP(t),iR);
+ iR = appendL(wMemIFP,iR);
ik = wmem_kind(acctype,false);
},
MemOp_LOAD => {
- oR = append(xFP(t),oR);
+ oR = appendL(xFP(t),oR);
ik = rmem_kind(acctype,false);
},
MemOp_PREFETCH => aR = [| |]
}
},
- (LoadStorePair(wback,postindex,n,t,t2,acctype,memop,_signed,datasize,offset)) => {
+ (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);
+ iR = appendL(CheckSPAlignmentIFP,iR);
+ iR = appendL(rSPIFP,iR);
+ aR = appendL(rSPIFP,aR);
}
else {
- iR = append(xFP(n),iR);
- aR = append(xFP(n),aR);
+ iR = appendL(xFP(n),iR);
+ aR = appendL(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);
+ if n == 31 then let (i,o) = wSPFP in {iR = appendL(i,iR); oR = appendL(o,oR)}
+ else oR = appendL(xFP(n),oR);
};
match memop {
MemOp_STORE => {
if rt_unknown & t == n then ()
- else iR = append(xFP(t),iR);
+ else iR = appendL(xFP(t),iR);
if rt_unknown & t2 == n then ()
- else iR = append(xFP(t2),iR);
- iR = append(wMemIFP,iR);
+ else iR = appendL(xFP(t2),iR);
+ iR = appendL(wMemIFP,iR);
ik = wmem_kind(acctype,false);
},
MemOp_LOAD => {
- oR = append(xFP(t),oR);
- oR = append(xFP(t2),oR);
+ oR = appendL(xFP(t),oR);
+ oR = appendL(xFP(t2),oR);
ik = rmem_kind(acctype,false);
- }
+ },
+ _ => exit()
}
},
- (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);
+ (AddSubImmediate((d,n,datasize,sub_op,setflags,imm))) => {
+ iR = appendL(if n == 31 then rSPIFP else xFP(n),iR);
+ if setflags then oR = appendL(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);
+ { iR = appendL(i,iR);
+ oR = appendL(o,oR) }
+ else oR = appendL(xFP(d),oR)
+ },
+ (BitfieldMove((d,n,datasize,inzero,extend,R,S,wmask,tmask))) => {
+ if inzero then () else iR= appendL(xFP(d),iR);
+ iR = appendL(xFP(n),iR);
+ oR = appendL(xFP(d),oR);
+ },
+ (ExtractRegister((d,n,m,datasize,lsb))) => {
+ iR = appendL(xFP(n),appendL(xFP(m),iR));
+ oR = appendL(xFP(d),oR);
+ },
+ (LogicalImmediate((d,n,datasize,setflags,op,imm))) => {
+ iR = appendL(xFP(n),iR);
+ if setflags then oR = appendL(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)
+ { iR = appendL(i,iR); oR = appendL(o,oR) }
+ else oR = appendL(xFP(d),oR)
},
- (MoveWide(d,datasize,imm,pos,opcode)) => {
- if opcode == MoveWideOp_K then iR = append(xFP(d),iR);
- oR = append(xFP(d),oR);
+ (MoveWide((d,datasize,imm,pos,opcode))) => {
+ if opcode == MoveWideOp_K then iR = appendL(xFP(d),iR);
+ oR = appendL(xFP(d),oR);
},
(Address(d,page,imm)) => {
iR = _PCfp :: iR;
- oR = append(xFP(d),oR);
+ oR = appendL(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);
+ (AddSubExtendRegister((d,n,m,datasize,sub_op,setflags,extend_type,shift))) => {
+ iR = appendL(if n == 31 then rSPIFP else xFP(n),iR);
+ iR = appendL(xFP(m),iR);
+ if setflags then oR = appendL(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)
+ { iR = appendL(i,iR); oR = appendL(o,oR) }
+ else oR = appendL(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);
+ (AddSubShiftedRegister((d,n,m,datasize,sub_op,setflags,shift_type,shift_amount))) => {
+ iR = appendL(xFP(n),appendL(xFP(m),iR));
+ if setflags then oR = appendL(NZCVfp,oR);
+ oR = appendL(xFP(d),oR);
},
- (AddSubCarry(d,n,m,datasize,sub_op,setflags)) => {
- iR = append(xFP(n),append(xFP(m),iR));
+ (AddSubCarry((d,n,m,datasize,sub_op,setflags))) => {
+ iR = appendL(xFP(n),appendL(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);
+ if setflags then oR = appendL(NZCVfp,oR);
+ oR = appendL(xFP(d),oR);
+ },
+ (ConditionalCompareImmediate((n,datasize,sub_op,condition,flags,imm))) => {
+ iR = appendL(xFP(n),iR);
+ iR = appendL(ConditionHoldsIFP(condition),iR);
+ oR = appendL(NZCVfp,oR);
+ },
+ (ConditionalCompareRegister((n,m,datasize,sub_op,condition,flags))) => {
+ iR = appendL(xFP(n),appendL(xFP(m),iR));
+ iR = appendL(ConditionHoldsIFP(condition),iR);
+ oR = appendL(NZCVfp,oR);
+ },
+ (ConditionalSelect((d,n,m,datasize,condition,else_inv,else_inc))) => {
+ iR = appendL(xFP(n),appendL(xFP(m),iR));
+ iR = appendL(ConditionHoldsIFP(condition),iR);
+ oR = appendL(xFP(d),oR);
+ },
+ (Reverse((d,n,datasize,op))) => {
+ iR = appendL(xFP(n),iR);
+ oR = appendL(xFP(d),oR);
+ },
+ (CountLeading((d,n,datasize,opcode))) => {
+ iR = appendL(xFP(n),iR);
+ oR = appendL(xFP(d),oR);
+ },
+ (Division((d,n,m,datasize,_unsigned))) => {
+ iR = appendL(xFP(n),appendL(xFP(m),iR));
+ oR = appendL(xFP(d),oR);
+ },
+ (Shift((d,n,m,datasize,shift_type))) => {
+ iR = appendL(xFP(m),iR);
+ iR = appendL(xFP(n),iR);
+ oR = appendL(xFP(d),oR);
+ },
+ (CRC((d,n,m,size,crc32c))) => {
+ iR = appendL(xFP(n),appendL(xFP(m),iR));
+ oR = appendL(xFP(d),oR);
+ },
+ (MultiplyAddSub((d,n,m,a,destsize,datasize,sub_op))) => {
+ iR = appendL(xFP(n),iR);
+ iR = appendL(xFP(m),iR);
+ iR = appendL(xFP(a),iR);
+ oR = appendL(xFP(d),oR);
+ },
+ (MultiplyAddSubLong((d,n,m,a,destsize,datasize,sub_op,_unsigned))) => {
+ iR = appendL(xFP(n),iR);
+ iR = appendL(xFP(m),iR);
+ iR = appendL(xFP(a),iR);
+ oR = appendL(xFP(d),oR);
+ },
+ (MultiplyHigh((d,n,m,a,destsize,datasize,_unsigned))) => {
+ iR = appendL(xFP(n),appendL(xFP(m),iR));
+ oR = appendL(xFP(d),oR);
+ },
+ (LogicalShiftedRegister((d,n,m,datasize,setflags,op,shift_type,shift_amount,invert))) => {
+ iR = appendL(xFP(n),appendL(xFP(m),iR));
+ if setflags then oR = appendL(NZCVfp,oR);
+ oR = appendL(xFP(d),oR);
}
};
(iR,oR,aR,Nias,Dia,ik)
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail
index e4ac4c7f..c7d2d480 100644
--- a/aarch64_small/armV8.sail
+++ b/aarch64_small/armV8.sail
@@ -77,7 +77,7 @@ union ast = {
BitfieldMove : {'R 'r 's, RegisterSize('R) & 0 <= 'r < 'R & 0 <= 's < 'R. (reg_index,reg_index,atom('R),boolean,boolean,atom('r),atom('s),bits('R),bits('R))},
ExtractRegister : {'R 'lsb, RegisterSize('R) & 0 <= 'lsb <= 'R. (reg_index,reg_index,reg_index,atom('R),atom('lsb))},
LogicalImmediate : {'R, RegisterSize('R). (reg_index,reg_index,atom('R),boolean,LogicalOp,bits('R))},
- MoveWide : {'R, RegisterSize('R). (reg_index,atom('R),bits(16),uinteger,MoveWideOp)},
+ MoveWide : {'R 'pos, RegisterSize('R) & 0 <= 'pos < div('R, 2). (reg_index,atom('R),bits(16),atom('pos),MoveWideOp)},
Address : (reg_index,boolean,bits(64)),
AddSubExtendRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,boolean,ExtendType,range(0,7))},
AddSubShiftedRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,boolean,ShiftType,range(0,63))},
@@ -90,10 +90,10 @@ union ast = {
Division : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean)},
Shift : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),ShiftType)},
CRC : {'D, DataSize('D). (reg_index,reg_index,reg_index,atom('D),boolean)},
- MultiplyAddSub : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,atom('R),atom('D),boolean)},
+ MultiplyAddSub : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,atom('R),atom('R),boolean)},
MultiplyAddSubLong : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,atom('R),atom('D),boolean,boolean)},
- MultiplyHigh : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,atom('R),atom('D),boolean)},
- LogicalShiftedRegister : {'D 'R, DataSize('D) & RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,LogicalOp,ShiftType,range(0,63),boolean)},
+ MultiplyHigh : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,reg_index,atom('R),atom('R),boolean)},
+ LogicalShiftedRegister : {'R, RegisterSize('R). (reg_index,reg_index,reg_index,atom('R),boolean,LogicalOp,ShiftType,range(0,63),boolean)},
}
val execute : ast -> unit effect {rreg,wreg,rmem,barr,eamem,wmv,exmem,escape}
@@ -564,8 +564,8 @@ function decodeTestBranchImmediate ([b5]@0b011011@[op]@(b40 : bits(5))@(imm14 :
Some(TestBitAndBranch((t,datasize,bit_pos,bit_val,offset)));
}
-function clause execute ( TestBitAndBranch((t,(datasize as atom('R)),bit_pos,bit_val,offset)) ) = {
- operand : bits('R) = rX(datasize,t);
+function clause execute ( TestBitAndBranch((t:reg_index,datasize as atom('R),bit_pos,bit_val,offset)) ) = {
+ let operand : bits('R) = rX(t);
if operand[bit_pos] == bit_val then
BranchTo(rPC() + offset, BranchType_JMP);
@@ -1763,7 +1763,7 @@ function clause execute (LogicalImmediate((d,n,datasize as atom('R),setflags,op,
val decodeMoveWideImmediate : bits(32) -> option(ast) effect {escape}
function decodeMoveWideImmediate ([sf]@(opc:bits(2))@0b100101@(hw : bits(2))@(imm16 : bits(16))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
- datasize : {|32,64|} /* : atom('R) */ = if sf == b1 then 64 else 32;
+ let datasize : {|32,64|} /* : atom('R) */ = if sf == b1 then 64 else 32;
imm : (bits(16)) = imm16;
pos : (uinteger) = 0; /* ARM: uninitialized */
opcode : (MoveWideOp) = MoveWideOp_N; /* ARM: uninitialized */
@@ -1776,7 +1776,8 @@ function decodeMoveWideImmediate ([sf]@(opc:bits(2))@0b100101@(hw : bits(2))@(im
};
if sf == b0 & hw[1] == b1 then UnallocatedEncoding();
- pos = UInt(hw@0b0000);
+ let pos = UInt(hw@0b0000);
+ assert(pos < (datasize / 2));
Some(MoveWide(d,datasize,imm,pos,opcode));
}
@@ -1924,7 +1925,7 @@ function clause execute( AddSubCarry((d,n,m,(datasize as atom('R)),sub_op,setfla
if sub_op then
operand2 = NOT(operand2);
- let (result,nzcv) = AddWithCarry (operand1, operand2, PSTATE_C()) in {
+ let (result,nzcv) = AddWithCarry (operand1, operand2, PSTATE_C()[0]) in {
if setflags then
wPSTATE_NZCV() = nzcv;
@@ -1934,29 +1935,28 @@ function clause execute( AddSubCarry((d,n,m,(datasize as atom('R)),sub_op,setfla
/* CCMN (immediate) */
/* CCMP (immediate) */
-val decodeConditionalCompareImmediate : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
-function decodeConditionalCompareImmediate ([sf]@[op]@[1]@0b11010010@(imm5 : bits(5))@ _cond@[1]@[0]@Rn@[0]@nzcv) = {
+val decodeConditionalCompareImmediate : bits(32) -> option(ast) effect pure
+function decodeConditionalCompareImmediate ([sf]@[op]@[b1]@0b11010010@(imm5 : bits(5))@(_cond:bits(4))@[b1]@[b0]@(Rn:bits(5))@[b0]@(nzcv:bits(4))) = {
n : (reg_index) = UInt_reg(Rn);
- datasize : atom('R) = if sf == 1 then 64 else 32;
- sub_op : boolean = (op ==1);
+ let datasize : {| 32, 64 |} /* : atom('R) */ = if sf == b1 then 64 else 32;
+ sub_op : boolean = (op == b1);
condition : bits(4) = _cond;
flags : bits(4) = nzcv;
- imm : bits('R) = ZeroExtend(imm5);
+ imm /* : bits('R) */ = ZeroExtend(datasize,imm5);
- Some(ConditionalCompareImmediate(n,datasize,sub_op,condition,flags,imm));
+ Some(ConditionalCompareImmediate((n,datasize,sub_op,condition,flags,imm)));
}
-function clause execute (ConditionalCompareImmediate(n,datasize,sub_op,condition,flags,imm)) = {
+function clause execute(ConditionalCompareImmediate((n,datasize as atom('R),sub_op,condition,flags,imm))) = {
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = imm;
- carry_in : (bit) = 0;
+ carry_in : (bit) = b0;
flags' : (bits(4)) = flags;
if ConditionHolds(condition) then {
if sub_op then {
operand2 = NOT(operand2);
- carry_in = 1;
+ carry_in = b1;
};
let (_,nzcv) = AddWithCarry(operand1, operand2, carry_in) in {flags' = nzcv};
};
@@ -1965,29 +1965,28 @@ function clause execute (ConditionalCompareImmediate(n,datasize,sub_op,condition
/* CCMN (register) */
/* CCMP (register) */
-val decodeConditionalCompareRegister : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
-function decodeConditionalCompareRegister ([sf]@[op]@[1]@0b11010010@Rm@ _cond@[0]@[0]@Rn@[0]@nzcv) = {
+val decodeConditionalCompareRegister : bits(32) -> option(ast) effect pure
+function decodeConditionalCompareRegister ([sf]@[op]@[b1]@0b11010010@(Rm:bits(5))@ (_cond:bits(4))@[b0]@[b0]@(Rn:bits(5))@[b0]@(nzcv:bits(4))) = {
n : reg_index = UInt_reg(Rn);
m : reg_index = UInt_reg(Rm);
- datasize : atom('R) = if sf == 1 then 64 else 32;
- sub_op : boolean = (op ==1);
+ datasize : {|32,64|} /* : atom('R) */ = if sf == b1 then 64 else 32;
+ sub_op : boolean = (op == b1);
condition : bits(4) = _cond;
flags : bits(4) = nzcv;
Some(ConditionalCompareRegister(n,m,datasize,sub_op,condition,flags));
}
-function clause execute (ConditionalCompareRegister(n,m,datasize,sub_op,condition,flags)) = {
+function clause execute (ConditionalCompareRegister((n,m,datasize as atom('R),sub_op,condition,flags))) = {
operand1 : bits('R) = rX(n);
operand2 : bits('R) = rX(m);
- carry_in : bit = 0;
+ carry_in : bit = b0;
flags' : bits(4) = flags;
if ConditionHolds(condition) then {
if sub_op then {
operand2 = NOT(operand2);
- carry_in = 1;
+ carry_in = b1;
};
let (_,nzcv) = AddWithCarry (operand1, operand2, carry_in) in {flags' = nzcv};
};
@@ -1998,22 +1997,21 @@ function clause execute (ConditionalCompareRegister(n,m,datasize,sub_op,conditio
/* CSINC op=0,o2=1 */
/* CSINV op=1,o2=0 */
/* CSNEG op=1,o2=1 */
-val decodeConditionalSelect : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
-function decodeConditionalSelect ([sf]@[op]@[0]@0b11010100@Rm@ _cond@[0]@[o2]@Rn@Rd) = {
+val decodeConditionalSelect : bits(32) -> option(ast) effect pure
+function decodeConditionalSelect ([sf]@[op]@[b0]@0b11010100@(Rm:bits(5))@(_cond:bits(4))@[b0]@[o2]@(Rn:bits(5))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- datasize : (atom('R)) = if sf == 1 then 64 else 32;
+ datasize : {|32,64|}/* (atom('R)) */ = if sf == b1 then 64 else 32;
condition : (bits(4)) = _cond;
- else_inv : (boolean) = (op == 1);
- else_inc : (boolean) = (o2 == 1);
+ else_inv : (boolean) = (op == b1);
+ else_inc : (boolean) = (o2 == b1);
Some(ConditionalSelect(d,n,m,datasize,condition,else_inv,else_inc));
}
-function clause execute ( ConditionalSelect(d,n,m,datasize,condition,else_inv,else_inc) ) = {
- result : (bits('R)) = 0; /* ARM: uninitialized */
+function clause execute ( ConditionalSelect((d,n,m,datasize as atom('R),condition,else_inv,else_inc)) ) = {
+ result : (bits('R)) = Zeros(); /* ARM: uninitialized */
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = rX(m);
@@ -2028,21 +2026,20 @@ function clause execute ( ConditionalSelect(d,n,m,datasize,condition,else_inv,el
wX(d) = result;
}
-val decodeData1Source : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
+val decodeData1Source : bits(32) -> option(ast) effect pure
scattered function decodeData1Source
/* RBIT */
/* REV */
/* REV16 */
/* REV32 */
-function clause decodeData1Source ([sf]@[1]@[0]@0b11010110@0b00000@0b0000@opc@Rn@Rd) = {
+function clause decodeData1Source ([sf]@[b1]@[b0]@0b11010110@0b00000@0b0000@(opc:bits(2))@(Rn:bits(5))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
- datasize : (atom('R)) = if sf == 1 then 64 else 32;
+ datasize : {|32,64|}/* (atom('R)) */ = if sf == b1 then 64 else 32;
- op : (RevOp) = 0; /* ARM: uninitialized */
+ op : (RevOp) = RevOp_RBIT; /* ARM: uninitialized */
match opc {
0b00 =>
op = RevOp_RBIT,
@@ -2051,7 +2048,7 @@ function clause decodeData1Source ([sf]@[1]@[0]@0b11010110@0b00000@0b0000@opc@Rn
0b10 =>
op = RevOp_REV32,
0b11 => {
- if sf == 0 then UnallocatedEncoding();
+ if sf == b0 then UnallocatedEncoding();
op = RevOp_REV64;
}
};
@@ -2059,27 +2056,31 @@ function clause decodeData1Source ([sf]@[1]@[0]@0b11010110@0b00000@0b0000@opc@Rn
Some(Reverse(d,n,datasize,op));
}
-function clause execute ( Reverse(d,n,datasize,op) ) = {
- result : (bits('R)) = 0; /* ARM uninitialized */
- V : (bits(6)) = 0; /* ARM uninitialized */
+function clause execute ( Reverse((d,n,datasize as atom('R),op)) ) = {
+ result : (bits('R)) = Zeros(); /* ARM uninitialized */
+ /* let V : (bits(6)) = Zeros(); /\* ARM uninitialized *\/ */
- match op {
- RevOp_REV16 => V = 0b001000,
- RevOp_REV32 => V = 0b011000,
- RevOp_REV64 => V = 0b111000,
- RevOp_RBIT => V = if datasize == 64 then 0b111111 else 0b011111
+ let V : (bits(6)) = match op {
+ RevOp_REV16 => /* V = */ 0b001000,
+ RevOp_REV32 => /* V = */ 0b011000,
+ RevOp_REV64 => /* V = */ 0b111000,
+ RevOp_RBIT => /* V = */ if datasize == 64 then 0b111111 else 0b011111
};
- result = rX(n);
+ result : (bits('R)) = rX(n);
foreach (vbit from 0 to 5) {
/* Swap pairs of 2^vbit bits in result */
- if V[vbit] == 1 then {
+ if V[vbit] == b1 then {
tmp : (bits('R)) = result;
- vsize : (uinteger) = lsl(1, vbit);
+ let vsize /* : (uinteger) */ = lsl(1, vbit);
+ assert (vsize > 0); /* FIXME: CP adding assertion to make typecheck */
foreach (base from 0 to (datasize - 1) by (2 * vsize)) { /* ARM: while base < datasize do */
- result[((base+vsize) - 1)..base] = tmp[(base+(2*vsize) - 1)..(base+vsize)];
- result[(base+(2*vsize) - 1)..(base+vsize)] = tmp[(base+vsize - 1)..base];
+ assert (base+vsize*2 - 1 < datasize); /* FIXME: CP adding assertion to make typecheck */
+ let a = tmp[(base+(2*vsize) - 1)..(base+vsize)];
+ result[((base+vsize) - 1)..base] = a;
+ let b = tmp[(base+vsize - 1)..base];
+ result[(base+(2*vsize) - 1)..(base+vsize)] = b;
/* ARM: base = base + (2 * vsize); */
};
};
@@ -2089,17 +2090,17 @@ function clause execute ( Reverse(d,n,datasize,op) ) = {
/* CLS */
/* CLZ */
-function clause decodeData1Source ([sf]@[1]@[0]@0b11010110@0b00000@0b00010@[op]@Rn@Rd) = {
+function clause decodeData1Source ([sf]@[b1]@[b0]@0b11010110@0b00000@0b00010@[op]@(Rn:bits(5))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
- datasize : (atom('R)) = if sf == 1 then 64 else 32;
- opcode : (CountOp) = if op == 0 then CountOp_CLZ else CountOp_CLS;
+ datasize : {| 32,64 |} /* (atom('R)) */ = if sf == b1 then 64 else 32;
+ opcode : (CountOp) = if op == b0 then CountOp_CLZ else CountOp_CLS;
Some(CountLeading(d,n,datasize,opcode));
}
-function clause execute (CountLeading(d,n,datasize,opcode)) = {
- result : (uinteger) = 0; /* ARM: uninitialized */
+function clause execute (CountLeading((d,n,datasize as atom('R),opcode))) = {
+ result : integer = 0; /* ARM: uninitialized */
operand1 : (bits('R)) = rX(n);
if opcode == CountOp_CLZ then
@@ -2107,28 +2108,27 @@ function clause execute (CountLeading(d,n,datasize,opcode)) = {
else
result = CountLeadingSignBits(operand1);
- wX(d) = result : bits('R);
+ wX(d) = to_bits(result) : bits('R);
}
end decodeData1Source
-val decodeData2Source : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
+val decodeData2Source : bits(32) -> option(ast) effect pure
scattered function decodeData2Source
/* SDIV o1=1 */
/* UDIV o1=0 */
-function clause decodeData2Source ([sf]@[0]@[0]@0b11010110@Rm@0b00001@[o1]@Rn@Rd) = {
+function clause decodeData2Source ([sf]@[b0]@[b0]@0b11010110@(Rm:bits(5))@0b00001@[o1]@(Rn:bits(5))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- datasize : (atom('R)) = if sf == 1 then 64 else 32;
- _unsigned : (boolean) = (o1 == 0);
+ datasize : {| 32, 64 |} /* (atom('R)) */ = if sf == b1 then 64 else 32;
+ _unsigned : (boolean) = (o1 == b0);
Some(Division(d,n,m,datasize,_unsigned));
}
-function clause execute ( Division(d,n,m,datasize,_unsigned) ) = {
+function clause execute ( Division((d,n,m,datasize as atom('R),_unsigned)) ) = {
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = rX(m);
result : (integer) = 0; /* ARM: uninitialized */
@@ -2138,25 +2138,25 @@ function clause execute ( Division(d,n,m,datasize,_unsigned) ) = {
else
result = /* ARM: RoundTowardsZero*/ quot (_Int(operand1, _unsigned), _Int(operand2, _unsigned)); /* FIXME: does quot round towards zero? */
- wX(d) = result : (bits('R)) ; /* ARM: result[(datasize-1)..0] */
+ wX(d) = to_bits(result) : (bits('R)) ; /* ARM: result[(datasize-1)..0] */
}
/* ASRV */
/* LSLV */
/* LSRV */
/* RORV */
-function clause decodeData2Source ([sf]@[0]@[0]@0b11010110@Rm@0b0010@op2@Rn@Rd) = {
+function clause decodeData2Source ([sf]@[b0]@[b0]@0b11010110@(Rm:bits(5))@0b0010@(op2:bits(2))@(Rn:bits(5))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- datasize : (atom('R)) = if sf == 1 then 64 else 32;
+ datasize : {| 32, 64 |} /* (atom('R)) */ = if sf == b1 then 64 else 32;
shift_type : (ShiftType) = DecodeShift(op2);
Some(Shift(d,n,m,datasize,shift_type));
}
-function clause execute (Shift(d,n,m,datasize,shift_type)) = {
- result : (bits('R)) = 0; /* ARM: uninitialized */
+function clause execute (Shift((d,n,m,datasize as atom('R),shift_type))) = {
+ result : (bits('R)) = Zeros(); /* ARM: uninitialized */
operand2 : (bits('R)) = rX(m);
result = ShiftReg(n, shift_type, mod (UInt(operand2), datasize));
@@ -2165,19 +2165,20 @@ function clause execute (Shift(d,n,m,datasize,shift_type)) = {
/* CRC32B/CRC32H/CRC32W/CRC32X C=0 */
/* CRC32CB/CRC32CH/CRC32CW/CRC32CX C=1 */
-function clause decodeData2Source ([sf]@[0]@[0]@0b11010110@Rm@0b010@[C]@sz@Rn@Rd) = {
+function clause decodeData2Source ([sf]@[b0]@[b0]@0b11010110@(Rm:bits(5))@0b010@[C]@(sz:bits(2))@(Rn:bits(5))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- if sf == 1 & sz != 0b11 then UnallocatedEncoding();
- if sf == 0 & sz == 0b11 then UnallocatedEncoding();
- size : (atom('D)) = lsl(8, UInt(sz)); /* 2-bit size field -> 8, 16, 32, 64 */
- crc32c : (boolean) = (C == 1);
+ if sf == b1 & sz != 0b11 then UnallocatedEncoding();
+ if sf == b0 & sz == 0b11 then UnallocatedEncoding();
+ let size /* : {| 8,16,32,64 |} */ /* (atom('D)) */ = lsl(8, UInt(sz)); /* 2-bit size field -> 8, 16, 32, 64 */
+ assert (size == 8 | size == 16 | size == 32 | size == 64); /*FIXME: CP adding assertion to make typecheck*/
+ crc32c : (boolean) = (C == b1);
Some(CRC(d,n,m,size,crc32c));
}
-function clause execute ( CRC(d,n,m,size,crc32c) ) = {
+function clause execute ( CRC((d,n,m,(size as atom('D)),crc32c)) ) = {
if ~(HaveCRCExt()) then
UnallocatedEncoding();
@@ -2194,25 +2195,24 @@ function clause execute ( CRC(d,n,m,size,crc32c) ) = {
end decodeData2Source
-val decodeData3Source : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
+val decodeData3Source : bits(32) -> option(ast) effect pure
scattered function decodeData3Source
/* MADD o0=0 */
/* MSUB o0=1 */
-function clause decodeData3Source ([sf]@0b00@0b11011@0b000@Rm@[o0]@Ra@Rn@Rd) = {
- d : (reg_index) = UInt_reg(Rd);
- n : (reg_index) = UInt_reg(Rn);
- m : (reg_index) = UInt_reg(Rm);
- a : (reg_index) = UInt_reg(Ra);
- destsize : (atom('R)) = if sf == 1 then 64 else 32;
- datasize : (atom('D)) = destsize;
- sub_op : (boolean) = (o0 == 1);
+function clause decodeData3Source ([sf]@0b00@0b11011@0b000@(Rm:bits(5))@[o0]@(Ra:bits(5))@(Rn:bits(5))@(Rd:bits(5))) = {
+ let d : (reg_index) = UInt_reg(Rd);
+ let n : (reg_index) = UInt_reg(Rn);
+ let m : (reg_index) = UInt_reg(Rm);
+ let a : (reg_index) = UInt_reg(Ra);
+ let destsize /* (atom('R)) */ = if sf == b1 then 64 else 32;
+ let datasize /* (atom('D)) */ = destsize;
+ let sub_op : (boolean) = (o0 == b1);
- Some(MultiplyAddSub(d,n,m,a,destsize,datasize,sub_op));
+ Some(MultiplyAddSub((d,n,m,a,destsize,datasize,sub_op)));
}
-function clause execute ( MultiplyAddSub(d,n,m,a,destsize,datasize,sub_op) ) = {
+function clause execute ( MultiplyAddSub((d,n,m,a,destsize as atom('D),datasize as atom('R),sub_op)) ) = {
operand1 : (bits('D)) = rX(n);
operand2 : (bits('D)) = rX(m);
operand3 : (bits('R)) = rX(a);
@@ -2224,27 +2224,27 @@ function clause execute ( MultiplyAddSub(d,n,m,a,destsize,datasize,sub_op) ) = {
else
result = UInt(operand3) + (UInt(operand1) * UInt(operand2));
- wX(d) = result : (bits('R));
+ wX(d) = to_bits(result) : (bits('R));
}
/* SMADDL */
/* SMSUBL */
/* UMADDL */
/* UMSUBL */
-function clause decodeData3Source ([1]@0b00@0b11011@[U]@0b01@Rm@[o0]@Ra@Rn@Rd) = {
+function clause decodeData3Source ([b1]@0b00@0b11011@[U]@0b01@(Rm:bits(5))@[o0]@(Ra:bits(5))@(Rn:bits(5))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
a : (reg_index) = UInt_reg(Ra);
- destsize : (atom('R)) = 64;
- datasize : (atom('D)) = 32;
- sub_op : (boolean) = (o0 == 1);
- _unsigned : (boolean) = (U == 1);
+ destsize /* : (atom('R)) */ = 64;
+ datasize /* : (atom('D)) */ = 32;
+ sub_op : (boolean) = (o0 == b1);
+ _unsigned : (boolean) = (U == b1);
Some(MultiplyAddSubLong(d,n,m,a,destsize,datasize,sub_op,_unsigned));
}
-function clause execute ( MultiplyAddSubLong(d,n,m,a,destsize,datasize,sub_op,_unsigned) ) = {
+function clause execute ( MultiplyAddSubLong((d,n,m,a,destsize as atom('R),datasize as atom('D),sub_op,_unsigned)) ) = {
operand1 : (bits('D)) = rX(n);
operand2 : (bits('D)) = rX(m);
operand3 : (bits('R)) = rX(a);
@@ -2256,32 +2256,32 @@ function clause execute ( MultiplyAddSubLong(d,n,m,a,destsize,datasize,sub_op,_u
else
result = _Int(operand3, _unsigned) + (_Int(operand1, _unsigned) * _Int(operand2, _unsigned));
- wX(d) = result : (bits(64));
+ wX(d) = to_bits(result) : (bits(64));
}
/* SMULH */
/* UMULH */
-function clause decodeData3Source ([1]@0b00@0b11011@[U]@0b10@Rm@[0]@Ra@Rn@Rd) = {
+function clause decodeData3Source ([b1]@0b00@0b11011@[U]@0b10@(Rm:bits(5))@[b0]@(Ra:bits(5))@(Rn:bits(5))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
a : (reg_index) = UInt_reg(Ra); /* ignored by UMULH/SMULH */
- destsize : (atom('R)) = 64;
- datasize : (atom('D)) = destsize;
- _unsigned : (boolean) = (U == 1);
+ destsize /* : (atom('R)) */ = 64;
+ datasize /* : (atom('D)) */ = destsize;
+ _unsigned : (boolean) = (U == b1);
Some(MultiplyHigh(d,n,m,a,destsize,datasize,_unsigned));
}
-function clause execute ( MultiplyHigh(d,n,m,a,destsize,datasize,_unsigned) ) = {
+function clause execute ( MultiplyHigh((d,n,m,a,destsize as atom('R),datasize,_unsigned)) ) = {
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = rX(m);
- result : (integer) = 0; /* ARM: uninitialized */
+ /* result : (integer) = 0; /\* ARM: uninitialized *\/ */
result = _Int(operand1, _unsigned) * _Int(operand2, _unsigned);
- wX(d) = (result : bits(128))[127..64];
+ wX(d) = (to_bits(result) : bits(128))[127..64];
}
end decodeData3Source
@@ -2292,13 +2292,12 @@ end decodeData3Source
/* ORN (shifted register) */
/* ORR (shifted register) */
/* BIC/BICS (shifted register) */
-val decodeLogicalShiftedRegister : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
-function decodeLogicalShiftedRegister ([sf]@opc@0b01010@shift@[N]@Rm@(imm6 : bits(6))@Rn@Rd) = {
+val decodeLogicalShiftedRegister : bits(32) -> option(ast) effect {escape}
+function decodeLogicalShiftedRegister ([sf]@(opc:bits(2))@0b01010@(shift:bits(2))@[N]@(Rm:bits(5))@(imm6 : bits(6))@(Rn:bits(5))@(Rd:bits(5))) = {
d : (reg_index) = UInt_reg(Rd);
n : (reg_index) = UInt_reg(Rn);
m : (reg_index) = UInt_reg(Rm);
- datasize : (atom('R)) = if sf == 1 then 64 else 32;
+ datasize : {| 32,64 |} /* : (atom('R)) */ = if sf == b1 then 64 else 32;
setflags : (boolean) = false; /* ARM: uninitialized */
op : (LogicalOp) = LogicalOp_AND; /* ARM: uninitialized */
match opc {
@@ -2308,23 +2307,23 @@ function decodeLogicalShiftedRegister ([sf]@opc@0b01010@shift@[N]@Rm@(imm6 : bit
0b11 => {op = LogicalOp_AND; setflags = true}
};
- if sf == 0 & imm6[5] == 1 then ReservedValue();
+ if sf == b0 & imm6[5] == b1 then ReservedValue();
shift_type : (ShiftType) = DecodeShift(shift);
shift_amount : range(0,63) = UInt(imm6);
- invert : (boolean) = (N == 1);
+ invert : (boolean) = (N == b1);
- Some(LogicalShiftedRegister(d,n,m,datasize,setflags,op,shift_type,shift_amount,invert))
+ Some(LogicalShiftedRegister((d,n,m,datasize,setflags,op,shift_type,shift_amount,invert)))
}
-function clause execute (LogicalShiftedRegister(d,n,m,datasize,setflags,op,shift_type,shift_amount,invert)) = {
+function clause execute (LogicalShiftedRegister((d,n,m,datasize as atom('R),setflags,op,shift_type,shift_amount,invert))) = {
operand1 : (bits('R)) = rX(n);
operand2 : (bits('R)) = ShiftReg(m, shift_type, shift_amount);
if invert then operand2 = NOT(operand2);
- result : (bits('R)) = 0; /* ARM: uninitialized */
+ result : (bits('R)) = Zeros(); /* ARM: uninitialized */
match op {
LogicalOp_AND => result = (operand1 & operand2),
LogicalOp_ORR => result = (operand1 | operand2),
@@ -2337,116 +2336,108 @@ function clause execute (LogicalShiftedRegister(d,n,m,datasize,setflags,op,shift
wX(d) = result;
}
-val decodeDataSIMDFPoint1 : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect {escape}
+val decodeDataSIMDFPoint1 : bits(32) -> option(ast) effect {escape}
function decodeDataSIMDFPoint1 (machineCode) = {
not_implemented("decodeDataSIMDFPoint1");
- Some(Unallocated);
+ Some(Unallocated());
}
-val decodeDataSIMDFPoint2 : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect {escape}
+val decodeDataSIMDFPoint2 : bits(32) -> option(ast) effect {escape}
function decodeDataSIMDFPoint2 ( machineCode) = {
not_implemented("decodeDataSIMDFPoint2");
- Some(Unallocated);
+ Some(Unallocated());
}
-val decodeDataRegister : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
+val decodeDataRegister : bits(32) -> option(ast) effect {escape}
function decodeDataRegister (machineCode) = {
match machineCode {
- ([_]@[_]@[_]@[0]@ [1]@[0]@[1]@[0]@ [_]@[_]@[_]@ (_ : bits(9)) @[_]@(_ : bits(11))) => decodeLogicalShiftedRegister(machineCode),
- ([_]@[_]@[_]@[0]@ [1]@[0]@[1]@[1]@ [_]@[_]@[0]@ (_ : bits(9)) @[_]@(_ : bits(11))) => decodeAddSubtractShiftedRegister(machineCode),
- ([_]@[_]@[_]@[0]@ [1]@[0]@[1]@[1]@ [_]@[_]@[1]@ (_ : bits(9)) @[_]@(_ : bits(11))) => decodeAddSubtractExtendedRegister(machineCode),
- ([_]@[_]@[_]@[1]@ [1]@[0]@[1]@[0]@ [0]@[0]@[0]@ (_ : bits(9)) @[_]@(_ : bits(11))) => decodeAddSubtractWithCarry(machineCode),
- ([_]@[_]@[_]@[1]@ [1]@[0]@[1]@[0]@ [0]@[1]@[0]@ (_ : bits(9)) @[0]@(_ : bits(11))) => decodeConditionalCompareRegister(machineCode),
- ([_]@[_]@[_]@[1]@ [1]@[0]@[1]@[0]@ [0]@[1]@[0]@ (_ : bits(9)) @[1]@(_ : bits(11))) => decodeConditionalCompareImmediate(machineCode),
- ([_]@[_]@[_]@[1]@ [1]@[0]@[1]@[0]@ [1]@[0]@[0]@ (_ : bits(9)) @[_]@(_ : bits(11))) => decodeConditionalSelect(machineCode),
- ([_]@[_]@[_]@[1]@ [1]@[0]@[1]@[1]@ [_]@[_]@[_]@ (_ : bits(9)) @[_]@(_ : bits(11))) => decodeData3Source(machineCode),
- ([_]@[0]@[_]@[1]@ [1]@[0]@[1]@[0]@ [1]@[1]@[0]@ (_ : bits(9)) @[_]@(_ : bits(11))) => decodeData2Source(machineCode),
- ([_]@[1]@[_]@[1]@ [1]@[0]@[1]@[0]@ [1]@[1]@[0]@ (_ : bits(9)) @[_]@(_ : bits(11))) => decodeData1Source(machineCode)
+ ([_]@[_ ]@[_]@[b0]@ [b1]@[b0]@[b1]@[b0]@ [_ ]@[_ ]@[_ ]@ (_ : bits(9)) @[_ ]@(_ : bits(11))) => decodeLogicalShiftedRegister(machineCode),
+ ([_]@[_ ]@[_]@[b0]@ [b1]@[b0]@[b1]@[b1]@ [_ ]@[_ ]@[b0]@ (_ : bits(9)) @[_ ]@(_ : bits(11))) => decodeAddSubtractShiftedRegister(machineCode),
+ ([_]@[_ ]@[_]@[b0]@ [b1]@[b0]@[b1]@[b1]@ [_ ]@[_ ]@[b1]@ (_ : bits(9)) @[_ ]@(_ : bits(11))) => decodeAddSubtractExtendedRegister(machineCode),
+ ([_]@[_ ]@[_]@[b1]@ [b1]@[b0]@[b1]@[b0]@ [b0]@[b0]@[b0]@ (_ : bits(9)) @[_ ]@(_ : bits(11))) => decodeAddSubtractWithCarry(machineCode),
+ ([_]@[_ ]@[_]@[b1]@ [b1]@[b0]@[b1]@[b0]@ [b0]@[b1]@[b0]@ (_ : bits(9)) @[b0]@(_ : bits(11))) => decodeConditionalCompareRegister(machineCode),
+ ([_]@[_ ]@[_]@[b1]@ [b1]@[b0]@[b1]@[b0]@ [b0]@[b1]@[b0]@ (_ : bits(9)) @[b1]@(_ : bits(11))) => decodeConditionalCompareImmediate(machineCode),
+ ([_]@[_ ]@[_]@[b1]@ [b1]@[b0]@[b1]@[b0]@ [b1]@[b0]@[b0]@ (_ : bits(9)) @[_ ]@(_ : bits(11))) => decodeConditionalSelect(machineCode),
+ ([_]@[_ ]@[_]@[b1]@ [b1]@[b0]@[b1]@[b1]@ [_ ]@[_ ]@[_] @ (_ : bits(9)) @[_ ]@(_ : bits(11))) => decodeData3Source(machineCode),
+ ([_]@[b0]@[_]@[b1]@ [b1]@[b0]@[b1]@[b0]@ [b1]@[b1]@[b0]@ (_ : bits(9)) @[_ ]@(_ : bits(11))) => decodeData2Source(machineCode),
+ ([_]@[b1]@[_]@[b1]@ [b1]@[b0]@[b1]@[b0]@ [b1]@[b1]@[b0]@ (_ : bits(9)) @[_ ]@(_ : bits(11))) => decodeData1Source(machineCode)
}
}
-val decodeDataImmediate : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
+val decodeDataImmediate : bits(32) -> option(ast) effect {escape}
function decodeDataImmediate (machineCode) = {
match machineCode {
- ((_ : bits(3))@[1]@[0]@[0]@[0]@[0]@[_]@(_ : bits(23))) => decodePCRelAddressing(machineCode),
- ((_ : bits(3))@[1]@[0]@[0]@[0]@[1]@[_]@(_ : bits(23))) => decodeAddSubtractImmediate(machineCode),
- ((_ : bits(3))@[1]@[0]@[0]@[1]@[0]@[0]@(_ : bits(23))) => decodeLogicalImmediate(machineCode),
- ((_ : bits(3))@[1]@[0]@[0]@[1]@[0]@[1]@(_ : bits(23))) => decodeMoveWideImmediate(machineCode),
- ((_ : bits(3))@[1]@[0]@[0]@[1]@[1]@[0]@(_ : bits(23))) => decodeBitfield(machineCode),
- ((_ : bits(3))@[1]@[0]@[0]@[1]@[1]@[1]@(_ : bits(23))) => decodeExtract(machineCode)
+ ((_ : bits(3))@[b1]@[b0]@[b0]@[b0]@[b0]@[_ ]@(_ : bits(23))) => decodePCRelAddressing(machineCode),
+ ((_ : bits(3))@[b1]@[b0]@[b0]@[b0]@[b1]@[_ ]@(_ : bits(23))) => decodeAddSubtractImmediate(machineCode),
+ ((_ : bits(3))@[b1]@[b0]@[b0]@[b1]@[b0]@[b0]@(_ : bits(23))) => decodeLogicalImmediate(machineCode),
+ ((_ : bits(3))@[b1]@[b0]@[b0]@[b1]@[b0]@[b1]@(_ : bits(23))) => decodeMoveWideImmediate(machineCode),
+ ((_ : bits(3))@[b1]@[b0]@[b0]@[b1]@[b1]@[b0]@(_ : bits(23))) => decodeBitfield(machineCode),
+ ((_ : bits(3))@[b1]@[b0]@[b0]@[b1]@[b1]@[b1]@(_ : bits(23))) => decodeExtract(machineCode)
}
}
-val decodeLoadsStores : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
+val decodeLoadsStores : bits(32) -> option(ast) effect {escape}
function decodeLoadsStores (machineCode) = {
match machineCode {
- ([_]@[_]@[0]@[0]@ [1]@[0]@[0]@[0]@ [_]@[_]@[_]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreExclusive(machineCode),
- ([_]@[_]@[0]@[1]@ [1]@[_]@[0]@[0]@ [_]@[_]@[_]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadRegisterLiteral(machineCode),
- ([_]@[_]@[1]@[0]@ [1]@[_]@[0]@[0]@ [0]@[_]@[_]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreNoAllocatePairOffset(machineCode),
- ([_]@[_]@[1]@[0]@ [1]@[_]@[0]@[0]@ [1]@[_]@[_]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreRegisterPairPostIndexed(machineCode),
- ([_]@[_]@[1]@[0]@ [1]@[_]@[0]@[1]@ [0]@[_]@[_]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreRegisterPairOffset(machineCode),
- ([_]@[_]@[1]@[0]@ [1]@[_]@[0]@[1]@ [1]@[_]@[_]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreRegisterPairPreIndexed(machineCode),
- ([_]@[_]@[1]@[1]@ [1]@[_]@[0]@[0]@ [_]@[_]@[0]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[0]@[0]@ (_ : bits(10)) ) => decodeLoadStoreRegisterUnscaledImmediate(machineCode),
- ([_]@[_]@[1]@[1]@ [1]@[_]@[0]@[0]@ [_]@[_]@[0]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[0]@[1]@ (_ : bits(10)) ) => decodeLoadStoreRegisterImmediatePostIndexed(machineCode),
- ([_]@[_]@[1]@[1]@ [1]@[_]@[0]@[0]@ [_]@[_]@[0]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[1]@[0]@ (_ : bits(10)) ) => decodeLoadStoreRegisterUnprivileged(machineCode),
- ([_]@[_]@[1]@[1]@ [1]@[_]@[0]@[0]@ [_]@[_]@[0]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[1]@[1]@ (_ : bits(10)) ) => decodeLoadStoreRegisterImmediatePreIndexed(machineCode),
- ([_]@[_]@[1]@[1]@ [1]@[_]@[0]@[0]@ [_]@[_]@[1]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[1]@[0]@ (_ : bits(10)) ) => decodeLoadStoreRegisterRegisterOffset(machineCode),
- ([_]@[_]@[1]@[1]@ [1]@[_]@[0]@[1]@ [_]@[_]@[_]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreRegisterUnsignedImmediate(machineCode),
- ([0]@[_]@[0]@[0]@ [1]@[1]@[0]@[0]@ [0]@[_]@[0]@[0]@ [0]@[0]@[0]@[0]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeAdvSIMDLoadStoreMultiStruct(machineCode),
- ([0]@[_]@[0]@[0]@ [1]@[1]@[0]@[0]@ [1]@[_]@[0]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeAdvSIMDLoadStoreMultiStructPostIndexed(machineCode),
- ([0]@[_]@[0]@[0]@ [1]@[1]@[0]@[1]@ [0]@[_]@[_]@[0]@ [0]@[0]@[0]@[0]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeAdvSIMDLoadStoreSingleStruct(machineCode),
- ([0]@[_]@[0]@[0]@ [1]@[1]@[0]@[1]@ [1]@[_]@[_]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeAdvSIMDLoadStoreSingleStructPostIndexed(machineCode)
+ ([_ ]@[_]@[b0]@[b0]@ [b1]@[b0]@[b0]@[b0]@ [_ ]@[_]@[_ ]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreExclusive(machineCode),
+ ([_ ]@[_]@[b0]@[b1]@ [b1]@[_ ]@[b0]@[b0]@ [_ ]@[_]@[_ ]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadRegisterLiteral(machineCode),
+ ([_ ]@[_]@[b1]@[b0]@ [b1]@[_ ]@[b0]@[b0]@ [b0]@[_]@[_ ]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreNoAllocatePairOffset(machineCode),
+ ([_ ]@[_]@[b1]@[b0]@ [b1]@[_ ]@[b0]@[b0]@ [b1]@[_]@[_ ]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreRegisterPairPostIndexed(machineCode),
+ ([_ ]@[_]@[b1]@[b0]@ [b1]@[_ ]@[b0]@[b1]@ [b0]@[_]@[_ ]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreRegisterPairOffset(machineCode),
+ ([_ ]@[_]@[b1]@[b0]@ [b1]@[_ ]@[b0]@[b1]@ [b1]@[_]@[_ ]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreRegisterPairPreIndexed(machineCode),
+ ([_ ]@[_]@[b1]@[b1]@ [b1]@[_ ]@[b0]@[b0]@ [_ ]@[_]@[b0]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[b0]@[b0]@ (_ : bits(10)) ) => decodeLoadStoreRegisterUnscaledImmediate(machineCode),
+ ([_ ]@[_]@[b1]@[b1]@ [b1]@[_ ]@[b0]@[b0]@ [_ ]@[_]@[b0]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[b0]@[b1]@ (_ : bits(10)) ) => decodeLoadStoreRegisterImmediatePostIndexed(machineCode),
+ ([_ ]@[_]@[b1]@[b1]@ [b1]@[_ ]@[b0]@[b0]@ [_ ]@[_]@[b0]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[b1]@[b0]@ (_ : bits(10)) ) => decodeLoadStoreRegisterUnprivileged(machineCode),
+ ([_ ]@[_]@[b1]@[b1]@ [b1]@[_ ]@[b0]@[b0]@ [_ ]@[_]@[b0]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[b1]@[b1]@ (_ : bits(10)) ) => decodeLoadStoreRegisterImmediatePreIndexed(machineCode),
+ ([_ ]@[_]@[b1]@[b1]@ [b1]@[_ ]@[b0]@[b0]@ [_ ]@[_]@[b1]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[b1]@[b0]@ (_ : bits(10)) ) => decodeLoadStoreRegisterRegisterOffset(machineCode),
+ ([_ ]@[_]@[b1]@[b1]@ [b1]@[_ ]@[b0]@[b1]@ [_ ]@[_]@[_ ]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeLoadStoreRegisterUnsignedImmediate(machineCode),
+ ([b0]@[_]@[b0]@[b0]@ [b1]@[b1]@[b0]@[b0]@ [b0]@[_]@[b0]@[b0]@ [b0]@[b0]@[b0]@[b0]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeAdvSIMDLoadStoreMultiStruct(machineCode),
+ ([b0]@[_]@[b0]@[b0]@ [b1]@[b1]@[b0]@[b0]@ [b1]@[_]@[b0]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeAdvSIMDLoadStoreMultiStructPostIndexed(machineCode),
+ ([b0]@[_]@[b0]@[b0]@ [b1]@[b1]@[b0]@[b1]@ [b0]@[_]@[_ ]@[b0]@ [b0]@[b0]@[b0]@[b0]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeAdvSIMDLoadStoreSingleStruct(machineCode),
+ ([b0]@[_]@[b0]@[b0]@ [b1]@[b1]@[b0]@[b1]@ [b1]@[_]@[_ ]@[_]@ [_]@[_]@[_]@[_]@ (_ : bits(4)) @[_]@[_]@ (_ : bits(10)) ) => decodeAdvSIMDLoadStoreSingleStructPostIndexed(machineCode)
}
}
-val decodeSystemImplementationDefined : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
+val decodeSystemImplementationDefined : bits(32) -> option(ast) effect {escape}
function decodeSystemImplementationDefined (machineCode) = {
match machineCode {
- ((_ : bits(11)) @[0]@[1]@[_]@[_]@[_]@[1]@[_]@[1]@[1]@(_ : bits(12))) => decodeImplementationDefined(machineCode),
- ((_ : bits(11)) @[1]@[1]@[_]@[_]@[_]@[1]@[_]@[1]@[1]@(_ : bits(12))) => decodeImplementationDefined(machineCode),
- ((_ : bits(11)) @[_]@[_]@[_]@[_]@[_]@[_]@[_]@[_]@[_]@(_ : bits(12))) => decodeSystem(machineCode)
+ ((_ : bits(11)) @[b0]@[b1]@[_]@[_]@[_]@[b1]@[_]@[b1]@[b1]@(_ : bits(12))) => decodeImplementationDefined(machineCode),
+ ((_ : bits(11)) @[b1]@[b1]@[_]@[_]@[_]@[b1]@[_]@[b1]@[b1]@(_ : bits(12))) => decodeImplementationDefined(machineCode),
+ ((_ : bits(11)) @[_ ]@[_ ]@[_]@[_]@[_]@[_ ]@[_]@[_ ]@[_ ]@(_ : bits(12))) => decodeSystem(machineCode)
}
}
-val decodeBranchesExceptionSystem : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect pure
+val decodeBranchesExceptionSystem : bits(32) -> option(ast) effect {escape}
function decodeBranchesExceptionSystem (machineCode) = {
match machineCode {
- ([_]@[0]@[0]@[1]@[0]@[1]@[_]@[_]@[_]@[_]@(_ : bits(22))) => decodeUnconditionalBranchImmediate(machineCode),
- ([_]@[0]@[1]@[1]@[0]@[1]@[0]@[_]@[_]@[_]@(_ : bits(22))) => decodeCompareBranchImmediate(machineCode),
- ([_]@[0]@[1]@[1]@[0]@[1]@[1]@[_]@[_]@[_]@(_ : bits(22))) => decodeTestBranchImmediate(machineCode),
- ([0]@[1]@[0]@[1]@[0]@[1]@[0]@[_]@[_]@[_]@(_ : bits(22))) => decodeConditionalBranchImmediate(machineCode),
- ([1]@[1]@[0]@[1]@[0]@[1]@[0]@[0]@[_]@[_]@(_ : bits(22))) => decodeExceptionGeneration(machineCode),
- ([1]@[1]@[0]@[1]@[0]@[1]@[0]@[1]@[0]@[0]@(_ : bits(22))) => decodeSystemImplementationDefined(machineCode),
- ([1]@[1]@[0]@[1]@[0]@[1]@[1]@[_]@[_]@[_]@(_ : bits(22))) => decodeUnconditionalBranchRegister(machineCode)
+ ([_ ]@[b0]@[b0]@[b1]@[b0]@[b1]@[_ ]@[_]@[_]@[_]@(_ : bits(22))) => decodeUnconditionalBranchImmediate(machineCode),
+ ([_ ]@[b0]@[b1]@[b1]@[b0]@[b1]@[b0]@[_]@[_]@[_]@(_ : bits(22))) => decodeCompareBranchImmediate(machineCode),
+ ([_ ]@[b0]@[b1]@[b1]@[b0]@[b1]@[b1]@[_]@[_]@[_]@(_ : bits(22))) => decodeTestBranchImmediate(machineCode),
+ ([b0]@[b1]@[b0]@[b1]@[b0]@[b1]@[b0]@[_]@[_]@[_]@(_ : bits(22))) => decodeConditionalBranchImmediate(machineCode),
+ ([b1]@[b1]@[b0]@[b1]@[b0]@[b1]@[b0]@[b0]@[_]@[_]@(_ : bits(22))) => decodeExceptionGeneration(machineCode),
+ ([b1]@[b1]@[b0]@[b1]@[b0]@[b1]@[b0]@[b1]@[b0]@[b0]@(_ : bits(22))) => decodeSystemImplementationDefined(machineCode),
+ ([b1]@[b1]@[b0]@[b1]@[b0]@[b1]@[b1]@[_]@[_]@[_]@(_ : bits(22))) => decodeUnconditionalBranchRegister(machineCode)
}
}
-val decode : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast) effect {escape}
+val decode : bits(32) -> option(ast) effect {escape}
function decode (machineCode) = {
match machineCode {
- ((_ : bits(3)) @[0]@[0]@[_]@[_]@(_ : bits(25))) => Some(Unallocated),
- ((_ : bits(3)) @[1]@[0]@[0]@[_]@(_ : bits(25))) => decodeDataImmediate(machineCode),
- ((_ : bits(3)) @[1]@[0]@[1]@[_]@(_ : bits(25))) => decodeBranchesExceptionSystem(machineCode),
- ((_ : bits(3)) @[_]@[1]@[_]@[0]@(_ : bits(25))) => decodeLoadsStores(machineCode),
- ((_ : bits(3)) @[_]@[1]@[0]@[1]@(_ : bits(25))) => decodeDataRegister(machineCode),
- ((_ : bits(3)) @[0]@[1]@[1]@[1]@(_ : bits(25))) => decodeDataSIMDFPoint1(machineCode),
- ((_ : bits(3)) @[1]@[1]@[1]@[1]@(_ : bits(25))) => decodeDataSIMDFPoint2(machineCode),
- _ => None
+ ((_ : bits(3)) @[b0]@[b0]@[_ ]@[_ ]@(_ : bits(25))) => Some(Unallocated()),
+ ((_ : bits(3)) @[b1]@[b0]@[b0]@[_ ]@(_ : bits(25))) => decodeDataImmediate(machineCode),
+ ((_ : bits(3)) @[b1]@[b0]@[b1]@[_ ]@(_ : bits(25))) => decodeBranchesExceptionSystem(machineCode),
+ ((_ : bits(3)) @[_ ]@[b1]@[_ ]@[b0]@(_ : bits(25))) => decodeLoadsStores(machineCode),
+ ((_ : bits(3)) @[_ ]@[b1]@[b0]@[b1]@(_ : bits(25))) => decodeDataRegister(machineCode),
+ ((_ : bits(3)) @[b0]@[b1]@[b1]@[b1]@(_ : bits(25))) => decodeDataSIMDFPoint1(machineCode),
+ ((_ : bits(3)) @[b1]@[b1]@[b1]@[b1]@(_ : bits(25))) => decodeDataSIMDFPoint2(machineCode),
+ _ => None()
}
}
end execute
-val supported_instructions : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}. ast -> option(ast) effect pure
+val supported_instructions : ast -> option(ast) effect {escape}
function supported_instructions (instr) = {
match instr {
_ => Some(instr)
diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail
index e92b6fa4..5b6cd52e 100644
--- a/aarch64_small/armV8_common_lib.sail
+++ b/aarch64_small/armV8_common_lib.sail
@@ -387,10 +387,11 @@ function SInt(x) = {
/** FUNCTION:bits(N) SignExtend(bits(M) x, integer N) */
-function SignExtend (N, ([h]@(remainder : bits('M - 1)) as x) : bits('M)) = {
- let M = length(x); /* necessary for the type system to rewrite sizeof */
- (Replicate([h]) : bits(('N - 'M))) @ x
- }
+function SignExtend (N, x : bits('M)) = {
+ let M = length(x); /* necessary for the type system to rewrite sizeof */
+ let h = x[M - 1];
+ (Replicate([h]) : bits(('N - 'M))) @ x
+}
/** FUNCTION:integer UInt(bits(N) x) */
diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail
index 55667949..ffb91630 100644
--- a/aarch64_small/prelude.sail
+++ b/aarch64_small/prelude.sail
@@ -173,3 +173,4 @@ function error(message) = {
type min ('M : Int, 'N : Int) = {'O, ('O == 'M | 'O == 'N) & 'O <= 'M & 'O <= 'N. atom('O)}
+val appendL : forall ('a:Type). (list('a),list('a)) -> list('a)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 10:39:04 +0000