Skip to content

Commit

Permalink
x64: update ainvs for asid_map removal
Browse files Browse the repository at this point in the history
  • Loading branch information
lsf37 committed Jan 11, 2018
1 parent 1fbcf1d commit 3bc1cb7
Show file tree
Hide file tree
Showing 8 changed files with 59 additions and 565 deletions.
125 changes: 7 additions & 118 deletions proof/invariant-abstract/X64/ArchAcc_AI.thy
Original file line number Diff line number Diff line change
Expand Up @@ -31,9 +31,6 @@ bundle unfold_objects_asm =
kernel_object.split_asm[split]
arch_kernel_obj.split_asm[split]

definition
"valid_asid asid s \<equiv> x64_asid_map (arch_state s) asid \<noteq> None"

definition
"update_object ptr obj = do
kobj <- get_object ptr;
Expand Down Expand Up @@ -1549,52 +1546,6 @@ lemma image_in_rtrancl_image:

definition "set_diff A B \<equiv> A - B \<union> (B - A)"

lemma set_pt_asid_map [wp]:
"\<lbrace>valid_asid_map and
(\<lambda>s. (\<forall>a aobj ptr. aa_type nobj = AASIDPool \<and> ((a, ptr) \<in> graph_of (x64_asid_map (arch_state s)) \<and> ko_at (ArchObj aobj) p s)
\<longrightarrow> ([VSRef (ucast (asid_high_bits_of a)) None], p) \<in> vs_asid_refs (x64_asid_table (arch_state s))
\<longrightarrow> (VSRef (a && mask asid_low_bits) (Some AASIDPool), ptr) \<notin> set_diff (vs_refs (ArchObj nobj)) (vs_refs (ArchObj aobj))))
\<rbrace> update_object p (ArchObj nobj) \<lbrace>\<lambda>_. valid_asid_map\<rbrace>"
apply (simp add: valid_asid_map_def vspace_at_asid_def update_object_def set_object_def)
apply (wp get_object_wp)
apply clarsimp
apply (drule(1) bspec)
apply clarsimp
apply (rule decrease_predictI)
apply force
apply (simp add: vs_lookup_def)
apply (rule image_in_rtrancl_image)
apply (clarsimp simp: vs_lookup_def)
apply (erule vs_lookup1_wellformed.lookupE)
apply (clarsimp simp: vs_lookup1_def vs_asid_refs_def)
apply (clarsimp simp: Image_def vs_asid_refs_def dest!: vs_lookup1D)
apply (rule bexI[rotated])
apply simp
apply clarsimp
apply (case_tac "pa \<noteq> p")
apply (rule vs_lookup1I[rotated -1])
apply simp
apply (simp add: obj_at_def)
apply (clarsimp simp: lookup_leaf_def obj_at_def
dest!: vs_lookup1_wellformed.lookup_rtrancl_stepD vs_lookup1D)
apply (clarsimp simp: lookup_leaf_def obj_at_def
dest!: vs_lookup1_wellformed.lookup_rtrancl_stepD vs_lookup1D)
apply (clarsimp simp: vs_lookup1_def)
apply (drule_tac x = a in spec)
apply (clarsimp simp: obj_at_def dest!:a_type_is_aobj)
apply (rule ccontr)
apply (elim allE)
apply (erule impE)
apply (rule context_conjI)
apply (rule ccontr)
apply (case_tac nobj)
apply ((fastforce simp: aa_type_simps a_type_def vs_refs_def image_def
split: kernel_object.split_asm if_split_asm arch_kernel_obj.split_asm)+)[6]
apply fastforce
apply (clarsimp simp: image_def graph_of_def)
apply (fastforce simp: set_diff_def image_def)
done

declare graph_of_None_update[simp]
declare graph_of_Some_update[simp]

