@@ -936,6 +936,28 @@ private module Cached {
936936 ValueNumber getUnary ( ) { result .getAnInstruction ( ) = instr .getUnary ( ) }
937937 }
938938
939+ private class ConvertValueNumber extends ValueNumber {
940+ ConvertInstruction convert ;
941+
942+ ConvertValueNumber ( ) { convert = this .getAnInstruction ( ) }
943+
944+ ValueNumber getUnary ( ) { result .getAnInstruction ( ) = convert .getUnary ( ) }
945+ }
946+
947+ private class ConvertBoolToIntOrPointerInstruction extends ConvertInstruction {
948+ ConvertBoolToIntOrPointerInstruction ( ) {
949+ this .getUnary ( ) .getResultIRType ( ) instanceof IRBooleanType and
950+ (
951+ this .getResultIRType ( ) instanceof IRIntegerType or
952+ this .getResultIRType ( ) instanceof IRAddressType
953+ )
954+ }
955+ }
956+
957+ private class ConvertBoolToIntOrPointerValueNumber extends ConvertValueNumber {
958+ override ConvertBoolToIntOrPointerInstruction convert ;
959+ }
960+
939961 /**
940962 * Holds if `left == right + k` is `areEqual` given that test is `testIsTrue`.
941963 *
@@ -966,6 +988,26 @@ private module Cached {
966988 )
967989 or
968990 compares_eq ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , left , right , k , areEqual , value )
991+ or
992+ // If we have e.g.:
993+ // ```
994+ // x = (a == b)
995+ // if(x != c) { ... }
996+ // ```
997+ // then `x != c` is true implies that `a == b` is true.
998+ // ```
999+ exists ( Operand l , Operand r , ValueNumber vn , int c , AbstractValue v |
1000+ test .( CompareValueNumber ) .hasOperands ( l , r ) and
1001+ int_value ( r .getDef ( ) ) = c and
1002+ vn .getAnInstruction ( ) = getBooleanInstruction ( l .getDef ( ) ) and
1003+ compares_eq ( vn , left , right , k , areEqual , v )
1004+ |
1005+ test instanceof CompareNEValueNumber and
1006+ if c = 0 then value = v else value = v .getDualValue ( )
1007+ or
1008+ test instanceof CompareEQValueNumber and
1009+ if c = 0 then value = v .getDualValue ( ) else value = v
1010+ )
9691011 }
9701012
9711013 private predicate isConvertedBool ( Instruction instr ) {
@@ -1006,19 +1048,24 @@ private module Cached {
10061048 k = k1 + k2
10071049 )
10081050 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 )
1051+ // If we have e.g.:
1052+ // ```
1053+ // x = (a == 10)
1054+ // if(x != c) { ... }
1055+ // ```
1056+ // then `x != c` is true implies that `a == 10` is true.
1057+ // ```
1058+ exists ( Operand l , Operand r , ValueNumber vn , int c , AbstractValue v |
1059+ test .( CompareValueNumber ) .hasOperands ( l , r ) and
1060+ int_value ( r .getDef ( ) ) = c and
1061+ vn .getAnInstruction ( ) = getBooleanInstruction ( l .getDef ( ) ) and
1062+ compares_lt ( vn , op , k , areEqual , v )
10161063 |
1017- cmp instanceof CompareNEValueNumber and
1018- v = value
1064+ test instanceof CompareNEValueNumber and
1065+ if c = 0 then value = v else value = v . getDualValue ( )
10191066 or
1020- cmp instanceof CompareEQValueNumber and
1021- v .getDualValue ( ) = value
1067+ test instanceof CompareEQValueNumber and
1068+ if c = 0 then value = v .getDualValue ( ) else value = v
10221069 )
10231070 or
10241071 unary_compares_eq ( test .( BuiltinExpectCallValueNumber ) .getCondition ( ) , op , k , areEqual , value )
@@ -1192,6 +1239,12 @@ private module Cached {
11921239 unary_builtin_expect_eq ( test , op , k , areEqual , value )
11931240 }
11941241
1242+ private Instruction getBooleanInstruction ( Instruction instr ) {
1243+ result = instr .( ConvertBoolToIntOrPointerInstruction ) .getUnary ( )
1244+ or
1245+ result = getBooleanInstruction ( instr .( CopyInstruction ) .getSourceValue ( ) )
1246+ }
1247+
11951248 /*
11961249 * Simplification of inequality expressions
11971250 * Simplify conditions in the source to the canonical form l < r + k.
@@ -1215,6 +1268,26 @@ private module Cached {
12151268 exists ( AbstractValue dual | value = dual .getDualValue ( ) |
12161269 compares_lt ( test .( LogicalNotValueNumber ) .getUnary ( ) , left , right , k , isLt , dual )
12171270 )
1271+ or
1272+ // If we have e.g.:
1273+ // ```
1274+ // x = (a < b)
1275+ // if(x != c) { ... }
1276+ // ```
1277+ // then `x != c` is true implies that `a < b` is true.
1278+ // ```
1279+ exists ( Operand l , Operand r , ValueNumber vn , int c , AbstractValue v |
1280+ test .( CompareValueNumber ) .hasOperands ( l , r ) and
1281+ int_value ( r .getDef ( ) ) = c and
1282+ vn .getAnInstruction ( ) = getBooleanInstruction ( l .getDef ( ) ) and
1283+ compares_lt ( vn , left , right , k , isLt , v )
1284+ |
1285+ test instanceof CompareNEValueNumber and
1286+ if c = 0 then value = v else value = v .getDualValue ( )
1287+ or
1288+ test instanceof CompareEQValueNumber and
1289+ if c = 0 then value = v .getDualValue ( ) else value = v
1290+ )
12181291 }
12191292
12201293 /** Holds if `op < k` evaluates to `isLt` given that `test` evaluates to `value`. */
@@ -1234,6 +1307,26 @@ private module Cached {
12341307 int_value ( const ) = k1 and
12351308 k = k1 + k2
12361309 )
1310+ or
1311+ // If we have e.g.:
1312+ // ```
1313+ // x = (a < 10)
1314+ // if(x != c) { ... }
1315+ // ```
1316+ // then `x != c` is true implies that `a < 10` is true.
1317+ // ```
1318+ exists ( Operand l , Operand r , ValueNumber vn , int c , AbstractValue v |
1319+ test .( CompareValueNumber ) .hasOperands ( l , r ) and
1320+ int_value ( r .getDef ( ) ) = c and
1321+ vn .getAnInstruction ( ) = getBooleanInstruction ( l .getDef ( ) ) and
1322+ compares_lt ( vn , op , k , isLt , v )
1323+ |
1324+ test instanceof CompareNEValueNumber and
1325+ if c = 0 then value = v else value = v .getDualValue ( )
1326+ or
1327+ test instanceof CompareEQValueNumber and
1328+ if c = 0 then value = v .getDualValue ( ) else value = v
1329+ )
12371330 }
12381331
12391332 /** `(a < b + k) => (b > a - k) => (b >= a + (1-k))` */
0 commit comments