From 281922dd89d4f9709edab092a460125e7e43c434 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Wed, 24 Jul 2024 17:39:16 +0200 Subject: [PATCH] Hide statements (#5562) ### Description - Introduce hide statements, which work together with the existing reveal statements. A function that has _not_ been declared `opaque`, can still be hidden using `hide`. Hiding all functions can be done using `hide *`. Hide statements can be used as an alternative to making functions `opaque`, and unlike `opaque`, allow optimizing the performance of specific proofs in your codebase without affecting the remaining code. ### How has this been tested? - Added several CLI tests related to hiding and revealing 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). --- Source/DafnyCore/AST/Expressions/StmtExpr.cs | 2 +- .../AST/Grammar/ParserNonGeneratedPart.cs | 10 +- .../AST/Grammar/Printer/Printer.Statement.cs | 30 +- .../DafnyCore/AST/Grammar/Printer/Printer.cs | 2 +- Source/DafnyCore/AST/Members/Function.cs | 17 +- Source/DafnyCore/AST/Members/ICodeContext.cs | 3 + Source/DafnyCore/AST/Members/Method.cs | 27 +- .../DafnyCore/AST/Members/MethodOrFunction.cs | 7 +- .../AST/Statements/ControlFlow/Label.cs | 1 + .../AST/Statements/ControlFlow/LoopStmt.cs | 1 + Source/DafnyCore/AST/Statements/Statement.cs | 1 + .../Statements/Verification/HideRevealStmt.cs | 139 ++++ .../AST/Statements/Verification/RevealStmt.cs | 103 --- Source/DafnyCore/AST/Substituter.cs | 10 +- .../AST/TypeDeclarations/IteratorDecl.cs | 5 +- Source/DafnyCore/Dafny.atg | 42 +- Source/DafnyCore/DafnyCore.csproj | 2 +- .../Resolver/GhostInterestVisitor.cs | 8 +- .../CheckTypeInferenceVisitor.cs | 2 +- .../NameResolutionAndTypeInference.cs | 29 +- .../PreType/PreTypeResolve.Expressions.cs | 10 +- .../PreType/PreTypeResolve.Statements.cs | 4 +- .../PreType/UnderspecificationDetector.cs | 2 +- Source/DafnyCore/Resolver/TailRecursion.cs | 2 +- .../AutoRevealFunctionDependencies.cs | 11 +- .../Rewriters/OpaqueMemberRewriter.cs | 4 +- .../Verifier/BoogieGenerator.BoogieFactory.cs | 2 +- .../BoogieGenerator.DefiniteAssignment.cs | 4 +- .../BoogieGenerator.ExpressionWellformed.cs | 54 +- .../Verifier/BoogieGenerator.Fields.cs | 6 +- .../Verifier/BoogieGenerator.Functions.cs | 57 +- .../Verifier/BoogieGenerator.Iterators.cs | 25 +- .../Verifier/BoogieGenerator.LetExpr.cs | 390 ++++----- .../Verifier/BoogieGenerator.Methods.cs | 43 +- .../Verifier/BoogieGenerator.Reveal.cs | 48 ++ .../Verifier/BoogieGenerator.SplitExpr.cs | 57 +- .../BoogieGenerator.TrPredicateStatement.cs | 83 +- .../Verifier/BoogieGenerator.TrStatement.cs | 527 ++++++------ .../Verifier/BoogieGenerator.Types.cs | 14 +- Source/DafnyCore/Verifier/BoogieGenerator.cs | 23 +- .../Verifier/BoogieStmtListBuilder.cs | 18 +- .../Verifier/ProofObligationDescription.cs | 4 +- Source/DafnyDriver/DafnyDoc.cs | 2 +- .../Inlining/RemoveShortCircuitRewriter.cs | 2 +- .../LitTests/LitTest/ast/reveal/focus.dfy | 44 + .../LitTest/ast/reveal/focus.dfy.expect | 2 + .../LitTest/ast/reveal/revealConstants.dfy | 13 + .../ast/reveal/revealConstants.dfy.expect | 3 + .../LitTest/ast/reveal/revealFunctions.dfy | 84 ++ .../ast/reveal/revealFunctions.dfy.expect | 5 + .../LitTest/ast/reveal/revealInBlock.dfy | 102 +++ .../ast/reveal/revealInBlock.dfy.expect | 12 + .../LitTest/ast/reveal/revealInExpression.dfy | 39 + .../ast/reveal/revealInExpression.dfy.expect | 8 + .../LitTest/ast/reveal/revealMethods.dfy | 17 + .../ast/reveal/revealMethods.dfy.expect | 3 + .../LitTest/ast/reveal/revealSubsets.dfy | 36 + .../ast/reveal/revealSubsets.dfy.expect | 2 + .../Twostate-Resolution.dfy.refresh.expect | 765 ++++++++++++++++++ .../git-issue-5017b.dfy.refresh.expect | 23 + customBoogie.patch | 2 +- docs/DafnyRef/Statements.8b.expect | 4 + docs/DafnyRef/Statements.md | 80 +- docs/DafnyRef/Types.md | 32 +- docs/DafnyRef/UserGuide.md | 4 - docs/dev/news/5562.feat | 1 + 66 files changed, 2264 insertions(+), 850 deletions(-) create mode 100644 Source/DafnyCore/AST/Statements/Verification/HideRevealStmt.cs delete mode 100644 Source/DafnyCore/AST/Statements/Verification/RevealStmt.cs create mode 100644 Source/DafnyCore/Verifier/BoogieGenerator.Reveal.cs create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/focus.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/focus.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealConstants.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealConstants.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealFunctions.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInBlock.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInBlock.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInExpression.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealInExpression.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealMethods.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealMethods.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealSubsets.dfy create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/ast/reveal/revealSubsets.dfy.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Twostate-Resolution.dfy.refresh.expect create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5017b.dfy.refresh.expect create mode 100644 docs/DafnyRef/Statements.8b.expect create mode 100644 docs/dev/news/5562.feat diff --git a/Source/DafnyCore/AST/Expressions/StmtExpr.cs b/Source/DafnyCore/AST/Expressions/StmtExpr.cs index 8af66ea9d2..ea509b3c1a 100644 --- a/Source/DafnyCore/AST/Expressions/StmtExpr.cs +++ b/Source/DafnyCore/AST/Expressions/StmtExpr.cs @@ -61,7 +61,7 @@ public Expression GetSConclusion() { } else if (S is CalcStmt) { var s = (CalcStmt)S; return s.Result; - } else if (S is RevealStmt) { + } else if (S is HideRevealStmt) { return CreateBoolLiteral(tok, true); // one could use the definition axiom or the referenced labeled assertions, but "true" is conservative and much simpler :) } else if (S is UpdateStmt) { return CreateBoolLiteral(tok, true); // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :) diff --git a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs index 267040e7c7..783e171681 100644 --- a/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs +++ b/Source/DafnyCore/AST/Grammar/ParserNonGeneratedPart.cs @@ -25,6 +25,8 @@ public Parser(DafnyOptions options, Scanner/*!*/ scanner, Errors/*!*/ errors, Ca theModule = new FileModuleDefinition(scanner.FirstToken); } + bool IsReveal(IToken nextToken) => la.kind == _reveal || (la.kind == _hide && nextToken.kind is _star or _ident); + bool IsIdentifier(int kind) { return kind == _ident || kind == _least || kind == _greatest || kind == _older || kind == _opaque; } @@ -156,7 +158,12 @@ bool IsWitness() { } bool IsFunctionDecl() { - switch (la.kind) { + var kind = la.kind; + return IsFunctionDecl(kind); + } + + private bool IsFunctionDecl(int kind) { + switch (kind) { case _function: case _predicate: case _copredicate: @@ -620,7 +627,6 @@ class DeclModifierData { public bool IsOpaque; public IToken OpaqueToken; public IToken FirstToken; - } private ModuleKindEnum GetModuleKind(DeclModifierData mods) { diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs index 945563d92e..26227fae09 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.Statement.cs @@ -70,8 +70,8 @@ public void PrintStatement(Statement stmt, int indent) { PrintAttributeArgs(s.Args, true); wr.Write(";"); - } else if (stmt is RevealStmt revealStmt) { - PrintRevealStmt(revealStmt); + } else if (stmt is HideRevealStmt revealStmt) { + PrintHideReveal(revealStmt); } else if (stmt is BreakStmt) { var s = (BreakStmt)stmt; if (s.TargetLabel != null) { @@ -457,17 +457,21 @@ public void PrintStatement(Statement stmt, int indent) { } } - private void PrintRevealStmt(RevealStmt revealStmt) { - wr.Write("reveal "); - var sep = ""; - foreach (var e in revealStmt.Exprs) { - wr.Write(sep); - sep = ", "; - if (RevealStmt.SingleName(e) != null) { - // this will do the printing correctly for labels (or label-lookalikes) like 00_023 (which by PrintExpression below would be printed as 23) - wr.Write(RevealStmt.SingleName(e)); - } else { - PrintExpression(e, true); + private void PrintHideReveal(HideRevealStmt revealStmt) { + wr.Write(revealStmt.Mode == Bpl.HideRevealCmd.Modes.Hide ? "hide " : "reveal "); + if (revealStmt.Wildcard) { + wr.Write("*"); + } else { + var sep = ""; + foreach (var e in revealStmt.Exprs) { + wr.Write(sep); + sep = ", "; + if (HideRevealStmt.SingleName(e) != null) { + // this will do the printing correctly for labels (or label-lookalikes) like 00_023 (which by PrintExpression below would be printed as 23) + wr.Write(HideRevealStmt.SingleName(e)); + } else { + PrintExpression(e, true); + } } } wr.Write(";"); diff --git a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs index 14ca23325b..dbd0e854ae 100644 --- a/Source/DafnyCore/AST/Grammar/Printer/Printer.cs +++ b/Source/DafnyCore/AST/Grammar/Printer/Printer.cs @@ -979,7 +979,7 @@ private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes, if (printMode == PrintModes.NoIncludes || printMode == PrintModes.NoGhostOrIncludes) { bool verify = true; if (Attributes.ContainsBool(attributes, "verify", ref verify) && !verify) { return true; } - if (name.Contains("INTERNAL") || name.StartsWith(RevealStmt.RevealLemmaPrefix)) { return true; } + if (name.Contains("INTERNAL") || name.StartsWith(HideRevealStmt.RevealLemmaPrefix)) { return true; } } return false; } diff --git a/Source/DafnyCore/AST/Members/Function.cs b/Source/DafnyCore/AST/Members/Function.cs index 84f6940a22..3e20e20169 100644 --- a/Source/DafnyCore/AST/Members/Function.cs +++ b/Source/DafnyCore/AST/Members/Function.cs @@ -402,14 +402,15 @@ public override void Resolve(ModuleResolver resolver) { resolver.ResolveParameterDefaultValues(Ins, ResolutionContext.FromCodeContext(this)); + var contractContext = new ResolutionContext(this, this is TwoStateFunction); foreach (var req in Req) { - resolver.ResolveAttributes(req, new ResolutionContext(this, this is TwoStateFunction)); + resolver.ResolveAttributes(req, contractContext); Expression r = req.E; - resolver.ResolveExpression(r, new ResolutionContext(this, this is TwoStateFunction)); + resolver.ResolveExpression(r, contractContext); Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression resolver.ConstrainTypeExprBool(r, "Precondition must be a boolean (got {0})"); } - resolver.ResolveAttributes(Reads, new ResolutionContext(this, this is TwoStateFunction)); + resolver.ResolveAttributes(Reads, contractContext); foreach (FrameExpression fr in Reads.Expressions) { resolver.ResolveFrameExpressionTopLevel(fr, FrameExpressionUse.Reads, this); } @@ -420,16 +421,16 @@ public override void Resolve(ModuleResolver resolver) { } foreach (AttributedExpression e in Ens) { Expression r = e.E; - resolver.ResolveAttributes(e, new ResolutionContext(this, this is TwoStateFunction)); - resolver.ResolveExpression(r, new ResolutionContext(this, this is TwoStateFunction) with { InFunctionPostcondition = true }); + resolver.ResolveAttributes(e, contractContext); + resolver.ResolveExpression(r, contractContext with { InFunctionPostcondition = true }); Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression resolver.ConstrainTypeExprBool(r, "Postcondition must be a boolean (got {0})"); } resolver.scope.PopMarker(); // function result name - resolver.ResolveAttributes(Decreases, new ResolutionContext(this, this is TwoStateFunction)); + resolver.ResolveAttributes(Decreases, contractContext); foreach (Expression r in Decreases.Expressions) { - resolver.ResolveExpression(r, new ResolutionContext(this, this is TwoStateFunction)); + resolver.ResolveExpression(r, contractContext); // any type is fine } resolver.SolveAllTypeConstraints(); // solve type constraints in the specification @@ -458,7 +459,7 @@ public override void Resolve(ModuleResolver resolver) { if (Result != null) { resolver.scope.Push(Result.Name, Result); // function return only visible in post-conditions (and in function attributes) } - resolver.ResolveAttributes(this, new ResolutionContext(this, this is TwoStateFunction), true); + resolver.ResolveAttributes(this, contractContext, true); resolver.scope.PopMarker(); // function result name resolver.scope.PopMarker(); // formals diff --git a/Source/DafnyCore/AST/Members/ICodeContext.cs b/Source/DafnyCore/AST/Members/ICodeContext.cs index bcf14888f6..f7dd2fcfb7 100644 --- a/Source/DafnyCore/AST/Members/ICodeContext.cs +++ b/Source/DafnyCore/AST/Members/ICodeContext.cs @@ -46,6 +46,9 @@ public static ICodeContext Unwrap(ICodeContext codeContext) { } } +interface ICodeContainer { + bool ContainsHide { get; set; } +} /// /// An ICallable is a Function, Method, IteratorDecl, or (less fitting for the name ICallable) RedirectingTypeDecl or DatatypeDecl. diff --git a/Source/DafnyCore/AST/Members/Method.cs b/Source/DafnyCore/AST/Members/Method.cs index ff27577373..e8dd717a03 100644 --- a/Source/DafnyCore/AST/Members/Method.cs +++ b/Source/DafnyCore/AST/Members/Method.cs @@ -28,7 +28,6 @@ static Method() { Concat(Ins).Concat(Outs).Concat(TypeArgs). Concat(Req).Concat(Ens).Concat(Reads.Expressions).Concat(Mod.Expressions); public override IEnumerable PreResolveChildren => Children; - public override string WhatKind => "method"; public bool SignatureIsOmitted { get { return SignatureEllipsis != null; } } public readonly IToken SignatureEllipsis; @@ -142,7 +141,8 @@ public Method(RangeToken rangeToken, Name name, [Captured] List ens, [Captured] Specification decreases, [Captured] BlockStmt body, - Attributes attributes, IToken signatureEllipsis, bool isByMethod = false) + Attributes attributes, IToken signatureEllipsis, + bool isByMethod = false) : base(rangeToken, name, hasStaticKeyword, isGhost, attributes, signatureEllipsis != null, typeArgs, ins, req, ens, decreases) { Contract.Requires(rangeToken != null); @@ -283,29 +283,31 @@ public override void Resolve(ModuleResolver resolver) { resolver.scope.Push(p.Name, p); } - resolver.ResolveParameterDefaultValues(Ins, new ResolutionContext(this, this is TwoStateLemma)); + var resolutionContext = new ResolutionContext(this, this is TwoStateLemma); + resolver.ResolveParameterDefaultValues(Ins, resolutionContext); // Start resolving specification... foreach (AttributedExpression e in Req) { - resolver.ResolveAttributes(e, new ResolutionContext(this, this is TwoStateLemma)); - resolver.ResolveExpression(e.E, new ResolutionContext(this, this is TwoStateLemma)); + resolver.ResolveAttributes(e, resolutionContext); + resolver.ResolveExpression(e.E, resolutionContext); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression resolver.ConstrainTypeExprBool(e.E, "Precondition must be a boolean (got {0})"); } - resolver.ResolveAttributes(Reads, new ResolutionContext(this, false)); + var context = new ResolutionContext(this, false); + resolver.ResolveAttributes(Reads, context); foreach (FrameExpression fe in Reads.Expressions) { resolver.ResolveFrameExpressionTopLevel(fe, FrameExpressionUse.Reads, this); } - resolver.ResolveAttributes(Mod, new ResolutionContext(this, false)); + resolver.ResolveAttributes(Mod, context); foreach (FrameExpression fe in Mod.Expressions) { resolver.ResolveFrameExpressionTopLevel(fe, FrameExpressionUse.Modifies, this); } - resolver.ResolveAttributes(Decreases, new ResolutionContext(this, false)); + resolver.ResolveAttributes(Decreases, context); foreach (Expression e in Decreases.Expressions) { - resolver.ResolveExpression(e, new ResolutionContext(this, this is TwoStateLemma)); + resolver.ResolveExpression(e, resolutionContext); // any type is fine } @@ -331,8 +333,9 @@ public override void Resolve(ModuleResolver resolver) { // ... continue resolving specification foreach (AttributedExpression e in Ens) { - resolver.ResolveAttributes(e, new ResolutionContext(this, true)); - resolver.ResolveExpression(e.E, new ResolutionContext(this, true)); + var ensuresContext = new ResolutionContext(this, true); + resolver.ResolveAttributes(e, ensuresContext); + resolver.ResolveExpression(e.E, ensuresContext); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression resolver.ConstrainTypeExprBool(e.E, "Postcondition must be a boolean (got {0})"); } @@ -366,7 +369,7 @@ public override void Resolve(ModuleResolver resolver) { } // attributes are allowed to mention both in- and out-parameters (including the implicit _k, for greatest lemmas) - resolver.ResolveAttributes(this, new ResolutionContext(this, this is TwoStateLemma), true); + resolver.ResolveAttributes(this, resolutionContext, true); resolver.Options.WarnShadowing = warnShadowingOption; // restore the original warnShadowing value resolver.scope.PopMarker(); // for the out-parameters and outermost-level locals diff --git a/Source/DafnyCore/AST/Members/MethodOrFunction.cs b/Source/DafnyCore/AST/Members/MethodOrFunction.cs index ea5b76dd09..eef6b37214 100644 --- a/Source/DafnyCore/AST/Members/MethodOrFunction.cs +++ b/Source/DafnyCore/AST/Members/MethodOrFunction.cs @@ -6,7 +6,7 @@ namespace Microsoft.Dafny; -public abstract class MethodOrFunction : MemberDecl { +public abstract class MethodOrFunction : MemberDecl, ICodeContainer { public static readonly Option AllowExternalContracts = new("--allow-external-contracts", "Allow exporting callables with preconditions, and importing callables with postconditions"); @@ -14,6 +14,8 @@ static MethodOrFunction() { DooFile.RegisterLibraryCheck(AllowExternalContracts, OptionCompatibility.OptionLibraryImpliesLocalError); } + [FilledInDuringResolution] + public bool ContainsHide { get; set; } public readonly List TypeArgs; public readonly List Req; public readonly List Ens; @@ -39,6 +41,9 @@ protected MethodOrFunction(Cloner cloner, MethodOrFunction original) : base(clon this.Decreases = cloner.CloneSpecExpr(original.Decreases); this.Ens = original.Ens.ConvertAll(cloner.CloneAttributedExpr); this.Ins = original.Ins.ConvertAll(p => cloner.CloneFormal(p, false)); + if (cloner.CloneResolvedFields) { + this.ContainsHide = original.ContainsHide; + } } protected abstract bool Bodyless { get; } diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/Label.cs b/Source/DafnyCore/AST/Statements/ControlFlow/Label.cs index e696b3df4a..7e4e125dfc 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/Label.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/Label.cs @@ -6,6 +6,7 @@ public class Label { public readonly IToken Tok; public readonly string Name; string uniqueId = null; + public string AssignUniqueId(FreshIdGenerator idGen) { if (uniqueId == null) { uniqueId = idGen.FreshNumericId("label"); diff --git a/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs b/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs index d28972d3a6..551a031aaf 100644 --- a/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs +++ b/Source/DafnyCore/AST/Statements/ControlFlow/LoopStmt.cs @@ -6,6 +6,7 @@ namespace Microsoft.Dafny; public abstract class LoopStmt : Statement, IHasNavigationToken { public readonly List Invariants; public readonly Specification Decreases; + [FilledInDuringResolution] public bool InferredDecreases; // says that no explicit "decreases" clause was given and an attempt was made to find one automatically (which may or may not have produced anything) public readonly Specification Mod; [ContractInvariantMethod] diff --git a/Source/DafnyCore/AST/Statements/Statement.cs b/Source/DafnyCore/AST/Statements/Statement.cs index 8c8ab1ba0d..a8e2a7302a 100644 --- a/Source/DafnyCore/AST/Statements/Statement.cs +++ b/Source/DafnyCore/AST/Statements/Statement.cs @@ -9,6 +9,7 @@ public abstract class Statement : RangeNode, IAttributeBearingDeclaration { public override IToken Tok => PostLabelToken ?? StartToken; public IToken PostLabelToken { get; set; } + public int ScopeDepth { get; set; } public LList - void CheckWellformed(Expression expr, WFOptions options, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { + void CheckWellformed(Expression expr, WFOptions wfOptions, List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran) { Contract.Requires(expr != null); - Contract.Requires(options != null); + Contract.Requires(wfOptions != null); Contract.Requires(locals != null); Contract.Requires(builder != null); Contract.Requires(etran != null); Contract.Requires(predef != null); - CheckWellformedWithResult(expr, options, null, null, locals, builder, etran); + CheckWellformedWithResult(expr, wfOptions, null, null, locals, builder, etran); } /// @@ -261,17 +262,8 @@ void CheckWellformed(Expression expr, WFOptions options, List locals, /// assume the equivalent of "result == expr". /// See class WFOptions for descriptions of the specified options. /// - void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr result, Type resultType, - List locals, BoogieStmtListBuilder builder, ExpressionTranslator etran, - string resultDescription = null) { - Contract.Requires(expr != null); - Contract.Requires(wfOptions != null); - Contract.Requires((result == null) == (resultType == null)); - Contract.Requires(locals != null); - Contract.Requires(builder != null); - Contract.Requires(etran != null); - Contract.Requires(predef != null); - + void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Expr result, Type resultType, List locals, + BoogieStmtListBuilder builder, ExpressionTranslator etran, string resultDescription = null) { var origOptions = wfOptions; if (wfOptions.LValueContext) { // Turn off LValueContext for any recursive call @@ -811,7 +803,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re Expression precond = Substitute(p.E, e.Receiver, substMap, e.GetTypeArgumentSubstitutions()); var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes); - foreach (var ss in TrSplitExpr(precond, etran, true, out var splitHappened)) { + foreach (var ss in TrSplitExpr(builder.Context, precond, etran, true, out _)) { if (ss.IsChecked) { var tok = new NestedToken(GetToken(expr), ss.Tok); var desc = new PODesc.PreconditionSatisfied(directPrecond, errorMessage, successMessage); @@ -992,13 +984,13 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re switch (e.ResolvedOp) { case BinaryExpr.ResolvedOpcode.And: case BinaryExpr.ResolvedOpcode.Imp: { - BoogieStmtListBuilder b = new BoogieStmtListBuilder(this, options); + BoogieStmtListBuilder b = new BoogieStmtListBuilder(this, options, builder.Context); CheckWellformed(e.E1, wfOptions, locals, b, etran); builder.Add(new Bpl.IfCmd(binaryExpr.tok, etran.TrExpr(e.E0), b.Collect(binaryExpr.tok), null, null)); } break; case BinaryExpr.ResolvedOpcode.Or: { - BoogieStmtListBuilder b = new BoogieStmtListBuilder(this, options); + BoogieStmtListBuilder b = new BoogieStmtListBuilder(this, options, builder.Context); CheckWellformed(e.E1, wfOptions, locals, b, etran); builder.Add(new Bpl.IfCmd(binaryExpr.tok, Bpl.Expr.Not(etran.TrExpr(e.E0)), b.Collect(binaryExpr.tok), null, null)); } @@ -1268,8 +1260,8 @@ void CheckOperand(Expression operand) { case ITEExpr iteExpr: { ITEExpr e = iteExpr; CheckWellformed(e.Test, wfOptions, locals, builder, etran); - var bThen = new BoogieStmtListBuilder(this, options); - var bElse = new BoogieStmtListBuilder(this, options); + var bThen = new BoogieStmtListBuilder(this, options, builder.Context); + var bElse = new BoogieStmtListBuilder(this, options, builder.Context); if (e.IsBindingGuard) { // if it is BindingGuard, e.Thn is a let-such-that created from the BindingGuard. // We don't need to do well-formedness check on the Rhs of the LetExpr since it @@ -1356,12 +1348,12 @@ private Expr TrMatchExpr(MatchExpr me, WFOptions wfOptions, Expr result, Type re CheckWellformed(me.Source, wfOptions, locals, builder, etran); Bpl.Expr src = etran.TrExpr(me.Source); Bpl.IfCmd ifCmd = null; - BoogieStmtListBuilder elsBldr = new BoogieStmtListBuilder(this, options); + 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); + var b = new BoogieStmtListBuilder(this, options, builder.Context); List newLocals = new List(); Bpl.Expr r = CtorInvocation(me.tok, missingCtor, etran, newLocals, b); locals.AddRange(newLocals); @@ -1385,7 +1377,7 @@ private Expr TrMatchExpr(MatchExpr me, WFOptions wfOptions, Expr result, Type re for (int i = me.Cases.Count; 0 <= --i;) { MatchCaseExpr mc = me.Cases[i]; - BoogieStmtListBuilder b = new BoogieStmtListBuilder(this, options); + 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, result, resultType, locals, b, etran, "match expression branch result"); @@ -1519,7 +1511,7 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r var substMap = SetupBoundVarsAsLocals(lhsVars, out var typeAntecedent, builder, locals, etran); var rhs = Substitute(e.RHSs[0], null, substMap); if (checkRhs) { - var wellFormednessBuilder = new BoogieStmtListBuilder(this, this.options); + var wellFormednessBuilder = new BoogieStmtListBuilder(this, this.options, builder.Context); CheckWellformed(rhs, wfOptions, locals, wellFormednessBuilder, etran); var ifCmd = new Bpl.IfCmd(e.tok, typeAntecedent, wellFormednessBuilder.Collect(e.tok), null, null); builder.Add(ifCmd); @@ -1549,7 +1541,7 @@ void CheckWellformedLetExprWithResult(LetExpr e, WFOptions wfOptions, Bpl.Expr r new PODesc.LetSuchThatUnique(e.RHSs[0], e.BoundVars.ToList()))); } // assume $let$canCall(g); - LetDesugaring(e); // call LetDesugaring to prepare the desugaring and populate letSuchThatExprInfo with something for e + etran.LetDesugaring(e); // call LetDesugaring to prepare the desugaring and populate letSuchThatExprInfo with something for e var info = letSuchThatExprInfo[e]; builder.Add(new Bpl.AssumeCmd(e.tok, info.CanCallFunctionCall(this, etran))); // If we are supposed to assume "result" to equal this expression, then use the body of the let-such-that, not the generated $let#... function diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs index 2ef1fa11fc..85eaa55d10 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Fields.cs @@ -119,7 +119,9 @@ Bpl.Function GetReadonlyField(Field f) { if (cf.Rhs != null && RevealedInScope(cf)) { var etran = new ExpressionTranslator(this, predef, NewOneHeapExpr(f.tok), null); if (!IsOpaque(cf)) { - sink.AddTopLevelDeclaration(ff.CreateDefinitionAxiom(etran.TrExpr(cf.Rhs))); + var definitionAxiom = ff.CreateDefinitionAxiom(etran.TrExpr(cf.Rhs)); + definitionAxiom.CanHide = true; + sink.AddTopLevelDeclaration(definitionAxiom); } } sink.AddTopLevelDeclaration(ff); @@ -204,7 +206,7 @@ void AddWellformednessCheck(ConstantField decl) { var implInParams = Bpl.Formal.StripWhereClauses(inParams); var locals = new List(); - var builder = new BoogieStmtListBuilder(this, options); + var builder = new BoogieStmtListBuilder(this, options, new BodyTranslationContext(false)); builder.Add(new CommentCmd(string.Format("AddWellformednessCheck for {0} {1}", decl.WhatKind, decl))); builder.AddCaptureState(decl.tok, false, "initial state"); isAllocContext = new IsAllocContext(options, true); diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs index 2dd812c60b..41058d9ba7 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Functions.cs @@ -90,14 +90,15 @@ void AddWellformednessCheck(Function f) { }; // check that postconditions hold var ens = new List(); - foreach (AttributedExpression p in f.Ens) { + var context = new BodyTranslationContext(f.ContainsHide); + foreach (AttributedExpression ensures in f.Ens) { var functionHeight = currentModule.CallGraph.GetSCCRepresentativePredecessorCount(f); var splits = new List(); - bool splitHappened /*we actually don't care*/ = TrSplitExpr(p.E, splits, true, functionHeight, true, true, etran); - var (errorMessage, successMessage) = CustomErrorMessage(p.Attributes); + bool splitHappened /*we actually don't care*/ = TrSplitExpr(context, ensures.E, splits, true, functionHeight, true, true, etran); + var (errorMessage, successMessage) = CustomErrorMessage(ensures.Attributes); foreach (var s in splits) { if (s.IsChecked && !RefinementToken.IsInherited(s.Tok, currentModule)) { - AddEnsures(ens, EnsuresWithDependencies(s.Tok, false, p.E, s.E, errorMessage, successMessage, null)); + AddEnsures(ens, EnsuresWithDependencies(s.Tok, false, ensures.E, s.E, errorMessage, successMessage, null)); } } } @@ -117,8 +118,8 @@ void AddWellformednessCheck(Function f) { var implInParams = Bpl.Formal.StripWhereClauses(inParams); var implOutParams = Bpl.Formal.StripWhereClauses(outParams); var locals = new List(); - var builder = new BoogieStmtListBuilder(this, options); - var builderInitializationArea = new BoogieStmtListBuilder(this, options); + var builder = new BoogieStmtListBuilder(this, options, context); + var builderInitializationArea = new BoogieStmtListBuilder(this, options, context); builder.Add(new CommentCmd("AddWellformednessCheck for function " + f)); if (f is TwoStateFunction) { // $Heap := current$Heap; @@ -181,7 +182,8 @@ void AddWellformednessCheck(Function f) { // check well-formedness of the decreases clauses (including termination, but no reads checks) foreach (Expression p in f.Decreases.Expressions) { - CheckWellformed(p, new WFOptions(null, false), locals, builder, etran); + CheckWellformed(p, new WFOptions(null, false), + locals, builder, etran); } // Generate: // if (*) { @@ -192,7 +194,7 @@ void AddWellformednessCheck(Function f) { // // fall through to check the postconditions themselves // } // Here go the postconditions (termination checks included, but no reads checks) - BoogieStmtListBuilder postCheckBuilder = new BoogieStmtListBuilder(this, options); + BoogieStmtListBuilder postCheckBuilder = new BoogieStmtListBuilder(this, options, context); // Assume the type returned by the call itself respects its type (this matters if the type is "nat", for example) { var args = new List(); @@ -232,7 +234,7 @@ void AddWellformednessCheck(Function f) { CheckWellformedAndAssume(p.E, new WFOptions(f, false), locals, postCheckBuilder, etran, "ensures clause"); } // Here goes the body (and include both termination checks and reads checks) - BoogieStmtListBuilder bodyCheckBuilder = new BoogieStmtListBuilder(this, options); + BoogieStmtListBuilder bodyCheckBuilder = new BoogieStmtListBuilder(this, options, context); if (f.Body == null || !RevealedInScope(f)) { // don't fall through to postcondition checks bodyCheckBuilder.Add(TrAssumeCmd(f.tok, Bpl.Expr.False)); @@ -925,7 +927,9 @@ private Axiom GetFunctionAxiom(Function f, Expression body, List lits) { } else { comment += " (opaque)"; } - return new Axiom(f.tok, BplImp(activate, ax), comment); + return new Axiom(f.tok, BplImp(activate, ax), comment) { + CanHide = true + }; } @@ -948,39 +952,6 @@ Expr TrFunctionSideEffect(Statement stmt, ExpressionTranslator etran) { return e; } - Expr TrStmtSideEffect(Expr e, Statement stmt, ExpressionTranslator etran) { - if (stmt is CallStmt) { - var call = (CallStmt)stmt; - var m = call.Method; - if (IsOpaqueRevealLemma(m)) { - List args = Attributes.FindExpressions(m.Attributes, "fuel"); - if (args != null) { - MemberSelectExpr selectExpr = args[0].Resolved as MemberSelectExpr; - if (selectExpr != null) { - Function f = selectExpr.Member as Function; - FuelConstant fuelConstant = this.functionFuel.Find(x => x.f == f); - 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 layer = etran.layerInterCluster.LayerN(1, moreFuel_expr); - Bpl.Expr layerAssert = etran.layerInterCluster.LayerN(2, moreFuel_expr); - - e = BplAnd(e, Bpl.Expr.Eq(startFuel, layer)); - e = BplAnd(e, Bpl.Expr.Eq(startFuelAssert, layerAssert)); - e = BplAnd(e, Bpl.Expr.Eq(this.FunctionCall(f.tok, BuiltinFunction.AsFuelBottom, null, moreFuel_expr), moreFuel_expr)); - } - } - } - } - } else if (stmt is RevealStmt) { - var reveal = (RevealStmt)stmt; - foreach (var s in reveal.ResolvedStatements) { - e = BplAnd(e, TrFunctionSideEffect(s, etran)); - } - } - return e; - } public string FunctionHandle(Function f) { diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs index 8d31c39e58..b08bf91f8a 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.Iterators.cs @@ -94,7 +94,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { // don't include this precondition here, but record it for later use p.Label.E = etran.Old.TrExpr(p.E); } else { - foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) { + foreach (var s in TrSplitExprForMethodSpec(new BodyTranslationContext(false), p.E, etran, kind)) { if (kind == MethodTranslationKind.Call && RefinementToken.IsInherited(s.Tok, currentModule)) { // this precondition was inherited into this module, so just ignore it } else { @@ -107,7 +107,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { } comment = "user-defined postconditions"; foreach (var p in iter.Ensures) { - foreach (var s in TrSplitExprForMethodSpec(p.E, etran, kind)) { + foreach (var s in TrSplitExprForMethodSpec(new BodyTranslationContext(false), p.E, etran, kind)) { if (kind == MethodTranslationKind.Implementation && RefinementToken.IsInherited(s.Tok, currentModule)) { // this postcondition was inherited into this module, so just ignore it } else { @@ -145,7 +145,7 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { Contract.Assert(1 <= inParams.Count); // there should at least be a receiver parameter Contract.Assert(proc.OutParams.Count == 0); - var builder = new BoogieStmtListBuilder(this, options); + var builder = new BoogieStmtListBuilder(this, options, new BodyTranslationContext(false)); 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(). @@ -161,15 +161,16 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { CheckSubrange(e.tok, etran.TrExpr(e), e.Type, formal.Type, e, builder); } // check well-formedness of the preconditions, and then assume each one of them + var wfOptions = new WFOptions(); foreach (var p in iter.Requires) { - CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, builder, etran, "iterator requires clause"); + CheckWellformedAndAssume(p.E, wfOptions, localVariables, builder, etran, "iterator requires clause"); } // check well-formedness of the modifies and reads clauses - CheckFrameWellFormed(new WFOptions(), iter.Modifies.Expressions, localVariables, builder, etran); - CheckFrameWellFormed(new WFOptions(), iter.Reads.Expressions, localVariables, builder, etran); + CheckFrameWellFormed(wfOptions, iter.Modifies.Expressions, localVariables, builder, etran); + CheckFrameWellFormed(wfOptions, iter.Reads.Expressions, localVariables, builder, etran); // check well-formedness of the decreases clauses foreach (var p in iter.Decreases.Expressions) { - CheckWellformed(p, new WFOptions(), localVariables, builder, etran); + CheckWellformed(p, wfOptions, localVariables, builder, etran); } // Next, we assume about this.* whatever we said that the iterator constructor promises @@ -220,8 +221,8 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { builder.Add(TrAssumeCmd(iter.tok, yeEtran.TrExpr(cond))); // check wellformedness of postconditions - var yeBuilder = new BoogieStmtListBuilder(this, options); - var endBuilder = new BoogieStmtListBuilder(this, options); + var yeBuilder = new BoogieStmtListBuilder(this, options, builder.Context); + var endBuilder = new BoogieStmtListBuilder(this, options, builder.Context); // In the yield-ensures case: assume this.Valid(); yeBuilder.Add(TrAssumeCmdWithDependencies(yeEtran, iter.tok, validCall, "iterator validity")); Contract.Assert(iter.OutsFields.Count == iter.OutsHistoryFields.Count); @@ -244,10 +245,10 @@ void AddIteratorWellformednessCheck(IteratorDecl iter, Procedure proc) { } foreach (var p in iter.YieldEnsures) { - CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, yeBuilder, yeEtran, "iterator yield-ensures clause"); + CheckWellformedAndAssume(p.E, wfOptions, localVariables, yeBuilder, yeEtran, "iterator yield-ensures clause"); } foreach (var p in iter.Ensures) { - CheckWellformedAndAssume(p.E, new WFOptions(), localVariables, endBuilder, yeEtran, "iterator ensures clause"); + CheckWellformedAndAssume(p.E, wfOptions, localVariables, endBuilder, yeEtran, "iterator ensures clause"); } builder.Add(new Bpl.IfCmd(iter.tok, null, yeBuilder.Collect(iter.tok), null, endBuilder.Collect(iter.tok))); @@ -278,7 +279,7 @@ void AddIteratorImpl(IteratorDecl iter, Bpl.Procedure proc) { Contract.Assert(1 <= inParams.Count); // there should at least be a receiver parameter Contract.Assert(proc.OutParams.Count == 0); - var builder = new BoogieStmtListBuilder(this, options); + var builder = new BoogieStmtListBuilder(this, options, new BodyTranslationContext(iter.ContainsHide)); 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(). diff --git a/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs b/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs index 5cad787b4c..15e39c0850 100644 --- a/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs +++ b/Source/DafnyCore/Verifier/BoogieGenerator.LetExpr.cs @@ -8,51 +8,33 @@ using System; using System.Collections.Generic; using System.Linq; -using System.Numerics; using System.Diagnostics.Contracts; -using System.IO; -using System.Reflection; -using System.Security.Cryptography; using Bpl = Microsoft.Boogie; -using BplParser = Microsoft.Boogie.Parser; -using System.Text; -using System.Text.RegularExpressions; -using System.Threading; using Microsoft.Boogie; using static Microsoft.Dafny.Util; -using Core; -using DafnyCore.Verifier; -using Microsoft.BaseTypes; -using Microsoft.Dafny.Compilers; -using Microsoft.Dafny.Triggers; -using Action = System.Action; -using PODesc = Microsoft.Dafny.ProofObligationDescription; -using static Microsoft.Dafny.GenericErrors; namespace Microsoft.Dafny { public partial class BoogieGenerator { + public partial class ExpressionTranslator { - partial class ExpressionTranslator { - - - private Expr LetCanCallAssumption(LetExpr letExpr) { - if (!letExpr.Exact) { + private Expr LetCanCallAssumption(LetExpr expr) { + if (!expr.Exact) { // CanCall[[ var b0,b1 :| RHS(b0,b1,g); Body(b0,b1,g,h) ]] = // $let$canCall(g) && // CanCall[[ Body($let$b0(g), $let$b1(g), h) ]] - BoogieGenerator.LetDesugaring(letExpr); // call LetDesugaring to prepare the desugaring and populate letSuchThatExprInfo with something for e - var info = BoogieGenerator.letSuchThatExprInfo[letExpr]; + LetDesugaring(expr); // call LetDesugaring to prepare the desugaring and populate letSuchThatExprInfo with something for e + var info = BoogieGenerator.letSuchThatExprInfo[expr]; // $let$canCall(g) var canCall = info.CanCallFunctionCall(BoogieGenerator, this); Dictionary substMap = new Dictionary(); - foreach (var bv in letExpr.BoundVars) { + foreach (var bv in expr.BoundVars) { // create a call to $let$x(g) var args = info.SkolemFunctionArgs(bv, BoogieGenerator, this); var call = new BoogieFunctionCall(bv.tok, info.SkolemFunctionName(bv), info.UsesHeap, info.UsesOldHeap, info.UsesHeapAt, args.Item1, args.Item2); call.Type = bv.Type; substMap.Add(bv, call); } - var p = Substitute(letExpr.Body, null, substMap); + var p = Substitute(expr.Body, null, substMap); var cc = BplAnd(canCall, CanCallAssumption(p)); return cc; } else { @@ -60,11 +42,11 @@ private Expr LetCanCallAssumption(LetExpr letExpr) { // CanCall[[ RHS(g) ]] && // (var lhs0,lhs1,... := rhs0,rhs1,...; CanCall[[ Body ]]) Boogie.Expr canCallRHS = Boogie.Expr.True; - foreach (var rhs in letExpr.RHSs) { + foreach (var rhs in expr.RHSs) { canCallRHS = BplAnd(canCallRHS, CanCallAssumption(rhs)); } - var bodyCanCall = CanCallAssumption(letExpr.Body); + var bodyCanCall = CanCallAssumption(expr.Body); // We'd like to compute the free variables if "bodyCanCall". It would be nice to use the Boogie // routine Bpl.Expr.ComputeFreeVariables for this purpose. However, calling it requires the Boogie // expression to be resolved. Instead, we do the cheesy thing of computing the set of names of @@ -74,7 +56,7 @@ private Expr LetCanCallAssumption(LetExpr letExpr) { List lhssAll; List rhssAll; - TrLetExprPieces(letExpr, out lhssAll, out rhssAll); + TrLetExprPieces(expr, out lhssAll, out rhssAll); Contract.Assert(lhssAll.Count == rhssAll.Count); // prune lhss,rhss to contain only those pairs where the LHS is used in the body @@ -87,38 +69,39 @@ private Expr LetCanCallAssumption(LetExpr letExpr) { rhssPruned.Add(rhssAll[i]); } } - Boogie.Expr let = lhssPruned.Count == 0 ? bodyCanCall : new Boogie.LetExpr(letExpr.tok, lhssPruned, rhssPruned, null, bodyCanCall); + Boogie.Expr let = lhssPruned.Count == 0 ? bodyCanCall : new Boogie.LetExpr(expr.tok, lhssPruned, rhssPruned, null, bodyCanCall); return BplAnd(canCallRHS, let); } } private Expr TrLetExpr(LetExpr letExpr) { - var e = letExpr; - if (!e.Exact) { - var d = BoogieGenerator.LetDesugaring(e); + if (!letExpr.Exact) { + var d = LetDesugaring(letExpr); return TrExpr(d); } else { - TrLetExprPieces(e, out var lhss, out var rhss); + TrLetExprPieces(letExpr, out var lhss, out var rhss); // in the translation of body, treat a let-bound variable as IsLit if its RHS definition is IsLit - Contract.Assert(lhss.Count == rhss.Count); // this is a postcondition of TrLetExprPieces + Contract.Assert(lhss.Count == rhss.Count); // this is a postcondition of TrLetExprPieces var previousCount = BoogieGenerator.letBoundVariablesWithLitRHS.Count; for (var i = 0; i < lhss.Count; i++) { if (BoogieGenerator.IsLit(rhss[i])) { BoogieGenerator.letBoundVariablesWithLitRHS.Add(lhss[i].Name); } + i++; } - var body = TrExpr(e.Body); + + var body = TrExpr(letExpr.Body); foreach (var v in lhss) { BoogieGenerator.letBoundVariablesWithLitRHS.Remove(v.Name); } + Contract.Assert(previousCount == BoogieGenerator.letBoundVariablesWithLitRHS.Count); // in the following, use the token for Body instead of the token for the whole let expression; this gives better error locations - return new Boogie.LetExpr(GetToken(e.Body), lhss, rhss, null, body); + return new Boogie.LetExpr(GetToken(letExpr.Body), lhss, rhss, null, body); } } - public void TrLetExprPieces(LetExpr let, out List lhss, out List rhss) { Contract.Requires(let != null); var substMap = new Dictionary(); @@ -137,171 +120,186 @@ public void TrLetExprPieces(LetExpr let, out List lhss, out Lis rhss.Add(TrExpr(rhs)); } } - } - /// - /// Fills in, if necessary, the e.translationDesugaring field, and returns it. - /// Also, makes sure that letSuchThatExprInfo maps e to something. - /// - Expression LetDesugaring(LetExpr e) { - Contract.Requires(e != null); - Contract.Requires(!e.Exact); - Contract.Ensures(Contract.Result() != null); - if (e.GetTranslationDesugaring(this) == null) { - // For let-such-that expression: - // var x:X, y:Y :| P(x,y,g); F(...) - // where - // - g has type G, and - // - tt* denotes the list of type variables in the types X and Y and expression F(...), - // declare a function for each bound variable: - // function $let$x(Ty*, G): X; - // function $let$y(Ty*, G): Y; - // function $let_canCall(Ty*, G): bool; - // and add an axiom about these functions: - // axiom (forall tt*:Ty*, g:G :: - // { $let$x(tt*, g) } - // { $let$y(tt*, g) } - // $let$_canCall(tt*, g)) ==> - // P($let$x(tt*, g), $let$y(tt*, g), g)); - // and create the desugaring: - // var x:X, y:Y := $let$x(tt*, g), $let$y(tt*, g); F(...) - if (e is SubstLetExpr) { - // desugar based on the original letexpr. - var expr = (SubstLetExpr)e; - var orgExpr = expr.orgExpr; - Expression d = LetDesugaring(orgExpr); - e.SetTranslationDesugaring(this, Substitute(d, null, expr.substMap, expr.typeMap)); - var orgInfo = letSuchThatExprInfo[orgExpr]; - letSuchThatExprInfo.Add(expr, new LetSuchThatExprInfo(orgInfo, this, expr.substMap, expr.typeMap)); - } else { - // First, determine "g" as a list of Dafny variables FVs plus possibly this, $Heap, and old($Heap), - // and determine "tt*" as a list of Dafny type variables - LetSuchThatExprInfo info; - { - var FVs = new HashSet(); - bool usesHeap = false, usesOldHeap = false; - var FVsHeapAt = new HashSet