Theory LLVM_DS_NArray
section ‹Array with Potential Zero Size›
theory LLVM_DS_NArray
imports "LLVM_DS_Array"
begin
term array_assn
type_synonym 'a narray = "'a ptr"
definition "narray_assn ≡ mk_assn (λxs p. case xs of [] ⇒ ↑(p=null) | _ ⇒ ↿array_assn xs p)"
term array_new
definition [llvm_inline]:
"narray_new TYPE('a::llvm_rep) n ≡ if n=signed_nat 0 then Mreturn null else array_new TYPE('a) n"
thm array_new_rule_snat[no_vars]
lemma narray_new_rule_snat[vcg_rules]:
"llvm_htriple (↿snat.assn n ni) (narray_new TYPE(_) ni) (↿narray_assn (replicate n init))"
unfolding narray_assn_def narray_new_def
supply [split] = list.split
apply vcg_monadify
apply vcg
done
lemma narray_assn_init_pure: "□ ⊢ ↿narray_assn [] null"
unfolding narray_assn_def
by (auto simp: sep_algebra_simps)
thm array_nth_rule_snat[no_vars]
lemma narray_nth_rule[vcg_rules]: "llvm_htriple
(↿narray_assn xs p ∧* ↿snat.assn i ii ∧* ↑⇩d(i < length xs))
(array_nth p ii)
(λr. ↑(r = xs ! i) ∧* ↿narray_assn xs p)"
unfolding narray_assn_def
apply (clarsimp split: list.split)
apply vcg
done
thm array_upd_rule_snat[no_vars]
lemma narray_upd_rule_snat[vcg_rules]: "llvm_htriple
(↿narray_assn xs p ∧* ↿snat.assn i ii ∧* ↑⇩d(i < length xs))
(array_upd p ii x)
(λr. ↑(r = p) ∧* ↿narray_assn (xs[i := x]) p)"
unfolding narray_assn_def
apply (clarsimp split: list.splits nat.splits; intro allI impI conjI)
apply vcg
done
definition [llvm_code]: "narray_free p ≡ if p=null then Mreturn () else array_free p"
thm array_free_rule[no_vars]
lemma narray_free_rule[vcg_rules]:
"llvm_htriple (↿narray_assn xs p) (narray_free p) (λ_. □)"
unfolding narray_assn_def narray_free_def
apply (cases xs; clarsimp)
apply vcg
done
lemma narrayset_rule_snat[vcg_rules]: "llvm_htriple
(↿narray_assn dst dsti ** ↿snat.assn n ni ** ↑⇩d(n≤length dst))
(arrayset dsti c ni)
(λ_. ↿narray_assn (replicate n c @ drop n dst) dsti)"
unfolding narray_assn_def
apply (cases dst; clarsimp split: list.splits)
supply [vcg_rules] = arrayset_zerosize_rule
by vcg
definition [llvm_code]: "narray_new_init n (c::'a::llvm_rep) ≡ doM {
r ← narray_new TYPE('a) n;
arrayset r c n;
Mreturn r
}"
lemma narray_new_init_rule[vcg_rules]: "llvm_htriple
(↿snat.assn n ni)
(narray_new_init ni c)
(λr. ↿narray_assn (replicate n c) r)"
unfolding narray_new_init_def
by vcg
lemma arraycpy_0_rl:
"llvm_htriple (↿snat.assn 0 ni) (arraycpy dsti srci ni) (λ_. □)"
unfolding arraycpy_def
apply (subst llc_while_unfold)
apply vcg_monadify
apply vcg'
done
lemma narraycpy_rule_snat[vcg_rules]:
"llvm_htriple
(↿narray_assn dst dsti ** ↿narray_assn src srci ** ↿snat.assn n ni ** ↑⇩d(n≤length src ∧ n≤length dst))
(arraycpy dsti srci ni)
(λ_. ↿narray_assn (take n src @ drop n dst) dsti ** ↿narray_assn src srci)"
unfolding narray_assn_def
apply (cases dst; cases src; simp)
supply [vcg_rules] = arraycpy_0_rl
apply vcg
apply (clarsimp split: list.splits)
apply vcg
done
definition [llvm_code]: "array_grow newsz oldsz src ≡ doM {
dst ← narray_new TYPE(_) newsz;
arraycpy dst src oldsz;
narray_free src;
Mreturn dst
}"
lemma narray_grow_rule_snat[vcg_rules]: "llvm_htriple
(↿narray_assn src srci ** ↿snat.assn newsz newszi ** ↿snat.assn oldsz oldszi ** ↑(oldsz ≤ length src ∧ oldsz ≤ newsz))
(array_grow newszi oldszi srci)
(λdsti. ↿narray_assn (take oldsz src@replicate (newsz - oldsz) init) dsti)"
unfolding array_grow_def
by vcg
definition [llvm_code]: "example1 (n::64 word) ≡ doM {
a ← narray_new TYPE(8 word) n;
array_upd a (1::64 word) 42;
narray_free a
}"
export_llvm (debug) example1
subsection ‹Array Slices›
context begin
interpretation llvm_prim_mem_setup .
definition "array_base_assn ≡ mk_assn (λn p. if n=0 then ↑(p=null) else ll_malloc_tag (int n) p)"
definition "array_slice_assn ≡ mk_assn (λxs p.
if xs=[] then □
else ↿(ll_range {0..<int (length xs)}) ((!) xs o nat) p
)"
lemma array_slice_empty[sep_algebra_simps]:
"↿array_slice_assn [] p = □"
"↿array_slice_assn xs null = ↑(xs=[])"
unfolding array_slice_assn_def
by (auto simp add: sep_algebra_simps ll_range_def)
lemma array_assn_split: "↿narray_assn xs p = (↿array_slice_assn xs p ** ↿array_base_assn (length xs) p)"
unfolding array_assn_def narray_assn_def array_slice_assn_def array_base_assn_def
by (auto simp: sep_algebra_simps split: list.split)
lemma array_slice_split_aux: "{0..<i + j} = {0..<i} ∪ {i..<i+j}" if "i≥0" "j≥0" for i j :: int
using that by auto
lemma ll_range_shift:
"↿(ll_range {l+ofs..<h+ofs}) f p = ↿(ll_range {l..<h}) (λi. f (i+ofs)) (p+⇩aofs)"
proof -
have "(⋃*i∈{l + ofs..<h + ofs}. ↿ll_pto (f i) (p +⇩a i)) = (⋃*i∈((+)ofs)`{l..<h}. ↿ll_pto (f i) (p +⇩a i))"
by simp
also have "… = (⋃*x∈{l..<h}. ↿ll_pto (f (x + ofs)) (p +⇩a (ofs + x)))"
apply (subst sep_set_img_map)
apply (simp_all add: algebra_simps)
done
finally show ?thesis
apply (simp add: ll_range_def)
apply (cases "abase p"; simp add: sep_algebra_simps)
done
qed
lemma ll_range_empty[sep_algebra_simps]: "↿(ll_range {}) f p = ↑(abase p)" unfolding ll_range_def by (auto)
lemma ll_range_no_base[sep_algebra_simps]: "¬abase p ⟹ ↿(ll_range I) f p = sep_false"
unfolding ll_range_def by (auto)
lemma array_slice_assn_split: "↿array_slice_assn (xs⇩1@xs⇩2) p = (↿array_slice_assn xs⇩1 p ** ↿array_slice_assn xs⇩2 (p +⇩a int (length xs⇩1)))"
proof -
have 1: "↿(ll_range {0..<int (length xs⇩1)}) (λi. (xs⇩1 @ xs⇩2) ! nat i) p
= ↿(ll_range {0..<int (length xs⇩1)}) (λi. xs⇩1 ! nat i) p"
apply (rule ll_range_cong)
apply auto
done
have "↿(ll_range {int (length xs⇩1)..<int (length xs⇩1) + int (length xs⇩2)}) (λx. (xs⇩1 @ xs⇩2) ! nat x) p
= ↿(ll_range {0+int (length xs⇩1)..<int (length xs⇩2) + int (length xs⇩1)}) (λx. (xs⇩1 @ xs⇩2) ! nat x) p"
by (simp add: algebra_simps)
also have "… = ↿(ll_range {0..<int (length xs⇩2)}) (λi. (xs⇩1 @ xs⇩2) ! nat (i + int (length xs⇩1))) (p +⇩a int (length xs⇩1))"
apply (subst ll_range_shift)
..
also have "… = ↿(ll_range {0..<int (length xs⇩2)}) (λi. xs⇩2 ! nat i) (p +⇩a int (length xs⇩1))"
apply (rule ll_range_cong)
apply (auto simp: nth_append nat_add_distrib)
done
finally show ?thesis
unfolding array_slice_assn_def
apply (simp add: comp_def array_slice_split_aux ll_range_merge[symmetric] 1)
apply (cases "abase p")
apply (auto simp: sep_algebra_simps)
done
qed
lemma array_slice_assn_cnv_range_upd:
"i<length xs ⟹ ↿array_slice_assn (xs[i:=x]) p = (↿(ll_range {0..<int (length xs)}) (((!) xs ∘ nat)(int i := x)) p)"
unfolding array_slice_assn_def
apply (simp add: sep_algebra_simps)
apply (rule ll_range_cong)
by auto
lemma array_slice_nth_rule_snat[vcg_rules]: "llvm_htriple
(↿array_slice_assn xs p ** ↿snat.assn i ii ** ↑⇩d(i<length xs))
(array_nth p ii)
(λr. ↑(r = xs!i) ** ↿array_slice_assn xs p)"
unfolding array_nth_def array_slice_assn_def snat.assn_def
supply [simp] = cnv_snat_to_uint and [simp del] = nat_uint_eq
by vcg
lemma array_slice_rule_snat[vcg_rules]: "llvm_htriple
(↿array_slice_assn xs p ** ↿snat.assn i ii ** ↑⇩d(i<length xs))
(array_upd p ii x)
(λr. ↑(r=p) ** ↿array_slice_assn (xs[i:=x]) p)"
apply (cases "i<length xs")
subgoal
apply (subst array_slice_assn_cnv_range_upd; simp)
unfolding array_upd_def array_slice_assn_def snat.assn_def
supply [simp] = cnv_snat_to_uint and [simp del] = nat_uint_eq
supply [fri_rules] = fri_abs_cong_rl
apply vcg
done
subgoal by vcg
done
end
end