Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Effect.thy Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/MicroJava/BV/Effect.thy
    Author:     Gerwin Klein
    Copyright   2000 Technische Universitaet Muenchen
*)

section \<open>Effect of Instructions on the State Type\<close>

theory Effect
imports JVMType "../JVM/JVMExceptions"
begin

type_synonym succ_type = "(p_count \ state_type option) list"

text \<open>Program counter of successor instructions:\<close>
primrec succs :: "instr \ p_count \ p_count list" where
  "succs (Load idx) pc = [pc+1]"
| "succs (Store idx) pc = [pc+1]"
| "succs (LitPush v) pc = [pc+1]"
| "succs (Getfield F C) pc = [pc+1]"
| "succs (Putfield F C) pc = [pc+1]"
| "succs (New C) pc = [pc+1]"
| "succs (Checkcast C) pc = [pc+1]"
| "succs Pop pc = [pc+1]"
| "succs Dup pc = [pc+1]"
| "succs Dup_x1 pc = [pc+1]"
| "succs Dup_x2 pc = [pc+1]"
| "succs Swap pc = [pc+1]"
| "succs IAdd pc = [pc+1]"
| "succs (Ifcmpeq b) pc = [pc+1, nat (int pc + b)]"
| "succs (Goto b) pc = [nat (int pc + b)]"
| "succs Return pc = [pc]"
| "succs (Invoke C mn fpTs) pc = [pc+1]"
| "succs Throw pc = [pc]"

text "Effect of instruction on the state type:"

