Skip to content

Commit

Permalink
Collapse unrep definition
Browse files Browse the repository at this point in the history
  • Loading branch information
@BraeWebb
BraeWebb committed Jan 21, 2024
1 parent fa8fff6 commit 94af1a8
Show file tree
Hide file tree
Showing 4 changed files with 200 additions and 338 deletions.
4 changes: 3 additions & 1 deletion Papers/Semantics/SemanticsSnippets.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,8 @@ theory SemanticsSnippets
Semantics.IRStepObj Semantics.Form Proofs.Stuttering Snippets.Snipping
begin

declare [[show_types=false]]

(*notation (latex)
NoNode ("\<epsilon>")
*)
Expand Down Expand Up @@ -287,4 +289,4 @@ notation (latex output)
notation (latex output)
IntVal ("IntVal (2 _)")

end
end
38 changes: 14 additions & 24 deletions Semantics/IRStepObj.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,10 +142,8 @@ inductive step :: "IRGraph \<Rightarrow> Params \<Rightarrow> (ID \<times> MapSt
"\<lbrakk>(kind g nid) = (FixedGuardNode cond before next);
[g, m, p] \<turnstile> cond \<mapsto> val;
\<not>(val_to_bool val);
nid' = next\<rbrakk>
\<Longrightarrow> g, p \<turnstile> (nid, m, h) \<rightarrow> (nid', m, h)" |
\<not>(val_to_bool val)\<rbrakk>
\<Longrightarrow> g, p \<turnstile> (nid, m, h) \<rightarrow> (next, m, h)" |

BytecodeExceptionNode:
"\<lbrakk>(kind g nid) = (BytecodeExceptionNode args st nid');
Expand Down Expand Up @@ -227,30 +225,26 @@ inductive step :: "IRGraph \<Rightarrow> Params \<Rightarrow> (ID \<times> MapSt
LoadFieldNode:
"\<lbrakk>kind g nid = (LoadFieldNode nid f (Some obj) nid');
[g, m, p] \<turnstile> obj \<mapsto> ObjRef ref;
h_load_field f ref h = v;
m' = m(nid := v)\<rbrakk>
m' = m(nid := h_load_field f ref h)\<rbrakk>
\<Longrightarrow> g, p \<turnstile> (nid, m, h) \<rightarrow> (nid', m', h)" |

SignedDivNode:
"\<lbrakk>kind g nid = (SignedDivNode nid x y zero sb nxt);
"\<lbrakk>kind g nid = (SignedDivNode nid x y zero sb next);
[g, m, p] \<turnstile> x \<mapsto> v1;
[g, m, p] \<turnstile> y \<mapsto> v2;
v = (intval_div v1 v2);
m' = m(nid := v)\<rbrakk>
\<Longrightarrow> g, p \<turnstile> (nid, m, h) \<rightarrow> (nxt, m', h)" |
m' = m(nid := intval_div v1 v2)\<rbrakk>
\<Longrightarrow> g, p \<turnstile> (nid, m, h) \<rightarrow> (next, m', h)" |

SignedRemNode:
"\<lbrakk>kind g nid = (SignedRemNode nid x y zero sb nxt);
"\<lbrakk>kind g nid = (SignedRemNode nid x y zero sb next);
[g, m, p] \<turnstile> x \<mapsto> v1;
[g, m, p] \<turnstile> y \<mapsto> v2;
v = (intval_mod v1 v2);
m' = m(nid := v)\<rbrakk>
\<Longrightarrow> g, p \<turnstile> (nid, m, h) \<rightarrow> (nxt, m', h)" |
m' = m(nid := intval_mod v1 v2)\<rbrakk>
\<Longrightarrow> g, p \<turnstile> (nid, m, h) \<rightarrow> (next, m', h)" |

StaticLoadFieldNode:
"\<lbrakk>kind g nid = (LoadFieldNode nid f None nid');
h_load_field f None h = v;
m' = m(nid := v)\<rbrakk>
m' = m(nid := h_load_field f None h)\<rbrakk>
\<Longrightarrow> g, p \<turnstile> (nid, m, h) \<rightarrow> (nid', m', h)" |

StoreFieldNode:
Expand Down Expand Up @@ -316,17 +310,15 @@ inductive step_top :: "System \<Rightarrow> (IRGraph \<times> ID \<times> MapSta
kind g callTarget = (MethodCallTargetNode targetMethod actuals invoke_kind);
\<not>(hasReceiver invoke_kind);
Some targetGraph = (dynamic_lookup S ''None'' targetMethod []);
g \<turnstile> actuals \<simeq>\<^sub>L argsE;
[m, p] \<turnstile> argsE \<mapsto>\<^sub>L p'\<rbrakk>
[g, m, p] \<turnstile> actuals \<longmapsto> p'\<rbrakk>
\<Longrightarrow> (S) \<turnstile> ((g,nid,m,p)#stk, h) \<longrightarrow> ((targetGraph,0,new_map_state,p')#(g,nid,m,p)#stk, h)" |

InvokeNodeStep:
"\<lbrakk>is_Invoke (kind g nid);
callTarget = ir_callTarget (kind g nid);
kind g callTarget = (MethodCallTargetNode targetMethod arguments invoke_kind);
hasReceiver invoke_kind;
g \<turnstile> arguments \<simeq>\<^sub>L argsE;
[m, p] \<turnstile> argsE \<mapsto>\<^sub>L p';
[g, m, p] \<turnstile> arguments \<longmapsto> p';
ObjRef self = hd p';
ObjStr cname = (h_load_field ''class'' self h);
S = (P,cl);
Expand All @@ -336,8 +328,7 @@ inductive step_top :: "System \<Rightarrow> (IRGraph \<times> ID \<times> MapSta
(* TODO this produces two parse trees after importing Class *)
ReturnNode:
"\<lbrakk>kind g nid = (ReturnNode (Some expr) _);
g \<turnstile> expr \<simeq> e;
[m, p] \<turnstile> e \<mapsto> v;
[g, m, p] \<turnstile> expr \<mapsto> v;
m'\<^sub>c = m\<^sub>c(nid\<^sub>c := v);
nid'\<^sub>c = (successors_of (kind g\<^sub>c nid\<^sub>c))!0\<rbrakk>
Expand All @@ -354,8 +345,7 @@ inductive step_top :: "System \<Rightarrow> (IRGraph \<times> ID \<times> MapSta
UnwindNode:
"\<lbrakk>kind g nid = (UnwindNode exception);
g \<turnstile> exception \<simeq> exceptionE;
[m, p] \<turnstile> exceptionE \<mapsto> e;
[g, m, p] \<turnstile> exception \<mapsto> e;
kind g\<^sub>c nid\<^sub>c = (InvokeWithExceptionNode _ _ _ _ _ _ exEdge);
Expand Down
131 changes: 53 additions & 78 deletions Semantics/TreeToGraph.thy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -408,6 +408,18 @@ export_code get_fresh_id
value "get_fresh_id eg2_sq"
value "get_fresh_id (add_node 6 (ParameterNode 2, default_stamp) eg2_sq)"

inductive unique :: "IRGraph \<Rightarrow> (IRNode \<times> Stamp) \<Rightarrow> (IRGraph \<times> ID) \<Rightarrow> bool" where
Exists:
"\<lbrakk>find_node_and_stamp g node = Some n\<rbrakk>
\<Longrightarrow> unique g node (g, n)" |
New:
"\<lbrakk>find_node_and_stamp g node = None;
n = get_fresh_id g;
g' = add_node n node g\<rbrakk>
\<Longrightarrow> unique g node (g', n)"

code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as uniqueE) unique .

(* Second version of tree insertion into graph:
g \<triangleleft> expr \<leadsto> (g',n) re-inserts expr into g and returns the new root n.
Expand All @@ -416,75 +428,36 @@ value "get_fresh_id (add_node 6 (ParameterNode 2, default_stamp) eg2_sq)"
*)
inductive
unrep :: "IRGraph \<Rightarrow> IRExpr \<Rightarrow> (IRGraph \<times> ID) \<Rightarrow> bool" ("_ \<oplus> _ \<leadsto> _" 55)
where

ConstantNodeSame:
"\<lbrakk>find_node_and_stamp g (ConstantNode c, constantAsStamp c) = Some n\<rbrakk>
\<Longrightarrow> g \<oplus> (ConstantExpr c) \<leadsto> (g, n)" |

ConstantNodeNew:
"\<lbrakk>find_node_and_stamp g (ConstantNode c, constantAsStamp c) = None;
n = get_fresh_id g;
g' = add_node n (ConstantNode c, constantAsStamp c) g \<rbrakk>
\<Longrightarrow> g \<oplus> (ConstantExpr c) \<leadsto> (g', n)" |

ParameterNodeSame:
"\<lbrakk>find_node_and_stamp g (ParameterNode i, s) = Some n\<rbrakk>
\<Longrightarrow> g \<oplus> (ParameterExpr i s) \<leadsto> (g, n)" |
where

ParameterNodeNew:
"\<lbrakk>find_node_and_stamp g (ParameterNode i, s) = None;
n = get_fresh_id g;
g' = add_node n (ParameterNode i, s) g\<rbrakk>
\<Longrightarrow> g \<oplus> (ParameterExpr i s) \<leadsto> (g', n)" |

ConditionalNodeSame:
"\<lbrakk>find_node_and_stamp g4 (ConditionalNode c t f, s') = Some n;
g \<oplus> ce \<leadsto> (g2, c);
g2 \<oplus> te \<leadsto> (g3, t);
g3 \<oplus> fe \<leadsto> (g4, f);
s' = meet (stamp g4 t) (stamp g4 f)\<rbrakk>
\<Longrightarrow> g \<oplus> (ConditionalExpr ce te fe) \<leadsto> (g4, n)" |

ConditionalNodeNew:
"\<lbrakk>find_node_and_stamp g4 (ConditionalNode c t f, s') = None;
g \<oplus> ce \<leadsto> (g2, c);
g2 \<oplus> te \<leadsto> (g3, t);
g3 \<oplus> fe \<leadsto> (g4, f);
s' = meet (stamp g4 t) (stamp g4 f);
n = get_fresh_id g4;
g' = add_node n (ConditionalNode c t f, s') g4\<rbrakk>
\<Longrightarrow> g \<oplus> (ConditionalExpr ce te fe) \<leadsto> (g', n)" |

UnaryNodeSame:
"\<lbrakk>find_node_and_stamp g' (unary_node op x, s') = Some n;
g \<oplus> xe \<leadsto> (g', x);
s' = stamp_unary op (stamp g' x)\<rbrakk>
\<Longrightarrow> g \<oplus> (UnaryExpr op xe) \<leadsto> (g', n)" |

UnaryNodeNew:
"\<lbrakk>find_node_and_stamp g' (unary_node op x, s') = None;
g \<oplus> xe \<leadsto> (g', x);
s' = stamp_unary op (stamp g' x);
n = get_fresh_id g';
g'' = add_node n (unary_node op x, s') g'\<rbrakk>
\<Longrightarrow> g \<oplus> (UnaryExpr op xe) \<leadsto> (g'', n)" |

BinaryNodeSame:
"\<lbrakk>find_node_and_stamp g3 (bin_node op x y, s') = Some n;
g \<oplus> xe \<leadsto> (g2, x);
g2 \<oplus> ye \<leadsto> (g3, y);
s' = stamp_binary op (stamp g3 x) (stamp g3 y)\<rbrakk>
\<Longrightarrow> g \<oplus> (BinaryExpr op xe ye) \<leadsto> (g3, n)" |

BinaryNodeNew:
"\<lbrakk>find_node_and_stamp g3 (bin_node op x y, s') = None;
g \<oplus> xe \<leadsto> (g2, x);
g2 \<oplus> ye \<leadsto> (g3, y);
s' = stamp_binary op (stamp g3 x) (stamp g3 y);
n = get_fresh_id g3;
g' = add_node n (bin_node op x y, s') g3\<rbrakk>
\<Longrightarrow> g \<oplus> (BinaryExpr op xe ye) \<leadsto> (g', n)" |
UnrepConstantNode:
"\<lbrakk>unique g (ConstantNode c, constantAsStamp c) (g\<^sub>1, n)\<rbrakk>
\<Longrightarrow> g \<oplus> (ConstantExpr c) \<leadsto> (g\<^sub>1, n)" |

UnrepParameterNode:
"\<lbrakk>unique g (ParameterNode i, s) (g\<^sub>1, n)\<rbrakk>
\<Longrightarrow> g \<oplus> (ParameterExpr i s) \<leadsto> (g\<^sub>1, n)" |

UnrepConditionalNode:
"\<lbrakk>g \<oplus> ce \<leadsto> (g\<^sub>1, c);
g\<^sub>1 \<oplus> te \<leadsto> (g\<^sub>2, t);
g\<^sub>2 \<oplus> fe \<leadsto> (g\<^sub>3, f);
s' = meet (stamp g\<^sub>3 t) (stamp g\<^sub>3 f);
unique g\<^sub>3 (ConditionalNode c t f, s') (g\<^sub>4, n)\<rbrakk>
\<Longrightarrow> g \<oplus> (ConditionalExpr ce te fe) \<leadsto> (g\<^sub>4, n)" |

UnrepUnaryNode:
"\<lbrakk>g \<oplus> xe \<leadsto> (g\<^sub>1, x);
s' = stamp_unary op (stamp g\<^sub>1 x);
unique g\<^sub>1 (unary_node op x, s') (g\<^sub>2, n)\<rbrakk>
\<Longrightarrow> g \<oplus> (UnaryExpr op xe) \<leadsto> (g\<^sub>2, n)" |

UnrepBinaryNode:
"\<lbrakk>g \<oplus> xe \<leadsto> (g\<^sub>1, x);
g\<^sub>1 \<oplus> ye \<leadsto> (g\<^sub>2, y);
s' = stamp_binary op (stamp g\<^sub>2 x) (stamp g\<^sub>2 y);
unique g\<^sub>2 (bin_node op x y, s') (g\<^sub>3, n)\<rbrakk>
\<Longrightarrow> g \<oplus> (BinaryExpr op xe ye) \<leadsto> (g\<^sub>3, n)" |

AllLeafNodes:
"\<lbrakk>stamp g n = s;
Expand All @@ -507,18 +480,20 @@ code_pred (modes: i \<Rightarrow> i \<Rightarrow> o \<Rightarrow> bool as unrepE
[show_steps,show_mode_inference,show_intermediate_results]
*) unrep .

text_raw \<open>\Snip{unique}%
\begin{center}
@{thm[mode=Rule] unique.Exists [no_vars]}\\[8px]
@{thm[mode=Rule] unique.New [no_vars]}\\[8px]
\end{center}
\EndSnip\<close>

text_raw \<open>\Snip{unrepRules}%
\begin{center}
@{thm[mode=Rule] unrep.ConstantNodeSame [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.ConstantNodeNew [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.ParameterNodeSame [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.ParameterNodeNew [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.ConditionalNodeSame [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.ConditionalNodeNew [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.BinaryNodeSame [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.BinaryNodeNew [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.UnaryNodeSame [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.UnaryNodeNew [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.UnrepConstantNode [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.UnrepParameterNode [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.UnrepConditionalNode [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.UnrepBinaryNode [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.UnrepUnaryNode [no_vars]}\\[8px]
@{thm[mode=Rule] unrep.AllLeafNodes [no_vars]}\\[8px]
\end{center}
\EndSnip\<close>
Expand Down
Loading

0 comments on commit 94af1a8

Please sign in to comment.