C++: Support reasoning about whether a phi node overwrites the entire buffer

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImpl.qll

@@ -136,7 +136,9 @@ private module SourceVariables {
     NormalSourceVariable() { this = TNormalSourceVariable(base, ind) }
 
     final override string toString() {
-      result = repeatStars(this.getIndirection()) + base.toString()
+      if ind = 0
+      then result = "&" + base.toString()
+      else result = repeatStars(this.getIndirection() - 1) + base.toString()
     }
   }
 
@@ -157,7 +159,9 @@ private module SourceVariables {
     }
 
     final override string toString() {
-      result = repeatStars(this.getIndirection()) + base.toString() + " [before crement]"
+      if ind = 0
+      then result = "&" + base.toString() + " [before crement]"
+      else result = repeatStars(this.getIndirection() - 1) + base.toString() + " [before crement]"
     }
 
     /**
@@ -1353,6 +1357,53 @@ class PhiNode extends Definition instanceof SsaImpl::PhiNode {
   final predicate hasInputFromBlock(Definition input, IRBlock bb) {
     phiHasInputFromBlock(this, input, bb)
   }
+
+  override int getIndirection() { result = this.getSourceVariable().getIndirection() }
+
+  override predicate isCertain() {
+    // If this phi node is part of a phi cycle of phi nodes the least
+    // fixed-point semantics of datalog means we don't get the right answer.
+    // So we perform an SCC reduction to simulate greatest fixed-point semantics.
+    getCycle(this).isCertain()
+    or
+    // If there is no cycle we get the right semantics through traditional
+    // recursion.
+    not exists(getCycle(this)) and
+    forex(Definition inp | inp = this.getAnInput() | inp.isCertain())
+  }
+
+  final override Declaration getFunction() {
+    result = SsaImpl::PhiNode.super.getBasicBlock().getEnclosingFunction()
+  }
+}
+
+private PhiNode getAnInput(PhiNode phi) { result = phi.getAnInput() }
+
+private predicate definitionCycle(PhiNode phi) { getAnInput+(phi) = phi }
+
+private predicate hasAnInput(PhiNode phi1, PhiNode phi2) {
+  definitionCycle(phi1) and
+  definitionCycle(phi2) and
+  getAnInput(phi1) = phi2
+}
+
+private module PhiCycleEquivalence = QlBuiltins::EquivalenceRelation<PhiNode, hasAnInput/2>;
+
+private PhiCycle getCycle(PhiNode phi) { result.getAPhiNode() = phi }
+
+private class PhiCycle extends PhiCycleEquivalence::EquivalenceClass {
+  PhiNode getAPhiNode() { PhiCycleEquivalence::getEquivalenceClass(result) = this }
+
+  predicate hasPhiNode(PhiNode phi) { this.getAPhiNode() = phi }
+
+  string toString() { result = strictconcat(this.getAPhiNode().toString(), ", ") }
+
+  predicate isCertain() {
+    // A phi cycle is certain if all of the inputs into the phi cycle is certain.
+    forex(PhiNode phi | phi = this.getAPhiNode() |
+      forall(PhiNode inp | phi.getAnInput() = inp and not this.hasPhiNode(inp) | inp.isCertain())
+    )
+  }
 }
 
 /** An static single assignment (SSA) definition. */

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/SsaImplCommon.qll

