Use separate Info specifically for smoke detection

Author: bruggerl

src/main/scala/viper/silver/plugin/standard/refute/RefuteErrors.scala

@@ -7,16 +7,16 @@
 package viper.silver.plugin.standard.refute
 
 import viper.silver.ast.FalseLit
-import viper.silver.cfg.utility.IdInfo
+import viper.silver.plugin.standard.smoke.SmokeDetectionInfo
 import viper.silver.verifier._
 
 sealed abstract class RefuteError extends ExtensionAbstractVerificationError
 sealed abstract class RefuteErrorReason extends ExtensionAbstractErrorReason
 
 case class RefuteFailed(override val offendingNode: Refute, override val reason: ErrorReason, override val cached: Boolean = false) extends RefuteError {
   override val id = "refute.failed"
-  override val text = if (offendingNode.exp.isInstanceOf[FalseLit] && offendingNode.info.getUniqueInfo[IdInfo].isDefined)
-    "Smoke detected: False could be proven here (which should never hold)." else
+  override val text: String = if (offendingNode.exp.isInstanceOf[FalseLit] && offendingNode.info.getUniqueInfo[SmokeDetectionInfo].isDefined)
+    "Smoke detection: False could be proven here (which should never hold)." else
     "Refute holds in all cases or could not be reached (e.g. see Silicon `numberOfErrorsToReport`)."
 
   override def withNode(offendingNode: errors.ErrorNode = this.offendingNode): RefuteFailed =

src/main/scala/viper/silver/plugin/standard/smoke/SmokeDetectionPlugin.scala

@@ -5,7 +5,6 @@ import viper.silver.ast._
 import viper.silver.ast.utility.ViperStrategy
 import viper.silver.cfg.silver.SilverCfg
 import viper.silver.cfg.silver.SilverCfg.SilverBlock
-import viper.silver.cfg.utility.IdInfo
 import viper.silver.parser.FastParser
 import viper.silver.plugin.standard.refute.Refute
 import viper.silver.plugin.{ParserPluginTemplate, SilverPlugin}
@@ -85,7 +84,7 @@ class SmokeDetectionPlugin(@unused reporter: viper.silver.reporter.Reporter,
 
       ViperStrategy.Slim({
         case r@Refute(_) =>
-          val idInfo = r.info.getUniqueInfo[IdInfo]
+          val idInfo = r.info.getUniqueInfo[SmokeDetectionInfo]
 
           if (idInfo.isDefined &&
             !result._1.contains(idInfo.get.id) && // not marked reachable
@@ -124,7 +123,7 @@ class SmokeDetectionPlugin(@unused reporter: viper.silver.reporter.Reporter,
    * @return a [[Refute]] instance with with the `exp` set to `false` and the given position and ID
    */
   private def refuteFalse(pos: Position, id: Int): Refute = {
-    Refute(FalseLit()(pos))(pos, IdInfo(id))
+    Refute(FalseLit()(pos))(pos, SmokeDetectionInfo(id))
   }
 
   /**
@@ -176,7 +175,7 @@ class SmokeDetectionPlugin(@unused reporter: viper.silver.reporter.Reporter,
           unreachableSuccessors = true
         case refute: Refute if refute.exp.isInstanceOf[FalseLit] =>
           // Encountered `refute false` statement -> add ID to list if it is reachable
-          val idInfo = refute.info.getUniqueInfo[IdInfo]
+          val idInfo = refute.info.getUniqueInfo[SmokeDetectionInfo]
 
           if (idInfo.isDefined) {
             val id = idInfo.get.id
@@ -222,3 +221,15 @@ class SmokeDetectionPlugin(@unused reporter: viper.silver.reporter.Reporter,
     successors.forall(s => collectRefutesToKeepUntilExit(cfg, s, exits, seen, refutesToKeep, seenRefutes, unreachableSuccessors))
   }
 }
+
+/**
+ * An info used to mark AST nodes (more specifically, `refute false` statements) as used in smoke detection,
+ * also assigning a unique identifier to it.
+ *
+ * @param id the ID of the node
+ */
+case class SmokeDetectionInfo(id: Int) extends Info {
+  override def comment: Seq[String] = Seq(s"`refute false` #$id")
+
+  override def isCached: Boolean = false
+}