diff options
Diffstat (limited to 'aarch64_small/armV8_lib.h.sail')
| -rw-r--r-- | aarch64_small/armV8_lib.h.sail | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/aarch64_small/armV8_lib.h.sail b/aarch64_small/armV8_lib.h.sail index 50909c88..6f09ad13 100644 --- a/aarch64_small/armV8_lib.h.sail +++ b/aarch64_small/armV8_lib.h.sail @@ -153,33 +153,33 @@ struct AddressDescriptor = { enum PrefetchHint = {Prefetch_READ, Prefetch_WRITE, Prefetch_EXEC} -val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect pure +val ASR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect {escape} val LSL_C : forall 'N 'S, 'N >= 0 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect pure -val LSR_C : forall 'N 'S, 'N >= 0 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect pure -val ROR_C : forall 'N 'S, 'N >= 0 & ('S >= 1 | 'S <= -1). (bits('N),int('S)) -> (bits('N), bit) effect pure +val LSR_C : forall 'N 'S, 'N >= 1 & 'S >= 1. (bits('N),atom('S)) -> (bits('N), bit) effect pure +val ROR_C : forall 'N 'S, 'N >= 1 & 'S != 0. (bits('N),atom('S)) -> (bits('N), bit) effect pure val IsZero : forall 'N, 'N >=0. bits('N) -> boolean effect pure -val Replicate : forall 'N 'M, 'N >=0 & 'M >=0. (implicit('N),bits('M)) -> bits('N) effect pure -val SignExtend : forall 'N 'M, 'N > 'M & 'M >= 1. (implicit('N),bits('M)) -> bits('N) effect pure +val Replicate : forall 'N 'M, 'N >='M & 'M >=0. (implicit('N),bits('M)) -> bits('N) effect {escape} +val SignExtend : forall 'N 'M, 'N > 'M & 'M >= 1. (implicit('N),bits('M)) -> bits('N) effect {escape} val ZeroExtend : forall 'N 'M, 'N >= 'M & 'M >= 0. (implicit('N),bits('M)) -> bits('N) effect pure val Zeros : forall 'N, 'N >=0. implicit('N) -> bits('N) effect pure -val Ones : forall 'N, 'N >=0. implicit('N) -> bits('N) effect pure +val Ones : forall 'N, 'N >=1. implicit('N) -> bits('N) effect {escape} /* val UInt : forall Nat 'N, Nat 'M, 'M = 2**'N. bits('N) -> [|'M + -1|] effect pure */ -val UInt : forall 'N, 'N >=0 . bits('N) -> range(0, 2 ^ 'N + -1) +val UInt : forall 'N, 'N >=0 . bits('N) -> range(0, 2 ^ 'N + -1) effect {escape} /* val UInt : forall 'N 'M, 'N >=0 & 'M >= 0. bits('N) -> Int('M) effect pure */ /* val SInt : forall Nat 'N, Nat 'M, Nat 'K, 'M = 'N + -1, 'K = 2**'M. bits('N) -> [|'K * -1:'K + -1|] effect pure */ -val SInt : forall 'N, 'N >= 0. bits('N) -> range(-(2 ^ ('N - 1) - 1), 2 ^ ('N - 1) - 1) effect pure +val SInt : forall 'N, 'N > 0. bits('N) -> range(-(2 ^ ('N - 1)), 2 ^ ('N - 1) - 1) effect pure val HighestSetBit : forall 'N, 'N >= 0. bits('N) -> option(range(0,'N - 1)) effect pure val CountLeadingZeroBits : forall 'N, 'N >= 0. bits('N) -> range(0,'N) effect pure -val IsSecure : unit -> boolean effect {rreg} -val IsSecureBelowEL3 : unit -> boolean effect {rreg} -val SCR_GEN : unit -> SCRType effect pure +val IsSecure : unit -> boolean effect {escape,rreg} +val IsSecureBelowEL3 : unit -> boolean effect {escape,rreg} +val SCR_GEN : unit -> SCRType effect {escape,rreg} val UsingAArch32 : unit -> boolean effect pure val ELUsingAArch32 : bits(2) -> boolean effect pure val Halted : unit -> boolean effect {rreg} -val HaveEL : bits(2) -> boolean effect pure +val HaveEL : bits(2) -> boolean effect {escape} val HaveAnyAArch32 : unit -> boolean effect pure val HighestELUsingAArch32 : unit -> boolean effect pure -val Unreachable : unit -> unit effect pure +val Unreachable : unit -> unit effect {escape} val Hint_Branch : BranchType -> unit effect pure /*************************************************************************/ @@ -211,20 +211,20 @@ enum PSTATEField = {PSTATEField_DAIFSet, PSTATEField_DAIFClr, PSTATEField_SP} val rPC : unit -> bits(64) effect {rreg} -val rSP : forall 'N, 'N in {8,16,32,64}. implicit('N) -> bits('N) effect {rreg} +val rSP : forall 'N, 'N in {8,16,32,64}. implicit('N) -> bits('N) effect {rreg,escape} val wX : forall 'N, 'N in {32,64}. (reg_index,bits('N)) -> unit effect {wreg} val rX : forall 'N, 'N in {8,16,32,64}. (implicit('N),reg_index) -> bits('N) effect {rreg} 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} -val SCTLR : unit -> SCTLR_type 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 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} val AArch64_AlignmentFault : (AccType,boolean,boolean) -> FaultRecord effect pure val AArch64_ResetGeneralRegisters : unit -> unit effect {wreg} val AArch64_ResetSIMDFPRegisters : unit -> unit effect {wreg} -val AArch64_ResetSpecialRegisters : unit -> unit effect {wreg} +val AArch64_ResetSpecialRegisters : unit -> unit effect {wreg,escape} val AArch64_IsExclusiveVA : (bits(64),integer,uinteger) -> boolean effect pure /*************************************************************************/ |