@@ -406,6 +406,22 @@ class GroupedMemoryLocation extends TGroupedMemoryLocation, MemoryLocation {
406
406
predicate isSome ( ) { isAll = false }
407
407
}
408
408
409
+ private GroupedMemoryLocation getGroupedMemoryLocation (
410
+ Allocation alloc , boolean isMayAccess , boolean isAll
411
+ ) {
412
+ result .getAnAllocation ( ) = alloc and
413
+ (
414
+ isMayAccess = true and result .isMayAccess ( )
415
+ or
416
+ isMayAccess = false and not result .isMayAccess ( )
417
+ ) and
418
+ (
419
+ isAll = true and result .isAll ( )
420
+ or
421
+ isAll = false and result .isSome ( )
422
+ )
423
+ }
424
+
409
425
class EntireAllocationMemoryLocation extends TEntireAllocationMemoryLocation ,
410
426
AllocationMemoryLocation
411
427
{
@@ -755,13 +771,24 @@ MemoryLocation getResultMemoryLocation(Instruction instr) {
755
771
(
756
772
(
757
773
isIndirectOrBufferMemoryAccess ( kind ) and
758
- if hasResultMemoryAccess ( instr , _, _, _, _, _, _)
774
+ if hasResultMemoryAccess ( _ , instr , _ , _, _, _, _, _, _)
759
775
then
760
- exists ( Allocation var , IRType type , IntValue startBitOffset , IntValue endBitOffset |
761
- hasResultMemoryAccess ( instr , var , type , _, startBitOffset , endBitOffset , isMayAccess ) and
762
- result =
763
- TVariableMemoryLocation ( var , type , _, startBitOffset , endBitOffset ,
764
- unbindBool ( isMayAccess ) )
776
+ exists (
777
+ Allocation var , IRType type , IntValue startBitOffset , IntValue endBitOffset ,
778
+ boolean grouped
779
+ |
780
+ hasResultMemoryAccess ( _, instr , var , type , _, startBitOffset , endBitOffset , isMayAccess ,
781
+ grouped )
782
+ |
783
+ // If the instruction is only associated with one allocation we assign it a `VariableMemoryLocation`
784
+ if grouped = false
785
+ then
786
+ result =
787
+ TVariableMemoryLocation ( var , type , _, startBitOffset , endBitOffset ,
788
+ unbindBool ( isMayAccess ) )
789
+ else
790
+ // And otherwise we assign it a memory location that groups all the relevant memory locations into one.
791
+ result = getGroupedMemoryLocation ( var , unbindBool ( isMayAccess ) , false )
765
792
)
766
793
else result = TUnknownMemoryLocation ( instr .getEnclosingIRFunction ( ) , isMayAccess )
767
794
)
@@ -788,12 +815,23 @@ MemoryLocation getOperandMemoryLocation(MemoryOperand operand) {
788
815
(
789
816
(
790
817
isIndirectOrBufferMemoryAccess ( kind ) and
791
- if hasOperandMemoryAccess ( operand , _, _, _, _, _, _)
818
+ if hasOperandMemoryAccess ( _ , operand , _ , _, _, _, _, _, _)
792
819
then
793
- exists ( Allocation var , IRType type , IntValue startBitOffset , IntValue endBitOffset |
794
- hasOperandMemoryAccess ( operand , var , type , _, startBitOffset , endBitOffset , isMayAccess ) and
795
- result =
796
- TVariableMemoryLocation ( var , type , _, startBitOffset , endBitOffset , isMayAccess )
820
+ exists (
821
+ Allocation var , IRType type , IntValue startBitOffset , IntValue endBitOffset ,
822
+ boolean grouped
823
+ |
824
+ hasOperandMemoryAccess ( _, operand , var , type , _, startBitOffset , endBitOffset ,
825
+ isMayAccess , grouped )
826
+ |
827
+ // If the operand is only associated with one memory location we assign it a `VariableMemoryLocation`
828
+ if grouped = false
829
+ then
830
+ result =
831
+ TVariableMemoryLocation ( var , type , _, startBitOffset , endBitOffset , isMayAccess )
832
+ else
833
+ // And otherwise we assign it a memory location that groups all relevant memory locations into one.
834
+ result = getGroupedMemoryLocation ( var , isMayAccess , false )
797
835
)
798
836
else result = TUnknownMemoryLocation ( operand .getEnclosingIRFunction ( ) , isMayAccess )
799
837
)
0 commit comments