From 0fcac3ac1a2f5d23111f14fa1b56b4fa33485b26 Mon Sep 17 00:00:00 2001 From: Remy Willems Date: Tue, 14 Jan 2025 20:44:51 +0100 Subject: [PATCH] Allow translating by blocks (#6050) ### What was changed? Allow translating by blocks ### How has this been tested? Updated CLI tests 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). --- .../SinglePassCodeGenerator.Statement.cs | 3 +++ .../TestFiles/LitTests/LitTest/comp/Arrays.dfy | 4 +++- .../LitTest/expectations/ExpectAndExceptions.dfy | 4 +++- .../expectations/ExpectAndExceptions.dfy.expect | 8 ++++---- .../expectations/ExpectAndExceptions.dfy.expect | 10 +++++----- docs/dev/news/6050.fix | 1 + 6 files changed, 19 insertions(+), 11 deletions(-) create mode 100644 docs/dev/news/6050.fix diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs index 92470ef44f2..dffe4000596 100644 --- a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs +++ b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs @@ -558,6 +558,9 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree case TryRecoverStatement h: EmitHaltRecoveryStmt(h.TryBody, IdName(h.HaltMessageVar), h.RecoverBody, wr); break; + case BlockByProofStmt blockByProofStmt: + TrStmt(blockByProofStmt.Body, wr, wStmts); + break; default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Arrays.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Arrays.dfy index cd1247526f6..cd35cc00ca0 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Arrays.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/Arrays.dfy @@ -492,7 +492,9 @@ module NativeArrays { var iIndex: int, bIndex: byte, bvIndex: bv9 := 3, 4, 5; m[iIndex, bIndex] := arr[iIndex]; arr[iIndex] := m[iIndex, bvIndex - 1]; - assert arr[iIndex] == 17; + assert arr[iIndex] == 17 by { + assert true; + } print arr[iIndex], " "; // 17 m[bIndex, iIndex] := arr[bIndex]; arr[bIndex] := m[bvIndex - 1, iIndex]; diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy index 8a356da3c22..ac1919accfa 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy @@ -8,7 +8,9 @@ include "../exceptions/NatOutcomeDt.dfy" include "../exceptions/GenericOutcomeDt.dfy" method TestAssignOrHalt() { - var stmt1: nat :- expect NatSuccess(42); + var stmt1: nat :- expect NatSuccess(42) by { + assert true; + } // Regression test for when assign-or-halt was also calling PropagateFailure, which led // to the error "type variable 'U' in the function call to 'PropagateFailure' could not be determined" // (because of the lack of type constraints). diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy.expect index 572284717d0..cb29b57833f 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/expectations/ExpectAndExceptions.dfy.expect @@ -1,12 +1,12 @@ Dafny program verifier finished with 2 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!") +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!") Dafny program verifier finished with 2 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!") +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!") Dafny program verifier finished with 2 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!") +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!") Dafny program verifier finished with 2 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure("Kaboom!") +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure("Kaboom!") diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/expectations/ExpectAndExceptions.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/expectations/ExpectAndExceptions.dfy.expect index 18fac6636f6..4ac29e24bf2 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/expectations/ExpectAndExceptions.dfy.expect +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/unicodecharsFalse/expectations/ExpectAndExceptions.dfy.expect @@ -1,15 +1,15 @@ Dafny program verifier finished with 0 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!) +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!) Dafny program verifier finished with 0 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!) +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!) Dafny program verifier finished with 0 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!) +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!) Dafny program verifier finished with 0 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!) +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!) Dafny program verifier finished with 0 verified, 0 errors -[Program halted] ExpectAndExceptions.dfy(17,22): NatOutcome.NatFailure(Kaboom!) +[Program halted] ExpectAndExceptions.dfy(19,22): NatOutcome.NatFailure(Kaboom!) diff --git a/docs/dev/news/6050.fix b/docs/dev/news/6050.fix new file mode 100644 index 00000000000..c9e1028c8d6 --- /dev/null +++ b/docs/dev/news/6050.fix @@ -0,0 +1 @@ +Fix a bug that caused a crash when translating by blocks \ No newline at end of file