Merge

6 files changed, 106 insertions, 62 deletions

diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs
index c4b5d7a9..9df982d9 100644
--- a/Source/Core/Absy.cs
+++ b/Source/Core/Absy.cs
@@ -911,6 +911,25 @@ namespace Microsoft.Boogie {
       }

       return globals;

     }

+

+    private int invariantGenerationCounter = 0;

+

+    public Constant MakeExistentialBoolean() {

+      Constant ExistentialBooleanConstant = new Constant(Token.NoToken, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false);

+      invariantGenerationCounter++;

+      ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });

+      TopLevelDeclarations.Add(ExistentialBooleanConstant);

+      return ExistentialBooleanConstant;

+    }

+

+    public PredicateCmd CreateCandidateInvariant(Expr e, string tag = null) {

+      Constant ExistentialBooleanConstant = MakeExistentialBoolean();

+      IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);

+      PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));

+      if (tag != null)

+        invariant.Attributes = new QKeyValue(Token.NoToken, "tag", new List<object>(new object[] { tag }), null);

+      return invariant;

+    }

   }

 

   //---------------------------------------------------------------------

diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 1839b138..40e27310 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -25,7 +25,6 @@ namespace GPUVerify
         private HashSet<string> ReservedNames = new HashSet<string>();

 

         private int TempCounter = 0;

-        private int invariantGenerationCounter = 0;

 

         internal const string LOCAL_ID_X_STRING = "local_id_x";

         internal const string LOCAL_ID_Y_STRING = "local_id_y";

@@ -815,18 +814,16 @@ namespace GPUVerify
 

         internal void AddCandidateRequires(Procedure Proc, Expr e)

         {

-            Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);

+            Constant ExistentialBooleanConstant = Program.MakeExistentialBoolean();

             IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);

             Proc.Requires.Add(new Requires(false, Expr.Imp(ExistentialBoolean, e)));

-            Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);

         }

 

         internal void AddCandidateEnsures(Procedure Proc, Expr e)

         {

-            Constant ExistentialBooleanConstant = MakeExistentialBoolean(Proc.tok);

+            Constant ExistentialBooleanConstant = Program.MakeExistentialBoolean();

             IdentifierExpr ExistentialBoolean = new IdentifierExpr(Proc.tok, ExistentialBooleanConstant);

             Proc.Ensures.Add(new Ensures(false, Expr.Imp(ExistentialBoolean, e)));

-            Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);

         }

 

         private List<Expr> GetUserSuppliedInvariants(string ProcedureName)

@@ -1043,14 +1040,6 @@ namespace GPUVerify
             return _GROUP_SIZE_Z != null;

         }

 

-        internal Constant MakeExistentialBoolean(IToken tok)

-        {

-            Constant ExistentialBooleanConstant = new Constant(tok, new TypedIdent(tok, "_b" + invariantGenerationCounter, Microsoft.Boogie.Type.Bool), false);

-            invariantGenerationCounter++;

-            ExistentialBooleanConstant.AddAttribute("existential", new object[] { Expr.True });

-            return ExistentialBooleanConstant;

-        }

