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

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

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

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

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

/** Holds if a read can be reached from multiple definitions. */
query predicate nonUniqueDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
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. */
query predicate readWithoutDef(SourceVariable v, BasicBlock bb, int i) {
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. */
query predicate deadDef(RelevantDefinition def, SourceVariable v) {
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. */
query predicate notDominatedByDef(RelevantDefinition def, SourceVariable v, BasicBlock bb, int i) {
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