From 8a0df70ffb8d57d1bd210ce2e1c9522ba0967365 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 18 Aug 2015 18:58:40 -0700 Subject: Refactor the error reporting code The new error reporting system has a simpler interface, isn't tied to the resolver, and contains error source information. --- Source/Dafny/Reporting.cs | 164 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 164 insertions(+) create mode 100644 Source/Dafny/Reporting.cs (limited to 'Source/Dafny/Reporting.cs') diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs new file mode 100644 index 00000000..c3797574 --- /dev/null +++ b/Source/Dafny/Reporting.cs @@ -0,0 +1,164 @@ +using Microsoft.Boogie; +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using System.Text; + +namespace Microsoft.Dafny { + public enum ErrorLevel { + Info, Warning, Error + } + + public enum MessageSource { + Parser, Resolver, Translator, Rewriter, Other, + RefinementTransformer, + Cloner + } + + public struct ErrorMessage { + public IToken token; + public string message; + public MessageSource source; + } + + public abstract class ErrorReporter { + public bool ErrorsOnly { get; set; } + public Dictionary> AllMessages { get; private set; } + + protected ErrorReporter() { + ErrorsOnly = false; + AllMessages = new Dictionary>(); + AllMessages[ErrorLevel.Error] = new List(); + AllMessages[ErrorLevel.Warning] = new List(); + AllMessages[ErrorLevel.Info] = new List(); + } + + protected bool ShouldDiscard(MessageSource source, ErrorLevel level) { + return ((ErrorsOnly && level != ErrorLevel.Error) || + (!DafnyOptions.O.PrintTooltips && level == ErrorLevel.Info)); + } + + // This is the only thing that needs to be overriden + public virtual bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) { + var discard = ShouldDiscard(source, level); + + if (!discard) { + AllMessages[level].Add(new ErrorMessage { token = tok, message = msg }); + return true; + } + + return false; + } + + public int Count(ErrorLevel level) { + return AllMessages[level].Count; + } + + public void Error(MessageSource source, IToken tok, string msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); + Message(source, ErrorLevel.Error, tok, msg); + } + + // This method required by the Parser + internal void Error(MessageSource source, string filename, int line, int col, string msg) { + var tok = new Token(line, col); + tok.filename = filename; + Error(source, tok, msg); + } + + public void Error(MessageSource source, IToken tok, string msg, params object[] args) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); + Error(source, tok, String.Format(msg, args)); + } + + public void Error(MessageSource source, Declaration d, string msg, params object[] args) { + Contract.Requires(d != null); + Contract.Requires(msg != null); + Error(source, d.tok, msg, args); + } + + public void Error(MessageSource source, Statement s, string msg, params object[] args) { + Contract.Requires(s != null); + Contract.Requires(msg != null); + Error(source, s.Tok, msg, args); + } + + public void Error(MessageSource source, NonglobalVariable v, string msg, params object[] args) { + Contract.Requires(v != null); + Contract.Requires(msg != null); + Error(source, v.tok, msg, args); + } + + public void Error(MessageSource source, Expression e, string msg, params object[] args) { + Contract.Requires(e != null); + Contract.Requires(msg != null); + Error(source, e.tok, msg, args); + } + + public void Warning(MessageSource source, IToken tok, string msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); + Message(source, ErrorLevel.Warning, tok, msg); + } + + public void Warning(MessageSource source, IToken tok, string msg, params object[] args) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); + Warning(source, tok, String.Format(msg, args)); + } + + public void Info(MessageSource source, IToken tok, string msg) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); + Message(source, ErrorLevel.Info, tok, msg); + } + + public void Info(MessageSource source, IToken tok, string msg, params object[] args) { + Contract.Requires(tok != null); + Contract.Requires(msg != null); + Info(source, tok, String.Format(msg, args)); + } + + public string ErrorToString(ErrorLevel header, IToken tok, string msg) { + return ErrorToString_Internal(": " + header.ToString(), tok.filename, tok.line, tok.col, ": " + msg); + } + + public string ErrorToString(ErrorLevel header, string filename, int oneBasedLine, int oneBasedColumn, string msg) { + return ErrorToString_Internal(": " + header.ToString(), filename, oneBasedLine, oneBasedColumn, ": " + msg); + } + + public string ErrorToString_Internal(string header, string filename, int oneBasedLine, int oneBasedColumn, string msg) { + return String.Format("{0}({1},{2}){3}{4}", filename, oneBasedLine, oneBasedColumn - 1, header, msg ?? ""); + } + } + + public class ConsoleErrorReporter : ErrorReporter { + private ConsoleColor ColorForLevel(ErrorLevel level) { + switch (level) { + case ErrorLevel.Error: + return ConsoleColor.Red; + case ErrorLevel.Warning: + return ConsoleColor.Yellow; + case ErrorLevel.Info: + return ConsoleColor.Green; + default: + throw new cce.UnreachableException(); + } + } + + public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) { + if (base.Message(source, level, tok, msg)) { + ConsoleColor previousColor = Console.ForegroundColor; + Console.ForegroundColor = ColorForLevel(level); + Console.WriteLine(ErrorToString(level, tok, msg)); + Console.ForegroundColor = previousColor; + return true; + } else { + return false; + } + } + } +} -- cgit v1.2.3 From cfdaf4ccbea24636f2a94ca9d2f75b8699921d60 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 20 Aug 2015 10:28:47 -0700 Subject: Mark a few reporting functions as static --- Source/Dafny/Reporting.cs | 6 +++--- Source/Dafny/Translator.cs | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'Source/Dafny/Reporting.cs') diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index c3797574..77869d9f 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -122,15 +122,15 @@ namespace Microsoft.Dafny { Info(source, tok, String.Format(msg, args)); } - public string ErrorToString(ErrorLevel header, IToken tok, string msg) { + public static string ErrorToString(ErrorLevel header, IToken tok, string msg) { return ErrorToString_Internal(": " + header.ToString(), tok.filename, tok.line, tok.col, ": " + msg); } - public string ErrorToString(ErrorLevel header, string filename, int oneBasedLine, int oneBasedColumn, string msg) { + public static string ErrorToString(ErrorLevel header, string filename, int oneBasedLine, int oneBasedColumn, string msg) { return ErrorToString_Internal(": " + header.ToString(), filename, oneBasedLine, oneBasedColumn, ": " + msg); } - public string ErrorToString_Internal(string header, string filename, int oneBasedLine, int oneBasedColumn, string msg) { + public static string ErrorToString_Internal(string header, string filename, int oneBasedLine, int oneBasedColumn, string msg) { return String.Format("{0}({1},{2}){3}{4}", filename, oneBasedLine, oneBasedColumn - 1, header, msg ?? ""); } } diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 8146d2cf..e39b777d 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -3585,7 +3585,7 @@ namespace Microsoft.Dafny { Contract.Requires(tok != null); Contract.Ensures(Contract.Result() != null); var col = tok.col + (isEndToken ? tok.val.Length : 0); - string description = reporter.ErrorToString_Internal(additionalInfo == null ? "" : ": ", tok.filename, tok.line, tok.col, additionalInfo ?? ""); + string description = ErrorReporter.ErrorToString_Internal(additionalInfo == null ? "" : ": ", tok.filename, tok.line, tok.col, additionalInfo ?? ""); QKeyValue kv = new QKeyValue(tok, "captureState", new List() { description }, null); return new Bpl.AssumeCmd(tok, Bpl.Expr.True, kv); } -- cgit v1.2.3 From 75e436019003604ea3118a13ccd9b6ea079c643f Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 20 Aug 2015 11:52:32 -0700 Subject: Discard error messages that refer to a non-nested TokenWrapper. The VS extension already did that, but it also filtered out nested tokens. That prevented info about triggers from being reported. Other interfaces (the CLI and Emacs, in particular) should have the same ability. Surprinsingly, this doesn't cause any tests failures. --- Source/Dafny/Reporting.cs | 13 +++---------- Source/DafnyExtension/IdentifierTagger.cs | 21 ++++----------------- 2 files changed, 7 insertions(+), 27 deletions(-) (limited to 'Source/Dafny/Reporting.cs') diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 77869d9f..63ec520a 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -34,21 +34,14 @@ namespace Microsoft.Dafny { AllMessages[ErrorLevel.Info] = new List(); } - protected bool ShouldDiscard(MessageSource source, ErrorLevel level) { - return ((ErrorsOnly && level != ErrorLevel.Error) || - (!DafnyOptions.O.PrintTooltips && level == ErrorLevel.Info)); - } - // This is the only thing that needs to be overriden public virtual bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) { - var discard = ShouldDiscard(source, level); - + bool discard = (ErrorsOnly && level != ErrorLevel.Error) || // Discard non-errors if ErrorsOnly is set + (tok is TokenWrapper && !(tok is NestedToken)); // Discard wrapped tokens, except for nested ones if (!discard) { AllMessages[level].Add(new ErrorMessage { token = tok, message = msg }); - return true; } - - return false; + return !discard; } public int Count(ErrorLevel level) { diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs index 13991496..5b70329d 100644 --- a/Source/DafnyExtension/IdentifierTagger.cs +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -15,7 +15,6 @@ using Microsoft.VisualStudio.Text.Tagging; using Microsoft.VisualStudio.Utilities; using Bpl = Microsoft.Boogie; - namespace DafnyLanguage { @@ -136,8 +135,7 @@ namespace DafnyLanguage List newRegions = new List(); - foreach (var info in program.reporter.AllMessages[ErrorLevel.Info]) - { + foreach (var info in program.reporter.AllMessages[ErrorLevel.Info]) { IdRegion.Add(newRegions, info.token, info.message, info.token.val.Length); } @@ -368,11 +366,6 @@ namespace DafnyLanguage public readonly OccurrenceKind Kind; public readonly IVariable Variable; - static bool SurfaceSyntaxToken(Bpl.IToken tok) { - Contract.Requires(tok != null); - return !(tok is TokenWrapper); - } - public static void Add(List regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) { Contract.Requires(regions != null); Contract.Requires(tok != null); @@ -383,27 +376,21 @@ namespace DafnyLanguage Contract.Requires(regions != null); Contract.Requires(tok != null); Contract.Requires(v != null); - if (SurfaceSyntaxToken(tok)) { - regions.Add(new IdRegion(tok, v, isDefinition, kind, context)); - } + regions.Add(new IdRegion(tok, v, isDefinition, kind, context)); } public static void Add(List regions, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) { Contract.Requires(regions != null); Contract.Requires(tok != null); Contract.Requires(decl != null); Contract.Requires(kind != null); - if (SurfaceSyntaxToken(tok)) { - regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context)); - } + regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context)); } public static void Add(List regions, Bpl.IToken tok, string text, int length) { Contract.Requires(regions != null); Contract.Requires(tok != null); Contract.Requires(text != null); - if (SurfaceSyntaxToken(tok)) { - regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length)); - } + regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length)); } private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) { -- cgit v1.2.3 From 4b7ef1b817fe00bc32294b75797e7e264e2edbdd Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 20 Aug 2015 11:53:00 -0700 Subject: Move indentation of error messages to the ConsoleErrorReporter This indentation is just needed by CLI-based clients --- Source/Dafny/Reporting.cs | 5 ++++- Source/Dafny/Triggers/QuantifiersCollection.cs | 3 +-- 2 files changed, 5 insertions(+), 3 deletions(-) (limited to 'Source/Dafny/Reporting.cs') diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 63ec520a..4cfbf20e 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -143,7 +143,10 @@ namespace Microsoft.Dafny { } public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) { - if (base.Message(source, level, tok, msg)) { + if (base.Message(source, level, tok, msg) && (DafnyOptions.O.PrintTooltips || level != ErrorLevel.Info)) { + // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI + msg = msg.Replace(Environment.NewLine, Environment.NewLine + " "); + ConsoleColor previousColor = Console.ForegroundColor; Console.ForegroundColor = ColorForLevel(level); Console.WriteLine(ErrorToString(level, tok, msg)); diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index ec2f1777..e2afa2ee 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -171,8 +171,7 @@ namespace Microsoft.Dafny.Triggers { } if (msg.Length > 0) { - // Extra indent added to make it easier to distinguish multiline error messages - var msgStr = msg.ToString().Replace(Environment.NewLine, Environment.NewLine + " ").TrimEnd("\r\n ".ToCharArray()); + var msgStr = msg.ToString().TrimEnd("\r\n ".ToCharArray()); reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msgStr); } } -- cgit v1.2.3 From 8ede9fda35767f083899940886b69f53640891c9 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 18:59:10 -0700 Subject: Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience) Dafny now first looks for a z3 binary in z3/bin, and if it can't find one it looks for one in Binaries/z3.exe (mostly for backwards-compatibility with already set-up source installations). --- Binaries/z3 | Bin 16438468 -> 0 bytes Source/Dafny/DafnyOptions.cs | 37 ++++++++++++++++++++++++++++----- Source/Dafny/Reporting.cs | 2 +- Source/DafnyDriver/DafnyDriver.cs | 14 ++++++------- Source/DafnyServer/DafnyHelper.cs | 5 ++++- Source/DafnyServer/Utilities.cs | 4 ++-- Source/DafnyServer/VerificationTask.cs | 3 +-- 7 files changed, 47 insertions(+), 18 deletions(-) delete mode 100755 Binaries/z3 (limited to 'Source/Dafny/Reporting.cs') diff --git a/Binaries/z3 b/Binaries/z3 deleted file mode 100755 index 7c60feb4..00000000 Binary files a/Binaries/z3 and /dev/null differ diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 1986ea6d..08e53d5c 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -9,8 +9,11 @@ namespace Microsoft.Dafny { public class DafnyOptions : Bpl.CommandLineOptions { - public DafnyOptions() + private ErrorReporter errorReporter; + + public DafnyOptions(ErrorReporter errorReporter = null) : base("Dafny", "Dafny program verifier") { + this.errorReporter = errorReporter; SetZ3ExecutableName(); } @@ -257,13 +260,37 @@ namespace Microsoft.Dafny // TODO: provide attribute help here } + + /// + /// Dafny comes with it's own copy of z3, to save new users the trouble of having to install extra dependency. + /// For this to work, Dafny makes the Z3ExecutablePath point to the path were Z3 is put by our release script. + /// For developers though (and people getting this from source), it's convenient to be able to run right away, + /// so we vendor a Windows version. + /// private void SetZ3ExecutableName() { var platform = (int)System.Environment.OSVersion.Platform; - var isLinux = platform == 4 || platform == 128; // http://www.mono-project.com/docs/faq/technical/ - //TODO should we also vendor an OSX build? - var binDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location); - Z3ExecutablePath = System.IO.Path.Combine(binDir, isLinux ? "z3" : "z3.exe"); + // http://www.mono-project.com/docs/faq/technical/ + var isUnix = platform == 4 || platform == 128; + + var z3binName = isUnix ? "z3" : "z3.exe"; + var dafnyBinDir = System.IO.Path.GetDirectoryName(System.Reflection.Assembly.GetExecutingAssembly().Location); + var z3BinDir = System.IO.Path.Combine(dafnyBinDir, "z3", "bin"); + var z3BinPath = System.IO.Path.Combine(z3BinDir, z3binName); + + if (!System.IO.File.Exists(z3BinPath) && !isUnix) { + // This is most likely a Windows user running from source without downloading z3 + // separately; this is ok, since we vendor z3.exe. + z3BinPath = System.IO.Path.Combine(dafnyBinDir, z3binName); + } + + if (!System.IO.File.Exists(z3BinPath) && errorReporter != null) { + var tok = new Bpl.Token(1, 1) { filename = "*** " }; + errorReporter.Warning(MessageSource.Other, tok, "Could not find '{0}' in '{1}'.{2}Downloading and extracting a Z3 distribution to Dafny's 'Binaries' folder would solve this issue; for now, we'll rely on Boogie to find Z3.", + z3binName, z3BinDir, System.Environment.NewLine); + } else { + Z3ExecutablePath = z3BinPath; + } } public override void Usage() { diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 4cfbf20e..760392ca 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -143,7 +143,7 @@ namespace Microsoft.Dafny { } public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) { - if (base.Message(source, level, tok, msg) && (DafnyOptions.O.PrintTooltips || level != ErrorLevel.Info)) { + if (base.Message(source, level, tok, msg) && ((DafnyOptions.O != null && DafnyOptions.O.PrintTooltips) || level != ErrorLevel.Info)) { // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI msg = msg.Replace(Environment.NewLine, Environment.NewLine + " "); diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 4b5ae8d8..c45d66fc 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -40,10 +40,11 @@ namespace Microsoft.Dafny public static int ThreadMain(string[] args) { Contract.Requires(cce.NonNullElements(args)); - + + ErrorReporter reporter = new ConsoleErrorReporter(); ExecutionEngine.printer = new DafnyConsolePrinter(); // For boogie errors - DafnyOptions.Install(new DafnyOptions()); + DafnyOptions.Install(new DafnyOptions(reporter)); ExitValue exitValue = ExitValue.VERIFIED; CommandLineOptions.Clo.RunningBoogieFromCommandLine = true; @@ -92,7 +93,7 @@ namespace Microsoft.Dafny goto END; } } - exitValue = ProcessFiles(CommandLineOptions.Clo.Files); + exitValue = ProcessFiles(CommandLineOptions.Clo.Files, reporter); END: if (CommandLineOptions.Clo.XmlSink != null) { @@ -112,7 +113,7 @@ namespace Microsoft.Dafny } - static ExitValue ProcessFiles(IList/*!*/ fileNames, bool lookForSnapshots = true, string programId = null) + static ExitValue ProcessFiles(IList/*!*/ fileNames, ErrorReporter reporter, bool lookForSnapshots = true, string programId = null) { Contract.Requires(cce.NonNullElements(fileNames)); @@ -128,7 +129,7 @@ namespace Microsoft.Dafny { Console.WriteLine(); Console.WriteLine("-------------------- {0} --------------------", f); - var ev = ProcessFiles(new List { f }, lookForSnapshots, f); + var ev = ProcessFiles(new List { f }, reporter, lookForSnapshots, f); if (exitValue != ev && ev != ExitValue.VERIFIED) { exitValue = ev; @@ -142,7 +143,7 @@ namespace Microsoft.Dafny var snapshotsByVersion = ExecutionEngine.LookForSnapshots(fileNames); foreach (var s in snapshotsByVersion) { - var ev = ProcessFiles(new List(s), false, programId); + var ev = ProcessFiles(new List(s), reporter, false, programId); if (exitValue != ev && ev != ExitValue.VERIFIED) { exitValue = ev; @@ -153,7 +154,6 @@ namespace Microsoft.Dafny using (XmlFileScope xf = new XmlFileScope(CommandLineOptions.Clo.XmlSink, fileNames[fileNames.Count-1])) { Dafny.Program dafnyProgram; - ErrorReporter reporter = new ConsoleErrorReporter(); string programName = fileNames.Count == 1 ? fileNames[0] : "the program"; string err = Dafny.Main.ParseCheck(fileNames, programName, reporter, out dafnyProgram); if (err != null) { diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 3204fdb3..e54e2b48 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -29,18 +29,21 @@ namespace Microsoft.Dafny { class DafnyHelper { private string fname; private string source; + private string[] args; private readonly Dafny.ErrorReporter reporter; private Dafny.Program dafnyProgram; private Bpl.Program boogieProgram; - public DafnyHelper(string fname, string source) { + public DafnyHelper(string[] args, string fname, string source) { + this.args = args; this.fname = fname; this.source = source; this.reporter = new Dafny.ConsoleErrorReporter(); } public bool Verify() { + ServerUtils.ApplyArgs(args, reporter); return Parse() && Resolve() && Translate() && Boogie(); } diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index 59b3abb9..5e2c6f96 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -43,8 +43,8 @@ namespace Microsoft.Dafny { } } - internal static void ApplyArgs(string[] args) { - Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); + internal static void ApplyArgs(string[] args, ErrorReporter reporter) { + Dafny.DafnyOptions.Install(new Dafny.DafnyOptions(reporter)); Dafny.DafnyOptions.O.ProverKillTime = 15; //This is just a default; it can be overriden if (CommandLineOptions.Clo.Parse(args)) { diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs index a00688b1..eb740e70 100644 --- a/Source/DafnyServer/VerificationTask.cs +++ b/Source/DafnyServer/VerificationTask.cs @@ -52,8 +52,7 @@ namespace Microsoft.Dafny { } internal void Run() { - ServerUtils.ApplyArgs(args); - new DafnyHelper(filename, ProgramSource).Verify(); + new DafnyHelper(args, filename, ProgramSource).Verify(); } } } -- cgit v1.2.3 From 74d1631a4724739dbb897c74713f54c4d060e781 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 5 Feb 2016 15:18:29 -0800 Subject: Fix issue 125. Add the missing case 2 and 3 with refinement and opened imports. For the following situation module LibA { // ...things declared here... } MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit module LibB { // ...things declared here... } module R { import opened LibA // ...things declared here... } module S refines R { import opened LibB // ...declared here... } 1. If module R declares a TopLevelDecl “G”, then we should report an error if S attempts to declare an incompatible TopLevelDecl “G”. Dafny does this already. 2. If LibA declares a TopLevelDecl “G” but R does not directly declare any TopLevelDecl G”, then we should also issue an error for any TopLevelDecl “G” in S. This behavior is missing in Dafny. 3. If each of LibA and LibB declares some TopLevelDecl “G”, but neither R nor S directly declares any TopLevelDecl “G”, then no error should be issued, and any use of “G” in S should resolve to the “G” in LibA. This behavior is missing in Dafny. --- Source/Dafny/Cloner.cs | 5 +- Source/Dafny/DafnyAst.cs | 15 +++ Source/Dafny/RefinementTransformer.cs | 174 +++++++++++++++++++--------------- Source/Dafny/Reporting.cs | 2 +- Source/Dafny/Resolver.cs | 11 +++ Test/dafny0/Modules0.dfy | 12 +++ Test/dafny0/Modules0.dfy.expect | 3 +- Test/dafny4/Bug125.dfy | 82 ++++++++++++++++ Test/dafny4/Bug125.dfy.expect | 2 + 9 files changed, 225 insertions(+), 81 deletions(-) create mode 100644 Test/dafny4/Bug125.dfy create mode 100644 Test/dafny4/Bug125.dfy.expect (limited to 'Source/Dafny/Reporting.cs') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 8971d2c1..6d5e2961 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -23,7 +23,10 @@ namespace Microsoft.Dafny nw.TopLevelDecls.Add(CloneDeclaration(d, nw)); } if (null != m.RefinementBase) { - nw.RefinementBase = m.RefinementBase; + nw.RefinementBase = m.RefinementBase; + } + if (null != m.RefinementBaseSig) { + nw.RefinementBaseSig = m.RefinementBaseSig; } nw.ClonedFrom = m; nw.Height = m.Height; diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 33186a76..0e4c4751 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1823,6 +1823,21 @@ namespace Microsoft.Dafny { public int ExclusiveRefinementCount { get; set; } + private ModuleSignature refinementBaseSig; // module signature of the refinementBase. + public ModuleSignature RefinementBaseSig { + get { + return refinementBaseSig; + } + + set { + // the refinementBase member may only be changed once. + if (null != refinementBaseSig) { + throw new InvalidOperationException(string.Format("This module ({0}) already has a refinement base ({1}).", Name, refinementBase.Name)); + } + refinementBaseSig = value; + } + } + private ModuleDefinition refinementBase; // filled in during resolution via RefinementBase property (null if no refinement base yet or at all). public ModuleDefinition RefinementBase { diff --git a/Source/Dafny/RefinementTransformer.cs b/Source/Dafny/RefinementTransformer.cs index 6281417d..a243ad53 100644 --- a/Source/Dafny/RefinementTransformer.cs +++ b/Source/Dafny/RefinementTransformer.cs @@ -141,99 +141,117 @@ namespace Microsoft.Dafny } // Merge the declarations of prev into the declarations of m + List processedDecl = new List(); foreach (var d in prev.TopLevelDecls) { int index; + processedDecl.Add(d.Name); if (!declaredNames.TryGetValue(d.Name, out index)) { m.TopLevelDecls.Add(refinementCloner.CloneDeclaration(d, m)); } else { var nw = m.TopLevelDecls[index]; - if (d is ModuleDecl) { - if (!(nw is ModuleDecl)) { - reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name); - } else if (!(d is ModuleFacadeDecl)) { - reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only refine a module facade", nw.Name); - } else { - ModuleSignature original = ((ModuleFacadeDecl)d).OriginalSignature; - ModuleSignature derived = null; - if (nw is AliasModuleDecl) { - derived = ((AliasModuleDecl)nw).Signature; - } else if (nw is ModuleFacadeDecl) { - derived = ((ModuleFacadeDecl)nw).Signature; - } else { - reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only be refined by an alias module or a module facade", d.Name); + MergeTopLevelDecls(m, nw, d, index); + } + } + + // Merge the imports of prev + var prevTopLevelDecls = RefinedSig.TopLevels.Values; + foreach (var d in prevTopLevelDecls) { + int index; + if (!processedDecl.Contains(d.Name) && (declaredNames.TryGetValue(d.Name, out index))) { + // if it is redefined, we need to merge them. + var nw = m.TopLevelDecls[index]; + MergeTopLevelDecls(m, nw, d, index); + } + } + m.RefinementBaseSig = RefinedSig; + + Contract.Assert(moduleUnderConstruction == m); // this should be as it was set earlier in this method + } + + private void MergeTopLevelDecls(ModuleDefinition m, TopLevelDecl nw, TopLevelDecl d, int index) { + if (d is ModuleDecl) { + if (!(nw is ModuleDecl)) { + reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name); + } else if (!(d is ModuleFacadeDecl)) { + reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only refine a module facade", nw.Name); + } else { + ModuleSignature original = ((ModuleFacadeDecl)d).OriginalSignature; + ModuleSignature derived = null; + if (nw is AliasModuleDecl) { + derived = ((AliasModuleDecl)nw).Signature; + } else if (nw is ModuleFacadeDecl) { + derived = ((ModuleFacadeDecl)nw).Signature; + } else { + reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) can only be refined by an alias module or a module facade", d.Name); + } + if (derived != null) { + // check that the new module refines the previous declaration + if (!CheckIsRefinement(derived, original)) + reporter.Error(MessageSource.RefinementTransformer, nw.tok, "a module ({0}) can only be replaced by a refinement of the original module", d.Name); + } + } + } else if (d is OpaqueTypeDecl) { + if (nw is ModuleDecl) { + reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name); + } else { + bool dDemandsEqualitySupport = ((OpaqueTypeDecl)d).MustSupportEquality; + if (nw is OpaqueTypeDecl) { + if (dDemandsEqualitySupport != ((OpaqueTypeDecl)nw).MustSupportEquality) { + reporter.Error(MessageSource.RefinementTransformer, nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name); + } + if (nw.TypeArgs.Count != d.TypeArgs.Count) { + reporter.Error(MessageSource.RefinementTransformer, nw, "type '{0}' is not allowed to change its number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count); + } + } else if (dDemandsEqualitySupport) { + if (nw is ClassDecl) { + // fine, as long as "nw" takes the right number of type parameters + if (nw.TypeArgs.Count != d.TypeArgs.Count) { + reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count); } - if (derived != null) { - // check that the new module refines the previous declaration - if (!CheckIsRefinement(derived, original)) - reporter.Error(MessageSource.RefinementTransformer, nw.tok, "a module ({0}) can only be replaced by a refinement of the original module", d.Name); + } else if (nw is NewtypeDecl) { + // fine, as long as "nw" does not take any type parameters + if (nw.TypeArgs.Count != 0) { + reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a newtype, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s"); } - } - } else if (d is OpaqueTypeDecl) { - if (nw is ModuleDecl) { - reporter.Error(MessageSource.RefinementTransformer, nw, "a module ({0}) must refine another module", nw.Name); + } else if (nw is CoDatatypeDecl) { + reporter.Error(MessageSource.RefinementTransformer, nw, "a type declaration that requires equality support cannot be replaced by a codatatype"); } else { - bool dDemandsEqualitySupport = ((OpaqueTypeDecl)d).MustSupportEquality; - if (nw is OpaqueTypeDecl) { - if (dDemandsEqualitySupport != ((OpaqueTypeDecl)nw).MustSupportEquality) { - reporter.Error(MessageSource.RefinementTransformer, nw, "type declaration '{0}' is not allowed to change the requirement of supporting equality", nw.Name); - } - if (nw.TypeArgs.Count != d.TypeArgs.Count) { - reporter.Error(MessageSource.RefinementTransformer, nw, "type '{0}' is not allowed to change its number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count); - } - } else if (dDemandsEqualitySupport) { - if (nw is ClassDecl) { - // fine, as long as "nw" takes the right number of type parameters - if (nw.TypeArgs.Count != d.TypeArgs.Count) { - reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a class that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count); - } - } else if (nw is NewtypeDecl) { - // fine, as long as "nw" does not take any type parameters - if (nw.TypeArgs.Count != 0) { - reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}', which has {1} type argument{2}, is not allowed to be replaced by a newtype, which takes none", nw.Name, d.TypeArgs.Count, d.TypeArgs.Count == 1 ? "" : "s"); - } - } else if (nw is CoDatatypeDecl) { - reporter.Error(MessageSource.RefinementTransformer, nw, "a type declaration that requires equality support cannot be replaced by a codatatype"); - } else { - Contract.Assert(nw is IndDatatypeDecl || nw is TypeSynonymDecl); - if (nw.TypeArgs.Count != d.TypeArgs.Count) { - reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count); - } else { - // Here, we need to figure out if the new type supports equality. But we won't know about that until resolution has - // taken place, so we defer it until the PostResolve phase. - var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw); - postTasks.Enqueue(() => { - if (!udt.SupportsEquality) { - reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}' is used to refine an opaque type with equality support, but '{0}' does not support equality", udt.Name); - } - }); - } - } - } else if (d.TypeArgs.Count != nw.TypeArgs.Count) { + Contract.Assert(nw is IndDatatypeDecl || nw is TypeSynonymDecl); + if (nw.TypeArgs.Count != d.TypeArgs.Count) { reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count); + } else { + // Here, we need to figure out if the new type supports equality. But we won't know about that until resolution has + // taken place, so we defer it until the PostResolve phase. + var udt = UserDefinedType.FromTopLevelDecl(nw.tok, nw); + postTasks.Enqueue(() => { + if (!udt.SupportsEquality) { + reporter.Error(MessageSource.RefinementTransformer, udt.tok, "type '{0}' is used to refine an opaque type with equality support, but '{0}' does not support equality", udt.Name); + } + }); } } - } else if (nw is OpaqueTypeDecl) { - reporter.Error(MessageSource.RefinementTransformer, nw, "an opaque type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name); - } else if (nw is DatatypeDecl) { - reporter.Error(MessageSource.RefinementTransformer, nw, "a datatype declaration ({0}) in a refinement module can only replace an opaque type declaration", nw.Name); - } else if (nw is IteratorDecl) { - if (d is IteratorDecl) { - m.TopLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d); - } else { - reporter.Error(MessageSource.RefinementTransformer, nw, "an iterator declaration ({0}) is a refining module cannot replace a different kind of declaration in the refinement base", nw.Name); - } - } else { - Contract.Assert(nw is ClassDecl); - if (d is DatatypeDecl) { - reporter.Error(MessageSource.RefinementTransformer, nw, "a class declaration ({0}) in a refining module cannot replace a different kind of declaration in the refinement base", nw.Name); - } else { - m.TopLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d); - } + } else if (d.TypeArgs.Count != nw.TypeArgs.Count) { + reporter.Error(MessageSource.RefinementTransformer, nw, "opaque type '{0}' is not allowed to be replaced by a type that takes a different number of type parameters (got {1}, expected {2})", nw.Name, nw.TypeArgs.Count, d.TypeArgs.Count); } } + } else if (nw is OpaqueTypeDecl) { + reporter.Error(MessageSource.RefinementTransformer, nw, "an opaque type declaration ({0}) in a refining module cannot replace a more specific type declaration in the refinement base", nw.Name); + } else if (nw is DatatypeDecl) { + reporter.Error(MessageSource.RefinementTransformer, nw, "a datatype declaration ({0}) in a refinement module can only replace an opaque type declaration", nw.Name); + } else if (nw is IteratorDecl) { + if (d is IteratorDecl) { + m.TopLevelDecls[index] = MergeIterator((IteratorDecl)nw, (IteratorDecl)d); + } else { + reporter.Error(MessageSource.RefinementTransformer, nw, "an iterator declaration ({0}) is a refining module cannot replace a different kind of declaration in the refinement base", nw.Name); + } + } else { + Contract.Assert(nw is ClassDecl); + if (d is DatatypeDecl) { + reporter.Error(MessageSource.RefinementTransformer, nw, "a class declaration ({0}) in a refining module cannot replace a different kind of declaration in the refinement base", nw.Name); + } else { + m.TopLevelDecls[index] = MergeClass((ClassDecl)nw, (ClassDecl)d); + } } - - Contract.Assert(moduleUnderConstruction == m); // this should be as it was set earlier in this method } public bool CheckIsRefinement(ModuleSignature derived, ModuleSignature original) { diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 760392ca..b36efc55 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -37,7 +37,7 @@ namespace Microsoft.Dafny { // This is the only thing that needs to be overriden public virtual bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) { bool discard = (ErrorsOnly && level != ErrorLevel.Error) || // Discard non-errors if ErrorsOnly is set - (tok is TokenWrapper && !(tok is NestedToken)); // Discard wrapped tokens, except for nested ones + (tok is TokenWrapper && !(tok is NestedToken) && !(tok is RefinementToken)); // Discard wrapped tokens, except for nested and refinement if (!discard) { AllMessages[level].Add(new ErrorMessage { token = tok, message = msg }); } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index e47220d7..99b31923 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1103,6 +1103,17 @@ namespace Microsoft.Dafny } } } + + // second go through and overriding anything from the opened imports with the ones from the refinementBase + if (useImports && moduleDef.RefinementBaseSig != null) { + foreach (var kv in moduleDef.RefinementBaseSig.TopLevels) { + sig.TopLevels[kv.Key] = kv.Value; + } + foreach (var kv in moduleDef.RefinementBaseSig.StaticMembers) { + sig.StaticMembers[kv.Key] = kv.Value; + } + } + // This is solely used to detect duplicates amongst the various e Dictionary toplevels = new Dictionary(); // Now add the things present diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index dbbffd87..4b86d848 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -335,3 +335,15 @@ module TopLevelStatics { static method M() // error/warning: static keyword does not belong here { } } + +module Library { + class T { } +} + +module AA { + import opened Library +} + +module B refines AA { + datatype T = MakeT(int) // illegal +} diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index e4b46cce..f51e0f6c 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -30,5 +30,6 @@ Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon' Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List) Modules0.dfy(324,30): Error: member Create does not exist in class Klassy +Modules0.dfy(348,11): Error: a datatype declaration (T) in a refinement module can only replace an opaque type declaration Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name or declare a module import 'opened?') -31 resolution/type errors detected in Modules0.dfy +32 resolution/type errors detected in Modules0.dfy diff --git a/Test/dafny4/Bug125.dfy b/Test/dafny4/Bug125.dfy new file mode 100644 index 00000000..916dd3f8 --- /dev/null +++ b/Test/dafny4/Bug125.dfy @@ -0,0 +1,82 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +abstract module AbstractModuleA +{ + type T +} + +abstract module AbstractModuleB +{ + import opened AMA : AbstractModuleA + + method Foo(t:T) +} + +abstract module AbstractModuleC refines AbstractModuleB +{ + import opened AMA2 : AbstractModuleA +} + +module LibA { + class G { + static function f(x:int) : bool { + x >= 10 + } + } + + function g() : bool { + true + } +} + +module LibB { + class G { + static function f(x:int) : bool { + x < 10 + } + } + + function g() : bool { + false + } +} + +module R { + import opened LibA +} + +module S refines R { + import opened LibB + method m() { + assert g(); // should be LibA.g + } + + method m1() { + assert G.f(20); // should be LibA.G.f + } +} + + +module Library { + + class T { } + +} + + + +module A { + + import opened Library + class T { + } +} + + + +module B refines A { + + datatype T = MakeT(int) // illegal for the same reason as above, but Dafny fails to issue an error + +} diff --git a/Test/dafny4/Bug125.dfy.expect b/Test/dafny4/Bug125.dfy.expect new file mode 100644 index 00000000..c87e2af2 --- /dev/null +++ b/Test/dafny4/Bug125.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 10 verified, 0 errors -- cgit v1.2.3