Shared: Disjunctive barrier guards for free

Author: hvitved

shared/ssa/codeql/ssa/Ssa.qll

@@ -1219,6 +1219,133 @@ module Make<LocationSig Location, InputSig<Location> Input> {
 
       /** Holds if the `i`th node of basic block `bb` evaluates this guard. */
       predicate hasCfgNode(BasicBlock bb, int i);
+
+      /** Gets the location of this guard. */
+      Location getLocation();
+    }
+
+    /**
+     * A logical conjunction guard.
+     *
+     * Guards are automatically lifted to conjunctions:
+     *
+     * ```csharp
+     * // Example 1
+     * if (x == "safe" && x == "safe")
+     * {
+     *     sink(x); // guarded
+     * }
+     * else
+     * {
+     *     sink(x); // unguarded
+     * }
+     *
+     * // Example 2
+     * if (x == "safe" && x != "safe2")
+     * {
+     *     sink(x); // guarded
+     * }
+     * else
+     * {
+     *     sink(x); // unguarded
+     * }
+     *
+     * // Example 3
+     * if (x != "safe" && x == "safe2")
+     * {
+     *     sink(x); // guarded
+     * }
+     * else
+     * {
+     *     sink(x); // unguarded
+     * }
+     *
+     * // Example 4
+     * if (x != "safe1" && x != "safe2")
+     * {
+     *     sink(x); // unguarded
+     * }
+     * else
+     * {
+     *     sink(x); // guarded
+     * }
+     * ```
+     *
+     * Examples 1--3 should normally be handled via the control-flow graph (CFG)
+     * implementation, but they are included in our logic for completeness.
+     *
+     * Example 4, which does not come for free just from the CFG, requires that
+     * logical conjunctions be modeled post-order in the CFG, as they will
+     * otherwise not dominate their `else` branch.
+     */
+    class AndGuard extends Guard {
+      /** Gets the left operand of this conjunction. */
+      Guard getLeftOperand();
+
+      /** Gets the right operand of this conjunction. */
+      Guard getRightOperand();
+    }
+
+    /**
+     * A logical disjunction guard.
+     *
+     * Guards are automatically lifted to disjunctions:
+     *
+     * ```csharp
+     * // Example 1
+     * if (x == "safe1" || x == "safe2")
+     * {
+     *     sink(x); // guarded
+     * }
+     * else
+     * {
+     *     sink(x); // unguarded
+     * }
+     *
+     * // Example 2
+     * if (x == "safe" || x != "safe2")
+     * {
+     *     sink(x); // unguarded
+     * }
+     * else
+     * {
+     *     sink(x); // guarded
+     * }
+     *
+     * // Example 3
+     * if (x != "safe" || x == "safe2")
+     * {
+     *     sink(x); // unguarded
+     * }
+     * else
+     * {
+     *     sink(x); // guarded
+     * }
+     *
+     * // Example 4
+     * if (x != "safe" || x != "safe")
+     * {
+     *     sink(x); // unguarded
+     * }
+     * else
+     * {
+     *     sink(x); // guarded
+     * }
+     * ```
+     *
+     * Examples 1--3 should normally be handled via the control-flow graph (CFG)
+     * implementation, but they are included in our logic for completeness.
+     *
+     * Example 4, which does not come for free just from the CFG, requires that
+     * logical disjunctions be modeled post-order in the CFG, as they will
+     * otherwise not dominate their `else` branch.
+     */
+    class OrGuard extends Guard {
+      /** Gets the left operand of this disjunction. */
+      Guard getLeftOperand();
+
+      /** Gets the right operand of this disjunction. */
+      Guard getRightOperand();
     }
 
     /** Holds if `guard` controls block `bb` upon evaluating to `branch`. */
@@ -1641,6 +1768,24 @@ module Make<LocationSig Location, InputSig<Location> Input> {
       pragma[nomagic]
       private predicate guardChecksSsaDef(DfInput::Guard g, Definition def, boolean branch) {
         guardChecks(g, DfInput::getARead(def), branch)
+        or
+        exists(boolean branchLeft, boolean branchRight |
+          // Automatically lift to conjunctions
+          g =
+            any(DfInput::AndGuard ag |
+              guardChecksSsaDef(ag.getLeftOperand(), def, branchLeft) and
+              guardChecksSsaDef(ag.getRightOperand(), def, branchRight) and
+              branch = branchLeft.booleanOr(branchRight)
+            )
+          or
+          // Automatically lift to disjunctions
+          g =
+            any(DfInput::OrGuard og |
+              guardChecksSsaDef(og.getLeftOperand(), def, branchLeft) and
+              guardChecksSsaDef(og.getRightOperand(), def, branchRight) and
+              branch = branchLeft.booleanAnd(branchRight)
+            )
+        )
       }
 
       /** Gets a node that is safely guarded by the given guard check. */