diff options
Diffstat (limited to 'arm/armV8.h.sail')
| -rw-r--r-- | arm/armV8.h.sail | 164 |
1 files changed, 164 insertions, 0 deletions
diff --git a/arm/armV8.h.sail b/arm/armV8.h.sail new file mode 100644 index 00000000..d9232a5b --- /dev/null +++ b/arm/armV8.h.sail @@ -0,0 +1,164 @@ +(*========================================================================*) +(* *) +(* 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. *) +(*========================================================================*) + +default Order dec + +typedef boolean = bit +typedef integer = int +typedef uinteger = nat (* ARM ARM does not have nat/uint type *) +typedef reg_size = bit[5] +typedef reg_index = [|31|] +typedef SIMD_index = [|32|] + +register (bit[64]) _PC + +(* General purpose registers *) + +register (bit[64]) R30 +register (bit[64]) R29 +register (bit[64]) R28 +register (bit[64]) R27 +register (bit[64]) R26 +register (bit[64]) R25 +register (bit[64]) R24 +register (bit[64]) R23 +register (bit[64]) R22 +register (bit[64]) R21 +register (bit[64]) R20 +register (bit[64]) R19 +register (bit[64]) R18 +register (bit[64]) R17 +register (bit[64]) R16 +register (bit[64]) R15 +register (bit[64]) R14 +register (bit[64]) R13 +register (bit[64]) R12 +register (bit[64]) R11 +register (bit[64]) R10 +register (bit[64]) R9 +register (bit[64]) R8 +register (bit[64]) R7 +register (bit[64]) R6 +register (bit[64]) R5 +register (bit[64]) R4 +register (bit[64]) R3 +register (bit[64]) R2 +register (bit[64]) R1 +register (bit[64]) R0 + +let (vector<31,32,dec,(register<bit[64]>)>) _R = + [undefined,R30,R29,R28,R27,R26,R25,R24,R23,R22,R21, + R20,R19,R18,R17,R16,R15,R14,R13,R12,R11, + R10,R9 ,R8 ,R7 ,R6 ,R5 ,R4 ,R3 ,R2 ,R1 , + R0] + +function reg_index effect pure UInt_reg((reg_size) x) = (reg_index) x + +(* SIMD and floating-point registers *) + +register (bit[128]) V31 +register (bit[128]) V30 +register (bit[128]) V29 +register (bit[128]) V28 +register (bit[128]) V27 +register (bit[128]) V26 +register (bit[128]) V25 +register (bit[128]) V24 +register (bit[128]) V23 +register (bit[128]) V22 +register (bit[128]) V21 +register (bit[128]) V20 +register (bit[128]) V19 +register (bit[128]) V18 +register (bit[128]) V17 +register (bit[128]) V16 +register (bit[128]) V15 +register (bit[128]) V14 +register (bit[128]) V13 +register (bit[128]) V12 +register (bit[128]) V11 +register (bit[128]) V10 +register (bit[128]) V9 +register (bit[128]) V8 +register (bit[128]) V7 +register (bit[128]) V6 +register (bit[128]) V5 +register (bit[128]) V4 +register (bit[128]) V3 +register (bit[128]) V2 +register (bit[128]) V1 +register (bit[128]) V0 + +let (vector<32,33,dec,(register<bit[128]>)>) _V = + [undefined,V31,V30,V29,V28,V27,V26,V25,V24,V23,V22, + V21,V20,V19,V18,V17,V16,V15,V14,V13,V12, + V11,V10,V9 ,V8 ,V7 ,V6 ,V5 ,V4 ,V3 ,V2 , + V1 ,V0] + + +(* lsl: used instead of the ARM ARM << over integers *) +function forall Nat 'm, Nat 'n, 'm >= 0, 'n >= 0. [:'n * 2** 'm:] lsl(([:'n:]) n, ([:'m:]) m) = n * (2 ** m) + +(* not_implemented is used to indicate something WE did not implement *) +function unit effect { escape } not_implemented((string) message) = +{ + exit message; +} + +(* info is used to convey information to the user *) +function unit effect pure info((string) message) = () + +typedef IMPLEMENTATION_DEFINED_type = const struct +{ + boolean HaveCRCExt; + boolean HaveAArch32EL; + boolean HaveAnyAArch32; + boolean HaveEL2; + boolean HaveEL3; + boolean HighestELUsingAArch32; + boolean IsSecureBelowEL3; +} +let IMPLEMENTATION_DEFINED = +{ + HaveCRCExt = true; + HaveAArch32EL = false; + HaveAnyAArch32 = false; + HaveEL2 = false; + HaveEL3 = false; + HighestELUsingAArch32 = false; + IsSecureBelowEL3 = false; +} + +(* FIXME: ask Kathy what should we do with this *) +let UNKNOWN = 0 |