fun eff' :: "instr \ jvm_prog \ state_type \ state_type"
where
"eff' (Load idx, G, (ST, LT)) = (ok_val (LT ! idx) # ST, LT)" |
"eff' (Store idx, G, (ts#ST, LT)) = (ST, LT[idx:= OK ts])" |
"eff' (LitPush v, G, (ST, LT)) = (the (typeof (\v. None) v) # ST, LT)" |
"eff' (Getfield F C, G, (oT#ST, LT)) = (snd (the (field (G,C) F)) # ST, LT)" |
"eff' (Putfield F C, G, (vT#oT#ST, LT)) = (ST,LT)" |
"eff' (New C, G, (ST,LT)) = (Class C # ST, LT)" |
"eff' (Checkcast C, G, (RefT rt#ST,LT)) = (Class C # ST,LT)" |
"eff' (Pop, G, (ts#ST,LT)) = (ST,LT)" |
"eff' (Dup, G, (ts#ST,LT)) = (ts#ts#ST,LT)" |
"eff' (Dup_x1, G, (ts1#ts2#ST,LT)) = (ts1#ts2#ts1#ST,LT)" |
"eff' (Dup_x2, G, (ts1#ts2#ts3#ST,LT)) = (ts1#ts2#ts3#ts1#ST,LT)" |
"eff' (Swap, G, (ts1#ts2#ST,LT)) = (ts2#ts1#ST,LT)" |
"eff' (IAdd, G, (PrimT Integer#PrimT Integer#ST,LT))
                                         = (PrimT Integer#ST,LT)" |
"eff' (Ifcmpeq b, G, (ts1#ts2#ST,LT)) = (ST,LT)" |
"eff' (Goto b, G, s) = s" |
  \<comment> \<open>Return has no successor instruction in the same method\<close>
"eff' (Return, G, s) = s" |
  \<comment> \<open>Throw always terminates abruptly\<close>
"eff' (Throw, G, s) = s" |
"eff' (Invoke C mn fpTs, G, (ST,LT)) = (let ST' = drop (length fpTs) ST
  in  (fst (snd (the (method (G,C) (mn,fpTs))))#(tl ST'),LT))"

primrec match_any :: "jvm_prog \ p_count \ exception_table \ cname list" where
  "match_any G pc [] = []"
| "match_any G pc (e#es) = (let (start_pc, end_pc, handler_pc, catch_type) = e;
                                es' = match_any G pc es
                            in
                            if start_pc <= pc \<and> pc < end_pc then catch_type#es' else es')"

primrec match :: "jvm_prog \ xcpt \ p_count \ exception_table \ cname list" where
  "match G X pc [] = []"
| "match G X pc (e#es) =
  (if match_exception_entry G (Xcpt X) pc e then [Xcpt X] else match G X pc es)"

lemma match_some_entry:
  "match G X pc et = (if \e \ set et. match_exception_entry G (Xcpt X) pc e then [Xcpt X] else [])"
  by (induct et) auto

fun
  xcpt_names :: "instr \ jvm_prog \ p_count \ exception_table \ cname list"
where
  "xcpt_names (Getfield F C, G, pc, et) = match G NullPointer pc et"
| "xcpt_names (Putfield F C, G, pc, et) = match G NullPointer pc et"
| "xcpt_names (New C, G, pc, et) = match G OutOfMemory pc et"
| "xcpt_names (Checkcast C, G, pc, et) = match G ClassCast pc et"
| "xcpt_names (Throw, G, pc, et) = match_any G pc et"
| "xcpt_names (Invoke C m p, G, pc, et) = match_any G pc et"
| "xcpt_names (i, G, pc, et) = []"

definition xcpt_eff :: "instr \ jvm_prog \ p_count \ state_type option \ exception_table \ succ_type" where
  "xcpt_eff i G pc s et ==
   map (\<lambda>C. (the (match_exception_table G C pc et), case s of None \<Rightarrow> None | Some s' \<Rightarrow> Some ([Class C], snd s')))
       (xcpt_names (i,G,pc,et))"

definition norm_eff :: "instr \ jvm_prog \ state_type option \ state_type option" where
  "norm_eff i G == map_option (\s. eff' (i,G,s))"

definition eff :: "instr \ jvm_prog \ p_count \ exception_table \ state_type option \ succ_type" where
  "eff i G pc et s == (map (\pc'. (pc',norm_eff i G s)) (succs i pc)) @ (xcpt_eff i G pc s et)"

definition isPrimT :: "ty \ bool" where
  "isPrimT T == case T of PrimT T' \ True | RefT T' \ False"

definition isRefT :: "ty \ bool" where
  "isRefT T == case T of PrimT T' \ False | RefT T' \ True"

lemma isPrimT [simp]:
  "isPrimT T = (\T'. T = PrimT T')" by (simp add: isPrimT_def split: ty.splits)

lemma isRefT [simp]:
  "isRefT T = (\T'. T = RefT T')" by (simp add: isRefT_def split: ty.splits)

lemma "list_all2 P a b \ \(x,y) \ set (zip a b). P x y"
  by (simp add: list_all2_iff)

text "Conditions under which eff is applicable:"

fun
app' :: "instr \ jvm_prog \ p_count \ nat \ ty \ state_type \ bool"
where
"app' (Load idx, G, pc, maxs, rT, s) =
  (idx < length (snd s) \<and> (snd s) ! idx \<noteq> Err \<and> length (fst s) < maxs)" |
"app' (Store idx, G, pc, maxs, rT, (ts#ST, LT)) =
  (idx < length LT)" |
"app' (LitPush v, G, pc, maxs, rT, s) =
  (length (fst s) < maxs \<and> typeof (\<lambda>t. None) v \<noteq> None)" |
"app' (Getfield F C, G, pc, maxs, rT, (oT#ST, LT)) =
  (is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
  G \<turnstile> oT \<preceq> (Class C))" |
"app' (Putfield F C, G, pc, maxs, rT, (vT#oT#ST, LT)) =
  (is_class G C \<and> field (G,C) F \<noteq> None \<and> fst (the (field (G,C) F)) = C \<and>
  G \<turnstile> oT \<preceq> (Class C) \<and> G \<turnstile> vT \<preceq> (snd (the (field (G,C) F))))" |
"app' (New C, G, pc, maxs, rT, s) =
  (is_class G C \<and> length (fst s) < maxs)" |
"app' (Checkcast C, G, pc, maxs, rT, (RefT rt#ST,LT)) =
  (is_class G C)" |
"app' (Pop, G, pc, maxs, rT, (ts#ST,LT)) =
  True" |
"app' (Dup, G, pc, maxs, rT, (ts#ST,LT)) =
  (1+length ST < maxs)" |
"app' (Dup_x1, G, pc, maxs, rT, (ts1#ts2#ST,LT)) =
  (2+length ST < maxs)" |
"app' (Dup_x2, G, pc, maxs, rT, (ts1#ts2#ts3#ST,LT)) =
  (3+length ST < maxs)" |
"app' (Swap, G, pc, maxs, rT, (ts1#ts2#ST,LT)) =
  True" |
"app' (IAdd, G, pc, maxs, rT, (PrimT Integer#PrimT Integer#ST,LT)) =
  True" |
"app' (Ifcmpeq b, G, pc, maxs, rT, (ts#ts'#ST,LT)) =
  (0 \<le> int pc + b \<and> (isPrimT ts \<and> ts' = ts \<or> isRefT ts \<and> isRefT ts'))" |
"app' (Goto b, G, pc, maxs, rT, s) =
  (0 \<le> int pc + b)" |
"app' (Return, G, pc, maxs, rT, (T#ST,LT)) =
  (G \<turnstile> T \<preceq> rT)" |
"app' (Throw, G, pc, maxs, rT, (T#ST,LT)) =
  isRefT T" |
"app' (Invoke C mn fpTs, G, pc, maxs, rT, s) =
  (length fpTs < length (fst s) \<and>
  (let apTs = rev (take (length fpTs) (fst s));
       X    = hd (drop (length fpTs) (fst s))
   in
       G \<turnstile> X \<preceq> Class C \<and> is_class G C \<and> method (G,C) (mn,fpTs) \<noteq> None \<and>
       list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs fpTs))" |

"app' (i,G, pc,maxs,rT,s) = False"

definition xcpt_app :: "instr \ jvm_prog \ nat \ exception_table \ bool" where
  "xcpt_app i G pc et \ \C\set(xcpt_names (i,G,pc,et)). is_class G C"

definition app :: "instr \ jvm_prog \ nat \ ty \ nat \ exception_table \ state_type option \ bool" where
  "app i G maxs rT pc et s == case s of None \ True | Some t \ app' (i,G,pc,maxs,rT,t) \ xcpt_app i G pc et"

lemma match_any_match_table:
  "C \ set (match_any G pc et) \ match_exception_table G C pc et \ None"
  apply (induct et)
   apply simp
  apply simp
  apply clarify
  apply (simp split: if_split_asm)
  apply (auto simp add: match_exception_entry_def)
  done

lemma match_X_match_table:
  "C \ set (match G X pc et) \ match_exception_table G C pc et \ None"
  apply (induct et)
   apply simp
  apply (simp split: if_split_asm)
  done

lemma xcpt_names_in_et:
  "C \ set (xcpt_names (i,G,pc,et)) \
  \<exists>e \<in> set et. the (match_exception_table G C pc et) = fst (snd (snd e))"
  apply (cases i)
  apply (auto dest!: match_any_match_table match_X_match_table
              dest: match_exception_table_in_et)
  done

lemma 1: "2 < length a \ (\l l' l'' ls. a = l#l'#l''#ls)"
proof (cases a)
  fix x xs assume "a = x#xs" "2 < length a"
  thus ?thesis by - (cases xs, simp, cases "tl xs", auto)
qed auto

lemma 2: "\(2 < length a) \ a = [] \ (\ l. a = [l]) \ (\ l l'. a = [l,l'])"
proof -
  assume "\(2 < length a)"
  hence "length a < (Suc (Suc (Suc 0)))" by simp
  hence * : "length a = 0 \ length a = Suc 0 \ length a = Suc (Suc 0)"
    by (auto simp add: less_Suc_eq)

  {
    fix x
    assume "length x = Suc 0"
    hence "\ l. x = [l]" by (cases x) auto
  } note 0 = this

  have "length a = Suc (Suc 0) \ \l l'. a = [l,l']" by (cases a) (auto dest: 0)
  with * show ?thesis by (auto dest: 0)
qed

lemmas [simp] = app_def xcpt_app_def

text \<open>
\medskip
simp rules for \<^term>\<open>app\<close>
\<close>
lemma appNone[simp]: "app i G maxs rT pc et None = True" by simp

lemma appLoad[simp]:
"(app (Load idx) G maxs rT pc et (Some s)) = (\ST LT. s = (ST,LT) \ idx < length LT \ LT!idx \ Err \ length ST < maxs)"
  by (cases s, simp)

lemma appStore[simp]:
"(app (Store idx) G maxs rT pc et (Some s)) = (\ts ST LT. s = (ts#ST,LT) \ idx < length LT)"
  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)

