feat: Dafny Main method to accept optional seq<string> argument

RELEASE_NOTES.md

@@ -1,9 +1,11 @@
 # Upcoming
 
+- feat: Command-line arguments are now available from `Main` in Dafny programs, using `Main(args: seq<string>)` (https://github.com/dafny-lang/dafny/pull/2594)
 - fix: Missing related position in failing precondition (https://github.com/dafny-lang/dafny/pull/2658)
 - fix: No more IDE crashing on the elephant operator (https://github.com/dafny-lang/dafny/pull/2668)
 - feat: generate warning when 'old' has no effect
 
+
 # 3.8.1
 
 - feat: Support for the `{:opaque}` attibute on `const` (https://github.com/dafny-lang/dafny/pull/2545)

Source/Dafny/Compilers/Compiler-Csharp.cs

@@ -222,11 +222,11 @@ private void EmitInitNewArrays(BuiltIns builtIns, ConcreteSyntaxTree dafnyNamesp
       }
     }
 
-    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw) {
+    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) {
       var wr = ((ClassWriter)cw).StaticMemberWriter;
       // See EmitCallToMain() - this is named differently because otherwise C# tries
       // to resolve the reference to the instance-level Main method
-      return wr.NewBlock("public static void _StaticMain()");
+      return wr.NewBlock($"public static void _StaticMain(Dafny.ISequence<Dafny.ISequence<char>> {argsParameterName})");
     }
 
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string /*?*/ libraryName, ConcreteSyntaxTree wr) {
@@ -3270,7 +3270,7 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
         throw new Exception("Cannot call run target on a compilation whose assembly has no entry.");
       }
       try {
-        object[] parameters = entry.GetParameters().Length == 0 ? new object[] { } : new object[] { new string[0] };
+        object[] parameters = entry.GetParameters().Length == 0 ? new object[] { } : new object[] { DafnyOptions.O.MainArgs.ToArray() };
         entry.Invoke(null, parameters);
         return true;
       } catch (System.Reflection.TargetInvocationException e) {
@@ -3325,7 +3325,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete
       var idName = IssueCreateStaticMain(mainMethod) ? "_StaticMain" : IdName(mainMethod);
 
       Coverage.EmitSetup(wBody);
-      wBody.WriteLine($"{GetHelperModuleName()}.WithHaltHandling({companion}.{idName});");
+      wBody.WriteLine($"{GetHelperModuleName()}.WithHaltHandling(() => {companion}.{idName}(Dafny.Sequence<Dafny.ISequence<char>>.FromMainArguments(args)));");
       Coverage.EmitTearDown(wBody);
     }
 

Source/Dafny/Compilers/Compiler-cpp.cs

@@ -142,16 +142,16 @@ protected override void EmitFooter(Program program, ConcreteSyntaxTree wr) {
     }
 
     public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
-      var w = wr.NewBlock("int main()");
+      var w = wr.NewBlock("int main(int argc, char *argv[])");
       var tryWr = w.NewBlock("try");
-      tryWr.WriteLine(string.Format("{0}::{1}::{2}();", mainMethod.EnclosingClass.EnclosingModuleDefinition.CompileName, mainMethod.EnclosingClass.CompileName, mainMethod.Name));
+      tryWr.WriteLine(string.Format("{0}::{1}::{2}(dafny_get_args(argc, argv));", mainMethod.EnclosingClass.EnclosingModuleDefinition.CompileName, mainMethod.EnclosingClass.CompileName, mainMethod.Name));
       var catchWr = w.NewBlock("catch (DafnyHaltException & e)");
       catchWr.WriteLine("std::cout << \"Program halted: \" << e.what() << std::endl;");
     }
 
