Move block predicator to VCGeneration

6 files changed, 43 insertions, 40 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 645fdc49..284247e6 100644..100755
--- a/Source/GPUVerify/BlockPredicator.cs
+++ b/Source/VCGeneration/BlockPredicator.cs
@@ -1,20 +1,19 @@
 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;
@@ -27,10 +26,10 @@ class BlockPredicator {
   Dictionary<Block, Expr> blockIds = new Dictionary<Block, Expr>();
   HashSet<Block> doneBlocks = new HashSet<Block>();
 
-  BlockPredicator(GPUVerifier v, Program p, Implementation i, bool upp) {
-    verifier = v;
+  BlockPredicator(Program p, Implementation i, bool cci, bool upp) {
     prog = p;
-    impl = i;
+    impl = i;

+    createCandidateInvariants = cci;
     useProcedurePredicates = upp;
   }
 
@@ -222,7 +221,7 @@ class BlockPredicator {
                                             new BlockSeq(runBlock));
 
         pExpr = Expr.Eq(cur, blockIds[runBlock]);
-        if (CommandLineOptions.Inference && blockGraph.Headers.Contains(runBlock)) {
+        if (createCandidateInvariants && blockGraph.Headers.Contains(runBlock)) {
           AddUniformCandidateInvariant(runBlock.Cmds, runBlock);
           AddNonUniformCandidateInvariant(runBlock.Cmds, runBlock);
         }
@@ -252,7 +251,7 @@ class BlockPredicator {
   }
 
   private void AddUniformCandidateInvariant(CmdSeq cs, Block header) {
-    cs.Add(verifier.CreateCandidateInvariant(Expr.Eq(cur,
+    cs.Add(prog.CreateCandidateInvariant(Expr.Eq(cur,
                CreateIfFPThenElse(blockIds[header], returnBlockId)),
              "uniform loop"));
   }
@@ -274,12 +273,14 @@ 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(
+    cs.Add(prog.CreateCandidateInvariant(
              CreateIfFPThenElse(curIsHeaderOrExit, Expr.Eq(cur, returnBlockId)),
              "non-uniform loop"));
   }
 
-  public static void Predicate(GPUVerifier v, Program p, bool useProcedurePredicates = true) {
+  public static void Predicate(Program p,

+                               bool createCandidateInvariants = true,

+                               bool useProcedurePredicates = true) {
     foreach (var decl in p.TopLevelDeclarations.ToList()) {
       if (useProcedurePredicates && decl is DeclWithFormals && !(decl is Function)) {
         var dwf = (DeclWithFormals)decl;
@@ -293,7 +294,7 @@ class BlockPredicator {
       }
       var impl = decl as Implementation;
       if (impl != null)
-        new BlockPredicator(v, p, impl, useProcedurePredicates).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" />