From 3dafec7d46f8e581b93445f80b362d3cc136b05e Mon Sep 17 00:00:00 2001 From: Joel Beeren Date: Thu, 26 Jan 2017 14:20:48 +1100 Subject: [PATCH] backport changes to ARM proofs from X64 work in progress - replace ARM-specific constants and types with aliases which can be instantiated separately for each architecture. - expand lib with lemmas used in X64 proofs. - simplify some proofs. Also-by: Matthew Brecknell --- .gitignore | 63 +++--- .licenseignore | 8 +- lib/LemmaBucket.thy | 3 + lib/NonDetMonadLemmaBucket.thy | 213 ++++++++++++++++++ lib/Word_Lib/Word_Lemmas.thy | 18 ++ lib/Word_Lib/Word_Lemmas_64.thy | 17 ++ lib/X64/WordSetup.thy | 44 ++++ proof/access-control/Retype_AC.thy | 2 +- proof/access-control/Syscall_AC.thy | 12 - proof/crefine/Arch_C.thy | 2 +- proof/crefine/Detype_C.thy | 6 +- proof/drefine/KHeap_DR.thy | 10 +- proof/drefine/Tcb_DR.thy | 2 +- proof/drefine/Untyped_DR.thy | 6 +- proof/infoflow/Example_Valid_State.thy | 14 +- proof/invariant-abstract/ARM/ArchAcc_AI.thy | 95 +------- .../ARM/ArchBCorres2_AI.thy | 2 +- .../ARM/ArchCSpacePre_AI.thy | 3 +- .../invariant-abstract/ARM/ArchCSpace_AI.thy | 31 ++- .../ARM/ArchDeterministic_AI.thy | 3 +- .../invariant-abstract/ARM/ArchDetype_AI.thy | 17 +- .../ARM/ArchInterrupt_AI.thy | 8 +- .../ARM/ArchInvariants_AI.thy | 2 + proof/invariant-abstract/ARM/ArchIpc_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchKHeap_AI.thy | 6 +- .../invariant-abstract/ARM/ArchRetype_AI.thy | 103 ++------- proof/invariant-abstract/ARM/ArchTcb_AI.thy | 7 +- .../invariant-abstract/ARM/ArchUntyped_AI.thy | 14 +- .../invariant-abstract/ARM/ArchVSpace_AI.thy | 24 +- proof/invariant-abstract/BCorres_AI.thy | 2 +- proof/invariant-abstract/CSpace_AI.thy | 118 +++++----- .../DetSchedSchedule_AI.thy | 4 + proof/invariant-abstract/Deterministic_AI.thy | 2 + proof/invariant-abstract/Detype_AI.thy | 139 ++---------- proof/invariant-abstract/Finalise_AI.thy | 2 +- proof/invariant-abstract/Interrupt_AI.thy | 14 +- proof/invariant-abstract/Invariants_AI.thy | 12 +- proof/invariant-abstract/IpcCancel_AI.thy | 2 +- proof/invariant-abstract/LevityCatch_AI.thy | 61 ++++- proof/invariant-abstract/Retype_AI.thy | 167 ++------------ proof/invariant-abstract/Syscall_AI.thy | 37 ++- proof/invariant-abstract/Tcb_AI.thy | 8 +- proof/invariant-abstract/Untyped_AI.thy | 160 +++++++------ proof/refine/ADT_H.thy | 2 +- proof/refine/Detype_R.thy | 12 +- proof/refine/Include.thy | 2 +- proof/refine/Retype_R.thy | 6 +- proof/refine/Syscall_R.thy | 2 +- proof/refine/Untyped_R.thy | 15 +- spec/ROOT | 2 +- spec/abstract/ARM/ArchCSpace_A.thy | 19 ++ spec/abstract/ARM/ArchTcb_A.thy | 29 +++ spec/abstract/ARM/Arch_Structs_A.thy | 6 + spec/abstract/CSpace_A.thy | 14 +- spec/abstract/Structures_A.thy | 8 +- spec/abstract/Tcb_A.thy | 9 +- spec/design/ARM/ArchIntermediate_H.thy | 68 ++++++ spec/design/ArchInterrupt_H.thy | 31 --- spec/design/{ARM => }/Intermediate_H.thy | 84 ++----- spec/design/m-skel/ARM/MachineTypes.thy | 7 + spec/haskell/SEL4.cabal | 40 +++- spec/haskell/src/SEL4/API/Invocation.lhs | 5 +- spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs | 2 +- spec/haskell/src/SEL4/Object/Interrupt.lhs | 2 + spec/machine/ARM/MachineTypes.thy | 7 + spec/machine/MachineExports.thy | 12 + tools/c-parser/.gitignore | 13 ++ tools/c-parser/IsaMakefile | 12 +- tools/c-parser/standalone-parser/Makefile | 26 +-- tools/c-parser/testfiles/{ => ARM}/asm_stmt.c | 0 .../c-parser/testfiles/{ => ARM}/asm_stmt.thy | 2 +- .../testfiles/ARM/imports/MachineWords.thy | 24 ++ .../testfiles/X64/imports/MachineWords.thy | 24 ++ tools/c-parser/testfiles/factorial.c | 22 +- tools/c-parser/testfiles/factorial.thy | 68 +++--- tools/c-parser/testfiles/kmalloc.thy | 4 +- tools/c-parser/testfiles/list_reverse.c | 8 +- tools/c-parser/testfiles/list_reverse.thy | 4 +- tools/c-parser/testfiles/list_reverse_norm.c | 6 +- .../c-parser/testfiles/list_reverse_norm.thy | 6 +- .../umm_heap/{FAKE64 => X64}/Addr_Type.thy | 0 .../umm_heap/{FAKE64 => X64}/TargetNumbers.ML | 4 +- .../{FAKE64 => X64}/Word_Mem_Encoding.thy | 0 tools/haskell-translator/caseconvs | 57 ++++- tools/haskell-translator/make_spec.sh | 2 +- tools/tests.xml | 1 + 86 files changed, 1157 insertions(+), 975 deletions(-) create mode 100644 lib/X64/WordSetup.thy create mode 100644 spec/abstract/ARM/ArchTcb_A.thy create mode 100644 spec/design/ARM/ArchIntermediate_H.thy delete mode 100644 spec/design/ArchInterrupt_H.thy rename spec/design/{ARM => }/Intermediate_H.thy (57%) rename tools/c-parser/testfiles/{ => ARM}/asm_stmt.c (100%) rename tools/c-parser/testfiles/{ => ARM}/asm_stmt.thy (94%) create mode 100644 tools/c-parser/testfiles/ARM/imports/MachineWords.thy create mode 100644 tools/c-parser/testfiles/X64/imports/MachineWords.thy rename tools/c-parser/umm_heap/{FAKE64 => X64}/Addr_Type.thy (100%) rename tools/c-parser/umm_heap/{FAKE64 => X64}/TargetNumbers.ML (96%) rename tools/c-parser/umm_heap/{FAKE64 => X64}/Word_Mem_Encoding.thy (100%) diff --git a/.gitignore b/.gitignore index d792b1fa8..2f761c61e 100644 --- a/.gitignore +++ b/.gitignore @@ -7,45 +7,36 @@ *.lev *#*# -spec/cspec/c/32/ -spec/cspec/c/api/ -spec/cspec/c/arch/ -spec/cspec/c/kernel_all.c -spec/cspec/c/kernel_all.c_pp -spec/cspec/c/parsetab.py -spec/cspec/c/plat/ -spec/cspec/c/sources_list_updated -spec/cspec/c/autoconf.h +/spec/cspec/c/32/ +/spec/cspec/c/64/ +/spec/cspec/c/api/ +/spec/cspec/c/arch/ +/spec/cspec/c/kernel_all.c +/spec/cspec/c/kernel_all.c_pp +/spec/cspec/c/parsetab.py +/spec/cspec/c/plat/ +/spec/cspec/c/sources_list_updated +/spec/cspec/c/autoconf.h -spec/haskell/doc/**/*.aux -spec/haskell/doc/**/*.bbl -spec/haskell/doc/**/*.blg -spec/haskell/doc/**/*.log -spec/haskell/doc/**/*.mpx -spec/haskell/doc/**/*.out -spec/haskell/doc/**/*.toc +/spec/haskell/doc/**/*.aux +/spec/haskell/doc/**/*.bbl +/spec/haskell/doc/**/*.blg +/spec/haskell/doc/**/*.log +/spec/haskell/doc/**/*.mpx +/spec/haskell/doc/**/*.out +/spec/haskell/doc/**/*.toc -**/CFunDump.txt -**/umm_types.txt +CFunDump.txt +umm_types.txt -tools/autocorres/doc/quickstart/output/ -tools/autocorres/sel4.txt -tools/autocorres/tests/ROOT -tools/autocorres/tests/parse-tests/*.thy -tools/autocorres/tests/examples/trace_demo_incr.trace +/tools/autocorres/doc/quickstart/output/ +/tools/autocorres/sel4.txt +/tools/autocorres/tests/ROOT +/tools/autocorres/tests/parse-tests/*.thy +/tools/autocorres/tests/examples/trace_demo_incr.trace -tools/c-parser/standalone-parser/table.ML -tools/c-parser/StrictC.grm.desc -tools/c-parser/standalone-parser/ARM/ -tools/c-parser/standalone-parser/FAKE64/ -tools/c-parser/tools/mllex/mllex -tools/c-parser/tools/mlyacc/mlyacc -tools/c-parser/tools/mlyacc/src/yacc.lex.sml -tools/c-parser/testfiles/ROOT -tools/c-parser/testfiles/umm_types.txt +/tools/haskell-translator/caseconvs-useful -tools/haskell-translator/caseconvs-useful +/camkes/adl-spec/camkes.ML -camkes/adl-spec/camkes.ML - -internal +/internal/ diff --git a/.licenseignore b/.licenseignore index 4a7dd71c6..93c82374b 100644 --- a/.licenseignore +++ b/.licenseignore @@ -65,9 +65,12 @@ spec/haskell/src/SEL4/Object/CNode.lhs-boot spec/haskell/src/SEL4/Object/Endpoint.lhs-boot spec/haskell/src/SEL4/Object/ObjectType.lhs-boot spec/haskell/src/SEL4/Object/TCB.lhs-boot +spec/haskell/src/SEL4/Object/IOPort/X64.lhs-boot spec/design/version +spec/cspec/c/32/* +spec/cspec/c/64/* spec/cspec/c/api/* spec/cspec/c/arch/* spec/cspec/c/kernel_all.c @@ -151,9 +154,10 @@ tools/c-parser/standalone-parser/*/tokenizer tools/c-parser/tools/mllex/mllex tools/c-parser/tools/mlyacc/mlyacc tools/c-parser/tools/mlyacc/src/yacc.lex.sml -tools/c-parser/testfiles/jiraver473.minfo -tools/c-parser/testfiles/ROOT +tools/c-parser/testfiles/**/*.minfo +tools/c-parser/testfiles/**/ROOT tools/c-parser/testfiles/umm_types.txt +tools/c-parser/testfiles/modifies_speed.c tools/haskell-translator/caseconvs-useful tools/haskell-translator/primrecs diff --git a/lib/LemmaBucket.thy b/lib/LemmaBucket.thy index e2785d6c3..379e71f3a 100644 --- a/lib/LemmaBucket.thy +++ b/lib/LemmaBucket.thy @@ -440,4 +440,7 @@ lemma list_ran_prop:"map_of (map (\x. (f x, g x)) xs) i = Some t \ set (enumerate n xs) \ (b = xs ! (a - n))" by (simp add: in_set_enumerate_eq) +lemma subset_eq_notI: "\a\ B;a\ C\ \ \ B \ C" + by auto + end diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy index 08d0e9503..f93c3a4ba 100644 --- a/lib/NonDetMonadLemmaBucket.thy +++ b/lib/NonDetMonadLemmaBucket.thy @@ -2897,4 +2897,217 @@ lemma hoare_assume_preNF: "(\s. P s \ \P\ f \Q\!) \ \P\ f \Q\!" by (metis validNF_alt_def) +lemma bexEI: "\\x\S. Q x; \x. \x \ S; Q x\ \ P x\ \ \x\S. P x" by blast + +lemma monad_eq_split: + assumes "\r s. Q r s \ f r s = f' r s" + "\P\ g \\r s. Q r s\" + "P s" + shows "(g >>= f) s = (g >>= f') s" +proof - + have pre: "\rv s'. \(rv, s') \ fst (g s)\ \ f rv s' = f' rv s'" + using assms unfolding valid_def + by (erule_tac x=s in allE) auto + show ?thesis + apply (simp add: bind_def image_def) + apply (intro conjI) + apply (rule set_eqI) + apply (clarsimp simp: Union_eq) + apply (rule iffI; elim exEI conjE; simp; elim exEI bexEI; clarsimp simp: pre) + apply (rule iffI; cases "snd (g s)"; simp; elim exEI bexEI; clarsimp simp: pre) + done +qed + +lemma monad_eq_split2: +assumes eq: " g' s = g s" +assumes tail:"\r s. Q r s \ f r s = f' r s" +and hoare: "\P\g\\r s. Q r s\" "P s" +shows "(g>>=f) s = (g'>>= f') s" +proof - +have pre: "\aa bb. \(aa, bb) \ fst (g s)\ \ Q aa bb" + using hoare by (auto simp: valid_def) +show ?thesis + apply (simp add:bind_def eq split_def image_def) + apply (rule conjI) + apply (rule set_eqI) + apply (clarsimp simp:Union_eq) + apply (metis pre surjective_pairing tail) + apply (metis pre surjective_pairing tail) + done +qed + +lemma monad_eq_split_tail: + "\f = g;a s = b s\ \ (a >>= f) s = ((b >>= g) s)" + by (simp add:bind_def) + +definition monad_commute where + "monad_commute P a b \ + (\s. (P s \ ((do x\a;y\b; return (x, y) od) s) = ((do y\b;x\a; return (x, y) od) s)))" + + +lemma monad_eq: + "a s = b s \ (a >>= g) s = (b >>= g) s" + by (auto simp:bind_def) + +lemma monad_commute_simple: + "\monad_commute P a b;P s\ \ ((do x\a;y\b; g x y od) s) = ((do y\b;x\a; g x y od) s)" + apply (clarsimp simp:monad_commute_def) + apply (drule spec) + apply (erule(1) impE) + apply (drule_tac g = "(\t. g (fst t) (snd t))" in monad_eq) + apply (simp add:bind_assoc) + done + +lemma commute_commute: + "monad_commute P f h \ monad_commute P h f" + apply (simp (no_asm) add: monad_commute_def) + apply (clarsimp) + apply (erule monad_commute_simple[symmetric]) + apply simp + done + +lemma assert_commute: "monad_commute (K G) (assert G) f" + by (clarsimp simp:assert_def monad_commute_def) + +lemma cond_fail_commute: "monad_commute (K (\G)) (when G fail) f" + by (clarsimp simp:when_def fail_def monad_commute_def) + +lemma return_commute: "monad_commute \ (return a) f" + by (clarsimp simp: return_def bind_def monad_commute_def) + +lemma monad_commute_guard_imp: + "\monad_commute P f h; \s. Q s \ P s \ \ monad_commute Q f h" + by (clarsimp simp:monad_commute_def) + +lemma monad_commute_split: + "\\r. monad_commute (Q r) f (g r); monad_commute P f h; + \P'\ h \\r. Q r\\ + \ monad_commute (P and P') f (h>>=g)" + apply (simp (no_asm) add:monad_commute_def) + apply (clarsimp simp:bind_assoc) + apply (subst monad_commute_simple) + apply simp+ + apply (rule_tac Q = "(\x. Q x)" in monad_eq_split) + apply (subst monad_commute_simple[where a = f]) + apply assumption + apply simp+ + done + +lemma monad_commute_get: + assumes hf: "\P. \P\ f \\r. P\" + and hg: "\P. \P\ g \\r. P\" + and eptyf: "empty_fail f" "empty_fail g" + shows "monad_commute \ f g" +proof - + have fsame: "\a b s. (a,b) \ fst (f s) \ b = s" + by (drule use_valid[OF _ hf],auto) + have gsame: "\a b s. (a,b) \ fst (g s) \ b = s" + by (drule use_valid[OF _ hg],auto) + note ef = empty_fail_not_snd[OF _ eptyf(1)] + note eg = empty_fail_not_snd[OF _ eptyf(2)] + show ?thesis + apply (simp add:monad_commute_def) + apply (clarsimp simp:bind_def split_def return_def) + apply (intro conjI) + apply (rule set_eqI) + apply (rule iffI) + apply (clarsimp simp:Union_eq dest!: singletonD) + apply (frule fsame) + apply clarsimp + apply (frule gsame) + apply (metis fst_conv snd_conv) + apply (clarsimp simp:Union_eq dest!: singletonD) + apply (frule gsame) + apply clarsimp + apply (frule fsame) + apply clarsimp + apply (metis fst_conv snd_conv) + apply (rule iffI) + apply (erule disjE) + apply (clarsimp simp:image_def) + apply (metis fsame) + apply (clarsimp simp:image_def) + apply (drule eg) + apply clarsimp + apply (rule bexI [rotated], assumption) + apply (frule gsame) + apply clarsimp + apply (erule disjE) + apply (clarsimp simp:image_def dest!:gsame) + apply (clarsimp simp:image_def) + apply (drule ef) + apply clarsimp + apply (frule fsame) + apply (erule bexI[rotated]) + apply simp + done +qed + +lemma mapM_x_commute: +assumes commute: + "\r. monad_commute (P r) a (b r)" +and single: + "\r x. \P r and K (f r \ f x) and P x\ b x \\v. P r \" +shows + "monad_commute (\s. (distinct (map f list)) \ (\r\ set list. P r s)) a (mapM_x b list)" + apply (induct list) + apply (clarsimp simp:mapM_x_Nil return_def bind_def monad_commute_def) + apply (clarsimp simp:mapM_x_Cons) + apply (rule monad_commute_guard_imp) + apply (rule monad_commute_split) + apply assumption + apply (rule monad_commute_guard_imp[OF commute]) + apply assumption + apply (wp hoare_vcg_ball_lift) + apply (rule single) + apply (clarsimp simp: image_def) + apply auto + done + +lemma commute_name_pre_state: +assumes "\s. P s \ monad_commute (op = s) f g" +shows "monad_commute P f g" + using assms + by (clarsimp simp:monad_commute_def) + +lemma commute_rewrite: +assumes rewrite: "\s. Q s \ f s = t s" + and hold : "\P\ g \\x. Q\" + shows "monad_commute R t g \ monad_commute (P and Q and R) f g" + apply (clarsimp simp:monad_commute_def bind_def split_def return_def) + apply (drule_tac x = s in spec) + apply (clarsimp simp:rewrite[symmetric]) + apply (intro conjI) + apply (rule set_eqI) + apply (rule iffI) + apply clarsimp + apply (rule bexI[rotated],assumption) + apply (subst rewrite) + apply (rule use_valid[OF _ hold]) + apply simp+ + apply (erule bexI[rotated],simp) + apply clarsimp + apply (rule bexI[rotated],assumption) + apply (subst rewrite[symmetric]) + apply (rule use_valid[OF _ hold]) + apply simp+ + apply (erule bexI[rotated],simp) + apply (intro iffI) + apply clarsimp + apply (rule bexI[rotated],assumption) + apply simp + apply (subst rewrite) + apply (erule(1) use_valid[OF _ hold]) + apply simp + apply (clarsimp) + apply (drule bspec,assumption) + apply clarsimp + apply (metis rewrite use_valid[OF _ hold]) + done + + +lemma commute_grab_asm: + "(F \ monad_commute P f g) \ (monad_commute (P and (K F)) f g)" + by (clarsimp simp: monad_commute_def) + end diff --git a/lib/Word_Lib/Word_Lemmas.thy b/lib/Word_Lib/Word_Lemmas.thy index feaad0d1d..0790c9588 100644 --- a/lib/Word_Lib/Word_Lemmas.thy +++ b/lib/Word_Lib/Word_Lemmas.thy @@ -5322,6 +5322,8 @@ lemma NOT_mask_shifted_lenword: apply (simp add: word_size nth_shiftl nth_shiftr) by auto +(* Comparisons between different word sizes. *) + lemma eq_ucast_ucast_eq: fixes x :: "'a::len word" and y :: "'b::len word" @@ -5364,4 +5366,20 @@ lemma ucast_le_ucast: apply simp done +(* High bits w.r.t. mask operations. *) + +lemma and_neg_mask_eq_iff_not_mask_le: + "w && ~~ mask n = ~~ mask n \ ~~ mask n \ w" + by (metis (full_types) dual_order.antisym neg_mask_mono_le word_and_le1 word_and_le2 + word_bool_alg.conj_absorb) + +lemma le_mask_high_bits: + shows "w \ mask n \ (\ i \ {n ..< size w}. \ w !! i)" + by (auto simp: word_size and_mask_eq_iff_le_mask[symmetric] word_eq_iff) + +lemma neg_mask_le_high_bits: + shows "~~ mask n \ w \ (\ i \ {n ..< size w}. w !! i)" + by (auto simp: word_size and_neg_mask_eq_iff_not_mask_le[symmetric] + word_eq_iff neg_mask_bang) + end diff --git a/lib/Word_Lib/Word_Lemmas_64.thy b/lib/Word_Lib/Word_Lemmas_64.thy index 5950375c3..bbe09523f 100644 --- a/lib/Word_Lib/Word_Lemmas_64.thy +++ b/lib/Word_Lib/Word_Lemmas_64.thy @@ -84,6 +84,23 @@ lemma unat_less_word_bits: lemmas unat_mask_word64' = unat_mask[where 'a=64] lemmas unat_mask_word64 = unat_mask_word64'[folded word_bits_def] +lemma Suc_unat_mask_div: + "Suc (unat (mask sz div word_size::word64)) = 2 ^ (min sz word_bits - 3)" + apply (case_tac "sz < word_bits") + apply (case_tac "3\sz") + apply (clarsimp simp: word_size_def word_bits_def min_def mask_def) + apply (drule (2) Suc_div_unat_helper + [where 'a=64 and sz=sz and us=3, simplified, symmetric]) + apply (simp add: not_le word_size_def word_bits_def) + apply (case_tac sz, simp add: unat_word_ariths) + apply (case_tac nat, simp add: unat_word_ariths + unat_mask_word64 min_def word_bits_def) + apply (case_tac nata, simp add: unat_word_ariths unat_mask_word64 word_bits_def) + apply simp + apply (simp add: unat_word_ariths + unat_mask_word64 min_def word_bits_def word_size_def) + done + lemmas word64_minus_one_le' = word_minus_one_le[where 'a=64] lemmas word64_minus_one_le = word64_minus_one_le'[simplified] diff --git a/lib/X64/WordSetup.thy b/lib/X64/WordSetup.thy new file mode 100644 index 000000000..7a8430541 --- /dev/null +++ b/lib/X64/WordSetup.thy @@ -0,0 +1,44 @@ +(* + * Copyright 2014, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + *) + + +theory WordSetup +imports + "../Distinct_Prop" + "../Word_Lib/Word_Lemmas_64" +begin + +(* Distinct_Prop lemmas that need word lemmas: *) + +lemma distinct_prop_enum: + "\ \x y. \ x \ stop; y \ stop; x \ y \ \ P x y \ + \ distinct_prop P [0 :: 'a :: len word .e. stop]" + apply (simp add: upto_enum_def distinct_prop_map del: upt.simps) + apply (rule distinct_prop_distinct) + apply simp + apply (simp add: less_Suc_eq_le del: upt.simps) + apply (erule_tac x="of_nat x" in meta_allE) + apply (erule_tac x="of_nat y" in meta_allE) + apply (frule_tac y=x in unat_le) + apply (frule_tac y=y in unat_le) + apply (erule word_unat.Rep_cases)+ + apply (simp add: toEnum_of_nat[OF unat_lt2p] + word_le_nat_alt) + done + +lemma distinct_prop_enum_step: + "\ \x y. \ x \ stop div step; y \ stop div step; x \ y \ \ P (x * step) (y * step) \ + \ distinct_prop P [0, step .e. stop]" + apply (simp add: upto_enum_step_def distinct_prop_map) + apply (rule distinct_prop_enum) + apply simp + done + +end diff --git a/proof/access-control/Retype_AC.thy b/proof/access-control/Retype_AC.thy index e6431ff78..5c32316d6 100644 --- a/proof/access-control/Retype_AC.thy +++ b/proof/access-control/Retype_AC.thy @@ -1168,7 +1168,7 @@ lemma usable_range_disjoint: < ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us" apply (rule minus_one_helper,simp) apply (rule neq_0_no_wrap) - apply (rule word32_plus_mono_right_split) + apply (rule machine_word_plus_mono_right_split) apply (simp add:shiftl_t2n range_cover_unat[OF cover] field_simps) apply (simp add:range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+ done diff --git a/proof/access-control/Syscall_AC.thy b/proof/access-control/Syscall_AC.thy index 3356e14c3..fece1e526 100644 --- a/proof/access-control/Syscall_AC.thy +++ b/proof/access-control/Syscall_AC.thy @@ -202,18 +202,6 @@ lemma set_thread_state_authorised[wp]: apply (wp sts_valid_untyped_inv ct_in_state_set hoare_vcg_ex_lift sts_obj_at_impossible | simp)+ - apply (rename_tac tcb_invocation) - apply (case_tac tcb_invocation, simp_all) - apply (wp hoare_case_option_wp sts_typ_ats set_thread_state_cte_wp_at - hoare_vcg_conj_lift static_imp_wp - | wp_once valid_case_option_post_wp - | simp)+ - apply ((clarsimp split: option.splits)+)[3] - apply ((wp - | simp)+)[2] - apply (rename_tac option) - apply (case_tac option, simp_all)[1] - apply (wp set_thread_state_tcb_at sts_obj_at_impossible | simp add: authorised_tcb_inv_def)+ apply (rename_tac cnode_invocation) apply (case_tac cnode_invocation, simp_all add: cnode_inv_auth_derivations_def authorised_cnode_inv_def)[1] diff --git a/proof/crefine/Arch_C.thy b/proof/crefine/Arch_C.thy index a7a669be0..2fc5fc572 100644 --- a/proof/crefine/Arch_C.thy +++ b/proof/crefine/Arch_C.thy @@ -3409,7 +3409,7 @@ proof - show "w \ w + (end - start)" using assms apply - - apply (rule word32_plus_mono_right_split, rule c) + apply (rule machine_word_plus_mono_right_split, rule c) apply (simp add:pbfs_less_wb') done diff --git a/proof/crefine/Detype_C.thy b/proof/crefine/Detype_C.thy index f80b548a1..96d615f2b 100644 --- a/proof/crefine/Detype_C.thy +++ b/proof/crefine/Detype_C.thy @@ -1640,13 +1640,13 @@ lemma deleteObjects_ccorres': apply (rule ccorres_assert) apply (rule ccorres_stateAssert_fwd) apply (subst bind_assoc[symmetric]) - apply (unfold freeMemory_def word_size_def) + apply (unfold freeMemory_def) apply (subst ksPSpace_update_ext) apply (subgoal_tac "bits \ word_bits") prefer 2 apply (clarsimp simp:cte_wp_at_ctes_of) - apply (clarsimp simp: mapM_x_storeWord_step intvl_range_conv - intvl_range_conv[where 'a=32, folded word_bits_def] + apply (clarsimp simp: mapM_x_storeWord_step[simplified word_size_bits_def] + intvl_range_conv intvl_range_conv[where 'a=32, folded word_bits_def] doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm bind_assoc modify_machinestate_assert_cnodes_swap modify_modify_bind) diff --git a/proof/drefine/KHeap_DR.thy b/proof/drefine/KHeap_DR.thy index 873d1e3ac..6aaa49746 100644 --- a/proof/drefine/KHeap_DR.thy +++ b/proof/drefine/KHeap_DR.thy @@ -3064,11 +3064,11 @@ lemma branch_map_simp1: apply (rule iffI) apply (subst(asm) shiftr_bl_of) apply simp - apply (rule_tac cref1=ref and cref'1="of_bl ref" in iffD1[OF guard_mask_shift]) - apply (simp add: word_rep_drop)+ + apply (rule_tac cref1=ref and cref'1="of_bl ref::word32" in iffD1[OF guard_mask_shift]) + apply (simp add: word_rep_drop) apply (subst shiftr_bl_of) apply simp+ - apply (drule_tac cref1=ref and cref'1="of_bl ref" in iffD2[OF guard_mask_shift,rotated]) + apply (drule_tac cref1=ref and cref'1="of_bl ref::word32" in iffD2[OF guard_mask_shift,rotated]) apply (simp add: word_rep_drop)+ done @@ -3080,7 +3080,7 @@ lemma branch_map_simp2: " \length cref \ 32; 0 < nata;nata + length list < length cref; list \ cref\ \ unat ((((of_bl cref)::word32) >> length cref - (nata + length list)) && mask nata) = nat (bl_to_bin (take nata (drop (length list) cref)))" apply (subgoal_tac "take nata (drop (length list) cref) \ drop (length list) cref") - apply (frule_tac iffD2[OF guard_mask_shift,rotated,where cref1="drop (length list) cref" and cref'1="of_bl cref"]) + apply (frule_tac iffD2[OF guard_mask_shift,rotated,where cref1="drop (length list) cref" and cref'1="of_bl cref::word32"]) defer apply clarsimp apply (subgoal_tac "nata\ length cref - length list") @@ -3183,7 +3183,7 @@ lemma resolve_address_bits_terminate_corres: opt_object_def transform_def split: nat.splits)+)[3] apply fastforce - apply (frule_tac cref1=ref and cref'1="of_bl ref" in iffD2[OF guard_mask_shift,rotated]) + apply (frule_tac cref1=ref and cref'1="of_bl ref::word32" in iffD2[OF guard_mask_shift,rotated]) apply (simp add: word_rep_drop)+ done diff --git a/proof/drefine/Tcb_DR.thy b/proof/drefine/Tcb_DR.thy index dec28f056..23bdcc8e3 100644 --- a/proof/drefine/Tcb_DR.thy +++ b/proof/drefine/Tcb_DR.thy @@ -1030,7 +1030,7 @@ lemma dcorres_tcb_update_ipc_buffer: (\ptr frame. doE cap_delete (obj_id', tcb_cnode_index 4); liftE $ thread_set (tcb_ipc_buffer_update (\_. ptr)) obj_id'; - liftE $ as_user obj_id' $ set_register TPIDRURW ptr; + liftE $ arch_tcb_set_ipc_buffer obj_id' ptr; liftE $ case_option (return ()) (case_prod diff --git a/proof/drefine/Untyped_DR.thy b/proof/drefine/Untyped_DR.thy index 2a0aa3c1b..61d434567 100644 --- a/proof/drefine/Untyped_DR.thy +++ b/proof/drefine/Untyped_DR.thy @@ -257,8 +257,8 @@ lemma freeMemory_dcorres: in use_valid) apply (simp add: do_machine_op_def split_def) apply wp - apply (clarsimp simp: freeMemory_def word_size_def - mapM_x_storeWord_step intvl_range_conv') + apply (clarsimp simp: freeMemory_def mapM_x_storeWord_step[simplified word_size_bits_def] + intvl_range_conv') apply (rule conjI, fastforce) apply clarsimp apply (erule use_valid[where P=P and Q="%_. P" for P]) @@ -947,7 +947,7 @@ lemma retype_transform_ref_subseteq_strong: apply (simp add:unat_of_nat_m1 less_imp_le) using cover apply (simp add:range_cover_def word_bits_def) - apply (rule word32_plus_mono_right_split[where sz = sz]) + apply (rule machine_word_plus_mono_right_split[where sz = sz]) using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::word32))"] apply (clarsimp simp:unat_of_nat_m1) using cover diff --git a/proof/infoflow/Example_Valid_State.thy b/proof/infoflow/Example_Valid_State.thy index b96cab505..4d4bc2356 100644 --- a/proof/infoflow/Example_Valid_State.thy +++ b/proof/infoflow/Example_Valid_State.thy @@ -682,7 +682,7 @@ where lemma irq_node_offs_min: "init_irq_node_ptr \ init_irq_node_ptr + (ucast (irq:: 10 word) << cte_level_bits)" - apply (rule_tac sz=28 in word32_plus_mono_right_split) + apply (rule_tac sz=28 in machine_word_plus_mono_right_split) apply (simp add: unat_word_ariths mask_def shiftl_t2n s0_ptr_defs cte_level_bits_def) apply (cut_tac x=irq and 'a=32 in ucast_less) apply simp @@ -1300,7 +1300,7 @@ lemma pspace_distinct_s0: apply (simp add: word_less_nat_alt) apply (simp add: mult.commute) apply (drule_tac y="0x10" and x="0xE0007FFF" in word_plus_mono_right) - apply (rule_tac sz=28 in word32_plus_mono_right_split) + apply (rule_tac sz=28 in machine_word_plus_mono_right_split) apply (simp add: unat_word_ariths mask_def) apply (cut_tac x=irqa and 'a=32 in ucast_less) apply simp @@ -1314,14 +1314,14 @@ lemma pspace_distinct_s0: and c="0xE0007FFF + (ucast irqa << 4)" and d="ucast irqa << 4" in word_sub_mono) apply simp apply simp - apply (rule_tac sz=28 in word32_plus_mono_right_split) + apply (rule_tac sz=28 in machine_word_plus_mono_right_split) apply (simp add: unat_word_ariths mask_def shiftl_t2n) apply (cut_tac x=irqa and 'a=32 in ucast_less) apply simp apply (simp add: word_less_nat_alt) apply (simp add: word_bits_def) apply simp - apply (rule_tac sz=28 in word32_plus_mono_right_split) + apply (rule_tac sz=28 in machine_word_plus_mono_right_split) apply (simp add: unat_word_ariths mask_def shiftl_t2n) apply (cut_tac x=irqa and 'a=32 in ucast_less) apply simp @@ -1346,7 +1346,7 @@ lemma pspace_distinct_s0: apply (simp add: word_less_nat_alt) apply (simp add: mult.commute) apply (drule_tac y="0x10" and x="0xE0007FFF" in word_plus_mono_right) - apply (rule_tac sz=28 in word32_plus_mono_right_split) + apply (rule_tac sz=28 in machine_word_plus_mono_right_split) apply (simp add: unat_word_ariths mask_def) apply (cut_tac x=irq and 'a=32 in ucast_less) apply simp @@ -1360,14 +1360,14 @@ lemma pspace_distinct_s0: and c="0xE0007FFF + (ucast irq << 4)" and d="ucast irq << 4" in word_sub_mono) apply simp apply simp - apply (rule_tac sz=28 in word32_plus_mono_right_split) + apply (rule_tac sz=28 in machine_word_plus_mono_right_split) apply (simp add: unat_word_ariths mask_def shiftl_t2n) apply (cut_tac x=irq and 'a=32 in ucast_less) apply simp apply (simp add: word_less_nat_alt) apply (simp add: word_bits_def) apply simp - apply (rule_tac sz=28 in word32_plus_mono_right_split) + apply (rule_tac sz=28 in machine_word_plus_mono_right_split) apply (simp add: unat_word_ariths mask_def shiftl_t2n) apply (cut_tac x=irq and 'a=32 in ucast_less) apply simp diff --git a/proof/invariant-abstract/ARM/ArchAcc_AI.thy b/proof/invariant-abstract/ARM/ArchAcc_AI.thy index 4f65f0f5b..f51f6cd65 100644 --- a/proof/invariant-abstract/ARM/ArchAcc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchAcc_AI.thy @@ -18,12 +18,6 @@ imports "../SubMonad_AI" begin -(*FIXME: Move or remove *) - -method spec for x :: "_ :: type" = (erule allE[of _ x]) -method bspec for x :: "_ :: type" = (erule ballE[of _ _ x]) -method prove for x :: "prop" = (rule revcut_rl[of "PROP x"]) - context Arch begin global_naming ARM @@ -221,105 +215,30 @@ lemma set_asid_pool_pred_tcb_at[wp]: apply (wpsimp wp: get_object_wp simp: pred_tcb_at_def obj_at_def) done -lemmas word_simps = - word_size word_ops_nth_size nth_ucast nth_shiftr nth_shiftl - pd_bits_def pageBits_def - + lemma mask_pd_bits_inner_beauty: "is_aligned p 2 \ (p && ~~ mask pd_bits) + (ucast ((ucast (p && mask pd_bits >> 2))::12 word) << 2) = (p::word32)" - apply (simp add: is_aligned_nth) - apply (subst word_plus_and_or_coroll; rule word_eqI) - subgoal - by (clarsimp simp: word_simps) - subgoal for n - apply (clarsimp simp: word_simps) - apply (rule iffI, (erule disjE;clarsimp)) - subgoal by (clarsimp simp: SucSucMinus) - apply (spec n) - apply (clarsimp simp: SucSucMinus) - by arith - done - + by (rule mask_split_aligned; simp add: pd_bits_def pageBits_def) lemma more_pd_inner_beauty: fixes x :: "12 word" fixes p :: word32 assumes x: "x \ ucast (p && mask pd_bits >> 2)" shows "(p && ~~ mask pd_bits) + (ucast x << 2) = p \ False" - apply (subst (asm) word_plus_and_or_coroll) - apply (clarsimp simp: word_simps bang_eq) - subgoal for n - apply (drule test_bit_size) - apply (clarsimp simp: word_simps) - by arith - apply (insert x) - apply (erule notE) - apply (rule word_eqI) - subgoal for n - apply (clarsimp simp: word_simps bang_eq) - apply (spec "n+2") - by (clarsimp simp: word_ops_nth_size word_size) - done - -lemma mask_alignment_ugliness: - "\ x \ x + z && ~~ mask m; - is_aligned (x + z && ~~ mask m) m; - is_aligned x m; - \n \ m. \z !! n\ - \ False" - apply (erule notE) - apply (rule word_eqI) - apply (clarsimp simp: is_aligned_nth word_ops_nth_size word_size pd_bits_def pageBits_def) - apply (subst word_plus_and_or_coroll) - apply (rule word_eqI) - apply (clarsimp simp: word_size) - - subgoal for \ na - apply (spec na)+ - by simp - by auto - + by (rule mask_split_aligned_neg[OF _ _ x]; simp add: pd_bits_def pageBits_def) lemma mask_pt_bits_inner_beauty: "is_aligned p 2 \ (p && ~~ mask pt_bits) + (ucast ((ucast (p && mask pt_bits >> 2))::word8) << 2) = (p::word32)" - apply (simp add: is_aligned_nth) - apply (subst word_plus_and_or_coroll; rule word_eqI) - subgoal by (clarsimp simp: word_simps) - apply (clarsimp simp: word_simps) - subgoal for n - apply (rule iffI) - apply (erule disjE;clarsimp) - subgoal by (prove "Suc (Suc (n - 2)) = n") simp+ - apply clarsimp - apply (rule context_conjI) - apply (rule leI) - subgoal by clarsimp - apply (prove "Suc (Suc (n - 2)) = n") subgoal by arith - by (simp add: pt_bits_def pageBits_def) - done - + by (rule mask_split_aligned; simp add: pt_bits_def pageBits_def) lemma more_pt_inner_beauty: fixes x :: "word8" fixes p :: word32 assumes x: "x \ ucast (p && mask pt_bits >> 2)" shows "(p && ~~ mask pt_bits) + (ucast x << 2) = p \ False" - apply (subst (asm) word_plus_and_or_coroll) - apply (clarsimp simp: word_size word_ops_nth_size nth_ucast - nth_shiftl bang_eq) - apply (drule test_bit_size) - apply (clarsimp simp: word_size pt_bits_def pageBits_def) - apply arith - apply (rule x[THEN notE]) - apply (rule word_eqI) - subgoal for n - apply (clarsimp simp: bang_eq word_simps) - apply (spec "n+2") - apply (clarsimp simp: word_ops_nth_size word_size) - by (clarsimp simp: pt_bits_def pageBits_def) - done + by (rule mask_split_aligned_neg[OF _ _ x]; simp add: pt_bits_def pageBits_def) lemma set_pd_aligned [wp]: @@ -511,9 +430,7 @@ lemma pde_shifting: apply (drule (1) order_le_less_trans) apply (drule bang_is_le) apply (drule order_le_less_trans[where z="2 ^ 4"], assumption) - apply (drule word_power_increasing) - apply (fold_subgoals (prefix))[4] - subgoal premises using prems by simp+ + apply (drule word_power_increasing; simp) apply (spec "n' + 20") apply (frule test_bit_size[where n = "n' + 20"]) by (simp add: word_size) diff --git a/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy b/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy index d50fe7fd4..477a82a34 100644 --- a/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy +++ b/proof/invariant-abstract/ARM/ArchBCorres2_AI.thy @@ -28,7 +28,7 @@ crunch (bcorres)bcorres[wp]: set_extra_badge,derive_cap truncate_state (ignore: crunch (bcorres)bcorres[wp]: invoke_untyped truncate_state (ignore: sequence_x) -crunch (bcorres)bcorres[wp]: set_mcpriority truncate_state +crunch (bcorres)bcorres[wp]: set_mcpriority,arch_tcb_set_ipc_buffer truncate_state lemma invoke_tcb_bcorres[wp]: fixes a diff --git a/proof/invariant-abstract/ARM/ArchCSpacePre_AI.thy b/proof/invariant-abstract/ARM/ArchCSpacePre_AI.thy index 38732313b..9ff910737 100644 --- a/proof/invariant-abstract/ARM/ArchCSpacePre_AI.thy +++ b/proof/invariant-abstract/ARM/ArchCSpacePre_AI.thy @@ -201,7 +201,8 @@ lemma same_aobject_as_commute: "same_aobject_as x y \ same_aobject_as y x" by (cases x; cases y; clarsimp) -lemmas wellformed_cap_simps = wellformed_cap_simps[simplified wellformed_acap_def, split_simps arch_cap.split] +lemmas wellformed_cap_simps = wellformed_cap_def + [simplified wellformed_acap_def, split_simps cap.split arch_cap.split] lemma same_master_cap_same_types: "cap_master_cap cap = cap_master_cap cap' \ diff --git a/proof/invariant-abstract/ARM/ArchCSpace_AI.thy b/proof/invariant-abstract/ARM/ArchCSpace_AI.thy index 8253109a0..b8ee39431 100644 --- a/proof/invariant-abstract/ARM/ArchCSpace_AI.thy +++ b/proof/invariant-abstract/ARM/ArchCSpace_AI.thy @@ -38,25 +38,24 @@ lemma weak_derived_valid_cap [CSpace_AI_assms]: apply (clarsimp simp: copy_of_def split: if_split_asm) apply (auto simp: is_cap_simps same_object_as_def wellformed_cap_simps valid_cap_def cap_aligned_def bits_of_def - aobj_ref_cases Let_def cap_asid_def - split: cap.splits arch_cap.splits option.splits) + aobj_ref_cases Let_def cap_asid_def + split: cap.splits arch_cap.splits option.splits) done -lemma weak_derived_tcb_cap_valid [CSpace_AI_assms]: +(* FIXME: unused *) +lemma weak_derived_tcb_cap_valid: "\ tcb_cap_valid cap p s; weak_derived cap cap' \ \ tcb_cap_valid cap' p s" apply (clarsimp simp add: tcb_cap_valid_def weak_derived_def obj_at_def is_tcb split: option.split) apply (clarsimp simp: st_tcb_def2) - apply (erule disjE, simp_all add: copy_of_def split: if_split_asm) - apply clarsimp - apply (clarsimp simp: tcb_cap_cases_def split: if_split_asm) - apply (auto simp: is_cap_simps same_object_as_def - valid_ipc_buffer_cap_def is_nondevice_page_cap_simps - is_nondevice_page_cap_arch_def - split: cap.split_asm arch_cap.split_asm - Structures_A.thread_state.split_asm)[3] - apply clarsimp + apply (erule disjE; simp add: copy_of_def split: if_split_asm; (solves \clarsimp\)?) + apply (clarsimp simp: tcb_cap_cases_def split: if_split_asm) + apply (auto simp: is_cap_simps same_object_as_def + valid_ipc_buffer_cap_def is_nondevice_page_cap_simps + is_nondevice_page_cap_arch_def + split: cap.split_asm arch_cap.split_asm + thread_state.split_asm) done lemma copy_obj_refs [CSpace_AI_assms]: @@ -268,12 +267,12 @@ lemma cap_insert_valid_arch_caps [CSpace_AI_assms]: prefer 2 apply (erule iffD2[OF caps_of_state_cteD']) apply (wp set_untyped_cap_as_full_cte_wp_at hoare_vcg_all_lift hoare_vcg_imp_lift - set_untyped_cap_as_full_cte_wp_at_neg hoare_vcg_ex_lift | clarsimp)+ + set_untyped_cap_as_full_cte_wp_at_neg hoare_vcg_ex_lift | clarsimp)+ apply (rule hoare_strengthen_post) prefer 2 apply (erule iffD2[OF caps_of_state_cteD']) apply (wp set_untyped_cap_as_full_cte_wp_at hoare_vcg_all_lift hoare_vcg_imp_lift - set_untyped_cap_as_full_cte_wp_at_neg hoare_vcg_ex_lift | clarsimp)+ + set_untyped_cap_as_full_cte_wp_at_neg hoare_vcg_ex_lift | clarsimp)+ apply (wp get_cap_wp)+ apply (intro conjI allI impI disj_subst) apply simp @@ -406,7 +405,7 @@ lemma update_cap_data_validI [CSpace_AI_assms]: apply (simp_all add: is_cap_defs update_cap_data_def Let_def split_def) apply (simp add: valid_cap_def cap_aligned_def) apply (simp add: valid_cap_def cap_aligned_def) - apply (simp add: the_cnode_cap_def valid_cap_def cap_aligned_def) + apply (simp add: the_cnode_cap_def valid_cap_def cap_aligned_def word_bits_def) apply (rename_tac arch_cap) apply (case_tac arch_cap) apply (simp_all add: is_cap_defs arch_update_cap_data_def) @@ -523,7 +522,7 @@ lemma cap_insert_simple_arch_caps_no_ap: end -global_interpretation CSpace_AI?: CSpace_AI_7 +global_interpretation CSpace_AI?: CSpace_AI proof goal_cases interpret Arch . case 1 show ?case by (unfold_locales; (fact CSpace_AI_assms)?) diff --git a/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy b/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy index d93595a07..83c6dbd35 100644 --- a/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDeterministic_AI.thy @@ -16,7 +16,8 @@ context Arch begin global_naming ARM named_theorems Deterministic_AI_assms -crunch valid_list[wp, Deterministic_AI_assms]: cap_swap_for_delete,set_cap,finalise_cap valid_list +crunch valid_list[wp, Deterministic_AI_assms]: + cap_swap_for_delete,set_cap,finalise_cap,arch_tcb_set_ipc_buffer valid_list (wp: crunch_wps simp: unless_def crunch_simps) end diff --git a/proof/invariant-abstract/ARM/ArchDetype_AI.thy b/proof/invariant-abstract/ARM/ArchDetype_AI.thy index 0d70e3f24..61a09c4ce 100644 --- a/proof/invariant-abstract/ARM/ArchDetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetype_AI.thy @@ -40,10 +40,10 @@ lemma caps_of_state_ko[Detype_AI_asms]: lemma mapM_x_storeWord[Detype_AI_asms]: (* FIXME: taken from Retype_C.thy and adapted wrt. the missing intvl syntax. *) - assumes al: "is_aligned ptr 2" - shows "mapM_x (\x. storeWord (ptr + of_nat x * 4) 0) [0..x. storeWord (ptr + of_nat x * word_size) 0) [0..m x. if \k. x = ptr + of_nat k \ k < n * 4 then 0 else m x))" + (\m x. if \k. x = ptr + of_nat k \ k < n * word_size then 0 else m x))" proof (induct n) case 0 thus ?case @@ -81,13 +81,13 @@ next from al have "is_aligned (ptr + of_nat n' * 4) 2" apply (rule aligned_add_aligned) apply (rule is_aligned_mult_triv2 [where n = 2, simplified]) - apply (simp add: word_bits_conv)+ + apply (simp add: word_bits_conv word_size_bits_def)+ done thus ?case apply (simp add: mapM_x_append bind_assoc Suc.hyps mapM_x_singleton) apply (simp add: storeWord_def assert_def is_aligned_mask modify_modify - comp_def) + comp_def word_size_def) apply (simp only: funs_eq) done qed @@ -599,16 +599,17 @@ lemma delete_objects_invs[wp]: apply (simp add: freeMemory_def word_size_def bind_assoc empty_fail_mapM_x ef_storeWord) apply (rule hoare_pre) - apply (rule_tac G="is_aligned ptr bits \ 2 \ bits \ bits \ word_bits" + apply (rule_tac G="is_aligned ptr bits \ word_size_bits \ bits \ bits \ word_bits" in hoare_grab_asm) - apply (simp add: mapM_storeWord_clear_um intvl_range_conv[where 'a=32, folded word_bits_def]) + apply (simp add: mapM_storeWord_clear_um[unfolded word_size_def] + intvl_range_conv[where 'a=machine_word_len, folded word_bits_def]) apply wp apply clarsimp apply (frule invs_untyped_children) apply (frule detype_invariants, clarsimp+) apply (drule invs_valid_objs) apply (drule (1) cte_wp_valid_cap) - apply (simp add: valid_cap_def cap_aligned_def) + apply (simp add: valid_cap_def cap_aligned_def word_size_bits_def) done end end diff --git a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy index 3dc5c8615..7a24b49c4 100644 --- a/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInterrupt_AI.thy @@ -12,7 +12,13 @@ theory ArchInterrupt_AI imports "../Interrupt_AI" begin -context Arch begin +context Arch begin global_naming ARM + +defs arch_irq_control_inv_valid_def: + "arch_irq_control_inv_valid irq_inv \ \" + +declare arch_irq_control_inv_valid_def [simp] + named_theorems Interrupt_AI_asms diff --git a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy index dea3be353..8a41bafe5 100644 --- a/proof/invariant-abstract/ARM/ArchInvariants_AI.thy +++ b/proof/invariant-abstract/ARM/ArchInvariants_AI.thy @@ -373,6 +373,8 @@ definition where "vs_lookup \ \s. vs_lookup_trans s `` vs_asid_refs (arm_asid_table (arch_state s))" +definition "second_level_tables \ arch_state.arm_global_pts" + end context begin interpretation Arch . diff --git a/proof/invariant-abstract/ARM/ArchIpc_AI.thy b/proof/invariant-abstract/ARM/ArchIpc_AI.thy index 49f08b9e9..8ca476a95 100644 --- a/proof/invariant-abstract/ARM/ArchIpc_AI.thy +++ b/proof/invariant-abstract/ARM/ArchIpc_AI.thy @@ -50,7 +50,7 @@ lemma update_cap_data_closedform: the_cnode_cap_def fst_conv snd_conv fun_app_def the_arch_cap_def arch_update_cap_data_def cong: if_cong) - apply auto + apply (auto simp: word_bits_def) done lemma cap_asid_PageCap_None [simp]: diff --git a/proof/invariant-abstract/ARM/ArchKHeap_AI.thy b/proof/invariant-abstract/ARM/ArchKHeap_AI.thy index 4588d7abb..6e6a9a3d3 100644 --- a/proof/invariant-abstract/ARM/ArchKHeap_AI.thy +++ b/proof/invariant-abstract/ARM/ArchKHeap_AI.thy @@ -261,13 +261,11 @@ lemma set_object_valid_kernel_mappings: lemma valid_vs_lookup_lift: assumes lookup: "\P. \\s. P (vs_lookup_pages s)\ f \\_ s. P (vs_lookup_pages s)\" assumes cap: "\P. \\s. P (caps_of_state s)\ f \\_ s. P (caps_of_state s)\" - assumes pts: "\P. \\s. P (arm_global_pts (arch_state s))\ f \\_ s. P (arm_global_pts (arch_state s))\" shows "\valid_vs_lookup\ f \\_. valid_vs_lookup\" unfolding valid_vs_lookup_def apply (rule hoare_lift_Pf [where f=vs_lookup_pages]) apply (rule hoare_lift_Pf [where f="\s. (caps_of_state s)"]) - apply (rule hoare_lift_Pf [where f="\s. arm_global_pts (arch_state s)"]) - apply (wp lookup cap pts)+ + apply (wp lookup cap)+ done @@ -402,7 +400,7 @@ lemma arch_lifts: apply (rule aobj_at) apply clarsimp done - + subgoal apply (simp add: valid_arch_state_def valid_asid_table_def) apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch]) diff --git a/proof/invariant-abstract/ARM/ArchRetype_AI.thy b/proof/invariant-abstract/ARM/ArchRetype_AI.thy index e31b8371f..b787aba63 100644 --- a/proof/invariant-abstract/ARM/ArchRetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchRetype_AI.thy @@ -58,14 +58,6 @@ lemma retype_region_ret_folded [Retype_AI_assms]: declare store_pde_state_refs_of [wp] -(* FIXME: move to Machine_R.thy *) -lemma clearMemory_corres: - "corres_underlying Id False True dc \ (\_. is_aligned y 2) - (clearMemory y a) (clearMemory y a)" - apply (rule corres_Id) - apply simp+ - done - (* These also prove facts about copy_global_mappings *) crunch pspace_aligned[wp]: init_arch_objects "pspace_aligned" (ignore: clearMemory wp: crunch_wps hoare_unless_wp) @@ -150,22 +142,6 @@ lemmas init_arch_objects_valid_cap[wp] = valid_cap_typ [OF init_arch_objects_typ lemmas init_arch_objects_cap_table[wp] = cap_table_at_lift_valid [OF init_arch_objects_typ_at] -lemma clearMemory_vms: - "valid_machine_state s \ - \x\fst (clearMemory ptr bits (machine_state s)). - valid_machine_state (s\machine_state := snd x\)" - apply (clarsimp simp: valid_machine_state_def - disj_commute[of "in_user_frame p s" for p s]) - apply (drule_tac x=p in spec, simp) - apply (drule_tac P4="\m'. underlying_memory m' p = 0" - in use_valid[where P=P and Q="\_. P" for P], simp_all) - apply (simp add: clearMemory_def cleanCacheRange_PoU_def machine_op_lift_def - machine_rest_lift_def split_def) - apply (wp hoare_drop_imps | simp | wp mapM_x_wp_inv)+ - apply (simp add: storeWord_def | wp)+ - apply (simp add: word_rsplit_0)+ - done - crunch device_state_inv[wp]: clearMemory "\ms. P (device_state ms)" (wp: mapM_x_wp) @@ -174,8 +150,6 @@ crunch cap_refs_respects_device_region[wp]: reserve_region cap_refs_respects_dev crunch invs [wp]: reserve_region "invs" -crunch invs [wp]: reserve_region "invs" - crunch iflive[wp]: copy_global_mappings "if_live_then_nonz_cap" (wp: crunch_wps) @@ -312,12 +286,8 @@ lemma store_pde_map_global_valid_arch_caps: lemma store_pde_map_global_valid_arch_objs: "\valid_arch_objs and valid_arch_state and valid_global_objs - and K (valid_pde_mappings pde) - and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) - \ kernel_vsrefs) - and (\s. \p. pde_ref pde = Some p - \ p \ set (arm_global_pts (arch_state s)))\ - store_pde p pde + and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \ kernel_vsrefs)\ + store_pde p pde \\rv. valid_arch_objs\" apply (simp add: store_pde_def) apply (wp set_pd_arch_objs_map[where T="{}" and S="{}"]) @@ -431,8 +401,6 @@ lemma copy_global_equal_kernel_mappings_restricted: apply (drule mp) apply (simp add: kernel_base_def pd_bits_def pageBits_def) apply (clarsimp simp: obj_at_def) - apply (case_tac "global_pd = pd") - apply simp apply (subst equal_kernel_mappings_specific_def) apply (fastforce simp add: obj_at_def restrict_map_def) apply (subst(asm) equal_kernel_mappings_specific_def) @@ -576,7 +544,7 @@ requalify_consts post_retype_invs_check end definition - post_retype_invs :: "apiobject_type \ word32 list \ 'z::state_ext state \ bool" + post_retype_invs :: "apiobject_type \ machine_word list \ 'z::state_ext state \ bool" where "post_retype_invs tp refs \ if post_retype_invs_check tp @@ -672,7 +640,7 @@ context Arch begin global_naming ARM lemma valid_untyped_helper [Retype_AI_assms]: assumes valid_c : "s \ c" and cte_at : "cte_wp_at (op = c) q s" - and tyunt: "ty \ Structures_A.apiobject_type.Untyped" + and tyunt: "ty \ Untyped" and cover : "range_cover ptr sz (obj_bits_api ty us) n" and range : "is_untyped_cap c \ usable_untyped_range c \ {ptr..ptr + of_nat (n * 2 ^ (obj_bits_api ty us)) - 1} = {}" and pn : "pspace_no_overlap_range_cover ptr sz s" @@ -847,18 +815,10 @@ end context retype_region_proofs_arch begin -lemma obj_at_valid_pte: - "\valid_pte pte s; \P p. obj_at P p s \ obj_at P p s'\ - \ valid_pte pte s'" - apply (cases pte,simp_all add: valid_pte_def data_at_def) - apply (clarsimp | elim disjE)+ - done - -lemma obj_at_valid_pde: - "\valid_pde pde s; \P p. obj_at P p s \ obj_at P p s'\ - \ valid_pde pde s'" - apply (cases pde, simp_all add: valid_pte_def data_at_def) - apply (clarsimp | elim disjE)+ +lemma valid_arch_obj_pres: + "valid_arch_obj ao s \ valid_arch_obj ao s'" + apply (cases ao; simp add: obj_at_pres) + apply (erule allEI ballEI; rename_tac t i; case_tac "t i"; fastforce simp: data_at_def obj_at_pres)+ done end @@ -887,12 +847,7 @@ proof have "valid_arch_obj ao s" by (auto simp: vs_lookup' elim: valid_arch_objsD) hence "valid_arch_obj ao s'" - apply (cases ao, simp_all add: obj_at_pres) - apply (erule allEI) - apply (erule (1) obj_at_valid_pte[OF _ obj_at_pres]) - apply (erule ballEI) - apply (erule (1) obj_at_valid_pde[OF _ obj_at_pres]) - done + by (rule valid_arch_obj_pres) } ultimately show "valid_arch_obj ao s'" by blast @@ -908,18 +863,16 @@ end context Arch begin global_naming ARM (*FIXME: arch_split*) definition - valid_vs_lookup2 :: "(vs_ref list \ word32) set \ word32 set \ (cslot_ptr \ cap) \ bool" + valid_vs_lookup2 :: "(vs_ref list \ word32) set \ (cslot_ptr \ cap) \ bool" where - "valid_vs_lookup2 lookup S caps \ + "valid_vs_lookup2 lookup caps \ \p ref. (ref, p) \ lookup \ ref \ [VSRef 0 (Some AASIDPool), VSRef 0 None] \ (\p' cap. caps p' = Some cap \ p \ obj_refs cap \ vs_cap_ref cap = Some ref)" lemma valid_vs_lookup_def2: - "valid_vs_lookup s = valid_vs_lookup2 - (vs_lookup_pages s) (set (arm_global_pts (arch_state s))) - (null_filter (caps_of_state s))" + "valid_vs_lookup s = valid_vs_lookup2 (vs_lookup_pages s) (null_filter (caps_of_state s))" apply (simp add: valid_vs_lookup_def valid_vs_lookup2_def) apply (intro iff_allI imp_cong[OF refl] disj_cong[OF refl] iff_exI conj_cong[OF refl]) @@ -947,12 +900,6 @@ lemma unique_table_refs_null: done -definition - region_in_kernel_window :: "word32 set \ 'z state \ bool" -where - "region_in_kernel_window S \ - \s. \x \ S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow" - lemma pspace_respects_device_regionI: assumes uat: "\ptr sz. kheap s ptr = Some (ArchObj (DataPage False sz)) \ obj_range ptr (ArchObj $ DataPage False sz) \ - device_region s" @@ -1020,8 +967,18 @@ lemma default_obj_dev: by (clarsimp simp: default_object_def default_arch_object_def split: apiobject_type.split_asm aobject_type.split_asm) + +definition + region_in_kernel_window :: "word32 set \ 'z state \ bool" +where + "region_in_kernel_window S \ + \s. \x \ S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow" + end +context begin interpretation Arch . +requalify_consts region_in_kernel_window +end lemma cap_range_respects_device_region_cong[cong]: @@ -1030,11 +987,6 @@ lemma cap_range_respects_device_region_cong[cong]: by (clarsimp simp: cap_range_respects_device_region_def) -context begin interpretation Arch . -requalify_consts region_in_kernel_window -end - - context retype_region_proofs_arch begin lemmas unique_table_caps_eq @@ -1064,16 +1016,6 @@ lemma valid_arch_caps: unique_table_refs_eq valid_table_caps) -lemma valid_arch_obj_pres: - "valid_arch_obj ao s \ valid_arch_obj ao s'" - apply (cases ao, simp_all) - apply (simp add: obj_at_pres) - apply (erule allEI) - apply (erule (1) obj_at_valid_pte[OF _ obj_at_pres]) - apply (erule ballEI) - apply (erule (1) obj_at_valid_pde[OF _ obj_at_pres]) - done - lemma valid_global_objs: "valid_global_objs s \ valid_global_objs s'" apply (simp add: valid_global_objs_def valid_ao_at_def) @@ -1314,7 +1256,6 @@ lemma storeWord_um_eq_0: \\_ m. underlying_memory m p = 0\" by (simp add: storeWord_def word_rsplit_0 | wp)+ - lemma clearMemory_um_eq_0: "\\m. underlying_memory m p = 0\ clearMemory ptr bits diff --git a/proof/invariant-abstract/ARM/ArchTcb_AI.thy b/proof/invariant-abstract/ARM/ArchTcb_AI.thy index 299d560cf..3504b113c 100644 --- a/proof/invariant-abstract/ARM/ArchTcb_AI.thy +++ b/proof/invariant-abstract/ARM/ArchTcb_AI.thy @@ -360,7 +360,7 @@ lemma update_cap_valid[Tcb_AI_asms]: split del: if_split) apply (simp add: badge_update_def cap_rights_update_def) apply (simp add: badge_update_def) - apply simp + apply (simp add: word_bits_def) apply (rename_tac arch_cap) using valid_validate_vm_rights[simplified valid_vm_rights_def] apply (case_tac arch_cap, simp_all add: acap_rights_update_def @@ -371,11 +371,16 @@ lemma update_cap_valid[Tcb_AI_asms]: crunch pred_tcb_at: switch_to_thread "pred_tcb_at proj P t" (wp: crunch_wps simp: crunch_simps) +crunch typ_at[wp]: invoke_tcb "\s. P (typ_at T p s)" + (ignore: check_cap_at setNextPC zipWithM + wp: hoare_drop_imps mapM_x_wp' check_cap_inv + simp: crunch_simps) end context begin interpretation Arch . requalify_consts is_cnode_or_valid_arch +requalify_facts invoke_tcb_typ_at end global_interpretation Tcb_AI?: Tcb_AI diff --git a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy index 74ab5b604..e164b0e49 100644 --- a/proof/invariant-abstract/ARM/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/ARM/ArchUntyped_AI.thy @@ -313,7 +313,7 @@ lemma delete_objects_rewrite[Untyped_AI_assms]: od" apply (clarsimp simp:delete_objects_def freeMemory_def word_size_def) apply (subgoal_tac "is_aligned (ptr &&~~ mask sz) sz") - apply (subst mapM_storeWord_clear_um) + apply (subst mapM_storeWord_clear_um[simplified word_size_def word_size_bits_def]) apply (simp) apply simp apply (simp add:range_cover_def) @@ -326,7 +326,7 @@ declare store_pde_pred_tcb_at [wp] (* nonempty_table *) definition - nonempty_table :: "word32 set \ Structures_A.kernel_object \ bool" + nonempty_table :: "machine_word set \ Structures_A.kernel_object \ bool" where "nonempty_table S ko \ (a_type ko = AArch APageTable \ a_type ko = AArch APageDirectory) @@ -342,7 +342,7 @@ lemma create_cap_valid_arch_caps[wp, Untyped_AI_assms]: and valid_cap (default_cap tp oref sz dev) and (\(s::'state_ext::state_ext state). \r\obj_refs (default_cap tp oref sz dev). (\p'. \ cte_wp_at (\cap. r \ obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) and cte_wp_at (op = cap.NullCap) cref and K (tp \ ArchObject ASIDPoolObj)\ create_cap tp sz p dev (cref, oref) \\rv. valid_arch_caps\" @@ -361,7 +361,7 @@ lemma create_cap_valid_arch_caps[wp, Untyped_AI_assms]: apply (case_tac cref, fastforce) apply (simp add: obj_ref_none_no_asid) apply (rule conjI) - apply (auto simp: is_cap_simps valid_cap_def + apply (auto simp: is_cap_simps valid_cap_def second_level_tables_def obj_at_def nonempty_table_def a_type_simps)[1] apply (clarsimp simp del: imp_disjL) apply (case_tac "\x. x \ obj_refs cap") @@ -549,15 +549,15 @@ lemma mapM_copy_global_mappings_nonempty_table[wp]: done lemma init_arch_objects_nonempty_table[Untyped_AI_assms, wp]: - "\(\s. \ (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s) + "\(\s. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ valid_global_objs s \ valid_arch_state s \ pspace_aligned s) and K (\ref\set refs. is_aligned ref (obj_bits_api tp us))\ init_arch_objects tp ptr bits us refs - \\rv s. \ (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s)\" + \\rv s. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\" apply (rule hoare_gen_asm) apply (simp add: init_arch_objects_def split del: if_split) apply (rule hoare_pre) - apply (wp hoare_unless_wp | wpc | simp add: reserve_region_def)+ + apply (wp hoare_unless_wp | wpc | simp add: reserve_region_def second_level_tables_def)+ apply (clarsimp simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def) done diff --git a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy index 7a3582871..781b98b77 100644 --- a/proof/invariant-abstract/ARM/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpace_AI.thy @@ -116,20 +116,14 @@ lemma pd_at_asid_unique: valid_arch_state s; asid < 2 ^ asid_bits; asid' < 2 ^ asid_bits \ \ asid = asid'" apply (clarsimp simp: vspace_at_asid_def) - apply (subgoal_tac "pd \ set (arm_global_pts (arch_state s))") - apply (drule(1) valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI])+ - apply (clarsimp simp: table_cap_ref_ap_eq[symmetric]) - apply (clarsimp simp: table_cap_ref_def - split: cap.split_asm arch_cap.split_asm option.split_asm) - apply (drule(2) unique_table_refsD, - simp+, clarsimp simp: table_cap_ref_def, - erule(1) asid_low_high_bits) - apply simp+ - apply clarsimp - apply (drule(2) vs_ref_order) - apply clarsimp - apply (drule(1) valid_global_ptsD) - apply (clarsimp simp: obj_at_def a_type_def) + apply (drule(1) valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI])+ + apply (clarsimp simp: table_cap_ref_ap_eq[symmetric]) + apply (clarsimp simp: table_cap_ref_def + split: cap.split_asm arch_cap.split_asm option.split_asm) + apply (drule(2) unique_table_refsD, + simp+, clarsimp simp: table_cap_ref_def, + erule(1) asid_low_high_bits) + apply simp+ done lemma pd_at_asid_unique2: @@ -4994,7 +4988,7 @@ lemma set_asid_pool_valid_arch_caps_map: apply (wp get_object_wp) apply clarsimp apply (frule obj_at_not_pt_not_in_global_pts[where p=pd], clarsimp+) - apply (simp add: a_type_def) + apply (simp add: a_type_def) apply (frule obj_at_not_pt_not_in_global_pts[where p=ap], clarsimp+) apply (clarsimp simp: obj_at_def valid_arch_caps_def caps_of_state_after_update) diff --git a/proof/invariant-abstract/BCorres_AI.thy b/proof/invariant-abstract/BCorres_AI.thy index 1f13db478..d5e4c7211 100644 --- a/proof/invariant-abstract/BCorres_AI.thy +++ b/proof/invariant-abstract/BCorres_AI.thy @@ -202,7 +202,7 @@ lemma throw_on_false_bcorres[wp]: "bcorres f f' \ bcorres (thro done context Arch begin - crunch (bcorres)bcorres[wp]: arch_finalise_cap truncate_state (simp: swp_def) + crunch (bcorres)bcorres[wp]: arch_finalise_cap truncate_state (simp: swp_def ignore: forM_x) end requalify_facts Arch.arch_finalise_cap_bcorres diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy index f011dcdcb..900aafb03 100644 --- a/proof/invariant-abstract/CSpace_AI.thy +++ b/proof/invariant-abstract/CSpace_AI.thy @@ -39,9 +39,13 @@ requalify_facts loadWord_inv valid_global_refsD2 arch_derived_is_device + valid_ao_at_lift + update_cnode_cap_data_def end +(* Proofs don't want to see these details. *) +declare update_cnode_cap_data_def [simp] definition capBadge_ordering :: "bool \ (badge option \ badge option) set" @@ -106,7 +110,7 @@ lemma gets_machine_state_modify: by (simp add: bind_def split_def simpler_gets_def simpler_modify_def) -locale CSpace_AI = +locale CSpace_AI_getActiveIRQ_wp = fixes state_ext_t :: "'state_ext::state_ext itself" assumes getActiveIRQ_wp[wp]: "\P :: 'state_ext state \ bool. @@ -120,7 +124,7 @@ lemma OR_choiceE_weak_wp: split: option.splits if_split_asm) done -context CSpace_AI begin +context CSpace_AI_getActiveIRQ_wp begin lemma preemption_point_inv: fixes P :: "'state_ext state \ bool" @@ -338,58 +342,59 @@ lemmas is_cap_defs = is_arch_cap_def is_zombie_def lemma guard_mask_shift: - fixes cref' :: word32 + fixes cref' :: "'a::len word" assumes postfix: "to_bl cref' = xs @ cref" shows "(length guard \ length cref \ - (cref' >> length cref - length guard) && mask (length guard) = of_bl guard) - = - (guard \ cref)" (is "(_ \ ?l = ?r) = _ " is "(?len \ ?shift) = ?prefix") + (cref' >> (length cref - length guard)) && mask (length guard) = of_bl guard) + = (guard \ cref)" (is "(_ \ ?l = ?r) = _ " is "(?len \ ?shift) = ?prefix") proof + let ?w_len = "len_of TYPE('a)" from postfix have "length (to_bl cref') = length xs + length cref" by simp - hence 32: "32 = \" by simp + hence w_len: "?w_len = \" by simp assume "?len \ ?shift" hence shift: ?shift and c_len: ?len by auto - from 32 c_len have "length guard \ 32" by simp + from w_len c_len have "length guard \ ?w_len" by simp with shift - have "(replicate (32 - length guard) False) @ guard = to_bl ?l" + have "(replicate (?w_len - length guard) False) @ guard = to_bl ?l" by (simp add: word_rep_drop) also - have "\ = replicate (32 - length guard) False @ - drop (32 - length guard) (to_bl (cref' >> length cref - length guard))" + have "\ = replicate (?w_len - length guard) False @ + drop (?w_len - length guard) (to_bl (cref' >> (length cref - length guard)))" by (simp add: bl_and_mask) also from c_len - have "\ = replicate (32 - length guard) False @ take (length guard) cref" - by (simp add: bl_shiftr 32 word_size postfix) + have "\ = replicate (?w_len - length guard) False @ take (length guard) cref" + by (simp add: bl_shiftr w_len word_size postfix) finally have "take (length guard) cref = guard" by simp thus ?prefix by (simp add: take_prefix) next + let ?w_len = "len_of TYPE('a)" assume ?prefix then obtain zs where cref: "cref = guard @ zs" by (auto simp: prefix_def less_eq_list_def) with postfix have to_bl_c: "to_bl cref' = xs @ guard @ zs" by simp hence "length (to_bl cref') = length \" by simp - hence 32: "32 = \" by simp + hence w_len: "?w_len = \" by simp from cref have c_len: "length guard \ length cref" by simp from cref have "length cref - length guard = length zs" by simp - hence "to_bl ?l = replicate (32-length guard) False @ - drop (32-length guard) (to_bl (cref' >> length zs))" + hence "to_bl ?l = replicate (?w_len - length guard) False @ + drop (?w_len - length guard) (to_bl (cref' >> (length zs)))" by (simp add: bl_and_mask) - also - have "drop (32-length guard) (to_bl (cref' >> length zs)) = guard" - by (simp add: bl_shiftr word_size 32 to_bl_c) + also + have "drop (?w_len - length guard) (to_bl (cref' >> (length zs))) = guard" + by (simp add: bl_shiftr word_size w_len to_bl_c) finally have "to_bl ?l = to_bl ?r" - by (simp add: word_rep_drop 32) + by (simp add: word_rep_drop w_len) with c_len show "?len \ ?shift" by simp qed @@ -914,7 +919,7 @@ lemma null_no_mdb: end - +(* True if cap' is derived from cap. *) definition is_derived :: "cdt \ cslot_ptr \ cap \ cap \ bool" where @@ -2722,16 +2727,6 @@ lemma weak_derived_Null: done -locale CSpace_AI_2 = CSpace_AI state_ext_t - for state_ext_t :: "'state_ext::state_ext itself" + - assumes weak_derived_valid_cap: - "\(s::'state_ext state) c c'. - \ s \ c; wellformed_cap c'; weak_derived c' c\ \ s \ c'" - assumes weak_derived_tcb_cap_valid: - "\(s::'state_ext state) cap p cap'. - \ tcb_cap_valid cap p s; weak_derived cap cap' \ \ tcb_cap_valid cap' p s" - - lemma weak_derived_refl [intro!, simp]: "weak_derived c c" by (simp add: weak_derived_def) @@ -3080,8 +3075,10 @@ lemma copy_of_Null2 [simp]: by (auto simp add: copy_of_def same_object_as_def is_cap_simps) -locale CSpace_AI_3 = CSpace_AI_2 state_ext_t - for state_ext_t :: "'state_ext::state_ext itself" + +locale CSpace_AI_weak_derived = + fixes state_ext_t :: "'state_ext::state_ext itself" + assumes weak_derived_valid_cap: + "\(s:: 'state_ext state) c c'. \ s \ c; wellformed_cap c'; weak_derived c' c\ \ s \ c'" assumes copy_obj_refs: "\cap cap'. copy_of cap cap' \ obj_refs cap' = obj_refs cap" assumes weak_derived_cap_class[simp]: @@ -3099,7 +3096,7 @@ lemma weak_derived_untyped_range: split: if_split_asm cap.splits) -context CSpace_AI_3 begin +context CSpace_AI_weak_derived begin lemma weak_derived_cap_range: "\dcap cap. weak_derived dcap cap \ cap_range dcap = cap_range cap" @@ -3110,7 +3107,7 @@ end locale mdb_move_abs_gen = mdb_move_abs src dest m s' s m'' m' - + CSpace_AI_3 state_ext_t + + CSpace_AI_weak_derived state_ext_t for state_ext_t :: "'state_ext::state_ext itself" and src dest m and s' :: "'state_ext state" @@ -3199,12 +3196,12 @@ lemma weak_derived_untyped2: lemma weak_derived_Null_eq [simp]: - "(weak_derived cap.NullCap cap) = (cap = cap.NullCap)" + "(weak_derived NullCap cap) = (cap = NullCap)" by (auto simp: weak_derived_def) lemma weak_derived_eq_Null [simp]: - "(weak_derived cap cap.NullCap) = (cap = cap.NullCap)" + "(weak_derived cap NullCap) = (cap = NullCap)" by (auto simp: weak_derived_def) @@ -3216,12 +3213,12 @@ lemma weak_derived_is_untyped: lemma weak_derived_irq [simp]: - "weak_derived cap.IRQControlCap cap = (cap = cap.IRQControlCap)" + "weak_derived IRQControlCap cap = (cap = IRQControlCap)" by (auto simp add: weak_derived_def copy_of_def same_object_as_def split: cap.splits) -lemmas (in CSpace_AI_3) weak_derived_ranges = +lemmas (in CSpace_AI_weak_derived) weak_derived_ranges = weak_derived_is_untyped weak_derived_untyped_range weak_derived_obj_refs @@ -3249,7 +3246,7 @@ lemma weak_derived_Reply: split: if_split_asm cap.split_asm) -lemmas (in CSpace_AI_3) weak_derived_replies = +lemmas (in CSpace_AI_weak_derived) weak_derived_replies = weak_derived_is_reply weak_derived_is_reply_master weak_derived_obj_ref_of @@ -3355,7 +3352,7 @@ end declare is_master_reply_cap_NullCap [simp] -context CSpace_AI_3 begin +context CSpace_AI_weak_derived begin lemma mdb_move_abs_gen: "\src dest m (s::'state_ext state). @@ -3556,8 +3553,8 @@ lemma set_free_index_valid_pspace: apply (clarsimp simp: is_nondevice_page_cap_simps) done -locale CSpace_AI_4 = CSpace_AI_3 state_ext_t - for state_ext_t :: "'state_ext::state_ext itself" + +locale CSpace_AI_set_free_index_invs = + fixes state_ext_t :: "'state_ext::state_ext itself" assumes set_free_index_invs_known_cap: "\cap idx. \\s::'state_ext state. (free_index_of cap \ idx \ is_untyped_cap cap \ idx \ 2^cap_bits cap) @@ -3565,7 +3562,7 @@ locale CSpace_AI_4 = CSpace_AI_3 state_ext_t set_cap (free_index_update (\_. idx) cap) cref \\rv s'. invs s'\" -lemma (in CSpace_AI_4) set_free_index_invs: +lemma (in CSpace_AI_set_free_index_invs) set_free_index_invs: "\\s::'state_ext state. (free_index_of cap \ idx \ is_untyped_cap cap \ idx \ 2^cap_bits cap) \ invs s \ cte_wp_at (\cp. \ptr sz dev idx' idx''. idx' \ idx \ cp = UntypedCap dev ptr sz idx' \ cap = UntypedCap dev ptr sz idx'') cref s\ @@ -3875,8 +3872,8 @@ lemma unique_table_refs_upd_eqD: done -locale CSpace_AI_5 = CSpace_AI_4 state_ext_t - for state_ext_t :: "'state_ext::state_ext itself" + +locale CSpace_AI_set_untyped_cap_as_full = + fixes state_ext_t :: "'state_ext::state_ext itself" assumes set_untyped_cap_as_full_valid_arch_caps: "\src_cap src cap. \valid_arch_caps and cte_wp_at (op = src_cap) src\ @@ -3943,8 +3940,8 @@ lemma derived_cap_master_cap_eq: "is_derived m n b c \ cap_maste by (clarsimp simp:is_derived_def split:if_splits) -locale CSpace_AI_6 = CSpace_AI_5 state_ext_t - for state_ext_t :: "'state_ext::state_ext itself" + +locale CSpace_AI_cap_insert = + fixes state_ext_t :: "'state_ext::state_ext itself" assumes cap_insert_valid_arch_caps: "\src cap dest. \valid_arch_caps and (\s::'state_ext state. cte_wp_at (is_derived (cdt s) src cap) src s)\ @@ -4100,7 +4097,7 @@ lemma valid_irq_states_exst_update[simp]: by(auto simp: valid_irq_states_def) -context CSpace_AI_6 begin +context CSpace_AI_cap_insert begin interpretation cap_insert_crunches . @@ -4231,7 +4228,12 @@ lemma cap_swap_valid_objs: done -locale CSpace_AI_7 = CSpace_AI_6 state_ext_t +locale CSpace_AI + = CSpace_AI_getActiveIRQ_wp state_ext_t + + CSpace_AI_weak_derived state_ext_t + + CSpace_AI_set_free_index_invs state_ext_t + + CSpace_AI_set_untyped_cap_as_full state_ext_t + + CSpace_AI_cap_insert state_ext_t for state_ext_t :: "'state_ext::state_ext itself" + assumes mask_cap_valid[simp]: "\(s::'state_ext state) c R. s \ c \ s \ mask_cap R c" @@ -4582,7 +4584,7 @@ lemma appropriate_cte_cap_def2: \ (\ irq. cte_cap \ IRQHandlerCap irq))" by (clarsimp simp: appropriate_cte_cap_def cap_irqs_def cap_irq_opt_def split: cap.split) -context CSpace_AI_7 begin +context CSpace_AI begin lemma setup_reply_master_ifunsafe[wp]: "\t. @@ -4654,10 +4656,8 @@ crunch empty_table_at[wp]: setup_reply_master "obj_at (empty_table S) p" (ignore: set_cap wp: set_cap_obj_at_impossible crunch_wps simp: if_apply_def2 empty_table_caps_of) - lemmas setup_reply_master_valid_ao_at[wp] - = ARM.valid_ao_at_lift [OF setup_reply_master_typ_at setup_reply_master_arch_ko_at] - + = valid_ao_at_lift [OF setup_reply_master_typ_at setup_reply_master_arch_ko_at] crunch v_ker_map[wp]: setup_reply_master "valid_kernel_mappings" @@ -4686,7 +4686,7 @@ lemma setup_reply_master_cap_refs_respects_device_region[wp]: apply (auto simp: cte_wp_at_caps_of_state) done -context CSpace_AI_7 begin +context CSpace_AI begin crunch cap_refs_in_kernel_window[wp]: setup_reply_master "cap_refs_in_kernel_window" end @@ -4718,7 +4718,7 @@ lemma setup_reply_master_vms[wp]: crunch valid_irq_states[wp]: setup_reply_master "valid_irq_states" -context CSpace_AI_7 begin +context CSpace_AI begin lemma setup_reply_master_invs[wp]: "\t. @@ -4750,7 +4750,7 @@ definition is_untyped_cap parent \ descendants_of p m = {})" -context CSpace_AI_7 begin +context CSpace_AI begin lemma safe_parent_cap_range: "\ m p cap pcap. safe_parent_for m p cap pcap \ cap_range cap \ cap_range pcap" @@ -4784,7 +4784,7 @@ lemma safe_parent_is_parent: done -context CSpace_AI_7 begin +context CSpace_AI begin lemma safe_parent_ut_descendants: "\m p cap pcap. @@ -4922,7 +4922,7 @@ lemma (in mdb_insert_abs) reply_mdb_simple: by (simp add: reply_caps_mdb_simple reply_masters_mdb_simple) -context CSpace_AI_7 begin +context CSpace_AI begin lemma cap_insert_simple_mdb: fixes dest src cap diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index f3adaed05..46eed9edc 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -1665,6 +1665,9 @@ lemma set_mcpriority_valid_sched[wp]: crunch simple_sched_action[wp]: set_priority,set_mcpriority simple_sched_action context begin interpretation Arch . (*FIXME: arch_split*) + +crunch valid_sched[wp]: arch_tcb_set_ipc_buffer valid_sched + lemma tc_valid_sched[wp]: "\valid_sched and simple_sched_action\ invoke_tcb (ThreadControl a sl b mcp pr e f g) @@ -1675,6 +1678,7 @@ lemma tc_valid_sched[wp]: apply (wp check_cap_inv thread_set_not_state_valid_sched hoare_vcg_all_lift gts_wp static_imp_wp | wpc | simp add: option_update_thread_def)+ done + end lemma set_scheduler_action_swt_weak_valid_sched: diff --git a/proof/invariant-abstract/Deterministic_AI.thy b/proof/invariant-abstract/Deterministic_AI.thy index 2ac6ec234..42c2a1dd3 100644 --- a/proof/invariant-abstract/Deterministic_AI.thy +++ b/proof/invariant-abstract/Deterministic_AI.thy @@ -3895,6 +3895,8 @@ locale Deterministic_AI_1 = "\param_a param_b. \valid_list\ finalise_cap param_a param_b \\_. valid_list\" assumes get_cap_valid_list[wp]: "\param_a. \valid_list\ get_cap param_a \\_. valid_list\" + assumes arch_tcb_set_ipc_buffer_valid_list[wp]: + "\t ptr. \valid_list\ arch_tcb_set_ipc_buffer t ptr \\_. valid_list\" context Deterministic_AI_1 begin diff --git a/proof/invariant-abstract/Detype_AI.thy b/proof/invariant-abstract/Detype_AI.thy index 58370f6de..2c2943d47 100644 --- a/proof/invariant-abstract/Detype_AI.thy +++ b/proof/invariant-abstract/Detype_AI.thy @@ -23,10 +23,10 @@ locale Detype_AI = cap_range cap = {} \ (\ptr \ cap_range cap. \ko. kheap s ptr = Some ko)" assumes mapM_x_storeWord: - "\ptr. is_aligned ptr 2 - \ mapM_x (\x. storeWord (ptr + of_nat x * 4) 0) [0..ptr. is_aligned ptr word_size_bits + \ mapM_x (\x. storeWord (ptr + of_nat x * word_size) 0) [0..m x. if \k. x = ptr + of_nat k \ k < n * 4 then 0 else m x))" + (\m x. if \k. x = ptr + of_nat k \ k < n * word_size then 0 else m x))" assumes empty_fail_freeMemory: "empty_fail (freeMemory ptr bits)" @@ -73,7 +73,7 @@ lemma state_refs_of_detype: definition - obj_reply_refs :: "cap \ word32 set" + obj_reply_refs :: "cap \ machine_word set" where "obj_reply_refs cap \ obj_refs cap \ (case cap of cap.ReplyCap t m \ {t} | _ \ {})" @@ -897,15 +897,14 @@ lemma of_nat_le_pow: apply simp done -(* FIXME: move, fix underlying -1 problem *) -lemma maxword_32_conv: "(x::32 word) + 0xFFFFFFFF = x - 1" by simp +lemma maxword_len_conv': "(x::machine_word) + max_word = x - 1" by (simp add: max_word_def) (* FIXME: copied from Retype_C and slightly adapted. *) lemma (in Detype_AI) mapM_x_storeWord_step: assumes al: "is_aligned ptr sz" - and sz2: "2 \ sz" + and sz2: "word_size_bits \ sz" and sz: "sz <= word_bits" - shows "mapM_x (\p. storeWord p 0) [ptr , ptr + 4 .e. ptr + 2 ^ sz - 1] = + shows "mapM_x (\p. storeWord p 0) [ptr , ptr + word_size .e. ptr + 2 ^ sz - 1] = modify (underlying_memory_update (\m x. if x \ {x. \k. x = ptr + of_nat k \ k < 2 ^ sz} then 0 else m x))" using al sz @@ -913,21 +912,20 @@ lemma (in Detype_AI) mapM_x_storeWord_step: apply (subst if_not_P) apply (subst not_less) apply (erule is_aligned_no_overflow) - apply (simp add: mapM_x_map comp_def upto_enum_word maxword_32_conv del: upt.simps) - apply (simp add:Suc_unat_mask_div[simplified mask_2pm1 word_size_def] min_def) + apply (simp add: mapM_x_map comp_def upto_enum_word maxword_len_conv' del: upt.simps) + apply (simp add: Suc_unat_mask_div_obfuscated[simplified mask_2pm1] min_def) apply (subst mapM_x_storeWord) apply (erule is_aligned_weaken [OF _ sz2]) apply (rule arg_cong) - apply (subgoal_tac "2^2 = (4::nat)") - apply (cut_tac power_add[symmetric,of "2::nat" "sz - 2" 2]) - apply (simp only: le_add_diff_inverse2[OF sz2]) - apply simp + apply (subgoal_tac "2^word_size_bits = (word_size :: nat)") + apply (cut_tac power_add[symmetric,of "2::nat" "sz - word_size_bits" word_size_bits]) + apply (simp only: le_add_diff_inverse2[OF sz2]) + apply (simp add: word_size_size_bits_nat) done - lemma (in Detype_AI) mapM_storeWord_clear_um: - "is_aligned p n \ 2\n \ n<=word_bits \ - do_machine_op (mapM_x (\p. storeWord p 0) [p, p + 4 .e. p + 2 ^ n - 1]) = + "is_aligned p n \ word_size_bits\n \ n<=word_bits \ + do_machine_op (mapM_x (\p. storeWord p 0) [p, p + word_size .e. p + 2 ^ n - 1]) = modify (clear_um {x. \k. x = p + of_nat k \ k < 2 ^ n})" apply (simp add: mapM_x_storeWord_step) apply (rule ext) @@ -1000,7 +998,7 @@ lemma dom_known_length: lemma of_bl_length2: - "length xs < word_bits - cte_level_bits \ of_bl xs * 16 < (2 :: word32) ^ (length xs + 4)" + "length xs < word_bits - cte_level_bits \ of_bl xs * 16 < (2 :: machine_word) ^ (length xs + 4)" apply (simp add: power_add) apply (rule word_mult_less_mono1) apply (rule of_bl_length, simp add: word_bits_def) @@ -1122,9 +1120,9 @@ lemma refl_spec[simp]: by clarsimp lemma pre_helper: - "\base x n. \ is_aligned (base :: word32) (n + 4); n + 4 < word_bits \ - \ base + (x && mask n) * 16 \ {base .. base + 2 ^ (n + 4) - 1}" - apply (subgoal_tac "(x && mask n) * 0x10 < 2 ^ (n + 4)") + "\base x n. \ is_aligned (base :: machine_word) (n + (a::nat)); n + a < word_bits \ + \ base + (x && mask n) * 2^a \ {base .. base + 2 ^ (n + a) - 1}" + apply (subgoal_tac "(x && mask n) * bit(a) < 2 ^ (n + a)") apply simp apply (rule context_conjI) apply (erule(1) is_aligned_no_wrap') @@ -1136,13 +1134,14 @@ lemma pre_helper: apply (simp add: power_add) apply (rule word_mult_less_mono1) apply (rule and_mask_less_size, simp add: word_size word_bits_def) - apply simp + apply (simp add: p2_gt_0 word_bits_def) apply (simp add: word_bits_def) apply (drule power_strict_increasing[where a="2 :: nat"], simp_all) + apply (simp add: power_add[where a="2::nat"]) done lemma pre_helper2: - "\base x n. \ is_aligned (base :: word32) n; n < word_bits; 2 \ n; x < 2 ^ (n - 2) \ + "\base x n. \ is_aligned (base :: machine_word) n; n < word_bits; 2 \ n; x < 2 ^ (n - 2) \ \ base + x * 4 \ {base .. base + 2 ^ n - 1}" apply (subgoal_tac "x * 4 < 2 ^ n") apply simp @@ -1166,20 +1165,11 @@ lemma pre_helper2: lemmas ucast_ucast_mask_8 = ucast_ucast_mask[where 'a=8, simplified, symmetric] - -lemma subset_eq_notI: "\a\ B;a\ C\ \ \ B \ C" by auto - - lemma pspace_no_overlap_obj_range: "\ pspace_no_overlap S s; kheap s p = Some obj \ \ obj_range p obj \ S = {}" by (auto simp add: pspace_no_overlap_def obj_range_def field_simps) -lemma commute_grab_asm: - "(F \ monad_commute P f g) \ (monad_commute (P and (K F)) f g)" - by (clarsimp simp: monad_commute_def) - - (* FIXME: generalised version of Arch_AI.range_cover_full *) lemma range_cover_full: "\is_aligned (ptr :: 'a :: len word) sz;sz < len_of TYPE('a)\ \ range_cover ptr sz sz (Suc 0)" @@ -1192,68 +1182,6 @@ lemma range_cover_plus_us: apply simp+ done -lemma commute_name_pre_state: -assumes "\s. P s \ monad_commute (op = s) f g" -shows "monad_commute P f g" - using assms - by (clarsimp simp:monad_commute_def) - -lemma commute_rewrite: -assumes rewrite: "\s. Q s \ f s = t s" - and hold : "\P\ g \\x. Q\" - shows "monad_commute R t g \ monad_commute (P and Q and R) f g" - apply (clarsimp simp:monad_commute_def bind_def split_def return_def) - apply (drule_tac x = s in spec) - apply (clarsimp simp:rewrite[symmetric]) - apply (intro conjI) - apply (rule set_eqI) - apply (rule iffI) - apply clarsimp - apply (rule bexI[rotated],assumption) - apply (subst rewrite) - apply (rule use_valid[OF _ hold]) - apply simp+ - apply (erule bexI[rotated],simp) - apply clarsimp - apply (rule bexI[rotated],assumption) - apply (subst rewrite[symmetric]) - apply (rule use_valid[OF _ hold]) - apply simp+ - apply (erule bexI[rotated],simp) - apply (intro iffI) - apply clarsimp - apply (rule bexI[rotated],assumption) - apply simp - apply (subst rewrite) - apply (erule(1) use_valid[OF _ hold]) - apply simp - apply (clarsimp) - apply (drule bspec,assumption) - apply clarsimp - apply (metis rewrite use_valid[OF _ hold]) - done - -lemma mapM_x_commute: -assumes commute: - "\r. monad_commute (P r) a (b r)" -and single: - "\r x. \P r and K (f r \ f x) and P x\ b x \\v. P r \" -shows - "monad_commute (\s. (distinct (map f list)) \ (\r\ set list. P r s)) a (mapM_x b list)" - apply (induct list) - apply (clarsimp simp:mapM_x_Nil return_def bind_def monad_commute_def) - apply (clarsimp simp:mapM_x_Cons) - apply (rule monad_commute_guard_imp) - apply (rule monad_commute_split) - apply assumption - apply (rule monad_commute_guard_imp[OF commute]) - apply assumption - apply (wp hoare_vcg_ball_lift) - apply (rule single) - apply (clarsimp simp: image_def) - apply auto - done - lemma mask_sub: "n \ m \ mask m - mask n = mask m && ~~ mask n" apply (simp add: field_simps) apply (subst word_plus_and_or_coroll) @@ -1333,29 +1261,6 @@ lemma range_cover_tail_mask: done -lemma monad_eq_split2: -assumes eq: " g' s = g s" -assumes tail:"\r s. Q r s \ f r s = f' r s" -and hoare: "\P\g\\r s. Q r s\" "P s" -shows "(g>>=f) s = (g'>>= f') s" -proof - -have pre: "\aa bb. \(aa, bb) \ fst (g s)\ \ Q aa bb" - using hoare by (auto simp: valid_def) -show ?thesis - apply (simp add:bind_def eq split_def image_def) - apply (rule conjI) - apply (rule set_eqI) - apply (clarsimp simp:Union_eq) - apply (metis pre surjective_pairing tail) - apply (metis pre surjective_pairing tail) - done -qed - -lemma monad_eq_split_tail: - "\f = g;a s = b s\ \ (a >>= f) s = ((b >>= g) s)" - by (simp add:bind_def) - - lemma shift_distinct_helper: "\ (x :: 'a :: len word) < bnd; y < bnd; x \ y; x << n = y << n; n < len_of TYPE('a); bnd - 1 \ 2 ^ ((len_of TYPE('a)) - n) - 1 \ diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index f3a0096f6..b5feb5f1d 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -984,7 +984,7 @@ crunch tcb_at[wp]: unbind_notification "tcb_at t" locale Finalise_AI_3 = Finalise_AI_2 a b for a :: "('a :: state_ext) itself" and b :: "('b :: state_ext) itself" + - fixes replaceable_or_arch_update :: "'a state \ 32 word \ bool list \ cap \ cap \ bool" + fixes replaceable_or_arch_update :: "'a state \ machine_word \ bool list \ cap \ cap \ bool" fixes c :: "'c itself" assumes finalise_cap_invs: "\ cap slot x. diff --git a/proof/invariant-abstract/Interrupt_AI.thy b/proof/invariant-abstract/Interrupt_AI.thy index 4d6c602f3..7edbe2f96 100644 --- a/proof/invariant-abstract/Interrupt_AI.thy +++ b/proof/invariant-abstract/Interrupt_AI.thy @@ -39,17 +39,20 @@ where \ cte_wp_at (interrupt_derived cap) cte_ptr s \ s \ cap \ is_ntfn_cap cap)" +consts + arch_irq_control_inv_valid :: "arch_irq_control_invocation \ ('a :: state_ext) state \ bool" primrec - irq_control_inv_valid :: "irq_control_invocation \ 'z::state_ext state \ bool" + irq_control_inv_valid :: "irq_control_invocation \ 'a::state_ext state \ bool" where - "irq_control_inv_valid (Invocations_A.ArchIRQControl ivk) = \" + "irq_control_inv_valid (Invocations_A.ArchIRQControl ivk) = (arch_irq_control_inv_valid ivk)" | "irq_control_inv_valid (Invocations_A.IRQControl irq ptr ptr') = (cte_wp_at (op = cap.NullCap) ptr and cte_wp_at (op = cap.IRQControlCap) ptr' and ex_cte_cap_wp_to is_cnode_cap ptr and real_cte_at ptr and K (irq \ maxIRQ))" + locale Interrupt_AI = fixes state_ext_type1 :: "('a :: state_ext) itself" assumes decode_irq_control_invocation_inv[wp]: @@ -108,7 +111,12 @@ locale Interrupt_AI = "\ f irq. empty_fail (maskInterrupt f irq)" assumes handle_interrupt_invs [wp]: "\ irq. \invs :: 'a state \ bool\ handle_interrupt irq \\_. invs\" - + assumes sts_arch_irq_control_inv_valid [wp]: + "\i t st. + \arch_irq_control_inv_valid i :: 'a state \ bool\ + set_thread_state t st + \\rv. arch_irq_control_inv_valid i\" + crunch inv[wp]: decode_irq_handler_invocation "P" (simp: crunch_simps) diff --git a/proof/invariant-abstract/Invariants_AI.thy b/proof/invariant-abstract/Invariants_AI.thy index f09c9dcff..5b7041014 100644 --- a/proof/invariant-abstract/Invariants_AI.thy +++ b/proof/invariant-abstract/Invariants_AI.thy @@ -216,7 +216,7 @@ where subsection "Valid caps and objects" primrec - untyped_range :: "cap \ word32 set" + untyped_range :: "cap \ machine_word set" where "untyped_range (cap.UntypedCap dev p n f) = {p..p + (1 << n) - 1}" | "untyped_range (cap.NullCap) = {}" @@ -231,10 +231,10 @@ where | "untyped_range (cap.Zombie r b n) = {}" | "untyped_range (cap.ArchObjectCap cap) = {}" -primrec - usable_untyped_range :: "cap \ word32 set" +primrec (nonexhaustive) + usable_untyped_range :: "cap \ machine_word set" where - "usable_untyped_range (cap.UntypedCap _ p n f) = + "usable_untyped_range (UntypedCap _ p n f) = (if f < 2^n then {p+of_nat f .. p + 2 ^ n - 1} else {})" definition @@ -300,7 +300,7 @@ where case c of UntypedCap dev p sz idx \ sz \ 4 | NotificationCap r badge rights \ AllowGrant \ rights - | CNodeCap r bits guard \ bits \ 0 \ length guard \ 32 + | CNodeCap r bits guard \ bits \ 0 \ length guard \ word_bits | IRQHandlerCap irq \ irq \ maxIRQ | Zombie r b n \ (case b of None \ n \ 5 | Some b \ n \ 2 ^ b \ b \ 0) @@ -336,7 +336,7 @@ where | NotificationCap r badge rights \ ntfn_at r s \ AllowGrant \ rights | CNodeCap r bits guard \ - cap_table_at bits r s \ bits \ 0 \ length guard \ 32 + cap_table_at bits r s \ bits \ 0 \ length guard \ word_bits | ThreadCap r \ tcb_at r s | DomainCap \ True | ReplyCap r m \ tcb_at r s diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index ba4ee4ae4..7544d75d3 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -811,7 +811,7 @@ lemma suspend_unlive: done -definition bound_refs_of_tcb :: "'a state \ 32 word \ (32 word \ reftype) set" +definition bound_refs_of_tcb :: "'a state \ machine_word \ (machine_word \ reftype) set" where "bound_refs_of_tcb s t \ case kheap s t of Some (TCB tcb) \ tcb_bound_refs (tcb_bound_notification tcb) diff --git a/proof/invariant-abstract/LevityCatch_AI.thy b/proof/invariant-abstract/LevityCatch_AI.thy index 41e899dcb..fb2fb8250 100644 --- a/proof/invariant-abstract/LevityCatch_AI.thy +++ b/proof/invariant-abstract/LevityCatch_AI.thy @@ -19,6 +19,12 @@ requalify_facts end +(*FIXME: Move or remove *) + +method spec for x :: "_ :: type" = (erule allE[of _ x]) +method bspec for x :: "_ :: type" = (erule ballE[of _ _ x]) +method prove for x :: "prop" = (rule revcut_rl[of "PROP x"]) + lemmas aobj_ref_arch_cap_simps[simp] = aobj_ref_arch_cap lemma detype_arch_state : @@ -81,7 +87,58 @@ lemma select_ext_wp[wp]:"\\s. a s \ S \ Q (a (* FIXME: move *) lemmas mapM_UNIV_wp = mapM_wp[where S="UNIV", simplified] -(* FIXME: move *) -lemma bexEI: "\\x\S. Q x; \x. \x \ S; Q x\ \ P x\ \ \x\S. P x" by blast +lemmas word_simps = + word_size word_ops_nth_size nth_ucast nth_shiftr nth_shiftl + +lemma mask_split_aligned: + assumes len: "m \ a + len_of TYPE('a)" + assumes align: "is_aligned p a" + shows "(p && ~~ mask m) + (ucast ((ucast (p && mask m >> a))::'a::len word) << a) = p" + apply (insert align[simplified is_aligned_nth]) + apply (subst word_plus_and_or_coroll; rule word_eqI; clarsimp simp: word_simps) + apply (rule iffI) + apply (erule disjE; clarsimp) + apply (case_tac "n < m"; case_tac "n < a") + using len by auto + +lemma mask_split_aligned_neg: + fixes x :: "'a::len word" + fixes p :: "'b::len word" + assumes len: "a + len_of TYPE('a) \ len_of TYPE('b)" + "m = a + len_of TYPE('a)" + assumes x: "x \ ucast (p && mask m >> a)" + shows "(p && ~~ mask m) + (ucast x << a) = p \ False" + apply (subst (asm) word_plus_and_or_coroll) + apply (clarsimp simp: word_simps bang_eq) + subgoal for n + apply (drule test_bit_size) + apply (clarsimp simp: word_simps) + using len by arith + apply (insert x) + apply (erule notE) + apply (rule word_eqI) + subgoal for n + using len + apply (clarsimp simp: word_simps bang_eq) + apply (spec "n + a") + by (clarsimp simp: word_ops_nth_size word_size) + done + +lemma mask_alignment_ugliness: + "\ x \ x + z && ~~ mask m; + is_aligned (x + z && ~~ mask m) m; + is_aligned x m; + \n \ m. \z !! n\ + \ False" + apply (erule notE) + apply (rule word_eqI) + apply (clarsimp simp: is_aligned_nth word_ops_nth_size word_size) + apply (subst word_plus_and_or_coroll) + apply (rule word_eqI) + apply (clarsimp simp: word_size) + subgoal for \ na + apply (spec na)+ + by simp + by auto end diff --git a/proof/invariant-abstract/Retype_AI.thy b/proof/invariant-abstract/Retype_AI.thy index 76b223589..378afb373 100644 --- a/proof/invariant-abstract/Retype_AI.thy +++ b/proof/invariant-abstract/Retype_AI.thy @@ -43,32 +43,12 @@ lemma upto_enum_inc_1: apply (subgoal_tac "unat (1 +a) = 1 + unat a") apply simp apply (subst unat_plus_simple[THEN iffD1]) - apply (rule word_plus_mono_right2[where b = "2^32 - 2"]) + apply (rule word_plus_mono_right2[where b = "2^word_bits - 2"]) apply (simp add:word_bits_def minus_one_norm)+ apply unat_arith apply simp done -(* FIXME: move *) -lemma monad_eq_split: - assumes "\r s. Q r s \ f r s = f' r s" - "\P\ g \\r s. Q r s\" - "P s" - shows "(g >>= f) s = (g >>= f') s" -proof - - have pre: "\rv s'. \(rv, s') \ fst (g s)\ \ f rv s' = f' rv s'" - using assms unfolding valid_def - by (erule_tac x=s in allE) auto - show ?thesis - apply (simp add: bind_def image_def) - apply (intro conjI) - apply (rule set_eqI) - apply (clarsimp simp: Union_eq) - apply (rule iffI; elim exEI conjE; simp; elim exEI bexEI; clarsimp simp: pre) - apply (rule iffI; cases "snd (g s)"; simp; elim exEI bexEI; clarsimp simp: pre) - done -qed - lemma unat_of_nat_minus_1: "\n < 2^len_of TYPE('a);n\ 0\ \ (unat (((of_nat n):: 'a :: len word) - 1)) = n - 1" apply (subst unat_minus_one) @@ -78,119 +58,6 @@ lemma unat_of_nat_minus_1: apply (simp add:unat_of_nat word_bits_def) done - -definition monad_commute where - "monad_commute P a b \ - (\s. (P s \ ((do x\a;y\b; return (x, y) od) s) = ((do y\b;x\a; return (x, y) od) s)))" - - -lemma monad_eq: - "a s = b s \ (a >>= g) s = (b >>= g) s" - by (auto simp:bind_def) - - -lemma monad_commute_simple: - "\monad_commute P a b;P s\ \ ((do x\a;y\b; g x y od) s) = ((do y\b;x\a; g x y od) s)" - apply (clarsimp simp:monad_commute_def) - apply (drule spec) - apply (erule(1) impE) - apply (drule_tac g = "(\t. g (fst t) (snd t))" in monad_eq) - apply (simp add:bind_assoc) - done - - -lemma commute_commute: - "monad_commute P f h \ monad_commute P h f" - apply (simp (no_asm) add: monad_commute_def) - apply (clarsimp) - apply (erule monad_commute_simple[symmetric]) - apply simp - done - - -lemma assert_commute: "monad_commute (K G) (assert G) f" - by (clarsimp simp:assert_def monad_commute_def) - - -lemma cond_fail_commute: "monad_commute (K (\G)) (when G fail) f" - by (clarsimp simp:when_def fail_def monad_commute_def) - - -lemma return_commute: "monad_commute \ (return a) f" - by (clarsimp simp: return_def bind_def monad_commute_def) - - -lemma monad_commute_guard_imp: - "\monad_commute P f h; \s. Q s \ P s \ \ monad_commute Q f h" - by (clarsimp simp:monad_commute_def) - - -lemma monad_commute_split: - "\\r. monad_commute (Q r) f (g r); monad_commute P f h; - \P'\ h \\r. Q r\\ - \ monad_commute (P and P') f (h>>=g)" - apply (simp (no_asm) add:monad_commute_def) - apply (clarsimp simp:bind_assoc) - apply (subst monad_commute_simple) - apply simp+ - apply (rule_tac Q = "(\x. Q x)" in monad_eq_split) - apply (subst monad_commute_simple[where a = f]) - apply assumption - apply simp+ - done - - -lemma monad_commute_get: - assumes hf: "\P. \P\ f \\r. P\" - and hg: "\P. \P\ g \\r. P\" - and eptyf: "empty_fail f" "empty_fail g" - shows "monad_commute \ f g" -proof - - have fsame: "\a b s. (a,b) \ fst (f s) \ b = s" - by (drule use_valid[OF _ hf],auto) - have gsame: "\a b s. (a,b) \ fst (g s) \ b = s" - by (drule use_valid[OF _ hg],auto) - note ef = empty_fail_not_snd[OF _ eptyf(1)] - note eg = empty_fail_not_snd[OF _ eptyf(2)] - show ?thesis - apply (simp add:monad_commute_def) - apply (clarsimp simp:bind_def split_def return_def) - apply (intro conjI) - apply (rule set_eqI) - apply (rule iffI) - apply (clarsimp simp:Union_eq dest!: singletonD) - apply (frule fsame) - apply clarsimp - apply (frule gsame) - apply (metis fst_conv snd_conv) - apply (clarsimp simp:Union_eq dest!: singletonD) - apply (frule gsame) - apply clarsimp - apply (frule fsame) - apply clarsimp - apply (metis fst_conv snd_conv) - apply (rule iffI) - apply (erule disjE) - apply (clarsimp simp:image_def) - apply (metis fsame) - apply (clarsimp simp:image_def) - apply (drule eg) - apply clarsimp - apply (rule bexI [rotated], assumption) - apply (frule gsame) - apply clarsimp - apply (erule disjE) - apply (clarsimp simp:image_def dest!:gsame) - apply (clarsimp simp:image_def) - apply (drule ef) - apply clarsimp - apply (frule fsame) - apply (erule bexI[rotated]) - apply simp - done -qed - - lemma range_to_bl': "\ is_aligned (ptr :: 'a :: len word) bits; bits < len_of TYPE('a) \ \ {ptr .. ptr + (2 ^ bits) - 1} = {x. take (len_of TYPE('a) - bits) (to_bl x) @@ -507,7 +374,7 @@ lemma word_plus_mono_right_split: apply (auto simp:unat_plus_if_size word_size word_bits_def not_less) done -lemmas word32_plus_mono_right_split = word_plus_mono_right_split[where 'a=32, folded word_bits_def] +lemmas machine_word_plus_mono_right_split = word_plus_mono_right_split[where 'a=machine_word_len, folded word_bits_def] (* range_cover locale: @@ -846,7 +713,7 @@ proof - proof (rule base_member_set) from vp show "is_aligned x (obj_bits ko)" using ps' by (auto elim!: valid_pspaceE pspace_alignedE) - show "obj_bits ko < len_of TYPE(32)" + show "obj_bits ko < len_of TYPE(machine_word_len)" by (rule valid_pspace_obj_sizes [OF _ ranI, unfolded word_bits_def]) fact+ qed @@ -1213,7 +1080,7 @@ lemma retype_region_global_refs_disjoint: apply (rule subsetI, simp only: mask_in_range[symmetric]) apply (clarsimp simp: ptr_add_def) apply (intro conjI) - apply (rule word32_plus_mono_right_split[where sz = sz]) + apply (rule machine_word_plus_mono_right_split[where sz = sz]) apply (erule(1) range_cover.range_cover_compare) apply (simp add:range_cover_def word_bits_def) apply (subst p_assoc_help) @@ -1290,7 +1157,7 @@ crunch cap_refs_in_kernel_window[wp]: do_machine_op "cap_refs_in_kernel_window" locale Retype_AI_post_retype_invs = fixes state_ext_t :: "'state_ext::state_ext itself" and post_retype_invs_check :: "apiobject_type \ bool" - and post_retype_invs :: "apiobject_type \ word32 list \ 'state_ext state \ bool" + and post_retype_invs :: "apiobject_type \ machine_word list \ 'state_ext state \ bool" assumes post_retype_invs_def': "post_retype_invs tp refs \ if post_retype_invs_check tp @@ -1324,13 +1191,13 @@ lemma honestly_16_10: definition - caps_no_overlap :: "word32 \ nat \ 'z::state_ext state \ bool" + caps_no_overlap :: "machine_word \ nat \ 'z::state_ext state \ bool" where "caps_no_overlap ptr sz s \ \cap \ ran (caps_of_state s). untyped_range cap \ {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} \ {} \ {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} \ untyped_range cap" -definition caps_overlap_reserved :: "word32 set \ ('z::state_ext) state \ bool" +definition caps_overlap_reserved :: "machine_word set \ ('z::state_ext) state \ bool" where "caps_overlap_reserved S (s :: ('z::state_ext) state) \ \cap \ ran (caps_of_state s). (is_untyped_cap cap \ usable_untyped_range cap \ S = {})" @@ -1672,11 +1539,11 @@ lemma retype_addrs_obj_range_subset_strong: and not_0:"n\ 0" and tyunt:"ty\ Untyped" note n_less = range_cover.range_cover_n_less[OF cover] - have unat_of_nat_m1: "unat (of_nat n - (1::word32)) < n" + have unat_of_nat_m1: "unat (of_nat n - (1::machine_word)) < n" using not_0 n_less by (simp add:unat_of_nat_minus_1) have decomp:"of_nat n * 2 ^ obj_bits_api ty us = of_nat (n - 1) * 2 ^ (obj_bits (default_object ty dev us)) - + (2 :: word32) ^ obj_bits (default_object ty dev us)" + + (2 :: machine_word) ^ obj_bits (default_object ty dev us)" apply (simp add:distrib_right[where b = "1::'a::len word",simplified,symmetric]) using not_0 n_less apply (simp add: unat_of_nat_minus_1 obj_bits_api_def3 tyunt cong: obj_bits_cong) @@ -1706,8 +1573,8 @@ lemma retype_addrs_obj_range_subset_strong: apply (simp add:unat_of_nat_m1 less_imp_le) using cover apply (simp add:range_cover_def word_bits_def) - apply (rule word32_plus_mono_right_split[where sz = sz]) - using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::word32))"] + apply (rule machine_word_plus_mono_right_split[where sz = sz]) + using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::machine_word))"] apply (clarsimp simp:unat_of_nat_m1) using cover apply (simp add:range_cover_def word_bits_def) @@ -1800,7 +1667,7 @@ lemma usable_range_subseteq: lemma usable_range_emptyD: "\cap_aligned cap;is_untyped_cap cap ;usable_untyped_range cap = {}\ \ 2 ^ cap_bits cap \ free_index_of cap" apply (clarsimp simp:is_cap_simps not_le free_index_of_def cap_aligned_def split:if_splits) - apply (drule(1) of_nat_less_pow_32) + apply (drule(1) of_nat_power [where 'a=machine_word_len, folded word_bits_def]) apply (drule word_plus_mono_right[OF _ is_aligned_no_overflow[unfolded p_assoc_help],rotated]) apply simp apply (simp add:p_assoc_help) @@ -2224,7 +2091,7 @@ lemma p_in_obj_range: apply (drule valid_obj_sizes, erule ranI) apply (simp add: obj_range_def add_diff_eq[symmetric]) apply (erule is_aligned_no_wrap') - apply (erule word_power_less_1[where 'a=32, folded word_bits_def]) + apply (erule word_power_less_1[where 'a=machine_word_len, folded word_bits_def]) done lemma p_in_obj_range_internal: @@ -2288,8 +2155,8 @@ locale retype_region_proofs_invs + Retype_AI_post_retype_invs "TYPE('state_ext)" post_retype_invs_check post_retype_invs for s :: "'state_ext :: state_ext state" and ty us ptr sz n ps s' dev post_retype_invs_check - and post_retype_invs :: "apiobject_type \ word32 list \ 'state_ext state \ bool" + - fixes region_in_kernel_window :: "word32 set \ 'state_ext state \ bool" + and post_retype_invs :: "apiobject_type \ machine_word list \ 'state_ext state \ bool" + + fixes region_in_kernel_window :: "machine_word set \ 'state_ext state \ bool" assumes valid_global_refs: "valid_global_refs s \ valid_global_refs s'" assumes valid_arch_state: "valid_arch_state s \ valid_arch_state s'" assumes valid_arch_objs': "valid_arch_objs s \ valid_arch_objs s'" @@ -2342,11 +2209,11 @@ locale Retype_AI + Retype_AI_dmo_eq_kernel_restricted state_ext_t machine_op_t for state_ext_t :: "'state_ext::state_ext itself" and post_retype_invs_check - and post_retype_invs :: "apiobject_type \ word32 list \ 'state_ext state \ bool" + and post_retype_invs :: "apiobject_type \ machine_word list \ 'state_ext state \ bool" and no_gs_types and machine_op_t :: "'machine_op_t itself" + fixes state_ext'_t :: "'state_ext'::state_ext itself" - fixes region_in_kernel_window :: "word32 set \ 'state_ext state \ bool" + fixes region_in_kernel_window :: "machine_word set \ 'state_ext state \ bool" assumes invs_post_retype_invs: "\(s::'state_ext state) ty refs. invs s \ post_retype_invs ty refs s" assumes equal_kernel_mappings_trans_state[simp]: diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index 885aedc47..16fe1a04a 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -522,29 +522,22 @@ lemma sts_mcpriority_tcb_at_ct[wp]: apply clarsimp done - + +lemma sts_tcb_inv_wf [wp]: + "\tcb_inv_wf i\ set_thread_state t st \\rv. tcb_inv_wf i\" + apply (case_tac i) + apply (wp set_thread_state_valid_cap hoare_vcg_all_lift hoare_vcg_const_imp_lift + | simp add: tcb_at_typ split: option.split + | safe + | wp sts_obj_at_impossible)+ + done + lemma sts_valid_inv[wp]: "\valid_invocation i\ set_thread_state t st \\rv. valid_invocation i\" - apply (case_tac i, simp_all add: ntfn_at_typ ep_at_typ - sts_valid_untyped_inv sts_valid_arch_inv) - apply (wp | simp)+ - apply (rename_tac tcb_invocation) - apply (case_tac tcb_invocation, - (wp set_thread_state_valid_cap hoare_vcg_all_lift hoare_vcg_const_imp_lift| - simp add: tcb_at_typ split: option.split| - safe | - wp sts_obj_at_impossible )+) - apply (rename_tac cnode_invocation) - apply (case_tac cnode_invocation, simp_all)[1] - apply (case_tac cnode_invocation, - (wp set_thread_state_valid_cap sts_nasty_bit hoare_vcg_const_imp_lift - | simp)+) - apply (rename_tac irq_control_invocation) - apply (case_tac irq_control_invocation; wpsimp) - apply (rename_tac irq_handler_invocation) - apply (case_tac irq_handler_invocation; - wpsimp wp: ex_cte_cap_to_pres hoare_vcg_ex_lift set_thread_state_valid_cap) - done + by (cases i; wpsimp simp: sts_valid_untyped_inv sts_valid_arch_inv; + rename_tac i'; case_tac i'; simp; + wpsimp wp: set_thread_state_valid_cap sts_nasty_bit + hoare_vcg_const_imp_lift hoare_vcg_ex_lift) lemma sts_Restart_stay_simple: @@ -766,7 +759,7 @@ proof (induct param rule: resolve_address_bits'.induct) apply (elim conjE exE disjE) apply ((clarsimp simp: whenE_def bindE_def bind_def lift_def liftE_def throwError_def returnOk_def return_def valid_fault_def - valid_cap_def2 wellformed_cap_def + valid_cap_def2 wellformed_cap_def word_bits_def split: if_split_asm cap.splits)+)[4] apply (split if_split_asm) apply (clarsimp simp: whenE_def bindE_def bind_def lift_def liftE_def diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index 1339b993d..e05887078 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -590,7 +590,6 @@ lemma out_no_cap_to_trivial: apply (wpsimp wp: hoare_vcg_const_Ball_lift out_cte_wp_at_trivialT) done -(* FIXME: eliminate *) lemmas thread_set_no_cap_to_trivial = thread_set_no_cap_obj_ref_trivial @@ -865,11 +864,6 @@ lemma (in Tcb_AI) tcbinv_invs: apply clarsimp done -crunch typ_at[wp]: invoke_tcb "\s. P (typ_at T p s)" - (ignore: check_cap_at setNextPC zipWithM - wp: hoare_drop_imps mapM_x_wp' check_cap_inv - simp: crunch_simps) - lemma inj_ucast: "\ uc = ucast; is_up uc \ \ inj uc" apply simp apply (rule inj_on_inverseI) @@ -1015,7 +1009,7 @@ where primrec - thread_control_target :: "tcb_invocation \ word32" + thread_control_target :: "tcb_invocation \ machine_word" where "thread_control_target (tcb_invocation.ThreadControl a b c d e f g h) = a" diff --git a/proof/invariant-abstract/Untyped_AI.thy b/proof/invariant-abstract/Untyped_AI.thy index c5a9fab55..63f20fa12 100644 --- a/proof/invariant-abstract/Untyped_AI.thy +++ b/proof/invariant-abstract/Untyped_AI.thy @@ -19,6 +19,8 @@ context begin interpretation Arch . requalify_consts region_in_kernel_window + arch_default_cap + second_level_tables end primrec @@ -61,7 +63,7 @@ locale Untyped_AI_of_bl_nat_to_cref = lemma cnode_cap_bits_range: "\ cte_wp_at P p s; invs s \ \ (\c. P c \ (is_cnode_cap c \ - (\n. n > 0 \ n < 28 \ is_aligned (obj_ref_of c) (n + 4)) (bits_of c)))" + (\n. n > 0 \ n < (word_bits - 4) \ is_aligned (obj_ref_of c) (n + 4)) (bits_of c)))" apply (frule invs_valid_objs) apply (drule(1) cte_wp_at_valid_objs_valid_cap) apply clarsimp @@ -283,7 +285,7 @@ locale Untyped_AI_arch = "\ptr sz s x6 us n dev. \pspace_no_overlap_range_cover ptr sz (s::'state_ext state) \ x6 \ ASIDPoolObj \ range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \ ptr \ 0(*; tp = ArchObject x6*)\ \ \y\{0..kheap := foldr (\p kh. kh(p \ default_object (ArchObject x6) dev us)) (map (\p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0.. \ ArchObjectCap (ARM_A.arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)" + (kheap s)\ \ ArchObjectCap (arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)" assumes init_arch_objects_descendants_range[wp]: "\x cref ty ptr n us y. \\(s::'state_ext state). descendants_range x cref s \ init_arch_objects ty ptr n us y @@ -373,20 +375,23 @@ qed lemma range_cover_stuff: - "\0 < n;n \ unat ((2::word32) ^ sz - of_nat rv >> bits); + notes unat_power_lower_machine = unat_power_lower[where 'a=machine_word_len] + notes unat_of_nat_machine = unat_of_nat_eq[where 'a=machine_word_len] + shows + "\0 < n;n \ unat ((2::machine_word) ^ sz - of_nat rv >> bits); rv \ 2^ sz; sz < word_bits; is_aligned w sz\ \ rv \ unat (alignUp (w + of_nat rv) bits - w) \ (alignUp (w + of_nat rv) bits) && ~~ mask sz = w \ - range_cover (alignUp (w + ((of_nat rv)::word32)) bits) sz bits n" + range_cover (alignUp (w + ((of_nat rv)::machine_word)) bits) sz bits n" apply (clarsimp simp: range_cover_def) proof (intro conjI) assume not_0 : "0 unat ((2::word32) ^ sz - of_nat rv >> bits)" "rv\ 2^sz" + assume bound : "n \ unat ((2::machine_word) ^ sz - of_nat rv >> bits)" "rv\ 2^sz" "sz < word_bits" assume al: "is_aligned w sz" - have space: "(2::word32) ^ sz - of_nat rv \ 2^ sz" + have space: "(2::machine_word) ^ sz - of_nat rv \ 2^ sz" apply (rule word_sub_le[OF word_of_nat_le]) - apply (clarsimp simp: bound unat_power_lower32) + apply (clarsimp simp: bound unat_power_lower_machine) done show cmp: "bits \ sz" using not_0 bound @@ -396,7 +401,7 @@ lemma range_cover_stuff: apply (drule le_trans) apply (rule word_le_nat_alt[THEN iffD1]) apply (rule le_shiftr[OF space]) - apply (subgoal_tac "(2::word32)^sz >> bits = 0") + apply (subgoal_tac "(2::machine_word)^sz >> bits = 0") apply simp apply (rule and_mask_eq_iff_shiftr_0[THEN iffD1]) apply (simp add: and_mask_eq_iff_le_mask) @@ -404,18 +409,18 @@ lemma range_cover_stuff: apply (simp add: word_bits_def mask_def power_overflow) apply (subst le_mask_iff_lt_2n[THEN iffD1]) apply (simp add: word_bits_def) - apply (simp add: word_less_nat_alt[THEN iffD2] unat_power_lower32) + apply (simp add: word_less_nat_alt[THEN iffD2] unat_power_lower_machine) done - have shiftr_t2n[simp]:"(2::word32)^sz >> bits = 2^ (sz - bits)" + have shiftr_t2n[simp]:"(2::machine_word)^sz >> bits = 2^ (sz - bits)" using bound cmp apply (case_tac "sz = 0",simp) - apply (subgoal_tac "(1::word32) << sz >> bits = 2^ (sz -bits)") + apply (subgoal_tac "(1::machine_word) << sz >> bits = 2^ (sz -bits)") apply simp apply (subst shiftl_shiftr1) apply (simp add: word_size word_bits_def shiftl_t2n word_1_and_bl)+ done - have cmp2[simp]: "alignUp (of_nat rv) bits < (2 :: word32) ^ sz" + have cmp2[simp]: "alignUp (of_nat rv) bits < (2 :: machine_word) ^ sz" using bound cmp not_0 apply - apply (case_tac "rv = 0") @@ -423,7 +428,7 @@ lemma range_cover_stuff: apply (clarsimp simp: alignUp_def2) apply (subst mask_eq_x_eq_0[THEN iffD1]) apply (simp add: and_mask_eq_iff_le_mask mask_def) - apply (simp add: p2_gt_0[where 'a=32, folded word_bits_def]) + apply (simp add: p2_gt_0[where 'a=machine_word_len, folded word_bits_def]) apply (simp add: alignUp_def3) apply (subgoal_tac "1 \ unat (2 ^ sz - of_nat rv >> bits)") prefer 2 @@ -433,7 +438,7 @@ lemma range_cover_stuff: apply (simp add: shiftr_div_2n') apply (simp add: td_gal[symmetric]) apply (subst (asm) unat_sub) - apply (simp add: word_of_nat_le unat_power_lower32) + apply (simp add: word_of_nat_le unat_power_lower_machine) apply (simp add: le_diff_conv2 word_of_nat_le unat_le_helper word_less_nat_alt) apply (rule le_less_trans[OF unat_plus_gt]) apply (rule less_le_trans[where y = "2^bits + unat (of_nat rv)"]) @@ -448,7 +453,7 @@ lemma range_cover_stuff: apply simp done - show "n + unat (alignUp (w + ((of_nat rv)::word32)) bits && mask sz >> bits) \ 2 ^ (sz - bits)" + show "n + unat (alignUp (w + ((of_nat rv)::machine_word)) bits && mask sz >> bits) \ 2 ^ (sz - bits)" using not_0 bound cmp apply - apply (erule le_trans[OF add_le_mono]) @@ -493,37 +498,42 @@ lemma range_cover_stuff: apply (case_tac "rv = 0") apply simp apply (rule le_trans[OF _ word_le_nat_alt[THEN iffD1,OF alignUp_ge]]) - apply (subst unat_of_nat32) - apply (erule le_less_trans) - apply simp - apply (simp_all add: word_bits_def)[2] + apply (subst unat_of_nat_machine) + apply (erule le_less_trans) + apply (rule power_strict_increasing) + apply (simp_all add: word_bits_def)[4] apply (rule alignUp_is_aligned_nz[where x = "2^sz"]) - apply (rule is_aligned_weaken[OF is_aligned_triv2]) - apply (simp_all add: word_bits_def)[2] - apply (subst word_of_nat_le) - apply (subst unat_power_lower32) - apply simp+ - apply (erule of_nat_neq_0) - apply (erule le_less_trans) - apply (subst word_bits_def[symmetric]) - apply simp - done + apply (rule is_aligned_weaken[OF is_aligned_triv2]) + apply (simp_all add: word_bits_def)[2] + apply (subst word_of_nat_le) + apply (subst unat_power_lower_machine) + apply (simp add: word_bits_def)+ + apply (erule of_nat_neq_0) + apply (erule le_less_trans) + apply (rule power_strict_increasing) + apply (simp add: word_bits_def)+ + done show "alignUp (w + of_nat rv) bits && ~~ mask sz = w" using bound not_0 cmp al apply (clarsimp simp: alignUp_plus[OF is_aligned_weaken] mask_out_add_aligned[symmetric]) apply (clarsimp simp: and_not_mask) - apply (subgoal_tac "alignUp ((of_nat rv)::word32) bits >> sz = 0") + apply (subgoal_tac "alignUp ((of_nat rv)::machine_word) bits >> sz = 0") apply simp apply (simp add: le_mask_iff[symmetric] mask_def) done - show "sz < 32" by (simp add: bound(3)[unfolded word_bits_def, simplified]) - qed + qed (simp add: word_bits_def) + +context Arch begin + (*FIXME: generify proof that uses this *) + lemmas range_cover_stuff_arch = range_cover_stuff[unfolded word_bits_def, simplified] +end + lemma cte_wp_at_range_cover: "\bits < word_bits; rv\ 2^ sz; invs s; cte_wp_at (op = (cap.UntypedCap dev w sz idx)) p s; - 0 < n; n \ unat ((2::word32) ^ sz - of_nat rv >> bits)\ + 0 < n; n \ unat ((2::machine_word) ^ sz - of_nat rv >> bits)\ \ range_cover (alignUp (w + of_nat rv) bits) sz bits n" apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule(1) caps_of_state_valid) @@ -535,7 +545,7 @@ lemma cte_wp_at_range_cover: lemma le_mask_le_2p: - "\idx \ unat ((ptr::word32) && mask sz);sz < word_bits\ \ idx < 2^ sz" + "\idx \ unat ((ptr::machine_word) && mask sz);sz < word_bits\ \ idx < 2^ sz" apply (erule le_less_trans) apply (rule unat_less_helper) apply simp @@ -666,18 +676,18 @@ lemma cases_imp_eq: by blast lemma inj_16: - "\ of_nat x * 16 = of_nat y * (16 :: word32); + "\ of_nat x * 16 = of_nat y * (16 :: machine_word); x < bnd; y < bnd; bnd \ 2 ^ (word_bits - 4) \ - \ of_nat x = (of_nat y :: word32)" + \ of_nat x = (of_nat y :: machine_word)" apply (fold shiftl_t2n [where n=4, simplified, simplified mult.commute]) apply (simp only: word_bl.Rep_inject[symmetric] bl_shiftl) apply (drule(1) order_less_le_trans)+ - apply (drule of_nat_mono_maybe[rotated, where 'a=32]) + apply (drule of_nat_mono_maybe[rotated, where 'a=machine_word_len]) apply (rule power_strict_increasing) apply (simp add: word_bits_def) apply simp - apply (drule of_nat_mono_maybe[rotated, where 'a=32]) + apply (drule of_nat_mono_maybe[rotated, where 'a=machine_word_len]) apply (rule power_strict_increasing) apply (simp add: word_bits_def) apply simp @@ -689,12 +699,15 @@ lemma inj_16: lemma of_nat_shiftR: "a < 2 ^ word_bits \ - unat (of_nat (shiftR a b)::word32) = unat ((of_nat a :: word32) >> b)" + unat (of_nat (shiftR a b)::machine_word) = unat ((of_nat a :: machine_word) >> b)" apply (subst shiftr_div_2n') apply (clarsimp simp: shiftR_nat) - apply (subst unat_of_nat32) + apply (subst unat_of_nat_eq[where 'a=machine_word_len]) + apply (simp only: word_bits_def) apply (erule le_less_trans[OF div_le_dividend]) - apply (simp add: unat_of_nat32) + apply (subst unat_of_nat_eq[where 'a=machine_word_len]) + apply (simp only: word_bits_def) + apply simp done @@ -1437,17 +1450,17 @@ lemma of_nat_shift_distinct_helper: done -lemmas of_nat_shift_distinct_helper32 = of_nat_shift_distinct_helper[where 'a=32, folded word_bits_def] +lemmas of_nat_shift_distinct_helper_machine = of_nat_shift_distinct_helper[where 'a=machine_word_len, folded word_bits_def] lemma ptr_add_distinct_helper: - "\ ptr_add (p :: word32) (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x \ y; + "\ ptr_add (p :: machine_word) (x * 2 ^ n) = ptr_add p (y * 2 ^ n); x \ y; x < bnd; y < bnd; n < word_bits; bnd \ 2 ^ (word_bits - n) \ \ P" apply (clarsimp simp: ptr_add_def word_unat_power[symmetric] shiftl_t2n[symmetric, simplified mult.commute]) - apply (erule(5) of_nat_shift_distinct_helper32) + apply (erule(5) of_nat_shift_distinct_helper_machine) done @@ -1608,12 +1621,12 @@ lemma retype_region_distinct_sets: apply (clarsimp simp: retype_addrs_def distinct_prop_map) apply (rule distinct_prop_distinct) apply simp - apply (subgoal_tac "of_nat y * (2::word32) ^ obj_bits_api tp us \ of_nat x * 2 ^ obj_bits_api tp us") + apply (subgoal_tac "of_nat y * (2::machine_word) ^ obj_bits_api tp us \ of_nat x * 2 ^ obj_bits_api tp us") apply (case_tac tp) defer apply (simp add:cap_range_def ptr_add_def)+ apply (clarsimp simp: ptr_add_def word_unat_power[symmetric] shiftl_t2n[simplified mult.commute, symmetric]) - apply (erule(2) of_nat_shift_distinct_helper[where 'a=32 and n = "obj_bits_api tp us"]) + apply (erule(2) of_nat_shift_distinct_helper[where 'a=machine_word_len and n = "obj_bits_api tp us"]) apply simp apply (simp add:range_cover_def) apply (erule range_cover.range_cover_n_le) @@ -2035,10 +2048,10 @@ lemma op_equal: "(\x. x = c) = (op = c)" by (rule ext) auto lemma mask_out_eq_0: - "\idx < 2^ sz;sz \ ((of_nat idx)::word32) && ~~ mask sz = 0" + "\idx < 2^ sz;sz \ ((of_nat idx)::machine_word) && ~~ mask sz = 0" apply (clarsimp simp: mask_out_sub_mask) apply (subst less_mask_eq[symmetric]) - apply (erule(1) of_nat_less_pow_32) + apply (erule(1) of_nat_power[where 'a=machine_word_len, folded word_bits_def]) apply simp done @@ -2063,7 +2076,7 @@ lemma is_aligned_neg_mask_eq': (* FIXME: move *) lemma neg_mask_mask_unat: "sz < word_bits \ - unat ((ptr::word32) && ~~ mask sz) + unat (ptr && mask sz) = unat ptr" + unat ((ptr::machine_word) && ~~ mask sz) + unat (ptr && mask sz) = unat ptr" apply (subst unat_plus_simple[THEN iffD1,symmetric]) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask[OF le_refl]]) apply (rule and_mask_less') @@ -2293,7 +2306,7 @@ proof - apply - apply (erule disjE) apply (erule cte_wp_at_caps_descendants_range_inI[OF _ _ _ range_cover.sz(1) - [where 'a=32, folded word_bits_def]]) + [where 'a=machine_word_len, folded word_bits_def]]) apply (simp add:cte_wp_at_caps_of_state desc_range)+ done thus "descendants_range_in usable_range cref s" @@ -2313,7 +2326,7 @@ lemma ps_no_overlap[simp]: "\ reset \ pspace_no_overlap_ran using misc cte_wp_at cover idx_cases apply clarsimp apply (erule cte_wp_at_pspace_no_overlapI[OF _ _ _ - range_cover.sz(1)[where 'a=32, folded word_bits_def]]) + range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]]) apply (simp add: cte_wp_at_caps_of_state) apply simp+ done @@ -2323,7 +2336,7 @@ lemma caps_no_overlap[simp]: "caps_no_overlap ptr sz s" apply - apply (erule disjE) apply (erule cte_wp_at_caps_no_overlapI[OF _ _ _ range_cover.sz(1) - [where 'a=32, folded word_bits_def]]) + [where 'a=machine_word_len, folded word_bits_def]]) apply (simp add:cte_wp_at_caps_of_state)+ apply (erule descendants_range_caps_no_overlapI) apply (simp add:cte_wp_at_caps_of_state desc_range)+ @@ -2388,14 +2401,14 @@ lemma usable_range_disjoint: {ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {}" proof - have idx_compare''[simp]: - "unat ((ptr && mask sz) + (of_nat (length slots) * (2::word32) ^ obj_bits_api tp us)) < 2 ^ sz + "unat ((ptr && mask sz) + (of_nat (length slots) * (2::machine_word) ^ obj_bits_api tp us)) < 2 ^ sz \ ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us" apply (rule minus_one_helper,simp) apply (rule neq_0_no_wrap) - apply (rule word32_plus_mono_right_split) + apply (rule machine_word_plus_mono_right_split) apply (simp add:shiftl_t2n range_cover_unat[OF cover] field_simps) - apply (simp add:range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+ + apply (simp add:range_cover.sz[where 'a=machine_word_len, folded word_bits_def, OF cover])+ done show ?thesis apply (clarsimp simp:mask_out_sub_mask blah) @@ -2499,14 +2512,14 @@ lemma valid_untyped_cap_inc: apply simp apply (erule disjoint_subset[rotated]) apply (frule(1) le_mask_le_2p[OF _ - range_cover.sz(1)[where 'a=32, folded word_bits_def]]) + range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]]) apply clarsimp apply (rule word_plus_mono_right) apply (rule word_of_nat_le) - apply (simp add: unat_of_nat32 range_cover_unat field_simps) + apply (simp add: unat_of_nat_eq[where 'a=machine_word_len] range_cover_unat field_simps) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask[OF le_refl]]) apply (simp add: word_less_nat_alt - unat_power_lower[where 'a=32, folded word_bits_def]) + unat_power_lower[where 'a=machine_word_len, folded word_bits_def]) apply (simp add: range_cover_unat range_cover.unat_of_nat_shift shiftl_t2n field_simps) apply (subst add.commute) apply (simp add: range_cover.range_cover_compare_bound) @@ -3081,16 +3094,15 @@ lemma create_cap_irq_handlers[wp]: crunch valid_arch_objs[wp]: create_cap "valid_arch_objs" (simp: crunch_simps) - locale Untyped_AI_nonempty_table = fixes state_ext_t :: "('state_ext::state_ext) itself" - fixes nonempty_table :: "word32 set \ Structures_A.kernel_object \ bool" + fixes nonempty_table :: "machine_word set \ Structures_A.kernel_object \ bool" assumes create_cap_valid_arch_caps[wp]: "\tp oref sz dev cref p.\valid_arch_caps and valid_cap (default_cap tp oref sz dev) and (\(s::'state_ext state). \r\obj_refs (default_cap tp oref sz dev). (\p'. \ cte_wp_at (\cap. r \ obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) and cte_wp_at (op = cap.NullCap) cref and K (tp \ ArchObject ASIDPoolObj)\ create_cap tp sz p dev (cref, oref) \\rv. valid_arch_caps\" @@ -3102,11 +3114,11 @@ locale Untyped_AI_nonempty_table = assumes nonempty_table_caps_of: "\S ko. nonempty_table S ko \ caps_of ko = {}" assumes init_arch_objects_nonempty_table: - "\(\s. \ (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + "\(\s. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ valid_global_objs s \ valid_arch_state s \ pspace_aligned s) and K (\ref\set refs. is_aligned ref (obj_bits_api tp us))\ init_arch_objects tp ptr bits us refs - \\rv. \s :: 'state_ext state. \ (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)\" + \\rv. \s :: 'state_ext state. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\" crunch valid_global_objs[wp]: create_cap "valid_global_objs" (simp: crunch_simps) @@ -3182,7 +3194,7 @@ lemma (in Untyped_AI_nonempty_table) create_cap_invs[wp]: and real_cte_at cref and (\(s::'state_ext state). \r\obj_refs (default_cap tp oref sz dev). (\p'. \ cte_wp_at (\cap. r \ obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) and K (p \ cref \ tp \ ArchObject ASIDPoolObj)\ create_cap tp sz p dev (cref, oref) \\rv. invs\" apply (rule hoare_pre) @@ -3213,9 +3225,9 @@ lemma create_cap_no_cap[wp]: unfolding create_cap_def cte_wp_at_caps_of_state by wpsimp lemma (in Untyped_AI_nonempty_table) create_cap_nonempty_tables[wp]: - "\\s. P (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) p s)\ + "\\s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\ create_cap tp sz p' dev (cref, oref) - \\rv s. P (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) p s)\" + \\rv s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\" apply (rule hoare_pre) apply (rule hoare_use_eq [where f=arch_state, OF create_cap_arch_state]) apply (simp add: create_cap_def set_cdt_def) @@ -3265,7 +3277,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs_inv: real_cte_at (fst tup) s) \ (\tup \ set ((cref,oref)#list). \r \ obj_refs (default_cap tp (snd tup) sz dev). (\p'. \ cte_wp_at (\cap. r \ Structures_A.obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ distinct (p # (map fst ((cref,oref)#list))) \ tp \ ArchObject ASIDPoolObj) \ create_cap tp sz p dev (cref,oref) @@ -3290,7 +3302,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs_inv: real_cte_at (fst tup) s) \ (\tup \ set list. \r \ obj_refs (default_cap tp (snd tup) sz dev). (\p'. \ cte_wp_at (\cap. r \ Structures_A.obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ distinct (p # (map fst list)) \ tp \ ArchObject ASIDPoolObj) \" apply (rule hoare_pre) @@ -3342,7 +3354,7 @@ lemma (in Untyped_AI_nonempty_table) create_caps_invs: real_cte_at (fst tup) s) \ (\tup \ set (zip crefs orefs). \r \ obj_refs (default_cap tp (snd tup) sz dev). (\p'. \ cte_wp_at (\cap. r \ Structures_A.obj_refs cap) p' s) - \ \ obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s) + \ \ obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ distinct (p # (map fst (zip crefs orefs))) \ tp \ ArchObject ASIDPoolObj) and K (set orefs \ set (retype_addrs ptr tp (length slots) us))\ @@ -3441,7 +3453,7 @@ lemma retype_region_refs_distinct[wp]: | drule subsetD [OF obj_refs_default_cap] less_two_pow_divD)+ apply (simp add: range_cover_def word_bits_def) - apply (erule range_cover.range_cover_n_le[where 'a=32, folded word_bits_def]) + apply (erule range_cover.range_cover_n_le[where 'a=machine_word_len, folded word_bits_def]) done @@ -3496,9 +3508,9 @@ lemma do_machine_op_obj_at_arch_state[wp]: by (clarsimp simp: do_machine_op_def split_def | wp)+ lemma (in Untyped_AI_nonempty_table) retype_nonempty_table[wp]: - "\\(s::('state_ext::state_ext) state). \ (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)\ + "\\(s::('state_ext::state_ext) state). \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\ retype_region ptr sz us tp dev - \\rv s. \ (obj_at (nonempty_table (set (arch_state.arm_global_pts (arch_state s)))) r s)\" + \\rv s. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\" apply (simp add: retype_region_def split del: if_split) apply (rule hoare_pre) apply (wp|simp del: fun_upd_apply)+ @@ -3528,9 +3540,9 @@ lemma invs_cap_refs_in_kernel_window[elim!]: by (simp add: invs_def valid_state_def) lemma (in Untyped_AI_nonempty_table) set_cap_nonempty_tables[wp]: - "\\s. P (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) p s)\ + "\\s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\ set_cap cap cref - \\rv s. P (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) p s)\" + \\rv s. P (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) p s)\" apply (rule hoare_pre) apply (rule hoare_use_eq [where f=arch_state, OF set_cap_arch]) apply (wp set_cap_obj_at_impossible) diff --git a/proof/refine/ADT_H.thy b/proof/refine/ADT_H.thy index fd13c6737..cc7a0335d 100644 --- a/proof/refine/ADT_H.thy +++ b/proof/refine/ADT_H.thy @@ -346,7 +346,7 @@ lemma cap_relation_imp_CapabilityMap: apply (rule set_eqI, clarsimp) apply (case_tac "x", simp_all) apply (rule set_eqI, clarsimp) - apply (case_tac "x", simp_all) + apply (case_tac "x", simp_all add: word_bits_def) apply (simp add: uint_of_bl_is_bl_to_bin bl_bin_bl[simplified]) apply (simp add: zbits_map_def split: option.splits) apply (rename_tac arch_cap) diff --git a/proof/refine/Detype_R.thy b/proof/refine/Detype_R.thy index 55f5b5cbe..7bca93983 100644 --- a/proof/refine/Detype_R.thy +++ b/proof/refine/Detype_R.thy @@ -846,16 +846,16 @@ lemma valid_cap_ctes_pre: | _ \ True" apply (drule valid_capAligned) apply (simp split: capability.split zombie_type.split arch_capability.split, safe) - apply (clarsimp simp add: capRange_def capAligned_def objBits_simps pre_helper field_simps - simp del: atLeastAtMost_iff) + using pre_helper[where a=4] + apply (clarsimp simp add: capRange_def capAligned_def objBits_simps field_simps) apply (clarsimp simp add: capRange_def capAligned_def simp del: atLeastAtMost_iff capBits.simps) apply (rule pre_helper2, simp_all)[1] apply (clarsimp simp add: capRange_def capAligned_def simp del: atLeastAtMost_iff capBits.simps) apply (rule pre_helper2, simp_all)[1] - apply (clarsimp simp add: capRange_def capAligned_def objBits_simps pre_helper field_simps - simp del: atLeastAtMost_iff) + using pre_helper[where a=4] + apply (clarsimp simp add: capRange_def capAligned_def objBits_simps field_simps) done lemma replycap_argument: @@ -1643,8 +1643,8 @@ proof - apply (clarsimp simp add: deleteObjects_def2) apply (simp add: freeMemory_def bind_assoc doMachineOp_bind ef_storeWord) apply (simp add: bind_assoc[where f="\_. modify f" for f, symmetric]) - apply (simp add: word_size_def mapM_x_storeWord_step doMachineOp_modify - modify_modify) + apply (simp add: mapM_x_storeWord_step[simplified word_size_bits_def] + doMachineOp_modify modify_modify) apply (simp add: bind_assoc intvl_range_conv'[where 'a=32, folded word_bits_def] mask_def field_simps) apply (wp) apply (simp cong: if_cong) diff --git a/proof/refine/Include.thy b/proof/refine/Include.thy index cac06b727..fc526866e 100644 --- a/proof/refine/Include.thy +++ b/proof/refine/Include.thy @@ -12,7 +12,7 @@ theory Include imports "../../spec/abstract/Syscall_A" "../../spec/design/API_H" - "../../spec/design/$L4V_ARCH/Intermediate_H" + "../../spec/design/$L4V_ARCH/ArchIntermediate_H" begin no_notation bind_drop (infixl ">>" 60) diff --git a/proof/refine/Retype_R.thy b/proof/refine/Retype_R.thy index f0864abac..d17e3b63c 100644 --- a/proof/refine/Retype_R.thy +++ b/proof/refine/Retype_R.thy @@ -836,7 +836,7 @@ lemma new_cap_addrs_subset: dest!: less_two_pow_divD) apply (intro conjI) apply (insert range_cover) - apply (rule word32_plus_mono_right_split[OF range_cover.range_cover_compare]) + apply (rule machine_word_plus_mono_right_split[OF range_cover.range_cover_compare]) apply assumption apply simp apply (simp add:range_cover_def word_bits_def) @@ -3216,7 +3216,7 @@ lemma obj_range'_subset_strong: apply (simp add:unat_of_nat_m1 less_imp_le) using cover apply (simp add:range_cover_def word_bits_def) - apply (rule word32_plus_mono_right_split[where sz = sz]) + apply (rule machine_word_plus_mono_right_split[where sz = sz]) using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::word32))"] apply (clarsimp simp:unat_of_nat_m1) using cover @@ -3646,7 +3646,7 @@ proof - apply unat_arith using upbound apply (simp add:word_bits_def) - apply (rule word32_plus_mono_right_split[where sz = sz]) + apply (rule machine_word_plus_mono_right_split[where sz = sz]) apply (rule less_le_trans[rotated -1]) apply (rule range_cover.range_cover_compare_bound[OF cover']) apply (simp add: unat_minus_one[OF not_0']) diff --git a/proof/refine/Syscall_R.thy b/proof/refine/Syscall_R.thy index 8f6573a6c..675edec51 100644 --- a/proof/refine/Syscall_R.thy +++ b/proof/refine/Syscall_R.thy @@ -202,7 +202,7 @@ lemma decode_invocation_corres: apply (rule corres_guard_imp) apply (rule_tac F="length list \ 32" in corres_gen_asm) apply (rule dec_cnode_inv_corres, simp+) - apply (simp add: valid_cap_def) + apply (simp add: valid_cap_def word_bits_def) apply simp -- "ThreadCap" apply (simp add: isCap_defs Let_def CanModify_def diff --git a/proof/refine/Untyped_R.thy b/proof/refine/Untyped_R.thy index 1f4cddfa5..5dba77aba 100644 --- a/proof/refine/Untyped_R.thy +++ b/proof/refine/Untyped_R.thy @@ -3253,7 +3253,7 @@ lemma createNewCaps_range_helper2: apply (fastforce simp:range_cover_def) apply simp apply (rule range_subsetI) - apply (rule word32_plus_mono_right_split[OF range_cover.range_cover_compare]) + apply (rule machine_word_plus_mono_right_split[OF range_cover.range_cover_compare]) apply (assumption)+ apply (simp add:range_cover_def word_bits_def) apply (frule range_cover_cell_subset) @@ -4477,7 +4477,7 @@ lemma caps_no_overlap'[simp]: "caps_no_overlap'' ptr sz s" < ptr + of_nat (length slots) * 2 ^ APIType_capBits tp us" apply (rule minus_one_helper,simp) apply (rule neq_0_no_wrap) - apply (rule word32_plus_mono_right_split) + apply (rule machine_word_plus_mono_right_split) apply (simp add: shiftl_t2n range_cover_unat[OF cover] field_simps) apply (simp add: range_cover.sz(1) [where 'a=32, folded word_bits_def, OF cover])+ @@ -5273,11 +5273,8 @@ let ?ui' = "Invocations_H.untyped_invocation.Retype (cte_map cref) reset using cover apply (clarsimp simp:delete_objects_def freeMemory_def word_size_def) apply (subgoal_tac "is_aligned (ptr &&~~ mask sz) sz") - apply (subst mapM_storeWord_clear_um) - apply (simp) - apply simp - apply (simp add:range_cover_def word_bits_def) - apply clarsimp + apply (subst mapM_storeWord_clear_um[simplified word_size_def word_size_bits_def]; + clarsimp simp: range_cover_def word_bits_def) apply (rule is_aligned_neg_mask) apply simp done @@ -5351,7 +5348,7 @@ let ?ui' = "Invocations_H.untyped_invocation.Retype (cte_map cref) reset < ptr + of_nat (length slots) * 2 ^ obj_bits_api (APIType_map2 (Inr ao')) us" apply (rule minus_one_helper,simp) apply (rule neq_0_no_wrap) - apply (rule word32_plus_mono_right_split) + apply (rule machine_word_plus_mono_right_split) apply (simp add:shiftl_t2n range_cover_unat[OF cover] field_simps) apply (simp add:range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+ done @@ -5366,7 +5363,7 @@ let ?ui' = "Invocations_H.untyped_invocation.Retype (cte_map cref) reset apply (rule minus_one_helper,simp) apply (simp add:is_aligned_neg_mask_eq'[symmetric]) apply (rule neq_0_no_wrap) - apply (rule word32_plus_mono_right_split[where sz = sz]) + apply (rule machine_word_plus_mono_right_split[where sz = sz]) apply (simp add:is_aligned_mask)+ apply (simp add:range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+ done diff --git a/spec/ROOT b/spec/ROOT index 7e2f5bbcd..7878ad693 100644 --- a/spec/ROOT +++ b/spec/ROOT @@ -67,7 +67,7 @@ session ExecSpec = Word_Lib + options [document = false] theories "design/API_H" - "design/$L4V_ARCH/Intermediate_H" + "design/$L4V_ARCH/ArchIntermediate_H" (* diff --git a/spec/abstract/ARM/ArchCSpace_A.thy b/spec/abstract/ARM/ArchCSpace_A.thy index 6cfd109c4..06c105d4c 100644 --- a/spec/abstract/ARM/ArchCSpace_A.thy +++ b/spec/abstract/ARM/ArchCSpace_A.thy @@ -18,8 +18,27 @@ theory ArchCSpace_A imports ArchVSpace_A begin + context Arch begin global_naming ARM_A +definition cnode_guard_size_bits :: "nat" +where + cnode_guard_size_bits_def [simp]: "cnode_guard_size_bits \ 5" + +definition cnode_padding_bits :: "nat" +where + cnode_padding_bits_def [simp]: "cnode_padding_bits \ 3" + +text {* On a user request to modify a cnode capability, extract new guard bits and guard. *} +definition + update_cnode_cap_data :: "data \ nat \ data" where + "update_cnode_cap_data w \ + let + guard_bits = 18; + guard_size' = unat ((w >> cnode_padding_bits) && mask cnode_guard_size_bits); + guard'' = (w >> (cnode_padding_bits + cnode_guard_size_bits)) && mask guard_bits + in (guard_size', guard'')" + text {* For some purposes capabilities to physical objects are treated differently to others. *} definition diff --git a/spec/abstract/ARM/ArchTcb_A.thy b/spec/abstract/ARM/ArchTcb_A.thy new file mode 100644 index 000000000..84e0b6b42 --- /dev/null +++ b/spec/abstract/ARM/ArchTcb_A.thy @@ -0,0 +1,29 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +(* +Arch-specific functions for the abstract model of CSpace. +*) + +chapter "Architecture-specific TCB functions" + +theory ArchTcb_A +imports "../KHeap_A" +begin + +context Arch begin global_naming ARM_A + +definition + arch_tcb_set_ipc_buffer :: "machine_word \ vspace_ref \ (unit, 'a::state_ext) s_monad" +where + "arch_tcb_set_ipc_buffer target ptr \ as_user target $ set_register TPIDRURW ptr" + +end +end diff --git a/spec/abstract/ARM/Arch_Structs_A.thy b/spec/abstract/ARM/Arch_Structs_A.thy index d088e8745..7ae1f6f9a 100644 --- a/spec/abstract/ARM/Arch_Structs_A.thy +++ b/spec/abstract/ARM/Arch_Structs_A.thy @@ -260,7 +260,13 @@ where | DataPage dev sz \ if dev then ADeviceData sz else AUserData sz | ASIDPool f \ AASIDPool)" + +text {* For implementation reasons the badge word has differing amounts of bits *} +definition + badge_bits :: nat where + badge_bits_def [simp]: "badge_bits \ 28" end + section "Arch-specific tcb" diff --git a/spec/abstract/CSpace_A.thy b/spec/abstract/CSpace_A.thy index c95c1e432..daa6ec31f 100644 --- a/spec/abstract/CSpace_A.thy +++ b/spec/abstract/CSpace_A.thy @@ -32,11 +32,13 @@ requalify_consts arch_is_physical arch_same_region_as same_aobject_as - msg_max_length cap_transfer_data_size msg_max_extra_caps msg_align_bits + update_cnode_cap_data + cnode_padding_bits + cnode_guard_size_bits end @@ -96,7 +98,7 @@ where "max_free_index_update cap \ cap \ free_index:= max_free_index (untyped_sz_bits cap) \" definition - set_untyped_cap_as_full :: "cap \ cap \ obj_ref \ bool list\ (unit,'z::state_ext) s_monad" + set_untyped_cap_as_full :: "cap \ cap \ obj_ref \ bool list \ (unit,'z::state_ext) s_monad" where "set_untyped_cap_as_full src_cap new_cap src_slot \ if (is_untyped_cap src_cap \ is_untyped_cap new_cap @@ -136,11 +138,7 @@ definition else if is_cnode_cap cap then let (oref, bits, guard) = the_cnode_cap cap; - rights_bits = 3; - guard_bits = 18; - guard_size_bits = 5; - guard_size' = unat ((w >> rights_bits) && mask guard_size_bits); - guard'' = (w >> (rights_bits + guard_size_bits)) && mask guard_bits; + (guard_size', guard'') = update_cnode_cap_data w; guard' = drop (size guard'' - guard_size') (to_bl guard'') in if guard_size' + bits > word_bits @@ -856,6 +854,6 @@ definition section "Cap classification used to define invariants" datatype capclass = - PhysicalClass | ReplyClass "obj_ref" | IRQClass | ASIDMasterClass | NullClass | DomainClass + PhysicalClass | ReplyClass "obj_ref" | IRQClass | ASIDMasterClass | NullClass | DomainClass | IOPortClass end diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy index 8217191c4..067047602 100755 --- a/spec/abstract/Structures_A.thy +++ b/spec/abstract/Structures_A.thy @@ -41,6 +41,7 @@ requalify_consts asid_high_bits asid_low_bits arch_is_frame_type + badge_bits default_arch_tcb arch_tcb_context_get arch_tcb_context_set @@ -227,13 +228,6 @@ definition | ArchObjectCap acap \ ArchObjectCap (acap_rights_update cr' acap) | _ \ cap" -text {* For implementation reasons not all bits of the badge word can be used. *} -definition - badge_bits :: nat where - "badge_bits \ 28" - -declare badge_bits_def [simp] - definition badge_update :: "badge \ cap \ cap" where "badge_update data cap \ diff --git a/spec/abstract/Tcb_A.thy b/spec/abstract/Tcb_A.thy index ad16a2fbd..abb428313 100644 --- a/spec/abstract/Tcb_A.thy +++ b/spec/abstract/Tcb_A.thy @@ -15,13 +15,14 @@ The TCB and thread related specifications. chapter "Threads and TCBs" theory Tcb_A -imports TcbAcc_A Schedule_A +imports TcbAcc_A Schedule_A "$L4V_ARCH/ArchTcb_A" begin context begin interpretation Arch . requalify_consts arch_activate_idle_thread + arch_tcb_set_ipc_buffer end @@ -177,7 +178,7 @@ where | Some (ptr, frame) \ doE cap_delete (target, tcb_cnode_index 4); liftE $ thread_set (\t. t \ tcb_ipc_buffer := ptr \) target; - liftE $ as_user target $ set_register ARM.TPIDRURW ptr; + liftE $ arch_tcb_set_ipc_buffer target ptr; liftE $ case frame of None \ return () | Some (new_cap, src_slot) \ check_cap_at new_cap src_slot @@ -240,6 +241,10 @@ where return [] od)" +context Arch begin +declare arch_tcb_set_ipc_buffer_def [simp] +end + definition set_domain :: "obj_ref \ domain \ unit det_ext_monad" where "set_domain tptr new_dom \ do diff --git a/spec/design/ARM/ArchIntermediate_H.thy b/spec/design/ARM/ArchIntermediate_H.thy new file mode 100644 index 000000000..6fde0462f --- /dev/null +++ b/spec/design/ARM/ArchIntermediate_H.thy @@ -0,0 +1,68 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(GD_GPL) + *) + +chapter "Intermediate" + +theory ArchIntermediate_H +imports "../Intermediate_H" +begin + +context Arch begin +context begin + +private abbreviation (input) + "createNewPageCaps regionBase numObjects dev gSize pSize \ + let Data = (if dev then KOUserDataDevice else KOUserData) in + (do addrs \ createObjects regionBase numObjects Data gSize; + modify (\ks. ks \ gsUserPages := (\ addr. + if addr `~elem~` map fromPPtr addrs then Just pSize + else gsUserPages ks addr)\); + return $ map (\n. PageCap dev (PPtr (fromPPtr n)) VMReadWrite pSize Nothing) addrs + od)" + +private abbreviation (input) + "createNewTableCaps regionBase numObjects tableBits objectProto cap initialiseMappings \ (do + tableSize \ return (tableBits - objBits objectProto); + addrs \ createObjects regionBase numObjects (injectKO objectProto) tableSize; + pts \ return (map (PPtr \ fromPPtr) addrs); + initialiseMappings pts; + return $ map (\pt. cap pt Nothing) pts + od)" + +defs Arch_createNewCaps_def: +"Arch_createNewCaps t regionBase numObjects userSize dev \ + let pointerCast = PPtr \ fromPPtr + in (case t of + APIObjectType apiObject \ haskell_fail [] + | SmallPageObject \ + createNewPageCaps regionBase numObjects dev 0 ARMSmallPage + | LargePageObject \ + createNewPageCaps regionBase numObjects dev 4 ARMLargePage + | SectionObject \ + createNewPageCaps regionBase numObjects dev 8 ARMSection + | SuperSectionObject \ + createNewPageCaps regionBase numObjects dev 12 ARMSuperSection + | PageTableObject \ + createNewTableCaps regionBase numObjects ptBits (makeObject::pte) PageTableCap + (\pts. return ()) + | PageDirectoryObject \ + createNewTableCaps regionBase numObjects pdBits (makeObject::pde) PageDirectoryCap + (\pds. do objSize \ return (((1::nat) `~shiftL~` pdBits)); + mapM_x copyGlobalMappings pds; + doMachineOp $ mapM_x (\x. cleanCacheRange_PoU x + (x + (fromIntegral objSize) - 1) + (addrFromPPtr x)) pds + od) + )" + +end +end + +end diff --git a/spec/design/ArchInterrupt_H.thy b/spec/design/ArchInterrupt_H.thy deleted file mode 100644 index c34b7aceb..000000000 --- a/spec/design/ArchInterrupt_H.thy +++ /dev/null @@ -1,31 +0,0 @@ -(* - * Copyright 2014, General Dynamics C4 Systems - * - * This software may be distributed and modified according to the terms of - * the GNU General Public License version 2. Note that NO WARRANTY is provided. - * See "LICENSE_GPLv2.txt" for details. - * - * @TAG(GD_GPL) - *) - -theory ArchInterrupt_H -imports RetypeDecls_H -begin - -definition -decodeIRQControlInvocation :: "machine_word \ machine_word list \ machine_word \ capability list \ ( syscall_error , ArchRetypeDecls_H.irqcontrol_invocation ) kernel_f" -where -"decodeIRQControlInvocation arg1 arg2 arg3 arg4 \ throw IllegalOperation" - -definition -invokeIRQControl :: "ArchRetypeDecls_H.irqcontrol_invocation \ unit kernel_p" -where -"invokeIRQControl arg1 \ haskell_fail []" - -definition -checkIRQ :: "machine_word \ ( syscall_error , unit ) kernel_f" -where -"checkIRQ irq\ rangeCheck irq (fromEnum minIRQ) (fromEnum maxIRQ)" - - -end diff --git a/spec/design/ARM/Intermediate_H.thy b/spec/design/Intermediate_H.thy similarity index 57% rename from spec/design/ARM/Intermediate_H.thy rename to spec/design/Intermediate_H.thy index 05aa83aa6..ac675fc42 100644 --- a/spec/design/ARM/Intermediate_H.thy +++ b/spec/design/Intermediate_H.thy @@ -11,12 +11,14 @@ chapter "Intermediate" theory Intermediate_H -imports "../API_H" +imports "API_H" begin + context begin interpretation Arch . requalify_consts clearMemory end + (* * Intermediate function bodies that were once in the Haskell spec, but are * now no longer. @@ -44,95 +46,37 @@ createNewCaps :: "object_type \ machine_word \ nat \ machine_word \ nat \ nat \ bool \ arch_capability list kernel" -thm injectKO_defs + defs insertNewCaps_def: "insertNewCaps newType srcSlot destSlots regionBase magnitudeBits dev \ (do - caps \ createNewCaps newType regionBase (length destSlots) magnitudeBits dev ; + caps \ createNewCaps newType regionBase (length destSlots) magnitudeBits dev; zipWithM_x (insertNewCap srcSlot) destSlots caps -od)" - -defs (in Arch) Arch_createNewCaps_def: -"Arch_createNewCaps t regionBase numObjects arg4 dev \ - let pointerCast = PPtr \ fromPPtr; - Data = (if dev then KOUserDataDevice else KOUserData) - in (case t of - APIObjectType v5 \ - haskell_fail [] - | SmallPageObject \ (do - addrs \ createObjects regionBase numObjects Data 0; - modify (\ ks. ks \ gsUserPages := (\ addr. - if addr `~elem~` map fromPPtr addrs then Just ARMSmallPage - else gsUserPages ks addr)\); - return $ map (\ n. PageCap dev (pointerCast n) VMReadWrite - ARMSmallPage Nothing) addrs - od) - | LargePageObject \ (do - addrs \ createObjects regionBase numObjects Data 4; - modify (\ ks. ks \ gsUserPages := (\ addr. - if addr `~elem~` map fromPPtr addrs then Just ARMLargePage - else gsUserPages ks addr)\); - return $ map (\ n. PageCap dev (pointerCast n) VMReadWrite - ARMLargePage Nothing) addrs - od) - | SectionObject \ (do - addrs \ createObjects regionBase numObjects Data 8; - modify (\ ks. ks \ gsUserPages := (\ addr. - if addr `~elem~` map fromPPtr addrs then Just ARMSection - else gsUserPages ks addr)\); - return $ map (\ n. PageCap dev (pointerCast n) VMReadWrite - ARMSection Nothing) addrs - od) - | SuperSectionObject \ (do - addrs \ createObjects regionBase numObjects Data 12; - modify (\ ks. ks \ gsUserPages := (\ addr. - if addr `~elem~` map fromPPtr addrs then Just ARMSuperSection - else gsUserPages ks addr)\); - return $ map (\ n. PageCap dev (pointerCast n) VMReadWrite - ARMSuperSection Nothing) addrs - od) - | PageTableObject \ (do - ptSize \ return ( ptBits - objBits (makeObject ::pte)); - addrs \ createObjects regionBase numObjects (injectKO (makeObject ::pte)) ptSize; - objSize \ return (((1::nat) `~shiftL~` ptBits)); - pts \ return ( map pointerCast addrs); - return $ map (\ pt. PageTableCap pt Nothing) pts - od) - | PageDirectoryObject \ (do - pdSize \ return ( pdBits - objBits (makeObject ::pde)); - addrs \ createObjects regionBase numObjects (injectKO (makeObject ::pde)) pdSize; - objSize \ return ( ((1::nat) `~shiftL~` pdBits)); - pds \ return ( map pointerCast addrs); - mapM_x copyGlobalMappings pds; - doMachineOp $ mapM_x (\x. cleanCacheRange_PoU x (x + (fromIntegral objSize) - 1) - (addrFromPPtr x)) pds; - return $ map (\ pd. PageDirectoryCap pd Nothing) pds - od) - )" + od)" defs createNewCaps_def: "createNewCaps t regionBase numObjects userSize dev \ (case toAPIType t of - Some TCBObject \ (do + Some TCBObject \ (do addrs \ createObjects regionBase numObjects (injectKO (makeObject ::tcb)) 0; curdom \ curDomain; mapM_x (\tptr. threadSet (tcbDomain_update (\_. curdom)) tptr) addrs; return $ map (\ addr. ThreadCap addr) addrs od) - | Some EndpointObject \ (do + | Some EndpointObject \ (do addrs \ createObjects regionBase numObjects (injectKO (makeObject ::endpoint)) 0; return $ map (\ addr. EndpointCap addr 0 True True True) addrs - od) - | Some NotificationObject \ (do + od) + | Some NotificationObject \ (do addrs \ createObjects regionBase numObjects (injectKO (makeObject ::notification)) 0; return $ map (\ addr. NotificationCap addr 0 True True) addrs - od) - | Some ArchTypes_H.CapTableObject \ (do + od) + | Some ArchTypes_H.CapTableObject \ (do addrs \ createObjects regionBase numObjects (injectKO (makeObject ::cte)) userSize; modify (\ ks. ks \ gsCNodes := (\ addr. if addr `~elem~` map fromPPtr addrs then Just userSize else gsCNodes ks addr)\); return $ map (\ addr. CNodeCap addr userSize 0 0) addrs - od) + od) | Some ArchTypes_H.Untyped \ return $ map (\ n. UntypedCap dev (regionBase + n * 2 ^ (fromIntegral userSize)) userSize 0) @@ -140,7 +84,7 @@ defs createNewCaps_def: | None \ (do archCaps \ Arch_createNewCaps t regionBase numObjects userSize dev; return $ map ArchObjectCap archCaps - od) + od) )" defs createObjects_def: diff --git a/spec/design/m-skel/ARM/MachineTypes.thy b/spec/design/m-skel/ARM/MachineTypes.thy index d796f362e..c75f27a03 100644 --- a/spec/design/m-skel/ARM/MachineTypes.thy +++ b/spec/design/m-skel/ARM/MachineTypes.thy @@ -29,8 +29,15 @@ section "Types" #INCLUDE_HASKELL SEL4/Machine/RegisterSet/ARM.lhs CONTEXT ARM decls_only (*<*) +section "Machine Words" + type_synonym machine_word_len = 32 +definition + word_size_bits :: "'a :: numeral" +where + "word_size_bits \ 2" + end context begin interpretation Arch . diff --git a/spec/haskell/SEL4.cabal b/spec/haskell/SEL4.cabal index 115d3fba1..7d1e7fb79 100644 --- a/spec/haskell/SEL4.cabal +++ b/spec/haskell/SEL4.cabal @@ -21,13 +21,17 @@ Flag FFI description: Include the C language bindings default: True +Flag ArchArm + description: Include ARM modules and platforms (else x64) + default: True + Library exposed-modules: SEL4 SEL4.Machine.Target - -- Newer mtl's cause old APIs to be deprecated, which fails -Werror. -- base-4.8 (ghc 7.10) exports conflicting name Prelude.Word. build-depends: mtl==2.1.3.1, base==4.7.*, array, containers, transformers + if flag(FFI) -- FFIBindings currently relies on POSIX signal handlers. This could -- be fixed. @@ -36,6 +40,9 @@ Library include-dirs: include install-includes: sel4model.h gic.h dist/build/Simulation/FFIBindings_stub.h + else + build-depends: unix + include-dirs: include other-modules: SEL4.API SEL4.API.Syscall @@ -75,13 +82,15 @@ Library Data.BinaryTree Data.Helpers + SEL4.Machine.Hardware.GICInterface + SEL4.Machine.Hardware.MCTInterface + SEL4.Machine.Hardware.MPTimerInterface + if flag(ArchArm) + other-modules: SEL4.Machine.Hardware.ARM.KZM SEL4.Machine.Hardware.ARM.Exynos4210 SEL4.Machine.Hardware.ARM.Sabre SEL4.Machine.Hardware.ARM.Callbacks - SEL4.Machine.Hardware.GICInterface - SEL4.Machine.Hardware.MCTInterface - SEL4.Machine.Hardware.MPTimerInterface SEL4.API.Types.ARM SEL4.API.InvocationLabels.ARM @@ -98,7 +107,28 @@ Library SEL4.Model.StateData.ARM SEL4.Machine.RegisterSet.ARM SEL4.Machine.Hardware.ARM - + + else + -- FIXME: should be a flag also, or some other way to conditionally compile + -- Setup.hs hooks can handle this, but do we want to do that? + other-modules: + + SEL4.API.Types.X64 + SEL4.API.InvocationLabels.X64 + SEL4.API.Invocation.X64 + SEL4.Kernel.VSpace.X64 + SEL4.Kernel.Thread.X64 + SEL4.Object.ObjectType.X64 + SEL4.Object.Structures.X64 + SEL4.Object.Interrupt.X64 + SEL4.Object.Instances.X64 + SEL4.Object.IOPort.X64 + SEL4.Object.TCB.X64 + SEL4.Model.StateData.X64 + SEL4.Machine.RegisterSet.X64 + SEL4.Machine.Hardware.X64 + + SEL4.Machine.Hardware.X64.PC99 hs-source-dirs: src ghc-prof-options: -auto-all -prof -fprof-auto diff --git a/spec/haskell/src/SEL4/API/Invocation.lhs b/spec/haskell/src/SEL4/API/Invocation.lhs index dfcc916dc..09316c44a 100644 --- a/spec/haskell/src/SEL4/API/Invocation.lhs +++ b/spec/haskell/src/SEL4/API/Invocation.lhs @@ -126,11 +126,14 @@ The following data type defines the parameters expected for invocations of Untyp The following data type defines the set of possible invocations for interrupt controller capabilities. +%FIXME IssueIRQHandler is not really handled on x64, instead it has two arch-specific ones + > data IRQControlInvocation > = ArchIRQControl { archIRQControl :: Arch.IRQControlInvocation } > | IssueIRQHandler { > issueHandlerIRQ :: IRQ, -> issueHandlerSlot, issueHandlerControllerSlot :: PPtr CTE } +> issueHandlerSlot, +> issueHandlerControllerSlot :: PPtr CTE } > deriving Show \subsubsection{IRQ Handler Invocations} diff --git a/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs b/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs index 9229374e9..653c3e877 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs +++ b/spec/haskell/src/SEL4/Kernel/Thread/ARM.lhs @@ -26,7 +26,7 @@ This module contains the architecture-specific thread switch code for the ARM. \end{impdetails} -The ARM thread switch function invalidates all caches and the TLB, and writes the IPC buffer pointer to the first word of the globals page. +The ARM thread switch function invalidates all caches and the TLB. > switchToThread :: PPtr TCB -> Kernel () > switchToThread tcb = do diff --git a/spec/haskell/src/SEL4/Object/Interrupt.lhs b/spec/haskell/src/SEL4/Object/Interrupt.lhs index ef1611a60..4faeef2f7 100644 --- a/spec/haskell/src/SEL4/Object/Interrupt.lhs +++ b/spec/haskell/src/SEL4/Object/Interrupt.lhs @@ -107,6 +107,8 @@ An IRQ handler capability allows a thread possessing it to set an endpoint which > toBool :: Word -> Bool > toBool w = w /= 0 +%FIXME x64 naming: this should be called perform, not invoke, same for CNode + > invokeIRQHandler :: IRQHandlerInvocation -> Kernel () > invokeIRQHandler (AckIRQ irq) = > doMachineOp $ maskInterrupt False irq diff --git a/spec/machine/ARM/MachineTypes.thy b/spec/machine/ARM/MachineTypes.thy index 136f59915..779bcbc50 100644 --- a/spec/machine/ARM/MachineTypes.thy +++ b/spec/machine/ARM/MachineTypes.thy @@ -59,8 +59,15 @@ sanitiseRegister :: "register \ machine_word \ machine_w (*<*) +section "Machine Words" + type_synonym machine_word_len = 32 +definition + word_size_bits :: "'a :: numeral" +where + "word_size_bits \ 2" + end context begin interpretation Arch . diff --git a/spec/machine/MachineExports.thy b/spec/machine/MachineExports.thy index 0a737495c..e7da6a1a3 100644 --- a/spec/machine/MachineExports.thy +++ b/spec/machine/MachineExports.thy @@ -45,8 +45,20 @@ requalify_consts resetTimer maxIRQ minIRQ + word_size_bits clearMemory +(* HERE IS THE PLACE FOR GENERIC WORD LEMMAS FOR ALL ARCHITECTURES *) + +lemma Suc_unat_mask_div_obfuscated: + "Suc (unat (mask sz div (word_size::machine_word))) = 2 ^ (min sz word_bits - word_size_bits)" + unfolding word_size_bits_def + by (rule Suc_unat_mask_div) + +lemma word_size_size_bits_nat: + "2^word_size_bits = (word_size :: nat)" + by (simp add: word_size_bits_def word_size_def) + end end diff --git a/tools/c-parser/.gitignore b/tools/c-parser/.gitignore index e4d01046e..158a93f26 100644 --- a/tools/c-parser/.gitignore +++ b/tools/c-parser/.gitignore @@ -2,3 +2,16 @@ *.minfo umm_types.txt globalmakevars.local + +/StrictC.grm.desc + +/standalone-parser/table.ML +/standalone-parser/ARM/ +/standalone-parser/X64/ + +/tools/mllex/mllex +/tools/mlyacc/mlyacc +/tools/mlyacc/src/yacc.lex.sml + +/testfiles/**/ROOT +/testfiles/modifies_speed.c diff --git a/tools/c-parser/IsaMakefile b/tools/c-parser/IsaMakefile index f17433b34..3c46a53d0 100644 --- a/tools/c-parser/IsaMakefile +++ b/tools/c-parser/IsaMakefile @@ -42,12 +42,12 @@ $(HEAPS): .FORCE # We dynamically generate a ROOT file containing all the test files, and # then build it using Isabelle. # -cparser_test: testfiles/ROOT .FORCE - $(ISABELLE_TOOL) build -d ../.. -d testfiles -b -v CParserTest -testfiles/ROOT: testfiles testfiles/*.c testfiles/*.thy ../../misc/scripts/gen_isabelle_root.py - python ../../misc/scripts/gen_isabelle_root.py -i testfiles -o testfiles/ROOT -s CParserTest -b CParser -all_tests.thy: testfiles testfiles/*.c ../../misc/scripts/gen_isabelle_root.py - python ../../misc/scripts/gen_isabelle_root.py -T -o $@ -b CParser -i testfiles +cparser_test: testfiles/$(L4V_ARCH)/ROOT .FORCE + $(ISABELLE_TOOL) build -d ../.. -d testfiles/$(L4V_ARCH) -b -v CParserTest +testfiles/$(L4V_ARCH)/ROOT: testfiles testfiles/*.c testfiles/*.thy ../../misc/scripts/gen_isabelle_root.py + python ../../misc/scripts/gen_isabelle_root.py -i testfiles -i testfiles/$(L4V_ARCH) -o testfiles/$(L4V_ARCH)/ROOT -s CParserTest -b CParser +all_tests_$(L4V_ARCH).thy: testfiles testfiles/*.c ../../misc/scripts/gen_isabelle_root.py + python ../../misc/scripts/gen_isabelle_root.py -T -o $@ -b CParser -i testfiles -i testfiles/$(L4V_ARCH) GRAMMAR_PRODUCTS = l4c.lex.sml l4c.grm.sml l4c.grm.sig diff --git a/tools/c-parser/standalone-parser/Makefile b/tools/c-parser/standalone-parser/Makefile index 078c39943..7952b4929 100644 --- a/tools/c-parser/standalone-parser/Makefile +++ b/tools/c-parser/standalone-parser/Makefile @@ -20,16 +20,16 @@ ifndef STP_INCLUDED STP_INCLUDED=true ARM_DIR=$(STP_PFX)/ARM -F64_DIR=$(STP_PFX)/FAKE64 -ARCH_DIRS=$(ARM_DIR) $(F64_DIR) +X64_DIR=$(STP_PFX)/X64 +ARCH_DIRS=$(ARM_DIR) $(X64_DIR) STPARSER_ARM=$(ARM_DIR)/c-parser -STPARSER_F64=$(F64_DIR)/c-parser -STPARSERS=$(STPARSER_ARM) $(STPARSER_F64) +STPARSER_X64=$(X64_DIR)/c-parser +STPARSERS=$(STPARSER_ARM) $(STPARSER_X64) TOKENIZER_ARM=$(ARM_DIR)/tokenizer -TOKENIZER_F64=$(F64_DIR)/tokenizer -TOKENIZERS=$(TOKENIZER_ARM) $(TOKENIZER_F64) +TOKENIZER_X64=$(X64_DIR)/tokenizer +TOKENIZERS=$(TOKENIZER_ARM) $(TOKENIZER_X64) .PHONY: all cparser_tools stp_all standalone-cparser standalone-tokenizer @@ -55,26 +55,26 @@ ifeq ($(SML_COMPILER),mlton) # ARM_MLB_PATH := -mlb-path-var 'L4V_ARCH ARM' -F64_MLB_PATH := -mlb-path-var 'L4V_ARCH FAKE64' +X64_MLB_PATH := -mlb-path-var 'L4V_ARCH X64' PARSER_DEPS_ARM := $(shell mlton $(ARM_MLB_PATH) -stop f $(STP_PFX)/c-parser.mlb) -PARSER_DEPS_F64 := $(shell mlton $(F64_MLB_PATH) -stop f $(STP_PFX)/c-parser.mlb) +PARSER_DEPS_X64 := $(shell mlton $(X64_MLB_PATH) -stop f $(STP_PFX)/c-parser.mlb) TOKENIZER_DEPS_ARM := $(shell mlton $(ARM_MLB_PATH) -stop f $(STP_PFX)/tokenizer.mlb) -TOKENIZER_DEPS_F64 := $(shell mlton $(F64_MLB_PATH) -stop f $(STP_PFX)/tokenizer.mlb) +TOKENIZER_DEPS_X64 := $(shell mlton $(X64_MLB_PATH) -stop f $(STP_PFX)/tokenizer.mlb) $(STPARSER_ARM): $(PARSER_DEPS_ARM) | $(ARM_DIR) mlton $(ARM_MLB_PATH) -output $@ $< -$(STPARSER_F64): $(PARSER_DEPS_F64) | $(F64_DIR) - mlton $(F64_MLB_PATH) -output $@ $< +$(STPARSER_X64): $(PARSER_DEPS_X64) | $(X64_DIR) + mlton $(X64_MLB_PATH) -output $@ $< $(TOKENIZER_ARM): $(TOKENIZER_DEPS_ARM) | $(ARM_DIR) mlton $(ARM_MLB_PATH) -output $@ $< -$(TOKENIZER_F64): $(TOKENIZER_DEPS_F64) | $(F64_DIR) - mlton $(F64_MLB_PATH) -output $@ $< +$(TOKENIZER_X64): $(TOKENIZER_DEPS_X64) | $(X64_DIR) + mlton $(X64_MLB_PATH) -output $@ $< else ifeq ($(SML_COMPILER),poly) diff --git a/tools/c-parser/testfiles/asm_stmt.c b/tools/c-parser/testfiles/ARM/asm_stmt.c similarity index 100% rename from tools/c-parser/testfiles/asm_stmt.c rename to tools/c-parser/testfiles/ARM/asm_stmt.c diff --git a/tools/c-parser/testfiles/asm_stmt.thy b/tools/c-parser/testfiles/ARM/asm_stmt.thy similarity index 94% rename from tools/c-parser/testfiles/asm_stmt.thy rename to tools/c-parser/testfiles/ARM/asm_stmt.thy index da07df7bc..918248ee4 100644 --- a/tools/c-parser/testfiles/asm_stmt.thy +++ b/tools/c-parser/testfiles/ARM/asm_stmt.thy @@ -10,7 +10,7 @@ theory asm_stmt -imports "../CTranslation" +imports "../../CTranslation" begin diff --git a/tools/c-parser/testfiles/ARM/imports/MachineWords.thy b/tools/c-parser/testfiles/ARM/imports/MachineWords.thy new file mode 100644 index 000000000..f9ddab148 --- /dev/null +++ b/tools/c-parser/testfiles/ARM/imports/MachineWords.thy @@ -0,0 +1,24 @@ +(* + * Copyright 2014, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + *) + +theory MachineWords +imports "../../../CTranslation" +begin + +type_synonym machine_word_len = "32" + +type_synonym machine_word = "machine_word_len word" + +abbreviation "machine_word_bytes \ 4 :: nat" + +lemma of_nat_machine_word_bytes[simp]: "of_nat machine_word_bytes = 4" + by simp + +end diff --git a/tools/c-parser/testfiles/X64/imports/MachineWords.thy b/tools/c-parser/testfiles/X64/imports/MachineWords.thy new file mode 100644 index 000000000..9bf8a8b74 --- /dev/null +++ b/tools/c-parser/testfiles/X64/imports/MachineWords.thy @@ -0,0 +1,24 @@ +(* + * Copyright 2014, NICTA + * + * This software may be distributed and modified according to the terms of + * the BSD 2-Clause license. Note that NO WARRANTY is provided. + * See "LICENSE_BSD2.txt" for details. + * + * @TAG(NICTA_BSD) + *) + +theory MachineWords +imports "../../../CTranslation" +begin + +type_synonym machine_word_len = "64" + +type_synonym machine_word = "machine_word_len word" + +abbreviation "machine_word_bytes \ 8 :: nat" + +lemma of_nat_machine_word_bytes[simp]: "of_nat machine_word_bytes = 8" + by simp + +end diff --git a/tools/c-parser/testfiles/factorial.c b/tools/c-parser/testfiles/factorial.c index 01dc8be0e..ba6b543ef 100644 --- a/tools/c-parser/testfiles/factorial.c +++ b/tools/c-parser/testfiles/factorial.c @@ -11,24 +11,24 @@ /** FNSPEC alloc_spec: "\\ k. \ \ \\. (free_pool k)\<^bsup>sep\<^esup> \ - \ret__ptr_to_unsigned :== PROC alloc() + \ret__ptr_to_unsigned_long :== PROC alloc() \ ((\p s. if k > 0 then (\\<^sub>s p \\<^sup>* \\<^sub>s (p +\<^sub>p 1) \\<^sup>* - free_pool (k - 1)) s else (free_pool k) s \ p = NULL) \ret__ptr_to_unsigned)\<^bsup>sep\<^esup> \" + free_pool (k - 1)) s else (free_pool k) s \ p = NULL) \ret__ptr_to_unsigned_long)\<^bsup>sep\<^esup> \" */ -unsigned int *alloc(void) +unsigned long *alloc(void) { /* Stub */ } /** FNSPEC free_spec: "\\ k. \ \ - \\. (sep_cut' (ptr_val \p) (2 * size_of TYPE(word32)) \\<^sup>* free_pool k)\<^bsup>sep\<^esup> \ + \\. (sep_cut' (ptr_val \p) (2 * size_of TYPE(machine_word)) \\<^sup>* free_pool k)\<^bsup>sep\<^esup> \ PROC free(\p) \ (free_pool (k + 1))\<^bsup>sep\<^esup> \" */ -void free(unsigned int *p) +void free(unsigned long *p) { /* Stub */ } @@ -36,14 +36,14 @@ void free(unsigned int *p) /** FNSPEC factorial_spec: "\\ k. \ \ \\. (free_pool k)\<^bsup>sep\<^esup> \ - \ret__ptr_to_unsigned :== PROC factorial(\n) - \ if \ret__ptr_to_unsigned \ NULL then (sep_fac_list \<^bsup>\\<^esup>n \ret__ptr_to_unsigned \\<^sup>* + \ret__ptr_to_unsigned_long :== PROC factorial(\n) + \ if \ret__ptr_to_unsigned_long \ NULL then (sep_fac_list \<^bsup>\\<^esup>n \ret__ptr_to_unsigned_long \\<^sup>* free_pool (k - (unat \<^bsup>\\<^esup>n + 1)))\<^bsup>sep\<^esup> \ (unat \<^bsup>\\<^esup>n + 1) \ k else (free_pool k)\<^bsup>sep\<^esup> \" */ -unsigned int *factorial(unsigned int n) +unsigned long *factorial(unsigned long n) { - unsigned int *p, *q; + unsigned long *p, *q; if (n == 0) { p = alloc(); @@ -69,7 +69,7 @@ unsigned int *factorial(unsigned int n) /** INV: "\ \xs. (sep_list xs \q \\<^sup>* free_pool (k - length xs))\<^bsup>sep\<^esup> \ length xs \ k \" */ { - unsigned int *k = (unsigned int *)*(q + 1); + unsigned long *k = (unsigned long *)*(q + 1); free(q); q = k; @@ -79,7 +79,7 @@ unsigned int *factorial(unsigned int n) } *p = n * *q; - *(p + 1) = (unsigned int)q; + *(p + 1) = (unsigned long)q; return p; } diff --git a/tools/c-parser/testfiles/factorial.thy b/tools/c-parser/testfiles/factorial.thy index 2b3d2a246..97f3d7220 100644 --- a/tools/c-parser/testfiles/factorial.thy +++ b/tools/c-parser/testfiles/factorial.thy @@ -1,5 +1,5 @@ (* - * Copyright 2014, NICTA + * Copyright 201machine_word_bytes, NICTA * * This software may be distributed and modified according to the terms of * the BSD 2-Clause license. Note that NO WARRANTY is provided. @@ -9,7 +9,7 @@ *) theory factorial -imports "../CTranslation" +imports "../CTranslation" "$L4V_ARCH/imports/MachineWords" begin declare hrs_simps [simp add] @@ -18,7 +18,7 @@ declare sep_conj_ac [simp add] consts free_pool :: "nat \ heap_assert" primrec - fac :: "nat \ word32" + fac :: "nat \ machine_word" where "fac 0 = 1" | "fac (Suc n) = of_nat (Suc n) * fac n" @@ -40,7 +40,7 @@ lemma fac_unfold: done primrec - fac_list :: "nat \ word32 list" + fac_list :: "nat \ machine_word list" where "fac_list 0 = [1]" | "fac_list (Suc n) = fac (Suc n) # fac_list n" @@ -58,7 +58,7 @@ lemma fac_list_unfold: done primrec - sep_list :: "word32 list \ word32 ptr \ heap_assert" + sep_list :: "machine_word list \ machine_word ptr \ heap_assert" where "sep_list [] p = (\s. p=NULL \ \ s)" | "sep_list (x#xs) p = (\s. \j. ((p \ x) \\<^sup>* (p +\<^sub>p 1) \ j \\<^sup>* @@ -69,7 +69,7 @@ lemma sep_list_NULL [simp]: by (case_tac xs) auto definition - sep_fac_list :: "word32 \ word32 ptr \ heap_assert" + sep_fac_list :: "machine_word \ machine_word ptr \ heap_assert" where "sep_fac_list n p \ sep_list (fac_list (unat n)) p" @@ -103,7 +103,7 @@ install_C_file memsafe "factorial.c" thm factorial_global_addresses.factorial_body_def lemma (in factorial_global_addresses) mem_safe_alloc: - "mem_safe (\ret__ptr_to_unsigned :== PROC alloc()) \" + "mem_safe (\ret__ptr_to_unsigned_long :== PROC alloc()) \" apply(insert alloc_impl) apply(unfold alloc_body_def) apply(subst mem_safe_restrict) @@ -113,10 +113,10 @@ lemma (in factorial_global_addresses) mem_safe_alloc: done lemma (in factorial_global_addresses) sep_frame_alloc: - "\ \\. \ \ \\. (P (f \(\x. x)))\<^bsup>sep\<^esup> \ \ret__ptr_to_unsigned :== PROC alloc() \ (Q (g \ \(\x. x)))\<^bsup>sep\<^esup> \; + "\ \\. \ \ \\. (P (f \(\x. x)))\<^bsup>sep\<^esup> \ \ret__ptr_to_unsigned_long :== PROC alloc() \ (Q (g \ \(\x. x)))\<^bsup>sep\<^esup> \; htd_ind f; htd_ind g; \s. htd_ind (g s) \ \ \\. \ \ \\. (P (f \(\x. x)) \\<^sup>* R (h \(\x. x)))\<^bsup>sep\<^esup> \ - \ret__ptr_to_unsigned :== PROC alloc() + \ret__ptr_to_unsigned_long :== PROC alloc() \ (Q (g \ \(\x. x)) \\<^sup>* R (h \))\<^bsup>sep\<^esup> \" unfolding sep_app_def by (rule sep_frame, auto intro!: mem_safe_alloc) @@ -124,9 +124,9 @@ lemma (in factorial_global_addresses) sep_frame_alloc: lemma (in alloc_spec) alloc_spec': shows "\\ k R f. factorial_global_addresses.\ \ \\. ((\x. free_pool k) ((\x. undefined) \(\x. x)) \\<^sup>* R (f \(\x. x)))\<^bsup>sep\<^esup> \ - \ret__ptr_to_unsigned :== PROC alloc() + \ret__ptr_to_unsigned_long :== PROC alloc() \ ((\p s. if k > 0 then (\\<^sub>s p \\<^sup>* \\<^sub>s (p +\<^sub>p 1) \\<^sup>* - free_pool (k - 1)) s else (free_pool k) s \ p = NULL) \ret__ptr_to_unsigned + free_pool (k - 1)) s else (free_pool k) s \ p = NULL) \ret__ptr_to_unsigned_long \\<^sup>* R (f \))\<^bsup>sep\<^esup> \" apply clarify apply(insert alloc_spec) @@ -159,7 +159,7 @@ lemma (in factorial_global_addresses) sep_frame_free: lemma (in free_spec) free_spec': shows "\\ k R f. factorial_global_addresses.\ \ - \\. ((\p. sep_cut' (ptr_val p) (2 * size_of TYPE(word32)) \\<^sup>* free_pool k) \p \\<^sup>* R (f \(\x. x)))\<^bsup>sep\<^esup> \ + \\. ((\p. sep_cut' (ptr_val p) (2 * size_of TYPE(machine_word)) \\<^sup>* free_pool k) \p \\<^sup>* R (f \(\x. x)))\<^bsup>sep\<^esup> \ PROC free(\p) \ ((\x. free_pool (k + 1)) ((\x. ()) \(\x. x)) \\<^sup>* R (f \))\<^bsup>sep\<^esup> \" apply clarify @@ -171,28 +171,28 @@ lemma (in free_spec) free_spec': done lemma double_word_sep_cut': - "(p \ x \\<^sup>* (p +\<^sub>p 1) \ y) s \ sep_cut' (ptr_val (p::word32 ptr)) 8 s" + "(p \ x \\<^sup>* (p +\<^sub>p 1) \ y) s \ sep_cut' (ptr_val (p::machine_word ptr)) (2*machine_word_bytes) s" apply(clarsimp simp: sep_conj_def sep_cut'_def dest!: sep_map_dom) -apply(subgoal_tac "{ptr_val p..+4} \ {ptr_val p..+8}") - apply(subgoal_tac "{ptr_val p+4..+4} \ {ptr_val p..+8}") +apply(subgoal_tac "{ptr_val p..+machine_word_bytes} \ {ptr_val p..+(2*machine_word_bytes)}") + apply(subgoal_tac "{ptr_val p+(of_nat machine_word_bytes)..+machine_word_bytes} \ {ptr_val p..+(2*machine_word_bytes)}") apply rule - apply fast + apply (fastforce simp: ptr_add_def) apply clarsimp apply(drule intvlD) apply clarsimp - apply(case_tac "k < 4") + apply(case_tac "k < machine_word_bytes") apply(erule intvlI) apply(erule notE) apply(clarsimp simp: intvl_def) - apply(rule_tac x="k - 4" in exI) + apply(rule_tac x="k - machine_word_bytes" in exI) apply rule apply(simp only: unat_simps) apply(subst mod_less) apply(simp add: addr_card) - apply simp + apply (simp add: ptr_add_def addr_card) apply simp apply(clarsimp simp: intvl_def) - apply(rule_tac x="4+k" in exI) + apply(rule_tac x="machine_word_bytes+k" in exI) apply simp apply(rule intvl_start_le) apply simp @@ -209,11 +209,9 @@ lemma (in specs) factorial_spec: prefer 2 apply (simp add: whileAnno_def factorial_invs_body_def) apply(subst factorial_invs_body_def) - apply (simp only: ucast_id) apply(unfold sep_app_def) apply (vcg exspec=alloc_spec' exspec=free_spec') apply (fold lift_def) - apply(clarsimp simp: sep_app_def) apply (rule conjI) apply clarsimp @@ -224,12 +222,12 @@ lemma (in specs) factorial_spec: apply (rule conjI) apply clarsimp apply clarsimp - apply (rename_tac a b ret__ptr_to_unsigned) - apply(subgoal_tac "(\\<^sub>s ret__ptr_to_unsigned \\<^sup>* sep_true) (lift_state (a,b))") + apply (rename_tac a b ret__ptr_to_unsigned_long) + apply(subgoal_tac "(\\<^sub>s ret__ptr_to_unsigned_long \\<^sup>* sep_true) (lift_state (a,b))") prefer 2 apply(drule sep_conj_sep_true_right) apply simp - apply(subgoal_tac "(\\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \\<^sup>* sep_true) (lift_state (a,b))") + apply(subgoal_tac "(\\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \\<^sup>* sep_true) (lift_state (a,b))") prefer 2 apply(drule sep_conj_sep_true_left) apply simp @@ -258,18 +256,18 @@ lemma (in specs) factorial_spec: apply(rule_tac x="fac_list (unat (n - 1))" in exI) apply clarsimp apply clarsimp - apply(subgoal_tac "(\\<^sub>s ret__ptr_to_unsigned \\<^sup>* sep_true) (lift_state (ab,bb))") + apply(subgoal_tac "(\\<^sub>s ret__ptr_to_unsigned_long \\<^sup>* sep_true) (lift_state (ab,bb))") prefer 2 apply(erule (1) sep_conj_impl) apply simp - apply(subgoal_tac "(\\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \\<^sup>* sep_true) (lift_state (ab,bb))") + apply(subgoal_tac "(\\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \\<^sup>* sep_true) (lift_state (ab,bb))") prefer 2 - apply(subgoal_tac "(\\<^sub>s ret__ptr_to_unsigned \\<^sup>* - \\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \\<^sup>* - sep_fac_list (n - 1) ret__ptr_to_unsigneda \\<^sup>* + apply(subgoal_tac "(\\<^sub>s ret__ptr_to_unsigned_long \\<^sup>* + \\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \\<^sup>* + sep_fac_list (n - 1) ret__ptr_to_unsigned_longa \\<^sup>* free_pool (k - Suc (unat n))) = - (\\<^sub>s (ret__ptr_to_unsigned +\<^sub>p 1) \\<^sup>* (\\<^sub>s ret__ptr_to_unsigned \\<^sup>* - sep_fac_list (n - 1) ret__ptr_to_unsigneda \\<^sup>* + (\\<^sub>s (ret__ptr_to_unsigned_long +\<^sub>p 1) \\<^sup>* (\\<^sub>s ret__ptr_to_unsigned_long \\<^sup>* + sep_fac_list (n - 1) ret__ptr_to_unsigned_longa \\<^sup>* free_pool (k - Suc (unat n))))") prefer 2 apply simp @@ -282,7 +280,7 @@ lemma (in specs) factorial_spec: apply clarsimp apply (rule conjI, unat_arith) apply sep_exists_tac - apply(rule_tac x="ptr_val ret__ptr_to_unsigneda" in exI) + apply(rule_tac x="ptr_val ret__ptr_to_unsigned_longa" in exI) apply clarsimp apply(subst fac_unfold) apply unat_arith @@ -317,7 +315,7 @@ lemma (in specs) factorial_spec: apply(subst (asm) sep_conj_assoc [symmetric])+ apply(erule sep_conj_impl) apply simp - apply(erule double_word_sep_cut') + apply(erule double_word_sep_cut'[simplified]) apply assumption apply simp apply clarsimp @@ -330,7 +328,7 @@ lemma (in specs) factorial_spec: declare hrs_simps [simp del] lemma (in factorial_global_addresses) mem_safe_factorial: - shows "mem_safe (\ret__ptr_to_unsigned :== PROC factorial(\n)) \" + shows "mem_safe (\ret__ptr_to_unsigned_long :== PROC factorial(\n)) \" apply(subst mem_safe_restrict) apply(rule intra_mem_safe) apply (insert factorial_impl free_impl alloc_impl) diff --git a/tools/c-parser/testfiles/kmalloc.thy b/tools/c-parser/testfiles/kmalloc.thy index 2cf6ebb93..8bf0904b3 100644 --- a/tools/c-parser/testfiles/kmalloc.thy +++ b/tools/c-parser/testfiles/kmalloc.thy @@ -9,14 +9,14 @@ *) theory kmalloc -imports "../CTranslation" +imports "../CTranslation" "$L4V_ARCH/imports/MachineWords" begin (* no proof here, just testing the parser *) consts KMC :: word32 - ptr_retyps :: "nat \ word32 \ heap_typ_desc \ heap_typ_desc" + ptr_retyps :: "nat \ machine_word \ heap_typ_desc \ heap_typ_desc" install_C_file "kmalloc.c" diff --git a/tools/c-parser/testfiles/list_reverse.c b/tools/c-parser/testfiles/list_reverse.c index be8691824..911022b25 100644 --- a/tools/c-parser/testfiles/list_reverse.c +++ b/tools/c-parser/testfiles/list_reverse.c @@ -8,16 +8,16 @@ * @TAG(NICTA_BSD) */ -typedef unsigned int word_t; +typedef unsigned long word_t; /** FNSPEC reverse_spec: "\ \ \ (list zs \i)\<^bsup>sep\<^esup> \ - \ret__int :== PROC reverse(\i) - \ (list (rev zs) (Ptr (scast \ret__int)))\<^bsup>sep\<^esup> \" + \ret__long :== PROC reverse(\i) + \ (list (rev zs) (Ptr (scast \ret__long)))\<^bsup>sep\<^esup> \" */ -int reverse(word_t *i) +long reverse(word_t *i) { word_t j = 0; diff --git a/tools/c-parser/testfiles/list_reverse.thy b/tools/c-parser/testfiles/list_reverse.thy index 50f503710..04b4104ba 100644 --- a/tools/c-parser/testfiles/list_reverse.thy +++ b/tools/c-parser/testfiles/list_reverse.thy @@ -9,7 +9,7 @@ *) theory list_reverse -imports "../CTranslation" +imports "../CTranslation" "$L4V_ARCH/imports/MachineWords" begin declare hrs_simps [simp add] @@ -17,7 +17,7 @@ declare exists_left [simp add] declare sep_conj_ac [simp add] primrec - list :: "word32 list \ word32 ptr \ heap_state \ bool" + list :: "machine_word list \ machine_word ptr \ heap_state \ bool" where "list [] i = (\s. i=NULL \ \ s)" | "list (x#xs) i = (\s. i=Ptr x \ x\0 \ (\j. ((i \ j) \\<^sup>* list xs (Ptr j)) s))" diff --git a/tools/c-parser/testfiles/list_reverse_norm.c b/tools/c-parser/testfiles/list_reverse_norm.c index e304cebe2..1a471e4f5 100644 --- a/tools/c-parser/testfiles/list_reverse_norm.c +++ b/tools/c-parser/testfiles/list_reverse_norm.c @@ -8,13 +8,13 @@ * @TAG(NICTA_BSD) */ -typedef unsigned int word_t; +typedef unsigned long word_t; /** FNSPEC reverse_spec: "\ \ \ list (lift_t_c \) zs \i \ - \ret__unsigned :== PROC reverse(\i) - \ list (lift_t_c \) (rev zs) (Ptr \ret__unsigned) \" + \ret__unsigned_long :== PROC reverse(\i) + \ list (lift_t_c \) (rev zs) (Ptr \ret__unsigned_long) \" */ diff --git a/tools/c-parser/testfiles/list_reverse_norm.thy b/tools/c-parser/testfiles/list_reverse_norm.thy index ab02ce043..14e768024 100644 --- a/tools/c-parser/testfiles/list_reverse_norm.thy +++ b/tools/c-parser/testfiles/list_reverse_norm.thy @@ -9,14 +9,14 @@ *) theory list_reverse_norm -imports "../CTranslation" +imports "../CTranslation" "$L4V_ARCH/imports/MachineWords" begin declare sep_conj_ac [simp add] declare hrs_simps [simp add] primrec - list :: "word32 typ_heap \ word32 list \ word32 ptr \ bool" + list :: "machine_word typ_heap \ machine_word list \ machine_word ptr \ bool" where "list h [] i = (i = Ptr 0)" @@ -63,7 +63,7 @@ lemma in_list_Some: lemma in_list_valid [simp]: "\ list (lift_t_c (h,d)) xs p; ptr_val q \ set xs \ - \ d \\<^sub>t (q::word32 ptr)" + \ d \\<^sub>t (q::machine_word ptr)" by (auto dest: in_list_Some simp: lift_t_if split: if_split_asm) lemma list_restrict: diff --git a/tools/c-parser/umm_heap/FAKE64/Addr_Type.thy b/tools/c-parser/umm_heap/X64/Addr_Type.thy similarity index 100% rename from tools/c-parser/umm_heap/FAKE64/Addr_Type.thy rename to tools/c-parser/umm_heap/X64/Addr_Type.thy diff --git a/tools/c-parser/umm_heap/FAKE64/TargetNumbers.ML b/tools/c-parser/umm_heap/X64/TargetNumbers.ML similarity index 96% rename from tools/c-parser/umm_heap/FAKE64/TargetNumbers.ML rename to tools/c-parser/umm_heap/X64/TargetNumbers.ML index eee48ad09..33bb0e0e9 100644 --- a/tools/c-parser/umm_heap/FAKE64/TargetNumbers.ML +++ b/tools/c-parser/umm_heap/X64/TargetNumbers.ML @@ -26,10 +26,10 @@ val boolWidth = fromInt 8 val charWidth = 8 val shortWidth = 16 val intWidth = 32 -val longWidth = 32 +val longWidth = 64 val llongWidth = 64 val ptrWidth : int = 64 -val ptr_t = BaseCTypes.LongLong +val ptr_t = BaseCTypes.Long val CHAR_BIT : int = 8 fun umax width = exp(2, width) - 1 diff --git a/tools/c-parser/umm_heap/FAKE64/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy similarity index 100% rename from tools/c-parser/umm_heap/FAKE64/Word_Mem_Encoding.thy rename to tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy diff --git a/tools/haskell-translator/caseconvs b/tools/haskell-translator/caseconvs index 07d2bbd19..2ecb6cf78 100644 --- a/tools/haskell-translator/caseconvs +++ b/tools/haskell-translator/caseconvs @@ -896,6 +896,11 @@ case \x of (cap@PageCap { capVPIsDevice = isDevice }) -> (cap@PageTableCap { cap in ->5 else undefined +case \x of ArchObjectCap (frame@PageCap {capVPIsDevice = False}) -> _ -> ---> let cap = \x in + if isPageCap cap \ \ capVPIsDevice cap + then ->1 + else ->2 + case \x of (srcIndex:srcDepth:args, srcRootCap:_) | label < 4 -> (_, _) | label == 4 -> (_, _) | label == 5 -> (_, _) | label == 6 -> (_, _) | label == 7 -> (pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, pivotRootCap:srcRootCap:_) | label == 8 -> (_, _) | label > 8 -> _ -> ---> let (\v0\, \v1\) = \x in case (if label < 4 then 1 else if label = 4 then 2 @@ -1468,7 +1473,7 @@ case \x of (cap@PageCap {}) -> _ -> ---> let cap = \x in then ->1 else ->2 -case \x of (ArchInvocationLabel X64PDPTMap, vaddr':attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PageDirectoryMap, _, _) -> (ArchInvocationLabel X64PageDirectoryUnmap, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in +case \x of (ArchInvocationLabel X64PDPTMap, vaddr':attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PDPTMap, _, _) -> (ArchInvocationLabel X64PDPTUnmap, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in case (label, args, extraCaps) of (ArchInvocationLabel X64PDPTMap, vaddr'#attr#_, (vspaceCap,_)#_) => ->1 | (ArchInvocationLabel X64PageDirectoryMap, _, _) => ->2 @@ -1568,6 +1573,20 @@ case \x of (ArchInvocationLabel X64PageMap, vaddr:rightsMask:attr:_, (vspaceCap, | (ArchInvocationLabel X64PageGetAddress, _, _) => ->7 | _ => ->8 +case \x of (ArchInvocationLabel X64IOPageTableMap, ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64IOPageTableMap, _, _) -> (ArchInvocationLabel X64IOPageTableUnmap, _, _) -> _ -> ---> let (ilabel, args, extraCaps) = \x in + case (ilabel, args, extraCaps) of + (ArchInvocationLabel X64IOPageTableMap, ioaddr#_, (iospaceCap,_)#_) => ->1 + | (ArchInvocationLabel X64IOPageTableMap, _, _) => ->2 + | (ArchInvocationLabel X64IOPageTableUnmap, _, _) => ->3 + | _ => ->4 + +case \x of (ArchInvocationLabel X64PageMapIO, rw:ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64PageMapIO, _, _) -> (ArchInvocationLabel X64PageUnmap, _, _) -> _ -> ---> let (ilabel, args, extraCaps) = \x in + case (ilabel, args, extraCaps) of + (ArchInvocationLabel X64PageMapIO, rw:ioaddr#_, (iospaceCap,_)#_) => ->1 + | (ArchInvocationLabel X64PageMapIO, _, _) => ->2 + | (ArchInvocationLabel X64PageUnmap, _, _) => ->3 + | _ => ->4 + case \x of cap@(PDPointerTableCap {}) -> _ -> ---> let cap = \x in if isPDPointerTableCap cap then ->1 @@ -1607,13 +1626,41 @@ case \x of cap@(PageCap {}) -> cap@(PDPointerTableCap {}) -> cap@(PageDirectoryC then ->8 else ->9 -case \x of (ArchInvocationLabel X64PDPTMap, vaddr':attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PDPTMap, _, _) -> (ArchInvocationLabel X64PDPTUnmap, _, _) -> _ -> ---X> - - -case \x of ArchObjectCap (frame@PageCap {capVPIsDevice = False}) -> _ -> ---X> +case \x of cap@(IOPageTableCap {}) -> _ -> ---> let cap = \x in + if isIOPageTableCap + then ->1 + else ->2 case \x of (cap@UntypedCap {}) -> _ -> ---> let cap = \x in if isUntypedCap cap then ->1 else ->2 +case \x of cap@(PageCap {}) -> _ -> ---> let cap = \x in + if isPageCap cap + then ->1 + else ->2 + +case \x of (PageMap asid cap ctSlot entries) -> (PageRemap entries) -> (PageUnmap cap ctSlot) -> (PageIOMap cap cptr vtdpte slot) -> (PageIOUnmap (ArchObjectCap cap@PageCap {}) ctSlot) -> (PageIOUnmap _ _) -> (PageGetAddr ptr) -> ---> let \v0\ = \x in + case \v0\ of + PageMap asid cap ct ctSlot entries => ->1 + | PageRemap entries => ->2 + | PageUnmap cap ctSlot => ->3 + | PageIOMap cap cptr ctdpte slot => ->4 + | PageIOUnmap (ArchObjectCap cap) ctSlot => + if isPageCap cap + then ->5 + else ->6 + | PageIOUnmap _ _ => ->6 + | PageGetAddr ptr => ->7 + +case \x of UntypedCap {} | capBlockSize untyped == objBits pool -> _ -> ---> let \v0\ = \x in + if isUntypedCap \v0\ \ capBlockSize \v0\ == objBits pool + then ->1 + else ->2 + +case \x of (cap@IOPageTableCap {}) -> _ -> ---> let cap = \x in + if isIOPageTableCap cap + then ->1 + else ->2 + diff --git a/tools/haskell-translator/make_spec.sh b/tools/haskell-translator/make_spec.sh index da12b608c..e0b1ce99d 100755 --- a/tools/haskell-translator/make_spec.sh +++ b/tools/haskell-translator/make_spec.sh @@ -74,7 +74,7 @@ then (cd $L4CAP && git status --short) >> $SPEC/version fi -ARCHES=("ARM") +ARCHES=("ARM" "X64") NAMES=`cd $SKEL; ls *.thy` diff --git a/tools/tests.xml b/tools/tests.xml index 7f672ade9..20d519311 100644 --- a/tools/tests.xml +++ b/tools/tests.xml @@ -23,6 +23,7 @@ ../../isabelle/bin/isabelle env make -f IsaMakefile CParser ../../isabelle/bin/isabelle env make -f IsaMakefile cparser_test + L4V_ARCH=X64 ../../isabelle/bin/isabelle env make -f IsaMakefile cparser_test ../../isabelle/bin/isabelle env make -f IsaMakefile cparser_tools