From 68aa9f8cce53a93d13d0758d833523cfe86f2ad4 Mon Sep 17 00:00:00 2001 From: Nicolas Klose Date: Tue, 10 Sep 2024 19:10:28 +0200 Subject: [PATCH] I have a plan now --- src/main/scala/biabduction/BiAbduction.scala | 7 +++---- src/main/scala/interfaces/Verification.scala | 2 +- src/main/scala/rules/ChunkSupporter.scala | 4 ++++ src/main/scala/rules/Consumer.scala | 19 +++++++------------ src/main/scala/rules/Executor.scala | 20 ++++++++++++-------- 5 files changed, 27 insertions(+), 25 deletions(-) diff --git a/src/main/scala/biabduction/BiAbduction.scala b/src/main/scala/biabduction/BiAbduction.scala index 70039b93..a008e540 100644 --- a/src/main/scala/biabduction/BiAbduction.scala +++ b/src/main/scala/biabduction/BiAbduction.scala @@ -114,7 +114,7 @@ trait BiAbductionRule[S] { // TODO nklose can we move this all into happening for consumes only? object BiAbductionSolver { - def solveAbduction(s: State, v: Verifier, goal: Seq[Exp], tra: Option[AbductionQuestionTransformer], loc: Position): BiAbductionResult = { + def solveAbduction(s: State, v: Verifier, goal: Seq[Exp], tra: Option[AbductionQuestionTransformer], loc: Position): Seq[BiAbductionResult] = { val res = executionFlowController.locally(s, v)((s1, v1) => { @@ -136,10 +136,9 @@ object BiAbductionSolver { res match { case nf: NonFatalResult => - // TODO Can we ever get multiple abduction results here? - abductionUtils.getAbductionResults(nf).head + abductionUtils.getAbductionResults(nf) case _ => - BiAbductionFailure(s, v) + Seq(BiAbductionFailure(s, v)) } } diff --git a/src/main/scala/interfaces/Verification.scala b/src/main/scala/interfaces/Verification.scala index cf95fd88..bd91e6d1 100644 --- a/src/main/scala/interfaces/Verification.scala +++ b/src/main/scala/interfaces/Verification.scala @@ -108,7 +108,7 @@ case class Failure/*[ST <: Store[ST], case class SiliconFailureContext(branchConditions: Seq[ast.Exp], counterExample: Option[Counterexample], reasonUnknown: Option[String], - abductionResult: Option[BiAbductionResult]) extends FailureContext { + abductionResult: Option[Seq[BiAbductionResult]]) extends FailureContext { lazy val branchConditionString: String = { if (branchConditions.nonEmpty) { diff --git a/src/main/scala/rules/ChunkSupporter.scala b/src/main/scala/rules/ChunkSupporter.scala index 288c9a65..0eccadb5 100644 --- a/src/main/scala/rules/ChunkSupporter.scala +++ b/src/main/scala/rules/ChunkSupporter.scala @@ -140,6 +140,10 @@ object chunkSupporter extends ChunkSupportRules { case _ if v1.decider.checkSmoke(true) => Success() // TODO: Mark branch as dead? case _ => + + // TODO nklose: we should move abduction out of createFailure to here and then just recurse with the results + // This should also replace the result handling in executor and consumer + // We can then do the abduction on the "original" state s, not the partial heap h createFailure(ve, v1, s1, "consuming chunk", true) } } diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index ad85fdc4..f6043277 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -6,16 +6,9 @@ package viper.silicon.rules -import viper.silicon.debugger.DebugExp import viper.silicon.Config.JoinMode - -import scala.collection.mutable -import viper.silver.ast -import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion -import viper.silver.verifier.PartialVerificationError -import viper.silver.verifier.reasons._ -import viper.silicon.interfaces.VerificationResult import viper.silicon.biabduction.{AbductionSuccess, BiAbductionFailure} +import viper.silicon.debugger.DebugExp import viper.silicon.interfaces.{Failure, SiliconFailureContext, Success, VerificationResult} import viper.silicon.logger.records.data.{CondExpRecord, ConsumeRecord, ImpliesRecord} import viper.silicon.state._ @@ -186,16 +179,18 @@ object consumer extends ConsumptionRules { res match { case f@Failure(ve, _) if abductionLocation.isDefined => ve.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult match { - case Some(as: AbductionSuccess) => { + case Some((as: AbductionSuccess) :: rest ) => { + // Current assumption: we always do this recursively up the stack, so we only have to do the head producer.produces(s, freshSnap, as.state, ContractNotWellformed, v) { (s1, v1) => executor.execs(s1, as.stmts.reverse, v1) { (s2, v2) => // TODO nklose this is not working. The abduced heap chunk is not being consumed - wrappedConsumeTlc(s2, s2.h, a, pve, v2, abductionLocation)(Q) && Success(Some(as.copy(loc = abductionLocation.get))) + val restSuc = rest.foldLeft[VerificationResult](Success()){ case (suc, abs: AbductionSuccess) => suc && Success(Some(abs.copy(loc = abductionLocation.get))) } + restSuc && Success(Some(as.copy(loc = abductionLocation.get))) && wrappedConsumeTlc(s2, s2.h, a, pve, v2, abductionLocation)(Q) } } } - case Some(_: BiAbductionFailure) => - println("Abduction failed") + case Some(Seq(_: BiAbductionFailure)) => + //println("Abduction failed") f } case res => res diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 0d9aa1a3..8ffc8e17 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -767,21 +767,25 @@ object executor extends ExecutionRules { | _: ast.While => sys.error(s"Unexpected statement (${stmt.getClass.getName}): $stmt") } + // TODO nklose: make everything happen in consume, nothing here. executed match { + case Failure(_: PostconditionViolated, _) => executed // Postconditions are handled elsewhere, we do not want to restart for them case Failure(ve, _) if ve.failureContexts.nonEmpty => - ve.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult match { - case Some(as: AbductionSuccess) => + val abReses = ve.failureContexts.head.asInstanceOf[SiliconFailureContext].abductionResult.get + abReses.head match { + case as: AbductionSuccess => producer.produces(s, freshSnap, as.state, ContractNotWellformed, v) { (s1, v1) => executor.execs(s1, as.stmts.reverse, v1) { (s2, v2) => - exec(s2, stmt, v2)((s3, v3) => Q(s3, v3) && Success(Some(as))) + val restSuc = abReses.tail.foldLeft[VerificationResult](Success()){ case (suc, abs: AbductionSuccess) => suc && Success(Some(abs.copy(loc = stmt.pos))) } + restSuc && Success(Some(as)) && exec(s2, stmt, v2)((s3, v3) => Q(s3, v3)) } - } + } - case Some(_: BiAbductionFailure) => - println("Abduction failed") - executed - } + case _: BiAbductionFailure => + //println("Abduction failed") + executed + } case _ => executed } }