What are the roles of origins and blames

[pieter-bos]

Loosely speaking, origins do the following:

• preferredName states the approximate name we want to use for a declaration, for example from the user source, a literal for a generated definition, or a prefix for a derived definition
• context and inlineContext repeat the user source that the origin source is pointing to, or provide extra context around an inner origin
• shortPosition roughly means "please just give me the file position"
• explain a node's reason to exist, by virtue of the layered structure of the origin.

this accumulates into enough surface area to make Origin also a Blame: it can state an error in the context in which it occurs.

Blames do the following:

• explain how to transform errors: usually one-to-one, but sometimes 1-to-0, 1-to-many, or something custom via stateful accounting (e.g. inversion)
• explain the reason a proof obligation exists, by virtue of the layered structure of the blame
• explain what to do when an error of a particular kind occurs when transforming is done: usually something like println(err.toString)

[pieter-bos]

List of all origin implementations

case object FileSpanningOrigin extends Origin {
  override def preferredName: String = "unknown"
  override def shortPosition: String = "multiple"
  override def context: String = "[At node that spans multiple files]"
  override def inlineContext: String = "[Node that spans multiple files]"
}

case object DiagnosticOrigin extends Origin {
  override def preferredName: String = "unknown"
  override def context: String = ""
  override def inlineContext: String = ""
  override def shortPosition: String = "unknown"
}

abstract class InputOrigin extends Origin {
  override def preferredName: String = "unknown"
}

case class ReadableOrigin(readable: Readable,
                          startLineIdx: Int, endLineIdx: Int,
                          cols: Option[(Int, Int)])
  extends InputOrigin {
  private def startText: String = cols match {
    case Some((startColIdx, _)) => f"${readable.fileName}:${startLineIdx+1}:${startColIdx+1}"
    case None => f"${readable.fileName}:${startLineIdx+1}"
  }

  private def endText: String = cols match {
    case Some((_, endColIdx)) => f"${endLineIdx+1}:${endColIdx+1}"
    case None => f"${endLineIdx+1}"
  }

  private def baseFilename: String = Paths.get(readable.fileName).getFileName.toString

  override def shortPosition: String = cols match {
    case Some((startColIdx, _)) => f"$baseFilename:${startLineIdx+1}:${startColIdx+1}"
    case None => f"$baseFilename:${startLineIdx+1}"
  }

  override def context: String = {
    val atLine = f" At $startText:\n"

    if(readable.isRereadable) {
      atLine + Origin.HR + InputOrigin.contextLines(readable, startLineIdx, endLineIdx, cols)
    } else {
      atLine
    }
  }

  override def inlineContext: String =
    if(readable.isRereadable)
      InputOrigin.inlineContext(readable, startLineIdx, endLineIdx, cols)
    else
      f"(non-rereadable source ${readable.fileName})"

  override def toString: String = f"$startText - $endText"
}

case class InterpretedOriginVariable(name: String, original: Origin)
  extends InputOrigin {
  override def preferredName: String = name

  override def context: String = original.context

  override def inlineContext: String = original.inlineContext

  override def shortPosition: String = original.shortPosition
}

case class InterpretedOrigin(interpreted: Readable,
                             startLineIdx: Int, endLineIdx: Int,
                             cols: Option[(Int, Int)],
                             original: Origin)
  extends InputOrigin {
  private def startText: String = cols match {
    case Some((startColIdx, _)) => f"${interpreted.fileName}:${startLineIdx+1}:${startColIdx+1}"
    case None => f"${interpreted.fileName}:${startLineIdx+1}"
  }

  private def endText: String = cols match {
    case Some((_, endColIdx)) => f"${endLineIdx+1}:${endColIdx+1}"
    case None => f"${endLineIdx+1}"
  }

  override def shortPosition: String = original.shortPosition

  override def context: String = {
    val interpretedAtLine = f" Interpreted at $startText as:\n"

    val interpretedText = if(interpreted.isRereadable) {
      interpretedAtLine + Origin.HR + InputOrigin.contextLines(interpreted, startLineIdx, endLineIdx, cols)
    } else {
      interpretedAtLine
    }

    original.context + Origin.HR + interpretedText
  }

  override def inlineContext: String =
    if(interpreted.isRereadable)
      InputOrigin.inlineContext(interpreted, startLineIdx, endLineIdx, cols)
    else
      f"(non-rereadable source ${interpreted.fileName})"

  override def toString: String =
    f"$startText - $endText interpreted from $original"
}

