pts3o3h.dl

.type NumConstant
.decl isNumConstant(?n:NumConstant)
.type Modifier
.decl isModifier(?m:Modifier)
.decl Modifier_abstract(?mod:Modifier)
.decl Modifier_final(?mod:Modifier)
.decl Modifier_public(?mod:Modifier)
.decl Modifier_private(?mod:Modifier)
.decl Modifier_static(?mod:Modifier)
.type Type
.type PrimitiveType = Type
.type ReferenceType = Type
.type NullType = ReferenceType
.type ArrayType = ReferenceType
.type ClassType = ReferenceType
.type InterfaceType = ReferenceType
.decl isType(?t:Type)
.decl isPrimitiveType(?t:PrimitiveType)
.decl isReferenceType(?t:ReferenceType)
.decl isNullType(?t:NullType)
.decl isArrayType(?t:ArrayType)
.decl isClassType(?t:ClassType)
.decl isInterfaceType(?t:InterfaceType)
.decl DirectSuperclass(?class:ClassType, ?superclass:ClassType)
.decl DirectSuperinterface(?ref:ReferenceType, ?interface:InterfaceType)
.decl ApplicationClass(?ref:ReferenceType)
.decl ConcreteClass(?ref:ReferenceType)
.decl MainClass(?class:ClassType)
.decl Type_boolean(?t:PrimitiveType)
.decl Type_byte(?t:PrimitiveType)
.decl Type_char(?t:PrimitiveType)
.decl Type_short(?t:PrimitiveType)
.decl Type_int(?t:PrimitiveType)
.decl Type_long(?t:PrimitiveType)
.decl Type_float(?t:PrimitiveType)
.decl Type_double(?t:PrimitiveType)
.decl Type_void(?t:PrimitiveType)
.decl Type_null(?t:PrimitiveType)
.decl Type_object(?t:PrimitiveType)
.decl ClassModifier(?mod:Modifier, ?class:ReferenceType)
.type Field
.decl isField(?field:Field)
.decl Field_DeclaringType(?field:Field, ?declaringClass:ReferenceType)
.decl Field_SimpleName(?field:Field, ?simpleName:symbol)
.decl Field_Type(?field:Field, ?type:Type)
.decl Field_Modifier(?mod:Modifier, ?field:Field)
.type MethodDescriptor
.decl isMethodDescriptor(?md:MethodDescriptor)
.type Method
.decl isMethod(?m:Method)
.decl Method_DeclaringType(?method:Method, ?declaringType:ReferenceType)
.decl Method_ReturnType(?method:Method, ?returnType:Type)
.decl Method_SimpleName(?method:Method, ?simpleName:symbol)
.decl Method_Descriptor(?method:Method, ?descriptor:MethodDescriptor)
.type JVMDescriptor
.decl isJVMDescriptor(?jvmd:JVMDescriptor)
.decl Method_JVMDescriptor(?method:Method, ?descriptor:JVMDescriptor)
.decl Method_Modifier(?mod:Modifier, ?method:Method)
.decl Method_DeclaresException(?exceptionType:ReferenceType, ?method:Method)
.decl FormalParam(?index:number, ?method:Method, ?var:Var)
.decl ThisVar(?method:Method, ?var:Var)
.type Var
.decl isVar(v:Var)
.decl Var_Type(?var:Var, ?type:Type)
.decl Var_DeclaringMethod(?var:Var, ?method:Method)
.decl ApplicationVar(?var:Var)
.type HeapAllocation
.type NormalHeap = HeapAllocation
.type StringConstant = HeapAllocation
.type ClassHeap = HeapAllocation
.type MethodHandleConstant = HeapAllocation
.decl isHeapAllocation(?h:HeapAllocation)
.decl isNormalHeap(?h:NormalHeap)
.decl isStringConstant(?h:StringConstant)
.decl isClassHeap(?h:ClassHeap)
.decl isMethodHandleConstant(?h:MethodHandleConstant)
.decl isStringRaw(?id:symbol)
.decl HeapAllocation_Type(?heap:HeapAllocation, ?type:Type)
.decl HeapAllocation_EmptyArray(?heap:HeapAllocation)
.decl HeapAllocation_Null(?null:HeapAllocation)
.decl MainMethodArgArray(?heap:HeapAllocation)
.decl MainMethodArgArrayContent(?heap:HeapAllocation)
.decl ClassHeap_InstanceType(?classHeap:ClassHeap, ?instanceType:Type)
.decl MethodHandleConstant_InstanceType(?classHeap:MethodHandleConstant, ?instanceType:Type)
.type Instruction
.decl isInstruction(?insn:Instruction)
.decl Instruction_Index(?insn:Instruction, ?index:number)
.decl Instruction_Method(?insn:Instruction, ?inMethod:Method)
.type Throw_Insn = Instruction
.type ThrowNull_Insn = Throw_Insn
.type Goto_Insn = Instruction
.type If_Insn = Instruction
.type Switch_Insn = Instruction
.type TableSwitch_Insn = Switch_Insn
.type LookupSwitch_Insn = Switch_Insn
.type MonitorInstruction = Instruction
.type EnterMonitor_Insn = MonitorInstruction
.type ExitMonitor_Insn = MonitorInstruction
.type FieldInstruction = Instruction
.type LoadInstanceField_Insn = FieldInstruction
.type StoreInstanceField_Insn = FieldInstruction
.type LoadStaticField_Insn = FieldInstruction
.type StoreStaticField_Insn = FieldInstruction
.type ArrayInstruction = Instruction
.type LoadArrayIndex_Insn = ArrayInstruction
.type StoreArrayIndex_Insn = ArrayInstruction
.decl isThrow_Insn(?insn:Throw_Insn)
.decl isThrowNull_Insn(?insn:ThrowNull_Insn)
.decl isGoto_Insn(?insn:Goto_Insn)
.decl isIf_Insn(?insn:If_Insn)
.decl isSwitch_Insn(?insn:Switch_Insn)
.decl isTableSwitch_Insn(?insn:TableSwitch_Insn)
.decl isLookupSwitch_Insn(?insn:LookupSwitch_Insn)
.decl isMonitorInstruction(?insn:MonitorInstruction)
.decl isEnterMonitor_Insn(?insn:EnterMonitor_Insn)
.decl isExitMonitor_Insn(?insn:ExitMonitor_Insn)
.decl isFieldInstruction(?insn:FieldInstruction)
.decl isLoadInstanceField_Insn(?insn:LoadInstanceField_Insn)
.decl isStoreInstanceField_Insn(?insn:StoreInstanceField_Insn)
.decl isLoadStaticField_Insn(?insn:LoadStaticField_Insn)
.decl isStoreStaticField_Insn(?insn:StoreStaticField_Insn)
.decl isArrayInstruction(?insn:ArrayInstruction)
.decl isLoadArrayIndex_Insn(?insn:LoadArrayIndex_Insn)
.decl isStoreArrayIndex_Insn(?insn:StoreArrayIndex_Insn)
.type AssignInstruction = Instruction
.type AssignOper_Insn = AssignInstruction
.type AssignBinop_Insn = AssignOper_Insn
.type AssignUnop_Insn = AssignOper_Insn
.type AssignLocal_Insn = AssignOper_Insn
.type AssignInstanceOf_Insn = AssignInstruction
.type AssignNull_Insn = AssignInstruction
.type AssignNumConstant_Insn = AssignInstruction
.type AssignCast_Insn = AssignInstruction
.type AssignCastNull_Insn = AssignCast_Insn
.type AssignCastNumConstant_Insn = AssignCast_Insn
.type AssignHeapAllocation_Insn = AssignInstruction
.type ReturnInstruction = Instruction
.type ReturnVoid_Insn = ReturnInstruction
.type ReturnNonvoid_Insn = ReturnInstruction
.decl isAssignInstruction(?insn:AssignInstruction)
.decl isAssignOper_Insn(?insn:AssignOper_Insn)
.decl isAssignBinop_Insn(?insn:AssignBinop_Insn)
.decl isAssignUnop_Insn(?insn:AssignUnop_Insn)
.decl isAssignLocal_Insn(?insn:AssignLocal_Insn)
.decl isAssignInstanceOf_Insn(?insn:AssignInstanceOf_Insn)
.decl isAssignNull_Insn(?insn:AssignNull_Insn)
.decl isAssignNumConstant_Insn(?insn:AssignNumConstant_Insn)
.decl isAssignCast_Insn(?insn:AssignCast_Insn)
.decl isAssignCastNull_Insn(?insn:AssignCastNull_Insn)
.decl isAssignCastNumConstant_Insn(?insn:AssignCastNumConstant_Insn)
.decl isAssignHeapAllocation_Insn(?insn:AssignHeapAllocation_Insn)
.decl isReturnInstruction(?insn:ReturnInstruction)
.decl isReturnVoid_Insn(?insn:ReturnVoid_Insn)
.decl isReturnNonvoid_Insn(?insn:ReturnNonvoid_Insn)
.type MethodInvocation = Instruction
.type VirtualMethodInvocation_Insn = MethodInvocation
.type SpecialMethodInvocation_Insn = MethodInvocation
.type StaticMethodInvocation_Insn = MethodInvocation
.type DynamicMethodInvocation_Insn = MethodInvocation
.decl isMethodInvocation(?insn:MethodInvocation)
.decl isVirtualMethodInvocation_Insn(?insn:VirtualMethodInvocation_Insn)
.decl isSpecialMethodInvocation_Insn(?insn:SpecialMethodInvocation_Insn)
.decl isStaticMethodInvocation_Insn(?insn:StaticMethodInvocation_Insn)
.decl isDynamicMethodInvocation_Insn(?insn:DynamicMethodInvocation_Insn)
.type UnsupportedInstruction = Instruction
.type AssignPhantomInvoke = UnsupportedInstruction
.type PhantomInvoke = UnsupportedInstruction
.type BreakpointStmt = UnsupportedInstruction
.decl isUnsupportedInstruction(?insn:UnsupportedInstruction)
.decl isAssignPhantomInvoke(?insn:AssignPhantomInvoke)
.decl isPhantomInvoke(?insn:PhantomInvoke)
.decl isBreakpointStmt(?insn:BreakpointStmt)
.decl If_Var(?insn:If_Insn, ?var:Var)
.decl Throw_Var(?insn:Throw_Insn, ?var:Var)
.decl Goto_Target(?insn:Goto_Insn, ?index:number)
.decl If_Target(?insn:If_Insn, ?index:number)
.decl Switch_Key(?insn:Switch_Insn, ?key:Var)
.decl Switch_Target(?insn:Switch_Insn, ?value:number, ?index:number)
.decl Switch_DefaultTarget(?insn:Switch_Insn, ?index:number)
.decl EnterMonitor_Var(?insn:EnterMonitor_Insn, ?var:Var)
.decl ExitMonitor_Var(?insn:ExitMonitor_Insn, ?var:Var)
.decl FieldInstruction_Signature(?insn:FieldInstruction, ?sign:Field)
.decl LoadInstanceField_Base(?insn:LoadInstanceField_Insn, ?var:Var)
.decl LoadInstanceField_To(?insn:LoadInstanceField_Insn, ?var:Var)
.decl StoreInstanceField_From(?insn:StoreInstanceField_Insn, ?var:Var)
.decl StoreInstanceField_Base(?insn:StoreInstanceField_Insn, ?var:Var)
.decl LoadStaticField_To(?insn:LoadStaticField_Insn, ?var:Var)
.decl StoreStaticField_From(?insn:StoreStaticField_Insn, ?var:Var)
.decl ArrayInsnIndex(?insn:Instruction, ?index:Var)
.decl ComponentType(?arrayType:ArrayType, ?componentType:Type)
.decl LoadArrayIndex_Base(?insn:LoadArrayIndex_Insn, ?var:Var)
.decl LoadArrayIndex_To(?insn:LoadArrayIndex_Insn, var:Var)
.decl StoreArrayIndex_From(?insn:StoreArrayIndex_Insn, ?var:Var)
.decl StoreArrayIndex_Base(?insn:StoreArrayIndex_Insn, ?var:Var)
.decl AssignInstruction_To(?insn:AssignInstruction, ?to:Var)
.decl AssignNumConstant_Id(?insn:AssignNumConstant_Insn, ?const:NumConstant)
.decl AssignCast_From(?insn:AssignCast_Insn, ?from:Var)
.decl AssignCast_Type(?insn:AssignCast_Insn, ?type:Type)
.decl AssignCastNumConstant_Id(?insn:AssignCastNumConstant_Insn, ?const:NumConstant)
.decl AssignLocal_From(?insn:AssignLocal_Insn, ?from:Var)
.decl AssignInstanceOf_From(?insn:AssignInstanceOf_Insn, ?from:Var)
.decl AssignInstanceOf_Type(?insn:AssignInstanceOf_Insn, ?type:Type)
.decl AssignOper_From(?insn:AssignOper_Insn, ?from:Var)
.decl AssignOper_Type(?insn:AssignOper_Insn, ?type:symbol)
.decl AssignHeapAllocation_Heap(?insn:AssignHeapAllocation_Insn, ?heap:HeapAllocation)
.decl ReturnNonvoid_Var(?return:ReturnNonvoid_Insn, ?var:Var)
.decl MethodInvocation_Line(?invocation:MethodInvocation, ?line:number)
.decl MethodInvocation_Method(?invocation:MethodInvocation, ?signature:Method)
.decl ApplicationMethod(?method:Method)
.output ApplicationMethod(IO="file",filename="ApplicationMethod.csv",delimiter="\t")
.decl AssignReturnValue(?invocation:MethodInvocation, ?to:Var)
.decl ActualParam(?index:number, ?invocation:MethodInvocation, ?var:Var)
.decl VirtualMethodInvocation_Base(?invocation:VirtualMethodInvocation_Insn, ?base:Var)
.decl VirtualMethodInvocation_SimpleName(?invocation:MethodInvocation, ?simplename:symbol)
.decl VirtualMethodInvocation_Descriptor(?invocation:MethodInvocation, ?descriptor:MethodDescriptor)
.decl DynamicMethodInvocation_Bootstrap(?invocation:DynamicMethodInvocation_Insn, ?bootSignature:Method)
.decl DynamicMethodInvocation_DynMethod(?invocation:DynamicMethodInvocation_Insn, ?dynName:symbol)
.decl BootstrapParam(?index:number, ?invocation:DynamicMethodInvocation_Insn, ?var:Var)
.decl StaticMethodInvocation_SimpleName(?invocation:MethodInvocation, ?simplename:symbol)
.decl StaticMethodInvocation_Descriptor(?invocation:MethodInvocation, ?descriptor:MethodDescriptor)
.decl SpecialMethodInvocation_Base(?invocation:SpecialMethodInvocation_Insn, ?base:Var)
.decl SpecialMethodInvocation_SimpleName(?invocation:MethodInvocation, ?simplename:symbol)
.decl SpecialMethodInvocation_Descriptor(?invocation:MethodInvocation, ?descriptor:MethodDescriptor)
.type ExceptionHandler
.decl isExceptionHandler(?handler:ExceptionHandler)
.decl ExceptionHandler_Method(?handler:ExceptionHandler, ?inmethod:Method)
.decl ExceptionHandler_Index(?handler:ExceptionHandler, ?index:number)
.decl ExceptionHandler_Type(?handler:ExceptionHandler, ?type:Type)
.decl ExceptionHandler_FormalParam(?handler:ExceptionHandler, ?var:Var)
.decl ExceptionHandler_Begin(?handler:ExceptionHandler, ?index:number)
.decl ExceptionHandler_End(?handler:ExceptionHandler, ?index:number)
.decl ExceptionHandler_Previous(?handler:ExceptionHandler, ?previous:ExceptionHandler)
.decl Properties(?path:StringConstant, ?key:StringConstant, ?value:StringConstant)
.decl NativeReturnVar(?var:Var, ?method:Method)
.decl Config_DynamicClass(?class:ReferenceType, ?invocation:MethodInvocation)
.decl Stats_Metrics(order:symbol, msg:symbol, c:number)
.decl Activity(?x:Type)
.decl Service(?x:Type)
.decl ContentProvider(?x:Type)
.decl BroadcastReceiver(?x:Type)
.decl CallbackMethod(?x:Method)
.decl LayoutControl(?id:NumConstant, ?type:Type, ?parent:symbol)
.decl LayoutControl0(?id:NumConstant, ?typename:symbol, ?parent:symbol)
.decl FieldInitialValue(?fld:Field, ?valueString:symbol)
.decl AndroidEntryPoint(?m:Method)
.decl Throw(?insn:Throw_Insn, ?var:Var)
.decl LoadInstanceField(?base:Var, ?sig:Field, ?to:Var, ?inmethod:Method)
.decl StoreInstanceField(?from:Var, ?base:Var, ?signature:Field, ?inmethod:Method)
.decl LoadStaticField(?sig:Field, ?to:Var, ?inmethod:Method)
.decl StoreStaticField(?from:Var, ?signature:Field, ?inmethod:Method)
.decl LoadArrayIndex(?base:Var, ?to:Var, ?inmethod:Method)
.decl StoreArrayIndex(?from:Var, ?base:Var, ?inmethod:Method)
.decl AssignCast(?type:Type, ?from:Var, ?to:Var, ?inmethod:Method)
.decl AssignLocal(?from:Var, ?to:Var, ?inmethod:Method)
.decl AssignNull(?to:Var, ?inmethod:Method)
.decl AssignHeapAllocation(?heap:HeapAllocation, ?to:Var, ?inmethod:Method)
.decl ReturnVar(?var:Var, ?method:Method)
.decl VirtualMethodInvocation(?invocation:MethodInvocation, ?signature:Method, ?inmethod:Method)
.decl StaticMethodInvocation(?invocation:MethodInvocation, ?signature:Method, ?inmethod:Method)
.decl _ClassType(?class:symbol)
.input _ClassType(IO="file", filename="ClassType.facts", delimiter="\t")
isType(?class),
isReferenceType(?class),
isClassType(?class) :-
  _ClassType(?class).
.decl _ArrayType(?arrayType:symbol)
.input _ArrayType(IO="file", filename="ArrayType.facts", delimiter="\t")
isType(?arrayType),
isReferenceType(?arrayType),
isArrayType(?arrayType) :-
  _ArrayType(?arrayType).
.decl _InterfaceType(?interface:symbol)
.input _InterfaceType(IO="file", filename="InterfaceType.facts", delimiter="\t")
isType(?interface),
isReferenceType(?interface),
isInterfaceType(?interface) :-
  _InterfaceType(?interface).
.decl _ComponentType(?arrayType:symbol, ?componentType:symbol)
.input _ComponentType(IO="file", filename="ComponentType.facts", delimiter="\t")
isType(?arrayType),
isReferenceType(?arrayType),
isArrayType(?arrayType),
isType(?componentType),
ComponentType(?arrayType, ?componentType) :-
  _ComponentType(?arrayType, ?componentType).
.decl _ActualParam(?index:number, ?invocation:symbol, ?var:symbol)
.input _ActualParam(IO="file", filename="ActualParam.facts", delimiter="\t")
isInstruction(?invocation),
isMethodInvocation(?invocation),
isVar(?var),
ActualParam(?index, ?invocation, ?var) :-
  _ActualParam(?index, ?invocation, ?var).
.decl _BootstrapParam(?index:number, ?invocation:symbol, ?var:symbol)
.input _BootstrapParam(IO="file", filename="BootstrapParam.facts", delimiter="\t")
isInstruction(?invocation),
isMethodInvocation(?invocation),
isDynamicMethodInvocation_Insn(?invocation),
isVar(?var),
BootstrapParam(?index, ?invocation, ?var) :-
  _BootstrapParam(?index, ?invocation, ?var).
.decl _DirectSuperinterface(?class:symbol, ?interface:symbol)
.input _DirectSuperinterface(IO="file", filename="DirectSuperinterface.facts", delimiter="\t")
isType(?class),
isReferenceType(?class),
isType(?interface),
isReferenceType(?interface),
isInterfaceType(?interface),
DirectSuperinterface(?class, ?interface) :-
  _DirectSuperinterface(?class, ?interface).
.decl _DirectSuperclass(?class:symbol, ?superclass:symbol)
.input _DirectSuperclass(IO="file", filename="DirectSuperclass.facts", delimiter="\t")
isType(?class),
isReferenceType(?class),
isClassType(?class),
isType(?superclass),
isReferenceType(?superclass),
isClassType(?superclass),
DirectSuperclass(?class, ?superclass) :-
  _DirectSuperclass(?class, ?superclass).
.decl _Field_Modifier(?modifier:symbol, ?field:symbol)
.input _Field_Modifier(IO="file", filename="Field-Modifier.facts", delimiter="\t")
isModifier(?modifier),
isField(?field),
Field_Modifier(?modifier, ?field) :-
  _Field_Modifier(?modifier, ?field).
.decl _ClassModifier(?class:symbol, ?modifier:symbol)
.input _ClassModifier(IO="file", filename="ClassModifier.facts", delimiter="\t")
ClassModifier(?class, ?modifier) :-
  _ClassModifier(?class, ?modifier).
.decl _FormalParam(?index:number, ?method:symbol, ?var:symbol)
.input _FormalParam(IO="file", filename="FormalParam.facts", delimiter="\t")
isMethod(?method),
isVar(?var),
FormalParam(?index, ?method, ?var) :-
  _FormalParam(?index, ?method, ?var).
.decl _Method_DeclaresException(?exceptionType:symbol, ?method:symbol)
.input _Method_DeclaresException(IO="file", filename="Method-DeclaresException.facts", delimiter="\t")
isType(?exceptionType),
isReferenceType(?exceptionType),
isMethod(?method),
Method_DeclaresException(?exceptionType, ?method) :-
  _Method_DeclaresException(?exceptionType, ?method).
.decl _Method_Modifier(?mod:symbol, ?method:symbol)
.input _Method_Modifier(IO="file", filename="Method-Modifier.facts", delimiter="\t")
isModifier(?mod),
isMethod(?method),
Method_Modifier(?mod, ?method) :-
  _Method_Modifier(?mod, ?method).
.decl _NativeReturnVar(?var:symbol, ?method:symbol)
.input _NativeReturnVar(IO="file", filename="NativeReturnVar.facts", delimiter="\t")
isVar(?var),
isMethod(?method),
NativeReturnVar(?var, ?method) :-
  _NativeReturnVar(?var, ?method).
.decl _Var_Type(?var:symbol, ?type:symbol)
.input _Var_Type(IO="file", filename="Var-Type.facts", delimiter="\t")
isVar(?var),
isType(?type),
Var_Type(?var, ?type) :-
  _Var_Type(?var, ?type).
.decl _Var_DeclaringMethod(?var:symbol, ?method:symbol)
.input _Var_DeclaringMethod(IO="file", filename="Var-DeclaringMethod.facts", delimiter="\t")
isVar(?var),
isMethod(?method),
Var_DeclaringMethod(?var, ?method) :-
  _Var_DeclaringMethod(?var, ?method).
.decl _ApplicationClass(?type:symbol)
.input _ApplicationClass(IO="file", filename="ApplicationClass.facts", delimiter="\t")
isType(?type),
isReferenceType(?type),
ApplicationClass(?type) :-
  _ApplicationClass(?type).
.decl _ThisVar(?method:symbol, ?var:symbol)
.input _ThisVar(IO="file", filename="ThisVar.facts", delimiter="\t")
isMethod(?method),
isVar(?var),
ThisVar(?method, ?var) :-
  _ThisVar(?method, ?var).
.decl _ExceptionHandler_Previous(?handler:symbol, ?previous:symbol)
.input _ExceptionHandler_Previous(IO="file", filename="ExceptionHandler-Previous.facts", delimiter="\t")
isExceptionHandler(?handler),
isExceptionHandler(?previous),
ExceptionHandler_Previous(?handler, ?previous) :-
  _ExceptionHandler_Previous(?handler, ?previous).
.decl _AssignReturnValue(?invocation:symbol, ?to:symbol)
.input _AssignReturnValue(IO="file", filename="AssignReturnValue.facts", delimiter="\t")
isInstruction(?invocation),
isMethodInvocation(?invocation),
isVar(?to),
AssignReturnValue(?invocation, ?to) :-
  _AssignReturnValue(?invocation, ?to).
.decl _NormalHeap(?id:symbol, ?type:symbol)
.input _NormalHeap(IO="file", filename="NormalHeap.facts", delimiter="\t")
isType(?type),
isHeapAllocation(?id),
isNormalHeap(?id),
HeapAllocation_Type(?id, ?type) :-
  _NormalHeap(?id, ?type).
isClassType("java.lang.String").
.decl _StringConstant(?id:symbol)
.input _StringConstant(IO="file", filename="StringConstant.facts", delimiter="\t")
isHeapAllocation(?id),
isStringConstant(?id),
HeapAllocation_Type(?id, "java.lang.String") :-
  _StringConstant(?id).
.decl _StringRaw(?id:symbol, ?rawId:symbol)
.input _StringRaw(IO="file", filename="StringRaw.facts", delimiter="\t")
.decl String_toRaw(?id:symbol, ?rawId:symbol)
isStringRaw(?id),
String_toRaw(?id, ?rawId) :-
  _StringRaw(?id, ?rawId).
.decl _ClassHeap(?id:symbol, ?instanceType:symbol)
.input _ClassHeap(IO="file", filename="ClassHeap.facts", delimiter="\t")
isType(?instanceType),
isHeapAllocation(?id),
isClassHeap(?id),
ClassHeap_InstanceType(?id, ?instanceType),
HeapAllocation_Type(?id, "java.lang.Class") :-
  _ClassHeap(?id, ?instanceType).
.decl _MethodHandleConstant(?id:symbol)
.input _MethodHandleConstant(IO="file", filename="MethodHandleConstant.facts", delimiter="\t")
isType("java.lang.invoke.MethodHandle").
isReferenceType("java.lang.invoke.MethodHandle").
isClassType("java.lang.invoke.MethodHandle").
isHeapAllocation(?id),
isMethodHandleConstant(?id),
HeapAllocation_Type(?id, "java.lang.invoke.MethodHandle") :-
  _MethodHandleConstant(?id).
.decl _EmptyArray(?id:symbol)
.input _EmptyArray(IO="file", filename="EmptyArray.facts", delimiter="\t")
HeapAllocation_EmptyArray(?id) :-
  _EmptyArray(?id).
.decl _AssignHeapAllocation(?instruction:symbol, ?index:number, ?heap:symbol, ?to:symbol, ?inmethod:symbol)
.input _AssignHeapAllocation(IO="file", filename="AssignHeapAllocation.facts", delimiter="\t")
isInstruction(?instruction),
isAssignInstruction(?instruction),
isAssignHeapAllocation_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
AssignInstruction_To(?instruction, ?to),
AssignHeapAllocation_Heap(?instruction, ?heap) :-
  _AssignHeapAllocation(?instruction, ?index, ?heap, ?to, ?method).
.decl _AndroidEntryPoint(?method:symbol)
.input _AndroidEntryPoint(IO="file", filename="AndroidEntryPoint.facts", delimiter="\t")
AndroidEntryPoint(?method) :-
  _AndroidEntryPoint(?method).
.decl _AssignLocal(?instruction:symbol, ?index:number, ?from:symbol, ?to:symbol, ?inmethod:symbol)
.input _AssignLocal(IO="file", filename="AssignLocal.facts", delimiter="\t")
isInstruction(?instruction),
isAssignInstruction(?instruction),
isAssignOper_Insn(?instruction),
isAssignLocal_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
AssignLocal_From(?instruction, ?from),
AssignInstruction_To(?instruction, ?to) :-
  _AssignLocal(?instruction, ?index, ?from, ?to, ?method).
.decl _AssignBinop(?instruction:symbol, ?index:number, ?to:symbol, ?inmethod:symbol)
.input _AssignBinop(IO="file", filename="AssignBinop.facts", delimiter="\t")
isInstruction(?instruction),
isAssignInstruction(?instruction),
isAssignOper_Insn(?instruction),
isAssignBinop_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
AssignInstruction_To(?instruction, ?to) :-
  _AssignBinop(?instruction, ?index, ?to, ?method).
.decl _AssignUnop(?instruction:symbol, ?index:number, ?to:symbol, ?inmethod:symbol)
.input _AssignUnop(IO="file", filename="AssignUnop.facts", delimiter="\t")
isInstruction(?instruction),
isAssignInstruction(?instruction),
isAssignOper_Insn(?instruction),
isAssignUnop_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
AssignInstruction_To(?instruction, ?to) :-
  _AssignUnop(?instruction, ?index, ?to, ?method).
.decl _AssignOperFrom(?instruction:symbol, ?from:symbol)
.input _AssignOperFrom(IO="file", filename="AssignOperFrom.facts", delimiter="\t")
AssignOper_From(?instruction, ?from) :-
  _AssignOperFrom(?instruction, ?from).
.decl _AssignOperType(?instruction:symbol, ?type:symbol)
.input _AssignOperType(IO="file", filename="AssignOperType.facts", delimiter="\t")
AssignOper_Type(?instruction, ?type) :-
  _AssignOperType(?instruction, ?type).
.decl _IfVar(?instruction:symbol, ?var:symbol)
.input _IfVar(IO="file", filename="IfVar.facts", delimiter="\t")
If_Var(?instruction, ?var) :-
  _IfVar(?instruction, ?var).
.decl _AssignCast(?instruction:symbol, ?index:number, ?from:symbol, ?to:symbol, ?type:symbol, ?inmethod:symbol)
.input _AssignCast(IO="file", filename="AssignCast.facts", delimiter="\t")
isInstruction(?instruction),
isAssignInstruction(?instruction),
isAssignCast_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
AssignCast_Type(?instruction, ?type),
AssignCast_From(?instruction, ?from),
AssignInstruction_To(?instruction, ?to) :-
  _AssignCast(?instruction, ?index, ?from, ?to, ?type, ?method).
.decl _AssignCastNumConstant(?instruction:symbol, ?index:number, ?const:symbol, ?to:symbol, ?type:symbol, ?inmethod:symbol)
.input _AssignCastNumConstant(IO="file", filename="AssignCastNumConstant.facts", delimiter="\t")
isNumConstant(?const),
isInstruction(?instruction),
isAssignInstruction(?instruction),
isAssignCast_Insn(?instruction),
isAssignCastNumConstant_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
AssignCast_Type(?instruction, ?type),
AssignCastNumConstant_Id(?instruction, ?const),
AssignInstruction_To(?instruction, ?to) :-
  _AssignCastNumConstant(?instruction, ?index, ?const, ?to, ?type, ?method).
.decl _AssignCastNull(?instruction:symbol, ?index:number, ?to:symbol, ?type:symbol, ?method:symbol)
.input _AssignCastNull(IO="file", filename="AssignCastNull.facts", delimiter="\t")
isInstruction(?instruction),
isAssignInstruction(?instruction),
isAssignCast_Insn(?instruction),
isAssignCastNull_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
AssignCast_Type(?instruction, ?type),
AssignInstruction_To(?instruction, ?to) :-
  _AssignCastNull(?instruction, ?index, ?to, ?type, ?method).
.decl _AssignNumConstant(?instruction:symbol, ?index:number, ?const:symbol, ?to:symbol, ?inmethod:symbol)
.input _AssignNumConstant(IO="file", filename="AssignNumConstant.facts", delimiter="\t")
isNumConstant(?const),
isInstruction(?instruction),
isAssignInstruction(?instruction),
isAssignNumConstant_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
AssignNumConstant_Id(?instruction, ?const),
AssignInstruction_To(?instruction, ?to) :-
  _AssignNumConstant(?instruction, ?index, ?const, ?to, ?method).
.decl _AssignNull(?instruction:symbol, ?index:number, ?to:symbol, ?method:symbol)
.input _AssignNull(IO="file", filename="AssignNull.facts", delimiter="\t")
isInstruction(?instruction),
isAssignInstruction(?instruction),
isAssignNull_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
AssignInstruction_To(?instruction, ?to) :-
  _AssignNull(?instruction, ?index, ?to, ?method).
.decl _AssignInstanceOf(?instruction:symbol, ?index:number, ?from:symbol, ?to:symbol, ?type:symbol, ?inmethod:symbol)
.input _AssignInstanceOf(IO="file", filename="AssignInstanceOf.facts", delimiter="\t")
isInstruction(?instruction),
isAssignInstruction(?instruction),
isAssignInstanceOf_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
AssignInstanceOf_From(?instruction, ?from),
AssignInstanceOf_Type(?instruction, ?type),
AssignInstruction_To(?instruction, ?to) :-
  _AssignInstanceOf(?instruction, ?index, ?from, ?to, ?type, ?method).
.decl _Field(?signature:symbol, ?declaringClass:symbol, ?simplename:symbol, ?type:symbol)
.input _Field(IO="file", filename="Field.facts", delimiter="\t")
isField(?signature),
Field_DeclaringType(?signature, ?declaringType),
Field_SimpleName(?signature, ?simplename),
Field_Type(?signature, ?type) :-
  _Field(?signature, ?declaringType, ?simplename, ?type).
.decl _EnterMonitor(?instruction:symbol, ?index:number, ?var:symbol, ?method:symbol)
.input _EnterMonitor(IO="file", filename="EnterMonitor.facts", delimiter="\t")
isInstruction(?instruction),
isMonitorInstruction(?instruction),
isEnterMonitor_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
EnterMonitor_Var(?instruction, ?var) :-
  _EnterMonitor(?instruction, ?index, ?var, ?method).
.decl _ExitMonitor(?instruction:symbol, ?index:number, ?var:symbol, ?method:symbol)
.input _ExitMonitor(IO="file", filename="ExitMonitor.facts", delimiter="\t")
isInstruction(?instruction),
isMonitorInstruction(?instruction),
isExitMonitor_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
ExitMonitor_Var(?instruction, ?var) :-
  _ExitMonitor(?instruction, ?index, ?var, ?method).
.decl _MethodInvocation_Line(?instruction:symbol, line:number)
.input _MethodInvocation_Line(IO="file", filename="MethodInvocation-Line.facts", delimiter="\t")
isMethodInvocation(?instruction),
MethodInvocation_Line(?instruction, ?line) :-
  _MethodInvocation_Line(?instruction, ?line).
.decl _StaticMethodInvocation(?instruction:symbol, ?index:number, ?signature:symbol, ?method:symbol)
.input _StaticMethodInvocation(IO="file", filename="StaticMethodInvocation.facts", delimiter="\t")
isMethod(?signature),
isInstruction(?instruction),
isMethodInvocation(?instruction),
isStaticMethodInvocation_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
MethodInvocation_Method(?instruction, ?signature) :-
  _StaticMethodInvocation(?instruction, ?index, ?signature, ?method).
.decl _SpecialMethodInvocation(?instruction:symbol, ?index:number, ?signature:symbol, ?base:symbol, ?method:symbol)
.input _SpecialMethodInvocation(IO="file", filename="SpecialMethodInvocation.facts", delimiter="\t")
isMethod(?signature),
isInstruction(?instruction),
isMethodInvocation(?instruction),
isSpecialMethodInvocation_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
SpecialMethodInvocation_Base(?instruction, ?base),
MethodInvocation_Method(?instruction, ?signature) :-
  _SpecialMethodInvocation(?instruction, ?index, ?signature, ?base, ?method).
.decl _VirtualMethodInvocation(?instruction:symbol, ?index:number, ?signature:symbol, ?base:symbol, ?method:symbol)
.input _VirtualMethodInvocation(IO="file", filename="VirtualMethodInvocation.facts", delimiter="\t")
isMethod(?signature),
isInstruction(?instruction),
isMethodInvocation(?instruction),
isVirtualMethodInvocation_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
VirtualMethodInvocation_Base(?instruction, ?base),
MethodInvocation_Method(?instruction, ?signature) :-
  _VirtualMethodInvocation(?instruction, ?index, ?signature, ?base, ?method).
.decl _DynamicMethodInvocation(?instruction:symbol, ?index:number, ?bootSignature:symbol, ?dynName:symbol, ?method:symbol)
.input _DynamicMethodInvocation(IO="file", filename="DynamicMethodInvocation.facts", delimiter="\t")
isInstruction(?instruction),
isMethodInvocation(?instruction),
isDynamicMethodInvocation_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
DynamicMethodInvocation_Bootstrap(?instruction, ?bootSignature),
DynamicMethodInvocation_DynMethod(?instruction, ?dynName) :-
  _DynamicMethodInvocation(?instruction, ?index, ?bootSignature, ?dynName, ?method).
.decl _Throw(?instruction:symbol, ?index:number, ?var:symbol, ?method:symbol)
.input _Throw(IO="file", filename="Throw.facts", delimiter="\t")
isInstruction(?instruction),
isThrow_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
Throw(?instruction, ?var),
Throw_Var(?instruction, ?var) :-
  _Throw(?instruction, ?index, ?var, ?method).
.decl _ThrowNull(?instruction:symbol, ?index:number, ?method:symbol)
.input _ThrowNull(IO="file", filename="ThrowNull.facts", delimiter="\t")
isInstruction(?instruction),
isThrow_Insn(?instruction),
isThrowNull_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method) :-
  _ThrowNull(?instruction, ?index, ?method).
.decl _ExceptionHandler(?handler:symbol, ?method:symbol, ?index:number, ?type:symbol, ?var:symbol, ?begin:number, ?end:number)
.input _ExceptionHandler(IO="file", filename="ExceptionHandler.facts", delimiter="\t")
isExceptionHandler(?handler),
ExceptionHandler_Method(?handler, ?method),
ExceptionHandler_Index(?handler, ?index),
ExceptionHandler_Type(?handler, ?type),
ExceptionHandler_FormalParam(?handler, ?var),
ExceptionHandler_Begin(?handler, ?begin),
ExceptionHandler_End(?handler, ?end) :-
  _ExceptionHandler(?handler, ?method, ?index, ?type, ?var, ?begin, ?end).
.decl _Method(?method:symbol, ?simplename:symbol, ?descriptor:symbol, ?declaringType:symbol, ?returnType:symbol, ?jvmDescriptor:symbol)
.input _Method(IO="file", filename="Method.facts", delimiter="\t")
isMethod(?method),
isMethodDescriptor(?descriptor),
isJVMDescriptor(?jvmDescriptor),
Method_SimpleName(?method, ?simplename),
Method_Descriptor(?method, ?descriptor),
Method_DeclaringType(?method, ?declaringType),
Method_JVMDescriptor(?method, ?jvmDescriptor),
Method_ReturnType(?method, ?returnType) :-
  _Method(?method, ?simplename, ?descriptor, ?declaringType, ?returnType, ?jvmDescriptor).
.decl _StoreInstanceField(?instruction:symbol, ?index:number, ?from:symbol, ?base:symbol, ?signature:symbol, ?method:symbol)
.input _StoreInstanceField(IO="file", filename="StoreInstanceField.facts", delimiter="\t")
isInstruction(?instruction),
isFieldInstruction(?instruction),
isStoreInstanceField_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
FieldInstruction_Signature(?instruction, ?signature),
StoreInstanceField_Base(?instruction, ?base),
StoreInstanceField_From(?instruction, ?from) :-
  _StoreInstanceField(?instruction, ?index, ?from, ?base, ?signature, ?method).
.decl _LoadInstanceField(?instruction:symbol, ?index:number, ?to:symbol, ?base:symbol, ?signature:symbol, ?method:symbol)
.input _LoadInstanceField(IO="file", filename="LoadInstanceField.facts", delimiter="\t")
isInstruction(?instruction),
isFieldInstruction(?instruction),
isLoadInstanceField_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
FieldInstruction_Signature(?instruction, ?signature),
LoadInstanceField_Base(?instruction, ?base),
LoadInstanceField_To(?instruction, ?to) :-
  _LoadInstanceField(?instruction, ?index, ?to, ?base, ?signature, ?method).
.decl _StoreStaticField(?instruction:symbol, ?index:number, ?from:symbol, ?signature:symbol, ?method:symbol)
.input _StoreStaticField(IO="file", filename="StoreStaticField.facts", delimiter="\t")
isInstruction(?instruction),
isFieldInstruction(?instruction),
isStoreStaticField_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
FieldInstruction_Signature(?instruction, ?signature),
StoreStaticField_From(?instruction, ?from) :-
  _StoreStaticField(?instruction, ?index, ?from, ?signature, ?method).
.decl _LoadStaticField(?instruction:symbol, ?index:number, ?to:symbol, ?signature:symbol, ?method:symbol)
.input _LoadStaticField(IO="file", filename="LoadStaticField.facts", delimiter="\t")
isInstruction(?instruction),
isFieldInstruction(?instruction),
isLoadStaticField_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
FieldInstruction_Signature(?instruction, ?signature),
LoadStaticField_To(?instruction, ?to) :-
  _LoadStaticField(?instruction, ?index, ?to, ?signature, ?method).
.decl _StoreArrayIndex(?instruction:symbol, ?index:number, ?from:symbol, ?base:symbol, ?method:symbol)
.input _StoreArrayIndex(IO="file", filename="StoreArrayIndex.facts", delimiter="\t")
isInstruction(?instruction),
isArrayInstruction(?instruction),
isStoreArrayIndex_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
StoreArrayIndex_Base(?instruction, ?base),
StoreArrayIndex_From(?instruction, ?from) :-
  _StoreArrayIndex(?instruction, ?index, ?from, ?base, ?method).
.decl _LoadArrayIndex(?instruction:symbol, ?index:number, ?to:symbol, ?base:symbol, ?method:symbol)
.input _LoadArrayIndex(IO="file", filename="LoadArrayIndex.facts", delimiter="\t")
isInstruction(?instruction),
isArrayInstruction(?instruction),
isLoadArrayIndex_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
LoadArrayIndex_Base(?instruction, ?base),
LoadArrayIndex_To(?instruction, ?to) :-
  _LoadArrayIndex(?instruction, ?index, ?to, ?base, ?method).
.decl _ArrayInsnIndex(?instruction:symbol, ?index:symbol)
.input _ArrayInsnIndex(IO="file", filename="ArrayInsnIndex.facts", delimiter="\t")
ArrayInsnIndex(?instruction, ?index) :-
  _ArrayInsnIndex(?instruction, ?index).
.decl _Goto(?instruction:symbol, ?index:number, ?to:number, ?method:symbol)
.input _Goto(IO="file", filename="Goto.facts", delimiter="\t")
isInstruction(?instruction),
isGoto_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
Goto_Target(?instruction, ?to) :-
  _Goto(?instruction, ?index, ?to, ?method).
.decl _If(?instruction:symbol, ?index:number, ?to:number, ?method:symbol)
.input _If(IO="file", filename="If.facts", delimiter="\t")
isInstruction(?instruction),
isIf_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
If_Target(?instruction, ?to) :-
  _If(?instruction, ?index, ?to, ?method).
.decl _TableSwitch(?instruction:symbol, ?index:number, ?key:symbol, ?method:symbol)
.input _TableSwitch(IO="file", filename="TableSwitch.facts", delimiter="\t")
isInstruction(?instruction),
isSwitch_Insn(?instruction),
isTableSwitch_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
Switch_Key(?instruction, ?key) :-
  _TableSwitch(?instruction, ?index, ?key, ?method).
.decl _LookupSwitch(?instruction:symbol, ?index:number, ?key:symbol, ?method:symbol)
.input _LookupSwitch(IO="file", filename="LookupSwitch.facts", delimiter="\t")
isInstruction(?instruction),
isSwitch_Insn(?instruction),
isLookupSwitch_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
Switch_Key(?instruction, ?key) :-
  _LookupSwitch(?instruction, ?index, ?key, ?method).
.decl _TableSwitch_Target(?instruction:symbol, ?value:number, ?target:number)
.input _TableSwitch_Target(IO="file", filename="TableSwitch-Target.facts", delimiter="\t")
Switch_Target(?instruction, ?value, ?target) :-
  _TableSwitch_Target(?instruction, ?value, ?target).
.decl _LookupSwitch_Target(?instruction:symbol, ?value:number, ?target:number)
.input _LookupSwitch_Target(IO="file", filename="LookupSwitch-Target.facts", delimiter="\t")
Switch_Target(?instruction, ?value, ?target) :-
  _LookupSwitch_Target(?instruction, ?value, ?target).
.decl _TableSwitch_DefaultTarget(?instruction:symbol, ?target:number)
.input _TableSwitch_DefaultTarget(IO="file", filename="TableSwitch-Default.facts", delimiter="\t")
Switch_DefaultTarget(?instruction, ?target) :-
    _TableSwitch_DefaultTarget(?instruction, ?target).
.decl _LookupSwitch_DefaultTarget(?instruction:symbol, ?target:number)
.input _LookupSwitch_DefaultTarget(IO="file", filename="LookupSwitch-Default.facts", delimiter="\t")
Switch_DefaultTarget(?instruction, ?target) :-
    _LookupSwitch_DefaultTarget(?instruction, ?target).
.decl _Return(?instruction:symbol, ?index:number, ?var:symbol, ?method:symbol)
.input _Return(IO="file", filename="Return.facts", delimiter="\t")
isInstruction(?instruction),
isReturnInstruction(?instruction),
isReturnNonvoid_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method),
ReturnNonvoid_Var(?instruction, ?var) :-
  _Return(?instruction, ?index, ?var, ?method).
.decl _ReturnVoid(?instruction:symbol, ?index:number, ?method:symbol)
.input _ReturnVoid(IO="file", filename="ReturnVoid.facts", delimiter="\t")
isInstruction(?instruction),
isReturnInstruction(?instruction),
isReturnVoid_Insn(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method) :-
  _ReturnVoid(?instruction, ?index, ?method).
.decl _AssignPhantomInvoke(?instruction:symbol, ?index:number, ?method:symbol)
.input _AssignPhantomInvoke(IO="file", filename="AssignPhantomInvoke.facts", delimiter="\t")
isInstruction(?instruction),
isUnsupportedInstruction(?instruction),
isAssignPhantomInvoke(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method) :-
  _AssignPhantomInvoke(?instruction, ?index, ?method).
.decl _PhantomInvoke(?instruction:symbol, ?index:number, ?method:symbol)
.input _PhantomInvoke(IO="file", filename="PhantomInvoke.facts", delimiter="\t")
isInstruction(?instruction),
isUnsupportedInstruction(?instruction),
isPhantomInvoke(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method) :-
  _PhantomInvoke(?instruction, ?index, ?method).
.decl _BreakpointStmt(?instruction:symbol, ?index:number, ?method:symbol)
.input _BreakpointStmt(IO="file", filename="BreakpointStmt.facts", delimiter="\t")
isInstruction(?instruction),
isUnsupportedInstruction(?instruction),
isBreakpointStmt(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method) :-
  _BreakpointStmt(?instruction, ?index, ?method).
.decl _UnsupportedInstruction(?instruction:symbol, ?index:number, ?method:symbol)
.input _UnsupportedInstruction(IO="file", filename="UnsupportedInstruction.facts", delimiter="\t")
isInstruction(?instruction),
isUnsupportedInstruction(?instruction),
Instruction_Index(?instruction, ?index),
Instruction_Method(?instruction, ?method) :-
  _UnsupportedInstruction(?instruction, ?index, ?method).
.decl _Activity(?id:symbol)
.input _Activity(IO="file", filename="Activity.facts", delimiter="\t")
isType(?id),
Activity(?id) :-
  _Activity(?id).
.decl _Service(?id:symbol)
.input _Service(IO="file", filename="Service.facts", delimiter="\t")
isType(?id),
Service(?id) :-
  _Service(?id).
.decl _ContentProvider(?id:symbol)
.input _ContentProvider(IO="file", filename="ContentProvider.facts", delimiter="\t")
isType(?id),
ContentProvider(?id) :-
  _ContentProvider(?id).
.decl _BroadcastReceiver(?id:symbol)
.input _BroadcastReceiver(IO="file", filename="BroadcastReceiver.facts", delimiter="\t")
isType(?id),
BroadcastReceiver(?id) :-
  _BroadcastReceiver(?id).
.decl _CallbackMethod(?id:symbol)
.input _CallbackMethod(IO="file", filename="CallbackMethod.facts", delimiter="\t")
isMethod(?id),
CallbackMethod(?id) :-
  _CallbackMethod(?id).
.decl _LayoutControl(?id:NumConstant, ?typename:symbol, ?parent:symbol)
.input _LayoutControl(IO="file", filename="LayoutControl.facts", delimiter="\t")
LayoutControl0(?id, ?typename, ?parent) :-
  _LayoutControl(?id, ?typename, ?parent).
.decl _FieldInitialValue(?fld:symbol, ?valueString:symbol)
.input _FieldInitialValue(IO="file", filename="FieldInitialValue.facts", delimiter="\t")
FieldInitialValue(?fld, ?valueString) :-
  _FieldInitialValue(?fld, ?valueString).
