@@ -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
*
@@ -966,14 +1037,19 @@ private module Cached {
966
1037
)
967
1038
or
968
1039
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 ( ) )
975
1040
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
+ )
977
1053
}
978
1054
979
1055
/**
@@ -1006,19 +1082,11 @@ private module Cached {
1006
1082
k = k1 + k2
1007
1083
)
1008
1084
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 )
1022
1090
)
1023
1091
or
1024
1092
unary_compares_eq ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , op , k , areEqual , value )
@@ -1116,70 +1184,26 @@ private module Cached {
1116
1184
)
1117
1185
}
1118
1186
1187
+ private predicate isBuiltInExpectArg ( Instruction instr ) {
1188
+ instr = any ( BuiltinExpectCallInstruction buildinExpect ) .getArgument ( 0 )
1189
+ }
1190
+
1119
1191
/** A call to the builtin operation `__builtin_expect`. */
1120
1192
private class BuiltinExpectCallInstruction extends CallInstruction {
1121
1193
BuiltinExpectCallInstruction ( ) { this .getStaticCallTarget ( ) .hasName ( "__builtin_expect" ) }
1122
1194
1123
1195
/** 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 ) )
1130
1198
}
1131
1199
}
1132
1200
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
-
1155
1201
private predicate complex_eq (
1156
1202
ValueNumber cmp , Operand left , Operand right , int k , boolean areEqual , AbstractValue value
1157
1203
) {
1158
1204
sub_eq ( cmp , left , right , k , areEqual , value )
1159
1205
or
1160
1206
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
- )
1183
1207
}
1184
1208
1185
1209
private predicate unary_complex_eq (
@@ -1188,8 +1212,6 @@ private module Cached {
1188
1212
unary_sub_eq ( test , op , k , areEqual , value )
1189
1213
or
1190
1214
unary_add_eq ( test , op , k , areEqual , value )
1191
- or
1192
- unary_builtin_expect_eq ( test , op , k , areEqual , value )
1193
1215
}
1194
1216
1195
1217
/*
@@ -1215,6 +1237,15 @@ private module Cached {
1215
1237
exists ( AbstractValue dual | value = dual .getDualValue ( ) |
1216
1238
compares_lt ( test .( LogicalNotValueNumber ) .getUnary ( ) , left , right , k , isLt , dual )
1217
1239
)
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
+ )
1218
1249
}
1219
1250
1220
1251
/** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
@@ -1234,6 +1265,15 @@ private module Cached {
1234
1265
int_value ( const ) = k1 and
1235
1266
k = k1 + k2
1236
1267
)
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
+ )
1237
1277
}
1238
1278
1239
1279
/** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */
0 commit comments