Expand Down Expand Up @@ -1887,9 +1838,6 @@ lemma update_object_state_hyp_refs[wp]:
lemma update_object_invs[wp]:
"\<lbrace> \<lambda>s. invs s \<and> valid_table_caps_aobj (caps_of_state s) (arch_state s) (ArchObj obj) ptr
\<and> (aa_type obj \<noteq> AASIDPool \<longrightarrow> ptr \<notin> global_refs s)
\<and> (\<forall>a aobj p. (aa_type obj = AASIDPool \<and> ((a, p) \<in> graph_of (x64_asid_map (arch_state s)) \<and> ko_at (ArchObj aobj) ptr s))
\<longrightarrow> ([VSRef (ucast (asid_high_bits_of a)) None], ptr) \<in> vs_asid_refs (x64_asid_table (arch_state s))
\<longrightarrow> (VSRef (a && mask asid_low_bits) (Some AASIDPool), p) \<notin> set_diff (vs_refs (ArchObj obj)) (vs_refs (ArchObj aobj)))
\<and> obj_at (\<lambda>ko. case obj of PageMapL4 pm \<Rightarrow> \<exists>pm'. ko = ArchObj (PageMapL4 pm') \<and> (\<forall>x\<in>kernel_mapping_slots. pm x = pm' x) | _ \<Rightarrow> True) ptr s
\<and> valid_kernel_mappings_if_pm (set (second_level_tables (arch_state s))) (ArchObj obj)
\<and> valid_global_objs_upd ptr obj (arch_state s)
Expand Down Expand Up @@ -1921,8 +1869,8 @@ lemma update_object_invs[wp]:
(\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some rs))\<rbrace>
update_object ptr (ArchObj obj)
\<lbrace> \<lambda>_. invs \<rbrace>"
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def)
apply_trace (wp valid_irq_node_typ valid_irq_handlers_lift update_aobj_valid_global_vspace_mappings)
apply (clarsimp simp: invs_def valid_state_def valid_pspace_def valid_asid_map_def)
apply (wp valid_irq_node_typ valid_irq_handlers_lift update_aobj_valid_global_vspace_mappings)
apply (clarsimp simp: valid_arch_state_def)
done

Expand Down Expand Up @@ -2179,17 +2127,6 @@ lemma vs_lookup_pages_arch_update:
apply simp
done


lemma vs_lookup_asid_map [iff]:
"vs_lookup (s\<lparr>arch_state := x64_asid_map_update f (arch_state s)\<rparr>) = vs_lookup s"
by (simp add: vs_lookup_arch_update)


lemma vs_lookup_pages_asid_map[iff]:
"vs_lookup_pages (s\<lparr>arch_state := x64_asid_map_update f (arch_state s)\<rparr>) =
vs_lookup_pages s"
by (simp add: vs_lookup_pages_arch_update)

lemma valid_vspace_objs_arch_update:
"x64_asid_table (f (arch_state s)) = x64_asid_table (arch_state s) \<Longrightarrow>
valid_vspace_objs (arch_state_update f s) = valid_vspace_objs s"
Expand Down Expand Up @@ -2828,48 +2765,6 @@ crunch v_ker_map[wp]: set_asid_pool "valid_kernel_mappings"
(ignore: set_object wp: set_object_v_ker_map crunch_wps)


lemma set_asid_pool_restrict_asid_map:
"\<lbrace>valid_asid_map and ko_at (ArchObj (ASIDPool ap)) p and
(\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> ucast asid \<notin> S \<longrightarrow>
x64_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow>
x64_asid_map (arch_state s) asid = None)\<rbrace>
set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_asid_map\<rbrace>"
apply (simp add: set_asid_pool_def valid_asid_map_def set_object_def update_object_def)
apply (wp get_object_wp)
apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits
simp del: fun_upd_apply)
apply (drule(1) bspec)
apply (clarsimp simp: vspace_at_asid_def obj_at_def graph_of_def)
apply (drule subsetD, erule domI)
apply simp
apply (drule spec, drule(1) mp)
apply simp
apply (erule vs_lookupE)
apply (rule vs_lookupI, simp)
apply (clarsimp simp: vs_asid_refs_def graph_of_def)
apply (drule rtranclD)
apply (erule disjE, clarsimp)
apply clarsimp
apply (drule tranclD)
apply clarsimp
apply (rule r_into_rtrancl)
apply (drule vs_lookup1D)
apply clarsimp
apply (subst vs_lookup1_def)
apply (clarsimp simp: obj_at_def)
apply (erule rtranclE)
apply (clarsimp simp: vs_refs_def graph_of_def)
apply (rule image_eqI[where x="(_, _)"])
apply (simp add: split_def)
apply (clarsimp simp: restrict_map_def)
apply (drule ucast_up_inj, simp)
apply (simp add: mask_asid_low_bits_ucast_ucast)
apply clarsimp
apply (drule vs_lookup1_trans_is_append)
apply clarsimp
apply (drule vs_lookup1D)
by clarsimp

