Add 'unreachable' to LLVM, assume switch is well-formed

effekt/shared/src/main/scala/effekt/core/optimizer/Normalizer.scala

@@ -58,6 +58,22 @@ object Normalizer { normal =>
     }
   }
 
+  /**
+   * Do the clauses name every constructor of the scrutinee's type?
+   * If so, the default is unreachable!
+   *
+   * Beware: Deadcode might have dropped constructors that are never built.
+   */
+  private def covers(tpe: ValueType, clauses: List[(Id, BlockLit)])(using C: Context): Boolean = tpe match {
+    case ValueType.Data(name, _) => C.decls.findData(name).exists { data =>
+      clauses.length >= data.constructors.length && {
+        val tags = clauses.iterator.map(_._1).toSet
+        data.constructors.forall { c => tags.contains(c.id) }
+      }
+    }
+    case _ => false
+  }
+
   /** Within a branch, we know the value of the condition. */
   private def assuming(cond: Expr, value: Boolean)(using C: Context): Context =
     C.knowing(cond, Expr.Literal(value, Type.TBoolean))
@@ -280,7 +296,7 @@ object Normalizer { normal =>
         val normalized = normalize(scrutinee)
         Stmt.Match(normalized, tpe, clauses.map { case (tag, clause) =>
           tag -> normalize(clause)(using selecting(normalized, tag, clause))
-        }, default.map(normalize))
+        }, default.filter(_ => !covers(normalized.tpe, clauses)).map(normalize))
     }
 
     // [[ if (true) stmt1 else stmt2 ]] = [[ stmt1 ]]

effekt/shared/src/main/scala/effekt/generator/llvm/PrettyPrinter.scala

@@ -112,6 +112,9 @@ ${indentedLines(instructions.map(show).mkString("\n"))}
     case ExtractValue(result, aggregate, index) =>
       s"${localName(result)} = extractvalue ${show(aggregate)}, $index"
 
+    case Icmp(result, predicate, tpe, operand0, operand1) =>
+      s"${localName(result)} = icmp ${predicate} ${show(tpe)} ${showOperand(operand0)._2}, ${showOperand(operand1)._2}"
+
     case Comment(msg) if C.config.debug() =>
       val sanitized = msg.map((c: Char) => if (' ' <= c && c != '\\' && c <= '~') c else '?').mkString
       s"\n; $sanitized"
@@ -122,25 +125,32 @@ ${indentedLines(instructions.map(show).mkString("\n"))}
   def show(terminator: Terminator): LLVMString = terminator match {
     case RetVoid() =>
       s"ret void"
-    case Ret(operand) => 
+    case Ret(operand) =>
       s"ret ${show(operand)}"
     case Switch(operand, defaultDest, dests) =>
       def destAsFragment(dest: (Int, String)) = s"i64 ${dest._1}, label ${localName(dest._2)}";
       s"switch ${show(operand)}, label ${localName(defaultDest)} [${spaceSeparated(dests.map(destAsFragment))}]"
     case CondBr(condition, trueDest, falseDest) =>
       s"br ${show(condition)}, label ${localName(trueDest)}, label ${localName(falseDest)}"
+    case Unreachable() =>
+      s"unreachable"
+  }
+
+  private def showOperand(operand: Operand): (Type, LLVMString) = operand match {
+    case LocalReference(tpe, name)          => (tpe, localName(name))
+    case ConstantGlobal(name)               => (PointerType(), globalName(name))
+    case ConstantInt(n)                     => (IntegerType64(), s"$n")
+    case ConstantByte(n)                    => (IntegerType8(), s"$n")
+    case ConstantDouble(n)                  => (DoubleType(), s"$n")
+    case ConstantAggregateZero(tpe)         => (tpe, "zeroinitializer")
+    case ConstantNull(tpe)                  => (tpe, "null")
+    case ConstantArray(memberType, members) => (ArrayType(members.length, memberType), s"[${commaSeparated(members.map(show))}]")
+    case ConstantInteger8(b)                => (IntegerType8(), s"$b")
   }
 
