@@ -573,7 +573,7 @@ module Make<InputSig Input> {
573
573
private import SsaDefReaches
574
574
575
575
pragma [ nomagic]
576
- predicate liveThrough ( BasicBlock bb , SourceVariable v ) {
576
+ private predicate liveThrough ( BasicBlock bb , SourceVariable v ) {
577
577
liveAtExit ( bb , v ) and
578
578
not ssaRef ( bb , _, v , SsaDef ( ) )
579
579
}
@@ -847,29 +847,35 @@ module Make<InputSig Input> {
847
847
// TODO: Make these `query` predicates once class signatures are supported
848
848
// (`SourceVariable` and `BasicBlock` must have `toString`)
849
849
module Consistency {
850
+ /** A definition that is relevant for the consistency queries. */
850
851
abstract class RelevantDefinition extends Definition {
852
+ /** Override this predicate to ensure locations in consistency results. */
851
853
abstract predicate hasLocationInfo (
852
854
string filepath , int startline , int startcolumn , int endline , int endcolumn
853
855
) ;
854
856
}
855
857
858
+ /** Holds if a read can be reached from multiple definitions. */
856
859
predicate nonUniqueDef ( RelevantDefinition def , SourceVariable v , BasicBlock bb , int i ) {
857
860
ssaDefReachesRead ( v , def , bb , i ) and
858
861
not exists ( unique( Definition def0 | ssaDefReachesRead ( v , def0 , bb , i ) ) )
859
862
}
860
863
864
+ /** Holds if a read cannot be reached from a definition. */
861
865
predicate readWithoutDef ( SourceVariable v , BasicBlock bb , int i ) {
862
866
variableRead ( bb , i , v , _) and
863
867
not ssaDefReachesRead ( v , _, bb , i )
864
868
}
865
869
870
+ /** Holds if a definition cannot reach a read. */
866
871
predicate deadDef ( RelevantDefinition def , SourceVariable v ) {
867
872
v = def .getSourceVariable ( ) and
868
873
not ssaDefReachesRead ( _, def , _, _) and
869
874
not phiHasInputFromBlock ( _, def , _) and
870
875
not uncertainWriteDefinitionInput ( _, def )
871
876
}
872
877
878
+ /** Holds if a read is not dominated by a definition. */
873
879
predicate notDominatedByDef ( RelevantDefinition def , SourceVariable v , BasicBlock bb , int i ) {
874
880
exists ( BasicBlock bbDef , int iDef | def .definesAt ( v , bbDef , iDef ) |
875
881
ssaDefReachesReadWithinBlock ( v , def , bb , i ) and
0 commit comments