summaryrefslogtreecommitdiff
path: root/aarch64_small
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64_small')
-rw-r--r--aarch64_small/armV8.h.sail24
-rw-r--r--aarch64_small/armV8.sail56
-rw-r--r--aarch64_small/armV8_A64_lib.sail215
-rw-r--r--aarch64_small/armV8_A64_sys_regs.sail6
-rw-r--r--aarch64_small/armV8_common_lib.sail30
-rw-r--r--aarch64_small/armV8_lib.h.sail2
-rw-r--r--aarch64_small/armV8_pstate.sail4
-rw-r--r--aarch64_small/prelude.sail31
8 files changed, 212 insertions, 156 deletions
diff --git a/aarch64_small/armV8.h.sail b/aarch64_small/armV8.h.sail
index dc28ffde..03f390bc 100644
--- a/aarch64_small/armV8.h.sail
+++ b/aarch64_small/armV8.h.sail
@@ -137,8 +137,8 @@ let _R : vector(31,dec,register(bits(64))) =
/* val reg_index : reg_size -> UInt_reg effect pure */
/* function reg_index x = (x : (reg_index)) */
-val reg_index : reg_size -> reg_index
-function reg_index x = unsigned(x)
+val UInt_reg : reg_size -> reg_index
+function UInt_reg x = unsigned(x)
/* SIMD and floating-point registers */
@@ -223,19 +223,26 @@ function lsl (n, m) = n * (2 ^ m)
/* not_implemented is used to indicate something WE did not implement */
val not_implemented : forall ('a : Type). string -> 'a effect { escape }
-function not_implemented message = exit () /* TODO message */
+function not_implemented(message) = {
+ print(message);
+ exit ()
+}
/* not_implemented_extern is used to indicate something ARM did not define
and we did not define yet either. Those functions used to be declared as
external but undefined there. */
/* val not_implemented_extern : forall 'a. string -> 'a effect { escape } */
val not_implemented_extern : forall ('a : Type). string -> 'a effect { escape }
-function not_implemented_extern (message) =
- exit () /* message; TODO */
+function not_implemented_extern (message) = {
+ print(message);
+ exit ()
+}
/* info is used to convey information to the user */
val info : string -> unit effect pure
-function info(message) = ()
+function info(message) = {
+ print(message)
+}
struct IMPLEMENTATION_DEFINED_type = {
HaveCRCExt : boolean,
@@ -259,7 +266,8 @@ let IMPLEMENTATION_DEFINED : IMPLEMENTATION_DEFINED_type = struct {
/* FIXME: ask Kathy what should we do with this */
let UNKNOWN = 0
-val UNKNOWN_VEC: forall 'N, 'N >= 0. implicit('N) -> bits('N)
-function UNKNOWN_VEC(N) = (replicate_bits(0b0, 'N)) : bits('N)
+val UNKNOWN_BITS: forall 'N, 'N >= 0. implicit('N) -> bits('N)
+function UNKNOWN_BITS(N) = (replicate_bits(0b0, 'N)) : bits('N)
+let UNKNOWN_BIT = bitzero
/* external */ val speculate_exclusive_success : unit -> bool effect {exmem}
diff --git a/aarch64_small/armV8.sail b/aarch64_small/armV8.sail
index a3082261..e4b74740 100644
--- a/aarch64_small/armV8.sail
+++ b/aarch64_small/armV8.sail
@@ -112,16 +112,16 @@ function decodeTMStart (Rt) = {
function clause execute (TMStart(t)) = {
nesting : bits(8) = TxNestingLevel;
- if nesting <_u TXIDR_EL0.DEPTH then {
+ if nesting <_u TXIDR_EL0.DEPTH() then {
TxNestingLevel = nesting + 1;
- status : bits(64) = 0;
- if nesting == 0 then
- status = TMStartEffect; /* fake effect */
+ status : bits(64) = Zeros();
+ if nesting == 0b00000000 then
+ status = TMStartEffect.bits(); /* fake effect */
wX(t) = status;
} else {
- status : bits(64) = 0;
- status[10] = 1; /* set the NEST bit */
- TMAbortEffect = status; /* fake effect */
+ status : bits(64) = Zeros();
+ status[10] = bitone; /* set the NEST bit */
+ TMAbortEffect->bits() = status; /* fake effect */
}
}
@@ -130,17 +130,17 @@ function clause execute (TMStart(t)) = {
/* TCOMMIT - dummy decoding */
val decodeTMCommit : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
unit -> option(ast('R,'D)) effect pure
-function decodeTMCommit () = {
- Some(TMCommit);
-}
+function decodeTMCommit () =
+ Some(TMCommit())
+
/* transactional memory, not part of the official spec */
-function clause execute (TMCommit) = {
+function clause execute (TMCommit()) = {
nesting : bits(8) = TxNestingLevel;
- if nesting == 1 then
+ if nesting == 0b00000001 then
TMCommitEffect() /* fake effect */
- else if nesting == 0 then
+ else if nesting == 0b00000000 then
AArch64_UndefinedFault();
TxNestingLevel = nesting - 1;
@@ -149,13 +149,13 @@ function clause execute (TMCommit) = {
/* TTEST - dummy decoding */
val decodeTMTest : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
unit -> option(ast('R,'D)) effect pure
-function decodeTMTest () = {
- Some(TMTest);
-}
+function decodeTMTest () =
+ Some(TMTest())
+
/* transactional memory, not part of the official spec */
-function clause execute (TMTest) = {
- if TxNestingLevel > 0 then
+function clause execute (TMTest()) = {
+ if 0b00000000 <_u TxNestingLevel then
wPSTATE_NZCV() = 0b0000
else
wPSTATE_NZCV() = 0b0100
@@ -170,23 +170,25 @@ function decodeTMAbort ([R] @ (imm5 : bits(5))) = {
/* transactional memory, not part of the official spec */
function clause execute (TMAbort(retry,reason)) = {
- if TxNestingLevel > 0 then {
- status : bits(64) = 0;
+ if 0b00000000 <_u TxNestingLevel then {
+ status : bits(64) = Zeros();
status[4..0] = reason; /* REASON */
status[8] = retry; /* RTRY */
- status[9] = 1; /* ABRT */
- TMAbortEffect = status; /* fake effect */
+ status[9] = bitone; /* ABRT */
+ TMAbortEffect->bits() = status; /* fake effect */
};
}
/* CBNZ */
/* CBZ */
-val decodeCompareBranchImmediate : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}.
- bits(32) -> option(ast('R,'D)) effect pure
-function decodeCompareBranchImmediate ([sf]@0b011010@[op]@(imm19:bits(19))@Rt) = {
+/* val decodeCompareBranchImmediate : forall 'R 'D, 'R in {32,64} & 'D in {8,16,32,64}. */
+/* bits(32) -> option(ast('R,'D)) effect pure */
+val decodeCompareBranchImmediate :
+ bits(32) -> {'R 'D, 'R in {32, 64} & 'D in {8,16,32,64}. option(ast('R,'D))} effect pure
+function decodeCompareBranchImmediate ([sf]@0b011010@[op]@(imm19:bits(19))@(Rt:bits(5))) = {
t : reg_index = UInt_reg(Rt);
- datasize : atom('R) = if sf == 1 then 64 else 32;
- iszero : boolean = (op == 0);
+ datasize : {|32,64|} = if sf == bitone then 64 else 32;
+ iszero : boolean = (op == bitzero);
offset : bits(64) = SignExtend(imm19@0b00);
Some(CompareAndBranch(t,datasize,iszero,offset));
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);
diff --git a/aarch64_small/armV8_A64_sys_regs.sail b/aarch64_small/armV8_A64_sys_regs.sail
index b051c87d..36f7c3f6 100644
--- a/aarch64_small/armV8_A64_sys_regs.sail
+++ b/aarch64_small/armV8_A64_sys_regs.sail
@@ -173,6 +173,12 @@ bitfield SCTLR_type : bits(32) =
register SCTLR_EL2 : SCTLR_type /* System Control Register (EL2) */
register SCTLR_EL3 : SCTLR_type /* System Control Register (EL3) */
+
+
+/* CP: added coercion from SCTLR_EL1_type to SCTLR_type for the SCTLR function */
+val cast SCTLR_EL1_type_to_SCTLR_type : SCTLR_EL1_type -> SCTLR_type
+
+
bitfield TCR_EL1_type : bits(64) =
{
/*RES0 : 63..39,*/
diff --git a/aarch64_small/armV8_common_lib.sail b/aarch64_small/armV8_common_lib.sail
index fa7e48d3..5e8fc63c 100644
--- a/aarch64_small/armV8_common_lib.sail
+++ b/aarch64_small/armV8_common_lib.sail
@@ -216,7 +216,7 @@ function CountLeadingZeroBits(x) =
}
/** FUNCTION:bits(N) Extend(bits(M) x, integer N, boolean unsigned) */
-val Extend : forall 'N 'M, 1 <= 'M & 'M < 'N. (atom('N),bits('M),bit) -> bits('N) effect {escape}
+val Extend : forall 'N 'M, 1 <= 'M & 'M < 'N. (implicit('N),bits('M),bit) -> bits('N) effect {escape}
function Extend (n, x, _unsigned) =
if _unsigned then ZeroExtend(n,x) else SignExtend(n,x)
@@ -314,11 +314,11 @@ function LSR_C(x, shift) = {
/** FUNCTION:integer Min(integer a, integer b) */
-val Min : (integer, integer) -> integer
+val Min : forall 'M 'N.(atom('M), atom('N)) -> min('M,'N)
function Min (a,b) =
if a <= b then a else b
-val uMin : (uinteger, uinteger) -> uinteger
+val uMin : forall 'M 'N, 'M >= 0 & 'N >= 0. (atom('M), atom('N)) -> min('M,'N)
function uMin (a,b) =
if a <= b then a else b
@@ -520,7 +520,7 @@ function AddWithCarry (x, y, carry_in) = {
/** TYPE:shared/functions/memory/AddressDescriptor */
/** FUNCTION:boolean BigEndian() */
-val BigEndian : unit -> boolean effect {rreg}
+val BigEndian : unit -> boolean effect {rreg,escape}
function BigEndian() = {
/* bigend : boolean = bitzero; /\* ARM: uninitialized *\/ */
if UsingAArch32() then
@@ -661,9 +661,9 @@ function flush_read_buffer(read_buffer, size) =
AccType_STREAM => value = rMem_STREAM (read_buffer.address, size),
AccType_UNPRIV => value = rMem_NORMAL (read_buffer.address, size),
AccType_ORDERED => value = rMem_ORDERED(read_buffer.address, size),
- AccType_ATOMIC => assert(false,"Reached AccType_ATOMIC: unreachable when address values are known"),
+ AccType_ATOMIC => error("Reached AccType_ATOMIC: unreachable when address values are known"),
/* (*old code*) value = rMem_NORMAL (read_buffer.address, size) (* the second read of 64-bit LDXP *)*/
- _ => assert(false)
+ _ => exit()
}
};
@@ -804,7 +804,7 @@ function BranchTo(target, branch_type) = {
if TCR_EL3.TBI() == 0b1 then
target'[63..56] = 0b00000000;
}
- else assert(false)
+ else exit()
};
_PC = target';
};
@@ -928,7 +928,7 @@ function HaveEL(el : bits(2)) -> boolean = {
if el == EL2 then IMPLEMENTATION_DEFINED.HaveEL2
else if el == EL3 then IMPLEMENTATION_DEFINED.HaveEL3
- else {assert (false); false};
+ else exit();
};
}
@@ -996,9 +996,17 @@ function SendEvent() -> unit =
/** FUNCTION:shared/functions/system/Unreachable */
-function Unreachable() -> unit = {
- assert (false,"Unreachable reached");
-}
+/* CP: adding two variants, one that takes a string argument, the other one doesn't */
+val Unreachable_no_message : forall ('a : Type) . unit -> 'a effect{escape}
+function Unreachable_no_message() =
+ error("Unreachable reached")
+
+val Unreachable_message : forall ('a : Type) . string -> 'a effect{escape}
+function Unreachable_message(message) =
+ error(message)
+
+overload Unreachable = {Unreachable_no_message, Unreachable_message}
+
/** FUNCTION:shared/functions/system/UsingAArch32 */
diff --git a/aarch64_small/armV8_lib.h.sail b/aarch64_small/armV8_lib.h.sail
index 6f09ad13..662fc1f4 100644
--- a/aarch64_small/armV8_lib.h.sail
+++ b/aarch64_small/armV8_lib.h.sail
@@ -217,7 +217,7 @@ val rX : forall 'N, 'N in {8,16,32,64}. (implicit('N),reg_index) -> bits('N) eff
val wV : forall 'N, 'N in {8,16,32,64,128}. (SIMD_index,bits('N)) -> unit effect {wreg}
val rV : forall 'N, 'N in {8,16,32,64,128}. (implicit('N),SIMD_index) -> bits('N) effect {rreg}
val rVpart : forall 'N, 'N in {8,16,32,64,128}. (implicit('N),SIMD_index,range(0,1)) -> bits('N) effect {rreg,escape}
-val SCTLR' : unit -> SCTLR_type effect {rreg}
+val SCTLR' : unit -> SCTLR_type effect {rreg,escape}
val AArch64_UndefinedFault : unit -> unit effect {escape}
val AArch64_TranslateAddress : (bits(64),AccType,boolean,boolean,uinteger) -> AddressDescriptor effect pure
val AArch64_WFxTrap : (bits(2),boolean) -> unit effect {escape}
diff --git a/aarch64_small/armV8_pstate.sail b/aarch64_small/armV8_pstate.sail
index 38932472..65b8f2bd 100644
--- a/aarch64_small/armV8_pstate.sail
+++ b/aarch64_small/armV8_pstate.sail
@@ -119,8 +119,8 @@ register PSTATE_M : bits(5) /* Mode field [AArc
/* this is a convenient way to do "PSTATE.<N,Z,C,V> = nzcv;" */
-val wPSTATE_NZCV : (unit, bits(4)) -> unit effect {wreg}
-function wPSTATE_NZCV((), [n,z,c,v]) = {
+val wPSTATE_NZCV : (bits(4)) -> unit effect {wreg}
+function wPSTATE_NZCV([n,z,c,v]) = {
PSTATE_N() = [n];
PSTATE_Z() = [z];
PSTATE_C() = [c];
diff --git a/aarch64_small/prelude.sail b/aarch64_small/prelude.sail
index 2516f32c..a7bc2388 100644
--- a/aarch64_small/prelude.sail
+++ b/aarch64_small/prelude.sail
@@ -78,16 +78,13 @@ function cast_bit_bool (b) =
val and_bits = {c:"and_bits", _: "and_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
overload operator & = {and_bool, and_bits}
val or_bits = {c:"or_bits", _: "or_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
-
overload operator | = {or_bool, or_bits}
val not_vec = {c:"not_bits", _:"not_vec"} : forall 'n. bits('n) -> bits('n)
-
overload ~ = {not_bool, not_vec}
val eq_anything = {ocaml: "(fun (x, y) -> x = y)", lem: "eq", coq: "generic_eq", _:"eq_anything"} : forall ('a : Type). ('a, 'a) -> bool
@@ -103,6 +100,22 @@ function neq_anything (x, y) = not_bool(x == y)
overload operator != = {neq_atom, neq_int, neq_vec, neq_anything}
+val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm.
+ (int('n), int('m)) -> int('n + 'm)
+val add_vec = {c: "add_bits", _: "add_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val add_vec_int = {c: "add_bits_int", _: "add_vec_int"} : forall 'n. (bits('n), int) -> bits('n)
+overload operator + = {add_int, add_vec, add_vec_int}
+
+val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm.
+ (int('n), int('m)) -> int('n - 'm)
+val sub_nat = {ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)",
+ lem: "integerMinus", coq: "sub_nat", c: "sub_nat"}
+ : (nat, nat) -> nat
+val sub_vec = {c: "sub_bits", _: "sub_vec"} : forall 'n. (bits('n), bits('n)) -> bits('n)
+val sub_vec_int = {c: "sub_bits_int", _: "sub_vec_int"} : forall 'n. (bits('n), int) -> bits('n)
+overload operator - = {sub_int, sub_vec, sub_vec_int}
+
+
/* val reg_index : reg_size -> reg_index */
/* function reg_index x = unsigned(x) */
@@ -141,4 +154,14 @@ val mod = {
coq: "Z.rem"
} : forall 'M 'N. (atom('M), atom('N)) -> {'O, 0 <= 'O & 'O < N . atom('O)}
-/* overload operator % = {mod_int} */ \ No newline at end of file
+/* overload operator % = {mod_int} */
+
+val print = "print_endline" : string -> unit
+
+val error : forall ('a : Type). string -> 'a effect{escape}
+function error(message) = {
+ print(message);
+ exit()
+}
+
+type min ('M : Int, 'N : Int) = {'O, ('O == 'M | 'O == 'N) & 'O <= 'M & 'O <= 'N. atom('O)}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 11:05:23 +0000