Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 2 additions & 10 deletions csharp/ql/consistency-queries/SsaConsistency.ql
Original file line number Diff line number Diff line change
@@ -1,23 +1,15 @@
import csharp
import semmle.code.csharp.dataflow.internal.SsaImpl::Consistency as Consistency
import semmle.code.csharp.dataflow.internal.SsaImpl::Consistency
import Ssa

class MyRelevantDefinition extends Consistency::RelevantDefinition, Ssa::Definition {
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)
}
}

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
Expand Down
12 changes: 2 additions & 10 deletions ruby/ql/consistency-queries/SsaConsistency.ql
Original file line number Diff line number Diff line change
@@ -1,18 +1,10 @@
import codeql.ruby.dataflow.SSA
import codeql.ruby.dataflow.internal.SsaImpl::Consistency as Consistency
import codeql.ruby.dataflow.internal.SsaImpl::Consistency

class MyRelevantDefinition extends Consistency::RelevantDefinition, Ssa::Definition {
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)
}
}

query predicate nonUniqueDef = Consistency::nonUniqueDef/4;

query predicate readWithoutDef = Consistency::readWithoutDef/3;

query predicate deadDef = Consistency::deadDef/2;

query predicate notDominatedByDef = Consistency::notDominatedByDef/4;
20 changes: 12 additions & 8 deletions shared/ssa/codeql/ssa/Ssa.qll
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,10 @@ signature module InputSig {
* A basic block, that is, a maximal straight-line sequence of control flow nodes
* without branches or joins.
*/
class BasicBlock;
class BasicBlock {
/** Gets a textual representation of this basic block. */
string toString();
}

/**
* Gets the basic block that immediately dominates basic block `bb`, if any.
Expand Down Expand Up @@ -43,7 +46,10 @@ signature module InputSig {
class ExitBasicBlock extends BasicBlock;

/** A variable that can be SSA converted. */
class SourceVariable;
class SourceVariable {
/** Gets a textual representation of this variable. */
string toString();
}

/**
* Holds if the `i`th node of basic block `bb` is a (potential) write to source
Expand Down Expand Up @@ -846,8 +852,6 @@ module Make<InputSig Input> {
}

/** Provides a set of consistency queries. */
// TODO: Make these `query` predicates once class signatures are supported
// (`SourceVariable` and `BasicBlock` must have `toString`)
module Consistency {
/** A definition that is relevant for the consistency queries. */
abstract class RelevantDefinition extends Definition {
Expand All @@ -858,27 +862,27 @@ module Make<InputSig Input> {
}

/** Holds if a read can be reached from multiple definitions. */
predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
query predicate nonUniqueDef(RelevantDefinition 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 cannot be reached from a definition. */
predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
variableRead(bb, i, v, _) and
not ssaDefReachesRead(v, _, bb, i)
}

/** Holds if a definition cannot reach a read. */
predicate deadDef(RelevantDefinition def, SourceVariable v) {
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
v = def.getSourceVariable() and
not ssaDefReachesRead(_, def, _, _) and
not phiHasInputFromBlock(_, def, _) and
not uncertainWriteDefinitionInput(_, def)
}

/** Holds if a read is not dominated by a definition. */
predicate notDominatedByDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
query predicate notDominatedByDef(RelevantDefinition 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)
Expand Down