From ce19972aeff42c93b9594897831e1d7b99b4dc8c Mon Sep 17 00:00:00 2001 From: Anders Schack-Mulligen Date: Thu, 3 Apr 2025 16:16:20 +0200 Subject: [PATCH] SSA: Reinstate consistency check. --- shared/ssa/codeql/ssa/Ssa.qll | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/shared/ssa/codeql/ssa/Ssa.qll b/shared/ssa/codeql/ssa/Ssa.qll index dab99df65b4..5a18d128ab6 100644 --- a/shared/ssa/codeql/ssa/Ssa.qll +++ b/shared/ssa/codeql/ssa/Ssa.qll @@ -1408,6 +1408,18 @@ module Make Input> { not uncertainWriteDefinitionInput(_, def) } + /** Holds if a read is not dominated by a definition. */ + query predicate notDominatedByDef(Definition def, SourceVariable v, BasicBlock bb, int i) { + exists(BasicBlock bbDef, int iDef | def.definesAt(v, bbDef, iDef) | + SsaDefReachesNew::ssaDefReachesReadWithinBlock(v, def, bb, i) and + (bb != bbDef or i < iDef) + or + ssaDefReachesRead(v, def, bb, i) and + not SsaDefReachesNew::ssaDefReachesReadWithinBlock(v, def, bb, i) and + not def.definesAt(v, getImmediateBasicBlockDominator*(bb), _) + ) + } + /** Holds if the end of a basic block can be reached by multiple definitions. */ query predicate nonUniqueDefReachesEndOfBlock(Definition def, SourceVariable v, BasicBlock bb) { ssaDefReachesEndOfBlock(bb, def, v) and