diff options
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 5 | ||||
| -rw-r--r-- | Source/DafnyExtension/MenuProxy.cs | 17 | ||||
| -rw-r--r-- | Source/DafnyExtension/ProgressMargin.cs | 46 | ||||
| -rw-r--r-- | Source/DafnyMenu/DafnyMenu.vsct | 11 | ||||
| -rw-r--r-- | Source/DafnyMenu/DafnyMenuPackage.cs | 32 | ||||
| -rw-r--r-- | Source/DafnyMenu/PkgCmdID.cs | 1 |
6 files changed, 100 insertions, 12 deletions
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index 5b8cc943..7f39fe34 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -239,6 +239,11 @@ namespace DafnyLanguage return Dafny.DafnyOptions.Clo.VerifySnapshots;
}
+ public static void SetDiagnoseTimeouts(bool v)
+ {
+ Dafny.DafnyOptions.Clo.RunDiagnosticsOnTimeout = v;
+ }
+
public static int ChangeIncrementalVerification(int mode)
{
var old = Dafny.DafnyOptions.Clo.VerifySnapshots;
diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs index 11e1287f..9ddc8344 100644 --- a/Source/DafnyExtension/MenuProxy.cs +++ b/Source/DafnyExtension/MenuProxy.cs @@ -67,6 +67,15 @@ namespace DafnyLanguage }
}
+ public void DiagnoseTimeouts(IWpfTextView activeTextView)
+ {
+ DafnyLanguage.ProgressTagger tagger;
+ if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))
+ {
+ tagger.StartVerification(false, true);
+ }
+ }
+
public bool MenuEnabled(IWpfTextView activeTextView)
{
return activeTextView != null && activeTextView.TextBuffer.ContentType.DisplayName == "dafny";
@@ -80,6 +89,14 @@ namespace DafnyLanguage && resolver.Program != null;
}
+ public bool DiagnoseTimeoutsCommandEnabled(IWpfTextView activeTextView)
+ {
+ ResolverTagger resolver;
+ return activeTextView != null
+ && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+ && resolver.VerificationErrors.Any(err => err.Message.Contains("timed out"));
+ }
+
public void Compile(IWpfTextView activeTextView)
{
ResolverTagger resolver;
diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs index b4e58d3d..c3f56259 100644 --- a/Source/DafnyExtension/ProgressMargin.cs +++ b/Source/DafnyExtension/ProgressMargin.cs @@ -197,6 +197,7 @@ namespace DafnyLanguage bool verificationInProgress; // this field is protected by "this". Invariant: !verificationInProgress ==> bufferChangesPreVerificationStart.Count == 0
System.Threading.Tasks.Task verificationTask;
public bool VerificationDisabled { get; private set; }
+ bool isDiagnosingTimeouts;
string lastRequestId;
public static readonly IDictionary<ITextBuffer, ProgressTagger> ProgressTaggers = new ConcurrentDictionary<ITextBuffer, ProgressTagger>();
@@ -227,14 +228,21 @@ namespace DafnyLanguage if (prog == null || VerificationDisabled) return;
// We have a successfully resolved program to verify
- var resolvedVersion = snap.Version.VersionNumber;
- if (bufferChangesPostVerificationStart.Count == 0) {
- // Nothing new to verify. No reason to start a new verification.
- return;
- } else if (!bufferChangesPostVerificationStart.TrueForAll(span => span.Snapshot.Version.VersionNumber <= resolvedVersion)) {
- // There have been buffer changes since the program that was resolved. Do nothing here,
- // and instead just await the next resolved program.
- return;
+ var dt = isDiagnosingTimeouts;
+ if (!dt)
+ {
+ var resolvedVersion = snap.Version.VersionNumber;
+ if (bufferChangesPostVerificationStart.Count == 0)
+ {
+ // Nothing new to verify. No reason to start a new verification.
+ return;
+ }
+ else if (!bufferChangesPostVerificationStart.TrueForAll(span => span.Snapshot.Version.VersionNumber <= resolvedVersion))
+ {
+ // There have been buffer changes since the program that was resolved. Do nothing here,
+ // and instead just await the next resolved program.
+ return;
+ }
}
// at this time, we're committed to running the verifier
@@ -254,10 +262,14 @@ namespace DafnyLanguage }
verificationTask = System.Threading.Tasks.Task.Factory.StartNew(
- () => RunVerifier(prog, snap, lastRequestId, resolver),
+ () => RunVerifier(prog, snap, lastRequestId, resolver, dt),
TaskCreationOptions.LongRunning);
verificationInProgress = true;
+ if (dt)
+ {
+ isDiagnosingTimeouts = false;
+ }
// Change orange progress markers into yellow ones
Contract.Assert(bufferChangesPreVerificationStart.Count == 0); // follows from monitor invariant
@@ -293,7 +305,7 @@ namespace DafnyLanguage }
}
- public void StartVerification()
+ public void StartVerification(bool clearCache = true, bool diagnoseTimeouts = false)
{
lock (this)
{
@@ -301,7 +313,11 @@ namespace DafnyLanguage bufferChangesPostVerificationStart.Clear();
bufferChangesPostVerificationStart.Add(new SnapshotSpan(_buffer.CurrentSnapshot, 0, _buffer.CurrentSnapshot.Length));
VerificationDisabled = false;
- ClearCachedVerificationResults();
+ isDiagnosingTimeouts = diagnoseTimeouts;
+ if (clearCache)
+ {
+ ClearCachedVerificationResults();
+ }
NotifyAboutChangedTags(_buffer.CurrentSnapshot);
}
}
@@ -314,7 +330,7 @@ namespace DafnyLanguage }
}
- void RunVerifier(Dafny.Program program, ITextSnapshot snapshot, string requestId, ResolverTagger errorListHolder) {
+ void RunVerifier(Dafny.Program program, ITextSnapshot snapshot, string requestId, ResolverTagger errorListHolder, bool diagnoseTimeouts) {
Contract.Requires(program != null);
Contract.Requires(snapshot != null);
Contract.Requires(requestId != null);
@@ -332,6 +348,8 @@ namespace DafnyLanguage _version++;
}
+ DafnyDriver.SetDiagnoseTimeouts(diagnoseTimeouts);
+
try
{
bool success = DafnyDriver.Verify(program, errorListHolder, GetHashCode().ToString(), requestId, errorInfo =>
@@ -369,6 +387,10 @@ namespace DafnyLanguage {
errorListHolder.AddError(new DafnyError("$$program$$", 0, 0, ErrorCategory.InternalError, "Verification process error: " + e.Message, snapshot, false), "$$program$$", requestId);
}
+ finally
+ {
+ DafnyDriver.SetDiagnoseTimeouts(!diagnoseTimeouts);
+ }
lock (this) {
bufferChangesPreVerificationStart.Clear();
diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct index 4c4b1403..4c9a4913 100644 --- a/Source/DafnyMenu/DafnyMenu.vsct +++ b/Source/DafnyMenu/DafnyMenu.vsct @@ -122,6 +122,16 @@ </Strings>
</Button>
+ <Button guid="guidDafnyMenuCmdSet" id="cmdidDiagnoseTimeouts" priority="0x0106" type="Button">
+ <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
+ <CommandFlag>DynamicVisibility</CommandFlag>
+ <CommandFlag>DefaultInvisible</CommandFlag>
+ <CommandFlag>TextChanges</CommandFlag>
+ <Strings>
+ <ButtonText>Re-verify to diagnose timeouts</ButtonText>
+ </Strings>
+ </Button>
+
</Buttons>
<!--The bitmaps section is used to define the bitmaps that are used for the commands.-->
@@ -154,6 +164,7 @@ <IDSymbol name="cmdidToggleSnapshotVerification" value="0x0103" />
<IDSymbol name="cmdidToggleBVD" value="0x0104" />
<IDSymbol name="cmdidToggleMoreAdvancedSnapshotVerification" value="0x0105" />
+ <IDSymbol name="cmdidDiagnoseTimeouts" value="0x0106" />
</GuidSymbol>
<!--
diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs index 0acf3554..58c8f0ab 100644 --- a/Source/DafnyMenu/DafnyMenuPackage.cs +++ b/Source/DafnyMenu/DafnyMenuPackage.cs @@ -53,6 +53,12 @@ namespace DafnyLanguage.DafnyMenu void ShowErrorModel(IWpfTextView activeTextView);
+
+
+ bool DiagnoseTimeoutsCommandEnabled(IWpfTextView activeTextView);
+
+
+ void DiagnoseTimeouts(IWpfTextView activeTextView);
}
@@ -88,6 +94,7 @@ namespace DafnyLanguage.DafnyMenu private OleMenuCommand toggleSnapshotVerificationCommand;
private OleMenuCommand toggleMoreAdvancedSnapshotVerificationCommand;
private OleMenuCommand toggleBVDCommand;
+ private OleMenuCommand diagnoseTimeoutsCommand;
bool BVDDisabled;
@@ -157,6 +164,12 @@ namespace DafnyLanguage.DafnyMenu toggleBVDCommand.BeforeQueryStatus += showErrorModelCommand_BeforeQueryStatus;
mcs.AddCommand(toggleBVDCommand);
+ var diagnoseTimeoutsCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidDiagnoseTimeouts);
+ diagnoseTimeoutsCommand = new OleMenuCommand(DiagnoseTimeoutsCallback, diagnoseTimeoutsCommandID);
+ diagnoseTimeoutsCommand.Enabled = true;
+ diagnoseTimeoutsCommand.BeforeQueryStatus += diagnoseTimeoutsCommand_BeforeQueryStatus;
+ mcs.AddCommand(diagnoseTimeoutsCommand);
+
var menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu);
menuCommand = new OleMenuCommand(new EventHandler((sender, e) => { }), menuCommandID);
menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus;
@@ -301,6 +314,16 @@ namespace DafnyLanguage.DafnyMenu }
}
+ void diagnoseTimeoutsCommand_BeforeQueryStatus(object sender, EventArgs e)
+ {
+ var atv = ActiveTextView;
+ if (MenuProxy != null && atv != null)
+ {
+ var visible = MenuProxy.DiagnoseTimeoutsCommandEnabled(atv);
+ diagnoseTimeoutsCommand.Visible = visible;
+ }
+ }
+
private void toggleMoreAdvancedSnapshotVerificationCommand_BeforeQueryStatus(object sender, EventArgs e)
{
var atv = ActiveTextView;
@@ -317,6 +340,15 @@ namespace DafnyLanguage.DafnyMenu toggleBVDCommand.Text = (BVDDisabled ? "Enable" : "Disable") + " BVD";
}
+ void DiagnoseTimeoutsCallback(object sender, EventArgs e)
+ {
+ var atv = ActiveTextView;
+ if (MenuProxy != null && atv != null)
+ {
+ MenuProxy.DiagnoseTimeouts(atv);
+ }
+ }
+
public void ExecuteAsCompiling(Action action, TextWriter outputWriter)
{
IVsStatusbar statusBar = (IVsStatusbar)GetGlobalService(typeof(SVsStatusbar));
diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs index b6f30145..427dd888 100644 --- a/Source/DafnyMenu/PkgCmdID.cs +++ b/Source/DafnyMenu/PkgCmdID.cs @@ -13,5 +13,6 @@ namespace DafnyLanguage.DafnyMenu public static uint cmdidToggleSnapshotVerification = 0x103;
public const uint cmdidToggleBVD = 0x104;
public static uint cmdidToggleMoreAdvancedSnapshotVerification = 0x105;
+ public static uint cmdidDiagnoseTimeouts = 0x106;
};
}
\ No newline at end of file |