theory SE_Graph
imports
Step_Prime
SE_Graph_Pre
begin
section ‹Playing with bundle and notation›
bundle IA_formula_notation
begin
notation IA.implies (infix "⟹⇩I⇩A" 41)
notation IA.satisfies (infix "⊨⇩I⇩A" 40)
notation IA.eval ("⟦(_)⟧⇩I⇩A")
notation form_and (infixl "∧⇩f" 42)
end
bundle no_IA_formula_notation
begin
no_notation IA.implies (infix "⟹⇩I⇩A" 41)
no_notation IA.satisfies (infix "⊨⇩I⇩A" 40)
no_notation IA.eval ("⟦(_)⟧⇩I⇩A")
no_notation form_and (infixl "∧⇩f" 42)
end
unbundle IA_formula_notation
section ‹Abstract states, mappings, etc›
type_synonym 'lv abstract_state = "(LLVM_Syntax.pos, name, 'lv) abstract_state"
inductive valid_var_mapping for
cs :: "(name, llvm_constant) mapping" and as :: "name ⇀ 'v" and ev :: "'v × IA.ty ⇒ IA.val"
where
"valid_var_mapping cs as ev"
if
"⋀l i lv pv. Mapping.lookup cs pv = Some (IntConstant l i)
⟹ as pv = Some lv
⟹ ev (lv, IA.IntT) = IA.Int i"
inductive same_stack_names for cs :: "(name, llvm_constant) mapping" and as where
"same_stack_names cs as"
if
"⋀n. (Mapping.lookup cs n ≠ None) = (as n ≠ None)"
inductive represents_frame for f as v where
"represents_frame f as v"
if
"frame.pos f = pos as"
"same_stack_names (frame.stack f) (abstract_state.stack as)"
"IA.assignment v"
"valid_var_mapping (frame.stack f) (abstract_state.stack as) v"
"IA.satisfies v (kb as)"
inductive represents_state for fs as where
"represents_state fs as"
if "frames fs ≠ []" and "represents_frame (hd (frames fs)) as v"
lemma
"represents_state fs as"
if "frames fs ≠ []" and "represents_frame (hd (frames fs)) as v"
apply(rule represents_state.intros)
using that by auto
lemmas represents_simps = represents_state.simps represents_frame.simps
fun encode_var where
"encode_var v = (Var (v, IA.IntT))"
fun encode_const where
"encode_const i = Fun (IA.ConstF i) []"
fun encode_sig :: "IA.sig ⇒ _ IA.exp ⇒ _ IA.exp ⇒ _ IA.formula" where
"encode_sig s e⇩1 e⇩2 = Atom (Fun s [e⇩1, e⇩2])"
fun encode_eq :: "_ IA.exp ⇒ _ IA.exp ⇒ _ IA.formula" where
"encode_eq e⇩1 e⇩2 = encode_sig IA.EqF e⇩1 e⇩2"
fun encode_binop :: "binop_instruction ⇒ _ ⇒ _ IA.exp ⇒ _ IA.exp ⇒ _ IA.formula" where
"encode_binop Mul v t⇩1 t⇩2 = encode_eq (encode_var v) (Fun (IA.ProdF 2) [t⇩1, t⇩2])"
| "encode_binop Add v t⇩1 t⇩2 = encode_eq (encode_var v) (Fun (IA.SumF 2) [t⇩1, t⇩2])"
| "encode_binop Sub v t⇩1 t⇩2 = encode_eq (encode_var v)
(Fun (IA.SumF 2) [t⇩1, Fun (IA.ProdF 2) [Fun (IA.ConstF (-1)) [], t⇩2]])"
| "encode_binop Xor v t⇩1 t⇩2 = True⇩f"
fun encode_pred :: "integerPredicate ⇒ _ IA.exp ⇒ _ IA.exp ⇒ _ IA.formula" where
"encode_pred LLVM_Syntax.SLT t⇩1 t⇩2 = encode_sig IA.LessF t⇩1 t⇩2"
| "encode_pred LLVM_Syntax.SGT t⇩1 t⇩2 = encode_sig IA.LessF t⇩2 t⇩1"
| "encode_pred LLVM_Syntax.EQ t⇩1 t⇩2 = encode_sig IA.EqF t⇩1 t⇩2"
| "encode_pred LLVM_Syntax.SLE t⇩1 t⇩2 = encode_sig IA.LeF t⇩1 t⇩2"
| "encode_pred LLVM_Syntax.SGE t⇩1 t⇩2 = encode_sig IA.LeF t⇩2 t⇩1"
| "encode_pred LLVM_Syntax.NE t⇩1 t⇩2 = NegAtom (Fun IA.EqF [t⇩1, t⇩2])"
fun assig_of_frame :: "frame ⇒ name × IA.ty ⇒ IA.val" where
"assig_of_frame f (n,IA.IntT) = IA.Int (integerValue (the (Mapping.lookup (frame.stack f) n)))"
| "assig_of_frame f (n,IA.BoolT) = IA.Bool undefined"
definition assig_of_state :: "llvm_state ⇒ name × IA.ty ⇒ IA.val" where
"assig_of_state st = assig_of_frame (hd (frames st))"
lemma same_stack_names_def': "same_stack_names cs as =
(∀n. (∃l i. Mapping.lookup cs n = Some (IntConstant l i)) = (as n ≠ None))"
unfolding same_stack_names.simps by (auto) (metis llvm_constant.exhaust)+
lemma assignment_assig_of_frame: "IA.assignment (assig_of_frame f)"
proof -
have "assig_of_frame f (a, b) ∈ IA.Values_of_type b" for a b
by (cases b) auto
then show ?thesis
unfolding IA.assignment_def by (auto)
qed
lemma assignment_assig_of_state: "IA.assignment (assig_of_state cs)"
unfolding assig_of_state_def using assignment_assig_of_frame by blast
fun operand_value :: "'v abstract_state ⇒ operand ⇒ ('v IA.exp) option" where
"operand_value as (LocalReference n) = map_option (λv. Var (v, IA.IntT)) ((stack as) n)" |
"operand_value as (ConstantOperand (IntConstant l i)) = Some (Fun (IA.ConstF i) [])"
inductive update_as for as⇩1 as⇩2 :: "'v abstract_state" and n v⇩n φ where
"update_as as⇩1 as⇩2 n v⇩n φ"
if
"Some v⇩n ∉ range (stack as⇩1)"
"(v⇩n, IA.IntT) ∉ vars_formula (kb as⇩1)"
"stack as⇩2 = ((stack as⇩1)(n ↦ v⇩n))"
"IA.implies (kb as⇩1 ∧⇩f φ) (kb as⇩2)"
lemma operand_value_fresh: assumes
"operand_value as⇩1 op = Some t" "update_as as⇩1 as⇩2 n v⇩n φ"
shows "(v⇩n, IA.IntT) ∉ vars_term t"
proof (cases op)
case (LocalReference n)
then show ?thesis using assms apply (auto simp add: image_def update_as.simps) by metis
next
case (ConstantOperand x2)
then show ?thesis using assms by (cases x2, auto intro: llvm_constant.exhaust)
qed
lemma ssn_update:
assumes
"update_as as⇩1 as⇩2 n v⇩n φ"
"same_stack_names s (stack as⇩1)"
"s' = Mapping.update n (IntConstant l i) s"
shows "same_stack_names s' (stack as⇩2)"
using assms unfolding same_stack_names.simps
by (auto simp add: lookup_update' elim: update_as.induct)
lemma vvm_update:
assumes "valid_var_mapping s (stack as⇩1) v" "update_as as⇩1 as⇩2 n v⇩n φ"
"v' = v ((v⇩n, IA.IntT) := IA.Int i)"
"s' = Mapping.update n (IntConstant l i) s"
shows "valid_var_mapping s' (stack as⇩2) v'"
proof -
show ?thesis
unfolding valid_var_mapping.simps using assms rangeI
apply(auto simp add: lookup_update lookup_update' valid_var_mapping.simps
update_as.simps)
by (metis rangeI)
qed
lemma operand_value_valid_var_mapping:
assumes op: "operand_value as op = Some t"
and step: "small_step.operand_value f op = Inr (IntConstant l i)"
and val: "valid_var_mapping (frame.stack f) (abstract_state.stack as) v"
shows "IA.to_int (IA.eval t v) = i"
proof (cases op)
case (ConstantOperand c)
thus ?thesis using op step by (cases c, auto simp: small_step.operand_value.simps)
next
case (LocalReference n)
thus ?thesis using op step val[unfolded valid_var_mapping.simps, rule_format, of n]
by (cases "Mapping.lookup (frame.stack f) n",
auto simp: small_step.operand_value.simps)
qed
fun new_b_id_pos where
"new_b_id_pos (fn, _, _) new_b_id = (fn, new_b_id, 0)"
inductive evalAsInf for prog as⇩1 as⇩2 where
"find_statement prog (pos as⇩1) = Inr (Instruction (Named n (Binop binop o⇩1 o⇩2))) ⟹
pos as⇩2 = inc_pos (pos as⇩1) ⟹
operand_value as⇩1 o⇩1 = Some t⇩1 ⟹
operand_value as⇩1 o⇩2 = Some t⇩2 ⟹
φ = encode_binop binop v⇩n t⇩1 t⇩2 ⟹
update_as as⇩1 as⇩2 n v⇩n φ ⟹
evalAsInf prog as⇩1 as⇩2"
lemma evalAsInf_represents_step: "evalAsInf prog as⇩1 as⇩2 ⟹
represents_state cs⇩1 as⇩1 ⟹
step prog cs⇩1 = Inr cs⇩2 ⟹
represents_state cs⇩2 as⇩2 ∧ as_as_step as⇩1 as⇩2 (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
proof(induction rule: evalAsInf.induct)
case (1 n binop o⇩1 o⇩2 t⇩1 t⇩2 φ v⇩n)
note u = `update_as as⇩1 as⇩2 n v⇩n φ`
define ins where "ins = (Named n (Binop binop o⇩1 o⇩2))"
obtain f⇩1 fs⇩1 where cs⇩1: "cs⇩1 = Llvm_state (f⇩1 # fs⇩1)"
using 1 unfolding represents_state.simps by (metis hd_Cons_tl llvm_state.collapse)
interpret small_step prog cs⇩1 f⇩1 fs⇩1 .
have [simp]: "hd (frames cs⇩1) = f⇩1"
by (simp add: cs⇩1)
obtain fn bn p where p: "pos as⇩1 = (fn, bn, p)"
using prod_cases3 by blast
then have p': "frame.pos f⇩1 = (fn, bn, p)"
using 1 cs⇩1 by (auto simp add: represents_state.simps represents_frame.simps)
have "Inr cs⇩2 = step prog (Llvm_state (f⇩1 # fs⇩1))"
using cs⇩1 1 by auto
also have "… = run_instruction ins"
using 1(1) p p' ins_def cs⇩1 by (auto)
finally have cs⇩2': "run_instruction ins = Inr cs⇩2"
by simp
then obtain l i l' i' where
li_def: "operand_value o⇩1 = Inr (IntConstant l i)" "operand_value o⇩2 = Inr (IntConstant l' i')"
by (auto simp add: ins_def split: sum_bind_splits elim: binop_llvm_constant.elims)
define f⇩2 where "f⇩2 = LLVM_Syntax.update_stack
(λ_. Mapping.update n (IntConstant l' (binop_instruction binop i i')) (frame.stack f⇩1))
(update_pos (λ_. (fn, bn, Suc p)) f⇩1)"
have cs⇩2: "cs⇩2 = Llvm_state (f⇩2#fs⇩1)"
using cs⇩2' li_def unfolding ins_def f⇩2_def
by (auto simp add: p' ins_def split: if_splits sum_bind_splits intro: frame.expand)
obtain v where v: "represents_frame f⇩1 as⇩1 v"
using 1 unfolding represents_state.simps by auto
define v⇩2 where "v⇩2 = v((v⇩n, IA.IntT) := IA.Int (binop_instruction binop i i'))"
have [simp]: "IA.assignment v⇩2"
using v unfolding v⇩2_def represents_frame.simps by fastforce
have [simp]: "v⇩2 ⊨⇩I⇩A kb as⇩1"
using u v by (simp add: update_as.simps represents_frame.simps v⇩2_def)
have ttii [simp]: "IA.to_int (⟦t⇩1⟧⇩I⇩A v⇩2) = i" "IA.to_int (⟦t⇩2⟧⇩I⇩A v⇩2) = i'"
unfolding v⇩2_def
using "1.hyps"(3,4) cs⇩1 li_def operand_value_valid_var_mapping represents_frame.simps
operand_value_fresh u v IA.eval_with_fresh_var by smt+
have [simp]: "v⇩2 ⊨⇩I⇩A φ"
unfolding `φ = encode_binop binop v⇩n t⇩1 t⇩2` by (cases binop) (auto, auto simp add: v⇩2_def)
have [simp]: "v⇩2 ⊨⇩I⇩A kb as⇩2"
apply(rule IA.impliesD[of "kb as⇩1 ∧⇩f φ"])
using update_as.simps u apply(metis)
using represents_frame.simps by (auto)
have as⇩1_v⇩2: "IA.Int (integerValue (the (Mapping.lookup (frame.stack f⇩1) m))) = v⇩2 (lv, IA.IntT)"
if t: "stack as⇩1 m = Some lv" for m lv
proof -
obtain ll ii where look: "Mapping.lookup (frame.stack f⇩1) m = Some (IntConstant ll ii)"
using v cs⇩1 t unfolding same_stack_names_def' represents_frame.simps by fastforce+
have lvvn: "lv ≠ v⇩n"
using t by (metis u update_as.simps rangeI)
then have "v⇩2 (lv, IA.IntT) = v (lv, IA.IntT)"
unfolding v⇩2_def by simp
then show ?thesis
by (metis llvm_constant.sel(2) look option.sel represents_frame.cases that v
valid_var_mapping.cases)
qed
have a: "same_stack_names (Mapping.update n (IntConstant l' (binop_instruction binop i i')) (frame.stack f⇩1))
(abstract_state.stack as⇩2)"
apply(rule ssn_update[of as⇩1 _ n v⇩n φ])
using u 1 unfolding cs⇩1 by (auto simp add: represents_state.simps represents_frame.simps)
have r_f⇩2_v⇩2: "represents_frame f⇩2 as⇩2 v⇩2"
apply(auto simp add: f⇩2_def represents_frame.simps)
subgoal
using 1 by (auto simp add: p)
subgoal using a by simp
apply(rule vvm_update[OF _ u, of "frame.stack f⇩1" v, where l=l' ])
using represents_frame.cases v apply blast
using v⇩2_def apply(blast)
using 1 by (blast)
have "represents_state cs⇩2 as⇩2"
unfolding cs⇩2 represents_state.simps using r_f⇩2_v⇩2 1 by (auto)
moreover have "as_as_step as⇩1 as⇩2 (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
apply(rule as_as_step.intros[where v=v⇩2 and v'=v⇩2])
using 1 assignment_assig_of_state apply(auto)[6]
defer
unfolding assig_of_state_def using u unfolding update_as.simps apply(auto)
apply (simp add: cs⇩2 f⇩2_def lookup_update' v⇩2_def)
apply (simp add: as⇩1_v⇩2 cs⇩2 f⇩2_def lookup_update_neq)
apply (simp add: 1)
using "1.hyps" as⇩1_v⇩2 by blast
ultimately show ?case
by simp
qed
lemma operand_value_v_v_mapping_s_s_names:
assumes op: "operand_value as op = Some t"
and val: "valid_var_mapping (frame.stack f) (abstract_state.stack as) v"
and ssn: "same_stack_names (frame.stack f) (abstract_state.stack as)"
shows "∃l i. small_step.operand_value f op = Inr (IntConstant l i) ∧ IA.to_int (IA.eval t v) = i"
proof (cases op)
case (LocalReference x)
then obtain lv where lv: "abstract_state.stack as x = Some lv"
using op by (auto simp add: map_option_case split: option.splits)
then obtain l i where li: "Mapping.lookup (frame.stack f) x = Some (IntConstant l i)"
using ssn unfolding same_stack_names_def' by blast
then have a: "small_step.operand_value f op = Inr (IntConstant l i)"
using LocalReference by (auto simp: small_step.operand_value.simps)
have "t = (Var (lv, IA.IntT))"
using op lv LocalReference by (auto)
then have b: "IA.to_int (IA.eval t v) = i"
using val li lv by (auto elim: valid_var_mapping.induct)
show ?thesis
using a b by blast
next
case (ConstantOperand x)
then show ?thesis
using op by (cases x) (auto simp: small_step.operand_value.simps)
qed
inductive genAsInf for as⇩1 as⇩2 μ where
"pos as⇩1 = pos as⇩2 ⟹
dom (stack as⇩1) = dom (stack as⇩2) ⟹
kb as⇩1 ⟹⇩I⇩A rename_vars μ (kb as⇩2) ⟹
(∀n lv. stack as⇩2 n = Some lv ⟶ stack as⇩1 n = Some (μ lv)) ⟹
genAsInf as⇩1 as⇩2 μ"
lemma genAsInf_represents: "genAsInf as⇩1 as⇩2 μ ⟹
represents_state cs as⇩1 ⟹
represents_state cs as⇩2 ∧ as_as_step as⇩1 as⇩2 (assig_of_state cs) (assig_of_state cs) μ"
proof (induction rule: genAsInf.induct)
case (1)
have "(∃v. represents_frame f as⇩2 v) ∧ as_as_step as⇩1 as⇩2 (assig_of_frame f) (assig_of_frame f) μ"
if r: "represents_frame f as⇩1 v" for f v
proof -
have v: "valid_var_mapping (frame.stack f) (abstract_state.stack as⇩1) v" "v ⊨⇩I⇩A kb as⇩1"
"IA.assignment v"
and pos: "frame.pos f = abstract_state.pos as⇩1" and sn: "same_stack_names (frame.stack f) (abstract_state.stack as⇩1)"
using r unfolding represents_frame.simps by auto
define v' where "v' = v ∘ (map_prod μ id)"
have a: "IA.assignment v" "IA.assignment v'"
using v(3) unfolding v'_def unfolding IA.assignment_def by auto
have sn': "same_stack_names (frame.stack f) (abstract_state.stack as⇩2)"
using sn 1 unfolding same_stack_names.simps by blast
have "valid_var_mapping (frame.stack f) (abstract_state.stack as⇩2) v'"
using 1 v unfolding v'_def valid_var_mapping.simps by (auto)
moreover have kbt: "v' ⊨⇩I⇩A kb as⇩2"
proof -
have "v ⊨⇩I⇩A map_formula (rename_vars μ) (kb as⇩2)"
using v 1 a by blast
then show ?thesis
using a unfolding v'_def by (metis IA.satisfies_rename_vars comp_apply id_apply map_prod_simp)
qed
moreover have "as_as_step as⇩1 as⇩2 (assig_of_frame f) (assig_of_frame f) μ"
proof -
have "IA.Int (integerValue (the (Mapping.lookup (frame.stack f) n))) = v (lv, IA.IntT)" if
"abstract_state.stack as⇩1 n = Some lv" for lv n
using sn unfolding same_stack_names_def' apply(auto)
by (metis llvm_constant.sel(2) option.sel that v(1) valid_var_mapping.simps)
moreover have "IA.Int (integerValue (the (Mapping.lookup (frame.stack f) n))) = v (μ lv, IA.IntT)"
if "abstract_state.stack as⇩2 n = Some lv" for n lv
using sn' unfolding same_stack_names.simps apply(auto)
using "1.hyps"(4) calculation that by blast
ultimately show ?thesis
using 1 kbt v(2) assignment_assig_of_frame
by (auto intro: as_as_step.intros[OF a] simp add: v'_def)
qed
ultimately show ?thesis
unfolding represents_frame.simps
using a 1 sn pos by (auto simp add: same_stack_names.simps)
qed
then show ?case
using 1 unfolding assig_of_state_def represents_state.simps by blast
qed
inductive refineAsInf for as as⇩t as⇩f where
"pos as⇩t = pos as ⟹
pos as⇩f = pos as ⟹
stack as⇩t = stack as ⟹
stack as⇩f = stack as ⟹
kb as ∧⇩f φ ⟹⇩I⇩A kb as⇩t ⟹
kb as ∧⇩f (¬⇩f φ) ⟹⇩I⇩A kb as⇩f ⟹
refineAsInf as as⇩t as⇩f"
lemma refineAsInf_represents:
shows "refineAsInf as as⇩t as⇩f ⟹
represents_state cs as ⟹
represents_state cs as⇩t ∧ as_as_step as as⇩t (assig_of_state cs) (assig_of_state cs) id
∨ represents_state cs as⇩f ∧ as_as_step as as⇩f (assig_of_state cs) (assig_of_state cs) id"
proof (induction rule: refineAsInf.induct)
case (1 φ)
from this[unfolded represents_state.simps] obtain f fs v
where fcs: "frames cs = f # fs" and "represents_frame f as v" by (cases "frames cs", auto)
from this(2)[unfolded represents_frame.simps]
have pos: "frame.pos f = abstract_state.pos as" and
stack: "same_stack_names (frame.stack f) (stack as)" and
ass: "IA.assignment v" and
var: "valid_var_mapping (frame.stack f) (stack as) v" and
kb: "v ⊨⇩I⇩A kb as" by blast+
have "∃ as' ∈ {as⇩t, as⇩f}. v ⊨⇩I⇩A kb as'"
proof (cases "v ⊨⇩I⇩A φ")
case True
with kb ass 1(5) have "v ⊨⇩I⇩A kb as⇩t"
using IA.satisfies_and by blast
thus ?thesis by auto
next
case False
hence "v ⊨⇩I⇩A ¬⇩f φ" by auto
with kb ass 1(6) have "v ⊨⇩I⇩A kb as⇩f"
using IA.satisfies_and by blast
thus ?thesis by auto
qed
then obtain as' where as': "as' ∈ {as⇩t, as⇩f}" and kb': "v ⊨⇩I⇩A kb as'" by auto
from 1(1-2) pos as' have pos': "frame.pos f = abstract_state.pos as'"
by auto
from 1(3-4) as' have id': "stack as' = stack as" by auto
from stack id' have stack': "same_stack_names (frame.stack f) (stack as')"
by auto
from var id' have var': "valid_var_mapping (frame.stack f) (stack as') v"
by auto
have repr': "represents_frame f as' v"
unfolding represents_frame.simps
by (intro conjI pos' stack' exI[of _ v] ass var' kb')
have assig_stack: "assig_of_frame f (n, IA.IntT) = v (lv, IA.IntT)"
if "stack as n = Some lv" for n lv
using var[unfolded valid_var_mapping.simps, rule_format, OF _ that]
stack[unfolded same_stack_names_def', rule_format, of n] that by auto
have "as_as_step as as' (assig_of_state cs) (assig_of_state cs) id"
unfolding assig_of_state_def fcs list.sel using assignment_assig_of_frame assig_stack kb kb' 1
by (auto simp: id' intro: as_as_step.intros[OF ass ass, of _ _ _ _ id])
then show ?case
using repr' as' unfolding represents_state.simps fcs by auto
qed
lemma lookup_None_keys: "Mapping.lookup m n ≠ None ⟹ n ∈ Mapping.keys m"
by (simp add: domIff keys_dom_lookup)
lemma vars_formula_satisfies:
assumes "⋀x. x ∈ vars_formula f ⟹ v⇩2 x = v⇩1 x" "v⇩1 ⊨⇩I⇩A f"
shows "v⇩2 ⊨⇩I⇩A f"
using assms proof (induction f)
case (Atom x)
then have "⟦x⟧⇩I⇩A v⇩1 = ⟦x⟧⇩I⇩A v⇩2"
by force
then show ?case
using Atom by (auto)
next
case (NegAtom x)
then have "⟦x⟧⇩I⇩A v⇩1 = ⟦x⟧⇩I⇩A v⇩2"
by force
then show ?case
using NegAtom by (auto)
qed (fastforce+)
inductive phi_abstract' for as⇩1 as⇩2 x ps v⇩x t⇩x old_b_id where
"phi_abstract' as⇩1 as⇩2 x ps v⇩x t⇩x old_b_id"
if "small_step.phi_bid old_b_id ps = Some y⇩x"
"operand_value as⇩1 y⇩x = Some t⇩x" "v⇩x ∉ ran (stack as⇩1)" "stack as⇩2 x = Some v⇩x"
"v⇩x ∉ fst ` vars_formula (kb as⇩1)"
"IA.has_type t⇩x IA.IntT"
inductive phi_abstract where
"phi_abstract as⇩1 as⇩2 ((x, ps)#xs) ((v⇩x, t⇩x)#ys) old_b_id"
if "phi_abstract' as⇩1 as⇩2 x ps v⇩x t⇩x old_b_id"
"phi_abstract as⇩1 as⇩2 xs ys old_b_id"
| "phi_abstract as⇩1 as⇩2 [] [] old_b_id"
inductive branchAsInf for prog as⇩1 as⇩2 where
"find_statement prog (pos as⇩1) = Inr (Terminator t) ⟹
named_instruction t = Br new_b_id ⟹
pos as⇩1 = (f_id, old_b_id, p) ⟹
pos as⇩2 = (f_id, new_b_id, length phis_stats) ⟹
Inr phis_stats = find_phis prog f_id new_b_id ⟹
phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id ⟹
(Conjunction (map (λ(v⇩x,t⇩x). encode_eq (encode_var v⇩x) t⇩x) φs)) ∧⇩f (kb as⇩1) ⟹⇩I⇩A kb as⇩2 ⟹
inj_on (stack as⇩2) (fst ` set phis_stats) ⟹
(∀a ∈ fst ` ⋃ (vars_term ` snd ` set φs). a ∉ fst ` set φs) ⟹
(∀x ∈ dom (stack as⇩1). x ∉ (fst ` set phis_stats) ⟶ stack as⇩2 x = stack as⇩1 x) ⟹
dom (stack as⇩2) = dom (stack as⇩1) ∪ fst ` set phis_stats ⟹
distinct (map fst φs) ⟹
distinct (map fst phis_stats) ⟹
branchAsInf prog as⇩1 as⇩2"
lemma branchAsInf_represents: "branchAsInf prog as⇩1 as⇩2 ⟹
represents_state cs⇩1 as⇩1 ⟹
step prog cs⇩1 = Inr cs⇩2 ⟹
represents_state cs⇩2 as⇩2 ∧ as_as_step as⇩1 as⇩2 (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
proof (induction rule: branchAsInf.induct)
case (1 t new_b_id f_id old_b_id p phis_stats φs)
interpret successful_step prog cs⇩1 cs⇩2
by (standard) (use 1 in ‹auto simp del: step.simps›)
interpret successful_step' prog cs⇩1 cs⇩2 f_id old_b_id p
by(standard)
(use 1 in ‹auto simp add: represents_frame.simps represents_state.simps f⇩1_def simp del: step.simps›)
note frames_cs⇩1[simp]
have "c_action = Terminator t"
using 1 c_block_def' c_find_action by (auto simp del: find_fun_block.simps)
then have "Inr cs⇩2 = terminate_frame t"
using 1 c_action_Terminator by simp
also have "… = update_bid_frame new_b_id ⤜ update_frame"
using 1 c_block_def'' c_fun_def' by (auto simp add: terminate_frame_def)
finally have uu: "Inr cs⇩2 = update_bid_frame new_b_id ⤜ update_frame"
by simp
define s where "s = projr (compute_phis old_b_id phis_stats)"
define s' where "s' = foldr (λ(k,v). Mapping.update k v) s (frame.stack f⇩1)"
define f⇩2 where "f⇩2 = update_pos (λ_. (f_id, new_b_id, length phis_stats)) ((LLVM_Syntax.update_stack (λ_. s')) f⇩1)"
obtain v⇩1 where v⇩1: "represents_frame f⇩1 as⇩1 v⇩1"
using ‹represents_state cs⇩1 as⇩1› unfolding represents_state.simps by auto
define v⇩2 where "v⇩2 = (λ(v, t).
if t = IA.IntT
then case map_of φs v of Some t⇩x ⇒ (⟦t⇩x⟧⇩I⇩A v⇩1) | None ⇒ v⇩1 (v,t)
else v⇩1 (v,t))"
have s': "Mapping.lookup s' x = (case map_of s x of None ⇒ Mapping.lookup (frame.stack f⇩1) x | y ⇒ y)" for x
unfolding s'_def by (induction s) (auto simp add: lookup_update lookup_update')
have s: "compute_phis old_b_id phis_stats = Inr s"
unfolding s_def
apply(rule sum.collapse(2)[symmetric])
using uu by (auto simp add: 1(5)[symmetric] c_pos simp del: find_phis.simps split: sum_bind_splits)
have v⇩2_v⇩1: "v⇩2 (v,t) = v⇩1 (v,t)" if "v ∉ fst ` set φs" for v t
using that map_of_eq_None_iff 1(12) unfolding v⇩2_def by (auto split: option.splits)
have v⇩2_s: "v⇩2 (v,IA.IntT) = (⟦t⇩x⟧⇩I⇩A v⇩1)" if "(v,t⇩x) ∈ set φs" for v t⇩x
using that map_of_eq_Some_iff 1 unfolding v⇩2_def by (auto)
have φs_kb_as⇩1: "fst ` set φs ∩ fst ` vars_formula (kb as⇩1) = {}"
using `phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id`
by (induction rule: phi_abstract.induct) (auto simp add: phi_abstract'.simps)
have cs⇩2: "cs⇩2 = Llvm_state (f⇩2#fs⇩1)"
using uu 1(5)[symmetric] s unfolding f⇩2_def c_pos s'_def
by (auto simp add: c_pos simp del: find_phis.simps split: sum_bind_splits intro: frame.expand)
then have frames_cs⇩2[simp]: "frames cs⇩2 = (f⇩2#fs⇩1)"
by auto
then have vars_term_t⇩x: "a ∉ fst ` set φs" if "(a, b) ∈ vars_term t⇩x" "(v⇩x,t⇩x) ∈ set φs" for v⇩x a b t⇩x
using 1(9) that by blast
have t⇩x_IntT: "IA.has_type t⇩x IA.IntT" if "(v⇩x,t⇩x) ∈ set φs" for v⇩x t⇩x
using `phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id` that
by (induction rule: phi_abstract.induct) (auto simp add: phi_abstract'.simps)
have d1: "map fst s = map fst phis_stats"
using s by (induction old_b_id phis_stats arbitrary: s rule: compute_phis.induct )
(fastforce split: Option.bind_splits sum_bind_splits)+
then have d: "fst ` set s = fst ` set phis_stats"
by (metis list.set_map)
have e: "abstract_state.stack as⇩1 pv = Some lv ⟹ lv ∉ fst ` set φs" for lv pv
using `phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id`
by (induction rule: phi_abstract.induct) (auto simp add: phi_abstract'.simps ranI)
have f: "phi_abstract' as⇩1 as⇩2 pv ps lv t⇩x old_b_id"
if "abstract_state.stack as⇩2 pv = Some lv" "(lv, t⇩x) ∈ set φs" "(pv, ps) ∈ set phis_stats"
for pv lv t⇩x ps
using `phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id` that 1(12) 1(8) 1(13)
proof (induction as⇩1 as⇩2 phis_stats φs old_b_id rule: phi_abstract.induct)
case (1 as⇩1 as⇩2 x ps⇩a v⇩x t⇩x⇩a xs ys)
have "pv = x ⟷ lv = v⇩x"
apply(rule)
defer
apply(rule inj_onD)
using 1 apply(blast)
using 1(1,4) that unfolding phi_abstract'.simps apply(auto)[1]
using 1 apply(blast)
apply(simp)
using 1 unfolding phi_abstract'.simps by (auto)
then show ?case
using 1 by (auto)
next
case (2 as⇩1 as⇩2)
then show ?case by simp
qed
have g: "operand_value y⇩x = Inr (IntConstant l i)"
if "(pv, ps) ∈ set phis_stats" "phi_bid old_b_id ps = Some y⇩x" "(pv, IntConstant l i) ∈ set s"
for pv ps y⇩x l i
using 1(13) s that unfolding d1[symmetric] using 1(13)
proof (induction old_b_id phis_stats arbitrary: ps s rule: compute_phis.induct)
case (1 old_b_id a psa as)
obtain x where x: "compute_phi old_b_id psa = Inr x"
using 1 by (auto split: sum_bind_splits)
have tl_s: "compute_phis old_b_id as = Inr (tl s)"
using 1 by (auto split: sum_bind_splits)
have ?case if "pv = a"
using 1 that by force
moreover have ?case if "pv ≠ a"
apply(rule 1(1)[of _ "tl s" ps]) using x apply(simp)
using 1 apply(fastforce)
using tl_s apply(simp)
using 1 that apply(simp)
using 1 that apply(blast)
using 1 that by (fastforce)+
ultimately show ?case
by blast
qed (auto)
have h: "∃t⇩x. (lv, t⇩x) ∈ set φs" if "abstract_state.stack as⇩2 pv = Some lv" "pv ∈ fst ` set phis_stats"
for lv pv
using `phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id` that
by (induction rule: phi_abstract.induct) (auto simp add: phi_abstract'.simps ranI)
have "frame.pos (hd (frames cs⇩2)) = abstract_state.pos as⇩2"
unfolding cs⇩2 f⇩2_def using 1 by (simp)
moreover have 2: "v⇩2 ⊨⇩I⇩A kb as⇩1"
apply(rule vars_formula_satisfies[of _ _ v⇩1])
apply(auto)
apply(rule v⇩2_v⇩1)
using φs_kb_as⇩1 apply(blast)
using v⇩1 unfolding represents_frame.simps by auto
moreover have 3: "IA.assignment v⇩2"
using v⇩1 unfolding represents_frame.simps v⇩2_def IA.assignment_def apply(auto split: option.splits)
apply blast
subgoal for a x2
apply(subgoal_tac "IA.has_type x2 IA.IntT")
using IA.eval_types IA_locale.Values_of_type.simps(2) represents_frame.cases v⇩1
apply metis
using t⇩x_IntT
by (meson map_of_SomeD)
done
moreover have "v⇩2 ⊨⇩I⇩A kb as⇩2"
apply(rule IA.impliesD[of "(Conjunction (map (λ(v⇩x,t⇩x). encode_eq (encode_var v⇩x) t⇩x) φs)) ∧⇩f (kb as⇩1)"])
using 1 apply(simp)
defer
apply(auto)
apply(subst v⇩2_s) apply(simp)
apply(subst IA.eval_same_vars[of _ v⇩1 v⇩2])
apply(auto)
apply(subst v⇩2_v⇩1[symmetric])
apply(rule vars_term_t⇩x)
apply(simp) apply(auto)
using 2 apply(simp)
using 3 by simp
moreover have t: "same_stack_names (frame.stack (hd (frames cs⇩2))) (abstract_state.stack as⇩2)"
apply(rule same_stack_names.intros)
apply(auto simp add: f⇩2_def)
subgoal for n y
apply(subgoal_tac "n ∈ dom (abstract_state.stack as⇩2)")
apply(blast)
unfolding 1(11) s' apply(auto split: option.splits)
using v⇩1 unfolding represents_frame.simps same_stack_names.simps
apply(blast)
using d
by (metis domI dom_map_of_conv_image_fst list.set_map)
apply(subgoal_tac "n ∈ dom (abstract_state.stack as⇩2)")
subgoal for n y
unfolding 1(11) s' apply(auto split: option.splits)
using v⇩1 unfolding represents_frame.simps same_stack_names.simps
apply(blast)
defer
using d
by (metis img_fst list.set_map map_of_eq_None_iff)
by blast
moreover have u: "valid_var_mapping (frame.stack (hd (frames cs⇩2))) (abstract_state.stack as⇩2) v⇩2"
apply(rule valid_var_mapping.intros)
apply(clarsimp simp add: f⇩2_def s' split: option.splits)
subgoal for l i lv pv
apply(subgoal_tac "abstract_state.stack as⇩1 pv = Some lv")
apply(subst v⇩2_v⇩1)
using e apply(simp)
apply (meson represents_frame.cases v⇩1 valid_var_mapping.cases)
apply(subgoal_tac "pv ∈ dom (abstract_state.stack as⇩1)")
apply (simp add: "1.hyps"(10) d map_of_eq_None_iff)
apply(subgoal_tac "pv ∈ dom (abstract_state.stack as⇩2)")
unfolding 1 apply (simp add: domD map_of_eq_None_iff d[symmetric] )
using 1 by (metis domI)
subgoal for l i lv pv
apply(subgoal_tac "(pv, IntConstant l i) ∈ set s")
apply(subgoal_tac "∃t⇩x. (lv, t⇩x) ∈ set φs")
apply(auto)
subgoal for t⇩x
apply(subst v⇩2_s)
apply(simp)
proof (goal_cases)
note H = 1
case 1
then have "pv ∈ fst ` set phis_stats"
using d by blast
then obtain ps where ps: "(pv, ps) ∈ set phis_stats"
by auto
from f[OF 1(1) 1(4) ps, unfolded phi_abstract'.simps]
obtain y⇩x where y⇩x: "phi_bid old_b_id ps = Some y⇩x" "SE_Graph.operand_value as⇩1 y⇩x = Some t⇩x"
by auto
then show ?case
using g[OF ps y⇩x(1) 1(3)]
apply(cases y⇩x) apply(auto elim!: option_to_sum.elims)
by (meson represents_frame.cases v⇩1 valid_var_mapping.cases)
qed
subgoal apply(rule h) using d by blast+
by (simp add: map_of_SomeD)
done
moreover have "assig_of_state cs⇩1 (n, IA.IntT) = v⇩2 (lv, IA.IntT)" if "abstract_state.stack as⇩1 n = Some lv" for n lv
unfolding assig_of_state_def apply(auto) using that
apply(subst v⇩2_v⇩1)
using e apply blast
apply(subgoal_tac "Mapping.lookup (frame.stack f⇩1) n ≠ None")
apply(auto)
subgoal for y
apply(cases y)
apply(auto)
using v⇩1 unfolding represents_frame.simps valid_var_mapping.simps by (auto)
using v⇩1 unfolding represents_frame.simps same_stack_names.simps by (auto)
moreover have "assig_of_state cs⇩2 (n, IA.IntT) = v⇩2 (lv, IA.IntT)" if "abstract_state.stack as⇩2 n = Some lv " for n lv
unfolding assig_of_state_def apply(auto) using that
apply(subgoal_tac "Mapping.lookup (frame.stack f⇩2) n ≠ None")
apply(auto)
subgoal for y
apply(cases y)
apply(auto)
using u unfolding valid_var_mapping.simps by (auto)
using t unfolding same_stack_names.simps by auto
ultimately have "represents_frame (hd (frames cs⇩2)) as⇩2 v⇩2"
"as_as_step as⇩1 as⇩2 (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
using 1 assignment_assig_of_state
by (auto intro!: represents_frame.intros as_as_step.intros[of v⇩2 v⇩2])
then show ?case
unfolding represents_state.simps using 1 by auto
qed
inductive condBranchAsInf for prog as⇩1 as⇩2 where
"find_statement prog (pos as⇩1) = Inr (Terminator t) ⟹
named_instruction t = CondBr c b_id_true b_id_false ⟹
operand_value as⇩1 c = Some c' ⟹
new_b_id =
(if b then b_id_true else b_id_false) ⟹
(b ⟹ kb as⇩1 ⟹⇩I⇩A encode_eq c' (Fun (IA.ConstF 1) [])) ⟹
(¬ b ⟹ kb as⇩1 ⟹⇩I⇩A encode_eq c' (Fun (IA.ConstF 0) [])) ⟹
pos as⇩1 = (f_id, old_b_id, p) ⟹
pos as⇩2 = (f_id, new_b_id, length phis_stats) ⟹
Inr phis_stats = find_phis prog f_id new_b_id ⟹
phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id ⟹
((Conjunction (map (λ(v⇩x,t⇩x). encode_eq (encode_var v⇩x) t⇩x) φs)) ∧⇩f (kb as⇩1) ⟹⇩I⇩A kb as⇩2) ⟹
inj_on (stack as⇩2) (fst ` set phis_stats) ⟹
(∀x ∈ dom (stack as⇩1). x ∉ (fst ` set phis_stats) ⟶ stack as⇩2 x = stack as⇩1 x) ⟹
dom (stack as⇩2) = dom (stack as⇩1) ∪ fst ` set phis_stats ⟹
distinct (map fst φs) ⟹
distinct (map fst phis_stats) ⟹
(∀a ∈ fst ` ⋃ (vars_term ` snd ` set φs). a ∉ fst ` set φs) ⟹
condBranchAsInf prog as⇩1 as⇩2"
lemma condBranchAsInf_represents: "condBranchAsInf prog as⇩1 as⇩2 ⟹
represents_state cs⇩1 as⇩1 ⟹
step prog cs⇩1 = Inr cs⇩2 ⟹
represents_state cs⇩2 as⇩2 ∧ as_as_step as⇩1 as⇩2 (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
proof (induction rule: condBranchAsInf.induct)
case (1 t c b_id_true b_id_false c' new_b_id b f_id old_b_id p phis_stats φs)
interpret successful_step prog cs⇩1 cs⇩2
by (standard) (use 1 in ‹auto›)
interpret successful_step' prog cs⇩1 cs⇩2 f_id old_b_id p
by (standard) (use 1 in ‹auto simp add: represents_frame.simps represents_state.simps f⇩1_def›)
note frames_cs⇩1[simp]
define s where "s = projr (compute_phis old_b_id phis_stats)"
define s' where "s' = foldr (λ(k,v). Mapping.update k v) s (frame.stack f⇩1)"
define f⇩2 where "f⇩2 = update_pos (λ_. (f_id, new_b_id, length phis_stats)) ((LLVM_Syntax.update_stack (λ_. s')) f⇩1)"
obtain v⇩1 where v⇩1: "represents_frame f⇩1 as⇩1 v⇩1"
using ‹represents_state cs⇩1 as⇩1› unfolding represents_state.simps by auto
define v⇩2 where "v⇩2 = (λ(v, t).
if t = IA.IntT
then case map_of φs v of Some t⇩x ⇒ (⟦t⇩x⟧⇩I⇩A v⇩1) | None ⇒ v⇩1 (v,t)
else v⇩1 (v,t))"
have "∃oc. operand_value c = Inr oc"
using `SE_Graph.operand_value as⇩1 c = Some c'`
using v⇩1 unfolding represents_frame.simps same_stack_names.simps
by (cases c, auto elim: option_to_sum.elims) (force)
then obtain oc where oc: "operand_value c = Inr oc"
by blast
have "c_action = Terminator t"
using 1 c_block_def' c_find_action by (auto simp del: find_fun_block.simps)
then have a: "Inr cs⇩2 = terminate_frame t"
using 1 c_action_Terminator by simp
then have oc': "oc = IntConstant 1 0 ∨ oc = IntConstant 1 1"
using `named_instruction t = CondBr c b_id_true b_id_false` oc
by (auto simp add: terminate_frame_def elim!: condBr_to_frame.elims split: sum_bind_splits if_splits)
then have a: "Inr cs⇩2 = update_bid_frame (if oc = IntConstant 1 1 then b_id_true else b_id_false) ⤜ update_frame"
using a `named_instruction t = CondBr c b_id_true b_id_false`
using c_block_def'' c_fun_def' oc by (auto simp add: terminate_frame_def)
have "oc = IntConstant 1 1" if "b"
unfolding 1 using that oc' oc using `SE_Graph.operand_value as⇩1 c = Some c'`
using `b ⟹ kb as⇩1 ⟹⇩I⇩A encode_eq c' (Fun (IA.ConstF 1) [])`
apply(auto)
apply(cases c)
apply(auto)
using "1.hyps"(3) IA.eval.simps(1) IA.satisfies_Language oc operand_value_valid_var_mapping represents_frame.cases subset_Collect_conv v⇩1
apply smt
by (smt IA.satisfies_Language empty_iff represents_frame.cases v⇩1)
moreover have "oc = IntConstant 1 0" if "¬ b"
unfolding 1 using that oc' oc using `SE_Graph.operand_value as⇩1 c = Some c'`
using `¬ b ⟹ kb as⇩1 ⟹⇩I⇩A encode_eq c' (Fun (IA.ConstF 0) [])`
apply(auto)
apply(cases c)
apply(auto elim!: option_to_error.elims)
using "1.hyps"(3) IA.eval.simps(1) IA.satisfies_Language oc operand_value_valid_var_mapping represents_frame.cases subset_Collect_conv v⇩1
apply smt
by (smt IA.satisfies_Language empty_iff represents_frame.cases v⇩1)
ultimately have b: "new_b_id = (if oc = IntConstant 1 1 then b_id_true else b_id_false)"
unfolding 1 by (auto)
have uu: "Inr cs⇩2 = update_bid_frame new_b_id ⤜ update_frame"
using a b by simp
have s': "Mapping.lookup s' x = (case map_of s x of None ⇒ Mapping.lookup (frame.stack f⇩1) x | y ⇒ y)" for x
unfolding s'_def by (induction s) (auto simp add: lookup_update lookup_update')
have s: "compute_phis old_b_id phis_stats = Inr s"
unfolding s_def
apply(rule sum.collapse(2)[symmetric])
using uu by (auto simp add: 1(9)[symmetric] c_pos simp del: find_phis.simps split: sum_bind_splits)
have v⇩2_v⇩1: "v⇩2 (v,t) = v⇩1 (v,t)" if "v ∉ fst ` set φs" for v t
using that map_of_eq_None_iff 1(15) unfolding v⇩2_def by (auto split: option.splits)
have v⇩2_s: "v⇩2 (v,IA.IntT) = (⟦t⇩x⟧⇩I⇩A v⇩1)" if "(v,t⇩x) ∈ set φs" for v t⇩x
using that map_of_eq_Some_iff 1 unfolding v⇩2_def by (auto)
have φs_kb_as⇩1: "fst ` set φs ∩ fst ` vars_formula (kb as⇩1) = {}"
using `phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id`
by (induction rule: phi_abstract.induct) (auto simp add: phi_abstract'.simps)
have cs⇩2: "cs⇩2 = Llvm_state (f⇩2#fs⇩1)"
using uu 1(9)[symmetric] s unfolding f⇩2_def c_pos s'_def
by (auto simp add: c_pos simp del: find_phis.simps split: sum_bind_splits intro: frame.expand)
then have frames_cs⇩2[simp]: "frames cs⇩2 = (f⇩2#fs⇩1)"
by auto
then have vars_term_t⇩x: "a ∉ fst ` set φs" if "(a, b) ∈ vars_term t⇩x" "(v⇩x,t⇩x) ∈ set φs" for v⇩x a b t⇩x
using 1(17) that by blast
have t⇩x_IntT: "IA.has_type t⇩x IA.IntT" if "(v⇩x,t⇩x) ∈ set φs" for v⇩x t⇩x
using `phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id` that
by (induction rule: phi_abstract.induct) (auto simp add: phi_abstract'.simps)
have d1: "map fst s = map fst phis_stats"
using s by (induction old_b_id phis_stats arbitrary: s rule: compute_phis.induct )
(fastforce split: Option.bind_splits sum_bind_splits)+
then have d: "fst ` set s = fst ` set phis_stats"
by (metis list.set_map)
have e: "abstract_state.stack as⇩1 pv = Some lv ⟹ lv ∉ fst ` set φs" for lv pv
using `phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id`
by (induction rule: phi_abstract.induct) (auto simp add: phi_abstract'.simps ranI)
have f: "phi_abstract' as⇩1 as⇩2 pv ps lv t⇩x old_b_id"
if "abstract_state.stack as⇩2 pv = Some lv" "(lv, t⇩x) ∈ set φs" "(pv, ps) ∈ set phis_stats"
for pv lv t⇩x ps
using `phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id` that 1(15) 1(12) 1(16)
proof (induction as⇩1 as⇩2 phis_stats φs old_b_id rule: phi_abstract.induct)
case (1 as⇩1 as⇩2 x ps⇩a v⇩x t⇩x⇩a xs ys)
have "pv = x ⟷ lv = v⇩x"
apply(rule)
defer
apply(rule inj_onD)
using 1 apply(blast)
using 1 that unfolding phi_abstract'.simps apply(auto)[1]
using 1 apply(blast)
apply(simp)
using 1 unfolding phi_abstract'.simps by (auto)
then show ?case
using 1 by (auto)
next
case (2 as⇩1 as⇩2)
then show ?case by simp
qed
have g: "operand_value y⇩x = Inr (IntConstant l i)"
if "(pv, ps) ∈ set phis_stats" "phi_bid old_b_id ps = Some y⇩x" "(pv, IntConstant l i) ∈ set s"
for pv ps y⇩x l i
using 1(16) s that unfolding d1[symmetric] using 1(16)
proof (induction old_b_id phis_stats arbitrary: ps s rule: compute_phis.induct)
case (1 old_b_id a psa as)
obtain x where x: "compute_phi old_b_id psa = Inr x"
using 1 by (auto split: sum_bind_splits)
have tl_s: "compute_phis old_b_id as = Inr (tl s)"
using 1 by (auto split: sum_bind_splits)
have ?case if "pv = a"
using 1 that by force
moreover have ?case if "pv ≠ a"
apply(rule 1(1)[of _ "tl s" ps]) using x apply(simp)
using 1 apply(fastforce)
using tl_s apply(simp)
using 1 that apply(simp)
using 1 that apply(blast)
using 1 that by (fastforce)+
ultimately show ?case
by blast
qed (auto)
have h: "∃t⇩x. (lv, t⇩x) ∈ set φs" if "abstract_state.stack as⇩2 pv = Some lv" "pv ∈ fst ` set phis_stats"
for lv pv
using `phi_abstract as⇩1 as⇩2 phis_stats φs old_b_id` that
by (induction rule: phi_abstract.induct) (auto simp add: phi_abstract'.simps ranI)
have "frame.pos (hd (frames cs⇩2)) = abstract_state.pos as⇩2"
unfolding cs⇩2 f⇩2_def using 1 by (simp)
moreover have 2: "v⇩2 ⊨⇩I⇩A kb as⇩1"
apply(rule vars_formula_satisfies[of _ _ v⇩1])
apply(auto)
apply(rule v⇩2_v⇩1)
using φs_kb_as⇩1 apply(blast)
using v⇩1 unfolding represents_frame.simps by auto
moreover have 3: "IA.assignment v⇩2"
using v⇩1 unfolding represents_frame.simps v⇩2_def IA.assignment_def apply(auto split: option.splits)
apply blast
subgoal for a x2
apply(subgoal_tac "IA.has_type x2 IA.IntT")
using IA.eval_types IA_locale.Values_of_type.simps(2) represents_frame.cases v⇩1
apply metis
using t⇩x_IntT
by (meson map_of_SomeD)
done
moreover have "v⇩2 ⊨⇩I⇩A kb as⇩2"
apply(rule IA.impliesD[of "(Conjunction (map (λ(v⇩x,t⇩x). encode_eq (encode_var v⇩x) t⇩x) φs)) ∧⇩f (kb as⇩1)"])
using 1 apply(simp)
defer
apply(auto)
apply(subst v⇩2_s) apply(simp)
apply(subst IA.eval_same_vars[of _ v⇩1 v⇩2])
apply(auto)
apply(subst v⇩2_v⇩1[symmetric])
apply(rule vars_term_t⇩x)
apply(simp) apply(auto)
using 2 apply(simp)
using 3 by simp
moreover have t: "same_stack_names (frame.stack (hd (frames cs⇩2))) (abstract_state.stack as⇩2)"
apply(rule same_stack_names.intros)
apply(auto simp add: f⇩2_def)
subgoal for n y
apply(subgoal_tac "n ∈ dom (abstract_state.stack as⇩2)")
apply(blast)
unfolding 1(14) s' apply(auto split: option.splits)
using v⇩1 unfolding represents_frame.simps same_stack_names.simps
apply(blast)
using d
by (metis domI dom_map_of_conv_image_fst list.set_map)
apply(subgoal_tac "n ∈ dom (abstract_state.stack as⇩2)")
subgoal for n y
unfolding 1(14) s' apply(auto split: option.splits)
using v⇩1 unfolding represents_frame.simps same_stack_names.simps
apply(blast)
defer
using d
by (metis img_fst list.set_map map_of_eq_None_iff)
by blast
moreover have u: "valid_var_mapping (frame.stack (hd (frames cs⇩2))) (abstract_state.stack as⇩2) v⇩2"
apply(rule valid_var_mapping.intros)
apply(clarsimp simp add: f⇩2_def s' split: option.splits)
subgoal for l i lv pv
apply(subgoal_tac "abstract_state.stack as⇩1 pv = Some lv")
apply(subst v⇩2_v⇩1)
using e apply(simp)
apply (meson represents_frame.cases v⇩1 valid_var_mapping.cases)
apply(subgoal_tac "pv ∈ dom (abstract_state.stack as⇩1)")
apply (simp add: "1.hyps"(13) d map_of_eq_None_iff)
apply(subgoal_tac "pv ∈ dom (abstract_state.stack as⇩2)")
unfolding 1 apply (simp add: domD map_of_eq_None_iff d[symmetric] )
using 1 by (metis domI)
subgoal for l i lv pv
apply(subgoal_tac "(pv, IntConstant l i) ∈ set s")
apply(subgoal_tac "∃t⇩x. (lv, t⇩x) ∈ set φs")
apply(auto)
subgoal for t⇩x
apply(subst v⇩2_s)
apply(simp)
proof (goal_cases)
note H = 1
case 1
then have "pv ∈ fst ` set phis_stats"
using d by blast
then obtain ps where ps: "(pv, ps) ∈ set phis_stats"
by auto
from f[OF 1(1) 1(4) ps, unfolded phi_abstract'.simps]
obtain y⇩x where y⇩x: "phi_bid old_b_id ps = Some y⇩x" "SE_Graph.operand_value as⇩1 y⇩x = Some t⇩x"
by auto
then show ?case
using g[OF ps y⇩x(1) 1(3)]
apply(cases y⇩x) apply(auto elim!: option_to_sum.elims)
by (meson represents_frame.cases v⇩1 valid_var_mapping.cases)
qed
subgoal apply(rule h) using d by blast+
by (simp add: map_of_SomeD)
done
moreover have "assig_of_state cs⇩1 (n, IA.IntT) = v⇩2 (lv, IA.IntT)" if a: "abstract_state.stack as⇩1 n = Some lv" for n lv
proof -
obtain y where y: "Mapping.lookup (frame.stack f⇩1) n = Some y"
using v⇩1 that a unfolding represents_frame.simps same_stack_names.simps by (auto)
moreover have "IA.Int (integerValue y) = v⇩1 (lv, IA.IntT)"
using v⇩1 y a unfolding represents_frame.simps valid_var_mapping.simps by (cases y) (auto)
ultimately show ?thesis
unfolding assig_of_state_def using e a by (auto simp add: v⇩2_v⇩1)
qed
moreover have "assig_of_state cs⇩2 (n, IA.IntT) = v⇩2 (lv, IA.IntT)" if a: "abstract_state.stack as⇩2 n = Some lv " for n lv
proof -
obtain y where y: "Mapping.lookup (frame.stack f⇩2) n = Some y"
using v⇩1 t a unfolding represents_frame.simps same_stack_names.simps by fastforce
moreover have "IA.Int (integerValue y) = v⇩2 (lv, IA.IntT)"
using v⇩1 y a u unfolding represents_frame.simps valid_var_mapping.simps by (cases y) (auto)
ultimately show ?thesis
unfolding assig_of_state_def using a by (auto simp add: v⇩2_v⇩1)
qed
ultimately have "represents_frame (hd (frames cs⇩2)) as⇩2 v⇩2" "as_as_step as⇩1 as⇩2 (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
using 1 assignment_assig_of_state by (auto intro!: represents_frame.intros as_as_step.intros[of v⇩2 v⇩2])
then show ?case
unfolding represents_state.simps using 1 by auto
qed
inductive icmpAsInf for prog as⇩1 as⇩2 where
"icmpAsInf prog as⇩1 as⇩2"
if
"find_statement prog (pos as⇩1) = Inr (Instruction (Named n (Icmp p o⇩1 o⇩2)))"
"φ = encode_pred p t⇩1 t⇩2"
"(b ⟹ kb as⇩1 ⟹⇩I⇩A φ)"
"(¬b ⟹ kb as⇩1 ⟹⇩I⇩A (¬⇩f φ))"
"χ = (if b then encode_eq (encode_var v⇩n) (Fun (IA.ConstF 1) []) else encode_eq (encode_var v⇩n) (Fun (IA.ConstF 0) []))"
"pos as⇩2 = inc_pos (pos as⇩1)"
"operand_value as⇩1 o⇩1 = Some t⇩1"
"operand_value as⇩1 o⇩2 = Some t⇩2"
"update_as as⇩1 as⇩2 n v⇩n χ"
lemma icmpAsInf_represents:
assumes "icmpAsInf prog as⇩1 as⇩2" "represents_state cs⇩1 as⇩1" "step prog cs⇩1 = Inr cs⇩2"
shows "represents_state cs⇩2 as⇩2 ∧ as_as_step as⇩1 as⇩2 (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
using assms proof(induction rule: icmpAsInf.induct)
case (1 n p o⇩1 o⇩2 φ t⇩1 t⇩2 b χ v⇩n)
note IA.implies_Language[simp del]
note u = `update_as as⇩1 as⇩2 n v⇩n χ`
define ins where "ins = (Named n (Icmp p o⇩1 o⇩2))"
obtain f⇩1 fs⇩1 where cs⇩1: "cs⇩1 = Llvm_state (f⇩1 # fs⇩1)"
using 1 unfolding represents_state.simps
by (metis list.exhaust_sel llvm_state.collapse)
interpret small_step prog cs⇩1 f⇩1 fs⇩1 .
have [simp]: "hd (frames cs⇩1) = f⇩1"
by (simp add: cs⇩1)
obtain fn bn pp where p: "pos as⇩1 = (fn, bn, pp)"
using prod_cases3 by blast
then have p': "frame.pos f⇩1 = (fn, bn, pp)"
using 1 cs⇩1 by (auto simp add: represents_state.simps represents_frame.simps)
have "Inr cs⇩2 = step prog (Llvm_state (f⇩1 # fs⇩1))"
using cs⇩1 1 by auto
also have "… = run_instruction ins"
using 1(1) p p' ins_def cs⇩1 by (auto)
finally have cs⇩2': "run_instruction ins = Inr cs⇩2"
by simp
then obtain x x' l i l' i' where
li_def: "operand_value o⇩1 = Inr x" "x = IntConstant l i"
"operand_value o⇩2 = Inr x'" "x' = IntConstant l' i'"
by (auto simp add: ins_def split: sum_bind_splits elim!: icmp_llvm_constant.elims)
(meson llvm_constant.exhaust)+
define f⇩2 where "f⇩2 = LLVM_Syntax.update_stack
(λ_. Mapping.update n (icmp_llvm_constant p x x') (frame.stack f⇩1))
(update_pos (λ_. (fn, bn, Suc pp)) f⇩1)"
have cs⇩2: "cs⇩2 = Llvm_state (f⇩2 # fs⇩1)"
using cs⇩2' li_def unfolding ins_def f⇩2_def
by (auto simp add: p' ins_def split: if_splits sum_bind_splits intro: frame.expand)
obtain v where v: "represents_frame f⇩1 as⇩1 v"
using 1 unfolding represents_state.simps by auto
define vv where "vv = IA.Int (if kb as⇩1 ⟹⇩I⇩A φ then 1 else 0)"
define v⇩2 where "v⇩2 = v((v⇩n, IA.IntT) := vv)"
have [simp]: "IA.assignment v⇩2"
using v unfolding v⇩2_def vv_def represents_frame.simps by (fastforce)
have [simp]: "v⇩2 ⊨⇩I⇩A kb as⇩1"
using u v by (simp add: update_as.simps represents_frame.simps v⇩2_def)
have ttii [simp]: "IA.to_int (⟦t⇩1⟧⇩I⇩A v⇩2) = i" "IA.to_int (⟦t⇩2⟧⇩I⇩A v⇩2) = i'"
unfolding v⇩2_def
using "1.hyps"(7,8) cs⇩1 li_def operand_value_valid_var_mapping represents_frame.simps
operand_value_fresh u v IA.eval_with_fresh_var SE_Graph.operand_value_fresh
by (smt)+
have χ[simp]: "v⇩2 ⊨⇩I⇩A χ"
unfolding `χ = (if b then encode_eq (encode_var v⇩n) (Fun (IA.ConstF 1) []) else encode_eq (encode_var v⇩n) (Fun (IA.ConstF 0) []))`
unfolding `φ = encode_pred p t⇩1 t⇩2`
apply (cases p)
apply (auto simp add: v⇩2_def vv_def `φ = encode_pred p t⇩1 t⇩2`)
apply (metis (no_types, lifting) "1.hyps"(2) "1.hyps"(4) ‹IA.assignment v⇩2› ‹v⇩2 ⊨⇩I⇩A kb as⇩1› encode_pred.simps(1) encode_sig.elims formula.implies_def formula.satisfies_not)
using "1.hyps"(2) "1.hyps"(3) apply (auto)
apply (metis (no_types, lifting) "1.hyps"(4) ‹IA.assignment v⇩2› ‹v⇩2 ⊨⇩I⇩A kb as⇩1› formula.implies_def formula.satisfies_not)
apply (metis "1"(4) ‹IA.assignment v⇩2› ‹v⇩2 ⊨⇩I⇩A kb as⇩1› IA.impliesE IA.satisfies_not)
apply (smt "1"(4) ‹IA.assignment v⇩2› ‹v⇩2 ⊨⇩I⇩A kb as⇩1› form_not.simps(1) formula.impliesD IA.satisfies_NegAtom)
by (metis "1"(4) ‹IA.assignment v⇩2› ‹v⇩2 ⊨⇩I⇩A kb as⇩1› formula.satisfies_not IA.impliesD )+
have [simp]: "v⇩2 ⊨⇩I⇩A kb as⇩2"
apply(rule IA.impliesD[of "kb as⇩1 ∧⇩f χ"])
using update_as.simps u apply(metis)
using represents_frame.simps by (auto)
have as⇩1_v⇩2: "IA.Int (integerValue (the (Mapping.lookup (frame.stack f⇩1) m))) = v⇩2 (lv, IA.IntT)"
if t: "stack as⇩1 m = Some lv" for m lv
proof -
obtain ll ii where look: "Mapping.lookup (frame.stack f⇩1) m = Some (IntConstant ll ii)"
using v cs⇩1 t unfolding same_stack_names_def' represents_frame.simps by fastforce+
have lvvn: "lv ≠ v⇩n"
using t by (metis u update_as.simps rangeI)
then have "v⇩2 (lv, IA.IntT) = v (lv, IA.IntT)"
unfolding v⇩2_def by simp
then show ?thesis
by (metis llvm_constant.sel(2) look option.sel represents_frame.cases that v
valid_var_mapping.cases)
qed
have iI: "icmp_llvm_constant p x x' = IntConstant 1 (if b then 1 else 0)"
unfolding `χ = (if b then encode_eq (encode_var v⇩n) (Fun (IA.ConstF 1) []) else encode_eq (encode_var v⇩n) (Fun (IA.ConstF 0) []))`
unfolding `φ = encode_pred p t⇩1 t⇩2` apply (cases p)
apply (auto simp add: v⇩2_def vv_def `φ = encode_pred p t⇩1 t⇩2`)
using 1(3) 1(4) 1(5) apply (auto simp add: v⇩2_def vv_def `φ = encode_pred p t⇩1 t⇩2` li_def split: if_splits)
using IA.impliesD[OF _ ‹IA.assignment v⇩2› ‹v⇩2 ⊨⇩I⇩A kb as⇩1›]
by force+
have r_f⇩2_v⇩2: "represents_frame f⇩2 as⇩2 v⇩2"
proof -
have a: "same_stack_names (Mapping.update n (icmp_llvm_constant p x x') (frame.stack f⇩1))
(abstract_state.stack as⇩2)"
using ‹update_as as⇩1 as⇩2 n v⇩n χ› v
by (auto intro: same_stack_names.intros simp add: update_as.simps represents_simps
same_stack_names.simps lookup_update')
show ?thesis
apply(auto simp add: f⇩2_def represents_frame.simps)
subgoal
using 1 by (auto simp add: p)
subgoal
using a by simp
apply(rule vvm_update[OF _ u, of "frame.stack f⇩1" v, where l=1 ])
using represents_frame.cases v apply blast
using v⇩2_def vv_def apply(blast)
using iI apply auto
using "1.hyps"(3,4) apply blast
using "1.hyps"(4)
by (metis (mono_tags, lifting) ‹IA.assignment v⇩2› ‹v⇩2 ⊨⇩I⇩A kb as⇩1› formula.implies_def formula.satisfies_not)
qed
have "represents_state cs⇩2 as⇩2"
unfolding cs⇩2 represents_state.simps using r_f⇩2_v⇩2 1 by (auto)
moreover have "as_as_step as⇩1 as⇩2 (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
proof -
have a: "IA.Int (integerValue (the (Mapping.lookup (frame.stack f⇩2) n))) = v⇩2 (v⇩n, IA.IntT)"
unfolding v⇩2_def f⇩2_def vv_def iI using `b ⟹ kb as⇩1 ⟹⇩I⇩A φ` `¬ b ⟹ kb as⇩1 ⟹⇩I⇩A ¬⇩f φ`
by (auto) (metis IA.impliesE IA.satisfies_not ‹IA.assignment v⇩2› ‹v⇩2 ⊨⇩I⇩A kb as⇩1›)
have b: "assig_of_state cs⇩2 (n, IA.IntT) = v⇩2 (lv, IA.IntT)" if "abstract_state.stack as⇩2 n = Some lv" for lv
using that u as⇩1_v⇩2 unfolding update_as.simps
by (auto simp add: assig_of_state_def cs⇩2 a lookup_update_neq cs⇩2 lookup_update_neq)
have c: "assig_of_state cs⇩2 (m, IA.IntT) = v⇩2 (lv, IA.IntT)"
if "abstract_state.stack as⇩2 m = Some lv" "m ≠ n" for m lv
using that u as⇩1_v⇩2 unfolding update_as.simps
by (auto simp add: assig_of_state_def as⇩1_v⇩2 cs⇩2 f⇩2_def lookup_update_neq)
show ?thesis
apply(rule as_as_step.intros[where v=v⇩2 and v'=v⇩2])
using 1 assignment_assig_of_state
using as⇩1_v⇩2 a f⇩2_def a b c
by (auto intro!: assignment_assig_of_frame simp add: cs⇩2 cs⇩1 assig_of_state_def lookup_update_neq
as⇩1_v⇩2 f⇩2_def lookup_update')
qed
ultimately show ?case
by simp
qed
inductive evalExternalAsInf for prog as⇩1 as⇩2 where
"find_statement prog (pos as⇩1) = Inr (Instruction (Named n (Call t g ls))) ⟹
small_step.map_of_funs prog g = Some (ExternalFunction _ _ ps) ⟹
pos as⇩2 = inc_pos (pos as⇩1) ⟹
update_as as⇩1 as⇩2 n v⇩n True⇩f ⟹
evalExternalAsInf prog as⇩1 as⇩2"
lemma evalExternalAsInf_represents_step':
assumes "evalExternalAsInf prog as⇩1 as⇩2" "represents_state cs⇩1 as⇩1" "step' prog cs⇩1 (Inr cs⇩2)"
shows "represents_state cs⇩2 as⇩2 ∧ as_as_step as⇩1 as⇩2 (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
using assms proof(induction rule: evalExternalAsInf.induct)
case (1 n t g ls uu uv ps v⇩n)
note u = `update_as as⇩1 as⇩2 n v⇩n True⇩f`
define ins where "ins = Instruction (Named n (Call t g ls))"
obtain f⇩1 fs⇩1 where cs⇩1: "cs⇩1 = Llvm_state (f⇩1 # fs⇩1)"
using 1 unfolding represents_state.simps by (metis hd_Cons_tl llvm_state.collapse)
interpret small_step prog cs⇩1 f⇩1 fs⇩1 .
have [simp]: "hd (frames cs⇩1) = f⇩1"
by (simp add: cs⇩1)
obtain fn bn p where p: "pos as⇩1 = (fn, bn, p)"
using prod_cases3 by blast
then have p': "frame.pos f⇩1 = (fn, bn, p)"
using 1 cs⇩1 by (auto simp add: represents_state.simps represents_frame.simps)
have "call_external_function g ls n (Inr cs⇩2)"
using 1 cs⇩1 p p' unfolding step'_def step_call.simps
by (auto split: list.splits sum.splits action.splits named.splits instruction.splits)
then have "assign_unknown_value n (Inr cs⇩2)"
using 1 cs⇩1 p p' unfolding call_external_function_def
by (auto split: list.splits sum.splits action.splits named.splits instruction.splits)
then obtain c where c: "Inr cs⇩2 = update_frames_stack n (Inr c)"
unfolding assign_unknown_value.simps by blast
then obtain f⇩2 where f⇩2: "cs⇩2 = Llvm_state (f⇩2#fs⇩1)"
unfolding update_frames_stack.simps by (auto split: prod.splits)
obtain v where v: "represents_frame f⇩1 as⇩1 v"
using 1 unfolding represents_state.simps by auto
define v⇩2 where "v⇩2 = v((v⇩n, IA.IntT) := IA.Int (integerValue c))"
have [simp]: "IA.assignment v⇩2"
using v unfolding v⇩2_def represents_frame.simps by fastforce
have [simp]: "v⇩2 ⊨⇩I⇩A kb as⇩1"
using u v by (simp add: update_as.simps represents_frame.simps v⇩2_def)
have [simp]: "v⇩2 ⊨⇩I⇩A True⇩f"
by simp
have [simp]: "v⇩2 ⊨⇩I⇩A kb as⇩2"
apply(rule IA.impliesD[of "kb as⇩1 ∧⇩f True⇩f"])
using update_as.simps u apply(metis)
using represents_frame.simps by (auto)
have as⇩1_v⇩2: "IA.Int (integerValue (the (Mapping.lookup (frame.stack f⇩1) m))) = v⇩2 (lv, IA.IntT)"
if t: "stack as⇩1 m = Some lv" for m lv
proof -
obtain ll ii where look: "Mapping.lookup (frame.stack f⇩1) m = Some (IntConstant ll ii)"
using v cs⇩1 t unfolding same_stack_names_def' represents_frame.simps by fastforce+
have lvvn: "lv ≠ v⇩n"
using t by (metis u update_as.simps rangeI)
then have "v⇩2 (lv, IA.IntT) = v (lv, IA.IntT)"
unfolding v⇩2_def by simp
then show ?thesis
by (metis llvm_constant.sel(2) look option.sel represents_frame.cases that v
valid_var_mapping.cases)
qed
have a: "same_stack_names (Mapping.update n c (frame.stack f⇩1))
(abstract_state.stack as⇩2)"
apply(cases c)
apply(rule ssn_update[of as⇩1 as⇩2 n v⇩n True⇩f ])
using u 1 unfolding cs⇩1 by (auto simp add: represents_state.simps represents_frame.simps)
have r_f⇩2_v⇩2: "represents_frame f⇩2 as⇩2 v⇩2"
apply(auto simp add: represents_frame.simps)
subgoal
using 1 c f⇩2 by (auto simp add: p' p)
subgoal using a c f⇩2 by (auto split: prod.splits)
apply(rule vvm_update[OF _ u, of "frame.stack f⇩1" v, where l="integerBits c" ])
using represents_frame.cases v apply blast
using v⇩2_def apply(blast)
using f⇩2 c 1 by (auto split: prod.splits)
have "represents_state cs⇩2 as⇩2"
unfolding represents_state.simps using f⇩2 r_f⇩2_v⇩2 by (auto)
moreover have "as_as_step as⇩1 as⇩2 (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
apply(rule as_as_step.intros[where v=v⇩2 and v'=v⇩2])
using 1 assignment_assig_of_state apply(auto)[6]
subgoal
unfolding v⇩2_def apply(auto)
apply(subgoal_tac "Some v⇩n ∈ range (abstract_state.stack as⇩1)")
using 1 unfolding update_as.simps
apply(simp)
unfolding image_def apply(simp)
apply(metis)
by (simp add: as⇩1_v⇩2 assig_of_state_def v⇩2_def)
subgoal
using f⇩2 c apply (auto simp add: as⇩1_v⇩2 assig_of_state_def v⇩2_def)
apply(cases f⇩1)
apply (auto simp add: as⇩1_v⇩2 assig_of_state_def v⇩2_def)
using 1 unfolding update_as.simps image_def apply(auto)[1]
apply(metis)
using as⇩1_v⇩2
apply(cases f⇩1)
using 1 f⇩2 c unfolding update_as.simps
by (auto split: prod.splits simp add: small_step.simps as⇩1_v⇩2 assig_of_state_def v⇩2_def)
by auto
ultimately show ?case
by simp
qed
locale llvm_se_graph = graph' as_of_node for
as_of_node :: "'n ⇒ ('lv::linorder) abstract_state" +
fixes prog :: llvm_prog
begin
inductive represents for cs n where
"represents cs n"
if "n ∈ nodes" "represents_state cs (as_of_node n)"
inductive evalInf for n⇩1 n⇩2 where
"evalAsInf prog as⇩1 as⇩2 ⟹
as_of_node n⇩1 = as⇩1 ⟹
as_of_node n⇩2 = as⇩2 ⟹
renaming_of_edge (n⇩1, n⇩2) = id ⟹
n⇩1 ∈ nodes ⟹ n⇩2 ∈ nodes ⟹ (n⇩1,n⇩2) ∈ edges ⟹
evalInf n⇩1 n⇩2"
lemma evalInf_represents_step:
assumes "evalInf n⇩1 n⇩2" "represents cs⇩1 n⇩1" "step prog cs⇩1 = Inr cs⇩2"
shows "represents cs⇩2 n⇩2 ∧ ((n⇩1, assig_of_state cs⇩1), (n⇩2, assig_of_state cs⇩2)) ∈ as_step"
using evalAsInf_represents_step assms unfolding evalInf.simps represents.simps
by (fastforce intro!: as_as_as_step)
inductive genInf for n⇩1 n⇩2 where
"genAsInf as⇩1 as⇩2 μ ⟹
as_of_node n⇩1 = as⇩1 ⟹
as_of_node n⇩2 = as⇩2 ⟹
renaming_of_edge (n⇩1, n⇩2) = μ ⟹
n⇩1 ∈ nodes ⟹ n⇩2 ∈ nodes ⟹ (n⇩1,n⇩2) ∈ edges ⟹
genInf n⇩1 n⇩2"
lemma genInf_represents:
assumes "genInf n⇩1 n⇩2" "represents cs n⇩1"
shows "represents cs n⇩2 ∧ ((n⇩1, assig_of_state cs), (n⇩2, assig_of_state cs)) ∈ as_step"
using genAsInf_represents assms unfolding genInf.simps represents.simps
by (fastforce intro!: as_as_as_step)
inductive refineInf for n n⇩t n⇩f where
"refineAsInf as as⇩t as⇩f ⟹
as_of_node n = as ⟹
as_of_node n⇩t = as⇩t ⟹
as_of_node n⇩f = as⇩f ⟹
renaming_of_edge (n, n⇩t) = id ⟹
renaming_of_edge (n, n⇩f) = id ⟹
n ∈ nodes ⟹ n⇩t ∈ nodes ⟹ n⇩f ∈ nodes ⟹
(n,n⇩t) ∈ edges ⟹ (n,n⇩f) ∈ edges ⟹
refineInf n n⇩t n⇩f"
lemma refineInf_represents: "refineInf n n⇩t n⇩f ⟹
represents cs n ⟹
represents cs n⇩t ∧ ((n, assig_of_state cs), (n⇩t, assig_of_state cs)) ∈ as_step
∨ represents cs n⇩f ∧ ((n, assig_of_state cs), (n⇩f, assig_of_state cs)) ∈ as_step"
using refineAsInf_represents unfolding refineInf.simps represents.simps
by (fastforce intro!: as_as_as_step)
inductive branchInf for n⇩1 n⇩2 where
"branchAsInf prog as⇩1 as⇩2 ⟹
as_of_node n⇩1 = as⇩1 ⟹
as_of_node n⇩2 = as⇩2 ⟹
renaming_of_edge (n⇩1, n⇩2) = id ⟹
n⇩1 ∈ nodes ⟹ n⇩2 ∈ nodes ⟹ (n⇩1,n⇩2) ∈ edges ⟹
branchInf n⇩1 n⇩2"
lemma branchInf_represents:
assumes "branchInf n⇩1 n⇩2" "represents cs⇩1 n⇩1" "step prog cs⇩1 = Inr cs⇩2"
shows "represents cs⇩2 n⇩2 ∧ ((n⇩1, assig_of_state cs⇩1), (n⇩2, assig_of_state cs⇩2)) ∈ as_step"
using assms branchAsInf_represents unfolding branchInf.simps represents.simps
by (fastforce intro!: as_as_as_step)
inductive condBranchInf for n⇩1 n⇩2 where
"condBranchAsInf prog as⇩1 as⇩2 ⟹
as_of_node n⇩1 = as⇩1 ⟹
as_of_node n⇩2 = as⇩2 ⟹
renaming_of_edge (n⇩1, n⇩2) = id ⟹
n⇩1 ∈ nodes ⟹ n⇩2 ∈ nodes ⟹ (n⇩1,n⇩2) ∈ edges ⟹
condBranchInf n⇩1 n⇩2"
lemma condBranchInf_represents:
assumes "condBranchInf n⇩1 n⇩2" "represents cs⇩1 n⇩1" "step prog cs⇩1 = Inr cs⇩2"
shows "represents cs⇩2 n⇩2 ∧ ((n⇩1, assig_of_state cs⇩1), (n⇩2, assig_of_state cs⇩2)) ∈ as_step"
using assms condBranchAsInf_represents unfolding condBranchInf.simps represents.simps
by (fastforce intro!: as_as_as_step)
inductive icmpInf for n⇩1 n⇩2 where
"icmpAsInf prog as⇩1 as⇩2 ⟹
as_of_node n⇩1 = as⇩1 ⟹
as_of_node n⇩2 = as⇩2 ⟹
renaming_of_edge (n⇩1, n⇩2) = id ⟹
n⇩1 ∈ nodes ⟹ n⇩2 ∈ nodes ⟹ (n⇩1,n⇩2) ∈ edges ⟹
icmpInf n⇩1 n⇩2"
lemma icmpInf_represents:
assumes "icmpInf n⇩1 n⇩2" "represents cs⇩1 n⇩1" "step prog cs⇩1 = Inr cs⇩2"
shows "represents cs⇩2 n⇩2 ∧ ((n⇩1, assig_of_state cs⇩1), (n⇩2, assig_of_state cs⇩2)) ∈ as_step"
using assms icmpAsInf_represents unfolding icmpInf.simps represents.simps
by (fastforce intro!: as_as_as_step)
inductive returnInf where
"find_statement prog (pos as⇩1) = Inr (Terminator t) ⟹
named_instruction t = Ret (Some op) ⟹
operand_value as⇩1 op = Some t⇩1 ⟹
as_of_node n⇩1 = as⇩1 ⟹
n⇩1 ∈ nodes ⟹
returnInf n⇩1"
inductive evalExternalInf for n⇩1 n⇩2 where
"evalExternalInf n⇩1 n⇩2"
if
"evalExternalAsInf prog (as_of_node n⇩1) (as_of_node n⇩2)"
"renaming_of_edge (n⇩1, n⇩2) = id"
"n⇩1 ∈ nodes" "n⇩2 ∈ nodes" "(n⇩1,n⇩2) ∈ edges"
subsection ‹step' semantics and inference rules›
lemma evalInf_represents_step':
assumes "evalInf n⇩1 n⇩2" "represents cs⇩1 n⇩1" "step' prog cs⇩1 (Inr cs⇩2)"
shows "represents cs⇩2 n⇩2 ∧ ((n⇩1, assig_of_state cs⇩1), (n⇩2, assig_of_state cs⇩2)) ∈ as_step"
proof -
have "step prog cs⇩1 = Inr cs⇩2"
using assms
by (auto simp add: step'_def evalAsInf.simps evalInf.simps represents.simps represents_simps
split: list.splits)
then show ?thesis
using evalInf_represents_step assms by blast
qed
lemma branchInf_represents_step':
assumes "branchInf n⇩1 n⇩2" "represents cs⇩1 n⇩1" "step' prog cs⇩1 (Inr cs⇩2)"
shows "represents cs⇩2 n⇩2 ∧ ((n⇩1, assig_of_state cs⇩1), (n⇩2, assig_of_state cs⇩2)) ∈ as_step"
proof -
have "step prog cs⇩1 = Inr cs⇩2"
using assms
by (auto simp add: step'_def branchInf.simps branchAsInf.simps represents.simps represents_simps
small_step.terminate_frame'_def
split: list.splits)
then show ?thesis
using branchInf_represents assms by blast
qed
lemma condBranchInf_represents_step':
assumes "condBranchInf n⇩1 n⇩2" "represents cs⇩1 n⇩1" "step' prog cs⇩1 (Inr cs⇩2)"
shows "represents cs⇩2 n⇩2 ∧ ((n⇩1, assig_of_state cs⇩1), (n⇩2, assig_of_state cs⇩2)) ∈ as_step"
proof -
have "step prog cs⇩1 = Inr cs⇩2"
using assms
by (auto simp add: step'_def condBranchInf.simps condBranchAsInf.simps represents.simps represents_simps
small_step.terminate_frame'_def
split: list.splits)
then show ?thesis
using condBranchInf_represents assms by blast
qed
lemma icmpInf_represents_step':
assumes "icmpInf n⇩1 n⇩2" "represents cs⇩1 n⇩1" "step' prog cs⇩1 (Inr cs⇩2)"
shows "represents cs⇩2 n⇩2 ∧ ((n⇩1, assig_of_state cs⇩1), (n⇩2, assig_of_state cs⇩2)) ∈ as_step"
proof -
have "step prog cs⇩1 = Inr cs⇩2"
using assms
by (auto simp add: step'_def icmpInf.simps icmpAsInf.simps represents.simps represents_simps
small_step.terminate_frame'_def
split: list.splits)
then show ?thesis
using icmpInf_represents assms by blast
qed
lemma returnInf_represents_step': "returnInf n⇩1 ⟹
represents cs⇩1 n⇩1 ⟹
(∃c. step' prog cs⇩1 (Inl (ReturnValue c)))"
proof(induction rule: returnInf.induct)
case (1 as⇩1 t op t⇩1 n⇩1)
obtain f⇩1 fs⇩1 where cs⇩1: "cs⇩1 = Llvm_state (f⇩1 # fs⇩1)"
using 1 unfolding represents.simps represents_state.simps
by (metis llvm_state.exhaust_sel neq_Nil_conv)
interpret small_step prog cs⇩1 f⇩1 fs⇩1 .
have [simp]: "hd (frames cs⇩1) = f⇩1"
by (simp add: cs⇩1)
obtain fn bn pp where p: "pos as⇩1 = (fn, bn, pp)"
using prod_cases3 by blast
then have p': "frame.pos f⇩1 = (fn, bn, pp)"
using 1 cs⇩1 by (auto simp add: represents.simps represents_state.simps represents_frame.simps)
have a: "step' prog cs⇩1 (operand_value op ⤜ (λc. Inl (ReturnValue c)))"
using cs⇩1 1 p p' by (auto simp add: step'_def small_step.terminate_frame'_def)
have "(∃c. operand_value op = Inr c)"
using 1 unfolding represents.simps represents_state.simps represents_frame.simps
same_stack_names.simps apply(cases op) apply(auto)
by (metis (no_types, hide_lams) option_to_sum.simps(1))
then obtain c where "operand_value op = Inr c"
by auto
then show ?case
using a by auto
qed
lemma evalExternalInf_represents_step':
assumes "evalExternalInf n⇩1 n⇩2" "represents cs⇩1 n⇩1" "step' prog cs⇩1 (Inr cs⇩2)"
shows "represents cs⇩2 n⇩2 ∧ ((n⇩1, assig_of_state cs⇩1), (n⇩2, assig_of_state cs⇩2)) ∈ as_step"
proof -
have "represents cs⇩2 n⇩2"
using evalExternalAsInf_represents_step' assms unfolding evalExternalInf.simps represents.simps
by blast
moreover have "((n⇩1, assig_of_state cs⇩1), (n⇩2, assig_of_state cs⇩2)) ∈ as_step"
apply(rule as_as_as_step)
using evalExternalAsInf_represents_step' assms unfolding evalExternalInf.simps represents.simps
by (fastforce)+
ultimately show ?thesis
by simp
qed
lemma returnInf_represents_unique_step':
assumes "returnInf n⇩1" "represents cs⇩1 n⇩1" "step' prog cs⇩1 x" "step' prog cs⇩1 (Inl (ReturnValue c))"
shows "x = Inl (ReturnValue c)"
using assms
by (auto simp add: returnInf.simps step'_def represents.simps represents_simps split: list.splits)
end
inductive skipCallInf for as⇩1 as⇩s n v⇩n where "skipCallInf as⇩1 as⇩s n v⇩n"
if
"pos as⇩s = inc_pos (pos as⇩1)"
"update_as as⇩1 as⇩s n v⇩n True⇩f"
inductive linkParams' for as⇩1 as⇩2 a x v⇩a t⇩x where "linkParams' as⇩1 as⇩2 a x v⇩a t⇩x"
if
"operand_value as⇩1 x = Some t⇩x"
"stack as⇩2 a = Some v⇩a"
"v⇩a ∉ ran (stack as⇩1)"
"v⇩a ∉ fst ` vars_formula (kb as⇩1)"
"IA.has_type t⇩x IA.IntT"
inductive linkParams where
"linkParams as⇩1 as⇩2 ((a, x)#xs) ((v⇩a, t⇩x)#ys)"
if
"linkParams' as⇩1 as⇩2 a x v⇩a t⇩x" "linkParams as⇩1 as⇩2 xs ys"
| "linkParams as⇩1 as⇩2 [] []"
inductive callCallInf for prog as⇩1 as⇩f f bs vs where "callCallInf prog as⇩1 as⇩f f bs vs"
if
"pos as⇩f = (f, LLVM_Syntax.name b, 0)"
"small_step.map_of_funs prog f = Some (Function _ _ ps b _)"
"linkParams as⇩1 as⇩f (zip (map parameter_name ps) bs) vs"
"(Formula.Conjunction (map (λ(v⇩x,t⇩x). encode_eq (encode_var v⇩x) t⇩x) vs)) ∧⇩f (kb as⇩1) ⟹⇩I⇩A kb as⇩f"
"distinct (map fst vs)"
"dom (stack as⇩f) = set (map parameter_name ps)"
"distinct (map parameter_name ps)"
"(∀x ∈ fst ` ⋃ (vars_term ` snd ` set vs). x ∉ fst ` set vs)"
lemma step_call_Inl_Inr:
assumes "step_call prog s f fs n t g ps (Inr s')"
shows "∄e. step_call prog s f fs n t g ps (Inl e)"
using assms map_of_funs_name unfolding step_call.simps
apply (auto simp add: small_step.simps small_step.call_external_function_def small_step.assign_unknown_value.simps split: list.splits option.splits action.splits
named.splits instruction.splits sum.splits sum_bind_splits prod.splits llvm_fun.splits option.splits)
apply (meson old.sum.exhaust)
apply (meson old.sum.exhaust)
by fastforce+
lemma step'_Inl_Inr:
assumes "step' prog s⇩1 (Inr s⇩2)"
shows "∄e. step' prog s⇩1 (Inl e)"
proof -
have ?thesis if "find_statement prog (frame.pos f) = Inl x" "frames s⇩1 = f#fs" for f fs x
using assms that step_call_Inl_Inr
by (auto simp add: step'_def small_step.simps small_step.terminate_frame'_def
split: list.splits option.splits action.splits named.splits instruction.splits sum_bind_splits
prod.splits terminator.splits)
moreover have ?thesis if "find_statement prog (frame.pos f) = Inr x" "frames s⇩1 = f#fs" for f fs x
using assms that step_call_Inl_Inr
by (fastforce simp add: step'_def small_step.simps small_step.terminate_frame'_def
split: list.splits option.splits action.splits named.splits instruction.splits sum_bind_splits
prod.splits terminator.splits)
ultimately have ?thesis if "frames s⇩1 = f#fs" for f fs
using that by (cases "find_statement prog (frame.pos f)") blast+
then show ?thesis
using assms by (auto simp add: step'_def split: list.splits)
qed
inductive callAsInf for prog as⇩1 as⇩f as⇩s where "callAsInf prog as⇩1 as⇩f as⇩s"
if
"find_statement prog (pos as⇩1) = Inr (Instruction (Named x (Call t g ls)))"
"skipCallInf as⇩1 as⇩s x v⇩n"
"callCallInf prog as⇩1 as⇩f g ls vs"
lemma callInf_represents_step':
assumes "callAsInf prog as⇩1 as⇩f as⇩s" "represents_state cs⇩1 as⇩1" "step' prog cs⇩1 (Inr cs⇩2)"
shows "represents_state cs⇩2 as⇩f ∧ as_as_step as⇩1 as⇩f (assig_of_state cs⇩1) (assig_of_state cs⇩2) id
∨ represents_state cs⇩2 as⇩s ∧ as_as_step as⇩1 as⇩s (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
using assms proof (induction rule: callAsInf.induct)
case (1 x t g ls v⇩n vs)
note callInf = 1
obtain f⇩1 fs⇩1 where f⇩1: "frames cs⇩1 = f⇩1#fs⇩1"
using callInf by (auto simp add: step'_def split: list.splits)
have [simp]: "pos as⇩1 = frame.pos f⇩1"
using callInf by (auto simp add: represents_simps f⇩1)
obtain t⇩g ps⇩g b⇩g bs⇩g where find_fun: "small_step.map_of_funs prog g = Some (Function t⇩g g ps⇩g b⇩g bs⇩g)"
using callInf unfolding callCallInf.simps using map_of_funs_name by auto blast
have callCallInf: "abstract_state.pos as⇩f = (g, basic_block.name b⇩g, 0)"
"linkParams as⇩1 as⇩f (zip (map parameter_name ps⇩g) ls) vs"
"distinct (map fst vs)"
"dom (abstract_state.stack as⇩f) = set (map parameter_name ps⇩g)"
"(⋀⇩f (v⇩x, y)←vs. encode_eq (encode_var v⇩x) y) ∧⇩f kb as⇩1 ⟹⇩I⇩A kb as⇩f"
"(∀x ∈ fst ` ⋃ (vars_term ` snd ` set vs). x ∉ fst ` set vs)"
"distinct (map parameter_name ps⇩g)"
using find_fun callInf(3)[unfolded callCallInf.simps] by (force)+
obtain v⇩1 where v⇩1: "represents_frame f⇩1 as⇩1 v⇩1"
using callInf unfolding represents_state.simps f⇩1 by auto
have "step_call prog cs⇩1 f⇩1 fs⇩1 x t g ls (Inr cs⇩2)"
using callInf by (auto simp add: f⇩1 step'_def split: list.splits)
then consider
(call) "small_step.call_external_function prog cs⇩1 f⇩1 fs⇩1 g ls x (Inr cs⇩2)"
| (skip) f' c where "Inr f' = small_step.enter_frame prog f⇩1 g ls"
"(Inr (update_frames (λ_. [f']) cs⇩1), Inl (ReturnValue c)) ∈ (step_rel_e prog)⇧+"
"Inr cs⇩2 = small_step.update_frames_stack cs⇩1 f⇩1 fs⇩1 x (Inr c)"
unfolding step_call.simps by blast
then show ?case
proof (cases)
case call
then have call: "Inr cs⇩2 = small_step.run_instruction prog cs⇩1 f⇩1 fs⇩1 (Named x (Call t g ls))"
unfolding small_step.call_external_function_def using find_fun by (auto simp add: small_step.simps)
have a: "Inr cs⇩2 =
small_step.zip_parameters f⇩1 ls ps⇩g ⤜
(λzs. Inr (Llvm_state (Frame (g, basic_block.name b⇩g, 0) zs # f⇩1 # fs⇩1)))"
using callInf find_fun unfolding call callCallInf.simps
by (auto simp add: small_step.simps split: sum_bind_splits)
obtain zs where zs_def: "Inr zs = small_step.zip_parameters f⇩1 ls ps⇩g"
using callInf find_fun step'_Inl_Inr [OF ‹step' prog cs⇩1 (Inr cs⇩2)›] unfolding call callCallInf.simps
by (auto simp add: small_step.simps split: sum_bind_splits)
define f⇩2 where "f⇩2 = Frame (g, basic_block.name b⇩g, 0) zs"
have cs⇩2: "cs⇩2 = Llvm_state (f⇩2 # f⇩1 # fs⇩1)"
using f⇩2_def a zs_def by (auto split: sum_bind_splits)
define v⇩2 where "v⇩2 = (λ(v, t).
if t = IA.IntT
then case map_of vs v of Some t⇩x ⇒ (⟦t⇩x⟧⇩I⇩A v⇩1) | None ⇒ v⇩1 (v,t)
else v⇩1 (v,t))"
have v⇩2_v⇩1: "v⇩2 (v,t) = v⇩1 (v,t)" if "v ∉ fst ` set vs" for v t
using that map_of_eq_None_iff 1 unfolding v⇩2_def callCallInf.simps by (auto split: option.splits)
have v⇩2_s: "v⇩2 (v,IA.IntT) = (⟦t⇩x⟧⇩I⇩A v⇩1)" if "(v,t⇩x) ∈ set vs" for v t⇩x
using that map_of_eq_Some_iff 1 unfolding v⇩2_def callCallInf.simps by (auto)
have b: "lv ∉ fst ` set vs" if "abstract_state.stack as⇩1 pv = Some lv" for lv pv
using `linkParams as⇩1 as⇩f (zip (map parameter_name ps⇩g) ls) vs` that
by (induction rule: linkParams.induct) (auto simp add: linkParams'.simps ranI)
have vars_term_t⇩x: "a ∉ fst ` set vs" if "(a, b) ∈ vars_term t⇩x" "(v⇩x,t⇩x) ∈ set vs" for v⇩x a b t⇩x
using callCallInf that by blast
have t⇩x_IntT: "IA.has_type t⇩x IA.IntT" if "(v⇩x,t⇩x) ∈ set vs" for v⇩x t⇩x
using `linkParams as⇩1 as⇩f (zip (map parameter_name ps⇩g) ls) vs` that
by (induction rule: linkParams.induct) (auto simp add: linkParams'.simps ranI)
have v⇩2_assig: "IA.assignment v⇩2"
proof -
have a: "v⇩1 (n, IA.IntT) ∈ range IA.Int" for n
using v⇩1 unfolding represents_frame.simps IA.assignment_def by fastforce
have "IA.has_type t IA.IntT" if "map_of vs n = Some t" for n t
using that t⇩x_IntT by (meson map_of_SomeD)
then have b: "⟦t⟧⇩I⇩A v⇩1 ∈ range IA.Int" if "map_of vs n = Some t" for n t
using that IA.eval_types IA_locale.Values_of_type.simps(2) represents_frame.cases v⇩1
by metis
show ?thesis
using v⇩1 a b unfolding represents_frame.simps v⇩2_def IA.assignment_def
by (auto split: option.splits)
qed
have vs_kb_as⇩1: "fst ` set vs ∩ fst ` vars_formula (kb as⇩1) = {}"
using `linkParams as⇩1 as⇩f (zip (map parameter_name ps⇩g) ls) vs`
by (induction rule: linkParams.induct) (auto simp add: linkParams'.simps)
have c: "v⇩2 ⊨⇩I⇩A kb as⇩1"
proof -
have "v⇩2 x = v⇩1 x" if "x ∈ vars_formula (kb as⇩1)" for x
using vs_kb_as⇩1 that by (cases x) (auto intro!: v⇩2_v⇩1)
then show ?thesis
by (rule vars_formula_satisfies[of _ _ v⇩1])
(use v⇩1 in ‹auto simp add: represents_frame.simps›)
qed
have v⇩2_kb: "v⇩2 ⊨⇩I⇩A kb as⇩f"
proof -
have a: "v⇩1 x = v⇩2 x" if "(n, t) ∈ set vs" "x ∈ vars_term t" for n t x
using vars_term_t⇩x that by (cases x) (auto simp add: v⇩2_v⇩1)
then have b: "v⇩2 ⊨⇩I⇩A (⋀⇩f (v⇩x, t⇩x)←vs. encode_eq (encode_var v⇩x) t⇩x) ∧⇩f kb as⇩1" (is "_ ⊨⇩I⇩A ?f")
using c by (auto simp add: v⇩2_s IA.eval_same_vars[OF a])
show ?thesis
by (rule IA.impliesD[of ?f]) (use callCallInf v⇩2_assig b in auto)
qed
define xs where "xs = zip (map parameter_name ps⇩g) ls"
have ls: "length ls = length ps⇩g"
using zs_def
by(induction ls ps⇩g arbitrary: zs x rule: small_step.zip_parameters.induct)
(fastforce split: sum_bind_splits simp add: small_step.zip_parameters.simps)+
have lPa: "linkParams as⇩1 as⇩f xs vs"
unfolding xs_def using callCallInf by blast
have d: "same_stack_names (frame.stack f⇩2) (abstract_state.stack as⇩f)"
proof -
have "∃y. abstract_state.stack as⇩f n = Some y" if "Mapping.lookup zs n = Some x" for n x
proof -
have "n ∈ set (map parameter_name ps⇩g)"
using zs_def that
by(induction ls ps⇩g arbitrary: zs n x rule: small_step.zip_parameters.induct)
(fastforce split: sum_bind_splits simp add: small_step.zip_parameters.simps)+
then have "∃p⇩o. (n, p⇩o) ∈ set xs"
unfolding xs_def using ls by (metis in_set_impl_in_set_zip1 length_map)
then obtain p⇩o where p⇩o: "(n, p⇩o) ∈ set xs"
by blast
have "∃v⇩n t. linkParams' as⇩1 as⇩f n p⇩o v⇩n t"
using lPa p⇩o by (induction as⇩1 as⇩f xs vs rule: linkParams.induct) (auto)
then show ?thesis
unfolding linkParams'.simps by auto
qed
moreover have "∃x. Mapping.lookup zs n = Some x" if "abstract_state.stack as⇩f n = Some y" for n y
proof -
have a: "n ∈ set (map parameter_name ps⇩g)"
using callCallInf that by blast
then show "∃x. Mapping.lookup zs n = Some x"
using zs_def
by (induction ls ps⇩g arbitrary: zs n x rule: small_step.zip_parameters.induct)
(fastforce split: sum_bind_splits simp add: small_step.zip_parameters.simps)+
qed
ultimately show ?thesis
using same_stack_names.intros by (auto simp add: f⇩2_def intro!: same_stack_names.intros)
qed
have e: "valid_var_mapping (frame.stack f⇩2) (abstract_state.stack as⇩f) v⇩2"
proof -
have "v⇩2 (lv, IA.IntT) = IA.Int i" if "Mapping.lookup zs n = Some (IntConstant l i)"
"abstract_state.stack as⇩f n = Some lv" for lv l i n
proof -
have "n ∈ set (map parameter_name ps⇩g)"
using zs_def that
by(induction ls ps⇩g arbitrary: zs n x rule: small_step.zip_parameters.induct)
(fastforce split: sum_bind_splits simp add: small_step.zip_parameters.simps)+
then have "∃p⇩o. (n, p⇩o) ∈ set xs"
unfolding xs_def using ls by (metis in_set_impl_in_set_zip1 length_map)
then obtain p⇩o where p⇩o: "(n, p⇩o) ∈ set xs"
by blast
have "∃v⇩n t. (v⇩n, t) ∈ set vs ∧ linkParams' as⇩1 as⇩f n p⇩o v⇩n t"
using lPa p⇩o by (induction as⇩1 as⇩f xs vs rule: linkParams.induct) (auto)
then obtain v⇩n t where v⇩n: "(v⇩n, t) ∈ set vs" "linkParams' as⇩1 as⇩f n p⇩o v⇩n t"
by auto
have ssop⇩o: "small_step.operand_value f⇩1 p⇩o = Inr (IntConstant l i)"
using zs_def that(1) p⇩o callCallInf(7) unfolding xs_def
proof (induction ls ps⇩g arbitrary: zs x p⇩o rule: small_step.zip_parameters.induct)
case (1 x' xs' t' n' ps')
then show ?case
using set_zip_leftD
by(cases "n = n'")
(fastforce split: sum_bind_splits simp add: small_step.zip_parameters.simps)+
qed (auto split: sum_bind_splits simp add: small_step.zip_parameters.simps)
have "IA.to_int (⟦t⟧⇩I⇩A v⇩1) = i"
using v⇩n v⇩1 ssop⇩o unfolding linkParams'.simps represents_frame.simps
by (auto intro: operand_value_valid_var_mapping)
then have "⟦t⟧⇩I⇩A v⇩1 = IA.Int i"
using v⇩n v⇩1
unfolding linkParams'.simps represents_frame.simps
by (auto simp add: IA.assignment_def IA.IA_exp_to_tpoly IA.assignmentI)
then show ?thesis
using v⇩1 operand_value_valid_var_mapping v⇩n that
unfolding linkParams'.simps represents_frame.simps
by (auto simp add: IA.assignment_def v⇩2_s)
qed
then show ?thesis
by (rule valid_var_mapping.intros) (auto simp add: f⇩2_def)
qed
have "assig_of_state cs⇩1 (n, IA.IntT) = v⇩2 (lv, IA.IntT)" if a: "stack as⇩1 n = Some lv" for n lv
proof -
obtain y where y: "Mapping.lookup (frame.stack f⇩1) n = Some y"
using v⇩1 that a unfolding represents_frame.simps same_stack_names.simps by (auto)
moreover have "IA.Int (integerValue y) = v⇩1 (lv, IA.IntT)"
using v⇩1 y a unfolding represents_frame.simps valid_var_mapping.simps by (cases y) (auto)
moreover have "IA.Int (integerValue y) = v⇩1 (lv, IA.IntT)"
using v⇩1 y a unfolding represents_frame.simps valid_var_mapping.simps by (cases y) (auto)
ultimately show ?thesis
unfolding assig_of_state_def f⇩1 using a b by (auto simp add: v⇩2_v⇩1)
qed
moreover have "assig_of_state cs⇩2 (n, IA.IntT) = v⇩2 (lv, IA.IntT)" if a: "abstract_state.stack as⇩f n = Some lv " for n lv
proof -
obtain y where y: "Mapping.lookup (frame.stack f⇩2) n = Some y"
using cs⇩2 a d unfolding f⇩2_def represents_frame.simps same_stack_names.simps by fastforce
moreover have "IA.Int (integerValue y) = v⇩2 (lv, IA.IntT)"
using v⇩1 y a e unfolding represents_frame.simps valid_var_mapping.simps by (cases y) (auto)
ultimately show ?thesis
unfolding assig_of_state_def cs⇩2 using a by (auto simp add: v⇩2_v⇩1)
qed
ultimately have "as_as_step as⇩1 as⇩f (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
using 1 c v⇩2_kb v⇩2_assig assignment_assig_of_state
by (intro as_as_step.intros[where v=v⇩2 and v'=v⇩2]) (auto)
moreover have "represents_state cs⇩2 as⇩f"
using 1 d e v⇩2_assig v⇩2_kb f⇩2_def callCallInf
unfolding cs⇩2 f⇩2_def
by (auto simp add: represents_state.simps represents_frame.simps)
ultimately show ?thesis
by (auto)
next
case skip
have skipCallInf: "pos as⇩s = inc_pos (pos as⇩1)" "update_as as⇩1 as⇩s x v⇩n True⇩f"
using find_fun callInf(2)[unfolded skipCallInf.simps] by (force)+
obtain l i where c: "c = IntConstant l i"
using llvm_constant.exhaust by blast
define f⇩2 where "f⇩2 = update_pos (λ_. inc_pos (pos as⇩1)) (small_step.update_stack f⇩1 x c)"
have cs⇩2: "cs⇩2 = Llvm_state (f⇩2 # fs⇩1)"
using skip
by (auto simp add: small_step.update_frames_stack.simps small_step.update_frame.simps f⇩2_def
split: prod.splits)
define v⇩2 where "v⇩2 = v⇩1((v⇩n, IA.IntT) := IA.Int i)"
have a: "same_stack_names (frame.stack f⇩2) (abstract_state.stack as⇩s)"
using v⇩1 skipCallInf unfolding f⇩2_def c
by (auto intro: ssn_update simp add: represents_frame.simps small_step.update_stack.simps)
have b: "IA.assignment v⇩2"
using v⇩1 unfolding v⇩2_def represents_frame.simps by (auto)
have c: "valid_var_mapping (frame.stack f⇩2) (abstract_state.stack as⇩s) v⇩2"
using v⇩1 skipCallInf unfolding v⇩2_def f⇩2_def represents_frame.simps
by (auto intro: vvm_update simp add: small_step.update_stack.simps c)
have d: "v⇩2 ⊨⇩I⇩A kb as⇩1"
using v⇩1 skipCallInf by (simp add: update_as.simps represents_frame.simps v⇩2_def)
have e: "v⇩2 ⊨⇩I⇩A kb as⇩s"
by(rule IA.impliesD[where φ="kb as⇩1"])
(use skipCallInf b d in ‹auto simp add: update_as.simps ›)
have "assig_of_state cs⇩1 (n, IA.IntT) = v⇩2 (lv, IA.IntT)" if A: "abstract_state.stack as⇩1 n = Some lv" for n lv
proof -
obtain y where y: "Mapping.lookup (frame.stack f⇩1) n = Some y"
using v⇩1 that A unfolding represents_frame.simps same_stack_names.simps by (auto)
have "IA.Int (integerValue y) = v⇩1 (lv, IA.IntT)"
using v⇩1 y A unfolding represents_frame.simps valid_var_mapping.simps by (cases y) (auto)
then have "v⇩2 (lv, IA.IntT) = IA.Int (integerValue y)"
using skipCallInf A rangeI[where f="stack as⇩1" and x=n]
unfolding update_as.simps v⇩2_def by auto
then show ?thesis
unfolding assig_of_state_def f⇩1 using y by (auto simp add: v⇩2_def)
qed
moreover have "assig_of_state cs⇩2 (n, IA.IntT) = v⇩2 (lv, IA.IntT)" if A: "abstract_state.stack as⇩s n = Some lv " for n lv
proof -
obtain y where y: "Mapping.lookup (frame.stack f⇩2) n = Some y"
using cs⇩2 A a unfolding f⇩2_def represents_frame.simps same_stack_names.simps by fastforce
moreover have "IA.Int (integerValue y) = v⇩2 (lv, IA.IntT)"
using v⇩1 y A c unfolding represents_frame.simps valid_var_mapping.simps by (cases y) (auto)
ultimately show ?thesis
unfolding assig_of_state_def cs⇩2 using a by (auto simp add: v⇩2_def)
qed
ultimately have f: "as_as_step as⇩1 as⇩s (assig_of_state cs⇩1) (assig_of_state cs⇩2) id"
using 1 b e d assignment_assig_of_state by (auto intro: as_as_step.intros)
moreover have "represents_state cs⇩2 as⇩s"
using a b c e skipCallInf unfolding cs⇩2 f⇩2_def
by (auto simp add: represents_state.simps represents_frame.simps)
ultimately show ?thesis
by (auto)
qed
qed
context llvm_se_graph
begin
inductive callInf for n⇩1 n⇩f n⇩s where "callInf n⇩1 n⇩f n⇩s"
if
"callAsInf prog as⇩1 as⇩f as⇩s"
"as_of_node n⇩1 = as⇩1"
"as_of_node n⇩s = as⇩s"
"as_of_node n⇩f = as⇩f"
"n⇩1 ∈ nodes"
"n⇩f ∈ nodes" "(n⇩1,n⇩f) ∈ edges" "renaming_of_edge (n⇩1, n⇩f) = id"
"n⇩s ∈ nodes" "(n⇩1,n⇩s) ∈ edges" "renaming_of_edge (n⇩1, n⇩s) = id"
lemma callInf_represents_step':
assumes "callInf n⇩1 n⇩f n⇩s" "represents cs⇩1 n⇩1" "step' prog cs⇩1 (Inr cs⇩2)"
shows "represents cs⇩2 n⇩f ∧ ((n⇩1, assig_of_state cs⇩1), (n⇩f, assig_of_state cs⇩2)) ∈ as_step
∨ represents cs⇩2 n⇩s ∧ ((n⇩1, assig_of_state cs⇩1), (n⇩s, assig_of_state cs⇩2)) ∈ as_step"
using assms callInf_represents_step' unfolding callInf.simps represents.simps
by (fastforce intro!: as_as_as_step)
inductive valid_edge where
"valid_edge n" if "evalInf n n'"
| "valid_edge n" if "genInf n n'"
| "valid_edge n" if "refineInf n n⇩t n⇩f"
| "valid_edge n" if "branchInf n n'"
| "valid_edge n" if "condBranchInf n n'"
| "valid_edge n" if "icmpInf n n'"
| "valid_edge n" if "returnInf n"
| "valid_edge n" if "evalExternalInf n n'"
| "valid_edge n" if "callInf n n⇩f n⇩s"
definition seg_represents where
"seg_represents = (∀ n ∈ nodes. valid_edge n)"
context
fixes cs :: "nat ⇒ llvm_state"
assumes closed: seg_represents
and inf_run: "step' prog (cs i) (Inr (cs (Suc i)))"
begin
lemma closed_graph_inf_run_successor:
assumes repr: "represents (cs i) n"
shows "∃ j m. represents (cs j) m ∧ ((n, assig_of_state (cs i)), (m, assig_of_state (cs j))) ∈ as_step"
proof -
from repr[unfolded represents.simps] have n: "n ∈ nodes" by auto
from closed[unfolded seg_represents_def, rule_format, OF n]
consider (eval) n' where "evalInf n n'"
| (gen) n' where "genInf n n'"
| (ref) n⇩t n⇩f where "refineInf n n⇩t n⇩f"
| (br) n' where "branchInf n n'"
| (condbr) n' where "condBranchInf n n'"
| (icmp) n' where "icmpInf n n'"
| (ret) "returnInf n"
| (ext) n' where "evalExternalInf n n'"
| (call) n⇩f n⇩s where "callInf n n⇩f n⇩s"
unfolding valid_edge.simps by auto
then show ?thesis
proof cases
case (eval n')
from evalInf_represents_step'[OF eval repr inf_run] show ?thesis by auto
next
case (gen n')
from genInf_represents[OF gen repr] show ?thesis by auto
next
case (ref n⇩t n⇩f)
from refineInf_represents[OF ref repr] show ?thesis by auto
next
case (br n')
from branchInf_represents_step'[OF br repr inf_run] show ?thesis by auto
next
case (condbr n')
from condBranchInf_represents_step'[OF condbr repr inf_run] show ?thesis by auto
next
case (icmp n')
from icmpInf_represents_step'[OF icmp repr inf_run] show ?thesis by auto
next
case (ret)
have False
using returnInf_represents_step'[OF ret repr] returnInf_represents_unique_step'[OF ret repr]
inf_run by blast
then show ?thesis
by simp
next
case (ext n')
from evalExternalInf_represents_step'[OF ext repr inf_run] show ?thesis by auto
next
case (call n⇩f n⇩s)
from callInf_represents_step'[OF call repr inf_run] show ?thesis by auto
qed
qed
context
fixes n_init :: 'n
and i_init :: nat
assumes init: "represents (cs i_init) n_init"
begin
fun ni where
"ni 0 = (n_init, i_init)"
| "ni (Suc k) = (let nik = ni k in (SOME ni'. represents (cs (snd ni')) (fst ni') ∧
((fst nik, assig_of_state (cs (snd nik))), (fst ni', assig_of_state (cs (snd ni')))) ∈ as_step))"
lemmas ni_simps = ni.simps[unfolded Let_def]
declare ni.simps[simp del]
lemma inf_simulation: "((fst (ni k), assig_of_state (cs (snd (ni k))))
, (fst (ni (Suc k)), assig_of_state (cs (snd (ni (Suc k)))))) ∈ as_step"
(is "(?p k, ?p (Suc k)) ∈ _")
proof -
let ?c = "λ k. cs (snd (ni k))"
let ?n = "λ k. fst (ni k)"
have "?thesis ∧ represents (?c k) (?n k) ∧ represents (?c (Suc k)) (?n (Suc k))"
proof (induct k)
case 0
let ?cc = "?c 0"
let ?nn = "?n 0"
have c0: "?cc = cs i_init" and n0: "?nn = n_init" by (auto simp: ni.simps)
with init have repr: "represents ?cc ?nn" by simp
from closed_graph_inf_run_successor[OF this]
obtain j m where "represents (cs j) m" "(?p 0, m, assig_of_state (cs j)) ∈ as_step" by auto
hence "∃ p. represents (cs (snd p)) (fst p) ∧ (?p 0, fst p, assig_of_state (cs (snd p))) ∈ as_step"
by auto
from someI_ex[OF this, folded ni_simps] repr show ?case by auto
next
case (Suc k)
let ?cc = "?c (Suc k)"
let ?nn = "?n (Suc k)"
from Suc have repr: "represents ?cc ?nn" by simp
from closed_graph_inf_run_successor[OF this]
obtain j m where "represents (cs j) m" "(?p (Suc k), m, assig_of_state (cs j)) ∈ as_step" by auto
hence "∃ p. represents (cs (snd p)) (fst p) ∧ (?p (Suc k), fst p, assig_of_state (cs (snd p))) ∈ as_step"
by auto
from someI_ex[OF this, folded ni_simps] repr Suc show ?case by auto
qed
thus ?thesis ..
qed
end
end
end
fun initial_abstract_state where
"initial_abstract_state p fn as =
(let op = do {
fu ← find_fun p fn;
let bn = basic_block.name (hd_blocks fu);
let p = map parameter_name (params fu);
Inr (set p = dom (stack as) ∧ inj_on (stack as) (dom (stack as)) ∧ pos as = (fn, bn, 0)
∧ IA.valid (kb as))
}
in case op of Inr x ⇒ x | Inl _ ⇒ False)"
fun initial_llvm_frame where
"initial_llvm_frame p fn fr =
(let op = do {
fu ← find_fun p fn;
let bn = basic_block.name (hd_blocks fu);
let p = map parameter_name (params fu);
Inr (Mapping.keys (frame.stack fr) = set p ∧ frame.pos fr = (fn, bn, 0))
}
in case op of Inr x ⇒ x | Inl _ ⇒ False)"
fun initial_fun_llvm_state where
"initial_fun_llvm_state p fn s =
(case frames s of
(f#fs) ⇒ initial_llvm_frame p fn f
| [] ⇒ False)"
context llvm_se_graph
begin
lemma SN_as_step_imp_SN_step'_relation:
assumes seg_represents: seg_represents
and repr: "represents c n"
and SN: "SN_on as_step {(n, assig_of_state c)}"
shows "SN_on (step'_relation prog) {c}"
proof
fix cs :: "nat ⇒ llvm_state"
assume a: "cs 0 ∈ {c}"
hence repr: "represents (cs 0) n" using repr by auto
assume b: "∀ i. (cs i, cs (Suc i)) ∈ step'_relation prog"
hence inf_run: "step' prog (cs i) (Inr (cs (Suc i)))" for i
unfolding step'_relation_def by auto
define cs' where "cs' = (λi. (cs i, assig_of_state (cs i)))"
have c: "(fst (ni cs n 0 0), assig_of_state (cs (snd (ni cs n 0 0)))) ∈ {(n, assig_of_state c)}"
unfolding ni.simps[OF seg_represents, of cs, OF inf_run repr] using a by auto
note d = inf_simulation[OF seg_represents, of cs, OF inf_run repr, unfolded ni.simps]
show False
using c d SN by fast
qed
lemma SN_on_step'_step:
assumes "SN_on (step'_relation prog) {c}" "stack_size c = 1"
shows "SN_on (step_relation prog) {c}"
proof
fix cs :: "nat ⇒ llvm_state"
assume 1: "cs 0 ∈ {c}"
assume 2: "∀ i. (cs i, cs (Suc i)) ∈ step_relation prog"
then have "step prog (cs i) = Inr (cs (Suc i))" for i
unfolding step_relation_def by simp
then interpret inf_run cs prog
by unfold_locales simp
define cs' where "cs' x = cs (inf_run.r cs prog x)" for x
have 3: "cs' 0 = cs 0"
unfolding cs'_def
using stack_never_empty assms 1
apply(auto simp add: k⇩m⇩i⇩n_def min_stack_size_def s⇩c⇩s_def)
apply(rule arg_cong[of _ _ cs])
apply(rule Least_eq_0)
apply(simp add: image_def)
apply(rule Least_equality[symmetric])
apply(metis)
using nat_geq_1_eq_neqz by auto
have "step' prog (cs' i) (Inr (cs' (Suc i)))" for i
using inf_run_step' unfolding cs'_def by simp
then show False
using assms 1 3 step'_relation_def by blast
qed
lemma same_stack_names_dom:
assumes "dom m' = Mapping.keys m"
shows "same_stack_names m m'"
using assms by (auto intro!: same_stack_names.intros simp add: dom_def keys_dom_lookup)
lemma SN_on_initial_state:
assumes "SN_on as_step {(n, assig_of_state c)}"
"initial_abstract_state prog f (as_of_node n)" "n ∈ nodes"
"initial_llvm_frame prog f fr" "frames c = [fr]" "seg_represents"
shows "SN_on (step'_relation prog) {c}"
proof -
have "∃v. represents_frame (hd (frames c)) (as_of_node n) v"
proof -
let ?lookup_f = "Mapping.lookup (frame.stack (hd (frames c)))"
let ?lookup_as = "abstract_state.stack (as_of_node n)"
define v where "v =
(λt. case t of
(lv, IA.IntT) ⇒
(if (∃pv. ?lookup_as pv = Some lv)
then IA.Int (integerValue (the (?lookup_f (SOME pv. ?lookup_as pv = Some lv))))
else IA.Int 0)
| _ ⇒ IA.Bool True)"
have "IA.assignment v"
unfolding v_def by (auto split: prod.splits IA.ty.splits)
moreover have "same_stack_names (frame.stack (hd (frames c))) (abstract_state.stack (as_of_node n))"
using assms by (intro same_stack_names_dom) (auto split: list.splits sum_bind_splits)
moreover have "valid_var_mapping (frame.stack (hd (frames c))) (abstract_state.stack (as_of_node n)) v"
proof -
have "integerValue (the (?lookup_f (SOME pv. ?lookup_as pv = Some lv))) = i"
if a: "?lookup_f pv = Some (IntConstant l i)" "?lookup_as pv = Some lv"
for pv lv l i
proof -
have b: "x = pv" if "?lookup_as x = Some lv" for x
using assms a that by (auto split: option.splits sum_bind_splits simp add: domI inj_onD)
then have c: "integerValue (the (?lookup_f x)) = i"
if "abstract_state.stack (as_of_node n) x = Some lv" for x
using that a by (subst b) (auto)
show ?thesis
by(rule someI2[of _ pv])
(use that assms c in ‹auto split: option.splits Option.bind_splits›)
qed
then show ?thesis
by (auto intro!: valid_var_mapping.intros simp add: v_def)
qed
ultimately show ?thesis
using assms
by (intro exI[of _ v]) (auto intro: represents_frame.intros split: list.splits sum_bind_splits)
qed
then have "represents c n"
using assms unfolding represents.simps represents_state.simps
by (auto split: option.splits)
then show ?thesis
using assms by (auto intro: SN_as_step_imp_SN_step'_relation)
qed
end
unbundle no_IA_formula_notation
end