add enableDebug config flag

src/main/scala/Config.scala

@@ -784,6 +784,12 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
+  val enableDebugging: ScallopOption[Boolean] = opt[Boolean]("enableDebugging",
+    descr = "Enable debugging mode",
+    default = Some(false),
+    noshort = true
+  )
+
   /* Option validation (trailing file argument is validated by parent class) */
 
   validateOpt(prover) {

src/main/scala/debugger/SiliconDebugger.scala

@@ -2,7 +2,7 @@ package debugger
 
 import viper.silicon.common.collections.immutable.InsertionOrderedSet
 import viper.silicon.decider._
-import viper.silicon.interfaces.{Failure, SiliconFailureContext, Success, VerificationResult}
+import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, SiliconFailureContext, Success, VerificationResult}
 import viper.silicon.rules.evaluator
 import viper.silicon.state.terms.{False, Term}
 import viper.silicon.state.{IdentifierFactory, State}
@@ -90,8 +90,13 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
   var counter: Int = 0
 
   def startDebugger(): Unit = {
+    if(!Verifier.config.enableDebugging()){
+      println("Debugging mode is disabled")
+      return
+    }
+
     if (failures.isEmpty) {
-      println("Nothing to debug. All assertions verified.")
+      println("No failures found. Debugging mode terminated.")
       return
     }
 
@@ -131,7 +136,7 @@ class SiliconDebugger(verificationResults: List[VerificationResult],
       println(s"\nVerification result $idx:")
       val currResult: Failure = failures(idx)
       println(s"$currResult")
-      val failureContexts = (currResult.message.failureContexts filter (_.isInstanceOf[SiliconFailureContext])) map (_.asInstanceOf[SiliconFailureContext])
+      val failureContexts = (currResult.message.failureContexts filter (_.isInstanceOf[SiliconDebuggingFailureContext])) map (_.asInstanceOf[SiliconDebuggingFailureContext])
 
       if (failureContexts.isEmpty) {
         println(s"Debugging results are not available. No failure context found.")

src/main/scala/decider/Decider.scala

@@ -227,10 +227,14 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     /* Assuming facts */
 
     def startDebugSubExp(): Unit = {
-      debugExpStack = InsertionOrderedSet[DebugExp]().empty +: debugExpStack
+      if (Verifier.config.enableDebugging()) {
+        debugExpStack = InsertionOrderedSet[DebugExp]().empty +: debugExpStack
+      }
     }
 
     private def popDebugSubExp(): InsertionOrderedSet[DebugExp] = {
+      if (!Verifier.config.enableDebugging()) return InsertionOrderedSet.empty
+
       if (debugExpStack.isEmpty) {
         InsertionOrderedSet.empty // TODO ake: this should not happen
       } else {
@@ -241,11 +245,15 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
     }
 
     def finishDebugSubExp(description : String): Unit ={
+      if (!Verifier.config.enableDebugging()) return
+
       val debugExp = DebugExp.createInstance(description = description, children = popDebugSubExp())
       addDebugExp(debugExp)
     }
 
     private def addDebugExp(e: DebugExp): Unit = {
+      if (!Verifier.config.enableDebugging()) return
+
       if(e.getTerms.nonEmpty && e.getTerms.forall(t => PathConditions.isGlobal(t))){
         pathConditions.addGlobalDebugExp(e)
       }else{
@@ -283,15 +291,17 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
       if (filteredTerms.nonEmpty) assumeWithoutSmokeChecks(filteredTerms, e)
     }
 
-    private def assumeWithoutSmokeChecks(terms: InsertionOrderedSet[Term], e : DebugExp) = {
+    private def assumeWithoutSmokeChecks(terms: InsertionOrderedSet[Term], e: DebugExp) = {
       val assumeRecord = new DeciderAssumeRecord(terms)
       val sepIdentifier = symbExLog.openScope(assumeRecord)
 
       /* Add terms to Silicon-managed path conditions */
       terms foreach pathConditions.add
 
-      val debugExp = e.withTerms(terms)
-      addDebugExp(debugExp)
+      if(Verifier.config.enableDebugging()){
+        val debugExp = e.withTerms(terms)
+        addDebugExp(debugExp)
+      }
 
       /* Add terms to the prover's assumptions */
       terms foreach prover.assume
@@ -368,26 +378,26 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
 
     def fresh(id: String, sort: Sort, pType: PType): Var = {
       val term = prover_fresh[Var](id, Nil, sort)
-      debugVariableTypes += (term.id.name -> pType)
+      if(Verifier.config.enableDebugging()) debugVariableTypes += (term.id.name -> pType)
       term
     }
 
     def fresh(s: Sort, pType: PType): Var = {
       val term = prover_fresh[Var]("$t", Nil, s)
-      debugVariableTypes += (term.id.name -> pType)
+      if(Verifier.config.enableDebugging()) debugVariableTypes += (term.id.name -> pType)
       term
     }
 
     def fresh(v: ast.AbstractLocalVar): Var = {
       val term = prover_fresh[Var](v.name, Nil, symbolConverter.toSort(v.typ))
-      debugVariableTypes += (term.id.name -> extractPTypeFromExp(v))
+      if(Verifier.config.enableDebugging()) debugVariableTypes += (term.id.name -> extractPTypeFromExp(v))
       term
     }
 
     def freshARP(id: String = "$k"): (Var, Term) = {
       val permVar = prover_fresh[Var](id, Nil, sorts.Perm)
       val permVarConstraints = IsReadPermVar(permVar)
-      debugVariableTypes += (permVar.id.name -> PPrimitiv("Perm")())
+      if(Verifier.config.enableDebugging()) debugVariableTypes += (permVar.id.name -> PPrimitiv("Perm")())
       (permVar, permVarConstraints)
     }
 

src/main/scala/interfaces/Verification.scala

@@ -105,6 +105,37 @@ case class Failure/*[ST <: Store[ST],
 }
 
 case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
+                                 counterExample: Option[Counterexample],
+                                 reasonUnknown: Option[String]) extends FailureContext {
+  lazy val branchConditionString: String = {
+    if(branchConditions.nonEmpty) {
+      val branchConditionsString =
+        branchConditions
+          .map(bc => s"$bc [ ${bc.pos} ] ")
+          .mkString("\t\t"," ~~> ","")
+
+      s"\n\t\tunder branch conditions:\n$branchConditionsString"
+    } else {
+      ""
+    }
+  }
+
+  lazy val counterExampleString: String = {
+    counterExample.fold("")(ce => s"\n\t\tcounterexample:\n$ce")
+  }
+
+  lazy val reasonUnknownString: String = {
+    if (reasonUnknown.isDefined) {
+      s"\nPotential prover incompleteness: ${reasonUnknown.get}"
+    } else {
+      ""
+    }
+  }
+
+  override lazy val toString: String = branchConditionString + counterExampleString + reasonUnknownString
+}
+
+case class SiliconDebuggingFailureContext(branchConditions: Seq[ast.Exp],
                                  counterExample: Option[Counterexample],
                                  reasonUnknown: Option[String],
                                  state: Option[State],
@@ -115,11 +146,11 @@ case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
                                  assumptions: InsertionOrderedSet[DebugExp],
                                  failedAssertion: Option[ast.Exp]) extends FailureContext {
   lazy val branchConditionString: String = {
-    if(branchConditions.nonEmpty) {
+    if (branchConditions.nonEmpty) {
       val branchConditionsString =
         branchConditions
           .map(bc => s"$bc [ ${bc.pos} ] ")
-          .mkString("\t\t"," ~~> ","")
+          .mkString("\t\t", " ~~> ", "")
 
       s"\n\t\tunder branch conditions:\n$branchConditionsString"
     } else {
@@ -147,17 +178,6 @@ case class SiliconFailureContext(branchConditions: Seq[ast.Exp],
     }
   }
 
-  lazy val nonInternalassumptionsString: String = {
-    if(assumptions.nonEmpty){
-      val nonInternalAssumptions = assumptions.filter(de => !de.isInternal)
-      val config = new DebugExpPrintConfiguration
-      config.isPrintInternalEnabled = false
-      s"\n\nassumptions:\n\t${nonInternalAssumptions.tail.foldLeft[String](nonInternalAssumptions.head.toString(config))((s, de) => de.toString(config) + "\n\t" + s)}"
-    }else{
-      ""
-    }
-  }
-
   lazy val allAssumptionsString: String = {
     if (assumptions.nonEmpty) {
       val config = new DebugExpPrintConfiguration

src/main/scala/rules/Evaluator.scala

@@ -224,7 +224,7 @@ object evaluator extends EvaluationRules {
                 val fvfLookup = Lookup(fa.field.name, fvfDef.sm, tRcvr)
                 val fr1 = s1.functionRecorder.recordSnapshot(fa, v1.decider.pcs.branchConditions, fvfLookup)
                 val s2 = s1.copy(functionRecorder = fr1)
-                val s3 = if (!s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s2))) else s2
+                val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s2))) else s2
                 Q(s3, fvfLookup, newFa, v1)
               } else {
                 v1.decider.assert(IsPositive(totalPermissions.replace(`?r`, tRcvr))) {
@@ -238,7 +238,7 @@ object evaluator extends EvaluationRules {
                     else
                       s1.possibleTriggers
                     val s2 = s1.copy(functionRecorder = fr1, possibleTriggers = possTriggers)
-                    val s3 = if (!s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s2))) else s2
+                    val s3 = if (Verifier.config.enableDebugging() && !s2.isEvalInOld) s2.copy(oldHeaps = s2.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s2))) else s2
                     Q(s3, fvfLookup, newFa, v1)}
               }
             case _ =>
@@ -272,7 +272,7 @@ object evaluator extends EvaluationRules {
                                        .recordFvfAndDomain(smDef1)
                   val s3 = s1.copy(functionRecorder = fr2/*,
                                    smCache = smCache1*/)
-                  val s4 = if (!s3.isEvalInOld) s3.copy(oldHeaps = s3.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s3))) else s3
+                  val s4 = if (Verifier.config.enableDebugging() && !s3.isEvalInOld) s3.copy(oldHeaps = s3.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s3))) else s3
                   Q(s4, smLookup, newFa, v1)}
               }})
 
