From 828d1871981e07e41a93a477169862c861a1a695 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 19 Oct 2022 15:03:36 +0200 Subject: [PATCH 1/2] Dataflow: Fix a couple of join-orders. --- .../lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll index 8cd1071d084..2dde1c2819d 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap From a1dba823609d5f0833aed50b76076027500e6317 Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Wed, 19 Oct 2022 15:03:55 +0200 Subject: [PATCH 2/2] Dataflow: Sync. --- .../semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll | 6 ++++++ .../semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll | 6 ++++++ .../semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll | 6 ++++++ .../semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll | 6 ++++++ .../lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll | 6 ++++++ .../lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll | 6 ++++++ .../lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll | 6 ++++++ .../lib/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll | 6 ++++++ .../semmle/code/cpp/dataflow/internal/DataFlowImplLocal.qll | 6 ++++++ .../semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll | 6 ++++++ .../semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll | 6 ++++++ .../semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll | 6 ++++++ .../semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll | 6 ++++++ .../semmle/code/csharp/dataflow/internal/DataFlowImpl.qll | 6 ++++++ .../semmle/code/csharp/dataflow/internal/DataFlowImpl2.qll | 6 ++++++ .../semmle/code/csharp/dataflow/internal/DataFlowImpl3.qll | 6 ++++++ .../semmle/code/csharp/dataflow/internal/DataFlowImpl4.qll | 6 ++++++ .../semmle/code/csharp/dataflow/internal/DataFlowImpl5.qll | 6 ++++++ .../dataflow/internal/DataFlowImplForContentDataFlow.qll | 6 ++++++ .../semmle/code/java/dataflow/internal/DataFlowImpl2.qll | 6 ++++++ .../semmle/code/java/dataflow/internal/DataFlowImpl3.qll | 6 ++++++ .../semmle/code/java/dataflow/internal/DataFlowImpl4.qll | 6 ++++++ .../semmle/code/java/dataflow/internal/DataFlowImpl5.qll | 6 ++++++ .../semmle/code/java/dataflow/internal/DataFlowImpl6.qll | 6 ++++++ .../dataflow/internal/DataFlowImplForOnActivityResult.qll | 6 ++++++ .../dataflow/internal/DataFlowImplForSerializability.qll | 6 ++++++ .../semmle/python/dataflow/new/internal/DataFlowImpl.qll | 6 ++++++ .../semmle/python/dataflow/new/internal/DataFlowImpl2.qll | 6 ++++++ .../semmle/python/dataflow/new/internal/DataFlowImpl3.qll | 6 ++++++ .../semmle/python/dataflow/new/internal/DataFlowImpl4.qll | 6 ++++++ ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll | 6 ++++++ ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl2.qll | 6 ++++++ .../internal/DataFlowImplForHttpClientLibraries.qll | 6 ++++++ .../ruby/dataflow/internal/DataFlowImplForPathname.qll | 6 ++++++ .../codeql/ruby/dataflow/internal/DataFlowImplForRegExp.qll | 6 ++++++ .../ql/lib/codeql/swift/dataflow/internal/DataFlowImpl.qll | 6 ++++++ 36 files changed, 216 insertions(+) diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll b/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll +++ b/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll b/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll +++ b/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll b/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll +++ b/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll b/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll +++ b/cpp/ql/lib/experimental/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl2.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl3.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl4.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplLocal.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplLocal.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplLocal.qll +++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplLocal.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl2.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl3.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll index 8cd1071d084..2dde1c2819d 100644 --- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll +++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl4.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll index 8cd1071d084..2dde1c2819d 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl2.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl2.qll index 8cd1071d084..2dde1c2819d 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl2.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl2.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl3.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl3.qll index 8cd1071d084..2dde1c2819d 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl3.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl3.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl4.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl4.qll index 8cd1071d084..2dde1c2819d 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl4.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl4.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl5.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl5.qll index 8cd1071d084..2dde1c2819d 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl5.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl5.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImplForContentDataFlow.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImplForContentDataFlow.qll index 8cd1071d084..2dde1c2819d 100644 --- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImplForContentDataFlow.qll +++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImplForContentDataFlow.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl2.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl2.qll index 8cd1071d084..2dde1c2819d 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl2.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl2.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl3.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl3.qll index 8cd1071d084..2dde1c2819d 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl3.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl3.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl4.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl4.qll index 8cd1071d084..2dde1c2819d 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl4.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl4.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl5.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl5.qll index 8cd1071d084..2dde1c2819d 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl5.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl5.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl6.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl6.qll index 8cd1071d084..2dde1c2819d 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl6.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl6.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForOnActivityResult.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForOnActivityResult.qll index 8cd1071d084..2dde1c2819d 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForOnActivityResult.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForOnActivityResult.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForSerializability.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForSerializability.qll index 8cd1071d084..2dde1c2819d 100644 --- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForSerializability.qll +++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImplForSerializability.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll index 8cd1071d084..2dde1c2819d 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl2.qll b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl2.qll index 8cd1071d084..2dde1c2819d 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl2.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl2.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl3.qll b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl3.qll index 8cd1071d084..2dde1c2819d 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl3.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl3.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl4.qll b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl4.qll index 8cd1071d084..2dde1c2819d 100644 --- a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl4.qll +++ b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl4.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll index 8cd1071d084..2dde1c2819d 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl2.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl2.qll index 8cd1071d084..2dde1c2819d 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl2.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl2.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForHttpClientLibraries.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForHttpClientLibraries.qll index 8cd1071d084..2dde1c2819d 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForHttpClientLibraries.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForHttpClientLibraries.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForPathname.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForPathname.qll index 8cd1071d084..2dde1c2819d 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForPathname.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForPathname.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForRegExp.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForRegExp.qll index 8cd1071d084..2dde1c2819d 100644 --- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForRegExp.qll +++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImplForRegExp.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap diff --git a/swift/ql/lib/codeql/swift/dataflow/internal/DataFlowImpl.qll b/swift/ql/lib/codeql/swift/dataflow/internal/DataFlowImpl.qll index 8cd1071d084..2dde1c2819d 100644 --- a/swift/ql/lib/codeql/swift/dataflow/internal/DataFlowImpl.qll +++ b/swift/ql/lib/codeql/swift/dataflow/internal/DataFlowImpl.qll @@ -2629,6 +2629,7 @@ private predicate evalUnfold(AccessPathApprox apa, boolean unfold, Configuration /** * Gets the number of `AccessPath`s that correspond to `apa`. */ +pragma[assume_small_delta] private int countAps(AccessPathApprox apa, Configuration config) { evalUnfold(apa, false, config) and result = 1 and @@ -2647,6 +2648,7 @@ private int countAps(AccessPathApprox apa, Configuration config) { * that it is expanded to a precise head-tail representation. */ language[monotonicAggregates] +pragma[assume_small_delta] private int countPotentialAps(AccessPathApprox apa, Configuration config) { apa instanceof AccessPathApproxNil and result = 1 or @@ -2681,6 +2683,7 @@ private newtype TAccessPath = } private newtype TPathNode = + pragma[assume_small_delta] TPathNodeMid( NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap, Configuration config ) { @@ -2778,6 +2781,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { override AccessPathFrontHead getFront() { result = TFrontHead(head) } + pragma[assume_small_delta] override AccessPathApproxCons getApprox() { result = TConsNil(head, tail.(AccessPathNil).getType()) or @@ -2786,6 +2790,7 @@ private class AccessPathCons extends AccessPath, TAccessPathCons { result = TCons1(head, this.length()) } + pragma[assume_small_delta] override int length() { result = 1 + tail.length() } private string toStringImpl(boolean needsSuffix) { @@ -3155,6 +3160,7 @@ private predicate pathNode( * Holds if data may flow from `mid` to `node`. The last step in or out of * a callable is recorded by `cc`. */ +pragma[assume_small_delta] pragma[nomagic] private predicate pathStep( PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, AccessPath ap