Theory JVM

Up to index of Isabelle/HOL/jsr

theory JVM = Typing_Framework_JVM + Kildall:
(*  Title:      HOL/MicroJava/BV/JVM.thy
    ID:         $Id: JVM.html,v 1.1 2002/11/28 14:17:20 kleing Exp $
    Author:     Tobias Nipkow, Gerwin Klein
    Copyright   2000 TUM
*)

header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *}

theory JVM = Typing_Framework_JVM + Kildall:

constdefs
  kiljvm :: "jvm_prog \<Rightarrow> cname \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> exception_table \<Rightarrow> 
             instr list \<Rightarrow> state list \<Rightarrow> state list"
  "kiljvm G C maxs maxr rT ini et bs \<equiv>
  kildall (JVMType.le) (JVMType.sup) (exec G C maxs rT ini et bs)"


  c_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> nat 
             \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> state list"
  "c_kil G C pTs rT ini mxs mxl et bs \<equiv>
  let this   = OK (if ini \<and> C \<noteq> Object then PartInit C else Init (Class C));
      first  = (([],this#(map (OK\<circ>Init) pTs)@(replicate mxl Err)), C=Object);
      start  = OK {first}#(replicate (size bs - 1) (OK {}))
  in kiljvm G C mxs (1+size pTs+mxl) rT ini et bs start"


  wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> bool \<Rightarrow> nat \<Rightarrow> nat 
             \<Rightarrow> exception_table \<Rightarrow> instr list \<Rightarrow> bool"
  "wt_kil G C pTs rT ini mxs mxl et bs \<equiv>
  0 < size bs \<and> (\<forall>n < size bs. c_kil G C pTs rT ini mxs mxl et bs ! n \<noteq> Err)"


  wt_jvm_prog_kildall :: "jvm_prog \<Rightarrow> bool"
  "wt_jvm_prog_kildall G \<equiv>
  wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). 
            wt_kil G C (snd sig) rT (fst sig=init) maxs maxl et b) G"



theorem (in start_context) is_bcv_kiljvm:
  "is_bcv r Err step (size bs) A (kiljvm G C mxs mxr rT (mn=init) et bs)"
  apply simp  
  apply (insert wf)
  apply (unfold kiljvm_def)
  apply (rule is_bcv_kildall)
       apply (fold sl_def2, rule semilat_JVM)
      apply (rule acc_JVM)
     apply (simp add: JVMType.le_def)
    apply (erule exec_pres_type)
   apply (rule bounded_exec)
  apply (erule exec_mono)
  done


lemma subset_replicate: "set (replicate n x) \<subseteq> {x}"
  by (induct n) auto

lemma in_set_replicate:
  "x \<in> set (replicate n y) \<Longrightarrow> x = y"
proof -
  assume "x \<in> set (replicate n y)"
  also have "set (replicate n y) \<subseteq> {y}" by (rule subset_replicate)
  finally have "x \<in> {y}" .
  thus ?thesis by simp
qed


lemma (in start_context) start_in_A [intro?]:
  "0 < size bs \<Longrightarrow> start \<in> list (size bs) A"
    apply (insert pTs C)
    apply (simp split del: split_if)
    apply (unfold states_def address_types_def init_tys_def)
    apply (auto simp add: map_compose split 
                intro!: listI list_appendI dest!: in_set_replicate)
    apply force+
    done   

theorem (in start_context) wt_kil_correct:
  assumes wtk: "wt_kil G C pTs rT (mn=init) mxs mxl et bs"
  shows "\<exists>phi. wt_method G C mn pTs rT mxs mxl bs et phi"
