Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Filter assertions #5031

Merged
merged 50 commits into from
Feb 8, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
50 commits
Select commit Hold shift + click to select a range
4b98f81
Fix build errors for new Boogie version
keyboardDrummer Jan 31, 2024
d225e31
Add Boogie as a submodule
keyboardDrummer Jan 31, 2024
ea44d00
Trying to get back to existing behavior
keyboardDrummer Jan 31, 2024
d138919
Exclude boogie folder in format command
keyboardDrummer Jan 31, 2024
5350dfa
Fixes
keyboardDrummer Jan 31, 2024
3874586
Rename
keyboardDrummer Jan 31, 2024
87b22dd
Step towards getting RedundantAssumptionsGetWarnings to work again
keyboardDrummer Jan 31, 2024
536b1c4
RedundantAssumptionsGetWarnings works now
keyboardDrummer Jan 31, 2024
a035817
Merge remote-tracking branch 'origin/master' into filterAssertions
keyboardDrummer Jan 31, 2024
178b85a
Trigger CI
keyboardDrummer Jan 31, 2024
bed7a5d
Enable --filter-position on individual assertions/ensures clauses, fi…
keyboardDrummer Feb 1, 2024
cfe91fd
Fixes
keyboardDrummer Feb 1, 2024
775adbb
Update expect files
keyboardDrummer Feb 1, 2024
7a1c3e6
Gutter icon fixes
keyboardDrummer Feb 2, 2024
8b0f648
Fix gutter test
keyboardDrummer Feb 2, 2024
31da8ed
Ran formatter
keyboardDrummer Feb 2, 2024
cef25e0
Fix bug
keyboardDrummer Feb 2, 2024
634921e
Use SplitIndex
keyboardDrummer Feb 2, 2024
4337c01
Fix status bug and fix tests
keyboardDrummer Feb 2, 2024
0ee78f5
Fix counter example bug
keyboardDrummer Feb 2, 2024
90885ea
Trigger CI
keyboardDrummer Feb 2, 2024
60ebf1b
Merge remote-tracking branch 'origin/master' into filterAssertions
keyboardDrummer Feb 2, 2024
c12e426
Refactoring
keyboardDrummer Feb 2, 2024
a3e9277
Update expect file
keyboardDrummer Feb 2, 2024
a65dda0
Updato to latest Boogie
keyboardDrummer Feb 2, 2024
53b0427
Remove submodule
keyboardDrummer Feb 2, 2024
cb1ddf5
Add code to help debug problems
keyboardDrummer Feb 5, 2024
28e5c3b
Fix missing exception
keyboardDrummer Feb 5, 2024
06cfe77
Halt earlier:
keyboardDrummer Feb 5, 2024
01f3eca
Merge branch 'master' into filterAssertions
keyboardDrummer Feb 5, 2024
1f734dc
Add more tests to filter.dfy file
keyboardDrummer Feb 5, 2024
78b4332
Improve verification summary when using a line filter
keyboardDrummer Feb 5, 2024
797567e
Fix customBoogie.patch
keyboardDrummer Feb 5, 2024
b7bdfab
Add a timeout on the queue task
keyboardDrummer Feb 5, 2024
1957d33
Merge branch 'filterAssertions' of github.com:keyboardDrummer/dafny i…
keyboardDrummer Feb 5, 2024
b65691a
Fix path
keyboardDrummer Feb 6, 2024
c06af7a
Remove obsolete code
keyboardDrummer Feb 6, 2024
07f5f10
Add test-case and allow not specifying the filter position filename
keyboardDrummer Feb 6, 2024
b025fac
Add missing capital
keyboardDrummer Feb 6, 2024
3931b5e
Merge branch 'master' into filterAssertions
keyboardDrummer Feb 6, 2024
db5561e
Configure test timeout
keyboardDrummer Feb 6, 2024
b4ea428
Merge branch 'filterAssertions' of github.com:keyboardDrummer/dafny i…
keyboardDrummer Feb 6, 2024
5f38dc9
Merge branch 'master' into filterAssertions
keyboardDrummer Feb 7, 2024
5d2a749
Fixes
keyboardDrummer Feb 7, 2024
154d342
Merge branch 'filterAssertions' of github.com:keyboardDrummer/dafny i…
keyboardDrummer Feb 7, 2024
f2f0c65
Remove duplication and make error message more specific
keyboardDrummer Feb 7, 2024
fcf801b
Merge remote-tracking branch 'origin/master' into filterAssertions
keyboardDrummer Feb 8, 2024
1683a4b
Remove unused check
keyboardDrummer Feb 8, 2024
201e4ca
Fix counterexample tracking
keyboardDrummer Feb 8, 2024
0c644b4
Merge branch 'master' into filterAssertions
atomb Feb 8, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -73,7 +73,7 @@ z3-ubuntu:
chmod +x ${DIR}/Binaries/z3/bin/z3-*

