From dd08b0245fde74e50a6a0ca5d3818ba840420bd9 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 16 Aug 2022 10:52:45 -0500 Subject: [PATCH 01/22] MVP for compile arguments --- Source/Dafny/Compilers/Compiler-Csharp.cs | 6 +++-- Source/Dafny/Compilers/SinglePassCompiler.cs | 16 +++++++++++-- Source/Dafny/DafnyOptions.cs | 14 +++++++++-- Test/comp/CompileWithArguments.dfy | 25 ++++++++++++++++++++ Test/comp/CompileWithArguments.dfy.expect | 21 ++++++++++++++++ 5 files changed, 76 insertions(+), 6 deletions(-) create mode 100644 Test/comp/CompileWithArguments.dfy create mode 100644 Test/comp/CompileWithArguments.dfy.expect diff --git a/Source/Dafny/Compilers/Compiler-Csharp.cs b/Source/Dafny/Compilers/Compiler-Csharp.cs index 552c832da9d..2cf2c95f4c0 100644 --- a/Source/Dafny/Compilers/Compiler-Csharp.cs +++ b/Source/Dafny/Compilers/Compiler-Csharp.cs @@ -3271,7 +3271,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) { @@ -3326,7 +3326,9 @@ 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[] dafnyArgs = new Dafny.ISequence[args.Length];"); + wBody.WriteLine($"for(var i = 0; i < args.Length; i++) dafnyArgs[i] = Dafny.Sequence.FromString(args[i]);"); + wBody.WriteLine($"{GetHelperModuleName()}.WithHaltHandling(() => {companion}.{idName}(dafnyArgs));"); Coverage.EmitTearDown(wBody); } diff --git a/Source/Dafny/Compilers/SinglePassCompiler.cs b/Source/Dafny/Compilers/SinglePassCompiler.cs index 5554a47b314..86ea2cc0ca3 100644 --- a/Source/Dafny/Compilers/SinglePassCompiler.cs +++ b/Source/Dafny/Compilers/SinglePassCompiler.cs @@ -1629,6 +1629,7 @@ public static bool IsPermittedAsMain(Method m, out String reason) { // 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: @@ -1670,8 +1671,19 @@ 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.IsArrayType || + typeOfUniqueFormal.TypeArgs.Count != 1 || + typeOfUniqueFormal.TypeArgs[0].AsSeqType is not { } seqType || + !seqType.Arg.IsCharType) { + reason = "the method's non-ghost argument type should be an array, got " + typeOfUniqueFormal.TypeArgs[0]; + return false; + } } if (!m.Outs.TrueForAll(f => f.IsGhost)) { reason = "the method has non-ghost out parameters"; diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 82ec92c5e84..191982ecab4 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -86,6 +86,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; @@ -283,7 +284,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)); } @@ -309,6 +310,15 @@ protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) { return true; } + case "mainArgs": + case "MainArgs": { + if (ps.ConfirmArgumentCount(1)) { + MainArgs.AddRange(ParseInnerArguments(args[ps.i])); + } + + return true; + } + case "runAllTests": { int runAllTests = 0; if (ps.GetIntArgument(ref runAllTests, 2)) { @@ -642,7 +652,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( diff --git a/Test/comp/CompileWithArguments.dfy b/Test/comp/CompileWithArguments.dfy new file mode 100644 index 00000000000..e52eb0e5d41 --- /dev/null +++ b/Test/comp/CompileWithArguments.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "/mainArgs:csharp 1" "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:js "/mainArgs:javascript 2" "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:go "/mainArgs:\"go go\" 1" "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:java "/mainArgs:java heya" "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:py "/mainArgs:python 1" "%s" >> "%t" +// RUN: %dafny /noVerify /compile:2 /compileTarget:cs "%s" /out:CompileWithArgument.dll +// RUN: %dotnet CompileWithArgument.dll "ellel" 2 >> "%t" +// RUN: %dotnet CompileWithArgument.dll "on the go" 1 >> "%t" +// RUN: %dotnet CompileWithArgument.dll "dll" "Aloha from" >> "%t" +// RUN: %diff "%s.expect" "%t" + +method Main(args: array) { + if args.Length != 2 { + print "Expected 2 arguments, got ", args.Length; + } else { + if args[1] == "1" { + print "Hello ",args[0], "\n"; + } else if args[1] == "2" { + print "Howdy ", args[0], "\n"; + } else { + print args[1], " ", args[0], "\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..5bcf851ad0a --- /dev/null +++ b/Test/comp/CompileWithArguments.dfy.expect @@ -0,0 +1,21 @@ + +Dafny program verifier finished with 6 verified, 0 errors + +Dafny program verifier did not attempt verification +Hello csharp + +Dafny program verifier did not attempt verification +Howdy javascript + +Dafny program verifier did not attempt verification +Hello go go + +Dafny program verifier did not attempt verification +Heya java + +Dafny program verifier did not attempt verification +Hello Python + +Howdy ellel +Hello on the go +Aloha from dll \ No newline at end of file From 9f49d954a2837946b5fd1ba8e53c0d8a25e52f51 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 16 Aug 2022 12:44:03 -0500 Subject: [PATCH 02/22] Multiple /arg instead of /mainArgs --- Source/Dafny/DafnyOptions.cs | 5 ++--- Test/comp/CompileWithArguments.dfy | 10 +++++----- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 191982ecab4..30d67ffe84c 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -310,10 +310,9 @@ protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) { return true; } - case "mainArgs": - case "MainArgs": { + case "arg": { if (ps.ConfirmArgumentCount(1)) { - MainArgs.AddRange(ParseInnerArguments(args[ps.i])); + MainArgs.Add(args[ps.i]); } return true; diff --git a/Test/comp/CompileWithArguments.dfy b/Test/comp/CompileWithArguments.dfy index e52eb0e5d41..054002ed55c 100644 --- a/Test/comp/CompileWithArguments.dfy +++ b/Test/comp/CompileWithArguments.dfy @@ -1,9 +1,9 @@ // RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "/mainArgs:csharp 1" "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js "/mainArgs:javascript 2" "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "/mainArgs:\"go go\" 1" "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java "/mainArgs:java heya" "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:py "/mainArgs:python 1" "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /arg:csharp /arg:1 "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:js /arg:javascript /arg:2 "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:go "/arg:go go" /arg:1 "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:java /arg:java /arg:heya "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:py "/arg:python /arg:1 "%s" >> "%t" // RUN: %dafny /noVerify /compile:2 /compileTarget:cs "%s" /out:CompileWithArgument.dll // RUN: %dotnet CompileWithArgument.dll "ellel" 2 >> "%t" // RUN: %dotnet CompileWithArgument.dll "on the go" 1 >> "%t" From bf5b81cef525239b34a0f05156eb90f685aad422 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 16 Aug 2022 14:15:14 -0500 Subject: [PATCH 03/22] Works for Java as well --- Source/Dafny/Compilers/Compiler-Csharp.cs | 4 ++-- Source/Dafny/Compilers/Compiler-cpp.cs | 4 ++-- Source/Dafny/Compilers/Compiler-go.cs | 3 ++- Source/Dafny/Compilers/Compiler-java.cs | 11 ++++++----- Source/Dafny/Compilers/Compiler-js.cs | 4 ++-- Source/Dafny/Compilers/Compiler-python.cs | 4 ++-- Source/Dafny/Compilers/SinglePassCompiler.cs | 11 +++++++---- Source/Dafny/DafnyOptions.cs | 3 +++ 8 files changed, 26 insertions(+), 18 deletions(-) diff --git a/Source/Dafny/Compilers/Compiler-Csharp.cs b/Source/Dafny/Compilers/Compiler-Csharp.cs index 2cf2c95f4c0..c8b92f10664 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, 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(string[] {argsParameterName})"); } protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string /*?*/ libraryName, ConcreteSyntaxTree wr) { diff --git a/Source/Dafny/Compilers/Compiler-cpp.cs b/Source/Dafny/Compilers/Compiler-cpp.cs index 4e7566e02f2..c4e7f68da28 100644 --- a/Source/Dafny/Compilers/Compiler-cpp.cs +++ b/Source/Dafny/Compilers/Compiler-cpp.cs @@ -149,9 +149,9 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete 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(int argc, char *{argsParameterName}[])"); } protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) { diff --git a/Source/Dafny/Compilers/Compiler-go.cs b/Source/Dafny/Compilers/Compiler-go.cs index 46fb809a030..e60997e6936 100644 --- a/Source/Dafny/Compilers/Compiler-go.cs +++ b/Source/Dafny/Compilers/Compiler-go.cs @@ -130,8 +130,9 @@ 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; + argsParameterName = "os.Args[1:]"; return wr.NewNamedBlock("func (_this * {0}) Main()", FormatCompanionTypeName(((GoCompiler.ClassWriter)cw).ClassName)); } diff --git a/Source/Dafny/Compilers/Compiler-java.cs b/Source/Dafny/Compilers/Compiler-java.cs index 52c4c5868f8..63102af7407 100644 --- a/Source/Dafny/Compilers/Compiler-java.cs +++ b/Source/Dafny/Compilers/Compiler-java.cs @@ -342,8 +342,9 @@ 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);"); - Coverage.EmitTearDown(wBody); + wBody.WriteLine($"dafny.DafnySequence[] dafnyArgs = new dafny.DafnySequence[args.length];"); + wBody.WriteLine($"for(int i = 0; i < args.length; i++) dafnyArgs[i] = dafny.DafnySequence.asString(args[i]);"); + wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling(() -> {{ {companion}.__Main(dafnyArgs); }} );"); } void EmitImports(ConcreteSyntaxTree wr, out ConcreteSyntaxTree importWriter) { @@ -2279,7 +2280,7 @@ 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", Path.GetFileNameWithoutExtension(targetFilename) + " " + DafnyOptions.O.MainArgsString) { CreateNoWindow = true, UseShellExecute = false, RedirectStandardOutput = true, @@ -3996,9 +3997,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[] {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 7cb0615425f..537b3c4914d 100644 --- a/Source/Dafny/Compilers/Compiler-js.cs +++ b/Source/Dafny/Compilers/Compiler-js.cs @@ -56,9 +56,9 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete 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) { diff --git a/Source/Dafny/Compilers/Compiler-python.cs b/Source/Dafny/Compilers/Compiler-python.cs index 9e093622fed..6104672499b 100644 --- a/Source/Dafny/Compilers/Compiler-python.cs +++ b/Source/Dafny/Compilers/Compiler-python.cs @@ -88,8 +88,8 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete .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, diff --git a/Source/Dafny/Compilers/SinglePassCompiler.cs b/Source/Dafny/Compilers/SinglePassCompiler.cs index 86ea2cc0ca3..d21b05dedf8 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, ref string argsParameterName); protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr); protected abstract string GetHelperModuleName(); protected interface IClassWriter { @@ -2371,6 +2371,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); @@ -2407,7 +2409,8 @@ private void CompileMethod(Program program, Method m, IClassWriter cw, bool look } if (m == program.MainMethod && IssueCreateStaticMain(m)) { - w = CreateStaticMain(cw); + var args_name = STATIC_ARGS_NAME; + w = CreateStaticMain(cw, ref args_name); var ty = UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(m.EnclosingClass); LocalVariable receiver = null; if (!m.IsStatic) { @@ -2432,8 +2435,8 @@ private void CompileMethod(Program program, Method m, IClassWriter cw, bool look w.Write("{0}.", companion); } EmitNameAndActualTypeArgs(IdName(m), TypeArgumentInstantiation.ToActuals(ForTypeParameters(typeArgs, m, false)), m.tok, w); - w.Write("("); - var sep = ""; + w.Write("(" + args_name); + var sep = ", "; if (receiver != null && customReceiver) { w.Write("{0}", IdName(receiver)); sep = ", "; diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 30d67ffe84c..b7bc376bb67 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -185,6 +185,9 @@ public void CopyTo(DafnyOptions dst) { public virtual TestGenerationOptions TestGenOptions => testGenOptions ??= new TestGenerationOptions(); + public string MainArgsString => + string.Join(" ", MainArgs.Select(x => x.Replace(@"\", @"\\").Replace(@"""", @"\\"""))); + protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) { var args = ps.args; // convenient synonym switch (name) { From 9413f531afe8fe1792203b54211cc2af9c6c5dcf Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 16 Aug 2022 14:35:16 -0500 Subject: [PATCH 04/22] Support for compiled tests --- RELEASE_NOTES.md | 1 + Source/Dafny/Compilers/Compiler-java.cs | 1 + Test/comp/CompileWithArguments.dfy | 14 +++++++------- Test/comp/CompileWithArguments.dfy.expect | 10 +++++----- 4 files changed, 14 insertions(+), 12 deletions(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 39f98b93a65..47f7d649198 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,5 +1,6 @@ # Upcoming +- feat: Command-line arguments available from Main() in Dafny programs (https://github.com/dafny-lang/dafny/pull/2594) - fix: Use the right bitvector comparison in decrease checks (https://github.com/dafny-lang/dafny/pull/2512) - fix: Don't use native division and modulo operators for non-native int-based newtypes in Java and C#. diff --git a/Source/Dafny/Compilers/Compiler-java.cs b/Source/Dafny/Compilers/Compiler-java.cs index 63102af7407..5c6e90603ae 100644 --- a/Source/Dafny/Compilers/Compiler-java.cs +++ b/Source/Dafny/Compilers/Compiler-java.cs @@ -342,6 +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(@"@SuppressWarnings(""unchecked"")"); wBody.WriteLine($"dafny.DafnySequence[] dafnyArgs = new dafny.DafnySequence[args.length];"); wBody.WriteLine($"for(int i = 0; i < args.length; i++) dafnyArgs[i] = dafny.DafnySequence.asString(args[i]);"); wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling(() -> {{ {companion}.__Main(dafnyArgs); }} );"); diff --git a/Test/comp/CompileWithArguments.dfy b/Test/comp/CompileWithArguments.dfy index 054002ed55c..6a8105d1d00 100644 --- a/Test/comp/CompileWithArguments.dfy +++ b/Test/comp/CompileWithArguments.dfy @@ -1,13 +1,13 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs /arg:csharp /arg:1 "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /arg:javascript /arg:2 "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "/arg:go go" /arg:1 "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java /arg:java /arg:heya "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:py "/arg:python /arg:1 "%s" >> "%t" -// RUN: %dafny /noVerify /compile:2 /compileTarget:cs "%s" /out:CompileWithArgument.dll -// RUN: %dotnet CompileWithArgument.dll "ellel" 2 >> "%t" -// RUN: %dotnet CompileWithArgument.dll "on the go" 1 >> "%t" -// RUN: %dotnet CompileWithArgument.dll "dll" "Aloha from" >> "%t" +// RN: %dafny /noVerify /compile:4 /compileTarget:js /arg:javascript /arg:2 "%s" >> "%t" +// RN: %dafny /noVerify /compile:4 /compileTarget:go "/arg:go go" /arg:1 "%s" >> "%t" +// RN: %dafny /noVerify /compile:4 /compileTarget:py "/arg:python /arg:1 "%s" >> "%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: array) { diff --git a/Test/comp/CompileWithArguments.dfy.expect b/Test/comp/CompileWithArguments.dfy.expect index 5bcf851ad0a..a6ecdcc8970 100644 --- a/Test/comp/CompileWithArguments.dfy.expect +++ b/Test/comp/CompileWithArguments.dfy.expect @@ -1,21 +1,21 @@ -Dafny program verifier finished with 6 verified, 0 errors +Dafny program verifier finished with 1 verified, 0 errors Dafny program verifier did not attempt verification Hello csharp Dafny program verifier did not attempt verification -Howdy javascript +heya java Dafny program verifier did not attempt verification -Hello go go +Howdy javascript Dafny program verifier did not attempt verification -Heya java +Hello go go Dafny program verifier did not attempt verification Hello Python Howdy ellel Hello on the go -Aloha from dll \ No newline at end of file +Aloha from dll From 7e99661b371602eb7192abdb66fb928ca68b14bb Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 16 Aug 2022 14:47:28 -0500 Subject: [PATCH 05/22] Documentation options --- Source/Dafny/DafnyOptions.cs | 3 +++ docs/DafnyRef/Options.txt | 5 ++++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index b7bc376bb67..3df8643ca5a 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -1283,6 +1283,9 @@ verification outcome /Main: 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'. +/arg: (repeated) + When running the dafny program through /compile:3 or /compile:4, each individual + becomes an element of the array provided to the main function /runAllTests: (experimental) 0 (default) - Annotates compiled methods with the {{:test}} attribute such that they can be tested using a testing framework diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index 744167901fd..fcab8f6aeaa 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -324,6 +324,9 @@ Usage: Dafny [ option ... ] [ filename ... ] /Main: 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'. + /arg: (repeated) + When running the dafny program through /compile:3 or /compile:4, each individual + becomes an element of the array provided to the main function /runAllTests: (experimental) 0 (default) - Annotates compiled methods with the {:test} attribute such that they can be tested using a testing framework @@ -713,4 +716,4 @@ Usage: Dafny [ option ... ] [ filename ... ] 2 - print to stderr /restartProver Restart the prover after each query -``` +``` \ No newline at end of file From c53df3d880317fa89fff58535abb58b3833bf6db Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 16 Aug 2022 15:04:30 -0500 Subject: [PATCH 06/22] Support for js --- Source/Dafny/Compilers/Compiler-js.cs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/Source/Dafny/Compilers/Compiler-js.cs b/Source/Dafny/Compilers/Compiler-js.cs index 537b3c4914d..15fa473691b 100644 --- a/Source/Dafny/Compilers/Compiler-js.cs +++ b/Source/Dafny/Compilers/Compiler-js.cs @@ -52,7 +52,7 @@ 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.slice(1)));", mainMethod.EnclosingClass.FullCompileName, mainMethod.IsStatic ? IdName(mainMethod) : "Main"); Coverage.EmitTearDown(wr); } @@ -2442,6 +2442,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); @@ -2462,6 +2468,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(); From b3088992737bc349107738cc9a2d4c68de749bc8 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 17 Aug 2022 10:19:33 -0500 Subject: [PATCH 07/22] Support for go with arguments --- Source/Dafny/Compilers/Compiler-go.cs | 15 ++++++++++++--- Source/Dafny/Compilers/Compiler-java.cs | 2 +- Source/Dafny/Compilers/Compiler-python.cs | 7 ++++--- Source/Dafny/DafnyOptions.cs | 6 ++++-- Source/DafnyDriver/DafnyDriver.cs | 2 +- Test/comp/CompileWithArguments.dfy | 6 +++--- Test/comp/CompileWithArguments.dfy.expect | 5 ++--- 7 files changed, 27 insertions(+), 16 deletions(-) diff --git a/Source/Dafny/Compilers/Compiler-go.cs b/Source/Dafny/Compilers/Compiler-go.cs index e60997e6936..74beb0d3e37 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,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)-1"); + wBody.WriteLine($"var {dafnyArgs} []interface{{}} = make([]interface{{}}, size)"); + wBody.WriteLine($"for i, item := range os.Args[1:] {{ {dafnyArgs}[i] = {GetHelperModuleName()}.SeqOfString(item) }}"); + wBody.WriteLine("{0}.{1}({2}.NewArrayWithValues({3}...))", companion, idName, GetHelperModuleName(), dafnyArgs); Coverage.EmitTearDown(wBody); } @@ -197,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); + } } } @@ -3604,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, diff --git a/Source/Dafny/Compilers/Compiler-java.cs b/Source/Dafny/Compilers/Compiler-java.cs index 5c6e90603ae..0314d44611d 100644 --- a/Source/Dafny/Compilers/Compiler-java.cs +++ b/Source/Dafny/Compilers/Compiler-java.cs @@ -2281,7 +2281,7 @@ 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) + " " + DafnyOptions.O.MainArgsString) { + var psi = new ProcessStartInfo("java", Path.GetFileNameWithoutExtension(targetFilename) + DafnyOptions.O.ArgsStringExtra) { CreateNoWindow = true, UseShellExecute = false, RedirectStandardOutput = true, diff --git a/Source/Dafny/Compilers/Compiler-python.cs b/Source/Dafny/Compilers/Compiler-python.cs index 6104672499b..2c9258f8f61 100644 --- a/Source/Dafny/Compilers/Compiler-python.cs +++ b/Source/Dafny/Compilers/Compiler-python.cs @@ -82,8 +82,10 @@ 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[1:]]") + .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\")"); } @@ -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 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, diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 3df8643ca5a..d4ece83d4e5 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -185,8 +185,10 @@ public void CopyTo(DafnyOptions dst) { public virtual TestGenerationOptions TestGenOptions => testGenOptions ??= new TestGenerationOptions(); - public string MainArgsString => - string.Join(" ", MainArgs.Select(x => x.Replace(@"\", @"\\").Replace(@"""", @"\\"""))); + public string ArgsStringExtra => + string.Join("", MainArgs.Select(x => " " + + (!x.Contains(" ") ? x : + "\"" + x.Replace(@"\", @"\\").Replace(@"""", @"\\""") + "\""))); protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) { var args = ps.args; // convenient synonym diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 95c2c75a85b..94f1e8e9071 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -179,7 +179,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/Test/comp/CompileWithArguments.dfy b/Test/comp/CompileWithArguments.dfy index 6a8105d1d00..3f072bbd75f 100644 --- a/Test/comp/CompileWithArguments.dfy +++ b/Test/comp/CompileWithArguments.dfy @@ -1,9 +1,9 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs /arg:csharp /arg:1 "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java /arg:java /arg:heya "%s" >> "%t" -// RN: %dafny /noVerify /compile:4 /compileTarget:js /arg:javascript /arg:2 "%s" >> "%t" -// RN: %dafny /noVerify /compile:4 /compileTarget:go "/arg:go go" /arg:1 "%s" >> "%t" -// RN: %dafny /noVerify /compile:4 /compileTarget:py "/arg:python /arg:1 "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:js /arg:javascript /arg:2 "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:py /arg:python /arg:1 "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:go "/arg:go go" /arg:1 "%s" >> "%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" diff --git a/Test/comp/CompileWithArguments.dfy.expect b/Test/comp/CompileWithArguments.dfy.expect index a6ecdcc8970..23568951bde 100644 --- a/Test/comp/CompileWithArguments.dfy.expect +++ b/Test/comp/CompileWithArguments.dfy.expect @@ -11,11 +11,10 @@ Dafny program verifier did not attempt verification Howdy javascript Dafny program verifier did not attempt verification -Hello go go +Hello python Dafny program verifier did not attempt verification -Hello Python - +Hello go go Howdy ellel Hello on the go Aloha from dll From aa57f695dd38b4003ca3a2121f54c35a4cb7a7b8 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 17 Aug 2022 10:27:48 -0500 Subject: [PATCH 08/22] Tested the first failing error message --- Source/Dafny/Compilers/SinglePassCompiler.cs | 2 +- Test/comp/CompileWithArgumentsFail.dfy | 7 +++++++ Test/comp/CompileWithArgumentsFail.dfy.expect | 5 +++++ 3 files changed, 13 insertions(+), 1 deletion(-) create mode 100644 Test/comp/CompileWithArgumentsFail.dfy create mode 100644 Test/comp/CompileWithArgumentsFail.dfy.expect diff --git a/Source/Dafny/Compilers/SinglePassCompiler.cs b/Source/Dafny/Compilers/SinglePassCompiler.cs index d21b05dedf8..534486bb9e5 100644 --- a/Source/Dafny/Compilers/SinglePassCompiler.cs +++ b/Source/Dafny/Compilers/SinglePassCompiler.cs @@ -1681,7 +1681,7 @@ public static bool IsPermittedAsMain(Method m, out String reason) { typeOfUniqueFormal.TypeArgs.Count != 1 || typeOfUniqueFormal.TypeArgs[0].AsSeqType is not { } seqType || !seqType.Arg.IsCharType) { - reason = "the method's non-ghost argument type should be an array, got " + typeOfUniqueFormal.TypeArgs[0]; + reason = "the method's non-ghost argument type should be an array, got " + typeOfUniqueFormal; return false; } } diff --git a/Test/comp/CompileWithArgumentsFail.dfy b/Test/comp/CompileWithArgumentsFail.dfy new file mode 100644 index 00000000000..4aa0d291cdf --- /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 /arg:csharp /arg:1 "%s" >> "%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..33556852cd2 --- /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 array, got int). From e86a74a3b0e761e842a71dd085428e3f041b6381 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 17 Aug 2022 10:30:22 -0500 Subject: [PATCH 09/22] Second test for checking failure --- Test/comp/CompileWithArgumentsFail2.dfy | 7 +++++++ Test/comp/CompileWithArgumentsFail2.dfy.expect | 5 +++++ 2 files changed, 12 insertions(+) create mode 100644 Test/comp/CompileWithArgumentsFail2.dfy create mode 100644 Test/comp/CompileWithArgumentsFail2.dfy.expect diff --git a/Test/comp/CompileWithArgumentsFail2.dfy b/Test/comp/CompileWithArgumentsFail2.dfy new file mode 100644 index 00000000000..01d962dc207 --- /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 /arg:csharp /arg:1 "%s" >> "%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). From e159db4255e97abe35a3e5c51b65f6dd14dfa2c9 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 17 Aug 2022 11:58:44 -0500 Subject: [PATCH 10/22] Support for no-arg main --- Source/Dafny/Compilers/SinglePassCompiler.cs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/Source/Dafny/Compilers/SinglePassCompiler.cs b/Source/Dafny/Compilers/SinglePassCompiler.cs index 534486bb9e5..be859da568a 100644 --- a/Source/Dafny/Compilers/SinglePassCompiler.cs +++ b/Source/Dafny/Compilers/SinglePassCompiler.cs @@ -1530,7 +1530,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; @@ -1570,7 +1570,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; @@ -1611,7 +1611,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 { @@ -1624,7 +1624,7 @@ 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 @@ -1684,6 +1684,11 @@ typeOfUniqueFormal.TypeArgs[0].AsSeqType is not { } seqType || reason = "the method's non-ghost argument type should be an array, got " + typeOfUniqueFormal; return false; } + } else { + // Need to manually insert the args. + var argsType = program.BuiltIns.ArrayType(1, new SeqType(new CharType()), true); + argsType.ResolvedClass = new ArrayClassDecl(1, program.DefaultModuleDef, null); + 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"; From 37a3e817e1f9903c155bc49b8fef2dee63a67d5b Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 23 Aug 2022 12:06:14 -0500 Subject: [PATCH 11/22] Works for c#, C++, Java, Go --- Source/Dafny/Compilers/Compiler-Csharp.cs | 2 +- Source/Dafny/Compilers/Compiler-cpp.cs | 13 +++++++++---- Source/Dafny/Compilers/Compiler-go.cs | 3 ++- Source/Dafny/Compilers/Compiler-java.cs | 11 +++++++---- Source/Dafny/Compilers/SinglePassCompiler.cs | 12 +++++------- Test/comp/CompileWithArguments.dfy | 7 ++++--- Test/comp/CompileWithArguments.dfy.expect | 3 +++ 7 files changed, 31 insertions(+), 20 deletions(-) diff --git a/Source/Dafny/Compilers/Compiler-Csharp.cs b/Source/Dafny/Compilers/Compiler-Csharp.cs index c8b92f10664..079736888ee 100644 --- a/Source/Dafny/Compilers/Compiler-Csharp.cs +++ b/Source/Dafny/Compilers/Compiler-Csharp.cs @@ -3328,7 +3328,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete Coverage.EmitSetup(wBody); wBody.WriteLine($"Dafny.ISequence[] dafnyArgs = new Dafny.ISequence[args.Length];"); wBody.WriteLine($"for(var i = 0; i < args.Length; i++) dafnyArgs[i] = Dafny.Sequence.FromString(args[i]);"); - wBody.WriteLine($"{GetHelperModuleName()}.WithHaltHandling(() => {companion}.{idName}(dafnyArgs));"); + wBody.WriteLine($"{GetHelperModuleName()}.WithHaltHandling(() => {companion}.{idName}(Dafny.Sequence>.FromArray(dafnyArgs)));"); Coverage.EmitTearDown(wBody); } diff --git a/Source/Dafny/Compilers/Compiler-cpp.cs b/Source/Dafny/Compilers/Compiler-cpp.cs index c4e7f68da28..4d10187fbd2 100644 --- a/Source/Dafny/Compilers/Compiler-cpp.cs +++ b/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> dafnyArgs((uint64)argc - 1);"); + tryWr.WriteLine("for(int i = 1; i < argc; i++) {"); + tryWr.WriteLine(" std::string s = argv[i];"); + tryWr.WriteLine(" dafnyArgs.start[i-1] = 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, ref string argsParameterName) { var wr = (cw as CppCompiler.ClassWriter).MethodWriter; - return wr.NewBlock($"int main(int argc, char *{argsParameterName}[])"); + return wr.NewBlock($"int main(DafnySequence> {argsParameterName})"); } protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string/*?*/ libraryName, ConcreteSyntaxTree wr) { @@ -2497,7 +2502,7 @@ 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(ComputeExeName(targetFilename)) { + var psi = new ProcessStartInfo(ComputeExeName(targetFilename), DafnyOptions.O.ArgsStringExtra) { CreateNoWindow = true, UseShellExecute = false, RedirectStandardOutput = true, diff --git a/Source/Dafny/Compilers/Compiler-go.cs b/Source/Dafny/Compilers/Compiler-go.cs index 74beb0d3e37..ee646dd1a9e 100644 --- a/Source/Dafny/Compilers/Compiler-go.cs +++ b/Source/Dafny/Compilers/Compiler-go.cs @@ -123,7 +123,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete wBody.WriteLine("var size = len(os.Args)-1"); wBody.WriteLine($"var {dafnyArgs} []interface{{}} = make([]interface{{}}, size)"); wBody.WriteLine($"for i, item := range os.Args[1:] {{ {dafnyArgs}[i] = {GetHelperModuleName()}.SeqOfString(item) }}"); - wBody.WriteLine("{0}.{1}({2}.NewArrayWithValues({3}...))", companion, idName, GetHelperModuleName(), dafnyArgs); + wBody.WriteLine("{0}.{1}({2}.SeqOf({3}...))", companion, idName, GetHelperModuleName(), dafnyArgs); Coverage.EmitTearDown(wBody); } @@ -3614,6 +3614,7 @@ private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, } var args = string.Format("{0} \"{1}\"", verb, targetFilename) + DafnyOptions.O.ArgsStringExtra; + Console.Write(args); var psi = new ProcessStartInfo("go", args) { CreateNoWindow = Environment.OSVersion.Platform != PlatformID.Win32NT, UseShellExecute = false, diff --git a/Source/Dafny/Compilers/Compiler-java.cs b/Source/Dafny/Compilers/Compiler-java.cs index 0314d44611d..3179ddd8670 100644 --- a/Source/Dafny/Compilers/Compiler-java.cs +++ b/Source/Dafny/Compilers/Compiler-java.cs @@ -343,9 +343,11 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete companion = modName + companion; Coverage.EmitSetup(wBody); wBody.WriteLine(@"@SuppressWarnings(""unchecked"")"); - wBody.WriteLine($"dafny.DafnySequence[] dafnyArgs = new dafny.DafnySequence[args.length];"); - wBody.WriteLine($"for(int i = 0; i < args.length; i++) dafnyArgs[i] = dafny.DafnySequence.asString(args[i]);"); - wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling(() -> {{ {companion}.__Main(dafnyArgs); }} );"); + wBody.WriteLine($"dafny.TypeDescriptor> type = dafny.DafnySequence._typeDescriptor(dafny.TypeDescriptor.CHAR);"); + wBody.WriteLine($"dafny.Array> dafnyArgs = dafny.Array.newArray(type, args.length);"); + wBody.WriteLine($"for (int i = 0; i < args.length; i++) dafnyArgs.set(i, dafny.DafnySequence.asString(args[i]));"); + wBody.WriteLine($"dafny.DafnySequence> result = dafny.DafnySequence.fromArray(type, dafnyArgs);"); + wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling(() -> {{ {companion}.__Main(result); }} );"); } void EmitImports(ConcreteSyntaxTree wr, out ConcreteSyntaxTree importWriter) { @@ -2252,6 +2254,7 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target files.Add($"\"{Path.GetFullPath(file)}\""); } var classpath = GetClassPath(targetFilename); + Console.Write("javac " + string.Join(" ", files)); var psi = new ProcessStartInfo("javac", string.Join(" ", files)) { CreateNoWindow = true, UseShellExecute = false, @@ -4000,7 +4003,7 @@ protected override bool IssueCreateStaticMain(Method m) { } protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, ref string argsParameterName) { var wr = ((ClassWriter)cw).StaticMemberWriter; - return wr.NewBlock($"public static void __Main(dafny.DafnySequence[] {argsParameterName})"); + 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/SinglePassCompiler.cs b/Source/Dafny/Compilers/SinglePassCompiler.cs index be859da568a..6663b7dddd3 100644 --- a/Source/Dafny/Compilers/SinglePassCompiler.cs +++ b/Source/Dafny/Compilers/SinglePassCompiler.cs @@ -1677,17 +1677,15 @@ public static bool IsPermittedAsMain(Program program, Method m, out String reaso return false; } var typeOfUniqueFormal = nonGhostFormals[0].Type.NormalizeExpandKeepConstraints(); - if (!typeOfUniqueFormal.IsArrayType || - typeOfUniqueFormal.TypeArgs.Count != 1 || - typeOfUniqueFormal.TypeArgs[0].AsSeqType is not { } seqType || - !seqType.Arg.IsCharType) { - reason = "the method's non-ghost argument type should be an array, got " + typeOfUniqueFormal; + 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 = program.BuiltIns.ArrayType(1, new SeqType(new CharType()), true); - argsType.ResolvedClass = new ArrayClassDecl(1, program.DefaultModuleDef, null); + 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)) { diff --git a/Test/comp/CompileWithArguments.dfy b/Test/comp/CompileWithArguments.dfy index 3f072bbd75f..d96d64435ed 100644 --- a/Test/comp/CompileWithArguments.dfy +++ b/Test/comp/CompileWithArguments.dfy @@ -1,5 +1,6 @@ // RUN: %dafny /compile:0 "%s" > "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:cs /arg:csharp /arg:1 "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:cpp /arg:cpp /arg:Yipee "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:java /arg:java /arg:heya "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:js /arg:javascript /arg:2 "%s" >> "%t" // RUN: %dafny /noVerify /compile:4 /compileTarget:py /arg:python /arg:1 "%s" >> "%t" @@ -10,9 +11,9 @@ // RUN: dotnet %s.dll "dll" "Aloha from" >> "%t" // RUN: %diff "%s.expect" "%t" -method Main(args: array) { - if args.Length != 2 { - print "Expected 2 arguments, got ", args.Length; +method Main(args: seq) { + if |args| != 2 { + print "Expected 2 arguments, got ", |args|; } else { if args[1] == "1" { print "Hello ",args[0], "\n"; diff --git a/Test/comp/CompileWithArguments.dfy.expect b/Test/comp/CompileWithArguments.dfy.expect index 23568951bde..7ad0c9afa60 100644 --- a/Test/comp/CompileWithArguments.dfy.expect +++ b/Test/comp/CompileWithArguments.dfy.expect @@ -4,6 +4,9 @@ Dafny program verifier finished with 1 verified, 0 errors Dafny program verifier did not attempt verification Hello csharp +Dafny program verifier did not attempt verification +Yipee cpp + Dafny program verifier did not attempt verification heya java From b0805874f8c88ecac7b157b30b3d9a582dfd86e5 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 23 Aug 2022 12:32:22 -0500 Subject: [PATCH 12/22] Fixed support for C++ --- Source/Dafny/Compilers/Compiler-cpp.cs | 7 ++++++- Source/Dafny/Compilers/Compiler-go.cs | 1 - Source/Dafny/Compilers/Compiler-java.cs | 1 - 3 files changed, 6 insertions(+), 3 deletions(-) diff --git a/Source/Dafny/Compilers/Compiler-cpp.cs b/Source/Dafny/Compilers/Compiler-cpp.cs index 4d10187fbd2..5d87835abb8 100644 --- a/Source/Dafny/Compilers/Compiler-cpp.cs +++ b/Source/Dafny/Compilers/Compiler-cpp.cs @@ -1151,7 +1151,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; } diff --git a/Source/Dafny/Compilers/Compiler-go.cs b/Source/Dafny/Compilers/Compiler-go.cs index ee646dd1a9e..ded5c55645f 100644 --- a/Source/Dafny/Compilers/Compiler-go.cs +++ b/Source/Dafny/Compilers/Compiler-go.cs @@ -3614,7 +3614,6 @@ private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, } var args = string.Format("{0} \"{1}\"", verb, targetFilename) + DafnyOptions.O.ArgsStringExtra; - Console.Write(args); var psi = new ProcessStartInfo("go", args) { CreateNoWindow = Environment.OSVersion.Platform != PlatformID.Win32NT, UseShellExecute = false, diff --git a/Source/Dafny/Compilers/Compiler-java.cs b/Source/Dafny/Compilers/Compiler-java.cs index 3179ddd8670..37d49dbdd76 100644 --- a/Source/Dafny/Compilers/Compiler-java.cs +++ b/Source/Dafny/Compilers/Compiler-java.cs @@ -2254,7 +2254,6 @@ public override bool CompileTargetProgram(string dafnyProgramName, string target files.Add($"\"{Path.GetFullPath(file)}\""); } var classpath = GetClassPath(targetFilename); - Console.Write("javac " + string.Join(" ", files)); var psi = new ProcessStartInfo("javac", string.Join(" ", files)) { CreateNoWindow = true, UseShellExecute = false, From af0f559ba48b34b1b374e6faac7eedb1ee21ac0b Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 23 Aug 2022 13:11:37 -0500 Subject: [PATCH 13/22] Count the first argument --- Source/Dafny/Compilers/Compiler-Csharp.cs | 5 +++-- Source/Dafny/Compilers/Compiler-cpp.cs | 6 +++--- Source/Dafny/Compilers/Compiler-go.cs | 4 ++-- Source/Dafny/Compilers/Compiler-java.cs | 5 +++-- Source/Dafny/Compilers/Compiler-js.cs | 2 +- Source/Dafny/Compilers/Compiler-python.cs | 2 +- Test/comp/CompileWithArguments.dfy | 20 ++++++++++++------- Test/comp/CompileWithArguments.dfy.expect | 18 ++++++++--------- Test/comp/CompileWithArgumentsFail.dfy.expect | 2 +- 9 files changed, 36 insertions(+), 28 deletions(-) diff --git a/Source/Dafny/Compilers/Compiler-Csharp.cs b/Source/Dafny/Compilers/Compiler-Csharp.cs index 079736888ee..ecc16ae0156 100644 --- a/Source/Dafny/Compilers/Compiler-Csharp.cs +++ b/Source/Dafny/Compilers/Compiler-Csharp.cs @@ -3326,8 +3326,9 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete var idName = IssueCreateStaticMain(mainMethod) ? "_StaticMain" : IdName(mainMethod); Coverage.EmitSetup(wBody); - wBody.WriteLine($"Dafny.ISequence[] dafnyArgs = new Dafny.ISequence[args.Length];"); - wBody.WriteLine($"for(var i = 0; i < args.Length; i++) dafnyArgs[i] = Dafny.Sequence.FromString(args[i]);"); + wBody.WriteLine($"Dafny.ISequence[] dafnyArgs = new Dafny.ISequence[args.Length + 1];"); + wBody.WriteLine($"dafnyArgs[0] = Dafny.Sequence.FromString(\"dotnet\");"); + wBody.WriteLine($"for(var i = 0; i < args.Length; i++) dafnyArgs[i+1] = Dafny.Sequence.FromString(args[i]);"); wBody.WriteLine($"{GetHelperModuleName()}.WithHaltHandling(() => {companion}.{idName}(Dafny.Sequence>.FromArray(dafnyArgs)));"); Coverage.EmitTearDown(wBody); } diff --git a/Source/Dafny/Compilers/Compiler-cpp.cs b/Source/Dafny/Compilers/Compiler-cpp.cs index 5d87835abb8..f7ed302fc02 100644 --- a/Source/Dafny/Compilers/Compiler-cpp.cs +++ b/Source/Dafny/Compilers/Compiler-cpp.cs @@ -144,10 +144,10 @@ protected override void EmitFooter(Program program, ConcreteSyntaxTree wr) { public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) { var w = wr.NewBlock("int main(int argc, char *argv[])"); var tryWr = w.NewBlock("try"); - tryWr.WriteLine("DafnySequence> dafnyArgs((uint64)argc - 1);"); - tryWr.WriteLine("for(int i = 1; i < argc; i++) {"); + tryWr.WriteLine("DafnySequence> dafnyArgs((uint64)argc);"); + tryWr.WriteLine("for(int i = 0; i < argc; i++) {"); tryWr.WriteLine(" std::string s = argv[i];"); - tryWr.WriteLine(" dafnyArgs.start[i-1] = DafnySequenceFromString(s);"); + 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)"); diff --git a/Source/Dafny/Compilers/Compiler-go.cs b/Source/Dafny/Compilers/Compiler-go.cs index ded5c55645f..ec9bd107caa 100644 --- a/Source/Dafny/Compilers/Compiler-go.cs +++ b/Source/Dafny/Compilers/Compiler-go.cs @@ -120,9 +120,9 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete Coverage.EmitSetup(wBody); var dafnyArgs = "dafnyArgs"; - wBody.WriteLine("var size = len(os.Args)-1"); + wBody.WriteLine("var size = len(os.Args)"); wBody.WriteLine($"var {dafnyArgs} []interface{{}} = make([]interface{{}}, size)"); - wBody.WriteLine($"for i, item := range os.Args[1:] {{ {dafnyArgs}[i] = {GetHelperModuleName()}.SeqOfString(item) }}"); + 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); } diff --git a/Source/Dafny/Compilers/Compiler-java.cs b/Source/Dafny/Compilers/Compiler-java.cs index 37d49dbdd76..dc22c95b28c 100644 --- a/Source/Dafny/Compilers/Compiler-java.cs +++ b/Source/Dafny/Compilers/Compiler-java.cs @@ -344,8 +344,9 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete Coverage.EmitSetup(wBody); wBody.WriteLine(@"@SuppressWarnings(""unchecked"")"); wBody.WriteLine($"dafny.TypeDescriptor> type = dafny.DafnySequence._typeDescriptor(dafny.TypeDescriptor.CHAR);"); - wBody.WriteLine($"dafny.Array> dafnyArgs = dafny.Array.newArray(type, args.length);"); - wBody.WriteLine($"for (int i = 0; i < args.length; i++) dafnyArgs.set(i, dafny.DafnySequence.asString(args[i]));"); + wBody.WriteLine($"dafny.Array> 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> result = dafny.DafnySequence.fromArray(type, dafnyArgs);"); wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling(() -> {{ {companion}.__Main(result); }} );"); } diff --git a/Source/Dafny/Compilers/Compiler-js.cs b/Source/Dafny/Compilers/Compiler-js.cs index 15fa473691b..347939329f1 100644 --- a/Source/Dafny/Compilers/Compiler-js.cs +++ b/Source/Dafny/Compilers/Compiler-js.cs @@ -52,7 +52,7 @@ 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}(require('process').argv.slice(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); } diff --git a/Source/Dafny/Compilers/Compiler-python.cs b/Source/Dafny/Compilers/Compiler-python.cs index 2c9258f8f61..0c9dde83edf 100644 --- a/Source/Dafny/Compilers/Compiler-python.cs +++ b/Source/Dafny/Compilers/Compiler-python.cs @@ -84,7 +84,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete Coverage.EmitSetup(wr); var dafnyArgs = "dafnyArgs"; wr.NewBlockPy("try:") - .WriteLine($"{dafnyArgs} = [{DafnyRuntimeModule}.Seq(a) for a in sys.argv[1:]]") + .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\")"); diff --git a/Test/comp/CompileWithArguments.dfy b/Test/comp/CompileWithArguments.dfy index d96d64435ed..8ccab3f113b 100644 --- a/Test/comp/CompileWithArguments.dfy +++ b/Test/comp/CompileWithArguments.dfy @@ -12,15 +12,21 @@ // RUN: %diff "%s.expect" "%t" method Main(args: seq) { - if |args| != 2 { - print "Expected 2 arguments, got ", |args|; + if |args| != 3 { + print "Expected 3 arguments, got ", |args|; } else { - if args[1] == "1" { - print "Hello ",args[0], "\n"; - } else if args[1] == "2" { - print "Howdy ", args[0], "\n"; + var executable := args[0]; + if |executable| < 24 { + print executable, " says "; } else { - print args[1], " ", args[0], "\n"; + 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 index 7ad0c9afa60..75f8877dc54 100644 --- a/Test/comp/CompileWithArguments.dfy.expect +++ b/Test/comp/CompileWithArguments.dfy.expect @@ -2,22 +2,22 @@ Dafny program verifier finished with 1 verified, 0 errors Dafny program verifier did not attempt verification -Hello csharp +dotnet says Hello csharp Dafny program verifier did not attempt verification -Yipee cpp +Someone says Yipee cpp Dafny program verifier did not attempt verification -heya java +java says heya java Dafny program verifier did not attempt verification -Howdy javascript + says Howdy javascript Dafny program verifier did not attempt verification -Hello python +Someone says Hello python Dafny program verifier did not attempt verification -Hello go go -Howdy ellel -Hello on the go -Aloha from dll +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.expect b/Test/comp/CompileWithArgumentsFail.dfy.expect index 33556852cd2..3660adb6f41 100644 --- a/Test/comp/CompileWithArgumentsFail.dfy.expect +++ b/Test/comp/CompileWithArgumentsFail.dfy.expect @@ -2,4 +2,4 @@ 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 array, got int). +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). From b28e07778d469ceebec3c89d7c54b3e73dfb9abe Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 23 Aug 2022 14:04:25 -0500 Subject: [PATCH 14/22] Fixed the test for main methods everywhere + documentation. --- Source/Dafny/Compilers/Compiler-Csharp.cs | 2 +- Source/Dafny/Compilers/Compiler-go.cs | 4 ++-- Source/Dafny/Compilers/SinglePassCompiler.cs | 5 +++-- docs/DafnyRef/Options.txt | 2 +- 4 files changed, 7 insertions(+), 6 deletions(-) diff --git a/Source/Dafny/Compilers/Compiler-Csharp.cs b/Source/Dafny/Compilers/Compiler-Csharp.cs index ecc16ae0156..d6e50417e60 100644 --- a/Source/Dafny/Compilers/Compiler-Csharp.cs +++ b/Source/Dafny/Compilers/Compiler-Csharp.cs @@ -226,7 +226,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, ref stri 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(string[] {argsParameterName})"); + return wr.NewBlock($"public static void _StaticMain(Dafny.ISequence> {argsParameterName})"); } protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string /*?*/ libraryName, ConcreteSyntaxTree wr) { diff --git a/Source/Dafny/Compilers/Compiler-go.cs b/Source/Dafny/Compilers/Compiler-go.cs index ec9bd107caa..5ea07a91aa3 100644 --- a/Source/Dafny/Compilers/Compiler-go.cs +++ b/Source/Dafny/Compilers/Compiler-go.cs @@ -137,8 +137,8 @@ ConcreteSyntaxTree CreateDescribedSection(string desc, ConcreteSyntaxTree wr, pa protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, ref string argsParameterName) { var wr = ((GoCompiler.ClassWriter)cw).ConcreteMethodWriter; - argsParameterName = "os.Args[1:]"; - 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) { diff --git a/Source/Dafny/Compilers/SinglePassCompiler.cs b/Source/Dafny/Compilers/SinglePassCompiler.cs index 6663b7dddd3..cfdf80a6d18 100644 --- a/Source/Dafny/Compilers/SinglePassCompiler.cs +++ b/Source/Dafny/Compilers/SinglePassCompiler.cs @@ -2438,13 +2438,14 @@ private void CompileMethod(Program program, Method m, IClassWriter cw, bool look w.Write("{0}.", companion); } EmitNameAndActualTypeArgs(IdName(m), TypeArgumentInstantiation.ToActuals(ForTypeParameters(typeArgs, m, false)), m.tok, w); - w.Write("(" + args_name); - var sep = ", "; + w.Write("("); + var sep = ""; if (receiver != null && customReceiver) { w.Write("{0}", IdName(receiver)); sep = ", "; } EmitTypeDescriptorsActuals(ForTypeDescriptors(typeArgs, m, false), m.tok, w, ref sep); + w.Write(sep + args_name); w.Write(")"); EndStmt(w); } diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index fcab8f6aeaa..b13683ac820 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -716,4 +716,4 @@ Usage: Dafny [ option ... ] [ filename ... ] 2 - print to stderr /restartProver Restart the prover after each query -``` \ No newline at end of file +``` From 3089663822f751f4d5d5a78f78d04ed34469426a Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 23 Aug 2022 15:23:06 -0500 Subject: [PATCH 15/22] Fixed branch coverage. --- Source/Dafny/Compilers/Compiler-java.cs | 1 + 1 file changed, 1 insertion(+) diff --git a/Source/Dafny/Compilers/Compiler-java.cs b/Source/Dafny/Compilers/Compiler-java.cs index 56a5d5234e9..2b9363ae056 100644 --- a/Source/Dafny/Compilers/Compiler-java.cs +++ b/Source/Dafny/Compilers/Compiler-java.cs @@ -349,6 +349,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete wBody.WriteLine($"for (int i = 0; i < args.length; i++) dafnyArgs.set(i + 1, dafny.DafnySequence.asString(args[i]));"); wBody.WriteLine($"dafny.DafnySequence> result = dafny.DafnySequence.fromArray(type, dafnyArgs);"); wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling(() -> {{ {companion}.__Main(result); }} );"); + Coverage.EmitTearDown(wBody); } void EmitImports(ConcreteSyntaxTree wr, out ConcreteSyntaxTree importWriter) { From 1805a3d0185ca819b5fb081d2b3b1d9d48facf7e Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Tue, 23 Aug 2022 15:26:08 -0500 Subject: [PATCH 16/22] Fixed hopefully the last test --- Test/git-issues/git-issue-MainE.dfy.expect | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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). From 1d9066f8fc4d453e2953dc080b624d64891d3430 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 24 Aug 2022 13:53:40 -0500 Subject: [PATCH 17/22] New way of entering arguments with '--' --- Source/Dafny/DafnyOptions.cs | 31 ++++++++++++++++--------- Test/comp/CompileWithArguments.dfy | 12 +++++----- Test/comp/CompileWithArgumentsFail.dfy | 2 +- Test/comp/CompileWithArgumentsFail2.dfy | 2 +- docs/DafnyRef/Options.txt | 8 ++++--- 5 files changed, 33 insertions(+), 22 deletions(-) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 102d0a44898..bccd5e59198 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] == "--") { + 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; @@ -313,14 +328,6 @@ protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) { return true; } - case "arg": { - if (ps.ConfirmArgumentCount(1)) { - MainArgs.Add(args[ps.i]); - } - - return true; - } - case "runAllTests": { int runAllTests = 0; if (ps.GetIntArgument(ref runAllTests, 2)) { @@ -1274,9 +1281,11 @@ verification outcome /Main: 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'. -/arg: (repeated) - When running the dafny program through /compile:3 or /compile:4, each individual - becomes an element of the array provided to the main function + A Main method can have at most one (non-ghost) argument of type `seq` +-- ... + When running a Dafny file through /compile:3 or /compile:4, '--' 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/Test/comp/CompileWithArguments.dfy b/Test/comp/CompileWithArguments.dfy index 8ccab3f113b..a885e939a51 100644 --- a/Test/comp/CompileWithArguments.dfy +++ b/Test/comp/CompileWithArguments.dfy @@ -1,10 +1,10 @@ // RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs /arg:csharp /arg:1 "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cpp /arg:cpp /arg:Yipee "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java /arg:java /arg:heya "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js /arg:javascript /arg:2 "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:py /arg:python /arg:1 "%s" >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "/arg:go go" /arg:1 "%s" >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" -- csharp 1 >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:cpp "%s" -- cpp Yipee >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" -- java heya >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" -- javascript 2 >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" -- python 1 >> "%t" +// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" -- "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" diff --git a/Test/comp/CompileWithArgumentsFail.dfy b/Test/comp/CompileWithArgumentsFail.dfy index 4aa0d291cdf..3d932398d4b 100644 --- a/Test/comp/CompileWithArgumentsFail.dfy +++ b/Test/comp/CompileWithArgumentsFail.dfy @@ -1,5 +1,5 @@ // RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:cs /arg:csharp /arg:1 "%s" >> "%t" +// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:cs "%s" -- csharp 1 >> "%t" // RUN: %diff "%s.expect" "%t" method Main(args: int) { diff --git a/Test/comp/CompileWithArgumentsFail2.dfy b/Test/comp/CompileWithArgumentsFail2.dfy index 01d962dc207..dd085140b98 100644 --- a/Test/comp/CompileWithArgumentsFail2.dfy +++ b/Test/comp/CompileWithArgumentsFail2.dfy @@ -1,5 +1,5 @@ // RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:cs /arg:csharp /arg:1 "%s" >> "%t" +// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:cs "%s" -- csharp 1 >> "%t" // RUN: %diff "%s.expect" "%t" method Main(args: array, dummy: int) { diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index b13683ac820..501ea871bc5 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -324,9 +324,11 @@ Usage: Dafny [ option ... ] [ filename ... ] /Main: 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'. - /arg: (repeated) - When running the dafny program through /compile:3 or /compile:4, each individual - becomes an element of the array provided to the main function + A Main method can have at most one (non-ghost) argument of type `seq` + -- ... + When running a Dafny file through /compile:3 or /compile:4, '--' 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 From b1364a17b331d40c91a9edb22fc0f96c11219daa Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 26 Aug 2022 13:44:21 -0500 Subject: [PATCH 18/22] Use of "--args" instead of "--" --- Source/Dafny/DafnyOptions.cs | 6 +++--- Test/comp/CompileWithArguments.dfy | 12 ++++++------ Test/comp/CompileWithArgumentsFail.dfy | 2 +- Test/comp/CompileWithArgumentsFail2.dfy | 2 +- docs/DafnyRef/Options.txt | 4 ++-- 5 files changed, 13 insertions(+), 13 deletions(-) diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index bccd5e59198..da1f16c8153 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -27,7 +27,7 @@ public static DafnyOptions Create(params string[] arguments) { public override bool Parse(string[] arguments) { int i; for (i = 0; i < arguments.Length; i++) { - if (arguments[i] == "--") { + if (arguments[i] == "--args") { break; } } @@ -1282,8 +1282,8 @@ verification outcome 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` --- ... - When running a Dafny file through /compile:3 or /compile:4, '--' provides +--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) diff --git a/Test/comp/CompileWithArguments.dfy b/Test/comp/CompileWithArguments.dfy index a885e939a51..f79568b93d3 100644 --- a/Test/comp/CompileWithArguments.dfy +++ b/Test/comp/CompileWithArguments.dfy @@ -1,10 +1,10 @@ // RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" -- csharp 1 >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:cpp "%s" -- cpp Yipee >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" -- java heya >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" -- javascript 2 >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" -- python 1 >> "%t" -// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" -- "go go" 1 >> "%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" diff --git a/Test/comp/CompileWithArgumentsFail.dfy b/Test/comp/CompileWithArgumentsFail.dfy index 3d932398d4b..085bf5b0340 100644 --- a/Test/comp/CompileWithArgumentsFail.dfy +++ b/Test/comp/CompileWithArgumentsFail.dfy @@ -1,5 +1,5 @@ // RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:cs "%s" -- csharp 1 >> "%t" +// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:cs "%s" --args csharp 1 >> "%t" // RUN: %diff "%s.expect" "%t" method Main(args: int) { diff --git a/Test/comp/CompileWithArgumentsFail2.dfy b/Test/comp/CompileWithArgumentsFail2.dfy index dd085140b98..ffb97591df8 100644 --- a/Test/comp/CompileWithArgumentsFail2.dfy +++ b/Test/comp/CompileWithArgumentsFail2.dfy @@ -1,5 +1,5 @@ // RUN: %dafny /compile:0 "%s" > "%t" -// RUN: %dafny_0 /noVerify /compile:4 /compileTarget:cs "%s" -- csharp 1 >> "%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) { diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index 501ea871bc5..da4adc55400 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -325,8 +325,8 @@ Usage: Dafny [ option ... ] [ filename ... ] 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` - -- ... - When running a Dafny file through /compile:3 or /compile:4, '--' provides + --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) From ebf8dcb4974ebdd98e9c2e38e042f923fe66092a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Fri, 26 Aug 2022 15:22:50 -0500 Subject: [PATCH 19/22] Update RELEASE_NOTES.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Clément Pit-Claudel --- RELEASE_NOTES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index a3905f89367..a9119021b81 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -1,6 +1,6 @@ # Upcoming -- feat: Command-line arguments available from Main() in Dafny programs (https://github.com/dafny-lang/dafny/pull/2594) +- feat: Command-line arguments are now available from `Main` in Dafny programs, using `Main(args: seq)` (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) From 0ca5a2f7b4f0d57ab5424db2a988189c0ecec1a3 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Mon, 29 Aug 2022 11:21:13 -0500 Subject: [PATCH 20/22] Moved the code to transform arguments into the DafnyRuntime. --- Source/Dafny/Compilers/Compiler-Csharp.cs | 7 ++----- Source/Dafny/Compilers/Compiler-cpp.cs | 9 ++------- Source/Dafny/Compilers/Compiler-go.cs | 11 +++-------- Source/Dafny/Compilers/Compiler-java.cs | 10 ++-------- Source/Dafny/Compilers/Compiler-js.cs | 2 +- Source/Dafny/Compilers/Compiler-python.cs | 2 +- Source/Dafny/Compilers/SinglePassCompiler.cs | 7 +++---- Source/DafnyRuntime/DafnyRuntime.cs | 11 +++++++++++ Source/DafnyRuntime/DafnyRuntime.go | 9 +++++++++ Source/DafnyRuntime/DafnyRuntime.h | 9 +++++++++ .../DafnyRuntimeJava/src/main/java/dafny/Helpers.java | 9 +++++++++ 11 files changed, 52 insertions(+), 34 deletions(-) diff --git a/Source/Dafny/Compilers/Compiler-Csharp.cs b/Source/Dafny/Compilers/Compiler-Csharp.cs index 0e70bae63f5..436f98e1c52 100644 --- a/Source/Dafny/Compilers/Compiler-Csharp.cs +++ b/Source/Dafny/Compilers/Compiler-Csharp.cs @@ -222,7 +222,7 @@ private void EmitInitNewArrays(BuiltIns builtIns, ConcreteSyntaxTree dafnyNamesp } } - protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, ref string argsParameterName) { + 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 @@ -3325,10 +3325,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete var idName = IssueCreateStaticMain(mainMethod) ? "_StaticMain" : IdName(mainMethod); Coverage.EmitSetup(wBody); - wBody.WriteLine($"Dafny.ISequence[] dafnyArgs = new Dafny.ISequence[args.Length + 1];"); - wBody.WriteLine($"dafnyArgs[0] = Dafny.Sequence.FromString(\"dotnet\");"); - wBody.WriteLine($"for(var i = 0; i < args.Length; i++) dafnyArgs[i+1] = Dafny.Sequence.FromString(args[i]);"); - wBody.WriteLine($"{GetHelperModuleName()}.WithHaltHandling(() => {companion}.{idName}(Dafny.Sequence>.FromArray(dafnyArgs)));"); + 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 89fc12fa20c..11dbcdc0605 100644 --- a/Source/Dafny/Compilers/Compiler-cpp.cs +++ b/Source/Dafny/Compilers/Compiler-cpp.cs @@ -144,17 +144,12 @@ protected override void EmitFooter(Program program, ConcreteSyntaxTree wr) { public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) { var w = wr.NewBlock("int main(int argc, char *argv[])"); var tryWr = w.NewBlock("try"); - tryWr.WriteLine("DafnySequence> 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)); + 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, ref string argsParameterName) { + protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) { var wr = (cw as CppCompiler.ClassWriter).MethodWriter; return wr.NewBlock($"int main(DafnySequence> {argsParameterName})"); } diff --git a/Source/Dafny/Compilers/Compiler-go.cs b/Source/Dafny/Compilers/Compiler-go.cs index 5ea07a91aa3..39c701e8c81 100644 --- a/Source/Dafny/Compilers/Compiler-go.cs +++ b/Source/Dafny/Compilers/Compiler-go.cs @@ -119,11 +119,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete var idName = IssueCreateStaticMain(mainMethod) ? "Main" : IdName(mainMethod); Coverage.EmitSetup(wBody); - 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); + wBody.WriteLine("{0}.{1}({2}.FromMainArguments(os.Args))", companion, idName, GetHelperModuleName()); Coverage.EmitTearDown(wBody); } @@ -135,10 +131,9 @@ ConcreteSyntaxTree CreateDescribedSection(string desc, ConcreteSyntaxTree wr, pa return body; } - protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, ref string argsParameterName) { + protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) { var wr = ((GoCompiler.ClassWriter)cw).ConcreteMethodWriter; - argsParameterName = "args"; - return wr.NewNamedBlock("func (_this * {0}) Main(args _dafny.Seq)", 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) { diff --git a/Source/Dafny/Compilers/Compiler-java.cs b/Source/Dafny/Compilers/Compiler-java.cs index 2b9363ae056..2f588cd03fd 100644 --- a/Source/Dafny/Compilers/Compiler-java.cs +++ b/Source/Dafny/Compilers/Compiler-java.cs @@ -342,13 +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(@"@SuppressWarnings(""unchecked"")"); - wBody.WriteLine($"dafny.TypeDescriptor> type = dafny.DafnySequence._typeDescriptor(dafny.TypeDescriptor.CHAR);"); - wBody.WriteLine($"dafny.Array> 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> result = dafny.DafnySequence.fromArray(type, dafnyArgs);"); - wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling(() -> {{ {companion}.__Main(result); }} );"); + wBody.WriteLine($"{DafnyHelpersClass}.withHaltHandling(() -> {{ {companion}.__Main({DafnyHelpersClass}.FromMainArguments(args)); }} );"); Coverage.EmitTearDown(wBody); } @@ -4001,7 +3995,7 @@ protected override void EmitTypeTest(string localName, Type fromType, Type toTyp protected override bool IssueCreateStaticMain(Method m) { return true; } - protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, ref string argsParameterName) { + protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) { var wr = ((ClassWriter)cw).StaticMemberWriter; return wr.NewBlock($"public static void __Main(dafny.DafnySequence> {argsParameterName})"); } diff --git a/Source/Dafny/Compilers/Compiler-js.cs b/Source/Dafny/Compilers/Compiler-js.cs index 8162323ce7a..0e46b2bdc9f 100644 --- a/Source/Dafny/Compilers/Compiler-js.cs +++ b/Source/Dafny/Compilers/Compiler-js.cs @@ -56,7 +56,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete Coverage.EmitTearDown(wr); } - protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, ref string argsParameterName) { + protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) { var wr = (cw as JavaScriptCompiler.ClassWriter).MethodWriter; return wr.NewBlock($"static Main({argsParameterName})"); } diff --git a/Source/Dafny/Compilers/Compiler-python.cs b/Source/Dafny/Compilers/Compiler-python.cs index 0c9dde83edf..382982bfd06 100644 --- a/Source/Dafny/Compilers/Compiler-python.cs +++ b/Source/Dafny/Compilers/Compiler-python.cs @@ -90,7 +90,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete .WriteLine($"{DafnyRuntimeModule}.print(\"[Program halted] \" + str(e) + \"\\n\")"); } - protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, ref string argsParameterName) { + protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string argsParameterName) { return ((ClassWriter)cw).MethodWriter.NewBlockPy($"def Main({argsParameterName}):"); } diff --git a/Source/Dafny/Compilers/SinglePassCompiler.cs b/Source/Dafny/Compilers/SinglePassCompiler.cs index cfdf80a6d18..51d6de2dbe3 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, ref string argsParameterName); + 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 { @@ -2412,8 +2412,7 @@ private void CompileMethod(Program program, Method m, IClassWriter cw, bool look } if (m == program.MainMethod && IssueCreateStaticMain(m)) { - var args_name = STATIC_ARGS_NAME; - w = CreateStaticMain(cw, ref args_name); + w = CreateStaticMain(cw, STATIC_ARGS_NAME); var ty = UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(m.EnclosingClass); LocalVariable receiver = null; if (!m.IsStatic) { @@ -2445,7 +2444,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 + args_name); + w.Write(sep + STATIC_ARGS_NAME); w.Write(")"); EndStmt(w); } 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) { From fbfc0caefb5c9cb2a54ef41ac42f1d58cafd25f3 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Wed, 31 Aug 2022 13:50:18 -0500 Subject: [PATCH 21/22] Arguments fixed --- Source/Dafny/Compilers/Compiler-cpp.cs | 8 ++++++-- Source/Dafny/Compilers/Compiler-go.cs | 8 ++++++-- Source/Dafny/Compilers/Compiler-java.cs | 6 +++++- Source/Dafny/Compilers/Compiler-js.cs | 2 +- Source/Dafny/Compilers/Compiler-python.cs | 6 +++++- Source/Dafny/DafnyOptions.cs | 5 ----- Test/comp/CompileWithArguments.dfy.expect | 2 +- 7 files changed, 24 insertions(+), 13 deletions(-) diff --git a/Source/Dafny/Compilers/Compiler-cpp.cs b/Source/Dafny/Compilers/Compiler-cpp.cs index 11dbcdc0605..912993bd52d 100644 --- a/Source/Dafny/Compilers/Compiler-cpp.cs +++ b/Source/Dafny/Compilers/Compiler-cpp.cs @@ -2501,12 +2501,16 @@ 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(ComputeExeName(targetFilename), DafnyOptions.O.ArgsStringExtra) { + var psi = new ProcessStartInfo(ComputeExeName(targetFilename)) { 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 39c701e8c81..17ae4bddf83 100644 --- a/Source/Dafny/Compilers/Compiler-go.cs +++ b/Source/Dafny/Compilers/Compiler-go.cs @@ -3608,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) + DafnyOptions.O.ArgsStringExtra; - 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. diff --git a/Source/Dafny/Compilers/Compiler-java.cs b/Source/Dafny/Compilers/Compiler-java.cs index 2f588cd03fd..00ed6f21b8b 100644 --- a/Source/Dafny/Compilers/Compiler-java.cs +++ b/Source/Dafny/Compilers/Compiler-java.cs @@ -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) + DafnyOptions.O.ArgsStringExtra) { + 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) { diff --git a/Source/Dafny/Compilers/Compiler-js.cs b/Source/Dafny/Compilers/Compiler-js.cs index 0e46b2bdc9f..2f4e34f0086 100644 --- a/Source/Dafny/Compilers/Compiler-js.cs +++ b/Source/Dafny/Compilers/Compiler-js.cs @@ -2467,7 +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.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 382982bfd06..f806f688deb 100644 --- a/Source/Dafny/Compilers/Compiler-python.cs +++ b/Source/Dafny/Compilers/Compiler-python.cs @@ -1591,13 +1591,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 + DafnyOptions.O.ArgsStringExtra) { + 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/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index da1f16c8153..07ac6c1f55e 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -198,11 +198,6 @@ public void CopyTo(DafnyOptions dst) { public virtual TestGenerationOptions TestGenOptions => testGenOptions ??= new TestGenerationOptions(); - public string ArgsStringExtra => - string.Join("", MainArgs.Select(x => " " + - (!x.Contains(" ") ? x : - "\"" + x.Replace(@"\", @"\\").Replace(@"""", @"\\""") + "\""))); - protected override bool ParseOption(string name, Bpl.CommandLineParseState ps) { var args = ps.args; // convenient synonym switch (name) { diff --git a/Test/comp/CompileWithArguments.dfy.expect b/Test/comp/CompileWithArguments.dfy.expect index 75f8877dc54..885f26f2b66 100644 --- a/Test/comp/CompileWithArguments.dfy.expect +++ b/Test/comp/CompileWithArguments.dfy.expect @@ -11,7 +11,7 @@ Dafny program verifier did not attempt verification java says heya java Dafny program verifier did not attempt verification - says Howdy javascript +node says Howdy javascript Dafny program verifier did not attempt verification Someone says Hello python From c0cfb9e15d3ca46d640e1b834d0066717424eb2f Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 2 Sep 2022 16:40:32 -0500 Subject: [PATCH 22/22] Fixed verb handling in Go --- Source/Dafny/Compilers/Compiler-go.cs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Source/Dafny/Compilers/Compiler-go.cs b/Source/Dafny/Compilers/Compiler-go.cs index 17ae4bddf83..2fb99eb23dc 100644 --- a/Source/Dafny/Compilers/Compiler-go.cs +++ b/Source/Dafny/Compilers/Compiler-go.cs @@ -3568,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; @@ -3605,7 +3605,9 @@ private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, } } - verb = string.Format("build -o \"{0}\"", output); + verb.Add("build"); + verb.Add("-o"); + verb.Add(output); } var psi = new ProcessStartInfo("go") { @@ -3615,7 +3617,9 @@ private bool SendToNewGoProcess(string dafnyProgramName, string targetFilename, RedirectStandardOutput = false, RedirectStandardError = false, }; - psi.ArgumentList.Add(verb); + foreach (var verbArg in verb) { + psi.ArgumentList.Add(verbArg); + } psi.ArgumentList.Add(targetFilename); foreach (var arg in DafnyOptions.O.MainArgs) { psi.ArgumentList.Add(arg);