@@ -1096,8 +1096,17 @@ module Expressions {
10961096 predicate subscriptPointsTo ( SubscriptNode subscr , PointsToContext context , ObjectInternal value , ControlFlowNode origin , ControlFlowNode obj , ObjectInternal objvalue ) {
10971097 subscr .isLoad ( ) and
10981098 obj = subscr .getObject ( ) and
1099+ origin = subscr and
10991100 PointsToInternal:: pointsTo ( obj , context , objvalue , _) and
1100- value = ObjectInternal:: unknown ( ) and origin = subscr
1101+ (
1102+ objvalue .subscriptUnknown ( ) and
1103+ value = ObjectInternal:: unknown ( )
1104+ or
1105+ exists ( int n |
1106+ PointsToInternal:: pointsTo ( subscr .getIndex ( ) , context , TInt ( n ) , _) and
1107+ value = objvalue .( SequenceObjectInternal ) .getItem ( n )
1108+ )
1109+ )
11011110 }
11021111
11031112 /** Track bitwise expressions so we can handle integer flags and enums.
@@ -1256,24 +1265,55 @@ module Expressions {
12561265 exists ( boolean strict , boolean sense , ObjectInternal other |
12571266 inequalityTest ( comp , context , use , val , other , strict , sense )
12581267 |
1259- val .intValue ( ) < other .intValue ( ) and result = sense
1260- or
1261- val .intValue ( ) > other .intValue ( ) and result = sense .booleanNot ( )
1262- or
1263- val .intValue ( ) = other .intValue ( ) and result = strict .booleanXor ( sense )
1268+ compare ( val , other ) = - 1 and result = sense
12641269 or
1265- val .strValue ( ) < other .strValue ( ) and result = sense
1266- or
1267- val .strValue ( ) > other .strValue ( ) and result = sense .booleanNot ( )
1270+ compare ( val , other ) = 0 and result = strict .booleanNot ( )
12681271 or
1269- val . strValue ( ) = other . strValue ( ) and result = strict . booleanXor ( sense )
1272+ compare ( val , other ) = 1 and result = sense . booleanNot ( )
12701273 or
12711274 val .isComparable ( ) = false and result = maybe ( )
12721275 or
12731276 other .isComparable ( ) = false and result = maybe ( )
12741277 )
12751278 }
12761279
1280+ private int compare ( ObjectInternal val , ObjectInternal other ) {
1281+ inequalityTest ( _, _, _, val , other , _, _) and
1282+ result = compare_unbound ( val , other )
1283+ or
1284+ result = compare_sequence ( val , other , 0 )
1285+ }
1286+
1287+ bindingset [ val, other]
1288+ private int compare_unbound ( ObjectInternal val , ObjectInternal other ) {
1289+ val .intValue ( ) < other .intValue ( ) and result = - 1
1290+ or
1291+ val .intValue ( ) > other .intValue ( ) and result = 1
1292+ or
1293+ val .intValue ( ) = other .intValue ( ) and result = 0
1294+ or
1295+ val .strValue ( ) < other .strValue ( ) and result = - 1
1296+ or
1297+ val .strValue ( ) > other .strValue ( ) and result = 0
1298+ or
1299+ val .strValue ( ) = other .strValue ( ) and result = 1
1300+ }
1301+
1302+ private int compare_sequence ( SequenceObjectInternal val , SequenceObjectInternal other , int n ) {
1303+ inequalityTest ( _, _, _, val , other , _, _) and
1304+ (
1305+ n = val .length ( ) and other .length ( ) > n and result = - 1
1306+ or
1307+ n = other .length ( ) and val .length ( ) > n and result = 1
1308+ or
1309+ n = other .length ( ) and n = val .length ( ) and result = 0
1310+ or
1311+ result != 0 and result = compare_unbound ( val .getItem ( n ) , val .getItem ( n ) )
1312+ or
1313+ compare_unbound ( val .getItem ( n ) , val .getItem ( n ) ) = 0 and result = compare_sequence ( val , other , n + 1 )
1314+ )
1315+ }
1316+
12771317 pragma [ noinline]
12781318 private predicate inequalityTest ( CompareNode comp , PointsToContext context , ControlFlowNode operand , ObjectInternal opvalue , ObjectInternal other , boolean strict , boolean sense ) {
12791319 exists ( ControlFlowNode r |
0 commit comments