Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/HOL/MicroJava/JVM/   (Beweissystem Isabelle Version 2025-1©)  Datei vom 16.11.2025 mit Größe 6 kB image not shown  

SSL JVMDefensive.thy   Interaktion und
PortierbarkeitIsabelle

 
(*  Title:      HOL/MicroJava/JVM/JVMDefensive.thy
    Author:     Gerwin Klein
*)

section \<open>A Defensive JVM\<close>

theory JVMDefensive
imports JVMExec
begin

text \<open>
  Extend the state space by one element indicating a type error (or
  other abnormal termination)\<close>
datatype 'a type_error = TypeError | Normal 'a


abbreviation
  fifth :: "'a \ 'b \ 'c \ 'd \ 'e \ 'f \ 'e"
  where "fifth x == fst(snd(snd(snd(snd x))))"

fun isAddr :: "val \ bool" where
  "isAddr (Addr loc) = True"
| "isAddr v = False"

fun isIntg :: "val \ bool" where
  "isIntg (Intg i) = True"
| "isIntg v = False"

definition isRef :: "val \ bool" where
  "isRef v \ v = Null \ isAddr v"

primrec check_instr :: "[instr, jvm_prog, aheap, opstack, locvars,
                  cname, sig, p_count, nat, frame list] \<Rightarrow> bool" where
  "check_instr (Load idx) G hp stk vars C sig pc mxs frs =
  (idx < length vars \<and> size stk < mxs)"

| "check_instr (Store idx) G hp stk vars Cl sig pc mxs frs =
  (0 < length stk \<and> idx < length vars)"

| "check_instr (LitPush v) G hp stk vars Cl sig pc mxs frs =
  (\<not>isAddr v \<and> size stk < mxs)"

| "check_instr (New C) G hp stk vars Cl sig pc mxs frs =
  (is_class G C \<and> size stk < mxs)"

| "check_instr (Getfield F C) G hp stk vars Cl sig pc mxs frs =
  (0 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> 
  (let (C', T) = the (field (G,C) F); ref = hd stk in
    C' = C \ isRef ref \ (ref \ Null \
      hp (the_Addr ref) \<noteq> None \<and> 
      (let (D,vs) = the (hp (the_Addr ref)) in 
        G \<turnstile> D \<preceq>C C \<and> vs (F,C) \<noteq> None \<and> G,hp \<turnstile> the (vs (F,C)) ::\<preceq> T))))" 

| "check_instr (Putfield F C) G hp stk vars Cl sig pc mxs frs =
  (1 < length stk \<and> is_class G C \<and> field (G,C) F \<noteq> None \<and> 
  (let (C', T) = the (field (G,C) F); v = hd stk; ref = hd (tl stk) in
    C' = C \ isRef ref \ (ref \ Null \
      hp (the_Addr ref) \<noteq> None \<and> 
      (let (D,vs) = the (hp (the_Addr ref)) in 
        G \<turnstile> D \<preceq>C C \<and> G,hp \<turnstile> v ::\<preceq> T))))" 

| "check_instr (Checkcast C) G hp stk vars Cl sig pc mxs frs =
  (0 < length stk \<and> is_class G C \<and> isRef (hd stk))"

| "check_instr (Invoke C mn ps) G hp stk vars Cl sig pc mxs frs =
  (length ps < length stk \<and> 
  (let n = length ps; v = stk!n in
  isRef v \<and> (v \<noteq> Null \<longrightarrow> 
    hp (the_Addr v) \<noteq> None \<and>
    method (G,cname_of hp v) (mn,ps) \<noteq> None \<and>
    list_all2 (\<lambda>v T. G,hp \<turnstile> v ::\<preceq> T) (rev (take n stk)) ps)))"
  
| "check_instr Return G hp stk0 vars Cl sig0 pc mxs frs =
  (0 < length stk0 \<and> (0 < length frs \<longrightarrow> 
    method (G,Cl) sig0 \<noteq> None \<and>    
    (let v = hd stk0;  (C, rT, body) = the (method (G,Cl) sig0) in
    Cl = C \<and> G,hp \<turnstile> v ::\<preceq> rT)))"
 
