@@ -406,6 +406,22 @@ class GroupedMemoryLocation extends TGroupedMemoryLocation, MemoryLocation {
406406 predicate isSome ( ) { isAll = false }
407407}
408408
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+
409425class EntireAllocationMemoryLocation extends TEntireAllocationMemoryLocation ,
410426 AllocationMemoryLocation
411427{
@@ -755,13 +771,24 @@ MemoryLocation getResultMemoryLocation(Instruction instr) {
755771 (
756772 (
757773 isIndirectOrBufferMemoryAccess ( kind ) and
758- if hasResultMemoryAccess ( instr , _, _, _, _, _, _)
774+ if hasResultMemoryAccess ( _ , instr , _ , _, _, _, _, _, _)
759775 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 )
765792 )
766793 else result = TUnknownMemoryLocation ( instr .getEnclosingIRFunction ( ) , isMayAccess )
767794 )
@@ -788,12 +815,23 @@ MemoryLocation getOperandMemoryLocation(MemoryOperand operand) {
788815 (
789816 (
790817 isIndirectOrBufferMemoryAccess ( kind ) and
791- if hasOperandMemoryAccess ( operand , _, _, _, _, _, _)
818+ if hasOperandMemoryAccess ( _ , operand , _ , _, _, _, _, _, _)
792819 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 )
797835 )
798836 else result = TUnknownMemoryLocation ( operand .getEnclosingIRFunction ( ) , isMayAccess )
799837 )
0 commit comments