From 990966db7dcea00045c5c104ded084348e8f7dde Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 31 Jul 2015 14:26:53 -0700 Subject: Split the server source into multiple files --- Source/DafnyServer/DafnyHelper.cs | 87 ++++++++++++++ Source/DafnyServer/DafnyServer.csproj | 7 +- Source/DafnyServer/Server.cs | 202 +++------------------------------ Source/DafnyServer/Utilities.cs | 60 ++++++++++ Source/DafnyServer/VerificationTask.cs | 59 ++++++++++ 5 files changed, 227 insertions(+), 188 deletions(-) create mode 100644 Source/DafnyServer/DafnyHelper.cs create mode 100644 Source/DafnyServer/Utilities.cs create mode 100644 Source/DafnyServer/VerificationTask.cs (limited to 'Source/DafnyServer') diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs new file mode 100644 index 00000000..10d98677 --- /dev/null +++ b/Source/DafnyServer/DafnyHelper.cs @@ -0,0 +1,87 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Text; +using System.Threading.Tasks; +using Microsoft.Boogie; +using Bpl = Microsoft.Boogie; + +namespace Microsoft.Dafny { + // FIXME: This should not be duplicated here + class DafnyConsolePrinter : ConsolePrinter { + public override void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) { + // Dafny has 0-indexed columns, but Boogie counts from 1 + var realigned_tok = new Token(tok.line, tok.col - 1); + realigned_tok.kind = tok.kind; + realigned_tok.pos = tok.pos; + realigned_tok.val = tok.val; + realigned_tok.filename = tok.filename; + base.ReportBplError(realigned_tok, message, error, tw, category); + + if (tok is Dafny.NestedToken) { + var nt = (Dafny.NestedToken)tok; + ReportBplError(nt.Inner, "Related location", false, tw); + } + } + } + + class DafnyHelper { + private string fname; + private string source; + + private Dafny.Errors errors; + private Dafny.Program dafnyProgram; + private Bpl.Program boogieProgram; + + public DafnyHelper(string fname, string source) { + this.fname = fname; + this.source = source; + this.errors = new Dafny.Errors(); + } + + public bool Verify() { + return Parse() && Resolve() && Translate() && Boogie(); + } + + private bool Parse() { + Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null); + Dafny.BuiltIns builtIns = new Dafny.BuiltIns(); + var success = (Dafny.Parser.Parse(source, fname, fname, module, builtIns, errors) == 0 && + Dafny.Main.ParseIncludes(module, builtIns, new List(), errors) == null); + if (success) { + dafnyProgram = new Dafny.Program(fname, module, builtIns); + } + return success; + } + + private bool Resolve() { + var resolver = new Dafny.Resolver(dafnyProgram); + resolver.ResolveProgram(dafnyProgram); + return resolver.ErrorCount == 0; + } + + private bool Translate() { + var translator = new Dafny.Translator() { InsertChecksums = true, UniqueIdPrefix = null }; //FIXME check if null is OK for UniqueIdPrefix + boogieProgram = translator.Translate(dafnyProgram); // FIXME how are translation errors reported? + return true; + } + + private bool Boogie() { + if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { //FIXME ResolveAndTypecheck? + ExecutionEngine.EliminateDeadVariables(boogieProgram); + ExecutionEngine.CollectModSets(boogieProgram); + ExecutionEngine.CoalesceBlocks(boogieProgram); + ExecutionEngine.Inline(boogieProgram); + + switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) { // FIXME check if null is ok for error delegate + case PipelineOutcome.Done: + case PipelineOutcome.VerificationCompleted: + return true; + } + } + + return false; + } + } +} diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj index 0aac88b2..3da33f16 100644 --- a/Source/DafnyServer/DafnyServer.csproj +++ b/Source/DafnyServer/DafnyServer.csproj @@ -1,4 +1,4 @@ - + @@ -55,6 +55,9 @@ + + + @@ -72,4 +75,4 @@ --> - + \ No newline at end of file diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index 660188ba..c6f619d3 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -10,116 +10,21 @@ using Bpl = Microsoft.Boogie; using Microsoft.Boogie; namespace Microsoft.Dafny { - class Interaction { - internal static string SUCCESS = "SUCCESS"; - internal static string FAILURE = "FAILURE"; - internal static string SERVER_EOM_TAG = "[[DAFNY-SERVER: EOM]]"; - internal static string CLIENT_EOM_TAG = "[[DAFNY-CLIENT: EOM]]"; - - internal static void EOM(string header, string msg) { - var trailer = (msg == null) ? "" : "\n"; - Console.Write("{0}{1}[{2}] {3}\n", msg ?? "", trailer, header, SERVER_EOM_TAG); - Console.Out.Flush(); - } - - internal static void EOM(string header, Exception ex, string subHeader="") { - var aggregate = ex as AggregateException; - subHeader = String.IsNullOrEmpty(subHeader) ? "" : subHeader + " "; - - if (aggregate == null) { - EOM(header, subHeader + ex.Message); - } else { - EOM(header, subHeader + aggregate.InnerExceptions.MapConcat(exn => exn.Message, ", ")); - } - } - } - - // FIXME: This should not be duplicated here - class DafnyConsolePrinter : ConsolePrinter { - public override void ReportBplError(IToken tok, string message, bool error, TextWriter tw, string category = null) { - // Dafny has 0-indexed columns, but Boogie counts from 1 - var realigned_tok = new Token(tok.line, tok.col - 1); - realigned_tok.kind = tok.kind; - realigned_tok.pos = tok.pos; - realigned_tok.val = tok.val; - realigned_tok.filename = tok.filename; - base.ReportBplError(realigned_tok, message, error, tw, category); - - if (tok is Dafny.NestedToken) { - var nt = (Dafny.NestedToken)tok; - ReportBplError(nt.Inner, "Related location", false, tw); - } - } - } - - [Serializable] - class VerificationTask { - [DataMember] - string[] args = null; - - [DataMember] - string filename = null; - - [DataMember] - string source = null; - - [DataMember] - bool sourceIsFile = false; - - string ProgramSource { get { return sourceIsFile ? File.ReadAllText(source) : source; } } - - internal static VerificationTask ReadTask(string b64_repr) { - try { - var json = Encoding.UTF8.GetString(System.Convert.FromBase64String(b64_repr)); - using (MemoryStream ms = new MemoryStream(Encoding.Unicode.GetBytes(json))) { - DataContractJsonSerializer serializer = new DataContractJsonSerializer(typeof(VerificationTask)); - return (VerificationTask)serializer.ReadObject(ms); - } - } catch (Exception ex) { - throw new ServerException("Deserialization failed: {0}.", ex.Message); - } - } - - internal static void SelfTest() { - var task = new VerificationTask() { - filename = "", - sourceIsFile = false, - args = new string[] { }, - source = "method selftest() { assert true; }" - }; - try { - task.Run(); - Interaction.EOM(Interaction.SUCCESS, null); - } catch (Exception ex) { - Interaction.EOM(Interaction.FAILURE, ex); - } - } - - internal void Run() { - Server.ApplyArgs(args); - new DafnyHelper(filename, ProgramSource).Verify(); - } - } - - class ServerException : Exception { - internal ServerException(string message) : base(message) { } - internal ServerException(string message, params object[] args) : base(String.Format(message, args)) { } - } - class Server { private bool running; static void Main(string[] args) { Server server = new Server(); - if (args.Length > 0) { - if (args[0] == "selftest") { - VerificationTask.SelfTest(); - } else if (File.Exists(args[0])) { - Console.SetIn(new StreamReader(args[0])); - server.Loop(); - } else { - Console.WriteLine("Not sure what to do with '{0}'", String.Join(" ", args)); - } + + var hasArg = args.Length > 0; + var arg = hasArg ? args[0] : null; + + if (hasArg && args[0] == "selftest") { + VerificationTask.SelfTest(); + } else if (hasArg && File.Exists(arg)) { + Console.WriteLine("# Reading from {0}", arg); + Console.SetIn(new StreamReader(arg)); + server.Loop(); } else { server.Loop(); } @@ -131,19 +36,6 @@ namespace Microsoft.Dafny { ExecutionEngine.printer = new DafnyConsolePrinter(); } - internal static void ApplyArgs(string[] args) { - Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); - if (CommandLineOptions.Clo.Parse(args)) { - // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME - // Dafny.DafnyOptions.O.ModelViewFile = "-"; - Dafny.DafnyOptions.O.ProverKillTime = 10; - Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); - Dafny.DafnyOptions.O.VerifySnapshots = 2; - } else { - throw new ServerException("Invalid command line options"); - } - } - void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { e.Cancel = true; // FIXME TerminateProver and RunningProverFromCommandLine @@ -167,8 +59,10 @@ namespace Microsoft.Dafny { void Loop() { for (int cycle = 0; running; cycle++) { var line = Console.ReadLine() ?? "quit"; - var command = line.Split(); - Respond(command); + if (line != String.Empty && !line.StartsWith("#")) { + var command = line.Split(); + Respond(command); + } } } @@ -180,11 +74,11 @@ namespace Microsoft.Dafny { var verb = command[0]; if (verb == "verify") { - checkArgs(command, 0); + ServerUtils.checkArgs(command, 0); var payload = ReadPayload(); VerificationTask.ReadTask(payload).Run(); } else if (verb == "quit") { - checkArgs(command, 0); + ServerUtils.checkArgs(command, 0); Exit(); } else { throw new ServerException("Unknown verb '{0}'", verb); @@ -199,73 +93,9 @@ namespace Microsoft.Dafny { } } - void checkArgs(string[] command, int expectedLength) { - if (command.Length - 1 != expectedLength) { - throw new ServerException("Invalid argument count (got {0}, expected {1})", command.Length - 1, expectedLength); - } - } - void Exit() { this.running = false; } } - class DafnyHelper { - private string fname; - private string source; - - private Dafny.Errors errors; - private Dafny.Program dafnyProgram; - private Bpl.Program boogieProgram; - - public DafnyHelper(string fname, string source) { - this.fname = fname; - this.source = source; - this.errors = new Dafny.Errors(); - } - - public bool Verify() { - return Parse() && Resolve() && Translate() && Boogie(); - } - - private bool Parse() { - Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null); - Dafny.BuiltIns builtIns = new Dafny.BuiltIns(); - var success = (Dafny.Parser.Parse(source, fname, fname, module, builtIns, errors) == 0 && - Dafny.Main.ParseIncludes(module, builtIns, new List(), errors) == null); - if (success) { - dafnyProgram = new Dafny.Program(fname, module, builtIns); - } - return success; - } - - private bool Resolve() { - var resolver = new Dafny.Resolver(dafnyProgram); - resolver.ResolveProgram(dafnyProgram); - return resolver.ErrorCount == 0; - } - - private bool Translate() { - var translator = new Dafny.Translator() { InsertChecksums = true, UniqueIdPrefix = null }; //FIXME check if null is OK for UniqueIdPrefix - boogieProgram = translator.Translate(dafnyProgram); // FIXME how are translation errors reported? - return true; - } - - private bool Boogie() { - if (boogieProgram.Resolve() == 0 && boogieProgram.Typecheck() == 0) { //FIXME ResolveAndTypecheck? - ExecutionEngine.EliminateDeadVariables(boogieProgram); - ExecutionEngine.CollectModSets(boogieProgram); - ExecutionEngine.CoalesceBlocks(boogieProgram); - ExecutionEngine.Inline(boogieProgram); - - switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) { // FIXME check if null is ok for error delegate - case PipelineOutcome.Done: - case PipelineOutcome.VerificationCompleted: - return true; - } - } - - return false; - } - } } \ No newline at end of file diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs new file mode 100644 index 00000000..8fb03b05 --- /dev/null +++ b/Source/DafnyServer/Utilities.cs @@ -0,0 +1,60 @@ +using System; +using System.IO; +using System.Text; +using System.Collections.Generic; +using System.Runtime.Serialization; +using System.Runtime.Serialization.Json; +using Microsoft.Boogie; + +namespace Microsoft.Dafny { + class Interaction { + internal static string SUCCESS = "SUCCESS"; + internal static string FAILURE = "FAILURE"; + internal static string SERVER_EOM_TAG = "[[DAFNY-SERVER: EOM]]"; + internal static string CLIENT_EOM_TAG = "[[DAFNY-CLIENT: EOM]]"; + + internal static void EOM(string header, string msg) { + var trailer = (msg == null) ? "" : "\n"; + Console.Write("{0}{1}[{2}] {3}\n", msg ?? "", trailer, header, SERVER_EOM_TAG); + Console.Out.Flush(); + } + + internal static void EOM(string header, Exception ex, string subHeader = "") { + var aggregate = ex as AggregateException; + subHeader = String.IsNullOrEmpty(subHeader) ? "" : subHeader + " "; + + if (aggregate == null) { + EOM(header, subHeader + ex.Message); + } else { + EOM(header, subHeader + aggregate.InnerExceptions.MapConcat(exn => exn.Message, ", ")); + } + } + } + + class ServerException : Exception { + internal ServerException(string message) : base(message) { } + internal ServerException(string message, params object[] args) : base(String.Format(message, args)) { } + } + + class ServerUtils { + internal static void checkArgs(string[] command, int expectedLength) { + if (command.Length - 1 != expectedLength) { + throw new ServerException("Invalid argument count (got {0}, expected {1})", command.Length - 1, expectedLength); + } + } + + internal static void ApplyArgs(string[] args) { + Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); + + if (CommandLineOptions.Clo.Parse(args)) { + // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME + // Dafny.DafnyOptions.O.ModelViewFile = "-"; + Dafny.DafnyOptions.O.ProverKillTime = 10; + Dafny.DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); + Dafny.DafnyOptions.O.VerifySnapshots = 2; + } else { + throw new ServerException("Invalid command line options"); + } + } + } +} diff --git a/Source/DafnyServer/VerificationTask.cs b/Source/DafnyServer/VerificationTask.cs new file mode 100644 index 00000000..a00688b1 --- /dev/null +++ b/Source/DafnyServer/VerificationTask.cs @@ -0,0 +1,59 @@ +using System; +using System.Collections.Generic; +using System.IO; +using System.Linq; +using System.Runtime.Serialization; +using System.Runtime.Serialization.Json; +using System.Text; +using System.Threading.Tasks; + +namespace Microsoft.Dafny { + [Serializable] + class VerificationTask { + [DataMember] + string[] args = null; + + [DataMember] + string filename = null; + + [DataMember] + string source = null; + + [DataMember] + bool sourceIsFile = false; + + string ProgramSource { get { return sourceIsFile ? File.ReadAllText(source) : source; } } + + internal static VerificationTask ReadTask(string b64_repr) { + try { + var json = Encoding.UTF8.GetString(System.Convert.FromBase64String(b64_repr)); + using (MemoryStream ms = new MemoryStream(Encoding.Unicode.GetBytes(json))) { + DataContractJsonSerializer serializer = new DataContractJsonSerializer(typeof(VerificationTask)); + return (VerificationTask)serializer.ReadObject(ms); + } + } catch (Exception ex) { + throw new ServerException("Deserialization failed: {0}.", ex.Message); + } + } + + internal static void SelfTest() { + var task = new VerificationTask() { + filename = "", + sourceIsFile = false, + args = new string[] { }, + source = "method selftest() { assert true; }" + }; + try { + task.Run(); + Interaction.EOM(Interaction.SUCCESS, null); + } catch (Exception ex) { + Interaction.EOM(Interaction.FAILURE, ex); + } + } + + internal void Run() { + ServerUtils.ApplyArgs(args); + new DafnyHelper(filename, ProgramSource).Verify(); + } + } +} -- cgit v1.2.3