From 71ae0909d8dd039e55bf2711dfb7f4f6c031bfcd Mon Sep 17 00:00:00 2001
From: Anders Schack-Mulligen <aschackmull@github.com>
Date: Thu, 27 Apr 2023 14:32:12 +0200
Subject: [PATCH] Dataflow: Enforce type pruning in all forward stages.

---
 .../cpp/dataflow/internal/DataFlowImpl.qll    | 36 +++++++++++--------
 .../cpp/ir/dataflow/internal/DataFlowImpl.qll | 36 +++++++++++--------
 .../csharp/dataflow/internal/DataFlowImpl.qll | 36 +++++++++++--------
 .../go/dataflow/internal/DataFlowImpl.qll     | 36 +++++++++++--------
 .../java/dataflow/internal/DataFlowImpl.qll   | 36 +++++++++++--------
 .../dataflow/new/internal/DataFlowImpl.qll    | 36 +++++++++++--------
 .../ruby/dataflow/internal/DataFlowImpl.qll   | 36 +++++++++++--------
 .../swift/dataflow/internal/DataFlowImpl.qll  | 36 +++++++++++--------
 8 files changed, 168 insertions(+), 120 deletions(-)

diff --git a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll
index 2c29bc5c311..ddf98ac0f2f 100644
--- a/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll
+++ b/cpp/ql/lib/semmle/code/cpp/dataflow/internal/DataFlowImpl.qll
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
 
   private import LocalFlowBigStep
 
+  pragma[nomagic]
+  private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
+
   private module Stage3Param implements MkStage<Stage2>::StageParam {
     private module PrevStage = Stage2;
 
@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
     }
 
     bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
+    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      exists(state) and
+      exists(ap)
+    }
 
-    // Type checking is not necessary here as it has already been done in stage 3.
     bindingset[typ, contentType]
-    predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
+    predicate typecheckStore(Typ typ, DataFlowType contentType) {
+      compatibleTypes(typ, contentType)
+    }
   }
 
   private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
       or
       // ... or a step from an existing PathNode to another node.
       pathStep(_, node, state, cc, sc, t, ap) and
-      Stage5::revFlow(node, state, ap.getApprox())
+      Stage5::revFlow(node, state, ap.getApprox()) and
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
     } or
     TPathNodeSink(NodeEx node, FlowState state) {
       exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
     PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
     DataFlowType t, CallContext cc
   ) {
-    t0 = mid.getType() and
-    ap0 = mid.getAp() and
-    Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
-    state = mid.getState() and
-    cc = mid.getCallContext()
+    exists(DataFlowType contentType |
+      t0 = mid.getType() and
+      ap0 = mid.getAp() and
+      Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
+      state = mid.getState() and
+      cc = mid.getCallContext() and
+      compatibleTypes(t0, contentType)
+    )
   }
 
   private predicate pathOutOfCallable0(
diff --git a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll
index 2c29bc5c311..ddf98ac0f2f 100644
--- a/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll
+++ b/cpp/ql/lib/semmle/code/cpp/ir/dataflow/internal/DataFlowImpl.qll
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
 
   private import LocalFlowBigStep
 
+  pragma[nomagic]
+  private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
+
   private module Stage3Param implements MkStage<Stage2>::StageParam {
     private module PrevStage = Stage2;
 
@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
     }
 
     bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
+    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      exists(state) and
+      exists(ap)
+    }
 
-    // Type checking is not necessary here as it has already been done in stage 3.
     bindingset[typ, contentType]
-    predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
+    predicate typecheckStore(Typ typ, DataFlowType contentType) {
+      compatibleTypes(typ, contentType)
+    }
   }
 
   private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
       or
       // ... or a step from an existing PathNode to another node.
       pathStep(_, node, state, cc, sc, t, ap) and