case class SourceNameOrigin(name: String, inner: Origin) extends Origin {
  override def preferredName: String = name
  override def shortPosition: String = inner.shortPosition
  override def context: String = inner.context
  override def inlineContext: String = inner.inlineContext

  override def toString: String =
    s"$name at $inner"
}

  case class JavaSystemOrigin(preferredName: String) extends Origin {
    override def shortPosition: String = "reflection"
    override def context: String = s"At: [Class loaded from JRE with reflection]"
    override def inlineContext: String = "[Class loaded from JRE with reflection]"
  }

  case class CoercionOrigin(of: Expr[_]) extends Origin {
    override def preferredName: String = "unknown"
    override def shortPosition: String = of.o.shortPosition
    override def context: String = of.o.context
    override def inlineContext: String = of.o.inlineContext
  }

  private case class ConstOrigin(value: scala.Any) extends Origin {
    override def preferredName: String = "unknown"
    override def shortPosition: String = "generated"
    override def context: String = s"[At generated constant `$value`]"
    override def inlineContext: String = value.toString
  }

  case object GeneratedQuantifier extends Origin {
    override def preferredName: String = "i"
    override def shortPosition: String = "generated"
    override def context: String = "[At generated quantifier]"
    override def inlineContext: String = "[Generated quantifier]"
  }

  case class CheckSatOrigin(inner: Origin, n: Option[String]) extends Origin {
    override def preferredName: String = "check_sat_" + n.getOrElse(inner.preferredName)
    override def context: String = inner.context
    override def inlineContext: String = inner.inlineContext
    override def shortPosition: String = inner.shortPosition
  }

  case object TypeOfOrigin extends Origin {
    override def preferredName: String = "type"
    override def shortPosition: String = "generated"
    override def context: String = "[At function type]"
    override def inlineContext: String = "[Function type]"
  }

  case object InstanceOfOrigin extends Origin {
    override def preferredName: String = "subtype"
    override def shortPosition: String = "generated"
    override def context: String = "[At function subtype]"
    override def inlineContext: String = "[Function subtype]"
  }

  case object This extends Origin {
    override def preferredName: String = "this"
    override def shortPosition: String = "generated"
    override def context: String = "[At generated parameter for 'this']"
    override def inlineContext: String = "this"
  }

  case class ValuesFunctionOrigin(preferredName: String = "unknown") extends Origin {
    override def shortPosition: String = "generated"
    override def context: String = "[At node generated for \\values]"
    override def inlineContext: String = "[Node generated for \\values]"
  }

  case class ArrayCreationOrigin(preferredName: String = "unknown") extends Origin {
    override def shortPosition: String = "generated"
    override def context: String = "[At node generated for array creation]"
    override def inlineContext: String = "[Node generated for array creation]"
  }

  case object CurrentThreadIdOrigin extends Origin {
    override def preferredName: String = "tid"
    override def shortPosition: String = "generated"
    override def context: String = "[At generated variable for the current thread ID]"
    override def inlineContext: String = "\\current_thread"
  }

  case class IdleToken(cls: Class[_]) extends Origin {
    override def preferredName: String = cls.o.preferredName + "Idle"
    override def context: String = cls.o.context
    override def inlineContext: String = cls.o.inlineContext
    override def shortPosition: String = cls.o.shortPosition
  }

  case class RunningToken(cls: Class[_]) extends Origin {
    override def preferredName: String = cls.o.preferredName + "Running"
    override def context: String = cls.o.context
    override def inlineContext: String = cls.o.inlineContext
    override def shortPosition: String = cls.o.shortPosition
  }

  case class ForkMethod(cls: Class[_]) extends Origin {
    override def preferredName: String = "fork" + cls.o.preferredName
    override def context: String = cls.o.context
    override def inlineContext: String = cls.o.inlineContext
    override def shortPosition: String = cls.o.shortPosition
  }

  case class JoinMethod(cls: Class[_]) extends Origin {
    override def preferredName: String = "join" + cls.o.preferredName
    override def context: String = cls.o.context
    override def inlineContext: String = cls.o.inlineContext
    override def shortPosition: String = cls.o.shortPosition
  }

  case class LockInvariantOrigin(cls: Class[_]) extends Origin {
    override def preferredName: String = "lock_inv_" + cls.o.preferredName
    override def shortPosition: String = cls.intrinsicLockInvariant.o.shortPosition
    override def context: String = cls.intrinsicLockInvariant.o.context
    override def inlineContext: String = cls.intrinsicLockInvariant.o.inlineContext
  }

  case class HeldTokenOrigin(cls: Class[_]) extends Origin {
    override def preferredName: String = "lock_held_" + cls.o.preferredName
    override def shortPosition: String = cls.intrinsicLockInvariant.o.shortPosition
    override def context: String = cls.intrinsicLockInvariant.o.context
    override def inlineContext: String = cls.intrinsicLockInvariant.o.inlineContext
  }

  case class CommittedOrigin(cls: Class[_]) extends Origin {
    override def preferredName: String = "lock_committed_" + cls.o.preferredName
    override def shortPosition: String = cls.intrinsicLockInvariant.o.shortPosition
    override def context: String = cls.intrinsicLockInvariant.o.context
    override def inlineContext: String = cls.intrinsicLockInvariant.o.inlineContext
  }

  case object Once extends Origin {
    override def preferredName: String = "once"
    override def context: String = "[At node generated to execute a while loop once]"
    override def inlineContext: String = "Node generated to execute a while loop once"
    override def shortPosition: String = "generated"
  }

  case object Indet extends Origin {
    override def preferredName: String = "indet"
    override def context: String = "[At node generated to contain an indeterminate integer]"
    override def inlineContext: String = "Node generated to contain an indeterminate integer"
    override def shortPosition: String = "generated"
  }

  case object EvaluationOrigin extends Origin {
    override def preferredName: String = "evaluationDummy"
    override def shortPosition: String = "generated"
    override def context: String = s"[At variable generated for an evaluation]"
    override def inlineContext: String = "[Variable generated for an evaluation]"
  }

  case object ExplodeOrigin extends Origin {
    override def preferredName: String = "unknown"
    override def context: String = "At: [node generated to split out verification]"
    override def inlineContext: String = "[Node generated to split out verification]"
    override def shortPosition: String = "generated"
  }

  case class AssumeFunction(inner: Origin) extends Origin {
    override def preferredName: String = "assume" + inner.preferredName.capitalize
    override def context: String = inner.context
    override def inlineContext: String = inner.inlineContext
    override def shortPosition: String = inner.shortPosition
  }

  case class FormalParameterOrigin(inner: Origin) extends Origin {
    override def preferredName: String = "formal" + inner.preferredName.capitalize
    override def context: String = inner.context
    override def inlineContext: String = inner.inlineContext
    override def shortPosition: String = inner.shortPosition
  }

  case class CastFuncOrigin(preferredName: String) extends Origin {
    override val context: String = "function generated by FloatToRat"
    override val inlineContext: String = "function generated by FloatToRat"
    override val shortPosition: String = "function generated by FloatToRat"
  }

  case class YieldDummy(forArg: Variable[_]) extends Origin {
    override def preferredName: String = "dummy_" + forArg.o.preferredName
    override def shortPosition: String = "generated"
    override def context: String = "[At dummy variable for an unused out parameter]"
    override def inlineContext: String = "[Dummy variable for an unused out parameter]"
  }

  case class InlinedOrigin(definition: Origin, usages: Seq[Apply[_]]) extends Origin {
    override def preferredName: String = definition.preferredName
    override def shortPosition: String = usages.head.o.shortPosition
    override def context: String =
      usages.map(_.o.context).mkString(
        start = " Inlined from:\n" + Origin.HR,
        sep = Origin.HR + " ...Then inlined from:\n" + Origin.HR,
        end = "",
      ) + Origin.HR +
        " In definition:\n" + Origin.HR +
        definition.context

    override def inlineContext: String = s"${definition.inlineContext} [inlined from] ${usages.head.o.inlineContext}"
  }

  case object IterationContractOrigin extends Origin {
    override def preferredName: String = ???
    override def shortPosition: String = "generated"
    override def context: String = ???
    override def inlineContext: String = ???
  }

  case class LowEvalOrigin(v: IterVariable[_]) extends Origin {
    override def preferredName: String = "lo_" + v.variable.o.preferredName
    override def context: String = v.variable.o.context
    override def inlineContext: String = v.variable.o.inlineContext
    override def shortPosition: String = v.variable.o.shortPosition
  }

  case class HighEvalOrigin(v: IterVariable[_]) extends Origin {
    override def preferredName: String = v.variable.o.preferredName + "_hi"
    override def context: String = v.variable.o.context
    override def inlineContext: String = v.variable.o.inlineContext
    override def shortPosition: String = v.variable.o.shortPosition
  }

  case object PureMethodOrigin extends Origin {
    override def preferredName: String = "unknown"
    override def shortPosition: String = "generated"
    override def context: String = "[At node generated for pure method]"
    override def inlineContext: String = "[Node generated for pure method]"
  }

  case object GeneratedQuantifierOrigin extends Origin {
    override def preferredName: String = "i"
    override def shortPosition: String = "generated"
    override def context: String = "[At node generated for auto-quantified expressions containing `*`]"
    override def inlineContext: String = "[* index]"
  }

  case class EvalCheckFunction(preferredName: String = "unknown") extends Origin {
    override def context: String = "At: [Function generated to check the evaluation of an expression is ok]"
    override def inlineContext: String = "[Function generated to check the evaluation of an expression is ok]"
    override def shortPosition: String = "generated"
  }

  case object SideEffectOrigin extends Origin {
    override def preferredName: String = "flatten"
    override def shortPosition: String = "generated"
    override def context: String = "[At node generated to collect side effects]"
    override def inlineContext: String = "[Extracted expression]"
  }

  case object ResultVar extends Origin {
    override def preferredName: String = "res"
    override def shortPosition: String = "generated"
    override def context: String = "[At node generated to contain the result of a method]"
    override def inlineContext: String = "[Method return value]"
  }

  case class CheckScale(preferredName: String = "") extends Origin {
    override def shortPosition: String = "generated"
    override def context: String = "[At function generated to check that scale values are non-negative]"
    override def inlineContext: String = "[Function generated to check that scale values are non-negative]"
  }

  case object SimplifyNestedQuantifiersOrigin extends Origin {
    override def preferredName: String = "unknown"

    override def shortPosition: String = "generated"

    override def context: String = "[At generated expression for the simplification of nested quantifiers]"

    override def inlineContext: String = "[Simplified expression]"
  }

  case class BinderOrigin(name: String) extends Origin {
    override def preferredName: String = name

    override def shortPosition: String = "generated"

    override def context: String = "[At generated expression for the simplification of nested quantifiers]"

    override def inlineContext: String = "[Simplified expression]"
  }

  case object SimplifyQuantifiedRelationsOrigin extends Origin {
    override def preferredName: String = "unknown"
    override def shortPosition: String = "generated"
    override def context: String = "[At generated expression for the simplification of quantified integer relations]"
    override def inlineContext: String = "[Simplified expression]"
  }

  case class ArrayField(t: Type[_]) extends Origin {
    override def preferredName: String = typeText(t)
    override def shortPosition: String = "generated"
    override def context: String = s"[At field generated for array location of type $t]"
    override def inlineContext: String = s"[Field generated for array location of type $t]"
  }

  case class PointerField(t: Type[_]) extends Origin {
    override def preferredName: String = typeText(t)
    override def shortPosition: String = "generated"
    override def context: String = s"[At field generated for pointer location of type $t]"
    override def inlineContext: String = s"[Field generated for pointer location of type $t]"
  }