@@ -147,7 +147,7 @@ abstract class Indirection extends Type {
    *
    * `certain` is `true` if this write is guaranteed to write to the address.
    */
-  predicate isAdditionalWrite(Node0Impl value, Operand address, boolean certain) { none() }
+  predicate isAdditionalWrite(Node0Impl value, Operand address, Certainty certain) { none() }
 
   /**
    * Gets the base type of this indirection, after specifiers have been deeply
@@ -198,11 +198,11 @@ private module IteratorIndirections {
       baseType = super.getValueType()
     }
 
-    override predicate isAdditionalWrite(Node0Impl value, Operand address, boolean certain) {
+    override predicate isAdditionalWrite(Node0Impl value, Operand address, Certainty certain) {
       exists(CallInstruction call | call.getArgumentOperand(0) = value.asOperand() |
         this = call.getStaticCallTarget().(Function).getClassAndName("operator=") and
         address = call.getThisArgumentOperand() and
-        certain = false
+        certain instanceof AlwaysUncertain
       )
     }
 
@@ -271,30 +271,62 @@ predicate isDereference(Instruction deref, Operand address, boolean additional)
   additional = false
 }
 
-predicate isWrite(Node0Impl value, Operand address, boolean certain) {
+private newtype TCertainty =
+  TCertainWhenAddressIsCertain() or
+  TAlwaysCertain() or
+  TAlwaysUncertain()
+
+abstract private class Certainty extends TCertainty {
+  abstract predicate isCertain(boolean addressIsCertain);
+
+  abstract string toString();
+}
+
+private class CertainWhenAddressIsCertain extends Certainty, TCertainWhenAddressIsCertain {
+  override predicate isCertain(boolean addressIsCertain) { addressIsCertain = true }
+
+  override string toString() { result = "CertainWhenAddressIsCertain" }
+}
+
+private class AlwaysCertain extends Certainty, TAlwaysCertain {
+  override predicate isCertain(boolean addressIsCertain) {
+    addressIsCertain = true or addressIsCertain = false
+  }
+
+  override string toString() { result = "AlwaysCertain" }
+}
+
+private class AlwaysUncertain extends Certainty, TAlwaysUncertain {
+  override predicate isCertain(boolean addressIsCertain) { none() }
+
+  override string toString() { result = "AlwaysUncertain" }
+}
+
+predicate isWrite(Node0Impl value, Operand address, Certainty certain) {
   any(Indirection ind).isAdditionalWrite(value, address, certain)
   or
-  certain = true and
-  (
-    exists(StoreInstruction store |
-      value.asInstruction() = store and
-      address = store.getDestinationAddressOperand()
-    )
-    or
-    exists(InitializeParameterInstruction init |
-      value.asInstruction() = init and
-      address = init.getAnOperand()
-    )
-    or
-    exists(InitializeDynamicAllocationInstruction init |
-      value.asInstruction() = init and
-      address = init.getAllocationAddressOperand()
-    )
-    or
-    exists(UninitializedInstruction uninitialized |
-      value.asInstruction() = uninitialized and
-      address = uninitialized.getAnOperand()
-    )
+  exists(StoreInstruction store |
+    value.asInstruction() = store and
+    address = store.getDestinationAddressOperand() and
+    certain instanceof CertainWhenAddressIsCertain
+  )
+  or
+  exists(InitializeParameterInstruction init |
+    value.asInstruction() = init and
+    address = init.getAnOperand() and
+    certain instanceof AlwaysCertain
+  )
+  or
+  exists(InitializeDynamicAllocationInstruction init |
+    value.asInstruction() = init and
+    address = init.getAllocationAddressOperand() and
+    certain instanceof AlwaysCertain
+  )
+  or
+  exists(UninitializedInstruction uninitialized |
+    value.asInstruction() = uninitialized and
+    address = uninitialized.getAnOperand() and
+    certain instanceof AlwaysCertain
   )
 }
 
@@ -718,16 +750,18 @@ private module Cached {
     int indirectionIndex
   ) {
     exists(
-      boolean writeIsCertain, boolean addressIsCertain, int ind0, CppType type, int lower, int upper
+      Certainty writeIsCertain, boolean addressIsCertain, int ind0, CppType type, int lower,
+      int upper
     |
       isWrite(value, address, writeIsCertain) and
       isDefImpl(address, base, ind0, addressIsCertain) and
-      certain = writeIsCertain.booleanAnd(addressIsCertain) and
       type = getLanguageType(address) and
       upper = countIndirectionsForCppType(type) and
       ind = ind0 + [lower .. upper] and
       indirectionIndex = ind - (ind0 + lower) and
       lower = getMinIndirectionsForType(any(Type t | type.hasUnspecifiedType(t, _)))
+    |
+      if writeIsCertain.isCertain(addressIsCertain) then certain = true else certain = false
     )
   }