Reachability logic, formalized

[dmlloyd]

As a part of the work being done in #1059 it would be useful to formalize the existing reachability logic into a series of pseudo-Prolog-style rules to describe the conditions under which a fact can become known, because the Facts API establishes logical relationships in a way that is structurally similar to this. However, since I have not actually touched Prolog syntax in many years, I've modified it for simplicity (and so I'm off the hook for any incorrectness).

The rule syntax used below is as follows:

• a :- b - a is true when b is true.
• a :- b,c - a is true when b and c are true (conjunction).
• a :- b;c - a is true when b or c or both b and c are true (disjunction).

Some basic functors are assumed:

• Encloses(t, m) is true when type t contains a member m.
• IsSuperClass(x, y) is true when class x is a superclass of class y.
• IsArray(x, y) is true when class x is an array of type y.
• IsSuperInterface(x, y) is true when interface x is a superinterface of class or interface y.
• HasInvokeStaticNode(m) is true when member m is directly invoked by a reachable static invocation node.
• HasInvokeExactNode(m) is true when member m is directly invoked by a reachable exact invocation node (including constructors).
• HasInvokeVirtualNode(m) is true when member m is indirectly invoked by a reachable virtual invocation node.
• HasInvokeInterfaceNode(m) is true when member m is indirectly invoked by a reachable interface invocation node.
• HasNewNode(t) is true when type t is used with a New node.
• IsClassOf(o, t) is true when the type of object o is t.
• HasLiteral(o) is true when object o appears by way of a reachable object literal.
• RefersTo(oa, ob) is true when object oa refers to object ob.
• RefersToMethod(o, m) is true when object o contains a pointer to method m.
• IsInherited(m, t) is true when method m is inherited from supertype t.

This is the initial, mostly-complete set that I've gleaned from the existing code. I've used the term "provisionally" instead of "deferred" in some places.

% -- object and class rules --

% If a method is directly invoked, it can appear in stack traces, and thus needs a `Class` instance.
HasClassObject(t) :- Encloses(t, m), HasInvokeExactNode(m).
HasClassObject(t) :- Encloses(t, m), HasInvokeStaticNode(m).

% If an object class is directly instantiated, it will usually have a constructor invocation; however, it is possible that this could be optimized away. Make sure there is explicitly a class object for this case.
% See `org.qbicc.plugin.reachability.ReachabilityBlockBuilder.ReachabilityVisitor#visit(org.qbicc.plugin.reachability.ReachabilityBlockBuilder.ReachabilityContext, org.qbicc.graph.New)`.
HasClassObject(t) :- HasNewNode(t).

% If an object class is used in an array, it will need a `Class` instance.
% See `org.qbicc.plugin.reachability.ReachabilityBlockBuilder.ReachabilityVisitor#visit(org.qbicc.plugin.reachability.ReachabilityBlockBuilder.ReachabilityContext, org.qbicc.graph.NewReferenceArray)`, `org.qbicc.plugin.reachability.ReachabilityBlockBuilder.ReachabilityVisitor#visit(org.qbicc.plugin.reachability.ReachabilityBlockBuilder.ReachabilityContext, org.qbicc.graph.MultiNewArray)`.
HasClassObject(t) :- HasClassObject(a), IsArray(a, t).

% An object is reachable when it is found in a literal or indirectly referred to from another reachable object.
% See `org.qbicc.plugin.reachability.BuildtimeHeapAnalyzer#traceHeap(org.qbicc.context.CompilationContext, org.qbicc.plugin.reachability.ReachabilityAnalysis, org.qbicc.interpreter.VmObject, org.qbicc.type.definition.element.ExecutableElement)`
IsReachableObject(o) :- HasLiteral(o).
IsReachableObject(o) :- IsReachableObject(oa), RefersTo(oa, o).

% If reachable object is on the heap, then its class considered to have an instance on the heap.
InstanceIsOnHeap(t) :- IsReachableObject(o), IsClassOf(o, t).

% If an object is reachable, then it must have a class object to support `getClass()`.
HasClassObject(t) :- InstanceIsOnHeap(t).

% If a subclass of a class has a class object, then the class also must have one to support `getSuperclass()` on the subclass object.
HasClassObject(t) :- HasClassObject(s), IsSuperClass(t, s).

% If a subtype of an interface has an interface object, then the interface must also have one to support `getInterfaces()` on the subtype object.
HasClassObject(t) :- HasClassObject(s), IsSuperInterface(t, s).

% -- invocation rules --

% A static method can be reachable directly.
IsStaticInvoked(m) :- HashInvokeStaticNode(m).

% A static method can be reachable via a heap object.
% See `org.qbicc.plugin.reachability.BuildtimeHeapAnalyzer#traceHeap(org.qbicc.context.CompilationContext, org.qbicc.plugin.reachability.ReachabilityAnalysis, org.qbicc.interpreter.VmObject, org.qbicc.type.definition.element.ExecutableElement)`.
IsStaticInvoked(m) :- IsReachableObject(o), RefersToMethod(o, m).

