diff --git a/lib/LemmaBucket_C.thy b/lib/LemmaBucket_C.thy index cb42e8ed4..70893debd 100644 --- a/lib/LemmaBucket_C.thy +++ b/lib/LemmaBucket_C.thy @@ -299,16 +299,16 @@ lemma heap_update_list_update: (* FIXME: generalise *) lemma heap_update_list_append2: - fixes v :: word8 - shows "length xs + length ys < 2 ^ word_bits \ heap_update_list s (xs @ ys) hp = - (heap_update_list s xs (heap_update_list (s + of_nat (length xs)) ys hp))" + "length xs + length ys < 2 ^ word_bits \ + heap_update_list s (xs @ ys) hp + = heap_update_list s xs (heap_update_list (s + of_nat (length xs)) ys hp)" proof (induct xs arbitrary: hp s) case Nil show ?case by simp next case (Cons v' vs') - have "(1 :: word32) + of_nat (length vs') = of_nat (length (v' # vs'))" + have "(1 :: addr) + of_nat (length vs') = of_nat (length (v' # vs'))" by simp also have "\ \ 0" using Cons.prems apply - @@ -316,15 +316,15 @@ next apply simp apply (simp add: word_bits_conv) done - finally have neq0: "(1 :: word32) + of_nat (length vs') \ 0" . + finally have neq0: "(1 :: addr) + of_nat (length vs') \ 0" . - have "(1 :: word32) + of_nat (length vs') = of_nat (length (v' # vs'))" + have "(1 :: addr) + of_nat (length vs') = of_nat (length (v' # vs'))" by simp also have "unat \ + length ys < 2 ^ word_bits" using Cons.prems apply (subst unat_of_nat) apply (simp add: word_bits_conv) done - finally have lt: "unat ((1 :: word32) + of_nat (length vs')) + length ys < 2 ^ word_bits" . + finally have lt: "unat ((1 :: addr) + of_nat (length vs')) + length ys < 2 ^ word_bits" . from Cons.prems have "length vs' + length ys < 2 ^ word_bits" by simp thus ?case @@ -412,7 +412,7 @@ lemma intvl_disjoint2: lemma intvl_off_disj: - fixes x :: word32 + fixes x :: addr assumes ylt: "y \ off" and zoff: "z + off < 2 ^ word_bits" shows "{x ..+ y} \ {x + of_nat off ..+ z} = {}" @@ -422,7 +422,7 @@ lemma intvl_off_disj: apply (rule contrapos_pp [OF TrueI]) apply (drule intvl_inter) apply (erule disjE) - apply (cut_tac intvl_nowrap [where x = x and y = "of_nat off :: word32" and z = z]) + apply (cut_tac intvl_nowrap [where x = x and y = "of_nat off :: addr" and z = z]) apply simp apply (rule of_nat_neq_0) apply simp @@ -776,20 +776,20 @@ lemma heap_update_commute: lemma heap_update_Array_update: assumes n: "n < CARD('b :: finite)" - assumes size: "CARD('b) * size_of TYPE('a :: packed_type) < 2 ^ 32" + assumes size: "CARD('b) * size_of TYPE('a :: packed_type) < 2 ^ addr_bitsize" shows "heap_update p (Arrays.update (arr :: 'a['b]) n v) hp = heap_update (array_ptr_index p False n) v (heap_update p arr hp)" proof - have P: "\x k. \ x < CARD('b); k < size_of TYPE('a) \ - \ unat (of_nat x * of_nat (size_of TYPE('a)) + (of_nat k :: word32)) + \ unat (of_nat x * of_nat (size_of TYPE('a)) + (of_nat k :: addr)) = x * size_of TYPE('a) + k" using size apply (case_tac "size_of TYPE('a)", simp_all) apply (case_tac "CARD('b)", simp_all) apply (subst unat_add_lem[THEN iffD1]) apply (simp add: unat_word_ariths unat_of_nat less_Suc_eq_le) - apply (subgoal_tac "Suc x * size_of TYPE('a) < 2 ^ 32", simp_all) + apply (subgoal_tac "Suc x * size_of TYPE('a) < 2 ^ addr_bitsize", simp_all) apply (erule order_le_less_trans[rotated], simp add: add_mono) apply (subst unat_mult_lem[THEN iffD1]) apply (simp add: unat_of_nat unat_add_lem[THEN iffD1]) @@ -835,7 +835,7 @@ lemma heap_update_Array_element'': fixes hp w assumes p: "p = array_ptr_index p' False n" assumes n: "n < CARD('b)" - assumes size: "CARD('b) * size_of TYPE('a) < 2 ^ 32" + assumes size: "CARD('b) * size_of TYPE('a) < 2 ^ addr_bitsize" shows "heap_update p' (Arrays.update (h_val hp p') n w) hp = heap_update p w hp" apply (subst heap_update_Array_update[OF n size]) @@ -846,7 +846,7 @@ 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" + "CARD('b :: fourthousand_count) * size_of TYPE('a :: oneMB_size) < 2 ^ addr_bitsize" using oneMB_size_ax[where 'a='a] fourthousand_count_ax[where 'a='b] apply (clarsimp dest!: nat_le_Suc_less_imp) apply (drule(1) mult_mono, simp+) @@ -1097,7 +1097,7 @@ lemma hrs_mem_update_id3: "hrs_mem_update id = id" unfolding hrs_mem_update_def by simp abbreviation - ptr_span :: "'a::mem_type ptr \ word32 set" where + ptr_span :: "'a::mem_type ptr \ addr set" where "ptr_span p \ {ptr_val p ..+ size_of TYPE('a)}" abbreviation (input) diff --git a/lib/TypHeapLib.thy b/lib/TypHeapLib.thy index 1b708ad0e..c15b35257 100644 --- a/lib/TypHeapLib.thy +++ b/lib/TypHeapLib.thy @@ -419,9 +419,9 @@ lemma c_guard_array_field: instantiation ptr :: (type) enum begin - definition "enum_ptr \ map Ptr (enum_class.enum :: 32 word list)" - definition "enum_all_ptr P \ enum_class.enum_all (\v :: 32 word. P (Ptr v))" - definition "enum_ex_ptr P \ enum_class.enum_ex (\v :: 32 word. P (Ptr v))" + definition "enum_ptr \ map Ptr enum_class.enum" + definition "enum_all_ptr P \ enum_class.enum_all (\v. P (Ptr v))" + definition "enum_ex_ptr P \ enum_class.enum_ex (\v. P (Ptr v))" instance apply (intro_classes) diff --git a/tools/c-parser/umm_heap/Vanilla32.thy b/tools/c-parser/umm_heap/Vanilla32.thy index dfdac5965..e33f069da 100644 --- a/tools/c-parser/umm_heap/Vanilla32.thy +++ b/tools/c-parser/umm_heap/Vanilla32.thy @@ -305,12 +305,16 @@ lemma ptr_add_word32 [simp]: fixes a :: "32 word ptr" shows "ptr_val (a +\<^sub>p uint x) = ptr_val a + 4 * x" by (cases a) (simp add: ptr_add_def scast_id) -(* + +lemma ptr_add_word64_signed [simp]: + fixes a :: "64 word ptr" + shows "ptr_val (a +\<^sub>p x) = ptr_val a + 8 * of_int x" + by (cases a) (simp add: CTypesDefs.ptr_add_def scast_id) + lemma ptr_add_word64 [simp]: - fixes a :: "64 word ptr" and x :: "64 word" + fixes a :: "64 word ptr" shows "ptr_val (a +\<^sub>p uint x) = ptr_val a + 8 * x" by (cases a) (simp add: ptr_add_def scast_id) -*) lemma ptr_add_0_id[simp]:"x +\<^sub>p 0 = x" by (simp add:CTypesDefs.ptr_add_def) @@ -322,8 +326,7 @@ lemma from_bytes_ptr_to_bytes_ptr: length_word_rsplit_exp_size' word_rcat_rsplit) lemma ptr_aligned_coerceI: - "ptr_aligned (ptr_coerce x::32 word ptr) \ - ptr_aligned (x::'a::mem_type ptr ptr)" + "ptr_aligned (ptr_coerce x::addr ptr) \ ptr_aligned (x::'a::mem_type ptr ptr)" by (simp add: ptr_aligned_def) lemma lift_ptr_ptr [simp]: diff --git a/tools/c-parser/umm_heap/X64/Addr_Type.thy b/tools/c-parser/umm_heap/X64/Addr_Type.thy index cfe3d19c7..f68a54f93 100644 --- a/tools/c-parser/umm_heap/X64/Addr_Type.thy +++ b/tools/c-parser/umm_heap/X64/Addr_Type.thy @@ -17,7 +17,7 @@ begin type_synonym addr_bitsize = "64" type_synonym addr = "addr_bitsize word" definition addr_bitsize :: nat where "addr_bitsize \ 64" -definition addr_align :: nat where "addr_align \ 2" +definition addr_align :: nat where "addr_align \ 3" declare addr_align_def[simp] definition addr_card :: nat where diff --git a/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy b/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy index 7da5136d0..c67026fd5 100644 --- a/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy +++ b/tools/c-parser/umm_heap/X64/Word_Mem_Encoding.thy @@ -16,6 +16,11 @@ begin definition word_tag :: "'a::len8 word itself \ 'a word typ_info" where - "word_tag (w::'a::len8 word itself) \ TypDesc (TypScalar (len_of TYPE('a) div 8) (len_exp TYPE('a)) \ field_access = \v bs. (rev o word_rsplit) v, field_update = \bs v. (word_rcat (rev bs)::'a::len8 word) \) (''word'' @ nat_to_bin_string (len_of TYPE('a)) )" + "word_tag (w::'a::len8 word itself) \ + TypDesc (TypScalar (len_of TYPE('a) div 8) + (len_exp TYPE('a)) + \ field_access = \v bs. (rev o word_rsplit) v, + field_update = \bs v. (word_rcat (rev bs)::'a::len8 word) \) + (''word'' @ nat_to_bin_string (len_of TYPE('a)))" end