Overview of features required by DOOP basic-only analysis

[rlwww]

The following syntax features have been manually found in the basic-only analysis of DOOP. Also, following files which are added automatically by DOOP: facts/facts.dl, basic/basic.dl, basic-only/analysis.dl, and possible more (depending on flags, see https://bitbucket.org/yanniss/doop/src/master/src/main/groovy/org/clyze/doop/core/SouffleAnalysis.groovy).

It probably does not make sense to mirror the Souffle syntax 1:1, so some things can/must be replaced with some additional preprocessing of the rules.

• [x] Disjunctions in the body (We do not need this.)
• [x] Conjunctions in the head
• [x] Primitive Data types, see https://souffle-lang.github.io/types
  • Strings
  • Numbers
• [x] Constants in rules (in the place of variables)
• [x] Facts
• [x] Stratified negation, see https://souffle-lang.github.io/rules#negation-in-rules

  isStaticMethodInvocation_Insn(?instruction) :-
  _StaticMethodInvocation(?instruction, _, ?signature, _),
  !isOpaqueMethod(?signature).

• [x] #325

  • Equality to constants (this could maybe be replaced by allowing constants in the place of variables)

    isOpaqueMethod(m) :- isMethod(m), m = "<sun.misc.ProxyGenerator: byte[] generateClassFile()>".

  • String ordinal number, see https://souffle-lang.github.io/arguments#intrinsic-functors-and-operations

    TypeToSCCId(type, scc) :-
    PartitionedType(type),
    scc = min ord(x) : TypesInSameSCC(type, x).

  • String concatenation

    Method_Descriptor(?method, ?descriptor) :-
    Method_ReturnType(?method, ?returnType),
    Method_ParamTypes(?method, ?params),
    ?descriptor = cat(?returnType, cat("(", cat(?params, ")"))).

  • Aggregates such as min and count, see https://souffle-lang.github.io/aggregates

    _MethodLookup_ClosestInterface(?simplename, ?descriptor, ?type, ?method) :-
    _MethodLookup_MoreThanOne(?simplename, ?descriptor, ?type),
    ?minLen = min ?len : { _MethodLookup_WithLen(?simplename, ?descriptor, ?type, _, ?len) },
    _MethodLookup_WithLen(?simplename, ?descriptor, ?type, ?method, ?minLen),
    !_MethodLookup_ClassResolution(?simplename, ?descriptor, ?type, _).

  • Arithmetic operations, e.g. -, *, see https://souffle-lang.github.io/arguments

    PossibleNativeCodeTargetMethod(?method, "<<UNKNOWN>>", ?file) :-
    _NativeMethodTypeCandidate(?file, ?function, ?descriptor, _),
    _NativeNameCandidate(?file, ?function, ?name, _),
    _NativeXRef(?descriptor, ?file, _, ?descriptorRefAddr),
    _NativeXRef(?name, ?file, _, ?nameRefAddr),
    Method_SimpleName(?method, ?name),
    Method_JVMDescriptor(?method, ?descriptor),
    (?nameRefAddr - ?descriptorRefAddr) <= 15,
    (?descriptorRefAddr - ?nameRefAddr) <= 15 .

  • Constrains

    • String matching

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

    !match("sun.*", ?class),

    -   Number comparison, e.g. `>`, `<=`, `=`, `!=`
    ```lua
    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.

[monsterkrampe]

Supporting modules requires some more fundamental (theoretical) considerations. We still need to make up our minds, what kind of module system we want to build. This might deviate from Souffle's components quite a bit. In this sense, #324 is still on the roadmap. The feature is not vital for implementing a basic Doop-like program analysis since the same behavior can likely be achieved already by executing multiple Nemo programs consecutively or simply merging them into a single Nemo program.