Consistency

Author: hvitved

csharp/ql/consistency-queries/SsaConsistency.ql

@@ -1,5 +1,6 @@
 import csharp
-import semmle.code.csharp.dataflow.internal.SsaImpl::Consistency
+import semmle.code.csharp.dataflow.internal.SsaImpl as Impl
+import Impl::Consistency
 import Ssa
 
 class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
@@ -10,6 +11,14 @@ class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
   }
 }
 
+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

ruby/ql/consistency-queries/SsaConsistency.ql

@@ -1,5 +1,6 @@
 import codeql.ruby.dataflow.SSA
-import codeql.ruby.dataflow.internal.SsaImpl::Consistency
+import codeql.ruby.dataflow.internal.SsaImpl
+import Consistency
 
 class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
   override predicate hasLocationInfo(
@@ -8,3 +9,11 @@ class MyRelevantDefinition extends RelevantDefinition, Ssa::Definition {
     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)
+  }
+}

shared/ssa/codeql/ssa/Ssa.qll

@@ -1055,18 +1055,40 @@ module Make<InputSig Input> {
       );
     }
 
+    /** 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) {
       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) {
       v = def.getSourceVariable() and
@@ -1075,6 +1097,15 @@ module Make<InputSig Input> {
       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 phiHasInputFromBlock(_, def, _) and
+      not phiReadHasInputFromBlock(_, 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) {
       exists(BasicBlock bbDef, int iDef | def.definesAt(v, bbDef, iDef) |
@@ -1086,5 +1117,19 @@ module Make<InputSig 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), _, _)
+      )
+    }
   }
 }