Added "unmarshal" command to Dafny server to aid in debugging. The command deserializes (that is, unmarshals) and prints the serialized Dafny program.

Author: RustanLeino

Source/DafnyServer/Server.cs

@@ -87,6 +87,10 @@ void Respond(string[] command) {
           ServerUtils.checkArgs(command, 0);
           ReadPayload();
           VersionCheck.CurrentVersion();
+        } else if (verb == "unmarshal") {
+          ServerUtils.checkArgs(command, 0);
+          var payload = ReadPayload();
+          VerificationTask.ReadTask(payload).Unmarshal();
         } else if (verb == "quit") {
           ServerUtils.checkArgs(command, 0);
           Exit();

Source/DafnyServer/VerificationTask.cs

@@ -63,5 +63,9 @@ public void CounterExample() {
     public void DotGraph() {
       new DafnyHelper(args, filename, ProgramSource).DotGraph();
     }
+
+    public void Unmarshal() {
+      Console.WriteLine(ProgramSource);
+    }
   }
 }

Test/server/unmarshal.transcript

@@ -0,0 +1,8 @@
+# RUN: %server "%s" > "%t"
+# RUN: %diff "%s.expect" "%t"
+unmarshal
+eyJhcmdzIjpbIi9jb21waWxlOjAiLCIvbm9sb2dvIiwiL3ByaW50VG9vbHRpcHMiLCIvdGltZUxp
+bWl0OjIwIl0sImZpbGVuYW1lIjoidHJhbnNjcmlwdCIsInNvdXJjZSI6Im1ldGhvZCBBKGE6aW50
+KSByZXR1cm5zIChiOiBpbnQpIHtcbiAgYiA6PSBhO1xuICBhc3NlcnQgZmFsc2U7XG59XG4iLCJz
+b3VyY2VJc0ZpbGUiOmZhbHNlfQ==
+[[DAFNY-CLIENT: EOM]]

Test/server/unmarshal.transcript.expect

@@ -0,0 +1,10 @@
+# Reading from unmarshal.transcript
+method A(a:int) returns (b: int) {
+  b := a;
+  assert false;
+}
+
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]
+Verification completed successfully!
+[SUCCESS] [[DAFNY-SERVER: EOM]]