Add safeguard against FM explosion

- FM has a worst case exponential complexity. For our purposes, this worst case
  is rarely expected, but could still appear due to improperly constructed
  constraints (a logical/memory error in other methods for eg.) or artificially
  created arbitrarily complex integer sets (adversarial / fuzz tests).

  Add a check to detect such an explosion in the number of constraints and
  conservatively return false from isEmpty() (instead of running out of memory
  or running for too long).

- Add an artifical virus test case.

PiperOrigin-RevId: 228753496
This commit is contained in:
Uday Bondhugula 2019-01-10 12:13:18 -08:00 committed by jpienaar
parent 9003490287
commit 2370c601ba
3 changed files with 84 additions and 2 deletions

View File

@ -203,8 +203,15 @@ class IntegerValueSet {
/// Returns true if this integer set is determined to be empty. Emptiness is
/// checked by by eliminating identifiers successively (through either
/// Gaussian or Fourier-Motzkin) while using the GCD test and a trivial
/// constraint check. Returns 'true' if the constaint system is found to be
/// empty; false otherwise.
/// invalid constraint check. Returns 'true' if the constaint system is found
/// to be empty; false otherwise. This method is exact for rational spaces but
/// not integer spaces - thus, if it returns true, the set is provably integer
/// empty as well, but if it returns false, it doesn't necessarily mean an
/// integer point exists in it. This method also returns false where an
/// explosion of constraints is detected - due to the super-exponential
/// worse-case complexity of Fourier-Motzkin elimination (rare for realistic
/// problem cases but possible for artificial adversarial or improperly
// constructed ones), this method returns false conservatively.
bool isEmpty() const;
bool getNumDims() const { return set.getNumDims(); }
@ -673,6 +680,18 @@ private:
/// Temporary ones or those that aren't associated to any Value are to be
/// set to None.
SmallVector<Optional<Value *>, 8> ids;
/// A parameter that controls detection of an unrealistic number of
/// constraints. If the number of constraints is this many times the number of
/// variables, we consider such a system out of line with the intended use
/// case of FlatAffineConstraints.
// The rationale for 32 is that in the typical simplest of cases, an
// identifier is expected to have one lower bound and one upper bound
// constraint. With a level of tiling or a connection to another identifier
// through a div or mod, an extra pair of bounds gets added. As a limit, we
// don't expect an identifier to have more than 32 lower/upper/equality
// constraints. This is conservatively set low and can be raised if needed.
constexpr static unsigned kExplosionFactor = 32;
};
} // end namespace mlir.

View File

@ -1024,6 +1024,16 @@ bool FlatAffineConstraints::isEmpty() const {
for (unsigned i = 0, e = tmpCst.getNumIds(); i < e; i++) {
tmpCst.FourierMotzkinEliminate(
getBestIdToEliminate(tmpCst, 0, tmpCst.getNumIds()));
// Check for a constraint explosion. This rarely happens in practice, but
// this check exists as a safeguard against improperly constructed
// constraint systems or artifically created arbitrarily complex systems
// that aren't the intended use case for FlatAffineConstraints. This is
// needed since FM has a worst case exponential complexity in theory.
if (tmpCst.getNumConstraints() >= kExplosionFactor * getNumIds()) {
LLVM_DEBUG(llvm::dbgs() << "FM constraint explosion detected");
return false;
}
// FM wouldn't have modified the equalities in any way. So no need to again
// run GCD test. Check for trivial invalid constraints.
if (tmpCst.hasInvalidConstraint())

View File

@ -53,6 +53,47 @@
d0 * 7 + d1 * 5 + s0 * 11 + s1 == 0,
d0 - 1 == 0, d0 + 2 == 0)
// This is an artifically created system to exercise the worst case behavior of
// FM elimination - as a safeguard against improperly constructed constraint
// systems or fuzz input.
#set_fuzz_virus = (d0, d1, d2, d3, d4, d5) : ( 1089234*d0 + 203472*d1 + 82342 >= 0,
-55*d0 + 24*d1 + 238*d2 - 234*d3 - 9743 >= 0,
-5445*d0 - 284*d1 + 23*d2 + 34*d3 - 5943 >= 0,
-5445*d0 + 284*d1 + 238*d2 - 34*d3 >= 0,
445*d0 + 284*d1 + 238*d2 + 39*d3 >= 0,
-545*d0 + 214*d1 + 218*d2 - 94*d3 >= 0,
44*d0 - 184*d1 - 231*d2 + 14*d3 >= 0,
-45*d0 + 284*d1 + 138*d2 - 39*d3 >= 0,
154*d0 - 84*d1 + 238*d2 - 34*d3 >= 0,
54*d0 - 284*d1 - 223*d2 + 384*d3 >= 0,
-55*d0 + 284*d1 + 23*d2 + 34*d3 >= 0,
54*d0 - 84*d1 + 28*d2 - 34*d3 >= 0,
54*d0 - 24*d1 - 23*d2 + 34*d3 >= 0,
-55*d0 + 24*d1 + 23*d2 + 4*d3 >= 0,
15*d0 - 84*d1 + 238*d2 - 3*d3 >= 0,
5*d0 - 24*d1 - 223*d2 + 84*d3 >= 0,
-5*d0 + 284*d1 + 23*d2 - 4*d3 >= 0,
14*d0 + 4*d2 + 7234 >= 0,
-174*d0 - 534*d2 + 9834 >= 0,
194*d0 - 954*d2 + 9234 >= 0,
47*d0 - 534*d2 + 9734 >= 0,
-194*d0 - 934*d2 + 984 >= 0,
-947*d0 - 953*d2 + 234 >= 0,
184*d0 - 884*d2 + 884 >= 0,
-174*d0 + 834*d2 + 234 >= 0,
844*d0 + 634*d2 + 9874 >= 0,
-797*d2 - 79*d3 + 257 >= 0,
2039*d0 + 793*d2 - 99*d3 - 24*d4 + 234*d5 >= 0,
78*d2 - 788*d5 + 257 >= 0,
d3 - (d5 + 97*d0) floordiv 423 >= 0,
234* (d0 + d3 mod 5 floordiv 2342) mod 2309
+ (d0 + 2038*d3) floordiv 208 >= 0,
239* (d0 + 2300 * d3) floordiv 2342
mod 2309 mod 239423 == 0,
d0 + d3 mod 2642 + (d3 + 2*d0) mod 1247
mod 2038 mod 2390 mod 2039 floordiv 55 >= 0
)
func @test() {
for %n0 = 0 to 127 {
for %n1 = 0 to 7 {
@ -148,6 +189,18 @@ func @test_gaussian_elimination_empty_set5() {
return
}
// CHECK-LABEL: func @test_fuzz_explosion
func @test_fuzz_explosion(%arg0 : index, %arg1 : index, %arg2 : index, %arg3 : index) {
for %i0 = 1 to 10 {
for %i1 = 1 to 100 {
if #set_fuzz_virus(%i0, %i1, %arg0, %arg1, %arg2, %arg3) {
}
}
}
return
}
// CHECK-LABEL: func @test_empty_set(%arg0: index) {
func @test_empty_set(%N : index) {
for %i = 0 to 10 {