-    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw) {
+    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) {
       var wr = (cw as CppCompiler.ClassWriter).MethodWriter;
-      return wr.NewBlock("int main()");
+      return wr.NewBlock($"int main(DafnySequence<DafnySequence<char>> {argsParameterName})");
     }
 
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) {
@@ -1146,7 +1146,12 @@ protected void DeclareField(string className, List<TypeParameter> targs, string
 
     private string DeclareFormalString(string prefix, string name, Type type, IToken tok, bool isInParam) {
       if (isInParam) {
-        return String.Format("{0}{2} {1}", prefix, name, TypeName(type, null, tok));
+        var result = String.Format("{0}{2} {1}", prefix, name, TypeName(type, null, tok));
+        if (name == "__noArgsParameter") {
+          result += " __attribute__((unused))";
+        }
+
+        return result;
       } else {
         return null;
       }
@@ -2500,8 +2505,12 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
         CreateNoWindow = true,
         UseShellExecute = false,
         RedirectStandardOutput = true,
-        RedirectStandardError = true,
+        RedirectStandardError = true
       };
+      foreach (var arg in DafnyOptions.O.MainArgs) {
+        psi.ArgumentList.Add(arg);
+      }
+
       var proc = Process.Start(psi);
       while (!proc.StandardOutput.EndOfStream) {
         outputWriter.WriteLine(proc.StandardOutput.ReadLine());

Source/Dafny/Compilers/Compiler-go.cs

@@ -58,6 +58,7 @@ static string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
     private static List<Import> StandardImports =
       new List<Import> {
         new Import { Name = "_dafny", Path = "dafny" },
+        new Import { Name = "os", Path = "os" },
       };
     private static string DummyTypeName = "Dummy__";
 
@@ -118,7 +119,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete
       var idName = IssueCreateStaticMain(mainMethod) ? "Main" : IdName(mainMethod);
 
       Coverage.EmitSetup(wBody);
-      wBody.WriteLine("{0}.{1}()", companion, idName);
+      wBody.WriteLine("{0}.{1}({2}.FromMainArguments(os.Args))", companion, idName, GetHelperModuleName());
       Coverage.EmitTearDown(wBody);
     }
 
@@ -130,9 +131,9 @@ ConcreteSyntaxTree CreateDescribedSection(string desc, ConcreteSyntaxTree wr, pa
       return body;
     }
 
-    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw) {
+    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) {
       var wr = ((GoCompiler.ClassWriter)cw).ConcreteMethodWriter;
-      return wr.NewNamedBlock("func (_this * {0}) Main()", FormatCompanionTypeName(((GoCompiler.ClassWriter)cw).ClassName));
+      return wr.NewNamedBlock("func (_this * {0}) Main({1} _dafny.Seq)", FormatCompanionTypeName(((GoCompiler.ClassWriter)cw).ClassName), argsParameterName);
     }
 
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) {
@@ -196,7 +197,11 @@ private void EmitImport(Import import, ConcreteSyntaxTree importWriter, Concrete
       importWriter.WriteLine("{0} \"{1}\"", id, path);
 
       if (!import.SuppressDummy) {
-        importDummyWriter.WriteLine("var _ {0}.{1}", id, DummyTypeName);
+        if (id == "os") {
+          importDummyWriter.WriteLine("var _ = os.Args");
+        } else {
+          importDummyWriter.WriteLine("var _ {0}.{1}", id, DummyTypeName);
+        }
       }
     }
 
@@ -3603,14 +3608,18 @@ private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename,
         verb = string.Format("build -o \"{0}\"", output);
       }
 
-      var args = string.Format("{0} \"{1}\"", verb, targetFilename);
-      var psi = new ProcessStartInfo("go", args) {
+      var psi = new ProcessStartInfo("go") {
         CreateNoWindow = Environment.OSVersion.Platform != PlatformID.Win32NT,
         UseShellExecute = false,
         RedirectStandardInput = false,
         RedirectStandardOutput = false,
         RedirectStandardError = false,
       };
+      psi.ArgumentList.Add(verb);
+      psi.ArgumentList.Add(targetFilename);
+      foreach (var arg in DafnyOptions.O.MainArgs) {
+        psi.ArgumentList.Add(arg);
+      }
       psi.EnvironmentVariables["GOPATH"] = GoPath(targetFilename);
       // Dafny compiles to the old Go package system, whereas Go has moved on to a module
       // system. Until Dafny's Go compiler catches up, the GO111MODULE variable has to be set.

Source/Dafny/Compilers/Compiler-java.cs

@@ -342,7 +342,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete
       var modName = mainMethod.EnclosingClass.EnclosingModuleDefinition.CompileName == "_module" ? "_System." : "";
       companion = modName + companion;
       Coverage.EmitSetup(wBody);
-      wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling({companion}::__Main);");
+      wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling(() -> {{ {companion}.__Main({DafnyHelpersClass}.FromMainArguments(args)); }} );");
       Coverage.EmitTearDown(wBody);
     }
 