isModifier(?x), Modifier_abstract(?x) :- ?x = "abstract".
isModifier(?x), Modifier_public(?x) :- ?x = "public".
isModifier(?x), Modifier_private(?x) :- ?x = "private".
isModifier(?x), Modifier_final(?x) :- ?x = "final".
isModifier(?x), Modifier_static(?x) :- ?x = "static".
isType(?t), isPrimitiveType(?t), Type_boolean(?t) :- ?t = "boolean".
isType(?t), isPrimitiveType(?t), Type_byte(?t) :- ?t = "byte".
isType(?t), isPrimitiveType(?t), Type_char(?t) :- ?t = "char".
isType(?t), isPrimitiveType(?t), Type_short(?t) :- ?t = "short".
isType(?t), isPrimitiveType(?t), Type_int(?t) :- ?t = "int".
isType(?t), isPrimitiveType(?t), Type_long(?t) :- ?t = "long".
isType(?t), isPrimitiveType(?t), Type_float(?t) :- ?t = "float".
isType(?t), isPrimitiveType(?t), Type_double(?t) :- ?t = "double".
isType(?t), isPrimitiveType(?t), Type_void(?t) :- ?t = "void".
isType(?t), isReferenceType(?t), isNullType(?t), Type_null(?t) :- ?t = "null_type".
isType(?t), isReferenceType(?t), isClassType(?t), Type_object(?t) :- ?t = "java.lang.Object".
.decl _Dacapo(?id:symbol, ?method:symbol)
.input _Dacapo(IO="file", filename="Dacapo.facts", delimiter="\t")
Throw(?insn, ?var) :-
  isThrow_Insn(?insn),
  Throw_Var(?insn, ?var).
LoadInstanceField(?base, ?sig, ?to, ?inmethod) :-
  isLoadInstanceField_Insn(?insn),
  Instruction_Method(?insn, ?inmethod),
  LoadInstanceField_Base(?insn, ?base),
  FieldInstruction_Signature(?insn, ?sig),
  LoadInstanceField_To(?insn, ?to).
StoreInstanceField(?from, ?base, ?sig, ?inmethod) :-
  isStoreInstanceField_Insn(?insn),
  Instruction_Method(?insn, ?inmethod),
  StoreInstanceField_From(?insn, ?from),
  StoreInstanceField_Base(?insn, ?base),
  FieldInstruction_Signature(?insn, ?sig).
LoadStaticField(?sig, ?to, ?inmethod) :-
  isLoadStaticField_Insn(?insn),
  Instruction_Method(?insn, ?inmethod),
  FieldInstruction_Signature(?insn, ?sig),
  LoadStaticField_To(?insn, ?to).
StoreStaticField(?from, ?sig, ?inmethod) :-
  isStoreStaticField_Insn(?insn),
  Instruction_Method(?insn, ?inmethod),
  StoreStaticField_From(?insn, ?from),
  FieldInstruction_Signature(?insn, ?sig).
LoadArrayIndex(?base, ?to, ?inmethod) :-
  isLoadArrayIndex_Insn(?insn),
  Instruction_Method(?insn, ?inmethod),
  LoadArrayIndex_Base(?insn, ?base),
  LoadArrayIndex_To(?insn, ?to).
StoreArrayIndex(?from, ?base, ?inmethod) :-
  isStoreArrayIndex_Insn(?insn),
  Instruction_Method(?insn, ?inmethod),
  StoreArrayIndex_From(?insn, ?from),
  StoreArrayIndex_Base(?insn, ?base).
AssignCast(?type, ?from, ?to, ?inmethod) :-
  isAssignCast_Insn(?insn),
  Instruction_Method(?insn, ?inmethod),
  AssignCast_From(?insn, ?from),
  AssignInstruction_To(?insn, ?to),
  AssignCast_Type(?insn, ?type).
AssignLocal(?from, ?to, ?inmethod) :-
  isAssignLocal_Insn(?insn),
  AssignInstruction_To(?insn, ?to),
  Instruction_Method(?insn, ?inmethod),
  AssignLocal_From(?insn, ?from).
AssignNull(?to, ?inmethod) :-
  isAssignNull_Insn(?insn),
  AssignInstruction_To(?insn, ?to),
  Instruction_Method(?insn, ?inmethod).
AssignHeapAllocation(?heap, ?to, ?inmethod) :-
  isAssignHeapAllocation_Insn(?insn),
  Instruction_Method(?insn, ?inmethod),
  AssignHeapAllocation_Heap(?insn, ?heap),
  AssignInstruction_To(?insn, ?to).
ReturnVar(?var, ?method) :-
  isReturnNonvoid_Insn(?insn),
  Instruction_Method(?insn, ?method),
  ReturnNonvoid_Var(?insn, ?var).
ReturnVar(?var, ?method) :-
  NativeReturnVar(?var, ?method).
VirtualMethodInvocation(?invocation, ?signature, ?inmethod) :-
  isVirtualMethodInvocation_Insn(?invocation),
  Instruction_Method(?invocation, ?inmethod),
  MethodInvocation_Method(?invocation, ?signature).
StaticMethodInvocation(?invocation, ?signature, ?inmethod) :-
  isStaticMethodInvocation_Insn(?invocation),
  Instruction_Method(?invocation, ?inmethod),
  MethodInvocation_Method(?invocation, ?signature).
isHeapAllocation(?null), HeapAllocation_Type(?null, ?type),
HeapAllocation_Null(?null) :-
  ?null = "<<null pseudo heap>>",
  Type_null(?type).
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type),
MainMethodArgArray(?heap) :-
  ?heap = "<<main method array>>",
  ?type = "java.lang.String[]".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type),
MainMethodArgArrayContent(?heap) :-
  ?heap = "<<main method array content>>",
  ?type = "java.lang.String".
ApplicationMethod(?method) :-
  Method_DeclaringType(?method, ?class),
  ApplicationClass(?class).
ApplicationVar(?var) :-
  Var_DeclaringMethod(?var, ?method),
  ApplicationMethod(?method).
ConcreteClass(?class) :-
  isClassType(?class),
  !ClassModifier("abstract", ?class).
VirtualMethodInvocation_SimpleName(?invocation, ?simplename),
VirtualMethodInvocation_Descriptor(?invocation, ?descriptor) :-
  isVirtualMethodInvocation_Insn(?invocation),
  MethodInvocation_Method(?invocation, ?signature),
  Method_SimpleName(?signature, ?simplename),
  Method_Descriptor(?signature, ?descriptor).
StaticMethodInvocation_SimpleName(?invocation, ?simplename),
StaticMethodInvocation_Descriptor(?invocation, ?descriptor) :-
  isStaticMethodInvocation_Insn(?invocation),
  MethodInvocation_Method(?invocation, ?signature),
  Method_SimpleName(?signature, ?simplename),
  Method_Descriptor(?signature, ?descriptor).
SpecialMethodInvocation_SimpleName(?invocation, ?simplename),
SpecialMethodInvocation_Descriptor(?invocation, ?descriptor) :-
  isSpecialMethodInvocation_Insn(?invocation),
  MethodInvocation_Method(?invocation, ?signature),
  Method_SimpleName(?signature, ?simplename),
  Method_Descriptor(?signature, ?descriptor).
LayoutControl(?id, ?type, ?parent) :-
  LayoutControl0(?id, ?type, ?parent),
  isType(?type).
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap = "java.io.FileSystem.getFileSystem/new java.io.UnixFileSystem",
   ?type = "java.io.UnixFileSystem".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="java.io.UnixFileSystem.list/new java.lang.String[]",
   ?type = "java.lang.String[]".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="java.io.UnixFileSystem.list/new java.lang.String",
   ?type = "java.lang.String".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   (?heap ="<<string-constant>>";
    ?heap ="<<reflection-string-constant>>"),
   ?type = "java.lang.String".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="<<string-buffer>>",
   ?type = "java.lang.StringBuffer".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="<<string-builder>>",
   ?type = "java.lang.StringBuilder".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   (?heap ="<<system-thread-group>>";
    ?heap ="<<main-thread-group>>"),
   ?type = "java.lang.ThreadGroup".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="<<main-thread>>",
   ?type = "java.lang.Thread".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="<<initial-context>>",
   ?type = "java.lang.Object".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="<<jvm-startup-context>>",
   ?type = "java.lang.Object".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="<<jvm-startup-hcontext>>",
   ?type = "java.lang.Object".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="<<clinit-context>>",
   ?type = "java.lang.Object".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="<<immutable-context>>",
   ?type = "java.lang.Object".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="<<immutable-hcontext>>",
   ?type = "java.lang.Object".
isHeapAllocation(?heap), HeapAllocation_Type(?heap, ?type) :-
   ?heap ="<<immutable>>",
   ?type = "java.lang.Object".
.output CallGraphEdge()
.output VarPointsTo()
.output Stats_Metrics
.decl Tamiflex_ReflectionData(?classStr:symbol, ?methodStr:symbol, ?mapped:symbol, ?inClassStr:symbol,
                              ?inMethodStr:symbol, ?lineNumber:number)
.decl Tamiflex_ReflectionMap(?mapped:symbol, ?invocation:MethodInvocation)
.decl _Tamiflex_ToDoopFormat(?orig:symbol, ?formatted:symbol)
_Tamiflex_ToDoopFormat("Class", "java.lang.Class").
_Tamiflex_ToDoopFormat("Constructor", "java.lang.reflect.Constructor").
_Tamiflex_ToDoopFormat("Field", "java.lang.reflect.Field").
_Tamiflex_ToDoopFormat("Method", "java.lang.reflect.Method").
_Tamiflex_ToDoopFormat("Array", "java.lang.reflect.Array").
_Tamiflex_ToDoopFormat("get*", "get").
_Tamiflex_ToDoopFormat("set*", "set").
.decl _Tamiflex_ReflectionData(?classStr:symbol, ?methodStr:symbol, ?mapped:symbol, ?inClassStr:symbol,
                               ?inMethodStr:symbol, ?lineNumber:number)
.input _Tamiflex_ReflectionData(IO="file", filename="Tamiflex.facts", delimiter="\t")
Tamiflex_ReflectionData(?classStr, ?methodStr, ?mapped, ?inClassStr, ?inMethodStr, ?lineNumber) :-
  _Tamiflex_ReflectionData(?classStr0, ?methodStr0, ?mapped, ?inClassStr, ?inMethodStr, ?lineNumber),
  _Tamiflex_ToDoopFormat(?classStr0, ?classStr),
  (_Tamiflex_ToDoopFormat(?methodStr0, ?methodStr) ;
   ?methodStr0 = ?methodStr).
Tamiflex_ReflectionMap(?mapped, ?invocation) :-
   Tamiflex_ReflectionData(?class, ?methodStr, ?mapped, ?inClass, ?inMethodStr, ?line),
   isClassType(?class),
   Method_SimpleName(?method, ?methodStr),
   Method_DeclaringType(?method, ?class),
   isClassType(?inClass),
   Method_SimpleName(?inMethod, ?inMethodStr),
   Method_DeclaringType(?inMethod, ?inClass),
   (
     ?line > 0, MethodInvocation_Line(?invocation, ?line)
   ;
     ?line = 0
   ),
   MethodInvocation_Method(?invocation, ?method),
   Instruction_Method(?invocation, ?inMethod).
.decl AllocatedObjectSupportsFinalize(?heap:HeapAllocation, ?inmethod:Method)
.decl OverridesFinalize(?class:Type)
.decl MethodLookup(?simplename:symbol, ?descriptor:MethodDescriptor, ?type:Type, ?method:Method)
.decl MethodImplemented(?simplename:symbol, ?descriptor:MethodDescriptor, ?type:Type, ?method:Method)
.decl ResolveInvocation(?type:Type, ?invocation:MethodInvocation, ?tomethod:Method)
.decl OverridableMethod(?type:Type, ?method:Method)
.decl ClassConstructor(?method:Method, ?type:Type)
.decl DirectSubclass(?a:Type, ?c:Type)
.decl Subclass(?c:Type, ?a:Type)
.decl Superclass(?c:Type, ?a:Type)
.decl Superinterface(?k:Type, ?c:Type)
.decl SubtypeOf(?subtype:Type, ?type:Type)
.decl SupertypeOf(?supertype:Type, ?type:Type)
.decl Unsubclassable(?type:Type)
.decl Subclassable(?type:Type)
.decl MainMethodDeclaration(?method:Method)
AllocatedObjectSupportsFinalize(?heap, ?inmethod) :-
    AssignHeapAllocation(?heap, _, ?inmethod),
    HeapAllocation_Type(?heap, ?class),
    OverridesFinalize(?class).
OverridesFinalize(?class) :-
    MethodLookup("finalize", "void()", ?class, ?method),
    ?method != "<java.lang.Object: void finalize()>".
MethodLookup(?simplename, ?descriptor, ?type, ?method) :-
    MethodImplemented(?simplename, ?descriptor, ?type, ?method).
MethodLookup(?simplename, ?descriptor, ?type, ?method) :-
    DirectSuperclass(?type, ?supertype),
    MethodLookup(?simplename, ?descriptor, ?supertype, ?method),
    ! MethodImplemented(?simplename, ?descriptor, ?type, _).
MethodLookup(?simplename, ?descriptor, ?arraytype, ?method) :-
    isArrayType(?arraytype),
    isType(?objectType),
    MethodImplemented(?simplename, ?descriptor, ?objectType, ?method),
    ?objectType = "java.lang.Object".
MethodImplemented(?simplename, ?descriptor, ?type, ?method) :-
    Method_SimpleName(?method, ?simplename),
    Method_Descriptor(?method, ?descriptor),
    Method_DeclaringType(?method, ?type),
    ! Method_Modifier("abstract", ?method).
ResolveInvocation(?type, ?invocation, ?tomethod) :-
    VirtualMethodInvocation_SimpleName(?invocation, ?simplename),
    VirtualMethodInvocation_Descriptor(?invocation, ?descriptor),
    VirtualMethodInvocation_Base(?invocation, ?base),
    Var_Type(?base, ?basetype),
    SubtypeOf(?type, ?basetype),
    MethodLookup(?simplename, ?descriptor, ?type, ?tomethod).
OverridableMethod(?type, ?method) :-
    MethodLookup(_, _, ?type, ?method),
    ! Method_Modifier("static", ?method),
    ! Method_Modifier("final", ?method),
    Method_Modifier("public", ?method),
    Subclassable(?type).
OverridableMethod(?type, ?method) :-
    MethodLookup(_, _, ?type, ?method),
    ! Method_Modifier("static", ?method),
    ! Method_Modifier("final", ?method),
    Method_Modifier("protected", ?method),
    Subclassable(?type).
ClassConstructor(method, type) :-
    MethodLookup(_, _, type, method),
    isMethod(method),
    match(".*<init>.*", method).
DirectSubclass(?a, ?c) :-
    DirectSuperclass(?a, ?c).
Subclass(?c, ?a) :-
    DirectSubclass(?a, ?c).
Subclass(?c, ?a) :-
    Subclass(?b, ?a),
    DirectSubclass(?b, ?c).
Superclass(?c, ?a) :-
    Subclass(?a, ?c).
Superinterface(?k, ?c) :-
    DirectSuperinterface(?c, ?k).
Superinterface(?k, ?c) :-
    DirectSuperinterface(?c, ?j),
    Superinterface(?k, ?j).
Superinterface(?k, ?c) :-
    DirectSuperclass(?c, ?super),
    Superinterface(?k, ?super).
SupertypeOf(?s, ?t) :-
    SubtypeOf(?t, ?s).
SubtypeOf(?s, ?s) :-
    isClassType(?s).
SubtypeOf(?s, ?t) :-
    Subclass(?t, ?s).
SubtypeOf(?s, ?t) :-
    isClassType(?s),
    Superinterface(?t, ?s).
SubtypeOf(?s, ?t) :-
    isInterfaceType(?s),
    isType(?t),
    ?t = "java.lang.Object".
SubtypeOf(?s, ?s) :-
    isInterfaceType(?s).
SubtypeOf(?s, ?t) :-
    isInterfaceType(?s),
    Superinterface(?t, ?s).
SubtypeOf(?s, ?t) :-
    isArrayType(?s),
    isType(?t),
    ?t = "java.lang.Object".
SubtypeOf(?s, ?t) :-
    isArrayType(?s),
    isArrayType(?t),
    ComponentType(?s, ?sc),
    ComponentType(?t, ?sc),
    isPrimitiveType(?sc).
SubtypeOf(?s, ?t) :-
    ComponentType(?s, ?sc),
    ComponentType(?t, ?tc),
    isReferenceType(?sc),
    isReferenceType(?tc),
    SubtypeOf(?sc, ?tc).
SubtypeOf(?s, ?t) :-
    isArrayType(?s),
    isInterfaceType(?t),
    isType(?t),
    ?t = "java.lang.Cloneable".
SubtypeOf(?s, ?t) :-
    isArrayType(?s),
    isInterfaceType(?t),
    isType(?t),
    ?t = "java.io.Serializable".
SubtypeOf(?s, ?t) :-
    Type_null(?s),
    isReferenceType(?t),
    ?t != ?s.
SubtypeOf(?s, ?t) :-
    Type_float(?s),
    Type_double(?t).
SubtypeOf(?s, ?t) :-
    Type_long(?s),
    Type_float(?t).
SubtypeOf(?s, ?t) :-
    Type_int(?s),
    Type_long(?t).
SubtypeOf(?s, ?t) :-
    Type_char(?s),
    Type_int(?t).
SubtypeOf(?s, ?t) :-
    Type_short(?s),
    Type_int(?t).
SubtypeOf(?s, ?t) :-
    Type_byte(?s),
    Type_short(?t).
SubtypeOf(?t, ?t) :-
    isType(?t).
Unsubclassable("java.lang.ClassLoader").
Unsubclassable("java.lang.SecurityManager").
Subclassable(?type) :-
    ClassModifier("public", ?type),
    ! ClassModifier("final", ?type),
    ClassConstructor(?method, ?type),
    Method_Modifier("public", ?method),
    ! Unsubclassable(?type).
Subclassable(?type) :-
    ClassModifier("public", ?type),
    ! ClassModifier("final", ?type),
    ClassConstructor(?method, ?type),
    Method_Modifier("protected", ?method),
    ! Unsubclassable(?type).
MainMethodDeclaration(?method) :-
   MainClass(?type),
   Method_DeclaringType(?method, ?type),
   Method_SimpleName(?method, "main"),
   Method_Descriptor(?method, "void(java.lang.String[])"),
   Method_Modifier("public", ?method),
   Method_Modifier("static", ?method).
.decl AndroidAppComponent(?type:symbol)
.decl ReifiedComponent(?type:Type, ?value:Value)
.decl ReifiedLayoutControl(?type:Type, ?id:NumConstant, ?value:Value)
.decl ImplicitlyInstantiatedLibraryType(?type:Type)
.decl AndroidLibraryType(?type:Type)
.decl AndroidApplicationClass(?class:ClassType)
.decl AndroidViewType(?type:Type)
.decl AndroidLibraryListenerType(?type:Type)
.decl ListenerType(?type:Type)
.decl AndroidApplicationListenerClass(?class:ClassType)
.decl MethodDeclaredOrInherited(?meth:Method, ?class:ClassType)
.decl PublicMethodOfComponent(?meth:Method)
.decl ProtectedMethodOfComponent(?meth:Method)
.decl AppMethodOverridesAndroidLibraryMethod(?meth:Method)
.decl OverridingProtectedMethodOfComponent(?meth:Method)
.decl ForcedReachableAndroidContext(?ctx:Context, ?meth:Method)
.decl PublicOnMethodOfLayoutControl(?meth:Method)
.decl ProtectedOnMethodOfLayoutControl(?meth:Method)
.decl OverridingProtectedOnMethodOfLayoutControl(?meth:Method)
.decl ReachableApplicationObjectOfType(?hctx:HContext, ?value:Value, ?type:Type)
.decl ApplicationObjectFlowingToLibrary(?hctx:HContext, ?value:Value, ?ofType:Type)
.decl PublicOnMethodOfReachableListener(?meth:Method)
.decl LibraryReachableAppListener(?type:ClassType)
.decl LibraryReachableAppListenerType(?type:Type)
.decl ProtectedOnMethodOfReachableListener(?meth:Method)
.decl OverridingProtectedOnMethodOfReachableListener(?meth:Method)
.decl ReifiedAndroidObjectValue(?value:Value, ?type:Type)
.decl ReifiedLibraryObject(?type:Type, ?value:Value)
.decl FormalOfForcedReachableContext(?ctx:Context, ?formal:Var, ?formalType:Type)
.decl ApplicationObjectFlowingToLibraryStaticType(?hctx:HContext, ?value:Value, ?possibleType:Type)
.decl ViewRetrievalByArg0MethodInvocation(?invo:MethodInvocation)
.decl VarsAtInvocationRetrievingView(?ret:Var, ?var:Var)
.decl ViewObjectValueFromId(?viewValue:Value, ?numId:NumConstant)
.decl ClassInitializer(?type:Type, ?method:Method)
.decl InitializedClass(?classOrInterface:Type)
.decl Instruction_Throws(?hctx:HContext, ?value:Value, ?ctx:Context, ?insn:Instruction)
.decl ExceptionHandler_InRange(?handler:ExceptionHandler, ?instruction:Instruction)
.decl ExceptionHandler_Before(?before:ExceptionHandler, ?handler:ExceptionHandler)
.decl ThrowPointsTo(?hctx:HContext, ?value:Value, ?ctx:Context, ?method:Method)
.decl ExceptionHandler_SameInsn_Repr(?insn:Instruction, ?repr:ExceptionHandler)
.decl ExceptionHandler_SameInsn_PartialOrder(?h1:ExceptionHandler, ?h2:ExceptionHandler, ?insn:Instruction)
.decl ExceptionHandler_SameBlock_Repr(?handler:ExceptionHandler, ?repr:ExceptionHandler)
.decl ExceptionHandler_SameBlock_PartialOrder(?repr:ExceptionHandler, ?handler:ExceptionHandler)
.decl ExceptionHandler_TypeIsCaught(?type:Type, ?block:ExceptionHandler)
.decl ExceptionHandler_Impossible(?type:Type, ?h2:ExceptionHandler, ?insn:Instruction)
.decl ImplicitReachable(?sig:Method)
.decl RunningThread(?hctx:HContext, ?value:Value)
.decl ReachableCurrentThreadInvocation(?callerCtx:Context, ?local:Var)
.decl FakeInvocation_RegisterFinalize0(?heap:HeapAllocation, ?invo:MethodInvocation)
.decl FakeInvocation_RegisterFinalize(?value:Value, ?invo:MethodInvocation)
.type Value = HeapAllocation | NumConstant
.decl isValue(?value:Value)
.decl Value_isHeap(?value:Value)
.decl Value_isMock(?value:Value)
.decl Value_Num(?value:Value, ?const:NumConstant)
.decl Value_isNonHeap(?value:Value)
.decl NotSpecialObject(?value:Value)
.decl Value_Type(?value:Value, ?type:Type)
.decl Value_DeclaringType(?value:Value, ?type:Type)
.decl Value_Null(?null:Value)
.decl isContext(?ctx:Context)
.decl isHContext(?hctx:HContext)
.decl isImmutableContext(?ctx:Context)
.decl isInitialContext(?ctx:Context)
.decl isJVMStartupContext(?ctx:Context)
.decl isClinitContext(?ctx:Context)
.decl isImmutableHContext(?hctx:HContext)
.decl isJVMStartupHContext(?hctx:HContext)
.decl ImmutableContextFromHContext(?hctx:HContext, ?ctx:Context)
.decl ImmutableHContextFromContext(?ctx:Context, ?hctx:HContext)
.decl ImmutableContextFromContext(?ctx1:Context, ?ctx2:Context)
.type ContextComponent
.decl isContextComponent(?comp:ContextComponent)
.decl ContextComponent_MethodInvocation(?invo:MethodInvocation, ?comp:ContextComponent)
.decl ContextComponent_Value(?value:Value, ?comp:ContextComponent)
.decl VarPointsTo(?hctx:HContext, ?value:Value, ?ctx:Context, ?var:Var)
.decl InstanceFieldPointsTo(?hctx:HContext, ?value:Value, ?sig:Field, ?basehctx:HContext, ?basevalue:Value)
.decl StaticFieldPointsTo(?hctx:HContext, ?value:Value, ?sig:Field)
.decl ArrayIndexPointsTo(?hctx:HContext, ?value:Value, ?basehctx:HContext, ?basevalue:Value)
.decl Assign(?type:Type, ?toCtx:Context, ?to:Var, ?fromCtx:Context, ?from:Var)
.decl CallGraphEdge(?callerCtx:Context, ?invocation:MethodInvocation, ?calleeCtx:Context, ?method:Method)
.decl Reachable(?method:Method)
.output Reachable(IO="file",filename="Reachable.csv",delimiter="\t")
.decl ReachableContext(?ctx:Context, ?method:Method)
.decl OptLoadInstanceField(?to:Var, ?signature:Field, ?base:Var)
.decl OptLoadStaticField(?ctx:Context, ?to:Var, ?signature:Field)
.decl OptStoreStaticField(?signature:Field, ?from:Var)
.decl OptStoreInstanceField(?from:Var, ?signature:Field, ?base:Var)
.decl OptInterproceduralAssign(?toCtx:Context, ?to:Var, ?fromCtx:Context, ?from:Var)
.decl ReachableSpecialMethodInvocation(?invocation:MethodInvocation, ?base:Var)
.decl ReachableVirtualMethodInvocation(?invocation:MethodInvocation, ?base:Var)
.decl OptLoadArrayIndex(?to:Var, ?base:Var)
.decl OptStoreArrayIndex(?from:Var, ?base:Var)
.decl OptStoreIntoArray(?hctx:HContext, ?basehctx:HContext, ?basevalue:Value, ?value:Value)
.decl LoadHeapInstanceField(?ctx:Context, ?to:Var, ?sig:Field, ?basehctx:HContext, ?basevalue:Value)
.decl StoreHeapInstanceField(?sig:Field, ?basehctx:HContext, ?basevalue:Value, ?ctx:Context, ?from:Var)
.decl LoadHeapArrayIndex(?ctx:Context, ?to:Var, ?basehctx:HContext, ?basevalue:Value)
.decl StoreHeapArrayIndex(?basehctx:HContext, ?basevalue:Value, ?ctx:Context, ?from:Var)
.decl AssignNormalHeapAllocation(?heap:HeapAllocation, ?var:Var, ?inmethod:Method)
.decl AssignAuxiliaryHeapAllocation(?heap:HeapAllocation, ?var:Var, ?inmethod:Method)
.decl AssignContextInsensitiveHeapAllocation(?heap:HeapAllocation, ?var:Var, ?inmethod:Method)
.decl SystemThreadGroup(?hctx:HContext, ?value:Value)
.decl MainThreadGroup(?hctx:HContext, ?value:Value)
.decl MainThread(?hctx:HContext, ?value:Value)
.decl SiteToRefine(?invocation:MethodInvocation)
.decl TempSiteToRefine(?invocation:MethodInvocation)
.decl ValueToRefine(?value:Value)
.decl TempValueToRefine(?value:Value)
.decl NegativeSiteFilter(?v:symbol)
.decl TempNegativeSiteFilter(?v:symbol)
.decl NegativeObjectFilter(?v:symbol)
.decl TempNegativeObjectFilter(?v:symbol)
Value_DeclaringType(?value, "java.lang.System") :-
   ?value = "<<string-constant>>",
   isValue(?value) ;
   ?value = "<<reflection-string-constant>>",
   isValue(?value) ;
   ?value = "<<string-buffer>>",
   isValue(?value) ;
   ?value = "<<string-builder>>",
   isValue(?value) ;
   ?value = "<<initial-context>>",
   isValue(?value) ;
   ?value = "<<jvm-startup-context>>",
   isValue(?value) ;
   ?value = "<<jvm-startup-hcontext>>",
   isValue(?value) ;
   ?value = "<<clinit-context>>",
   isValue(?value) ;
   ?value = "<<system-thread-group>>",
   isValue(?value) ;
   ?value = "<<main-thread-group>>",
   isValue(?value) ;
   ?value = "<<main-thread>>",
   isValue(?value) ;
   ?value = "<<immutable-context>>",
   isValue(?value) ;
   ?value = "<<immutable-hcontext>>",
   isValue(?value) ;
   ?value = "<<immutable>>",
   isValue(?value).
