From e81605e480d055843132b41a58451e4ab2cf18b0 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Fri, 13 Aug 2010 00:44:20 +0000 Subject: Boogie: Committing new source code for VCExpr --- Source/VCExpr/VCExprASTVisitors.cs | 1546 +++++++++++++++++++++++------------- 1 file changed, 984 insertions(+), 562 deletions(-) (limited to 'Source/VCExpr/VCExprASTVisitors.cs') diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index c9d56962..4a13cbb5 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -8,51 +8,223 @@ using System.Text; using System.IO; using System.Collections; using System.Collections.Generic; -using Microsoft.Contracts; +using System.Diagnostics.Contracts; using Microsoft.Basetypes; // Some visitor skeletons for the VCExpression AST -namespace Microsoft.Boogie.VCExprAST -{ +namespace Microsoft.Boogie.VCExprAST { using Microsoft.Boogie; - public interface IVCExprVisitor { - Result Visit(VCExprLiteral! node, Arg arg); - Result Visit(VCExprNAry! node, Arg arg); - Result Visit(VCExprVar! node, Arg arg); - Result Visit(VCExprQuantifier! node, Arg arg); - Result Visit(VCExprLet! node, Arg arg); + [ContractClass(typeof(IVCExprVisitorContracts<,>))] + public interface IVCExprVisitor { + Result Visit(VCExprLiteral/*!*/ node, Arg arg); + Result Visit(VCExprNAry/*!*/ node, Arg arg); + Result Visit(VCExprVar/*!*/ node, Arg arg); + Result Visit(VCExprQuantifier/*!*/ node, Arg arg); + Result Visit(VCExprLet/*!*/ node, Arg arg); } + [ContractClassFor(typeof(IVCExprVisitor<,>))] + public abstract class IVCExprVisitorContracts : IVCExprVisitor { + #region IVCExprVisitor Members + public Result Visit(VCExprLiteral node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result Visit(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result Visit(VCExprVar node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result Visit(VCExprQuantifier node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result Visit(VCExprLet node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + #endregion + } + [ContractClass(typeof(IVCExprOpVisitorContracts<,>))] public interface IVCExprOpVisitor { - Result VisitNotOp (VCExprNAry! node, Arg arg); - Result VisitEqOp (VCExprNAry! node, Arg arg); - Result VisitNeqOp (VCExprNAry! node, Arg arg); - Result VisitAndOp (VCExprNAry! node, Arg arg); - Result VisitOrOp (VCExprNAry! node, Arg arg); - Result VisitImpliesOp (VCExprNAry! node, Arg arg); - Result VisitDistinctOp (VCExprNAry! node, Arg arg); - Result VisitLabelOp (VCExprNAry! node, Arg arg); - Result VisitSelectOp (VCExprNAry! node, Arg arg); - Result VisitStoreOp (VCExprNAry! node, Arg arg); - Result VisitBvOp (VCExprNAry! node, Arg arg); - Result VisitBvExtractOp(VCExprNAry! node, Arg arg); - Result VisitBvConcatOp (VCExprNAry! node, Arg arg); - Result VisitAddOp (VCExprNAry! node, Arg arg); - Result VisitSubOp (VCExprNAry! node, Arg arg); - Result VisitMulOp (VCExprNAry! node, Arg arg); - Result VisitDivOp (VCExprNAry! node, Arg arg); - Result VisitModOp (VCExprNAry! node, Arg arg); - Result VisitLtOp (VCExprNAry! node, Arg arg); - Result VisitLeOp (VCExprNAry! node, Arg arg); - Result VisitGtOp (VCExprNAry! node, Arg arg); - Result VisitGeOp (VCExprNAry! node, Arg arg); - Result VisitSubtypeOp (VCExprNAry! node, Arg arg); - Result VisitSubtype3Op (VCExprNAry! node, Arg arg); - Result VisitBoogieFunctionOp (VCExprNAry! node, Arg arg); - Result VisitIfThenElseOp (VCExprNAry! node, Arg arg); - Result VisitCustomOp (VCExprNAry! node, Arg arg); + Result VisitNotOp(VCExprNAry node, Arg arg); + Result VisitEqOp(VCExprNAry node, Arg arg); + Result VisitNeqOp(VCExprNAry node, Arg arg); + Result VisitAndOp(VCExprNAry node, Arg arg); + Result VisitOrOp(VCExprNAry node, Arg arg); + Result VisitImpliesOp(VCExprNAry node, Arg arg); + Result VisitDistinctOp(VCExprNAry node, Arg arg); + Result VisitLabelOp(VCExprNAry node, Arg arg); + Result VisitSelectOp(VCExprNAry node, Arg arg); + Result VisitStoreOp(VCExprNAry node, Arg arg); + Result VisitBvOp(VCExprNAry node, Arg arg); + Result VisitBvExtractOp(VCExprNAry node, Arg arg); + Result VisitBvConcatOp(VCExprNAry node, Arg arg); + Result VisitAddOp(VCExprNAry node, Arg arg); + Result VisitSubOp(VCExprNAry node, Arg arg); + Result VisitMulOp(VCExprNAry node, Arg arg); + Result VisitDivOp(VCExprNAry node, Arg arg); + Result VisitModOp(VCExprNAry node, Arg arg); + Result VisitLtOp(VCExprNAry node, Arg arg); + Result VisitLeOp(VCExprNAry node, Arg arg); + Result VisitGtOp(VCExprNAry node, Arg arg); + Result VisitGeOp(VCExprNAry node, Arg arg); + Result VisitSubtypeOp(VCExprNAry node, Arg arg); + Result VisitSubtype3Op(VCExprNAry node, Arg arg); + Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg); + Result VisitIfThenElseOp(VCExprNAry node, Arg arg); + Result VisitCustomOp (VCExprNAry node, Arg arg); + } + [ContractClassFor(typeof(IVCExprOpVisitor<,>))] + public abstract class IVCExprOpVisitorContracts:IVCExprOpVisitor { + #region IVCExprOpVisitor Members + + public Result VisitNotOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitEqOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitNeqOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitAndOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitOrOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitImpliesOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitDistinctOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitLabelOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitSelectOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitStoreOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitBvOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitBvExtractOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitBvConcatOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitAddOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitSubOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitMulOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitDivOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitModOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitLtOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitLeOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitGtOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitGeOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitSubtypeOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitSubtype3Op(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitIfThenElseOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + public Result VisitCustomOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + + #endregion } ////////////////////////////////////////////////////////////////////////////// @@ -64,29 +236,35 @@ namespace Microsoft.Boogie.VCExprAST // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary // to avoid stack overflows + + [ContractClass(typeof(TraversingVCExprVisitorContracts<,>))] public abstract class TraversingVCExprVisitor : IVCExprVisitor { - protected abstract Result StandardResult(VCExpr! node, Arg arg); + protected abstract Result StandardResult(VCExpr/*!*/ node, Arg arg); - public Result Traverse(VCExpr! node, Arg arg) { + public Result Traverse(VCExpr node, Arg arg) { + Contract.Requires(node != null); return node.Accept(this, arg); } - public virtual Result Visit(VCExprLiteral! node, Arg arg) { + public virtual Result Visit(VCExprLiteral node, Arg arg) { + Contract.Requires(node != null); return StandardResult(node, arg); } - public virtual Result Visit(VCExprNAry! node, Arg arg) { + public virtual Result Visit(VCExprNAry node, Arg arg){ +Contract.Requires(node != null); Result res = StandardResult(node, arg); if (node.TypeParamArity == 0) { - VCExprOp! op = node.Op; + Contract.Assert(node.Op != null); + VCExprOp op = node.Op; IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node); enumerator.MoveNext(); // skip the node itself while (enumerator.MoveNext()) { - VCExpr! expr = (VCExpr!)enumerator.Current; + VCExpr/*!*/ expr = cce.NonNull((VCExpr/*!*/)enumerator.Current); VCExprNAry naryExpr = expr as VCExprNAry; if (naryExpr == null || !naryExpr.Op.Equals(op)) { expr.Accept(this, arg); @@ -95,34 +273,45 @@ namespace Microsoft.Boogie.VCExprAST } } } else { - foreach (VCExpr! e in node) - e.Accept(this, arg); + foreach (VCExpr e in node){Contract.Assert(e != null); + e.Accept(this, arg);} } return res; } - public virtual Result Visit(VCExprVar! node, Arg arg) { + public virtual Result Visit(VCExprVar node, Arg arg) { + Contract.Requires(node != null); return StandardResult(node, arg); } - public virtual Result Visit(VCExprQuantifier! node, Arg arg) { + public virtual Result Visit(VCExprQuantifier node, Arg arg){ +Contract.Requires(node != null); Result res = StandardResult(node, arg); - foreach (VCTrigger! trigger in node.Triggers) - foreach (VCExpr! expr in trigger.Exprs) - expr.Accept(this, arg); + foreach (VCTrigger/*!*/ trigger in node.Triggers){Contract.Assert(trigger != null); + foreach (VCExpr/*!*/ expr in trigger.Exprs) { + Contract.Assert(expr != null); + expr.Accept(this, arg);}} node.Body.Accept(this, arg); return res; } - public virtual Result Visit(VCExprLet! node, Arg arg) { + public virtual Result Visit(VCExprLet node, Arg arg){ +Contract.Requires(node != null); Result res = StandardResult(node, arg); // visit the bound expressions first - foreach (VCExprLetBinding! binding in node) - binding.E.Accept(this, arg); + foreach (VCExprLetBinding/*!*/ binding in node) { + Contract.Assert(binding != null); + binding.E.Accept(this, arg);} node.Body.Accept(this, arg); return res; } } - + [ContractClassFor(typeof(TraversingVCExprVisitor<,>))] + public abstract class TraversingVCExprVisitorContracts : TraversingVCExprVisitor { + protected override Result StandardResult(VCExpr node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + } ////////////////////////////////////////////////////////////////////////////// // Class to iterate over the nodes of a tree of VCExprNAry. This is // used to avoid handling such VCExpr recursively, which can easily @@ -130,13 +319,19 @@ namespace Microsoft.Boogie.VCExprAST public class VCExprNAryEnumerator : IEnumerator { - private readonly VCExprNAry! CompleteExpr; + private readonly VCExprNAry/*!*/ CompleteExpr; private VCExpr CurrentExpr = null; - private readonly Stack! ExprTodo = new Stack (); - - public VCExprNAryEnumerator(VCExprNAry! completeExpr) { + private readonly Stack/*!*/ ExprTodo = new Stack(); + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(CompleteExpr != null); + Contract.Invariant(cce.NonNullElements(ExprTodo)); + } + + public VCExprNAryEnumerator(VCExprNAry completeExpr){ +Contract.Requires(completeExpr != null); this.CompleteExpr = completeExpr; - Stack! exprTodo = new Stack (); + Stack/*!*/ exprTodo = new Stack(); exprTodo.Push(completeExpr); ExprTodo = exprTodo; } @@ -144,10 +339,11 @@ namespace Microsoft.Boogie.VCExprAST // Method using which a subclass can decide whether the // subexpressions of an expression should be enumerated as well // The default is to enumerate all nodes - protected virtual bool Descend(VCExprNAry! expr) { + protected virtual bool Descend(VCExprNAry expr) { + Contract.Requires(expr != null); return true; } - + //////////////////////////////////////////////////////////////////////////// public bool MoveNext() { @@ -160,14 +356,15 @@ namespace Microsoft.Boogie.VCExprAST for (int i = currentNAry.Arity - 1; i >= 0; --i) ExprTodo.Push(currentNAry[i]); } - + return true; } public object Current { get { - return (!)CurrentExpr; - } } + return cce.NonNull(CurrentExpr); + } + } public void Reset() { ExprTodo.Clear(); @@ -176,19 +373,27 @@ namespace Microsoft.Boogie.VCExprAST } } - + ////////////////////////////////////////////////////////////////////////////// public class VCExprNAryUniformOpEnumerator : VCExprNAryEnumerator { - private readonly VCExprOp! Op; - public VCExprNAryUniformOpEnumerator(VCExprNAry! completeExpr) { - base(completeExpr); + private readonly VCExprOp/*!*/ Op; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Op != null); + } + + public VCExprNAryUniformOpEnumerator(VCExprNAry completeExpr) + : base(completeExpr) { + Contract.Requires(completeExpr != null); + this.Op = completeExpr.Op; } - protected override bool Descend(VCExprNAry! expr) { + protected override bool Descend(VCExprNAry expr) { + Contract.Requires(expr != null); return expr.Op.Equals(Op) && - // we never skip nodes with type parameters - // (those are too interesting ...) + // we never skip nodes with type parameters + // (those are too interesting ...) expr.TypeParamArity == 0; } } @@ -200,19 +405,33 @@ namespace Microsoft.Boogie.VCExprAST : TraversingVCExprVisitor { // Maps with all variables bound above a certain location in the VCExpression. // The value of the map tells how often a particular symbol was bound - private readonly IDictionary! BoundTermVarsDict = - new Dictionary (); - private readonly IDictionary! BoundTypeVarsDict = - new Dictionary (); - - protected ICollection! BoundTermVars { get { - return BoundTermVarsDict.Keys; - } } - protected ICollection! BoundTypeVars { get { - return BoundTypeVarsDict.Keys; - } } - - private void AddBoundVar(IDictionary! dict, T! sym) { + private readonly IDictionary/*!*/ BoundTermVarsDict = + new Dictionary(); + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(BoundTermVarsDict)); + Contract.Invariant(cce.NonNullElements(BoundTypeVarsDict)); + } + + private readonly IDictionary/*!*/ BoundTypeVarsDict = + new Dictionary(); + + protected ICollection/*!*/ BoundTermVars { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return BoundTermVarsDict.Keys; + } + } + protected ICollection/*!*/ BoundTypeVars { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return BoundTypeVarsDict.Keys; + } + } + + private void AddBoundVar(IDictionary dict, T sym) { + Contract.Requires(sym != null); + Contract.Requires(cce.NonNullElements(dict)); int n; if (dict.TryGetValue(sym, out n)) dict[sym] = n + 1; @@ -220,47 +439,54 @@ namespace Microsoft.Boogie.VCExprAST dict[sym] = 1; } - private void RemoveBoundVar(IDictionary! dict, T! sym) { + private void RemoveBoundVar(IDictionary/*!*/ dict, T sym) { + Contract.Requires(sym != null); + Contract.Requires(cce.NonNullElements(dict)); int n; bool b = dict.TryGetValue(sym, out n); - assert b && n > 0; + Contract.Assert(b && n > 0); if (n == 1) dict.Remove(sym); else dict[sym] = n - 1; } - public override Result Visit(VCExprQuantifier! node, Arg arg) { + public override Result Visit(VCExprQuantifier node, Arg arg){ +Contract.Requires(node != null); // we temporarily add bound (term and type) variables to the // corresponding lists - foreach (VCExprVar! v in node.BoundVars) - AddBoundVar(BoundTermVarsDict, v); - foreach (TypeVariable! v in node.TypeParameters) - AddBoundVar(BoundTypeVarsDict, v); + foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null); + AddBoundVar(BoundTermVarsDict, v);} + foreach (TypeVariable/*!*/ v in node.TypeParameters){Contract.Assert(v != null); + AddBoundVar(BoundTypeVarsDict, v);} Result res; try { res = VisitAfterBinding(node, arg); } finally { - foreach (VCExprVar! v in node.BoundVars) - RemoveBoundVar(BoundTermVarsDict, v); - foreach (TypeVariable! v in node.TypeParameters) - RemoveBoundVar(BoundTypeVarsDict, v); + foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null); + RemoveBoundVar(BoundTermVarsDict, v);} + foreach (TypeVariable/*!*/ v in node.TypeParameters) { + Contract.Assert(v != null); + RemoveBoundVar(BoundTypeVarsDict, v);} } return res; } - public override Result Visit(VCExprLet! node, Arg arg) { + public override Result Visit(VCExprLet node, Arg arg){ +Contract.Requires(node != null); // we temporarily add bound term variables to the // corresponding lists - foreach (VCExprVar! v in node.BoundVars) - AddBoundVar(BoundTermVarsDict, v); + foreach (VCExprVar/*!*/ v in node.BoundVars){Contract.Assert(v != null); + AddBoundVar(BoundTermVarsDict, v);} Result res; try { res = VisitAfterBinding(node, arg); } finally { - foreach (VCExprVar! v in node.BoundVars) + foreach (VCExprVar/*!*/ v in node.BoundVars) { + Contract.Assert(v != null); RemoveBoundVar(BoundTermVarsDict, v); + } } return res; } @@ -271,11 +497,13 @@ namespace Microsoft.Boogie.VCExprAST // (when overriding the normal visit-methods, the node will be visited // before the binding happens) - protected virtual Result VisitAfterBinding(VCExprQuantifier! node, Arg arg) { + protected virtual Result VisitAfterBinding(VCExprQuantifier node, Arg arg) { + Contract.Requires(node != null); return base.Visit(node, arg); } - protected virtual Result VisitAfterBinding(VCExprLet! node, Arg arg) { + protected virtual Result VisitAfterBinding(VCExprLet node, Arg arg) { + Contract.Requires(node != null); return base.Visit(node, arg); } } @@ -285,174 +513,231 @@ namespace Microsoft.Boogie.VCExprAST // As the visitor is not used anywhere for the time being, it maybe should // be removed + [ContractClass(typeof(CollectingVCExprVisitorContracts<,>))] public abstract class CollectingVCExprVisitor : IVCExprVisitor { - protected abstract Result CombineResults(List! results, Arg arg); + protected abstract Result CombineResults(List/*!*/ results, Arg arg); - public Result Collect(VCExpr! node, Arg arg) { + public Result Collect(VCExpr node, Arg arg) { + Contract.Requires(node != null); return node.Accept(this, arg); } - public virtual Result Visit(VCExprLiteral! node, Arg arg) { - return CombineResults(new List (), arg); + public virtual Result Visit(VCExprLiteral node, Arg arg) { + Contract.Requires(node != null); + return CombineResults(new List(), arg); } - public virtual Result Visit(VCExprNAry! node, Arg arg) { - List! results = new List (); - foreach (VCExpr! subnode in node) - results.Add(subnode.Accept(this, arg)); + public virtual Result Visit(VCExprNAry node, Arg arg){ +Contract.Requires(node != null); + List/*!*/ results = new List (); + foreach (VCExpr/*!*/ subnode in node) { + Contract.Assert(subnode != null); + results.Add(subnode.Accept(this, arg));} return CombineResults(results, arg); } - public virtual Result Visit(VCExprVar! node, Arg arg) { - return CombineResults(new List (), arg); + public virtual Result Visit(VCExprVar node, Arg arg) { + Contract.Requires(node != null); + return CombineResults(new List(), arg); } - public virtual Result Visit(VCExprQuantifier! node, Arg arg) { - List! result = new List (); + public virtual Result Visit(VCExprQuantifier node, Arg arg){ +Contract.Requires(node != null); + List/*!*/ result = new List (); result.Add(node.Body.Accept(this, arg)); - foreach (VCTrigger! trigger in node.Triggers) - foreach (VCExpr! expr in trigger.Exprs) - result.Add(expr.Accept(this, arg)); + foreach (VCTrigger/*!*/ trigger in node.Triggers){Contract.Assert(trigger != null); + foreach (VCExpr/*!*/ expr in trigger.Exprs) { + Contract.Assert(expr != null); + result.Add(expr.Accept(this, arg));}} return CombineResults(result, arg); } - public virtual Result Visit(VCExprLet! node, Arg arg) { - List! results = new List (); + public virtual Result Visit(VCExprLet node, Arg arg){ +Contract.Requires(node != null); + List/*!*/ results = new List (); // visit the bound expressions first - foreach (VCExprLetBinding! binding in node) + foreach (VCExprLetBinding/*!*/ binding in node) { + Contract.Assert(binding != null); results.Add(binding.E.Accept(this, arg)); + } results.Add(node.Body.Accept(this, arg)); return CombineResults(results, arg); } } - + [ContractClassFor(typeof(CollectingVCExprVisitor<,>))] + public abstract class CollectingVCExprVisitorContracts : CollectingVCExprVisitor { + protected override Result CombineResults(List results, Arg arg) { + Contract.Requires(results != null); + throw new NotImplementedException(); + } + } //////////////////////////////////////////////////////////////////////////// - public class SizeComputingVisitor : TraversingVCExprVisitor { + public class SizeComputingVisitor : TraversingVCExprVisitor { - private int Size = 0; + private int Size = 0; - public static int ComputeSize(VCExpr! expr) { - SizeComputingVisitor! visitor = new SizeComputingVisitor(); - visitor.Traverse(expr, true); - return visitor.Size; - } - - protected override bool StandardResult(VCExpr! node, bool arg) { - Size = Size + 1; - return true; + public static int ComputeSize(VCExpr expr) { + Contract.Requires(expr != null); + SizeComputingVisitor/*!*/ visitor = new SizeComputingVisitor(); + visitor.Traverse(expr, true); + return visitor.Size; + } + + protected override bool StandardResult(VCExpr node, bool arg) { + Contract.Requires(node != null); + Size = Size + 1; + return true; + } } - } - //////////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////// - // Collect all free term and type variables in a VCExpr. Type variables - // can occur free either in the types of bound variables, or in the type - // parameters of VCExprNAry. + // Collect all free term and type variables in a VCExpr. Type variables + // can occur free either in the types of bound variables, or in the type + // parameters of VCExprNAry. + + // the result and argument (of type bool) are not used currently + public class FreeVariableCollector : BoundVarTraversingVCExprVisitor { + public readonly Dictionary/*!*/ FreeTermVars = new Dictionary(); + public readonly List/*!*/ FreeTypeVars = new List(); + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(FreeTermVars)); + Contract.Invariant(cce.NonNullElements(FreeTypeVars)); + } - // the result and argument (of type bool) are not used currently - public class FreeVariableCollector : BoundVarTraversingVCExprVisitor { - public readonly Dictionary! FreeTermVars = new Dictionary (); - public readonly List! FreeTypeVars = new List (); - // not used - protected override bool StandardResult(VCExpr! node, bool arg) { - return true; - } + // not used + protected override bool StandardResult(VCExpr node, bool arg) { + Contract.Requires(node != null); + return true; + } - public static Dictionary! FreeTermVariables(VCExpr! node) { - FreeVariableCollector collector = new FreeVariableCollector (); - collector.Traverse(node, true); - return collector.FreeTermVars; - } + public static Dictionary/*!*/ FreeTermVariables(VCExpr node) { + Contract.Requires(node != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + FreeVariableCollector collector = new FreeVariableCollector(); + collector.Traverse(node, true); + return collector.FreeTermVars; + } - public static List! FreeTypeVariables(VCExpr! node) { - FreeVariableCollector collector = new FreeVariableCollector (); - collector.Traverse(node, true); - return collector.FreeTypeVars; - } + public static List/*!*/ FreeTypeVariables(VCExpr node) { + Contract.Requires(node != null); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + FreeVariableCollector collector = new FreeVariableCollector(); + collector.Traverse(node, true); + return collector.FreeTypeVars; + } - public void Reset() { - FreeTermVars.Clear(); - FreeTypeVars.Clear(); - } + public void Reset() { + FreeTermVars.Clear(); + FreeTypeVars.Clear(); + } - public void Collect(VCExpr! node) { - Traverse(node, true); - } + public void Collect(VCExpr node) { + Contract.Requires(node != null); + Traverse(node, true); + } - public void Collect(Type! type) { - AddTypeVariables(type.FreeVariables.ToList()); - } + public void Collect(Type type) { + Contract.Requires(type != null); + AddTypeVariables(type.FreeVariables.ToList()); + } - ///////////////////////////////////////////////////////////////////////// + ///////////////////////////////////////////////////////////////////////// - private void CollectTypeVariables(IEnumerable! boundVars) { - foreach (VCExprVar! var in boundVars) + private void CollectTypeVariables(IEnumerable/*!*/ boundVars){Contract.Requires(cce.NonNullElements(boundVars)); + foreach (VCExprVar/*!*/ var in boundVars) { + Contract.Assert(var != null); Collect(var.Type); + } } - private void AddTypeVariables(IEnumerable! typeVars) { - foreach (TypeVariable! tvar in typeVars) - if (!BoundTypeVars.Contains(tvar) && !FreeTypeVars.Contains(tvar)) - FreeTypeVars.Add(tvar); - } + private void AddTypeVariables(IEnumerable/*!*/ typeVars) { + Contract.Requires(cce.NonNullElements(typeVars)); + foreach (TypeVariable/*!*/ tvar in typeVars) { + Contract.Assert(tvar != null); + if (!BoundTypeVars.Contains(tvar) && !FreeTypeVars.Contains(tvar)) + FreeTypeVars.Add(tvar); + } + } - public override bool Visit(VCExprVar! node, bool arg) { - if (!BoundTermVars.Contains(node) && !FreeTermVars.ContainsKey(node)) { - FreeTermVars.Add(node, null); - Collect(node.Type); + public override bool Visit(VCExprVar node, bool arg) { + Contract.Requires(node != null); + if (!BoundTermVars.Contains(node) && !FreeTermVars.ContainsKey(node)) { + FreeTermVars.Add(node, null); + Collect(node.Type); + } + return true; } - return true; - } - public override bool Visit(VCExprNAry! node, bool arg) { - foreach (Type! t in node.TypeArguments) - Collect(t); - return base.Visit(node, arg); - } + public override bool Visit(VCExprNAry node, bool arg) { + Contract.Requires(node != null); + foreach (Type/*!*/ t in node.TypeArguments) { + Contract.Assert(t != null); + Collect(t); + } + return base.Visit(node, arg); + } - protected override bool VisitAfterBinding(VCExprQuantifier! node, bool arg) { - CollectTypeVariables(node.BoundVars); - return base.VisitAfterBinding(node, arg); - } + protected override bool VisitAfterBinding(VCExprQuantifier node, bool arg) { + Contract.Requires(node != null); + CollectTypeVariables(node.BoundVars); + return base.VisitAfterBinding(node, arg); + } - protected override bool VisitAfterBinding(VCExprLet! node, bool arg) { - CollectTypeVariables(node.BoundVars); - return base.VisitAfterBinding(node, arg); + protected override bool VisitAfterBinding(VCExprLet node, bool arg) { + Contract.Requires(node != null); + CollectTypeVariables(node.BoundVars); + return base.VisitAfterBinding(node, arg); + } } - } - - //////////////////////////////////////////////////////////////////////////// - // Framework for mutating VCExprs - // The Visit implementations in the following visitor work - // recursively, apart from the implementation for VCExprNAry that - // uses its own stack when applied to nested nodes with the same - // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary - // to avoid stack overflows (like in TraversingVCExprVisitor) + //////////////////////////////////////////////////////////////////////////// + // Framework for mutating VCExprs + + // The Visit implementations in the following visitor work + // recursively, apart from the implementation for VCExprNAry that + // uses its own stack when applied to nested nodes with the same + // operator, e.g., (AND (AND (AND ...) ...) ...). This is necessary + // to avoid stack overflows (like in TraversingVCExprVisitor) + + public abstract class MutatingVCExprVisitor + : IVCExprVisitor { + protected readonly VCExpressionGenerator/*!*/ Gen; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Gen != null); + } - public abstract class MutatingVCExprVisitor - : IVCExprVisitor { - protected readonly VCExpressionGenerator! Gen; - public MutatingVCExprVisitor(VCExpressionGenerator! gen) { - this.Gen = gen; - } + public MutatingVCExprVisitor(VCExpressionGenerator gen) { + Contract.Requires(gen != null); + this.Gen = gen; + } - public VCExpr! Mutate(VCExpr! expr, Arg arg) { - return expr.Accept(this, arg); - } + public VCExpr Mutate(VCExpr expr, Arg arg) { + Contract.Requires(expr != null); + Contract.Ensures(Contract.Result() != null); + return expr.Accept(this, arg); + } - public List! MutateSeq(IEnumerable! exprs, Arg arg) { - List! res = new List (); - foreach (VCExpr! expr in exprs) + public List/*!*/ MutateSeq(IEnumerable/*!*/ exprs, Arg arg){ +Contract.Requires(cce.NonNullElements(exprs)); +Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List/*!*/ res = new List (); + foreach (VCExpr/*!*/ expr in exprs) { + Contract.Assert(expr != null); res.Add(expr.Accept(this, arg)); + } return res; } - private List! MutateList(List! exprs, Arg arg) { + private List/*!*/ MutateList(List/*!*/ exprs, Arg arg){ +Contract.Requires(cce.NonNullElements(exprs)); +Contract.Ensures(cce.NonNullElements(Contract.Result>())); bool changed = false; - List! res = new List (); - foreach (VCExpr! expr in exprs) { - VCExpr! newExpr = expr.Accept(this, arg); + List/*!*/ res = new List (); + foreach (VCExpr/*!*/ expr in exprs) {Contract.Assert(expr != null); + VCExpr/*!*/ newExpr = expr.Accept(this, arg); if (!Object.ReferenceEquals(expr, newExpr)) changed = true; res.Add(newExpr); @@ -462,54 +747,69 @@ namespace Microsoft.Boogie.VCExprAST return res; } - public virtual VCExpr! Visit(VCExprLiteral! node, Arg arg) { - return node; - } - - //////////////////////////////////////////////////////////////////////////// - - // Special element used to mark the positions in the todo-stack where - // results have to be popped from the result-stack. - private static readonly VCExpr! CombineResultsMarker = new VCExprLiteral (Type.Bool); + public virtual VCExpr Visit(VCExprLiteral node, Arg arg) { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + return node; + } - // The todo-stack contains records of the shape - // - // arg0 - // arg1 - // arg2 - // ... - // CombineResultsMarker - // f(arg0, arg1, arg2, ...) (the original expression) + //////////////////////////////////////////////////////////////////////////// + + // Special element used to mark the positions in the todo-stack where + // results have to be popped from the result-stack. + private static readonly VCExpr/*!*/ CombineResultsMarker = new VCExprLiteral(Type.Bool); + + // The todo-stack contains records of the shape + // + // arg0 + // arg1 + // arg2 + // ... + // CombineResultsMarker + // f(arg0, arg1, arg2, ...) (the original expression) + + private readonly Stack/*!*/ NAryExprTodoStack = new Stack(); + private readonly Stack/*!*/ NAryExprResultStack = new Stack(); + [ContractInvariantMethod] + void ObjectInvarianta() { + Contract.Invariant(cce.NonNullElements(NAryExprResultStack)); + Contract.Invariant(cce.NonNullElements(NAryExprTodoStack)); + } - private readonly Stack! NAryExprTodoStack = new Stack (); - private readonly Stack! NAryExprResultStack = new Stack (); - private void PushTodo(VCExprNAry! exprTodo) { - NAryExprTodoStack.Push(exprTodo); - NAryExprTodoStack.Push(CombineResultsMarker); - for (int i = exprTodo.Arity - 1; i >= 0; --i) - NAryExprTodoStack.Push(exprTodo[i]); - } + private void PushTodo(VCExprNAry exprTodo) { + Contract.Requires(exprTodo != null); + NAryExprTodoStack.Push(exprTodo); + NAryExprTodoStack.Push(CombineResultsMarker); + for (int i = exprTodo.Arity - 1; i >= 0; --i) + NAryExprTodoStack.Push(exprTodo[i]); + } - public virtual VCExpr! Visit(VCExprNAry! node, Arg arg) { - VCExprOp! op = node.Op; + public virtual VCExpr Visit(VCExprNAry node, Arg arg){ +Contract.Requires(node != null); +Contract.Ensures(Contract.Result() != null); + VCExprOp/*!*/ op = node.Op; + Contract.Assert(op != null); int initialStackSize = NAryExprTodoStack.Count; int initialResultStackSize = NAryExprResultStack.Count; PushTodo(node); while (NAryExprTodoStack.Count > initialStackSize) { - VCExpr! subExpr = NAryExprTodoStack.Pop(); + VCExpr/*!*/ subExpr = NAryExprTodoStack.Pop(); + Contract.Assert(subExpr != null); if (Object.ReferenceEquals(subExpr, CombineResultsMarker)) { // // assemble a result - VCExprNAry! originalExpr = (VCExprNAry)NAryExprTodoStack.Pop(); + VCExprNAry/*!*/ originalExpr = (VCExprNAry)NAryExprTodoStack.Pop(); + Contract.Assert(originalExpr != null); bool changed = false; - List! newSubExprs = new List (); + List/*!*/ newSubExprs = new List (); for (int i = op.Arity - 1; i >= 0; --i) { - VCExpr! nextSubExpr = NAryExprResultStack.Pop(); + VCExpr/*!*/ nextSubExpr = NAryExprResultStack.Pop(); + Contract.Assert(nextSubExpr != null); if (!Object.ReferenceEquals(nextSubExpr, originalExpr[i])) changed = true; newSubExprs.Insert(0, nextSubExpr); @@ -532,35 +832,41 @@ namespace Microsoft.Boogie.VCExprAST } } - assert NAryExprTodoStack.Count == initialStackSize && - NAryExprResultStack.Count == initialResultStackSize + 1; + Contract.Assert(NAryExprTodoStack.Count == initialStackSize && NAryExprResultStack.Count == initialResultStackSize + 1); return NAryExprResultStack.Pop(); } - protected virtual VCExpr! UpdateModifiedNode(VCExprNAry! originalNode, - List! newSubExprs, - // has any of the subexpressions changed? - bool changed, - Arg arg) { - if (changed) - return Gen.Function(originalNode.Op, - newSubExprs, originalNode.TypeArguments); - else - return originalNode; - } + protected virtual VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List/*!*/ newSubExprs, // has any of the subexpressions changed? + bool changed, + Arg arg) { + Contract.Requires(cce.NonNullElements(newSubExprs)); + Contract.Ensures(Contract.Result() != null); - //////////////////////////////////////////////////////////////////////////// + if (changed) + return Gen.Function(originalNode.Op, + newSubExprs, originalNode.TypeArguments); + else + return originalNode; + } - public virtual VCExpr! Visit(VCExprVar! node, Arg arg) { - return node; - } + //////////////////////////////////////////////////////////////////////////// + + public virtual VCExpr Visit(VCExprVar node, Arg arg) { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + return node; + } - protected List! MutateTriggers(List! triggers, Arg arg) { - List! newTriggers = new List (); + protected List/*!*/ MutateTriggers(List/*!*/ triggers, Arg arg){ +Contract.Requires(cce.NonNullElements(triggers)); +Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List/*!*/ newTriggers = new List (); bool changed = false; - foreach (VCTrigger! trigger in triggers) { - List! exprs = trigger.Exprs; - List! newExprs = MutateList(exprs, arg); + foreach (VCTrigger/*!*/ trigger in triggers) { + Contract.Assert(trigger != null); + List/*!*/ exprs = trigger.Exprs; + List/*!*/ newExprs = MutateList(exprs, arg); + if (Object.ReferenceEquals(exprs, newExprs)) { newTriggers.Add(trigger); } else { @@ -573,17 +879,23 @@ namespace Microsoft.Boogie.VCExprAST return newTriggers; } - public virtual VCExpr! Visit(VCExprQuantifier! node, Arg arg) { + public virtual VCExpr Visit(VCExprQuantifier node, Arg arg){ +Contract.Requires(node != null); +Contract.Ensures(Contract.Result() != null); bool changed = false; - VCExpr! body = node.Body; - VCExpr! newbody = body.Accept(this, arg); + VCExpr/*!*/ body = node.Body; + Contract.Assert(body != null); + VCExpr/*!*/ newbody = body.Accept(this, arg); + Contract.Assert(newbody != null); if (!Object.ReferenceEquals(body, newbody)) changed = true; // visit the trigger expressions as well - List! triggers = node.Triggers; - List! newTriggers = MutateTriggers(triggers, arg); + List/*!*/ triggers = node.Triggers; + Contract.Assert(cce.NonNullElements(triggers)); + List/*!*/ newTriggers = MutateTriggers(triggers, arg); + Contract.Assert(cce.NonNullElements(newTriggers)); if (!Object.ReferenceEquals(triggers, newTriggers)) changed = true; @@ -593,19 +905,22 @@ namespace Microsoft.Boogie.VCExprAST newTriggers, node.Infos, newbody); } - public virtual VCExpr! Visit(VCExprLet! node, Arg arg) { + public virtual VCExpr Visit(VCExprLet node, Arg arg){ +Contract.Requires(node != null); +Contract.Ensures(Contract.Result() != null); bool changed = false; - VCExpr! body = node.Body; - VCExpr! newbody = body.Accept(this, arg); + VCExpr/*!*/ body = node.Body; + VCExpr/*!*/ newbody = body.Accept(this, arg); if (!Object.ReferenceEquals(body, newbody)) changed = true; - List! newbindings = new List (); + List/*!*/ newbindings = new List (); for (int i = 0; i < node.Length; ++i) { - VCExprLetBinding! binding = node[i]; - VCExpr! e = binding.E; - VCExpr! newE = e.Accept(this, arg); + VCExprLetBinding/*!*/ binding = node[i]; + Contract.Assert(binding != null); + VCExpr/*!*/ e = binding.E; + VCExpr/*!*/ newE = e.Accept(this, arg); if (Object.ReferenceEquals(e, newE)) { newbindings.Add(binding); } else { @@ -618,174 +933,220 @@ namespace Microsoft.Boogie.VCExprAST return node; return Gen.Let(newbindings, newbody); } - } - - //////////////////////////////////////////////////////////////////////////// - // Substitutions and a visitor for applying substitutions. A substitution can - // substitute both type variables and term variables + } - public class VCExprSubstitution { - private readonly List!>! TermSubsts; - private readonly List!>! TypeSubsts; + //////////////////////////////////////////////////////////////////////////// + // Substitutions and a visitor for applying substitutions. A substitution can + // substitute both type variables and term variables + + public class VCExprSubstitution { + private readonly List/*!*/>/*!*/ TermSubsts; + [ContractInvariantMethod] + void TermSubstsInvariantMethod() { + Contract.Invariant(TermSubsts != null && Contract.ForAll(TermSubsts, i => cce.NonNullElements(i))); + } + private readonly List/*!*/>/*!*/ TypeSubsts; + [ContractInvariantMethod] + void TypeSubstsInvariantMethod() { + Contract.Invariant(TermSubsts != null && Contract.ForAll(TypeSubsts, i => cce.NonNullElements(i))); + } - public VCExprSubstitution(IDictionary! termSubst, - IDictionary! typeSubst) { - List!>! termSubsts = - new List!> (); + public VCExprSubstitution(IDictionary/*!*/ termSubst, IDictionary/*!*/ typeSubst) { + Contract.Requires(cce.NonNullElements(termSubst)); + Contract.Requires(cce.NonNullElements(typeSubst)); + List/*!*/>/*!*/ termSubsts = + new List/*!*/> (); termSubsts.Add(termSubst); - List!>! typeSubsts = - new List!> (); + List/*!*/>/*!*/ typeSubsts = + new List/*!*/>(); typeSubsts.Add(typeSubst); this.TermSubsts = termSubsts; this.TypeSubsts = typeSubsts; } - public VCExprSubstitution() { - this(new Dictionary (), new Dictionary ()); + public VCExprSubstitution() :this(new Dictionary(), new Dictionary()){ + } - public void PushScope() { - TermSubsts.Add(new Dictionary ()); - TypeSubsts.Add(new Dictionary ()); + public void PushScope() { + TermSubsts.Add(new Dictionary ()); + TypeSubsts.Add(new Dictionary()); } - public void PopScope() { - TermSubsts.RemoveAt(TermSubsts.Count - 1); - TypeSubsts.RemoveAt(TypeSubsts.Count - 1); - } + public void PopScope() { + TermSubsts.RemoveAt(TermSubsts.Count - 1); + TypeSubsts.RemoveAt(TypeSubsts.Count - 1); + } - public VCExpr this[VCExprVar! var] { - get { - VCExpr res; - for (int i = TermSubsts.Count - 1; i >= 0; --i) { - if (TermSubsts[i].TryGetValue(var, out res)) - return res; + public VCExpr this[VCExprVar/*!*/ var] { + get { + Contract.Requires(var != null); + VCExpr res; + for (int i = TermSubsts.Count - 1; i >= 0; --i) { + if (TermSubsts[i].TryGetValue(var, out res)) + return res; + } + return null; + } + set { + TermSubsts[TermSubsts.Count - 1][var] = cce.NonNull(value); } - return null; - } - set { - TermSubsts[TermSubsts.Count - 1][var] = (!)value; } - } - public Type this[TypeVariable! var] { - get { - Type res; - for (int i = TypeSubsts.Count - 1; i >= 0; --i) { - if (TypeSubsts[i].TryGetValue(var, out res)) - return res; + public Type this[TypeVariable/*!*/ var] { + get { + Contract.Requires(var != null); + Type res; + for (int i = TypeSubsts.Count - 1; i >= 0; --i) { + if (TypeSubsts[i].TryGetValue(var, out res)) + return res; + } + return null; + } + set { + TypeSubsts[TypeSubsts.Count - 1][var] = cce.NonNull(value); } - return null; - } - set { - TypeSubsts[TypeSubsts.Count - 1][var] = (!)value; } - } - public bool ContainsKey(VCExprVar! var) { - return this[var] != null; - } + public bool ContainsKey(VCExprVar var) { + Contract.Requires(var != null); + return this[var] != null; + } - public bool ContainsKey(TypeVariable! var) { - return this[var] != null; - } + public bool ContainsKey(TypeVariable var) { + Contract.Requires(var != null); + return this[var] != null; + } - public bool TermSubstIsEmpty { get { - return forall{IDictionary! dict in TermSubsts; - dict.Count == 0}; - } } + public bool TermSubstIsEmpty { + get { + return Contract.ForAll(TermSubsts, dict => dict.Count == 0); + } + } - public bool TypeSubstIsEmpty { get { - return forall{IDictionary! dict in TypeSubsts; - dict.Count == 0}; - } } + public bool TypeSubstIsEmpty { + get { + return Contract.ForAll(TypeSubsts, dict => dict.Count == 0); + } + } - public IDictionary! ToTypeSubst { get { - IDictionary! res = new Dictionary (); - foreach (IDictionary! dict in TypeSubsts) - foreach (KeyValuePair pair in dict) - // later ones overwrite earlier ones - res[pair.Key] = pair.Value; - return res; - } } + public IDictionary/*!*/ ToTypeSubst { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result < IDictionary>())); + IDictionary/*!*/ res = new Dictionary(); + foreach (IDictionary/*!*/ dict in TypeSubsts) { + foreach (KeyValuePair pair in dict) { + Contract.Assert(cce.NonNullElements(pair)); + // later ones overwrite earlier ones + res[pair.Key] = pair.Value; + } + } + return res; + } + } - // the variables that are not mapped to themselves - public IEnumerable! TermDomain { get { - Dictionary! domain = new Dictionary (); - foreach (IDictionary! dict in TermSubsts) - foreach (VCExprVar! var in dict.Keys) + // the variables that are not mapped to themselves + public IEnumerable/*!*/ TermDomain { + get {Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Dictionary/*!*/ domain = new Dictionary (); + foreach (IDictionary/*!*/ dict in TermSubsts) { + Contract.Assert(dict != null); + foreach (VCExprVar/*!*/ var in dict.Keys) { + Contract.Assert(var != null); if (!var.Equals(this[var])) domain.Add(var, true); + } + } return domain.Keys; - } } + } + } - // the variables that are not mapped to themselves - public IEnumerable! TypeDomain { get { - Dictionary! domain = new Dictionary (); - foreach (IDictionary! dict in TypeSubsts) - foreach (TypeVariable! var in dict.Keys) + // the variables that are not mapped to themselves + public IEnumerable/*!*/ TypeDomain { + get {Contract.Ensures(cce.NonNullElements(Contract.Result>())); + Dictionary/*!*/ domain = new Dictionary (); + foreach (IDictionary/*!*/ dict in TypeSubsts) { + Contract.Assert(dict != null); + foreach (TypeVariable/*!*/ var in dict.Keys) { + Contract.Assert(var != null); if (!var.Equals(this[var])) domain.Add(var, true); + } + } return domain.Keys; - } } - - public FreeVariableCollector! Codomains { get { - FreeVariableCollector! coll = new FreeVariableCollector (); - foreach (VCExprVar! var in TermDomain) - coll.Collect((!)this[var]); - foreach (TypeVariable! var in TypeDomain) - coll.Collect((!)this[var]); + } + } + + public FreeVariableCollector/*!*/ Codomains { + get {Contract.Ensures(Contract.Result() != null); + + FreeVariableCollector/*!*/ coll = new FreeVariableCollector (); + foreach (VCExprVar/*!*/ var in TermDomain) + coll.Collect(cce.NonNull(this)[var]); + foreach (TypeVariable/*!*/ var in TypeDomain) + coll.Collect(cce.NonNull(this)[var]); return coll; - } } + } + } - public VCExprSubstitution! Clone() { - VCExprSubstitution! res = new VCExprSubstitution (); - foreach (IDictionary! dict in TermSubsts) + public VCExprSubstitution Clone() { +Contract.Ensures(Contract.Result() != null); + VCExprSubstitution/*!*/ res = new VCExprSubstitution (); + foreach (IDictionary/*!*/ dict in TermSubsts) res.TermSubsts.Add(HelperFuns.Clone(dict)); - foreach (IDictionary! dict in TypeSubsts) + foreach (IDictionary/*!*/ dict in TypeSubsts) res.TypeSubsts.Add(HelperFuns.Clone(dict)); return res; } - } + } - ///////////////////////////////////////////////////////////////////////////////// + ///////////////////////////////////////////////////////////////////////////////// - public class SubstitutingVCExprVisitor - : MutatingVCExprVisitor { - public SubstitutingVCExprVisitor(VCExpressionGenerator! gen) { - base(gen); - } + public class SubstitutingVCExprVisitor + : MutatingVCExprVisitor { + public SubstitutingVCExprVisitor(VCExpressionGenerator gen) :base(gen){ + Contract.Requires(gen != null); + + } - // when descending across a binder, we have to check that no collisions - // or variable capture can occur. if this might happen, we replace the - // term and type variables bound by the binder with fresh variables - private bool CollisionPossible(IEnumerable! typeParams, - IEnumerable! boundVars, - VCExprSubstitution! substitution) { + // when descending across a binder, we have to check that no collisions + // or variable capture can occur. if this might happen, we replace the + // term and type variables bound by the binder with fresh variables + private bool CollisionPossible(IEnumerable/*!*/ typeParams, IEnumerable/*!*/ boundVars, VCExprSubstitution/*!*/ substitution) { + Contract.Requires(cce.NonNullElements(typeParams)); + Contract.Requires(cce.NonNullElements(boundVars)); + Contract.Requires(substitution != null); // variables can be shadowed by a binder - if (exists{TypeVariable! var in typeParams; substitution.ContainsKey(var)} || - exists{VCExprVar! var in boundVars; substitution.ContainsKey(var)}) + if (Contract.Exists(typeParams, var=> substitution.ContainsKey(var)) || + Contract.Exists(boundVars, var=> substitution.ContainsKey(var))) return true; // compute the codomain of the substitution - FreeVariableCollector! coll = substitution.Codomains; + FreeVariableCollector coll = substitution.Codomains; + Contract.Assert(coll != null); // variables could be captured when applying the substitution - return exists{TypeVariable! var in typeParams; coll.FreeTypeVars.Contains(var)} || - exists{VCExprVar! var in boundVars; coll.FreeTermVars.ContainsKey(var)}; + return Contract.Exists(typeParams, var=> coll.FreeTypeVars.Contains(var)) || + Contract.Exists(boundVars, var=> coll.FreeTermVars.ContainsKey(var)); } - // can be overwritten if names of bound variables are to be changed - protected virtual string! ChooseNewVariableName(string! oldName) { - return oldName; - } + // can be overwritten if names of bound variables are to be changed + protected virtual string ChooseNewVariableName(string oldName) { + Contract.Requires(oldName != null); + Contract.Ensures(Contract.Result() != null); + return oldName; + } - // handle type parameters in VCExprNAry - protected override VCExpr! UpdateModifiedNode(VCExprNAry! originalNode, - List! newSubExprs, - bool changed, - VCExprSubstitution! substitution) { - List! typeParams = new List (); - foreach (Type! t in originalNode.TypeArguments) { - Type! newType = t.Substitute(substitution.ToTypeSubst); + // handle type parameters in VCExprNAry + protected override VCExpr/*!*/ UpdateModifiedNode(VCExprNAry/*!*/ originalNode, List/*!*/ newSubExprs, bool changed, VCExprSubstitution/*!*/ substitution) { + Contract.Requires(originalNode != null); + Contract.Requires(cce.NonNullElements(newSubExprs)); + Contract.Requires(substitution != null); + Contract.Ensures(Contract.Result() != null); + + List/*!*/ typeParams = new List (); + foreach (Type/*!*/ t in originalNode.TypeArguments) { + Contract.Assert(t != null); + Type/*!*/ newType = t.Substitute(substitution.ToTypeSubst); + Contract.Assert(newType != null); if (!ReferenceEquals(t, newType)) changed = true; typeParams.Add(newType); @@ -796,211 +1157,272 @@ namespace Microsoft.Boogie.VCExprAST return originalNode; } - public override VCExpr! Visit(VCExprQuantifier! node, - VCExprSubstitution! substitution) { - // the default is to refresh bound variables only if necessary - // because of collisions - return Visit(node, substitution, false); - } - - public VCExpr! Visit(VCExprQuantifier! node, - VCExprSubstitution! substitution, - bool refreshBoundVariables) { - substitution.PushScope(); try { + public override VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution) { + Contract.Requires(node != null); + Contract.Requires(substitution != null); + Contract.Ensures(Contract.Result() != null); - List! typeParams = node.TypeParameters; - bool refreshAllVariables = refreshBoundVariables || - CollisionPossible(node.TypeParameters, node.BoundVars, substitution); - if (refreshAllVariables) { - // we introduce fresh type variables to ensure that none gets captured - typeParams = new List (); - foreach (TypeVariable! var in node.TypeParameters) { - TypeVariable! freshVar = - new TypeVariable (Token.NoToken, ChooseNewVariableName(var.Name)); - typeParams.Add(freshVar); - substitution[var] = freshVar; - // this might overwrite other elements of the substitution, deliberately - } + // the default is to refresh bound variables only if necessary + // because of collisions + return Visit(node, substitution, false); } - List! boundVars = node.BoundVars; - if (refreshAllVariables || !substitution.TypeSubstIsEmpty) { - // collisions are possible, or we also substitute type variables. in this case - // the bound term variables have to be replaced with fresh variables with the - // right types - boundVars = new List (); - IDictionary! typeSubst = substitution.ToTypeSubst; - foreach (VCExprVar! var in node.BoundVars) { - VCExprVar! freshVar = - Gen.Variable(ChooseNewVariableName(var.Name), - var.Type.Substitute(typeSubst)); - boundVars.Add(freshVar); - substitution[var] = freshVar; - // this might overwrite other elements of the substitution, deliberately - } - } + public VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution, bool refreshBoundVariables) { + Contract.Requires(node != null); + Contract.Requires(substitution != null); + Contract.Ensures(Contract.Result() != null); + + substitution.PushScope(); + try { + + List/*!*/ typeParams = node.TypeParameters; + Contract.Assert(cce.NonNullElements(typeParams)); + bool refreshAllVariables = refreshBoundVariables || + CollisionPossible(node.TypeParameters, node.BoundVars, substitution); + if (refreshAllVariables) { + // we introduce fresh type variables to ensure that none gets captured + typeParams = new List(); + foreach (TypeVariable/*!*/ var in node.TypeParameters) { + Contract.Assert(var != null); + TypeVariable/*!*/ freshVar = + new TypeVariable(Token.NoToken, ChooseNewVariableName(var.Name)); + Contract.Assert(freshVar != null); + typeParams.Add(freshVar); + substitution[var] = freshVar; + // this might overwrite other elements of the substitution, deliberately + } + } - List! newTriggers = new List (); - foreach (VCTrigger! trigger in node.Triggers) - newTriggers.Add(Gen.Trigger(trigger.Pos, MutateSeq(trigger.Exprs, substitution))); + List/*!*/ boundVars = node.BoundVars; + Contract.Assert(cce.NonNullElements(boundVars)); + if (refreshAllVariables || !substitution.TypeSubstIsEmpty) { + // collisions are possible, or we also substitute type variables. in this case + // the bound term variables have to be replaced with fresh variables with the + // right types + boundVars = new List(); + IDictionary/*!*/ typeSubst = substitution.ToTypeSubst; + Contract.Assert(cce.NonNullElements(typeSubst)); + foreach (VCExprVar/*!*/ var in node.BoundVars) { + Contract.Assert(var != null); + VCExprVar/*!*/ freshVar = + Gen.Variable(ChooseNewVariableName(var.Name), + var.Type.Substitute(typeSubst)); + Contract.Assert(freshVar != null); + boundVars.Add(freshVar); + substitution[var] = freshVar; + // this might overwrite other elements of the substitution, deliberately + } + } - VCExpr! newBody = Mutate(node.Body, substitution); + List/*!*/ newTriggers = new List(); + foreach (VCTrigger/*!*/ trigger in node.Triggers) { + Contract.Assert(trigger != null); + newTriggers.Add(Gen.Trigger(trigger.Pos, MutateSeq(trigger.Exprs, substitution))); + } - return Gen.Quantify(node.Quan, typeParams, boundVars, - newTriggers, node.Infos, newBody); + VCExpr/*!*/ newBody = Mutate(node.Body, substitution); + Contract.Assert(newBody != null); - } finally { - substitution.PopScope(); + return Gen.Quantify(node.Quan, typeParams, boundVars, + newTriggers, node.Infos, newBody); + + } finally { + substitution.PopScope(); + } } - } - public override VCExpr! Visit(VCExprVar! node, - VCExprSubstitution! substitution) { - VCExpr res = substitution[node]; - if (res != null) - return res; - return node; - } + public override VCExpr Visit(VCExprVar node, VCExprSubstitution substitution) { + Contract.Requires(substitution != null); + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + VCExpr res = substitution[node]; + if (res != null) + return res; + return node; + } - public override VCExpr! Visit(VCExprLet! node, - VCExprSubstitution! substitution) { - // the default is to refresh bound variables only if necessary - // because of collisions - return Visit(node, substitution, false); - } + public override VCExpr Visit(VCExprLet node, VCExprSubstitution substitution) { + Contract.Requires(substitution != null); + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + // the default is to refresh bound variables only if necessary + // because of collisions + return Visit(node, substitution, false); + } - public VCExpr! Visit(VCExprLet! node, - VCExprSubstitution! substitution, - bool refreshBoundVariables) { + public VCExpr Visit(VCExprLet node, VCExprSubstitution substitution, bool refreshBoundVariables){ +Contract.Requires(substitution != null); +Contract.Requires(node != null); +Contract.Ensures(Contract.Result() != null); // let-expressions do not have type parameters (fortunately ...) substitution.PushScope (); try { bool refreshAllVariables = refreshBoundVariables || !substitution.TypeSubstIsEmpty || - CollisionPossible(new List (), node.BoundVars, substitution); + CollisionPossible(new List (), node.BoundVars, substitution); - List! newBoundVars = node.BoundVars; + List/*!*/ newBoundVars = node.BoundVars; + Contract.Assert(cce.NonNullElements(newBoundVars)); if (refreshAllVariables) { // collisions are possible, or we also substitute type variables. in this case // the bound term variables have to be replaced with fresh variables with the // right types - newBoundVars = new List (); - IDictionary! typeSubst = substitution.ToTypeSubst; - foreach (VCExprVar! var in node.BoundVars) { - VCExprVar! freshVar = + newBoundVars = new List (); + IDictionary/*!*/ typeSubst = substitution.ToTypeSubst; + Contract.Assert(cce.NonNullElements(typeSubst)); + foreach (VCExprVar/*!*/ var in node.BoundVars) { + Contract.Assert(var != null); + VCExprVar/*!*/ freshVar = Gen.Variable(ChooseNewVariableName(var.Name), var.Type.Substitute(typeSubst)); + Contract.Assert(freshVar != null); newBoundVars.Add(freshVar); substitution[var] = freshVar; // this might overwrite other elements of the substitution, deliberately } } - List! newbindings = new List (); + List/*!*/ newbindings = new List (); for (int i = 0; i < node.Length; ++i) { - VCExprLetBinding! binding = node[i]; + VCExprLetBinding/*!*/ binding = node[i]; + Contract.Assert(binding != null); newbindings.Add(Gen.LetBinding(newBoundVars[i], Mutate(binding.E, substitution))); } - - VCExpr! newBody = Mutate(node.Body, substitution); + + VCExpr/*!*/ newBody = Mutate(node.Body, substitution); + Contract.Assert(newBody != null); return Gen.Let(newbindings, newBody); } finally { substitution.PopScope(); } } - } + } - //////////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////// + [ContractClassFor(typeof(StandardVCExprOpVisitor<,>))] + public abstract class StandardVCExprOpVisitorContracts : StandardVCExprOpVisitor { + protected override Result StandardResult(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); + } + } - public abstract class StandardVCExprOpVisitor - : IVCExprOpVisitor { - protected abstract Result StandardResult(VCExprNAry! node, Arg arg); - public virtual Result VisitNotOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitEqOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitNeqOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitAndOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitOrOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitImpliesOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitDistinctOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitLabelOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitSelectOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitStoreOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitBvOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitBvExtractOp(VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitBvConcatOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitIfThenElseOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitCustomOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitAddOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitSubOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitMulOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitDivOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitModOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitLtOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitLeOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitGtOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitGeOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitSubtypeOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); - } - public virtual Result VisitSubtype3Op (VCExprNAry! node, Arg arg) { + [ContractClass(typeof(StandardVCExprOpVisitorContracts<,>))] + public abstract class StandardVCExprOpVisitor + : IVCExprOpVisitor { + protected abstract Result StandardResult(VCExprNAry/*!*/ node, Arg arg); + + public virtual Result VisitNotOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitEqOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitNeqOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitAndOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitOrOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitImpliesOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitDistinctOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitLabelOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitSelectOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitStoreOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitBvOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitBvExtractOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitBvConcatOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitIfThenElseOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitCustomOp (VCExprNAry node, Arg arg) { + Contract.Requires(node != null); return StandardResult(node, arg); } - public virtual Result VisitBoogieFunctionOp (VCExprNAry! node, Arg arg) { - return StandardResult(node, arg); + public virtual Result VisitAddOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitSubOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitMulOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitDivOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitModOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitLtOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitLeOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitGtOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitGeOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitSubtypeOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitSubtype3Op(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } + public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + return StandardResult(node, arg); + } } - } - -} - + } \ No newline at end of file -- cgit v1.2.3