diff options
| -rw-r--r-- | Source/GPUVerify/AdversarialAbstraction.cs | 203 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerifier.cs | 167 | ||||
| -rw-r--r-- | Source/GPUVerify/GPUVerify.csproj | 1 |
3 files changed, 205 insertions, 166 deletions
diff --git a/Source/GPUVerify/AdversarialAbstraction.cs b/Source/GPUVerify/AdversarialAbstraction.cs new file mode 100644 index 00000000..b6c0ee86 --- /dev/null +++ b/Source/GPUVerify/AdversarialAbstraction.cs @@ -0,0 +1,203 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Diagnostics;
+using Microsoft.Boogie;
+using System.Diagnostics.Contracts;
+
+namespace GPUVerify {
+
+ class AdversarialAbstraction {
+
+ private GPUVerifier verifier;
+
+ internal AdversarialAbstraction(GPUVerifier verifier) {
+ this.verifier = verifier;
+ }
+
+ internal void Abstract() {
+ List<Declaration> NewTopLevelDeclarations = new List<Declaration>();
+ foreach (Declaration d in verifier.Program.TopLevelDeclarations) {
+ if (d is Variable && verifier.KernelArrayInfo.Contains(d as Variable) &&
+ verifier.ArrayModelledAdversarially(d as Variable)) {
+ continue;
+ }
+
+ if (d is Implementation) {
+ Abstract(d as Implementation);
+ }
+
+ if (d is Procedure) {
+ Abstract(d as Procedure);
+ }
+
+ NewTopLevelDeclarations.Add(d);
+
+ }
+
+ verifier.Program.TopLevelDeclarations = NewTopLevelDeclarations;
+
+ AbstractRequiresClauses(verifier.KernelProcedure);
+ }
+
+
+ private void AbstractRequiresClauses(Procedure proc) {
+ RequiresSeq newRequires = new RequiresSeq();
+ foreach (Requires r in proc.Requires) {
+ var visitor = new AccessesAdversarialArrayVisitor(verifier);
+ visitor.VisitRequires(r);
+ if (!visitor.found) {
+ newRequires.Add(r);
+ }
+ }
+ proc.Requires = newRequires;
+ }
+
+ private void Abstract(Procedure proc) {
+ AbstractModifiesSet(proc);
+ }
+
+ private void AbstractModifiesSet(Procedure proc) {
+ IdentifierExprSeq NewModifies = new IdentifierExprSeq();
+ foreach (IdentifierExpr e in proc.Modifies) {
+ var visitor = new AccessesAdversarialArrayVisitor(verifier);
+ visitor.VisitIdentifierExpr(e);
+ if(!visitor.found) {
+ NewModifies.Add(e);
+ }
+ }
+ proc.Modifies = NewModifies;
+ }
+
+ private void Abstract(Implementation impl) {
+ VariableSeq NewLocVars = new VariableSeq();
+
+ foreach (Variable v in impl.LocVars) {
+ Debug.Assert(!verifier.KernelArrayInfo.getGroupSharedArrays().Contains(v));
+ NewLocVars.Add(v);
+ }
+
+ impl.LocVars = NewLocVars;
+
+ if (CommandLineOptions.Unstructured)
+ impl.Blocks = impl.Blocks.Select(Abstract).ToList();
+ else
+ impl.StructuredStmts = Abstract(impl.StructuredStmts);
+ }
+
+
+ private StmtList Abstract(StmtList stmtList) {
+ Contract.Requires(stmtList != null);
+
+ StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
+
+ foreach (BigBlock bodyBlock in stmtList.BigBlocks) {
+ result.BigBlocks.Add(Abstract(bodyBlock));
+ }
+ return result;
+ }
+
+ private CmdSeq Abstract(CmdSeq cs) {
+ var result = new CmdSeq();
+
+ foreach (Cmd c in cs) {
+ if (c is AssignCmd) {
+ AssignCmd assign = c as AssignCmd;
+
+ var lhss = new List<AssignLhs>();
+ var rhss = new List<Expr>();
+
+ for (int i = 0; i != assign.Lhss.Count; i++) {
+ AssignLhs lhs = assign.Lhss[i];
+ Expr rhs = assign.Rhss[i];
+ ReadCollector rc = new ReadCollector(verifier.KernelArrayInfo);
+ rc.Visit(rhs);
+
+ bool foundAdversarial = false;
+ foreach (AccessRecord ar in rc.accesses) {
+ if (verifier.ArrayModelledAdversarially(ar.v)) {
+ foundAdversarial = true;
+ break;
+ }
+ }
+
+ if (foundAdversarial) {
+ Debug.Assert(lhs is SimpleAssignLhs);
+ result.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));
+ continue;
+ }
+
+ WriteCollector wc = new WriteCollector(verifier.KernelArrayInfo);
+ wc.Visit(lhs);
+ if (wc.GetAccess() != null && verifier.ArrayModelledAdversarially(wc.GetAccess().v)) {
+ continue; // Just remove the write
+ }
+
+ lhss.Add(lhs);
+ rhss.Add(rhs);
+ }
+
+ if (lhss.Count != 0) {
+ result.Add(new AssignCmd(assign.tok, lhss, rhss));
+ }
+ continue;
+ }
+ result.Add(c);
+ }
+
+ return result;
+ }
+
+ private Block Abstract(Block b) {
+ b.Cmds = Abstract(b.Cmds);
+ return b;
+ }
+
+ private BigBlock Abstract(BigBlock bb) {
+ BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
+
+ result.simpleCmds = Abstract(bb.simpleCmds);
+
+ if (bb.ec is WhileCmd) {
+ WhileCmd WhileCommand = bb.ec as WhileCmd;
+ result.ec =
+ new WhileCmd(WhileCommand.tok, WhileCommand.Guard, WhileCommand.Invariants, Abstract(WhileCommand.Body));
+ }
+ else if (bb.ec is IfCmd) {
+ IfCmd IfCommand = bb.ec as IfCmd;
+ Debug.Assert(IfCommand.elseIf == null);
+ result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, Abstract(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? Abstract(IfCommand.elseBlock) : null);
+ }
+ else {
+ Debug.Assert(bb.ec == null || bb.ec is BreakCmd);
+ }
+
+ return result;
+
+ }
+
+ class AccessesAdversarialArrayVisitor : StandardVisitor {
+ internal bool found;
+ private GPUVerifier verifier;
+
+ internal AccessesAdversarialArrayVisitor(GPUVerifier verifier) {
+ this.found = false;
+ this.verifier = verifier;
+ }
+
+ public override Variable VisitVariable(Variable v) {
+ if (verifier.KernelArrayInfo.Contains(v)) {
+ if (verifier.ArrayModelledAdversarially(v)) {
+ found = true;
+ }
+ }
+ return base.VisitVariable(v);
+ }
+
+ }
+
+ }
+
+
+}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs index 409ea837..b3a7dcdc 100644 --- a/Source/GPUVerify/GPUVerifier.cs +++ b/Source/GPUVerify/GPUVerifier.cs @@ -1503,172 +1503,7 @@ namespace GPUVerify private void AbstractSharedState()
{
- List<Declaration> NewTopLevelDeclarations = new List<Declaration>();
-
- foreach (Declaration d in Program.TopLevelDeclarations)
- {
- if (d is Variable && KernelArrayInfo.Contains(d as Variable) && ArrayModelledAdversarially(d as Variable))
- {
- continue;
- }
-
- if (d is Implementation)
- {
- PerformFullSharedStateAbstraction(d as Implementation);
- }
-
- if (d is Procedure)
- {
- PerformFullSharedStateAbstraction(d as Procedure);
- }
-
- NewTopLevelDeclarations.Add(d);
-
- }
-
- Program.TopLevelDeclarations = NewTopLevelDeclarations;
-
- }
-
- private void PerformFullSharedStateAbstraction(Procedure proc)
- {
- IdentifierExprSeq NewModifies = new IdentifierExprSeq();
-
- foreach (IdentifierExpr e in proc.Modifies)
- {
- if (!KernelArrayInfo.Contains(e.Decl) || !ArrayModelledAdversarially(e.Decl))
- {
- NewModifies.Add(e);
- }
- }
-
- proc.Modifies = NewModifies;
-
- }
-
- private void PerformFullSharedStateAbstraction(Implementation impl)
- {
- VariableSeq NewLocVars = new VariableSeq();
-
- foreach (Variable v in impl.LocVars)
- {
- Debug.Assert(!KernelArrayInfo.getGroupSharedArrays().Contains(v));
- NewLocVars.Add(v);
- }
-
- impl.LocVars = NewLocVars;
-
- if (CommandLineOptions.Unstructured)
- impl.Blocks = impl.Blocks.Select(PerformFullSharedStateAbstraction).ToList();
- else
- impl.StructuredStmts = PerformFullSharedStateAbstraction(impl.StructuredStmts);
- }
-
-
- private StmtList PerformFullSharedStateAbstraction(StmtList stmtList)
- {
- Contract.Requires(stmtList != null);
-
- StmtList result = new StmtList(new List<BigBlock>(), stmtList.EndCurly);
-
- foreach (BigBlock bodyBlock in stmtList.BigBlocks)
- {
- result.BigBlocks.Add(PerformFullSharedStateAbstraction(bodyBlock));
- }
- return result;
- }
-
- private CmdSeq PerformFullSharedStateAbstraction(CmdSeq cs)
- {
- var result = new CmdSeq();
-
- foreach (Cmd c in cs)
- {
- if (c is AssignCmd)
- {
- AssignCmd assign = c as AssignCmd;
-
- var lhss = new List<AssignLhs>();
- var rhss = new List<Expr>();
-
- for (int i = 0; i != assign.Lhss.Count; i++)
- {
- AssignLhs lhs = assign.Lhss[i];
- Expr rhs = assign.Rhss[i];
- ReadCollector rc = new ReadCollector(KernelArrayInfo);
- rc.Visit(rhs);
-
- bool foundAdversarial = false;
- foreach (AccessRecord ar in rc.accesses)
- {
- if (ArrayModelledAdversarially(ar.v))
- {
- foundAdversarial = true;
- break;
- }
- }
-
- if (foundAdversarial)
- {
- Debug.Assert(lhs is SimpleAssignLhs);
- result.Add(new HavocCmd(c.tok, new IdentifierExprSeq(new IdentifierExpr[] { (lhs as SimpleAssignLhs).AssignedVariable })));
- continue;
- }
-
- WriteCollector wc = new WriteCollector(KernelArrayInfo);
- wc.Visit(lhs);
- if (wc.GetAccess() != null && ArrayModelledAdversarially(wc.GetAccess().v))
- {
- continue; // Just remove the write
- }
-
- lhss.Add(lhs);
- rhss.Add(rhs);
- }
-
- if (lhss.Count != 0)
- {
- result.Add(new AssignCmd(assign.tok, lhss, rhss));
- }
- continue;
- }
- result.Add(c);
- }
-
- return result;
- }
-
- private Block PerformFullSharedStateAbstraction(Block b)
- {
- b.Cmds = PerformFullSharedStateAbstraction(b.Cmds);
- return b;
- }
-
- private BigBlock PerformFullSharedStateAbstraction(BigBlock bb)
- {
- BigBlock result = new BigBlock(bb.tok, bb.LabelName, new CmdSeq(), null, bb.tc);
-
- result.simpleCmds = PerformFullSharedStateAbstraction(bb.simpleCmds);
-
- if (bb.ec is WhileCmd)
- {
- WhileCmd WhileCommand = bb.ec as WhileCmd;
- result.ec =
- new WhileCmd(WhileCommand.tok, WhileCommand.Guard, WhileCommand.Invariants, PerformFullSharedStateAbstraction(WhileCommand.Body));
- }
- else if (bb.ec is IfCmd)
- {
- IfCmd IfCommand = bb.ec as IfCmd;
- Debug.Assert(IfCommand.elseIf == null);
- result.ec = new IfCmd(IfCommand.tok, IfCommand.Guard, PerformFullSharedStateAbstraction(IfCommand.thn), IfCommand.elseIf, IfCommand.elseBlock != null ? PerformFullSharedStateAbstraction(IfCommand.elseBlock) : null);
- }
- else
- {
- Debug.Assert(bb.ec == null || bb.ec is BreakCmd);
- }
-
- return result;
-
+ new AdversarialAbstraction(this).Abstract();
}
internal static string MakeOffsetVariableName(string Name, string AccessType)
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj index 47965b43..08913944 100644 --- a/Source/GPUVerify/GPUVerify.csproj +++ b/Source/GPUVerify/GPUVerify.csproj @@ -105,6 +105,7 @@ <ItemGroup>
<Compile Include="AccessCollector.cs" />
<Compile Include="AccessRecord.cs" />
+ <Compile Include="AdversarialAbstraction.cs" />
<Compile Include="ArrayControlFlowAnalyser.cs" />
<Compile Include="AsymmetricExpressionFinder.cs" />
<Compile Include="StrideConstraint.cs" />
|