ExtractLoops cleanup (#939)

- Removed some options that were added specifically for Corral
- Eliminated dependency of ExtractLoops on RecursionBound in favor of
LoopUnrollCount
- Added documentation for /extractLoops

Co-authored-by: Shaz Qadeer <shaz@meta.com>

Source/Core/CoreOptions.cs

@@ -55,12 +55,11 @@ public enum VerbosityLevel
     uint ResourceLimit { get; }
     bool DoModSetAnalysis { get; }
     bool DebugStagedHoudini { get; }
+    int LoopUnrollCount { get; }
     bool DeterministicExtractLoops { get; }
     string VariableDependenceIgnore { get; }
     bool PruneInfeasibleEdges { get; }
     bool ModifyTopologicalSorting { get; }
-    bool ExtractLoopsUnrollIrreducible { get; }
-    int RecursionBound { get; }
     int InlineDepth { get; }
     bool TraceTimes { get; }
     bool FreeVarLambdaLifting { get; }

Source/ExecutionEngine/CommandLineOptions.cs

@@ -544,11 +544,6 @@ public bool PrintInlined {
     // disable model generation, used by Corral/SI
     public bool StratifiedInliningWithoutModels { get; set; }
 
-    // Sets the recursion bound, used for loop extraction, etc.
-    public int RecursionBound { get; set; } = 500;
-
-    public bool ExtractLoopsUnrollIrreducible { get; set; } = true; // unroll irreducible loops? (set programmatically)
-
     public CoreOptions.TypeEncoding TypeEncodingMethod { get; set; } = CoreOptions.TypeEncoding.Monomorphic;
 
     public bool ReflectAdd { get; set; } = false;
@@ -1118,13 +1113,7 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
           }
 
           return true;
-        case "recursionBound":
-          if (ps.ConfirmArgumentCount(1))
-          {
-            RecursionBound = Int32.Parse(cce.NonNull(args[ps.i]));
-          }
 
-          return true;
         case "enableUnSatCoreExtraction":
           if (ps.ConfirmArgumentCount(1))
           {
@@ -1806,6 +1795,10 @@ checking errors
 
   /loopUnroll:<n>
                 unroll loops, following up to n back edges (and then some)
+                default is -1, which means loops are not unrolled
+  /extractLoops
+                extract reducible loops into recursive procedures and
+                inline irreducible loops using the bound supplied by /loopUnroll:<n>
   /soundLoopUnrolling
                 sound loop unrolling
   /doModSetAnalysis

Source/ExecutionEngine/ExecutionEngine.cs

@@ -1118,10 +1118,6 @@ internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options,
           if (msgIfVerifies != null) {
             tw.WriteLine(msgIfVerifies);
           }
-
-          break;
-        case VcOutcome.ReachedBound:
-          tw.WriteLine($"Stratified Inlining: Reached recursion bound of {options.RecursionBound}");
           break;
         case VcOutcome.Errors:
         case VcOutcome.TimedOut:
@@ -1166,36 +1162,31 @@ internal static ErrorInformation GetOutcomeError(ExecutionEngineOptions options,
               }
             }
           }
-
           break;
         case VcOutcome.OutOfResource:
           if (implName != null && implTok != null) {
             string msg = "Verification out of resource (" + implName + ")";
             errorInfo = ErrorInformation.Create(implTok, msg);
           }
-
           break;
         case VcOutcome.OutOfMemory:
           if (implName != null && implTok != null) {
             string msg = "Verification out of memory (" + implName + ")";
             errorInfo = ErrorInformation.Create(implTok, msg);
           }
-
           break;
         case VcOutcome.SolverException:
           if (implName != null && implTok != null) {
             string msg = "Verification encountered solver exception (" + implName + ")";
             errorInfo = ErrorInformation.Create(implTok, msg);
           }
-
           break;
 
         case VcOutcome.Inconclusive:
           if (implName != null && implTok != null) {
             string msg = "Verification inconclusive (" + implName + ")";
             errorInfo = ErrorInformation.Create(implTok, msg);
           }
-
           break;
       }
 
@@ -1211,9 +1202,6 @@ private static string OutcomeIndication(VcOutcome vcOutcome, List<Counterexample
         default:
           Contract.Assert(false); // unexpected outcome
           throw new cce.UnreachableException();
-        case VcOutcome.ReachedBound:
-          traceOutput = "verified";
-          break;
         case VcOutcome.Correct:
           traceOutput = "verified";
           break;
@@ -1251,38 +1239,27 @@ private static void UpdateStatistics(PipelineStatistics stats, VcOutcome vcOutco
         default:
           Contract.Assert(false); // unexpected outcome
           throw new cce.UnreachableException();
-        case VcOutcome.ReachedBound:
-          Interlocked.Increment(ref stats.VerifiedCount);
-
-          break;
         case VcOutcome.Correct:
           Interlocked.Increment(ref stats.VerifiedCount);
-
           break;
         case VcOutcome.TimedOut:
           Interlocked.Increment(ref stats.TimeoutCount);
-
           break;
         case VcOutcome.OutOfResource:
           Interlocked.Increment(ref stats.OutOfResourceCount);
-
           break;
         case VcOutcome.OutOfMemory:
           Interlocked.Increment(ref stats.OutOfMemoryCount);
-
           break;
         case VcOutcome.SolverException:
           Interlocked.Increment(ref stats.SolverExceptionCount);
-
           break;
         case VcOutcome.Inconclusive:
           Interlocked.Increment(ref stats.InconclusiveCount);
-
           break;
         case VcOutcome.Errors:
           int cnt = errors.Count(e => !e.IsAuxiliaryCexForDiagnosingTimeouts);
           Interlocked.Add(ref stats.ErrorCount, cnt);
-
           break;
       }
     }