case class ContinueToBreakOrigin(labelDeclOrigin: Origin) extends Origin {
  override def preferredName: String = "continue" + labelDeclOrigin.preferredName.capitalize
  override def shortPosition: String = "generated"
  override def context: String = labelDeclOrigin.context
  override def inlineContext: String = labelDeclOrigin.inlineContext
}

  case class PostLabeledStatementOrigin(label: LabelDecl[_]) extends Origin {
    override def preferredName: String = "break_" + label.o.preferredName
    override def shortPosition: String = "generated"
    override def context: String = "[At node generated to jump past a statement]"
    override def inlineContext: String = "[After] " + label.o.inlineContext
  }

  case object ReturnClass extends Origin {
    override def preferredName: String = "Return"
    override def shortPosition: String = "generated"
    override def context: String = "[At class generated to encode return with an exception]"
    override def inlineContext: String = "[Return value exception class]"
  }

  case object ReturnField extends Origin {
    override def preferredName: String = "value"
    override def shortPosition: String = "generated"
    override def context: String = "[At field generated to encode return with an exception]"
    override def inlineContext: String = "[Return value exception class field]"
  }

  case object ReturnTarget extends Origin {
    override def preferredName: String = "end"
    override def shortPosition: String = "generated"
    override def context: String = "[At label generated for the end of the method]"
    override def inlineContext: String = "[End of method]"
  }

  case object ReturnVariable extends Origin {
    override def preferredName: String = "return"
    override def shortPosition: String = "generated"
    override def context: String = "[At variable generated for the result of the method]"
    override def inlineContext: String = "[Return value]"
  }

  case object BreakException extends Origin {
    override def preferredName: String = "Break"
    override def shortPosition: String = "generated"
    override def context: String = "[At exception class generated to break on a label or loop]"
    override def inlineContext: String = "[Break exception class]"
  }

  case object ExcVar extends Origin {
    override def preferredName: String = "exc"

    override def shortPosition: String = "generated"

    override def context: String = "[At variable generated to contain thrown exception]"

    override def inlineContext: String = "[Current exception]"
  }

  case object CurrentlyHandling extends Origin {
    override def preferredName: String = "currently_handling_exc"

    override def shortPosition: String = "generated"

    override def context: String = "[At variable generated to remember exception currently being handled]"

    override def inlineContext: String = "[Exception currently being handled]"
  }

  case object ReturnPoint extends Origin {
    override def preferredName: String = "bubble"

    override def shortPosition: String = "generated"

    override def context: String = "[At label generated to bubble an exception]"

    override def inlineContext: String = "[Exception bubble label]"
  }

  case object CatchLabel extends Origin {
    override def preferredName: String = "catches"

    override def shortPosition: String = "generated"

    override def context: String = "[At label generated for catch blocks]"

    override def inlineContext: String = "[Catch label]"
  }

  case object FinallyLabel extends Origin {
    override def preferredName: String = "finally"

    override def shortPosition: String = "generated"

    override def context: String = "[At label generated for finally]"

    override def inlineContext: String = "[Finally label]"
  }

  case object ExcBeforeLoop extends Origin {
    override def preferredName: String = "excBeforeLoop"

    override def shortPosition: String = "generated"

    override def context: String = "[At variable generated to contain exc before loop]"

    override def inlineContext: String = "[Exception before loop]"
  }