proof -
  from wtk obtain res where    
    result:   "res = kiljvm G C mxs mxr rT (mn=init) et bs start" and
    success:  "\<forall>n < size bs. res!n \<noteq> Err" and
    instrs:   "0 < size bs" 
    by (unfold wt_kil_def c_kil_def) (simp add: map_compose)
      
  have bcv:
    "is_bcv r Err step (size bs) A (kiljvm G C mxs mxr rT (mn=init) et bs)"
    by (rule is_bcv_kiljvm)
    
  from instrs have "start \<in> list (size bs) A" ..
  with bcv success result have 
    "\<exists>ts\<in>list (size bs) A. start <=[r] ts \<and> wt_step r Err step ts"
    by (unfold is_bcv_def) blast
  then obtain phi' where
    in_A: "phi' \<in> list (size bs) A" and
    s:    "start <=[r] phi'" and
    w:    "wt_step r Err step phi'"
    by blast
  hence wt_err_step: "wt_err_step (op \<subseteq>) step phi'"
    by (simp add: wt_err_step_def JVMType.le_def)

  from in_A have l: "size phi' = size bs" by simp  
  moreover {
    from in_A  have "check_types G mxs mxr (size bs) phi'" by (simp add: check_types_def)
    also from w
    have [symmetric]: "map OK (map ok_val phi') = phi'" 
      by (auto intro!: map_id simp add: wt_step_def not_Err_eq)
    finally  have "check_types G mxs mxr (size bs) (map OK (map ok_val phi'))" .
  } 
  moreover {  
    from s have "start!0 <=_r phi'!0" by (rule le_listD) simp
    moreover
    from instrs w l 
    have "phi'!0 \<noteq> Err" by (unfold wt_step_def) simp
    then obtain phi0 where "phi'!0 = OK phi0" by (auto simp add: not_Err_eq)
    ultimately
    have "wt_start G C mn pTs mxl (map ok_val phi')" using l instrs
      by (unfold wt_start_def) 
         (simp add: map_compose lesub_def JVMType.le_def Err.le_def)
  }
  moreover
  have bounded: "bounded step (length bs) A" by simp (rule bounded_exec)
  from in_A have "set phi' \<subseteq> A" by simp  
  with wt_err_step bounded
  have "wt_app_eff (op \<subseteq>) app eff (map ok_val phi')"
    by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def states_def)
  ultimately
  have "wt_method G C mn pTs rT mxs mxl bs et (map ok_val phi')"
    using instrs by (simp add: wt_method_def2)
  thus ?thesis by blast
qed


theorem (in start_context) wt_kil_complete:
  assumes wtm: "wt_method G C mn pTs rT mxs mxl bs et phi"
  shows "wt_kil G C pTs rT (mn=init) mxs mxl et bs"
proof -
  from wtm obtain
    instrs:   "0 < size bs" and
    length:   "length phi = length bs" and 
    ck_type:  "check_types G mxs mxr (size bs) (map OK phi)" and
    wt_start: "wt_start G C mn pTs mxl phi" and
    app_eff:  "wt_app_eff (op \<subseteq>) app eff phi"
    by (simp add: wt_method_def2)

  from ck_type
  have in_A: "set (map OK phi) \<subseteq> A" 
    by (simp add: check_types_def)  
  have bounded: "bounded step (size bs) A"
    by simp (rule bounded_exec)
  with app_eff in_A
  have "wt_err_step (op \<subseteq>) (err_step (size phi) app eff) (map OK phi)"
    by - (erule wt_app_eff_imp_wt_err,
          auto simp add: exec_def length states_def)
  hence wt_err: "wt_err_step (op \<subseteq>) step (map OK phi)"
    by (simp add: exec_def length) 
  have is_bcv: 
    "is_bcv r Err step (size bs) A (kiljvm G C mxs mxr rT (mn=init) et bs)"
    by (rule is_bcv_kiljvm)
  moreover
  from instrs have "start \<in> list (size bs) A" ..
  moreover
  let ?phi = "map OK phi"  
  have less_phi: "start <=[r] ?phi"
  proof (rule le_listI)
    from length instrs
    show "length start = length (map OK phi)" by simp
  next
    fix n
    from wt_start have "ok_val (start!0) \<subseteq> phi!0" 
      by (simp add: wt_start_def map_compose)
    moreover from instrs length have "0 < length phi" by simp
    ultimately have "start!0 <=_r ?phi!0" 
      by (simp add: JVMType.le_def Err.le_def lesub_def)
    moreover {
      fix n'
      have "OK {} <=_r ?phi!n"
        by (auto simp add: JVMType.le_def Err.le_def lesub_def 
                 split: err.splits)
      hence "\<lbrakk> n = Suc n'; n < size start \<rbrakk> 
             \<Longrightarrow> start!n <=_r ?phi!n" by simp
    }
    ultimately
    show "n < size start \<Longrightarrow> start!n <=_r ?phi!n" by (cases n, blast+)   
  qed
  moreover
  from ck_type length
  have "?phi \<in> list (size bs) A"
    by (auto intro!: listI simp add: check_types_def)
  moreover
  from wt_err have "wt_step r Err step ?phi" 
    by (simp add: wt_err_step_def JVMType.le_def)
  ultimately
  have "\<forall>p. p < size bs \<longrightarrow> kiljvm G C mxs mxr rT (mn=init) et bs start ! p \<noteq> Err" 
    by (unfold is_bcv_def) blast
  with instrs
  show "wt_kil G C pTs rT (mn=init) mxs mxl et bs" 
    by (unfold c_kil_def wt_kil_def) (simp add: map_compose)
