diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index 068bcc03e..2e292a023 100644 --- a/src/main/scala/Config.scala +++ b/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) { diff --git a/src/main/scala/debugger/SiliconDebugger.scala b/src/main/scala/debugger/SiliconDebugger.scala index 41f629259..bb173ee2d 100644 --- a/src/main/scala/debugger/SiliconDebugger.scala +++ b/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.") diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 94df7875d..5b669f097 100644 --- a/src/main/scala/decider/Decider.scala +++ b/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) } diff --git a/src/main/scala/interfaces/Verification.scala b/src/main/scala/interfaces/Verification.scala index 4f0b434d5..95f36b8e1 100644 --- a/src/main/scala/interfaces/Verification.scala +++ b/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 diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 89b9f9141..ba7b35c60 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/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) }) }) diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index af1e69b3e..ab4dac3cf 100644 --- a/src/main/scala/rules/Executor.scala +++ b/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) }) }) diff --git a/src/main/scala/rules/SymbolicExecutionRules.scala b/src/main/scala/rules/SymbolicExecutionRules.scala index ad77133a8..87ce3bff9 100644 --- a/src/main/scala/rules/SymbolicExecutionRules.scala +++ b/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()) } diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 3f5347ee2..936621a19 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/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 } diff --git a/src/test/resources/viperDebugger/gaussianSumRef.vpr b/src/test/resources/viperDebugger/gaussianSumRef.vpr index 92fb84354..5aabe5ccc 100644 --- a/src/test/resources/viperDebugger/gaussianSumRef.vpr +++ b/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 diff --git a/src/test/scala/SiliconTests.scala b/src/test/scala/SiliconTests.scala index 027bd3da2..237e49b7d 100644 --- a/src/test/scala/SiliconTests.scala +++ b/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