diff options
Diffstat (limited to 'Source/AIFramework/VariableMap/Nullness.cs')
| -rw-r--r-- | Source/AIFramework/VariableMap/Nullness.cs | 107 |
1 files changed, 67 insertions, 40 deletions
diff --git a/Source/AIFramework/VariableMap/Nullness.cs b/Source/AIFramework/VariableMap/Nullness.cs index bbd1da70..9eac6b29 100644 --- a/Source/AIFramework/VariableMap/Nullness.cs +++ b/Source/AIFramework/VariableMap/Nullness.cs @@ -3,18 +3,24 @@ // Copyright (C) Microsoft Corporation. All Rights Reserved.
//
//-----------------------------------------------------------------------------
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
namespace Microsoft.AbstractInterpretationFramework
{
using System.Collections;
using System.Diagnostics;
- using System.Compiler.Analysis;
+ //using System.Compiler.Analysis;
public class NullnessLattice : MicroLattice
{
- readonly INullnessFactory! factory;
+ readonly INullnessFactory/*!*/ factory;
+ [ContractInvariantMethod]
+ void ObjectInvariant() {
+ Contract.Invariant(factory != null);
+ }
- public NullnessLattice(INullnessFactory! factory) {
+
+ public NullnessLattice(INullnessFactory/*!*/ factory){
+Contract.Requires(factory != null);
this.factory = factory;
// base();
}
@@ -28,77 +34,92 @@ namespace Microsoft.AbstractInterpretationFramework public Elt (Value v) { this.value = v; }
[Pure]
- public override System.Collections.Generic.ICollection<IVariable!>! FreeVariables()
- {
- return (!) (new System.Collections.Generic.List<IVariable!>()).AsReadOnly();
+ 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()
- {
+ public override Element/*!*/ Clone() {
+Contract.Ensures(Contract.Result<Element>() != null);
return new Elt(this.value);
}
}
- public override Element! Top
+ public override Element/*!*/ Top
{
- get { return new Elt(Value.MayBeNull); }
+ get {Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.MayBeNull); }
}
- public override Element! Bottom
+ public override Element/*!*/ Bottom
{
- get { return new Elt(Value.Bottom); }
+ get {Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Bottom); }
}
- public static Element! Null
+ public static Element/*!*/ Null
{
- get { return new Elt(Value.Null); }
+ get {Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.Null); }
}
- public static Element! NotNull
+ public static Element/*!*/ NotNull
{
- get { return new Elt(Value.NotNull); }
+ get {Contract.Ensures(Contract.Result<Element>() != null);
+ return new Elt(Value.NotNull); }
}
- public override bool IsTop (Element! element)
- {
+ public override bool IsTop (Element/*!*/ element){
+Contract.Requires(element != null);
Elt e = (Elt) element;
return e.value == Value.MayBeNull;
}
- public override bool IsBottom (Element! element)
- {
+ public override bool IsBottom (Element/*!*/ element){
+Contract.Requires(element != null);
Elt e = (Elt) element;
return e.value == Value.Bottom;
}
- public override Lattice.Element! NontrivialJoin (Element! first, Element! second)
- {
+ public override Lattice.Element/*!*/ NontrivialJoin (Element/*!*/ first, Element/*!*/ second){
+Contract.Requires(second != null);
+Contract.Requires(first != null);
+Contract.Ensures(Contract.Result<Lattice.Element>() != null);
Elt a = (Elt) first;
Elt b = (Elt) second;
return (a.value == b.value) ? a : (Elt)Top;
}
- public override Lattice.Element! NontrivialMeet (Element! first, Element! second)
- {
+ public override Lattice.Element/*!*/ NontrivialMeet (Element/*!*/ first, Element/*!*/ second){
+Contract.Requires(second != null);
+Contract.Requires(first != null);
+Contract.Ensures(Contract.Result<Lattice.Element>() != null);
Elt a = (Elt) first;
Elt b = (Elt) second;
return (a.value == b.value) ? a : (Elt)Bottom;
}
- 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);
return Join(first,second);
}
- protected override bool AtMost (Element! first, Element! second) // this <= that
+ 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.value == b.value;
}
- public override IExpr! ToPredicate(IVariable! var, Element! element) {
+ public override IExpr/*!*/ ToPredicate(IVariable/*!*/ var, Element/*!*/ element){
+Contract.Requires(element != null);
+Contract.Requires(var != null);
+Contract.Ensures(Contract.Result<IExpr>() != null);
Elt e = (Elt)element;
if (e.value == Value.NotNull)
@@ -109,11 +130,12 @@ namespace Microsoft.AbstractInterpretationFramework {
return factory.Eq(var, factory.Null);
}
- assert false;
+ {Contract.Assert(false);throw new cce.UnreachableException();}
throw new System.Exception();
}
- public override IExpr GetFoldExpr(Element! e) {
+ public override IExpr GetFoldExpr(Element/*!*/ e){
+Contract.Requires(e != null);
Elt elt = (Elt)e;
if (elt.value == Value.Null) {
return factory.Null;
@@ -123,13 +145,15 @@ namespace Microsoft.AbstractInterpretationFramework }
}
- public override bool Understands(IFunctionSymbol! f, IList/*<IExpr!>*/! args) {
+ public override bool Understands(IFunctionSymbol/*!*/ f, IList/*<IExpr!>*//*!*/ args){
+Contract.Requires(args != null);
+Contract.Requires(f != null);
if (f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq) ||
f.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
- assert args.Count == 2;
- IExpr! arg0 = (IExpr!)args[0];
- IExpr! arg1 = (IExpr!)args[1];
+ Contract.Assert(args.Count == 2);
+ IExpr/*!*/ arg0 = (IExpr/*!*/)cce.NonNull(args[0]);
+ IExpr/*!*/ arg1 = (IExpr/*!*/)cce.NonNull(args[1]);
// Look for "x OP null" or "null OP x" where OP is "==" or "!=".
if (arg0 is IVariable && arg1 is IFunApp && ((IFunApp)arg1).FunctionSymbol == Ref.Null) {
@@ -141,15 +165,18 @@ namespace Microsoft.AbstractInterpretationFramework return false;
}
- public override Element! EvaluatePredicate(IExpr! e) {
+ public override Element/*!*/ EvaluatePredicate(IExpr/*!*/ e){
+Contract.Requires(e != null);
+Contract.Ensures(Contract.Result<Element>() != null);
IFunApp nary = e as IFunApp;
if (nary != null) {
bool isEq = nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
if (isEq || nary.FunctionSymbol.Equals(Microsoft.AbstractInterpretationFramework.Value.Neq)) {
- IList/*<IExpr!>*/! args = nary.Arguments;
- assert args.Count == 2;
- IExpr! arg0 = (IExpr!)args[0];
- IExpr! arg1 = (IExpr!)args[1];
+ 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 OP null" or "null OP x" where OP is "==" or "!=".
IVariable var = null;
|