From ead3e6fdc44a43732ae08c0f674caffabec4975b Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 15 Jul 2018 16:17:06 +0100 Subject: [PATCH] aspec: message_info_to_data is mostly arch independent Factored out msg_label_bits, which is the only architecture specific part. --- proof/drefine/Intent_DR.thy | 6 +-- proof/drefine/Syscall_DR.thy | 2 +- proof/invariant-abstract/ARM/ArchIpc_AI.thy | 6 +-- .../invariant-abstract/ARM_HYP/ArchIpc_AI.thy | 6 +-- proof/invariant-abstract/X64/ArchIpc_AI.thy | 6 +-- proof/refine/ARM/VSpace_R.thy | 7 ++-- proof/refine/ARM_HYP/VSpace_R.thy | 7 ++-- proof/refine/X64/VSpace_R.thy | 12 ++---- spec/abstract/ARM/ArchInvocation_A.thy | 20 ---------- spec/abstract/ARM/Machine_A.thy | 4 ++ spec/abstract/ARM_HYP/ArchInvocation_A.thy | 20 ---------- spec/abstract/ARM_HYP/Machine_A.thy | 4 ++ spec/abstract/Invocations_A.thy | 4 -- spec/abstract/Structures_A.thy | 39 +++++++++++-------- spec/abstract/X64/ArchInvocation_A.thy | 22 ----------- spec/abstract/X64/Machine_A.thy | 4 ++ 16 files changed, 54 insertions(+), 115 deletions(-) diff --git a/proof/drefine/Intent_DR.thy b/proof/drefine/Intent_DR.thy index adcbb0341..50a2aa3ad 100644 --- a/proof/drefine/Intent_DR.thy +++ b/proof/drefine/Intent_DR.thy @@ -1598,10 +1598,10 @@ lemma store_word_corres_helper: apply (rule_tac sz = vmpage_size and y = thread in within_page_ipc_buf) apply (simp add:ipc_frame_wp_at_def obj_at_def ipc_buffer_wp_at_def)+ apply (simp add:msg_max_length_def msg_align_bits buffer_cptr_index_def) - apply (case_tac "(get_tcb_message_info tcb)") + apply (case_tac "get_tcb_message_info tcb") apply (clarsimp simp add: get_tcb_message_info_def data_to_message_info_def) apply (erule order_less_le_trans) - apply simp + apply (simp add: mask_def) apply (rule iffD1[OF word_le_nat_alt[where b = "0x6::word32",simplified]]) apply (rule less_less_trans) apply (rule word_and_le1[where a = 3]) @@ -1734,7 +1734,7 @@ lemma dcorres_store_word_safe: apply (case_tac "get_tcb_message_info tcb") apply (clarsimp simp add: get_tcb_message_info_def data_to_message_info_def) apply (erule order_less_le_trans) - apply simp + apply (simp add: mask_def) apply (rule iffD1[OF word_le_nat_alt[where b = "0x6::word32",simplified]]) apply (rule less_less_trans) apply (rule word_and_le1[where a = 3]) diff --git a/proof/drefine/Syscall_DR.thy b/proof/drefine/Syscall_DR.thy index 61184add6..f2681fcf9 100644 --- a/proof/drefine/Syscall_DR.thy +++ b/proof/drefine/Syscall_DR.thy @@ -1053,7 +1053,7 @@ lemma reply_from_kernel_error: apply (rule exI) apply (rule conjI[rotated]) apply (simp add:obj_at_def) - apply (simp add:get_tcb_message_info_def data_to_message_info_def word_neq_0_conv) + apply (simp add:get_tcb_message_info_def data_to_message_info_def word_neq_0_conv mask_def) apply (simp add:shiftr_over_or_dist le_mask_iff word_neq_0_conv) apply (subst shiftl_shiftr_id) apply (simp add:word_bits_def mask_def le_mask_iff[symmetric])+ diff --git a/proof/invariant-abstract/ARM/ArchIpc_AI.thy b/proof/invariant-abstract/ARM/ArchIpc_AI.thy index 256dc9811..843e4dae7 100644 --- a/proof/invariant-abstract/ARM/ArchIpc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchIpc_AI.thy @@ -118,10 +118,8 @@ lemma is_derived_cap_rights [simp, Ipc_AI_assms]: lemma data_to_message_info_valid [Ipc_AI_assms]: "valid_message_info (data_to_message_info w)" - apply (simp add: valid_message_info_def data_to_message_info_def) - apply (rule conjI) - apply (simp add: word_and_le1 msg_max_length_def msg_max_extra_caps_def Let_def not_less)+ - done + by (simp add: valid_message_info_def data_to_message_info_def word_and_le1 msg_max_length_def + msg_max_extra_caps_def Let_def not_less mask_def) lemma get_extra_cptrs_length[wp, Ipc_AI_assms]: "\\s . valid_message_info mi\ diff --git a/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy index e2a7fca9c..dc5981178 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchIpc_AI.thy @@ -120,10 +120,8 @@ lemma is_derived_cap_rights [simp, Ipc_AI_assms]: lemma data_to_message_info_valid [Ipc_AI_assms]: "valid_message_info (data_to_message_info w)" - apply (simp add: valid_message_info_def data_to_message_info_def) - apply (rule conjI) - apply (simp add: word_and_le1 msg_max_length_def msg_max_extra_caps_def Let_def not_less)+ - done + by (simp add: valid_message_info_def data_to_message_info_def word_and_le1 msg_max_length_def + msg_max_extra_caps_def Let_def not_less mask_def) lemma get_extra_cptrs_length[wp, Ipc_AI_assms]: "\\s . valid_message_info mi\ diff --git a/proof/invariant-abstract/X64/ArchIpc_AI.thy b/proof/invariant-abstract/X64/ArchIpc_AI.thy index 739ca0a51..037be3a71 100644 --- a/proof/invariant-abstract/X64/ArchIpc_AI.thy +++ b/proof/invariant-abstract/X64/ArchIpc_AI.thy @@ -120,10 +120,8 @@ lemma is_derived_cap_rights [simp, Ipc_AI_assms]: lemma data_to_message_info_valid [Ipc_AI_assms]: "valid_message_info (data_to_message_info w)" - apply (simp add: valid_message_info_def data_to_message_info_def) - apply (rule conjI) - apply (simp add: word_and_le1 msg_max_length_def msg_max_extra_caps_def Let_def not_less)+ - done + by (simp add: valid_message_info_def data_to_message_info_def word_and_le1 msg_max_length_def + msg_max_extra_caps_def Let_def not_less mask_def) lemma get_extra_cptrs_length[wp, Ipc_AI_assms]: "\\s . valid_message_info mi\ diff --git a/proof/refine/ARM/VSpace_R.thy b/proof/refine/ARM/VSpace_R.thy index 6628fa254..2a65e088d 100644 --- a/proof/refine/ARM/VSpace_R.thy +++ b/proof/refine/ARM/VSpace_R.thy @@ -2106,10 +2106,9 @@ lemma message_info_to_data_eqv: lemma message_info_from_data_eqv: "message_info_map (data_to_message_info rv) = messageInfoFromWord rv" - apply (auto simp add: data_to_message_info_def messageInfoFromWord_def - msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def - shiftL_nat Let_def not_less msgMaxLength_def msgLabelBits_def) - done + by (auto simp: data_to_message_info_def messageInfoFromWord_def Let_def not_less + msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def mask_def + shiftL_nat msgMaxLength_def msgLabelBits_def) lemma set_mi_corres: "mi' = message_info_map mi \ diff --git a/proof/refine/ARM_HYP/VSpace_R.thy b/proof/refine/ARM_HYP/VSpace_R.thy index 8cc91649b..b9982fe47 100644 --- a/proof/refine/ARM_HYP/VSpace_R.thy +++ b/proof/refine/ARM_HYP/VSpace_R.thy @@ -2740,10 +2740,9 @@ lemma message_info_to_data_eqv: lemma message_info_from_data_eqv: "message_info_map (data_to_message_info rv) = messageInfoFromWord rv" - apply (auto simp add: data_to_message_info_def messageInfoFromWord_def - msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def - shiftL_nat Let_def not_less msgMaxLength_def msgLabelBits_def) - done + by (auto simp: data_to_message_info_def messageInfoFromWord_def Let_def not_less + msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def mask_def + shiftL_nat msgMaxLength_def msgLabelBits_def) lemma set_mi_corres: "mi' = message_info_map mi \ diff --git a/proof/refine/X64/VSpace_R.thy b/proof/refine/X64/VSpace_R.thy index ef793b0e6..4320ad1fa 100644 --- a/proof/refine/X64/VSpace_R.thy +++ b/proof/refine/X64/VSpace_R.thy @@ -1117,19 +1117,15 @@ lemma set_cap_valid_page_map_inv: lemma message_info_to_data_eqv: "wordFromMessageInfo (message_info_map mi) = message_info_to_data mi" apply (cases mi) - apply (simp add: wordFromMessageInfo_def - msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def - shiftL_nat) + apply (simp add: wordFromMessageInfo_def msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def shiftL_nat) done lemma message_info_from_data_eqv: "message_info_map (data_to_message_info rv) = messageInfoFromWord rv" using shiftr_mask_eq[where 'a=64 and n=12] - apply (auto simp add: data_to_message_info_def messageInfoFromWord_def - msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def - shiftL_nat Let_def not_less msgMaxLength_def msgLabelBits_def - mask_def word_size) - done + by (auto simp: data_to_message_info_def messageInfoFromWord_def Let_def not_less + msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def mask_def + shiftL_nat msgMaxLength_def msgLabelBits_def) lemma set_mi_corres: "mi' = message_info_map mi \ diff --git a/spec/abstract/ARM/ArchInvocation_A.thy b/spec/abstract/ARM/ArchInvocation_A.thy index 402f56d3d..6a7df8192 100644 --- a/spec/abstract/ARM/ArchInvocation_A.thy +++ b/spec/abstract/ARM/ArchInvocation_A.thy @@ -20,26 +20,6 @@ begin context Arch begin global_naming ARM_A -text {* Message infos are encoded to or decoded from a data word. *} -primrec - message_info_to_data :: "message_info \ data" -where - "message_info_to_data (MI len exc unw mlabel) = - (let - extra = exc << 7; - unwrapped = unw << 9; - label = mlabel << 12 - in - label || extra || unwrapped || len)" - -text {* Hard-coded to avoid recursive imports? *} -definition - data_to_message_info :: "data \ message_info" -where - "data_to_message_info w \ - MI (let v = w && ((1 << 7) - 1) in if v > 120 then 120 else v) ((w >> 7) && ((1 << 2) - 1)) - ((w >> 9) && ((1 << 3) - 1)) ((w >> 12) && ((1 << 20) - 1))" - text {* These datatypes encode the arguments to the various possible ARM-specific system calls. Selectors are defined for various fields for convenience elsewhere. *} diff --git a/spec/abstract/ARM/Machine_A.thy b/spec/abstract/ARM/Machine_A.thy index 6f682acc6..28482bdcc 100644 --- a/spec/abstract/ARM/Machine_A.thy +++ b/spec/abstract/ARM/Machine_A.thy @@ -107,6 +107,10 @@ definition slot_bits :: nat where "slot_bits \ 4" +definition + msg_label_bits :: nat where + [simp]: "msg_label_bits \ 20" + type_synonym user_context = "register \ data" definition diff --git a/spec/abstract/ARM_HYP/ArchInvocation_A.thy b/spec/abstract/ARM_HYP/ArchInvocation_A.thy index 011f0b947..4a273d4b0 100644 --- a/spec/abstract/ARM_HYP/ArchInvocation_A.thy +++ b/spec/abstract/ARM_HYP/ArchInvocation_A.thy @@ -20,26 +20,6 @@ begin context Arch begin global_naming ARM_A -text {* Message infos are encoded to or decoded from a data word. *} -primrec - message_info_to_data :: "message_info \ data" -where - "message_info_to_data (MI len exc unw mlabel) = - (let - extra = exc << 7; - unwrapped = unw << 9; - label = mlabel << 12 - in - label || extra || unwrapped || len)" - -text {* Hard-coded to avoid recursive imports? *} -definition - data_to_message_info :: "data \ message_info" -where - "data_to_message_info w \ - MI (let v = w && ((1 << 7) - 1) in if v > 120 then 120 else v) ((w >> 7) && ((1 << 2) - 1)) - ((w >> 9) && ((1 << 3) - 1)) ((w >> 12) && ((1 << 20) - 1))" - text {* These datatypes encode the arguments to the various possible ARM-specific system calls. Selectors are defined for various fields for convenience elsewhere. *} diff --git a/spec/abstract/ARM_HYP/Machine_A.thy b/spec/abstract/ARM_HYP/Machine_A.thy index d020ebe3e..12350960e 100644 --- a/spec/abstract/ARM_HYP/Machine_A.thy +++ b/spec/abstract/ARM_HYP/Machine_A.thy @@ -107,6 +107,10 @@ definition slot_bits :: nat where "slot_bits \ 4" +definition + msg_label_bits :: nat where + [simp]: "msg_label_bits \ 20" + type_synonym user_context = "register \ data" definition diff --git a/spec/abstract/Invocations_A.thy b/spec/abstract/Invocations_A.thy index 9456f01ca..6a2896cb2 100644 --- a/spec/abstract/Invocations_A.thy +++ b/spec/abstract/Invocations_A.thy @@ -25,10 +25,6 @@ requalify_types arch_irq_control_invocation arch_invocation -requalify_consts - message_info_to_data - data_to_message_info - end text {* These datatypes encode the arguments to the available system calls. *} diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy index aaf46e20e..cbd122caa 100644 --- a/spec/abstract/Structures_A.thy +++ b/spec/abstract/Structures_A.thy @@ -55,6 +55,7 @@ requalify_consts aa_type untyped_min_bits untyped_max_bits + msg_label_bits end text {* @@ -264,28 +265,32 @@ transferred. The @{text mi_label} parameter is transferred directly from sender to receiver as part of the message. *} -datatype message_info = MI length_type length_type data msg_label +datatype message_info = + MI (mi_length: length_type) + (mi_extra_caps: length_type) + (mi_caps_unwrapped: data) + (mi_label: msg_label) +text {* Message infos are encoded to or decoded from a data word. *} primrec - mi_label :: "message_info \ msg_label" + message_info_to_data :: "message_info \ data" where - "mi_label (MI len exc unw label) = label" + "message_info_to_data (MI len exc unw mlabel) = + (let + extra = exc << 7; + unwrapped = unw << 9; + label = mlabel << 12 + in + label || extra || unwrapped || len)" -primrec - mi_length :: "message_info \ length_type" +definition + data_to_message_info :: "data \ message_info" where - "mi_length (MI len exc unw label) = len" - -primrec - mi_extra_caps :: "message_info \ length_type" -where - "mi_extra_caps (MI len exc unw label) = exc" - -primrec - mi_caps_unwrapped :: "message_info \ data" -where - "mi_caps_unwrapped (MI len exc unw label) = unw" - + "data_to_message_info w \ + MI (let v = w && mask 7 in if v > 120 then 120 else v) + ((w >> 7) && mask 2) + ((w >> 9) && mask 3) + ((w >> 12) && mask msg_label_bits)" section {* Kernel Objects *} diff --git a/spec/abstract/X64/ArchInvocation_A.thy b/spec/abstract/X64/ArchInvocation_A.thy index 723cb2a1a..65c08ca82 100644 --- a/spec/abstract/X64/ArchInvocation_A.thy +++ b/spec/abstract/X64/ArchInvocation_A.thy @@ -20,28 +20,6 @@ begin context Arch begin global_naming X64_A -text {* Message infos are encoded to or decoded from a data word. *} -primrec - message_info_to_data :: "message_info \ data" -where - "message_info_to_data (MI len exc unw mlabel) = - (let - extra = exc << 7; - unwrapped = unw << 9; - label = mlabel << 12 - in - label || extra || unwrapped || len)" - -text {* Hard-coded to avoid recursive imports? *} -definition - data_to_message_info :: "data \ message_info" -where - "data_to_message_info w \ - MI (let v = w && ((1 << 7) - 1) in if v > 120 then 120 else v) - ((w >> 7) && ((1 << 2) - 1)) - ((w >> 9) && ((1 << 3) - 1)) - (w >> 12)" - text {* These datatypes encode the arguments to the various possible x64-specific system calls. Selectors are defined for various fields for convenience elsewhere. *} diff --git a/spec/abstract/X64/Machine_A.thy b/spec/abstract/X64/Machine_A.thy index f0f402072..969366dac 100644 --- a/spec/abstract/X64/Machine_A.thy +++ b/spec/abstract/X64/Machine_A.thy @@ -110,6 +110,10 @@ definition slot_bits :: nat where "slot_bits \ 5" +definition + msg_label_bits :: nat where + [simp]: "msg_label_bits \ 52" + definition new_context :: "user_context" where "new_context \ UserContext FPUNullState ((\r. 0)(CS := selCS3, SS := selDS3, FLAGS := 0x202))"