From 3f93ecbc6dbdc315b79de4ee69bf6bc6a6420d57 Mon Sep 17 00:00:00 2001 From: Alasdair Armstrong Date: Thu, 3 May 2018 15:30:55 +0100 Subject: Flow typing and l-expression changes for ASL parser 1. Experiment with allowing some flow typing on mutable variables for translating ASL in a more idiomatic way. I realise after updating some of the test cases that this could have some problematic side effects for lem translation, where mutable variables are translated into monadic code. We'd need to ensure that whatever flow typing happens for mutable variables also works for monadic code, including within transformed loops. If this doesn't work out some of these changes may need to be reverted. 2. Make the type inference for l-expressions a bit smarter. Splits the type checking rules for l-expressions into a inference part and a checking part like the other bi-directional rules. Should not be able to type check slightly more l-expresions, such as nested vector slices that may not have checked previously. The l-expression rules for vector patterns should be simpler now, but they are also more strict about bounds checking. Previously the bounds checks were derived from the corresponding operations that would appear on the RHS (i.e. LEXP_vector would get it's check from vector_access). This meant that the l-expression bounds checks could be weakend by weakening the checks on those operations. Now this is no longer possible, there is a -no_lexp_bounds_check option which turns of bounds checking in l-expressions. Currently this is on for the generated ARM spec, but this should only be temporary. 3. Add a LEXP_vector_concat which mirrors P_vector_concat except in l-expressions. Previously there was a hack that overloaded LEXP_tup for this to translate some ASL patterns, but that was fairly ugly. Adapt the rewriter and other parts of the code to handle this. The rewriter for lexp tuple vector assignments is now a rewriter for vector concat assignments. 4. Include a newly generated version of aarch64_no_vector 5. Update the Ocaml test suite to use builtins in lib/ --- aarch64/no_vector/spec.sail | 343 +++++++++++++++++++++----------------------- aarch64/prelude.sail | 38 +---- 2 files changed, 166 insertions(+), 215 deletions(-) (limited to 'aarch64') 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 -$include +$include 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 -- cgit v1.2.3