format:
dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs
dotnet format whitespace Source/Dafny.sln --exclude Source/DafnyCore/Scanner.cs --exclude Source/DafnyCore/Parser.cs --exclude boogie --exclude Source/DafnyCore/GeneratedFromDafny.cs --exclude Source/DafnyRuntime/DafnyRuntimeSystemModule.cs

clean:
(cd ${DIR}; cd Source; rm -rf Dafny/bin Dafny/obj DafnyDriver/bin DafnyDriver/obj DafnyRuntime/obj DafnyRuntime/bin DafnyServer/bin DafnyServer/obj DafnyPipeline/obj DafnyPipeline/bin DafnyCore/obj DafnyCore/bin)
Expand Down
11 changes: 11 additions & 0 deletions Source/DafnyCore/AST/Tokens.cs
Original file line number Diff line number Diff line change
Expand Up @@ -109,6 +109,13 @@ public IToken WithVal(string newVal) {
};
}

public int CompareTo(Boogie.IToken other) {
if (line != other.line) {
return line.CompareTo(other.line);
}
return col.CompareTo(other.col);
}

public override int GetHashCode() {
return pos;
}
Expand Down Expand Up @@ -189,6 +196,10 @@ public virtual IToken Prev {
public int CompareTo(IToken other) {
return WrappedToken.CompareTo(other);
}

public int CompareTo(Boogie.IToken other) {
return WrappedToken.CompareTo(other);
}
}

public static class TokenExtensions {
Expand Down
22 changes: 11 additions & 11 deletions Source/DafnyCore/DafnyConsolePrinter.cs
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ public class DafnyConsolePrinter : ConsolePrinter {
}
}

private readonly static ConditionalWeakTable<DafnyOptions, ConcurrentDictionary<Uri, List<string>>> fsCaches = new();
private static readonly ConditionalWeakTable<DafnyOptions, ConcurrentDictionary<Uri, List<string>>> fsCaches = new();

private DafnyOptions options;

Expand All @@ -29,28 +29,28 @@ public record VCResultLogEntry(
int VCNum,
DateTime StartTime,
TimeSpan RunTime,
ProverInterface.Outcome Outcome,
SolverOutcome Outcome,
List<(Boogie.IToken Tok, string Description)> Asserts,
IEnumerable<TrackedNodeComponent> CoveredElements,
int ResourceCount);
public record VerificationResultLogEntry(
ConditionGeneration.Outcome Outcome,
VcOutcome Outcome,
TimeSpan RunTime,
int ResourceCount,
List<VCResultLogEntry> VCResults,
List<Counterexample> Counterexamples);
public record ConsoleLogEntry(ImplementationLogEntry Implementation, VerificationResultLogEntry Result);

public static VerificationResultLogEntry DistillVerificationResult(VerificationResult verificationResult) {
public static VerificationResultLogEntry DistillVerificationResult(ImplementationRunResult verificationResult) {
return new VerificationResultLogEntry(
verificationResult.Outcome, verificationResult.End - verificationResult.Start,
verificationResult.ResourceCount, verificationResult.VCResults.Select(DistillVCResult).ToList(), verificationResult.Errors);
verificationResult.VcOutcome, verificationResult.End - verificationResult.Start,
verificationResult.ResourceCount, verificationResult.RunResults.Select(DistillVCResult).ToList(), verificationResult.Errors);
}

