Draft of verification API to get discussion started on #2084

Source/Dafny.sln

@@ -34,6 +34,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern", "AutoExtern\Au
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern.Test", "AutoExtern.Test\AutoExtern.Test.csproj", "{A47E2F45-DEA3-4700-A82F-9506FEEB199A}"
 EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyAPI", "DafnyAPI\DafnyAPI.csproj", "{B7F0E978-15B2-43A6-A510-DB712FB53957}"
+EndProject
 Global
 	GlobalSection(SolutionConfigurationPlatforms) = preSolution
 		Debug|Any CPU = Debug|Any CPU
@@ -84,6 +86,10 @@ Global
 		{896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Release|Any CPU.ActiveCfg = Release|Any CPU
 		{896E7F24-FD59-4B34-A1BF-53C51DDBC9E9}.Release|Any CPU.Build.0 = Release|Any CPU
+		{B7F0E978-15B2-43A6-A510-DB712FB53957}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+		{B7F0E978-15B2-43A6-A510-DB712FB53957}.Debug|Any CPU.Build.0 = Debug|Any CPU
+		{B7F0E978-15B2-43A6-A510-DB712FB53957}.Release|Any CPU.ActiveCfg = Release|Any CPU
+		{B7F0E978-15B2-43A6-A510-DB712FB53957}.Release|Any CPU.Build.0 = Release|Any CPU
 		{F185BDC2-1327-47A4-A293-D3FCDC419867}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
 		{F185BDC2-1327-47A4-A293-D3FCDC419867}.Debug|Any CPU.Build.0 = Debug|Any CPU
 		{F185BDC2-1327-47A4-A293-D3FCDC419867}.Release|Any CPU.ActiveCfg = Release|Any CPU

Source/Dafny/DafnyMain.cs

@@ -66,7 +66,7 @@ public DafnyFile(string filePath, bool useStdin = false) {
         var asm = Assembly.LoadFile(filePath);
         string sourceText = null;
         foreach (var adata in asm.CustomAttributes) {
-          if (adata.Constructor.DeclaringType.Name == "DafnySourceAttribute") {
+          if (adata.Constructor.DeclaringType?.Name == "DafnySourceAttribute") {
             foreach (var args in adata.ConstructorArguments) {
               if (args.ArgumentType.FullName == "System.String") {
                 sourceText = (string)args.Value;
@@ -321,4 +321,4 @@ public static bool IsBoogieVerified(PipelineOutcome outcome, PipelineStatistics
     }
 
   }
-}
+}

Source/DafnyAPI/API.cs

@@ -0,0 +1,110 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
+// This is an experimental API for using Dafny as a library.
+// We expect it to change from version to version as we discover which features are needed by clients.
+
+using System.Runtime.Versioning;
+
+namespace Microsoft.Dafny {
+  public class DafnyEngine {
+    public DafnyOptions Options { get; }
+    public ErrorReporter Reporter { get; private set; }
+    public Boogie.ExecutionEngine BoogieEngine { get; }
+
+    private static DafnyEngine? _singleton;
+
+    public static DafnyEngine Init(ErrorReporter reporter, string[] commandLineOptions) {
+      _singleton ??= new DafnyEngine();
+      _singleton.Reporter = reporter;
+      _singleton.Options.Parse(commandLineOptions);
+      return _singleton;
+    }
+
+    private DafnyEngine() {
+      Options = DafnyOptions.Create();
+      Reporter = new ErrorReporterSink();
+      BoogieEngine = Boogie.ExecutionEngine.CreateWithoutSharedCache(Options);
+      DafnyOptions.Install(Options);
+    }
+
+    public DafnyInput CreateDafnyInput(string fname, string source) {
+      return new DafnyInput(this, fname, source);
+    }
+  }
+
+  public class DafnyInput {
+    private readonly DafnyEngine engine;
+    public string FileName { get; init; }
+    public string Source { get; init; }
+
+    internal DafnyInput(DafnyEngine engine, string fname, string source) {
+      this.engine = engine;
+      FileName = fname;
+      Source = source;
+    }
+
+    public bool Verify() {
+      return Translate() is { } boogieModules && VerifyBoogieModules(boogieModules);
+    }
+
+    public Program? Parse() {
+      var module = new LiteralModuleDecl(new DefaultModuleDecl(), null);
+      var builtIns = new BuiltIns();
+      var errors = new Errors(engine.Reporter);
+      if (Parser.Parse(Source, FileName, FileName, null, module, builtIns, errors) == 0 &&
+          Main.ParseIncludes(module, builtIns, new List<string>(), errors) == null) {
+        return new Program(FileName, module, builtIns, engine.Reporter);
+      }
+
+      return null;
+    }
+
+    public Program? Resolve() {
+      return Parse() is { } parsedProgram ? Resolve(parsedProgram) : null;
+    }
+
+    private Program? Resolve(Program parsedProgram) {
+      new Resolver(parsedProgram).ResolveProgram(parsedProgram);
+      return engine.Reporter.Count(ErrorLevel.Error) == 0 ? parsedProgram : null;
+    }
+
+    private List<Tuple<string, Boogie.Program>>? Translate(Program resolvedProgram) {
+      var flags = new Translator.TranslatorFlags {InsertChecksums = true, UniqueIdPrefix = FileName};
+      return Translator.Translate(resolvedProgram, engine.Reporter, flags).ToList();
+    }
+
+    public List<Tuple<string, Boogie.Program>>? Translate() {
+      return (Resolve() is { } resolvedProgram) ? Translate(resolvedProgram) : null;
+    }
+
+    public bool VerifyBoogieModule(string moduleName, Microsoft.Boogie.Program boogieProgram) {
+      if (boogieProgram.Resolve(engine.Options) == 0 && boogieProgram.Typecheck(engine.Options) == 0) {
+        engine.BoogieEngine.EliminateDeadVariables(boogieProgram);
+        engine.BoogieEngine.CollectModSets(boogieProgram);
+        engine.BoogieEngine.CoalesceBlocks(boogieProgram);
+        engine.BoogieEngine.Inline(boogieProgram);
+
+        // FIXME: Use reporter
+        switch (engine.BoogieEngine.InferAndVerify(Console.Out, boogieProgram, new Boogie.PipelineStatistics(),
+                  "ServerProgram_" + moduleName, null, DateTime.UtcNow.Ticks.ToString()).Result) {
+          case Boogie.PipelineOutcome.Done:
+          case Boogie.PipelineOutcome.VerificationCompleted:
+            return true;
+        }
+      }
+
+      return false;
+    }
+
+    public bool VerifyBoogieModules(List<Tuple<string, Boogie.Program>> boogieModules) {
+      foreach (var (moduleName, boogieProgram) in boogieModules) {
+        if (!VerifyBoogieModule(moduleName, boogieProgram)) {
+          return false;
+        }
+      }
+
+      return true;
+    }
+  }
+}

Source/DafnyAPI/DafnyAPI.csproj

@@ -0,0 +1,13 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+    <PropertyGroup>
+        <TargetFramework>net6.0</TargetFramework>
+        <ImplicitUsings>enable</ImplicitUsings>
+        <Nullable>enable</Nullable>
+    </PropertyGroup>
+
+    <ItemGroup>
+      <ProjectReference Include="..\Dafny\DafnyPipeline.csproj" />
+    </ItemGroup>
+
+</Project>

Source/DafnyServer/DafnyServer.csproj

@@ -20,6 +20,7 @@
   </PropertyGroup>
 
   <ItemGroup>
+    <ProjectReference Include="..\DafnyAPI\DafnyAPI.csproj" />
     <ProjectReference Include="..\Dafny\DafnyPipeline.csproj" />
   </ItemGroup>