Skip to content

Commit

Permalink
Filter assertions (#5031)
Browse files Browse the repository at this point in the history
### Description
- Allow using `--filter-position` to only verify individual assertions.

The implementation relies on a new version of Boogie, which changes the
API so that Boogie returns not a list of implementations but instead of
a list of 'verification tasks', which map to individual SMT executions
or 'assertion batches'. When using `--isolate-assertions`, each
assertion is given such as task, and it becomes easy to filter these
tasks/assertions based on a file position.

#### Background of some of the code changes
This change in the Boogie API means Dafny is not longer updated when all
the tasks for a particular Boogie implementation are finished, which
effects a few things that rely on all tasks in a Boogie implementation
to be done:
 - Computation of redundant assertions
- Gutter icons (maybe it conceptually does not depend on Boogie
implementations, I'm not sure, but the current implementation cares
about Boogie implementations)

There is no change in behavior for the above, but the code had to be
updated so on the Dafny side we track whether everything for a
particular implementation is done.

### How has this been tested?
- Added new cases to the existing littish test `filter.dfy`
- Some gutter icons tests have been updated, which is I think due to an
improvement. The last batch completed + implementation completed steps
are now combined, so two updates that would always immediately follow
each other are now squashed together.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
keyboardDrummer authored Feb 8, 2024
1 parent 728433a commit 385103d
Show file tree
Hide file tree
Showing 55 changed files with 666 additions and 500 deletions.
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

0 comments on commit 385103d

Please sign in to comment.