Split the server source into multiple files

5 files changed, 227 insertions, 188 deletions

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<string>(), 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 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

   <PropertyGroup>

@@ -55,6 +55,9 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

+    <Compile Include="DafnyHelper.cs" />

+    <Compile Include="Utilities.cs" />

+    <Compile Include="VerificationTask.cs" />

     <Compile Include="Properties\AssemblyInfo.cs" />

     <Compile Include="Server.cs" />

   </ItemGroup>

@@ -72,4 +75,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ 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 = "<none>", 

-        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<string>(), 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 = "<none>",

+        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();

+    }

+  }

+}