FakeInvocation_RegisterFinalize0(?val2, cat("<register-finalize ", cat(?val1, cat( "/", cat(?val2, "  >"))))),
isInstruction(cat("<register-finalize ", cat(?val1, cat( "/", cat(?val2, "  >"))))), isMethodInvocation(cat("<register-finalize ", cat(?val1, cat( "/", cat(?val2, "  >"))))) :-
    AllocatedObjectSupportsFinalize(?val2, ?val1),
    isMethod(?val1),
    isHeapAllocation(?val2).
ImmutableContextFromHContext(?hctx, ?ctx) :-
  isImmutableContext(?ctx),
  isHContext(?hctx).
ImmutableHContextFromContext(?ctx, ?hctx) :-
  isImmutableHContext(?hctx),
  isContext(?ctx).
ImmutableContextFromContext(?ctx1, ?ctx2) :-
  isImmutableContext(?ctx2),
  isContext(?ctx1).
AndroidAppComponent(?type) :-
  Activity(?type);
  Service(?type);
  BroadcastReceiver(?type);
  ContentProvider(?type).
Value_isMock(cat("<android component object ", cat(?type, ">"))), isValue(cat("<android component object ", cat(?type, ">"))), Value_Type(cat("<android component object ", cat(?type, ">")), ?type),
ReifiedComponent(?type, cat("<android component object ", cat(?type, ">"))) :-
  AndroidAppComponent(?type),
  isType(?type).
Value_isMock(cat("<layout control object ", cat(?id, cat(" of type ", cat(?type, ">"))))), isValue(cat("<layout control object ", cat(?id, cat(" of type ", cat(?type, ">"))))), Value_Type(cat("<layout control object ", cat(?id, cat(" of type ", cat(?type, ">")))), ?type),
ReifiedLayoutControl(?type, ?id, cat("<layout control object ", cat(?id, cat(" of type ", cat(?type, ">"))))) :-
  LayoutControl(?id, ?type, _),
  isType(?type).
ImplicitlyInstantiatedLibraryType(?type) :-
  (?type = "android.content.Intent";
   ?type = "android.os.Bundle"),
  isType(?type).
Value_isMock(cat("<android library object ", cat(?type, ">"))), isValue(cat("<android library object ", cat(?type, ">"))), Value_Type(cat("<android library object ", cat(?type, ">")), ?type),
ReifiedLibraryObject(?type, cat("<android library object ", cat(?type, ">"))) :-
  ImplicitlyInstantiatedLibraryType(?type),
  isType(?type).
AndroidLibraryType(?type) :-
  isType(?type),
  match("^android.*", ?type).
AndroidApplicationClass(?class) :-
  ApplicationClass(?class),
  !AndroidLibraryType(?class).
AndroidViewType(?type) :-
  SubtypeOf(?type, ?supertype),
  (?superType = "android.view.View",
   isType(?supertype);
   ?superType = "android.view.ViewGroup",
   isType(?supertype)).
AndroidLibraryListenerType(?type) :-
  AndroidLibraryType(?type),
  isType(?type),
  (contains("Listener", ?type);
   contains("Callback", ?type)).
ListenerType(?type) :-
  AndroidLibraryListenerType(?listenerType),
  SubtypeOf(?type, ?listenerType).
AndroidApplicationListenerClass(?class) :-
  AndroidApplicationClass(?class),
  ListenerType(?class).
MethodDeclaredOrInherited(?meth, ?class) :-
  isClassType(?class),
  Method_DeclaringType(?meth, ?class).
MethodDeclaredOrInherited(?meth, ?class) :-
  MethodDeclaredOrInherited(?meth, ?superClass),
  Method_Descriptor(?meth, ?descriptor),
  Method_SimpleName(?meth, ?simplename),
  DirectSuperclass(?class, ?superClass),
  MethodLookup(?simplename, ?descriptor, ?class, ?meth).
PublicMethodOfComponent(?meth) :-
  AndroidAppComponent(?type),
  MethodDeclaredOrInherited(?meth, ?type),
  Method_Modifier("public", ?meth).
ProtectedMethodOfComponent(?meth) :-
  AndroidAppComponent(?type),
  MethodDeclaredOrInherited(?meth, ?type),
  Method_Modifier("protected", ?meth).
AppMethodOverridesAndroidLibraryMethod(?meth) :-
  Method_DeclaringType(?meth, ?type),
  AndroidApplicationClass(?type),
  Method_Descriptor(?meth, ?descriptor),
  Method_SimpleName(?meth, ?simplename),
  SupertypeOf(?libraryType, ?type),
  AndroidLibraryType(?libraryType),
  MethodLookup(?simplename, ?descriptor, ?libraryType, _).
OverridingProtectedMethodOfComponent(?meth) :-
  ProtectedMethodOfComponent(?meth),
  AppMethodOverridesAndroidLibraryMethod(?meth).
ForcedReachableAndroidContext(?ctx, ?meth),
ReachableContext(?ctx, ?meth) :-
  (PublicMethodOfComponent(?meth);
   OverridingProtectedMethodOfComponent(?meth);
   CallbackMethod(?meth)),
  isImmutableContext(?ctx).
PublicOnMethodOfLayoutControl(?meth) :-
  MethodDeclaredOrInherited(?meth, ?type),
  LayoutControl(_, ?type, _),
  Method_SimpleName(?meth, ?simplename),
  match("^on.*", ?simplename),
  Method_Modifier("public", ?meth).
ProtectedOnMethodOfLayoutControl(?meth) :-
  MethodDeclaredOrInherited(?meth, ?type),
  LayoutControl(_, ?type, _),
  Method_SimpleName(?meth, ?simplename),
  match("^on.*", ?simplename),
  Method_Modifier("protected", ?meth).
OverridingProtectedOnMethodOfLayoutControl(?meth) :-
  ProtectedOnMethodOfLayoutControl(?meth),
  AppMethodOverridesAndroidLibraryMethod(?meth).
ForcedReachableAndroidContext(?ctx, ?meth),
ReachableContext(?ctx, ?meth) :-
  (PublicOnMethodOfLayoutControl(?meth);
   OverridingProtectedOnMethodOfLayoutControl(?meth)),
  isImmutableContext(?ctx).
ReachableApplicationObjectOfType(?hctx, ?value, ?ofType) :-
  ApplicationClass(?ofType),
  Value_Type(?value, ?ofType),
  VarPointsTo(?hctx, ?value, _, _).
ApplicationObjectFlowingToLibrary(?hctx, ?value, ?ofType),
LibraryReachableAppListenerType(?type) :-
  ReachableApplicationObjectOfType(?hctx, ?value, ?ofType),
  AndroidApplicationListenerClass(?type).
PublicOnMethodOfReachableListener(?meth) :-
  MethodDeclaredOrInherited(?meth, ?class),
  LibraryReachableAppListenerType(?class),
  Method_SimpleName(?meth, ?simplename),
  match("^on.*", ?simplename),
  Method_Modifier("public", ?meth).
ProtectedOnMethodOfReachableListener(?meth) :-
  MethodDeclaredOrInherited(?meth, ?class),
  LibraryReachableAppListenerType(?class),
  Method_SimpleName(?meth, ?simplename),
  match("^on.*", ?simplename),
  Method_Modifier("protected", ?meth).
OverridingProtectedOnMethodOfReachableListener(?meth) :-
  ProtectedOnMethodOfReachableListener(?meth),
  AppMethodOverridesAndroidLibraryMethod(?meth).
ForcedReachableAndroidContext(?ctx, ?meth),
ReachableContext(?ctx, ?meth) :-
  (PublicOnMethodOfReachableListener(?meth);
   OverridingProtectedOnMethodOfReachableListener(?meth)),
  isImmutableContext(?ctx).
ReifiedAndroidObjectValue(?value, ?type) :-
  ReifiedComponent(?type, ?value);
  ReifiedLayoutControl(?type, _, ?value);
  ReifiedLibraryObject(?type, ?value).
VarPointsTo(?hctx, ?value, ?ctx, ?this) :-
  ForcedReachableAndroidContext(?ctx, ?meth),
  ImmutableHContextFromContext(?ctx, ?hctx),
  Method_DeclaringType(?meth, ?class),
  ReifiedAndroidObjectValue(?value, ?class),
  ThisVar(?meth, ?this).
  .plan 1:(2,1,3,4,5)
VarPointsTo(?hctx, ?value, ?ctx, ?this) :-
  ForcedReachableAndroidContext(?ctx, ?meth),
  Method_DeclaringType(?meth, ?ofType),
  ApplicationObjectFlowingToLibrary(?hctx, ?value, ?ofType),
  ThisVar(?meth, ?this).
  .plan 1:(3,2,1,4)
FormalOfForcedReachableContext(?ctx, ?formal, ?formalType) :-
  ForcedReachableAndroidContext(?ctx, ?meth),
  FormalParam(_, ?meth, ?formal),
  Var_Type(?formal, ?formalType).
VarPointsTo(?hctx, ?value, ?ctx, ?formal) :-
  FormalOfForcedReachableContext(?ctx, ?formal, ?formalType),
  ImmutableHContextFromContext(?ctx, ?hctx),
  SubtypeOf(?type, ?formalType),
  ReifiedAndroidObjectValue(?value, ?type).
  .plan 1:(2,1,3,4)
ApplicationObjectFlowingToLibraryStaticType(?hctx, ?value, ?possibleType) :-
  ApplicationObjectFlowingToLibrary(?hctx, ?value, ?ofType),
  SupertypeOf(?possibleType, ?ofType).
VarPointsTo(?hctx, ?value, ?ctx, ?formal) :-
  FormalOfForcedReachableContext(?ctx, ?formal, ?formalType),
  ApplicationObjectFlowingToLibraryStaticType(?hctx, ?value, ?formalType).
  .plan 1:(2,1)
ViewRetrievalByArg0MethodInvocation(?invo) :-
  (?calleeName = "inflate";
   ?calleeName = "getView";
   ?calleeName = "findViewById"),
  Method_SimpleName(?method, ?calleeName),
  ?retType = "android.view.View",
  Method_ReturnType(?method, ?retType),
  isType(?retType),
  MethodInvocation_Method(?invo, ?method).
VarsAtInvocationRetrievingView(?ret, ?var) :-
  ViewRetrievalByArg0MethodInvocation(?invo),
  AssignReturnValue(?invo, ?ret),
  ActualParam(0, ?invo, ?var).
ViewObjectValueFromId(?viewValue, ?numId) :-
  LayoutControl(?numId, ?type, _),
  ReifiedLayoutControl(?type, ?numId, ?viewValue).
VarPointsTo(?hctx, ?viewValue, ?ctx, ?ret) :-
  VarsAtInvocationRetrievingView(?ret, ?var),
  VarPointsTo(?hctx, ?value, ?ctx, ?var),
  Value_Num(?value, ?numId),
  ViewObjectValueFromId(?viewValue, ?numId).
Reachable(?clinit) :-
   InitializedClass(?class),
   ClassInitializer(?class, ?clinit).
ClassInitializer(?type, ?method) :-
   MethodImplemented("<clinit>", "void()", ?type, ?method).
InitializedClass(?superclass) :-
   InitializedClass(?classOrInterface),
   DirectSuperclass(?classOrInterface, ?superclass).
InitializedClass(?class) :-
   MainMethodDeclaration(?method),
   Method_DeclaringType(?method, ?class).
InitializedClass(?class) :-
   Reachable(?inmethod),
   AssignHeapAllocation(?heap, _, ?inmethod),
   HeapAllocation_Type(?heap, ?class).
InitializedClass(?class) :-
   Reachable(?inmethod),
   Instruction_Method(?invocation, ?inmethod),
   isStaticMethodInvocation_Insn(?invocation),
   MethodInvocation_Method(?invocation, ?signature),
   Method_DeclaringType(?signature, ?class).
InitializedClass(?classOrInterface) :-
   Reachable(?inmethod),
   StoreStaticField(_, ?signature, ?inmethod),
   Field_DeclaringType(?signature, ?classOrInterface).
InitializedClass(?classOrInterface) :-
   Reachable(?inmethod),
   LoadStaticField(?signature, _, ?inmethod),
   Field_DeclaringType(?signature, ?classOrInterface).
Instruction_Throws(?hctx, ?value, ?ctx, ?insn) :-
  Throw(?insn, ?var),
  VarPointsTo(?hctx, ?value, ?ctx, ?var).
Instruction_Throws(?hctx, ?value, ?callerCtx, ?invocation) :-
  CallGraphEdge(?callerCtx, ?invocation, ?calleeCtx, ?tomethod),
  ThrowPointsTo(?hctx, ?value, ?calleeCtx, ?tomethod).
  .plan 1:(2,1)
ThrowPointsTo(?hctx, ?value, ?ctx, ?method) :-
  Instruction_Throws(?hctx, ?value, ?ctx, ?insn),
  Instruction_Method(?insn, ?method),
  !ExceptionHandler_InRange(_, ?insn).
ThrowPointsTo(?hctx, ?value, ?ctx, ?method) :-
  Instruction_Throws(?hctx, ?value, ?ctx, ?insn),
  Value_Type(?value, ?valueType),
  Instruction_Method(?insn, ?method),
  ExceptionHandler_SameInsn_Repr(?insn, ?repr),
  ExceptionHandler_SameBlock_Repr(?repr, ?block),
  !ExceptionHandler_TypeIsCaught(?valueType, ?block).
VarPointsTo(?hctx, ?value, ?ctx, ?param) :-
  Instruction_Throws(?hctx, ?value, ?ctx, ?insn),
  Value_Type(?value, ?valueType),
  ExceptionHandler_InRange(?handler, ?insn),
  ExceptionHandler_Type(?handler, ?handlerType),
  SubtypeOf(?valueType, ?handlerType),
  ConcreteClass(?valueType),
  ExceptionHandler_FormalParam(?handler, ?param),
  !ExceptionHandler_Impossible(?valueType, ?handler, ?insn).
ExceptionHandler_TypeIsCaught(?type, ?block) :-
  ExceptionHandler_InRange(?handler, ?insn),
  ExceptionHandler_SameInsn_Repr(?insn, ?repr),
  ExceptionHandler_SameBlock_Repr(?repr, ?block),
  ExceptionHandler_Type(?handler, ?handlerType),
  SubtypeOf(?type, ?handlerType),
  ConcreteClass(?type).
ExceptionHandler_Impossible(?type, ?h2, ?insn) :-
  ExceptionHandler_InRange(?h1, ?insn),
  ExceptionHandler_InRange(?h2, ?insn),
  ExceptionHandler_Before(?h1, ?h2),
  ExceptionHandler_Type(?h1, ?h1Type),
  ExceptionHandler_Type(?h2, ?h2Type),
  SubtypeOf(?type, ?h1Type),
  SubtypeOf(?type, ?h2Type),
  ConcreteClass(?type).
ExceptionHandler_InRange(?handler, ?instruction) :-
  ExceptionHandler_Method(?handler, ?method),
  Instruction_Method(?instruction, ?method),
  Instruction_Index(?instruction, ?index),
  ExceptionHandler_Begin(?handler, ?beginIndex),
  ?beginIndex <= ?index,
  ExceptionHandler_End(?handler, ?endIndex),
  ?endIndex > ?index.
ExceptionHandler_Before(?previous, ?handler) :-
  ExceptionHandler_Previous(?handler, ?previous).
ExceptionHandler_Before(?before, ?handler) :-
  ExceptionHandler_Before(?middle, ?handler),
  ExceptionHandler_Previous(?middle, ?before).
ExceptionHandler_SameInsn_PartialOrder(?h1, ?h2, ?insn) :-
  ExceptionHandler_InRange(?h1, ?insn),
  ExceptionHandler_InRange(?h2, ?insn),
  ExceptionHandler_Before(?h1, ?h2).
ExceptionHandler_SameInsn_Repr(?insn, ?handler) :-
  ExceptionHandler_InRange(?handler, ?insn),
  !ExceptionHandler_SameInsn_PartialOrder(_, ?handler, ?insn).
ExceptionHandler_SameBlock_PartialOrder(?h1, ?h2) :-
  ExceptionHandler_Before(?h1, ?h2),
  ExceptionHandler_Index(?h1, ?h1Index),
  ExceptionHandler_Index(?h2, ?h2Index),
  ?h1Index = ?h2Index.
ExceptionHandler_SameBlock_Repr(?handler, ?handler) :-
  isExceptionHandler(?handler),
  !ExceptionHandler_SameBlock_PartialOrder(_, ?handler).
ExceptionHandler_SameBlock_Repr(?handler, ?repr) :-
  ExceptionHandler_SameBlock_PartialOrder(?repr, ?handler),
  !ExceptionHandler_SameBlock_PartialOrder(_, ?repr).
isContext(?newCtx),
isHContext(?newHCtx),
CallGraphEdge(?callerCtx, ?fakeinvo, ?newCtx, ?register),
VarPointsTo(?newHCtx, ?heapValue, ?newCtx, ?formal) :-
  FakeInvocation_RegisterFinalize(?heapValue, ?fakeinvo),
  AllocatedObjectSupportsFinalize(?heapValue, ?inmethod),
  (!(HeapAllocation_Merge(?heapValue, _));
   HeapAllocation_Merge(?heapValue, ?heapValue)),
  ReachableContext(?callerCtx, ?inmethod),
  ?register = "<java.lang.ref.Finalizer: void register(java.lang.Object)>",
  isMethod(?register),
  FormalParam(0, ?register, ?formal),
  ?callerCtx = [ctxValue1, ctxValue2, ctxValue3], ?newHCtx = [ctxValue1, ctxValue2, ctxValue3],
  ?callerCtx = [ctxValue1, ctxValue2, ctxValue3], ?newCtx = [ctxValue2, ctxValue3, ?heapValue].
ImplicitReachable(sig) :-
    AndroidEntryPoint(sig).
ImplicitReachable(?m) :-
  ?m = "<java.lang.System: void initializeSystemClass()>",
  isMethod(?m).
ImplicitReachable(?m) :-
  ?m = "<java.lang.Thread: void <init>(java.lang.ThreadGroup,java.lang.Runnable)>",
  isMethod(?m).
ImplicitReachable(?m) :-
  ?m = "<java.lang.Thread: void <init>(java.lang.ThreadGroup,java.lang.String)>",
  isMethod(?m).
ImplicitReachable(?m) :-
  ?m = "<java.lang.ThreadGroup: void <init>()>",
  isMethod(?m).
ImplicitReachable(?m) :-
  ?m = "<java.lang.Thread: void exit()>",
  isMethod(?m).
ImplicitReachable(?m) :-
  ?m = "<java.lang.ThreadGroup: void uncaughtException(java.lang.Thread,java.lang.Throwable)>",
  isMethod(?m).
ImplicitReachable(?m) :-
  ?m = "<java.lang.ClassLoader: void <init>()>",
  isMethod(?m).
ImplicitReachable(?m) :-
  ?m = "<java.lang.ClassLoader: java.lang.Class loadClassInternal(java.lang.String)>",
  isMethod(?m).
ImplicitReachable(?m) :-
  ?m = "<java.lang.ClassLoader: void checkPackageAccess(java.lang.Class,java.security.ProtectionDomain)>",
  isMethod(?m).
ImplicitReachable(?m) :-
  ?m = "<java.lang.ClassLoader: void addClass(java.lang.Class)>",
  isMethod(?m).
ImplicitReachable(?m) :-
  ?m = "<java.lang.ClassLoader: long findNative(java.lang.ClassLoader,java.lang.String)>",
  isMethod(?m).
ImplicitReachable(?m) :-
  ?m = "<java.security.PrivilegedActionException: void <init>(java.lang.Exception)>",
  isMethod(?m).
VarPointsTo(?hctx, ?argArray, ?ctx, ?args),
ArrayIndexPointsTo(?hctx, ?argArrayContent, ?hctx, ?argArray) :-
   ImmutableHContextFromContext(?ctx, ?hctx),
   MainMethodDeclaration(?mainMethod),
   ReachableContext(?ctx, ?mainMethod),
   FormalParam(0, ?mainMethod, ?args),
   MainMethodArgArray(?argArray),
   MainMethodArgArrayContent(?argArrayContent).
