Don't silently swallow exceptions when verifying #488

atomb · 2022-01-21T23:37:51Z

(Edited to address my own comment below).

Re-throw exceptions that occur during the split and verify worker, rather than silently swallowing them. Avoids printing "valid" when exceptions occur during solver interaction.

Addresses #487.

When verifying an implementation, set the initial value of the outcome to `Uninitialized` (a new alternative) instead of `Correct` to avoid spurious verification success when exceptions occur during solver interaction.

atomb · 2022-01-22T00:05:12Z

An alternative (or additional?) approach could be to address what I think is perhaps a separate part of the problem:

boogie/Source/VCGeneration/SplitAndVerifyWorker.cs

Lines 97 to 109 in da30caa

    
           async Task DoWork(Split split) 
        
           { 
        
             var checker = await split.parent.CheckerPool.FindCheckerFor(split.parent, split); 
        
             try { 
        
               StartCheck(split, checker); 
        
               await split.ProverTask; 
        
               await ProcessResult(split); 
        
             } 
        
             catch { 
        
               split.ReleaseChecker(); 
        
             } 
        
           }

This releases the checker silently if any exception occurs during checking, without indicating that the proof obligation being checked has not yet been established.

atomb · 2022-01-22T00:47:39Z

I'm not sure this is ready to go yet, but I'm adding reviewers in the hope of identifying the correct solution.

This reverts commit c278ea9.

atomb · 2022-01-24T18:04:26Z

The current fix now seems pretty reasonable to me, and it's very small. It does cause two current tests to fail because the expected error gets caught in a different place, leading to different output.

Source/ExecutionEngine/ExecutionEngine.cs

Source/VCGeneration/SplitAndVerifyWorker.cs

keyboardDrummer · 2022-01-25T09:25:47Z

Source/ExecutionEngine/ExecutionEngine.cs

@@ -1244,6 +1244,13 @@ private static void CleanupCheckers(string requestId)
            verificationResult.Errors = null;
            verificationResult.Outcome = VCGen.Outcome.Inconclusive;
          }
+          catch(AggregateException e)


Can we catch something more specific? I wouldn't want to swallow any bugs here but catching a bad solver argument seems good.

There's nothing below AggregateException in the class hierarchy, AFAIK, though we could pull out the wrapped exceptions and behave differently depending on what they are. This code will always lead to a message and an inconclusive result, so I wouldn't expect it to hide bugs. It could be that, after some experience with it, we realize that it would be best to handle different exceptions differently, but at the moment I'm not sure what the different behavior would be.

At the moment, this does catch bad solver arguments and paths, but also things like a broken pipe if a solver crashes, or exceptions thrown by internal code that relates to solver interaction (like failing to parse a solver result).

Inspecting the internals of AggregateException and rethrowing if it doesn't contain something we want to handle, seems fine to me.

This code will always lead to a message and an inconclusive result, so I wouldn't expect it to hide bugs.

That's true but I do think it is nicer to handle IO and input errors differently than bugs. As a user I'd also appreciate bugs being identified as such so I know immediately that I'm not to blame.

That sounds good to me. I'll update it to look inside the AggregateException.

One possibility is to only handle IOException here. Solver configuration issues result in a ProverException which is then handled higher up, meaning the output expected by the current solver configuration error tests doesn't change.

The latest commit does just this, and I think I like the way it behaves now (as detailed in the response below).

keyboardDrummer · 2022-01-25T09:27:58Z

Source/ExecutionEngine/ExecutionEngine.cs

@@ -1244,6 +1244,13 @@ private static void CleanupCheckers(string requestId)
            verificationResult.Errors = null;
            verificationResult.Outcome = VCGen.Outcome.Inconclusive;
          }
+          catch(AggregateException e)


Can we catch something more specific? I wouldn't want to swallow any bugs here but catching a bad solver argument seems good.

keyboardDrummer · 2022-01-25T09:28:15Z

Source/ExecutionEngine/ExecutionEngine.cs

+            printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because: {1}",
+              impl.Name, e.Message);
+            verificationResult.Errors = null;
+            verificationResult.Outcome = VCGen.Outcome.Inconclusive;


Could we set the default of verificationResult.Outcome to Inconclusive? Right now the default is Outcome.Correct, which seems like asking for soundness issues.

keyboardDrummer · 2022-01-25T09:28:57Z

Source/ExecutionEngine/ExecutionEngine.cs

+            printer.AdvisoryWriteLine("Advisory: {0} SKIPPED because: {1}",
+              impl.Name, e.Message);
+            verificationResult.Errors = null;
+            verificationResult.Outcome = VCGen.Outcome.Inconclusive;


Inconclusive means that the solver ran but couldn't prove unsat or sat right? For the scenario of invalid solver arguments I wouldn't mind an additional enum value, like InvalidConfiguration.

keyboardDrummer · 2022-01-25T09:29:59Z

Source/VCGeneration/SplitAndVerifyWorker.cs

