Theory LLVM_Memory_RS
theory LLVM_Memory_RS
imports
"../basic/LLVM_Basic_Main"
Sep_Value_RS
Sep_Array_Block_RS
begin
interpretation ab: array_block2 "STATIC_ERROR ''''" MEM_ERROR "vload MEM_ERROR::_ ⇒ (llvm_primval val,_,_,_,_) M" "vstore MEM_ERROR" "checked_gep MEM_ERROR" val_α vpto_assn "λv. v∈range val_α"
apply unfold_locales
apply (rule vload_rule)
apply (rule vstore_rule)
apply (rule vpto_assn_notZ)
apply auto []
apply (simp; rule vpto_assn_this)
apply auto []
done
datatype llvm_amemory = LLVM_AMEMORY (the_amemory: "(nat ⇒ (nat ⇒ llvm_primval aval) × int tsa_opt)")
instantiation llvm_amemory :: unique_zero_sep_algebra begin
definition "sep_disj_llvm_amemory a b ≡ the_amemory a ## the_amemory b"
definition "plus_llvm_amemory a b ≡ LLVM_AMEMORY (the_amemory a + the_amemory b)"
definition "zero_llvm_amemory ≡ LLVM_AMEMORY 0"
instance
apply standard
unfolding sep_disj_llvm_amemory_def plus_llvm_amemory_def zero_llvm_amemory_def
apply (auto simp: sep_algebra_simps llvm_amemory.expand)
done
end
type_synonym llvm_assn = "llvm_amemory ⇒ bool"
definition "llvm_α ≡ LLVM_AMEMORY o ab.ba.α o llvm_memory.the_memory"
definition "llvm_pto x p ≡ (ab.ba.pto (llvm_val.the_val x) (llvm_ptr.the_ptr p)) o llvm_amemory.the_amemory"
definition "llvm_malloc_tag n p ≡ ab.ba.tag n (llvm_ptr.the_ptr p) o llvm_amemory.the_amemory"
instantiation llvm_ptr :: addr_algebra begin
definition "abase_llvm_ptr = abase o llvm_ptr.the_ptr"
definition "acompat_llvm_ptr a b ≡ acompat (llvm_ptr.the_ptr a) (llvm_ptr.the_ptr b)"
definition "adiff_llvm_ptr a b ≡ adiff (llvm_ptr.the_ptr a) (llvm_ptr.the_ptr b)"
definition "aidx_llvm_ptr a i ≡ LLVM_PTR ((llvm_ptr.the_ptr a) +⇩a i)"
instance
apply standard
unfolding abase_llvm_ptr_def acompat_llvm_ptr_def adiff_llvm_ptr_def aidx_llvm_ptr_def
apply (intro part_equivpI sympI transpI)
apply (metis ab.block_ptr_imp_abase ab.is_block_ptr_simps(2) acompat_refl llvm_ptr.sel)
apply (auto intro: acompat_trans simp: acompat_dom)
done
end
lemma xfer_htriple:
assumes "notime.htriple ab.ba.α P c Q"
assumes "P' = P o llvm_amemory.the_amemory"
assumes "c' = llvm_zoom_base α c"
assumes "⋀r. Q' (α r) = Q r o llvm_amemory.the_amemory"
shows "notime.htriple llvm_α P' c' Q'"
using assms unfolding notime.htriple_alt llvm_zoom_base_def llvm_α_def wpn_def
apply (clarsimp simp: run_simps)
proof goal_cases
case A: (1 p s f)
find_theorems llvm_memory.the_memory⇩L
from ‹p##f› ‹LLVM_AMEMORY (ab.ba.α (get' llvm_memory.the_memory⇩L s)) = p + f›
have "llvm_amemory.the_amemory p ## llvm_amemory.the_amemory f"
and "ab.ba.α (get' llvm_memory.the_memory⇩L s) = llvm_amemory.the_amemory p + llvm_amemory.the_amemory f"
by (auto simp: sep_disj_llvm_amemory_def plus_llvm_amemory_def)
from A(1)[rule_format] show ?case
apply (rule mwp_cons)
apply (intro conjI; fact)
apply (clarsimp_all simp: run_simps)
by (metis (full_types) assms(4) comp_apply llvm_amemory.sel plus_llvm_amemory_def sep_disj_llvm_amemory_def)
qed
lemma llvm_load_rule[vcg_rules]: "notime.htriple llvm_α (llvm_pto x p) (llvm_load p) (λr. ↑(r=x) ** llvm_pto x p)"
apply (rule xfer_htriple[OF ab.ba.load_rule])
unfolding llvm_pto_def llvm_load_def
apply simp
apply simp
apply (rule ext)
apply (auto simp: sep_algebra_simps pred_lift_extract_simps)
done
lemma llvm_store_unchecked_rule[vcg_rules]: "notime.htriple llvm_α (llvm_pto xx p) (llvm_store_unchecked x p) (λ_. llvm_pto x p)"
apply (rule xfer_htriple[OF ab.ba.store_rule])
unfolding llvm_pto_def llvm_store_unchecked_def
apply simp
apply simp
apply (rule ext)
apply (auto simp: sep_algebra_simps pred_lift_extract_simps)
done
lemma llvm_store_rule[vcg_rules]: "llvm_vstruct x = llvm_vstruct xx
⟹ notime.htriple llvm_α (llvm_pto xx p) (llvm_store x p) (λ_. llvm_pto x p)"
unfolding llvm_store_def
by vcg
lemma the_amemoryZ[simp]: "the_amemory 0 = 0" by (auto simp: zero_llvm_amemory_def)
lemma the_amemoryZ_iff[simp]: "the_amemory x = 0 ⟷ x=0"
by (auto simp: zero_llvm_amemory_def llvm_amemory.expand)
lemma xfer_sep_conj1: "((λx. a (the_amemory x)) ** (λx. b (the_amemory x))) = (a**b) o the_amemory"
apply (rule ext)
apply (auto 3 3 simp: sep_conj_def sep_disj_llvm_amemory_def plus_llvm_amemory_def)
by (metis (full_types) llvm_amemory.exhaust_sel llvm_amemory.sel)
lemma xfer_sep_conj2: "((a o the_amemory) ** (b o the_amemory)) = (a**b) o the_amemory"
using xfer_sep_conj1 unfolding comp_def .
lemmas xfer_sep_conj = xfer_sep_conj1 xfer_sep_conj2
lemma xfer_sep_list_conj1: "(⋀*map (λx. f x o the_amemory) l) = (⋀*map f l) o the_amemory"
apply (induction l)
apply auto
by (auto simp: sep_algebra_simps xfer_sep_conj)
lemma xfer_sep_list_conj2: "(⋀*map (λx s. f x (the_amemory s)) l) = (⋀*map f l) o the_amemory"
using xfer_sep_list_conj1 unfolding comp_def .
lemmas xfer_sep_list_conj = xfer_sep_list_conj1 xfer_sep_list_conj2
lemma xfer_sep_set_img1: "(⋃*x∈I. f x o the_amemory) = (⋃*x∈I. f x) o the_amemory"
proof (cases "finite I")
case True then show ?thesis
by (induction) (auto del: ext intro!: ext simp: sep_algebra_simps xfer_sep_conj)
qed auto
lemma xfer_sep_set_img2: "(⋃*x∈I. (λs. f x (the_amemory s))) = (⋃*x∈I. f x) o the_amemory"
using xfer_sep_set_img1 unfolding comp_def .
lemmas xfer_sep_set_img = xfer_sep_set_img1 xfer_sep_set_img2
lemma llvm_allocn_rule[vcg_rules]:
"notime.htriple llvm_α
□
(llvm_allocn v n)
(λr. (⋃*i∈{0..<int n}. llvm_pto v (r +⇩a i))
** llvm_malloc_tag (int n) r ** ↑(abase r))"
apply (rule xfer_htriple[OF ab.ba_allocn_rule])
unfolding llvm_pto_def llvm_allocn_def llvm_malloc_tag_def abase_llvm_ptr_def aidx_llvm_ptr_def
apply (rule ext) apply (auto simp: sep_algebra_simps) []
apply simp
apply (rule ext)
apply (auto simp: sep_algebra_simps pred_lift_extract_simps xfer_sep_set_img xfer_sep_conj)
done
lemma llvm_free_rule[vcg_rules]:
"notime.htriple llvm_α
((⋃*i∈{0..<n}. EXS v. llvm_pto v (p +⇩a i))
** llvm_malloc_tag n p)
(llvm_free p)
(λ_. □)"
apply (rule xfer_htriple[OF ab.ba_freen_rule[where p="llvm_ptr.the_ptr p" and n=n], where α=id])
apply (cases p; simp add: )
unfolding llvm_pto_def llvm_free_def llvm_malloc_tag_def aidx_llvm_ptr_def
apply (auto simp: sep_algebra_simps)
apply (subst xfer_sep_set_img xfer_sep_conj)+
apply (cases p; simp)
by (metis llvm_val.sel)
lemma llvm_checked_idx_ptr_rule[vcg_rules]:
"abase p ⟹
notime.htriple llvm_α
(llvm_pto v (p +⇩a i))
(llvm_checked_idx_ptr p i)
(λr. ↑(r= p +⇩a i) ** llvm_pto v (p +⇩a i))
"
supply R=xfer_htriple[OF ab.checked_idx_ptr_rule[where p="llvm_ptr.the_ptr p" and i=i and xx="llvm_val.the_val v"], where α=LLVM_PTR]
apply (rule R)
unfolding llvm_checked_idx_ptr_def llvm_pto_def abase_llvm_ptr_def aidx_llvm_ptr_def
apply (auto simp: xfer_sep_conj sep_algebra_simps pred_lift_extract_simps)
done
end