Skip to content

Commit aada8d3

Browse files
smowtonsmowton
authored
Merge pull request #8405 from smowton/smowton/fix/range-analysis-use-ranked-phi-nodes
C#/Java: Range analysis: use ranked phi nodes
2 parents 4c2081b + 579b57c commit aada8d3

File tree

9 files changed

+105
-69
lines changed

9 files changed

+105
-69
lines changed

‎csharp/ql/lib/semmle/code/csharp/dataflow/ModulusAnalysis.qll‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -111,13 +111,6 @@ private predicate evenlyDivisibleExpr(Expr e, int factor) {
111111
)
112112
}
113113

114-
/**
115-
* Holds if `rix` is the number of input edges to `phi`.
116-
*/
117-
private predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
118-
rix = max(int r | rankedPhiInput(phi, _, _, r))
119-
}
120-
121114
/**
122115
* Gets the remainder of `val` modulo `mod`.
123116
*

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll‎

Lines changed: 0 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -43,37 +43,4 @@ module Private {
4343
predicate ssaUpdateStep = RU::ssaUpdateStep/3;
4444

4545
Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode() }
46-
47-
private class PhiInputEdgeBlock extends BasicBlock {
48-
PhiInputEdgeBlock() { this = any(SsaReadPositionPhiInputEdge edge).getOrigBlock() }
49-
}
50-
51-
int getId(PhiInputEdgeBlock bb) {
52-
exists(CfgImpl::ControlFlowTree::Range_ t | CfgImpl::ControlFlowTree::idOf(t, result) |
53-
t = bb.getFirstNode().getElement()
54-
or
55-
t = bb.(CS::ControlFlow::BasicBlocks::EntryBlock).getCallable()
56-
)
57-
}
58-
59-
private string getSplitString(PhiInputEdgeBlock bb) {
60-
result = bb.getFirstNode().(CS::ControlFlow::Nodes::ElementNode).getSplitsString()
61-
or
62-
not exists(bb.getFirstNode().(CS::ControlFlow::Nodes::ElementNode).getSplitsString()) and
63-
result = ""
64-
}
65-
66-
/**
67-
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
68-
* in an arbitrary 1-based numbering of the input edges to `phi`.
69-
*/
70-
predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
71-
edge.phiInput(phi, inp) and
72-
edge =
73-
rank[r](SsaReadPositionPhiInputEdge e |
74-
e.phiInput(phi, _)
75-
|
76-
e order by getId(e.getOrigBlock()), getSplitString(e.getOrigBlock())
77-
)
78-
}
7946
}

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
*/
44

55
private import SsaReadPositionSpecific
6+
import SsaReadPositionSpecific::Public
67

78
private newtype TSsaReadPosition =
89
TSsaReadPositionBlock(BasicBlock bb) { bb = getAReadBasicBlock(_) } or
@@ -55,3 +56,10 @@ class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiIn
5556

5657
override string toString() { result = "edge" }
5758
}
59+
60+
/**
61+
* Holds if `rix` is the number of input edges to `phi`.
62+
*/
63+
predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
64+
rix = max(int r | rankedPhiInput(phi, _, _, r))
65+
}

‎csharp/ql/lib/semmle/code/csharp/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@
33
*/
44

55
private import csharp
6+
private import SsaReadPositionCommon
7+
private import semmle.code.csharp.controlflow.internal.ControlFlowGraphImpl as CfgImpl
68

79
class SsaVariable = Ssa::Definition;
810

@@ -14,3 +16,41 @@ class BasicBlock = ControlFlow::BasicBlock;
1416
BasicBlock getAReadBasicBlock(SsaVariable v) {
1517
result = v.getARead().getAControlFlowNode().getBasicBlock()
1618
}
19+
20+
private class PhiInputEdgeBlock extends BasicBlock {
21+
PhiInputEdgeBlock() { this = any(SsaReadPositionPhiInputEdge edge).getOrigBlock() }
22+
}
23+
24+
private int getId(PhiInputEdgeBlock bb) {
25+
exists(CfgImpl::ControlFlowTree::Range_ t | CfgImpl::ControlFlowTree::idOf(t, result) |
26+
t = bb.getFirstNode().getElement()
27+
or
28+
t = bb.(ControlFlow::BasicBlocks::EntryBlock).getCallable()
29+
)
30+
}
31+
32+
private string getSplitString(PhiInputEdgeBlock bb) {
33+
result = bb.getFirstNode().(ControlFlow::Nodes::ElementNode).getSplitsString()
34+
or
35+
not exists(bb.getFirstNode().(ControlFlow::Nodes::ElementNode).getSplitsString()) and
36+
result = ""
37+
}
38+
39+
/**
40+
* Declarations to be exposed to users of SsaReadPositionCommon.
41+
*/
42+
module Public {
43+
/**
44+
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
45+
* in an arbitrary 1-based numbering of the input edges to `phi`.
46+
*/
47+
predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
48+
edge.phiInput(phi, inp) and
49+
edge =
50+
rank[r](SsaReadPositionPhiInputEdge e |
51+
e.phiInput(phi, _)
52+
|
53+
e order by getId(e.getOrigBlock()), getSplitString(e.getOrigBlock())
54+
)
55+
}
56+
}

‎java/ql/lib/semmle/code/java/dataflow/ModulusAnalysis.qll‎

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -111,13 +111,6 @@ private predicate evenlyDivisibleExpr(Expr e, int factor) {
111111
)
112112
}
113113

114-
/**
115-
* Holds if `rix` is the number of input edges to `phi`.
116-
*/
117-
private predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
118-
rix = max(int r | rankedPhiInput(phi, _, _, r))
119-
}
120-
121114
/**
122115
* Gets the remainder of `val` modulo `mod`.
123116
*

‎java/ql/lib/semmle/code/java/dataflow/RangeAnalysis.qll‎

Lines changed: 23 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -725,6 +725,26 @@ private predicate boundedPhiCandValidForEdge(
725725
)
726726
}
727727

728+
/**
729+
* Holds if `b + delta` is a valid bound for `phi`'s `rix`th input edge.
730+
* - `upper = true` : `phi <= b + delta`
731+
* - `upper = false` : `phi >= b + delta`
732+
*/
733+
private predicate boundedPhiStep(
734+
SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
735+
Reason reason, int rix
736+
) {
737+
exists(SsaVariable inp, SsaReadPositionPhiInputEdge edge |
738+
rankedPhiInput(phi, inp, edge, rix) and
739+
boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge) and
740+
(
741+
rix = 1
742+
or
743+
boundedPhiStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, rix - 1)
744+
)
745+
)
746+
}
747+
728748
/**
729749
* Holds if `b + delta` is a valid bound for `phi`.
730750
* - `upper = true` : `phi <= b + delta`
@@ -734,8 +754,9 @@ private predicate boundedPhi(
734754
SsaPhiNode phi, Bound b, int delta, boolean upper, boolean fromBackEdge, int origdelta,
735755
Reason reason
736756
) {
737-
forex(SsaVariable inp, SsaReadPositionPhiInputEdge edge | edge.phiInput(phi, inp) |
738-
boundedPhiCandValidForEdge(phi, b, delta, upper, fromBackEdge, origdelta, reason, inp, edge)
757+
exists(int r |
758+
boundedPhiStep(phi, b, delta, upper, fromBackEdge, origdelta, reason, r) and
759+
maxPhiInputRank(phi, r)
739760
)
740761
}
741762

‎java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/ModulusAnalysisSpecific.qll‎

Lines changed: 0 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -111,24 +111,4 @@ module Private {
111111
predicate ssaUpdateStep = RU::ssaUpdateStep/3;
112112

113113
Expr getABasicBlockExpr(BasicBlock bb) { result = bb.getANode() }
114-
115-
private predicate id(BasicBlock x, BasicBlock y) { x = y }
116-
117-
private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
118-
119-
private int getId(BasicBlock bb) { idOf(bb, result) }
120-
121-
/**
122-
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
123-
* in an arbitrary 1-based numbering of the input edges to `phi`.
124-
*/
125-
predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
126-
edge.phiInput(phi, inp) and
127-
edge =
128-
rank[r](SsaReadPositionPhiInputEdge e |
129-
e.phiInput(phi, _)
130-
|
131-
e order by getId(e.getOrigBlock())
132-
)
133-
}
134114
}

‎java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionCommon.qll‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
*/
44

55
private import SsaReadPositionSpecific
6+
import SsaReadPositionSpecific::Public
67

78
private newtype TSsaReadPosition =
89
TSsaReadPositionBlock(BasicBlock bb) { bb = getAReadBasicBlock(_) } or
@@ -55,3 +56,10 @@ class SsaReadPositionPhiInputEdge extends SsaReadPosition, TSsaReadPositionPhiIn
5556

5657
override string toString() { result = "edge" }
5758
}
59+
60+
/**
61+
* Holds if `rix` is the number of input edges to `phi`.
62+
*/
63+
predicate maxPhiInputRank(SsaPhiNode phi, int rix) {
64+
rix = max(int r | rankedPhiInput(phi, _, _, r))
65+
}

‎java/ql/lib/semmle/code/java/dataflow/internal/rangeanalysis/SsaReadPositionSpecific.qll‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44

55
private import semmle.code.java.dataflow.SSA as Ssa
66
private import semmle.code.java.controlflow.BasicBlocks as BB
7+
private import SsaReadPositionCommon
78

89
class SsaVariable = Ssa::SsaVariable;
910

@@ -13,3 +14,28 @@ class BasicBlock = BB::BasicBlock;
1314

1415
/** Gets a basic block in which SSA variable `v` is read. */
1516
BasicBlock getAReadBasicBlock(SsaVariable v) { result = v.getAUse().getBasicBlock() }
17+
18+
private predicate id(BasicBlock x, BasicBlock y) { x = y }
19+
20+
private predicate idOf(BasicBlock x, int y) = equivalenceRelation(id/2)(x, y)
21+
22+
private int getId(BasicBlock bb) { idOf(bb, result) }
23+
24+
/**
25+
* Declarations to be exposed to users of SsaReadPositionCommon
26+
*/
27+
module Public {
28+
/**
29+
* Holds if `inp` is an input to `phi` along `edge` and this input has index `r`
30+
* in an arbitrary 1-based numbering of the input edges to `phi`.
31+
*/
32+
predicate rankedPhiInput(SsaPhiNode phi, SsaVariable inp, SsaReadPositionPhiInputEdge edge, int r) {
33+
edge.phiInput(phi, inp) and
34+
edge =
35+
rank[r](SsaReadPositionPhiInputEdge e |
36+
e.phiInput(phi, _)
37+
|
38+
e order by getId(e.getOrigBlock())
39+
)
40+
}
41+
}

0 commit comments

Comments
 (0)