# Theory J1State

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

section ‹The intermediate language J1›

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

type_synonym

type_synonym

type_synonym

translations

type_synonym

type_synonym

type_synonym

(* 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;
end
›

(* 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
›

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"
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)"

― ‹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"
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)"

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)"

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

by(induct es, auto)

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

by(induct es) auto

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'"