Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -140,10 +140,8 @@ private module LambdaFlow {
}

pragma[nomagic]
private TReturnPositionSimple viableReturnPosLambda(
DataFlowCall call, DataFlowCallOption lastCall, ReturnKind kind
) {
result = TReturnPositionSimple0(viableCallableLambda(call, lastCall), kind)
private TReturnPositionSimple viableReturnPosLambda(DataFlowCall call, ReturnKind kind) {
result = TReturnPositionSimple0(viableCallableLambda(call, _), kind)
}

private predicate viableReturnPosOutNonLambda(
Expand All @@ -155,11 +153,12 @@ private module LambdaFlow {
)
}

pragma[nomagic]
private predicate viableReturnPosOutLambda(
DataFlowCall call, DataFlowCallOption lastCall, TReturnPositionSimple pos, OutNode out
DataFlowCall call, TReturnPositionSimple pos, OutNode out
) {
exists(ReturnKind kind |
pos = viableReturnPosLambda(call, lastCall, kind) and
pos = viableReturnPosLambda(call, kind) and
out = getAnOutNode(call, kind)
)
}
Expand Down Expand Up @@ -188,6 +187,7 @@ private module LambdaFlow {
else any()
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlow0(
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
Expand Down Expand Up @@ -274,6 +274,7 @@ private module LambdaFlow {
)
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlowOut(
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
Expand All @@ -285,7 +286,7 @@ private module LambdaFlow {
or
// non-linear recursion
revLambdaFlowOutLambdaCall(lambdaCall, kind, out, t, toJump, call, lastCall) and
viableReturnPosOutLambda(call, _, pos, out)
viableReturnPosOutLambda(call, pos, out)
)
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -140,10 +140,8 @@ private module LambdaFlow {
}

pragma[nomagic]
private TReturnPositionSimple viableReturnPosLambda(
DataFlowCall call, DataFlowCallOption lastCall, ReturnKind kind
) {
result = TReturnPositionSimple0(viableCallableLambda(call, lastCall), kind)
private TReturnPositionSimple viableReturnPosLambda(DataFlowCall call, ReturnKind kind) {
result = TReturnPositionSimple0(viableCallableLambda(call, _), kind)
}

private predicate viableReturnPosOutNonLambda(
Expand All @@ -155,11 +153,12 @@ private module LambdaFlow {
)
}

pragma[nomagic]
private predicate viableReturnPosOutLambda(
DataFlowCall call, DataFlowCallOption lastCall, TReturnPositionSimple pos, OutNode out
DataFlowCall call, TReturnPositionSimple pos, OutNode out
) {
exists(ReturnKind kind |
pos = viableReturnPosLambda(call, lastCall, kind) and
pos = viableReturnPosLambda(call, kind) and
out = getAnOutNode(call, kind)
)
}
Expand Down Expand Up @@ -188,6 +187,7 @@ private module LambdaFlow {
else any()
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlow0(
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
Expand Down Expand Up @@ -274,6 +274,7 @@ private module LambdaFlow {
)
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlowOut(
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
Expand All @@ -285,7 +286,7 @@ private module LambdaFlow {
or
// non-linear recursion
revLambdaFlowOutLambdaCall(lambdaCall, kind, out, t, toJump, call, lastCall) and
viableReturnPosOutLambda(call, _, pos, out)
viableReturnPosOutLambda(call, pos, out)
)
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -140,10 +140,8 @@ private module LambdaFlow {
}

pragma[nomagic]
private TReturnPositionSimple viableReturnPosLambda(
DataFlowCall call, DataFlowCallOption lastCall, ReturnKind kind
) {
result = TReturnPositionSimple0(viableCallableLambda(call, lastCall), kind)
private TReturnPositionSimple viableReturnPosLambda(DataFlowCall call, ReturnKind kind) {
result = TReturnPositionSimple0(viableCallableLambda(call, _), kind)
}

private predicate viableReturnPosOutNonLambda(
Expand All @@ -155,11 +153,12 @@ private module LambdaFlow {
)
}

pragma[nomagic]
private predicate viableReturnPosOutLambda(
DataFlowCall call, DataFlowCallOption lastCall, TReturnPositionSimple pos, OutNode out
DataFlowCall call, TReturnPositionSimple pos, OutNode out
) {
exists(ReturnKind kind |
pos = viableReturnPosLambda(call, lastCall, kind) and
pos = viableReturnPosLambda(call, kind) and
out = getAnOutNode(call, kind)
)
}
Expand Down Expand Up @@ -188,6 +187,7 @@ private module LambdaFlow {
else any()
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlow0(
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
Expand Down Expand Up @@ -274,6 +274,7 @@ private module LambdaFlow {
)
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlowOut(
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
Expand All @@ -285,7 +286,7 @@ private module LambdaFlow {
or
// non-linear recursion
revLambdaFlowOutLambdaCall(lambdaCall, kind, out, t, toJump, call, lastCall) and
viableReturnPosOutLambda(call, _, pos, out)
viableReturnPosOutLambda(call, pos, out)
)
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,7 @@ module Public {
}

/** Gets the stack obtained by dropping the first `i` elements, if any. */
pragma[assume_small_delta]
SummaryComponentStack drop(int i) {
i = 0 and result = this
or
Expand Down
15 changes: 8 additions & 7 deletions go/ql/lib/semmle/go/dataflow/internal/DataFlowImplCommon.qll
Original file line number Diff line number Diff line change
Expand Up @@ -140,10 +140,8 @@ private module LambdaFlow {
}

pragma[nomagic]
private TReturnPositionSimple viableReturnPosLambda(
DataFlowCall call, DataFlowCallOption lastCall, ReturnKind kind
) {
result = TReturnPositionSimple0(viableCallableLambda(call, lastCall), kind)
private TReturnPositionSimple viableReturnPosLambda(DataFlowCall call, ReturnKind kind) {
result = TReturnPositionSimple0(viableCallableLambda(call, _), kind)
}

private predicate viableReturnPosOutNonLambda(
Expand All @@ -155,11 +153,12 @@ private module LambdaFlow {
)
}

pragma[nomagic]
private predicate viableReturnPosOutLambda(
DataFlowCall call, DataFlowCallOption lastCall, TReturnPositionSimple pos, OutNode out
DataFlowCall call, TReturnPositionSimple pos, OutNode out
) {
exists(ReturnKind kind |
pos = viableReturnPosLambda(call, lastCall, kind) and
pos = viableReturnPosLambda(call, kind) and
out = getAnOutNode(call, kind)
)
}
Expand Down Expand Up @@ -188,6 +187,7 @@ private module LambdaFlow {
else any()
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlow0(
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
Expand Down Expand Up @@ -274,6 +274,7 @@ private module LambdaFlow {
)
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlowOut(
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
Expand All @@ -285,7 +286,7 @@ private module LambdaFlow {
or
// non-linear recursion
revLambdaFlowOutLambdaCall(lambdaCall, kind, out, t, toJump, call, lastCall) and
viableReturnPosOutLambda(call, _, pos, out)
viableReturnPosOutLambda(call, pos, out)
)
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,7 @@ module Public {
}

/** Gets the stack obtained by dropping the first `i` elements, if any. */
pragma[assume_small_delta]
SummaryComponentStack drop(int i) {
i = 0 and result = this
or
Expand Down
2 changes: 2 additions & 0 deletions java/ql/lib/semmle/code/java/ControlFlowGraph.qll
Original file line number Diff line number Diff line change
Expand Up @@ -365,6 +365,7 @@ private module ControlFlowGraphImpl {
/**
* Gets a non-overridable method that always throws an exception or calls `exit`.
*/
pragma[assume_small_delta]
private Method nonReturningMethod() {
result instanceof MethodExit
or
Expand All @@ -381,6 +382,7 @@ private module ControlFlowGraphImpl {
/**
* Gets a virtual method that always throws an exception or calls `exit`.
*/
pragma[assume_small_delta]
private EffectivelyNonVirtualMethod likelyNonReturningMethod() {
result.getReturnType() instanceof VoidType and
not exists(ReturnStmt ret | ret.getEnclosingCallable() = result) and
Expand Down
2 changes: 2 additions & 0 deletions java/ql/lib/semmle/code/java/dataflow/SSA.qll
Original file line number Diff line number Diff line change
Expand Up @@ -451,6 +451,7 @@ private module SsaImpl {
* Holds if `f` is live in `b` at index `i`. The rank of `i` is `rankix` as
* defined by `callDefUseRank`.
*/
pragma[assume_small_delta]
private predicate liveAtRank(TrackedField f, BasicBlock b, int rankix, int i) {
callDefUseRank(f, b, rankix, i) and
(
Expand Down Expand Up @@ -564,6 +565,7 @@ private module SsaImpl {
}

/** Holds if a phi node for `v` is needed at the beginning of basic block `b`. */
pragma[assume_small_delta]
cached
predicate phiNode(TrackedVar v, BasicBlock b) {
liveAtEntry(v, b) and
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -151,6 +151,7 @@ private module SsaImpl {
}

/** Holds if a phi node for `v` is needed at the beginning of basic block `b`. */
pragma[assume_small_delta]
cached
predicate phiNode(BaseSsaSourceVariable v, BasicBlock b) {
liveAtEntry(v, b) and
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -140,10 +140,8 @@ private module LambdaFlow {
}

pragma[nomagic]
private TReturnPositionSimple viableReturnPosLambda(
DataFlowCall call, DataFlowCallOption lastCall, ReturnKind kind
) {
result = TReturnPositionSimple0(viableCallableLambda(call, lastCall), kind)
private TReturnPositionSimple viableReturnPosLambda(DataFlowCall call, ReturnKind kind) {
result = TReturnPositionSimple0(viableCallableLambda(call, _), kind)
}

private predicate viableReturnPosOutNonLambda(
Expand All @@ -155,11 +153,12 @@ private module LambdaFlow {
)
}

pragma[nomagic]
private predicate viableReturnPosOutLambda(
DataFlowCall call, DataFlowCallOption lastCall, TReturnPositionSimple pos, OutNode out
DataFlowCall call, TReturnPositionSimple pos, OutNode out
) {
exists(ReturnKind kind |
pos = viableReturnPosLambda(call, lastCall, kind) and
pos = viableReturnPosLambda(call, kind) and
out = getAnOutNode(call, kind)
)
}
Expand Down Expand Up @@ -188,6 +187,7 @@ private module LambdaFlow {
else any()
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlow0(
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
Expand Down Expand Up @@ -274,6 +274,7 @@ private module LambdaFlow {
)
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlowOut(
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
Expand All @@ -285,7 +286,7 @@ private module LambdaFlow {
or
// non-linear recursion
revLambdaFlowOutLambdaCall(lambdaCall, kind, out, t, toJump, call, lastCall) and
viableReturnPosOutLambda(call, _, pos, out)
viableReturnPosOutLambda(call, pos, out)
)
}

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,7 @@ module Public {
}

/** Gets the stack obtained by dropping the first `i` elements, if any. */
pragma[assume_small_delta]
SummaryComponentStack drop(int i) {
i = 0 and result = this
or
Expand Down
2 changes: 2 additions & 0 deletions java/ql/lib/semmle/code/java/frameworks/JaxWS.qll
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ private predicate hasPathAnnotation(Annotatable annotatable) {
* A method which is annotated with one or more JaxRS resource type annotations e.g. `@GET`, `@POST` etc.
*/
class JaxRsResourceMethod extends Method {
pragma[assume_small_delta]
JaxRsResourceMethod() {
exists(AnnotationType a |
a = this.getAnAnnotation().getType() and
Expand Down Expand Up @@ -91,6 +92,7 @@ class JaxRsResourceMethod extends Method {
* This class contains resource methods, which are executed in response to requests.
*/
class JaxRsResourceClass extends Class {
pragma[assume_small_delta]
JaxRsResourceClass() {
// A root resource class has a @Path annotation on the class.
hasPathAnnotation(this)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -140,10 +140,8 @@ private module LambdaFlow {
}

pragma[nomagic]
private TReturnPositionSimple viableReturnPosLambda(
DataFlowCall call, DataFlowCallOption lastCall, ReturnKind kind
) {
result = TReturnPositionSimple0(viableCallableLambda(call, lastCall), kind)
private TReturnPositionSimple viableReturnPosLambda(DataFlowCall call, ReturnKind kind) {
result = TReturnPositionSimple0(viableCallableLambda(call, _), kind)
}

private predicate viableReturnPosOutNonLambda(
Expand All @@ -155,11 +153,12 @@ private module LambdaFlow {
)
}

pragma[nomagic]
private predicate viableReturnPosOutLambda(
DataFlowCall call, DataFlowCallOption lastCall, TReturnPositionSimple pos, OutNode out
DataFlowCall call, TReturnPositionSimple pos, OutNode out
) {
exists(ReturnKind kind |
pos = viableReturnPosLambda(call, lastCall, kind) and
pos = viableReturnPosLambda(call, kind) and
out = getAnOutNode(call, kind)
)
}
Expand Down Expand Up @@ -188,6 +187,7 @@ private module LambdaFlow {
else any()
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlow0(
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
Expand Down Expand Up @@ -274,6 +274,7 @@ private module LambdaFlow {
)
}

pragma[assume_small_delta]
pragma[nomagic]
predicate revLambdaFlowOut(
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,
Expand All @@ -285,7 +286,7 @@ private module LambdaFlow {
or
// non-linear recursion
revLambdaFlowOutLambdaCall(lambdaCall, kind, out, t, toJump, call, lastCall) and
viableReturnPosOutLambda(call, _, pos, out)
viableReturnPosOutLambda(call, pos, out)
)
}

Expand Down
Loading