Theory CLanguage
chapter ‹More Building Blocks for our C-Language Model›
theory CLanguage
imports
CProof
Lens
begin
section ‹addr bounds›
lemma addr_card_eq: "addr_card = 2^LENGTH(addr_bitsize)"
by (simp add: addr_card_def card_word)
lemma size_of_bnd: "size_of TYPE('a::mem_type) < 2^LENGTH(addr_bitsize)"
by (rule less_le_trans[OF max_size]) (simp add: addr_card_eq)
lemma size_of_mem_type[simp]: "size_of TYPE('c::mem_type) ≠ 0"
by simp
lemma addr_card_len_of_conv: "addr_card = 2 ^ len_of TYPE(addr_bitsize)"
by (simp add: addr_card)
lemma intvl_split:
"⟦ n ≥ a ⟧ ⟹ { p :: ('a :: len) word ..+ n } = { p ..+ a } ∪ { p + of_nat a ..+ (n - a)}"
apply (rule set_eqI, rule iffI)
apply (clarsimp simp: intvl_def not_less)
subgoal for k
apply (rule exI[where x=k])
apply clarsimp
apply (rule classical)
apply (drule_tac x="k - a" in spec)
apply (clarsimp simp: not_less)
apply (metis diff_less_mono not_less)
done
subgoal for x
apply (clarsimp simp: intvl_def not_less)
apply (rule exI[where x="unat (x - p)"])
apply clarsimp
apply (erule disjE)
apply clarsimp
apply (metis le_unat_uoi less_or_eq_imp_le not_less order_trans)
apply clarsimp
apply (metis le_def le_eq_less_or_eq le_unat_uoi less_diff_conv
add.commute of_nat_add)
done
done
section "More Heap Typing"
primrec
htd_upd :: "addr ⇒ typ_slice list ⇒ heap_typ_desc ⇒ heap_typ_desc"
where
"htd_upd p [] d = d"
| "htd_upd p (x#xs) d = htd_upd (p+1) xs (d(p := (True, x)))"
definition (in c_type) ptr_force_type :: "'a ptr ⇒ heap_typ_desc ⇒ heap_typ_desc" where
"ptr_force_type p ≡ htd_upd (ptr_val p) (typ_slices TYPE('a))"
definition ptr_force_types :: "'a::c_type ptr list ⇒ heap_typ_desc ⇒ heap_typ_desc" where
"ptr_force_types = fold ptr_force_type"
definition ptr_force_free :: "addr ⇒ nat ⇒ heap_typ_desc ⇒ heap_typ_desc" where
"ptr_force_free p b = ptr_force_types (map (λn. PTR(8 word) p +⇩p n) (map of_nat [0..<2^b]))"
definition ptr_u :: "'a::c_type ptr ⇒ (addr × typ_uinfo)" where
"ptr_u p = (ptr_val p, typ_uinfo_t TYPE('a))"
abbreviation "ptr_span_u ≡ (λ(a, t). {a ..+ size_td t})"
definition typ_slices_u :: "typ_uinfo ⇒ typ_slice list" where
"typ_slices_u t = map (λn. list_map (typ_slice_t t n)) [0..<size_td t]"
definition ptr_force_type_u :: "typ_uinfo ⇒ addr ⇒ heap_typ_desc ⇒ heap_typ_desc" where
"ptr_force_type_u t a ≡ htd_upd a (typ_slices_u t)"
lemma heap_update_list_id: "heap_update_list x [] = (λx. x)"
by auto
lemma to_bytes_word8:
"to_bytes (v :: word8) xs = [v]"
by (simp add: to_bytes_def typ_info_word word_rsplit_same)
lemma heap_update_heap_update_list:
"⟦ ptr_val p = q + (of_nat (length l)); Suc (length l) < addr_card ⟧ ⟹
heap_update (p :: word8 ptr) v (heap_update_list q l s) = (heap_update_list q (l @ [v]) s)"
by (metis to_bytes_word8 heap_update_def heap_update_list_concat_fold)
lemma htd_upd_empty[simp]: "htd_upd p [] = id"
by (simp add: fun_eq_iff)
lemma htd_upd_append:
"htd_upd p (xs @ ys) = htd_upd (p + of_nat (length xs)) ys ∘ htd_upd p xs"
by (induction xs arbitrary: p) (simp_all add: fun_eq_iff ac_simps)
lemma htd_upd_singleton[simp]: "htd_upd p [x] = upd_fun p (λh. (True, x))"
by (simp add: fun_eq_iff upd_fun_def)
lemma intvl_Suc_eq: "{p ..+ Suc n} = insert p {p + 1 ..+ n}"
using intvl_split[of 1 "Suc n" p] by (auto simp add: intvl_def)
lemma htd_upd_disj: "p ∉ {p' ..+ length v} ⟹ htd_upd p' v h p = h p"
by (induction v arbitrary: p' h)
(auto simp add: intvl_Suc_eq fun_upd_other simp del: fun_upd_apply)
lemma htd_upd_head:
"xs ≠ [] ⟹ length xs ≤ addr_card ⟹ htd_upd p xs s p = (True, hd xs)"
using intvl_Suc_nmem''[of "length xs" p] htd_upd_disj[of p "p + 1" "tl xs" _]
by (cases xs) (simp_all add: addr_card_eq del: intvl_Suc_nmem')
lemma htd_upd_at:
"i < length xs ⟹ length xs ≤ addr_card ⟹ htd_upd p xs s (p + of_nat i) = (True, xs ! i)"
proof (induction i arbitrary: p xs s)
case 0 with htd_upd_head[of xs p s] show ?case by (simp add: hd_conv_nth)
next
case (Suc n)
from Suc.prems show ?case by (cases xs) (simp_all add: Suc.IH flip: add.assoc)
qed
lemma ptr_force_type_disj:
"p ∉ ptr_span (p' :: 'a::mem_type ptr) ⟹ ptr_force_type p' h p = h p"
unfolding ptr_force_type_def
by (intro htd_upd_disj) simp_all
lemma ptr_force_types_disj:
fixes xs :: "'a::mem_type ptr list"
assumes "⋀x. x ∈ set xs ⟹ i ∉ ptr_span x"
shows "ptr_force_types xs h i = h i"
by (use assms in ‹induction xs rule: rev_induct›)
(auto simp: ptr_force_types_def ptr_force_type_disj)
subsection ‹Heap type tag and valid simple footprint›