% If a method is called via virtual or interface invocation, but it is unknown whether the receiver actually exists on the heap, it is considered "provisionally dispatch invoked".
% See `org.qbicc.plugin.reachability.RapidTypeAnalysis#processReachableExactInvocation`
IsProvisionallyDispatchInvoked(m) :- HasInvokeVirtualNode(m); HasInvokeInterfaceNode(m).

% A method's receiver is considered to be on the heap when an instance of the method's enclosing type is on the heap.
ReceiverIsOnHeap(m) :- Encloses(t, m), InstanceIsOnHeap(t).

% A method's receiver is considered to be on the heap when that method is inherited by a class which has an instance on the heap.
% See `org.qbicc.plugin.reachability.RapidTypeAnalysis#processInstantiatedClass`.
RecevierIsOnHeap(m) :- IsInherited(m, s), InstanceIsOnHeap(s).

% A method is "dispatch invoked" when it is provisionally dispatch invoked and an instance of that object appears on the heap.
% See `org.qbicc.plugin.reachability.RapidTypeAnalysis#processInstantiatedClass` and `org.qbicc.plugin.reachability.RapidTypeAnalysis#processReachableExactInvocation`.
IsDispatchInvoked(m) :- IsProvisionallyDispatchInvoked(m), ReceiverIsOnHeap(m).

% -- field accesses --

% TODO: Accessing a static field causes its enclosing class to be reachable; why?

[dgrove-oss]

For dispatching, I think we are missing the rule that connects a reachable New to provisionally dispatched invokes. Something like:

IsDispatchInvoked(m) :- IsProvisionallyDispatchInvoked(m),  isInherited(m, s), HasNewNode(s)

I think there's a chance that the logic that says that accessing a static field causes the enclosing class to be reachable is a relic of when we were also tracking class initialization as part of reachability. However, if the static field is reachable we do need "somewhere" to put its declaration, so we need the ProgramModule for the class (or need somewhere else to put the declaration).

[dmlloyd]

For dispatching, I think we are missing the rule that connects a reachable New to provisionally dispatched invokes. Something like:

IsDispatchInvoked(m) :- IsProvisionallyDispatchInvoked(m),  isInherited(m, s), HasNewNode(s)

Hmm I think you're right; the RecevierIsOnHeap(m) :- IsInherited(m, s), InstanceIsOnHeap(s). rule gets us part of the way there through transitivity, but not all of the way. I think this addition might connect all of the dots:

InstanceIsOnHeap(t) :- HasNewNode(t).

I think there's a chance that the logic that says that accessing a static field causes the enclosing class to be reachable is a relic of when we were also tracking class initialization as part of reachability. However, if the static field is reachable we do need "somewhere" to put its declaration, so we need the ProgramModule for the class (or need somewhere else to put the declaration).

Ah that's a good point. I was actually thinking of another rule or rule set, something like this:

HasProgramModule(t) :- IsStaticInvoked(m), Encloses(t, m).
HasProgramModule(t) :- IsExactInvoked(m), Encloses(t, m).
% ...
% more rules covering field accesses, vtable/itable emission, literals, runtime initializers...

Or perhaps creating intermediate facts like HasVTable(t), HasLiteral(t), etc.

[dgrove-oss]

For dispatching, I think we are missing the rule that connects a reachable New to provisionally dispatched invokes. Something like:

IsDispatchInvoked(m) :- IsProvisionallyDispatchInvoked(m),  isInherited(m, s), HasNewNode(s)

Hmm I think you're right; the RecevierIsOnHeap(m) :- IsInherited(m, s), InstanceIsOnHeap(s). rule gets us part of the way there through transitivity, but not all of the way. I think this addition might connect all of the dots:

InstanceIsOnHeap(t) :- HasNewNode(t).

I wasn't sure if we wanted InstanceIsOnHeap to be talking about only the build-time heap or the union of the build time and runtime heap. If the later, then adding the rule you proposed would take care of it. If we want to be able to distinguish between types that are truly instantiated at build time and in the initial heap vs. types that "just" have a runtime reachable New then we'll need to do something subtler.

[dmlloyd]

I wasn't sure if we wanted InstanceIsOnHeap to be talking about only the build-time heap or the union of the build time and runtime heap. If the later, then adding the rule you proposed would take care of it. If we want to be able to distinguish between types that are truly instantiated at build time and in the initial heap vs. types that "just" have a runtime reachable New then we'll need to do something subtler.

It currently represents the union in the initial draft, though I'm not completely committed to that. I just can't think of a case where we need to distinguish being on the heap at build time vs being instantiated at run time - at least, not with our current initialization rules.