Basic implementation of proof dependency analysis

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -2,7 +2,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Numerics;
-using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
 

Source/DafnyCore/AST/Program.cs

@@ -30,6 +30,7 @@ void ObjectInvariant() {
  public SystemModuleManager SystemModuleManager;
  public DafnyOptions Options => Reporter.Options;
  public ErrorReporter Reporter { get; set; }
+ public ProofDependencyManager ProofDependencyManager { get; set; }
 
  public Program(string name, [Captured] LiteralModuleDecl module, [Captured] SystemModuleManager systemModuleManager, ErrorReporter reporter,
  CompilationData compilation) {

Source/DafnyCore/AST/SystemModuleManager.cs

@@ -6,7 +6,6 @@
 using System.Linq;
 using System.Security.Cryptography;
 using System.Security.Policy;
-using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
 

Source/DafnyCore/AST/TypeDeclarations/TupleTypeDecl.cs

@@ -2,7 +2,6 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using JetBrains.Annotations;
-using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
 

Source/DafnyCore/Compilers/Python/Compiler-python.cs

@@ -10,7 +10,6 @@
 using JetBrains.Annotations;
 using ExtensionMethods;
 using Microsoft.BaseTypes;
-using Microsoft.Boogie;
 
 namespace ExtensionMethods {
  using Microsoft.Dafny;

Source/DafnyCore/DafnyCore.csproj

@@ -32,7 +32,7 @@
  <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
  <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
  <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
- <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.0" />
+ <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.1" />
  <PackageReference Include="Tomlyn" Version="0.16.2" />
  </ItemGroup>
 

Source/DafnyCore/Feature.cs

@@ -1,7 +1,6 @@
 using System;
 using System.Diagnostics.Contracts;
 using System.Linq;
-using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
 

Source/DafnyCore/JsonDiagnostics.cs

@@ -6,7 +6,6 @@
 using System.Linq;
 using System.Text.Json;
 using System.Text.Json.Nodes;
-using Microsoft.Boogie;
 using VCGeneration;
 using static Microsoft.Dafny.ErrorRegistry;
 

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -3,7 +3,6 @@
 using System.IO;
 using System.Linq;
 using DafnyCore;
-using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
 

Source/DafnyCore/Resolver/BoundsDiscovery.cs

@@ -7,7 +7,6 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Diagnostics.Contracts;
-using Microsoft.Boogie;
 
 namespace Microsoft.Dafny {
  public partial class ModuleResolver {

Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs

@@ -1,5 +1,4 @@
 using System.Diagnostics.Contracts;
-using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
 

Source/DafnyCore/Resolver/GhostInterestVisitor.cs

@@ -1,7 +1,6 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using JetBrains.Annotations;
-using Microsoft.Boogie;
 using static Microsoft.Dafny.ResolutionErrors;
 
 namespace Microsoft.Dafny;

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs

@@ -15,7 +15,6 @@
 using System.Reflection;
 using JetBrains.Annotations;
 using Microsoft.BaseTypes;
-using Microsoft.Boogie;
 using Microsoft.CodeAnalysis.CSharp.Syntax;
 using Microsoft.Dafny.Plugins;
 

Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs

@@ -9,7 +9,6 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Diagnostics.Contracts;
-using Microsoft.Boogie;
 
 namespace Microsoft.Dafny {
  public class Advice {

Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs

@@ -8,7 +8,6 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Diagnostics.Contracts;
-using Microsoft.Boogie;
 using ResolutionContext = Microsoft.Dafny.ResolutionContext;
 
 namespace Microsoft.Dafny {

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -10,7 +10,6 @@
 using System.Linq;
 using System.Numerics;
 using System.Diagnostics.Contracts;
-using Microsoft.Boogie;
 using ResolutionContext = Microsoft.Dafny.ResolutionContext;
 
 namespace Microsoft.Dafny {

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Statements.cs

@@ -13,7 +13,6 @@
 using System.Diagnostics.Contracts;
 using System.Runtime.Intrinsics.X86;
 using JetBrains.Annotations;
-using Microsoft.Boogie;
 using Bpl = Microsoft.Boogie;
 using ResolutionContext = Microsoft.Dafny.ResolutionContext;
 

Source/DafnyCore/Resolver/TypeConstraint.cs

@@ -11,8 +11,6 @@
 using System.Numerics;
 using System.Diagnostics.Contracts;
 using JetBrains.Annotations;
-using Microsoft.BaseTypes;
-using Microsoft.Boogie;
 using Microsoft.CodeAnalysis.CSharp.Syntax;
 
 namespace Microsoft.Dafny {

Source/DafnyCore/Rewriters/BitvectorOptimization.cs

@@ -4,7 +4,6 @@
 using System;
 using System.Linq.Expressions;
 using System.Numerics;
-using Microsoft.Boogie;
 
 namespace Microsoft.Dafny;
 

Source/DafnyCore/Rewriters/RunAllTestsMainMethod.cs

@@ -1,7 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
-using Microsoft.Boogie;
 using System.Text.RegularExpressions;
 using static Microsoft.Dafny.RewriterErrors;
 

Source/DafnyCore/Triggers/QuantifierSplitter.cs

@@ -1,7 +1,6 @@
 // Copyright by the contributors to the Dafny Project
 // SPDX-License-Identifier: MIT
 
-using Microsoft.Boogie;
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;

Source/DafnyCore/Triggers/QuantifiersCollection.cs

@@ -7,7 +7,6 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Text;
-using Microsoft.Boogie;
 using System.Diagnostics.Contracts;
 using static Microsoft.Dafny.ErrorRegistry;
 

Source/DafnyCore/Triggers/QuantifiersCollector.cs

@@ -5,7 +5,6 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Text;
-using Microsoft.Boogie;
 using System.Collections.ObjectModel;
 using System.Diagnostics.Contracts;
 

Source/DafnyCore/Verifier/ProofDependency.cs

@@ -0,0 +1,209 @@
+// Copyright (C) Microsoft Corporation. All Rights Reserved.
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+//
+//-----------------------------------------------------------------------------
+using Microsoft.Dafny;
+using IToken = Microsoft.Dafny.IToken;
+using PODesc = Microsoft.Dafny.ProofObligationDescription;
+
+namespace DafnyCore.Verifier;
+
+// A proof dependency represents a particular part of a Dafny program
+// that may be used in the process of proving its correctness. When
+// Boogie proves a particular verification condition, it returns a
+// list of strings, returned by the SMT solver, indicating which
+// program elements were used in completing the proof. After this, the
+// ProofDependencyManager can map each string to a more structured
+// ProofDependency.
+public abstract class ProofDependency {
+ public abstract string Description { get; }
+
+ public abstract RangeToken Range { get; }
+
+ public string LocationString() {
+ if (Range?.StartToken is null) {
+ return "<no location>";
+ }
+ var fn = Range.StartToken.filename;
+ var sl = Range.StartToken.line;
+ var sc = Range.StartToken.col - 1;
+ return $"{fn}({sl},{sc})";
+ }
+
+ public string RangeString() {
+ if (Range?.StartToken is null) {
+ return "<no range>";
+ }
+ var fn = Range.StartToken.filename;
+ var sl = Range.StartToken.line;
+ var sc = Range.StartToken.col - 1;
+ var el = Range.EndToken.line;
+ var ec = Range.EndToken.col - 1;
+ return $"{fn}({sl},{sc})-({el},{ec})";
+ }
+
+ public string OriginalString() {
+ return Range?.PrintOriginal();
+ }
+}
+
+// Represents the portion of a Dafny program corresponding to a proof
+// obligation. This is particularly important to track because if a particular
+// assertion batch can be proved without proving one of the assertions that is
+// a proof obligation within it, that assertion must have been proved vacuously.
+public class ProofObligationDependency : ProofDependency {
+ public override RangeToken Range { get; }
+
+ public PODesc.ProofObligationDescription ProofObligation { get; }
+
+ public override string Description =>
+ $"{ProofObligation.SuccessDescription}";
+
+ public ProofObligationDependency(IToken tok, PODesc.ProofObligationDescription proofObligation) {
+ Range = tok as RangeToken ?? new RangeToken(tok, tok);
+ ProofObligation = proofObligation;
+ }
+}
+
+// Represents the assumption of a requires clause in the process of
+// proving a Dafny definition.
+public class RequiresDependency : ProofDependency {
+ private Expression requires;
+
+ public override RangeToken Range =>
+ requires.RangeToken;
+
+ public override string Description =>
+ $"requires clause";
+
+ public RequiresDependency(Expression requires) {
+ this.requires = requires;
+ }
+}
+
+// Represents the goal of proving an ensures clause of a Dafny definition.
+public class EnsuresDependency : ProofDependency {
+ private Expression ensures;
+
+ public override RangeToken Range =>
+ ensures.RangeToken;
+
+ public override string Description =>
+ "ensures clause";
+
+ public EnsuresDependency(Expression ensures) {
+ this.ensures = ensures;
+ }
+}
+
+// Represents the goal of proving a specific requires clause of a specific
+// call.
+public class CallRequiresDependency : ProofDependency {
+ private CallDependency call;
+ private RequiresDependency requires;
+
+ public override RangeToken Range =>
+ call.Range;
+
+ public override string Description =>
+ $"requires clause at {requires.RangeString()} from call";
+
+ public CallRequiresDependency(CallDependency call, RequiresDependency requires) {
+ this.call = call;
+ this.requires = requires;
+ }
+}
+
+// Represents the assumption of a specific ensures clause of a specific
+// call.
+public class CallEnsuresDependency : ProofDependency {
+ private CallDependency call;
+ private EnsuresDependency ensures;
+
+ public override RangeToken Range =>
+ call.Range;
+
+ public override string Description =>
+ $"ensures clause at {ensures.RangeString()} from call";
+
+ public CallEnsuresDependency(CallDependency call, EnsuresDependency ensures) {
+ this.call = call;
+ this.ensures = ensures;
+ }
+}
+
+// Represents the fact that a particular call occurred.
+public class CallDependency : ProofDependency {
+ private CallStmt call;
+
+ public override RangeToken Range =>
+ call.RangeToken;
+
+ public override string Description =>
+ $"call";
+
+ public CallDependency(CallStmt call) {
+ this.call = call;
+ }
+}
+
+// Represents the assumption of a predicate in an `assume` statement.
+public class AssumptionDependency : ProofDependency {
+ private Expression expr;
+
+ public override RangeToken Range =>
+ expr.RangeToken;
+
+ public override string Description =>
+ comment ?? $"assume {OriginalString()}";
+
+ private string comment;
+
+ public AssumptionDependency(string comment, Expression expr) {
+ this.comment = comment;
+ this.expr = expr;
+ }
+}
+
+// Represents the invariant of a loop.
+public class InvariantDependency : ProofDependency {
+ private Expression invariant;
+
+ public override RangeToken Range =>
+ invariant.RangeToken;
+
+ public override string Description =>
+ $"loop invariant";
+
+ public InvariantDependency(Expression invariant) {
+ this.invariant = invariant;
+ }
+}
+
+// Represents an assignment statement. This includes the assignment to an
+// out parameter implicit in a return statement.
+public class AssignmentDependency : ProofDependency {
+ public override RangeToken Range { get; }
+
+ public override string Description =>
+ "assignment (or return)";
+
+ public AssignmentDependency(RangeToken rangeToken) {
+ this.Range = rangeToken;
+ }
+}
+
+// Represents dependency of a proof on the definition of a specific function.
+public class FunctionDefinitionDependency : ProofDependency {
+ public override RangeToken Range => function.RangeToken;
+
+ public override string Description =>
+ $"function definition for {function.Name}";
+
+ private Function function;
+
+ public FunctionDefinitionDependency(Function f) {
+ function = f;
+ }
+}