@@ -182,35 +182,30 @@ class UnknownVirtualVariable extends TUnknownVirtualVariable, VirtualVariable {
182182
183183Overlap getOverlap ( MemoryLocation def , MemoryLocation use ) {
184184 // The def and the use must have the same virtual variable, or no overlap is possible.
185- def .getVirtualVariable ( ) = use .getVirtualVariable ( ) and
186185 (
187186 // An UnknownVirtualVariable must totally overlap any location within the same virtual variable.
188- def instanceof UnknownVirtualVariable and result instanceof MustTotallyOverlap or
187+ def .getVirtualVariable ( ) = use .getVirtualVariable ( ) and
188+ def instanceof UnknownVirtualVariable and result instanceof MustTotallyOverlap
189+ or
189190 // An UnknownMemoryLocation may partially overlap any Location within the same virtual variable.
190- def instanceof UnknownMemoryLocation and result instanceof MayPartiallyOverlap or
191+ def .getVirtualVariable ( ) = use .getVirtualVariable ( ) and
192+ def instanceof UnknownMemoryLocation and result instanceof MayPartiallyOverlap
193+ or
191194 exists ( VariableMemoryLocation defVariableLocation |
192195 defVariableLocation = def and
193196 (
194197 (
195198 // A VariableMemoryLocation may partially overlap an unknown location within the same virtual variable.
199+ def .getVirtualVariable ( ) = use .getVirtualVariable ( ) and
196200 ( ( use instanceof UnknownMemoryLocation ) or ( use instanceof UnknownVirtualVariable ) ) and
197201 result instanceof MayPartiallyOverlap
198202 ) or
199203 // A VariableMemoryLocation overlaps another location within the same variable based on the relationship
200204 // of the two offset intervals.
201- exists ( VariableMemoryLocation useVariableLocation , IntValue defStartOffset , IntValue defEndOffset ,
202- IntValue useStartOffset , IntValue useEndOffset , Overlap intervalOverlap |
203- useVariableLocation = use and
204- // The def and use must access the same `IRVariable`.
205- defVariableLocation .getVariable ( ) = useVariableLocation .getVariable ( ) and
206- // The def and use intervals must overlap.
207- defStartOffset = defVariableLocation .getStartBitOffset ( ) and
208- defEndOffset = defVariableLocation .getEndBitOffset ( ) and
209- useStartOffset = useVariableLocation .getStartBitOffset ( ) and
210- useEndOffset = useVariableLocation .getEndBitOffset ( ) and
211- intervalOverlap = Interval:: getOverlap ( defStartOffset , defEndOffset , useStartOffset , useEndOffset ) and
205+ exists ( Overlap intervalOverlap |
206+ intervalOverlap = getVariableMemoryLocationOverlap ( def , use ) and
212207 if intervalOverlap instanceof MustExactlyOverlap then (
213- if defVariableLocation .getType ( ) = useVariableLocation .getType ( ) then (
208+ if def .getType ( ) = use .getType ( ) then (
214209 // The def and use types match, so it's an exact overlap.
215210 result instanceof MustExactlyOverlap
216211 )
@@ -234,6 +229,50 @@ Overlap getOverlap(MemoryLocation def, MemoryLocation use) {
234229 )
235230}
236231
232+ predicate isRelevantOffset ( VirtualVariable vv , IntValue offset ) {
233+ exists ( VariableMemoryLocation ml |
234+ ml .getVirtualVariable ( ) = vv
235+ |
236+ ml .getStartBitOffset ( ) = offset
237+ or
238+ ml .getEndBitOffset ( ) = offset
239+ )
240+ }
241+
242+ predicate isRelatableMemoryLocation ( VariableMemoryLocation vml ) {
243+ vml .getEndBitOffset ( ) != Ints:: unknown ( ) and
244+ vml .getStartBitOffset ( ) != Ints:: unknown ( )
245+ }
246+
247+ predicate isCoveredOffset ( VariableMemoryLocation vml , VirtualVariable vv , IntValue offset ) {
248+ isRelevantOffset ( vv , offset ) and
249+ vv = vml .getVirtualVariable ( ) and
250+ isRelatableMemoryLocation ( vml ) and
251+ vml .getStartBitOffset ( ) <= offset and
252+ offset <= vml .getEndBitOffset ( )
253+ }
254+
255+ predicate hasUnknownOffset ( VariableMemoryLocation vml , VirtualVariable vv ) {
256+ vml .getVirtualVariable ( ) = vv and
257+ (
258+ vml .getStartBitOffset ( ) = Ints:: unknown ( ) or
259+ vml .getEndBitOffset ( ) = Ints:: unknown ( )
260+ )
261+ }
262+
263+
264+
265+ Overlap getVariableMemoryLocationOverlap ( VariableMemoryLocation def , VariableMemoryLocation use ) {
266+ (
267+ exists ( VirtualVariable vv , IntValue offset | isCoveredOffset ( def , vv , offset ) and isCoveredOffset ( use , vv , offset ) )
268+ or
269+ hasUnknownOffset ( def , use .getVirtualVariable ( ) )
270+ or
271+ hasUnknownOffset ( use , def .getVirtualVariable ( ) )
272+ ) and
273+ result = Interval:: getOverlap ( def .getStartBitOffset ( ) , def .getEndBitOffset ( ) , use .getStartBitOffset ( ) , use .getEndBitOffset ( ) )
274+ }
275+
237276MemoryLocation getResultMemoryLocation ( Instruction instr ) {
238277 exists ( MemoryAccessKind kind |
239278 kind = instr .getResultMemoryAccess ( ) and
0 commit comments