-      Stage5::revFlow(node, state, ap.getApprox())
+      Stage5::revFlow(node, state, ap.getApprox()) and
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
     } or
     TPathNodeSink(NodeEx node, FlowState state) {
       exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
     PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
     DataFlowType t, CallContext cc
   ) {
-    t0 = mid.getType() and
-    ap0 = mid.getAp() and
-    Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
-    state = mid.getState() and
-    cc = mid.getCallContext()
+    exists(DataFlowType contentType |
+      t0 = mid.getType() and
+      ap0 = mid.getAp() and
+      Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
+      state = mid.getState() and
+      cc = mid.getCallContext() and
+      compatibleTypes(t0, contentType)
+    )
   }
 
   private predicate pathOutOfCallable0(
diff --git a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll
index 2c29bc5c311..ddf98ac0f2f 100644
--- a/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll
+++ b/csharp/ql/lib/semmle/code/csharp/dataflow/internal/DataFlowImpl.qll
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
 
   private import LocalFlowBigStep
 
+  pragma[nomagic]
+  private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
+
   private module Stage3Param implements MkStage<Stage2>::StageParam {
     private module PrevStage = Stage2;
 
@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
     }
 
     bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
+    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      exists(state) and
+      exists(ap)
+    }
 
-    // Type checking is not necessary here as it has already been done in stage 3.
     bindingset[typ, contentType]
-    predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
+    predicate typecheckStore(Typ typ, DataFlowType contentType) {
+      compatibleTypes(typ, contentType)
+    }
   }
 
   private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
       or
       // ... or a step from an existing PathNode to another node.
       pathStep(_, node, state, cc, sc, t, ap) and
-      Stage5::revFlow(node, state, ap.getApprox())
+      Stage5::revFlow(node, state, ap.getApprox()) and
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
     } or
     TPathNodeSink(NodeEx node, FlowState state) {
       exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
     PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
     DataFlowType t, CallContext cc
   ) {
-    t0 = mid.getType() and
-    ap0 = mid.getAp() and
-    Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
-    state = mid.getState() and
-    cc = mid.getCallContext()
+    exists(DataFlowType contentType |
+      t0 = mid.getType() and
+      ap0 = mid.getAp() and
+      Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
+      state = mid.getState() and
+      cc = mid.getCallContext() and
+      compatibleTypes(t0, contentType)
+    )
   }
 
   private predicate pathOutOfCallable0(
diff --git a/go/ql/lib/semmle/go/dataflow/internal/DataFlowImpl.qll b/go/ql/lib/semmle/go/dataflow/internal/DataFlowImpl.qll
index 2c29bc5c311..ddf98ac0f2f 100644
--- a/go/ql/lib/semmle/go/dataflow/internal/DataFlowImpl.qll
+++ b/go/ql/lib/semmle/go/dataflow/internal/DataFlowImpl.qll
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
 
   private import LocalFlowBigStep
 
+  pragma[nomagic]
+  private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
+
   private module Stage3Param implements MkStage<Stage2>::StageParam {
     private module PrevStage = Stage2;
 
@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
     }
 
     bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
+    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      exists(state) and
+      exists(ap)
+    }
 
-    // Type checking is not necessary here as it has already been done in stage 3.
     bindingset[typ, contentType]
-    predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
+    predicate typecheckStore(Typ typ, DataFlowType contentType) {
+      compatibleTypes(typ, contentType)
+    }
   }
 
   private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
       or
       // ... or a step from an existing PathNode to another node.
       pathStep(_, node, state, cc, sc, t, ap) and
-      Stage5::revFlow(node, state, ap.getApprox())
+      Stage5::revFlow(node, state, ap.getApprox()) and
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
     } or
     TPathNodeSink(NodeEx node, FlowState state) {
       exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
     PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
     DataFlowType t, CallContext cc
   ) {
-    t0 = mid.getType() and
-    ap0 = mid.getAp() and
-    Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
-    state = mid.getState() and
-    cc = mid.getCallContext()
+    exists(DataFlowType contentType |
+      t0 = mid.getType() and
+      ap0 = mid.getAp() and
+      Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
+      state = mid.getState() and
+      cc = mid.getCallContext() and
+      compatibleTypes(t0, contentType)
+    )
   }
 
   private predicate pathOutOfCallable0(
diff --git a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll
index 2c29bc5c311..ddf98ac0f2f 100644
--- a/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll
+++ b/java/ql/lib/semmle/code/java/dataflow/internal/DataFlowImpl.qll
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
 
   private import LocalFlowBigStep
 
+  pragma[nomagic]
+  private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
+
   private module Stage3Param implements MkStage<Stage2>::StageParam {
     private module PrevStage = Stage2;
 
@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
     }
 
     bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
+    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      exists(state) and
+      exists(ap)
+    }
 
