@@ -936,6 +936,77 @@ private module Cached {
936936 ValueNumber getUnary ( ) { result .getAnInstruction ( ) = instr .getUnary ( ) }
937937 }
938938
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+
9391010 /**
9401011 * Holds if `left == right + k` is `areEqual` given that test is `testIsTrue`.
9411012 *
@@ -966,14 +1037,19 @@ private module Cached {
9661037 )
9671038 or
9681039 compares_eq ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , left , right , k , areEqual , value )
969- }
970-
971- private predicate isConvertedBool ( Instruction instr ) {
972- instr .getResultIRType ( ) instanceof IRBooleanType
973- or
974- isConvertedBool ( instr .( ConvertInstruction ) .getUnary ( ) )
9751040 or
976- isConvertedBool ( instr .( BuiltinExpectCallInstruction ) .getCondition ( ) )
1041+ exists ( Operand l , BooleanValue bv |
1042+ // 1. test = value -> int(l) = 0 is !bv
1043+ unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
1044+ // 2. l = bv -> left + right is areEqual
1045+ compares_eq ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) , left ,
1046+ right , k , areEqual , bv )
1047+ // We want this to hold:
1048+ // `test = value -> left + right is areEqual`
1049+ // Applying 2 we need to show:
1050+ // `test = value -> l = bv`
1051+ // And `l = bv` holds by `int(l) = 0 is !bv`
1052+ )
9771053 }
9781054
9791055 /**
@@ -1006,19 +1082,11 @@ private module Cached {
10061082 k = k1 + k2
10071083 )
10081084 or
1009- exists ( CompareValueNumber cmp , Operand left , Operand right , AbstractValue v |
1010- test = cmp and
1011- pragma [ only_bind_into ] ( cmp )
1012- .hasOperands ( pragma [ only_bind_into ] ( left ) , pragma [ only_bind_into ] ( right ) ) and
1013- isConvertedBool ( left .getDef ( ) ) and
1014- int_value ( right .getDef ( ) ) = 0 and
1015- unary_compares_eq ( valueNumberOfOperand ( left ) , op , k , areEqual , v )
1016- |
1017- cmp instanceof CompareNEValueNumber and
1018- v = value
1019- or
1020- cmp instanceof CompareEQValueNumber and
1021- v .getDualValue ( ) = value
1085+ // See argument for why this is correct in compares_eq
1086+ exists ( Operand l , BooleanValue bv |
1087+ unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
1088+ unary_compares_eq ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) ,
1089+ op , k , areEqual , bv )
10221090 )
10231091 or
10241092 unary_compares_eq ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , op , k , areEqual , value )
@@ -1116,70 +1184,26 @@ private module Cached {
11161184 )
11171185 }
11181186
1187+ private predicate isBuiltInExpectArg ( Instruction instr ) {
1188+ instr = any ( BuiltinExpectCallInstruction buildinExpect ) .getArgument ( 0 )
1189+ }
1190+
11191191 /** A call to the builtin operation `__builtin_expect`. */
11201192 private class BuiltinExpectCallInstruction extends CallInstruction {
11211193 BuiltinExpectCallInstruction ( ) { this .getStaticCallTarget ( ) .hasName ( "__builtin_expect" ) }
11221194
11231195 /** Gets the condition of this call. */
1124- Instruction getCondition ( ) { result = this .getConditionOperand ( ) .getDef ( ) }
1125-
1126- Operand getConditionOperand ( ) {
1127- // The first parameter of `__builtin_expect` has type `long`. So we skip
1128- // the conversion when inferring guards.
1129- result = this .getArgument ( 0 ) .( ConvertInstruction ) .getUnaryOperand ( )
1196+ Instruction getCondition ( ) {
1197+ result = BooleanInstruction< isBuiltInExpectArg / 1 > :: get ( this .getArgument ( 0 ) )
11301198 }
11311199 }
11321200
1133- /**
1134- * Holds if `left == right + k` is `areEqual` if `cmp` evaluates to `value`,
1135- * and `cmp` is an instruction that compares the value of
1136- * `__builtin_expect(left == right + k, _)` to `0`.
1137- */
1138- private predicate builtin_expect_eq (
1139- CompareValueNumber cmp , Operand left , Operand right , int k , boolean areEqual ,
1140- AbstractValue value
1141- ) {
1142- exists ( BuiltinExpectCallValueNumber call , Instruction const , AbstractValue innerValue |
1143- int_value ( const ) = 0 and
1144- cmp .hasOperands ( call .getAUse ( ) , const .getAUse ( ) ) and
1145- compares_eq ( call .getCondition ( ) , left , right , k , areEqual , innerValue )
1146- |
1147- cmp instanceof CompareNEValueNumber and
1148- value = innerValue
1149- or
1150- cmp instanceof CompareEQValueNumber and
1151- value .getDualValue ( ) = innerValue
1152- )
1153- }
1154-
11551201 private predicate complex_eq (
11561202 ValueNumber cmp , Operand left , Operand right , int k , boolean areEqual , AbstractValue value
11571203 ) {
11581204 sub_eq ( cmp , left , right , k , areEqual , value )
11591205 or
11601206 add_eq ( cmp , left , right , k , areEqual , value )
1161- or
1162- builtin_expect_eq ( cmp , left , right , k , areEqual , value )
1163- }
1164-
1165- /**
1166- * Holds if `op == k` is `areEqual` if `cmp` evaluates to `value`, and `cmp` is
1167- * an instruction that compares the value of `__builtin_expect(op == k, _)` to `0`.
1168- */
1169- private predicate unary_builtin_expect_eq (
1170- CompareValueNumber cmp , Operand op , int k , boolean areEqual , AbstractValue value
1171- ) {
1172- exists ( BuiltinExpectCallValueNumber call , Instruction const , AbstractValue innerValue |
1173- int_value ( const ) = 0 and
1174- cmp .hasOperands ( call .getAUse ( ) , const .getAUse ( ) ) and
1175- unary_compares_eq ( call .getCondition ( ) , op , k , areEqual , innerValue )
1176- |
1177- cmp instanceof CompareNEValueNumber and
1178- value = innerValue
1179- or
1180- cmp instanceof CompareEQValueNumber and
1181- value .getDualValue ( ) = innerValue
1182- )
11831207 }
11841208
11851209 private predicate unary_complex_eq (
@@ -1188,8 +1212,6 @@ private module Cached {
11881212 unary_sub_eq ( test , op , k , areEqual , value )
11891213 or
11901214 unary_add_eq ( test , op , k , areEqual , value )
1191- or
1192- unary_builtin_expect_eq ( test , op , k , areEqual , value )
11931215 }
11941216
11951217 /*
@@ -1215,6 +1237,15 @@ private module Cached {
12151237 exists ( AbstractValue dual | value = dual .getDualValue ( ) |
12161238 compares_lt ( test .( LogicalNotValueNumber ) .getUnary ( ) , left , right , k , isLt , dual )
12171239 )
1240+ or
1241+ compares_lt ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , left , right , k , isLt , value )
1242+ or
1243+ // See argument for why this is correct in compares_eq
1244+ exists ( Operand l , BooleanValue bv |
1245+ unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
1246+ compares_lt ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) , left ,
1247+ right , k , isLt , bv )
1248+ )
12181249 }
12191250
12201251 /** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
@@ -1234,6 +1265,15 @@ private module Cached {
12341265 int_value ( const ) = k1 and
12351266 k = k1 + k2
12361267 )
1268+ or
1269+ compares_lt ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , op , k , isLt , value )
1270+ or
1271+ // See argument for why this is correct in compares_eq
1272+ exists ( Operand l , BooleanValue bv |
1273+ unary_compares_eq ( test , l , 0 , bv .getValue ( ) .booleanNot ( ) , value ) and
1274+ compares_lt ( valueNumber ( BooleanInstruction< isUnaryComparesEqLeft / 1 > :: get ( l .getDef ( ) ) ) , op , k ,
1275+ isLt , bv )
1276+ )
12371277 }
12381278
12391279 /** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */
0 commit comments