lemma set_asid_pool_cur [wp]:
"\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> set_asid_pool p a \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>"
unfolding set_asid_pool_def by (wpsimp wp: get_object_wp)
Expand Down Expand Up @@ -3006,24 +2901,18 @@ lemma set_asid_pool_zombies_state_hyp_refs [wp]:
by (simp add: update_object_state_hyp_refs)

lemma set_asid_pool_invs_restrict:
"\<lbrace>invs and ko_at (ArchObj (ASIDPool ap)) p and
(\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> ucast asid \<notin> S \<longrightarrow>
x64_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow>
x64_asid_map (arch_state s) asid = None)\<rbrace>
"\<lbrace>invs and ko_at (ArchObj (ASIDPool ap)) p \<rbrace>
set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def
apply (simp add: invs_def valid_state_def valid_pspace_def valid_asid_map_def
valid_arch_caps_def del: set_asid_pool_simpler_def)
apply (wp valid_irq_node_typ set_asid_pool_typ_at
apply (wp valid_irq_node_typ
set_asid_pool_vspace_objs_unmap valid_irq_handlers_lift
set_asid_pool_vs_lookup_unmap set_asid_pool_restrict_asid_map
set_asid_pool_vs_lookup_unmap
| simp del: set_asid_pool_simpler_def)+
done

lemma set_asid_pool_invs_unmap:
"\<lbrace>invs and ko_at (ArchObj (ASIDPool ap)) p and
(\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> ucast asid = x \<longrightarrow>
x64_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow>
x64_asid_map (arch_state s) asid = None)\<rbrace>
"\<lbrace>invs and ko_at (ArchObj (ASIDPool ap)) p\<rbrace>
set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. invs\<rbrace>"
using set_asid_pool_invs_restrict[where S="- {x}"]
by (simp add: restrict_map_def fun_upd_def if_flip)
Expand Down
19 changes: 1 addition & 18 deletions proof/invariant-abstract/X64/ArchArch_AI.thy
Original file line number Diff line number Diff line change
Expand Up @@ -382,24 +382,7 @@ lemma valid_arch_caps:

lemma valid_asid_map':
"valid_asid_map s \<Longrightarrow> valid_asid_map s'"
using empty
apply (clarsimp simp: valid_asid_map_def s'_def)
apply (drule bspec, blast)
apply (clarsimp simp: vspace_at_asid_def)
apply (drule vs_lookup_2ConsD)
apply clarsimp
apply (erule vs_lookup_atE)
apply (drule vs_lookup1D)
apply clarsimp
apply (rule vs_lookupI[rotated])
apply (rule r_into_rtrancl)
apply (rule vs_lookup1I)
apply (fastforce simp: obj_at_def)
apply assumption
apply simp
apply (clarsimp simp: vs_asid_refs_def graph_of_def)
apply fastforce
done
by (clarsimp simp: valid_asid_map_def)

end

Expand Down
11 changes: 1 addition & 10 deletions proof/invariant-abstract/X64/ArchDetype_AI.thy
Original file line number Diff line number Diff line change
Expand Up @@ -397,16 +397,7 @@ lemma valid_kernel_mappings_detype[detype_invs_proofs]:
qed

lemma valid_asid_map_detype[detype_invs_proofs]: "valid_asid_map (detype (untyped_range cap) s)"
proof -
have "valid_asid_map s"
using invs by (simp add: invs_def valid_state_def)
thus ?thesis
apply (clarsimp simp: valid_asid_map_def arch_state_det)
apply (drule bspec)
apply (blast)
apply (clarsimp simp: vspace_at_asid_def vs_lookup)
done
qed
by (simp add: valid_asid_map_def)

lemma equal_kernel_mappings_detype[detype_invs_proofs]:
"equal_kernel_mappings (detype (untyped_range cap) s)"
Expand Down
102 changes: 19 additions & 83 deletions proof/invariant-abstract/X64/ArchFinalise_AI.thy
Original file line number Diff line number Diff line change
Expand Up @@ -75,62 +75,34 @@ lemmas nat_to_cref_unat_of_bl = nat_to_cref_unat_of_bl' [OF _ refl]

lemma invs_x64_asid_table_unmap:
"invs s \<and> is_aligned base asid_low_bits \<and> base \<le> mask asid_bits
\<and> (\<forall>x\<in>set [0.e.2 ^ asid_low_bits - 1]. x64_asid_map (arch_state s) (base + x) = None)
\<and> tab = x64_asid_table (arch_state s)
\<longrightarrow> invs (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table := tab(asid_high_bits_of base := None)\<rparr>\<rparr>)"
apply (clarsimp simp: invs_def valid_state_def valid_arch_caps_def)
apply (strengthen valid_asid_map_unmap valid_vspace_objs_unmap_strg
apply (strengthen valid_vspace_objs_unmap_strg
valid_vs_lookup_unmap_strg valid_arch_state_unmap_strg)
apply (simp add: valid_irq_node_def valid_kernel_mappings_def
valid_global_objs_arch_update)
valid_global_objs_arch_update valid_asid_map_def)
apply (simp add: valid_table_caps_def valid_machine_state_def second_level_tables_def)
done

crunch asid_map[wp]: do_machine_op "valid_asid_map"

lemma delete_asid_pool_invs[wp]:
"\<lbrace>invs and K (base \<le> mask asid_bits)\<rbrace>
delete_asid_pool base pptr
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: delete_asid_pool_def)
apply wp
apply (strengthen invs_x64_asid_table_unmap)
apply simp
apply (rule hoare_vcg_conj_lift,
(rule mapM_invalidate[where ptr=pptr, simplified])?,
((wp mapM_wp' | simp add: if_apply_def2)+)[1])+
apply wp+
apply (strengthen invs_x64_asid_table_unmap)
apply (wpsimp wp: mapM_wp', simp)
apply (wp+)[3]
apply (clarsimp simp: is_aligned_mask[symmetric])
apply (rule conjI)
apply (rule vs_lookupI)
apply (erule vs_asid_refsI)
apply simp
apply clarsimp
done

lemma invalidate_asid_entry_invalidates:
"\<lbrace>valid_asid_map and valid_arch_state and K (asid \<le> mask asid_bits) and
(\<lambda>s. x64_asid_table (arch_state s) (asid_high_bits_of asid) = Some ap)\<rbrace>
invalidate_asid_entry asid pm
\<lbrace>\<lambda>rv s. \<forall>asida. asida \<le> mask asid_bits \<longrightarrow>
ucast asida = (ucast asid :: 9 word) \<longrightarrow>
x64_asid_table (arch_state s) (asid_high_bits_of asida) =
Some ap \<longrightarrow>
x64_asid_map (arch_state s) asida = None\<rbrace>"
apply (simp add: invalidate_asid_entry_def)
apply (wp invalidate_asid_invalidates)
apply clarsimp
done

lemma delete_asid_invs[wp]:
"\<lbrace>invs and K (asid \<le> mask asid_bits)\<rbrace>
delete_asid asid pd
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: delete_asid_def cong: option.case_cong del: set_arch_obj_simps(5))
apply (wp set_asid_pool_invs_unmap | wpc)+
apply (wp invalidate_asid_entry_invalidates gets_wp hoare_vcg_const_imp_lift hoare_vcg_all_lift
hoare_vcg_imp_lift invalidate_asid_asid_map_None_inv)+
apply (clarsimp simp del: fun_upd_apply simp: invs_valid_asid_map)
apply (wpsimp wp: set_asid_pool_invs_unmap)
done

crunch vs_lookup[wp]: set_vm_root "\<lambda>s. P (vs_lookup s)"
Expand Down Expand Up @@ -1564,37 +1536,6 @@ lemma set_asid_pool_empty_table_lookup:
apply (simp add: vs_cap_ref_def)
done

lemma set_asid_pool_empty_valid_asid_map:
"\<lbrace>\<lambda>s. valid_asid_map s \<and> asid_pool_at p s
\<and> (\<forall>asid'. \<not> ([VSRef asid' None] \<rhd> p) s)
\<and> (\<forall>p'. \<not> ([VSRef (ucast (asid_high_bits_of base)) None] \<rhd> p') s)\<rbrace>
set_asid_pool p empty
\<lbrace>\<lambda>rv s. valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: set_asid_pool_def set_object_def update_object_def)
apply (wp get_object_wp)
apply (clarsimp simp: valid_asid_map_def vspace_at_asid_def
dest!: graph_ofD
split: Structures_A.kernel_object.split_asm
arch_kernel_obj.split_asm )
apply (drule bspec, erule graph_ofI)
apply (clarsimp dest!: vs_lookup_2ConsD vs_lookup1D)
apply (case_tac "p = pa")
apply simp
apply (clarsimp elim!: vs_lookup_atE)
apply (rule vs_lookupI[rotated])
apply (rule r_into_rtrancl)
apply (rule_tac p=pa in vs_lookup1I)
apply (simp add: obj_at_def)
apply assumption
apply simp
apply (rule vs_asid_refsI)
apply (clarsimp simp: a_type_simps)
apply (drule vs_asid_refsI)+
apply (drule vs_lookupI, rule rtrancl_refl)
apply simp
done

