diff options
| author | Christopher Pulte | 2019-02-28 13:18:54 +0000 |
|---|---|---|
| committer | Christopher Pulte | 2019-02-28 13:18:54 +0000 |
| commit | a20101dc3769b5c5a6e51753c1be42f78df86e22 (patch) | |
| tree | d99cfbf3ec04e1d117c39912a4d04e22f5ccd0a0 /aarch64_small/armV8_embed_sequential.lem | |
| parent | 9fd08144367f0b3a08bd5fd3e973ede900a9c72d (diff) | |
more progress
Diffstat (limited to 'aarch64_small/armV8_embed_sequential.lem')
| -rw-r--r-- | aarch64_small/armV8_embed_sequential.lem | 5561 |
1 files changed, 0 insertions, 5561 deletions
diff --git a/aarch64_small/armV8_embed_sequential.lem b/aarch64_small/armV8_embed_sequential.lem deleted file mode 100644 index 21841fe1..00000000 --- a/aarch64_small/armV8_embed_sequential.lem +++ /dev/null @@ -1,5561 +0,0 @@ -(*Generated by Sail from armV8.sail.*) -open import Pervasives_extra -open import Sail_impl_base -open import State -open import Sail_values -open import ArmV8_embed_types -open import ArmV8_extras_embed_sequential -let lsl' (n, m) = n * (pow (2:ii) m) - -let not_implemented message = exit message - -let not_implemented_extern message = exit message - -let info message = () - -let UNKNOWN = (0:ii) - -let M32_User = Vector [B1;B0;B0;B0;B0] 4 false - -let M32_FIQ = Vector [B1;B0;B0;B0;B1] 4 false - -let M32_IRQ = Vector [B1;B0;B0;B1;B0] 4 false - -let M32_Svc = Vector [B1;B0;B0;B1;B1] 4 false - -let M32_Monitor = Vector [B1;B0;B1;B1;B0] 4 false - -let M32_Abort = Vector [B1;B0;B1;B1;B1] 4 false - -let M32_Hyp = Vector [B1;B1;B0;B1;B0] 4 false - -let M32_Undef = Vector [B1;B1;B0;B1;B1] 4 false - -let M32_System = Vector [B1;B1;B1;B1;B1] 4 false - -let EL3 = Vector [B1;B1] 1 false - -let EL2 = Vector [B1;B0] 1 false - -let EL1 = Vector [B0;B1] 1 false - -let EL0 = Vector [B0;B0] 1 false - -let DebugHalt_Breakpoint = Vector [B0;B0;B0;B1;B1;B1] 5 false - -let DebugHalt_EDBGRQ = Vector [B0;B1;B0;B0;B1;B1] 5 false - -let DebugHalt_Step_Normal = Vector [B0;B1;B1;B0;B1;B1] 5 false - -let DebugHalt_Step_Exclusive = Vector [B0;B1;B1;B1;B1;B1] 5 false - -let DebugHalt_OSUnlockCatch = Vector [B1;B0;B0;B0;B1;B1] 5 false - -let DebugHalt_ResetCatch = Vector [B1;B0;B0;B1;B1;B1] 5 false - -let DebugHalt_Watchpoint = Vector [B1;B0;B1;B0;B1;B1] 5 false - -let DebugHalt_HaltInstruction = Vector [B1;B0;B1;B1;B1;B1] 5 false - -let DebugHalt_SoftwareAccess = Vector [B1;B1;B0;B0;B1;B1] 5 false - -let DebugHalt_ExceptionCatch = Vector [B1;B1;B0;B1;B1;B1] 5 false - -let DebugHalt_Step_NoSyndrome = Vector [B1;B1;B1;B0;B1;B1] 5 false - -let HighestSetBit x = - let N = length (reset_vector_start (set_vector_start_to_length x)) in - let result = (0:ii) in - let break = B0 in - let (break, result) = - (foreach_dec (N - (1:ii),(0:ii),(1:ii)) (break,result) - (fun i (break,result) -> - let (result, break) = - if bitU_to_bool - ((~break) &. - (eq - (match (access (set_vector_start_to_length x) i) with - | B0 -> (0:ii) - | B1 -> (1:ii) - end, - (1:ii)))) - then - let result = i in - let break = B1 in - (result,break) - else (result,break) in - (break,result))) in - if bitU_to_bool break - then Just result - else Nothing - -let IsZero x = eq_vec_range (set_vector_start_to_length x, (0:ii)) - -let NOT x = - set_vector_start_to_length (bitwise_not (reset_vector_start (set_vector_start_to_length x))) - -let NOT' x = ~x - -let SInt x = signed (reset_vector_start (set_vector_start_to_length x)) - -let UInt x = unsigned (reset_vector_start (set_vector_start_to_length x)) - -let Zeros N' = set_vector_start_to_length (to_vec_dec (N',(0:ii))) - -let BitReverse data = - let N = length (reset_vector_start (set_vector_start_to_length data)) in - let result = set_vector_start_to_length (to_vec_dec (length data,(0:ii))) in - (foreach_inc ((0:ii),N - (1:ii),(1:ii)) result - (fun i result -> - update_pos result ((N - i) - (1:ii)) (access (set_vector_start_to_length data) i))) - -let ELUsingAArch32 el = B0 - -let Hint_Yield () = () - -let SendEvent () = () - -let Unreachable () = assert' B0 (Just "Unreachable reached") - -let UsingAArch32 () = B0 - -let _Rs = - Vector ["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"] 30 false - -let IMPLEMENTATION_DEFINED = - <| IMPLEMENTATION_DEFINED_type_HaveCRCExt = B1; - IMPLEMENTATION_DEFINED_type_HaveAArch32EL = B0; - IMPLEMENTATION_DEFINED_type_HaveAnyAArch32 = B0; - IMPLEMENTATION_DEFINED_type_HaveEL2 = B0; - IMPLEMENTATION_DEFINED_type_HaveEL3 = B0; - IMPLEMENTATION_DEFINED_type_HighestELUsingAArch32 = B0; - IMPLEMENTATION_DEFINED_type_IsSecureBelowEL3 = B0 |> - -let AArch64_ResetControlRegisters cold_reset = () - -let DCPSInstruction target_el = not_implemented "DCPSInstruction" - -let DRPSInstruction () = not_implemented "DRPSInstruction" - -let Halt reason = not_implemented "Halt" - -let Align' (x, y) = y * (quot x y) - -let CountLeadingZeroBits x = - match (HighestSetBit (reset_vector_start (set_vector_start_to_length x))) with - | Nothing -> length (reset_vector_start (set_vector_start_to_length x)) - | Just (n) -> ((length (reset_vector_start (set_vector_start_to_length x))) - (1:ii)) - n - end - -let IsZeroBit x = - if bitU_to_bool (IsZero (reset_vector_start (set_vector_start_to_length x))) - then B1 - else B0 - -let LSL_C (x, shift) = - let extended_x = - set_vector_start_to_length - ((set_vector_start_to_length x) ^^ - (set_vector_start_to_length (set_vector_start_to_length (Zeros shift)))) in - let result = - set_vector_start_to_length - (set_vector_start_to_length - (mask (length x,reset_vector_start (set_vector_start_to_length extended_x)))) in - let carry_out = - access (set_vector_start_to_length extended_x) (length - (reset_vector_start (set_vector_start_to_length - x))) in - (set_vector_start_to_length result,carry_out) - -let Min (a, b) = if bitU_to_bool (lteq (a, b)) then a else b - -let uMin (a, b) = if bitU_to_bool (lteq (a, b)) then a else b - -let Replicate (N', x) = - let (N, M) = - (length (reset_vector_start (set_vector_start_to_length (to_vec_dec (N',(0:ii))))),length - (reset_vector_start (set_vector_start_to_length - (to_vec_dec - (length - x, - (0:ii)))))) in - let _ = assert' (eq_range (modulo N M, (0:ii))) (Nothing) in - let result = set_vector_start_to_length (to_vec_dec (N',(0:ii))) in - let zeros = set_vector_start_to_length (Zeros ((length result) - (length x))) in - (foreach_inc (M,N,M) result - (fun i result -> - set_vector_start_to_length - (bitwise_or - (set_vector_start_to_length (bitwise_leftshift (set_vector_start_to_length result, M)), - set_vector_start_to_length - ((set_vector_start_to_length zeros) ^^ (set_vector_start_to_length x)))))) - -let ZeroExtend (N', x) = - set_vector_start_to_length - ((set_vector_start_to_length - (set_vector_start_to_length (Zeros (N' + ((length x) * ((0-1):ii)))))) ^^ - (set_vector_start_to_length x)) - -let Poly32Mod2 (data, poly) = - let result = set_vector_start_to_length data in - let N = length (reset_vector_start (set_vector_start_to_length data)) in - let _ = assert' (gt (N, (32:ii))) (Nothing) in - let data' = set_vector_start_to_length data in - let zeros = set_vector_start_to_length (Zeros ((length data) - (32:ii))) in - let data' = - (foreach_dec (N - (1:ii),(32:ii),(1:ii)) data' - (fun i data' -> - if bitU_to_bool - (eq - (match (access (set_vector_start_to_length data') i) with - | B0 -> (0:ii) - | B1 -> (1:ii) - end, - (1:ii))) - then - update - data' (i - (1:ii)) (0:ii) - (set_vector_start_to_length - (bitwise_xor - (set_vector_start_to_length - (slice (set_vector_start_to_length data') (i - (1:ii)) (0:ii)), - set_vector_start_to_length - ((set_vector_start_to_length poly) ^^ - (set_vector_start_to_length - (slice (set_vector_start_to_length zeros) (i - (33:ii)) (0:ii))))))) - else data')) in - slice (set_vector_start_to_length data') (31:ii) (0:ii) - -let ClearExclusiveLocal processorid = - info "The model does not implement the exclusive monitors explicitly." - -let ProcessorID () = (0:ii) - -let rec BigEndianReverse value = - let width = length (reset_vector_start (set_vector_start_to_length value)) in - let half = quot width (2:ii) in - if bitU_to_bool (eq_range (width, (8:ii))) - then set_vector_start_to_length value - else - set_vector_start_to_length - ((set_vector_start_to_length - (BigEndianReverse - (reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length value) (half - (1:ii)) (0:ii)))))) ^^ - (set_vector_start_to_length - (BigEndianReverse - (reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length value) (width - (1:ii)) half)))))) - -let ClearEventRegister () = not_implemented_extern "ClearEventRegister" - -let EventRegisterSet () = not_implemented_extern "EventRegisterSet" - -let EventRegistered () = not_implemented_extern "EventRegistered" - -let InterruptPending () = not_implemented_extern "InterruptPending" - -let WaitForEvent () = not_implemented_extern "WaitForEvent" - -let WaitForInterrupt () = not_implemented_extern "WaitForInterrupt" - -let AArch64_SPAlignmentFault () = not_implemented "AArch64_SPAlignmentFault" - -let AArch64_SoftwareBreakpoint immediate = not_implemented "AArch64_SoftwareBreakpoint" - -let AArch64_CallHypervisor immediate = not_implemented "AArch64_CallHypervisor" - -let AArch64_CallSecureMonitor immediate = not_implemented "AArch64_CallSecureMonitor" - -let AArch64_CallSupervisor immediate = not_implemented "AArch64_CallSupervisor" - -let AArch64_SystemRegisterTrap (target_el, op0, op2, op1, crn, rt, crm, dir) = - not_implemented "AArch64_SystemRegisterTrap" - -let AArch64_UndefinedFault () = not_implemented "AArch64_UndefinedFault" - -let rPC () = read_reg _PC - -let AArch64_ExceptionReturn (new_pc, spsr) = not_implemented "AArch64_ExceptionReturn" - -let UInt_reg x = unsigned x - -let signalDBGEN () = not_implemented_extern "signalDBGEN" - -let signelNIDEN () = not_implemented_extern "signalNIDEN" - -let signalSPIDEN () = not_implemented_extern "signalSPIDEN" - -let signalDPNIDEN () = not_implemented_extern "signalSPNIDEN" - -let Halted () = - read_reg_field EDSCR "STATUS" >>= fun w__0 -> - read_reg_field EDSCR "STATUS" >>= fun w__1 -> - return (~((eq_vec - (set_vector_start_to_length w__0, - set_vector_start_to_length (Vector [B0;B0;B0;B0;B0;B1] 5 false))) |. - (eq_vec - (set_vector_start_to_length w__1, - set_vector_start_to_length (Vector [B0;B0;B0;B0;B1;B0] 5 false))))) - -let HaveCRCExt () = IMPLEMENTATION_DEFINED.IMPLEMENTATION_DEFINED_type_HaveCRCExt - -let ExclusiveMonitorsStatus () = - let _ = info "The model does not implement the exclusive monitors explicitly." in - not_implemented "ExclusiveMonitorsStatus should not be called" >> - return B0 - -let Hint_Branch hint = - info "This hint can be used for hardware optimization that has no effect on the model." - -let ResetExternalDebugRegisters b = not_implemented_extern "ResetExternalDebugRegisters" - -let HaveAnyAArch32 () = IMPLEMENTATION_DEFINED.IMPLEMENTATION_DEFINED_type_HaveAnyAArch32 - -let AArch64_WFxTrap (target_el, is_wfe) = not_implemented "AArch64_WFxTrap" - -let AArch64_CheckUnallocatedSystemAccess (op0, op1, crn, crm, op2, read) = - match (op0,op1,crn,crm,op2,read) with - | (Vector [B0;B0] _ _, Vector [B0;B0;B0] _ _, Vector [B0;B1;B0;B0] _ _, _, Vector [B1;B0;B1] _ _, _) -> - read_reg_field CurrentEL "EL" >>= fun w__0 -> - return (lt_vec (set_vector_start_to_length w__0, set_vector_start_to_length EL1)) - | (Vector [B0;B0] _ _, Vector [B0;B1;B1] _ _, Vector [B0;B1;B0;B0] _ _, _, Vector [B1;B1;B0] _ _, _) -> - return B0 - | (Vector [B0;B0] _ _, Vector [B0;B1;B1] _ _, Vector [B0;B1;B0;B0] _ _, _, Vector [B1;B1;B1] _ _, _) -> - return B0 - | (Vector [B1;B1] _ _, Vector [B0;B1;B1] _ _, Vector [B0;B1;B0;B0] _ _, Vector [B0;B0;B1;B0] _ _, Vector [B0;B0;B0] _ _, _) -> - return B0 - | (Vector [B1;B1] _ _, Vector [B0;B1;B1] _ _, Vector [B0;B1;B0;B0] _ _, Vector [B0;B0;B1;B0] _ _, Vector [B0;B0;B1] _ _, _) -> - return B0 - end - -let SysOp_R (op0, op1, crn, crm, op2) = - not_implemented "SysOp_R" >> - return (to_vec_dec ((64:ii),(0:ii))) - -let SysOp_W (op0, op1, crn, crm, op2, _val) = not_implemented "SysOp_W" - -let TxNestingLevelfp = RFull "TxNestingLevel" - -let TXIDR_EL0_DEPTHfp = RField ("TXIDR_EL0","DEPTH") - -let PSTATE_Nfp = RField ("NZCV","N") - -let PSTATE_Zfp = RField ("NZCV","Z") - -let PSTATE_Cfp = RField ("NZCV","C") - -let PSTATE_Vfp = RField ("NZCV","V") - -let PSTATE_Dfp = RField ("DAIF","D") - -let PSTATE_Afp = RField ("DAIF","A") - -let PSTATE_Ifp = RField ("DAIF","I") - -let PSTATE_Ffp = RField ("DAIF","F") - -let PSTATE_ELfp = RFull "CurrentEL" - -let PSTATE_SPfp = RField ("SPSel","SP") - -let _PCfp = RFull "_PC" - -let Hint_Prefetch (addr, hint, target, stream) = () - -let AArch64_IsExclusiveVA (address, processorid, size) = - let _ = info "The model does not implement the exclusive monitors explicitly." in - B1 - -let AArch64_MarkExclusiveVA (address, processorid, size) = - info "The model does not implement the exclusive monitors explicitly." - -let wPSTATE_NZCV ((), Vector [n;z;c;v] _ _) = - write_reg_bitfield NZCV "N" n >> - write_reg_bitfield NZCV "Z" z >> - write_reg_bitfield NZCV "C" c >> - write_reg_bitfield NZCV "V" v - -let wPSTATE_DAIF ((), Vector [d;a;i;f] _ _) = - write_reg_bitfield DAIF "D" d >> - write_reg_bitfield DAIF "A" a >> - write_reg_bitfield DAIF "I" i >> - write_reg_bitfield DAIF "F" f - -let Int (x, unsigned) = - if bitU_to_bool unsigned - then UInt (reset_vector_start (set_vector_start_to_length x)) - else SInt (reset_vector_start (set_vector_start_to_length x)) - -let ClearExclusiveByAddress (paddress, processorid, size) = - info "The model does not implement the exclusive monitors explicitly." - -let IsExclusiveGlobal (paddress, processorid, size) = - let _ = info "The model does not implement the exclusive monitors explicitly." in - B1 - -let IsExclusiveLocal (paddress, processorid, size) = - let _ = info "The model does not implement the exclusive monitors explicitly." in - B1 - -let MarkExclusiveGlobal (paddress, processorid, size) = - info "The model does not implement the exclusive monitors explicitly." - -let MarkExclusiveLocal (paddress, processorid, size) = - info "The model does not implement the exclusive monitors explicitly." - -let PAMax () = - let pa_size = (0:ii) in - read_reg_field ID_AA64MMFR0_EL1 "PARange" >>= fun w__0 -> - let pa_size = - match w__0 with - | Vector [B0;B0;B0;B0] _ _ -> (32:ii) - | Vector [B0;B0;B0;B1] _ _ -> (36:ii) - | Vector [B0;B0;B1;B0] _ _ -> (40:ii) - | Vector [B0;B0;B1;B1] _ _ -> (42:ii) - | Vector [B0;B1;B0;B0] _ _ -> (44:ii) - | Vector [B0;B1;B0;B1] _ _ -> (48:ii) - | _ -> pa_size - end in - return pa_size - -let AddWithCarry (x, y, carry_in) = - let unsigned_sum = - ((UInt (reset_vector_start (set_vector_start_to_length x))) + - (UInt (reset_vector_start (set_vector_start_to_length y)))) + - (UInt (reset_vector_start (set_vector_start_to_length (Vector [carry_in] 0 false)))) in - let signed_sum = - ((SInt (reset_vector_start (set_vector_start_to_length x))) + - (SInt (reset_vector_start (set_vector_start_to_length y)))) + - (UInt (reset_vector_start (set_vector_start_to_length (Vector [carry_in] 0 false)))) in - let result = set_vector_start_to_length (to_vec_dec (length x,unsigned_sum)) in - let n = - access (set_vector_start_to_length result) ((length - (reset_vector_start (set_vector_start_to_length - result))) - (1:ii)) in - let z = - if bitU_to_bool (IsZero (reset_vector_start (set_vector_start_to_length result))) - then B1 - else B0 in - let c = - if bitU_to_bool - (eq_range (UInt (reset_vector_start (set_vector_start_to_length result)), unsigned_sum)) - then B0 - else B1 in - let v = - if bitU_to_bool - (eq_range (SInt (reset_vector_start (set_vector_start_to_length result)), signed_sum)) - then B0 - else B1 in - (set_vector_start_to_length result,set_vector_start 3 - ((set_vector_start_to_length (Vector [n] 0 false)) ^^ - (set_vector_start_to_length - ((set_vector_start_to_length (Vector [z] 0 false)) ^^ - (set_vector_start_to_length - ((set_vector_start_to_length (Vector [c] 0 false)) ^^ - (set_vector_start_to_length (Vector [v] 0 false)))))))) - -let ConditionHolds _cond = - let result = B0 in - match (slice _cond (3:ii) (1:ii)) with - | Vector [B0;B0;B0] _ _ -> - read_reg_bitfield NZCV "Z" >>= fun w__0 -> - let result = eq (match w__0 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - return result - | Vector [B0;B0;B1] _ _ -> - read_reg_bitfield NZCV "C" >>= fun w__1 -> - let result = eq (match w__1 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - return result - | Vector [B0;B1;B0] _ _ -> - read_reg_bitfield NZCV "N" >>= fun w__2 -> - let result = eq (match w__2 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - return result - | Vector [B0;B1;B1] _ _ -> - read_reg_bitfield NZCV "V" >>= fun w__3 -> - let result = eq (match w__3 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - return result - | Vector [B1;B0;B0] _ _ -> - read_reg_bitfield NZCV "C" >>= fun w__4 -> - read_reg_bitfield NZCV "Z" >>= fun w__5 -> - let result = - (eq (match w__4 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) &. - (eq (match w__5 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) in - return result - | Vector [B1;B0;B1] _ _ -> - read_reg_bitfield NZCV "N" >>= fun w__6 -> - read_reg_bitfield NZCV "V" >>= fun w__7 -> - let result = eq_bit (w__6, w__7) in - return result - | Vector [B1;B1;B0] _ _ -> - read_reg_bitfield NZCV "N" >>= fun w__8 -> - read_reg_bitfield NZCV "V" >>= fun w__9 -> - read_reg_bitfield NZCV "Z" >>= fun w__10 -> - let result = - (eq_bit (w__8, w__9)) &. (eq (match w__10 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) in - return result - | Vector [B1;B1;B1] _ _ -> return B1 - end >>= fun result -> - let result = - if bitU_to_bool - ((eq (match (access _cond (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) &. - (neq_vec - (set_vector_start_to_length _cond, - set_vector_start_to_length (Vector [B1;B1;B1;B1] 3 false)))) - then ~result - else result in - return result - -let DecodeShift op = - match toNatural (unsigned (reset_vector_start op)) with - | (0:nn) -> ShiftType_LSL - | (1:nn) -> ShiftType_LSR - | (2:nn) -> ShiftType_ASR - | (3:nn) -> ShiftType_ROR - end - -let HaveEL el = - if bitU_to_bool - ((eq_vec (set_vector_start_to_length el, set_vector_start_to_length EL1)) |. - (eq_vec (set_vector_start_to_length el, set_vector_start_to_length EL0))) - then B1 - else - if bitU_to_bool (eq_vec (set_vector_start_to_length el, set_vector_start_to_length EL2)) - then IMPLEMENTATION_DEFINED.IMPLEMENTATION_DEFINED_type_HaveEL2 - else - if bitU_to_bool (eq_vec (set_vector_start_to_length el, set_vector_start_to_length EL3)) - then IMPLEMENTATION_DEFINED.IMPLEMENTATION_DEFINED_type_HaveEL3 - else - let _ = assert' B0 (Nothing) in - B0 - -let System_Put (op0, op1, crn, crm, op2, _val) = - match toNaturalFiveTup (op0,op1,crn,crm,op2) with - | ((3:nn), (3:nn), (4:nn), (2:nn), (0:nn)) -> write_reg NZCV (slice _val (31:ii) (0:ii)) - | ((3:nn), (3:nn), (4:nn), (2:nn), (1:nn)) -> write_reg DAIF (slice _val (31:ii) (0:ii)) - | ((3:nn), (3:nn), (13:nn), (0:nn), (2:nn)) -> write_reg TPIDR_EL0 (slice _val (63:ii) (0:ii)) - end - -let DataSynchronizationBarrier (domain, types) = - (if bitU_to_bool (neq (domain, MBReqDomain_FullSystem)) - then not_implemented "DataSynchronizationBarrier: not MBReqDomain_FullSystem" - else return ()) >> - match types with - | MBReqTypes_Reads -> DataSynchronizationBarrier_Reads () - | MBReqTypes_Writes -> DataSynchronizationBarrier_Writes () - | MBReqTypes_All -> DataSynchronizationBarrier_All () - end - -let rELR el = - let r = to_vec_dec ((64:ii),(0:ii)) in - if bitU_to_bool (eq_vec (set_vector_start_to_length el, set_vector_start_to_length EL1)) - then read_reg ELR_EL1 - else - if bitU_to_bool (eq_vec (set_vector_start_to_length el, set_vector_start_to_length EL2)) - then read_reg ELR_EL2 - else - if bitU_to_bool (eq_vec (set_vector_start_to_length el, set_vector_start_to_length EL3)) - then read_reg ELR_EL3 - else return r - -let DataMemoryBarrier (domain, types) = - (if bitU_to_bool - ((neq (domain, MBReqDomain_FullSystem)) &. (neq (domain, MBReqDomain_InnerShareable))) - then not_implemented "DataMemoryBarrier: not MBReqDomain_FullSystem or _InnerShareable" - else return ()) >> - match types with - | MBReqTypes_Reads -> DataMemoryBarrier_Reads () - | MBReqTypes_Writes -> DataMemoryBarrier_Writes () - | MBReqTypes_All -> DataMemoryBarrier_All () - end - -let wMem_Addr (address, size, acctype, excl) = - match (excl,acctype) with - | (B0, AccType_NORMAL) -> wMem_Addr_NORMAL (reset_vector_start address,size) - | (B0, AccType_STREAM) -> wMem_Addr_NORMAL (reset_vector_start address,size) - | (B0, AccType_UNPRIV) -> wMem_Addr_NORMAL (reset_vector_start address,size) - | (B0, AccType_ORDERED) -> wMem_Addr_ORDERED (reset_vector_start address,size) - | (B1, AccType_ATOMIC) -> wMem_Addr_ATOMIC (reset_vector_start address,size) - | (B1, AccType_ORDERED) -> wMem_Addr_ATOMIC_ORDERED (reset_vector_start address,size) - | _ -> not_implemented "unrecognised memory access" - end - -let SCTLR regime = - if bitU_to_bool (eq_vec (set_vector_start_to_length regime, set_vector_start_to_length EL1)) - then SCTLR_EL1 - else - if bitU_to_bool (eq_vec (set_vector_start_to_length regime, set_vector_start_to_length EL2)) - then SCTLR_EL2 - else - if bitU_to_bool (eq_vec (set_vector_start_to_length regime, set_vector_start_to_length EL3)) - then SCTLR_EL3 - else - let _ = assert' B0 (Just "SCTLR_type unreachable") in - SCTLR_EL1 - -let DecodeRegExtend op = - match op with - | Vector [B0;B0;B0] _ _ -> ExtendType_UXTB - | Vector [B0;B0;B1] _ _ -> ExtendType_UXTH - | Vector [B0;B1;B0] _ _ -> ExtendType_UXTW - | Vector [B0;B1;B1] _ _ -> ExtendType_UXTX - | Vector [B1;B0;B0] _ _ -> ExtendType_SXTB - | Vector [B1;B0;B1] _ _ -> ExtendType_SXTH - | Vector [B1;B1;B0] _ _ -> ExtendType_SXTW - | Vector [B1;B1;B1] _ _ -> ExtendType_SXTX - end - -let rSP N' = - read_reg_bitfield SPSel "SP" >>= fun w__0 -> - if bitU_to_bool (eq (match w__0 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) - then - read_reg SP_EL0 >>= fun w__1 -> - return (set_vector_start_to_length (mask (N',w__1))) - else - read_reg_field CurrentEL "EL" >>= fun pstate_el -> - if bitU_to_bool (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL0)) - then - read_reg SP_EL0 >>= fun w__2 -> - return (set_vector_start_to_length (mask (N',w__2))) - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL1)) - then - read_reg SP_EL1 >>= fun w__3 -> - return (set_vector_start_to_length (mask (N',w__3))) - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL2)) - then - read_reg SP_EL2 >>= fun w__4 -> - return (set_vector_start_to_length (mask (N',w__4))) - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL3)) - then - read_reg SP_EL3 >>= fun w__5 -> - return (set_vector_start_to_length (mask (N',w__5))) - else - let _ = assert' B0 (Nothing) in - read_reg SP_EL3 >>= fun w__6 -> - return (set_vector_start_to_length (mask (N',w__6))) - -let rSPSR () = - let result = to_vec_dec ((32:ii),(0:ii)) in - if bitU_to_bool (UsingAArch32 ()) - then - not_implemented "rSPSR UsingAArch32" >> - return result - else - read_reg_field CurrentEL "EL" >>= fun pstate_el -> - if bitU_to_bool (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL1)) - then read_reg SPSR_EL1 - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL2)) - then read_reg SPSR_EL2 - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL3)) - then read_reg SPSR_EL3 - else return result - -let _R = - Vector [UndefinedRegister 0;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] 31 false - -let _V = - Vector [UndefinedRegister 0;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] 32 false - -let ReservedValue () = AArch64_UndefinedFault () - -let UnallocatedEncoding () = AArch64_UndefinedFault () - -let CountLeadingSignBits x = - CountLeadingZeroBits - (reset_vector_start (set_vector_start_to_length - (bitwise_xor - (set_vector_start_to_length - (slice (set_vector_start_to_length x) - ((length (reset_vector_start (set_vector_start_to_length x))) - (1:ii)) (1:ii)), - set_vector_start_to_length - (slice (set_vector_start_to_length x) - ((length (reset_vector_start (set_vector_start_to_length x))) - (2:ii)) (0:ii)))))) - -let LSR_C (x, shift) = - let extended_x = - set_vector_start_to_length - (ZeroExtend ((length x) + shift,reset_vector_start (set_vector_start_to_length x))) in - let result = - set_vector_start_to_length - (slice (set_vector_start_to_length extended_x) - ((shift + (length (reset_vector_start (set_vector_start_to_length x)))) - (1:ii)) shift) in - let carry_out = access (set_vector_start_to_length extended_x) (shift - (1:ii)) in - (set_vector_start_to_length result,carry_out) - -let Ones N' = - set_vector_start_to_length - (Replicate (N',reset_vector_start (set_vector_start_to_length (Vector [B1] 0 false)))) - -let SignExtend (N', ((Vector (h::_) _ _) as x)) = - let remainder = slice_raw x (1:ii) ((length (reset_vector_start x)) - (1:ii)) in - set_vector_start_to_length - ((set_vector_start_to_length - (set_vector_start_to_length - (Replicate - (N' - (length x), - reset_vector_start (set_vector_start_to_length (Vector [h] 0 false)))))) ^^ - (set_vector_start_to_length x)) - -let supported_instructions instr = match instr with | _ -> Just instr end - -let LSL (x, shift) = - let result = set_vector_start_to_length (to_vec_dec (length x,(0:ii))) in - if bitU_to_bool (eq_range (shift, (0:ii))) - then set_vector_start_to_length x - else - let (result', _) = - match (LSL_C (reset_vector_start (set_vector_start_to_length x),shift)) with - | (v0v', v1v') -> (v0v',v1v') - end in - set_vector_start_to_length result' - -let ThisInstrAddr N' = - let N = length (reset_vector_start (set_vector_start_to_length (to_vec_dec (N',(0:ii))))) in - let _ = - assert' ((eq_range (N, (64:ii))) |. ((eq_range (N, (32:ii))) &. (UsingAArch32 ()))) (Nothing) in - rPC () >>= fun w__0 -> - return (set_vector_start_to_length - (mask (N',reset_vector_start (set_vector_start_to_length w__0)))) - -let AArch64_Abort (vaddress, fault) = not_implemented "AArch64_Abort" - -let rV (N', n) = - read_reg (access _V n) >>= fun w__0 -> - return (set_vector_start_to_length - (mask (N',reset_vector_start (set_vector_start_to_length w__0)))) - -let rVpart (N', n, part) = - if bitU_to_bool (eq_range (part, (0:ii))) - then - read_reg (access _V n) >>= fun w__0 -> - return (set_vector_start_to_length - (set_vector_start_to_length (mask (N',reset_vector_start (set_vector_start_to_length w__0))))) - else - let _ = - assert' (eq_range - (length (reset_vector_start (set_vector_start_to_length (to_vec_dec (N',(0:ii))))), - (64:ii))) (Nothing) in - read_reg_range (access _V n) (127:ii) (64:ii) >>= fun w__1 -> - return (set_vector_start_to_length (set_vector_start 63 w__1)) - -let ExternalInvasiveDebugEnabled () = - signalDBGEN () >>= fun w__0 -> - return (eq (w__0, HIGH)) - -let Align (x, y) = - set_vector_start_to_length - (to_vec_dec (length x,Align' (UInt (reset_vector_start (set_vector_start_to_length x)),y))) - -let empty_read_buffer = - <| read_buffer_type_size = (0:ii); - read_buffer_type_acctype = AccType_NORMAL; - read_buffer_type_exclusive = B0; - read_buffer_type_address = (to_vec_dec ((64:ii),(0:ii))) |> - -let empty_write_buffer = - <| write_buffer_type_size = (0:ii); - write_buffer_type_acctype = AccType_NORMAL; - write_buffer_type_exclusive = B0; - write_buffer_type_address = (to_vec_dec ((64:ii),(0:ii))); - write_buffer_type_value = (to_vec_dec ((128:ii),(0:ii))) |> - -let HighestELUsingAArch32 () = - if bitU_to_bool (~(HaveAnyAArch32 ())) - then B0 - else IMPLEMENTATION_DEFINED.IMPLEMENTATION_DEFINED_type_HighestELUsingAArch32 - -let rX (N', n) = - if bitU_to_bool (neq_range (n, (31:ii))) - then - read_reg (access _R n) >>= fun w__0 -> - return (set_vector_start_to_length - (mask (N',reset_vector_start (set_vector_start_to_length w__0)))) - else return (set_vector_start_to_length (Zeros N')) - -let rELR' () = - read_reg_field CurrentEL "EL" >>= fun w__0 -> - let _ = - assert' (neq_vec (set_vector_start_to_length w__0, set_vector_start_to_length EL0)) (Nothing) in - read_reg_field CurrentEL "EL" >>= fun w__1 -> - rELR (reset_vector_start (set_vector_start 1 w__1)) - -let rSPIFP = [RFull "SP_EL0";PSTATE_SPfp] - -let wSPFP = ([PSTATE_SPfp],[RFull "SP_EL0"]) - -let xFP n = if bitU_to_bool (neq_range (n, (31:ii))) then [RFull (access _Rs n)] else [] - -let BigEndianIFP = if bitU_to_bool (UsingAArch32 ()) then [RFull "PSTATE_E"] else [PSTATE_ELfp] - -let flush_write_buffer_exclusive write_buffer = - let _ = assert' write_buffer.write_buffer_type_exclusive (Nothing) in - match write_buffer.write_buffer_type_acctype with - | AccType_ATOMIC -> - wMem_Val_ATOMIC - (write_buffer.write_buffer_type_size, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length write_buffer.write_buffer_type_value) - ((write_buffer.write_buffer_type_size * (8:ii)) - (1:ii)) (0:ii)))) - | AccType_ORDERED -> - wMem_Val_ATOMIC - (write_buffer.write_buffer_type_size, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length write_buffer.write_buffer_type_value) - ((write_buffer.write_buffer_type_size * (8:ii)) - (1:ii)) (0:ii)))) - | _ -> - not_implemented "unrecognised memory access" >> - return B0 - end - -let AArch64_CreateFaultRecord (type', ipaddress, level, acctype, write, extflag, secondstage, s2fs1walk) = - <| FaultRecord_type' = type'; - FaultRecord_domain = (to_vec_dec ((4:ii),UNKNOWN)); - FaultRecord_debugmoe = (to_vec_dec ((4:ii),UNKNOWN)); - FaultRecord_ipaddress = ipaddress; - FaultRecord_level = level; - FaultRecord_acctype = acctype; - FaultRecord_write = write; - FaultRecord_extflag = extflag; - FaultRecord_secondstage = secondstage; - FaultRecord_s2fs1walk = s2fs1walk |> - -let flush_write_buffer write_buffer = - let _ = assert' (eq_bit (write_buffer.write_buffer_type_exclusive, B0)) (Nothing) in - match write_buffer.write_buffer_type_acctype with - | AccType_NORMAL -> - wMem_Val_NORMAL - (write_buffer.write_buffer_type_size, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length write_buffer.write_buffer_type_value) - ((write_buffer.write_buffer_type_size * (8:ii)) - (1:ii)) (0:ii)))) - | AccType_STREAM -> - wMem_Val_NORMAL - (write_buffer.write_buffer_type_size, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length write_buffer.write_buffer_type_value) - ((write_buffer.write_buffer_type_size * (8:ii)) - (1:ii)) (0:ii)))) - | AccType_UNPRIV -> - wMem_Val_NORMAL - (write_buffer.write_buffer_type_size, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length write_buffer.write_buffer_type_value) - ((write_buffer.write_buffer_type_size * (8:ii)) - (1:ii)) (0:ii)))) - | AccType_ORDERED -> - wMem_Val_NORMAL - (write_buffer.write_buffer_type_size, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length write_buffer.write_buffer_type_value) - ((write_buffer.write_buffer_type_size * (8:ii)) - (1:ii)) (0:ii)))) - | _ -> not_implemented "unrecognised memory access" - end - -let System_Get (op0, op1, crn, crm, op2) = - match toNaturalFiveTup (op0,op1,crn,crm,op2) with - | ((3:nn), (3:nn), (4:nn), (2:nn), (0:nn)) -> - read_reg NZCV >>= fun w__0 -> - return (ZeroExtend ((64:ii),w__0)) - | ((3:nn), (3:nn), (4:nn), (2:nn), (1:nn)) -> - read_reg DAIF >>= fun w__1 -> - return (ZeroExtend ((64:ii),w__1)) - | ((3:nn), (3:nn), (13:nn), (0:nn), (2:nn)) -> read_reg TPIDR_EL0 - end - -let Prefetch (address, prfop) = - let hint = - match toNatural (0:ii) with - | (0:nn) -> Prefetch_READ - | (1:nn) -> Prefetch_WRITE - | (2:nn) -> Prefetch_EXEC - end in - let target = (0:ii) in - let stream = B0 in - let returnv = B0 in - let (returnv, hint) = - match (slice prfop (4:ii) (3:ii)) with - | Vector [B0;B0] _ _ -> - let hint = Prefetch_READ in - (returnv,hint) - | Vector [B0;B1] _ _ -> - let hint = Prefetch_EXEC in - (returnv,hint) - | Vector [B1;B0] _ _ -> - let hint = Prefetch_WRITE in - (returnv,hint) - | Vector [B1;B1] _ _ -> - let returnv = B1 in - (returnv,hint) - end in - let (target, stream) = - if bitU_to_bool (~returnv) - then - let target = unsigned (reset_vector_start (slice prfop (2:ii) (1:ii))) in - let stream = neq (match (access prfop (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)) in - (target,stream) - else (target,stream) in - () - -let DoubleLockStatus () = - if bitU_to_bool (ELUsingAArch32 (reset_vector_start EL1)) - then - read_reg_bitfield DBGOSDLR "DLK" >>= fun w__0 -> - read_reg_bitfield DBGPRCR "CORENPDRQ" >>= fun w__1 -> - Halted () >>= fun w__2 -> - return ((eq (match w__0 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) &. - ((eq (match w__1 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) &. (~w__2))) - else - read_reg_bitfield OSDLR_EL1 "DLK" >>= fun w__3 -> - read_reg_bitfield DBGPRCR_EL1 "CORENPDRQ" >>= fun w__4 -> - Halted () >>= fun w__5 -> - return ((eq (match w__3 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) &. - ((eq (match w__4 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) &. (~w__5))) - -let wSP ((), value) = - read_reg_bitfield SPSel "SP" >>= fun w__0 -> - if bitU_to_bool (eq (match w__0 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) - then write_reg SP_EL0 (ZeroExtend ((64:ii),reset_vector_start (set_vector_start_to_length value))) - else - read_reg_field CurrentEL "EL" >>= fun pstate_el -> - if bitU_to_bool (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL0)) - then - write_reg SP_EL0 (ZeroExtend ((64:ii),reset_vector_start (set_vector_start_to_length value))) - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL1)) - then - write_reg - SP_EL1 - (ZeroExtend ((64:ii),reset_vector_start (set_vector_start_to_length value))) - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL2)) - then - write_reg - SP_EL2 - (ZeroExtend ((64:ii),reset_vector_start (set_vector_start_to_length value))) - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL3)) - then - write_reg - SP_EL3 - (ZeroExtend ((64:ii),reset_vector_start (set_vector_start_to_length value))) - else return (assert' B0 (Nothing)) - -let decodeTMCommit () = Just (TMCommit) - -let decodeTMTest () = Just (TMTest) - -let decodeTMAbort ((Vector [R;_;_;_;_;_] _ _) as v__975) = - let imm5 = slice_raw v__975 (1:ii) (5:ii) in - Just (TMAbort (R,reset_vector_start imm5)) - -let wV (n, value) = - write_reg - (access _V n) - (ZeroExtend ((128:ii),reset_vector_start (set_vector_start_to_length value))) - -let wVpart (n, part, value) = - if bitU_to_bool (eq_range (part, (0:ii))) - then - write_reg - (access _V n) - (ZeroExtend ((128:ii),reset_vector_start (set_vector_start_to_length value))) - else - let _ = - assert' (eq_range - (length - (reset_vector_start (set_vector_start_to_length - (to_vec_dec (length value,(0:ii))))), - (64:ii))) (Nothing) in - write_reg_range (access _V n) (127:ii) (64:ii) (set_vector_start 127 value) - -let wX (n, value) = - if bitU_to_bool (neq_range (n, (31:ii))) - then - write_reg - (access _R n) - (ZeroExtend ((64:ii),reset_vector_start (set_vector_start_to_length value))) - else return () - -let decodeAdvSIMDLoadStoreMultiStruct machineCode = - not_implemented "decodeAdvSIMDLoadStoreMultiStruct" >> - return (Just (Unallocated)) - -let decodeAdvSIMDLoadStoreMultiStructPostIndexed machineCode = - not_implemented "decodeAdvSIMDLoadStoreMultiStructPostIndexed" >> - return (Just (Unallocated)) - -let decodeAdvSIMDLoadStoreSingleStruct machineCode = - not_implemented "decodeAdvSIMDLoadStoreSingleStruct" >> - return (Just (Unallocated)) - -let decodeAdvSIMDLoadStoreSingleStructPostIndexed machineCode = - not_implemented "decodeAdvSIMDLoadStoreSingleStructPostIndexed" >> - return (Just (Unallocated)) - -let decodeDataSIMDFPoint1 machineCode = - not_implemented "decodeDataSIMDFPoint1" >> - return (Just (Unallocated)) - -let decodeDataSIMDFPoint2 machineCode = - not_implemented "decodeDataSIMDFPoint2" >> - return (Just (Unallocated)) - -let AArch64_CheckForWFxTrap (target_el, is_wfe) = - let _ = assert' (HaveEL (reset_vector_start target_el)) (Nothing) in - let trap = B0 in - (if bitU_to_bool (eq_vec (set_vector_start_to_length target_el, set_vector_start_to_length EL1)) - then - (if bitU_to_bool is_wfe - then - read_reg_bitfield SCTLR_EL1 "nTWE" >>= fun w__0 -> - return (match w__0 with | B0 -> (0:ii) | B1 -> (1:ii) end) - else - read_reg_bitfield SCTLR_EL1 "nTWI" >>= fun w__1 -> - return (match w__1 with | B0 -> (0:ii) | B1 -> (1:ii) end)) >>= fun w__2 -> - let trap = eq (w__2, (0:ii)) in - return trap - else - if bitU_to_bool (eq_vec (set_vector_start_to_length target_el, set_vector_start_to_length EL2)) - then - (if bitU_to_bool is_wfe - then - read_reg_bitfield HCR_EL2 "TWE" >>= fun w__3 -> - return (match w__3 with | B0 -> (0:ii) | B1 -> (1:ii) end) - else - read_reg_bitfield HCR_EL2 "TWI" >>= fun w__4 -> - return (match w__4 with | B0 -> (0:ii) | B1 -> (1:ii) end)) >>= fun w__5 -> - let trap = eq (w__5, (1:ii)) in - return trap - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length target_el, set_vector_start_to_length EL3)) - then - (if bitU_to_bool is_wfe - then - read_reg_bitfield SCR_EL3 "TWE" >>= fun w__6 -> - return (match w__6 with | B0 -> (0:ii) | B1 -> (1:ii) end) - else - read_reg_bitfield SCR_EL3 "TWI" >>= fun w__7 -> - return (match w__7 with | B0 -> (0:ii) | B1 -> (1:ii) end)) >>= fun w__8 -> - let trap = eq (w__8, (1:ii)) in - return trap - else - let _ = assert' B0 (Nothing) in - return trap) >>= fun trap -> - if bitU_to_bool trap - then AArch64_WFxTrap (reset_vector_start target_el,is_wfe) - else return () - -let wmem_kind (acctype, exclusive) = - if bitU_to_bool exclusive - then - match acctype with - | AccType_ATOMIC -> return (IK_mem_write Write_exclusive) - | AccType_ORDERED -> return (IK_mem_write Write_exclusive_release) - | _ -> - not_implemented "unimplemented memory access" >> - return (IK_mem_write Write_exclusive) - end - else - match acctype with - | AccType_NORMAL -> return (IK_mem_write Write_plain) - | AccType_STREAM -> return (IK_mem_write Write_plain) - | AccType_UNPRIV -> return (IK_mem_write Write_plain) - | AccType_ORDERED -> return (IK_mem_write Write_release) - | _ -> - not_implemented "unimplemented memory access" >> - return (IK_mem_write Write_plain) - end - -let BranchTo (target, branch_type) = - let target' = set_vector_start_to_length target in - let _ = Hint_Branch branch_type in - (if bitU_to_bool - (eq_range (length (reset_vector_start (set_vector_start_to_length target)), (32:ii))) - then - let _ = assert' (UsingAArch32 ()) (Nothing) in - write_reg _PC (ZeroExtend ((64:ii),reset_vector_start (set_vector_start_to_length target))) >> - return target' - else - let _ = - assert' ((eq_range (length (reset_vector_start (set_vector_start_to_length target)), (64:ii))) &. - (~(UsingAArch32 ()))) (Nothing) in - read_reg_field CurrentEL "EL" >>= fun pstate_el -> - (if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL0)) - then - read_reg_bitfield TCR_EL1 "TBI1" >>= fun w__0 -> - let target' = - if bitU_to_bool - ((eq - (match (access (set_vector_start_to_length target') (55:ii)) with - | B0 -> (0:ii) - | B1 -> (1:ii) - end, - (1:ii))) &. (eq (match w__0 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))) - then - update - target' (63:ii) (56:ii) - (set_vector_start 63 (Vector [B1;B1;B1;B1;B1;B1;B1;B1] 7 false)) - else target' in - read_reg_bitfield TCR_EL1 "TBI0" >>= fun w__1 -> - let target' = - if bitU_to_bool - ((eq - (match (access (set_vector_start_to_length target') (55:ii)) with - | B0 -> (0:ii) - | B1 -> (1:ii) - end, - (0:ii))) &. (eq (match w__1 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))) - then - update - target' (63:ii) (56:ii) - (set_vector_start 63 (Vector [B0;B0;B0;B0;B0;B0;B0;B0] 7 false)) - else target' in - return target' - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL1)) - then - read_reg_bitfield TCR_EL1 "TBI1" >>= fun w__2 -> - let target' = - if bitU_to_bool - ((eq - (match (access (set_vector_start_to_length target') (55:ii)) with - | B0 -> (0:ii) - | B1 -> (1:ii) - end, - (1:ii))) &. (eq (match w__2 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))) - then - update - target' (63:ii) (56:ii) - (set_vector_start 63 (Vector [B1;B1;B1;B1;B1;B1;B1;B1] 7 false)) - else target' in - read_reg_bitfield TCR_EL1 "TBI0" >>= fun w__3 -> - let target' = - if bitU_to_bool - ((eq - (match (access (set_vector_start_to_length target') (55:ii)) with - | B0 -> (0:ii) - | B1 -> (1:ii) - end, - (0:ii))) &. (eq (match w__3 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))) - then - update - target' (63:ii) (56:ii) - (set_vector_start 63 (Vector [B0;B0;B0;B0;B0;B0;B0;B0] 7 false)) - else target' in - return target' - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL2)) - then - read_reg_bitfield TCR_EL2 "TBI" >>= fun w__4 -> - let target' = - if bitU_to_bool (eq (match w__4 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then - update - target' (63:ii) (56:ii) - (set_vector_start 63 (Vector [B0;B0;B0;B0;B0;B0;B0;B0] 7 false)) - else target' in - return target' - else - if bitU_to_bool - (eq_vec (set_vector_start_to_length pstate_el, set_vector_start_to_length EL3)) - then - read_reg_bitfield TCR_EL3 "TBI" >>= fun w__5 -> - let target' = - if bitU_to_bool (eq (match w__5 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then - update - target' (63:ii) (56:ii) - (set_vector_start 63 (Vector [B0;B0;B0;B0;B0;B0;B0;B0] 7 false)) - else target' in - return target' - else return target') >>= fun target' -> - write_reg _PC target' >> - return target') >>= fun target' -> - return () - -let rmem_kind (acctype, exclusive) = - if bitU_to_bool exclusive - then - match acctype with - | AccType_ATOMIC -> return (IK_mem_read Read_exclusive) - | AccType_ORDERED -> return (IK_mem_read Read_exclusive_acquire) - | _ -> - not_implemented "unimplemented memory access" >> - return (IK_mem_read Read_exclusive) - end - else - return (match acctype with - | AccType_NORMAL -> IK_mem_read Read_plain - | AccType_ATOMIC -> IK_mem_read Read_plain - | AccType_STREAM -> IK_mem_read Read_stream - | AccType_UNPRIV -> IK_mem_read Read_plain - | AccType_ORDERED -> IK_mem_read Read_acquire - end) - -let decodeTMStart Rt = - let t = UInt_reg (reset_vector_start Rt) in - Just (TMStart t) - -let decodeAddSubtractWithCarry ((Vector [sf;op;S;B1;B1;B0;B1;B0;B0;B0;B0;_;_;_;_;_;B0;B0;B0;B0;B0;B0;_;_;_;_;_;_;_;_;_;_] _ _) as v__969) = - let Rm = slice_raw v__969 (11:ii) (15:ii) in - let Rn = slice_raw v__969 (22:ii) (26:ii) in - let Rd = slice_raw v__969 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let sub_op = eq (match op with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let setflags = eq (match S with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - Just (AddSubCarry (d,n,m,datasize,sub_op,setflags)) - -let decodeConditionalCompareRegister ((Vector [sf;op;B1;B1;B1;B0;B1;B0;B0;B1;B0;_;_;_;_;_;_;_;_;_;B0;B0;_;_;_;_;_;B0;_;_;_;_] _ _) as v__961) = - let Rm = slice_raw v__961 (11:ii) (15:ii) in - let _cond = slice_raw v__961 (16:ii) (19:ii) in - let Rn = slice_raw v__961 (22:ii) (26:ii) in - let nzcv = slice_raw v__961 (28:ii) (31:ii) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let sub_op = eq (match op with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let condition = set_vector_start 3 _cond in - let flags = set_vector_start 3 nzcv in - Just (ConditionalCompareRegister (n,m,datasize,sub_op,reset_vector_start condition,reset_vector_start flags)) - -let decodeConditionalSelect ((Vector [sf;op;B0;B1;B1;B0;B1;B0;B1;B0;B0;_;_;_;_;_;_;_;_;_;B0;o2;_;_;_;_;_;_;_;_;_;_] _ _) as v__954) = - let Rm = slice_raw v__954 (11:ii) (15:ii) in - let _cond = slice_raw v__954 (16:ii) (19:ii) in - let Rn = slice_raw v__954 (22:ii) (26:ii) in - let Rd = slice_raw v__954 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let condition = set_vector_start 3 _cond in - let else_inv = eq (match op with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let else_inc = eq (match o2 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - Just (ConditionalSelect (d,n,m,datasize,reset_vector_start condition,else_inv,else_inc)) - -let BranchToFP (iR, oR) = - (if bitU_to_bool (UsingAArch32 ()) - then iR - else PSTATE_ELfp :: iR,_PCfp :: oR) - -let decodeImplementationDefined = function - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B1;B0;B0;B0;B0;B1;B0;B1;B1;B1;_;B1;B1;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;isEnd] _ _) as v__920) -> - Just (ImplementationDefinedTestBeginEnd isEnd) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B1;B0;B0;B0;B0;B1;B0;B1;B1;B1;_;B1;B1;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B1;B0] _ _) as v__932) -> - Just (ImplementationDefinedStopFetching) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B1;B0;B0;B0;B0;B1;B0;B1;B1;B1;_;B1;B1;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;B1;B1] _ _) as v__943) -> - Just (ImplementationDefinedThreadStart) - end - -let NZCVfp = [PSTATE_Vfp;PSTATE_Cfp;PSTATE_Zfp;PSTATE_Nfp] - -let decodeConditionalCompareImmediate ((Vector [sf;op;B1;B1;B1;B0;B1;B0;B0;B1;B0;_;_;_;_;_;_;_;_;_;B1;B0;_;_;_;_;_;B0;_;_;_;_] _ _) as v__912) = - let imm5 = slice_raw v__912 (11:ii) (15:ii) in - let _cond = slice_raw v__912 (16:ii) (19:ii) in - let Rn = slice_raw v__912 (22:ii) (26:ii) in - let nzcv = slice_raw v__912 (28:ii) (31:ii) in - let n = UInt_reg (reset_vector_start Rn) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let sub_op = eq (match op with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let condition = set_vector_start 3 _cond in - let flags = set_vector_start 3 nzcv in - let imm = - set_vector_start_to_length - (ZeroExtend (datasize,reset_vector_start (set_vector_start_to_length imm5))) in - Just (ConditionalCompareImmediate (n,datasize,sub_op,reset_vector_start condition,reset_vector_start flags,reset_vector_start (set_vector_start_to_length - imm))) - -let decodeMoveWideImmediate ((Vector [sf;_;_;B1;B0;B0;B1;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__909) = - let opc = slice_raw v__909 (1:ii) (2:ii) in - let hw = slice_raw v__909 (9:ii) (10:ii) in - let imm16 = slice_raw v__909 (11:ii) (26:ii) in - let Rd = slice_raw v__909 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let imm = imm16 in - let pos = (0:ii) in - let opcode = - match toNatural (0:ii) with - | (0:nn) -> MoveWideOp_N - | (1:nn) -> MoveWideOp_Z - | (2:nn) -> MoveWideOp_K - end in - match opc with - | Vector [B0;B0] _ _ -> return MoveWideOp_N - | Vector [B1;B0] _ _ -> return MoveWideOp_Z - | Vector [B1;B1] _ _ -> return MoveWideOp_K - | _ -> - UnallocatedEncoding () >> - return opcode - end >>= fun opcode -> - (if bitU_to_bool - ((eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) &. - (eq (match (access hw (1:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))) - then UnallocatedEncoding () - else return ()) >> - let pos = - UInt - (reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length hw) ^^ - (set_vector_start_to_length (Vector [B0;B0;B0;B0] 3 false))))) in - return (Just (MoveWide (d,datasize,reset_vector_start imm,pos,opcode))) - -let decodeLoadStoreExclusive ((Vector [_;_;B0;B0;B1;B0;B0;B0;o2;L;o1;_;_;_;_;_;o0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__903) = - let size = slice_raw v__903 (0:ii) (1:ii) in - let Rs = slice_raw v__903 (11:ii) (15:ii) in - let Rt2 = slice_raw v__903 (17:ii) (21:ii) in - let Rn = slice_raw v__903 (22:ii) (26:ii) in - let Rt = slice_raw v__903 (27:ii) (31:ii) in - let n = UInt_reg (reset_vector_start Rn) in - let t = UInt_reg (reset_vector_start Rt) in - let t2 = UInt_reg (reset_vector_start Rt2) in - let s = UInt_reg (reset_vector_start Rs) in - (if bitU_to_bool - ((eq_vec - (set_vector_start_to_length (Vector [o2;o1;o0] 2 false), - set_vector_start_to_length (Vector [B1;B0;B0] 2 false))) |. - (eq_vec - (set_vector_start_to_length (Vector [o2;o1] 1 false), - set_vector_start_to_length (Vector [B1;B1] 1 false)))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool - ((eq (match o1 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) &. - (eq (match (access size (1:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)))) - then UnallocatedEncoding () - else return ()) >> - let acctype = - if bitU_to_bool (eq (match o0 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then AccType_ORDERED - else AccType_ATOMIC in - let excl = eq (match o2 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)) in - let pair = eq (match o1 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let memop = - if bitU_to_bool (eq (match L with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then MemOp_LOAD - else MemOp_STORE in - let elsize = lsl' ((8:ii),UInt (reset_vector_start (set_vector_start_to_length size))) in - let regsize = if bitU_to_bool (eq_range (elsize, (64:ii))) then (64:ii) else (32:ii) in - let datasize = if bitU_to_bool pair then elsize * (2:ii) else elsize in - return (Just (LoadStoreAcqExc (n,t,t2,s,acctype,excl,pair,memop,elsize,regsize,datasize))) - -let sharedDecodeLoadImmediate (opc, size, Rn, Rt, wback, postindex, scale, offset, acctype, prefetchAllowed) = - let n = UInt_reg Rn in - let t = UInt_reg Rt in - let memop = - match toNatural (0:ii) with - | (0:nn) -> MemOp_LOAD - | (1:nn) -> MemOp_STORE - | (2:nn) -> MemOp_PREFETCH - end in - let _signed = B0 in - let regsize = (64:ii) in - (if bitU_to_bool (eq (match (access opc (1:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) - then - let memop = - if bitU_to_bool - (eq (match (access opc (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then MemOp_LOAD - else MemOp_STORE in - let regsize = - if bitU_to_bool - (eq_vec - (set_vector_start_to_length size, - set_vector_start_to_length (Vector [B1;B1] 1 false))) - then (64:ii) - else (32:ii) in - let _signed = B0 in - return (memop,regsize,_signed) - else - (if bitU_to_bool - (eq_vec - (set_vector_start_to_length size, - set_vector_start_to_length (Vector [B1;B1] 1 false))) - then - (if bitU_to_bool prefetchAllowed - then - let memop = MemOp_PREFETCH in - (if bitU_to_bool - (eq (match (access opc (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then UnallocatedEncoding () - else return ()) >> - return memop - else - UnallocatedEncoding () >> - return memop) >>= fun memop -> - return (regsize,_signed,memop) - else - let memop = MemOp_LOAD in - (if bitU_to_bool - ((eq_vec - (set_vector_start_to_length size, - set_vector_start_to_length (Vector [B1;B0] 1 false))) &. - (eq (match (access opc (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))) - then UnallocatedEncoding () - else return ()) >> - let regsize = - if bitU_to_bool - (eq (match (access opc (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (32:ii) - else (64:ii) in - let _signed = B1 in - return (regsize,_signed,memop)) >>= fun (regsize, _signed, memop) -> - return (memop,regsize,_signed)) >>= fun (memop, regsize, _signed) -> - let datasize = lsl' ((8:ii),scale) in - return (Just (LoadImmediate (n,t,acctype,memop,_signed,wback,postindex,reset_vector_start offset,regsize,datasize))) - -let sharedDecodeLoadRegister (Rn, Rt, Rm, opc, size, wback, postindex, scale, extend_type, shift) = - let n = UInt_reg Rn in - let t = UInt_reg Rt in - let m = UInt_reg Rm in - let acctype = AccType_NORMAL in - let memop = - match toNatural (0:ii) with - | (0:nn) -> MemOp_LOAD - | (1:nn) -> MemOp_STORE - | (2:nn) -> MemOp_PREFETCH - end in - let _signed = B0 in - let regsize = (64:ii) in - (if bitU_to_bool (eq (match (access opc (1:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) - then - let memop = - if bitU_to_bool - (eq (match (access opc (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then MemOp_LOAD - else MemOp_STORE in - let regsize = - if bitU_to_bool - (eq_vec - (set_vector_start_to_length size, - set_vector_start_to_length (Vector [B1;B1] 1 false))) - then (64:ii) - else (32:ii) in - let _signed = B0 in - return (memop,regsize,_signed) - else - (if bitU_to_bool - (eq_vec - (set_vector_start_to_length size, - set_vector_start_to_length (Vector [B1;B1] 1 false))) - then - let memop = MemOp_PREFETCH in - (if bitU_to_bool - (eq (match (access opc (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then UnallocatedEncoding () - else return ()) >> - return (regsize,_signed,memop) - else - let memop = MemOp_LOAD in - (if bitU_to_bool - ((eq_vec - (set_vector_start_to_length size, - set_vector_start_to_length (Vector [B1;B0] 1 false))) &. - (eq (match (access opc (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))) - then UnallocatedEncoding () - else return ()) >> - let regsize = - if bitU_to_bool - (eq (match (access opc (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (32:ii) - else (64:ii) in - let _signed = B1 in - return (regsize,_signed,memop)) >>= fun (regsize, _signed, memop) -> - return (memop,regsize,_signed)) >>= fun (memop, regsize, _signed) -> - let datasize = lsl' ((8:ii),scale) in - return (Just (LoadRegister (n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize,datasize))) - -let ConditionHoldsIFP _cond = - match (slice _cond (3:ii) (1:ii)) with - | Vector [B0;B0;B0] _ _ -> [PSTATE_Zfp] - | Vector [B0;B0;B1] _ _ -> [PSTATE_Cfp] - | Vector [B0;B1;B0] _ _ -> [PSTATE_Nfp] - | Vector [B0;B1;B1] _ _ -> [PSTATE_Vfp] - | Vector [B1;B0;B0] _ _ -> [PSTATE_Zfp;PSTATE_Cfp] - | Vector [B1;B0;B1] _ _ -> [PSTATE_Vfp;PSTATE_Nfp] - | Vector [B1;B1;B0] _ _ -> [PSTATE_Zfp;PSTATE_Vfp;PSTATE_Nfp] - | Vector [B1;B1;B1] _ _ -> [] - end - -let decodeAddSubtractImmediate ((Vector [sf;op;S;B1;B0;B0;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__898) = - let shift = slice_raw v__898 (8:ii) (9:ii) in - let imm12 = slice_raw v__898 (10:ii) (21:ii) in - let Rn = slice_raw v__898 (22:ii) (26:ii) in - let Rd = slice_raw v__898 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let sub_op = eq (match op with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let setflags = eq (match S with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let imm = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - match shift with - | Vector [B0;B0] _ _ -> - let imm = - set_vector_start_to_length - (ZeroExtend (datasize,reset_vector_start (set_vector_start_to_length imm12))) in - return imm - | Vector [B0;B1] _ _ -> - let imm = - set_vector_start_to_length - (ZeroExtend - (datasize, - reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length imm12) ^^ - (set_vector_start_to_length - (duplicate_bits (set_vector_start_to_length (Vector [B0] 0 false), (12:ii)))))))) in - return imm - | Vector [B1;_] _ _ -> - ReservedValue () >> - return imm - end >>= fun imm -> - return (Just (AddSubImmediate (d,n,datasize,sub_op,setflags,reset_vector_start (set_vector_start_to_length - imm)))) - -let decodeData3Source = function - | ((Vector [sf;B0;B0;B1;B1;B0;B1;B1;B0;B0;B0;_;_;_;_;_;o0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__878) -> - let Rm = slice_raw v__878 (11:ii) (15:ii) in - let Ra = slice_raw v__878 (17:ii) (21:ii) in - let Rn = slice_raw v__878 (22:ii) (26:ii) in - let Rd = slice_raw v__878 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let a = UInt_reg (reset_vector_start Ra) in - let destsize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let datasize = destsize in - let sub_op = eq (match o0 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - Just (MultiplyAddSub (d,n,m,a,destsize,datasize,sub_op)) - | ((Vector [B1;B0;B0;B1;B1;B0;B1;B1;U;B0;B1;_;_;_;_;_;o0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__884) -> - let Rm = slice_raw v__884 (11:ii) (15:ii) in - let Ra = slice_raw v__884 (17:ii) (21:ii) in - let Rn = slice_raw v__884 (22:ii) (26:ii) in - let Rd = slice_raw v__884 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let a = UInt_reg (reset_vector_start Ra) in - let destsize = (64:ii) in - let datasize = (32:ii) in - let sub_op = eq (match o0 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let _unsigned = eq (match U with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - Just (MultiplyAddSubLong (d,n,m,a,destsize,datasize,sub_op,_unsigned)) - | ((Vector [B1;B0;B0;B1;B1;B0;B1;B1;U;B1;B0;_;_;_;_;_;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__891) -> - let Rm = slice_raw v__891 (11:ii) (15:ii) in - let Ra = slice_raw v__891 (17:ii) (21:ii) in - let Rn = slice_raw v__891 (22:ii) (26:ii) in - let Rd = slice_raw v__891 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let a = UInt_reg (reset_vector_start Ra) in - let destsize = (64:ii) in - let datasize = destsize in - let _unsigned = eq (match U with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - Just (MultiplyHigh (d,n,m,a,destsize,datasize,_unsigned)) - end - -let decodeExtract ((Vector [sf;B0;B0;B1;B0;B0;B1;B1;B1;N;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__872) = - let Rm = slice_raw v__872 (11:ii) (15:ii) in - let imms = slice_raw v__872 (16:ii) (21:ii) in - let Rn = slice_raw v__872 (22:ii) (26:ii) in - let Rd = slice_raw v__872 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let lsb = (0:ii) in - (if bitU_to_bool (neq_bit (N, sf)) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool - ((eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) &. - (eq (match (access imms (5:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))) - then ReservedValue () - else return ()) >> - let lsb = UInt (reset_vector_start (set_vector_start_to_length imms)) in - return (Just (ExtractRegister (d,n,m,datasize,lsb))) - -let decodeAddSubtractExtendedRegister ((Vector [sf;op;S;B0;B1;B0;B1;B1;B0;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__865) = - let Rm = slice_raw v__865 (11:ii) (15:ii) in - let option_v = slice_raw v__865 (16:ii) (18:ii) in - let imm3 = slice_raw v__865 (19:ii) (21:ii) in - let Rn = slice_raw v__865 (22:ii) (26:ii) in - let Rd = slice_raw v__865 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let sub_op = eq (match op with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let setflags = eq (match S with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let extend_type = DecodeRegExtend (reset_vector_start (set_vector_start 2 option_v)) in - let shift = UInt (reset_vector_start (set_vector_start_to_length imm3)) in - (if bitU_to_bool (gt (shift, (4:ii))) - then ReservedValue () - else return ()) >> - return (Just (AddSubExtendRegister (d,n,m,datasize,sub_op,setflags,extend_type,shift))) - -let decodeAddSubtractShiftedRegister ((Vector [sf;op;S;B0;B1;B0;B1;B1;_;_;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__859) = - let shift = slice_raw v__859 (8:ii) (9:ii) in - let Rm = slice_raw v__859 (11:ii) (15:ii) in - let imm6 = slice_raw v__859 (16:ii) (21:ii) in - let Rn = slice_raw v__859 (22:ii) (26:ii) in - let Rd = slice_raw v__859 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let sub_op = eq (match op with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let setflags = eq (match S with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - (if bitU_to_bool - (eq_vec - (set_vector_start_to_length shift, - set_vector_start_to_length (Vector [B1;B1] 1 false))) - then ReservedValue () - else return ()) >> - (if bitU_to_bool - ((eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) &. - (eq (match (access imm6 (5:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))) - then ReservedValue () - else return ()) >> - let shift_type = DecodeShift (reset_vector_start (set_vector_start 1 shift)) in - let shift_amount = UInt (reset_vector_start (set_vector_start_to_length imm6)) in - return (Just (AddSubShiftedRegister (d,n,m,datasize,sub_op,setflags,shift_type,shift_amount))) - -let decodeLogicalShiftedRegister ((Vector [sf;_;_;B0;B1;B0;B1;B0;_;_;N;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__855) = - let opc = slice_raw v__855 (1:ii) (2:ii) in - let shift = slice_raw v__855 (8:ii) (9:ii) in - let Rm = slice_raw v__855 (11:ii) (15:ii) in - let imm6 = slice_raw v__855 (16:ii) (21:ii) in - let Rn = slice_raw v__855 (22:ii) (26:ii) in - let Rd = slice_raw v__855 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let setflags = B0 in - let op = LogicalOp_AND in - let (op, setflags) = - match opc with - | Vector [B0;B0] _ _ -> - let op = LogicalOp_AND in - let setflags = B0 in - (op,setflags) - | Vector [B0;B1] _ _ -> - let op = LogicalOp_ORR in - let setflags = B0 in - (op,setflags) - | Vector [B1;B0] _ _ -> - let op = LogicalOp_EOR in - let setflags = B0 in - (op,setflags) - | Vector [B1;B1] _ _ -> - let op = LogicalOp_AND in - let setflags = B1 in - (op,setflags) - end in - (if bitU_to_bool - ((eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) &. - (eq (match (access imm6 (5:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))) - then ReservedValue () - else return ()) >> - let shift_type = DecodeShift (reset_vector_start (set_vector_start 1 shift)) in - let shift_amount = UInt (reset_vector_start (set_vector_start_to_length imm6)) in - let invert = eq (match N with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - return (Just (LogicalShiftedRegister (d,n,m,datasize,setflags,op,shift_type,shift_amount,invert))) - -let decodeData1Source = function - | ((Vector [sf;B1;B0;B1;B1;B0;B1;B0;B1;B1;B0;B0;B0;B0;B0;B0;B0;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__840) -> - let opc = slice_raw v__840 (20:ii) (21:ii) in - let Rn = slice_raw v__840 (22:ii) (26:ii) in - let Rd = slice_raw v__840 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let op = - match toNatural (0:ii) with - | (0:nn) -> RevOp_RBIT - | (1:nn) -> RevOp_REV16 - | (2:nn) -> RevOp_REV32 - | (3:nn) -> RevOp_REV64 - end in - match opc with - | Vector [B0;B0] _ _ -> return RevOp_RBIT - | Vector [B0;B1] _ _ -> return RevOp_REV16 - | Vector [B1;B0] _ _ -> return RevOp_REV32 - | Vector [B1;B1] _ _ -> - (if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) - then UnallocatedEncoding () - else return ()) >> - return RevOp_REV64 - end >>= fun op -> - return (Just (Reverse (d,n,datasize,op))) - | ((Vector [sf;B1;B0;B1;B1;B0;B1;B0;B1;B1;B0;B0;B0;B0;B0;B0;B0;B0;B0;B1;B0;op;_;_;_;_;_;_;_;_;_;_] _ _) as v__847) -> - let Rn = slice_raw v__847 (22:ii) (26:ii) in - let Rd = slice_raw v__847 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let opcode = - if bitU_to_bool (eq (match op with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) - then CountOp_CLZ - else CountOp_CLS in - return (Just (CountLeading (d,n,datasize,opcode))) - end - -let decodeUnconditionalBranchRegister = function - | ((Vector [B1;B1;B0;B1;B0;B1;B1;B0;B0;_;_;B1;B1;B1;B1;B1;B0;B0;B0;B0;B0;B0;_;_;_;_;_;B0;B0;B0;B0;B0] _ _) as v__820) -> - let op = slice_raw v__820 (9:ii) (10:ii) in - let Rn = slice_raw v__820 (22:ii) (26:ii) in - let n = UInt_reg (reset_vector_start Rn) in - let branch_type = - match toNatural (0:ii) with - | (0:nn) -> BranchType_CALL - | (1:nn) -> BranchType_ERET - | (2:nn) -> BranchType_DBGEXIT - | (3:nn) -> BranchType_RET - | (4:nn) -> BranchType_JMP - | (5:nn) -> BranchType_EXCEPTION - | (6:nn) -> BranchType_UNKNOWN - end in - match op with - | Vector [B0;B0] _ _ -> return BranchType_JMP - | Vector [B0;B1] _ _ -> return BranchType_CALL - | Vector [B1;B0] _ _ -> return BranchType_RET - | _ -> - UnallocatedEncoding () >> - return branch_type - end >>= fun branch_type -> - return (Just (BranchRegister (n,branch_type))) - | ((Vector [B1;B1;B0;B1;B0;B1;B1;B0;B1;B0;B0;B1;B1;B1;B1;B1;B0;B0;B0;B0;B0;B0;B1;B1;B1;B1;B1;B0;B0;B0;B0;B0] _ _) as v__826) -> - return (Just (ExceptionReturn)) - | ((Vector [B1;B1;B0;B1;B0;B1;B1;B0;B1;B0;B1;B1;B1;B1;B1;B1;B0;B0;B0;B0;B0;B0;B1;B1;B1;B1;B1;B0;B0;B0;B0;B0] _ _) as v__833) -> - return (Just (DebugRestorePState)) - end - -let decodeData2Source = function - | ((Vector [sf;B0;B0;B1;B1;B0;B1;B0;B1;B1;B0;_;_;_;_;_;B0;B0;B0;B0;B1;o1;_;_;_;_;_;_;_;_;_;_] _ _) as v__800) -> - let Rm = slice_raw v__800 (11:ii) (15:ii) in - let Rn = slice_raw v__800 (22:ii) (26:ii) in - let Rd = slice_raw v__800 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let _unsigned = eq (match o1 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)) in - return (Just (Division (d,n,m,datasize,_unsigned))) - | ((Vector [sf;B0;B0;B1;B1;B0;B1;B0;B1;B1;B0;_;_;_;_;_;B0;B0;B1;B0;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__807) -> - let Rm = slice_raw v__807 (11:ii) (15:ii) in - let op2 = slice_raw v__807 (20:ii) (21:ii) in - let Rn = slice_raw v__807 (22:ii) (26:ii) in - let Rd = slice_raw v__807 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let shift_type = DecodeShift (reset_vector_start (set_vector_start 1 op2)) in - return (Just (Shift (d,n,m,datasize,shift_type))) - | ((Vector [sf;B0;B0;B1;B1;B0;B1;B0;B1;B1;B0;_;_;_;_;_;B0;B1;B0;C;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__813) -> - let Rm = slice_raw v__813 (11:ii) (15:ii) in - let sz = slice_raw v__813 (20:ii) (21:ii) in - let Rn = slice_raw v__813 (22:ii) (26:ii) in - let Rd = slice_raw v__813 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let m = UInt_reg (reset_vector_start Rm) in - (if bitU_to_bool - ((eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) &. - (neq_vec - (set_vector_start_to_length sz, - set_vector_start_to_length (Vector [B1;B1] 1 false)))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool - ((eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) &. - (eq_vec - (set_vector_start_to_length sz, - set_vector_start_to_length (Vector [B1;B1] 1 false)))) - then UnallocatedEncoding () - else return ()) >> - let size = lsl' ((8:ii),UInt (reset_vector_start (set_vector_start_to_length sz))) in - let crc32c = eq (match C with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - return (Just (CRC (d,n,m,size,crc32c))) - end - -let decodeExceptionGeneration = function - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B0;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;B0;B0;B0;B0;B1] _ _) as v__771) -> - let imm16 = slice_raw v__771 (11:ii) (26:ii) in - let imm = imm16 in - return (Just (GenerateExceptionEL1 (reset_vector_start imm))) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B0;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;B0;B0;B0;B1;B0] _ _) as v__776) -> - let imm16 = slice_raw v__776 (11:ii) (26:ii) in - let imm = imm16 in - return (Just (GenerateExceptionEL2 (reset_vector_start imm))) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B0;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;B0;B0;B0;B1;B1] _ _) as v__781) -> - let imm16 = slice_raw v__781 (11:ii) (26:ii) in - let imm = imm16 in - return (Just (GenerateExceptionEL3 (reset_vector_start imm))) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B0;B0;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;B0;B0;B0;B0;B0] _ _) as v__786) -> - let imm16 = slice_raw v__786 (11:ii) (26:ii) in - let comment = imm16 in - return (Just (DebugBreakpoint (reset_vector_start comment))) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B0;B0;B1;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;B0;B0;B0;B0;B0] _ _) as v__791) -> - let imm16 = slice_raw v__791 (11:ii) (26:ii) in - return (Just (ExternalDebugBreakpoint)) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B0;B1;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;B0;B0;B0;_;_] _ _) as v__796) -> - let imm16 = slice_raw v__796 (11:ii) (26:ii) in - let LL = slice_raw v__796 (30:ii) (31:ii) in - let target_level = LL in - (if bitU_to_bool - (eq_vec - (set_vector_start_to_length LL, - set_vector_start_to_length (Vector [B0;B0] 1 false))) - then UnallocatedEncoding () - else return ()) >> - return (Just (DebugSwitchToExceptionLevel (reset_vector_start target_level))) - end - -let decodeSystem = function - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B1;B0;B0;B0;B0;B0;_;_;_;B0;B1;B0;B0;_;_;_;_;_;_;_;B1;B1;B1;B1;B1] _ _) as v__706) -> - let op1 = slice_raw v__706 (13:ii) (15:ii) in - let CRm = slice_raw v__706 (20:ii) (23:ii) in - let op2 = slice_raw v__706 (24:ii) (26:ii) in - let operand = set_vector_start 3 CRm in - let field' = - match toNatural (0:ii) with - | (0:nn) -> PSTATEField_DAIFSet - | (1:nn) -> PSTATEField_DAIFClr - | (2:nn) -> PSTATEField_SP - end in - match ((set_vector_start_to_length op1) ^^ (set_vector_start_to_length op2)) with - | ((Vector [B0;B0;B0;B1;B0;B1] _ _) as v__712) -> return PSTATEField_SP - | ((Vector [B0;B1;B1;B1;B1;B0] _ _) as v__715) -> return PSTATEField_DAIFSet - | ((Vector [B0;B1;B1;B1;B1;B1] _ _) as v__718) -> return PSTATEField_DAIFClr - | _ -> - UnallocatedEncoding () >> - return field' - end >>= fun field' -> - return (Just (MoveSystemImmediate (reset_vector_start operand,field'))) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B1;B0;B0;B0;B0;B0;B0;B1;B1;B0;B0;B1;B0;_;_;_;_;_;_;_;B1;B1;B1;B1;B1] _ _) as v__721) -> - let CRm = slice_raw v__721 (20:ii) (23:ii) in - let op2 = slice_raw v__721 (24:ii) (26:ii) in - let op = - match toNatural (0:ii) with - | (0:nn) -> SystemHintOp_NOP - | (1:nn) -> SystemHintOp_YIELD - | (2:nn) -> SystemHintOp_WFE - | (3:nn) -> SystemHintOp_WFI - | (4:nn) -> SystemHintOp_SEV - | (5:nn) -> SystemHintOp_SEVL - end in - let op = - match ((set_vector_start_to_length CRm) ^^ (set_vector_start_to_length op2)) with - | ((Vector [B0;B0;B0;B0;B0;B0;B0] _ _) as v__728) -> SystemHintOp_NOP - | ((Vector [B0;B0;B0;B0;B0;B0;B1] _ _) as v__731) -> SystemHintOp_YIELD - | ((Vector [B0;B0;B0;B0;B0;B1;B0] _ _) as v__734) -> SystemHintOp_WFE - | ((Vector [B0;B0;B0;B0;B0;B1;B1] _ _) as v__737) -> SystemHintOp_WFI - | ((Vector [B0;B0;B0;B0;B1;B0;B0] _ _) as v__740) -> SystemHintOp_SEV - | ((Vector [B0;B0;B0;B0;B1;B0;B1] _ _) as v__743) -> SystemHintOp_SEVL - | _ -> SystemHintOp_NOP - end in - return (Just (Hint op)) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B1;B0;B0;B0;B0;B0;B0;B1;B1;B0;B0;B1;B1;_;_;_;_;B0;B1;B0;B1;B1;B1;B1;B1] _ _) as v__746) -> - let CRm = slice_raw v__746 (20:ii) (23:ii) in - let imm = unsigned (reset_vector_start CRm) in - return (Just (ClearExclusiveMonitor imm)) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B1;B0;B0;B0;B0;B0;B0;B1;B1;B0;B0;B1;B1;_;_;_;_;B1;_;_;B1;B1;B1;B1;B1] _ _) as v__754) -> - let CRm = slice_raw v__754 (20:ii) (23:ii) in - let opc = slice_raw v__754 (25:ii) (26:ii) in - let op = - match toNatural (0:ii) with - | (0:nn) -> MemBarrierOp_DSB - | (1:nn) -> MemBarrierOp_DMB - | (2:nn) -> MemBarrierOp_ISB - end in - let domain = - match toNatural (0:ii) with - | (0:nn) -> MBReqDomain_Nonshareable - | (1:nn) -> MBReqDomain_InnerShareable - | (2:nn) -> MBReqDomain_OuterShareable - | (3:nn) -> MBReqDomain_FullSystem - end in - let types = - match toNatural (0:ii) with - | (0:nn) -> MBReqTypes_Reads - | (1:nn) -> MBReqTypes_Writes - | (2:nn) -> MBReqTypes_All - end in - match opc with - | Vector [B0;B0] _ _ -> return MemBarrierOp_DSB - | Vector [B0;B1] _ _ -> return MemBarrierOp_DMB - | Vector [B1;B0] _ _ -> return MemBarrierOp_ISB - | _ -> - UnallocatedEncoding () >> - return op - end >>= fun op -> - let domain = - match (slice CRm (3:ii) (2:ii)) with - | Vector [B0;B0] _ _ -> MBReqDomain_OuterShareable - | Vector [B0;B1] _ _ -> MBReqDomain_Nonshareable - | Vector [B1;B0] _ _ -> MBReqDomain_InnerShareable - | Vector [B1;B1] _ _ -> MBReqDomain_FullSystem - end in - let (domain, types) = - match (slice CRm (1:ii) (0:ii)) with - | Vector [B0;B1] _ _ -> - let types = MBReqTypes_Reads in - (domain,types) - | Vector [B1;B0] _ _ -> - let types = MBReqTypes_Writes in - (domain,types) - | Vector [B1;B1] _ _ -> - let types = MBReqTypes_All in - (domain,types) - | _ -> - let types = MBReqTypes_All in - let domain = MBReqDomain_FullSystem in - (domain,types) - end in - return (Just (Barrier (op,domain,types))) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B1;B0;B0;L;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__762) -> - let op1 = slice_raw v__762 (13:ii) (15:ii) in - let CRn = slice_raw v__762 (16:ii) (19:ii) in - let CRm = slice_raw v__762 (20:ii) (23:ii) in - let op2 = slice_raw v__762 (24:ii) (26:ii) in - let Rt = slice_raw v__762 (27:ii) (31:ii) in - let t = UInt_reg (reset_vector_start Rt) in - let sys_op0 = (1:ii) in - let sys_op1 = UInt (reset_vector_start (set_vector_start_to_length op1)) in - let sys_op2 = UInt (reset_vector_start (set_vector_start_to_length op2)) in - let sys_crn = UInt (reset_vector_start (set_vector_start_to_length CRn)) in - let sys_crm = UInt (reset_vector_start (set_vector_start_to_length CRm)) in - let has_result = eq (match L with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - return (Just (System (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result))) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B1;B0;B0;L;B1;o0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__766) -> - let op1 = slice_raw v__766 (13:ii) (15:ii) in - let CRn = slice_raw v__766 (16:ii) (19:ii) in - let CRm = slice_raw v__766 (20:ii) (23:ii) in - let op2 = slice_raw v__766 (24:ii) (26:ii) in - let Rt = slice_raw v__766 (27:ii) (31:ii) in - let t = UInt_reg (reset_vector_start Rt) in - let sys_op0 = - (2:ii) + (UInt (reset_vector_start (set_vector_start_to_length (Vector [o0] 0 false)))) in - let sys_op1 = UInt (reset_vector_start (set_vector_start_to_length op1)) in - let sys_op2 = UInt (reset_vector_start (set_vector_start_to_length op2)) in - let sys_crn = UInt (reset_vector_start (set_vector_start_to_length CRn)) in - let sys_crm = UInt (reset_vector_start (set_vector_start_to_length CRm)) in - let read = eq (match L with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - return (Just (MoveSystemRegister (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read))) - end - -let ASR_C (x, shift) = - let extended_x = - set_vector_start_to_length - (SignExtend (shift + (length x),reset_vector_start (set_vector_start_to_length x))) in - let result = - set_vector_start_to_length - (slice (set_vector_start_to_length extended_x) - ((shift + (length (reset_vector_start (set_vector_start_to_length x)))) - (1:ii)) shift) in - let carry_out = access (set_vector_start_to_length extended_x) (shift - (1:ii)) in - (set_vector_start_to_length result,carry_out) - -let ASR (x, shift) = - let result = set_vector_start_to_length (to_vec_dec (length x,(0:ii))) in - if bitU_to_bool (eq_range (shift, (0:ii))) - then set_vector_start_to_length x - else - let (result', _) = - match (ASR_C (reset_vector_start (set_vector_start_to_length x),shift)) with - | (v0v', v1v') -> (v0v',v1v') - end in - set_vector_start_to_length result' - -let LSR (x, shift) = - let result = set_vector_start_to_length (to_vec_dec (length x,(0:ii))) in - if bitU_to_bool (eq_range (shift, (0:ii))) - then set_vector_start_to_length x - else - let (result', _) = - match (LSR_C (reset_vector_start (set_vector_start_to_length x),shift)) with - | (v0v', v1v') -> (v0v',v1v') - end in - set_vector_start_to_length result' - -let AArch64_ResetGeneralRegisters () = - (foreachM_inc ((0:ii),(30:ii),(1:ii)) () - (fun i _ -> - wX (i,reset_vector_start (set_vector_start_to_length (to_vec_dec ((64:ii),UNKNOWN)))))) - -let AArch64_ResetSIMDFPRegisters () = - (foreachM_inc ((0:ii),(31:ii),(1:ii)) () - (fun i _ -> - wV (i,reset_vector_start (set_vector_start_to_length (to_vec_dec ((128:ii),UNKNOWN)))))) - -let wMem'IFP = BigEndianIFP - -let IsFault addrdesc = neq (addrdesc.AddressDescriptor_fault.FaultRecord_type', Fault_None) - -let Extend (N', x, unsigned) = - if bitU_to_bool unsigned - then - set_vector_start_to_length (ZeroExtend (N',reset_vector_start (set_vector_start_to_length x))) - else - set_vector_start_to_length (SignExtend (N',reset_vector_start (set_vector_start_to_length x))) - -let _rMem (read_buffer, desc, size, acctype, exclusive) = - if bitU_to_bool (eq_range (read_buffer.read_buffer_type_size, (0:ii))) - then - <| read_buffer_type_acctype = acctype; - read_buffer_type_exclusive = exclusive; - read_buffer_type_address = desc.AddressDescriptor_paddress.FullAddress_physicaladdress; - read_buffer_type_size = size |> - else - let _ = assert' (eq (read_buffer.read_buffer_type_acctype, acctype)) (Nothing) in - let _ = assert' (eq_bit (read_buffer.read_buffer_type_exclusive, exclusive)) (Nothing) in - let _ = - assert' (eq_vec - (set_vector_start_to_length - (set_vector_start 63 - (add_VIV - (reset_vector_start (set_vector_start_to_length - read_buffer.read_buffer_type_address)) - read_buffer.read_buffer_type_size)), - set_vector_start_to_length - desc.AddressDescriptor_paddress.FullAddress_physicaladdress)) (Nothing) in - <|read_buffer with read_buffer_type_size = (read_buffer.read_buffer_type_size + size)|> - -let CheckSPAlignmentIFP = PSTATE_ELfp :: rSPIFP - -let SCR_GEN () = - let _ = assert' (HaveEL (reset_vector_start EL3)) (Nothing) in - if bitU_to_bool (HighestELUsingAArch32 ()) - then SCR - else SCR_EL3 - -let AArch64_AlignmentFault (acctype, iswrite, secondstage) = - let ipaddress = to_vec_dec ((48:ii),UNKNOWN) in - let level = UNKNOWN in - let extflag = if bitU_to_bool (is_one UNKNOWN) then B1 else B0 in - let s2fs1walk = if bitU_to_bool (is_one UNKNOWN) then B1 else B0 in - AArch64_CreateFaultRecord - (Fault_Alignment, - reset_vector_start ipaddress, - level, - acctype, - iswrite, - extflag, - secondstage, - s2fs1walk) - -let AArch64_NoFault () = - let ipaddress = to_vec_dec ((48:ii),UNKNOWN) in - let level = UNKNOWN in - let acctype = AccType_NORMAL in - let iswrite = if bitU_to_bool (is_one UNKNOWN) then B1 else B0 in - let extflag = if bitU_to_bool (is_one UNKNOWN) then B1 else B0 in - let secondstage = B0 in - let s2fs1walk = B0 in - AArch64_CreateFaultRecord - (Fault_None, - reset_vector_start ipaddress, - level, - acctype, - iswrite, - extflag, - secondstage, - s2fs1walk) - -let decodeConditionalBranchImmediate ((Vector [B0;B1;B0;B1;B0;B1;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;B0;_;_;_;_] _ _) as v__702) = - let imm19 = slice_raw v__702 (8:ii) (26:ii) in - let _cond = slice_raw v__702 (28:ii) (31:ii) in - let offset = - SignExtend - ((64:ii), - reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length imm19) ^^ - (set_vector_start_to_length (Vector [B0;B0] 1 false))))) in - let condition = set_vector_start 3 _cond in - Just (BranchConditional (reset_vector_start offset,reset_vector_start condition)) - -let _wMem (write_buffer, desc, size, acctype, exclusive, value) = - if bitU_to_bool (eq_range (write_buffer.write_buffer_type_size, (0:ii))) - then - <| write_buffer_type_acctype = acctype; - write_buffer_type_exclusive = exclusive; - write_buffer_type_address = desc.AddressDescriptor_paddress.FullAddress_physicaladdress; - write_buffer_type_value = - (ZeroExtend ((128:ii),reset_vector_start (set_vector_start_to_length value))); - write_buffer_type_size = size |> - else - let _ = assert' (eq (write_buffer.write_buffer_type_acctype, acctype)) (Nothing) in - let _ = assert' (eq_bit (write_buffer.write_buffer_type_exclusive, exclusive)) (Nothing) in - let _ = - assert' (eq_vec - (set_vector_start_to_length - (set_vector_start 63 - (add_VIV - (reset_vector_start (set_vector_start_to_length - write_buffer.write_buffer_type_address)) - write_buffer.write_buffer_type_size)), - set_vector_start_to_length - desc.AddressDescriptor_paddress.FullAddress_physicaladdress)) (Nothing) in - <|write_buffer with - write_buffer_type_value = - (ZeroExtend - ((128:ii), - reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length value) ^^ - (set_vector_start_to_length - (slice (set_vector_start_to_length write_buffer.write_buffer_type_value) - ((write_buffer.write_buffer_type_size * (8:ii)) - (1:ii)) (0:ii))))))); write_buffer_type_size = - (write_buffer.write_buffer_type_size + size)|> - -let HaveAArch32EL el = - if bitU_to_bool (~(HaveEL (reset_vector_start el))) - then B0 - else - if bitU_to_bool (~(HaveAnyAArch32 ())) - then B0 - else - if bitU_to_bool (HighestELUsingAArch32 ()) - then B1 - else - if bitU_to_bool (eq_vec (set_vector_start_to_length el, set_vector_start_to_length EL0)) - then B1 - else IMPLEMENTATION_DEFINED.IMPLEMENTATION_DEFINED_type_HaveAArch32EL - -let decodeUnconditionalBranchImmediate ((Vector [op;B0;B0;B1;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__699) = - let imm26 = slice_raw v__699 (6:ii) (31:ii) in - let branch_type = - if bitU_to_bool (eq (match op with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then BranchType_CALL - else BranchType_JMP in - let offset = - SignExtend - ((64:ii), - reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length imm26) ^^ - (set_vector_start_to_length (Vector [B0;B0] 1 false))))) in - Just (BranchImmediate (branch_type,reset_vector_start offset)) - -let decodeCompareBranchImmediate ((Vector [sf;B0;B1;B1;B0;B1;B0;op;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__695) = - let imm19 = slice_raw v__695 (8:ii) (26:ii) in - let Rt = slice_raw v__695 (27:ii) (31:ii) in - let t = UInt_reg (reset_vector_start Rt) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let iszero = eq (match op with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)) in - let offset = - SignExtend - ((64:ii), - reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length imm19) ^^ - (set_vector_start_to_length (Vector [B0;B0] 1 false))))) in - Just (CompareAndBranch (t,datasize,iszero,reset_vector_start offset)) - -let decodePCRelAddressing ((Vector [op;_;_;B1;B0;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__692) = - let immlo = slice_raw v__692 (1:ii) (2:ii) in - let immhi = slice_raw v__692 (8:ii) (26:ii) in - let Rd = slice_raw v__692 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let page = eq (match op with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)) in - let imm = to_vec_dec ((64:ii),(0:ii)) in - let imm = - if bitU_to_bool page - then - SignExtend - ((64:ii), - reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length immhi) ^^ - (set_vector_start_to_length - ((set_vector_start_to_length immlo) ^^ - (set_vector_start_to_length - (duplicate_bits (set_vector_start_to_length (Vector [B0] 0 false), (12:ii))))))))) - else - SignExtend - ((64:ii), - reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length immhi) ^^ (set_vector_start_to_length immlo)))) in - Just (Address (d,page,reset_vector_start imm)) - -let decodeTestBranchImmediate ((Vector [b5;B0;B1;B1;B0;B1;B1;op;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__688) = - let b40 = slice_raw v__688 (8:ii) (12:ii) in - let imm14 = slice_raw v__688 (13:ii) (26:ii) in - let Rt = slice_raw v__688 (27:ii) (31:ii) in - let t = UInt_reg (reset_vector_start Rt) in - let datasize = - if bitU_to_bool (eq (match b5 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let bit_pos = - UInt - (reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length (Vector [b5] 0 false)) ^^ (set_vector_start_to_length b40)))) in - let bit_val = op in - let offset = - SignExtend - ((64:ii), - reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length imm14) ^^ - (set_vector_start_to_length (Vector [B0;B0] 1 false))))) in - Just (TestBitAndBranch (t,datasize,bit_pos,bit_val,reset_vector_start offset)) - -let decodeLoadStoreRegisterRegisterOffset ((Vector [_;_;B1;B1;B1;B0;B0;B0;_;_;B1;_;_;_;_;_;_;_;_;S;B1;B0;_;_;_;_;_;_;_;_;_;_] _ _) as v__681) = - let size = slice_raw v__681 (0:ii) (1:ii) in - let opc = slice_raw v__681 (8:ii) (9:ii) in - let Rm = slice_raw v__681 (11:ii) (15:ii) in - let option_v = slice_raw v__681 (16:ii) (18:ii) in - let Rn = slice_raw v__681 (22:ii) (26:ii) in - let Rt = slice_raw v__681 (27:ii) (31:ii) in - let wback = B0 in - let postindex = B0 in - let scale = UInt (reset_vector_start (set_vector_start_to_length size)) in - (if bitU_to_bool - (eq - (match (access (set_vector_start_to_length option_v) (1:ii)) with - | B0 -> (0:ii) - | B1 -> (1:ii) - end, - (0:ii))) - then UnallocatedEncoding () - else return ()) >> - let extend_type = DecodeRegExtend (reset_vector_start (set_vector_start 2 option_v)) in - let shift = - if bitU_to_bool (eq (match S with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then scale - else (0:ii) in - sharedDecodeLoadRegister - (reset_vector_start Rn, - reset_vector_start Rt, - reset_vector_start Rm, - reset_vector_start (set_vector_start 1 opc), - reset_vector_start (set_vector_start 1 size), - wback, - postindex, - scale, - extend_type, - shift) - -let decodeLoadRegisterLiteral ((Vector [_;_;B0;B1;B1;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__677) = - let opc = slice_raw v__677 (0:ii) (1:ii) in - let imm19 = slice_raw v__677 (8:ii) (26:ii) in - let Rt = slice_raw v__677 (27:ii) (31:ii) in - let t = UInt_reg (reset_vector_start Rt) in - let memop = MemOp_LOAD in - let _signed = B0 in - let size = (0:ii) in - let offset = to_vec_dec ((64:ii),(4:ii)) in - let (memop, _signed, size) = - match opc with - | Vector [B0;B0] _ _ -> - let size = (4:ii) in - (memop,_signed,size) - | Vector [B0;B1] _ _ -> - let size = (8:ii) in - (memop,_signed,size) - | Vector [B1;B0] _ _ -> - let size = (4:ii) in - let _signed = B1 in - (memop,_signed,size) - | Vector [B1;B1] _ _ -> - let memop = MemOp_PREFETCH in - (memop,_signed,size) - end in - let offset = - SignExtend - ((64:ii), - reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length imm19) ^^ - (set_vector_start_to_length (Vector [B0;B0] 1 false))))) in - let datasize = size * (8:ii) in - Just (LoadLiteral (t,memop,_signed,size,reset_vector_start offset,datasize)) - -let ROR_C (x, shift) = - let N = length (reset_vector_start (set_vector_start_to_length x)) in - let m = modulo shift N in - let result = - set_vector_start_to_length - (bitwise_or - (set_vector_start_to_length (LSR (reset_vector_start (set_vector_start_to_length x),m)), - set_vector_start_to_length (LSL (reset_vector_start (set_vector_start_to_length x),N - m)))) in - let carry_out = access (set_vector_start_to_length result) (N - (1:ii)) in - (set_vector_start_to_length result,carry_out) - -let decodeSystemImplementationDefined machineCode = - match machineCode with - | ((Vector [_;_;_;_;_;_;_;_;_;_;_;B0;B1;_;_;_;B1;_;B1;B1;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__647) -> - return (decodeImplementationDefined (reset_vector_start machineCode)) - | ((Vector [_;_;_;_;_;_;_;_;_;_;_;B1;B1;_;_;_;B1;_;B1;B1;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__657) -> - return (decodeImplementationDefined (reset_vector_start machineCode)) - | ((Vector [_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__667) -> - decodeSystem (reset_vector_start machineCode) - end - -let decodeLoadStoreRegisterImmediatePostIndexed ((Vector [_;_;B1;B1;B1;B0;B0;B0;_;_;B0;_;_;_;_;_;_;_;_;_;B0;B1;_;_;_;_;_;_;_;_;_;_] _ _) as v__641) = - let size = slice_raw v__641 (0:ii) (1:ii) in - let opc = slice_raw v__641 (8:ii) (9:ii) in - let imm9 = slice_raw v__641 (11:ii) (19:ii) in - let Rn = slice_raw v__641 (22:ii) (26:ii) in - let Rt = slice_raw v__641 (27:ii) (31:ii) in - let wback = B1 in - let postindex = B1 in - let scale = UInt (reset_vector_start (set_vector_start_to_length size)) in - let offset = SignExtend ((64:ii),reset_vector_start (set_vector_start_to_length imm9)) in - sharedDecodeLoadImmediate - (reset_vector_start (set_vector_start 1 opc), - reset_vector_start (set_vector_start 1 size), - reset_vector_start Rn, - reset_vector_start Rt, - wback, - postindex, - scale, - reset_vector_start offset, - AccType_NORMAL, - B0) - -let decodeLoadStoreRegisterImmediatePreIndexed ((Vector [_;_;B1;B1;B1;B0;B0;B0;_;_;B0;_;_;_;_;_;_;_;_;_;B1;B1;_;_;_;_;_;_;_;_;_;_] _ _) as v__635) = - let size = slice_raw v__635 (0:ii) (1:ii) in - let opc = slice_raw v__635 (8:ii) (9:ii) in - let imm9 = slice_raw v__635 (11:ii) (19:ii) in - let Rn = slice_raw v__635 (22:ii) (26:ii) in - let Rt = slice_raw v__635 (27:ii) (31:ii) in - let wback = B1 in - let postindex = B0 in - let scale = UInt (reset_vector_start (set_vector_start_to_length size)) in - let offset = SignExtend ((64:ii),reset_vector_start (set_vector_start_to_length imm9)) in - sharedDecodeLoadImmediate - (reset_vector_start (set_vector_start 1 opc), - reset_vector_start (set_vector_start 1 size), - reset_vector_start Rn, - reset_vector_start Rt, - wback, - postindex, - scale, - reset_vector_start offset, - AccType_NORMAL, - B0) - -let decodeLoadStoreRegisterUnprivileged ((Vector [_;_;B1;B1;B1;B0;B0;B0;_;_;B0;_;_;_;_;_;_;_;_;_;B1;B0;_;_;_;_;_;_;_;_;_;_] _ _) as v__629) = - let size = slice_raw v__629 (0:ii) (1:ii) in - let opc = slice_raw v__629 (8:ii) (9:ii) in - let imm9 = slice_raw v__629 (11:ii) (19:ii) in - let Rn = slice_raw v__629 (22:ii) (26:ii) in - let Rt = slice_raw v__629 (27:ii) (31:ii) in - let wback = B0 in - let postindex = B0 in - let scale = UInt (reset_vector_start (set_vector_start_to_length size)) in - let offset = SignExtend ((64:ii),reset_vector_start (set_vector_start_to_length imm9)) in - sharedDecodeLoadImmediate - (reset_vector_start (set_vector_start 1 opc), - reset_vector_start (set_vector_start 1 size), - reset_vector_start Rn, - reset_vector_start Rt, - wback, - postindex, - scale, - reset_vector_start offset, - AccType_UNPRIV, - B0) - -let decodeLoadStoreRegisterUnscaledImmediate ((Vector [_;_;B1;B1;B1;B0;B0;B0;_;_;B0;_;_;_;_;_;_;_;_;_;B0;B0;_;_;_;_;_;_;_;_;_;_] _ _) as v__623) = - let size = slice_raw v__623 (0:ii) (1:ii) in - let opc = slice_raw v__623 (8:ii) (9:ii) in - let imm9 = slice_raw v__623 (11:ii) (19:ii) in - let Rn = slice_raw v__623 (22:ii) (26:ii) in - let Rt = slice_raw v__623 (27:ii) (31:ii) in - let wback = B0 in - let postindex = B0 in - let scale = UInt (reset_vector_start (set_vector_start_to_length size)) in - let offset = SignExtend ((64:ii),reset_vector_start (set_vector_start_to_length imm9)) in - sharedDecodeLoadImmediate - (reset_vector_start (set_vector_start 1 opc), - reset_vector_start (set_vector_start 1 size), - reset_vector_start Rn, - reset_vector_start Rt, - wback, - postindex, - scale, - reset_vector_start offset, - AccType_NORMAL, - B1) - -let decodeLoadStoreRegisterUnsignedImmediate ((Vector [_;_;B1;B1;B1;B0;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__619) = - let size = slice_raw v__619 (0:ii) (1:ii) in - let opc = slice_raw v__619 (8:ii) (9:ii) in - let imm12 = slice_raw v__619 (10:ii) (21:ii) in - let Rn = slice_raw v__619 (22:ii) (26:ii) in - let Rt = slice_raw v__619 (27:ii) (31:ii) in - let wback = B0 in - let postindex = B0 in - let scale = UInt (reset_vector_start (set_vector_start_to_length size)) in - let offset = - LSL - (reset_vector_start (set_vector_start_to_length - (ZeroExtend ((64:ii),reset_vector_start (set_vector_start_to_length imm12)))), - scale) in - sharedDecodeLoadImmediate - (reset_vector_start (set_vector_start 1 opc), - reset_vector_start (set_vector_start 1 size), - reset_vector_start Rn, - reset_vector_start Rt, - wback, - postindex, - scale, - reset_vector_start offset, - AccType_NORMAL, - B1) - -let decodeLoadStoreNoAllocatePairOffset ((Vector [_;_;B1;B0;B1;B0;B0;B0;B0;L;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__614) = - let opc = slice_raw v__614 (0:ii) (1:ii) in - let imm7 = slice_raw v__614 (10:ii) (16:ii) in - let Rt2 = slice_raw v__614 (17:ii) (21:ii) in - let Rn = slice_raw v__614 (22:ii) (26:ii) in - let Rt = slice_raw v__614 (27:ii) (31:ii) in - let wback = B0 in - let postindex = B0 in - let n = UInt_reg (reset_vector_start Rn) in - let t = UInt_reg (reset_vector_start Rt) in - let t2 = UInt_reg (reset_vector_start Rt2) in - let acctype = AccType_STREAM in - let memop = - if bitU_to_bool (eq (match L with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then MemOp_LOAD - else MemOp_STORE in - (if bitU_to_bool (eq (match (access opc (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then UnallocatedEncoding () - else return ()) >> - let scale = - (2:ii) + - (UInt (reset_vector_start (set_vector_start_to_length (Vector [access opc (1:ii)] 0 false)))) in - let datasize = lsl' ((8:ii),scale) in - let offset = - LSL - (reset_vector_start (set_vector_start_to_length - (SignExtend ((64:ii),reset_vector_start (set_vector_start_to_length imm7)))), - scale) in - return (Just (LoadStorePairNonTemp (wback,postindex,n,t,t2,acctype,memop,scale,datasize,reset_vector_start offset))) - -let sharedDecodeLoadStorePair (L, opc, imm7, Rn, Rt, Rt2, wback, postindex) = - let n = UInt_reg Rn in - let t = UInt_reg Rt in - let t2 = UInt_reg Rt2 in - let acctype = AccType_NORMAL in - let memop = if bitU_to_bool (eq (L, (1:ii))) then MemOp_LOAD else MemOp_STORE in - (if bitU_to_bool - ((eq_vec - (set_vector_start_to_length - (Vector [if bitU_to_bool (is_one L) then B1 else B0;access opc (0:ii)] 1 false), - set_vector_start_to_length (Vector [B0;B1] 1 false))) |. - (eq_vec - (set_vector_start_to_length opc, - set_vector_start_to_length (Vector [B1;B1] 1 false)))) - then UnallocatedEncoding () - else return ()) >> - let _signed = neq (match (access opc (0:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)) in - let scale = - (2:ii) + - (UInt (reset_vector_start (set_vector_start_to_length (Vector [access opc (1:ii)] 0 false)))) in - let datasize = lsl' ((8:ii),scale) in - let offset = - LSL - (reset_vector_start (set_vector_start_to_length (SignExtend ((64:ii),reset_vector_start imm7))), - scale) in - return (Just (LoadStorePair (wback,postindex,n,t,t2,acctype,memop,_signed,datasize,reset_vector_start offset))) - -let decodeDataRegister machineCode = - match machineCode with - | ((Vector [_;_;_;B0;B1;B0;B1;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__484) -> - decodeLogicalShiftedRegister (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;_;B0;B1;B0;B1;B1;_;_;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__497) -> - decodeAddSubtractShiftedRegister (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;_;B0;B1;B0;B1;B1;_;_;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__510) -> - decodeAddSubtractExtendedRegister (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;_;B1;B1;B0;B1;B0;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__523) -> - return (decodeAddSubtractWithCarry - (reset_vector_start (set_vector_start_to_length machineCode))) - | ((Vector [_;_;_;B1;B1;B0;B1;B0;B0;B1;B0;_;_;_;_;_;_;_;_;_;B0;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__536) -> - return (decodeConditionalCompareRegister (reset_vector_start machineCode)) - | ((Vector [_;_;_;B1;B1;B0;B1;B0;B0;B1;B0;_;_;_;_;_;_;_;_;_;B1;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__549) -> - return (decodeConditionalCompareImmediate (reset_vector_start machineCode)) - | ((Vector [_;_;_;B1;B1;B0;B1;B0;B1;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__562) -> - return (decodeConditionalSelect (reset_vector_start machineCode)) - | ((Vector [_;_;_;B1;B1;B0;B1;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__575) -> - return (decodeData3Source (reset_vector_start machineCode)) - | ((Vector [_;B0;_;B1;B1;B0;B1;B0;B1;B1;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__588) -> - decodeData2Source (reset_vector_start machineCode) - | ((Vector [_;B1;_;B1;B1;B0;B1;B0;B1;B1;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__601) -> - decodeData1Source (reset_vector_start machineCode) - end - -let ROR (x, shift) = - let result = set_vector_start_to_length (to_vec_dec (length x,(0:ii))) in - if bitU_to_bool (eq_range (shift, (0:ii))) - then set_vector_start_to_length x - else - let (result', _) = - match (ROR_C (reset_vector_start (set_vector_start_to_length x),shift)) with - | (v0v', v1v') -> (v0v',v1v') - end in - set_vector_start_to_length result' - -let wMemIFP = wMem'IFP - -let decodeLoadStoreRegisterPairOffset ((Vector [_;_;B1;B0;B1;B0;B0;B1;B0;L;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__479) = - let opc = slice_raw v__479 (0:ii) (1:ii) in - let imm7 = slice_raw v__479 (10:ii) (16:ii) in - let Rt2 = slice_raw v__479 (17:ii) (21:ii) in - let Rn = slice_raw v__479 (22:ii) (26:ii) in - let Rt = slice_raw v__479 (27:ii) (31:ii) in - let wback = B0 in - let postindex = B0 in - sharedDecodeLoadStorePair - (match L with | B0 -> (0:ii) | B1 -> (1:ii) end, - reset_vector_start (set_vector_start 1 opc), - reset_vector_start (set_vector_start_to_length imm7), - reset_vector_start Rn, - reset_vector_start Rt, - reset_vector_start Rt2, - wback, - postindex) - -let decodeLoadStoreRegisterPairPostIndexed ((Vector [_;_;B1;B0;B1;B0;B0;B0;B1;L;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__474) = - let opc = slice_raw v__474 (0:ii) (1:ii) in - let imm7 = slice_raw v__474 (10:ii) (16:ii) in - let Rt2 = slice_raw v__474 (17:ii) (21:ii) in - let Rn = slice_raw v__474 (22:ii) (26:ii) in - let Rt = slice_raw v__474 (27:ii) (31:ii) in - let wback = B1 in - let postindex = B1 in - sharedDecodeLoadStorePair - (match L with | B0 -> (0:ii) | B1 -> (1:ii) end, - reset_vector_start (set_vector_start 1 opc), - reset_vector_start (set_vector_start_to_length imm7), - reset_vector_start Rn, - reset_vector_start Rt, - reset_vector_start Rt2, - wback, - postindex) - -let decodeLoadStoreRegisterPairPreIndexed ((Vector [_;_;B1;B0;B1;B0;B0;B1;B1;L;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__469) = - let opc = slice_raw v__469 (0:ii) (1:ii) in - let imm7 = slice_raw v__469 (10:ii) (16:ii) in - let Rt2 = slice_raw v__469 (17:ii) (21:ii) in - let Rn = slice_raw v__469 (22:ii) (26:ii) in - let Rt = slice_raw v__469 (27:ii) (31:ii) in - let wback = B1 in - let postindex = B0 in - sharedDecodeLoadStorePair - (match L with | B0 -> (0:ii) | B1 -> (1:ii) end, - reset_vector_start (set_vector_start 1 opc), - reset_vector_start (set_vector_start_to_length imm7), - reset_vector_start Rn, - reset_vector_start Rt, - reset_vector_start Rt2, - wback, - postindex) - -let IsSecureBelowEL3 () = - if bitU_to_bool (HaveEL (reset_vector_start EL3)) - then - read_reg_bitfield (SCR_GEN ()) "NS" >>= fun w__0 -> - return (eq (match w__0 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) - else - return (if bitU_to_bool (HaveEL (reset_vector_start EL2)) - then B0 - else IMPLEMENTATION_DEFINED.IMPLEMENTATION_DEFINED_type_IsSecureBelowEL3) - -let AArch64_ResetSpecialRegisters () = - write_reg SP_EL0 (to_vec_dec ((64:ii),UNKNOWN)) >> - write_reg SP_EL1 (to_vec_dec ((64:ii),UNKNOWN)) >> - write_reg SPSR_EL1 (to_vec_dec ((32:ii),UNKNOWN)) >> - write_reg ELR_EL1 (to_vec_dec ((64:ii),UNKNOWN)) >> - (if bitU_to_bool (HaveEL (reset_vector_start EL2)) - then - write_reg SP_EL2 (to_vec_dec ((64:ii),UNKNOWN)) >> - write_reg SPSR_EL2 (to_vec_dec ((32:ii),UNKNOWN)) >> - write_reg ELR_EL2 (to_vec_dec ((64:ii),UNKNOWN)) - else return ()) >> - (if bitU_to_bool (HaveEL (reset_vector_start EL3)) - then - write_reg SP_EL3 (to_vec_dec ((64:ii),UNKNOWN)) >> - write_reg SPSR_EL3 (to_vec_dec ((32:ii),UNKNOWN)) >> - write_reg ELR_EL3 (to_vec_dec ((64:ii),UNKNOWN)) - else return ()) >> - let _ = - if bitU_to_bool (HaveAArch32EL (reset_vector_start EL1)) - then - let SPSR_fiq = to_vec_dec ((32:ii),UNKNOWN) in - let SPSR_irq = to_vec_dec ((32:ii),UNKNOWN) in - let SPSR_abt = to_vec_dec ((32:ii),UNKNOWN) in - let SPSR_und = to_vec_dec ((32:ii),UNKNOWN) in - () - else () in - let DLR_EL0 = to_vec_dec ((64:ii),UNKNOWN) in - let DSPSR_EL0 = to_vec_dec ((32:ii),UNKNOWN) in - return () - -let DecodeBitMasks (M', immN, imms, immr, immediate) = - let M = length (reset_vector_start (set_vector_start_to_length (to_vec_dec (M',(0:ii))))) in - let levels = to_vec_dec ((6:ii),(0:ii)) in - let len = - match (HighestSetBit - (reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length (Vector [immN] 0 false)) ^^ - (set_vector_start_to_length - (NOT (reset_vector_start (set_vector_start_to_length imms)))))))) with - | Nothing -> - let _ = assert' B0 (Just "DecodeBitMasks: HighestSetBit returned None") in - (0:ii) - | Just (c) -> c - end in - (if bitU_to_bool (lt (len, (1:ii))) - then ReservedValue () - else return ()) >> - let _ = assert' (gteq (M, lsl' ((1:ii),len))) (Nothing) in - let levels = - ZeroExtend - ((6:ii), - reset_vector_start (set_vector_start_to_length - (duplicate_bits (set_vector_start_to_length (Vector [B1] 0 false), len)))) in - (if bitU_to_bool - (immediate &. - (eq_vec - (set_vector_start_to_length - (bitwise_and (set_vector_start_to_length imms, set_vector_start_to_length levels)), - set_vector_start_to_length levels))) - then ReservedValue () - else return ()) >> - let S = - set_vector_start 5 - (bitwise_and (set_vector_start_to_length imms, set_vector_start_to_length levels)) in - let R = - set_vector_start 5 - (bitwise_and (set_vector_start_to_length immr, set_vector_start_to_length levels)) in - let diff = - set_vector_start 5 - (minus_VVV - (reset_vector_start (set_vector_start_to_length S)) - (reset_vector_start (set_vector_start_to_length R))) in - let esize = lsl' ((1:ii),len) in - let d = set_vector_start 5 (slice diff (len - (1:ii)) (0:ii)) in - let welem = - set_vector_start_to_length - (ZeroExtend - (esize, - reset_vector_start (set_vector_start_to_length - (duplicate_bits - (set_vector_start_to_length (Vector [B1] 0 false), - add_VII (reset_vector_start (set_vector_start_to_length S)) (1:ii)))))) in - let telem = - set_vector_start_to_length - (ZeroExtend - (esize, - reset_vector_start (set_vector_start_to_length - (duplicate_bits - (set_vector_start_to_length (Vector [B1] 0 false), - add_VII (reset_vector_start (set_vector_start_to_length d)) (1:ii)))))) in - let wmask = - Replicate - (M', - reset_vector_start (set_vector_start_to_length - (ROR - (reset_vector_start (set_vector_start_to_length welem), - unsigned (reset_vector_start R))))) in - let tmask = Replicate (M',reset_vector_start (set_vector_start_to_length telem)) in - return (set_vector_start_to_length wmask,set_vector_start_to_length tmask) - -let AArch64_TranslateAddress (vaddress, acctype, iswrite, wasaligned, size) = - let _ = - info - "Translation is not implemented, return same address as the virtual (no fault, normal, shareable, non-secure)." in - <| AddressDescriptor_fault = (AArch64_NoFault ()); - AddressDescriptor_memattrs = - (<| MemoryAttributes_type' = MemType_Normal; - MemoryAttributes_shareable = B1 |>); - AddressDescriptor_paddress = - (<| FullAddress_physicaladdress = vaddress; - FullAddress_NS = B1 |>) |> - -let ExtendReg (N', _reg, type', shift) = - rX (N',_reg) >>= fun w__0 -> - let _val = set_vector_start_to_length w__0 in - let _unsigned = B0 in - let len = (0:ii) in - let (_unsigned, len) = - match type' with - | ExtendType_SXTB -> - let _unsigned = B0 in - let len = (8:ii) in - (_unsigned,len) - | ExtendType_SXTH -> - let _unsigned = B0 in - let len = (16:ii) in - (_unsigned,len) - | ExtendType_SXTW -> - let _unsigned = B0 in - let len = (32:ii) in - (_unsigned,len) - | ExtendType_SXTX -> - let _unsigned = B0 in - let len = (64:ii) in - (_unsigned,len) - | ExtendType_UXTB -> - let _unsigned = B1 in - let len = (8:ii) in - (_unsigned,len) - | ExtendType_UXTH -> - let _unsigned = B1 in - let len = (16:ii) in - (_unsigned,len) - | ExtendType_UXTW -> - let _unsigned = B1 in - let len = (32:ii) in - (_unsigned,len) - | ExtendType_UXTX -> - let _unsigned = B1 in - let len = (64:ii) in - (_unsigned,len) - end in - let len = uMin (len,(length (reset_vector_start (set_vector_start_to_length _val))) - shift) in - return (set_vector_start_to_length - (Extend - (length _val, - reset_vector_start (set_vector_start_to_length - ((set_vector_start_to_length - (slice (set_vector_start_to_length _val) (len - (1:ii)) (0:ii))) ^^ - (set_vector_start_to_length (set_vector_start_to_length (Zeros shift))))), - _unsigned))) - -let ShiftReg (N', _reg, type', amount) = - rX (N',_reg) >>= fun w__0 -> - let result = set_vector_start_to_length w__0 in - let result = - match type' with - | ShiftType_LSL -> - set_vector_start_to_length - (LSL (reset_vector_start (set_vector_start_to_length result),amount)) - | ShiftType_LSR -> - set_vector_start_to_length - (LSR (reset_vector_start (set_vector_start_to_length result),amount)) - | ShiftType_ASR -> - set_vector_start_to_length - (ASR (reset_vector_start (set_vector_start_to_length result),amount)) - | ShiftType_ROR -> - set_vector_start_to_length - (ROR (reset_vector_start (set_vector_start_to_length result),amount)) - end in - return (set_vector_start_to_length result) - -let initial_analysis instr = - let iR = [] in - let oR = [] in - let aR = [] in - let Nias = [NIAFP_successor] in - let Dia = DIAFP_none in - let ik = IK_simple in - match instr with - | TMStart (t) -> - let iR = TxNestingLevelfp :: TXIDR_EL0_DEPTHfp :: iR in - let oR = TxNestingLevelfp :: (oR ++ (xFP t)) in - let ik = IK_trans Transaction_start in - return (aR,Nias,iR,oR,ik) - | TMCommit -> - let iR = TxNestingLevelfp :: iR in - let oR = TxNestingLevelfp :: oR in - let ik = IK_trans Transaction_commit in - return (aR,Nias,iR,oR,ik) - | TMAbort (retry,reason) -> - let iR = TxNestingLevelfp :: iR in - let ik = IK_trans Transaction_abort in - return (aR,Nias,iR,oR,ik) - | TMTest -> - let iR = TxNestingLevelfp :: iR in - let oR = (RFull "NZCV") :: oR in - return (aR,Nias,iR,oR,ik) - | CompareAndBranch (t,datasize,iszero,offset) -> - let iR = iR ++ (xFP t) in - let (i, o) = match (BranchToFP (iR,oR)) with | (v0v', v1v') -> (v0v',v1v') end in - let iR = i in - let oR = o in - rPC () >>= fun w__0 -> - let nia' = - set_vector_start 63 - (add_VVV - (reset_vector_start (set_vector_start_to_length w__0)) - (reset_vector_start (set_vector_start_to_length offset))) in - let Nias = [NIAFP_concrete_address (reset_vector_start nia');NIAFP_successor] in - let ik = IK_branch in - return (aR,Nias,iR,oR,ik) - | BranchConditional (offset,condition) -> - let iR = iR ++ (ConditionHoldsIFP (reset_vector_start condition)) in - let (i, o) = match (BranchToFP (iR,oR)) with | (v2v', v3v') -> (v2v',v3v') end in - let iR = i in - let oR = o in - rPC () >>= fun w__1 -> - let Nias = - [NIAFP_concrete_address (reset_vector_start (set_vector_start 63 - (add_VVV - (reset_vector_start (set_vector_start_to_length w__1)) - (reset_vector_start (set_vector_start_to_length offset)))));NIAFP_successor] in - let ik = IK_branch in - return (aR,Nias,iR,oR,ik) - | GenerateExceptionEL1 (imm) -> - not_implemented "GenerateExceptionEL1" >> - return (aR,Nias,iR,oR,ik) - | GenerateExceptionEL2 (imm) -> - not_implemented "GenerateExceptionEL2" >> - return (aR,Nias,iR,oR,ik) - | GenerateExceptionEL3 (imm) -> - not_implemented "GenerateExceptionEL3" >> - return (aR,Nias,iR,oR,ik) - | DebugBreakpoint (comment) -> - not_implemented "DebugBreakpoint" >> - return (aR,Nias,iR,oR,ik) - | ExternalDebugBreakpoint -> - not_implemented "ExternalDebugBreakpoint" >> - return (aR,Nias,iR,oR,ik) - | DebugSwitchToExceptionLevel (target_level) -> - not_implemented "DebugSwitchToExceptionLevel" >> - return (aR,Nias,iR,oR,ik) - | MoveSystemImmediate (operand,field') -> - let (iR, oR) = - match field' with - | PSTATEField_SP -> - let oR = PSTATE_SPfp :: oR in - (iR,oR) - | PSTATEField_DAIFSet -> - let iR = iR ++ [PSTATE_Ffp;PSTATE_Ifp;PSTATE_Afp;PSTATE_Dfp] in - let oR = oR ++ [PSTATE_Ffp;PSTATE_Ifp;PSTATE_Afp;PSTATE_Dfp] in - (iR,oR) - | PSTATEField_DAIFClr -> - let iR = iR ++ [PSTATE_Ffp;PSTATE_Ifp;PSTATE_Afp;PSTATE_Dfp] in - let oR = oR ++ [PSTATE_Ffp;PSTATE_Ifp;PSTATE_Afp;PSTATE_Dfp] in - (iR,oR) - end in - return (aR,Nias,iR,oR,ik) - | Hint (op) -> - match op with - | SystemHintOp_YIELD -> return () - | SystemHintOp_WFE -> - EventRegistered () >>= fun w__2 -> - if bitU_to_bool w__2 - then return () - else not_implemented "Hint(SystemHintOp_WFE);" - | SystemHintOp_WFI -> not_implemented "Hint(SystemHintOp_WFI);" - | SystemHintOp_SEV -> return () - | SystemHintOp_SEVL -> not_implemented "Hint(SystemHintOp_SEVL);" - | _ -> return () - end >> - return (aR,Nias,iR,oR,ik) - | ClearExclusiveMonitor (imm) -> return (aR,Nias,iR,oR,ik) - | Barrier (op,domain,types) -> - let ik = - match op with - | MemBarrierOp_DSB -> - match types with - | MBReqTypes_Reads -> IK_barrier Barrier_DSB_LD - | MBReqTypes_Writes -> IK_barrier Barrier_DSB_ST - | MBReqTypes_All -> IK_barrier Barrier_DSB - end - | MemBarrierOp_DMB -> - match types with - | MBReqTypes_Reads -> IK_barrier Barrier_DMB_LD - | MBReqTypes_Writes -> IK_barrier Barrier_DMB_ST - | MBReqTypes_All -> IK_barrier Barrier_DMB - end - | MemBarrierOp_ISB -> IK_barrier Barrier_ISB - end in - return (aR,Nias,iR,oR,ik) - | System (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result) -> - let oR = oR ++ (xFP t) in - not_implemented "System" >> - return (aR,Nias,iR,oR,ik) - | MoveSystemRegister (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read) -> - let (oR, iR) = - if bitU_to_bool read - then - let oR = oR ++ (xFP t) in - let iR = - match toNaturalFiveTup (sys_op0,sys_op1,sys_crn,sys_crm,sys_op2) with - | ((3:nn), (3:nn), (4:nn), (2:nn), (0:nn)) -> (RFull "NZCV") :: iR - | ((3:nn), (3:nn), (4:nn), (2:nn), (1:nn)) -> (RFull "DAIF") :: iR - | ((3:nn), (3:nn), (13:nn), (0:nn), (2:nn)) -> (RFull "TPIDR_EL0") :: iR - end in - (oR,iR) - else - let iR = iR ++ (xFP t) in - let oR = - match toNaturalFiveTup (sys_op0,sys_op1,sys_crn,sys_crm,sys_op2) with - | ((3:nn), (3:nn), (4:nn), (2:nn), (0:nn)) -> (RFull "NZCV") :: oR - | ((3:nn), (3:nn), (4:nn), (2:nn), (1:nn)) -> (RFull "DAIF") :: oR - | ((3:nn), (3:nn), (13:nn), (0:nn), (2:nn)) -> (RFull "TPIDR_EL0") :: oR - end in - (oR,iR) in - return (aR,Nias,iR,oR,ik) - | ImplementationDefinedTestBeginEnd (isEnd) -> return (aR,Nias,iR,oR,ik) - | ImplementationDefinedStopFetching -> return (aR,Nias,iR,oR,ik) - | ImplementationDefinedThreadStart -> return (aR,Nias,iR,oR,ik) - | TestBitAndBranch (t,datasize,bit_pos,bit_val,offset) -> - let iR = (xFP t) ++ iR in - let (i, o) = match (BranchToFP (iR,oR)) with | (v4v', v5v') -> (v4v',v5v') end in - let iR = i in - let oR = o in - rPC () >>= fun w__3 -> - let Nias = - [NIAFP_concrete_address (reset_vector_start (set_vector_start 63 - (add_VVV - (reset_vector_start (set_vector_start_to_length w__3)) - (reset_vector_start (set_vector_start_to_length offset)))));NIAFP_successor] in - let ik = IK_branch in - return (aR,Nias,iR,oR,ik) - | BranchImmediate (branch_type,offset) -> - let (iR, oR) = - if bitU_to_bool (eq (branch_type, BranchType_CALL)) - then - let iR = _PCfp :: iR in - let oR = (xFP (30:ii)) ++ oR in - (iR,oR) - else (iR,oR) in - let (i, o) = match (BranchToFP (iR,oR)) with | (v6v', v7v') -> (v6v',v7v') end in - let iR = i in - let oR = o in - rPC () >>= fun w__4 -> - let Nias = - [NIAFP_concrete_address (reset_vector_start (set_vector_start 63 - (add_VVV - (reset_vector_start (set_vector_start_to_length w__4)) - (reset_vector_start (set_vector_start_to_length offset)))))] in - let ik = IK_branch in - return (aR,Nias,iR,oR,ik) - | BranchRegister (n,branch_type) -> - let iR = iR ++ (xFP n) in - let (iR, oR) = - if bitU_to_bool (eq (branch_type, BranchType_CALL)) - then - let iR = _PCfp :: iR in - let oR = (xFP (30:ii)) ++ oR in - (iR,oR) - else (iR,oR) in - let (i, o) = match (BranchToFP (iR,oR)) with | (v8v', v9v') -> (v8v',v9v') end in - let iR = i in - let oR = o in - let Nias = - if bitU_to_bool (eq_range (n, (31:ii))) - then [NIAFP_concrete_address (reset_vector_start (to_vec_dec ((64:ii),(0:ii))))] - else [NIAFP_indirect_address] in - let ik = IK_branch in - return (aR,Nias,iR,oR,ik) - | ExceptionReturn -> - not_implemented "ExceptionReturn" >> - return (aR,Nias,iR,oR,ik) - | DebugRestorePState -> - not_implemented "DebugRestorePState" >> - return (aR,Nias,iR,oR,ik) - | LoadLiteral (t,memop,_signed,size,offset,datasize) -> - let iR = _PCfp :: iR in - let oR = (xFP t) ++ oR in - let aR = _PCfp :: aR in - let (aR, ik) = - match memop with - | MemOp_LOAD -> - let ik = IK_mem_read Read_plain in - (aR,ik) - | MemOp_PREFETCH -> - let ik = IK_simple in - let aR = [] in - (aR,ik) - end in - return (aR,Nias,iR,oR,ik) - | LoadStoreAcqExc (n,t,t2,s,acctype,excl,pair,memop,elsize,regsize,datasize) -> - let rt_unknown = B0 in - let rn_unknown = B0 in - let (iR, aR) = - if bitU_to_bool (eq_range (n, (31:ii))) - then - let iR = CheckSPAlignmentIFP ++ iR in - let iR = rSPIFP ++ iR in - let aR = rSPIFP ++ aR in - (iR,aR) - else - let (iR, aR) = - if bitU_to_bool rn_unknown - then (iR,aR) - else - let iR = (xFP n) ++ iR in - let aR = (xFP n) ++ aR in - (iR,aR) in - (iR,aR) in - match memop with - | MemOp_STORE -> - let iR = - if bitU_to_bool rt_unknown - then iR - else if bitU_to_bool pair then (xFP t) ++ ((xFP t2) ++ iR) else (xFP t) ++ iR in - (if bitU_to_bool excl - then - let iR = iR ++ wMemIFP in - let oR = (xFP s) ++ oR in - wmem_kind (acctype,B1) >>= fun w__5 -> - let ik = w__5 in - return (iR,oR,ik) - else - let iR = iR ++ wMemIFP in - wmem_kind (acctype,B0) >>= fun w__6 -> - let ik = w__6 in - return (iR,oR,ik)) >>= fun (iR, oR, ik) -> - return (aR,iR,oR,ik) - | MemOp_LOAD -> - (if bitU_to_bool pair - then - let (iR, oR) = - if bitU_to_bool rt_unknown - then - let oR = (xFP t) ++ oR in - (iR,oR) - else - let (iR, oR) = - if bitU_to_bool (eq_range (elsize, (32:ii))) - then - let iR = iR ++ BigEndianIFP in - let oR = (xFP t) ++ ((xFP t2) ++ oR) in - (iR,oR) - else - let oR = (xFP t) ++ ((xFP t2) ++ oR) in - (iR,oR) in - (iR,oR) in - rmem_kind (acctype,B1) >>= fun w__7 -> - let ik = w__7 in - return (oR,iR,ik) - else - let oR = (xFP t) ++ oR in - rmem_kind (acctype,excl) >>= fun w__8 -> - let ik = w__8 in - return (oR,iR,ik)) >>= fun (oR, iR, ik) -> - return (aR,iR,oR,ik) - | MemOp_PREFETCH -> - let aR = [] in - return (aR,iR,oR,ik) - end >>= fun (aR, iR, oR, ik) -> - return (aR,Nias,iR,oR,ik) - | LoadStorePairNonTemp (wback,postindex,n,t,t2,acctype,memop,scale,datasize,offset) -> - let rt_unknown = B0 in - let (iR, aR) = - if bitU_to_bool (eq_range (n, (31:ii))) - then - let iR = CheckSPAlignmentIFP ++ iR in - let iR = rSPIFP ++ iR in - let aR = rSPIFP ++ aR in - (iR,aR) - else - let iR = (xFP n) ++ iR in - let aR = (xFP n) ++ aR in - (iR,aR) in - let (iR, oR) = - if bitU_to_bool wback - then - let (iR, oR) = - if bitU_to_bool (eq_range (n, (31:ii))) - then - let (i, o) = match wSPFP with | (v10v', v11v') -> (v10v',v11v') end in - let iR = i ++ iR in - let oR = o ++ oR in - (iR,oR) - else - let oR = (xFP n) ++ oR in - (iR,oR) in - (iR,oR) - else (iR,oR) in - match memop with - | MemOp_STORE -> - let iR = if bitU_to_bool (rt_unknown &. (eq_range (t, n))) then iR else (xFP t) ++ iR in - let iR = if bitU_to_bool (rt_unknown &. (eq_range (t2, n))) then iR else (xFP t2) ++ iR in - let iR = wMemIFP ++ iR in - wmem_kind (acctype,B0) >>= fun w__9 -> - let ik = w__9 in - return (oR,iR,ik) - | MemOp_LOAD -> - let oR = (xFP t) ++ ((xFP t2) ++ oR) in - rmem_kind (acctype,B0) >>= fun w__10 -> - let ik = w__10 in - return (oR,iR,ik) - end >>= fun (oR, iR, ik) -> - return (aR,Nias,iR,oR,ik) - | LoadImmediate (n,t,acctype,memop,_signed,wback,postindex,offset,regsize,datasize) -> - let wb_unknown = B0 in - let rt_unknown = B0 in - let (iR, aR) = - if bitU_to_bool (eq_range (n, (31:ii))) - then - let iR = CheckSPAlignmentIFP ++ iR in - let iR = rSPIFP ++ iR in - let aR = rSPIFP ++ aR in - (iR,aR) - else - let iR = (xFP n) ++ iR in - let aR = (xFP n) ++ aR in - (iR,aR) in - let (iR, oR) = - if bitU_to_bool wback - then - let (iR, oR) = - if bitU_to_bool (eq_range (n, (31:ii))) - then - let (i, o) = match wSPFP with | (v12v', v13v') -> (v12v',v13v') end in - let iR = i ++ iR in - let oR = o ++ oR in - (iR,oR) - else - let oR = (xFP n) ++ oR in - (iR,oR) in - (iR,oR) - else (iR,oR) in - match memop with - | MemOp_STORE -> - let iR = if bitU_to_bool rt_unknown then iR else (xFP t) ++ iR in - let iR = wMemIFP ++ iR in - wmem_kind (acctype,B0) >>= fun w__11 -> - let ik = w__11 in - return (aR,oR,iR,ik) - | MemOp_LOAD -> - let oR = (xFP t) ++ oR in - rmem_kind (acctype,B0) >>= fun w__12 -> - let ik = w__12 in - return (aR,oR,iR,ik) - | MemOp_PREFETCH -> - let aR = [] in - return (aR,oR,iR,ik) - end >>= fun (aR, oR, iR, ik) -> - return (aR,Nias,iR,oR,ik) - | LoadRegister (n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize,datasize) -> - let iR = (xFP m) ++ iR in - let aR = (xFP m) ++ aR in - let wb_unknown = B0 in - let rt_unknown = B0 in - let (iR, aR) = - if bitU_to_bool (eq_range (n, (31:ii))) - then - let iR = CheckSPAlignmentIFP ++ iR in - let iR = rSPIFP ++ iR in - let aR = rSPIFP ++ aR in - (iR,aR) - else - let iR = (xFP n) ++ iR in - let aR = (xFP n) ++ aR in - (iR,aR) in - let (iR, oR) = - if bitU_to_bool wback - then - let (iR, oR) = - if bitU_to_bool (eq_range (n, (31:ii))) - then - let (i, o) = match wSPFP with | (v14v', v15v') -> (v14v',v15v') end in - let iR = i ++ iR in - let oR = o ++ oR in - (iR,oR) - else - let oR = (xFP n) ++ oR in - (iR,oR) in - (iR,oR) - else (iR,oR) in - match memop with - | MemOp_STORE -> - let iR = if bitU_to_bool rt_unknown then iR else (xFP t) ++ iR in - let iR = wMemIFP ++ iR in - wmem_kind (acctype,B0) >>= fun w__13 -> - let ik = w__13 in - return (aR,oR,iR,ik) - | MemOp_LOAD -> - let oR = (xFP t) ++ oR in - rmem_kind (acctype,B0) >>= fun w__14 -> - let ik = w__14 in - return (aR,oR,iR,ik) - | MemOp_PREFETCH -> - let aR = [] in - return (aR,oR,iR,ik) - end >>= fun (aR, oR, iR, ik) -> - return (aR,Nias,iR,oR,ik) - | LoadStorePair (wback,postindex,n,t,t2,acctype,memop,_signed,datasize,offset) -> - let rt_unknown = B0 in - let wb_unknown = B0 in - let (iR, aR) = - if bitU_to_bool (eq_range (n, (31:ii))) - then - let iR = CheckSPAlignmentIFP ++ iR in - let iR = rSPIFP ++ iR in - let aR = rSPIFP ++ aR in - (iR,aR) - else - let iR = (xFP n) ++ iR in - let aR = (xFP n) ++ aR in - (iR,aR) in - let (iR, oR) = - if bitU_to_bool wback - then - let (iR, oR) = - if bitU_to_bool (eq_range (n, (31:ii))) - then - let (i, o) = match wSPFP with | (v16v', v17v') -> (v16v',v17v') end in - let iR = i ++ iR in - let oR = o ++ oR in - (iR,oR) - else - let oR = (xFP n) ++ oR in - (iR,oR) in - (iR,oR) - else (iR,oR) in - match memop with - | MemOp_STORE -> - let iR = if bitU_to_bool (rt_unknown &. (eq_range (t, n))) then iR else (xFP t) ++ iR in - let iR = if bitU_to_bool (rt_unknown &. (eq_range (t2, n))) then iR else (xFP t2) ++ iR in - let iR = wMemIFP ++ iR in - wmem_kind (acctype,B0) >>= fun w__15 -> - let ik = w__15 in - return (oR,iR,ik) - | MemOp_LOAD -> - let oR = (xFP t) ++ oR in - let oR = (xFP t2) ++ oR in - rmem_kind (acctype,B0) >>= fun w__16 -> - let ik = w__16 in - return (oR,iR,ik) - end >>= fun (oR, iR, ik) -> - return (aR,Nias,iR,oR,ik) - | AddSubImmediate (d,n,datasize,sub_op,setflags,imm) -> - let iR = (if bitU_to_bool (eq_range (n, (31:ii))) then rSPIFP else xFP n) ++ iR in - let oR = if bitU_to_bool setflags then NZCVfp ++ oR else oR in - let (iR, oR) = - if bitU_to_bool ((eq_range (d, (31:ii))) &. (~setflags)) - then - let (i, o) = match wSPFP with | (v18v', v19v') -> (v18v',v19v') end in - let iR = i ++ iR in - let oR = o ++ oR in - (iR,oR) - else - let oR = (xFP d) ++ oR in - (iR,oR) in - return (aR,Nias,iR,oR,ik) - | BitfieldMove (d,n,datasize,inzero,extend,R,S,wmask,tmask) -> - let iR = if bitU_to_bool inzero then iR else (xFP d) ++ iR in - let iR = (xFP n) ++ iR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | ExtractRegister (d,n,m,datasize,lsb) -> - let iR = (xFP n) ++ ((xFP m) ++ iR) in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | LogicalImmediate (d,n,datasize,setflags,op,imm) -> - let iR = (xFP n) ++ iR in - let oR = if bitU_to_bool setflags then NZCVfp ++ oR else oR in - let (iR, oR) = - if bitU_to_bool ((eq_range (d, (31:ii))) &. (~setflags)) - then - let (i, o) = match wSPFP with | (v20v', v21v') -> (v20v',v21v') end in - let iR = i ++ iR in - let oR = o ++ oR in - (iR,oR) - else - let oR = (xFP d) ++ oR in - (iR,oR) in - return (aR,Nias,iR,oR,ik) - | MoveWide (d,datasize,imm,pos,opcode) -> - let iR = if bitU_to_bool (eq (opcode, MoveWideOp_K)) then (xFP d) ++ iR else iR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | Address (d,page,imm) -> - let iR = _PCfp :: iR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | AddSubExtendRegister (d,n,m,datasize,sub_op,setflags,extend_type,shift) -> - let iR = (if bitU_to_bool (eq_range (n, (31:ii))) then rSPIFP else xFP n) ++ iR in - let iR = (xFP m) ++ iR in - let oR = if bitU_to_bool setflags then NZCVfp ++ oR else oR in - let (iR, oR) = - if bitU_to_bool ((eq_range (d, (31:ii))) &. (~setflags)) - then - let (i, o) = match wSPFP with | (v22v', v23v') -> (v22v',v23v') end in - let iR = i ++ iR in - let oR = o ++ oR in - (iR,oR) - else - let oR = (xFP d) ++ oR in - (iR,oR) in - return (aR,Nias,iR,oR,ik) - | AddSubShiftedRegister (d,n,m,datasize,sub_op,setflags,shift_type,shift_amount) -> - let iR = (xFP n) ++ ((xFP m) ++ iR) in - let oR = if bitU_to_bool setflags then NZCVfp ++ oR else oR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | AddSubCarry (d,n,m,datasize,sub_op,setflags) -> - let iR = (xFP n) ++ ((xFP m) ++ iR) in - let iR = PSTATE_Cfp :: iR in - let oR = if bitU_to_bool setflags then NZCVfp ++ oR else oR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | ConditionalCompareImmediate (n,datasize,sub_op,condition,flags,imm) -> - let iR = (xFP n) ++ iR in - let iR = (ConditionHoldsIFP (reset_vector_start condition)) ++ iR in - let oR = NZCVfp ++ oR in - return (aR,Nias,iR,oR,ik) - | ConditionalCompareRegister (n,m,datasize,sub_op,condition,flags) -> - let iR = (xFP n) ++ ((xFP m) ++ iR) in - let iR = (ConditionHoldsIFP (reset_vector_start condition)) ++ iR in - let oR = NZCVfp ++ oR in - return (aR,Nias,iR,oR,ik) - | ConditionalSelect (d,n,m,datasize,condition,else_inv,else_inc) -> - let iR = (xFP n) ++ ((xFP m) ++ iR) in - let iR = (ConditionHoldsIFP (reset_vector_start condition)) ++ iR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | Reverse (d,n,datasize,op) -> - let iR = (xFP n) ++ iR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | CountLeading (d,n,datasize,opcode) -> - let iR = (xFP n) ++ iR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | Division (d,n,m,datasize,_unsigned) -> - let iR = (xFP n) ++ ((xFP m) ++ iR) in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | Shift (d,n,m,datasize,shift_type) -> - let iR = (xFP m) ++ iR in - let iR = (xFP n) ++ iR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | CRC (d,n,m,size,crc32c) -> - let iR = (xFP n) ++ ((xFP m) ++ iR) in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | MultiplyAddSub (d,n,m,a,destsize,datasize,sub_op) -> - let iR = (xFP n) ++ iR in - let iR = (xFP m) ++ iR in - let iR = (xFP a) ++ iR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | MultiplyAddSubLong (d,n,m,a,destsize,datasize,sub_op,_unsigned) -> - let iR = (xFP n) ++ iR in - let iR = (xFP m) ++ iR in - let iR = (xFP a) ++ iR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | MultiplyHigh (d,n,m,a,destsize,datasize,_unsigned) -> - let iR = (xFP n) ++ ((xFP m) ++ iR) in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - | LogicalShiftedRegister (d,n,m,datasize,setflags,op,shift_type,shift_amount,invert) -> - let iR = (xFP n) ++ ((xFP m) ++ iR) in - let oR = if bitU_to_bool setflags then NZCVfp ++ oR else oR in - let oR = (xFP d) ++ oR in - return (aR,Nias,iR,oR,ik) - end >>= fun (aR, Nias, iR, oR, ik) -> - return (iR,oR,aR,Nias,Dia,ik) - -let decodeBranchesExceptionSystem machineCode = - match machineCode with - | ((Vector [_;B0;B0;B1;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__392) -> - return (decodeUnconditionalBranchImmediate - (reset_vector_start (set_vector_start_to_length machineCode))) - | ((Vector [_;B0;B1;B1;B0;B1;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__403) -> - return (decodeCompareBranchImmediate - (reset_vector_start (set_vector_start_to_length machineCode))) - | ((Vector [_;B0;B1;B1;B0;B1;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__414) -> - return (decodeTestBranchImmediate (reset_vector_start (set_vector_start_to_length machineCode))) - | ((Vector [B0;B1;B0;B1;B0;B1;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__425) -> - return (decodeConditionalBranchImmediate - (reset_vector_start (set_vector_start_to_length machineCode))) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__436) -> - decodeExceptionGeneration (reset_vector_start machineCode) - | ((Vector [B1;B1;B0;B1;B0;B1;B0;B1;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__447) -> - decodeSystemImplementationDefined (reset_vector_start machineCode) - | ((Vector [B1;B1;B0;B1;B0;B1;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__458) -> - decodeUnconditionalBranchRegister (reset_vector_start machineCode) - end - -let IsSecure () = - read_reg_field CurrentEL "EL" >>= fun w__0 -> - if bitU_to_bool - ((HaveEL (reset_vector_start EL3)) &. - ((~(UsingAArch32 ())) &. - (eq_vec (set_vector_start_to_length w__0, set_vector_start_to_length EL3)))) - then return B1 - else - read_reg PSTATE_M >>= fun w__1 -> - if bitU_to_bool - ((HaveEL (reset_vector_start EL3)) &. - ((UsingAArch32 ()) &. (eq_vec (w__1, set_vector_start_to_length M32_Monitor)))) - then return B1 - else IsSecureBelowEL3 () - -let decodeLogicalImmediate ((Vector [sf;_;_;B1;B0;B0;B1;B0;B0;N;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__388) = - let opc = slice_raw v__388 (1:ii) (2:ii) in - let immr = slice_raw v__388 (10:ii) (15:ii) in - let imms = slice_raw v__388 (16:ii) (21:ii) in - let Rn = slice_raw v__388 (22:ii) (26:ii) in - let Rd = slice_raw v__388 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let setflags = B0 in - let op = LogicalOp_AND in - let (op, setflags) = - match opc with - | Vector [B0;B0] _ _ -> - let op = LogicalOp_AND in - let setflags = B0 in - (op,setflags) - | Vector [B0;B1] _ _ -> - let op = LogicalOp_ORR in - let setflags = B0 in - (op,setflags) - | Vector [B1;B0] _ _ -> - let op = LogicalOp_EOR in - let setflags = B0 in - (op,setflags) - | Vector [B1;B1] _ _ -> - let op = LogicalOp_AND in - let setflags = B1 in - (op,setflags) - end in - (if bitU_to_bool - ((eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) &. - (neq (match N with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)))) - then ReservedValue () - else return ()) >> - DecodeBitMasks (datasize,N,reset_vector_start imms,reset_vector_start immr,B1) >>= fun w__0 -> - let (imm, _) = match w__0 with | (v0v', v1v') -> (v0v',v1v') end in - return (Just (LogicalImmediate (d,n,datasize,setflags,op,reset_vector_start (set_vector_start_to_length - imm)))) - -let decodeBitfield ((Vector [sf;_;_;B1;B0;B0;B1;B1;B0;N;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__384) = - let opc = slice_raw v__384 (1:ii) (2:ii) in - let immr = slice_raw v__384 (10:ii) (15:ii) in - let imms = slice_raw v__384 (16:ii) (21:ii) in - let Rn = slice_raw v__384 (22:ii) (26:ii) in - let Rd = slice_raw v__384 (27:ii) (31:ii) in - let d = UInt_reg (reset_vector_start Rd) in - let n = UInt_reg (reset_vector_start Rn) in - let datasize = - if bitU_to_bool (eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then (64:ii) - else (32:ii) in - let inzero = B0 in - let extend = B0 in - let R = (0:ii) in - let S = (0:ii) in - match opc with - | Vector [B0;B0] _ _ -> - let inzero = B1 in - let extend = B1 in - return (inzero,extend) - | Vector [B0;B1] _ _ -> - let inzero = B0 in - let extend = B0 in - return (inzero,extend) - | Vector [B1;B0] _ _ -> - let inzero = B1 in - let extend = B0 in - return (inzero,extend) - | Vector [B1;B1] _ _ -> - UnallocatedEncoding () >> - return (inzero,extend) - end >>= fun (inzero, extend) -> - (if bitU_to_bool - ((eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) &. - (neq (match N with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))) - then ReservedValue () - else return ()) >> - (if bitU_to_bool - ((eq (match sf with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) &. - ((neq (match N with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) |. - ((neq (match (access immr (5:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) |. - (neq (match (access imms (5:ii)) with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)))))) - then ReservedValue () - else return ()) >> - let R = UInt (reset_vector_start (set_vector_start_to_length immr)) in - let S = UInt (reset_vector_start (set_vector_start_to_length imms)) in - DecodeBitMasks (datasize,N,reset_vector_start imms,reset_vector_start immr,B0) >>= fun (wmask, tmask) -> - return (Just (BitfieldMove (d,n,datasize,inzero,extend,R,S,reset_vector_start (set_vector_start_to_length - wmask),reset_vector_start (set_vector_start_to_length tmask)))) - -let AArch64_SetExclusiveMonitors (address, size) = - let acctype = AccType_ATOMIC in - let iswrite = B0 in - let aligned = - neq_vec - (set_vector_start_to_length address, - set_vector_start_to_length - (Align (reset_vector_start (set_vector_start_to_length address),size))) in - let memaddrdesc = - AArch64_TranslateAddress (reset_vector_start address,acctype,iswrite,aligned,size) in - if bitU_to_bool (IsFault memaddrdesc) - then () - else - let _ = - if bitU_to_bool memaddrdesc.AddressDescriptor_memattrs.MemoryAttributes_shareable - then MarkExclusiveGlobal (memaddrdesc.AddressDescriptor_paddress,ProcessorID (),size) - else () in - let _ = MarkExclusiveLocal (memaddrdesc.AddressDescriptor_paddress,ProcessorID (),size) in - AArch64_MarkExclusiveVA (reset_vector_start address,ProcessorID (),size) - -let AArch64_TakeReset cold_reset = - let _ = assert' (~(HighestELUsingAArch32 ())) (Nothing) in - write_reg PSTATE_nRW (to_vec_dec ((1:ii),(0:ii))) >> - (if bitU_to_bool (HaveEL (reset_vector_start EL3)) - then - write_reg_field CurrentEL "EL" (set_vector_start 3 EL3) >> - write_reg_bitfield SCR_EL3 "NS" B0 - else - if bitU_to_bool (HaveEL (reset_vector_start EL2)) - then write_reg_field CurrentEL "EL" (set_vector_start 3 EL2) - else write_reg_field CurrentEL "EL" (set_vector_start 3 EL1)) >> - let _ = AArch64_ResetControlRegisters cold_reset in - write_reg_bitfield SPSel "SP" B0 >> - wPSTATE_DAIF ((),reset_vector_start (Vector [B1;B1;B1;B1] 3 false)) >> - let PSTATE_SS = (0:ii) in - let PSTATE_IL = (0:ii) in - AArch64_ResetGeneralRegisters () >> - AArch64_ResetSIMDFPRegisters () >> - AArch64_ResetSpecialRegisters () >> - ResetExternalDebugRegisters cold_reset >> - let rv = to_vec_dec ((64:ii),(0:ii)) in - (if bitU_to_bool (HaveEL (reset_vector_start EL3)) - then read_reg RVBAR_EL3 - else - if bitU_to_bool (HaveEL (reset_vector_start EL2)) - then read_reg RVBAR_EL2 - else read_reg RVBAR_EL1) >>= fun rv -> - PAMax () >>= fun w__3 -> - let _ = - assert' ((IsZero - (reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length rv) (63:ii) w__3)))) &. - (IsZero - (reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length rv) (1:ii) (0:ii)))))) (Just "reset vector not correctly aligned") in - BranchTo (reset_vector_start (set_vector_start_to_length rv),BranchType_UNKNOWN) - -let AArch64_rMemSingle (read_buffer, address, size, acctype, wasaligned, exclusive) = - let _ = - assert' (eq_vec - (set_vector_start_to_length address, - set_vector_start_to_length - (Align (reset_vector_start (set_vector_start_to_length address),size)))) (Nothing) in - let value = set_vector_start_to_length (to_vec_dec (size * (8:ii),(0:ii))) in - let iswrite = B0 in - let memaddrdesc = - AArch64_TranslateAddress (reset_vector_start address,acctype,iswrite,wasaligned,size) in - (if bitU_to_bool (IsFault memaddrdesc) - then AArch64_Abort (reset_vector_start address,memaddrdesc.AddressDescriptor_fault) - else return ()) >> - return (_rMem (read_buffer,memaddrdesc,size,acctype,exclusive)) - -let AArch64_wMemSingle (write_buffer, address, size, acctype, wasaligned, exclusive, value) = - let _ = - assert' (eq_vec - (set_vector_start_to_length address, - set_vector_start_to_length - (Align (reset_vector_start (set_vector_start_to_length address),size)))) (Nothing) in - let iswrite = B1 in - let memaddrdesc = - AArch64_TranslateAddress (reset_vector_start address,acctype,iswrite,wasaligned,size) in - (if bitU_to_bool (IsFault memaddrdesc) - then AArch64_Abort (reset_vector_start address,memaddrdesc.AddressDescriptor_fault) - else return ()) >> - let _ = - if bitU_to_bool memaddrdesc.AddressDescriptor_memattrs.MemoryAttributes_shareable - then ClearExclusiveByAddress (memaddrdesc.AddressDescriptor_paddress,ProcessorID (),size) - else () in - return (_wMem - (write_buffer, - memaddrdesc, - size, - acctype, - exclusive, - reset_vector_start (set_vector_start_to_length value))) - -let AArch64_ExclusiveMonitorsPass (address, size) = - let acctype = AccType_ATOMIC in - let iswrite = B1 in - let aligned = - eq_vec - (set_vector_start_to_length address, - set_vector_start_to_length - (Align (reset_vector_start (set_vector_start_to_length address),size))) in - (if bitU_to_bool (~aligned) - then - let secondstage = B0 in - AArch64_Abort (reset_vector_start address,AArch64_AlignmentFault (acctype,iswrite,secondstage)) - else return ()) >> - let passed = AArch64_IsExclusiveVA (reset_vector_start address,ProcessorID (),size) in - (if bitU_to_bool (~passed) - then return (B0,passed) - else - let memaddrdesc = - AArch64_TranslateAddress (reset_vector_start address,acctype,iswrite,aligned,size) in - (if bitU_to_bool (IsFault memaddrdesc) - then AArch64_Abort (reset_vector_start address,memaddrdesc.AddressDescriptor_fault) - else return ()) >> - let passed = IsExclusiveLocal (memaddrdesc.AddressDescriptor_paddress,ProcessorID (),size) in - let passed = - if bitU_to_bool passed - then - let _ = ClearExclusiveLocal (ProcessorID ()) in - if bitU_to_bool memaddrdesc.AddressDescriptor_memattrs.MemoryAttributes_shareable - then IsExclusiveGlobal (memaddrdesc.AddressDescriptor_paddress,ProcessorID (),size) - else passed - else passed in - return (passed,passed)) >>= fun (w__0, passed) -> - return w__0 - -let decodeLoadsStores machineCode = - match machineCode with - | ((Vector [_;_;B0;B0;B1;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__80) -> - decodeLoadStoreExclusive (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;B0;B1;B1;_;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__99) -> - return (decodeLoadRegisterLiteral (reset_vector_start (set_vector_start_to_length machineCode))) - | ((Vector [_;_;B1;B0;B1;_;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__118) -> - decodeLoadStoreNoAllocatePairOffset - (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;B1;B0;B1;_;B0;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__137) -> - decodeLoadStoreRegisterPairPostIndexed - (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;B1;B0;B1;_;B0;B1;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__156) -> - decodeLoadStoreRegisterPairOffset (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;B1;B0;B1;_;B0;B1;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__175) -> - decodeLoadStoreRegisterPairPreIndexed - (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;B1;B1;B1;_;B0;B0;_;_;B0;_;_;_;_;_;_;_;_;_;B0;B0;_;_;_;_;_;_;_;_;_;_] _ _) as v__194) -> - decodeLoadStoreRegisterUnscaledImmediate - (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;B1;B1;B1;_;B0;B0;_;_;B0;_;_;_;_;_;_;_;_;_;B0;B1;_;_;_;_;_;_;_;_;_;_] _ _) as v__213) -> - decodeLoadStoreRegisterImmediatePostIndexed - (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;B1;B1;B1;_;B0;B0;_;_;B0;_;_;_;_;_;_;_;_;_;B1;B0;_;_;_;_;_;_;_;_;_;_] _ _) as v__232) -> - decodeLoadStoreRegisterUnprivileged - (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;B1;B1;B1;_;B0;B0;_;_;B0;_;_;_;_;_;_;_;_;_;B1;B1;_;_;_;_;_;_;_;_;_;_] _ _) as v__251) -> - decodeLoadStoreRegisterImmediatePreIndexed - (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;B1;B1;B1;_;B0;B0;_;_;B1;_;_;_;_;_;_;_;_;_;B1;B0;_;_;_;_;_;_;_;_;_;_] _ _) as v__270) -> - decodeLoadStoreRegisterRegisterOffset - (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;B1;B1;B1;_;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__289) -> - decodeLoadStoreRegisterUnsignedImmediate - (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [B0;_;B0;B0;B1;B1;B0;B0;B0;_;B0;B0;B0;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__308) -> - decodeAdvSIMDLoadStoreMultiStruct (reset_vector_start machineCode) - | ((Vector [B0;_;B0;B0;B1;B1;B0;B0;B1;_;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__327) -> - decodeAdvSIMDLoadStoreMultiStructPostIndexed (reset_vector_start machineCode) - | ((Vector [B0;_;B0;B0;B1;B1;B0;B1;B0;_;_;B0;B0;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__346) -> - decodeAdvSIMDLoadStoreSingleStruct (reset_vector_start machineCode) - | ((Vector [B0;_;B0;B0;B1;B1;B0;B1;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__365) -> - decodeAdvSIMDLoadStoreSingleStructPostIndexed (reset_vector_start machineCode) - end - -let S1TranslationRegime () = - read_reg_field CurrentEL "EL" >>= fun w__0 -> - if bitU_to_bool (neq_vec (set_vector_start_to_length w__0, set_vector_start_to_length EL0)) - then - read_reg_field CurrentEL "EL" >>= fun w__1 -> - return (set_vector_start 1 w__1) - else - IsSecure () >>= fun w__2 -> - return (if bitU_to_bool - (w__2 &. - ((HaveEL (reset_vector_start EL3)) &. (ELUsingAArch32 (reset_vector_start EL3)))) - then EL3 - else EL1) - -let AArch64_CheckForSMCTrap imm = - IsSecure () >>= fun w__0 -> - read_reg_field CurrentEL "EL" >>= fun w__1 -> - read_reg_field CurrentEL "EL" >>= fun w__2 -> - read_reg_bitfield HCR_EL2 "TSC" >>= fun w__3 -> - let route_to_el2 = - (HaveEL (reset_vector_start EL2)) &. - ((~w__0) &. - (((eq_vec (set_vector_start_to_length w__1, set_vector_start_to_length EL0)) |. - (eq_vec (set_vector_start_to_length w__2, set_vector_start_to_length EL1))) &. - (eq (match w__3 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))))) in - if bitU_to_bool route_to_el2 - then not_implemented "AArch64_CheckForSMCTrap route_to_el2" - else return () - -let CheckSystemAccess (op0, op1, crn, crm, op2, rt, read) = - let unallocated = B0 in - let need_secure = B0 in - let min_EL = to_vec_dec ((2:ii),(0:ii)) in - match op1 with - | ((Vector [B0;B0;_] _ _) as v__77) -> - let min_EL = EL1 in - return (need_secure,min_EL) - | Vector [B0;B1;B0] _ _ -> - let min_EL = EL1 in - return (need_secure,min_EL) - | Vector [B0;B1;B1] _ _ -> - let min_EL = EL0 in - return (need_secure,min_EL) - | Vector [B1;B0;B0] _ _ -> - let min_EL = EL2 in - return (need_secure,min_EL) - | Vector [B1;B0;B1] _ _ -> - UnallocatedEncoding () >> - return (need_secure,min_EL) - | Vector [B1;B1;B0] _ _ -> - let min_EL = EL3 in - return (need_secure,min_EL) - | Vector [B1;B1;B1] _ _ -> - let min_EL = EL1 in - let need_secure = B1 in - return (need_secure,min_EL) - end >>= fun (need_secure, min_EL) -> - read_reg_field CurrentEL "EL" >>= fun w__0 -> - if bitU_to_bool (lt_vec (set_vector_start_to_length w__0, set_vector_start_to_length min_EL)) - then UnallocatedEncoding () - else - IsSecure () >>= fun w__1 -> - if bitU_to_bool (need_secure &. (~w__1)) - then UnallocatedEncoding () - else - AArch64_CheckUnallocatedSystemAccess - (reset_vector_start op0, - reset_vector_start op1, - reset_vector_start crn, - reset_vector_start crm, - reset_vector_start op2, - read) >>= fun w__2 -> - if bitU_to_bool w__2 - then UnallocatedEncoding () - else return () - -let ExternalSecureInvasiveDebugEnabled () = - IsSecure () >>= fun w__0 -> - if bitU_to_bool ((~(HaveEL (reset_vector_start EL3))) &. (~w__0)) - then return B0 - else - ExternalInvasiveDebugEnabled () >>= fun w__1 -> - signalSPIDEN () >>= fun w__2 -> - return (w__1 &. (eq (w__2, HIGH))) - -let decodeDataImmediate machineCode = - match machineCode with - | ((Vector [_;_;_;B1;B0;B0;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__35) -> - return (decodePCRelAddressing (reset_vector_start (set_vector_start_to_length machineCode))) - | ((Vector [_;_;_;B1;B0;B0;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__42) -> - decodeAddSubtractImmediate (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;_;B1;B0;B0;B1;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__49) -> - decodeLogicalImmediate (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;_;B1;B0;B0;B1;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__56) -> - decodeMoveWideImmediate (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;_;B1;B0;B0;B1;B1;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__63) -> - decodeBitfield (reset_vector_start (set_vector_start_to_length machineCode)) - | ((Vector [_;_;_;B1;B0;B0;B1;B1;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__70) -> - decodeExtract (reset_vector_start (set_vector_start_to_length machineCode)) - end - -let SCTLR' () = - S1TranslationRegime () >>= fun w__0 -> - return (SCTLR (reset_vector_start w__0)) - -let HaltingAllowed () = - Halted () >>= fun w__0 -> - DoubleLockStatus () >>= fun w__1 -> - if bitU_to_bool (w__0 |. w__1) - then return B0 - else - IsSecure () >>= fun w__2 -> - if bitU_to_bool w__2 - then ExternalSecureInvasiveDebugEnabled () - else ExternalInvasiveDebugEnabled () - -let decode machineCode = - match machineCode with - | ((Vector [_;_;_;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__0) -> - return (Just (Unallocated)) - | ((Vector [_;_;_;B1;B0;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__5) -> - decodeDataImmediate (reset_vector_start machineCode) - | ((Vector [_;_;_;B1;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__10) -> - decodeBranchesExceptionSystem (reset_vector_start machineCode) - | ((Vector [_;_;_;_;B1;_;B0;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__15) -> - decodeLoadsStores (reset_vector_start machineCode) - | ((Vector [_;_;_;_;B1;B0;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__20) -> - decodeDataRegister (reset_vector_start machineCode) - | ((Vector [_;_;_;B0;B1;B1;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__25) -> - decodeDataSIMDFPoint1 (reset_vector_start machineCode) - | ((Vector [_;_;_;B1;B1;B1;B1;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_;_] _ _) as v__30) -> - decodeDataSIMDFPoint2 (reset_vector_start machineCode) - | _ -> return (Nothing) - end - -let BigEndian () = - let bigend = B0 in - if bitU_to_bool (UsingAArch32 ()) - then - read_reg PSTATE_E >>= fun w__0 -> - let bigend = neq_vec_range (w__0, (0:ii)) in - return bigend - else - read_reg_field CurrentEL "EL" >>= fun w__1 -> - if bitU_to_bool (eq_vec (set_vector_start_to_length w__1, set_vector_start_to_length EL0)) - then - read_reg_bitfield SCTLR_EL1 "E0E" >>= fun w__2 -> - let bigend = neq (match w__2 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)) in - return bigend - else - SCTLR' () >>= fun w__3 -> - read_reg_bitfield w__3 "EE" >>= fun w__4 -> - let bigend = neq (match w__4 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)) in - return bigend - -let flush_read_buffer (read_buffer, size) = - let _ = assert' (eq_range (read_buffer.read_buffer_type_size, size)) (Nothing) in - let value = set_vector_start_to_length (to_vec_dec (size * (8:ii),(0:ii))) in - (if bitU_to_bool read_buffer.read_buffer_type_exclusive - then - match read_buffer.read_buffer_type_acctype with - | AccType_ATOMIC -> - rMem_ATOMIC - (reset_vector_start read_buffer.read_buffer_type_address, - read_buffer.read_buffer_type_size) >>= fun w__0 -> - return (set_vector_start_to_length w__0) - | AccType_ORDERED -> - rMem_ATOMIC_ORDERED - (reset_vector_start read_buffer.read_buffer_type_address, - read_buffer.read_buffer_type_size) >>= fun w__1 -> - return (set_vector_start_to_length w__1) - | _ -> - not_implemented "unimplemented memory access" >> - return value - end - else - match read_buffer.read_buffer_type_acctype with - | AccType_NORMAL -> - rMem_NORMAL - (reset_vector_start read_buffer.read_buffer_type_address, - read_buffer.read_buffer_type_size) >>= fun w__2 -> - return (set_vector_start_to_length w__2) - | AccType_STREAM -> - rMem_STREAM - (reset_vector_start read_buffer.read_buffer_type_address, - read_buffer.read_buffer_type_size) >>= fun w__3 -> - return (set_vector_start_to_length w__3) - | AccType_UNPRIV -> - rMem_NORMAL - (reset_vector_start read_buffer.read_buffer_type_address, - read_buffer.read_buffer_type_size) >>= fun w__4 -> - return (set_vector_start_to_length w__4) - | AccType_ORDERED -> - rMem_ORDERED - (reset_vector_start read_buffer.read_buffer_type_address, - read_buffer.read_buffer_type_size) >>= fun w__5 -> - return (set_vector_start_to_length w__5) - | AccType_ATOMIC -> return value - end) >>= fun value -> - BigEndian () >>= fun w__6 -> - let value = - if bitU_to_bool w__6 - then - set_vector_start_to_length - (BigEndianReverse (reset_vector_start (set_vector_start_to_length value))) - else value in - return (set_vector_start_to_length value) - -let CheckSPAlignment () = - rSP (64:ii) >>= fun sp -> - let stack_align_check = B0 in - read_reg_field CurrentEL "EL" >>= fun w__0 -> - (if bitU_to_bool (eq_vec (set_vector_start_to_length w__0, set_vector_start_to_length EL0)) - then - read_reg_bitfield SCTLR_EL1 "SA0" >>= fun w__1 -> - let stack_align_check = neq (match w__1 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)) in - return stack_align_check - else - SCTLR' () >>= fun w__2 -> - read_reg_bitfield w__2 "SA" >>= fun w__3 -> - let stack_align_check = neq (match w__3 with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii)) in - return stack_align_check) >>= fun stack_align_check -> - if bitU_to_bool - (stack_align_check &. - (neq_vec - (set_vector_start_to_length sp, - set_vector_start_to_length - (Align (reset_vector_start (set_vector_start_to_length sp),(16:ii)))))) - then AArch64_SPAlignmentFault () - else return () - -let AArch64_CheckAlignment (address, size, acctype, iswrite) = - let aligned = - eq_vec - (set_vector_start_to_length address, - set_vector_start_to_length - (Align (reset_vector_start (set_vector_start_to_length address),size))) in - SCTLR' () >>= fun w__0 -> - read_reg_bitfield w__0 "A" >>= fun A -> - (if bitU_to_bool - ((~aligned) &. - ((eq (acctype, AccType_ATOMIC)) |. - ((eq (acctype, AccType_ORDERED)) |. - (eq (match A with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii)))))) - then - let secondstage = B0 in - AArch64_Abort (reset_vector_start address,AArch64_AlignmentFault (acctype,iswrite,secondstage)) - else return ()) >> - return aligned - -let rMem' (read_buffer, address, size, acctype, exclusive) = - let read_buffer' = read_buffer in - let i = (0:ii) in - let iswrite = B0 in - AArch64_CheckAlignment (reset_vector_start address,size,acctype,iswrite) >>= fun aligned -> - let atomic = - (aligned &. (~((eq (acctype, AccType_VEC)) |. (eq (acctype, AccType_VECSTREAM))))) |. - (eq_range (size, (1:ii))) in - if bitU_to_bool (~atomic) - then - let _ = assert' (~exclusive) (Nothing) in - let _ = assert' (gt (size, (1:ii))) (Nothing) in - if bitU_to_bool (~exclusive) - then - AArch64_rMemSingle (read_buffer',reset_vector_start address,(1:ii),acctype,aligned,B0) >>= fun w__0 -> - let read_buffer' = w__0 in - (foreachM_inc ((1:ii),size - (1:ii),(1:ii)) read_buffer' - (fun i read_buffer' -> - AArch64_rMemSingle - (read_buffer', - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) i)), - (1:ii), - acctype, - aligned, - B0))) - else return read_buffer' - else AArch64_rMemSingle (read_buffer',reset_vector_start address,size,acctype,aligned,exclusive) - -let wMem' (write_buffer, address, size, acctype, value, exclusive) = - let write_buffer' = write_buffer in - let value' = set_vector_start_to_length value in - let i = (0:ii) in - let iswrite = B1 in - BigEndian () >>= fun w__0 -> - let value' = - if bitU_to_bool w__0 - then - set_vector_start_to_length - (BigEndianReverse (reset_vector_start (set_vector_start_to_length value'))) - else value' in - AArch64_CheckAlignment (reset_vector_start address,size,acctype,iswrite) >>= fun aligned -> - let atomic = - (aligned &. (~((eq (acctype, AccType_VEC)) |. (eq (acctype, AccType_VECSTREAM))))) |. - (eq_range (size, (1:ii))) in - let exclusiveSuccess = B0 in - if bitU_to_bool (~atomic) - then - let _ = assert' (~exclusive) (Nothing) in - if bitU_to_bool (~exclusive) - then - let _ = assert' (gt (size, (1:ii))) (Nothing) in - AArch64_wMemSingle - (write_buffer', - reset_vector_start address, - (1:ii), - acctype, - aligned, - B0, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length value') (7:ii) (0:ii)))) >>= fun w__1 -> - let write_buffer' = w__1 in - (foreachM_inc ((1:ii),size - (1:ii),(1:ii)) write_buffer' - (fun i write_buffer' -> - AArch64_wMemSingle - (write_buffer', - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) i)), - (1:ii), - acctype, - aligned, - B0, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length value') (((8:ii) * i) + (7:ii)) ((8:ii) * i)))))) - else return write_buffer' - else - AArch64_wMemSingle - (write_buffer', - reset_vector_start address, - size, - acctype, - aligned, - exclusive, - reset_vector_start (set_vector_start_to_length value')) - -let rMem (read_buffer, address, size, acctype) = - rMem' (read_buffer,reset_vector_start address,size,acctype,B0) - -let rMem_exclusive (read_buffer, address, size, acctype) = - rMem' (read_buffer,reset_vector_start address,size,acctype,B1) - -let wMem (write_buffer, address, size, acctype, value) = - wMem' - (write_buffer, - reset_vector_start address, - size, - acctype, - reset_vector_start (set_vector_start_to_length value), - B0) - -let wMem_exclusive (write_buffer, address, size, acctype, value) = - wMem' - (write_buffer, - reset_vector_start address, - size, - acctype, - reset_vector_start (set_vector_start_to_length value), - B1) - - - -let execute_TMStart t = - read_reg TxNestingLevel >>= fun nesting -> - read_reg_field TXIDR_EL0 "DEPTH" >>= fun w__0 -> - if bitU_to_bool - (lt_vec_unsigned (set_vector_start_to_length nesting, set_vector_start_to_length w__0)) - then - write_reg - TxNestingLevel - (set_vector_start 7 (add_VIV (reset_vector_start (set_vector_start_to_length nesting)) (1:ii))) >> - let status = to_vec_dec ((64:ii),(0:ii)) in - (if bitU_to_bool (eq_vec_range (set_vector_start_to_length nesting, (0:ii))) - then read_reg TMStartEffect - else return status) >>= fun status -> - wX (t,reset_vector_start (set_vector_start_to_length status)) - else - let status = to_vec_dec ((64:ii),(0:ii)) in - let status = update_pos status (10:ii) B1 in - write_reg TMAbortEffect status - -let execute_TMCommit () = - read_reg TxNestingLevel >>= fun nesting -> - (if bitU_to_bool (eq_vec_range (set_vector_start_to_length nesting, (1:ii))) - then TMCommitEffect () - else - if bitU_to_bool (eq_vec_range (set_vector_start_to_length nesting, (0:ii))) - then AArch64_UndefinedFault () - else return ()) >> - write_reg - TxNestingLevel - (set_vector_start 7 (minus_VIV (reset_vector_start (set_vector_start_to_length nesting)) (1:ii))) - -let execute_TMTest () = - read_reg TxNestingLevel >>= fun w__0 -> - if bitU_to_bool (gt_vec_range (w__0, (0:ii))) - then wPSTATE_NZCV ((),reset_vector_start (Vector [B0;B0;B0;B0] 3 false)) - else wPSTATE_NZCV ((),reset_vector_start (Vector [B0;B1;B0;B0] 3 false)) - -let execute_TMAbort (retry, reason) = - read_reg TxNestingLevel >>= fun w__0 -> - if bitU_to_bool (gt_vec_range (w__0, (0:ii))) - then - let status = to_vec_dec ((64:ii),(0:ii)) in - let status = update status (4:ii) (0:ii) reason in - let status = update_pos status (8:ii) retry in - let status = update_pos status (9:ii) B1 in - write_reg TMAbortEffect status - else return () - -let execute_CompareAndBranch (t, datasize, iszero, offset) = - rX (datasize,t) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - if bitU_to_bool - (eq_bit (IsZero (reset_vector_start (set_vector_start_to_length operand1)), iszero)) - then - rPC () >>= fun w__1 -> - BranchTo - (reset_vector_start (set_vector_start_to_length - (add_VVV - (reset_vector_start (set_vector_start_to_length w__1)) - (reset_vector_start (set_vector_start_to_length offset)))), - BranchType_JMP) - else return () - -let execute_BranchConditional (offset, condition) = - ConditionHolds (reset_vector_start condition) >>= fun w__0 -> - if bitU_to_bool w__0 - then - rPC () >>= fun w__1 -> - BranchTo - (reset_vector_start (set_vector_start_to_length - (add_VVV - (reset_vector_start (set_vector_start_to_length w__1)) - (reset_vector_start (set_vector_start_to_length offset)))), - BranchType_JMP) - else return () - -let execute_GenerateExceptionEL1 imm = AArch64_CallSupervisor (reset_vector_start imm) - -let execute_GenerateExceptionEL2 imm = - read_reg_field CurrentEL "EL" >>= fun w__0 -> - read_reg_field CurrentEL "EL" >>= fun w__1 -> - IsSecure () >>= fun w__2 -> - (if bitU_to_bool - ((~(HaveEL (reset_vector_start EL2))) |. - ((eq_vec (set_vector_start_to_length w__0, set_vector_start_to_length EL0)) |. - ((eq_vec (set_vector_start_to_length w__1, set_vector_start_to_length EL1)) &. w__2))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool (HaveEL (reset_vector_start EL3)) - then read_reg_bitfield SCR_EL3 "HCE" - else - read_reg_bitfield HCR_EL2 "HCD" >>= fun w__4 -> - return (NOT' w__4)) >>= fun hvc_enable -> - if bitU_to_bool (eq (match hvc_enable with | B0 -> (0:ii) | B1 -> (1:ii) end, (0:ii))) - then AArch64_UndefinedFault () - else AArch64_CallHypervisor (reset_vector_start imm) - -let execute_GenerateExceptionEL3 imm = - read_reg_field CurrentEL "EL" >>= fun w__0 -> - (if bitU_to_bool - ((~(HaveEL (reset_vector_start EL3))) |. - (eq_vec (set_vector_start_to_length w__0, set_vector_start_to_length EL0))) - then UnallocatedEncoding () - else return ()) >> - AArch64_CheckForSMCTrap (reset_vector_start imm) >> - read_reg_bitfield SCR_EL3 "SMD" >>= fun w__1 -> - if bitU_to_bool (eq (match w__1 with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then AArch64_UndefinedFault () - else AArch64_CallSecureMonitor (reset_vector_start imm) - -let execute_DebugBreakpoint comment = AArch64_SoftwareBreakpoint (reset_vector_start comment) - -let execute_ExternalDebugBreakpoint () = Halt (reset_vector_start DebugHalt_HaltInstruction) - -let execute_DebugSwitchToExceptionLevel target_level = - DCPSInstruction (reset_vector_start target_level) - -let execute_MoveSystemImmediate (operand, field') = - match field' with - | PSTATEField_SP -> write_reg_bitfield SPSel "SP" (access operand (0:ii)) - | PSTATEField_DAIFSet -> - read_reg_bitfield DAIF "D" >>= fun w__0 -> - write_reg_bitfield DAIF "D" (w__0 |. (access operand (3:ii))) >> - read_reg_bitfield DAIF "A" >>= fun w__1 -> - write_reg_bitfield DAIF "A" (w__1 |. (access operand (2:ii))) >> - read_reg_bitfield DAIF "I" >>= fun w__2 -> - write_reg_bitfield DAIF "I" (w__2 |. (access operand (1:ii))) >> - read_reg_bitfield DAIF "F" >>= fun w__3 -> - write_reg_bitfield DAIF "F" (w__3 |. (access operand (0:ii))) - | PSTATEField_DAIFClr -> - read_reg_bitfield DAIF "D" >>= fun w__4 -> - write_reg_bitfield DAIF "D" (w__4 &. (NOT' (access operand (3:ii)))) >> - read_reg_bitfield DAIF "A" >>= fun w__5 -> - write_reg_bitfield DAIF "A" (w__5 &. (NOT' (access operand (2:ii)))) >> - read_reg_bitfield DAIF "I" >>= fun w__6 -> - write_reg_bitfield DAIF "I" (w__6 &. (NOT' (access operand (1:ii)))) >> - read_reg_bitfield DAIF "F" >>= fun w__7 -> - write_reg_bitfield DAIF "F" (w__7 &. (NOT' (access operand (0:ii)))) - end - -let execute_Hint op = - match op with - | SystemHintOp_YIELD -> return (Hint_Yield ()) - | SystemHintOp_WFE -> - EventRegistered () >>= fun w__0 -> - if bitU_to_bool w__0 - then ClearEventRegister () - else - read_reg_field CurrentEL "EL" >>= fun w__1 -> - (if bitU_to_bool (eq_vec (set_vector_start_to_length w__1, set_vector_start_to_length EL0)) - then AArch64_CheckForWFxTrap (reset_vector_start EL1,B1) - else return ()) >> - IsSecure () >>= fun w__2 -> - read_reg_field CurrentEL "EL" >>= fun w__3 -> - read_reg_field CurrentEL "EL" >>= fun w__4 -> - (if bitU_to_bool - ((HaveEL (reset_vector_start EL2)) &. - ((~w__2) &. - ((eq_vec (set_vector_start_to_length w__3, set_vector_start_to_length EL0)) |. - (eq_vec (set_vector_start_to_length w__4, set_vector_start_to_length EL1))))) - then AArch64_CheckForWFxTrap (reset_vector_start EL2,B1) - else return ()) >> - read_reg_field CurrentEL "EL" >>= fun w__5 -> - (if bitU_to_bool - ((HaveEL (reset_vector_start EL3)) &. - (neq_vec (set_vector_start_to_length w__5, set_vector_start_to_length EL3))) - then AArch64_CheckForWFxTrap (reset_vector_start EL3,B1) - else return ()) >> - WaitForEvent () - | SystemHintOp_WFI -> - InterruptPending () >>= fun w__6 -> - if bitU_to_bool (~w__6) - then - read_reg_field CurrentEL "EL" >>= fun w__7 -> - (if bitU_to_bool (eq_vec (set_vector_start_to_length w__7, set_vector_start_to_length EL0)) - then AArch64_CheckForWFxTrap (reset_vector_start EL1,B0) - else return ()) >> - IsSecure () >>= fun w__8 -> - read_reg_field CurrentEL "EL" >>= fun w__9 -> - read_reg_field CurrentEL "EL" >>= fun w__10 -> - (if bitU_to_bool - ((HaveEL (reset_vector_start EL2)) &. - ((~w__8) &. - ((eq_vec (set_vector_start_to_length w__9, set_vector_start_to_length EL0)) |. - (eq_vec (set_vector_start_to_length w__10, set_vector_start_to_length EL1))))) - then AArch64_CheckForWFxTrap (reset_vector_start EL2,B0) - else return ()) >> - read_reg_field CurrentEL "EL" >>= fun w__11 -> - (if bitU_to_bool - ((HaveEL (reset_vector_start EL3)) &. - (neq_vec (set_vector_start_to_length w__11, set_vector_start_to_length EL3))) - then AArch64_CheckForWFxTrap (reset_vector_start EL3,B0) - else return ()) >> - WaitForInterrupt () - else return () - | SystemHintOp_SEV -> return (SendEvent ()) - | SystemHintOp_SEVL -> EventRegisterSet () - | _ -> return () - end - -let execute_ClearExclusiveMonitor imm = return (ClearExclusiveLocal (ProcessorID ())) - -let execute_Barrier (op, domain, types) = - match op with - | MemBarrierOp_DSB -> DataSynchronizationBarrier (domain,types) - | MemBarrierOp_DMB -> DataMemoryBarrier (domain,types) - | MemBarrierOp_ISB -> InstructionSynchronizationBarrier () - end - -let execute_System (t, sys_op0, sys_op1, sys_op2, sys_crn, sys_crm, has_result) = - if bitU_to_bool has_result - then - SysOp_R (sys_op0,sys_op1,sys_crn,sys_crm,sys_op2) >>= fun w__0 -> - wX (t,reset_vector_start (set_vector_start_to_length w__0)) - else - rX ((64:ii),t) >>= fun w__1 -> - SysOp_W (sys_op0,sys_op1,sys_crn,sys_crm,sys_op2,reset_vector_start w__1) - -let execute_MoveSystemRegister (t, sys_op0, sys_op1, sys_op2, sys_crn, sys_crm, read) = - if bitU_to_bool read - then - System_Get (sys_op0,sys_op1,sys_crn,sys_crm,sys_op2) >>= fun w__0 -> - wX (t,reset_vector_start (set_vector_start_to_length w__0)) - else - rX ((64:ii),t) >>= fun w__1 -> - System_Put (sys_op0,sys_op1,sys_crn,sys_crm,sys_op2,reset_vector_start w__1) - -let execute_ImplementationDefinedTestBeginEnd isEnd = - return (if bitU_to_bool isEnd - then info "test ends" - else info "test begins") - -let execute_ImplementationDefinedStopFetching () = return (info "stop fetching instructions") - -let execute_ImplementationDefinedThreadStart () = return (info "thread start") - -let execute_TestBitAndBranch (t, datasize, bit_pos, bit_val, offset) = - rX (datasize,t) >>= fun w__0 -> - let operand = set_vector_start_to_length w__0 in - if bitU_to_bool (eq_bit (access (set_vector_start_to_length operand) bit_pos, bit_val)) - then - rPC () >>= fun w__1 -> - BranchTo - (reset_vector_start (set_vector_start_to_length - (add_VVV - (reset_vector_start (set_vector_start_to_length w__1)) - (reset_vector_start (set_vector_start_to_length offset)))), - BranchType_JMP) - else return () - -let execute_BranchImmediate (branch_type, offset) = - (if bitU_to_bool (eq (branch_type, BranchType_CALL)) - then - rPC () >>= fun w__0 -> - wX - ((30:ii), - reset_vector_start (set_vector_start_to_length - (add_VIV (reset_vector_start (set_vector_start_to_length w__0)) (4:ii)))) - else return ()) >> - rPC () >>= fun w__1 -> - BranchTo - (reset_vector_start (set_vector_start_to_length - (add_VVV - (reset_vector_start (set_vector_start_to_length w__1)) - (reset_vector_start (set_vector_start_to_length offset)))), - branch_type) - -let execute_BranchRegister (n, branch_type) = - rX ((64:ii),n) >>= fun target -> - (if bitU_to_bool (eq (branch_type, BranchType_CALL)) - then - rPC () >>= fun w__0 -> - wX - ((30:ii), - reset_vector_start (set_vector_start_to_length - (add_VIV (reset_vector_start (set_vector_start_to_length w__0)) (4:ii)))) - else return ()) >> - BranchTo (reset_vector_start (set_vector_start_to_length target),branch_type) - -let execute_ExceptionReturn () = - rELR' () >>= fun w__0 -> - rSPSR () >>= fun w__1 -> - AArch64_ExceptionReturn (reset_vector_start w__0,reset_vector_start w__1) - -let execute_DebugRestorePState () = DRPSInstruction () - -let execute_LoadLiteral (t, memop, _signed, size, offset, datasize) = - rPC () >>= fun w__0 -> - let address = - set_vector_start 63 - (add_VVV - (reset_vector_start (set_vector_start_to_length w__0)) - (reset_vector_start (set_vector_start_to_length offset))) in - let data = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - match memop with - | MemOp_LOAD -> - rMem (empty_read_buffer,reset_vector_start address,size,AccType_NORMAL) >>= fun w__1 -> - flush_read_buffer (w__1,size) >>= fun w__2 -> - let data = set_vector_start_to_length w__2 in - (if bitU_to_bool _signed - then - wX - (t, - reset_vector_start (set_vector_start_to_length - (SignExtend ((64:ii),reset_vector_start (set_vector_start_to_length data))))) - else wX (t,reset_vector_start (set_vector_start_to_length data))) >> - return data - | MemOp_PREFETCH -> return data - end >>= fun data -> - return () - -let execute_LoadStoreAcqExc (n, t, t2, s, acctype, excl, pair, memop, elsize, regsize, datasize) = - let address = to_vec_dec ((64:ii),(0:ii)) in - let data = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - let dbytes = quot datasize (8:ii) in - let rt_unknown = B0 in - let rn_unknown = B0 in - (if bitU_to_bool ((eq (memop, MemOp_LOAD)) &. (pair &. (eq_range (t, t2)))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool ((eq (memop, MemOp_STORE)) &. excl) - then - (if bitU_to_bool ((eq_range (s, t)) |. (pair &. (eq_range (s, t2)))) - then UnallocatedEncoding () - else return ()) >> - if bitU_to_bool ((eq_range (s, n)) &. (neq_range (n, (31:ii)))) - then UnallocatedEncoding () - else return () - else return ()) >> - let status = B0 in - (if bitU_to_bool ((eq (memop, MemOp_STORE)) &. excl) - then - speculate_exclusive_success () >>= fun w__0 -> - let status = if bitU_to_bool w__0 then B0 else B1 in - wX - (s, - reset_vector_start (set_vector_start_to_length - (ZeroExtend - ((32:ii), - reset_vector_start (set_vector_start_to_length (Vector [status] 0 false)))))) >> - return status - else return status) >>= fun status -> - (if bitU_to_bool (eq (match status with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then return (address,data,status) - else - (if bitU_to_bool (eq_range (n, (31:ii))) - then - CheckSPAlignment () >> - rSP (64:ii) - else - if bitU_to_bool rn_unknown - then - let address = to_vec_dec ((64:ii),UNKNOWN) in - return address - else rX ((64:ii),n)) >>= fun address -> - match memop with - | MemOp_STORE -> - wMem_Addr (reset_vector_start address,dbytes,acctype,excl) >> - (if bitU_to_bool rt_unknown - then - let data = set_vector_start_to_length (to_vec_dec (length data,UNKNOWN)) in - return data - else - if bitU_to_bool pair - then - let _ = assert' excl (Nothing) in - rX (regsize,t) >>= fun w__3 -> - let el1 = set_vector_start_to_length w__3 in - rX (length el1,t2) >>= fun w__4 -> - let el2 = set_vector_start_to_length w__4 in - BigEndian () >>= fun w__5 -> - let data = - if bitU_to_bool w__5 - then - set_vector_start_to_length - ((set_vector_start_to_length el1) ^^ (set_vector_start_to_length el2)) - else - set_vector_start_to_length - ((set_vector_start_to_length el2) ^^ (set_vector_start_to_length el1)) in - return data - else - rX (length data,t) >>= fun w__6 -> - return (set_vector_start_to_length w__6)) >>= fun data -> - (if bitU_to_bool excl - then - let status = B1 in - AArch64_ExclusiveMonitorsPass (reset_vector_start address,dbytes) >>= fun w__7 -> - if bitU_to_bool w__7 - then - wMem_exclusive - (empty_write_buffer, - reset_vector_start address, - dbytes, - acctype, - reset_vector_start (set_vector_start_to_length data)) >>= fun w__8 -> - flush_write_buffer_exclusive w__8 - else return status - else - wMem - (empty_write_buffer, - reset_vector_start address, - dbytes, - acctype, - reset_vector_start (set_vector_start_to_length data)) >>= fun w__10 -> - flush_write_buffer w__10 >> - return status) >>= fun status -> - return (data,status) - | MemOp_LOAD -> - let _ = - if bitU_to_bool excl - then AArch64_SetExclusiveMonitors (reset_vector_start address,dbytes) - else () in - (if bitU_to_bool pair - then - let _ = assert' excl (Nothing) in - if bitU_to_bool rt_unknown - then - wX - (t, - reset_vector_start (set_vector_start_to_length (to_vec_dec (length data,UNKNOWN)))) >> - return data - else - if bitU_to_bool (eq_range (elsize, (32:ii))) - then - rMem_exclusive (empty_read_buffer,reset_vector_start address,dbytes,acctype) >>= fun w__11 -> - flush_read_buffer (w__11,dbytes) >>= fun w__12 -> - let data = set_vector_start_to_length w__12 in - BigEndian () >>= fun w__13 -> - (if bitU_to_bool w__13 - then - wX - (t, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length data) (datasize - (1:ii)) elsize))) >> - wX - (t2, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length data) (elsize - (1:ii)) (0:ii)))) - else - wX - (t, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length data) (elsize - (1:ii)) (0:ii)))) >> - wX - (t2, - reset_vector_start (set_vector_start_to_length - (slice (set_vector_start_to_length data) (datasize - (1:ii)) elsize)))) >> - return data - else - (if bitU_to_bool - (neq_vec - (set_vector_start_to_length address, - set_vector_start_to_length - (Align (reset_vector_start (set_vector_start_to_length address),dbytes)))) - then - let iswrite = B0 in - let secondstage = B0 in - AArch64_Abort - (reset_vector_start address, - AArch64_AlignmentFault (acctype,iswrite,secondstage)) - else return ()) >> - rMem_exclusive - (empty_read_buffer, - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) (0:ii))), - (8:ii), - acctype) >>= fun read_buffer -> - rMem_exclusive - (read_buffer, - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) (8:ii))), - (8:ii), - acctype) >>= fun w__14 -> - let read_buffer = w__14 in - flush_read_buffer (read_buffer,(8:ii) * (2:ii)) >>= fun w__15 -> - let value = set_vector_start 127 w__15 in - wX (t,reset_vector_start (set_vector_start_to_length (slice value (63:ii) (0:ii)))) >> - wX - (t2, - reset_vector_start (set_vector_start_to_length (slice value (127:ii) (64:ii)))) >> - return data - else - rMem' (empty_read_buffer,reset_vector_start address,dbytes,acctype,excl) >>= fun w__16 -> - flush_read_buffer (w__16,dbytes) >>= fun w__17 -> - let data = set_vector_start_to_length w__17 in - wX - (t, - reset_vector_start (set_vector_start_to_length - (set_vector_start_to_length - (ZeroExtend (regsize,reset_vector_start (set_vector_start_to_length data)))))) >> - return data) >>= fun data -> - return (data,status) - end >>= fun (data, status) -> - return (address,data,status)) >>= fun (address, data, status) -> - return () - -let execute_LoadStorePairNonTemp (wback, postindex, n, t, t2, acctype, memop, scale, datasize, offset) = - let address = to_vec_dec ((64:ii),(0:ii)) in - let data1 = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - let data2 = set_vector_start_to_length (to_vec_dec (length data1,(0:ii))) in - let dbytes = quot datasize (8:ii) in - let rt_unknown = B0 in - (if bitU_to_bool ((eq (memop, MemOp_LOAD)) &. (eq_range (t, t2))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool (eq_range (n, (31:ii))) - then - CheckSPAlignment () >> - rSP (64:ii) - else rX ((64:ii),n)) >>= fun address -> - let address = - if bitU_to_bool (~postindex) - then - set_vector_start 63 - (add_VVV - (reset_vector_start (set_vector_start_to_length address)) - (reset_vector_start (set_vector_start_to_length offset))) - else address in - (if bitU_to_bool (eq (memop, MemOp_STORE)) - then wMem_Addr (reset_vector_start address,dbytes * (2:ii),acctype,B0) - else return ()) >> - (if bitU_to_bool wback - then - let address' = - if bitU_to_bool (~postindex) - then address - else - add_VVV - (reset_vector_start (set_vector_start_to_length address)) - (reset_vector_start (set_vector_start_to_length offset)) in - if bitU_to_bool (eq_range (n, (31:ii))) - then wSP ((),reset_vector_start (set_vector_start_to_length address')) - else wX (n,reset_vector_start (set_vector_start_to_length address')) - else return ()) >> - match memop with - | MemOp_STORE -> - (if bitU_to_bool (rt_unknown &. (eq_range (t, n))) - then - let data1 = set_vector_start_to_length (to_vec_dec (length data1,UNKNOWN)) in - return data1 - else - rX (length data1,t) >>= fun w__2 -> - return (set_vector_start_to_length w__2)) >>= fun data1 -> - (if bitU_to_bool (rt_unknown &. (eq_range (t2, n))) - then - let data2 = set_vector_start_to_length (to_vec_dec (length data1,UNKNOWN)) in - return data2 - else - rX (length data1,t2) >>= fun w__3 -> - return (set_vector_start_to_length w__3)) >>= fun data2 -> - wMem - (empty_write_buffer, - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) (0:ii))), - dbytes, - acctype, - reset_vector_start (set_vector_start_to_length data1)) >>= fun write_buffer -> - wMem - (write_buffer, - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) dbytes)), - dbytes, - acctype, - reset_vector_start (set_vector_start_to_length data2)) >>= fun w__4 -> - let write_buffer = w__4 in - flush_write_buffer write_buffer >> - return (data1,data2) - | MemOp_LOAD -> - rMem - (empty_read_buffer, - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) (0:ii))), - dbytes, - acctype) >>= fun read_buffer -> - rMem - (read_buffer, - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) dbytes)), - dbytes, - acctype) >>= fun w__5 -> - let read_buffer = w__5 in - flush_read_buffer (read_buffer,dbytes * (2:ii)) >>= fun w__6 -> - let read_data = set_vector_start_to_length w__6 in - let data1 = - set_vector_start_to_length - (slice (set_vector_start_to_length read_data) (datasize - (1:ii)) (0:ii)) in - let data2 = - set_vector_start_to_length - (slice (set_vector_start_to_length read_data) ((datasize * (2:ii)) - (1:ii)) datasize) in - let (data1, data2) = - if bitU_to_bool rt_unknown - then - let data1 = set_vector_start_to_length (to_vec_dec (length data1,UNKNOWN)) in - let data2 = set_vector_start_to_length (to_vec_dec (length data1,UNKNOWN)) in - (data1,data2) - else (data1,data2) in - wX (t,reset_vector_start (set_vector_start_to_length data1)) >> - wX (t2,reset_vector_start (set_vector_start_to_length data2)) >> - return (data1,data2) - end >>= fun (data1, data2) -> - return () - -let execute_LoadImmediate (n, t, acctype, memop, _signed, wback, postindex, offset, regsize, datasize) = - let address = to_vec_dec ((64:ii),(0:ii)) in - let data = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - let wb_unknown = B0 in - let rt_unknown = B0 in - (if bitU_to_bool - ((eq (memop, MemOp_LOAD)) &. (wback &. ((eq_range (n, t)) &. (neq_range (n, (31:ii)))))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool - ((eq (memop, MemOp_STORE)) &. (wback &. ((eq_range (n, t)) &. (neq_range (n, (31:ii)))))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool (eq_range (n, (31:ii))) - then - (if bitU_to_bool (neq (memop, MemOp_PREFETCH)) - then CheckSPAlignment () - else return ()) >> - rSP (64:ii) - else rX ((64:ii),n)) >>= fun address -> - let address = - if bitU_to_bool (~postindex) - then - set_vector_start 63 - (add_VVV - (reset_vector_start (set_vector_start_to_length address)) - (reset_vector_start (set_vector_start_to_length offset))) - else address in - (if bitU_to_bool (eq (memop, MemOp_STORE)) - then wMem_Addr (reset_vector_start address,quot datasize (8:ii),acctype,B0) - else return ()) >> - (if bitU_to_bool wback - then - let address' = - if bitU_to_bool (~postindex) - then address - else - add_VVV - (reset_vector_start (set_vector_start_to_length address)) - (reset_vector_start (set_vector_start_to_length offset)) in - if bitU_to_bool (eq_range (n, (31:ii))) - then wSP ((),reset_vector_start (set_vector_start_to_length address')) - else wX (n,reset_vector_start (set_vector_start_to_length address')) - else return ()) >> - match memop with - | MemOp_STORE -> - (if bitU_to_bool rt_unknown - then - let data = set_vector_start_to_length (to_vec_dec (length data,UNKNOWN)) in - return data - else - rX (length data,t) >>= fun w__2 -> - return (set_vector_start_to_length w__2)) >>= fun data -> - wMem - (empty_write_buffer, - reset_vector_start address, - quot datasize (8:ii), - acctype, - reset_vector_start (set_vector_start_to_length data)) >>= fun w__3 -> - flush_write_buffer w__3 >> - return data - | MemOp_LOAD -> - rMem (empty_read_buffer,reset_vector_start address,quot datasize (8:ii),acctype) >>= fun w__4 -> - flush_read_buffer (w__4,quot datasize (8:ii)) >>= fun w__5 -> - let data = set_vector_start_to_length w__5 in - (if bitU_to_bool _signed - then - wX - (t, - reset_vector_start (set_vector_start_to_length - (set_vector_start_to_length - (SignExtend (regsize,reset_vector_start (set_vector_start_to_length data)))))) - else - wX - (t, - reset_vector_start (set_vector_start_to_length - (set_vector_start_to_length - (ZeroExtend (regsize,reset_vector_start (set_vector_start_to_length data))))))) >> - return data - | MemOp_PREFETCH -> return data - end >>= fun data -> - return () - -let execute_LoadRegister (n, t, m, acctype, memop, _signed, wback, postindex, extend_type, shift, regsize, datasize) = - ExtendReg ((64:ii),m,extend_type,shift) >>= fun offset -> - let address = to_vec_dec ((64:ii),(0:ii)) in - let data = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - let wb_unknown = B0 in - let rt_unknown = B0 in - (if bitU_to_bool - ((eq (memop, MemOp_LOAD)) &. (wback &. ((eq_range (n, t)) &. (neq_range (n, (31:ii)))))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool - ((eq (memop, MemOp_STORE)) &. (wback &. ((eq_range (n, t)) &. (neq_range (n, (31:ii)))))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool (eq_range (n, (31:ii))) - then - (if bitU_to_bool (neq (memop, MemOp_PREFETCH)) - then CheckSPAlignment () - else return ()) >> - rSP (64:ii) - else rX ((64:ii),n)) >>= fun address -> - let address = - if bitU_to_bool (~postindex) - then - set_vector_start 63 - (add_VVV - (reset_vector_start (set_vector_start_to_length address)) - (reset_vector_start (set_vector_start_to_length offset))) - else address in - (if bitU_to_bool (eq (memop, MemOp_STORE)) - then wMem_Addr (reset_vector_start address,quot datasize (8:ii),acctype,B0) - else return ()) >> - (if bitU_to_bool wback - then - let address' = - if bitU_to_bool (~postindex) - then address - else - add_VVV - (reset_vector_start (set_vector_start_to_length address)) - (reset_vector_start (set_vector_start_to_length offset)) in - if bitU_to_bool (eq_range (n, (31:ii))) - then wSP ((),reset_vector_start (set_vector_start_to_length address')) - else wX (n,reset_vector_start (set_vector_start_to_length address')) - else return ()) >> - match memop with - | MemOp_STORE -> - (if bitU_to_bool rt_unknown - then - let data = set_vector_start_to_length (to_vec_dec (length data,UNKNOWN)) in - return data - else - rX (length data,t) >>= fun w__2 -> - return (set_vector_start_to_length w__2)) >>= fun data -> - wMem - (empty_write_buffer, - reset_vector_start address, - quot datasize (8:ii), - acctype, - reset_vector_start (set_vector_start_to_length data)) >>= fun w__3 -> - flush_write_buffer w__3 >> - return data - | MemOp_LOAD -> - rMem (empty_read_buffer,reset_vector_start address,quot datasize (8:ii),acctype) >>= fun w__4 -> - flush_read_buffer (w__4,quot datasize (8:ii)) >>= fun w__5 -> - let data = set_vector_start_to_length w__5 in - (if bitU_to_bool _signed - then - wX - (t, - reset_vector_start (set_vector_start_to_length - (set_vector_start_to_length - (SignExtend (regsize,reset_vector_start (set_vector_start_to_length data)))))) - else - wX - (t, - reset_vector_start (set_vector_start_to_length - (set_vector_start_to_length - (ZeroExtend (regsize,reset_vector_start (set_vector_start_to_length data))))))) >> - return data - | MemOp_PREFETCH -> return data - end >>= fun data -> - return () - -let execute_LoadStorePair (wback, postindex, n, t, t2, acctype, memop, _signed, datasize, offset) = - let address = to_vec_dec ((64:ii),(0:ii)) in - let data1 = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - let data2 = set_vector_start_to_length (to_vec_dec (length data1,(0:ii))) in - let dbytes = quot datasize (8:ii) in - let rt_unknown = B0 in - let wb_unknown = B0 in - (if bitU_to_bool - ((eq (memop, MemOp_LOAD)) &. - (wback &. (((eq_range (t, n)) |. (eq_range (t2, n))) &. (neq_range (n, (31:ii)))))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool - ((eq (memop, MemOp_STORE)) &. - (wback &. (((eq_range (t, n)) |. (eq_range (t2, n))) &. (neq_range (n, (31:ii)))))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool ((eq (memop, MemOp_LOAD)) &. (eq_range (t, t2))) - then UnallocatedEncoding () - else return ()) >> - (if bitU_to_bool (eq_range (n, (31:ii))) - then - CheckSPAlignment () >> - rSP (64:ii) - else rX ((64:ii),n)) >>= fun address -> - let address = - if bitU_to_bool (~postindex) - then - set_vector_start 63 - (add_VVV - (reset_vector_start (set_vector_start_to_length address)) - (reset_vector_start (set_vector_start_to_length offset))) - else address in - (if bitU_to_bool (eq (memop, MemOp_STORE)) - then wMem_Addr (reset_vector_start address,dbytes * (2:ii),acctype,B0) - else return ()) >> - (if bitU_to_bool wback - then - let address' = - if bitU_to_bool (~postindex) - then address - else - add_VVV - (reset_vector_start (set_vector_start_to_length address)) - (reset_vector_start (set_vector_start_to_length offset)) in - if bitU_to_bool (eq_range (n, (31:ii))) - then wSP ((),reset_vector_start (set_vector_start_to_length address')) - else wX (n,reset_vector_start (set_vector_start_to_length address')) - else return ()) >> - match memop with - | MemOp_STORE -> - (if bitU_to_bool (rt_unknown &. (eq_range (t, n))) - then - let data1 = set_vector_start_to_length (to_vec_dec (length data1,UNKNOWN)) in - return data1 - else - rX (length data1,t) >>= fun w__2 -> - return (set_vector_start_to_length w__2)) >>= fun data1 -> - (if bitU_to_bool (rt_unknown &. (eq_range (t2, n))) - then - let data2 = set_vector_start_to_length (to_vec_dec (length data1,UNKNOWN)) in - return data2 - else - rX (length data1,t2) >>= fun w__3 -> - return (set_vector_start_to_length w__3)) >>= fun data2 -> - wMem - (empty_write_buffer, - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) (0:ii))), - dbytes, - acctype, - reset_vector_start (set_vector_start_to_length data1)) >>= fun write_buffer -> - wMem - (write_buffer, - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) dbytes)), - dbytes, - acctype, - reset_vector_start (set_vector_start_to_length data2)) >>= fun w__4 -> - let write_buffer = w__4 in - flush_write_buffer write_buffer >> - return (data1,data2) - | MemOp_LOAD -> - rMem - (empty_read_buffer, - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) (0:ii))), - dbytes, - acctype) >>= fun read_buffer -> - rMem - (read_buffer, - reset_vector_start (set_vector_start 63 - (add_VIV (reset_vector_start (set_vector_start_to_length address)) dbytes)), - dbytes, - acctype) >>= fun w__5 -> - let read_buffer = w__5 in - flush_read_buffer (read_buffer,dbytes * (2:ii)) >>= fun w__6 -> - let read_data = set_vector_start_to_length w__6 in - let data1 = - set_vector_start_to_length - (slice (set_vector_start_to_length read_data) (datasize - (1:ii)) (0:ii)) in - let data2 = - set_vector_start_to_length - (slice (set_vector_start_to_length read_data) ((datasize * (2:ii)) - (1:ii)) datasize) in - let (data1, data2) = - if bitU_to_bool rt_unknown - then - let data1 = set_vector_start_to_length (to_vec_dec (length data1,UNKNOWN)) in - let data2 = set_vector_start_to_length (to_vec_dec (length data1,UNKNOWN)) in - (data1,data2) - else (data1,data2) in - (if bitU_to_bool _signed - then - wX - (t, - reset_vector_start (set_vector_start_to_length - (SignExtend ((64:ii),reset_vector_start (set_vector_start_to_length data1))))) >> - wX - (t2, - reset_vector_start (set_vector_start_to_length - (SignExtend ((64:ii),reset_vector_start (set_vector_start_to_length data2))))) - else - wX (t,reset_vector_start (set_vector_start_to_length data1)) >> - wX (t2,reset_vector_start (set_vector_start_to_length data2))) >> - return (data1,data2) - end >>= fun (data1, data2) -> - return () - -let execute_AddSubImmediate (d, n, datasize, sub_op, setflags, imm) = - (if bitU_to_bool (eq_range (n, (31:ii))) - then - rSP datasize >>= fun w__0 -> - return (set_vector_start_to_length w__0) - else - rX (datasize,n) >>= fun w__1 -> - return (set_vector_start_to_length w__1)) >>= fun operand1 -> - let operand2 = set_vector_start_to_length imm in - let carry_in = B0 in - let (operand2, carry_in) = - if bitU_to_bool sub_op - then - let operand2 = - set_vector_start_to_length (NOT (reset_vector_start (set_vector_start_to_length operand2))) in - let carry_in = B1 in - (operand2,carry_in) - else - let carry_in = B0 in - (operand2,carry_in) in - let (result, nzcv) = - match (AddWithCarry - (reset_vector_start (set_vector_start_to_length operand1), - reset_vector_start (set_vector_start_to_length operand2), - carry_in)) with - | (v0v', v1v') -> (v0v',v1v') - end in - (if bitU_to_bool setflags - then wPSTATE_NZCV ((),reset_vector_start nzcv) - else return ()) >> - if bitU_to_bool ((eq_range (d, (31:ii))) &. (~setflags)) - then wSP ((),reset_vector_start (set_vector_start_to_length result)) - else wX (d,reset_vector_start (set_vector_start_to_length result)) - -let execute_BitfieldMove (d, n, datasize, inzero, extend, R, S, wmask, tmask) = - (if bitU_to_bool inzero - then return (set_vector_start_to_length (Zeros datasize)) - else - rX (datasize,d) >>= fun w__0 -> - return (set_vector_start_to_length w__0)) >>= fun dst -> - rX (datasize,n) >>= fun w__1 -> - let src = set_vector_start_to_length w__1 in - let bot = - set_vector_start_to_length - (bitwise_or - (set_vector_start_to_length - (bitwise_and - (set_vector_start_to_length dst, - set_vector_start_to_length - (NOT (reset_vector_start (set_vector_start_to_length wmask))))), - set_vector_start_to_length - (bitwise_and - (set_vector_start_to_length - (ROR (reset_vector_start (set_vector_start_to_length src),R)), - set_vector_start_to_length wmask)))) in - let top = - if bitU_to_bool extend - then - set_vector_start_to_length - (Replicate - (length bot, - reset_vector_start (set_vector_start_to_length - (Vector [access (set_vector_start_to_length src) S] 0 false)))) - else set_vector_start_to_length dst in - wX - (d, - reset_vector_start (set_vector_start_to_length - (bitwise_or - (set_vector_start_to_length - (bitwise_and - (set_vector_start_to_length top, - set_vector_start_to_length - (NOT (reset_vector_start (set_vector_start_to_length tmask))))), - set_vector_start_to_length - (bitwise_and (set_vector_start_to_length bot, set_vector_start_to_length tmask)))))) - -let execute_ExtractRegister (d, n, m, datasize, lsb) = - let result = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - rX (datasize,m) >>= fun w__1 -> - let operand2 = set_vector_start_to_length w__1 in - let concat = - set_vector_start_to_length - ((set_vector_start_to_length operand1) ^^ (set_vector_start_to_length operand2)) in - let result = - set_vector_start_to_length - (slice (set_vector_start_to_length concat) ((lsb + datasize) - (1:ii)) lsb) in - wX (d,reset_vector_start (set_vector_start_to_length result)) - -let execute_LogicalImmediate (d, n, datasize, setflags, op, imm) = - let result = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - let operand2 = set_vector_start_to_length imm in - let result = - match op with - | LogicalOp_AND -> - set_vector_start_to_length - (bitwise_and (set_vector_start_to_length operand1, set_vector_start_to_length operand2)) - | LogicalOp_ORR -> - set_vector_start_to_length - (bitwise_or (set_vector_start_to_length operand1, set_vector_start_to_length operand2)) - | LogicalOp_EOR -> - set_vector_start_to_length - (bitwise_xor (set_vector_start_to_length operand1, set_vector_start_to_length operand2)) - end in - (if bitU_to_bool setflags - then - wPSTATE_NZCV - ((), - reset_vector_start (set_vector_start 3 - ((set_vector_start_to_length - (Vector [access (set_vector_start_to_length result) ((length - (reset_vector_start (set_vector_start_to_length - result))) - (1:ii))] 0 false)) ^^ - (set_vector_start_to_length - ((set_vector_start_to_length - (Vector [IsZeroBit (reset_vector_start (set_vector_start_to_length result))] 0 false)) ^^ - (set_vector_start_to_length (Vector [B0;B0] 1 false))))))) - else return ()) >> - if bitU_to_bool ((eq_range (d, (31:ii))) &. (~setflags)) - then wSP ((),reset_vector_start (set_vector_start_to_length result)) - else wX (d,reset_vector_start (set_vector_start_to_length result)) - -let execute_MoveWide (d, datasize, imm, pos, opcode) = - let result = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - (if bitU_to_bool (eq (opcode, MoveWideOp_K)) - then - rX (datasize,d) >>= fun w__0 -> - return (set_vector_start_to_length w__0) - else - let result = set_vector_start_to_length (Zeros datasize) in - return result) >>= fun result -> - let result = update result (pos + (15:ii)) pos (set_vector_start_to_length imm) in - let result = - if bitU_to_bool (eq (opcode, MoveWideOp_N)) - then set_vector_start_to_length (NOT (reset_vector_start (set_vector_start_to_length result))) - else result in - wX (d,reset_vector_start (set_vector_start_to_length result)) - -let execute_Address (d, page, imm) = - rPC () >>= fun base -> - let base = if bitU_to_bool page then update base (11:ii) (0:ii) (Zeros (12:ii)) else base in - wX - (d, - reset_vector_start (set_vector_start_to_length - (add_VVV - (reset_vector_start (set_vector_start_to_length base)) - (reset_vector_start (set_vector_start_to_length imm))))) - -let execute_AddSubExtendRegister (d, n, m, datasize, sub_op, setflags, extend_type, shift) = - (if bitU_to_bool (eq_range (n, (31:ii))) - then - rSP datasize >>= fun w__0 -> - return (set_vector_start_to_length w__0) - else - rX (datasize,n) >>= fun w__1 -> - return (set_vector_start_to_length w__1)) >>= fun operand1 -> - ExtendReg (datasize,m,extend_type,shift) >>= fun w__2 -> - let operand2 = set_vector_start_to_length w__2 in - let carry_in = B0 in - let (operand2, carry_in) = - if bitU_to_bool sub_op - then - let operand2 = - set_vector_start_to_length (NOT (reset_vector_start (set_vector_start_to_length operand2))) in - let carry_in = B1 in - (operand2,carry_in) - else - let carry_in = B0 in - (operand2,carry_in) in - let (result, nzcv) = - match (AddWithCarry - (reset_vector_start (set_vector_start_to_length operand1), - reset_vector_start (set_vector_start_to_length operand2), - carry_in)) with - | (v2v', v3v') -> (v2v',v3v') - end in - (if bitU_to_bool setflags - then wPSTATE_NZCV ((),reset_vector_start nzcv) - else return ()) >> - if bitU_to_bool ((eq_range (d, (31:ii))) &. (~setflags)) - then wSP ((),reset_vector_start (set_vector_start_to_length result)) - else wX (d,reset_vector_start (set_vector_start_to_length result)) - -let execute_AddSubShiftedRegister (d, n, m, datasize, sub_op, setflags, shift_type, shift_amount) = - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - ShiftReg (datasize,m,shift_type,shift_amount) >>= fun w__1 -> - let operand2 = set_vector_start_to_length w__1 in - let carry_in = B0 in - let (operand2, carry_in) = - if bitU_to_bool sub_op - then - let operand2 = - set_vector_start_to_length (NOT (reset_vector_start (set_vector_start_to_length operand2))) in - let carry_in = B1 in - (operand2,carry_in) - else - let carry_in = B0 in - (operand2,carry_in) in - let (result, nzcv) = - match (AddWithCarry - (reset_vector_start (set_vector_start_to_length operand1), - reset_vector_start (set_vector_start_to_length operand2), - carry_in)) with - | (v4v', v5v') -> (v4v',v5v') - end in - (if bitU_to_bool setflags - then wPSTATE_NZCV ((),reset_vector_start nzcv) - else return ()) >> - wX (d,reset_vector_start (set_vector_start_to_length result)) - -let execute_AddSubCarry (d, n, m, datasize, sub_op, setflags) = - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - rX (datasize,m) >>= fun w__1 -> - let operand2 = set_vector_start_to_length w__1 in - let operand2 = - if bitU_to_bool sub_op - then set_vector_start_to_length (NOT (reset_vector_start (set_vector_start_to_length operand2))) - else operand2 in - read_reg_bitfield NZCV "C" >>= fun w__2 -> - let (result, nzcv) = - match (AddWithCarry - (reset_vector_start (set_vector_start_to_length operand1), - reset_vector_start (set_vector_start_to_length operand2), - w__2)) with - | (v6v', v7v') -> (v6v',v7v') - end in - (if bitU_to_bool setflags - then wPSTATE_NZCV ((),reset_vector_start nzcv) - else return ()) >> - wX (d,reset_vector_start (set_vector_start_to_length result)) - -let execute_ConditionalCompareImmediate (n, datasize, sub_op, condition, flags, imm) = - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - let operand2 = set_vector_start_to_length imm in - let carry_in = B0 in - let flags' = flags in - ConditionHolds (reset_vector_start condition) >>= fun w__1 -> - let (operand2, carry_in, flags') = - if bitU_to_bool w__1 - then - let (operand2, carry_in) = - if bitU_to_bool sub_op - then - let operand2 = - set_vector_start_to_length - (NOT (reset_vector_start (set_vector_start_to_length operand2))) in - let carry_in = B1 in - (operand2,carry_in) - else (operand2,carry_in) in - let (_, nzcv) = - match (AddWithCarry - (reset_vector_start (set_vector_start_to_length operand1), - reset_vector_start (set_vector_start_to_length operand2), - carry_in)) with - | (v8v', v9v') -> (v8v',v9v') - end in - let flags' = nzcv in - (operand2,carry_in,flags') - else (operand2,carry_in,flags') in - wPSTATE_NZCV ((),reset_vector_start flags') - -let execute_ConditionalCompareRegister (n, m, datasize, sub_op, condition, flags) = - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - rX (datasize,m) >>= fun w__1 -> - let operand2 = set_vector_start_to_length w__1 in - let carry_in = B0 in - let flags' = flags in - ConditionHolds (reset_vector_start condition) >>= fun w__2 -> - let (operand2, carry_in, flags') = - if bitU_to_bool w__2 - then - let (operand2, carry_in) = - if bitU_to_bool sub_op - then - let operand2 = - set_vector_start_to_length - (NOT (reset_vector_start (set_vector_start_to_length operand2))) in - let carry_in = B1 in - (operand2,carry_in) - else (operand2,carry_in) in - let (_, nzcv) = - match (AddWithCarry - (reset_vector_start (set_vector_start_to_length operand1), - reset_vector_start (set_vector_start_to_length operand2), - carry_in)) with - | (v10v', v11v') -> (v10v',v11v') - end in - let flags' = nzcv in - (operand2,carry_in,flags') - else (operand2,carry_in,flags') in - wPSTATE_NZCV ((),reset_vector_start flags') - -let execute_ConditionalSelect (d, n, m, datasize, condition, else_inv, else_inc) = - let result = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - rX (datasize,m) >>= fun w__1 -> - let operand2 = set_vector_start_to_length w__1 in - ConditionHolds (reset_vector_start condition) >>= fun w__2 -> - let result = - if bitU_to_bool w__2 - then set_vector_start_to_length operand1 - else - let result = set_vector_start_to_length operand2 in - let result = - if bitU_to_bool else_inv - then - set_vector_start_to_length (NOT (reset_vector_start (set_vector_start_to_length result))) - else result in - if bitU_to_bool else_inc - then - set_vector_start_to_length - (add_VIV (reset_vector_start (set_vector_start_to_length result)) (1:ii)) - else result in - wX (d,reset_vector_start (set_vector_start_to_length result)) - -let execute_Reverse (d, n, datasize, op) = - let result = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - let V = to_vec_dec ((6:ii),(0:ii)) in - let V = - match op with - | RevOp_REV16 -> Vector [B0;B0;B1;B0;B0;B0] 5 false - | RevOp_REV32 -> Vector [B0;B1;B1;B0;B0;B0] 5 false - | RevOp_REV64 -> Vector [B1;B1;B1;B0;B0;B0] 5 false - | RevOp_RBIT -> - if bitU_to_bool (eq_range (datasize, (64:ii))) - then Vector [B1;B1;B1;B1;B1;B1] 5 false - else Vector [B0;B1;B1;B1;B1;B1] 5 false - end in - rX (datasize,n) >>= fun w__0 -> - let result = set_vector_start_to_length w__0 in - let result = - (foreach_inc ((0:ii),(5:ii),(1:ii)) result - (fun vbit result -> - if bitU_to_bool (eq (match (access V vbit) with | B0 -> (0:ii) | B1 -> (1:ii) end, (1:ii))) - then - let tmp = set_vector_start_to_length result in - let vsize = lsl' ((1:ii),vbit) in - (foreach_inc ((0:ii),datasize - (1:ii),(2:ii) * vsize) result - (fun base result -> - let result = - update - result ((base + vsize) - (1:ii)) base - (set_vector_start_to_length - (slice (set_vector_start_to_length tmp) - ((base + ((2:ii) * vsize)) - (1:ii)) (base + vsize))) in - update - result ((base + ((2:ii) * vsize)) - (1:ii)) (base + vsize) - (set_vector_start_to_length - (slice (set_vector_start_to_length tmp) ((base + vsize) - (1:ii)) base)))) - else result)) in - wX (d,reset_vector_start (set_vector_start_to_length result)) - -let execute_CountLeading (d, n, datasize, opcode) = - let result = (0:ii) in - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - let result = - if bitU_to_bool (eq (opcode, CountOp_CLZ)) - then CountLeadingZeroBits (reset_vector_start (set_vector_start_to_length operand1)) - else CountLeadingSignBits (reset_vector_start (set_vector_start_to_length operand1)) in - wX (d,reset_vector_start (set_vector_start_to_length (to_vec_dec (datasize,result)))) - -let execute_Division (d, n, m, datasize, _unsigned) = - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - rX (datasize,m) >>= fun w__1 -> - let operand2 = set_vector_start_to_length w__1 in - let result = (0:ii) in - let result = - if bitU_to_bool (IsZero (reset_vector_start (set_vector_start_to_length operand2))) - then (0:ii) - else - quot - (Int (reset_vector_start (set_vector_start_to_length operand1),_unsigned)) - (Int (reset_vector_start (set_vector_start_to_length operand2),_unsigned)) in - wX (d,reset_vector_start (set_vector_start_to_length (to_vec_dec (datasize,result)))) - -let execute_Shift (d, n, m, datasize, shift_type) = - let result = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - rX (datasize,m) >>= fun w__0 -> - let operand2 = set_vector_start_to_length w__0 in - ShiftReg - (datasize, - n, - shift_type, - modulo (UInt (reset_vector_start (set_vector_start_to_length operand2))) datasize) >>= fun w__1 -> - let result = set_vector_start_to_length w__1 in - wX (d,reset_vector_start (set_vector_start_to_length result)) - -let execute_CRC (d, n, m, size, crc32c) = - (if bitU_to_bool (~(HaveCRCExt ())) - then UnallocatedEncoding () - else return ()) >> - rX ((32:ii),n) >>= fun acc -> - rX (size,m) >>= fun w__0 -> - let _val = set_vector_start_to_length w__0 in - let poly = - if bitU_to_bool crc32c - then - Vector [B0;B0;B0;B1;B1;B1;B1;B0;B1;B1;B0;B1;B1;B1;B0;B0;B0;B1;B1;B0;B1; - B1;B1;B1;B0;B1;B0;B0;B0;B0;B0;B1] 31 false - else - Vector [B0;B0;B0;B0;B0;B1;B0;B0;B1;B1;B0;B0;B0;B0;B0;B1;B0;B0;B0;B1;B1; - B1;B0;B1;B1;B0;B1;B1;B0;B1;B1;B1] 31 false in - let tempacc = - set_vector_start_to_length - ((set_vector_start_to_length - (BitReverse (reset_vector_start (set_vector_start_to_length acc)))) ^^ - (set_vector_start_to_length (set_vector_start_to_length (Zeros (length _val))))) in - let tempval = - set_vector_start_to_length - ((set_vector_start_to_length - (BitReverse (reset_vector_start (set_vector_start_to_length _val)))) ^^ - (Zeros (32:ii))) in - wX - (d, - reset_vector_start (set_vector_start_to_length - (BitReverse - (reset_vector_start (set_vector_start_to_length - (Poly32Mod2 - (reset_vector_start (set_vector_start_to_length - (bitwise_xor - (set_vector_start_to_length tempacc, - set_vector_start_to_length tempval))), - reset_vector_start poly))))))) - -let execute_MultiplyAddSub (d, n, m, a, destsize, datasize, sub_op) = - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - rX (datasize,m) >>= fun w__1 -> - let operand2 = set_vector_start_to_length w__1 in - rX (destsize,a) >>= fun w__2 -> - let operand3 = set_vector_start_to_length w__2 in - let result = (0:ii) in - let result = - if bitU_to_bool sub_op - then - (UInt (reset_vector_start (set_vector_start_to_length operand3))) - - ((UInt (reset_vector_start (set_vector_start_to_length operand1))) * - (UInt (reset_vector_start (set_vector_start_to_length operand2)))) - else - (UInt (reset_vector_start (set_vector_start_to_length operand3))) + - ((UInt (reset_vector_start (set_vector_start_to_length operand1))) * - (UInt (reset_vector_start (set_vector_start_to_length operand2)))) in - wX (d,reset_vector_start (set_vector_start_to_length (to_vec_dec (destsize,result)))) - -let execute_MultiplyAddSubLong (d, n, m, a, destsize, datasize, sub_op, _unsigned) = - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - rX (datasize,m) >>= fun w__1 -> - let operand2 = set_vector_start_to_length w__1 in - rX (destsize,a) >>= fun w__2 -> - let operand3 = set_vector_start_to_length w__2 in - let result = (0:ii) in - let result = - if bitU_to_bool sub_op - then - (Int (reset_vector_start (set_vector_start_to_length operand3),_unsigned)) - - ((Int (reset_vector_start (set_vector_start_to_length operand1),_unsigned)) * - (Int (reset_vector_start (set_vector_start_to_length operand2),_unsigned))) - else - (Int (reset_vector_start (set_vector_start_to_length operand3),_unsigned)) + - ((Int (reset_vector_start (set_vector_start_to_length operand1),_unsigned)) * - (Int (reset_vector_start (set_vector_start_to_length operand2),_unsigned))) in - wX (d,reset_vector_start (set_vector_start_to_length (to_vec_dec ((64:ii),result)))) - -let execute_MultiplyHigh (d, n, m, a, destsize, datasize, _unsigned) = - rX (destsize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - rX (destsize,m) >>= fun w__1 -> - let operand2 = set_vector_start_to_length w__1 in - let result = (0:ii) in - let result = - (Int (reset_vector_start (set_vector_start_to_length operand1),_unsigned)) * - (Int (reset_vector_start (set_vector_start_to_length operand2),_unsigned)) in - wX - (d, - reset_vector_start (set_vector_start_to_length - (slice (to_vec_dec ((128:ii),result)) (127:ii) (64:ii)))) - -let execute_LogicalShiftedRegister (d, n, m, datasize, setflags, op, shift_type, shift_amount, invert) = - rX (datasize,n) >>= fun w__0 -> - let operand1 = set_vector_start_to_length w__0 in - ShiftReg (datasize,m,shift_type,shift_amount) >>= fun w__1 -> - let operand2 = set_vector_start_to_length w__1 in - let operand2 = - if bitU_to_bool invert - then set_vector_start_to_length (NOT (reset_vector_start (set_vector_start_to_length operand2))) - else operand2 in - let result = set_vector_start_to_length (to_vec_dec (datasize,(0:ii))) in - let result = - match op with - | LogicalOp_AND -> - set_vector_start_to_length - (bitwise_and (set_vector_start_to_length operand1, set_vector_start_to_length operand2)) - | LogicalOp_ORR -> - set_vector_start_to_length - (bitwise_or (set_vector_start_to_length operand1, set_vector_start_to_length operand2)) - | LogicalOp_EOR -> - set_vector_start_to_length - (bitwise_xor (set_vector_start_to_length operand1, set_vector_start_to_length operand2)) - end in - (if bitU_to_bool setflags - then - wPSTATE_NZCV - ((), - reset_vector_start (set_vector_start 3 - ((set_vector_start_to_length - (Vector [access (set_vector_start_to_length result) (datasize - (1:ii))] 0 false)) ^^ - (set_vector_start_to_length - ((set_vector_start_to_length - (Vector [IsZeroBit (reset_vector_start (set_vector_start_to_length result))] 0 false)) ^^ - (set_vector_start_to_length (Vector [B0;B0] 1 false))))))) - else return ()) >> - wX (d,reset_vector_start (set_vector_start_to_length result)) - -let execute = function - - | TMStart (t) -> execute_TMStart (t) - | TMCommit -> execute_TMCommit () - | TMTest -> execute_TMTest () - | TMAbort (retry,reason) -> execute_TMAbort (retry,reason) - | CompareAndBranch (t,datasize,iszero,offset) -> execute_CompareAndBranch (t,datasize,iszero,offset) - | BranchConditional (offset,condition) -> execute_BranchConditional (offset,condition) - | GenerateExceptionEL1 (imm) -> execute_GenerateExceptionEL1 (imm) - | GenerateExceptionEL2 (imm) -> execute_GenerateExceptionEL2 (imm) - | GenerateExceptionEL3 (imm) -> execute_GenerateExceptionEL3 (imm) - | DebugBreakpoint (comment) -> execute_DebugBreakpoint (comment) - | ExternalDebugBreakpoint -> execute_ExternalDebugBreakpoint () - | DebugSwitchToExceptionLevel (target_level) -> execute_DebugSwitchToExceptionLevel (target_level) - | MoveSystemImmediate (operand,field') -> execute_MoveSystemImmediate (operand,field') - | Hint (op) -> execute_Hint (op) - | ClearExclusiveMonitor (imm) -> execute_ClearExclusiveMonitor (imm) - | Barrier (op,domain,types) -> execute_Barrier (op,domain,types) - | System (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result) -> execute_System (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,has_result) - | MoveSystemRegister (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read) -> execute_MoveSystemRegister (t,sys_op0,sys_op1,sys_op2,sys_crn,sys_crm,read) - | ImplementationDefinedTestBeginEnd (isEnd) -> execute_ImplementationDefinedTestBeginEnd (isEnd) - | ImplementationDefinedStopFetching -> execute_ImplementationDefinedStopFetching () - | ImplementationDefinedThreadStart -> execute_ImplementationDefinedThreadStart () - | TestBitAndBranch (t,datasize,bit_pos,bit_val,offset) -> execute_TestBitAndBranch (t,datasize,bit_pos,bit_val,offset) - | BranchImmediate (branch_type,offset) -> execute_BranchImmediate (branch_type,offset) - | BranchRegister (n,branch_type) -> execute_BranchRegister (n,branch_type) - | ExceptionReturn -> execute_ExceptionReturn () - | DebugRestorePState -> execute_DebugRestorePState () - | LoadLiteral (t,memop,_signed,size,offset,datasize) -> execute_LoadLiteral (t,memop,_signed,size,offset,datasize) - | LoadStoreAcqExc (n,t,t2,s,acctype,excl,pair,memop,elsize,regsize,datasize) -> execute_LoadStoreAcqExc (n,t,t2,s,acctype,excl,pair,memop,elsize,regsize,datasize) - | LoadStorePairNonTemp (wback,postindex,n,t,t2,acctype,memop,scale,datasize,offset) -> execute_LoadStorePairNonTemp (wback,postindex,n,t,t2,acctype,memop,scale,datasize,offset) - | LoadImmediate (n,t,acctype,memop,_signed,wback,postindex,offset,regsize,datasize) -> execute_LoadImmediate (n,t,acctype,memop,_signed,wback,postindex,offset,regsize,datasize) - | LoadRegister (n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize,datasize) -> execute_LoadRegister (n,t,m,acctype,memop,_signed,wback,postindex,extend_type,shift,regsize,datasize) - | LoadStorePair (wback,postindex,n,t,t2,acctype,memop,_signed,datasize,offset) -> execute_LoadStorePair (wback,postindex,n,t,t2,acctype,memop,_signed,datasize,offset) - | AddSubImmediate (d,n,datasize,sub_op,setflags,imm) -> execute_AddSubImmediate (d,n,datasize,sub_op,setflags,imm) - | BitfieldMove (d,n,datasize,inzero,extend,R,S,wmask,tmask) -> execute_BitfieldMove (d,n,datasize,inzero,extend,R,S,wmask,tmask) - | ExtractRegister (d,n,m,datasize,lsb) -> execute_ExtractRegister (d,n,m,datasize,lsb) - | LogicalImmediate (d,n,datasize,setflags,op,imm) -> execute_LogicalImmediate (d,n,datasize,setflags,op,imm) - | MoveWide (d,datasize,imm,pos,opcode) -> execute_MoveWide (d,datasize,imm,pos,opcode) - | Address (d,page,imm) -> execute_Address (d,page,imm) - | AddSubExtendRegister (d,n,m,datasize,sub_op,setflags,extend_type,shift) -> execute_AddSubExtendRegister (d,n,m,datasize,sub_op,setflags,extend_type,shift) - | AddSubShiftedRegister (d,n,m,datasize,sub_op,setflags,shift_type,shift_amount) -> execute_AddSubShiftedRegister (d,n,m,datasize,sub_op,setflags,shift_type,shift_amount) - | AddSubCarry (d,n,m,datasize,sub_op,setflags) -> execute_AddSubCarry (d,n,m,datasize,sub_op,setflags) - | ConditionalCompareImmediate (n,datasize,sub_op,condition,flags,imm) -> execute_ConditionalCompareImmediate (n,datasize,sub_op,condition,flags,imm) - | ConditionalCompareRegister (n,m,datasize,sub_op,condition,flags) -> execute_ConditionalCompareRegister (n,m,datasize,sub_op,condition,flags) - | ConditionalSelect (d,n,m,datasize,condition,else_inv,else_inc) -> execute_ConditionalSelect (d,n,m,datasize,condition,else_inv,else_inc) - | Reverse (d,n,datasize,op) -> execute_Reverse (d,n,datasize,op) - | CountLeading (d,n,datasize,opcode) -> execute_CountLeading (d,n,datasize,opcode) - | Division (d,n,m,datasize,_unsigned) -> execute_Division (d,n,m,datasize,_unsigned) - | Shift (d,n,m,datasize,shift_type) -> execute_Shift (d,n,m,datasize,shift_type) - | CRC (d,n,m,size,crc32c) -> execute_CRC (d,n,m,size,crc32c) - | MultiplyAddSub (d,n,m,a,destsize,datasize,sub_op) -> execute_MultiplyAddSub (d,n,m,a,destsize,datasize,sub_op) - | MultiplyAddSubLong (d,n,m,a,destsize,datasize,sub_op,_unsigned) -> execute_MultiplyAddSubLong (d,n,m,a,destsize,datasize,sub_op,_unsigned) - | MultiplyHigh (d,n,m,a,destsize,datasize,_unsigned) -> execute_MultiplyHigh (d,n,m,a,destsize,datasize,_unsigned) - | LogicalShiftedRegister (d,n,m,datasize,setflags,op,shift_type,shift_amount,invert) -> execute_LogicalShiftedRegister (d,n,m,datasize,setflags,op,shift_type,shift_amount,invert) - end - |