diff options
Diffstat (limited to 'Source/GPUVerify/AdversarialAbstraction.cs')
| -rw-r--r-- | Source/GPUVerify/AdversarialAbstraction.cs | 203 |
1 files changed, 203 insertions, 0 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);
+ }
+
+ }
+
+ }
+
+
+}
|