-  def show(operand: Operand): LLVMString = operand match {
-    case LocalReference(tpe, name)          => s"${show(tpe)} ${localName(name)}"
-    case ConstantGlobal(name)               => s"ptr ${globalName(name)}"
-    case ConstantInt(n)                     => s"i64 $n"
-    case ConstantByte(n)                    => s"i8 $n"
-    case ConstantDouble(n)                  => s"double $n"
-    case ConstantAggregateZero(tpe)         => s"${show(tpe)} zeroinitializer"
-    case ConstantNull(tpe)                  => s"${show(tpe)} null"
-    case ConstantArray(memberType, members) => s"[${members.length} x ${show(memberType)}] [${commaSeparated(members.map(show))}]"
-    case ConstantInteger8(b)                => s"i8 $b"
+  def show(operand: Operand): LLVMString = {
+    val (typ, name) = showOperand(operand)
+    s"${show(typ)} $name"
   }
 
   def show(tpe: Type): LLVMString = tpe match {

effekt/shared/src/main/scala/effekt/generator/llvm/Transformer.scala

@@ -2,6 +2,7 @@ package effekt
 package generator
 package llvm
 
+import effekt.context.Context
 import effekt.machine
 import effekt.util.intercalate
 import effekt.util.messages.ErrorReporter
@@ -16,10 +17,10 @@ object Transformer {
 
   val llvmFeatureFlags: List[String] = List("llvm", "c")
 
-  def transform(program: machine.Program)(using ErrorReporter): List[Definition] = program match {
+  def transform(program: machine.Program)(using C: Context): List[Definition] = program match {
     case machine.Program(declarations, definitions, entry) =>
 
-      given MC: ModuleContext = ModuleContext();
+      given MC: ModuleContext = ModuleContext(debug = C.config.debug());
       declarations.foreach(transform);
       definitions.foreach(transform);
 
@@ -132,9 +133,9 @@ object Transformer {
         eraseValues(List(variable), freeVariables(rest))
         transform(rest)
 
+      // No clauses and no default: the scrutinee's type is uninhabited ~> unreachable
       case machine.Switch(value, Nil, None) =>
-        // TODO unreachable
-        RetVoid()
+        Unreachable()
 
       case machine.Switch(value, clauses, default) =>
         emit(Comment(s"switch ${value.name}, ${clauses.length} clauses"))
@@ -146,6 +147,14 @@ object Transformer {
         emit(ExtractValue(tagName, transform(value), 0))
         emit(ExtractValue(objectName, transform(value), 1))
 
+        // if there's no default clause, tell LLVM that it can assume that the tag is less than number of clauses
+        if (default.isEmpty) {
+          val cmpName = freshName("tagInRange")
+          val numTags = clauses.iterator.map(_._1).max + 1 // TODO: carry this on the switch / data type?
+          emit(Icmp(cmpName, "ult", IntegerType64(), LocalReference(IntegerType64(), tagName), ConstantInt(numTags)))
+          emit(Call("_", Ccc(), VoidType(), assume, List(LocalReference(IntegerType1(), cmpName))))
+        }
+
         val stack = getStack()
         def labelClause(clause: machine.Clause, isDefault: Boolean): String = {
           implicit val BC = BlockContext()
@@ -167,9 +176,12 @@ object Transformer {
 
         val defaultLabel = default match {
           case Some(clause) => labelClause(clause, isDefault = true)
+          // No default ~> clauses cover every tag the scrutinee can have ~> unreachable
+          // in `--debug` mode, we emit a call to [[unmatchedTag]] for better debugging
           case None =>
             val label = freshName("label");
-            emit(BasicBlock(label, List(), RetVoid()))
+            val checks = if MC.debug then List(Call("_", Ccc(), VoidType(), unmatchedTag, List())) else Nil
+            emit(BasicBlock(label, checks, Unreachable()))
             label
         }
 
@@ -453,8 +465,8 @@ object Transformer {
        val litName = freshName("hole_pos")
        emit(GlobalConstant(s"$litName.lit", ConstantArray(IntegerType8(), utf8.map { b => ConstantInteger8(b) }.toList)))
 
-       emit(Call("_", Ccc(), VoidType(), ConstantGlobal("hole"), List(ConstantGlobal(s"$litName.lit"))))
-       RetVoid()
+       emit(Call("_", Ccc(), VoidType(), hole, List(ConstantGlobal(s"$litName.lit"))))
+       Unreachable() // hole never returns
     }
 
   def transform(label: machine.Label): ConstantGlobal =
@@ -851,6 +863,10 @@ object Transformer {
 
   val freeStack = ConstantGlobal("freeStack")
 
+  val hole = ConstantGlobal("hole");
+  val unmatchedTag = ConstantGlobal("unmatched_tag");
+  val assume = ConstantGlobal("llvm.assume");
+
   val newReference = ConstantGlobal("newReference")
   val getVarPointer = ConstantGlobal("getVarPointer")
 
@@ -867,7 +883,7 @@ object Transformer {
   /**
    * Extra info in context
    */
-  class ModuleContext() {
+  class ModuleContext(val debug: Boolean) {
     var counter = 0;
     var definitions: List[Definition] = List();
     val erasers = mutable.HashMap[(List[machine.Type], EraserKind), Operand]();

effekt/shared/src/main/scala/effekt/generator/llvm/Tree.scala

@@ -71,6 +71,8 @@ enum Instruction {
   case FAdd(result: String, operand0: Operand, operand1: Operand)
   case InsertValue(result: String, aggregate: Operand, element: Operand, index: Int)
   case ExtractValue(result: String, aggregate: Operand, index: Int)
+  // predicate is one of LLVM's icmp predicates, for example: "ult", "eq", "ule"
+  case Icmp(result: String, predicate: String, tpe: Type, operand0: Operand, operand1: Operand)
   case Comment(msg: String)
 }
 export Instruction.*
@@ -80,6 +82,7 @@ enum Terminator {
   case Ret(operand: Operand)
   case Switch(operand: Operand, defaultDest: String, dests: List[(Int, String)])
   case CondBr(condition: Operand, trueDest: String, falseDest: String)
+  case Unreachable()
 }
 export Terminator.*
 

libraries/llvm/forward-declare-c.ll

@@ -8,8 +8,9 @@ declare void @c_io_println(%Pos)
 declare %Pos @c_io_readln()
 declare %Double @c_io_random()
 
-declare void @hole(i8*) cold
-declare void @duplicated_prompt() cold
+declare void @hole(i8*) cold noreturn
+declare void @duplicated_prompt() cold noreturn
+declare void @unmatched_tag() cold noreturn
 
 declare %Pos @c_ref_fresh(%Pos)
 declare %Pos @c_ref_get(%Pos)

libraries/llvm/panic.c

@@ -7,16 +7,23 @@
 // this should _morally_ be using `stderr`, but we don't tee it in tests
 // see PR #823 & issue #815 for context
 
-__attribute__((cold))
+__attribute__((cold, noreturn))
 void hole(const char* message) {
     printf("PANIC: %s not implemented yet\n", message);
     exit(1);
 }
 
-__attribute__((cold))
+__attribute__((cold, noreturn))
 void duplicated_prompt() {
     printf("PANIC: Continuation invoked itself\n");
     exit(1);
 }
 
+// Only emitted in debug builds: the backend otherwise assumes this is unreachable
+__attribute__((cold, noreturn))
+void unmatched_tag() {
+    printf("PANIC: no case matched the scrutinee's tag (this is a bug in the Effekt compiler)\n");
+    exit(1);
+}
+
 #endif

libraries/llvm/rts.ll

@@ -694,13 +694,11 @@ define private tailcc void @topLevel(%Pos %val, %Stack %stack) {
 }
 
 define private void @topLevelSharer(%Environment %environment) {
-    ; TODO this should never be called
-    ret void
+    unreachable ; should never be called
 }
 
 define private void @topLevelEraser(%Environment %environment) {
-    ; TODO this should never be called
-    ret void
+    unreachable ; should never be called
 }
 
 define private %Stack @withEmptyStack() {