C++/C#: Add combineOverlap() predicate

This commit is contained in:
Dave Bartolomeo
2020-04-20 15:37:41 -04:00
committed by Robert Marsh
parent 86b1d032ae
commit 922cf640f4
2 changed files with 70 additions and 0 deletions

View File

@@ -8,6 +8,16 @@ private newtype TOverlap =
*/
abstract class Overlap extends TOverlap {
abstract string toString();
/**
* Gets a value representing how precise this overlap is. The higher the value, the more precise
* the overlap. The precision values are ordered as
* follows, from most to least precise:
* `MustExactlyOverlap`
* `MustTotallyOverlap`
* `MayPartiallyOverlap`
*/
abstract int getPrecision();
}
/**
@@ -16,6 +26,8 @@ abstract class Overlap extends TOverlap {
*/
class MayPartiallyOverlap extends Overlap, TMayPartiallyOverlap {
final override string toString() { result = "MayPartiallyOverlap" }
final override int getPrecision() { result = 0 }
}
/**
@@ -24,6 +36,8 @@ class MayPartiallyOverlap extends Overlap, TMayPartiallyOverlap {
*/
class MustTotallyOverlap extends Overlap, TMustTotallyOverlap {
final override string toString() { result = "MustTotallyOverlap" }
final override int getPrecision() { result = 1 }
}
/**
@@ -32,4 +46,25 @@ class MustTotallyOverlap extends Overlap, TMustTotallyOverlap {
*/
class MustExactlyOverlap extends Overlap, TMustExactlyOverlap {
final override string toString() { result = "MustExactlyOverlap" }
final override int getPrecision() { result = 2 }
}
/**
* Gets the `Overlap` that best represents the relationship between two memory locations `a` and
* `c`, where `getOverlap(a, b) = previousOverlap` and `getOverlap(b, c) = newOverlap`, for some
* intermediate memory location `b`.
*/
Overlap combineOverlap(Overlap previousOverlap, Overlap newOverlap) {
// Note that it's possible that two less precise overlaps could combine to result in a more
// precise overlap. For example, both `previousOverlap` and `newOverlap` could be
// `MustTotallyOverlap` even though the actual relationship between `a` and `c` is
// `MustExactlyOverlap`. We will still return `MustTotallyOverlap` as the best conservative
// approximation we can make without additional input information.
result =
min(Overlap overlap |
overlap = [previousOverlap, newOverlap]
|
overlap order by overlap.getPrecision()
)
}