AssignLocal("java.lang.Object.clone/@this", "java.lang.Object.clone/@native-return", "<java.lang.Object: java.lang.Object clone()>") :- isVar("java.lang.Object.clone/@this"), isVar("java.lang.Object.clone/@native-return"), isMethod("<java.lang.Object: java.lang.Object clone()>").
StoreStaticField("java.lang.System.setIn0/@param0", "<java.lang.System: java.io.InputStream in>", "<java.lang.System: void setIn0(java.io.InputStream)>") :- isMethod("<java.lang.System: void setIn0(java.io.InputStream)>"), isVar("java.lang.System.setIn0/@param0"), isField("<java.lang.System: java.io.InputStream in>").
StoreStaticField("java.lang.System.setOut0/@param0", "<java.lang.System: java.io.PrintStream out>", "<java.lang.System: void setOut0(java.io.PrintStream)>") :- isMethod("<java.lang.System: void setOut0(java.io.PrintStream)>"), isVar("java.lang.System.setOut0/@param0"), isField("<java.lang.System: java.io.PrintStream out>").
StoreStaticField("java.lang.System.setErr0/@param0", "<java.lang.System: java.io.PrintStream err>", "<java.lang.System: void setErr0(java.io.PrintStream)>") :- isMethod("<java.lang.System: void setErr0(java.io.PrintStream)>"), isVar("java.lang.System.setErr0/@param0"), isField("<java.lang.System: java.io.PrintStream err>").
isVar(cat(?invocation, "/@tmp-arraycopy")), Var_Type(cat(?invocation, "/@tmp-arraycopy"), ?tmpType), Var_DeclaringMethod(cat(?invocation, "/@tmp-arraycopy"), ?inmethod),
LoadArrayIndex(?src, cat(?invocation, "/@tmp-arraycopy"), ?inmethod),
StoreArrayIndex(cat(?invocation, "/@tmp-arraycopy"), ?dest, ?inmethod) :-
   ?arraycopy = "<java.lang.System: void arraycopy(java.lang.Object,int,java.lang.Object,int,int)>",
   isMethod(?arraycopy),
   StaticMethodInvocation(?invocation, ?arraycopy, ?inmethod),
   ActualParam(0, ?invocation, ?src),
   ActualParam(2, ?invocation, ?dest),
   isMethodInvocation(?invocation),
   ?tmpType = "java.lang.Object",
   isType(?tmpType).
StoreArrayIndex(?from, ?base, ?inmethod) :-
  ?casObject = "<sun.misc.Unsafe: boolean compareAndSwapObject(java.lang.Object,long,java.lang.Object,java.lang.Object)>",
  isMethod(?casObject),
  VirtualMethodInvocation(?invocation, ?casObject, ?inmethod),
  ActualParam(0, ?invocation, ?base),
  ActualParam(3, ?invocation, ?from).
StoreArrayIndex(?from, ?base, ?inmethod) :-
  (?putObj = "<sun.misc.Unsafe: void putObject(java.lang.Object,long,java.lang.Object)>";
   ?putObj = "<sun.misc.Unsafe: void putObject(java.lang.Object,int,java.lang.Object)>";
   ?putObj = "<sun.misc.Unsafe: void putObjectVolatile(java.lang.Object,long,java.lang.Object)>";
   ?putObj = "<sun.misc.Unsafe: void putOrderedObject(java.lang.Object,long,java.lang.Object)>"),
  isMethod(?putObj),
  VirtualMethodInvocation(?invocation, ?putObj, ?inmethod),
  ActualParam(0, ?invocation, ?base),
  ActualParam(2, ?invocation, ?from).
LoadArrayIndex(?base, ?to, ?inmethod) :-
  (?getObj = "<sun.misc.Unsafe: java.lang.Object getObjectVolatile(java.lang.Object,long)>";
   ?getObj = "<sun.misc.Unsafe: java.lang.Object getObject(java.lang.Object,long)>";
   ?getObj = "<sun.misc.Unsafe: java.lang.Object getObject(java.lang.Object,int)>"),
  isMethod(?getObj),
  VirtualMethodInvocation(?invocation, ?getObj, ?inmethod),
  ActualParam(0, ?invocation, ?base),
  AssignReturnValue(?invocation, ?to).
