Merge

6 files changed, 314 insertions, 19 deletions

diff --git a/Source/GPUVerify/AccessInvariantProcessor.cs b/Source/GPUVerify/AccessInvariantProcessor.cs
new file mode 100644
index 00000000..fbbfda79
--- /dev/null
+++ b/Source/GPUVerify/AccessInvariantProcessor.cs
@@ -0,0 +1,94 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    class AccessInvariantProcessor : StandardVisitor

+    {

+

+        private const string NO_READ = "__no_read_";

+        private const string NO_WRITE = "__no_write_";

+        private const string READ_OFFSET = "__read_offset_";

+        private const string WRITE_OFFSET = "__write_offset_";

+        private const string READ_IMPLIES = "__read_implies_";

+        private const string WRITE_IMPLIES = "__write_implies_";

+

+        public override Expr VisitNAryExpr(NAryExpr node)

+        {

+

+            if (node.Fun is FunctionCall)

+            {

+                FunctionCall call = node.Fun as FunctionCall;

+

+                if (MatchesIntrinsic(call.Func, NO_READ))

+                {

+                    return Expr.Not(

+                        MakeReadHasOccurred(node, call)

+                    );

+                }

+

+                if (MatchesIntrinsic(call.Func, NO_WRITE))

+                {

+                    return Expr.Not(

+                        MakeWriteHasOccurred(node, call)

+                    );

+                }

+

+                if (MatchesIntrinsic(call.Func, READ_OFFSET))

+                {

+                    return new IdentifierExpr(node.tok, new GlobalVariable(

+                            node.tok, new TypedIdent(node.tok, "_READ_OFFSET_X_" +

+                                call.Func.Name.Substring(READ_OFFSET.Length), Microsoft.Boogie.Type.GetBvType(32)))

+                    );

+                }

+

+                if (MatchesIntrinsic(call.Func, WRITE_OFFSET))

+                {

+                    return new IdentifierExpr(node.tok, new GlobalVariable(

+                            node.tok, new TypedIdent(node.tok, "_WRITE_OFFSET_X_" +

+                                call.Func.Name.Substring(WRITE_OFFSET.Length), Microsoft.Boogie.Type.GetBvType(32)))

+                    );

+                }

+

+                if (MatchesIntrinsic(call.Func, READ_IMPLIES))

+                {

+                    return Expr.Imp(MakeReadHasOccurred(node, call), node.Args[0]);

+                }

+

+                if (MatchesIntrinsic(call.Func, WRITE_IMPLIES))

+                {

+                    return Expr.Imp(MakeWriteHasOccurred(node, call), node.Args[0]);

+                }

+

+            }

+

+            return base.VisitNAryExpr(node);

+        }

+

+        private static IdentifierExpr MakeReadHasOccurred(NAryExpr node, FunctionCall call)

+        {

+            return new IdentifierExpr(node.tok, new GlobalVariable(

+                                        node.tok, new TypedIdent(node.tok, "_READ_HAS_OCCURRED_" +

+                                            call.Func.Name.Substring(NO_READ.Length), Microsoft.Boogie.Type.Bool)));

+        }

+

+        private static IdentifierExpr MakeWriteHasOccurred(NAryExpr node, FunctionCall call)

+        {

+            return new IdentifierExpr(node.tok, new GlobalVariable(

+                                        node.tok, new TypedIdent(node.tok, "_WRITE_HAS_OCCURRED_" +

+                                            call.Func.Name.Substring(NO_WRITE.Length), Microsoft.Boogie.Type.Bool)));

+        }

+

+

+        private bool MatchesIntrinsic(Function function, string intrinsicPrefix)

+        {

+            return function.Name.Length > intrinsicPrefix.Length &&

+                function.Name.Substring(0, intrinsicPrefix.Length).Equals(intrinsicPrefix);

+        }

+    

+    

+    }

+}

diff --git a/Source/GPUVerify/AsymmetricExpressionFinder.cs b/Source/GPUVerify/AsymmetricExpressionFinder.cs
new file mode 100644
index 00000000..40c7eb32
--- /dev/null
+++ b/Source/GPUVerify/AsymmetricExpressionFinder.cs
@@ -0,0 +1,29 @@
+using System;

+using System.Collections.Generic;

+using System.Linq;

+using System.Text;

+using Microsoft.Boogie;

+

+namespace GPUVerify

+{

+    class AsymmetricExpressionFinder : StandardVisitor

+    {

+        private bool found = false;

+

+        internal bool foundAsymmetricExpr()

+        {

+            return found;

+        }

+

+        public override Variable VisitVariable(Variable node)

+        {

+            if (node.TypedIdent.Name.Contains("_READ_HAS_OCCURRED") ||

+                node.TypedIdent.Name.Contains("_READ_OFFSET"))

+            {

+                found = true;

+            }

+            return node;

+        }

+

+    }

+}

diff --git a/Source/GPUVerify/CrossThreadInvariantProcessor.cs b/Source/GPUVerify/CrossThreadInvariantProcessor.cs
index b5772c0c..16416e11 100644
--- a/Source/GPUVerify/CrossThreadInvariantProcessor.cs
+++ b/Source/GPUVerify/CrossThreadInvariantProcessor.cs
@@ -19,10 +19,8 @@ namespace GPUVerify
 

                 if (call.Func.Name.Equals("__uniform_bv32") || call.Func.Name.Equals("__uniform_bool"))

                 {

-                    return Expr.True;

-/*                    Debug.Assert(false);

                     return Expr.Eq(new VariableDualiser(1).VisitExpr(node.Args[0].Clone() as Expr),

-                                   new VariableDualiser(2).VisitExpr(node.Args[0].Clone() as Expr));*/

+                                   new VariableDualiser(2).VisitExpr(node.Args[0].Clone() as Expr));

                 }

 

                 if (call.Func.Name.Equals("__distinct_bv32") || call.Func.Name.Equals("__distinct_bool"))

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 7432c823..632777c9 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -310,6 +310,8 @@ namespace GPUVerify
                 return;

             }

 

+            ProcessAccessInvariants();

+

             if (CommandLineOptions.ShowStages)

             {

                 emitProgram(outputFilename + "_instrumented");

@@ -406,35 +408,146 @@ namespace GPUVerify
 

         }

 

-        private void ProcessCrossThreadInvariants()

+        private void ProcessAccessInvariants()

         {

             foreach (Declaration d in Program.TopLevelDeclarations)

             {

                 if (d is Procedure)

                 {

-                    // TODO: requires and ensures

+                    Procedure p = d as Procedure;

+                    p.Requires = ProcessAccessInvariants(p.Requires);

+                    p.Ensures = ProcessAccessInvariants(p.Ensures);

                 }

+

                 if (d is Implementation)

                 {

                     Implementation i = d as Implementation;

-                    List<Block> newBlocks = new List<Block>();

-                    foreach (Block b in i.Blocks)

-                    {

-                        Console.WriteLine("Before");

-                        Console.WriteLine(b.Cmds);

-                        Block newBlock = new CrossThreadInvariantProcessor().VisitBlock(b);

-                        Console.WriteLine("After");

-                        Console.WriteLine(newBlock.Cmds);

+                    ProcessAccessInvariants(i.StructuredStmts);

+                }

+            }

+        }

 

+        private void ProcessAccessInvariants(StmtList stmtList)

+        {

+            

+            foreach (BigBlock bb in stmtList.BigBlocks)

+            {

+                ProcessAccessInvariants(bb);

+            }

+        }

 

-                        newBlocks.Add(newBlock);

-                    }

-                    i.Blocks = newBlocks;

+        private void ProcessAccessInvariants(BigBlock bb)

+        {

+            if (bb.ec is WhileCmd)

+            {

+                WhileCmd whileCmd = bb.ec as WhileCmd;

+                whileCmd.Invariants = ProcessAccessInvariants(whileCmd.Invariants);

+                ProcessAccessInvariants(whileCmd.Body);

+            }

+            else if (bb.ec is IfCmd)

+            {

+                ProcessAccessInvariants((bb.ec as IfCmd).thn);

+                if ((bb.ec as IfCmd).elseBlock != null)

+                {

+                    ProcessAccessInvariants((bb.ec as IfCmd).elseBlock);

+                }

+            }

+        }

+

+        private List<PredicateCmd> ProcessAccessInvariants(List<PredicateCmd> invariants)

+        {

+            List<PredicateCmd> result = new List<PredicateCmd>();

+

+            foreach (PredicateCmd p in invariants)

+            {

+                result.Add(new AssertCmd(p.tok, new AccessInvariantProcessor().VisitExpr(p.Expr.Clone() as Expr)));

+            }

+

+            return result;

+        }

+

+        private EnsuresSeq ProcessAccessInvariants(EnsuresSeq ensuresSeq)

+        {

+            EnsuresSeq result = new EnsuresSeq();

+            foreach (Ensures e in ensuresSeq)

+            {

+                result.Add(new Ensures(e.Free, new AccessInvariantProcessor().VisitExpr(e.Condition.Clone() as Expr)));

+            }

+            return result;

+        }

+

+        private RequiresSeq ProcessAccessInvariants(RequiresSeq requiresSeq)

+        {

+            RequiresSeq result = new RequiresSeq();

+            foreach (Requires r in requiresSeq)

+            {

+                result.Add(new Requires(r.Free, new AccessInvariantProcessor().VisitExpr(r.Condition.Clone() as Expr)));

+            }

+            return result;

+        }

+

+        private void ProcessCrossThreadInvariants()

+        {

+            foreach (Declaration d in Program.TopLevelDeclarations)

+            {

+                if (d is Procedure)

+                {

+                    Procedure p = d as Procedure;

+                    p.Requires = ProcessCrossThreadInvariants(p.Requires);

+                    p.Ensures = ProcessCrossThreadInvariants(p.Ensures);

+                }

+                if (d is Implementation)

+                {

+                    Implementation i = d as Implementation;

+                    ProcessCrossThreadInvariants(i.StructuredStmts);

                 }

 

             }

         }

 

+        private EnsuresSeq ProcessCrossThreadInvariants(EnsuresSeq ensuresSeq)

+        {

+            EnsuresSeq result = new EnsuresSeq();

+            foreach (Ensures e in ensuresSeq)

+            {

+                result.Add(new Ensures(e.Free, new CrossThreadInvariantProcessor().VisitExpr(e.Condition.Clone() as Expr)));

+            }

+            return result;

+        }

+

+        private RequiresSeq ProcessCrossThreadInvariants(RequiresSeq requiresSeq)

+        {

+            RequiresSeq result = new RequiresSeq();

+            foreach (Requires r in requiresSeq)

+            {

+                result.Add(new Requires(r.Free, new CrossThreadInvariantProcessor().VisitExpr(r.Condition.Clone() as Expr)));

+            }

+            return result;

+        }

+

+        private void ProcessCrossThreadInvariants(StmtList stmtList)

+        {

+            foreach (BigBlock bb in stmtList.BigBlocks)

+            {

+                ProcessCrossThreadInvariants(bb);

+            }

+        }

+

+        private void ProcessCrossThreadInvariants(BigBlock bb)

+        {

+            if (bb.ec is WhileCmd)

+            {

+                WhileCmd whileCmd = bb.ec as WhileCmd;

+                List<PredicateCmd> newInvariants = new List<PredicateCmd>();

+                foreach(PredicateCmd p in whileCmd.Invariants)

+                {

+                    newInvariants.Add(new AssertCmd(p.tok, new CrossThreadInvariantProcessor().VisitExpr(p.Expr)));

+                }

+                whileCmd.Invariants = newInvariants;

+                ProcessCrossThreadInvariants(whileCmd.Body);

+            }

+        }

+

         private void emitProgram(string filename)

         {

             using (TokenTextWriter writer = new TokenTextWriter(filename + ".bpl"))

@@ -1924,6 +2037,9 @@ namespace GPUVerify
 

                     bool HalfDualise = HalfDualisedProcedureNames.Contains(proc.Name);

 

+                    proc.Requires = DualiseRequires(proc.Requires);

+                    proc.Ensures = DualiseEnsures(proc.Ensures);

+

                     proc.InParams = DualiseVariableSequence(proc.InParams, HalfDualise);

                     proc.OutParams = DualiseVariableSequence(proc.OutParams, HalfDualise);

                     IdentifierExprSeq NewModifies = new IdentifierExprSeq();

@@ -1988,6 +2104,42 @@ namespace GPUVerify
 

         }

 

+        private EnsuresSeq DualiseEnsures(EnsuresSeq ensuresSeq)

+        {

+            EnsuresSeq newEnsures = new EnsuresSeq();

+            foreach (Ensures e in ensuresSeq)

+            {

+                newEnsures.Add(new Ensures(e.Free, new VariableDualiser(1).VisitExpr(e.Condition.Clone() as Expr)));

+                if (!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(e.Condition))

+                {

+                    newEnsures.Add(new Ensures(e.Free, new VariableDualiser(2).VisitExpr(e.Condition.Clone() as Expr)));

+                }

+            }

+            return newEnsures;

+        }

+

+        private RequiresSeq DualiseRequires(RequiresSeq requiresSeq)

+        {

+            RequiresSeq newRequires = new RequiresSeq();

+            foreach (Requires r in requiresSeq)

+            {

+                newRequires.Add(new Requires(r.Free, new VariableDualiser(1).VisitExpr(r.Condition.Clone() as Expr)));

+

+                if (!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(r.Condition))

+                {

+                    newRequires.Add(new Requires(r.Free, new VariableDualiser(2).VisitExpr(r.Condition.Clone() as Expr)));

+                }

+            }

+            return newRequires;

+        }

+

+        private bool ContainsAsymmetricExpression(Expr expr)

+        {

+            AsymmetricExpressionFinder finder = new AsymmetricExpressionFinder();

+            finder.VisitExpr(expr);

+            return finder.foundAsymmetricExpr();

+        }

+

         private static VariableSeq DualiseVariableSequence(VariableSeq seq, bool HalfDualise)

         {

             VariableSeq result = new VariableSeq();

@@ -2017,12 +2169,29 @@ namespace GPUVerify
                         // Add predicate to start of parameter list

                         Procedure proc = d as Procedure;

                         VariableSeq NewIns = new VariableSeq();

-                        NewIns.Add(new LocalVariable(proc.tok, new TypedIdent(proc.tok, "_P", Microsoft.Boogie.Type.Bool)));

+                        TypedIdent enabled = new TypedIdent(proc.tok, "_P", Microsoft.Boogie.Type.Bool);

+                        NewIns.Add(new LocalVariable(proc.tok, enabled));

                         foreach (Variable v in proc.InParams)

                         {

                             NewIns.Add(v);

                         }

                         proc.InParams = NewIns;

+

+                        RequiresSeq newRequires = new RequiresSeq();

+                        foreach (Requires r in proc.Requires)

+                        {

+                            newRequires.Add(new Requires(r.Free, Predicator.ProcessEnabledIntrinsics(r.Condition, enabled)));

+                        }

+                        proc.Requires = newRequires;

+

+                        EnsuresSeq newEnsures = new EnsuresSeq();

+                        foreach (Ensures e in proc.Ensures)

+                        {

+                            newEnsures.Add(new Ensures(e.Free, Predicator.ProcessEnabledIntrinsics(e.Condition, enabled)));

+                        }

+                        proc.Ensures = newEnsures;

+

+

                     }

 

                 }

@@ -2195,7 +2364,10 @@ namespace GPUVerify
             foreach(PredicateCmd p in originalInvariants)

             {

                 result.Add(new AssertCmd(p.tok, new VariableDualiser(1).VisitExpr(p.Expr.Clone() as Expr)));

-                result.Add(new AssertCmd(p.tok, new VariableDualiser(2).VisitExpr(p.Expr.Clone() as Expr)));

+                if (!CommandLineOptions.Symmetry || !ContainsAsymmetricExpression(p.Expr))

+                {

+                    result.Add(new AssertCmd(p.tok, new VariableDualiser(2).VisitExpr(p.Expr.Clone() as Expr)));

+                }

             }

 

             return result;

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 204ffabe..99cbf0cd 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -104,7 +104,9 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="AccessCollector.cs" />

+    <Compile Include="AccessInvariantProcessor.cs" />

     <Compile Include="AccessRecord.cs" />

+    <Compile Include="AsymmetricExpressionFinder.cs" />

     <Compile Include="CrossThreadInvariantProcessor.cs" />

     <Compile Include="EnabledToPredicateVisitor.cs" />

     <Compile Include="CommandLineOptions.cs" />

diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs
index 1ade15c9..7b4f7982 100644
--- a/Source/GPUVerify/Predicator.cs
+++ b/Source/GPUVerify/Predicator.cs
@@ -258,7 +258,7 @@ namespace GPUVerify
             return result;

         }

 

-        private Expr ProcessEnabledIntrinsics(Expr expr, TypedIdent currentPredicate)

+        internal static Expr ProcessEnabledIntrinsics(Expr expr, TypedIdent currentPredicate)

         {

             return new EnabledToPredicateVisitor(currentPredicate).VisitExpr(expr);

         }