Shared state is now properly abstracted in requires clauses.

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" />