integrating predication

4 files changed, 52 insertions, 5 deletions

diff --git a/Source/BoogieDriver/BoogieDriver.cs b/Source/BoogieDriver/BoogieDriver.cs
index ae26d8db..746504b3 100644
--- a/Source/BoogieDriver/BoogieDriver.cs
+++ b/Source/BoogieDriver/BoogieDriver.cs
@@ -594,6 +594,15 @@ namespace Microsoft.Boogie {
         program.UnrollLoops(CommandLineOptions.Clo.LoopUnrollCount);

       }

 

+      if (CommandLineOptions.Clo.DoPredication && CommandLineOptions.Clo.StratifiedInlining > 0) {

+        BlockPredicator.Predicate(program, false, false);

+        if (CommandLineOptions.Clo.PrintInstrumented) {

+          using (TokenTextWriter writer = new TokenTextWriter(Console.Out)) {

+            program.Emit(writer);

+          }

+        }

+      }

+

       Dictionary<string, Dictionary<string, Block>> extractLoopMappingInfo = null;

       if (CommandLineOptions.Clo.ExtractLoops)

       {

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index 7d55e177..e7633014 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -574,6 +574,8 @@ namespace Microsoft.Boogie {
     public string CoverageReporterPath = null;

     public Process coverageReporter = null; // used internally for debugging

 

+    public bool DoPredication = false;

+

     public enum TypeEncoding {

       None,

       Predicates,

@@ -1230,7 +1232,8 @@ namespace Microsoft.Boogie {
               ps.CheckBooleanFlag("useUnsatCoreForContractInfer", ref UseUnsatCoreForContractInfer) ||

               ps.CheckBooleanFlag("printAssignment", ref PrintAssignment) ||

               ps.CheckBooleanFlag("nonUniformUnfolding", ref NonUniformUnfolding) ||

-              ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops)

+              ps.CheckBooleanFlag("deterministicExtractLoops", ref DeterministicExtractLoops) ||

+              ps.CheckBooleanFlag("predicate", ref DoPredication)

               ) {

             // one of the boolean flags matched

             return true;

diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs
index f4e82182..345c0365 100644
--- a/Source/VCGeneration/BlockPredicator.cs
+++ b/Source/VCGeneration/BlockPredicator.cs
@@ -77,10 +77,10 @@ public class BlockPredicator {
         // the first statement in the block.
         var assign = cmdSeq.Last();
         cmdSeq.Truncate(cmdSeq.Length-1);
-        cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(pExpr, aCmd.Expr)));
+        cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));
         cmdSeq.Add(assign);
       } else {
-        cmdSeq.Add(new AssertCmd(Token.NoToken, Expr.Imp(p, aCmd.Expr)));
+        cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(p, aCmd.Expr)));
       }
     } else if (cmd is AssumeCmd) {
       var aCmd = (AssumeCmd)cmd;
@@ -156,8 +156,13 @@ public class BlockPredicator {
     }
   }
 
-  void PredicateImplementation() {
-    blockGraph = prog.ProcessLoops(impl);
+  void PredicateImplementation() {

+    try {

+      blockGraph = prog.ProcessLoops(impl);

+    }

+    catch (Program.IrreducibleLoopException) {

+      return;

+    }
     var sortedBlocks = blockGraph.LoopyTopSort();
 
     int blockId = 0;
@@ -296,6 +301,10 @@ public class BlockPredicator {
       if (impl != null)
         new BlockPredicator(p, impl, createCandidateInvariants, useProcedurePredicates).PredicateImplementation();
     }
+  }

+

+  public static void Predicate(Program p, Implementation impl) {

+    new BlockPredicator(p, impl, false, false).PredicateImplementation();

   }
 
 }
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 373b685a..18417830 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1403,6 +1403,12 @@ namespace VC {
 

       ConvertCFG2DAG(impl);

 

+      if (CommandLineOptions.Clo.DoPredication) {

+        DesugarCalls(impl);

+        BlockPredicator.Predicate(program, impl);

+        impl.ComputePredecessorsForBlocks();

+      }

+

       SmokeTester smoke_tester = null;

       if (CommandLineOptions.Clo.SoundnessSmokeTest) {

         smoke_tester = new SmokeTester(this, impl, program, callback);

@@ -1968,6 +1974,26 @@ namespace VC {
       #endregion

     }

 

+    public void DesugarCalls(Implementation impl) {

+      foreach (Block block in impl.Blocks) {

+        CmdSeq newCmds = new CmdSeq();

+        foreach (Cmd cmd in block.Cmds) {

+          SugaredCmd sugaredCmd = cmd as SugaredCmd;

+          if (sugaredCmd != null) {

+            StateCmd stateCmd = sugaredCmd.Desugaring as StateCmd;

+            foreach (Variable v in stateCmd.Locals) {

+              impl.LocVars.Add(v);

+            }

+            newCmds.AddRange(stateCmd.Cmds);

+          }

+          else {

+            newCmds.Add(cmd);

+          }

+        }

+        block.Cmds = newCmds;

+      }

+    }

+

     public Hashtable/*TransferCmd->ReturnCmd*/ PassifyImpl(Implementation impl, out ModelViewInfo mvInfo)

     {

       Contract.Requires(impl != null);