From 7681e01e7711a19e3a1c8588b294cba0925cb179 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Fri, 18 Oct 2024 17:32:01 +0200 Subject: [PATCH] Extract match and if verification (#5843) ### Description - Extract match and if verification ### How has this been tested? Pure refactoring, no additional tests needed By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt). --- .../Verifier/BoogieGenerator.BoogieFactory.cs | 88 ++--- .../Verifier/BoogieGenerator.Decreases.cs | 16 +- .../BoogieGenerator.DefiniteAssignment.cs | 2 +- .../BoogieGenerator.ExpressionTranslator.cs | 14 +- .../BoogieGenerator.ExpressionWellformed.cs | 79 +--- .../Verifier/BoogieGenerator.Extremes.cs | 10 +- .../Verifier/BoogieGenerator.Fields.cs | 36 +- ...oogieGenerator.Functions.Wellformedness.cs | 8 +- .../Verifier/BoogieGenerator.Functions.cs | 84 ++--- .../Verifier/BoogieGenerator.Iterators.cs | 26 +- .../Verifier/BoogieGenerator.LetExpr.cs | 16 +- .../Verifier/BoogieGenerator.Methods.cs | 98 ++--- .../Verifier/BoogieGenerator.Reveal.cs | 2 +- .../Verifier/BoogieGenerator.SplitExpr.cs | 10 +- .../Verifier/BoogieGenerator.Types.cs | 156 ++++---- Source/DafnyCore/Verifier/BoogieGenerator.cs | 345 +++++++----------- .../Datatypes/BoogieGenerator.DataTypes.cs | 108 +++--- .../BoogieGenerator.TrAssignment.cs | 28 +- .../Statements/BoogieGenerator.TrCall.cs | 14 +- .../BoogieGenerator.TrForallStmt.cs | 12 +- .../Statements/BoogieGenerator.TrLoop.cs | 6 +- .../BoogieGenerator.TrPredicateStatement.cs | 6 +- .../Statements/BoogieGenerator.TrStatement.cs | 195 +--------- .../Statements/IfStatementVerifier.cs | 54 +++ .../Verifier/Statements/MatchVerifier.cs | 238 ++++++++++++ 25 files changed, 836 insertions(+), 815 deletions(-) create mode 100644 Source/DafnyCore/Verifier/Statements/IfStatementVerifier.cs create mode 100644 Source/DafnyCore/Verifier/Statements/MatchVerifier.cs diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs index 0773f1ac449..bd868d1038c 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs @@ -15,7 +15,7 @@ public Bpl.Type BplBvType(int width) { // Boogie claims to support bv0, but it translates it straight down to the SMT solver's 0-width bitvector type. // However, the SMT-LIB 2 standard does not define such a bitvector width, so this is a bug in Boogie. The // best would be to fix this in Boogie, but for now, we simply work around it here. - return predef.Bv0Type; + return Predef.Bv0Type; } else { return Bpl.Type.GetBvType(width); } @@ -39,7 +39,7 @@ internal Bpl.Expr BplBvLiteralExpr(Bpl.IToken tok, BaseTypes.BigNum n, int width // Bpl.LiteralExpr for a bitvector. var zero = new Bpl.LiteralExpr(tok, BaseTypes.BigNum.ZERO, width); var absN = new Bpl.LiteralExpr(tok, -n, width); - var etran = new ExpressionTranslator(this, predef, tok, null); + var etran = new ExpressionTranslator(this, Predef, tok, null); return etran.TrToFunctionCall(tok, "sub_bv" + width, BplBvType(width), zero, absN, false); } else { return new Bpl.LiteralExpr(tok, n, width); @@ -209,7 +209,7 @@ private Bpl.AssumeCmd TrAssumeCmdWithDependencies(ExpressionTranslator etran, Bp // expressions, for instance), creates an assume statement in Boogie, // and then adds information to track that assumption as a potential // proof dependency. - private Bpl.AssumeCmd TrAssumeCmdWithDependenciesAndExtend(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Func extendExpr, + public Bpl.AssumeCmd TrAssumeCmdWithDependenciesAndExtend(ExpressionTranslator etran, Bpl.IToken tok, Expression dafnyExpr, Func extendExpr, string comment = null, bool warnWhenUnused = false, Bpl.QKeyValue attributes = null) { var expr = etran.TrExpr(dafnyExpr); var cmd = TrAssumeCmd(tok, extendExpr(expr), attributes); @@ -234,7 +234,7 @@ bool IsLit(Bpl.Expr expr) { Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstantiation, params Bpl.Expr[] args) { Contract.Requires(tok != null); Contract.Requires(args != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Ensures(Contract.Result() != null); switch (f) { @@ -253,19 +253,19 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan case BuiltinFunction.LayerSucc: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); - return FunctionCall(tok, "$LS", predef.LayerType, args); + return FunctionCall(tok, "$LS", Predef.LayerType, args); case BuiltinFunction.AsFuelBottom: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); - return FunctionCall(tok, "AsFuelBottom", predef.LayerType, args); + return FunctionCall(tok, "AsFuelBottom", Predef.LayerType, args); case BuiltinFunction.CharFromInt: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); - return FunctionCall(tok, "char#FromInt", predef.CharType, args); + return FunctionCall(tok, "char#FromInt", Predef.CharType, args); case BuiltinFunction.CharToInt: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); - return FunctionCall(tok, "char#ToInt", predef.CharType, args); + return FunctionCall(tok, "char#ToInt", Predef.CharType, args); case BuiltinFunction.IsChar: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); @@ -298,21 +298,21 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan return FunctionCall(tok, "Set#Card", Bpl.Type.Int, args); case BuiltinFunction.SetEmpty: { Contract.Assert(args.Length == 0); - Bpl.Type resultType = predef.SetType; + Bpl.Type resultType = Predef.SetType; return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Set#Empty", resultType, args), resultType); } case BuiltinFunction.SetUnionOne: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "Set#UnionOne", predef.SetType, args); + return FunctionCall(tok, "Set#UnionOne", Predef.SetType, args); case BuiltinFunction.SetUnion: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "Set#Union", predef.SetType, args); + return FunctionCall(tok, "Set#Union", Predef.SetType, args); case BuiltinFunction.SetIntersection: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "Set#Intersection", predef.SetType, args); + return FunctionCall(tok, "Set#Intersection", Predef.SetType, args); case BuiltinFunction.SetDifference: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "Set#Difference", predef.SetType, args); + return FunctionCall(tok, "Set#Difference", Predef.SetType, args); case BuiltinFunction.SetEqual: Contract.Assert(args.Length == 2); Contract.Assert(typeInstantiation == null); @@ -327,21 +327,21 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan return FunctionCall(tok, "Set#Disjoint", Bpl.Type.Bool, args); case BuiltinFunction.ISetEmpty: { Contract.Assert(args.Length == 0); - Bpl.Type resultType = predef.ISetType; + Bpl.Type resultType = Predef.ISetType; return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "ISet#Empty", resultType, args), resultType); } case BuiltinFunction.ISetUnionOne: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "ISet#UnionOne", predef.ISetType, args); + return FunctionCall(tok, "ISet#UnionOne", Predef.ISetType, args); case BuiltinFunction.ISetUnion: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "ISet#Union", predef.ISetType, args); + return FunctionCall(tok, "ISet#Union", Predef.ISetType, args); case BuiltinFunction.ISetIntersection: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "ISet#Intersection", predef.ISetType, args); + return FunctionCall(tok, "ISet#Intersection", Predef.ISetType, args); case BuiltinFunction.ISetDifference: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "ISet#Difference", predef.ISetType, args); + return FunctionCall(tok, "ISet#Difference", Predef.ISetType, args); case BuiltinFunction.ISetEqual: Contract.Assert(args.Length == 2); return FunctionCall(tok, "ISet#Equal", Bpl.Type.Bool, args); @@ -356,21 +356,21 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan return FunctionCall(tok, "MultiSet#Card", Bpl.Type.Int, args); case BuiltinFunction.MultiSetEmpty: { Contract.Assert(args.Length == 0); - Bpl.Type resultType = predef.MultiSetType; + Bpl.Type resultType = Predef.MultiSetType; return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "MultiSet#Empty", resultType, args), resultType); } case BuiltinFunction.MultiSetUnionOne: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "MultiSet#UnionOne", predef.MultiSetType, args); + return FunctionCall(tok, "MultiSet#UnionOne", Predef.MultiSetType, args); case BuiltinFunction.MultiSetUnion: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "MultiSet#Union", predef.MultiSetType, args); + return FunctionCall(tok, "MultiSet#Union", Predef.MultiSetType, args); case BuiltinFunction.MultiSetIntersection: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "MultiSet#Intersection", predef.MultiSetType, args); + return FunctionCall(tok, "MultiSet#Intersection", Predef.MultiSetType, args); case BuiltinFunction.MultiSetDifference: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "MultiSet#Difference", predef.MultiSetType, args); + return FunctionCall(tok, "MultiSet#Difference", Predef.MultiSetType, args); case BuiltinFunction.MultiSetEqual: Contract.Assert(args.Length == 2); return FunctionCall(tok, "MultiSet#Equal", Bpl.Type.Bool, args); @@ -382,10 +382,10 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan return FunctionCall(tok, "MultiSet#Disjoint", Bpl.Type.Bool, args); case BuiltinFunction.MultiSetFromSet: Contract.Assert(args.Length == 1); - return FunctionCall(tok, "MultiSet#FromSet", predef.MultiSetType, args); + return FunctionCall(tok, "MultiSet#FromSet", Predef.MultiSetType, args); case BuiltinFunction.MultiSetFromSeq: Contract.Assert(args.Length == 1); - return FunctionCall(tok, "MultiSet#FromSeq", predef.MultiSetType, args); + return FunctionCall(tok, "MultiSet#FromSeq", Predef.MultiSetType, args); case BuiltinFunction.IsGoodMultiSet: Contract.Assert(args.Length == 1); return FunctionCall(tok, "$IsGoodMultiSet", Bpl.Type.Bool, args); @@ -395,30 +395,30 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan return FunctionCall(tok, "Seq#Length", Bpl.Type.Int, args); case BuiltinFunction.SeqEmpty: { Contract.Assert(args.Length == 0); - Bpl.Type resultType = predef.SeqType; + Bpl.Type resultType = Predef.SeqType; return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Seq#Empty", resultType, args), resultType); } case BuiltinFunction.SeqBuild: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "Seq#Build", predef.SeqType, args); + return FunctionCall(tok, "Seq#Build", Predef.SeqType, args); case BuiltinFunction.SeqAppend: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "Seq#Append", predef.SeqType, args); + return FunctionCall(tok, "Seq#Append", Predef.SeqType, args); case BuiltinFunction.SeqIndex: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "Seq#Index", predef.BoxType, args); + return FunctionCall(tok, "Seq#Index", Predef.BoxType, args); case BuiltinFunction.SeqUpdate: Contract.Assert(args.Length == 3); - return FunctionCall(tok, "Seq#Update", predef.SeqType, args); + return FunctionCall(tok, "Seq#Update", Predef.SeqType, args); case BuiltinFunction.SeqContains: Contract.Assert(args.Length == 2); return FunctionCall(tok, "Seq#Contains", Bpl.Type.Bool, args); case BuiltinFunction.SeqDrop: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "Seq#Drop", predef.SeqType, args); + return FunctionCall(tok, "Seq#Drop", Predef.SeqType, args); case BuiltinFunction.SeqTake: Contract.Assert(args.Length == 2); - return FunctionCall(tok, "Seq#Take", predef.SeqType, args); + return FunctionCall(tok, "Seq#Take", Predef.SeqType, args); case BuiltinFunction.SeqEqual: Contract.Assert(args.Length == 2); return FunctionCall(tok, "Seq#Equal", Bpl.Type.Bool, args); @@ -434,7 +434,7 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan case BuiltinFunction.MapEmpty: { Contract.Assert(args.Length == 0); - Bpl.Type resultType = predef.MapType; + Bpl.Type resultType = Predef.MapType; return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "Map#Empty", resultType, args), resultType); } case BuiltinFunction.MapCard: @@ -449,7 +449,7 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan return FunctionCall(tok, "Map#Elements", typeInstantiation, args); case BuiltinFunction.MapGlue: Contract.Assert(args.Length == 3); - return FunctionCall(tok, "Map#Glue", predef.MapType, args); + return FunctionCall(tok, "Map#Glue", Predef.MapType, args); case BuiltinFunction.MapEqual: Contract.Assert(args.Length == 2); Contract.Assert(typeInstantiation == null); @@ -465,7 +465,7 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan case BuiltinFunction.IMapEmpty: { Contract.Assert(args.Length == 0); - Bpl.Type resultType = predef.IMapType; + Bpl.Type resultType = Predef.IMapType; return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "IMap#Empty", resultType, args), resultType); } case BuiltinFunction.IMapDomain: @@ -476,7 +476,7 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan return FunctionCall(tok, "IMap#Elements", typeInstantiation, args); case BuiltinFunction.IMapGlue: Contract.Assert(args.Length == 3); - return FunctionCall(tok, "IMap#Glue", predef.IMapType, args); + return FunctionCall(tok, "IMap#Glue", Predef.IMapType, args); case BuiltinFunction.IMapEqual: Contract.Assert(args.Length == 2); Contract.Assert(typeInstantiation == null); @@ -485,16 +485,16 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan case BuiltinFunction.IndexField: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); - return FunctionCall(tok, "IndexField", predef.FieldName(tok), args); + return FunctionCall(tok, "IndexField", Predef.FieldName(tok), args); case BuiltinFunction.MultiIndexField: Contract.Assert(args.Length == 2); Contract.Assert(typeInstantiation == null); - return FunctionCall(tok, "MultiIndexField", predef.FieldName(tok), args); + return FunctionCall(tok, "MultiIndexField", Predef.FieldName(tok), args); case BuiltinFunction.Box: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); - return FunctionCall(tok, "$Box", predef.BoxType, args); + return FunctionCall(tok, "$Box", Predef.BoxType, args); case BuiltinFunction.Unbox: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation != null); @@ -529,19 +529,19 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan case BuiltinFunction.DynamicType: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); - return FunctionCall(tok, "dtype", predef.ClassNameType, args); + return FunctionCall(tok, "dtype", Predef.ClassNameType, args); case BuiltinFunction.TypeTuple: Contract.Assert(args.Length == 2); Contract.Assert(typeInstantiation == null); - return FunctionCall(tok, "TypeTuple", predef.ClassNameType, args); + return FunctionCall(tok, "TypeTuple", Predef.ClassNameType, args); case BuiltinFunction.DeclType: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation != null); - return FunctionCall(tok, "DeclType", predef.ClassNameType, args); + return FunctionCall(tok, "DeclType", Predef.ClassNameType, args); case BuiltinFunction.FieldOfDecl: Contract.Assert(args.Length == 2); Contract.Assert(typeInstantiation != null); - return FunctionCall(tok, "FieldOfDecl", predef.FieldName(tok), args); + return FunctionCall(tok, "FieldOfDecl", Predef.FieldName(tok), args); case BuiltinFunction.FDim: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation != null); @@ -554,7 +554,7 @@ Bpl.NAryExpr FunctionCall(Bpl.IToken tok, BuiltinFunction f, Bpl.Type typeInstan case BuiltinFunction.DatatypeCtorId: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); - return FunctionCall(tok, "DatatypeCtorId", predef.DtCtorId, args); + return FunctionCall(tok, "DatatypeCtorId", Predef.DtCtorId, args); case BuiltinFunction.DtRank: Contract.Assert(args.Length == 1); Contract.Assert(typeInstantiation == null); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs index c9b395b372a..0cfd8932c2d 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Decreases.cs @@ -110,7 +110,7 @@ Bpl.Expr DecreasesCheck(List toks, List prevGhostLocals, Contract.Requires(cce.NonNullElements(dafny1)); Contract.Requires(cce.NonNullElements(ee0)); Contract.Requires(cce.NonNullElements(ee1)); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Requires(dafny0.Count == dafny1.Count && dafny0.Count == ee0.Count && ee0.Count == ee1.Count); Contract.Requires(builder == null || suffixMsg != null); Contract.Ensures(Contract.Result() != null); @@ -246,7 +246,7 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out Contract.Requires(ty1 != null); Contract.Requires(e0 != null); Contract.Requires(e1 != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Ensures(Contract.ValueAtReturn(out less) != null); Contract.Ensures(Contract.ValueAtReturn(out atmost) != null); Contract.Ensures(Contract.ValueAtReturn(out eq) != null); @@ -314,8 +314,8 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out b1 = e1; } else { // for maps, compare their domains as sets - b0 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType, e0); - b1 = FunctionCall(tok, BuiltinFunction.MapDomain, predef.MapType, e1); + b0 = FunctionCall(tok, BuiltinFunction.MapDomain, Predef.MapType, e0); + b1 = FunctionCall(tok, BuiltinFunction.MapDomain, Predef.MapType, e1); } eq = FunctionCall(tok, BuiltinFunction.SetEqual, null, b0, b1); less = ProperSubset(tok, b0, b1); @@ -330,8 +330,8 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out } else { Contract.Assert(!((MapType)ty0).Finite); // for maps, compare their domains as sets - b0 = FunctionCall(tok, BuiltinFunction.IMapDomain, predef.MapType, e0); - b1 = FunctionCall(tok, BuiltinFunction.IMapDomain, predef.MapType, e1); + b0 = FunctionCall(tok, BuiltinFunction.IMapDomain, Predef.MapType, e0); + b1 = FunctionCall(tok, BuiltinFunction.IMapDomain, Predef.MapType, e1); } eq = FunctionCall(tok, BuiltinFunction.ISetEqual, null, b0, b1); less = Bpl.Expr.False; @@ -366,8 +366,8 @@ void ComputeLessEq(IToken tok, Type ty0, Type ty1, Bpl.Expr e0, Bpl.Expr e1, out } else { // reference type Contract.Assert(ty0.IsRefType); // otherwise, unexpected type - var b0 = Bpl.Expr.Neq(e0, predef.Null); - var b1 = Bpl.Expr.Neq(e1, predef.Null); + var b0 = Bpl.Expr.Neq(e0, Predef.Null); + var b1 = Bpl.Expr.Neq(e1, Predef.Null); eq = BplIff(b0, b1); less = BplAnd(Bpl.Expr.Not(b0), b1); atmost = BplImp(b0, b1); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs index 87fb7cb6cbb..70a8c6b57ef 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs @@ -172,7 +172,7 @@ void AssumeCanCallForByMethodDecl(Method method, BoogieStmtListBuilder builder) // fn == new FunctionCallExpr(tok, f.Name, receiver, tok, tok, f.Formals.ConvertAll(Expression.CreateIdentExpr)); Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(method.tok, method.FullSanitizedName + "#canCall", Bpl.Type.Bool); - var etran = new ExpressionTranslator(this, predef, method.tok, method); + var etran = new ExpressionTranslator(this, Predef, method.tok, method); List args = arguments.Select(arg => etran.TrExpr(arg)).ToList(); var formals = MkTyParamBinders(GetTypeParams(method), out var tyargs); if (method.FunctionFromWhichThisIsByMethodDecl.ReadsHeap) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs index 10d78a37498..d7ce4d1af1a 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs @@ -390,7 +390,7 @@ public Boogie.Expr TrExpr(Expression expr) { args.Add(Old.HeapExpr); } foreach (var heapAtLabel in e.HeapAtLabels) { - var bv = BplBoundVar("$Heap_at_" + heapAtLabel.AssignUniqueId(BoogieGenerator.CurrentIdGenerator), BoogieGenerator.predef.HeapType, out var ve); + var bv = BplBoundVar("$Heap_at_" + heapAtLabel.AssignUniqueId(BoogieGenerator.CurrentIdGenerator), BoogieGenerator.Predef.HeapType, out var ve); args.Add(ve); } foreach (var arg in e.Args) { @@ -1642,7 +1642,7 @@ public Boogie.Expr TrBoundVariables(List boundVars, List boundVars, List>(); foreach (BoundVar bv in boundVars) { - var tid = new Boogie.TypedIdent(bv.tok, bv.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator), BoogieGenerator.TrType(bv.Type)); + var tid = new Boogie.TypedIdent(bv.tok, bv.AssignUniqueName(BoogieGenerator.CurrentDeclaration.IdGenerator), BoogieGenerator.TrType(bv.Type)); var bvar = new Boogie.BoundVariable(bv.tok, tid); var wh = BoogieGenerator.GetWhereClause(bv.tok, new Boogie.IdentifierExpr(bv.tok, bvar), bv.Type, this, NOALLOC); varsAndAntecedents.Add(Tuple.Create(bvar, wh)); @@ -1683,10 +1683,10 @@ public Boogie.Expr TrBoundVariablesRename(List boundVars, List() != null); if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr || expr is BoogieWrapper) { @@ -2249,7 +2249,7 @@ public Expr CanCallAssumption(Expression expr) { var bvarsAndAntecedents = new List>(); var varNameGen = BoogieGenerator.CurrentIdGenerator.NestedFreshIdGenerator("$l#"); - Boogie.Expr heap; var hVar = BplBoundVar(varNameGen.FreshId("#heap#"), BoogieGenerator.predef.HeapType, out heap); + Boogie.Expr heap; var hVar = BplBoundVar(varNameGen.FreshId("#heap#"), BoogieGenerator.Predef.HeapType, out heap); var et = new ExpressionTranslator(this, heap); Dictionary subst = new Dictionary(); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs index d7c3aa02760..8ec7fcb6537 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.ExpressionWellformed.cs @@ -139,7 +139,7 @@ public void CheckWellformedAndAssume(Expression expr, WFOptions wfOptions, Varia Contract.Requires(locals != null); Contract.Requires(builder != null); Contract.Requires(etran != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); if (expr is BinaryExpr) { var e = (BinaryExpr)expr; switch (e.ResolvedOp) { @@ -254,7 +254,7 @@ public void CheckWellformed(Expression expr, WFOptions wfOptions, Variables loca Contract.Requires(locals != null); Contract.Requires(builder != null); Contract.Requires(etran != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); CheckWellformedWithResult(expr, wfOptions, locals, builder, etran, null); } @@ -265,7 +265,7 @@ public void CheckWellformed(Expression expr, WFOptions wfOptions, Variables loca /// assume the equivalent of "result == expr". /// See class WFOptions for descriptions of the specified options. /// - void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, + public void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Variables locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, AddResultCommands addResultCommands) { var origOptions = wfOptions; @@ -387,7 +387,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, CheckWellformed(e.Seq, wfOptions, locals, builder, etran); Bpl.Expr seq = etran.TrExpr(e.Seq); if (eSeqType.IsArrayType) { - builder.Add(Assert(GetToken(e.Seq), Bpl.Expr.Neq(seq, predef.Null), + builder.Add(Assert(GetToken(e.Seq), Bpl.Expr.Neq(seq, Predef.Null), new NonNull("array", e.Seq), builder.Context)); if (etran.UsesOldHeap) { builder.Add(Assert(GetToken(e.Seq), MkIsAlloc(seq, eSeqType, etran.HeapExpr), @@ -400,7 +400,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, e0 = etran.TrExpr(e.E0); CheckWellformed(e.E0, wfOptions, locals, builder, etran); var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain; - Bpl.Expr inDomain = FunctionCall(selectExpr.tok, f, finite ? predef.MapType : predef.IMapType, seq); + Bpl.Expr inDomain = FunctionCall(selectExpr.tok, f, finite ? Predef.MapType : Predef.IMapType, seq); inDomain = Bpl.Expr.Select(inDomain, BoxIfNecessary(e.tok, e0, e.E0.Type)); builder.Add(Assert(GetToken(expr), inDomain, new ElementInDomain(e.Seq, e.E0), builder.Context, wfOptions.AssertKv)); @@ -467,7 +467,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, MultiSelectExpr e = selectExpr; CheckWellformed(e.Array, wfOptions, locals, builder, etran); Bpl.Expr array = etran.TrExpr(e.Array); - builder.Add(Assert(GetToken(e.Array), Bpl.Expr.Neq(array, predef.Null), + builder.Add(Assert(GetToken(e.Array), Bpl.Expr.Neq(array, Predef.Null), new NonNull("array", e.Array), builder.Context)); if (etran.UsesOldHeap) { builder.Add(Assert(GetToken(e.Array), MkIsAlloc(array, e.Array.Type, etran.HeapExpr), @@ -696,12 +696,12 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Type et = p.Type.Subst(e.GetTypeArgumentSubstitutions()); LocalVariable local = new LocalVariable(p.RangeToken, "##" + p.Name, et, p.IsGhost); local.type = local.SyntacticType; // resolve local here - var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)) { + var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(CurrentDeclaration.IdGenerator)) { Var = local }; ie.Type = ie.Var.Type; // resolve ie here substMap.Add(p, ie); - locals.GetOrAdd(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), TrType(local.Type)))); + locals.GetOrAdd(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(local.Type)))); Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie); // TODO: is this cast always justified? Expression ee = e.Args[i]; directSubstMap.Add(p, ee); @@ -959,7 +959,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, nonNull = Bpl.Expr.True; } else { Contract.Assert(ty.IsRefType); - nonNull = Bpl.Expr.Neq(r, predef.Null); + nonNull = Bpl.Expr.Neq(r, Predef.Null); builder.Add(Assert(GetToken(fe.E), BplImp(ante, nonNull), new NonNull(description, fe.E, description != "object"), builder.Context)); } @@ -1173,7 +1173,7 @@ void CheckOperand(Expression operand) { var comprehensionEtran = etran; if (lam != null) { // Havoc heap - locals.GetOrAdd(BplLocalVar(CurrentIdGenerator.FreshId((etran.UsesOldHeap ? "$Heap_at_" : "") + "$lambdaHeap#"), predef.HeapType, out var lambdaHeap)); + locals.GetOrAdd(BplLocalVar(CurrentIdGenerator.FreshId((etran.UsesOldHeap ? "$Heap_at_" : "") + "$lambdaHeap#"), Predef.HeapType, out var lambdaHeap)); comprehensionEtran = new ExpressionTranslator(comprehensionEtran, lambdaHeap); nextBuilder.Add(new HavocCmd(e.tok, Singleton((Bpl.IdentifierExpr)comprehensionEtran.HeapExpr))); nextBuilder.Add(new AssumeCmd(e.tok, FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, comprehensionEtran.HeapExpr))); @@ -1313,7 +1313,7 @@ void AddResultCommands(BoogieStmtListBuilder returnBuilder, Expression result) { break; } case MatchExpr matchExpr: - TrMatchExpr(matchExpr, wfOptions, locals, builder, etran, addResultCommands); + MatchStatementVerifier.TrMatchExpr(this, matchExpr, wfOptions, locals, builder, etran, addResultCommands); addResultCommands = null; break; case DatatypeUpdateExpr updateExpr: { @@ -1380,55 +1380,6 @@ public void CheckSubsetType(ExpressionTranslator etran, Expression expr, Bpl.Exp builder.Add(TrAssumeCmd(expr.tok, MkIs(selfCall, resultType))); } - private void TrMatchExpr(MatchExpr me, WFOptions wfOptions, Variables locals, - BoogieStmtListBuilder builder, ExpressionTranslator etran, AddResultCommands addResultCommands) { - FillMissingCases(me); - - CheckWellformed(me.Source, wfOptions, locals, builder, etran); - Bpl.Expr src = etran.TrExpr(me.Source); - Bpl.IfCmd ifCmd = null; - BoogieStmtListBuilder elsBldr = new BoogieStmtListBuilder(this, options, builder.Context); - elsBldr.Add(TrAssumeCmd(me.tok, Bpl.Expr.False)); - StmtList els = elsBldr.Collect(me.tok); - foreach (var missingCtor in me.MissingCases) { - // havoc all bound variables - var b = new BoogieStmtListBuilder(this, options, builder.Context); - Variables newLocals = new(); - Bpl.Expr r = CtorInvocation(me.tok, missingCtor, etran, newLocals, b); - locals.AddRange(newLocals.Values); - - if (newLocals.Count != 0) { - List havocIds = new List(); - foreach (Variable local in newLocals.Values) { - havocIds.Add(new Bpl.IdentifierExpr(local.tok, local)); - } - - builder.Add(new Bpl.HavocCmd(me.tok, havocIds)); - } - - String missingStr = me.Context.FillHole(new IdCtx(missingCtor)).AbstractAllHoles().ToString(); - b.Add(Assert(GetToken(me), Bpl.Expr.False, - new MatchIsComplete("expression", missingStr), builder.Context)); - - Bpl.Expr guard = Bpl.Expr.Eq(src, r); - ifCmd = new Bpl.IfCmd(me.tok, guard, b.Collect(me.tok), ifCmd, els); - els = null; - } - - for (int i = me.Cases.Count; 0 <= --i;) { - MatchCaseExpr mc = me.Cases[i]; - var b = new BoogieStmtListBuilder(this, options, builder.Context); - Bpl.Expr ct = CtorInvocation(mc, me.Source.Type, etran, locals, b, NOALLOC, false); - // generate: if (src == ctor(args)) { assume args-is-well-typed; mc.Body is well-formed; assume Result == TrExpr(case); } else ... - - CheckWellformedWithResult(mc.Body, wfOptions, locals, b, etran, addResultCommands); - ifCmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifCmd, els); - els = null; - } - - builder.Add(ifCmd); - } - private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, Variables locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, AddResultCommands addResultCommands) { @@ -1469,9 +1420,9 @@ private void CheckWellformedStmtExpr(StmtExpr stmtExpr, WFOptions wfOptions, Var void BuildWithHeapAs(IToken token, Bpl.Expr temporaryHeap, string heapVarSuffix, Variables locals, BoogieStmtListBuilder builder, System.Action build) { var suffix = CurrentIdGenerator.FreshId(heapVarSuffix); - var tmpHeapVar = locals.GetOrAdd(new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "Heap$" + suffix, predef.HeapType))); + var tmpHeapVar = locals.GetOrAdd(new Bpl.LocalVariable(token, new Bpl.TypedIdent(token, "Heap$" + suffix, Predef.HeapType))); var tmpHeap = new Bpl.IdentifierExpr(token, tmpHeapVar); - var generalEtran = new ExpressionTranslator(this, predef, token, null); + var generalEtran = new ExpressionTranslator(this, Predef, token, null); var theHeap = generalEtran.HeapCastToIdentifierExpr; // tmpHeap := $Heap; @@ -1527,7 +1478,7 @@ void CheckWellformedSpecialFunction(FunctionCallExpr expr, WFOptions options, Bp } } - delegate void AddResultCommands(BoogieStmtListBuilder builder, Expression result); + public delegate void AddResultCommands(BoogieStmtListBuilder builder, Expression result); void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Variables locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, bool checkRhs, AddResultCommands addResultCommands) { @@ -1616,7 +1567,7 @@ void CheckFrameWellFormed(WFOptions wfo, List fes, Variables lo foreach (var fe in fes) { CheckWellformed(fe.E, wfo, locals, builder, etran); if (fe.Field != null && fe.E.Type.IsRefType) { - builder.Add(Assert(fe.tok, Bpl.Expr.Neq(etran.TrExpr(fe.E), predef.Null), new FrameDereferenceNonNull(fe.E), builder.Context)); + builder.Add(Assert(fe.tok, Bpl.Expr.Neq(etran.TrExpr(fe.E), Predef.Null), new FrameDereferenceNonNull(fe.E), builder.Context)); } } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs index d68ee1c6472..3825e266eb4 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Extremes.cs @@ -50,10 +50,10 @@ public partial class BoogieGenerator { /// void AddPrefixPredicateAxioms(PrefixPredicate pp) { Contract.Requires(pp != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); var co = pp.ExtremePred; var tok = pp.tok; - var etran = new ExpressionTranslator(this, predef, tok, pp); + var etran = new ExpressionTranslator(this, Predef, tok, pp); var tyvars = MkTyParamBinders(GetTypeParams(pp), out var tyexprs); @@ -63,7 +63,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) { var prefixArgsLimited = new List(tyexprs); var prefixArgsLimitedM = new List(tyexprs); if (pp.IsFuelAware()) { - var sV = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$ly", predef.LayerType)); + var sV = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$ly", Predef.LayerType)); var s = new Bpl.IdentifierExpr(tok, sV); var succS = FunctionCall(tok, BuiltinFunction.LayerSucc, null, s); bvs.Add(sV); @@ -75,7 +75,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) { Bpl.Expr h; if (pp.ReadsHeap) { - var heapIdent = new Bpl.TypedIdent(tok, predef.HeapVarName, predef.HeapType); + var heapIdent = new Bpl.TypedIdent(tok, Predef.HeapVarName, Predef.HeapType); var bv = new Bpl.BoundVariable(tok, heapIdent); h = new Bpl.IdentifierExpr(tok, bv); bvs.Add(bv); @@ -180,7 +180,7 @@ void AddPrefixPredicateAxioms(PrefixPredicate pp) { moreBvs.Add(k); var z = Bpl.Expr.Eq(kId, pp.Ins[0].Type.IsBigOrdinalType - ? (Bpl.Expr)FunctionCall(tok, "ORD#FromNat", predef.BigOrdinalType, Bpl.Expr.Literal(0)) + ? (Bpl.Expr)FunctionCall(tok, "ORD#FromNat", Predef.BigOrdinalType, Bpl.Expr.Literal(0)) : Bpl.Expr.Literal(0)); funcID = new Bpl.IdentifierExpr(tok, pp.FullSanitizedName, TrType(pp.ResultType)); Bpl.Expr prefixLimitedBody = new Bpl.NAryExpr(tok, new Bpl.FunctionCall(funcID), prefixArgsLimited); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs index 06cc23c7a22..ec154154c3a 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs @@ -15,7 +15,7 @@ public partial class BoogieGenerator { Bpl.Constant GetField(Field f) { Contract.Requires(f != null && f.IsMutable); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(VisibleInScope(f)); @@ -25,7 +25,7 @@ Bpl.Constant GetField(Field f) { Contract.Assert(fc != null); } else { // const f: Field ty; - Bpl.Type ty = predef.FieldName(f.tok); + Bpl.Type ty = Predef.FieldName(f.tok); fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullSanitizedName, ty), false); fields.Add(f, fc); // axiom FDim(f) == 0 && FieldOfDecl(C, name) == f && @@ -46,7 +46,7 @@ Bpl.Constant GetField(Field f) { Bpl.Function GetReadonlyField(Field f) { Contract.Requires(f != null && !f.IsMutable); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); Contract.Ensures(Contract.Result() != null); Contract.Assert(VisibleInScope(f)); @@ -57,33 +57,33 @@ Bpl.Function GetReadonlyField(Field f) { } else { // Here are some built-in functions defined in "predef" (so there's no need to cache them in "fieldFunctions") if (f.EnclosingClass is ArrayClassDecl && f.Name == "Length") { - return predef.ArrayLength; + return Predef.ArrayLength; } else if (f.EnclosingClass is ValuetypeDecl { Name: "real" } && f.Name == "Floor") { - return predef.RealFloor; + return Predef.RealFloor; } else if (f is SpecialField && !(f is DatatypeDestructor || f.EnclosingClass is TopLevelDeclWithMembers and not ValuetypeDecl)) { if (f.Name is "Keys" or "Values" or "Items") { var fType = f.Type.NormalizeExpand(); Contract.Assert(fType is SetType); var setType = (SetType)fType; return f.Name switch { - "Keys" => setType.Finite ? predef.MapDomain : predef.IMapDomain, - "Values" => setType.Finite ? predef.MapValues : predef.IMapValues, - _ => setType.Finite ? predef.MapItems : predef.IMapItems + "Keys" => setType.Finite ? Predef.MapDomain : Predef.IMapDomain, + "Values" => setType.Finite ? Predef.MapValues : Predef.IMapValues, + _ => setType.Finite ? Predef.MapItems : Predef.IMapItems }; } if (f.Name == "IsLimit") { - return predef.ORDINAL_IsLimit; + return Predef.ORDINAL_IsLimit; } else if (f.Name == "IsSucc") { - return predef.ORDINAL_IsSucc; + return Predef.ORDINAL_IsSucc; } else if (f.Name == "Offset") { - return predef.ORDINAL_Offset; + return Predef.ORDINAL_Offset; } else if (f.Name == "IsNat") { - return predef.ORDINAL_IsNat; + return Predef.ORDINAL_IsNat; } } else if (f.FullSanitizedName == "_System.Tuple2._0") { - return predef.Tuple2Destructors0; + return Predef.Tuple2Destructors0; } else if (f.FullSanitizedName == "_System.Tuple2._1") { - return predef.Tuple2Destructors1; + return Predef.Tuple2Destructors1; } // Create a new function @@ -117,7 +117,7 @@ Bpl.Function GetReadonlyField(Field f) { // function QQ():int { 3 } var cf = (ConstantField)f; if (cf.Rhs != null && RevealedInScope(cf)) { - var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(f.tok), null); + var etran = new ExpressionTranslator(this, Predef, NewOneHeapExpr(f.tok), null); if (!IsOpaque(cf, options)) { var definitionAxiom = ff.CreateDefinitionAxiom(etran.TrExpr(cf.Rhs)); definitionAxiom.CanHide = true; @@ -129,7 +129,7 @@ Bpl.Function GetReadonlyField(Field f) { } else if (f.EnclosingClass is ArrayClassDecl) { // add non-negative-range axioms for array Length fields // axiom (forall o: Ref :: 0 <= array.Length(o)); - Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "o", predef.RefType)); + Bpl.BoundVariable oVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "o", Predef.RefType)); Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(f.tok, oVar); var rhs = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(ff), new List { o }); Bpl.Expr body = Bpl.Expr.Le(Bpl.Expr.Literal(0), rhs); @@ -151,7 +151,7 @@ Bpl.Expr GetField(MemberSelectExpr fse) { void AddWellformednessCheck(ConstantField decl) { Contract.Requires(decl != null); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); Contract.Requires(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null); Contract.Ensures(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null); @@ -169,7 +169,7 @@ void AddWellformednessCheck(ConstantField decl) { currentModule = decl.EnclosingModule; codeContext = decl; fuelContext = FuelSetting.NewFuelContext(decl); - var etran = new ExpressionTranslator(this, predef, decl.tok, null); + var etran = new ExpressionTranslator(this, Predef, decl.tok, null); // parameters of the procedure List inParams = MkTyParamFormals(GetTypeParams(decl.EnclosingClass), true); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs index d6e92d20317..b0005c0cdcb 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.Wellformedness.cs @@ -26,7 +26,7 @@ public void Check(Function f) { generator.currentModule = f.EnclosingClass.EnclosingModuleDefinition; generator.codeContext = f; - ExpressionTranslator ordinaryEtran = new ExpressionTranslator(generator, generator.predef, f.tok, f); + ExpressionTranslator ordinaryEtran = new ExpressionTranslator(generator, generator.Predef, f.tok, f); var etran = GetExpressionTranslator(f, ordinaryEtran, out var additionalRequires, out var heapParameters); // parameters of the procedure @@ -330,13 +330,13 @@ private ExpressionTranslator GetExpressionTranslator(Function f, ExpressionTrans additionalRequires = new(); inParams_Heap = new List(); if (f is TwoStateFunction) { - var prevHeapVar = new Bpl.Formal(f.tok, new TypedIdent(f.tok, "previous$Heap", generator.predef.HeapType), true); - var currHeapVar = new Bpl.Formal(f.tok, new TypedIdent(f.tok, "current$Heap", generator.predef.HeapType), true); + var prevHeapVar = new Bpl.Formal(f.tok, new TypedIdent(f.tok, "previous$Heap", generator.Predef.HeapType), true); + var currHeapVar = new Bpl.Formal(f.tok, new TypedIdent(f.tok, "current$Heap", generator.Predef.HeapType), true); inParams_Heap.Add(prevHeapVar); inParams_Heap.Add(currHeapVar); Expr prevHeap = new Bpl.IdentifierExpr(f.tok, prevHeapVar); Expr currHeap = new Bpl.IdentifierExpr(f.tok, currHeapVar); - etran = new ExpressionTranslator(generator, generator.predef, currHeap, prevHeap, f); + etran = new ExpressionTranslator(generator, generator.Predef, currHeap, prevHeap, f); // free requires prevHeap == Heap && HeapSucc(prevHeap, currHeap) && IsHeap(currHeap) var a0 = Expr.Eq(prevHeap, ordinaryEtran.HeapExpr); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs index 0a419e5021a..5d1b4865e5d 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs @@ -61,7 +61,7 @@ void AddFunctionAxiom(Bpl.Function boogieFunction, Function f, Expression body) void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, List ens) { Contract.Requires(f != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Requires(f.EnclosingClass != null); bool readsHeap = f.ReadsHeap; @@ -73,14 +73,14 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis ExpressionTranslator etran; Bpl.BoundVariable bvPrevHeap = null; if (f is TwoStateFunction) { - bvPrevHeap = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", predef.HeapType)); - etran = new ExpressionTranslator(this, predef, - f.ReadsHeap ? new Bpl.IdentifierExpr(f.tok, predef.HeapVarName, predef.HeapType) : null, + bvPrevHeap = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", Predef.HeapType)); + etran = new ExpressionTranslator(this, Predef, + f.ReadsHeap ? new Bpl.IdentifierExpr(f.tok, Predef.HeapVarName, Predef.HeapType) : null, new Bpl.IdentifierExpr(f.tok, bvPrevHeap), f); etranHeap = etran; } else { - etranHeap = new ExpressionTranslator(this, predef, f.tok, f); - etran = readsHeap ? etranHeap : new ExpressionTranslator(this, predef, (Bpl.Expr)null, f); + etranHeap = new ExpressionTranslator(this, Predef, f.tok, f); + etran = readsHeap ? etranHeap : new ExpressionTranslator(this, Predef, (Bpl.Expr)null, f); } // This method generate the Consequence Axiom, which has information about the function's @@ -123,7 +123,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis var olderInParams = new List(); // for use with older-condition Bpl.BoundVariable layer; if (f.IsFuelAware()) { - layer = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType)); + layer = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", Predef.LayerType)); formals.Add(layer); etran = etran.WithCustomFuelSetting(new CustomFuelSettings { { f, new FuelSetting(this, 0, new Bpl.IdentifierExpr(f.tok, layer)) } }); //etran = etran.WithLayer(new Bpl.IdentifierExpr(f.tok, layer)); @@ -151,7 +151,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis ante = BplAnd(ante, goodHeap); anteIsAlloc = BplAnd(anteIsAlloc, goodHeap); } - var bvHeap = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType)); + var bvHeap = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, Predef.HeapVarName, Predef.HeapType)); if (f.ReadsHeap) { args.Add(new Bpl.IdentifierExpr(f.tok, bvHeap)); } @@ -192,7 +192,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis } } foreach (Formal p in f.Ins) { - var bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(currentDeclaration.IdGenerator), TrType(p.Type))); + var bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(p.Type))); Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv); formals.Add(bv); olderInParams.Add(bv); @@ -303,7 +303,7 @@ void AddFunctionConsequenceAxiom(Boogie.Function boogieFunction, Function f, Lis /// private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { Contract.Requires(f != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Requires(f.EnclosingClass != null); Contract.Ensures((Contract.Result() == null) == (body == null)); // return null iff body is null @@ -371,14 +371,14 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { ExpressionTranslator etran; Bpl.BoundVariable bvPrevHeap = null; if (f is TwoStateFunction) { - bvPrevHeap = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", predef.HeapType)); - etran = new ExpressionTranslator(this, predef, - f.ReadsHeap ? new Bpl.IdentifierExpr(f.tok, predef.HeapVarName, predef.HeapType) : null, + bvPrevHeap = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", Predef.HeapType)); + etran = new ExpressionTranslator(this, Predef, + f.ReadsHeap ? new Bpl.IdentifierExpr(f.tok, Predef.HeapVarName, Predef.HeapType) : null, new Bpl.IdentifierExpr(f.tok, bvPrevHeap), f); } else { etran = readsHeap - ? new ExpressionTranslator(this, predef, f.tok, f) - : new ExpressionTranslator(this, predef, (Bpl.Expr)null, f); + ? new ExpressionTranslator(this, Predef, f.tok, f) + : new ExpressionTranslator(this, Predef, (Bpl.Expr)null, f); } // quantify over the type arguments, and add them first to the arguments @@ -392,7 +392,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { Bpl.BoundVariable layer; Bpl.BoundVariable reveal; if (f.IsFuelAware()) { - layer = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType)); + layer = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", Predef.LayerType)); forallFormals.Add(layer); funcFormals.Add(layer); reqFuncArguments.Add(new Bpl.IdentifierExpr(f.tok, layer)); @@ -422,7 +422,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { } Bpl.Expr goodHeap = null; - var bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType)); + var bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, Predef.HeapVarName, Predef.HeapType)); if (f.ReadsHeap) { funcFormals.Add(bv); } @@ -480,7 +480,7 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { foreach (Formal p in f.Ins) { var pType = p.Type.Subst(typeMap); bv = new Bpl.BoundVariable(p.tok, - new Bpl.TypedIdent(p.tok, p.AssignUniqueName(currentDeclaration.IdGenerator), TrType(pType))); + new Bpl.TypedIdent(p.tok, p.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(pType))); forallFormals.Add(bv); funcFormals.Add(bv); reqFuncArguments.Add(new Bpl.IdentifierExpr(f.tok, bv)); @@ -689,10 +689,10 @@ public string FunctionHandle(Function f) { } tyargs.Add(TypeToTy(f.ResultType)); if (f.IsFuelAware()) { - vars.Add(BplBoundVar("$ly", predef.LayerType, out var ly)); + vars.Add(BplBoundVar("$ly", Predef.LayerType, out var ly)); args.Add(ly); argsRequires.Add(ly); - formals.Add(BplFormalVar("$fuel", predef.LayerType, true)); + formals.Add(BplFormalVar("$fuel", Predef.LayerType, true)); AddFuelSuccSynonymAxiom(f, true); } if (f.IsOpaque || f.IsMadeImplicitlyOpaque(options)) { @@ -707,8 +707,8 @@ public string FunctionHandle(Function f) { Dictionary rhs_dict = new Dictionary(); if (f is TwoStateFunction) { // also add previous-heap to the list of fixed arguments of the handle - var prevH = BplBoundVar("$prevHeap", predef.HeapType, vars); - formals.Add(BplFormalVar("h", predef.HeapType, true)); + var prevH = BplBoundVar("$prevHeap", Predef.HeapType, vars); + formals.Add(BplFormalVar("h", Predef.HeapType, true)); SnocPrevH = xs => Snoc(xs, prevH); } if (f.IsStatic) { @@ -724,7 +724,7 @@ public string FunctionHandle(Function f) { // F#Handle(Ty, .., Ty, LayerType, ref) : HandleType sink.AddTopLevelDeclaration( - new Bpl.Function(f.tok, name, formals, BplFormalVar(null, predef.HandleType, false))); + new Bpl.Function(f.tok, name, formals, BplFormalVar(null, Predef.HandleType, false))); var bvars = new List(); var lhs_args = new List(); @@ -737,7 +737,7 @@ public string FunctionHandle(Function f) { foreach (var fm in f.Ins) { string fm_name = idGen.FreshId("x#"); // Box and its [Unbox]args - var fe = BplBoundVar(fm_name, predef.BoxType, bvars); + var fe = BplBoundVar(fm_name, Predef.BoxType, bvars); lhs_args.Add(fe); var be = UnboxUnlessInherentlyBoxed(fe, fm.Type); rhs_args.Add(be); @@ -750,7 +750,7 @@ public string FunctionHandle(Function f) { boxed_func_args.Add(boxed); } - var h = BplBoundVar("$heap", predef.HeapType, vars); + var h = BplBoundVar("$heap", Predef.HeapType, vars); int arity = f.Ins.Count; @@ -758,7 +758,7 @@ public string FunctionHandle(Function f) { // Apply(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, arg1, ..., argN) // = [Box] F(Ty1, .., TyN, Layer, Heap, self, [Unbox] arg1, .., [Unbox] argN) - var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(SnocPrevH(args))); + var fhandle = FunctionCall(f.tok, name, Predef.HandleType, SnocSelf(SnocPrevH(args))); var lhs = FunctionCall(f.tok, Apply(arity), TrType(f.ResultType), Concat(tyargs, Cons(h, Cons(fhandle, lhs_args)))); var args_h = f.ReadsHeap ? Snoc(SnocPrevH(args), h) : args; @@ -778,7 +778,7 @@ public string FunctionHandle(Function f) { // The requires clause of the .requires function is simply true. // The requires clause of the .reads function checks that the precondtion of the receiving function holds. - var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(SnocPrevH(args))); + var fhandle = FunctionCall(f.tok, name, Predef.HandleType, SnocSelf(SnocPrevH(args))); var lhs = FunctionCall(f.tok, Requires(arity), Bpl.Type.Bool, Concat(tyargs, Cons(h, Cons(fhandle, lhs_args)))); Bpl.Expr rhs; if (f.EnclosingClass is ArrowTypeDecl && f.Name == "requires") { @@ -808,14 +808,14 @@ public string FunctionHandle(Function f) { // In both cases, the precondition of the receiving function must be checked before its reads clause can // be referred to. - var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(SnocPrevH(args))); + var fhandle = FunctionCall(f.tok, name, Predef.HandleType, SnocSelf(SnocPrevH(args))); Bpl.Expr lhs_inner = FunctionCall(f.tok, Reads(arity), TrType(program.SystemModuleManager.ObjectSetType()), Concat(tyargs, Cons(h, Cons(fhandle, lhs_args)))); - Bpl.Expr bx; var bxVar = BplBoundVar("$bx", predef.BoxType, out bx); - Bpl.Expr unboxBx = FunctionCall(f.tok, BuiltinFunction.Unbox, predef.RefType, bx); + Bpl.Expr bx; var bxVar = BplBoundVar("$bx", Predef.BoxType, out bx); + Bpl.Expr unboxBx = FunctionCall(f.tok, BuiltinFunction.Unbox, Predef.RefType, bx); Bpl.Expr lhs = Bpl.Expr.SelectTok(f.tok, lhs_inner, bx); - var et = new ExpressionTranslator(this, predef, h, f); + var et = new ExpressionTranslator(this, Predef, h, f); var rhs = InRWClause_Aux(f.tok, unboxBx, bx, null, f.Reads.Expressions, false, et, selfExpr, rhs_dict); if (f.EnclosingClass is ArrowTypeDecl) { @@ -833,7 +833,7 @@ public string FunctionHandle(Function f) { // F(Ty1, .., TyN, Layer, Heap, self, arg1, .., argN) // = [Unbox]Apply1(Ty.., F#Handle( Ty1, ..., TyN, Layer, self), Heap, [Box]arg1, ..., [Box]argN) - var fhandle = FunctionCall(f.tok, name, predef.HandleType, SnocSelf(SnocPrevH(args))); + var fhandle = FunctionCall(f.tok, name, Predef.HandleType, SnocSelf(SnocPrevH(args))); var args_h = f.ReadsHeap ? Snoc(SnocPrevH(args), h) : args; var lhs = FunctionCall(f.tok, f.FullSanitizedName, TrType(f.ResultType), Concat(SnocSelf(args_h), func_args)); var rhs = FunctionCall(f.tok, Apply(arity), TrType(f.ResultType), Concat(tyargs, Cons(h, Cons(fhandle, boxed_func_args)))); @@ -872,7 +872,7 @@ public string FunctionHandle(Function f) { /// void AddFrameAxiom(Function f) { Contract.Requires(f != null); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); var comment = "frame axiom for " + f.FullSanitizedName; // This is the general case @@ -886,21 +886,21 @@ void AddFrameAxiom(Function f) { if (f is TwoStateFunction) { // The previous-heap argument is the same for both function arguments. That is, // the frame axiom says nothing about functions invoked with different previous heaps. - prevHVar = BplBoundVar("$prevHeap", predef.HeapType, out prevH); + prevHVar = BplBoundVar("$prevHeap", Predef.HeapType, out prevH); } - Bpl.Expr h0; var h0Var = BplBoundVar("$h0", predef.HeapType, out h0); - Bpl.Expr h1; var h1Var = BplBoundVar("$h1", predef.HeapType, out h1); + Bpl.Expr h0; var h0Var = BplBoundVar("$h0", Predef.HeapType, out h0); + Bpl.Expr h1; var h1Var = BplBoundVar("$h1", Predef.HeapType, out h1); - var etran0 = new ExpressionTranslator(this, predef, h0, f); - var etran1 = new ExpressionTranslator(this, predef, h1, f); + var etran0 = new ExpressionTranslator(this, Predef, h0, f); + var etran1 = new ExpressionTranslator(this, Predef, h1, f); Bpl.Expr wellFormed = BplAnd( FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran0.HeapExpr), FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran1.HeapExpr)); - Bpl.Expr o; var oVar = BplBoundVar("$o", predef.RefType, out o); - Bpl.Expr field; var fieldVar = BplBoundVar("$f", predef.FieldName(f.tok), out field); - Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null); + Bpl.Expr o; var oVar = BplBoundVar("$o", Predef.RefType, out o); + Bpl.Expr field; var fieldVar = BplBoundVar("$f", Predef.FieldName(f.tok), out field); + Bpl.Expr oNotNull = Bpl.Expr.Neq(o, Predef.Null); Bpl.Expr oNotNullAlloced = oNotNull; Bpl.Expr unchanged = Bpl.Expr.Eq(ReadHeap(f.tok, h0, o, field), ReadHeap(f.tok, h1, o, field)); @@ -917,7 +917,7 @@ void AddFrameAxiom(Function f) { var f0argsCanCall = new List(tyexprs); var f1argsCanCall = new List(tyexprs); if (f.IsFuelAware()) { - Bpl.Expr s; var sV = BplBoundVar("$ly", predef.LayerType, out s); + Bpl.Expr s; var sV = BplBoundVar("$ly", Predef.LayerType, out s); bvars.Add(sV); f0args.Add(s); f1args.Add(s); // but don't add to f0argsCanCall or f1argsCanCall } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs index e09f4617c86..6201c0f9c31 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs @@ -60,7 +60,7 @@ void AddIteratorSpecAndBody(IteratorDecl iter) { Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { Contract.Requires(iter != null); Contract.Requires(kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Requires(currentModule == null && codeContext == null); Contract.Ensures(currentModule == null && codeContext == null); Contract.Ensures(Contract.Result() != null); @@ -69,7 +69,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { currentModule = iter.EnclosingModuleDefinition; codeContext = iter; - var etran = new ExpressionTranslator(this, predef, iter.tok, iter); + var etran = new ExpressionTranslator(this, Predef, iter.tok, iter); var inParams = new List(); GenerateMethodParametersChoose(iter.tok, iter, kind, @@ -147,7 +147,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { Contract.Assert(proc.OutParams.Count == 0); var builder = new BoogieStmtListBuilder(this, options, new BodyTranslationContext(false)); - var etran = new ExpressionTranslator(this, predef, iter.tok, iter); + var etran = new ExpressionTranslator(this, Predef, iter.tok, iter); // Don't do reads checks since iterator reads clauses mean something else. // See comment inside GenerateIteratorImplPrelude(). etran = etran.WithReadsFrame(null); @@ -202,7 +202,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { } // save the heap (representing the state where yield-requires holds): $_OldIterHeap := Heap; - var oldIterHeap = localVariables.GetOrAdd(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$_OldIterHeap", predef.HeapType))); + var oldIterHeap = localVariables.GetOrAdd(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$_OldIterHeap", Predef.HeapType))); builder.Add(Bpl.Cmd.SimpleAssign(iter.tok, new Bpl.IdentifierExpr(iter.tok, oldIterHeap), etran.HeapExpr)); // simulate a modifies this, this._modifies, this._new; var nw = new MemberSelectExpr(iter.tok, th, iter.Member_New); @@ -211,7 +211,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { new List())); // assume the implicit postconditions promised by MoveNext: // assume fresh(_new - old(_new)); - var yeEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType), iter); + var yeEtran = new ExpressionTranslator(this, Predef, etran.HeapExpr, new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", Predef.HeapType), iter); var old_nw = new OldExpr(iter.tok, nw); old_nw.Type = nw.Type; // resolve here var setDiff = new BinaryExpr(iter.tok, BinaryExpr.Opcode.Sub, nw, old_nw); @@ -266,7 +266,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { Contract.Requires(iter != null); Contract.Requires(proc != null); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); Contract.Requires(iter.Body != null); Contract.Requires(currentModule == null && codeContext == null && yieldCountVariable == null && _tmpIEs.Count == 0); Contract.Ensures(currentModule == null && codeContext == null && yieldCountVariable == null && _tmpIEs.Count == 0); @@ -280,7 +280,7 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { Contract.Assert(proc.OutParams.Count == 0); var builder = new BoogieStmtListBuilder(this, options, new BodyTranslationContext(iter.ContainsHide)); - var etran = new ExpressionTranslator(this, predef, iter.tok, iter); + var etran = new ExpressionTranslator(this, Predef, iter.tok, iter); // Don't do reads checks since iterator reads clauses mean something else. // See comment inside GenerateIteratorImplPrelude(). etran = etran.WithReadsFrame(null); @@ -303,15 +303,15 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { } // add the _yieldCount variable, and assume its initial value to be 0 yieldCountVariable = (Bpl.LocalVariable)localVariables.GetOrAdd(new Bpl.LocalVariable(iter.tok, - new Bpl.TypedIdent(iter.tok, iter.YieldCountVariable.AssignUniqueName(currentDeclaration.IdGenerator), TrType(iter.YieldCountVariable.Type)))); + new Bpl.TypedIdent(iter.tok, iter.YieldCountVariable.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(iter.YieldCountVariable.Type)))); yieldCountVariable.TypedIdent.WhereExpr = YieldCountAssumption(iter, etran); // by doing this after setting "yieldCountVariable", the variable can be used by YieldCountAssumption builder.Add(TrAssumeCmd(iter.tok, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable), Bpl.Expr.Literal(0)))); // add a variable $_OldIterHeap - var oih = new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", predef.HeapType); + var oih = new Bpl.IdentifierExpr(iter.tok, "$_OldIterHeap", Predef.HeapType); Bpl.Expr wh = BplAnd( FunctionCall(iter.tok, BuiltinFunction.IsGoodHeap, null, oih), HeapSucc(oih, etran.HeapExpr)); - localVariables.GetOrAdd(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$_OldIterHeap", predef.HeapType, wh))); + localVariables.GetOrAdd(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, "$_OldIterHeap", Predef.HeapType, wh))); // do an initial YieldHavoc YieldHavoc(iter.tok, iter, builder, etran); @@ -341,7 +341,7 @@ Bpl.Expr YieldCountAssumption(IteratorDecl iter, ExpressionTranslator etran) { wh = BplAnd(wh, Bpl.Expr.Eq(new Bpl.IdentifierExpr(iter.tok, yieldCountVariable), FunctionCall(iter.tok, BuiltinFunction.SeqLength, null, ApplyUnbox(iter.tok, ReadHeap(iter.tok, etran.HeapExpr, - new Bpl.IdentifierExpr(iter.tok, etran.This, predef.RefType), + new Bpl.IdentifierExpr(iter.tok, etran.This, Predef.RefType), new Bpl.IdentifierExpr(iter.tok, GetField(ys))), TrType(ys.Type))))); } return wh; @@ -354,7 +354,7 @@ void GenerateIteratorImplPrelude(IteratorDecl iter, List inParams, Lis Contract.Requires(outParams != null); Contract.Requires(builder != null); Contract.Requires(localVariables != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); // set up the information used to verify the method's modifies clause var iteratorFrame = new List(); @@ -394,7 +394,7 @@ void YieldHavoc(IToken tok, IteratorDecl iter, BoogieStmtListBuilder builder, Ex builder.Add(TrAssumeCmdWithDependencies(etran, tok, p.E, "iterator yield-requires clause")); } // $_OldIterHeap := Heap; - builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, "$_OldIterHeap", predef.HeapType), etran.HeapExpr)); + builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, "$_OldIterHeap", Predef.HeapType), etran.HeapExpr)); } } } diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs b/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs index 15e39c0850a..2a0c1b15226 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs @@ -115,7 +115,7 @@ public void TrLetExprPieces(LetExpr let, out List lhss, out Lis rhss = new List(); foreach (var v in let.BoundVars) { var rhs = substMap[v]; // this should succeed (that is, "v" is in "substMap"), because the AddCasePatternVarSubstitutions calls above should have added a mapping for each bound variable in let.BoundVars - var bv = BplBoundVar(v.AssignUniqueName(BoogieGenerator.currentDeclaration.IdGenerator), BoogieGenerator.TrType(v.Type), out var bvIde); + var bv = BplBoundVar(v.AssignUniqueName(BoogieGenerator.CurrentDeclaration.IdGenerator), BoogieGenerator.TrType(v.Type), out var bvIde); lhss.Add(bv); rhss.Add(TrExpr(rhs)); } @@ -174,7 +174,7 @@ public Expression LetDesugaring(LetExpr e) { ComputeFreeTypeVariables(e.RHSs[0], FTVs); info = new LetSuchThatExprInfo(e.tok, BoogieGenerator.letSuchThatExprInfo.Count, FVs.ToList(), FTVs.ToList(), usesHeap, - usesOldHeap, FVsHeapAt, usesThis, BoogieGenerator.currentDeclaration); + usesOldHeap, FVsHeapAt, usesThis, BoogieGenerator.CurrentDeclaration); BoogieGenerator.letSuchThatExprInfo.Add(e, info); } @@ -375,7 +375,7 @@ public Bpl.Expr CanCallFunctionCall(BoogieGenerator boogieGenerator, ExpressionT foreach (var heapAtLabel in UsesHeapAt) { Bpl.Expr ve; var bv = BplBoundVar("$Heap_at_" + heapAtLabel.AssignUniqueId(boogieGenerator.CurrentIdGenerator), - boogieGenerator.predef.HeapType, out ve); + boogieGenerator.Predef.HeapType, out ve); gExprs.Add(ve); } @@ -397,7 +397,7 @@ public string CanCallFunctionName() { public Bpl.Expr HeapExpr(BoogieGenerator boogieGenerator, bool old) { Contract.Requires(boogieGenerator != null); - return new Bpl.IdentifierExpr(Tok, old ? "$heap$old" : "$heap", boogieGenerator.predef.HeapType); + return new Bpl.IdentifierExpr(Tok, old ? "$heap$old" : "$heap", boogieGenerator.Predef.HeapType); } /// @@ -412,10 +412,10 @@ public List GAsVars(BoogieGenerator boogieGenerator, bool wantFormals, Contract.Requires(boogieGenerator != null); var vv = new List(); // first, add the type variables - vv.AddRange(Map(FTVs, tp => NewVar(NameTypeParam(tp), boogieGenerator.predef.Ty, wantFormals))); + vv.AddRange(Map(FTVs, tp => NewVar(NameTypeParam(tp), boogieGenerator.Predef.Ty, wantFormals))); typeAntecedents = Bpl.Expr.True; if (UsesHeap) { - var nv = NewVar("$heap", boogieGenerator.predef.HeapType, wantFormals); + var nv = NewVar("$heap", boogieGenerator.Predef.HeapType, wantFormals); vv.Add(nv); if (etran != null) { var isGoodHeap = boogieGenerator.FunctionCall(Tok, BuiltinFunction.IsGoodHeap, null, @@ -425,7 +425,7 @@ public List GAsVars(BoogieGenerator boogieGenerator, bool wantFormals, } if (UsesOldHeap) { - var nv = NewVar("$heap$old", boogieGenerator.predef.HeapType, wantFormals); + var nv = NewVar("$heap$old", boogieGenerator.Predef.HeapType, wantFormals); vv.Add(nv); if (etran != null) { var isGoodHeap = boogieGenerator.FunctionCall(Tok, BuiltinFunction.IsGoodHeap, null, @@ -436,7 +436,7 @@ public List GAsVars(BoogieGenerator boogieGenerator, bool wantFormals, foreach (var heapAtLabel in UsesHeapAt) { var nv = NewVar("$Heap_at_" + heapAtLabel.AssignUniqueId(boogieGenerator.CurrentIdGenerator), - boogieGenerator.predef.HeapType, wantFormals); + boogieGenerator.Predef.HeapType, wantFormals); vv.Add(nv); if (etran != null) { // TODO: It's not clear to me that $IsGoodHeap predicates are needed for these axioms. (Same comment applies above for $heap$old.) diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs index 49cba315060..a8d7ae3b4cc 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Methods.cs @@ -11,7 +11,7 @@ namespace Microsoft.Dafny { public partial class BoogieGenerator { void AddClassMembers(TopLevelDeclWithMembers c, bool includeAllMethods, bool includeInformationAboutType) { - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); Contract.Requires(c != null); Contract.Ensures(fuelContext == Contract.OldValue(fuelContext)); Contract.Assert(VisibleInScope(c)); @@ -29,7 +29,7 @@ void AddClassMembers(TopLevelDeclWithMembers c, bool includeAllMethods, bool inc if (c is TraitDecl) { //this adds: function implements$J(Ty, typeArgs): bool; - var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, "ty", predef.Ty), true); + var arg_ref = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, "ty", Predef.Ty), true); var vars = new List { arg_ref }; vars.AddRange(MkTyParamFormals(GetTypeParams(c), false)); var res = new Bpl.Formal(c.tok, new Bpl.TypedIdent(c.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false); @@ -42,7 +42,7 @@ void AddClassMembers(TopLevelDeclWithMembers c, bool includeAllMethods, bool inc foreach (MemberDecl member in c.Members.FindAll(VisibleInScope)) { Contract.Assert(isAllocContext == null); - currentDeclaration = member; + CurrentDeclaration = member; if (!filterOnlyMembers || member.HasUserAttribute("only", out _)) { SetAssertionOnlyFilter(member); } else { @@ -67,7 +67,7 @@ void AddClassMembers(TopLevelDeclWithMembers c, bool includeAllMethods, bool inc sink.AddTopLevelDeclaration(fieldDeclaration); } else { fieldDeclaration = GetReadonlyField(f); - if (fieldDeclaration != predef.ArrayLength) { + if (fieldDeclaration != Predef.ArrayLength) { sink.AddTopLevelDeclaration(fieldDeclaration); } } @@ -99,16 +99,16 @@ private void AddIsAndIsAllocForReferenceType(ClassLikeDecl c) { MapM(Bools, is_alloc => { var vars = MkTyParamBinders(GetTypeParams(c), out var tyexprs); - var o = BplBoundVar("$o", predef.RefType, vars); + var o = BplBoundVar("$o", Predef.RefType, vars); Bpl.Expr body, is_o; - Bpl.Expr o_null = Bpl.Expr.Eq(o, predef.Null); + Bpl.Expr o_null = Bpl.Expr.Eq(o, Predef.Null); Bpl.Expr o_ty = ClassTyCon(c, tyexprs); string name; if (is_alloc) { name = $"$IsAlloc axiom for {c.WhatKind} {c}"; - var h = BplBoundVar("$h", predef.HeapType, vars); + var h = BplBoundVar("$h", Predef.HeapType, vars); // $IsAlloc(o, ..) is_o = MkIsAlloc(o, o_ty, h); body = BplIff(is_o, BplOr(o_null, IsAlloced(c.tok, h, o))); @@ -217,14 +217,14 @@ private void AddAllocationAxiom(Boogie.Declaration fieldDeclaration, Field f, To Contract.Requires(c != null); // IFF you're adding the array axioms, then the field should be null Contract.Requires(is_array == (f == null)); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); Bpl.Expr heightAntecedent = Bpl.Expr.True; if (f is ConstantField) { var cf = (ConstantField)f; AddWellformednessCheck(cf); if (InVerificationScope(cf)) { - var etran = new ExpressionTranslator(this, predef, f.tok, null); + var etran = new ExpressionTranslator(this, Predef, f.tok, null); heightAntecedent = Bpl.Expr.Lt(Bpl.Expr.Literal(cf.EnclosingModule.CallGraph.GetSCCRepresentativePredecessorCount(cf)), etran.FunctionContextHeight()); } } @@ -273,7 +273,7 @@ private void AddInstanceFieldAllocationAxioms(Bpl.Declaration fieldDeclaration, // This is the typical case (that is, f is not a static const field) - var hVar = BplBoundVar("$h", predef.HeapType, out var h); + var hVar = BplBoundVar("$h", Predef.HeapType, out var h); var oVar = BplBoundVar("$o", TrType(ModuleResolver.GetThisType(c.tok, c)), out var o); Bpl.Expr o_ty; // to hold TClassA(G) @@ -326,7 +326,7 @@ private void AddInstanceFieldAllocationAxioms(Bpl.Declaration fieldDeclaration, // generate h[o,f] var ty = TrType(f.Type); oDotF = ReadHeap(c.tok, h, o, new Bpl.IdentifierExpr(c.tok, GetField(f))); - oDotF = ty == predef.BoxType ? oDotF : ApplyUnbox(c.tok, oDotF, ty); + oDotF = ty == Predef.BoxType ? oDotF : ApplyUnbox(c.tok, oDotF, ty); bvsTypeAxiom.Add(hVar); bvsTypeAxiom.Add(oVar); bvsAllocationAxiom.Add(hVar); @@ -353,7 +353,7 @@ private void AddInstanceFieldAllocationAxioms(Bpl.Declaration fieldDeclaration, Bpl.Expr is_o = BplAnd( ReceiverNotNull(o), - !o.Type.Equals(predef.RefType) || c is TraitDecl + !o.Type.Equals(Predef.RefType) || c is TraitDecl ? MkIs(o, o_ty, ModeledAsBoxType(ModuleResolver.GetThisType(c.tok, c))) // $Is(o, ..) : DType(o, o_ty)); // dtype(o) == o_ty ante = BplAnd(ante, is_o); @@ -454,7 +454,7 @@ private void AddStaticConstFieldAllocationAxiom(Boogie.Declaration fieldDeclarat AddOtherDefinition(fieldDeclaration, isAxiom); { - var hVar = BplBoundVar("$h", predef.HeapType, out var h); + var hVar = BplBoundVar("$h", Predef.HeapType, out var h); bvsAllocationAxiom.Add(hVar); var isGoodHeap = FunctionCall(c.tok, BuiltinFunction.IsGoodHeap, null, h); var isalloc_hf = MkIsAlloc(oDotF, f.Type, h); // $IsAlloc(h[o, f], ..) @@ -526,7 +526,7 @@ private void AddClassMember_Function(Function f) { private void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc) { Contract.Requires(m != null); Contract.Requires(proc != null); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); Contract.Requires(wellformednessProc || m.Body != null); Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null); Contract.Ensures(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext == null); @@ -541,7 +541,7 @@ private void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc var builder = new BoogieStmtListBuilder(this, options, new BodyTranslationContext(m.ContainsHide)); builder.Add(new CommentCmd("AddMethodImpl: " + m + ", " + proc)); - var etran = new ExpressionTranslator(this, predef, m.tok, + var etran = new ExpressionTranslator(this, Predef, m.tok, m.IsByMethod ? m.FunctionFromWhichThisIsByMethodDecl : m); // Only do reads checks for methods, not lemmas // (which aren't allowed to declare frames and don't check reads and writes against them). @@ -814,7 +814,7 @@ private StmtList TrMethodBody(Method m, BoogieStmtListBuilder builder, Variables private void AddMethodOverrideCheckImpl(Method m, Boogie.Procedure proc) { Contract.Requires(m != null); Contract.Requires(proc != null); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); Contract.Requires(m.OverriddenMethod != null); Contract.Requires(m.Ins.Count == m.OverriddenMethod.Ins.Count); Contract.Requires(m.Outs.Count == m.OverriddenMethod.Outs.Count); @@ -831,7 +831,7 @@ private void AddMethodOverrideCheckImpl(Method m, Boogie.Procedure proc) { List outParams = Boogie.Formal.StripWhereClauses(proc.OutParams); var builder = new BoogieStmtListBuilder(this, options, new BodyTranslationContext(false)); - var etran = new ExpressionTranslator(this, predef, m.tok, m); + var etran = new ExpressionTranslator(this, Predef, m.tok, m); var localVariables = new Variables(); InitializeFuelConstant(m.tok, builder, etran); @@ -840,8 +840,8 @@ private void AddMethodOverrideCheckImpl(Method m, Boogie.Procedure proc) { if (m is TwoStateLemma) { // $Heap := current$Heap; - var heap = ExpressionTranslator.HeapIdentifierExpr(predef, m.tok); - builder.Add(Boogie.Cmd.SimpleAssign(m.tok, heap, new Boogie.IdentifierExpr(m.tok, "current$Heap", predef.HeapType))); + var heap = ExpressionTranslator.HeapIdentifierExpr(Predef, m.tok); + builder.Add(Boogie.Cmd.SimpleAssign(m.tok, heap, new Boogie.IdentifierExpr(m.tok, "current$Heap", Predef.HeapType))); } @@ -914,7 +914,7 @@ private void HavocMethodFrameLocations(Method m, BoogieStmtListBuilder builder, private void AddFunctionOverrideCheckImpl(Function f) { Contract.Requires(f != null); Contract.Requires(f.EnclosingClass is TopLevelDeclWithMembers); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); Contract.Requires(f.OverriddenFunction != null); Contract.Requires(f.Ins.Count == f.OverriddenFunction.Ins.Count); Contract.Requires(currentModule == null && codeContext == null && _tmpIEs.Count == 0 && isAllocContext != null); @@ -929,19 +929,19 @@ private void AddFunctionOverrideCheckImpl(Function f) { Boogie.Expr prevHeap = null; Boogie.Expr currHeap = null; - var ordinaryEtran = new ExpressionTranslator(this, predef, f.tok, f); + var ordinaryEtran = new ExpressionTranslator(this, Predef, f.tok, f); ExpressionTranslator etran; var inParams_Heap = new List(); if (f is TwoStateFunction) { - var prevHeapVar = new Boogie.Formal(f.tok, new Boogie.TypedIdent(f.tok, "previous$Heap", predef.HeapType), true); + var prevHeapVar = new Boogie.Formal(f.tok, new Boogie.TypedIdent(f.tok, "previous$Heap", Predef.HeapType), true); inParams_Heap.Add(prevHeapVar); prevHeap = new Boogie.IdentifierExpr(f.tok, prevHeapVar); if (f.ReadsHeap) { - var currHeapVar = new Boogie.Formal(f.tok, new Boogie.TypedIdent(f.tok, "current$Heap", predef.HeapType), true); + var currHeapVar = new Boogie.Formal(f.tok, new Boogie.TypedIdent(f.tok, "current$Heap", Predef.HeapType), true); inParams_Heap.Add(currHeapVar); currHeap = new Boogie.IdentifierExpr(f.tok, currHeapVar); } - etran = new ExpressionTranslator(this, predef, currHeap, prevHeap, f); + etran = new ExpressionTranslator(this, Predef, currHeap, prevHeap, f); } else { etran = ordinaryEtran; } @@ -1155,7 +1155,7 @@ private void AddOverrideCheckTypeArgumentInstantiations(MemberDecl member, Boogi } var typeMap = GetTypeArgumentSubstitutionMap(overriddenMember, member); foreach (var tp in Util.Concat(overriddenMember.EnclosingClass.TypeArgs, overriddenTypeParameters)) { - localVariables.GetOrAdd(BplLocalVar(NameTypeParam(tp), predef.Ty, out var lhs)); + localVariables.GetOrAdd(BplLocalVar(NameTypeParam(tp), Predef.Ty, out var lhs)); var rhs = TypeToTy(typeMap[tp]); builder.Add(new Boogie.AssumeCmd(tp.tok, Boogie.Expr.Eq(lhs, rhs))); } @@ -1184,11 +1184,11 @@ private void AddFunctionOverrideSubsetChk(Function func, BoogieStmtListBuilder b Contract.Assert(traitFrame.Type != null); // follows from the postcondition of ReadsFrame var frame = localVariables.GetOrAdd(new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, null ?? traitFrame.Name, traitFrame.Type))); // $_ReadsFrame := (lambda $o: ref, $f: Field :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause); - Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType)); + Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", Predef.RefType)); Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar); - Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok))); + Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", Predef.FieldName(tok))); Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar); - Bpl.Expr ante = BplAnd(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o)); + Bpl.Expr ante = BplAnd(Bpl.Expr.Neq(o, Predef.Null), etran.IsAlloced(tok, o)); Bpl.Expr consequent = InRWClause(tok, o, f, traitFrameExps, etran, null, null); Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new List(), new List { oVar, fVar }, null, BplImp(ante, consequent)); @@ -1250,7 +1250,7 @@ private void AddFunctionOverrideReqsChk(Function f, BoogieStmtListBuilder builde private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFunction) { Contract.Requires(f != null); Contract.Requires(overridingFunction != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Requires(f.EnclosingClass != null); Contract.Requires(!f.IsStatic); Contract.Requires(overridingFunction.EnclosingClass is TopLevelDeclWithMembers); @@ -1261,15 +1261,15 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti ExpressionTranslator etran; Boogie.BoundVariable bvPrevHeap = null; if (f is TwoStateFunction) { - bvPrevHeap = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, "$prevHeap", predef.HeapType)); - etran = new ExpressionTranslator(this, predef, - f.ReadsHeap ? new Boogie.IdentifierExpr(f.tok, predef.HeapVarName, predef.HeapType) : null, + bvPrevHeap = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, "$prevHeap", Predef.HeapType)); + etran = new ExpressionTranslator(this, Predef, + f.ReadsHeap ? new Boogie.IdentifierExpr(f.tok, Predef.HeapVarName, Predef.HeapType) : null, new Boogie.IdentifierExpr(f.tok, bvPrevHeap), f); } else if (readsHeap) { - etran = new ExpressionTranslator(this, predef, f.tok, f); + etran = new ExpressionTranslator(this, Predef, f.tok, f); } else { - etran = new ExpressionTranslator(this, predef, (Boogie.Expr)null, f); + etran = new ExpressionTranslator(this, Predef, (Boogie.Expr)null, f); } // "forallFormals" is built to hold the bound variables of the quantification @@ -1291,14 +1291,14 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti // Add the fuel argument if (f.IsFuelAware()) { Contract.Assert(overridingFunction.IsFuelAware()); // f.IsFuelAware() ==> overridingFunction.IsFuelAware() - var fuel = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, "$fuel", predef.LayerType)); + var fuel = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, "$fuel", Predef.LayerType)); forallFormals.Add(fuel); layer = new Boogie.IdentifierExpr(f.tok, fuel); argsJF.Add(layer); } else if (overridingFunction.IsFuelAware()) { // We can't use a bound variable $fuel, because then one of the triggers won't be mentioning this $fuel. // Instead, we do the next best thing: use the literal $LZ. - layer = new Boogie.IdentifierExpr(f.tok, "$LZ", predef.LayerType); // $LZ + layer = new Boogie.IdentifierExpr(f.tok, "$LZ", Predef.LayerType); // $LZ } if (f.IsOpaque || f.IsMadeImplicitlyOpaque(options)) { @@ -1319,7 +1319,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti moreArgsCF.Add(etran.Old.HeapExpr); } if (f.ReadsHeap || overridingFunction.ReadsHeap) { - var heap = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType)); + var heap = new Boogie.BoundVariable(f.tok, new Boogie.TypedIdent(f.tok, Predef.HeapVarName, Predef.HeapType)); forallFormals.Add(heap); if (f.ReadsHeap) { argsJF.Add(new Boogie.IdentifierExpr(f.tok, heap)); @@ -1346,7 +1346,7 @@ private Boogie.Axiom FunctionOverrideAxiom(Function f, Function overridingFuncti var typeMap = GetTypeArgumentSubstitutionMap(f, overridingFunction); foreach (Formal p in f.Ins) { var pType = p.Type.Subst(typeMap); - var bv = new Boogie.BoundVariable(p.tok, new Boogie.TypedIdent(p.tok, p.AssignUniqueName(currentDeclaration.IdGenerator), TrType(pType))); + var bv = new Boogie.BoundVariable(p.tok, new Boogie.TypedIdent(p.tok, p.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(pType))); forallFormals.Add(bv); var jfArg = new Boogie.IdentifierExpr(p.tok, bv); argsJF.Add(ModeledAsBoxType(p.Type) ? BoxIfNotNormallyBoxed(p.tok, jfArg, pType) : jfArg); @@ -1624,11 +1624,11 @@ private void AddMethodOverrideFrameSubsetChk(Method m, bool isModifies, BoogieSt var kv = etran.TrAttributes(m.Attributes, null); var tok = m.tok; - var oVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$o", predef.RefType)); + var oVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$o", Predef.RefType)); var o = new Boogie.IdentifierExpr(tok, oVar); - var fVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$f", predef.FieldName(tok))); + var fVar = new Boogie.BoundVariable(tok, new Boogie.TypedIdent(tok, "$f", Predef.FieldName(tok))); var f = new Boogie.IdentifierExpr(tok, fVar); - var ante = BplAnd(Boogie.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o)); + var ante = BplAnd(Boogie.Expr.Neq(o, Predef.Null), etran.IsAlloced(tok, o)); // emit: assert (forall o: ref, f: Field :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> $_Frame[o,f]); var oInCallee = InRWClause(tok, o, f, classFrameExps, etran, null, null); @@ -1687,7 +1687,7 @@ private void ResetAssertionOnlyFilter() { private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { Contract.Requires(m != null); Contract.Requires(m.EnclosingClass != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Requires(currentModule == null && codeContext == null && isAllocContext == null); Contract.Ensures(currentModule == null && codeContext == null && isAllocContext == null); Contract.Ensures(Contract.Result() != null); @@ -1699,18 +1699,18 @@ private Boogie.Procedure AddMethod(Method m, MethodTranslationKind kind) { isAllocContext = new IsAllocContext(options, m.IsGhost); Boogie.Expr prevHeap = null; Boogie.Expr currHeap = null; - var ordinaryEtran = new ExpressionTranslator(this, predef, m.tok, m); + var ordinaryEtran = new ExpressionTranslator(this, Predef, m.tok, m); ExpressionTranslator etran; var inParams = new List(); var bodyKind = kind == MethodTranslationKind.SpecWellformedness || kind == MethodTranslationKind.Implementation; if (m is TwoStateLemma) { - var prevHeapVar = new Boogie.Formal(m.tok, new Boogie.TypedIdent(m.tok, "previous$Heap", predef.HeapType), true); - var currHeapVar = new Boogie.Formal(m.tok, new Boogie.TypedIdent(m.tok, "current$Heap", predef.HeapType), true); + var prevHeapVar = new Boogie.Formal(m.tok, new Boogie.TypedIdent(m.tok, "previous$Heap", Predef.HeapType), true); + var currHeapVar = new Boogie.Formal(m.tok, new Boogie.TypedIdent(m.tok, "current$Heap", Predef.HeapType), true); inParams.Add(prevHeapVar); inParams.Add(currHeapVar); prevHeap = new Boogie.IdentifierExpr(m.tok, prevHeapVar); currHeap = new Boogie.IdentifierExpr(m.tok, currHeapVar); - etran = new ExpressionTranslator(this, predef, currHeap, prevHeap, m); + etran = new ExpressionTranslator(this, Predef, currHeap, prevHeap, m); } else { etran = ordinaryEtran; } @@ -1901,7 +1901,7 @@ public void TypeBoundAxiomExpressions(IToken tok, List bvarsTypePa // $IsBox(bx, Bound0) && $IsBox(bx, Bound1) && ...); var vars = new List(); vars.AddRange(bvarsTypeParameters); - var bx = BplBoundVar("bx", predef.BoxType, vars); + var bx = BplBoundVar("bx", Predef.BoxType, vars); var isBox = MkIs(bx, TypeToTy(type), true); Bpl.Expr bounds = Bpl.Expr.True; foreach (var typeBound in typeBounds) { @@ -1919,8 +1919,8 @@ public void TypeBoundAxiomExpressions(IToken tok, List bvarsTypePa // $IsAllocBox(bx, Bound0, $h) && $IsAllocBox(bx, Bound1, $h) && ...); var vars = new List(); vars.AddRange(bvarsTypeParameters); - var bx = BplBoundVar("bx", predef.BoxType, vars); - var heap = BplBoundVar("$h", predef.HeapType, vars); + var bx = BplBoundVar("bx", Predef.BoxType, vars); + var heap = BplBoundVar("$h", Predef.HeapType, vars); var isGoodHeap = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, heap); var isAllocBox = MkIsAlloc(bx, TypeToTy(type), heap, true); Bpl.Expr bounds = Bpl.Expr.True; diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Reveal.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Reveal.cs index 53edc92ed6e..8d70ebbd9d2 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Reveal.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Reveal.cs @@ -27,7 +27,7 @@ Expr TrStmtSideEffect(Expr e, Statement stmt, ExpressionTranslator etran) { if (fuelConstant != null) { Bpl.Expr startFuel = fuelConstant.startFuel; Bpl.Expr startFuelAssert = fuelConstant.startFuelAssert; - Bpl.Expr moreFuel_expr = fuelConstant.MoreFuel(sink, predef, f.IdGenerator); + Bpl.Expr moreFuel_expr = fuelConstant.MoreFuel(sink, Predef, f.IdGenerator); Bpl.Expr layer = etran.layerInterCluster.LayerN(1, moreFuel_expr); Bpl.Expr layerAssert = etran.layerInterCluster.LayerN(2, moreFuel_expr); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs b/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs index e3041c4e1bf..d16ed5d9303 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs @@ -179,7 +179,7 @@ bool TrSplitExpr(BodyTranslationContext context, Expression expr, List bvs; List args; CreateBoundVariables(ctor.Formals, out bvs, out args); - Bpl.Expr ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); + Bpl.Expr ct = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); // (exists args :: args-have-the-expected-types && ct(args) == expr) Bpl.Expr q = Bpl.Expr.Binary(ctor.tok, BinaryOperator.Opcode.Eq, ct, expr); if (bvs.Count != 0) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs index e84f9579e45..d014a32deef 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Types.cs @@ -33,9 +33,9 @@ private void AddArrowTypeAxioms(ArrowTypeDecl ad) { var tok = ad.tok; // [Heap, Box, ..., Box] - var map_args = Cons(predef.HeapType, Map(Enumerable.Range(0, arity), i => predef.BoxType)); + var map_args = Cons(Predef.HeapType, Map(Enumerable.Range(0, arity), i => Predef.BoxType)); // [Heap, Box, ..., Box] Box - var apply_ty = new Bpl.MapType(tok, new List(), map_args, predef.BoxType); + var apply_ty = new Bpl.MapType(tok, new List(), map_args, Predef.BoxType); // [Heap, Box, ..., Box] Bool var requires_ty = new Bpl.MapType(tok, new List(), map_args, Bpl.Type.Bool); // Set Box @@ -45,7 +45,7 @@ private void AddArrowTypeAxioms(ArrowTypeDecl ad) { { // function HandleN([Heap, Box, ..., Box] Box, [Heap, Box, ..., Box] Bool) : HandleType - var res = BplFormalVar(null, predef.HandleType, true); + var res = BplFormalVar(null, Predef.HandleType, true); var arg = new List { BplFormalVar(null, apply_ty, true), BplFormalVar(null, requires_ty, true), @@ -57,10 +57,10 @@ private void AddArrowTypeAxioms(ArrowTypeDecl ad) { Action SelectorFunction = (dafnyFunction, name, t) => { var args = new List(); - MapM(Enumerable.Range(0, arity + 1), i => args.Add(BplFormalVar(null, predef.Ty, true))); - args.Add(BplFormalVar(null, predef.HeapType, true)); - args.Add(BplFormalVar(null, predef.HandleType, true)); - MapM(Enumerable.Range(0, arity), i => args.Add(BplFormalVar(null, predef.BoxType, true))); + MapM(Enumerable.Range(0, arity + 1), i => args.Add(BplFormalVar(null, Predef.Ty, true))); + args.Add(BplFormalVar(null, Predef.HeapType, true)); + args.Add(BplFormalVar(null, Predef.HandleType, true)); + MapM(Enumerable.Range(0, arity), i => args.Add(BplFormalVar(null, Predef.BoxType, true))); var boogieFunction = new Bpl.Function(Token.NoToken, name, args, BplFormalVar(null, t, false)); if (dafnyFunction != null) { declarationMapping[dafnyFunction] = boogieFunction; @@ -70,7 +70,7 @@ private void AddArrowTypeAxioms(ArrowTypeDecl ad) { // function ApplyN(Ty, ... Ty, HandleType, Heap, Box, ..., Box) : Box if (arity != 1) { // Apply1 is already declared in DafnyPrelude.bpl - SelectorFunction(null, Apply(arity), predef.BoxType); + SelectorFunction(null, Apply(arity), Predef.BoxType); } // function RequiresN(Ty, ... Ty, HandleType, Heap, Box, ..., Box) : Bool SelectorFunction(ad.Requires, Requires(arity), Bpl.Type.Bool); @@ -86,9 +86,9 @@ private void AddArrowTypeAxioms(ArrowTypeDecl ad) { Contract.Assert((precond == null) == (precondTy == null)); var bvars = new List(); - var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, predef.Ty, bvars)); + var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, Predef.Ty, bvars)); - var heap = BplBoundVar("heap", predef.HeapType, bvars); + var heap = BplBoundVar("heap", Predef.HeapType, bvars); var handleargs = new List { BplBoundVar("h", apply_ty, bvars), @@ -96,9 +96,9 @@ private void AddArrowTypeAxioms(ArrowTypeDecl ad) { BplBoundVar("rd", reads_ty, bvars) }; - var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, predef.BoxType, bvars)); + var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, Predef.BoxType, bvars)); - var lhsargs = Concat(types, Cons(heap, Cons(FunctionCall(tok, Handle(arity), predef.HandleType, handleargs), boxes))); + var lhsargs = Concat(types, Cons(heap, Cons(FunctionCall(tok, Handle(arity), Predef.HandleType, handleargs), boxes))); Bpl.Expr lhs = FunctionCall(tok, selector, selectorTy, lhsargs); Func pre = x => x; if (precond != null) { @@ -109,7 +109,7 @@ private void AddArrowTypeAxioms(ArrowTypeDecl ad) { Cons(new Bpl.IdentifierExpr(tok, selectorVar, selectorVarTy), Cons(heap, boxes))); Func op = Bpl.Expr.Eq; if (selectorVar == "rd") { - var bx = BplBoundVar("bx", predef.BoxType, bvars); + var bx = BplBoundVar("bx", Predef.BoxType, bvars); lhs = Bpl.Expr.SelectTok(tok, lhs, bx); rhs = Bpl.Expr.SelectTok(tok, rhs, bx); // op = BplImp; @@ -120,7 +120,7 @@ private void AddArrowTypeAxioms(ArrowTypeDecl ad) { AddOtherDefinition(GetOrCreateTypeConstructor(ad), new Axiom(tok, BplForall(bvars, BplTrigger(lhs), op(lhs, rhs)))); }; - SelectorSemantics(Apply(arity), predef.BoxType, "h", apply_ty, Requires(arity), requires_ty); + SelectorSemantics(Apply(arity), Predef.BoxType, "h", apply_ty, Requires(arity), requires_ty); SelectorSemantics(Requires(arity), Bpl.Type.Bool, "r", requires_ty, null, null); SelectorSemantics(Reads(arity), objset_ty, "rd", reads_ty, null, null); @@ -132,13 +132,13 @@ private void AddArrowTypeAxioms(ArrowTypeDecl ad) { var formals = new List(); var rhsargs = new List(); - MapM(Enumerable.Range(0, arity + 1), i => rhsargs.Add(BplFormalVar("t" + i, predef.Ty, true, formals))); + MapM(Enumerable.Range(0, arity + 1), i => rhsargs.Add(BplFormalVar("t" + i, Predef.Ty, true, formals))); - var heap = BplFormalVar("heap", predef.HeapType, true, formals); + var heap = BplFormalVar("heap", Predef.HeapType, true, formals); rhsargs.Add(heap); - rhsargs.Add(BplFormalVar("f", predef.HandleType, true, formals)); + rhsargs.Add(BplFormalVar("f", Predef.HandleType, true, formals)); - MapM(Enumerable.Range(0, arity), i => rhsargs.Add(BplFormalVar("bx" + i, predef.BoxType, true, formals))); + MapM(Enumerable.Range(0, arity), i => rhsargs.Add(BplFormalVar("bx" + i, Predef.BoxType, true, formals))); sink.AddTopLevelDeclaration( new Bpl.Function(f.tok, f.FullSanitizedName + "#canCall", new List(), formals, @@ -180,17 +180,17 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 { var bvars = new List(); - var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, predef.Ty, bvars)); + var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, Predef.Ty, bvars)); - var h0 = BplBoundVar("h0", predef.HeapType, bvars); - var h1 = BplBoundVar("h1", predef.HeapType, bvars); + var h0 = BplBoundVar("h0", Predef.HeapType, bvars); + var h1 = BplBoundVar("h1", Predef.HeapType, bvars); var heapSucc = HeapSucc(h0, h1); var goodHeaps = BplAnd( FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, h0), FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, h1)); - var f = BplBoundVar("f", predef.HandleType, bvars); - var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, predef.BoxType, bvars)); + var f = BplBoundVar("f", Predef.HandleType, bvars); + var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, Predef.BoxType, bvars)); var isness = BplAnd( Snoc(Map(Enumerable.Range(0, arity), i => @@ -201,12 +201,12 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 // inner forall vars var ivars = new List(); - var o = BplBoundVar("o", predef.RefType, ivars); - var fld = BplBoundVar("fld", predef.FieldName(tok), ivars); + var o = BplBoundVar("o", Predef.RefType, ivars); + var fld = BplBoundVar("fld", Predef.FieldName(tok), ivars); var inner_forall = new Bpl.ForallExpr(tok, new List(), ivars, BplImp( BplAnd( - Bpl.Expr.Neq(o, predef.Null), + Bpl.Expr.Neq(o, Predef.Null), // Note, the MkIsAlloc conjunct of "isness" implies that everything in the reads frame is allocated in "h0", which by HeapSucc(h0,h1) also implies the frame is allocated in "h1" new Bpl.NAryExpr(tok, new Bpl.MapSelect(tok, 1), new List { FunctionCall(tok, Reads(ad.Arity), objset_ty, Concat(types, Cons(hN, Cons(f, boxes)))), @@ -241,11 +241,11 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 */ { var bvars = new List(); - var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, predef.Ty, bvars)); + var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, Predef.Ty, bvars)); var oneheap = NewOneHeapExpr(tok); - var h = BplBoundVar("heap", predef.HeapType, bvars); - var f = BplBoundVar("f", predef.HandleType, bvars); - var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, predef.BoxType, bvars)); + var h = BplBoundVar("heap", Predef.HeapType, bvars); + var f = BplBoundVar("f", Predef.HandleType, bvars); + var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, Predef.BoxType, bvars)); var goodHeap = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, h); @@ -256,7 +256,7 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 var readsOne = FunctionCall(tok, Reads(arity), objset_ty, Concat(types, Cons(oneheap, Cons(f, boxes)))); var readsH = FunctionCall(tok, Reads(arity), objset_ty, Concat(types, Cons(h, Cons(f, boxes)))); - var empty = FunctionCall(tok, BuiltinFunction.SetEmpty, predef.BoxType); + var empty = FunctionCall(tok, BuiltinFunction.SetEmpty, Predef.BoxType); var readsNothingOne = FunctionCall(tok, BuiltinFunction.SetEqual, null, readsOne, empty); var readsNothingH = FunctionCall(tok, BuiltinFunction.SetEqual, null, readsH, empty); @@ -279,11 +279,11 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 */ { var bvars = new List(); - var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, predef.Ty, bvars)); + var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, Predef.Ty, bvars)); var oneheap = NewOneHeapExpr(tok); - var h = BplBoundVar("heap", predef.HeapType, bvars); - var f = BplBoundVar("f", predef.HandleType, bvars); - var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, predef.BoxType, bvars)); + var h = BplBoundVar("heap", Predef.HeapType, bvars); + var f = BplBoundVar("f", Predef.HandleType, bvars); + var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, Predef.BoxType, bvars)); var goodHeap = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, h); @@ -293,7 +293,7 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 BplAnd(MkIs(f, ClassTyCon(ad, types)), Bpl.Expr.True))); var readsOne = FunctionCall(tok, Reads(arity), objset_ty, Concat(types, Cons(oneheap, Cons(f, boxes)))); - var empty = FunctionCall(tok, BuiltinFunction.SetEmpty, predef.BoxType); + var empty = FunctionCall(tok, BuiltinFunction.SetEmpty, Predef.BoxType); var readsNothingOne = FunctionCall(tok, BuiltinFunction.SetEqual, null, readsOne, empty); var requiresOne = FunctionCall(tok, Requires(arity), Bpl.Type.Bool, Concat(types, Cons(oneheap, Cons(f, boxes)))); @@ -321,17 +321,17 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 */ { var bvarsOuter = new List(); - var f = BplBoundVar("f", predef.HandleType, bvarsOuter); - var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, predef.Ty, bvarsOuter)); + var f = BplBoundVar("f", Predef.HandleType, bvarsOuter); + var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, Predef.Ty, bvarsOuter)); var Is = MkIs(f, ClassTyCon(ad, types)); var bvarsInner = new List(); - var h = BplBoundVar("h", predef.HeapType, bvarsInner); - var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, predef.BoxType, bvarsInner)); + var h = BplBoundVar("h", Predef.HeapType, bvarsInner); + var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, Predef.BoxType, bvarsInner)); var goodHeap = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, h); var isBoxes = BplAnd(Map(Enumerable.Range(0, arity), i => MkIs(boxes[i], types[i], true))); - var pre = FunctionCall(tok, Requires(ad.Arity), predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); - var applied = FunctionCall(tok, Apply(ad.Arity), predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); + var pre = FunctionCall(tok, Requires(ad.Arity), Predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); + var applied = FunctionCall(tok, Apply(ad.Arity), Predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); var applied_is = MkIs(applied, types[ad.Arity], true); sink.AddTopLevelDeclaration(new Axiom(tok, @@ -353,15 +353,15 @@ even fields of *unallocated* objects o are unchanged from h0 to h1 */ { var bvarsOuter = new List(); - var f = BplBoundVar("f", predef.HandleType, bvarsOuter); - var typesT = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, predef.Ty, bvarsOuter)); + var f = BplBoundVar("f", Predef.HandleType, bvarsOuter); + var typesT = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, Predef.Ty, bvarsOuter)); var IsT = MkIs(f, ClassTyCon(ad, typesT)); - var typesU = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("u" + i, predef.Ty, bvarsOuter)); + var typesU = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("u" + i, Predef.Ty, bvarsOuter)); var IsU = MkIs(f, ClassTyCon(ad, typesU)); Func Inner = (a, b) => { var bvarsInner = new List(); - var bx = BplBoundVar("bx", predef.BoxType, bvarsInner); + var bx = BplBoundVar("bx", Predef.BoxType, bvarsInner); var isBoxA = MkIs(bx, a, true); var isBoxB = MkIs(bx, b, true); var tr = new Bpl.Trigger(tok, true, new[] { isBoxA }, new Bpl.Trigger(tok, true, new[] { isBoxB })); @@ -398,24 +398,24 @@ and implies nothing about the reads set. */ { var bvarsOuter = new List(); - var f = BplBoundVar("f", predef.HandleType, bvarsOuter); - var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, predef.Ty, bvarsOuter)); - var h = BplBoundVar("h", predef.HeapType, bvarsOuter); + var f = BplBoundVar("f", Predef.HandleType, bvarsOuter); + var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, Predef.Ty, bvarsOuter)); + var h = BplBoundVar("h", Predef.HeapType, bvarsOuter); var goodHeap = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, h); var isAlloc = MkIsAlloc(f, ClassTyCon(ad, types), h); var bvarsInner = new List(); - var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, predef.BoxType, bvarsInner)); + var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, Predef.BoxType, bvarsInner)); var isAllocBoxes = BplAnd(Map(Enumerable.Range(0, arity), i => BplAnd(MkIs(boxes[i], types[i], true), MkIsAlloc(boxes[i], types[i], h, true)))); - var pre = FunctionCall(tok, Requires(ad.Arity), predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); - var applied = FunctionCall(tok, Apply(ad.Arity), predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); + var pre = FunctionCall(tok, Requires(ad.Arity), Predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); + var applied = FunctionCall(tok, Apply(ad.Arity), Predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); // (forall r: ref :: {Reads1(t0, t1, f, h, bx0)[$Box(r)]} r != null && Reads1(t0, t1, f, h, bx0)[$Box(r)] ==> h[r, alloc]) var bvarsR = new List(); - var r = BplBoundVar("r", predef.RefType, bvarsR); - var rNonNull = Bpl.Expr.Neq(r, predef.Null); - var reads = FunctionCall(tok, Reads(ad.Arity), predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); + var r = BplBoundVar("r", Predef.RefType, bvarsR); + var rNonNull = Bpl.Expr.Neq(r, Predef.Null); + var reads = FunctionCall(tok, Reads(ad.Arity), Predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); var rInReads = Bpl.Expr.Select(reads, FunctionCall(tok, BuiltinFunction.Box, null, r)); var rAlloc = IsAlloced(tok, h, r); var isAllocReads = BplForall(bvarsR, BplTrigger(rInReads), BplImp(BplAnd(rNonNull, rInReads), rAlloc)); @@ -444,17 +444,17 @@ and implies nothing about the reads set. */ { var bvarsOuter = new List(); - var f = BplBoundVar("f", predef.HandleType, bvarsOuter); - var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, predef.Ty, bvarsOuter)); - var h = BplBoundVar("h", predef.HeapType, bvarsOuter); + var f = BplBoundVar("f", Predef.HandleType, bvarsOuter); + var types = Map(Enumerable.Range(0, arity + 1), i => BplBoundVar("t" + i, Predef.Ty, bvarsOuter)); + var h = BplBoundVar("h", Predef.HeapType, bvarsOuter); var goodHeap = FunctionCall(tok, BuiltinFunction.IsGoodHeap, null, h); var isAlloc = MkIsAlloc(f, ClassTyCon(ad, types), h); var bvarsInner = new List(); - var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, predef.BoxType, bvarsInner)); + var boxes = Map(Enumerable.Range(0, arity), i => BplBoundVar("bx" + i, Predef.BoxType, bvarsInner)); var isAllocBoxes = BplAnd(Map(Enumerable.Range(0, arity), i => MkIsAlloc(boxes[i], types[i], h, true))); - var pre = FunctionCall(tok, Requires(ad.Arity), predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); - var applied = FunctionCall(tok, Apply(ad.Arity), predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); + var pre = FunctionCall(tok, Requires(ad.Arity), Predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); + var applied = FunctionCall(tok, Apply(ad.Arity), Predef.BoxType, Concat(types, Cons(h, Cons(f, boxes)))); var applied_isAlloc = MkIsAlloc(applied, types[ad.Arity], h, true); sink.AddTopLevelDeclaration(new Axiom(tok, @@ -491,9 +491,9 @@ private string AddTyAxioms(TopLevelDecl td) { */ for (int i = 0; i < func.InParams.Count; i++) { var args = MkTyParamBinders(td.TypeArgs, out var argExprs); - var inner = FunctionCall(tok, name, predef.Ty, argExprs); - Bpl.Variable tyVarIn = BplFormalVar(null, predef.Ty, true); - Bpl.Variable tyVarOut = BplFormalVar(null, predef.Ty, false); + var inner = FunctionCall(tok, name, Predef.Ty, argExprs); + Bpl.Variable tyVarIn = BplFormalVar(null, Predef.Ty, true); + Bpl.Variable tyVarOut = BplFormalVar(null, Predef.Ty, false); var injname = name + "_" + i; var injfunc = new Bpl.Function(tok, injname, Singleton(tyVarIn), tyVarOut); sink.AddTopLevelDeclaration(injfunc); @@ -515,7 +515,7 @@ private string AddTyAxioms(TopLevelDecl td) { if (!ModeledAsBoxType(UserDefinedType.FromTopLevelDecl(td.tok, td))) { var args = MkTyParamBinders(td.TypeArgs, out var argExprs); var ty_repr = TrType(UserDefinedType.FromTopLevelDecl(td.tok, td)); - var typeTerm = FunctionCall(tok, name, predef.Ty, argExprs); + var typeTerm = FunctionCall(tok, name, Predef.Ty, argExprs); AddBoxUnboxAxiom(tok, name, typeTerm, ty_repr, args); } @@ -538,24 +538,24 @@ private Axiom CreateTagAndCallingForTypeConstructor(TopLevelDecl td) { string name = "T" + inner_name; var args = MkTyParamBinders(td.TypeArgs, out var argExprs); - var inner = FunctionCall(tok, name, predef.Ty, argExprs); + var inner = FunctionCall(tok, name, Predef.Ty, argExprs); Bpl.Expr body = Bpl.Expr.True; if (!td.EnclosingModuleDefinition.IsFacade) { var tagName = "Tag" + inner_name; - var tag = new Bpl.Constant(tok, new Bpl.TypedIdent(tok, tagName, predef.TyTag), true); + var tag = new Bpl.Constant(tok, new Bpl.TypedIdent(tok, tagName, Predef.TyTag), true); sink.AddTopLevelDeclaration(tag); - body = Bpl.Expr.Eq(FunctionCall(tok, "Tag", predef.TyTag, inner), new Bpl.IdentifierExpr(tok, tag)); + body = Bpl.Expr.Eq(FunctionCall(tok, "Tag", Predef.TyTag, inner), new Bpl.IdentifierExpr(tok, tag)); } if (!tytagConstants.TryGetValue(td.Name, out var tagFamily)) { tagFamily = new Bpl.Constant(Token.NoToken, - new Bpl.TypedIdent(Token.NoToken, "tytagFamily$" + td.Name, predef.TyTagFamily), true); + new Bpl.TypedIdent(Token.NoToken, "tytagFamily$" + td.Name, Predef.TyTagFamily), true); tytagConstants.Add(td.Name, tagFamily); } body = BplAnd(body, - Bpl.Expr.Eq(FunctionCall(tok, "TagFamily", predef.TyTagFamily, inner), new Bpl.IdentifierExpr(tok, tagFamily))); + Bpl.Expr.Eq(FunctionCall(tok, "TagFamily", Predef.TyTagFamily, inner), new Bpl.IdentifierExpr(tok, tagFamily))); var qq = BplForall(args, BplTrigger(inner), body); var tagAxiom = new Axiom(tok, qq, name + " Tag"); @@ -587,7 +587,7 @@ private void AddBitvectorTypeAxioms(int w) { // axiom (forall v: bv3, heap: Heap :: { $IsAlloc(v, TBitvector(3), h) } $IsAlloc(v, TBitvector(3), heap)); vVar = BplBoundVar("v", boogieType, out v); - var heapVar = BplBoundVar("heap", predef.HeapType, out var heap); + var heapVar = BplBoundVar("heap", Predef.HeapType, out var heap); bvs = new List() { vVar, heapVar }; var isAllocBv = MkIsAlloc(v, typeTerm, heap); tr = BplTrigger(isAllocBv); @@ -609,7 +609,7 @@ private void AddBoxUnboxAxiom(IToken tok, string printableName, Bpl.Expr typeTer Contract.Requires(tyRepr != null); Contract.Requires(args != null); - var bxVar = BplBoundVar("bx", predef.BoxType, out var bx); + var bxVar = BplBoundVar("bx", Predef.BoxType, out var bx); var unbox = FunctionCall(tok, BuiltinFunction.Unbox, tyRepr, bx); var box_is = MkIs(bx, typeTerm, true); var unbox_is = MkIs(unbox, typeTerm, false); @@ -987,7 +987,7 @@ void AddRedirectingTypeDeclAxioms(bool is_alloc, T dd, string fullName) if (is_alloc) { comment = $"$IsAlloc axiom for {dd.WhatKind} {fullName}"; - var h = BplBoundVar("$h", predef.HeapType, vars); + var h = BplBoundVar("$h", Predef.HeapType, vars); // $IsAlloc(o, ..) is_o = MkIsAlloc(o, o_ty, h, ModeledAsBoxType(baseType)); trigger = BplTrigger(is_o); @@ -1005,7 +1005,7 @@ void AddRedirectingTypeDeclAxioms(bool is_alloc, T dd, string fullName) // $Is(o, ..) is_o = MkIs(o, o_ty, ModeledAsBoxType(baseType)); trigger = BplTrigger(is_o); - var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(dd.tok), null); + var etran = new ExpressionTranslator(this, Predef, NewOneHeapExpr(dd.tok), null); Bpl.Expr parentConstraint, constraint; if (baseType.IsNumericBased() || baseType.IsBitVectorType || baseType.IsBoolType || baseType.IsCharType) { // optimize this to only use the numeric/bitvector constraint, not the whole $Is thing on the base type @@ -1052,7 +1052,7 @@ Bpl.Expr ConvertExpression(IToken tok, Bpl.Expr r, Type fromType, Type toType) { } else if (toType.IsBitVectorType) { r = IntToBV(tok, r, toType); } else if (toType.IsBigOrdinalType) { - r = FunctionCall(tok, "ORD#FromNat", predef.BigOrdinalType, r); + r = FunctionCall(tok, "ORD#FromNat", Predef.BigOrdinalType, r); } else { Contract.Assert(false, $"No translation implemented from {fromType} to {toType}"); } @@ -1090,7 +1090,7 @@ Bpl.Expr ConvertExpression(IToken tok, Bpl.Expr r, Type fromType, Type toType) { r = FunctionCall(tok, BuiltinFunction.CharFromInt, null, r); } else if (toType.IsBigOrdinalType) { r = FunctionCall(tok, "nat_from_bv" + fromWidth, Bpl.Type.Int, r); - r = FunctionCall(tok, "ORD#FromNat", predef.BigOrdinalType, r); + r = FunctionCall(tok, "ORD#FromNat", Predef.BigOrdinalType, r); } else { Contract.Assert(false, $"No translation implemented from {fromType} to {toType}"); } @@ -1421,7 +1421,7 @@ void CheckResultToBeInType_Aux(IToken tok, Expression boogieExpr, Expression ori void AddWellformednessCheck(RedirectingTypeDecl decl) { Contract.Requires(decl != null); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); Contract.Requires(currentModule == null && codeContext == null && isAllocContext == null); Contract.Ensures(currentModule == null && codeContext == null && isAllocContext == null); @@ -1434,7 +1434,7 @@ void AddWellformednessCheck(RedirectingTypeDecl decl) { currentModule = decl.Module; codeContext = new CallableWrapper(decl, true); - var etran = new ExpressionTranslator(this, predef, decl.tok, null); + var etran = new ExpressionTranslator(this, Predef, decl.tok, null); // parameters of the procedure var inParams = MkTyParamFormals(decl.TypeArgs, true); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.cs b/Source/DafnyCore/Verifier/BoogieGenerator.cs index a32575bf5da..14dbf57d7fc 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.cs @@ -90,7 +90,7 @@ public BoogieGenerator(ErrorReporter reporter, ProofDependencyManager depManager foreach (var function in boogieProgram.TopLevelDeclarations.OfType()) { function.AlwaysRevealed = true; } - predef = FindPredefinedDecls(boogieProgram); + Predef = FindPredefinedDecls(boogieProgram); } } @@ -138,7 +138,7 @@ public void AddReferencedMember(MemberDecl m) { } FuelContext fuelContext = null; - IsAllocContext isAllocContext = null; + internal IsAllocContext isAllocContext = null; Program program; [ContractInvariantMethod] @@ -209,7 +209,7 @@ bool InVerificationScope(RedirectingTypeDecl d) { private VisibilityScope verificationScope; private Dictionary declarationMapping = new(); - readonly PredefinedDecls predef; + public readonly PredefinedDecls Predef; private TranslatorFlags flags; private bool InsertChecksums { get { return flags.InsertChecksums; } } @@ -691,7 +691,7 @@ public Bpl.IdentifierExpr TrVar(IToken tok, IVariable var) { Contract.Requires(var != null); Contract.Requires(tok != null); Contract.Ensures(Contract.Result() != null); - return new Bpl.IdentifierExpr(tok, var.AssignUniqueName(currentDeclaration.IdGenerator), TrType(var.Type)); + return new Bpl.IdentifierExpr(tok, var.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(var.Type)); } public Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { @@ -743,7 +743,7 @@ public Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { } foreach (TopLevelDecl d in program.SystemModuleManager.SystemModule.TopLevelDecls) { - currentDeclaration = d; + CurrentDeclaration = d; if (d is AbstractTypeDecl abstractType) { GetOrCreateTypeConstructor(abstractType); AddClassMembers(abstractType, true, true); @@ -794,7 +794,7 @@ public Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { } foreach (TopLevelDecl d in visibleTopLevelDecls) { - currentDeclaration = d; + CurrentDeclaration = d; if (d is AbstractTypeDecl abstractType) { AddClassMembers(abstractType, true, true); } else if (d is ModuleDecl) { @@ -1017,15 +1017,15 @@ private void ComputeFunctionFuel() { // declare the fuel constant if (f.IsFueled) { // const BaseFuel_FunctionA : LayerType - Bpl.Constant baseFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "BaseFuel_" + f.FullName, predef.LayerType), false); + Bpl.Constant baseFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "BaseFuel_" + f.FullName, Predef.LayerType), false); sink.AddTopLevelDeclaration(baseFuel); Bpl.Expr baseFuel_expr = new Bpl.IdentifierExpr(f.tok, baseFuel); // const StartFuel_FunctionA : LayerType - Bpl.Constant startFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuel_" + f.FullName, predef.LayerType), false); + Bpl.Constant startFuel = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuel_" + f.FullName, Predef.LayerType), false); sink.AddTopLevelDeclaration(startFuel); Bpl.Expr startFuel_expr = new Bpl.IdentifierExpr(f.tok, startFuel); // const StartFuelAssert_FunctionA : LayerType - Bpl.Constant startFuelAssert = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuelAssert_" + f.FullName, predef.LayerType), false); + Bpl.Constant startFuelAssert = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, "StartFuelAssert_" + f.FullName, Predef.LayerType), false); sink.AddTopLevelDeclaration(startFuelAssert); Bpl.Expr startFuelAssert_expr = new Bpl.IdentifierExpr(f.tok, startFuelAssert); this.functionFuel.Add(new FuelConstant(f, baseFuel_expr, startFuel_expr, startFuelAssert_expr)); @@ -1097,7 +1097,7 @@ private void AddTraitParentAxioms() { TypeBoundAxiomExpressions(c.tok, bvarsTypeParameters, childType, new List() { parentType }, out var isBoxExpr, out var isAllocBoxExpr); - var heapVar = BplBoundVar("$heap", predef.HeapType, out var heap); + var heapVar = BplBoundVar("$heap", Predef.HeapType, out var heap); var oVar = BplBoundVar("$o", TrType(childType), out var o); var oj = BoxifyForTraitParent(c.tok, o, ((UserDefinedType)parentType.NormalizeExpand()).ResolvedClass, childType); @@ -1180,8 +1180,8 @@ public Expr TypeSpecificEqual(IToken tok, Dafny.Type type, Expr e0, Expr e1) { Contract.Requires(A != null); Contract.Requires(B != null); Contract.Requires(l != null); - Contract.Requires(predef != null); - var etran = new ExpressionTranslator(this, predef, dt.tok, dt); + Contract.Requires(Predef != null); + var etran = new ExpressionTranslator(this, Predef, dt.tok, dt); // For example, for possibly infinite lists: // codatatype SList = Nil | SCons(head: T, tail: SList); // produce with conjucts=false (default): @@ -1308,7 +1308,7 @@ public Bpl.Expr IsAlloced(IToken tok, Bpl.Expr heapExpr, Bpl.Expr e) { Contract.Requires(e != null); Contract.Ensures(Contract.Result() != null); - return ApplyUnbox(tok, ReadHeap(tok, heapExpr, e, predef.Alloc(tok)), Bpl.Type.Bool); + return ApplyUnbox(tok, ReadHeap(tok, heapExpr, e, Predef.Alloc(tok)), Bpl.Type.Bool); } /// @@ -1322,9 +1322,9 @@ public Bpl.Expr ReadHeap(IToken tok, Expr heap, Expr r, Expr f) { Contract.Ensures(Contract.Result() != null); var res = new Bpl.NAryExpr(tok, - new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", predef.BoxType)), + new Bpl.FunctionCall(new Bpl.IdentifierExpr(tok, "read", Predef.BoxType)), new List { heap, r, f }); - res.Type = predef.BoxType; + res.Type = Predef.BoxType; return res; } @@ -1468,7 +1468,7 @@ public Specialization(IVariable formal, MatchCase mc, Specialization prev, Boogi List rArgs = new List(); foreach (BoundVar p in mc.Arguments) { - IdentifierExpr ie = new IdentifierExpr(p.tok, p.AssignUniqueName(boogieGenerator.currentDeclaration.IdGenerator)); + IdentifierExpr ie = new IdentifierExpr(p.tok, p.AssignUniqueName(boogieGenerator.CurrentDeclaration.IdGenerator)); ie.Var = p; ie.Type = ie.Var.Type; // resolve it here rArgs.Add(ie); } @@ -1523,8 +1523,8 @@ public Specialization(IVariable formal, MatchCase mc, Specialization prev, Boogi // (forall h: Heap :: { OlderTag(h) } // IsGoodHeap(h) && OlderTag(h) && F(x, y) && IsAlloc(y, Y, h) // ==> IsAlloc(x, X, h)) - var heapVar = BplBoundVar("$olderHeap", predef.HeapType, out var heap); - var etran = new ExpressionTranslator(this, predef, heap, f); + var heapVar = BplBoundVar("$olderHeap", Predef.HeapType, out var heap); + var etran = new ExpressionTranslator(this, Predef, heap, f); var isGoodHeap = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, heap); var olderTag = FunctionCall(f.tok, "$OlderTag", Bpl.Type.Bool, heap); @@ -1577,8 +1577,8 @@ Bpl.Type TrReceiverType(MemberDecl f) { Bpl.Expr ReceiverNotNull(Bpl.Expr th) { Contract.Requires(th != null); - if (th.Type == predef.RefType) { - return Bpl.Expr.Neq(th, predef.Null); + if (th.Type == Predef.RefType) { + return Bpl.Expr.Neq(th, Predef.Null); } else { return Bpl.Expr.True; } @@ -1587,7 +1587,7 @@ Bpl.Expr ReceiverNotNull(Bpl.Expr th) { void AddFuelSuccSynonymAxiom(Function f, bool forHandle = false) { Contract.Requires(f != null); Contract.Requires(f.IsFuelAware()); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); // axiom // layer synonym axiom // (forall s, $Heap, formals :: // { f(Succ(s), $Heap, formals) } @@ -1598,7 +1598,7 @@ void AddFuelSuccSynonymAxiom(Function f, bool forHandle = false) { var args1 = new List(tyargs); var args0 = new List(tyargs); - var bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType)); + var bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", Predef.LayerType)); formals.Add(bv); var s = new Bpl.IdentifierExpr(f.tok, bv); args1.Add(FunctionCall(f.tok, BuiltinFunction.LayerSucc, null, s)); @@ -1612,14 +1612,14 @@ void AddFuelSuccSynonymAxiom(Function f, bool forHandle = false) { } if (f is TwoStateFunction) { - bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", predef.HeapType)); + bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", Predef.HeapType)); formals.Add(bv); s = new Bpl.IdentifierExpr(f.tok, bv); args1.Add(s); args0.Add(s); } if (!forHandle && f.ReadsHeap) { - bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType)); + bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, Predef.HeapVarName, Predef.HeapType)); formals.Add(bv); s = new Bpl.IdentifierExpr(f.tok, bv); args1.Add(s); @@ -1660,7 +1660,7 @@ void AddFuelZeroSynonymAxiom(Function f) { // f(s, $Heap, formals) == f($LZ, $Heap, formals)); Contract.Requires(f != null); Contract.Requires(f.IsFuelAware()); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); List tyargs; var formals = MkTyParamBinders(GetTypeParams(f), out tyargs); @@ -1668,12 +1668,12 @@ void AddFuelZeroSynonymAxiom(Function f) { var args1 = new List(tyargs); var args0 = new List(tyargs); - var bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType)); + var bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$ly", Predef.LayerType)); formals.Add(bv); var s = new Bpl.IdentifierExpr(f.tok, bv); args2.Add(FunctionCall(f.tok, BuiltinFunction.AsFuelBottom, null, s)); args1.Add(s); - args0.Add(new Bpl.IdentifierExpr(f.tok, "$LZ", predef.LayerType)); // $LZ + args0.Add(new Bpl.IdentifierExpr(f.tok, "$LZ", Predef.LayerType)); // $LZ if (f.IsOpaque || f.IsMadeImplicitlyOpaque(options)) { var bvReveal = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$reveal", Boogie.Type.Bool)); formals.Add(bvReveal); @@ -1684,7 +1684,7 @@ void AddFuelZeroSynonymAxiom(Function f) { } if (f is TwoStateFunction) { - bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", predef.HeapType)); + bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", Predef.HeapType)); formals.Add(bv); s = new Bpl.IdentifierExpr(f.tok, bv); args2.Add(s); @@ -1692,7 +1692,7 @@ void AddFuelZeroSynonymAxiom(Function f) { args0.Add(s); } if (f.ReadsHeap) { - bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType)); + bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, Predef.HeapVarName, Predef.HeapType)); formals.Add(bv); s = new Bpl.IdentifierExpr(f.tok, bv); args2.Add(s); @@ -1807,21 +1807,21 @@ Bpl.IdentifierExpr GetTmpVar_IdExpr(Bpl.IToken tok, string name, Bpl.Type ty, Va Bpl.IdentifierExpr GetPrevHeapVar_IdExpr(IToken tok, Variables locals) // local variable that's shared between statements that need it { Contract.Requires(tok != null); - Contract.Requires(locals != null); Contract.Requires(predef != null); + Contract.Requires(locals != null); Contract.Requires(Predef != null); Contract.Ensures(Contract.Result() != null); - return GetTmpVar_IdExpr(tok, "$prevHeap", predef.HeapType, locals); + return GetTmpVar_IdExpr(tok, "$prevHeap", Predef.HeapType, locals); } Bpl.IdentifierExpr GetNewVar_IdExpr(IToken tok, Variables locals) // local variable that's shared between statements that need it { Contract.Requires(tok != null); Contract.Requires(locals != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Ensures(Contract.Result() != null); // important: the following declaration produces no where clause (that's why we're going through the trouble of setting of this variable in the first place) - return GetTmpVar_IdExpr(tok, "$nw", predef.RefType, locals); + return GetTmpVar_IdExpr(tok, "$nw", Predef.RefType, locals); } /// @@ -1895,7 +1895,7 @@ bool DefineFuelConstant(IToken tok, Attributes attribs, BoogieStmtListBuilder bu if (fuelConstant != null) { Bpl.Expr startFuel = fuelConstant.startFuel; Bpl.Expr startFuelAssert = fuelConstant.startFuelAssert; - Bpl.Expr moreFuel_expr = fuelConstant.MoreFuel(sink, predef, f.IdGenerator); + Bpl.Expr moreFuel_expr = fuelConstant.MoreFuel(sink, Predef, f.IdGenerator); Bpl.Expr layer = etran.layerInterCluster.LayerN(settings.low, moreFuel_expr); Bpl.Expr layerAssert = etran.layerInterCluster.LayerN(settings.high, moreFuel_expr); builder.Add(TrAssumeCmd(tok, Bpl.Expr.Eq(startFuel, layer))); @@ -2028,13 +2028,13 @@ void GenerateImplPrelude(Method m, bool wellformednessProc, List inPar Contract.Requires(outParams != null); Contract.Requires(builder != null); Contract.Requires(localVariables != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Requires(wellformednessProc || m.Body != null); if (m is TwoStateLemma) { // $Heap := current$Heap; - var heap = ExpressionTranslator.HeapIdentifierExpr(predef, m.tok); - builder.Add(Bpl.Cmd.SimpleAssign(m.tok, heap, new Bpl.IdentifierExpr(m.tok, "current$Heap", predef.HeapType))); + var heap = ExpressionTranslator.HeapIdentifierExpr(Predef, m.tok); + builder.Add(Bpl.Cmd.SimpleAssign(m.tok, heap, new Bpl.IdentifierExpr(m.tok, "current$Heap", Predef.HeapType))); } // set up the information used to verify the method's reads and modifies clauses @@ -2058,23 +2058,23 @@ public void DefineFrame(IToken/*!*/ tok, Boogie.IdentifierExpr frameIdentifier, Contract.Requires(frameIdentifier.Type != null); Contract.Requires(cce.NonNullElements(frameClause)); Contract.Requires(builder != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); if (etran == null) { // This is the common case. It means that the frame will be defined in terms of the usual variable $Heap. // The one case where a frame is needed for a different heap is for lambda expressions, because they may // sit inside of an "old" expression. - etran = new ExpressionTranslator(this, predef, tok, null); + etran = new ExpressionTranslator(this, Predef, tok, null); } // Declare a local variable $_Frame: [ref, Field]bool var frame = localVariables.GetOrAdd(new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, name ?? frameIdentifier.Name, frameIdentifier.Type))); // $_Frame := (lambda $o: ref, $f: Field :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Modifies/Reads-Clause); // $_Frame := (lambda $o: ref, $f: Field :: $o != null ==> ($o,$f) in Modifies/Reads-Clause); - Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType)); + Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", Predef.RefType)); Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar); - Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok))); + Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", Predef.FieldName(tok))); Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar); - Bpl.Expr oNotNull = Bpl.Expr.Neq(o, predef.Null); + Bpl.Expr oNotNull = Bpl.Expr.Neq(o, Predef.Null); Bpl.Expr ante = BplAnd(oNotNull, etran.IsAlloced(tok, o)); Bpl.Expr consequent = InRWClause(tok, o, f, frameClause, etran, null, null); Bpl.Expr lambda = new Bpl.LambdaExpr(tok, new List(), new List { oVar, fVar }, null, @@ -2104,14 +2104,14 @@ void CheckFrameSubset(IToken tok, List calleeFrame, Contract.Requires(receiverReplacement == null || substMap != null); Contract.Requires(etran != null); Contract.Requires(makeAssert != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); // emit: assert (forall o: ref, f: Field :: o != null && $Heap[o,alloc] && (o,f) in subFrame ==> enclosingFrame[o,f]); - var oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType)); + var oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", Predef.RefType)); var o = new Bpl.IdentifierExpr(tok, oVar); - var fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok))); + var fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", Predef.FieldName(tok))); var f = new Bpl.IdentifierExpr(tok, fVar); - var ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o)); + var ante = Bpl.Expr.And(Bpl.Expr.Neq(o, Predef.Null), etran.IsAlloced(tok, o)); var oInCallee = InRWClause(tok, o, f, calleeFrame, etran, receiverReplacement, substMap); var inEnclosingFrame = Bpl.Expr.Select(enclosingFrame, o, f); @@ -2131,14 +2131,14 @@ void CheckFrameEmpty(IToken tok, Contract.Requires(etran != null); Contract.Requires(frame != null); Contract.Requires(etran != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); // emit: assert (forall o: ref, f: Field :: o != null && $Heap[o,alloc] ==> !frame[o,f]); - var oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType)); + var oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", Predef.RefType)); var o = new Bpl.IdentifierExpr(tok, oVar); - var fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok))); + var fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", Predef.FieldName(tok))); var f = new Bpl.IdentifierExpr(tok, fVar); - var ante = BplAnd(Bpl.Expr.Neq(o, predef.Null), etran.IsAlloced(tok, o)); + var ante = BplAnd(Bpl.Expr.Neq(o, Predef.Null), etran.IsAlloced(tok, o)); var inFrame = Bpl.Expr.Select(frame, o, f); var notInFrame = Bpl.Expr.Not(inFrame); @@ -2202,7 +2202,7 @@ Bpl.Expr InRWClause(IToken tok, Bpl.Expr o, Bpl.Expr f, List rw Contract.Requires(etran != null); Contract.Requires(cce.NonNullElements(rw)); Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap)); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Requires(receiverReplacement == null || substMap != null); Contract.Ensures(Contract.Result() != null); return InRWClause(tok, o, f, rw, false, etran, receiverReplacement, substMap); @@ -2216,7 +2216,7 @@ Bpl.Expr InRWClause(IToken tok, Bpl.Expr o, Bpl.Expr f, List rw Contract.Requires(etran != null); Contract.Requires(cce.NonNullElements(rw)); Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap)); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Requires(receiverReplacement == null || substMap != null); Contract.Ensures(Contract.Result() != null); var boxO = FunctionCall(tok, BuiltinFunction.Box, null, o); @@ -2237,7 +2237,7 @@ Bpl.Expr InRWClause_Aux(IToken tok, Bpl.Expr o, Bpl.Expr boxO, Bpl.Expr f, List< Contract.Requires(etran != null); Contract.Requires(cce.NonNullElements(rw)); Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap)); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Requires((substMap == null && receiverReplacement == null) || substMap != null); Contract.Ensures(Contract.Result() != null); @@ -2274,7 +2274,7 @@ Bpl.Expr InRWClause_Aux(IToken tok, Bpl.Expr o, Bpl.Expr boxO, Bpl.Expr f, List< Bpl.Variable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int)); Bpl.Expr i = new Bpl.IdentifierExpr(tok, iVar); Bpl.Expr iBounds = InSeqRange(tok, i, Type.Int, etran.TrExpr(e), true, null, false); - Bpl.Expr XsubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, etran.TrExpr(e), i); + Bpl.Expr XsubI = FunctionCall(tok, BuiltinFunction.SeqIndex, Predef.BoxType, etran.TrExpr(e), i); // TODO: the equality in the next line should be changed to one that understands extensionality //TRIG (exists $i: int :: 0 <= $i && $i < Seq#Length(read($h0, this, _module.DoublyLinkedList.Nodes)) && Seq#Index(read($h0, this, _module.DoublyLinkedList.Nodes), $i) == $Box($o)) disjunct = new Bpl.ExistsExpr(tok, new List { iVar }, BplAnd(iBounds, Bpl.Expr.Eq(XsubI, boxO))); // LL_TRIGGER @@ -2286,7 +2286,7 @@ Bpl.Expr InRWClause_Aux(IToken tok, Bpl.Expr o, Bpl.Expr boxO, Bpl.Expr f, List< Bpl.Expr q = Bpl.Expr.Eq(f, new Bpl.IdentifierExpr(rwComponent.E.tok, GetField(rwComponent.Field))); if (usedInUnchanged) { q = BplOr(q, - Bpl.Expr.Eq(f, new Bpl.IdentifierExpr(rwComponent.E.tok, predef.AllocField))); + Bpl.Expr.Eq(f, new Bpl.IdentifierExpr(rwComponent.E.tok, Predef.AllocField))); } disjunct = BplAnd(disjunct, q); } @@ -2296,72 +2296,6 @@ Bpl.Expr InRWClause_Aux(IToken tok, Bpl.Expr o, Bpl.Expr boxO, Bpl.Expr f, List< } - /// - /// If "declareLocals" is "false", then the locals are added only if they are new, that is, if - /// they don't already exist in "locals". - /// - Bpl.Expr CtorInvocation(MatchCase mc, Type sourceType, ExpressionTranslator etran, Variables locals, BoogieStmtListBuilder localTypeAssumptions, IsAllocType isAlloc, bool declareLocals = true) { - Contract.Requires(mc != null); - Contract.Requires(sourceType != null); - Contract.Requires(etran != null); - Contract.Requires(locals != null); - Contract.Requires(localTypeAssumptions != null); - Contract.Requires(predef != null); - Contract.Ensures(Contract.Result() != null); - - sourceType = sourceType.NormalizeExpand(); - Contract.Assert(sourceType.TypeArgs.Count == mc.Ctor.EnclosingDatatype.TypeArgs.Count); - var subst = new Dictionary(); - for (var i = 0; i < mc.Ctor.EnclosingDatatype.TypeArgs.Count; i++) { - subst.Add(mc.Ctor.EnclosingDatatype.TypeArgs[i], sourceType.TypeArgs[i]); - } - - List args = new List(); - for (int i = 0; i < mc.Arguments.Count; i++) { - BoundVar p = mc.Arguments[i]; - var nm = p.AssignUniqueName(currentDeclaration.IdGenerator); - var local = declareLocals ? null : locals.GetValueOrDefault(nm); // find previous local - if (local == null) { - local = locals.GetOrAdd(new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, nm, TrType(p.Type)))); - } else { - Contract.Assert(Bpl.Type.Equals(local.TypedIdent.Type, TrType(p.Type))); - } - var pFormalType = mc.Ctor.Formals[i].Type.Subst(subst); - var pIsAlloc = (isAlloc == ISALLOC) ? isAllocContext.Var(p) : NOALLOC; - Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, local), pFormalType, etran, pIsAlloc); - if (wh != null) { - localTypeAssumptions.Add(TrAssumeCmd(p.tok, wh)); - } - CheckSubrange(p.tok, new Bpl.IdentifierExpr(p.tok, local), pFormalType, p.Type, new IdentifierExpr(p.Tok, p), localTypeAssumptions); - args.Add(CondApplyBox(mc.tok, new Bpl.IdentifierExpr(p.tok, local), cce.NonNull(p.Type), mc.Ctor.Formals[i].Type)); - } - Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(mc.tok, mc.Ctor.FullName, predef.DatatypeType); - return new Bpl.NAryExpr(mc.tok, new Bpl.FunctionCall(id), args); - } - - Bpl.Expr CtorInvocation(IToken tok, DatatypeCtor ctor, ExpressionTranslator etran, Variables locals, BoogieStmtListBuilder localTypeAssumptions) { - Contract.Requires(tok != null); - Contract.Requires(ctor != null); - Contract.Requires(etran != null); - Contract.Requires(locals != null); - Contract.Requires(localTypeAssumptions != null); - Contract.Requires(predef != null); - Contract.Ensures(Contract.Result() != null); - - // create local variables for the formals - var varNameGen = CurrentIdGenerator.NestedFreshIdGenerator("a#"); - var args = new List(); - foreach (Formal arg in ctor.Formals) { - Contract.Assert(arg != null); - var nm = varNameGen.FreshId(string.Format("#{0}#", args.Count)); - var bv = locals.GetOrAdd(new Bpl.LocalVariable(arg.tok, new Bpl.TypedIdent(arg.tok, nm, TrType(arg.Type)))); - args.Add(new Bpl.IdentifierExpr(arg.tok, bv)); - } - - Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(tok, ctor.FullName, predef.DatatypeType); - return new Bpl.NAryExpr(tok, new Bpl.FunctionCall(id), args); - } - void AddCasePatternVarSubstitutions(CasePattern pat, Bpl.Expr rhs, Dictionary substMap) { Contract.Requires(pat != null); Contract.Requires(rhs != null); @@ -2458,7 +2392,7 @@ void CheckNonNull(IToken tok, Expression e, BoogieStmtListBuilder builder, Expre Contract.Requires(e != null); Contract.Requires(builder != null); Contract.Requires(etran != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); if (!e.Type.IsRefType) { // nothing to do @@ -2467,7 +2401,7 @@ void CheckNonNull(IToken tok, Expression e, BoogieStmtListBuilder builder, Expre } else if (e is StaticReceiverExpr) { // also ok } else { - builder.Add(Assert(tok, Bpl.Expr.Neq(etran.TrExpr(e), predef.Null), + builder.Add(Assert(tok, Bpl.Expr.Neq(etran.TrExpr(e), Predef.Null), new NonNull("target object", e), builder.Context, kv)); } } @@ -2503,7 +2437,7 @@ Bpl.Expr ClassTyCon(UserDefinedType cl, List args) { Bpl.Expr ClassTyCon(TopLevelDecl cl, List args) { Contract.Requires(cl != null); Contract.Requires(cce.NonNullElements(args)); - return FunctionCall(cl.tok, GetClassTyCon(cl), predef.Ty, args); + return FunctionCall(cl.tok, GetClassTyCon(cl), Predef.Ty, args); } // Takes a Bpl.Constant, which typically will be one from GetClass, @@ -2545,7 +2479,7 @@ public string RequiresName(Function f) { } private Expr NewOneHeapExpr(IToken tok) { - return new Bpl.IdentifierExpr(tok, "$OneHeap", predef.HeapType); + return new Bpl.IdentifierExpr(tok, "$OneHeap", Predef.HeapType); } /// @@ -2612,7 +2546,7 @@ void EachReferenceInFrameExpression(Expression e, Variables locals, BoogieStmtLi antecedent = Boogie.Expr.Gt(Bpl.Expr.SelectTok(e.tok, s, BoxIfNecessary(e.tok, x, type)), Boogie.Expr.Literal(0)); } else { description = "sequence element"; - obj = UnboxUnlessInherentlyBoxed(FunctionCall(e.tok, BuiltinFunction.SeqIndex, predef.BoxType, s, x), type); + obj = UnboxUnlessInherentlyBoxed(FunctionCall(e.tok, BuiltinFunction.SeqIndex, Predef.BoxType, s, x), type); antecedent = InSeqRange(e.tok, x, Type.Int, s, true, null, false); } } @@ -2625,24 +2559,24 @@ private Bpl.Function GetOrCreateTypeConstructor(TopLevelDecl td) { Bpl.Function func; if (td is TraitDecl { IsObjectTrait: true }) { // the type constructor for "object" is in DafnyPrelude.bpl - func = predef.ObjectTypeConstructor; + func = Predef.ObjectTypeConstructor; } else if (td is TupleTypeDecl ttd && ttd.Dims == 2 && ttd.NonGhostDims == 2) { // the type constructor for "Tuple2" is in DafnyPrelude.bpl - func = this.predef.Tuple2TypeConstructor; + func = this.Predef.Tuple2TypeConstructor; } else { var inner_name = GetClass(td).TypedIdent.Name; string name = "T" + inner_name; - Bpl.Variable tyVarOut = BplFormalVar(null, predef.Ty, false); - var args = td.TypeArgs.ConvertAll(_ => (Bpl.Variable)BplFormalVar(null, predef.Ty, true)); + Bpl.Variable tyVarOut = BplFormalVar(null, Predef.Ty, false); + var args = td.TypeArgs.ConvertAll(_ => (Bpl.Variable)BplFormalVar(null, Predef.Ty, true)); func = new Bpl.Function(td.tok, name, args, tyVarOut); sink.AddTopLevelDeclaration(func); if (td is AbstractTypeDecl or InternalTypeSynonymDecl) { // axiom (forall T0, T1, ... { T(T0, T1, T2) } :: WhereClause( T(T0, T1, T2) )); var argBoundVars = new List(); - var argExprs = td.TypeArgs.ConvertAll(ta => BplBoundVar(ta.Name, predef.Ty, argBoundVars)); - var funcAppl = FunctionCall(td.tok, name, predef.Ty, argExprs); + var argExprs = td.TypeArgs.ConvertAll(ta => BplBoundVar(ta.Name, Predef.Ty, argBoundVars)); + var funcAppl = FunctionCall(td.tok, name, Predef.Ty, argExprs); var characteristics = td is AbstractTypeDecl ? ((AbstractTypeDecl)td).Characteristics : ((InternalTypeSynonymDecl)td).Characteristics; var whereClause = GetTyWhereClause(funcAppl, characteristics); if (whereClause != null) { @@ -2664,7 +2598,7 @@ private Bpl.Function GetOrCreateTypeConstructor(TopLevelDecl td) { Bpl.Constant GetClass(TopLevelDecl cl) { Contract.Requires(cl != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Ensures(Contract.Result() != null); if (classes.TryGetValue(cl, out var cc)) { @@ -2674,7 +2608,7 @@ Bpl.Constant GetClass(TopLevelDecl cl) { if (cl is ClassLikeDecl { NonNullTypeDecl: { } }) { name = name + "?"; // TODO: this doesn't seem like the best place to do this name transformation } - cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + name, predef.ClassNameType), !cl.EnclosingModuleDefinition.IsFacade); + cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + name, Predef.ClassNameType), !cl.EnclosingModuleDefinition.IsFacade); classes.Add(cl, cc); } return cc; @@ -2682,13 +2616,13 @@ Bpl.Constant GetClass(TopLevelDecl cl) { Bpl.Constant GetFieldNameFamily(string n) { Contract.Requires(n != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Ensures(Contract.Result() != null); if (fieldConstants.TryGetValue(n, out var cc)) { Contract.Assert(cc != null); } else { - cc = new Bpl.Constant(Token.NoToken, new Bpl.TypedIdent(Token.NoToken, "field$" + n, predef.NameFamilyType), true); + cc = new Bpl.Constant(Token.NoToken, new Bpl.TypedIdent(Token.NoToken, "field$" + n, Predef.NameFamilyType), true); fieldConstants.Add(n, cc); } return cc; @@ -2703,7 +2637,7 @@ Bpl.Function GetOrCreateFunction(Function f) { } Contract.Requires(f != null); - Contract.Requires(predef != null && sink != null); + Contract.Requires(Predef != null && sink != null); var func = GetFunctionBoogieDefinition(f); sink.AddTopLevelDeclaration(func); @@ -2720,17 +2654,17 @@ private Bpl.Function GetFunctionBoogieDefinition(Function f) { var formals = new List(); formals.AddRange(MkTyParamFormals(GetTypeParams(f), false)); if (f.IsFuelAware()) { - formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$ly", predef.LayerType), true)); + formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$ly", Predef.LayerType), true)); } if (f.IsOpaque || f.IsMadeImplicitlyOpaque(options)) { formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$reveal", Boogie.Type.Bool), true)); } if (f is TwoStateFunction) { - formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", predef.HeapType), true)); + formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", Predef.HeapType), true)); } if (f.ReadsHeap) { - formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$heap", predef.HeapType), true)); + formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$heap", Predef.HeapType), true)); } if (!f.IsStatic) { formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", TrReceiverType(f)), true)); @@ -2753,10 +2687,10 @@ private Bpl.Function GetCanCallFunction(Function f) { var formals = new List(); formals.AddRange(MkTyParamFormals(GetTypeParams(f), false)); if (f is TwoStateFunction) { - formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", predef.HeapType), true)); + formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$prevHeap", Predef.HeapType), true)); } if (f.ReadsHeap) { - formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$heap", predef.HeapType), true)); + formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "$heap", Predef.HeapType), true)); } if (!f.IsStatic) { formals.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", TrReceiverType(f)), true)); @@ -2894,9 +2828,9 @@ private void GenerateMethodParametersChoose(IToken tok, IMethodCodeContext m, Me Contract.Assert(VisibleInScope(p.Type)); Bpl.Type varType = TrType(p.Type); Bpl.Expr wh = GetExtendedWhereClause(p.tok, - new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(currentDeclaration.IdGenerator), varType), + new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(CurrentDeclaration.IdGenerator), varType), p.Type, p.IsOld ? etran.Old : etran, isAllocContext.Var(p)); - inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(currentDeclaration.IdGenerator), varType, wh), true)); + inParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(CurrentDeclaration.IdGenerator), varType, wh), true)); } } if (includeOutParams) { @@ -2907,7 +2841,7 @@ private void GenerateMethodParametersChoose(IToken tok, IMethodCodeContext m, Me Contract.Assert(!p.IsOld); // out-parameters are never old (perhaps we want to relax this condition in the future) Bpl.Type varType = TrType(p.Type); Bpl.Expr wh = GetWhereClause(p.tok, - new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(currentDeclaration.IdGenerator), varType), + new Bpl.IdentifierExpr(p.tok, p.AssignUniqueName(CurrentDeclaration.IdGenerator), varType), p.Type, etran, isAllocContext.Var(p)); if (kind == MethodTranslationKind.Implementation) { var tracker = AddDefiniteAssignmentTracker(p, outParams, true, m.IsGhost); @@ -2915,7 +2849,7 @@ private void GenerateMethodParametersChoose(IToken tok, IMethodCodeContext m, Me wh = BplImp(tracker, wh); } } - outParams.GetOrAdd(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(currentDeclaration.IdGenerator), varType, wh), false)); + outParams.GetOrAdd(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(CurrentDeclaration.IdGenerator), varType, wh), false)); DefiniteAssignmentTrackers = beforeTrackers; } @@ -3009,7 +2943,7 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes Contract.Requires(etran != null); Contract.Requires(etranPre != null); Contract.Requires(cce.NonNullElements(frame)); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Ensures(Contract.Result() != null); // read is handled in AddFrameAxiom @@ -3050,7 +2984,7 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes // ==> // $Heap[o] == PreHeap[o]) // #endif - var oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType)); + var oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", Predef.RefType)); var o = new Bpl.IdentifierExpr(tok, oVar); Bpl.Expr f; @@ -3060,7 +2994,7 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes Bpl.Expr preHeapOF; if (fieldGranularity) { typeVars = new List { }; - var fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok))); + var fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", Predef.FieldName(tok))); f = new Bpl.IdentifierExpr(tok, fVar); quantifiedVars = new List { oVar, fVar }; heapOF = ReadHeap(tok, etran.HeapExpr, o, f); @@ -3074,7 +3008,7 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes preHeapOF = ReadHeap(tok, etranPre.HeapExpr, o); // Box type is Bpl.Type.Bool, but no need to unbox for equality check } - Bpl.Expr ante = Bpl.Expr.Neq(o, predef.Null); + Bpl.Expr ante = Bpl.Expr.Neq(o, Predef.Null); if (canAllocate && use == FrameExpressionUse.Modifies) { ante = BplAnd(ante, etranMod.IsAlloced(tok, o)); } @@ -3090,7 +3024,7 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes Contract.Requires(tok != null); Contract.Requires(etran != null); Contract.Requires(etranPre != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Ensures(Contract.Result() != null); // generate: @@ -3098,14 +3032,14 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes // o != null && old($Heap)[o,alloc] ==> // $Heap[o,f] == PreHeap[o,f] || // $_Frame[o,f]) - Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType)); + Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", Predef.RefType)); Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar); - Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok))); + Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", Predef.FieldName(tok))); Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar); Bpl.Expr heapOF = ReadHeap(tok, etran.HeapExpr, o, f); Bpl.Expr preHeapOF = ReadHeap(tok, etranPre.HeapExpr, o, f); - Bpl.Expr ante = BplAnd(Bpl.Expr.Neq(o, predef.Null), etranPre.IsAlloced(tok, o)); + Bpl.Expr ante = BplAnd(Bpl.Expr.Neq(o, Predef.Null), etranPre.IsAlloced(tok, o)); Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF); consequent = BplOr(consequent, Bpl.Expr.SelectTok(tok, frameExpr, o, f)); @@ -3132,9 +3066,9 @@ static Type NormalizeToVerificationTypeRepresentation(Type type) { // Translates a type into the representation Boogie type, // c.f. TypeToTy which translates a type to its Boogie expression // to be used in $Is and $IsAlloc. - Bpl.Type TrType(Type type) { + public Bpl.Type TrType(Type type) { Contract.Requires(type != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Ensures(Contract.Result() != null); type = NormalizeToVerificationTypeRepresentation(type); @@ -3142,40 +3076,40 @@ Bpl.Type TrType(Type type) { if (type is BoolType) { return Bpl.Type.Bool; } else if (type is CharType) { - return predef.CharType; + return Predef.CharType; } else if (type is IntType) { return Bpl.Type.Int; } else if (type is RealType) { return Bpl.Type.Real; } else if (type is BigOrdinalType) { - return predef.BigOrdinalType; + return Predef.BigOrdinalType; } else if (type is BitvectorType) { var t = (BitvectorType)type; return BplBvType(t.Width); } else if (type is IteratorDecl.EverIncreasingType) { return Bpl.Type.Int; } else if (type is ArrowType) { - return predef.HandleType; + return Predef.HandleType; } else if (type.IsTypeParameter || type.IsAbstractType) { - return predef.BoxType; + return Predef.BoxType; } else if (type.IsInternalTypeSynonym) { - return predef.BoxType; + return Predef.BoxType; } else if (type.IsRefType) { // object and class types translate to ref - return predef.RefType; + return Predef.RefType; } else if (type is UserDefinedType { ResolvedClass: TraitDecl }) { // non-reference trait type - return predef.BoxType; + return Predef.BoxType; } else if (type.IsDatatype) { - return predef.DatatypeType; + return Predef.DatatypeType; } else if (type is SetType) { - return ((SetType)type).Finite ? predef.SetType : predef.ISetType; + return ((SetType)type).Finite ? Predef.SetType : Predef.ISetType; } else if (type is MultiSetType) { - return predef.MultiSetType; + return Predef.MultiSetType; } else if (type is MapType) { - return ((MapType)type).Finite ? predef.MapType : predef.IMapType; + return ((MapType)type).Finite ? Predef.MapType : Predef.IMapType; } else if (type is SeqType) { - return predef.SeqType; + return Predef.SeqType; } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected type } @@ -3253,7 +3187,7 @@ public Bpl.Expr BoxIfNotNormallyBoxed(Bpl.IToken tok, Bpl.Expr e, Type t) { public Bpl.Expr ApplyBox(Bpl.IToken tok, Bpl.Expr e) { Contract.Assert(tok != null); Contract.Assert(e != null); - if (e.Type == predef.BoxType || e is NAryExpr { Fun.FunctionName: "$Box" }) { + if (e.Type == Predef.BoxType || e is NAryExpr { Fun.FunctionName: "$Box" }) { return e; } return FunctionCall(tok, BuiltinFunction.Box, null, e); @@ -3273,7 +3207,7 @@ public Bpl.Expr UnboxUnlessInherentlyBoxed(Bpl.Expr e, Type t) { } public Expr UnboxUnlessBoxType(IToken tok, Expr e, Type type) { - return TrType(type) == predef.BoxType ? e : ApplyUnbox(tok, e, TrType(type)); + return TrType(type) == Predef.BoxType ? e : ApplyUnbox(tok, e, TrType(type)); } /// @@ -3283,8 +3217,8 @@ public Bpl.Expr ApplyUnbox(Bpl.IToken tok, Bpl.Expr e, Bpl.Type ty) { Contract.Assert(e != null); Contract.Assert(ty != null); Contract.Assert(tok != null); - Contract.Assert((e.Type != null && e.Type.Equals(predef.BoxType) || - (e.ShallowType != null && e.ShallowType.Equals(predef.BoxType)))); + Contract.Assert((e.Type != null && e.Type.Equals(Predef.BoxType) || + (e.ShallowType != null && e.ShallowType.Equals(Predef.BoxType)))); return FunctionCall(tok, BuiltinFunction.Unbox, ty, e); } @@ -3429,13 +3363,13 @@ Bpl.Requires Requires(IToken tok, bool free, Expression dafnyCondition, Bpl.Expr return req; } - Bpl.StmtList TrStmt2StmtList(BoogieStmtListBuilder builder, + public Bpl.StmtList TrStmt2StmtList(BoogieStmtListBuilder builder, Statement block, Variables locals, ExpressionTranslator etran, bool introduceScope = false) { Contract.Requires(builder != null); Contract.Requires(block != null); Contract.Requires(locals != null); Contract.Requires(etran != null); - Contract.Requires(codeContext != null && predef != null); + Contract.Requires(codeContext != null && Predef != null); Contract.Ensures(Contract.Result() != null); TrStmtList(new List { block }, builder, locals, etran, introduceScope ? block.RangeToken : null, processLabels: false); @@ -3542,10 +3476,10 @@ Dictionary SetupBoundVarsAsLocals(List boundVar foreach (BoundVar bv in boundVars) { LocalVariable local = new LocalVariable(bv.RangeToken, nameSuffix == null ? bv.Name : bv.Name + nameSuffix, bv.Type, bv.IsGhost); local.type = local.SyntacticType; // resolve local here - IdentifierExpr ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)); + IdentifierExpr ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(CurrentDeclaration.IdGenerator)); ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here substMap.Add(bv, ie); - Bpl.LocalVariable bvar = new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), TrType(local.Type))); + Bpl.LocalVariable bvar = new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(local.Type))); locals.GetOrAdd(bvar); var bIe = new Bpl.IdentifierExpr(bvar.tok, bvar); builder.Add(new Bpl.HavocCmd(bv.tok, new List { bIe })); @@ -3587,11 +3521,11 @@ Bpl.Expr SetupVariableAsLocal(IVariable v, Dictionary sub var local = new LocalVariable(v.RangeToken, v.Name, v.Type, v.IsGhost); local.type = local.SyntacticType; // resolve local here - var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator)); + var ie = new IdentifierExpr(local.Tok, local.AssignUniqueName(CurrentDeclaration.IdGenerator)); ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here substMap.Add(v, ie); - var bvar = new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), TrType(local.Type))); + var bvar = new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(local.Type))); locals.GetOrAdd(bvar); var bIe = new Bpl.IdentifierExpr(bvar.tok, bvar); builder.Add(new Bpl.HavocCmd(v.Tok, new List { bIe })); @@ -3621,7 +3555,7 @@ Bpl.Expr SetupVariableAsLocal(IVariable v, Dictionary sub } - void AddComment(BoogieStmtListBuilder builder, Statement stmt, string comment) { + public void AddComment(BoogieStmtListBuilder builder, Statement stmt, string comment) { Contract.Requires(builder != null); Contract.Requires(stmt != null); Contract.Requires(comment != null); @@ -3639,7 +3573,7 @@ Bpl.Expr GetExtendedWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTra Contract.Requires(x != null); Contract.Requires(type != null); Contract.Requires(etran != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); var r = GetWhereClause(tok, x, type, etran, alloc); type = type.NormalizeExpand(); if (type.IsDatatype) { @@ -3672,29 +3606,29 @@ Bpl.Expr TypeToTy(Type type) { return ClassTyCon(((UserDefinedType)type), args); } else if (type is SetType) { bool finite = ((SetType)type).Finite; - return FunctionCall(Token.NoToken, finite ? "TSet" : "TISet", predef.Ty, TypeToTy(((CollectionType)type).Arg)); + return FunctionCall(Token.NoToken, finite ? "TSet" : "TISet", Predef.Ty, TypeToTy(((CollectionType)type).Arg)); } else if (type is MultiSetType) { - return FunctionCall(Token.NoToken, "TMultiSet", predef.Ty, TypeToTy(((CollectionType)type).Arg)); + return FunctionCall(Token.NoToken, "TMultiSet", Predef.Ty, TypeToTy(((CollectionType)type).Arg)); } else if (type is SeqType) { - return FunctionCall(Token.NoToken, "TSeq", predef.Ty, TypeToTy(((CollectionType)type).Arg)); + return FunctionCall(Token.NoToken, "TSeq", Predef.Ty, TypeToTy(((CollectionType)type).Arg)); } else if (type is MapType) { bool finite = ((MapType)type).Finite; - return FunctionCall(Token.NoToken, finite ? "TMap" : "TIMap", predef.Ty, + return FunctionCall(Token.NoToken, finite ? "TMap" : "TIMap", Predef.Ty, TypeToTy(((MapType)type).Domain), TypeToTy(((MapType)type).Range)); } else if (type is BoolType) { - return new Bpl.IdentifierExpr(Token.NoToken, "TBool", predef.Ty); + return new Bpl.IdentifierExpr(Token.NoToken, "TBool", Predef.Ty); } else if (type is CharType) { - return new Bpl.IdentifierExpr(Token.NoToken, "TChar", predef.Ty); + return new Bpl.IdentifierExpr(Token.NoToken, "TChar", Predef.Ty); } else if (type is RealType) { - return new Bpl.IdentifierExpr(Token.NoToken, "TReal", predef.Ty); + return new Bpl.IdentifierExpr(Token.NoToken, "TReal", Predef.Ty); } else if (type is BitvectorType) { var t = (BitvectorType)type; - return FunctionCall(Token.NoToken, "TBitvector", predef.Ty, Bpl.Expr.Literal(t.Width)); + return FunctionCall(Token.NoToken, "TBitvector", Predef.Ty, Bpl.Expr.Literal(t.Width)); } else if (type is IntType) { - return new Bpl.IdentifierExpr(Token.NoToken, "TInt", predef.Ty); + return new Bpl.IdentifierExpr(Token.NoToken, "TInt", Predef.Ty); } else if (type is BigOrdinalType) { - return new Bpl.IdentifierExpr(Token.NoToken, "TORDINAL", predef.Ty); + return new Bpl.IdentifierExpr(Token.NoToken, "TORDINAL", Predef.Ty); } else if (type is ParamTypeProxy) { return TrTypeParameter(((ParamTypeProxy)type).orig); } else { @@ -3714,7 +3648,7 @@ static string NameTypeParam(TypeParameter tp) { Bpl.Expr TrTypeParameter(TypeParameter tp) { var nm = NameTypeParam(tp); // return an identifier denoting a constant - return new Bpl.IdentifierExpr(tp.tok, nm, predef.Ty); + return new Bpl.IdentifierExpr(tp.tok, nm, Predef.Ty); } Bpl.Expr TrAbstractType(AbstractTypeDecl abstractType, List tyArguments) { @@ -3722,7 +3656,7 @@ Bpl.Expr TrAbstractType(AbstractTypeDecl abstractType, List tyArguments) { var fn = GetOrCreateTypeConstructor(abstractType); var args = tyArguments.ConvertAll(TypeToTy); - return FunctionCall(abstractType.tok, fn.Name, predef.Ty, args); + return FunctionCall(abstractType.tok, fn.Name, Predef.Ty, args); } public List GetTypeParams(IMethodCodeContext cc) { @@ -3796,13 +3730,13 @@ Bpl.Expr MkIsAlloc(Bpl.Expr x, Bpl.Expr t, Bpl.Expr h, bool box = false) { /// To do this in Dafny, Dafny would have to compute loop targets, which is better done in Boogie (which /// already has to do it). /// - Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran, IsAllocType alloc, + public Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran, IsAllocType alloc, bool allocatednessOnly = false, bool alwaysUseSymbolicName = false) { Contract.Requires(tok != null); Contract.Requires(x != null); Contract.Requires(type != null); Contract.Requires(etran != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); if (type.NormalizeExpand() is TypeProxy) { // Unresolved proxy @@ -4004,7 +3938,7 @@ Bpl.Expr GetSubrangeCheck( return cre; } - void CheckSubrange(IToken tok, Bpl.Expr bSource, Type sourceType, Type targetType, Expression source, BoogieStmtListBuilder builder, string errorMsgPrefix = "") { + public void CheckSubrange(IToken tok, Bpl.Expr bSource, Type sourceType, Type targetType, Expression source, BoogieStmtListBuilder builder, string errorMsgPrefix = "") { Contract.Requires(tok != null); Contract.Requires(bSource != null); Contract.Requires(sourceType != null); @@ -4030,7 +3964,7 @@ void Check_NewRestrictions(IToken tok, Expression dObj, Bpl.Expr obj, Field f, B // assert Set#Subset(rhs, obj._new); var fId = new Bpl.IdentifierExpr(tok, GetField(f)); var subset = FunctionCall(tok, BuiltinFunction.SetSubset, null, rhs, - ApplyUnbox(tok, ReadHeap(tok, etran.HeapExpr, obj, fId), predef.SetType)); + ApplyUnbox(tok, ReadHeap(tok, etran.HeapExpr, obj, fId), Predef.SetType)); builder.Add(Assert(tok, subset, new AssignmentShrinks(dObj, f.Name), builder.Context)); } } @@ -4063,7 +3997,7 @@ void CreateMapComprehensionProjectionFunctions(MapComprehension mc) { } int projectionFunctionCount = 0; - private Declaration currentDeclaration; + public Declaration CurrentDeclaration; // ----- Expression --------------------------------------------------------------------------- @@ -4230,7 +4164,7 @@ public FuelSetting WithContext(CustomFuelSettings settings) { public Bpl.Expr LayerZero() { Contract.Ensures(Contract.Result() != null); - return new Bpl.IdentifierExpr(Token.NoToken, "$LZ", boogieGenerator.predef.LayerType); + return new Bpl.IdentifierExpr(Token.NoToken, "$LZ", boogieGenerator.Predef.LayerType); } public Bpl.Expr LayerN(int n) { @@ -4441,10 +4375,8 @@ public static FuelContext PopFuelContext() { } } - - internal enum IsAllocType { ISALLOC, NOALLOC, NEVERALLOC }; // NEVERALLOC is like NOALLOC, but overrides AlwaysAlloc - static IsAllocType ISALLOC { get { return IsAllocType.ISALLOC; } } - static IsAllocType NOALLOC { get { return IsAllocType.NOALLOC; } } + public static IsAllocType ISALLOC { get { return IsAllocType.ISALLOC; } } + public static IsAllocType NOALLOC { get { return IsAllocType.NOALLOC; } } private bool DisableNonLinearArithmetic => DetermineDisableNonLinearArithmetic(forModule, options); private int ArithmeticSolver { get { @@ -4581,7 +4513,7 @@ Bpl.Trigger TrTrigger(ExpressionTranslator etran, Attributes attribs, IToken tok bool useFuelAsQuantifier = argsEtran.Statistics_CustomLayerFunctionCount > 0; bool useHeapAsQuantifier = argsEtran.Statistics_HeapAsQuantifierCount > 0; if (useHeapAsQuantifier) { - var heapExpr = BplBoundVar(CurrentIdGenerator.FreshId("tr$heap#"), predef.HeapType, bvars); + var heapExpr = BplBoundVar(CurrentIdGenerator.FreshId("tr$heap#"), Predef.HeapType, bvars); argsEtran = new ExpressionTranslator(argsEtran, heapExpr); } @@ -4820,7 +4752,7 @@ public override BinderExpr VisitBinderExpr(BinderExpr node) { var vars = new List(); exprs = new List(); foreach (TypeParameter v in args) { - vars.Add(BplBoundVar(NameTypeParam(v), predef.Ty, out var e)); + vars.Add(BplBoundVar(NameTypeParam(v), Predef.Ty, out var e)); exprs.Add(e); } return vars; @@ -4836,8 +4768,8 @@ List MkTyParamFormals(List args, bool includeWhereClaus var vars = new List(); exprs = new List(); foreach (TypeParameter v in args) { - var whereClause = includeWhereClause ? GetTyWhereClause(new Bpl.IdentifierExpr(v.tok, NameTypeParam(v), predef.Ty), v.Characteristics) : null; - vars.Add(BplFormalVar(named ? NameTypeParam(v) : null, predef.Ty, true, out var e, whereClause)); + var whereClause = includeWhereClause ? GetTyWhereClause(new Bpl.IdentifierExpr(v.tok, NameTypeParam(v), Predef.Ty), v.Characteristics) : null; + vars.Add(BplFormalVar(named ? NameTypeParam(v) : null, Predef.Ty, true, out var e, whereClause)); exprs.Add(e); } return vars; @@ -4870,3 +4802,4 @@ public Expr GetRevealConstant(Function f) { public enum AssertMode { Keep, Assume, Check } } +public enum IsAllocType { ISALLOC, NOALLOC, NEVERALLOC }; // NEVERALLOC is like NOALLOC, but overrides AlwaysAlloc diff --git a/Source/DafnyCore/Verifier/Datatypes/BoogieGenerator.DataTypes.cs b/Source/DafnyCore/Verifier/Datatypes/BoogieGenerator.DataTypes.cs index d89e515ed34..ac396367510 100644 --- a/Source/DafnyCore/Verifier/Datatypes/BoogieGenerator.DataTypes.cs +++ b/Source/DafnyCore/Verifier/Datatypes/BoogieGenerator.DataTypes.cs @@ -14,7 +14,7 @@ namespace Microsoft.Dafny { partial class BoogieGenerator { void AddDatatype(DatatypeDecl dt) { Contract.Requires(dt != null); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); var mayInvolveReferences = UserDefinedType.FromTopLevelDecl(dt.tok, dt).MayInvolveReferences; var constructorFunctions = dt.Ctors.ToDictionary(ctor => ctor, ctor => AddDataTypeConstructor(dt, ctor, mayInvolveReferences)); @@ -85,15 +85,15 @@ private void AddInductiveDatatypeAxioms(Dictionary c var dtEqualName = DtEqualName(dt); var args = new List(); - args.Add(new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), false)); - args.Add(new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), false)); + args.Add(new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Predef.DatatypeType), false)); + args.Add(new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Predef.DatatypeType), false)); var ctorEqualResult = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false); sink.AddTopLevelDeclaration(new Bpl.Function(dt.tok, dtEqualName, args, ctorEqualResult, "Datatype extensional equality declaration")); - var aVar = BplBoundVar("a", predef.DatatypeType, out var a); - var bVar = BplBoundVar("b", predef.DatatypeType, out var b); + var aVar = BplBoundVar("a", Predef.DatatypeType, out var a); + var bVar = BplBoundVar("b", Predef.DatatypeType, out var b); var dtEqual = FunctionCall(dt.tok, dtEqualName, Bpl.Type.Bool, a, b); @@ -137,8 +137,8 @@ private static string DtEqualName(IndDatatypeDecl dt) { private void AddExtensionalityAxiom(IndDatatypeDecl dt) { var dtEqualName = DtEqualName(dt); { - var aVar = BplBoundVar("a", predef.DatatypeType, out var a); - var bVar = BplBoundVar("b", predef.DatatypeType, out var b); + var aVar = BplBoundVar("a", Predef.DatatypeType, out var a); + var bVar = BplBoundVar("b", Predef.DatatypeType, out var b); var lhs = FunctionCall(dt.tok, dtEqualName, Bpl.Type.Bool, a, b); var rhs = Bpl.Expr.Eq(a, b); @@ -199,9 +199,9 @@ private void AddCoDatatypeDeclAxioms(CoDatatypeDecl codecl) { kIsLimit = Bpl.Expr.True; } - var ly = BplBoundVar("ly", predef.LayerType, vars); - var d0 = BplBoundVar("d0", predef.DatatypeType, vars); - var d1 = BplBoundVar("d1", predef.DatatypeType, vars); + var ly = BplBoundVar("ly", Predef.LayerType, vars); + var d0 = BplBoundVar("d0", Predef.DatatypeType, vars); + var d1 = BplBoundVar("d1", Predef.DatatypeType, vars); K(tyargs, vars, lexprs, rexprs, kVar, k, kIsValid, kIsNonZero, kHasSuccessor, kIsLimit, ly, d0, d1); }; @@ -214,9 +214,9 @@ private void AddCoDatatypeDeclAxioms(CoDatatypeDecl codecl) { args.Add(BplFormalVar(null, typeOfK, true)); } - args.Add(BplFormalVar(null, predef.LayerType, true)); - args.Add(BplFormalVar(null, predef.DatatypeType, true)); - args.Add(BplFormalVar(null, predef.DatatypeType, true)); + args.Add(BplFormalVar(null, Predef.LayerType, true)); + args.Add(BplFormalVar(null, Predef.DatatypeType, true)); + args.Add(BplFormalVar(null, Predef.DatatypeType, true)); var r = BplFormalVar(null, Bpl.Type.Bool, false); var fn_nm = typeOfK != null ? CoPrefixName(codecl) : CoEqualName(codecl); var fn = new Bpl.Function(codecl.tok, fn_nm, args, r); @@ -281,8 +281,8 @@ private void AddCoDatatypeDeclAxioms(CoDatatypeDecl codecl) { "Equality for codatatypes")); }); - Bpl.Type theTypeOfK = predef.BigOrdinalType; - AddAxioms(predef.BigOrdinalType); // Add the above axioms for $PrefixEqual + Bpl.Type theTypeOfK = Predef.BigOrdinalType; + AddAxioms(Predef.BigOrdinalType); // Add the above axioms for $PrefixEqual // The connection between the full codatatype equality and its prefix version // axiom (forall d0, d1: DatatypeType :: $Eq#Dt(d0, d1) <==> @@ -302,7 +302,7 @@ private void AddCoDatatypeDeclAxioms(CoDatatypeDecl codecl) { CoAxHelper(Bpl.Type.Int, (tyargs, vars, lexprs, rexprs, kVar, k, kIsValid, kIsNonZero, kHasSuccessor, kIsLimit, ly, d0, d1) => { var Eq = CoEqualCall(codecl, lexprs, rexprs, null, LayerSucc(ly), d0, d1); - var PEq = CoEqualCall(codecl, lexprs, rexprs, FunctionCall(k.tok, "ORD#FromNat", predef.BigOrdinalType, k), + var PEq = CoEqualCall(codecl, lexprs, rexprs, FunctionCall(k.tok, "ORD#FromNat", Predef.BigOrdinalType, k), LayerSucc(ly), d0, d1); vars.Remove(kVar); AddOtherDefinition(GetOrCreateTypeConstructor(codecl), new Axiom(codecl.tok, @@ -350,7 +350,7 @@ private void AddDepthOneCaseSplitFunction(DatatypeDecl dt) { // function $IsA#Dt(G: Ty,d: DatatypeType): bool { // Dt.Ctor0?(G, d) || Dt.Ctor1?(G, d) || ... // } - var cases_dBv = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), true); + var cases_dBv = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Predef.DatatypeType), true); var cases_resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false); var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.FullSanitizedName, new List { cases_dBv }, @@ -363,7 +363,7 @@ private void AddDepthOneCaseSplitFunction(DatatypeDecl dt) { sink.AddTopLevelDeclaration(cases_fn); // and here comes the actual axiom: - var dVar = BplBoundVar("d", predef.DatatypeType, out var d); + var dVar = BplBoundVar("d", Predef.DatatypeType, out var d); var lhs = FunctionCall(dt.tok, cases_fn.Name, Bpl.Type.Bool, d); Bpl.Expr cases_body = Bpl.Expr.False; foreach (DatatypeCtor ctor in dt.Ctors) { @@ -386,10 +386,10 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, } Bpl.Variable resType = new Bpl.Formal(ctor.tok, - new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), false); + new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, Predef.DatatypeType), false); Bpl.Function fn; if (dt is TupleTypeDecl ttd && ttd.Dims == 2 && ttd.NonGhostDims == 2) { - fn = predef.Tuple2Constructor; + fn = Predef.Tuple2Constructor; } else { fn = new Bpl.Function(ctor.tok, ctor.FullName, argTypes, resType, "Constructor function declaration"); sink.AddTopLevelDeclaration(fn); @@ -404,7 +404,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, // Add: const unique ##dt.ctor: DtCtorId; var definitionAxioms = new List(); Bpl.Constant constructorId = new Bpl.Constant(ctor.tok, - new Bpl.TypedIdent(ctor.tok, "#" + ctor.FullName, predef.DtCtorId), true, + new Bpl.TypedIdent(ctor.tok, "#" + ctor.FullName, Predef.DtCtorId), true, definitionAxioms: definitionAxioms); Bpl.Expr constructorIdReference = new Bpl.IdentifierExpr(ctor.tok, constructorId); var constructorIdentifierAxiom = CreateConstructorIdentifierAxiom(ctor, constructorIdReference); @@ -419,7 +419,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, // and here comes the associated axiom: - var thVar = BplBoundVar("d", predef.DatatypeType, out var th); + var thVar = BplBoundVar("d", Predef.DatatypeType, out var th); var queryPredicate = FunctionCall(ctor.tok, queryField.Name, Bpl.Type.Bool, th); var ctorId = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, th); var rhs = Bpl.Expr.Eq(ctorId, constructorIdReference); @@ -437,8 +437,8 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, { // Add: axiom (forall d: DatatypeType :: dt.ctor?(d) ==> (exists params :: d == #dt.ctor(params)); CreateBoundVariables(ctor.Formals, out var bvs, out var args); - Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); - var dBv = BplBoundVar("d", predef.DatatypeType, out var dId); + Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); + var dBv = BplBoundVar("d", Predef.DatatypeType, out var dId); Bpl.Expr q = Bpl.Expr.Eq(dId, rhs); if (bvs.Count != 0) { q = new Bpl.ExistsExpr(ctor.tok, bvs, null /*always in a Skolemization context*/, q); @@ -461,8 +461,8 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, litargs.Add(Lit(arg)); } - Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, litargs); - Bpl.Expr rhs = Lit(FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args), predef.DatatypeType); + Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, litargs); + Bpl.Expr rhs = Lit(FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args), Predef.DatatypeType); Bpl.Expr q = BplForall(bvs, BplTrigger(lhs), Bpl.Expr.Eq(lhs, rhs)); var constructorLiteralAxiom = new Bpl.Axiom(ctor.tok, q, "Constructor literal"); AddOtherDefinition(fn, constructorLiteralAxiom); @@ -475,7 +475,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, var sf = ctor.Destructors[i]; Contract.Assert(sf != null); fn = GetReadonlyField(sf); - if (fn == predef.Tuple2Destructors0 || fn == predef.Tuple2Destructors1) { + if (fn == Predef.Tuple2Destructors0 || fn == Predef.Tuple2Destructors1) { // the two destructors for 2-tuples are predefined in Prelude for use // by the Map#Items axiom } else if (sf.EnclosingCtors[0] != ctor) { @@ -486,7 +486,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, // axiom (forall params :: ##dt.ctor#i(#dt.ctor(params)) == params_i); CreateBoundVariables(ctor.Formals, out var bvs, out var args); - var inner = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); + var inner = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); var outer = FunctionCall(ctor.tok, fn.Name, TrType(arg.Type), inner); var q = BplForall(bvs, BplTrigger(inner), Bpl.Expr.Eq(outer, args[i])); AddOtherDefinition(fn, (new Bpl.Axiom(ctor.tok, q, "Constructor injectivity"))); @@ -503,7 +503,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, argType.IsDatatype ? args[i] : FunctionCall(ctor.tok, BuiltinFunction.Unbox, predef.DatatypeType, args[i])); */ - Bpl.Expr ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); + Bpl.Expr ct = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct); var trigger = BplTrigger(ct); q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Lt(lhs, rhs)); @@ -520,10 +520,10 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, Bpl.Expr ante = BplAnd( Bpl.Expr.Le(Bpl.Expr.Literal(0), ie), Bpl.Expr.Lt(ie, FunctionCall(arg.tok, BuiltinFunction.SeqLength, null, args[i]))); - var seqIndex = FunctionCall(arg.tok, BuiltinFunction.SeqIndex, predef.DatatypeType, args[i], ie); + var seqIndex = FunctionCall(arg.tok, BuiltinFunction.SeqIndex, Predef.DatatypeType, args[i], ie); Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, - FunctionCall(arg.tok, BuiltinFunction.Unbox, predef.DatatypeType, seqIndex)); - var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); + FunctionCall(arg.tok, BuiltinFunction.Unbox, Predef.DatatypeType, seqIndex)); + var ct = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct); q = new Bpl.ForallExpr(ctor.tok, bvs, new Trigger(lhs.tok, true, new List { seqIndex, ct }), BplImp(ante, Bpl.Expr.Lt(lhs, rhs))); @@ -534,7 +534,7 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, { CreateBoundVariables(ctor.Formals, out bvs, out args); var lhs = FunctionCall(ctor.tok, BuiltinFunction.SeqRank, null, args[i]); - var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); + var ct = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct); var trigger = BplTrigger(ct); q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, Bpl.Expr.Lt(lhs, rhs)); @@ -545,12 +545,12 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, // that is: // axiom (forall params, d: Datatype {arg[Box(d)], #dt.ctor(params)} :: arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params))); CreateBoundVariables(ctor.Formals, out bvs, out args); - Bpl.Variable dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", predef.DatatypeType)); + Bpl.Variable dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", Predef.DatatypeType)); bvs.Add(dVar); Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, dVar); Bpl.Expr inSet = Bpl.Expr.SelectTok(arg.tok, args[i], FunctionCall(arg.tok, BuiltinFunction.Box, null, ie)); Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ie); - var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); + var ct = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct); var trigger = new Bpl.Trigger(ctor.tok, true, new List { inSet, ct }); q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(inSet, Bpl.Expr.Lt(lhs, rhs))); @@ -560,13 +560,13 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, // that is: // axiom (forall params, d: Datatype {arg[Box(d)], #dt.ctor(params)} :: 0 < arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params))); CreateBoundVariables(ctor.Formals, out bvs, out args); - Bpl.Variable dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", predef.DatatypeType)); + Bpl.Variable dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", Predef.DatatypeType)); bvs.Add(dVar); Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, dVar); var inMultiset = Bpl.Expr.SelectTok(arg.tok, args[i], FunctionCall(arg.tok, BuiltinFunction.Box, null, ie)); Bpl.Expr ante = Bpl.Expr.Gt(inMultiset, Bpl.Expr.Literal(0)); Bpl.Expr lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ie); - var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); + var ct = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct); var trigger = new Bpl.Trigger(ctor.tok, true, new List { inMultiset, ct }); q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(ante, Bpl.Expr.Lt(lhs, rhs))); @@ -578,15 +578,15 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, // { Map#Domain(arg)[$Box(d)], #dt.ctor(params) } // Map#Domain(arg)[$Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params))); CreateBoundVariables(ctor.Formals, out bvs, out args); - var dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", predef.DatatypeType)); + var dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", Predef.DatatypeType)); bvs.Add(dVar); var ie = new Bpl.IdentifierExpr(arg.tok, dVar); var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain; - var domain = FunctionCall(arg.tok, f, finite ? predef.MapType : predef.IMapType, + var domain = FunctionCall(arg.tok, f, finite ? Predef.MapType : Predef.IMapType, args[i]); var inDomain = Bpl.Expr.SelectTok(arg.tok, domain, FunctionCall(arg.tok, BuiltinFunction.Box, null, ie)); var lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ie); - var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); + var ct = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct); var trigger = new Bpl.Trigger(ctor.tok, true, new List { inDomain, ct }); q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(inDomain, Bpl.Expr.Lt(lhs, rhs))); @@ -597,20 +597,20 @@ private Bpl.Function AddDataTypeConstructor(DatatypeDecl dt, DatatypeCtor ctor, // { Map#Elements(arg)[bx], #dt.ctor(params) } // Map#Domain(arg)[bx] ==> DtRank($Unbox(Map#Elements(arg)[bx]): DatatypeType) < DtRank(#dt.ctor(params))); CreateBoundVariables(ctor.Formals, out bvs, out args); - var bxVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "bx", predef.BoxType)); + var bxVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "bx", Predef.BoxType)); bvs.Add(bxVar); var ie = new Bpl.IdentifierExpr(arg.tok, bxVar); var f = finite ? BuiltinFunction.MapDomain : BuiltinFunction.IMapDomain; - var domain = FunctionCall(arg.tok, f, finite ? predef.MapType : predef.IMapType, + var domain = FunctionCall(arg.tok, f, finite ? Predef.MapType : Predef.IMapType, args[i]); var inDomain = Bpl.Expr.SelectTok(arg.tok, domain, ie); var ef = finite ? BuiltinFunction.MapElements : BuiltinFunction.IMapElements; - var element = FunctionCall(arg.tok, ef, finite ? predef.MapType : predef.IMapType, + var element = FunctionCall(arg.tok, ef, finite ? Predef.MapType : Predef.IMapType, args[i]); var elmt = Bpl.Expr.SelectTok(arg.tok, element, ie); - var unboxElmt = FunctionCall(arg.tok, BuiltinFunction.Unbox, predef.DatatypeType, elmt); + var unboxElmt = FunctionCall(arg.tok, BuiltinFunction.Unbox, Predef.DatatypeType, elmt); var lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, unboxElmt); - var ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); + var ct = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); var rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ct); var trigger = new Bpl.Trigger(ctor.tok, true, new List { inDomain, ct }); q = new Bpl.ForallExpr(ctor.tok, bvs, trigger, BplImp(inDomain, Bpl.Expr.Lt(lhs, rhs))); @@ -627,7 +627,7 @@ private void AddConstructorAxioms(DatatypeDecl dt, DatatypeCtor ctor, Bpl.Functi var tyvars = MkTyParamBinders(dt.TypeArgs, out var tyexprs); CreateBoundVariables(ctor.Formals, out var bvs, out var args); bvs.InsertRange(0, tyvars); - var c_params = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); + var c_params = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); var c_ty = ClassTyCon(dt, tyexprs); AddsIsConstructorAxiom(ctor, ctorFunction, args, bvs, c_params, c_ty); if (includeIsAllocAxiom) { @@ -645,7 +645,7 @@ private void AddConstructorAxioms(DatatypeDecl dt, DatatypeCtor ctor, Bpl.Functi */ private void AddIsAllocConstructorAxiom(DatatypeDecl dt, DatatypeCtor ctor, Bpl.Function ctorFunction, List args, List bvs, NAryExpr c_params, Expr c_ty) { - var hVar = BplBoundVar("$h", predef.HeapType, out var h); + var hVar = BplBoundVar("$h", Predef.HeapType, out var h); Bpl.Expr conj = Bpl.Expr.True; for (var i = 0; i < ctor.Formals.Count; i++) { @@ -678,7 +678,7 @@ private void AddCommonIsAllocConstructorAxiom(DatatypeDecl dt) { MkIsPredicateForDatatype(dt, out var boundVariables, out var d, out var tyExpr, out var isPredicate); - var hVar = BplBoundVar("$h", predef.HeapType, out var h); + var hVar = BplBoundVar("$h", Predef.HeapType, out var h); var isGoodHeap = FunctionCall(dt.tok, BuiltinFunction.IsGoodHeap, null, h); var isAlloc = MkIsAlloc(d, tyExpr, h); @@ -705,7 +705,7 @@ private void AddCommonIsAllocConstructorAxiom(DatatypeDecl dt) { private void MkIsPredicateForDatatype(DatatypeDecl datatypeDecl, out List boundVariables, out Bpl.Expr varExpression, out Bpl.Expr typeExpression, out Bpl.Expr isPredicate) { var typeVariables = MkTyParamBinders(datatypeDecl.TypeArgs, out var typeExpressions); - var dVar = BplBoundVar("d", predef.DatatypeType, out varExpression); + var dVar = BplBoundVar("d", Predef.DatatypeType, out varExpression); boundVariables = Snoc(typeVariables, dVar); typeExpression = ClassTyCon(datatypeDecl, typeExpressions); isPredicate = MkIs(varExpression, typeExpression); @@ -721,11 +721,11 @@ private void MkIsPredicateForDatatype(DatatypeDecl datatypeDecl, out List tyvars, Expr c_ty) { - var hVar = BplBoundVar("$h", predef.HeapType, out var h); + var hVar = BplBoundVar("$h", Predef.HeapType, out var h); for (int i = 0; i < ctor.Formals.Count; i++) { var arg = ctor.Formals[i]; var dtor = GetReadonlyField(ctor.Destructors[i]); - var dBv = BplBoundVar("d", predef.DatatypeType, out var dId); + var dBv = BplBoundVar("d", Predef.DatatypeType, out var dId); var isGoodHeap = FunctionCall(ctor.tok, BuiltinFunction.IsGoodHeap, null, h); Bpl.Expr dtq = FunctionCall(ctor.tok, ctor.QueryField.FullSanitizedName, Bpl.Type.Bool, dId); var c_alloc = MkIsAlloc(dId, c_ty, h); @@ -786,7 +786,7 @@ private void AddsIsConstructorAxiom(DatatypeCtor ctor, Bpl.Function ctorFunction private Axiom CreateConstructorIdentifierAxiom(DatatypeCtor ctor, Expr c) { // Add: axiom (forall params :: DatatypeCtorId(#dt.ctor(params)) == ##dt.ctor); CreateBoundVariables(ctor.Formals, out var bvs, out var args); - var constructorCall = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args); + var constructorCall = FunctionCall(ctor.tok, ctor.FullName, Predef.DatatypeType, args); var lhs = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, constructorCall); Bpl.Expr q = Bpl.Expr.Eq(lhs, c); var trigger = BplTrigger(constructorCall); @@ -796,7 +796,7 @@ private Axiom CreateConstructorIdentifierAxiom(DatatypeCtor ctor, Expr c) { void AddWellformednessCheck(DatatypeCtor ctor) { Contract.Requires(ctor != null); - Contract.Requires(sink != null && predef != null); + Contract.Requires(sink != null && Predef != null); Contract.Requires(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null); Contract.Ensures(currentModule == null && codeContext == null && isAllocContext == null && fuelContext == null); @@ -815,7 +815,7 @@ void AddWellformednessCheck(DatatypeCtor ctor) { currentModule = ctor.EnclosingDatatype.EnclosingModuleDefinition; codeContext = ctor.EnclosingDatatype; fuelContext = FuelSetting.NewFuelContext(ctor.EnclosingDatatype); - var etran = new ExpressionTranslator(this, predef, ctor.tok, null); + var etran = new ExpressionTranslator(this, Predef, ctor.tok, null); // parameters of the procedure List inParams = MkTyParamFormals(GetTypeParams(ctor.EnclosingDatatype), true); diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrAssignment.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrAssignment.cs index 0d78e61af61..3f22ad98b84 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrAssignment.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrAssignment.cs @@ -22,7 +22,7 @@ void TrAssignment(Statement stmt, Expression lhs, AssignmentRhs rhs, Contract.Requires(rhs != null); Contract.Requires(builder != null); Contract.Requires(etran != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); var lhss = new List() { lhs }; ProcessLhss(lhss, rhs.CanAffectPreviouslyKnownExpressions, true, builder, locals, etran, stmt, @@ -43,7 +43,7 @@ void ProcessRhss(List lhsBuilder, List(); for (int i = 0; i < lhss.Count; i++) { @@ -94,7 +94,7 @@ void ProcessRhss(List lhsBuilder, List>(), i => i != null)); var finalRhss = new List(); @@ -140,7 +140,7 @@ private void CheckLhssDistinctness(List rhs, List rhsOr Contract.Requires(lhss.Count == rhsOriginal.Count); Contract.Requires(builder != null); Contract.Requires(etran != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); for (int i = 0; i < lhss.Count; i++) { var lhs = lhss[i]; @@ -196,7 +196,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi Contract.Requires(cce.NonNullElements(lhss)); Contract.Requires(builder != null); Contract.Requires(etran != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Ensures(Contract.ValueAtReturn(out lhsBuilders).Count == lhss.Count); Contract.Ensures(Contract.ValueAtReturn(out lhsBuilders).Count == Contract.ValueAtReturn(out bLhss).Count); @@ -259,7 +259,7 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi var useSurrogateLocal = inBodyInitContext && Expression.AsThis(fse.Obj) != null; var obj = SaveInTemp(etran.TrExpr(fse.Obj), rhsCanAffectPreviouslyKnownExpressions, - "$obj" + i, predef.RefType, builder, locals); + "$obj" + i, Predef.RefType, builder, locals); prevObj[i] = obj; if (!useSurrogateLocal) { // check that the enclosing modifies clause allows this object to be written: assert $_ModifiesFrame[obj]); @@ -305,11 +305,11 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi Contract.Assert(sel.Seq.Type != null && sel.Seq.Type.IsArrayType); Contract.Assert(sel.E0 != null); var obj = SaveInTemp(etran.TrExpr(sel.Seq), rhsCanAffectPreviouslyKnownExpressions, - "$obj" + i, predef.RefType, builder, locals); + "$obj" + i, Predef.RefType, builder, locals); var idx = etran.TrExpr(sel.E0); idx = ConvertExpression(sel.E0.tok, idx, sel.E0.Type, Type.Int); var fieldName = SaveInTemp(FunctionCall(tok, BuiltinFunction.IndexField, null, idx), rhsCanAffectPreviouslyKnownExpressions, - "$index" + i, predef.FieldName(tok), builder, locals); + "$index" + i, Predef.FieldName(tok), builder, locals); prevObj[i] = obj; prevIndex[i] = fieldName; // check that the enclosing modifies clause allows this object to be written: assert $_Frame[obj,index]); @@ -333,9 +333,9 @@ void ProcessLhss(List lhss, bool rhsCanAffectPreviouslyKnownExpressi Contract.Assert(mse.Array.Type != null && mse.Array.Type.IsArrayType); var obj = SaveInTemp(etran.TrExpr(mse.Array), rhsCanAffectPreviouslyKnownExpressions, - "$obj" + i, predef.RefType, builder, locals); + "$obj" + i, Predef.RefType, builder, locals); var fieldName = SaveInTemp(etran.GetArrayIndexFieldName(mse.tok, mse.Indices), rhsCanAffectPreviouslyKnownExpressions, - "$index" + i, predef.FieldName(mse.tok), builder, locals); + "$index" + i, Predef.FieldName(mse.tok), builder, locals); prevObj[i] = obj; prevIndex[i] = fieldName; var desc = new Modifiable("an array element", contextModFrames, mse.Array, null); @@ -386,7 +386,7 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs Contract.Requires(builder != null); Contract.Requires(locals != null); Contract.Requires(etran != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Contract.Ensures(Contract.Result() != null); Contract.Ensures(bGivenLhs == null || Contract.Result() == bGivenLhs); @@ -521,10 +521,10 @@ Bpl.Expr TrAssignmentRhs(IToken tok, Bpl.IdentifierExpr bGivenLhs, IVariable lhs if (codeContext is IteratorDecl) { var iter = (IteratorDecl)codeContext; // $Heap[this, _new] := Set#UnionOne($Heap[this, _new], $Box($nw)); - var th = new Bpl.IdentifierExpr(tok, etran.This, predef.RefType); + var th = new Bpl.IdentifierExpr(tok, etran.This, Predef.RefType); var nwField = new Bpl.IdentifierExpr(tok, GetField(iter.Member_New)); - var thisDotNew = ApplyUnbox(tok, ReadHeap(tok, etran.HeapExpr, th, nwField), predef.SetType); - var unionOne = FunctionCall(tok, BuiltinFunction.SetUnionOne, predef.BoxType, thisDotNew, ApplyBox(tok, nw)); + var thisDotNew = ApplyUnbox(tok, ReadHeap(tok, etran.HeapExpr, th, nwField), Predef.SetType); + var unionOne = FunctionCall(tok, BuiltinFunction.SetUnionOne, Predef.BoxType, thisDotNew, ApplyBox(tok, nw)); var heapRhs = UpdateHeap(tok, etran.HeapExpr, th, nwField, unionOne); heapAllocationRecorder = Bpl.Cmd.SimpleAssign(tok, etran.HeapCastToIdentifierExpr, heapRhs); } diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrCall.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrCall.cs index 5110548c1f7..aeb7cadac40 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrCall.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrCall.cs @@ -48,7 +48,7 @@ void TrCallStmt(CallStmt s, BoogieStmtListBuilder builder, Variables locals, Exp Bpl.IdentifierExpr initHeap = null; if (codeContext is IteratorDecl) { // var initHeap := $Heap; - var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, CurrentIdGenerator.FreshId("$initHeapCallStmt#"), predef.HeapType)); + var initHeapVar = new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, CurrentIdGenerator.FreshId("$initHeapCallStmt#"), Predef.HeapType)); locals.Add(initHeapVar); initHeap = new Bpl.IdentifierExpr(s.Tok, initHeapVar); // initHeap := $Heap; @@ -184,7 +184,7 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E var formal = callee.Ins[i]; var local = new LocalVariable(formal.RangeToken, formal.Name + "#", formal.Type.Subst(tySubst), formal.IsGhost); local.type = local.SyntacticType; // resolve local here - var localName = local.AssignUniqueName(currentDeclaration.IdGenerator); + var localName = local.AssignUniqueName(CurrentDeclaration.IdGenerator); var ie = new IdentifierExpr(local.Tok, localName); ie.Var = local; ie.Type = ie.Var.Type; // resolve ie here substMap.Add(formal, ie); @@ -196,12 +196,12 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E if (i == 0 && method is ExtremeLemma && isRecursiveCall) { // Treat this call to M(args) as a call to the corresponding prefix lemma M#(_k - 1, args), so insert an argument here. var k = ((PrefixLemma)callee).K; - var bplK = new Bpl.IdentifierExpr(k.tok, k.AssignUniqueName(currentDeclaration.IdGenerator), TrType(k.Type)); + var bplK = new Bpl.IdentifierExpr(k.tok, k.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(k.Type)); dActual = Expression.CreateSubtract(Expression.CreateIdentExpr(k), Expression.CreateNatLiteral(k.tok, 1, k.Type)); if (k.Type.IsBigOrdinalType) { - bActual = FunctionCall(k.tok, "ORD#Minus", predef.BigOrdinalType, + bActual = FunctionCall(k.tok, "ORD#Minus", Predef.BigOrdinalType, bplK, - FunctionCall(k.tok, "ORD#FromNat", predef.BigOrdinalType, Bpl.Expr.Literal(1))); + FunctionCall(k.tok, "ORD#FromNat", Predef.BigOrdinalType, Bpl.Expr.Literal(1))); } else { bActual = Bpl.Expr.Sub(bplK, Bpl.Expr.Literal(1)); } @@ -332,9 +332,9 @@ void ProcessCallStmt(CallStmt cs, Dictionary tySubst, Bpl.E var bLhs = Lhss[i]; if (ModeledAsBoxType(callee.Outs[i].Type) && !ModeledAsBoxType(LhsTypes[i])) { // we need an Unbox - Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, CurrentIdGenerator.FreshId("$tmp##"), predef.BoxType)); + Bpl.LocalVariable var = new Bpl.LocalVariable(bLhs.tok, new Bpl.TypedIdent(bLhs.tok, CurrentIdGenerator.FreshId("$tmp##"), Predef.BoxType)); locals.Add(var); - Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(bLhs.tok, var.Name, predef.BoxType); + Bpl.IdentifierExpr varIdE = new Bpl.IdentifierExpr(bLhs.tok, var.Name, Predef.BoxType); tmpOuts.Add(varIdE); outs.Add(varIdE); } else { diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs index ab7e6ae4a58..e5311a01fb8 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrForallStmt.cs @@ -136,10 +136,10 @@ void TrForallStmtCall(IToken tok, List boundVars, List bo // Now for the other branch, where the postcondition of the call is exported. { - var initHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, CurrentIdGenerator.FreshId("$initHeapForallStmt#"), predef.HeapType)); + var initHeapVar = new Bpl.LocalVariable(tok, new Bpl.TypedIdent(tok, CurrentIdGenerator.FreshId("$initHeapForallStmt#"), Predef.HeapType)); locals.Add(initHeapVar); var initHeap = new Bpl.IdentifierExpr(tok, initHeapVar); - var initEtran = new ExpressionTranslator(this, predef, initHeap, etran.Old.HeapExpr, etran.scope); + var initEtran = new ExpressionTranslator(this, Predef, initHeap, etran.Old.HeapExpr, etran.scope); // initHeap := $Heap; exporter.Add(Bpl.Cmd.SimpleAssign(tok, initHeap, etran.HeapExpr)); var heapIdExpr = etran.HeapCastToIdentifierExpr; @@ -166,7 +166,7 @@ void TrForallStmtCall(IToken tok, List boundVars, List bo Bpl.Expr ante; var argsSubstMap = new Dictionary(); // maps formal arguments to actuals Contract.Assert(s0.Method.Ins.Count == s0.Args.Count); - var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap, etran.scope); + var callEtran = new ExpressionTranslator(this, Predef, etran.HeapExpr, initHeap, etran.scope); Bpl.Expr post = Bpl.Expr.True; Bpl.Trigger tr; if (forallExpressions != null) { @@ -357,7 +357,7 @@ void TrForallAssign(ForallStmt s, SingleAssignStmt s0, // Now for the translation of the update itself Bpl.IdentifierExpr prevHeap = GetPrevHeapVar_IdExpr(s.Tok, locals); - var prevEtran = new ExpressionTranslator(this, predef, prevHeap, etran.scope); + var prevEtran = new ExpressionTranslator(this, Predef, prevHeap, etran.scope); updater.Add(Bpl.Cmd.SimpleAssign(s.Tok, prevHeap, etran.HeapExpr)); updater.Add(new Bpl.HavocCmd(s.Tok, new List { etran.HeapCastToIdentifierExpr })); updater.Add(TrAssumeCmd(s.Tok, HeapSucc(prevHeap, etran.HeapExpr))); @@ -368,9 +368,9 @@ void TrForallAssign(ForallStmt s, SingleAssignStmt s0, // $Heap[o,f] = oldHeap[o,f] || // (exists x,y :: Range(x,y)[$Heap:=oldHeap] && // o == Object(x,y)[$Heap:=oldHeap] && f == Field(x,y)[$Heap:=oldHeap])); - Bpl.BoundVariable oVar = new Bpl.BoundVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$o", predef.RefType)); + Bpl.BoundVariable oVar = new Bpl.BoundVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$o", Predef.RefType)); Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(s.Tok, oVar); - Bpl.BoundVariable fVar = new Bpl.BoundVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$f", predef.FieldName(s.Tok))); + Bpl.BoundVariable fVar = new Bpl.BoundVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$f", Predef.FieldName(s.Tok))); Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(s.Tok, fVar); Bpl.Expr heapOF = ReadHeap(s.Tok, etran.HeapExpr, o, f); Bpl.Expr oldHeapOF = ReadHeap(s.Tok, prevHeap, o, f); diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs index cebd7141fd1..caac55b8822 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrLoop.cs @@ -39,7 +39,7 @@ private void TrForLoop(ForLoopStmt stmt, BoogieStmtListBuilder builder, Variable AddComment(builder, stmt, "for-loop statement"); var indexVar = stmt.LoopIndex; - var indexVarName = indexVar.AssignUniqueName(currentDeclaration.IdGenerator); + var indexVarName = indexVar.AssignUniqueName(CurrentDeclaration.IdGenerator); var dIndex = new IdentifierExpr(indexVar.tok, indexVar); locals.GetOrCreate(indexVarName, () => new Bpl.LocalVariable(indexVar.tok, new Bpl.TypedIdent(indexVar.Tok, indexVarName, TrType(indexVar.Type)))); var bIndex = new Bpl.IdentifierExpr(indexVar.tok, indexVarName); @@ -180,9 +180,9 @@ void TrLoop(LoopStmt loop, Expression Guard, BodyTranslator/*?*/ bodyTr, var theDecreases = loop.Decreases.Expressions; var preloopheap = "$PreLoopHeap$" + suffix; - var preLoopHeapVar = locals.GetOrCreate(preloopheap, () => new Bpl.LocalVariable(loop.Tok, new Bpl.TypedIdent(loop.Tok, preloopheap, predef.HeapType))); + var preLoopHeapVar = locals.GetOrCreate(preloopheap, () => new Bpl.LocalVariable(loop.Tok, new Bpl.TypedIdent(loop.Tok, preloopheap, Predef.HeapType))); Bpl.IdentifierExpr preLoopHeap = new Bpl.IdentifierExpr(loop.Tok, preLoopHeapVar); - ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, predef, preLoopHeap, etran.scope); + ExpressionTranslator etranPreLoop = new ExpressionTranslator(this, Predef, preLoopHeap, etran.scope); ExpressionTranslator updatedFrameEtran; string loopFrameName = FrameVariablePrefix + suffix; if (loop.Mod.Expressions != null) { diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs index 39d271c2c56..e81a983b8c7 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrPredicateStatement.cs @@ -94,7 +94,7 @@ public void TrAssertStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, Vari if (assertStmt is { Label: not null }) { // make copies of the variables used in the assertion var name = "$Heap_at_" + assertStmt.Label.AssignUniqueId(CurrentIdGenerator); - var heapAt = locals.GetOrAdd(new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, name, predef.HeapType))); + var heapAt = locals.GetOrAdd(new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, name, Predef.HeapType))); var heapReference = new Bpl.IdentifierExpr(stmt.Tok, heapAt); b.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, heapReference, etran.HeapExpr)); var substMap = new Dictionary(); @@ -104,12 +104,12 @@ public void TrAssertStmt(PredicateStmt stmt, BoogieStmtListBuilder builder, Vari v.IsGhost); vcopy.type = vcopy.SyntacticType; // resolve local here IdentifierExpr ie = new IdentifierExpr(vcopy.Tok, - vcopy.AssignUniqueName(currentDeclaration.IdGenerator)); + vcopy.AssignUniqueName(CurrentDeclaration.IdGenerator)); ie.Var = vcopy; ie.Type = ie.Var.Type; // resolve ie here substMap.Add(v, ie); locals.GetOrAdd(new Bpl.LocalVariable(vcopy.Tok, - new Bpl.TypedIdent(vcopy.Tok, vcopy.AssignUniqueName(currentDeclaration.IdGenerator), + new Bpl.TypedIdent(vcopy.Tok, vcopy.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(vcopy.Type)))); b.Add(Bpl.Cmd.SimpleAssign(stmt.Tok, TrVar(stmt.Tok, vcopy), TrVar(stmt.Tok, v))); } diff --git a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs index 1c34054edad..c9617350941 100644 --- a/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Statements/BoogieGenerator.TrStatement.cs @@ -22,7 +22,7 @@ public void TrStmt(Statement stmt, BoogieStmtListBuilder builder, Contract.Requires(builder != null); Contract.Requires(locals != null); Contract.Requires(etran != null); - Contract.Requires(codeContext != null && predef != null); + Contract.Requires(codeContext != null && Predef != null); Contract.Ensures(fuelContext == Contract.OldValue(fuelContext)); stmtContext = StmtType.NONE; @@ -109,7 +109,7 @@ public void TrStmt(Statement stmt, BoogieStmtListBuilder builder, // assume $IsGoodHeap($Heap); builder.Add(AssumeGoodHeap(s.Tok, etran)); // assert YieldEnsures[subst]; // where 'subst' replaces "old(E)" with "E" being evaluated in $_OldIterHeap - var yeEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, new Bpl.IdentifierExpr(s.Tok, "$_OldIterHeap", predef.HeapType), iter); + var yeEtran = new ExpressionTranslator(this, Predef, etran.HeapExpr, new Bpl.IdentifierExpr(s.Tok, "$_OldIterHeap", Predef.HeapType), iter); var rhss = s.Rhss == null ? dafnyOutExprs @@ -297,7 +297,7 @@ public void TrStmt(Statement stmt, BoogieStmtListBuilder builder, TrStmtList(blockStmt.Body, builder, locals, etran, blockStmt.RangeToken); DefiniteAssignmentTrackers = previousTrackers; } else if (stmt is IfStmt ifStmt) { - TrIfStmt(ifStmt, builder, locals, etran); + IfStatementVerifier.EmitBoogie(this, ifStmt, builder, locals, etran); } else if (stmt is AlternativeStmt) { AddComment(builder, stmt, "alternative statement"); @@ -325,7 +325,7 @@ public void TrStmt(Statement stmt, BoogieStmtListBuilder builder, // cause the change of the heap according to the given frame var suffix = CurrentIdGenerator.FreshId("modify#"); string modifyFrameName = FrameVariablePrefix + suffix; - var preModifyHeapVar = locals.GetOrAdd(new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$PreModifyHeap$" + suffix, predef.HeapType))); + var preModifyHeapVar = locals.GetOrAdd(new Bpl.LocalVariable(s.Tok, new Bpl.TypedIdent(s.Tok, "$PreModifyHeap$" + suffix, Predef.HeapType))); DefineFrame(s.Tok, etran.ModifiesFrame(s.Tok), s.Mod.Expressions, builder, locals, modifyFrameName); if (s.Body == null) { var preModifyHeap = new Bpl.IdentifierExpr(s.Tok, preModifyHeapVar); @@ -336,7 +336,7 @@ public void TrStmt(Statement stmt, BoogieStmtListBuilder builder, // assume $HeapSucc(preModifyHeap, $Heap); OR $HeapSuccGhost builder.Add(TrAssumeCmd(s.Tok, HeapSucc(preModifyHeap, etran.HeapExpr, s.IsGhost))); // assume nothing outside the frame was changed - var etranPreLoop = new ExpressionTranslator(this, predef, preModifyHeap, this.currentDeclaration is IFrameScope fs ? fs : null); + var etranPreLoop = new ExpressionTranslator(this, Predef, preModifyHeap, this.CurrentDeclaration is IFrameScope fs ? fs : null); var updatedFrameEtran = etran.WithModifiesFrame(modifyFrameName); builder.Add(TrAssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran, updatedFrameEtran.ModifiesFrame(s.Tok)))); } else { @@ -355,14 +355,14 @@ public void TrStmt(Statement stmt, BoogieStmtListBuilder builder, } else if (stmt is NestedMatchStmt nestedMatchStmt) { TrStmt(nestedMatchStmt.Flattened, builder, locals, etran); } else if (stmt is MatchStmt matchStmt) { - TrMatchStmt(matchStmt, builder, locals, etran); + MatchStatementVerifier.TrMatchStmt(this, matchStmt, builder, locals, etran); } else if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; TrVarDeclStmt(s, builder, locals, etran); } else if (stmt is VarDeclPattern varDeclPattern) { foreach (var dafnyLocal in varDeclPattern.LocalVars) { var boogieLocal = locals.GetOrAdd(new Bpl.LocalVariable(dafnyLocal.Tok, - new Bpl.TypedIdent(dafnyLocal.Tok, dafnyLocal.AssignUniqueName(currentDeclaration.IdGenerator), + new Bpl.TypedIdent(dafnyLocal.Tok, dafnyLocal.AssignUniqueName(CurrentDeclaration.IdGenerator), TrType(dafnyLocal.Type)))); var variableReference = new Bpl.IdentifierExpr(boogieLocal.tok, boogieLocal); builder.Add(new Bpl.HavocCmd(dafnyLocal.Tok, new List @@ -449,7 +449,7 @@ void TrVarDeclStmt(VarDeclStmt varDeclStmt, BoogieStmtListBuilder builder, Varia foreach (var local in varDeclStmt.Locals) { Bpl.Type varType = TrType(local.Type); Bpl.Expr wh = GetWhereClause(local.Tok, - new Bpl.IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), varType), + new Bpl.IdentifierExpr(local.Tok, local.AssignUniqueName(CurrentDeclaration.IdGenerator), varType), local.Type, etran, isAllocContext.Var(varDeclStmt.IsGhost, local)); // if needed, register definite-assignment tracking for this local var needDefiniteAssignmentTracking = varDeclStmt.Assign == null || varDeclStmt.Assign is AssignSuchThatStmt; @@ -474,7 +474,7 @@ void TrVarDeclStmt(VarDeclStmt varDeclStmt, BoogieStmtListBuilder builder, Varia } } // create the variable itself (now that "wh" may mention the definite-assignment tracker) - var var = locals.GetOrAdd(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), varType, wh))); + var var = locals.GetOrAdd(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.AssignUniqueName(CurrentDeclaration.IdGenerator), varType, wh))); var.Attributes = etran.TrAttributes(local.Attributes, null); newLocalIds.Add(new Bpl.IdentifierExpr(local.Tok, var)); i++; @@ -487,7 +487,7 @@ void TrVarDeclStmt(VarDeclStmt varDeclStmt, BoogieStmtListBuilder builder, Varia foreach (var local in varDeclStmt.Locals) { if (Attributes.Contains(local.Attributes, "assumption")) { Bpl.Type varType = TrType(local.Type); - builder.Add(new AssumeCmd(local.Tok, new Bpl.IdentifierExpr(local.Tok, local.AssignUniqueName(currentDeclaration.IdGenerator), varType), new QKeyValue(local.Tok, "assumption_variable_initialization", new List(), null))); + builder.Add(new AssumeCmd(local.Tok, new Bpl.IdentifierExpr(local.Tok, local.AssignUniqueName(CurrentDeclaration.IdGenerator), varType), new QKeyValue(local.Tok, "assumption_variable_initialization", new List(), null))); } } if (varDeclStmt.Assign != null) { @@ -619,114 +619,6 @@ private void TrCalcStmt(CalcStmt stmt, BoogieStmtListBuilder builder, Variables this.fuelContext = FuelSetting.PopFuelContext(); } - private void TrMatchStmt(MatchStmt stmt, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran) { - Contract.Requires(stmt != null); - Contract.Requires(builder != null); - Contract.Requires(locals != null); - Contract.Requires(etran != null); - - FillMissingCases(stmt); - - TrStmt_CheckWellformed(stmt.Source, builder, locals, etran, true); - Bpl.Expr source = etran.TrExpr(stmt.Source); - var b = new BoogieStmtListBuilder(this, options, builder.Context); - b.Add(TrAssumeCmd(stmt.Tok, Bpl.Expr.False)); - Bpl.StmtList els = b.Collect(stmt.Tok); - Bpl.IfCmd ifCmd = null; - foreach (var missingCtor in stmt.MissingCases) { - // havoc all bound variables - b = new BoogieStmtListBuilder(this, options, builder.Context); - var newLocals = new Variables(); - Bpl.Expr r = CtorInvocation(stmt.Tok, missingCtor, etran, newLocals, b); - locals.AddRange(newLocals.Values); - - if (newLocals.Count != 0) { - List havocIds = new List(); - foreach (Variable local in newLocals.Values) { - havocIds.Add(new Bpl.IdentifierExpr(local.tok, local)); - } - builder.Add(new Bpl.HavocCmd(stmt.Tok, havocIds)); - } - String missingStr = stmt.Context.FillHole(new IdCtx(missingCtor)).AbstractAllHoles() - .ToString(); - var desc = new MatchIsComplete("statement", missingStr); - b.Add(Assert(stmt.Tok, Bpl.Expr.False, desc, builder.Context)); - - Bpl.Expr guard = Bpl.Expr.Eq(source, r); - ifCmd = new Bpl.IfCmd(stmt.Tok, guard, b.Collect(stmt.Tok), ifCmd, els); - els = null; - } - for (int i = stmt.Cases.Count; 0 <= --i;) { - var mc = (MatchCaseStmt)stmt.Cases[i]; - CurrentIdGenerator.Push(); - // havoc all bound variables - b = new BoogieStmtListBuilder(this, options, builder.Context); - var newLocals = new Variables(); - Bpl.Expr r = CtorInvocation(mc, stmt.Source.Type, etran, newLocals, b, stmt.IsGhost ? NOALLOC : ISALLOC); - locals.AddRange(newLocals.Values); - - if (newLocals.Count != 0) { - List havocIds = new List(); - foreach (Variable local in newLocals.Values) { - havocIds.Add(new Bpl.IdentifierExpr(local.tok, local)); - } - builder.Add(new Bpl.HavocCmd(mc.tok, havocIds)); - } - - // translate the body into b - var prevDefiniteAssignmentTrackers = DefiniteAssignmentTrackers; - TrStmtList(mc.Body, b, locals, etran); - DefiniteAssignmentTrackers = prevDefiniteAssignmentTrackers; - - Bpl.Expr guard = Bpl.Expr.Eq(source, r); - ifCmd = new Bpl.IfCmd(mc.tok, guard, b.Collect(mc.tok), ifCmd, els); - els = null; - CurrentIdGenerator.Pop(); - } - if (ifCmd != null) { - builder.Add(ifCmd); - } - } - - void FillMissingCases(IMatch match) { - Contract.Requires(match != null); - if (match.MissingCases.Any()) { - return; - } - - var dtd = match.Source.Type.AsDatatype; - var constructors = dtd?.ConstructorsByName; - - ISet memberNamesUsed = new HashSet(); - - foreach (var matchCase in match.Cases) { - if (constructors != null) { - Contract.Assert(dtd != null); - var ctorId = matchCase.Ctor.Name; - if (match.Source.Type.AsDatatype is TupleTypeDecl) { - var tuple = (TupleTypeDecl)match.Source.Type.AsDatatype; - ctorId = SystemModuleManager.TupleTypeCtorName(tuple.Dims); - } - - if (constructors.ContainsKey(ctorId)) { - memberNamesUsed.Add(ctorId); // add mc.Id to the set of names used - } - } - } - if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) { - // We could complain about the syntactic omission of constructors: - // Reporter.Error(MessageSource.Resolver, stmt, "match statement does not cover all constructors"); - // but instead we let the verifier do a semantic check. - // So, for now, record the missing constructors: - foreach (var ctr in dtd.Ctors) { - if (!memberNamesUsed.Contains(ctr.Name)) { - match.MissingCases.Add(ctr); - } - } - Contract.Assert(memberNamesUsed.Count + match.MissingCases.Count == dtd.Ctors.Count); - } - } - private static SubrangeCheckContext MakeNumericBoundsSubrangeCheckContext(BoundVar bvar, Expression lo, Expression hi) { var source = new IdentifierExpr(Token.NoToken, bvar); var loBound = lo == null ? null : new BinaryExpr(Token.NoToken, BinaryExpr.Opcode.Le, lo, source); @@ -748,53 +640,6 @@ private static SubrangeCheckContext MakeNumericBoundsSubrangeCheckContext(BoundV return CheckContext; } - private void TrIfStmt(IfStmt stmt, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran) { - Contract.Requires(stmt != null); - Contract.Requires(builder != null); - Contract.Requires(locals != null); - Contract.Requires(etran != null); - - AddComment(builder, stmt, "if statement"); - Expression guard; - if (stmt.Guard == null) { - guard = null; - } else { - guard = stmt.IsBindingGuard ? ((ExistsExpr)stmt.Guard).AlphaRename("eg$") : stmt.Guard; - TrStmt_CheckWellformed(guard, builder, locals, etran, true); - } - BoogieStmtListBuilder b = new BoogieStmtListBuilder(this, options, builder.Context); - if (stmt.IsBindingGuard) { - CurrentIdGenerator.Push(); - var exists = (ExistsExpr)stmt.Guard; // the original (that is, not alpha-renamed) guard - IntroduceAndAssignExistentialVars(exists, b, builder, locals, etran, stmt.IsGhost); - CurrentIdGenerator.Pop(); - } - CurrentIdGenerator.Push(); - Bpl.StmtList thn = TrStmt2StmtList(b, stmt.Thn, locals, etran, stmt.Thn is not BlockStmt); - CurrentIdGenerator.Pop(); - Bpl.StmtList els; - Bpl.IfCmd elsIf = null; - b = new BoogieStmtListBuilder(this, options, builder.Context); - if (stmt.IsBindingGuard) { - b.Add(TrAssumeCmdWithDependenciesAndExtend(etran, guard.tok, guard, Expr.Not, "if statement binding guard")); - } - if (stmt.Els == null) { - els = b.Collect(stmt.Tok); - } else { - CurrentIdGenerator.Push(); - els = TrStmt2StmtList(b, stmt.Els, locals, etran, stmt.Els is not BlockStmt); - CurrentIdGenerator.Pop(); - if (els.BigBlocks.Count == 1) { - Bpl.BigBlock bb = els.BigBlocks[0]; - if (bb.LabelName == null && bb.simpleCmds.Count == 0 && bb.ec is Bpl.IfCmd) { - elsIf = (Bpl.IfCmd)bb.ec; - els = null; - } - } - } - builder.Add(new Bpl.IfCmd(stmt.Tok, guard == null || stmt.IsBindingGuard ? null : etran.TrExpr(guard), thn, elsIf, els)); - } - void TrAlternatives(List alternatives, IToken elseToken, Action buildElseCase, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran, bool isGhost) { @@ -859,10 +704,10 @@ void RecordNewObjectsIn_New(IToken tok, IteratorDecl iter, Bpl.Expr initHeap, Bp Contract.Requires(locals != null); Contract.Requires(etran != null); // Add all newly allocated objects to the set this._new - var updatedSet = locals.GetOrAdd(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, CurrentIdGenerator.FreshId("$iter_newUpdate"), predef.SetType))); + var updatedSet = locals.GetOrAdd(new Bpl.LocalVariable(iter.tok, new Bpl.TypedIdent(iter.tok, CurrentIdGenerator.FreshId("$iter_newUpdate"), Predef.SetType))); var updatedSetIE = new Bpl.IdentifierExpr(iter.tok, updatedSet); // call $iter_newUpdate := $IterCollectNewObjects(initHeap, $Heap, this, _new); - var th = new Bpl.IdentifierExpr(iter.tok, etran.This, predef.RefType); + var th = new Bpl.IdentifierExpr(iter.tok, etran.This, Predef.RefType); var nwField = new Bpl.IdentifierExpr(tok, GetField(iter.Member_New)); Cmd cmd = Call(builder.Context, iter.tok, "$IterCollectNewObjects", new List() { initHeap, etran.HeapExpr, th, nwField }, @@ -913,7 +758,7 @@ private void SelectAllocateObject(IToken tok, Bpl.IdentifierExpr nw, Type type, // havoc $nw; builder.Add(new Bpl.HavocCmd(tok, new List { nw })); // assume $nw != null && $Is($nw, type); - var nwNotNull = Bpl.Expr.Neq(nw, predef.Null); + var nwNotNull = Bpl.Expr.Neq(nw, Predef.Null); // drop the $Is conjunct if the type is "object", because "new object" allocates an object of an arbitrary type var rightType = type.IsObjectQ ? Bpl.Expr.True : MkIs(nw, type); builder.Add(TrAssumeCmd(tok, BplAnd(nwNotNull, rightType))); @@ -930,7 +775,7 @@ private void CommitAllocatedObject(IToken tok, Bpl.IdentifierExpr nw, Bpl.Cmd ex Contract.Requires(etran != null); // $Heap[$nw, alloc] := true; - Bpl.Expr alloc = predef.Alloc(tok); + Bpl.Expr alloc = Predef.Alloc(tok); Bpl.IdentifierExpr heap = etran.HeapCastToIdentifierExpr; Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(tok, heap, UpdateHeap(tok, heap, nw, alloc, Bpl.Expr.True)); builder.Add(cmd); @@ -944,7 +789,7 @@ private void CommitAllocatedObject(IToken tok, Bpl.IdentifierExpr nw, Bpl.Cmd ex } - private void IntroduceAndAssignExistentialVars(ExistsExpr exists, BoogieStmtListBuilder builder, BoogieStmtListBuilder builderOutsideIfConstruct, Variables locals, ExpressionTranslator etran, bool isGhost) { + public void IntroduceAndAssignExistentialVars(ExistsExpr exists, BoogieStmtListBuilder builder, BoogieStmtListBuilder builderOutsideIfConstruct, Variables locals, ExpressionTranslator etran, bool isGhost) { Contract.Requires(exists != null); Contract.Requires(exists.Range == null); Contract.Requires(builder != null); @@ -956,9 +801,9 @@ private void IntroduceAndAssignExistentialVars(ExistsExpr exists, BoogieStmtList foreach (var bv in exists.BoundVars) { Bpl.Type varType = TrType(bv.Type); Bpl.Expr wh = GetWhereClause(bv.Tok, - new Bpl.IdentifierExpr(bv.Tok, bv.AssignUniqueName(currentDeclaration.IdGenerator), varType), + new Bpl.IdentifierExpr(bv.Tok, bv.AssignUniqueName(CurrentDeclaration.IdGenerator), varType), bv.Type, etran, isAllocContext.Var(isGhost, bv)); - Bpl.Variable local = locals.GetOrAdd(new Bpl.LocalVariable(bv.Tok, new Bpl.TypedIdent(bv.Tok, bv.AssignUniqueName(currentDeclaration.IdGenerator), varType, wh))); + Bpl.Variable local = locals.GetOrAdd(new Bpl.LocalVariable(bv.Tok, new Bpl.TypedIdent(bv.Tok, bv.AssignUniqueName(CurrentDeclaration.IdGenerator), varType, wh))); iesForHavoc.Add(new Bpl.IdentifierExpr(local.tok, local)); } builderOutsideIfConstruct.Add(new Bpl.HavocCmd(exists.tok, iesForHavoc)); @@ -1004,7 +849,7 @@ public void TrStmtList(List stmts, BoogieStmtListBuilder builder, Var if (processLabels) { for (var l = ss.Labels; l != null; l = l.Next) { var heapAt = locals.GetOrAdd(new Bpl.LocalVariable(ss.Tok, - new Bpl.TypedIdent(ss.Tok, "$Heap_at_" + l.Data.AssignUniqueId(CurrentIdGenerator), predef.HeapType))); + new Bpl.TypedIdent(ss.Tok, "$Heap_at_" + l.Data.AssignUniqueId(CurrentIdGenerator), Predef.HeapType))); builder.Add(Bpl.Cmd.SimpleAssign(ss.Tok, new Bpl.IdentifierExpr(ss.Tok, heapAt), etran.HeapExpr)); } } @@ -1020,13 +865,13 @@ public void TrStmtList(List stmts, BoogieStmtListBuilder builder, Var } } - void TrStmt_CheckWellformed(Expression expr, BoogieStmtListBuilder builder, Variables locals, + public void TrStmt_CheckWellformed(Expression expr, BoogieStmtListBuilder builder, Variables locals, ExpressionTranslator etran, bool subsumption, bool lValueContext = false, AddResultCommands addResultCommands = null) { Contract.Requires(expr != null); Contract.Requires(builder != null); Contract.Requires(locals != null); Contract.Requires(etran != null); - Contract.Requires(predef != null); + Contract.Requires(Predef != null); Bpl.QKeyValue kv; if (subsumption) { diff --git a/Source/DafnyCore/Verifier/Statements/IfStatementVerifier.cs b/Source/DafnyCore/Verifier/Statements/IfStatementVerifier.cs new file mode 100644 index 00000000000..84d1bb942ec --- /dev/null +++ b/Source/DafnyCore/Verifier/Statements/IfStatementVerifier.cs @@ -0,0 +1,54 @@ +using System.Diagnostics.Contracts; +using Microsoft.Boogie; + +namespace Microsoft.Dafny; + +public class IfStatementVerifier { + public static void EmitBoogie(BoogieGenerator generator, IfStmt stmt, BoogieStmtListBuilder builder, Variables locals, BoogieGenerator.ExpressionTranslator etran) { + Contract.Requires(stmt != null); + Contract.Requires(builder != null); + Contract.Requires(locals != null); + Contract.Requires(etran != null); + + generator.AddComment(builder, stmt, "if statement"); + Expression guard; + if (stmt.Guard == null) { + guard = null; + } else { + guard = stmt.IsBindingGuard ? ((ExistsExpr)stmt.Guard).AlphaRename("eg$") : stmt.Guard; + generator.TrStmt_CheckWellformed(guard, builder, locals, etran, true); + } + BoogieStmtListBuilder b = new BoogieStmtListBuilder(generator, generator.Options, builder.Context); + if (stmt.IsBindingGuard) { + generator.CurrentIdGenerator.Push(); + var exists = (ExistsExpr)stmt.Guard; // the original (that is, not alpha-renamed) guard + generator.IntroduceAndAssignExistentialVars(exists, b, builder, locals, etran, stmt.IsGhost); + generator.CurrentIdGenerator.Pop(); + } + + generator.CurrentIdGenerator.Push(); + Boogie.StmtList thn = generator.TrStmt2StmtList(b, stmt.Thn, locals, etran, stmt.Thn is not BlockStmt); + generator.CurrentIdGenerator.Pop(); + Boogie.StmtList els; + Boogie.IfCmd elsIf = null; + b = new BoogieStmtListBuilder(generator, generator.Options, builder.Context); + if (stmt.IsBindingGuard) { + b.Add(generator.TrAssumeCmdWithDependenciesAndExtend(etran, guard.tok, guard, Expr.Not, "if statement binding guard")); + } + if (stmt.Els == null) { + els = b.Collect(stmt.Tok); + } else { + generator.CurrentIdGenerator.Push(); + els = generator.TrStmt2StmtList(b, stmt.Els, locals, etran, stmt.Els is not BlockStmt); + generator.CurrentIdGenerator.Pop(); + if (els.BigBlocks.Count == 1) { + Boogie.BigBlock bb = els.BigBlocks[0]; + if (bb.LabelName == null && bb.simpleCmds.Count == 0 && bb.ec is Boogie.IfCmd) { + elsIf = (Boogie.IfCmd)bb.ec; + els = null; + } + } + } + builder.Add(new Boogie.IfCmd(stmt.Tok, guard == null || stmt.IsBindingGuard ? null : etran.TrExpr(guard), thn, elsIf, els)); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Verifier/Statements/MatchVerifier.cs b/Source/DafnyCore/Verifier/Statements/MatchVerifier.cs new file mode 100644 index 00000000000..00b6fed7dd4 --- /dev/null +++ b/Source/DafnyCore/Verifier/Statements/MatchVerifier.cs @@ -0,0 +1,238 @@ +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using Microsoft.Boogie; + +namespace Microsoft.Dafny; + +public static class MatchStatementVerifier { + public static void TrMatchStmt(BoogieGenerator generator, MatchStmt stmt, BoogieStmtListBuilder builder, + Variables locals, BoogieGenerator.ExpressionTranslator etran) { + Contract.Requires(stmt != null); + Contract.Requires(builder != null); + Contract.Requires(locals != null); + Contract.Requires(etran != null); + + FillMissingCases(stmt); + + generator.TrStmt_CheckWellformed(stmt.Source, builder, locals, etran, true); + Boogie.Expr source = etran.TrExpr(stmt.Source); + var b = new BoogieStmtListBuilder(generator, generator.Options, builder.Context); + b.Add(BoogieGenerator.TrAssumeCmd(stmt.Tok, Boogie.Expr.False)); + Boogie.StmtList els = b.Collect(stmt.Tok); + Boogie.IfCmd ifCmd = null; + foreach (var missingCtor in stmt.MissingCases) { + // havoc all bound variables + b = new BoogieStmtListBuilder(generator, generator.Options, builder.Context); + var newLocals = new Variables(); + Boogie.Expr r = CtorInvocation(generator, stmt.Tok, missingCtor, etran, newLocals, b); + locals.AddRange(newLocals.Values); + + if (newLocals.Count != 0) { + List havocIds = new List(); + foreach (Variable local in newLocals.Values) { + havocIds.Add(new Boogie.IdentifierExpr(local.tok, local)); + } + builder.Add(new Boogie.HavocCmd(stmt.Tok, havocIds)); + } + String missingStr = stmt.Context.FillHole(new IdCtx(missingCtor)).AbstractAllHoles() + .ToString(); + var desc = new MatchIsComplete("statement", missingStr); + b.Add(generator.Assert(stmt.Tok, Boogie.Expr.False, desc, builder.Context)); + + Boogie.Expr guard = Boogie.Expr.Eq(source, r); + ifCmd = new Boogie.IfCmd(stmt.Tok, guard, b.Collect(stmt.Tok), ifCmd, els); + els = null; + } + for (int i = stmt.Cases.Count; 0 <= --i;) { + var mc = (MatchCaseStmt)stmt.Cases[i]; + generator.CurrentIdGenerator.Push(); + // havoc all bound variables + b = new BoogieStmtListBuilder(generator, generator.Options, builder.Context); + var newLocals = new Variables(); + Boogie.Expr r = CtorInvocation(generator, mc, stmt.Source.Type, etran, newLocals, b, stmt.IsGhost ? BoogieGenerator.NOALLOC : BoogieGenerator.ISALLOC); + locals.AddRange(newLocals.Values); + + if (newLocals.Count != 0) { + List havocIds = new List(); + foreach (Variable local in newLocals.Values) { + havocIds.Add(new Boogie.IdentifierExpr(local.tok, local)); + } + builder.Add(new Boogie.HavocCmd(mc.tok, havocIds)); + } + + // translate the body into b + var prevDefiniteAssignmentTrackers = generator.DefiniteAssignmentTrackers; + generator.TrStmtList(mc.Body, b, locals, etran); + generator.DefiniteAssignmentTrackers = prevDefiniteAssignmentTrackers; + + Boogie.Expr guard = Boogie.Expr.Eq(source, r); + ifCmd = new Boogie.IfCmd(mc.tok, guard, b.Collect(mc.tok), ifCmd, els); + els = null; + generator.CurrentIdGenerator.Pop(); + } + if (ifCmd != null) { + builder.Add(ifCmd); + } + } + + private static void FillMissingCases(IMatch match) { + Contract.Requires(match != null); + if (match.MissingCases.Any()) { + return; + } + + var dtd = match.Source.Type.AsDatatype; + var constructors = dtd?.ConstructorsByName; + + ISet memberNamesUsed = new HashSet(); + + foreach (var matchCase in match.Cases) { + if (constructors != null) { + Contract.Assert(dtd != null); + var ctorId = matchCase.Ctor.Name; + if (match.Source.Type.AsDatatype is TupleTypeDecl) { + var tuple = (TupleTypeDecl)match.Source.Type.AsDatatype; + ctorId = SystemModuleManager.TupleTypeCtorName(tuple.Dims); + } + + if (constructors.ContainsKey(ctorId)) { + memberNamesUsed.Add(ctorId); // add mc.Id to the set of names used + } + } + } + if (dtd != null && memberNamesUsed.Count != dtd.Ctors.Count) { + // We could complain about the syntactic omission of constructors: + // Reporter.Error(MessageSource.Resolver, stmt, "match statement does not cover all constructors"); + // but instead we let the verifier do a semantic check. + // So, for now, record the missing constructors: + foreach (var ctr in dtd.Ctors) { + if (!memberNamesUsed.Contains(ctr.Name)) { + match.MissingCases.Add(ctr); + } + } + Contract.Assert(memberNamesUsed.Count + match.MissingCases.Count == dtd.Ctors.Count); + } + } + + public static void TrMatchExpr(BoogieGenerator generator, MatchExpr me, WFOptions wfOptions, Variables locals, + BoogieStmtListBuilder builder, BoogieGenerator.ExpressionTranslator etran, BoogieGenerator.AddResultCommands addResultCommands) { + MatchStatementVerifier.FillMissingCases(me); + + generator.CheckWellformed(me.Source, wfOptions, locals, builder, etran); + Boogie.Expr src = etran.TrExpr(me.Source); + Boogie.IfCmd ifCmd = null; + BoogieStmtListBuilder elsBldr = new BoogieStmtListBuilder(generator, generator.Options, builder.Context); + elsBldr.Add(BoogieGenerator.TrAssumeCmd(me.tok, Boogie.Expr.False)); + StmtList els = elsBldr.Collect(me.tok); + foreach (var missingCtor in me.MissingCases) { + // havoc all bound variables + var b = new BoogieStmtListBuilder(generator, generator.Options, builder.Context); + Variables newLocals = new(); + Boogie.Expr r = CtorInvocation(generator, me.tok, missingCtor, etran, newLocals, b); + locals.AddRange(newLocals.Values); + + if (newLocals.Count != 0) { + List havocIds = new List(); + foreach (Variable local in newLocals.Values) { + havocIds.Add(new Boogie.IdentifierExpr(local.tok, local)); + } + + builder.Add(new Boogie.HavocCmd(me.tok, havocIds)); + } + + String missingStr = me.Context.FillHole(new IdCtx(missingCtor)).AbstractAllHoles().ToString(); + b.Add(generator.Assert(generator.GetToken(me), Boogie.Expr.False, + new MatchIsComplete("expression", missingStr), builder.Context)); + + Boogie.Expr guard = Boogie.Expr.Eq(src, r); + ifCmd = new Boogie.IfCmd(me.tok, guard, b.Collect(me.tok), ifCmd, els); + els = null; + } + + for (int i = me.Cases.Count; 0 <= --i;) { + MatchCaseExpr mc = me.Cases[i]; + var b = new BoogieStmtListBuilder(generator, generator.Options, builder.Context); + Boogie.Expr ct = CtorInvocation(generator, mc, me.Source.Type, etran, locals, b, BoogieGenerator.NOALLOC, false); + // generate: if (src == ctor(args)) { assume args-is-well-typed; mc.Body is well-formed; assume Result == TrExpr(case); } else ... + + generator.CheckWellformedWithResult(mc.Body, wfOptions, locals, b, etran, addResultCommands); + ifCmd = new Boogie.IfCmd(mc.tok, Boogie.Expr.Eq(src, ct), b.Collect(mc.tok), ifCmd, els); + els = null; + } + + builder.Add(ifCmd); + } + + /// + /// If "declareLocals" is "false", then the locals are added only if they are new, that is, if + /// they don't already exist in "locals". + /// + private static Boogie.Expr CtorInvocation(BoogieGenerator boogieGenerator, MatchCase mc, Type sourceType, + BoogieGenerator.ExpressionTranslator etran, Variables locals, BoogieStmtListBuilder localTypeAssumptions, + IsAllocType isAlloc, bool declareLocals = true) { + Contract.Requires(mc != null); + Contract.Requires(sourceType != null); + Contract.Requires(etran != null); + Contract.Requires(locals != null); + Contract.Requires(localTypeAssumptions != null); + Contract.Requires(boogieGenerator.Predef != null); + Contract.Ensures(Contract.Result() != null); + + sourceType = sourceType.NormalizeExpand(); + Contract.Assert(sourceType.TypeArgs.Count == mc.Ctor.EnclosingDatatype.TypeArgs.Count); + var subst = new Dictionary(); + for (var i = 0; i < mc.Ctor.EnclosingDatatype.TypeArgs.Count; i++) { + subst.Add(mc.Ctor.EnclosingDatatype.TypeArgs[i], sourceType.TypeArgs[i]); + } + + List args = new List(); + for (int i = 0; i < mc.Arguments.Count; i++) { + BoundVar p = mc.Arguments[i]; + var nm = p.AssignUniqueName(boogieGenerator.CurrentDeclaration.IdGenerator); + var local = declareLocals ? null : locals.GetValueOrDefault(nm); // find previous local + if (local == null) { + local = locals.GetOrAdd(new Boogie.LocalVariable(p.tok, new Boogie.TypedIdent(p.tok, nm, boogieGenerator.TrType(p.Type)))); + } else { + Contract.Assert(Boogie.Type.Equals(local.TypedIdent.Type, boogieGenerator.TrType(p.Type))); + } + var pFormalType = mc.Ctor.Formals[i].Type.Subst(subst); + var pIsAlloc = (isAlloc == BoogieGenerator.ISALLOC) ? boogieGenerator.isAllocContext.Var(p) : BoogieGenerator.NOALLOC; + Boogie.Expr wh = boogieGenerator.GetWhereClause(p.tok, new Boogie.IdentifierExpr(p.tok, local), pFormalType, etran, pIsAlloc); + if (wh != null) { + localTypeAssumptions.Add(BoogieGenerator.TrAssumeCmd(p.tok, wh)); + } + + boogieGenerator.CheckSubrange(p.tok, new Boogie.IdentifierExpr(p.tok, local), pFormalType, p.Type, new IdentifierExpr(p.Tok, p), localTypeAssumptions); + args.Add(boogieGenerator.CondApplyBox(mc.tok, new Boogie.IdentifierExpr(p.tok, local), cce.NonNull(p.Type), mc.Ctor.Formals[i].Type)); + } + Boogie.IdentifierExpr id = new Boogie.IdentifierExpr(mc.tok, mc.Ctor.FullName, boogieGenerator.Predef.DatatypeType); + return new Boogie.NAryExpr(mc.tok, new Boogie.FunctionCall(id), args); + } + + private static Boogie.Expr CtorInvocation(BoogieGenerator generator, IToken tok, DatatypeCtor ctor, + BoogieGenerator.ExpressionTranslator etran, Variables locals, + BoogieStmtListBuilder localTypeAssumptions) { + Contract.Requires(tok != null); + Contract.Requires(ctor != null); + Contract.Requires(etran != null); + Contract.Requires(locals != null); + Contract.Requires(localTypeAssumptions != null); + Contract.Requires(generator.Predef != null); + Contract.Ensures(Contract.Result() != null); + + // create local variables for the formals + var varNameGen = generator.CurrentIdGenerator.NestedFreshIdGenerator("a#"); + var args = new List(); + foreach (Formal arg in ctor.Formals) { + Contract.Assert(arg != null); + var nm = varNameGen.FreshId(string.Format("#{0}#", args.Count)); + var bv = locals.GetOrAdd(new Boogie.LocalVariable(arg.tok, new Boogie.TypedIdent(arg.tok, nm, generator.TrType(arg.Type)))); + args.Add(new Boogie.IdentifierExpr(arg.tok, bv)); + } + + Boogie.IdentifierExpr id = new Boogie.IdentifierExpr(tok, ctor.FullName, generator.Predef.DatatypeType); + return new Boogie.NAryExpr(tok, new Boogie.FunctionCall(id), args); + } +} \ No newline at end of file