@@ -286,7 +286,7 @@ object evaluator extends EvaluationRules {
             val debugOldLabel = getDebugOldLabel(fa)
             val newFa = if(s3.isEvalInOld) ast.FieldAccess(eArgs.head, fa.field)(e.pos, e.info, e.errT)
                         else ast.DebugLabelledOld(ast.FieldAccess(eArgs.head, fa.field)(), debugOldLabel)(e.pos, e.info, e.errT)
-            val s4 = if(!s3.isEvalInOld) s3.copy(oldHeaps = s3.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s3))) else s3
+            val s4 = if(Verifier.config.enableDebugging() && !s3.isEvalInOld) s3.copy(oldHeaps = s3.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s3))) else s3
             Q(s4, tSnap, newFa, v1)
           })
         })

src/main/scala/rules/Executor.scala

@@ -360,7 +360,7 @@ object executor extends ExecutionRules {
                   case column: HasLineColumn => s"line@${column.line + 1}"
                   case _ => s"line@unknown"
                 }
-                val s5 = s4.copy(oldHeaps = s4.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s4)))
+                val s5 = if(Verifier.config.enableDebugging()) s4.copy(oldHeaps = s4.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s4))) else s4
                 Q(s5, v2)
               case (Incomplete(_, _), s3, _) =>
                 createFailure(pve dueTo InsufficientPermission(fa), v2, s3, None)}}))
