Merge

4 files changed, 55 insertions, 39 deletions

diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs
index ed80f6ac..1827b12e 100644
--- a/Source/Core/CommandLineOptions.cs
+++ b/Source/Core/CommandLineOptions.cs
@@ -564,6 +564,7 @@ namespace Microsoft.Boogie {
     public int StratifiedInliningOption = 0;

     public bool StratifiedInliningWithoutModels = false; // disable model generation for SI

     public int StratifiedInliningVerbose = 0; // verbosity level

+    public bool BctModeForStratifiedInlining = false;

     public int RecursionBound = 500;

     public bool NonUniformUnfolding = false;

     public string inferLeastForUnsat = null;

@@ -1009,6 +1010,12 @@ namespace Microsoft.Boogie {
             StratifiedInliningVerbose = Int32.Parse(cce.NonNull(args[ps.i]));

           }

           return true;

+        case "siBct":

+          if (ps.ConfirmArgumentCount(1))

+          {

+              BctModeForStratifiedInlining = (Int32.Parse(cce.NonNull(args[ps.i])) == 1);

+          }

+          return true;

         case "recursionBound":

           if (ps.ConfirmArgumentCount(1)) {

             RecursionBound = Int32.Parse(cce.NonNull(args[ps.i]));

diff --git a/Source/GPUVerify/CommandLineOptions.cs b/Source/GPUVerify/CommandLineOptions.cs
index 8c090b6a..b2e54dbd 100644
--- a/Source/GPUVerify/CommandLineOptions.cs
+++ b/Source/GPUVerify/CommandLineOptions.cs
@@ -44,6 +44,8 @@ namespace GPUVerify
         public static bool ShowMayBeTidPlusConstantAnalysis = false;

         public static bool ShowArrayControlFlowAnalysis = false;

 

+        public static bool NoLoopPredicateInvariants = false;

+

         public static int Parse(string[] args)

         {

             for (int i = 0; i < args.Length; i++)

@@ -196,6 +198,11 @@ namespace GPUVerify
                     ShowArrayControlFlowAnalysis = true;

                     break;

 

+                    case "-noLoopPredicateInvariants":

+                    case "/noLoopPredicateInvariants":

+                    NoLoopPredicateInvariants = true;

+                    break;

+

                     default:

                         inputFiles.Add(args[i]);

                         break;

diff --git a/Source/GPUVerify/Predicator.cs b/Source/GPUVerify/Predicator.cs
index 0950cd9a..316a3df6 100644
--- a/Source/GPUVerify/Predicator.cs
+++ b/Source/GPUVerify/Predicator.cs
@@ -251,7 +251,7 @@ namespace GPUVerify
                     VisitWhileInvariants(whileCmd.Invariants, NewGuard),

                     VisitStmtList(whileCmd.Body));

 

-                if (NewInvariant != null)

+                if (NewInvariant != null && !CommandLineOptions.NoLoopPredicateInvariants)

                 {

                     NewWhile.Invariants.Add(NewInvariant);

                 }

diff --git a/Source/VCGeneration/StratifiedVC.cs b/Source/VCGeneration/StratifiedVC.cs
index 98f20d21..fa8a7f0d 100644
--- a/Source/VCGeneration/StratifiedVC.cs
+++ b/Source/VCGeneration/StratifiedVC.cs
@@ -438,8 +438,11 @@ namespace VC
                 checker2.Pop();

 

                 var end = DateTime.UtcNow;

-                Console.WriteLine("Summary computation took {0} sec and inferred {1} of {2} contracts", 

-                    (end - start).TotalSeconds, found, calls.allSummaryConst.Count);

+                if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)

+                {

+                    Console.WriteLine(">> Summary computation took {0} sec and inferred {1} of {2} contracts",

+                        (end - start).TotalSeconds, found, calls.allSummaryConst.Count);

+                }

 

             }

 

@@ -1570,7 +1573,7 @@ namespace VC
 

                 foreach (int id in calls.currCandidates)

                 {

-                    if (calls.isNonTrivialCandidate(id) && calls.getRecursionBound(id) <= CommandLineOptions.Clo.RecursionBound)

+                    if (calls.getRecursionBound(id) <= CommandLineOptions.Clo.RecursionBound)

                     {

                         toExpand.Add(id);

                     }

@@ -1754,7 +1757,14 @@ namespace VC
                         if (CommandLineOptions.Clo.StratifiedInliningVerbose > 0)

                         {

                             Console.Write(">> SI Inlining: ");

-                            reporter.candidatesToExpand.ForEach(c => Console.Write("{0} ", calls.getProc(c)));

+                            reporter.candidatesToExpand.ForEach(c =>

+                                { if (!calls.isSkipped(c)) Console.Write("{0} ", calls.getProc(c)); });

+

+                            Console.WriteLine();

+                            Console.Write(">> SI Skipping: ");

+                            reporter.candidatesToExpand.ForEach(c =>

+                            { if (calls.isSkipped(c)) Console.Write("{0} ", calls.getProc(c)); });

+

                             Console.WriteLine();

                         }

                         // Expand and try again

@@ -1790,7 +1800,7 @@ namespace VC
                 Console.WriteLine(">> SI: Calls to Z3: {0}", vState.numQueries);

                 Console.WriteLine(">> SI: Expansions performed: {0}", vState.expansionCount);

                 Console.WriteLine(">> SI: Candidates left: {0}", calls.currCandidates.Count);

-                Console.WriteLine(">> SI: Nontrivial Candidates left: {0}", calls.numNonTrivialCandidates());

+                Console.WriteLine(">> SI: Candidates skipped: {0}", calls.currCandidates.Where(i => calls.isSkipped(i)).Count());

                 Console.WriteLine(">> SI: VC Size: {0}", vState.vcSize);

             }

             #endregion

