Skip to content

Example Ekeko Queries

Coen De Roover edited this page Dec 18, 2013 · 10 revisions

Some illustrative Ekeko queries. See the Ekeko API documentation for an overview of all relations and functions that are included.

Querying Eclipse JDT Projects

The following queries quantify over the relations between org.eclipse.jdt.core.dom.ASTNode instances and the values of their properties described by org.eclipse.jdt.core.dom.StructuralPropertyDescriptor instances.

Basic AST relations

See [ast/2](http://cderoove.github.io/damp.ekeko/damp.ekeko.jdt.reification.html#var-ast, [has/3](http://cderoove.github.io/damp.ekeko/damp.ekeko.jdt.reification.html#var-has, child/3 and child+/2 of the damp.ekeko.jdt.reification namespace.

All AST nodes of a certain kind:

  ;;all MethodDeclaration instances ?m
  (ekeko* [?m] (ast :MethodDeclaration ?m))

  ;;all CompilationUnit instances ?cu
  (ekeko* [?cu] (ast :CompilationUnit ?cu))
  
  ;;all StringLiteral instances ?cu
  (ekeko* [?cu] (ast :StringLiteral ?cu))

Properties of an AST node:

  ;;Value ?property-value of property named ?property-key of CompilationUnit instances ?cu
  (ekeko* [?cu ?property-key ?property-value] 
    (ast :CompilationUnit ?cu)
    (has ?property-key ?cu ?property-value))

  ;;All method invocations ?inv with an implicit receiver 
  ;;(have null as the value of their expression property) 
  (ekeko* [?inv]
    (ast :MethodInvocation ?inv) 
      (fresh [?exp]
        (has :expression ?inv ?exp)
        (value|null ?exp)))

  ;;All AST nodes and their properties
  (ekeko* [?node ?nodetype ?childtype ?child] 
    (ast ?nodetype ?node) 
    (has ?childtype ?node ?child))

Node-valued properties of an AST node (i.e., its children):

 
  ;;all children of all nodes 
  (ekeko* [?node ?child ?keyword] 
    (child ?keyword ?node ?child)) 
  
  ;;all children residing at an arbitrary depth within any method ?m 
  (ekeko* [?m ?deep-child] 
   (ast :MethodDeclaration ?m) 
   (child+ ?m ?deep-child))

Some basic object-oriented relations:

  ;;methods and their overriders
  (ekeko* [?m ?o] 
    (methoddeclaration-methoddeclaration|overrides ?m ?o))
  
  ;;invocations and the methods they might invoke
  (ekeko* [?i ?m]
    (methodinvocation-methoddeclaration ?i ?m))

  ;;type declarations and the type they declare
  (ekeko* [?typedeclaration ?type]
    (typedeclaration-type ?typedeclaration ?type))
  
  ;;type declarations, the type they declare, occurrences of this type in the program, and how they occur
  (ekeko* [?typeoccurrencekind ?typeoccurrence ?type ?typedeclaration]
           (ast|type-type ?typeoccurrencekind ?typeoccurrence ?type)
           (typedeclaration-type ?typedeclaration ?type))

Callouts to Clojure and Java

See the non-relational equals/2, succeeds/1, and contains/2 of the damp.ekeko.logic namespace.

  ;;all TypeDeclaration instances ?t and the ITypeBinding ?b they resolve to 
  (ekeko* [?t ?b] 
   (ast :TypeDeclaration ?t) 
   (equals ?b (.resolveBinding ?t)))

  ;;all return statements ?s residing at an arbitrary depth within any method ?m
  (ekeko* [?m ?s]
   (ast :MethodDeclaration ?m)
   (child+ ?m ?s)
   (ast :ReturnStatement ?s))

Regular path expressions over JDT control flow graphs

See method-cfg and method-cfg-entry in namespace damp.ekeko.jdt.reification.

Using damp.qwal:

   ;;all methods of which all complete paths through their 
   ;;control flow graph end in a ReturnStatement ?return that 
   ;;is immediately preceded by exactly one other statement ?beforeReturn 
   (ekeko* [?m ?cfg ?entry ?end]
           (method-cfg ?m ?cfg) 
           (method-cfg-entry ?m ?entry)
           (fresh [?beforeReturn ?return]
                  (qwal ?cfg ?entry ?end []
                                  (qcurrent [currentStatement]
                                            (equals currentStatement ?beforeReturn))
                                  q=>
                                  (qcurrent [currentStatement]
                                            (equals currentStatement ?return)
                                            (ast :ReturnStatement ?return)))))

Querying SOOT Program Analyses

The following queries assume a SOOT whole-program analysis has been run on a single JDT project and no other projects are queried by Ekeko.

Basic relations involving Soot Entities

See soot/2, soot-class-method/2, soot-method-units/2 and soot-unit/2 of the damp.ekeko.soot.soot namespace.

    ;;all SootClass instances ?c
    (ekeko* [?c] (soot :class ?c))

    ;;all SootMethod instances ?m declared by SootClass instances ?c
    (ekeko* [?c ?m] (soot-class-method ?c ?m))
    
    ;;chain of SootUnits ?units within SootMethod ?m
    (ekeko* [?m ?units] (soot-method-units ?m ?units)) 

    ;;all SootUnit instances ?unit of kind ?key
    (ekeko* [?unit ?key] (soot-unit ?key ?unit))

Regular path expressions over Soot control flow graphs

See soot-method-cfg/2, soot-method-cfg-entry/3, soot-method-cfg-exit/3 and [soot-unit/2](http://cderoove.github.io/damp.ekeko/damp.ekeko.soot.soot.html#var-soot-unit] of the damp.ekeko.soot.soot namespace.

Using damp.qwal:

   ;;all units on every path through a SOOT control flow graph from an entry point ?entry
   ;;to an exit point ?exit where the exit point uses a value ?defval defined
   ;;by a previous Soot statement ?unit that uses a value ?usedval of type ?keyw
   (ekeko*  [?m ?entry ?exit ?unit ?keyw]
            (fresh [?cfg ?defbox ?exitbox ?usebox ?defval ?usedval]
                   (soot-method-cfg-entry ?m ?cfg ?entry)
                   (soot-method-cfg-exit ?m ?cfg ?exit)
                   (qwal ?cfg ?entry ?exit 
                         []
                         (q=>*)
                         (qcurrent [curr] 
                           (equals curr ?unit) 
                           (soot-unit-defbox ?unit ?defbox) 
                           (soot-valuebox-value ?defbox ?defval) 
                           (soot-unit-usebox ?unit ?usebox)
                           (soot-valuebox-value ?usebox ?usedval) 
                           (soot-value ?keyw ?usedval))
                         (q=>+)
                           (qcurrent [curr]
                             (equals curr ?exit) 
                             (soot-unit-usebox ?exit ?exitbox) 
                             (soot-valuebox-value ?exitbox ?defval)))))

Mapping between SOOT and Eclipse JDT

Note that this mapping is still approximate.

See ast-soot-method/2, soot-method-cfg-entry/3, ast-reference-model-soot-unit-local/5 and ast-references-soot-model-may-alias/3 of the damp.ekeko.jdt.soot namespace.

   ;; all Soot application methods ?sm for which a corresponding JDT method ?m could be found 
   (ekeko* [?m ?sm] (ast-soot-method ?m ?sm))
   
   ;;JDT reference-valued expressions ?ast that could not be mapped to a single Soot ?local-in-?unit pair
   (ekeko*  [?ast ?unit ?local ?unit1 ?local1] 
        (fresh [?model]
          (ast-reference-model-soot-unit-local ?ast ?model ?unit ?local)
          (ast-reference-model-soot-unit-local ?ast ?model ?unit1 ?local1)
          (!= ?local ?local1)))
 
    ;;all JDT AST nodes that are in a may-alias relation according to Soot's interprocedural points-to analysis
    (ekeko-n* 100
          [?ast1 ?ast2]
          (fresh [?model]
                 (ast-references-soot-model-may-alias ?ast1 ?ast2 ?model)))