From f09bf83d24438d712021ada6fab252b0f7f11986 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Fri, 27 Aug 2010 21:52:03 +0000 Subject: Boogie: Commented out all occurences of repeated inherited contracts - makes fewer error messages when compiling with runtime checking on. --- Source/VCExpr/VCExprASTVisitors.cs | 1282 ++++++++++++++++++------------------ 1 file changed, 654 insertions(+), 628 deletions(-) (limited to 'Source/VCExpr/VCExprASTVisitors.cs') diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index e87b04ce..3e65ec23 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -17,7 +17,7 @@ namespace Microsoft.Boogie.VCExprAST { using Microsoft.Boogie; [ContractClass(typeof(IVCExprVisitorContracts<,>))] - public interface IVCExprVisitor { + public interface IVCExprVisitor { Result Visit(VCExprLiteral/*!*/ node, Arg arg); Result Visit(VCExprNAry/*!*/ node, Arg arg); Result Visit(VCExprVar/*!*/ node, Arg arg); @@ -25,7 +25,7 @@ namespace Microsoft.Boogie.VCExprAST { Result Visit(VCExprLet/*!*/ node, Arg arg); } [ContractClassFor(typeof(IVCExprVisitor<,>))] - public abstract class IVCExprVisitorContracts : IVCExprVisitor { + public abstract class IVCExprVisitorContracts : IVCExprVisitor { #region IVCExprVisitor Members public Result Visit(VCExprLiteral node, Arg arg) { @@ -83,10 +83,10 @@ namespace Microsoft.Boogie.VCExprAST { 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 VisitCustomOp(VCExprNAry node, Arg arg); } [ContractClassFor(typeof(IVCExprOpVisitor<,>))] - public abstract class IVCExprOpVisitorContracts:IVCExprOpVisitor { + public abstract class IVCExprOpVisitorContracts : IVCExprOpVisitor { #region IVCExprOpVisitor Members public Result VisitNotOp(VCExprNAry node, Arg arg) { @@ -248,23 +248,22 @@ namespace Microsoft.Boogie.VCExprAST { } public virtual Result Visit(VCExprLiteral node, Arg arg) { - Contract.Requires(node != null); + //Contract.Requires(node != null); return StandardResult(node, arg); } - public virtual Result Visit(VCExprNAry node, Arg arg){ -Contract.Requires(node != null); + public virtual Result Visit(VCExprNAry node, Arg arg) { + //Contract.Requires(node != null); Result res = StandardResult(node, arg); if (node.TypeParamArity == 0 && (node.Op == VCExpressionGenerator.AndOp || - node.Op == VCExpressionGenerator.OrOp || - node.Op == VCExpressionGenerator.ImpliesOp)) - { + node.Op == VCExpressionGenerator.OrOp || + node.Op == VCExpressionGenerator.ImpliesOp)) { Contract.Assert(node.Op != null); VCExprOp op = node.Op; - + IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node); enumerator.MoveNext(); // skip the node itself @@ -278,34 +277,40 @@ Contract.Requires(node != null); } } } else { - foreach (VCExpr e in node){Contract.Assert(e != null); - 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) { - Contract.Requires(node != null); + //Contract.Requires(node != null); return StandardResult(node, arg); } - public virtual Result Visit(VCExprQuantifier node, Arg arg){ -Contract.Requires(node != null); + public virtual Result Visit(VCExprQuantifier node, Arg arg) { + //Contract.Requires(node != null); Result res = StandardResult(node, 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);}} + 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){ -Contract.Requires(node != null); + 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) { Contract.Assert(binding != null); - binding.E.Accept(this, arg);} + binding.E.Accept(this, arg); + } node.Body.Accept(this, arg); return res; } @@ -333,8 +338,8 @@ Contract.Requires(node != null); Contract.Invariant(cce.NonNullElements(ExprTodo)); } - public VCExprNAryEnumerator(VCExprNAry completeExpr){ -Contract.Requires(completeExpr != null); + public VCExprNAryEnumerator(VCExprNAry completeExpr) { + Contract.Requires(completeExpr != null); this.CompleteExpr = completeExpr; Stack/*!*/ exprTodo = new Stack(); exprTodo.Push(completeExpr); @@ -395,7 +400,7 @@ Contract.Requires(completeExpr != null); this.Op = completeExpr.Op; } protected override bool Descend(VCExprNAry expr) { - Contract.Requires(expr != null); + //Contract.Requires(expr != null); return expr.Op.Equals(Op) && // we never skip nodes with type parameters // (those are too interesting ...) @@ -456,33 +461,42 @@ Contract.Requires(completeExpr != null); dict[sym] = n - 1; } - public override Result Visit(VCExprQuantifier node, Arg arg){ -Contract.Requires(node != null); + 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){Contract.Assert(v != null); - AddBoundVar(BoundTermVarsDict, v);} - foreach (TypeVariable/*!*/ v in node.TypeParameters){Contract.Assert(v != null); - 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){Contract.Assert(v != null); - RemoveBoundVar(BoundTermVarsDict, 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);} + RemoveBoundVar(BoundTypeVarsDict, v); + } } return res; } - public override Result Visit(VCExprLet node, Arg arg){ -Contract.Requires(node != null); + 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){Contract.Assert(v != null); - AddBoundVar(BoundTermVarsDict, v);} + foreach (VCExprVar/*!*/ v in node.BoundVars) { + Contract.Assert(v != null); + AddBoundVar(BoundTermVarsDict, v); + } Result res; try { @@ -529,34 +543,38 @@ Contract.Requires(node != null); } public virtual Result Visit(VCExprLiteral node, Arg arg) { - Contract.Requires(node != null); + //Contract.Requires(node != null); return CombineResults(new List(), arg); } - public virtual Result Visit(VCExprNAry node, Arg arg){ -Contract.Requires(node != null); - List/*!*/ results = new List (); + 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));} + results.Add(subnode.Accept(this, arg)); + } return CombineResults(results, arg); } public virtual Result Visit(VCExprVar node, Arg arg) { - Contract.Requires(node != null); + //Contract.Requires(node != null); return CombineResults(new List(), arg); } - public virtual Result Visit(VCExprQuantifier node, Arg arg){ -Contract.Requires(node != null); - 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){Contract.Assert(trigger != null); - foreach (VCExpr/*!*/ expr in trigger.Exprs) { - Contract.Assert(expr != null); - 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){ -Contract.Requires(node != null); - 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) { Contract.Assert(binding != null); @@ -575,160 +593,161 @@ Contract.Requires(node != null); } //////////////////////////////////////////////////////////////////////////// - public class SizeComputingVisitor : TraversingVCExprVisitor { + public class SizeComputingVisitor : TraversingVCExprVisitor { - private int Size = 0; + private int Size = 0; - public static int ComputeSize(VCExpr expr) { - Contract.Requires(expr != null); - SizeComputingVisitor/*!*/ visitor = new SizeComputingVisitor(); - visitor.Traverse(expr, true); - return visitor.Size; - } + 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; - } + 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. - - // 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)); - } + // 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)); + } - // not used - protected override bool StandardResult(VCExpr node, bool arg) { - Contract.Requires(node != null); - return true; - } + // not used + protected override bool StandardResult(VCExpr node, bool arg) { + //Contract.Requires(node != null); + return true; + } - 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 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) { - Contract.Requires(node != null); - Contract.Ensures(cce.NonNullElements(Contract.Result>())); - 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) { - Contract.Requires(node != null); - Traverse(node, true); - } + public void Collect(VCExpr node) { + Contract.Requires(node != null); + Traverse(node, true); + } - public void Collect(Type type) { - Contract.Requires(type != null); - AddTypeVariables(type.FreeVariables.ToList()); - } + public void Collect(Type type) { + Contract.Requires(type != null); + AddTypeVariables(type.FreeVariables.ToList()); + } - ///////////////////////////////////////////////////////////////////////// + ///////////////////////////////////////////////////////////////////////// - private void CollectTypeVariables(IEnumerable/*!*/ boundVars){Contract.Requires(cce.NonNullElements(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) { - Contract.Requires(cce.NonNullElements(typeVars)); - foreach (TypeVariable/*!*/ tvar in typeVars) { - Contract.Assert(tvar != null); - 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) { - Contract.Requires(node != null); - if (!BoundTermVars.Contains(node) && !FreeTermVars.ContainsKey(node)) { - FreeTermVars.Add(node, null); - Collect(node.Type); - } - return true; + 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; + } - 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); + 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) { - Contract.Requires(node != null); - 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) { - Contract.Requires(node != null); - 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) - - public abstract class MutatingVCExprVisitor - : IVCExprVisitor { - protected readonly VCExpressionGenerator/*!*/ Gen; - [ContractInvariantMethod] - void ObjectInvariant() { - Contract.Invariant(Gen != null); - } + //////////////////////////////////////////////////////////////////////////// + // 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 MutatingVCExprVisitor(VCExpressionGenerator gen) { - Contract.Requires(gen != null); - this.Gen = gen; - } + public abstract class MutatingVCExprVisitor + : IVCExprVisitor { + protected readonly VCExpressionGenerator/*!*/ Gen; + [ContractInvariantMethod] + void ObjectInvariant() { + Contract.Invariant(Gen != null); + } - 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){ -Contract.Requires(cce.NonNullElements(exprs)); -Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List/*!*/ res = new List (); + public MutatingVCExprVisitor(VCExpressionGenerator gen) { + Contract.Requires(gen != null); + this.Gen = gen; + } + + 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) { + 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)); @@ -736,13 +755,14 @@ Contract.Ensures(cce.NonNullElements(Contract.Result>())); return res; } - private List/*!*/ MutateList(List/*!*/ exprs, Arg arg){ -Contract.Requires(cce.NonNullElements(exprs)); -Contract.Ensures(cce.NonNullElements(Contract.Result>())); + 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) {Contract.Assert(expr != null); - 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); @@ -752,65 +772,65 @@ Contract.Ensures(cce.NonNullElements(Contract.Result>())); return res; } - public virtual VCExpr Visit(VCExprLiteral node, Arg arg) { - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - return node; - } + public virtual VCExpr Visit(VCExprLiteral node, Arg arg) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); + 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); - - // 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)); - } + //////////////////////////////////////////////////////////////////////////// + + // 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 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]); - } + 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){ -Contract.Requires(node != null); -Contract.Ensures(Contract.Result() != null); + 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); + Contract.Assert(op != null); int initialStackSize = NAryExprTodoStack.Count; int initialResultStackSize = NAryExprResultStack.Count; PushTodo(node); - + while (NAryExprTodoStack.Count > initialStackSize) { VCExpr/*!*/ subExpr = NAryExprTodoStack.Pop(); Contract.Assert(subExpr != null); - + if (Object.ReferenceEquals(subExpr, CombineResultsMarker)) { // // assemble a result 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(); @@ -819,15 +839,15 @@ Contract.Ensures(Contract.Result() != null); changed = true; newSubExprs.Insert(0, nextSubExpr); } - + NAryExprResultStack.Push(UpdateModifiedNode(originalExpr, newSubExprs, changed, arg)); // } else { // VCExprNAry narySubExpr = subExpr as VCExprNAry; if (narySubExpr != null && narySubExpr.Op.Equals(op) && - // as in VCExprNAryUniformOpEnumerator, all expressions with - // type parameters are allowed to be inspected more closely + // as in VCExprNAryUniformOpEnumerator, all expressions with + // type parameters are allowed to be inspected more closely narySubExpr.TypeParamArity == 0) { PushTodo(narySubExpr); } else { @@ -841,37 +861,37 @@ Contract.Ensures(Contract.Result() != null); return NAryExprResultStack.Pop(); } - 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); + 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; - } + if (changed) + return Gen.Function(originalNode.Op, + newSubExprs, originalNode.TypeArguments); + else + return originalNode; + } - //////////////////////////////////////////////////////////////////////////// + //////////////////////////////////////////////////////////////////////////// - public virtual VCExpr Visit(VCExprVar node, Arg arg) { - Contract.Requires(node != null); - Contract.Ensures(Contract.Result() != null); - 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){ -Contract.Requires(cce.NonNullElements(triggers)); -Contract.Ensures(cce.NonNullElements(Contract.Result>())); - 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) { Contract.Assert(trigger != null); List/*!*/ exprs = trigger.Exprs; List/*!*/ newExprs = MutateList(exprs, arg); - + if (Object.ReferenceEquals(exprs, newExprs)) { newTriggers.Add(trigger); } else { @@ -884,15 +904,15 @@ Contract.Ensures(cce.NonNullElements(Contract.Result>())); return newTriggers; } - public virtual VCExpr Visit(VCExprQuantifier node, Arg arg){ -Contract.Requires(node != null); -Contract.Ensures(Contract.Result() != null); + public virtual VCExpr Visit(VCExprQuantifier node, Arg arg) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); bool changed = false; VCExpr/*!*/ body = node.Body; - Contract.Assert(body != null); + Contract.Assert(body != null); VCExpr/*!*/ newbody = body.Accept(this, arg); - Contract.Assert(newbody != null); + Contract.Assert(newbody != null); if (!Object.ReferenceEquals(body, newbody)) changed = true; @@ -910,9 +930,9 @@ Contract.Ensures(Contract.Result() != null); newTriggers, node.Infos, newbody); } - public virtual VCExpr Visit(VCExprLet node, Arg arg){ -Contract.Requires(node != null); -Contract.Ensures(Contract.Result() != null); + public virtual VCExpr Visit(VCExprLet node, Arg arg) { + //Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); bool changed = false; VCExpr/*!*/ body = node.Body; @@ -920,7 +940,7 @@ Contract.Ensures(Contract.Result() != null); 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]; Contract.Assert(binding != null); @@ -938,29 +958,29 @@ Contract.Ensures(Contract.Result() != null); 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; - [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))); - } + //////////////////////////////////////////////////////////////////////////// + // 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) { + public VCExprSubstitution(IDictionary/*!*/ termSubst, IDictionary/*!*/ typeSubst) { Contract.Requires(cce.NonNullElements(termSubst)); Contract.Requires(cce.NonNullElements(typeSubst)); List/*!*/>/*!*/ termSubsts = - new List/*!*/> (); + new List/*!*/>(); termSubsts.Add(termSubst); List/*!*/>/*!*/ typeSubsts = new List/*!*/>(); @@ -969,185 +989,190 @@ Contract.Ensures(Contract.Result() != null); this.TypeSubsts = typeSubsts; } - public VCExprSubstitution() :this(new Dictionary(), new Dictionary()){ - + public VCExprSubstitution() + : this(new Dictionary(), new Dictionary()) { + } - public void PushScope() { - TermSubsts.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 { - 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); + 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; } - - 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); - } + set { + TermSubsts[TermSubsts.Count - 1][var] = cce.NonNull(value); } + } - public bool ContainsKey(VCExprVar var) { + public Type this[TypeVariable/*!*/ var] { + get { Contract.Requires(var != null); - return this[var] != null; + Type res; + for (int i = TypeSubsts.Count - 1; i >= 0; --i) { + if (TypeSubsts[i].TryGetValue(var, out res)) + return res; + } + return null; } - - public bool ContainsKey(TypeVariable var) { - Contract.Requires(var != null); - return this[var] != null; + set { + TypeSubsts[TypeSubsts.Count - 1][var] = cce.NonNull(value); } + } - public bool TermSubstIsEmpty { - get { - return Contract.ForAll(TermSubsts, dict => dict.Count == 0); - } + public bool ContainsKey(VCExprVar var) { + Contract.Requires(var != null); + return this[var] != null; + } + + public bool ContainsKey(TypeVariable var) { + Contract.Requires(var != null); + return this[var] != null; + } + + public bool TermSubstIsEmpty { + get { + return Contract.ForAll(TermSubsts, dict => dict.Count == 0); } + } - public bool TypeSubstIsEmpty { - get { - return Contract.ForAll(TypeSubsts, dict => dict.Count == 0); - } + public bool TypeSubstIsEmpty { + get { + return Contract.ForAll(TypeSubsts, dict => dict.Count == 0); } + } - 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; - } + public IDictionary/*!*/ ToTypeSubst { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + 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; } + return res; } + } - // 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/*!*/ 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 {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); + // 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; } - return domain.Keys; } - } - public FreeVariableCollector/*!*/ Codomains { - get {Contract.Ensures(Contract.Result() != null); + public FreeVariableCollector/*!*/ Codomains { + get { + Contract.Ensures(Contract.Result() != null); - FreeVariableCollector/*!*/ coll = new FreeVariableCollector (); + 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() { -Contract.Ensures(Contract.Result() != null); - VCExprSubstitution/*!*/ res = new VCExprSubstitution (); + 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) res.TypeSubsts.Add(HelperFuns.Clone(dict)); return res; } - } + } - ///////////////////////////////////////////////////////////////////////////////// + ///////////////////////////////////////////////////////////////////////////////// - public class SubstitutingVCExprVisitor - : MutatingVCExprVisitor { - public SubstitutingVCExprVisitor(VCExpressionGenerator gen) :base(gen){ - Contract.Requires(gen != null); - - } + 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 (Contract.Exists(typeParams, var=> substitution.ContainsKey(var)) || - Contract.Exists(boundVars, var=> 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; Contract.Assert(coll != null); // variables could be captured when applying the substitution - return Contract.Exists(typeParams, var=> coll.FreeTypeVars.Contains(var)) || - Contract.Exists(boundVars, var=> 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) { - Contract.Requires(oldName != null); - Contract.Ensures(Contract.Result() != null); - 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) { - Contract.Requires(originalNode != null); - Contract.Requires(cce.NonNullElements(newSubExprs)); - Contract.Requires(substitution != null); + // 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 (); + List/*!*/ typeParams = new List(); foreach (Type/*!*/ t in originalNode.TypeArguments) { Contract.Assert(t != null); Type/*!*/ newType = t.Substitute(substitution.ToTypeSubst); @@ -1162,272 +1187,273 @@ Contract.Ensures(Contract.Result() != null); return originalNode; } - public override VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution) { - Contract.Requires(node != null); - Contract.Requires(substitution != null); - Contract.Ensures(Contract.Result() != null); + public override VCExpr/*!*/ Visit(VCExprQuantifier/*!*/ node, VCExprSubstitution/*!*/ substitution) { + Contract.Requires(node != null); + Contract.Requires(substitution != null); + Contract.Ensures(Contract.Result() != null); - // the default is to refresh bound variables only if necessary - // because of collisions - return Visit(node, substitution, false); - } + // 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) { - 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 - } - } + 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/*!*/ 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 - } + 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) { - Contract.Assert(trigger != null); - 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); - Contract.Assert(newBody != null); + 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); - 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; + } finally { + substitution.PopScope(); } + } - 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 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) { + 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){ -Contract.Requires(substitution != null); -Contract.Requires(node != null); -Contract.Ensures(Contract.Result() != null); + 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 { + substitution.PushScope(); + try { - bool refreshAllVariables = - refreshBoundVariables || - !substitution.TypeSubstIsEmpty || - CollisionPossible(new List (), node.BoundVars, substitution); + bool refreshAllVariables = + refreshBoundVariables || + !substitution.TypeSubstIsEmpty || + 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; - 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 + 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; + 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 (); - for (int i = 0; i < node.Length; ++i) { - VCExprLetBinding/*!*/ binding = node[i]; - Contract.Assert(binding != null); - newbindings.Add(Gen.LetBinding(newBoundVars[i], Mutate(binding.E, substitution))); - } + List/*!*/ newbindings = new List(); + for (int i = 0; i < node.Length; ++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); - Contract.Assert(newBody != null); - return Gen.Let(newbindings, newBody); + 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(); - } + //////////////////////////////////////////////////////////////////////////// + [ContractClassFor(typeof(StandardVCExprOpVisitor<,>))] + public abstract class StandardVCExprOpVisitorContracts : StandardVCExprOpVisitor { + protected override Result StandardResult(VCExprNAry node, Arg arg) { + Contract.Requires(node != null); + throw new NotImplementedException(); } + } - [ContractClass(typeof(StandardVCExprOpVisitorContracts<,>))] - public abstract class StandardVCExprOpVisitor - : IVCExprOpVisitor { - protected abstract Result StandardResult(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); + public virtual Result VisitNotOp(VCExprNAry node, Arg arg) { + //Contract.Requires(node != null); 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); - } + 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 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 +} \ No newline at end of file -- cgit v1.2.3