VCGeneration: implement smart predication

This predication algorithm is intended to reduce the complexity
of predicated verification conditions by reducing the amount of
predicated state and using only boolean algebra, as opposed to the
previous algorithm which also uses integers.

It assigns a unique predicate to every superblock, which is defined
per Agrawal [1] except that superblocks are further partitioned
such that either no element of the same superblock may be contained
within a natural loop or each element of the superblock has the same
innermost natural loop head.  Predicates are assigned at the element
of the superblock which dominates all others, and are reset to false
at a loop head and at the start of a procedure in order to ensure
correct execution for future iterations.  When exiting a loop, all
predicates corresponding to heads of exited loops are reset to false.

The algorithm requires that every successor at every divergence
point in the CFG contains assumes marked with an attribute (called
':partition') which a frontend uses to certify to the predicator
that for each block, if each successor of that block contains an
assume statement marked with :partition, exactly one of those assume
statement's predicates will hold.  The frontend we use for GPUVerify
generates such attributes, and as such the new predicator is only
used there, and the old predicator has been retained for Corral etc.

[1] Hiralal Agrawal. Dominators, super blocks, and program coverage.
    In POPL '94, p25-34.

1 files changed, 2 insertions, 1 deletions

diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index 39da0be6..780e4891 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -155,6 +155,7 @@
     <Compile Include="GraphAlgorithms.cs" />

     <Compile Include="HasseDiagram.cs" />

     <Compile Include="OrderingAxioms.cs" />

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

     <Compile Include="StratifiedVC.cs" />

     <Compile Include="VC.cs" />

     <Compile Include="VCDoomed.cs" />

@@ -223,4 +224,4 @@
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>
\ No newline at end of file
+</Project>