How to debug KeyError: 'the_predicate'?

[anantoni]

Hi,

I am trying to do an evaluation of Logica for program analysis. For the most part, I was able to debug my program by removing rules and re-adding them, but now I'm stuck with the following error:

I don't know if it's of any help, but here is my program (I'd love to share the facts too, but some files are too large for Git/Git-LFS.

@Engine("duckdb");

@Ground(AssignHeapAllocation);
AssignHeapAllocation(..r) :-
    `('./facts/AssignHeapAllocation.csv')`(..r);

@Ground(ActualParam);
ActualParam(..r) :-
    `('./facts/ActualParam.csv')`(..r);

@Ground(AssignLocal);
AssignLocal(..r) :-
    `('./facts/AssignLocal.csv')`(..r);

@Ground(ApplicationClass);
ApplicationClass(..r) :-
    `('./facts/ApplicationClass.csv')`(..r);

@Ground(MainClass);
MainClass(..r) :-
    `('./facts/MainClass.csv')`(..r);

@Ground(Method);
Method(..r) :-
    `('./facts/Method.csv')`(..r);

@Ground(FormalParam);
FormalParam(..r) :-
    `('./facts/FormalParam.csv')`(..r);

@Ground(Var_Type);
Var_Type(..r) :-
    `('./facts/Var-Type.csv')`(..r);

@Ground(VirtualMethodInvocation);
VirtualMethodInvocation(..r) :-
    `('./facts/VirtualMethodInvocation.csv')`(..r);

@Ground(SpecialMethodInvocation);
SpecialMethodInvocation(..r) :-
    `('./facts/SpecialMethodInvocation.csv')`(..r);

@Ground(StaticMethodInvocation);
StaticMethodInvocation(..r) :-
    `('./facts/StaticMethodInvocation.csv')`(..r);

@Ground(StoreArrayIndex);
StoreArrayIndex(..r) :-
    `('./facts/StoreArrayIndex.csv')`(..r);

@Ground(LoadArrayIndex);
LoadArrayIndex(..r) :-
    `('./facts/LoadArrayIndex.csv')`(..r);

@Ground(StoreStaticField);
StoreStaticField(..r) :-
    `('./facts/StoreStaticField.csv')`(..r);

@Ground(LoadStaticField);
LoadStaticField(..r) :-
    `('./facts/LoadStaticField.csv')`(..r);

@Ground(StoreInstanceField);
StoreInstanceField(..r) :-
    `('./facts/StoreInstanceField.csv')`(..r);

@Ground(LoadInstanceField);
LoadInstanceField(..r) :-
    `('./facts/LoadInstanceField.csv')`(..r);

@Ground(HeapAllocation_Type);
HeapAllocation_Type(..r) :-
    `('./facts/HeapAllocation_Type.csv')`(..r);

@Ground(DirectSuperclass);
DirectSuperclass(..r) :-
    `('./facts/DirectSuperclass.csv')`(..r);

isClassType(class1:) distinct :-
    DirectSuperclass(class:, superclass:),
    class1 == class;
isClassType(class1:) distinct :-    
    DirectSuperclass(class:, superclass:),
    class1 == superclass;

/**
 * Subtyping
 */
DirectSubclass(class, superclass) distinct :-
    DirectSuperclass(class:, superclass:);

/**
 * A class A is a subclass of a class C if A is a direct subclass of C
 */
Subclass(c, class1) distinct :-
    DirectSubclass(class1, c);

/**
 * A class A is a subclass of a class C if there is a direct subclass B of C and class A is a subclass of B
 */
Subclass(c, class1) distinct :-
    Subclass(b, class1),
    DirectSubclass(b, c);

/**
 * A Class A is a superclass of class C whenever C is a subclass of A
 */
Superclass(c, class1) distinct :-
    Subclass(class1, c);

/**
 * The following rules check whether type S can be cast to type T. Implicitly,
 * they expose the type hierarchy.
 */
SupertypeOf(s, t) distinct :-
    SubtypeOf(t, s);

/**
 * If S is an ordinary (nonarray) class, then
 * - S must be the same class as T
 * - or a subclass of T
 */
SubtypeOf(s, s) distinct :-
    isClassType(s);

SubtypeOf(s, t) distinct :-
    Subclass(t, s);

/**
 * If T is an interface type, then
 * - S must implement interface T
 */
SubtypeOf(s, t) distinct :-
    isClassType(s),
    Superinterface(t, s);

/**
 * If S is an interface type, then
 * - If T is a class type, then T must be Object
 */
SubtypeOf(s, t) distinct :-
    isInterfaceType(s),
    isType(t),
    t == "java.lang.Object";

/**
 * If T is an interface type, then
 * - T must be the same interface as S
 * - or a superinterface of S
 */
SubtypeOf(s, s) distinct :-
    isInterfaceType(s);

SubtypeOf(s, t) distinct :-
    isInterfaceType(s),
    Superinterface(t, s);

/**
 *  If S is a class representing the array type SC[], that is, an array of
 *  components of type SC, then
 *  - If T is a class type, then T must be Object
 */
SubtypeOf(s, t) distinct :-
    isArrayType(s),
    isType(t),
    t == "java.lang.Object";

/**
 *  If T is an array type TC[], that is, an array of components of type TC,
 *  then one of the following must be true
 *  - TC and SC are the same primitive type
 */
SubtypeOf(s, t) distinct :-
    isArrayType(s),
    isArrayType(t),
    ComponentType(s, sc),
    ComponentType(t, sc),
    isPrimitiveType(sc);

MethodInvocation_Method(instruction, signature) distinct :-
    StaticMethodInvocation(instruction, _, signature, _);

MethodInvocation_Method(instruction, signature) distinct :-
    SpecialMethodInvocation(instruction, _, signature, _, _);

MethodInvocation_Method(instruction, signature) distinct :-
    VirtualMethodInvocation(instruction, _, signature, _, _);

VirtualMethodInvocation_Base(instruction, base) distinct :-
    VirtualMethodInvocation(instruction, _, signature, base, _);

SpecialMethodInvocation_Base(instruction, base) distinct :-
    SpecialMethodInvocation(instruction, _, signature, base, _);

VirtualMethodInvocation_BaseType(invocation, basetype) distinct :-
    VirtualMethodInvocation_Base(invocation, base),
    Var_Type(base, basetype);

ResolveInvocation(type, invocation, tomethod) distinct :-
    VirtualMethodInvocation_SimpleName(invocation, simplename),
    VirtualMethodInvocation_Descriptor(invocation, descriptor),
    VirtualMethodInvocation_BaseType(invocation, basetype),
    SubtypeOf(type, basetype),
    MethodLookup(simplename, descriptor, type, tomethod);

ResolveInvocation(basetype, invocation, tomethod) distinct :-
    SuperMethodInvocation_SimpleName(invocation, simplename),
    SuperMethodInvocation_Descriptor(invocation, descriptor),
    SuperMethodInvocation_Base(invocation, base),
    Var_Type(base, basetype),
    DirectSuperclass(basetype, supertype),
    MethodLookup(simplename, descriptor, supertype, tomethod);

ConcreteMethodDeclared(meth, class) distinct :-
    isClassType(class),
    Method_DeclaringType(meth, class),
    !Method_Modifier("abstract", meth);

MethodDeclaredOrInherited(meth, class) distinct :-
  Method_DeclaringType(meth, class);

MethodDeclaredOrInherited(meth, class) distinct :-
  MethodDeclaredOrInherited(meth, superclass),
  DirectSuperclass(class, superclass);

MethodDeclaredOrInherited(meth, class) distinct :-
  MethodDeclaredOrInherited(meth, superinterface),
  !Method_Modifier("abstract", meth),
  DirectSuperinterface(class, superinterface);

MethodsOfSameOrSuperType(method1, method2) distinct :-
  MethodDeclaredOrInherited(method1, class),
  MethodDeclaredOrInherited(method2, class);

MethodsOfSameNonSDKType(method1, method2, class) distinct :-
  Method_DeclaringType(method1, class),
  !match("java.*", class),
  !match("sun.*", class),
  Method_DeclaringType(method2, class);

/**
 * Invocation assignments
 */

Assign(class1ctual, formal) distinct :-
   CallGraphEdge(invocation, method),
   FormalParam(index, method, formal),
   ActualParam(index, invocation, class1ctual);

Assign(return, local) distinct :-
   CallGraphEdge(invocation, method),
   ReturnVar(return, method),
   AssignReturnValue(invocation, local);

VarPointsTo(heap, var) distinct :-
  AssignHeapAllocation(heap, var, inmethod),
  Reachable(inmethod);

/**
 *  Variable points to heap object via assignment
 */

VarPointsTo(heap, to) distinct :-
   Assign(from, to),
   VarPointsTo(heap, from);

/**
 *  Local Assignments
 */

VarPointsTo(heap, to) distinct :-
   Reachable(inmethod),
   AssignLocal(from, to, inmethod),
   VarPointsTo(heap, from);

/**
 * Cast Assignments
 */

VarPointsTo(heap, to) distinct :-
    Reachable(method),
    AssignCast(type, from, to, method),
    SupertypeOf(type, heaptype),
    HeapAllocation_Type(heap, heaptype),
    VarPointsTo(heap, from);

/**
 * Arrays
 */

ArrayIndexPointsTo(baseheap, heap) distinct :-
   Reachable(inmethod),
   StoreArrayIndex(from, base, inmethod),
   VarPointsTo(baseheap, base),
   VarPointsTo(heap, from),
   HeapAllocation_Type(heap, heaptype),
   HeapAllocation_Type(baseheap, baseheaptype),
   ComponentType(baseheaptype, componenttype),
   SupertypeOf(componenttype, heaptype);

VarPointsTo(heap, to) distinct :-
   Reachable(inmethod),
   LoadArrayIndex(base, to, inmethod),
   VarPointsTo(baseheap, base),
   ArrayIndexPointsTo(baseheap, heap),
   Var_Type(to, type),
   HeapAllocation_Type(baseheap, baseheaptype),
   ComponentType(baseheaptype, basecomponenttype),
   SupertypeOf(type, basecomponenttype);

/**
 * Load instance fields
 */

VarPointsTo(heap, to) distinct :-
   Reachable(inmethod),
   LoadInstanceField(base, signature, to, inmethod),
   VarPointsTo(baseheap, base),
   InstanceFieldPointsTo(heap, signature, baseheap);

/**
 * Store instance fields
 */

InstanceFieldPointsTo(heap, fld, baseheap) distinct :-
  Reachable(inmethod),
  StoreInstanceField(from, base, fld, inmethod),
  VarPointsTo(heap, from),
  VarPointsTo(baseheap, base);

/**
 * Load static fields
 */

VarPointsTo(heap, to) distinct :-
  Reachable(inmethod),
  LoadStaticField(fld, to, inmethod),
  StaticFieldPointsTo(heap, fld);

/**
 * Store static fields
 */

StaticFieldPointsTo(heap, fld) distinct :-
    Reachable(inmethod),
    StoreStaticField(from, fld, inmethod),
    VarPointsTo(heap, from);

VarPointsTo(heap, this) distinct :-
  Reachable(inmethod),
  Instruction_Method(invocation, inmethod),
  VirtualMethodInvocation_Base(invocation, base),
  VarPointsTo(heap, base),
  HeapAllocation_Type(heap, heaptype),
  VirtualMethodInvocation_SimpleName(invocation, simplename),
  VirtualMethodInvocation_Descriptor(invocation, descriptor),
  MethodLookup(simplename, descriptor, heaptype, tomethod),
  ThisVar(tomethod, this);

/**
 *   Call graph creation
 **/

Reachable(tomethod) distinct :-
  Reachable(inmethod),
  Instruction_Method(invocation, inmethod),
  VirtualMethodInvocation_Base(invocation, base),
  VarPointsTo(heap, base),
  HeapAllocation_Type(heap, heaptype),
  VirtualMethodInvocation_SimpleName(invocation, simplename),
  VirtualMethodInvocation_Descriptor(invocation, descriptor),
  MethodLookup(simplename, descriptor, heaptype, tomethod);

CallGraphEdge(invocation, tomethod) distinct :-
  Reachable(inmethod),
  Instruction_Method(invocation, inmethod),
  VirtualMethodInvocation_Base(invocation, base),
  VarPointsTo(heap, base),
  HeapAllocation_Type(heap, heaptype),
  VirtualMethodInvocation_SimpleName(invocation, simplename),
  VirtualMethodInvocation_Descriptor(invocation, descriptor),
  MethodLookup(simplename, descriptor, heaptype, tomethod);

Reachable(tomethod) distinct :-
  Reachable(inmethod),
  StaticMethodInvocation(invocation, tomethod, inmethod);

CallGraphEdge(invocation, tomethod) distinct :-
   Reachable(inmethod),
   StaticMethodInvocation(invocation, tomethod, inmethod);

Reachable(tomethod) distinct :- 
   Reachable(inmethod),
   Instruction_Method(invocation, inmethod),
   SpecialMethodInvocation_Base(invocation, base),
   VarPointsTo(heap, base),
   MethodInvocation_Method(invocation, tomethod),
   ThisVar(tomethod, this);

CallGraphEdge(invocation, tomethod) distinct :-
   Reachable(inmethod),
   Instruction_Method(invocation, inmethod),
   SpecialMethodInvocation_Base(invocation, base),
   VarPointsTo(heap, base),
   MethodInvocation_Method(invocation, tomethod),
   ThisVar(tomethod, this);

VarPointsTo(heap, this) distinct :-
   Reachable(inmethod),
   Instruction_Method(invocation, inmethod),
   SpecialMethodInvocation_Base(invocation, base),
   VarPointsTo(heap, base),
   MethodInvocation_Method(invocation, tomethod),
   ThisVar(tomethod, this);

/**
 * Implicitly reachable methods are invoked by the JVM on startup.
 */
Reachable(method) distinct :-
    ImplicitReachable(method);

/**
 * Reachable methods. Main method, for sure.
 */
Reachable(method) distinct :-
    MainmethodDeclaration(method);

/**
 * If a class needs to be initialized, then its class initializer is
 * invoked.
 *
 * Note that InitializedClass already deals with superclasses that
 * needs to be initialized as well, so we don't need to invoke class
 * initializers of the superclass here.
 */
Reachable(clinit) distinct :-
   InitializedClass(class),
   ClassInitializer(class, clinit);

To get back to my question, is there a consistent way to understand and resolve "KeyError: 'the_predicate'"? Any recommendations?

Thanks,
Anastasios

[EvgSkv]

Hello @anantoni !

If you are getting a python exception when running Logica then most likely you have found a bug in Logica!

It is assumed for a few annotations (like @limit, @Ground, etc) that first argument is a predicate and it seems that you passed something else.

However I don't see the error in your program. But also definition of e.g. isInterfaceType is missing. So maybe you have more lines in your script?

Anyway I have submitted change to main branch of Logica that shoud be producing a proper error message and pointing where the issue in the program is.

Would you be able to run Logica by cloning the repo?
You could copy your script into the cloned folder and then execute it as python3 logica.py your_script.l run YourPredicate.

Let me know if you have any issues with it and what is the outcome :-)

Thank you for finding the bug!
Evgeny.