@@ -2171,11 +2181,11 @@ namespace VC
             reporter.underapproximationMode = true;

             checker.LogComment(";;;;;;;;;;;; Underapprox mode begin ;;;;;;;;;;");

             List<VCExpr> assumptions = new List<VCExpr>();

-            List<int> ids = new List<int>();

+            

             foreach (int id in calls.currCandidates)

             {

-                assumptions.Add(calls.getFalseExpr(id));

-                ids.Add(id);

+                if (!calls.isSkipped(id))

+                    assumptions.Add(calls.getFalseExpr(id));

             }

             Outcome ret = checker.CheckAssumptions(assumptions);

             checker.LogComment(";;;;;;;;;;;; Underapprox mode end ;;;;;;;;;;");

@@ -2211,11 +2221,14 @@ namespace VC
 

             foreach (int id in calls.currCandidates)

             {

+                if (calls.isSkipped(id)) continue;

+

                 int idBound = calls.getRecursionBound(id);

                 if (idBound <= bound)

                 {

                     if (idBound > 1)

                       softAssumptions.Add(calls.getFalseExpr(id));

+

                     if (block.Contains(id))

                     {

                         Contract.Assert(useSummary);

@@ -2287,6 +2300,9 @@ namespace VC
 

         // Does on-demand inlining -- pushes procedure bodies on the theorem prover stack.

         private void DoExpansion(bool incremental, List<int>/*!*/ candidates, VerificationState vState) {

+          // Skipped calls don't get inlined

+          candidates = candidates.FindAll(id => !vState.calls.isSkipped(id));

+

           vState.expansionCount += candidates.Count;

 

           if (incremental)

@@ -2859,37 +2875,23 @@ namespace VC
                 return cce.NonNull(implName2StratifiedInliningInfo[currProc].label2absy);

             }

 

-            // How many of the current candidates represent calls to procedures

-            // with non-trivial mod sets.

-            // This is only used for statistic purposes

-            public bool isNonTrivialCandidate(int id)

+            // Is this candidate a "skipped" call

+            // Currently this is experimental

+            public bool isSkipped(int id)

             {

-                string proc = getProc(id);

-                if (proc == "") return false;

-                if (!implName2StratifiedInliningInfo.ContainsKey(proc)) return false;

-                var info = implName2StratifiedInliningInfo[proc];

-                if (info.impl.Proc.Modifies.Length != 0) return true;

-                return false;

-                /*

-                foreach (IdentifierExpr ie in info.impl.Proc.Modifies)

-                {

-                    if (ie.Decl.Name.StartsWith("Mem_") || ie.Decl.Name.StartsWith("Res_"))

-                    {

-                        return true;

-                    }

-                }

-                return false;

-                 */

-            }

+                if (!CommandLineOptions.Clo.BctModeForStratifiedInlining) return false;

 

-            public int numNonTrivialCandidates()

-            {

-                int ret = 0;

-                foreach (int id in currCandidates)

-                {

-                    if (isNonTrivialCandidate(id)) ret++;

-                }

-                return ret;

+                var proc = getProc(id);

+                if (!implName2StratifiedInliningInfo.ContainsKey(proc)) return false;

+                var modSet = new HashSet<string>();

+                implName2StratifiedInliningInfo[proc].impl.Proc.Modifies

+                    .Cast<IdentifierExpr>()

+                    .Select(ie => ie.Decl.Name)

+                    .Iter(s => modSet.Add(s));

+                modSet.Remove("$Alloc");

+                modSet.Remove("assertsPassed");

+                modSet.Remove("$Exception");

+                return modSet.Count == 0;

             }

 

             // Finds labels and changes them:

@@ -3453,7 +3455,7 @@ namespace VC
                 if (underapproximationMode)

                 {

                     var cex = GenerateTraceMain(labels, model, mvInfo);

-                    Debug.Assert(candidatesToExpand.Count == 0);

+                    Debug.Assert(candidatesToExpand.All(calls.isSkipped));

                     if (cex != null) {

                       GetModelWithStates(model);

                       callback.OnCounterexample(cex, null);