Add support for Java mocking

.gitignore

@@ -64,4 +64,10 @@ Source/.vs
 
 node_modules/
 package.json
-package-lock.json
+package-lock.json
+
+
+lecture_programs
+natural_doc
+natural_config
+Working\ Data

Scripts/post-create.sh

@@ -0,0 +1,17 @@
+#!/usr/bin/env bash
+
+# find the source directory for this script even if it's been symlinked [issue #185]
+# from https://stackoverflow.com/questions/59895/
+SOURCE="${BASH_SOURCE[0]}"
+while [ -h "$SOURCE" ]; do
+    DIR="$( cd -P "$( dirname "$SOURCE" )" && pwd )"
+    SOURCE="$(readlink "$SOURCE")"
+    [[ $SOURCE != /* ]] && SOURCE="$DIR/$SOURCE"
+done
+DAFNY_ROOT="$( cd -P "$( dirname $( dirname "$SOURCE" ))" && pwd )"
+
+cd $DAFNY_ROOT
+# pre-commit install
+npm install bignumber.js 
+cd $DAFNY_ROOT/Binaries
+ln -s /opt/z3/z3-4.8.5-x64-ubuntu-16.04/ z3

Source/Dafny.sln

@@ -16,6 +16,7 @@ EndProject
 Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Solution Items", "Solution Items", "{9542E008-355F-4A62-B262-A8DA314DA8C1}"
 	ProjectSection(SolutionItems) = preProject
 		version.cs = version.cs
+		global.json = global.json
 	EndProjectSection
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "IntegrationTests", "IntegrationTests\IntegrationTests.csproj", "{A4BC2C77-3A48-4917-AA22-41978DFFE24E}"

Source/Dafny/Compilers/Compiler-Csharp.cs

@@ -1162,6 +1162,10 @@ public ConcreteSyntaxTree SynthesizeMethod(Method method, List<TypeArgumentInsta
         return csharpSynthesizer.SynthesizeMethod(method, typeArgs, createBody, Writer(method.IsStatic, createBody, method), forBodyInheritance, lookasideBody);
       }
 
+      public ConcreteSyntaxTree CreateFreshMethod(Method m) {
+         return csharpSynthesizer.CreateFreshMethod(m, Writer(m.IsStatic, true, m));
+      }
+
       public ConcreteSyntaxTree /*?*/ CreateFunction(string name, List<TypeArgumentInstantiation> typeArgs, List<Formal> formals, Type resultType, Bpl.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);
       }

Source/Dafny/Compilers/Compiler-cpp.cs

@@ -733,6 +733,10 @@ public ConcreteSyntaxTree SynthesizeMethod(Method m, List<TypeArgumentInstantiat
         throw new UnsupportedFeatureException(m.tok, Feature.MethodSynthesis);
       }
 
+      public ConcreteSyntaxTree CreateFreshMethod(Method m) {
+         throw new NotImplementedException();
+      }
+
       public ConcreteSyntaxTree/*?*/ CreateFunction(string name, List<TypeArgumentInstantiation>/*?*/ typeArgs, List<Formal> formals, Type resultType, Bpl.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);
       }

Source/Dafny/Compilers/Compiler-go.cs

@@ -1030,6 +1030,10 @@ public ConcreteSyntaxTree SynthesizeMethod(Method m, List<TypeArgumentInstantiat
         throw new UnsupportedFeatureException(m.tok, Feature.MethodSynthesis);
       }
 
+      public ConcreteSyntaxTree CreateFreshMethod(Method m) {
+         throw new NotImplementedException();
+      }
+
       public ConcreteSyntaxTree/*?*/ CreateFunction(string name, List<TypeArgumentInstantiation> typeArgs, List<Formal> formals, Type resultType, Bpl.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);
       }

Source/Dafny/Compilers/Compiler-java.cs

@@ -31,6 +31,9 @@ public override void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection<str
 
     public override string TargetLanguage => "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) =>
@@ -182,6 +185,22 @@ protected override void DeclareSpecificOutCollector(string collectorVarName, Con
         wr.Write($"{returnedTypes[0]} {collectorVarName} = ");
       }
     }