lemma appLitPush[simp]:
"(app (LitPush v) G maxs rT pc et (Some s)) = (\ST LT. s = (ST,LT) \ length ST < maxs \ typeof (\v. None) v \ None)"
  by (cases s, simp)

lemma appGetField[simp]:
"(app (Getfield F C) G maxs rT pc et (Some s)) =
(\<exists> oT vT ST LT. s = (oT#ST, LT) \<and> is_class G C \<and>
  field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> (Class C) \<and> (\<forall>x \<in> set (match G NullPointer pc et). is_class G x))"
  by (cases s, cases "2 , auto dest!: 1 2)

lemma appPutField[simp]:
"(app (Putfield F C) G maxs rT pc et (Some s)) =
(\<exists> vT vT' oT ST LT. s = (vT#oT#ST, LT) \<and> is_class G C \<and>
  field (G,C) F = Some (C, vT') \ G \ oT \ (Class C) \ G \ vT \ vT' \
  (\<forall>x \<in> set (match G NullPointer pc et). is_class G x))"
  by (cases s, cases "2 , auto dest!: 1 2)

lemma appNew[simp]:
  "(app (New C) G maxs rT pc et (Some s)) =
  (\<exists>ST LT. s=(ST,LT) \<and> is_class G C \<and> length ST < maxs \<and>
  (\<forall>x \<in> set (match G OutOfMemory pc et). is_class G x))"
  by (cases s, simp)

lemma appCheckcast[simp]:
  "(app (Checkcast C) G maxs rT pc et (Some s)) =
  (\<exists>rT ST LT. s = (RefT rT#ST,LT) \<and> is_class G C \<and>
  (\<forall>x \<in> set (match G ClassCast pc et). is_class G x))"
  by (cases s, cases "fst s", simp) (cases "hd (fst s)", auto)

lemma appPop[simp]:
"(app Pop G maxs rT pc et (Some s)) = (\ts ST LT. s = (ts#ST,LT))"
  by (cases s, cases "2 , auto dest: 1 2)

lemma appDup[simp]:
"(app Dup G maxs rT pc et (Some s)) = (\ts ST LT. s = (ts#ST,LT) \ 1+length ST < maxs)"
  by (cases s, cases "2 , auto dest: 1 2)

lemma appDup_x1[simp]:
"(app Dup_x1 G maxs rT pc et (Some s)) = (\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \ 2+length ST < maxs)"
  by (cases s, cases "2 , auto dest: 1 2)

lemma appDup_x2[simp]:
"(app Dup_x2 G maxs rT pc et (Some s)) = (\ts1 ts2 ts3 ST LT. s = (ts1#ts2#ts3#ST,LT) \ 3+length ST < maxs)"
  by (cases s, cases "2 , auto dest: 1 2)

lemma appSwap[simp]:
"app Swap G maxs rT pc et (Some s) = (\ts1 ts2 ST LT. s = (ts1#ts2#ST,LT))"
  by (cases s, cases "2 ) (auto dest: 1 2)

lemma appIAdd[simp]:
"app IAdd G maxs rT pc et (Some s) = (\ ST LT. s = (PrimT Integer#PrimT Integer#ST,LT))"
  (is "?app s = ?P s")
proof (cases s)
  case (Pair a b)
  have "?app (a,b) = ?P (a,b)"
  proof (cases a)
    fix t ts assume a: "a = t#ts"
    show ?thesis
    proof (cases t)
      fix p assume p: "t = PrimT p"
      show ?thesis
      proof (cases p)
        assume ip: "p = Integer"
        show ?thesis
        proof (cases ts)
          fix t' ts' assume t': "ts = t' # ts'"
          show ?thesis
          proof (cases t')
            fix p' assume "t' = PrimT p'"
            with t' ip p a
            show ?thesis by (cases p') auto
          qed (auto simp add: a p ip t')
        qed (auto simp add: a p ip)
      qed (auto simp add: a p)
    qed (auto simp add: a)
  qed auto
  with Pair show ?thesis by simp
qed

lemma appIfcmpeq[simp]:
"app (Ifcmpeq b) G maxs rT pc et (Some s) =
  (\<exists>ts1 ts2 ST LT. s = (ts1#ts2#ST,LT) \<and> 0 \<le> int pc + b \<and>
  ((\<exists> p. ts1 = PrimT p \<and> ts2 = PrimT p) \<or> (\<exists>r r'. ts1 = RefT r \<and> ts2 = RefT r')))"
  by (cases s, cases "2 , auto dest!: 1 2)

lemma appReturn[simp]:
"app Return G maxs rT pc et (Some s) = (\T ST LT. s = (T#ST,LT) \ (G \ T \ rT))"
  by (cases s, cases "2 , auto dest: 1 2)

lemma appGoto[simp]:
"app (Goto b) G maxs rT pc et (Some s) = (0 \ int pc + b)"
  by simp

lemma appThrow[simp]:
  "app Throw G maxs rT pc et (Some s) =
  (\<exists>T ST LT r. s=(T#ST,LT) \<and> T = RefT r \<and> (\<forall>C \<in> set (match_any G pc et). is_class G C))"
  by (cases s, cases "2 < length (fst s)", auto dest: 1 2)

lemma appInvoke[simp]:
"app (Invoke C mn fpTs) G maxs rT pc et (Some s) = (\apTs X ST LT mD' rT' b'.
  s = ((rev apTs) @ (X # ST), LT) \<and> length apTs = length fpTs \<and> is_class G C \<and>
  G \<turnstile> X \<preceq> Class C \<and> (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>
  method (G,C) (mn,fpTs) = Some (mD', rT', b') \
  (\<forall>C \<in> set (match_any G pc et). is_class G C))" (is "?app s = ?P s")
proof (cases s)
  note list_all2_iff [simp]
  case (Pair a b)
  have "?app (a,b) \ ?P (a,b)"
  proof -
    assume app: "?app (a,b)"
    hence "a = (rev (rev (take (length fpTs) a))) @ (drop (length fpTs) a) \
           length fpTs < length a" (is "?a \<and> ?l")
      by auto
    hence "?a \ 0 < length (drop (length fpTs) a)" (is "?a \ ?l")
      by auto
    hence "?a \ ?l \ length (rev (take (length fpTs) a)) = length fpTs"
      by (auto)
    hence "\apTs ST. a = rev apTs @ ST \ length apTs = length fpTs \ 0 < length ST"
      by blast
    hence "\apTs ST. a = rev apTs @ ST \ length apTs = length fpTs \ ST \ []"
      by blast
    hence "\apTs ST. a = rev apTs @ ST \ length apTs = length fpTs \
           (\<exists>X ST'. ST = X#ST')"
      by (simp add: neq_Nil_conv)
    hence "\apTs X ST. a = rev apTs @ X # ST \ length apTs = length fpTs"
      by blast
    with app
    show ?thesis by clarsimp blast
  qed
  with Pair
  have "?app s \ ?P s" by (simp only:)
  moreover
  have "?P s \ ?app s" by (clarsimp simp add: min.absorb2)
  ultimately
  show ?thesis by (rule iffI)
qed

lemma effNone:
  "(pc', s') \ set (eff i G pc et None) \ s' = None"
  by (auto simp add: eff_def xcpt_eff_def norm_eff_def)

lemma xcpt_app_lemma [code]:
  "xcpt_app i G pc et = list_all (is_class G) (xcpt_names (i, G, pc, et))"
  by (simp add: list_all_iff)

lemmas [simp del] = app_def xcpt_app_def

end

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.