Merge remote-tracking branch 'upstream/main' into dbartol/use-workspace-versions

This commit is contained in:
Dave Bartolomeo
2022-11-02 12:38:03 -04:00
80 changed files with 1558 additions and 586 deletions

View File

@@ -1,8 +1,8 @@
import csharp
import semmle.code.csharp.dataflow.internal.SsaImpl::Consistency
import semmle.code.csharp.dataflow.internal.SsaImpl::Consistency as Consistency
import Ssa
class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
class MyRelevantDefinition extends Consistency::RelevantDefinition, Ssa::Definition {
override predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
@@ -10,6 +10,14 @@ class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
}
}
query predicate nonUniqueDef = Consistency::nonUniqueDef/4;
query predicate readWithoutDef = Consistency::readWithoutDef/3;
query predicate deadDef = Consistency::deadDef/2;
query predicate notDominatedByDef = Consistency::notDominatedByDef/4;
query predicate localDeclWithSsaDef(LocalVariableDeclExpr d) {
// Local variables in C# must be initialized before every use, so uninitialized
// local variables should not have an SSA definition, as that would imply that

View File

@@ -1067,6 +1067,59 @@ private predicate variableReadPseudo(ControlFlow::BasicBlock bb, int i, Ssa::Sou
capturedReadIn(bb, i, v, _, _, _)
}
pragma[noinline]
private predicate adjacentDefRead(
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2,
SsaInput::SourceVariable v
) {
adjacentDefRead(def, bb1, i1, bb2, i2) and
v = def.getSourceVariable()
}
private predicate adjacentDefReachesRead(
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
) {
exists(SsaInput::SourceVariable v | adjacentDefRead(def, bb1, i1, bb2, i2, v) |
def.definesAt(v, bb1, i1)
or
SsaInput::variableRead(bb1, i1, v, true)
)
or
exists(SsaInput::BasicBlock bb3, int i3 |
adjacentDefReachesRead(def, bb1, i1, bb3, i3) and
SsaInput::variableRead(bb3, i3, _, false) and
adjacentDefRead(def, bb3, i3, bb2, i2)
)
}
/** Same as `adjacentDefRead`, but skips uncertain reads. */
pragma[nomagic]
private predicate adjacentDefSkipUncertainReads(
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
) {
adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
SsaInput::variableRead(bb2, i2, _, true)
}
private predicate adjacentDefReachesUncertainRead(
Definition def, SsaInput::BasicBlock bb1, int i1, SsaInput::BasicBlock bb2, int i2
) {
adjacentDefReachesRead(def, bb1, i1, bb2, i2) and
SsaInput::variableRead(bb2, i2, _, false)
}
/** Same as `lastRefRedef`, but skips uncertain reads. */
pragma[nomagic]
private predicate lastRefSkipUncertainReads(Definition def, SsaInput::BasicBlock bb, int i) {
lastRef(def, bb, i) and
not SsaInput::variableRead(bb, i, def.getSourceVariable(), false)
or
exists(SsaInput::BasicBlock bb0, int i0 |
lastRef(def, bb0, i0) and
adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
)
}
cached
private module Cached {
cached
@@ -1237,7 +1290,7 @@ private module Cached {
predicate firstReadSameVar(Definition def, ControlFlow::Node cfn) {
exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
def.definesAt(_, bb1, i1) and
adjacentDefNoUncertainReads(def, bb1, i1, bb2, i2) and
adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
cfn = bb2.getNode(i2)
)
}
@@ -1252,20 +1305,27 @@ private module Cached {
exists(ControlFlow::BasicBlock bb1, int i1, ControlFlow::BasicBlock bb2, int i2 |
cfn1 = bb1.getNode(i1) and
variableReadActual(bb1, i1, _) and
adjacentDefNoUncertainReads(def, bb1, i1, bb2, i2) and
adjacentDefSkipUncertainReads(def, bb1, i1, bb2, i2) and
cfn2 = bb2.getNode(i2)
)
}
/** Same as `lastRefRedef`, but skips uncertain reads. */
cached
predicate lastRefBeforeRedef(Definition def, ControlFlow::BasicBlock bb, int i, Definition next) {
lastRefRedefNoUncertainReads(def, bb, i, next)
lastRefRedef(def, bb, i, next) and
not SsaInput::variableRead(bb, i, def.getSourceVariable(), false)
or
exists(SsaInput::BasicBlock bb0, int i0 |
lastRefRedef(def, bb0, i0, next) and
adjacentDefReachesUncertainRead(def, bb, i, bb0, i0)
)
}
cached
predicate lastReadSameVar(Definition def, ControlFlow::Node cfn) {
exists(ControlFlow::BasicBlock bb, int i |
lastRefNoUncertainReads(def, bb, i) and
lastRefSkipUncertainReads(def, bb, i) and
variableReadActual(bb, i, _) and
cfn = bb.getNode(i)
)