damp.ekeko.jdt.soot documentation

Relations between JDT ASTNodes and SOOT whole-program analyses.

ast-reference-model-soot-unit-local

Relation between a JDT reference-valued Expression ?expression,
the Ekeko model ?model in which it resides,
its corresponding SootUnit ?unit and Local ?local. 

Tabled.

Using ?unit and ?local, the Soot program analyses in ?model
can be queried about the results for ?expression.
Source

ast-reference-soot-model

(ast-reference-soot-model ?ast ?model)
Relation between reference-valued JDT Expression instances ?ast
and the Ekeko model ?model in which they reside.
Source

ast-reference-soot-model-method

(ast-reference-soot-model-method ?ast ?model ?sm)
Relation between a reference-valued JDT Expression ?ast,
the Ekeko model ?model in which it resides,
and the SootMethod ?sm in which the corresponding Soot
Unit is to be found.

Note that ?sm can be a class initializer as well as
a constructor.
Source

ast-reference-soot-model-points-to

Relation between a reference-valued JDT ASTNode ?ast, 
the Ekeko model in which it resides,
and the points-to set ?set of object approximations it might evaluate to
at run-time.
Tabled.
Source

ast-references-soot-model-local-must-alias

(ast-references-soot-model-local-must-alias ?ast1 ?ast2 ?model)
Relation of two reference-valued JDT ASTNode instances
?ast1 and ?ast2 in the same method, 
that must alias according to the method's intra-procedural must alias analysis, 
and the model ?model in which they reside.
Source

ast-references-soot-model-local-must-alias-strong

(ast-references-soot-model-local-must-alias-strong ?ast1 ?ast2 ?model)
Relation of two reference-valued JDT ASTNode instances
?ast1 and ?ast2 in the same method, 
that must alias according to the method's 
strong intra-procedural must alias analysis, 
and the model ?model in which they reside.
Source

ast-references-soot-model-may-alias

(ast-references-soot-model-may-alias ?ast1 ?ast2 ?model)
Relation of two reference-valued JDT ASTNode instances ?ast1 and ?ast2
that may alias each other (i.e., have a non-empty intersection of points-to sets)
and the model ?model in which they reside.


Examples:
(ekeko-n* 100
          [?ast1 ?ast2]
          (l/fresh [?model]
                 (ast-references-soot-model-may-alias ?ast1 ?ast2 ?model)))
Source

ast-soot-class

(ast-soot-class ?jdt ?soot)
Relation between the JDT TypeDeclaration ?jdt
and the corresponding SootClass ?soot.
Source

ast-soot-field

(ast-soot-field ?declaration ?field ?soot)
Relation between the JDT FieldDeclaration ?declaration,
 one of its VariableDeclarationFragment instances ?field,
 and the corresponding SootField ?soot.

Note that a field declaration AST node can declare multiple fields.
Source

ast-soot-method

Relation between the JDT MethodDeclaration ?jdt
and the corresponding SootMethod ?soot.
Tabled.
Source

field-signature

(field-signature ?ast ?signature)
Relation between the JDT FieldDeclaration ?ast
and its Soot signature string ?signature.
Source

is-ast-expression-soot-field-access-compatible-local-on-lhs?

(is-ast-expression-soot-field-access-compatible-local-on-lhs? ?fieldBinding ?expressionKeyw ?expression ?valKeyw ?value)
Non-relational. Verifies that JDT Expression ?expression of kind ?expressionKeyw 
that accesses a field with binding ?fieldBinding, can feature on the RHS of
a Soot Unit with SootValue ?value on its LHS of which ?valKeyw represents the kind.
Source

is-ast-expression-soot-field-access-compatible-local-on-rhs?

(is-ast-expression-soot-field-access-compatible-local-on-rhs? ?fieldBinding ?expressionKeyw ?expression ?valKeyw ?value)
Non-relational. Verifies that JDT Expression ?expression of kind ?expressionKeyw 
that accesses a field with binding ?fieldBinding, can feature on the LHS of
a Soot Unit with SootValue ?value on its RHS of which ?valKeyw represents the kind.
Source

is-ast-expression-soot-value-compatible-local-on-lhs?

(is-ast-expression-soot-value-compatible-local-on-lhs? ?keyw ?expression ?valkeyw ?value)
Non-relational. Verifies that JDT Expression ?expression of which ?keyw
represents the kind, can feature on the RHS of a Soot Unit 
with SootValue ?value on its LHS of which ?valKeyw represents the kind.
Source

is-ast-expression-soot-value-compatible-local-on-rhs?

(is-ast-expression-soot-value-compatible-local-on-rhs? ?keyw ?expression ?lvalkeyw ?lvalue)
Non-relational. Verifies that JDT Expression ?expression of kind ?expressionKeyw 
that accesses a field with binding ?fieldBinding, can feature on the LHS of
a Soot Unit with SootValue ?value on its RHS of which ?valKeyw represents the kind.
Source

is-ast-invocation-soot-value-compatible-name-args?

(is-ast-invocation-soot-value-compatible-name-args? ?expression ?value)
Non-relational. Verifies that the names and argument counts of invocation-like
JDT Expression instance ?expression and SootMethodRef ?value are compatible.
Source

is-ast-soot-name-local-compatible?

(is-ast-soot-name-local-compatible? ?name ?local)
Non-relational. Verifies that JDT SimpleName instance ?name
has the same identifier as Soot JimpleLocal ?local.
Source

is-ast-soot-unit-position-compatible?

(is-ast-soot-unit-position-compatible? ?ast ?unit)
Relation of JDT ASTNode instances ?ast and Soot Unit instances ?unit
that are compatible based on their respective line number information.
Source

is-ast-soot-value-type-compatible?

(is-ast-soot-value-type-compatible? ?expression ?value)
Non-relational. Verifies that the declared type of JDT Expression instance ?expression
and the declared type of Soot Value ?value have the same Soot signature string.
Source

is-ast-unit-assign-compatible-local-on-lhs?

(is-ast-unit-assign-compatible-local-on-lhs? ?expression ?unit)
Non-relational. Verifies that ?unit is a Soot assignment Unit
with a JimpleLocal on the LHS and a Soot value compatible with
JDT ASTNode ?expression on its RHS.
Source

is-ast-unit-assign-compatible-local-on-rhs?

(is-ast-unit-assign-compatible-local-on-rhs? ?expression ?unit)
Non-relational. Verifies that ?unit is a Soot assignment Unit
with a JimpleLocal on the RHS and a Soot value compatible with
JDT ASTNode ?expression on its LHS.
Source

is-ast-unit-identity-or-assignment-compatible-local-on-lhs?

(is-ast-unit-identity-or-assignment-compatible-local-on-lhs? ?expression ?unitkeyw ?unit)
Non-relational. Verifies that ?unit is a Soot JIdentityStmt or JAssignStmt
with a JimpleLocal on its LHS that is compatible with the SimpleName or
ThisExpression ?expression.
Source

is-soot-local-named-this?

(is-soot-local-named-this? ?local)
Non-relational. Verifies that Soot JimpleLocal ?local
is named 'this'.
Source

method-declaration-signature

(method-declaration-signature ?ast ?signature)
Relation between the JDT MethodDeclaration ?ast
and its Soot signature string ?signature.
Source

type-declaration-signature

(type-declaration-signature ?ast ?signature)
Relation between the JDT TypeDeclaration ?ast
and its Soot signature string ?signature.
Source