@@ -383,7 +383,7 @@ object executor extends ExecutionRules {
                   case column: HasLineColumn => s"line@${column.line + 1}"
                   case _ => s"line@unknown"
                 }
-                val s6 = s5.copy(oldHeaps = s5.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s5)))
+                val s6 = if(Verifier.config.enableDebugging()) s5.copy(oldHeaps = s5.oldHeaps + (debugOldLabel -> magicWandSupporter.getEvalHeap(s5))) else s5
                 Q(s6, v4)
               })
             })

src/main/scala/rules/SymbolicExecutionRules.scala

@@ -7,7 +7,7 @@
 package viper.silicon.rules
 
 import org.jgrapht.alg.util.Pair
-import viper.silicon.interfaces.{Failure, SiliconFailureContext, SiliconMappedCounterexample, SiliconNativeCounterexample, SiliconVariableCounterexample}
+import viper.silicon.interfaces.{Failure, SiliconDebuggingFailureContext, SiliconFailureContext, SiliconMappedCounterexample, SiliconNativeCounterexample, SiliconVariableCounterexample}
 import viper.silicon.state.State
 import viper.silicon.verifier.Verifier
 import viper.silver.ast
@@ -67,9 +67,13 @@ trait SymbolicExecutionRules {
         })
     } else Seq()
 
