search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.9k stars 261 forks source link

Crash in Boogie when using `disable-nonlinear-arithmetic` #4760

Open MikaelMayer opened 11 months ago

MikaelMayer commented 11 months ago

Dafny version

latest-nightly

Code to produce this issue

function PowerOfTwo(ntimes: nat): int {
  if ntimes == 0 then 1 else
  2*PowerOfTwo(ntimes - 1)
}

lemma CornerCase(ntimes: nat) 
  ensures // Putting as an assert solves the problem
    var r := PowerOfTwo(ntimes); // inlining solves the problem
    && 1 <= r // Replacing by true solves the problem
{
  assume false;
}

Command to run and resulting output

Paste in VSCode
Verify on the command line using "dafny verify"

What happened?

What type of operating system are you experiencing the problem on?

Windows

MikaelMayer commented 11 months ago

Refactoring the postcondition to a lemma solves the problem

MikaelMayer commented 11 months ago

Update: The discrepancy from the CLI and VSCode comes from a flag that I'm passing to the language server that I had forgotten about: --disable-nonlinear-arithmetic. So just by removing this flag, the code above passes in VSCode.

Now I can also reproduce the issue on the command line:

& "C:\Program Files\dotnet\dotnet.EXE" "...\.vscode\extensions\dafny-lang.ide-vscode-3.2.1\out\resources\nightly-2023-11-12-906db28\github\dafny\Dafny.dll" "verify" "--disable-nonlinear-arithmetic" "...\dafny\Source\IntegrationTests\TestFiles\LitTests\LitTest\libraries\src\Parsers\parserDebug.dfy"
Advisory: CornerCase (correctness) SKIPPED because of internal error: unexpected prover output: System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Boogie.TypeErasure.OpTypeEraserArguments.OriginalOpTypes(VCExprNAry node)
   at Microsoft.Boogie.TypeErasure.OpTypeEraserArguments.VisitBoogieFunctionOp(VCExprNAry node, VariableBindings bindings)
   at Microsoft.Boogie.VCExprAST.VCExprBoogieFunctionOp.Accept[Result,Arg](VCExprNAry expr, IVCExprOpVisitor`2 visitor, Arg arg)
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg](IVCExprOpVisitor`2 visitor, Arg arg)   at Microsoft.Boogie.TypeErasure.TypeEraser.Visit(VCExprNAry node, VariableBindings bindings)    
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg](IVCExprVisitor`2 visitor, Arg arg)  
   at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1.MutateList(List`1 exprs, Arg arg)
   at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1.MutateTriggers(List`1 triggers, Arg arg)  
   at Microsoft.Boogie.TypeErasure.TypeEraserArguments.HandleQuantifier(VCExprQuantifier node, List`1 newBoundVars, VariableBindings bindings)
   at Microsoft.Boogie.TypeErasure.TypeEraserArguments.Visit(VCExprQuantifier node, VariableBindings oldBindings)
   at Microsoft.Boogie.VCExprAST.VCExprQuantifier.Accept[Result,Arg](IVCExprVisitor`2 visitor, Arg 
arg)
   at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1.Visit(VCExprNAry node, Arg arg)
   at Microsoft.Boogie.TypeErasure.TypeEraser.Visit(VCExprNAry node, VariableBindings bindings)    
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg](IVCExprVisitor`2 visitor, Arg arg)  
   at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1.Mutate(VCExpr expr, Arg arg)
   at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitImpliesOp(VCExprNAry node, VariableBindings bindings)
   at Microsoft.Boogie.VCExprAST.VCExprOp.Accept[Result,Arg](VCExprNAry expr, IVCExprOpVisitor`2 visitor, Arg arg)
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg](IVCExprOpVisitor`2 visitor, Arg arg)   at Microsoft.Boogie.TypeErasure.TypeEraser.Visit(VCExprNAry node, VariableBindings bindings)    
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg](IVCExprVisitor`2 visitor, Arg arg)  
   at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1.Mutate(VCExpr expr, Arg arg)
   at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitImpliesOp(VCExprNAry node, VariableBindings bindings)
   at Microsoft.Boogie.VCExprAST.VCExprOp.Accept[Result,Arg](VCExprNAry expr, IVCExprOpVisitor`2 visitor, Arg arg)
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg](IVCExprOpVisitor`2 visitor, Arg arg)   at Microsoft.Boogie.TypeErasure.TypeEraser.Visit(VCExprNAry node, VariableBindings bindings)    
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg](IVCExprVisitor`2 visitor, Arg arg)  
   at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1.Mutate(VCExpr expr, Arg arg)
   at Microsoft.Boogie.TypeErasure.TypeEraser.Visit(VCExprLet node, VariableBindings bindings)     
   at Microsoft.Boogie.VCExprAST.VCExprLet.Accept[Result,Arg](IVCExprVisitor`2 visitor, Arg arg)   
   at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1.Mutate(VCExpr expr, Arg arg)
   at Microsoft.Boogie.TypeErasure.OpTypeEraser.VisitImpliesOp(VCExprNAry node, VariableBindings bindings)
   at Microsoft.Boogie.VCExprAST.VCExprOp.Accept[Result,Arg](VCExprNAry expr, IVCExprOpVisitor`2 visitor, Arg arg)
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg](IVCExprOpVisitor`2 visitor, Arg arg)   at Microsoft.Boogie.TypeErasure.TypeEraser.Visit(VCExprNAry node, VariableBindings bindings)    
   at Microsoft.Boogie.VCExprAST.VCExprNAry.Accept[Result,Arg](IVCExprVisitor`2 visitor, Arg arg)  
   at Microsoft.Boogie.VCExprAST.MutatingVCExprVisitor`1.Mutate(VCExpr expr, Arg arg)
   at Microsoft.Boogie.TypeErasure.TypeEraser.Erase(VCExpr expr, Int32 polarity)
   at Microsoft.Boogie.SMTLib.SMTLibProcessTheoremProver.VCExpr2String(VCExpr expr, Int32 polarity)   at Microsoft.Boogie.SMTLib.SMTLibInteractiveTheoremProver.Check(String descriptiveName, VCExpr vc, ErrorHandler handler, Int32 errorLimit, CancellationToken cancellationToken)
   at Microsoft.Boogie.Checker.Check(String descriptiveName, VCExpr vc, CancellationToken cancellationToken)
Unhandled exception: System.ArgumentNullException: Value cannot be null. (Parameter 'source')
   at System.Linq.ThrowHelper.ThrowArgumentNullException(ExceptionArgument argument)
   at System.Linq.Enumerable.Select[TSource,TResult](IEnumerable`1 source, Func`2 selector)        
   at Microsoft.Dafny.DafnyConsolePrinter.DistillVerificationResult(VerificationResult verificationResult)
   at Microsoft.Dafny.DafnyConsolePrinter.ReportEndVerifyImplementation(Implementation implementation, VerificationResult result)
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass48_0.<VerifyImplementation>b__0(IVerificationStatus status)
   at System.Reactive.Linq.ObservableImpl.Do`1.OnNext._.OnNext(TSource value) in /_/Rx.NET/Source/src/System.Reactive/Linq/Observable/Do.cs:line 38
