diff options
| author |  tabarbe <unknown> | 2010-08-27 21:15:08 +0000 |
|---|---|---|
| committer | tabarbe <unknown> | 2010-08-27 21:15:08 +0000 |
| commit | c333ecd2f30badea143e79f5f944a8c63398b959 (patch) | |
| tree | 28b04dc9f46d6fa90b4fdf38ffb24898bdc139b0 /Source/AIFramework/VariableMap/ConstantAbstraction.cs | |
| parent | dce6bf46952b5dd470ae841cae03706dbc30bc3b (diff) | |
Boogie: Removed some errors with code contracts (commenting out doubly-inherited requires statements), and set the code contracts settings to the correct compilation style for when runtime checking is turned on. (I did not turn on runtime checking, however).
Diffstat (limited to 'Source/AIFramework/VariableMap/ConstantAbstraction.cs')
| -rw-r--r-- | Source/AIFramework/VariableMap/ConstantAbstraction.cs | 414 |
1 files changed, 216 insertions, 198 deletions
diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.cs b/Source/AIFramework/VariableMap/ConstantAbstraction.cs index 89a64290..d8f17a3c 100644 --- a/Source/AIFramework/VariableMap/ConstantAbstraction.cs +++ b/Source/AIFramework/VariableMap/ConstantAbstraction.cs @@ -4,230 +4,248 @@ //
//-----------------------------------------------------------------------------
using System.Diagnostics.Contracts;
-namespace Microsoft.AbstractInterpretationFramework
-{
- using System.Collections;
- using System.Diagnostics;
- //using System.Compiler.Analysis;
- using Microsoft.Basetypes;
+namespace Microsoft.AbstractInterpretationFramework {
+ using System.Collections;
+ using System.Diagnostics;
+ //using System.Compiler.Analysis;
+ using Microsoft.Basetypes;
+
+ /// <summary>
+ /// Represents an invariant over constant variable assignments.
+ /// </summary>
+ public class ConstantLattice : MicroLattice {
+ enum Value {
+ Top,
+ Bottom,
+ Constant
+ }
- /// <summary>
- /// Represents an invariant over constant variable assignments.
- /// </summary>
- public class ConstantLattice : MicroLattice
- {
- enum Value { Top, Bottom, Constant }
+ private class Elt : Element {
+ public Value domainValue;
+ public BigNum constantValue; // valid iff domainValue == Value.Constant
- private class Elt : Element
- {
- public Value domainValue;
- public BigNum constantValue; // valid iff domainValue == Value.Constant
+ public Elt(Value v) {
+ this.domainValue = v;
+ }
- public Elt (Value v) { this.domainValue = v; }
+ public Elt(BigNum i) {
+ this.domainValue = Value.Constant;
+ this.constantValue = i;
+ }
- public Elt (BigNum i) { this.domainValue = Value.Constant; this.constantValue = i; }
+ public bool IsConstant {
+ get {
+ return this.domainValue == Value.Constant;
+ }
+ }
- public bool IsConstant { get { return this.domainValue == Value.Constant; } }
+ public BigNum Constant {
+ get {
+ return this.constantValue;
+ }
+ } // only when IsConstant
- public BigNum Constant { get { return this.constantValue; } } // only when IsConstant
+ [Pure]
+ public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+ Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
+ return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
+ }
- [Pure]
- public override System.Collections.Generic.ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
-Contract.Ensures(cce.NonNullElements(Contract.Result<System.Collections.Generic.ICollection<IVariable>>()));
-return cce.NonNull(new System.Collections.Generic.List<IVariable/*!*/>()).AsReadOnly();
- }
-
- public override Element/*!*/ Clone() {
-Contract.Ensures(Contract.Result<Element>() != null);
- if (this.IsConstant)
- return new Elt(constantValue);
- else
- return new Elt(domainValue);
- }
- }
+ public override Element/*!*/ Clone() {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ if (this.IsConstant)
+ return new Elt(constantValue);
+ else
+ return new Elt(domainValue);
+ }
+ }
- readonly IIntExprFactory/*!*/ factory;
- [ContractInvariantMethod]
- void ObjectInvariant() {
- Contract.Invariant(factory != null);
- }
+ readonly IIntExprFactory/*!*/ factory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(factory != null);
+ }
- public ConstantLattice(IIntExprFactory/*!*/ factory){
-Contract.Requires(factory != null);
- this.factory = factory;
- // base();
- }
+ public ConstantLattice(IIntExprFactory/*!*/ factory) {
+ Contract.Requires(factory != null);
+ this.factory = factory;
+ // base();
+ }
- public override Element/*!*/ Top{get{
-Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.Top); }
- }
+ public override Element/*!*/ Top {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Top);
+ }
+ }
- public override Element/*!*/ Bottom{get{
-Contract.Ensures(Contract.Result<Element>() != null);
- return new Elt(Value.Bottom); }
- }
+ public override Element/*!*/ Bottom {
+ get {
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Bottom);
+ }
+ }
- public override bool IsTop (Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- return e.domainValue == Value.Top; - }
+ public override bool IsTop(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ return e.domainValue == Value.Top;
+ }
- public override bool IsBottom (Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- return e.domainValue == Value.Bottom; - }
+ public override bool IsBottom(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ return e.domainValue == Value.Bottom;
+ }
- public override Element/*!*/ NontrivialJoin (Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
- Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
- return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Top;
- }
+ public override Element/*!*/ NontrivialJoin(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
+ return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Top;
+ }
- public override Element/*!*/ NontrivialMeet (Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
- Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
- return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Bottom;
- }
-
- public override Element/*!*/ Widen (Element/*!*/ first, Element/*!*/ second){
-Contract.Requires(second != null);
-Contract.Requires(first != null);
-Contract.Ensures(Contract.Result<Element>() != null);
- return Join(first,second);
- }
+ public override Element/*!*/ NontrivialMeet(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ Debug.Assert(a.domainValue == Value.Constant && b.domainValue == Value.Constant);
+ return (a.constantValue.Equals(b.constantValue)) ? a : (Elt)Bottom;
+ }
- protected override bool AtMost (Element/*!*/ first, Element/*!*/ second) // this <= that
- {
- Contract.Requires(first!= null);
- Contract.Requires(second != null);
- Elt a = (Elt)first;
- Elt b = (Elt)second;
- return a.Constant.Equals(b.Constant);
- }
+ public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) {
+ //Contract.Requires(second != null);
+ //Contract.Requires(first != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+ return Join(first, second);
+ }
- public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element){
-Contract.Requires(element != null);
-Contract.Requires(var != null);
-Contract.Ensures(Contract.Result<IExpr>() != null);
- return factory.Eq(var, cce.NonNull(GetFoldExpr(element)));
- }
+ protected override bool AtMost(Element/*!*/ first, Element/*!*/ second) // this <= that
+ {
+ //Contract.Requires(first!= null);
+ //Contract.Requires(second != null);
+ Elt a = (Elt)first;
+ Elt b = (Elt)second;
+ return a.Constant.Equals(b.Constant);
+ }
- public override IExpr GetFoldExpr(Element/*!*/ element){
-Contract.Requires(element != null);
- Elt e = (Elt)element;
- Contract.Assert(e.domainValue == Value.Constant);
- return factory.Const(e.constantValue);
- }
+ public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ //Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ return factory.Eq(var, cce.NonNull(GetFoldExpr(element)));
+ }
- public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args){
-Contract.Requires(args != null);
-Contract.Requires(f != null);
- return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
- }
+ public override IExpr GetFoldExpr(Element/*!*/ element) {
+ //Contract.Requires(element != null);
+ Elt e = (Elt)element;
+ Contract.Assert(e.domainValue == Value.Constant);
+ return factory.Const(e.constantValue);
+ }
- public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e){
-Contract.Requires(e != null);
-Contract.Ensures(Contract.Result<Element>() != null);
-
- IFunApp nary = e as IFunApp;
- if (nary != null) {
- if (nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) {
- IList/*<IExpr!>*//*!*/ args = nary.Arguments;
- Contract.Assert(args != null);
- Contract.Assert(args.Count == 2);
- IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
- IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
-
- // Look for "x == const" or "const == x".
- try {
- if (arg0 is IVariable) {
- BigNum z;
- if (Fold(arg1, out z)) {
- return new Elt(z);
- }
- } else if (arg1 is IVariable) {
- BigNum z;
- if (Fold(arg0, out z)) {
- return new Elt(z);
- }
- }
- } catch (System.ArithmeticException) {
- // fall through and return Top. (Note, an alternative design may
- // consider returning Bottom.)
- }
- }
- }
- return Top;
- }
+ public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args) {
+ //Contract.Requires(args != null);
+ //Contract.Requires(f != null);
+ return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
+ }
- /// <summary>
- /// Returns true if "expr" represents a constant integer expressions, in which case
- /// "z" returns as that integer. Otherwise, returns false, in which case "z" should
- /// not be used by the caller.
- ///
- /// This method throws an System.ArithmeticException in the event that folding the
- /// constant expression results in an arithmetic overflow or division by zero.
- /// </summary>
- private bool Fold(IExpr/*!*/ expr, out BigNum z){
-Contract.Requires(expr != null);
- IFunApp e = expr as IFunApp;
- if (e == null) {
- z = BigNum.ZERO;
- return false;
+ public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e) {
+ //Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<Element>() != null);
+
+ IFunApp nary = e as IFunApp;
+ if (nary != null) {
+ if (nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) {
+ IList/*<IExpr!>*//*!*/ args = nary.Arguments;
+ Contract.Assert(args != null);
+ Contract.Assert(args.Count == 2);
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+ IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
+
+ // Look for "x == const" or "const == x".
+ try {
+ if (arg0 is IVariable) {
+ BigNum z;
+ if (Fold(arg1, out z)) {
+ return new Elt(z);
+ }
+ } else if (arg1 is IVariable) {
+ BigNum z;
+ if (Fold(arg0, out z)) {
+ return new Elt(z);
+ }
}
+ } catch (System.ArithmeticException) {
+ // fall through and return Top. (Note, an alternative design may
+ // consider returning Bottom.)
+ }
+ }
+ }
+ return Top;
+ }
- if (e.FunctionSymbol is IntSymbol) {
- z = ((IntSymbol)e.FunctionSymbol).Value;
- return true;
-
- } else if (e.FunctionSymbol.Equals(Int.Negate)) {
- IList/*<IExpr!>*//*!*/ args = e.Arguments;
- Contract.Assert(args != null);
- Contract.Assert(args.Count == 1);
- IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
-
- if (Fold(arg0, out z)) {
- z = z.Neg;
- return true;
- }
-
- } else if (e.Arguments.Count == 2) {
- IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(e.Arguments[0]);
- IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(e.Arguments[1]);
- BigNum z0, z1;
- if (Fold(arg0, out z0) && Fold(arg1, out z1)) {
- if (e.FunctionSymbol.Equals(Int.Add)) {
- z = z0 + z1;
- } else if (e.FunctionSymbol.Equals(Int.Sub)) {
- z = z0 - z1;
- } else if (e.FunctionSymbol.Equals(Int.Mul)) {
- z = z0 * z1;
- } else if (e.FunctionSymbol.Equals(Int.Div)) {
- z = z0 / z1;
- } else if (e.FunctionSymbol.Equals(Int.Mod)) {
- z = z0 % z1;
- } else {
- z = BigNum.ZERO;
- return false;
- }
- return true;
- }
- }
-
+ /// <summary>
+ /// Returns true if "expr" represents a constant integer expressions, in which case
+ /// "z" returns as that integer. Otherwise, returns false, in which case "z" should
+ /// not be used by the caller.
+ ///
+ /// This method throws an System.ArithmeticException in the event that folding the
+ /// constant expression results in an arithmetic overflow or division by zero.
+ /// </summary>
+ private bool Fold(IExpr/*!*/ expr, out BigNum z) {
+ Contract.Requires(expr != null);
+ IFunApp e = expr as IFunApp;
+ if (e == null) {
+ z = BigNum.ZERO;
+ return false;
+ }
+
+ if (e.FunctionSymbol is IntSymbol) {
+ z = ((IntSymbol)e.FunctionSymbol).Value;
+ return true;
+
+ } else if (e.FunctionSymbol.Equals(Int.Negate)) {
+ IList/*<IExpr!>*//*!*/ args = e.Arguments;
+ Contract.Assert(args != null);
+ Contract.Assert(args.Count == 1);
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+
+ if (Fold(arg0, out z)) {
+ z = z.Neg;
+ return true;
+ }
+
+ } else if (e.Arguments.Count == 2) {
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(e.Arguments[0]);
+ IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(e.Arguments[1]);
+ BigNum z0, z1;
+ if (Fold(arg0, out z0) && Fold(arg1, out z1)) {
+ if (e.FunctionSymbol.Equals(Int.Add)) {
+ z = z0 + z1;
+ } else if (e.FunctionSymbol.Equals(Int.Sub)) {
+ z = z0 - z1;
+ } else if (e.FunctionSymbol.Equals(Int.Mul)) {
+ z = z0 * z1;
+ } else if (e.FunctionSymbol.Equals(Int.Div)) {
+ z = z0 / z1;
+ } else if (e.FunctionSymbol.Equals(Int.Mod)) {
+ z = z0 % z1;
+ } else {
z = BigNum.ZERO;
return false;
+ }
+ return true;
}
+ }
+
+ z = BigNum.ZERO;
+ return false;
}
+ }
}
|