AssignHeapAllocation("java.io.FileSystem.getFileSystem/new java.io.UnixFileSystem", ?return, "<java.io.FileSystem: java.io.FileSystem getFileSystem()>") :- isMethod("<java.io.FileSystem: java.io.FileSystem getFileSystem()>"), ReturnVar(?return, "<java.io.FileSystem: java.io.FileSystem getFileSystem()>"), isHeapAllocation("java.io.FileSystem.getFileSystem/new java.io.UnixFileSystem"). SpecialMethodInvocation_Base(cat("<java.io.FileSystem: java.io.FileSystem getFileSystem()>", cat("/native", "<java.io.UnixFileSystem: void <init>()>")), ?return), Instruction_Method(cat("<java.io.FileSystem: java.io.FileSystem getFileSystem()>", cat("/native", "<java.io.UnixFileSystem: void <init>()>")), "<java.io.FileSystem: java.io.FileSystem getFileSystem()>"), MethodInvocation_Method(cat("<java.io.FileSystem: java.io.FileSystem getFileSystem()>", cat("/native", "<java.io.UnixFileSystem: void <init>()>")), "<java.io.UnixFileSystem: void <init>()>"), isInstruction(cat("<java.io.FileSystem: java.io.FileSystem getFileSystem()>", cat("/native", "<java.io.UnixFileSystem: void <init>()>"))), isMethodInvocation(cat("<java.io.FileSystem: java.io.FileSystem getFileSystem()>", cat("/native", "<java.io.UnixFileSystem: void <init>()>"))), isSpecialMethodInvocation_Insn(cat("<java.io.FileSystem: java.io.FileSystem getFileSystem()>", cat("/native", "<java.io.UnixFileSystem: void <init>()>"))), Instruction_Index(cat("<java.io.FileSystem: java.io.FileSystem getFileSystem()>", cat("/native", "<java.io.UnixFileSystem: void <init>()>")), ?index) :- isMethod("<java.io.FileSystem: java.io.FileSystem getFileSystem()>"), ReturnVar(?return, "<java.io.FileSystem: java.io.FileSystem getFileSystem()>"), isMethod("<java.io.UnixFileSystem: void <init>()>"), ?index = 1 .
AssignHeapAllocation("java.io.UnixFileSystem.list/new java.lang.String[]", ?return, "<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>") :- isMethod("<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>"), ReturnVar(?return, "<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>"), isHeapAllocation("java.io.UnixFileSystem.list/new java.lang.String[]"). isVar(cat("<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>", "/@native-array-element")), Var_Type(cat("<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>", "/@native-array-element"), "java.lang.String"), Var_DeclaringMethod(cat("<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>", "/@native-array-element"), "<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>"), AssignHeapAllocation("java.io.UnixFileSystem.list/new java.lang.String", cat("<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>", "/@native-array-element"), "<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>"), StoreArrayIndex(cat("<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>", "/@native-array-element"), ?base, "<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>") :- isMethod("<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>"), ReturnVar(?base, "<java.io.UnixFileSystem: java.lang.String[] list(java.io.File)>"), isType("java.lang.String"), isHeapAllocation("java.io.UnixFileSystem.list/new java.lang.String").
isInstruction(cat("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", cat("/native ", "<java.lang.Object: void finalize()>"))), isMethodInvocation(cat("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", cat("/native ", "<java.lang.Object: void finalize()>"))), isVirtualMethodInvocation_Insn(cat("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", cat("/native ", "<java.lang.Object: void finalize()>"))), VirtualMethodInvocation(cat("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", cat("/native ", "<java.lang.Object: void finalize()>")), "<java.lang.Object: void finalize()>", "<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>"), VirtualMethodInvocation_Base(cat("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", cat("/native ", "<java.lang.Object: void finalize()>")), ?base), Instruction_Method(cat("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", cat("/native ", "<java.lang.Object: void finalize()>")), "<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>"), MethodInvocation_Method(cat("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", cat("/native ", "<java.lang.Object: void finalize()>")), "<java.lang.Object: void finalize()>"), Instruction_Index(cat("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", cat("/native ", "<java.lang.Object: void finalize()>")), ?index) :- isMethod("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>"), FormalParam(0, "<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", ?base), isMethod("<java.lang.Object: void finalize()>"), ?index = 1. isInstruction(cat("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", cat("/native ", "<java.lang.Object: void finalize()>"))), isMethodInvocation(cat("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", cat("/native ", "<java.lang.Object: void finalize()>"))), AssignReturnValue(cat("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>", cat("/native ", "<java.lang.Object: void finalize()>")), ?return) :- isMethod("<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>"), ReturnVar(?return, "<java.lang.ref.Finalizer: void invokeFinalizeMethod(java.lang.Object)>").
isInstruction(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>"))), isMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>"))), isVirtualMethodInvocation_Insn(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>"))), VirtualMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), "<java.security.PrivilegedAction: java.lang.Object run()>", "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>"), VirtualMethodInvocation_Base(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), ?base), Instruction_Method(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>"), MethodInvocation_Method(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), "<java.security.PrivilegedAction: java.lang.Object run()>"), Instruction_Index(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), ?index) :- isMethod("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>"), FormalParam(0, "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", ?base), isMethod("<java.security.PrivilegedAction: java.lang.Object run()>"), ?index = 1. isInstruction(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>"))), isMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>"))), AssignReturnValue(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), ?return) :- isMethod("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>"), ReturnVar(?return, "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction)>").
isInstruction(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>"))), isMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>"))), isVirtualMethodInvocation_Insn(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>"))), VirtualMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), "<java.security.PrivilegedAction: java.lang.Object run()>", "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>"), VirtualMethodInvocation_Base(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), ?base), Instruction_Method(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>"), MethodInvocation_Method(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), "<java.security.PrivilegedAction: java.lang.Object run()>"), Instruction_Index(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), ?index) :- isMethod("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>"), FormalParam(0, "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", ?base), isMethod("<java.security.PrivilegedAction: java.lang.Object run()>"), ?index = 1. isInstruction(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>"))), isMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>"))), AssignReturnValue(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedAction: java.lang.Object run()>")), ?return) :- isMethod("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>"), ReturnVar(?return, "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedAction,java.security.AccessControlContext)>").
isInstruction(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"))), isMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"))), isVirtualMethodInvocation_Insn(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"))), VirtualMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), "<java.security.PrivilegedExceptionAction: java.lang.Object run()>", "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>"), VirtualMethodInvocation_Base(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), ?base), Instruction_Method(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>"), MethodInvocation_Method(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"), Instruction_Index(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), ?index) :- isMethod("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>"), FormalParam(0, "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", ?base), isMethod("<java.security.PrivilegedExceptionAction: java.lang.Object run()>"), ?index = 1. isInstruction(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"))), isMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"))), AssignReturnValue(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), ?return) :- isMethod("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>"), ReturnVar(?return, "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction)>").
isInstruction(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"))), isMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"))), isVirtualMethodInvocation_Insn(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"))), VirtualMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), "<java.security.PrivilegedExceptionAction: java.lang.Object run()>", "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>"), VirtualMethodInvocation_Base(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), ?base), Instruction_Method(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>"), MethodInvocation_Method(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"), Instruction_Index(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), ?index) :- isMethod("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>"), FormalParam(0, "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", ?base), isMethod("<java.security.PrivilegedExceptionAction: java.lang.Object run()>"), ?index = 1. isInstruction(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"))), isMethodInvocation(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>"))), AssignReturnValue(cat("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>", cat("/native ", "<java.security.PrivilegedExceptionAction: java.lang.Object run()>")), ?return) :- isMethod("<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>"), ReturnVar(?return, "<java.security.AccessController: java.lang.Object doPrivileged(java.security.PrivilegedExceptionAction,java.security.AccessControlContext)>").
StaticFieldPointsTo(?hctx, ?value, ?pending) :-
   ?pending = "<java.lang.ref.Reference: java.lang.ref.Reference pending>",
   ?this = "<java.lang.ref.Reference: void <init>(java.lang.Object,java.lang.ref.ReferenceQueue)>/@this",
   isField(?pending),
   isVar(?this),
   VarPointsTo(?hctx, ?value, _, ?this).
.decl HeapAllocation_Special(?heap:HeapAllocation)
HeapAllocation_Special(?heap) :-
  HeapAllocation_ContextInsensitive(?heap).
HeapAllocation_Special(?heap) :-
  HeapAllocation_Merge(?heap, _).
.decl HeapAllocation_ContextInsensitive(?heap:HeapAllocation)
.decl HeapAllocation_Merge(?heap:HeapAllocation, ?mergeHeap:HeapAllocation)
.decl HeapAllocation_Keep(?heap:HeapAllocation)
AssignNormalHeapAllocation(?heap, ?var, ?inmethod) :-
  AssignHeapAllocation(?heap, ?var, ?inmethod),
  !HeapAllocation_Special(?heap).
AssignContextInsensitiveHeapAllocation(?mergeHeap, ?var, ?inmethod) :-
  AssignHeapAllocation(?heap, ?var, ?inmethod),
  HeapAllocation_Merge(?heap, ?mergeHeap).
AssignContextInsensitiveHeapAllocation(?heap, ?var, ?inmethod) :-
  AssignHeapAllocation(?heap, ?var, ?inmethod),
  HeapAllocation_ContextInsensitive(?heap),
  !(HeapAllocation_Merge(?heap, _)).
.decl HeapRepresentative(?heap:HeapAllocation, ?heapRepr:symbol)
.decl HeapIsMergedString(?heap:HeapAllocation)
HeapIsMergedString(?heap) :-
  HeapRepresentative("<<string-constant>>", ?heap).
HeapAllocation_Merge(?heap, ?heapRepr) :-
  ?heapRepr = "<<string-constant>>",
  HeapRepresentative(?heapRepr, ?heap).
.decl HeapIsMergedStringFactory(?heap:HeapAllocation)
HeapIsMergedStringFactory(?heap) :-
  HeapRepresentative("<<string-buffer>>", ?heap);
  HeapRepresentative("<<string-builder>>", ?heap).
HeapAllocation_Merge(?heap, ?heapRepr) :-
  (?heapRepr = "<<string-buffer>>",
   HeapRepresentative(?heapRepr, ?heap));
  (?heapRepr = "<<string-builder>>",
   HeapRepresentative(?heapRepr, ?heap)).
.decl RepresentativesToPickFrom(?heapRepr:HeapAllocation, ?heap:HeapAllocation)
RepresentativesToPickFrom(?heapRepr, ?heap) :-
  HeapRepresentative(?heapRepr, ?heap),
  !HeapIsMergedString(?heap),
  !HeapIsMergedStringFactory(?heap),
  !HeapAllocation_Keep(?heap).
.decl MinRepresentativeHeapToPickFromOrdinal(?minHeapReprOrd:number, ?heap:HeapAllocation)
MinRepresentativeHeapToPickFromOrdinal(?minHeapReprOrd, ?heap) :-
  RepresentativesToPickFrom(_, ?heap),
  ?minHeapReprOrd = min ord(?heapRepr): RepresentativesToPickFrom(?heapRepr, ?heap).
HeapAllocation_Merge(?heap, ?mergeHeap) :-
  isHeapAllocation(?mergeHeap),
  ord(?mergeHeap) = ?minHeapReprOrd,
  MinRepresentativeHeapToPickFromOrdinal(?minHeapReprOrd, ?heap).
.decl ReflectionStringConstant(?heap:HeapAllocation)
.decl ReflectionSubstringObject(?heap:HeapAllocation)
HeapRepresentative(?constant, ?heap) :-
  isStringConstant(?heap),
  ?constant = "<<string-constant>>",
  isHeapAllocation(?constant),
  !HeapAllocation_Keep(?heap).
HeapAllocation_ContextInsensitive(?heap) :-
  isStringConstant(?heap),
  !HeapRepresentative(_, ?heap).
.decl NonTrivialStringConstant(?heap:HeapAllocation)
NonTrivialStringConstant(?heap) :-
  isStringConstant(?heap),
  strlen(?heap) >= 7.
.decl ClassNameMatchingStringConstant_Type(?type:Type, ?heap:HeapAllocation)
.decl MethodNameMatchingStringConstant_Signature(?sig:Method, ?heap:HeapAllocation)
.decl FieldNameMatchingStringConstant_Signature(?sig:Field, ?heap:HeapAllocation)
.decl PreClassNameMatchingStringConstant(?heap:HeapAllocation)
.decl PreClassNameMatchingStringConstant_Type(?type:Type, ?heap:HeapAllocation)
.decl PreClassNameMatchingStringConstantExact_Type(?type:Type, ?heap:HeapAllocation)
.decl PreClassNameMatchingStringConstantInexact_Type(?type:Type, ?heap:HeapAllocation)
ClassNameMatchingStringConstant_Type(?type, ?heap) :-
  PreClassNameMatchingStringConstant_Type(?type, ?heap).
MethodNameMatchingStringConstant_Signature(?sig, ?heap) :-
  PreMethodNameMatchingStringConstant_Signature(?sig, ?heap).
FieldNameMatchingStringConstant_Signature(?sig, ?heap) :-
  PreFieldNameMatchingStringConstant_Signature(?sig, ?heap).
PreClassNameMatchingStringConstant(?string),
PreClassNameMatchingStringConstant_Type(?type, ?string),
PreClassNameMatchingStringConstantExact_Type(?type, ?string) :-
  isStringConstant(?string),
  isReferenceType(?type),
  ord(?type) = ord(?string),
  ApplicationClass(?type),
  NonTrivialStringConstant(?string).
.decl PreMethodNameMatchingStringConstant(?heap:HeapAllocation)
.decl PreMethodNameMatchingStringConstant_Signature(?sig:Method, ?heap:HeapAllocation)
.decl PreMethodNameMatchingStringConstantExact_Signature(?sig:Method, ?heap:HeapAllocation)
.decl PreMethodNameMatchingStringConstantInexact_Signature(?sig:Method, ?heap:HeapAllocation)
PreMethodNameMatchingStringConstant(?string),
PreMethodNameMatchingStringConstant_Signature(?sig, ?string),
PreMethodNameMatchingStringConstantExact_Signature(?sig, ?string) :-
  isStringConstant(?string),
  Method_SimpleName(?sig, ?string),
  ?string != "<init>",
  ?string != "<clinit>".
.decl PreFieldNameMatchingStringConstant(?heap:HeapAllocation)
.decl PreFieldNameMatchingStringConstant_Signature(?sig:Field, ?heap:HeapAllocation)
.decl PreFieldNameMatchingStringConstantExact_Signature(?sig:Field, ?heap:HeapAllocation)
.decl PreFieldNameMatchingStringConstantInexact_Signature(?sig:Field, ?heap:HeapAllocation)
PreFieldNameMatchingStringConstant(?string),
PreFieldNameMatchingStringConstant_Signature(?sig, ?string),
PreFieldNameMatchingStringConstantExact_Signature(?sig, ?string) :-
  isStringConstant(?string),
  NonTrivialStringConstant(?string),
  Field_SimpleName(?sig, ?string).
HeapAllocation_ContextInsensitive(?heap) :-
  isClassHeap(?heap).
.decl MethodAllocationMergeThreshold(?t:number)
MethodAllocationMergeThreshold(50).
.decl ExceptionType(?type:Type)
ExceptionType(?type) :-
  ?throw = "java.lang.Throwable",
  isType(?throw),
  SubtypeOf(?type, ?throw).
.decl OptAssignHeapAllocation(?inmethod:Method, ?heap:HeapAllocation)
OptAssignHeapAllocation(?inmethod, ?heap) :-
  AssignHeapAllocation(?heap, _, ?inmethod).
.decl ObjectMultipleAllocated(?heap:HeapAllocation)
ObjectMultipleAllocated(?heap) :-
  OptAssignHeapAllocation(?inmethod1, ?heap),
  OptAssignHeapAllocation(?inmethod2, ?heap),
  ?inmethod1 != ?inmethod2.
.decl MethodAndTypeToHeap(?heap:HeapAllocation, ?heapType:Type, ?method:Method)
MethodAndTypeToHeap(?heap, ?heaptype, ?meth) :-
  AssignHeapAllocation(?heap, _, ?meth),
  HeapAllocation_Type(?heap, ?heaptype),
  !isStringConstant(?heap),
  !StringFactoryHeap(?heap),
  !HeapAllocation_EmptyArray(?heap),
  !ObjectMultipleAllocated(?heap),
  !HeapAllocation_Keep(?heap).
.decl AllocationsPerMethodAndType(?type:Type, ?meth:Method, ?n:number)
AllocationsPerMethodAndType(?type, ?meth, ?n) :-
  MethodAndTypeToHeap(_, ?type, ?meth),
  ?n = count : MethodAndTypeToHeap(_, ?type, ?meth).
.decl AllocationShouldBeMergedPerMethod(?heaptype:Type, ?meth:Method)
AllocationShouldBeMergedPerMethod(?heaptype, ?meth) :-
  AllocationsPerMethodAndType(?heaptype, ?meth, ?n),
  MethodAllocationMergeThreshold(?t),
  ?n > ?t.
.decl MethodAndTypeToMergedHeap(?heap:HeapAllocation, ?heaptype:Type, ?meth:Method)
MethodAndTypeToMergedHeap(?heap, ?heaptype, ?meth) :-
  AllocationShouldBeMergedPerMethod(?heaptype, ?meth),
  MethodAndTypeToHeap(?heap, ?heaptype, ?meth).
.decl MinHeapOrdinalPerMethodAndType(?ord:number, ?type:Type, ?meth:Method)
.decl MethodAndTypeToRepresentative(?type:Type, ?meth:Method, ?reprHeap:HeapAllocation)
MinHeapOrdinalPerMethodAndType(?minHeapOrd, ?type, ?meth) :-
  MethodAndTypeToMergedHeap(_, ?type, ?meth),
  ?minHeapOrd = min ord(?heap): MethodAndTypeToMergedHeap(?heap, ?type, ?meth).
MethodAndTypeToRepresentative(?type, ?meth, ?representativeHeap) :-
  isHeapAllocation(?representativeHeap),
  MinHeapOrdinalPerMethodAndType(?minHeapOrd, ?type, ?meth),
  ord(?representativeHeap) = ?minHeapOrd.
HeapRepresentative(?representativeHeap, ?heap) :-
  MethodAndTypeToRepresentative(?type, ?meth, ?representativeHeap),
  MethodAndTypeToMergedHeap(?heap, ?type, ?meth).
.decl ClassAndTypeToHeap(?heap:HeapAllocation, ?heaptype:Type, ?class:ClassType)
.decl AllocationsPerClassAndType(?type:Type, ?class:ClassType, ?n:number)
ClassAndTypeToHeap(?heap, ?heaptype, ?class) :-
  MethodAndTypeToHeap(?heap, ?heaptype, ?meth),
  Method_DeclaringType(?meth, ?class).
AllocationsPerClassAndType(?type, ?class, ?n) :-
  ClassAndTypeToHeap(_, ?type, ?class),
  ?n = count : ClassAndTypeToHeap(_, ?type, ?class).
.decl AllocationShouldBeMergedPerClass(?heaptype:Type, ?class:Type)
.decl ClassAndTypeToMergedHeap(?heap:HeapAllocation, ?heaptype:Type, ?class:Type)
ClassAndTypeToMergedHeap(?heap, ?heaptype, ?class) :-
  AllocationShouldBeMergedPerClass(?heaptype, ?class),
  ClassAndTypeToHeap(?heap, ?heaptype, ?class).
.decl MinHeapOrdinalPerClassAndType(?minHeapOrd:number, ?type:Type, ?class:Type)
.decl ClassAndTypeToRepresentative(?type:Type, ?class:Type, ?reprHeap:HeapAllocation)
MinHeapOrdinalPerClassAndType(?minHeapOrd, ?type, ?class) :-
  ClassAndTypeToMergedHeap(_, ?type, ?class),
  ?minHeapOrd = min ord(?heap): ClassAndTypeToMergedHeap(?heap, ?type, ?class).
ClassAndTypeToRepresentative(?type, ?class, ?representativeHeap) :-
  isHeapAllocation(?representativeHeap),
  MinHeapOrdinalPerClassAndType(?minHeapOrd, ?type, ?class),
  ord(?representativeHeap) = ?minHeapOrd.
HeapRepresentative(?representativeHeap, ?heap) :-
  ClassAndTypeToRepresentative(?type, ?class, ?representativeHeap),
  ClassAndTypeToMergedHeap(?heap, ?type, ?class).
.decl ClassNameIndexes(?pos:number, ?type:ClassType)
ClassNameIndexes(0, ?type) :-
  isClassType(?type).
ClassNameIndexes(?pos+1, ?t) :-
  ClassNameIndexes(?pos, ?t),
  ?pos+1 < strlen(?t).
.decl DotsInClassName(?type:ClassType, ?pos:number)
.decl NotLastDot(?pos:number, ?type:ClassType)
.decl NotSecondLastDot(?pos:number, ?type:ClassType)
.decl LastDot(?type:ClassType, ?pos:number)
.decl SecondLastDot(?type:ClassType, ?pos:number)
.decl Class_PackageHack(?type:ClassType, ?packageName:symbol)
DotsInClassName(?type, ?pos) :-
  ClassNameIndexes(?pos, ?type),
  substr(?type, ?pos, 1) = ".".
NotLastDot(?pos, ?type) :-
  DotsInClassName(?type, ?pos),
  DotsInClassName(?type, ?pos2),
  ?pos2 > ?pos.
NotSecondLastDot(?pos, ?type) :-
  DotsInClassName(?type, ?pos),
  DotsInClassName(?type, ?pos2),
  ?pos2 > ?pos,
  NotLastDot(?pos2, ?type).
NotSecondLastDot(?pos, ?type) :-
  LastDot(?type, ?pos).
LastDot(?type, ?pos) :-
  DotsInClassName(?type, ?pos),
  !NotLastDot(?pos, ?type).
SecondLastDot(?type, ?pos) :-
  DotsInClassName(?type, ?pos),
  !NotSecondLastDot(?pos, ?type).
Class_PackageHack(?type, substr(?type, 0, ?secondLastPos)) :-
  SecondLastDot(?type, ?secondLastPos),
  isClassType(?type).
Class_PackageHack(?type, substr(?type, 0, ?lastPos)) :-
  !(SecondLastDot(?type, _)),
  isClassType(?type),
  LastDot(?type, ?lastPos).
Class_PackageHack(?type, ?type) :-
  !(LastDot(?type, _)),
  isClassType(?type).
.decl PackageAndTypeToHeap(?heap:HeapAllocation, ?heaptype:Type, ?packageName:symbol)
.decl AllocationsPerPackageAndType(?type:Type, ?packageName:symbol, ?n:number)
PackageAndTypeToHeap(?heap, ?heaptype, ?packageName) :-
  ClassAndTypeToHeap(?heap, ?heaptype, ?class),
  Class_PackageHack(?class, ?packageName).
AllocationsPerPackageAndType(?type, ?packageName, ?n) :-
  PackageAndTypeToHeap(_, ?type, ?packageName),
  ?n = count : PackageAndTypeToHeap(_, ?type, ?packageName).
.decl AllocationShouldBeMergedPerPackage(?heaptype:Type, ?packageName:symbol)
.decl PackageAndTypeToMergedHeap(?heap:HeapAllocation, ?heaptype:Type, ?packageName:symbol)
PackageAndTypeToMergedHeap(?heap, ?heaptype, ?packageName) :-
  AllocationShouldBeMergedPerPackage(?heaptype, ?packageName),
  PackageAndTypeToHeap(?heap, ?heaptype, ?packageName).
.decl MinHeapOrdinalPerPackageAndType(?minHeapOrd:number, ?type:Type, ?packageName:symbol)
.decl PackageAndTypeToRepresentative(?type:Type, ?packageName:symbol, ?representativeHeap:HeapAllocation)
MinHeapOrdinalPerPackageAndType(?minHeapOrd, ?type, ?packageName) :-
  PackageAndTypeToMergedHeap(_, ?type, ?packageName),
  ?minHeapOrd = min ord(?heap): PackageAndTypeToMergedHeap(?heap, ?type, ?packageName).
PackageAndTypeToRepresentative(?type, ?packageName, ?representativeHeap) :-
  isHeapAllocation(?representativeHeap),
  MinHeapOrdinalPerPackageAndType(?minHeapOrd, ?type, ?packageName),
  ord(?representativeHeap) = ?minHeapOrd.
HeapRepresentative(?representativeHeap, ?heap) :-
  PackageAndTypeToRepresentative(?type, ?packageName, ?representativeHeap),
  PackageAndTypeToMergedHeap(?heap, ?type, ?packageName).
.decl TypeToHeap(?heap:HeapAllocation, ?heaptype:Type)
.decl AllocationsPerType(?type:Type, ?n:number)
TypeToHeap(?heap, ?heaptype) :-
  ClassAndTypeToHeap(?heap, ?heaptype, _).
AllocationsPerType(?type, ?n) :-
  TypeToHeap(_, ?type),
  ?n = count : TypeToHeap(_, ?type).
.decl AllocationShouldBeMergedGlobally(?heaptype:Type)
.decl TypeToMergedHeap(?heap:HeapAllocation, ?heaptype:Type)
TypeToMergedHeap(?heap, ?heaptype) :-
  AllocationShouldBeMergedGlobally(?heaptype),
  TypeToHeap(?heap, ?heaptype).
.decl MinHeapOrdinalPerType(?minHeapOrd:number, ?type:Type)
.decl TypeToRepresentative(?type:Type, ?representativeHeap:HeapAllocation)
MinHeapOrdinalPerType(?minHeapOrd, ?type) :-
  TypeToMergedHeap(_, ?type),
  ?minHeapOrd = min ord(?heap): TypeToMergedHeap(?heap, ?type).
TypeToRepresentative(?type, ?representativeHeap) :-
  isHeapAllocation(?representativeHeap),
  MinHeapOrdinalPerType(?minHeapOrd, ?type),
  ord(?representativeHeap) = ?minHeapOrd.
HeapRepresentative(?representativeHeap, ?heap) :-
  TypeToRepresentative(?type, ?representativeHeap),
  TypeToMergedHeap(?heap, ?type).
.decl SpecialLibraryObject(?heap:HeapAllocation)
SpecialLibraryObject(?heap) :-
  AssignHeapAllocation_Heap(?insn, ?heap),
  Instruction_Method(?insn, ?method),
  SpecialLibraryMethod(?method).
.decl SpecialLibraryMethod(?method:Method)
SpecialLibraryMethod(?method) :-
  Method_DeclaringType(?method, ?class),
  SpecialLibraryClass(?class).
.decl SpecialLibraryClass(?class:Type)
SpecialLibraryClass(?class) :-
  isClassType(?class),
  !ApplicationClass(?class),
  !CollectionLibraryClass(?class).
.decl CollectionLibraryClass(?class:Type)
CollectionLibraryClass(?class) :-
  isClassType(?class),
  !ApplicationClass(?class),
  isType(?class),
  match("java\.util.*", ?class).
HeapAllocation_ContextInsensitive(?heap) :-
  SpecialLibraryObject(?heap),
  !HeapRepresentative(_, ?heap).
AllocationShouldBeMergedPerMethod(?heaptype, ?meth) :-
  AllocationsPerMethodAndType(?heaptype, ?meth, ?n),
  ?n > 1,
  Method_DeclaringType(?meth, ?class),
  SpecialLibraryClass(?class).
.decl StringFactoryType(?type:Type)
.decl StringFactoryHeap(?heap:HeapAllocation)
StringFactoryType(?type) :-
  ?type = "java.lang.StringBuffer" ;
  ?type = "java.lang.StringBuilder".
StringFactoryHeap(?heap) :-
  HeapAllocation_Type(?heap, ?heaptype),
  StringFactoryType(?heaptype).
.decl StringFactoryVar(?var:Var)
.decl StringFactoryVarPointsTo(?factoryHctx:HContext, ?factoryValue:Value, ?ctx:Context, ?var:Var)
HeapRepresentative("<<string-buffer>>", ?heap) :-
  HeapAllocation_Type(?heap, "java.lang.StringBuffer"),
  !HeapAllocation_Keep(?heap).
HeapRepresentative("<<string-builder>>", ?heap) :-
  HeapAllocation_Type(?heap, "java.lang.StringBuilder"),
  !HeapAllocation_Keep(?heap).
.decl ExceptionTypeToHeap(?heap:HeapAllocation, ?type:Type)
ExceptionTypeToHeap(?heap, ?heaptype) :-
  AssignHeapAllocation(?heap, _, _),
  HeapAllocation_Type(?heap, ?heaptype),
  ExceptionType(?heaptype).
.decl ExceptionHeapTypeRepresentativeOrdinal(?type:Type, ?reprHeapOrd:number)
ExceptionHeapTypeRepresentativeOrdinal(?type, ?representativeHeapOrd) :-
  ExceptionTypeToHeap(_, ?type),
  ?representativeHeapOrd = min ord(?heap) : ExceptionTypeToHeap(?heap, ?type).
HeapRepresentative(?representativeHeap, ?heap) :-
  ExceptionHeapTypeRepresentativeOrdinal(?heaptype, ?representativeHeapOrd),
  ExceptionTypeToHeap(?heap, ?heaptype),
  ord(?representativeHeap) = ?representativeHeapOrd,
  isHeapAllocation(?representativeHeap).
HeapAllocation_ContextInsensitive(?heap) :-
  HeapAllocation_Type(?heap, ?type),
  isArrayType(?type),
  ComponentType(?type, ?componentType),
  isPrimitiveType(?componentType).
RunningThread(?hctx, ?value) :-
    MainThread(?hctx, ?value).
isContext(?calleeCtx),
ReachableContext(?calleeCtx, ?run),
VarPointsTo(?hctx, ?value, ?calleeCtx, ?runThis),
RunningThread(?hctx, ?value)
:-
    ?start = "<java.lang.Thread: void start0()>",
    ThisVar(?start, ?startThis),
    VarPointsTo(?hctx, ?value, ?callerCtx, ?startThis),
    Value_Type(?value, ?valuetype),
    MethodLookup("run", "void()", ?valuetype, ?run),
    ThisVar(?run, ?runThis),
    ?callerCtx = ?callerCtx,
    ?hctx = [hctxValue1, hctxValue2, hctxValue3], ?calleeCtx = [hctxValue2, hctxValue3, ?value].
VarPointsTo(?hctx, ?value, ?callerCtx, ?local) :-
   ReachableCurrentThreadInvocation(?callerCtx, ?local),
   RunningThread(?hctx, ?value),
   ?callerCtx = ?callerCtx, ?hctx = ?hctx.
ReachableCurrentThreadInvocation(?callerCtx, ?local) :-
   ?signature = "<java.lang.Thread: java.lang.Thread currentThread()>",
   StaticMethodInvocation(?invocation, ?signature, ?inmethod),
   ReachableContext(?callerCtx, ?inmethod),
   AssignReturnValue(?invocation, ?local).
isContext(?calleeCtx),
ReachableContext(?calleeCtx, ?signature),
VarPointsTo(?hctx, ?value, ?calleeCtx, ?this) :-
    ?signature = "<java.lang.ThreadGroup: void <init>()>",
    ThisVar(?signature, ?this),
    SystemThreadGroup(?hctx, ?value),
    ?hctx = [hctxValue1, hctxValue2, hctxValue3], ?calleeCtx = [hctxValue2, hctxValue3, ?value].
isContext(?calleeCtx),
ReachableContext(?calleeCtx, ?signature),
VarPointsTo(?hctx, ?value, ?calleeCtx, ?this),
VarPointsTo(?groupHCtx, ?group, ?calleeCtx, ?groupParam) :-
    ?signature = "<java.lang.ThreadGroup: void <init>(java.lang.ThreadGroup,java.lang.String)>",
    ThisVar(?signature, ?this),
    MainThreadGroup(?hctx, ?value),
    FormalParam(0, ?signature, ?groupParam),
    SystemThreadGroup(?groupHCtx, ?group),
    ?hctx = ?hctx, ?groupHCtx = ?groupHCtx,
    ?hctx = [hctxValue1, hctxValue2, hctxValue3], ?calleeCtx = [hctxValue2, hctxValue3, ?value].
isContext(?calleeCtx),
ReachableContext(?calleeCtx, ?signature),
VarPointsTo(?hctx, ?value, ?calleeCtx, ?this),
VarPointsTo(?groupHCtx, ?group, ?calleeCtx, ?groupParam) :-
    ?signature = "<java.lang.Thread: void <init>(java.lang.ThreadGroup,java.lang.String)>",
    ThisVar(?signature, ?this),
    MainThread(?hctx, ?value),
    FormalParam(0, ?signature, ?groupParam),
    MainThreadGroup(?groupHCtx, ?group),
    ?hctx = ?hctx, ?groupHCtx = ?groupHCtx,
    ?hctx = [hctxValue1, hctxValue2, hctxValue3], ?calleeCtx = [hctxValue2, hctxValue3, ?value].
FakeInvocation_RegisterFinalize0(?val2, cat("<register-finalize ", cat(?val1, cat( "/", cat(?val2, "  >"))))),
isInstruction(cat("<register-finalize ", cat(?val1, cat( "/", cat(?val2, "  >"))))), isMethodInvocation(cat("<register-finalize ", cat(?val1, cat( "/", cat(?val2, "  >"))))) :-
    AllocatedObjectSupportsFinalize(?val2, ?val1),
    isMethod(?val1),
    isHeapAllocation(?val2).
FakeInvocation_RegisterFinalize(?heapValue, ?invo) :-
  FakeInvocation_RegisterFinalize0(?heapValue, ?invo).
Value_isHeap(?heapValue),
isValue(?heapValue),
Value_Type(?heapValue, ?type) :-
  isHeapAllocation(?heapValue),
  HeapAllocation_Type(?heapValue, ?type).
Value_Num(cat("num-constant-", ?const), ?const),
isValue(cat("num-constant-", ?const)),
Value_Type(cat("num-constant-", ?const), ?type) :-
  isNumConstant(?const),
  AssignNumConstant_Id(?insn, ?const),
  Instruction_Method(?insn, ?meth),
  Method_SimpleName(?meth, "<clinit>"),
  Method_DeclaringType(?meth, ?className),
  isType(?className),
  contains(".R$", ?className),
  Type_int(?type).
Value_Num(cat("num-constant-", ?const), ?const),
isValue(cat("num-constant-", ?const)),
Value_Type(cat("num-constant-", ?const), ?type) :-
  isNumConstant(?const),
  FieldInitialValue(?fld, ?const),
  Field_DeclaringType(?fld, ?className),
  isType(?className),
  contains(".R$", ?className),
  Type_int(?type).
Value_isNonHeap(?value) :-
  Value_isMock(?value) ;
  Value_Num(?value, _).
Value_Null(?nullheap) :-
  HeapAllocation_Null(?nullheap).
Value_DeclaringType(?heapValue, ?type) :-
  AssignHeapAllocation(?heapValue, _, ?inmethod),
  Method_DeclaringType(?inmethod, ?type),
  !isStringConstant(?heapValue),
  !isClassHeap(?heapValue),
  !isMethodHandleConstant(?heapValue).
Value_DeclaringType(?heapValue, "java.lang.System") :-
  isClassHeap(?heapValue).
Value_DeclaringType(?heapValue, "java.lang.String") :-
  isStringConstant(?heapValue).
Value_DeclaringType(?value, "java.lang.Object") :-
  Value_Null(?value);
  MainMethodArgArray(?value);
  MainMethodArgArrayContent(?value).
Value_DeclaringType(?heapValue, "java.lang.invoke.MethodHandle") :-
  isMethodHandleConstant(?heapValue).
NotSpecialObject(?value) :-
  Value_isHeap(?value) ;
  Value_isMock(?value) ;
  Value_Num(?value, _).
isImmutableContext(ctx), isContext(ctx) :- ctx = ["<<immutable-context>>", "<<immutable-context>>", "<<immutable-context>>"].
isInitialContext(ctx), isContext(ctx) :- ctx = ["<<initial-context>>", "<<initial-context>>", "<<initial-context>>"].
isJVMStartupContext(ctx), isContext(ctx) :- ctx = ["<<jvm-startup-context>>", "<<jvm-startup-context>>", "<<jvm-startup-context>>"].
isClinitContext(ctx), isContext(ctx) :- ctx = ["<<clinit-context>>", "<<clinit-context>>", "<<clinit-context>>"].
ReachableContext(?initialContext, ?method) :-
  isInitialContext(?initialContext),
  MainMethodDeclaration(?method).
ReachableContext(?jvmStartUpContext, ?method) :-
  isJVMStartupContext(?jvmStartUpContext),
  ImplicitReachable(?method).
ReachableContext(?clinitContext, ?clinit) :-
  isClinitContext(?clinitContext),
  InitializedClass(?class),
  ClassInitializer(?class, ?clinit).
isImmutableHContext(hctx), isHContext(hctx) :- hctx = ["<<immutable-hcontext>>", "<<immutable-hcontext>>", "<<immutable-hcontext>>"].
isJVMStartupHContext(hctx), isHContext(hctx) :- hctx = ["<<jvm-startup-hcontext>>", "<<jvm-startup-hcontext>>", "<<jvm-startup-hcontext>>"].
SystemThreadGroup(?hctx, ?alloc) :-
  isJVMStartupHContext(?hctx),
  ?alloc = "<<system-thread-group>>",
  isValue(?alloc).
MainThreadGroup(?hctx, ?alloc) :-
  isJVMStartupHContext(?hctx),
  ?alloc = "<<main-thread-group>>",
  isValue(?alloc).
MainThread(?hctx, ?alloc) :-
  isJVMStartupHContext(?hctx),
  ?alloc = "<<main-thread>>",
  isValue(?alloc).
isHContext(?newHCtx),
VarPointsTo(?newHCtx, ?heapValue, ?ctx, ?var) :-
  AssignNormalHeapAllocation(?heapValue, ?var, ?inmethod),
  ReachableContext(?ctx, ?inmethod),
  ?ctx = [ctxValue1, ctxValue2, ctxValue3], ?newHCtx = [ctxValue1, ctxValue2, ctxValue3],
  ObjectShouldNotBeRefined(?heapValue).
isHContext(?newHCtx),
VarPointsTo(?newHCtx, ?heapValue, ?ctx, ?var) :-
  AssignAuxiliaryHeapAllocation(?heapValue, ?var, ?inmethod),
  ReachableContext(?ctx, ?inmethod),
  ?ctx = [ctxValue1, ctxValue2, ctxValue3], ?newHCtx = [ctxValue1, ctxValue2, ctxValue3].
VarPointsTo(?hctx, ?heapValue, ?ctx, ?var) :-
  Reachable(?inmethod),
  AssignContextInsensitiveHeapAllocation(?heapValue, ?var, ?inmethod),
  ReachableContext(?ctx, ?inmethod),
  ImmutableHContextFromContext(?ctx, ?hctx).
  .plan 2:(4,3,1,2)
VarPointsTo(?hctx, ?null, ?toCtx, ?to) :-
   Reachable(?inmethod),
   AssignNull(?to, ?inmethod),
   Value_Null(?null),
   ReachableContext(?toCtx, ?inmethod),
   ImmutableHContextFromContext(?toCtx, ?hctx).
   .plan 2:(5,4,1,2,3)
VarPointsTo(?hctx, ?value, ?toCtx, ?to) :-
   ReachableContext(?toCtx, ?inmethod),
   Instruction_Method(?insn, ?inmethod),
   (AssignNumConstant_Id(?insn, ?const);
    AssignCastNumConstant_Id(?insn, ?const)),
   AssignInstruction_To(?insn, ?to),
   Value_Num(?value, ?const),
   ImmutableHContextFromContext(?toCtx, ?hctx).
   .plan 1:(6,1,2,3,4,5)
VarPointsTo(?hctx, ?value, ?ctx, ?to) :-
  VarPointsTo(?hctx, ?value, ?ctx, ?from),
  AssignLocal(?from, ?to, _).
.decl OptAssignCast(?type:Type, ?to:Var, ?from:Var)
OptAssignCast(?type, ?to, ?from) :-
  Reachable(?inmethod),
  AssignCast(?type, ?from, ?to, ?inmethod).
VarPointsTo(?hctx, ?value, ?ctx, ?to) :-
  OptAssignCast(?type, ?to, ?from),
  VarPointsTo(?hctx, ?value, ?ctx, ?from),
  Value_Type(?value, ?valuetype),
  SupertypeOf(?type, ?valuetype).
VarPointsTo(?hctx, ?value, ?ctx, ?to) :-
  LoadHeapInstanceField(?ctx, ?to, ?signature, ?basehctx, ?basevalue),
  InstanceFieldPointsTo(?hctx, ?value, ?signature, ?basehctx, ?basevalue).
  .plan 1:(2,1)
LoadHeapInstanceField(?ctx, ?to, ?sig, ?basehctx, ?basevalue) :-
  LoadInstanceField(?base, ?sig, ?to, _),
  VarPointsTo(?basehctx, ?basevalue, ?ctx, ?base).
InstanceFieldPointsTo(?hctx, ?value, ?signature, ?basehctx, ?basevalue) :-
  StoreHeapInstanceField(?signature, ?basehctx, ?basevalue, ?ctx, ?from),
  VarPointsTo(?hctx, ?value, ?ctx, ?from),
  NotSpecialObject(?value),
  !Value_Null(?basevalue).
  .plan 1:(2,1,3)
StoreHeapInstanceField(?signature, ?basehctx, ?basevalue, ?ctx, ?from) :-
  StoreInstanceField(?from, ?base, ?signature, _),
  VarPointsTo(?basehctx, ?basevalue, ?ctx, ?base).
VarPointsTo(?hctx, ?value, ?ctx, ?to) :-
  StaticFieldPointsTo(?hctx, ?value, ?sig),
  LoadStaticField(?sig, ?to, ?inmethod),
  ReachableContext(?ctx, ?inmethod),
  ?ctx = ?ctx, ?hctx = ?hctx.
  .plan 1:(3,2,1)
StaticFieldPointsTo(?hctx, ?value, ?signature) :-
  ReachableStoreStaticFieldFrom(?from),
  StoreStaticField(?from, ?signature, _),
  VarPointsTo(?hctx, ?value, _, ?from).
.decl ReachableStoreStaticFieldFrom(?from:Var)
ReachableStoreStaticFieldFrom(?from) :-
  Reachable(?inmethod),
  StoreStaticField(?from, _, ?inmethod).
StaticFieldPointsTo(?hctx, ?value, ?signature) :-
  FieldInitialValue(?signature, ?const),
  Value_Num(?value, ?const),
  isImmutableHContext(?hctx).
.decl OptLoadHeapArrayIndex(?var:Var, ?value:Value)
.decl Temp1(?value:Value, ?var:Var)
.decl Temp2(?ctx:Context, ?var:Var, ?hctx:HContext, ?value:Value)
OptLoadHeapArrayIndex(?to, ?basevalue) :-
  LoadHeapArrayIndex(_, ?to, _, ?basevalue).
Temp1(?basevalue, ?to) :-
  NotEmptyArrayValue(?basevalue),
  OptLoadHeapArrayIndex(?to, ?basevalue),
  Value_Type(?basevalue, ?basevaluetype),
  ComponentType(?basevaluetype, ?basecomponenttype),
  Var_Type(?to, ?type),
  SupertypeOf(?type, ?basecomponenttype).
Temp2(?ctx, ?to, ?basehctx, ?basevalue) :-
  Temp1(?basevalue, ?to),
  LoadHeapArrayIndex(?ctx, ?to, ?basehctx, ?basevalue).
VarPointsTo(?hctx, ?value, ?ctx, ?to) :-
  Temp2(?ctx, ?to, ?basehctx, ?basevalue),
  ArrayIndexPointsTo(?hctx, ?value, ?basehctx, ?basevalue).
.decl NotEmptyArrayValue(?value:Value)
NotEmptyArrayValue(?heapValue) :-
  Value_isHeap(?heapValue),
  !HeapAllocation_EmptyArray(?heapValue).
NotEmptyArrayValue(?value) :-
  Value_isNonHeap(?value).
LoadHeapArrayIndex(?ctx, ?to, ?basehctx, ?basevalue) :-
  ReachableLoadArrayIndexBase(?base),
  OptLoadArrayIndex(?to, ?base),
  VarPointsTo(?basehctx, ?basevalue, ?ctx, ?base).
OptLoadArrayIndex(?to, ?base) :-
  LoadArrayIndex(?base, ?to, _).
.decl ReachableLoadArrayIndexBase(?base:Var)
ReachableLoadArrayIndexBase(?base) :-
  Reachable(?inmethod),
  LoadArrayIndex(?base, _, ?inmethod).
OptStoreIntoArray(?hctx, ?basehctx, ?basevalue, ?value) :-
  StoreHeapArrayIndex(?basehctx, ?basevalue, ?ctx, ?from),
  VarPointsTo(?hctx, ?value, ?ctx, ?from).
ArrayIndexPointsTo(?hctx, ?value, ?basehctx, ?basevalue) :-
  OptStoreIntoArray(?hctx, ?basehctx, ?basevalue, ?value),
  NotSpecialObject(?value),
  NotEmptyArrayValue(?basevalue),
  Value_Type(?value, ?valuetype),
  Value_Type(?basevalue, ?basevaluetype),
  ComponentType(?basevaluetype, ?componenttype),
  SupertypeOf(?componenttype, ?valuetype).
StoreHeapArrayIndex(?basehctx, ?basevalue, ?ctx, ?from) :-
  ReachableStoreArrayIndexBase(?base),
  OptStoreArrayIndex(?from, ?base),
  VarPointsTo(?basehctx, ?basevalue, ?ctx, ?base).
.decl ReachableStoreArrayIndexBase(?base:Var)
ReachableStoreArrayIndexBase(?base) :-
  Reachable(?inmethod),
  StoreArrayIndex(_, ?base, ?inmethod).
OptStoreArrayIndex(?from, ?base) :-
  StoreArrayIndex(?from, ?base, _).
OptInterproceduralAssign(?calleeCtx, ?formal, ?callerCtx, ?actual) :-
  CallGraphEdge(?callerCtx, ?invocation, ?calleeCtx, ?method),
  ActualParam(?index, ?invocation, ?actual),
  FormalParam(?index, ?method, ?formal).
OptInterproceduralAssign(?callerCtx, ?local, ?calleeCtx, ?return) :-
  CallGraphEdge(?callerCtx, ?invocation, ?calleeCtx, ?method),
  AssignReturnValue(?invocation, ?local),
  ReturnVar(?return, ?method).
VarPointsTo(?hctx, ?value, ?toCtx, ?to) :-
  OptInterproceduralAssign(?toCtx, ?to, ?fromCtx, ?from),
  VarPointsTo(?hctx, ?value, ?fromCtx, ?from).
  .plan 1:(2,1)
.decl OptVirtualMethodInvocationBase(?invocation:MethodInvocation, ?base:Var)
OptVirtualMethodInvocationBase(?invocation, ?base) :-
  Reachable(?inmethod),
  Instruction_Method(?invocation, ?inmethod),
  VirtualMethodInvocation_Base(?invocation, ?base).
isContext(?newCtx),
CallGraphEdge(?callerCtx, ?invocation, ?newCtx, ?tomethod),
VarPointsTo(?hctx, ?value, ?newCtx, ?this) :-
  OptVirtualMethodInvocationBase(?invocation, ?base),
  VarPointsTo(?hctx, ?value, ?callerCtx, ?base),
  Value_Type(?value, ?valuetype),
  ResolveInvocation(?valuetype, ?invocation, ?tomethod),
  ThisVar(?tomethod, ?this),
  SiteShouldNotBeRefined(?invocation),
  ?hctx = [hctxValue1, hctxValue2, hctxValue3], ?newCtx = [hctxValue2, hctxValue3, ?value].
isContext(?newCtx),
CallGraphEdge(?callerCtx, ?invocation, ?newCtx, ?tomethod) :-
  ReachableContext(?callerCtx, ?inmethod),
  StaticMethodInvocation(?invocation, ?tomethod, ?inmethod),
  ?newCtx = ?callerCtx.
.decl OptSpecialMethodInvocationBase(?invocation:MethodInvocation, ?base:Var)
OptSpecialMethodInvocationBase(?invocation, ?base) :-
  Reachable(?inmethod),
  Instruction_Method(?invocation, ?inmethod),
  SpecialMethodInvocation_Base(?invocation, ?base).
isContext(?newCtx),
CallGraphEdge(?callerCtx, ?invocation, ?newCtx, ?tomethod),
VarPointsTo(?hctx, ?value, ?newCtx, ?this) :-
  OptSpecialMethodInvocationBase(?invocation, ?base),
  MethodInvocation_Method(?invocation, ?tomethod),
  ThisVar(?tomethod, ?this),
  VarPointsTo(?hctx, ?value, ?callerCtx, ?base),
  SiteShouldNotBeRefined(?invocation),
  ?hctx = [hctxValue1, hctxValue2, hctxValue3], ?newCtx = [hctxValue2, hctxValue3, ?value].
ReachableContext(?ctx, ?method) :-
  CallGraphEdge(_, _, ?ctx, ?method).
Reachable(?method) :-
  ReachableContext(_, ?method).
.decl ObjectShouldNotBeRefined(?heap:HeapAllocation)
ObjectShouldNotBeRefined(?heap) :-
  NegativeObjectFilter("true"),
  ValueToRefine(?heap).
ObjectShouldNotBeRefined(?heap) :-
  !NegativeObjectFilter("true"),
  isValue(?heap),
  !ValueToRefine(?heap).
.decl ObjectShouldBeRefined(?heap:HeapAllocation)
ObjectShouldBeRefined(?heap) :-
  !NegativeObjectFilter("true"),
  ValueToRefine(?heap).
ObjectShouldBeRefined(?heap) :-
  NegativeObjectFilter("true"),
  isValue(?heap),
  !ValueToRefine(?heap).
.decl SiteShouldNotBeRefined(?invocation:MethodInvocation)
SiteShouldNotBeRefined(?invocation) :-
  !NegativeSiteFilter("true"),
  isMethodInvocation(?invocation),
  !SiteToRefine(?invocation).
SiteShouldNotBeRefined(?invocation) :-
  NegativeSiteFilter("true"),
  SiteToRefine(?invocation).
.decl SiteShouldBeRefined(?invocation:MethodInvocation)
SiteShouldBeRefined(?invocation) :-
  !NegativeSiteFilter("true"),
  SiteToRefine(?invocation).
SiteShouldBeRefined(?invocation) :-
  NegativeSiteFilter("true"),
  isMethodInvocation(?invocation),
  !SiteToRefine(?invocation).
.type Context = [ value1:Value, value2:Value, value3:Value ]
.type HContext = [ value1:Value, value2:Value, value3:Value ]
.decl EntryPoint(?method:Method)
.decl PossibleEntryPoint(?method:Method)
.decl ClassHasPossibleEntryPoint(?class:ReferenceType)
ClassHasPossibleEntryPoint(?class),
PossibleEntryPoint(?method) :-
  Method_DeclaringType(?method, ?class),
  Method_Modifier("public", ?method),
  !ClassModifier("private", ?class),
  !Method_Modifier("static", ?method).
.decl PrefixAbove(class:ReferenceType, str:symbol, ?len:number)
.decl PrefixBelow(class:ReferenceType, str:symbol)
PrefixAbove(?classAbove, substr(?classAbove, 0, ?lastDotPos+1), ?lastDotPos+1) :-
  ClassHasPossibleEntryPoint(?classAbove),
  LastDot(?classAbove, ?lastDotPos).
PrefixBelow(?classBelow, substr(?classBelow, 0, ?lastDotPos)) :-
  ClassHasPossibleEntryPoint(?classBelow),
  LastDot(?classBelow, ?lastDotPos).
.decl ClassIsAboveOtherInNamingHierarchy(?classAbove:ReferenceType, ?classBelow:ReferenceType)
ClassIsAboveOtherInNamingHierarchy(?classAbove, ?classBelow) :-
  PrefixAbove(?classAbove, ?prefixAbove, ?prefixLen),
  PrefixBelow(?classBelow, ?prefixBelow),
  substr(?prefixBelow, 0, ?prefixLen) = ?prefixAbove.
.decl ClassWithTopLevelEntryPoint(?class:ReferenceType)
.decl TopLevelEntryPoint(?method:Method)
ClassWithTopLevelEntryPoint(?class) :-
  ClassHasPossibleEntryPoint(?class),
  !ClassIsAboveOtherInNamingHierarchy(_, ?class).
TopLevelEntryPoint(?method) :-
  PossibleEntryPoint(?method),
  Method_DeclaringType(?method, ?class),
  ApplicationClass(?class),
  ClassWithTopLevelEntryPoint(?class).
EntryPoint(?method) :-
  TopLevelEntryPoint(?method).
.decl AllConcreteImplementations(?class:ClassType, ?type:Type)
.decl ConcreteType(?class:ClassType)
AllConcreteImplementations(?class, ?staticType) :-
  isClassType(?class),
  SubtypeOf(?class, ?staticType),
  !ClassModifier("abstract", ?class).
AllConcreteImplementations(?class, ?class) :-
  isClassType(?class),
  !ClassModifier("abstract", ?class).
AllConcreteImplementations(?type, ?type) :-
  isArrayType(?type).
ConcreteType(?type) :-
  AllConcreteImplementations(?type, _).
.decl ObjToMock(?class:ReferenceType)
.decl MockObjFromEntryPoint(?class:ReferenceType)
.decl MockObjFromArray(?class:ReferenceType)
MockObjFromEntryPoint(?class),
ObjToMock(?class) :-
  EntryPoint(?method),
  Method_DeclaringType(?method, ?class),
  isReferenceType(?class),
  !ClassModifier("abstract", ?class).
MockObjFromArray(?class),
ObjToMock(?class) :-
  ObjToMock(?type),
  isArrayType(?type),
  ComponentType(?type, ?componentType),
  StaticToActualType(?class, ?componentType).
.decl MockObjFromField(?fieldType:ReferenceType)
.decl MockObjectForType(?value:Value, ?staticType:Type)
MockObjectForType(?value, ?staticType) :-
  MockObject(?value, ?class),
  StaticToActualType(?class, ?staticType).
.decl MockObjectForComponentType(?value:Value, ?arrayType:ArrayType)
MockObjectForComponentType(?value, ?arrayType) :-
  ComponentType(?arrayType, ?componentType),
  MockObjectForType(?value, ?componentType).
ArrayIndexPointsTo(?hctx, ?componentValue, ?hctx, ?arrayValue) :-
  MockObjectContext(?hctx, ?arrayValue, ?arrayType),
  isArrayType(?arrayType),
  MockObjectForComponentType(?componentValue, ?arrayType).
.decl FormalsForEntryPoints(?method:Method, ?formal:Var)
FormalsForEntryPoints(?method, ?formal) :-
  EntryPoint(?method),
  FormalParam(_, ?method, ?formal).
.decl MockObjFromFormal(?type:ReferenceType)
.decl TypeForFormals(?formal:Var, ?method:Method, ?type:ReferenceType)
ObjToMock(?subtype),
MockObjFromFormal(?subtype),
TypeForFormals(?formal, ?method, ?subtype) :-
  FormalsForEntryPoints(?method, ?formal),
  Var_Type(?formal, ?staticType),
  StaticToActualType(?subtype, ?staticType).
.decl MockForFormal(?value:Value, ?formal:Var, ?type:ReferenceType, ?method:Method)
MockForFormal(?value, ?formal, ?type, ?method) :-
  TypeForFormals(?formal, ?method, ?type),
  MockObject(?value, ?type).
.decl MockObject(?value:Value, ?class:ReferenceType)
.decl MockObjectContext(?hctx:HContext, ?value:Value, ?class:ReferenceType)
.decl ContextForEntryPoint(?ctx:Context, ?method:Method)
.decl HContextForEntryPoint(?hctx:HContext, ?method:Method)
MockObjectContext(?hctx, ?value, ?class),
VarPointsTo(?hctx, ?value, ?ctx, ?formal) :-
  ContextForEntryPoint(?ctx, ?method),
  HContextForEntryPoint(?hctx, ?method),
  MockForFormal(?value, ?formal, ?class, ?method).
.decl ReceiverPointsTo(?value:Value, ?ctx:Context, ?receiver:Var, ?class:ReferenceType, ?method:Method)
HContextForEntryPoint(?hctx, ?method),
MockObjectContext(?hctx, ?value, ?class),
VarPointsTo(?hctx, ?value, ?calleeCtx, ?receiver) :-
  ?calleeCtx = [ctxValue1, ctxValue2, ctxValue3], ?hctx = [ctxValue1, ctxValue2, ctxValue3],
  ReceiverPointsTo(?value, ?calleeCtx, ?receiver, ?class, ?method).
ReceiverPointsTo(?value, ?calleeCtx, ?receiver, ?class, ?method),
ContextForEntryPoint(?calleeCtx, ?method) :-
  ThisVar(?method, ?receiver),
  Method_DeclaringType(?method, ?class),
  MockObjectForType(?value, ?class),
  isImmutableHContext(?immutablehctx),
  ?immutablehctx = [hctxValue1, hctxValue2, hctxValue3], ?calleeCtx = [hctxValue2, hctxValue3, ?value],
  EntryPoint(?method).
ReachableContext(?ctx, ?method) :-
  ContextForEntryPoint(?ctx, ?method).
.decl TypeToConcreteImplementationOrd(?staticType:Type, ?classOrd:number)
.decl ConcreteImplementations(?staticType:Type, ?class:ClassType)
TypeToConcreteImplementationOrd(?staticType, ?classOrd) :-
  AllConcreteImplementations(_, ?staticType),
  ?classOrd = min ord(?allClasses) : {
     AllConcreteImplementations(?allClasses, ?staticType)
   }.
ConcreteImplementations(?staticType, ?class) :-
  TypeToConcreteImplementationOrd(?staticType, ?classOrd),
  isType(?class),
  ord(?class) = ?classOrd.
.decl StaticToActualType(?class:ClassType, ?staticType:Type)
StaticToActualType(?class, ?staticType) :-
  ConcreteImplementations(?staticType, ?class),
  !ConcreteType(?staticType).
StaticToActualType(?type, ?type) :-
  ConcreteType(?type).
MockObject(cat(?class, "::: (Mock)"), ?class),
Value_isMock(cat(?class, "::: (Mock)")), isValue(cat(?class, "::: (Mock)")), Value_Type(cat(?class, "::: (Mock)"), ?class),
Value_DeclaringType(cat(?class, "::: (Mock)"), ?class) :-
  !MainMethodDeclaration(_),
  !AndroidAppComponent(_),
  ObjToMock(?class).
.decl Dacapo(?classNameHeap:StringConstant, method:Method)
isHeapAllocation(?heap), isStringConstant(?heap), HeapAllocation_Type(?heap, "java.lang.String"),
HeapAllocation_Keep(?heap),
Dacapo(?heap, ?method) :-
  _Dacapo(?heap, ?method).
VarPointsTo(?hctx, ?classNameHeap, ?ctx, ?to) :-
  Dacapo(?classNameHeap, ?dacapoMethod),
  MethodInvocation_Method(?invo, ?dacapoMethod),
  VirtualMethodInvocation_Base(?invo, ?base),
  Var_DeclaringMethod(?base, ?method),
  ReachableContext(?ctx, ?method),
  ImmutableHContextFromContext(?ctx, ?hctx),
  ActualParam(0, ?invo, ?to).
.decl Tamiflex_Class_NewInstance(?invocation:MethodInvocation, ?value:Value)
.decl Tamiflex_Constructor_NewInstance(?invocation:MethodInvocation, ?constructor:Method, ?value:Value)
.decl Tamiflex_Array_NewInstance(?invocation:MethodInvocation, ?value:Value)
.decl Tamiflex_Invoke(?callerCtx:Context, ?invocation:MethodInvocation, ?method:Method)
.decl Tamiflex_ReifiedField(?fld:Field, ?value:Value, ?invocation:MethodInvocation)
.decl Tamiflex_ReifiedFieldArray(?type:Type, ?value:Value, ?invocation:MethodInvocation)
.decl Tamiflex_ReifiedMethod(?method:Method, ?value:Value, ?invocation:MethodInvocation)
.decl Tamiflex_ReifiedMethodArray(?type:Type, ?value:Value, ?invocation:MethodInvocation)
LoadArrayIndex(?array, ?value, ?inmethod) :-
  ?sig = "<java.lang.reflect.Array: java.lang.Object get(java.lang.Object,int)>",
  isMethod(?sig),
  StaticMethodInvocation(?invocation, ?sig, ?inmethod),
  ActualParam(0, ?invocation, ?array),
  AssignReturnValue(?invocation, ?value).
StoreArrayIndex(?value, ?array, ?inmethod) :-
  ?sig = "<java.lang.reflect.Array: void set(java.lang.Object,int,java.lang.Object)>",
  isMethod(?sig),
  StaticMethodInvocation(?invocation, ?sig, ?inmethod),
  ActualParam(0, ?invocation, ?array),
  ActualParam(2, ?invocation, ?value).
LoadInstanceField(?base, ?fld, ?to, ?inmethod) :-
  ?sig = "<java.lang.reflect.Field: java.lang.Object get(java.lang.Object)>",
  isMethod(?sig),
  VirtualMethodInvocation(?invocation, ?sig, ?inmethod),
  Tamiflex_ReflectionMap(?fld, ?invocation),
  isField(?fld),
  ! Field_Modifier("static", ?fld),
  ActualParam(0, ?invocation, ?base),
  AssignReturnValue(?invocation, ?to).
LoadStaticField(?fld, ?to, ?inmethod) :-
  ?sig = "<java.lang.reflect.Field: java.lang.Object get(java.lang.Object)>",
  isMethod(?sig),
  VirtualMethodInvocation(?invocation, ?sig, ?inmethod),
  Tamiflex_ReflectionMap(?fld, ?invocation),
  isField(?fld),
  Field_Modifier("static", ?fld),
  AssignReturnValue(?invocation, ?to).
StoreInstanceField(?from, ?base, ?fld, ?inmethod) :-
  ?sig = "<java.lang.reflect.Field: void set(java.lang.Object,java.lang.Object)>",
  isMethod(?sig),
  VirtualMethodInvocation(?invocation, ?sig, ?inmethod),
  Tamiflex_ReflectionMap(?fld, ?invocation),
  isField(?fld),
  ! Field_Modifier("static", ?fld),
  ActualParam(0, ?invocation, ?base),
  ActualParam(1, ?invocation, ?from).
StoreStaticField(?from, ?fld, ?inmethod) :-
  ?sig = "<java.lang.reflect.Field: void set(java.lang.Object,java.lang.Object)>",
  isMethod(?sig),
  VirtualMethodInvocation(?invocation, ?sig, ?inmethod),
  Tamiflex_ReflectionMap(?fld, ?invocation),
  isField(?fld),
  Field_Modifier("static", ?fld),
  ActualParam(1, ?invocation, ?from).
Value_DeclaringType(?value, ?type) :-
  (Tamiflex_Class_NewInstance(?invocation, ?value) ;
   Tamiflex_Constructor_NewInstance(?invocation, _, ?value) ;
   Tamiflex_Array_NewInstance(?invocation, ?value)),
  Instruction_Method(?invocation, ?meth),
  Method_DeclaringType(?meth, ?type).
Value_DeclaringType(?value, ?type) :-
  (Tamiflex_ReifiedField(_, ?value, _) ;
   Tamiflex_ReifiedFieldArray(_, ?value, _) ;
   Tamiflex_ReifiedMethod(_, ?value, _) ;
   Tamiflex_ReifiedMethodArray(_, ?value, _)),
  Value_Type(?value, ?type).
Value_isMock(cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">")), isValue(cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">")), Value_Type(cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">"), ?type),
Tamiflex_Class_NewInstance(?invocation, cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">")) :-
  ?sig = "<java.lang.Class: java.lang.Object newInstance()>",
  isMethod(?sig),
  VirtualMethodInvocation(?invocation, ?sig, _),
  Tamiflex_ReflectionMap(?type, ?invocation),
  isInstruction(?invocation),
  isType(?type).