case class ImplicitLabelOrigin(inner: Origin) extends Origin {
  override def preferredName: String = "loop"
  override def shortPosition: String = inner.shortPosition
  override def context: String = inner.context
  override def inlineContext: String = inner.inlineContext
}

  case class CudaIndexVariableOrigin(dim: RefCudaVecDim[_]) extends Origin {
    override def preferredName: String =
      dim.vec.name + dim.name.toUpperCase

    override def context: String = s"At: [Variable for dimension ${dim.name} of ${dim.vec.name}]"
    override def inlineContext: String = s"[Variable for dimension ${dim.name} of ${dim.vec.name}]"
    override def shortPosition: String = "generated"
  }

  case class JavaFieldOrigin(fields: JavaFields[_], idx: Int) extends Origin {
    override def preferredName: String = fields.decls(idx).name
    override def shortPosition: String = fields.decls(idx).o.shortPosition
    override def context: String = fields.o.context
    override def inlineContext: String = fields.decls(idx).o.inlineContext
  }

  case class JavaLocalOrigin(locals: JavaLocalDeclaration[_], idx: Int) extends Origin {
    override def preferredName: String = locals.decls(idx).name
    override def shortPosition: String = locals.decls(idx).o.shortPosition
    override def context: String = locals.o.context
    override def inlineContext: String = locals.decls(idx).o.inlineContext
  }

  case class JavaConstructorOrigin(cons: JavaConstructor[_]) extends Origin {
    override def preferredName: String = cons.name
    override def shortPosition: String = cons.o.shortPosition
    override def context: String = cons.o.context
    override def inlineContext: String = cons.o.inlineContext
  }

  case class JavaMethodOrigin(method: JavaMethod[_]) extends Origin {
    override def preferredName: String = method.name
    override def shortPosition: String = method.o.shortPosition
    override def context: String = method.o.context
    override def inlineContext: String = method.o.inlineContext
  }

  case class JavaAnnotationMethodOrigin(method: JavaAnnotationMethod[_]) extends Origin {
    override def preferredName: String = method.name
    override def shortPosition: String = method.o.shortPosition
    override def context: String = method.o.context
    override def inlineContext: String = method.o.inlineContext
  }

  case class JavaInstanceClassOrigin(cls: JavaClassOrInterface[_]) extends Origin {
    override def preferredName: String = cls.name
    override def shortPosition: String = cls.o.shortPosition
    override def context: String = cls.o.context
    override def inlineContext: String = cls.o.inlineContext
  }

  case class JavaStaticsClassOrigin(cls: JavaClassOrInterface[_]) extends Origin {
    override def preferredName: String = cls.name + "Statics"
    override def shortPosition: String = cls.o.shortPosition
    override def context: String = cls.o.context
    override def inlineContext: String = cls.o.inlineContext
  }

  case class JavaStaticsClassSingletonOrigin(cls: JavaClassOrInterface[_]) extends Origin {
    override def preferredName: String = cls.name + "StaticsSingleton"
    override def shortPosition: String = cls.o.shortPosition
    override def context: String = cls.o.context
    override def inlineContext: String = cls.o.inlineContext
  }

  case class JavaInlineArrayInitializerOrigin(inner: Origin) extends Origin {
    override def preferredName: String = "arrayInitializer"
    override def shortPosition: String = inner.shortPosition
    override def context: String = inner.context
    override def inlineContext: String = inner.inlineContext
  }

  case object ThisVar extends Origin {
    override def preferredName: String = "this"
    override def shortPosition: String = "generated"
    override def context: String = "[At node generated to store the this value for constructors]"
    override def inlineContext: String = "this"
  }

  case class ExtractOrigin(name: String) extends Origin {
    override def preferredName: String = name
    override def shortPosition: String = "generated"
    override def context: String = "[At extracted expression]"
    override def inlineContext: String = "[Extracted expression]"
  }

  case class SilverPositionOrigin(node: silver.Positioned) extends Origin {
    override def preferredName: String = "unknown"
    override def shortPosition: String = node.pos match {
      case pos: AbstractSourcePosition => s"${pos.start.line}:${pos.start.column}"
      case _ => "unknown"
    }
    override def context: String = node.pos match {
      case NoPosition => "[Unknown position from silver parse tree]"
      case pos: AbstractSourcePosition =>
        val (start, end) = (pos.start, pos.end.getOrElse(pos.start))
        ReadableOrigin(RWFile(pos.file.toFile), start.line-1, end.line-1, Some((start.column-1, end.column-1))).context
      case other => s"[Unknown silver position kind: $other]"
    }
    override def inlineContext: String = InputOrigin.compressInlineText(node.toString)
  }

