确定两个周期间隔序列是否具有非空交集的算法

Question

我正在寻找一种算法，给定自然参数 l1、n1、m1、l2、n2、m2 和大小， 当且仅当存在自然数 k1、k2、r1、r2 且满足以下条件时，才回答“true”:

l1 + k1*m1 + r1 = l2 + k2*m2 + r2

约束条件 k1 <= n1、k2 <= n2、r1 < size、r2 < size 和 r1 <> r2。

明显的解在 min(n1, n2) 中是线性的。我正在寻找更高效的东西。

上下文

我正在尝试在静态分析器中实现对 C99 规则 6.5.16.1:3 的检查

If the value being stored in an object is read from another object that overlaps in any way the storage of the first object, then the overlap shall be exact [...] otherwise, the behavior is undefined.

当分析器遇到赋值*p1 = *p2;时，其中p1和p2可能指向同一个 block ，它必须检查p1 和 p2 指向的区域不会以上述规则禁止的方式重叠。上面的参数“size”对应于p1和p2指向的类型的大小。该尺寸是静态已知的。 p1 已知指向 block 内的偏移量表示为一组 l1 + k1*m1，其中 l1 和 m1 固定，已知自然整数，k1 在 0 和 n1 之间变化(n1 也是固定的)并已知)。类似地，对于某些已知的 l2、m2 和 n2，已知 p2 所指向的偏移量的形式为 l2 + k2*m2。等式 l1 + k1*m1 + r1 = l2 + k2*m2 + r2 对应于一些重叠偏移的存在。条件 r1 <> r2 对应于重叠不精确的情况，此时分析器必须发出警告。

Answer 1

您似乎正在寻找线性同余系统的解决方案。 Chinese remainder theorem应该适用。它不会应用您的边界检查，但如果它找到解决方案，您可以自己简单地检查边界。

编辑:忘记 CRT。

假设size <= m1和size <= m2 ，将内存区域的低(包含)和高(不包含)边缘建模为线性关系:

addr1low = l1 + k1*m1
addr1high = addr1low + size = l1 + k1*m1 + size
addr2low = l2 + k2*m2
addr2high = addr2low + size = l2 + k2*m2 + size

你想知道是否存在k1, k2在 addr1low < addr2low < addr1high 的范围内或addr1low < addr2high < addr1high 。注意排它不等式；这样我们就可以避免完全重叠范围。

假设m1 = m2 = m 。考虑:

addr1low < addr2low
l1 + k1*m < l2 + k2*m
(k1 - k2) * m < l2 - l1
k1 - k2 < (l2 - l1) / m

addr2low < addr1high
l2 + k2*m < l1 + k1*m + size
l2 - l1 < (k1 - k2) * m + size
(l2 - l1 - size) < (k1 - k2) * m
(l2 - l1 - size) / m < k1 - k2

上述过程是可逆的。假设k1, k2可能是 0，-n2 <= k1 - k2 <= n1 。如果有一个整数在 (l2 - l1 - size) / m 之间和(l2 - l1) / m ，则系统成立并且存在重叠。也就是说，如果ceil(max((l2 - l1 - size) / m, -n2)) <= floor(min((l2 - l1) / m, n1)) 。另一个案例 ( addr1low < addr2high < addr1high ) 的处理过程类似:

addr1low < addr2high
l1 + k1*m < l2 + k2*m + size
// ..
(l1 - l2 - size) / m < k2 - k1

addr2high < addr1high
addr2low + size < addr1low + size
addr2low < addr1low
// ..
k2 - k1 < (l1 - l2) / m

现在测试变成 ceil(max((l1 - l2 - size) / m, -n1)) <= floor(min((l1 - l2) / m, n2)) .

现在考虑m1 <> m1 ，并且不失一般性地取 m1 < m2 .

将变量视为连续的，求解交集:

addr1low < addr2low
l1 + k*m1 < l2 + k*m2
(l1 - l2) < k * (m2 - m1)
(l1 - l2) / (m2 - m1) < k

addr2low < addr1high
l2 + k*m2 < l1 + k*m1 + size
l2 - l1 - size < k * (m1 - m2)
(l2 - l1 - size) / (m1 - m2) > k  // m1 - m2 < 0

同样，这些步骤是可逆的，因此任何整数 k < min(n1, n2)满足界限将使系统成立。也就是说，如果 ceil(max((l1 - l2) / (m2 - m1), 0)) <= floor(min((l2 - l1 - size) / (m1 - m2), n1, n2)) 则成立。 。另一种情况:

addr1low < addr2high
l1 + k*m1 < l2 + k*m2 + size
l1 - l2 - size < k * (m2 - m1)
(l1 - l2 - size) / (m2 - m1) < k

addr2high < addr1high
addr2low + size < addr1low + size
addr2low < addr1low
l2 + k*m2 < l1 + k*m1
l2 - l1 < k * (m1 - m2)
(l2 - l1) / (m1 - m2) > k   // m1 - m2 < 0

这里的测试变成 ceil(max((l1 - l2 - size) / (m2 - m1), 0)) <= floor(min((l2 - l1) / (m1 - m2), n1, n2)) .

最终的伪代码可能如下所示:

intersectos?(l1, n1, m1, l2, n2, m2, size) {
  if (m1 == m2) {
    return ceil(max((l2 - l1 - size) / m, -n2)) <= floor(min((l2 - l1) / m, n1)) ||
           ceil(max((l1 - l2 - size) / m, -n1)) <= floor(min((l1 - l2) / m, n2));
  }

  if (m1 > m2) {
    swap the arguments
  }

  return ceil(max((l1 - l2) / (m2 - m1), 0)) <= floor(min((l2 - l1 - size) / (m1 - m2), n1, n2)) ||
         ceil(max((l1 - l2 - size) / (m2 - m1), 0)) <= floor(min((l2 - l1) / (m1 - m2), n1, n2));
}