C++: Flow through uncertain writes.

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

@@ -718,7 +718,7 @@ class UninitializedNode extends Node {
   UninitializedNode() {
     exists(Ssa::Def def |
       def.getValue().asInstruction() instanceof UninitializedInstruction and
-      Ssa::nodeToDefOrUse(this, def) and
+      Ssa::nodeToDefOrUse(this, def, _) and
       v = def.getSourceVariable().getBaseVariable().(Ssa::BaseIRVariable).getIRVariable().getAst()
     )
   }

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

@@ -291,10 +291,13 @@ predicate outNodeHasAddressAndIndex(
   out.getIndirectionIndex() = indirectionIndex
 }
 
-private predicate defToNode(Node nodeFrom, Def def) {
-  nodeHasOperand(nodeFrom, def.getValue().asOperand(), def.getIndirectionIndex())
-  or
-  nodeHasInstruction(nodeFrom, def.getValue().asInstruction(), def.getIndirectionIndex())
+private predicate defToNode(Node nodeFrom, Def def, boolean uncertain) {
+  (
+    nodeHasOperand(nodeFrom, def.getValue().asOperand(), def.getIndirectionIndex())
+    or
+    nodeHasInstruction(nodeFrom, def.getValue().asInstruction(), def.getIndirectionIndex())
+  ) and
+  if def.isCertain() then uncertain = false else uncertain = true
 }
 
 /**
@@ -302,12 +305,13 @@ private predicate defToNode(Node nodeFrom, Def def) {
  *
  * Holds if `nodeFrom` is the node that correspond to the definition or use `defOrUse`.
  */
-predicate nodeToDefOrUse(Node nodeFrom, SsaDefOrUse defOrUse) {
+predicate nodeToDefOrUse(Node nodeFrom, SsaDefOrUse defOrUse, boolean uncertain) {
   // Node -> Def
-  defToNode(nodeFrom, defOrUse)
+  defToNode(nodeFrom, defOrUse, uncertain)
   or
   // Node -> Use
-  useToNode(defOrUse, nodeFrom)
+  useToNode(defOrUse, nodeFrom) and
+  uncertain = false
 }
 
 /**
@@ -316,7 +320,7 @@ predicate nodeToDefOrUse(Node nodeFrom, SsaDefOrUse defOrUse) {
  */
 private predicate indirectConversionFlowStep(Node nFrom, Node nTo) {
   not exists(UseOrPhi defOrUse |
-    nodeToDefOrUse(nTo, defOrUse) and
+    nodeToDefOrUse(nTo, defOrUse, _) and
     adjacentDefRead(defOrUse, _)
   ) and
   exists(Operand op1, Operand op2, int indirectionIndex, Instruction instr |
@@ -342,31 +346,60 @@ private predicate indirectConversionFlowStep(Node nFrom, Node nTo) {
  * So this predicate recurses back along conversions and `PointerArithmeticInstruction`s to find the
  * first use that has provides use-use flow, and uses that target as the target of the `nodeFrom`.
  */
-private predicate adjustForPointerArith(Node nodeFrom, UseOrPhi use) {
+private predicate adjustForPointerArith(Node nodeFrom, UseOrPhi use, boolean uncertain) {
   nodeFrom = any(PostUpdateNode pun).getPreUpdateNode() and
   exists(DefOrUse defOrUse, Node adjusted |
     indirectConversionFlowStep*(adjusted, nodeFrom) and
-    nodeToDefOrUse(adjusted, defOrUse) and
+    nodeToDefOrUse(adjusted, defOrUse, uncertain) and
     adjacentDefRead(defOrUse, use)
   )
 }
 
-/** Holds if there is def-use or use-use flow from `nodeFrom` to `nodeTo`. */
-predicate ssaFlow(Node nodeFrom, Node nodeTo) {
+private predicate ssaFlowImpl(Node nodeFrom, Node nodeTo, boolean uncertain) {
   // `nodeFrom = any(PostUpdateNode pun).getPreUpdateNode()` is implied by adjustedForPointerArith.
   exists(UseOrPhi use |
-    adjustForPointerArith(nodeFrom, use) and
+    adjustForPointerArith(nodeFrom, use, uncertain) and
     useToNode(use, nodeTo)
   )
   or
   not nodeFrom = any(PostUpdateNode pun).getPreUpdateNode() and
   exists(DefOrUse defOrUse1, UseOrPhi use |
-    nodeToDefOrUse(nodeFrom, defOrUse1) and
+    nodeToDefOrUse(nodeFrom, defOrUse1, uncertain) and
     adjacentDefRead(defOrUse1, use) and
     useToNode(use, nodeTo)
   )
 }
 
+/**
+ * Holds if `def` is the corresponding definition of
+ * the SSA library's `definition`.
+ */
+private predicate ssaDefinition(Def def, Definition definition) {
+  exists(IRBlock block, int i, SourceVariable sv |
+    def.hasIndexInBlock(block, i, sv) and
+    definition.definesAt(sv, block, i)
+  )
+}
+
+/** Gets a node that represents the prior definition of `node`. */
+private Node getAPriorDefinition(Node node) {
+  exists(Def def, Definition definition, Definition inp, Def input |
+    defToNode(node, def, true) and
+    ssaDefinition(def, definition) and
+    uncertainWriteDefinitionInput(pragma[only_bind_into](definition), pragma[only_bind_into](inp)) and
+    ssaDefinition(input, inp) and
+    defToNode(result, input, _)
+  )
+}
+
+/** Holds if there is def-use or use-use flow from `nodeFrom` to `nodeTo`. */
+predicate ssaFlow(Node nodeFrom, Node nodeTo) {
+  exists(Node nFrom, boolean uncertain |
+    ssaFlowImpl(nFrom, nodeTo, uncertain) and
+    if uncertain = true then nodeFrom = [nFrom, getAPriorDefinition(nFrom)] else nodeFrom = nFrom
+  )
+}
+
 /**
  * Holds if `use` is a use of `sv` and is a next adjacent use of `phi` in
  * index `i1` in basic block `bb1`.
@@ -460,6 +493,11 @@ module SsaCached {
   predicate lastRefRedef(Definition def, IRBlock bb, int i, Definition next) {
     SsaImpl::lastRefRedef(def, bb, i, next)
   }
+
+  cached
+  predicate uncertainWriteDefinitionInput(SsaImpl::UncertainWriteDefinition def, Definition inp) {
+    SsaImpl::uncertainWriteDefinitionInput(def, inp)
+  }
 }
 
 cached
@@ -498,6 +536,10 @@ class DefOrUse extends TDefOrUse, SsaDefOrUse {
   final SourceVariable getSourceVariable() { result = defOrUse.getSourceVariable() }
 
   override string toString() { result = defOrUse.toString() }
+
+  predicate hasIndexInBlock(IRBlock block, int index, SourceVariable sv) {
+    defOrUse.hasIndexInBlock(block, index, sv)
+  }
 }
 
 class Phi extends TPhi, SsaDefOrUse {
@@ -541,6 +583,8 @@ class Def extends DefOrUse {
   }
 
   Node0Impl getValue() { result = defOrUse.getValue() }
+
+  predicate isCertain() { defOrUse.isCertain() }
 }
 
 private module SsaImpl = SsaImplCommon::Make<SsaInput>;
@@ -549,4 +593,6 @@ class PhiNode = SsaImpl::PhiNode;
 
 class Definition = SsaImpl::Definition;
 
+class UncertainWriteDefinition = SsaImpl::UncertainWriteDefinition;
+
 import SsaCached

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

@@ -428,9 +428,12 @@ private module Cached {
     boolean certain, Node0Impl value, Operand address, BaseSourceVariableInstruction base, int ind,
     int indirectionIndex
   ) {
-    exists(int ind0, CppType type, int lower, int upper |
-      isWrite(value, address, certain) and
-      isDefImpl(address, base, ind0) and
+    exists(
+      boolean 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
@@ -439,6 +442,16 @@ private module Cached {
     )
   }
 
+  /**
+   * Holds if the address computed by `operand` is guarenteed to write
+   * to a specific address.
+   */
+  private predicate isCertainAddress(Operand operand) {
+    operand.getDef() instanceof VariableAddressInstruction
+    or
+    operand.getType() instanceof Cpp::ReferenceType
+  }
+
   /**
    * Holds if `address` is a use of an SSA variable rooted at `base`, and the
    * path from `base` to `address` passes through `ind` load-like instructions.
@@ -446,27 +459,30 @@ private module Cached {
    * Note: Unlike `isUseImpl`, this predicate recurses through pointer-arithmetic
    * instructions.
    */
-  private predicate isDefImpl(Operand address, BaseSourceVariableInstruction base, int ind) {
+  private predicate isDefImpl(
+    Operand operand, BaseSourceVariableInstruction base, int ind, boolean certain
+  ) {
     DataFlowImplCommon::forceCachingInSameStage() and
     ind = 0 and
-    address = base.getAUse()
+    operand = base.getAUse() and
+    (if isCertainAddress(operand) then certain = true else certain = false)
     or
-    exists(Operand mid, Instruction instr |
-      isDefImpl(mid, base, ind) and
-      instr = address.getDef() and
-      conversionFlow(mid, instr, _)
+    exists(Operand mid, Instruction instr, boolean certain0, boolean isPointerArith |
+      isDefImpl(mid, base, ind, certain0) and
+      instr = operand.getDef() and
+      conversionFlow(mid, instr, isPointerArith) and
+      if isPointerArith = true then certain = false else certain = certain0
     )
     or
-    exists(int ind0 |
-      exists(Operand operand |
-        isDereference(address.getDef(), operand) and
-        isDefImpl(operand, base, ind - 1)
-      )
-      or
-      isDefImpl(address.getDef().(InitializeParameterInstruction).getAnOperand(), base, ind0)
+    exists(Operand address, boolean certain0 |
+      isDereference(operand.getDef(), address) and
+      isDefImpl(address, base, ind - 1, certain0)
     |
-      ind0 = ind - 1
+      if isCertainAddress(operand) then certain = certain0 else certain = false
     )
+    or
+    isDefImpl(operand.getDef().(InitializeParameterInstruction).getAnOperand(), base, ind - 1, _) and
+    certain = true
   }
 }
 

cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/ssa0/SsaInternals.qll

@@ -32,7 +32,7 @@ private newtype TDefOrUseImpl =
   TDefImpl(Operand address) { isDef(_, _, address, _, _, _) } or
   TUseImpl(Operand operand) {
     isUse(_, operand, _, _, _) and
-    not isDef(_, _, operand, _, _, _)
+    not isDef(true, _, operand, _, _, _)
   }
 
 abstract private class DefOrUseImpl extends TDefOrUseImpl {