1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7(* 8Utilities for the machine level which are not machine-dependent. 9*) 10 11chapter "Machine Accessor Functions" 12 13theory MiscMachine_A 14imports Machine_A "ExecSpec.MachineExports" 15begin 16 17context begin interpretation Arch . 18 19requalify_types 20 user_context 21 user_monad 22 register 23 data 24 obj_ref 25 asid_high_len 26 asid_high_index 27 asid_low_len 28 asid_low_index 29 asid_len 30 asid_rep_len 31 asid 32 cap_ref 33 length_type 34 vspace_ref 35 36requalify_consts 37 nat_to_cref 38 msg_info_register 39 msg_registers 40 cap_register 41 badge_register 42 frame_registers 43 gp_registers 44 exception_message 45 syscall_message 46 new_context 47 slot_bits 48 oref_to_data 49 data_to_oref 50 vref_to_data 51 data_to_vref 52 nat_to_len 53 data_to_nat 54 data_to_16 55 data_to_cptr 56 combine_ntfn_badges 57 58end 59 60(* Needs to be done here after plain type names are exported *) 61translations 62 (type) "'a user_monad" <= (type) "user_context \<Rightarrow> ('a \<times> user_context) set \<times> bool" 63 64definition 65 asid_high_bits :: nat 66where 67 "asid_high_bits \<equiv> LENGTH(asid_high_len)" 68 69definition 70 asid_low_bits :: nat 71where 72 "asid_low_bits \<equiv> LENGTH(asid_low_len)" 73 74definition 75 asid_bits :: nat 76where 77 "asid_bits \<equiv> LENGTH(asid_len)" 78 79lemmas asid_bits_defs = 80 asid_bits_def asid_high_bits_def asid_low_bits_def 81 82(* Sanity checks. *) 83lemma asid_bits_len_checks: 84 "asid_bits = asid_high_bits + asid_low_bits" 85 "asid_bits \<le> LENGTH(asid_rep_len)" 86 unfolding asid_bits_defs by auto 87 88end 89