theory SALOverflowPlatform_deep = SALSafetyLogic_deep + TupleOrd:

section {* SAL Overflow Platform *}

text {* In this theory we instantiate a wellformedness checker and the generic VCG from the PCC Framework. *}

subsection {* Wellformedness Checker *}

consts
  checkPos :: "SALprogram \<Rightarrow> (pos list) \<Rightarrow> bool"

primrec
 "checkPos prg [] = True"
 "checkPos prg (pc # pcs) = (if (let (pn, i) = pc in (case (cmd prg pc) of
    None \<Rightarrow> False
  | Some c \<Rightarrow> (case c of
      SET x n \<Rightarrow> True
    | ADD x y \<Rightarrow> True
    | SUB x y \<Rightarrow> True
    | INC x \<Rightarrow> True
    | JMPEQ x y t \<Rightarrow> (t = 0) \<longrightarrow> ((anF prg (pn, i)) \<noteq> None)
    | JMPL x y t \<Rightarrow> (t = 0) \<longrightarrow> ((anF prg (pn, i)) \<noteq> None)
    | JLE x y t \<Rightarrow> (t = 0) \<longrightarrow> ((anF prg (pn, i)) \<noteq> None)
    | JMPB  t \<Rightarrow> ((anF prg (pn, i - t)) \<noteq> None)
    | JMPI x \<Rightarrow> (case (anF prg pc) of None \<Rightarrow> False | Some A \<Rightarrow> jumptargets pn x A \<noteq> [])
    | CALL x pn' \<Rightarrow> (anF prg (pn', 0) \<noteq> None)
    | RET x \<Rightarrow> (list_all (\<lambda> (pc, B). anF prg pc \<noteq> None) (ret_succs prg pc x (callpoints prg pn))) \<and> (0 < pn)
    | MOV s t \<Rightarrow> True
    | HALT \<Rightarrow> True
 ))) 
  then (checkPos prg pcs)
  else False)"

constdefs
  wf :: "SALprogram \<Rightarrow> bool" 
 "wf prg \<equiv> checkPos prg (domC prg)"

constdefs
  domA :: "SALprogram \<Rightarrow> pos list"
 "domA \<equiv> \<lambda> prg. [pc\<in> domC prg. (anF prg pc) \<noteq> None]"


constdefs
  vcgSALDeep :: "SALprogram \<Rightarrow> SALform"
 "vcgSALDeep prg \<equiv> vcG Conj Impl FalseF ipc initF safeF succsF wpF domC domA anF prg"

syntax
  callmem :: "env \<Rightarrow> tram" ("\<m> _")
  callpc :: "env \<Rightarrow> pos" ("\<pc> _")
  callenv :: "env \<Rightarrow> env" ("\<e> _")


subsection {* Generate ML code for the VCG *}

(*<*)
types_code
  set ("(_ -> bool)")

consts_code
  "op :" ("(_ |> _)")
  "Collect" ("(_)")


ML {* fun term_of_fun_type _ _ _ _= error "term_of_fun_type applied" *} 

ML {* fun term_of_bool  _ = error "term_of_bool applied" *} 
(*>*)
                                                                                    
generate_code ("vcgSALDeep.ML") [term_of]
  vcg = "vcgSALDeep"

end