lemma set_asid_pool_invs_table:
"\<lbrace>\<lambda>s. invs s \<and> asid_pool_at p s
\<and> (\<exists>p'. caps_of_state s p' = Some (ArchObjectCap (ASIDPoolCap p base)))
Expand All @@ -1603,28 +1544,23 @@ lemma set_asid_pool_invs_table:
set_asid_pool p empty
\<lbrace>\<lambda>x s. invs (s\<lparr>arch_state := arch_state s\<lparr>x64_asid_table :=
x64_asid_table (arch_state s)(asid_high_bits_of base \<mapsto> p)\<rparr>\<rparr>)\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def del:set_asid_pool_simpler_def)
apply (rule hoare_pre)
apply (wp valid_irq_node_typ set_asid_pool_typ_at
set_asid_pool_empty_table_objs
valid_irq_handlers_lift set_asid_pool_empty_table_lookup
set_asid_pool_empty_valid_asid_map
apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def valid_asid_map_def
del: set_asid_pool_simpler_def)
apply (wp valid_irq_node_typ set_asid_pool_typ_at
set_asid_pool_empty_table_objs
valid_irq_handlers_lift set_asid_pool_empty_table_lookup
| strengthen valid_arch_state_table_strg)+
apply (clarsimp simp: conj_comms)
apply (rule context_conjI)
apply clarsimp
apply (frule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp)
apply clarsimp
apply (drule obj_ref_elemD)
apply (frule(2) unique_table_refsD,
unfold obj_refs.simps aobj_ref.simps option.simps,
assumption)
apply (clarsimp simp:vs_cap_ref_def table_cap_ref_def
split:cap.split_asm arch_cap.split_asm)
apply clarsimp
apply (drule vs_asid_refsI)
apply (drule vs_lookupI, rule rtrancl_refl)
apply simp
apply (frule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp)
apply clarsimp
apply (drule obj_ref_elemD)
apply (frule(2) unique_table_refsD,
unfold obj_refs.simps aobj_ref.simps option.simps,
assumption)
apply (clarsimp simp: vs_cap_ref_def table_cap_ref_def
split: cap.split_asm arch_cap.split_asm)
done

lemma delete_asid_pool_unmapped2:
Expand Down
5 changes: 1 addition & 4 deletions proof/invariant-abstract/X64/ArchInvariants_AI.thy
Original file line number Diff line number Diff line change
Expand Up @@ -1219,10 +1219,7 @@ where
definition
valid_asid_map :: "'z::state_ext state \<Rightarrow> bool"
where
"valid_asid_map \<equiv>
\<lambda>s. dom (x64_asid_map (arch_state s)) \<subseteq> {0 .. mask asid_bits} \<and>
(\<forall>(asid, pd) \<in> graph_of (x64_asid_map (arch_state s)).
vspace_at_asid asid pd s \<and> asid \<noteq> 0)"
"valid_asid_map \<equiv> \<lambda>s. True"


section "Lemmas"
Expand Down
Loading

0 comments on commit 3bc1cb7

Please sign in to comment.