From 74ac2e7f2a2b01baf41000979f9332a34692ade2 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 10 Aug 2023 08:38:24 -0700 Subject: [PATCH 1/4] Print verification coverage only when -trace used The -trackVerificationCoverage option enables tracking of verification coverage but the results are printed only when -trace is also provided. This makes it possible to see the results in text, but makes the output less noisy for clients of Boogie as a library (such as Dafny). --- Source/ExecutionEngine/ExecutionEngine.cs | 2 +- Test/coverage/verificationCoverage.bpl | 17 +++++++++++++++-- ...ct.plain => verificationCoverage.bpl.expect} | 0 .../verificationCoverage.bpl.expect.coverage | 3 --- 4 files changed, 16 insertions(+), 6 deletions(-) rename Test/coverage/{verificationCoverage.bpl.expect.plain => verificationCoverage.bpl.expect} (100%) delete mode 100644 Test/coverage/verificationCoverage.bpl.expect.coverage diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 78d20b958..1eec9f43c 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -673,7 +673,7 @@ private async Task VerifyEachImplementation(TextWriter output, CleanupRequest(requestId); } - if (Options.TrackVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) { + if (Options.Trace && Options.TrackVerificationCoverage && processedProgram.Program.AllCoveredElements.Any()) { Options.OutputWriter.WriteLine("Elements covered by verification: {0}", string.Join(", ", processedProgram.Program.AllCoveredElements.OrderBy(s => s))); } diff --git a/Test/coverage/verificationCoverage.bpl b/Test/coverage/verificationCoverage.bpl index e5e27f135..351cf0ae1 100644 --- a/Test/coverage/verificationCoverage.bpl +++ b/Test/coverage/verificationCoverage.bpl @@ -1,7 +1,20 @@ // RUN: %boogie "%s" > "%t.plain" -// RUN: %diff "%s.expect.plain" "%t.plain" +// RUN: %diff "%s.expect" "%t.plain" +// RUN: %boogie -trackVerificationCoverage -trace "%s" > "%t.coverage" +// RUN %OutputCheck "%s" --file-to-check="%t.coverage" +// CHECK: Covered elements: a0, assert_a0, assert_r0, r0 +// CHECK: Covered elements: sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1 +// CHECK: Covered elements: cont_assume_1, cont_assume_2 +// CHECK: Covered elements: false_req +// CHECK: Covered elements: cont_req_1, cont_req_2 +// CHECK: Covered elements: assumeFalse +// CHECK: Covered elements: tee0, tee1, ter0 +// CHECK: Covered elements: call2_tee1, tee_not_1, tee0$call1$ensures, tee0$call2$ensures, tee1$call2$ensures, ter0$call1$requires, ter0$call2$requires, ter1, xy_sum +// CHECK: Covered elements: a_gt_10, constrained, x_gt_10 +// CHECK: Covered elements: cont_ens_abs$call_cont$ensures, xpos_abs$call_cont$requires, xpos_caller +// CHECK: Elements covered by verification: a_gt_10, a0, assert_a0, assert_r0, assumeFalse, call2_tee1, constrained, cont_assume_1, cont_assume_2, cont_ens_abs$call_cont$ensures, cont_req_1, cont_req_2, false_req, r0, sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1, tee_not_1, tee0, tee0$call1$ensures, tee0$call2$ensures, tee1, tee1$call2$ensures, ter0, ter0$call1$requires, ter0$call2$requires, ter1, x_gt_10, xpos_abs$call_cont$requires, xpos_caller, xy_sum // RUN: %boogie -trackVerificationCoverage "%s" > "%t.coverage" -// RUN: %diff "%s.expect.coverage" "%t.coverage" +// RUN: %diff "%s.expect" "%t.coverage" // UNSUPPORTED: batch_mode procedure testRequiresAssign(n: int) diff --git a/Test/coverage/verificationCoverage.bpl.expect.plain b/Test/coverage/verificationCoverage.bpl.expect similarity index 100% rename from Test/coverage/verificationCoverage.bpl.expect.plain rename to Test/coverage/verificationCoverage.bpl.expect diff --git a/Test/coverage/verificationCoverage.bpl.expect.coverage b/Test/coverage/verificationCoverage.bpl.expect.coverage deleted file mode 100644 index 32f5d2408..000000000 --- a/Test/coverage/verificationCoverage.bpl.expect.coverage +++ /dev/null @@ -1,3 +0,0 @@ -Elements covered by verification: a_gt_10, a0, assert_a0, assert_r0, assumeFalse, call2_tee1, constrained, cont_assume_1, cont_assume_2, cont_ens_abs$call_cont$ensures, cont_req_1, cont_req_2, false_req, r0, sinv_not_1$established, sinv_not_1$maintained, sinv1$assume_in_body, sinv1$established, sinv1$maintained, sinv2$assume_in_body, sinv2$established, sinv2$maintained, spost, spre1, tee_not_1, tee0, tee0$call1$ensures, tee0$call2$ensures, tee1, tee1$call2$ensures, ter0, ter0$call1$requires, ter0$call2$requires, ter1, x_gt_10, xpos_abs$call_cont$requires, xpos_caller, xy_sum - -Boogie program verifier finished with 10 verified, 0 errors From 40d1e0881c0700d97d4503ff806d7432f3684663 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Thu, 10 Aug 2023 11:23:37 -0700 Subject: [PATCH 2/4] Fix unnecessaryassumes1 --- Test/unnecessaryassumes/unnecessaryassumes1.bpl | 7 +++++-- Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect | 3 --- 2 files changed, 5 insertions(+), 5 deletions(-) delete mode 100644 Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl b/Test/unnecessaryassumes/unnecessaryassumes1.bpl index 34377644f..e5ec0bbbe 100644 --- a/Test/unnecessaryassumes/unnecessaryassumes1.bpl +++ b/Test/unnecessaryassumes/unnecessaryassumes1.bpl @@ -1,6 +1,9 @@ // We use boogie instead of parallel-boogie here to fix the order of the output from /trackVerificationCoverage -// RUN: %boogie /trackVerificationCoverage "%s" > "%t" -// RUN: %diff "%s.expect" "%t" +// RUN: %boogie -trackVerificationCoverage -trace "%s" > "%t" +// RUN: %OutputCheck "%s" --file-to-check="%t" +// CHECK: Covered elements: s0 +// CHECK: Covered elements: s2, s3 +// CHECK: Elements covered by verification: s0, s2, s3 // UNSUPPORTED: batch_mode procedure test0(n: int) diff --git a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect b/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect deleted file mode 100644 index 34f57618e..000000000 --- a/Test/unnecessaryassumes/unnecessaryassumes1.bpl.expect +++ /dev/null @@ -1,3 +0,0 @@ -Elements covered by verification: s0, s2, s3 - -Boogie program verifier finished with 3 verified, 0 errors From 29854ff7dd94bbbf11fd2d445c6505b6d3afbd87 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 11 Aug 2023 08:49:30 -0700 Subject: [PATCH 3/4] Attempt to fix proof failure for GC.bpl --- Test/civl/samples/GC.bpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/civl/samples/GC.bpl b/Test/civl/samples/GC.bpl index 560489b9d..dbbbe612c 100644 --- a/Test/civl/samples/GC.bpl +++ b/Test/civl/samples/GC.bpl @@ -2,7 +2,7 @@ // Copyright (c) Microsoft Corporation. All rights reserved. // -// RUN: %parallel-boogie "%s" > "%t" +// RUN: %parallel-boogie -vcsSplitOnEveryAssert "%s" > "%t" // RUN: %diff "%s.expect" "%t" type {:linear "tid"} X = int; From 77a9f01557dec379f12edb54f4962045310132d1 Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Sat, 12 Aug 2023 07:20:38 -0700 Subject: [PATCH 4/4] another attempt to fix flakiness --- Test/civl/samples/GC.bpl | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Test/civl/samples/GC.bpl b/Test/civl/samples/GC.bpl index dbbbe612c..59c2b5154 100644 --- a/Test/civl/samples/GC.bpl +++ b/Test/civl/samples/GC.bpl @@ -2,7 +2,7 @@ // Copyright (c) Microsoft Corporation. All rights reserved. // -// RUN: %parallel-boogie -vcsSplitOnEveryAssert "%s" > "%t" +// RUN: %parallel-boogie "%s" > "%t" // RUN: %diff "%s.expect" "%t" type {:linear "tid"} X = int; @@ -293,6 +293,7 @@ requires call Yield_RootScanBarrierInv(); call UpdateMutatorPhase(tid); call Yield_Iso(); call ptr, absPtr := AllocRaw(tid, y); + assert {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet); } atomic action {:layer 101} AtomicWriteField({:linear "tid"} tid:Tid, x: idx, f: fld, y: idx) // x.f = y