Value_isMock(cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">")), isValue(cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">")), Value_Type(cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">"), ?type),
Tamiflex_Constructor_NewInstance(?invocation, ?constructor, cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">")) :-
  ?sig = "<java.lang.reflect.Constructor: java.lang.Object newInstance(java.lang.Object[])>",
  isMethod(?sig),
  VirtualMethodInvocation(?invocation, ?sig, _),
  Tamiflex_ReflectionMap(?constructor, ?invocation),
  isInstruction(?invocation),
  isMethod(?constructor),
  Method_DeclaringType(?constructor, ?type),
  isType(?type).
Value_isMock(cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">")), isValue(cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">")), Value_Type(cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">"), ?type),
Tamiflex_Array_NewInstance(?invocation, cat(cat(cat(cat("<(Tamiflex) ", ?invocation), "/"), ?type), ">")) :-
  ?sig = "<java.lang.reflect.Array: java.lang.Object newInstance(java.lang.Class,int)>",
  isMethod(?sig),
  StaticMethodInvocation(?invocation, ?sig, _),
  Tamiflex_ReflectionMap(?type, ?invocation),
  isInstruction(?invocation),
  isType(?type).
Value_isMock(cat(cat("<(Tamiflex) ", ?fld), ">")), isValue(cat(cat("<(Tamiflex) ", ?fld), ">")), Value_Type(cat(cat("<(Tamiflex) ", ?fld), ">"), ?type),
Tamiflex_ReifiedField(?fld, cat(cat("<(Tamiflex) ", ?fld), ">"), ?invocation) :-
  (?sig = "<java.lang.Class: java.lang.reflect.Field getDeclaredField(java.lang.String)>" ;
   ?sig = "<java.lang.Class: java.lang.reflect.Field getField(java.lang.String)>" ),
  isMethod(?sig),
  VirtualMethodInvocation(?invocation, ?sig, _),
  Tamiflex_ReflectionMap(?fld, ?invocation),
  isField(?fld),
  ?type = "java.lang.reflect.Field",
  isType(?type).
Value_isMock(cat(cat("<(Tamiflex) ", ?type), "/Field[]>")), isValue(cat(cat("<(Tamiflex) ", ?type), "/Field[]>")), Value_Type(cat(cat("<(Tamiflex) ", ?type), "/Field[]>"), ?javaFieldArrayType),
Tamiflex_ReifiedFieldArray(?type, cat(cat("<(Tamiflex) ", ?type), "/Field[]>"), ?invocation) :-
  (?sig = "<java.lang.Class: java.lang.reflect.Field[] getDeclaredFields()>" ;
   ?sig = "<java.lang.Class: java.lang.reflect.Field[] getFields()>" ),
  isMethod(?sig),
  VirtualMethodInvocation(?invocation, ?sig, _),
  Tamiflex_ReflectionMap(?type, ?invocation),
  isType(?type),
  ?javaFieldArrayType = "java.lang.reflect.Field[]",
  isType(?javaFieldArrayType).
Value_isMock(cat(cat("<(Tamiflex) ", ?method), ">")), isValue(cat(cat("<(Tamiflex) ", ?method), ">")), Value_Type(cat(cat("<(Tamiflex) ", ?method), ">"), ?type),
Tamiflex_ReifiedMethod(?method, cat(cat("<(Tamiflex) ", ?method), ">"), ?invocation) :-
  (?sig = "<java.lang.Class: java.lang.reflect.Method getDeclaredMethod(java.lang.String,java.lang.Class[])>" ;
   ?sig = "<java.lang.Class: java.lang.reflect.Method getMethod(java.lang.String,java.lang.Class[])>" ),
  isMethod(?sig),
  VirtualMethodInvocation(?invocation, ?sig, _),
  Tamiflex_ReflectionMap(?method, ?invocation),
  isMethod(?method),
  ?type = "java.lang.reflect.Method",
  isType(?type).
Value_isMock(cat(cat("<(Tamiflex) ", ?type), "/Method[]>")), isValue(cat(cat("<(Tamiflex) ", ?type), "/Method[]>")), Value_Type(cat(cat("<(Tamiflex) ", ?type), "/Method[]>"), ?javaMethodArrayType),
Tamiflex_ReifiedMethodArray(?type, cat(cat("<(Tamiflex) ", ?type), "/Method[]>"), ?invocation) :-
  (?sig = "<java.lang.Class: java.lang.reflect.Method[] getDeclaredMethods()>" ;
   ?sig = "<java.lang.Class: java.lang.reflect.Method[] getMethods()>" ),
  isMethod(?sig),
  VirtualMethodInvocation(?invocation, ?sig, _),
  Tamiflex_ReflectionMap(?type, ?invocation),
  isType(?type),
  ?javaMethodArrayType = "java.lang.reflect.Method[]",
  isType(?javaMethodArrayType).
.decl TamiflexCallGraphEdge(?callerCtx:Context, ?invocation:MethodInvocation,
                            ?calleeCtx:Context, ?callee:Method)
ReachableContext(?calleeCtx, ?callee) :-
  TamiflexCallGraphEdge(_, _, ?calleeCtx, ?callee).
.decl OptForNameInvocation(?invocation:MethodInvocation, ?inmethod:Method)
OptForNameInvocation(?invocation, ?inmethod) :-
  (?sig = "<java.lang.Class: java.lang.Class forName(java.lang.String)>" ;
   ?sig = "<java.lang.Class: java.lang.Class forName(java.lang.String,boolean,java.lang.ClassLoader)>" ),
  isMethod(?sig),
  StaticMethodInvocation(?invocation, ?sig, ?inmethod).
VarPointsTo(?hctx, ?classObj, ?ctx, ?return) :-
  OptForNameInvocation(?invocation, ?inmethod),
  ReachableContext(?ctx, ?inmethod),
  ImmutableHContextFromContext(?ctx, ?hctx),
  Tamiflex_ReflectionMap(?class, ?invocation),
  ?classObj = cat(cat("<class ", ?class), ">"),
  isHeapAllocation(?classObj),
  HeapAllocation_Type(?classObj, "java.lang.Class"),
  AssignReturnValue(?invocation, ?return).
VarPointsTo(?hctx, ?value, ?ctx, ?return) :-
  (Tamiflex_Class_NewInstance(?invocation, ?value) ;
   Tamiflex_Array_NewInstance(?invocation, ?value) ),
  Instruction_Method(?invocation, ?inmethod),
  AssignReturnValue(?invocation, ?return),
  ReachableContext(?ctx, ?inmethod),
  ImmutableHContextFromContext(?ctx, ?hctx).
