Skip to content

Commit 1c616d1

Browse files
authored
Merge pull request github#18819 from aschackmull/ssa/refactor-phiread3
Ssa: Refactor shared SSA in preparation for eliminating phi-read definitions
2 parents 26da997 + 8c0cc07 commit 1c616d1

File tree

10 files changed

+448
-280
lines changed

10 files changed

+448
-280
lines changed

csharp/ql/lib/semmle/code/csharp/dataflow/internal/SsaImpl.qll

Lines changed: 11 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -734,15 +734,15 @@ private predicate variableReadPseudo(ControlFlow::BasicBlock bb, int i, Ssa::Sou
734734
}
735735

736736
pragma[noinline]
737-
private predicate adjacentDefRead(
737+
deprecated private predicate adjacentDefRead(
738738
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
739739
SsaInput::SourceVariable v
740740
) {
741741
Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
742742
v = def.getSourceVariable()
743743
}
744744

745-
private predicate adjacentDefReachesRead(
745+
deprecated private predicate adjacentDefReachesRead(
746746
Definition def, SsaInput::SourceVariable v, SsaInput::BasicBlock bb1, int i1,
747747
SsaInput::BasicBlock bb2, int i2
748748
) {
@@ -760,18 +760,7 @@ private predicate adjacentDefReachesRead(
760760
)
761761
}
762762

763-
/** Same as `adjacentDefRead`, but skips uncertain reads. */
764-
pragma[nomagic]
765-
private predicate adjacentDefSkipUncertainReads(
766-
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
767-
) {
768-
exists(SsaInput::SourceVariable v |
769-
adjacentDefReachesRead(def, v, bb1, i1, bb2, i2) and
770-
SsaInput::variableRead(bb2, i2, v, true)
771-
)
772-
}
773-
774-
private predicate adjacentDefReachesUncertainRead(
763+
deprecated private predicate adjacentDefReachesUncertainRead(
775764
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
776765
) {
777766
exists(SsaInput::SourceVariable v |
@@ -933,10 +922,8 @@ private module Cached {
933922
*/
934923
cached
935924
predicate firstReadSameVar(Definition def, ControlFlow::Node cfn) {
936-
exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
937-
def.definesAt(_, bb1, i1) and
938-
adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
939-
cfn = bb2.getNode(i2)
925+
exists(ControlFlow::BasicBlock bb, int i |
926+
Impl::firstUse(def, bb, i, true) and cfn = bb.getNode(i)
940927
)
941928
}
942929

@@ -947,25 +934,17 @@ private module Cached {
947934
*/
948935
cached
949936
predicate adjacentReadPairSameVar(Definition def, ControlFlow::Node cfn1, ControlFlow::Node cfn2) {
950-
exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
937+
exists(
938+
ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2,
939+
Ssa::SourceVariable v
940+
|
941+
Impl::ssaDefReachesRead(v, def, bb1, i1) and
942+
Impl::adjacentUseUse(bb1, i1, bb2, i2, v, true) and
951943
cfn1 = bb1.getNode(i1) and
952-
variableReadActual(bb1, i1, _) and
953-
adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
954944
cfn2 = bb2.getNode(i2)
955945
)
956946
}
957947

958-
cached
959-
predicate lastRefBeforeRedef(Definition def, ControlFlow::BasicBlock bb, int i, Definition next) {
960-
Impl::lastRefRedef(def, bb, i, next) and
961-
not SsaInput::variableRead(bb, i, def.getSourceVariable(), false)
962-
or
963-
exists(SsaInput::BasicBlock bb0, int i0 |
964-
Impl::lastRefRedef(def, bb0, i0, next) and
965-
adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
966-
)
967-
}
968-
969948
cached
970949
Definition uncertainWriteDefinitionInput(UncertainWriteDefinition def) {
971950
Impl::uncertainWriteDefinitionInput(def, result)

java/ql/lib/semmle/code/java/dataflow/internal/SsaImpl.qll

Lines changed: 12 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -490,26 +490,11 @@ private module Cached {
490490
)
491491
}
492492

493-
pragma[nomagic]
494-
private predicate captureDefReaches(Definition def, SsaInput::BasicBlock bb2, int i2) {
495-
variableCapture(def.getSourceVariable(), _, _, _) and
496-
exists(SsaInput::BasicBlock bb1, int i1 |
497-
Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
498-
def.definesAt(_, bb1, i1)
499-
)
500-
or
501-
exists(SsaInput::BasicBlock bb3, int i3 |
502-
captureDefReaches(def, bb3, i3) and
503-
SsaInput::variableRead(bb3, i3, _, _) and
504-
Impl::adjacentDefRead(def, bb3, i3, bb2, i2)
505-
)
506-
}
507-
508493
/** Holds if `init` is a closure variable that captures the value of `capturedvar`. */
509494
cached
510495
predicate captures(SsaImplicitInit init, SsaVariable capturedvar) {
511496
exists(BasicBlock bb, int i |
512-
captureDefReaches(capturedvar, bb, i) and
497+
Impl::ssaDefReachesRead(_, capturedvar, bb, i) and
513498
variableCapture(capturedvar.getSourceVariable(), init.getSourceVariable(), bb, i)
514499
)
515500
}
@@ -523,34 +508,15 @@ private module Cached {
523508
Impl::uncertainWriteDefinitionInput(redef, def)
524509
}
525510

526-
pragma[nomagic]
527-
private predicate defReaches(Definition def, DataFlowIntegration::Node node) {
528-
exists(DataFlowIntegration::SsaDefinitionExtNode nodeFrom |
529-
nodeFrom.getDefinitionExt() = def and
530-
DataFlowIntegrationImpl::localFlowStep(_, nodeFrom, node, false)
531-
)
532-
or
533-
exists(DataFlowIntegration::Node mid |
534-
defReaches(def, mid) and
535-
DataFlowIntegrationImpl::localFlowStep(_, mid, node, _)
536-
|
537-
// flow into phi input node
538-
mid instanceof DataFlowIntegration::SsaInputNode
539-
or
540-
// flow into definition
541-
mid instanceof DataFlowIntegration::SsaDefinitionExtNode
542-
)
543-
}
544-
545511
/**
546512
* Holds if the value defined at `def` can reach `use` without passing through
547513
* any other uses, but possibly through phi nodes and uncertain implicit updates.
548514
*/
549515
cached
550516
predicate firstUse(Definition def, VarRead use) {
551-
exists(DataFlowIntegration::ExprNode nodeTo |
552-
nodeTo.getExpr() = use and
553-
defReaches(def, nodeTo)
517+
exists(BasicBlock bb, int i |
518+
Impl::firstUse(def, bb, i, _) and
519+
use.getControlFlowNode() = bb.getNode(i)
554520
)
555521
}
556522

@@ -609,40 +575,17 @@ private module Cached {
609575

610576
cached
611577
module SsaPublic {
612-
pragma[nomagic]
613-
private predicate useReaches(VarRead use, DataFlowIntegration::Node node, boolean sameVar) {
614-
exists(DataFlowIntegration::ExprNode nodeFrom |
615-
nodeFrom.getExpr() = use and
616-
DataFlowIntegration::localFlowStep(_, nodeFrom, node, true) and
617-
sameVar = true
618-
)
619-
or
620-
exists(DataFlowIntegration::Node mid, boolean sameVarMid |
621-
useReaches(use, mid, sameVarMid) and
622-
DataFlowIntegration::localFlowStep(_, mid, node, _)
623-
|
624-
exists(Impl::DefinitionExt def |
625-
// flow into definition
626-
def = mid.(DataFlowIntegration::SsaDefinitionExtNode).getDefinitionExt()
627-
or
628-
// flow into phi input node
629-
def = mid.(DataFlowIntegration::SsaInputNode).getDefinitionExt()
630-
|
631-
if def instanceof Impl::PhiReadNode then sameVar = sameVarMid else sameVar = false
632-
)
633-
)
634-
}
635-
636578
/**
637579
* Holds if `use1` and `use2` form an adjacent use-use-pair of the same SSA
638580
* variable, that is, the value read in `use1` can reach `use2` without passing
639581
* through any other use or any SSA definition of the variable.
640582
*/
641583
cached
642584
predicate adjacentUseUseSameVar(VarRead use1, VarRead use2) {
643-
exists(DataFlowIntegration::ExprNode nodeTo |
644-
nodeTo.getExpr() = use2 and
645-
useReaches(use1, nodeTo, true)
585+
exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
586+
use1.getControlFlowNode() = bb1.getNode(i1) and
587+
use2.getControlFlowNode() = bb2.getNode(i2) and
588+
Impl::adjacentUseUse(bb1, i1, bb2, i2, _, true)
646589
)
647590
}
648591

@@ -654,9 +597,10 @@ private module Cached {
654597
*/
655598
cached
656599
predicate adjacentUseUse(VarRead use1, VarRead use2) {
657-
exists(DataFlowIntegration::ExprNode nodeTo |
658-
nodeTo.getExpr() = use2 and
659-
useReaches(use1, nodeTo, _)
600+
exists(BasicBlock bb1, int i1, BasicBlock bb2, int i2 |
601+
use1.getControlFlowNode() = bb1.getNode(i1) and
602+
use2.getControlFlowNode() = bb2.getNode(i2) and
603+
Impl::adjacentUseUse(bb1, i1, bb2, i2, _, _)
660604
)
661605
}
662606
}
Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
public class A {
2+
Object source() { return null; }
3+
void sink(Object o) { }
4+
5+
boolean isSafe(Object o) { return o == null; }
6+
7+
void foo() {
8+
Object x = source();
9+
if (!isSafe(x)) {
10+
x = null;
11+
}
12+
sink(x);
13+
14+
x = source();
15+
if (!isSafe(x)) {
16+
if (isSafe(x)) {
17+
sink(x);
18+
} else {
19+
throw new RuntimeException();
20+
}
21+
}
22+
sink(x);
23+
}
24+
}

java/ql/test/library-tests/dataflow/ssa/test.expected

Whitespace-only changes.
Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,31 @@
1+
import java
2+
import semmle.code.java.controlflow.Guards
3+
import semmle.code.java.dataflow.DataFlow
4+
5+
private predicate isSafe(Guard g, Expr checked, boolean branch) {
6+
exists(MethodCall mc | g = mc |
7+
mc.getMethod().hasName("isSafe") and
8+
checked = mc.getAnArgument() and
9+
branch = true
10+
)
11+
}
12+
13+
module TestConfig implements DataFlow::ConfigSig {
14+
predicate isSource(DataFlow::Node source) {
15+
source.asExpr().(MethodCall).getMethod().hasName("source")
16+
}
17+
18+
predicate isSink(DataFlow::Node sink) {
19+
exists(MethodCall mc | mc.getMethod().hasName("sink") and mc.getAnArgument() = sink.asExpr())
20+
}
21+
22+
predicate isBarrier(DataFlow::Node node) {
23+
node = DataFlow::BarrierGuard<isSafe/3>::getABarrierNode()
24+
}
25+
}
26+
27+
module Flow = DataFlow::Global<TestConfig>;
28+
29+
from DataFlow::Node source, DataFlow::Node sink
30+
where Flow::flow(source, sink)
31+
select source, sink

java/ql/test/library-tests/pattern-switch/dfg/GuardTest.java

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -24,13 +24,6 @@ case String s when isSafe(s):
2424
break;
2525

2626
}
27-
28-
String s2 = "string";
29-
30-
if (!isSafe(s2)) {
31-
s2 = null;
32-
}
33-
sink(s2);
3427
}
3528

3629
}

ruby/ql/lib/codeql/ruby/dataflow/internal/SsaImpl.qll

Lines changed: 4 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -222,15 +222,6 @@ private predicate hasVariableReadWithCapturedWrite(
222222
variableReadActualInOuterScope(bb, i, v, scope)
223223
}
224224

225-
pragma[noinline]
226-
private predicate adjacentDefRead(
227-
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
228-
SsaInput::SourceVariable v
229-
) {
230-
Impl::adjacentDefRead(def, bb1, i1, bb2, i2) and
231-
v = def.getSourceVariable()
232-
}
233-
234225
pragma[noinline]
235226
deprecated private predicate adjacentDefReadExt(
236227
DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
@@ -240,22 +231,6 @@ deprecated private predicate adjacentDefReadExt(
240231
v = def.getSourceVariable()
241232
}
242233

243-
private predicate adjacentDefReachesRead(
244-
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
245-
) {
246-
exists(SsaInput::SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
247-
def.definesAt(v, bb1, i1)
248-
or
249-
SsaInput::variableRead(bb1, i1, v, true)
250-
)
251-
or
252-
exists(SsaInput::BasicBlock bb3, int i3 |
253-
adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
254-
SsaInput::variableRead(bb3, i3, _, false) and
255-
Impl::adjacentDefRead(def, bb3, i3, bb2, i2)
256-
)
257-
}
258-
259234
deprecated private predicate adjacentDefReachesReadExt(
260235
DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
261236
) {
@@ -272,15 +247,6 @@ deprecated private predicate adjacentDefReachesReadExt(
272247
)
273248
}
274249

275-
/** Same as `adjacentDefRead`, but skips uncertain reads. */
276-
pragma[nomagic]
277-
private predicate adjacentDefSkipUncertainReads(
278-
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
279-
) {
280-
adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
281-
SsaInput::variableRead(bb2, i2, _, true)
282-
}
283-
284250
deprecated private predicate adjacentDefReachesUncertainReadExt(
285251
DefinitionExt def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
286252
) {
@@ -391,11 +357,7 @@ private module Cached {
391357
*/
392358
cached
393359
predicate firstRead(Definition def, VariableReadAccessCfgNode read) {
394-
exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2 |
395-
def.definesAt(_, bb1, i1) and
396-
adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
397-
read = bb2.getNode(i2)
398-
)
360+
exists(Cfg::BasicBlock bb, int i | Impl::firstUse(def, bb, i, true) and read = bb.getNode(i))
399361
}
400362

401363
/**
@@ -407,10 +369,10 @@ private module Cached {
407369
predicate adjacentReadPair(
408370
Definition def, VariableReadAccessCfgNode read1, VariableReadAccessCfgNode read2
409371
) {
410-
exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2 |
372+
exists(Cfg::BasicBlock bb1, int i1, Cfg::BasicBlock bb2, int i2, LocalVariable v |
373+
Impl::ssaDefReachesRead(v, def, bb1, i1) and
374+
Impl::adjacentUseUse(bb1, i1, bb2, i2, v, true) and
411375
read1 = bb1.getNode(i1) and
412-
variableReadActual(bb1, i1, _) and
413-
adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
414376
read2 = bb2.getNode(i2)
415377
)
416378
}

ruby/ql/test/library-tests/variables/ssa.expected

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -527,7 +527,6 @@ adjacentReads
527527
| nested_scopes.rb:8:5:35:7 | self (N) | nested_scopes.rb:8:5:35:7 | self | nested_scopes.rb:30:16:30:19 | self | nested_scopes.rb:34:7:34:12 | self |
528528
| nested_scopes.rb:13:11:13:11 | a | nested_scopes.rb:13:11:13:11 | a | nested_scopes.rb:14:16:14:16 | a | nested_scopes.rb:15:11:15:11 | a |
529529
| nested_scopes.rb:27:7:29:9 | self (show) | nested_scopes.rb:27:7:29:9 | self | nested_scopes.rb:28:11:28:16 | self | nested_scopes.rb:28:16:28:16 | self |
530-
| nested_scopes.rb:30:16:30:19 | self (class << ...) | nested_scopes.rb:30:7:33:9 | self | nested_scopes.rb:30:16:30:19 | self | nested_scopes.rb:32:11:32:16 | self |
531530
| parameters.rb:1:9:5:3 | <captured entry> self | parameters.rb:1:1:62:1 | self | parameters.rb:3:4:3:9 | self | parameters.rb:4:4:4:9 | self |
532531
| parameters.rb:7:26:7:31 | pizzas | parameters.rb:7:26:7:31 | pizzas | parameters.rb:8:6:8:11 | pizzas | parameters.rb:11:14:11:19 | pizzas |
533532
| parameters.rb:25:1:28:3 | self (opt_param) | parameters.rb:25:1:28:3 | self | parameters.rb:26:3:26:11 | self | parameters.rb:27:3:27:11 | self |

0 commit comments

Comments
 (0)