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

Question

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

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));
}