Imported Upstream version 3.6.0

Former-commit-id: da6be194a6b1221998fc28233f2503bd61dd9d14

mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/AssertionFinder.cs

@@ -0,0 +1,134 @@
+// 
+// AssertionFinder.cs
+// 
+// Authors:
+// 	Alexander Chebaturkin (chebaturkin@gmail.com)
+// 
+// Copyright (C) 2011 Alexander Chebaturkin
+// 
+// Permission is hereby granted, free of charge, to any person obtaining
+// a copy of this software and associated documentation files (the
+// "Software"), to deal in the Software without restriction, including
+// without limitation the rights to use, copy, modify, merge, publish,
+// distribute, sublicense, and/or sell copies of the Software, and to
+// permit persons to whom the Software is furnished to do so, subject to
+// the following conditions:
+// 
+// The above copyright notice and this permission notice shall be
+// included in all copies or substantial portions of the Software.
+//  
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 
+// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+// 
+
+using System;
+using System.Collections.Generic;
+using Mono.CodeContracts.Static.AST.Visitors;
+using Mono.CodeContracts.Static.Analysis.Drivers;
+using Mono.CodeContracts.Static.ControlFlow;
+using Mono.CodeContracts.Static.Lattices;
+
+namespace Mono.CodeContracts.Static.Proving {
+	static class AssertionFinder {
+		public static void ValidateAssertions<TExpression, TVariable> (IFactQuery<BoxedExpression, TVariable> facts, IMethodDriver<TExpression, TVariable> driver, List<string> proofResults)
+			where TExpression : IEquatable<TExpression>
+			where TVariable : IEquatable<TVariable>
+		{
+			Bind<TExpression, TVariable>.ValidateAssertions (facts, driver, proofResults);
+		}
+
+		#region Nested type: Bind
+		private static class Bind<TExpression, TVariable>
+			where TExpression : IEquatable<TExpression>
+			where TVariable : IEquatable<TVariable> {
+			public static void ValidateAssertions (IFactQuery<BoxedExpression, TVariable> facts, IMethodDriver<TExpression, TVariable> driver, List<string> proofResults)
+			{
+				APC entryAfterRequires = driver.ContextProvider.MethodContext.CFG.EntryAfterRequires;
+				if (facts.IsUnreachable (entryAfterRequires)) {
+					proofResults.Add ("Method precondition is unsatisfiable");
+					return;
+				}
+
+				object assertStats;
+				foreach (AssertionObligation obl in GetAssertions (driver, out assertStats)) {
+					FlatDomain<bool> outcome = facts.IsTrue (obl.Apc, BoxedExpression.For (driver.ContextProvider.ExpressionContext.Refine (obl.Apc, obl.Condition), driver.ExpressionDecoder));
+
+					string pc = obl.Apc.ToString ();
+
+				    if (outcome.IsNormal ())
+				        proofResults.Add (string.Format ("Assertion at point {0} is {1}", pc, outcome.IsTrue () ? "true" : "false"));
+				    else if (outcome.IsTop)
+				        proofResults.Add ("Assertion at point " + pc + " is unproven");
+                    else
+                        proofResults.Add("Assertion at point " + pc + " is unreachable");
+				}
+			}
+
+			private static IEnumerable<AssertionObligation> GetAssertions (IMethodDriver<TExpression, TVariable> driver, out object assertStats)
+			{
+				var analysis = new AssertionCrawlerAnalysis ();
+				List<AssertionObligation> obligations = analysis.Gather (driver);
+
+				assertStats = null;
+				return obligations;
+			}
+
+			#region Nested type: AssertionCrawlerAnalysis
+			private class AssertionCrawlerAnalysis : ValueCodeVisitor<TVariable> {
+				private readonly List<AssertionObligation> Obligations = new List<AssertionObligation> ();
+
+				public List<AssertionObligation> Gather (IMethodDriver<TExpression, TVariable> driver)
+				{
+					Run (driver.ValueLayer);
+					return this.Obligations;
+				}
+
+				public override bool Assert (APC pc, EdgeTag tag, TVariable condition, bool data)
+				{
+					if (pc.InsideRequiresAtCallInsideContract)
+						return data;
+
+					this.Obligations.Add (new AssertionObligation (pc, tag, condition));
+					return data;
+				}
+
+				public override bool Assume (APC pc, EdgeTag tag, TVariable condition, bool data)
+				{
+					if (!pc.InsideRequiresAtCallInsideContract && tag == EdgeTag.Assume)
+						this.Obligations.Add (new AssertionObligation (pc, tag, condition, true));
+
+					return data;
+				}
+			}
+			#endregion
+
+			#region Nested type: AssertionObligation
+			private class AssertionObligation {
+				public readonly APC Apc;
+				public readonly TVariable Condition;
+				public readonly bool IsAssume;
+				public readonly EdgeTag Tag;
+
+				public AssertionObligation (APC pc, EdgeTag tag, TVariable cond)
+					: this (pc, tag, cond, false)
+				{
+				}
+
+				public AssertionObligation (APC pc, EdgeTag tag, TVariable cond, bool isAssume)
+				{
+					this.Apc = pc;
+					this.Tag = tag;
+					this.Condition = cond;
+					this.IsAssume = isAssume;
+				}
+			}
+			#endregion
+		}
+		#endregion
+	}
+}

mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/BasicFacts.cs

@@ -0,0 +1,133 @@
+// 
+// BasicFacts.cs
+// 
+// Authors:
+// 	Alexander Chebaturkin (chebaturkin@gmail.com)
+// 
+// Copyright (C) 2011 Alexander Chebaturkin
+// 
+// Permission is hereby granted, free of charge, to any person obtaining
+// a copy of this software and associated documentation files (the
+// "Software"), to deal in the Software without restriction, including
+// without limitation the rights to use, copy, modify, merge, publish,
+// distribute, sublicense, and/or sell copies of the Software, and to
+// permit persons to whom the Software is furnished to do so, subject to
+// the following conditions:
+// 
+// The above copyright notice and this permission notice shall be
+// included in all copies or substantial portions of the Software.
+//  
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 
+// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+// 
+
+using System;
+using Mono.CodeContracts.Static.Analysis;
+using Mono.CodeContracts.Static.ControlFlow;
+using Mono.CodeContracts.Static.DataStructures;
+using Mono.CodeContracts.Static.Lattices;
+
+namespace Mono.CodeContracts.Static.Proving {
+	class BasicFacts<Expression, Variable> : IFactQuery<BoxedExpression, Variable> {
+		protected IExpressionContextProvider<Expression, Variable> ContextProvider;
+		protected IFactBase<Variable> FactBase;
+		protected Predicate<APC> isUnreachable;
+
+		public BasicFacts (IExpressionContextProvider<Expression, Variable> contextProvider, IFactBase<Variable> factBase, Predicate<APC> isUnreachable)
+		{
+			this.ContextProvider = contextProvider;
+			this.FactBase = factBase;
+			this.isUnreachable = isUnreachable;
+		}
+
+		#region Implementation of IFactBase<Variable>
+        public FlatDomain<bool> IsNull(APC pc, Variable variable)
+		{
+			return this.FactBase.IsNull (pc, variable);
+		}
+
+        public FlatDomain<bool> IsNonNull(APC pc, Variable variable)
+		{
+			return this.FactBase.IsNonNull (pc, variable);
+		}
+
+		public bool IsUnreachable (APC pc)
+		{
+			if (this.isUnreachable != null && this.isUnreachable (pc))
+				return true;
+
+			return this.FactBase.IsUnreachable (pc);
+		}
+
+		protected static bool TryVariable (BoxedExpression e, out Variable v)
+		{
+			object underlyingVariable = e.UnderlyingVariable;
+			if (underlyingVariable is Variable) {
+				v = (Variable) underlyingVariable;
+				return true;
+			}
+
+			v = default(Variable);
+			return false;
+		}
+		#endregion
+
+		#region Implementation of IFactQuery<BoxedExpression,Variable>
+        public virtual FlatDomain<bool> IsNull(APC pc, BoxedExpression expr)
+		{
+			Variable v;
+			if (TryVariable (expr, out v)) {
+                FlatDomain<bool> outcome = this.FactBase.IsNull(pc, v);
+				if (!outcome.IsTop)
+					return outcome;
+			}
+			return ProofOutcome.Top;
+		}
+
+        public virtual FlatDomain<bool> IsNonNull(APC pc, BoxedExpression expr)
+		{
+			Variable v;
+			if (TryVariable (expr, out v)) {
+                FlatDomain<bool> outcome = this.FactBase.IsNonNull(pc, v);
+				if (!outcome.IsTop)
+					return outcome;
+			}
+			return ProofOutcome.Top;
+		}
+
+        public FlatDomain<bool> IsTrue(APC pc, BoxedExpression expr)
+		{
+			return IsNonZero (pc, expr);
+		}
+
+        public FlatDomain<bool> IsTrueImply(APC pc, Sequence<BoxedExpression> positiveAssumptions, Sequence<BoxedExpression> negativeAssumptions, BoxedExpression goal)
+		{
+            FlatDomain<bool> outcome = IsTrue(pc, goal);
+            if (outcome.IsTrue() || outcome.IsBottom)
+                return outcome;
+
+            return ProofOutcome.Top;
+		}
+
+        public FlatDomain<bool> IsGreaterEqualToZero(APC pc, BoxedExpression expr)
+		{
+			return ProofOutcome.Top;
+		}
+
+        public FlatDomain<bool> IsLessThan(APC pc, BoxedExpression expr, BoxedExpression right)
+		{
+			return ProofOutcome.Top;
+		}
+
+        public FlatDomain<bool> IsNonZero(APC pc, BoxedExpression expr)
+		{
+			return IsNonNull (pc, expr);
+		}
+		#endregion
+	}
+}

mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/BoxedExpressionExtensions.cs

@@ -0,0 +1,167 @@
+// 
+// BoxedExpressionExtensions.cs
+// 
+// Authors:
+// 	Alexander Chebaturkin (chebaturkin@gmail.com)
+// 
+// Copyright (C) 2011 Alexander Chebaturkin
+// 
+// Permission is hereby granted, free of charge, to any person obtaining
+// a copy of this software and associated documentation files (the
+// "Software"), to deal in the Software without restriction, including
+// without limitation the rights to use, copy, modify, merge, publish,
+// distribute, sublicense, and/or sell copies of the Software, and to
+// permit persons to whom the Software is furnished to do so, subject to
+// the following conditions:
+// 
+// The above copyright notice and this permission notice shall be
+// included in all copies or substantial portions of the Software.
+//  
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 
+// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+// 
+
+using System;
+
+using Mono.CodeContracts.Static.AST;
+using Mono.CodeContracts.Static.DataStructures;
+
+namespace Mono.CodeContracts.Static.Proving
+{
+	static class BoxedExpressionExtensions
+	{
+		public static bool IsConstantIntOrNull(this BoxedExpression e, out int res)
+		{
+			res = 0;
+			if (e.IsConstant) {
+				IConvertible convertible = e.Constant as IConvertible;
+				if (convertible != null) {
+					if (e.Constant is string || e.Constant is float || e.Constant is double)
+						return false;
+
+					try {
+						res = convertible.ToInt32 (null);
+						return true;
+					} catch {
+					}
+				}
+				if (e.Constant == null)
+					return true;
+			}
+			return false;
+		}
+
+                public static bool IsConstantBool(this BoxedExpression e, out bool result)
+                {
+                        if (e.IsConstant && e.Constant is bool)
+                                return true.With ((bool) e.Constant, out result);
+
+                        return false.Without (out result);
+                }
+
+                public static bool IsTrivialCondition(this BoxedExpression e, out bool result)
+                {
+                        int value;
+                        if (e.IsConstantIntOrNull (out value))
+                                return true.With (value != 0, out result);
+                        if (e.IsConstantBool (out result))
+                                return true;
+
+                        BinaryOperator bop;
+                        BoxedExpression left;
+                        BoxedExpression right;
+                        if (e.IsBinaryExpression (out bop, out left, out right)) {
+                                int l, r;
+                                var isLeftInt = left.IsConstantIntOrNull (out l);
+                                var isRightInt = right.IsConstantIntOrNull (out r);
+                                if (bop == BinaryOperator.Ceq) {
+                                        if (isLeftInt && isRightInt)
+                                                return true.With (l == r, out result);
+                                        bool leftResult;
+                                        if (isRightInt && r == 0 && left.IsTrivialCondition (out leftResult))
+                                                return true.With (!leftResult, out result);
+
+                                        bool rightResult;
+                                        if (isLeftInt && l == 0 && right.IsTrivialCondition (out rightResult))
+                                                return true.With (!rightResult, out result);
+
+                                        return false.Without (out result);
+                                }
+
+                                switch (bop) {
+                                        case BinaryOperator.Add:
+                                        case BinaryOperator.Add_Ovf:
+                                        case BinaryOperator.Add_Ovf_Un:
+                                                return true.With (l + r != 0, out result);
+                                        case BinaryOperator.And:
+                                                return true.With ((l & r) != 0, out result);
+                                        case BinaryOperator.Cne_Un:
+                                                return true.With (l != r, out result);
+                                        case BinaryOperator.Cge:
+                                                return true.With (l >= r, out result);
+                                        case BinaryOperator.Cge_Un:
+                                                return true.With ((uint) l >= (uint) r, out result);
+                                        case BinaryOperator.Cgt:
+                                                return true.With (l > r, out result);
+                                        case BinaryOperator.Cgt_Un:
+                                                return true.With ((uint) l > (uint) r, out result);
+                                        case BinaryOperator.Cle:
+                                                return true.With (l <= r, out result);
+                                        case BinaryOperator.Cle_Un:
+                                                return true.With ((uint) l <= (uint) r, out result);
+                                        case BinaryOperator.Clt:
+                                                return true.With (l < r, out result);
+                                        case BinaryOperator.Clt_Un:
+                                                return true.With ((uint) l < (uint) r, out result);
+                                        case BinaryOperator.Div:
+                                                if (r == 0)
+                                                        return false.Without (out result);
+                                                return true.With (l / r != 0, out result);
+                                        case BinaryOperator.Div_Un:
+                                                if (r == 0)
+                                                        return false.Without (out result);
+                                                return true.With ((uint) l / (uint) r != 0, out result);
+                                        case BinaryOperator.LogicalAnd:
+                                                return true.With (l != 0 && r != 0, out result);
+                                        case BinaryOperator.LogicalOr:
+                                                return true.With (l != 0 || r != 0, out result);
+                                        case BinaryOperator.Mul:
+                                        case BinaryOperator.Mul_Ovf:
+                                        case BinaryOperator.Mul_Ovf_Un:
+                                                return true.With (l * r != 0, out result);
+                                        case BinaryOperator.Or:
+                                                return true.With ((l | r) != 0, out result);
+                                        case BinaryOperator.Rem:
+                                                if (r == 0)
+                                                        return false.Without (out result);
+                                                return true.With (l % r != 0, out result);
+                                        case BinaryOperator.Rem_Un:
+                                                if (r == 0)
+                                                        return false.Without (out result);
+                                                return true.With (((uint) l) % ((uint) r) != 0, out result);
+                                        case BinaryOperator.Shl:
+                                                return true.With (l << r != 0, out result);
+                                        case BinaryOperator.Shr:
+                                                return true.With (l >> r != 0, out result);
+                                        case BinaryOperator.Shr_Un:
+                                                return true.With (((uint) l) >> r != 0, out result);
+                                        case BinaryOperator.Sub:
+                                        case BinaryOperator.Sub_Ovf:
+                                        case BinaryOperator.Sub_Ovf_Un:
+                                                return true.With (l - r != 0, out result);
+                                        case BinaryOperator.Xor:
+                                                return true.With ((l ^ r) != 0, out result);
+                                        default:
+                                                return false.Without (out result);
+                                }
+                        }
+
+                        return false.Without (out result);
+                }
+	}
+}

mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/ComposedFactQuery.cs

@@ -0,0 +1,166 @@
+// 
+// ComposedFactQuery.cs
+// 
+// Authors:
+// 	Alexander Chebaturkin (chebaturkin@gmail.com)
+// 
+// Copyright (C) 2011 Alexander Chebaturkin
+// 
+// Permission is hereby granted, free of charge, to any person obtaining
+// a copy of this software and associated documentation files (the
+// "Software"), to deal in the Software without restriction, including
+// without limitation the rights to use, copy, modify, merge, publish,
+// distribute, sublicense, and/or sell copies of the Software, and to
+// permit persons to whom the Software is furnished to do so, subject to
+// the following conditions:
+// 
+// The above copyright notice and this permission notice shall be
+// included in all copies or substantial portions of the Software.
+//  
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 
+// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+// 
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using Mono.CodeContracts.Static.AST;
+using Mono.CodeContracts.Static.ControlFlow;
+using Mono.CodeContracts.Static.DataStructures;
+using Mono.CodeContracts.Static.Lattices;
+
+namespace Mono.CodeContracts.Static.Proving
+{
+	class ComposedFactQuery<Variable> : IFactQuery<BoxedExpression, Variable>
+	{
+		private List<IFactQuery<BoxedExpression, Variable>> elements = new List<IFactQuery<BoxedExpression, Variable>> ();
+		private Predicate<APC> isUnreachable;
+
+		public ComposedFactQuery(Predicate<APC> isUnreachable )
+		{
+			this.isUnreachable = isUnreachable;
+		}
+
+		public void Add(IFactQuery<BoxedExpression, Variable> item)
+		{
+			if (item == null)
+				return;
+			this.elements.Add (item);
+		}
+
+		#region Implementation of IFactBase<Variable>
+		public FlatDomain<bool> IsNull(APC pc, Variable variable)
+		{
+			return elements.Select(fact => fact.IsNull(pc, variable)).FirstOrDefault(factResult => !factResult.IsTop);
+		}
+
+        public FlatDomain<bool> IsNonNull(APC pc, Variable variable)
+		{
+            return elements.Select(fact => fact.IsNonNull(pc, variable)).FirstOrDefault(factResult => !factResult.IsTop);
+		}
+
+		public bool IsUnreachable(APC pc)
+		{
+			if (this.isUnreachable != null && this.isUnreachable(pc))
+				return true;
+			return elements.Any (factQuery => factQuery.IsUnreachable (pc));
+		}
+		#endregion
+
+		#region Implementation of IFactQuery<BoxedExpression,Variable>
+        public FlatDomain<bool> IsNull(APC pc, BoxedExpression expr)
+		{
+            return elements.Select(fact => fact.IsNull(pc, expr)).FirstOrDefault(factResult => !factResult.IsTop);
+		}
+
+        public FlatDomain<bool> IsNonNull(APC pc, BoxedExpression expr)
+		{
+            return elements.Select(fact => fact.IsNonNull(pc, expr)).FirstOrDefault(factResult => !factResult.IsTop);
+		}
+
+        public FlatDomain<bool> IsTrue(APC pc, BoxedExpression expr)
+		{
+            FlatDomain<bool> res = ProofOutcome.Top;
+			foreach (var factQuery in elements) {
+				var outcome = factQuery.IsTrue (pc, expr);
+
+                if (outcome.IsTrue() || outcome.IsBottom)
+                    return outcome;
+			    if (outcome.IsFalse ())
+			        res = outcome;
+			}
+			if (!res.IsTop)
+				return res;
+
+			BinaryOperator op;
+			BoxedExpression left;
+			BoxedExpression right;
+			if (expr.IsBinaryExpression (out op, out left, out right)) {
+				if ((op == BinaryOperator.Ceq || op == BinaryOperator.Cobjeq) && this.IsRelational (left) && this.IsNull (pc, right).IsTrue ()) {
+					var outcome = this.IsTrue (pc, left);
+				    return outcome.Negate ();
+				}
+				int leftInt;
+				int rightInt;
+				if (op == BinaryOperator.Ceq && left.IsConstantIntOrNull (out leftInt) && right.IsConstantIntOrNull (out rightInt))
+					return leftInt == rightInt ? ProofOutcome.True : ProofOutcome.False;
+			}
+
+			if (expr.IsUnary && expr.UnaryOperator == UnaryOperator.Not) {
+				var outcome = this.IsTrue (pc, expr.UnaryArgument);
+			    return outcome.Negate ();
+			} 
+
+			return ProofOutcome.Top;
+		}
+
+		private bool IsRelational(BoxedExpression e)
+		{
+			BinaryOperator op;
+			BoxedExpression left;
+			BoxedExpression right;
+			if (e.IsBinaryExpression (out op, out left, out right))
+				switch (op) {
+					case BinaryOperator.Ceq:
+					case BinaryOperator.Cobjeq:
+					case BinaryOperator.Cne_Un:
+					case BinaryOperator.Cge:
+					case BinaryOperator.Cge_Un:
+					case BinaryOperator.Cgt:
+					case BinaryOperator.Cgt_Un:
+					case BinaryOperator.Cle:
+					case BinaryOperator.Cle_Un:
+					case BinaryOperator.Clt:
+					case BinaryOperator.Clt_Un:
+						return true;
+				}
+			return false;
+		}
+
+		public FlatDomain<bool> IsTrueImply(APC pc, Sequence<BoxedExpression> positiveAssumptions, Sequence<BoxedExpression> negativeAssumptions, BoxedExpression goal)
+		{
+            return elements.Select(fact => fact.IsTrueImply(pc, positiveAssumptions, negativeAssumptions, goal)).FirstOrDefault(factResult => !factResult.IsTop);
+		}
+
+        public FlatDomain<bool> IsGreaterEqualToZero(APC pc, BoxedExpression expr)
+		{
+			return elements.Select(fact => fact.IsGreaterEqualToZero(pc, expr)).FirstOrDefault(factResult => !factResult.IsTop);
+		}
+
+        public FlatDomain<bool> IsLessThan(APC pc, BoxedExpression expr, BoxedExpression right)
+		{
+            return elements.Select(fact => fact.IsLessThan(pc, expr, right)).FirstOrDefault(factResult => !factResult.IsTop);
+		}
+
+        public FlatDomain<bool> IsNonZero(APC pc, BoxedExpression expr)
+		{
+            return elements.Select(fact => fact.IsNonZero(pc, expr)).FirstOrDefault(factResult => !factResult.IsTop);
+		}
+		#endregion
+	}
+}

mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/ConstantPropagationFactQuery.cs

@@ -0,0 +1,182 @@
+// 
+// ConstantPropagationFactQuery.cs
+// 
+// Authors:
+// 	Alexander Chebaturkin (chebaturkin@gmail.com)
+// 
+// Copyright (C) 2011 Alexander Chebaturkin
+// 
+// Permission is hereby granted, free of charge, to any person obtaining
+// a copy of this software and associated documentation files (the
+// "Software"), to deal in the Software without restriction, including
+// without limitation the rights to use, copy, modify, merge, publish,
+// distribute, sublicense, and/or sell copies of the Software, and to
+// permit persons to whom the Software is furnished to do so, subject to
+// the following conditions:
+// 
+// The above copyright notice and this permission notice shall be
+// included in all copies or substantial portions of the Software.
+//  
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 
+// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+// 
+
+using Mono.CodeContracts.Static.AST;
+using Mono.CodeContracts.Static.ControlFlow;
+using Mono.CodeContracts.Static.DataStructures;
+using Mono.CodeContracts.Static.Lattices;
+
+namespace Mono.CodeContracts.Static.Proving
+{
+	class ConstantPropagationFactQuery<Variable> : IFactQuery<BoxedExpression, Variable> {
+		#region Implementation of IFactBase<Variable>
+        public bool IsUnreachable(APC pc)
+        {
+            return false;
+        }
+
+		public FlatDomain<bool> IsNull(APC pc, Variable variable)
+		{
+			return ProofOutcome.Top;
+		}
+
+        public FlatDomain<bool> IsNonNull(APC pc, Variable variable)
+		{
+			return ProofOutcome.Top;
+		}
+		#endregion
+
+		#region Implementation of IFactQuery<BoxedExpression,Variable>
+        public FlatDomain<bool> IsNull(APC pc, BoxedExpression expr)
+		{
+			int num;
+			if (expr.IsConstantIntOrNull (out num))
+				return (num == 0).ToTrueOrTop ();
+
+			return ProofOutcome.Top;
+		}
+
+        public FlatDomain<bool> IsNonNull(APC pc, BoxedExpression expr)
+		{
+			int num;
+			if (expr.IsConstantIntOrNull (out num))
+				return (num != 0).ToTrueOrTop ();
+
+			return ProofOutcome.Top;
+		}
+
+        public FlatDomain<bool> IsTrue(APC pc, BoxedExpression expr)
+		{
+			int num;
+			if (expr.IsConstantIntOrNull (out num))
+				return (num != 0).ToTrueOrTop ();
+
+			return ConstantFact (expr);
+		}
+
+        public FlatDomain<bool> IsTrueImply(APC pc, Sequence<BoxedExpression> positiveAssumptions, Sequence<BoxedExpression> negativeAssumptions, BoxedExpression goal)
+		{
+			UnaryOperator op;
+			BoxedExpression arg;
+			while (goal.IsUnaryExpression (out op, out arg) && op.IsConversionOperator ())
+				goal = arg;
+
+			if (positiveAssumptions.Any(assumption => assumption.Equals (goal)))
+				return ProofOutcome.True;
+
+			return ProofOutcome.Top;
+		}
+
+        public FlatDomain<bool> IsGreaterEqualToZero(APC pc, BoxedExpression expr)
+		{
+			int num;
+			if (expr.IsConstantIntOrNull(out num))
+				return (num >= 0).ToTrueOrTop ();
+
+			return ProofOutcome.Top;
+		}
+
+        public FlatDomain<bool> IsLessThan(APC pc, BoxedExpression left, BoxedExpression right)
+		{
+			int l;
+			int r;
+			if (left.IsConstantIntOrNull(out l) && right.IsConstantIntOrNull(out r))
+				return (l < r).ToTrueOrTop ();
+
+			return ProofOutcome.Top;
+		}
+
+        public FlatDomain<bool> IsNonZero(APC pc, BoxedExpression expr)
+		{
+			int num;
+			if (expr.IsConstantIntOrNull(out num))
+				return (num != 0).ToTrueOrTop ();
+
+			return ProofOutcome.Top;
+		}
+
+        private static FlatDomain<bool> ConstantFact(BoxedExpression expr)
+		{
+			BinaryOperator op;
+			BoxedExpression left;
+			BoxedExpression right;
+			if (expr.IsBinaryExpression (out op, out left, out right)) {
+				int l;
+				var leftIsInt = left.IsConstantIntOrNull (out l);
+				
+				int r;
+				var rightIsInt = right.IsConstantIntOrNull(out r);
+
+				if (leftIsInt || rightIsInt) {
+					if (leftIsInt && rightIsInt) {
+						switch (op) {
+							case BinaryOperator.Add:        return ((l + r) != 0).ToTrueOrTop ();
+							case BinaryOperator.And:        return ((l & r) != 0).ToTrueOrTop ();
+							case BinaryOperator.Ceq:        return (l == r).ToTrueOrTop ();
+							case BinaryOperator.Cobjeq:     return ProofOutcome.Top;
+							case BinaryOperator.Cne_Un:     return (l != r).ToTrueOrTop ();
+							case BinaryOperator.Cge:        return (l >= r).ToTrueOrTop ();
+							case BinaryOperator.Cge_Un:     return ((uint)l >= (uint)r).ToTrueOrTop ();
+							case BinaryOperator.Cgt:        return (l > r).ToTrueOrTop ();
+							case BinaryOperator.Cgt_Un:     return ((uint)l > (uint)r).ToTrueOrTop ();
+							case BinaryOperator.Cle:        return (l <= r).ToTrueOrTop ();
+							case BinaryOperator.Cle_Un:     return ((uint)l <= (uint)r).ToTrueOrTop ();
+							case BinaryOperator.Clt:        return (l < r).ToTrueOrTop ();
+							case BinaryOperator.Clt_Un:     return ((uint)l < (uint)r).ToTrueOrTop ();
+							case BinaryOperator.Div:        return (r != 0 && ((l / r) != 0)).ToTrueOrTop ();
+							case BinaryOperator.LogicalAnd: return (l != 0 && r != 0).ToTrueOrTop ();
+							case BinaryOperator.LogicalOr:  return (l != 0 || r != 0).ToTrueOrTop ();
+							case BinaryOperator.Mul:        return (l * r != 0).ToTrueOrTop ();
+							case BinaryOperator.Or:         return ((l | r) != 0).ToTrueOrTop ();
+							case BinaryOperator.Rem:        return (r != 0 && (l % r != 0)).ToTrueOrTop ();
+							case BinaryOperator.Shl:        return (l << r != 0).ToTrueOrTop ();
+							case BinaryOperator.Shr:        return (l >> r != 0).ToTrueOrTop ();
+							case BinaryOperator.Sub:        return (l - r != 0).ToTrueOrTop ();
+							case BinaryOperator.Xor:        return ((l ^ r) != 0).ToTrueOrTop ();
+						}
+					}
+					if (op == BinaryOperator.Ceq && (leftIsInt && l == 0 || rightIsInt && r == 0))
+						return ConstantFact (left).Negate ();
+				}
+				else if (left.IsConstant && right.IsConstant) {
+					var lConst = left.Constant;
+					var rConst = right.Constant;
+					switch (op) {
+						case BinaryOperator.Cobjeq:
+							return lConst == null ? (rConst == null).ToTrueOrTop () : lConst.Equals (rConst).ToTrueOrTop ();
+						case BinaryOperator.Cne_Un:
+							return lConst == null ? (rConst != null).ToTrueOrTop () : (!lConst.Equals (rConst)).ToTrueOrTop ();
+					}
+				}
+			}
+
+			return ProofOutcome.Top;
+		}
+		#endregion
+	}
+}

mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/IFactBase.cs

@@ -0,0 +1,39 @@
+// 
+// IFactBase.cs
+// 
+// Authors:
+// 	Alexander Chebaturkin (chebaturkin@gmail.com)
+// 
+// Copyright (C) 2011 Alexander Chebaturkin
+// 
+// Permission is hereby granted, free of charge, to any person obtaining
+// a copy of this software and associated documentation files (the
+// "Software"), to deal in the Software without restriction, including
+// without limitation the rights to use, copy, modify, merge, publish,
+// distribute, sublicense, and/or sell copies of the Software, and to
+// permit persons to whom the Software is furnished to do so, subject to
+// the following conditions:
+// 
+// The above copyright notice and this permission notice shall be
+// included in all copies or substantial portions of the Software.
+//  
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 
+// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+// 
+
+using Mono.CodeContracts.Static.ControlFlow;
+using Mono.CodeContracts.Static.Lattices;
+
+namespace Mono.CodeContracts.Static.Proving {
+	interface IFactBase<in Variable> {
+        bool IsUnreachable(APC pc);
+
+		FlatDomain<bool> IsNull (APC pc, Variable variable);
+        FlatDomain<bool> IsNonNull(APC pc, Variable variable);
+	}
+}

mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/IFactQuery.cs

@@ -0,0 +1,43 @@
+// 
+// IFactQuery.cs
+// 
+// Authors:
+// 	Alexander Chebaturkin (chebaturkin@gmail.com)
+// 
+// Copyright (C) 2011 Alexander Chebaturkin
+// 
+// Permission is hereby granted, free of charge, to any person obtaining
+// a copy of this software and associated documentation files (the
+// "Software"), to deal in the Software without restriction, including
+// without limitation the rights to use, copy, modify, merge, publish,
+// distribute, sublicense, and/or sell copies of the Software, and to
+// permit persons to whom the Software is furnished to do so, subject to
+// the following conditions:
+// 
+// The above copyright notice and this permission notice shall be
+// included in all copies or substantial portions of the Software.
+//  
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 
+// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+// 
+
+using Mono.CodeContracts.Static.ControlFlow;
+using Mono.CodeContracts.Static.DataStructures;
+using Mono.CodeContracts.Static.Lattices;
+
+namespace Mono.CodeContracts.Static.Proving {
+	interface IFactQuery<Expression, Variable> : IFactBase<Variable> {
+        FlatDomain<bool> IsNull(APC pc, Expression expr);
+        FlatDomain<bool> IsNonNull(APC pc, Expression expr);
+        FlatDomain<bool> IsTrue(APC pc, Expression expr);
+        FlatDomain<bool> IsTrueImply(APC pc, Sequence<Expression> positiveAssumptions, Sequence<Expression> negativeAssumptions, Expression goal);
+        FlatDomain<bool> IsGreaterEqualToZero(APC pc, Expression expr);
+        FlatDomain<bool> IsLessThan(APC pc, Expression expr, Expression right);
+        FlatDomain<bool> IsNonZero(APC pc, Expression expr);
+	}
+}

