From c1b06a908ab1ed746672dd42eaf9417916a297cc Mon Sep 17 00:00:00 2001 From: Shaz Qadeer Date: Thu, 1 Oct 2015 09:40:42 -0700 Subject: another fix requested by Chris verification is performed now for all created layers --- Source/Concurrency/CivlRefinement.cs | 2 +- Source/Concurrency/CivlTypeChecker.cs | 20 -------------------- Source/Concurrency/YieldTypeChecker.cs | 2 +- Test/civl/DeviceCache.bpl.expect | 2 +- Test/civl/FlanaganQadeer.bpl.expect | 2 +- Test/civl/Program1.bpl.expect | 2 +- Test/civl/Program2.bpl.expect | 2 +- Test/civl/Program3.bpl.expect | 2 +- Test/civl/Program4.bpl.expect | 2 +- Test/civl/Program5.bpl.expect | 2 +- Test/civl/StoreBuffer.bpl.expect | 2 +- Test/civl/akash.bpl.expect | 2 +- Test/civl/alloc.bpl.expect | 2 +- Test/civl/bar.bpl.expect | 2 +- Test/civl/chris2.bpl.expect | 2 +- Test/civl/chris6.bpl | 14 ++++++++++++++ Test/civl/chris6.bpl.expect | 5 +++++ Test/civl/civl-paper.bpl.expect | 2 +- Test/civl/foo.bpl.expect | 2 +- Test/civl/ghost.bpl.expect | 2 +- Test/civl/linear-set.bpl.expect | 2 +- Test/civl/linear-set2.bpl.expect | 2 +- Test/civl/lock-introduced.bpl.expect | 2 +- Test/civl/lock.bpl.expect | 2 +- Test/civl/lock2.bpl.expect | 2 +- Test/civl/multiset.bpl.expect | 2 +- Test/civl/new1.bpl.expect | 2 +- Test/civl/one.bpl.expect | 2 +- Test/civl/par-incr.bpl.expect | 2 +- Test/civl/parallel1.bpl.expect | 2 +- Test/civl/parallel2.bpl.expect | 2 +- Test/civl/parallel4.bpl.expect | 2 +- Test/civl/parallel5.bpl.expect | 2 +- Test/civl/perm.bpl.expect | 2 +- Test/civl/t1.bpl.expect | 2 +- Test/civl/termination2.bpl.expect | 2 +- Test/civl/ticket.bpl.expect | 2 +- Test/civl/treiber-stack.bpl.expect | 2 +- Test/civl/wsq.bpl.expect | 2 +- 39 files changed, 55 insertions(+), 56 deletions(-) create mode 100644 Test/civl/chris6.bpl create mode 100644 Test/civl/chris6.bpl.expect diff --git a/Source/Concurrency/CivlRefinement.cs b/Source/Concurrency/CivlRefinement.cs index 43d0f60c..8fc27be9 100644 --- a/Source/Concurrency/CivlRefinement.cs +++ b/Source/Concurrency/CivlRefinement.cs @@ -1212,7 +1212,7 @@ namespace Microsoft.Boogie public static void AddCheckers(LinearTypeChecker linearTypeChecker, CivlTypeChecker civlTypeChecker, List decls) { Program program = linearTypeChecker.program; - foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums) + foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums) { if (CommandLineOptions.Clo.TrustLayersDownto <= layerNum || layerNum <= CommandLineOptions.Clo.TrustLayersUpto) continue; diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs index dba7ab4b..5215bc52 100644 --- a/Source/Concurrency/CivlTypeChecker.cs +++ b/Source/Concurrency/CivlTypeChecker.cs @@ -486,26 +486,6 @@ namespace Microsoft.Boogie } } - private HashSet allImplementedLayerNums; - public IEnumerable AllImplementedLayerNums - { - get - { - if (allImplementedLayerNums == null) - { - allImplementedLayerNums = new HashSet(); - foreach (ActionInfo actionInfo in procToActionInfo.Values) - { - if (actionInfo.hasImplementation) - { - allImplementedLayerNums.Add(actionInfo.createdAtLayerNum); - } - } - } - return allImplementedLayerNums; - } - } - private HashSet allCreatedLayerNums; public IEnumerable AllCreatedLayerNums { diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index a69f066d..027e7e83 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -141,7 +141,7 @@ namespace Microsoft.Boogie Graph implGraph = Program.GraphFromImpl(impl); implGraph.ComputeLoops(); int specLayerNum = civlTypeChecker.procToActionInfo[impl.Proc].createdAtLayerNum; - foreach (int layerNum in civlTypeChecker.AllImplementedLayerNums) + foreach (int layerNum in civlTypeChecker.AllCreatedLayerNums) { if (layerNum > specLayerNum) continue; YieldTypeChecker executor = new YieldTypeChecker(civlTypeChecker, impl, layerNum, implGraph.Headers); diff --git a/Test/civl/DeviceCache.bpl.expect b/Test/civl/DeviceCache.bpl.expect index c4cf5ccf..129e60e2 100644 --- a/Test/civl/DeviceCache.bpl.expect +++ b/Test/civl/DeviceCache.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 30 verified, 0 errors +Boogie program verifier finished with 39 verified, 0 errors diff --git a/Test/civl/FlanaganQadeer.bpl.expect b/Test/civl/FlanaganQadeer.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/FlanaganQadeer.bpl.expect +++ b/Test/civl/FlanaganQadeer.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/Program1.bpl.expect b/Test/civl/Program1.bpl.expect index 41374b00..00ddb38b 100644 --- a/Test/civl/Program1.bpl.expect +++ b/Test/civl/Program1.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/Program2.bpl.expect b/Test/civl/Program2.bpl.expect index a9949f2e..9823d44a 100644 --- a/Test/civl/Program2.bpl.expect +++ b/Test/civl/Program2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/Program3.bpl.expect b/Test/civl/Program3.bpl.expect index a9949f2e..9823d44a 100644 --- a/Test/civl/Program3.bpl.expect +++ b/Test/civl/Program3.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/Program4.bpl.expect b/Test/civl/Program4.bpl.expect index a9949f2e..9823d44a 100644 --- a/Test/civl/Program4.bpl.expect +++ b/Test/civl/Program4.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/civl/Program5.bpl.expect b/Test/civl/Program5.bpl.expect index fde7e712..4bcb1071 100644 --- a/Test/civl/Program5.bpl.expect +++ b/Test/civl/Program5.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 18 verified, 0 errors +Boogie program verifier finished with 21 verified, 0 errors diff --git a/Test/civl/StoreBuffer.bpl.expect b/Test/civl/StoreBuffer.bpl.expect index 8c74fe2e..1931ffd2 100644 --- a/Test/civl/StoreBuffer.bpl.expect +++ b/Test/civl/StoreBuffer.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 17 verified, 0 errors +Boogie program verifier finished with 27 verified, 0 errors diff --git a/Test/civl/akash.bpl.expect b/Test/civl/akash.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/akash.bpl.expect +++ b/Test/civl/akash.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/alloc.bpl.expect b/Test/civl/alloc.bpl.expect index f08c6e00..4bcb1071 100644 --- a/Test/civl/alloc.bpl.expect +++ b/Test/civl/alloc.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 12 verified, 0 errors +Boogie program verifier finished with 21 verified, 0 errors diff --git a/Test/civl/bar.bpl.expect b/Test/civl/bar.bpl.expect index 810c93bf..be6722fe 100644 --- a/Test/civl/bar.bpl.expect +++ b/Test/civl/bar.bpl.expect @@ -10,4 +10,4 @@ Execution trace: (0,0): anon00 (0,0): inline$Impl_YieldChecker_PC_1$0$L0 -Boogie program verifier finished with 3 verified, 2 errors +Boogie program verifier finished with 8 verified, 2 errors diff --git a/Test/civl/chris2.bpl.expect b/Test/civl/chris2.bpl.expect index ddb8537e..f3b66f4a 100644 --- a/Test/civl/chris2.bpl.expect +++ b/Test/civl/chris2.bpl.expect @@ -15,4 +15,4 @@ Execution trace: Execution trace: (0,0): this_A -Boogie program verifier finished with 1 verified, 4 errors +Boogie program verifier finished with 2 verified, 4 errors diff --git a/Test/civl/chris6.bpl b/Test/civl/chris6.bpl new file mode 100644 index 00000000..a0aecf1e --- /dev/null +++ b/Test/civl/chris6.bpl @@ -0,0 +1,14 @@ +// RUN: %boogie -noinfer -useArrayTheory "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure{:extern}{:yields}{:layer 1,2} P1(); + requires{:layer 1} false; + ensures{:atomic} |{ A: return true; }|; + +procedure{:yields}{:layer 2,3} P2() + ensures{:atomic} |{ A: return true; }|; +{ + assert{:layer 1} false; + yield; + call P1(); + yield; +} diff --git a/Test/civl/chris6.bpl.expect b/Test/civl/chris6.bpl.expect new file mode 100644 index 00000000..229e4e10 --- /dev/null +++ b/Test/civl/chris6.bpl.expect @@ -0,0 +1,5 @@ +chris6.bpl(10,3): Error BP5001: This assertion might not hold. +Execution trace: + chris6.bpl(10,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/civl/civl-paper.bpl.expect b/Test/civl/civl-paper.bpl.expect index 11d204a8..bd1df2f9 100644 --- a/Test/civl/civl-paper.bpl.expect +++ b/Test/civl/civl-paper.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 35 verified, 0 errors +Boogie program verifier finished with 45 verified, 0 errors diff --git a/Test/civl/foo.bpl.expect b/Test/civl/foo.bpl.expect index 41e30691..44a93860 100644 --- a/Test/civl/foo.bpl.expect +++ b/Test/civl/foo.bpl.expect @@ -5,4 +5,4 @@ Execution trace: foo.bpl(14,3): inline$Incr_1$0$A (0,0): inline$Impl_YieldChecker_PC_1$0$L0 -Boogie program verifier finished with 4 verified, 1 error +Boogie program verifier finished with 9 verified, 1 error diff --git a/Test/civl/ghost.bpl.expect b/Test/civl/ghost.bpl.expect index 9823d44a..76a9a2bf 100644 --- a/Test/civl/ghost.bpl.expect +++ b/Test/civl/ghost.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 6 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/linear-set.bpl.expect b/Test/civl/linear-set.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/linear-set.bpl.expect +++ b/Test/civl/linear-set.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/linear-set2.bpl.expect b/Test/civl/linear-set2.bpl.expect index 00ddb38b..76a9a2bf 100644 --- a/Test/civl/linear-set2.bpl.expect +++ b/Test/civl/linear-set2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/lock-introduced.bpl.expect b/Test/civl/lock-introduced.bpl.expect index f08c6e00..8c74fe2e 100644 --- a/Test/civl/lock-introduced.bpl.expect +++ b/Test/civl/lock-introduced.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 12 verified, 0 errors +Boogie program verifier finished with 17 verified, 0 errors diff --git a/Test/civl/lock.bpl.expect b/Test/civl/lock.bpl.expect index 3e6d423a..76a9a2bf 100644 --- a/Test/civl/lock.bpl.expect +++ b/Test/civl/lock.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/lock2.bpl.expect b/Test/civl/lock2.bpl.expect index 3e6d423a..76a9a2bf 100644 --- a/Test/civl/lock2.bpl.expect +++ b/Test/civl/lock2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/multiset.bpl.expect b/Test/civl/multiset.bpl.expect index 0a77c517..63682bb4 100644 --- a/Test/civl/multiset.bpl.expect +++ b/Test/civl/multiset.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 78 verified, 0 errors +Boogie program verifier finished with 85 verified, 0 errors diff --git a/Test/civl/new1.bpl.expect b/Test/civl/new1.bpl.expect index 41374b00..00ddb38b 100644 --- a/Test/civl/new1.bpl.expect +++ b/Test/civl/new1.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/one.bpl.expect b/Test/civl/one.bpl.expect index 37fad75c..41374b00 100644 --- a/Test/civl/one.bpl.expect +++ b/Test/civl/one.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 1 verified, 0 errors +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/par-incr.bpl.expect b/Test/civl/par-incr.bpl.expect index 00ddb38b..3e3dc54b 100644 --- a/Test/civl/par-incr.bpl.expect +++ b/Test/civl/par-incr.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 4 verified, 0 errors +Boogie program verifier finished with 7 verified, 0 errors diff --git a/Test/civl/parallel1.bpl.expect b/Test/civl/parallel1.bpl.expect index 889ee4f2..fa974099 100644 --- a/Test/civl/parallel1.bpl.expect +++ b/Test/civl/parallel1.bpl.expect @@ -5,4 +5,4 @@ Execution trace: parallel1.bpl(14,3): inline$Incr_1$0$A (0,0): inline$Impl_YieldChecker_PC_1$0$L0 -Boogie program verifier finished with 3 verified, 1 error +Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/parallel2.bpl.expect b/Test/civl/parallel2.bpl.expect index 3e6d423a..12041afe 100644 --- a/Test/civl/parallel2.bpl.expect +++ b/Test/civl/parallel2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 10 verified, 0 errors diff --git a/Test/civl/parallel4.bpl.expect b/Test/civl/parallel4.bpl.expect index 2d4c8148..baf228c8 100644 --- a/Test/civl/parallel4.bpl.expect +++ b/Test/civl/parallel4.bpl.expect @@ -3,4 +3,4 @@ Execution trace: parallel4.bpl(29,5): anon0 (0,0): anon01 -Boogie program verifier finished with 3 verified, 1 error +Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/civl/parallel5.bpl.expect b/Test/civl/parallel5.bpl.expect index 3e6d423a..12041afe 100644 --- a/Test/civl/parallel5.bpl.expect +++ b/Test/civl/parallel5.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 5 verified, 0 errors +Boogie program verifier finished with 10 verified, 0 errors diff --git a/Test/civl/perm.bpl.expect b/Test/civl/perm.bpl.expect index 41374b00..00ddb38b 100644 --- a/Test/civl/perm.bpl.expect +++ b/Test/civl/perm.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 2 verified, 0 errors +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/civl/t1.bpl.expect b/Test/civl/t1.bpl.expect index fcef7e58..27a208d4 100644 --- a/Test/civl/t1.bpl.expect +++ b/Test/civl/t1.bpl.expect @@ -6,4 +6,4 @@ Execution trace: t1.bpl(25,21): inline$SetG_1$0$A (0,0): inline$Impl_YieldChecker_A_1$0$L1 -Boogie program verifier finished with 4 verified, 1 error +Boogie program verifier finished with 9 verified, 1 error diff --git a/Test/civl/termination2.bpl.expect b/Test/civl/termination2.bpl.expect index 37fad75c..41374b00 100644 --- a/Test/civl/termination2.bpl.expect +++ b/Test/civl/termination2.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 1 verified, 0 errors +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/civl/ticket.bpl.expect b/Test/civl/ticket.bpl.expect index b072912b..dc45a0ee 100644 --- a/Test/civl/ticket.bpl.expect +++ b/Test/civl/ticket.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 16 verified, 0 errors +Boogie program verifier finished with 24 verified, 0 errors diff --git a/Test/civl/treiber-stack.bpl.expect b/Test/civl/treiber-stack.bpl.expect index 9823d44a..76a9a2bf 100644 --- a/Test/civl/treiber-stack.bpl.expect +++ b/Test/civl/treiber-stack.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 6 verified, 0 errors +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/civl/wsq.bpl.expect b/Test/civl/wsq.bpl.expect index a9949f2e..9823d44a 100644 --- a/Test/civl/wsq.bpl.expect +++ b/Test/civl/wsq.bpl.expect @@ -1,2 +1,2 @@ -Boogie program verifier finished with 3 verified, 0 errors +Boogie program verifier finished with 6 verified, 0 errors -- cgit v1.2.3