-

         internal static string StripThreadIdentifier(string p)

         {

             if (p.Contains("$"))

@@ -2153,7 +2142,7 @@ namespace GPUVerify
         {

             if (CommandLineOptions.Unstructured)

             {

-                BlockPredicator.Predicate(this, Program);

+                BlockPredicator.Predicate(Program, /*createCandidateInvariants=*/CommandLineOptions.Inference);

                 return;

             }

 

@@ -2257,19 +2246,9 @@ namespace GPUVerify
 

         internal void AddCandidateInvariant(IRegion region, Expr e, string tag)

         {

-            region.AddInvariant(CreateCandidateInvariant(e, tag));

+            region.AddInvariant(Program.CreateCandidateInvariant(e, tag));

         }

 

-        internal PredicateCmd CreateCandidateInvariant(Expr e, string tag)

-        {

-            Constant ExistentialBooleanConstant = MakeExistentialBoolean(Token.NoToken);

-            IdentifierExpr ExistentialBoolean = new IdentifierExpr(Token.NoToken, ExistentialBooleanConstant);

-            PredicateCmd invariant = new AssertCmd(Token.NoToken, Expr.Imp(ExistentialBoolean, e));

-            invariant.Attributes = new QKeyValue(Token.NoToken, "tag", new List<object>(new object[] { tag }), null);

-            Program.TopLevelDeclarations.Add(ExistentialBooleanConstant);

-            return invariant;

-        }

-            

         internal Implementation GetImplementation(string procedureName)

         {

             foreach (Declaration D in Program.TopLevelDeclarations)

diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 0c87587f..eba91cd2 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -108,10 +108,8 @@
     <Compile Include="AccessRecord.cs" />

     <Compile Include="ArrayControlFlowAnalyser.cs" />

     <Compile Include="AsymmetricExpressionFinder.cs" />

-    <Compile Include="BlockPredicator.cs" />

     <Compile Include="UnstructuredRegion.cs" />

     <Compile Include="IRegion.cs" />

-    <Compile Include="GraphAlgorithms.cs" />

     <Compile Include="InvariantGenerationRules\LoopVariableBoundsInvariantGenerator.cs" />

     <Compile Include="InvariantGenerationRules\InvariantGenerationRule.cs" />

     <Compile Include="InvariantGenerationRules\PowerOfTwoInvariantGenerator.cs" />

@@ -170,6 +168,10 @@
       <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

       <Name>ParserHelper</Name>

     </ProjectReference>

+    <ProjectReference Include="..\VCGeneration\VCGeneration.csproj">

+      <Project>{E1F10180-C7B9-4147-B51F-FA1B701966DC}</Project>

+      <Name>VCGeneration</Name>

+    </ProjectReference>

   </ItemGroup>

   <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

   <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

diff --git a/Source/GPUVerify/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs
index a006bde6..f4e82182 100644
--- a/Source/GPUVerify/BlockPredicator.cs
+++ b/Source/VCGeneration/BlockPredicator.cs
@@ -1,19 +1,21 @@
 using Graphing;
-using Microsoft.Boogie;
 using System;
 using System.Collections.Generic;
+using System.Diagnostics;
 using System.Diagnostics.Contracts;
 using System.Linq;
 
-namespace GPUVerify {
+namespace Microsoft.Boogie {
 
-class BlockPredicator {
+public class BlockPredicator {
 
-  GPUVerifier verifier;
   Program prog;
   Implementation impl;
   Graph<Block> blockGraph;
 
+  bool createCandidateInvariants = true;
+  bool useProcedurePredicates = true;
+
   Expr returnBlockId;
 
   LocalVariable curVar, pVar;
@@ -24,10 +26,39 @@ class BlockPredicator {
   Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
   HashSet<Block> doneBlocks = new HashSet<Block>();
 
-  BlockPredicator(GPUVerifier v, Program p, Implementation i) {
-    verifier = v;
+  BlockPredicator(Program p, Implementation i, bool cci, bool upp) {
     prog = p;
     impl = i;
+    createCandidateInvariants = cci;
+    useProcedurePredicates = upp;
+  }
+
+  void PredicateCmd(List<Block> blocks, Block block, Cmd cmd, out Block nextBlock) {
+    if (!useProcedurePredicates && cmd is CallCmd) {
+      var trueBlock = new Block();
+      blocks.Add(trueBlock);
+      trueBlock.Label = block.Label + ".call.true";
+      trueBlock.Cmds.Add(new AssumeCmd(Token.NoToken, p));
+      trueBlock.Cmds.Add(cmd);
+
+      var falseBlock = new Block();
+      blocks.Add(falseBlock);
+      falseBlock.Label = block.Label + ".call.false";
+      falseBlock.Cmds.Add(new AssumeCmd(Token.NoToken, Expr.Not(p)));
+
+      var contBlock = new Block();
+      blocks.Add(contBlock);
+      contBlock.Label = block.Label + ".call.cont";
+
+      block.TransferCmd =
+        new GotoCmd(Token.NoToken, new BlockSeq(trueBlock, falseBlock));
+      trueBlock.TransferCmd = falseBlock.TransferCmd =
+        new GotoCmd(Token.NoToken, new BlockSeq(contBlock));
+      nextBlock = contBlock;
+    } else {
+      PredicateCmd(block.Cmds, cmd);
+      nextBlock = block;
+    }
   }
 
   void PredicateCmd(CmdSeq cmdSeq, Cmd cmd) {
@@ -79,6 +110,7 @@ class BlockPredicator {
                                       new ExprSeq(p, havocTempExpr, v))));
       }
     } else if (cmd is CallCmd) {
+      Debug.Assert(useProcedurePredicates);
       var cCmd = (CallCmd)cmd;
       cCmd.Ins.Insert(0, p);
       cmdSeq.Add(cCmd);
@@ -145,16 +177,16 @@ class BlockPredicator {
     impl.LocVars.Add(pVar);
     p = Expr.Ident(pVar);
 
+    if (useProcedurePredicates)
+      fp = Expr.Ident(impl.InParams[0]);
+
     var newBlocks = new List<Block>();
 
-    fp = Expr.Ident(impl.InParams[0]);
     Block entryBlock = new Block();
     entryBlock.Label = "entry";
     entryBlock.Cmds = new CmdSeq(Cmd.SimpleAssign(Token.NoToken, cur,
-                        new NAryExpr(Token.NoToken,
-                          new IfThenElse(Token.NoToken),
-                          new ExprSeq(fp, blockIds[sortedBlocks[0].Item1],
-                                      returnBlockId))));
+                        CreateIfFPThenElse(blockIds[sortedBlocks[0].Item1],
+                                           returnBlockId)));
     newBlocks.Add(entryBlock);
 
     var prevBlock = entryBlock;
@@ -182,22 +214,23 @@ class BlockPredicator {
         prevBlock = tailBlock;
       } else {
         var runBlock = n.Item1;
+        var oldCmdSeq = runBlock.Cmds;
+        runBlock.Cmds = new CmdSeq();
         newBlocks.Add(runBlock);
+        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
+                                            new BlockSeq(runBlock));
 
         pExpr = Expr.Eq(cur, blockIds[runBlock]);
-        CmdSeq newCmdSeq = new CmdSeq();
-        if (CommandLineOptions.Inference && blockGraph.Headers.Contains(runBlock)) {
-          AddUniformCandidateInvariant(newCmdSeq, runBlock);
-          AddNonUniformCandidateInvariant(newCmdSeq, runBlock);
+        if (createCandidateInvariants && blockGraph.Headers.Contains(runBlock)) {
+          AddUniformCandidateInvariant(runBlock.Cmds, runBlock);
+          AddNonUniformCandidateInvariant(runBlock.Cmds, runBlock);
         }
-        newCmdSeq.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr));
-        foreach (Cmd cmd in runBlock.Cmds)
-          PredicateCmd(newCmdSeq, cmd);
-        PredicateTransferCmd(newCmdSeq, runBlock.TransferCmd);
-        runBlock.Cmds = newCmdSeq;
+        runBlock.Cmds.Add(Cmd.SimpleAssign(Token.NoToken, p, pExpr));
+        var transferCmd = runBlock.TransferCmd;
+        foreach (Cmd cmd in oldCmdSeq)
+          PredicateCmd(newBlocks, runBlock, cmd, out runBlock);
+        PredicateTransferCmd(runBlock.Cmds, transferCmd);
 
-        prevBlock.TransferCmd = new GotoCmd(Token.NoToken,
-                                            new BlockSeq(runBlock));
         prevBlock = runBlock;
         doneBlocks.Add(runBlock);
       }
@@ -207,12 +240,20 @@ class BlockPredicator {
     impl.Blocks = newBlocks;
   }
 
-  private void AddUniformCandidateInvariant(CmdSeq cs, Block header) {
-    cs.Add(verifier.CreateCandidateInvariant(Expr.Eq(cur,
-            new NAryExpr(Token.NoToken,
+  private Expr CreateIfFPThenElse(Expr then, Expr eElse) {
+    if (useProcedurePredicates) {
+      return new NAryExpr(Token.NoToken,
                  new IfThenElse(Token.NoToken),
-                 new ExprSeq(fp, blockIds[header], returnBlockId))),
-          "uniform loop"));
+                 new ExprSeq(fp, then, eElse));
+    } else {
+      return then;
+    }
+  }
+
+  private void AddUniformCandidateInvariant(CmdSeq cs, Block header) {
+    cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur,
+               CreateIfFPThenElse(blockIds[header], returnBlockId)),
+             "uniform loop"));
   }
 
   private void AddNonUniformCandidateInvariant(CmdSeq cs, Block header) {
@@ -232,15 +273,16 @@ class BlockPredicator {
     }
     var curIsHeaderOrExit = exits.Aggregate((Expr)Expr.Eq(cur, blockIds[header]),
                                             (e, exit) => Expr.Or(e, Expr.Eq(cur, exit)));
-    cs.Add(verifier.CreateCandidateInvariant(new NAryExpr(Token.NoToken,
-                 new IfThenElse(Token.NoToken),
-                 new ExprSeq(fp, curIsHeaderOrExit, Expr.Eq(cur, returnBlockId))),
-                 "non-uniform loop"));
+    cs.Add(prog.CreateCandidateInvariant(
+             CreateIfFPThenElse(curIsHeaderOrExit, Expr.Eq(cur, returnBlockId)),
+             "non-uniform loop"));
   }
 
-  public static void Predicate(GPUVerifier v, Program p) {
+  public static void Predicate(Program p,
+                               bool createCandidateInvariants = true,
+                               bool useProcedurePredicates = true) {
     foreach (var decl in p.TopLevelDeclarations.ToList()) {
-      if (decl is DeclWithFormals && !(decl is Function)) {
+      if (useProcedurePredicates && decl is DeclWithFormals && !(decl is Function)) {
         var dwf = (DeclWithFormals)decl;
         var fpVar = new Formal(Token.NoToken,
                                new TypedIdent(Token.NoToken, "_P",
@@ -252,7 +294,7 @@ class BlockPredicator {
       }
       var impl = decl as Implementation;
       if (impl != null)
-        new BlockPredicator(v, p, impl).PredicateImplementation();
+        new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();
     }
   }
 
diff --git a/Source/GPUVerify/GraphAlgorithms.cs b/Source/VCGeneration/GraphAlgorithms.cs
index 3442a64d..def77485 100644..100755
--- a/Source/GPUVerify/GraphAlgorithms.cs
+++ b/Source/VCGeneration/GraphAlgorithms.cs
@@ -4,7 +4,7 @@ using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
 
-namespace GPUVerify {
+namespace Microsoft.Boogie {
 
 public static class GraphAlgorithms {
 
diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index 5b2541a9..39da0be6 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -144,6 +144,7 @@
     <Reference Include="System.Xml" />

   </ItemGroup>

   <ItemGroup>

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

     <Compile Include="Check.cs" />

     <Compile Include="ConditionGeneration.cs" />

     <Compile Include="Context.cs" />

@@ -151,6 +152,7 @@
     <Compile Include="DoomedLoopUnrolling.cs" />

     <Compile Include="DoomedStrategy.cs" />

     <Compile Include="DoomErrorHandler.cs" />

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

     <Compile Include="HasseDiagram.cs" />

     <Compile Include="OrderingAxioms.cs" />

     <Compile Include="StratifiedVC.cs" />