[pieter-bos]

Naming:

• Just unknown:
  • Because it's not referring to a declaration
  • Because it's not used for output (e.g. DiagnosticOrigin)
  • Because the specification of the name from the input is delayed
  • Because of lazyness :)
• The formal source name, currently just one string
  • From user text
  • From the JRE via reflection
• An appropriate constant for a generated definition
• Derived from another origin
  • With a prefix
  • With a postfix
• Derived from a type

[pieter-bos]

Pointing:

• Text explaining we don't know how to point to something:
  • Node spans across multiple files
  • Node is not actually output (such as DiagnosticOrigin)
  • The input is not re-readable (contrived; from stdin)
  • Loaded from reflection
  • Generated definition, not for any particular other definition (e.g. type)
  • Generated definition, associated to a particular other definition (e.g. this)
  • Silver NoPosition
• A range from text input:
  • In a file
  • In a literal string (from the test framework)
  • Silver AbstractSourcePosition
• Forward a different origin unchanged
  • For a generated definition, associated to a particular other definition (e.g. lock_invariant)
• Interpreted, which points to two ranges
• Inlined, which points to 1000 ranges
• ??? lmao

[pieter-bos]

Random observations:

• We should make a bunch of SourceNameOrigin's for different kinds of name, which should also deal somewhat nicely with snake_case, UPPER_SNAKE_CASE, CamelCase and camelCase, in combination with pre/postfixes
• Generated definitions that associate to another definition should be a special kind of context that explains "the this parameter for this method"
• For all other don't knows I don't think we care about the context that much, because we will never (?) print errors about them
• If we keep the context structure fairly simple we can easily group context's by file and close-by file range
• Simple context structure -> no formal explanation for the reason of nodes existing, but I doubt its use anyway. We should instead of course make a time traveling debugger! :)

[pieter-bos]

List of all blame implementations

case class FilterExpectedErrorBlame(otherwise: Blame[VerificationFailure], expectedError: ExpectedError) extends Blame[VerificationFailure] {
  override def blame(error: VerificationFailure): Unit =
    if(expectedError.errorCode.r.matches(error.code)) {
      expectedError.trip(error)
    } else {
      otherwise.blame(error)
    }
}

case class PostBlameSplit[T >: PostconditionFailed <: VerificationFailure](blames: Map[AccountedDirection, Blame[PostconditionFailed]], default: Blame[T]) extends Blame[T] {
  override def blame(error: T): Unit = error match {
    case PostconditionFailed(path, failure, invokable) => path match {
      case Nil => throw BlamePathError
      case FailLeft :: tail => blames(FailLeft).blame(PostconditionFailed(tail, failure, invokable))
      case FailRight :: tail => blames(FailRight).blame(PostconditionFailed(tail, failure, invokable))
    }
    case other => default.blame(other)
  }
}

case class PreBlameSplit[T >: PreconditionFailed <: VerificationFailure](blames: Map[AccountedDirection, Blame[PreconditionFailed]], default: Blame[T]) extends Blame[T] {
  override def blame(error: T): Unit = error match {
    case PreconditionFailed(path, failure, invokable) => path match {
      case Nil =>
        throw BlamePathError
      case FailLeft :: tail => blames(FailLeft).blame(PreconditionFailed(tail, failure, invokable))
      case FailRight :: tail => blames(FailRight).blame(PreconditionFailed(tail, failure, invokable))
    }
    case other => default.blame(other)
  }
}

case class PanicBlame(message: String) extends Blame[VerificationFailure] {
  override def blame(error: VerificationFailure): Unit =
    throw BlameUnreachable(message, error)
}

trait UnsafeDontCare[T <: VerificationFailure] extends Blame[T] with LazyLogging {
  def reason: String

  override def blame(error: T): Unit = {
    logger.debug(s"We do not care about ${error.code} here, since $reason:")
    logger.debug(error.toString)
  }
}

case class NoContext(inner: Blame[PreconditionFailed]) extends Blame[InvocationFailure] {
  override def blame(error: InvocationFailure): Unit = error match {
    case pre: PreconditionFailed => inner.blame(pre)
    case ctx: ContextEverywhereFailedInPre => PanicBlame("Function or method does not list any context_everywhere clauses, so cannot fail on a context_everywhere clause.").blame(ctx)
  }
}

trait Origin extends Blame[VerificationFailure]

