@@ -421,50 +421,36 @@ private predicate isRelatableMemoryLocation(VariableMemoryLocation vml) {
421421 vml .getStartBitOffset ( ) != Ints:: unknown ( )
422422}
423423
424- private predicate isCoveredOffset (
425- VirtualVariable vv , IRVariable var , int offsetRank , VariableMemoryLocation vml
426- ) {
427- exists ( int startRank , int endRank |
428- vml .getStartBitOffset ( ) = rank [ startRank ] ( IntValue offset_ | isRelevantOffset ( vv , offset_ ) ) and
429- vml .getEndBitOffset ( ) = rank [ endRank ] ( IntValue offset_ | isRelevantOffset ( vv , offset_ ) ) and
430- hasVariableAndVirtualVariable ( vv , var , vml ) and
424+ private predicate isCoveredOffset ( IRVariable var , int offsetRank , VariableMemoryLocation vml ) {
425+ exists ( int startRank , int endRank , VirtualVariable vvar |
426+ vml .getStartBitOffset ( ) = rank [ startRank ] ( IntValue offset_ | isRelevantOffset ( vvar , offset_ ) ) and
427+ vml .getEndBitOffset ( ) = rank [ endRank ] ( IntValue offset_ | isRelevantOffset ( vvar , offset_ ) ) and
428+ var = vml .getVariable ( ) and
429+ vvar = vml .getVirtualVariable ( ) and
431430 isRelatableMemoryLocation ( vml ) and
432431 offsetRank in [ startRank .. endRank ]
433432 )
434433}
435434
436- private predicate hasUnknownOffset ( VirtualVariable vv , IRVariable var , VariableMemoryLocation vml ) {
437- hasVariableAndVirtualVariable ( vv , var , vml ) and
435+ private predicate hasUnknownOffset ( IRVariable var , VariableMemoryLocation vml ) {
436+ vml . getVariable ( ) = var and
438437 (
439438 vml .getStartBitOffset ( ) = Ints:: unknown ( ) or
440439 vml .getEndBitOffset ( ) = Ints:: unknown ( )
441440 )
442441}
443442
444- private predicate hasVariableAndVirtualVariable (
445- VirtualVariable vv , IRVariable var , VariableMemoryLocation vml
446- ) {
447- var = vml .getVariable ( ) and
448- vv = vml .getVirtualVariable ( )
449- }
450-
451443private predicate overlappingIRVariableMemoryLocations (
452444 VariableMemoryLocation def , VariableMemoryLocation use
453445) {
454- exists ( VirtualVariable vv , IRVariable var , int offsetRank |
455- isCoveredOffset ( vv , var , offsetRank , def ) and
456- isCoveredOffset ( vv , var , offsetRank , use )
446+ exists ( IRVariable var , int offsetRank |
447+ isCoveredOffset ( var , offsetRank , def ) and
448+ isCoveredOffset ( var , offsetRank , use )
457449 )
458450 or
459- exists ( VirtualVariable vv , IRVariable var |
460- hasUnknownOffset ( vv , var , def ) and
461- hasVariableAndVirtualVariable ( vv , var , use )
462- )
451+ hasUnknownOffset ( use .getVariable ( ) , def )
463452 or
464- exists ( VirtualVariable vv , IRVariable var |
465- hasUnknownOffset ( vv , var , use ) and
466- hasVariableAndVirtualVariable ( vv , var , def )
467- )
453+ hasUnknownOffset ( def .getVariable ( ) , use )
468454}
469455
470456private Overlap getVariableMemoryLocationOverlap (
0 commit comments