hohn/codeql
1
0
Fork 0
mirror of https://github.com/github/codeql.git synced 2025-12-17 01:03:14 +01:00
Code Issues Packages Projects Releases Wiki Activity

SSA: Reinstate consistency check.

Browse Source
This commit is contained in:
Anders Schack-Mulligen
2025-04-03 16:16:20 +02:00
parent 6ac4cb71cb
commit ce19972aef
1 changed files with 12 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
shared/ssa/codeql/ssa/Ssa.qll
View File

@@ -1408,6 +1408,18 @@ module Make<LocationSig Location, InputSig<Location> Input> {
not uncertainWriteDefinitionInput(_, def) 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. */ /** Holds if the end of a basic block can be reached by multiple definitions. */
query predicate nonUniqueDefReachesEndOfBlock(Definition def, SourceVariable v, BasicBlock bb) { query predicate nonUniqueDefReachesEndOfBlock(Definition def, SourceVariable v, BasicBlock bb) {
ssaDefReachesEndOfBlock(bb, def, v) and ssaDefReachesEndOfBlock(bb, def, v) and