From 2f4b822da9b85128710bb538a9ae84fa579a083a Mon Sep 17 00:00:00 2001 From: Matthew Brecknell Date: Thu, 22 Jun 2017 17:10:23 +1000 Subject: [PATCH] x64: configure arch-specific array types --- lib/LemmaBucket_C.thy | 8 +- lib/TypHeapLib.thy | 2 +- proof/asmrefine/SEL4GlobalsSwap.thy | 6 +- proof/crefine/Retype_C.thy | 2 +- tools/autocorres/HeapLift.thy | 40 +-- .../tests/proof-tests/nested_struct.thy | 6 +- tools/c-parser/CTranslation.thy | 1 + tools/c-parser/PackedTypes.thy | 17 +- tools/c-parser/UMM_Proofs.ML | 20 +- tools/c-parser/X64/calculate_state_arch.ML | 21 ++ tools/c-parser/calculate_state.ML | 6 +- tools/c-parser/umm_heap/ArrayAssertion.thy | 2 +- tools/c-parser/umm_heap/ArraysMemInstance.thy | 307 +----------------- tools/c-parser/umm_heap/TypHeap.thy | 2 +- .../umm_heap/X64/ArchArraysMemInstance.thy | 265 +++++++++++++++ 15 files changed, 342 insertions(+), 363 deletions(-) create mode 100644 tools/c-parser/X64/calculate_state_arch.ML create mode 100644 tools/c-parser/umm_heap/X64/ArchArraysMemInstance.thy diff --git a/lib/LemmaBucket_C.thy b/lib/LemmaBucket_C.thy index cb42e8ed4..1f844c786 100644 --- a/lib/LemmaBucket_C.thy +++ b/lib/LemmaBucket_C.thy @@ -845,15 +845,15 @@ lemma heap_update_Array_element'': lemmas heap_update_Array_element' = heap_update_Array_element''[simplified array_ptr_index_simps] -lemma fourthousand_size: - "CARD('b :: fourthousand_count) * size_of TYPE('a :: oneMB_size) < 2 ^ 32" - using oneMB_size_ax[where 'a='a] fourthousand_count_ax[where 'a='b] +lemma array_count_size: + "CARD('b :: array_max_count) * size_of TYPE('a :: array_outer_max_size) < 2 ^ 32" + using array_outer_max_size_ax[where 'a='a] array_max_count_ax[where 'a='b] apply (clarsimp dest!: nat_le_Suc_less_imp) apply (drule(1) mult_mono, simp+) done lemmas heap_update_Array_element - = heap_update_Array_element'[OF refl _ fourthousand_size] + = heap_update_Array_element'[OF refl _ array_count_size] lemma typ_slice_list_cut: "\ (\x \ set xs. size_td (dt_fst x) = m); m \ 0; n < (length xs * m) \ diff --git a/lib/TypHeapLib.thy b/lib/TypHeapLib.thy index 1b708ad0e..255a7ff01 100644 --- a/lib/TypHeapLib.thy +++ b/lib/TypHeapLib.thy @@ -412,7 +412,7 @@ lemma c_guard_array_c_guard: lemma c_guard_array_field: assumes parent_cguard: "c_guard (p :: 'a :: mem_type ptr)" and subfield: "field_ti TYPE('a :: mem_type) f = Some t" - and type_match: "export_uinfo t = export_uinfo (typ_info_t TYPE(('b :: oneMB_size, 'c :: fourthousand_count) array))" + and type_match: "export_uinfo t = export_uinfo (typ_info_t TYPE(('b :: array_outer_max_size, 'c :: array_max_count) array))" shows "c_guard (Ptr &(p\f) :: 'b ptr)" by (metis c_guard_array_c_guard c_guard_field parent_cguard ptr_coerce.simps subfield type_match) diff --git a/proof/asmrefine/SEL4GlobalsSwap.thy b/proof/asmrefine/SEL4GlobalsSwap.thy index b0bf6f462..b8e208882 100644 --- a/proof/asmrefine/SEL4GlobalsSwap.thy +++ b/proof/asmrefine/SEL4GlobalsSwap.thy @@ -32,9 +32,9 @@ lemma globals_update_eq_iff: apply (rule state.fold_congs, simp+) done -instance ptr :: (c_type)oneMB_packed .. -instance tcb_queue_C :: oneMB_packed .. -instance region_C :: oneMB_packed .. +instance ptr :: (c_type)array_outer_packed .. +instance tcb_queue_C :: array_outer_packed .. +instance region_C :: array_outer_packed .. locale graph_refine_locale = kernel_all_substitute + assumes globals_list_distinct: diff --git a/proof/crefine/Retype_C.thy b/proof/crefine/Retype_C.thy index e145f12e3..34a2a646d 100644 --- a/proof/crefine/Retype_C.thy +++ b/proof/crefine/Retype_C.thy @@ -17,7 +17,7 @@ begin declare word_neq_0_conv [simp del] -instance cte_C :: oneMB_size +instance cte_C :: array_outer_max_size by intro_classes simp context begin interpretation Arch . (*FIXME: arch_split*) diff --git a/tools/autocorres/HeapLift.thy b/tools/autocorres/HeapLift.thy index 6c29a4811..3e84f46b1 100644 --- a/tools/autocorres/HeapLift.thy +++ b/tools/autocorres/HeapLift.thy @@ -674,11 +674,11 @@ lemma struct_rewrite_guard_c_guard_field [heap_abs]: (\s. c_guard (Ptr (field_lvalue (p s :: 'a ptr) field_name) :: 'f ptr))" by (simp add: valid_struct_field_def struct_rewrite_expr_def struct_rewrite_guard_def) -lemma align_of_array: "align_of TYPE(('a :: oneMB_size)['b' :: fourthousand_count]) = align_of TYPE('a)" +lemma align_of_array: "align_of TYPE(('a :: array_outer_max_size)['b' :: array_max_count]) = align_of TYPE('a)" by (simp add: align_of_def align_td_array) lemma c_guard_array: - "\ 0 \ k; nat k < CARD('b); c_guard (p :: (('a::oneMB_size)['b::fourthousand_count]) ptr) \ + "\ 0 \ k; nat k < CARD('b); c_guard (p :: (('a::array_outer_max_size)['b::array_max_count]) ptr) \ \ c_guard (ptr_coerce p +\<^sub>p k :: 'a ptr)" apply (clarsimp simp: ptr_add_def c_guard_def c_null_guard_def) apply (rule conjI[rotated]) @@ -698,7 +698,7 @@ lemma c_guard_array: done lemma struct_rewrite_guard_c_guard_Array_field [heap_abs]: - "\ valid_struct_field st field_name (field_getter :: ('a :: packed_type) \ ('f::oneMB_packed ['n::fourthousand_count])) field_setter t_hrs t_hrs_update; + "\ valid_struct_field st field_name (field_getter :: ('a :: packed_type) \ ('f::array_outer_packed ['n::array_max_count])) field_setter t_hrs t_hrs_update; struct_rewrite_expr P p' p; struct_rewrite_guard Q (\s. c_guard (p' s)) \ \ struct_rewrite_guard (\s. P s \ Q s \ 0 \ k \ nat k < CARD('n)) @@ -764,7 +764,7 @@ lemma struct_rewrite_expr_field [heap_abs]: (* Descend into struct fields that are themselves arrays. *) lemma struct_rewrite_expr_Array_field [heap_abs]: "\ valid_struct_field st field_name - (field_getter :: ('a :: packed_type) \ 'f::oneMB_packed ['n::fourthousand_count]) + (field_getter :: ('a :: packed_type) \ 'f::array_outer_packed ['n::array_max_count]) field_setter t_hrs t_hrs_update; struct_rewrite_expr P p' p; struct_rewrite_expr Q a (\s. h_val (hrs_mem (t_hrs s)) (p' s)) \ @@ -819,9 +819,9 @@ lemma heap_update_field_unpacked: (* \ heap_update_Array_element. Would want this for struct_rewrite_modifies_Array_field. *) lemma heap_update_Array_element_unpacked: - "n < CARD('b::fourthousand_count) \ + "n < CARD('b::array_max_count) \ heap_update (ptr_coerce p' +\<^sub>p int n) w hp = - heap_update (p'::('a::oneMB_size['b::fourthousand_count]) ptr) + heap_update (p'::('a::array_outer_max_size['b::array_max_count]) ptr) (Arrays.update (h_val hp p') n w) hp" oops @@ -918,7 +918,7 @@ lemma struct_rewrite_modifies_field__unused: done lemma struct_rewrite_modifies_Array_field__unused: - "\ valid_struct_field (st :: 's \ 't) field_name (field_getter :: ('a::packed_type) \ (('f::oneMB_packed)['n::fourthousand_count])) field_setter t_hrs t_hrs_update; + "\ valid_struct_field (st :: 's \ 't) field_name (field_getter :: ('a::packed_type) \ (('f::array_outer_packed)['n::array_max_count])) field_setter t_hrs t_hrs_update; struct_rewrite_expr P p' p; struct_rewrite_expr Q f' f; struct_rewrite_modifies R @@ -1021,7 +1021,7 @@ lemma struct_rewrite_modifies_field [heap_abs]: (* FIXME: this is nearly a duplicate. Would a standalone array rule work instead? *) lemma struct_rewrite_modifies_Array_field [heap_abs]: - "\ valid_struct_field (st :: 's \ 't) field_name (field_getter :: ('a::packed_type) \ (('f::oneMB_packed)['n::fourthousand_count])) field_setter t_hrs t_hrs_update; + "\ valid_struct_field (st :: 's \ 't) field_name (field_getter :: ('a::packed_type) \ (('f::array_outer_packed)['n::array_max_count])) field_setter t_hrs t_hrs_update; struct_rewrite_expr P p' p; struct_rewrite_expr Q f' f; \s. heap_lift__wrap_h_val (h_val_p' s) (h_val (hrs_mem (t_hrs s)) (p' s)); @@ -1385,7 +1385,7 @@ lemma heap_abs_expr_c_guard_array [heap_abs]: abs_expr st P x' (\s. ptr_coerce (x s) :: 'a ptr) \ \ abs_guard st (\s. P s \ (\a \ set (array_addrs (x' s) CARD('b)). vgetter s a)) - (\s. c_guard (x s :: ('a::oneMB_size, 'b::fourthousand_count) array ptr))" + (\s. c_guard (x s :: ('a::array_outer_max_size, 'b::array_max_count) array ptr))" apply (clarsimp simp: abs_expr_def abs_guard_def simple_lift_def heap_ptr_valid_def) apply (subgoal_tac "\a\set (array_addrs (x' (st s)) CARD('b)). c_guard a") apply (erule allE, erule (1) impE) @@ -1521,9 +1521,9 @@ lemma concat_nth_chunk: done lemma array_update_split: - "\ valid_typ_heap st (getter :: 's \ ('a::oneMB_size) ptr \ 'a) setter + "\ valid_typ_heap st (getter :: 's \ ('a::array_outer_max_size) ptr \ 'a) setter vgetter vsetter t_hrs t_hrs_update; - \x \ set (array_addrs (ptr_coerce p) CARD('b::fourthousand_count)). + \x \ set (array_addrs (ptr_coerce p) CARD('b::array_max_count)). vgetter (st s) x \ \ st (t_hrs_update (hrs_mem_update (heap_update p (arr :: 'a['b]))) s) = fold (\i. setter (\x. x(ptr_coerce p +\<^sub>p int i := index arr i))) @@ -1561,7 +1561,7 @@ lemma array_update_split: apply simp (* remove false dependency *) - apply (subst fold_heap_update_list[OF fourthousand_size]) + apply (subst fold_heap_update_list[OF array_count_size]) apply (rule fold_cong[OF refl refl]) apply (clarsimp simp: ptr_add_def) @@ -1620,10 +1620,10 @@ lemma fold_update_id: apply simp done -lemma fourthousand_index: - "\ i < CARD('b::fourthousand_count); j < CARD('b) \ +lemma array_count_index: + "\ i < CARD('b::array_max_count); j < CARD('b) \ \ (i = j) = - ((of_nat (i * size_of TYPE('a::oneMB_size)) :: word32) + ((of_nat (i * size_of TYPE('a::array_outer_max_size)) :: word32) = of_nat (j * size_of TYPE('a)))" apply (rule_tac t = "i = j" and s = "i * size_of TYPE('a) = j * size_of TYPE('a)" in subst) apply clarsimp @@ -1635,7 +1635,7 @@ lemma fourthousand_index: rule less_trans, erule_tac b = "CARD('b)" in mult_strict_right_mono, rule sz_nzero, - rule fourthousand_size)+ + rule array_count_size)+ done (* end machinery for heap_abs_array_update *) @@ -1652,7 +1652,7 @@ theorem heap_abs_array_update [heap_abs]: (\s. setter (\v. v(ptr_coerce (b' s) +\<^sub>p int (n' s) := v' s)) s) (\s. t_hrs_update (hrs_mem_update ( heap_update (b s) (Arrays.update ((h_val (hrs_mem (t_hrs s)) (b s)) - :: ('a::oneMB_size)['b::fourthousand_count]) (n s) (v s)))) s)" + :: ('a::array_outer_max_size)['b::array_max_count]) (n s) (v s)))) s)" apply (clarsimp simp: abs_modifies_def abs_expr_def) (* rewrite heap_update of array *) apply (subst array_update_split @@ -1687,7 +1687,7 @@ theorem heap_abs_array_update [heap_abs]: apply assumption apply (clarsimp simp: ptr_add_def) apply (subst of_nat_mult[symmetric])+ - apply (rule fourthousand_index) + apply (rule array_count_index) apply (erule less_trans, assumption)+ apply clarsimp @@ -1696,7 +1696,7 @@ theorem heap_abs_array_update [heap_abs]: apply assumption apply (clarsimp simp: ptr_add_def) apply (subst of_nat_mult[symmetric])+ - apply (erule fourthousand_index) + apply (erule array_count_index) apply assumption apply clarsimp (* index n is disjoint *) @@ -1705,7 +1705,7 @@ theorem heap_abs_array_update [heap_abs]: apply (clarsimp simp: ptr_add_def) apply (subgoal_tac "of_nat (i * size_of TYPE('a)) \ of_nat (n s * size_of TYPE('a))") apply force - apply (subst fourthousand_index[symmetric]) + apply (subst array_count_index[symmetric]) apply assumption apply simp apply simp diff --git a/tools/autocorres/tests/proof-tests/nested_struct.thy b/tools/autocorres/tests/proof-tests/nested_struct.thy index 839cb4bd6..0a6f514c8 100644 --- a/tools/autocorres/tests/proof-tests/nested_struct.thy +++ b/tools/autocorres/tests/proof-tests/nested_struct.thy @@ -16,8 +16,8 @@ theory nested_struct imports "../../AutoCorres" begin install_C_file "nested_struct.c" (* Nested struct translation currently only works for packed_type types. *) -instance s1_C :: oneMB_packed by intro_classes auto -instance s3_C :: oneMB_packed by intro_classes auto +instance s1_C :: array_outer_packed by intro_classes auto +instance s3_C :: array_outer_packed by intro_classes auto autocorres "nested_struct.c" context nested_struct begin @@ -57,4 +57,4 @@ lemma "\ \h. is_valid_s4_C h s \ end -end \ No newline at end of file +end diff --git a/tools/c-parser/CTranslation.thy b/tools/c-parser/CTranslation.thy index 8b0e6be4f..74d8a6b0e 100644 --- a/tools/c-parser/CTranslation.thy +++ b/tools/c-parser/CTranslation.thy @@ -114,6 +114,7 @@ ML_file "program_analysis.ML" ML_file "heapstatetype.ML" ML_file "MemoryModelExtras-sig.ML" ML_file "MemoryModelExtras.ML" +ML_file "$L4V_ARCH/calculate_state_arch.ML" ML_file "calculate_state.ML" ML_file "syntax_transforms.ML" ML_file "expression_translation.ML" diff --git a/tools/c-parser/PackedTypes.thy b/tools/c-parser/PackedTypes.thy index 5b24d95c3..b65f72261 100644 --- a/tools/c-parser/PackedTypes.thy +++ b/tools/c-parser/PackedTypes.thy @@ -656,22 +656,19 @@ end text {* Arrays of packed types are in turn packed *} -class oneMB_packed = packed_type + oneMB_size -class twoToSix_packed = oneMB_packed + twoToSix_size +class array_outer_packed = packed_type + array_outer_max_size +class array_inner_packed = array_outer_packed + array_inner_max_size -instance word :: (len8)oneMB_packed .. -instance word :: (len8)twoToSix_packed .. +instance word :: (len8)array_outer_packed .. +instance word :: (len8)array_inner_packed .. -instantiation array :: (oneMB_packed, fourthousand_count) packed_type -begin -instance - apply(intro_classes) +instance array :: (array_outer_packed, array_max_count) packed_type + apply(intro_classes) apply (simp add: td_fafu_idem_intro_simps) apply (simp add: td_fa_hi_intro_simps) done -end -instance array :: (twoToSix_packed, fourthousand_count) oneMB_packed .. +instance array :: (array_inner_packed, array_max_count) array_outer_packed .. section {* Theorems about packed types *} diff --git a/tools/c-parser/UMM_Proofs.ML b/tools/c-parser/UMM_Proofs.ML index 70f073cb1..8109a1a9a 100644 --- a/tools/c-parser/UMM_Proofs.ML +++ b/tools/c-parser/UMM_Proofs.ML @@ -596,7 +596,7 @@ end (* prove that the new type is an instance of the class finite *) - (* prove that the new type is an instance of the class fourthousand_count *) + (* prove that the new type is an instance of the class array_max_count *) fun umm_array_calculation el_ty n st thy = let val _ = Feedback.informStr (0, "Proving that an array of "^Int.toString n^" "^ Syntax.string_of_typ (thy2ctxt thy) el_ty ^" is a mem_type") @@ -611,19 +611,19 @@ fun umm_array_calculation el_ty n st thy = let This is done exploiting the fact that we have the following instance in our context already - instance array :: (oneMB_size, fourthousand_count) mem_type + instance array :: (array_outer_max_size, array_max_count) mem_type - Thanks to the neat instance declarations in ArraysMemInstance.thy - (all those classes with names lt), the fourthousand_count for + Thanks to the neat instance declarations in ArchArraysMemInstance.thy + (all those classes with names lt), the array_max_count for the array size will be handled automatically by type-checking. This means that we just need to do one independent instance proofs, - for el_ty :: oneMB_size + for el_ty :: array_outer_max_size Even that may be done automatically, for certain element types. For example all the word types have this happen through - instance word :: (len8) oneMB_size + instance word :: (len8) array_outer_max_size instance word_length8 :: len8 instance word_length16 :: len8 instance word_length32 :: len8 @@ -633,7 +633,7 @@ fun umm_array_calculation el_ty n st thy = let Arrays get to use the - instance array :: (twoToSix_size, fourthousand_count) oneMB_size + instance array :: (array_inner_max_size, array_max_count) array_outer_max_size information. @@ -647,7 +647,7 @@ in val (st,thy) = case args of [] => (* will be a record type *) - prove_type_in_szclass (st, thy) el_ty "ArraysMemInstance.oneMB_size" + prove_type_in_szclass (st, thy) el_ty "ArchArraysMemInstance.array_outer_max_size" | [_] => (* can compute sizes for words and ptrs *) if tyname = @{type_name "Word.word"} then (st, thy) else if tyname = @{type_name "CTypesBase.ptr"} then (st, thy) @@ -655,12 +655,12 @@ in | [a,_] => let val _ = tyname = @{type_name "array"} orelse error "Binary type operator is not array." - (* a is an element type and must be in twoToSix_size *) + (* a is an element type and must be in array_inner_max_size *) val (atyname, aargs) = case a of Type p => p | _ => error "Array eltype is not Type" in case aargs of - [] => prove_type_in_szclass (st,thy) a "ArraysMemInstance.twoToSix_size" + [] => prove_type_in_szclass (st,thy) a "ArchArraysMemInstance.array_inner_max_size" | [_] => if atyname = @{type_name "word"} orelse atyname = @{type_name "ptr"} then (st, thy) diff --git a/tools/c-parser/X64/calculate_state_arch.ML b/tools/c-parser/X64/calculate_state_arch.ML new file mode 100644 index 000000000..5cc27a689 --- /dev/null +++ b/tools/c-parser/X64/calculate_state_arch.ML @@ -0,0 +1,21 @@ +(* + * Copyright 2017, Data61, CSIRO + * + * 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(DATA61_BSD) + *) + +signature CALCULATE_STATE_ARCH = sig + val mk_array_size_type : int -> typ +end; + +structure CalculateStateArch : CALCULATE_STATE_ARCH = struct + open TermsTypes + fun mk_array_size_type sz = + if sz = 1048576 + then @{typ "ty1048576"} + else mk_numeral_type sz +end diff --git a/tools/c-parser/calculate_state.ML b/tools/c-parser/calculate_state.ML index 1a83b9088..f61dbe4fa 100644 --- a/tools/c-parser/calculate_state.ML +++ b/tools/c-parser/calculate_state.ML @@ -227,6 +227,7 @@ in end fun isa_type_to_typ ctxt (ity : isa_type) = let + open CalculateStateArch fun m s = let val thy = Proof_Context.theory_of ctxt val known = (Syntax.parse_typ ctxt s; true) handle ERROR _ => false @@ -234,16 +235,13 @@ fun isa_type_to_typ ctxt (ity : isa_type) = let in f s end - fun mk_numeral_type' sz = - if sz = 8192 then @{typ "ty8192"} - else mk_numeral_type sz in case ity of refty (NONE, _) => mk_ptr_ty unit | refty (SOME ity0, _) => mk_ptr_ty (isa_type_to_typ ctxt ity0) | recd (s, _) => Type (m s, []) | array (ity, sz, _) => - Type("Arrays.array", [isa_type_to_typ ctxt ity, mk_numeral_type' sz]) + Type("Arrays.array", [isa_type_to_typ ctxt ity, mk_array_size_type sz]) | existing (ty, _) => ty end diff --git a/tools/c-parser/umm_heap/ArrayAssertion.thy b/tools/c-parser/umm_heap/ArrayAssertion.thy index bdb364a5c..acfa5b7a2 100644 --- a/tools/c-parser/umm_heap/ArrayAssertion.thy +++ b/tools/c-parser/umm_heap/ArrayAssertion.thy @@ -13,7 +13,7 @@ theory ArrayAssertion imports - "ArraysMemInstance" + "$L4V_ARCH/ArchArraysMemInstance" "StructSupport" begin diff --git a/tools/c-parser/umm_heap/ArraysMemInstance.thy b/tools/c-parser/umm_heap/ArraysMemInstance.thy index 404f3b4ce..69c8ce3df 100644 --- a/tools/c-parser/umm_heap/ArraysMemInstance.thy +++ b/tools/c-parser/umm_heap/ArraysMemInstance.thy @@ -28,10 +28,7 @@ definition array_tag :: "('a::c_type,'b::finite) array itself \ ('a,'b) array typ_info" where "array_tag t \ array_tag_n (CARD('b))" -instantiation array :: (c_type,finite) c_type -begin -instance .. -end +instance array :: (c_type,finite) c_type .. overloading typ_info_array \ typ_info_t begin definition @@ -205,10 +202,7 @@ apply(subgoal_tac "align_of TYPE('a) dvd size_of TYPE('a)") apply(rule align_size_of) done -instantiation array :: (mem_type,finite) mem_type_sans_size -begin - -instance +instance array :: (mem_type,finite) mem_type_sans_size apply intro_classes apply(simp_all add: typ_info_array array_tag_def size_of_def norm_bytes_def) @@ -229,8 +223,6 @@ apply(rule dvd_trans) apply(simp add: size_of_def) done -end - declare atn_base [simp del] declare atn_rec [simp del] @@ -249,299 +241,4 @@ apply(subst align_td_array_tag) apply simp+ done -(* Showing arrays are in mem_type requires maximum sizes for objects, - and maximum counts for elements *) -class oneMB_size = mem_type + - assumes oneMB_size_ax: "size_of TYPE('a::c_type) < 2 ^ 19" - -class fourthousand_count = finite + - assumes fourthousand_count_ax: "CARD ('a) <= 2 ^ 13" - -instantiation array :: (oneMB_size, fourthousand_count) mem_type -begin - -instance -apply intro_classes -apply simp -apply (subgoal_tac "addr_card = 2 ^ (addr_bitsize - 19) * 2 ^ 19") - apply (erule ssubst) - apply (rule less_le_trans[where y = "card (UNIV::'b set) * 2 ^ 19"]) - apply (rule mult_less_mono2) - apply (rule oneMB_size_ax) - apply simp - apply (rule mult_le_mono1) - apply (rule le_trans[where j = "2 ^ 13"]) - apply (rule fourthousand_count_ax) - apply simp - apply simp -apply (simp add: addr_card) -done - -end - -class twoToSix_size = oneMB_size + - assumes twoToSix_size_ax: "size_of TYPE('a::c_type) < 2 ^ 6" - -instantiation array :: (twoToSix_size, fourthousand_count) oneMB_size -begin - -instance -apply intro_classes -apply simp - apply (rule order_less_le_trans) - apply (rule mult_le_less_imp_less) - apply (rule fourthousand_count_ax) - apply (rule twoToSix_size_ax) - apply simp - apply simp - apply simp - done - -end - -instantiation word :: (len8) oneMB_size -begin -instance -apply intro_classes -apply(simp add: size_of_def) -apply(subgoal_tac "len_of TYPE('a) \ 128") - apply simp -apply(rule len8_width) -done -end - -instantiation word :: (len8) twoToSix_size -begin -instance -apply intro_classes -apply(simp add: size_of_def) -apply(subgoal_tac "len_of TYPE('a) \ 128") - apply simp -apply(rule len8_width) -done -end - -instantiation ptr :: (c_type) oneMB_size -begin -instance -apply intro_classes -apply (simp add: size_of_def) -done -end - -instantiation ptr :: (c_type) twoToSix_size -begin -instance -apply intro_classes -apply (simp add: size_of_def) -done -end - -class lt12 = finite + - assumes lt12_ax: "CARD ('a) < 2 ^ 12" -class lt11 = lt12 + - assumes lt11_ax: "CARD ('a) < 2 ^ 11" -class lt10 = lt11 + - assumes lt10_ax: "CARD ('a) < 2 ^ 10" -class lt9 = lt10 + - assumes lt9_ax: "CARD ('a) < 2 ^ 9" -class lt8 = lt9 + - assumes lt8_ax: "CARD ('a) < 2 ^ 8" -class lt7 = lt8 + - assumes lt7_ax: "CARD ('a) < 2 ^ 7" -class lt6 = lt7 + - assumes lt6_ax: "CARD ('a) < 2 ^ 6" -class lt5 = lt6 + - assumes lt5_ax: "CARD ('a) < 2 ^ 5" -class lt4 = lt5 + - assumes lt4_ax: "CARD ('a) < 2 ^ 4" -class lt3 = lt4 + - assumes lt3_ax: "CARD ('a) < 2 ^ 3" -class lt2 = lt3 + - assumes lt2_ax: "CARD ('a) < 2 ^ 2" -class lt1 = lt2 + - assumes lt1_ax: "CARD ('a) < 2 ^ 1" - -instantiation bit0 :: (lt12) fourthousand_count -begin -instance - by (intro_classes, insert lt12_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt12) fourthousand_count -begin -instance - by (intro_classes, insert lt12_ax[where 'a = 'a], simp) -end - -instantiation bit0 :: (lt11) lt12 -begin -instance - by (intro_classes, insert lt11_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt11) lt12 -begin -instance - by (intro_classes, insert lt11_ax[where 'a = 'a], simp) -end - -instantiation bit0 :: (lt10) lt11 -begin -instance - by (intro_classes, insert lt10_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt10) lt11 -begin -instance - by (intro_classes, insert lt10_ax[where 'a = 'a], simp) -end - -instantiation bit0 :: (lt9) lt10 -begin -instance - by (intro_classes, insert lt9_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt9) lt10 -begin -instance - by (intro_classes, insert lt9_ax[where 'a = 'a], simp) -end - -instantiation bit0 :: (lt8) lt9 -begin -instance - by (intro_classes, insert lt8_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt8) lt9 -begin -instance - by (intro_classes, insert lt8_ax[where 'a = 'a], simp) -end - -instantiation bit0 :: (lt7) lt8 -begin -instance - by (intro_classes, insert lt7_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt7) lt8 -begin -instance - by (intro_classes, insert lt7_ax[where 'a = 'a], simp) -end - -instantiation bit0 :: (lt6) lt7 -begin -instance - by (intro_classes, insert lt6_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt6) lt7 -begin -instance - by (intro_classes, insert lt6_ax[where 'a = 'a], simp) -end - -instantiation bit0 :: (lt5) lt6 -begin -instance - by (intro_classes, insert lt5_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt5) lt6 -begin -instance - by (intro_classes, insert lt5_ax[where 'a = 'a], simp) -end - -instantiation bit0 :: (lt4) lt5 -begin -instance - by (intro_classes, insert lt4_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt4) lt5 -begin -instance - by (intro_classes, insert lt4_ax[where 'a = 'a], simp) -end - -instantiation bit0 :: (lt3) lt4 -begin -instance - by (intro_classes, insert lt3_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt3) lt4 -begin -instance - by (intro_classes, insert lt3_ax[where 'a = 'a], simp) -end - -instantiation bit0 :: (lt2) lt3 -begin -instance - by (intro_classes, insert lt2_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt2) lt3 -begin -instance - by (intro_classes, insert lt2_ax[where 'a = 'a], simp) -end - -instantiation bit0 :: (lt1) lt2 -begin -instance - by (intro_classes, insert lt1_ax[where 'a = 'a], simp) -end - -instantiation bit1 :: (lt1) lt2 -begin -instance - by (intro_classes, insert lt1_ax[where 'a = 'a], simp) -end - -instantiation num1 :: lt1 -begin -instance - by (intro_classes, simp_all) -end - -(* don't understand why this also seems to be necessary *) -instantiation num1 :: fourthousand_count -begin -instance - by (intro_classes, simp) -end - -(* introduce hackish handling of 8192 type by making a copy of the type - under a constructor, and then manually showing that it is an instance of - fourthousand_count *) -datatype ty8192 = ty8192 "8192" - -lemma univ8192: "(UNIV::ty8192 set) = image ty8192 (UNIV::8192 set)" -apply (simp add: set_eq_iff image_iff) -apply (rule_tac allI) -apply (rule_tac ty8192.induct) -apply simp -done - -instance "ty8192" :: finite -apply intro_classes -apply (simp add: univ8192) -done - -lemma card8192[simp]: "CARD(ty8192) = CARD(8192)" -apply (simp add: univ8192 card_image inj_on_def) -done - -instance "ty8192" :: fourthousand_count -by intro_classes simp - - end diff --git a/tools/c-parser/umm_heap/TypHeap.thy b/tools/c-parser/umm_heap/TypHeap.thy index 943d46676..cbb23314f 100644 --- a/tools/c-parser/umm_heap/TypHeap.thy +++ b/tools/c-parser/umm_heap/TypHeap.thy @@ -13,7 +13,7 @@ theory TypHeap imports Vanilla32 - ArraysMemInstance + "$L4V_ARCH/ArchArraysMemInstance" HeapRawState MapExtraTrans begin diff --git a/tools/c-parser/umm_heap/X64/ArchArraysMemInstance.thy b/tools/c-parser/umm_heap/X64/ArchArraysMemInstance.thy new file mode 100644 index 000000000..19e4c0fcc --- /dev/null +++ b/tools/c-parser/umm_heap/X64/ArchArraysMemInstance.thy @@ -0,0 +1,265 @@ +(* + * Copyright 2017, 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 ArchArraysMemInstance +imports "../ArraysMemInstance" +begin + +(* Showing arrays are in mem_type requires maximum sizes for objects, + and maximum counts for elements *) +class array_outer_max_size = mem_type + + assumes array_outer_max_size_ax: "size_of TYPE('a::c_type) < 2 ^ 26" + +class array_max_count = finite + + assumes array_max_count_ax: "CARD ('a) <= 2 ^ 20" + +instance array :: (array_outer_max_size, array_max_count) mem_type +apply intro_classes +apply simp +apply (subgoal_tac "addr_card = 2 ^ (addr_bitsize - 26) * 2 ^ 26") + apply (erule ssubst) + apply (rule less_le_trans[where y = "card (UNIV::'b set) * 2 ^ 26"]) + apply (rule mult_less_mono2) + apply (rule array_outer_max_size_ax) + apply simp + apply (rule mult_le_mono1) + apply (rule le_trans[where j = "2 ^ 20"]) + apply (rule array_max_count_ax) + apply simp + apply simp +apply (simp add: addr_card) +done + +class array_inner_max_size = array_outer_max_size + + assumes array_inner_max_size_ax: "size_of TYPE('a::c_type) < 2 ^ 6" + +instance array :: (array_inner_max_size, array_max_count) array_outer_max_size +apply intro_classes +apply simp + apply (rule order_less_le_trans) + apply (rule mult_le_less_imp_less) + apply (rule array_max_count_ax) + apply (rule array_inner_max_size_ax) + apply simp + apply simp + apply simp + done + +instance word :: (len8) array_outer_max_size +apply intro_classes +apply(simp add: size_of_def) +apply(subgoal_tac "len_of TYPE('a) \ 128") + apply simp +apply(rule len8_width) +done + +instance word :: (len8) array_inner_max_size +apply intro_classes +apply(simp add: size_of_def) +apply(subgoal_tac "len_of TYPE('a) \ 128") + apply simp +apply(rule len8_width) +done + +instance ptr :: (c_type) array_outer_max_size +apply intro_classes +apply (simp add: size_of_def) +done + +instance ptr :: (c_type) array_inner_max_size +apply intro_classes +apply (simp add: size_of_def) +done + +class lt19 = finite + + assumes lt19_ax: "CARD ('a) < 2 ^ 19" +class lt18 = lt19 + + assumes lt18_ax: "CARD ('a) < 2 ^ 18" +class lt17 = lt18 + + assumes lt17_ax: "CARD ('a) < 2 ^ 17" +class lt16 = lt17 + + assumes lt16_ax: "CARD ('a) < 2 ^ 16" +class lt15 = lt16 + + assumes lt15_ax: "CARD ('a) < 2 ^ 15" +class lt14 = lt15 + + assumes lt14_ax: "CARD ('a) < 2 ^ 14" +class lt13 = lt14 + + assumes lt13_ax: "CARD ('a) < 2 ^ 13" +class lt12 = lt13 + + assumes lt12_ax: "CARD ('a) < 2 ^ 12" +class lt11 = lt12 + + assumes lt11_ax: "CARD ('a) < 2 ^ 11" +class lt10 = lt11 + + assumes lt10_ax: "CARD ('a) < 2 ^ 10" +class lt9 = lt10 + + assumes lt9_ax: "CARD ('a) < 2 ^ 9" +class lt8 = lt9 + + assumes lt8_ax: "CARD ('a) < 2 ^ 8" +class lt7 = lt8 + + assumes lt7_ax: "CARD ('a) < 2 ^ 7" +class lt6 = lt7 + + assumes lt6_ax: "CARD ('a) < 2 ^ 6" +class lt5 = lt6 + + assumes lt5_ax: "CARD ('a) < 2 ^ 5" +class lt4 = lt5 + + assumes lt4_ax: "CARD ('a) < 2 ^ 4" +class lt3 = lt4 + + assumes lt3_ax: "CARD ('a) < 2 ^ 3" +class lt2 = lt3 + + assumes lt2_ax: "CARD ('a) < 2 ^ 2" +class lt1 = lt2 + + assumes lt1_ax: "CARD ('a) < 2 ^ 1" + +instance bit0 :: (lt19) array_max_count + using lt19_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt19) array_max_count + using lt19_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt18) lt19 + using lt18_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt18) lt19 + using lt18_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt17) lt18 + using lt17_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt17) lt18 + using lt17_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt16) lt17 + using lt16_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt16) lt17 + using lt16_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt15) lt16 + using lt15_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt15) lt16 + using lt15_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt14) lt15 + using lt14_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt14) lt15 + using lt14_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt13) lt14 + using lt13_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt13) lt14 + using lt13_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt12) lt13 + using lt12_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt12) lt13 + using lt12_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt11) lt12 + using lt11_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt11) lt12 + using lt11_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt10) lt11 + using lt10_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt10) lt11 + using lt10_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt9) lt10 + using lt9_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt9) lt10 + using lt9_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt8) lt9 + using lt8_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt8) lt9 + using lt8_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt7) lt8 + using lt7_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt7) lt8 + using lt7_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt6) lt7 + using lt6_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt6) lt7 + using lt6_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt5) lt6 + using lt5_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt5) lt6 + using lt5_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt4) lt5 + using lt4_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt4) lt5 + using lt4_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt3) lt4 + using lt3_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt3) lt4 + using lt3_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt2) lt3 + using lt2_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt2) lt3 + using lt2_ax[where 'a='a] by intro_classes simp + +instance bit0 :: (lt1) lt2 + using lt1_ax[where 'a='a] by intro_classes simp + +instance bit1 :: (lt1) lt2 + using lt1_ax[where 'a='a] by intro_classes simp + +instance num1 :: lt1 + by (intro_classes, simp_all) + +(* don't understand why this also seems to be necessary *) +instance num1 :: array_max_count + by (intro_classes, simp) + +(* introduce hackish handling of 8192 type by making a copy of the type + under a constructor, and then manually showing that it is an instance of + array_max_count *) +datatype ty1048576 = ty1048576 "1048576" + +lemma univ1048576: "(UNIV::ty1048576 set) = image ty1048576 (UNIV::1048576 set)" +apply (simp add: set_eq_iff image_iff) +apply (rule_tac allI) +apply (rule_tac ty1048576.induct) +apply simp +done + +instance "ty1048576" :: finite +apply intro_classes +apply (simp add: univ1048576) +done + +lemma card8192[simp]: "CARD(ty1048576) = CARD(1048576)" +apply (simp add: univ1048576 card_image inj_on_def) +done + +instance "ty1048576" :: array_max_count + by intro_classes simp + +end