pkg/compiler/lib/src/cps_ir/octagon.dart - sdk - Git at Google

 // Copyright (c) 2015, the Dart project authors.  Please see the AUTHORS file
 // for details. All rights reserved. Use of this source code is governed by a
 // BSD-style license that can be found in the LICENSE file.

 library dart2js.cps_ir.octagon;

 /// For every variable in the constraint system, two [SignedVariable]s exist,
 /// representing the positive and negative uses of the variable.
 ///
 /// For instance, `v1 - v2` is represented as `v1 + (-v2)`, with -v2 being
 /// a "negative use" of v2.
 class SignedVariable {
   /// Negated version of this variable.
   SignedVariable _negated;
   SignedVariable get negated => _negated;

   /// Constraints that mention this signed variable.
   final List<Constraint> _constraints = <Constraint>[];

   static int _hashCount = 0;
   final int hashCode = (_hashCount = _hashCount + 1) & 0x0fffffff;

   /// Temporary field used by the constraint solver's graph search.
   bool _isBeingVisited = false;

   SignedVariable._make() {
     _negated = new SignedVariable._makeTwin(this);
   }

   SignedVariable._makeTwin(this._negated);
 }

 /// A constraint of form `v1 + v2 <= k`.
 class Constraint {
   final SignedVariable v1, v2;
   final int bound;

   Constraint(this.v1, this.v2, this.bound);
 }

 /// A system of constraints of form `v1 + v2 <= k`.
 ///
 /// Constraints can be added and removed in stack-order.  The octagon will
 /// always determine whether it is in a solvable state, but will otherwise
 /// not optimize its internal representation.
 ///
 /// There is currently no support for querying the upper and lower bounds
 /// of a variable, (which can be used to approximate ternary constraints
 /// `v1 + v2 + v3 <= k`), but it is something we could consider adding.
 class Octagon {
   /// Number of constraints that have been added since the constraint system
   /// became unsolvable (including the constraint that made it unsolvable).
   ///
   /// This is well-defined because constraints are pushed/popped in stack order.
   int _unsolvableCounter = 0;

   /// True if the constraint system is unsolvable in its current state.
   ///
   /// It will remain unsolvable until a number of constraints have been popped.
   bool get isUnsolvable => _unsolvableCounter > 0;

   /// True if the constraint system is solvable in its current state.
   bool get isSolvable => _unsolvableCounter == 0;

   /// Make a new variable, optionally with known lower and upper bounds
   /// (both inclusive).
   ///
   /// The constraints generated for [min] and [max] are also expressible using
   /// [Constraint] objects, but the constraints added in [makeVariable] live
   /// outside the stack discipline (i.e. the bounds are never popped), which is
   /// useful when generating variables on-the-fly.
   SignedVariable makeVariable([int min, int max]) {
     SignedVariable v1 = new SignedVariable._make();
     if (min != null) {
       // v1 >= min   <==>   -v1 - v1 <= -2 * min
       v1.negated._constraints.add(
           new Constraint(v1.negated, v1.negated, -2 * min));
     }
     if (max != null) {
       // v1 <= max   <==>   v1 + v1 <= 2 * max
       v1._constraints.add(new Constraint(v1, v1, 2 * max));
     }
     return v1;
   }

   /// Add the constraint `v1 + v2 <= k`.
   ///
   /// The constraint should be removed again using [popConstraint].
   void pushConstraint(Constraint constraint) {
     if (_unsolvableCounter > 0) {
       ++_unsolvableCounter;
     }
     constraint.v1._constraints.add(constraint);
     if (constraint.v1 != constraint.v2) {
       constraint.v2._constraints.add(constraint);
     }
     // Check if this constraint has made the system unsolvable.
     if (_unsolvableCounter == 0 && _checkUnsolvable(constraint)) {
       _unsolvableCounter = 1;
     }
   }

   /// Remove a constraint that was previously added with [pushConstraint].
   ///
   /// Constraints must be added and removed in stack-order.
   void popConstraint(Constraint constraint) {
     assert(constraint.v1._constraints.last == constraint);
     assert(constraint.v2._constraints.last == constraint);
     constraint.v1._constraints.removeLast();
     if (constraint.v1 != constraint.v2) {
       constraint.v2._constraints.removeLast();
     }
     if (_unsolvableCounter > 0) {
       --_unsolvableCounter;
     }
   }

   // Temporaries using during path finding.
   SignedVariable _goal;
   Map<SignedVariable, int> _distanceToGoal;

   /// Return true if the recently added [constraint] made the system unsolvable.
   ///
   /// This function assumes the system was solvable before adding [constraint].
   bool _checkUnsolvable(Constraint constraint) {
     // Constraints are transitively composed like so:
     //    v1 - v2 <= k1
     //    v2 - v3 <= k2
     // implies:
     //    v1 - v3 <= k1 + k2
     //
     // We construct a graph such that the tightest bound on `v1 - v3` is the
     // weight of the shortest path from `v1` to `v3`.
     //
     // Ever constraint `v1 - v2 <= k` gives rise to two edges:
     //     (v1)  --k--> (v2)
     //     (-v2) --k--> (-v2)
     //
     // The system is unsolvable if and only if a negative-weight cycle exists
     // in this graph (this corresponds to a variable being less than itself).

     // We assume the system was solvable to begin with, so we only look for
     // cycles that use the new edges.
     //
     // The new [constraint] `v1 + v2 <= k` just added the edges:
     //     (v1)  --k--> (-v2)
     //     (v2)  --k--> (-v1)
     //
     // Look for a path from (-v2) to (v1) with weight at most -k-1, as this
     // will complete a negative-weight cycle.

     // It suffices to do this once. We need not check for the converse path
     // (-v1) to (v2) because of the symmetry in the graph.
     //
     // Note that the graph symmetry is not a redundancy. Some cycles include
     // both of the new edges at once, so they must be added to the graph
     // beforehand.
     _goal = constraint.v2;
     _distanceToGoal = <SignedVariable, int>{};
     int targetWeight = -constraint.bound - 1;
     int pathWeight = _search(constraint.v1.negated, targetWeight, 0);
     return pathWeight != null && pathWeight <= targetWeight;
   }

   static const int MAX_DEPTH = 100;

   /// Returns the shortest path from [v1] to [_goal] (or any path shorter than
   /// [budget]), or `null` if no path exists.
   int _search(SignedVariable v1, int budget, int depth) {
     if (v1 == _goal && budget >= 0) return 0;

     // Disregard paths that use a lot of edges.
     // In extreme cases (e.g. hundreds of `push` calls or nested ifs) this can
     // get slow and/or overflow the stack.  Most paths that matter are very
     // short (1-5 edges) with some occasional 10-30 length paths in math code.
     if (depth >= MAX_DEPTH) return null;

     // We found a cycle, but not the one we're looking for. If the constraint
     // system was solvable to being with, then this must be a positive-weight
     // cycle, and no shortest path goes through a positive-weight cycle.
     if (v1._isBeingVisited) return null;

     // Check if we have previously searched from here.
     if (_distanceToGoal.containsKey(v1)) {
       // We have already searched this node, return the cached answer.
       // Note that variables may explicitly map to null, so the double lookup
       // is necessary.
       return _distanceToGoal[v1];
     }

     v1._isBeingVisited = true;

     int shortestDistance = v1 == _goal ? 0 : null;
     for (Constraint c in v1._constraints) {
       SignedVariable v2 = c.v1 == v1 ? c.v2 : c.v1;
       int distance = _search(v2.negated, budget - c.bound, depth + 1);
       if (distance != null) {
         distance += c.bound; // Pay the cost of using the edge.
          if (distance <= budget) {
           // Success! We found a path that is short enough so return fast.
           // All recursive calls will now return immediately, so there is no
           // need to update distanceToGoal, but we need to clear the
           // beingVisited flag for the next query.
           v1._isBeingVisited = false;
           return distance;
         } else if (shortestDistance == null || distance < shortestDistance) {
           shortestDistance = distance;
         }
       }
     }
     v1._isBeingVisited = false;
     _distanceToGoal[v1] = shortestDistance;
     return shortestDistance;
   }
 }
	// Copyright (c) 2015, the Dart project authors. Please see the AUTHORS file
	// for details. All rights reserved. Use of this source code is governed by a
	// BSD-style license that can be found in the LICENSE file.

	library dart2js.cps_ir.octagon;

	/// For every variable in the constraint system, two [SignedVariable]s exist,
	/// representing the positive and negative uses of the variable.
	///
	/// For instance, `v1 - v2` is represented as `v1 + (-v2)`, with -v2 being
	/// a "negative use" of v2.
	class SignedVariable {
	/// Negated version of this variable.
	SignedVariable _negated;
	SignedVariable get negated => _negated;

	/// Constraints that mention this signed variable.
	final List<Constraint> _constraints = <Constraint>[];

	static int _hashCount = 0;
	final int hashCode = (_hashCount = _hashCount + 1) & 0x0fffffff;

	/// Temporary field used by the constraint solver's graph search.
	bool _isBeingVisited = false;

	SignedVariable._make() {
	_negated = new SignedVariable._makeTwin(this);
	}

	SignedVariable._makeTwin(this._negated);
	}

	/// A constraint of form `v1 + v2 <= k`.
	class Constraint {
	final SignedVariable v1, v2;
	final int bound;

	Constraint(this.v1, this.v2, this.bound);
	}

	/// A system of constraints of form `v1 + v2 <= k`.
	///
	/// Constraints can be added and removed in stack-order. The octagon will
	/// always determine whether it is in a solvable state, but will otherwise
	/// not optimize its internal representation.
	///
	/// There is currently no support for querying the upper and lower bounds
	/// of a variable, (which can be used to approximate ternary constraints
	/// `v1 + v2 + v3 <= k`), but it is something we could consider adding.
	class Octagon {
	/// Number of constraints that have been added since the constraint system
	/// became unsolvable (including the constraint that made it unsolvable).
	///
	/// This is well-defined because constraints are pushed/popped in stack order.
	int _unsolvableCounter = 0;

	/// True if the constraint system is unsolvable in its current state.
	///
	/// It will remain unsolvable until a number of constraints have been popped.
	bool get isUnsolvable => _unsolvableCounter > 0;

	/// True if the constraint system is solvable in its current state.
	bool get isSolvable => _unsolvableCounter == 0;

	/// Make a new variable, optionally with known lower and upper bounds
	/// (both inclusive).
	///
	/// The constraints generated for [min] and [max] are also expressible using
	/// [Constraint] objects, but the constraints added in [makeVariable] live
	/// outside the stack discipline (i.e. the bounds are never popped), which is
	/// useful when generating variables on-the-fly.
	SignedVariable makeVariable([int min, int max]) {
	SignedVariable v1 = new SignedVariable._make();
	if (min != null) {
	// v1 >= min <==> -v1 - v1 <= -2 * min
	v1.negated._constraints.add(
	new Constraint(v1.negated, v1.negated, -2 * min));
	}
	if (max != null) {
	// v1 <= max <==> v1 + v1 <= 2 * max
	v1._constraints.add(new Constraint(v1, v1, 2 * max));
	}
	return v1;
	}

	/// Add the constraint `v1 + v2 <= k`.
	///
	/// The constraint should be removed again using [popConstraint].
	void pushConstraint(Constraint constraint) {
	if (_unsolvableCounter > 0) {
	++_unsolvableCounter;
	}
	constraint.v1._constraints.add(constraint);
	if (constraint.v1 != constraint.v2) {
	constraint.v2._constraints.add(constraint);
	}
	// Check if this constraint has made the system unsolvable.
	if (_unsolvableCounter == 0 && _checkUnsolvable(constraint)) {
	_unsolvableCounter = 1;
	}
	}

	/// Remove a constraint that was previously added with [pushConstraint].
	///
	/// Constraints must be added and removed in stack-order.
	void popConstraint(Constraint constraint) {
	assert(constraint.v1._constraints.last == constraint);
	assert(constraint.v2._constraints.last == constraint);
	constraint.v1._constraints.removeLast();
	if (constraint.v1 != constraint.v2) {
	constraint.v2._constraints.removeLast();
	}
	if (_unsolvableCounter > 0) {
	--_unsolvableCounter;
	}
	}

	// Temporaries using during path finding.
	SignedVariable _goal;
	Map<SignedVariable, int> _distanceToGoal;

	/// Return true if the recently added [constraint] made the system unsolvable.
	///
	/// This function assumes the system was solvable before adding [constraint].
	bool _checkUnsolvable(Constraint constraint) {
	// Constraints are transitively composed like so:
	// v1 - v2 <= k1
	// v2 - v3 <= k2
	// implies:
	// v1 - v3 <= k1 + k2
	//
	// We construct a graph such that the tightest bound on `v1 - v3` is the
	// weight of the shortest path from `v1` to `v3`.
	//
	// Ever constraint `v1 - v2 <= k` gives rise to two edges:
	// (v1) --k--> (v2)
	// (-v2) --k--> (-v2)
	//
	// The system is unsolvable if and only if a negative-weight cycle exists
	// in this graph (this corresponds to a variable being less than itself).

	// We assume the system was solvable to begin with, so we only look for
	// cycles that use the new edges.
	//
	// The new [constraint] `v1 + v2 <= k` just added the edges:
	// (v1) --k--> (-v2)
	// (v2) --k--> (-v1)
	//
	// Look for a path from (-v2) to (v1) with weight at most -k-1, as this
	// will complete a negative-weight cycle.

	// It suffices to do this once. We need not check for the converse path
	// (-v1) to (v2) because of the symmetry in the graph.
	//
	// Note that the graph symmetry is not a redundancy. Some cycles include
	// both of the new edges at once, so they must be added to the graph
	// beforehand.
	_goal = constraint.v2;
	_distanceToGoal = <SignedVariable, int>{};
	int targetWeight = -constraint.bound - 1;
	int pathWeight = _search(constraint.v1.negated, targetWeight, 0);
	return pathWeight != null && pathWeight <= targetWeight;
	}

	static const int MAX_DEPTH = 100;

	/// Returns the shortest path from [v1] to [_goal] (or any path shorter than
	/// [budget]), or `null` if no path exists.
	int _search(SignedVariable v1, int budget, int depth) {
	if (v1 == _goal && budget >= 0) return 0;

	// Disregard paths that use a lot of edges.
	// In extreme cases (e.g. hundreds of `push` calls or nested ifs) this can
	// get slow and/or overflow the stack. Most paths that matter are very
	// short (1-5 edges) with some occasional 10-30 length paths in math code.
	if (depth >= MAX_DEPTH) return null;

	// We found a cycle, but not the one we're looking for. If the constraint
	// system was solvable to being with, then this must be a positive-weight
	// cycle, and no shortest path goes through a positive-weight cycle.
	if (v1._isBeingVisited) return null;

	// Check if we have previously searched from here.
	if (_distanceToGoal.containsKey(v1)) {
	// We have already searched this node, return the cached answer.
	// Note that variables may explicitly map to null, so the double lookup
	// is necessary.
	return _distanceToGoal[v1];
	}

	v1._isBeingVisited = true;

	int shortestDistance = v1 == _goal ? 0 : null;
	for (Constraint c in v1._constraints) {
	SignedVariable v2 = c.v1 == v1 ? c.v2 : c.v1;
	int distance = _search(v2.negated, budget - c.bound, depth + 1);
	if (distance != null) {
	distance += c.bound; // Pay the cost of using the edge.
	if (distance <= budget) {
	// Success! We found a path that is short enough so return fast.
	// All recursive calls will now return immediately, so there is no
	// need to update distanceToGoal, but we need to clear the
	// beingVisited flag for the next query.
	v1._isBeingVisited = false;
	return distance;
	} else if (shortestDistance == null \|\| distance < shortestDistance) {
	shortestDistance = distance;
	}
	}
	}
	v1._isBeingVisited = false;
	_distanceToGoal[v1] = shortestDistance;
	return shortestDistance;
	}
	}