diff options
Diffstat (limited to 'Source/AIFramework/Polyhedra/LinearConstraintSystem.cs')
| -rw-r--r-- | Source/AIFramework/Polyhedra/LinearConstraintSystem.cs | 1376 |
1 files changed, 638 insertions, 738 deletions
diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs index e444b0ca..8e5fdf86 100644 --- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs +++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.cs @@ -3,33 +3,39 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
-namespace Microsoft.AbstractInterpretationFramework
-{
- using System.Collections;
- using System.Collections.Generic;
- using System.Diagnostics;
- using System;
- using Microsoft.SpecSharp.Collections;
- using Microsoft.Contracts;
- using Microsoft.Basetypes;
- using IMutableSet = Microsoft.Boogie.Set;
- using HashSet = Microsoft.Boogie.Set;
- using ISet = Microsoft.Boogie.Set;
-
- /// <summary>
- /// Represents a system of linear constraints (constraint/frame representations).
- /// </summary>
- public class LinearConstraintSystem
- {
+namespace Microsoft.AbstractInterpretationFramework {
+ using System.Collections;
+ using System.Collections.Generic;
+ using System.Diagnostics;
+ using System;
+ //using Microsoft.SpecSharp.Collections;
+ using System.Diagnostics.Contracts;
+ using Microsoft.Basetypes;
+ using IMutableSet = Microsoft.Boogie.Set;
+ using HashSet = Microsoft.Boogie.Set;
+ using ISet = Microsoft.Boogie.Set;
+
+ /// <summary>
+ /// Represents a system of linear constraints (constraint/frame representations).
+ /// </summary>
+ public class LinearConstraintSystem {
// --------------------------------------------------------------------------------------------------------
// ------------------ Data structure ----------------------------------------------------------------------
// --------------------------------------------------------------------------------------------------------
public /*maybe null*/ ArrayList /*LinearConstraint!*/ Constraints;
- /*maybe null*/ ArrayList /*FrameElement!*/ FrameVertices;
- /*maybe null*/ ArrayList /*FrameElement!*/ FrameRays;
- IMutableSet/*IVariable!*/! FrameDimensions;
- /*maybe null*/ ArrayList /*FrameElement!*/ FrameLines;
+ /*maybe null*/
+ ArrayList /*FrameElement!*/ FrameVertices;
+ /*maybe null*/
+ ArrayList /*FrameElement!*/ FrameRays;
+ IMutableSet/*IVariable!*//*!*/ FrameDimensions;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(FrameDimensions != null);
+ }
+
+ /*maybe null*/
+ ArrayList /*FrameElement!*/ FrameLines;
// Invariant: Either all of Constraints, FrameVertices, FrameRays, and FrameLines are
// null, or all are non-null.
// Invariant: Any dimension mentioned in Constraints, FrameVertices, FrameRays, or
@@ -37,36 +43,32 @@ namespace Microsoft.AbstractInterpretationFramework // The meaning of FrameDimensions is that for any dimension x not in FrameDimensions,
// there is an implicit line along dimension x (that is, (<x,1>)).
- void CheckInvariant()
- {
- if (Constraints == null)
- {
+ void CheckInvariant() {
+ if (Constraints == null) {
System.Diagnostics.Debug.Assert(FrameVertices == null);
System.Diagnostics.Debug.Assert(FrameRays == null);
System.Diagnostics.Debug.Assert(FrameLines == null);
System.Diagnostics.Debug.Assert(FrameDimensions.Count == 0);
- }
- else
- {
+ } else {
System.Diagnostics.Debug.Assert(FrameVertices != null);
System.Diagnostics.Debug.Assert(FrameRays != null);
System.Diagnostics.Debug.Assert(FrameLines != null);
- foreach (LinearConstraint! cc in Constraints)
- {
+ foreach (LinearConstraint/*!*/ cc in Constraints) {
+ Contract.Assert(cc != null);
#if FIXED_DESERIALIZER
- assert Forall{IVariable! var in cc.GetDefinedDimensions(); FrameDimensions.Contains(var)};
-#endif
- assert cc.coefficients.Count != 0;
+ Contract.Assert(Contract.ForAll(cc.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
+#endif
+ Contract.Assert(cc.coefficients.Count != 0);
}
- foreach (ArrayList /*FrameElement*/! FrameComponent in new ArrayList /*FrameElement*/ [] {FrameVertices, FrameRays, FrameLines})
- {
- foreach (FrameElement fe in FrameComponent)
- {
- if (fe == null) continue;
+ foreach (ArrayList /*FrameElement*//*!*/ FrameComponent in new ArrayList /*FrameElement*/ [] { FrameVertices, FrameRays, FrameLines }) {
+ Contract.Assert(FrameComponent != null);
+ foreach (FrameElement fe in FrameComponent) {
+ if (fe == null)
+ continue;
#if FIXED_DESERIALIZER
- assert Forall{IVariable! var in fe.GetDefinedDimensions(); FrameDimensions.Contains(var)};
-#endif
+ Contract.Assert(Contract.ForAll(fe.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
+#endif
}
}
}
@@ -81,10 +83,9 @@ namespace Microsoft.AbstractInterpretationFramework /// an unsatisfiable system of constraints.
/// </summary>
[NotDelayed]
- public LinearConstraintSystem()
- {
+ public LinearConstraintSystem() {
FrameDimensions = new HashSet /*IVariable!*/ ();
- base();
+ //:base();
CheckInvariant();
}
@@ -94,19 +95,20 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
/// <param name="cs"></param>
[NotDelayed]
- public LinearConstraintSystem(ArrayList /*LinearConstraint!*/! cs)
+ public LinearConstraintSystem(ArrayList /*LinearConstraint!*//*!*/ cs) {
+ Contract.Requires(cs != null);
#if BUG_159_HAS_BEEN_FIXED
- requires Forall{LinearConstraint! cc in cs; cc.coefficients.Count != 0};
+ Contract.Requires(Contract.ForAll(cs) , cc=> cc.coefficients.Count != 0);
#endif
- {
+
ArrayList constraints = new ArrayList /*LinearConstraint!*/ (cs.Count);
- foreach (LinearConstraint! cc in cs)
- {
+ foreach (LinearConstraint/*!*/ cc in cs) {
+ Contract.Assert(cc != null);
constraints.Add(cc);
}
Constraints = constraints;
FrameDimensions = new HashSet /*IVariable!*/ (); // to please compiler; this value will be overridden in the call to GenerateFrameConstraints below
- base();
+ //:base();
GenerateFrameFromConstraints();
SimplifyConstraints();
@@ -123,12 +125,13 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
/// <param name="v"></param>
[NotDelayed]
- LinearConstraintSystem(FrameElement! v)
- {
- IMutableSet! frameDims = v.GetDefinedDimensions();
+ LinearConstraintSystem(FrameElement/*!*/ v) {
+ Contract.Requires(v != null);
+ IMutableSet/*!*/ frameDims = v.GetDefinedDimensions();
+ Contract.Assert(frameDims != null);
ArrayList /*LinearConstraint!*/ constraints = new ArrayList /*LinearConstraint!*/ ();
- foreach (IVariable! dim in frameDims)
- {
+ foreach (IVariable/*!*/ dim in frameDims) {
+ Contract.Assert(dim != null);
LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.EQ);
lc.SetCoefficient(dim, Rational.ONE);
lc.rhs = v[dim];
@@ -144,12 +147,11 @@ namespace Microsoft.AbstractInterpretationFramework FrameRays = new ArrayList /*FrameElement*/ ();
FrameLines = new ArrayList /*FrameElement*/ ();
- base();
+ //:base();
CheckInvariant();
}
- void ChangeIntoBottom()
- {
+ void ChangeIntoBottom() {
Constraints = null;
FrameVertices = null;
FrameRays = null;
@@ -162,54 +164,47 @@ namespace Microsoft.AbstractInterpretationFramework // ------------------ Public operations and their support routines ----------------------------------------
// --------------------------------------------------------------------------------------------------------
- public bool IsBottom()
- {
+ public bool IsBottom() {
return Constraints == null;
}
- public bool IsTop()
- {
+ public bool IsTop() {
return Constraints != null && Constraints.Count == 0;
}
[Pure]
- public override string! ToString()
- {
- if (Constraints == null)
- {
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ if (Constraints == null) {
return "<bottom>";
- }
- else if (Constraints.Count == 0)
- {
+ } else if (Constraints.Count == 0) {
return "<top>";
- }
- else
- {
+ } else {
string z = null;
- foreach (LinearConstraint! lc in Constraints)
- {
+ foreach (LinearConstraint/*!*/ lc in Constraints) {
+ Contract.Assert(lc != null);
string s = lc.ToString();
- if (z == null)
- {
+ if (z == null) {
z = s;
- }
- else
- {
+ } else {
z += " AND " + s;
}
}
- assert z != null;
+ Contract.Assert(z != null);
return z;
}
}
- public ICollection<IVariable!>! FreeVariables()
- ensures result.IsReadOnly;
- {
- List<IVariable!> list = new List<IVariable!>();
- foreach (IVariable! v in FrameDimensions) { list.Add(v); }
- return (!)list.AsReadOnly();
+ public ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
+ Contract.Ensures(Contract.Result<ICollection<IVariable>>().IsReadOnly);
+ List<IVariable/*!*/> list = new List<IVariable/*!*/>();
+ foreach (IVariable/*!*/ v in FrameDimensions) {
+ Contract.Assert(v != null);
+ list.Add(v);
+ }
+ return cce.NonNull(list.AsReadOnly());
}
/// <summary>
@@ -217,8 +212,9 @@ namespace Microsoft.AbstractInterpretationFramework /// not required elsewhere in this class.
/// </summary>
/// <returns></returns>
- public IExpr! ConvertToExpression(ILinearExprFactory! factory)
- {
+ public IExpr/*!*/ ConvertToExpression(ILinearExprFactory/*!*/ factory) {
+ Contract.Requires(factory != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
if (this.Constraints == null) {
return factory.False;
}
@@ -227,12 +223,12 @@ namespace Microsoft.AbstractInterpretationFramework }
IExpr result = null;
- foreach (LinearConstraint! lc in Constraints)
- {
+ foreach (LinearConstraint/*!*/ lc in Constraints) {
+ Contract.Assert(lc != null);
IExpr conjunct = lc.ConvertToExpression(factory);
result = (result == null) ? conjunct : (IExpr)factory.And(conjunct, result);
}
- assert result != null;
+ Contract.Assert(result != null);
return result;
}
@@ -240,14 +236,11 @@ namespace Microsoft.AbstractInterpretationFramework /* IsSubset(): determines if 'lcs' is a subset of 'this'
* -- See Cousot/Halbwachs 1978, section
*/
- public bool IsSubset(LinearConstraintSystem! lcs)
- {
- if (lcs.IsBottom())
- {
+ public bool IsSubset(LinearConstraintSystem/*!*/ lcs) {
+ Contract.Requires(lcs != null);
+ if (lcs.IsBottom()) {
return true;
- }
- else if (this.IsBottom())
- {
+ } else if (this.IsBottom()) {
return false;
#if DEBUG
#else
@@ -256,11 +249,10 @@ namespace Microsoft.AbstractInterpretationFramework } else if (lcs.IsTop()) { // optimization -- this case not needed for correctness
return false;
#endif
- }
- else
- {
+ } else {
// phase 0: check if frame dimensions are a superset of the constraint dimensions
- ISet /*IVariable!*/! frameDims = lcs.GetDefinedDimensions();
+ ISet /*IVariable!*//*!*/ frameDims = lcs.GetDefinedDimensions();
+ Contract.Assert(frameDims != null);
#if DEBUG_PRINT
Console.WriteLine("DEBUG: IsSubset:");
Console.WriteLine(" --- this:");
@@ -269,14 +261,14 @@ namespace Microsoft.AbstractInterpretationFramework lcs.Dump();
Console.WriteLine(" ---");
#endif
- foreach (LinearConstraint! cc in (!)this.Constraints)
- {
+ foreach (LinearConstraint/*!*/ cc in cce.NonNull(this.Constraints)) {
+ Contract.Assert(cc != null);
#if DEBUG_PRINT
Console.WriteLine(" cc: {0}", cc);
Console.WriteLine(" cc.GetDefinedDimensions(): {0}", cc.GetDefinedDimensions());
#endif
- if (!forall{IVariable! var in cc.GetDefinedDimensions(); frameDims.Contains(var)})
- {
+
+ if (!Contract.ForAll(cc.GetDefinedDimensionsGeneric(), var => frameDims.Contains(var))) {
#if DEBUG_PRINT
Console.WriteLine(" ---> phase 0 subset violated, return false from IsSubset");
#endif
@@ -286,25 +278,20 @@ namespace Microsoft.AbstractInterpretationFramework }
// phase 1: check frame vertices against each constraint...
- foreach (FrameElement! v in (!)lcs.FrameVertices)
- {
- foreach (LinearConstraint! cc in this.Constraints)
- {
+ foreach (FrameElement/*!*/ v in cce.NonNull(lcs.FrameVertices)) {
+ Contract.Assert(v != null);
+ foreach (LinearConstraint/*!*/ cc in this.Constraints) {
+ Contract.Assert(cc != null);
Rational q = cc.EvaluateLhs(v);
- if (cc.Relation == LinearConstraint.ConstraintRelation.LE)
- {
- if (!(q <= cc.rhs))
- {
+ if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
+ if (!(q <= cc.rhs)) {
#if DEBUG_PRINT
Console.WriteLine(" ---> phase 1a subset violated, return false from IsSubset");
#endif
return false;
}
- }
- else
- {
- if (!(q == cc.rhs))
- {
+ } else {
+ if (!(q == cc.rhs)) {
#if DEBUG_PRINT
Console.WriteLine(" ---> phase 1b subset violated, return false from IsSubset");
#endif
@@ -333,27 +320,22 @@ namespace Microsoft.AbstractInterpretationFramework // a1*r1 + a2*r2 + ... + an*rn <= 0
// If the constraint is an equality constraint, we simply replace "<=" with "=="
// above.
- foreach (FrameElement! r in (!)lcs.FrameRays)
- {
+ foreach (FrameElement/*!*/ r in cce.NonNull(lcs.FrameRays)) {
+ Contract.Assert(r != null);
System.Diagnostics.Debug.Assert(r != null, "encountered a null ray...");
- foreach (LinearConstraint! cc in this.Constraints)
- {
+ foreach (LinearConstraint/*!*/ cc in this.Constraints) {
+ Contract.Assert(cc != null);
System.Diagnostics.Debug.Assert(cc != null, "encountered an null constraint...");
Rational q = cc.EvaluateLhs(r);
- if (cc.Relation == LinearConstraint.ConstraintRelation.LE)
- {
- if (q.IsPositive)
- {
+ if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
+ if (q.IsPositive) {
#if DEBUG_PRINT
Console.WriteLine(" ---> phase 2a subset violated, return false from IsSubset");
#endif
return false;
}
- }
- else
- {
- if (q.IsNonZero)
- {
+ } else {
+ if (q.IsNonZero) {
#if DEBUG_PRINT
Console.WriteLine(" ---> phase 2b subset violated, return false from IsSubset");
#endif
@@ -379,15 +361,14 @@ namespace Microsoft.AbstractInterpretationFramework // Putting (*) and (**) together, we conclude that we need to check:
// a1*L1 + a2*L2 + ... + an*Ln == 0
// If the constraint is an equality constraint, we end up with the same equation.
- foreach (FrameElement! line in (!)lcs.FrameLines)
- {
+ foreach (FrameElement/*!*/ line in cce.NonNull(lcs.FrameLines)) {
+ Contract.Assert(line != null);
System.Diagnostics.Debug.Assert(line != null, "encountered a null line...");
- foreach (LinearConstraint! cc in this.Constraints)
- {
+ foreach (LinearConstraint/*!*/ cc in this.Constraints) {
+ Contract.Assert(cc != null);
System.Diagnostics.Debug.Assert(cc != null, "encountered an null constraint...");
Rational q = cc.EvaluateLhs(line);
- if (q.IsNonZero)
- {
+ if (q.IsNonZero) {
#if DEBUG_PRINT
Console.WriteLine(" ---> phase 3 subset violated, return false from IsSubset");
#endif
@@ -402,10 +383,11 @@ namespace Microsoft.AbstractInterpretationFramework return true;
}
- public LinearConstraintSystem! Meet(LinearConstraintSystem! lcs)
- requires this.Constraints != null;
- requires lcs.Constraints != null;
- {
+ public LinearConstraintSystem/*!*/ Meet(LinearConstraintSystem/*!*/ lcs) {
+ Contract.Requires(lcs != null);
+ Contract.Requires((this.Constraints != null));
+ Contract.Requires((lcs.Constraints != null));
+ Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
ArrayList /*LinearConstraint*/ clist = new ArrayList(this.Constraints.Count + lcs.Constraints.Count);
clist.AddRange(this.Constraints);
clist.AddRange(lcs.Constraints);
@@ -436,43 +418,35 @@ namespace Microsoft.AbstractInterpretationFramework /// <param name="lcs"></param>
/// <returns></returns>
#if DEBUG_PRINT
- public LinearConstraintSystem JoinX(LinearConstraintSystem lcs)
+ public LinearConstraintSystem JoinX(LinearConstraintSystem lcs) {
#else
- public LinearConstraintSystem! Join(LinearConstraintSystem! lcs)
+ public LinearConstraintSystem/*!*/ Join(LinearConstraintSystem/*!*/ lcs) {
+ Contract.Requires(lcs != null);
+ Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
#endif
- {
- if (this.IsBottom())
- {
- return (!) lcs.Clone();
- }
- else if (lcs.IsBottom())
- {
- return (!) this.Clone();
- }
- else if (this.IsTop() || lcs.IsTop())
- {
+
+ if (this.IsBottom()) {
+ return cce.NonNull(lcs.Clone());
+ } else if (lcs.IsBottom()) {
+ return cce.NonNull(this.Clone());
+ } else if (this.IsTop() || lcs.IsTop()) {
return new LinearConstraintSystem(new ArrayList /*LinearConstraint*/ ());
- }
- else
- {
- LinearConstraintSystem! z;
+ } else {
+ LinearConstraintSystem/*!*/ z;
// Start from the "larger" of the two frames (this is just a heuristic measure intended
// to save work).
- assume this.FrameVertices != null;
- assume this.FrameRays != null;
- assume this.FrameLines != null;
- assume lcs.FrameVertices != null;
- assume lcs.FrameRays != null;
- assume lcs.FrameLines != null;
+ Contract.Assume(this.FrameVertices != null);
+ Contract.Assume(this.FrameRays != null);
+ Contract.Assume(this.FrameLines != null);
+ Contract.Assume(lcs.FrameVertices != null);
+ Contract.Assume(lcs.FrameRays != null);
+ Contract.Assume(lcs.FrameLines != null);
if (this.FrameVertices.Count + this.FrameRays.Count + this.FrameLines.Count - this.FrameDimensions.Count <
- lcs.FrameVertices.Count + lcs.FrameRays.Count + lcs.FrameLines.Count - lcs.FrameDimensions.Count)
- {
- z = (!) lcs.Clone();
+ lcs.FrameVertices.Count + lcs.FrameRays.Count + lcs.FrameLines.Count - lcs.FrameDimensions.Count) {
+ z = cce.NonNull(lcs.Clone());
lcs = this;
- }
- else
- {
- z = (!) this.Clone();
+ } else {
+ z = cce.NonNull(this.Clone());
}
#if DEBUG_PRINT
Console.WriteLine("DEBUG: LinearConstraintSystem.Join ---------------");
@@ -483,17 +457,16 @@ namespace Microsoft.AbstractInterpretationFramework #endif
// Start by explicating the implicit lines of z for the dimensions dims(lcs)-dims(z).
- foreach (IVariable! dim in lcs.FrameDimensions)
- {
- if (!z.FrameDimensions.Contains(dim))
- {
+ foreach (IVariable/*!*/ dim in lcs.FrameDimensions) {
+ Contract.Assert(dim != null);
+ if (!z.FrameDimensions.Contains(dim)) {
z.FrameDimensions.Add(dim);
FrameElement line = new FrameElement();
line.AddCoordinate(dim, Rational.ONE);
// Note: AddLine is not called (because the line already exists in z--it's just that
// it was represented implicitly). Instead, just tack the explicit representation onto
// FrameLines.
- assume z.FrameLines != null;
+ Contract.Assume(z.FrameLines != null);
z.FrameLines.Add(line);
#if DEBUG_PRINT
Console.WriteLine("Join: After explicating line: {0}", line);
@@ -503,24 +476,24 @@ namespace Microsoft.AbstractInterpretationFramework }
// Now, the vertices, rays, and lines can be added.
- foreach (FrameElement! v in lcs.FrameVertices)
- {
+ foreach (FrameElement/*!*/ v in lcs.FrameVertices) {
+ Contract.Assert(v != null);
z.AddVertex(v);
#if DEBUG_PRINT
Console.WriteLine("Join: After adding vertex: {0}", v);
z.Dump();
#endif
}
- foreach (FrameElement! r in lcs.FrameRays)
- {
+ foreach (FrameElement/*!*/ r in lcs.FrameRays) {
+ Contract.Assert(r != null);
z.AddRay(r);
#if DEBUG_PRINT
Console.WriteLine("Join: After adding ray: {0}", r);
z.Dump();
#endif
}
- foreach (FrameElement! l in lcs.FrameLines)
- {
+ foreach (FrameElement/*!*/ l in lcs.FrameLines) {
+ Contract.Assert(l != null);
z.AddLine(l);
#if DEBUG_PRINT
Console.WriteLine("Join: After adding line: {0}", l);
@@ -528,10 +501,9 @@ namespace Microsoft.AbstractInterpretationFramework #endif
}
// also add to z the implicit lines of lcs
- foreach (IVariable! dim in z.FrameDimensions)
- {
- if (!lcs.FrameDimensions.Contains(dim))
- {
+ foreach (IVariable/*!*/ dim in z.FrameDimensions) {
+ Contract.Assert(dim != null);
+ if (!lcs.FrameDimensions.Contains(dim)) {
// "dim" is a dimension that's explicit in "z" but implicit in "lcs"
FrameElement line = new FrameElement();
line.AddCoordinate(dim, Rational.ONE);
@@ -574,35 +546,30 @@ namespace Microsoft.AbstractInterpretationFramework #endif
#if DEBUG_PRINT
- public LinearConstraintSystem WidenX(LinearConstraintSystem lcs)
+ public LinearConstraintSystem WidenX(LinearConstraintSystem lcs){
#else
- public LinearConstraintSystem! Widen(LinearConstraintSystem! lcs)
-#endif
- {
- if (this.IsBottom())
- {
- return (!) lcs.Clone();
- }
- else if (lcs.IsBottom())
- {
- return (!) this.Clone();
- }
- else if (this.IsTop() || lcs.IsTop())
- {
+ public LinearConstraintSystem/*!*/ Widen(LinearConstraintSystem/*!*/ lcs) {
+ Contract.Requires(lcs != null);
+ Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
+#endif
+ if (this.IsBottom()) {
+ return cce.NonNull(lcs.Clone());
+ } else if (lcs.IsBottom()) {
+ return cce.NonNull(this.Clone());
+ } else if (this.IsTop() || lcs.IsTop()) {
return new LinearConstraintSystem(new ArrayList /*LinearConstraint*/ ());
}
// create new LCS, we will add only verified constraints to this...
ArrayList /*LinearConstraint*/ newConstraints = new ArrayList /*LinearConstraint*/ ();
- assume this.Constraints != null;
- foreach (LinearConstraint! ccX in this.Constraints)
- {
+ Contract.Assume(this.Constraints != null);
+ foreach (LinearConstraint/*!*/ ccX in this.Constraints) {
+ Contract.Assert(ccX != null);
LinearConstraint cc = ccX;
#if DEBUG_PRINT
Console.WriteLine("Widen checking: Starting to check constraint: {0}", cc);
#endif
- if (cc.IsConstant())
- {
+ if (cc.IsConstant()) {
// (Can this ever occur in the stable state of a LinearConstraintSystem? --KRML)
// constraint is unaffected by the frame components
#if DEBUG_PRINT
@@ -614,21 +581,17 @@ namespace Microsoft.AbstractInterpretationFramework // PHASE I: verify constraints against all frame vertices...
- foreach (FrameElement! vertex in (!)lcs.FrameVertices)
- {
+ foreach (FrameElement/*!*/ vertex in cce.NonNull(lcs.FrameVertices)) {
+ Contract.Assert(vertex != null);
Rational lhs = cc.EvaluateLhs(vertex);
- if (lhs > cc.rhs)
- {
+ if (lhs > cc.rhs) {
// the vertex does not satisfy the inequality <=
- if (cc.Relation == LinearConstraint.ConstraintRelation.LE)
- {
+ if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
#if DEBUG_PRINT
Console.WriteLine("Widen checking: throwing out because of vertex: {0}", vertex);
#endif
goto CHECK_NEXT_CONSTRAINT;
- }
- else
- {
+ } else {
// ... but it does satisfy the inequality >=
#if DEBUG_PRINT
Console.WriteLine("Widen checking: throwing out <= because of vertex: {0}", vertex);
@@ -638,9 +601,7 @@ namespace Microsoft.AbstractInterpretationFramework Console.WriteLine("Widen checking: left with constraint: {0}", cc);
#endif
}
- }
- else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ && lhs < cc.rhs)
- {
+ } else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ && lhs < cc.rhs) {
// the vertex does not satisfy the inequality >=, and the constraint is an equality constraint
#if DEBUG_PRINT
Console.WriteLine("Widen checking: throwing out >= because of vertex: {0}", vertex);
@@ -654,22 +615,18 @@ namespace Microsoft.AbstractInterpretationFramework // PHASE II: verify constraints against all frame rays...
- foreach (FrameElement! ray in (!)lcs.FrameRays)
- {
+ foreach (FrameElement/*!*/ ray in cce.NonNull(lcs.FrameRays)) {
+ Contract.Assert(ray != null);
// The following assumes the constraint to have some dimension with a non-zero coefficient
Rational lhs = cc.EvaluateLhs(ray);
- if (lhs.IsPositive)
- {
+ if (lhs.IsPositive) {
// the ray does not satisfy the inequality <=
- if (cc.Relation == LinearConstraint.ConstraintRelation.LE)
- {
+ if (cc.Relation == LinearConstraint.ConstraintRelation.LE) {
#if DEBUG_PRINT
Console.WriteLine("Widen checking: throwing out because of ray: {0}", ray);
#endif
goto CHECK_NEXT_CONSTRAINT;
- }
- else
- {
+ } else {
// ... but it does satisfy the inequality >=
#if DEBUG_PRINT
Console.WriteLine("Widen checking: throwing out <= because of ray: {0}", ray);
@@ -679,9 +636,7 @@ namespace Microsoft.AbstractInterpretationFramework Console.WriteLine("Widen checking: left with contraint: {0}", cc);
#endif
}
- }
- else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ && lhs.IsNegative)
- {
+ } else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ && lhs.IsNegative) {
// the ray does not satisfy the inequality >=, and the constraint is an equality constraint
#if DEBUG_PRINT
Console.WriteLine("Widen checking: throwing out >= because of ray: {0}", ray);
@@ -695,12 +650,11 @@ namespace Microsoft.AbstractInterpretationFramework // PHASE III: verify constraints against all frame lines...
- foreach (FrameElement! line in (!)lcs.FrameLines)
- {
+ foreach (FrameElement/*!*/ line in cce.NonNull(lcs.FrameLines)) {
+ Contract.Assert(line != null);
// The following assumes the constraint to have some dimension with a non-zero coefficient
Rational lhs = cc.EvaluateLhs(line);
- if (!lhs.IsZero)
- {
+ if (!lhs.IsZero) {
// The line satisfies neither the inequality <= nor the equality ==
#if DEBUG_PRINT
Console.WriteLine("Widen checking: throwing out because of line: {0}", line);
@@ -715,7 +669,8 @@ namespace Microsoft.AbstractInterpretationFramework #endif
newConstraints.Add(cc);
- CHECK_NEXT_CONSTRAINT: {}
+ CHECK_NEXT_CONSTRAINT: {
+ }
#if DEBUG_PRINT
Console.WriteLine("Widen checking: done with that constraint"); #endif
@@ -725,8 +680,8 @@ namespace Microsoft.AbstractInterpretationFramework }
#if DEBUG_PRINT
- public LinearConstraintSystem Project(IVariable! dim)
- {
+ public LinearConstraintSystem Project(IVariable/*!*/ dim){
+Contract.Requires(dim != null);
Console.WriteLine("===================================================================================");
Console.WriteLine("DEBUG: Project(dim={0})", dim);
Console.WriteLine("Project: this=");
@@ -741,19 +696,24 @@ namespace Microsoft.AbstractInterpretationFramework #endif
#if DEBUG_PRINT
- public LinearConstraintSystem ProjectX(IVariable! dim)
+ public LinearConstraintSystem ProjectX(IVariable/*!*/ dim){Contract.Requires(dim != null);Contract.Requires(this.Constraints != null);
#else
- public LinearConstraintSystem! Project(IVariable! dim)
+ public LinearConstraintSystem/*!*/ Project(IVariable/*!*/ dim) {
+ Contract.Requires(dim != null);
+ Contract.Requires(this.Constraints != null);
+ Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
#endif
- requires this.Constraints != null;
- {
- ArrayList /*LinearConstraint!*/! cc = Project(dim, Constraints);
+
+
+ ArrayList /*LinearConstraint!*//*!*/ cc = Project(dim, Constraints);
+ Contract.Assert(cc != null);
return new LinearConstraintSystem(cc);
}
#if DEBUG_PRINT
- public LinearConstraintSystem Rename(IVariable! oldName, IVariable! newName)
- {
+ public LinearConstraintSystem Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName){
+Contract.Requires(newName != null);
+Contract.Requires(oldName != null);
Console.WriteLine("===================================================================================");
Console.WriteLine("DEBUG: Rename(oldName={0}, newName={1})", oldName, newName);
Console.WriteLine("Rename: this=");
@@ -768,45 +728,49 @@ namespace Microsoft.AbstractInterpretationFramework #endif
#if DEBUG_PRINT
- public LinearConstraintSystem RenameX(IVariable! oldName, IVariable! newName)
+ public LinearConstraintSystem RenameX(IVariable/*!*/ oldName, IVariable/*!*/ newName){Contract.Requires(oldName != null);Contract.Requires(newName != null);
#else
- public LinearConstraintSystem! Rename(IVariable! oldName, IVariable! newName)
+ public LinearConstraintSystem/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+ Contract.Requires(oldName != null);
+ Contract.Requires(newName != null);
+ Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
#endif
- {
- if (this.Constraints == null)
- {
+ if (this.Constraints == null) {
System.Diagnostics.Debug.Assert(this.FrameVertices == null);
System.Diagnostics.Debug.Assert(this.FrameRays == null);
System.Diagnostics.Debug.Assert(this.FrameLines == null);
return this;
}
- IMutableSet /*IVariable!*/! dims = this.FrameDimensions;
- if (!dims.Contains(oldName))
- {
+ IMutableSet /*IVariable!*//*!*/ dims = this.FrameDimensions;
+ Contract.Assert(dims != null);
+ if (!dims.Contains(oldName)) {
return this;
}
LinearConstraintSystem z = new LinearConstraintSystem();
- z.FrameDimensions = (HashSet! /*IVariable!*/)dims.Clone();
+ z.FrameDimensions = cce.NonNull((HashSet/*!*/ /*IVariable!*/)dims.Clone());
z.FrameDimensions.Remove(oldName);
z.FrameDimensions.Add(newName);
z.Constraints = new ArrayList /*LinearConstraint!*/ (this.Constraints.Count);
- foreach (LinearConstraint! lc in (!)this.Constraints)
- {
+ foreach (LinearConstraint/*!*/ lc in cce.NonNull(this.Constraints)) {
+ Contract.Assert(lc != null);
z.Constraints.Add(lc.Rename(oldName, newName));
}
- z.FrameVertices = RenameInFE((!)this.FrameVertices, oldName, newName);
- z.FrameRays = RenameInFE((!)this.FrameRays, oldName, newName);
- z.FrameLines = RenameInFE((!)this.FrameLines, oldName, newName);
+ z.FrameVertices = RenameInFE(cce.NonNull(this.FrameVertices), oldName, newName);
+ z.FrameRays = RenameInFE(cce.NonNull(this.FrameRays), oldName, newName);
+ z.FrameLines = RenameInFE(cce.NonNull(this.FrameLines), oldName, newName);
return z;
}
- static ArrayList /*FrameElement*/ RenameInFE(ArrayList! /*FrameElement*/ list, IVariable! oldName, IVariable! newName)
- {
- ArrayList/*FrameElement!*/! z = new ArrayList/*FrameElement!*/ (list.Count);
- foreach (FrameElement! fe in list)
- {
+ static ArrayList /*FrameElement*/ RenameInFE(ArrayList/*!*/ /*FrameElement*/ list, IVariable/*!*/ oldName, IVariable/*!*/ newName) {
+ Contract.Requires(list != null);
+ Contract.Requires(newName != null);
+ Contract.Requires(oldName != null);
+ ArrayList/*FrameElement!*//*!*/ z = new ArrayList/*FrameElement!*/ (list.Count);
+ Contract.Assert(z != null);
+ foreach (FrameElement/*!*/ fe in list) {
+ Contract.Assert(fe != null);
z.Add(fe.Rename(oldName, newName));
}
System.Diagnostics.Debug.Assert(z.Count == list.Count);
@@ -824,88 +788,73 @@ namespace Microsoft.AbstractInterpretationFramework /// <param name="dim"></param>
/// <param name="constraints"></param>
/// <returns></returns>
- static ArrayList /*LinearConstraint!*/! Project(IVariable! dim, ArrayList /*LinearConstraint!*/! constraints)
- {
+ static ArrayList /*LinearConstraint!*//*!*/ Project(IVariable/*!*/ dim, ArrayList /*LinearConstraint!*//*!*/ constraints) {
+ Contract.Requires(constraints != null);
+ Contract.Requires(dim != null);
+ Contract.Ensures(Contract.Result<ArrayList>() != null);
// Sort the inequality constaints into ones where dimension "dim" is 0, negative, and
// positive, respectively. Put equality constraints with a non-0 "dim" into "eq".
- ArrayList /*LinearConstraint!*/! final = new ArrayList /*LinearConstraint!*/ ();
- ArrayList /*LinearConstraint!*/! negative = new ArrayList /*LinearConstraint!*/ ();
- ArrayList /*LinearConstraint!*/! positive = new ArrayList /*LinearConstraint!*/ ();
- ArrayList /*LinearConstraint!*/! eq = new ArrayList /*LinearConstraint!*/ ();
- foreach (LinearConstraint! cc in constraints)
- {
+ ArrayList /*LinearConstraint!*//*!*/ final = new ArrayList /*LinearConstraint!*/ ();
+ ArrayList /*LinearConstraint!*//*!*/ negative = new ArrayList /*LinearConstraint!*/ ();
+ ArrayList /*LinearConstraint!*//*!*/ positive = new ArrayList /*LinearConstraint!*/ ();
+ ArrayList /*LinearConstraint!*//*!*/ eq = new ArrayList /*LinearConstraint!*/ ();
+ foreach (LinearConstraint/*!*/ cc in constraints) {
+ Contract.Assert(cc != null);
Rational coeff = cc[dim];
- if (coeff.IsZero)
- {
- LinearConstraint lc = (!) cc.Clone();
- if (!lc.IsConstant())
- {
+ if (coeff.IsZero) {
+ LinearConstraint lc = cce.NonNull(cc.Clone());
+ if (!lc.IsConstant()) {
lc.RemoveDimension(dim);
final.Add(lc);
}
- }
- else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ)
- {
+ } else if (cc.Relation == LinearConstraint.ConstraintRelation.EQ) {
eq.Add(cc);
- }
- else if (coeff.IsNegative)
- {
+ } else if (coeff.IsNegative) {
negative.Add(cc);
- }
- else
- {
+ } else {
System.Diagnostics.Debug.Assert(coeff.IsPositive);
positive.Add(cc);
- }
+ }
}
- if (eq.Count != 0)
- {
- LinearConstraint eqConstraint = (LinearConstraint!)eq[eq.Count-1];
- eq.RemoveAt(eq.Count-1);
+ if (eq.Count != 0) {
+ LinearConstraint eqConstraint = (LinearConstraint/*!*/)cce.NonNull(eq[eq.Count - 1]);
+ eq.RemoveAt(eq.Count - 1);
Rational eqC = -eqConstraint[dim];
- foreach (ArrayList /*LinearConstraint!*/! list in new ArrayList[]{eq, negative, positive})
- {
- foreach (LinearConstraint! lcX in list)
- {
- LinearConstraint lc = (!) lcX.Clone();
- lc.AddMultiple(lc[dim]/eqC, eqConstraint);
+ foreach (ArrayList /*LinearConstraint!*/ list in new ArrayList[] { eq, negative, positive }) {
+ Contract.Assert(list != null);
+ foreach (LinearConstraint/*!*/ lcX in list) {
+ Contract.Assert(lcX != null);
+ LinearConstraint lc = cce.NonNull(lcX.Clone());
+ lc.AddMultiple(lc[dim] / eqC, eqConstraint);
System.Diagnostics.Debug.Assert(lc[dim].IsZero);
- if (!lc.IsConstant())
- {
+ if (!lc.IsConstant()) {
lc.RemoveDimension(dim);
final.Add(lc);
- }
- else
- {
+ } else {
System.Diagnostics.Debug.Assert(lc.IsConstantSatisfiable());
}
}
}
- }
- else
- {
+ } else {
// Consider all pairs of constraints with (negative,positive) coefficients of "dim".
- foreach (LinearConstraint! cn in negative)
- {
+ foreach (LinearConstraint/*!*/ cn in negative) {
+ Contract.Assert(cn != null);
Rational dn = -cn[dim];
System.Diagnostics.Debug.Assert(dn.IsNonNegative);
- foreach (LinearConstraint! cp in positive)
- {
+ foreach (LinearConstraint/*!*/ cp in positive) {
+ Contract.Assert(cp != null);
Rational dp = cp[dim];
LinearConstraint lc = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
lc.AddMultiple(dn, cp);
lc.AddMultiple(dp, cn);
System.Diagnostics.Debug.Assert(lc[dim].IsZero);
- if (!lc.IsConstant())
- {
+ if (!lc.IsConstant()) {
lc.RemoveDimension(dim);
final.Add(lc);
- }
- else
- {
+ } else {
System.Diagnostics.Debug.Assert(lc.IsConstantSatisfiable());
}
}
@@ -922,17 +871,15 @@ namespace Microsoft.AbstractInterpretationFramework ///
/// If the set of Constraints is unsatisfiable, then "this" is changed into Bottom.
/// </summary>
- void GenerateFrameFromConstraints()
- {
- if (Constraints == null)
- {
+ void GenerateFrameFromConstraints() {
+ if (Constraints == null) {
FrameVertices = null;
FrameRays = null;
FrameLines = null;
FrameDimensions = new HashSet /*IVariable!*/ ();
return;
}
-
+
// Step 1 (see Cousot and Halbwachs, section 3.4.3): create a Simplex Tableau.
#if DEBUG_PRINT
Console.WriteLine("DEBUG: --- GenerateFrameFromConstraint ---");
@@ -964,8 +911,7 @@ namespace Microsoft.AbstractInterpretationFramework Console.WriteLine("Tableau after Step 3:");
tableau.Dump();
#endif
- if (!tableau.IsFeasibleBasis)
- {
+ if (!tableau.IsFeasibleBasis) {
// The polyhedron is empty (according to Cousot and Halbwachs)
ChangeIntoBottom();
return;
@@ -974,29 +920,25 @@ namespace Microsoft.AbstractInterpretationFramework FrameVertices = new ArrayList /*FrameElement*/ ();
FrameRays = new ArrayList /*FrameElement*/ ();
FrameLines = new ArrayList /*FrameElement*/ ();
- if (FrameDimensions.Count == 0)
- {
+ if (FrameDimensions.Count == 0) {
// top element
return;
}
- if (tableau.AllInitialVarsInBasis)
- {
+ if (tableau.AllInitialVarsInBasis) {
// All initial variables are in basis; there are no lines.
#if DEBUG_PRINT
Console.WriteLine("Tableau after Steps 2 and 3 (all initial variables in basis):");
tableau.Dump();
#endif
- }
- else
- {
+ } else {
// There are lines
#if DEBUG_PRINT
Console.WriteLine("Tableau after Steps 2 and 3 (NOT all initial variables in basis--there are lines):");
tableau.Dump();
#endif
// Step 4.2: Pick out the lines, then produce the tableau for a new polyhedron without those lines.
- ArrayList /*LinearConstraint*/ moreConstraints = (ArrayList! /*LinearConstraint*/) Constraints.Clone();
+ ArrayList /*LinearConstraint*/ moreConstraints = cce.NonNull((ArrayList/*!*/ /*LinearConstraint*/)Constraints.Clone());
tableau.ProduceLines(FrameLines, moreConstraints);
tableau = new SimplexTableau(moreConstraints);
#if DEBUG_PRINT
@@ -1034,35 +976,33 @@ namespace Microsoft.AbstractInterpretationFramework #endif
}
- class LambdaDimension : IVariable
- {
+ class LambdaDimension : IVariable {
readonly int id;
static int count = 0;
/// <summary>
/// Return the name of the variable
/// </summary>
- public string! Name
- {
- get
- {
+ public string Name {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+
return this.ToString();
}
- }
+ }
- public LambdaDimension()
- {
+ public LambdaDimension() {
id = count;
count++;
}
[Pure]
- public override string! ToString()
- {
+ public override string/*!*/ ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
return "lambda" + id;
}
[Pure]
- public object DoVisit(ExprVisitor! visitor)
- {
+ public object DoVisit(ExprVisitor/*!*/ visitor) {
+ Contract.Requires(visitor != null);
return visitor.VisitVariable(this);
}
}
@@ -1076,9 +1016,9 @@ namespace Microsoft.AbstractInterpretationFramework /// Assumes Constraints (and the frame fields) to be non-null.
/// </summary>
/// <param name="vertex"></param>
- void AddVertex(FrameElement! vertex)
- requires this.FrameVertices != null;
- {
+ void AddVertex(FrameElement/*!*/ vertex) {
+ Contract.Requires(vertex != null);
+ Contract.Requires(this.FrameVertices != null);
#if DEBUG_PRINT
Console.WriteLine("DEBUG: AddVertex called on {0}", vertex);
Console.WriteLine(" Initial constraints:");
@@ -1089,11 +1029,11 @@ namespace Microsoft.AbstractInterpretationFramework FrameVertices.Add(vertex.Clone());
#if FIXED_DESERIALIZER
- assert Forall{IVariable! var in vertex.GetDefinedDimensions(); FrameDimensions.Contains(var)};
-#endif
+ Contract.Assert(Contract.ForAll(vertex.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
+#endif
// We use a new temporary dimension.
- IVariable! lambda = new LambdaDimension();
+ IVariable/*!*/ lambda = new LambdaDimension();
// We change the constraints A*X <= B into
// A*X + (A*vector - B)*lambda <= A*vector.
@@ -1109,8 +1049,8 @@ namespace Microsoft.AbstractInterpretationFramework // = { A*vector is a row vector whose every row i is the dot-product of
// row i of A with the column vector "vector" }
// A[k]*vector - B[k]
- foreach (LinearConstraint! cc in (!)Constraints)
- {
+ foreach (LinearConstraint/*!*/ cc in cce.NonNull(Constraints)) {
+ Contract.Assert(cc != null);
Rational d = cc.EvaluateLhs(vertex);
cc.SetCoefficient(lambda, d - cc.rhs);
cc.rhs = d;
@@ -1153,9 +1093,9 @@ namespace Microsoft.AbstractInterpretationFramework /// Assumes Constraints (and the frame fields) to be non-null.
/// </summary>
/// <param name="ray"></param>
- void AddRay(FrameElement! ray)
- requires this.FrameRays != null;
- {
+ void AddRay(FrameElement/*!*/ ray) {
+ Contract.Requires(ray != null);
+ Contract.Requires(this.FrameRays != null);
#if DEBUG_PRINT
Console.WriteLine("DEBUG: AddRay called on {0}", ray);
Console.WriteLine(" Initial constraints:");
@@ -1166,11 +1106,11 @@ namespace Microsoft.AbstractInterpretationFramework FrameRays.Add(ray.Clone());
#if FIXED_DESERIALIZER
- assert Forall{IVariable! var in ray.GetDefinedDimensions(); FrameDimensions.Contains(var)};
-#endif
+ Contract.Assert(Contract.ForAll(ray.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
+#endif
// We use a new temporary dimension.
- IVariable! lambda = new LambdaDimension();
+ IVariable/*!*/ lambda = new LambdaDimension();
// We change the constraints A*X <= B into
// A*X - (A*ray)*lambda <= B.
@@ -1183,8 +1123,8 @@ namespace Microsoft.AbstractInterpretationFramework // = { A*ray is a row vector whose every row i is the dot-product of
// row i of A with the column vector "ray" }
// A[k]*ray
- foreach (LinearConstraint! cc in (!)Constraints)
- {
+ foreach (LinearConstraint/*!*/ cc in cce.NonNull(Constraints)) {
+ Contract.Assert(cc != null);
Rational d = cc.EvaluateLhs(ray);
cc.SetCoefficient(lambda, -d);
}
@@ -1221,9 +1161,9 @@ namespace Microsoft.AbstractInterpretationFramework /// Assumes Constraints (and the frame fields) to be non-null.
/// </summary>
/// <param name="line"></param>
- void AddLine(FrameElement! line)
- requires this.FrameLines != null;
- {
+ void AddLine(FrameElement/*!*/ line) {
+ Contract.Requires(line != null);
+ Contract.Requires(this.FrameLines != null);
// Note: The code for AddLine is identical to that of AddRay, except the AddLine
// does not introduce the constraint 0 <= lambda. (One could imagine sharing the
// code between AddRay and AddLine.)
@@ -1237,11 +1177,11 @@ namespace Microsoft.AbstractInterpretationFramework FrameLines.Add(line.Clone());
#if FIXED_DESERIALIZER
- assert Forall{IVariable! var in line.GetDefinedDimensions(); FrameDimensions.Contains(var)};
-#endif
+ Contract.Assert(Contract.ForAll(line.GetDefinedDimensions() , var=> FrameDimensions.Contains(var)));
+#endif
// We use a new temporary dimension.
- IVariable! lambda = new LambdaDimension();
+ IVariable/*!*/ lambda = new LambdaDimension();
// We change the constraints A*X <= B into
// A*X - (A*line)*lambda <= B.
@@ -1254,8 +1194,8 @@ namespace Microsoft.AbstractInterpretationFramework // = { A*line is a row vector whose every row i is the dot-product of
// row i of A with the column vector "line" }
// A[k]*line
- foreach (LinearConstraint! cc in (!)Constraints)
- {
+ foreach (LinearConstraint/*!*/ cc in cce.NonNull(Constraints)) {
+ Contract.Assert(cc != null);
Rational d = cc.EvaluateLhs(line);
cc.SetCoefficient(lambda, -d);
}
@@ -1278,17 +1218,15 @@ namespace Microsoft.AbstractInterpretationFramework #endif
}
- ISet /*IVariable!*/! GetDefinedDimensions()
- {
- HashSet /*IVariable!*/! dims = new HashSet /*IVariable!*/ ();
- foreach (ArrayList p in new ArrayList[]{FrameVertices, FrameRays, FrameLines})
- {
- if (p != null)
- {
- foreach (FrameElement! element in p)
- {
- foreach (IVariable! dim in element.GetDefinedDimensions())
- {
+ ISet /*IVariable!*//*!*/ GetDefinedDimensions() {
+ Contract.Ensures(Contract.Result<ISet>() != null);
+ HashSet /*IVariable!*//*!*/ dims = new HashSet /*IVariable!*/ ();
+ foreach (ArrayList p in new ArrayList[] { FrameVertices, FrameRays, FrameLines }) {
+ if (p != null) {
+ foreach (FrameElement/*!*/ element in p) {
+ Contract.Assert(element != null);
+ foreach (IVariable/*!*/ dim in element.GetDefinedDimensions()) {
+ Contract.Assert(dim != null);
dims.Add(dim);
}
}
@@ -1304,19 +1242,22 @@ namespace Microsoft.AbstractInterpretationFramework /// <summary>
/// Uses the Constraints to simplify the frame. See section 3.4.4 of Cousot and Halbwachs.
/// </summary>
- void SimplifyFrame()
- requires this.Constraints != null;
- {
- SimplificationStatus[]! status;
+ void SimplifyFrame() {
+ Contract.Requires(this.Constraints != null);
+ SimplificationStatus[]/*!*/ status;
- SimplifyFrameElements((!)FrameVertices, true, Constraints, out status);
+ SimplifyFrameElements(cce.NonNull(FrameVertices), true, Constraints, out status);
RemoveIrrelevantFrameElements(FrameVertices, status, null);
- SimplifyFrameElements((!)FrameRays, false, Constraints, out status);
+ SimplifyFrameElements(cce.NonNull(FrameRays), false, Constraints, out status);
RemoveIrrelevantFrameElements(FrameRays, status, FrameLines);
}
- enum SimplificationStatus { Irrelevant, Relevant, More };
+ enum SimplificationStatus {
+ Irrelevant,
+ Relevant,
+ More
+ };
/// <summary>
/// For each i, sets status[i] to:
@@ -1330,32 +1271,26 @@ namespace Microsoft.AbstractInterpretationFramework /// <param name="vertices">true if "ff" contains vertices; false if "ff" contains rays</param>
/// <param name="constraints"></param>
/// <param name="status"></param>
- static void SimplifyFrameElements(ArrayList! /*FrameElement*/ ff, bool vertices,
- ArrayList! /*LinearConstraint*/ constraints,
- out SimplificationStatus[]! status)
- {
+ static void SimplifyFrameElements(ArrayList/*!*/ /*FrameElement*/ ff, bool vertices, ArrayList/*!*/ /*LinearConstraint*/ constraints, out SimplificationStatus[]/*!*/ status) {
+ Contract.Requires(ff != null);
+ Contract.Requires(constraints != null);
+ Contract.Requires(Contract.ValueAtReturn(out status) != null);
status = new SimplificationStatus[ff.Count];
bool[,] sat = new bool[ff.Count, constraints.Count];
- for (int i = 0; i < ff.Count; i++)
- {
- FrameElement f = (FrameElement!)ff[i];
+ for (int i = 0; i < ff.Count; i++) {
+ FrameElement f = (FrameElement/*!*/)cce.NonNull(ff[i]);
int cnt = 0;
- for (int c = 0; c < constraints.Count; c++)
- {
- LinearConstraint lc = (LinearConstraint!)constraints[c];
+ for (int c = 0; c < constraints.Count; c++) {
+ LinearConstraint lc = (LinearConstraint/*!*/)cce.NonNull(constraints[c]);
bool s = lc.IsSaturatedBy(f, vertices);
- if (s)
- {
- sat[i,c] = true;
+ if (s) {
+ sat[i, c] = true;
cnt++;
}
}
- if (!vertices && cnt == constraints.Count)
- {
+ if (!vertices && cnt == constraints.Count) {
status[i] = SimplificationStatus.More;
- }
- else
- {
+ } else {
status[i] = SimplificationStatus.Relevant;
}
}
@@ -1368,81 +1303,65 @@ namespace Microsoft.AbstractInterpretationFramework /// </summary>
/// <param name="sat"></param>
/// <param name="status"></param>
- static void CheckPairSimplifications(bool[,]! sat, SimplificationStatus[]! status)
- requires sat.GetLength(0) == status.Length;
- {
+ static void CheckPairSimplifications(bool[,]/*!*/ sat, SimplificationStatus[]/*!*/ status) {
+ Contract.Requires(status != null);
+ Contract.Requires(sat != null);
+ Contract.Requires(sat.GetLength(0) == status.Length);
int M = sat.GetLength(0);
int N = sat.GetLength(1);
- for (int i = 0; i < M-1; i++)
- {
- if (status[i] != SimplificationStatus.Relevant)
- {
+ for (int i = 0; i < M - 1; i++) {
+ if (status[i] != SimplificationStatus.Relevant) {
continue;
}
- for (int j = i+1; j < M; j++)
- {
- if (status[j] != SimplificationStatus.Relevant)
- {
+ for (int j = i + 1; j < M; j++) {
+ if (status[j] != SimplificationStatus.Relevant) {
continue;
}
// check (sat[i,*] <= sat[j,*]) and (sat[i,*] >= sat[j,*])
int cmp = 0; // -1: (sat[i,*] <= sat[j,*]), 0: equal, 1: (sat[i,*] >= sat[j,*])
- for (int c = 0; c < N; c++)
- {
- if (cmp < 0)
- {
- if (sat[i,c] && !sat[j,c])
- {
+ for (int c = 0; c < N; c++) {
+ if (cmp < 0) {
+ if (sat[i, c] && !sat[j, c]) {
// incomparable
goto NEXT_PAIR;
}
- }
- else if (0 < cmp)
- {
- if (!sat[i,c] && sat[j,c])
- {
+ } else if (0 < cmp) {
+ if (!sat[i, c] && sat[j, c]) {
// incomparable
goto NEXT_PAIR;
}
- }
- else if (sat[i,c] != sat[j,c])
- {
- if (!sat[i,c])
- {
+ } else if (sat[i, c] != sat[j, c]) {
+ if (!sat[i, c]) {
cmp = -1;
- }
- else
- {
+ } else {
cmp = 1;
}
}
}
- if (cmp <= 0)
- {
+ if (cmp <= 0) {
// sat[i,*] <= sat[j,*] holds, so mark i as irrelevant
status[i] = SimplificationStatus.Irrelevant;
goto NEXT_OUTER;
- }
- else
- {
+ } else {
// sat[i,*] >= sat[j,*] holds, so mark j as irrelevant
status[j] = SimplificationStatus.Irrelevant;
}
- NEXT_PAIR: {}
+ NEXT_PAIR: {
+ }
+ }
+ NEXT_OUTER: {
}
- NEXT_OUTER: {}
}
}
- static void RemoveIrrelevantFrameElements(ArrayList! /*FrameElement*/ ff, SimplificationStatus[]! status,
- /*maybe null*/ ArrayList /*FrameElement*/ lines)
- requires ff.Count == status.Length;
- {
- for (int j = ff.Count - 1; 0 <= j; j--)
- {
- switch (status[j])
- {
+ static void RemoveIrrelevantFrameElements(ArrayList/*!*/ /*FrameElement*/ ff, SimplificationStatus[]/*!*/ status,
+ /*maybe null*/ ArrayList /*FrameElement*/ lines) {
+ Contract.Requires(ff != null);
+ Contract.Requires(status != null);
+ Contract.Requires(ff.Count == status.Length);
+ for (int j = ff.Count - 1; 0 <= j; j--) {
+ switch (status[j]) {
case SimplificationStatus.Relevant:
break;
case SimplificationStatus.Irrelevant:
@@ -1458,7 +1377,7 @@ namespace Microsoft.AbstractInterpretationFramework Console.WriteLine("Changing ray into line: {0}", f);
#endif
ff.RemoveAt(j);
- assert lines != null;
+ Contract.Assert(lines != null);
lines.Add(f);
break;
}
@@ -1471,55 +1390,45 @@ namespace Microsoft.AbstractInterpretationFramework /// Note: This code does not necessarily eliminate all irrelevant equalities; Cousot and
/// Halbwachs only claim that the technique eliminates all irrelevant inequalities.
/// </summary>
- void SimplifyConstraints()
- {
- if (Constraints == null)
- {
+ void SimplifyConstraints() {
+ if (Constraints == null) {
return;
}
- assume this.FrameVertices != null;
- assume this.FrameRays != null;
+ Contract.Assume(this.FrameVertices != null);
+ Contract.Assume(this.FrameRays != null);
SimplificationStatus[] status = new SimplificationStatus[Constraints.Count];
- /*readonly*/ int feCount = FrameVertices.Count + FrameRays.Count;
+ /*readonly*/
+ int feCount = FrameVertices.Count + FrameRays.Count;
// Create a table that keeps track of which constraints are satisfied by which vertices and rays
bool[,] sat = new bool[Constraints.Count, FrameVertices.Count + FrameRays.Count];
- for (int i = 0; i < Constraints.Count; i++)
- {
+ for (int i = 0; i < Constraints.Count; i++) {
status[i] = SimplificationStatus.Relevant;
- LinearConstraint lc = (LinearConstraint!)Constraints[i];
+ LinearConstraint lc = (LinearConstraint/*!*/)cce.NonNull(Constraints[i]);
int cnt = 0; // number of vertices and rays that saturate lc
- for (int j = 0; j < FrameVertices.Count; j++)
- {
- FrameElement vertex = (FrameElement!)FrameVertices[j];
- if (lc.IsSaturatedBy(vertex, true))
- {
- sat[i,j] = true;
+ for (int j = 0; j < FrameVertices.Count; j++) {
+ FrameElement vertex = (FrameElement/*!*/)cce.NonNull(FrameVertices[j]);
+ if (lc.IsSaturatedBy(vertex, true)) {
+ sat[i, j] = true;
cnt++;
}
}
- if (cnt == 0)
- {
+ if (cnt == 0) {
// no vertex saturates the constraint, so the constraint is irrelevant
status[i] = SimplificationStatus.Irrelevant;
continue;
}
- for (int j = 0; j < FrameRays.Count; j++)
- {
- FrameElement ray = (FrameElement!)FrameRays[j];
- if (lc.IsSaturatedBy(ray, false))
- {
+ for (int j = 0; j < FrameRays.Count; j++) {
+ FrameElement ray = (FrameElement/*!*/)cce.NonNull(FrameRays[j]);
+ if (lc.IsSaturatedBy(ray, false)) {
sat[i, FrameVertices.Count + j] = true;
cnt++;
}
}
- if (cnt == feCount)
- {
+ if (cnt == feCount) {
status[i] = SimplificationStatus.More;
- }
- else
- {
+ } else {
// Cousot and Halbwachs says that all equalities are found in the way we just tested.
// If I understand that right, then we should not get here if the constraint is an
// equality constraint. The following assertion tests my understanding. --KRML
@@ -1530,10 +1439,8 @@ namespace Microsoft.AbstractInterpretationFramework CheckPairSimplifications(sat, status);
// Finally, make the changes to the list of constraints
- for (int i = Constraints.Count - 1; 0 <= i; i--)
- {
- switch (status[i])
- {
+ for (int i = Constraints.Count - 1; 0 <= i; i--) {
+ switch (status[i]) {
case SimplificationStatus.Relevant:
break;
case SimplificationStatus.Irrelevant:
@@ -1543,9 +1450,8 @@ namespace Microsoft.AbstractInterpretationFramework Constraints.RemoveAt(i);
break;
case SimplificationStatus.More:
- LinearConstraint lc = (LinearConstraint!)Constraints[i];
- if (lc.Relation == LinearConstraint.ConstraintRelation.LE)
- {
+ LinearConstraint lc = (LinearConstraint/*!*/)cce.NonNull(Constraints[i]);
+ if (lc.Relation == LinearConstraint.ConstraintRelation.LE) {
#if DEBUG_PRINT
Console.WriteLine("Converting the following constraint into an equality: {0}", lc);
#endif
@@ -1555,9 +1461,10 @@ namespace Microsoft.AbstractInterpretationFramework break;
}
}
-
- foreach (LinearConstraint! lc in Constraints) {
- lc.Normalize();
+
+ foreach (LinearConstraint/*!*/ lc in Constraints) {
+ Contract.Assert(lc != null);
+ lc.Normalize();
}
}
@@ -1565,292 +1472,285 @@ namespace Microsoft.AbstractInterpretationFramework // ------------------ Cloning routines --------------------------------------------------------------------
// --------------------------------------------------------------------------------------------------------
- public LinearConstraintSystem! Clone()
- {
- LinearConstraintSystem z = new LinearConstraintSystem();
- z.FrameDimensions = (IMutableSet /*IVariable!*/!)this.FrameDimensions.Clone();
- if (this.Constraints != null)
- {
- z.Constraints = DeeperListCopy_LC(this.Constraints);
- z.FrameVertices = DeeperListCopy_FE((!)this.FrameVertices);
- z.FrameRays = DeeperListCopy_FE((!)this.FrameRays);
- z.FrameLines = DeeperListCopy_FE((!)this.FrameLines);
- }
- else
- {
- System.Diagnostics.Debug.Assert(this.FrameVertices == null);
- System.Diagnostics.Debug.Assert(this.FrameRays == null);
- System.Diagnostics.Debug.Assert(this.FrameLines == null);
- // the constructor should already have set these fields of z to null
- System.Diagnostics.Debug.Assert(z.Constraints == null);
- System.Diagnostics.Debug.Assert(z.FrameVertices == null);
- System.Diagnostics.Debug.Assert(z.FrameRays == null);
- System.Diagnostics.Debug.Assert(z.FrameLines == null);
- }
- return z;
- }
+ public LinearConstraintSystem/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<LinearConstraintSystem>() != null);
+ LinearConstraintSystem z = new LinearConstraintSystem();
+ z.FrameDimensions = (IMutableSet /*IVariable!*//*!*/)cce.NonNull(this.FrameDimensions.Clone());
+ if (this.Constraints != null) {
+ z.Constraints = DeeperListCopy_LC(this.Constraints);
+ z.FrameVertices = DeeperListCopy_FE(cce.NonNull(this.FrameVertices));
+ z.FrameRays = DeeperListCopy_FE(cce.NonNull(this.FrameRays));
+ z.FrameLines = DeeperListCopy_FE(cce.NonNull(this.FrameLines));
+ } else {
+ System.Diagnostics.Debug.Assert(this.FrameVertices == null);
+ System.Diagnostics.Debug.Assert(this.FrameRays == null);
+ System.Diagnostics.Debug.Assert(this.FrameLines == null);
+ // the constructor should already have set these fields of z to null
+ System.Diagnostics.Debug.Assert(z.Constraints == null);
+ System.Diagnostics.Debug.Assert(z.FrameVertices == null);
+ System.Diagnostics.Debug.Assert(z.FrameRays == null);
+ System.Diagnostics.Debug.Assert(z.FrameLines == null);
+ }
+ return z;
+ }
- /// <summary>
- /// Clones "list" and the elements of "list".
- /// </summary>
- /// <param name="list"></param>
- /// <returns></returns>
- ArrayList /*LinearConstraint*/ DeeperListCopy_LC(ArrayList! /*LinearConstraint*/ list)
- {
- ArrayList /*LinearConstraint*/ z = new ArrayList /*LinearConstraint*/ (list.Count);
- foreach (LinearConstraint! lc in list)
- {
- z.Add(lc.Clone());
- }
- System.Diagnostics.Debug.Assert(z.Count == list.Count);
- return z;
- }
+ /// <summary>
+ /// Clones "list" and the elements of "list".
+ /// </summary>
+ /// <param name="list"></param>
+ /// <returns></returns>
+ ArrayList /*LinearConstraint*/ DeeperListCopy_LC(ArrayList/*!*/ /*LinearConstraint*/ list) {
+ Contract.Requires(list != null);
+ ArrayList /*LinearConstraint*/ z = new ArrayList /*LinearConstraint*/ (list.Count);
+ foreach (LinearConstraint/*!*/ lc in list) {
+ Contract.Assert(lc != null);
+ z.Add(lc.Clone());
+ }
+ System.Diagnostics.Debug.Assert(z.Count == list.Count);
+ return z;
+ }
- /// <summary>
- /// Clones "list" and the elements of "list".
- /// </summary>
- /// <param name="list"></param>
- /// <returns></returns>
- ArrayList /*FrameElement*/ DeeperListCopy_FE(ArrayList! /*FrameElement*/ list)
- {
- ArrayList /*FrameElement*/ z = new ArrayList /*FrameElement*/ (list.Count);
- foreach (FrameElement! fe in list)
- {
- z.Add(fe.Clone());
- }
- System.Diagnostics.Debug.Assert(z.Count == list.Count);
- return z;
- }
+ /// <summary>
+ /// Clones "list" and the elements of "list".
+ /// </summary>
+ /// <param name="list"></param>
+ /// <returns></returns>
+ ArrayList /*FrameElement*/ DeeperListCopy_FE(ArrayList/*!*/ /*FrameElement*/ list) {
+ Contract.Requires(list != null);
+ ArrayList /*FrameElement*/ z = new ArrayList /*FrameElement*/ (list.Count);
+ foreach (FrameElement/*!*/ fe in list) {
+ Contract.Assert(fe != null);
+ z.Add(fe.Clone());
+ }
+ System.Diagnostics.Debug.Assert(z.Count == list.Count);
+ return z;
+ }
// --------------------------------------------------------------------------------------------------------
// ------------------ Debugging and unit test routines ----------------------------------------------------
// --------------------------------------------------------------------------------------------------------
- public void Dump()
- {
- Console.WriteLine(" Constraints:");
- if (Constraints == null)
- {
- Console.WriteLine(" <bottom>");
- }
- else
- {
- foreach (LinearConstraint cc in Constraints)
- {
- Console.WriteLine(" {0}", cc);
- }
- }
-
- Console.WriteLine(" FrameDimensions: {0}", FrameDimensions);
-
- Console.WriteLine(" FrameVerticies:");
- if (FrameVertices == null)
- {
- Console.WriteLine(" <null>");
- }
- else
- {
- foreach (FrameElement fe in FrameVertices)
- {
- Console.WriteLine(" {0}", fe);
- }
- }
+ public void Dump() {
+ Console.WriteLine(" Constraints:");
+ if (Constraints == null) {
+ Console.WriteLine(" <bottom>");
+ } else {
+ foreach (LinearConstraint cc in Constraints) {
+ Console.WriteLine(" {0}", cc);
+ }
+ }
- Console.WriteLine(" FrameRays:");
- if (FrameRays == null)
- {
- Console.WriteLine(" <null>");
- }
- else
- {
- foreach (FrameElement fe in FrameRays)
- {
- Console.WriteLine(" {0}", fe);
- }
- }
+ Console.WriteLine(" FrameDimensions: {0}", FrameDimensions);
- Console.WriteLine(" FrameLines:");
- if (FrameLines == null)
- {
- Console.WriteLine(" <null>");
- }
- else
- {
- foreach (FrameElement fe in FrameLines)
- {
- Console.WriteLine(" {0}", fe);
- }
- }
+ Console.WriteLine(" FrameVerticies:");
+ if (FrameVertices == null) {
+ Console.WriteLine(" <null>");
+ } else {
+ foreach (FrameElement fe in FrameVertices) {
+ Console.WriteLine(" {0}", fe);
}
+ }
- class TestVariable : IVariable {
- readonly string! name;
-
- public string! Name
- {
- get
- {
- return name;
- }
- }
-
- public TestVariable(string! name) {
- this.name = name;
- }
- [Pure]
- public object DoVisit(ExprVisitor! visitor) {
- return visitor.VisitVariable(this);
- }
+ Console.WriteLine(" FrameRays:");
+ if (FrameRays == null) {
+ Console.WriteLine(" <null>");
+ } else {
+ foreach (FrameElement fe in FrameRays) {
+ Console.WriteLine(" {0}", fe);
}
-
- public static void RunValidationA()
- {
- IVariable! dim1 = new TestVariable("X");
- IVariable! dim2 = new TestVariable("Y");
- IVariable! dim3 = new TestVariable("Z");
-
- FrameElement s1 = new FrameElement();
- s1.AddCoordinate(dim1, Rational.ONE);
- s1.AddCoordinate(dim2, Rational.MINUS_ONE);
- s1.AddCoordinate(dim3, Rational.ZERO);
- FrameElement s2 = new FrameElement();
- s2.AddCoordinate(dim1, Rational.MINUS_ONE);
- s2.AddCoordinate(dim2, Rational.ONE);
- s2.AddCoordinate(dim3, Rational.ZERO);
- FrameElement r1 = new FrameElement();
- r1.AddCoordinate(dim1, Rational.ZERO);
- r1.AddCoordinate(dim2, Rational.ZERO);
- r1.AddCoordinate(dim3, Rational.ONE);
- FrameElement d1 = new FrameElement();
- d1.AddCoordinate(dim1, Rational.ONE);
- d1.AddCoordinate(dim2, Rational.ONE);
- d1.AddCoordinate(dim3, Rational.ZERO);
-
- // create lcs from frame -- cf. Cousot/Halbwachs 1978, section 3.3.1.1
- LinearConstraintSystem lcs = new LinearConstraintSystem(s1);
- lcs.Dump();
-
- lcs.AddVertex(s2);
- lcs.Dump();
-
- lcs.AddRay(r1);
- lcs.Dump();
-
- lcs.AddLine(d1);
- lcs.Dump();
-
- lcs.SimplifyConstraints();
- lcs.Dump();
+ }
-#if LATER
- lcs.GenerateFrameFromConstraints(); // should give us back the original frame...
-#endif
- Console.WriteLine("IsSubset? {0}", lcs.IsSubset(lcs.Clone()));
- lcs.Dump();
+ Console.WriteLine(" FrameLines:");
+ if (FrameLines == null) {
+ Console.WriteLine(" <null>");
+ } else {
+ foreach (FrameElement fe in FrameLines) {
+ Console.WriteLine(" {0}", fe);
}
+ }
+ }
- /// <summary>
- /// Tests the example in section 3.4.3 of Cousot and Halbwachs.
- /// </summary>
- public static void RunValidationB()
- {
- IVariable! X = new TestVariable("X");
- IVariable! Y = new TestVariable("Y");
- IVariable! Z = new TestVariable("Z");
- ArrayList /*LinearConstraint*/ cs = new ArrayList /*LinearConstraint*/ ();
-
- LinearConstraint c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
- c.SetCoefficient(X, Rational.MINUS_ONE);
- c.SetCoefficient(Y, Rational.ONE);
- c.SetCoefficient(Z, Rational.MINUS_ONE);
- c.rhs = Rational.ZERO;
- cs.Add(c);
-
- c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
- c.SetCoefficient(X, Rational.MINUS_ONE);
- c.rhs = Rational.MINUS_ONE;
- cs.Add(c);
-
- c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
- c.SetCoefficient(X, Rational.MINUS_ONE);
- c.SetCoefficient(Y, Rational.MINUS_ONE);
- c.SetCoefficient(Z, Rational.ONE);
- c.rhs = Rational.ZERO;
- cs.Add(c);
-
- c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
- c.SetCoefficient(Y, Rational.MINUS_ONE);
- c.SetCoefficient(Z, Rational.ONE);
- c.rhs = Rational.FromInt(3);
- cs.Add(c);
-
- LinearConstraintSystem lcs = new LinearConstraintSystem(cs);
- Console.WriteLine("==================== The final linear constraint system ====================");
- lcs.Dump();
+ class TestVariable : IVariable {
+ readonly string/*!*/ name;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(name != null);
+ }
+
+
+ public string/*!*/ Name {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+
+ return name;
}
+ }
- public static void RunValidationC()
- {
- // Run the example in section 3.4.3 of Cousot and Halbwachs backwards, that is, from
- // from to constraints.
- IVariable! dim1 = new TestVariable("X");
- IVariable! dim2 = new TestVariable("Y");
- IVariable! dim3 = new TestVariable("Z");
+ public TestVariable(string/*!*/ name) {
+ Contract.Requires(name != null);
+ this.name = name;
+ }
+ [Pure]
+ public object DoVisit(ExprVisitor/*!*/ visitor) {
+ Contract.Requires(visitor != null);
+ return visitor.VisitVariable(this);
+ }
+ }
- FrameElement s0 = new FrameElement();
- s0.AddCoordinate(dim1, Rational.ONE);
- s0.AddCoordinate(dim2, Rational.FromInts(1, 2));
- s0.AddCoordinate(dim3, Rational.FromInts(-1, 2));
+ public static void RunValidationA() {
+ IVariable/*!*/ dim1 = new TestVariable("X");
+ IVariable/*!*/ dim2 = new TestVariable("Y");
+ IVariable/*!*/ dim3 = new TestVariable("Z");
+ Contract.Assert(dim1 != null);
+ Contract.Assert(dim2 != null);
+ Contract.Assert(dim3 != null);
+
+ FrameElement s1 = new FrameElement();
+ s1.AddCoordinate(dim1, Rational.ONE);
+ s1.AddCoordinate(dim2, Rational.MINUS_ONE);
+ s1.AddCoordinate(dim3, Rational.ZERO);
+ FrameElement s2 = new FrameElement();
+ s2.AddCoordinate(dim1, Rational.MINUS_ONE);
+ s2.AddCoordinate(dim2, Rational.ONE);
+ s2.AddCoordinate(dim3, Rational.ZERO);
+ FrameElement r1 = new FrameElement();
+ r1.AddCoordinate(dim1, Rational.ZERO);
+ r1.AddCoordinate(dim2, Rational.ZERO);
+ r1.AddCoordinate(dim3, Rational.ONE);
+ FrameElement d1 = new FrameElement();
+ d1.AddCoordinate(dim1, Rational.ONE);
+ d1.AddCoordinate(dim2, Rational.ONE);
+ d1.AddCoordinate(dim3, Rational.ZERO);
+
+ // create lcs from frame -- cf. Cousot/Halbwachs 1978, section 3.3.1.1
+ LinearConstraintSystem lcs = new LinearConstraintSystem(s1);
+ lcs.Dump();
- FrameElement s1 = new FrameElement();
- s1.AddCoordinate(dim1, Rational.ONE);
- s1.AddCoordinate(dim2, Rational.FromInts(-1, 2));
- s1.AddCoordinate(dim3, Rational.FromInts(1, 2));
+ lcs.AddVertex(s2);
+ lcs.Dump();
- FrameElement s2 = new FrameElement();
- s2.AddCoordinate(dim1, Rational.FromInt(3));
- s2.AddCoordinate(dim2, Rational.FromInts(-3, 2));
- s2.AddCoordinate(dim3, Rational.FromInts(3, 2));
+ lcs.AddRay(r1);
+ lcs.Dump();
- FrameElement r0 = new FrameElement();
- r0.AddCoordinate(dim1, Rational.ONE);
- r0.AddCoordinate(dim2, Rational.FromInts(1, 2));
- r0.AddCoordinate(dim3, Rational.FromInts(-1, 2));
+ lcs.AddLine(d1);
+ lcs.Dump();
- FrameElement r1 = new FrameElement();
- r1.AddCoordinate(dim1, Rational.ONE);
- r1.AddCoordinate(dim2, Rational.ZERO);
- r1.AddCoordinate(dim3, Rational.ZERO);
+ lcs.SimplifyConstraints();
+ lcs.Dump();
+
+#if LATER
+ lcs.GenerateFrameFromConstraints(); // should give us back the original frame...
+#endif
+ Console.WriteLine("IsSubset? {0}", lcs.IsSubset(lcs.Clone()));
+ lcs.Dump();
+ }
- FrameElement d0 = new FrameElement();
- d0.AddCoordinate(dim1, Rational.ZERO);
- d0.AddCoordinate(dim2, Rational.ONE);
- d0.AddCoordinate(dim3, Rational.ONE);
+ /// <summary>
+ /// Tests the example in section 3.4.3 of Cousot and Halbwachs.
+ /// </summary>
+ public static void RunValidationB() {
+ IVariable/*!*/ X = new TestVariable("X");
+ IVariable/*!*/ Y = new TestVariable("Y");
+ IVariable/*!*/ Z = new TestVariable("Z");
+ Contract.Assert(X != null);
+ Contract.Assert(Y != null);
+ Contract.Assert(Z != null);
+ ArrayList /*LinearConstraint*/ cs = new ArrayList /*LinearConstraint*/ ();
+
+ LinearConstraint c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+ c.SetCoefficient(X, Rational.MINUS_ONE);
+ c.SetCoefficient(Y, Rational.ONE);
+ c.SetCoefficient(Z, Rational.MINUS_ONE);
+ c.rhs = Rational.ZERO;
+ cs.Add(c);
+
+ c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+ c.SetCoefficient(X, Rational.MINUS_ONE);
+ c.rhs = Rational.MINUS_ONE;
+ cs.Add(c);
+
+ c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+ c.SetCoefficient(X, Rational.MINUS_ONE);
+ c.SetCoefficient(Y, Rational.MINUS_ONE);
+ c.SetCoefficient(Z, Rational.ONE);
+ c.rhs = Rational.ZERO;
+ cs.Add(c);
+
+ c = new LinearConstraint(LinearConstraint.ConstraintRelation.LE);
+ c.SetCoefficient(Y, Rational.MINUS_ONE);
+ c.SetCoefficient(Z, Rational.ONE);
+ c.rhs = Rational.FromInt(3);
+ cs.Add(c);
+
+ LinearConstraintSystem lcs = new LinearConstraintSystem(cs);
+ Console.WriteLine("==================== The final linear constraint system ====================");
+ lcs.Dump();
+ }
- LinearConstraintSystem lcs = new LinearConstraintSystem(s0);
- lcs.Dump();
+ public static void RunValidationC() {
+ // Run the example in section 3.4.3 of Cousot and Halbwachs backwards, that is, from
+ // from to constraints.
+ IVariable/*!*/ dim1 = new TestVariable("X");
+ IVariable/*!*/ dim2 = new TestVariable("Y");
+ IVariable/*!*/ dim3 = new TestVariable("Z");
+ Contract.Assert(dim1 != null);
+ Contract.Assert(dim2 != null);
+ Contract.Assert(dim3 != null);
+
+ FrameElement s0 = new FrameElement();
+ s0.AddCoordinate(dim1, Rational.ONE);
+ s0.AddCoordinate(dim2, Rational.FromInts(1, 2));
+ s0.AddCoordinate(dim3, Rational.FromInts(-1, 2));
+
+ FrameElement s1 = new FrameElement();
+ s1.AddCoordinate(dim1, Rational.ONE);
+ s1.AddCoordinate(dim2, Rational.FromInts(-1, 2));
+ s1.AddCoordinate(dim3, Rational.FromInts(1, 2));
+
+ FrameElement s2 = new FrameElement();
+ s2.AddCoordinate(dim1, Rational.FromInt(3));
+ s2.AddCoordinate(dim2, Rational.FromInts(-3, 2));
+ s2.AddCoordinate(dim3, Rational.FromInts(3, 2));
+
+ FrameElement r0 = new FrameElement();
+ r0.AddCoordinate(dim1, Rational.ONE);
+ r0.AddCoordinate(dim2, Rational.FromInts(1, 2));
+ r0.AddCoordinate(dim3, Rational.FromInts(-1, 2));
+
+ FrameElement r1 = new FrameElement();
+ r1.AddCoordinate(dim1, Rational.ONE);
+ r1.AddCoordinate(dim2, Rational.ZERO);
+ r1.AddCoordinate(dim3, Rational.ZERO);
+
+ FrameElement d0 = new FrameElement();
+ d0.AddCoordinate(dim1, Rational.ZERO);
+ d0.AddCoordinate(dim2, Rational.ONE);
+ d0.AddCoordinate(dim3, Rational.ONE);
+
+ LinearConstraintSystem lcs = new LinearConstraintSystem(s0);
+ lcs.Dump();
- lcs.AddVertex(s1);
- lcs.Dump();
+ lcs.AddVertex(s1);
+ lcs.Dump();
- lcs.AddVertex(s2);
- lcs.Dump();
+ lcs.AddVertex(s2);
+ lcs.Dump();
- lcs.AddRay(r0);
- lcs.Dump();
+ lcs.AddRay(r0);
+ lcs.Dump();
- lcs.AddRay(r1);
- lcs.Dump();
+ lcs.AddRay(r1);
+ lcs.Dump();
- lcs.AddLine(d0);
- lcs.Dump();
+ lcs.AddLine(d0);
+ lcs.Dump();
- lcs.SimplifyConstraints();
- lcs.Dump();
+ lcs.SimplifyConstraints();
+ lcs.Dump();
#if LATER
lcs.GenerateFrameFromConstraints(); // should give us back the original frame...
#endif
- }
}
+ }
}
\ No newline at end of file |