Add termination checking infrastructure

Author: OzairFaizan

compiler/src/dotty/tools/dotc/Compiler.scala

@@ -35,7 +35,8 @@ class Compiler {
     List(new TyperPhase) ::         // Compiler frontend: namer, typer
     List(new WInferUnion,           // Check for type arguments inferred as union types
          CheckUnused.PostTyper(),   // Check for unused
-         CheckShadowing()) ::       // Check for shadowed elements
+         CheckShadowing(),          // Check for shadowed elements
+         CheckTermination()) ::     // Check if annotated functions terminate.
     List(new YCheckPositions) ::    // YCheck positions
     List(new sbt.ExtractDependencies) :: // Sends information on classes' dependencies to sbt via callbacks
     List(new semanticdb.ExtractSemanticInfo) :: // Extract info into .semanticdb files

compiler/src/dotty/tools/dotc/config/ScalaSettings.scala

@@ -397,6 +397,7 @@ private sealed trait YSettings:
   val Yhelp: Setting[Boolean] = BooleanSetting(ForkSetting, "Y", "Print a synopsis of private options.")
   val Ycheck: Setting[List[String]] = PhasesSetting(ForkSetting, "Ycheck", "Check the tree at the end of")
   val YcheckMods: Setting[Boolean] = BooleanSetting(ForkSetting, "Ycheck-mods", "Check that symbols and their defining trees have modifiers in sync.")
+  val YcheckTermination: Setting[Boolean] = BooleanSetting(ForkSetting, "Ycheck-termination", "check if annotated functions terminate")
   val Ydebug: Setting[Boolean] = BooleanSetting(ForkSetting, "Ydebug", "Increase the quantity of debugging output.")
   val YdebugTrace: Setting[Boolean] = BooleanSetting(ForkSetting, "Ydebug-trace", "Trace core operations.")
   val YdebugFlags: Setting[Boolean] = BooleanSetting(ForkSetting, "Ydebug-flags", "Print all flags of definitions.")

compiler/src/dotty/tools/dotc/core/Definitions.scala

@@ -1084,6 +1084,7 @@ class Definitions {
   @tu lazy val SerialVersionUIDAnnot: ClassSymbol = requiredClass("scala.SerialVersionUID")
   @tu lazy val SilentIntoAnnot: ClassSymbol = requiredClass("scala.annotation.internal.$into")
   @tu lazy val TailrecAnnot: ClassSymbol = requiredClass("scala.annotation.tailrec")
+  @tu lazy val TerminationAnnot: ClassSymbol = requiredClass("scala.annotation.terminates")
   @tu lazy val ThreadUnsafeAnnot: ClassSymbol = requiredClass("scala.annotation.threadUnsafe")
   @tu lazy val ConstructorOnlyAnnot: ClassSymbol = requiredClass("scala.annotation.constructorOnly")
   @tu lazy val CompileTimeOnlyAnnot: ClassSymbol = requiredClass("scala.annotation.compileTimeOnly")

compiler/src/dotty/tools/dotc/transform/CheckTermination.scala

@@ -0,0 +1,47 @@
+package dotty.tools.dotc
+package transform
+
+import ast.tpd
+import core.Contexts.{ctx, Context}
+import core.Decorators.*
+import core.Flags.*
+import core.Symbols.*
+import MegaPhase.MiniPhase
+
+class CheckTermination extends MiniPhase {
+  import tpd.*
+
+  override def phaseName: String = CheckTermination.name
+
+  override def description: String = CheckTermination.description
+
+  override def isEnabled(using Context): Boolean = ctx.settings.YcheckTermination.value
+
+  override def transformDefDef(tree: DefDef)(using Context): Tree = {
+    val method = tree.symbol
+    val mandatory = method.hasAnnotation(defn.TerminationAnnot)
+
+    if mandatory && !method.is(Deferred) then {
+      val checker = new TerminationChecker(method, tree.termParamss.flatten.map(_.symbol))
+      checker.traverse(tree.rhs)
+    }
+
+    tree
+  }
+
+  private class TerminationChecker(method: Symbol, params: List[Symbol])(using Context) extends TreeTraverser {
+
+    override def traverse(tree: Tree)(using Context): Unit =
+      tree match {
+        case tree @ Apply(fun, args) if fun.symbol == method =>
+          report.error(s"Recursive call to ${method.name}", tree.srcPos)
+          traverseChildren(tree)
+        case _ => traverseChildren(tree)
+      }
+  }
+}
+
+object CheckTermination:
+  val name = "check-termination"
+  val description = "check if annotated functions terminate"
+

library/src/scala/annotation/terminates.scala

@@ -0,0 +1,19 @@
+/*
+ * Scala (https://www.scala-lang.org)
+ *
+ * Copyright EPFL and Lightbend, Inc. dba Akka
+ *
+ * Licensed under Apache License 2.0
+ * (http://www.apache.org/licenses/LICENSE-2.0).
+ *
+ * See the NOTICE file distributed with this work for
+ * additional information regarding copyright ownership.
+ */
+
+package scala.annotation
+
+import scala.language.`2.13`
+
+/** A method annotation which verifies that the method will terminate
+ */
+final class terminates extends StaticAnnotation

tests/neg/ycheck-termination-norecursive.check

@@ -0,0 +1,8 @@
+-- Error: tests/neg/ycheck-termination-norecursive.scala:8:8 -----------------------------------------------------------
+8 |    loop(0 :: l) // error
+  |    ^^^^^^^^^^^^
+  |    Recursive call to loop
+-- Error: tests/neg/ycheck-termination-norecursive.scala:15:15 ---------------------------------------------------------
+15 |        x + sum(xs) // error
+   |            ^^^^^^^
+   |            Recursive call to sum

tests/neg/ycheck-termination-norecursive.scala

@@ -0,0 +1,19 @@
+//> using options -Ycheck-termination
+
+class C {
+  import scala.annotation.terminates
+
+  @terminates
+  def loop(l: List[Int]): List[Int] =
+    loop(0 :: l) // error
+
+  @terminates
+  def sum(l: List[Int]): Int =
+    l match {
+      case Nil => 0
+      case x :: xs =>
+        x + sum(xs) // error
+    }
+
+}
+