Skip to content

Commit

Permalink
Merge pull request #17863 from aschackmull/shared/universal-flow
Browse files Browse the repository at this point in the history
Shared: Add a Universal Flow library and refactor TypeFlow to use it.
  • Loading branch information
aschackmull authored Nov 6, 2024
2 parents f8058e4 + bae6187 commit 4df4a1e
Show file tree
Hide file tree
Showing 5 changed files with 394 additions and 245 deletions.
14 changes: 4 additions & 10 deletions cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/TypeFlow.qll
Original file line number Diff line number Diff line change
Expand Up @@ -159,7 +159,7 @@ private module Input implements TypeFlowInput<Location> {
)
}

predicate joinStep(TypeFlowNode n1, TypeFlowNode n2) {
predicate step(TypeFlowNode n1, TypeFlowNode n2) {
// instruction -> phi
getAnUltimateLocalDefinition(n2.asInstruction()) = n1.asInstruction()
or
Expand All @@ -179,6 +179,8 @@ private module Input implements TypeFlowInput<Location> {
n1.asInstruction() = arg and
n2.asInstruction() = p
)
or
instructionStep(n1.asInstruction(), n2.asInstruction())
}

/**
Expand All @@ -199,10 +201,6 @@ private module Input implements TypeFlowInput<Location> {
i2.(PointerArithmeticInstruction).getLeft() = i1
}

predicate step(TypeFlowNode n1, TypeFlowNode n2) {
instructionStep(n1.asInstruction(), n2.asInstruction())
}

predicate isNullValue(TypeFlowNode n) { n.isNullValue() }

private newtype TType =
Expand Down Expand Up @@ -245,11 +243,7 @@ private module Input implements TypeFlowInput<Location> {

pragma[nomagic]
private predicate upcastCand(TypeFlowNode n, Type t1, Type t2) {
exists(TypeFlowNode next |
step(n, next)
or
joinStep(n, next)
|
exists(TypeFlowNode next | step(n, next) |
n.getType() = t1 and
next.getType() = t2 and
t1 != t2
Expand Down
19 changes: 7 additions & 12 deletions java/ql/lib/semmle/code/java/dataflow/TypeFlow.qll
Original file line number Diff line number Diff line change
Expand Up @@ -84,10 +84,11 @@ private module Input implements TypeFlowInput<Location> {
}

/**
* Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
* necessarily functionally determined by `n2`.
* Holds if data can flow from `n1` to `n2` in one step.
*
* For a given `n2`, this predicate must include all possible `n1` that can flow to `n2`.
*/
predicate joinStep(TypeFlowNode n1, TypeFlowNode n2) {
predicate step(TypeFlowNode n1, TypeFlowNode n2) {
n2.asExpr().(ChooseExpr).getAResultExpr() = n1.asExpr()
or
exists(Field f, Expr e |
Expand All @@ -112,13 +113,7 @@ private module Input implements TypeFlowInput<Location> {
// skip trivial recursion
not arg = n2.asSsa().getAUse()
)
}

/**
* Holds if data can flow from `n1` to `n2` in one step, and `n1` is
* functionally determined by `n2`.
*/
predicate step(TypeFlowNode n1, TypeFlowNode n2) {
or
n2.asExpr() = n1.asField().getAnAccess()
or
n2.asExpr() = n1.asSsa().getAUse()
Expand All @@ -143,7 +138,7 @@ private module Input implements TypeFlowInput<Location> {
exists(LocalVariableDeclExpr decl |
n.asSsa().(BaseSsaUpdate).getDefiningExpr() = decl and
not decl.hasImplicitInit() and
not exists(decl.getInit())
not exists(decl.getInitOrPatternSource())
)
}

Expand All @@ -169,7 +164,7 @@ private module Input implements TypeFlowInput<Location> {
*/
pragma[nomagic]
private predicate upcastCand(TypeFlowNode n, RefType t1, RefType t1e, RefType t2, RefType t2e) {
exists(TypeFlowNode next | step(n, next) or joinStep(n, next) |
exists(TypeFlowNode next | step(n, next) |
n.getType() = t1 and
next.getType() = t2 and
t1.getErasure() = t1e and
Expand Down
11 changes: 3 additions & 8 deletions shared/typeflow/codeql/typeflow/TypeFlow.qll
Original file line number Diff line number Diff line change
Expand Up @@ -28,14 +28,9 @@ signature module TypeFlowInput<LocationSig Location> {
}

/**
* Holds if data can flow from `n1` to `n2` in one step, and `n1` is not
* necessarily functionally determined by `n2`.
*/
predicate joinStep(TypeFlowNode n1, TypeFlowNode n2);

/**
* Holds if data can flow from `n1` to `n2` in one step, and `n1` is
* functionally determined by `n2`.
* Holds if data can flow from `n1` to `n2` in one step.
*
* For a given `n2`, this predicate must include all possible `n1` that can flow to `n2`.
*/
predicate step(TypeFlowNode n1, TypeFlowNode n2);

Expand Down
Loading

0 comments on commit 4df4a1e

Please sign in to comment.