+
+    /// <summary>
+    /// Return true if the AST contains a method annotated with an attribute
+    /// </summary>
+    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<string> lhsNames,
       ConcreteSyntaxTree wr, List<Type> formalTypes, List<Type> lhsTypes, Bpl.IToken tok) {
       var wOuts = new List<ConcreteSyntaxTree>();
@@ -322,6 +341,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();
@@ -411,6 +431,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);
@@ -419,6 +440,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) {
@@ -434,8 +456,13 @@ 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<TypeArgumentInstantiation> typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody) {
-        throw new UnsupportedFeatureException(m.tok, Feature.MethodSynthesis);
+      public ConcreteSyntaxTree CreateFreshMethod(Method m) {
+        return javaSynthesizer.CreateFreshMethod(m, Writer(m.IsStatic, true, m));
+      }
+
+      public ConcreteSyntaxTree SynthesizeMethod(Method method, List<TypeArgumentInstantiation> 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<TypeArgumentInstantiation> typeArgs, List<Formal> formals, Type resultType, Bpl.IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) {
@@ -501,6 +528,7 @@ protected override void DeclareLocalVar(string name, Type /*?*/ type, Bpl.IToken
       }
       return wGet;
     }
+
     protected ConcreteSyntaxTree CreateMethod(Method m, List<TypeArgumentInstantiation> 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
@@ -522,7 +550,7 @@ protected ConcreteSyntaxTree CreateMethod(Method m, List<TypeArgumentInstantiati
       }
       var customReceiver = createBody && !forBodyInheritance && NeedsCustomReceiver(m);
       var receiverType = UserDefinedType.FromTopLevelDecl(m.tok, m.EnclosingClass);
-      wr.Write("public {0}{1}", !createBody && !(m.EnclosingClass is TraitDecl) ? "abstract " : "", m.IsStatic || customReceiver ? "static " : "");
+      wr.Write("public {0}{1}", !createBody && m.EnclosingClass is not TraitDecl ? "abstract " : "", m.IsStatic || customReceiver ? "static " : "");
       wr.Write(TypeParameters(TypeArgumentInstantiation.ToFormals(ForTypeParameters(typeArgs, m, lookasideBody)), " "));
       wr.Write("{0} {1}", targetReturnTypeReplacement ?? "void", IdName(m));
       wr.Write("(");
@@ -541,6 +569,48 @@ protected ConcreteSyntaxTree CreateMethod(Method m, List<TypeArgumentInstantiati
       }
     }
 
+    internal string Keywords(bool isPublic = false, bool isStatic = false, bool isExtern = false) {
+      return (isPublic ? "public " : "") + (isStatic ? "static " : "") + (isExtern ? "extern " : "") + (Synthesize && !isStatic && isPublic ? "virtual " : "");
+    }
+
+    internal ConcreteSyntaxTree GetMethodParameters(Method m, List<TypeArgumentInstantiation> typeArgs, bool lookasideBody, bool customReceiver, string returnType) {
+      //var parameters = GetFunctionParameters(m.Ins, m, typeArgs, lookasideBody, customReceiver);
+      var parameters = new ConcreteSyntaxTree();
+      var sep = "";
+      WriteRuntimeTypeDescriptorsFormals(m, 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) {
@@ -614,7 +684,7 @@ private void EmitSuppression(ConcreteSyntaxTree wr) {
       wr.WriteLine("@SuppressWarnings({\"unchecked\", \"deprecation\"})");
     }
 
-    string TypeParameters(List<TypeParameter>/*?*/ targs, string suffix = "") {
+    internal string TypeParameters(List<TypeParameter>/*?*/ targs, string suffix = "") {
       Contract.Requires(targs == null || cce.NonNullElements(targs));
       Contract.Ensures(Contract.Result<string>() != null);
 

Source/Dafny/Compilers/Compiler-js.cs

@@ -612,6 +612,10 @@ public ConcreteSyntaxTree SynthesizeMethod(Method m, List<TypeArgumentInstantiat
         throw new UnsupportedFeatureException(m.tok, Feature.MethodSynthesis);
       }
 
+      public ConcreteSyntaxTree CreateFreshMethod(Method m) {
+         throw new NotImplementedException();
+      }
+
       public ConcreteSyntaxTree/*?*/ CreateFunction(string name, List<TypeArgumentInstantiation> typeArgs, List<Formal> formals, Type resultType, Bpl.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);
       }

Source/Dafny/Compilers/Compiler-python.cs

@@ -351,6 +351,10 @@ public ConcreteSyntaxTree SynthesizeMethod(Method m, List<TypeArgumentInstantiat
         throw new UnsupportedFeatureException(Token.NoToken, Feature.MethodSynthesis);
       }
 
+      public ConcreteSyntaxTree CreateFreshMethod(Method m) {
+         throw new NotImplementedException();
+      }
+
       public ConcreteSyntaxTree CreateFunction(string name, List<TypeArgumentInstantiation> typeArgs,
           List<Formal> formals, Type resultType, IToken tok, bool isStatic, bool createBody, MemberDecl member,
           bool forBodyInheritance, bool lookasideBody) {

Source/Dafny/Compilers/SinglePassCompiler.cs

@@ -114,6 +114,7 @@ public override void OnPostCompile() {
     protected interface IClassWriter {
       ConcreteSyntaxTree/*?*/ CreateMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody);
       ConcreteSyntaxTree/*?*/ SynthesizeMethod(Method m, List<TypeArgumentInstantiation> typeArgs, bool createBody, bool forBodyInheritance, bool lookasideBody);
+      ConcreteSyntaxTree/*?*/ CreateFreshMethod(Method m);
       ConcreteSyntaxTree/*?*/ CreateFunction(string name, List<TypeArgumentInstantiation> typeArgs, List<Formal> formals, Type resultType, Bpl.IToken tok, bool isStatic, bool createBody,
         MemberDecl member, bool forBodyInheritance, bool lookasideBody);
       ConcreteSyntaxTree/*?*/ CreateGetter(string name, TopLevelDecl enclosingDecl, Type resultType, Bpl.IToken tok, bool isStatic, bool isConst, bool createBody, MemberDecl/*?*/ member, bool forBodyInheritance);  // returns null iff !createBody
@@ -1406,6 +1407,10 @@ public ConcreteSyntaxTree SynthesizeMethod(Method m, List<TypeArgumentInstantiat
         throw new UnsupportedFeatureException(m.tok, Feature.MethodSynthesis);
       }
 
+      public ConcreteSyntaxTree CreateFreshMethod(Method m) {
+        throw new NotImplementedException();
+      }
+
       public ConcreteSyntaxTree/*?*/ CreateFunction(string name, List<TypeArgumentInstantiation> typeArgs, List<Formal> formals, Type resultType, Bpl.IToken tok, bool isStatic, bool createBody, MemberDecl member, bool forBodyInheritance, bool lookasideBody) {
         return createBody ? block : null;
       }
@@ -1918,18 +1923,34 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite
           v.Visit(f);
         } else if (member is Method m) {
           if (Attributes.Contains(m.Attributes, "synthesize")) {
-            if (m.IsStatic && m.Outs.Count > 0 && m.Body == null) {
-              classWriter.SynthesizeMethod(m, CombineAllTypeArguments(m), true, true, false);
-            } else {
-              Error(m.tok, "Method {0} is annotated with :synthesize but " +
+            var args = Attributes.FindExpressions(m.Attributes, "synthesize");
+            if (args != null && (string)(args[0] as StringLiteralExpr)?.Value == "mock") {
+              if (m.IsStatic && m.Outs.Count > 0 && m.Body == null) {
+                classWriter.SynthesizeMethod(m, CombineAllTypeArguments(m), true, true, false);
+              } else {
+                Error(m.tok, "Method {0} is annotated with :synthesize but " +
                            "is not static, has a body, or does not return " +
                            "anything",
                 errorWr, m.FullName);
+              }
+            } else if (args != null && (string)(args[0] as StringLiteralExpr)?.Value == "fresh") {
+              if (m.IsStatic && m.Outs.Count > 0 && m.Body == null) {
+                classWriter.CreateFreshMethod(m);
+              } else {
+                Error(m.tok, "Method {0} is annotated with :synthesize but " +
+                           "is not static, has a body, or does not return " +
+                           "anything",
+                errorWr, m.FullName);
+              }
+            } else {
+              Error(m.tok, "Method {0} is annotated with :synthesize but " +
+                          "does not have the required parameters",
+                errorWr, m.FullName);
             }
           } else if (m.Body == null && !(c is TraitDecl && !m.IsStatic) &&
                      !(!DafnyOptions.O.DisallowExterns && (Attributes.Contains(m.Attributes, "dllimport") || (IncludeExternMembers && Attributes.Contains(m.Attributes, "extern"))))) {
             // A (ghost or non-ghost) method must always have a body, except if it's an instance method in a trait.
-            if (Attributes.Contains(m.Attributes, "axiom") || (!DafnyOptions.O.DisallowExterns && Attributes.Contains(m.Attributes, "extern"))) {
+            if (Attributes.Contains(m.Attributes, "axiom")) {
               // suppress error message
             } else {
               Error(m.tok, "Method {0} has no body", errorWr, m.FullName);
@@ -2823,7 +2844,7 @@ void TrStmtNonempty(Statement stmt, ConcreteSyntaxTree wr) {
     protected internal void TrStmt(Statement stmt, ConcreteSyntaxTree wr) {
       Contract.Requires(stmt != null);
       Contract.Requires(wr != null);
-
+      
       if (stmt.IsGhost) {
         return;
       }

Source/Dafny/Compilers/Synthesizer-Csharp.cs

@@ -41,6 +41,18 @@ public CsharpSynthesizer(CsharpCompiler compiler, ConcreteSyntaxTree errorWriter
     ErrorWriter = errorWriter;
   }
 
+  /// <summary>
+  /// Create a body for a method returning a fresh instance of an object 
+  /// </summary>
+  public ConcreteSyntaxTree CreateFreshMethod(Method m,
+    ConcreteSyntaxTree wr) {
+    var keywords = "public static ";
+    var returnType = compiler.GetTargetReturnTypeReplacement(m, wr);
+    wr = wr.NewBlock($"{keywords}{returnType} {m.CompileName}()");
+    wr.FormatLine($"return new {returnType}();");
+    return wr;
+  }
+
   /// <summary>
   /// Create a body of a method that synthesizes one or more objects.
   /// For instance, the following Dafny method: