Theory J1State

(*  Title:      JinjaThreads/Compiler/J1State.thy
    Author:     Andreas Lochbihler
*)

section ‹The intermediate language J1›

theory J1State imports
  "../J/State"
  CallExpr
begin

type_synonym
  'addr expr1 = "(nat, nat, 'addr) exp"

type_synonym
  'addr J1_prog = "'addr expr1 prog"

type_synonym
  'addr locals1 = "'addr val list"

translations
  (type) "'addr expr1" <= (type) "(nat, nat, 'addr) exp"
  (type) "'addr J1_prog" <= (type) "'addr expr1 prog"

type_synonym
  'addr J1state = "('addr expr1 × 'addr locals1) list"

type_synonym
  ('addr, 'thread_id, 'heap) J1_thread_action = 
  "('addr, 'thread_id, ('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list,'heap) Jinja_thread_action"

type_synonym
  ('addr, 'thread_id, 'heap) J1_state = 
  "('addr,'thread_id,('addr expr1 × 'addr locals1) × ('addr expr1 × 'addr locals1) list,'heap,'addr) state"

(* pretty printing for J1_thread_action type *)
print_translation ‹
  let
    fun tr'
       [a1, t
       , Const (@{type_syntax "prod"}, _) $ 
           (Const (@{type_syntax "prod"}, _) $
              (Const (@{type_syntax "exp"}, _) $ Const (@{type_syntax "nat"}, _) $ Const (@{type_syntax "nat"}, _) $ a2) $
              (Const (@{type_syntax "list"}, _) $ (Const (@{type_syntax "val"}, _) $ a3))) $
           (Const (@{type_syntax "list"}, _) $
              (Const (@{type_syntax "prod"}, _) $
                (Const (@{type_syntax "exp"}, _) $ Const (@{type_syntax "nat"}, _) $ Const (@{type_syntax "nat"}, _) $ a4) $
                (Const (@{type_syntax "list"}, _) $ (Const (@{type_syntax "val"}, _) $ a5))))
       , h] =
      if a1 = a2 andalso a2 = a3 andalso a3 = a4 andalso a4 = a5 
      then Syntax.const @{type_syntax "J1_thread_action"} $ a1 $ t $ h
      else raise Match;
    in [(@{type_syntax "Jinja_thread_action"}, K tr')]
  end
›
typ "('addr,'thread_id,'heap) J1_thread_action"

(* pretty printing for J1_state type *)
print_translation ‹
  let
    fun tr'
       [a1, t
       , Const (@{type_syntax "prod"}, _) $ 
           (Const (@{type_syntax "prod"}, _) $
              (Const (@{type_syntax "exp"}, _) $ Const (@{type_syntax "nat"}, _) $ Const (@{type_syntax "nat"}, _) $ a2) $
              (Const (@{type_syntax "list"}, _) $ (Const (@{type_syntax "val"}, _) $ a3))) $
           (Const (@{type_syntax "list"}, _) $
              (Const (@{type_syntax "prod"}, _) $
                (Const (@{type_syntax "exp"}, _) $ Const (@{type_syntax "nat"}, _) $ Const (@{type_syntax "nat"}, _) $ a4) $
                (Const (@{type_syntax "list"}, _) $ (Const (@{type_syntax "val"}, _) $ a5))))
       , h, a6] =
      if a1 = a2 andalso a2 = a3 andalso a3 = a4 andalso a4 = a5 andalso a5 = a6
      then Syntax.const @{type_syntax "J1_state"} $ a1 $ t $ h
      else raise Match;
    in [(@{type_syntax "state"}, K tr')]
  end
›
typ "('addr, 'thread_id, 'heap) J1_state"

fun blocks1 :: "nat ⇒ ty list ⇒ (nat,'b,'addr) exp ⇒ (nat,'b,'addr) exp"
where 
  "blocks1 n [] e = e"
| "blocks1 n (T#Ts) e = {n:T=None; blocks1 (Suc n) Ts e}"

primrec max_vars:: "('a,'b,'addr) exp ⇒ nat"
  and max_varss:: "('a,'b,'addr) exp list ⇒ nat"
where
  "max_vars (new C) = 0"
| "max_vars (newA T⌊e⌉) = max_vars e"
| "max_vars (Cast C e) = max_vars e"
| "max_vars (e instanceof T) = max_vars e"
| "max_vars (Val v) = 0"
| "max_vars (e «bop» e') = max (max_vars e) (max_vars e')"
| "max_vars (Var V) = 0"
| "max_vars (V:=e) = max_vars e"
| "max_vars (a⌊i⌉) = max (max_vars a) (max_vars i)"
| "max_vars (AAss a i e) = max (max (max_vars a) (max_vars i)) (max_vars e)"
| "max_vars (a∙length) = max_vars a"
| "max_vars (e∙F{D}) = max_vars e"
| "max_vars (FAss e⇩1 F D e⇩2) = max (max_vars e⇩1) (max_vars e⇩2)"
| "max_vars (e∙compareAndSwap(D∙F, e', e'')) = max (max (max_vars e) (max_vars e')) (max_vars e'')"
| "max_vars (e∙M(es)) = max (max_vars e) (max_varss es)"
| "max_vars ({V:T=vo; e}) = max_vars e + 1"
― ‹sync and insync will need an extra local variable when compiling to bytecode to store the object that is being synchronized on until its release›
| "max_vars (sync⇘V⇙ (e') e) = max (max_vars e') (max_vars e + 1)"
| "max_vars (insync⇘V⇙ (a) e) = max_vars e + 1"
| "max_vars (e⇩1;;e⇩2) = max (max_vars e⇩1) (max_vars e⇩2)"
| "max_vars (if (e) e⇩1 else e⇩2) =
   max (max_vars e) (max (max_vars e⇩1) (max_vars e⇩2))"
| "max_vars (while (b) e) = max (max_vars b) (max_vars e)"
| "max_vars (throw e) = max_vars e"
| "max_vars (try e⇩1 catch(C V) e⇩2) = max (max_vars e⇩1) (max_vars e⇩2 + 1)"

| "max_varss [] = 0"
| "max_varss (e#es) = max (max_vars e) (max_varss es)"

― ‹Indices in blocks increase by 1›

primrec ℬ :: "'addr expr1 ⇒ nat ⇒ bool"
  and ℬs :: "'addr expr1 list ⇒ nat ⇒ bool"
where
  "ℬ (new C) i = True"
| "ℬ (newA T⌊e⌉) i = ℬ e i"
| "ℬ (Cast C e) i = ℬ e i"
| "ℬ (e instanceof T) i = ℬ e i"
| "ℬ (Val v) i = True"
| "ℬ (e1 «bop» e2) i = (ℬ e1 i ∧ ℬ e2 i)"
| "ℬ (Var j) i = True"
| "ℬ (j:=e) i = ℬ e i"
| "ℬ (a⌊j⌉) i = (ℬ a i ∧ ℬ j i)"
| "ℬ (a⌊j⌉:=e) i = (ℬ a i ∧ ℬ j i ∧ ℬ e i)"
| "ℬ (a∙length) i = ℬ a i"
| "ℬ (e∙F{D}) i = ℬ e i"
| "ℬ (e1∙F{D} := e2) i = (ℬ e1 i ∧ ℬ e2 i)"
| "ℬ (e∙compareAndSwap(D∙F, e', e'')) i = (ℬ e i ∧ ℬ e' i ∧ ℬ e'' i)"
| "ℬ (e∙M(es)) i = (ℬ e i ∧ ℬs es i)"
| "ℬ ({j:T=vo; e}) i = (i = j ∧ ℬ e (i+1))"
| "ℬ (sync⇘V⇙ (o') e) i = (i = V ∧ ℬ o' i ∧ ℬ e (i+1))"
| "ℬ (insync⇘V⇙ (a) e) i = (i = V ∧ ℬ e (i+1))"
| "ℬ (e1;;e2) i = (ℬ e1 i ∧ ℬ e2 i)"
| "ℬ (if (e) e1 else e2) i = (ℬ e i ∧ ℬ e1 i ∧ ℬ e2 i)"
| "ℬ (throw e) i = ℬ e i"
| "ℬ (while (e) c) i = (ℬ e i ∧ ℬ c i)"
| "ℬ (try e1 catch(C j) e2) i = (ℬ e1 i ∧ i=j ∧ ℬ e2 (i+1))"

| "ℬs [] i = True"
| "ℬs (e#es) i = (ℬ e i ∧ ℬs es i)"

text ‹
  Variables for monitor addresses do not occur freely in synchonization blocks
›

primrec syncvars :: "('a, 'a, 'addr) exp ⇒ bool"
  and syncvarss :: "('a, 'a, 'addr) exp list ⇒ bool"
where
  "syncvars (new C) = True"
| "syncvars (newA T⌊e⌉) = syncvars e"
| "syncvars (Cast T e) = syncvars e"
| "syncvars (e instanceof T) = syncvars e"
| "syncvars (Val v) = True"
| "syncvars (e1 «bop» e2) = (syncvars e1 ∧ syncvars e2)"
| "syncvars (Var V) = True"
| "syncvars (V:=e) = syncvars e"
| "syncvars (a⌊i⌉) = (syncvars a ∧ syncvars i)"
| "syncvars (a⌊i⌉ := e) = (syncvars a ∧ syncvars i ∧ syncvars e)"
| "syncvars (a∙length) = syncvars a"
| "syncvars (e∙F{D}) = syncvars e"
| "syncvars (e∙F{D} := e2) = (syncvars e ∧ syncvars e2)"
| "syncvars (e∙compareAndSwap(D∙F, e', e'')) = (syncvars e ∧ syncvars e' ∧ syncvars e'')"
| "syncvars (e∙M(es)) = (syncvars e ∧ syncvarss es)"
| "syncvars {V:T=vo;e} = syncvars e"
| "syncvars (sync⇘V⇙ (e1) e2) = (syncvars e1 ∧ syncvars e2 ∧ V ∉ fv e2)"
| "syncvars (insync⇘V⇙ (a) e) = (syncvars e ∧ V ∉ fv e)"
| "syncvars (e1;;e2) = (syncvars e1 ∧ syncvars e2)"
| "syncvars (if (b) e1 else e2) = (syncvars b ∧ syncvars e1 ∧ syncvars e2)"
| "syncvars (while (b) c) = (syncvars b ∧ syncvars c)"
| "syncvars (throw e) = syncvars e"
| "syncvars (try e1 catch(C V) e2) = (syncvars e1 ∧ syncvars e2)"

| "syncvarss [] = True"
| "syncvarss (e#es) = (syncvars e ∧ syncvarss es)"

definition bsok :: "'addr expr1 ⇒ nat ⇒ bool"
where "bsok e n ≡ ℬ e n ∧ expr_locks e = (λad. 0)"

definition bsoks :: "'addr expr1 list ⇒ nat ⇒ bool"
where "bsoks es n ≡ ℬs es n ∧ expr_lockss es = (λad. 0)"

primrec call1 :: "('a, 'b, 'addr) exp ⇒ ('addr × mname × 'addr val list) option"
  and calls1 :: "('a, 'b, 'addr) exp list ⇒ ('addr × mname × 'addr val list) option"
where
  "call1 (new C) = None"
| "call1 (newA T⌊e⌉) = call1 e"
| "call1 (Cast C e) = call1 e"
| "call1 (e instanceof T) = call1 e"
| "call1 (Val v) = None"
| "call1 (Var V) = None"
| "call1 (V:=e) = call1 e"
| "call1 (e «bop» e') = (if is_val e then call1 e' else call1 e)"
| "call1 (a⌊i⌉) = (if is_val a then call1 i else call1 a)"
| "call1 (AAss a i e) = (if is_val a then (if is_val i then call1 e else call1 i) else call1 a)"
| "call1 (a∙length) = call1 a"
| "call1 (e∙F{D}) = call1 e"
| "call1 (FAss e F D e') = (if is_val e then call1 e' else call1 e)"
| "call1 (CompareAndSwap e D F e' e'') = (if is_val e then (if is_val e' then call1 e'' else call1 e') else call1 e)"
| "call1 (e∙M(es)) = (if is_val e then
                     (if is_vals es ∧ is_addr e then ⌊(THE a. e = addr a, M, THE vs. es = map Val vs)⌋ else calls1 es) 
                     else call1 e)"
| "call1 ({V:T=vo; e}) = (case vo of None ⇒ call1 e | Some v ⇒ None)"
| "call1 (sync⇘V⇙ (o') e) = call1 o'"
| "call1 (insync⇘V⇙ (a) e) = call1 e"
| "call1 (e;;e') = call1 e"
| "call1 (if (e) e1 else e2) = call1 e"
| "call1 (while(b) e) = None"
| "call1 (throw e) = call1 e"
| "call1 (try e1 catch(C V) e2) = call1 e1"

| "calls1 [] = None"
| "calls1 (e#es) = (if is_val e then calls1 es else call1 e)"


lemma expr_locks_blocks1 [simp]:
  "expr_locks (blocks1 n Ts e) = expr_locks e"
by(induct n Ts e rule: blocks1.induct) simp_all

lemma max_varss_append [simp]:
  "max_varss (es @ es') = max (max_varss es) (max_varss es')"
by(induct es, auto)

lemma max_varss_map_Val [simp]: "max_varss (map Val vs) = 0"
by(induct vs) auto

lemma blocks1_max_vars:
  "max_vars (blocks1 n Ts e) = max_vars e + length Ts"
by(induct n Ts e rule: blocks1.induct)(auto)

lemma blocks_max_vars:
  "⟦ length vs = length pns; length Ts = length pns ⟧
  ⟹ max_vars (blocks pns Ts vs e) = max_vars e + length pns"
by(induct pns Ts vs e rule: blocks.induct)(auto)

lemma Bs_append [simp]: "ℬs (es @ es') n ⟷ ℬs es n ∧ ℬs es' n"
by(induct es) auto

lemma Bs_map_Val [simp]: "ℬs (map Val vs) n"
by(induct vs) auto

lemma B_blocks1 [intro]: "ℬ body (n + length Ts) ⟹ ℬ (blocks1 n Ts body) n"
by(induct n Ts body rule: blocks1.induct)(auto)

lemma B_extRet2J [simp]: "ℬ e n ⟹ ℬ (extRet2J e va) n"
by(cases va) auto

lemma B_inline_call: "⟦ ℬ e n; ⋀n. ℬ e' n ⟧ ⟹ ℬ (inline_call e' e) n"
  and Bs_inline_calls: "⟦ ℬs es n; ⋀n. ℬ e' n ⟧ ⟹ ℬs (inline_calls e' es) n"
by(induct e and es arbitrary: n and n rule: call.induct calls.induct) auto

lemma syncvarss_append [simp]: "syncvarss (es @ es') ⟷ syncvarss es ∧ syncvarss es'"
by(induct es) auto

lemma syncvarss_map_Val [simp]: "syncvarss (map Val vs)"
by(induct vs) auto

lemma bsok_simps [simp]:
  "bsok (new C) n = True"
  "bsok (newA T⌊e⌉) n = bsok e n"
  "bsok (Cast T e) n = bsok e n"
  "bsok (e instanceof T) n = bsok e n"
  "bsok (e1 «bop» e2) n = (bsok e1 n ∧ bsok e2 n)"
  "bsok (Var V) n = True"
  "bsok (Val v) n = True"
  "bsok (V := e) n = bsok e n"
  "bsok (a⌊i⌉) n = (bsok a n ∧ bsok i n)"
  "bsok (a⌊i⌉ := e) n = (bsok a n ∧ bsok i n ∧ bsok e n)"
  "bsok (a∙length) n = bsok a n"
  "bsok (e∙F{D}) n = bsok e n"
  "bsok (e∙F{D} := e') n = (bsok e n ∧ bsok e' n)"
  "bsok (e∙compareAndSwap(D∙F, e', e'')) n = (bsok e n ∧ bsok e' n ∧ bsok e'' n)"
  "bsok (e∙M(ps)) n = (bsok e n ∧ bsoks ps n)"
  "bsok {V:T=vo; e} n = (bsok e (Suc n) ∧ V = n)"
  "bsok (sync⇘V⇙ (e) e') n = (bsok e n ∧ bsok e' (Suc n) ∧ V = n)"
  "bsok (insync⇘V⇙ (ad) e) n = False"
  "bsok (e;; e') n = (bsok e n ∧ bsok e' n)"
  "bsok (if (e) e1 else e2) n = (bsok e n ∧ bsok e1 n ∧ bsok e2 n)"
  "bsok (while (b) c) n = (bsok b n ∧ bsok c n)"
  "bsok (throw e) n = bsok e n"
  "bsok (try e catch(C V) e') n = (bsok e n ∧ bsok e' (Suc n) ∧ V = n)"
  and bsoks_simps [simp]:
  "bsoks [] n = True"
  "bsoks (e # es) n = (bsok e n ∧ bsoks es n)"
by(auto simp add: bsok_def bsoks_def fun_eq_iff)

lemma call1_callE:
  assumes "call1 (obj∙M(pns)) = ⌊(a, M', vs)⌋"
  obtains (CallObj) "call1 obj = ⌊(a, M', vs)⌋"
  | (CallParams) v where "obj = Val v" "calls1 pns = ⌊(a, M', vs)⌋"
  | (Call) "obj = addr a" "pns = map Val vs" "M = M'"
using assms by(auto split: if_split_asm simp add: is_vals_conv)

lemma calls1_map_Val_append [simp]:
  "calls1 (map Val vs @ es) = calls1 es"
by(induct vs) simp_all

lemma calls1_map_Val [simp]:
  "calls1 (map Val vs) = None"
by(induct vs) simp_all

lemma fixes e :: "('a, 'b, 'addr) exp" and es :: "('a, 'b, 'addr) exp list"
  shows call1_imp_call: "call1 e = ⌊aMvs⌋ ⟹ call e = ⌊aMvs⌋"
  and calls1_imp_calls: "calls1 es = ⌊aMvs⌋ ⟹ calls es = ⌊aMvs⌋"
by(induct e and es rule: call1.induct calls1.induct) auto

lemma max_vars_inline_call: "max_vars (inline_call e' e) ≤ max_vars e + max_vars e'"
  and max_varss_inline_calls: "max_varss (inline_calls e' es) ≤ max_varss es + max_vars e'"
by(induct e and es rule: call1.induct calls1.induct) auto

lemmas inline_call_max_vars1 = max_vars_inline_call
lemmas inline_calls_max_varss1 = max_varss_inline_calls

end