diff options
Diffstat (limited to 'arm/armv8_lib.h.sail')
| -rw-r--r-- | arm/armv8_lib.h.sail | 240 |
1 files changed, 240 insertions, 0 deletions
diff --git a/arm/armv8_lib.h.sail b/arm/armv8_lib.h.sail new file mode 100644 index 00000000..e8e979c8 --- /dev/null +++ b/arm/armv8_lib.h.sail @@ -0,0 +1,240 @@ +(*========================================================================*) +(* *) +(* Copyright (c) 2015-2016 Shaked Flur *) +(* Copyright (c) 2015-2016 Kathyrn Gray *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(*========================================================================*) + +(*** common lib ***) + +typedef AccType = + enumerate {AccType_NORMAL; AccType_VEC; (* Normal loads and stores *) + AccType_STREAM; AccType_VECSTREAM; (* Streaming loads and stores *) + AccType_ATOMIC; (* Atomic loads and stores *) + AccType_ORDERED; (* Load-Acquire and Store-Release *) + AccType_UNPRIV; (* Load and store unprivileged *) + AccType_IFETCH; (* Instruction fetch *) + AccType_PTW; (* Page table walk *) + (* Other operations*) + AccType_DC; (* Data cache maintenance *) + AccType_IC; (* Instruction cache maintenance *) + AccType_AT} (* Address translation *) + +typedef MBReqDomain = + enumerate {MBReqDomain_Nonshareable; MBReqDomain_InnerShareable; + MBReqDomain_OuterShareable; MBReqDomain_FullSystem} + +typedef MBReqTypes = + enumerate {MBReqTypes_Reads; MBReqTypes_Writes; MBReqTypes_All} + + +typedef BranchType = + enumerate {BranchType_CALL; BranchType_ERET; BranchType_DBGEXIT; + BranchType_RET; BranchType_JMP; BranchType_EXCEPTION; + BranchType_UNKNOWN} + +typedef MoveWideOp = + enumerate {MoveWideOp_N; MoveWideOp_Z; MoveWideOp_K} + +(* shared/functions/system/Mode_Bits *) +let M32_User = 0b10000 +let M32_FIQ = 0b10001 +let M32_IRQ = 0b10010 +let M32_Svc = 0b10011 +let M32_Monitor = 0b10110 +let M32_Abort = 0b10111 +let M32_Hyp = 0b11010 +let M32_Undef = 0b11011 +let M32_System = 0b11111 + +(* shared/functions/system/EL0 *) +let EL3 = 0b11 +let EL2 = 0b10 +let EL1 = 0b01 +let EL0 = 0b00 + +typedef DeviceType = enumerate {DeviceType_GRE; DeviceType_nGRE; + DeviceType_nGnRE; DeviceType_nGnRnE} + +typedef Fault = + enumerate { Fault_None; + Fault_AccessFlag; + Fault_Alignment; + Fault_Background; + Fault_Domain; + Fault_Permission; + Fault_Translation; + Fault_AddressSize; + Fault_SyncExternal; + Fault_SyncExternalOnWalk; + Fault_SyncParity; + Fault_SyncParityOnWalk; + Fault_AsyncParity; + Fault_AsyncExternal; + Fault_Debug; + Fault_TLBConflict; + Fault_Lockdown; + Fault_Exclusive; + Fault_ICacheMaint } + +typedef FaultRecord = const struct { + Fault type; (* Fault Status *) + AccType acctype; (* Type of access that faulted *) + bit[48] ipaddress; (* Intermediate physical address *) + boolean s2fs1walk; (* Is on a Stage 1 page table walk *) + boolean write; (* TRUE for a write, FALSE for a read *) + uinteger level; (* For translation, access flag and permission faults *) + bit extflag; (* IMPLEMENTATION DEFINED syndrome for external aborts *) + boolean secondstage; (* Is a Stage 2 abort *) + bit[4] domain; (* Domain number, AArch32 only *) + bit[4] debugmoe; (* Debug method of entry, from AArch32 only *) +} + +typedef MemAttrHints = const struct { + bit[2] attrs; (* The possible encodings for each attributes field are as below *) + bit[2] hints; (* The possible encodings for the hints are below *) + boolean transient; +} + +typedef MemType = enumerate {MemType_Normal; MemType_Device} + +typedef MemoryAttributes = const struct { + MemType type; + +(* DeviceType device; (* For Device memory types *) *) +(* MemAttrHints inner; (* Inner hints and attributes *) *) +(* MemAttrHints outer; (* Outer hints and attributes *) *) + + boolean shareable; +(* boolean outershareable; *) +} + +typedef FullAddress = const struct { + (* because we don't use TLB this is actually a virtual address and + therefore we have to use 64 bits instead of 48 *) + bit[64] physicaladdress; (* ARM: bit[48] physicaladdress *) + bit NS; (* '0' = Secure, '1' = Non-secure *) +} + +typedef AddressDescriptor = const struct { + FaultRecord fault; (* fault.type indicates whether the address is valid *) + MemoryAttributes memattrs; + FullAddress paddress; +} + +typedef PrefetchHint = + enumerate {Prefetch_READ; Prefetch_WRITE; Prefetch_EXEC} + +val forall Nat 'N, Nat 'S, 'S >= 1. (bit['N],[:'S:]) -> (bit['N], bit) effect pure ASR_C +val forall Nat 'N, Nat 'S, 'S >= 1. (bit['N],[:'S:]) -> (bit['N], bit) effect pure LSL_C +val forall Nat 'N, Nat 'S, 'S >= 1. (bit['N],[:'S:]) -> (bit['N], bit) effect pure LSR_C +val forall Nat 'N, Nat 'S, 'S >= 1, 'S <= -1. (bit['N],[:'S:]) -> (bit['N], bit) effect pure ROR_C +val forall Nat 'N. bit['N] -> boolean effect pure IsZero +val forall Nat 'N, Nat 'M. (implicit<'N>,bit['M]) -> bit['N] effect pure Replicate +val forall Nat 'N, Nat 'M, 'N >= 'M. (implicit<'N>,bit['M]) -> bit['N] effect pure SignExtend +val forall Nat 'N, Nat 'M, 'N >= 'M. (implicit<'N>,bit['M]) -> bit['N] effect pure ZeroExtend +val forall Nat 'N. implicit<'N> -> bit['N] effect pure Zeros +val forall Nat 'N. implicit<'N> -> bit['N] effect pure Ones +(* val forall Nat 'N, Nat 'M, 'M = 2**'N. bit['N] -> [|'M + -1|] effect pure UInt *) +val forall Nat 'N, Nat 'M. bit['N] -> [:'M:] effect pure UInt +(* val forall Nat 'N, Nat 'M, Nat 'K, 'M = 'N + -1, 'K = 2**'M. bit['N] -> [|'K * -1:'K + -1|] effect pure SInt *) +val forall Nat 'N, Nat 'M. bit['N] -> [:'M:] effect pure SInt +val forall Nat 'N. bit['N+1] -> [|-1:'N|] effect pure HighestSetBit +val forall Nat 'N. bit['N] -> [|'N|] effect pure CountLeadingZeroBits +val unit -> boolean effect {rreg} IsSecure +val unit -> boolean effect {rreg} IsSecureBelowEL3 +val unit -> SCRType effect pure SCR_GEN +val unit -> boolean effect pure UsingAArch32 +val bit[2] -> boolean effect pure ELUsingAArch32 +val unit -> boolean effect {rreg} Halted +val bit[2] -> boolean effect pure HaveEL +val unit -> boolean effect pure HaveAnyAArch32 +val unit -> boolean effect pure HighestELUsingAArch32 +val unit -> unit effect pure Unreachable +val BranchType -> unit effect pure Hint_Branch + +(*************************************************************************) +(*** AArch64 lib ***) + +typedef CountOp = + enumerate {CountOp_CLZ; CountOp_CLS; CountOp_CNT} + +typedef ExtendType = + (* the oreder is important for decoding *) + enumerate { ExtendType_UXTB; ExtendType_UXTH; ExtendType_UXTW; ExtendType_UXTX; + ExtendType_SXTB; ExtendType_SXTH; ExtendType_SXTW; ExtendType_SXTX } + +typedef RevOp = + enumerate {RevOp_RBIT; RevOp_REV16; RevOp_REV32; RevOp_REV64} + +typedef ShiftType = + (* the oreder is important for decoding *) + enumerate {ShiftType_LSL; ShiftType_LSR; ShiftType_ASR; ShiftType_ROR} + +typedef LogicalOp = + enumerate {LogicalOp_AND; LogicalOp_EOR; LogicalOp_ORR} + +typedef MemOp = + enumerate {MemOp_LOAD; MemOp_STORE; MemOp_PREFETCH} + +typedef MemBarrierOp = + enumerate {MemBarrierOp_DSB; MemBarrierOp_DMB; MemBarrierOp_ISB} + +typedef SystemHintOp = + enumerate {SystemHintOp_NOP; SystemHintOp_YIELD; + SystemHintOp_WFE; SystemHintOp_WFI; + SystemHintOp_SEV; SystemHintOp_SEVL} + +typedef PSTATEField = + enumerate {PSTATEField_DAIFSet; PSTATEField_DAIFClr; + PSTATEField_SP} + +val unit -> bit[64] effect {rreg} rPC +val forall Nat 'N, 'N IN {8,16,32,64}. implicit<'N> -> bit['N] effect {rreg} rSP +val forall Nat 'N, 'N IN {32,64}. (reg_index,bit['N]) -> unit effect {wreg} wX +val forall Nat 'N, 'N IN {8,16,32,64}. (implicit<'N>,reg_index) -> bit['N] effect {rreg} rX +val forall Nat 'N, 'N IN {8,16,32,64,128}. (SIMD_index,bit['N]) -> unit effect {wreg} wV +val forall Nat 'N, 'N IN {8,16,32,64,128}. (implicit<'N>,SIMD_index) -> bit['N] effect {rreg} rV +val forall Nat 'N, 'N IN {8,16,32,64,128}. (implicit<'N>,SIMD_index,[|1|]) -> bit['N] effect {rreg} rVpart +val unit -> SCTLR_type effect {rreg} SCTLR' +val unit -> unit effect {escape} AArch64_UndefinedFault +val (bit[64],AccType,boolean,boolean,uinteger) -> AddressDescriptor effect pure AArch64_TranslateAddress +val (bit[2],boolean) -> unit effect {escape} AArch64_WFxTrap +val (AccType,boolean,boolean) -> FaultRecord effect pure AArch64_AlignmentFault +val unit -> unit effect {wreg} AArch64_ResetGeneralRegisters +val unit -> unit effect {wreg} AArch64_ResetSIMDFPRegisters +val unit -> unit effect {wreg} AArch64_ResetSpecialRegisters +val (bit[64],integer,uinteger) -> boolean effect pure AArch64_IsExclusiveVA + +(*************************************************************************) +(*** AArch32 lib ***) + + + |