Theory LLVM_Shallow_RS
section ‹LLVM Shallow Embedding --- Reasoning Setup›
theory LLVM_Shallow_RS
imports
"../basic/LLVM_Basic_Main"
LLVM_Simple_Memory_RS
begin
subsection ‹Monadification Setup for VCG›
ML ‹
structure LLVM_VCG_Monadify = struct
structure Monadify = Gen_Monadify_Cong (
fun mk_return x = @{mk_term "Mreturn ?x ::_ llM"}
fun mk_bind m f = @{mk_term "Mbind ?m ?f ::_ llM"}
fun dest_return @{mpat "Mreturn ?x ::_ llM"} = SOME x | dest_return _ = NONE
fun dest_bind @{mpat "Mbind ?m ?f ::_ llM"} = SOME (m,f) | dest_bind _ = NONE
val dest_monadT = try LLC_Lib.dest_llM
val bind_return_thm = @{lemma "Mbind m Mreturn = m" by simp}
val return_bind_thm = @{lemma "Mbind (Mreturn x) f = f x" by simp}
val bind_bind_thm = @{lemma "Mbind (Mbind m (λx. f x)) g = Mbind m (λx. Mbind (f x) g)" by simp}
)
val _ = Theory.setup
(Attrib.setup \<^binding>‹vcg_const›
(Args.term >> (fn t => Thm.declaration_attribute (K (Monadify.prepare_add_const_decl false t))))
"declaration of new vcg-constant")
fun monadify_all_tac ctxt = CONVERSION (Conv.top_sweep_conv (Monadify.monadify_conv) ctxt)
end
›
named_theorems vcg_monadify_xforms
method_setup vcg_monadify_raw = ‹Scan.succeed (SIMPLE_METHOD' o LLVM_VCG_Monadify.monadify_all_tac)›
method vcg_monadify_xform_raw = (simp only: vcg_monadify_xforms)?
method vcg_monadify uses simp =
vcg_monadify_xform_raw; ((changed ‹vcg_monadify_raw; vcg_monadify_xform_raw›)+)?
declare llvm_inline_bind_laws[vcg_monadify_xforms]
subsection ‹Abbreviations for VCG›
type_synonym ll_assn = "(llvm_amemory ⇒ bool)"
abbreviation llvm_htriple
:: "ll_assn ⇒ 'a llM ⇒ ('a ⇒ ll_assn) ⇒ bool"
where "llvm_htriple ≡ htriple"
locale llvm_prim_setup
subsection ‹General VCG Setup›
lemma [fri_extract_simps]: "(case p of (a,b) ⇒ (P a b :: ll_assn)) = (EXS a b. ↑(p=(a,b)) ** P a b)"
apply (cases p) apply (rule ext)
apply (auto simp: sep_algebra_simps)
done
lemma norm_prod_case[vcg_normalize_simps]:
"wp (case p of (a,b) ⇒ f a b) Q s ⟷ (∀a b. p=(a,b) ⟶ wp (f a b) Q s)"
by (auto split: prod.split)
subsection ‹Assertions›
typedef ('a,'c) dr_assn = "UNIV :: ('a ⇒ 'c ⇒ ll_assn) set" by simp
setup_lifting type_definition_dr_assn
lemma dr_assn_inverses[simp]:
"Abs_dr_assn (Rep_dr_assn A) = A"
"Rep_dr_assn (Abs_dr_assn B) = B"
using Rep_dr_assn_inverse Abs_dr_assn_inverse by auto
definition dr_assn_prefix :: "('a, 'b) dr_assn ⇒ 'a ⇒ 'b ⇒ ll_assn" ("↿_" [1000] 1000) where
"↿A a c ≡ Rep_dr_assn A a c"
definition "is_pure A ≡ ∀a c. sep_is_pure_assn (↿A a c)"
definition dr_assn_pure_prefix ("↿⇩p_" [1000] 1000) where
"↿⇩pA a c ≡ ↑pure_part (↿A a c)"
definition dr_assn_pure_asm_prefix ("♭⇩p_" [1000] 1000) where
"♭⇩pA a c ≡ pure_part (↿A a c) ∧ is_pure A"
lemma pure_fri_rule[fri_rules]: "PRECOND (SOLVE_ASM (♭⇩pA a c)) ⟹ □ ⊢ ↿⇩pA a c"
unfolding vcg_tag_defs entails_def dr_assn_pure_prefix_def dr_assn_pure_asm_prefix_def
is_pure_def
apply clarsimp
apply (subst pure_part_pure_eq[symmetric])
apply (auto simp: sep_algebra_simps)
done
lemma prepare_pure_assn[named_ss fri_prepare_simps]: "↿A a c = ↿⇩pA a c" if "is_pure A"
using that
by (simp add: dr_assn_pure_prefix_def is_pure_def)
lemma [fri_extract_simps]: "↿A a c = ↑♭⇩pA a c" if "is_pure A"
using that
unfolding vcg_tag_defs entails_def dr_assn_pure_asm_prefix_def is_pure_def
apply (auto simp: sep_algebra_simps)
done
attribute_setup is_pure_rule = ‹Attrib.add_del
(VCG_Lib.chained_decl_attr @{context} @{attributes [named_ss fri_prepare_simps, fri_extract_simps]})
(VCG_Lib.chained_decl_attr @{context} @{attributes [named_ss fri_prepare_simps del, fri_extract_simps del]})
›
‹Rules to introduce pure assertions›
text ‹This rule is to be overloaded by later rules›
lemma pure_part_pureD[vcg_prep_ext_rules]: "pure_part (↑Φ) ⟹ Φ" by simp
lemma prep_ext_pure_part_pure[vcg_prep_ext_rules]:
"pure_part (↿⇩pA a c) ⟹ pure_part (↿A a c)"
unfolding dr_assn_pure_prefix_def by simp
lemma thin_dr_pure_asm[vcg_prep_ext_rules]: "(♭⇩pA a c) ⟹ pure_part (↿A a c)"
unfolding dr_assn_pure_asm_prefix_def by simp
definition "mk_assn ≡ Abs_dr_assn"
definition "mk_pure_assn A ≡ mk_assn (λa c. ↑A a c)"
lemma is_pure_mk_pure[simp]: "is_pure (mk_pure_assn A)"
unfolding is_pure_def mk_pure_assn_def mk_assn_def dr_assn_prefix_def
by (auto)
lemma sel_mk_assn[simp]: "↿(mk_assn A) a c = A a c"
by (auto simp: mk_assn_def dr_assn_prefix_def)
lemma sel_mk_pure_assn[simp]:
"↿(mk_pure_assn A) a c = ↑(A a c)"
"↿⇩p(mk_pure_assn A) a c = ↑(A a c)"
"♭⇩p(mk_pure_assn A) a c = A a c"
apply (auto simp: mk_pure_assn_def dr_assn_pure_prefix_def dr_assn_pure_asm_prefix_def)
apply (auto simp: mk_assn_def is_pure_def dr_assn_prefix_def sep_algebra_simps)
done
lemma :
assumes "pure_part (↿(mk_pure_assn A) a c)"
assumes "A a c ⟹ Φ a c"
shows "Φ a c"
using assms
by auto
lemma :
assumes "pure_part (↿(mk_assn A) a c)"
assumes "A a c ⊢ ↑Φ a c ** sep_true"
shows "Φ a c"
using assms
by (auto simp: entails_def sep_conj_def pred_lift_def sep_algebra_simps)
lemma :
assumes "pure_part (↿(mk_assn A) a c)"
assumes "FRAME (A a c) (↑Φ a c) F"
shows "Φ a c"
apply (rule mk_assn_extractI[OF assms(1)])
using assms(2) unfolding FRAME_def
by (metis (no_types, lifting) entails_def entails_mp sep_conj_commute)
lemma pure_part_mk_assnD[vcg_prep_ext_rules]:
"pure_part (↿(mk_assn f) a c) ⟹ pure_part (f a c)"
by auto
lemma fri_abs_cong_rl: "PRECOND (SOLVE_AUTO (a=a')) ⟹ ↿A a c ⊢ ↿A a' c"
unfolding vcg_tag_defs by auto
subsection ‹Memory Reasoning›
locale llvm_prim_mem_setup
sublocale llvm_prim_setup < llvm_prim_mem_setup .
subsubsection ‹Pointers›
text ‹Assertion for pointer to single value›
definition ll_pto :: "('a::llvm_rep, 'a ptr) dr_assn"
where "ll_pto ≡ mk_assn (λv p. llvm_pto (to_val v) (the_raw_ptr p))"
lemma ll_pto_null[simp]: "↿ll_pto x null = sep_false"
by (simp add: ll_pto_def null_def llvm_pto_def)
instantiation ptr :: (llvm_rep) addr_algebra begin
definition "abase ≡ abase o the_raw_ptr"
definition "acompat a b ≡ acompat (the_raw_ptr a) (the_raw_ptr b)"
definition "adiff a b ≡ adiff (the_raw_ptr a) (the_raw_ptr b)"
definition aidx_ptr :: "'a ptr ⇒ int ⇒ 'a ptr" where "aidx a i ≡ PTR (aidx (the_raw_ptr a) i)"
instance
apply standard
apply (intro part_equivpI sympI transpI)
unfolding abase_ptr_def acompat_ptr_def adiff_ptr_def aidx_ptr_def
apply (metis acompat_equiv part_equivp_def ptr.sel)
apply (auto intro: acompat_trans simp: acompat_dom)
done
end
find_theorems pure_part
lemma ll_pto_base[vcg_prep_ext_rules]: "pure_part (↿ll_pto x p) ⟹ abase p"
by (simp add: ll_pto_def null_def llvm_pto_def abase_ptr_def split: llvm_ptr.splits)
lemma abase_not_null[simp]: "¬abase null"
by (auto simp: abase_ptr_def null_def)
text ‹Assertion to range of array›
definition "ll_range I ≡ mk_assn (λf p. ↑(abase p) ** (⋃*i∈I. ↿ll_pto (f i) (p +⇩a i)))"
lemma ll_range_not_null[simp]: "↿(ll_range I) f null = sep_false"
by (simp add: ll_range_def)
lemma ll_range_base[vcg_prep_ext_rules]: "pure_part (↿(ll_range I) xs p) ⟹ abase p"
unfolding ll_range_def apply (cases "abase p") apply (simp_all) done
lemma ll_pto_not_same: "(↿ll_pto x p ** ↿ll_pto y p) = sep_false"
apply (rule ext)
apply (auto simp add: ll_pto_def llvm_pto_def sep_conj_def sep_algebra_simps split: llvm_ptr.splits)
done
lemma ll_range_merge: "I⇩1∩I⇩2={} ⟹ (↿(ll_range I⇩1) f p ** ↿(ll_range I⇩2) f p) = ↿(ll_range (I⇩1∪I⇩2)) f p"
unfolding ll_range_def
by (auto simp: sep_algebra_simps)
lemma ll_range_bogus_upd[simp]: "x∉I ⟹ ↿(ll_range I) (f(x:=v)) p = ↿(ll_range I) f p"
unfolding ll_range_def
apply (cases "abase p"; simp add: sep_algebra_simps)
by (rule sep_set_img_cong) (auto)
lemma open_ll_range: "i∈I ⟹ ↿(ll_range I) f p = (↑(abase p) ** ↿ll_pto (f i) (p +⇩a i) ** ↿(ll_range (I-{i})) f p)"
unfolding ll_range_def
by (auto simp: sep_algebra_simps sep_set_img_remove)
lemma diff_ll_range:
assumes "F ⊢ ↿(ll_range (I'-I)) f p ** F'"
shows "↿(ll_range I) f p ** F ⊢ ↿(ll_range I') f p ** ↿(ll_range (I-I')) f p ** F'"
proof -
have "↿(ll_range I) f p ** F ⊢ ↿(ll_range I) f p ** ↿(ll_range (I'-I)) f p ** F'"
using assms(1) conj_entails_mono by blast
also have "… = (↿(ll_range (I ∪ (I'-I))) f p ** F')"
apply (subst ll_range_merge[symmetric])
by auto
also have "… = ((↿(ll_range I') f p ** ↿(ll_range (I-I')) f p) ** F')"
apply (rewrite in "_=⌑" ll_range_merge)
apply (auto simp: Un_commute)
done
finally show ?thesis by simp
qed
subsubsection ‹Load and Store›
context llvm_prim_mem_setup begin
lemma checked_from_val_rule[vcg_rules]: "llvm_htriple (□) (checked_from_val (to_val x)) (λr. ↑(r=x))"
unfolding checked_from_val_def
by vcg
find_theorems "HT " pure_part
text ‹Standard rules for load and store from pointer›
lemma ll_load_rule[vcg_rules]: "llvm_htriple (↿ll_pto x p) (ll_load p) (λr. ↑(r=x) ** ↿ll_pto x p)"
unfolding ll_load_def ll_pto_def llvm_load_def llvm_extract_addr_def to_val_ptr_def
apply (simp add: llvm_pto_def split!: llvm_ptr.splits)
apply vcg
done
lemma ll_store_rule[vcg_rules]: "llvm_htriple (↿ll_pto xx p) (ll_store x p) (λ_. ↿ll_pto x p)"
unfolding ll_store_def ll_pto_def llvm_store_def llvm_extract_addr_def to_val_ptr_def
apply (simp add: llvm_pto_def split!: llvm_ptr.splits)
apply vcg
done
text ‹Rules for load and store from indexed pointer, wrt. range›
lemmas [fri_extract_simps] = sep_conj_assoc
lemma ll_load_rule_range[vcg_rules]:
shows "llvm_htriple (↿(ll_range I) a p ** ↑⇩!( p' ~⇩a p ∧ p' -⇩a p ∈ I )) (ll_load p') (λr. ↑(r = a (p' -⇩a p)) ** ↿(ll_range I) a p)"
apply vcg
apply (clarsimp simp: open_ll_range)
apply vcg
done
lemma ll_store_rule_range[vcg_rules]:
shows "llvm_htriple (↿(ll_range I) a p ** ↑⇩!( p' ~⇩a p ∧ p' -⇩a p ∈ I )) (ll_store x p') (λ_. ↿(ll_range I) (a(p' -⇩a p := x)) p)"
apply vcg
apply (clarsimp simp: open_ll_range)
apply vcg
done
lemma ll_load_rule_range':
shows "llvm_htriple (↿(ll_range I) a p ** ↑⇩!( ofs ∈ I )) (ll_load (p +⇩a ofs)) (λr. ↑(r = a ofs) ** ↿(ll_range I) a p)"
apply vcg
done
lemma ll_store_rule_range':
shows "llvm_htriple (↿(ll_range I) a p ** ↑⇩!( ofs ∈ I )) (ll_store x (p +⇩a ofs)) (λ_. ↿(ll_range I) (a(ofs := x)) p)"
apply vcg
apply (clarsimp simp: open_ll_range)
apply vcg
done
subsubsection ‹Offsetting Pointers›
lemma [vcg_normalize_simps]: "llvm_extract_sint (to_val i) = Mreturn (sint i)"
unfolding llvm_extract_sint_def to_val_word_def
by (simp add: sint_uint)
lemma [vcg_normalize_simps]: "llvm_extract_unat (to_val n) = Mreturn (unat n)"
unfolding llvm_extract_unat_def to_val_word_def
by (auto split: llvm_val.split)
lemma abase_is_ptr[simp]: "abase (the_raw_ptr p) ⟹ llvm_ptr.is_addr (the_raw_ptr p)"
unfolding abase_ptr_def apply (cases p) subgoal for lp apply (cases lp) apply auto done done
text ‹Rule for indexing pointer. Note, the new target address must exist›
lemma from_val_LL_PTR[simp]: "from_val (LL_PTR p) = PTR p"
unfolding from_val_ptr_def by simp
lemma ll_ofs_ptr_rule[vcg_rules]:
"llvm_htriple
(↿ll_pto v (p +⇩a (sint i)) ** ↑⇩!(abase p))
(ll_ofs_ptr p i)
(λr. ↑(r= p +⇩a (sint i)) ** ↿ll_pto v (p +⇩a (sint i)))"
unfolding ll_ofs_ptr_def llvm_ofs_ptr_def llvm_extract_ptr_def ll_pto_def abase_ptr_def aidx_ptr_def
to_val_ptr_def
apply vcg
done
text ‹Rule for indexing pointer into range. Note, the new target address must exist›
lemma ll_ofs_ptr_rule'[vcg_rules]:
shows "llvm_htriple
(↿(ll_range I) x p ** ↑⇩!(p ~⇩a p' ∧ (p' +⇩a sint i) -⇩a p ∈ I))
(ll_ofs_ptr p' i)
(λr. ↑(r= p' +⇩a sint i) ** ↿(ll_range I) x p)"
apply vcg
apply (clarsimp simp: open_ll_range)
apply vcg
done
subsubsection ‹Allocate and Free›
text ‹Memory allocation tag, which expresses ownership of an allocated block.›
definition ll_malloc_tag :: "int ⇒ 'a::llvm_rep ptr ⇒ _"
where "ll_malloc_tag n p ≡ ↑(n≥0) ** llvm_blockp (the_raw_ptr p) (nat n)"
lemma abase_ptr_iff: "abase (PTR r) ⟷ abase r"
by (simp add: abase_ptr_def)
lemma the_raw_PTR_aidx: "the_raw_ptr (PTR r +⇩a x) = r +⇩a x"
by (simp add: aidx_ptr_def)
lemma range_split_last: "l≤h ⟹ {l..<1+h} = insert h {l..<h}" for l h :: int by auto
lemma llvm_blockv_Nil[simp]: "llvm_blockv [] b = 0"
by (simp add: llvm_blockv_def)
lemma block_base_abase[simp]: "llvm_ptr_is_block_base p ⟹ abase (PTR p)"
by (cases p; auto simp: llvm_ptr_is_block_base_def abase_ptr_def)
lemma llvm_pto_is_ato: "⟦llvm_ptr.is_addr p; addr.index (llvm_ptr.the_addr p) ≥ 0⟧
⟹ llvm_pto x p = EXACT (llvm_ato x (llvm_ptr.the_addr p))"
by (cases p; simp add: llvm_pto_def)
find_theorems "to_val (from_val _)"
lemma range_split_aux: "(⋃*i∈{0..<int (length xs)}. llvm_pto (to_val ((from_val ((xs @ [x]) ! nat i)) :: 'a :: llvm_rep )) (f i))
= (⋃*i∈{0..<int (length xs)}. llvm_pto (to_val ((from_val (xs ! nat i)) :: 'a )) (f i))"
apply (rule sep_set_img_cong)
apply (auto)
done
lemma is_addr_add[simp]: "llvm_ptr.is_addr (p +⇩a i) ⟷ llvm_ptr.is_addr p"
by (cases p; auto)
lemma addr_idx_the_addr_add[simp]: "llvm_ptr.is_addr p ⟹ addr.index (llvm_ptr.the_addr (p +⇩a i)) = addr.index (llvm_ptr.the_addr p) + i"
by (cases p) auto
lemma blockv_range_conv:
"⟦llvm_ptr_is_block_base p; ∀x∈set xs. llvm_struct_of_val x = struct_of TYPE('a::llvm_rep) ⟧ ⟹
EXACT (llvm_blockv xs (llvm_ptr_the_block p))
= (↿(ll_range {0..<int (length xs)}) (λi. from_val (xs ! nat i) :: 'a ) (PTR p))"
apply (induction xs rule: rev_induct)
apply (auto simp: ll_range_def range_split_last sep_algebra_simps EXACT_split ll_pto_def)
apply (auto simp: llvm_ptr_is_block_base_def range_split_aux the_raw_PTR_aidx)
apply (auto simp: llvm_pto_is_ato llvm_ptr_is_block_base_def range_split_aux the_raw_PTR_aidx)
apply (subst sep_conj_commute)
apply (cases p; simp)
by (smt (z3) fold_addr_add llvm_ptr.sel llvm_ptr_the_block_def)
lemma blockvp_range_conv:
assumes "∀x∈set xs. llvm_struct_of_val x = struct_of TYPE('a::llvm_rep)"
shows "llvm_blockvp xs p = (↑(llvm_ptr_is_block_base p) ** ↿(ll_range {0..<int (length xs)}) (λi. from_val (xs!nat i) :: 'a) (PTR p))"
unfolding llvm_blockvp_def
apply (cases "llvm_ptr_is_block_base p"; simp add: sep_algebra_simps blockv_range_conv assms)
done
lemma ll_range_init_conv_aux: "↿(ll_range {0..<uint n}) (λi. from_val (replicate (unat n) (llvm_zero_initializer (struct_of TYPE('a::llvm_rep))) ! nat i)) p
= ↿(ll_range {0..<uint n}) (λ_. init::'a) p"
apply (cases "abase p"; simp add: ll_range_def sep_algebra_simps)
apply (rule sep_set_img_cong; clarsimp)
subgoal for i
apply (subgoal_tac "nat i < unat n")
apply simp
subgoal by (metis from_to_id' init_zero)
subgoal by (metis Word.of_nat_unat nat_less_iff)
done
done
text ‹Allocation returns an array-base pointer to an initialized range,
as well as an allocation tag›
lemma ll_malloc_rule[vcg_rules]:
"llvm_htriple
(↑(n≠0))
(ll_malloc TYPE('a::llvm_rep) n)
(λr. ↿(ll_range {0..< uint n}) (λ_. init) r ** ll_malloc_tag (uint n) r)"
unfolding ll_malloc_def ll_pto_def ll_malloc_tag_def llvm_alloc_def
supply [simp] = unat_gt_0 abase_ptr_iff the_raw_PTR_aidx blockvp_range_conv ll_range_init_conv_aux
apply vcg
done
lemma llvm_blockvp_empty[simp]: "llvm_blockvp [] p = ↑llvm_ptr_is_block_base p"
unfolding llvm_blockvp_def by simp
lemma llvm_ptr_is_block_base_NULL[simp]: "¬llvm_ptr_is_block_base PTR_NULL" by (simp add: llvm_ptr_is_block_base_def)
lemma llvm_blockvp_split[simp]: "llvm_blockvp (xs@[x]) p = (llvm_blockvp xs p ** llvm_pto x (p +⇩a (int (length xs))))"
unfolding llvm_blockvp_def
apply (cases p; simp add: sep_algebra_simps llvm_pto_def EXACT_split)
apply (auto simp: )
subgoal for pp
apply (cases pp; auto simp add: llvm_ptr_is_block_base_def llvm_ptr_the_block_def sep_algebra_simps)
done
subgoal by (simp add: llvm_ptr_is_block_base_def)
done
lemma free_blockvp_aux:
assumes [simp]: "llvm_ptr_is_block_base p"
shows "(⋃*i∈{0..<n}. llvm_pto (to_val (f i)) (p +⇩a i)) = llvm_blockvp (map (to_val o f o int) [0..<nat n]) p"
proof -
have 1: "{0..<Suc n} = insert n {0..<n}" for n by auto
have A: "(⋃*i∈{0..<n}. llvm_pto (to_val (f (int i))) (p +⇩a int i)) = llvm_blockvp (map (to_val o f o int) [0..<n]) p"
for n :: nat
apply (induction n)
apply (auto simp: sep_algebra_simps 1 sep_conj_c)
done
have B: "n≥0 ⟹ {0..<nat n} = nat`{0..<n}"
apply (induction "nat n" arbitrary: n)
apply auto
by (metis image_atLeastZeroLessThan_int image_eqI int_nat_eq lessThan_iff of_nat_0_le_iff of_nat_eq_iff)
show ?thesis
apply (cases "n≥0"; (simp add: sep_algebra_simps)?)
using A[of "nat n"]
apply (simp add: B)
apply (subst (asm) sep_set_img_map)
subgoal by (simp add: eq_nat_nat_iff inj_on_def)
by simp
qed
text ‹Free takes a range and the matching allocation tag›
lemma ll_free_rule[vcg_rules]:
"llvm_htriple
(↿(ll_range {0..<n}) blk p ** ll_malloc_tag n p)
(ll_free p)
(λ_. □)
"
unfolding ll_free_def ll_pto_def ll_malloc_tag_def ll_range_def vcg_tag_defs llvm_free_def
llvm_extract_ptr_def to_val_ptr_def
apply (cases p; simp)
subgoal for pp
apply (cases "llvm_ptr_is_block_base pp")
subgoal
supply [simp] = list_conj_eq_sep_set_img abase_ptr_def aidx_ptr_def
supply [named_ss fri_prepare_simps] = sep_set_img_pull_EXS
apply (simp add: )
apply (simp add: sep_algebra_simps)
apply (subst free_blockvp_aux)
apply vcg
supply [vcg_rules] = llvmt_freep_rule[where xs="map _ [0..<nat n]", simplified]
apply vcg
done
subgoal by (simp add: llvm_blockp_def)
done
done
end
subsection ‹Arithmetic Instructions›
text ‹Tag for arithmetic bounds check proof obligations›
definition [vcg_tag_defs]: "WBOUNDS Φ ⟷ Φ"
lemma WBOUNDSI: "Φ ⟹ WBOUNDS Φ" by (simp add: WBOUNDS_def)
lemma WBOUNDSD: "WBOUNDS Φ ⟹ Φ" by (simp add: WBOUNDS_def)
declaration ‹K (Basic_VCG.add_solver (@{thms WBOUNDSI},@{binding solve_wbounds},fn ctxt => SELECT_GOAL (auto_tac ctxt)))›
abbreviation "in_srange op (a::'a::len word) (b::'a word) ≡ op (sint a) (sint b) ∈ sints (LENGTH ('a))"
lemma udivrem_is_undef_word_conv:
fixes a b :: "'a::len word"
shows "udivrem_is_undef (word_to_lint a) (word_to_lint b) ⟷ b=0"
by (auto simp: udivrem_is_undef_def word_to_lint_to_uint_0_iff)
lemma sdivrem_is_undef_word_conv:
fixes a b :: "'a::len word"
shows "sdivrem_is_undef (word_to_lint a) (word_to_lint b) ⟷ b=0 ∨ ¬in_srange (sdiv) a b"
by (auto simp: sdivrem_is_undef_def sdivrem_ovf_def word_to_lint_to_sint_conv)
subsubsection ‹VCG Simplifications and Rules›
text ‹
Most of the rules for arithmetic are set up as simplifications.
For operations with side-conditions, we have both,
a conditional simplification rule and a Hoare-rule.
Note that the Hoare-rule will only be tried if the simplification rule did not
succeed.
›
lemma cond_llvm_htripleI: "x = Mreturn y ⟹ llvm_htriple □ x (λr. ↑(r=y))" by vcg
locale llvm_prim_arith_setup
sublocale llvm_prim_setup < llvm_prim_arith_setup .
definition "vcg_assert_valid_ptr p ≡ llvmt_check_ptr (the_raw_ptr p)"
context llvm_prim_arith_setup begin
context
notes [simp] = op_lift_arith2'_def op_lift_arith2_def
op_lift_farith1_f_def op_lift_farith2_f_def
op_lift_farith1_d_def op_lift_farith2_d_def
op_lift_farith1_rm_f_def op_lift_farith2_rm_f_def op_lift_farith3_rm_f_def
op_lift_farith1_rm_d_def op_lift_farith2_rm_d_def op_lift_farith3_rm_d_def
op_lift_cmp_def op_lift_iconv_def
notes [simp] = word_to_lint_convs[symmetric]
notes [simp] = from_bool_lint_conv udivrem_is_undef_word_conv sdivrem_is_undef_word_conv
notes [simp] = word_to_lint_to_uint_conv word_to_lint_to_sint_conv
begin
paragraph ‹Arithmetic›
lemma ll_add_simp[vcg_normalize_simps]: "ll_add a b = Mreturn (a + b)" by (auto simp: ll_add_def)
lemma ll_sub_simp[vcg_normalize_simps]: "ll_sub a b = Mreturn (a - b)" by (auto simp: ll_sub_def)
lemma ll_mul_simp[vcg_normalize_simps]: "ll_mul a b = Mreturn (a * b)" by (auto simp: ll_mul_def)
lemma ll_udiv_simp[vcg_normalize_simps]: "b≠0 ⟹ ll_udiv a b = Mreturn (a div b)" by (auto simp: ll_udiv_def)
lemma ll_urem_simp[vcg_normalize_simps]: "b≠0 ⟹ ll_urem a b = Mreturn (a mod b)" by (auto simp: ll_urem_def)
lemma ll_sdiv_simp[vcg_normalize_simps]: "⟦b≠0; in_srange (sdiv) a b⟧ ⟹ ll_sdiv a b = Mreturn (a sdiv b)"
by (auto simp: ll_sdiv_def Let_def)
lemma ll_srem_simp[vcg_normalize_simps]: "⟦b≠0; in_srange (sdiv) a b⟧ ⟹ ll_srem a b = Mreturn (a smod b)"
by (auto simp: ll_srem_def)
lemma ll_udiv_rule[vcg_rules]: "WBOUNDS (b≠0) ⟹ llvm_htriple □ (ll_udiv a b) (λr. ↑(r = a div b))"
unfolding vcg_tag_defs by vcg
lemma ll_urem_rule[vcg_rules]: "WBOUNDS (b≠0) ⟹ llvm_htriple □ (ll_urem a b) (λr. ↑(r = a mod b))"
unfolding vcg_tag_defs by vcg
lemma ll_sdiv_rule[vcg_rules]: "⟦WBOUNDS (b≠0); WBOUNDS (in_srange (sdiv) a b)⟧ ⟹ llvm_htriple □ (ll_sdiv a b) (λr. ↑(r = a sdiv b))"
unfolding vcg_tag_defs by vcg
lemma ll_srem_rule[vcg_rules]: "⟦WBOUNDS (b≠0); WBOUNDS (in_srange (sdiv) a b)⟧ ⟹ llvm_htriple □ (ll_srem a b) (λr. ↑(r = a smod b))"
unfolding vcg_tag_defs by vcg
lemma ll_fadd_f_simp[vcg_normalize_simps]: "ll_fadd_f a b = nanize_single (a + b)" by (auto simp: ll_fadd_f_def)
lemma ll_fsub_f_simp[vcg_normalize_simps]: "ll_fsub_f a b = nanize_single (a - b)" by (auto simp: ll_fsub_f_def)
lemma ll_fmul_f_simp[vcg_normalize_simps]: "ll_fmul_f a b = nanize_single (a * b)" by (auto simp: ll_fmul_f_def)
lemma ll_fdiv_f_simp[vcg_normalize_simps]: "ll_fdiv_f a b = nanize_single (a / b)" by (auto simp: ll_fdiv_f_def)
lemma ll_frem_f_simp[vcg_normalize_simps]: "ll_frem_f a b = nanize_single (srem a b)" by (auto simp: ll_frem_f_def)
lemma ll_sqrt_f32_simp[vcg_normalize_simps]: "ll_sqrt_f32 a = nanize_single (ssqrt a)" by (auto simp: ll_sqrt_f32_def)
lemma ll_fadd_d_simp[vcg_normalize_simps]: "ll_fadd_d a b = nanize_double (a + b)" by (auto simp: ll_fadd_d_def)
lemma ll_fsub_d_simp[vcg_normalize_simps]: "ll_fsub_d a b = nanize_double (a - b)" by (auto simp: ll_fsub_d_def)
lemma ll_fmul_d_simp[vcg_normalize_simps]: "ll_fmul_d a b = nanize_double (a * b)" by (auto simp: ll_fmul_d_def)
lemma ll_fdiv_d_simp[vcg_normalize_simps]: "ll_fdiv_d a b = nanize_double (a / b)" by (auto simp: ll_fdiv_d_def)
lemma ll_frem_d_simp[vcg_normalize_simps]: "ll_frem_d a b = nanize_double (drem a b)" by (auto simp: ll_frem_d_def)
lemma ll_sqrt_f64_simp[vcg_normalize_simps]: "ll_sqrt_f64 a = nanize_double (dsqrt a)" by (auto simp: ll_sqrt_f64_def)
lemmas [vcg_normalize_simps] = xlate_rounding_mode_simps
lemma ll_x86_avx512_ss_simps[vcg_normalize_simps]:
"ll_x86_avx512_add_ss_round rm a b = doM {rm ← xlate_rounding_mode rm; nanize_single (sradd rm a b)}"
"ll_x86_avx512_sub_ss_round rm a b = doM {rm ← xlate_rounding_mode rm; nanize_single (srsub rm a b)}"
"ll_x86_avx512_mul_ss_round rm a b = doM {rm ← xlate_rounding_mode rm; nanize_single (srmul rm a b)}"
"ll_x86_avx512_div_ss_round rm a b = doM {rm ← xlate_rounding_mode rm; nanize_single (srdiv rm a b)}"
"ll_x86_avx512_sqrt_ss rm a = doM {rm ← xlate_rounding_mode rm; nanize_single (srsqrt rm a)}"
"ll_x86_avx512_vfmadd_f32 rm a b c = doM {rm ← xlate_rounding_mode rm; nanize_single (srfmadd rm a b c)}"
unfolding
ll_x86_avx512_add_ss_round_def
ll_x86_avx512_sub_ss_round_def
ll_x86_avx512_mul_ss_round_def
ll_x86_avx512_div_ss_round_def
ll_x86_avx512_sqrt_ss_def
ll_x86_avx512_vfmadd_f32_def
by auto
lemma ll_x86_avx512_sd_simps[vcg_normalize_simps]:
"ll_x86_avx512_add_sd_round rm a b = doM {rm ← xlate_rounding_mode rm; nanize_double (dradd rm a b)}"
"ll_x86_avx512_sub_sd_round rm a b = doM {rm ← xlate_rounding_mode rm; nanize_double (drsub rm a b)}"
"ll_x86_avx512_mul_sd_round rm a b = doM {rm ← xlate_rounding_mode rm; nanize_double (drmul rm a b)}"
"ll_x86_avx512_div_sd_round rm a b = doM {rm ← xlate_rounding_mode rm; nanize_double (drdiv rm a b)}"
"ll_x86_avx512_sqrt_sd rm a = doM {rm ← xlate_rounding_mode rm; nanize_double (drsqrt rm a)}"
"ll_x86_avx512_vfmadd_f64 rm a b c = doM {rm ← xlate_rounding_mode rm; nanize_double (drfmadd rm a b c)}"
unfolding
ll_x86_avx512_add_sd_round_def
ll_x86_avx512_sub_sd_round_def
ll_x86_avx512_mul_sd_round_def
ll_x86_avx512_div_sd_round_def
ll_x86_avx512_sqrt_sd_def
ll_x86_avx512_vfmadd_f64_def
by auto
paragraph ‹Comparison›
lemma ll_icmp_simps[vcg_normalize_simps]:
"ll_icmp_eq a b = Mreturn (from_bool (a = b))"
"ll_icmp_ne a b = Mreturn (from_bool (a ≠ b))"
"ll_icmp_sle a b = Mreturn (from_bool (a <=s b))"
"ll_icmp_slt a b = Mreturn (from_bool (a <s b))"
"ll_icmp_ule a b = Mreturn (from_bool (a ≤ b))"
"ll_icmp_ult a b = Mreturn (from_bool (a < b))"
unfolding ll_icmp_eq_def ll_icmp_ne_def ll_icmp_sle_def ll_icmp_slt_def ll_icmp_ule_def ll_icmp_ult_def
by auto
definition [vcg_normalize_simps]: "check_ptrs_cmp p⇩1 p⇩2 = (
if p⇩1=null ∨ p⇩2=null then Mreturn () else doM { vcg_assert_valid_ptr p⇩1; vcg_assert_valid_ptr p⇩2; Mreturn ()})"
lemma word1_to_lint_ltrue: "word_to_lint (1::1 word) = ltrue"
unfolding word_to_lint_def ltrue_def by auto
lemma word1_to_lint_lfalse: "word_to_lint (0::1 word) = lfalse"
unfolding word_to_lint_def lfalse_def by auto
lemma ll_ptrcmp_simps[vcg_normalize_simps]:
"ll_ptrcmp_eq a b = doM { check_ptrs_cmp a b; Mreturn (from_bool (a = b))}"
"ll_ptrcmp_ne a b = doM { check_ptrs_cmp a b; Mreturn (from_bool (a ≠ b))}"
unfolding ll_ptrcmp_eq_def ll_ptrcmp_ne_def check_ptrs_cmp_def llvm_ptr_eq_def llvm_ptr_neq_def llvm_extract_ptr_def
unfolding to_val_ptr_def null_def
subgoal
apply (cases a; cases b; auto simp: vcg_normalize_simps from_val_word_def)
subgoal by (auto simp: word1_to_lint_lfalse word1_to_lint_ltrue bool_to_lint_def)
subgoal by (auto simp: word1_to_lint_lfalse word1_to_lint_ltrue bool_to_lint_def)
unfolding vcg_assert_valid_ptr_def llvmt_ptr_eq_def llvmt_check_ptrcmp_def
apply (auto simp: lint_to_word_def)
done
subgoal
apply (cases a; cases b; auto simp: vcg_normalize_simps from_val_word_def)
subgoal by (auto simp: word1_to_lint_lfalse word1_to_lint_ltrue bool_to_lint_def)
subgoal by (auto simp: word1_to_lint_lfalse word1_to_lint_ltrue bool_to_lint_def)
unfolding vcg_assert_valid_ptr_def llvmt_ptr_neq_def llvmt_check_ptrcmp_def
apply (auto simp: lint_to_word_def)
done
done
lemma ll_fcmp_f_simp[vcg_normalize_simps]:
"ll_fcmp_oeq_f a b = Mreturn (from_bool (¬is_nan_single a ∧ ¬is_nan_single b ∧ eq_single a b))"
"ll_fcmp_ogt_f a b = Mreturn (from_bool (¬is_nan_single a ∧ ¬is_nan_single b ∧ a > b))"
"ll_fcmp_oge_f a b = Mreturn (from_bool (¬is_nan_single a ∧ ¬is_nan_single b ∧ a ≥ b))"
"ll_fcmp_olt_f a b = Mreturn (from_bool (¬is_nan_single a ∧ ¬is_nan_single b ∧ a < b))"
"ll_fcmp_ole_f a b = Mreturn (from_bool (¬is_nan_single a ∧ ¬is_nan_single b ∧ a ≤ b))"
"ll_fcmp_one_f a b = Mreturn (from_bool (¬is_nan_single a ∧ ¬is_nan_single b ∧ ¬eq_single a b))"
"ll_fcmp_ord_f a b = Mreturn (from_bool (¬is_nan_single a ∧ ¬is_nan_single b))"
"ll_fcmp_ueq_f a b = Mreturn (from_bool (is_nan_single a ∨ is_nan_single b ∨ eq_single a b))"
"ll_fcmp_ugt_f a b = Mreturn (from_bool (is_nan_single a ∨ is_nan_single b ∨ a > b))"
"ll_fcmp_uge_f a b = Mreturn (from_bool (is_nan_single a ∨ is_nan_single b ∨ a ≥ b))"
"ll_fcmp_ult_f a b = Mreturn (from_bool (is_nan_single a ∨ is_nan_single b ∨ a < b))"
"ll_fcmp_ule_f a b = Mreturn (from_bool (is_nan_single a ∨ is_nan_single b ∨ a ≤ b))"
"ll_fcmp_une_f a b = Mreturn (from_bool (is_nan_single a ∨ is_nan_single b ∨ ¬eq_single a b))"
"ll_fcmp_uno_f a b = Mreturn (from_bool (is_nan_single a ∨ is_nan_single b))"
unfolding
ll_fcmp_oeq_f_def
ll_fcmp_ogt_f_def
ll_fcmp_oge_f_def
ll_fcmp_olt_f_def
ll_fcmp_ole_f_def
ll_fcmp_one_f_def
ll_fcmp_ord_f_def
ll_fcmp_ueq_f_def
ll_fcmp_ugt_f_def
ll_fcmp_uge_f_def
ll_fcmp_ult_f_def
ll_fcmp_ule_f_def
ll_fcmp_une_f_def
ll_fcmp_uno_f_def
apply (auto simp: op_lift_fcmp_f_def)
done
lemma ll_fcmp_d_simp[vcg_normalize_simps]:
"ll_fcmp_oeq_d a b = Mreturn (from_bool (¬is_nan_double a ∧ ¬is_nan_double b ∧ eq_double a b))"
"ll_fcmp_ogt_d a b = Mreturn (from_bool (¬is_nan_double a ∧ ¬is_nan_double b ∧ a > b))"
"ll_fcmp_oge_d a b = Mreturn (from_bool (¬is_nan_double a ∧ ¬is_nan_double b ∧ a ≥ b))"
"ll_fcmp_olt_d a b = Mreturn (from_bool (¬is_nan_double a ∧ ¬is_nan_double b ∧ a < b))"
"ll_fcmp_ole_d a b = Mreturn (from_bool (¬is_nan_double a ∧ ¬is_nan_double b ∧ a ≤ b))"
"ll_fcmp_one_d a b = Mreturn (from_bool (¬is_nan_double a ∧ ¬is_nan_double b ∧ ¬eq_double a b))"
"ll_fcmp_ord_d a b = Mreturn (from_bool (¬is_nan_double a ∧ ¬is_nan_double b))"
"ll_fcmp_ueq_d a b = Mreturn (from_bool (is_nan_double a ∨ is_nan_double b ∨ eq_double a b))"
"ll_fcmp_ugt_d a b = Mreturn (from_bool (is_nan_double a ∨ is_nan_double b ∨ a > b))"
"ll_fcmp_uge_d a b = Mreturn (from_bool (is_nan_double a ∨ is_nan_double b ∨ a ≥ b))"
"ll_fcmp_ult_d a b = Mreturn (from_bool (is_nan_double a ∨ is_nan_double b ∨ a < b))"
"ll_fcmp_ule_d a b = Mreturn (from_bool (is_nan_double a ∨ is_nan_double b ∨ a ≤ b))"
"ll_fcmp_une_d a b = Mreturn (from_bool (is_nan_double a ∨ is_nan_double b ∨ ¬eq_double a b))"
"ll_fcmp_uno_d a b = Mreturn (from_bool (is_nan_double a ∨ is_nan_double b))"
unfolding
ll_fcmp_oeq_d_def
ll_fcmp_ogt_d_def
ll_fcmp_oge_d_def
ll_fcmp_olt_d_def
ll_fcmp_ole_d_def
ll_fcmp_one_d_def
ll_fcmp_ord_d_def
ll_fcmp_ueq_d_def
ll_fcmp_ugt_d_def
ll_fcmp_uge_d_def
ll_fcmp_ult_d_def
ll_fcmp_ule_d_def
ll_fcmp_une_d_def
ll_fcmp_uno_d_def
apply (auto simp: op_lift_fcmp_d_def)
done
paragraph ‹Bitwise›
lemma ll_and_simp[vcg_normalize_simps]: "ll_and a b = Mreturn (a AND b)" by (auto simp: ll_and_def)
lemma ll_or_simp[vcg_normalize_simps]: "ll_or a b = Mreturn (a OR b)" by (auto simp: ll_or_def)
lemma ll_xor_simp[vcg_normalize_simps]: "ll_xor a b = Mreturn (a XOR b)" by (auto simp: ll_xor_def)
lemma ll_shl_simp[vcg_normalize_simps]: "unat b < LENGTH ('a) ⟹ ll_shl (a::'a::len word) b = Mreturn (a << unat b)"
by (auto simp: ll_shl_def Let_def shift_ovf_def bitSHL'_def)
lemma ll_lshr_simp[vcg_normalize_simps]: "unat b < LENGTH ('a) ⟹ ll_lshr (a::'a::len word) b = Mreturn (a >> unat b)"
by (auto simp: ll_lshr_def Let_def shift_ovf_def bitLSHR'_def)
lemma ll_ashr_simp[vcg_normalize_simps]: "unat b < LENGTH ('a) ⟹ ll_ashr (a::'a::len word) b = Mreturn (a >>> unat b)"
by (auto simp: ll_ashr_def Let_def shift_ovf_def bitASHR'_def)
lemma [vcg_rules]:
fixes a b :: "'a::len word"
assumes "WBOUNDS (unat b < LENGTH ('a))"
shows ll_shl_rule: "llvm_htriple □ (ll_shl a b) (λr. ↑(r=a<<unat b))"
and ll_lshr_rule: "llvm_htriple □ (ll_lshr a b) (λr. ↑(r=a>>unat b))"
and ll_ashr_rule: "llvm_htriple □ (ll_ashr a b) (λr. ↑(r=a>>>unat b))"
using assms unfolding vcg_tag_defs
by vcg
paragraph ‹Conversion›
lemma ll_trunc_simp[vcg_normalize_simps]: "is_down' UCAST ('a→'b) ⟹ ll_trunc (a::'a::len word) TYPE('b::len word) = Mreturn (UCAST ('a→'b) a)"
by (auto simp: ll_trunc_def llb_trunc_def Let_def)
lemma ll_zext_simp[vcg_normalize_simps]: "is_up' UCAST ('a→'b) ⟹ ll_zext (a::'a::len word) TYPE('b::len word) = Mreturn (UCAST ('a→'b) a)"
by (auto simp: ll_zext_def llb_zext_def Let_def)
lemma ll_sext_simp[vcg_normalize_simps]: "is_up' SCAST ('a→'b) ⟹ ll_sext (a::'a::len word) TYPE('b::len word) = Mreturn (SCAST ('a→'b) a)"
by (auto simp: ll_sext_def llb_sext_def Let_def)
lemmas ll_trunc_rule[vcg_rules] = cond_llvm_htripleI[OF ll_trunc_simp, OF WBOUNDSD]
lemmas ll_zext_rule[vcg_rules] = cond_llvm_htripleI[OF ll_zext_simp, OF WBOUNDSD]
lemmas ll_sext_rule[vcg_rules] = cond_llvm_htripleI[OF ll_sext_simp, OF WBOUNDSD]
end
end
context llvm_prim_mem_setup begin
lemma vcg_assert_valid_ptr_rule[vcg_rules]: "llvm_htriple (↿ll_pto x p) (vcg_assert_valid_ptr p) (λ_. ↿ll_pto x p)"
unfolding vcg_assert_valid_ptr_def ll_pto_def
apply vcg
done
end
subsection ‹Control Flow›
locale llvm_prim_ctrl_setup
sublocale llvm_prim_setup < llvm_prim_ctrl_setup .
context llvm_prim_ctrl_setup begin
text ‹The if command is handled by a set of normalization rules.
Note that the VCG will split on the introduced conjunction automatically.
›
lemma llc_if_simps[vcg_normalize_simps]:
"llc_if 1 t e = t"
"r≠0 ⟹ llc_if r t e = t"
"llc_if 0 t e = e"
by (auto simp: llc_if_def)
lemma llc_if_simp[vcg_normalize_simps]: "wpa A (llc_if b t e) Q s ⟷ (to_bool b ⟶ wpa A t Q s) ∧ (¬to_bool b ⟶ wpa A e Q s)"
unfolding llc_if_def by simp
lemma if_simp[vcg_normalize_simps]: "wpa A (If b t e) Q s ⟷ (b ⟶ wpa A t Q s) ∧ (¬b ⟶ wpa A e Q s)"
by simp
end
text ‹The while command is handled by a standard invariant/variant rule.›
lemma llc_while_unfold: "llc_while b f σ = doM { ctd ← b σ; llc_if ctd (doM { σ←f σ; llc_while b f σ}) (Mreturn σ)}"
unfolding llc_while_def
unfolding llc_while_def llc_if_def
apply (rewrite Mwhile_unfold)
apply simp
done
definition llc_while_annot :: "('σ::llvm_rep ⇒ 't ⇒ llvm_amemory ⇒ bool) ⇒ ('t×'t) set ⇒ ('σ⇒1 word llM) ⇒ _"
where [llvm_pre_simp]: "llc_while_annot I R ≡ llc_while"
declare [[vcg_const "llc_while_annot I R"]]
lemma annotate_llc_while: "llc_while = llc_while_annot I R" by (simp add: llc_while_annot_def)
context llvm_prim_ctrl_setup begin
lemma basic_while_rule:
assumes "wf R"
assumes "STATE asf (I σ t) s"
assumes STEP: "⋀σ t s. ⟦ STATE asf (I σ t) s ⟧ ⟹ wpa A (b σ) (λctd s⇩1.
(to_bool ctd ⟶ wpa A (f σ) (λσ' s⇩2. STATE asf (EXS t'. I σ' t' ** ↑((t',t)∈R)) s⇩2) s⇩1)
∧ (¬to_bool ctd ⟶ Q σ s⇩1)
) s"
shows "wpa A (llc_while b f σ) Q s"
using assms(1,2)
proof (induction t arbitrary: σ s)
case (less t)
show ?case
apply (subst llc_while_unfold)
apply vcg
apply (rule wpa_monoI[OF STEP])
apply fact
subgoal for r s⇩1
apply (cases "to_bool r"; simp add: vcg_normalize_simps)
apply vcg
apply (erule wpa_monoI; clarsimp; fri_extract)
apply (rule less.IH; assumption)
done
subgoal by simp
subgoal by simp
done
qed
text ‹
Standard while rule.
Note that the second parameter of the invariant is the termination measure, which must
decrease wrt. a well-founded relation. It is initialized as a schematic variable, and must be
derivable via frame inference. In practice, the invariant will contain a ‹↑(t=…)› part.
›
lemma llc_while_annot_rule[vcg_decomp_erules]:
assumes "STATE asf P s"
assumes "FRAME P (I σ t) F"
assumes WF: "SOLVE_AUTO_DEFER (wf R)"
assumes STEP: "⋀σ t s. ⟦ STATE asf ((I σ t ** F)) s ⟧ ⟹ EXTRACT (wpa A (b σ) (λctd s⇩1.
(to_bool ctd ⟶ wpa A (f σ) (λσ' s⇩2. POSTCOND asf (EXS t'. I σ' t' ** ↑((t',t)∈R) ** F) s⇩2) s⇩1)
∧ (¬to_bool ctd ⟶ Q σ s⇩1)
) s)"
shows "wpa A (llc_while_annot I R b f σ) Q s"
proof -
from ‹STATE asf P s› ‹FRAME P (I σ t) F› have PRE: "STATE asf (I σ t ** F) s"
using FRAME_def STATE_monoI by blast
note STEP'=STEP[unfolded vcg_tag_defs]
show ?thesis
unfolding llc_while_annot_def
apply (rule basic_while_rule[where I="λσ t. I σ t ** F" and R=R])
subgoal using WF unfolding vcg_tag_defs .
apply (rule PRE)
apply (erule wpa_monoI[OF STEP'])
apply auto
apply (erule wpa_monoI;simp add: sep_algebra_simps)
apply (erule wpa_monoI;simp add: sep_algebra_simps)
done
qed
end
subsection ‹LLVM Code Generator Setup›
lemma elim_higher_order_return[llvm_pre_simp]: "doM { x::_⇒_ ← Mreturn f; m x } = m f" by simp
text ‹Useful shortcuts›
subsubsection ‹Direct Arithmetic›
context begin
interpretation llvm_prim_arith_setup .
lemma arith_inlines[llvm_pre_simp, vcg_monadify_xforms]:
"Mreturn (a+b) = ll_add a b"
"Mreturn (a-b) = ll_sub a b"
"Mreturn (a*b) = ll_mul a b"
"Mreturn (a AND b) = ll_and a b"
"Mreturn (a OR b) = ll_or a b"
"Mreturn (a XOR b) = ll_xor a b"
by vcg
lemma farith_inlines_f[llvm_pre_simp, vcg_monadify_xforms]:
"nanize_single (a+b) = ll_fadd_f a b"
"nanize_single (a-b) = ll_fsub_f a b"
"nanize_single (a*b) = ll_fmul_f a b"
"nanize_single (a/b) = ll_fdiv_f a b"
"nanize_single (srem a b) = ll_frem_f a b"
"nanize_single (ssqrt a) = ll_sqrt_f32 a"
by vcg
lemma farith_inlines_d[llvm_pre_simp, vcg_monadify_xforms]:
"nanize_double (a+b) = ll_fadd_d a b"
"nanize_double (a-b) = ll_fsub_d a b"
"nanize_double (a*b) = ll_fmul_d a b"
"nanize_double (a/b) = ll_fdiv_d a b"
"nanize_double (drem a b) = ll_frem_d a b"
"nanize_double (dsqrt a) = ll_sqrt_f64 a"
by vcg
term sqrt
end
text ‹Activates AVX512f for Isabelle/LLVM ›
locale llvm_avx512f_setup begin
declare [[llc_compile_avx512f]]
context begin
interpretation llvm_prim_arith_setup .
fun avx512_rm where
"avx512_rm To_nearest = AVX512_FROUND_TO_NEAREST_NO_EXC"
| "avx512_rm float_To_zero = AVX512_FROUND_TO_ZERO_NO_EXC"
| "avx512_rm To_pinfinity = AVX512_FROUND_TO_POS_INF_NO_EXC"
| "avx512_rm To_ninfinity = AVX512_FROUND_TO_NEG_INF_NO_EXC"
lemmas [llvm_pre_simp] = avx512_rm.simps
lemma avx512_arith_inlines[llvm_pre_simp]:
"nanize_double (dradd rm a b) = ll_x86_avx512_add_sd_round (avx512_rm rm) a b"
"nanize_double (drsub rm a b) = ll_x86_avx512_sub_sd_round (avx512_rm rm) a b"
"nanize_double (drmul rm a b) = ll_x86_avx512_mul_sd_round (avx512_rm rm) a b"
"nanize_double (drdiv rm a b) = ll_x86_avx512_div_sd_round (avx512_rm rm) a b"
"nanize_double (drsqrt rm a) = ll_x86_avx512_sqrt_sd (avx512_rm rm) a"
"nanize_double (drfmadd rm a b c) = ll_x86_avx512_vfmadd_f64 (avx512_rm rm) a b c"
by (cases rm; vcg)+
lemma avx512_arith_inlines_ss[llvm_pre_simp]:
"nanize_single (sradd rm a b) = ll_x86_avx512_add_ss_round (avx512_rm rm) a b"
"nanize_single (srsub rm a b) = ll_x86_avx512_sub_ss_round (avx512_rm rm) a b"
"nanize_single (srmul rm a b) = ll_x86_avx512_mul_ss_round (avx512_rm rm) a b"
"nanize_single (srdiv rm a b) = ll_x86_avx512_div_ss_round (avx512_rm rm) a b"
"nanize_single (srsqrt rm a) = ll_x86_avx512_sqrt_ss (avx512_rm rm) a"
"nanize_single (srfmadd rm a b c) = ll_x86_avx512_vfmadd_f32 (avx512_rm rm) a b c"
by (cases rm; vcg)+
end
end
subsubsection ‹Direct Comparison›
abbreviation (input) ll_cmp' :: "bool ⇒ 1 word" where "ll_cmp' ≡ from_bool"
definition [vcg_monadify_xforms,llvm_inline]: "ll_cmp b ≡ Mreturn (ll_cmp' b)"
definition "ll_cmp'_eq a b ≡ ll_cmp' (a=b)"
definition "ll_cmp'_ne a b ≡ ll_cmp' (a≠b)"
definition "ll_cmp'_ule a b ≡ ll_cmp' (a≤b)" for a b :: "_ word"
definition "ll_cmp'_ult a b ≡ ll_cmp' (a<b)" for a b :: "_ word"
definition "ll_cmp'_sle a b ≡ ll_cmp' (a <=s b)" for a b :: "_ word"
definition "ll_cmp'_slt a b ≡ ll_cmp' (a <s b)" for a b :: "_ word"
definition "ll_cmp'_fle_f a b ≡ ll_cmp' (a≤b)" for a b :: "single"
definition "ll_cmp'_flt_f a b ≡ ll_cmp' (a<b)" for a b :: "single"
definition "ll_cmp'_fle_d a b ≡ ll_cmp' (a≤b)" for a b :: "double"
definition "ll_cmp'_flt_d a b ≡ ll_cmp' (a<b)" for a b :: "double"
lemmas ll_cmp'_defs = ll_cmp'_eq_def ll_cmp'_ne_def ll_cmp'_ule_def ll_cmp'_ult_def ll_cmp'_sle_def ll_cmp'_slt_def
ll_cmp'_fle_f_def ll_cmp'_flt_f_def
ll_cmp'_fle_d_def ll_cmp'_flt_d_def
lemmas [llvm_pre_simp, vcg_monadify_xforms] = ll_cmp'_defs[symmetric]
lemma fcompare_has_ord_semantics:
"a<b ⟹ ¬is_nan_single a ∧ ¬is_nan_single b"
"a≤b ⟹ ¬is_nan_single a ∧ ¬is_nan_single b"
apply (all transfer')
unfolding less_float_def less_eq_float_def flt_def fle_def fcompare_def
by auto
lemma fcompare_ord_conv:
"¬ is_nan_single a ∧ ¬ is_nan_single b ∧ a < b ⟷ a < b"
"¬ is_nan_single a ∧ ¬ is_nan_single b ∧ a ≤ b ⟷ a ≤ b"
using fcompare_has_ord_semantics by blast+
lemma dcompare_has_ord_semantics:
"a<b ⟹ ¬is_nan_double a ∧ ¬is_nan_double b"
"a≤b ⟹ ¬is_nan_double a ∧ ¬is_nan_double b"
apply (all transfer')
unfolding less_float_def less_eq_float_def flt_def fle_def fcompare_def
by auto
lemma dcompare_ord_conv:
"¬ is_nan_double a ∧ ¬ is_nan_double b ∧ a < b ⟷ a < b"
"¬ is_nan_double a ∧ ¬ is_nan_double b ∧ a ≤ b ⟷ a ≤ b"
using dcompare_has_ord_semantics by blast+
context begin
interpretation llvm_prim_arith_setup .
lemma ll_cmp'_xforms[vcg_monadify_xforms,llvm_pre_simp]:
"Mreturn (ll_cmp'_eq a b) = ll_icmp_eq a b"
"Mreturn (ll_cmp'_ne a b) = ll_icmp_ne a b"
"Mreturn (ll_cmp'_ult a b) = ll_icmp_ult a b"
"Mreturn (ll_cmp'_ule a b) = ll_icmp_ule a b"
"Mreturn (ll_cmp'_slt a b) = ll_icmp_slt a b"
"Mreturn (ll_cmp'_sle a b) = ll_icmp_sle a b"
unfolding ll_cmp_def ll_cmp'_defs
by (all vcg_normalize)
lemma ll_cmp'_float_xforms[vcg_monadify_xforms,llvm_pre_simp]:
"Mreturn (ll_cmp'_flt_f a b) = ll_fcmp_olt_f a b"
"Mreturn (ll_cmp'_fle_f a b) = ll_fcmp_ole_f a b"
unfolding ll_cmp'_defs
apply (all vcg_normalize)
apply (simp_all add: fcompare_ord_conv)
done
lemma ll_cmp'_double_xforms[vcg_monadify_xforms,llvm_pre_simp]:
"Mreturn (ll_cmp'_flt_d a b) = ll_fcmp_olt_d a b"
"Mreturn (ll_cmp'_fle_d a b) = ll_fcmp_ole_d a b"
unfolding ll_cmp'_defs
apply (all vcg_normalize)
apply (simp_all add: dcompare_ord_conv)
done
text ‹Comparison with null pointers can be transformed automatically.
Any other pointer comparisons carry additional precondition, and cannot
be generated from pure statements.›
definition "ll_eq_null a ≡ ll_cmp'_eq a null"
definition "ll_ne_null a ≡ ll_cmp'_ne a null"
lemma ll_ptrcmp'_xforms[vcg_monadify_xforms,llvm_pre_simp]:
"Mreturn (ll_eq_null a) = ll_ptrcmp_eq a null"
"Mreturn (ll_ne_null a) = ll_ptrcmp_ne a null"
"ll_cmp'_eq a null = ll_eq_null a"
"ll_cmp'_eq null b = ll_eq_null b"
"ll_cmp'_ne a null = ll_ne_null a"
"ll_cmp'_ne null b = ll_ne_null b"
unfolding ll_cmp_def ll_cmp'_defs ll_eq_null_def ll_ne_null_def
by (all ‹vcg_normalize; simp add: eq_commute[of null]›)
end
subsubsection ‹Boolean Operations›
lemma llvm_if_inline[llvm_pre_simp,vcg_monadify_xforms]: "If b t e = llc_if (from_bool b) t e"
by (auto simp: llc_if_def)
lemma from_bool_to_bool1[llvm_pre_simp]: "from_bool (to_bool (x::1 word)) = x"
by (metis from_bool_1 to_bool_eq word1_cases)
lemma (in llvm_prim_arith_setup) llvm_from_bool_inline[llvm_pre_simp]:
"from_bool (a∧b) = (from_bool a AND from_bool b)"
"from_bool (a∨b) = (from_bool a OR from_bool b)"
"(from_bool (¬a)::1 word) = (1 - (from_bool a :: 1 word))"
subgoal by (metis and.idem and_zero_eq bit.conj_zero_left from_bool_eq_if')
subgoal by (smt (z3) from_bool_0 or.idem word_bw_comms(2) word_log_esimps(3))
subgoal by (metis (full_types) cancel_comm_monoid_add_class.diff_cancel diff_zero from_bool_eq_if')
done
subsubsection ‹Products›
lemma inline_prod_case[llvm_pre_simp]: "(λ(a,b). f a b) = (λx. doM { a←prod_extract_fst x; b ← prod_extract_snd x; f a b })"
by (auto simp: prod_ops_simp)
lemma inline_return_prod_case[llvm_pre_simp]:
"Mreturn (case x of (a,b) ⇒ f a b) = (case x of (a,b) ⇒ Mreturn (f a b))" by (rule prod.case_distrib)
lemma inline_return_prod[llvm_pre_simp]: "Mreturn (a,b) = doM { x ← prod_insert_fst init a; x ← prod_insert_snd x b; Mreturn x }"
by (auto simp: prod_ops_simp)
lemma :
"ll_extract_value (a,b) 0 = Mreturn a"
"ll_extract_value (a,b) 1 = Mreturn b"
unfolding ll_extract_value_def llvm_extract_value_def checked_from_val_def
by auto
txt ‹This lemma removes insert-extracts artifacts.
This makes code lemmas smaller, and can speed up preprocessing significantly.›
lemma ins_extr_prod_simp[llvm_pre_simp]: "doM {
(x::'a::llvm_rep × 'b::llvm_rep) ← ll_insert_value init a 0;
x ← ll_insert_value x b Numeral1;
a::'a ← ll_extract_value x 0;
b::'b ← ll_extract_value x Numeral1;
f a b
} = f a b"
apply (simp add: ll_insert_value_def ll_extract_value_def llvm_insert_value_def llvm_extract_value_def checked_from_val_def)
done
subsubsection ‹Marking of constants›
definition "ll_const x ≡ Mreturn x"
lemma ll_const_inline[llvm_pre_simp]: "Mbind (ll_const x) f = f x" by (auto simp: ll_const_def)
declare [[vcg_const "numeral a"]]
declare [[vcg_const "ll_const c"]]
section ‹Data Refinement›
locale standard_opr_abstraction =
fixes α :: "'c ⇒ 'a"
and I :: "'c ⇒ bool"
and dflt_PRE1 :: "('a⇒'a) ⇒ 'c itself ⇒ 'a ⇒ bool"
and dflt_PRE2 :: "('a⇒'a⇒'a) ⇒ 'c itself ⇒ 'a ⇒ 'a ⇒ bool"
and dflt_EPURE :: "'a ⇒ 'c ⇒ bool"
assumes dflt_EPURE_correct: "⋀c. I c ⟹ dflt_EPURE (α c) c"
begin
definition "assn ≡ mk_pure_assn (λa c. I c ∧ a=α c)"
lemma assn_pure[is_pure_rule]: "is_pure assn"
by (auto simp: assn_def)
lemma vcg_prep_delete_assn[vcg_prep_ext_rules]:
"pure_part (↿assn a c) ⟹ dflt_EPURE a c"
by (auto simp: assn_def dflt_EPURE_correct)
definition "is_un_op PRE cop mop aop ≡
(∀a::'c. I a ∧ PRE TYPE('c) (α a) ⟶ I (mop a) ∧ α (mop a) = aop (α a) ∧ cop a = Mreturn (mop a))"
definition "is_bin_op PRE cop mop aop ≡
(∀a b::'c. I a ∧ I b ∧ PRE TYPE('c) (α a) (α b) ⟶ I (mop a b) ∧ α (mop a b) = aop (α a) (α b) ∧ cop a b = Mreturn (mop a b))"
abbreviation "is_un_op' cop mop aop ≡ is_un_op (dflt_PRE1 aop) cop mop aop"
abbreviation "is_bin_op' cop mop aop ≡ is_bin_op (dflt_PRE2 aop) cop mop aop"
lemma is_un_opI[intro?]:
assumes "⋀a. ⟦I a; PRE TYPE('c) (α a)⟧ ⟹ cop a = Mreturn (mop a)"
assumes "⋀a. ⟦I a; PRE TYPE('c) (α a)⟧ ⟹ I (mop a)"
assumes "⋀a. ⟦I a; PRE TYPE('c) (α a)⟧ ⟹ α (mop a) = aop (α a)"
shows "is_un_op PRE cop mop aop"
using assms unfolding is_un_op_def by blast
lemma is_bin_opI[intro?]:
assumes "⋀a b. ⟦I a; I b; PRE TYPE('c) (α a) (α b)⟧ ⟹ cop a b = Mreturn (mop a b)"
assumes "⋀a b. ⟦I a; I b; PRE TYPE('c) (α a) (α b)⟧ ⟹ I (mop a b)"
assumes "⋀a b. ⟦I a; I b; PRE TYPE('c) (α a) (α b)⟧ ⟹ α (mop a b) = aop (α a) (α b)"
shows "is_bin_op PRE cop mop aop"
using assms unfolding is_bin_op_def by blast
lemma un_op_tmpl:
fixes w :: "'c"
assumes A: "is_un_op PRE cop mop aop"
shows "llvm_htriple
(↿assn i w ** ↑⇩d(PRE TYPE('c) i))
(cop w)
(λr. ↿assn (aop i) r ** ↿assn i w)
"
proof -
interpret llvm_prim_arith_setup .
show ?thesis
using A
unfolding is_un_op_def assn_def apply clarsimp
by vcg
qed
lemma bin_op_tmpl:
fixes w⇩1 w⇩2 :: "'c"
assumes A: "is_bin_op PRE cop mop aop"
shows "llvm_htriple
(↿assn i⇩1 w⇩1 ** ↿assn i⇩2 w⇩2 ** ↑⇩d(PRE TYPE('c) i⇩1 i⇩2))
(cop w⇩1 w⇩2)
(λr. ↿assn (aop i⇩1 i⇩2) r ** ↿assn i⇩1 w⇩1 ** ↿assn i⇩2 w⇩2)
"
proof -
interpret llvm_prim_arith_setup .
show ?thesis
using A
unfolding is_bin_op_def assn_def apply clarsimp
by vcg
qed
end
interpretation bool: standard_opr_abstraction "to_bool::1 word ⇒ bool" "λ_. True" ‹λ_ _ _. True› ‹λ_ _ _ _. True› "λ_ _. True"
by standard auto
context standard_opr_abstraction begin
definition "is_cmp_op cop mop aop ≡
(∀a b. I a ∧ I b ⟶ (cop a b = Mreturn (from_bool (mop a b)) ∧ (mop a b ⟷ aop (α a) (α b))))"
lemma is_cmp_opI[intro?]:
assumes "⋀a b. ⟦I a; I b⟧ ⟹ cop a b = Mreturn (from_bool (mop a b))"
assumes "⋀a b. ⟦I a; I b⟧ ⟹ mop a b ⟷ aop (α a) (α b)"
shows "is_cmp_op cop mop aop"
using assms unfolding is_cmp_op_def by blast
lemma cmp_op_tmpl:
fixes w⇩1 w⇩2 :: "'c"
assumes "is_cmp_op cop mop aop"
shows "llvm_htriple
(↿assn i⇩1 w⇩1 ** ↿assn i⇩2 w⇩2)
(cop w⇩1 w⇩2)
(λr. ↿bool.assn (aop i⇩1 i⇩2) r ** ↿assn i⇩1 w⇩1 ** ↿assn i⇩2 w⇩2)
"
using assms unfolding is_cmp_op_def assn_def bool.assn_def apply clarsimp
by vcg
end
subsection ‹Booleans›
lemma to_bool_logics:
fixes a b :: "1 word"
shows "to_bool (a&&b) ⟷ to_bool a ∧ to_bool b"
and "to_bool (a||b) ⟷ to_bool a ∨ to_bool b"
and "to_bool (a XOR b) ⟷ to_bool a ≠ to_bool b"
and "to_bool (NOT a) ⟷ ¬to_bool a"
apply (cases a; cases b; simp; fail)
apply (cases a; cases b; simp; fail)
apply (cases a; cases b; simp; fail)
apply (cases a; simp; fail)
done
context begin
interpretation llvm_prim_arith_setup .
abbreviation (input) ll_not1 :: "1 word ⇒ 1 word llM" where "ll_not1 x ≡ ll_add x 1"
lemma ll_not1_inline[llvm_pre_simp]: "Mreturn (~~x) ≡ ll_not1 x"
by (auto simp: word1_NOT_eq arith_inlines)
lemma bool_bin_ops:
"bool.is_bin_op' ll_and (AND) (∧)"
"bool.is_bin_op' ll_or (OR) (∨)"
"bool.is_bin_op' ll_xor (XOR) (≠)"
apply (all ‹rule›)
apply (simp_all only: to_bool_logics)
apply (all ‹vcg_normalize?›)
done
lemma bool_un_ops:
"bool.is_un_op' ll_not1 (NOT) Not"
apply (all ‹rule›)
apply (simp_all only: to_bool_logics)
apply (all ‹vcg_normalize?›)
apply (simp_all add: word1_NOT_eq)
done
lemmas bool_op_rules[vcg_rules] =
bool_bin_ops[THEN bool.bin_op_tmpl]
bool_un_ops[THEN bool.un_op_tmpl]
end
subsection ‹Control Flow›
definition "ABSTRACT asf c ty P s ≡ ∃F a. STATE asf (↿ty a c ** F) s ∧ P a"
lemma ABSTRACT_erule[vcg_decomp_erules]:
assumes "STATE asf P s"
assumes "FRAME P (↿ty a c) F"
assumes "STATE asf (↿ty a c ** F) s ⟹ EXTRACT (Q a)"
shows "ABSTRACT asf c ty Q s"
using assms
by (force simp: FRAME_def ABSTRACT_def STATE_def entails_def vcg_tag_defs)
context begin
interpretation llvm_prim_arith_setup + llvm_prim_ctrl_setup .
lemma dr_normalize_llc_if[vcg_normalize_simps]:
"♭⇩pbool.assn b bi ⟹ wpa A (llc_if bi t e) Q s ⟷ ((b ⟶ wpa A t Q s) ∧ (¬b⟶wpa A e Q s))"
unfolding bool.assn_def by vcg_normalize
lemma llc_while_annot_dr_rule[vcg_decomp_erules]:
assumes "STATE asf P s"
assumes "FRAME P (I σ t) F"
assumes WF: "SOLVE_AUTO_DEFER (wf R)"
assumes STEP: "⋀σ t s. ⟦ STATE asf ((I σ t ** F)) s ⟧ ⟹ EXTRACT (wpa A (b σ) (λctdi s⇩1.
ABSTRACT asf ctdi bool.assn (λctd.
(ctd ⟶ wpa A (f σ) (λσ' s⇩2. POSTCOND asf (EXS t'. I σ' t' ** ↑⇩d((t',t)∈R) ** F) s⇩2) s⇩1)
∧ (¬ctd ⟶ Q σ s⇩1)
) s⇩1
) s)"
shows "wpa A (llc_while_annot I R b f σ) Q s"
using assms(1) apply -
apply vcg_rl
apply fact
apply fact
apply (drule STEP)
apply (simp add: fri_extract_simps vcg_tag_defs bool.assn_def)
apply (simp add: ABSTRACT_def)
apply (erule wpa_monoI)
apply auto
done
end
end