| "check_instr Pop G hp stk vars Cl sig pc mxs frs =
  (0 < length stk)"

| "check_instr Dup G hp stk vars Cl sig pc mxs frs =
  (0 < length stk \<and> size stk < mxs)"

| "check_instr Dup_x1 G hp stk vars Cl sig pc mxs frs =
  (1 < length stk \<and> size stk < mxs)"

| "check_instr Dup_x2 G hp stk vars Cl sig pc mxs frs =
  (2 < length stk \<and> size stk < mxs)"

| "check_instr Swap G hp stk vars Cl sig pc mxs frs =
  (1 < length stk)"

| "check_instr IAdd G hp stk vars Cl sig pc mxs frs =
  (1 < length stk \<and> isIntg (hd stk) \<and> isIntg (hd (tl stk)))"

| "check_instr (Ifcmpeq b) G hp stk vars Cl sig pc mxs frs =
  (1 < length stk \<and> 0 \<le> int pc+b)"

| "check_instr (Goto b) G hp stk vars Cl sig pc mxs frs =
  (0 \<le> int pc+b)"

| "check_instr Throw G hp stk vars Cl sig pc mxs frs =
  (0 < length stk \<and> isRef (hd stk))"

definition check :: "jvm_prog \ jvm_state \ bool" where
  "check G s \ let (xcpt, hp, frs) = s in
               (case frs of [] \<Rightarrow> True | (stk,loc,C,sig,pc)#frs' \<Rightarrow> 
                (let  (C',rt,mxs,mxl,ins,et) = the (method (G,C) sig); i = ins!pc in
                 pc < size ins \<and> 
                 check_instr i G hp stk loc C sig pc mxs frs'))"


definition exec_d :: "jvm_prog \ jvm_state type_error \ jvm_state option type_error" where
  "exec_d G s \ case s of
      TypeError \<Rightarrow> TypeError 
    | Normal s' \ if check G s' then Normal (exec (G, s')) else TypeError"


definition
  exec_all_d :: "jvm_prog \ jvm_state type_error \ jvm_state type_error \ bool"
                   (\<open>_ \<turnstile> _ \<midarrow>jvmd\<rightarrow> _\<close> [61,61,61]60) where
  "G \ s \jvmd\ t \
         (s,t) \<in> ({(s,t). exec_d G s = TypeError \<and> t = TypeError} \<union>
                  {(s,t). \<exists>t'. exec_d G s = Normal (Some t') \<and> t = Normal t'})\<^sup>*"


declare split_paired_All [simp del]
declare split_paired_Ex [simp del]

lemma [dest!]:
  "(if P then A else B) \ B \ P"
  by (cases P, auto)

lemma exec_d_no_errorI [intro]:
  "check G s \ exec_d G (Normal s) \ TypeError"
  by (unfold exec_d_def) simp

theorem no_type_error_commutes:
  "exec_d G (Normal s) \ TypeError \
  exec_d G (Normal s) = Normal (exec (G, s))"
  by (unfold exec_d_def, auto)


lemma defensive_imp_aggressive:
  "G \ (Normal s) \jvmd\ (Normal t) \ G \ s \jvm\ t"
proof -
  have "\x y. G \ x \jvmd\ y \ \s t. x = Normal s \ y = Normal t \ G \ s \jvm\ t"
    apply (unfold exec_all_d_def)
    apply (erule rtrancl_induct)
     apply (simp add: exec_all_def)
    apply (fold exec_all_d_def)
    apply simp
    apply (intro allI impI)
    apply (erule disjE, simp)
    apply (elim exE conjE)
    apply (erule allE, erule impE, assumption)
    apply (simp add: exec_all_def exec_d_def split: type_error.splits if_split_asm)
    apply (rule rtrancl_trans, assumption)
    apply blast
    done
  moreover
  assume "G \ (Normal s) \jvmd\ (Normal t)"
  ultimately
  show "G \ s \jvm\ t" by blast
qed

end

100%


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.12Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤

*Eine klare Vorstellung vom Zielzustand




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.