@@ -1295,38 +1272,27 @@ private static void UpdateCachedStatistics(PipelineStatistics stats, VcOutcome v
         default:
           Contract.Assert(false); // unexpected outcome
           throw new cce.UnreachableException();
-        case VcOutcome.ReachedBound:
-          Interlocked.Increment(ref stats.CachedVerifiedCount);
-
-          break;
         case VcOutcome.Correct:
           Interlocked.Increment(ref stats.CachedVerifiedCount);
-
           break;
         case VcOutcome.TimedOut:
           Interlocked.Increment(ref stats.CachedTimeoutCount);
-
           break;
         case VcOutcome.OutOfResource:
           Interlocked.Increment(ref stats.CachedOutOfResourceCount);
-
           break;
         case VcOutcome.OutOfMemory:
           Interlocked.Increment(ref stats.CachedOutOfMemoryCount);
-
           break;
         case VcOutcome.SolverException:
           Interlocked.Increment(ref stats.CachedSolverExceptionCount);
-
           break;
         case VcOutcome.Inconclusive:
           Interlocked.Increment(ref stats.CachedInconclusiveCount);
-
           break;
         case VcOutcome.Errors:
           int cnt = errors.Count(e => !e.IsAuxiliaryCexForDiagnosingTimeouts);
           Interlocked.Add(ref stats.CachedErrorCount, cnt);
-
           break;
       }
     }

Source/ExecutionEngine/ExecutionEngineOptions.cs

@@ -38,7 +38,6 @@ public interface ExecutionEngineOptions : HoudiniOptions, ConcurrencyOptions
   bool ExpandLambdas { get; }
   bool PrintLambdaLifting { get; }
   bool UseAbstractInterpretation { get; }
-  int LoopUnrollCount { get; }
   bool SoundLoopUnrolling { get; }
   bool Verify { get; }
   bool ContractInfer { get; }

Source/Houdini/StagedHoudini.cs

@@ -339,17 +339,6 @@ private static VCGenOutcome ChooseOutcome(VCGenOutcome o1, VCGenOutcome o2)
         return o1;
       }
 
-      // Neither outcome is correct, so if one outcome is ReachedBound, return the other in case it is "worse"
-      if (vcOutcome1 == VcOutcome.ReachedBound)
-      {
-        return o2;
-      }
-
-      if (vcOutcome2 == VcOutcome.ReachedBound)
-      {
-        return o1;
-      }
-
       // Both outcomes must be timeout or memout; arbitrarily choose the first
       return o1;
     }

Source/VCGeneration/ConditionGeneration.cs

@@ -1617,7 +1617,6 @@ public enum VcOutcome
     OutOfResource,
     OutOfMemory,
     Inconclusive,
-    ReachedBound,
     SolverException
   }
 

Source/VCGeneration/LoopExtractor.cs

@@ -34,40 +34,42 @@ public static (Dictionary<string, Dictionary<string, Block>> loops, HashSet<Impl
           fullMap[impl.Name] = null;
           hasIrreducibleLoops.Add(impl);
 
-          if (options.ExtractLoopsUnrollIrreducible)
+          if (options.LoopUnrollCount == -1)
           {
-            // statically unroll loops in this procedure
+            continue;
+          }
 
-            // First, build a map of the current blocks
-            var origBlocks = new Dictionary<string, Block>();
-            foreach (var blk in impl.Blocks)
-            {
-              origBlocks.Add(blk.Label, blk);
-            }
+          // statically unroll loops in this procedure
 
-            // unroll
-            Block start = impl.Blocks[0];
-            impl.Blocks = LoopUnroll.UnrollLoops(start, options.RecursionBound, false);
+          // First, build a map of the current blocks
+          var origBlocks = new Dictionary<string, Block>();
+          foreach (var blk in impl.Blocks)
+          {
+            origBlocks.Add(blk.Label, blk);
+          }
 
-            // Now construct the "map back" information
-            // Resulting block label -> original block
-            var blockMap = new Dictionary<string, Block>();
-            foreach (var blk in impl.Blocks)
+          // unroll
+          Block start = impl.Blocks[0];
+          impl.Blocks = LoopUnroll.UnrollLoops(start, options.LoopUnrollCount, false);
+
+          // Now construct the "map back" information
+          // Resulting block label -> original block
+          var blockMap = new Dictionary<string, Block>();
+          foreach (var blk in impl.Blocks)
+          {
+            var sl = LoopUnroll.sanitizeLabel(blk.Label);
+            if (sl == blk.Label)
             {
-              var sl = LoopUnroll.sanitizeLabel(blk.Label);
-              if (sl == blk.Label)
-              {
-                blockMap.Add(blk.Label, blk);
-              }
-              else
-              {
-                Contract.Assert(origBlocks.ContainsKey(sl));
-                blockMap.Add(blk.Label, origBlocks[sl]);
-              }
+              blockMap.Add(blk.Label, blk);
+            }
+            else
+            {
+              Contract.Assert(origBlocks.ContainsKey(sl));
+              blockMap.Add(blk.Label, origBlocks[sl]);
             }
-
-            fullMap[impl.Name] = blockMap;
           }
+
+          fullMap[impl.Name] = blockMap;
         }
       }
     }