case class BlameCollector() extends Blame[VerificationFailure] {
  val errs: ArrayBuffer[VerificationFailure] = ArrayBuffer()

  override def blame(error: VerificationFailure): Unit =
    errs += error
}

  case class AssertPassedNontrivialUnsatisfiable(contract: ApplicableContract[_]) extends Blame[ExpectedErrorFailure] {
    override def blame(error: ExpectedErrorFailure): Unit = error match {
      case _: ExpectedErrorTrippedTwice =>
        // Ignore: Carbon may report the assert failed, even when the contract is not well-formed.
      case ExpectedErrorNotTripped(_) =>
        contract.blame.blame(NontrivialUnsatisfiable(contract))
    }
  }

  case class NotWellFormedIgnoreCheckSat(err: ExpectedError) extends Blame[VerificationFailure] {
    override def blame(error: VerificationFailure): Unit =
      err.trip(error)
  }

  case class ModelPostconditionFailed(process: ModelProcess[_]) extends Blame[CallableFailure] {
    override def blame(error: CallableFailure): Unit = error match {
      case post: PostconditionFailed => process.blame.blame(post)
      case ctx: ContextEverywhereFailedInPost =>
        PanicBlame("Generated methods for models do not have context_everywhere clauses.").blame(ctx)
      case _: SignalsFailed | _: ExceptionNotInSignals =>
        PanicBlame("Generated methods for models do not throw exceptions.").blame(error)
    }
  }

  case class InsufficientPermissionForModelField(modelDeref: ModelDeref[_]) extends Blame[InsufficientPermission] {
    override def blame(error: InsufficientPermission): Unit = modelDeref.blame.blame(ModelInsufficientPermission(modelDeref))
  }

  case class InstanceNullPreconditionFailed(inner: Blame[InstanceNull], inv: InvokingNode[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit =
      inner.blame(InstanceNull(inv))
  }

  case class FramedArraySubscriptBlame(blame: Blame[ArrayLocationError]) extends Blame[ArraySubscriptError] {
    override def blame(error: ArraySubscriptError): Unit = {
      error match {
        case error: ArrayLocationError => blame.blame(error)
        case ArrayInsufficientPermission(node) => PointsToDeref.blame(error)
      }
    }
  }

  case class FramedPointerDerefBlame(blame: Blame[PointerLocationError]) extends Blame[PointerDerefError] {
    override def blame(error: PointerDerefError): Unit = {
      error match {
        case error: PointerLocationError => blame.blame(error)
        case PointerInsufficientPermission(node) => PointsToDeref.blame(error)
      }
    }
  }

  case class ArrayValuesPreconditionFailed(values: Values[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit = error.path match {
      case Seq(FailLeft) =>
        values.blame.blame(ArrayValuesNull(values))
      case Seq(FailRight, FailLeft) =>
        values.blame.blame(ArrayValuesFromNegative(values))
      case Seq(FailRight, FailRight, FailLeft) =>
        values.blame.blame(ArrayValuesFromToOrder(values))
      case Seq(FailRight, FailRight, FailRight, FailLeft) =>
        values.blame.blame(ArrayValuesToLength(values))
      case Seq(FailRight, FailRight, FailRight, FailRight) =>
        values.blame.blame(ArrayValuesPerm(values))
      case other => throw Unreachable(s"Invalid postcondition path sequence: $other")
    }
  }

  case class ForkInstanceInvocation(fork: Fork[_]) extends Blame[InstanceInvocationFailure] {
    override def blame(error: InstanceInvocationFailure): Unit = error match {
      case InstanceNull(_) => fork.blame.blame(ForkNull(fork))
      case PreconditionFailed(Nil, _, _) => throw BlamePathError
      case PreconditionFailed(FailLeft :: _, _, _) => fork.blame.blame(RunnableNotIdle(fork))
      case PreconditionFailed(FailRight :: _, failure, _) => fork.blame.blame(RunnablePreconditionNotEstablished(fork, failure))
      case ContextEverywhereFailedInPre(_, _) => PanicBlame("fork method does not have c_e").blame(error)
    }
  }

  case class JoinInstanceInvocation(join: Join[_]) extends Blame[InstanceInvocationFailure] {
    override def blame(error: InstanceInvocationFailure): Unit = error match {
      case InstanceNull(_) => join.blame.blame(JoinNull(join))
      case PreconditionFailed(_, _, _) => join.blame.blame(RunnableNotRunning(join))
      case ContextEverywhereFailedInPre(_, _) => PanicBlame("join method does not have c_e").blame(error)
    }
  }

  case class UnlockInvariantFoldFailed(unlock: Unlock[_]) extends Blame[FoldFailed] {
    override def blame(error: FoldFailed): Unit =
      unlock.blame.blame(UnlockInvariantFailed(unlock, error.failure))
  }

  case class UnlockHeldExhaleFailed(unlock: Unlock[_]) extends Blame[ExhaleFailed] {
    override def blame(error: ExhaleFailed): Unit =
      unlock.blame.blame(LockTokenNotHeld(unlock, error.failure))
  }

  case class CommitFailedFoldFailed(commit: Commit[_]) extends Blame[FoldFailed] {
    override def blame(error: FoldFailed): Unit =
      commit.blame.blame(CommitFailed(commit, error.failure))
  }

  case class NotifyAssertFailed(not: Notify[_]) extends Blame[AssertFailed] {
    override def blame(error: AssertFailed): Unit =
      not.blame.blame(NotifyFailed(not, error.failure))
  }

  case class LockLockObjectNull(lock: Lock[_]) extends Blame[InstanceInvocationFailure] {
    override def blame(error: InstanceInvocationFailure): Unit = error match {
      case InstanceNull(_) => lock.blame.blame(LockObjectNull(lock))
      case failure: InvocationFailure => PanicBlame("elp").blame(failure)
    }
  }

  case class CommittedLockObjectNull(commit: Committed[_]) extends Blame[InstanceInvocationFailure] {
    override def blame(error: InstanceInvocationFailure): Unit = error match {
      case InstanceNull(_) => commit.blame.blame(LockObjectNull(commit))
      case failure: InvocationFailure => PanicBlame("elp").blame(failure)
    }
  }

  case class NotCommittedAssertFailed(lock: Lock[_]) extends Blame[AssertFailed] {
    override def blame(error: AssertFailed): Unit =
      lock.blame.blame(LockNotCommitted(lock))
  }

  case class FramedProofLoopInvariantFailed(proof: FramedProof[_]) extends Blame[LoopInvariantFailure] {
    override def blame(error: LoopInvariantFailure): Unit = error match {
      case LoopInvariantNotEstablished(failure, _) =>
        proof.blame.blame(FramedProofPreFailed(failure, proof))
      case LoopInvariantNotMaintained(failure, _) =>
        proof.blame.blame(FramedProofPostFailed(failure, proof))
    }
  }

  case class SendFailedExhaleFailed(send: Send[_]) extends Blame[ExhaleFailed] {
    override def blame(error: ExhaleFailed): Unit =
      send.blame.blame(SendFailed(error.failure, send))
  }

  case class ParBlockNotInjective(block: ParBlock[_], expr: Expr[_]) extends Blame[ReceiverNotInjective] {
    override def blame(error: ReceiverNotInjective): Unit =
      block.blame.blame(ParPredicateNotInjective(block, expr))
  }

  case class ParStatementExhaleFailed(region: ParRegion[_]) extends Blame[ExhaleFailed] {
    override def blame(error: ExhaleFailed): Unit =
      region.blame.blame(ParPreconditionFailed(error.failure, region))
  }

  case class ParSequenceProofFailed(region: ParRegion[_]) extends Blame[FramedProofFailure] {
    override def blame(error: FramedProofFailure): Unit = error match {
      case preFailed @ FramedProofPreFailed(_, _) =>
        PanicBlame("The precondition in the framed proof of a par sequence is `true`").blame(preFailed)
      case FramedProofPostFailed(failure, _) =>
        region.blame.blame(ParPreconditionFailed(failure, region))
    }
  }

  case class ParBlockProofFailed(block: ParBlock[_]) extends Blame[FramedProofFailure] {
    override def blame(error: FramedProofFailure): Unit = error match {
      case FramedProofPreFailed(failure, _) =>
        // PB: this is a bit dubious, maybe instead inhale the par precondition and panic here?
        block.blame.blame(ParPreconditionFailed(failure, block))
      case FramedProofPostFailed(failure, _) =>
        block.blame.blame(ParBlockPostconditionFailed(failure, block))
    }
  }

  case class ParInvariantCannotBeExhaled(invariant: ParInvariant[_]) extends Blame[ExhaleFailed] {
    override def blame(error: ExhaleFailed): Unit =
      invariant.blame.blame(ParInvariantNotEstablished(error.failure, invariant))
  }

  case class ParAtomicCannotBeExhaled(atomic: ParAtomic[_]) extends Blame[ExhaleFailed] {
    override def blame(error: ExhaleFailed): Unit =
      atomic.blame.blame(ParInvariantNotMaintained(error.failure, atomic))
  }

  case class ParBarrierInvariantExhaleFailed(barrier: ParBarrier[_]) extends Blame[ExhaleFailed] {
    override def blame(error: ExhaleFailed): Unit =
      barrier.blame.blame(ParBarrierInvariantBroken(error.failure, barrier))
  }

  case class ParBarrierExhaleFailed(barrier: ParBarrier[_]) extends Blame[ExhaleFailed] {
    override def blame(error: ExhaleFailed): Unit =
      barrier.blame.blame(ParBarrierNotEstablished(error.failure, barrier))
  }

  case class ParBarrierProofFailed(barrier: ParBarrier[_]) extends Blame[FramedProofFailure] {
    override def blame(error: FramedProofFailure): Unit = error match {
      case FramedProofPreFailed(_, _) =>
        PanicBlame("Barrier consistency proof requires true").blame(error)
      case FramedProofPostFailed(failure, _) =>
        barrier.blame.blame(ParBarrierInconsistent(failure, barrier))
    }
  }

  case class ContextEverywherePreconditionFailed(inv: InvokingNode[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit =
      inv.blame.blame(ContextEverywhereFailedInPre(error.failure, inv))
  }

  case class ContextEverywherePostconditionFailed(app: ContractApplicable[_]) extends Blame[PostconditionFailed] {
    override def blame(error: PostconditionFailed): Unit =
      app.blame.blame(ContextEverywhereFailedInPost(error.failure, app))
  }

  case class AssertPassedRefuteFailed(refute: Refute[_]) extends Blame[ExpectedErrorFailure] {
    override def blame(error: ExpectedErrorFailure): Unit = error match {
      case err: ExpectedErrorTrippedTwice =>
        PanicBlame("A single assert cannot trip twice").blame(err)
      case ExpectedErrorNotTripped(_) =>
        refute.blame.blame(RefuteFailed(refute))
    }
  }

  case class ScaleNegativePreconditionFailed(scale: Scale[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit =
      scale.blame.blame(ScaleNegative(scale))
  }

  case class ArrayNullOptNone(inner: Blame[ArrayNull], expr: Expr[_]) extends Blame[OptionNone] {
    override def blame(error: OptionNone): Unit =
      inner.blame(ArrayNull(expr))
  }

  case class ArrayBoundsPreconditionFailed(inner: Blame[ArrayBounds], subscript: Node[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit =
      inner.blame(ArrayBounds(subscript))
  }

  case class ArrayFieldInsufficientPermission(inner: Blame[ArrayInsufficientPermission], expr: Expr[_]) extends Blame[InsufficientPermission] {
    override def blame(error: InsufficientPermission): Unit =
      inner.blame(ArrayInsufficientPermission(expr))
  }

  case class NotLeftPreconditionFailed(get: GetLeft[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit =
      get.blame.blame(NotLeft(get))
  }

  case class NotRightPreconditionFailed(get: GetRight[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit =
      get.blame.blame(NotRight(get))
  }

  case class RatZFracPreconditionFailed(inner: Blame[CoerceRatZFracFailed], expr: Expr[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit =
      inner.blame(CoerceRatZFracFailed(expr))
  }

  case class RatFracPreconditionFailed(inner: Blame[CoerceRatFracFailed], expr: Expr[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit =
      inner.blame(CoerceRatFracFailed(expr))
  }

  case class ZFracFracPreconditionFailed(inner: Blame[CoerceZFracFracFailed], expr: Expr[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit =
      inner.blame(CoerceZFracFracFailed(expr))
  }

  case class OptionNonePreconditionFailed(access: OptGet[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit =
      access.blame.blame(OptionNone(access))
  }

  case class PointerNullOptNone(inner: Blame[PointerNull], expr: Expr[_]) extends Blame[OptionNone] {
    override def blame(error: OptionNone): Unit =
      inner.blame(PointerNull(expr))
  }

  case class PointerBoundsPreconditionFailed(inner: Blame[PointerBounds], expr: Node[_]) extends Blame[PreconditionFailed] {
    override def blame(error: PreconditionFailed): Unit =
      inner.blame(PointerBounds(expr))
  }

  case class PointerFieldInsufficientPermission(inner: Blame[PointerInsufficientPermission], expr: Expr[_]) extends Blame[InsufficientPermission] {
    override def blame(error: InsufficientPermission): Unit =
      inner.blame(PointerInsufficientPermission(expr))
  }

  case class ThrowNullAssertFailed(t: Throw[_]) extends Blame[AssertFailed] {
    override def blame(error: AssertFailed): Unit =
      t.blame.blame(ThrowNull(t))
  }

  case class PackageThrowsAssertFailed(pack: WandPackage[_]) extends Blame[AssertFailed] {
    override def blame(error: AssertFailed): Unit = pack.blame.blame(PackageThrows(pack))
  }

  case class SignalsClosedPostconditionFailed(method: AbstractMethod[_]) extends Blame[PostconditionFailed] {
    override def blame(error: PostconditionFailed): Unit =
      method.blame.blame(ExceptionNotInSignals(method))
  }

  case class AssertFailedSignalsNotClosed(method: AbstractMethod[_]) extends Blame[AssertFailed] {
    override def blame(error: AssertFailed): Unit =
      method.blame.blame(ExceptionNotInSignals(method))
  }

  case class SignalsFailedPostconditionFailed(method: AbstractMethod[_]) extends Blame[PostconditionFailed] {
    override def blame(error: PostconditionFailed): Unit =
      method.blame.blame(SignalsFailed(error.failure, method))
  }

  case class KernelNotInjective(kernel: CGpgpuKernelSpecifier[_]) extends Blame[ReceiverNotInjective] {
    override def blame(error: ReceiverNotInjective): Unit =
      kernel.blame.blame(KernelPredicateNotInjective(kernel, error.resource))
  }

  case class KernelParFailure(kernel: CGpgpuKernelSpecifier[_]) extends Blame[ParBlockFailure] {
    override def blame(error: ParBlockFailure): Unit = error match {
      case ParPredicateNotInjective(_, predicate) =>
        kernel.blame.blame(KernelPredicateNotInjective(kernel, predicate))
      case ParPreconditionFailed(_, _) =>
        PanicBlame("Kernel parallel block precondition cannot fail, since an identical predicate is required before.").blame(error)
      case ParBlockPostconditionFailed(failure, _) =>
        kernel.blame.blame(KernelPostconditionFailed(failure, kernel))
      case ParBlockMayNotThrow(_) =>
        PanicBlame("Please don't throw exceptions from a gpgpu kernel, it's not polite.").blame(error)
    }
  }

  case class KernelBarrierFailure(barrier: GpgpuBarrier[_]) extends Blame[ParBarrierFailure] {
    override def blame(error: ParBarrierFailure): Unit = error match {
      case ParBarrierNotEstablished(failure, _) =>
        barrier.blame.blame(KernelBarrierNotEstablished(failure, barrier))
      case ParBarrierInconsistent(failure, _) =>
        barrier.blame.blame(KernelBarrierInconsistent(failure, barrier))
      case ParBarrierMayNotThrow(_) =>
        PanicBlame("Please don't throw exceptions from a gpgpu barrier, it's not polite.").blame(error)
      case ParBarrierInvariantBroken(failure, _) =>
        barrier.blame.blame(KernelBarrierInvariantBroken(failure, barrier))
    }
  }

  case object LibraryFileBlame extends Blame[VerificationFailure] {
    override def blame(error: VerificationFailure): Unit =
      throw LibraryFileError(error)
  }

case object NoErrors extends Blame[VerificationFailure] {
  override def blame(error: VerificationFailure): Unit =
    fail(error.toString)
}

case class ExpectError()(implicit val registry: ExpectedErrorsRegistry) extends Blame[VerificationFailure] {
  var tripped = false
  registry.errors += this

  override def blame(error: VerificationFailure): Unit = tripped = true
}

class ExpectedError(val errorCode: String, val errorRegion: Origin, val blame: Blame[ExpectedErrorFailure]) extends LazyLogging {
  var tripped: Option[VerificationFailure] = None

  def trip(failure: VerificationFailure): Unit =
    tripped match {
      case None =>
        logger.debug(s"Swallowing error code $errorCode at ${errorRegion.shortPosition}")
        tripped = Some(failure)
      case Some(leftFailure) =>
        blame.blame(ExpectedErrorTrippedTwice(this, leftFailure, failure))
    }

  def signalDone(): Unit =
    if(tripped.isEmpty) {
      blame.blame(ExpectedErrorNotTripped(this))
    }
}

[pieter-bos]

Final handling of VerificationFailure:

• account an expected error occured
• throw an exception for ostensibly unreachable error conditions
• ignore (e.g. when duplicated or definitionally irrelevant)
• store in buffer

[pieter-bos]

Transforming errors:

• One-to-one:
  • Filtering an expected error by code
  • select next transformation by the path
  • select next transformation by subtype
  • explicit different error, because of a different encoding
    • may or may not include contractfailure

[pieter-bos]

Proposal:

• All assertions become AccountedPredicate, which I want to refactor to a ListMap[Tag, Expr]
• Although blames can accept a broader error than a case class, the backend should only have blames of concrete errors. This makes it so we can enumerate all hypothetical errors (potentially over all tags in the current assertion)
• We want to support "hypothetical" errors, so there should be an AbstractVerificationFailure or so, and a VerificationFailure that completes an AbstractVerificationFailure, both either with or without ContractFailure.
  • The abstract failure should carry the tag for all assertion-type errors, and stuff like a relevant node.
  • the concrete failure should carry the abstract failure, the path conditions and optionally the contractfailure
• Abstract failures should optionally carry a cancellative grouping, to represent expected errors. This should be arranged via a canary node that always throws an error (e.g. ExpectedErrorNotTripped)
• Abstract failures should optionally carry an explanation why an error can never occur, to replace PanicBlame.
• Ignoring an error is the same as a one-member cancellative grouping
• We should in principle just always return a list of errors, preferably Seq[FutureError], FutureError { def future: Future[Option[VerificationFailure]]; def failure: AbstractVerificationFailure }

Under all these conditions we can support having a list of hypothetical errors, and blames may be functional rather than imperative.