Fix + tests for #188.

We were only checking for recursion in procedures actually being called from
init/next. In combination with recent changes to the ProcedureInliner, this
could result in a stack overflow when there was recursion in such "unreachable"
procedures.

Note these procedures may not be really be unreachable thanks to instance
procedure calls.

src/main/resources/logback.xml

@@ -17,6 +17,7 @@
   <logger name="uclid.lang.ModularProductProgramPass" level="OFF"/>
   <logger name="uclid.lang.ConstantLitRewriterPass" level="OFF"/>
   <logger name="uclid.lang.ExpressionTypeCheckerPass" level="OFF"/>
+  <logger name="uclid.lang.FindProcedureDependency" level="OFF"/>
   <logger name="uclid.lang.InlineProcedurePass" level="OFF"/>
   <logger name="uclid.lang.LazySCSolver" level="OFF"/>
   <logger name="uclid.lang.LTLPropertyRewriterPass" level="OFF"/>

src/main/scala/uclid/lang/ProcedureInliner.scala

@@ -47,6 +47,7 @@ import com.typesafe.scalalogging.Logger
 
 class FindProcedureDependencyPass extends ReadOnlyPass[Map[Identifier, Set[Identifier]]] {
   type T = Map[Identifier, Set[Identifier]]
+  lazy val logger = Logger(classOf[FindProcedureDependency])
 
   override def applyOnProcedureCall(d : TraversalDirection.T, proc : ProcedureCallStmt, in : T, context : Scope) : T = {
     def addEdge(caller : Identifier, callee : Identifier) : T = {
@@ -55,6 +56,7 @@ class FindProcedureDependencyPass extends ReadOnlyPass[Map[Identifier, Set[Ident
         case None => in + (caller -> Set(callee))
       }
     }
+    logger.debug("statement: {}", proc.toString())
     if (d == TraversalDirection.Down) {
       context.procedure match {
         case Some(currentProc) => addEdge(currentProc.id, proc.id)
@@ -67,17 +69,21 @@ class FindProcedureDependencyPass extends ReadOnlyPass[Map[Identifier, Set[Ident
 class FindProcedureDependency extends ASTAnalyzer("FindProcedureDependency", new FindProcedureDependencyPass())
 {
   var procInliningOrder : List[Identifier] = List.empty
+  lazy val logger = Logger(classOf[FindProcedureDependency])
 
   override def visit(module : Module, context : Scope) : Option[Module] = {
     def recursionError(proc : Identifier, stack : List[Identifier]) : ModuleError = {
-      val msg = "Recursion involving procedures: " + Utils.join(stack.map(_.toString).toList, ", ")
+      val procedures = stack.map(_.toString).filter(n => n != "_top").toList
+      val msg = "Recursion involving procedure(s): " + Utils.join(procedures, ", ")
       ModuleError(msg, proc.position)
     }
 
     val procDepGraph = visitModule(module, Map.empty[Identifier, Set[Identifier]], context)
-    val errors = Utils.findCyclicDependencies(procDepGraph, List(Identifier("_top")), recursionError)
+    val callers = procDepGraph.map(_._1)
+    val errors = Utils.findCyclicDependencies(procDepGraph, callers.toList, recursionError)
+    logger.debug("DepedencyGraph: {}", procDepGraph.toString())
     if (errors.size > 0) {
-      throw new Utils.ParserErrorList(errors.map(e => (e.msg, e.position)))
+      throw new Utils.ParserErrorList(errors.map(e => (e.msg, e.position)).toSet.toList)
     }
     procInliningOrder = Utils.topoSort(List(Identifier("_top")), procDepGraph)
     Some(module)

src/test/scala/ParserSpec.scala

@@ -137,6 +137,20 @@ class ParserSpec extends FlatSpec {
       // this list has all the errors from parsing
       case p : Utils.ParserErrorList =>
         assert (p.errors.size == 1)
+        assert (p.errors(0)._1.contains("Recursion"))
+    }
+  }
+  "test-recursion-2.ucl" should "not parse successfully." in {
+    try {
+      val fileModules = UclidMain.compile(List(new File("test/test-recursion-2.ucl")), lang.Identifier("main"))
+      // should never get here.
+      assert (false);
+    }
+    catch {
+      // this list has all the errors from parsing
+      case p : Utils.ParserErrorList =>
+        assert (p.errors.size == 1)
+        assert (p.errors(0)._1.contains("Recursion"))
     }
   }
   "test-procedure-types-errors.ucl" should "not parse successfully." in {
@@ -225,8 +239,8 @@ class ParserSpec extends FlatSpec {
     catch {
       // this list has all the errors from parsing
       case p : Utils.ParserErrorList =>
-        assert (p.errors.size == 1)
-        assert (p.errors.exists(p => p._1.contains("Recursion involving procedures")))
+        assert (p.errors.size == 3)
+        assert (p.errors.exists(p => p._1.contains("Recursion involving procedure(s)")))
     }
   }
   "test-parsing-history-op-error.ucl" should "not parse successfully." in {

test/test-recursion-2.ucl

@@ -0,0 +1,18 @@
+
+
+module main
+{
+    procedure f() 
+    {
+        call () = f();
+    }
+
+    var x : integer;
+
+    control
+    {
+        verify(f);
+        check;
+    }
+}
+