.decl TamiflexConstructorCallGraphEdge(?callerCtx:Context, ?invocation:MethodInvocation,
                                       ?calleeCtx:Context, ?callee:Method)
VarPointsTo(?hctx, ?value, ?callerCtx, ?return),
TamiflexCallGraphEdge(?callerCtx, ?invocation, ?calleeCtx, ?constructor),
TamiflexConstructorCallGraphEdge(?callerCtx, ?invocation, ?calleeCtx, ?constructor),
VarPointsTo(?hctx, ?value, ?calleeCtx, ?this) :-
  Tamiflex_Constructor_NewInstance(?invocation, ?constructor, ?value),
  Instruction_Method(?invocation, ?inmethod),
  ReachableContext(?callerCtx, ?inmethod),
  AssignReturnValue(?invocation, ?return),
  ThisVar(?constructor, ?this),
  ImmutableHContextFromContext(?callerCtx, ?hctx),
  ImmutableContextFromContext(?callerCtx, ?calleeCtx).
Tamiflex_Invoke(?callerCtx, ?invocation, ?method) :-
  ?sig = "<java.lang.reflect.Method: java.lang.Object invoke(java.lang.Object,java.lang.Object[])>",
  isMethod(?sig),
  VirtualMethodInvocation(?invocation, ?sig, _),
  Tamiflex_ReflectionMap(?method, ?invocation),
  isMethod(?method),
  Instruction_Method(?invocation, ?inmethod),
  ReachableContext(?callerCtx, ?inmethod).
TamiflexCallGraphEdge(?callerCtx, ?invocation, ?calleeCtx, ?callee),
VarPointsTo(?hctx, ?value, ?calleeCtx, ?this) :-
  Tamiflex_Invoke(?callerCtx, ?invocation, ?callee),
  ! Method_Modifier("static", ?callee),
  ActualParam(0, ?invocation, ?base),
  VarPointsTo(?hctx, ?value, ?callerCtx, ?base),
  ThisVar(?callee, ?this),
  ImmutableContextFromHContext(?hctx, ?calleeCtx).
TamiflexCallGraphEdge(?callerCtx, ?invocation, ?calleeCtx, ?callee) :-
   Tamiflex_Invoke(?callerCtx, ?invocation, ?callee),
   Method_Modifier("static", ?callee),
   ImmutableContextFromContext(?callerCtx, ?calleeCtx).
OptInterproceduralAssign(?callerCtx, ?local, ?calleeCtx, ?return) :-
  Tamiflex_Invoke(?callerCtx, ?invocation, ?callee),
  AssignReturnValue(?invocation, ?local),
  ReturnVar(?return, ?callee),
  ImmutableContextFromContext(?callerCtx, ?calleeCtx).
.decl TamiflexInvocationFirstParam(?calleeCtx:Context, ?formal:Var,
                                   ?callerCtx:Context, ?argsParam:Var)
TamiflexInvocationFirstParam(?calleeCtx, ?formal, ?callerCtx, ?argsParam) :-
  Tamiflex_Invoke(?callerCtx, ?invocation, ?callee),
  ActualParam(1, ?invocation, ?argsParam),
  FormalParam(_, ?callee, ?formal),
  ImmutableContextFromContext(?callerCtx, ?calleeCtx).
TamiflexInvocationFirstParam(?calleeCtx, ?formal, ?callerCtx, ?argsParam) :-
  TamiflexConstructorCallGraphEdge(?callerCtx, ?invocation, ?calleeCtx, ?callee),
  ActualParam(0, ?invocation, ?argsParam),
  FormalParam(_, ?callee, ?formal).
.decl TamiflexInvocationArgumentArrayValue(?calleeCtx:Context, ?formal:Var,
                                           ?basehctx:HContext, ?basevalue:Value)
TamiflexInvocationArgumentArrayValue(?calleeCtx, ?formal, ?basehctx, ?basevalue) :-
  TamiflexInvocationFirstParam(?calleeCtx, ?formal, ?ctx, ?base),
  VarPointsTo(?basehctx, ?basevalue, ?ctx, ?base).
VarPointsTo(?hctx, ?value, ?calleeCtx, ?formal) :-
  TamiflexInvocationArgumentArrayValue(?calleeCtx, ?formal, ?basehctx, ?basevalue),
  ArrayIndexPointsTo(?hctx, ?value, ?basehctx, ?basevalue),
  Var_Type(?formal, ?type),
  Value_Type(?value, ?valuetype),
  SupertypeOf(?type, ?valuetype).
VarPointsTo(?hctx, ?value, ?ctx, ?return) :-
  (Tamiflex_ReifiedField(_, ?value, ?invocation) ;
   Tamiflex_ReifiedFieldArray(_, ?value, ?invocation) ;
   Tamiflex_ReifiedMethod(_, ?value, ?invocation) ;
   Tamiflex_ReifiedMethodArray(_, ?value, ?invocation) ),
  Instruction_Method(?invocation, ?inmethod),
  ReachableContext(?ctx, ?inmethod),
  ImmutableHContextFromContext(?ctx, ?hctx),
  AssignReturnValue(?invocation, ?return).
MainClass("Harness").
.decl Stats_Simple_InsensVarPointsTo(?value:Value, ?var:Var)
.output Stats_Simple_InsensVarPointsTo
.decl Stats_Simple_AssignedVariable(?var:Var)
.output Stats_Simple_AssignedVariable
.decl Stats_Simple_Application_InsensVarPointsTo(?value:Value, ?var:Var)
.output Stats_Simple_Application_InsensVarPointsTo
.decl Stats_Simple_Application_VarPointsTo(?hctx:HContext, ?value:Value, ?ctx:Context, ?var:Var)
.output Stats_Simple_Application_VarPointsTo
.decl Stats_Simple_InsensReachableVar(?var:Var)
.output Stats_Simple_InsensReachableVar
.decl Stats_Simple_ReachableVar(?ctx:Context, ?var:Var)
.output Stats_Simple_ReachableVar
.decl Stats_Simple_InsensArrayIndexPointsTo(?value:Value, ?basevalue:Value)
.output Stats_Simple_InsensArrayIndexPointsTo
.decl Stats_Simple_Application_InsensArrayIndexPointsTo(?value:Value, ?basevalue:Value)
.output Stats_Simple_Application_InsensArrayIndexPointsTo
.decl Stats_Simple_Application_ArrayIndexPointsTo(?hctx:HContext, ?value:Value, ?baseHCtx:HContext, ?basevalue:Value)
.output Stats_Simple_Application_ArrayIndexPointsTo
.decl Stats_Simple_InsensInstanceFieldPointsTo(?value:Value, ?sig:Field, ?basevalue:Value)
.output Stats_Simple_InsensInstanceFieldPointsTo
.decl Stats_Simple_InsensStaticFieldPointsTo(?value:Value, ?sig:Field)
.output Stats_Simple_InsensStaticFieldPointsTo
.decl Stats_Simple_Application_InsensInstanceFieldPointsTo(?value:Value, ?sig:Field, ?basevalue:Value)
.output Stats_Simple_Application_InsensInstanceFieldPointsTo
.decl Stats_Simple_Application_InstanceFieldPointsTo(?hctx:HContext, ?value:Value, ?sig:Field, ?baseHCtx:HContext, ?basevalue:Value)
.output Stats_Simple_Application_InstanceFieldPointsTo
.decl Stats_Simple_InsensCallGraphEdge(?from:MethodInvocation, ?to:Method)
.output Stats_Simple_InsensCallGraphEdge
.decl Stats_Simple_VirtualCallGraphEdge(?from:MethodInvocation, ?to:Method)
.output Stats_Simple_VirtualCallGraphEdge
.decl Stats_Simple_InsensReachableApplicationMethod(?method:Method)
.output Stats_Simple_InsensReachableApplicationMethod
.decl Stats_Simple_ReachableApplicationMethod(?ctx:Context, ?method:Method)
.output Stats_Simple_ReachableApplicationMethod
.decl Stats_Simple_ApplicationConcreteMethod(?method:Method)
.output Stats_Simple_ApplicationConcreteMethod
.decl Stats_Simple_NonReachableApplicationConcreteMethod(?method:Method)
.output Stats_Simple_NonReachableApplicationConcreteMethod
.decl Stats_Simple_ReachableVirtualMethodInvocation(?invocation:MethodInvocation)
.output Stats_Simple_ReachableVirtualMethodInvocation
.decl Stats_Simple_Application_ReachableVirtualMethodInvocation(?invocation:MethodInvocation)
.output Stats_Simple_Application_ReachableVirtualMethodInvocation
.decl Stats_Simple_VirtualTargets(?invocation:MethodInvocation, ?c:number)
.decl Stats_Simple_PolymorphicCallSite(?invocation:MethodInvocation)
.output Stats_Simple_PolymorphicCallSite
.decl Stats_Simple_NullVirtualMethodInvocation(?invocation:MethodInvocation)
.output Stats_Simple_NullVirtualMethodInvocation
.decl Stats_Simple_EmptyVirtualMethodInvocation(?invocation:MethodInvocation)
.output Stats_Simple_EmptyVirtualMethodInvocation
.decl Stats_Simple_Application_VirtualMethodInvocation(?invocation:MethodInvocation)
.output Stats_Simple_Application_VirtualMethodInvocation
.decl Stats_Simple_Application_PolymorphicCallSite(?invocation:MethodInvocation)
.output Stats_Simple_Application_PolymorphicCallSite
.decl Stats_Simple_Application_NullVirtualMethodInvocation(?invocation:MethodInvocation)
.output Stats_Simple_Application_NullVirtualMethodInvocation
.decl Stats_Simple_Application_EmptyVirtualMethodInvocation(?invocation:MethodInvocation)
.output Stats_Simple_Application_EmptyVirtualMethodInvocation
.decl Stats_Simple_ReachableCast(?inmethod:Method, ?type:Type, ?to:Var, ?from:Var)
.output Stats_Simple_ReachableCast
.decl Stats_Simple_PotentiallyFailingCast(?type:Type, ?from:Var, ?to:Var)
.output Stats_Simple_PotentiallyFailingCast
.decl Stats_Simple_Application_Cast(?type:Type, ?from:Var, ?to:Var, ?inmethod:Method)
.output Stats_Simple_Application_Cast
.decl Stats_Simple_Application_ReachableCast(?inmethod:Method, ?type:Type, ?to:Var, ?from:Var)
.output Stats_Simple_Application_ReachableCast
.decl Stats_Simple_Application_ReachableMethod(?method:Method)
.output Stats_Simple_Application_ReachableMethod
.decl Stats_Simple_Application_PotentiallyFailingCast(?type:Type, ?from:Var, ?to:Var)
.output Stats_Simple_Application_PotentiallyFailingCast
Stats_Simple_InsensVarPointsTo(?value, ?var) :-
  VarPointsTo(_, ?value, _, ?var).
Stats_Simple_AssignedVariable(?var) :-
  Stats_Simple_InsensVarPointsTo(_, ?var).
Stats_Simple_Application_InsensVarPointsTo(?value, ?var),
Stats_Simple_Application_VarPointsTo(?hctx, ?value, ?ctx, ?var) :-
  ApplicationVar(?var),
  VarPointsTo(?hctx, ?value, ?ctx, ?var).
Stats_Simple_InsensReachableVar(?var),
Stats_Simple_ReachableVar(?ctx, ?var) :-
  Stats_Simple_AssignedVariable(?var),
  Var_DeclaringMethod(?var, ?method),
  ReachableContext(?ctx, ?method).
Stats_Simple_InsensArrayIndexPointsTo(?value, ?basevalue) :-
   ArrayIndexPointsTo(_, ?value, _, ?basevalue).
Stats_Simple_Application_InsensArrayIndexPointsTo(?value, ?basevalue),
Stats_Simple_Application_ArrayIndexPointsTo(?hctx, ?value, ?baseHCtx, ?basevalue) :-
  ApplicationMethod(?meth),
  AssignNormalHeapAllocation(?basevalue, _, ?meth),
  ArrayIndexPointsTo(?hctx, ?value, ?baseHCtx, ?basevalue).
Stats_Simple_InsensInstanceFieldPointsTo(?value, ?sig, ?basevalue) :-
  InstanceFieldPointsTo(_, ?value, ?sig, _, ?basevalue).
Stats_Simple_InsensStaticFieldPointsTo(?value, ?sig) :-
  StaticFieldPointsTo(_, ?value, ?sig).
Stats_Simple_Application_InsensInstanceFieldPointsTo(?value, ?sig, ?basevalue),
Stats_Simple_Application_InstanceFieldPointsTo(?hctx, ?value, ?sig, ?baseHCtx, ?basevalue) :-
  ApplicationMethod(?meth),
  AssignNormalHeapAllocation(?basevalue, _, ?meth),
  InstanceFieldPointsTo(?hctx, ?value, ?sig, ?baseHCtx, ?basevalue).
Stats_Simple_InsensCallGraphEdge(?from, ?to) :-
   CallGraphEdge(_, ?from, _, ?to).
Stats_Simple_VirtualCallGraphEdge(?from, ?to) :-
   Stats_Simple_ReachableVirtualMethodInvocation(?from),
   Stats_Simple_InsensCallGraphEdge(?from, ?to).
Stats_Simple_InsensReachableApplicationMethod(?method),
Stats_Simple_ReachableApplicationMethod(?ctx, ?method) :-
  ApplicationMethod(?method),
  ReachableContext(?ctx, ?method).
Stats_Simple_ApplicationConcreteMethod(?method) :-
  ApplicationMethod(?method),
  !Method_Modifier("abstract", ?method).
Stats_Simple_NonReachableApplicationConcreteMethod(?method) :-
  Stats_Simple_ApplicationConcreteMethod(?method),
  !Stats_Simple_InsensReachableApplicationMethod(?method).
Stats_Simple_ReachableVirtualMethodInvocation(?invocation) :-
  Reachable(?method),
  Instruction_Method(?invocation, ?method),
  isVirtualMethodInvocation_Insn(?invocation).
Stats_Simple_Application_ReachableVirtualMethodInvocation(?invocation) :-
  Stats_Simple_InsensReachableApplicationMethod(?method),
  Instruction_Method(?invocation, ?method),
  isVirtualMethodInvocation_Insn(?invocation).
Stats_Simple_VirtualTargets(?from, ?c) :-
  Stats_Simple_VirtualCallGraphEdge(?from, _),
  ?c = count : Stats_Simple_VirtualCallGraphEdge(?from, _).
Stats_Simple_PolymorphicCallSite(?from) :-
  Stats_Simple_VirtualTargets(?from, ?size),
  ?size > 1.
Stats_Simple_NullVirtualMethodInvocation(?invocation) :-
  Value_Null(?null),
  Stats_Simple_InsensVarPointsTo(?null, ?base),
  VirtualMethodInvocation_Base(?invocation, ?base),
  Stats_Simple_ReachableVirtualMethodInvocation(?invocation).
Stats_Simple_EmptyVirtualMethodInvocation(?invocation) :-
  Stats_Simple_ReachableVirtualMethodInvocation(?invocation),
  VirtualMethodInvocation_Base(?invocation, ?base),
  !Stats_Simple_InsensVarPointsTo(_, ?base).
Stats_Simple_Application_VirtualMethodInvocation(?invocation) :-
  ApplicationMethod(?method),
  Instruction_Method(?invocation, ?method),
  isVirtualMethodInvocation_Insn(?invocation).
Stats_Simple_Application_PolymorphicCallSite(?from) :-
  Stats_Simple_PolymorphicCallSite(?from),
  Stats_Simple_Application_ReachableVirtualMethodInvocation(?from).
Stats_Simple_Application_NullVirtualMethodInvocation(?invocation) :-
  Value_Null(?null),
  Stats_Simple_InsensVarPointsTo(?null, ?base),
  VirtualMethodInvocation_Base(?invocation, ?base),
  Stats_Simple_Application_ReachableVirtualMethodInvocation(?invocation).
Stats_Simple_Application_EmptyVirtualMethodInvocation(?invocation) :-
  Stats_Simple_Application_ReachableVirtualMethodInvocation(?invocation),
  VirtualMethodInvocation_Base(?invocation, ?base),
  !Stats_Simple_InsensVarPointsTo(_, ?base).
Stats_Simple_ReachableCast(?inmethod, ?type, ?to, ?from) :-
  Stats_Simple_AssignedVariable(?from),
  AssignCast(?type, ?from, ?to, ?inmethod),
  Reachable(?inmethod).
Stats_Simple_PotentiallyFailingCast(?type, ?from, ?to) :-
  Stats_Simple_ReachableCast(_, ?type, ?to, ?from),
  Stats_Simple_InsensVarPointsTo(?value, ?from),
  Value_Type(?value, ?valuetype),
  !SupertypeOf(?type, ?valuetype).
Stats_Simple_Application_Cast(?type, ?from, ?to, ?inmethod) :-
  ApplicationMethod(?inmethod),
  AssignCast(?type, ?from, ?to, ?inmethod).
Stats_Simple_Application_ReachableCast(?inmethod, ?type, ?to, ?from) :-
  ApplicationMethod(?inmethod),
  Stats_Simple_ReachableCast(?inmethod, ?type, ?to, ?from).
Stats_Simple_Application_ReachableMethod(?method) :-
  Reachable(?method),
  ApplicationMethod(?method).
Stats_Simple_Application_PotentiallyFailingCast(?type, ?from, ?to) :-
  Stats_Simple_Application_ReachableCast(_, ?type, ?to, ?from),
  Stats_Simple_InsensVarPointsTo(?value, ?from),
  Value_Type(?value, ?valuetype),
  !SupertypeOf(?type, ?valuetype).
Stats_Metrics("1.0", "var points-to (INS)", c) :- c = count : { Stats_Simple_InsensVarPointsTo(_, _) }.
Stats_Metrics("1.5", "var points-to (SENS)", c) :- c = count : { VarPointsTo(_, _, _, _) }.
Stats_Metrics("5.0", "app var points-to (INS)", c) :- c = count : { Stats_Simple_Application_InsensVarPointsTo(_, _) }.
Stats_Metrics("5.5", "app var points-to (SENS)", c) :- c = count : { Stats_Simple_Application_VarPointsTo(_, _, _, _) }.
Stats_Metrics("10.0", "reachable variables (INS)", c) :- c = count : { Stats_Simple_InsensReachableVar(_) }.
Stats_Metrics("10.5", "reachable variables (SENS)", c) :- c = count : { Stats_Simple_ReachableVar(_, _) }.
Stats_Metrics("2.0", "array index points-to (INS)", c) :- c = count : { Stats_Simple_InsensArrayIndexPointsTo(_, _) }.
Stats_Metrics("2.5", "array index points-to (SENS)", c) :- c = count : { ArrayIndexPointsTo(_, _, _, _) }.
Stats_Metrics("6.0", "app array index points-to (INS)", c) :- c = count : { Stats_Simple_Application_InsensArrayIndexPointsTo(_, _) }.
Stats_Metrics("6.5", "app array index points-to (SENS)", c) :- c = count : { Stats_Simple_Application_ArrayIndexPointsTo(_, _, _, _) }.
Stats_Metrics("3.0", "instance field points-to (INS)", c) :- c = count : { Stats_Simple_InsensInstanceFieldPointsTo(_, _, _) }.
Stats_Metrics("3.5", "instance field points-to (SENS)", c) :- c = count : { InstanceFieldPointsTo(_, _, _, _, _) }.
Stats_Metrics("4.0", "static field points-to (INS)", c) :- c = count : { Stats_Simple_InsensStaticFieldPointsTo(_, _) }.
Stats_Metrics("4.5", "static field points-to (SENS)", c) :- c = count : { StaticFieldPointsTo(_, _, _) }.
Stats_Metrics("7.0", "app instance field points-to (INS)", c) :- c = count : { Stats_Simple_Application_InsensInstanceFieldPointsTo(_, _, _) }.
Stats_Metrics("7.5", "app instance field points-to (SENS)", c) :- c = count : { Stats_Simple_Application_InstanceFieldPointsTo(_, _, _, _, _) }.
Stats_Metrics("8.0", "call graph edges (INS)", c) :- c = count : { Stats_Simple_InsensCallGraphEdge(_, _) }.
Stats_Metrics("8.5", "call graph edges (SENS)", c) :- c = count : { CallGraphEdge(_, _, _, _) }.
Stats_Metrics("9.0", "non-reachable app concrete methods", c) :- c = count : { Stats_Simple_NonReachableApplicationConcreteMethod(_) }.
Stats_Metrics("11.0", "reachable methods (INS)", c) :- c = count : { Reachable(_) }.
Stats_Metrics("11.5", "reachable methods (SENS)", c) :- c = count : { ReachableContext(_, _) }.
Stats_Metrics("12.0", "virtual call sites (statically)", c) :- c = count : { isVirtualMethodInvocation_Insn(_) }.
Stats_Metrics("13.0", "reachable virtual call sites", c) :- c = count : { Stats_Simple_ReachableVirtualMethodInvocation(_) }.
Stats_Metrics("14.0", "polymorphic virtual call sites", c) :- c = count : { Stats_Simple_PolymorphicCallSite(_) }.
Stats_Metrics("15.0", "null virtual call sites", c) :- c = count : { Stats_Simple_NullVirtualMethodInvocation(_) }.
Stats_Metrics("15.5", "empty virtual call sites", c) :- c = count : { Stats_Simple_EmptyVirtualMethodInvocation(_) }.
Stats_Metrics("16.0", "app virtual call sites (statically)", c) :- c = count : { Stats_Simple_Application_VirtualMethodInvocation(_) }.
Stats_Metrics("17.0", "app reachable virtual call sites", c) :- c = count : { Stats_Simple_Application_ReachableVirtualMethodInvocation(_) }.
Stats_Metrics("18.0", "app polymorphic virtual call sites", c) :- c = count : { Stats_Simple_Application_PolymorphicCallSite(_) }.
Stats_Metrics("19.0", "app null virtual call sites", c) :- c = count : { Stats_Simple_Application_NullVirtualMethodInvocation(_) }.
Stats_Metrics("19.5", "app empty virtual call sites", c) :- c = count : { Stats_Simple_Application_EmptyVirtualMethodInvocation(_) }.
Stats_Metrics("20.0", "casts (statically)", c) :- c = count : { AssignCast(_, _, _, _) }.
Stats_Metrics("21.0", "reachable casts", c) :- c = count : { Stats_Simple_ReachableCast(_, _, _, _) }.
Stats_Metrics("22.0", "reachable casts that may fail", c) :- c = count : { Stats_Simple_PotentiallyFailingCast(_, _, _) }.
Stats_Metrics("23.0", "app casts (statically)", c) :- c = count : { Stats_Simple_Application_Cast(_, _, _, _) }.
Stats_Metrics("24.0", "app reachable casts", c) :- c = count : { Stats_Simple_Application_ReachableCast(_, _, _, _) }.
Stats_Metrics("25.0", "app reachable casts that may fail", c) :- c = count : { Stats_Simple_Application_PotentiallyFailingCast(_, _, _) }.
Stats_Metrics("25.5", "app reachable methods", c) :- c = count : { Stats_Simple_Application_ReachableMethod(_) }.
.decl UnfoldedContext(?ctx:Context, ?x1:Value, ?x2:Value, ?x3:Value)
UnfoldedContext([?x1, ?x2, ?x3], ?x1, ?x2, ?x3) :-
	VarPointsTo(_, _, [?x1, ?x2, ?x3], _).
.decl UnfoldedHContext(?hctx:HContext, ?x1:Value, ?x2:Value, ?x3:Value)
UnfoldedHContext([?x1, ?x2, ?x3], ?x1, ?x2, ?x3) :-
	VarPointsTo([?x1, ?x2, ?x3], _, _, _).
//.output UnfoldedContext()
//.output UnfoldedHContext()
.output Value_Type()
.output OptVirtualMethodInvocationBase()
//.output ResolveInvocation()
//.output ThisVar()
.output ThrowPointsTo()
.output StoreHeapInstanceField()
//.output MethodInvocation_Method()
.output Throw()
//.output OptLoadArrayIndex()
//.output AssignContextInsensitiveHeapAllocation()
//.output ReachableContext()
//.output ImmutableContextFromContext()
//.output ImmutableHContextFromContext()
//.output OptSpecialMethodInvocationBase()
//.output Tamiflex_Constructor_NewInstance()
//.output LoadInstanceField()
//.output isContext()
.output Instruction_Throws()
.output InstanceFieldPointsTo()
//.output OptStoreIntoArray()