src/HOL/BCV/JVM.thy

*** empty log message ***

(*  Title:      HOL/BCV/JVM.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   2000 TUM

A micro-JVM
*)

JVM = Kildall + JType + Opt + Product +

types mname
arities mname :: term

datatype instr =
    Load nat | Store nat | AConst_Null | IConst int
  | IAdd | Getfield ty cname | Putfield ty cname
  | New cname
  | Invoke cname mname ty ty
  | CmpEq nat
  | Return

types mdict = "cname => (mname * ty ~=> ty)"

constdefs
 wfi :: subclass => mdict => nat => instr => bool
"wfi S md maxr i == case i of
   Load n => n < maxr
 | Store n => n < maxr
 | AConst_Null => True
 | IConst j => True
 | IAdd => True
 | Getfield T C => is_type S T & is_type S (Class C)
 | Putfield T C => is_type S T & is_type S (Class C)
 | New C => is_type S (Class C)
 | Invoke C m pT rT => md C (m,pT) = Some(rT)
 | CmpEq n => True
 | Return => True"

 wfis :: subclass => mdict => nat => instr list => bool
"wfis S md maxr ins == !i : set ins. wfi S md maxr i"

types config = "ty list * ty err list"
      state  = config err option

constdefs
 stk_esl :: subclass => nat => ty list esl
"stk_esl S maxs == upto_esl maxs (JType.esl S)"

 reg_sl :: subclass => nat => ty err list sl
"reg_sl S maxr == Listn.sl maxr (Err.sl (JType.esl S))"

 sl :: subclass => nat => nat => state sl
"sl S maxs maxr ==
 Opt.sl(Err.sl(Product.esl (stk_esl S maxs) (Err.esl(reg_sl S maxr))))"

 states :: subclass => nat => nat => state set
"states S maxs maxr == fst(sl S maxs maxr)"

 le :: subclass => nat => nat => state ord
"le S maxs maxr == fst(snd(sl S maxs maxr))"

 sup :: subclass => nat => nat => state binop
"sup S maxs maxr == snd(snd(sl S maxs maxr))"

syntax "@lle" :: state => subclass => state => bool
       ("(_ /<<='__ _)" [50, 1000, 51] 50)

translations
"x <<=_S y" => "x <=_(le S arbitrary arbitrary) y"

constdefs

 wf_mdict :: subclass => mdict => bool
"wf_mdict S md ==
 !C mpT rT. md C mpT = Some(rT)
    --> is_type S rT &
        (!C'. (C',C) : S^*
            --> (EX rT'. md C' mpT = Some(rT') & rT' [=_S rT))"

 wti :: subclass => nat => ty => instr list => state list => nat => bool
"wti S maxs rT bs ss p ==
 case ss!p of
   None => True
 | Some e =>
 (case e of
   Err => False
 | OK (st,reg) =>
 (case bs!p of
   Load n => size st < maxs &
             (? T. reg!n = OK T & Some(OK(T#st,reg)) <<=_S ss!(p+1))
 | Store n => (? T Ts. st = T#Ts & Some(OK(Ts,reg[n := OK T])) <<=_S ss!(p+1))
 | AConst_Null => size st < maxs & Some(OK(NullT#st,reg)) <<=_S ss!(p+1)
 | IConst i => size st < maxs & Some(OK(Integer#st,reg)) <<=_S ss!(p+1)
 | IAdd => (? Ts. st = Integer#Integer#Ts &
                  Some(OK(Integer#Ts,reg)) <<=_S ss!(p+1))
 | Getfield fT C => (? T Ts. st = T#Ts & T [=_S Class(C) &
                            Some(OK(fT#Ts,reg)) <<=_S ss!(p+1))
 | Putfield fT C => (? vT oT Ts. st = vT#oT#Ts & vT [=_S fT & oT [=_S Class C &
                                 Some(OK(Ts,reg)) <<=_S ss!(p+1))
 | New C => (size st < maxs & Some(OK((Class C)#st,reg)) <<=_S ss!(p+1))
 | Invoke C m pT rT =>
   (? aT oT Ts. st = aT#oT#Ts & oT [=_S Class C & aT [=_S pT &
                Some(OK(rT#Ts,reg)) <<=_S ss!(p+1))
 | CmpEq q => (? T1 T2 Ts. st = T1#T2#Ts & (T1=T2 | is_ref T1 & is_ref T2) &
                           Some(OK(Ts,reg)) <<=_S ss!(p+1) &
                           Some(OK(Ts,reg)) <<=_S ss!q)
 | Return => (? T Ts. st = T#Ts & T [=_S rT)))"

 succs :: "instr list => nat => nat list"
"succs bs p ==
  case bs!p of
    Load n       => [p+1]
  | Store n      => [p+1]
  | AConst_Null  => [p+1]
  | IConst i     => [p+1]
  | IAdd         => [p+1]
  | Getfield x C => [p+1]
  | Putfield x C => [p+1]
  | New C        => [p+1]
  | Invoke C m pT rT => [p+1]
  | CmpEq q      => [p+1,q]
  | Return       => [p]"

 exec :: "subclass => nat => ty => instr => config => config err"
"exec S maxs rT instr == %(st,reg).
  case instr of
    Load n => if size st < maxs
              then case reg!n of Err => Err | OK T => OK(T#st,reg)
              else Err
  | Store n => (case st of [] => Err | T#Ts => OK(Ts,reg[n := OK T]))
  | AConst_Null => if size st < maxs then OK(NullT#st,reg) else Err
  | IConst i => if size st < maxs then OK(Integer#st,reg) else Err
  | IAdd =>
      (case st of [] => Err | T1#st1 =>
      (case st1 of [] => Err | T2#st2 =>
       if T1 = Integer & T2 = Integer then OK(st1,reg) else Err))
  | Getfield fT C =>
      (case st of [] => Err | oT#st' =>
      (if oT [=_S Class(C) then OK(fT#st',reg) else Err))
  | Putfield fT C =>
      (case st of [] => Err | vT#st1 =>
      (case st1 of [] => Err | oT#st2 =>
       if vT [=_S fT & oT [=_S Class C then OK(st2,reg) else Err))
  | New C => if size st < maxs then OK((Class C)#st,reg) else Err
  | Invoke C m pT rT =>
      (case st of [] => Err | aT#st1 =>
      (case st1 of [] => Err | oT#st2 =>
       if oT [=_S Class C & aT [=_S pT then OK(rT#st2,reg) else Err))
  | CmpEq q =>
      (case st of [] => Err | T1#st1 =>
      (case st1 of [] => Err | T2#st2 =>
       if T1=T2 | is_ref T1 & is_ref T2 then OK(st2,reg) else Err))
  | Return =>
      (case st of [] => Err | T#Ts =>
       if T [=_S rT then OK(st,reg) else Err)"

 step :: "subclass => nat => ty => instr list => nat => state => state"
"step S maxs rT bs p == option_map (lift (exec S maxs rT (bs!p)))"

 kiljvm ::
    "subclass => nat => nat => ty => instr list => state list => state list"
"kiljvm S maxs maxr rT bs ==
 kildall (sl S maxs maxr) (step S maxs rT bs) (succs bs)"

end