Skip to content

Commit 6912f7e

Browse files
cklincklin
authored
Merge pull request github#13638 from cklin/remove-pragma-assume-small-delta
Remove pragma[assume_small_delta]
2 parents d90ddf1 + ce464a7 commit 6912f7e

File tree

53 files changed

+78
-255
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

53 files changed

+78
-255
lines changed

‎cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -460,7 +460,6 @@ module Impl<FullStateConfigSig Config> {
460460
* The Boolean `cc` records whether the node is reached through an
461461
* argument in a call.
462462
*/
463-
pragma[assume_small_delta]
464463
private predicate fwdFlow(NodeEx node, Cc cc) {
465464
sourceNode(node, _) and
466465
if hasSourceCallCtx() then cc = true else cc = false
@@ -570,7 +569,6 @@ module Impl<FullStateConfigSig Config> {
570569
/**
571570
* Holds if `c` is the target of a store in the flow covered by `fwdFlow`.
572571
*/
573-
pragma[assume_small_delta]
574572
pragma[nomagic]
575573
private predicate fwdFlowConsCand(Content c) {
576574
exists(NodeEx mid, NodeEx node |
@@ -1216,7 +1214,6 @@ module Impl<FullStateConfigSig Config> {
12161214
fwdFlow1(_, _, _, _, _, _, t0, t, ap, _) and t0 != t
12171215
}
12181216

1219-
pragma[assume_small_delta]
12201217
pragma[nomagic]
12211218
private predicate fwdFlow0(
12221219
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
@@ -2777,7 +2774,6 @@ module Impl<FullStateConfigSig Config> {
27772774
/**
27782775
* Gets the number of `AccessPath`s that correspond to `apa`.
27792776
*/
2780-
pragma[assume_small_delta]
27812777
private int countAps(AccessPathApprox apa) {
27822778
evalUnfold(apa, false) and
27832779
result = 1 and
@@ -2796,7 +2792,6 @@ module Impl<FullStateConfigSig Config> {
27962792
* that it is expanded to a precise head-tail representation.
27972793
*/
27982794
language[monotonicAggregates]
2799-
pragma[assume_small_delta]
28002795
private int countPotentialAps(AccessPathApprox apa) {
28012796
apa instanceof AccessPathApproxNil and result = 1
28022797
or
@@ -2833,7 +2828,6 @@ module Impl<FullStateConfigSig Config> {
28332828
}
28342829

28352830
private newtype TPathNode =
2836-
pragma[assume_small_delta]
28372831
TPathNodeMid(
28382832
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, DataFlowType t, AccessPath ap
28392833
) {
@@ -2918,7 +2912,6 @@ module Impl<FullStateConfigSig Config> {
29182912

29192913
override AccessPathFrontHead getFront() { result = TFrontHead(head_) }
29202914

2921-
pragma[assume_small_delta]
29222915
override AccessPathApproxCons getApprox() {
29232916
result = TConsNil(head_, t) and tail_ = TAccessPathNil()
29242917
or
@@ -2927,7 +2920,6 @@ module Impl<FullStateConfigSig Config> {
29272920
result = TCons1(head_, this.length())
29282921
}
29292922

2930-
pragma[assume_small_delta]
29312923
override int length() { result = 1 + tail_.length() }
29322924

29332925
private string toStringImpl(boolean needsSuffix) {
@@ -3379,7 +3371,6 @@ module Impl<FullStateConfigSig Config> {
33793371
* Holds if data may flow from `mid` to `node`. The last step in or out of
33803372
* a callable is recorded by `cc`.
33813373
*/
3382-
pragma[assume_small_delta]
33833374
pragma[nomagic]
33843375
private predicate pathStep0(
33853376
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, DataFlowType t,
@@ -3592,7 +3583,6 @@ module Impl<FullStateConfigSig Config> {
35923583
)
35933584
}
35943585

3595-
pragma[assume_small_delta]
35963586
pragma[nomagic]
35973587
private predicate pathThroughCallable0(
35983588
DataFlowCall call, PathNodeMid mid, ReturnKindExt kind, FlowState state, CallContext cc,

‎cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImplCommon.qll

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -187,7 +187,6 @@ private module LambdaFlow {
187187
else any()
188188
}
189189

190-
pragma[assume_small_delta]
191190
pragma[nomagic]
192191
predicate revLambdaFlow0(
193192
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
@@ -274,7 +273,6 @@ private module LambdaFlow {
274273
)
275274
}
276275

277-
pragma[assume_small_delta]
278276
pragma[nomagic]
279277
predicate revLambdaFlowOut(
280278
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,

‎cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll

Lines changed: 0 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -460,7 +460,6 @@ module Impl<FullStateConfigSig Config> {
460460
* The Boolean `cc` records whether the node is reached through an
461461
* argument in a call.
462462
*/
463-
pragma[assume_small_delta]
464463
private predicate fwdFlow(NodeEx node, Cc cc) {
465464
sourceNode(node, _) and
466465
if hasSourceCallCtx() then cc = true else cc = false
@@ -570,7 +569,6 @@ module Impl<FullStateConfigSig Config> {
570569
/**
571570
* Holds if `c` is the target of a store in the flow covered by `fwdFlow`.
572571
*/
573-
pragma[assume_small_delta]
574572
pragma[nomagic]
575573
private predicate fwdFlowConsCand(Content c) {
576574
exists(NodeEx mid, NodeEx node |
@@ -1216,7 +1214,6 @@ module Impl<FullStateConfigSig Config> {
12161214
fwdFlow1(_, _, _, _, _, _, t0, t, ap, _) and t0 != t
12171215
}
12181216

1219-
pragma[assume_small_delta]
12201217
pragma[nomagic]
12211218
private predicate fwdFlow0(
12221219
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, TypOption argT,
@@ -2777,7 +2774,6 @@ module Impl<FullStateConfigSig Config> {
27772774
/**
27782775
* Gets the number of `AccessPath`s that correspond to `apa`.
27792776
*/
2780-
pragma[assume_small_delta]
27812777
private int countAps(AccessPathApprox apa) {
27822778
evalUnfold(apa, false) and
27832779
result = 1 and
@@ -2796,7 +2792,6 @@ module Impl<FullStateConfigSig Config> {
27962792
* that it is expanded to a precise head-tail representation.
27972793
*/
27982794
language[monotonicAggregates]
2799-
pragma[assume_small_delta]
28002795
private int countPotentialAps(AccessPathApprox apa) {
28012796
apa instanceof AccessPathApproxNil and result = 1
28022797
or
@@ -2833,7 +2828,6 @@ module Impl<FullStateConfigSig Config> {
28332828
}
28342829

28352830
private newtype TPathNode =
2836-
pragma[assume_small_delta]
28372831
TPathNodeMid(
28382832
NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, DataFlowType t, AccessPath ap
28392833
) {
@@ -2918,7 +2912,6 @@ module Impl<FullStateConfigSig Config> {
29182912

29192913
override AccessPathFrontHead getFront() { result = TFrontHead(head_) }
29202914

2921-
pragma[assume_small_delta]
29222915
override AccessPathApproxCons getApprox() {
29232916
result = TConsNil(head_, t) and tail_ = TAccessPathNil()
29242917
or
@@ -2927,7 +2920,6 @@ module Impl<FullStateConfigSig Config> {
29272920
result = TCons1(head_, this.length())
29282921
}
29292922

2930-
pragma[assume_small_delta]
29312923
override int length() { result = 1 + tail_.length() }
29322924

29332925
private string toStringImpl(boolean needsSuffix) {
@@ -3379,7 +3371,6 @@ module Impl<FullStateConfigSig Config> {
33793371
* Holds if data may flow from `mid` to `node`. The last step in or out of
33803372
* a callable is recorded by `cc`.
33813373
*/
3382-
pragma[assume_small_delta]
33833374
pragma[nomagic]
33843375
private predicate pathStep0(
33853376
PathNodeMid mid, NodeEx node, FlowState state, CallContext cc, SummaryCtx sc, DataFlowType t,
@@ -3592,7 +3583,6 @@ module Impl<FullStateConfigSig Config> {
35923583
)
35933584
}
35943585

3595-
pragma[assume_small_delta]
35963586
pragma[nomagic]
35973587
private predicate pathThroughCallable0(
35983588
DataFlowCall call, PathNodeMid mid, ReturnKindExt kind, FlowState state, CallContext cc,

‎cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImplCommon.qll

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -187,7 +187,6 @@ private module LambdaFlow {
187187
else any()
188188
}
189189

190-
pragma[assume_small_delta]
191190
pragma[nomagic]
192191
predicate revLambdaFlow0(
193192
DataFlowCall lambdaCall, LambdaCallKind kind, Node node, DataFlowType t, boolean toReturn,
@@ -274,7 +273,6 @@ private module LambdaFlow {
274273
)
275274
}
276275

277-
pragma[assume_small_delta]
278276
pragma[nomagic]
279277
predicate revLambdaFlowOut(
280278
DataFlowCall lambdaCall, LambdaCallKind kind, TReturnPositionSimple pos, DataFlowType t,

‎cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/ProductFlow.qll

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -359,7 +359,6 @@ module ProductFlow {
359359
Config::isSinkPair(node1.getNode(), node1.getState(), node2.getNode(), node2.getState())
360360
}
361361

362-
pragma[assume_small_delta]
363362
pragma[nomagic]
364363
private predicate fwdReachableInterprocEntry(Flow1::PathNode node1, Flow2::PathNode node2) {
365364
isSourcePair(node1, node2)
@@ -396,7 +395,6 @@ module ProductFlow {
396395
fwdIsSuccessorExit(pragma[only_bind_into](mid1), pragma[only_bind_into](mid2), succ1, succ2)
397396
}
398397

399-
pragma[assume_small_delta]
400398
private predicate fwdIsSuccessor(
401399
Flow1::PathNode pred1, Flow2::PathNode pred2, Flow1::PathNode succ1, Flow2::PathNode succ2
402400
) {
@@ -406,7 +404,6 @@ module ProductFlow {
406404
)
407405
}
408406

409-
pragma[assume_small_delta]
410407
pragma[nomagic]
411408
private predicate revReachableInterprocEntry(Flow1::PathNode node1, Flow2::PathNode node2) {
412409
fwdReachableInterprocEntry(node1, node2) and

‎cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaInternalsCommon.qll

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -588,7 +588,6 @@ private module Cached {
588588
)
589589
}
590590

591-
pragma[assume_small_delta]
592591
private predicate convertsIntoArgumentRev(Instruction instr) {
593592
convertsIntoArgumentFwd(instr) and
594593
(

‎cpp/ql/lib/semmle/code/cpp/ir/implementation/aliased_ssa/gvn/internal/ValueNumberingInternal.qll

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,6 @@ private predicate binaryValueNumber0(
176176
)
177177
}
178178

179-
pragma[assume_small_delta]
180179
private predicate binaryValueNumber(
181180
BinaryInstruction instr, IRFunction irFunc, Opcode opcode, TValueNumber leftOperand,
182181
TValueNumber rightOperand
@@ -202,7 +201,6 @@ private predicate pointerArithmeticValueNumber0(
202201
)
203202
}
204203

205-
pragma[assume_small_delta]
206204
private predicate pointerArithmeticValueNumber(
207205
PointerArithmeticInstruction instr, IRFunction irFunc, Opcode opcode, int elementSize,
208206
TValueNumber leftOperand, TValueNumber rightOperand
@@ -249,7 +247,6 @@ private predicate loadTotalOverlapValueNumber0(
249247
)
250248
}
251249

252-
pragma[assume_small_delta]
253250
private predicate loadTotalOverlapValueNumber(
254251
LoadTotalOverlapInstruction instr, IRFunction irFunc, IRType type, TValueNumber memOperand,
255252
TValueNumber operand

‎cpp/ql/lib/semmle/code/cpp/ir/implementation/raw/gvn/internal/ValueNumberingInternal.qll

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,6 @@ private predicate binaryValueNumber0(
176176
)
177177
}
178178

179-
pragma[assume_small_delta]
180179
private predicate binaryValueNumber(
181180
BinaryInstruction instr, IRFunction irFunc, Opcode opcode, TValueNumber leftOperand,
182181
TValueNumber rightOperand
@@ -202,7 +201,6 @@ private predicate pointerArithmeticValueNumber0(
202201
)
203202
}
204203

205-
pragma[assume_small_delta]
206204
private predicate pointerArithmeticValueNumber(
207205
PointerArithmeticInstruction instr, IRFunction irFunc, Opcode opcode, int elementSize,
208206
TValueNumber leftOperand, TValueNumber rightOperand
@@ -249,7 +247,6 @@ private predicate loadTotalOverlapValueNumber0(
249247
)
250248
}
251249

252-
pragma[assume_small_delta]
253250
private predicate loadTotalOverlapValueNumber(
254251
LoadTotalOverlapInstruction instr, IRFunction irFunc, IRType type, TValueNumber memOperand,
255252
TValueNumber operand

‎cpp/ql/lib/semmle/code/cpp/ir/implementation/unaliased_ssa/gvn/internal/ValueNumberingInternal.qll

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,6 @@ private predicate binaryValueNumber0(
176176
)
177177
}
178178

179-
pragma[assume_small_delta]
180179
private predicate binaryValueNumber(
181180
BinaryInstruction instr, IRFunction irFunc, Opcode opcode, TValueNumber leftOperand,
182181
TValueNumber rightOperand
@@ -202,7 +201,6 @@ private predicate pointerArithmeticValueNumber0(
202201
)
203202
}
204203

205-
pragma[assume_small_delta]
206204
private predicate pointerArithmeticValueNumber(
207205
PointerArithmeticInstruction instr, IRFunction irFunc, Opcode opcode, int elementSize,
208206
TValueNumber leftOperand, TValueNumber rightOperand
@@ -249,7 +247,6 @@ private predicate loadTotalOverlapValueNumber0(
249247
)
250248
}
251249

252-
pragma[assume_small_delta]
253250
private predicate loadTotalOverlapValueNumber(
254251
LoadTotalOverlapInstruction instr, IRFunction irFunc, IRType type, TValueNumber memOperand,
255252
TValueNumber operand

‎cpp/ql/lib/semmle/code/cpp/rangeanalysis/new/internal/semantic/analysis/RangeAnalysisStage.qll

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -877,7 +877,6 @@ module RangeStage<
877877
)
878878
}
879879

880-
pragma[assume_small_delta]
881880
pragma[nomagic]
882881
private predicate boundedPhiRankStep(
883882
SemSsaPhiNode phi, SemBound b, D::Delta delta, boolean upper, boolean fromBackEdge,

0 commit comments

Comments
 (0)