diff --git a/.github/workflows/msbuild.yml b/.github/workflows/msbuild.yml index abf0591c51a..71076267e09 100644 --- a/.github/workflows/msbuild.yml +++ b/.github/workflows/msbuild.yml @@ -53,7 +53,6 @@ jobs: build: runs-on: ${{ matrix.os }} - strategy: matrix: ## Windows jobs fail on some lit tests and sometimes fail even to @@ -126,4 +125,9 @@ jobs: unzip dafny/Package/CI.zip -d unzippedRelease - name: Run integration tests run: | - XUNIT_SHARD=${{ matrix.shard }} XUNIT_SHARD_COUNT=5 DAFNY_RELEASE=$PWD/unzippedRelease/dafny dotnet test -v:n dafny/Source/IntegrationTests/IntegrationTests.csproj + XUNIT_SHARD=${{ matrix.shard }} XUNIT_SHARD_COUNT=5 DAFNY_RELEASE=$PWD/unzippedRelease/dafny dotnet test -v:n --logger trx dafny/Source/IntegrationTests/IntegrationTests.csproj + - uses: actions/upload-artifact@v2 + if: always() + with: + name: integration-test-results-${{ matrix.os }} + path: dafny/Source/IntegrationTests/TestResults/*.trx diff --git a/.github/workflows/release-downloads.yml b/.github/workflows/release-downloads.yml index c1942e68301..301d90f34f2 100644 --- a/.github/workflows/release-downloads.yml +++ b/.github/workflows/release-downloads.yml @@ -5,6 +5,7 @@ name: Test Release Downloads on: release: types: [ published ] + workflow_dispatch: // For manual testing through the Actions UI jobs: build: @@ -16,14 +17,14 @@ jobs: os: [ ubuntu-latest, ubuntu-18.04, macos-latest, windows-latest ] include: - os: 'ubuntu-latest' - osn: 'ubuntu-18.04' + osn: 'ubuntu-16.04' - os: 'ubuntu-18.04' - osn: 'ubuntu-18.04' + osn: 'ubuntu-16.04' - os: 'macos-latest' osn: 'osx' - os: 'windows-latest' osn: 'win' - ver: '3.2.0' + ver: '3.3.0' # There is no hosted environment for Unbuntu 14.04 or for debian # Java is installed by default, but we need to select 1.8 diff --git a/.github/workflows/test-report.yml b/.github/workflows/test-report.yml new file mode 100644 index 00000000000..cca25b8c1b1 --- /dev/null +++ b/.github/workflows/test-report.yml @@ -0,0 +1,29 @@ +name: 'Test Report' +on: + workflow_run: + workflows: ['Run XUnit tests', 'Build and Test'] + types: + - completed +jobs: + report: + name: "Download and Publish Test Results" + needs: build + runs-on: ubuntu-latest + if: always() + + steps: + - uses: actions/checkout@v2 + with: + submodules: recursive + + - name: Download Artifacts + uses: actions/download-artifact@v2 + with: + path: artifacts + + - name: Publish Test Results + uses: dorny/test-reporter@v1 + with: + name: Test Results + path: 'artifacts/**/*.trx' + reporter: dotnet-trx diff --git a/.github/workflows/xunit-tests.yml b/.github/workflows/xunit-tests.yml index d7fd8dc3652..3a012d84ea6 100644 --- a/.github/workflows/xunit-tests.yml +++ b/.github/workflows/xunit-tests.yml @@ -56,8 +56,13 @@ jobs: - name: Build run: dotnet build --no-restore ${{env.solutionPath}} - name: Run DafnyLanguageServer Tests - run: dotnet test --no-restore --verbosity normal Source/DafnyLanguageServer.Test + run: dotnet test --no-restore --verbosity normal --logger trx Source/DafnyLanguageServer.Test - name: Run DafnyPipeline Tests - run: dotnet test --no-restore --verbosity normal Source/DafnyPipeline.Test + run: dotnet test --no-restore --verbosity normal --logger trx Source/DafnyPipeline.Test - name: Run DafnyTestGeneration Tests - run: dotnet test --no-restore --verbosity normal Source/DafnyTestGeneration.Test + run: dotnet test --no-restore --verbosity normal --logger trx Source/DafnyTestGeneration.Test + - uses: actions/upload-artifact@v2 + if: always() + with: + name: unit-test-results-${{ matrix.os }} + path: Source/*/TestResults/*.trx diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index c2bde2f0c1c..8144703a8df 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -4276,6 +4276,8 @@ public virtual List ParentTypes(List typeArgs) { Contract.Requires(this.TypeArgs.Count == typeArgs.Count); return new List(); } + + public bool AllowsAllocation => true; } public abstract class TopLevelDeclWithMembers : TopLevelDecl { @@ -4850,6 +4852,7 @@ public interface ICallable : ICodeContext { /// the property will get the value "true". This is so that a useful error message can be provided. /// bool InferredDecreases { get; set; } + bool AllowsAllocation { get; } } /// @@ -4873,6 +4876,8 @@ public bool InferredDecreases { get => cwInner.InferredDecreases; set { cwInner.InferredDecreases = value; } } + + public bool AllowsAllocation => cwInner.AllowsAllocation; } public class DontUseICallable : ICallable { @@ -4891,6 +4896,7 @@ public bool InferredDecreases { get { throw new cce.UnreachableException(); } set { throw new cce.UnreachableException(); } } + public bool AllowsAllocation => throw new cce.UnreachableException(); } /// /// An IMethodCodeContext is a Method or IteratorDecl. @@ -4916,6 +4922,7 @@ public NoContext(ModuleDefinition module) { bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } public bool AllowsNontermination { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } } + public bool AllowsAllocation => true; } public class IteratorDecl : ClassDecl, IMethodCodeContext { @@ -5403,6 +5410,7 @@ public bool InferredDecreases { get { throw new cce.UnreachableException(); } set { throw new cce.UnreachableException(); } } + public bool AllowsAllocation => true; } public class OpaqueTypeDecl : TopLevelDeclWithMembers, TypeParameter.ParentType, RevealableTypeDecl { @@ -6147,6 +6155,7 @@ public class Function : MemberDecl, TypeParameter.ParentType, ICallable { public Function OverriddenFunction; public Function Original => OverriddenFunction == null ? this : OverriddenFunction.Original; public override bool IsOverrideThatAddsBody => base.IsOverrideThatAddsBody && Body != null; + public bool AllowsAllocation => true; public bool containsQuantifier; public bool ContainsQuantifier { @@ -6561,6 +6570,8 @@ bool ICallable.InferredDecreases { get { return _inferredDecr; } } + public virtual bool AllowsAllocation => true; + ModuleDefinition ICodeContext.EnclosingModule { get { Contract.Assert(this.EnclosingClass != null); // this getter is supposed to be called only after signature-resolution is complete @@ -6590,7 +6601,7 @@ public BlockStmt Body { get { // Lemma from included files do not need to be resolved and translated // so we return emptyBody. This is to speed up resolvor and translator. - if (methodBody != null && (this is Lemma || this is TwoStateLemma) && this.tok is IncludeToken && !DafnyOptions.O.VerifyAllModules) { + if (methodBody != null && IsLemmaLike && this.tok is IncludeToken && !DafnyOptions.O.VerifyAllModules) { return Method.emptyBody; } else { return methodBody; @@ -6601,6 +6612,8 @@ public BlockStmt Body { } } + public bool IsLemmaLike => this is Lemma || this is TwoStateLemma || this is ExtremeLemma || this is PrefixLemma; + public BlockStmt BodyForRefinement { // For refinement, we still need to merge in the body // a lemma that is in the refinement base that is defined @@ -6624,6 +6637,8 @@ public Lemma(IToken tok, string name, Attributes attributes, IToken signatureEllipsis) : base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) { } + + public override bool AllowsAllocation => false; } public class TwoStateLemma : Method { @@ -6649,6 +6664,8 @@ public TwoStateLemma(IToken tok, string name, Contract.Requires(ens != null); Contract.Requires(decreases != null); } + + public override bool AllowsAllocation => false; } public class Constructor : Method { @@ -6676,6 +6693,7 @@ public List BodyProper { // second part of Body's statements } } public Constructor(IToken tok, string name, + bool isGhost, List typeArgs, List ins, List req, [Captured] Specification mod, @@ -6683,7 +6701,7 @@ public Constructor(IToken tok, string name, Specification decreases, DividedBlockStmt body, Attributes attributes, IToken signatureEllipsis) - : base(tok, name, false, false, typeArgs, ins, new List(), req, mod, ens, decreases, body, attributes, signatureEllipsis) { + : base(tok, name, false, isGhost, typeArgs, ins, new List(), req, mod, ens, decreases, body, attributes, signatureEllipsis) { Contract.Requires(tok != null); Contract.Requires(name != null); Contract.Requires(cce.NonNullElements(typeArgs)); @@ -6719,6 +6737,8 @@ public PrefixLemma(IToken tok, string name, bool hasStaticKeyword, K = k; ExtremeLemma = extremeLemma; } + + public override bool AllowsAllocation => false; } public abstract class ExtremeLemma : Method { @@ -6751,6 +6771,8 @@ public ExtremeLemma(IToken tok, string name, Contract.Requires(decreases != null); TypeOfK = typeOfK; } + + public override bool AllowsAllocation => false; } public class LeastLemma : ExtremeLemma { diff --git a/Source/Dafny/AST/Printer.cs b/Source/Dafny/AST/Printer.cs index 8ef0e45dbea..b2ad7005f64 100644 --- a/Source/Dafny/AST/Printer.cs +++ b/Source/Dafny/AST/Printer.cs @@ -933,7 +933,7 @@ public void PrintMethod(Method method, int indent, bool printSignatureOnly) { method is TwoStateLemma ? "twostate lemma" : "method"; if (method.HasStaticKeyword) { k = "static " + k; } - if (method.IsGhost && !(method is Lemma) && !(method is PrefixLemma) && !(method is TwoStateLemma) && !(method is ExtremeLemma)) { + if (method.IsGhost && !method.IsLemmaLike) { k = "ghost " + k; } string nm = method is Constructor && !((Constructor)method).HasName ? "" : method.Name; diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 7605501597e..8b8cc34bdae 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -798,7 +798,7 @@ public virtual Method CloneMethod(Method m) { BlockStmt body = CloneMethodBody(m); if (m is Constructor) { - return new Constructor(Tok(m.tok), m.Name, tps, ins, + return new Constructor(Tok(m.tok), m.Name, m.IsGhost, tps, ins, req, mod, ens, decreases, (DividedBlockStmt)body, CloneAttributes(m.Attributes), null); } else if (m is LeastLemma) { return new LeastLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, ((LeastLemma)m).TypeOfK, tps, ins, m.Outs.ConvertAll(CloneFormal), diff --git a/Source/Dafny/Compilers/Compiler-cpp.cs b/Source/Dafny/Compilers/Compiler-cpp.cs index da41eb9630a..d7ebda5d218 100644 --- a/Source/Dafny/Compilers/Compiler-cpp.cs +++ b/Source/Dafny/Compilers/Compiler-cpp.cs @@ -2364,7 +2364,7 @@ protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBod // ----- Target compilation and execution ------------------------------------------------------------- private string ComputeExeName(string targetFilename) { - return Path.GetFileNameWithoutExtension(targetFilename) + ".exe"; + return Path.ChangeExtension(Path.GetFullPath(targetFilename), "exe"); } public override bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string/*?*/ targetFilename, ReadOnlyCollection otherFileNames, @@ -2373,7 +2373,6 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target Contract.Assert(assemblyLocation != null); var codebase = System.IO.Path.GetDirectoryName(assemblyLocation); Contract.Assert(codebase != null); - var exeName = ComputeExeName(targetFilename); var warnings = "-Wall -Wextra -Wpedantic -Wno-unused-variable -Wno-deprecated-copy"; if (!RuntimeInformation.IsOSPlatform(OSPlatform.Linux)) { warnings += " -Wno-unknown-warning-option"; @@ -2381,7 +2380,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target if (RuntimeInformation.IsOSPlatform(OSPlatform.Linux)) { warnings += " -Wno-unused-but-set-variable"; } - var args = warnings + $" -g -std=c++17 -I {codebase} -o {exeName} {targetFilename}"; + var args = warnings + $" -g -std=c++17 -I {codebase} -o {ComputeExeName(targetFilename)} {targetFilename}"; compilationResult = null; var psi = new ProcessStartInfo("g++", args) { CreateNoWindow = true, @@ -2406,8 +2405,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter) { - var exeName = ComputeExeName(targetFilename); - var psi = new ProcessStartInfo(exeName) { + var psi = new ProcessStartInfo(ComputeExeName(targetFilename)) { CreateNoWindow = true, UseShellExecute = false, RedirectStandardOutput = true, diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 48a9c994afe..36c0b955fe9 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1713,7 +1713,7 @@ MethodDecl SemErr(t, "constructors are allowed only in classes"); } caption = "constructor"; - allowed = AllowedDeclModifiers.None; + allowed = AllowedDeclModifiers.Ghost; .) ) (. keywordToken = t; CheckDeclModifiers(dmod, caption, allowed); .) @@ -1731,7 +1731,7 @@ MethodDecl [ GenericParameters ] [ KType (. if (!(isGreatestLemma || isLeastLemma)) { SemErr(t, "type of _k can only be specified for least and greatest lemmas"); } .) ] - (. var isCompilable = (isPlainOlMethod && !dmod.IsGhost) || isConstructor; .) + (. var isCompilable = (isPlainOlMethod || isConstructor) && !dmod.IsGhost; .) Formals [ "returns" (. if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } .) Formals @@ -1748,7 +1748,7 @@ MethodDecl ] (. IToken tok = id; if (isConstructor) { - m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins, + m = new Constructor(tok, hasName ? id.val : "_ctor", dmod.IsGhost, typeArgs, ins, req, new Specification(mod, modAttrs), ens, new Specification(dec, decAttrs), (DividedBlockStmt)body, attrs, signatureEllipsis); } else if (isLeastLemma) { m = new LeastLemma(tok, id.val, dmod.IsStatic, kType, typeArgs, ins, outs, diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 3ad8f10d6ca..674e33d506a 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -102,7 +102,10 @@ public enum IncludesModes { None, Immediate, Transitive } public bool ShowSnippets = false; public bool WarningsAsErrors = false; [CanBeNull] private TestGenerationOptions testGenOptions = null; - public bool ExtractCounterExample = false; + public bool ExtractCounterexample = false; + public string VerificationLoggerConfig = null; + // Working around the fact that xmlFilename is private + public string BoogieXmlFilename = null; public virtual TestGenerationOptions TestGenOptions => testGenOptions ??= new TestGenerationOptions(); @@ -134,7 +137,7 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com } else if (args[ps.i].Equals("DllEmbed")) { PrintMode = PrintModes.DllEmbed; } else { - throw new Exception("Invalid value for printMode"); + InvalidArgumentError(name, ps); } } return true; @@ -176,7 +179,7 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com } else if (args[ps.i].Equals("php")) { CompileTarget = CompilationTarget.Php; } else { - throw new Exception("Invalid value for compileTarget"); + InvalidArgumentError(name, ps); } } return true; @@ -385,7 +388,7 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com } else if (args[ps.i].Equals("Transitive")) { PrintIncludesMode = IncludesModes.Transitive; } else { - throw new Exception("Invalid value for includesMode"); + InvalidArgumentError(name, ps); } if (PrintIncludesMode == IncludesModes.Immediate || PrintIncludesMode == IncludesModes.Transitive) { @@ -407,7 +410,7 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com } else if (args[ps.i].Equals("1")) { ShowSnippets = true; } else { - throw new Exception("Invalid value for showSnippets"); + InvalidArgumentError(name, ps); } } return true; @@ -417,8 +420,18 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com WarningsAsErrors = true; return true; - case "extractCounterExample": - ExtractCounterExample = true; + case "extractCounterexample": + ExtractCounterexample = true; + return true; + + case "verificationLogger": + if (ps.ConfirmArgumentCount(1)) { + if (args[ps.i] == "trx") { + VerificationLoggerConfig = args[ps.i]; + } else { + InvalidArgumentError(name, ps); + } + } return true; } @@ -426,9 +439,21 @@ protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.Com return TestGenOptions.ParseOption(name, ps) || base.ParseOption(name, ps); } + protected void InvalidArgumentError(string name, CommandLineParseState ps) { + ps.Error("Invalid argument \"{0}\" to option {1}", ps.args[ps.i], name); + } + public override void ApplyDefaultOptions() { base.ApplyDefaultOptions(); + if (VerificationLoggerConfig != null) { + if (XmlSink != null) { + throw new Exception("The /verificationLogger and /xml options cannot be used at the same time."); + } + BoogieXmlFilename = Path.GetTempFileName(); + XmlSink = new Bpl.XmlSink(BoogieXmlFilename); + } + // expand macros in filenames, now that LogPrefix is fully determined ExpandFilename(ref DafnyPrelude, LogPrefix, FileTimestamp); ExpandFilename(ref DafnyPrintFile, LogPrefix, FileTimestamp); @@ -872,10 +897,16 @@ or type definitions during translation. Read standard input and treat it as an input .dfy file. /warningsAsErrors Treat warnings as errors. -/extractCounterExample +/extractCounterexample If verification fails, report a detailed counterexample for the first failing assertion. Requires specifying the /mv option as well as /proverOpt:0:model_compress=false and /proverOpt:0:model.completion=true. +/verificationLogger: + Logs verification results to the given test result logger. + The only currently supported value is ""trx"", the XML-based format + commonly used for test results for .NET languages. + The exact mapping of verification concepts to the TRX format is + experimental and subject to change! {TestGenOptions.Help} Dafny generally accepts Boogie options and passes these on to Boogie. However, diff --git a/Source/Dafny/DafnyPrelude.bpl b/Source/Dafny/DafnyPrelude.bpl index da4fdbd9456..f0dd74bfce5 100644 --- a/Source/Dafny/DafnyPrelude.bpl +++ b/Source/Dafny/DafnyPrelude.bpl @@ -514,7 +514,7 @@ const unique alloc: Field bool; const unique allocName: NameFamily; axiom FDim(alloc) == 0 && DeclName(alloc) == allocName && - !$IsGhostField(alloc); // treat as non-ghost field, because it cannot be changed by ghost code + $IsGhostField(alloc); // treat as ghost field, since it is allowed to be changed by ghost code // --------------------------------------------------------------- // -- Arrays ----------------------------------------------------- diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 0ca44a20b56..c09bbfd9b5b 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -51,6 +51,95 @@ public override string filename { } } + /// + /// The "RefinementTransformer" is responsible for transforming a refining module (that is, + /// a module defined as "module Y refines X") according to the body of this module and + /// the module used as a starting point for the refinement (here, "X"). In a nutshell, + /// there are four kinds of transformations. + /// + /// 0. "Y" can fill in some definitions that "X" omitted. For example, if "X" defines + /// an opaque type "type T", then "Y" can define "T" to be a particular type, like + /// "type T = int". As another example, if "X" omits the body of a function, then + /// "Y" can give it a body. + /// + /// 1. "Y" can add definitions. For example, it can declare new types and it can add + /// members to existing types. + /// + /// 2. "Y" can superimpose statements on an existing method body. The format for this + /// is something that confuses most people. One reason for the common confusion is + /// that in many other language situations, it's the original ("X") that says what + /// parts can be replaced. Here, it the refining module ("Y") that decides where to + /// "squeeze in" new statements. For example, if a method body in "X" is + /// + /// var i := 0; + /// while i != 10 { + /// i := i + 1; + /// } + /// + /// then the refining module can write + /// + /// var j := 0; + /// ...; + /// while ... + /// invariant j == 2 * i + /// { + /// j := j + 2; + /// } + /// + /// Note, the two occurrences of "..." above are concrete syntax in Dafny. + /// + /// In the RefinementTransformer methods below, the former usually goes by some name like + /// "oldStmt", whereas the latter has some name like "skeleton". (Again, this can be confusing, + /// because a "skeleton" (or "template") is something you *add* things to, whereas here it is + /// description for *how* to add something to the "oldStmt".) + /// + /// The result of combining the "oldStmt" and the "skeleton" is called the "Merge" of + /// the two. For the example above, the merge is: + /// + /// var j := 0; + /// var i := 0; + /// while i != 10 + /// invariant j == 2 * i + /// { + /// j := j + 2; + /// i := i + 1; + /// } + /// + /// The IDE adds hover text that shows what each "...;" or "}" in the "skeleton" expands + /// to. + /// + /// Roughly speaking, the new program text that is being superimposed on the old is + /// allowed to add local variables and assignments to those (like "j" in the example above). + /// It is also allowed to add some forms of assertions (like the "invariant" in the + /// example). It cannot add statements that change the control flow, except that it + /// is allowed to add "return;" statements. Finally, in addition to these superimpositions, + /// there's a small number of refinement changes it can make. For example, it can reduce + /// nondeterminism in certain ways; e.g., it can change a statement "r :| 0 <= r <= 100;" + /// into "r := 38;". As another example of a refinement, it change change an "assume" + /// into an "assert" (by writing "assert ...;"). + /// + /// The rules about what kinds of superimpositions the language can allow has as its + /// guiding principle the idea that the verifier should not need to reverify anything that + /// was already verified in module "X". In some special cases, a superimposition needs + /// some condition to be verified (for example, an added "return;" statement causes the + /// postcondition to be reverified, but only at the point of the "return;"), so the verifier + /// adds the necessary additional checks. + /// + /// 3. Some modifiers and other decorations may be changed. For example, a "ghost var" + /// field can be changed to a "var" field, and vice versa. It may seem odd that a + /// refinement is allowed to change these (and in either direction!), but it's fine + /// as long as it doesn't affect what the verifier does. The entire merged module is + /// passed through Resolution, which catches any errors that these small changes + /// may bring about. For example, it will give an error for an assignment "a := b;" + /// if "a" and "b" were both compiled variables in "X" and "b" has been changed to be + /// a ghost variable in "Y". + /// + /// For more information about the refinement features in Dafny, see + /// + /// "Programming Language Features for Refinement" + /// Jason Koenig and K. Rustan M. Leino. + /// In EPTCS, 2016. (Post-workshop proceedings of REFINE 2015.) + /// public class RefinementTransformer : IRewriter { Cloner rawCloner; // This cloner just gives exactly the same thing back. RefinementCloner refinementCloner; // This cloner wraps things in a RefinementToken @@ -492,7 +581,7 @@ Method CloneMethod(Method m, List moreEnsures, Specificati if (m is Constructor) { var dividedBody = (DividedBlockStmt)newBody ?? refinementCloner.CloneDividedBlockStmt((DividedBlockStmt)m.BodyForRefinement); - return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, tps, ins, + return new Constructor(new RefinementToken(m.tok, moduleUnderConstruction), m.Name, m.IsGhost, tps, ins, req, mod, ens, decreases, dividedBody, refinementCloner.MergeAttributes(m.Attributes, moreAttributes), null); } var body = newBody ?? refinementCloner.CloneBlockStmt(m.BodyForRefinement); @@ -852,6 +941,9 @@ bool TypesAreSyntacticallyEqual(Type t, Type u) { return t.ToString() == u.ToString(); } + /// + /// This method merges the statement "oldStmt" into the template "skeleton". + /// BlockStmt MergeBlockStmt(BlockStmt skeleton, BlockStmt oldStmt) { Contract.Requires(skeleton != null); Contract.Requires(oldStmt != null); @@ -1069,7 +1161,10 @@ List MergeStmtList(List skeleton, List oldStmt, if (oldModifyStmt.Body == null && skel.Body == null) { mbody = null; } else if (oldModifyStmt.Body == null) { - mbody = skel.Body; + // Note, it is important to call MergeBlockStmt here (rather than just setting "mbody" to "skel.Body"), even + // though we're passing in an empty block as its second argument. The reason for this is that MergeBlockStmt + // also sets ".ReverifyPost" to "true" for any "return" statements. + mbody = MergeBlockStmt(skel.Body, new BlockStmt(oldModifyStmt.Tok, oldModifyStmt.EndTok, new List())); } else if (skel.Body == null) { reporter.Error(MessageSource.RefinementTransformer, cur.Tok, "modify template must have a body if the inherited modify statement does"); mbody = null; @@ -1351,8 +1446,18 @@ WhileStmt MergeWhileStmt(WhileStmt cNew, WhileStmt cOld, Expression guard) { var invs = cOld.Invariants.ConvertAll(refinementCloner.CloneAttributedExpr); invs.AddRange(cNew.Invariants); - var r = new RefinedWhileStmt(cNew.Tok, cNew.EndTok, guard, invs, decr, refinementCloner.CloneSpecFrameExpr(cOld.Mod), MergeBlockStmt(cNew.Body, cOld.Body)); - return r; + BlockStmt newBody; + if (cOld.Body == null && cNew.Body == null) { + newBody = null; + } else if (cOld.Body == null) { + newBody = MergeBlockStmt(cNew.Body, new BlockStmt(cOld.Tok, cOld.EndTok, new List())); + } else if (cNew.Body == null) { + reporter.Error(MessageSource.RefinementTransformer, cNew.Tok, "while template must have a body if the inherited while statement does"); + newBody = null; + } else { + newBody = MergeBlockStmt(cNew.Body, cOld.Body); + } + return new RefinedWhileStmt(cNew.Tok, cNew.EndTok, guard, invs, decr, refinementCloner.CloneSpecFrameExpr(cOld.Mod), newBody); } Statement MergeElse(Statement skeleton, Statement oldStmt) { diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 66164d7f3e5..06bdeb78a87 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -11,6 +11,7 @@ using System.Linq; using System.Numerics; using System.Diagnostics.Contracts; +using JetBrains.Annotations; using Microsoft.BaseTypes; using Microsoft.Boogie; using Microsoft.CodeAnalysis.CSharp.Syntax; @@ -1651,7 +1652,6 @@ private static string ModuleNotFoundErrorMessage(int i, List path, strin : ""); } - [Pure] private static bool EquivIfPresent(Dictionary dic, T1 key, T2 val) where T2 : class { T2 val2; @@ -1999,7 +1999,7 @@ ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef, bool useImport // saying is that the Method/Predicate does not take any type parameters over and beyond what the enclosing type (namely, the // iterator type) does. // --- here comes the constructor - var init = new Constructor(iter.tok, "_ctor", new List(), iter.Ins, + var init = new Constructor(iter.tok, "_ctor", false, new List(), iter.Ins, new List(), new Specification(new List(), null), new List(), @@ -2824,7 +2824,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, if (iter.Body != null) { CheckTypeInference(iter.Body, iter); if (prevErrCnt == reporter.Count(ErrorLevel.Error)) { - ComputeGhostInterest(iter.Body, false, iter); + ComputeGhostInterest(iter.Body, false, null, iter); CheckExpression(iter.Body, this, iter); } } @@ -3507,7 +3507,7 @@ private void ResolveClassMembers_Pass1(TopLevelDeclWithMembers cl) { var m = (Method)member; ResolveParameterDefaultValues_Pass1(m.Ins, m); if (m.Body != null) { - ComputeGhostInterest(m.Body, m.IsGhost, m); + ComputeGhostInterest(m.Body, m.IsGhost, m.IsLemmaLike ? "a " + m.WhatKind : null, m); CheckExpression(m.Body, this, m); DetermineTailRecursion(m); } @@ -3524,7 +3524,7 @@ private void ResolveClassMembers_Pass1(TopLevelDeclWithMembers cl) { } else { var m = f.ByMethodDecl; Contract.Assert(m != null && !m.IsGhost); - ComputeGhostInterest(m.Body, false, m); + ComputeGhostInterest(m.Body, false, null, m); CheckExpression(m.Body, this, m); DetermineTailRecursion(m); } @@ -6743,7 +6743,7 @@ protected override void VisitOneExpr(Expression expr) { "a type test to '{0}' must be from a compatible type (got '{1}')", e.ToType, fromType); } else if (!e.ToType.IsRefType) { resolver.reporter.Error(MessageSource.Resolver, e.tok, - "a non-trivial type test is allowed only for reference types (got '{0}')", e.ToType); + "a non-trivial type test is allowed only for reference types (tried to test if '{1}' is a '{0}')", e.ToType, fromType); } } else if (CheckTypeIsDetermined(expr.tok, expr.Type, "expression")) { if (expr is BinaryExpr) { @@ -6943,7 +6943,7 @@ public CheckExpression_Visitor(Resolver resolver, ICodeContext codeContext) protected override void VisitOneExpr(Expression expr) { if (expr is StmtExpr) { var e = (StmtExpr)expr; - resolver.ComputeGhostInterest(e.S, true, CodeContext); + resolver.ComputeGhostInterest(e.S, true, "a statement expression", CodeContext); } else if (expr is LetExpr) { var e = (LetExpr)expr; if (CodeContext.IsGhost) { @@ -6955,13 +6955,14 @@ protected override void VisitOneExpr(Expression expr) { } protected override void VisitOneStmt(Statement stmt) { - if (stmt is CalcStmt) { - var s = (CalcStmt)stmt; - foreach (var h in s.Hints) { - resolver.CheckHintRestrictions(h, new HashSet(), "a hint"); + if (stmt is CalcStmt calc) { + foreach (var h in calc.Hints) { + resolver.CheckLocalityUpdates(h, new HashSet(), "a hint"); } } else if (stmt is AssertStmt astmt && astmt.Proof != null) { - resolver.CheckHintRestrictions(astmt.Proof, new HashSet(), "an assert-by body"); + resolver.CheckLocalityUpdates(astmt.Proof, new HashSet(), "an assert-by body"); + } else if (stmt is ForallStmt forall && forall.Body != null) { + resolver.CheckLocalityUpdates(forall.Body, new HashSet(), "a forall statement"); } } } @@ -8290,20 +8291,22 @@ string TypeEqualityErrorMessageHint(Type argType) { // ----- ComputeGhostInterest --------------------------------------------------------------------------- // ------------------------------------------------------------------------------------------------------ #region ComputeGhostInterest - public void ComputeGhostInterest(Statement stmt, bool mustBeErasable, ICodeContext codeContext) { + public void ComputeGhostInterest(Statement stmt, bool mustBeErasable, [CanBeNull] string proofContext, ICodeContext codeContext) { Contract.Requires(stmt != null); Contract.Requires(codeContext != null); - var visitor = new GhostInterest_Visitor(codeContext, this); - visitor.Visit(stmt, mustBeErasable); + var visitor = new GhostInterest_Visitor(codeContext, this, false); + visitor.Visit(stmt, mustBeErasable, proofContext); } class GhostInterest_Visitor { readonly ICodeContext codeContext; readonly Resolver resolver; - public GhostInterest_Visitor(ICodeContext codeContext, Resolver resolver) { + private readonly bool inConstructorInitializationPhase; + public GhostInterest_Visitor(ICodeContext codeContext, Resolver resolver, bool inConstructorInitializationPhase) { Contract.Requires(codeContext != null); Contract.Requires(resolver != null); this.codeContext = codeContext; this.resolver = resolver; + this.inConstructorInitializationPhase = inConstructorInitializationPhase; } protected void Error(Statement stmt, string msg, params object[] msgArgs) { Contract.Requires(stmt != null); @@ -8324,11 +8327,18 @@ protected void Error(IToken tok, string msg, params object[] msgArgs) { resolver.reporter.Error(MessageSource.Resolver, tok, msg, msgArgs); } /// + /// There are three kinds of contexts for statements. + /// - compiled contexts, where the statement must be compilable + /// -- !mustBeErasable && proofContext == null + /// - ghost contexts that allow the allocation of new object + /// -- mustBeErasable && proofContext == null + /// - lemma/proof contexts, which are ghost and are not allowed to allocate new objects + /// -- mustBeErasable && proofContext != null + /// /// This method does three things, in order: /// 0. Sets .IsGhost to "true" if the statement is ghost. This often depends on some guard of the statement /// (like the guard of an "if" statement) or the LHS of the statement (if it is an assignment). /// Note, if "mustBeErasable", then the statement is already in a ghost context. - /// statement itself is ghost) or and the statement assigns to a non-ghost field /// 1. Determines if the statement and all its subparts are legal under its computed .IsGhost setting. /// 2. ``Upgrades'' .IsGhost to "true" if, after investigation of the substatements of the statement, it /// turns out that the statement can be erased during compilation. @@ -8341,16 +8351,22 @@ protected void Error(IToken tok, string msg, params object[] msgArgs) { /// * The method called by a StmtExpr must be ghost; however, this is checked elsewhere. For /// this reason, it is not necessary to visit all subexpressions, unless the subexpression /// matter for the ghost checking/recording of "stmt". + /// + /// If "proofContext" is non-null, then this method also checks that "stmt" does not allocate + /// memory or modify the heap, either directly or indirectly using a statement like "modify", a loop with + /// an explicit "modifies" clause, or a call to a method that may allocate memory or modify the heap. + /// The "proofContext" string is something that can be printed as part of an error message. /// - public void Visit(Statement stmt, bool mustBeErasable) { + public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofContext) { Contract.Requires(stmt != null); - Contract.Assume(!codeContext.IsGhost || mustBeErasable); // (this is really a precondition) codeContext.IsGhost ==> mustBeErasable + Contract.Assume(!codeContext.IsGhost || mustBeErasable); // (this is really a precondition) codeContext.IsGhost ==> mustBeErasable + Contract.Assume(mustBeErasable || proofContext == null); // (this is really a precondition) !mustBeErasable ==> proofContext == null if (stmt is AssertStmt || stmt is AssumeStmt) { stmt.IsGhost = true; var assertStmt = stmt as AssertStmt; if (assertStmt != null && assertStmt.Proof != null) { - Visit(assertStmt.Proof, true); + Visit(assertStmt.Proof, true, "an assert-by body"); } } else if (stmt is ExpectStmt) { @@ -8375,7 +8391,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is RevealStmt) { var s = (RevealStmt)stmt; - s.ResolvedStatements.Iter(ss => Visit(ss, mustBeErasable)); + s.ResolvedStatements.Iter(ss => Visit(ss, true, "a reveal statement")); s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost); } else if (stmt is BreakStmt) { var s = (BreakStmt)stmt; @@ -8392,7 +8408,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { Error(stmt, "{0} statement is not allowed in this context (because it is guarded by a specification-only expression)", kind); } if (s.hiddenUpdate != null) { - Visit(s.hiddenUpdate, mustBeErasable); + Visit(s.hiddenUpdate, mustBeErasable, proofContext); } } else if (stmt is AssignSuchThatStmt) { @@ -8416,12 +8432,12 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is UpdateStmt) { var s = (UpdateStmt)stmt; - s.ResolvedStatements.Iter(ss => Visit(ss, mustBeErasable)); + s.ResolvedStatements.Iter(ss => Visit(ss, mustBeErasable, proofContext)); s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost); } else if (stmt is AssignOrReturnStmt) { var s = (AssignOrReturnStmt)stmt; - s.ResolvedStatements.Iter(ss => Visit(ss, mustBeErasable)); + s.ResolvedStatements.Iter(ss => Visit(ss, mustBeErasable, proofContext)); s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost); } else if (stmt is VarDeclStmt) { @@ -8433,7 +8449,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { } } if (s.Update != null) { - Visit(s.Update, mustBeErasable); + Visit(s.Update, mustBeErasable, proofContext); } s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Locals.All(v => v.IsGhost); @@ -8461,77 +8477,23 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is AssignStmt) { var s = (AssignStmt)stmt; - var lhs = s.Lhs.Resolved; - - // Make an auto-ghost variable a ghost if the RHS is a ghost - if (lhs.Resolved is AutoGhostIdentifierExpr && s.Rhs is ExprRhs) { - var rhs = (ExprRhs)s.Rhs; - if (resolver.UsesSpecFeatures(rhs.Expr)) { - var autoGhostIdExpr = (AutoGhostIdentifierExpr)lhs.Resolved; - autoGhostIdExpr.Var.MakeGhost(); - } - } - - var gk = AssignStmt.LhsIsToGhost_Which(lhs); - if (gk == AssignStmt.NonGhostKind.IsGhost) { - s.IsGhost = true; - if (s.Rhs is TypeRhs) { - Error(s.Rhs.Tok, "'new' is not allowed in ghost contexts"); - } - } else if (gk == AssignStmt.NonGhostKind.Variable && codeContext.IsGhost) { - // cool - } else if (mustBeErasable) { - Error(stmt, "Assignment to {0} is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)", - AssignStmt.NonGhostKind_To_String(gk)); - } else { - if (gk == AssignStmt.NonGhostKind.Field) { - var mse = (MemberSelectExpr)lhs; - resolver.CheckIsCompilable(mse.Obj, codeContext); - } else if (gk == AssignStmt.NonGhostKind.ArrayElement) { - resolver.CheckIsCompilable(lhs, codeContext); - } - - if (s.Rhs is ExprRhs) { - var rhs = (ExprRhs)s.Rhs; - if (!AssignStmt.LhsIsToGhost(lhs)) { - resolver.CheckIsCompilable(rhs.Expr, codeContext); - } - } else if (s.Rhs is HavocRhs) { - // cool - } else { - var rhs = (TypeRhs)s.Rhs; - if (rhs.ArrayDimensions != null) { - rhs.ArrayDimensions.ForEach(ee => resolver.CheckIsCompilable(ee, codeContext)); - if (rhs.ElementInit != null) { - resolver.CheckIsCompilable(rhs.ElementInit, codeContext); - } - if (rhs.InitDisplay != null) { - rhs.InitDisplay.ForEach(ee => resolver.CheckIsCompilable(ee, codeContext)); - } - } - if (rhs.InitCall != null) { - for (var i = 0; i < rhs.InitCall.Args.Count; i++) { - if (!rhs.InitCall.Method.Ins[i].IsGhost) { - resolver.CheckIsCompilable(rhs.InitCall.Args[i], codeContext); - } - } - } - } - } + CheckAssignStmt(s, mustBeErasable, proofContext); } else if (stmt is CallStmt) { var s = (CallStmt)stmt; var callee = s.Method; Contract.Assert(callee != null); // follows from the invariant of CallStmt s.IsGhost = callee.IsGhost; - // check in-parameters - if (mustBeErasable) { + if (proofContext != null && !callee.IsLemmaLike) { + Error(s, $"in {proofContext}, calls are allowed only to lemmas"); + } else if (mustBeErasable) { if (!s.IsGhost) { Error(s, "only ghost methods can be called from this context"); } } else { int j; if (!callee.IsGhost) { + // check in-parameters resolver.CheckIsCompilable(s.Receiver, codeContext); j = 0; foreach (var e in s.Args) { @@ -8574,7 +8536,13 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is BlockStmt) { var s = (BlockStmt)stmt; s.IsGhost = mustBeErasable; // set .IsGhost before descending into substatements (since substatements may do a 'break' out of this block) - s.Body.Iter(ss => Visit(ss, mustBeErasable)); + if (s is DividedBlockStmt ds) { + var giv = new GhostInterest_Visitor(this.codeContext, this.resolver, true); + ds.BodyInit.Iter(ss => giv.Visit(ss, mustBeErasable, proofContext)); + ds.BodyProper.Iter(ss => Visit(ss, mustBeErasable, proofContext)); + } else { + s.Body.Iter(ss => Visit(ss, mustBeErasable, proofContext)); + } s.IsGhost = s.IsGhost || s.Body.All(ss => ss.IsGhost); // mark the block statement as ghost if all its substatements are ghost } else if (stmt is IfStmt) { @@ -8583,9 +8551,9 @@ public void Visit(Statement stmt, bool mustBeErasable) { if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost if"); } - Visit(s.Thn, s.IsGhost); + Visit(s.Thn, s.IsGhost, proofContext); if (s.Els != null) { - Visit(s.Els, s.IsGhost); + Visit(s.Els, s.IsGhost, proofContext); } // if both branches were all ghost, then we can mark the enclosing statement as ghost as well s.IsGhost = s.IsGhost || (s.Thn.IsGhost && (s.Els == null || s.Els.IsGhost)); @@ -8596,11 +8564,15 @@ public void Visit(Statement stmt, bool mustBeErasable) { if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost if"); } - s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost))); + s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost, proofContext))); s.IsGhost = s.IsGhost || s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost)); } else if (stmt is WhileStmt) { var s = (WhileStmt)stmt; + if (proofContext != null && s.Mod.Expressions != null && s.Mod.Expressions.Count != 0) { + Error(s.Mod.Expressions[0].tok, $"a loop in {proofContext} is not allowed to use 'modifies' clauses"); + } + s.IsGhost = mustBeErasable || (s.Guard != null && resolver.UsesSpecFeatures(s.Guard)); if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost while"); @@ -8612,7 +8584,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); } if (s.Body != null) { - Visit(s.Body, s.IsGhost); + Visit(s.Body, s.IsGhost, proofContext); if (s.Body.IsGhost && !s.Decreases.Expressions.Exists(e => e is WildcardExpr)) { s.IsGhost = true; } @@ -8620,6 +8592,10 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is AlternativeLoopStmt) { var s = (AlternativeLoopStmt)stmt; + if (proofContext != null && s.Mod.Expressions != null && s.Mod.Expressions.Count != 0) { + Error(s.Mod.Expressions[0].tok, $"a loop in {proofContext} is not allowed to use 'modifies' clauses"); + } + s.IsGhost = mustBeErasable || s.Alternatives.Exists(alt => resolver.UsesSpecFeatures(alt.Guard)); if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost while"); @@ -8630,11 +8606,15 @@ public void Visit(Statement stmt, bool mustBeErasable) { if (s.IsGhost && s.Mod.Expressions != null) { s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); } - s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost))); + s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost, proofContext))); s.IsGhost = s.IsGhost || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost))); } else if (stmt is ForLoopStmt) { var s = (ForLoopStmt)stmt; + if (proofContext != null && s.Mod.Expressions != null && s.Mod.Expressions.Count != 0) { + Error(s.Mod.Expressions[0].tok, $"a loop in {proofContext} is not allowed to use 'modifies' clauses"); + } + s.IsGhost = mustBeErasable || resolver.UsesSpecFeatures(s.Start) || (s.End != null && resolver.UsesSpecFeatures(s.End)); if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost for-loop"); @@ -8650,7 +8630,7 @@ public void Visit(Statement stmt, bool mustBeErasable) { s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); } if (s.Body != null) { - Visit(s.Body, s.IsGhost); + Visit(s.Body, s.IsGhost, proofContext); if (s.Body.IsGhost) { s.IsGhost = true; } @@ -8659,8 +8639,10 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; s.IsGhost = mustBeErasable || s.Kind != ForallStmt.BodyKind.Assign || resolver.UsesSpecFeatures(s.Range); - if (s.Body != null) { - Visit(s.Body, s.IsGhost); + if (proofContext != null && s.Kind == ForallStmt.BodyKind.Assign) { + Error(s, $"{proofContext} is not allowed to perform an aggregate heap update"); + } else if (s.Body != null) { + Visit(s.Body, s.IsGhost, s.Kind == ForallStmt.BodyKind.Assign ? proofContext : "a forall statement"); } s.IsGhost = s.IsGhost || s.Body == null || s.Body.IsGhost; @@ -8676,19 +8658,23 @@ public void Visit(Statement stmt, bool mustBeErasable) { } else if (stmt is ModifyStmt) { var s = (ModifyStmt)stmt; + if (proofContext != null) { + Error(stmt, $"a modify statement is not allowed in {proofContext}"); + } + s.IsGhost = mustBeErasable; if (s.IsGhost) { s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); } if (s.Body != null) { - Visit(s.Body, mustBeErasable); + Visit(s.Body, mustBeErasable, proofContext); } } else if (stmt is CalcStmt) { var s = (CalcStmt)stmt; s.IsGhost = true; foreach (var h in s.Hints) { - Visit(h, true); + Visit(h, true, "a hint"); } } else if (stmt is MatchStmt) { @@ -8697,17 +8683,17 @@ public void Visit(Statement stmt, bool mustBeErasable) { if (!mustBeErasable && s.IsGhost) { resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ghost match"); } - s.Cases.Iter(kase => kase.Body.Iter(ss => Visit(ss, s.IsGhost))); + s.Cases.Iter(kase => kase.Body.Iter(ss => Visit(ss, s.IsGhost, proofContext))); s.IsGhost = s.IsGhost || s.Cases.All(kase => kase.Body.All(ss => ss.IsGhost)); } else if (stmt is ConcreteSyntaxStatement) { var s = (ConcreteSyntaxStatement)stmt; - Visit(s.ResolvedStatement, mustBeErasable); + Visit(s.ResolvedStatement, mustBeErasable, proofContext); s.IsGhost = s.IsGhost || s.ResolvedStatement.IsGhost; } else if (stmt is SkeletonStatement) { var s = (SkeletonStatement)stmt; s.IsGhost = mustBeErasable; if (s.S != null) { - Visit(s.S, mustBeErasable); + Visit(s.S, mustBeErasable, proofContext); s.IsGhost = s.IsGhost || s.S.IsGhost; } @@ -8715,6 +8701,98 @@ public void Visit(Statement stmt, bool mustBeErasable) { Contract.Assert(false); throw new cce.UnreachableException(); } } + + private void CheckAssignStmt(AssignStmt s, bool mustBeErasable, [CanBeNull] string proofContext) { + Contract.Requires(s != null); + Contract.Requires(mustBeErasable || proofContext == null); + + var lhs = s.Lhs.Resolved; + + // Make an auto-ghost variable a ghost if the RHS is a ghost + if (lhs.Resolved is AutoGhostIdentifierExpr autoGhostIdExpr) { + if (s.Rhs is ExprRhs eRhs && resolver.UsesSpecFeatures(eRhs.Expr)) { + autoGhostIdExpr.Var.MakeGhost(); + } else if (s.Rhs is TypeRhs tRhs) { + if (tRhs.InitCall != null && tRhs.InitCall.Method.IsGhost) { + autoGhostIdExpr.Var.MakeGhost(); + } else if (tRhs.ArrayDimensions != null && tRhs.ArrayDimensions.Exists(resolver.UsesSpecFeatures)) { + autoGhostIdExpr.Var.MakeGhost(); + } else if (tRhs.ElementInit != null && resolver.UsesSpecFeatures(tRhs.ElementInit)) { + autoGhostIdExpr.Var.MakeGhost(); + } else if (tRhs.InitDisplay != null && tRhs.InitDisplay.Any(resolver.UsesSpecFeatures)) { + autoGhostIdExpr.Var.MakeGhost(); + } + } + } + + if (proofContext != null && s.Rhs is TypeRhs) { + Error(s.Rhs.Tok, $"{proofContext} is not allowed to use 'new'"); + } + + var gk = AssignStmt.LhsIsToGhost_Which(lhs); + if (gk == AssignStmt.NonGhostKind.IsGhost) { + s.IsGhost = true; + if (proofContext != null && !(lhs is IdentifierExpr)) { + Error(lhs.tok, $"{proofContext} is not allowed to make heap updates"); + } + if (s.Rhs is TypeRhs tRhs && tRhs.InitCall != null) { + Visit(tRhs.InitCall, true, proofContext); + } + } else if (gk == AssignStmt.NonGhostKind.Variable && codeContext.IsGhost) { + // cool + } else if (mustBeErasable) { + if (inConstructorInitializationPhase && codeContext is Constructor && codeContext.IsGhost && lhs is MemberSelectExpr mse && + mse.Obj.Resolved is ThisExpr) { + // in this first division (before "new;") of a ghost constructor, allow assignment to non-ghost field of the object being constructed + } else { + string reason; + if (codeContext.IsGhost) { + reason = string.Format("this is a ghost {0}", codeContext is MemberDecl member ? member.WhatKind : "context"); + } else { + reason = "the statement is in a ghost context; e.g., it may be guarded by a specification-only expression"; + } + Error(s, $"assignment to {AssignStmt.NonGhostKind_To_String(gk)} is not allowed in this context, because {reason}"); + } + } else { + if (gk == AssignStmt.NonGhostKind.Field) { + var mse = (MemberSelectExpr)lhs; + resolver.CheckIsCompilable(mse.Obj, codeContext); + } else if (gk == AssignStmt.NonGhostKind.ArrayElement) { + resolver.CheckIsCompilable(lhs, codeContext); + } + + if (s.Rhs is ExprRhs) { + var rhs = (ExprRhs)s.Rhs; + if (!AssignStmt.LhsIsToGhost(lhs)) { + resolver.CheckIsCompilable(rhs.Expr, codeContext); + } + } else if (s.Rhs is HavocRhs) { + // cool + } else { + var rhs = (TypeRhs)s.Rhs; + if (rhs.ArrayDimensions != null) { + rhs.ArrayDimensions.ForEach(ee => resolver.CheckIsCompilable(ee, codeContext)); + if (rhs.ElementInit != null) { + resolver.CheckIsCompilable(rhs.ElementInit, codeContext); + } + if (rhs.InitDisplay != null) { + rhs.InitDisplay.ForEach(ee => resolver.CheckIsCompilable(ee, codeContext)); + } + } + if (rhs.InitCall != null) { + var callee = rhs.InitCall.Method; + if (callee.IsGhost) { + Error(rhs.InitCall, "the result of a ghost constructor can only be assigned to a ghost variable"); + } + for (var i = 0; i < rhs.InitCall.Args.Count; i++) { + if (!callee.Ins[i].IsGhost) { + resolver.CheckIsCompilable(rhs.InitCall.Args[i], codeContext); + } + } + } + } + } + } } #endregion @@ -10128,7 +10206,7 @@ void ResolveMethod(Method m) { ResolveAttributes(m.Mod.Attributes, null, new ResolveOpts(m, false)); foreach (FrameExpression fe in m.Mod.Expressions) { ResolveFrameExpression(fe, FrameExpressionUse.Modifies, m); - if (m is Lemma || m is TwoStateLemma || m is ExtremeLemma) { + if (m.IsLemmaLike) { reporter.Error(MessageSource.Resolver, fe.tok, "{0}s are not allowed to have modifies clauses", m.WhatKind); } else if (m.IsGhost) { DisallowNonGhostFieldSpecifiers(fe); @@ -11289,6 +11367,12 @@ public void ResolveStatement(Statement stmt, ICodeContext codeContext) { Statement s0 = s.S0; if (s0 is AssignStmt) { s.Kind = ForallStmt.BodyKind.Assign; + + var rhs = ((AssignStmt)s0).Rhs; + if (rhs is TypeRhs) { + reporter.Error(MessageSource.Resolver, rhs.Tok, "new allocation not supported in aggregate assignments"); + } + } else if (s0 is CallStmt) { s.Kind = ForallStmt.BodyKind.Call; var call = (CallStmt)s.S0; @@ -11316,9 +11400,6 @@ public void ResolveStatement(Statement stmt, ICodeContext codeContext) { } } } - if (s.Body != null) { - CheckForallStatementBodyRestrictions(s.Body, s.Kind); - } if (s.ForallExpressions != null) { foreach (Expression expr in s.ForallExpressions) { @@ -13374,290 +13455,55 @@ void ResolveStatementWithLabels(Statement stmt, ICodeContext codeContext) { } /// - /// This method performs some additional checks on the body "stmt" of a forall statement of kind "kind". + /// Check that "stmt" is a valid statment for the body of an assert-by, forall, + /// or calc-hint statement. In particular, check that the local variables assigned in + /// the bodies of these statements are declared in the statements, not in some enclosing + /// context. /// - public void CheckForallStatementBodyRestrictions(Statement stmt, ForallStmt.BodyKind kind) { - Contract.Requires(stmt != null); - if (stmt is PredicateStmt) { - // cool - } else if (stmt is RevealStmt) { - var s = (RevealStmt)stmt; - foreach (var ss in s.ResolvedStatements) { - CheckForallStatementBodyRestrictions(ss, kind); - } - } else if (stmt is PrintStmt) { - reporter.Error(MessageSource.Resolver, stmt, "print statement is not allowed inside a forall statement"); - } else if (stmt is BreakStmt) { - // this case is checked already in the first pass through the forall-statement body, by doing so from an empty set of labeled statements and resetting the loop-stack - } else if (stmt is ReturnStmt) { - reporter.Error(MessageSource.Resolver, stmt, "return statement is not allowed inside a forall statement"); - } else if (stmt is YieldStmt) { - reporter.Error(MessageSource.Resolver, stmt, "yield statement is not allowed inside a forall statement"); - } else if (stmt is AssignSuchThatStmt) { - var s = (AssignSuchThatStmt)stmt; - foreach (var lhs in s.Lhss) { - CheckForallStatementBodyLhs(lhs.tok, lhs.Resolved, kind); - } - } else if (stmt is UpdateStmt) { - var s = (UpdateStmt)stmt; - foreach (var ss in s.ResolvedStatements) { - CheckForallStatementBodyRestrictions(ss, kind); - } - } else if (stmt is VarDeclStmt) { - var s = (VarDeclStmt)stmt; - if (s.Update != null) { - CheckForallStatementBodyRestrictions(s.Update, kind); - } - } else if (stmt is VarDeclPattern) { - // Are we fine? - } else if (stmt is AssignStmt) { - var s = (AssignStmt)stmt; - CheckForallStatementBodyLhs(s.Lhs.tok, s.Lhs.Resolved, kind); - var rhs = s.Rhs; // ExprRhs and HavocRhs are fine, but TypeRhs is not - if (rhs is TypeRhs) { - if (kind == ForallStmt.BodyKind.Assign) { - reporter.Error(MessageSource.Resolver, rhs.Tok, "new allocation not supported in forall statements"); - } else { - reporter.Error(MessageSource.Resolver, rhs.Tok, "new allocation not allowed in ghost context"); - } - } - } else if (stmt is CallStmt) { - var s = (CallStmt)stmt; - foreach (var lhs in s.Lhs) { - CheckForallStatementBodyLhs(lhs.tok, lhs, kind); - } - if (s.Method.Mod.Expressions.Count != 0) { - reporter.Error(MessageSource.Resolver, stmt, "the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause"); - } - if (!s.Method.IsGhost) { - // The reason for this restriction is that the compiler is going to omit the forall statement altogether--it has - // no effect. However, print effects are not documented, so to make sure that the compiler does not omit a call to - // a method that prints something, all calls to non-ghost methods are disallowed. (Note, if this restriction - // is somehow lifted in the future, then it is still necessary to enforce s.Method.Mod.Expressions.Count != 0 for - // calls to non-ghost methods.) - reporter.Error(MessageSource.Resolver, s, "the body of the enclosing forall statement is not allowed to call non-ghost methods"); - } - - } else if (stmt is ModifyStmt) { - reporter.Error(MessageSource.Resolver, stmt, "body of forall statement is not allowed to use a modify statement"); - } else if (stmt is BlockStmt) { - var s = (BlockStmt)stmt; - scope.PushMarker(); - foreach (var ss in s.Body) { - CheckForallStatementBodyRestrictions(ss, kind); - } - scope.PopMarker(); - - } else if (stmt is IfStmt) { - var s = (IfStmt)stmt; - CheckForallStatementBodyRestrictions(s.Thn, kind); - if (s.Els != null) { - CheckForallStatementBodyRestrictions(s.Els, kind); - } - - } else if (stmt is AlternativeStmt) { - var s = (AlternativeStmt)stmt; - foreach (var alt in s.Alternatives) { - foreach (var ss in alt.Body) { - CheckForallStatementBodyRestrictions(ss, kind); - } - } - - } else if (stmt is OneBodyLoopStmt) { - var s = (OneBodyLoopStmt)stmt; - if (s.Body != null) { - CheckForallStatementBodyRestrictions(s.Body, kind); - } - - } else if (stmt is AlternativeLoopStmt) { - var s = (AlternativeLoopStmt)stmt; - foreach (var alt in s.Alternatives) { - foreach (var ss in alt.Body) { - CheckForallStatementBodyRestrictions(ss, kind); - } - } - - } else if (stmt is ForallStmt) { - var s = (ForallStmt)stmt; - switch (s.Kind) { - case ForallStmt.BodyKind.Assign: - reporter.Error(MessageSource.Resolver, stmt, "a forall statement with heap updates is not allowed inside the body of another forall statement"); - break; - case ForallStmt.BodyKind.Call: - case ForallStmt.BodyKind.Proof: - // these are fine, since they don't update any non-local state - break; - default: - Contract.Assert(false); // unexpected kind - break; - } - - } else if (stmt is CalcStmt) { - // cool - } else if (stmt is ConcreteSyntaxStatement) { - var s = (ConcreteSyntaxStatement)stmt; - CheckForallStatementBodyRestrictions(s.ResolvedStatement, kind); - } else if (stmt is MatchStmt) { - var s = (MatchStmt)stmt; - foreach (var kase in s.Cases) { - foreach (var ss in kase.Body) { - CheckForallStatementBodyRestrictions(ss, kind); - } - } - - } else { - Contract.Assert(false); throw new cce.UnreachableException(); - } - } - - void CheckForallStatementBodyLhs(IToken tok, Expression lhs, ForallStmt.BodyKind kind) { - var idExpr = lhs as IdentifierExpr; - if (idExpr != null) { - if (scope.ContainsDecl(idExpr.Var)) { - reporter.Error(MessageSource.Resolver, tok, "body of forall statement is attempting to update a variable declared outside the forall statement"); - } - } else if (kind != ForallStmt.BodyKind.Assign) { - reporter.Error(MessageSource.Resolver, tok, "the body of the enclosing forall statement is not allowed to update heap locations"); - } - } - - /// - /// Check that a statment is a valid hint for a calculation. - /// ToDo: generalize the part for compound statements to take a delegate? - /// - public void CheckHintRestrictions(Statement stmt, ISet localsAllowedInUpdates, string where) { + public void CheckLocalityUpdates(Statement stmt, ISet localsAllowedInUpdates, string where) { Contract.Requires(stmt != null); Contract.Requires(localsAllowedInUpdates != null); Contract.Requires(where != null); - if (stmt is PredicateStmt) { - // cool - } else if (stmt is PrintStmt) { - // not allowed in ghost context - } else if (stmt is RevealStmt) { - var s = (RevealStmt)stmt; - foreach (var ss in s.ResolvedStatements) { - CheckHintRestrictions(ss, localsAllowedInUpdates, where); - } - } else if (stmt is BreakStmt) { - // already checked while resolving hints - } else if (stmt is ReturnStmt) { - reporter.Error(MessageSource.Resolver, stmt, "return statement is not allowed inside {0}", where); - } else if (stmt is YieldStmt) { - reporter.Error(MessageSource.Resolver, stmt, "yield statement is not allowed inside {0}", where); + + if (stmt is AssertStmt || stmt is ForallStmt || stmt is CalcStmt || stmt is ModifyStmt) { + // don't recurse, since CheckHintRestrictions will be called on that assert-by separately + return; } else if (stmt is AssignSuchThatStmt) { var s = (AssignSuchThatStmt)stmt; foreach (var lhs in s.Lhss) { - CheckHintLhs(lhs.tok, lhs.Resolved, localsAllowedInUpdates, where); + CheckLocalityUpdatesLhs(lhs, localsAllowedInUpdates, @where); } } else if (stmt is AssignStmt) { var s = (AssignStmt)stmt; - CheckHintLhs(s.Lhs.tok, s.Lhs.Resolved, localsAllowedInUpdates, where); + CheckLocalityUpdatesLhs(s.Lhs, localsAllowedInUpdates, @where); } else if (stmt is CallStmt) { var s = (CallStmt)stmt; - if (s.Method.Mod.Expressions.Count != 0) { - reporter.Error(MessageSource.Resolver, stmt, "calls to methods with side-effects are not allowed inside {0}", where); - } foreach (var lhs in s.Lhs) { - CheckHintLhs(lhs.tok, lhs.Resolved, localsAllowedInUpdates, where); - } - } else if (stmt is UpdateStmt) { - var s = (UpdateStmt)stmt; - foreach (var ss in s.ResolvedStatements) { - CheckHintRestrictions(ss, localsAllowedInUpdates, where); + CheckLocalityUpdatesLhs(lhs, localsAllowedInUpdates, @where); } } else if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; s.Locals.Iter(local => localsAllowedInUpdates.Add(local)); - if (s.Update != null) { - CheckHintRestrictions(s.Update, localsAllowedInUpdates, where); - } - } else if (stmt is VarDeclPattern) { - // Are we fine? } else if (stmt is ModifyStmt) { - reporter.Error(MessageSource.Resolver, stmt, "modify statements are not allowed inside {0}", where); + // no further complaints (note, ghost interests have already checked for 'modify' statements) } else if (stmt is BlockStmt) { - var s = (BlockStmt)stmt; - var newScopeForLocals = new HashSet(localsAllowedInUpdates); - foreach (var ss in s.Body) { - CheckHintRestrictions(ss, newScopeForLocals, where); - } - - } else if (stmt is IfStmt) { - var s = (IfStmt)stmt; - CheckHintRestrictions(s.Thn, localsAllowedInUpdates, where); - if (s.Els != null) { - CheckHintRestrictions(s.Els, localsAllowedInUpdates, where); - } - - } else if (stmt is AlternativeStmt) { - var s = (AlternativeStmt)stmt; - foreach (var alt in s.Alternatives) { - foreach (var ss in alt.Body) { - CheckHintRestrictions(ss, localsAllowedInUpdates, where); - } - } - - } else if (stmt is OneBodyLoopStmt) { - var s = (OneBodyLoopStmt)stmt; - if (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0) { - reporter.Error(MessageSource.Resolver, s.Mod.Expressions[0].tok, "a loop statement used inside {0} is not allowed to have a modifies clause", where); - } - if (s.Body != null) { - CheckHintRestrictions(s.Body, localsAllowedInUpdates, where); - } - - } else if (stmt is AlternativeLoopStmt) { - var s = (AlternativeLoopStmt)stmt; - if (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0) { - reporter.Error(MessageSource.Resolver, s.Mod.Expressions[0].tok, "a loop statement used inside {0} is not allowed to have a modifies clause", where); - } - foreach (var alt in s.Alternatives) { - foreach (var ss in alt.Body) { - CheckHintRestrictions(ss, localsAllowedInUpdates, where); - } - } - - } else if (stmt is ForallStmt) { - var s = (ForallStmt)stmt; - switch (s.Kind) { - case ForallStmt.BodyKind.Assign: - reporter.Error(MessageSource.Resolver, stmt, "a forall statement with heap updates is not allowed inside {0}", where); - break; - case ForallStmt.BodyKind.Call: - case ForallStmt.BodyKind.Proof: - // these are fine, since they don't update any non-local state - break; - default: - Contract.Assert(false); // unexpected kind - break; - } - - } else if (stmt is CalcStmt) { - // cool - - } else if (stmt is MatchStmt) { - var s = (MatchStmt)stmt; - foreach (var kase in s.Cases) { - foreach (var ss in kase.Body) { - CheckHintRestrictions(ss, localsAllowedInUpdates, where); - } - } + localsAllowedInUpdates = new HashSet(localsAllowedInUpdates); + // use this new set for the recursive calls + } - } else { - Contract.Assert(false); throw new cce.UnreachableException(); + foreach (var ss in stmt.SubStatements) { + CheckLocalityUpdates(ss, localsAllowedInUpdates, where); } } - void CheckHintLhs(IToken tok, Expression lhs, ISet localsAllowedInUpdates, string where) { - Contract.Requires(tok != null); + void CheckLocalityUpdatesLhs(Expression lhs, ISet localsAllowedInUpdates, string @where) { Contract.Requires(lhs != null); Contract.Requires(localsAllowedInUpdates != null); Contract.Requires(where != null); - var idExpr = lhs as IdentifierExpr; - if (idExpr == null) { - reporter.Error(MessageSource.Resolver, tok, "{0} is not allowed to update heap locations", where); - } else if (!localsAllowedInUpdates.Contains(idExpr.Var)) { - reporter.Error(MessageSource.Resolver, tok, "{0} is not allowed to update a variable it doesn't declare", where); + + lhs = lhs.Resolved; + if (lhs is IdentifierExpr idExpr && !localsAllowedInUpdates.Contains(idExpr.Var)) { + reporter.Error(MessageSource.Resolver, lhs.tok, "{0} is not allowed to update a variable it doesn't declare", where); } } @@ -15304,9 +15150,7 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { var r = e.S as UpdateStmt; if (r != null && r.ResolvedStatements.Count == 1) { var call = r.ResolvedStatements[0] as CallStmt; - if (call.Method.Mod.Expressions.Count != 0) { - reporter.Error(MessageSource.Resolver, call, "calls to methods with side-effects are not allowed inside a statement expression"); - } else if (call.Method is TwoStateLemma && !opts.twoState) { + if (call.Method is TwoStateLemma && !opts.twoState) { reporter.Error(MessageSource.Resolver, call, "two-state lemmas can only be used in two-state contexts"); } } diff --git a/Source/Dafny/Verifier/Translator.TrStatement.cs b/Source/Dafny/Verifier/Translator.TrStatement.cs index fb3f95d41da..e61bf713ed6 100644 --- a/Source/Dafny/Verifier/Translator.TrStatement.cs +++ b/Source/Dafny/Verifier/Translator.TrStatement.cs @@ -380,7 +380,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List f == null); var localSurrogates = fields.ConvertAll(f => new Bpl.LocalVariable(f.tok, new TypedIdent(f.tok, SurrogateName(f), TrType(f.Type)))); locals.AddRange(localSurrogates); - fields.Iter(f => AddDefiniteAssignmentTrackerSurrogate(f, cl, locals)); + fields.Iter(f => AddDefiniteAssignmentTrackerSurrogate(f, cl, locals, codeContext is Constructor && codeContext.IsGhost)); Contract.Assert(!inBodyInitContext); inBodyInitContext = true; @@ -1807,7 +1807,7 @@ void TrLoop(LoopStmt s, Expression Guard, BodyTranslator/*?*/ bodyTr, modifiesClause.AddRange(explicitModifies); } // include boilerplate invariants - foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, modifiesClause, s.IsGhost, etranPreLoop, etran, etran.Old)) { + foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, modifiesClause, s.IsGhost, codeContext.AllowsAllocation, etranPreLoop, etran, etran.Old)) { if (tri.IsFree) { invariants.Add(TrAssumeCmd(s.Tok, tri.Expr)); } else { @@ -2402,7 +2402,7 @@ void TrForallStmtCall(IToken tok, List boundVars, List { heapIdExpr, etran.Tick() })); Contract.Assert(s0.Method.Mod.Expressions.Count == 0); // checked by the resolver - foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(tok, new List(), s0.IsGhost, initEtran, etran, initEtran)) { + foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(tok, new List(), s0.IsGhost, s0.Method.AllowsAllocation, initEtran, etran, initEtran)) { if (tri.IsFree) { exporter.Add(TrAssumeCmd(tok, tri.Expr)); } diff --git a/Source/Dafny/Verifier/Translator.cs b/Source/Dafny/Verifier/Translator.cs index b0d6e47b06e..6624fc9e17d 100644 --- a/Source/Dafny/Verifier/Translator.cs +++ b/Source/Dafny/Verifier/Translator.cs @@ -2448,7 +2448,7 @@ Bpl.Procedure AddIteratorProc(IteratorDecl iter, MethodTranslationKind kind) { } } } - foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(iter.tok, iter.Modifies.Expressions, false, etran.Old, etran, etran.Old)) { + foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(iter.tok, iter.Modifies.Expressions, false, iter.AllowsAllocation, etran.Old, etran, etran.Old)) { ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment)); } } @@ -4522,7 +4522,7 @@ void AddMethodImpl(Method m, Bpl.Procedure proc, bool wellformednessProc) { // play havoc with the heap according to the modifies clause builder.Add(new Bpl.HavocCmd(m.tok, new List { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr })); // assume the usual two-state boilerplate information - foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, etran.Old, etran, etran.Old)) { + foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, m.AllowsAllocation, etran.Old, etran, etran.Old)) { if (tri.IsFree) { builder.Add(TrAssumeCmd(m.tok, tri.Expr)); } @@ -4614,12 +4614,12 @@ void AddExistingDefiniteAssignmentTracker(IVariable p, bool forceGhostVar) { } } - void AddDefiniteAssignmentTrackerSurrogate(Field field, TopLevelDeclWithMembers enclosingClass, List localVariables) { + void AddDefiniteAssignmentTrackerSurrogate(Field field, TopLevelDeclWithMembers enclosingClass, List localVariables, bool forceGhostVar) { Contract.Requires(field != null); Contract.Requires(localVariables != null); var type = Resolver.SubstType(field.Type, enclosingClass.ParentFormalTypeParametersToActuals); - if (!NeedsDefiniteAssignmentTracker(field.IsGhost, type)) { + if (!NeedsDefiniteAssignmentTracker(field.IsGhost || forceGhostVar, type)) { return; } var nm = SurrogateName(field); @@ -5119,17 +5119,6 @@ private static Dictionary GetTypeArgumentSubstitutionMap(Me return typeMap; } - private void HavocFunctionFrameLocations(Function f, BoogieStmtListBuilder builder, ExpressionTranslator etran, List localVariables) { - // play havoc with the heap according to the modifies clause - builder.Add(new Bpl.HavocCmd(f.tok, new List { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr })); - // assume the usual two-state boilerplate information - foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(f.tok, f.Reads, f.IsGhost, etran.Old, etran, etran.Old)) { - if (tri.IsFree) { - builder.Add(TrAssumeCmd(f.tok, tri.Expr)); - } - } - } - private void AddFunctionOverrideSubsetChk(Function func, BoogieStmtListBuilder builder, ExpressionTranslator etran, List localVariables, Dictionary substMap) { //getting framePrime List traitFrameExps = new List(); @@ -5283,7 +5272,7 @@ private void HavocMethodFrameLocations(Method m, BoogieStmtListBuilder builder, // play havoc with the heap according to the modifies clause builder.Add(new Bpl.HavocCmd(m.tok, new List { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr })); // assume the usual two-state boilerplate information - foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, etran.Old, etran, etran.Old)) { + foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, m.AllowsAllocation, etran.Old, etran, etran.Old)) { if (tri.IsFree) { builder.Add(TrAssumeCmd(m.tok, tri.Expr)); } @@ -9842,7 +9831,7 @@ Bpl.Procedure AddMethod(Method m, MethodTranslationKind kind) { var fresh = Bpl.Expr.Not(etran.Old.IsAlloced(m.tok, new Bpl.IdentifierExpr(m.tok, "this", TrReceiverType(m)))); AddEnsures(ens, Ensures(m.tok, false, fresh, null, "constructor allocates the object")); } - foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, ordinaryEtran.Old, ordinaryEtran, ordinaryEtran.Old)) { + foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, m.AllowsAllocation, ordinaryEtran.Old, ordinaryEtran, ordinaryEtran.Old)) { AddEnsures(ens, Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment)); } @@ -10023,7 +10012,8 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes /// S2. the post-state of the two-state interval /// This method assumes that etranPre denotes S1, etran denotes S2, and that etranMod denotes S0. /// - List/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, List/*!*/ modifiesClause, bool isGhostContext, + List/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, + List/*!*/ modifiesClause, bool isGhostContext, bool canAllocate, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod) { Contract.Requires(tok != null); Contract.Requires(modifiesClause != null); @@ -10032,16 +10022,16 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes Contract.Ensures(cce.NonNullElements(Contract.Result>())); var boilerplate = new List(); - if (isGhostContext && modifiesClause.Count == 0) { + if (!canAllocate && modifiesClause.Count == 0) { // plain and simple: S1 == S2 boilerplate.Add(new BoilerplateTriple(tok, true, Bpl.Expr.Eq(etranPre.HeapExpr, etran.HeapExpr), null, "frame condition")); } else { bool fieldGranularity = true; bool objectGranularity = !fieldGranularity; // the frame condition, which is free since it is checked with every heap update and call - boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, isGhostContext, Resolver.FrameExpressionUse.Modifies, etranPre, etran, etranMod, objectGranularity), null, "frame condition: object granularity")); + boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, canAllocate, Resolver.FrameExpressionUse.Modifies, etranPre, etran, etranMod, objectGranularity), null, "frame condition: object granularity")); if (modifiesClause.Exists(fe => fe.FieldName != null)) { - boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, isGhostContext, Resolver.FrameExpressionUse.Modifies, etranPre, etran, etranMod, fieldGranularity), null, "frame condition: field granularity")); + boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, canAllocate, Resolver.FrameExpressionUse.Modifies, etranPre, etran, etranMod, fieldGranularity), null, "frame condition: field granularity")); } // HeapSucc(S1, S2) or HeapSuccGhost(S1, S2) Bpl.Expr heapSucc = HeapSucc(etranPre.HeapExpr, etran.HeapExpr, isGhostContext); @@ -10064,7 +10054,7 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes /// if it's in the frame, then it is unchanged, /// and if it has a field designation, then furthermore 'alloc' is unchanged /// - Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List/*!*/ frame, bool isGhostContext, Resolver.FrameExpressionUse use, + Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List/*!*/ frame, bool canAllocate, Resolver.FrameExpressionUse use, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod, bool fieldGranularity) { Contract.Requires(tok != null); Contract.Requires(etran != null); @@ -10080,7 +10070,7 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes // (forall o: ref, f: Field alpha :: { $Heap[o][f] } // o != null // #if use==Modifies - // && old($Heap)[o][alloc] // include only in non-ghost contexts + // && old($Heap)[o][alloc] // include only in contexts that can allocate // #endif // ==> // #if use==Modifies @@ -10100,7 +10090,7 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes // (forall o: ref :: { $Heap[o] } // o != null // #if use==Modifies - // && old($Heap)[o][alloc] // include only in non-ghost contexts + // && old($Heap)[o][alloc] // include only in contexts that can allocate // #endif // ==> // #if use==Modifies @@ -10138,7 +10128,7 @@ public BoilerplateTriple(IToken tok, bool isFree, Bpl.Expr expr, string errorMes } Bpl.Expr ante = Bpl.Expr.Neq(o, predef.Null); - if (!isGhostContext && use == Resolver.FrameExpressionUse.Modifies) { + if (canAllocate && use == Resolver.FrameExpressionUse.Modifies) { ante = Bpl.Expr.And(ante, etranMod.IsAlloced(tok, o)); } var eq = Bpl.Expr.Eq(heapOF, preHeapOF); diff --git a/Source/DafnyDriver/BoogieXmlConvertor.cs b/Source/DafnyDriver/BoogieXmlConvertor.cs new file mode 100644 index 00000000000..e77583155ab --- /dev/null +++ b/Source/DafnyDriver/BoogieXmlConvertor.cs @@ -0,0 +1,106 @@ +//----------------------------------------------------------------------------- +// +// Copyright (C) Microsoft Corporation. All Rights Reserved. +// Copyright by the contributors to the Dafny Project +// SPDX-License-Identifier: MIT +// +//----------------------------------------------------------------------------- +using System; +using System.Collections.Generic; +using System.Linq; +using System.Xml.Linq; +using Microsoft.VisualStudio.TestPlatform.Extensions.TrxLogger; +using Microsoft.VisualStudio.TestPlatform.ObjectModel; +using Microsoft.VisualStudio.TestPlatform.ObjectModel.Client; +using Microsoft.VisualStudio.TestPlatform.ObjectModel.Logging; + +namespace Microsoft.Dafny { + + /// + /// Utility to parse the XML format produced by Boogie's /xml option and emit the + /// results therein as test logger events, allowing us to deliver verification results + /// as test results through common loggers on the .NET platform. For now we are just supporting + /// outputting TRX files, which can be understood and visualized by various tools. + /// + public static class BoogieXmlConvertor { + + public static void RaiseTestLoggerEvents(string fileName, string loggerConfig) { + // The only supported value for now + if (loggerConfig != "trx") { + throw new ArgumentException($"Unsupported verification logger config: {loggerConfig}"); + } + + var events = new LocalTestLoggerEvents(); + var logger = new TrxLogger(); + // Provide just enough configuration for the TRX logger to work + logger.Initialize(events, new Dictionary { + ["TestRunDirectory"] = Constants.DefaultResultsDirectory + }); + events.EnableEvents(); + + // Sort failures to the top, and then slower procedures first. + // Loggers may not maintain this ordering unfortunately. + var results = ReadTestResults(fileName) + .OrderBy(r => r.Outcome == TestOutcome.Passed) + .ThenByDescending(r => r.Duration); + foreach (var result in results) { + events.RaiseTestResult(new TestResultEventArgs(result)); + } + + events.RaiseTestRunComplete(new TestRunCompleteEventArgs( + new TestRunStatistics(), + false, false, null, null, new TimeSpan() + )); + } + + public static IEnumerable ReadTestResults(string xmlFileName) { + string currentFileFragment = null; + var root = XElement.Load(xmlFileName); + var testResults = new List(); + foreach (var child in root.Nodes().OfType()) { + switch (child.Name.LocalName) { + case "fileFragment": + currentFileFragment = child.Attribute("name")!.Value; + break; + case "method": + testResults.Add(ToTestResult(child, currentFileFragment)); + break; + } + } + + return testResults; + } + + private static TestResult ToTestResult(XElement node, string currentFileFragment) { + var name = node.Attribute("name")!.Value; + var startTime = node.Attribute("startTime")!.Value; + var conclusionNode = node.Nodes() + .OfType() + .Single(n => n.Name.LocalName == "conclusion"); + var endTime = conclusionNode.Attribute("endTime")!.Value; + var duration = float.Parse(conclusionNode.Attribute("duration")!.Value); + var outcome = conclusionNode.Attribute("outcome")!.Value; + + var testCase = new TestCase { + FullyQualifiedName = name, + ExecutorUri = new Uri("executor://dafnyverifier/v1"), + Source = currentFileFragment + }; + + var testResult = new TestResult(testCase) { + StartTime = DateTimeOffset.Parse(startTime), + EndTime = DateTimeOffset.Parse(endTime), + Duration = TimeSpan.FromMilliseconds((long)(duration * 1000)) + }; + + if (outcome == "correct") { + testResult.Outcome = TestOutcome.Passed; + } else { + testResult.Outcome = TestOutcome.Failed; + testResult.ErrorMessage = outcome; + } + + return testResult; + } + } +} \ No newline at end of file diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 584e807a7a4..addf840c226 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -10,9 +10,7 @@ // - main program for taking a Dafny program and verifying it //--------------------------------------------------------------------------------------------- -using System.Security; -using DafnyServer.CounterExampleGeneration; -using DafnyTestGeneration; +using DafnyServer.CounterexampleGeneration; namespace Microsoft.Dafny { using System; @@ -66,6 +64,9 @@ public static int ThreadMain(string[] args) { if (CommandLineOptions.Clo.XmlSink != null) { CommandLineOptions.Clo.XmlSink.Close(); + if (DafnyOptions.O.VerificationLoggerConfig != null) { + BoogieXmlConvertor.RaiseTestLoggerEvents(DafnyOptions.O.BoogieXmlFilename, DafnyOptions.O.VerificationLoggerConfig); + } } if (CommandLineOptions.Clo.Wait) { Console.WriteLine("Press Enter to exit."); @@ -216,7 +217,7 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(string[] ar return CommandLineArgumentsResult.PREPROCESSING_ERROR; } - if (DafnyOptions.O.ExtractCounterExample && DafnyOptions.O.ModelViewFile == null) { + if (DafnyOptions.O.ExtractCounterexample && DafnyOptions.O.ModelViewFile == null) { ExecutionEngine.printer.ErrorWriteLine(Console.Out, "*** Error: ModelView file must be specified when attempting counterexample extraction"); return CommandLineArgumentsResult.PREPROCESSING_ERROR; @@ -297,7 +298,7 @@ static ExitValue ProcessFiles(IList/*!*/ dafnyFiles, ReadOnlyCol if (err == null && dafnyProgram != null && DafnyOptions.O.PrintFunctionCallGraph) { Util.PrintFunctionCallGraph(dafnyProgram); } - if (dafnyProgram != null && DafnyOptions.O.ExtractCounterExample && exitValue == ExitValue.VERIFICATION_ERROR) { + if (dafnyProgram != null && DafnyOptions.O.ExtractCounterexample && exitValue == ExitValue.VERIFICATION_ERROR) { PrintCounterexample(DafnyOptions.O.ModelViewFile); } return exitValue; @@ -596,8 +597,14 @@ public override void ReportBplError(IToken tok, string message, bool error, Text #region Compilation - static string WriteDafnyProgramToFiles(Compiler compiler, string dafnyProgramName, bool targetProgramHasErrors, - string targetProgramText, string/*?*/ callToMain, Dictionary otherFiles, TextWriter outputWriter) { + private record TargetPaths(string Directory, string Filename) { + private Func DeleteDot = p => p == "." ? "" : p; + public string RelativeDirectory => DeleteDot(Path.GetRelativePath(Directory, Path.GetDirectoryName(Filename))); + public string RelativeFilename => DeleteDot(Path.GetRelativePath(Directory, Filename)); + public string SourceDirectory => Path.GetDirectoryName(Filename); + } + + private static TargetPaths GenerateTargetPaths(Compiler compiler, string dafnyProgramName) { string targetExtension; string baseName = Path.GetFileNameWithoutExtension(dafnyProgramName); string targetBaseDir = ""; @@ -632,34 +639,39 @@ static string WriteDafnyProgramToFiles(Compiler compiler, string dafnyProgramNam // Note that using Path.ChangeExtension here does the wrong thing when dafnyProgramName has multiple periods (e.g., a.b.dfy) string targetBaseName = baseName + "." + targetExtension; string targetDir = Path.Combine(Path.GetDirectoryName(dafnyProgramName), targetBaseDir); + + string targetFilename = Path.Combine(targetDir, targetBaseName); + + return new TargetPaths(Directory: Path.GetDirectoryName(dafnyProgramName), Filename: targetFilename); + } + + static void WriteDafnyProgramToFiles(TargetPaths paths, bool targetProgramHasErrors, string targetProgramText, + string/*?*/ callToMain, Dictionary otherFiles, TextWriter outputWriter) { // WARNING: Make sure that Directory.Delete is only called when the compilation target is Java. // If called during C# or JS compilation, you will lose your entire target directory. // Purpose is to delete the old generated folder with the Java compilation output and replace all contents. - if (DafnyOptions.O.CompileTarget is DafnyOptions.CompilationTarget.Java && Directory.Exists(targetDir)) { - Directory.Delete(targetDir, true); + if (DafnyOptions.O.CompileTarget is DafnyOptions.CompilationTarget.Java && Directory.Exists(paths.SourceDirectory)) { + Directory.Delete(paths.SourceDirectory, true); } - string targetFilename = Path.Combine(targetDir, targetBaseName); - WriteFile(targetFilename, targetProgramText, callToMain); - string relativeTarget = Path.Combine(targetBaseDir, targetBaseName); + WriteFile(paths.Filename, targetProgramText, callToMain); + if (targetProgramHasErrors) { // Something went wrong during compilation (e.g., the compiler may have found an "assume" statement). // As a courtesy, we're still printing the text of the generated target program. We print a message regardless // of the CompileVerbose settings. - outputWriter.WriteLine("Wrote textual form of partial target program to {0}", relativeTarget); + outputWriter.WriteLine("Wrote textual form of partial target program to {0}", paths.RelativeFilename); } else if (DafnyOptions.O.CompileVerbose) { - outputWriter.WriteLine("Wrote textual form of target program to {0}", relativeTarget); + outputWriter.WriteLine("Wrote textual form of target program to {0}", paths.RelativeFilename); } foreach (var entry in otherFiles) { var filename = entry.Key; - WriteFile(Path.Combine(targetDir, filename), entry.Value); + WriteFile(Path.Join(paths.SourceDirectory, filename), entry.Value); if (DafnyOptions.O.CompileVerbose) { - outputWriter.WriteLine("Additional target code written to {0}", Path.Combine(targetBaseDir, filename)); + outputWriter.WriteLine("Additional target code written to {0}", Path.Join(paths.RelativeDirectory, filename)); } } - - return targetFilename; } static void WriteFile(string filename, string text, string moreText = null) { @@ -749,10 +761,10 @@ public static bool CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyP compiler.Coverage.WriteLegendFile(); // blurt out the code to a file, if requested, or if other target-language files were specified on the command line. - string targetFilename = null; + var paths = GenerateTargetPaths(compiler, dafnyProgramName); if (DafnyOptions.O.SpillTargetCode > 0 || otherFileNames.Count > 0 || (invokeCompiler && !compiler.SupportsInMemoryCompilation) || (invokeCompiler && compiler.TextualTargetIsExecutable && !DafnyOptions.O.RunAfterCompile)) { - targetFilename = WriteDafnyProgramToFiles(compiler, dafnyProgramName, targetProgramHasErrors, targetProgramText, callToMain, otherFiles, outputWriter); + WriteDafnyProgramToFiles(paths, targetProgramHasErrors, targetProgramText, callToMain, otherFiles, outputWriter); } if (targetProgramHasErrors) { @@ -764,7 +776,7 @@ public static bool CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyP } // compile the program into an assembly - var compiledCorrectly = compiler.CompileTargetProgram(dafnyProgramName, targetProgramText, callToMain, targetFilename, otherFileNames, + var compiledCorrectly = compiler.CompileTargetProgram(dafnyProgramName, targetProgramText, callToMain, paths.Filename, otherFileNames, hasMain && DafnyOptions.O.RunAfterCompile, outputWriter, out var compilationResult); if (compiledCorrectly && DafnyOptions.O.RunAfterCompile) { if (hasMain) { @@ -772,7 +784,7 @@ public static bool CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyP outputWriter.WriteLine("Running..."); outputWriter.WriteLine(); } - compiledCorrectly = compiler.RunTargetProgram(dafnyProgramName, targetProgramText, callToMain, targetFilename, otherFileNames, compilationResult, outputWriter); + compiledCorrectly = compiler.RunTargetProgram(dafnyProgramName, targetProgramText, callToMain, paths.Filename, otherFileNames, compilationResult, outputWriter); } else { // make sure to give some feedback to the user if (DafnyOptions.O.CompileVerbose) { diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj index 29834976aec..73341969ff7 100644 --- a/Source/DafnyDriver/DafnyDriver.csproj +++ b/Source/DafnyDriver/DafnyDriver.csproj @@ -14,6 +14,22 @@ false false + + + + + + + + + + + + + + + + diff --git a/Source/DafnyDriver/LocalTestLoggerEvents.cs b/Source/DafnyDriver/LocalTestLoggerEvents.cs new file mode 100644 index 00000000000..d71924afa1f --- /dev/null +++ b/Source/DafnyDriver/LocalTestLoggerEvents.cs @@ -0,0 +1,426 @@ +using System; +using System.Collections.ObjectModel; +using System.Diagnostics; +using Microsoft.VisualStudio.TestPlatform.Common; +using Microsoft.VisualStudio.TestPlatform.ObjectModel; +using Microsoft.VisualStudio.TestPlatform.ObjectModel.Client; +using Microsoft.VisualStudio.TestPlatform.ObjectModel.Logging; +using Microsoft.VisualStudio.TestPlatform.Utilities; + +namespace Microsoft.Dafny { + + /// + /// Simple implementation of TestLoggerEvents in order to drive test results loggers. + /// Copied and modified (to remove the parent TestSessionMessageLogger reference) + /// from the internal but MIT-licensed version from inside VSTest: + /// https://github.com/microsoft/vstest/blob/main/src/Microsoft.TestPlatform.Common/Logging/InternalTestLoggerEvents.cs + /// + /// Since this class is copied and modified from existing source, I haven't made any effort + /// to align coding styles or clean up anything, for the sake of simplicity. + /// + public class LocalTestLoggerEvents : TestLoggerEvents, IDisposable { + #region Fields + + /// + /// Queue used for events which are to be sent to the loggers. + /// + /// + /// Using the queue accomplishes two things. + /// 1. Loggers do not need to be written to be thread safe because + /// we will only be raising one event to them at a time. + /// 2. Allows all events to go to all loggers even during initialization + /// because we queue up all events sent until raising of events to the + /// loggers is enabled + /// + private JobQueue loggerEventQueue; + + /// + /// Keeps track if we are disposed. + /// + private bool isDisposed = false; + + /// + /// Specifies whether logger event queue is bounded or not + /// + private bool isBoundsOnLoggerEventQueueEnabled; + + #endregion + + #region Constructor + + /// + /// Default constructor. + /// + public LocalTestLoggerEvents() { + + // Initialize the queue and pause it. + // Note: The queue will be resumed when events are enabled. This is done so all + // loggers receive all messages. + this.isBoundsOnLoggerEventQueueEnabled = IsBoundsEnabledOnLoggerEventQueue(); + this.loggerEventQueue = new JobQueue( + this.ProcessQueuedJob, + "Test Logger", + GetMaxNumberOfJobsInQueue(), + GetMaxBytesQueueCanHold(), + this.isBoundsOnLoggerEventQueueEnabled, + (message) => EqtTrace.Error(message)); + this.loggerEventQueue.Pause(); + } + + #endregion + + #region Events + + /// + /// Raised when a test message is received. + /// + public override event EventHandler TestRunMessage; + + /// + /// Raised when a test run starts. + /// + public override event EventHandler TestRunStart; + + /// + /// Raised when a test result is received. + /// + public override event EventHandler TestResult; + + /// + /// Raised when a test run is complete. + /// + public override event EventHandler TestRunComplete; + + /// + /// Raised when test discovery starts. + /// + public override event EventHandler DiscoveryStart; + + /// + /// Raised when a discovery message is received. + /// + public override event EventHandler DiscoveryMessage; + + /// + /// Raised when discovered tests are received + /// + public override event EventHandler DiscoveredTests; + + /// + /// Raised when test discovery is complete + /// + public override event EventHandler DiscoveryComplete; + + #endregion + + #region IDisposable + + /// + /// Waits for all pending messages to be processed by the loggers cleans up. + /// + public void Dispose() { + if (this.isDisposed) { + return; + } + + this.isDisposed = true; + + // Ensure that the queue is processed before returning. + this.loggerEventQueue.Resume(); + this.loggerEventQueue.Dispose(); + } + + #endregion + + #region Internal Methods + + /// + /// Enables sending of events to the loggers which are registered and flushes the queue. + /// + /// + /// By default events are disabled and will not be raised until this method is called. + /// This is done because during logger initialization, errors could be sent and we do not + /// want them broadcast out to the loggers until all loggers have been enabled. Without this + /// all loggers would not receive the errors which were sent prior to initialization finishing. + /// + internal void EnableEvents() { + this.CheckDisposed(); + + this.loggerEventQueue.Resume(); + + // Allow currently queued events to flush from the queue. This is done so that information + // logged during initialization completes processing before we begin other tasks. This is + // important for instance when errors are logged during initialization and need to be output + // to the console before we begin outputting other information to the console. + this.loggerEventQueue.Flush(); + } + + /// + /// Raises a test run message event to the enabled loggers. + /// + /// Arguments to be raised. + internal void RaiseTestRunMessage(TestRunMessageEventArgs args) { + if (args == null) { + throw new ArgumentNullException(nameof(args)); + } + + this.CheckDisposed(); + + // Sending 0 size as this event is not expected to contain any data. + this.SafeInvokeAsync(() => this.TestRunMessage, args, 0, "InternalTestLoggerEvents.SendTestRunMessage"); + } + + internal void WaitForEventCompletion() { + this.loggerEventQueue.Flush(); + } + + /// + /// Raises a test result event to the enabled loggers. + /// + /// Arguments to to be raised. + internal void RaiseTestResult(TestResultEventArgs args) { + ValidateArg.NotNull(args, nameof(args)); + + this.CheckDisposed(); + + // find the approx size of test result + int resultSize = 0; + if (this.isBoundsOnLoggerEventQueueEnabled) { + resultSize = FindTestResultSize(args) * sizeof(char); + } + + this.SafeInvokeAsync(() => this.TestResult, args, resultSize, "InternalTestLoggerEvents.SendTestResult"); + } + + /// + /// Raises the test run start event to enabled loggers. + /// + /// Arguments to be raised. + internal void RaiseTestRunStart(TestRunStartEventArgs args) { + ValidateArg.NotNull(args, nameof(args)); + + CheckDisposed(); + + this.SafeInvokeAsync(() => this.TestRunStart, args, 0, "InternalTestLoggerEvents.SendTestRunStart"); + } + + /// + /// Raises a discovery start event to the enabled loggers. + /// + /// Arguments to be raised. + internal void RaiseDiscoveryStart(DiscoveryStartEventArgs args) { + ValidateArg.NotNull(args, nameof(args)); + + CheckDisposed(); + + SafeInvokeAsync(() => this.DiscoveryStart, args, 0, "InternalTestLoggerEvents.SendDiscoveryStart"); + } + + /// + /// Raises a discovery message event to the enabled loggers. + /// + /// Arguments to be raised. + internal void RaiseDiscoveryMessage(TestRunMessageEventArgs args) { + ValidateArg.NotNull(args, nameof(args)); + + this.CheckDisposed(); + + // Sending 0 size as this event is not expected to contain any data. + this.SafeInvokeAsync(() => this.DiscoveryMessage, args, 0, "InternalTestLoggerEvents.SendDiscoveryMessage"); + } + + /// + /// Raises discovered tests event to the enabled loggers. + /// + /// Arguments to be raised. + internal void RaiseDiscoveredTests(DiscoveredTestsEventArgs args) { + ValidateArg.NotNull(args, nameof(args)); + + CheckDisposed(); + + SafeInvokeAsync(() => this.DiscoveredTests, args, 0, "InternalTestLoggerEvents.SendDiscoveredTests"); + } + + /// + /// Raises discovery complete event to the enabled loggers. + /// + /// Arguments to be raised. + internal void RaiseDiscoveryComplete(DiscoveryCompleteEventArgs args) { + ValidateArg.NotNull(args, nameof(args)); + + CheckDisposed(); + + // Sending 0 size as this event is not expected to contain any data. + SafeInvokeAsync(() => this.DiscoveryComplete, args, 0, "InternalTestLoggerEvents.SendDiscoveryComplete"); + + // Wait for the loggers to finish processing the messages for the run. + this.loggerEventQueue.Flush(); + } + + /// + /// Raises test run complete to the enabled loggers + /// + /// Arguments to be raised + internal void RaiseTestRunComplete(TestRunCompleteEventArgs args) { + ValidateArg.NotNull(args, nameof(args)); + + CheckDisposed(); + + // Size is being send as 0. (It is good to send the size as the job queue uses it) + SafeInvokeAsync(() => this.TestRunComplete, args, 0, "InternalTestLoggerEvents.SendTestRunComplete"); + + // Wait for the loggers to finish processing the messages for the run. + this.loggerEventQueue.Flush(); + } + + /// + /// Raise the test run complete event to test loggers and waits + /// for the events to be processed. + /// + /// Specifies the stats of the test run. + /// Specifies whether the test run is canceled. + /// Specifies whether the test run is aborted. + /// Specifies the error that occurs during the test run. + /// Run level attachment sets + /// Time elapsed in just running the tests. + internal void CompleteTestRun(ITestRunStatistics stats, bool isCanceled, bool isAborted, Exception error, + Collection attachmentSet, TimeSpan elapsedTime) { + this.CheckDisposed(); + + var args = new TestRunCompleteEventArgs(stats, isCanceled, isAborted, error, attachmentSet, elapsedTime); + + // Sending 0 size as this event is not expected to contain any data. + this.SafeInvokeAsync(() => this.TestRunComplete, args, 0, "InternalTestLoggerEvents.SendTestRunComplete"); + + // Wait for the loggers to finish processing the messages for the run. + this.loggerEventQueue.Flush(); + } + + #endregion + + #region Private Members + + /// + /// Called when a test run message is sent through the ITestRunMessageLogger which is exported. + /// + private void TestRunMessageHandler(object sender, TestRunMessageEventArgs e) { + // Broadcast the message to the loggers. + this.SafeInvokeAsync(() => this.TestRunMessage, e, 0, "InternalTestLoggerEvents.SendMessage"); + } + + /// + /// Invokes each of the subscribers of the event and handles exceptions which are thrown + /// ensuring that each handler is invoked even if one throws. + /// The actual calling of the subscribers is done on a background thread. + /// + private void SafeInvokeAsync(Func eventHandlersFactory, EventArgs args, int size, + string traceDisplayName) { + ValidateArg.NotNull(eventHandlersFactory, nameof(eventHandlersFactory)); + ValidateArg.NotNull(args, nameof(args)); + + // Invoke the handlers on a background thread. + this.loggerEventQueue.QueueJob( + () => { + var eventHandlers = eventHandlersFactory(); + eventHandlers?.SafeInvoke(this, args, traceDisplayName); + }, size); + } + + /// + /// Method called to process a job which is coming from the logger event queue. + /// + private void ProcessQueuedJob(Action action) { + action(); + } + + /// + /// Throws if we are disposed. + /// + private void CheckDisposed() { + if (this.isDisposed) { + throw new ObjectDisposedException(typeof(TestLoggerEvents).FullName); + } + } + + /// + /// The method parses the config file of vstest.console.exe to see if the Max Job Queue Length is defined. + /// Return the Max Queue Length so defined or a default value specified by TestPlatformDefaults.DefaultMaxLoggerEventsToCache + /// + private int GetMaxNumberOfJobsInQueue() { + return GetSetting(TestPlatformDefaults.MaxNumberOfEventsLoggerEventQueueCanHold, + TestPlatformDefaults.DefaultMaxNumberOfEventsLoggerEventQueueCanHold); + } + + /// + /// The method parses the config file of vstest.console.exe to see if the Max Job Queue size is defined. + /// Return the Max Queue size so defined or a default value specified by TestPlatformDefaults.DefaultMaxJobQueueSize + /// + private int GetMaxBytesQueueCanHold() { + return GetSetting(TestPlatformDefaults.MaxBytesLoggerEventQueueCanHold, + TestPlatformDefaults.DefaultMaxBytesLoggerEventQueueCanHold); + } + + /// + /// Returns whether flow control on logger events queue should be enabled or not. Default is enabled. + /// + private static bool IsBoundsEnabledOnLoggerEventQueue() { + bool enableBounds; +#if NETFRAMEWORK + string enableBoundsOnEventQueueIsDefined = + ConfigurationManager.AppSettings[TestPlatformDefaults.EnableBoundsOnLoggerEventQueue]; +#else + string enableBoundsOnEventQueueIsDefined = null; +#endif + if (string.IsNullOrEmpty(enableBoundsOnEventQueueIsDefined)) { + enableBounds = TestPlatformDefaults.DefaultEnableBoundsOnLoggerEventQueue; + } else { + if (!(bool.TryParse(enableBoundsOnEventQueueIsDefined, out enableBounds))) { + enableBounds = TestPlatformDefaults.DefaultEnableBoundsOnLoggerEventQueue; + } + } + + return enableBounds; + } + + /// + /// Returns the approximate size of a TestResult instance. + /// + private static int FindTestResultSize(TestResultEventArgs args) { + Debug.Assert(args != null && args.Result != null); + + int size = 0; + + if (args.Result.Messages.Count != 0) { + foreach (TestResultMessage msg in args.Result.Messages) { + if (!string.IsNullOrEmpty(msg.Text)) + size += msg.Text.Length; + } + } + + return size; + } + + /// + /// Get the appsetting value for the parameter appSettingKey. Use the parameter defaultValue if + /// value is not there or is invalid. + /// + private int GetSetting(string appSettingKey, int defaultValue) { + int value; +#if NETFRAMEWORK + string appSettingValue = ConfigurationManager.AppSettings[appSettingKey]; +#else + string appSettingValue = null; +#endif + if (string.IsNullOrEmpty(appSettingValue)) { + value = defaultValue; + } else if (!int.TryParse(appSettingValue, out value) || value < 1) { + EqtTrace.Warning("Unacceptable value '{0}' of {1}. Using default {2}", appSettingValue, appSettingKey, + defaultValue); + value = defaultValue; + } + + return value; + } + #endregion + } +} \ No newline at end of file diff --git a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs index a526830cac4..bccdbd3acd1 100644 --- a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs +++ b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs @@ -6,7 +6,7 @@ using System.Linq; using System.Text.RegularExpressions; using System.Threading.Tasks; -using DafnyServer.CounterExampleGeneration; +using DafnyServer.CounterexampleGeneration; namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Various { [TestClass] diff --git a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs index 672bddf531c..5ed821f7165 100644 --- a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs +++ b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs @@ -1,4 +1,4 @@ -using DafnyServer.CounterExampleGeneration; +using DafnyServer.CounterexampleGeneration; using Microsoft.Boogie; using Microsoft.Dafny.LanguageServer.Language; using Microsoft.Dafny.LanguageServer.Workspace; diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs index acc8238b4c1..ba2ff9f21ea 100644 --- a/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs +++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs @@ -9,7 +9,7 @@ using System.Text.RegularExpressions; using Microsoft.Boogie; -namespace DafnyServer.CounterExampleGeneration { +namespace DafnyServer.CounterexampleGeneration { /// /// a wrapper around Boogie's Model class that diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModelState.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModelState.cs index 3f0fb9daf3f..38ade895e23 100644 --- a/Source/DafnyServer/CounterExampleGeneration/DafnyModelState.cs +++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModelState.cs @@ -7,7 +7,7 @@ using System.Text.RegularExpressions; using Microsoft.Boogie; -namespace DafnyServer.CounterExampleGeneration { +namespace DafnyServer.CounterexampleGeneration { /// /// Represents a state in a `DafnyModel` and captures the values of all diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs index 92e0647b44b..1face09489d 100644 --- a/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs +++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs @@ -2,7 +2,7 @@ using System.Collections.Generic; using System.Text.RegularExpressions; -namespace DafnyServer.CounterExampleGeneration { +namespace DafnyServer.CounterexampleGeneration { /// /// Represents the type of a DafnyModelVariable. /// diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModelVariable.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModelVariable.cs index 14a3f2c6097..d37c86b1b76 100644 --- a/Source/DafnyServer/CounterExampleGeneration/DafnyModelVariable.cs +++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModelVariable.cs @@ -7,7 +7,7 @@ using System.Text.RegularExpressions; using Microsoft.Boogie; -namespace DafnyServer.CounterExampleGeneration { +namespace DafnyServer.CounterexampleGeneration { /// /// A static class for generating instance of DafnyModelvariable and its diff --git a/Source/DafnyServer/CounterExampleProvider.cs b/Source/DafnyServer/CounterExampleProvider.cs index 49bf716b1d4..9ac27da8a23 100644 --- a/Source/DafnyServer/CounterExampleProvider.cs +++ b/Source/DafnyServer/CounterExampleProvider.cs @@ -7,7 +7,7 @@ using System.Linq; using System.Runtime.Serialization; using System.Text.RegularExpressions; -using DafnyServer.CounterExampleGeneration; +using DafnyServer.CounterexampleGeneration; using Microsoft.Boogie; namespace DafnyServer { diff --git a/Source/DafnyTestGeneration/TestMethod.cs b/Source/DafnyTestGeneration/TestMethod.cs index 3d4a0042715..ee48622b540 100644 --- a/Source/DafnyTestGeneration/TestMethod.cs +++ b/Source/DafnyTestGeneration/TestMethod.cs @@ -3,7 +3,7 @@ using System.IO; using System.Linq; using System.Text.RegularExpressions; -using DafnyServer.CounterExampleGeneration; +using DafnyServer.CounterexampleGeneration; using Microsoft.Boogie; namespace DafnyTestGeneration { diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index 6e2c0a13183..3c426de6682 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -3,7 +3,7 @@ using System.IO; using System.Linq; using System.Text; -using DafnyServer.CounterExampleGeneration; +using DafnyServer.CounterexampleGeneration; using Microsoft.Boogie; using Microsoft.Dafny; using Action = System.Action; diff --git a/Source/version.cs b/Source/version.cs index 474fd7ef333..df375ed6a2c 100644 --- a/Source/version.cs +++ b/Source/version.cs @@ -1,4 +1,4 @@ using System.Reflection; -// Version 3.3.0, year 2018+3 month 10 day 20 -[assembly: AssemblyVersion("3.3.0.31020")] -[assembly: AssemblyFileVersion("3.3.0.31020")] +// Version 3.3.0, year 2018+3 month 11 day 4 +[assembly: AssemblyVersion("3.3.0.31104")] +[assembly: AssemblyFileVersion("3.3.0.31104")] diff --git a/Test/allocated1/dafny0/Parallel.dfy b/Test/allocated1/dafny0/Parallel.dfy index 4d0aac20a16..bd63bd152d7 100644 --- a/Test/allocated1/dafny0/Parallel.dfy +++ b/Test/allocated1/dafny0/Parallel.dfy @@ -6,7 +6,7 @@ class C { var n: nat var st: set - ghost method CLemma(k: int) + lemma CLemma(k: int) requires k != -23 ensures data < k // magic, isn't it (or bogus, some would say) } @@ -203,10 +203,10 @@ method OmittedRange() { class TwoState_C { ghost var data: int } -// It is not possible to achieve this postcondition in a ghost method, because ghost -// contexts are not allowed to allocate state. Callers of this ghost method will know +// It is not possible to achieve this postcondition in a lemma, because lemma +// contexts are not allowed to allocate state. Callers of this lemma will know // that the postcondition is tantamount to 'false'. -ghost method TwoState0(y: int) +lemma TwoState0(y: int) ensures exists o: TwoState_C {:nowarn} :: allocated(o) && fresh(o) method TwoState_Main0() { diff --git a/Test/allocated1/dafny0/Refinement.dfy.expect b/Test/allocated1/dafny0/Refinement.dfy.expect index 0cf610c5778..db9f7174b1a 100644 --- a/Test/allocated1/dafny0/Refinement.dfy.expect +++ b/Test/allocated1/dafny0/Refinement.dfy.expect @@ -1,3 +1,4 @@ +Refinement.dfy(233,4): Warning: note, this loop has no body (loop frame: i) Refinement.dfy(15,4): Error: A postcondition might not hold on this return path. Refinement.dfy(14,16): Related location: This is the postcondition that might not hold. Refinement.dfy[B](15,4): Error: A postcondition might not hold on this return path. @@ -14,5 +15,13 @@ Refinement.dfy(204,6): Error: assertion violation Refinement.dfy[IncorrectConcrete](131,18): Related location Refinement.dfy(209,6): Error: assertion violation Refinement.dfy[IncorrectConcrete](137,23): Related location +Refinement.dfy(253,6): Error: A postcondition might not hold on this return path. +Refinement.dfy[Modify1](223,19): Related location: This is the postcondition that might not hold. +Refinement.dfy(261,6): Error: A postcondition might not hold on this return path. +Refinement.dfy[Modify1](230,14): Related location: This is the postcondition that might not hold. +Refinement.dfy(268,4): Error: A postcondition might not hold on this return path. +Refinement.dfy[Modify1](238,14): Related location: This is the postcondition that might not hold. +Refinement.dfy(274,6): Error: A postcondition might not hold on this return path. +Refinement.dfy[Modify1](244,14): Related location: This is the postcondition that might not hold. -Dafny program verifier finished with 23 verified, 9 errors +Dafny program verifier finished with 28 verified, 13 errors diff --git a/Test/allocated1/dafny0/SmallTests.dfy b/Test/allocated1/dafny0/SmallTests.dfy index 4462190af86..96813a4eed8 100644 --- a/Test/allocated1/dafny0/SmallTests.dfy +++ b/Test/allocated1/dafny0/SmallTests.dfy @@ -751,10 +751,10 @@ class GT { { if (*) { P0(); - assert forall x: GT {:nowarn} :: allocated(x) ==> old(allocated(x)); // error: method P2 may have allocated stuff + assert forall x: GT {:nowarn} :: allocated(x) ==> old(allocated(x)); // error: method P0 may have allocated stuff } else { P1(); - assert forall x: GT {:nowarn} :: allocated(x) ==> old(allocated(x)); // fine, because the ghost method does not allocate anything + assert forall x: GT {:nowarn} :: allocated(x) ==> old(allocated(x)); // error: ghost method P1 may have allocated stuff } } } diff --git a/Test/allocated1/dafny0/SmallTests.dfy.expect b/Test/allocated1/dafny0/SmallTests.dfy.expect index bc4cc56ece4..90153c45e29 100644 --- a/Test/allocated1/dafny0/SmallTests.dfy.expect +++ b/Test/allocated1/dafny0/SmallTests.dfy.expect @@ -30,6 +30,7 @@ SmallTests.dfy(418,11): Error: assertion violation SmallTests.dfy(428,5): Error: cannot prove termination; try supplying a decreases clause SmallTests.dfy(733,13): Error: assertion violation SmallTests.dfy(754,13): Error: assertion violation +SmallTests.dfy(757,13): Error: assertion violation SmallTests.dfy(338,2): Error: A postcondition might not hold on this return path. SmallTests.dfy(332,10): Related location: This is the postcondition that might not hold. SmallTests.dfy(332,40): Related location @@ -49,7 +50,7 @@ SmallTests.dfy(701,9): Error: cannot establish the existence of LHS values that SmallTests.dfy(703,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate SmallTests.dfy(716,8): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Dafny program verifier finished with 51 verified, 45 errors +Dafny program verifier finished with 51 verified, 46 errors SmallTests.dfy.tmp.dprint.dfy(450,4): Warning: /!\ No trigger covering all quantified variables found. Dafny program verifier did not attempt verification diff --git a/Test/cloudmake/CloudMake-CachedBuilds.dfy b/Test/cloudmake/CloudMake-CachedBuilds.dfy index 197c7410b32..365ca45a952 100644 --- a/Test/cloudmake/CloudMake-CachedBuilds.dfy +++ b/Test/cloudmake/CloudMake-CachedBuilds.dfy @@ -1300,7 +1300,7 @@ abstract module M0 { { reveal Combine(); } - ghost method Combine_Representative(p: Path, sts: set, useCache: bool) returns (stRepr: State) + lemma Combine_Representative(p: Path, sts: set, useCache: bool) returns (stRepr: State) requires sts != {} && p in DomSt(Combine(sts, useCache)); ensures stRepr in sts && p in DomSt(stRepr) && GetSt(p, stRepr) == GetSt(p, Combine(sts, useCache)); { diff --git a/Test/comp/Class.dfy b/Test/comp/Class.dfy index 644de2bb66b..45c87246953 100644 --- a/Test/comp/Class.dfy +++ b/Test/comp/Class.dfy @@ -1,7 +1,8 @@ -// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:cs "%s" > "%t" -// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:js "%s" >> "%t" -// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:go "%s" >> "%t" -// RUN: %dafny /compile:3 /spillTargetCode:2 /compileTarget:java "%s" >> "%t" +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:cs "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:js "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:go "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /spillTargetCode:2 /compileTarget:java "%s" >> "%t" // RUN: %diff "%s.expect" "%t" class MyClass { @@ -129,6 +130,8 @@ method Main() { CallEm(c, t, i); DependentStaticConsts.Test(); NewtypeWithMethods.Test(); + TestGhostables(70); + TestInitializationMethods(); } module Module1 { @@ -178,3 +181,64 @@ newtype NewtypeWithMethods = x | 0 <= x < 42 { print a, " ", b, " ", a.double(), " ", q, " ", r, "\n"; } } + +class Ghostable { + var data: int + constructor A(x: int) { + data := x; + } + ghost constructor (x: int) { + data := x; + } +} + +class ConstructorLessGhostable { + var data: int +} + +function GInit(index: nat): int { + index - 7 +} + +method TestGhostables(ghost n: nat) { + print "TestGhostables\n"; + + var a0 := new Ghostable.A(10); + var a1 := new Ghostable(n); // note, a1 is ghost + + var b0 := new ConstructorLessGhostable; + ghost var b1 := new ConstructorLessGhostable; // note, b1 is ghost + + var c0 := new int[10]; + ghost var c1 := new int[n]; // note, c1 is ghost + c0 := new int[10](x => x + 2); + c1 := new int[n](x => x + n); + c1 := new int[100](GInit); +} + +// --------------------------------------------------- + +// Additional tests cases for order of evaluation of initialization-method parameters. + +class HasInitializationMethod { + var data: int + + method Init(x: int) + requires x == 15 + modifies this + ensures data == x + 1 + { + print "Init called with x=", x, "\n"; + data := x + 1; + } +} + +method TestInitializationMethods() { + var c := new HasInitializationMethod; + c.data := 15; + print c.data, "\n"; // 15 + + c := new HasInitializationMethod.Init(c.data); // should pass in c.data, not (new HasInitializationMethod).data + + print c.data, "\n"; // 16 +} diff --git a/Test/comp/Class.dfy.expect b/Test/comp/Class.dfy.expect index a75cb43552a..38f9e355a4d 100644 --- a/Test/comp/Class.dfy.expect +++ b/Test/comp/Class.dfy.expect @@ -1,5 +1,7 @@ -Dafny program verifier finished with 13 verified, 0 errors +Dafny program verifier finished with 16 verified, 0 errors + +Dafny program verifier did not attempt verification true true false 103 103 103 106 106 106 203 17 0 18 8 9 69 70 @@ -11,8 +13,12 @@ true true false 70 hi later 21 4 42 5 1 +TestGhostables +15 +Init called with x=15 +16 -Dafny program verifier finished with 13 verified, 0 errors +Dafny program verifier did not attempt verification true true false 103 103 103 106 106 106 203 17 0 18 8 9 69 70 @@ -24,8 +30,12 @@ true true false 70 hi later 21 4 42 5 1 +TestGhostables +15 +Init called with x=15 +16 -Dafny program verifier finished with 13 verified, 0 errors +Dafny program verifier did not attempt verification true true false 103 103 103 106 106 106 203 17 0 18 8 9 69 70 @@ -37,8 +47,12 @@ true true false 70 hi later 21 4 42 5 1 +TestGhostables +15 +Init called with x=15 +16 -Dafny program verifier finished with 13 verified, 0 errors +Dafny program verifier did not attempt verification true true false 103 103 103 106 106 106 203 17 0 18 8 9 69 70 @@ -50,3 +64,7 @@ true true false 70 hi later 21 4 42 5 1 +TestGhostables +15 +Init called with x=15 +16 diff --git a/Test/comp/compile1quiet/CompileRunQuietly.dfy b/Test/comp/compile1quiet/CompileRunQuietly.dfy index 95b489e25fd..64f50d91e71 100644 --- a/Test/comp/compile1quiet/CompileRunQuietly.dfy +++ b/Test/comp/compile1quiet/CompileRunQuietly.dfy @@ -1,5 +1,5 @@ // RUN: %dafny /compileTarget:cs "%s" > "%t" -// RUN: dotnet CompileRunQuietly.dll >> "%t" +// RUN: dotnet %S/CompileRunQuietly.dll >> "%t" // RUN: %dafny /compileTarget:js "%s" >> "%t" // RUN: node %S/CompileRunQuietly.js >> "%t" @@ -11,7 +11,7 @@ // RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileRunQuietly-java CompileRunQuietly >> "%t" // RUN: %dafny /compileTarget:cpp "%s" >> "%t" -// RUN: CompileRunQuietly.exe >> "%t" +// RUN: %S/CompileRunQuietly.exe >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/comp/compile1verbose/CompileAndThenRun.dfy b/Test/comp/compile1verbose/CompileAndThenRun.dfy index 0db655f9129..49ea197348b 100644 --- a/Test/comp/compile1verbose/CompileAndThenRun.dfy +++ b/Test/comp/compile1verbose/CompileAndThenRun.dfy @@ -1,5 +1,5 @@ // RUN: %dafny /compileVerbose:1 /compileTarget:cs "%s" > "%t" -// RUN: dotnet CompileAndThenRun.dll >> "%t" +// RUN: dotnet %S/CompileAndThenRun.dll >> "%t" // RUN: %dafny /compileVerbose:1 /compileTarget:js "%s" >> "%t" // RUN: node %S/CompileAndThenRun.js >> "%t" @@ -11,7 +11,7 @@ // RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/CompileAndThenRun-java CompileAndThenRun >> "%t" // RUN: %dafny /compileVerbose:1 /compileTarget:cpp "%s" >> "%t" -// RUN: CompileAndThenRun.exe >> "%t" +// RUN: %S/CompileAndThenRun.exe >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/comp/manualcompile/ManualCompile.dfy b/Test/comp/manualcompile/ManualCompile.dfy index 68255ca6431..269e7a4743d 100644 --- a/Test/comp/manualcompile/ManualCompile.dfy +++ b/Test/comp/manualcompile/ManualCompile.dfy @@ -6,15 +6,15 @@ // RUN: node %S/ManualCompile.js >> "%t" // RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:2 /compileTarget:go "%s" >> "%t" -// RUN: env GOPATH=%S/ManualCompile-go go run %S/ManualCompile-go/src/ManualCompile.go >> "%t" +// RUN: env GO111MODULE=auto GOPATH=%S/ManualCompile-go go run %S/ManualCompile-go/src/ManualCompile.go >> "%t" // RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:2 /compileTarget:java "%s" >> "%t" // RUN: javac -cp %binaryDir/DafnyRuntime.jar:%S/ManualCompile-java %S/ManualCompile-java/ManualCompile.java %S/ManualCompile-java/*/*.java // RUN: java -cp %binaryDir/DafnyRuntime.jar:%S/ManualCompile-java ManualCompile >> "%t" // RUN: %dafny /compileVerbose:1 /compile:0 /spillTargetCode:2 /compileTarget:cpp "%s" >> "%t" -// RUN: g++ -g -Wall -Wextra -Wpedantic -Wno-unused-variable -std=c++17 -I %binaryDir -o ManualCompile.exe %S/ManualCompile.cpp -// RUN: ManualCompile.exe >> "%t" +// RUN: g++ -g -Wall -Wextra -Wpedantic -Wno-unused-variable -std=c++17 -I %binaryDir -o %S/ManualCompile.exe %S/ManualCompile.cpp +// RUN: %S/ManualCompile.exe >> "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/ArrayElementInitResolution.dfy b/Test/dafny0/ArrayElementInitResolution.dfy index 61be60e0532..f2f400f33a7 100644 --- a/Test/dafny0/ArrayElementInitResolution.dfy +++ b/Test/dafny0/ArrayElementInitResolution.dfy @@ -60,8 +60,8 @@ module AM { module BM { function GhostF(x: int): char { 'D' } - method M(n: nat) { - var a := new char[n](GhostF); // error: use of ghost function not allowed here + method M(n: nat) returns (a: array) { + a := new char[n](GhostF); // error: use of ghost function not allowed here if 5 < n { assert a[5] == 'D'; } @@ -82,8 +82,8 @@ module CM { module DM { method Ghost(ghost g: int) - { - var a := new int[4] [100, 75, g, 25]; // error: "g" is ghost + { var a; + a := new int[4] [100, 75, g, 25]; // error: "g" is ghost } } diff --git a/Test/dafny0/ArrayElementInitResolution.dfy.expect b/Test/dafny0/ArrayElementInitResolution.dfy.expect index d0ae1273870..bc125b9cc60 100644 --- a/Test/dafny0/ArrayElementInitResolution.dfy.expect +++ b/Test/dafny0/ArrayElementInitResolution.dfy.expect @@ -2,9 +2,9 @@ ArrayElementInitResolution.dfy(16,26): Error: array-allocation initialization ex ArrayElementInitResolution.dfy(23,23): Error: array-allocation initialization expression expected to have type 'nat ~> D' (instead got 'D') (perhaps write '_ =>' in front of the expression you gave in order to make it an arrow type) ArrayElementInitResolution.dfy(38,33): Error: array-allocation initialization expression expected to have type '(nat, nat, nat) ~> char' (instead got 'int -> char') ArrayElementInitResolution.dfy(55,31): Error: array-allocation initialization expression expected to have type '(nat, nat, nat, nat, nat) ~> D' (instead got 'D') (perhaps write '(_, _, _, _, _) =>' in front of the expression you gave in order to make it an arrow type) -ArrayElementInitResolution.dfy(64,25): Error: ghost fields are allowed only in specification contexts +ArrayElementInitResolution.dfy(64,21): Error: ghost fields are allowed only in specification contexts ArrayElementInitResolution.dfy(79,36): Error: initial value must be assignable to array's elements (expected 'int32', got 'int') -ArrayElementInitResolution.dfy(86,34): Error: ghost variables are allowed only in specification contexts +ArrayElementInitResolution.dfy(86,30): Error: ghost variables are allowed only in specification contexts ArrayElementInitResolution.dfy(99,29): Error: initial value must be assignable to array's elements (expected 'bool', got 'char') ArrayElementInitResolution.dfy(116,28): Error: initial value must be assignable to array's elements (expected 'bool', got 'char') ArrayElementInitResolution.dfy(126,8): Error: the type of this variable is underspecified diff --git a/Test/dafny0/BigOrdinals.dfy b/Test/dafny0/BigOrdinals.dfy index b743cf72bc0..0d33fea89a1 100644 --- a/Test/dafny0/BigOrdinals.dfy +++ b/Test/dafny0/BigOrdinals.dfy @@ -120,7 +120,7 @@ method Constraints() returns (x: ORDINAL, y: ConstrainedOrdinal) y := 16; // error: may not assign 16 to a ConstrainedOrdinal } -ghost method Members(a: ORDINAL, n: nat) +lemma Members(a: ORDINAL, n: nat) { var b: ORDINAL := 25; assert b.IsNat; diff --git a/Test/dafny0/BindingGuardsResolution.dfy.expect b/Test/dafny0/BindingGuardsResolution.dfy.expect index 694b07eabd6..0fb941c9d3d 100644 --- a/Test/dafny0/BindingGuardsResolution.dfy.expect +++ b/Test/dafny0/BindingGuardsResolution.dfy.expect @@ -159,10 +159,10 @@ BindingGuardsResolution.dfy(19,6): Error: LHS of assignment must denote a mutabl BindingGuardsResolution.dfy(39,8): Error: Duplicate local-variable name: x BindingGuardsResolution.dfy(84,8): Error: LHS of assignment must denote a mutable variable BindingGuardsResolution.dfy(109,7): Error: type of bound variable 'x' could not be determined; please specify the type explicitly -BindingGuardsResolution.dfy(130,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -BindingGuardsResolution.dfy(132,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -BindingGuardsResolution.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -BindingGuardsResolution.dfy(142,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -BindingGuardsResolution.dfy(146,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +BindingGuardsResolution.dfy(130,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +BindingGuardsResolution.dfy(132,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +BindingGuardsResolution.dfy(140,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +BindingGuardsResolution.dfy(142,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +BindingGuardsResolution.dfy(146,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression BindingGuardsResolution.dfy(149,37): Error: predicate calls are allowed only in specification contexts (consider declaring the predicate a 'predicate method') 11 resolution/type errors detected in BindingGuardsResolution.dfy diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy index 7bfbb4771a9..1dbe00d2a02 100644 --- a/Test/dafny0/CoPrefix.dfy +++ b/Test/dafny0/CoPrefix.dfy @@ -41,7 +41,7 @@ greatest lemma {:induction false} Theorem0() } } -ghost method Theorem0_Manual() +lemma Theorem0_Manual() ensures atmost(zeros(), ones()); { forall k: ORDINAL { @@ -78,7 +78,7 @@ greatest lemma {:induction false} Theorem0_TerminationFailure_DefaultDecreases(y Theorem0_TerminationFailure_DefaultDecreases#[_k-1](y); } -ghost method {:induction true} Theorem0_Lemma(k: ORDINAL) +lemma {:induction true} Theorem0_Lemma(k: ORDINAL) ensures atmost#[k](zeros(), ones()); { } diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy index 7134b405ebf..614c8aa1ebd 100644 --- a/Test/dafny0/CoResolution.dfy +++ b/Test/dafny0/CoResolution.dfy @@ -98,8 +98,8 @@ module Mojul1 { Z(); W(); // error: not allowed to make co-recursive call to non-greatest lemma } - ghost method Z() { } - ghost method W() { M(); } + lemma Z() { } + lemma W() { M(); } greatest lemma G() { H(); } greatest lemma H() { G#[10](); } // fine for greatest lemma/prefix-lemma diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect index 97feb855df6..0502672291d 100644 --- a/Test/dafny0/CoResolution.dfy.expect +++ b/Test/dafny0/CoResolution.dfy.expect @@ -2,7 +2,7 @@ CoResolution.dfy(18,11): Error: member 'Undeclared#' does not exist in class 'Te CoResolution.dfy(19,6): Error: unresolved identifier: Undeclared# CoResolution.dfy(22,9): Error: unresolved identifier: _k CoResolution.dfy(41,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>) -CoResolution.dfy(52,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +CoResolution.dfy(52,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression CoResolution.dfy(76,33): Error: a greatest predicate is not allowed to declare any ensures clause CoResolution.dfy(86,27): Error: a recursive call from a greatest predicate can go only to other greatest predicates CoResolution.dfy(90,27): Error: a recursive call from a greatest predicate can go only to other greatest predicates diff --git a/Test/dafny0/DefaultParameters.dfy b/Test/dafny0/DefaultParameters.dfy index 0270629b3bd..7bdaead5c68 100644 --- a/Test/dafny0/DefaultParameters.dfy +++ b/Test/dafny0/DefaultParameters.dfy @@ -416,7 +416,7 @@ module TerminationCheck { datatype R = R(x: int := X(); 3) // error: termination violation function F(x: int := F(5)): int // error: termination violation function G(x: int := X(); 3): int // error: termination violation - ghost method M(x: int := X(); 3) // error: termination violation + lemma M(x: int := X(); 3) // error: termination violation method Caller() { // No additional errors are reported at the use sites @@ -505,7 +505,7 @@ module StmtExprCallPreconditionRegression { } module IteratorFrameRegression { - ghost method X() + lemma X() // The following once caused malformed Boogie, because the $_Frame variable had not been declared. iterator Iter() requires (X(); 3) == 3 diff --git a/Test/dafny0/DefaultParameters.dfy.expect b/Test/dafny0/DefaultParameters.dfy.expect index 78a22c256e3..977b203bbca 100644 --- a/Test/dafny0/DefaultParameters.dfy.expect +++ b/Test/dafny0/DefaultParameters.dfy.expect @@ -60,7 +60,7 @@ DefaultParameters.dfy(387,29): Error: value does not satisfy the subset constrai DefaultParameters.dfy(416,28): Error: default-value expression is not allowed to involve recursive or mutually recursive calls DefaultParameters.dfy(417,23): Error: default-value expression is not allowed to involve recursive or mutually recursive calls DefaultParameters.dfy(418,24): Error: cannot prove termination; try supplying a decreases clause -DefaultParameters.dfy(419,28): Error: cannot prove termination; try supplying a decreases clause +DefaultParameters.dfy(419,21): Error: cannot prove termination; try supplying a decreases clause DefaultParameters.dfy(438,27): Error: default-value expression is not allowed to involve recursive or mutually recursive calls DefaultParameters.dfy(443,28): Error: default-value expression is not allowed to involve recursive or mutually recursive calls DefaultParameters.dfy(447,5): Error: cannot prove termination; try supplying a decreases clause diff --git a/Test/dafny0/DefiniteAssignment.dfy b/Test/dafny0/DefiniteAssignment.dfy index 856640c4af8..d06dca218d6 100644 --- a/Test/dafny0/DefiniteAssignment.dfy +++ b/Test/dafny0/DefiniteAssignment.dfy @@ -413,3 +413,42 @@ module Regression { method N() returns (e: E) { } } + +module AdditionalTests { + type GGG(00) + + method DefiniteAssignmentLocal0() returns (r: GGG) { + var g: GGG; + r := g; // error: g is subject to definite-assignment rules and cannot be used unless first initialized + } + + method DefiniteAssignmentLocal1(a: bool, ghost b: bool) returns (ghost r: GGG, r': GGG) { + var g: GGG; + if a { + r := g; // error: g is subject to definite-assignment rules and cannot be used unless first initialized (despite being assigned to a ghost) + r' := g; // this is an error, but it is masked by the error on the previous line + } else { + if b { + var h: GGG; + h := g; // error: g is subject to definite-assignment rules and cannot be used unless first initialized (despite being assigned to a ghost) + } + } + } // error: r' may not have been assigned + + ghost method DefiniteAssignmentLocal2() returns (r: GGG) { + var g: GGG; // no initialization needed, since we're in a ghost context + r := g; + } + + method DefiniteAssignmentOut0() returns (r: GGG) { + } // error: g is subject to definite-assignment rules and cannot be used unless first initialized + + method DefiniteAssignmentOut1() returns (ghost r: GGG) { + } // no initialization needed, since the out-parameter is ghost + + ghost method DefiniteAssignmentOut2() returns (r: GGG) { + } // no initialization needed, since we're in a ghost context + + lemma DefiniteAssignmentOut3() returns (r: GGG) { + } // no initialization needed, since we're in a ghost context +} diff --git a/Test/dafny0/DefiniteAssignment.dfy.expect b/Test/dafny0/DefiniteAssignment.dfy.expect index f7c42512123..d96820ceecc 100644 --- a/Test/dafny0/DefiniteAssignment.dfy.expect +++ b/Test/dafny0/DefiniteAssignment.dfy.expect @@ -9,6 +9,11 @@ DefiniteAssignment.dfy(370,11): Error: field 'y', which is subject to definite-a DefiniteAssignment.dfy(377,6): Error: field 'y', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body DefiniteAssignment.dfy(382,4): Error: field 'y', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body DefiniteAssignment.dfy(387,4): Error: field 'x', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body +DefiniteAssignment.dfy(422,9): Error: variable 'g', which is subject to definite-assignment rules, might be used before it has been assigned +DefiniteAssignment.dfy(428,11): Error: variable 'g', which is subject to definite-assignment rules, might be used before it has been assigned +DefiniteAssignment.dfy(433,13): Error: variable 'g', which is subject to definite-assignment rules, might be used before it has been assigned +DefiniteAssignment.dfy(436,2): Error: out-parameter 'r'', which is subject to definite-assignment rules, might not have been defined at this return point +DefiniteAssignment.dfy(444,2): Error: out-parameter 'r', which is subject to definite-assignment rules, might not have been defined at this return point DefiniteAssignment.dfy(11,9): Error: field 'y', which is subject to definite-assignment rules, might be used before it has been assigned DefiniteAssignment.dfy(13,4): Error: field 'oxA', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body DefiniteAssignment.dfy(13,4): Error: field 'oxB', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body @@ -40,4 +45,4 @@ DefiniteAssignment.dfy(143,8): Error: variable 'w', which is subject to definite DefiniteAssignment.dfy(237,12): Error: variable 'a', which is subject to definite-assignment rules, might be used before it has been assigned DefiniteAssignment.dfy(238,12): Error: variable 'b', which is subject to definite-assignment rules, might be used before it has been assigned -Dafny program verifier finished with 12 verified, 41 errors +Dafny program verifier finished with 12 verified, 46 errors diff --git a/Test/dafny0/ForLoops-Resolution.dfy.expect b/Test/dafny0/ForLoops-Resolution.dfy.expect index 90bd049f9e3..1d01929fcdd 100644 --- a/Test/dafny0/ForLoops-Resolution.dfy.expect +++ b/Test/dafny0/ForLoops-Resolution.dfy.expect @@ -25,15 +25,14 @@ ForLoops-Resolution.dfy(321,18): Error: break label is undefined or not in scope ForLoops-Resolution.dfy(332,11): Error: unresolved identifier: i ForLoops-Resolution.dfy(353,24): Error: break label is undefined or not in scope: A ForLoops-Resolution.dfy(355,18): Error: trying to break out of more loop levels than there are enclosing loops -ForLoops-Resolution.dfy(390,10): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ForLoops-Resolution.dfy(412,10): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ForLoops-Resolution.dfy(434,10): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ForLoops-Resolution.dfy(446,10): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ForLoops-Resolution.dfy(457,10): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ForLoops-Resolution.dfy(479,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ForLoops-Resolution.dfy(390,10): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ForLoops-Resolution.dfy(412,10): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ForLoops-Resolution.dfy(434,10): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ForLoops-Resolution.dfy(446,10): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ForLoops-Resolution.dfy(457,10): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ForLoops-Resolution.dfy(479,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression ForLoops-Resolution.dfy(490,16): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) ForLoops-Resolution.dfy(503,6): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) -ForLoops-Resolution.dfy(490,16): Error: return statement is not allowed inside a hint ForLoops-Resolution.dfy(510,4): Error: a ghost loop must be terminating; make the end-expression specific or add a 'decreases' clause ForLoops-Resolution.dfy(517,4): Error: 'decreases *' is not allowed on ghost loops -35 resolution/type errors detected in ForLoops-Resolution.dfy +34 resolution/type errors detected in ForLoops-Resolution.dfy diff --git a/Test/dafny0/GhostAllocations-Resolution.dfy b/Test/dafny0/GhostAllocations-Resolution.dfy new file mode 100644 index 00000000000..ededb652d61 --- /dev/null +++ b/Test/dafny0/GhostAllocations-Resolution.dfy @@ -0,0 +1,699 @@ +// RUN: %dafny "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// ------- A constructor-less class can be allocated as either ghost or non-ghost + +module ConstructorLessClass { + class Cell { + var data: int + } + + method Cell0() returns (r: Cell) { + var c := new Cell; + ghost var g := new Cell; + if * { + r := c; + } else { + r := g; // error: cannot assign ghost to non-ghost + } + } +} + +// ------- A class with a constructor is ghost/non-ghost depending on the constructor called + +module Dual { + class Either { + constructor A(x: int) { + } + ghost constructor B(x: int) { + } + } + + method Either0() returns (r: Either) { + var e := new Either.A(5); + var g := new Either.B(5); // g is auto-ghost + + if * { + r := e; + } else { + r := g; // error: cannot assign ghost to non-ghost + } + } + + method Either1(n: nat, ghost n': nat) { + var e; + ghost var g; + e := new Either.A(n); + e := new Either.A(n'); // error: cannot pass ghost to non-ghost + g := new Either.B(n); + g := new Either.B(n'); + } + + method Either2(n: nat) { + var e; + ghost var g; + e := new Either.B(n); // error: ghost constructor can only be called in a ghost context + g := new Either.A(n); // error: non-ghost constructor cannot be called in a ghost context + } + + ghost method Either3(n: nat) { + var e; + e := new Either.B(n); // fine, since Either3 is a ghost context + e := new Either.A(n); // error: non-ghost constructor cannot be called in a ghost context + } + + class Cell { + var x: Either + ghost var y: Either + } + + method AlternativeLhss() { + var a := new object[10]; + a[0] := new Either.B(2); // error: cannot assign ghost to non-ghost + + var m := new object[10, 10]; + m[5, 3] := new Either.B(2); // error: cannot assign ghost to non-ghost + + var c := new Cell; + c.x := new Either.B(2); // error: cannot assign ghost to non-ghost + c.y := new Either.B(2); + } +} + +// ------- An array can be allocated as either ghost either non-ghost + +module Arrays { + method Array0(n: nat, ghost n': nat) { + var a; + ghost var g; + a := new int[n]; + a := new int[n']; // error: cannot use ghost in this context + g := new int[n]; + g := new int[n']; + } + + method Array1(f: int -> real, ghost f': int -> real) { + var a; + ghost var g; + a := new real[10](f); + a := new real[10](f'); // error: cannot use ghost in this context + g := new real[10](f); + g := new real[10](f'); + } + + method Array2(n: nat, ghost n': nat, f: int -> real, ghost f': int -> real) returns (r: object) { + // In the next line, b and d are auto-ghost + var a, b, c, d := new real[n], new real[n'], new real[10](f), new real[10](f'); + if + case true => + r := a; + case true => + r := b; // error: cannot assign ghost to non-ghost + case true => + r := c; + case true => + r := d; // error: cannot assign ghost to non-ghost + } + + method Array3(n: nat, ghost n': nat, f: int -> real, ghost f': int -> real) returns (r: object) { + // In the next line, b, c, and d are auto-ghost + var a, b, c, d := new real[n](f), new real[n'](f), new real[n](f'), new real[n'](f'); + if + case true => + r := a; + case true => + r := b; // error: cannot assign ghost to non-ghost + case true => + r := c; // error: cannot assign ghost to non-ghost + case true => + r := d; // error: cannot assign ghost to non-ghost + } + + method Array4() returns (ghost r: array) { + ghost var a := new int[20]; + ghost var b := new int[] [2, 3, 5, 7, var k := 11; k, ghost var g := 13; g]; + ghost var c := new int[100](i => 2 * i); + ghost var d := new int[] [2, 3, b[2], 7, 11, 13]; + r := a; + r := b; + r := c; + r := d; + } + + method Array5(ghost n: int) returns (ghost r: array) + requires n == 20 + { + // a, b, c, d are auto-ghost + var a := new int[n]; + var b := new int[] [2, 3, 5, 7, var k := 11; k, ghost var g := 13; g]; + var c := new int[100](Double); + var d := new int[] [2, 3, b[2], 7, 11, 13]; + r := a; + r := b; + r := c; + r := d; + } + + function Double(i: int): int { 2 * i } +} + +// ------- ghost constructors + +module GhostConstructors0 { + class G { + const c: int + ghost const d: int + const e: int := 5 + ghost const f: int := 6 + + ghost constructor (x: int) { + e := 100; // error: cannot assign to const field that has a RHS + f := 100; // error: cannot assign to const field that has a RHS + new; + c := 2; // error: cannot assign to const after "new;" + d := 3; // error: cannot assign to const after "new;" + } + } +} + +module GhostConstructors1 { + class Cell { + var data: int + } + + class G { + var a: int + ghost var b: int + const c: int + ghost const d: int + + ghost constructor (x: int) { + b, d := x, x + a; + a := 2; + c := 3; + if x < 17 { + Compiled(); // error: cannot call non-ghost from a ghost context + Ghost(); + Lemma(); + } + new; + a := 0; // error: cannot assign to non-ghost after "new;" in ghost constructor + b := 1; + Compiled(); // error: cannot call non-ghost from a ghost context + Ghost(); + Lemma(); + } + + static method Compiled() + static ghost method Ghost() + static lemma Lemma() + } + + type GGG(0) + + class GhostableAutoInit { + var g: GGG + ghost var h: GGG + + constructor A(g: GGG) { + this.g := g; + } + + constructor B() { // definite-assignment rules are not satisfied, but that's check during verification (see GhostAllocations.dfy) + } + + ghost constructor C(g: GGG) { + this.g := g; + } + + ghost constructor D() { // in a ghost context, we only need to know that g's type is nonempty (same as for h all along) + } + + ghost constructor PostNew(c: GhostableAutoInit) + modifies c + { + g := h; // fine before "new;" + c.g := h; // error: cannot assign to non-ghost field of non-this + print "hello\n"; // error: cannot use print in ghost context + new; + g := h; // error: after "new;", rules are as normal, so cannot assign to non-ghost field in this ghost context + print "bye\n"; // error: cannot use print in ghost context + } + + ghost constructor CalcInInitializationPhase() { + var c0 := new Cell; // fine here + var g0 := new G(5); // fine here + calc { + 5; + == { var c1 := new Cell; // error: cannot allocate inside calc hint + var g1 := new G(5); // error: cannot allocate inside calc hint + } + 2 + 3; + } + assert true by { + var c2 := new Cell; // error: cannot allocate inside assert-by + var g2 := new G(5); // error: cannot allocate inside assert-by + } + new; + } + } +} + +module GhostInitializingMethods { + class G { + var data: int + ghost var gata: int + + method CompiledInit(x: int) { + gata := x; + data := x; + } + + ghost method GhostInit(x: int) { + gata := x; + data := x; // error: cannot assign to a non-ghost field in a ghost context + } + } + + method M() returns (g: G) { + var a := new G.CompiledInit(5); + var b := new G.GhostInit(5); // b is auto-ghost + + if * { + g := a; + } else { + g := b; // error: cannot assign ghost to non-ghost + } + } +} + +// ------- lemmas are not allowed to allocate any state + +module Lemmas { + class Cell { + var data: int + } + + class Point { + constructor XY(x: real, y: real) + ghost constructor Polar(theta: real, mag: real) + } + + lemma A() { + var o := new object; // error: lemma is not allowed to allocate state + var c := new Cell; // error: lemma is not allowed to allocate state + } + + lemma B() { + var pt0 := new Point.XY(1.0, 0.0); // error: cannot call non-ghost constructor + var pt1 := new Point.Polar(0.0, 1.0); // error: ... or a ghost constructor, for that matter + } + + lemma C() { + var a := new int[25]; // error: lemma is not allowed to allocate state + var m := new real[640, 480]; // error: lemma is not allowed to allocate state + } + + twostate lemma D() { + var c := new Cell; // error: lemma is not allowed to allocate state + } + + greatest lemma E() { + var c := new Cell; // error: lemma is not allowed to allocate state + } +} + +// ------- ghost methods cannot be called from lemma/proof contexts + +module GhostMethodVersusLemma { + class Marker { } + class Cell { + var data: int + ghost var m: Marker? + } + + ghost method G(m: Marker) + ensures exists c: Cell :: allocated(c) && fresh(c) && c.m == m + { + var c := new Cell; + c.m := m; + } + + method M0() { + var m := new Marker; + forall c: Cell | allocated(c) + ensures c.m != m + { + assert old(allocated(c)); + } + var x := (G(m); 3); // error: not allowed to call ghost method in an expression + assert exists c: Cell :: allocated(c) && c.m == m; + assert false; + } + + method M1(ghost b: bool) { + var m := new Marker; + G(m); + if b { + G(m); + } + assert b by { + G(m); // error: not allowed to call ghost method from a hint + } + assert false; + } + + lemma GG(m: Marker) + ensures exists c: Cell :: allocated(c) && fresh(c) && c.m == m + { + G(m); // error: not allowed to call ghost method from a lemma + } + + method M2() { + var m := new Marker; + calc { + 5; + == { G(m); } // error: not allowed to call ghost method from a hint + 7 - 2; + } + } + + lemma M3(m: Marker) { + calc { + 5; + == { G(m); } // error: not allowed to call ghost method from a lemma + 7 - 2; + } + } + + lemma Modify0() { + var i := 0; + while i < 10 + modifies {} // error: not allowed modifies clause in lemma context + { + i := i + 1; + } + while + modifies {} // error: not allowed modifies clause in lemma context + { + case i < 20 => i := i + 1; + } + for j := 0 to 100 + modifies {} // error: not allowed modifies clause in lemma context + { + } + ghost var S: set := {}; + modify S; // error: not allowed modify statement in lemma context + modify S { // error: not allowed modify statement in lemma context + } + var c := new Cell; // error: 'new' not allowed in lemma context + c.m := null; // error: lemma is not allowed to make heap updates + } + ghost method Modify1() { + assert true by { + var i := 0; + while i < 10 + modifies {} // error: not allowed modifies clause in lemma context + { + i := i + 1; + } + while + modifies {} // error: not allowed modifies clause in lemma context + { + case i < 20 => i := i + 1; + } + for j := 0 to 100 + modifies {} // error: not allowed modifies clause in lemma context + { + } + ghost var S: set := {}; + modify S; // error: not allowed modify statement in lemma context + modify S { // error: not allowed modify statement in lemma context + } + var c := new Cell; // error: 'new' not allowed in lemma context + } + } + + ghost method Modify2() { + var i := 0; + while i < 10 + modifies {} + { + i := i + 1; + } + while + modifies {} + { + case i < 20 => i := i + 1; + } + for j := 0 to 100 + modifies {} + { + } + ghost var S: set := {}; + modify S; + modify S { + } + var c := new Cell; + } + + predicate IsBig(x: int) { + 100 <= x + } + + method OrdinaryMethod() + + ghost method PlainGhostMethod() + + ghost method GhostMethodWithModifies(c: Cell) + modifies c + + lemma Lemma() + + class Point { + constructor XY(x: real, y: real) + ghost constructor Polar(theta: real, mag: real) + } + + method Modify3() { + var c := new Cell; + forall i + ensures IsBig(i) ==> IsBig(i + 1) + { + var i := 0; + while i < 10 + modifies {} // error: not allowed modifies clause in lemma context + { + i := i + 1; + } + while + modifies {} // error: not allowed modifies clause in lemma context + { + case i < 20 => i := i + 1; + } + for j := 0 to 100 + modifies {} // error: not allowed modifies clause in lemma context + { + } + ghost var S: set := {}; + modify S; // error: not allowed modify statement in lemma context + modify S { // error: not allowed modify statement in lemma context + } + + OrdinaryMethod(); // error: cannot call non-ghost method from here + PlainGhostMethod(); // error: cannot call ghost method from here + GhostMethodWithModifies(c); // error: cannot call ghost method from here + Lemma(); // fine + + var c := new Cell; // error: 'new' not allowed in lemma context + var pt0 := new Point.XY(0.0, 0.0); // error: 'new' not allowed in lemma context + ghost var pt1 := new Point.Polar(0.0, 1.0); // error: 'new' not allowed in lemma context + } + } + + method Modify4() { + var c := new Cell; + calc { + 200_000; + == { + var i := 0; + while i < 10 + modifies {} // error: not allowed modifies clause in lemma context + { + i := i + 1; + } + while + modifies {} // error: not allowed modifies clause in lemma context + { + case i < 20 => i := i + 1; + } + for j := 0 to 100 + modifies {} // error: not allowed modifies clause in lemma context + { + } + ghost var S: set := {}; + modify S; // error: not allowed modify statement in lemma context + modify S { // error: not allowed modify statement in lemma context + } + + OrdinaryMethod(); // error: cannot call non-ghost method from here + PlainGhostMethod(); // error: cannot call ghost method from here + GhostMethodWithModifies(c); // error: cannot call ghost method from here + Lemma(); // fine + + var c := new Cell; // error: 'new' not allowed in lemma context + var pt0 := new Point.XY(0.0, 0.0); // error: 'new' not allowed in lemma context + ghost var pt1 := new Point.Polar(0.0, 1.0); // error: 'new' not allowed in lemma context + } + 200_000; + } + } + + method Modify5(n: nat, ghost b: bool) + requires n != 0 + { + var a := new int[n]; + var cell := new Cell; + var S := {cell}; + + a[0] := 0; + forall i | 0 <= i < n { + a[i] := i; + } + + cell.data := 0; + forall c | c in S { + c.data := 0; + } + + cell.m := null; + forall c | c in S { + c.m := null; + } + + if b { + a[0] := 0; // error: ghost context cannot assign to non-ghost heap location + forall i | 0 <= i < n { + a[i] := i; // error: ghost context cannot assign to non-ghost heap location + } + + cell.data := 0; // error: ghost context cannot assign to non-ghost heap location + forall c | c in S { + c.data := 0; // error: ghost context cannot assign to non-ghost heap location + } + + cell.m := null; + forall c | c in S { + c.m := null; + } + } + + calc { + 2016; + < { + a[0] := 0; // error: cannot assign to heap in this lemma context + forall i | 0 <= i < n { // error: cannot do aggregate heap update in this lemma context + a[i] := i; + } + + cell.data := 0; // error: a lemma context cannot update heap locations + forall c | c in S { // error: cannot do aggregate heap update in this lemma context + c.data := 0; + } + + cell.m := null; // error: a lemma context cannot update heap locations + forall c | c in S { // error: cannot do aggregate heap update in this lemma context + c.m := null; + } + } + 2020; + } + + assert true by { + a[0] := 0; // error: cannot assign to heap in this lemma context + forall i | 0 <= i < n { // error: cannot do aggregate heap update in this lemma context + a[i] := i; + } + + cell.data := 0; // error: a lemma context cannot update heap locations + forall c | c in S { // error: cannot do aggregate heap update in this lemma context + c.data := 0; + } + + cell.m := null; // error: a lemma context cannot update heap locations + forall c | c in S { // error: cannot do aggregate heap update in this lemma context + c.m := null; + } + } + + forall j | 0 <= j < n + ensures IsBig(j) ==> IsBig(j + 1) + { + a[0] := 0; // error: cannot assign to heap in this lemma context + forall i | 0 <= i < n { // error: cannot do aggregate heap update in this lemma context + a[i] := i; + } + + cell.data := 0; // error: a lemma context cannot update heap locations + forall c | c in S { // error: cannot do aggregate heap update in this lemma context + c.data := 0; + } + + cell.m := null; // error: a lemma context cannot update heap locations + forall c | c in S { // error: cannot do aggregate heap update in this lemma context + c.m := null; + } + } + } +} + +// --------------- assignments ------------------------------ + +module Assignments { + class Cell { } + class Point { + constructor XY() + ghost constructor Polar() + } + + method M0(n: nat, init: int -> int) { + var c, pt0, pt1, arr; + c := new Cell; + pt0 := new Point.XY(); + pt1 := new Point.Polar(); // error: cannot use ghost constructor to assign compiled variable + arr := new int[n]; + arr := new int[] [n]; + arr := new int[10](init); + } + + method M1(ghost n: nat, ghost init: int -> int) { + ghost var c, pt0, pt1; + var arr; + c := new Cell; + pt0 := new Point.XY(); // error: cannot use non-ghost constructor to assign ghost variable + pt1 := new Point.Polar(); + arr := new int[n]; // error: cannot use ghost in RHS + arr := new int[] [n]; // error: cannot use ghost RHS display + arr := new int[10](init); // error: cannot use ghost RHS initializer + } + + ghost method M2(n: nat, init: int -> int) { + var c, pt0, pt1, arr; + c := new Cell; + pt0 := new Point.XY(); // error: cannot use non-ghost constructor in ghost context + pt1 := new Point.Polar(); + arr := new int[n]; + arr := new int[] [n]; + arr := new int[10](init); + } + + lemma M3(n: nat, init: int -> int) { + var c, pt0, pt1, arr; + c := new Cell; // error: cannot use 'new' in lemma context + pt0 := new Point.XY(); // error (x2): cannot use 'new' in lemma context (and cannot call constructor) + pt1 := new Point.Polar(); // error (x2): cannot use 'new' in lemma context (and cannot call constructor) + arr := new int[n]; // error: cannot use 'new' in lemma context + arr := new int[] [n]; // error: cannot use 'new' in lemma context + arr := new int[10](init); // error: cannot use 'new' in lemma context + } +} diff --git a/Test/dafny0/GhostAllocations-Resolution.dfy.expect b/Test/dafny0/GhostAllocations-Resolution.dfy.expect new file mode 100644 index 00000000000..6d3e07d1d66 --- /dev/null +++ b/Test/dafny0/GhostAllocations-Resolution.dfy.expect @@ -0,0 +1,126 @@ +GhostAllocations-Resolution.dfy(17,11): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(39,11): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(47,22): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(55,20): Error: the result of a ghost constructor can only be assigned to a ghost variable +GhostAllocations-Resolution.dfy(56,20): Error: only ghost methods can be called from this context +GhostAllocations-Resolution.dfy(62,20): Error: only ghost methods can be called from this context +GhostAllocations-Resolution.dfy(72,23): Error: the result of a ghost constructor can only be assigned to a ghost variable +GhostAllocations-Resolution.dfy(75,26): Error: the result of a ghost constructor can only be assigned to a ghost variable +GhostAllocations-Resolution.dfy(78,22): Error: the result of a ghost constructor can only be assigned to a ghost variable +GhostAllocations-Resolution.dfy(90,17): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(99,22): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(111,11): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(115,11): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(125,11): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(127,11): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(129,11): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(170,6): Error: LHS of assignment must denote a mutable field +GhostAllocations-Resolution.dfy(171,6): Error: LHS of assignment must denote a mutable field +GhostAllocations-Resolution.dfy(173,6): Error: LHS of assignment must denote a mutable field +GhostAllocations-Resolution.dfy(174,6): Error: LHS of assignment must denote a mutable field +GhostAllocations-Resolution.dfy(195,16): Error: only ghost methods can be called from this context +GhostAllocations-Resolution.dfy(200,8): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost constructor +GhostAllocations-Resolution.dfy(202,14): Error: only ghost methods can be called from this context +GhostAllocations-Resolution.dfy(236,10): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost constructor +GhostAllocations-Resolution.dfy(237,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +GhostAllocations-Resolution.dfy(239,8): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost constructor +GhostAllocations-Resolution.dfy(240,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +GhostAllocations-Resolution.dfy(248,22): Error: a hint is not allowed to use 'new' +GhostAllocations-Resolution.dfy(249,22): Error: a hint is not allowed to use 'new' +GhostAllocations-Resolution.dfy(249,22): Error: in a hint, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(254,18): Error: an assert-by body is not allowed to use 'new' +GhostAllocations-Resolution.dfy(255,18): Error: an assert-by body is not allowed to use 'new' +GhostAllocations-Resolution.dfy(255,18): Error: in an assert-by body, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(274,11): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost method +GhostAllocations-Resolution.dfy(285,11): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(303,13): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(304,13): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(308,15): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(308,25): Error: in a lemma, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(309,15): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(309,25): Error: in a lemma, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(313,13): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(314,13): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(318,13): Error: a twostate lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(322,13): Error: a greatest lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(349,15): Error: in a statement expression, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(361,7): Error: in an assert-by body, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(369,5): Error: in a lemma, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(376,11): Error: in a hint, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(384,11): Error: in a hint, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(392,15): Error: a loop in a lemma is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(397,15): Error: a loop in a lemma is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(402,15): Error: a loop in a lemma is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(406,4): Error: a modify statement is not allowed in a lemma +GhostAllocations-Resolution.dfy(407,4): Error: a modify statement is not allowed in a lemma +GhostAllocations-Resolution.dfy(409,13): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(410,6): Error: a lemma is not allowed to make heap updates +GhostAllocations-Resolution.dfy(416,17): Error: a loop in an assert-by body is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(421,17): Error: a loop in an assert-by body is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(426,17): Error: a loop in an assert-by body is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(430,6): Error: a modify statement is not allowed in an assert-by body +GhostAllocations-Resolution.dfy(431,6): Error: a modify statement is not allowed in an assert-by body +GhostAllocations-Resolution.dfy(433,15): Error: an assert-by body is not allowed to use 'new' +GhostAllocations-Resolution.dfy(485,17): Error: a loop in a forall statement is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(490,17): Error: a loop in a forall statement is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(495,17): Error: a loop in a forall statement is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(499,6): Error: a modify statement is not allowed in a forall statement +GhostAllocations-Resolution.dfy(500,6): Error: a modify statement is not allowed in a forall statement +GhostAllocations-Resolution.dfy(503,20): Error: in a forall statement, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(504,22): Error: in a forall statement, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(505,29): Error: in a forall statement, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(508,15): Error: a forall statement is not allowed to use 'new' +GhostAllocations-Resolution.dfy(509,17): Error: a forall statement is not allowed to use 'new' +GhostAllocations-Resolution.dfy(509,27): Error: in a forall statement, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(510,23): Error: a forall statement is not allowed to use 'new' +GhostAllocations-Resolution.dfy(510,33): Error: in a forall statement, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(521,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(526,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(531,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +GhostAllocations-Resolution.dfy(535,10): Error: a modify statement is not allowed in a hint +GhostAllocations-Resolution.dfy(536,10): Error: a modify statement is not allowed in a hint +GhostAllocations-Resolution.dfy(539,24): Error: in a hint, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(540,26): Error: in a hint, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(541,33): Error: in a hint, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(544,19): Error: a hint is not allowed to use 'new' +GhostAllocations-Resolution.dfy(545,21): Error: a hint is not allowed to use 'new' +GhostAllocations-Resolution.dfy(545,31): Error: in a hint, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(546,27): Error: a hint is not allowed to use 'new' +GhostAllocations-Resolution.dfy(546,37): Error: in a hint, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(575,11): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostAllocations-Resolution.dfy(577,13): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostAllocations-Resolution.dfy(580,16): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostAllocations-Resolution.dfy(582,15): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostAllocations-Resolution.dfy(594,13): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostAllocations-Resolution.dfy(595,8): Error: a hint is not allowed to perform an aggregate heap update +GhostAllocations-Resolution.dfy(599,18): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostAllocations-Resolution.dfy(600,8): Error: a hint is not allowed to perform an aggregate heap update +GhostAllocations-Resolution.dfy(604,13): Error: a hint is not allowed to make heap updates +GhostAllocations-Resolution.dfy(605,8): Error: a hint is not allowed to perform an aggregate heap update +GhostAllocations-Resolution.dfy(613,11): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostAllocations-Resolution.dfy(614,6): Error: an assert-by body is not allowed to perform an aggregate heap update +GhostAllocations-Resolution.dfy(618,16): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostAllocations-Resolution.dfy(619,6): Error: an assert-by body is not allowed to perform an aggregate heap update +GhostAllocations-Resolution.dfy(623,11): Error: an assert-by body is not allowed to make heap updates +GhostAllocations-Resolution.dfy(624,6): Error: an assert-by body is not allowed to perform an aggregate heap update +GhostAllocations-Resolution.dfy(632,11): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostAllocations-Resolution.dfy(633,6): Error: a forall statement is not allowed to perform an aggregate heap update +GhostAllocations-Resolution.dfy(637,16): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +GhostAllocations-Resolution.dfy(638,6): Error: a forall statement is not allowed to perform an aggregate heap update +GhostAllocations-Resolution.dfy(642,11): Error: a forall statement is not allowed to make heap updates +GhostAllocations-Resolution.dfy(643,6): Error: a forall statement is not allowed to perform an aggregate heap update +GhostAllocations-Resolution.dfy(663,21): Error: the result of a ghost constructor can only be assigned to a ghost variable +GhostAllocations-Resolution.dfy(673,21): Error: only ghost methods can be called from this context +GhostAllocations-Resolution.dfy(675,19): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(676,22): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(677,23): Error: ghost variables are allowed only in specification contexts +GhostAllocations-Resolution.dfy(683,21): Error: only ghost methods can be called from this context +GhostAllocations-Resolution.dfy(692,9): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(693,11): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(693,21): Error: in a lemma, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(694,11): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(694,21): Error: in a lemma, calls are allowed only to lemmas +GhostAllocations-Resolution.dfy(695,11): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(696,11): Error: a lemma is not allowed to use 'new' +GhostAllocations-Resolution.dfy(697,11): Error: a lemma is not allowed to use 'new' +125 resolution/type errors detected in GhostAllocations-Resolution.dfy diff --git a/Test/dafny0/GhostAllocations.dfy b/Test/dafny0/GhostAllocations.dfy new file mode 100644 index 00000000000..a252cb3829e --- /dev/null +++ b/Test/dafny0/GhostAllocations.dfy @@ -0,0 +1,188 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +class Cell { + var data: int +} + +method M() returns (c: Cell) + ensures fresh(c) + +ghost method G() returns (c: Cell) + ensures fresh(c) + +lemma L() returns (c: Cell) + ensures fresh(c) + +twostate lemma L2() returns (c: Cell) + ensures fresh(c) + +predicate P(c: Cell) +least lemma Least() + ensures exists c: Cell :: P(c) && fresh(c) + +method Caller() { + if + case true => + var c := M(); + assert false; // error + case true => + var c := G(); + assert false; // error + case true => + var c := L(); + assert false; // unreachable, since lemma's postcondition is untenable + case true => + var c := L2(); + assert false; // unreachable, since lemma's postcondition is untenable + case true => + Least(); + ghost var c :| P(c) && fresh(c); + assert false; // unreachable, since lemma's postcondition is untenable + case true => + Least#[10](); + ghost var c :| P(c) && fresh(c); + assert false; // unreachable, since lemma's postcondition is untenable +} + +class CellWrapper { + var c: Cell + constructor (c: Cell) { + this.c := c; + } + ghost constructor Gh(c: Cell) { + this.c := c; + } +} + +method Modify0(w: CellWrapper) + modifies w +{ + modify w; + assume fresh(w.c); + assert false; // error: assuming fresh(w.c) does not lead to any contradiction +} + +method Modify1(w: CellWrapper) + modifies w +{ + assume fresh(w.c); + assert false; // unreachable, due to the previous assumption +} + +method Modify2() { + modify {}; + assume exists c: Cell :: P(c) && fresh(c); + assert false; // error: assuming the body-less modify statement allocates a Cell does not lead to any contradiction +} + +ghost method Modify3() { + modify {}; + assume exists c: Cell :: P(c) && fresh(c); + assert false; // error: assuming the body-less modify statement allocates a Cell does not lead to any contradiction +} + +method ModifyBody0(w: CellWrapper) + modifies w +{ + modify w { + w.c := new Cell; + w.c.data := 15; + } + assert fresh(w.c); + assert false; // error +} + +method ModifyBody1(w: CellWrapper) + modifies w +{ + modify w`c { + var c := new Cell; + c.data := 15; + w.c := c; + } + assert fresh(c); + assert false; // error +} + +// ------------------- new ------------------- + +method SimpleNew() { + ghost var c: Cell; + c := new Cell; + + ghost var w: CellWrapper; + w := new CellWrapper.Gh(c); + + ghost var arr: array, m: array2; + arr := new int[20]; + m := new real[2, 390]; + + var arr': array, m': array2; + arr' := new int[20]; + m' := new real[2, 390]; + arr, m := arr', m'; +} + +type GGG(00) + +class GhostableNonempty { + var g: GGG + ghost var h: GGG + + constructor A(g: GGG) { + this.g := g; + } + + constructor B() { + } // error: g is never assigned + + ghost constructor C(g: GGG) { + this.g := g; + } + + ghost constructor D() { // in a ghost context, we only need to know that g's type is nonempty (same as for h all along) + } +} + +type HHH(0) + +class GhostableAutoInit { + var g: HHH + ghost var h: HHH + + constructor A(g: HHH) { + this.g := g; + } + + constructor B() { + } + + ghost constructor C(g: HHH) { + this.g := g; + } + + ghost constructor D() { + } +} + +type JJJ + +class GhostablePossibleEmpty { + var g: JJJ + ghost var h: JJJ + + constructor A(g: JJJ) { + this.g := g; + } // error: h is never assigned + + constructor B() { + } // error (x2): g and h are never assigned + + ghost constructor C(g: JJJ) { + this.g := g; + } // error: h is never assigned + + ghost constructor D() { + } // error (x2): g and h are never assigned +} diff --git a/Test/dafny0/GhostAllocations.dfy.expect b/Test/dafny0/GhostAllocations.dfy.expect new file mode 100644 index 00000000000..053724aecb8 --- /dev/null +++ b/Test/dafny0/GhostAllocations.dfy.expect @@ -0,0 +1,16 @@ +GhostAllocations.dfy(138,2): Error: field 'g', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body +GhostAllocations.dfy(177,2): Error: field 'h', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body +GhostAllocations.dfy(180,2): Error: field 'g', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body +GhostAllocations.dfy(180,2): Error: field 'h', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body +GhostAllocations.dfy(184,2): Error: field 'h', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body +GhostAllocations.dfy(187,2): Error: field 'g', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body +GhostAllocations.dfy(187,2): Error: field 'h', which is subject to definite-assignment rules, might not have been defined at this point in the constructor body +GhostAllocations.dfy(28,11): Error: assertion violation +GhostAllocations.dfy(31,11): Error: assertion violation +GhostAllocations.dfy(63,9): Error: assertion violation +GhostAllocations.dfy(76,9): Error: assertion violation +GhostAllocations.dfy(82,9): Error: assertion violation +GhostAllocations.dfy(93,9): Error: assertion violation +GhostAllocations.dfy(105,9): Error: assertion violation + +Dafny program verifier finished with 5 verified, 14 errors diff --git a/Test/dafny0/LabeledAssertsResolution.dfy b/Test/dafny0/LabeledAssertsResolution.dfy index 7e65f895197..9d36daf4f63 100644 --- a/Test/dafny0/LabeledAssertsResolution.dfy +++ b/Test/dafny0/LabeledAssertsResolution.dfy @@ -1,117 +1,119 @@ // RUN: %dafny /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" + module ResolutionTests { -lemma A(b: bool, m: int, n: int) - requires m < n - requires sea: m + 3 < n - requires sjc: m + 5 < n - requires sjc: m + 7 < n // error: dominating label - requires jfk: m + 9 < n - requires m < n -{ - label a: assert true; - if b { - label x: assert true; - label K: assert {:myAttr 30} m < n; - label L: assert {:myAttr 30} m < n; - label 0: assert {:myAttr 30} m < n; - label 0: assert {:myAttr 30} m < n; // error: dominating label - label jfk: assert true; // error: dominating label - } else { - label x: assert true; + lemma A(b: bool, m: int, n: int) + requires m < n + requires sea: m + 3 < n + requires sjc: m + 5 < n + requires sjc: m + 7 < n // error: dominating label + requires jfk: m + 9 < n + requires m < n + { + label a: assert true; + if b { + label x: assert true; + label K: assert {:myAttr 30} m < n; + label L: assert {:myAttr 30} m < n; + label 0: assert {:myAttr 30} m < n; + label 0: assert {:myAttr 30} m < n; // error: dominating label + label jfk: assert true; // error: dominating label + } else { + label x: assert true; + assert {:myAttr 30} K: m < n; + assert {:myAttr 30} L: m < n; + assert {:myAttr 30} 0: m < n; + assert {:myAttr 30} 0: m < n; // error: dominating label + var x: int; + assert jfk: true; // error: dominating label + assert old(b) == old@a(b) == old@x(b); + } + assert 0010: m < n; assert {:myAttr 30} K: m < n; - assert {:myAttr 30} L: m < n; - assert {:myAttr 30} 0: m < n; - assert {:myAttr 30} 0: m < n; // error: dominating label - var x: int; - assert jfk: true; // error: dominating label - assert old(b) == old@a(b) == old@x(b); + label L: + assert {:myAttr 30} L: m < n; // error: dominating label + assert old(b) == old@a(b); + assert old(b) == old@sjc(b); + // var r := assert NotAllowedHere: 0 <= m; 10; // not allowed; won't parse } - assert 0010: m < n; - assert {:myAttr 30} K: m < n; - label L: - assert {:myAttr 30} L: m < n; // error: dominating label - assert old(b) == old@a(b); - assert old(b) == old@sjc(b); - // var r := assert NotAllowedHere: 0 <= m; 10; // not allowed; won't parse -} -function R(u: int): int - // requires i: 0 <= u // not allowed; won't parse -{ - // assert NotAllowedHere: 0 <= u; // not allowed; won't parse - u -} + function R(u: int): int + // requires i: 0 <= u // not allowed; won't parse + { + // assert NotAllowedHere: 0 <= u; // not allowed; won't parse + u + } -iterator Iter(x: int) yields (y: int) - requires A: 0 <= x - // yield requires B: 0 <= y // not allowed; won't parse -{ - assert C: 0 <= x < |ys|; - assert A: 0 <= x < |ys|; // error: dominating label - yield; - assert C: 0 <= x < |ys|; // error: dominating label -} + iterator Iter(x: int) yields (y: int) + requires A: 0 <= x + // yield requires B: 0 <= y // not allowed; won't parse + { + assert C: 0 <= x < |ys|; + assert A: 0 <= x < |ys|; // error: dominating label + yield; + assert C: 0 <= x < |ys|; // error: dominating label + } -twostate predicate Twop(x: int) - // requires A: 0 <= x // not allowed; won't parse -{ - true -} + twostate predicate Twop(x: int) + // requires A: 0 <= x // not allowed; won't parse + { + true + } -twostate lemma Twol(x: int) - requires A: 0 <= x -{ -} + twostate lemma Twol(x: int) + requires A: 0 <= x + { + } + + lemma Calc(x: int) + requires A: x < 10 + { + assert B: x < 150 by { reveal A; } + label QRS: assert TUV: x < 10 by { + break ABC; // error: a break is not allowed to leave the proof body + reveal A; + } -lemma Calc(x: int) - requires A: x < 10 -{ - assert B: x < 150 by { reveal A; } - label QRS: assert TUV: x < 10 by { - break ABC; // error: a break is not allowed to leave the proof body - reveal A; + calc { + x < 200; + == { reveal B; + label XYZ: + reveal C; // error: C is not dominated here + assert old@XYZ(x) == x; + } + x < 150; + == { assert C: x < 90 by { reveal A; } + reveal C; + } + x < 102; + == { assert C: x < 90 by { reveal A; } // it's okay to have another C here + } + x < 100; + == { reveal A;} + x < 10; + == { assert old@XYZ(x) == x; } // error: XYZ is not in scope here + x < 100; + == + { label ABC: assert DEF: x < 10 by { reveal A; } } + { label ABC: assert DEF: x < 10 by { reveal A; } } + x < 100; + } } - calc { - x < 200; - == { reveal B; - label XYZ: - reveal C; // error: C is not dominated here - assert old@XYZ(x) == x; - } - x < 150; - == { assert C: x < 90 by { reveal A; } - reveal C; - } - x < 102; - == { assert C: x < 90 by { reveal A; } // it's okay to have another C here - } - x < 100; - == { reveal A;} - x < 10; - == { assert old@XYZ(x) == x; } // error: XYZ is not in scope here - x < 100; - == - { label ABC: assert DEF: x < 10 by { reveal A; } } - { label ABC: assert DEF: x < 10 by { reveal A; } } - x < 100; + class C { + var g: int + var h: int } -} -class C { - var g: int - var h: int -} -twostate lemma T3(c: C) - requires old(c.g) == 10 - requires c.g == 20 - requires A: old(c.h) == 100 - requires B: c.h == 200 -{ - reveal A, B, A, A; // this can be a list - reveal A, X, A, A; // error: C not defined -} + twostate lemma T3(c: C) + requires old(c.g) == 10 + requires c.g == 20 + requires A: old(c.h) == 100 + requires B: c.h == 200 + { + reveal A, B, A, A; // this can be a list + reveal A, X, A, A; // error: C not defined + } } // module ResolutionTests @@ -165,7 +167,7 @@ module GitIssue408 { var u := 11; u := 20; x := 20; // error: x is declared outside this assert-by block - x := Six(); // error: x is declared outside this assert-by block + x := Six(); // error (x2): x is declared outside this assert-by block, and Six is a ghost method y := 20; // error: y is declared outside this assert-by block c.data := 20.0; // error: assert-by cannot modify heap locations a[0] := 20.0; // error: assert-by cannot modify heap locations @@ -190,7 +192,7 @@ module GitIssue408 { 5; == { var y := 9; y := 10; - x := Six(); // error: x is declared outside this hint + x := Six(); // error (x2): x is declared outside this hint, and Six is a ghost method assert 2 < 12 by { var u := 11; u := 20; @@ -280,10 +282,6 @@ module ForallStmtTests { var y := 9; x := 6; // error: x is declared outside forall statement x := Six(); // error: x is declared outside forall statement - c.data := 20.0; // error: proof-forall statement cannot modify heap locations - a[0] := 20.0; // error: proof-forall statement cannot modify heap locations - m[0,0] := 20.0; // error: proof-forall statement cannot modify heap locations - modify c; // error: proof-forall cannot modify heap locations } } @@ -381,3 +379,27 @@ module OddExpressionChecks { 2; ww + 7 } + +module MoreGhostTests { + class C { + ghost var data: real + } + + ghost method Six() returns (x: int) { + x := 6; + } + + method Forall(c: C, a: array, m: array2) { + ghost var x := 5; + + forall f | 0 <= f < 82 + ensures f < 100 + { + var y := 9; + c.data := 20.0; // error: proof-forall statement cannot modify heap locations + a[0] := 20.0; // error: proof-forall statement cannot modify heap locations + m[0,0] := 20.0; // error: proof-forall statement cannot modify heap locations + modify c; // error: proof-forall cannot modify heap locations + } + } +} diff --git a/Test/dafny0/LabeledAssertsResolution.dfy.expect b/Test/dafny0/LabeledAssertsResolution.dfy.expect index 7d965079383..06bc4907fc6 100644 --- a/Test/dafny0/LabeledAssertsResolution.dfy.expect +++ b/Test/dafny0/LabeledAssertsResolution.dfy.expect @@ -1,79 +1,70 @@ -LabeledAssertsResolution.dfy(51,9): Error: assert label shadows a dominating label -LabeledAssertsResolution.dfy(53,9): Error: assert label shadows a dominating label -LabeledAssertsResolution.dfy(8,11): Error: assert label shadows a dominating label -LabeledAssertsResolution.dfy(18,10): Error: label shadows a dominating label -LabeledAssertsResolution.dfy(19,10): Error: label shadows a dominating label -LabeledAssertsResolution.dfy(25,24): Error: assert label shadows a dominating label -LabeledAssertsResolution.dfy(27,11): Error: assert label shadows a dominating label -LabeledAssertsResolution.dfy(33,22): Error: assert label shadows a dominating label -LabeledAssertsResolution.dfy(72,10): Error: break label is undefined or not in scope: ABC -LabeledAssertsResolution.dfy(80,15): Error: unresolved identifier: reveal_C -LabeledAssertsResolution.dfy(93,15): Error: no label 'XYZ' in scope at this time -LabeledAssertsResolution.dfy(113,12): Error: unresolved identifier: reveal_X -LabeledAssertsResolution.dfy(244,10): Error: yield statement is not allowed in this context (because it is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(249,6): Error: yield statement is not allowed in this context (because it is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(244,10): Error: yield statement is not allowed inside a hint -LabeledAssertsResolution.dfy(249,6): Error: yield statement is not allowed inside an assert-by body -LabeledAssertsResolution.dfy(123,6): Error: an assert-by body is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(137,6): Error: an assert-by body is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(171,13): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(172,15): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(176,11): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(177,13): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(186,15): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(187,17): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(167,8): Error: an assert-by body is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(168,8): Error: an assert-by body is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(52,11): Error: assert label shadows a dominating label +LabeledAssertsResolution.dfy(54,11): Error: assert label shadows a dominating label +LabeledAssertsResolution.dfy(9,13): Error: assert label shadows a dominating label +LabeledAssertsResolution.dfy(19,12): Error: label shadows a dominating label +LabeledAssertsResolution.dfy(20,12): Error: label shadows a dominating label +LabeledAssertsResolution.dfy(26,26): Error: assert label shadows a dominating label +LabeledAssertsResolution.dfy(28,13): Error: assert label shadows a dominating label +LabeledAssertsResolution.dfy(34,24): Error: assert label shadows a dominating label +LabeledAssertsResolution.dfy(73,12): Error: break label is undefined or not in scope: ABC +LabeledAssertsResolution.dfy(81,17): Error: unresolved identifier: reveal_C +LabeledAssertsResolution.dfy(94,17): Error: no label 'XYZ' in scope at this time +LabeledAssertsResolution.dfy(115,14): Error: unresolved identifier: reveal_X +LabeledAssertsResolution.dfy(246,10): Error: yield statement is not allowed in this context (because it is guarded by a specification-only expression) +LabeledAssertsResolution.dfy(251,6): Error: yield statement is not allowed in this context (because it is guarded by a specification-only expression) +LabeledAssertsResolution.dfy(125,6): Error: an assert-by body is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(139,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +LabeledAssertsResolution.dfy(139,6): Error: an assert-by body is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(170,16): Error: in an assert-by body, calls are allowed only to lemmas +LabeledAssertsResolution.dfy(172,10): Error: an assert-by body is not allowed to make heap updates +LabeledAssertsResolution.dfy(173,13): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +LabeledAssertsResolution.dfy(174,15): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +LabeledAssertsResolution.dfy(175,8): Error: a modify statement is not allowed in an assert-by body +LabeledAssertsResolution.dfy(177,8): Error: an assert-by body is not allowed to make heap updates +LabeledAssertsResolution.dfy(178,11): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +LabeledAssertsResolution.dfy(179,13): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +LabeledAssertsResolution.dfy(180,6): Error: a modify statement is not allowed in an assert-by body +LabeledAssertsResolution.dfy(187,12): Error: a hint is not allowed to make heap updates +LabeledAssertsResolution.dfy(188,15): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +LabeledAssertsResolution.dfy(189,17): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +LabeledAssertsResolution.dfy(190,10): Error: a modify statement is not allowed in a hint +LabeledAssertsResolution.dfy(195,18): Error: in a hint, calls are allowed only to lemmas LabeledAssertsResolution.dfy(169,8): Error: an assert-by body is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(170,10): Error: an assert-by body is not allowed to update heap locations -LabeledAssertsResolution.dfy(171,9): Error: an assert-by body is not allowed to update heap locations -LabeledAssertsResolution.dfy(172,9): Error: an assert-by body is not allowed to update heap locations -LabeledAssertsResolution.dfy(173,8): Error: modify statements are not allowed inside an assert-by body -LabeledAssertsResolution.dfy(175,8): Error: an assert-by body is not allowed to update heap locations -LabeledAssertsResolution.dfy(176,7): Error: an assert-by body is not allowed to update heap locations -LabeledAssertsResolution.dfy(177,7): Error: an assert-by body is not allowed to update heap locations -LabeledAssertsResolution.dfy(178,6): Error: modify statements are not allowed inside an assert-by body -LabeledAssertsResolution.dfy(201,18): Error: a hint is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(202,18): Error: a hint is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(197,12): Error: an assert-by body is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(198,12): Error: an assert-by body is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(183,10): Error: a hint is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(185,12): Error: a hint is not allowed to update heap locations -LabeledAssertsResolution.dfy(186,11): Error: a hint is not allowed to update heap locations -LabeledAssertsResolution.dfy(187,11): Error: a hint is not allowed to update heap locations -LabeledAssertsResolution.dfy(188,10): Error: modify statements are not allowed inside a hint -LabeledAssertsResolution.dfy(193,10): Error: a hint is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(217,8): Error: an assert-by body is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(218,8): Error: an assert-by body is not allowed to update a variable it doesn't declare -LabeledAssertsResolution.dfy(220,31): Error: return statement is not allowed inside a hint -LabeledAssertsResolution.dfy(220,31): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(221,43): Error: return statement is not allowed inside a hint -LabeledAssertsResolution.dfy(221,43): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(230,14): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(235,10): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) -LabeledAssertsResolution.dfy(230,14): Error: return statement is not allowed inside a hint -LabeledAssertsResolution.dfy(235,10): Error: return statement is not allowed inside an assert-by body -LabeledAssertsResolution.dfy(320,6): Error: yield statement is not allowed inside a forall statement -LabeledAssertsResolution.dfy(281,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement -LabeledAssertsResolution.dfy(282,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement -LabeledAssertsResolution.dfy(283,8): Error: the body of the enclosing forall statement is not allowed to update heap locations -LabeledAssertsResolution.dfy(284,7): Error: the body of the enclosing forall statement is not allowed to update heap locations -LabeledAssertsResolution.dfy(285,7): Error: the body of the enclosing forall statement is not allowed to update heap locations -LabeledAssertsResolution.dfy(286,6): Error: body of forall statement is not allowed to use a modify statement -LabeledAssertsResolution.dfy(299,8): Warning: the conclusion of the body of this forall statement will not be known outside the forall statement; consider using an 'ensures' clause -LabeledAssertsResolution.dfy(300,10): Error: body of forall statement is attempting to update a variable declared outside the forall statement -LabeledAssertsResolution.dfy(301,10): Error: body of forall statement is attempting to update a variable declared outside the forall statement -LabeledAssertsResolution.dfy(302,10): Error: body of forall statement is attempting to update a variable declared outside the forall statement -LabeledAssertsResolution.dfy(312,6): Error: return statement is not allowed inside a forall statement -LabeledAssertsResolution.dfy(331,14): Error: trying to break out of more loop levels than there are enclosing loops -LabeledAssertsResolution.dfy(333,20): Error: break label is undefined or not in scope: A -LabeledAssertsResolution.dfy(338,10): Error: trying to break out of more loop levels than there are enclosing loops -LabeledAssertsResolution.dfy(339,16): Error: break label is undefined or not in scope: A -LabeledAssertsResolution.dfy(345,10): Error: trying to break out of more loop levels than there are enclosing loops -LabeledAssertsResolution.dfy(346,16): Error: break label is undefined or not in scope: A -LabeledAssertsResolution.dfy(357,8): Error: return statement is allowed only in method -LabeledAssertsResolution.dfy(372,8): Error: return statement is allowed only in method -LabeledAssertsResolution.dfy(364,10): Error: return statement is allowed only in method -LabeledAssertsResolution.dfy(379,10): Error: return statement is allowed only in method -77 resolution/type errors detected in LabeledAssertsResolution.dfy +LabeledAssertsResolution.dfy(170,8): Error: an assert-by body is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(171,8): Error: an assert-by body is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(203,18): Error: a hint is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(204,18): Error: a hint is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(199,12): Error: an assert-by body is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(200,12): Error: an assert-by body is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(185,10): Error: a hint is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(195,10): Error: a hint is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(219,8): Error: an assert-by body is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(220,8): Error: an assert-by body is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(222,31): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) +LabeledAssertsResolution.dfy(223,43): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) +LabeledAssertsResolution.dfy(232,14): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) +LabeledAssertsResolution.dfy(237,10): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) +LabeledAssertsResolution.dfy(297,8): Warning: the conclusion of the body of this forall statement will not be known outside the forall statement; consider using an 'ensures' clause +LabeledAssertsResolution.dfy(318,6): Error: yield statement is not allowed in this context (because it is guarded by a specification-only expression) +LabeledAssertsResolution.dfy(284,14): Error: in a forall statement, calls are allowed only to lemmas +LabeledAssertsResolution.dfy(283,6): Error: a forall statement is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(284,6): Error: a forall statement is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(298,10): Error: a forall statement is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(299,10): Error: a forall statement is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(300,10): Error: a forall statement is not allowed to update a variable it doesn't declare +LabeledAssertsResolution.dfy(310,6): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) +LabeledAssertsResolution.dfy(329,14): Error: trying to break out of more loop levels than there are enclosing loops +LabeledAssertsResolution.dfy(331,20): Error: break label is undefined or not in scope: A +LabeledAssertsResolution.dfy(336,10): Error: trying to break out of more loop levels than there are enclosing loops +LabeledAssertsResolution.dfy(337,16): Error: break label is undefined or not in scope: A +LabeledAssertsResolution.dfy(343,10): Error: trying to break out of more loop levels than there are enclosing loops +LabeledAssertsResolution.dfy(344,16): Error: break label is undefined or not in scope: A +LabeledAssertsResolution.dfy(355,8): Error: return statement is allowed only in method +LabeledAssertsResolution.dfy(370,8): Error: return statement is allowed only in method +LabeledAssertsResolution.dfy(362,10): Error: return statement is allowed only in method +LabeledAssertsResolution.dfy(377,10): Error: return statement is allowed only in method +LabeledAssertsResolution.dfy(399,8): Error: a forall statement is not allowed to make heap updates +LabeledAssertsResolution.dfy(400,11): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +LabeledAssertsResolution.dfy(401,13): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +LabeledAssertsResolution.dfy(402,6): Error: a modify statement is not allowed in a forall statement +68 resolution/type errors detected in LabeledAssertsResolution.dfy diff --git a/Test/dafny0/ModifyStmt.dfy b/Test/dafny0/ModifyStmt.dfy index 8937d487273..9ffe538d549 100644 --- a/Test/dafny0/ModifyStmt.dfy +++ b/Test/dafny0/ModifyStmt.dfy @@ -181,4 +181,3 @@ class ModifyBody { assert xx == x; // fine, because the modify body trumps the modify frame } } - diff --git a/Test/dafny0/NonGhostQuantifiers.dfy.expect b/Test/dafny0/NonGhostQuantifiers.dfy.expect index 402b2df5195..954aa323480 100644 --- a/Test/dafny0/NonGhostQuantifiers.dfy.expect +++ b/Test/dafny0/NonGhostQuantifiers.dfy.expect @@ -4,7 +4,7 @@ NonGhostQuantifiers.dfy(50,4): Error: quantifiers in non-ghost contexts must be NonGhostQuantifiers.dfy(54,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'n' NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'y' NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'x' -NonGhostQuantifiers.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +NonGhostQuantifiers.dfy(140,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression NonGhostQuantifiers.dfy(149,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references, but values of 'c' may contain references NonGhostQuantifiers.dfy(153,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references, but values of 'c' may contain references NonGhostQuantifiers.dfy(158,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references, but values of 'c' may contain references diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy index a9101a1f46d..a1816d5f335 100644 --- a/Test/dafny0/Parallel.dfy +++ b/Test/dafny0/Parallel.dfy @@ -6,7 +6,7 @@ class C { var n: nat var st: set - ghost method CLemma(k: int) + lemma CLemma(k: int) requires k != -23 ensures data < k // magic, isn't it (or bogus, some would say) } @@ -203,10 +203,10 @@ method OmittedRange() { class TwoState_C { ghost var data: int } -// It is not possible to achieve this postcondition in a ghost method, because ghost -// contexts are not allowed to allocate state. Callers of this ghost method will know +// It is not possible to achieve this postcondition in a lemma, because lemma +// contexts are not allowed to allocate state. Callers of this lemma will know // that the postcondition is tantamount to 'false'. -ghost method TwoState0(y: int) +lemma TwoState0(y: int) ensures exists o: TwoState_C {:nowarn} :: allocated(o) && fresh(o) method TwoState_Main0() { diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index 625f2fa83f8..56c59b27237 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -1,133 +1,261 @@ // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" -module Misc { -class C { - var data: int; - ghost var gdata: int; - ghost method Init_ModifyNothing() { } - ghost method Init_ModifyThis() modifies this; - { - gdata := 7; + +module Basics { + method M() { + var k := 0; + forall i | 0 <= i < 20 { + k := k + i; // error: not allowed to assign to local k, since k is not declared inside forall block + } + + forall i | 0 <= i < 20 + ensures true + { + var x := i; + x := x + 1; + } + + ghost var y; + var z; + forall i | 0 <= i + ensures true + { + var x := i; + x := x + 1; + y := 18; // error: assigning to a (ghost) variable inside a ghost forall block + z := 20; // error: assigning to a (non-ghost) variable inside a ghost forall block + } } - ghost method Init_ModifyStuff(c: C) modifies this, c; { } - method NonGhostMethod() { print "hello\n"; } - ghost method GhostMethodWithModifies(x: int) modifies this; { gdata := gdata + x; } } -method M0(IS: set) -{ - forall (i | 0 <= i < 20) { - i := i + 1; // error: not allowed to assign to bound variable - } +module Misc { + class C { } - var k := 0; - forall (i | 0 <= i < 20) { - k := k + i; // error: not allowed to assign to local k, since k is not declared inside forall block - } + method M0(IS: set) { + forall i | 0 <= i < 20 { + i := i + 1; // error: not allowed to assign to bound variable + } - forall (i | 0 <= i < 20) - ensures true; - { - var x := i; - x := x + 1; + forall i | 0 <= i + ensures true + { + ghost var x := i; + x := x + 1; // cool + } + + var ca := new C[20]; + forall i | 0 <= i < 20 { + ca[i] := new C; // error: new allocation not allowed + } } - ghost var y; - var z; - forall (i | 0 <= i) - ensures true; - { - var x := i; - x := x + 1; - y := 18; // error: assigning to a (ghost) variable inside a ghost forall block - z := 20; // error: assigning to a (non-ghost) variable inside a ghost forall block + method M1() { + forall i | 0 <= i < 20 { + assert i < 100; + if i == 17 { break; } // error: nothing to break out of + } + + var m := 0; + label OutsideLoop: + while m < 20 { + forall i | 0 <= i < 20 { + if i == 17 { break; } // error: not allowed to break out of loop that sits outside forall + if i == 8 { break break; } // error: ditto (also: attempt to break too far) + if i == 9 { break OutsideLoop; } // error: ditto + } + m := m + 1; + } + + forall i | 0 <= i < 20 { + var j := 0; + while j < i { + if j == 6 { break; } // fine + if j % 7 == 4 { break break; } // error: attempt to break out too far + if j % 7 == 4 { break OutsideLoop; } // error: attempt to break to place not in enclosing scope + j := j + 1; + } + } } +} - forall (i | 0 <= i) - ensures true; - { - ghost var x := i; - x := x + 1; // cool +module AnotherModule { + class C { + var data: int + ghost var gdata: int + + ghost method Init_ModifyNothing() { } + + ghost method Init_ModifyThis() + modifies this + { + data := 6; // error: assignment to a non-ghost field + gdata := 7; + } + + ghost method Init_ModifyStuff(c: C) + modifies this, c + { + } + + method NonGhostMethod() { + print "hello\n"; + } + + ghost method GhostMethodWithModifies(x: int) + modifies this + { + gdata := gdata + x; + } } - var ca := new C[20]; - forall (i | 0 <= i < 20) { - ca[i] := new C; // error: new allocation not allowed + method TestNew() { + forall i | 0 <= i < 20 + ensures true + { + var c := new C; // error: 'new' not allowed in proof context + var d := new C.Init_ModifyNothing(); // error (x2): 'new' not allowed in ghost context + var e := new C.Init_ModifyThis(); // error (x2): 'new' not allowed in ghost context + var f := new C.Init_ModifyStuff(e); // error (x2): 'new' not allowed in ghost context + c.Init_ModifyStuff(d); // error: not allowed to call method with modifies clause in ghost context + c.NonGhostMethod(); // error: only allowed to call ghost methods (because of possible 'print' statements, sigh) + } } - forall (i | 0 <= i < 20) - ensures true; - { - var c := new C; // error: 'new' not allowed in ghost context - var d := new C.Init_ModifyNothing(); // error: 'new' not allowed in ghost context - var e := new C.Init_ModifyThis(); // error: 'new' not allowed in ghost context - var f := new C.Init_ModifyStuff(e); // error: 'new' not allowed in ghost context - c.Init_ModifyStuff(d); // error: not allowed to call method with modifies clause in ghost context - c.NonGhostMethod(); // error: only allowed to call ghost methods (because of possible 'print' statements, sigh) + + method M2() { + var a := new int[100]; + forall x | 0 <= x < 100 + ensures true + { + a[x] :| assume a[x] > 0; // error: not allowed to update heap location in a proof-forall statement + } } -} -method M1() { - forall (i | 0 <= i < 20) { - assert i < 100; - if (i == 17) { break; } // error: nothing to break out of + method M3(c: C) { + forall x { + c.GhostMethodWithModifies(x); // error: not allowed to call method with nonempty modifies clause + } + forall x + ensures true + { + c.GhostMethodWithModifies(x); // error: not allowed to call method with nonempty modifies clause + } } - forall (i | 0 <= i < 20) ensures true; { - if (i == 8) { return; } // error: return not allowed inside forall block + method AggregatePrinting() { + forall i | 0 <= i < 1000 + ensures true + { + print "here we go\n"; // error: cannot print in ghost context + } } +} - var m := 0; - label OutsideLoop: - while (m < 20) { - forall (i | 0 <= i < 20) { - if (i == 17) { break; } // error: not allowed to break out of loop that sits outside forall - if (i == 8) { break break; } // error: ditto (also: attempt to break too far) - if (i == 9) { break OutsideLoop; } // error: ditto +module UpdatesInOuterScope { + method M() { + ghost var x := 0; + forall i | 0 <= i < 100 + ensures true + { + // AssignStmt + x := 10; + // AssignSuchThatStmt + x :| x == 10; + // CallStmt + x := P(); } - m := m + 1; } - forall (i | 0 <= i < 20) { - var j := 0; - while (j < i) { - if (j == 6) { break; } // fine - if (j % 7 == 4) { break break; } // error: attempt to break out too far - if (j % 7 == 4) { break OutsideLoop; } // error: attempt to break to place not in enclosing scope - j := j + 1; + method P() returns (x: int) +} + +module MoreReturn { + method M() { + forall i | 0 <= i < 20 + ensures true + { + if i == 8 { return; } // error: return not allowed inside forall block } } } -method M2() { - var a := new int[100]; - forall (x | 0 <= x < 100) - ensures true; +// ---------- refinement of modify statements + +module NoRefinement { + class Cell { + var data: int + } + + method W(c: Cell) { - a[x] :| assume a[x] > 0; // error: not allowed to update heap location in a proof-forall statement + var c := new Cell; + var i := 0; + label L: + while i < 10 + invariant i == 0 || c.data == 10 + { + modify c { + if * { + break; // fine + } else if * { + break L; // fine + } + c.data := 9; + } + c.data := 10; + i := i + 1; + } } } -method M3(c: C) - requires c != null; -{ - forall x { - c.GhostMethodWithModifies(x); // error: not allowed to call method with nonempty modifies clause +module ModifyStmtBreak0 { + class Cell { + var data: int } - forall x - ensures true; + + method W(c: Cell) + modifies c + ensures c.data == 10 { - c.GhostMethodWithModifies(x); // error: not allowed to call method with nonempty modifies clause + var i := 0; + label L: + while i < 10 + invariant i == 0 || c.data == 10 + { + modify c; + c.data := 10; + i := i + 1; + } } } + +module ModifyStmtBreak1 refines ModifyStmtBreak0 { + method W... { + ...; + while ... { + modify ... { + if * { + break; // error: a "break" here would cause a problem with the refinement + } else { + break L; // error: a "break" here would cause a problem with the refinement + } + } + ...; + } + } } -module AnotherModule { - class C { - var data: int; - ghost var gdata: int; - ghost method Init_ModifyThis() modifies this; - { - data := 6; // error: assignment to a non-ghost field - gdata := 7; + +module ModifyStmtBreak1' refines ModifyStmtBreak0 { + method W... { + ...; + while ... { + modify c { // note, this is a new "modify" statement, not a refinement of the one above + if * { + break; // error: this is still not allowed, since it skips the rest of the loop body + } else { + break L; // error: ditto + } + } + ...; // (the previous "modify c;" statement is included here) } } } diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect index 934d3b96186..dd815cef7bc 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy.expect +++ b/Test/dafny0/ParallelResolveErrors.dfy.expect @@ -1,23 +1,36 @@ -ParallelResolveErrors.dfy(20,4): Error: LHS of assignment must denote a mutable variable -ParallelResolveErrors.dfy(25,4): Error: body of forall statement is attempting to update a variable declared outside the forall statement -ParallelResolveErrors.dfy(42,4): Error: body of forall statement is attempting to update a variable declared outside the forall statement -ParallelResolveErrors.dfy(43,4): Error: body of forall statement is attempting to update a variable declared outside the forall statement -ParallelResolveErrors.dfy(55,13): Error: new allocation not supported in forall statements -ParallelResolveErrors.dfy(60,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context -ParallelResolveErrors.dfy(64,22): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -ParallelResolveErrors.dfy(65,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods -ParallelResolveErrors.dfy(72,19): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(76,18): Error: return statement is not allowed inside a forall statement -ParallelResolveErrors.dfy(83,21): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(84,20): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(85,26): Error: break label is undefined or not in scope: OutsideLoop -ParallelResolveErrors.dfy(94,24): Error: trying to break out of more loop levels than there are enclosing loops -ParallelResolveErrors.dfy(95,30): Error: break label is undefined or not in scope: OutsideLoop -ParallelResolveErrors.dfy(106,5): Error: the body of the enclosing forall statement is not allowed to update heap locations -ParallelResolveErrors.dfy(114,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -ParallelResolveErrors.dfy(119,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -ParallelResolveErrors.dfy(129,11): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -22 resolution/type errors detected in ParallelResolveErrors.dfy +ParallelResolveErrors.dfy(26,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ParallelResolveErrors.dfy(8,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ParallelResolveErrors.dfy(25,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ParallelResolveErrors.dfy(26,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ParallelResolveErrors.dfy(36,6): Error: LHS of assignment must denote a mutable variable +ParallelResolveErrors.dfy(48,15): Error: new allocation not supported in aggregate assignments +ParallelResolveErrors.dfy(55,19): Error: trying to break out of more loop levels than there are enclosing loops +ParallelResolveErrors.dfy(62,21): Error: trying to break out of more loop levels than there are enclosing loops +ParallelResolveErrors.dfy(63,20): Error: trying to break out of more loop levels than there are enclosing loops +ParallelResolveErrors.dfy(64,26): Error: break label is undefined or not in scope: OutsideLoop +ParallelResolveErrors.dfy(73,24): Error: trying to break out of more loop levels than there are enclosing loops +ParallelResolveErrors.dfy(74,30): Error: break label is undefined or not in scope: OutsideLoop +ParallelResolveErrors.dfy(91,11): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost method +ParallelResolveErrors.dfy(115,15): Error: a forall statement is not allowed to use 'new' +ParallelResolveErrors.dfy(116,15): Error: a forall statement is not allowed to use 'new' +ParallelResolveErrors.dfy(116,21): Error: in a forall statement, calls are allowed only to lemmas +ParallelResolveErrors.dfy(117,15): Error: a forall statement is not allowed to use 'new' +ParallelResolveErrors.dfy(117,21): Error: in a forall statement, calls are allowed only to lemmas +ParallelResolveErrors.dfy(118,15): Error: a forall statement is not allowed to use 'new' +ParallelResolveErrors.dfy(118,21): Error: in a forall statement, calls are allowed only to lemmas +ParallelResolveErrors.dfy(119,24): Error: in a forall statement, calls are allowed only to lemmas +ParallelResolveErrors.dfy(120,22): Error: in a forall statement, calls are allowed only to lemmas +ParallelResolveErrors.dfy(129,7): Error: cannot assign to array element in a ghost context +ParallelResolveErrors.dfy(135,31): Error: in a forall statement, calls are allowed only to lemmas +ParallelResolveErrors.dfy(140,31): Error: in a forall statement, calls are allowed only to lemmas +ParallelResolveErrors.dfy(148,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ParallelResolveErrors.dfy(164,12): Error: in a forall statement, calls are allowed only to lemmas +ParallelResolveErrors.dfy(160,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ParallelResolveErrors.dfy(162,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ParallelResolveErrors.dfy(164,6): Error: a forall statement is not allowed to update a variable it doesn't declare +ParallelResolveErrors.dfy(176,18): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) +ParallelResolveErrors.dfy(237,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment +ParallelResolveErrors.dfy(239,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment +ParallelResolveErrors.dfy(253,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment +ParallelResolveErrors.dfy(255,10): Error: break statement in skeleton is not allowed to break outside the skeleton fragment +35 resolution/type errors detected in ParallelResolveErrors.dfy diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy index dd0bd2c9335..0d9463b8c6c 100644 --- a/Test/dafny0/ParseErrors.dfy +++ b/Test/dafny0/ParseErrors.dfy @@ -102,7 +102,7 @@ ghost greatest lemma GhCL() // error: a lemma is not allowed to be declared "gh ghost twostate lemma GhL2() // error: a lemma is not allowed to be declared "ghost" -- it is already ghost class C { - ghost constructor Make() // error: a constructor is not allowed to be ghost + constructor Make() ghost method M() } @@ -188,3 +188,18 @@ module NameOnlyParameters { iterator Iter0(nameonly x: int) yields (y: int) iterator Iter0(x: int) yields (nameonly y: int) // error: 'nameonly' not allowed here } + +// ------------------------- parameters of ghost constructors ------------------------------ + +module GhostConstructors { + class Either { + constructor A(x: int) { + } + ghost constructor B(x: int) { + } + constructor C(ghost x: int) { + } + ghost constructor D(ghost x: int) { // error: don't use 'ghost' keyword for ghost constructor parameters + } +} +} diff --git a/Test/dafny0/ParseErrors.dfy.expect b/Test/dafny0/ParseErrors.dfy.expect index c837d3bfcd3..e26fd9c8855 100644 --- a/Test/dafny0/ParseErrors.dfy.expect +++ b/Test/dafny0/ParseErrors.dfy.expect @@ -18,7 +18,6 @@ ParseErrors.dfy(96,0): Error: a lemma cannot be declared ghost (they are 'ghost' ParseErrors.dfy(98,0): Error: a least lemma cannot be declared ghost (they are 'ghost' by default). ParseErrors.dfy(100,0): Error: a greatest lemma cannot be declared ghost (they are 'ghost' by default). ParseErrors.dfy(102,0): Error: a two-state lemma cannot be declared ghost (they are 'ghost' by default). -ParseErrors.dfy(105,2): Error: a constructor cannot be declared 'ghost'. ParseErrors.dfy(113,16): Error: formal cannot be declared 'ghost' in this context ParseErrors.dfy(114,11): Error: formal cannot be declared 'ghost' in this context ParseErrors.dfy(116,8): Error: formal cannot be declared 'ghost' in this context @@ -46,4 +45,5 @@ ParseErrors.dfy(179,14): Error: use of the 'nameonly' modifier must be accompani ParseErrors.dfy(183,23): Error: closeparen expected ParseErrors.dfy(186,28): Error: formal cannot be declared 'nameonly' in this context ParseErrors.dfy(189,33): Error: formal cannot be declared 'nameonly' in this context +ParseErrors.dfy(202,24): Error: formal cannot be declared 'ghost' in this context 48 parse errors detected in ParseErrors.dfy diff --git a/Test/dafny0/PrettyPrinting.dfy b/Test/dafny0/PrettyPrinting.dfy index 5e2c793fd4c..9c7f2fb3b68 100644 --- a/Test/dafny0/PrettyPrinting.dfy +++ b/Test/dafny0/PrettyPrinting.dfy @@ -117,3 +117,10 @@ module ByMethod { return -j; } } + +module GhostConstructors { + class C { + constructor X() + ghost constructor Y() + } +} diff --git a/Test/dafny0/PrettyPrinting.dfy.expect b/Test/dafny0/PrettyPrinting.dfy.expect index 803445526da..0b298ecac43 100644 --- a/Test/dafny0/PrettyPrinting.dfy.expect +++ b/Test/dafny0/PrettyPrinting.dfy.expect @@ -121,6 +121,14 @@ module ByMethod { return -j; } } + +module GhostConstructors { + class C { + constructor X() + + ghost constructor Y() + } +} PrettyPrinting.dfy(10,4): Warning: note, this loop has no body PrettyPrinting.dfy(11,4): Warning: note, this loop has no body PrettyPrinting.dfy(14,4): Warning: note, this loop has no body diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy index 82d74b4c6f6..47fefa14944 100644 --- a/Test/dafny0/Refinement.dfy +++ b/Test/dafny0/Refinement.dfy @@ -210,3 +210,69 @@ module IncorrectConcrete refines Abstract { } } } + +// ------------------------------------------------ + +module Modify0 { + class Cell { + var data: int + } + + method M(c: Cell) + modifies c + ensures c.data == 10 + { + modify c; + c.data := 10; + } + + method N() returns (x: int) + ensures x == 10 + { + var i := 0; + while i < 10 + x := 10; + } + + method P() returns (x: int) + ensures x == 10 + { + x := 10; + } + + method Q() returns (x: int) + ensures x == 10 + { + x := 10; + } +} + +module Modify1 refines Modify0 { + method M... { + modify ... { + return; // error: a "return" here would cause a problem with the refinement + } + ...; + } + + method N... { + ...; + while ... { + return; // error: a "return" here would cause a problem with the refinement + ...; + } + ...; + } + + method P... { + return; // error: a "return" here would cause a problem with the refinement + ...; + } + + method Q... { + { + return; // error: a "return" here would cause a problem with the refinement + } + ...; + } +} diff --git a/Test/dafny0/Refinement.dfy.expect b/Test/dafny0/Refinement.dfy.expect index 0cf610c5778..db9f7174b1a 100644 --- a/Test/dafny0/Refinement.dfy.expect +++ b/Test/dafny0/Refinement.dfy.expect @@ -1,3 +1,4 @@ +Refinement.dfy(233,4): Warning: note, this loop has no body (loop frame: i) Refinement.dfy(15,4): Error: A postcondition might not hold on this return path. Refinement.dfy(14,16): Related location: This is the postcondition that might not hold. Refinement.dfy[B](15,4): Error: A postcondition might not hold on this return path. @@ -14,5 +15,13 @@ Refinement.dfy(204,6): Error: assertion violation Refinement.dfy[IncorrectConcrete](131,18): Related location Refinement.dfy(209,6): Error: assertion violation Refinement.dfy[IncorrectConcrete](137,23): Related location +Refinement.dfy(253,6): Error: A postcondition might not hold on this return path. +Refinement.dfy[Modify1](223,19): Related location: This is the postcondition that might not hold. +Refinement.dfy(261,6): Error: A postcondition might not hold on this return path. +Refinement.dfy[Modify1](230,14): Related location: This is the postcondition that might not hold. +Refinement.dfy(268,4): Error: A postcondition might not hold on this return path. +Refinement.dfy[Modify1](238,14): Related location: This is the postcondition that might not hold. +Refinement.dfy(274,6): Error: A postcondition might not hold on this return path. +Refinement.dfy[Modify1](244,14): Related location: This is the postcondition that might not hold. -Dafny program verifier finished with 23 verified, 9 errors +Dafny program verifier finished with 28 verified, 13 errors diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index e625c8e24af..3cf15f06544 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -613,16 +613,16 @@ module NonInferredType { } } -// ------------ Here are some tests that ghost contexts don't allocate objects ------------- +// ------------ Here are some tests that lemma contexts don't allocate objects ------------- module GhostAllocationTests { class G { } iterator GIter() { } - - ghost method GhostNew0() + class H { constructor () } + lemma GhostNew0() ensures exists o: G :: fresh(o); { - var p := new G; // error: ghost context is not allowed to allocate state + var p := new G; // error: lemma context is not allowed to allocate state p := new G; // error: ditto } @@ -632,7 +632,7 @@ module GhostAllocationTests { z, t := 5, new G; // fine } if n < g { - var zz, tt := 5, new G; // error: 'new' not allowed in ghost contexts + var tt := new H(); // error: 'new' not allowed in ghost contexts } } @@ -642,37 +642,37 @@ module GhostAllocationTests { var y := new GIter(); // error: 'new' not allowed in ghost contexts (and a non-ghost method is not allowed to be called here either) } } - - method GhostNew3(n: nat) - { +} +module MoreGhostAllocationTests { + class G { } + method GhostNew3(n: nat) { var g := new G; calc { 5; - { var y := new G; } // error: 'new' not allowed in ghost contexts + { var y := new G; } // error: 'new' not allowed in lemma contexts 2 + 3; } } - ghost method GhostNew4(g: G) - modifies g; + modifies g { } } -module NewForall { +module NewForallAssign { class G { } - method NewForallTest(n: nat) - { + method NewForallTest(n: nat) { var a := new G[n]; forall i | 0 <= i < n { a[i] := new G; // error: 'new' is currently not supported in forall statements - } - forall i | 0 <= i < n - ensures true; // this makes the whole 'forall' statement into a ghost statement - { - a[i] := new G; // error: 'new' not allowed in ghost contexts, and proof-forall cannot update state - } - } + } } +} +module NewForallProof { + class G { } + method NewForallTest(n: nat) { var a := new G[n]; + forall i | 0 <= i < n ensures true { // this makes the whole 'forall' statement into a ghost statement + a[i] := new G; // error: proof-forall cannot update state (and 'new' not allowed in ghost contexts, but that's checked at a later stage) + } } } // ------------------------- underspecified types ------------------------------ @@ -780,20 +780,20 @@ module StatementsInExpressions { } 5; } + } +} - ghost method MyLemma() - ghost method MyGhostMethod() - modifies this; - method OrdinaryMethod() - ghost method OutParamMethod() returns (y: int) +module StmtExprOutParams { - function UseLemma(): int - { - MyLemma(); - MyGhostMethod(); // error: modifi2es state - OutParamMethod(); // error: has out-parameters - 10 - } + lemma MyLemma() + + lemma OutParamLemma() returns (y: int) + + function UseLemma(): int + { + MyLemma(); + OutParamLemma(); // error: has out-parameters + 10 } } @@ -930,22 +930,22 @@ module LhsLvalue { var c := new MyRecord[29]; mySeq[0] := 5; // error: cannot assign to a sequence element - mySeq[0] := MyLemma(); // error: ditto + mySeq[0] := MyMethod(); // error: ditto a[0] := 5; - a[0] := MyLemma(); + a[0] := MyMethod(); b[20, 18] := 5; - b[20, 18] := MyLemma(); + b[20, 18] := MyMethod(); c[25].x := 5; // error: cannot assign to a destructor - c[25].x := MyLemma(); // error: ditto + c[25].x := MyMethod(); // error: ditto mySeq[0..4] := 5; // error: cannot assign to a range - mySeq[0..4] := MyLemma(); // error: ditto + mySeq[0..4] := MyMethod(); // error: ditto a[0..4] := 5; // error: cannot assign to a range - a[0..4] := MyLemma(); // error: ditto + a[0..4] := MyMethod(); // error: ditto } datatype MyRecord = Make(x: int, y: int) - method MyLemma() returns (w: int) + method MyMethod() returns (w: int) } // ------------------- dirty loops ------------------- @@ -1547,16 +1547,16 @@ module GhostTests { } 5; } - ghost method MyLemma() - ghost method MyGhostMethod() - modifies this; - method OrdinaryMethod() - ghost method OutParamMethod() returns (y: int) - + } +} +module CallsInStmtExpr { + class MyClass { + lemma MyLemma() + ghost method MyEffectlessGhostMethod() function UseLemma(): int { + MyEffectlessGhostMethod(); // error: cannot call ghost methods (only lemmas) from this context MyLemma(); - OrdinaryMethod(); // error: not a ghost 10 } } diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index dc9fff1894c..36f5cff2095 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -65,8 +65,8 @@ ResolutionErrors.dfy(416,8): Error: arguments must have comparable types (got bo ResolutionErrors.dfy(416,8): Error: arguments must have comparable types (got bool and int) ResolutionErrors.dfy(420,8): Error: arguments must have comparable types (got bool and int) ResolutionErrors.dfy(420,8): Error: arguments must have comparable types (got bool and int) -ResolutionErrors.dfy(454,13): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(456,10): Error: a hint is not allowed to update heap locations +ResolutionErrors.dfy(454,13): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors.dfy(456,10): Error: a hint is not allowed to make heap updates ResolutionErrors.dfy(458,10): Error: a hint is not allowed to update a variable it doesn't declare ResolutionErrors.dfy(479,4): Error: More than one anonymous constructor ResolutionErrors.dfy(485,8): Error: when allocating an object of type 'Y', one of its constructor methods must be called @@ -82,21 +82,20 @@ ResolutionErrors.dfy(611,8): Error: the type of this local variable is underspec ResolutionErrors.dfy(612,25): Error: the type of this variable is underspecified ResolutionErrors.dfy(612,23): Error: type parameter 'T' (inferred to be '?') in the function call to 'P' could not be determined ResolutionErrors.dfy(612,18): Error: type of bound variable 'z' could not be determined; please specify the type explicitly -ResolutionErrors.dfy(625,13): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(626,9): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(635,23): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(642,15): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(651,17): Error: 'new' is not allowed in ghost contexts -ResolutionErrors.dfy(668,14): Error: new allocation not supported in forall statements -ResolutionErrors.dfy(673,7): Error: the body of the enclosing forall statement is not allowed to update heap locations -ResolutionErrors.dfy(673,14): Error: new allocation not allowed in ghost context +ResolutionErrors.dfy(625,13): Error: a lemma is not allowed to use 'new' +ResolutionErrors.dfy(626,9): Error: a lemma is not allowed to use 'new' +ResolutionErrors.dfy(635,16): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(642,15): Error: only ghost methods can be called from this context +ResolutionErrors.dfy(652,17): Error: a hint is not allowed to use 'new' +ResolutionErrors.dfy(667,14): Error: new allocation not supported in aggregate assignments +ResolutionErrors.dfy(674,14): Error: a forall statement is not allowed to use 'new' +ResolutionErrors.dfy(674,11): Error: assignment to array element is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression ResolutionErrors.dfy(690,26): Error: second argument to "in" must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got bool) ResolutionErrors.dfy(685,18): Error: second argument to "in" must be a set, multiset, or sequence with elements of type int, or a map with domain int (instead got ?) ResolutionErrors.dfy(702,13): Error: lemmas are not allowed to have modifies clauses ResolutionErrors.dfy(729,22): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating ResolutionErrors.dfy(762,22): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating -ResolutionErrors.dfy(793,19): Error: calls to methods with side-effects are not allowed inside a statement expression -ResolutionErrors.dfy(794,20): Error: wrong number of method result arguments (got 0, expected 1) +ResolutionErrors.dfy(795,17): Error: wrong number of method result arguments (got 0, expected 1) ResolutionErrors.dfy(816,4): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(827,40): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(850,6): Error: RHS (of type B) not assignable to LHS (of type object) @@ -212,22 +211,20 @@ ResolutionErrors.dfy(1433,13): Error: type of RHS of assign-such-that statement ResolutionErrors.dfy(1436,15): Error: type of left argument to + (int) must agree with the result type (bool) ResolutionErrors.dfy(1436,15): Error: type of right argument to + (int) must agree with the result type (bool) ResolutionErrors.dfy(1436,15): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -ResolutionErrors.dfy(1479,20): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(1501,10): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(1502,10): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(1503,20): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(1506,21): Error: a loop statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(1488,24): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(1501,18): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ResolutionErrors.dfy(1530,10): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(1531,10): Error: a hint is not allowed to update heap locations -ResolutionErrors.dfy(1532,11): Error: calls to methods with side-effects are not allowed inside a hint -ResolutionErrors.dfy(1535,21): Error: a loop statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(1523,24): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(1530,18): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ResolutionErrors.dfy(1559,20): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(1452,29): Error: only ghost methods can be called from this context -ResolutionErrors.dfy(1454,17): Error: calls to methods with side-effects are not allowed inside a hint +ResolutionErrors.dfy(1479,20): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors.dfy(1488,24): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors.dfy(1501,18): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost function +ResolutionErrors.dfy(1502,10): Error: a hint is not allowed to make heap updates +ResolutionErrors.dfy(1503,20): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors.dfy(1506,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +ResolutionErrors.dfy(1523,24): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors.dfy(1530,18): Error: assignment to non-ghost field is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ResolutionErrors.dfy(1531,10): Error: a hint is not allowed to make heap updates +ResolutionErrors.dfy(1532,11): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors.dfy(1535,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +ResolutionErrors.dfy(1452,29): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors.dfy(1454,17): Error: in a hint, calls are allowed only to lemmas +ResolutionErrors.dfy(1558,29): Error: in a statement expression, calls are allowed only to lemmas ResolutionErrors.dfy(1570,16): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating ResolutionErrors.dfy(1588,12): Error: trying to break out of more loop levels than there are enclosing loops ResolutionErrors.dfy(1600,20): Error: ghost fields are allowed only in specification contexts @@ -241,14 +238,14 @@ ResolutionErrors.dfy(1647,10): Error: the type of the bound variable 't' could n ResolutionErrors.dfy(1647,10): Error: the type of the bound variable 't' could not be determined ResolutionErrors.dfy(1647,10): Error: the type of the bound variable 't' could not be determined ResolutionErrors.dfy(1665,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) -ResolutionErrors.dfy(1667,10): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ResolutionErrors.dfy(1667,10): Error: assignment to non-ghost field is not allowed in this context, because this is a ghost method ResolutionErrors.dfy(1692,15): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x) -ResolutionErrors.dfy(1694,25): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -ResolutionErrors.dfy(1695,35): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ResolutionErrors.dfy(1694,25): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +ResolutionErrors.dfy(1695,35): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression ResolutionErrors.dfy(1705,4): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(1709,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ResolutionErrors.dfy(1709,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression ResolutionErrors.dfy(1719,4): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(1723,29): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ResolutionErrors.dfy(1723,29): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression ResolutionErrors.dfy(1731,21): Error: the type of the bound variable 'u' could not be determined ResolutionErrors.dfy(1732,23): Error: the type of the bound variable 'u' could not be determined ResolutionErrors.dfy(1735,27): Error: the type of the bound variable 'u' could not be determined @@ -531,8 +528,8 @@ ResolutionErrors.dfy(3366,9): Error: type parameter (T) passed to function MustB ResolutionErrors.dfy(3372,9): Error: type parameter (T) passed to function MustBeAutoInit must support auto-initialization (got PossiblyEmpty) ResolutionErrors.dfy(3387,9): Error: type parameter (T) passed to function NoReferences must support no references (got Class?) ResolutionErrors.dfy(3435,7): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(3449,21): Error: a loop statement used inside a hint is not allowed to have a modifies clause -ResolutionErrors.dfy(3456,21): Error: a loop statement used inside a hint is not allowed to have a modifies clause +ResolutionErrors.dfy(3449,21): Error: a loop in a hint is not allowed to use 'modifies' clauses +ResolutionErrors.dfy(3456,21): Error: a loop in a hint is not allowed to use 'modifies' clauses ResolutionErrors.dfy(3485,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got multiset) ResolutionErrors.dfy(3486,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got map) ResolutionErrors.dfy(3487,9): Error: the argument of a fresh expression must denote an object or a set or sequence of objects (instead got map) @@ -586,4 +583,4 @@ ResolutionErrors.dfy(3617,10): Error: a reads-clause expression must denote an o ResolutionErrors.dfy(3626,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got int -> int) ResolutionErrors.dfy(3631,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got set -> int) ResolutionErrors.dfy(3633,10): Error: a reads-clause expression must denote an object, a set/iset/multiset/seq of objects, or a function to a set/iset/multiset/seq of objects (instead got bool -> map) -583 resolution/type errors detected in ResolutionErrors.dfy +580 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 0e7aa7aa079..323963e8934 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -751,10 +751,10 @@ class GT { { if (*) { P0(); - assert forall x: GT {:nowarn} :: allocated(x) ==> old(allocated(x)); // error: method P2 may have allocated stuff + assert forall x: GT {:nowarn} :: allocated(x) ==> old(allocated(x)); // error: method P0 may have allocated stuff } else { P1(); - assert forall x: GT {:nowarn} :: allocated(x) ==> old(allocated(x)); // fine, because the ghost method does not allocate anything + assert forall x: GT {:nowarn} :: allocated(x) ==> old(allocated(x)); // error: ghost method P1 may have allocated stuff } } } diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index e589c422bbd..44573c94dfa 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -32,6 +32,7 @@ SmallTests.dfy(418,11): Error: assertion violation SmallTests.dfy(428,5): Error: cannot prove termination; try supplying a decreases clause SmallTests.dfy(733,13): Error: assertion violation SmallTests.dfy(754,13): Error: assertion violation +SmallTests.dfy(757,13): Error: assertion violation SmallTests.dfy(338,2): Error: A postcondition might not hold on this return path. SmallTests.dfy(332,10): Related location: This is the postcondition that might not hold. SmallTests.dfy(332,40): Related location @@ -51,7 +52,7 @@ SmallTests.dfy(701,9): Error: cannot establish the existence of LHS values that SmallTests.dfy(703,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate SmallTests.dfy(716,8): Error: cannot establish the existence of LHS values that satisfy the such-that predicate -Dafny program verifier finished with 56 verified, 47 errors +Dafny program verifier finished with 56 verified, 48 errors SmallTests.dfy.tmp.dprint.dfy(450,4): Warning: /!\ No trigger covering all quantified variables found. Dafny program verifier did not attempt verification diff --git a/Test/dafny0/StatementExpressions.dfy b/Test/dafny0/StatementExpressions.dfy index 84c13e36c2c..20f48e1bbe2 100644 --- a/Test/dafny0/StatementExpressions.dfy +++ b/Test/dafny0/StatementExpressions.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" // RUN: %diff "%s.expect" "%t" -ghost method M(n: nat) //returns (y: nat) +lemma M(n: nat) //returns (y: nat) { var y := F(n, 0); } @@ -15,7 +15,7 @@ function F(n: nat, p: int): nat n } -ghost method MM(n: nat) returns (y: nat) +lemma MM(n: nat) returns (y: nat) decreases n, 0; { if n != 0 { @@ -33,7 +33,7 @@ function FF(n: nat): nat n } -ghost method P(n: nat) +lemma P(n: nat) { if n != 0 { var y := @@ -46,7 +46,7 @@ ghost method P(n: nat) assert y == 100; } } -ghost method Q(n: nat) +lemma Q(n: nat) { if n != 0 { var y := diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 54263e35b81..825d37aa613 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -29,7 +29,7 @@ TypeTests.dfy(180,9): Error: cannot assign to non-ghost variable in a ghost cont TypeTests.dfy(198,10): Error: incorrect type of datatype constructor argument (expected int -> Dt, found int -> int) (covariant type parameter 1 would require int <: Dt) TypeTests.dfy(204,10): Error: incorrect type of datatype constructor argument (expected ? -> Dt, found Dt -> Dt) (contravariance for type parameter0 expects ? <: Dt) TypeTests.dfy(211,10): Error: incorrect type of function argument (expected ?, found set) -TypeTests.dfy(222,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +TypeTests.dfy(222,9): Error: assignment to array element is not allowed in this context, because this is a ghost method TypeTests.dfy(229,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'A' can be constructed TypeTests.dfy(230,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'B' can be constructed TypeTests.dfy(232,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Cycle' can be constructed diff --git a/Test/dafny4/ClassRefinement.dfy b/Test/dafny4/ClassRefinement.dfy index d259023ccf0..eea5caf7a16 100644 --- a/Test/dafny4/ClassRefinement.dfy +++ b/Test/dafny4/ClassRefinement.dfy @@ -6,12 +6,6 @@ // RUN: %diff "%s.expect" "%t" abstract module M0 { - class Cell { - var data: int - constructor (d: int) - ensures data == d - { data := d; } - } class Counter { ghost var N: int ghost var Repr: set @@ -51,6 +45,13 @@ abstract module M0 { } module M1 refines M0 { + class Cell { + var data: int + constructor (d: int) + ensures data == d + { data := d; } + } + class Counter ... { var c: Cell var d: Cell diff --git a/Test/dafny4/ClassRefinement.dfy.expect b/Test/dafny4/ClassRefinement.dfy.expect index 1c6cc1fd8cc..d698ab0e8aa 100644 --- a/Test/dafny4/ClassRefinement.dfy.expect +++ b/Test/dafny4/ClassRefinement.dfy.expect @@ -1,5 +1,5 @@ -Dafny program verifier finished with 12 verified, 0 errors +Dafny program verifier finished with 11 verified, 0 errors Dafny program verifier did not attempt verification 2 1 diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index 08756308162..bd10a9951a3 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -117,7 +117,7 @@ lemma Complete(n: int, lowDigit: int, base: int) returns (digits: seq) } } -ghost method inc(a: seq, lowDigit: int, base: int) returns (b: seq) +lemma inc(a: seq, lowDigit: int, base: int) returns (b: seq) requires IsSkewNumber(a, lowDigit, base) requires eval(a, base) == 0 ==> 1 < lowDigit + base ensures IsSkewNumber(b, lowDigit, base) && eval(b, base) == eval(a, base) + 1 @@ -157,7 +157,7 @@ ghost method inc(a: seq, lowDigit: int, base: int) returns (b: seq) } } -ghost method dec(a: seq, lowDigit: int, base: int) returns (b: seq) +lemma dec(a: seq, lowDigit: int, base: int) returns (b: seq) requires IsSkewNumber(a, lowDigit, base) requires eval(a, base) == 0 ==> lowDigit < 0 ensures IsSkewNumber(b, lowDigit, base) && eval(b, base) == eval(a, base) - 1 diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect index 1a70eeb592c..a90e75b402a 100644 --- a/Test/dafny4/set-compr.dfy.expect +++ b/Test/dafny4/set-compr.dfy.expect @@ -9,6 +9,6 @@ set-compr.dfy(53,26): Error: a function definition is not allowed to depend on t set-compr.dfy(52,33): Error: a function definition is not allowed to depend on the set of allocated references set-compr.dfy(54,30): Error: a function definition is not allowed to depend on the set of allocated references set-compr.dfy(56,28): Error: a function definition is not allowed to depend on the set of allocated references -set-compr.dfy(74,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) -set-compr.dfy(88,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +set-compr.dfy(74,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression +set-compr.dfy(88,8): Error: assignment to non-ghost variable is not allowed in this context, because the statement is in a ghost context; e.g., it may be guarded by a specification-only expression 13 resolution/type errors detected in set-compr.dfy diff --git a/Test/git-issues/git-issue-1545.dfy b/Test/git-issues/git-issue-1545.dfy new file mode 100644 index 00000000000..e9b3bf3cdfa --- /dev/null +++ b/Test/git-issues/git-issue-1545.dfy @@ -0,0 +1,9 @@ +// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +predicate Foo(s: seq) +{ + // Does not work + && (forall i :: 0 <= i < |s| ==> + && i is nat) +} \ No newline at end of file diff --git a/Test/git-issues/git-issue-1545.dfy.expect b/Test/git-issues/git-issue-1545.dfy.expect new file mode 100644 index 00000000000..6f26458f0a2 --- /dev/null +++ b/Test/git-issues/git-issue-1545.dfy.expect @@ -0,0 +1,2 @@ +git-issue-1545.dfy(8,11): Error: a non-trivial type test is allowed only for reference types (tried to test if 'int' is a 'nat') +1 resolution/type errors detected in git-issue-1545.dfy diff --git a/Test/git-issues/git-issue-663.dfy b/Test/git-issues/git-issue-663.dfy index fdec969995a..647ef80009c 100644 --- a/Test/git-issues/git-issue-663.dfy +++ b/Test/git-issues/git-issue-663.dfy @@ -271,7 +271,7 @@ newtype T = int { function method F(x: int, ghost y: int): int { 5 } function G(x: int): int { 5 } method M(x: int, ghost y: int) { } -ghost method N(x: int) { } +lemma N(x: int) { } datatype Dt = Dt(x: int, ghost y: int) diff --git a/Test/server/counterexample_commandline.dfy b/Test/server/counterexample_commandline.dfy index 498f57d72ef..fa67339bde5 100644 --- a/Test/server/counterexample_commandline.dfy +++ b/Test/server/counterexample_commandline.dfy @@ -1,4 +1,4 @@ -// RUN: %dafny /compile:0 /proverOpt:O:model_compress=false /proverOpt:O:model.completion=true /warnShadowing /extractCounterExample /errorTrace:0 /mv:%t.model "%s" > "%t" +// RUN: %dafny /compile:0 /proverOpt:O:model_compress=false /proverOpt:O:model.completion=true /warnShadowing /extractCounterexample /errorTrace:0 /mv:%t.model "%s" > "%t" // RUN: %diff "%s.expect" "%t" // The following method performs string equality comparison whereas its diff --git a/customBoogie.patch b/customBoogie.patch index 35d272f8cf1..f93291d11ac 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -1,8 +1,8 @@ diff --git a/Source/Dafny.sln b/Source/Dafny.sln -index 3cc1738d..789c04ca 100644 +index 36bb4d93..7194b644 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln -@@ -30,6 +30,30 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyTestGeneration", "Dafn +@@ -30,6 +30,34 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyTestGeneration", "Dafn EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyTestGeneration.Test", "DafnyTestGeneration.Test\DafnyTestGeneration.Test.csproj", "{896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}" EndProject @@ -29,11 +29,15 @@ index 3cc1738d..789c04ca 100644 +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Predication", "..\..\boogie\Source\Predication\Predication.csproj", "{0EDC0584-3567-43B7-AE36-1DAB91ABB2DE}" +EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SMTLib", "..\..\boogie\Source\Provers\SMTLib\SMTLib.csproj", "{0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}" ++EndProject ++Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCExpr", "..\..\boogie\Source\VCExpr\VCExpr.csproj", "{E760E37E-0257-4C96-89C4-722F85BABDBB}" ++EndProject ++Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "VCGeneration", "..\..\boogie\Source\VCGeneration\VCGeneration.csproj", "{1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|Any CPU = Debug|Any CPU -@@ -80,6 +104,64 @@ Global +@@ -80,6 +108,72 @@ Global {896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Debug|Any CPU.Build.0 = Debug|Any CPU {896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Release|Any CPU.ActiveCfg = Release|Any CPU {896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Release|Any CPU.Build.0 = Release|Any CPU @@ -95,10 +99,18 @@ index 3cc1738d..789c04ca 100644 + {0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}.Debug|Any CPU.Build.0 = Debug|Any CPU + {0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}.Release|Any CPU.ActiveCfg = Release|Any CPU + {0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F}.Release|Any CPU.Build.0 = Release|Any CPU ++ {E760E37E-0257-4C96-89C4-722F85BABDBB}.Debug|Any CPU.ActiveCfg = Debug|Any CPU ++ {E760E37E-0257-4C96-89C4-722F85BABDBB}.Debug|Any CPU.Build.0 = Debug|Any CPU ++ {E760E37E-0257-4C96-89C4-722F85BABDBB}.Release|Any CPU.ActiveCfg = Release|Any CPU ++ {E760E37E-0257-4C96-89C4-722F85BABDBB}.Release|Any CPU.Build.0 = Release|Any CPU ++ {1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}.Debug|Any CPU.ActiveCfg = Debug|Any CPU ++ {1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}.Debug|Any CPU.Build.0 = Debug|Any CPU ++ {1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}.Release|Any CPU.ActiveCfg = Release|Any CPU ++ {1EE372AA-4FF9-47FB-9C04-18CBF219F6E8}.Release|Any CPU.Build.0 = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE -@@ -75,4 +157,17 @@ Global +@@ -87,4 +181,19 @@ Global GlobalSection(ExtensibilityGlobals) = postSolution SolutionGuid = {280F572B-D27A-4613-998F-00B6FFE01187} EndGlobalSection @@ -114,10 +126,12 @@ index 3cc1738d..789c04ca 100644 + {D97C23B6-FB4A-4450-930E-58EC83D308A0} = {60332269-9C5D-465E-8582-01F9B738BD90} + {0EDC0584-3567-43B7-AE36-1DAB91ABB2DE} = {60332269-9C5D-465E-8582-01F9B738BD90} + {0EC245EE-54DD-4AE3-9C2E-34E67EE28B9F} = {60332269-9C5D-465E-8582-01F9B738BD90} ++ {E760E37E-0257-4C96-89C4-722F85BABDBB} = {60332269-9C5D-465E-8582-01F9B738BD90} ++ {1EE372AA-4FF9-47FB-9C04-18CBF219F6E8} = {60332269-9C5D-465E-8582-01F9B738BD90} + EndGlobalSection EndGlobal diff --git a/Source/Directory.Build.props b/Source/Directory.Build.props -index 4934fa8d..64a5a976 100644 +index 30e67936..64a5a976 100644 --- a/Source/Directory.Build.props +++ b/Source/Directory.Build.props @@ -7,7 +7,7 @@ diff --git a/docs/DafnyRef/Expressions.md b/docs/DafnyRef/Expressions.md index 92a7fc2d021..cbc297da35b 100644 --- a/docs/DafnyRef/Expressions.md +++ b/docs/DafnyRef/Expressions.md @@ -518,7 +518,26 @@ type `nat -> T` where `T` is the array element type: ```dafny var a := new int[5](i => i*i); ``` -TODO: what about multi-dimensional arrays + +To allocate a multi-dimensional array, simply give the sizes of +each dimension. For example, +```dafny +var m := new real[640, 480]; +``` +allocates a 640-by-480 two-dimensional array of `real`s. The initialization +portion cannot give a display of elements like in the one-dimensional +case, but it can use an initialization function. A function used to initialize +a n-dimensional array requires a function from n `nat`s to a `T`, where `T` +is element type of the array. Here is an example: +```dafny +var diag := new int[30, 30]((i, j) => if i == j then 1 else 0); +``` + +Array allocation is permitted in ghost contexts. If any expression +used to specify a dimension or initialization value is ghost, then the +`new` allocation can only be used in ghost contexts. Because the +elements of an array are non-ghost, an array allocated in a ghost +context in effect cannot be changed after initialization. ## 20.17. Object Allocation ````grammar @@ -589,7 +608,16 @@ AllocatedExpression_ = "allocated" "(" Expression(allowLemma: true, allowLambda: true) ")" ```` -TO BE WRITTEN -- allocated predicate +For any expression `e`, the expression `allocated(e)` evaluates to `true` +in a state if the value of `e` is available in that state, meaning that +it could in principle have been the value of a variable in that state. +This can be useful when, for example, `allocated(e)` is evaluated in an +`old` state. For instance, if `d` is a local variable holding a datatype value +`Cons(r, Nil)` where `r` is an object that was allocated in the enclosing +method, then `old(allocated(d))` is `false`. + +If the expression `e` is of a reference type, then `!old(allocated(e))` +is the same as `fresh(e)`. ## 20.23. Unchanged Expressions {#sec-unchanged-expression} diff --git a/docs/DafnyRef/Types.md b/docs/DafnyRef/Types.md index f2eb3887eff..1f500066cfa 100644 --- a/docs/DafnyRef/Types.md +++ b/docs/DafnyRef/Types.md @@ -1492,33 +1492,34 @@ the field `x` is shadowed by the declaration of the local variable `x`. There is no semantic difference between qualified and unqualified accesses to the same receiver and member. -A `C` instance is created using `new`, for example: +A `C` instance is created using `new`. There are three forms of `new`, +depending on whether or not the class declares any _constructors_ +(see [Section 13.3.2](#sec-constructor-methods)): + ```dafny c := new C; +c := new C.Init(args); +c := new C(args); ``` -Note that `new` simply allocates a `C` object and returns a reference -to it; the initial values of its fields are arbitrary values of their -respective types. Therefore, it is common to invoke a method, known -as an _initialization method_, immediately after creation, for -example: +For a class with no constructors, the first two forms can be used. +The first form simply allocates a new instance of a `C` object, initializing +its fields to values of their respective types (and initializing each `const` field +with a RHS to its specified value). The second form additionally invokes +an _initialization method_ (here, named `Init`) on the newly allocated object +and the given arguments. It is therefore a shorthand for ```dafny c := new C; -c.InitFromList(xs, 3); -``` -When an initialization method has no out-parameters and modifies no -more than `this`, then the two statements above can be combined into -one: -```dafny -c := new C.InitFromList(xs, 3); +c.Init(args); ``` -Note that a class can contain several initialization methods, that -these methods can be invoked at any time, not just as part of a `new`, -and that `new` does not require that an initialization method be -invoked at creation. +An initialization method is an ordinary method that has no out-parameters and +that modifies no more than `this`. -A class can declare special initializing methods called _constructor methods_. -See [Section 13.3](#sec-method-declarations). +For a class that declares one or more constructors, the second and third forms +of `new` can be used. For such a class, the second form invokes the indicated +constructor (here, named `Init`), which allocates and initializes the object. +The third form is the same as the second, but invokes the _anonymous constructor_ +of the class (that is, a constructor declared with the empty-string name). ## 13.1. Field Declarations ````grammar @@ -1711,57 +1712,79 @@ abstract under the following circumstances: Note that when there is no body, Dafny assumes that the *ensures* clauses are true without proof. (TODO: `:extern` attribute?) -### 13.3.2. Constructors +### 13.3.2. Constructors {#sec-constructor-methods} To write structured object-oriented programs, one often relies on objects being constructed only in certain ways. For this purpose, Dafny -provides _constructor (method)s_, which are a restricted form of -initialization methods. +provides _constructor (method)s_. A constructor is declared with the keyword -`constructor` instead of `method`; constructors are only permitted in classes. - -A constructor -can only be called at the time an object is allocated (see -object-creation examples below); for a class that contains one or -more constructors, object creation must be done in conjunction with a -call to a constructor. +`constructor` instead of `method`; constructors are permitted only in classes. +A constructor is allowed to be declared as `ghost`, in which case it +can only be used in ghost contexts. -When a class contains a +A constructor can only be called at the time an object is allocated (see +object-creation examples below). Moreover, when a class contains a constructor, every call to `new` for a class must be accompanied -by a call to one of its constructors. Moreover, a constructor -cannot be called at other times, only during object creation. Other -than these restrictions, there is no semantic difference between using -ordinary initialization methods and using constructors. Classes may +by a call to one of its constructors. A class may declare no constructors or one or more constructors. #### 13.3.2.1. Classes with no explicit constructors -A class that declares no constructors has a default constructor created -for it. This constructor is called with the syntax +For a class that declares no constructors, an instance of the class is +created with ```dafny c := new C; ``` -This constructor simply initializes the fields of the class. -The declaration of a const field may include an initializer, that is, a right-hand side (RHS) that specifies the constant's value. -The RHS of a const field may depend on other constant fields, but circular dependencies are not allowed. +This allocates an object and initializes its fields to values of their +respective types (and initializes each `const` field with a RHS to its specified +value). The RHS of a `const` field may depend on other `const` or `var` fields, +but circular dependencies are not allowed. -This constructor sets each class field to an arbitrary value -of the field's type if the field declaration has no initializer -and to the value of the initializer expression if it does declare an initializer. -For the purposes of proving Dafny programs -correct, assigning an arbitrary initial value means that the program must -be correct for any initial value. Compiled, executable versions of the program -may use a specific initial value -(for example, but not necessarily, a zero-equivalent or a declared _witness_ value for the type). +This simple form of `new` is allowed only if the class declares no constructors, +which is not possible to determine in every scope. +It is easy to determine whether or not a class declares any constructors if the +class is declared in the same module that performs the `new`. If the class is +declared in a different module and that module exports a constructor, then it is +also clear that the class has a constructor (and thus this simple form of `new` +cannot be used). (Note that an export set that `reveals` a class `C` also exports +the anonymous constructor of `C`, if any.) +But if the module that declares `C` does not export any constructors +for `C`, then callers outside the module do not know whether or not `C` has a +constructor. Therefore, this simple form of `new` is allowed only for classes that +are declared in the same module as the use of `new`. + +The simple `new C` is allowed in ghost contexts. Also, unlike the forms of `new` +that call a constructor or initialization method, it can be used in a simultaneous +assignment; for example +```dafny +c, d, e := new C, new C, 15; +``` +is legal. + +As a shorthand for writing +```dafny +c := new C; +c.Init(args); +``` +where `Init` is an initialization method (see the top of Section [#sec-class-types]), +one can write +```dafny +c := new C.Init(args); +``` +but it is more typical in such a case to declare a constructor for the class. + +(The syntactic support for initialization methods is provided for historical +reasons. It may be deprecated in some future version of Dafny. In most cases, +a constructor is to be preferred.) #### 13.3.2.2. Classes with one or more constructors -When one or more constructors are explicitly declared, they are named, -which promotes using names like `InitFromList` above. -Constructors must have distinct names, even if their signatures are different. -Many classes have just -one constructor or have a typical constructor. Therefore, Dafny -allows one _anonymous constructor_, that is, a constructor whose name -is essentially an empty string. For example: +Like other class members, constructors have names. And like other members, +their names must be distinct, even if their signatures are different. +Being able to name constructors promotes names like `InitFromList` or +`InitFromSet` (or just `FromList` and `FromSet`). +Unlike other members, one constructor is allowed to be _anonymous_; +in other words, an _anonymous constructor_ is a constructor whose name is +essentially the empty string. For example: ```dafny class Item { constructor I(xy: int) // ... @@ -1792,10 +1815,15 @@ a program may use `this` - as the entire RHS of an assignment to a field of `this`, - and as a member of a set on the RHS that is being assigned to a field of `this`. -Furthermore, `const` fields may only be assigned to in an initialization phase -(and may be assigned to more than once) -of their enclosing class, and then only if they do not already have an initialization -value in their declaration. +A `const` field with a RHS is not allowed to be assigned anywhere else. +A `const` field without a RHS may be assigned only in constructors, and more precisely +only in the initialization phase of constructors. During this phase, a `const` field +may be assigned more than once; whatever value the `const` field has at the end of the +initialization phase is the value it will have forever thereafter. + +For a constructor declared as `ghost`, the initialization phase is allowed to assign +both ghost and non-ghost fields. For such an object, values of non-ghost fields at +the end of the initialization phase are in effect no longer changeable. There are no restrictions on expressions or statements in the post-initialization phase. diff --git a/docs/DafnyRef/out/DafnyRef.pdf b/docs/DafnyRef/out/DafnyRef.pdf index acffc202c29..b4453c8261b 100644 Binary files a/docs/DafnyRef/out/DafnyRef.pdf and b/docs/DafnyRef/out/DafnyRef.pdf differ diff --git a/docs/OnlineTutorial/guide.md b/docs/OnlineTutorial/guide.md index 5a896573aad..30d1d5e3224 100644 --- a/docs/OnlineTutorial/guide.md +++ b/docs/OnlineTutorial/guide.md @@ -128,7 +128,7 @@ One caveat is that they always need braces around the branches, even if the branch only contains a single statement (compound or otherwise). Here the `if` statement checks whether `x` is less than zero, using the familiar comparison operator syntax, and returns the absolute value as -appropriate. (Other comparison operators are `<=`, `>`, `<=`, `!=` +appropriate. (Other comparison operators are `<=`, `>`, `>=`, `!=` and `==`, with the expected meaning. See the reference for more on operators.)