Theory IRNodeHierarchy

subsection ‹IR Graph Node Hierarchy›

theory IRNodeHierarchy
imports IRNodes
begin

text ‹
It is helpful to introduce a node hierarchy into our formalization.
Often the GraalVM compiler relies on explicit type checks to determine
which operations to perform on a given node, we try to mimic the same
functionality by using a suite of predicate functions over the IRNode
class to determine inheritance.

As one would expect, the function is<ClassName>Type will be true if
the node parameter is a subclass of the ClassName within the GraalVM compiler.

These functions have been automatically generated from the compiler.
›

(* Datatype with no parameters don't generate selectors *)
fun is_EndNode :: "IRNode ⇒ bool" where
  "is_EndNode EndNode = True" |
  "is_EndNode _ = False"

(* nodeout: isabelle-subclass *)
fun is_VirtualState :: "IRNode ⇒ bool" where
  "is_VirtualState n = ((is_FrameState n))"

fun is_BinaryArithmeticNode :: "IRNode ⇒ bool" where
  "is_BinaryArithmeticNode n = ((is_AddNode n) ∨ (is_AndNode n) ∨ (is_MulNode n) ∨ (is_OrNode n) ∨ (is_SubNode n) ∨ (is_XorNode n) ∨ (is_IntegerNormalizeCompareNode n) ∨ (is_IntegerMulHighNode n))"

fun is_ShiftNode :: "IRNode ⇒ bool" where
  "is_ShiftNode n = ((is_LeftShiftNode n) ∨ (is_RightShiftNode n) ∨ (is_UnsignedRightShiftNode n))"

fun is_BinaryNode :: "IRNode ⇒ bool" where
  "is_BinaryNode n = ((is_BinaryArithmeticNode n) ∨ (is_ShiftNode n))"

fun is_AbstractLocalNode :: "IRNode ⇒ bool" where
  "is_AbstractLocalNode n = ((is_ParameterNode n))"

fun is_IntegerConvertNode :: "IRNode ⇒ bool" where
  "is_IntegerConvertNode n = ((is_NarrowNode n) ∨ (is_SignExtendNode n) ∨ (is_ZeroExtendNode n))"

fun is_UnaryArithmeticNode :: "IRNode ⇒ bool" where
  "is_UnaryArithmeticNode n = ((is_AbsNode n) ∨ (is_NegateNode n) ∨ (is_NotNode n) ∨ (is_BitCountNode n) ∨ (is_ReverseBytesNode n))"

fun is_UnaryNode :: "IRNode ⇒ bool" where
  "is_UnaryNode n = ((is_IntegerConvertNode n) ∨ (is_UnaryArithmeticNode n))"

fun is_PhiNode :: "IRNode ⇒ bool" where
  "is_PhiNode n = ((is_ValuePhiNode n))"

fun is_FloatingGuardedNode :: "IRNode ⇒ bool" where
  "is_FloatingGuardedNode n = ((is_PiNode n))"

fun is_UnaryOpLogicNode :: "IRNode ⇒ bool" where
  "is_UnaryOpLogicNode n = ((is_IsNullNode n))"

fun is_IntegerLowerThanNode :: "IRNode ⇒ bool" where
  "is_IntegerLowerThanNode n = ((is_IntegerBelowNode n) ∨ (is_IntegerLessThanNode n))"

fun is_CompareNode :: "IRNode ⇒ bool" where
  "is_CompareNode n = ((is_IntegerEqualsNode n) ∨ (is_IntegerLowerThanNode n))"

fun is_BinaryOpLogicNode :: "IRNode ⇒ bool" where
  "is_BinaryOpLogicNode n = ((is_CompareNode n) ∨ (is_IntegerTestNode n))"

fun is_LogicNode :: "IRNode ⇒ bool" where
  "is_LogicNode n = ((is_BinaryOpLogicNode n) ∨ (is_LogicNegationNode n) ∨ (is_ShortCircuitOrNode n) ∨ (is_UnaryOpLogicNode n))"

fun is_ProxyNode :: "IRNode ⇒ bool" where
  "is_ProxyNode n = ((is_ValueProxyNode n))"

fun is_FloatingNode :: "IRNode ⇒ bool" where
  "is_FloatingNode n = ((is_AbstractLocalNode n) ∨ (is_BinaryNode n) ∨ (is_ConditionalNode n) ∨ (is_ConstantNode n) ∨ (is_FloatingGuardedNode n) ∨ (is_LogicNode n) ∨ (is_PhiNode n) ∨ (is_ProxyNode n) ∨ (is_UnaryNode n))"

fun is_AccessFieldNode :: "IRNode ⇒ bool" where
  "is_AccessFieldNode n = ((is_LoadFieldNode n) ∨ (is_StoreFieldNode n))"

fun is_AbstractNewArrayNode :: "IRNode ⇒ bool" where
  "is_AbstractNewArrayNode n = ((is_DynamicNewArrayNode n) ∨ (is_NewArrayNode n))"

fun is_AbstractNewObjectNode :: "IRNode ⇒ bool" where
  "is_AbstractNewObjectNode n = ((is_AbstractNewArrayNode n) ∨ (is_NewInstanceNode n))"

fun is_AbstractFixedGuardNode :: "IRNode ⇒ bool" where
  "is_AbstractFixedGuardNode n = (is_FixedGuardNode n)"

fun is_IntegerDivRemNode :: "IRNode ⇒ bool" where
  "is_IntegerDivRemNode n = ((is_SignedDivNode n) ∨ (is_SignedRemNode n))"

fun is_FixedBinaryNode :: "IRNode ⇒ bool" where
  "is_FixedBinaryNode n = (is_IntegerDivRemNode n)"

fun is_DeoptimizingFixedWithNextNode :: "IRNode ⇒ bool" where
  "is_DeoptimizingFixedWithNextNode n = ((is_AbstractNewObjectNode n) ∨ (is_FixedBinaryNode n) ∨ (is_AbstractFixedGuardNode n))"

fun is_AbstractMemoryCheckpoint :: "IRNode ⇒ bool" where
  "is_AbstractMemoryCheckpoint n = ((is_BytecodeExceptionNode n) ∨ (is_InvokeNode n))"

fun is_AbstractStateSplit :: "IRNode ⇒ bool" where
  "is_AbstractStateSplit n = ((is_AbstractMemoryCheckpoint n))"

fun is_AbstractMergeNode :: "IRNode ⇒ bool" where
  "is_AbstractMergeNode n = ((is_LoopBeginNode n) ∨ (is_MergeNode n))"

fun is_BeginStateSplitNode :: "IRNode ⇒ bool" where
  "is_BeginStateSplitNode n = ((is_AbstractMergeNode n) ∨ (is_ExceptionObjectNode n) ∨ (is_LoopExitNode n) ∨ (is_StartNode n))"

fun is_AbstractBeginNode :: "IRNode ⇒ bool" where
  "is_AbstractBeginNode n = ((is_BeginNode n) ∨ (is_BeginStateSplitNode n) ∨ (is_KillingBeginNode n))"

fun is_AccessArrayNode :: "IRNode ⇒ bool" where
  "is_AccessArrayNode n = ((is_LoadIndexedNode n) ∨ (is_StoreIndexedNode n))"

fun is_FixedWithNextNode :: "IRNode ⇒ bool" where
  "is_FixedWithNextNode n = ((is_AbstractBeginNode n) ∨ (is_AbstractStateSplit n) ∨ (is_AccessFieldNode n) ∨ (is_DeoptimizingFixedWithNextNode n) ∨ (is_ControlFlowAnchorNode n) ∨ (is_ArrayLengthNode n) ∨ (is_AccessArrayNode n))"

fun is_WithExceptionNode :: "IRNode ⇒ bool" where
  "is_WithExceptionNode n = ((is_InvokeWithExceptionNode n))"

fun is_ControlSplitNode :: "IRNode ⇒ bool" where
  "is_ControlSplitNode n = ((is_IfNode n) ∨ (is_WithExceptionNode n))"

fun is_ControlSinkNode :: "IRNode ⇒ bool" where
  "is_ControlSinkNode n = ((is_ReturnNode n) ∨ (is_UnwindNode n))"

fun is_AbstractEndNode :: "IRNode ⇒ bool" where
  "is_AbstractEndNode n = ((is_EndNode n) ∨ (is_LoopEndNode n))"

fun is_FixedNode :: "IRNode ⇒ bool" where
  "is_FixedNode n = ((is_AbstractEndNode n) ∨ (is_ControlSinkNode n) ∨ (is_ControlSplitNode n) ∨ (is_FixedWithNextNode n))"

fun is_CallTargetNode :: "IRNode ⇒ bool" where
  "is_CallTargetNode n = ((is_MethodCallTargetNode n))"

fun is_ValueNode :: "IRNode ⇒ bool" where
  "is_ValueNode n = ((is_CallTargetNode n) ∨ (is_FixedNode n) ∨ (is_FloatingNode n))"

fun is_Node :: "IRNode ⇒ bool" where
  "is_Node n = ((is_ValueNode n) ∨ (is_VirtualState n))"

fun is_MemoryKill :: "IRNode ⇒ bool" where
  "is_MemoryKill n = ((is_AbstractMemoryCheckpoint n))"

fun is_NarrowableArithmeticNode :: "IRNode ⇒ bool" where
  "is_NarrowableArithmeticNode n = ((is_AbsNode n) ∨ (is_AddNode n) ∨ (is_AndNode n) ∨ (is_MulNode n) ∨ (is_NegateNode n) ∨ (is_NotNode n) ∨ (is_OrNode n) ∨ (is_ShiftNode n) ∨ (is_SubNode n) ∨ (is_XorNode n))"

fun is_AnchoringNode :: "IRNode ⇒ bool" where
  "is_AnchoringNode n = ((is_AbstractBeginNode n))"

fun is_DeoptBefore :: "IRNode ⇒ bool" where
  "is_DeoptBefore n = ((is_DeoptimizingFixedWithNextNode n))"

fun is_IndirectCanonicalization :: "IRNode ⇒ bool" where
  "is_IndirectCanonicalization n = ((is_LogicNode n))"

fun is_IterableNodeType :: "IRNode ⇒ bool" where
  "is_IterableNodeType n = ((is_AbstractBeginNode n) ∨ (is_AbstractMergeNode n) ∨ (is_FrameState n) ∨ (is_IfNode n) ∨ (is_IntegerDivRemNode n) ∨ (is_InvokeWithExceptionNode n) ∨ (is_LoopBeginNode n) ∨ (is_LoopExitNode n) ∨ (is_MethodCallTargetNode n) ∨ (is_ParameterNode n) ∨ (is_ReturnNode n) ∨ (is_ShortCircuitOrNode n))"

fun is_Invoke :: "IRNode ⇒ bool" where
  "is_Invoke n = ((is_InvokeNode n) ∨ (is_InvokeWithExceptionNode n))"

fun is_Proxy :: "IRNode ⇒ bool" where
  "is_Proxy n = ((is_ProxyNode n))"

fun is_ValueProxy :: "IRNode ⇒ bool" where
  "is_ValueProxy n = ((is_PiNode n) ∨ (is_ValueProxyNode n))"

fun is_ValueNodeInterface :: "IRNode ⇒ bool" where
  "is_ValueNodeInterface n = ((is_ValueNode n))"

fun is_ArrayLengthProvider :: "IRNode ⇒ bool" where
  "is_ArrayLengthProvider n = ((is_AbstractNewArrayNode n) ∨ (is_ConstantNode n))"

fun is_StampInverter :: "IRNode ⇒ bool" where
  "is_StampInverter n = ((is_IntegerConvertNode n) ∨ (is_NegateNode n) ∨ (is_NotNode n))"

fun is_GuardingNode :: "IRNode ⇒ bool" where
  "is_GuardingNode n = ((is_AbstractBeginNode n))"

fun is_SingleMemoryKill :: "IRNode ⇒ bool" where
  "is_SingleMemoryKill n = ((is_BytecodeExceptionNode n) ∨ (is_ExceptionObjectNode n) ∨ (is_InvokeNode n) ∨ (is_InvokeWithExceptionNode n) ∨ (is_KillingBeginNode n) ∨ (is_StartNode n))"

fun is_LIRLowerable :: "IRNode ⇒ bool" where
  "is_LIRLowerable n = ((is_AbstractBeginNode n) ∨ (is_AbstractEndNode n) ∨ (is_AbstractMergeNode n) ∨ (is_BinaryOpLogicNode n) ∨ (is_CallTargetNode n) ∨ (is_ConditionalNode n) ∨ (is_ConstantNode n) ∨ (is_IfNode n) ∨ (is_InvokeNode n) ∨ (is_InvokeWithExceptionNode n) ∨ (is_IsNullNode n) ∨ (is_LoopBeginNode n) ∨ (is_PiNode n) ∨ (is_ReturnNode n) ∨ (is_SignedDivNode n) ∨ (is_SignedRemNode n) ∨ (is_UnaryOpLogicNode n) ∨ (is_UnwindNode n))"

fun is_GuardedNode :: "IRNode ⇒ bool" where
  "is_GuardedNode n = ((is_FloatingGuardedNode n))"

fun is_ArithmeticLIRLowerable :: "IRNode ⇒ bool" where
  "is_ArithmeticLIRLowerable n = ((is_AbsNode n) ∨ (is_BinaryArithmeticNode n) ∨ (is_IntegerConvertNode n) ∨ (is_NotNode n) ∨ (is_ShiftNode n) ∨ (is_UnaryArithmeticNode n))"

fun is_SwitchFoldable :: "IRNode ⇒ bool" where
  "is_SwitchFoldable n = ((is_IfNode n))"

fun is_VirtualizableAllocation :: "IRNode ⇒ bool" where
  "is_VirtualizableAllocation n = ((is_NewArrayNode n) ∨ (is_NewInstanceNode n))"

fun is_Unary :: "IRNode ⇒ bool" where
  "is_Unary n = ((is_LoadFieldNode n) ∨ (is_LogicNegationNode n) ∨ (is_UnaryNode n) ∨ (is_UnaryOpLogicNode n))"

fun is_FixedNodeInterface :: "IRNode ⇒ bool" where
  "is_FixedNodeInterface n = ((is_FixedNode n))"

fun is_BinaryCommutative :: "IRNode ⇒ bool" where
  "is_BinaryCommutative n = ((is_AddNode n) ∨ (is_AndNode n) ∨ (is_IntegerEqualsNode n) ∨ (is_MulNode n) ∨ (is_OrNode n) ∨ (is_XorNode n))"

fun is_Canonicalizable :: "IRNode ⇒ bool" where
  "is_Canonicalizable n = ((is_BytecodeExceptionNode n) ∨ (is_ConditionalNode n) ∨ (is_DynamicNewArrayNode n) ∨ (is_PhiNode n) ∨ (is_PiNode n) ∨ (is_ProxyNode n) ∨ (is_StoreFieldNode n) ∨ (is_ValueProxyNode n))"

fun is_UncheckedInterfaceProvider :: "IRNode ⇒ bool" where
  "is_UncheckedInterfaceProvider n = ((is_InvokeNode n) ∨ (is_InvokeWithExceptionNode n) ∨ (is_LoadFieldNode n) ∨ (is_ParameterNode n))"

fun is_Binary :: "IRNode ⇒ bool" where
  "is_Binary n = ((is_BinaryArithmeticNode n) ∨ (is_BinaryNode n) ∨ (is_BinaryOpLogicNode n) ∨ (is_CompareNode n) ∨ (is_FixedBinaryNode n) ∨ (is_ShortCircuitOrNode n))"

fun is_ArithmeticOperation :: "IRNode ⇒ bool" where
  "is_ArithmeticOperation n = ((is_BinaryArithmeticNode n) ∨ (is_IntegerConvertNode n) ∨ (is_ShiftNode n) ∨ (is_UnaryArithmeticNode n))"

fun is_ValueNumberable :: "IRNode ⇒ bool" where
  "is_ValueNumberable n = ((is_FloatingNode n) ∨ (is_ProxyNode n))"

fun is_Lowerable :: "IRNode ⇒ bool" where
  "is_Lowerable n = ((is_AbstractNewObjectNode n) ∨ (is_AccessFieldNode n) ∨ (is_BytecodeExceptionNode n) ∨ (is_ExceptionObjectNode n) ∨ (is_IntegerDivRemNode n) ∨ (is_UnwindNode n))"

fun is_Virtualizable :: "IRNode ⇒ bool" where
  "is_Virtualizable n = ((is_IsNullNode n) ∨ (is_LoadFieldNode n) ∨ (is_PiNode n) ∨ (is_StoreFieldNode n) ∨ (is_ValueProxyNode n))"

fun is_Simplifiable :: "IRNode ⇒ bool" where
  "is_Simplifiable n = ((is_AbstractMergeNode n) ∨ (is_BeginNode n) ∨ (is_IfNode n) ∨ (is_LoopExitNode n) ∨ (is_MethodCallTargetNode n) ∨ (is_NewArrayNode n))"

fun is_StateSplit :: "IRNode ⇒ bool" where
  "is_StateSplit n = ((is_AbstractStateSplit n) ∨ (is_BeginStateSplitNode n) ∨ (is_StoreFieldNode n))"

fun is_ConvertNode :: "IRNode ⇒ bool" where
  "is_ConvertNode n = ((is_IntegerConvertNode n))"
(* nodeout *)

fun is_sequential_node :: "IRNode ⇒ bool" where
  "is_sequential_node (StartNode _ _) = True" |
  "is_sequential_node (BeginNode _) = True" |
  "is_sequential_node (KillingBeginNode _) = True" |
  "is_sequential_node (LoopBeginNode _ _ _ _) = True" |
  "is_sequential_node (LoopExitNode _ _ _) = True" |
  "is_sequential_node (MergeNode _ _ _) = True" |
  "is_sequential_node (RefNode _) = True" |
  "is_sequential_node (ControlFlowAnchorNode _) = True" |
  "is_sequential_node _ = False"

text ‹
The following convenience function is useful in determining if
two IRNodes are of the same type irregardless of their edges.
It will return true if both the node parameters are the same node class.
›

(* nodeout: isabelle-compare-type *)
fun is_same_ir_node_type :: "IRNode ⇒ IRNode ⇒ bool" where
"is_same_ir_node_type n1 n2 = (
  ((is_AbsNode n1) ∧ (is_AbsNode n2)) ∨
  ((is_AddNode n1) ∧ (is_AddNode n2)) ∨
  ((is_AndNode n1) ∧ (is_AndNode n2)) ∨
  ((is_BeginNode n1) ∧ (is_BeginNode n2)) ∨
  ((is_BytecodeExceptionNode n1) ∧ (is_BytecodeExceptionNode n2)) ∨
  ((is_ConditionalNode n1) ∧ (is_ConditionalNode n2)) ∨
  ((is_ConstantNode n1) ∧ (is_ConstantNode n2)) ∨
  ((is_DynamicNewArrayNode n1) ∧ (is_DynamicNewArrayNode n2)) ∨
  ((is_EndNode n1) ∧ (is_EndNode n2)) ∨
  ((is_ExceptionObjectNode n1) ∧ (is_ExceptionObjectNode n2)) ∨
  ((is_FrameState n1) ∧ (is_FrameState n2)) ∨
  ((is_IfNode n1) ∧ (is_IfNode n2)) ∨
  ((is_IntegerBelowNode n1) ∧ (is_IntegerBelowNode n2)) ∨
  ((is_IntegerEqualsNode n1) ∧ (is_IntegerEqualsNode n2)) ∨
  ((is_IntegerLessThanNode n1) ∧ (is_IntegerLessThanNode n2)) ∨
  ((is_InvokeNode n1) ∧ (is_InvokeNode n2)) ∨
  ((is_InvokeWithExceptionNode n1) ∧ (is_InvokeWithExceptionNode n2)) ∨
  ((is_IsNullNode n1) ∧ (is_IsNullNode n2)) ∨
  ((is_KillingBeginNode n1) ∧ (is_KillingBeginNode n2)) ∨
  ((is_LeftShiftNode n1) ∧ (is_LeftShiftNode n2)) ∨
  ((is_LoadFieldNode n1) ∧ (is_LoadFieldNode n2)) ∨
  ((is_LogicNegationNode n1) ∧ (is_LogicNegationNode n2)) ∨
  ((is_LoopBeginNode n1) ∧ (is_LoopBeginNode n2)) ∨
  ((is_LoopEndNode n1) ∧ (is_LoopEndNode n2)) ∨
  ((is_LoopExitNode n1) ∧ (is_LoopExitNode n2)) ∨
  ((is_MergeNode n1) ∧ (is_MergeNode n2)) ∨
  ((is_MethodCallTargetNode n1) ∧ (is_MethodCallTargetNode n2)) ∨
  ((is_MulNode n1) ∧ (is_MulNode n2)) ∨
  ((is_NarrowNode n1) ∧ (is_NarrowNode n2)) ∨
  ((is_NegateNode n1) ∧ (is_NegateNode n2)) ∨
  ((is_NewArrayNode n1) ∧ (is_NewArrayNode n2)) ∨
  ((is_NewInstanceNode n1) ∧ (is_NewInstanceNode n2)) ∨
  ((is_NotNode n1) ∧ (is_NotNode n2)) ∨
  ((is_OrNode n1) ∧ (is_OrNode n2)) ∨
  ((is_ParameterNode n1) ∧ (is_ParameterNode n2)) ∨
  ((is_PiNode n1) ∧ (is_PiNode n2)) ∨
  ((is_ReturnNode n1) ∧ (is_ReturnNode n2)) ∨
  ((is_RightShiftNode n1) ∧ (is_RightShiftNode n2)) ∨
  ((is_ShortCircuitOrNode n1) ∧ (is_ShortCircuitOrNode n2)) ∨
  ((is_SignedDivNode n1) ∧ (is_SignedDivNode n2)) ∨
  ((is_SignedFloatingIntegerDivNode n1) ∧ (is_SignedFloatingIntegerDivNode n2)) ∨
  ((is_SignedFloatingIntegerRemNode n1) ∧ (is_SignedFloatingIntegerRemNode n2)) ∨
  ((is_SignedRemNode n1) ∧ (is_SignedRemNode n2)) ∨
  ((is_SignExtendNode n1) ∧ (is_SignExtendNode n2)) ∨
  ((is_StartNode n1) ∧ (is_StartNode n2)) ∨
  ((is_StoreFieldNode n1) ∧ (is_StoreFieldNode n2)) ∨
  ((is_SubNode n1) ∧ (is_SubNode n2)) ∨
  ((is_UnsignedRightShiftNode n1) ∧ (is_UnsignedRightShiftNode n2)) ∨
  ((is_UnwindNode n1) ∧ (is_UnwindNode n2)) ∨
  ((is_ValuePhiNode n1) ∧ (is_ValuePhiNode n2)) ∨
  ((is_ValueProxyNode n1) ∧ (is_ValueProxyNode n2)) ∨
  ((is_XorNode n1) ∧ (is_XorNode n2)) ∨
  ((is_ZeroExtendNode n1) ∧ (is_ZeroExtendNode n2)))"

end