QL code and tests for C#/C++/JavaScript.

javascript/ql/src/meta/SSA/DeadDef.ql

@@ -0,0 +1,16 @@
+/**
+ * @name Dead SSA definition
+ * @description Each SSA definition should have at least one use.
+ * @kind problem
+ * @problem.severity error
+ * @id js/sanity/dead-ssa-definition
+ * @tags sanity
+ */
+
+import javascript
+
+from SsaVariable d
+where not exists (d.getAUse()) and
+      not d = any(SsaPseudoDefinition phi).getAnInput() and
+      d.getSourceVariable() instanceof PurelyLocalVariable
+select d, "Dead SSA definition " + d + "."

javascript/ql/src/meta/SSA/Dominance.ql

@@ -0,0 +1,32 @@
+/**
+ * @name SSA definition does not dominate use
+ * @description Every use of an SSA variable should be dominated by its
+ *              definition.
+ * @kind problem
+ * @problem.severity error
+ * @id js/sanity/non-dominating-ssa-definition
+ * @tags sanity
+ */
+
+import javascript
+
+/**
+ * Holds if SSA definition `def` dominates `use`,
+ * which is a use of the same variable.
+ */
+predicate dominates(SsaDefinition def, VarUse use) {
+  exists (SsaSourceVariable v,
+          ReachableBasicBlock defbb, int defidx,
+          ReachableBasicBlock usebb, int useidx |
+    def.definesAt(defbb, defidx, v) and usebb.useAt(useidx, v, use) |
+    defbb = usebb and defidx <= useidx or
+    defbb.strictlyDominates(usebb)
+  )
+}
+
+from VarUse u, SsaDefinition d
+where u.getVariable() instanceof SsaSourceVariable and
+      exists (ReachableBasicBlock bb | u = bb.getANode()) and
+      u = d.getVariable().getAUse() and
+      not dominates(d, u)
+select u, "Variable use is not dominated by its definition $@.", d, d.toString()

javascript/ql/src/meta/SSA/MultipleDefs.ql

@@ -0,0 +1,19 @@
+/**
+ * @name Variable use with more than one corresponding SSA variable
+ * @description Every reachable use of an SSA-convertible variable should correspond to
+ *              exactly one SSA variable.
+ * @kind problem
+ * @problem.severity error
+ * @id js/sanity/ambiguous-ssa-definition
+ * @tags sanity
+ */
+
+import javascript
+
+from VarUse u, int n, SsaVariable v
+where u.getVariable() instanceof SsaSourceVariable and
+      exists (ReachableBasicBlock bb | u = bb.getANode()) and
+      n = count(u.getSsaVariable()) and
+      n > 1 and
+      v = u.getSsaVariable()
+select u, "Variable use has " + n + " corresponding SSA variables: $@.", v, v.toString()

javascript/ql/src/meta/SSA/MultipleRefinementInputs.ql

@@ -0,0 +1,16 @@
+/**
+ * @name Refinement node with more than one input
+ * @description Every SSA refinement node should have exactly one input.
+ * @kind problem
+ * @problem.severity error
+ * @id js/sanity/ambiguous-refinement-node
+ * @tags sanity
+ */
+
+import javascript
+
+from SsaRefinementNode ref, int n, SsaDefinition input
+where n = count(ref.getAnInput()) and
+      n > 1 and
+      input = ref.getAnInput()
+select ref, "Refinement node has " + n + " inputs: $@.", input, input.toString()

javascript/ql/src/meta/SSA/NoDefs.ql

@@ -0,0 +1,17 @@
+/**
+ * @name Variable use with no corresponding SSA variable
+ * @description Every reachable use of an SSA-convertible variable should correspond to
+ *              exactly one SSA variable.
+ * @kind problem
+ * @problem.severity error
+ * @id js/sanity/dead-ssa-use
+ * @tags sanity
+ */
+
+import javascript
+
+from VarUse u
+where u.getVariable() instanceof SsaSourceVariable and
+      exists (ReachableBasicBlock bb | u = bb.getANode()) and
+      not exists(u.getSsaVariable())
+select u, "Variable use has no corresponding SSA variable."

javascript/ql/src/meta/SSA/NoPhiInputs.ql

@@ -0,0 +1,14 @@
+/**
+ * @name Phi node without inputs
+ * @description Every SSA phi node should have two or more inputs.
+ * @kind problem
+ * @problem.severity error
+ * @id js/sanity/dead-phi-node
+ * @tags sanity
+ */
+
+import javascript
+
+from SsaPhiNode phi
+where not exists(phi.getAnInput())
+select phi, "Phi node without inputs."

javascript/ql/src/meta/SSA/NoRefinementInputs.ql

@@ -0,0 +1,14 @@
+/**
+ * @name Refinement node without inputs
+ * @description Every SSA refinement node should have exactly one input.
+ * @kind problem
+ * @problem.severity error
+ * @id js/sanity/dead-refinement-node
+ * @tags sanity
+ */
+
+import javascript
+
+from SsaRefinementNode ref
+where not exists(ref.getAnInput())
+select ref, "Refinement node without inputs."

javascript/ql/src/meta/SSA/SinglePhiInput.ql

@@ -0,0 +1,14 @@
+/**
+ * @name Phi node with a single input
+ * @description Every SSA phi node should have two or more inputs.
+ * @kind problem
+ * @problem.severity error
+ * @id js/sanity/trivial-phi-node
+ * @tags sanity
+ */
+
+import javascript
+
+from SsaPhiNode phi
+where count(phi.getAnInput()) = 1
+select phi, "Phi node with exactly one input $@.", phi.getAnInput(), phi.getAnInput().toString()