-    // Type checking is not necessary here as it has already been done in stage 3.
     bindingset[typ, contentType]
-    predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
+    predicate typecheckStore(Typ typ, DataFlowType contentType) {
+      compatibleTypes(typ, contentType)
+    }
   }
 
   private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
       or
       // ... or a step from an existing PathNode to another node.
       pathStep(_, node, state, cc, sc, t, ap) and
-      Stage5::revFlow(node, state, ap.getApprox())
+      Stage5::revFlow(node, state, ap.getApprox()) and
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
     } or
     TPathNodeSink(NodeEx node, FlowState state) {
       exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
     PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
     DataFlowType t, CallContext cc
   ) {
-    t0 = mid.getType() and
-    ap0 = mid.getAp() and
-    Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
-    state = mid.getState() and
-    cc = mid.getCallContext()
+    exists(DataFlowType contentType |
+      t0 = mid.getType() and
+      ap0 = mid.getAp() and
+      Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
+      state = mid.getState() and
+      cc = mid.getCallContext() and
+      compatibleTypes(t0, contentType)
+    )
   }
 
   private predicate pathOutOfCallable0(
diff --git a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll
index 2c29bc5c311..ddf98ac0f2f 100644
--- a/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll
+++ b/python/ql/lib/semmle/python/dataflow/new/internal/DataFlowImpl.qll
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
 
   private import LocalFlowBigStep
 
+  pragma[nomagic]
+  private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
+
   private module Stage3Param implements MkStage<Stage2>::StageParam {
     private module PrevStage = Stage2;
 
@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
     }
 
     bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
+    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      exists(state) and
+      exists(ap)
+    }
 
-    // Type checking is not necessary here as it has already been done in stage 3.
     bindingset[typ, contentType]
-    predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
+    predicate typecheckStore(Typ typ, DataFlowType contentType) {
+      compatibleTypes(typ, contentType)
+    }
   }
 
   private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
       or
       // ... or a step from an existing PathNode to another node.
       pathStep(_, node, state, cc, sc, t, ap) and
-      Stage5::revFlow(node, state, ap.getApprox())
+      Stage5::revFlow(node, state, ap.getApprox()) and
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
     } or
     TPathNodeSink(NodeEx node, FlowState state) {
       exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
     PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
     DataFlowType t, CallContext cc
   ) {
-    t0 = mid.getType() and
-    ap0 = mid.getAp() and
-    Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
-    state = mid.getState() and
-    cc = mid.getCallContext()
+    exists(DataFlowType contentType |
+      t0 = mid.getType() and
+      ap0 = mid.getAp() and
+      Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
+      state = mid.getState() and
+      cc = mid.getCallContext() and
+      compatibleTypes(t0, contentType)
+    )
   }
 
   private predicate pathOutOfCallable0(
diff --git a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll
index 2c29bc5c311..ddf98ac0f2f 100644
--- a/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll
+++ b/ruby/ql/lib/codeql/ruby/dataflow/internal/DataFlowImpl.qll
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
 
   private import LocalFlowBigStep
 
+  pragma[nomagic]
+  private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
+
   private module Stage3Param implements MkStage<Stage2>::StageParam {
     private module PrevStage = Stage2;
 
@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
     }
 
     bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
+    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      exists(state) and
+      exists(ap)
+    }
 
-    // Type checking is not necessary here as it has already been done in stage 3.
     bindingset[typ, contentType]
-    predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
+    predicate typecheckStore(Typ typ, DataFlowType contentType) {
+      compatibleTypes(typ, contentType)
+    }
   }
 
   private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
       or
       // ... or a step from an existing PathNode to another node.
       pathStep(_, node, state, cc, sc, t, ap) and
