Revert "Revert "SSA: Turn consistency predicates into `query` predicates""

This commit is contained in:
Tom Hvitved 2022-11-02 11:37:37 +01:00 коммит произвёл GitHub
Родитель f603d96f48
Коммит 1e3adcd14e
Не найден ключ, соответствующий данной подписи
Идентификатор ключа GPG: 4AEE18F83AFDEB23
3 изменённых файлов: 16 добавлений и 28 удалений

Просмотреть файл

@ -1,8 +1,8 @@
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
) {
@ -10,14 +10,6 @@ class MyRelevantDefinition extends Consistency::RelevantDefinition, Ssa::Definit
}
}
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

Просмотреть файл

@ -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;

Просмотреть файл

@ -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.
@ -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
@ -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 {
@ -858,19 +862,19 @@ 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
@ -878,7 +882,7 @@ module Make<InputSig Input> {
}
/** 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)