@@ -734,15 +734,15 @@ private predicate variableReadPseudo(ControlFlow::BasicBlock bb, int i, Ssa::Sou
734734}
735735
736736pragma [ noinline]
737- private predicate adjacentDefRead (
737+ deprecated private predicate adjacentDefRead (
738738 Definition def , SsaInput:: BasicBlock bb1 , int i1 , SsaInput:: BasicBlock bb2 , int i2 ,
739739 SsaInput:: SourceVariable v
740740) {
741741 Impl:: adjacentDefRead ( def , bb1 , i1 , bb2 , i2 ) and
742742 v = def .getSourceVariable ( )
743743}
744744
745- private predicate adjacentDefReachesRead (
745+ deprecated private predicate adjacentDefReachesRead (
746746 Definition def , SsaInput:: SourceVariable v , SsaInput:: BasicBlock bb1 , int i1 ,
747747 SsaInput:: BasicBlock bb2 , int i2
748748) {
@@ -760,18 +760,7 @@ private predicate adjacentDefReachesRead(
760760 )
761761}
762762
763- /** Same as `adjacentDefRead`, but skips uncertain reads. */
764- pragma [ nomagic]
765- private predicate adjacentDefSkipUncertainReads (
766- Definition def , SsaInput:: BasicBlock bb1 , int i1 , SsaInput:: BasicBlock bb2 , int i2
767- ) {
768- exists ( SsaInput:: SourceVariable v |
769- adjacentDefReachesRead ( def , v , bb1 , i1 , bb2 , i2 ) and
770- SsaInput:: variableRead ( bb2 , i2 , v , true )
771- )
772- }
773-
774- private predicate adjacentDefReachesUncertainRead (
763+ deprecated private predicate adjacentDefReachesUncertainRead (
775764 Definition def , SsaInput:: BasicBlock bb1 , int i1 , SsaInput:: BasicBlock bb2 , int i2
776765) {
777766 exists ( SsaInput:: SourceVariable v |
@@ -933,10 +922,8 @@ private module Cached {
933922 */
934923 cached
935924 predicate firstReadSameVar ( Definition def , ControlFlow:: Node cfn ) {
936- exists ( ControlFlow:: BasicBlock bb1 , int i1 , ControlFlow:: BasicBlock bb2 , int i2 |
937- def .definesAt ( _, bb1 , i1 ) and
938- adjacentDefSkipUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
939- cfn = bb2 .getNode ( i2 )
925+ exists ( ControlFlow:: BasicBlock bb , int i |
926+ Impl:: firstUse ( def , bb , i , true ) and cfn = bb .getNode ( i )
940927 )
941928 }
942929
@@ -947,25 +934,17 @@ private module Cached {
947934 */
948935 cached
949936 predicate adjacentReadPairSameVar ( Definition def , ControlFlow:: Node cfn1 , ControlFlow:: Node cfn2 ) {
950- exists ( ControlFlow:: BasicBlock bb1 , int i1 , ControlFlow:: BasicBlock bb2 , int i2 |
937+ exists (
938+ ControlFlow:: BasicBlock bb1 , int i1 , ControlFlow:: BasicBlock bb2 , int i2 ,
939+ Ssa:: SourceVariable v
940+ |
941+ Impl:: ssaDefReachesRead ( v , def , bb1 , i1 ) and
942+ Impl:: adjacentUseUse ( bb1 , i1 , bb2 , i2 , v , true ) and
951943 cfn1 = bb1 .getNode ( i1 ) and
952- variableReadActual ( bb1 , i1 , _) and
953- adjacentDefSkipUncertainReads ( def , bb1 , i1 , bb2 , i2 ) and
954944 cfn2 = bb2 .getNode ( i2 )
955945 )
956946 }
957947
958- cached
959- predicate lastRefBeforeRedef ( Definition def , ControlFlow:: BasicBlock bb , int i , Definition next ) {
960- Impl:: lastRefRedef ( def , bb , i , next ) and
961- not SsaInput:: variableRead ( bb , i , def .getSourceVariable ( ) , false )
962- or
963- exists ( SsaInput:: BasicBlock bb0 , int i0 |
964- Impl:: lastRefRedef ( def , bb0 , i0 , next ) and
965- adjacentDefReachesUncertainRead ( def , bb , i , bb0 , i0 )
966- )
967- }
968-
969948 cached
970949 Definition uncertainWriteDefinitionInput ( UncertainWriteDefinition def ) {
971950 Impl:: uncertainWriteDefinitionInput ( def , result )
0 commit comments