Type Parameters in Automatically Generated Tests

RELEASE_NOTES.md

@@ -7,6 +7,7 @@
 - feat: Live verification diagnostics for the language server (https://github.com/dafny-lang/dafny/pull/1942)
 - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080)
 - fix: Correctly specify the type of the receiver parameter when translating tail-recursive member functions to C# (https://github.com/dafny-lang/dafny/pull/2205)
+- fix: Added support for type parameters in automatically generated tests (https://github.com/dafny-lang/dafny/pull/2227)
 
 # 3.6.0
 

Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs

@@ -3,7 +3,6 @@
 
 using System;
 using System.Collections.Generic;
-using System.Collections.Specialized;
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
@@ -29,7 +28,7 @@ public class DafnyModel {
  fChar, fNull, fSetUnion, fSetIntersection, fSetDifference, fSetUnionOne,
  fSetEmpty, fSeqEmpty, fSeqBuild, fSeqAppend, fSeqDrop, fSeqTake,
  fSeqUpdate, fSeqCreate, fReal, fU2Real, fBool, fU2Bool, fInt, fU2Int,
- fMapDomain, fMapElements, fMapBuild;
+ fMapDomain, fMapElements, fMapBuild, fIs, fIsBox;
  private readonly Dictionary<Model.Element, Model.Element[]> arrayLengths = new();
  private readonly Dictionary<Model.Element, Model.FuncTuple> datatypeValues = new();
  private readonly Dictionary<Model.Element, string> localValue = new();
@@ -70,6 +69,8 @@ public DafnyModel(Model model) {
  fMapDomain = model.MkFunc("Map#Domain", 1);
  fMapElements = model.MkFunc("Map#Elements", 1);
  fMapBuild = model.MkFunc("Map#Build", 3);
+ fIs = model.MkFunc("$Is", 2);
+ fIsBox = model.MkFunc("$IsBox", 2);
  fBox = model.MkFunc("$Box", 1);
  fDim = model.MkFunc("FDim", 1);
  fIndexField = model.MkFunc("IndexField", 1);
@@ -292,7 +293,7 @@ private static string GetTrueName(Model.Element element) {
  /// with the element
  /// </summary>
  private string GetBoogieType(Model.Element element) {
- var typeElement = Model.GetFunc("type").OptEval(element);
+ var typeElement = fType.OptEval(element);
  if (typeElement == null) {
  return null;
  }
@@ -338,7 +339,7 @@ internal DafnyModelType GetDafnyType(Model.Element element) {
  /// </summary>
  private List<Model.Element> GetIsResults(Model.Element element) {
  List<Model.Element> result = new();
- foreach (var tuple in Model.GetFunc("$Is").AppsWithArg(0, element)) {
+ foreach (var tuple in fIs.AppsWithArg(0, element)) {
  if (((Model.Boolean)tuple.Result).Value) {
  result.Add(tuple.Args[1]);
  }
@@ -443,6 +444,14 @@ private DafnyModelType GetDafnyType(Model.Uninterpreted element) {
  return new DafnyModelType("?");
  case var bv when bvTypeRegex.IsMatch(bv):
  return new DafnyModelType(bv.Substring(0, bv.Length - 4));
+ case "BoxType":
+ var unboxedTypes = fIsBox.AppsWithArg(0, element)
+ .Where(tuple => ((Model.Boolean)tuple.Result).Value)
+ .Select(tuple => tuple.Args[1]).ToList();
+ if (unboxedTypes.Count == 1) {
+ return ReconstructType(unboxedTypes[0]);
+ }
+ return new DafnyModelType("?");
  default:
  return new DafnyModelType("?");
  }
@@ -456,7 +465,7 @@ private DafnyModelType ReconstructType(Model.Element typeElement) {
  return new DafnyModelType("?");
  }
  var fullName = GetTrueName(typeElement);
- if (fullName != null && fullName.Length > 7) {
+ if (fullName != null && fullName.Length > 7 && fullName.Substring(0, 7).Equals("Tclass.")) {
  return new DafnyModelType(fullName.Substring(7));
  }
  if (fullName is "TInt" or "TReal" or "TChar" or "TBool") {
@@ -465,6 +474,9 @@ private DafnyModelType ReconstructType(Model.Element typeElement) {
  if (fBv.AppWithResult(typeElement) != null) {
  return new DafnyModelType("bv" + ((Model.Integer)fBv.AppWithResult(typeElement).Args[0]).AsInt());
  }
+ if (fullName != null) { // this means this is a type variable
+ return new DafnyModelType(fullName);
+ }
  var tagElement = fTag.OptEval(typeElement);
  if (tagElement == null) {
  return new DafnyModelType("?");
@@ -606,7 +618,7 @@ private string GetUnreservedBoolValue(Model.Element element) {
  /// any other value of that type in the entire model.
  /// Reserve that value for given element
  /// </summary>
- private string GetUnreservedNumericValue(Model.Element element, Type numericType) {
+ public string GetUnreservedNumericValue(Model.Element element, Type numericType) {
  if (reservedValuesMap.TryGetValue(element, out var reservedValue)) {
  return reservedValue;
  }

Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs

@@ -11,7 +11,8 @@ public class DafnyModelType {
  public readonly string Name;
  public readonly List<DafnyModelType> TypeArgs;
 
- private static readonly Regex boogieToDafnyTypeRegex = new("(?<=[^_](__)*)_m");
+ private static readonly Regex ModuleSeparatorRegex = new("(?<=[^_](__)*)_m");
+ private static readonly Regex UnderscoreRemovalRegex = new("__");
 
  public DafnyModelType(string name, IEnumerable<DafnyModelType> typeArgs) {
  Name = name;
@@ -37,20 +38,11 @@ public override string ToString() {
  /// </summary>
  public DafnyModelType InDafnyFormat() {
  // The line below converts "_m" used in boogie to separate modules to ".":
- var tmp = boogieToDafnyTypeRegex.Replace(Name, ".");
+ var newName = ModuleSeparatorRegex.Replace(Name, ".");
+ // strip everything after @, this is done for type variables:
+ newName = newName.Split("@")[0];
  // The code below converts every "__" to "_":
- bool removeNextUnderscore = false;
- var newName = "";
- foreach (char c in tmp) {
- if (c == '_') {
- if (!removeNextUnderscore) {
- newName += c;
- }
- removeNextUnderscore = !removeNextUnderscore;
- } else {
- newName += c;
- }
- }
+ newName = UnderscoreRemovalRegex.Replace(newName, "_");
  return new(newName, TypeArgs.ConvertAll(type => type.InDafnyFormat()));
  }
 
@@ -59,6 +51,30 @@ public DafnyModelType GetNonNullable() {
  return new DafnyModelType(newName, TypeArgs);
  }
 
+ public DafnyModelType ReplaceTypeVariables(DafnyModelType with) {
+ // Assigns the given value to all type variables
+ if (Name.Contains("$")) {
+ return with;
+ }
+ return new(Name, TypeArgs.ConvertAll(type =>
+ type.ReplaceTypeVariables(with)));
+ }
+
+ public override int GetHashCode() {
+ int hash = Name.GetHashCode();
+ foreach (var typ in TypeArgs) {
+ hash = 31 * typ.GetHashCode();
+ }
+ return hash;
+ }
+
+ public override bool Equals(object other) {
+ if (other is not DafnyModelType typ) {
+ return false;
+ }
+ return typ.ToString() == ToString();
+ }
+
  /// <summary>
  /// Parse a string into a type.
  /// </summary>

Source/DafnyTestGeneration.Test/Various.cs

@@ -248,7 +248,7 @@ method ignoreNonNullableObject(v:Value<char>, b:bool) {
  Assert.IsTrue(m.DafnyInfo.IsStatic("Module.ignoreNonNullableObject"));
  Assert.AreEqual(2, m.ArgValues.Count);
  Assert.AreEqual(1, m.ObjectsToMock.Count);
- Assert.AreEqual("Module.Value<char>", m.ObjectsToMock[0].type.Name);
+ Assert.AreEqual("Module.Value<char>", m.ObjectsToMock[0].type.ToString());
  }
 
  [TestMethod]
@@ -287,6 +287,35 @@ method m(a:int) returns (b:int)
  Assert.AreEqual(1, stats.Count); // the only line with stats
  }
 
+ [TestMethod]
+ public async Task TypePolymorphism() {
+ var source = @"
+module Test {
+ method IsEvenLength<K>(s: seq<K>) returns (isEven: bool)
+ {
+ if (|s| % 2 == 0) {
+ return true;
+ } else {
+ return false;
+ }
+ }
+}
+".TrimStart();
+ var program = Utils.Parse(source);
+ DafnyOptions.O.TestGenOptions.TargetMethod = "Test.IsEvenLength";
+ DafnyOptions.O.TestGenOptions.SeqLengthLimit = 1;
+ var methods = await Main.GetTestMethodsForProgram(program).ToListAsync();
+ Assert.AreEqual(2, methods.Count);
+ Assert.IsTrue(methods.All(m => m.MethodName == "Test.IsEvenLength"));
+ Assert.IsTrue(methods.All(m => m.DafnyInfo.IsStatic("Test.IsEvenLength")));
+ Assert.IsTrue(methods.All(m => m.ArgValues.Count == 1));
+ Assert.IsTrue(methods.All(m => m.ObjectsToMock.Count == 0));
+ Assert.IsTrue(methods.All(m => m.NOfTypeParams == 1));
+ Assert.IsTrue(methods.Exists(m => m.ArgValues[0] == "[]"));
+ Assert.IsTrue(methods.Exists(m =>
+ Regex.IsMatch(m.ArgValues[0], "\\[[0-9]+\\]")));
+ }
+
  /// <summary>
  /// If this fails, consider amending ProgramModifier.MergeBoogiePrograms
  /// </summary>

Source/DafnyTestGeneration/DafnyInfo.cs

@@ -55,6 +55,8 @@ private void Visit(TopLevelDecl d) {
  Visit(moduleDecl);
  } else if (d is ClassDecl classDecl) {
  Visit(classDecl);
+ } else if (d is IndDatatypeDecl datatypeDecl) {
+ Visit(datatypeDecl);
  }
  }
 
@@ -69,6 +71,12 @@ private void Visit(LiteralModuleDecl d) {
  path.RemoveAt(path.Count - 1);
  }
 
+ private void Visit(IndDatatypeDecl d) {
+ path.Add(d.Name);
+ d.Members.ForEach(Visit);
+ path.RemoveAt(path.Count - 1);
+ }
+
  private void Visit(ClassDecl d) {
  if (d.Name == "_default") {
  insideAClass = false; // methods in _default are considered static
@@ -85,6 +93,8 @@ private void Visit(ClassDecl d) {
  private void Visit(MemberDecl d) {
  if (d is Method method) {
  Visit(method);
+ } else if (d is Function function) {
+ Visit(function);
  }
  }
 
@@ -99,6 +109,18 @@ private void Visit(MemberDecl d) {
  var returnTypes = m.Outs.Select(arg => arg.Type.ToString()).ToList();
  info.returnTypes[methodName] = returnTypes;
  }
+
+ private new void Visit(Function f) {
+ var methodName = f.Name;
+ if (path.Count != 0) {
+ methodName = $"{string.Join(".", path)}.{methodName}";
+ }
+ if (f.HasStaticKeyword || !insideAClass) {
+ info.isStatic.Add(methodName);
+ }
+ var returnTypes = new List<string> { f.ResultType.ToString() };
+ info.returnTypes[methodName] = returnTypes;
+ }
  }
  }
 }

Source/DafnyTestGeneration/TestMethod.cs

@@ -1,10 +1,9 @@
-using System;
 using System.Collections.Generic;
-using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
 using DafnyServer.CounterexampleGeneration;
 using Microsoft.Boogie;
+using Type = Microsoft.Dafny.Type;
 
 namespace DafnyTestGeneration {
 
@@ -24,14 +23,21 @@ public class TestMethod {
  public readonly string MethodName;
  // values of the arguments to be passed to the method call
  public readonly List<string> ArgValues;
+ // number of type parameters for the method (all will be set to defaultType)
+ public readonly int NOfTypeParams = 0;
+ // default type to replace any type variable with
+ private readonly DafnyModelType defaultType = new("int");
+ // the DafnyModel that describes the inputs to this test method
+ private DafnyModel dafnyModel;
 
  public TestMethod(DafnyInfo dafnyInfo, string log) {
  DafnyInfo = dafnyInfo;
  var typeNames = ExtractPrintedInfo(log, "Types | ");
  var argumentNames = ExtractPrintedInfo(log, "Impl | ");
- var dafnyModel = DafnyModel.ExtractModel(log);
+ dafnyModel = DafnyModel.ExtractModel(log);
  MethodName = Utils.GetDafnyMethodName(argumentNames.First());
  argumentNames.RemoveAt(0);
+ NOfTypeParams = typeNames.Count(typeName => typeName == "Ty");
  ArgValues = ExtractInputs(dafnyModel.States.First(), argumentNames, typeNames);
  }
 
@@ -51,6 +57,9 @@ private List<string> ExtractInputs(DafnyModelState state, IReadOnlyList<string>
  var result = new List<string>();
  var vars = state.ExpandedVariableSet(null);
  for (var i = 0; i < printOutput.Count; i++) {
+ if (types[i] == "Ty") {
+ continue; // this means that this parameter is a type variable
+ }
  if (printOutput[i] == "") {
  result.Add(GetDefaultValue(DafnyModelType.FromString(types[i])));
  continue;
@@ -75,6 +84,11 @@ private List<string> ExtractInputs(DafnyModelState state, IReadOnlyList<string>
  return result;
  }
 
+ // Returns a new value of the defaultType type (set to int by default)
+ private string GetADefaultTypeValue(DafnyModelVariable variable) {
+ return dafnyModel.GetUnreservedNumericValue(variable.Element, Type.Int);
+ }
+
  /// <summary>
  /// Extract the value of a variable. This can have side-effects on
  /// assignments, reservedValues, reservedValuesMap, and objectsToMock.
@@ -89,7 +103,11 @@ private string ExtractVariable(DafnyModelVariable variable) {
  }
 
  List<string> elements = new();
- switch (variable.Type.Name) {
+ var variableType = variable.Type.ReplaceTypeVariables(defaultType);
+ if (variableType.Equals(defaultType) && !variableType.Equals(variable.Type)) {
+ return GetADefaultTypeValue(variable);
+ }
+ switch (variableType.Name) {
  case "?":
  return "null";
  case "char":
@@ -106,7 +124,7 @@ private string ExtractVariable(DafnyModelVariable variable) {
  for (var i = 0; i < seqVar.GetLength(); i++) {
  var element = seqVar[i];
  if (element == null) {
- elements.Add(GetDefaultValue(variable.Type.TypeArgs.First()));
+ elements.Add(GetDefaultValue(variableType.TypeArgs.First()));
  continue;
  }
  elements.Add(ExtractVariable(element));
@@ -129,10 +147,11 @@ private string ExtractVariable(DafnyModelVariable variable) {
  return $"map[{string.Join(", ", mappingStrings)}]";
  case var arrType when new Regex("^_System.array[0-9]*\\?$").IsMatch(arrType):
  break;
+ case var _ when (!variable.Value.StartsWith("(") && variable.Value != "null"):
+ return "DATATYPES_NOT_SUPPORTED";
  default:
  var varId = $"v{ObjectsToMock.Count}";
- var dafnyType =
- new DafnyModelType(variable.Type.GetNonNullable().InDafnyFormat().ToString());
+ var dafnyType = variableType.GetNonNullable().InDafnyFormat();
  ObjectsToMock.Add(new(varId, dafnyType));
  mockedVarId[variable] = varId;
  foreach (var filedName in variable.children.Keys) {
@@ -153,6 +172,7 @@ private string ExtractVariable(DafnyModelVariable variable) {
  /// an element (e.g. T@U!val!25).
  /// </summary>
  private string GetDefaultValue(DafnyModelType type) {
+ type = type.ReplaceTypeVariables(defaultType);
  var result = type.Name switch {
  "char" => "\'a\'",
  "bool" => "false",
@@ -229,14 +249,18 @@ private List<string> TestMethodLines() {
  }
 
  // the method call itself:
+ var typeArguments = "";
+ if (NOfTypeParams > 0) {
+ typeArguments = "<" + string.Join(",", Enumerable.Repeat(defaultType.ToString(), NOfTypeParams)) + ">";
+ }
  string methodCall;
  if (DafnyInfo.IsStatic(MethodName)) {
- methodCall = $"{MethodName}({string.Join(", ", ArgValues)});";
+ methodCall = $"{MethodName}{typeArguments}({string.Join(", ", ArgValues)});";
  } else {
  var receiver = ArgValues[0];
  ArgValues.RemoveAt(0);
  methodCall = $"{receiver}.{MethodName.Split(".").Last()}" +
- $"({string.Join(", ", ArgValues)});";
+ $"{typeArguments}({string.Join(", ", ArgValues)});";
  ArgValues.Insert(0, receiver);
  }