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/AIFramework/Lattice.cs | 2 +- .../AIFramework/VariableMap/VariableMapLattice.cs | 12 +- Source/AbsInt/ExprFactories.cs | 75 +- Source/Core/Absy.cs | 8 +- Source/Core/AbsyExpr.cs | 30 +- Source/Core/AbsyQuant.cs | 8 +- Source/Core/AbsyType.cs | 24 +- Source/Core/DeadVarElim.cs | 6 +- Source/Provers/Isabelle/Prover.cs | 2 +- Source/Provers/Simplify/Prover.cs | 2 +- Source/Provers/Simplify/ProverInterface.cs | 2 +- Source/Provers/Z3/Inspector.cs | 2 +- Source/Provers/Z3/Prover.cs | 8 +- Source/Provers/Z3/ProverInterface.cs | 28 +- Source/Provers/Z3/TypeDeclCollector.cs | 2 +- Source/VCExpr/BigLiteralAbstracter.cs | 83 +- Source/VCExpr/Boogie2VCExpr.cs | 197 ++- Source/VCExpr/SimplifyLikeLineariser.cs | 683 ++++++----- Source/VCExpr/VCExprAST.cs | 221 ++-- Source/VCExpr/VCExprASTPrinter.cs | 300 +++-- Source/VCExpr/VCExprASTVisitors.cs | 1282 ++++++++++---------- Source/VCGeneration/Check.cs | 333 ++--- Source/VCGeneration/ConditionGeneration.cs | 4 +- Source/VCGeneration/DoomErrorHandler.cs | 6 +- Source/VCGeneration/VC.cs | 40 +- Source/VCGeneration/VCDoomed.cs | 6 +- 26 files changed, 1728 insertions(+), 1638 deletions(-) diff --git a/Source/AIFramework/Lattice.cs b/Source/AIFramework/Lattice.cs index 78f87421..8d7f6c45 100644 --- a/Source/AIFramework/Lattice.cs +++ b/Source/AIFramework/Lattice.cs @@ -792,7 +792,7 @@ namespace Microsoft.AbstractInterpretationFramework { public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) { //Contract.Requires(args != null); - Contract.Requires(f != null); + //Contract.Requires(f != null); understandsCount++; return lattice.Understands(f, args); } diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.cs b/Source/AIFramework/VariableMap/VariableMapLattice.cs index 169156b0..b3c702d7 100644 --- a/Source/AIFramework/VariableMap/VariableMapLattice.cs +++ b/Source/AIFramework/VariableMap/VariableMapLattice.cs @@ -329,7 +329,7 @@ namespace Microsoft.AbstractInterpretationFramework { } public override string/*!*/ ToString(Element/*!*/ element) { - Contract.Requires(element != null); + //Contract.Requires(element != null); Contract.Ensures(Contract.Result() != null); Elt e = (Elt)element; @@ -416,8 +416,8 @@ namespace Microsoft.AbstractInterpretationFramework { /// Perform the pointwise widening of the elements in the map /// public override Element/*!*/ Widen(Element/*!*/ first, Element/*!*/ second) { - Contract.Requires((second != null)); - Contract.Requires((first != null)); + //Contract.Requires((second != null)); + //Contract.Requires((first != null)); Contract.Ensures(Contract.Result() != null); Elt a = (Elt)first; Elt b = (Elt)second; @@ -568,7 +568,7 @@ namespace Microsoft.AbstractInterpretationFramework { } public override IExpr/*!*/ ToPredicate(Element/*!*/ element) { - Contract.Requires(element != null); + //Contract.Requires(element != null); Contract.Ensures(Contract.Result() != null); if (IsTop(element)) { return propExprFactory.True; @@ -765,8 +765,8 @@ namespace Microsoft.AbstractInterpretationFramework { public override bool Understands(IFunctionSymbol/*!*/ f, IList/*!*/ args) { - Contract.Requires(args != null); - Contract.Requires(f != null); + //Contract.Requires(args != null); + //Contract.Requires(f != null); return f.Equals(Prop.And) || f.Equals(Value.Eq) || microLattice.Understands(f, args); diff --git a/Source/AbsInt/ExprFactories.cs b/Source/AbsInt/ExprFactories.cs index 7979f061..34564cac 100644 --- a/Source/AbsInt/ExprFactories.cs +++ b/Source/AbsInt/ExprFactories.cs @@ -27,42 +27,42 @@ namespace Microsoft.Boogie.AbstractInterpretation { } public AI.IFunApp Not(AI.IExpr p) { - Contract.Requires(p != null); + //Contract.Requires(p != null); Contract.Ensures(Contract.Result() != null); return Expr.Unary(Token.NoToken, UnaryOperator.Opcode.Not, IExpr2Expr(p)); } public AI.IFunApp And(AI.IExpr p, AI.IExpr q) { - Contract.Requires(p != null); - Contract.Requires(q != null); + //Contract.Requires(p != null); + //Contract.Requires(q != null); Contract.Ensures(Contract.Result() != null); return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q)); } public AI.IFunApp Or(AI.IExpr p, AI.IExpr q) { - Contract.Requires(p != null); - Contract.Requires(q != null); + //Contract.Requires(p != null); + //Contract.Requires(q != null); Contract.Ensures(Contract.Result() != null); return Expr.Binary(BinaryOperator.Opcode.Or, IExpr2Expr(p), IExpr2Expr(q)); } public AI.IFunApp Implies(AI.IExpr p, AI.IExpr q) { - Contract.Requires(p != null); - Contract.Requires(q != null); + //Contract.Requires(p != null); + //Contract.Requires(q != null); Contract.Ensures(Contract.Result() != null); return Expr.Binary(BinaryOperator.Opcode.Imp, IExpr2Expr(p), IExpr2Expr(q)); } public AI.IFunApp Exists(AI.IFunction p) { - Contract.Requires(p != null); + //Contract.Requires(p != null); Contract.Ensures(Contract.Result() != null); return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr; } public AI.IFunApp Exists(AI.AIType paramType, AI.FunctionBody bodygen) { - Contract.Requires(bodygen != null); + //Contract.Requires(bodygen != null); Contract.Ensures(Contract.Result() != null); // generate a fresh new variable @@ -74,13 +74,13 @@ namespace Microsoft.Boogie.AbstractInterpretation { } public AI.IFunApp Forall(AI.IFunction p) { - Contract.Requires(p != null); + //Contract.Requires(p != null); Contract.Ensures(Contract.Result() != null); return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr; } public AI.IFunApp Forall(AI.AIType paramType, AI.FunctionBody bodygen) { - Contract.Requires(bodygen != null); + //Contract.Requires(bodygen != null); Contract.Ensures(Contract.Result() != null); // generate a fresh new variable @@ -116,15 +116,15 @@ namespace Microsoft.Boogie.AbstractInterpretation { public class BoogieValueFactory : BoogieFactory, AI.IValueExprFactory { public AI.IFunApp Eq(AI.IExpr e0, AI.IExpr e1) { - Contract.Requires(e0 != null); - Contract.Requires(e1 != null); + //Contract.Requires(e0 != null); + //Contract.Requires(e1 != null); Contract.Ensures(Contract.Result() != null); return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1)); } public AI.IFunApp Neq(AI.IExpr e0, AI.IExpr e1) { - Contract.Requires(e0 != null); - Contract.Requires(e1 != null); + //Contract.Requires(e0 != null); + //Contract.Requires(e1 != null); Contract.Ensures(Contract.Result() != null); return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1)); } @@ -132,15 +132,15 @@ namespace Microsoft.Boogie.AbstractInterpretation { public class BoogieNullnessFactory : BoogieFactory, AI.INullnessFactory { public AI.IFunApp Eq(AI.IExpr e0, AI.IExpr e1) { - Contract.Requires(e0 != null); - Contract.Requires(e1 != null); + //Contract.Requires(e0 != null); + //Contract.Requires(e1 != null); Contract.Ensures(Contract.Result() != null); return Expr.Eq(IExpr2Expr(e0), IExpr2Expr(e1)); } public AI.IFunApp Neq(AI.IExpr e0, AI.IExpr e1) { - Contract.Requires(e0 != null); - Contract.Requires(e1 != null); + //Contract.Requires(e0 != null); + //Contract.Requires(e1 != null); Contract.Ensures(Contract.Result() != null); return Expr.Neq(IExpr2Expr(e0), IExpr2Expr(e1)); } @@ -163,14 +163,14 @@ namespace Microsoft.Boogie.AbstractInterpretation { public class BoogieLinearFactory : BoogieIntFactory, AI.ILinearExprFactory { public AI.IFunApp AtMost(AI.IExpr e0, AI.IExpr e1) { - Contract.Requires(e0 != null); - Contract.Requires(e1 != null); + //Contract.Requires(e0 != null); + //Contract.Requires(e1 != null); Contract.Ensures(Contract.Result() != null); return Expr.Le(IExpr2Expr(e0), IExpr2Expr(e1)); } public AI.IFunApp Add(AI.IExpr e0, AI.IExpr e1) { - Contract.Requires(e0 != null); - Contract.Requires(e1 != null); + //Contract.Requires(e0 != null); + //Contract.Requires(e1 != null); Contract.Ensures(Contract.Result() != null); return Expr.Add(IExpr2Expr(e0), IExpr2Expr(e1)); } @@ -208,8 +208,8 @@ namespace Microsoft.Boogie.AbstractInterpretation { } } public AI.IFunApp And(AI.IExpr p, AI.IExpr q) { - Contract.Requires(p != null); - Contract.Requires(q != null); + //Contract.Requires(p != null); + //Contract.Requires(q != null); Contract.Ensures(Contract.Result() != null); return Expr.Binary(BinaryOperator.Opcode.And, IExpr2Expr(p), IExpr2Expr(q)); @@ -232,7 +232,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { /// [Pure] public bool IsTypeConstant(AI.IExpr t) { - Contract.Requires(t != null); + //Contract.Requires(t != null); Contract.Ensures(Contract.Result() == (t is Constant)); return t is Constant; } @@ -242,8 +242,8 @@ namespace Microsoft.Boogie.AbstractInterpretation { /// [Pure] public bool IsTypeEqual(AI.IExpr t0, AI.IExpr t1) { - Contract.Requires(t0 != null); - Contract.Requires(t1 != null); + //Contract.Requires(t0 != null); + //Contract.Requires(t1 != null); Constant c0 = t0 as Constant; Constant c1 = t1 as Constant; return c0 != null && c1 != null && c0 == c1; @@ -254,8 +254,8 @@ namespace Microsoft.Boogie.AbstractInterpretation { /// [Pure] public bool IsSubType(AI.IExpr t0, AI.IExpr t1) { - Contract.Requires(t0 != null); - Contract.Requires(t1 != null); + //Contract.Requires(t0 != null); + //Contract.Requires(t1 != null); Contract.Assert(false); // BUGBUG: TODO throw new cce.UnreachableException(); @@ -266,8 +266,8 @@ namespace Microsoft.Boogie.AbstractInterpretation { /// that "t0" and "t1" both represent types. /// public AI.IExpr JoinTypes(AI.IExpr t0, AI.IExpr t1) { - Contract.Requires(t0 != null); - Contract.Requires(t1 != null); + //Contract.Requires(t0 != null); + //Contract.Requires(t1 != null); Contract.Ensures(Contract.Result() != null); @@ -279,8 +279,8 @@ namespace Microsoft.Boogie.AbstractInterpretation { //PM: We need this assume because Boogie does not yet allow us to use the //PM: inherited precondition "requires IsTypeConstant(type)". //PM: Note that that precondition is currently commented out. - Contract.Requires(e != null); - Contract.Requires(type != null); + //Contract.Requires(e != null); + //Contract.Requires(type != null); Contract.Ensures(Contract.Result() != null); Contract.Assume(type is Constant); @@ -295,12 +295,13 @@ namespace Microsoft.Boogie.AbstractInterpretation { } public AI.IFunApp IsA(AI.IExpr e, AI.IExpr type) { + //Contract.Requires(e != null); + //Contract.Requires(type != null); + Contract.Ensures(Contract.Result() != null); //PM: We need this assume because Boogie does not yet allow us to use the //PM: inherited precondition "requires IsTypeConstant(type)". //PM: Note that that precondition is currently commented out. - Contract.Requires(e != null); - Contract.Requires(type != null); - Contract.Ensures(Contract.Result() != null); + Contract.Assume(type is Constant); Contract.Assert(false); diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index e8fdc385..1f5dca86 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -1121,7 +1121,7 @@ namespace Microsoft.Boogie { } public override void Emit(TokenTextWriter stream, int level) { - Contract.Requires(stream != null); + //Contract.Requires(stream != null); stream.Write(this, level, "var "); EmitAttributes(stream); EmitVitals(stream, level); @@ -1135,7 +1135,7 @@ namespace Microsoft.Boogie { this.TypedIdent.Emit(stream); } public override void Resolve(ResolutionContext rc) { - Contract.Requires(rc != null); + //Contract.Requires(rc != null); this.TypedIdent.Resolve(rc); } public void ResolveWhere(ResolutionContext rc) { @@ -1146,13 +1146,13 @@ namespace Microsoft.Boogie { ResolveAttributes(rc); } public override void Typecheck(TypecheckingContext tc) { - Contract.Requires(tc != null); + //Contract.Requires(tc != null); TypecheckAttributes(tc); this.TypedIdent.Typecheck(tc); } [Pure] public object DoVisit(AI.ExprVisitor visitor) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.VisitVariable(this); } } diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index f5771f7f..3797d551 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -598,7 +598,7 @@ namespace Microsoft.Boogie { } } public Microsoft.AbstractInterpretationFramework.IFunApp CloneWithArguments(IList/**/ args) { - Contract.Requires(args != null); + //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(args.Count == 0); return this; @@ -622,7 +622,7 @@ namespace Microsoft.Boogie { } [Pure] public object DoVisit(AI.ExprVisitor visitor) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.VisitFunApp(this); } @@ -923,14 +923,14 @@ namespace Microsoft.Boogie { } public AI.IFunApp CloneWithArguments(IList newargs) { - Contract.Requires(newargs != null); + //Contract.Requires(newargs != null); Contract.Ensures(Contract.Result() != null); return this; } [Pure] public object DoVisit(AI.ExprVisitor visitor) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.VisitFunApp(this); } @@ -1038,11 +1038,11 @@ namespace Microsoft.Boogie { } [Pure] public object DoVisit(AI.ExprVisitor visitor) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.VisitFunApp(this); } public AI.IFunApp CloneWithArguments(IList/**/ args) { - Contract.Requires(args != null); + //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); Contract.Assume(args.Count == 1); AI.IExpr/*!*/ iexpr = (AI.IExpr)cce.NonNull(args[0]); @@ -1985,7 +1985,7 @@ namespace Microsoft.Boogie { virtual public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) { //Contract.Requires(stream != null); - Contract.Requires(args != null); + //Contract.Requires(args != null); this.name.Emit(stream, 0xF0, false); stream.Write("("); args.Emit(stream); @@ -1993,7 +1993,7 @@ namespace Microsoft.Boogie { } public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { //Contract.Requires(subjectForErrorReporting != null); - Contract.Requires(rc != null); + //Contract.Requires(rc != null); if (Func != null) { // already resolved return; @@ -2291,14 +2291,14 @@ namespace Microsoft.Boogie { } } public AI.IFunApp CloneWithArguments(IList/**/ args) { - Contract.Requires(args != null); + //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); return new NAryExpr(this.tok, this.Fun, BoogieFactory.IExprArray2ExprSeq(args)); } [Pure] public object DoVisit(AI.ExprVisitor visitor) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.VisitFunApp(this); } @@ -2715,7 +2715,7 @@ namespace Microsoft.Boogie { public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) { //Contract.Requires(subjectForErrorReporting != null); - Contract.Requires(rc != null); + //Contract.Requires(rc != null); // PR: nothing? } @@ -2810,7 +2810,7 @@ namespace Microsoft.Boogie { } [Pure] public object DoVisit(AI.ExprVisitor visitor) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return this; } @@ -3013,7 +3013,7 @@ namespace Microsoft.Boogie { } } public AI.IFunApp CloneWithArguments(IList/**/ args) { - Contract.Requires(args != null); + //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); AI.IFunApp retFun; @@ -3033,7 +3033,7 @@ namespace Microsoft.Boogie { [Pure] public object DoVisit(AI.ExprVisitor visitor) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.VisitFunApp(this); } @@ -3161,7 +3161,7 @@ namespace Microsoft.Boogie { } } public AI.IFunApp CloneWithArguments(IList/**/ args) { - Contract.Requires(args != null); + //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); AI.IFunApp/*!*/ retFun; diff --git a/Source/Core/AbsyQuant.cs b/Source/Core/AbsyQuant.cs index c30211ca..e677f85c 100644 --- a/Source/Core/AbsyQuant.cs +++ b/Source/Core/AbsyQuant.cs @@ -257,7 +257,7 @@ namespace Microsoft.Boogie { [Pure] public object DoVisit(AI.ExprVisitor visitor) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.VisitFunApp(this); } @@ -284,7 +284,7 @@ namespace Microsoft.Boogie { } public AI.IFunApp CloneWithArguments(IList/**/ args) { - Contract.Requires(args != null); + //Contract.Requires(args != null); Contract.Ensures(Contract.Result() != null); Contract.Assume(args.Count == 1); @@ -336,7 +336,7 @@ namespace Microsoft.Boogie { [Pure] public object DoVisit(AI.ExprVisitor visitor) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.VisitFunction(this); } @@ -377,7 +377,7 @@ namespace Microsoft.Boogie { } } public AI.IFunction CloneWithBody(AI.IExpr body) { - Contract.Requires(body != null); + //Contract.Requires(body != null); Contract.Ensures(Contract.Result() != null); BinderExpr realquant; diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 7f3baa67..288f5769 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -904,7 +904,7 @@ namespace Microsoft.Boogie { public override bool Unify(Type that, TypeVariableSeq unifiableVariables, IDictionary/*!*/ unifier) { //Contract.Requires(unifiableVariables != null); //Contract.Requires(that != null); - Contract.Requires(cce.NonNullElements(unifier)); + //Contract.Requires(cce.NonNullElements(unifier)); // an idempotent substitution that describes the // unification result up to a certain point @@ -1068,7 +1068,7 @@ namespace Microsoft.Boogie { IDictionary/*!*/ unifier) { //Contract.Requires(that != null); //Contract.Requires(unifiableVariables != null); - Contract.Requires(cce.NonNullElements(unifier)); + //Contract.Requires(cce.NonNullElements(unifier)); that = that.Expanded; if (that is TypeProxy || that is TypeVariable) { return that.Unify(this, unifiableVariables, unifier); @@ -1218,9 +1218,9 @@ Contract.Requires(that != null); public override bool Equals(Type that, TypeVariableSeq/*!*/ thisBoundVariables, TypeVariableSeq/*!*/ thatBoundVariables) { - Contract.Requires(thisBoundVariables != null); - Contract.Requires(thatBoundVariables != null); - Contract.Requires(that != null); + //Contract.Requires(thisBoundVariables != null); + //Contract.Requires(thatBoundVariables != null); + //Contract.Requires(that != null); System.Diagnostics.Debug.Fail("UnresolvedTypeIdentifier.Equals should never be called"); return false; // to make the compiler happy } @@ -1230,9 +1230,9 @@ Contract.Requires(that != null); public override bool Unify(Type that, TypeVariableSeq/*!*/ unifiableVariables, IDictionary result) { - Contract.Requires(unifiableVariables != null); - Contract.Requires(cce.NonNullElements(result)); - Contract.Requires(that != null); + //Contract.Requires(unifiableVariables != null); + //Contract.Requires(cce.NonNullElements(result)); + //Contract.Requires(that != null); { Contract.Assert(false); throw new cce.UnreachableException(); @@ -1254,7 +1254,7 @@ Contract.Requires(that != null); //----------- Substitution of free variables with types not containing bound variables ----------------- public override Type Substitute(IDictionary/*!*/ subst) { - Contract.Requires(cce.NonNullElements(subst)); + //Contract.Requires(cce.NonNullElements(subst)); Contract.Ensures(Contract.Result() != null); { Contract.Assert(false); @@ -1266,7 +1266,7 @@ Contract.Requires(that != null); [Pure] public override int GetHashCode(TypeVariableSeq boundVariables) { - Contract.Requires(boundVariables != null); + //Contract.Requires(boundVariables != null); { Contract.Assert(false); throw new cce.UnreachableException(); @@ -1276,7 +1276,7 @@ Contract.Requires(that != null); //----------- Resolution ---------------------------------- public override Type ResolveType(ResolutionContext rc) { - Contract.Requires(rc != null); + //Contract.Requires(rc != null); Contract.Ensures(Contract.Result() != null); // first case: the type name denotes a bitvector-type if (Name.StartsWith("bv") && Name.Length > 2) { @@ -1392,7 +1392,7 @@ Contract.Requires(that != null); } public override Absy StdDispatch(StandardVisitor visitor) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); Contract.Ensures(Contract.Result() != null); return visitor.VisitUnresolvedTypeIdentifier(this); } diff --git a/Source/Core/DeadVarElim.cs b/Source/Core/DeadVarElim.cs index 240920c5..4eafdbbb 100644 --- a/Source/Core/DeadVarElim.cs +++ b/Source/Core/DeadVarElim.cs @@ -18,7 +18,7 @@ namespace Microsoft.Boogie { } public override Implementation VisitImplementation(Implementation node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); //Console.WriteLine("Procedure {0}", node.Name); Implementation/*!*/ impl = base.VisitImplementation(node); @@ -181,7 +181,7 @@ namespace Microsoft.Boogie { } public override Expr VisitOldExpr(OldExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); insideOldExpr++; node.Expr = this.VisitExpr(node.Expr); @@ -190,7 +190,7 @@ namespace Microsoft.Boogie { } public override Expr VisitIdentifierExpr(IdentifierExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); if (node.Decl != null) { usedVars.Add(node.Decl); diff --git a/Source/Provers/Isabelle/Prover.cs b/Source/Provers/Isabelle/Prover.cs index 696095eb..3544458e 100644 --- a/Source/Provers/Isabelle/Prover.cs +++ b/Source/Provers/Isabelle/Prover.cs @@ -936,7 +936,7 @@ namespace Microsoft.Boogie.Isabelle { public bool VisitBvConcatOp(VCExprNAry node, B2I b2i) { //Contract.Requires(node != null); //Contract.Requires(b2i != null); - Contract.Requires(node.Length >= 2); + //Contract.Requires(node.Length >= 2); VCExpr child1 = node[0]; Contract.Assert(child1 != null); diff --git a/Source/Provers/Simplify/Prover.cs b/Source/Provers/Simplify/Prover.cs index b789e588..e4a72a89 100644 --- a/Source/Provers/Simplify/Prover.cs +++ b/Source/Provers/Simplify/Prover.cs @@ -507,7 +507,7 @@ namespace Microsoft.Boogie.Simplify { protected override void DoBeginCheck(string descriptiveName, string formula) { //Contract.Requires(descriptiveName != null); - Contract.Requires(formula != null); + //Contract.Requires(formula != null); //simplify.Refresh(); //this.Comment("@@@@ Virtual Memory: " + simplify.PeakVirtualMemorySize64); //this.Comment("@@@@ Working Set: " + simplify.PeakWorkingSet64); diff --git a/Source/Provers/Simplify/ProverInterface.cs b/Source/Provers/Simplify/ProverInterface.cs index d300a685..1f563c0f 100644 --- a/Source/Provers/Simplify/ProverInterface.cs +++ b/Source/Provers/Simplify/ProverInterface.cs @@ -384,7 +384,7 @@ namespace Microsoft.Boogie.Simplify { public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) { //Contract.Requires(descriptiveName != null); //Contract.Requires(vc != null); - Contract.Requires(handler != null); + //Contract.Requires(handler != null); this.NewProblem(descriptiveName); this.proverException = null; diff --git a/Source/Provers/Z3/Inspector.cs b/Source/Provers/Z3/Inspector.cs index 3675f6a7..638acdb0 100644 --- a/Source/Provers/Z3/Inspector.cs +++ b/Source/Provers/Z3/Inspector.cs @@ -36,7 +36,7 @@ void ObjectInvariant() } protected override bool StandardResult(VCExpr node, bool arg) { - Contract.Requires(node!=null); + //Contract.Requires(node!=null); VCExprNAry nary = node as VCExprNAry; if (nary != null) { VCExprLabelOp lab = nary.Op as VCExprLabelOp; diff --git a/Source/Provers/Z3/Prover.cs b/Source/Provers/Z3/Prover.cs index c93b364d..a36ca87a 100644 --- a/Source/Provers/Z3/Prover.cs +++ b/Source/Provers/Z3/Prover.cs @@ -234,8 +234,8 @@ namespace Microsoft.Boogie.Z3 } protected override void DoBeginCheck(string descriptiveName, string formula) { - Contract.Requires(descriptiveName != null); - Contract.Requires(formula != null); + //Contract.Requires(descriptiveName != null); + //Contract.Requires(formula != null); ToWriteLine(formula); ToWriteLine(String.Format("; END OF FORMULA {0} - {1}", NumFormulasChecked.ToString(), descriptiveName)); ToFlush(); @@ -254,7 +254,7 @@ namespace Microsoft.Boogie.Z3 } public override ProverOutcome CheckOutcome(Microsoft.Boogie.ProverInterface.ErrorHandler handler) { - Contract.Requires(handler != null); + //Contract.Requires(handler != null); Contract.EnsuresOnThrow(true); //ProverOutcome outcome; bool isInvalid = false; @@ -920,7 +920,7 @@ namespace Microsoft.Boogie.Z3 } public override void Print(TextWriter writer) { - Contract.Requires(writer != null); + //Contract.Requires(writer != null); if (CommandLineOptions.Clo.PrintErrorModel == 4) { PrintReadableModel(writer); return; diff --git a/Source/Provers/Z3/ProverInterface.cs b/Source/Provers/Z3/ProverInterface.cs index 3813c63b..9289b5b7 100644 --- a/Source/Provers/Z3/ProverInterface.cs +++ b/Source/Provers/Z3/ProverInterface.cs @@ -53,7 +53,7 @@ void ObjectInvariant() } protected override Microsoft.Boogie.Simplify.ProverProcess CreateProverProcess(string proverPath) { - Contract.Requires(proverPath!= null); + //Contract.Requires(proverPath!= null); Contract.Ensures(Contract.Result() != null); @@ -66,7 +66,7 @@ void ObjectInvariant() } protected override AxiomVCExprTranslator SpawnVCExprTranslator(ProverOptions opts) { - Contract.Requires(opts != null); + //Contract.Requires(opts != null); Contract.Ensures(Contract.Result() != null); return new Z3VCExprTranslator(gen, (Z3InstanceOptions) opts); @@ -74,9 +74,9 @@ void ObjectInvariant() public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) { - Contract.Requires(descriptiveName != null); - Contract.Requires(vc != null); - Contract.Requires(handler != null); + //Contract.Requires(descriptiveName != null); + //Contract.Requires(vc != null); + //Contract.Requires(handler != null); FireUpInspector(); if (inspector != null) { inspector.NewProblem(descriptiveName, vc, handler); @@ -115,7 +115,7 @@ void ObjectInvariant() protected override bool Parse(string opt) { - Contract.Requires(opt!=null); + //Contract.Requires(opt!=null); return ParseBool(opt, "REVERSE_IMPLIES", ref InverseImplies) || ParseString(opt, "INSPECTOR", ref Inspector) || ParseBool(opt, "DIST", ref DistZ3) || @@ -211,7 +211,7 @@ REVERSE_IMPLIES= Encode P==>Q as Q||!P. } } public override LineariserOptions AddLetVariable(VCExprVar furtherVar) { - Contract.Requires(furtherVar != null); + //Contract.Requires(furtherVar != null); Contract.Ensures(Contract.Result() != null); List!*/> allVars = new List(); @@ -221,7 +221,7 @@ REVERSE_IMPLIES= Encode P==>Q as Q||!P. } public override LineariserOptions AddLetVariables(List!*/> furtherVars) { - Contract.Requires(furtherVars != null); + //Contract.Requires(furtherVars != null); Contract.Ensures(Contract.Result() != null); List!*/> allVars = new List (); @@ -292,14 +292,14 @@ REVERSE_IMPLIES= Encode P==>Q as Q||!P. public override string Lookup(VCExprVar var) { - Contract.Requires(var != null); + //Contract.Requires(var != null); Contract.Ensures(Contract.Result() != null); return Namer.Lookup(var); } public override string translate(VCExpr expr, int polarity) { - Contract.Requires(expr != null); + //Contract.Requires(expr != null); Contract.Ensures(Contract.Result() != null); DateTime start = DateTime.Now; @@ -385,8 +385,8 @@ REVERSE_IMPLIES= Encode P==>Q as Q||!P. public override object SpawnProver(ProverOptions popts, object ctxt) { - Contract.Requires(popts != null); - Contract.Requires(ctxt != null); + //Contract.Requires(popts != null); + //Contract.Requires(ctxt != null); Contract.Ensures(Contract.Result() != null); Z3InstanceOptions opts = cce.NonNull((Z3InstanceOptions)popts); @@ -396,8 +396,8 @@ REVERSE_IMPLIES= Encode P==>Q as Q||!P. } public override object NewProverContext(ProverOptions options) { - Contract.Requires(options != null); - Contract.Ensures(Contract.Result() != null); + //Contract.Requires(options != null); + //Contract.Ensures(Contract.Result() != null); if (CommandLineOptions.Clo.BracketIdsInVC < 0) { CommandLineOptions.Clo.BracketIdsInVC = 0; diff --git a/Source/Provers/Z3/TypeDeclCollector.cs b/Source/Provers/Z3/TypeDeclCollector.cs index 7cdc6f4f..cd01e325 100644 --- a/Source/Provers/Z3/TypeDeclCollector.cs +++ b/Source/Provers/Z3/TypeDeclCollector.cs @@ -73,7 +73,7 @@ void ObjectInvariant() // not used protected override bool StandardResult(VCExpr node, bool arg) { - Contract.Requires(node != null); + //Contract.Requires(node != null); return true; } diff --git a/Source/VCExpr/BigLiteralAbstracter.cs b/Source/VCExpr/BigLiteralAbstracter.cs index 63d87e17..7eb93541 100644 --- a/Source/VCExpr/BigLiteralAbstracter.cs +++ b/Source/VCExpr/BigLiteralAbstracter.cs @@ -15,23 +15,24 @@ using Microsoft.Basetypes; // constants. This is necessary for Simplify, which cannot deal with // literals larger than 32 bits -namespace Microsoft.Boogie.VCExprAST -{ +namespace Microsoft.Boogie.VCExprAST { public class BigLiteralAbstracter : MutatingVCExprVisitor, ICloneable { - public BigLiteralAbstracter(VCExpressionGenerator gen) :base(gen){ + public BigLiteralAbstracter(VCExpressionGenerator gen) + : base(gen) { Contract.Requires(gen != null); DummyVar = gen.Variable("x", Type.Int); - IncAxioms = new List (); - Literals = new List> (); + IncAxioms = new List(); + Literals = new List>(); } - private BigLiteralAbstracter(BigLiteralAbstracter abstracter) :base(abstracter.Gen){ + private BigLiteralAbstracter(BigLiteralAbstracter abstracter) + : base(abstracter.Gen) { Contract.Requires(abstracter != null); DummyVar = abstracter.DummyVar; - IncAxioms = new List (abstracter.IncAxioms); - Literals = new List> (abstracter.Literals); + IncAxioms = new List(abstracter.IncAxioms); + Literals = new List>(abstracter.Literals); } public Object Clone() { @@ -59,10 +60,9 @@ namespace Microsoft.Boogie.VCExprAST private readonly List/*!*/ IncAxioms; [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(cce.NonNullElements(IncAxioms)); -} + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(IncAxioms)); + } private void AddAxiom(VCExpr/*!*/ axiom) { Contract.Requires(axiom != null); @@ -72,7 +72,7 @@ void ObjectInvariant() // Return all axioms that were added since the last time NewAxioms // was called public VCExpr GetNewAxioms() { -Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); VCExpr res = Gen.NAry(VCExpressionGenerator.AndOp, IncAxioms); IncAxioms.Clear(); return res; @@ -86,39 +86,38 @@ Contract.Ensures(Contract.Result() != null); private readonly List>/*!*/ Literals; [ContractInvariantMethod] -void ObjectInvariat() -{ - Contract.Invariant(Literals!=null); - Contract.Invariant(Contract.ForAll(Literals,i=>i.Value!=null)); -} + void ObjectInvariat() { + Contract.Invariant(Literals != null); + Contract.Invariant(Contract.ForAll(Literals, i => i.Value != null)); + } + - private class EntryComparerC : IComparer> { public int Compare(KeyValuePair a, - KeyValuePair b) {Contract.Requires(a.Value!=null); - Contract.Requires(b.Value!=null); + KeyValuePair b) { + //Contract.Requires(a.Value!=null); + //Contract.Requires(b.Value!=null); return a.Key.CompareTo(b.Key); } } - private static readonly EntryComparerC EntryComparer = new EntryComparerC (); + private static readonly EntryComparerC EntryComparer = new EntryComparerC(); // variable used when searching for entries in the literal list private readonly VCExprVar/*!*/ DummyVar; [ContractInvariantMethod] -void ObjectInvarint() -{ - Contract.Invariant(DummyVar!=null); -} + void ObjectInvarint() { + Contract.Invariant(DummyVar != null); + } //////////////////////////////////////////////////////////////////////////// - + // Construct an expression to represent the given (large) integer // literal. Constants are defined and axiomatised if necessary private VCExpr Represent(BigNum lit) { -Contract.Requires((NegConstantDistance > lit || lit > ConstantDistance)); -Contract.Ensures(Contract.Result() != null); + Contract.Requires((NegConstantDistance > lit || lit > ConstantDistance)); + Contract.Ensures(Contract.Result() != null); if (lit.IsNegative) return Gen.Function(VCExpressionGenerator.SubOp, @@ -128,14 +127,14 @@ Contract.Ensures(Contract.Result() != null); } private VCExpr RepresentPos(BigNum lit) { -Contract.Requires((lit > ConstantDistance)); -Contract.Ensures(Contract.Result() != null); - + Contract.Requires((lit > ConstantDistance)); + Contract.Ensures(Contract.Result() != null); + int index = GetIndexFor(lit); if (index >= 0) // precise match return Literals[index].Value; - + // check whether a constant is defined that is at most // ConstantDistance away from lit index = ~index; @@ -168,33 +167,33 @@ Contract.Ensures(Contract.Result() != null); } private VCExpr AddConstantFor(BigNum lit) { -Contract.Requires((lit > ConstantDistance)); -Contract.Ensures(Contract.Result() != null); - + Contract.Requires((lit > ConstantDistance)); + Contract.Ensures(Contract.Result() != null); + VCExprVar res = Gen.Variable("int#" + lit, Type.Int); int index = GetIndexFor(lit); Contract.Assert(index < 0); index = ~index; Literals.Insert(index, new KeyValuePair(lit, res)); - + // relate the new constant to the predecessor and successor if (index > 0) DefineRelationship(Literals[index - 1].Value, Literals[index - 1].Key, res, lit); else DefineRelationship(Gen.Integer(BigNum.ZERO), BigNum.ZERO, res, lit); - + if (index < Literals.Count - 1) DefineRelationship(res, lit, Literals[index + 1].Value, Literals[index + 1].Key); return res; } - + private void DefineRelationship(VCExpr/*!*/ aExpr, BigNum aValue, - VCExpr/*!*/ bExpr, BigNum bValue) - {Contract.Requires(aValue < bValue); + VCExpr/*!*/ bExpr, BigNum bValue) { + Contract.Requires(aValue < bValue); Contract.Requires(aExpr != null); Contract.Requires(bExpr != null); @@ -219,7 +218,7 @@ Contract.Ensures(Contract.Result() != null); public override VCExpr Visit(VCExprLiteral node, bool arg) { Contract.Requires(node != null); -Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); VCExprIntLit intLit = node as VCExprIntLit; if (intLit != null) { if (NegConstantDistance > intLit.Val || intLit.Val > ConstantDistance) diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index a2b0c041..b90196e2 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -200,10 +200,10 @@ namespace Microsoft.Boogie.VCExprAST { VCExprVar res; foreach (Dictionary/*!*/ d in Mapping) { //Contract.Assert(cce.NonNullElements(d)); - if (d.TryGetValue(boogieVar, out res)) { - Contract.Assert(res != null); - return res; - } + if (d.TryGetValue(boogieVar, out res)) { + Contract.Assert(res != null); + return res; + } } return null; } @@ -288,7 +288,7 @@ namespace Microsoft.Boogie.VCExprAST { /////////////////////////////////////////////////////////////////////////////////// public override LiteralExpr VisitLiteralExpr(LiteralExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Push(TranslateLiteralExpr(node)); return node; @@ -317,7 +317,7 @@ namespace Microsoft.Boogie.VCExprAST { /////////////////////////////////////////////////////////////////////////////////// public override AIVariableExpr VisitAIVariableExpr(AIVariableExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); @@ -326,7 +326,7 @@ namespace Microsoft.Boogie.VCExprAST { /////////////////////////////////////////////////////////////////////////////////// public override Expr VisitIdentifierExpr(IdentifierExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assume(node.Decl != null); // the expression has to be resolved Push(LookupVariable(node.Decl)); @@ -340,7 +340,7 @@ namespace Microsoft.Boogie.VCExprAST { // causes it to become "x0". So we just remove old expressions with a visitor // before transforming it into a VCExpr. public override Expr VisitOldExpr(OldExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); @@ -349,7 +349,7 @@ namespace Microsoft.Boogie.VCExprAST { /////////////////////////////////////////////////////////////////////////////////// public override Expr VisitNAryExpr(NAryExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Push(TranslateNAryExpr(node)); return node; @@ -399,21 +399,21 @@ namespace Microsoft.Boogie.VCExprAST { /////////////////////////////////////////////////////////////////////////////////// public override QuantifierExpr VisitQuantifierExpr(QuantifierExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Push(TranslateQuantifierExpr(node)); return node; } public override ExistsExpr VisitExistsExpr(ExistsExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); node = (ExistsExpr)this.VisitQuantifierExpr(node); return node; } public override ForallExpr VisitForallExpr(ForallExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); node = (ForallExpr)this.VisitQuantifierExpr(node); return node; @@ -509,32 +509,32 @@ namespace Microsoft.Boogie.VCExprAST { /////////////////////////////////////////////////////////////////////////////////// public override BvExtractExpr VisitBvExtractExpr(BvExtractExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Push(TranslateBvExtractExpr(node)); return node; } - private VCExpr TranslateBvExtractExpr(BvExtractExpr node){ -Contract.Requires(node != null); -Contract.Requires((node.Start <= node.End)); -Contract.Ensures(Contract.Result() != null); -VCExpr/*!*/ bv = Translate(node.Bitvector); - return Gen.BvExtract(bv,cce.NonNull(node.Bitvector.Type).BvBits, node.Start, node.End); + private VCExpr TranslateBvExtractExpr(BvExtractExpr node) { + Contract.Requires(node != null); + Contract.Requires((node.Start <= node.End)); + Contract.Ensures(Contract.Result() != null); + VCExpr/*!*/ bv = Translate(node.Bitvector); + return Gen.BvExtract(bv, cce.NonNull(node.Bitvector.Type).BvBits, node.Start, node.End); } /////////////////////////////////////////////////////////////////////////////////// public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Push(TranslateBvConcatExpr(node)); return node; } - private VCExpr TranslateBvConcatExpr(BvConcatExpr node){ -Contract.Requires(node != null); -Contract.Ensures(Contract.Result() != null); + private VCExpr TranslateBvConcatExpr(BvConcatExpr node) { + Contract.Requires(node != null); + Contract.Ensures(Contract.Result() != null); VCExpr/*!*/ bv0 = Translate(node.E0); VCExpr/*!*/ bv1 = Translate(node.E1); return Gen.BvConcat(bv0, bv1); @@ -544,60 +544,59 @@ Contract.Ensures(Contract.Result() != null); // all the other cases should never happen public override Cmd VisitAssertCmd(AssertCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Cmd VisitAssignCmd(AssignCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Cmd VisitAssumeCmd(AssumeCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override AtomicRE VisitAtomicRE(AtomicRE node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Axiom VisitAxiom(Axiom node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Type VisitBasicType(BasicType node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Type VisitBvType(BvType node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Block VisitBlock(Block node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } CodeExprConverter codeExprConverter = null; - public void SetCodeExprConverter(CodeExprConverter f){ + public void SetCodeExprConverter(CodeExprConverter f) { this.codeExprConverter = f; } - public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr) - { - Contract.Requires(codeExpr != null); + public override Expr/*!*/ VisitCodeExpr(CodeExpr/*!*/ codeExpr) { + //Contract.Requires(codeExpr != null); Contract.Ensures(Contract.Result() != null); Contract.Assume(codeExprConverter != null); @@ -609,271 +608,271 @@ Contract.Ensures(Contract.Result() != null); return codeExpr; } public override BlockSeq VisitBlockSeq(BlockSeq blockSeq) { - Contract.Requires(blockSeq != null); + //Contract.Requires(blockSeq != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override List/*!*/ VisitBlockList(List/*!*/ blocks) { - Contract.Requires(cce.NonNullElements(blocks)); + //Contract.Requires(cce.NonNullElements(blocks)); Contract.Ensures(cce.NonNullElements(Contract.Result>())); Contract.Assert(false); throw new cce.UnreachableException(); } public override BoundVariable VisitBoundVariable(BoundVariable node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Cmd VisitCallCmd(CallCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Cmd VisitCallForallCmd(CallForallCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override CmdSeq VisitCmdSeq(CmdSeq cmdSeq) { - Contract.Requires(cmdSeq != null); + //Contract.Requires(cmdSeq != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Choice VisitChoice(Choice node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Cmd VisitCommentCmd(CommentCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Constant VisitConstant(Constant node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override CtorType VisitCtorType(CtorType node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Declaration VisitDeclaration(Declaration node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override List/*!*/ VisitDeclarationList(List/*!*/ declarationList) { - Contract.Requires(cce.NonNullElements(declarationList)); + //Contract.Requires(cce.NonNullElements(declarationList)); Contract.Ensures(cce.NonNullElements(Contract.Result>())); Contract.Assert(false); throw new cce.UnreachableException(); } public override DeclWithFormals VisitDeclWithFormals(DeclWithFormals node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Requires VisitRequires(Requires @requires) { - Contract.Requires(@requires != null); + //Contract.Requires(@requires != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override RequiresSeq VisitRequiresSeq(RequiresSeq requiresSeq) { - Contract.Requires(requiresSeq != null); + //Contract.Requires(requiresSeq != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Ensures VisitEnsures(Ensures @ensures) { - Contract.Requires(@ensures != null); + //Contract.Requires(@ensures != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override EnsuresSeq VisitEnsuresSeq(EnsuresSeq ensuresSeq) { - Contract.Requires(ensuresSeq != null); + //Contract.Requires(ensuresSeq != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Formal VisitFormal(Formal node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Function VisitFunction(Function node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override GlobalVariable VisitGlobalVariable(GlobalVariable node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override GotoCmd VisitGotoCmd(GotoCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Cmd VisitHavocCmd(HavocCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Implementation VisitImplementation(Implementation node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override LocalVariable VisitLocalVariable(LocalVariable node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override AssignLhs VisitMapAssignLhs(MapAssignLhs node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override MapType VisitMapType(MapType node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Procedure VisitProcedure(Procedure node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Program VisitProgram(Program node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Cmd VisitRE(RE node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override RESeq VisitRESeq(RESeq reSeq) { - Contract.Requires(reSeq != null); + //Contract.Requires(reSeq != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override ReturnCmd VisitReturnCmd(ReturnCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override ReturnExprCmd VisitReturnExprCmd(ReturnExprCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Sequential VisitSequential(Sequential node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override AssignLhs VisitSimpleAssignLhs(SimpleAssignLhs node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Cmd VisitStateCmd(StateCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override TransferCmd VisitTransferCmd(TransferCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Trigger VisitTrigger(Trigger node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Type VisitType(Type node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override TypedIdent VisitTypedIdent(TypedIdent node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Type VisitTypeSynonymAnnotation(TypeSynonymAnnotation node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Type VisitTypeVariable(TypeVariable node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Variable VisitVariable(Variable node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override VariableSeq VisitVariableSeq(VariableSeq variableSeq) { - Contract.Requires(variableSeq != null); + //Contract.Requires(variableSeq != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Cmd VisitAssertEnsuresCmd(AssertEnsuresCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); } public override Cmd VisitAssertRequiresCmd(AssertRequiresCmd node) { - Contract.Requires(node != null); + //Contract.Requires(node != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(false); throw new cce.UnreachableException(); @@ -924,13 +923,13 @@ Contract.Ensures(Contract.Result() != null); } - public VCExpr Translate(IAppliable app, Type ty, List/*!*/ args, List/*!*/ typeArgs){ -Contract.Requires(ty != null); -Contract.Requires(app != null); -Contract.Requires(cce.NonNullElements(typeArgs)); -Contract.Requires(cce.NonNullElements(args)); -Contract.Ensures(Contract.Result() != null); - + public VCExpr Translate(IAppliable app, Type ty, List/*!*/ args, List/*!*/ typeArgs) { + Contract.Requires(ty != null); + Contract.Requires(app != null); + Contract.Requires(cce.NonNullElements(typeArgs)); + Contract.Requires(cce.NonNullElements(args)); + Contract.Ensures(Contract.Result() != null); + List/*!*/ oldArgs = this.args; List/*!*/ oldTypeArgs = this.typeArgs; this.args = args; @@ -946,45 +945,45 @@ Contract.Ensures(Contract.Result() != null); public VCExpr Visit(UnaryOperator unaryOperator) { - Contract.Requires(unaryOperator != null); + //Contract.Requires(unaryOperator != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Not && this.args.Count == 1); return Gen.Not(this.args); } public VCExpr Visit(BinaryOperator binaryOperator) { - Contract.Requires(binaryOperator != null); + //Contract.Requires(binaryOperator != null); Contract.Ensures(Contract.Result() != null); return TranslateBinaryOperator(binaryOperator, this.args); } public VCExpr Visit(FunctionCall functionCall) { - Contract.Requires(functionCall != null); + //Contract.Requires(functionCall != null); Contract.Ensures(Contract.Result() != null); return TranslateFunctionCall(functionCall, this.args, this.typeArgs); } public VCExpr Visit(MapSelect mapSelect) { - Contract.Requires(mapSelect != null); + //Contract.Requires(mapSelect != null); Contract.Ensures(Contract.Result() != null); return Gen.Select(this.args, this.typeArgs); } public VCExpr Visit(MapStore mapStore) { - Contract.Requires(mapStore != null); + //Contract.Requires(mapStore != null); Contract.Ensures(Contract.Result() != null); return Gen.Store(this.args, this.typeArgs); } public VCExpr Visit(TypeCoercion typeCoercion) { - Contract.Requires(typeCoercion != null); + //Contract.Requires(typeCoercion != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(this.args.Count == 1); return this.args[0]; } public VCExpr Visit(IfThenElse ite) { - Contract.Requires(ite != null); + //Contract.Requires(ite != null); Contract.Ensures(Contract.Result() != null); return Gen.Function(VCExpressionGenerator.IfThenElseOp, this.args); } @@ -1038,12 +1037,12 @@ Contract.Ensures(Contract.Result() != null); /////////////////////////////////////////////////////////////////////////////// - private VCExpr/*!*/ TranslateFunctionCall(FunctionCall app, List/*!*/ args, List/*!*/ typeArgs){ + private VCExpr/*!*/ TranslateFunctionCall(FunctionCall app, List/*!*/ args, List/*!*/ typeArgs) { Contract.Requires(cce.NonNullElements(args)); Contract.Requires(cce.NonNullElements(typeArgs)); -Contract.Requires(app != null); + Contract.Requires(app != null); Contract.Requires((app.Func != null)); -Contract.Ensures(Contract.Result() != null); // resolution must have happened + Contract.Ensures(Contract.Result() != null); // resolution must have happened VCExpr res = ApplyExpansion(app, args, typeArgs); if (res != null) @@ -1053,8 +1052,8 @@ Contract.Ensures(Contract.Result() != null); // resolution must have return Gen.Function(functionOp, args, typeArgs); } - private VCExpr ApplyExpansion(FunctionCall app, List/*!*/ args, List/*!*/ typeArgs){ -Contract.Requires(app != null); + private VCExpr ApplyExpansion(FunctionCall app, List/*!*/ args, List/*!*/ typeArgs) { + Contract.Requires(app != null); Contract.Requires(cce.NonNullElements(args)); Contract.Requires(cce.NonNullElements(typeArgs)); Contract.Assert(app.Func != null); // resolution must have happened diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index 693fcf76..45eeda43 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -14,18 +14,17 @@ using Microsoft.Boogie.VCExprAST; // a naive method to turn VCExprs into strings that can be fed into Simplify -namespace Microsoft.Boogie.VCExprAST -{ +namespace Microsoft.Boogie.VCExprAST { [ContractClassFor(typeof(LineariserOptions))] - public abstract class LinOptContracts:LineariserOptions{ - public LinOptContracts() : base(true) { + public abstract class LinOptContracts : LineariserOptions { + public LinOptContracts() + : base(true) { } - public override LineariserOptions SetAsTerm(bool newVal) -{ - Contract.Ensures(Contract.Result() != null); - throw new NotImplementedException(); -} - + public override LineariserOptions SetAsTerm(bool newVal) { + Contract.Ensures(Contract.Result() != null); + throw new NotImplementedException(); + } + } // Options for the linearisation. Here one can choose, for instance, @@ -36,52 +35,72 @@ namespace Microsoft.Boogie.VCExprAST public readonly bool AsTerm; public abstract LineariserOptions/*!*/ SetAsTerm(bool newVal); - public abstract bool QuantifierIds { get; } + public abstract bool QuantifierIds { + get; + } - public virtual bool UseWeights { get { return false; } } + public virtual bool UseWeights { + get { + return false; + } + } - public virtual bool InverseImplies { get { return false; } } + public virtual bool InverseImplies { + get { + return false; + } + } // whether to include type specifications in quantifiers - public abstract bool UseTypes { get; } + public abstract bool UseTypes { + get; + } - public virtual CommandLineOptions.BvHandling Bitvectors { get { - return CommandLineOptions.BvHandling.None; - } } + public virtual CommandLineOptions.BvHandling Bitvectors { + get { + return CommandLineOptions.BvHandling.None; + } + } // variables representing formulas in let-bindings have to be // printed in a different way than other variables - public virtual List/*!*/ LetVariables { get {Contract.Ensures(cce.NonNullElements(Contract.Result>())); - return EmptyList; - } } + public virtual List/*!*/ LetVariables { + get { + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + return EmptyList; + } + } - public virtual LineariserOptions AddLetVariable(VCExprVar furtherVar){ -Contract.Requires(furtherVar != null); -Contract.Ensures(Contract.Result() != null); + public virtual LineariserOptions AddLetVariable(VCExprVar furtherVar) { + Contract.Requires(furtherVar != null); + Contract.Ensures(Contract.Result() != null); return this; } - public virtual LineariserOptions AddLetVariables(List/*!*/ furtherVars){ -Contract.Requires(cce.NonNullElements(furtherVars)); -Contract.Ensures(Contract.Result() != null); + public virtual LineariserOptions AddLetVariables(List/*!*/ furtherVars) { + Contract.Requires(cce.NonNullElements(furtherVars)); + Contract.Ensures(Contract.Result() != null); return this; } - + private static readonly List/*!*/ EmptyList = new List(); [ContractInvariantMethod] -void ObjectInvarinat() -{ - Contract.Invariant(EmptyList!=null); -} + void ObjectInvarinat() { + Contract.Invariant(EmptyList != null); + } - public bool NativeBv { get { - return Bitvectors == CommandLineOptions.BvHandling.Z3Native; - } } + public bool NativeBv { + get { + return Bitvectors == CommandLineOptions.BvHandling.Z3Native; + } + } - public bool IntBv { get { - return Bitvectors == CommandLineOptions.BvHandling.ToInt; - } } + public bool IntBv { + get { + return Bitvectors == CommandLineOptions.BvHandling.ToInt; + } + } //////////////////////////////////////////////////////////////////////////////////////// @@ -89,23 +108,28 @@ void ObjectInvarinat() this.AsTerm = asTerm; } - public static readonly LineariserOptions SimplifyDefault = new SimplifyOptions (false); - internal static readonly LineariserOptions SimplifyDefaultTerm = new SimplifyOptions (true); + public static readonly LineariserOptions SimplifyDefault = new SimplifyOptions(false); + internal static readonly LineariserOptions SimplifyDefaultTerm = new SimplifyOptions(true); //////////////////////////////////////////////////////////////////////////////////////// private class SimplifyOptions : LineariserOptions { - internal SimplifyOptions(bool asTerm):base(asTerm) { - + internal SimplifyOptions(bool asTerm) + : base(asTerm) { + + } + public override bool QuantifierIds { + get { + return false; + } + } + public override bool UseTypes { + get { + return false; + } } - public override bool QuantifierIds { get { - return false; - } } - public override bool UseTypes { get { - return false; - } } public override LineariserOptions SetAsTerm(bool newVal) { -Contract.Ensures(Contract.Result() != null); + Contract.Ensures(Contract.Result() != null); if (newVal) return SimplifyDefaultTerm; else @@ -119,21 +143,21 @@ Contract.Ensures(Contract.Result() != null); // Lineariser for expressions. The result (bool) is currently not used for anything public class SimplifyLikeExprLineariser : IVCExprVisitor { - public static string ToSimplifyString(VCExpr e, UniqueNamer namer){ -Contract.Requires(namer != null); -Contract.Requires(e != null); -Contract.Ensures(Contract.Result() != null); + public static string ToSimplifyString(VCExpr e, UniqueNamer namer) { + Contract.Requires(namer != null); + Contract.Requires(e != null); + Contract.Ensures(Contract.Result() != null); return ToString(e, LineariserOptions.SimplifyDefault, namer); } - public static string ToString(VCExpr/*!*/ e, LineariserOptions/*!*/ options,UniqueNamer/*!*/ namer) { + public static string ToString(VCExpr/*!*/ e, LineariserOptions/*!*/ options, UniqueNamer/*!*/ namer) { Contract.Requires(e != null); Contract.Requires(options != null); Contract.Requires(namer != null); Contract.Ensures(Contract.Result() != null); StringWriter sw = new StringWriter(); - SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser (sw, namer); + SimplifyLikeExprLineariser lin = new SimplifyLikeExprLineariser(sw, namer); lin.Linearise(e, options); return sw.ToString(); } @@ -141,60 +165,62 @@ Contract.Ensures(Contract.Result() != null); //////////////////////////////////////////////////////////////////////////////////////// [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(wr!=null); + void ObjectInvariant() { + Contract.Invariant(wr != null); Contract.Invariant(Namer != null); -} + } private readonly TextWriter/*!*/ wr; private SimplifyLikeOpLineariser OpLinObject = null; - private IVCExprOpVisitor/*!*/ OpLineariser { get {Contract.Ensures(Contract.Result>()!=null); - if (OpLinObject == null) - OpLinObject = new SimplifyLikeOpLineariser (this, wr); - return OpLinObject; - } } + private IVCExprOpVisitor/*!*/ OpLineariser { + get { + Contract.Ensures(Contract.Result>() != null); + if (OpLinObject == null) + OpLinObject = new SimplifyLikeOpLineariser(this, wr); + return OpLinObject; + } + } internal readonly UniqueNamer Namer; - public SimplifyLikeExprLineariser(TextWriter wr, UniqueNamer namer){ -Contract.Requires(namer != null); -Contract.Requires(wr != null); + public SimplifyLikeExprLineariser(TextWriter wr, UniqueNamer namer) { + Contract.Requires(namer != null); + Contract.Requires(wr != null); this.wr = wr; this.Namer = namer; } - public void Linearise(VCExpr expr, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(expr != null); + public void Linearise(VCExpr expr, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(expr != null); expr.Accept(this, options); } - public void LineariseAsTerm(VCExpr expr, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(expr != null); + public void LineariseAsTerm(VCExpr expr, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(expr != null); Linearise(expr, options.SetAsTerm(true)); } ///////////////////////////////////////////////////////////////////////////////////// - public static string MakeIdPrintable(string s){ -Contract.Requires(s != null); -Contract.Ensures(Contract.Result() != null); + public static string MakeIdPrintable(string s) { + Contract.Requires(s != null); + Contract.Ensures(Contract.Result() != null); // make sure that no keywords are used as identifiers - switch(s) { - case andName: - case orName: - case notName: - case impliesName: - case iffName: - case eqName: - case neqName: - case distinctName: - case TRUEName: - case FALSEName: - s = "nonkeyword_" + s; - break; + switch (s) { + case andName: + case orName: + case notName: + case impliesName: + case iffName: + case eqName: + case neqName: + case distinctName: + case TRUEName: + case FALSEName: + s = "nonkeyword_" + s; + break; } if (CommandLineOptions.Clo.BracketIdsInVC == 0) { @@ -242,29 +268,26 @@ Contract.Ensures(Contract.Result() != null); } } - private static void TypeToStringHelper(Type t, StringBuilder sb) - { + private static void TypeToStringHelper(Type t, StringBuilder sb) { Contract.Requires(t != null); TypeSynonymAnnotation syn = t as TypeSynonymAnnotation; if (syn != null) { TypeToStringHelper(syn.ExpandedType, sb); - } - else { + } else { if (t.IsMap) { MapType m = t.AsMap; sb.Append('['); for (int i = 0; i < m.MapArity; ++i) { - if (i != 0) sb.Append(','); + if (i != 0) + sb.Append(','); TypeToStringHelper(m.Arguments[i], sb); } sb.Append(']'); TypeToStringHelper(m.Result, sb); - } - else if (t.IsBool || t.IsInt || t.IsBv) { + } else if (t.IsBool || t.IsInt || t.IsBv) { sb.Append(TypeToString(t)); - } - else { + } else { System.IO.StringWriter buffer = new System.IO.StringWriter(); using (TokenTextWriter stream = new TokenTextWriter("", buffer, false)) { t.Emit(stream); @@ -276,8 +299,7 @@ Contract.Ensures(Contract.Result() != null); } - public static string TypeToString(Type t) - { + public static string TypeToString(Type t) { Contract.Requires(t != null); Contract.Ensures(Contract.Result() != null); @@ -294,39 +316,39 @@ Contract.Ensures(Contract.Result() != null); } } - public static string BvConcatOpName(VCExprNAry node){ -Contract.Requires(node != null); -Contract.Requires((node.Op is VCExprBvConcatOp)); -Contract.Ensures(Contract.Result() != null); + public static string BvConcatOpName(VCExprNAry node) { + Contract.Requires(node != null); + Contract.Requires((node.Op is VCExprBvConcatOp)); + Contract.Ensures(Contract.Result() != null); int bits1 = node[0].Type.BvBits; int bits2 = node[1].Type.BvBits; return "$bv" + (bits1 + bits2) + "_concat[" + bits1 + "." + bits2 + "]"; } - public static string BvExtractOpName(VCExprNAry node){ -Contract.Requires(node != null); -Contract.Requires(node.Op is VCExprBvExtractOp); -Contract.Ensures(Contract.Result() != null); + public static string BvExtractOpName(VCExprNAry node) { + Contract.Requires(node != null); + Contract.Requires(node.Op is VCExprBvExtractOp); + Contract.Ensures(Contract.Result() != null); VCExprBvExtractOp op = (VCExprBvExtractOp)node.Op; return "$bv" + node.Type.BvBits + "_extract" + op.Total + "[" + op.Start + ":" + op.End + "]"; } - public static string StoreOpName(VCExprNAry node){ -Contract.Requires(node != null); -Contract.Requires((node.Op is VCExprStoreOp)); -Contract.Ensures(Contract.Result() != null); + public static string StoreOpName(VCExprNAry node) { + Contract.Requires(node != null); + Contract.Requires((node.Op is VCExprStoreOp)); + Contract.Ensures(Contract.Result() != null); return "Store_" + TypeToString(node[0].Type); } - public static string SelectOpName(VCExprNAry node){ -Contract.Requires(node != null); -Contract.Requires((node.Op is VCExprSelectOp)); -Contract.Ensures(Contract.Result() != null); + public static string SelectOpName(VCExprNAry node) { + Contract.Requires(node != null); + Contract.Requires((node.Op is VCExprSelectOp)); + Contract.Ensures(Contract.Result() != null); return "Select_" + TypeToString(node[0].Type); } - - internal void WriteId(string s){ -Contract.Requires(s != null); + + internal void WriteId(string s) { + Contract.Requires(s != null); wr.Write(MakeIdPrintable(s)); } @@ -343,7 +365,7 @@ Contract.Requires(s != null); internal const string eqName = "EQ"; // equality internal const string neqName = "NEQ"; // inequality internal const string lessName = "<"; - internal const string greaterName = ">"; + internal const string greaterName = ">"; internal const string atmostName = "<="; internal const string atleastName = ">="; internal const string TRUEName = "TRUE"; // nullary predicate that is always true @@ -373,25 +395,25 @@ Contract.Requires(s != null); internal const string intDivName = "/"; internal const string intModName = "%"; - internal void AssertAsTerm(string x, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(x != null); + internal void AssertAsTerm(string x, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(x != null); if (!options.AsTerm) System.Diagnostics.Debug.Fail("One should never write " + x + " as a formula!"); } - internal void AssertAsFormula(string x, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(x != null); + internal void AssertAsFormula(string x, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(x != null); if (options.AsTerm) System.Diagnostics.Debug.Fail("One should never write " + x + " as a term!"); } ///////////////////////////////////////////////////////////////////////////////////// - public bool Visit(VCExprLiteral node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool Visit(VCExprLiteral node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); if (options.AsTerm) { if (node == VCExpressionGenerator.True) @@ -425,9 +447,9 @@ Contract.Requires(node != null); ///////////////////////////////////////////////////////////////////////////////////// - public bool Visit(VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool Visit(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); VCExprOp op = node.Op; Contract.Assert(op != null); @@ -438,11 +460,11 @@ Contract.Requires(node != null); wr.Write("({0}", op.Equals(VCExpressionGenerator.AndOp) ? andName : orName); - IEnumerator enumerator = new VCExprNAryUniformOpEnumerator (node); + IEnumerator enumerator = new VCExprNAryUniformOpEnumerator(node); Contract.Assert(enumerator != null); while (enumerator.MoveNext()) { VCExprNAry naryExpr = enumerator.Current as VCExprNAry; - if (naryExpr == null || !naryExpr.Op.Equals(op)) { + if (naryExpr == null || !naryExpr.Op.Equals(op)) { wr.Write(" "); Linearise(cce.NonNull((VCExpr)enumerator.Current), options); } @@ -458,24 +480,24 @@ Contract.Requires(node != null); ///////////////////////////////////////////////////////////////////////////////////// - public bool Visit(VCExprVar node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool Visit(VCExprVar node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); string printedName = Namer.GetName(node, node.Name); Contract.Assert(printedName != null); if (options.AsTerm || - // variables for formulas bound in a let-binding are never - // written as an equation + // variables for formulas bound in a let-binding are never + // written as an equation options.LetVariables.Contains(node) || - // if variables are properly typed, they cannot be written as - // equation either + // if variables are properly typed, they cannot be written as + // equation either options.UseTypes) { WriteId(printedName); } else { wr.Write("({0} ", eqName); WriteId(printedName); - wr.Write(" {0})", boolTrueName); + wr.Write(" {0})", boolTrueName); } return true; @@ -483,71 +505,71 @@ Contract.Requires(node != null); ///////////////////////////////////////////////////////////////////////////////////// - public bool Visit(VCExprQuantifier node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool Visit(VCExprQuantifier node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); AssertAsFormula(node.Quan.ToString(), options); Contract.Assert(node.TypeParameters.Count == 0); - Namer.PushScope(); try { + Namer.PushScope(); + try { - string kind = node.Quan == Quantifier.ALL ? "FORALL" : "EXISTS"; - wr.Write("({0} (", kind); + string kind = node.Quan == Quantifier.ALL ? "FORALL" : "EXISTS"; + wr.Write("({0} (", kind); - for (int i = 0; i < node.BoundVars.Count; i++) - { + for (int i = 0; i < node.BoundVars.Count; i++) { VCExprVar var = node.BoundVars[i]; - Contract.Assert(var != null); + Contract.Assert(var != null); string printedName = Namer.GetLocalName(var, var.Name); - Contract.Assert(printedName != null); + Contract.Assert(printedName != null); if (i != 0) wr.Write(" "); WriteId(printedName); if (options.UseTypes) wr.Write(" :TYPE {0}", TypeToString(var.Type)); } - wr.Write(") "); - - WriteTriggers(node.Triggers, options); - - if (options.QuantifierIds) { - // only needed for Z3 - VCQuantifierInfos infos = node.Infos; - Contract.Assert(infos != null); - if (infos.qid != null) { - wr.Write("(QID "); - wr.Write(infos.qid); - wr.Write(") "); - } - if (0 <= infos.uniqueId) { - wr.Write("(SKOLEMID "); - wr.Write(infos.uniqueId); - wr.Write(") "); + wr.Write(") "); + + WriteTriggers(node.Triggers, options); + + if (options.QuantifierIds) { + // only needed for Z3 + VCQuantifierInfos infos = node.Infos; + Contract.Assert(infos != null); + if (infos.qid != null) { + wr.Write("(QID "); + wr.Write(infos.qid); + wr.Write(") "); + } + if (0 <= infos.uniqueId) { + wr.Write("(SKOLEMID "); + wr.Write(infos.uniqueId); + wr.Write(") "); + } } - } - if (options.UseWeights) { - int weight = QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1); - if (weight != 1) { - wr.Write("(WEIGHT "); - wr.Write(weight); - wr.Write(") "); + if (options.UseWeights) { + int weight = QKeyValue.FindIntAttribute(node.Infos.attributes, "weight", 1); + if (weight != 1) { + wr.Write("(WEIGHT "); + wr.Write(weight); + wr.Write(") "); + } } - } - Linearise(node.Body, options); - wr.Write(")"); + Linearise(node.Body, options); + wr.Write(")"); - return true; + return true; } finally { Namer.PopScope(); } } - private void WriteTriggers(List/*!*/ triggers, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(cce.NonNullElements(triggers)); + private void WriteTriggers(List/*!*/ triggers, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(cce.NonNullElements(triggers)); // first, count how many neg/pos triggers there are int negTriggers = 0; int posTriggers = 0; @@ -568,7 +590,8 @@ Contract.Requires(cce.NonNullElements(triggers)); if (vcTrig.Exprs.Count > 1) { wr.Write(" (MPAT"); } - foreach (VCExpr e in vcTrig.Exprs) {Contract.Assert(e != null); + foreach (VCExpr e in vcTrig.Exprs) { + Contract.Assert(e != null); wr.Write(" "); LineariseAsTerm(e, options); } @@ -598,37 +621,39 @@ Contract.Requires(cce.NonNullElements(triggers)); ///////////////////////////////////////////////////////////////////////////////////// - public bool Visit(VCExprLet node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); - Namer.PushScope(); try { + public bool Visit(VCExprLet node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + Namer.PushScope(); + try { - wr.Write("(LET ("); + wr.Write("(LET ("); - LineariserOptions optionsWithVars = options.AddLetVariables(node.BoundVars); + LineariserOptions optionsWithVars = options.AddLetVariables(node.BoundVars); Contract.Assert(optionsWithVars != null); - - string s = "("; - foreach (VCExprLetBinding b in node) {Contract.Assert(b != null); - wr.Write(s); - string printedName = Namer.GetLocalName(b.V, b.V.Name); - - bool formula = b.V.Type.IsBool; - if (formula) - wr.Write("FORMULA "); - else - wr.Write("TERM "); - WriteId(printedName); - wr.Write(" "); - Linearise(b.E, optionsWithVars.SetAsTerm(!formula)); + + string s = "("; + foreach (VCExprLetBinding b in node) { + Contract.Assert(b != null); + wr.Write(s); + string printedName = Namer.GetLocalName(b.V, b.V.Name); + + bool formula = b.V.Type.IsBool; + if (formula) + wr.Write("FORMULA "); + else + wr.Write("TERM "); + WriteId(printedName); + wr.Write(" "); + Linearise(b.E, optionsWithVars.SetAsTerm(!formula)); + wr.Write(")"); + s = " ("; + } + wr.Write(") "); + Linearise(node.Body, optionsWithVars); wr.Write(")"); - s = " ("; - } - wr.Write(") "); - Linearise(node.Body, optionsWithVars); - wr.Write(")"); - return true; + return true; } finally { Namer.PopScope(); @@ -648,50 +673,50 @@ Contract.Requires(node != null); private readonly SimplifyLikeExprLineariser/*!*/ ExprLineariser; private readonly TextWriter/*!*/ wr; - public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser ExprLineariser, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(ExprLineariser != null); + public SimplifyLikeOpLineariser(SimplifyLikeExprLineariser ExprLineariser, TextWriter wr) { + Contract.Requires(wr != null); + Contract.Requires(ExprLineariser != null); this.ExprLineariser = ExprLineariser; this.wr = wr; } /////////////////////////////////////////////////////////////////////////////////// - private void WriteApplication(string op, IEnumerable/*!*/ args, LineariserOptions options, bool argsAsTerms){ -Contract.Requires(options != null); -Contract.Requires(op != null); -Contract.Requires(cce.NonNullElements(args)); + private void WriteApplication(string op, IEnumerable/*!*/ args, LineariserOptions options, bool argsAsTerms) { + Contract.Requires(options != null); + Contract.Requires(op != null); + Contract.Requires(cce.NonNullElements(args)); WriteApplication(op, op, args, options, argsAsTerms); } - private void WriteApplication(string op, IEnumerable/*!*/ args,LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(op != null); -Contract.Requires(cce.NonNullElements(args)); + private void WriteApplication(string op, IEnumerable/*!*/ args, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(op != null); + Contract.Requires(cce.NonNullElements(args)); WriteApplication(op, op, args, options, options.AsTerm); } - private void WriteTermApplication(string op, IEnumerable/*!*/ args,LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(op != null); -Contract.Requires(cce.NonNullElements(args)); + private void WriteTermApplication(string op, IEnumerable/*!*/ args, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(op != null); + Contract.Requires(cce.NonNullElements(args)); ExprLineariser.AssertAsTerm(op, options); WriteApplication(op, op, args, options, options.AsTerm); } - private void WriteApplication(string termOp, string predOp, IEnumerable/*!*/ args, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(predOp != null); -Contract.Requires(termOp != null); -Contract.Requires(cce.NonNullElements(args)); + private void WriteApplication(string termOp, string predOp, IEnumerable/*!*/ args, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(predOp != null); + Contract.Requires(termOp != null); + Contract.Requires(cce.NonNullElements(args)); WriteApplication(termOp, predOp, args, options, options.AsTerm); } - private void WriteApplication(string termOp, string predOp, IEnumerable/*!*/ args, LineariserOptions options, bool argsAsTerms){ -Contract.Requires(options != null); -Contract.Requires(predOp != null); -Contract.Requires(termOp != null); -Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the arguments? + private void WriteApplication(string termOp, string predOp, IEnumerable/*!*/ args, LineariserOptions options, bool argsAsTerms) { + Contract.Requires(options != null); + Contract.Requires(predOp != null); + Contract.Requires(termOp != null); + Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the arguments? wr.Write("({0}", options.AsTerm ? termOp : predOp); LineariserOptions newOptions = options.SetAsTerm(argsAsTerms); @@ -701,17 +726,17 @@ Contract.Requires(cce.NonNullElements(args));// change the AsTerm option for the wr.Write(" "); ExprLineariser.Linearise(e, newOptions); } - + wr.Write(")"); } // write an application that can only be a term. // if the expression is supposed to be printed as a formula, // it is turned into an equation (EQ (f args) |@true|) - private void WriteApplicationTermOnly(string termOp, IEnumerable/*!*/ args, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(termOp != null); -Contract.Requires(cce.NonNullElements(args)); + private void WriteApplicationTermOnly(string termOp, IEnumerable/*!*/ args, LineariserOptions options) { + Contract.Requires(options != null); + Contract.Requires(termOp != null); + Contract.Requires(cce.NonNullElements(args)); if (!options.AsTerm) // Write: (EQ (f args) |@true|) // where "args" are written as terms @@ -724,17 +749,17 @@ Contract.Requires(cce.NonNullElements(args)); } /////////////////////////////////////////////////////////////////////////////////// - - public bool VisitNotOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + + public bool VisitNotOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteApplication(boolNotName, notName, node, options); // arguments can be both terms and formulas return true; } - public bool VisitEqOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitEqOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); if (options.AsTerm) { // use equality on terms, also if the arguments have type bool WriteApplication(termEqName, node, options); @@ -753,9 +778,9 @@ Contract.Requires(node != null); return true; } - public bool VisitNeqOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitNeqOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); if (options.AsTerm) { // use equality on terms, also if the arguments have type bool WriteApplication(termNeqName, node, options); @@ -771,29 +796,29 @@ Contract.Requires(node != null); WriteApplication(neqName, node, options, true); } } - + return true; } - public bool VisitAndOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitAndOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); Contract.Assert(options.AsTerm); WriteApplication(boolAndName, andName, node, options); // arguments can be both terms and formulas return true; } - public bool VisitOrOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitOrOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); Contract.Assert(options.AsTerm); WriteApplication(boolOrName, orName, node, options); // arguments can be both terms and formulas return true; } - public bool VisitImpliesOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitImpliesOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); if (options.AsTerm) { wr.Write("({0} ({1} ", boolOrName, boolNotName); ExprLineariser.Linearise(node[0], options); @@ -807,16 +832,16 @@ Contract.Requires(node != null); ExprLineariser.Linearise(node[0], options); wr.Write("))"); } else { - WriteApplication(impliesName, node, options); + WriteApplication(impliesName, node, options); } return true; } - public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitDistinctOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); ExprLineariser.AssertAsFormula(distinctName, options); - + if (node.Length < 2) { ExprLineariser.Linearise(VCExpressionGenerator.True, options); } else { @@ -832,19 +857,20 @@ Contract.Requires(node != null); return true; } - public bool VisitLabelOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitLabelOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); VCExprLabelOp op = (VCExprLabelOp)node.Op; Contract.Assert(op != null); wr.Write(String.Format("({0} |{1}| ", op.pos ? "LBLPOS" : "LBLNEG", op.label)); - ExprLineariser.Linearise(node[0], options); wr.Write(")"); + ExprLineariser.Linearise(node[0], options); + wr.Write(")"); return true; } - public bool VisitSelectOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitSelectOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); wr.Write("(" + SelectOpName(node)); foreach (VCExpr/*!*/ e in node) { Contract.Assert(e != null); @@ -855,9 +881,9 @@ Contract.Requires(node != null); return true; } - public bool VisitStoreOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitStoreOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); wr.Write("(" + StoreOpName(node)); foreach (VCExpr e in node) { Contract.Assert(e != null); @@ -868,31 +894,31 @@ Contract.Requires(node != null); return true; } - public bool VisitBvOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitBvOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteTermApplication("$make_bv" + node.Type.BvBits, node, options); return true; } - public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitBvExtractOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteTermApplication(BvExtractOpName(node), node, options); return true; } - public bool VisitBvConcatOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitBvConcatOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteTermApplication(BvConcatOpName(node), node, options); return true; } - public bool VisitIfThenElseOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); - + public bool VisitIfThenElseOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); + wr.Write("(ITE "); ExprLineariser.Linearise(node[0], options.SetAsTerm(false)); wr.Write(" "); @@ -905,8 +931,8 @@ Contract.Requires(node != null); } public bool VisitCustomOp(VCExprNAry/*!*/ node, LineariserOptions/*!*/ options) { - Contract.Requires(node != null); - Contract.Requires(options != null); + //Contract.Requires(node != null); + //Contract.Requires(options != null); VCExprCustomOp op = (VCExprCustomOp)node.Op; wr.Write("({0}", op.Name); foreach (VCExpr arg in node) { @@ -917,9 +943,9 @@ Contract.Requires(node != null); return true; } - public bool VisitAddOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitAddOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); if (CommandLineOptions.Clo.ReflectAdd) { WriteTermApplication(intAddNameReflect, node, options); } else { @@ -928,79 +954,79 @@ Contract.Requires(node != null); return true; } - public bool VisitSubOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitSubOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteTermApplication(intSubName, node, options); return true; } - public bool VisitMulOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitMulOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteTermApplication(intMulName, node, options); return true; } - public bool VisitDivOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitDivOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteTermApplication(intDivName, node, options); return true; } - public bool VisitModOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitModOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteTermApplication(intModName, node, options); return true; } - public bool VisitLtOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitLtOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteApplication(termLessName, lessName, node, options, true); // arguments are always terms return true; } - public bool VisitLeOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitLeOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteApplication(termAtmostName, atmostName, node, options, true); // arguments are always terms return true; } - public bool VisitGtOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitGtOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteApplication(termGreaterName, greaterName, node, options, true); // arguments are always terms return true; } - public bool VisitGeOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitGeOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteApplication(termAtleastName, atleastName, node, options, true); // arguments are always terms return true; } - public bool VisitSubtypeOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitSubtypeOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteApplication(subtypeName, node, options, true); // arguments are always terms return true; } - public bool VisitSubtype3Op (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitSubtype3Op(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); WriteApplication(subtypeArgsName, node, options, true); // arguments are always terms return true; } - public bool VisitBoogieFunctionOp (VCExprNAry node, LineariserOptions options){ -Contract.Requires(options != null); -Contract.Requires(node != null); + public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) { + //Contract.Requires(options != null); + //Contract.Requires(node != null); VCExprBoogieFunctionOp op = (VCExprBoogieFunctionOp)node.Op; Contract.Assert(op != null); string funcName = op.Func.Name; @@ -1008,7 +1034,8 @@ Contract.Requires(node != null); string bvzName = op.Func.FindStringAttribute("external"); string printedName = ExprLineariser.Namer.GetName(op.Func, funcName); Contract.Assert(printedName != null); - if (bvzName != null) printedName = bvzName; + if (bvzName != null) + printedName = bvzName; if (options.UseTypes) { // we use term notation for arguments whose type is not bool, and @@ -1022,7 +1049,7 @@ Contract.Requires(node != null); wr.Write(" "); ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool)); } - + wr.Write(")"); } else { // arguments are always terms @@ -1031,7 +1058,7 @@ Contract.Requires(node != null); } return true; } - + } } diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index 7fc8073a..89c615ad 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -571,17 +571,22 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result() != null); return Quantify(Quantifier.ALL, typeParams, vars, triggers, infos, body); } - public VCExpr Forall(List/*!*/ vars, List/*!*/ triggers, string qid, VCExpr body){ -Contract.Requires(body != null);Contract.Requires(qid != null);Contract.Requires(cce.NonNullElements(triggers));Contract.Requires(cce.NonNullElements(vars)); -Contract.Ensures(Contract.Result() != null); -return Quantify(Quantifier.ALL, new List(), vars, - triggers, new VCQuantifierInfos (qid, -1, false, null), body); - } - public VCExpr Forall(List/*!*/ vars, List/*!*/ triggers, VCExpr body){ -Contract.Requires(body != null);Contract.Requires(cce.NonNullElements(triggers));Contract.Requires(cce.NonNullElements(vars)); -Contract.Ensures(Contract.Result() != null); -return Quantify(Quantifier.ALL, new List(), vars, - triggers, new VCQuantifierInfos (null, -1, false, null), body); + public VCExpr Forall(List/*!*/ vars, List/*!*/ triggers, string qid, VCExpr body) { + Contract.Requires(body != null); + Contract.Requires(qid != null); + Contract.Requires(cce.NonNullElements(triggers)); + Contract.Requires(cce.NonNullElements(vars)); + Contract.Ensures(Contract.Result() != null); + return Quantify(Quantifier.ALL, new List(), vars, + triggers, new VCQuantifierInfos(qid, -1, false, null), body); + } + public VCExpr Forall(List/*!*/ vars, List/*!*/ triggers, VCExpr body) { + Contract.Requires(body != null); + Contract.Requires(cce.NonNullElements(triggers)); + Contract.Requires(cce.NonNullElements(vars)); + Contract.Ensures(Contract.Result() != null); + return Quantify(Quantifier.ALL, new List(), vars, + triggers, new VCQuantifierInfos(null, -1, false, null), body); } public VCExpr Forall(VCExprVar var, VCTrigger trigger, VCExpr body) { Contract.Requires(body != null); @@ -599,13 +604,13 @@ return Quantify(Quantifier.ALL, new List(), vars, Contract.Ensures(Contract.Result() != null); return Quantify(Quantifier.EX, typeParams, vars, triggers, infos, body); } - public VCExpr Exists(List/*!*/ vars, List/*!*/ triggers, VCExpr body){ -Contract.Requires(body != null); + public VCExpr Exists(List/*!*/ vars, List/*!*/ triggers, VCExpr body) { + Contract.Requires(body != null); Contract.Requires(cce.NonNullElements(triggers)); Contract.Requires(cce.NonNullElements(vars)); -Contract.Ensures(Contract.Result() != null); - return Quantify(Quantifier.EX, new List (), vars, - triggers, new VCQuantifierInfos (null, -1, false, null), body); + Contract.Ensures(Contract.Result() != null); + return Quantify(Quantifier.EX, new List(), vars, + triggers, new VCQuantifierInfos(null, -1, false, null), body); } public VCExpr Exists(VCExprVar var, VCTrigger trigger, VCExpr body) { Contract.Requires(body != null); @@ -679,11 +684,11 @@ namespace Microsoft.Boogie.VCExprAST { return res; } - public static TypeSeq ToTypeSeq(VCExpr[] exprs, int startIndex){ -Contract.Requires(exprs != null); -Contract.Requires((Contract.ForAll(0,exprs.Length, i=> exprs[i] != null))); -Contract.Ensures(Contract.Result() != null); -TypeSeq/*!*/ res = new TypeSeq(); + public static TypeSeq ToTypeSeq(VCExpr[] exprs, int startIndex) { + Contract.Requires(exprs != null); + Contract.Requires((Contract.ForAll(0, exprs.Length, i => exprs[i] != null))); + Contract.Ensures(Contract.Result() != null); + TypeSeq/*!*/ res = new TypeSeq(); for (int i = startIndex; i < exprs.Length; ++i) res.Add(cce.NonNull(exprs[i]).Type); return res; @@ -760,14 +765,15 @@ TypeSeq/*!*/ res = new TypeSeq(); this.LitType = type; } public override Result Accept(IVCExprVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.Visit(this, arg); } } public class VCExprIntLit : VCExprLiteral { public readonly BigNum Val; - internal VCExprIntLit(BigNum val) :base(Type.Int){ + internal VCExprIntLit(BigNum val) + : base(Type.Int) { this.Val = val; } [Pure] @@ -899,7 +905,7 @@ TypeSeq/*!*/ res = new TypeSeq(); this.Op = op; } public override Result Accept(IVCExprVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.Visit(this, arg); } public Result Accept(IVCExprOpVisitor visitor, Arg arg) { @@ -944,7 +950,8 @@ TypeSeq/*!*/ res = new TypeSeq(); } } - internal VCExprNullary(VCExprOp op):base(op) { + internal VCExprNullary(VCExprOp op) + : base(op) { Contract.Requires(op != null); Contract.Requires(op.Arity == 0 && op.TypeParamArity == 0); this.ExprType = op.InferType(EMPTY_VCEXPR_LIST, EMPTY_TYPE_LIST); @@ -984,21 +991,23 @@ TypeSeq/*!*/ res = new TypeSeq(); } } - internal VCExprUnary(VCExprOp op, List arguments) :base(op){ + internal VCExprUnary(VCExprOp op, List arguments) + : base(op) { Contract.Requires(op != null); Contract.Requires(cce.NonNullElements(arguments)); Contract.Requires(op.Arity == 1 && op.TypeParamArity == 0 && arguments.Count == 1); - + this.Argument = arguments[0]; this.ExprType = op.InferType(arguments, EMPTY_TYPE_LIST); } - internal VCExprUnary(VCExprOp op, VCExpr argument) :base(op){ + internal VCExprUnary(VCExprOp op, VCExpr argument) + : base(op) { Contract.Requires(argument != null); Contract.Requires(op != null); Contract.Requires(op.Arity == 1 && op.TypeParamArity == 0); - + this.Argument = argument; // PR: could be optimised so that the argument does // not have to be boxed in an array each time @@ -1049,17 +1058,19 @@ TypeSeq/*!*/ res = new TypeSeq(); } } - internal VCExprBinary(VCExprOp op, List arguments) :base(op){ + internal VCExprBinary(VCExprOp op, List arguments) + : base(op) { Contract.Requires(op != null); Contract.Requires(cce.NonNullElements(arguments)); Contract.Requires(op.Arity == 2 && op.TypeParamArity == 0 && arguments.Count == 2); - + this.Argument0 = arguments[0]; this.Argument1 = arguments[1]; this.ExprType = op.InferType(arguments, EMPTY_TYPE_LIST); } - internal VCExprBinary(VCExprOp op, VCExpr argument0, VCExpr argument1) :base(op){ + internal VCExprBinary(VCExprOp op, VCExpr argument0, VCExpr argument1) + : base(op) { Contract.Requires(argument1 != null); Contract.Requires(argument0 != null); Contract.Requires(op != null); @@ -1109,7 +1120,8 @@ TypeSeq/*!*/ res = new TypeSeq(); } } - internal VCExprMultiAry(VCExprOp op, List arguments) :base(op){ + internal VCExprMultiAry(VCExprOp op, List arguments) + : base(op) { Contract.Requires(op != null); Contract.Requires(cce.NonNullElements(arguments)); //this(op, arguments, EMPTY_TYPE_LIST); @@ -1117,7 +1129,8 @@ TypeSeq/*!*/ res = new TypeSeq(); this.TypeArgumentsAttr = EMPTY_TYPE_LIST; this.ExprType = op.InferType(arguments, TypeArgumentsAttr); } - internal VCExprMultiAry(VCExprOp op, List arguments, List/*!*/ typeArguments):base(op){ + internal VCExprMultiAry(VCExprOp op, List arguments, List/*!*/ typeArguments) + : base(op) { Contract.Requires(op != null); Contract.Requires(cce.NonNullElements(typeArguments)); Contract.Requires(cce.NonNullElements(arguments)); @@ -1227,8 +1240,8 @@ TypeSeq/*!*/ res = new TypeSeq(); } } public override Type InferType(List args, List/*!*/ typeArgs) { - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(args)); + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); Contract.Ensures(Contract.Result() != null); return OpType; } @@ -1241,7 +1254,8 @@ TypeSeq/*!*/ res = new TypeSeq(); } public class VCExprDistinctOp : VCExprNAryOp { - internal VCExprDistinctOp(int arity) :base(arity, Type.Bool){ + internal VCExprDistinctOp(int arity) + : base(arity, Type.Bool) { } [Pure] [Reads(ReadsAttribute.Reads.Nothing)] @@ -1258,8 +1272,8 @@ TypeSeq/*!*/ res = new TypeSeq(); } public override Result Accept (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); - Contract.Requires(expr != null); + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); return visitor.VisitDistinctOp(expr, arg); } } @@ -1276,8 +1290,8 @@ TypeSeq/*!*/ res = new TypeSeq(); } } public override Type InferType(List args, List/*!*/ typeArgs) { - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(args)); + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); Contract.Ensures(Contract.Result() != null); return args[0].Type; } @@ -1312,8 +1326,8 @@ TypeSeq/*!*/ res = new TypeSeq(); } public override Result Accept (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); - Contract.Requires(expr != null); + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); return visitor.VisitLabelOp(expr, arg); } } @@ -1332,10 +1346,10 @@ TypeSeq/*!*/ res = new TypeSeq(); } } - public override Type InferType(List args, List/*!*/ typeArgs){ -Contract.Requires(cce.NonNullElements(typeArgs)); -Contract.Requires(cce.NonNullElements(args)); -Contract.Ensures(Contract.Result() != null); + public override Type InferType(List args, List/*!*/ typeArgs) { + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); + Contract.Ensures(Contract.Result() != null); MapType/*!*/ mapType = args[0].Type.AsMap; Contract.Assert(TypeParamArity == mapType.TypeParameters.Length); IDictionary/*!*/ subst = new Dictionary(); @@ -1366,8 +1380,8 @@ Contract.Ensures(Contract.Result() != null); } public override Result Accept (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); - Contract.Requires(expr != null); + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); return visitor.VisitSelectOp(expr, arg); } } @@ -1389,8 +1403,8 @@ Contract.Ensures(Contract.Result() != null); } public override Type InferType(List args, List/*!*/ typeArgs) { - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(args)); + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); Contract.Ensures(Contract.Result() != null); return args[0].Type; } @@ -1416,8 +1430,8 @@ Contract.Ensures(Contract.Result() != null); } public override Result Accept (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); - Contract.Requires(expr != null); + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); return visitor.VisitStoreOp(expr, arg); } } @@ -1434,8 +1448,8 @@ Contract.Ensures(Contract.Result() != null); } } public override Type InferType(List args, List/*!*/ typeArgs) { - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(args)); + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); Contract.Ensures(Contract.Result() != null); return args[1].Type; } @@ -1458,8 +1472,8 @@ Contract.Ensures(Contract.Result() != null); } public override Result Accept (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); - Contract.Requires(expr != null); + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); return visitor.VisitIfThenElseOp(expr, arg); } } @@ -1469,11 +1483,10 @@ Contract.Ensures(Contract.Result() != null); int arity; public readonly Type/*!*/ Type; [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(Name!=null); + void ObjectInvariant() { + Contract.Invariant(Name != null); Contract.Invariant(Type != null); -} + } public VCExprCustomOp(string/*!*/ name, int arity, Type/*!*/ type) { Contract.Requires(name != null); @@ -1482,7 +1495,8 @@ void ObjectInvariant() this.arity = arity; this.Type = type; } - [Pure][Reads(ReadsAttribute.Reads.Nothing)] + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] public override bool Equals(object that) { if (Object.ReferenceEquals(this, that)) return true; @@ -1491,15 +1505,26 @@ void ObjectInvariant() return false; return this.Name == t.Name && this.arity == t.arity && this.Type == t.Type; } - public override int Arity { get { return arity; } } - public override int TypeParamArity { get { return 0; } } - public override Type/*!*/ InferType(List/*!*/ args, List/*!*/ typeArgs) {Contract.Requires((cce.NonNullElements(args))); -Contract.Requires((cce.NonNullElements(typeArgs))); -Contract.Ensures(Contract.Result() != null); return Type; } + public override int Arity { + get { + return arity; + } + } + public override int TypeParamArity { + get { + return 0; + } + } + public override Type/*!*/ InferType(List/*!*/ args, List/*!*/ typeArgs) { + //Contract.Requires((cce.NonNullElements(args))); + //Contract.Requires((cce.NonNullElements(typeArgs))); + Contract.Ensures(Contract.Result() != null); + return Type; + } public override Result Accept (VCExprNAry/*!*/ expr, IVCExprOpVisitor/*!*/ visitor, Arg arg) { - Contract.Requires(expr != null); - Contract.Requires(visitor != null); + //Contract.Requires(expr != null); + //Contract.Requires(visitor != null); return visitor.VisitCustomOp(expr, arg); } } @@ -1521,8 +1546,8 @@ Contract.Ensures(Contract.Result() != null); return Type; } } } public override Type InferType(List args, List/*!*/ typeArgs) { - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(args)); + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); Contract.Ensures(Contract.Result() != null); return Type.GetBvType(Bits); } @@ -1546,8 +1571,8 @@ Contract.Ensures(Contract.Result() != null); return Type; } } public override Result Accept (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); - Contract.Requires(expr != null); + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); return visitor.VisitBvOp(expr, arg); } } @@ -1568,8 +1593,8 @@ Contract.Ensures(Contract.Result() != null); return Type; } } } public override Type InferType(List args, List/*!*/ typeArgs) { - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(args)); + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); Contract.Ensures(Contract.Result() != null); return Type.GetBvType(End - Start); } @@ -1598,8 +1623,8 @@ Contract.Ensures(Contract.Result() != null); return Type; } } public override Result Accept (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); - Contract.Requires(expr != null); + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); return visitor.VisitBvExtractOp(expr, arg); } } @@ -1619,8 +1644,8 @@ Contract.Ensures(Contract.Result() != null); return Type; } } } public override Type InferType(List args, List/*!*/ typeArgs) { - Contract.Requires(cce.NonNullElements(typeArgs)); - Contract.Requires(cce.NonNullElements(args)); + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); Contract.Ensures(Contract.Result() != null); return Type.GetBvType(args[0].Type.BvBits + args[1].Type.BvBits); } @@ -1648,8 +1673,8 @@ Contract.Ensures(Contract.Result() != null); return Type; } } public override Result Accept (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); - Contract.Requires(expr != null); + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); return visitor.VisitBvConcatOp(expr, arg); } } @@ -1675,10 +1700,10 @@ Contract.Ensures(Contract.Result() != null); return Type; } return Func.TypeParameters.Length; } } - public override Type InferType(List args, List/*!*/ typeArgs){ -Contract.Requires(cce.NonNullElements(typeArgs)); -Contract.Requires(cce.NonNullElements(args)); -Contract.Ensures(Contract.Result() != null); + public override Type InferType(List args, List/*!*/ typeArgs) { + //Contract.Requires(cce.NonNullElements(typeArgs)); + //Contract.Requires(cce.NonNullElements(args)); + Contract.Ensures(Contract.Result() != null); Contract.Assert(TypeParamArity == Func.TypeParameters.Length); if (TypeParamArity == 0) return cce.NonNull(Func.OutParams[0]).TypedIdent.Type; @@ -1710,8 +1735,8 @@ Contract.Ensures(Contract.Result() != null); } public override Result Accept (VCExprNAry expr, IVCExprOpVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); - Contract.Requires(expr != null); + //Contract.Requires(visitor != null); + //Contract.Requires(expr != null); return visitor.VisitBoogieFunctionOp(expr, arg); } } @@ -1745,7 +1770,7 @@ Contract.Ensures(Contract.Result() != null); this.VarType = type; } public override Result Accept(IVCExprVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.Visit(this, arg); } } @@ -1870,19 +1895,20 @@ Contract.Ensures(Contract.Result() != null); HelperFuns.PolyHash(123, 11, Triggers); } - internal VCExprQuantifier(Quantifier kind, List/*!*/ typeParams, List/*!*/ boundVars, List/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) :base(typeParams, boundVars, body){ + internal VCExprQuantifier(Quantifier kind, List/*!*/ typeParams, List/*!*/ boundVars, List/*!*/ triggers, VCQuantifierInfos infos, VCExpr body) + : base(typeParams, boundVars, body) { Contract.Requires(body != null); Contract.Requires(infos != null); Contract.Requires(cce.NonNullElements(triggers)); Contract.Requires(cce.NonNullElements(boundVars)); Contract.Requires(cce.NonNullElements(typeParams)); - + this.Quan = kind; this.Triggers = triggers; this.Infos = infos; } public override Result Accept(IVCExprVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.Visit(this, arg); } } @@ -1978,22 +2004,23 @@ Contract.Ensures(Contract.Result() != null); return Bindings.GetEnumerator(); } - private static List/*!*/ toSeq(List/*!*/ bindings){ -Contract.Requires(cce.NonNullElements(bindings)); -Contract.Ensures(cce.NonNullElements(Contract.Result>())); - List res = new List (); + private static List/*!*/ toSeq(List/*!*/ bindings) { + Contract.Requires(cce.NonNullElements(bindings)); + Contract.Ensures(cce.NonNullElements(Contract.Result>())); + List res = new List(); foreach (VCExprLetBinding/*!*/ b in bindings) res.Add(b.V); return res; } - internal VCExprLet(List/*!*/ bindings, VCExpr/*!*/ body) :base(new List(), toSeq(bindings), body){ + internal VCExprLet(List/*!*/ bindings, VCExpr/*!*/ body) + : base(new List(), toSeq(bindings), body) { Contract.Requires(cce.NonNullElements(bindings)); Contract.Requires(body != null); this.Bindings = bindings; } public override Result Accept(IVCExprVisitor visitor, Arg arg) { - Contract.Requires(visitor != null); + //Contract.Requires(visitor != null); return visitor.Visit(this, arg); } } diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs index c79c08db..adb3b27e 100644 --- a/Source/VCExpr/VCExprASTPrinter.cs +++ b/Source/VCExpr/VCExprASTPrinter.cs @@ -14,50 +14,44 @@ using Microsoft.Basetypes; // A simple visitor for turning a VCExpr into a human-readable string // (S-expr syntax) -namespace Microsoft.Boogie.VCExprAST -{ +namespace Microsoft.Boogie.VCExprAST { public class VCExprPrinter : IVCExprVisitor { private VCExprOpPrinter OpPrinterVar = null; - private VCExprOpPrinter/*!*/ OpPrinter { get {Contract.Ensures(Contract.Result() != null); + private VCExprOpPrinter/*!*/ OpPrinter { + get { + Contract.Ensures(Contract.Result() != null); - if (OpPrinterVar == null) - OpPrinterVar = new VCExprOpPrinter(this); - return OpPrinterVar; - } } + if (OpPrinterVar == null) + OpPrinterVar = new VCExprOpPrinter(this); + return OpPrinterVar; + } + } - public void Print(VCExpr expr, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(expr != null); + public void Print(VCExpr expr, TextWriter wr) { + Contract.Requires(wr != null); + Contract.Requires(expr != null); expr.Accept(this, wr); } - public bool Visit(VCExprLiteral node, TextWriter wr) - { - Contract.Requires(wr != null); - Contract.Requires(node != null); - if (node == VCExpressionGenerator.True) - { - wr.Write("true"); - } - else if (node == VCExpressionGenerator.False) - { - wr.Write("false"); - } - else if (node is VCExprIntLit) - { - wr.Write(((VCExprIntLit)node).Val); - } - else - { - Contract.Assert(false); throw new cce.UnreachableException(); - } - return true; + public bool Visit(VCExprLiteral node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + if (node == VCExpressionGenerator.True) { + wr.Write("true"); + } else if (node == VCExpressionGenerator.False) { + wr.Write("false"); + } else if (node is VCExprIntLit) { + wr.Write(((VCExprIntLit)node).Val); + } else { + Contract.Assert(false); + throw new cce.UnreachableException(); + } + return true; } - public bool Visit(VCExprNAry node, TextWriter wr) - { -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool Visit(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); VCExprOp/*!*/ op = node.Op; Contract.Assert(op != null); @@ -67,7 +61,7 @@ Contract.Requires(node != null); wr.Write("({0}", op.Equals(VCExpressionGenerator.AndOp) ? "And" : "Or"); - IEnumerator/*!*/ enumerator = new VCExprNAryUniformOpEnumerator (node); + IEnumerator/*!*/ enumerator = new VCExprNAryUniformOpEnumerator(node); Contract.Assert(enumerator != null); while (enumerator.MoveNext()) { VCExprNAry naryExpr = enumerator.Current as VCExprNAry; @@ -84,15 +78,15 @@ Contract.Requires(node != null); return node.Accept(OpPrinter, wr); } - public bool Visit(VCExprVar node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool Visit(VCExprVar node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); wr.Write(node.Name); return true; } - public bool Visit(VCExprQuantifier node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool Visit(VCExprQuantifier node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); string/*!*/ quan = node.Quan == Quantifier.ALL ? "Forall" : "Exists"; Contract.Assert(quan != null); @@ -101,8 +95,8 @@ Contract.Requires(node != null); if (node.TypeParameters.Count > 0) { wr.Write("<"); string/*!*/ sep = ""; - foreach(TypeVariable/*!*/ v in node.TypeParameters){ -Contract.Assert(v != null); + foreach (TypeVariable/*!*/ v in node.TypeParameters) { + Contract.Assert(v != null); wr.Write(sep); sep = ", "; wr.Write("{0}", v.Name); @@ -112,27 +106,27 @@ Contract.Assert(v != null); if (node.BoundVars.Count > 0) { string/*!*/ sep = ""; - foreach(VCExprVar/*!*/ v in node.BoundVars){ -Contract.Assert(v != null); + foreach (VCExprVar/*!*/ v in node.BoundVars) { + Contract.Assert(v != null); wr.Write(sep); sep = ", "; Print(v, wr); } wr.Write(" "); } - + wr.Write(":: "); if (node.Triggers.Count > 0) { wr.Write("{0} ", "{"); string/*!*/ sep = ""; - foreach(VCTrigger/*!*/ t in node.Triggers){ -Contract.Assert(t != null); + foreach (VCTrigger/*!*/ t in node.Triggers) { + Contract.Assert(t != null); wr.Write(sep); sep = ", "; string/*!*/ sep2 = ""; - foreach(VCExpr/*!*/ e in t.Exprs){ -Contract.Assert(e != null); + foreach (VCExpr/*!*/ e in t.Exprs) { + Contract.Assert(e != null); wr.Write(sep2); sep2 = "+"; Print(e, wr); @@ -145,14 +139,14 @@ Contract.Assert(e != null); wr.Write(")"); return true; } - public bool Visit(VCExprLet node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool Visit(VCExprLet node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); wr.Write("(Let "); string/*!*/ sep = ""; - foreach(VCExprLetBinding/*!*/ b in node){ -Contract.Assert(b != null); + foreach (VCExprLetBinding/*!*/ b in node) { + Contract.Assert(b != null); wr.Write(sep); sep = ", "; Print(b.V, wr); @@ -175,18 +169,18 @@ Contract.Assert(b != null); } - public VCExprOpPrinter(VCExprPrinter exprPrinter){ -Contract.Requires(exprPrinter != null); + public VCExprOpPrinter(VCExprPrinter exprPrinter) { + Contract.Requires(exprPrinter != null); this.ExprPrinter = exprPrinter; } - private bool PrintNAry(string op, VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); -Contract.Requires(op != null); + private bool PrintNAry(string op, VCExprNAry node, TextWriter wr) { + Contract.Requires(wr != null); + Contract.Requires(node != null); + Contract.Requires(op != null); wr.Write("({0}", op); - foreach(VCExpr/*!*/ arg in node){ -Contract.Assert(arg != null); + foreach (VCExpr/*!*/ arg in node) { + Contract.Assert(arg != null); wr.Write(" "); ExprPrinter.Print(arg, wr); } @@ -194,148 +188,150 @@ Contract.Assert(arg != null); return true; } - public bool VisitNotOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitNotOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("!", node, wr); } - public bool VisitEqOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitEqOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("==", node, wr); } - public bool VisitNeqOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitNeqOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("!=", node, wr); } - public bool VisitAndOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); - Contract.Assert(false); throw new cce.UnreachableException(); - } - public bool VisitOrOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); - Contract.Assert(false); throw new cce.UnreachableException(); - } - public bool VisitImpliesOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitAndOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + Contract.Assert(false); + throw new cce.UnreachableException(); + } + public bool VisitOrOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + Contract.Assert(false); + throw new cce.UnreachableException(); + } + public bool VisitImpliesOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("Implies", node, wr); } - public bool VisitDistinctOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitDistinctOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("Distinct", node, wr); } - public bool VisitLabelOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); -VCExprLabelOp/*!*/ op = (VCExprLabelOp)node.Op; -Contract.Assert(op != null); + public bool VisitLabelOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + VCExprLabelOp/*!*/ op = (VCExprLabelOp)node.Op; + Contract.Assert(op != null); return PrintNAry("Label " + op.label, node, wr); } - public bool VisitSelectOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitSelectOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("Select", node, wr); } - public bool VisitStoreOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitStoreOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("Store", node, wr); } - public bool VisitBvOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitBvOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("Bv", node, wr); } - public bool VisitBvExtractOp(VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitBvExtractOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("BvExtract", node, wr); } - public bool VisitBvConcatOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitBvConcatOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("BvConcat", node, wr); } - public bool VisitIfThenElseOp(VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitIfThenElseOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("if-then-else", node, wr); } public bool VisitCustomOp(VCExprNAry/*!*/ node, TextWriter/*!*/ wr) { - Contract.Requires(node!=null); - Contract.Requires(wr != null); + //Contract.Requires(node!=null); + //Contract.Requires(wr != null); VCExprCustomOp op = (VCExprCustomOp)node.Op; return PrintNAry(op.Name, node, wr); } - public bool VisitAddOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitAddOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); if (CommandLineOptions.Clo.ReflectAdd) { return PrintNAry("Reflect$Add", node, wr); } else { return PrintNAry("+", node, wr); } } - public bool VisitSubOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitSubOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("-", node, wr); } - public bool VisitMulOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitMulOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("*", node, wr); } - public bool VisitDivOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitDivOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("/", node, wr); } - public bool VisitModOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitModOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("%", node, wr); } - public bool VisitLtOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitLtOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("<", node, wr); } - public bool VisitLeOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitLeOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("<=", node, wr); } - public bool VisitGtOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitGtOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry(">", node, wr); } - public bool VisitGeOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitGeOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry(">=", node, wr); } - public bool VisitSubtypeOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitSubtypeOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("<:", node, wr); } - public bool VisitSubtype3Op (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); + public bool VisitSubtype3Op(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); return PrintNAry("<::", node, wr); } - public bool VisitBoogieFunctionOp (VCExprNAry node, TextWriter wr){ -Contract.Requires(wr != null); -Contract.Requires(node != null); -VCExprBoogieFunctionOp/*!*/ op = (VCExprBoogieFunctionOp)node.Op; -Contract.Assert(op != null); + public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) { + //Contract.Requires(wr != null); + //Contract.Requires(node != null); + VCExprBoogieFunctionOp/*!*/ op = (VCExprBoogieFunctionOp)node.Op; + Contract.Assert(op != null); return PrintNAry(op.Func.Name, node, wr); } } 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 diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs index d5505dd4..d30c93e9 100644 --- a/Source/VCGeneration/Check.cs +++ b/Source/VCGeneration/Check.cs @@ -14,26 +14,23 @@ using Microsoft.Boogie.AbstractInterpretation; using Microsoft.Boogie.VCExprAST; using Microsoft.Basetypes; -namespace Microsoft.Boogie -{ +namespace Microsoft.Boogie { /// /// Interface to the theorem prover specialized to Boogie. /// /// This class creates the appropriate background axioms. There /// should be one instance per BoogiePL program. /// - public sealed class Checker - { + public sealed class Checker { [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(gen!=null); + void ObjectInvariant() { + Contract.Invariant(gen != null); Contract.Invariant(thmProver != null); Contract.Invariant(ProverDone != null); -} + } private readonly VCExpressionGenerator gen; - + private ProverInterface thmProver; private CommandLineOptions.BvHandling bitvectors; private int timeout; @@ -50,34 +47,37 @@ void ObjectInvariant() public readonly AutoResetEvent ProverDone = new AutoResetEvent(false); - private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) - { - if (impl == null) return CommandLineOptions.Clo.Bitvectors; + private static CommandLineOptions.BvHandling BvHandlingForImpl(Implementation impl) { + if (impl == null) + return CommandLineOptions.Clo.Bitvectors; bool force_int = false; bool force_native = false; cce.NonNull(impl.Proc).CheckBooleanAttribute("forceBvInt", ref force_int); impl.Proc.CheckBooleanAttribute("forceBvZ3Native", ref force_native); impl.CheckBooleanAttribute("forceBvInt", ref force_int); impl.CheckBooleanAttribute("forceBvZ3Native", ref force_native); - if (force_native) return CommandLineOptions.BvHandling.Z3Native; - if (force_int) return CommandLineOptions.BvHandling.ToInt; + if (force_native) + return CommandLineOptions.BvHandling.Z3Native; + if (force_int) + return CommandLineOptions.BvHandling.ToInt; return CommandLineOptions.Clo.Bitvectors; } - public bool WillingToHandle(Implementation impl, int timeout) - { + public bool WillingToHandle(Implementation impl, int timeout) { return !closed && timeout == this.timeout && bitvectors == BvHandlingForImpl(impl); } - public VCExpressionGenerator VCExprGen - { - get {Contract.Ensures(Contract.Result() != null); - return this.gen; } + public VCExpressionGenerator VCExprGen { + get { + Contract.Ensures(Contract.Result() != null); + return this.gen; + } } - public ProverInterface TheoremProver - { - get {Contract.Ensures(Contract.Result() != null); - return this.thmProver; } + public ProverInterface TheoremProver { + get { + Contract.Ensures(Contract.Result() != null); + return this.thmProver; + } } ///////////////////////////////////////////////////////////////////////////////// @@ -85,10 +85,9 @@ void ObjectInvariant() private struct ContextCacheKey { [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(program!=null); -} + void ObjectInvariant() { + Contract.Invariant(program != null); + } public readonly Program program; public readonly CommandLineOptions.BvHandling bitvectors; @@ -100,7 +99,8 @@ void ObjectInvariant() this.bitvectors = bitvectors; } - [Pure][Reads(ReadsAttribute.Reads.Nothing)] + [Pure] + [Reads(ReadsAttribute.Reads.Nothing)] public override bool Equals(object that) { if (that is ContextCacheKey) { ContextCacheKey thatKey = (ContextCacheKey)that; @@ -121,8 +121,7 @@ void ObjectInvariant() /// /// Constructor. Initialize a checker with the program and log file. /// - public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout) - { + public Checker(VC.ConditionGeneration vcgen, Program prog, string/*?*/ logFilePath, bool appendLogFile, Implementation impl, int timeout) { Contract.Requires(vcgen != null); Contract.Requires(prog != null); this.bitvectors = BvHandlingForImpl(impl); @@ -143,14 +142,14 @@ void ObjectInvariant() } options.BitVectors = this.bitvectors; - ContextCacheKey key = new ContextCacheKey (prog, this.bitvectors); + ContextCacheKey key = new ContextCacheKey(prog, this.bitvectors); ProverContext ctx; ProverInterface prover; if (vcgen.CheckerCommonState == null) { - vcgen.CheckerCommonState = new Dictionary (); + vcgen.CheckerCommonState = new Dictionary(); } - IDictionary/*!>!*/ cachedContexts = (IDictionary) vcgen.CheckerCommonState; + IDictionary/*!>!*/ cachedContexts = (IDictionary)vcgen.CheckerCommonState; if (cachedContexts.TryGetValue(key, out ctx)) { ctx = (ProverContext)cce.NonNull(ctx).Clone(); @@ -203,7 +202,7 @@ void ObjectInvariant() CommandLineOptions.Clo.TheProverFactory.SpawnProver(options, ctx); cachedContexts.Add(key, cce.NonNull((ProverContext)ctx.Clone())); } - + this.thmProver = prover; this.gen = prover.VCExprGen; @@ -214,8 +213,7 @@ void ObjectInvariant() /// /// Clean-up. /// - public void Close() - { + public void Close() { this.closed = true; thmProver.Close(); } @@ -224,35 +222,37 @@ void ObjectInvariant() /// Push a Verification Condition as an Axiom /// (Required for Doomed Program Point detection) /// - public void PushVCExpr(VCExpr vc) - { + public void PushVCExpr(VCExpr vc) { Contract.Requires(vc != null); //thmProver.Context.AddAxiom(vc); thmProver.PushVCExpression(vc); } - public bool IsBusy - { - get { return busy; } + public bool IsBusy { + get { + return busy; + } } - public bool Closed - { - get { return closed; } + public bool Closed { + get { + return closed; + } } - public bool HasOutput - { - get { return hasOutput; } + public bool HasOutput { + get { + return hasOutput; + } } - public TimeSpan ProverRunTime - { - get { return proverRunTime; } + public TimeSpan ProverRunTime { + get { + return proverRunTime; + } } - private void WaitForOutput(object dummy) - { + private void WaitForOutput(object dummy) { try { outcome = thmProver.CheckOutcome(cce.NonNull(handler)); } catch (UnexpectedProverOutputException e) { @@ -277,20 +277,20 @@ void ObjectInvariant() break; } - Contract.Assert( busy); + Contract.Assert(busy); hasOutput = true; proverRunTime = DateTime.Now - proverStart; ProverDone.Set(); } - - public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler){ + + public void BeginCheck(string descriptiveName, VCExpr vc, ProverInterface.ErrorHandler handler) { Contract.Requires(descriptiveName != null); Contract.Requires(vc != null); Contract.Requires(handler != null); - - Contract.Requires( !IsBusy); - Contract.Assert( !busy); + + Contract.Requires(!IsBusy); + Contract.Assert(!busy); busy = true; hasOutput = false; outputExn = null; @@ -303,11 +303,11 @@ void ObjectInvariant() ThreadPool.QueueUserWorkItem(WaitForOutput); } - public ProverInterface.Outcome ReadOutcome(){ - - Contract.Requires( IsBusy); - Contract.Requires( HasOutput); - Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true); + public ProverInterface.Outcome ReadOutcome() { + + Contract.Requires(IsBusy); + Contract.Requires(HasOutput); + Contract.EnsuresOnThrow(true); hasOutput = false; busy = false; @@ -318,7 +318,7 @@ void ObjectInvariant() return outcome; } } - + // ----------------------------------------------------------------------------------------------- // ----------------------------------------------------------------------------------------------- // ----------------------------------------------------------------------------------------------- @@ -331,21 +331,20 @@ void ObjectInvariant() public Dictionary>/*!*/>/*!*/ definedFunctions; [ContractInvariantMethod] -void ObjectInvariant() -{ - Contract.Invariant(cce.NonNullElements(identifierToPartition)); + void ObjectInvariant() { + Contract.Invariant(cce.NonNullElements(identifierToPartition)); Contract.Invariant(partitionToIdentifiers != null); - Contract.Invariant(Contract.ForAll(partitionToIdentifiers,i=>cce.NonNullElements(i))); + Contract.Invariant(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i))); Contract.Invariant(partitionToValue != null); Contract.Invariant(valueToPartition != null); Contract.Invariant(cce.NonNullElements(definedFunctions)); -} + } public ErrorModel(Dictionary identifierToPartition, List> partitionToIdentifiers, List partitionToValue, Dictionary valueToPartition, Dictionary>> definedFunctions) { Contract.Requires(cce.NonNullElements(identifierToPartition)); Contract.Requires(partitionToIdentifiers != null); - Contract.Requires(Contract.ForAll(partitionToIdentifiers,i=>cce.NonNullElements(i))); + Contract.Requires(Contract.ForAll(partitionToIdentifiers, i => cce.NonNullElements(i))); Contract.Requires(partitionToValue != null); Contract.Requires(valueToPartition != null); Contract.Requires(cce.NonNullElements(definedFunctions)); @@ -356,39 +355,41 @@ void ObjectInvariant() this.definedFunctions = definedFunctions; } - public virtual void Print(TextWriter writer) {Contract.Requires(writer != null); } - - public int LookupPartitionValue(int partition) - { - BigNum bignum = (BigNum) cce.NonNull(partitionToValue)[partition]; + public virtual void Print(TextWriter writer) { + Contract.Requires(writer != null); + } + + public int LookupPartitionValue(int partition) { + BigNum bignum = (BigNum)cce.NonNull(partitionToValue)[partition]; return bignum.ToInt; } - - public int LookupControlFlowFunctionAt(int cfc, int id) - { + + public int LookupControlFlowFunctionAt(int cfc, int id) { List> tuples = this.definedFunctions["ControlFlow"]; Contract.Assert(tuples != null); - foreach (List tuple in tuples) - { - if (tuple == null) continue; - if (tuple.Count != 3) continue; + foreach (List tuple in tuples) { + if (tuple == null) + continue; + if (tuple.Count != 3) + continue; if (LookupPartitionValue(tuple[0]) == cfc && LookupPartitionValue(tuple[1]) == id) return LookupPartitionValue(tuple[2]); } - Contract.Assert(false);throw new cce.UnreachableException(); + Contract.Assert(false); + throw new cce.UnreachableException(); return 0; } - + private string LookupSkolemConstant(string name) { Contract.Requires(name != null); Contract.Ensures(Contract.Result() != null); - foreach (string functionName in identifierToPartition.Keys) - { + foreach (string functionName in identifierToPartition.Keys) { Contract.Assert(functionName != null); int index = functionName.LastIndexOf("!"); - if (index == -1) continue; + if (index == -1) + continue; string newFunctionName = cce.NonNull(functionName.Remove(index)); if (newFunctionName.Equals(name)) return functionName; @@ -399,67 +400,62 @@ void ObjectInvariant() Contract.Requires(name != null); Contract.Ensures(Contract.Result() != null); - foreach (string functionName in definedFunctions.Keys) - { + foreach (string functionName in definedFunctions.Keys) { Contract.Assert(functionName != null); int index = functionName.LastIndexOf("!"); - if (index == -1) continue; + if (index == -1) + continue; string newFunctionName = cce.NonNull(functionName.Remove(index)); if (newFunctionName.Equals(name)) return functionName; } return ""; } - public int LookupSkolemFunctionAt(string functionName, List values) - - { - Contract.Requires(functionName!= null); + public int LookupSkolemFunctionAt(string functionName, List values) { + Contract.Requires(functionName != null); Contract.Requires(values != null); string actualFunctionName = LookupSkolemFunction(functionName); Contract.Assert(actualFunctionName != null); - if (actualFunctionName.Equals("")) - { + if (actualFunctionName.Equals("")) { // The skolem function is actually a skolem constant actualFunctionName = LookupSkolemConstant(functionName); - Contract.Assert( !actualFunctionName.Equals("")); + Contract.Assert(!actualFunctionName.Equals("")); return identifierToPartition[actualFunctionName]; } List> tuples = this.definedFunctions[actualFunctionName]; - Contract.Assert( tuples.Count > 0); + Contract.Assert(tuples.Count > 0); // the last tuple is a dummy tuple - for (int n = 0; n < tuples.Count - 1; n++) - { + for (int n = 0; n < tuples.Count - 1; n++) { List tuple = cce.NonNull(tuples[n]); - Contract.Assert( tuple.Count - 1 <= values.Count); - for (int i = 0, j = 0; i < values.Count; i++) - { + Contract.Assert(tuple.Count - 1 <= values.Count); + for (int i = 0, j = 0; i < values.Count; i++) { if (values[i] == tuple[j]) { // succeeded in matching tuple[j] j++; - if (j == tuple.Count-1) return tuple[tuple.Count - 1]; + if (j == tuple.Count - 1) + return tuple[tuple.Count - 1]; } } } - Contract.Assert(false);throw new cce.UnreachableException(); + Contract.Assert(false); + throw new cce.UnreachableException(); return 0; } - - public List/*!>!*/ PartitionsToValues(List args) - { + + public List/*!>!*/ PartitionsToValues(List args) { Contract.Requires(args != null); Contract.Ensures(cce.NonNullElements(Contract.Result>())); List vals = new List(); - foreach(int i in args) - { + foreach (int i in args) { object o = cce.NonNull(partitionToValue[i]); if (o is bool) { vals.Add(o); } else if (o is BigNum) { vals.Add(o); } else if (o is List>) { - List> array = (List>) o; + List> array = (List>)o; List> arrayVal = new List>(); foreach (List tuple in array) { Contract.Assert(tuple != null); @@ -472,30 +468,33 @@ void ObjectInvariant() } vals.Add(arrayVal); } else { - Contract.Assert(false);throw new cce.UnreachableException(); + Contract.Assert(false); + throw new cce.UnreachableException(); } } return vals; } } - public abstract class ProverInterface - { - public enum Outcome { Valid, Invalid, TimeOut, OutOfMemory, Undetermined } - public class ErrorHandler - { - public virtual void OnModel(IList/*!>!*/ labels, ErrorModel errModel) - { + public abstract class ProverInterface { + public enum Outcome { + Valid, + Invalid, + TimeOut, + OutOfMemory, + Undetermined + } + public class ErrorHandler { + public virtual void OnModel(IList/*!>!*/ labels, ErrorModel errModel) { Contract.Requires(cce.NonNullElements(labels)); } - public virtual void OnResourceExceeded(string message) - { - Contract.Requires(message!=null); + public virtual void OnResourceExceeded(string message) { + Contract.Requires(message != null); } public virtual void OnProverWarning(string message) - //modifies Console.Out.*, Console.Error.*; + //modifies Console.Out.*, Console.Error.*; { Contract.Requires(message != null); switch (CommandLineOptions.Clo.PrintProverWarnings) { @@ -508,13 +507,13 @@ void ObjectInvariant() Console.Error.WriteLine("Prover warning: " + message); break; default: - Contract.Assume( false);throw new cce.UnreachableException(); // unexpected case + Contract.Assume(false); + throw new cce.UnreachableException(); // unexpected case } } - public virtual Absy Label2Absy(string label) - { + public virtual Absy Label2Absy(string label) { Contract.Requires(label != null); Contract.Ensures(Contract.Result() != null); @@ -529,26 +528,40 @@ void ObjectInvariant() } public virtual void Close() { } - + /// /// MSchaef: Allows to Push a VCExpression as Axiom on the prover stack (beta) /// for now it is only implemented by ProcessTheoremProver and still requires some /// testing /// - public virtual void PushVCExpression(VCExpr vc) {Contract.Requires(vc != null);} - public virtual string VCExpressionToString(VCExpr vc) {Contract.Requires(vc != null);Contract.Ensures(Contract.Result() != null); return ""; } - public virtual void Pop() - {Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);} - public virtual int NumAxiomsPushed() - { return 0; } - public virtual int FlushAxiomsToTheoremProver() - { Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);return 0; } - - - public abstract ProverContext Context { get; } -public abstract VCExpressionGenerator VCExprGen { get; } + public virtual void PushVCExpression(VCExpr vc) { + Contract.Requires(vc != null); + } + public virtual string VCExpressionToString(VCExpr vc) { + Contract.Requires(vc != null); + Contract.Ensures(Contract.Result() != null); + return ""; + } + public virtual void Pop() { + Contract.EnsuresOnThrow(true); + } + public virtual int NumAxiomsPushed() { + return 0; + } + public virtual int FlushAxiomsToTheoremProver() { + Contract.EnsuresOnThrow(true); + return 0; + } + + + public abstract ProverContext Context { + get; + } + public abstract VCExpressionGenerator VCExprGen { + get; + } } - public class ProverInterfaceContracts:ProverInterface{ + public class ProverInterfaceContracts : ProverInterface { public override ProverContext Context { get { Contract.Ensures(Contract.Result() != null); @@ -563,32 +576,34 @@ public abstract VCExpressionGenerator VCExprGen { get; } throw new NotImplementedException(); } } - public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler){/*Contract.Requires(descriptiveName != null);*/ Contract.Requires(vc != null);Contract.Requires(handler != null);throw new NotImplementedException();} + public override void BeginCheck(string descriptiveName, VCExpr vc, ErrorHandler handler) {/*Contract.Requires(descriptiveName != null);*/ + //Contract.Requires(vc != null); + //Contract.Requires(handler != null); + throw new NotImplementedException(); + } [NoDefaultContract] - public override Outcome CheckOutcome(ErrorHandler handler){ - //Contract.Requires(handler != null); - Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true); - throw new NotImplementedException();} + public override Outcome CheckOutcome(ErrorHandler handler) { + //Contract.Requires(handler != null); + Contract.EnsuresOnThrow(true); + throw new NotImplementedException(); + } } - - public class ProverException : Exception - { - public ProverException(string s) : base(s) - { + + public class ProverException : Exception { + public ProverException(string s) + : base(s) { } } - public class UnexpectedProverOutputException : ProverException, Microsoft.Contracts.ICheckedException - { - public UnexpectedProverOutputException(string s) : base(s) - { + public class UnexpectedProverOutputException : ProverException, Microsoft.Contracts.ICheckedException { + public UnexpectedProverOutputException(string s) + : base(s) { } } - public class ProverDiedException : UnexpectedProverOutputException - { - public ProverDiedException() : base("Prover died with no further output, perhaps it ran out of memory or was killed.") - { + public class ProverDiedException : UnexpectedProverOutputException { + public ProverDiedException() + : base("Prover died with no further output, perhaps it ran out of memory or was killed.") { } } } diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 209248ed..90ed5d5c 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -722,12 +722,12 @@ namespace VC { public readonly List/*!>!*/ examples = new List(); public override void OnCounterexample(Counterexample ce, string/*?*/ reason) { - Contract.Requires(ce != null); + //Contract.Requires(ce != null); examples.Add(ce); } public override void OnUnreachableCode(Implementation impl) { - Contract.Requires(impl != null); + //Contract.Requires(impl != null); System.Console.WriteLine("found unreachable code:"); EmitImpl(impl, false); // TODO report error about next to last in seq diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/VCGeneration/DoomErrorHandler.cs index 0bcf15f8..12936c1f 100644 --- a/Source/VCGeneration/DoomErrorHandler.cs +++ b/Source/VCGeneration/DoomErrorHandler.cs @@ -41,7 +41,7 @@ void ObjectInvariant() } public override Absy Label2Absy(string label) { - Contract.Requires(label != null); + //Contract.Requires(label != null); Contract.Ensures(Contract.Result() != null); int id = int.Parse(label); @@ -49,7 +49,7 @@ void ObjectInvariant() } public override void OnProverWarning(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); this.callback.OnWarning(msg); } @@ -75,7 +75,7 @@ void ObjectInvariant() } public override void OnModel(IList/*!>!*/ labels, ErrorModel errModel) { - Contract.Requires(labels != null); + //Contract.Requires(labels != null); m_CurrentTrace.Clear(); //Console.Write("Used Blocks: "); diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 9ca934b2..a053a153 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -780,7 +780,7 @@ namespace VC { } public override Absy Label2Absy(string label) { - Contract.Requires(label != null); + //Contract.Requires(label != null); Contract.Ensures(Contract.Result() != null); int id = int.Parse(label); @@ -788,7 +788,7 @@ namespace VC { } public override void OnProverWarning(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); this.callback.OnWarning(msg); } } @@ -1721,9 +1721,9 @@ namespace VC { } public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback){ - Contract.Requires(impl != null); - Contract.Requires(program != null); - Contract.Requires(callback != null); + //Contract.Requires(impl != null); + //Contract.Requires(program != null); + //Contract.Requires(callback != null); Contract.EnsuresOnThrow(true); if (impl.SkipVerification) { return Outcome.Inconclusive; // not sure about this one @@ -1888,9 +1888,9 @@ namespace VC { } public override Outcome StratifiedVerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback){ - Contract.Requires(impl != null); - Contract.Requires(program != null); - Contract.Requires(callback != null); + //Contract.Requires(impl != null); + //Contract.Requires(program != null); + //Contract.Requires(callback != null); Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true); // This flag control the nature of queries made by StratifiedVerifyImplementation // true: incremental search; false: in-place inlining @@ -2738,8 +2738,8 @@ namespace VC { bool changed, bool arg) { - Contract.Requires(originalNode != null); - Contract.Requires(cce.NonNullElements(newSubExprs)); + //Contract.Requires(originalNode != null); + //Contract.Requires(cce.NonNullElements(newSubExprs)); Contract.Ensures(Contract.Result() != null); VCExpr ret; @@ -2821,7 +2821,7 @@ namespace VC { bool changed, bool arg) { - Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null); + //Contract.Requires(originalNode != null);Contract.Requires(newSubExprs != null); Contract.Ensures(Contract.Result() != null); VCExpr ret; @@ -2911,7 +2911,7 @@ namespace VC { } public override void OnModel(IList/*!*/ labels, ErrorModel errModel) { - Contract.Requires(cce.NonNullElements(labels)); + //Contract.Requires(cce.NonNullElements(labels)); if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) { errModel.Print(ErrorReporter.ModelWriter); ErrorReporter.ModelWriter.Flush(); @@ -2955,7 +2955,7 @@ namespace VC { } public override Absy Label2Absy(string label) { - Contract.Requires(label != null); + //Contract.Requires(label != null); Contract.Ensures(Contract.Result() != null); int id = int.Parse(label); @@ -2963,12 +2963,12 @@ namespace VC { } public override void OnResourceExceeded(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); resourceExceededMessage = msg; } public override void OnProverWarning(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); callback.OnWarning(msg); } } @@ -2996,7 +2996,7 @@ namespace VC { } public override void OnModel(IList/*!*/ labels, ErrorModel errModel) { - Contract.Requires(cce.NonNullElements(labels)); + //Contract.Requires(cce.NonNullElements(labels)); // We ignore the error model here for enhanced error message purposes. // It is only printed to the command line. if (CommandLineOptions.Clo.PrintErrorModel >= 1 && errModel != null) { @@ -3092,7 +3092,7 @@ namespace VC { } public override void OnModel(IList/*!*/ labels, ErrorModel errModel) { - Contract.Requires(cce.NonNullElements(labels)); + //Contract.Requires(cce.NonNullElements(labels)); if (underapproximationMode) { if (errModel == null) return; @@ -3266,7 +3266,7 @@ namespace VC { } public override Absy Label2Absy(string label) { - Contract.Requires(label != null); + //Contract.Requires(label != null); Contract.Ensures(Contract.Result() != null); int id = int.Parse(label); @@ -3285,12 +3285,12 @@ namespace VC { } public override void OnResourceExceeded(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); //resourceExceededMessage = msg; } public override void OnProverWarning(string msg) { - Contract.Requires(msg != null); + //Contract.Requires(msg != null); callback.OnWarning(msg); } } diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs index 12543cd5..c1547009 100644 --- a/Source/VCGeneration/VCDoomed.cs +++ b/Source/VCGeneration/VCDoomed.cs @@ -283,9 +283,9 @@ namespace VC { /// /// public override Outcome VerifyImplementation(Implementation impl, Program program, VerifierCallback callback) { - Contract.Requires(impl != null); - Contract.Requires(program != null); - Contract.Requires(callback != null); + //Contract.Requires(impl != null); + //Contract.Requires(program != null); + //Contract.Requires(callback != null); Contract.EnsuresOnThrow(true); UseItAsDebugger = CommandLineOptions.Clo.useDoomDebug; -- cgit v1.2.3