--- End of stack trace from previous location ---
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass41_0.<<VerifyEachImplementation>b__1>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Boogie.ExecutionEngine.<>c__DisplayClass41_0.<<VerifyEachImplementation>b__1>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Boogie.ExecutionEngine.VerifyEachImplementation(TextWriter output, ProcessedProgram processedProgram, PipelineStatistics stats, String programId, ErrorReporterDelegate er, String requestId, Implementation[] stablePrioritizedImpls)
   at Microsoft.Boogie.ExecutionEngine.InferAndVerify(TextWriter output, Program program, PipelineStatistics stats, String programId, ErrorReporterDelegate er, String requestId)
   at Microsoft.Dafny.DafnyMain.BoogiePipelineWithRerun(DafnyOptions options, TextWriter output, ExecutionEngine engine, Program program, String bplFileName, String programId)
   at Microsoft.Dafny.DafnyMain.BoogieOnce(DafnyOptions options, TextWriter output, ExecutionEngine engine, String baseFile, String moduleName, Program boogieProgram, String programId)
   at Microsoft.Dafny.CompilerDriver.BoogieOnceWithTimerAsync(TextWriter output, DafnyOptions options, String baseName, String programId, String moduleName, Program program)
   at Microsoft.Dafny.CompilerDriver.<>c__DisplayClass8_0.<<BoogieAsync>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.CompilerDriver.<>c__DisplayClass8_0.<<BoogieAsync>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.CompilerDriver.BoogieAsync(DafnyOptions options, String baseName, IEnumerable`1 boogiePrograms, String programId)
   at Microsoft.Dafny.CompilerDriver.ProcessFilesAsync(IReadOnlyList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, DafnyOptions options, ProofDependencyManager depManager, Boolean lookForSnapshots, String programId)
   at Microsoft.Dafny.CompilerDriver.RunCompiler(DafnyOptions options)
   at Microsoft.Dafny.DafnyCli.<>c__DisplayClass10_0.<<SetHandlerUsingDafnyOptionsContinuation>g__Handle|0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Invocation.AnonymousCommandHandler.InvokeAsync(InvocationContext context) 
   at System.CommandLine.Invocation.InvocationPipeline.<>c__DisplayClass4_0.<<BuildInvocationChain>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass17_0.<<UseParseErrorReporting>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass12_0.<<UseHelp>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.DafnyCli.<>c__DisplayClass21_0.<<AddDeveloperHelp>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass22_0.<<UseVersionOption>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass19_0.<<UseTypoCorrections>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<UseSuggestDirective>b__18_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass16_0.<<UseParseDirective>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<RegisterWithDotnetSuggest>b__5_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass8_0.<<UseExceptionHandler>b__0>d.MoveNext()
MikaelMayer commented 11 months ago

First investigations show that it's cause by Boogie interpreting "1 <= r" as a trigger because "<=" is now uninterpreted. And since the variable r is local, it can't find a definition while trying to translate triggers to Z3

MikaelMayer commented 11 months ago

The first fault in the code is in Boogie apparently:

https://github.com/boogie-org/boogie/blob/aa56ffbd2b0302c1883077bc59e573c285c43d3d/Source/Core/AST/AbsyQuant.cs#L963-L974

      public override Expr VisitNAryExpr(NAryExpr node)
      {
        //Contract.Requires(node != null);
        Contract.Ensures(Contract.Result<Expr>() != null);
        FunctionCall fn = node.Fun as FunctionCall;
        if (fn != null && cce.NonNull(fn.Func).NeverTrigger)
        {
          parent.Triggers = new Trigger(fn.Func.tok, false, new List<Expr> {node}, parent.Triggers);
        }

        return base.VisitNAryExpr(node);
      }

The line:

parent.Triggers = new Trigger(fn.Func.tok, false, new List<Expr> {node}, parent.Triggers);

get executed with parent == forall $ih#ntimes0#0 :: ....

but the node itself is 1 <= r#h which is a local variable and apparently a "NeverTrigger" that still gets collected.

MikaelMayer commented 11 months ago

Note that even without --disable-nonlinear-arithmetic in vSCode, I still have a similar problem in my original code.

RustanLeino commented 11 months ago

Nice sleuthing!

The crash you're seeing is a bug in Boogie. Here is a smaller repro:

function {:never_pattern true} P(x: int): bool;

procedure Test() {
  assert (forall xyz: int ::
    (var r := xyz; P(r)));  
}

which for me produces:

d.bpl(50,21): Error: invalid type for argument 0 in application of P: bool (expected: int)
d.bpl(50,21): Error: internal error, shallow-type assignment was done incorrectly, r:bool != int
Process terminated. Assertion failed.
   at Microsoft.Boogie.IdentifierExpr.Typecheck(TypecheckingContext tc) in BOOGIE/Source/Core/AST/AbsyExpr.cs:line 1343
   at Microsoft.Boogie.NAryExpr.Typecheck(TypecheckingContext tc) in BOOGIE/Source/Core/AST/AbsyExpr.cs:line 3328
   at Microsoft.Boogie.LetExpr.Typecheck(TypecheckingContext tc) in BOOGIE/Source/Core/AST/AbsyQuant.cs:line 1313
   at Microsoft.Boogie.QuantifierExpr.Typecheck(TypecheckingContext tc) in BOOGIE/Source/Core/AST/AbsyQuant.cs:line 1077
   at Microsoft.Boogie.AssertCmd.Typecheck(TypecheckingContext tc) in BOOGIE/Source/Core/AST/AbsyCmd.cs:line 4368
   at Microsoft.Boogie.Block.Typecheck(TypecheckingContext tc) in BOOGIE/Source/Core/AST/AbsyCmd.cs:line 1381
   at Microsoft.Boogie.Implementation.Typecheck(TypecheckingContext tc) in BOOGIE/Source/Core/AST/Absy.cs:line 4068
   at Microsoft.Boogie.Program.Typecheck(TypecheckingContext tc) in BOOGIE/Source/Core/AST/Program.cs:line 152
   at Microsoft.Boogie.Program.Typecheck(CoreOptions options, IErrorSink errorSink) in BOOGIE/Source/Core/AST/Program.cs:line 140
   at Microsoft.Boogie.Program.Typecheck(CoreOptions options) in BOOGIE/Source/Core/AST/Program.cs:line 134
   at Microsoft.Boogie.ExecutionEngine.ResolveAndTypecheck(Program program, String bplFileName, CivlTypeChecker& civlTypeChecker) in BOOGIE/Source/ExecutionEngine/ExecutionEngine.cs:line 402
   at Microsoft.Boogie.ExecutionEngine.ProcessProgram(TextWriter output, Program program, String bplFileName, String programId) in BOOGIE/Source/ExecutionEngine/ExecutionEngine.cs:line 143
   at System.Runtime.CompilerServices.AsyncMethodBuilderCore.Start[TStateMachine](TStateMachine& stateMachine)
   at Microsoft.Boogie.ExecutionEngine.ProcessProgram(TextWriter output, Program program, String bplFileName, String programId)
   at Microsoft.Boogie.ExecutionEngine.ProcessFiles(TextWriter output, IList`1 fileNames, Boolean lookForSnapshots, String programId) in BOOGIE/Source/ExecutionEngine/ExecutionEngine.cs:line 123
   at System.Runtime.CompilerServices.AsyncMethodBuilderCore.Start[TStateMachine](TStateMachine& stateMachine)
   at Microsoft.Boogie.ExecutionEngine.ProcessFiles(TextWriter output, IList`1 fileNames, Boolean lookForSnapshots, String programId)
   at Microsoft.Boogie.OnlyBoogie.Main(String[] args) in BOOGIE/Source/BoogieDriver/BoogieDriver.cs:line 66

Here's an explanation:

The :never_pattern attribute in Boogie on a function P causes Boogie to attach the SMT

:no-pattern (P e)

to any quantifier that (doesn't already have an explicit trigger in Boogie and) contains an expression P(e) in its body. I suppose it does that by visiting every AST node in the quantifier's body, and if it encounters a function call to P, then it remembers the function arguments (e in my example) and then blurts out the SMT :no-pattern (P e).

Evidently, this visitation does not handle let expressions correctly. When the visitor encounters the expression P(r) in the example, it outputs :no-pattern (P r), even though r is not bound to anything at the outer scope of the quantifier body. This certainly generates a meaningless :no-pattern annotation. But before that, it also generates two type errors (see exception trace above). I imagine (but did not inspect the Boogie source code) that these type errors come about because the visitor adds Boogie :nopats attributes, which are later type checked and translated into SMT :no-pattern annotations. The type checking of those :nopats attributes is probably what generates the errors and subsequently causes a crash.

While the crash you're seeing is a Boogie bug, the example also reveals two other issues in Dafny: