Support for access annotations.

1 files changed, 187 insertions, 15 deletions

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;