summaryrefslogtreecommitdiff
path: root/Source/AIFramework/VariableMap/VariableMapLattice.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/AIFramework/VariableMap/VariableMapLattice.cs')
-rw-r--r--Source/AIFramework/VariableMap/VariableMapLattice.cs370
1 files changed, 225 insertions, 145 deletions
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs
index ab030b59..e0b9ac04 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.cs
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs
@@ -5,7 +5,7 @@
//-----------------------------------------------------------------------------
namespace Microsoft.AbstractInterpretationFramework
{
- using Microsoft.Contracts;
+ using System.Diagnostics.Contracts;
using System.Collections;
using System.Collections.Generic;
using System.Diagnostics;
@@ -47,20 +47,21 @@ namespace Microsoft.AbstractInterpretationFramework
}
}
- public override Element! Clone()
- {
+ public override Element/*!*/ Clone() {
+Contract.Ensures(Contract.Result<Element>() != null);
return new Elt(this.constraints);
}
[Pure]
- public override string! ToString()
- {
+ public override string/*!*/ ToString() {
+Contract.Ensures(Contract.Result<string>() != null);
if (constraints == null) {
return "<bottom>";
}
string s = "[";
string sep = "";
- foreach (IVariable! v in (!)constraints.Keys) {
+ foreach(IVariable/*!*/ v in cce.NonNull(constraints.Keys)){
+Contract.Assert(v != null);
Element m = (Element)constraints[v];
s += sep + v.Name + " -> " + m;
sep = ", ";
@@ -68,8 +69,15 @@ namespace Microsoft.AbstractInterpretationFramework
return s + "]";
}
- public static Elt! Top = new Elt(true);
- public static Elt! Bottom = new Elt(false);
+ public static Elt/*!*/ Top = new Elt(true);
+ public static Elt/*!*/ Bottom = new Elt(false);
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(Top != null);
+ Contract.Invariant(Bottom != null);
+}
+
public Elt(IFunctionalMap constraints)
{
@@ -84,16 +92,17 @@ namespace Microsoft.AbstractInterpretationFramework
public int Count { get { return this.constraints == null ? 0 : this.constraints.Count; } }
- public IEnumerable/*<IVariable>*/! Variables {
- get
- requires !this.IsBottom;
- {
- assume this.constraints != null;
- return (!) this.constraints.Keys;
+ public IEnumerable/*<IVariable>*//*!*/ Variables {
+ get {
+ Contract.Requires(!this.IsBottom);
+ Contract.Ensures(Contract.Result<IEnumerable>() != null);
+ Contract.Assume(this.constraints != null);
+ return cce.NonNull(this.constraints.Keys);
}
}
- public IEnumerable/*<IVariable>*/! SortedVariables(/*maybe null*/ IComparer variableComparer) {
+ public IEnumerable/*<IVariable>*//*!*/ SortedVariables(/*maybe null*/ IComparer variableComparer) {
+ Contract.Ensures(Contract.Result<IEnumerable>() != null);
if (variableComparer == null) {
return Variables;
} else {
@@ -112,11 +121,11 @@ namespace Microsoft.AbstractInterpretationFramework
return (Element)this.constraints[v];
}
- public Element this [IVariable! key] {
- get
- requires !this.IsBottom;
- {
- assume this.constraints != null;
+ public Element this [IVariable/*!*/ key] {
+ get{
+ Contract.Requires(!this.IsBottom);
+ Contract.Requires(key != null);
+ Contract.Assume(this.constraints != null);
return (Element)constraints[key];
}
}
@@ -125,11 +134,14 @@ namespace Microsoft.AbstractInterpretationFramework
/// Add a new entry in the functional map: var --> value.
/// If the variable is already there, throws an exception
/// </summary>
- public Elt! Add(IVariable! var, Element! value, MicroLattice! microLattice)
- requires !this.IsBottom;
- {
- assume this.constraints != null;
- assert !this.constraints.Contains(var);
+ public Elt/*!*/ Add(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice){
+Contract.Requires(microLattice != null);
+Contract.Requires(value != null);
+Contract.Requires(var != null);
+Contract.Requires((!this.IsBottom));
+Contract.Ensures(Contract.Result<Elt>() != null);
+ Contract.Assume(this.constraints != null);
+ Contract.Assert(!this.constraints.Contains(var));
if (microLattice.IsBottom(value)) { return Bottom; }
if (microLattice.IsTop(value)) { return this.Remove(var, microLattice); }
@@ -141,13 +153,16 @@ namespace Microsoft.AbstractInterpretationFramework
/// Set the value of the variable in the functional map
/// If the variable is not already there, throws an exception
/// </summary>
- public Elt! Set(IVariable! var, Element! value, MicroLattice! microLattice)
- {
+ public Elt/*!*/ Set(IVariable/*!*/ var, Element/*!*/ value, MicroLattice/*!*/ microLattice){
+ Contract.Requires(microLattice != null);
+ Contract.Requires(value != null);
+ Contract.Requires(var != null);
+ Contract.Ensures(Contract.Result<Elt>() != null);
if(microLattice.IsBottom(value)) { return Bottom; }
if(microLattice.IsTop(value)) { return this.Remove(var, microLattice); }
- assume this.constraints != null;
- assert this.constraints.Contains(var);
+ Contract.Assume(this.constraints != null);
+ Contract.Assert(this.constraints.Contains(var));
// this.constraints[var] = value;
IFunctionalMap newMap = this.constraints.Set(var, value);
@@ -155,74 +170,95 @@ namespace Microsoft.AbstractInterpretationFramework
return new Elt(newMap);
}
- public Elt! Remove(IVariable! var, MicroLattice microLattice)
- {
+ public Elt/*!*/ Remove(IVariable/*!*/ var, MicroLattice microLattice){
+Contract.Requires(var != null);
+Contract.Ensures(Contract.Result<Elt>() != null);
if (this.IsBottom) { return this; }
- assume this.constraints != null;
+ Contract.Assume(this.constraints != null);
return new Elt(this.constraints.Remove(var));
}
- public Elt! Rename(IVariable! oldName, IVariable! newName, MicroLattice! microLattice)
- requires !this.IsBottom;
- {
+ public Elt/*!*/ Rename(IVariable/*!*/ oldName, IVariable/*!*/ newName, MicroLattice/*!*/ microLattice){
+Contract.Requires(microLattice != null);
+Contract.Requires(newName != null);
+Contract.Requires(oldName != null);
+Contract.Requires((!this.IsBottom));
+Contract.Ensures(Contract.Result<Elt>() != null);
Element value = this[oldName];
if (value == null) { return this; } // 'oldName' isn't in the map, so neither will be 'newName'
- assume this.constraints != null;
+ Contract.Assume(this.constraints != null);
IFunctionalMap newMap = this.constraints.Remove(oldName);
newMap = newMap.Add(newName, value);
return new Elt(newMap);
}
[Pure]
- public override ICollection<IVariable!>! FreeVariables()
- {
+ public override ICollection<IVariable/*!*/>/*!*/ FreeVariables() {
+Contract.Ensures(cce.NonNullElements(Contract.Result<ICollection<IVariable>>()));
throw new System.NotImplementedException();
}
} // class
- private readonly MicroLattice! microLattice;
+ private readonly MicroLattice/*!*/ microLattice;
+
+ private readonly IPropExprFactory/*!*/ propExprFactory;
+ [ContractInvariantMethod]
+void ObjectInvariant()
+{
+ Contract.Invariant(microLattice != null);
+ Contract.Invariant(propExprFactory != null);
+}
- private readonly IPropExprFactory! propExprFactory;
private readonly /*maybe null*/IComparer variableComparer;
- public VariableMapLattice(IPropExprFactory! propExprFactory, IValueExprFactory! valueExprFactory, MicroLattice! microLattice, /*maybe null*/IComparer variableComparer)
- : base(valueExprFactory)
- {
+ public VariableMapLattice(IPropExprFactory/*!*/ propExprFactory, IValueExprFactory/*!*/ valueExprFactory, MicroLattice/*!*/ microLattice, /*maybe null*/IComparer variableComparer)
+ : base(valueExprFactory){
+Contract.Requires(microLattice != null);
+Contract.Requires(valueExprFactory != null);
+Contract.Requires(propExprFactory != null);
this.propExprFactory = propExprFactory;
this.microLattice = microLattice;
this.variableComparer = variableComparer;
// base(valueExprFactory);
}
- protected override object! UniqueId { get { return this.microLattice.GetType(); } }
+ protected override object/*!*/ UniqueId{
+ get{
+Contract.Ensures(Contract.Result<object>() != null);
+ return this.microLattice.GetType(); } }
- public override Element! Top { get { return Elt.Top; } }
+ public override Element/*!*/ Top{
+get{Contract.Ensures(Contract.Result<Element>() != null);
+ return Elt.Top; } }
- public override Element! Bottom { get { return Elt.Bottom; } }
+ public override Element Bottom{get{
+Contract.Ensures(Contract.Result<Element>() != null);
+ return Elt.Bottom; } }
- public override bool IsTop(Element! element)
- {
+ public override bool IsTop(Element/*!*/ element){
+Contract.Requires(element != null);
Elt e = (Elt)element;
return !e.IsBottom && e.Count == 0;
}
- public override bool IsBottom(Element! element)
- {
+ public override bool IsBottom(Element/*!*/ element){
+Contract.Requires(element != null);
return ((Elt)element).IsBottom;
}
- protected override bool AtMost(Element! first, Element! second)
- {
+ protected override bool AtMost(Element/*!*/ first, Element/*!*/ second){
+Contract.Requires(second != null);
+Contract.Requires(first != null);
Elt a = (Elt)first;
Elt b = (Elt)second;
// return true iff every constraint in "this" is no weaker than the corresponding
// constraint in "that" and there are no additional constraints in "that"
- foreach (IVariable! var in a.Variables)
- {
- Element thisValue = (!)a[var];
+ foreach(IVariable/*!*/ var in a.Variables){
+Contract.Assert(var != null);
+ Element thisValue = cce.NonNull(a[var]);
Element thatValue = b[var];
if (thatValue == null) { continue; } // it's okay for "a" to know something "b" doesn't
@@ -231,11 +267,11 @@ namespace Microsoft.AbstractInterpretationFramework
return false;
}
- foreach (IVariable! var in b.Variables)
- {
+ foreach(IVariable/*!*/ var in b.Variables){
+Contract.Assert(var != null);
if (a.Lookup(var) != null) { continue; } // we checked this case in the loop above
- Element thatValue = (!)b[var];
+ Element thatValue = cce.NonNull(b[var]);
if (this.microLattice.IsTop(thatValue)) { continue; } // this is a trivial constraint
return false;
@@ -243,8 +279,11 @@ namespace Microsoft.AbstractInterpretationFramework
return true;
}
- private Elt! AddConstraint(Element! element, IVariable! var, /*MicroLattice*/Element! newValue)
- {
+ private Elt/*!*/ AddConstraint(Element/*!*/ element, IVariable/*!*/ var, /*MicroLattice*/Element/*!*/ newValue) {
+Contract.Requires((newValue != null));
+Contract.Requires((var != null));
+Contract.Requires((element != null));
+Contract.Ensures(Contract.Result<Elt>() != null);
Elt e = (Elt)element;
if (!e.IsBottom && !this.microLattice.IsBottom(newValue)) // if we're not at bottom
@@ -266,8 +305,9 @@ namespace Microsoft.AbstractInterpretationFramework
return e;
}
- public override string! ToString(Element! element)
- {
+ public override string/*!*/ ToString(Element/*!*/ element){
+Contract.Requires(element != null);
+Contract.Ensures(Contract.Result<string>() != null);
Elt e = (Elt)element;
if (IsTop(e)) { return "<top>"; }
@@ -275,22 +315,24 @@ namespace Microsoft.AbstractInterpretationFramework
int k = 0;
System.Text.StringBuilder buffer = new System.Text.StringBuilder();
- foreach (IVariable! key in e.SortedVariables(variableComparer))
- {
+ foreach(IVariable/*!*/ key in e.SortedVariables(variableComparer)){
+Contract.Assert(key != null);
if (k++ > 0) { buffer.Append("; "); }
buffer.AppendFormat("{0} = {1}", key, e[key]);
}
return buffer.ToString();
}
- public override Element! NontrivialJoin(Element! first, Element! second)
- {
+ 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;
IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach (IVariable! key in a.Variables)
- {
+ foreach(IVariable/*!*/ key in a.Variables){
+Contract.Assert(key != null);
Element aValue = a[key];
Element bValue = b[key];
@@ -301,22 +343,25 @@ namespace Microsoft.AbstractInterpretationFramework
newMap = newMap.Add(key, newValue);
}
}
- Elt! join = new Elt(newMap);
+ Elt/*!*/ join = new Elt(newMap);
+ Contract.Assert(join != null);
// System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
return join;
}
- public override Element! NontrivialMeet(Element! first, Element! 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;
IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach (IVariable! key in a.Variables)
- {
- Element! aValue = (!) a[key];
+ foreach(IVariable/*!*/ key in a.Variables){
+Contract.Assert(key != null);
+Element/*!*/ aValue = cce.NonNull(a[key]);
Element bValue = b[key];
Element newValue =
@@ -325,8 +370,8 @@ namespace Microsoft.AbstractInterpretationFramework
newMap = newMap.Add(key, newValue);
}
- foreach (IVariable! key in b.Variables)
- {
+ foreach(IVariable/*!*/ key in b.Variables){
+Contract.Assert(key != null);
Element aValue = a[key];
Element bValue = b[key]; Debug.Assert(bValue != null);
@@ -342,8 +387,10 @@ namespace Microsoft.AbstractInterpretationFramework
/// <summary>
/// Perform the pointwise widening of the elements in the map
/// </summary>
- public override Element! Widen (Element! first, Element! second)
- {
+ public override Element/*!*/ Widen (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;
@@ -354,8 +401,8 @@ namespace Microsoft.AbstractInterpretationFramework
return new Elt(a.Constraints);
IFunctionalMap newMap = FunctionalHashtable.Empty;
- foreach (IVariable! key in a.Variables)
- {
+ foreach(IVariable/*!*/ key in a.Variables){
+Contract.Assert(key != null);
Element aValue = a[key];
Element bValue = b[key];
@@ -366,15 +413,17 @@ namespace Microsoft.AbstractInterpretationFramework
newMap = newMap.Add(key, newValue);
}
}
- Element! widen= new Elt(newMap);
-
+ Element/*!*/ widen= new Elt(newMap);
+ Contract.Assert(widen != null);
// System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
return widen;
}
- internal static ISet/*<IVariable!>*/! VariablesInExpression(IExpr! e, ISet/*<IVariable!>*/! ignoreVars)
- {
+ internal static ISet/*<IVariable!>*//*!*/ VariablesInExpression(IExpr/*!*/ e, ISet/*<IVariable!>*//*!*/ ignoreVars){
+Contract.Requires(ignoreVars != null);
+Contract.Requires(e != null);
+ Contract.Ensures(Contract.Result<ISet>() != null);
HashSet s = new HashSet();
IFunApp f = e as IFunApp;
@@ -387,8 +436,8 @@ namespace Microsoft.AbstractInterpretationFramework
}
else if (f != null) // e is IFunApp
{
- foreach (IExpr! arg in f.Arguments)
- {
+ foreach(IExpr/*!*/ arg in f.Arguments){
+Contract.Assert(arg != null);
s.AddAll(VariablesInExpression(arg, ignoreVars));
}
}
@@ -398,7 +447,7 @@ namespace Microsoft.AbstractInterpretationFramework
x.Add(lambda.Param);
// Ignore the bound variable
- s.AddAll(VariablesInExpression(lambda.Body, (!) Set.Union(ignoreVars, x)));
+ s.AddAll(VariablesInExpression(lambda.Body, cce.NonNull(Set.Union(ignoreVars, x))));
}
else if (e is IUnknown)
{
@@ -412,8 +461,9 @@ namespace Microsoft.AbstractInterpretationFramework
}
- private static ArrayList/*<IExpr>*/! FindConjuncts(IExpr e)
+ private static ArrayList/*<IExpr>*//*!*/ FindConjuncts(IExpr e)
{
+ Contract.Ensures(Contract.Result<ArrayList>() != null);
ArrayList result = new ArrayList();
IFunApp f = e as IFunApp;
@@ -445,8 +495,8 @@ namespace Microsoft.AbstractInterpretationFramework
}
private static bool IsSimpleEquality(IExpr expr, out IVariable left, out IVariable right)
- ensures result ==> left != null && right != null;
- {
+ {
+ Contract.Ensures(!Contract.Result<bool>() || Contract.ValueAtReturn(out left) != null && Contract.ValueAtReturn(out right) != null);
left = null;
right = null;
@@ -467,8 +517,8 @@ namespace Microsoft.AbstractInterpretationFramework
/// <summary>
/// Returns true iff the expression is in the form var == arithmeticExpr
/// </summary>
- private static bool IsArithmeticExpr(IExpr! expr)
- {
+ private static bool IsArithmeticExpr(IExpr/*!*/ expr){
+Contract.Requires(expr != null);
// System.Console.WriteLine("\t\tIsArithmetic called with {0} of type {1}", expr, expr.GetType().ToString());
if(expr is IVariable) // expr is a variable
@@ -480,13 +530,13 @@ namespace Microsoft.AbstractInterpretationFramework
if(fun.FunctionSymbol is IntSymbol) // it is an integer
return true;
else if(fun.FunctionSymbol.Equals(Int.Negate)) // it is an unary minus
- return IsArithmeticExpr((IExpr!) fun.Arguments[0]);
+ return IsArithmeticExpr((IExpr/*!*/)cce.NonNull(fun.Arguments[0]));
else if(fun.Arguments.Count != 2) // A function of two or more operands is not arithmetic
return false;
else
{
- IExpr! left = (IExpr!) fun.Arguments[0];
- IExpr! right = (IExpr!) fun.Arguments[1];
+ IExpr/*!*/ left = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ right = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
if(!(left is IVariable || right is IVariable)) // At least one of the two operands must be a variable
return false;
@@ -508,8 +558,9 @@ namespace Microsoft.AbstractInterpretationFramework
}
}
- public override IExpr! ToPredicate(Element! element)
- {
+ public override IExpr/*!*/ ToPredicate(Element/*!*/ element){
+Contract.Requires(element != null);
+Contract.Ensures(Contract.Result<IExpr>() != null);
if (IsTop(element)) { return propExprFactory.True; }
if (IsBottom(element)) { return propExprFactory.False; }
@@ -517,8 +568,8 @@ namespace Microsoft.AbstractInterpretationFramework
IExpr truth = propExprFactory.True;
IExpr result = truth;
- foreach (IVariable! variable in e.SortedVariables(variableComparer))
- {
+ foreach(IVariable/*!*/ variable in e.SortedVariables(variableComparer)){
+Contract.Assert(variable != null);
Element value = (Element)e[variable];
if (value == null || this.microLattice.IsTop(value)) { continue; } // Skip variables about which we know nothing.
@@ -532,14 +583,17 @@ namespace Microsoft.AbstractInterpretationFramework
}
- public override Element! Eliminate(Element! element, IVariable! variable)
- {
- return ((Elt!)element).Remove(variable, this.microLattice);
+ public override Element/*!*/ Eliminate(Element/*!*/ element, IVariable/*!*/ variable){
+Contract.Requires(variable != null);
+Contract.Requires(element != null);
+Contract.Ensures(Contract.Result<Element>() != null);
+ return cce.NonNull((Elt)element).Remove(variable, this.microLattice);
}
- private delegate IExpr! OnUnableToInline(IVariable! var);
- private IExpr! IdentityVarToExpr(IVariable! var)
- {
+ private delegate IExpr/*!*/ OnUnableToInline(IVariable/*!*/ var);
+ private IExpr/*!*/ IdentityVarToExpr(IVariable/*!*/ var){
+Contract.Requires(var != null);
+Contract.Ensures(Contract.Result<IExpr>() != null);
return var;
}
@@ -548,9 +602,13 @@ namespace Microsoft.AbstractInterpretationFramework
/// replaced by an expression representing what is known about
/// that variable.
/// </summary>
- private IExpr! InlineVariables(Elt! element, IExpr! expr, ISet/*<IVariable!>*/! notInlineable,
- OnUnableToInline! unableToInline)
- {
+ private IExpr/*!*/ InlineVariables(Elt/*!*/ element, IExpr/*!*/ expr, ISet/*<IVariable!>*//*!*/ notInlineable,
+ OnUnableToInline/*!*/ unableToInline){
+ Contract.Requires(unableToInline != null);
+Contract.Requires(notInlineable != null);
+Contract.Requires(expr != null);
+Contract.Requires(element != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
IVariable var = expr as IVariable;
if (var != null)
{
@@ -574,8 +632,8 @@ namespace Microsoft.AbstractInterpretationFramework
if (fun != null)
{
IList newargs = new ArrayList();
- foreach (IExpr! arg in fun.Arguments)
- {
+ foreach(IExpr/*!*/ arg in fun.Arguments){
+Contract.Assert(arg != null);
newargs.Add(InlineVariables(element, arg, notInlineable, unableToInline));
}
return fun.CloneWithArguments(newargs);
@@ -592,7 +650,7 @@ namespace Microsoft.AbstractInterpretationFramework
// Don't inline the bound variable
return lambda.CloneWithBody(
InlineVariables(element, lambda.Body,
- (!) Set.Union(notInlineable, x), unableToInline)
+ cce.NonNull(Set.Union(notInlineable, x)), unableToInline)
);
}
@@ -610,19 +668,22 @@ namespace Microsoft.AbstractInterpretationFramework
}
- public override Element! Constrain(Element! element, IExpr! expr)
- {
- Elt! result = (Elt)element;
+ public override Element/*!*/ Constrain(Element/*!*/ element, IExpr/*!*/ expr){
+Contract.Requires(expr != null);
+Contract.Requires(element != null);
+Contract.Ensures(Contract.Result<Element>() != null);
+ Elt/*!*/ result = (Elt)element;
+ Contract.Assert(result != null);
if(IsBottom(element))
{
return result; // == element
}
- expr = InlineVariables(result, expr, (!)Set.Empty, new OnUnableToInline(IdentityVarToExpr));
+ expr = InlineVariables(result, expr, cce.NonNull(Set.Empty), new OnUnableToInline(IdentityVarToExpr));
- foreach (IExpr! conjunct in FindConjuncts(expr))
- {
+ foreach(IExpr/*!*/ conjunct in FindConjuncts(expr)){
+Contract.Assert(conjunct != null);
IVariable left, right;
if (IsSimpleEquality(conjunct, out left, out right))
@@ -630,7 +691,7 @@ namespace Microsoft.AbstractInterpretationFramework
#region The conjunct is a simple equality
- assert left != null && right != null;
+ Contract.Assert(left != null && right != null);
Element leftValue = result[left], rightValue = result[right];
if (leftValue == null) { leftValue = this.microLattice.Top; }
@@ -650,9 +711,9 @@ namespace Microsoft.AbstractInterpretationFramework
#region We have just one variable
IVariable var = null;
- foreach (IVariable! v in variablesInvolved) { var = v; } // why is there no better way to get the elements?
- assert var != null;
- Element! value = this.microLattice.EvaluatePredicate(conjunct);
+ foreach (IVariable/*!*/ v in variablesInvolved) {Contract.Assert(v != null); var = v; } // why is there no better way to get the elements?
+ Contract.Assert(var != null);
+ Element/*!*/ value = this.microLattice.EvaluatePredicate(conjunct);
result = AddConstraint(result, var, value);
#endregion
@@ -665,12 +726,13 @@ namespace Microsoft.AbstractInterpretationFramework
if(fun.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq)) // if it is a symbol of equality
{
// get the variable to be assigned
- IExpr! leftArg = (IExpr!) fun.Arguments[0];
- IExpr! rightArg = (IExpr!) fun.Arguments[1];
- IExpr! var = (leftArg is IVariable) ? leftArg : rightArg;
-
- Element! value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
- result = AddConstraint(result, (IVariable!) var, value);
+ IExpr/*!*/ leftArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[0]);
+ IExpr/*!*/ rightArg = (IExpr/*!*/)cce.NonNull(fun.Arguments[1]);
+ IExpr/*!*/ var = (leftArg is IVariable) ? leftArg : rightArg;
+
+ Element/*!*/ value = this.microLattice.EvaluatePredicateWithState(conjunct, result.Constraints);
+ Contract.Assert(value != null);
+ result = AddConstraint(result, (IVariable/*!*/)cce.NonNull(var), value);
}
#endregion
}
@@ -680,8 +742,11 @@ namespace Microsoft.AbstractInterpretationFramework
}
- public override Element! Rename(Element! element, IVariable! oldName, IVariable! newName)
- {
+ public override Element/*!*/ Rename(Element/*!*/ element, IVariable/*!*/ oldName, IVariable/*!*/ newName){
+Contract.Requires(newName != null);
+Contract.Requires(oldName != null);
+Contract.Requires(element != null);
+Contract.Ensures(Contract.Result<Element>() != null);
if(IsBottom(element))
{
return element;
@@ -693,26 +758,34 @@ namespace Microsoft.AbstractInterpretationFramework
}
- public override bool Understands(IFunctionSymbol! f, IList! args)
- {
+ public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args){
+Contract.Requires(args != null);
+Contract.Requires(f != null);
return f.Equals(Prop.And) ||
f.Equals(Value.Eq) ||
microLattice.Understands(f, args);
}
- private sealed class EquivalentExprException : CheckedException { }
+ private sealed class EquivalentExprException :CheckedException { }
private sealed class EquivalentExprInlineCallback
{
- private readonly IVariable! var;
- public EquivalentExprInlineCallback(IVariable! var)
- {
+ private readonly IVariable/*!*/ var;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(var != null);
+ }
+
+ public EquivalentExprInlineCallback(IVariable/*!*/ var){
+Contract.Requires(var != null);
this.var = var;
// base();
}
- public IExpr! ThrowOnUnableToInline(IVariable! othervar)
- throws EquivalentExprException;
- {
+ public IExpr/*!*/ ThrowOnUnableToInline(IVariable/*!*/ othervar)
+ //throws EquivalentExprException;
+ {Contract.Requires(othervar != null);
+ Contract.Ensures(Contract.Result<IExpr>() != null);
+ Contract.EnsuresOnThrow<EquivalentExprException>(true);
if (othervar.Equals(var))
throw new EquivalentExprException();
else
@@ -720,12 +793,16 @@ namespace Microsoft.AbstractInterpretationFramework
}
}
- public override IExpr/*?*/ EquivalentExpr(Element! e, IQueryable! q, IExpr! expr, IVariable! var, ISet/*<IVariable!>*/! prohibitedVars)
- {
+ public override IExpr/*?*/ EquivalentExpr(Element/*!*/ e, IQueryable/*!*/ q, IExpr/*!*/ expr, IVariable/*!*/ var, ISet/*<IVariable!>*//*!*/ prohibitedVars){
+Contract.Requires(prohibitedVars != null);
+Contract.Requires(var != null);
+Contract.Requires(expr != null);
+Contract.Requires(q != null);
+Contract.Requires(e != null);
try
{
EquivalentExprInlineCallback closure = new EquivalentExprInlineCallback(var);
- return InlineVariables((Elt)e, expr, (!)Set.Empty,
+ return InlineVariables((Elt)e, expr, cce.NonNull(Set.Empty),
new OnUnableToInline(closure.ThrowOnUnableToInline));
}
catch (EquivalentExprException)
@@ -743,8 +820,9 @@ namespace Microsoft.AbstractInterpretationFramework
/// <param name="e">The lattice element.</param>
/// <param name="pred">The predicate.</param>
/// <returns>Yes, No, or Maybe</returns>
- public override Answer CheckPredicate(Element! e, IExpr! pred)
- {
+ public override Answer CheckPredicate(Element/*!*/ e, IExpr/*!*/ pred){
+Contract.Requires(pred != null);
+Contract.Requires(e != null);
return Answer.Maybe;
}
@@ -759,8 +837,10 @@ namespace Microsoft.AbstractInterpretationFramework
/// <param name="var1">The first variable.</param>
/// <param name="var2">The second variable.</param>
/// <returns>Yes, No, or Maybe.</returns>
- public override Answer CheckVariableDisequality(Element! e, IVariable! var1, IVariable! var2)
- {
+ public override Answer CheckVariableDisequality(Element/*!*/ e, IVariable/*!*/ var1, IVariable/*!*/ var2){
+Contract.Requires(var2 != null);
+Contract.Requires(var1 != null);
+Contract.Requires(e != null);
return Answer.Maybe;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 10:55:40 +0000