SSA/C#/Ruby/Rust: Clean up SSA consistency queries.

The RelevantDefinition class is no longer needed since the introduction
of LocationSig.
This commit is contained in:
Anders Schack-Mulligen
2025-02-26 14:01:01 +01:00
parent 8474a47c2b
commit 00b8c80c24
4 changed files with 3 additions and 103 deletions

View File

@@ -3,22 +3,6 @@ import semmle.code.csharp.dataflow.internal.SsaImpl as Impl
import Impl::Consistency
import Ssa
class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
override predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
}
}
class MyRelevantDefinitionExt extends RelevantDefinitionExt, Impl::DefinitionExt {
override predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
}
}
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

@@ -1,19 +1,3 @@
import codeql.ruby.dataflow.SSA
import codeql.ruby.dataflow.internal.SsaImpl
import Consistency
class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
override predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
}
}
class MyRelevantDefinitionExt extends RelevantDefinitionExt, DefinitionExt {
override predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
}
}

View File

@@ -1,19 +1,3 @@
import codeql.rust.dataflow.Ssa
import codeql.rust.dataflow.internal.SsaImpl
import Consistency
class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
override predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
}
}
class MyRelevantDefinitionExt extends RelevantDefinitionExt, DefinitionExt {
override predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
) {
this.getLocation().hasLocationInfo(filepath, startline, startcolumn, endline, endcolumn)
}
}

View File

@@ -1350,66 +1350,28 @@ module Make<LocationSig Location, InputSig<Location> Input> {
/** Provides a set of consistency queries. */
module Consistency {
/** A definition that is relevant for the consistency queries. */
abstract class RelevantDefinition extends Definition {
/** Override this predicate to ensure locations in consistency results. */
abstract predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
);
}
/** A definition that is relevant for the consistency queries. */
abstract class RelevantDefinitionExt extends DefinitionExt {
/** Override this predicate to ensure locations in consistency results. */
abstract predicate hasLocationInfo(
string filepath, int startline, int startcolumn, int endline, int endcolumn
);
}
/** Holds if a read can be reached from multiple definitions. */
query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
query predicate nonUniqueDef(Definition def, SourceVariable v, BasicBlock bb, int i) {
ssaDefReachesRead(v, def, bb, i) and
not exists(unique(Definition def0 | ssaDefReachesRead(v, def0, bb, i)))
}
/** Holds if a read can be reached from multiple definitions. */
query predicate nonUniqueDefExt(
RelevantDefinitionExt def, SourceVariable v, BasicBlock bb, int i
) {
ssaDefReachesReadExt(v, def, bb, i) and
not exists(unique(DefinitionExt def0 | ssaDefReachesReadExt(v, def0, bb, i)))
}
/** Holds if a read cannot be reached from a definition. */
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
variableRead(bb, i, v, _) and
not ssaDefReachesRead(v, _, bb, i)
}
/** Holds if a read cannot be reached from a definition. */
query predicate readWithoutDefExt(SourceVariable v, BasicBlock bb, int i) {
variableRead(bb, i, v, _) and
not ssaDefReachesReadExt(v, _, bb, i)
}
/** Holds if a definition cannot reach a read. */
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
query predicate deadDef(Definition def, SourceVariable v) {
v = def.getSourceVariable() and
not ssaDefReachesRead(_, def, _, _) and
not phiHasInputFromBlock(_, def, _) and
not uncertainWriteDefinitionInput(_, def)
}
/** Holds if a definition cannot reach a read. */
query predicate deadDefExt(RelevantDefinitionExt def, SourceVariable v) {
v = def.getSourceVariable() and
not ssaDefReachesReadExt(_, def, _, _) and
not phiHasInputFromBlockExt(_, def, _) and
not uncertainWriteDefinitionInput(_, def)
}
/** Holds if a read is not dominated by a definition. */
query predicate notDominatedByDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
query predicate notDominatedByDef(Definition def, SourceVariable v, BasicBlock bb, int i) {
exists(BasicBlock bbDef, int iDef | def.definesAt(v, bbDef, iDef) |
ssaDefReachesReadWithinBlock(v, def, bb, i) and
(bb != bbDef or i < iDef)
@@ -1419,20 +1381,6 @@ module Make<LocationSig Location, InputSig<Location> Input> {
not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _)
)
}
/** Holds if a read is not dominated by a definition. */
query predicate notDominatedByDefExt(
RelevantDefinitionExt def, SourceVariable v, BasicBlock bb, int i
) {
exists(BasicBlock bbDef, int iDef | def.definesAt(v, bbDef, iDef, _) |
ssaDefReachesReadWithinBlock(v, def, bb, i) and
(bb != bbDef or i < iDef)
or
ssaDefReachesReadExt(v, def, bb, i) and
not ssaDefReachesReadWithinBlock(v, def, bb, i) and
not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _, _)
)
}
}
/** Provides the input to `DataFlowIntegration`. */