diff --git a/Source/DafnyCore/Compilers/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/Compiler-Csharp.cs index 0fde115edbf..8f2a3c738fa 100644 --- a/Source/DafnyCore/Compilers/Compiler-Csharp.cs +++ b/Source/DafnyCore/Compilers/Compiler-Csharp.cs @@ -1181,7 +1181,6 @@ public ConcreteSyntaxTree SynthesizeMethod(Method method, List typeArgs, List formals, Type resultType, IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) { return Compiler.CreateFunction(name, typeArgs, formals, resultType, tok, isStatic, createBody, member, Writer(isStatic, createBody, member), forBodyInheritance, lookasideBody); } diff --git a/Source/DafnyCore/Compilers/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Compiler-cpp.cs index 908627e58a0..91ad4fc1cf2 100644 --- a/Source/DafnyCore/Compilers/Compiler-cpp.cs +++ b/Source/DafnyCore/Compilers/Compiler-cpp.cs @@ -729,7 +729,7 @@ public ClassWriter(string className, CppCompiler compiler, ConcreteSyntaxTree me public ConcreteSyntaxTree SynthesizeMethod(Method m, List typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) { throw new UnsupportedFeatureException(m.tok, Feature.MethodSynthesis); } - + public ConcreteSyntaxTree/*?*/ CreateFunction(string name, List/*?*/ typeArgs, List formals, Type resultType, IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) { return Compiler.CreateFunction(member.EnclosingClass.CompileName, member.EnclosingClass.TypeArgs, name, typeArgs, formals, resultType, tok, isStatic, createBody, member, MethodDeclWriter, MethodWriter, lookasideBody); } diff --git a/Source/DafnyCore/Compilers/Compiler-go.cs b/Source/DafnyCore/Compilers/Compiler-go.cs index 6706950d35a..be9edde086e 100644 --- a/Source/DafnyCore/Compilers/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/Compiler-go.cs @@ -1045,7 +1045,6 @@ public ConcreteSyntaxTree FieldInitWriter(bool isStatic) { public ConcreteSyntaxTree SynthesizeMethod(Method m, List typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) { throw new UnsupportedFeatureException(m.tok, Feature.MethodSynthesis); } - public ConcreteSyntaxTree/*?*/ CreateFunction(string name, List typeArgs, List formals, Type resultType, IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) { return Compiler.CreateFunction(name, typeArgs, formals, resultType, tok, isStatic, createBody, member, ClassName, AbstractMethodWriter, ConcreteMethodWriter, forBodyInheritance, lookasideBody); } diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs index 9e9de5eec5c..0744cad2ca4 100644 --- a/Source/DafnyCore/Compilers/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Compiler-java.cs @@ -30,6 +30,9 @@ public override void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection "Java"; public override string TargetExtension => "java"; + + // True if the most recently visited AST has a method annotated with {:synthesize}: + protected bool Synthesize = false; public override string TargetBasename(string dafnyProgramName) => TransformToClassName(base.TargetBasename(dafnyProgramName)); public override string TargetBaseDir(string dafnyProgramName) => @@ -44,7 +47,6 @@ public string TransformToClassName(string baseName) => Feature.Iterators, Feature.SubsetTypeTests, Feature.TraitTypeParameters, - Feature.MethodSynthesis, Feature.TuplesWiderThan20 }; @@ -181,6 +183,22 @@ protected override void DeclareSpecificOutCollector(string collectorVarName, Con wr.Write($"{returnedTypes[0]} {collectorVarName} = "); } } + + /// + /// Return true if the AST contains a method annotated with an attribute + /// + private static bool ProgramHasMethodsWithAttr(Program p, String attr) { + foreach (var module in p.Modules()) { + foreach (ICallable callable in ModuleDefinition.AllCallables( + module.TopLevelDecls)) { + if ((callable is Method method) && + Attributes.Contains(method.Attributes, attr)) { + return true; + } + } + } + return false; + } protected override void EmitCastOutParameterSplits(string outCollector, List lhsNames, ConcreteSyntaxTree wr, List formalTypes, List lhsTypes, IToken tok) { var wOuts = new List(); @@ -321,6 +339,7 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { wr.WriteLine($"// Dafny program {program.Name} compiled into Java"); ModuleName = program.MainMethod != null ? "main" : Path.GetFileNameWithoutExtension(program.Name); wr.WriteLine(); + Synthesize = ProgramHasMethodsWithAttr(program, "synthesize"); // Keep the import writers so that we can import subsequent modules into the main one EmitImports(wr, out RootImportWriter); wr.WriteLine(); @@ -410,6 +429,7 @@ protected class ClassWriter : IClassWriter { public readonly ConcreteSyntaxTree InstanceMemberWriter; public readonly ConcreteSyntaxTree StaticMemberWriter; public readonly ConcreteSyntaxTree CtorBodyWriter; + private readonly JavaSynthesizer javaSynthesizer; public ClassWriter(JavaCompiler compiler, ConcreteSyntaxTree instanceMemberWriter, ConcreteSyntaxTree ctorBodyWriter, ConcreteSyntaxTree staticMemberWriter = null) { Contract.Requires(compiler != null); @@ -418,6 +438,7 @@ public ClassWriter(JavaCompiler compiler, ConcreteSyntaxTree instanceMemberWrite this.InstanceMemberWriter = instanceMemberWriter; this.CtorBodyWriter = ctorBodyWriter; this.StaticMemberWriter = staticMemberWriter ?? instanceMemberWriter; + this.javaSynthesizer = new JavaSynthesizer(Compiler, ErrorWriter()); } public ConcreteSyntaxTree Writer(bool isStatic, bool createBody, MemberDecl/*?*/ member) { @@ -433,8 +454,9 @@ public ConcreteSyntaxTree Writer(bool isStatic, bool createBody, MemberDecl/*?*/ return Compiler.CreateMethod(m, typeArgs, createBody, Writer(m.IsStatic, createBody, m), forBodyInheritance, lookasideBody); } - public ConcreteSyntaxTree SynthesizeMethod(Method m, List typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) { - throw new UnsupportedFeatureException(m.tok, Feature.MethodSynthesis); + public ConcreteSyntaxTree SynthesizeMethod(Method method, List typeArgs, bool createBody, bool forBodyInheritance, + bool lookasideBody) { + return javaSynthesizer.SynthesizeMethod(method, typeArgs, createBody, Writer(method.IsStatic, createBody, method), forBodyInheritance, lookasideBody); } public ConcreteSyntaxTree/*?*/ CreateFunction(string name, List typeArgs, List formals, Type resultType, IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) { @@ -500,6 +522,7 @@ protected override void DeclareLocalVar(string name, Type /*?*/ type, IToken /*? } return wGet; } + protected ConcreteSyntaxTree CreateMethod(Method m, List typeArgs, bool createBody, ConcreteSyntaxTree wr, bool forBodyInheritance, bool lookasideBody) { if (m.IsExtern(out _, out _) && (m.IsStatic || m is Constructor)) { // No need for an abstract version of a static method or a constructor @@ -521,7 +544,7 @@ protected ConcreteSyntaxTree CreateMethod(Method m, List typeArgs, bool lookasideBody, bool customReceiver, string returnType) { + var parameters = new ConcreteSyntaxTree(); + var sep = ""; + WriteRuntimeTypeDescriptorsFormals(ForTypeDescriptors(typeArgs, m, lookasideBody), parameters, ref sep, tp => $"{DafnyTypeDescriptor}<{tp.CompileName}> {FormatTypeDescriptorVariable(tp)}"); + if (customReceiver) { + var nt = m.EnclosingClass; + var receiverType = UserDefinedType.FromTopLevelDecl(m.tok, nt); + DeclareFormal(sep, "_this", receiverType, m.tok, true, parameters); + sep = ", "; + } + WriteFormals(sep, m.Ins, parameters); + if (returnType == "void") { + WriteFormals(parameters.Nodes.Any() ? ", " : "", m.Outs, parameters); + } + return parameters; + } + + internal string GetTargetReturnTypeReplacement(Method m, ConcreteSyntaxTree wr) { + string targetReturnTypeReplacement = null; + int nonGhostOuts = 0; + int nonGhostIndex = 0; + for (int i = 0; i < m.Outs.Count; i++) { + if (!m.Outs[i].IsGhost) { + nonGhostOuts += 1; + nonGhostIndex = i; + } + } + if (nonGhostOuts == 1) { + targetReturnTypeReplacement = TypeName(m.Outs[nonGhostIndex].Type, wr, m.Outs[nonGhostIndex].tok); + } else if (nonGhostOuts > 1) { + targetReturnTypeReplacement = DafnyTupleClass(nonGhostOuts); + } + + targetReturnTypeReplacement ??= "void"; + return targetReturnTypeReplacement; + } + protected override ConcreteSyntaxTree EmitMethodReturns(Method m, ConcreteSyntaxTree wr) { int nonGhostOuts = 0; foreach (var t in m.Outs) { @@ -613,7 +677,7 @@ private void EmitSuppression(ConcreteSyntaxTree wr) { wr.WriteLine("@SuppressWarnings({\"unchecked\", \"deprecation\"})"); } - string TypeParameters(List/*?*/ targs, string suffix = "") { + internal string TypeParameters(List/*?*/ targs, string suffix = "") { Contract.Requires(targs == null || cce.NonNullElements(targs)); Contract.Ensures(Contract.Result() != null); diff --git a/Source/DafnyCore/Compilers/Compiler-js.cs b/Source/DafnyCore/Compilers/Compiler-js.cs index c86428973a6..b45ce7d8965 100644 --- a/Source/DafnyCore/Compilers/Compiler-js.cs +++ b/Source/DafnyCore/Compilers/Compiler-js.cs @@ -618,7 +618,6 @@ public ClassWriter(JavaScriptCompiler compiler, ConcreteSyntaxTree methodWriter, public ConcreteSyntaxTree SynthesizeMethod(Method m, List typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) { throw new UnsupportedFeatureException(m.tok, Feature.MethodSynthesis); } - public ConcreteSyntaxTree/*?*/ CreateFunction(string name, List typeArgs, List formals, Type resultType, IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) { return Compiler.CreateFunction(name, typeArgs, formals, resultType, tok, isStatic, createBody, member, MethodWriter, forBodyInheritance, lookasideBody); } diff --git a/Source/DafnyCore/Compilers/Synthesizer-Csharp.cs b/Source/DafnyCore/Compilers/Synthesizer-Csharp.cs index 9249ea9ee09..00ccdce0bed 100644 --- a/Source/DafnyCore/Compilers/Synthesizer-Csharp.cs +++ b/Source/DafnyCore/Compilers/Synthesizer-Csharp.cs @@ -26,19 +26,11 @@ namespace Microsoft.Dafny.Compilers; /// | BOUNDVARS, BOUNDVARS /// /// -public class CsharpSynthesizer { - - private readonly CsharpCompiler compiler; - private readonly ConcreteSyntaxTree ErrorWriter; - // maps identifiers to the names of the corresponding mock: - private Dictionary objectToMockName = new(); - // associates a bound variable with the lambda passed to argument matcher - private Dictionary bounds = new(); - private Method lastSynthesizedMethod = null; +public class CsharpSynthesizer : Synthesizer { public CsharpSynthesizer(CsharpCompiler compiler, ConcreteSyntaxTree errorWriter) { this.compiler = compiler; - ErrorWriter = errorWriter; + this.errorWriter = errorWriter; } /// @@ -67,20 +59,24 @@ public CsharpSynthesizer(CsharpCompiler compiler, ConcreteSyntaxTree errorWriter /// e2Return = e2; /// } /// - public ConcreteSyntaxTree SynthesizeMethod(Method method, + public override ConcreteSyntaxTree SynthesizeMethod(Method method, List typeArgs, bool createBody, ConcreteSyntaxTree wr, bool forBodyInheritance, bool lookasideBody) { lastSynthesizedMethod = method; + if (compiler is not CsharpCompiler csharpCompiler) { + throw new Exception($"'{compiler}' is not of the type CsharpCompiler"); + } + // The following few lines are identical to those in Compiler.CreateMethod: var customReceiver = createBody && !forBodyInheritance && compiler.NeedsCustomReceiver(method); - var keywords = compiler.Keywords(true, true); - var returnType = compiler.GetTargetReturnTypeReplacement(method, wr); - var typeParameters = compiler.TypeParameters(SinglePassCompiler.TypeArgumentInstantiation. + var keywords = csharpCompiler.Keywords(true, true); + var returnType = csharpCompiler.GetTargetReturnTypeReplacement(method, wr); + var typeParameters = csharpCompiler.TypeParameters(SinglePassCompiler.TypeArgumentInstantiation. ToFormals(compiler.ForTypeParameters(typeArgs, method, lookasideBody))); - var parameters = compiler + var parameters = csharpCompiler .GetMethodParameters(method, typeArgs, lookasideBody, customReceiver, returnType); // Out parameters cannot be used inside lambda expressions in Csharp @@ -125,46 +121,8 @@ public ConcreteSyntaxTree SynthesizeMethod(Method method, wr.WriteLine("}"); return wr; } - - /// - /// If the expression is a bound variable identifier, return the - /// variable and the string representation of the bounding condition - /// - private Tuple GetBound(Expression exp) { - if (exp is not NameSegment) { - return null; - } - var variable = ((IdentifierExpr)exp.Resolved).Var; - if (!bounds.ContainsKey(variable)) { - return null; - } - return new Tuple(variable, bounds[variable]); - } - - private void SynthesizeExpression(ConcreteSyntaxTree wr, Expression expr, ConcreteSyntaxTree wStmts) { - switch (expr) { - case LiteralExpr literalExpr: - compiler.TrExpr(literalExpr, wr, false, wStmts); - break; - case ApplySuffix applySuffix: - SynthesizeExpression(wr, applySuffix, wStmts); - break; - case BinaryExpr binaryExpr: - SynthesizeExpression(wr, binaryExpr, wStmts); - break; - case ForallExpr forallExpr: - SynthesizeExpression(wr, forallExpr, wStmts); - break; - case FreshExpr: - break; - default: - // TODO: Have the resolver reject all these unimplemented cases, - // or convert them to UnsupportedFeatureExceptions - throw new NotImplementedException(); - } - } - - private void SynthesizeExpression(ConcreteSyntaxTree wr, ApplySuffix applySuffix, ConcreteSyntaxTree wStmts) { + + protected override void SynthesizeExpression(ConcreteSyntaxTree wr, ApplySuffix applySuffix, ConcreteSyntaxTree wStmts) { var methodApp = (ExprDotName)applySuffix.Lhs; var receiver = ((IdentifierExpr)methodApp.Lhs.Resolved).Var; @@ -174,7 +132,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, ApplySuffix applySuffix if (((Function)method).Ens.Count != 0) { compiler.Error(lastSynthesizedMethod.tok, "Post-conditions on function {0} might " + "be unsatisfied when synthesizing code " + - "for method {1}", ErrorWriter, + "for method {1}", errorWriter, methodName, lastSynthesizedMethod.Name); } @@ -198,7 +156,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, ApplySuffix applySuffix wr.Write("))"); } - private void SynthesizeExpression(ConcreteSyntaxTree wr, BinaryExpr binaryExpr, ConcreteSyntaxTree wStmts) { + protected override void SynthesizeExpression(ConcreteSyntaxTree wr, BinaryExpr binaryExpr, ConcreteSyntaxTree wStmts) { if (binaryExpr.Op == BinaryExpr.Opcode.And) { Dictionary oldBounds = bounds .ToDictionary(entry => entry.Key, entry => entry.Value); @@ -216,7 +174,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, BinaryExpr binaryExpr, var fieldName = field.CompileName; compiler.Error(lastSynthesizedMethod.tok, "Stubbing fields is not recommended " + "(field {0} of object {1} inside method {2})", - ErrorWriter, fieldName, obj.Name, lastSynthesizedMethod.Name); + errorWriter, fieldName, obj.Name, lastSynthesizedMethod.Name); wr.Format($"{objectToMockName[obj]}.SetupGet({obj.CompileName} => {obj.CompileName}.@{fieldName}).Returns( "); compiler.TrExpr(binaryExpr.E1, wr, false, wStmts); wr.WriteLine(");"); @@ -248,7 +206,7 @@ private void SynthesizeExpression(ConcreteSyntaxTree wr, BinaryExpr binaryExpr, wr.WriteLine(");"); } - private void SynthesizeExpression(ConcreteSyntaxTree wr, ForallExpr forallExpr, ConcreteSyntaxTree wStmts) { + protected override void SynthesizeExpression(ConcreteSyntaxTree wr, ForallExpr forallExpr, ConcreteSyntaxTree wStmts) { if (forallExpr.Term is not BinaryExpr binaryExpr) { throw new NotImplementedException(); } diff --git a/Source/DafnyCore/Compilers/Synthesizer-Java.cs b/Source/DafnyCore/Compilers/Synthesizer-Java.cs new file mode 100644 index 00000000000..57bc3941e24 --- /dev/null +++ b/Source/DafnyCore/Compilers/Synthesizer-Java.cs @@ -0,0 +1,175 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text.RegularExpressions; + +namespace Microsoft.Dafny.Compilers; + +/// +/// Below is the full grammar of ensures clauses that can specify +/// the behavior of an object returned by a synthesize-annotated method +/// (S is the starting symbol, ID refers to a variable/field/method/type +/// identifier, EXPR stands for an arbitrary Dafny expression): +/// +/// S = FORALL +/// | EQUALS +/// | S && S +/// EQUALS = ID.ID (ARGLIST) == EXPR // stubs a method call +/// | EQUALS && EQUALS +/// FORALL = forall BOUNDVARS :: EXPR ==> EQUALS +/// ARGLIST = ID // this can be one of the bound variables +/// | EXPR // this expr may not reference any of the bound variables +/// | ARGLIST, ARGLIST +/// BOUNDVARS = ID : ID +/// | BOUNDVARS, BOUNDVARS +/// +/// +public class JavaSynthesizer : Synthesizer { + + public JavaSynthesizer(JavaCompiler compiler, ConcreteSyntaxTree errorWriter) { + this.compiler = compiler; + this.errorWriter = errorWriter; + } + + /// + /// Create a body of a method that synthesizes one or more objects. + /// For instance, the following Dafny method: + /// + /// method {:synthesize} CrossReferentialMock() + /// returns (e1:Even, e2:Even) + /// ensures fresh(e1) && fresh(e2) + /// ensures e1.Next() == e2 + /// ensures e2.Next() == e1 + /// + /// Gets compiled to the following Java code: + /// + /// public static void CrossReferentialMock(out Even e1Return, + /// out Even e2Return) { + /// Even e1Mock = org.mockito.Mockito.spy(Even.class); + /// Even e1 = e1Mock; + /// Even e2Mock = org.mockito.Mockito.spy(Even.class); + /// Even e2 = e2Mock; + /// org.mockito.Mockito.when(e1.Next()).thenReturn(e2); + /// org.mockito.Mockito.when(e2.Next()).thenReturn(e1); + /// return new dafny.Tuple2<>(e1Mock, e2Mock); + /// } + /// + public override ConcreteSyntaxTree SynthesizeMethod(Method method, + List typeArgs, bool createBody, + ConcreteSyntaxTree wr, bool forBodyInheritance, bool lookasideBody) { + + lastSynthesizedMethod = method; + if (compiler is not JavaCompiler javaCompiler) { + throw new Exception($"'{compiler}' is not of the type JavaCompiler"); + } + + // The following few lines are identical to those in Compiler.CreateMethod: + var customReceiver = createBody && + !forBodyInheritance && + compiler.NeedsCustomReceiver(method); + var keywords = javaCompiler.Keywords(true, true); + var returnType = javaCompiler.GetTargetReturnTypeReplacement(method, wr); + var typeParameters = javaCompiler.TypeParameters(SinglePassCompiler.TypeArgumentInstantiation. + ToFormals(javaCompiler.ForTypeParameters(typeArgs, method, lookasideBody))); + var parameters = javaCompiler + .GetMethodParameters(method, typeArgs, lookasideBody, customReceiver, returnType); + + var parameterString = parameters.ToString(); + wr = wr.NewBlock($"{keywords}{returnType} {compiler.PublicIdProtect(method.CompileName)}{typeParameters}({parameterString})"); + + // Create the mocks: + objectToMockName = method.Outs.ToDictionary(o => (IVariable)o, + o => o.CompileName + "Mock"); + string mockNames = null; + foreach (var (obj, mockName) in objectToMockName) { + var typeName = compiler.TypeName(obj.Type, wr, obj.Tok); + wr.FormatLine($"{typeName} {mockName} = org.mockito.Mockito.spy({typeName}.class);"); + wr.FormatLine($"{typeName} {obj.CompileName} = {mockName};"); + mockNames = mockNames + mockName + ", "; + } + + if (mockNames != null) { + mockNames = mockNames.Remove(mockNames.Length - 2); + } + + // Stub methods according to the Dafny post-conditions: + foreach (var ensureClause in method.Ens) { + bounds = new(); + var wStmts = wr.Fork(); + SynthesizeExpression(wr, ensureClause.E, wStmts); + } + + // Return the mocked objects: + wr.FormatLine(!returnType.Contains("Tuple") + ? (FormattableString)$"return {method.Outs[0].Name}Mock;" + : $"return new {returnType}<>({mockNames});"); + return wr; + } + + protected override void SynthesizeExpression(ConcreteSyntaxTree wr, ApplySuffix applySuffix, ConcreteSyntaxTree wStmts) { + + var methodApp = (ExprDotName)applySuffix.Lhs; + var receiver = ((IdentifierExpr)methodApp.Lhs.Resolved).Var; + var method = ((MemberSelectExpr)methodApp.Resolved).Member; + var methodName = method.CompileName; + + if (((Function)method).Ens.Count != 0) { + compiler.Error(lastSynthesizedMethod.tok, "Post-conditions on function {0} might " + + "be unsatisfied when synthesizing code " + + "for method {1}", errorWriter, + methodName, lastSynthesizedMethod.Name); + } + + wr.Format($"org.mockito.Mockito.when({objectToMockName[receiver]}.{methodName}("); + + // The remaining part of the method uses Mockitos's argument matching to + // describe the arguments for which the method should be stubbed + // (in Dafny, this condition is the antecedent over bound variables) + for (int i = 0; i < applySuffix.Args.Count; i++) { + var arg = applySuffix.Args[i]; + var bound = GetBound(arg); + if (bound != null) { // if true, arg is a bound variable + wr.Write(bound.Item2); + } else { + compiler.TrExpr(arg, wr, false, wStmts); + } + if (i != applySuffix.Args.Count - 1) { + wr.Write(", "); + } + } + wr.Write("))"); + } + + protected override void SynthesizeExpression(ConcreteSyntaxTree wr, BinaryExpr binaryExpr, ConcreteSyntaxTree wStmts) { + if (binaryExpr.Op == BinaryExpr.Opcode.And) { + Dictionary oldBounds = bounds + .ToDictionary(entry => entry.Key, entry => entry.Value); + SynthesizeExpression(wr, binaryExpr.E0, wStmts); + bounds = oldBounds; + SynthesizeExpression(wr, binaryExpr.E1, wStmts); + return; + } + if (binaryExpr.Op != BinaryExpr.Opcode.Eq) { + throw new NotImplementedException(); + } + if (binaryExpr.E0 is not ApplySuffix applySuffix) { + throw new NotImplementedException(); + } + SynthesizeExpression(wr, applySuffix, wStmts); + wr.Write(".thenReturn("); + compiler.TrExpr(binaryExpr.E1, wr, false, wStmts); + wr.WriteLine(");"); + } + + protected override void SynthesizeExpression(ConcreteSyntaxTree wr, ForallExpr forallExpr, ConcreteSyntaxTree wStmts) { + if (forallExpr.Term is not BinaryExpr binaryExpr) { + throw new NotImplementedException(); + } + + foreach (var boundVar in forallExpr.BoundVars) { + var varType = compiler.TypeName(boundVar.Type, wr, boundVar.tok); + bounds[boundVar] = $"org.mockito.Mockito.any({varType}.class)"; + } + SynthesizeExpression(wr, binaryExpr, wStmts); + } +} \ No newline at end of file diff --git a/Source/DafnyCore/Compilers/Synthesizer.cs b/Source/DafnyCore/Compilers/Synthesizer.cs new file mode 100644 index 00000000000..16e9cca5e09 --- /dev/null +++ b/Source/DafnyCore/Compilers/Synthesizer.cs @@ -0,0 +1,68 @@ +using System; +using System.Collections.Generic; + +namespace Microsoft.Dafny.Compilers; + +/// +/// Base class for synthesizers. Uses ensures clauses to specify +/// the behavior of an object returned by a synthesize-annotated method. +/// +public abstract class Synthesizer { + + protected SinglePassCompiler compiler; + protected ConcreteSyntaxTree errorWriter; + // maps identifiers to the names of the corresponding mock: + protected Dictionary objectToMockName = new(); + // associates a bound variable with the lambda passed to argument matcher + protected Dictionary bounds = new(); + protected Method lastSynthesizedMethod = null; + + /// + /// Create a body of a method that synthesizes one or more objects. + /// + public abstract ConcreteSyntaxTree SynthesizeMethod(Method method, + List typeArgs, bool createBody, + ConcreteSyntaxTree wr, bool forBodyInheritance, bool lookasideBody); + + /// + /// If the expression is a bound variable identifier, return the + /// variable and the string representation of the bounding condition + /// + protected Tuple GetBound(Expression exp) { + if (exp is not NameSegment) { + return null; + } + var variable = ((IdentifierExpr)exp.Resolved).Var; + if (!bounds.ContainsKey(variable)) { + return null; + } + return new Tuple(variable, bounds[variable]); + } + + protected void SynthesizeExpression(ConcreteSyntaxTree wr, Expression expr, ConcreteSyntaxTree wStmts) { + switch (expr) { + case LiteralExpr literalExpr: + compiler.TrExpr(literalExpr, wr, false, wStmts); + break; + case ApplySuffix applySuffix: + SynthesizeExpression(wr, applySuffix, wStmts); + break; + case BinaryExpr binaryExpr: + SynthesizeExpression(wr, binaryExpr, wStmts); + break; + case ForallExpr forallExpr: + SynthesizeExpression(wr, forallExpr, wStmts); + break; + case FreshExpr: + break; + default: + // TODO: Have the resolver reject all these unimplemented cases, + // or convert them to UnsupportedFeatureExceptions + throw new NotImplementedException(); + } + } + + protected abstract void SynthesizeExpression(ConcreteSyntaxTree wr, ApplySuffix applySuffix, ConcreteSyntaxTree wStmts); + protected abstract void SynthesizeExpression(ConcreteSyntaxTree wr, BinaryExpr binaryExpr, ConcreteSyntaxTree wStmts); + protected abstract void SynthesizeExpression(ConcreteSyntaxTree wr, ForallExpr forallExpr, ConcreteSyntaxTree wStmts); +} \ No newline at end of file diff --git a/Test/DafnyTests/DafnyTests.csproj b/Test/DafnyTests/DafnyTests.csproj index bd08c5c575e..2dd93868e05 100644 --- a/Test/DafnyTests/DafnyTests.csproj +++ b/Test/DafnyTests/DafnyTests.csproj @@ -1,4 +1,4 @@ - + net6.0 @@ -9,4 +9,4 @@ - + \ No newline at end of file diff --git a/docs/DafnyRef/Attributes.md b/docs/DafnyRef/Attributes.md index 742434493f3..136d8b59e3c 100644 --- a/docs/DafnyRef/Attributes.md +++ b/docs/DafnyRef/Attributes.md @@ -476,16 +476,17 @@ This is mostly helpful for debugging which assertion is taking the most time to ### 23.2.22. `{:synthesize}` {#sec-synthesize-attr} The `{:synthesize}` attribute must be used on methods that have no body and -return one or more fresh objects. During compilation, -the postconditions associated with such a -method are translated to a series of API calls to the target languages's -mocking framework. The object returned, therefore, behaves exactly as the -postconditions specify. If there is a possibility that this behavior violates -the specifications on the object's instance methods or hardcodes the values of -its fields, the compiler will throw an error but the compilation will go -through. Currently, this compilation pass is only supported in C# and requires -adding the latest version of the Moq library to the .csproj file before -generating the binary. +return one or more fresh or mocked objects. During compilation, the +postconditions associated with such a method are translated to a series of +API calls to the target languages's mocking framework. The object returned, +therefore, behaves exactly as the postconditions specify. If there is a +possibility that this behavior violates the specifications on the object's +instance methods or hardcodes the values of its fields, the compiler will +throw an error but the compilation will go through. + +Currently, this compilation pass is only supported in C# and Java. To use it for C#, +add the latest version of the Moq library to the .csproj file before +generating the binary. Not all Dafny postconditions can be successfully compiled - below is the grammar for postconditions that are supported (`S` is the start symbol, `EXPR` @@ -497,7 +498,7 @@ S = FORALL | EQUALS | S && S EQUALS = ID.ID (ARGLIST) == EXPR // stubs a function call - | ID.ID == EXPR // stubs field access + | ID.ID == EXPR // stubs field access, C# only | EQUALS && EQUALS FORALL = forall BOUNDVARS :: EXPR ==> EQUALS ARGLIST = ID // this can be one of the bound variables @@ -507,6 +508,9 @@ BOUNDVARS = ID : ID | BOUNDVARS, BOUNDVARS ``` +Note that stubbing field access is not supported for Java, as Java's mocking framework +(Mockito) does not allow fields to be stubbed. + ### 23.2.23. `{:options OPT0, OPT1, ... }` {#sec-attr-options} This attribute applies only to modules. It configures Dafny as if @@ -779,4 +783,3 @@ following attributes. * `{:weight}` * `{:yields}` - diff --git a/docs/dev/news/docs/dev/2024.feat b/docs/dev/news/docs/dev/2024.feat new file mode 100644 index 00000000000..910b8fb2f82 --- /dev/null +++ b/docs/dev/news/docs/dev/2024.feat @@ -0,0 +1 @@ +The Java backend now supports the {:synthesize} attribute. \ No newline at end of file