-      Stage5::revFlow(node, state, ap.getApprox())
+      Stage5::revFlow(node, state, ap.getApprox()) and
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
     } or
     TPathNodeSink(NodeEx node, FlowState state) {
       exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
     PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
     DataFlowType t, CallContext cc
   ) {
-    t0 = mid.getType() and
-    ap0 = mid.getAp() and
-    Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
-    state = mid.getState() and
-    cc = mid.getCallContext()
+    exists(DataFlowType contentType |
+      t0 = mid.getType() and
+      ap0 = mid.getAp() and
+      Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
+      state = mid.getState() and
+      cc = mid.getCallContext() and
+      compatibleTypes(t0, contentType)
+    )
   }
 
   private predicate pathOutOfCallable0(
diff --git a/swift/ql/lib/codeql/swift/dataflow/internal/DataFlowImpl.qll b/swift/ql/lib/codeql/swift/dataflow/internal/DataFlowImpl.qll
index 2c29bc5c311..ddf98ac0f2f 100644
--- a/swift/ql/lib/codeql/swift/dataflow/internal/DataFlowImpl.qll
+++ b/swift/ql/lib/codeql/swift/dataflow/internal/DataFlowImpl.qll
@@ -2162,6 +2162,9 @@ module Impl<FullStateConfigSig Config> {
 
   private import LocalFlowBigStep
 
+  pragma[nomagic]
+  private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
+
   private module Stage3Param implements MkStage<Stage2>::StageParam {
     private module PrevStage = Stage2;
 
@@ -2215,9 +2218,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2333,9 +2333,6 @@ module Impl<FullStateConfigSig Config> {
       )
     }
 
-    pragma[nomagic]
-    private predicate castingNodeEx(NodeEx node) { node.asNode() instanceof CastingNode }
-
     bindingset[node, state, t, ap]
     predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
       exists(state) and
@@ -2613,11 +2610,16 @@ module Impl<FullStateConfigSig Config> {
     }
 
     bindingset[node, state, t, ap]
-    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) { any() }
+    predicate filter(NodeEx node, FlowState state, Typ t, Ap ap) {
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any()) and
+      exists(state) and
+      exists(ap)
+    }
 
-    // Type checking is not necessary here as it has already been done in stage 3.
     bindingset[typ, contentType]
-    predicate typecheckStore(Typ typ, DataFlowType contentType) { any() }
+    predicate typecheckStore(Typ typ, DataFlowType contentType) {
+      compatibleTypes(typ, contentType)
+    }
   }
 
   private module Stage5 = MkStage<Stage4>::Stage<Stage5Param>;
@@ -2819,7 +2821,8 @@ module Impl<FullStateConfigSig Config> {
       or
       // ... or a step from an existing PathNode to another node.
       pathStep(_, node, state, cc, sc, t, ap) and
-      Stage5::revFlow(node, state, ap.getApprox())
+      Stage5::revFlow(node, state, ap.getApprox()) and
+      (if castingNodeEx(node) then compatibleTypes(node.getDataFlowType(), t) else any())
     } or
     TPathNodeSink(NodeEx node, FlowState state) {
       exists(PathNodeMid sink |
@@ -3418,11 +3421,14 @@ module Impl<FullStateConfigSig Config> {
     PathNodeMid mid, NodeEx node, FlowState state, DataFlowType t0, AccessPath ap0, Content c,
     DataFlowType t, CallContext cc
   ) {
-    t0 = mid.getType() and
-    ap0 = mid.getAp() and
-    Stage5::storeStepCand(mid.getNodeEx(), _, c, node, _, t) and
-    state = mid.getState() and
-    cc = mid.getCallContext()
+    exists(DataFlowType contentType |
+      t0 = mid.getType() and
+      ap0 = mid.getAp() and
+      Stage5::storeStepCand(mid.getNodeEx(), _, c, node, contentType, t) and
+      state = mid.getState() and
+      cc = mid.getCallContext() and
+      compatibleTypes(t0, contentType)
+    )
   }
 
   private predicate pathOutOfCallable0(