qed


theorem jvm_kildall_correct:
  "wt_jvm_prog_kildall G = (\<exists>Phi. wt_jvm_prog G Phi)"
proof 
  let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in 
              SOME phi. wt_method G C (fst sig) (snd sig) rT maxs maxl ins et phi"

  -- "soundness"
  assume "wt_jvm_prog_kildall G"
  hence "wt_jvm_prog G ?Phi"
    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)    
    apply (erule jvm_prog_lift)
    apply (auto dest!: start_context.wt_kil_correct intro: someI)
    done
  thus "\<exists>Phi. wt_jvm_prog G Phi" by fast
next
  -- "completeness"
  assume "\<exists>Phi. wt_jvm_prog G Phi"
  thus "wt_jvm_prog_kildall G"
    apply (clarify)
    apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def)
    apply (erule jvm_prog_lift)
    apply (auto intro: start_context.wt_kil_complete)
    done
qed




end

theorem is_bcv_kiljvm:

  [| wf_prog wf_mb G; is_class G C; Init ` set pTs <= init_tys G (length bs) |]
  ==> is_bcv JVMType.le Err
       (Typing_Framework_JVM.exec G C mxs rT (mn = init) et bs) (length bs)
       (states G mxs (1 + length pTs + mxl) (length bs))
       (kiljvm G C mxs (1 + length pTs + mxl) rT (mn = init) et bs)

lemma subset_replicate:

  set (replicate n x) <= {x}

lemma in_set_replicate:

  x : set (replicate n y) ==> x = y

lemma start_in_A:

  [| wf_prog wf_mb G; is_class G C; Init ` set pTs <= init_tys G (length bs);
     0 < length bs |]
  ==> OK {(([], OK (if mn = init & C ~= Object then PartInit C
                    else Init (Class C)) #
                map (OK o Init) pTs @ replicate mxl Err),
           C = Object)} #
      replicate (length bs - 1) (OK {})
      : list (length bs) (states G mxs (1 + length pTs + mxl) (length bs))

theorem

  [| wf_prog wf_mb G; is_class G C; Init ` set pTs <= init_tys G (length bs);
     wt_kil G C pTs rT (mn = init) mxs mxl et bs |]
  ==> EX phi. wt_method G C mn pTs rT mxs mxl bs et phi

theorem

  [| wf_prog wf_mb G; is_class G C; Init ` set pTs <= init_tys G (length bs);
     wt_method G C mn pTs rT mxs mxl bs et phi |]
  ==> wt_kil G C pTs rT (mn = init) mxs mxl et bs

theorem jvm_kildall_correct:

  wt_jvm_prog_kildall G = (EX Phi. wt_jvm_prog G Phi)