@@ -105,6 +105,7 @@ async Task DoWork(Split split)
      }
      catch {
        split.ReleaseChecker();
+        throw; // This can be better handled farther up the call stack.


Nitpick: I don't think the comment is necessary.

keyboardDrummer · 2022-01-26T09:55:27Z

Source/ExecutionEngine/ExecutionEngine.cs

@@ -1784,6 +1818,10 @@ private static ErrorInformation CreateErrorInformation(Counterexample error, VC.
      {
        cause = "Out of memory on";
      }
+      else if (outcome == VCGen.Outcome.SolverException)
+      {
+        cause = "Solver exception on";


From a user perspective, I think I like to know "is it my fault?" and "solver exception" seems a bit ambiguous is that regard. It sounds like it's the solver's fault, but this problem also occurs when you give incorrect solver arguments right?

That's right. It'll be hard to distinguish between an invalid solver and a crashing solver without digging into the text of the error message accompanying the exception, though. I think both will be instances of IOException. That text will be presented to the user, though, so they'll be able to tell the difference, even though it'll be toward the end of the message rather than the beginning.

With the most recent change, this is better behaved. An invalid solver path or option will lead to the old behavior: quitting immediately with a fatal error. A solver that starts up and then crashes will lead to the new behavior: a warning and a result of "solver exception", allowing the user to still get results for any proof obligation on which the solver succeeds.

Looks great, thanks :-)

This reverts commit 251353b.

Allow VCGen outcome to be uninitialized

c278ea9

When verifying an implementation, set the initial value of the outcome to `Uninitialized` (a new alternative) instead of `Correct` to avoid spurious verification success when exceptions occur during solver interaction.

atomb requested a review from keyboardDrummer January 22, 2022 00:47

atomb added 3 commits January 24, 2022 08:55

Revert "Allow VCGen outcome to be uninitialized"

4ca640d

This reverts commit c278ea9.

Simpler, more informative approach

8960166

Allow tests to pass after previous commit

6dce0d5

atomb changed the title ~~Allow VCGen outcome to be uninitialized~~ Don't silently swallow exceptions when verifying Jan 24, 2022

Update error messages issue 322 tests

251353b

atomb requested a review from rakamaric January 25, 2022 01:16

keyboardDrummer reviewed Jan 25, 2022

View reviewed changes

atomb added 2 commits January 25, 2022 11:24

Address @keyboardDrummer’s comment about comment

d4c6aa4

Introduce a SolverException outcome

8db3108

atomb requested a review from keyboardDrummer January 25, 2022 23:22

keyboardDrummer reviewed Jan 26, 2022

View reviewed changes

atomb added 2 commits January 26, 2022 09:49

Revert "Update error messages issue 322 tests"

e53da44

This reverts commit 251353b.

Handle only IOException in VerifyImplementation

8c20050

keyboardDrummer approved these changes Jan 27, 2022

View reviewed changes

keyboardDrummer merged commit 03ca412 into boogie-org:master Jan 27, 2022

atomb mentioned this pull request Feb 1, 2022

Exception in solver interaction leads to false report of validity #487

Closed

robin-aws mentioned this pull request Feb 4, 2022

Include Z3 resource counts in CSV logs dafny-lang/dafny#1766

Merged

atomb mentioned this pull request Feb 11, 2022

fix: Cancellation tokens to cancel and restart checkers #497

Merged

atomb deleted the no-assume-correct branch January 4, 2024 17:39

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Don't silently swallow exceptions when verifying #488

Don't silently swallow exceptions when verifying #488

atomb commented Jan 21, 2022 •

edited

Loading

atomb commented Jan 22, 2022 •

edited

Loading

atomb commented Jan 22, 2022

atomb commented Jan 24, 2022

keyboardDrummer Jan 25, 2022

atomb Jan 25, 2022

keyboardDrummer Jan 26, 2022 •

edited

Loading

atomb Jan 26, 2022

atomb Jan 26, 2022

atomb Jan 26, 2022

keyboardDrummer Jan 25, 2022

keyboardDrummer Jan 25, 2022

keyboardDrummer Jan 25, 2022

keyboardDrummer Jan 25, 2022

keyboardDrummer Jan 26, 2022

atomb Jan 26, 2022

atomb Jan 26, 2022 •

edited

Loading

keyboardDrummer Jan 27, 2022

Don't silently swallow exceptions when verifying #488

Don't silently swallow exceptions when verifying #488

Conversation

atomb commented Jan 21, 2022 • edited Loading

atomb commented Jan 22, 2022 • edited Loading

atomb commented Jan 22, 2022

atomb commented Jan 24, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jan 26, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb Jan 26, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb commented Jan 21, 2022 •

edited

Loading

atomb commented Jan 22, 2022 •

edited

Loading

keyboardDrummer Jan 26, 2022 •

edited

Loading

atomb Jan 26, 2022 •

edited

Loading