From 071a2eae55d581e725a0bbd9a032b4c036b4b266 Mon Sep 17 00:00:00 2001 From: stefanheule Date: Thu, 20 Sep 2012 11:01:25 +0200 Subject: Chalice: New regression test case from workitem 10221. --- Chalice/tests/regressions/workitem-10221.chalice | 158 +++++++++++++++++++++ .../tests/regressions/workitem-10221.output.txt | 4 + 2 files changed, 162 insertions(+) create mode 100644 Chalice/tests/regressions/workitem-10221.chalice create mode 100644 Chalice/tests/regressions/workitem-10221.output.txt diff --git a/Chalice/tests/regressions/workitem-10221.chalice b/Chalice/tests/regressions/workitem-10221.chalice new file mode 100644 index 00000000..2a8ae723 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10221.chalice @@ -0,0 +1,158 @@ +// In this example, additional unfold/fold pairs make the verification of the last three methods fail. + +class Node { + var next : Node; + var val : int; + + predicate list { + acc(next) && acc(val) && (next!=null ==> next.list) + } + + function vals() : seq + requires list + { + unfolding list in (next == null ? [val] : [val] ++ next.vals()) + } + + function reverse_vals() : seq + requires list + { + unfolding list in (next == null ? [val] : next.reverse_vals() ++ [val]) + } + + method reverse_in_place() returns (r:Node) + requires list; + ensures true; + { + var l : Node := this; + r := null; + + var rev : seq := this.reverse_vals(); + + while (l != null) + invariant l!=null ==> l.list; + invariant r!=null ==> r.list; + invariant rev == (l==null ? nil : l.reverse_vals()) ++ (r==null ? nil : r.vals()); + { + var y: Node; +// if (r != null) { +// unfold r.list; fold r.list; +// } + unfold l.list; +// if (l.next != null) { +// unfold l.next.list; fold l.next.list; +// } + + y := l.next; + l.next := r; + r := l; + fold r.list; + l := y; + } + assert r.vals() == rev; // should be the post-condition + } + + + method reverse_in_place_01() returns (r:Node) + requires list; + ensures true; + { + var l : Node := this; + r := null; + + var rev : seq := this.reverse_vals(); + + while (l != null) + invariant l!=null ==> l.list; + invariant r!=null ==> r.list; + invariant rev == (l==null ? nil : l.reverse_vals()) ++ (r==null ? nil : r.vals()); + { + var y: Node; +// if (r != null) { +// unfold r.list; fold r.list; +// } + unfold l.list; + if (l.next != null) { + unfold l.next.list; fold l.next.list; + } + + y := l.next; + l.next := r; + r := l; + fold r.list; + l := y; + } + assert r.vals() == rev; // should be the post-condition + } + + + + method reverse_in_place_10() returns (r:Node) + requires list; + ensures true; + { + var l : Node := this; + r := null; + + var rev : seq := this.reverse_vals(); + + while (l != null) + invariant l!=null ==> l.list; + invariant r!=null ==> r.list; + invariant rev == (l==null ? nil : l.reverse_vals()) ++ (r==null ? nil : r.vals()); + { + var y: Node; + if (r != null) { + unfold r.list; fold r.list; + } + unfold l.list; +// if (l.next != null) { +// unfold l.next.list; fold l.next.list; +// } + + y := l.next; + l.next := r; + r := l; + fold r.list; + l := y; + } + assert r.vals() == rev; // should be the post-condition + } + + + + + method reverse_in_place_11() returns (r:Node) + requires list; + ensures true; + { + var l : Node := this; + r := null; + + var rev : seq := this.reverse_vals(); + + while (l != null) + invariant l!=null ==> l.list; + invariant r!=null ==> r.list; + invariant rev == (l==null ? nil : l.reverse_vals()) ++ (r==null ? nil : r.vals()); + { + var y: Node; + if (r != null) { + unfold r.list; fold r.list; + } + unfold l.list; + if (l.next != null) { + unfold l.next.list; fold l.next.list; + } + + y := l.next; + l.next := r; + r := l; + fold r.list; + l := y; + } + assert r.vals() == rev; // should be the post-condition + } + + +} \ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10221.output.txt b/Chalice/tests/regressions/workitem-10221.output.txt new file mode 100644 index 00000000..e209c3c1 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10221.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10221.chalice using parameters="" + + +Boogie program verifier finished with 0 errors and 0 smoke test warnings -- cgit v1.2.3 From f5a4ee5fb54f704387dcfdc7e4ee183d1bbc7876 Mon Sep 17 00:00:00 2001 From: stefanheule Date: Thu, 20 Sep 2012 11:34:50 +0200 Subject: Chalice: New regression tests for fixed workitems 10189 and 10208. --- Chalice/tests/regressions/workitem-10189.chalice | 23 ++++++++++++ .../tests/regressions/workitem-10189.output.txt | 4 +++ Chalice/tests/regressions/workitem-10208.chalice | 41 ++++++++++++++++++++++ .../tests/regressions/workitem-10208.output.txt | 8 +++++ 4 files changed, 76 insertions(+) create mode 100644 Chalice/tests/regressions/workitem-10189.chalice create mode 100644 Chalice/tests/regressions/workitem-10189.output.txt create mode 100644 Chalice/tests/regressions/workitem-10208.chalice create mode 100644 Chalice/tests/regressions/workitem-10208.output.txt diff --git a/Chalice/tests/regressions/workitem-10189.chalice b/Chalice/tests/regressions/workitem-10189.chalice new file mode 100644 index 00000000..b37b83f2 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10189.chalice @@ -0,0 +1,23 @@ +class Node { + var v: int + var next: Node + + predicate V { + acc(v) + && acc(next) + && (next != null ==> next.V) + } + + unlimited function length(): int + requires rd(V) + { 1 + unfolding rd(V) in next == null ? 0 : next.length() } + + unlimited function at(i: int): int + requires rd(V) + requires i >= 0 + requires i < length() // XXXX + { + unfolding rd(V) in i == 0 ? v : next.at(i - 1) + // Precondition at XXX might not hold + } +} \ No newline at end of file diff --git a/Chalice/tests/regressions/workitem-10189.output.txt b/Chalice/tests/regressions/workitem-10189.output.txt new file mode 100644 index 00000000..96f05468 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10189.output.txt @@ -0,0 +1,4 @@ +Verification of workitem-10189.chalice using parameters="" + + +Boogie program verifier finished with 0 errors and 0 smoke test warnings diff --git a/Chalice/tests/regressions/workitem-10208.chalice b/Chalice/tests/regressions/workitem-10208.chalice new file mode 100644 index 00000000..ae1a7d89 --- /dev/null +++ b/Chalice/tests/regressions/workitem-10208.chalice @@ -0,0 +1,41 @@ +class Test { + var f1: int; + var f2: int; + + predicate valid { + acc(f1) && acc(f2) && f1 == f2 + } + + method test() + requires valid + { + unfold valid + f1 := 2 + f2 := 2 + fold valid + + /* --- not strictly necessary */ + unfold valid + assert f1 == 2 + fold valid + /* --- */ + + call test2() + + unfold valid + assert f1 == 2 // BUG: this should not verify (1) + assert false // BUG: this should not verify (2) + } + + method test2() + requires valid + ensures valid + ensures unfolding valid in f1 == 1 // line (1) above verifies also without this postcondition + { + unfold valid + f1 := 1 + f2 := 1 + fold valid + } + +} diff --git a/Chalice/tests/regressions/workitem-10208.output.txt b/Chalice/tests/regressions/workitem-10208.output.txt new file mode 100644 index 00000000..0666393a --- /dev/null +++ b/Chalice/tests/regressions/workitem-10208.output.txt @@ -0,0 +1,8 @@ +Verification of workitem-10208.chalice using parameters="" + + 26.5: Assertion might not hold. The expression at 26.12 might not evaluate to true. + +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. + 9.3: The end of method test is unreachable. + +Boogie program verifier finished with 1 errors and 1 smoke test warnings -- cgit v1.2.3 From 1eaa3f92b844ab69824df8e87d26250c3e5552a0 Mon Sep 17 00:00:00 2001 From: stefanheule Date: Fri, 21 Sep 2012 08:49:26 +0200 Subject: Chalice: Update release script to adapt to new scala version. --- Chalice/scripts/create_release/create_release.bat | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Chalice/scripts/create_release/create_release.bat b/Chalice/scripts/create_release/create_release.bat index a0d67fd9..5aadd36e 100644 --- a/Chalice/scripts/create_release/create_release.bat +++ b/Chalice/scripts/create_release/create_release.bat @@ -6,7 +6,7 @@ set BASE_DIR=%~dp0\..\.. set RELEASE_DIR_SRC=%~dp0\files set RELEASE_DIR_DST=%~dp0\release -set CHALICE_JAR_SRC=%BASE_DIR%\target\scala-2.8.1.final\chalice_2.8.1-1.0.jar +set CHALICE_JAR_SRC=%BASE_DIR%\target\scala-2.9.2\chalice_2.9.2-1.0.jar set CHALICE_JAR_DST=%RELEASE_DIR_DST%\chalice.jar pushd %BASE_DIR% -- cgit v1.2.3 From c2cb9eec0059d906a005605e563c95868620f6af Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 21 Sep 2012 09:56:35 +0200 Subject: Added linked list Chalice example --- .../tests/predicates/LinkedList-various.chalice | 176 +++++++++++++++++++++ 1 file changed, 176 insertions(+) create mode 100644 Chalice/tests/predicates/LinkedList-various.chalice diff --git a/Chalice/tests/predicates/LinkedList-various.chalice b/Chalice/tests/predicates/LinkedList-various.chalice new file mode 100644 index 00000000..a888b647 --- /dev/null +++ b/Chalice/tests/predicates/LinkedList-various.chalice @@ -0,0 +1,176 @@ +class Node +{ + var v:int; + var n:Node; + + predicate inv + { acc(v) && acc(n) && (n!=null ==> n.inv) } + + function len():int + requires inv; + ensures result>0; + { + unfolding inv in (n==null) ? 1 : 1+n.len() + } + + function get(i:int):int + requires inv && 0<=i && i get(i)==old(get(i))); + { + unfold inv; + if(n==null) + { + n:=new Node; + n.v:=x; n.n:=null; + fold n.inv; + } + else + { + call n.addLast(x); + } + fold inv; + } + + method append(p:List) + requires inv && p!=null && p.inv; + ensures inv; + ensures len()==old(len()+p.len()); + ensures (forall i in [0..old(len())] :: get(i)==old(get(i))); + ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len()))); + { + unfold inv; + if(n==null) + { + unfold p.inv; + n:=p.c; + } + else + { + call n.append(p); + } + fold inv; + } + + method remove(i:int) + requires inv && i>=0 && i c.inv) } + + function len():int + requires inv; + ensures result>=0; + { + unfolding inv in (c==null) ? 0 : c.len() + } + + function get(i:int):int + requires inv && 0<=i && i get(i)==old(get(i-1))); + { + var p:Node; + + unfold inv; + p:=new Node; p.v:=x; p.n:=c; c:=p; + fold c.inv; + assert c.len()==old(len())+1 + fold inv; + } + + method addLast(x:int) + requires inv; + ensures inv; + ensures len()==old(len())+1 && get(old(len()))==x; + ensures (forall i:int :: 0<=i && i get(i)==old(get(i))); + { + unfold inv; + if(c==null) + { + c:=new Node; + c.v:=x; c.n:=null; + fold c.inv; + } + else + { + call c.addLast(x); + } + fold inv; + } + + method append(p:List) + requires inv && p!=null && p.inv; + ensures inv; + ensures len()==old(len()+p.len()); + ensures (forall i in [0..old(len())] :: get(i)==old(get(i))); + ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len()))); + { + unfold inv; + if(c==null) + { + unfold p.inv; + c:=p.c; + } + else + { + call c.append(p); + } + fold inv; + } + + method remove(i:int) + requires inv && i>=0 && i Date: Fri, 21 Sep 2012 08:59:07 +0100 Subject: Added support for invariants about shared state. Reworked implementation of barriers. Started on support for barrier invariants. --- Source/GPUVerify/ArrayControlFlowAnalyser.cs | 4 +- Source/GPUVerify/GPUVerifier.cs | 103 +++++++++++++++++++-------- Source/GPUVerify/IRaceInstrumenter.cs | 2 +- Source/GPUVerify/NonLocalAccessCollector.cs | 1 - Source/GPUVerify/NullRaceInstrumenter.cs | 2 +- Source/GPUVerify/RaceInstrumenter.cs | 17 ++--- 6 files changed, 88 insertions(+), 41 deletions(-) diff --git a/Source/GPUVerify/ArrayControlFlowAnalyser.cs b/Source/GPUVerify/ArrayControlFlowAnalyser.cs index d7841f0e..649d76d7 100644 --- a/Source/GPUVerify/ArrayControlFlowAnalyser.cs +++ b/Source/GPUVerify/ArrayControlFlowAnalyser.cs @@ -172,7 +172,9 @@ namespace GPUVerify { CallCmd callCmd = c as CallCmd; - if (callCmd.callee != verifier.BarrierProcedure.Name) + if (callCmd.callee != verifier.BarrierProcedure.Name && + callCmd.callee != verifier.BarrierInvariantProcedure.Name && + callCmd.callee != verifier.BarrierInvariantInstantiationProcedure.Name) { Implementation CalleeImplementation = verifier.GetImplementation(callCmd.callee); diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 868bcaa1..351fe45e 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -18,7 +18,9 @@ namespace GPUVerify public Procedure KernelProcedure; public Implementation KernelImplementation; - public Procedure BarrierProcedure; + public Procedure BarrierProcedure; + public Procedure BarrierInvariantProcedure; + public Procedure BarrierInvariantInstantiationProcedure; public IKernelArrayInfo KernelArrayInfo = new KernelArrayInfoLists(); @@ -128,6 +130,42 @@ namespace GPUVerify ResContext.AddProcedure(p); } return p; + } + + private Procedure FindOrCreateBarrierInvariantProcedure() { + var p = CheckSingleInstanceOfAttributedProcedure("barrier_invariant"); + if (p == null) { + p = new Procedure(Token.NoToken, "barrier_invariant", new TypeVariableSeq(), + new VariableSeq(new Variable[] { + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__cond", + Microsoft.Boogie.Type.Bool), true) + }), + new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), + new EnsuresSeq(), + new QKeyValue(Token.NoToken, "barrier_invariant", new List(), null)); + Program.TopLevelDeclarations.Add(p); + ResContext.AddProcedure(p); + } + return p; + } + + private Procedure FindOrCreateBarrierInvariantInstantiationProcedure() { + var p = CheckSingleInstanceOfAttributedProcedure("barrier_invariant_instantiation"); + if (p == null) { + p = new Procedure(Token.NoToken, "barrier_invariant_instantiation", new TypeVariableSeq(), + new VariableSeq(new Variable[] { + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__t1", + new BvType(32)), true), + new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "__t2", + new BvType(32)), true) + }), + new VariableSeq(), new RequiresSeq(), new IdentifierExprSeq(), + new EnsuresSeq(), + new QKeyValue(Token.NoToken, "barrier_invariant_instantiation", new List(), null)); + Program.TopLevelDeclarations.Add(p); + ResContext.AddProcedure(p); + } + return p; } private Procedure CheckSingleInstanceOfAttributedProcedure(string attribute) @@ -1376,17 +1414,19 @@ namespace GPUVerify if(KernelArrayInfo.getGroupSharedArrays().Count > 0) { - Expr IfGuard1 = Expr.And(P1, LocalFence1); - Expr IfGuard2 = Expr.And(P2, LocalFence2); - - bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(), - new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetBlocks(1, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null), - null)); - bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(), - new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetBlocks(2, KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null), - null)); - - bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays())); + bigblocks.AddRange( + MakeResetBlocks(Expr.And(P1, LocalFence1), KernelArrayInfo.getGroupSharedArrays())); + + // This could be relaxed to take into account whether the threads are in different + // groups, but for now we keep it relatively simple + + Expr AtLeastOneEnabledWithLocalFence = + Expr.Or(Expr.And(P1, LocalFence1), Expr.And(P2, LocalFence2)); + + bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(new Cmd[] { }), + new IfCmd(Token.NoToken, + AtLeastOneEnabledWithLocalFence, + new StmtList(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null), null)); } if (KernelArrayInfo.getGlobalArrays().Count > 0) @@ -1394,14 +1434,16 @@ namespace GPUVerify Expr IfGuard1 = Expr.And(P1, GlobalFence1); Expr IfGuard2 = Expr.And(P2, GlobalFence2); - bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(), - new IfCmd(Token.NoToken, IfGuard1, new StmtList(MakeResetBlocks(1, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null), - null)); - bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(), - new IfCmd(Token.NoToken, IfGuard2, new StmtList(MakeResetBlocks(2, KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null), - null)); - - bigblocks.AddRange(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays())); + bigblocks.AddRange( + MakeResetBlocks(Expr.And(P1, GlobalFence1), KernelArrayInfo.getGlobalArrays())); + + Expr ThreadsInSameGroup_BothEnabled_AtLeastOneGlobalFence = + Expr.And(Expr.And(GPUVerifier.ThreadsInSameGroup(), Expr.And(P1, P2)), Expr.Or(GlobalFence1, GlobalFence2)); + + bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(new Cmd[] { }), + new IfCmd(Token.NoToken, + ThreadsInSameGroup_BothEnabled_AtLeastOneGlobalFence, + new StmtList(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null), null)); } StmtList statements = new StmtList(bigblocks, BarrierProcedure.tok); @@ -1432,16 +1474,16 @@ namespace GPUVerify new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 1)); } - private List MakeResetBlocks(int Thread, ICollection variables) + private List MakeResetBlocks(Expr ResetCondition, ICollection variables) { Debug.Assert(variables.Count > 0); - List ResetAndHavocBlocks = new List(); + List result = new List(); foreach (Variable v in variables) { - ResetAndHavocBlocks.Add(RaceInstrumenter.MakeResetReadWriteSetStatements(v, Thread)); + result.Add(RaceInstrumenter.MakeResetReadWriteSetStatements(v, ResetCondition)); } - Debug.Assert(ResetAndHavocBlocks.Count > 0); - return ResetAndHavocBlocks; + Debug.Assert(result.Count > 0); + return result; } private List MakeHavocBlocks(ICollection variables) { @@ -1765,7 +1807,7 @@ namespace GPUVerify } else if (c is AssertCmd) { - result.simpleCmds.Add(new AssertCmd(c.tok, PullOutNonLocalAccessesIntoTemps(result, (c as AssertCmd).Expr, impl))); + // Do not pull non-local accesses out of assert commands } else if (c is AssumeCmd) { @@ -1982,7 +2024,9 @@ namespace GPUVerify private int Check() { - BarrierProcedure = FindOrCreateBarrierProcedure(); + BarrierProcedure = FindOrCreateBarrierProcedure(); + BarrierInvariantProcedure = FindOrCreateBarrierInvariantProcedure(); + BarrierInvariantInstantiationProcedure = FindOrCreateBarrierInvariantInstantiationProcedure(); KernelProcedure = CheckExactlyOneKernelProcedure(); if (ErrorCount > 0) @@ -2039,8 +2083,9 @@ namespace GPUVerify { return D as Implementation; } - } - Debug.Assert(false); + } + Error(Token.NoToken, "No implementation found for procedure \"" + procedureName + "\""); + Environment.Exit(1); return null; } diff --git a/Source/GPUVerify/IRaceInstrumenter.cs b/Source/GPUVerify/IRaceInstrumenter.cs index c85989c9..7f14fcd0 100644 --- a/Source/GPUVerify/IRaceInstrumenter.cs +++ b/Source/GPUVerify/IRaceInstrumenter.cs @@ -15,7 +15,7 @@ namespace GPUVerify void AddRaceCheckingDeclarations(); - BigBlock MakeResetReadWriteSetStatements(Variable v, int thread); + BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition); void AddRaceCheckingCandidateRequires(Procedure Proc); diff --git a/Source/GPUVerify/NonLocalAccessCollector.cs b/Source/GPUVerify/NonLocalAccessCollector.cs index 6a934899..d1361ff4 100644 --- a/Source/GPUVerify/NonLocalAccessCollector.cs +++ b/Source/GPUVerify/NonLocalAccessCollector.cs @@ -70,7 +70,6 @@ namespace GPUVerify return collector.Accesses.Count > 0; } - public override Expr VisitNAryExpr(NAryExpr node) { if (IsNonLocalAccess(node, NonLocalState)) diff --git a/Source/GPUVerify/NullRaceInstrumenter.cs b/Source/GPUVerify/NullRaceInstrumenter.cs index fae08aa3..6452331f 100644 --- a/Source/GPUVerify/NullRaceInstrumenter.cs +++ b/Source/GPUVerify/NullRaceInstrumenter.cs @@ -24,7 +24,7 @@ namespace GPUVerify } - public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread) + public Microsoft.Boogie.BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition) { return new BigBlock(Token.NoToken, null, new CmdSeq(), null, null); } diff --git a/Source/GPUVerify/RaceInstrumenter.cs b/Source/GPUVerify/RaceInstrumenter.cs index c73b9b13..71214cb3 100644 --- a/Source/GPUVerify/RaceInstrumenter.cs +++ b/Source/GPUVerify/RaceInstrumenter.cs @@ -473,16 +473,17 @@ namespace GPUVerify { } - public BigBlock MakeResetReadWriteSetStatements(Variable v, int Thread) { + public BigBlock MakeResetReadWriteSetStatements(Variable v, Expr ResetCondition) { BigBlock result = new BigBlock(Token.NoToken, null, new CmdSeq(), null, null); - if (Thread == 2) { - return result; - } - Expr ResetReadAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken, - new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ")))); - Expr ResetWriteAssumeGuard = Expr.Not(new IdentifierExpr(Token.NoToken, - new VariableDualiser(1, null, null).VisitVariable(GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE")))); + Expr ResetReadAssumeGuard = Expr.Imp(ResetCondition, + Expr.Not(new IdentifierExpr(Token.NoToken, + new VariableDualiser(1, null, null).VisitVariable( + GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "READ"))))); + Expr ResetWriteAssumeGuard = Expr.Imp(ResetCondition, + Expr.Not(new IdentifierExpr(Token.NoToken, + new VariableDualiser(1, null, null).VisitVariable( + GPUVerifier.MakeAccessHasOccurredVariable(v.Name, "WRITE"))))); if (verifier.KernelArrayInfo.getGlobalArrays().Contains(v)) { ResetReadAssumeGuard = Expr.Imp(GPUVerifier.ThreadsInSameGroup(), ResetReadAssumeGuard); -- cgit v1.2.3 From 7a895df23fe9260196be1c86bac11486a8d895b2 Mon Sep 17 00:00:00 2001 From: Unknown Date: Fri, 21 Sep 2012 09:51:20 +0100 Subject: Fixed a bug with empty big blocks. --- Source/GPUVerify/GPUVerifier.cs | 33 ++++++++++++++++++++++++--------- 1 file changed, 24 insertions(+), 9 deletions(-) diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 351fe45e..85821da2 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -1423,10 +1423,12 @@ namespace GPUVerify Expr AtLeastOneEnabledWithLocalFence = Expr.Or(Expr.And(P1, LocalFence1), Expr.And(P2, LocalFence2)); - bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(new Cmd[] { }), - new IfCmd(Token.NoToken, - AtLeastOneEnabledWithLocalFence, - new StmtList(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null), null)); + if (SomeArrayModelledNonAdversarially(KernelArrayInfo.getGroupSharedArrays())) { + bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(), + new IfCmd(Token.NoToken, + AtLeastOneEnabledWithLocalFence, + new StmtList(MakeHavocBlocks(KernelArrayInfo.getGroupSharedArrays()), Token.NoToken), null, null), null)); + } } if (KernelArrayInfo.getGlobalArrays().Count > 0) @@ -1440,10 +1442,12 @@ namespace GPUVerify Expr ThreadsInSameGroup_BothEnabled_AtLeastOneGlobalFence = Expr.And(Expr.And(GPUVerifier.ThreadsInSameGroup(), Expr.And(P1, P2)), Expr.Or(GlobalFence1, GlobalFence2)); - bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(new Cmd[] { }), - new IfCmd(Token.NoToken, - ThreadsInSameGroup_BothEnabled_AtLeastOneGlobalFence, - new StmtList(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null), null)); + if (SomeArrayModelledNonAdversarially(KernelArrayInfo.getGlobalArrays())) { + bigblocks.Add(new BigBlock(Token.NoToken, null, new CmdSeq(), + new IfCmd(Token.NoToken, + ThreadsInSameGroup_BothEnabled_AtLeastOneGlobalFence, + new StmtList(MakeHavocBlocks(KernelArrayInfo.getGlobalArrays()), Token.NoToken), null, null), null)); + } } StmtList statements = new StmtList(bigblocks, BarrierProcedure.tok); @@ -1493,8 +1497,19 @@ namespace GPUVerify if (!ArrayModelledAdversarially(v)) { result.Add(HavocSharedArray(v)); } - } + } + Debug.Assert(result.Count > 0); return result; + } + + private bool SomeArrayModelledNonAdversarially(ICollection variables) { + Debug.Assert(variables.Count > 0); + foreach (Variable v in variables) { + if (!ArrayModelledAdversarially(v)) { + return true; + } + } + return false; } public static bool HasZDimension(Variable v) -- cgit v1.2.3