diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index a5a276b6120..7d52f65eee1 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,9 +1,11 @@ # Upcoming +- feat: Command-line arguments are now available from `Main` in Dafny programs, using `Main(args: seq)` (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) diff --git a/Source/Dafny/Compilers/Compiler-Csharp.cs b/Source/Dafny/Compilers/Compiler-Csharp.cs index 64a77bd782a..436f98e1c52 100644 --- a/Source/Dafny/Compilers/Compiler-Csharp.cs +++ b/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> {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>.FromMainArguments(args)));"); Coverage.EmitTearDown(wBody); } diff --git a/Source/Dafny/Compilers/Compiler-cpp.cs b/Source/Dafny/Compilers/Compiler-cpp.cs index fe87664e8b7..912993bd52d 100644 --- a/Source/Dafny/Compilers/Compiler-cpp.cs +++ b/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> {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 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()); diff --git a/Source/Dafny/Compilers/Compiler-go.cs b/Source/Dafny/Compilers/Compiler-go.cs index 46fb809a030..2fb99eb23dc 100644 --- a/Source/Dafny/Compilers/Compiler-go.cs +++ b/Source/Dafny/Compilers/Compiler-go.cs @@ -58,6 +58,7 @@ static string FormatDefaultTypeParameterValue(TopLevelDecl tp) { private static List StandardImports = new List { 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); + } } } @@ -3563,9 +3568,9 @@ private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, } } - string verb; + List verb = new(); if (run) { - verb = "run"; + verb.Add("run"); } else { string output; var outputToFile = !DafnyOptions.O.RunAfterCompile; @@ -3600,17 +3605,25 @@ private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, } } - verb = string.Format("build -o \"{0}\"", output); + verb.Add("build"); + verb.Add("-o"); + verb.Add(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, }; + foreach (var verbArg in verb) { + psi.ArgumentList.Add(verbArg); + } + 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. diff --git a/Source/Dafny/Compilers/Compiler-java.cs b/Source/Dafny/Compilers/Compiler-java.cs index 8574ace68fd..00ed6f21b8b 100644 --- a/Source/Dafny/Compilers/Compiler-java.cs +++ b/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 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> {argsParameterName})"); } protected override void CreateIIFE(string bvName, Type bvType, IToken bvTok, Type bodyType, IToken bodyTok, diff --git a/Source/Dafny/Compilers/Compiler-js.cs b/Source/Dafny/Compilers/Compiler-js.cs index 5288d8408f4..2f4e34f0086 100644 --- a/Source/Dafny/Compilers/Compiler-js.cs +++ b/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 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(); diff --git a/Source/Dafny/Compilers/Compiler-python.cs b/Source/Dafny/Compilers/Compiler-python.cs index 7eb127bf2e5..32fb8e5200e 100644 --- a/Source/Dafny/Compilers/Compiler-python.cs +++ b/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 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); diff --git a/Source/Dafny/Compilers/SinglePassCompiler.cs b/Source/Dafny/Compilers/SinglePassCompiler.cs index 6f66ab71e13..6293bdf760e 100644 --- a/Source/Dafny/Compilers/SinglePassCompiler.cs +++ b/Source/Dafny/Compilers/SinglePassCompiler.cs @@ -107,7 +107,7 @@ public override void OnPostCompile() { /// Creates a static Main method. The caller will fill the body of this static Main with a /// call to the instance Main method in the enclosing class. /// - protected abstract ConcreteSyntaxTree CreateStaticMain(IClassWriter wr); + protected abstract ConcreteSyntaxTree CreateStaticMain(IClassWriter wr, string argsParameterName); protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr); protected abstract string GetHelperModuleName(); protected interface IClassWriter { @@ -1532,7 +1532,7 @@ public static bool HasMain(Program program, out Method mainMethod) { foreach (MemberDecl member in c.Members) { if (member is Method m && member.FullDafnyName == name) { mainMethod = m; - if (!IsPermittedAsMain(mainMethod, out string reason)) { + if (!IsPermittedAsMain(program, mainMethod, out string reason)) { ReportError(program.Reporter, mainMethod.tok, "The method \"{0}\" is not permitted as a main method ({1}).", null, name, reason); mainMethod = null; return false; @@ -1572,7 +1572,7 @@ public static bool HasMain(Program program, out Method mainMethod) { } } if (hasMain) { - if (!IsPermittedAsMain(mainMethod, out string reason)) { + if (!IsPermittedAsMain(program, mainMethod, out string reason)) { ReportError(program.Reporter, mainMethod.tok, "This method marked \"{{:main}}\" is not permitted as a main method ({0}).", null, reason); mainMethod = null; return false; @@ -1613,7 +1613,7 @@ public static bool HasMain(Program program, out Method mainMethod) { } if (hasMain) { - if (!IsPermittedAsMain(mainMethod, out string reason)) { + if (!IsPermittedAsMain(program, mainMethod, out string reason)) { ReportError(program.Reporter, mainMethod.tok, "This method \"Main\" is not permitted as a main method ({0}).", null, reason); return false; } else { @@ -1626,11 +1626,12 @@ public static bool HasMain(Program program, out Method mainMethod) { } } - public static bool IsPermittedAsMain(Method m, out String reason) { + public static bool IsPermittedAsMain(Program program, Method m, out String reason) { Contract.Requires(m.EnclosingClass is TopLevelDeclWithMembers); // In order to be a legal Main() method, the following must be true: // The method is not a ghost method // The method takes no non-ghost parameters and no type parameters + // except at most one array of type "array" // The enclosing type does not take any type parameters // If the method is an instance (that is, non-static) method in a class, then the enclosing class must not declare any constructor // In addition, either: @@ -1672,8 +1673,22 @@ public static bool IsPermittedAsMain(Method m, out String reason) { } } if (!m.Ins.TrueForAll(f => f.IsGhost)) { - reason = "the method has non-ghost parameters"; - return false; + var nonGhostFormals = m.Ins.Where(f => !f.IsGhost).ToList(); + if (nonGhostFormals.Count > 1) { + reason = "the method has two or more non-ghost parameters"; + return false; + } + var typeOfUniqueFormal = nonGhostFormals[0].Type.NormalizeExpandKeepConstraints(); + if (typeOfUniqueFormal.AsSeqType is not { } seqType || + seqType.Arg.AsSeqType is not { } subSeqType || + !subSeqType.Arg.IsCharType) { + reason = "the method's non-ghost argument type should be an seq, got " + typeOfUniqueFormal; + return false; + } + } else { + // Need to manually insert the args. + var argsType = new SeqType(new SeqType(new CharType())); + m.Ins.Add(new ImplicitFormal(m.tok, "_noArgsParameter", argsType, true, false)); } if (!m.Outs.TrueForAll(f => f.IsGhost)) { reason = "the method has non-ghost out parameters"; @@ -2361,6 +2376,8 @@ private void CompileFunction(Function f, IClassWriter cw, bool lookasideBody) { } } + public const string STATIC_ARGS_NAME = "args"; + private void CompileMethod(Program program, Method m, IClassWriter cw, bool lookasideBody) { Contract.Requires(cw != null); Contract.Requires(m != null); @@ -2397,7 +2414,7 @@ private void CompileMethod(Program program, Method m, IClassWriter cw, bool look } if (m == program.MainMethod && IssueCreateStaticMain(m)) { - w = CreateStaticMain(cw); + w = CreateStaticMain(cw, STATIC_ARGS_NAME); var ty = UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(m.EnclosingClass); LocalVariable receiver = null; if (!m.IsStatic) { @@ -2429,6 +2446,7 @@ private void CompileMethod(Program program, Method m, IClassWriter cw, bool look sep = ", "; } EmitTypeDescriptorsActuals(ForTypeDescriptors(typeArgs, m, false), m.tok, w, ref sep); + w.Write(sep + STATIC_ARGS_NAME); w.Write(")"); EndStmt(w); } diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index f5bf9ca9a18..228d675cdd7 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -24,6 +24,21 @@ public static DafnyOptions Create(params string[] arguments) { return result; } + public override bool Parse(string[] arguments) { + int i; + for (i = 0; i < arguments.Length; i++) { + if (arguments[i] == "--args") { + break; + } + } + + if (i >= arguments.Length) { + return base.Parse(arguments); + } + MainArgs = arguments.Skip(i + 1).ToList(); + return base.Parse(arguments.Take(i).ToArray()); + } + public DafnyOptions() : base("Dafny", "Dafny program verifier", new DafnyConsolePrinter()) { ErrorTrace = 0; @@ -86,6 +101,7 @@ public enum PrintModes { public string DafnyPrintResolvedFile = null; public List DafnyPrintExportedViews = new List(); public bool Compile = true; + public List MainArgs = new List(); public Compiler Compiler; public bool CompileVerbose = true; @@ -281,7 +297,7 @@ protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) { // There are no commas in paths, but there can be in arguments var argumentsString = string.Join(',', pluginArray.Skip(1)); // Parse arguments, accepting and remove double quotes that isolate long arguments - arguments = ParsePluginArguments(argumentsString); + arguments = ParseInnerArguments(argumentsString); } Plugins.Add(AssemblyPlugin.Load(pluginPath, arguments)); } @@ -640,7 +656,7 @@ protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) { return TestGenOptions.ParseOption(name, ps) || base.ParseOption(name, ps); } - private static string[] ParsePluginArguments(string argumentsString) { + private static string[] ParseInnerArguments(string argumentsString) { var splitter = new Regex(@"""(?(?:[^""\\]|\\\\|\\"")*)""|(?[^ ]+)"); var escapedChars = new Regex(@"(?\\"")|\\\\"); return splitter.Matches(argumentsString).Select( @@ -1337,10 +1353,13 @@ verification outcome. features like traits or co-inductive types. /Main: - Specify the (fully-qualified) name of the method to use as the - executable entry point. Default is the method with the {{:main}} - attribute, or else the method named 'Main'. - + Specify the (fully-qualified) name of the method to use as the executable entry point. + Default is the method with the {{:main}} attribute, or else the method named 'Main'. + A Main method can have at most one (non-ghost) argument of type `seq` +--args ... + When running a Dafny file through /compile:3 or /compile:4, '--args' provides + all arguments after it to the Main function, at index starting at 1. + Index 0 is used to store the executable's name if it exists. /runAllTests: (experimental) 0 (default) - Annotates compiled methods with the {{:test}} attribute such that they can be tested using a testing framework diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index a3c6e6636c3..35e3f95e6db 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -177,7 +177,7 @@ public static CommandLineArgumentsResult ProcessCommandLineArguments(DafnyOption if (options.UseStdin) { dafnyFiles.Add(new DafnyFile("", true)); } else if (options.Files.Count == 0) { - options.Printer.ErrorWriteLine(Console.Error, "*** Error: No input files were specified."); + options.Printer.ErrorWriteLine(Console.Error, "*** Error: No input files were specified in command-line " + string.Join("|", args) + "."); return CommandLineArgumentsResult.PREPROCESSING_ERROR; } if (options.XmlSink != null) { diff --git a/Source/DafnyRuntime/DafnyRuntime.cs b/Source/DafnyRuntime/DafnyRuntime.cs index 4080dcbedfc..9f802d9af10 100755 --- a/Source/DafnyRuntime/DafnyRuntime.cs +++ b/Source/DafnyRuntime/DafnyRuntime.cs @@ -914,6 +914,17 @@ public static ISequence FromElements(params T[] values) { public static ISequence FromString(string s) { return new ArraySequence(s.ToCharArray()); } + + public static ISequence> FromMainArguments(string[] args) { + Dafny.ISequence[] dafnyArgs = new Dafny.ISequence[args.Length + 1]; + dafnyArgs[0] = Dafny.Sequence.FromString("dotnet"); + for (var i = 0; i < args.Length; i++) { + dafnyArgs[i + 1] = Dafny.Sequence.FromString(args[i]); + } + + return Sequence>.FromArray(dafnyArgs); + } + public ISequence DowncastClone(Func converter) { if (this is ISequence th) { return th; diff --git a/Source/DafnyRuntime/DafnyRuntime.go b/Source/DafnyRuntime/DafnyRuntime.go index a7b667d116e..5da418e8ec2 100644 --- a/Source/DafnyRuntime/DafnyRuntime.go +++ b/Source/DafnyRuntime/DafnyRuntime.go @@ -10,6 +10,15 @@ import ( "runtime" ) +func FromMainArguments(args []string) Seq { + var size = len(args) + var dafnyArgs []interface{} = make([]interface{}, size) + for i, item := range args { + dafnyArgs[i] = SeqOfString(item) + } + return SeqOf(dafnyArgs...) +} + /****************************************************************************** * Generic values ******************************************************************************/ diff --git a/Source/DafnyRuntime/DafnyRuntime.h b/Source/DafnyRuntime/DafnyRuntime.h index 8a879cb69f2..773eb12c47d 100644 --- a/Source/DafnyRuntime/DafnyRuntime.h +++ b/Source/DafnyRuntime/DafnyRuntime.h @@ -758,3 +758,12 @@ struct std::hash> { return seed; } }; + +DafnySequence> dafny_get_args(int argc, char* argv[]) { + DafnySequence> dafnyArgs((uint64)argc); + for(int i = 0; i < argc; i++) { + std::string s = argv[i]; + dafnyArgs.start[i] = DafnySequenceFromString(s); + } + return dafnyArgs; +} diff --git a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java index 2cdb4969d85..db2ac929b1a 100644 --- a/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java +++ b/Source/DafnyRuntime/DafnyRuntimeJava/src/main/java/dafny/Helpers.java @@ -18,6 +18,15 @@ public class Helpers { + public static DafnySequence> FromMainArguments(String[] args) { + @SuppressWarnings("unchecked") + TypeDescriptor> type = DafnySequence._typeDescriptor(TypeDescriptor.CHAR); + dafny.Array> dafnyArgs = dafny.Array.newArray(type, args.length + 1); + dafnyArgs.set(0, DafnySequence.asString("java")); + for (int i = 0; i < args.length; i++) dafnyArgs.set(i + 1, DafnySequence.asString(args[i])); + return DafnySequence.fromArray(type, dafnyArgs); + } + public static boolean Quantifier(Iterable vals, boolean frall, Predicate pred) { for (T t : vals) { if (pred.test(t) != frall) { diff --git a/Test/comp/CompileWithArguments.dfy b/Test/comp/CompileWithArguments.dfy new file mode 100644 index 00000000000..f79568b93d3 --- /dev/null +++ b/Test/comp/CompileWithArguments.dfy @@ -0,0 +1,32 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" --args csharp 1 >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:cpp "%s" --args cpp Yipee >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" --args java heya >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" --args javascript 2 >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" --args python 1 >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" --args "go go" 1 >> "%t" +// RUN: %dafny /noVerify /compile:2 /compileTarget:cs "%s" /out:%s.dll +// RUN: dotnet %s.dll "ellel" 2 >> "%t" +// RUN: dotnet %s.dll "on the go" 1 >> "%t" +// RUN: dotnet %s.dll "dll" "Aloha from" >> "%t" +// RUN: %diff "%s.expect" "%t" + +method Main(args: seq) { + if |args| != 3 { + print "Expected 3 arguments, got ", |args|; + } else { + var executable := args[0]; + if |executable| < 24 { + print executable, " says "; + } else { + print "Someone says "; + } + if args[2] == "1" { + print "Hello ",args[1], "\n"; + } else if args[2] == "2" { + print "Howdy ", args[1], "\n"; + } else { + print args[2], " ", args[1], "\n"; + } + } +} \ No newline at end of file diff --git a/Test/comp/CompileWithArguments.dfy.expect b/Test/comp/CompileWithArguments.dfy.expect new file mode 100644 index 00000000000..885f26f2b66 --- /dev/null +++ b/Test/comp/CompileWithArguments.dfy.expect @@ -0,0 +1,23 @@ + +Dafny program verifier finished with 1 verified, 0 errors + +Dafny program verifier did not attempt verification +dotnet says Hello csharp + +Dafny program verifier did not attempt verification +Someone says Yipee cpp + +Dafny program verifier did not attempt verification +java says heya java + +Dafny program verifier did not attempt verification +node says Howdy javascript + +Dafny program verifier did not attempt verification +Someone says Hello python + +Dafny program verifier did not attempt verification +Someone says Hello go go +dotnet says Howdy ellel +dotnet says Hello on the go +dotnet says Aloha from dll diff --git a/Test/comp/CompileWithArgumentsFail.dfy b/Test/comp/CompileWithArgumentsFail.dfy new file mode 100644 index 00000000000..085bf5b0340 --- /dev/null +++ b/Test/comp/CompileWithArgumentsFail.dfy @@ -0,0 +1,7 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:cs "%s" --args csharp 1 >> "%t" +// RUN: %diff "%s.expect" "%t" + +method Main(args: int) { + print "ok", args; +} \ No newline at end of file diff --git a/Test/comp/CompileWithArgumentsFail.dfy.expect b/Test/comp/CompileWithArgumentsFail.dfy.expect new file mode 100644 index 00000000000..3660adb6f41 --- /dev/null +++ b/Test/comp/CompileWithArgumentsFail.dfy.expect @@ -0,0 +1,5 @@ + +Dafny program verifier finished with 0 verified, 0 errors + +Dafny program verifier did not attempt verification +CompileWithArgumentsFail.dfy(5,7): Error: This method "Main" is not permitted as a main method (the method's non-ghost argument type should be an seq, got int). diff --git a/Test/comp/CompileWithArgumentsFail2.dfy b/Test/comp/CompileWithArgumentsFail2.dfy new file mode 100644 index 00000000000..ffb97591df8 --- /dev/null +++ b/Test/comp/CompileWithArgumentsFail2.dfy @@ -0,0 +1,7 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:cs "%s" --args csharp 1 >> "%t" +// RUN: %diff "%s.expect" "%t" + +method Main(args: array, dummy: int) { + print "ok", dummy; +} \ No newline at end of file diff --git a/Test/comp/CompileWithArgumentsFail2.dfy.expect b/Test/comp/CompileWithArgumentsFail2.dfy.expect new file mode 100644 index 00000000000..61b5f9be22d --- /dev/null +++ b/Test/comp/CompileWithArgumentsFail2.dfy.expect @@ -0,0 +1,5 @@ + +Dafny program verifier finished with 0 verified, 0 errors + +Dafny program verifier did not attempt verification +CompileWithArgumentsFail2.dfy(5,7): Error: This method "Main" is not permitted as a main method (the method has two or more non-ghost parameters). diff --git a/Test/git-issues/git-issue-MainE.dfy.expect b/Test/git-issues/git-issue-MainE.dfy.expect index b0c51185417..92fa9c1915f 100644 --- a/Test/git-issues/git-issue-MainE.dfy.expect +++ b/Test/git-issues/git-issue-MainE.dfy.expect @@ -2,7 +2,7 @@ Dafny program verifier finished with 1 verified, 0 errors Dafny program verifier did not attempt verification -git-issue-MainE.dfy(20,9): Error: The method "A.Test" is not permitted as a main method (the method has non-ghost parameters). +git-issue-MainE.dfy(20,9): Error: The method "A.Test" is not permitted as a main method (the method's non-ghost argument type should be an seq, got int). Dafny program verifier did not attempt verification git-issue-MainE.dfy(23,9): Error: The method "B.Test" is not permitted as a main method (the method has type parameters). diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index ea59245b1b0..90b20e90e01 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -407,10 +407,13 @@ Usage: Dafny [ option ... ] [ filename ... ] features like traits or co-inductive types. /Main: - Specify the (fully-qualified) name of the method to use as the - executable entry point. Default is the method with the {:main} - attribute, or else the method named 'Main'. - + Specify the (fully-qualified) name of the method to use as the executable entry point. + Default is the method with the {:main} attribute, or else the method named 'Main'. + A Main method can have at most one (non-ghost) argument of type `seq` + --args ... + When running a Dafny file through /compile:3 or /compile:4, '--args' provides + all arguments after it to the Main function, at index starting at 1. + Index 0 is used to store the executable's name if it exists. /runAllTests: (experimental) 0 (default) - Annotates compiled methods with the {:test} attribute such that they can be tested using a testing framework