summaryrefslogtreecommitdiff
path: root/aarch64
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64')
-rw-r--r--aarch64/no_vector/spec.sail343
-rw-r--r--aarch64/prelude.sail38
2 files changed, 166 insertions, 215 deletions
diff --git a/aarch64/no_vector/spec.sail b/aarch64/no_vector/spec.sail
index ccf8aba1..024393ad 100644
--- a/aarch64/no_vector/spec.sail
+++ b/aarch64/no_vector/spec.sail
@@ -1702,9 +1702,9 @@ function ExternalInvasiveDebugEnabled () = return(DBGEN == HIGH)
val ConstrainUnpredictableInteger : (int, int, Unpredictable) -> (Constraint, int) effect {undef}
-function ConstrainUnpredictableInteger (low, high, which) = {
+function ConstrainUnpredictableInteger ('low, 'high, which) = {
c : Constraint = ConstrainUnpredictable(which);
- if c == Constraint_UNKNOWN then return((c, low)) else return((c, undefined : int))
+ if c == Constraint_UNKNOWN then return((c, low)) else return((c, undefined))
}
val ConstrainUnpredictableBool : Unpredictable -> bool effect {escape}
@@ -1803,7 +1803,7 @@ function LookUpRIndex ('n, mode) = {
return(result)
}
-val HighestSetBit : forall ('N : Int), 'N >= 2. bits('N) -> int
+val HighestSetBit : forall ('N : Int), 'N >= 0. bits('N) -> int
function HighestSetBit x = {
foreach (i from ('N - 1) to 0 by 1 in dec)
@@ -1819,12 +1819,13 @@ val CountLeadingSignBits : forall ('N : Int), 'N >= 3. bits('N) -> int
function CountLeadingSignBits x = return(CountLeadingZeroBits(x[(('N - 1) - 1) + 1 .. 1] ^ x[('N - 1) - 1 .. 0]))
-val BitReverse : forall ('N : Int), 'N >= 2. bits('N) -> bits('N) effect {undef}
+val BitReverse : forall ('N : Int), 'N >= 0 & 'N >= 0.
+ bits('N) -> bits('N) effect {undef}
function BitReverse data = {
result : bits('N) = undefined;
foreach (i from 0 to ('N - 1) by 1 in inc)
- result[('N - i) - 1 .. ('N - i) - 1] = [data[i]];
+ result = __SetSlice_bits('N, 1, result, ('N - i) - 1, [data[i]]);
return(result)
}
@@ -2063,9 +2064,7 @@ val Replicate : forall ('M : Int) ('N : Int), 'M >= 0 & 'N >= 0.
function Replicate x = {
assert('N % 'M == 0, "((N MOD M) == 0)");
- let 'p = ex_int('N / 'M);
- assert(constraint('N = 'p * 'M));
- return(replicate_bits(x, p))
+ return(replicate_bits(x, 'N / 'M))
}
val Zeros__0 : forall ('N : Int), 'N >= 0. atom('N) -> bits('N)
@@ -2306,7 +2305,7 @@ val ConstrainUnpredictableBits : forall ('width : Int), 'width >= 0.
function ConstrainUnpredictableBits which = {
c : Constraint = ConstrainUnpredictable(which);
- if c == Constraint_UNKNOWN then return((c, Zeros('width))) else return((c, undefined : bits('width)))
+ if c == Constraint_UNKNOWN then return((c, Zeros('width))) else return((c, undefined))
}
val AArch64_SysInstrWithResult : (int, int, int, int, int) -> bits(64) effect {escape}
@@ -2741,17 +2740,15 @@ function aarch64_integer_insext_extract_immediate ('d, 'datasize, 'lsb, 'm, 'n)
aset_X(d, result)
}
-val aarch64_integer_arithmetic_rev : (int, int, int, int) -> unit effect {escape, wreg, undef, rreg}
+val aarch64_integer_arithmetic_rev : (int, int, int, int) -> unit effect {escape, rreg, undef, wreg}
-function aarch64_integer_arithmetic_rev ('container_size, 'd, 'datasize, 'n) = {
+function aarch64_integer_arithmetic_rev ('container_size, 'd, 'datasize, 'n) = let 'dbytes = ex_int(datasize / 8) in {
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
- assert(constraint('container_size >= 0 + 1));
+ assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
operand : bits('datasize) = aget_X(n);
result : bits('datasize) = undefined;
- let 'containers : int = datasize / container_size;
- assert(constraint('containers * 'container_size = 'datasize));
- let 'elements_per_container : int = container_size / 8;
- assert(constraint('elements_per_container * 8 = 'container_size));
+ containers : int = datasize / container_size;
+ elements_per_container : int = container_size / 8;
index : int = 0;
rev_index : int = undefined;
foreach (c from 0 to (containers - 1) by 1 in inc) {
@@ -2928,7 +2925,7 @@ function aarch64_integer_arithmetic_addsub_carry ('d, 'datasize, 'm, 'n, setflag
nzcv : bits(4) = undefined;
if sub_op then operand2 = ~(operand2) else ();
(result, nzcv) = AddWithCarry(operand1, operand2, PSTATE.C);
- if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else ();
+ if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else ();
aset_X(d, result)
}
@@ -3102,7 +3099,7 @@ function aarch64_integer_logical_shiftedreg ('d, 'datasize, invert, 'm, 'n, op,
LogicalOp_ORR => result = operand1 | operand2,
LogicalOp_EOR => result = operand1 ^ operand2
};
- if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else ();
+ if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else ();
aset_X(d, result)
}
@@ -3121,7 +3118,7 @@ function aarch64_integer_arithmetic_addsub_shiftedreg ('d, 'datasize, 'm, 'n, se
carry_in = 0b1
} else carry_in = 0b0;
(result, nzcv) = AddWithCarry(operand1, operand2, carry_in);
- if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else ();
+ if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else ();
aset_X(d, result)
}
@@ -3254,7 +3251,7 @@ function aarch64_integer_logical_immediate ('d, datasize, imm, 'n, op, setflags)
LogicalOp_ORR => result = operand1 | operand2,
LogicalOp_EOR => result = operand1 ^ operand2
};
- if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else ();
+ if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = ([result[datasize - 1]] @ IsZeroBit(result)) @ 0b00 else ();
if d == 31 & ~(setflags) then aset_SP(result) else aset_X(d, result)
}
@@ -3274,7 +3271,7 @@ function aarch64_integer_arithmetic_addsub_immediate ('d, datasize, imm, 'n, set
carry_in = 0b1
} else carry_in = 0b0;
(result, nzcv) = AddWithCarry(operand1, operand2, carry_in);
- if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else ();
+ if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else ();
if d == 31 & ~(setflags) then aset_SP(result) else aset_X(d, result)
}
@@ -3293,7 +3290,7 @@ function aarch64_integer_arithmetic_addsub_extendedreg ('d, 'datasize, extend_ty
carry_in = 0b1
} else carry_in = 0b0;
(result, nzcv) = AddWithCarry(operand1, operand2, carry_in);
- if setflags then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = nzcv else ();
+ if setflags then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = nzcv else ();
if d == 31 & ~(setflags) then aset_SP(result) else aset_X(d, result)
}
@@ -3972,7 +3969,7 @@ function FPToFixedJS (op, fpcr, Is64) = {
} else ();
if sign == 0b1 & value_name == 0.0 then Z = 0b0 else ();
if typ == FPType_Infinity then result = 0 else ();
- if Is64 then (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = (0b0 @ Z) @ 0b00 else FPSCR = __SetSlice_bits(32, 4, FPSCR, 28, (0b0 @ Z) @ 0b00);
+ if Is64 then (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = (0b0 @ Z) @ 0b00 else FPSCR = __SetSlice_bits(32, 4, FPSCR, 28, (0b0 @ Z) @ 0b00);
return(__GetSlice_int(32, result, 0))
}
@@ -4479,11 +4476,11 @@ function Halt reason = {
else assert([EDSCR[16]] == 0b1, "((EDSCR).SDD == '1')");
EDSCR[20 .. 20] = 0b0;
if UsingAArch32() then {
- (PSTATE.SS, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(4);
+ (PSTATE.SS @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(4);
PSTATE.IT = 0x00;
PSTATE.T = 0b1
} else
- (PSTATE.SS, PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(5);
+ (PSTATE.SS @ PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(5);
PSTATE.IL = 0b0;
StopInstructionPrefetchAndEnableITR();
EDSCR[5 .. 0] = reason;
@@ -4915,7 +4912,7 @@ function aarch64_integer_conditional_compare_register (condition, 'datasize, fla
} else ();
(__anon1, flags) = AddWithCarry(operand1, operand2, carry_in)
} else ();
- (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = flags
+ (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = flags
}
val integer_conditional_compare_register_decode : (bits(1), bits(1), bits(1), bits(5), bits(4), bits(1), bits(5), bits(1), bits(4)) -> unit effect {escape, rreg, undef, wreg}
@@ -4949,7 +4946,7 @@ function aarch64_integer_conditional_compare_immediate (condition, datasize, fla
} else ();
(__anon1, flags) = AddWithCarry(operand1, operand2, carry_in)
} else ();
- (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = flags
+ (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = flags
}
val integer_conditional_compare_immediate_decode : (bits(1), bits(1), bits(1), bits(5), bits(4), bits(1), bits(5), bits(1), bits(4)) -> unit effect {escape, wreg, undef, rreg}
@@ -6004,13 +6001,13 @@ function AArch64_TranslateAddressS1Off (vaddress, acctype, iswrite) = {
return(result)
}
-val AArch64_MaybeZeroRegisterUppers : unit -> unit effect {wreg, undef, rreg, escape}
+val AArch64_MaybeZeroRegisterUppers : unit -> unit effect {escape, rreg, undef, wreg}
function AArch64_MaybeZeroRegisterUppers () = {
assert(UsingAArch32(), "UsingAArch32()");
include_R15_name : bool = undefined;
- last : range(14, 30) = undefined;
- first : atom(0) = 0;
+ last : int = undefined;
+ first : int = undefined;
if PSTATE.EL == EL0 & ~(ELUsingAArch32(EL1)) then {
first = 0;
last = 14;
@@ -6025,9 +6022,9 @@ function AArch64_MaybeZeroRegisterUppers () = {
include_R15_name = true
};
foreach (n from first to last by 1 in inc)
- if (n : int != 15 : int | include_R15_name) & ConstrainUnpredictableBool(Unpredictable_ZEROUPPER) then {
+ if (n != 15 | include_R15_name) & ConstrainUnpredictableBool(Unpredictable_ZEROUPPER) then {
__tmp_3 : bits(64) = _R[n];
- __tmp_3[63 .. 32] = Zeros(32);
+ __tmp_3 = __SetSlice_bits(64, 32, __tmp_3, 32, Zeros());
_R[n] = __tmp_3
} else ();
()
@@ -6800,9 +6797,21 @@ function AArch64_StateMatch (SSC__arg, HMC__arg, PxC__arg, linked__arg, LBN, isb
return((priv_match & security_state_match) & (~(linked) | linked_match))
}
-val AArch64_WatchpointMatch : (int, bits(64), int, bool, bool) -> bool
+val AArch64_WatchpointMatch : (int, bits(64), int, bool, bool) -> bool effect {escape, rreg, undef}
-function AArch64_WatchpointMatch (n, vaddress, size, ispriv, iswrite) = false
+function AArch64_WatchpointMatch ('n, vaddress, 'size, ispriv, iswrite) = {
+ assert(~(ELUsingAArch32(S1TranslationRegime())), "!(ELUsingAArch32(S1TranslationRegime()))");
+ assert(n <= UInt(slice(ID_AA64DFR0_EL1, 20, 4)), "(n <= UInt((ID_AA64DFR0_EL1).WRPs))");
+ enabled : bool = [DBGWCR_EL1[n][0]] == 0b1;
+ linked : bool = [DBGWCR_EL1[n][20]] == 0b1;
+ isbreakpnt : bool = false;
+ state_match : bool = AArch64_StateMatch(slice(DBGWCR_EL1[n], 14, 2), [DBGWCR_EL1[n][13]], slice(DBGWCR_EL1[n], 1, 2), linked, slice(DBGWCR_EL1[n], 16, 4), isbreakpnt, ispriv);
+ ls_match : bool = [slice(DBGWCR_EL1[n], 3, 2)[if iswrite then 1 else 0]] == 0b1;
+ value_match_name : bool = false;
+ foreach (byte from 0 to (size - 1) by 1 in inc)
+ value_match_name = value_match_name | AArch64_WatchpointByteMatch(n, vaddress + byte);
+ return(((value_match_name & state_match) & ls_match) & enabled)
+}
val AArch64_BreakpointMatch : (int, bits(64), int) -> bool effect {escape, rreg, undef}
@@ -6955,7 +6964,7 @@ function AArch64_TakeReset cold_reset = {
else PSTATE.EL = EL1;
AArch64_ResetControlRegisters(cold_reset);
PSTATE.SP = 0b1;
- (PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = 0xF;
+ (PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = 0xF;
PSTATE.SS = 0b0;
PSTATE.IL = 0b0;
AArch64_ResetGeneralRegisters();
@@ -6991,11 +7000,18 @@ function AArch64_TakeException (target_el, exception, preferred_exception_return
if from_32 then AArch64_MaybeZeroRegisterUppers() else ();
if UInt(target_el) > UInt(PSTATE.EL) then {
lower_32 : bool = undefined;
- if target_el == EL3 then if ~(IsSecure()) & HaveEL(EL2) then lower_32 = ELUsingAArch32(EL2) else lower_32 = ELUsingAArch32(EL1) else if (IsInHost() & PSTATE.EL == EL0) & target_el == EL2 then lower_32 = ELUsingAArch32(EL0) else lower_32 = ELUsingAArch32(target_el - 1);
+ if target_el == EL3 then
+ if ~(IsSecure()) & HaveEL(EL2) then lower_32 = ELUsingAArch32(EL2)
+ else lower_32 = ELUsingAArch32(EL1)
+ else if (IsInHost() & PSTATE.EL == EL0) & target_el == EL2 then
+ lower_32 = ELUsingAArch32(EL0)
+ else lower_32 = ELUsingAArch32(target_el - 1);
vect_offset = vect_offset + (if lower_32 then 1536 else 1024)
- } else if PSTATE.SP == 0b1 then vect_offset = vect_offset + 512 else ();
+ } else if PSTATE.SP == 0b1 then vect_offset = vect_offset + 512
+ else ();
spsr : bits(32) = GetPSRFromPSTATE();
- if HaveUAOExt() then PSTATE.UAO = 0b0 else ();
+ if HaveUAOExt() then PSTATE.UAO = 0b0
+ else ();
if ~(exception.typ == Exception_IRQ | exception.typ == Exception_FIQ) then AArch64_ReportException(exception, target_el) else ();
PSTATE.EL = target_el;
PSTATE.nRW = 0b0;
@@ -7003,13 +7019,15 @@ function AArch64_TakeException (target_el, exception, preferred_exception_return
aset_SPSR(spsr);
aset_ELR(preferred_exception_return);
PSTATE.SS = 0b0;
- (PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = 0xF;
+ (PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = 0xF;
PSTATE.IL = 0b0;
if from_32 then {
PSTATE.IT = 0x00;
PSTATE.T = 0b0
} else ();
- if (HavePANExt() & (PSTATE.EL == EL1 | PSTATE.EL == EL2 & ELIsInHost(EL0))) & [aget_SCTLR()[23]] == 0b0 then PSTATE.PAN = 0b1 else ();
+ if (HavePANExt() & (PSTATE.EL == EL1 | PSTATE.EL == EL2 & ELIsInHost(EL0))) & [aget_SCTLR()[23]] == 0b0 then
+ PSTATE.PAN = 0b1
+ else ();
BranchTo(slice(aget_VBAR(), 11, 53) @ __GetSlice_int(11, vect_offset, 0), BranchType_EXCEPTION);
iesb_req : bool = undefined;
if HaveRASExt() & [aget_SCTLR()[21]] == 0b1 then {
@@ -7960,7 +7978,7 @@ function AArch32_EnterMode (target_mode, preferred_exception_return, 'lr_offset,
aset_R(14, preferred_exception_return + lr_offset);
PSTATE.T = [SCTLR[30]];
PSTATE.SS = 0b0;
- if target_mode == M32_FIQ then (PSTATE.A, PSTATE.I, PSTATE.F) = 0b111 else if target_mode == M32_Abort | target_mode == M32_IRQ then (PSTATE.A, PSTATE.I) = 0b11 else PSTATE.I = 0b1;
+ if target_mode == M32_FIQ then (PSTATE.A @ PSTATE.I @ PSTATE.F) = 0b111 else if target_mode == M32_Abort | target_mode == M32_IRQ then (PSTATE.A @ PSTATE.I) = 0b11 else PSTATE.I = 0b1;
PSTATE.E = [SCTLR[25]];
PSTATE.IL = 0b0;
PSTATE.IT = 0x00;
@@ -8120,7 +8138,7 @@ function aarch64_float_compare_uncond (cmp_with_zero, 'datasize, 'm, 'n, signal_
CheckFPAdvSIMDEnabled64();
operand1 : bits('datasize) = aget_V(n);
operand2 : bits('datasize) = if cmp_with_zero then FPZero(0b0) else aget_V(m);
- (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = FPCompare(operand1, operand2, signal_all_nans, FPCR)
+ (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = FPCompare(operand1, operand2, signal_all_nans, FPCR)
}
val aarch64_float_compare_cond : (bits(4), int, bits(4), int, int, bool) -> unit effect {escape, rreg, undef, wreg}
@@ -8133,7 +8151,7 @@ function aarch64_float_compare_cond (condition, 'datasize, flags__arg, 'm, 'n, s
operand1 : bits('datasize) = aget_V(n);
operand2 : bits('datasize) = aget_V(m);
if ConditionHolds(condition) then flags = FPCompare(operand1, operand2, signal_all_nans, FPCR) else ();
- (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = flags
+ (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = flags
}
val aarch64_float_arithmetic_unary : (int, int, FPUnaryOp, int) -> unit effect {escape, rreg, undef, wreg}
@@ -8585,11 +8603,11 @@ function aarch64_memory_vector_multiple_nowb (datasize, elements, esize, m, memo
} else ()
}
-val aarch64_memory_single_simdfp_register : forall ('datasize : Int).
- (AccType, atom('datasize), ExtendType, int, MemOp, int, bool, int, int, bool) -> unit effect {escape, rmem, wmem, undef, wreg, rreg}
+val aarch64_memory_single_simdfp_register : (AccType, int, ExtendType, int, MemOp, int, bool, int, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_single_simdfp_register (acctype, datasize, extend_type, m, memop, n, postindex, shift, t, wback) = {
+function aarch64_memory_single_simdfp_register (acctype, 'datasize, extend_type, 'm, memop, 'n, postindex, 'shift, 't, wback) = let 'dbytes = ex_int(datasize / 8) in {
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
+ assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
offset : bits(64) = ExtendReg(m, extend_type, shift);
CheckFPAdvSIMDEnabled64();
address : bits(64) = undefined;
@@ -8598,32 +8616,28 @@ function aarch64_memory_single_simdfp_register (acctype, datasize, extend_type,
CheckSPAlignment();
address = aget_SP()
} else address = aget_X(n);
- if ~(postindex) then address = address + offset
- else ();
- let 'dq8 = ex_int(datasize / 8);
- assert(constraint(8 * 'dq8 = 'datasize));
+ if ~(postindex) then address = address + offset else ();
match memop {
MemOp_STORE => {
data = aget_V(t);
- aset_Mem(address, dq8, acctype, data)
+ aset_Mem(address, datasize / 8, acctype, data)
},
MemOp_LOAD => {
- data = aget_Mem(address, dq8, acctype);
+ data = aget_Mem(address, datasize / 8, acctype);
aset_V(t, data)
}
};
if wback then {
- if postindex then address = address + offset
- else ();
+ if postindex then address = address + offset else ();
if n == 31 then aset_SP(address) else aset_X(n, address)
} else ()
}
-val aarch64_memory_single_simdfp_immediate_signed_postidx : forall ('datasize : Int).
- (AccType, atom('datasize), MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, rmem, wmem, undef, wreg, rreg}
+val aarch64_memory_single_simdfp_immediate_signed_postidx : (AccType, int, MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, datasize, memop, n, offset, postindex, t, wback) = {
+function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = let 'dbytes = ex_int(datasize / 8) in {
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
+ assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
CheckFPAdvSIMDEnabled64();
address : bits(64) = undefined;
data : bits('datasize) = undefined;
@@ -8631,32 +8645,28 @@ function aarch64_memory_single_simdfp_immediate_signed_postidx (acctype, datasiz
CheckSPAlignment();
address = aget_SP()
} else address = aget_X(n);
- if ~(postindex) then address = address + offset
- else ();
- let 'dq8 = ex_int(datasize / 8);
- assert(constraint('dq8 * 8 = 'datasize));
+ if ~(postindex) then address = address + offset else ();
match memop {
MemOp_STORE => {
data = aget_V(t);
- aset_Mem(address, dq8, acctype, data)
+ aset_Mem(address, datasize / 8, acctype, data)
},
MemOp_LOAD => {
- data = aget_Mem(address, dq8, acctype);
+ data = aget_Mem(address, datasize / 8, acctype);
aset_V(t, data)
}
};
if wback then {
- if postindex then address = address + offset
- else ();
+ if postindex then address = address + offset else ();
if n == 31 then aset_SP(address) else aset_X(n, address)
} else ()
}
-val aarch64_memory_single_simdfp_immediate_signed_offset_normal : forall ('datasize : Int).
- (AccType, atom('datasize), MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+val aarch64_memory_single_simdfp_immediate_signed_offset_normal : (AccType, int, MemOp, int, bits(64), bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, datasize, memop, n, offset, postindex, t, wback) = {
+function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, 'datasize, memop, 'n, offset, postindex, 't, wback) = let 'dbytes = ex_int(datasize / 8) in {
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
+ assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
CheckFPAdvSIMDEnabled64();
address : bits(64) = undefined;
data : bits('datasize) = undefined;
@@ -8664,23 +8674,19 @@ function aarch64_memory_single_simdfp_immediate_signed_offset_normal (acctype, d
CheckSPAlignment();
address = aget_SP()
} else address = aget_X(n);
- if ~(postindex) then address = address + offset
- else ();
- let 'dq8 = ex_int(datasize / 8);
- assert(constraint(8 * 'dq8 = 'datasize));
+ if ~(postindex) then address = address + offset else ();
match memop {
MemOp_STORE => {
data = aget_V(t);
- aset_Mem(address, dq8, acctype, data)
+ aset_Mem(address, datasize / 8, acctype, data)
},
MemOp_LOAD => {
- data = aget_Mem(address, dq8, acctype);
+ data = aget_Mem(address, datasize / 8, acctype);
aset_V(t, data)
}
};
if wback then {
- if postindex then address = address + offset
- else ();
+ if postindex then address = address + offset else ();
if n == 31 then aset_SP(address) else aset_X(n, address)
} else ()
}
@@ -8807,41 +8813,39 @@ function memory_literal_general_decode (opc, V, imm19, Rt) = {
aarch64_memory_literal_general(memop, offset, signed, size, t)
}
-val aarch64_memory_atomicops_swp : forall ('datasize : Int) ('regsize : Int).
- (atom('datasize), AccType, int, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+val aarch64_memory_atomicops_swp : (int, AccType, int, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_atomicops_swp (datasize, ldacctype, n, regsize, s, stacctype, t) = {
- assert(constraint('datasize in {8, 16, 32, 64, 128} & 'regsize >= 0), "datasize constraint");
+function aarch64_memory_atomicops_swp ('datasize, ldacctype, 'n, 'regsize, 's, stacctype, 't) = {
+ assert(constraint('regsize >= 0), "regsize constraint");
+ let 'dbytes = ex_int(datasize / 8);
+ assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
+ assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
address : bits(64) = undefined;
data : bits('datasize) = undefined;
- let 'dbytes = ex_int(datasize / 8);
- assert(constraint(8 * 'dbytes = 'datasize));
if n == 31 then {
CheckSPAlignment();
address = aget_SP()
} else address = aget_X(n);
- data = aget_Mem(address, dbytes, ldacctype);
- aset_Mem(address, dbytes, stacctype, aget_X(s));
+ data = aget_Mem(address, datasize / 8, ldacctype);
+ aset_Mem(address, datasize / 8, stacctype, aget_X(s));
aset_X(t, ZeroExtend(data, regsize))
}
-val aarch64_memory_atomicops_st : forall ('datasize : Int).
- (atom('datasize), AccType, int, MemAtomicOp, int, AccType) -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+val aarch64_memory_atomicops_st : (int, AccType, int, MemAtomicOp, int, AccType) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_atomicops_st (datasize, ldacctype, n, op, s, stacctype) = {
+function aarch64_memory_atomicops_st ('datasize, ldacctype, 'n, op, 's, stacctype) = let 'dbytes = ex_int(datasize / 8) in {
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
+ assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
address : bits(64) = undefined;
value_name : bits('datasize) = undefined;
data : bits('datasize) = undefined;
result : bits('datasize) = undefined;
value_name = aget_X(s);
- let 'dbytes = ex_int(datasize / 8);
- assert(constraint(8 * 'dbytes = 'datasize));
if n == 31 then {
CheckSPAlignment();
address = aget_SP()
} else address = aget_X(n);
- data = aget_Mem(address, dbytes, ldacctype);
+ data = aget_Mem(address, datasize / 8, ldacctype);
match op {
MemAtomicOp_ADD => result = data + value_name,
MemAtomicOp_BIC => result = data & ~(value_name),
@@ -8852,26 +8856,26 @@ function aarch64_memory_atomicops_st (datasize, ldacctype, n, op, s, stacctype)
MemAtomicOp_UMAX => result = if UInt(data) > UInt(value_name) then data else value_name,
MemAtomicOp_UMIN => result = if UInt(data) > UInt(value_name) then value_name else data
};
- aset_Mem(address, dbytes, stacctype, result)
+ aset_Mem(address, datasize / 8, stacctype, result)
}
-val aarch64_memory_atomicops_ld : forall ('datasize : Int) ('regsize : Int).
- (atom('datasize), AccType, int, MemAtomicOp, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+val aarch64_memory_atomicops_ld : (int, AccType, int, MemAtomicOp, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_atomicops_ld (datasize, ldacctype, n, op, regsize, s, stacctype, t) = {
- assert(constraint('datasize in {8, 16, 32, 64, 128} & 'regsize >= 0), "datasize constraint");
+function aarch64_memory_atomicops_ld ('datasize, ldacctype, 'n, op, 'regsize, 's, stacctype, 't) = {
+ assert(constraint('regsize >= 0), "regsize constraint");
+ let 'dbytes = ex_int(datasize / 8);
+ assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
+ assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
address : bits(64) = undefined;
value_name : bits('datasize) = undefined;
data : bits('datasize) = undefined;
result : bits('datasize) = undefined;
value_name = aget_X(s);
- let 'dbytes = ex_int(datasize / 8);
- assert(constraint(8 * 'dbytes = 'datasize));
if n == 31 then {
CheckSPAlignment();
address = aget_SP()
} else address = aget_X(n);
- data = aget_Mem(address, dbytes, ldacctype);
+ data = aget_Mem(address, datasize / 8, ldacctype);
match op {
MemAtomicOp_ADD => result = data + value_name,
MemAtomicOp_BIC => result = data & ~(value_name),
@@ -8882,15 +8886,14 @@ function aarch64_memory_atomicops_ld (datasize, ldacctype, n, op, regsize, s, st
MemAtomicOp_UMAX => result = if UInt(data) > UInt(value_name) then data else value_name,
MemAtomicOp_UMIN => result = if UInt(data) > UInt(value_name) then value_name else data
};
- aset_Mem(address, dbytes, stacctype, result);
+ aset_Mem(address, datasize / 8, stacctype, result);
aset_X(t, ZeroExtend(data, regsize))
}
-val aarch64_memory_atomicops_cas_single : forall ('datasize : Int) ('regsize : Int).
- (atom('datasize), AccType, int, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+val aarch64_memory_atomicops_cas_single : (int, AccType, int, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_atomicops_cas_single (datasize, ldacctype, n, regsize, s, stacctype, t) = {
- assert(constraint('regsize >= 0), "destsize constraint");
+function aarch64_memory_atomicops_cas_single ('datasize, ldacctype, 'n, 'regsize, 's, stacctype, 't) = {
+ assert(constraint('regsize >= 0), "regsize constraint");
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
@@ -8904,19 +8907,18 @@ function aarch64_memory_atomicops_cas_single (datasize, ldacctype, n, regsize, s
CheckSPAlignment();
address = aget_SP()
} else address = aget_X(n);
- data = aget_Mem(address, dbytes, ldacctype);
- if data == comparevalue then aset_Mem(address, dbytes, stacctype, newvalue) else ();
+ data = aget_Mem(address, datasize / 8, ldacctype);
+ if data == comparevalue then aset_Mem(address, datasize / 8, stacctype, newvalue) else ();
aset_X(s, ZeroExtend(data, regsize))
}
-val aarch64_memory_atomicops_cas_pair : forall ('datasize : Int) ('regsize : Int).
- (atom('datasize), AccType, int, atom('regsize), int, AccType, int) -> unit effect {escape, undef, wreg, rreg, rmem, wmem}
+val aarch64_memory_atomicops_cas_pair : (int, AccType, int, int, int, AccType, int) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_atomicops_cas_pair (datasize, ldacctype, n, regsize, s, stacctype, t) = {
- assert(constraint('regsize >= 0), "destsize constraint");
- let 'dbytes = ex_int((2 * datasize) / 8);
+function aarch64_memory_atomicops_cas_pair ('datasize, ldacctype, 'n, 'regsize, 's, stacctype, 't) = {
+ assert(constraint('regsize >= 0), "regsize constraint");
+ let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
- assert(constraint(4 * 'dbytes = 'datasize), "dbytes constraint");
+ assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
address : bits(64) = undefined;
comparevalue : bits(2 * 'datasize) = undefined;
newvalue : bits(2 * 'datasize) = undefined;
@@ -8931,8 +8933,8 @@ function aarch64_memory_atomicops_cas_pair (datasize, ldacctype, n, regsize, s,
CheckSPAlignment();
address = aget_SP()
} else address = aget_X(n);
- data = aget_Mem(address, dbytes, ldacctype);
- if data == comparevalue then aset_Mem(address, dbytes, stacctype, newvalue) else ();
+ data = aget_Mem(address, (2 * datasize) / 8, ldacctype);
+ if data == comparevalue then aset_Mem(address, (2 * datasize) / 8, stacctype, newvalue) else ();
if BigEndian() then {
aset_X(s, ZeroExtend(slice(data, datasize, datasize), regsize));
aset_X(s + 1, ZeroExtend(slice(data, 0, datasize), regsize))
@@ -9051,15 +9053,15 @@ function SetPSTATEFromPSR spsr__arg = {
}
};
if PSTATE.IL == 0b1 & PSTATE.nRW == 0b1 then if ConstrainUnpredictableBool(Unpredictable_ILZEROT) then spsr = __SetSlice_bits(32, 1, spsr, 5, 0b0) else () else ();
- (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V) = slice(spsr, 28, 4);
+ (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V) = slice(spsr, 28, 4);
if PSTATE.nRW == 0b1 then {
PSTATE.Q = [spsr[27]];
PSTATE.IT = RestoredITBits(spsr);
PSTATE.GE = slice(spsr, 16, 4);
PSTATE.E = [spsr[9]];
- (PSTATE.A, PSTATE.I, PSTATE.F) = slice(spsr, 6, 3);
+ (PSTATE.A @ PSTATE.I @ PSTATE.F) = slice(spsr, 6, 3);
PSTATE.T = [spsr[5]]
- } else (PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = slice(spsr, 6, 4);
+ } else (PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = slice(spsr, 6, 4);
if HavePANExt() then PSTATE.PAN = [spsr[22]] else ();
if HaveUAOExt() then PSTATE.UAO = [spsr[23]] else ();
()
@@ -9072,13 +9074,13 @@ function DRPSInstruction () = {
if (HaveRASExt() & [aget_SCTLR()[21]] == 0b1) & ConstrainUnpredictableBool(Unpredictable_IESBinDebug) then ErrorSynchronizationBarrier(MBReqDomain_FullSystem, MBReqTypes_All) else ();
SetPSTATEFromPSR(aget_SPSR());
if UsingAArch32() then {
- (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V, PSTATE.Q, PSTATE.GE, PSTATE.SS, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(13);
+ (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V @ PSTATE.Q @ PSTATE.GE @ PSTATE.SS @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(13);
PSTATE.IT = 0x00;
PSTATE.T = 0b1;
DLR = undefined : bits(32);
DSPSR = undefined : bits(32)
} else {
- (PSTATE.N, PSTATE.Z, PSTATE.C, PSTATE.V, PSTATE.SS, PSTATE.D, PSTATE.A, PSTATE.I, PSTATE.F) = undefined : bits(9);
+ (PSTATE.N @ PSTATE.Z @ PSTATE.C @ PSTATE.V @ PSTATE.SS @ PSTATE.D @ PSTATE.A @ PSTATE.I @ PSTATE.F) = undefined : bits(9);
DLR_EL0 = undefined : bits(64);
DSPSR_EL0 = undefined : bits(32)
};
@@ -9191,11 +9193,10 @@ function system_exceptions_runtime_hvc_decode (opc, imm16, op2, LL) = {
aarch64_system_exceptions_runtime_hvc(imm)
}
-val aarch64_memory_single_general_register : forall ('datasize : Int) ('regsize : Int).
- (AccType, atom('datasize), ExtendType, int, MemOp, int, bool, atom('regsize), int, bool, int, bool) -> unit effect {escape, undef, rreg, wreg, rmem, wmem}
+val aarch64_memory_single_general_register : (AccType, int, ExtendType, int, MemOp, int, bool, int, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_single_general_register (acctype, datasize, extend_type, m, memop, n, postindex, regsize, shift, signed, t, wback__arg) = {
- assert(constraint('regsize >= 0), "destsize constraint");
+function aarch64_memory_single_general_register (acctype, 'datasize, extend_type, 'm, memop, 'n, postindex, 'regsize, 'shift, signed, 't, wback__arg) = {
+ assert(constraint('regsize >= 0), "regsize constraint");
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
@@ -9230,33 +9231,28 @@ function aarch64_memory_single_general_register (acctype, datasize, extend_type,
if memop != MemOp_PREFETCH then CheckSPAlignment() else ();
address = aget_SP()
} else address = aget_X(n);
- if ~(postindex) then address = address + offset
- else ();
+ if ~(postindex) then address = address + offset else ();
match memop {
MemOp_STORE => {
- if rt_unknown then data = undefined
- else data = aget_X(t);
- aset_Mem(address, dbytes, acctype, data)
+ if rt_unknown then data = undefined else data = aget_X(t);
+ aset_Mem(address, datasize / 8, acctype, data)
},
MemOp_LOAD => {
- data = aget_Mem(address, dbytes, acctype);
+ data = aget_Mem(address, datasize / 8, acctype);
if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize))
},
MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0))
};
if wback then {
- if wb_unknown then address = undefined
- else if postindex then address = address + offset
- else ();
+ if wb_unknown then address = undefined else if postindex then address = address + offset else ();
if n == 31 then aset_SP(address) else aset_X(n, address)
} else ()
}
-val aarch64_memory_single_general_immediate_unsigned : forall ('datasize : Int) ('regsize : Int).
- (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, wmem, rmem}
+val aarch64_memory_single_general_immediate_unsigned : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_single_general_immediate_unsigned (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = {
- assert(constraint('regsize >= 0), "destsize constraint");
+function aarch64_memory_single_general_immediate_unsigned (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = {
+ assert(constraint('regsize >= 0), "regsize constraint");
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
@@ -9290,33 +9286,28 @@ function aarch64_memory_single_general_immediate_unsigned (acctype, datasize, me
if memop != MemOp_PREFETCH then CheckSPAlignment() else ();
address = aget_SP()
} else address = aget_X(n);
- if ~(postindex) then address = address + offset
- else ();
+ if ~(postindex) then address = address + offset else ();
match memop {
MemOp_STORE => {
- if rt_unknown then data = undefined
- else data = aget_X(t);
- aset_Mem(address, dbytes, acctype, data)
+ if rt_unknown then data = undefined else data = aget_X(t);
+ aset_Mem(address, datasize / 8, acctype, data)
},
MemOp_LOAD => {
- data = aget_Mem(address, dbytes, acctype);
+ data = aget_Mem(address, datasize / 8, acctype);
if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize))
},
MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0))
};
if wback then {
- if wb_unknown then address = undefined
- else if postindex then address = address + offset
- else ();
+ if wb_unknown then address = undefined else if postindex then address = address + offset else ();
if n == 31 then aset_SP(address) else aset_X(n, address)
} else ()
}
-val aarch64_memory_single_general_immediate_signed_postidx : forall ('datasize : Int) ('regsize : Int).
- (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, wmem, rmem}
+val aarch64_memory_single_general_immediate_signed_postidx : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_single_general_immediate_signed_postidx (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = {
- assert(constraint('regsize >= 0), "destsize constraint");
+function aarch64_memory_single_general_immediate_signed_postidx (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = {
+ assert(constraint('regsize >= 0), "regsize constraint");
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
@@ -9350,24 +9341,20 @@ function aarch64_memory_single_general_immediate_signed_postidx (acctype, datasi
if memop != MemOp_PREFETCH then CheckSPAlignment() else ();
address = aget_SP()
} else address = aget_X(n);
- if ~(postindex) then address = address + offset
- else ();
+ if ~(postindex) then address = address + offset else ();
match memop {
MemOp_STORE => {
- if rt_unknown then data = undefined
- else data = aget_X(t);
- aset_Mem(address, dbytes, acctype, data)
+ if rt_unknown then data = undefined else data = aget_X(t);
+ aset_Mem(address, datasize / 8, acctype, data)
},
MemOp_LOAD => {
- data = aget_Mem(address, dbytes, acctype);
+ data = aget_Mem(address, datasize / 8, acctype);
if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize))
},
MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0))
};
if wback then {
- if wb_unknown then address = undefined
- else if postindex then address = address + offset
- else ();
+ if wb_unknown then address = undefined else if postindex then address = address + offset else ();
if n == 31 then aset_SP(address) else aset_X(n, address)
} else ()
}
@@ -9404,11 +9391,10 @@ function aarch64_memory_single_general_immediate_signed_pac ('n, offset, 't, use
} else ()
}
-val aarch64_memory_single_general_immediate_signed_offset_unpriv : forall ('datasize : Int) ('regsize : Int).
- (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, rmem, wmem}
+val aarch64_memory_single_general_immediate_signed_offset_unpriv : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = {
- assert(constraint('regsize >= 0), "destsize constraint");
+function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = {
+ assert(constraint('regsize >= 0), "regsize constraint");
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
@@ -9442,33 +9428,28 @@ function aarch64_memory_single_general_immediate_signed_offset_unpriv (acctype,
if memop != MemOp_PREFETCH then CheckSPAlignment() else ();
address = aget_SP()
} else address = aget_X(n);
- if ~(postindex) then address = address + offset
- else ();
+ if ~(postindex) then address = address + offset else ();
match memop {
MemOp_STORE => {
- if rt_unknown then data = undefined
- else data = aget_X(t);
- aset_Mem(address, dbytes, acctype, data)
+ if rt_unknown then data = undefined else data = aget_X(t);
+ aset_Mem(address, datasize / 8, acctype, data)
},
MemOp_LOAD => {
- data = aget_Mem(address, dbytes, acctype);
+ data = aget_Mem(address, datasize / 8, acctype);
if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize))
},
MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0))
};
if wback then {
- if wb_unknown then address = undefined
- else if postindex then address = address + offset
- else ();
+ if wb_unknown then address = undefined else if postindex then address = address + offset else ();
if n == 31 then aset_SP(address) else aset_X(n, address)
} else ()
}
-val aarch64_memory_single_general_immediate_signed_offset_normal : forall ('datasize : Int) ('regsize : Int).
- (AccType, atom('datasize), MemOp, int, bits(64), bool, atom('regsize), bool, int, bool) -> unit effect {escape, undef, rreg, wreg, rmem, wmem}
+val aarch64_memory_single_general_immediate_signed_offset_normal : (AccType, int, MemOp, int, bits(64), bool, int, bool, int, bool) -> unit effect {escape, rmem, rreg, undef, wmem, wreg}
-function aarch64_memory_single_general_immediate_signed_offset_normal (acctype, datasize, memop, n, offset, postindex, regsize, signed, t, wback__arg) = {
- assert(constraint('regsize >= 0), "destsize constraint");
+function aarch64_memory_single_general_immediate_signed_offset_normal (acctype, 'datasize, memop, 'n, offset, postindex, 'regsize, signed, 't, wback__arg) = {
+ assert(constraint('regsize >= 0), "regsize constraint");
let 'dbytes = ex_int(datasize / 8);
assert(constraint('datasize in {8, 16, 32, 64, 128}), "datasize constraint");
assert(constraint(8 * 'dbytes = 'datasize), "dbytes constraint");
@@ -9502,24 +9483,20 @@ function aarch64_memory_single_general_immediate_signed_offset_normal (acctype,
if memop != MemOp_PREFETCH then CheckSPAlignment() else ();
address = aget_SP()
} else address = aget_X(n);
- if ~(postindex) then address = address + offset
- else ();
+ if ~(postindex) then address = address + offset else ();
match memop {
MemOp_STORE => {
- if rt_unknown then data = undefined
- else data = aget_X(t);
- aset_Mem(address, dbytes, acctype, data)
+ if rt_unknown then data = undefined else data = aget_X(t);
+ aset_Mem(address, datasize / 8, acctype, data)
},
MemOp_LOAD => {
- data = aget_Mem(address, dbytes, acctype);
+ data = aget_Mem(address, datasize / 8, acctype);
if signed then aset_X(t, SignExtend(data, regsize)) else aset_X(t, ZeroExtend(data, regsize))
},
MemOp_PREFETCH => Prefetch(address, __GetSlice_int(5, t, 0))
};
if wback then {
- if wb_unknown then address = undefined
- else if postindex then address = address + offset
- else ();
+ if wb_unknown then address = undefined else if postindex then address = address + offset else ();
if n == 31 then aset_SP(address) else aset_X(n, address)
} else ()
}
diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index 5cf4ce48..097dc7d9 100644
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -1,7 +1,7 @@
default Order dec
$include <smt.sail>
-$include <flow.sail>
+$include <arith.sail>
type bits ('n : Int) = vector('n, dec, bit)
@@ -202,11 +202,6 @@ val real_power = {ocaml: "real_power", lem: "realPowInteger", c: "real_power"} :
overload operator ^ = {xor_vec, int_power, real_power}
-val add_range = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : forall 'n 'm 'o 'p.
- (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p)
-
-val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int"} : (int, int) -> int
-
val add_vec = {
ocaml: "add_vec",
lem: "add_vec",
@@ -221,12 +216,7 @@ val add_vec_int = {
val add_real = {ocaml: "add_real", lem: "realAdd", c: "add_real"} : (real, real) -> real
-overload operator + = {add_range, add_int, add_vec, add_vec_int, add_real}
-
-val sub_range = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : forall 'n 'm 'o 'p.
- (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o)
-
-val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int"} : (int, int) -> int
+overload operator + = {add_vec, add_vec_int, add_real}
val "sub_vec" : forall 'n. (bits('n), bits('n)) -> bits('n)
@@ -238,24 +228,15 @@ val sub_vec_int = {
val sub_real = {ocaml: "sub_real", lem: "realMinus", c: "sub_real"} : (real, real) -> real
-val negate_range = {ocaml: "negate", lem: "integerNegate", c: "neg_int"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n)
-
-val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int"} : int -> int
-
val negate_real = {ocaml: "negate_real", lem: "realNegate", c: "neg_real"} : real -> real
-overload operator - = {sub_range, sub_int, sub_vec, sub_vec_int, sub_real}
+overload operator - = {sub_vec, sub_vec_int, sub_real}
-overload negate = {negate_range, negate_int, negate_real}
-
-val mult_range = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : forall 'n 'm 'o 'p.
- (range('n, 'm), range('o, 'p)) -> range('n * 'o, 'm * 'p)
-
-val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int"} : (int, int) -> int
+overload negate = {negate_real}
val mult_real = {ocaml: "mult_real", lem: "realMult", c: "mult_real"} : (real, real) -> real
-overload operator * = {mult_range, mult_int, mult_real}
+overload operator * = {mult_real}
val Sqrt = {ocaml: "sqrt_real", lem: "realSqrt", c: "sqrt_real"} : real -> real
@@ -279,11 +260,9 @@ val RoundDown = {ocaml: "round_down", lem: "realFloor", c: "round_down"} : real
val RoundUp = {ocaml: "round_up", lem: "realCeiling", c: "round_up"} : real -> int
-val abs_int = "abs_int" : int -> int
-
val abs_real = "abs_real" : real -> real
-overload abs = {abs_atom, abs_int, abs_real}
+overload abs = {abs_atom, abs_real}
val quotient_nat = {ocaml: "quotient", lem: "integerDiv", c: "div_int"} : (nat, nat) -> nat
@@ -299,10 +278,6 @@ overload operator % = {modulus}
val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real"} : int -> real
-val shl_int = "shl_int" : (int, int) -> int
-
-val shr_int = "shr_int" : (int, int) -> int
-
val min_nat = {ocaml: "min_int", lem: "min", c: "max_int"} : (nat, nat) -> nat
val min_int = {ocaml: "min_int", lem: "min", c: "max_int"} : (int, int) -> int
@@ -355,7 +330,6 @@ val slice = "slice" : forall ('n : Int) ('m : Int), 'm >= 0 & 'n >= 0.
val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n)
-val print_int = "print_int" : (string, int) -> unit
val print_bits = "print_bits" : forall 'n. (string, bits('n)) -> unit
val break : unit -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 05:52:22 +0000