mcs/class/Mono.CodeContracts/Mono.CodeContracts.Static.Proving/SimpleLogicInference.cs

@@ -0,0 +1,113 @@
+// 
+// SimpleLogicInference.cs
+// 
+// Authors:
+// 	Alexander Chebaturkin (chebaturkin@gmail.com)
+// 
+// Copyright (C) 2011 Alexander Chebaturkin
+// 
+// Permission is hereby granted, free of charge, to any person obtaining
+// a copy of this software and associated documentation files (the
+// "Software"), to deal in the Software without restriction, including
+// without limitation the rights to use, copy, modify, merge, publish,
+// distribute, sublicense, and/or sell copies of the Software, and to
+// permit persons to whom the Software is furnished to do so, subject to
+// the following conditions:
+// 
+// The above copyright notice and this permission notice shall be
+// included in all copies or substantial portions of the Software.
+//  
+// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+// EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF 
+// MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+// NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+// LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+// OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+// WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+// 
+
+using System;
+using Mono.CodeContracts.Static.AST;
+using Mono.CodeContracts.Static.Analysis;
+using Mono.CodeContracts.Static.Analysis.Numerical;
+using Mono.CodeContracts.Static.ControlFlow;
+using Mono.CodeContracts.Static.Lattices;
+
+namespace Mono.CodeContracts.Static.Proving {
+	class SimpleLogicInference<Expression, Variable> : BasicFacts<Expression, Variable> {
+		public SimpleLogicInference (IExpressionContextProvider<Expression, Variable> contextProvider, IFactBase<Variable> factBase, Predicate<APC> isUnreachable)
+			: base (contextProvider, factBase, isUnreachable)
+		{
+		}
+
+        public override FlatDomain<bool> IsNull(APC pc, BoxedExpression expr)
+		{
+			Variable v;
+			if (TryVariable (expr, out v)) {
+                FlatDomain<bool> proofOutcome = this.FactBase.IsNull(pc, v);
+				if (!proofOutcome.IsTop)
+					return proofOutcome;
+			}
+
+			if (expr.IsConstant) {
+				object constant = expr.Constant;
+				if (constant == null)
+					return ProofOutcome.True;
+				if (constant is string)
+					return ProofOutcome.False;
+
+			    long? longValue = constant.ConvertToLong ();
+                if (longValue.HasValue)
+                    return longValue == 0 ? ProofOutcome.True : ProofOutcome.False;
+                
+                return ProofOutcome.Top;
+			}
+
+			BinaryOperator op;
+			BoxedExpression left;
+			BoxedExpression right;
+			if (expr.IsBinaryExpression (out op, out left, out right)) {
+				if ((op == BinaryOperator.Ceq || op == BinaryOperator.Cobjeq) && IsNull (pc, right).IsTrue ())
+					return IsNonNull (pc, left);
+				if (op == BinaryOperator.Cne_Un && IsNull (pc, right).IsTrue ())
+					return IsNull (pc, left);
+			}
+			return ProofOutcome.Top;
+		}
+
+        public override FlatDomain<bool> IsNonNull(APC pc, BoxedExpression expr)
+		{
+			Variable v;
+			if (TryVariable (expr, out v)) {
+                FlatDomain<bool> proofOutcome = this.FactBase.IsNonNull(pc, v);
+				if (!proofOutcome.IsTop)
+					return proofOutcome;
+			}
+
+			if (expr.IsConstant) {
+				object constant = expr.Constant;
+				if (constant == null)
+					return ProofOutcome.False;
+				if (constant is string)
+					return ProofOutcome.True;
+                
+                long? longValue = constant.ConvertToLong();
+                if (longValue.HasValue)
+                    return longValue != 0 ? ProofOutcome.True : ProofOutcome.False;
+				
+                return ProofOutcome.Top;
+			}
+
+			BinaryOperator op;
+			BoxedExpression left;
+			BoxedExpression right;
+			if (expr.IsBinaryExpression (out op, out left, out right)) {
+				if ((op == BinaryOperator.Ceq || op == BinaryOperator.Cobjeq) && IsNull (pc, right).IsTrue ())
+					return IsNull (pc, left);
+				if (op == BinaryOperator.Cne_Un && IsNull (pc, right).IsTrue ())
+					return IsNonNull (pc, left);
+			}
+			return ProofOutcome.Top;
+		}
+	}
+}