@@ -229,7 +229,21 @@ Overlap getOverlap(MemoryLocation def, MemoryLocation use) {
229229 )
230230}
231231
232- predicate isRelevantOffset ( VirtualVariable vv , IntValue offset ) {
232+ /*
233+ * The following predicates compute the overlap relation between `VariableMemoryLocation`s in the
234+ * same `VirtualVariable` as follows:
235+ * 1. Compute the set of offsets within each virtual variable in `isRelevantOffset` (linear in
236+ * the number of VMLs)
237+ * 2. Compute the set of offsets that each VML with known start and end offsets covers in
238+ * `isCoveredOffset` (this is currently quadratic in the number of VMLs in a VVar, but
239+ * could be optimized further. The quadratic portion is never materialized, and it seems to
240+ * be performant in practice)
241+ * 3. In `getVariableMemoryLocationOverlap`, compute the set of overlapping pairs of VMLs using a
242+ * join on `isCoveredOffset` (linear in the size of the overlap set)
243+ * 4. In `getVariableMemoryLocationOverlap`, compute the precise overlap relation for each
244+ * overlapping pair of VMLs (linear in the size of the overlap set)
245+ */
246+ private predicate isRelevantOffset ( VirtualVariable vv , IntValue offset ) {
233247 exists ( VariableMemoryLocation ml |
234248 ml .getVirtualVariable ( ) = vv
235249 |
@@ -239,30 +253,28 @@ predicate isRelevantOffset(VirtualVariable vv, IntValue offset) {
239253 )
240254}
241255
242- predicate isRelatableMemoryLocation ( VariableMemoryLocation vml ) {
256+ private predicate isRelatableMemoryLocation ( VariableMemoryLocation vml ) {
243257 vml .getEndBitOffset ( ) != Ints:: unknown ( ) and
244258 vml .getStartBitOffset ( ) != Ints:: unknown ( )
245259}
246260
247- predicate isCoveredOffset ( VariableMemoryLocation vml , VirtualVariable vv , IntValue offset ) {
261+ private predicate isCoveredOffset ( VariableMemoryLocation vml , VirtualVariable vv , IntValue offset ) {
248262 isRelevantOffset ( vv , offset ) and
249263 vv = vml .getVirtualVariable ( ) and
250264 isRelatableMemoryLocation ( vml ) and
251265 vml .getStartBitOffset ( ) <= offset and
252266 offset <= vml .getEndBitOffset ( )
253267}
254268
255- predicate hasUnknownOffset ( VariableMemoryLocation vml , VirtualVariable vv ) {
269+ private predicate hasUnknownOffset ( VariableMemoryLocation vml , VirtualVariable vv ) {
256270 vml .getVirtualVariable ( ) = vv and
257271 (
258272 vml .getStartBitOffset ( ) = Ints:: unknown ( ) or
259273 vml .getEndBitOffset ( ) = Ints:: unknown ( )
260274 )
261275}
262276
263-
264-
265- Overlap getVariableMemoryLocationOverlap ( VariableMemoryLocation def , VariableMemoryLocation use ) {
277+ private Overlap getVariableMemoryLocationOverlap ( VariableMemoryLocation def , VariableMemoryLocation use ) {
266278 def .getVariable ( ) = use .getVariable ( ) and
267279 (
268280 exists ( VirtualVariable vv , IntValue offset | isCoveredOffset ( def , vv , offset ) and isCoveredOffset ( use , vv , offset ) )
0 commit comments