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

RELEASE_NOTES.md

@@ -1,9 +1,9 @@
 # Upcoming
 
+- feat: Command-line arguments available from Main() in Dafny programs (https://github.com/dafny-lang/dafny/pull/2594)
 - feat: Support for the `{:opaque}` attibute on `const`
 - fix: Check all compiled expressions to be compilable (https://github.com/dafny-lang/dafny/pull/2641)
 
-
 # 3.8.0
 
 - fix: Use the right bitvector comparison in decrease checks

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, ref 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,10 @@ 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($"Dafny.ISequence<char>[] dafnyArgs = new Dafny.ISequence<char>[args.Length + 1];");
+      wBody.WriteLine($"dafnyArgs[0] = Dafny.Sequence<char>.FromString(\"dotnet\");");
+      wBody.WriteLine($"for(var i = 0; i < args.Length; i++) dafnyArgs[i+1] = Dafny.Sequence<char>.FromString(args[i]);");
+      wBody.WriteLine($"{GetHelperModuleName()}.WithHaltHandling(() => {companion}.{idName}(Dafny.Sequence<Dafny.ISequence<char>>.FromArray(dafnyArgs)));");
       Coverage.EmitTearDown(wBody);
     }
 

Source/Dafny/Compilers/Compiler-cpp.cs

@@ -142,16 +142,21 @@ 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("DafnySequence<DafnySequence<char>> dafnyArgs((uint64)argc);");
+      tryWr.WriteLine("for(int i = 0; i < argc; i++) {");
+      tryWr.WriteLine("  std::string s = argv[i];");
+      tryWr.WriteLine("  dafnyArgs.start[i] = DafnySequenceFromString(s);");
+      tryWr.WriteLine("}");
+      tryWr.WriteLine(string.Format("{0}::{1}::{2}(dafnyArgs);", 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, ref 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 +1151,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;
       }
@@ -2496,7 +2506,7 @@ 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(ComputeExeName(targetFilename)) {
+      var psi = new ProcessStartInfo(ComputeExeName(targetFilename), DafnyOptions.O.ArgsStringExtra) {
         CreateNoWindow = true,
         UseShellExecute = false,
         RedirectStandardOutput = true,

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,11 @@ 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);
+      var dafnyArgs = "dafnyArgs";
+      wBody.WriteLine("var size = len(os.Args)");
+      wBody.WriteLine($"var {dafnyArgs} []interface{{}} = make([]interface{{}}, size)");
+      wBody.WriteLine($"for i, item := range os.Args {{ {dafnyArgs}[i] = {GetHelperModuleName()}.SeqOfString(item) }}");
+      wBody.WriteLine("{0}.{1}({2}.SeqOf({3}...))", companion, idName, GetHelperModuleName(), dafnyArgs);
       Coverage.EmitTearDown(wBody);
     }
 
@@ -130,9 +135,10 @@ ConcreteSyntaxTree CreateDescribedSection(string desc, ConcreteSyntaxTree wr, pa
       return body;
     }
 
-    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw) {
+    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, ref string argsParameterName) {
       var wr = ((GoCompiler.ClassWriter)cw).ConcreteMethodWriter;
-      return wr.NewNamedBlock("func (_this * {0}) Main()", FormatCompanionTypeName(((GoCompiler.ClassWriter)cw).ClassName));
+      argsParameterName = "args";
+      return wr.NewNamedBlock("func (_this * {0}) Main(args _dafny.Seq)", FormatCompanionTypeName(((GoCompiler.ClassWriter)cw).ClassName));
     }
 
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) {
@@ -196,7 +202,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,7 +3613,7 @@ private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename,
         verb = string.Format("build -o \"{0}\"", output);
       }
 
-      var args = string.Format("{0} \"{1}\"", verb, targetFilename);
+      var args = string.Format("{0} \"{1}\"", verb, targetFilename) + DafnyOptions.O.ArgsStringExtra;
       var psi = new ProcessStartInfo("go", args) {
         CreateNoWindow = Environment.OSVersion.Platform != PlatformID.Win32NT,
         UseShellExecute = false,

Source/Dafny/Compilers/Compiler-java.cs

@@ -342,7 +342,13 @@ 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(@"@SuppressWarnings(""unchecked"")");
+      wBody.WriteLine($"dafny.TypeDescriptor<dafny.DafnySequence<? extends Character>> type = dafny.DafnySequence.<Character>_typeDescriptor(dafny.TypeDescriptor.CHAR);");
+      wBody.WriteLine($"dafny.Array<dafny.DafnySequence<? extends Character>> dafnyArgs = dafny.Array.newArray(type, args.length + 1);");
+      wBody.WriteLine($"dafnyArgs.set(0, dafny.DafnySequence.asString(\"java\"));");
+      wBody.WriteLine($"for (int i = 0; i < args.length; i++) dafnyArgs.set(i + 1, dafny.DafnySequence.asString(args[i]));");
+      wBody.WriteLine($"dafny.DafnySequence<? extends dafny.DafnySequence<? extends Character>> result = dafny.DafnySequence.fromArray(type, dafnyArgs);");
+      wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling(() -> {{ {companion}.__Main(result); }} );");
       Coverage.EmitTearDown(wBody);
     }
 
@@ -2278,7 +2284,7 @@ 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", Path.GetFileNameWithoutExtension(targetFilename) + DafnyOptions.O.ArgsStringExtra) {
         CreateNoWindow = true,
         UseShellExecute = false,
         RedirectStandardOutput = true,
@@ -3995,9 +4001,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, ref 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, ref 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 = [\"\", " + string.Join(",", DafnyOptions.O.MainArgs.Select(ToStringLiteral)) + "];");
           nodeProcess.StandardInput.Write(callToMain);
         }
         nodeProcess.StandardInput.Flush();

Source/Dafny/Compilers/Compiler-python.cs

@@ -82,14 +82,16 @@ 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] \" + str(e) + \"\\n\")");
     }
 
-    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw) {
-      return ((ClassWriter)cw).MethodWriter.NewBlockPy("def Main():");
+    protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, ref string argsParameterName) {
+      return ((ClassWriter)cw).MethodWriter.NewBlockPy($"def Main({argsParameterName}):");
     }
 
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern,
@@ -1589,8 +1591,7 @@ 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", targetFilename + DafnyOptions.O.ArgsStringExtra) {
         CreateNoWindow = true,
         UseShellExecute = false,
         RedirectStandardInput = true,