@@ -936,6 +936,77 @@ private module Cached {
936
936
ValueNumber getUnary ( ) { result .getAnInstruction ( ) = instr .getUnary ( ) }
937
937
}
938
938
939
+ signature predicate sinkSig ( Instruction instr ) ;
940
+
941
+ private module BooleanInstruction< sinkSig / 1 isSink> {
942
+ /**
943
+ * Holds if `i1` flows to `i2` in a single step and `i2` is not an
944
+ * instruction that produces a value of Boolean type.
945
+ */
946
+ private predicate stepToNonBoolean ( Instruction i1 , Instruction i2 ) {
947
+ not i2 .getResultIRType ( ) instanceof IRBooleanType and
948
+ (
949
+ i2 .( CopyInstruction ) .getSourceValue ( ) = i1
950
+ or
951
+ i2 .( ConvertInstruction ) .getUnary ( ) = i1
952
+ or
953
+ i2 .( BuiltinExpectCallInstruction ) .getArgument ( 0 ) = i1
954
+ )
955
+ }
956
+
957
+ private predicate rev ( Instruction instr ) {
958
+ isSink ( instr )
959
+ or
960
+ exists ( Instruction instr1 |
961
+ rev ( instr1 ) and
962
+ stepToNonBoolean ( instr , instr1 )
963
+ )
964
+ }
965
+
966
+ private predicate hasBooleanType ( Instruction instr ) {
967
+ instr .getResultIRType ( ) instanceof IRBooleanType
968
+ }
969
+
970
+ private predicate fwd ( Instruction instr ) {
971
+ rev ( instr ) and
972
+ (
973
+ hasBooleanType ( instr )
974
+ or
975
+ exists ( Instruction instr0 |
976
+ fwd ( instr0 ) and
977
+ stepToNonBoolean ( instr0 , instr )
978
+ )
979
+ )
980
+ }
981
+
982
+ private predicate prunedStep ( Instruction i1 , Instruction i2 ) {
983
+ fwd ( i1 ) and
984
+ fwd ( i2 ) and
985
+ stepToNonBoolean ( i1 , i2 )
986
+ }
987
+
988
+ private predicate stepsPlus ( Instruction i1 , Instruction i2 ) =
989
+ doublyBoundedFastTC( prunedStep / 2 , hasBooleanType / 1 , isSink / 1 ) ( i1 , i2 )
990
+
991
+ /**
992
+ * Gets the Boolean-typed instruction that defines `instr` before any
993
+ * integer conversions are applied, if any.
994
+ */
995
+ Instruction get ( Instruction instr ) {
996
+ isSink ( instr ) and
997
+ (
998
+ result = instr
999
+ or
1000
+ stepsPlus ( result , instr )
1001
+ ) and
1002
+ hasBooleanType ( result )
1003
+ }
1004
+ }
1005
+
1006
+ private predicate isUnaryComparesEqLeft ( Instruction instr ) {
1007
+ unary_compares_eq ( _, instr .getAUse ( ) , 0 , _, _)
1008
+ }
1009
+
939
1010
/**
940
1011
* Holds if `left == right + k` is `areEqual` given that test is `testIsTrue`.
941
1012
*
@@ -971,7 +1042,8 @@ private module Cached {
971
1042
// 1. test = value -> int(l) = 0 is !bv
972
1043
unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
973
1044
// 2. l = bv -> left + right is areEqual
974
- compares_eq ( valueNumberOfOperand ( l ) , left , right , k , areEqual , bv )
1045
+ compares_eq ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) , left ,
1046
+ right , k , areEqual , bv )
975
1047
// We want this to hold:
976
1048
// `test = value -> left + right is areEqual`
977
1049
// Applying 2 we need to show:
@@ -1021,7 +1093,8 @@ private module Cached {
1021
1093
// See argument for why this is correct in compares_eq
1022
1094
exists ( Operand l , BooleanValue bv |
1023
1095
unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
1024
- unary_compares_eq ( valueNumberOfOperand ( l ) , op , k , areEqual , bv )
1096
+ unary_compares_eq ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) ,
1097
+ op , k , areEqual , bv )
1025
1098
)
1026
1099
or
1027
1100
unary_compares_eq ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , op , k , areEqual , value )
@@ -1119,17 +1192,17 @@ private module Cached {
1119
1192
)
1120
1193
}
1121
1194
1195
+ private predicate isBuiltInExpectArg ( Instruction instr ) {
1196
+ instr = any ( BuiltinExpectCallInstruction buildinExpect ) .getArgument ( 0 )
1197
+ }
1198
+
1122
1199
/** A call to the builtin operation `__builtin_expect`. */
1123
1200
private class BuiltinExpectCallInstruction extends CallInstruction {
1124
1201
BuiltinExpectCallInstruction ( ) { this .getStaticCallTarget ( ) .hasName ( "__builtin_expect" ) }
1125
1202
1126
1203
/** Gets the condition of this call. */
1127
- Instruction getCondition ( ) { result = this .getConditionOperand ( ) .getDef ( ) }
1128
-
1129
- Operand getConditionOperand ( ) {
1130
- // The first parameter of `__builtin_expect` has type `long`. So we skip
1131
- // the conversion when inferring guards.
1132
- result = this .getArgument ( 0 ) .( ConvertInstruction ) .getUnaryOperand ( )
1204
+ Instruction getCondition ( ) {
1205
+ result = BooleanInstruction< isBuiltInExpectArg / 1 > :: get ( this .getArgument ( 0 ) )
1133
1206
}
1134
1207
}
1135
1208
@@ -1222,7 +1295,8 @@ private module Cached {
1222
1295
// See argument for why this is correct in compares_eq
1223
1296
exists ( Operand l , BooleanValue bv |
1224
1297
unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
1225
- compares_lt ( valueNumberOfOperand ( l ) , left , right , k , isLt , bv )
1298
+ compares_lt ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) , left ,
1299
+ right , k , isLt , bv )
1226
1300
)
1227
1301
}
1228
1302
@@ -1247,7 +1321,8 @@ private module Cached {
1247
1321
// See argument for why this is correct in compares_eq
1248
1322
exists ( Operand l , BooleanValue bv |
1249
1323
unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
1250
- compares_lt ( valueNumberOfOperand ( l ) , op , k , isLt , bv )
1324
+ compares_lt ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) , op , k ,
1325
+ isLt , bv )
1251
1326
)
1252
1327
}
1253
1328
0 commit comments