private static VCResultLogEntry DistillVCResult(VCResult r) {
return new VCResultLogEntry(r.vcNum, r.startTime, r.runTime, r.outcome,
r.asserts.Select(a => (a.tok, a.Description.SuccessDescription)).ToList(), r.coveredElements,
r.resourceCount);
private static VCResultLogEntry DistillVCResult(VerificationRunResult r) {
return new VCResultLogEntry(r.VcNum, r.StartTime, r.RunTime, r.Outcome,
r.Asserts.Select(a => (a.tok, a.Description.SuccessDescription)).ToList(), r.CoveredElements,
r.ResourceCount);
}

public ConcurrentBag<ConsoleLogEntry> VerificationResults { get; } = new();
Expand Down Expand Up @@ -153,7 +153,7 @@ public override void ReportBplError(Boogie.IToken tok, string message, bool erro
}
}

public override void ReportEndVerifyImplementation(Implementation implementation, VerificationResult result) {
public override void ReportEndVerifyImplementation(Implementation implementation, ImplementationRunResult result) {
var impl = new ImplementationLogEntry(implementation.VerboseName, implementation.tok);
VerificationResults.Add(new ConsoleLogEntry(impl, DistillVerificationResult(result)));
}
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/DafnyCore.csproj
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,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.1" />
<PackageReference Include="Boogie.ExecutionEngine" Version="3.0.10" />
<PackageReference Include="Boogie.ExecutionEngine" Version="3.0.11" />
<PackageReference Include="Tomlyn" Version="0.16.2" />
</ItemGroup>

Expand Down
3 changes: 1 addition & 2 deletions Source/DafnyCore/Generic/BatchErrorReporter.cs
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,7 @@ public class BatchErrorReporter : ErrorReporter {

public void CopyDiagnostics(ErrorReporter intoReporter) {
foreach (var diagnostic in AllMessages) {
intoReporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token,
diagnostic.Message);
intoReporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token, diagnostic.Message);
}
}

Expand Down
1 change: 0 additions & 1 deletion Source/DafnyCore/Options/CommonOptionBag.cs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@
using System.IO;
using System.Linq;
using DafnyCore;
using Microsoft.Dafny.Compilers;

namespace Microsoft.Dafny;

Expand Down
99 changes: 47 additions & 52 deletions Source/DafnyCore/Pipeline/Compilation.cs
Original file line number Diff line number Diff line change
Expand Up @@ -50,10 +50,10 @@ public DafnyDiagnostic[] GetDiagnosticsForUri(Uri uri) =>
/// FilePosition is required because the default module lives in multiple files
/// </summary>
private readonly LazyConcurrentDictionary<ModuleDefinition,
Task<IReadOnlyDictionary<FilePosition, IReadOnlyList<IImplementationTask>>>> translatedModules = new();
Task<IReadOnlyDictionary<FilePosition, IReadOnlyList<IVerificationTask>>>> translatedModules = new();

private readonly ConcurrentDictionary<ICanVerify, Unit> verifyingOrVerifiedSymbols = new();
private readonly LazyConcurrentDictionary<ICanVerify, IReadOnlyList<IImplementationTask>> implementationsPerVerifiable = new();
private readonly LazyConcurrentDictionary<ICanVerify, IReadOnlyList<IVerificationTask>> tasksPerVerifiable = new();

private DafnyOptions Options => Input.Options;
public CompilationInput Input { get; }
Expand Down Expand Up @@ -237,12 +237,12 @@ private async Task<ResolutionResult> ResolveAsync() {
}
}

