From 6a549daec0151e2f4579345e483281616300051b Mon Sep 17 00:00:00 2001 From: Matthew Brecknell Date: Tue, 14 Feb 2017 16:30:59 +1100 Subject: [PATCH] x64: fix ADT_AI Updated some definitions, deleted unused lemmas. --- proof/invariant-abstract/ADT_AI.thy | 8 +- proof/invariant-abstract/X64/ArchADT_AI.thy | 337 +++----------------- 2 files changed, 52 insertions(+), 293 deletions(-) diff --git a/proof/invariant-abstract/ADT_AI.thy b/proof/invariant-abstract/ADT_AI.thy index 22f0c586e..b96462217 100644 --- a/proof/invariant-abstract/ADT_AI.thy +++ b/proof/invariant-abstract/ADT_AI.thy @@ -57,10 +57,10 @@ text {* the user memory is a mapping from addresses to bytes. A virtual-memory view will later on be built on top of that. *} -type_synonym user_mem = "word32 \ word8 option" +type_synonym user_mem = "machine_word \ word8 option" (* This is a temperary solution to model the user device memory *) -type_synonym device_state = "word32 \ word8 option" +type_synonym device_state = "machine_word \ word8 option" text {* A user state consists of a register context and (physical) user memory. @@ -68,10 +68,10 @@ text {* type_synonym user_state = "user_context \ user_mem \ device_state" text {* Virtual-memory mapping: translates virtual to physical addresses *} -type_synonym vm_mapping = "word32 \ word32" +type_synonym vm_mapping = "machine_word \ machine_word" text {* Memory rights for each virtual adress *} -type_synonym mem_rights = "word32 \ vm_rights" +type_synonym mem_rights = "machine_word \ vm_rights" text {* A user transition is characterized by a function diff --git a/proof/invariant-abstract/X64/ArchADT_AI.thy b/proof/invariant-abstract/X64/ArchADT_AI.thy index d57aa6a04..69fd4ea9c 100644 --- a/proof/invariant-abstract/X64/ArchADT_AI.thy +++ b/proof/invariant-abstract/X64/ArchADT_AI.thy @@ -20,22 +20,22 @@ context Arch begin global_naming X64 subsection {* Constructing a virtual-memory view *} text {* - Function @{text get_pd_of_thread} takes three parameters: + Function @{text get_vspace_of_thread} takes three parameters: the kernel heap, the architecture-specific state, and a thread identifier. - It returns the identifier of the corresponding page directory. + It returns the identifier of the corresponding virtual address space. Note that this function is total. If the traversal stops before a page directory can be found (e.g. because the VTable entry is not set or a reference has been invalid), the function returns the global kernel mapping. - Looking up the page directory for a thread reference involves the following + Looking up the address space for a thread reference involves the following steps: - At first, we check that the reference actually points to a TCB object in + At first, we check that the reference actually points to a TCB object in the kernel heap. If so, we check whether the vtable entry of the TCB contains a capability - to a page directory with valid mapping data. + to an address space with valid mapping data. Note that the mapping data might become stale. Hence, we have to follow the mapping data through the ASID table. *} @@ -46,15 +46,15 @@ where "get_vspace_of_thread khp astate tcb_ref \ case khp tcb_ref of Some (TCB tcb) \ (case tcb_vtable tcb of - ArchObjectCap (PML4Cap pd_ref (Some asid)) + ArchObjectCap (PML4Cap pm_ref (Some asid)) \ (case x64_asid_table astate (asid_high_bits_of asid) of None \ x64_global_pml4 astate | Some p \ (case khp p of Some (ArchObj ako) \ if (VSRef (asid && mask asid_low_bits) - (Some AASIDPool), pd_ref) + (Some AASIDPool), pm_ref) \ vs_refs_arch ako - then pd_ref + then pm_ref else x64_global_pml4 astate | _ \ x64_global_pml4 astate)) | _ \ x64_global_pml4 astate) @@ -63,8 +63,7 @@ where lemma VSRef_AASIDPool_in_vs_refs: "(VSRef (asid && mask asid_low_bits) (Some AASIDPool), r) \ vs_refs_arch ko = - (\apool. ko = arch_kernel_obj.ASIDPool apool \ - apool (ucast (asid && mask asid_low_bits)) = Some r)" + (\apool. ko = ASIDPool apool \ apool (ucast (asid && mask asid_low_bits)) = Some r)" apply simp apply (case_tac ko, simp_all add: image_def graph_of_def) apply (rename_tac arch_kernel_obj) @@ -85,12 +84,12 @@ lemma get_vspace_of_thread_def2: "get_vspace_of_thread khp astate tcb_ref \ case khp tcb_ref of Some (TCB tcb) \ (case tcb_vtable tcb of - ArchObjectCap (PML4Cap pd_ref (Some asid)) + ArchObjectCap (PML4Cap pm_ref (Some asid)) \ if (\p apool. x64_asid_table astate (asid_high_bits_of asid) = Some p \ khp p = Some (ArchObj (ASIDPool apool)) \ - apool (ucast (asid && mask asid_low_bits)) = Some pd_ref) - then pd_ref + apool (ucast (asid && mask asid_low_bits)) = Some pm_ref) + then pm_ref else x64_global_pml4 astate | _ \ x64_global_pml4 astate) | _ \ x64_global_pml4 astate" @@ -112,8 +111,8 @@ lemma get_vspace_of_thread_vs_lookup: (case kheap s tcb_ref of Some (TCB tcb) \ (case tcb_vtable tcb of - ArchObjectCap (PML4Cap pd_ref (Some asid)) \ - if (the (vs_cap_ref (tcb_vtable tcb)) \ pd_ref) s then pd_ref + ArchObjectCap (PML4Cap pm_ref (Some asid)) \ + if (the (vs_cap_ref (tcb_vtable tcb)) \ pm_ref) s then pm_ref else x64_global_pml4 (arch_state s) | _ \ x64_global_pml4 (arch_state s)) | _ \ x64_global_pml4 (arch_state s))" @@ -155,13 +154,13 @@ end (* NOTE: This statement would clearly be nicer for a partial function but later on, we really want the function to be total. *) lemma get_vspace_of_thread_eq: - "pd_ref \ x64_global_pml4 (arch_state s) \ - get_vspace_of_thread (kheap s) (arch_state s) tcb_ref = pd_ref \ + "pm_ref \ x64_global_pml4 (arch_state s) \ + get_vspace_of_thread (kheap s) (arch_state s) tcb_ref = pm_ref \ (\tcb. kheap s tcb_ref = Some (TCB tcb) \ (\asid. tcb_vtable tcb = cap.ArchObjectCap (PML4Cap - pd_ref (Some asid)) \ - (the (vs_cap_ref_arch (the_arch_cap (tcb_vtable tcb))) \ pd_ref) s))" + pm_ref (Some asid)) \ + (the (vs_cap_ref_arch (the_arch_cap (tcb_vtable tcb))) \ pm_ref) s))" by (auto simp: get_vspace_of_thread_vs_lookup vs_cap_ref_def split: option.splits Structures_A.kernel_object.splits cap.splits arch_cap.splits) @@ -191,138 +190,44 @@ definition | _ \ None" definition - "get_pdpt_entry ahp pd_ref vptr \ - case ahp pd_ref of - Some (PDPointerTable pd) \ - Some (pd (ucast ((vptr >> pdpt_shift_bits) && mask ptTranslationBits))) + "get_pdpt_entry ahp pdpt_ref vptr \ + case ahp pdpt_ref of + Some (PDPointerTable pdpt) \ + Some (pdpt (ucast ((vptr >> pdpt_shift_bits) && mask ptTranslationBits))) | _ \ None" definition - "get_pml4_entry ahp pd_ref vptr \ - case ahp pd_ref of - Some (PageMapL4 pd) \ - Some (pd (ucast ((vptr >> pml4_shift_bits) && mask ptTranslationBits))) + "get_pml4_entry ahp pm_ref vptr \ + case ahp pm_ref of + Some (PageMapL4 pm) \ + Some (pm (ucast ((vptr >> pml4_shift_bits) && mask ptTranslationBits))) | _ \ None" text {* The following function is used to extract the architecture-specific objects from the kernel heap *} definition "get_arch_obj == - case_option None (%x. case x of ArchObj a \ Some a | _ \ None)" - -lemma get_pd_entry_None_iff_get_pde_fail: - "is_aligned pd_ref pd_bits \ - get_pd_entry (\obj. get_arch_obj (kheap s obj)) pd_ref vptr = None \ - get_pde (pd_ref + (vptr >> pd_shift_bits << 3)) s = ({}, True)" - apply (subgoal_tac "(vptr >> pd_shift_bits << 3) && ~~ mask pd_bits = 0") - apply (clarsimp simp add: get_pd_entry_def get_arch_obj_def - split: option.splits Structures_A.kernel_object.splits - arch_kernel_obj.splits) - apply (clarsimp simp add: get_pde_def get_pd_def bind_def return_def assert_def - get_object_def simpler_gets_def fail_def split_def mask_out_sub_mask - mask_eqs) - apply (subgoal_tac "pd_ref + (vptr >> pd_shift_bits << 3) - - (pd_ref + (vptr >> pd_shift_bits << 3) && mask pd_bits) = pd_ref") - apply (simp (no_asm_simp) add: fail_def return_def) - apply clarsimp - apply (simp add: mask_add_aligned pd_bits_def pageBits_def pd_shift_bits_def - ptTranslationBits_def table_size - and_not_mask shiftl_shiftr3 word_size shiftr_shiftr)+ - apply (simp add: and_not_mask) - apply (simp add: pd_bits_def table_size_def ptTranslationBits_def word_size_bits_def pd_shift_bits_def) - apply (simp add: and_not_mask) - apply (simp add: shiftl_shiftr3 word_size shiftr_shiftr) - apply (subgoal_tac "vptr >> 32 = 0", simp) - apply (cut_tac shiftr_less_t2n'[of vptr 32 0], simp) - apply (simp add: mask_eq_iff) - apply (cut_tac lt2p_lem[of 32 vptr]) - apply (cut_tac word_bits_len_of, simp+) -sorry - -lemma get_pd_entry_Some_eq_get_pde: - "is_aligned pd_ref pd_bits \ - get_pd_entry (\obj. get_arch_obj (kheap s obj)) pd_ref vptr = Some x \ - get_pde (pd_ref + (vptr >> 20 << 2)) s = ({(x,s)}, False)" -apply (subgoal_tac "(vptr >> 20 << 2) && ~~ mask pd_bits = 0") - apply (clarsimp simp add: get_pd_entry_def get_arch_obj_def - split: option.splits Structures_A.kernel_object.splits - arch_kernel_obj.splits) - apply (clarsimp simp add: get_pde_def get_pd_def bind_def return_def assert_def - get_object_def simpler_gets_def fail_def split_def mask_out_sub_mask - mask_eqs) - apply (subgoal_tac "pd_ref + (vptr >> 20 << 2) - - (pd_ref + (vptr >> 20 << 2) && mask pd_bits) = pd_ref") - apply (simp (no_asm_simp) add: fail_def return_def) - apply (clarsimp simp add: mask_add_aligned pd_bits_def pageBits_def) - apply (cut_tac shiftl_shiftr_id[of 2 "vptr >> 20"]) - apply (simp add: word_bits_def)+ - apply (cut_tac shiftr_less_t2n'[of vptr 20 30]) - apply (simp add: word_bits_def) - apply (simp add: mask_eq_iff) - apply (cut_tac lt2p_lem[of 50 vptr]) - apply (cut_tac word_bits_len_of, simp+) - apply (simp add: mask_add_aligned pd_bits_def pageBits_def) -apply (simp add: pd_bits_def pageBits_def) -apply (simp add: and_not_mask) -apply (simp add: shiftl_shiftr3 word_size shiftr_shiftr) -apply (subgoal_tac "vptr >> 32 = 0", simp) -apply (cut_tac shiftr_less_t2n'[of vptr 32 0], simp) - apply (simp add: mask_eq_iff) - apply (cut_tac lt2p_lem[of 32 vptr]) - apply (cut_tac word_bits_len_of, simp+) -sorry - -lemma get_pt_entry_None_iff_get_pte_fail: - "is_aligned pt_ref pt_bits \ - get_pt_entry (\obj. get_arch_obj (kheap s obj)) pt_ref vptr = None \ - get_pte (pt_ref + ((vptr >> 12) && 0xFF << 2)) s = ({}, True)" -apply (clarsimp simp add: get_pt_entry_def get_arch_obj_def - split: option.splits Structures_A.kernel_object.splits - arch_kernel_obj.splits) -apply (clarsimp simp add: get_pte_def get_pt_def bind_def return_def assert_def - get_object_def simpler_gets_def fail_def split_def mask_out_sub_mask mask_eqs) -apply (subgoal_tac "pt_ref + ((vptr >> 12) && 0xFF << 2) - - (pt_ref + ((vptr >> 12) && 0xFF << 2) && mask pt_bits) = - pt_ref") - apply (simp (no_asm_simp) add: fail_def return_def) - apply clarsimp -apply (simp add: mask_add_aligned pt_bits_def pageBits_def) -apply (cut_tac and_mask_shiftl_comm[of 8 2 "vptr >> 12"]) - apply (simp_all add: word_size mask_def AND_twice) -sorry - -lemma get_pt_entry_Some_eq_get_pte: - "is_aligned pt_ref pt_bits \ - get_pt_entry (\obj. get_arch_obj (kheap s obj)) pt_ref vptr = Some x \ - get_pte (pt_ref + ((vptr >> 12) && mask 8 << 2)) s = ({(x,s)}, False)" - apply (clarsimp simp add: get_pt_entry_def get_arch_obj_def - split: option.splits Structures_A.kernel_object.splits - arch_kernel_obj.splits) - apply (clarsimp simp add: get_pte_def get_pt_def bind_def return_def - assert_def get_object_def simpler_gets_def fail_def split_def - mask_out_sub_mask mask_eqs) - apply (subgoal_tac "pt_ref + ((vptr >> 12) && mask 8 << 2) - - (pt_ref + ((vptr >> 12) && mask 8 << 2) && mask pt_bits) = - pt_ref") - apply (simp (no_asm_simp) add: fail_def return_def) - apply (clarsimp simp add: mask_add_aligned pt_bits_def pageBits_def - word_size - and_mask_shiftr_comm and_mask_shiftl_comm shiftr_shiftr AND_twice) - apply (cut_tac shiftl_shiftr_id[of 2 "(vptr >> 12)"]) - apply (simp add: word_bits_def)+ - apply (cut_tac shiftr_less_t2n'[of vptr 12 30]) - apply (simp add: word_bits_def) - apply (simp add: mask_eq_iff) - apply (cut_tac lt2p_lem[of 32 vptr]) - apply (cut_tac word_bits_len_of, simp+) - apply (simp add: mask_add_aligned pt_bits_def pageBits_def - word_size and_mask_shiftl_comm AND_twice) -sorry + case_option None (\x. case x of ArchObj a \ Some a | _ \ None)" +(* Auxilliary definitions for get_page_info *) definition "get_pt_info ahp pt_ref vptr \ case get_pt_entry ahp pt_ref vptr of - Some (SmallPagePTE base attrs rights) \ Some (base, 12, attrs, rights) + Some (SmallPagePTE base attrs rights) \ Some (base, pageBitsForSize X64SmallPage, attrs, rights) + | _ \ None" + +definition + "get_pd_info ahp pd_ref vptr \ + case get_pd_entry ahp pd_ref vptr of + Some (PageTablePDE p _ _) \ get_pt_info ahp (ptrFromPAddr p) vptr + | Some (LargePagePDE base attrs rights) \ Some (base, pageBitsForSize X64LargePage, attrs, rights) + | _ \ None" + +definition + "get_pdpt_info ahp pdpt_ref vptr \ + case get_pdpt_entry ahp pdpt_ref vptr of + Some (PageDirectoryPDPTE p _ _) \ get_pd_info ahp (ptrFromPAddr p) vptr + | Some (HugePagePDPTE base attrs rights) \ Some (base, pageBitsForSize X64HugePage, attrs, rights) | _ \ None" text {* @@ -339,170 +244,24 @@ definition machine_word \ (machine_word \ nat \ frame_attrs \ vm_rights)" where get_page_info_def: - "get_page_info ahp pd_ref vptr \ - case get_pd_entry ahp pd_ref vptr of - Some (PageTablePDE p _ _) \ - get_pt_info ahp (ptrFromPAddr p) vptr - | Some (SectionPDE base attrs _ rights) \ Some (base, 20, attrs, rights) - | Some (SuperSectionPDE base attrs rights) \ Some (base,24, attrs, rights) + "get_page_info ahp pm_ref vptr \ + case get_pml4_entry ahp pm_ref vptr of + Some (PDPointerTablePML4E p _ _) \ get_pdpt_info ahp (ptrFromPAddr p) vptr | _ \ None" - -(* FIXME: Lemma can be found in Untyped_R; - proof mostly copied from ArchAcc_R.pd_shifting *) -lemma pd_shifting': - "is_aligned pd pd_bits \ - (pd + (vptr >> 20 << 2) && ~~ mask pd_bits) = (pd::word32)" - apply (simp add: pd_bits_def pageBits_def) - apply (rule word_eqI) - apply (subst word_plus_and_or_coroll) - apply (rule word_eqI) - apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth) - apply (erule_tac x=na in allE) - apply (simp add: linorder_not_less) - apply (drule test_bit_size)+ - apply (simp add: word_size) - apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth - word_ops_nth_size pd_bits_def linorder_not_less) - apply (rule iffI) - apply clarsimp - apply (drule test_bit_size)+ - apply (simp add: word_size) - apply clarsimp - apply (erule_tac x=n in allE) - apply simp - sorry - -lemma lookup_pt_slot_fail: - "is_aligned pd pd_bits \ - lookup_pt_slot pd vptr s = ({},True) \ - (\pdo. kheap s pd \ Some (ArchObj (PageDirectory pdo)))" -apply (frule pd_shifting'[of _ vptr]) -by (auto simp add: lookup_pt_slot_def lookup_pd_slot_def liftE_def bindE_def - returnOk_def lift_def bind_def split_def throwError_def return_def - get_pde_def get_pd_def Union_eq get_object_def simpler_gets_def - assert_def fail_def mask_eqs - split: sum.splits if_split_asm Structures_A.kernel_object.splits - arch_kernel_obj.splits pde.splits) - -(* FIXME: Lemma can be found in ArchAcc_R *) -lemma shiftr_shiftl_mask_pd_bits: - "(((vptr :: word32) >> 20) << 2) && mask pd_bits = (vptr >> 20) << 2" - apply (rule iffD2 [OF mask_eq_iff_w2p]) - apply (simp add: pd_bits_def pageBits_def word_size) - apply (rule shiftl_less_t2n) - apply (simp_all add: pd_bits_def word_bits_def pageBits_def word_size) - apply (cut_tac shiftr_less_t2n'[of vptr 20 12]) - apply simp - apply (simp add: mask_eq_iff) - apply (cut_tac lt2p_lem[of 32 vptr], simp) - apply (cut_tac word_bits_len_of, simp) - apply simp - done - -lemma lookup_pt_slot_no_fail: - "is_aligned pd pd_bits \ - kheap s pd = Some (ArchObj (PageDirectory pdo)) \ - lookup_pt_slot pd vptr s = - (case pdo (ucast (vptr >> 20)) of - InvalidPDE \ - ({(Inl (ExceptionTypes_A.MissingCapability 20),s)},False) - | PageTablePDE p _ _ \ - ({(Inr (ptrFromPAddr p + ((vptr >> 12) && 0xFF << 2)),s)}, - False) - | SectionPDE _ _ _ _ \ - ({(Inl (ExceptionTypes_A.MissingCapability 20),s)},False) - | SuperSectionPDE _ _ _ \ - ({(Inl (ExceptionTypes_A.MissingCapability 20),s)},False) )" -apply (frule pd_shifting'[of _ vptr]) -apply (cut_tac shiftr_shiftl_mask_pd_bits[of vptr]) -apply (subgoal_tac "vptr >> 20 << 2 >> 2 = vptr >> 20") -defer - apply (rule shiftl_shiftr_id) - apply (simp_all add: word_bits_def) - apply (cut_tac shiftr_less_t2n'[of vptr 20 30]) - apply (simp add: word_bits_def) - apply (simp add: mask_eq_iff) - apply (cut_tac lt2p_lem[of 32 vptr]) - apply (cut_tac word_bits_len_of, simp_all) -by (clarsimp simp add: lookup_pt_slot_def lookup_pd_slot_def liftE_def bindE_def - returnOk_def lift_def bind_def split_def throwError_def return_def - get_pde_def get_pd_def Union_eq get_object_def simpler_gets_def - assert_def fail_def mask_add_aligned - split: sum.splits if_split_asm kernel_object.splits arch_kernel_obj.splits - pde.splits) - -lemma get_page_info_pte: - "is_aligned pd_ref pd_bits \ - lookup_pt_slot pd_ref vptr s = ({(Inr x,s)},False) \ - is_aligned (x - ((vptr >> 12) && 0xFF << 2)) pt_bits \ - get_pte x s = ({(pte,s)},False) \ - get_page_info (\obj. get_arch_obj (kheap s obj)) pd_ref vptr = - (case pte of - SmallPagePTE base attrs rights \ Some (base, 12, attrs, rights) - | LargePagePTE base attrs rights \ Some (base, 16, attrs, rights) - | _ \ None)" -apply (clarsimp simp add: get_page_info_def get_pd_entry_def - split: option.splits) -apply (intro conjI impI allI) - apply (frule lookup_pt_slot_fail[of _ vptr s], - clarsimp simp add: get_arch_obj_def) - apply (frule lookup_pt_slot_fail[of _ vptr s], - clarsimp simp add: get_arch_obj_def) -apply (frule lookup_pt_slot_fail[of _ vptr s], - clarsimp simp add: get_arch_obj_def) -apply (frule (1) lookup_pt_slot_no_fail[where vptr=vptr]) -apply (clarsimp split: pde.splits option.splits) -apply (clarsimp simp add: get_pt_info_def split: option.splits) -apply (intro conjI impI) - apply (drule get_pt_entry_None_iff_get_pte_fail[where s=s and vptr=vptr]) - apply (simp add: pt_bits_def pageBits_def mask_def) -apply clarsimp -apply (drule_tac x=x2 in get_pt_entry_Some_eq_get_pte[where s=s and vptr=vptr]) -apply (simp add: pt_bits_def pageBits_def mask_def) -done - -lemma get_page_info_section: - "is_aligned pd_ref pd_bits \ - get_pde (lookup_pd_slot pd_ref vptr) s = - ({(SectionPDE base attrs X rights, s)},False) \ - get_page_info (\obj. get_arch_obj (kheap s obj)) pd_ref vptr = - Some (base, 20, attrs, rights)" -apply (simp add: lookup_pd_slot_def get_page_info_def split: option.splits) -apply (intro conjI impI allI) - apply (drule get_pd_entry_None_iff_get_pde_fail[where s=s and vptr=vptr]) - apply (simp split: option.splits) -apply (drule_tac x=x2 in get_pd_entry_Some_eq_get_pde[where s=s and vptr=vptr]) -apply clarsimp -done - -lemma get_page_info_super_section: - "is_aligned pd_ref pd_bits \ - get_pde (lookup_pd_slot pd_ref vptr) s = - ({(SuperSectionPDE base attrs rights,s)},False) \ - get_page_info (\obj. get_arch_obj (kheap s obj)) pd_ref vptr = - Some (base, 24, attrs, rights)" -apply (simp add: lookup_pd_slot_def get_page_info_def split: option.splits) -apply (intro conjI impI allI) - apply (drule get_pd_entry_None_iff_get_pde_fail[where s=s and vptr=vptr]) - apply (simp split: option.splits) -apply (drule_tac x=x2 in get_pd_entry_Some_eq_get_pde[where s=s and vptr=vptr]) -apply clarsimp -done - text {* Both functions, @{text ptable_lift} and @{text vm_rights}, take a kernel state and a virtual address. The former returns the physical address, the latter the associated rights. *} definition - ptable_lift :: "obj_ref \ 'z state \ word32 \ word32" where + ptable_lift :: "obj_ref \ 'z state \ machine_word \ machine_word" where "ptable_lift tcb s \ \addr. case_option None (\(base, bits, rights). Some (base + (addr && mask bits))) (get_page_info (\obj. get_arch_obj (kheap s obj)) (get_vspace_of_thread (kheap s) (arch_state s) tcb) addr)" definition - ptable_rights :: "obj_ref \ 'z state \ word32 \ vm_rights" where + ptable_rights :: "obj_ref \ 'z state \ machine_word \ vm_rights" where "ptable_rights tcb s \ \addr. case_option {} (snd o snd o snd) (get_page_info (\obj. get_arch_obj (kheap s obj))