From 718819250be54f49a9fdca61c3206416d3767105 Mon Sep 17 00:00:00 2001
From: David Cok <david.r.cok@gmail.com>
Date: Mon, 22 May 2023 15:43:43 -0400
Subject: [PATCH] Avoiding a crash on empty input filename - Issue #3549
 (#3899)

Fixes #3549

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Co-authored-by: davidcok <davidcok@github.com>
---
 Source/DafnyCore/DafnyOptions.cs           | 13 +++++++++----
 Source/XUnitExtensions/Lit/ILitCommand.cs  | 12 +++++++++---
 Test/git-issues/git-issue-3549a.dfy        |  2 ++
 Test/git-issues/git-issue-3549a.dfy.expect |  1 +
 Test/git-issues/git-issue-3549b.dfy        |  2 ++
 Test/git-issues/git-issue-3549b.dfy.expect |  1 +
 docs/dev/3549.fix                          |  1 +
 7 files changed, 25 insertions(+), 7 deletions(-)
 create mode 100644 Test/git-issues/git-issue-3549a.dfy
 create mode 100644 Test/git-issues/git-issue-3549a.dfy.expect
 create mode 100644 Test/git-issues/git-issue-3549b.dfy
 create mode 100644 Test/git-issues/git-issue-3549b.dfy.expect
 create mode 100644 docs/dev/3549.fix

diff --git a/Source/DafnyCore/DafnyOptions.cs b/Source/DafnyCore/DafnyOptions.cs
index fc8517917e4..7550957cbc5 100644
--- a/Source/DafnyCore/DafnyOptions.cs
+++ b/Source/DafnyCore/DafnyOptions.cs
@@ -225,11 +225,16 @@ public override bool Parse(string[] arguments) {
         }
       }
 
-      if (i >= arguments.Length) {
-        return base.Parse(arguments);
+      try {
+        if (i >= arguments.Length) {
+          return base.Parse(arguments);
+        }
+        MainArgs = arguments.Skip(i + 1).ToList();
+        return base.Parse(arguments.Take(i).ToArray());
+      } catch (Exception e) {
+        ErrorWriter.WriteLine("Invalid filename: " + e.Message);
+        return false;
       }
-      MainArgs = arguments.Skip(i + 1).ToList();
-      return base.Parse(arguments.Take(i).ToArray());
     }
 
     public DafnyOptions(TextReader inputReader, TextWriter outputWriter, TextWriter errorWriter)
diff --git a/Source/XUnitExtensions/Lit/ILitCommand.cs b/Source/XUnitExtensions/Lit/ILitCommand.cs
index 83318221af4..161ad94544c 100644
--- a/Source/XUnitExtensions/Lit/ILitCommand.cs
+++ b/Source/XUnitExtensions/Lit/ILitCommand.cs
@@ -64,17 +64,20 @@ public static Token[] Tokenize(string line) {
       var singleQuoted = false;
       var doubleQuoted = false;
       var kind = Kind.Verbatim;
+      var tokenStarted = false;
       foreach (var c in line) {
         if (c == '\'' && !doubleQuoted) {
           singleQuoted = !singleQuoted;
+          tokenStarted = true;
         } else if (c == '"' && !singleQuoted) {
           doubleQuoted = !doubleQuoted;
+          tokenStarted = true;
         } else if (Char.IsWhiteSpace(c) && !(singleQuoted || doubleQuoted)) {
-          if (inProgressArgument.Length != 0) {
+          if (tokenStarted) {
             result.Add(new Token(inProgressArgument.ToString(), kind));
-
             inProgressArgument.Clear();
             kind = Kind.Verbatim;
+            tokenStarted = false;
           }
         } else {
           if (c is '?' && inProgressArgument.Length == 1 && inProgressArgument[0] == '-') {
@@ -83,10 +86,13 @@ public static Token[] Tokenize(string line) {
             kind = Kind.MustGlob;
           }
           inProgressArgument.Append(c);
+          tokenStarted = true;
         }
       }
 
-      result.Add(new Token(inProgressArgument.ToString(), kind));
+      if (tokenStarted) {
+        result.Add(new Token(inProgressArgument.ToString(), kind));
+      }
 
       return result.ToArray();
     }
diff --git a/Test/git-issues/git-issue-3549a.dfy b/Test/git-issues/git-issue-3549a.dfy
new file mode 100644
index 00000000000..9ce07b0f267
--- /dev/null
+++ b/Test/git-issues/git-issue-3549a.dfy
@@ -0,0 +1,2 @@
+// RUN: %exits-with 1 %baredafny "" 2> "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/git-issues/git-issue-3549a.dfy.expect b/Test/git-issues/git-issue-3549a.dfy.expect
new file mode 100644
index 00000000000..32d93e22db0
--- /dev/null
+++ b/Test/git-issues/git-issue-3549a.dfy.expect
@@ -0,0 +1 @@
+Invalid filename: The path is empty. (Parameter 'path')
diff --git a/Test/git-issues/git-issue-3549b.dfy b/Test/git-issues/git-issue-3549b.dfy
new file mode 100644
index 00000000000..2f565e87b9e
--- /dev/null
+++ b/Test/git-issues/git-issue-3549b.dfy
@@ -0,0 +1,2 @@
+// RUN: %exits-with 1 %baredafny resolve "" 2> "%t"
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/git-issues/git-issue-3549b.dfy.expect b/Test/git-issues/git-issue-3549b.dfy.expect
new file mode 100644
index 00000000000..87de056fa9f
--- /dev/null
+++ b/Test/git-issues/git-issue-3549b.dfy.expect
@@ -0,0 +1 @@
+*** Error: No input files were specified in command-line resolve|.
diff --git a/docs/dev/3549.fix b/docs/dev/3549.fix
new file mode 100644
index 00000000000..1354608251d
--- /dev/null
+++ b/docs/dev/3549.fix
@@ -0,0 +1 @@
+Fixed crash on an empty filename