summaryrefslogtreecommitdiff
path: root/aarch64_small/armV8_A64_lib.sail
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64_small/armV8_A64_lib.sail')
-rw-r--r--aarch64_small/armV8_A64_lib.sail215
1 files changed, 112 insertions, 103 deletions
diff --git a/aarch64_small/armV8_A64_lib.sail b/aarch64_small/armV8_A64_lib.sail
index 9daa94a6..2c707822 100644
--- a/aarch64_small/armV8_A64_lib.sail
+++ b/aarch64_small/armV8_A64_lib.sail
@@ -149,7 +149,7 @@ function AArch64_CheckForWFxTrap(target_el, is_wfe) = {
if target_el == EL1 then trap = ((if is_wfe then SCTLR_EL1.nTWE() else SCTLR_EL1.nTWI()) == 0b0)
else if target_el == EL2 then trap = ((if is_wfe then HCR_EL2.TWE() else HCR_EL2.TWI()) == 0b1)
else if target_el == EL3 then trap = ((if is_wfe then SCR_EL3.TWE() else SCR_EL3.TWI()) == 0b1)
- else {assert(false); ()};
+ else {exit()};
if trap then
@@ -183,8 +183,8 @@ function AArch64_CreateFaultRecord(
write : boolean, extflag : bit, secondstage : boolean, s2fs1walk : boolean) -> FaultRecord = {
struct {
faulttype = faulttype,
- domain = UNKNOWN_VEC() : bits(4),
- debugmoe = UNKNOWN_VEC() : bits(4),
+ domain = UNKNOWN_BITS() : bits(4),
+ debugmoe = UNKNOWN_BITS() : bits(4),
ipaddress = ipaddress,
level = level,
acctype = acctype,
@@ -458,7 +458,7 @@ function wMem_exclusive(write_buffer, address, size, acctype, value) =
function AArch64_ResetGeneralRegisters() -> unit =
{
foreach (i from 0 to 30)
- wX(i) = (UNKNOWN_VEC() : bits(64));
+ wX(i) = (UNKNOWN_BITS() : bits(64));
}
/** FUNCTION:aarch64/functions/registers/AArch64.ResetSIMDFPRegisters */
@@ -466,7 +466,7 @@ function AArch64_ResetGeneralRegisters() -> unit =
function AArch64_ResetSIMDFPRegisters() -> unit =
{
foreach (i from 0 to 31)
- wV(i) = (UNKNOWN_VEC() : bits(128));
+ wV(i) = (UNKNOWN_BITS() : bits(128));
}
/** FUNCTION:aarch64/functions/registers/AArch64.ResetSpecialRegisters */
@@ -474,32 +474,32 @@ function AArch64_ResetSIMDFPRegisters() -> unit =
function AArch64_ResetSpecialRegisters() -> unit =
{
/* AArch64 special registers */
- SP_EL0 = (UNKNOWN_VEC() : bits(64));
- SP_EL1 = (UNKNOWN_VEC() : bits(64));
- SPSR_EL1->bits() = (UNKNOWN_VEC() : bits(32));
- ELR_EL1 = (UNKNOWN_VEC() : bits(64));
+ SP_EL0 = (UNKNOWN_BITS() : bits(64));
+ SP_EL1 = (UNKNOWN_BITS() : bits(64));
+ SPSR_EL1->bits() = (UNKNOWN_BITS() : bits(32));
+ ELR_EL1 = (UNKNOWN_BITS() : bits(64));
if HaveEL(EL2) then {
- SP_EL2 = (UNKNOWN_VEC() : bits(64));
- SPSR_EL2->bits() = (UNKNOWN_VEC() : bits(32));
- ELR_EL2 = (UNKNOWN_VEC() : bits(64));
+ SP_EL2 = (UNKNOWN_BITS() : bits(64));
+ SPSR_EL2->bits() = (UNKNOWN_BITS() : bits(32));
+ ELR_EL2 = (UNKNOWN_BITS() : bits(64));
};
if HaveEL(EL3) then {
- SP_EL3 = (UNKNOWN_VEC() : bits(64));
- SPSR_EL3->bits() = (UNKNOWN_VEC() : bits(32));
- ELR_EL3 = (UNKNOWN_VEC() : bits(64));
+ SP_EL3 = (UNKNOWN_BITS() : bits(64));
+ SPSR_EL3->bits() = (UNKNOWN_BITS() : bits(32));
+ ELR_EL3 = (UNKNOWN_BITS() : bits(64));
};
/* AArch32 special registers that are not architecturally mapped to AArch64 registers */
if HaveAArch32EL(EL1) then {
- SPSR_fiq = (UNKNOWN_VEC() : bits(32));
- SPSR_irq = (UNKNOWN_VEC() : bits(32));
- SPSR_abt = (UNKNOWN_VEC() : bits(32));
- SPSR_und = (UNKNOWN_VEC() : bits(32));
+ SPSR_fiq = (UNKNOWN_BITS() : bits(32));
+ SPSR_irq = (UNKNOWN_BITS() : bits(32));
+ SPSR_abt = (UNKNOWN_BITS() : bits(32));
+ SPSR_und = (UNKNOWN_BITS() : bits(32));
};
/* External debug special registers */
- DLR_EL0 = (UNKNOWN_VEC() : bits(64));
- DSPSR_EL0 = (UNKNOWN_VEC() : bits(32));
+ DLR_EL0 = (UNKNOWN_BITS() : bits(64));
+ DSPSR_EL0 = (UNKNOWN_BITS() : bits(32));
}
/** FUNCTION:aarch64/functions/registers/PC */
@@ -520,7 +520,7 @@ function wSP ((), value) = {
else if pstate_el == EL1 then SP_EL1 = ZeroExtend(value)
else if pstate_el == EL2 then SP_EL2 = ZeroExtend(value)
else if pstate_el == EL3 then SP_EL3 = ZeroExtend(value)
- else assert(false); ();
+ else exit()
}
}
@@ -536,7 +536,7 @@ function rSP(N) = {
else if pstate_el == EL1 then mask(SP_EL1)
else if pstate_el == EL2 then mask(SP_EL2)
else if pstate_el == EL3 then mask(SP_EL3)
- else {assert(false); mask(SP_EL3)}
+ else {exit()}
}
}
@@ -578,22 +578,20 @@ function wVpart(n, part, value) = {
/** FUNCTION:// X[] - assignment form */
-val wX : forall 'N, 'N in {32,64}. (reg_index, bits('N)) -> unit effect {wreg}
function wX(n, value) = {
/*assert n >= 0 && n <= 31;*/
/*assert width IN {32,64};*/
if n != 31 then
- _R[n] = ZeroExtend(value);
+ (* _R[n]) = ZeroExtend(value);
}
/** FUNCTION:// X[] - non-assignment form */
-val rX : forall 'N, 'N in {8,16,32,64}. reg_index -> bits('N) effect {rreg}
-function rX(n) = {
+function rX(N,n) = {
/*assert n >= 0 && n <= 31;*/
/*assert width IN {8,16,32,64};*/
if n != 31 then
- mask(_R[n])
+ mask(reg_deref(_R[n]))
else
Zeros();
}
@@ -601,7 +599,7 @@ function rX(n) = {
/** FUNCTION:bits(64) ELR[bits(2) el] */
function rELR(el : bits(2)) -> bits(64) = {
- r = 0 : bits(64); /* ARM: uninitialized */
+ r = Zeros() : bits(64); /* ARM: uninitialized */
if el == EL1 then r = ELR_EL1
else if el == EL2 then r = ELR_EL2
else if el == EL3 then r = ELR_EL3
@@ -611,42 +609,42 @@ function rELR(el : bits(2)) -> bits(64) = {
/** FUNCTION:bits(64) ELR[] */
-function rELR'() -> bits(64) =
-{
- assert (PSTATE_EL != EL0, None);
- rELR(PSTATE_EL);
+function rELR'() -> bits(64) = {
+ let pstate_el = PSTATE_EL();
+ assert (pstate_el != EL0);
+ rELR(pstate_el);
}
/** FUNCTION:SCTLRType SCTLR[bits(2) regime] */
-val SCTLR : bits(2) -> SCTLR_type effect {rreg}
+/* FIXME: this reads the whole register. Do we want that? */
+val SCTLR : bits(2) -> SCTLR_type effect {escape, rreg}
function SCTLR (regime) = {
if regime == EL1 then SCTLR_EL1
else if regime == EL2 then SCTLR_EL2
else if regime == EL3 then SCTLR_EL3
- else {assert(false,Some("SCTLR_type unreachable")); SCTLR_EL1} /* ARM: Unreachabe() */
+ else Unreachable("SCTLR_type unreachable") /* ARM: Unreachabe() */
}
/** FUNCTION:SCTLRType SCTLR[] */
-val SCTLR' : unit -> SCTLR_type effect{rreg}
function SCTLR' () = SCTLR(S1TranslationRegime())
/** FUNCTION:aarch64/functions/system/AArch64.CheckUnallocatedSystemAccess */
/* return true if the access is not allowed */
function AArch64_CheckUnallocatedSystemAccess (op0 : bits(2), op1 : bits(3), crn : bits(4),
- crm : bits(4), op2 : bits(3), read : bit) -> boolean =
-{
+ crm : bits(4), op2 : bits(3), read : bit) -> boolean = {
match (op0,op1,crn,crm,op2, read) {
- (0b00,0b000,0b0100,_,0b101, _) => PSTATE_EL < EL1 /* SPSel */,
+ (0b00,0b000,0b0100,_,0b101, _) => UInt(PSTATE_EL()) < UInt(EL1) /* CP: added conversion to uint */ /* SPSel */,
(0b00,0b011,0b0100,_,0b110, _) => false, /* DAIFSet */ /* TODO: EL0 Config-RW ??? */
(0b00,0b011,0b0100,_,0b111, _) => false, /* DAIFClr */ /* TODO: EL0 Config-RW ??? */
/* follow the "Usage constraints" of each register */
(0b11,0b011,0b0100,0b0010,0b000, _) => false, /* NZCV */
- (0b11,0b011,0b0100,0b0010,0b001, _) => false /* DAIF */ /* TODO: EL0 Config-RW ??? */
-/* (0b11,0b000,0b0001,0b0000,0b001, _) => PSTATE_EL < EL1 /* ACTLR_EL1 */ */
+ (0b11,0b011,0b0100,0b0010,0b001, _) => false, /* DAIF */ /* TODO: EL0 Config-RW ??? */
+/* (0b11,0b000,0b0001,0b0000,0b001, _) => PSTATE_EL < EL1 (* ACTLR_EL1 *) */
+ _ => exit()
}
}
@@ -659,7 +657,7 @@ function CheckSystemAccess (op0 : bits(2), op1 : bits(3), crn : bits(4), crm : b
/*level, security state and configuration, based on the opcode's encoding.*/
unallocated : boolean = false;
need_secure : boolean = false;
- min_EL : bits(2) = 0; /* ARM: uninitialized */
+ min_EL : bits(2) = 0b00; /* ARM: uninitialized */
/*Check for traps by HCR_EL2.TIDCP*/
/* TODO: uncomment when implementing traps
@@ -691,7 +689,7 @@ function CheckSystemAccess (op0 : bits(2), op1 : bits(3), crn : bits(4), crm : b
need_secure = true;
}
};
- if PSTATE_EL < min_EL then /* ARM: UInt */
+ if UInt(PSTATE_EL()) < UInt(min_EL) then /* ARM: UInt */ /* CP: added Uint */
UnallocatedEncoding()
else if need_secure & ~(IsSecure()) then
UnallocatedEncoding()
@@ -714,27 +712,28 @@ function CheckSystemAccess (op0 : bits(2), op1 : bits(3), crn : bits(4), crm : b
/** FUNCTION:aarch64/functions/system/SysOp_R */
-val SysOp_R : (uinteger, uinteger, uinteger, uinteger, uinteger) -> bits(64)
+val SysOp_R : (uinteger, uinteger, uinteger, uinteger, uinteger) -> bits(64) effect {escape}
function SysOp_R(op0, op1, crn, crm, op2) = {
not_implemented("SysOp_R");
- 0;
+ Zeros();
}
/** FUNCTION:aarch64/functions/system/SysOp_W */
-val SysOp_W : (uinteger, uinteger, uinteger, uinteger, uinteger, bits(64)) -> unit
-function unit SysOp_W(op0, op1, crn, crm, op2, _val) = {
+val SysOp_W : (uinteger, uinteger, uinteger, uinteger, uinteger, bits(64)) -> unit effect {escape}
+function SysOp_W(op0, op1, crn, crm, op2, _val) = {
not_implemented("SysOp_W");
}
/** FUNCTION:bits(64) System_Get(integer op0, integer op1, integer crn, integer crm, integer op2); */
-val System_Get : (uinteger, uinteger, uinteger, uinteger, uinteger) -> bits(64)
+val System_Get : (uinteger, uinteger, uinteger, uinteger, uinteger) -> bits(64) effect{escape,rreg}
function System_Get(op0, op1, crn, crm, op2) -> bits(64) = {
match (op0,op1,crn,crm,op2) {
- (3,3,4,2,0) => ZeroExtend(NZCV),
- (3,3,4,2,1) => ZeroExtend(DAIF),
- (3, 3, 13, 0, 2) => TPIDR_EL0
+ (3,3,4,2,0) => ZeroExtend(NZCV.bits()),
+ (3,3,4,2,1) => ZeroExtend(DAIF.bits()),
+ (3, 3, 13, 0, 2) => TPIDR_EL0,
+ _ => exit()
/* TODO FIXME: higher EL TPIDRs */
/* (3,0,1,0,1) => ZeroExtend(ACTLR_EL1) */
@@ -743,12 +742,13 @@ function System_Get(op0, op1, crn, crm, op2) -> bits(64) = {
/** FUNCTION:System_Put(integer op0, integer op1, integer crn, integer crm, integer op2, bits(64) val); */
-val System_Put : (uinteger, uinteger, uinteger, uinteger, uinteger, bits(64)) -> unit effect {wreg}
+val System_Put : (uinteger, uinteger, uinteger, uinteger, uinteger, bits(64)) -> unit effect {wreg,escape}
function System_Put(op0, op1, crn, crm, op2, _val) = {
match (op0,op1,crn,crm,op2) {
- (3,3,4,2,0) => NZCV = _val[31..0],
- (3,3,4,2,1) => DAIF = _val[31..0],
- (3,3,13,0,2) => TPIDR_EL0 = _val[63..0]
+ (3,3,4,2,0) => NZCV->bits() = _val[31..0],
+ (3,3,4,2,1) => DAIF->bits() = _val[31..0],
+ (3,3,13,0,2) => TPIDR_EL0 = _val[63..0],
+ _ => exit()
/* TODO FIXME: higher EL TPIDRs */
/* (3,0,1,0,1) => ACTLR_EL1 = _val[31..0] */
@@ -757,14 +757,14 @@ function System_Put(op0, op1, crn, crm, op2, _val) = {
/** FUNCTION:aarch64/instrs/branch/eret/AArch64.ExceptionReturn */
-function unit AArch64_ExceptionReturn(new_pc : bits(64), spsr : bits(32)) = {
+function AArch64_ExceptionReturn(new_pc : bits(64), spsr : bits(32)) -> unit = {
not_implemented("AArch64_ExceptionReturn");
}
/** ENUMERATE:aarch64/instrs/countop/CountOp */
/** FUNCTION:ExtendType DecodeRegExtend(bits(3) op) */
-function ExtendType DecodeRegExtend (op : bits(3)) = {
+function DecodeRegExtend (op : bits(3)) -> ExtendType = {
match op {
0b000 => ExtendType_UXTB,
0b001 => ExtendType_UXTH,
@@ -780,11 +780,10 @@ function ExtendType DecodeRegExtend (op : bits(3)) = {
/** FUNCTION:aarch64/instrs/extendreg/ExtendReg */
val ExtendReg : forall 'N 'S, 'N in {8,16,32,64} & 'S >= 0 & 'S <= 4.
- (implicit('N), reg_index, ExtendType, atom('S)) -> bits('N) effect {rreg}
-function ExtendReg (_reg, etype, shift) =
-{
+ (implicit('N), reg_index, ExtendType, atom('S)) -> bits('N) effect {rreg,escape}
+function ExtendReg (N, _reg, etype, shift) = {
/*assert( shift >= 0 & shift <= 4 );*/
- /* _val */ rX : bits('N) = (_reg);
+ _val : bits('N) = rX(_reg);
_unsigned : boolean = false;
len : uinteger = 0;
@@ -799,7 +798,10 @@ function ExtendReg (_reg, etype, shift) =
ExtendType_UXTX => { _unsigned = true; len = 64}
};
- len = uMin(len, length(_val) - shift);
+ let len = uMin(len, length(_val) - shift);
+ assert( len >= 1 & 'S + len < 'N);
+ let a = (_val[(len - 1)..0]);
+ /* Zeros() */
Extend((_val[(len - 1)..0]) @ (Zeros() : bits('S)), _unsigned)
}
@@ -807,21 +809,21 @@ function ExtendReg (_reg, etype, shift) =
/** ENUMERATE:aarch64/instrs/integer/arithmetic/rev/revop/RevOp */
/** FUNCTION:(bits(M), bits(M)) DecodeBitMasks (bit immN, bits(6) imms, bits(6) immr, boolean immediate) */
-val DecodeBitMasks : forall 'M 'E, 'M >= 0 & 'E in {2,4,8,16,32,64}. (implicit('M),bit,bits(6),bits(6),boolean) -> (bits('M),bits('M)) effect {escape}
-function DecodeBitMasks(immN, imms, immr, immediate) = {
- let M = (length(0 : bits('M))) in {
-/* ARM: (bits('M)) tmask = 0; /* ARM: uninitialized */ */
-/* ARM: (bits('M)) wmask = 0; /* ARM: uninitialized */ */
- levels : bits(6) = 0; /* ARM: uninitialized */
+val DecodeBitMasks : forall 'M 'E, 'M >= 0 & 'E in {2,4,8,16,32,64}. (implicit('M), bit, bits(6), bits(6), boolean) -> (bits('M), bits('M)) effect {escape}
+function DecodeBitMasks(M : atom('M), immN : bit, imms : bits(6), immr : bits(6), immediate : boolean) = {
+ /* let M = (length((bit['M]) 0)) in { */
+ /* ARM: (bit['M]) tmask := 0; (* ARM: uninitialized *) */
+ /* ARM: (bit['M]) wmask := 0; (* ARM: uninitialized *) */
+ levels : bits(6) = Zeros(); /* ARM: uninitialized */
/* Compute log2 of element size */
/* 2^len must be in range [2, 'M] */
- len : range(0,6) = match HighestSetBit([immN]@(NOT(imms))) {
- None => { assert (false,Some("DecodeBitMasks: HighestSetBit returned None")); 0; },
- (Some(c)) => c
+ let len : range(0,6) = match HighestSetBit([immN]@(~(imms))) {
+ None() => { assert (false, "DecodeBitMasks: HighestSetBit returned None"); 0; },
+ Some(c) => c
};
- if len < 1 then ReservedValue();
- assert((M >= lsl(1, len)),None);
+ if len < 1 then {ReservedValue(); exit()} else {
+ assert(M >= lsl(1, len));
/* Determine S, R and S - R parameters */
levels = ZeroExtend(0b1 ^^ len);
@@ -831,28 +833,35 @@ function DecodeBitMasks(immN, imms, immr, immediate) = {
if immediate & ((imms & levels) == levels) then
ReservedValue();
- S : bits(6) = (imms & levels);
- R : bits(6) = (immr & levels);
- diff : bits(6) = S - R; /* 6-bit subtract with borrow */
-
- esize : atom('E) = lsl(1, len);
- d : bits(6) = diff[(len - 1)..0];
- welem : bits('E) = ZeroExtend(0b1 ^^ (S + 1));
- telem : bits('E) = ZeroExtend(0b1 ^^ (d + 1));
- wmask = Replicate(ROR(welem, R));
- tmask = Replicate(telem);
+ let S = UInt (imms & levels);
+ let R = UInt (immr & levels);
+ let diff : bits(6) = to_bits(S - R); /* 6-bit subtract with borrow */
+
+ let esize /* : atom('E) */ = lsl(1, len);
+ let d /* : bits(6) */ = UInt (diff[(len - 1)..0]);
+ assert(esize >= S+1); /* CP: adding this assertion to make typecheck */
+ welem /* : bits('E) */ = ZeroExtend(esize,Ones(S + 1));
+ telem /* : bits('E) */ = ZeroExtend(esize,Ones(d + 1));
+ wmask = Replicate(M,ROR(welem, R));
+ tmask = Replicate(M,telem);
(wmask, tmask);
}}
/** ENUMERATE:aarch64/instrs/integer/ins-ext/insert/movewide/movewideop/MoveWideOp */
/** FUNCTION:ShiftType DecodeShift(bits(2) op) */
-function ShiftType DecodeShift(op : bits(2)) = op : range(0,4)
+function DecodeShift(op : bits(2)) -> ShiftType =
+ match op {
+ 0b00 => ShiftType_LSL,
+ 0b01 => ShiftType_LSR,
+ 0b10 => ShiftType_ASR,
+ 0b11 => ShiftType_ROR
+ }
/** FUNCTION:bits(N) ShiftReg(integer reg, ShiftType type, integer amount) */
-val ShiftReg : forall 'N, 'N >= 0. (implicit('N), reg_index, ShiftType, nat) -> bits('N) effect {rreg}
-function ShiftReg(_reg, stype, amount) = {
+val ShiftReg : forall 'N, 'N in {8,16,32,64}. (implicit('N), reg_index, ShiftType, nat) -> bits('N) effect {escape, rreg}
+function ShiftReg(N,_reg, stype, amount) = {
result : bits('N) = rX(_reg);
match stype {
ShiftType_LSL => result = LSL(result, amount),
@@ -868,10 +877,10 @@ function ShiftReg(_reg, stype, amount) = {
/** ENUMERATE:aarch64/instrs/memory/memop/MemOp */
/** FUNCTION:aarch64/instrs/memory/prefetch/Prefetch */
-function unit Prefetch(address : bits(64), prfop : bits(5)) = {
- hint : PrefetchHint = 0;
+function Prefetch(address : bits(64), prfop : bits(5)) -> unit = {
+ hint : PrefetchHint = Prefetch_READ;
target : uinteger = 0;
- stream : boolean = 0;
+ stream : boolean = bitzero;
returnv : bool = false;
match prfop[4..3] {
@@ -881,8 +890,8 @@ function unit Prefetch(address : bits(64), prfop : bits(5)) = {
0b11 => returnv = true /* unallocated hint */
};
if ~(returnv) then {
- target = prfop[2..1]; /* target cache level */
- stream = (prfop[0] != 0); /* streaming (non-temporal) */
+ target = UInt(prfop[2..1]); /* target cache level */
+ stream = (prfop[0] != bitzero); /* streaming (non-temporal) */
Hint_Prefetch(address, hint, target, stream);
}}
@@ -891,11 +900,11 @@ function unit Prefetch(address : bits(64), prfop : bits(5)) = {
/** ENUMERATE:aarch64/instrs/system/register/cpsr/pstatefield/PSTATEField */
/** FUNCTION:aarch64/translation/faults/AArch64.AlignmentFault */
-function FaultRecord AArch64_AlignmentFault(acctype : AccType, iswrite : boolean, secondstage : boolean) = {
- ipaddress : bits(48) = UNKNOWN;
+function AArch64_AlignmentFault(acctype : AccType, iswrite : boolean, secondstage : boolean) -> FaultRecord = {
+ ipaddress : bits(48) = UNKNOWN_BITS();
level : uinteger = UNKNOWN;
- extflag : bit = UNKNOWN;
- s2fs1walk : boolean = UNKNOWN;
+ extflag : bit = UNKNOWN_BIT;
+ s2fs1walk : boolean = UNKNOWN_BIT;
AArch64_CreateFaultRecord(Fault_Alignment, ipaddress, level, acctype, iswrite,
extflag, secondstage, s2fs1walk);
@@ -903,12 +912,12 @@ function FaultRecord AArch64_AlignmentFault(acctype : AccType, iswrite : boolean
/** FUNCTION:aarch64/translation/faults/AArch64.NoFault */
-function FaultRecord AArch64_NoFault() = {
- ipaddress : bits(48) = UNKNOWN;
+function AArch64_NoFault() -> FaultRecord = {
+ ipaddress : bits(48) = UNKNOWN_BITS();
level : uinteger = UNKNOWN;
acctype : AccType = AccType_NORMAL;
- iswrite : boolean = UNKNOWN;
- extflag : bit = UNKNOWN;
+ iswrite : boolean = UNKNOWN_BIT;
+ extflag : bit = UNKNOWN_BIT;
secondstage : boolean = false;
s2fs1walk : boolean = false;
@@ -922,10 +931,10 @@ function AArch64_TranslateAddress
(vaddress : bits(64), acctype : AccType, iswrite : boolean,
wasaligned : boolean, size : uinteger) -> AddressDescriptor = {
info("Translation is not implemented, return same address as the virtual (no fault, normal, shareable, non-secure).");
- result : AddressDescriptor = {
- fault = AArch64_NoFault();
- memattrs = {MA_type = MemType_Normal; shareable = true};
- paddress = {physicaladdress = vaddress; NS = 1};
+ result : AddressDescriptor = struct {
+ fault = AArch64_NoFault(),
+ memattrs = struct {MA_type = MemType_Normal, shareable = true},
+ paddress = struct {physicaladdress = vaddress, NS = bitone}
};
/* ARM: uncomment when implementing TLB and delete the code above
(AddressDescriptor) result = AArch64_FullTranslate(vaddress, acctype, iswrite, wasaligned, size);