From 25321785b6f4e3c5f9b0d39f990b7ac58afde77e Mon Sep 17 00:00:00 2001 From: Tyler Dean Date: Wed, 26 Jan 2022 18:39:27 -0700 Subject: [PATCH 1/2] appends glue to concrete syntax tree --- Source/Dafny/Compilers/Compiler-Csharp.cs | 77 +++++++++++++++++++++- Source/Dafny/ConcreteSyntax/LineSegment.cs | 2 + 2 files changed, 78 insertions(+), 1 deletion(-) diff --git a/Source/Dafny/Compilers/Compiler-Csharp.cs b/Source/Dafny/Compilers/Compiler-Csharp.cs index 4457f3d66ad..135d157e9f1 100644 --- a/Source/Dafny/Compilers/Compiler-Csharp.cs +++ b/Source/Dafny/Compilers/Compiler-Csharp.cs @@ -2871,6 +2871,70 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg return false; } + private string GetClassNameFromWr(ConcreteSyntaxTree wr) { + foreach (var node in wr.Nodes) { + if (node is Microsoft.Dafny.LineSegment) { + Microsoft.Dafny.LineSegment lsNode = (Microsoft.Dafny.LineSegment) node; + string pattern = @"(?<=public )[^_]+(?=\()"; + System.Text.RegularExpressions.Match m = System.Text.RegularExpressions.Regex.Match(lsNode.Value, pattern); + if (m.Success) + return m.Value; + } + } + + return ""; + } + + private int GetTupleLength(string input) { + string pattern = @"(?<=Tuple)[0-9]*"; + System.Text.RegularExpressions.Match m = System.Text.RegularExpressions.Regex.Match(input, pattern); + if (m.Success) + return Int32.Parse(m.Value); + else + throw new Exception("Your dafny structure must be a sequence of tuples"); + } + + private (string, int) GetDafnyStructureFromWr(ConcreteSyntaxTree wr, string MethodName) { + foreach (var node in wr.Nodes) { + if (node is Microsoft.Dafny.LineSegment) { + Microsoft.Dafny.LineSegment lsNode = (Microsoft.Dafny.LineSegment) node; + string pattern = @"(?<=public static ).*(?= " + MethodName + ")"; + System.Text.RegularExpressions.Match m = System.Text.RegularExpressions.Regex.Match(lsNode.Value, pattern); + if (m.Success) { + int tupleLength = GetTupleLength(lsNode.Value); + return (m.Value, tupleLength); + } + } + } + throw new Exception("Method source must be a public static method"); + } + + private void WriteGlueCode(ConcreteSyntaxTree wr, string className, string methodName, string dafnyStructure, int tupleLength) { + wr.WriteLine("public static System.Collections.Generic.IEnumerable DafnyTupleToObjArray(" + dafnyStructure + " dafnyStructure) {"); + wr.WriteLine("System.Collections.Generic.List newList = new ();"); + wr.WriteLine("foreach (var tuple in dafnyStructure.UniqueElements) {"); + wr.Write("newList.Add(new object[] {"); + for (int i = 0; i < tupleLength; i++) { + string tupleValue = "tuple._" + i.ToString(); + wr.Write(tupleValue); + if (i < tupleLength - 1) + wr.Write(", "); + } + wr.WriteLine("});"); + wr.WriteLine("}"); + wr.WriteLine("return newList;"); + wr.WriteLine("}"); + + wr.WriteLine("public static System.Collections.Generic.IEnumerable _" + methodName + "(string methodName) {"); + wr.WriteLine("System.Reflection.MethodInfo m = typeof(" + className + ").GetMethod(methodName);"); + wr.WriteLine(dafnyStructure + " retValue = (" + dafnyStructure + ") m.Invoke(null, null);"); + wr.WriteLine("return DafnyTupleToObjArray(retValue);"); + wr.WriteLine("}"); + + wr.WriteLine("[Xunit.Theory]"); + wr.WriteLine("[Xunit.MemberData(nameof(_" + methodName + "), \"" + methodName + "\")]"); + } + private void AddTestCheckerIfNeeded(string name, Declaration decl, ConcreteSyntaxTree wr) { if (Attributes.Contains(decl.Attributes, "test")) { // TODO: The resolver needs to check the assumptions about the declaration @@ -2881,9 +2945,20 @@ private void AddTestCheckerIfNeeded(string name, Declaration decl, ConcreteSynta } else if (decl is Method) { var method = (Method)decl; hasReturnValue = method.Outs.Count > 1; + var ins = method.Ins.Count; } - wr.WriteLine("[Xunit.Fact]"); + var args = Attributes.FindExpressions(decl.Attributes, "test"); + + if (args.Count == 2 && args[0] is LiteralExpr && args[1] is LiteralExpr) { + string className = GetClassNameFromWr(wr); + LiteralExpr methodNameExpr = (LiteralExpr) args[1]; + (string dafnyStructure, int tupleLength) = GetDafnyStructureFromWr(wr, methodNameExpr.Value.ToString()); + WriteGlueCode(wr, className, methodNameExpr.Value.ToString(), dafnyStructure, tupleLength); + } + else { + wr.WriteLine("[Xunit.Fact]"); + } if (hasReturnValue) { wr = wr.NewNamedBlock("public static void {0}_CheckForFailureForXunit()", name); wr.WriteLine("var result = {0}();", name); diff --git a/Source/Dafny/ConcreteSyntax/LineSegment.cs b/Source/Dafny/ConcreteSyntax/LineSegment.cs index 7df93f4365d..e0e03024d96 100644 --- a/Source/Dafny/ConcreteSyntax/LineSegment.cs +++ b/Source/Dafny/ConcreteSyntax/LineSegment.cs @@ -6,6 +6,8 @@ namespace Microsoft.Dafny { class LineSegment : ICanRender { private readonly string _value; + public string Value => _value; + public LineSegment(string value) { this._value = value; } From d2d7514aa9ee1d8dd27c95099f5c1cb5f51b22f7 Mon Sep 17 00:00:00 2001 From: Tyler Dean Date: Wed, 26 Jan 2022 18:42:29 -0700 Subject: [PATCH 2/2] custom exception messages --- Source/Dafny/Compilers/Compiler-Csharp.cs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Source/Dafny/Compilers/Compiler-Csharp.cs b/Source/Dafny/Compilers/Compiler-Csharp.cs index 135d157e9f1..4507a0791e1 100644 --- a/Source/Dafny/Compilers/Compiler-Csharp.cs +++ b/Source/Dafny/Compilers/Compiler-Csharp.cs @@ -2882,7 +2882,7 @@ private string GetClassNameFromWr(ConcreteSyntaxTree wr) { } } - return ""; + throw new Exception("ParameterizedTests: tests must be in public class"); } private int GetTupleLength(string input) { @@ -2891,7 +2891,7 @@ private int GetTupleLength(string input) { if (m.Success) return Int32.Parse(m.Value); else - throw new Exception("Your dafny structure must be a sequence of tuples"); + throw new Exception("ParameterizedTests: Your dafny structure must be a sequence of tuples"); } private (string, int) GetDafnyStructureFromWr(ConcreteSyntaxTree wr, string MethodName) { @@ -2906,7 +2906,7 @@ private int GetTupleLength(string input) { } } } - throw new Exception("Method source must be a public static method"); + throw new Exception("ParameterizedTests: Method source must be a public static method"); } private void WriteGlueCode(ConcreteSyntaxTree wr, string className, string methodName, string dafnyStructure, int tupleLength) {