public static string GetImplementationName(Implementation implementation) {
var prefix = implementation.Name.Split(BoogieGenerator.NameSeparator)[0];
public static string GetTaskName(IVerificationTask task) {
var prefix = task.ScopeId + task.Split.SplitIndex;

// Refining declarations get the token of what they're refining, so to distinguish them we need to
// add the refining module name to the prefix.
if (implementation.tok is RefinementToken refinementToken) {
if (task.ScopeToken is RefinementToken refinementToken) {
prefix += "." + refinementToken.InheritingModule.Name;
}

Expand Down Expand Up @@ -276,10 +276,11 @@ public async Task<bool> VerifyLocation(FilePosition verifiableLocation, bool onl
return false;
}

return await VerifyCanVerify(canVerify, onlyPrepareVerificationForGutterTests);
return await VerifyCanVerify(canVerify, _ => true, onlyPrepareVerificationForGutterTests);
}

public async Task<bool> VerifyCanVerify(ICanVerify canVerify, bool onlyPrepareVerificationForGutterTests) {
public async Task<bool> VerifyCanVerify(ICanVerify canVerify, Func<IVerificationTask, bool> taskFilter,
bool onlyPrepareVerificationForGutterTests = false) {
var resolution = await Resolution;
var containingModule = canVerify.ContainingModule;
if (!containingModule.ShouldVerify(resolution.ResolvedProgram.Compilation)) {
Expand All @@ -293,22 +294,22 @@ public async Task<bool> VerifyCanVerify(ICanVerify canVerify, bool onlyPrepareVe
updates.OnNext(new ScheduledVerification(canVerify));

if (onlyPrepareVerificationForGutterTests) {
await VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution);
await VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution, taskFilter);
return true;
}

_ = VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution);
_ = VerifyUnverifiedSymbol(onlyPrepareVerificationForGutterTests, canVerify, resolution, taskFilter);
return true;
}

private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterTests, ICanVerify canVerify,
ResolutionResult resolution) {
ResolutionResult resolution, Func<IVerificationTask, bool> taskFilter) {
try {

var ticket = verificationTickets.Dequeue(CancellationToken.None);
var containingModule = canVerify.ContainingModule;

IReadOnlyDictionary<FilePosition, IReadOnlyList<IImplementationTask>> tasksForModule;
IReadOnlyDictionary<FilePosition, IReadOnlyList<IVerificationTask>> tasksForModule;
try {
tasksForModule = await translatedModules.GetOrAdd(containingModule, async () => {
var result = await verifier.GetVerificationTasksAsync(boogieEngine, resolution, containingModule,
Expand All @@ -317,9 +318,9 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
cancellationSource.Token.Register(task.Cancel);
}

return result.GroupBy(t => ((IToken)t.Implementation.tok).GetFilePosition()).ToDictionary(
return result.GroupBy(t => ((IToken)t.ScopeToken).GetFilePosition()).ToDictionary(
g => g.Key,
g => (IReadOnlyList<IImplementationTask>)g.ToList());
g => (IReadOnlyList<IVerificationTask>)g.ToList());
});
} catch (OperationCanceledException) {
throw;
Expand All @@ -328,26 +329,26 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
throw;
}

// For updated to be reliable, ImplementationsPerVerifiable must be Lazy
// For updated to be reliable, tasksPerVerifiable must be Lazy
var updated = false;
var tasks = implementationsPerVerifiable.GetOrAdd(canVerify, () => {
var tasks = tasksPerVerifiable.GetOrAdd(canVerify, () => {
var result =
tasksForModule.GetValueOrDefault(canVerify.NameToken.GetFilePosition()) ??
new List<IImplementationTask>(0);
new List<IVerificationTask>(0);

updated = true;
return result;
});
if (updated) {
updates.OnNext(new CanVerifyPartsIdentified(canVerify,
implementationsPerVerifiable[canVerify].ToList()));
tasksPerVerifiable[canVerify].ToList()));
}

// When multiple calls to VerifyUnverifiedSymbol are made, the order in which they pass this await matches the call order.
await ticket;

if (!onlyPrepareVerificationForGutterTests) {
foreach (var task in tasks) {
foreach (var task in tasks.Where(taskFilter)) {
VerifyTask(canVerify, task);
}
}
Expand All @@ -358,16 +359,10 @@ private async Task VerifyUnverifiedSymbol(bool onlyPrepareVerificationForGutterT
}
}

private void VerifyTask(ICanVerify canVerify, IImplementationTask task) {
private void VerifyTask(ICanVerify canVerify, IVerificationTask task) {
var statusUpdates = task.TryRun();
if (statusUpdates == null) {
if (task.CacheStatus is Completed completedCache) {
foreach (var result in completedCache.Result.VCResults) {
#pragma warning disable CS8625 // Cannot convert null literal to non-nullable reference type.
HandleStatusUpdate(canVerify, task, new BatchCompleted(null /* unused */, result));
#pragma warning restore CS8625 // Cannot convert null literal to non-nullable reference type.
}

HandleStatusUpdate(canVerify, task, completedCache);
}

Expand Down Expand Up @@ -399,21 +394,21 @@ public async Task Cancel(FilePosition filePosition) {
var resolution = await Resolution;
var canVerify = resolution.ResolvedProgram.FindNode<ICanVerify>(filePosition.Uri, filePosition.Position.ToDafnyPosition());
if (canVerify != null) {
var implementations = implementationsPerVerifiable.TryGetValue(canVerify, out var implementationsPerName)
? implementationsPerName! : Enumerable.Empty<IImplementationTask>();
var implementations = tasksPerVerifiable.TryGetValue(canVerify, out var implementationsPerName)
? implementationsPerName! : Enumerable.Empty<IVerificationTask>();
foreach (var view in implementations) {
view.Cancel();
}
verifyingOrVerifiedSymbols.TryRemove(canVerify, out _);
}
}

private void HandleStatusUpdate(ICanVerify canVerify, IImplementationTask implementationTask, IVerificationStatus boogieStatus) {
var tokenString = BoogieGenerator.ToDafnyToken(true, implementationTask.Implementation.tok).TokenToString(Options);
private void HandleStatusUpdate(ICanVerify canVerify, IVerificationTask verificationTask, IVerificationStatus boogieStatus) {
var tokenString = BoogieGenerator.ToDafnyToken(true, verificationTask.Split.Token).TokenToString(Options);
logger.LogDebug($"Received Boogie status {boogieStatus} for {tokenString}, version {Input.Version}");

updates.OnNext(new BoogieUpdate(transformedProgram!.ProofDependencyManager, canVerify,
implementationTask,
verificationTask,
boogieStatus));
}

Expand Down Expand Up @@ -461,7 +456,7 @@ public void Dispose() {
CancelPendingUpdates();
}

public static List<DafnyDiagnostic> GetDiagnosticsFromResult(DafnyOptions options, Uri uri, IImplementationTask task, VCResult result) {
public static List<DafnyDiagnostic> GetDiagnosticsFromResult(DafnyOptions options, Uri uri, IVerificationTask task, VerificationRunResult result) {
var errorReporter = new ObservableErrorReporter(options, uri);
List<DafnyDiagnostic> diagnostics = new();
errorReporter.Updates.Subscribe(d => diagnostics.Add(d.Diagnostic));
Expand All @@ -471,11 +466,11 @@ public static List<DafnyDiagnostic> GetDiagnosticsFromResult(DafnyOptions option
return diagnostics.OrderBy(d => d.Token.GetLspPosition()).ToList();
}

public static void ReportDiagnosticsInResult(DafnyOptions options, IImplementationTask task, VCResult result,
public static void ReportDiagnosticsInResult(DafnyOptions options, IVerificationTask task, VerificationRunResult result,
ErrorReporter errorReporter) {
var outcome = GetOutcome(result.outcome);
result.counterExamples.Sort(new CounterexampleComparer());
foreach (var counterExample in result.counterExamples) //.OrderBy(d => d.GetLocation()))
var outcome = GetOutcome(result.Outcome);
result.CounterExamples.Sort(new CounterexampleComparer());
foreach (var counterExample in result.CounterExamples) //.OrderBy(d => d.GetLocation()))
{
errorReporter.ReportBoogieError(counterExample.CreateErrorInformation(outcome, options.ForceBplErrors));
}
Expand All @@ -484,28 +479,28 @@ public static void ReportDiagnosticsInResult(DafnyOptions options, IImplementati
// The Boogie API forces us to create a temporary engine here to report the outcome, even though it only uses the options.
var boogieEngine = new ExecutionEngine(options, new VerificationResultCache(),
CustomStackSizePoolTaskScheduler.Create(0, 0));
var implementation = task.Implementation;
var implementation = task.Split.Implementation;
boogieEngine.ReportOutcome(null, outcome, outcomeError => errorReporter.ReportBoogieError(outcomeError, false),
implementation.VerboseName, implementation.tok, null, TextWriter.Null,
implementation.GetTimeLimit(options), result.counterExamples);
implementation.GetTimeLimit(options), result.CounterExamples);
}

private static ConditionGeneration.Outcome GetOutcome(ProverInterface.Outcome outcome) {
public static VcOutcome GetOutcome(SolverOutcome outcome) {
switch (outcome) {
case ProverInterface.Outcome.Valid:
return ConditionGeneration.Outcome.Correct;
case ProverInterface.Outcome.Invalid:
return ConditionGeneration.Outcome.Errors;
case ProverInterface.Outcome.TimeOut:
return ConditionGeneration.Outcome.TimedOut;
case ProverInterface.Outcome.OutOfMemory:
return ConditionGeneration.Outcome.OutOfMemory;
case ProverInterface.Outcome.OutOfResource:
return ConditionGeneration.Outcome.OutOfResource;
case ProverInterface.Outcome.Undetermined:
return ConditionGeneration.Outcome.Inconclusive;
case ProverInterface.Outcome.Bounded:
return ConditionGeneration.Outcome.ReachedBound;
case SolverOutcome.Valid:
return VcOutcome.Correct;
case SolverOutcome.Invalid:
return VcOutcome.Errors;
case SolverOutcome.TimeOut:
return VcOutcome.TimedOut;
case SolverOutcome.OutOfMemory:
return VcOutcome.OutOfMemory;
case SolverOutcome.OutOfResource:
return VcOutcome.OutOfResource;
case SolverOutcome.Undetermined:
return VcOutcome.Inconclusive;
case SolverOutcome.Bounded:
return VcOutcome.ReachedBound;
default:
throw new ArgumentOutOfRangeException(nameof(outcome), outcome, null);
}
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Pipeline/Events/BoogieException.cs
Original file line number Diff line number Diff line change
Expand Up @@ -4,4 +4,4 @@

namespace Microsoft.Dafny;

public record BoogieException(ICanVerify CanVerify, IImplementationTask Task, Exception Exception) : ICompilationEvent;
public record BoogieException(ICanVerify CanVerify, IVerificationTask Task, Exception Exception) : ICompilationEvent;
2 changes: 1 addition & 1 deletion Source/DafnyCore/Pipeline/Events/BoogieUpdate.cs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
namespace Microsoft.Dafny;

public record BoogieUpdate(ProofDependencyManager ProofDependencyManager,
ICanVerify CanVerify, IImplementationTask ImplementationTask, IVerificationStatus BoogieStatus)
ICanVerify CanVerify, IVerificationTask VerificationTask, IVerificationStatus BoogieStatus)
: ICompilationEvent {

}
Original file line number Diff line number Diff line change
Expand Up @@ -3,5 +3,5 @@

namespace Microsoft.Dafny;

public record CanVerifyPartsIdentified(ICanVerify CanVerify, IReadOnlyList<IImplementationTask> Parts) : ICompilationEvent {
public record CanVerifyPartsIdentified(ICanVerify CanVerify, IReadOnlyList<IVerificationTask> Parts) : ICompilationEvent {
}
6 changes: 3 additions & 3 deletions Source/DafnyCore/Pipeline/IProgramVerifier.cs
Original file line number Diff line number Diff line change
Expand Up @@ -6,15 +6,15 @@
using VC;

namespace Microsoft.Dafny {
public record AssertionBatchResult(Implementation Implementation, VCResult Result);
public record AssertionBatchResult(Implementation Implementation, VerificationRunResult Result);

public record ProgramVerificationTasks(IReadOnlyList<IImplementationTask> Tasks);
public record ProgramVerificationTasks(IReadOnlyList<IVerificationTask> Tasks);

/// <summary>
/// Implementations of this interface are responsible to verify the correctness of a program.
/// </summary>
public interface IProgramVerifier {
Task<IReadOnlyList<IImplementationTask>> GetVerificationTasksAsync(ExecutionEngine engine,
Task<IReadOnlyList<IVerificationTask>> GetVerificationTasksAsync(ExecutionEngine engine,
ResolutionResult resolution,
ModuleDefinition moduleDefinition,
CancellationToken cancellationToken);
Expand Down
Loading
Loading