-    val assumptions = v.decider.pcs.assumptionExps
+    if(Verifier.config.enableDebugging()){
+      val assumptions = v.decider.pcs.assumptionExps
+      res.failureContexts = Seq(SiliconDebuggingFailureContext(branchconditions, counterexample, reasonUnknown, Some(s), Some(v), v.decider.prover.getAllEmits(), v.decider.macroDecls, v.decider.functionDecls, assumptions, failedAssertExp))
+    }else{
+      res.failureContexts = Seq(SiliconFailureContext(branchconditions, counterexample, reasonUnknown))
+    }
 
-    res.failureContexts = Seq(SiliconFailureContext(branchconditions, counterexample, reasonUnknown, Some(s), Some(v), v.decider.prover.getAllEmits(), v.decider.macroDecls, v.decider.functionDecls, assumptions, failedAssertExp))
     Failure(res, v.reportFurtherErrors())
 
   }

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -296,9 +296,10 @@ class DefaultMainVerifier(config: Config,
      ++ predicateVerificationResults
      ++ methodVerificationResults)
 
-    // TODO ake: if debugging enabled
-//    val debugger = new SiliconDebugger(verificationResults, identifierFactory, reporter, FrontendStateCache.resolver, FrontendStateCache.pprogram, FrontendStateCache.translator, this)
-//    debugger.startDebugger()
+    if(Verifier.config.enableDebugging()){
+      val debugger = new SiliconDebugger(verificationResults, identifierFactory, reporter, FrontendStateCache.resolver, FrontendStateCache.pprogram, FrontendStateCache.translator, this)
+      debugger.startDebugger()
+    }
 
     verificationResults
   }

src/test/resources/viperDebugger/gaussianSumRef.vpr

@@ -13,6 +13,7 @@ method gaussian_sum_ref(n : Ref)
         invariant acc(n.val)
         invariant r == i * (i-1) / 2
         invariant i <= n.val
+        invariant 0 <= n.val
     {
         r := r + i
         i := i + 1

src/test/scala/SiliconTests.scala

@@ -15,13 +15,10 @@ import viper.silver.verifier.Verifier
 
 class SiliconTests extends SilSuite {
   private val siliconTestDirectories =
-    Seq("consistency", "issue387")
+    Seq()
 
   private val silTestDirectories =
-    Seq("all",
-        "quantifiedpermissions", "quantifiedpredicates", "quantifiedcombinations",
-        "wands", "termination", "refute",
-        "examples")
+    Seq("andrea")
 
   val testDirectories: Seq[String] = siliconTestDirectories ++ silTestDirectories