Drop irreducible exceptions

Author: radumcostache

Source/Core/AST/Implementation.cs

@@ -659,12 +659,14 @@ public override void Typecheck(TypecheckingContext tc)
           graph.ComputeLoops();
           if (!graph.Reducible)
           {
-            tc.Error(this, "irreducible control flow graph not allowed");
-          }
-          else
-          {
-            TypecheckLoopAnnotations(tc, graph);
+            this.ConvertToReducible(null); // TODO: should change the null
+            tc.Impl = this;
+            graph = Program.GraphFromImpl(this);           
           }
+
+          // the graph was either reducible from the begining or was converted to a reducible one
+          Contract.Assert(graph.Reducible);
+          TypecheckLoopAnnotations(tc, graph);
         }
       }
     }
@@ -1130,7 +1132,7 @@ private QKeyValue FreshenCaptureState(QKeyValue Attributes, int FreshCounter)
 
     return result;
   }
-  public Graph<Block> ConvertToReducible(CoreOptions options)
+  public Graph<Block> ConvertToReducible(CoreOptions /*?*/ options)
   {
     Dictionary<Block, int> nextLabels = this.Blocks.ToDictionary(b => b, _ => 0);
     Graph<Block> g = Program.GraphFromImpl(this);
@@ -1186,7 +1188,10 @@ public Graph<Block> ConvertToReducible(CoreOptions options)
         duplicatesDict.Values.ForEach(b => b.SubstituteBranchTargets(duplicatesDict));
       }
 
-      PruneUnreachableBlocks(options);
+      if (options != null)
+      {
+        PruneUnreachableBlocks(options);
+      }
       ComputePredecessorsForBlocks();
       g = Program.GraphFromImpl(this);
       g.ComputeLoops();

Source/Core/AST/Program.cs

@@ -541,21 +541,19 @@ public static Graph<Block> GraphFromImpl(Implementation impl, bool forward = tru
     return GraphFromBlocks(impl.Blocks, forward);
   }
 
-  public class IrreducibleLoopException : Exception
-  {
-  }
-
   public Graph<Block> ProcessLoops(CoreOptions options, Implementation impl)
   {
     impl.PruneUnreachableBlocks(options);
     impl.ComputePredecessorsForBlocks();
     Graph<Block> g = GraphFromImpl(impl);
     g.ComputeLoops();
-    if (g.Reducible)
+    if (!g.Reducible)
     {
-      return g;
+      impl.ConvertToReducible(options);
+      g = GraphFromImpl(impl);
     }
-    throw new IrreducibleLoopException();
+    Contract.Assert(g.Reducible);
+    return g;
   }
 
 

Source/VCGeneration/LoopExtractor.cs

@@ -23,54 +23,8 @@ public static (Dictionary<string, Dictionary<string, Block>> loops, HashSet<Impl
     {
       if (impl.Blocks != null && impl.Blocks.Count > 0)
       {
-        try
-        {
-          Graph<Block> g = program.ProcessLoops(options, impl);
-          CreateProceduresForLoops(options, impl, g, loopImpls, fullMap);
-        }
-        catch (Program.IrreducibleLoopException)
-        {
-          System.Diagnostics.Debug.Assert(!fullMap.ContainsKey(impl.Name));
-          fullMap[impl.Name] = null;
-          hasIrreducibleLoops.Add(impl);
-
-          if (options.LoopUnrollCount == -1)
-          {
-            continue;
-          }
-
-          // statically unroll loops in this procedure
-
-          // 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);
-          }
-
-          // 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)
-            {
-              blockMap.Add(blk.Label, blk);
-            }
-            else
-            {
-              Contract.Assert(origBlocks.ContainsKey(sl));
-              blockMap.Add(blk.Label, origBlocks[sl]);
-            }
-          }
-
-          fullMap[impl.Name] = blockMap;
-        }
+        Graph<Block> g = program.ProcessLoops(options, impl);
+        CreateProceduresForLoops(options, impl, g, loopImpls, fullMap);
       }
     }