@@ -2278,13 +2278,17 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
 
     public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string /*?*/ targetFilename,
      ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter) {
-      var psi = new ProcessStartInfo("java", Path.GetFileNameWithoutExtension(targetFilename)) {
+      var psi = new ProcessStartInfo("java") {
         CreateNoWindow = true,
         UseShellExecute = false,
         RedirectStandardOutput = true,
         RedirectStandardError = true,
         WorkingDirectory = Path.GetFullPath(Path.GetDirectoryName(targetFilename))
       };
+      psi.ArgumentList.Add(Path.GetFileNameWithoutExtension(targetFilename));
+      foreach (var arg in DafnyOptions.O.MainArgs) {
+        psi.ArgumentList.Add(arg);
+      }
       psi.EnvironmentVariables["CLASSPATH"] = GetClassPath(targetFilename);
       var proc = Process.Start(psi);
       while (!proc.StandardOutput.EndOfStream) {
@@ -3995,9 +3999,9 @@ protected override void EmitTypeTest(string localName, Type fromType, Type toTyp
     protected override bool IssueCreateStaticMain(Method m) {
       return true;
     }
-    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw) {
+    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) {
       var wr = ((ClassWriter)cw).StaticMemberWriter;
-      return wr.NewBlock("public static void __Main()");
+      return wr.NewBlock($"public static void __Main(dafny.DafnySequence<? extends dafny.DafnySequence<? extends Character>> {argsParameterName})");
     }
 
     protected override void CreateIIFE(string bvName, Type bvType, IToken bvTok, Type bodyType, IToken bodyTok,

Source/Dafny/Compilers/Compiler-js.cs

@@ -52,13 +52,13 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
 
     public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
       Coverage.EmitSetup(wr);
-      wr.WriteLine("_dafny.HandleHaltExceptions({0}.{1});", mainMethod.EnclosingClass.FullCompileName, mainMethod.IsStatic ? IdName(mainMethod) : "Main");
+      wr.WriteLine("_dafny.HandleHaltExceptions(() => {0}.{1}(require('process').argv));", mainMethod.EnclosingClass.FullCompileName, mainMethod.IsStatic ? IdName(mainMethod) : "Main");
       Coverage.EmitTearDown(wr);
     }
 
-    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw) {
+    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) {
       var wr = (cw as JavaScriptCompiler.ClassWriter).MethodWriter;
-      return wr.NewBlock("static Main()");
+      return wr.NewBlock($"static Main({argsParameterName})");
     }
 
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) {
@@ -2441,6 +2441,12 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
       return SendToNewNodeProcess(dafnyProgramName, targetProgramText, callToMain, targetFilename, otherFileNames, outputWriter);
     }
 
+    public string ToStringLiteral(string s) {
+      var wr = new ConcreteSyntaxTree();
+      EmitStringLiteral(s, false, wr);
+      return wr.ToString();
+    }
+
     bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string targetFilename, ReadOnlyCollection<string> otherFileNames,
       TextWriter outputWriter) {
       Contract.Requires(targetFilename != null || otherFileNames.Count == 0);
@@ -2461,6 +2467,7 @@ bool SendToNewNodeProcess(string dafnyProgramName, string targetProgramText, str
         }
         nodeProcess.StandardInput.Write(targetProgramText);
         if (callToMain != null && DafnyOptions.O.RunAfterCompile) {
+          nodeProcess.StandardInput.WriteLine("require('process').argv = [\"node\", " + string.Join(",", DafnyOptions.O.MainArgs.Select(ToStringLiteral)) + "];");
           nodeProcess.StandardInput.Write(callToMain);
         }
         nodeProcess.StandardInput.Flush();

Source/Dafny/Compilers/Compiler-python.cs

@@ -83,15 +83,17 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
 
     public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
       Coverage.EmitSetup(wr);
+      var dafnyArgs = "dafnyArgs";
       wr.NewBlockPy("try:")
-        .WriteLine($"{mainMethod.EnclosingClass.FullCompileName}.{(IssueCreateStaticMain(mainMethod) ? "Main" : IdName(mainMethod))}()");
+        .WriteLine($"{dafnyArgs} = [{DafnyRuntimeModule}.Seq(a) for a in sys.argv]")
+        .WriteLine($"{mainMethod.EnclosingClass.FullCompileName}.{(IssueCreateStaticMain(mainMethod) ? "Main" : IdName(mainMethod))}({dafnyArgs})");
       wr.NewBlockPy($"except {DafnyRuntimeModule}.HaltException as e:")
         .WriteLine($"{DafnyRuntimeModule}.print(\"[Program halted] \" + {DafnyRuntimeModule}.string_of(e.message) + \"\\n\")");
       Coverage.EmitTearDown(wr);
     }
 
-    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw) {
-      return ((ClassWriter)cw).MethodWriter.NewBlockPy("def Main():");
+    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) {
+      return ((ClassWriter)cw).MethodWriter.NewBlockPy($"def Main({argsParameterName}):");
     }
 
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern,
@@ -1695,14 +1697,17 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target
     public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string /*?*/ callToMain,
       string targetFilename, ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter) {
       Contract.Requires(targetFilename != null || otherFileNames.Count == 0);
-
-      var psi = new ProcessStartInfo("python3", targetFilename) {
+      var psi = new ProcessStartInfo("python3") {
         CreateNoWindow = true,
         UseShellExecute = false,
         RedirectStandardInput = true,
         RedirectStandardOutput = false,
         RedirectStandardError = false,
       };
+      psi.ArgumentList.Add(targetFilename);
+      foreach (var arg in DafnyOptions.O.MainArgs) {
+        psi.ArgumentList.Add(arg);
+      }
 
       try {
         using var pythonProcess = Process.Start(psi);