From ce5a4f1442607ff363d105e9f354ffea1ba16c7c Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 8 Jun 2022 13:40:32 +0200 Subject: [PATCH 01/31] Improve SymbExLogger: - Thread safe as long as silicon parallelizes up to the entity level: SymbLog itself is not thread safe. --ideModeAdvanced accordingly does not require --numberOfParallelVerifiers 1 anymore. - Change SymbLog to accept a listener for appropriate events. --- src/main/scala/Config.scala | 13 -- src/main/scala/Silicon.scala | 2 +- src/main/scala/logger/LogConfig.scala | 15 +- src/main/scala/logger/SymbExLogger.scala | 214 ++++++++++-------- .../records/structural/BranchingRecord.scala | 19 +- src/main/scala/logger/renderer/Renderer.scala | 2 +- .../logger/renderer/SimpleTreeRenderer.scala | 8 +- .../logger/writer/SymbExLogReportWriter.scala | 10 +- src/main/scala/rules/Brancher.scala | 2 +- .../verifier/DefaultMasterVerifier.scala | 2 +- 10 files changed, 160 insertions(+), 127 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index cca9cedaf..49058e402 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -735,19 +735,6 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { case _ => Right(()) } - validateOpt(ideModeAdvanced, numberOfParallelVerifiers) { - case (Some(false), _) => - Right(()) - case (Some(true), Some(n)) => - if (n == 1) - Right(()) - else - Left( s"Option ${ideModeAdvanced.name} requires setting " - + s"${numberOfParallelVerifiers.name} to 1") - case other => - sys.error(s"Unexpected combination: $other") - } - validateOpt(counterexample, enableMoreCompleteExhale) { case (Some(_), Some(false)) => Left( s"Option ${counterexample.name} requires setting " + s"flag ${enableMoreCompleteExhale.name}") diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala index cb655972b..271c75000 100644 --- a/src/main/scala/Silicon.scala +++ b/src/main/scala/Silicon.scala @@ -208,7 +208,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)] // verification was interrupted, therefore close the current member's scope: SymbExLogger.currentLog().closeMemberScope() if (config.ideModeAdvanced()) { - reporter report ExecutionTraceReport(SymbExLogger.memberList, List(), List()) + reporter report ExecutionTraceReport(SymbExLogger.memberList.toIndexedSeq, List(), List()) } result = Some(SilFailure(SilTimeoutOccurred(config.timeout(), "second(s)") :: Nil)) case exception: Exception if !config.disableCatchingExceptions() => diff --git a/src/main/scala/logger/LogConfig.scala b/src/main/scala/logger/LogConfig.scala index ae3914435..dd7d635e6 100644 --- a/src/main/scala/logger/LogConfig.scala +++ b/src/main/scala/logger/LogConfig.scala @@ -7,10 +7,23 @@ package viper.silicon.logger import spray.json._ +import viper.silicon.logger.records.data.DataRecord case class LogConfig(isBlackList: Boolean, includeStore: Boolean, includeHeap: Boolean, includeOldHeap: Boolean, includePcs: Boolean, - recordConfigs: List[RecordConfig]) + recordConfigs: List[RecordConfig]) { + def getRecordConfig(d: DataRecord): Option[RecordConfig] = { + for (rc <- recordConfigs) { + if (rc.kind.equals(d.toTypeString)) { + rc.value match { + case Some(value) => if (value.equals(d.toSimpleString)) return Some(rc) + case _ => return Some(rc) + } + } + } + None + } +} object LogConfig { def default(): LogConfig = LogConfig( diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index b07526b51..a277bb625 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -7,25 +7,26 @@ package viper.silicon.logger import java.nio.file.{Files, Path, Paths} - import spray.json._ import LogConfigProtocol._ import com.typesafe.scalalogging.Logger import org.slf4j.LoggerFactory import viper.silicon.decider.PathConditionStack -import viper.silicon.logger.SymbExLogger.getRecordConfig import viper.silicon.logger.records.SymbolicRecord import viper.silicon.logger.records.data.{DataRecord, FunctionRecord, MemberRecord, MethodRecord, PredicateRecord} import viper.silicon.logger.records.scoping.{CloseScopeRecord, OpenScopeRecord, ScopingRecord} -import viper.silicon.logger.records.structural.BranchingRecord +import viper.silicon.logger.records.structural.{BranchingRecord, StructuralRecord} import viper.silicon.logger.renderer.SimpleTreeRenderer import viper.silicon.state._ import viper.silicon.state.terms._ import viper.silicon.{Config, Map} import viper.silver.ast +import viper.silver.ast.Exp +import java.util.concurrent.atomic.AtomicInteger import scala.annotation.elidable import scala.annotation.elidable._ +import scala.collection.mutable.ArrayBuffer import scala.util.{Failure, Success, Try} /* TODO: InsertionOrderedSet is used by the logger, but the insertion order is @@ -37,8 +38,7 @@ import scala.util.{Failure, Success, Try} * ================================ * SymbExLogger Usage * ================================ - * The SymbExLogger has to be enabled by passing `--ideModeAdvanced` to Silicon (which in turn - * requires numberOfParallelVerifiers to be 1). + * The SymbExLogger has to be enabled by passing `--ideModeAdvanced` to Silicon. * Unless otherwise specified, the default logConfig will be used (viper.silicon.logger.LogConfig.default()): * All logged records will be included in the report, but store, heap, and path conditions will be omitted. * @@ -194,29 +194,16 @@ import scala.util.{Failure, Success, Try} object SymbExLogger { /** Collection of logged Method/Predicates/Functions. **/ - var memberList: Seq[SymbLog] = Seq[SymbLog]() - private var uidCounter = 0 + val memberList: ArrayBuffer[SymbLog] = ArrayBuffer() + var _currentLog: ThreadLocal[Option[SymbLog]] = ThreadLocal.withInitial(() => None) + + private val uidCounter = new AtomicInteger(0) var enabled = false var logConfig: LogConfig = LogConfig.default() + var listenerProvider: LogConfig => SymbLogListener = new InMemorySymbLog(_) - def freshUid(): Int = { - val uid = uidCounter - uidCounter = uidCounter + 1 - uid - } - - def getRecordConfig(d: DataRecord): Option[RecordConfig] = { - for (rc <- logConfig.recordConfigs) { - if (rc.kind.equals(d.toTypeString)) { - rc.value match { - case Some(value) => if (value.equals(d.toSimpleString)) return Some(rc) - case _ => return Some(rc) - } - } - } - None - } + def freshUid(): Int = uidCounter.getAndIncrement() /** * stores the last SMT solver statistics to calculate the diff @@ -233,7 +220,9 @@ object SymbExLogger { */ @elidable(INFO) def openMemberScope(member: ast.Member, s: State, pcs: PathConditionStack): Unit = { - memberList = memberList ++ Seq(new SymbLog(member, s, pcs)) + val log = new SymbLog(listenerProvider(logConfig), member, s, pcs) + memberList.synchronized { memberList += log } + _currentLog.set(Some(log)) } /** Use this method to access the current log, e.g., to access the log of the method @@ -243,7 +232,7 @@ object SymbExLogger { */ def currentLog(): SymbLog = { if (enabled) - memberList.last + _currentLog.get.get else NoopSymbLog } @@ -251,6 +240,7 @@ object SymbExLogger { def closeMemberScope(): Unit = { if (enabled) { currentLog().closeMemberScope() + _currentLog.set(None) } } @@ -264,6 +254,9 @@ object SymbExLogger { logConfig = parseLogConfig(c) } + def setListenerProvider(listener: LogConfig => SymbLogListener): Unit = + listenerProvider = listener + @elidable(INFO) private def setEnabled(b: Boolean): Unit = { enabled = b @@ -288,7 +281,7 @@ object SymbExLogger { def toSimpleTreeString: String = { if (enabled) { val simpleTreeRenderer = new SimpleTreeRenderer() - simpleTreeRenderer.render(memberList) + simpleTreeRenderer.render(memberList.map(_.listener).collect { case l: InMemorySymbLog => l }) } else "" } @@ -300,15 +293,16 @@ object SymbExLogger { * Only needed when several files are verified together (e.g., sbt test). */ def reset(): Unit = { - memberList = Seq[SymbLog]() - uidCounter = 0 + memberList.clear() + uidCounter.set(0) filePath = null logConfig = LogConfig.default() + listenerProvider = new InMemorySymbLog(_) prevSmtStatistics = new Map() } def resetMemberList(): Unit = { - memberList = Seq[SymbLog]() + memberList.clear() // or reset by calling it from Decider.reset prevSmtStatistics = new Map() } @@ -350,25 +344,97 @@ object SymbExLogger { //========================= SymbLog ======================== -/** - * Concept: One object of SymbLog per Method/Predicate/Function. SymbLog - * is used in the SymbExLogger-object. - */ -class SymbLog(v: ast.Member, s: State, pcs: PathConditionStack) { +trait SymbLogListener { + def appendDataRecord(symbLog: SymbLog, r: DataRecord): Unit + def appendScopingRecord(symbLog: SymbLog, r: ScopingRecord, ignoreBranchingStack: Boolean = false): Unit + def appendBranchingRecord(symbLog: SymbLog, r: BranchingRecord): Unit - val logger: Logger = - Logger(LoggerFactory.getLogger(s"${this.getClass.getName}")) + def switchToNextBranch(symbLog: SymbLog, uidBranchPoint: Int): Unit + def markBranchReachable(symbLog: SymbLog, uidBranchPoint: Int): Unit + def endBranchPoint(symbLog: SymbLog, uidBranchPoint: Int): Unit +} +class InMemorySymbLog(config: LogConfig) extends SymbLogListener { /** top level log entries for this member; these log entries were recorded consecutively without branching; - * in case branching occured, one of these records is a BranchingRecord with all branches as field attached to it */ + * in case branching occured, one of these records is a BranchingRecord with all branches as field attached to it */ var log: Vector[SymbolicRecord] = Vector[SymbolicRecord]() + /** this stack keeps track of BranchingRecords while adding records to the log; as soon as all branches of a - * BranchingRecord are done, logging has to switch back to the previous BranchingRecord */ + * BranchingRecord are done, logging has to switch back to the previous BranchingRecord */ var branchingStack: List[BranchingRecord] = List[BranchingRecord]() + /** if a record was ignored due to the logConfig, its ID is tracked here and corresponding open and close scope - * records will be ignored too */ + * records will be ignored too */ var ignoredDataRecords: Set[Int] = Set() + def appendRecord(r: SymbolicRecord, ignoreBranchingStack: Boolean = false): Unit = { + if (branchingStack.isEmpty || ignoreBranchingStack) { + log = log :+ r + } else { + branchingStack.head.appendLog(r) + } + } + + override def appendDataRecord(symbLog: SymbLog, r: DataRecord): Unit = { + val shouldIgnore = config.getRecordConfig(r) match { + case Some(_) => config.isBlackList + case None => !config.isBlackList + } + + if(shouldIgnore) { + ignoredDataRecords = ignoredDataRecords + r.id + } else { + appendRecord(r) + } + } + + override def appendScopingRecord(symbLog: SymbLog, r: ScopingRecord, ignoreBranchingStack: Boolean): Unit = { + if(!ignoredDataRecords.contains(r.refId)) { + if(ignoreBranchingStack) { + log = log :+ r + } else { + appendRecord(r) + } + } + } + + override def appendBranchingRecord(symbLog: SymbLog, r: BranchingRecord): Unit = { + appendRecord(r) + branchingStack +:= r + } + + override def switchToNextBranch(symbLog: SymbLog, uidBranchPoint: Int): Unit = { + assert(branchingStack.nonEmpty) + val branchingRecord = branchingStack.head + assert(branchingRecord.id == uidBranchPoint) + // no close scope is inserted because branches are not considered scopes + branchingRecord.switchToNextBranch() + } + + override def markBranchReachable(symbLog: SymbLog, uidBranchPoint: Int): Unit = { + assert(branchingStack.nonEmpty) + val branchingRecord = branchingStack.head + assert(branchingRecord.id == uidBranchPoint) + branchingRecord.markReachable() + } + + override def endBranchPoint(symbLog: SymbLog, uidBranchPoint: Int): Unit = { + assert(branchingStack.nonEmpty) + val branchingRecord = branchingStack.head + assert(branchingRecord.id == uidBranchPoint) + // no close scope is inserted because branches are not considered scopes + branchingStack = branchingStack.tail + } +} + +/** + * Concept: One object of SymbLog per Method/Predicate/Function. SymbLog + * is used in the SymbExLogger-object. + */ +class SymbLog(val listener: SymbLogListener, val v: ast.Member, val s: State, val pcs: PathConditionStack) { + val logger: Logger = + Logger(LoggerFactory.getLogger(s"${this.getClass.getName}")) + /** * indicates whether this member's close was already closed */ @@ -383,19 +449,8 @@ class SymbLog(v: ast.Member, s: State, pcs: PathConditionStack) { case f: ast.Function => new FunctionRecord(f, s, pcs) case _ => null } - openScope(main) - private def appendLog(r: SymbolicRecord, ignoreBranchingStack: Boolean = false): Unit = { - if (isClosed) { - logger warn "ignoring record insertion to an already closed SymbLog instance" - return - } - if (branchingStack.isEmpty || ignoreBranchingStack) { - log = log :+ r - } else { - branchingStack.head.appendLog(r) - } - } + openScope(main) /** * Inserts the record as well as a corresponding open scope record into the log @@ -405,19 +460,8 @@ class SymbLog(v: ast.Member, s: State, pcs: PathConditionStack) { @elidable(INFO) def openScope(s: DataRecord): Int = { s.id = SymbExLogger.freshUid() - // check whether this record should be ignored: - val recordConfig = getRecordConfig(s) - val ignore = recordConfig match { - case Some(_) => SymbExLogger.logConfig.isBlackList - case _ => !SymbExLogger.logConfig.isBlackList - } - if (ignore) { - ignoredDataRecords = ignoredDataRecords + s.id - } else { - appendLog(s) - val openRecord = new OpenScopeRecord(s) - insert(openRecord) - } + listener.appendDataRecord(this, s) + insert(new OpenScopeRecord(s)) s.id } @@ -430,11 +474,8 @@ class SymbLog(v: ast.Member, s: State, pcs: PathConditionStack) { @elidable(INFO) private def insert(s: ScopingRecord, ignoreBranchingStack: Boolean = false): Int = { s.id = SymbExLogger.freshUid() - if (!ignoredDataRecords.contains(s.refId)) { - // the corresponding data record is not ignored - s.timeMs = System.currentTimeMillis() - appendLog(s, ignoreBranchingStack) - } + s.timeMs = System.currentTimeMillis() + listener.appendScopingRecord(this, s, ignoreBranchingStack) s.id } @@ -447,11 +488,10 @@ class SymbLog(v: ast.Member, s: State, pcs: PathConditionStack) { * @return id of the branching record */ @elidable(INFO) - def insertBranchPoint(possibleBranchesCount: Int, condition: Option[Term] = None): Int = { - val branchingRecord = new BranchingRecord(possibleBranchesCount, condition) + def insertBranchPoint(possibleBranchesCount: Int, condition: Option[Term] = None, conditionExp: Option[Exp] = None): Int = { + val branchingRecord = new BranchingRecord(possibleBranchesCount, condition, conditionExp) branchingRecord.id = SymbExLogger.freshUid() - appendLog(branchingRecord) - branchingStack = branchingRecord :: branchingStack + listener.appendBranchingRecord(this, branchingRecord) branchingRecord.id } @@ -461,11 +501,7 @@ class SymbLog(v: ast.Member, s: State, pcs: PathConditionStack) { */ @elidable(INFO) def switchToNextBranch(uidBranchPoint: Int): Unit = { - assert(branchingStack.nonEmpty) - val branchingRecord = branchingStack.head - assert(branchingRecord.id == uidBranchPoint) - // no close scope is inserted because branches are not considered scopes - branchingRecord.switchToNextBranch() + listener.switchToNextBranch(this, uidBranchPoint) } /** @@ -474,10 +510,7 @@ class SymbLog(v: ast.Member, s: State, pcs: PathConditionStack) { */ @elidable(INFO) def markReachable(uidBranchPoint: Int): Unit = { - assert(branchingStack.nonEmpty) - val branchingRecord = branchingStack.head - assert(branchingRecord.id == uidBranchPoint) - branchingRecord.markReachable() + listener.markBranchReachable(this, uidBranchPoint) } /** @@ -496,11 +529,7 @@ class SymbLog(v: ast.Member, s: State, pcs: PathConditionStack) { */ @elidable(INFO) def endBranchPoint(uidBranchPoint: Int): Unit = { - assert(branchingStack.nonEmpty) - val branchingRecord = branchingStack.head - assert(branchingRecord.id == uidBranchPoint) - // no close scope is inserted because branches are not considered scopes - branchingStack = branchingStack.tail + listener.endBranchPoint(this, uidBranchPoint) } /** @@ -552,12 +581,15 @@ class SymbLog(v: ast.Member, s: State, pcs: PathConditionStack) { _macros = _macros + (m -> body) } - override def toString: String = new SimpleTreeRenderer().renderMember(this) + override def toString: String = listener match { + case log: InMemorySymbLog => new SimpleTreeRenderer().renderMember(log) + case _ => super.toString + } } -object NoopSymbLog extends SymbLog(null, null, null) { +object NoopSymbLog extends SymbLog(null, null, null, null) { override def openScope(s: DataRecord): Int = 0 - override def insertBranchPoint(possibleBranchesCount: Int, condition: Option[Term]): Int = 0 + override def insertBranchPoint(possibleBranchesCount: Int, condition: Option[Term], conditionExp: Option[Exp]): Int = 0 override def switchToNextBranch(uidBranchPoint: Int): Unit = {} override def markReachable(uidBranchPoint: Int): Unit = {} override def closeScope(n: Int): Unit = {} diff --git a/src/main/scala/logger/records/structural/BranchingRecord.scala b/src/main/scala/logger/records/structural/BranchingRecord.scala index ea99e8227..52876137c 100644 --- a/src/main/scala/logger/records/structural/BranchingRecord.scala +++ b/src/main/scala/logger/records/structural/BranchingRecord.scala @@ -8,22 +8,23 @@ package viper.silicon.logger.records.structural import viper.silicon.logger.records.SymbolicRecord import viper.silicon.state.terms.Term +import viper.silver.ast.Exp -class BranchingRecord(possibleBranchesCount: Int, val condition: Option[Term]) extends StructuralRecord { +class BranchingRecord(possibleBranchesCount: Int, val condition: Option[Term], val conditionExp: Option[Exp]) extends StructuralRecord { private var currentBranchIndex = 0 private val branches: Vector[BranchInfo] = Vector.tabulate(possibleBranchesCount)(_ => new BranchInfo()) - def appendLog(r: SymbolicRecord): Unit = { - assert(currentBranchIndex < branches.length) - val branch = branches(currentBranchIndex) - branch.records = branch.records :+ r + def getCurrentBranch: BranchInfo = { + assert(0 <= currentBranchIndex && currentBranchIndex < branches.length) + branches(currentBranchIndex) } + def appendLog(r: SymbolicRecord): Unit = + getCurrentBranch.records :+= r + def markReachable(): Unit = { - assert(currentBranchIndex < branches.length) - val branch = branches(currentBranchIndex) - branch.isReachable = true - branch.startTimeMs = System.currentTimeMillis() + getCurrentBranch.isReachable = true + getCurrentBranch.startTimeMs = System.currentTimeMillis() } def switchToNextBranch(): Unit = { diff --git a/src/main/scala/logger/renderer/Renderer.scala b/src/main/scala/logger/renderer/Renderer.scala index 29b621749..d76c424ef 100644 --- a/src/main/scala/logger/renderer/Renderer.scala +++ b/src/main/scala/logger/renderer/Renderer.scala @@ -9,5 +9,5 @@ package viper.silicon.logger.renderer trait Renderer[S, T] { def renderMember(s: S): T - def render(memberList: Seq[S]): T + def render(memberList: Iterable[S]): T } diff --git a/src/main/scala/logger/renderer/SimpleTreeRenderer.scala b/src/main/scala/logger/renderer/SimpleTreeRenderer.scala index cfd4589dc..ffa96f802 100644 --- a/src/main/scala/logger/renderer/SimpleTreeRenderer.scala +++ b/src/main/scala/logger/renderer/SimpleTreeRenderer.scala @@ -7,15 +7,15 @@ package viper.silicon.logger.renderer import scala.annotation.unused -import viper.silicon.logger.SymbLog +import viper.silicon.logger.InMemorySymbLog import viper.silicon.logger.records.SymbolicRecord import viper.silicon.logger.records.data.DataRecord import viper.silicon.logger.records.scoping.{CloseScopeRecord, OpenScopeRecord} import viper.silicon.logger.records.structural.{BranchingRecord, JoiningRecord} import viper.silicon.state.terms.Not -class SimpleTreeRenderer extends Renderer[SymbLog, String] { - def render(memberList: Seq[SymbLog]): String = { +class SimpleTreeRenderer extends Renderer[InMemorySymbLog, String] { + def render(memberList: Iterable[InMemorySymbLog]): String = { var res = "" for (m <- memberList) { res = res + renderMember(m) + "\n" @@ -23,7 +23,7 @@ class SimpleTreeRenderer extends Renderer[SymbLog, String] { res } - def renderMember(member: SymbLog): String = { + def renderMember(member: InMemorySymbLog): String = { // val filteredLog = filterEmptyScopes(member.log) toSimpleTree(member.log, 0, 0) } diff --git a/src/main/scala/logger/writer/SymbExLogReportWriter.scala b/src/main/scala/logger/writer/SymbExLogReportWriter.scala index 96d24be47..40ba9cefa 100644 --- a/src/main/scala/logger/writer/SymbExLogReportWriter.scala +++ b/src/main/scala/logger/writer/SymbExLogReportWriter.scala @@ -10,7 +10,7 @@ import spray.json.{JsArray, JsBoolean, JsNull, JsNumber, JsObject, JsString, JsT import viper.silicon.Map import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.interfaces.state.Chunk -import viper.silicon.logger.SymbLog +import viper.silicon.logger.InMemorySymbLog import viper.silicon.logger.records.scoping.{CloseScopeRecord, OpenScopeRecord} import viper.silicon.logger.records.structural.{BranchInfo, BranchingRecord, JoiningRecord} import viper.silicon.logger.records.{RecordData, SymbolicRecord} @@ -107,19 +107,19 @@ object SymbExLogReportWriter { * @param members A symbolic log per member to translate. * @return array of all records. */ - def toJSON(members: Seq[SymbLog]): JsArray = { + def toJSON(members: Seq[InMemorySymbLog]): JsArray = { val records = members.foldLeft(Vector[JsValue]()) { - (prevVal: Vector[JsValue], member: SymbLog) => prevVal ++ toJSON(member) + (prevVal: Vector[JsValue], member: InMemorySymbLog) => prevVal ++ toJSON(member) } JsArray(records) } - /** Translates a SymbLog to a vector of JsValues. + /** Translates a InMemorySymbLog to a vector of JsValues. * * @param symbLog The symbolic log to translate. * @return array of all records. */ - def toJSON(symbLog: SymbLog): Vector[JsValue] = { + def toJSON(symbLog: InMemorySymbLog): Vector[JsValue] = { val allRecords = getAllRecords(symbLog.log) allRecords.map(toJSON).toVector } diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index c184a6e0a..78a1273a5 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -75,7 +75,7 @@ object brancher extends BranchingRules { v.decider.prover.comment(thenBranchComment) v.decider.prover.comment(elseBranchComment) - val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(2, Some(condition)) + val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(2, Some(condition), conditionExp) val elseBranchVerificationTask: Verifier => VerificationResult = if (executeElseBranch) { diff --git a/src/main/scala/verifier/DefaultMasterVerifier.scala b/src/main/scala/verifier/DefaultMasterVerifier.scala index b0c97f19d..b89cecffd 100644 --- a/src/main/scala/verifier/DefaultMasterVerifier.scala +++ b/src/main/scala/verifier/DefaultMasterVerifier.scala @@ -252,7 +252,7 @@ class DefaultMasterVerifier(config: Config, override val reporter: Reporter) if (config.ideModeAdvanced()) { reporter report ExecutionTraceReport( - SymbExLogger.memberList, + SymbExLogger.memberList.toIndexedSeq, this.axiomsAfterAnalysis().toList, this.postConditionAxioms().toList) } From 88c2a546121902f48e2ca722f19042d1fe4202c3 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 8 Jun 2022 14:46:11 +0200 Subject: [PATCH 02/31] move smt delta calculation to ProverStdIO for thread safety --- src/main/scala/decider/Decider.scala | 4 +- src/main/scala/decider/ProverStdIO.scala | 42 ++++++++++++++++++- src/main/scala/logger/SymbExLogger.scala | 52 +++--------------------- 3 files changed, 47 insertions(+), 51 deletions(-) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index cdc187d96..3084e16fb 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -263,9 +263,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => val result = prover.assert(t, timeout) if (SymbExLogger.enabled) { - val statistics = prover.statistics() - val deltaStatistics = SymbExLogger.getDeltaSmtStatistics(statistics) - assertRecord.statistics = Some(statistics ++ deltaStatistics) + assertRecord.statistics = Some(prover.deltaStatistics()) } SymbExLogger.currentLog().closeScope(sepIdentifier) diff --git a/src/main/scala/decider/ProverStdIO.scala b/src/main/scala/decider/ProverStdIO.scala index 4d010f678..165fced30 100644 --- a/src/main/scala/decider/ProverStdIO.scala +++ b/src/main/scala/decider/ProverStdIO.scala @@ -40,6 +40,7 @@ abstract class ProverStdIO(uniqueId: String, var proverPath: Path = _ var lastModel : String = _ + var lastStatistics: Map[String, String] = Map.empty def name: String def minVersion: Version @@ -319,7 +320,7 @@ abstract class ProverStdIO(uniqueId: String, } } - def statistics(): Map[String, String] = { + private def queryStatistics(): Map[String, String] = { var repeat = true var line = "" var stats = scala.collection.immutable.SortedMap[String, String]() @@ -347,6 +348,45 @@ abstract class ProverStdIO(uniqueId: String, toMap(stats) } + def statistics(): Map[String, String] = { + lastStatistics = queryStatistics() + lastStatistics + } + + /** + * Queries the statistics, and calculates the diff between it and the last statistics query. + * The difference is calculated if value can be converted to an int or double + * @return map with the current statistics, and the differences (only containing values that could be converted) + * and keys with appended "-delta" + */ + def deltaStatistics(): Map[String, String] = { + val currentStatistics = queryStatistics() + val deltaStatistics = currentStatistics map getDelta filter { case (_, value) => value.nonEmpty } map { + case (key, Some(value)) => (key + "-delta", value) + case other => sys.error(s"Unexpected result pair $other") + } + lastStatistics = lastStatistics ++ currentStatistics + currentStatistics ++ deltaStatistics + } + + private def getDelta(pair: (String, String)): (String, Option[String]) = { + val curValInt = pair._2.toIntOption + val prevValInt = lastStatistics.get(pair._1) match { + case Some(value) => value.toIntOption + case _ => Some(0) // value not found + } + val curValDouble = pair._2.toDoubleOption + val prevValDouble = lastStatistics.get(pair._1) match { + case Some(value) => value.toDoubleOption + case _ => Some(0.0) // value not found + } + (curValInt, prevValInt, curValDouble, prevValDouble) match { + case (Some(curInt), Some(prevInt), _, _) => (pair._1, Some((curInt - prevInt).toString)) + case (_, _, Some(curDouble), Some(prevDouble)) => (pair._1, Some((curDouble - prevDouble).toString)) + case _ => (pair._1, None) + } + } + def comment(str: String): Unit = { val sanitisedStr = str.replaceAll("\r", "") diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index a277bb625..57d96cb3a 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -6,16 +6,15 @@ package viper.silicon.logger -import java.nio.file.{Files, Path, Paths} -import spray.json._ -import LogConfigProtocol._ import com.typesafe.scalalogging.Logger import org.slf4j.LoggerFactory +import spray.json._ import viper.silicon.decider.PathConditionStack +import viper.silicon.logger.LogConfigProtocol._ import viper.silicon.logger.records.SymbolicRecord -import viper.silicon.logger.records.data.{DataRecord, FunctionRecord, MemberRecord, MethodRecord, PredicateRecord} +import viper.silicon.logger.records.data._ import viper.silicon.logger.records.scoping.{CloseScopeRecord, OpenScopeRecord, ScopingRecord} -import viper.silicon.logger.records.structural.{BranchingRecord, StructuralRecord} +import viper.silicon.logger.records.structural.BranchingRecord import viper.silicon.logger.renderer.SimpleTreeRenderer import viper.silicon.state._ import viper.silicon.state.terms._ @@ -23,6 +22,7 @@ import viper.silicon.{Config, Map} import viper.silver.ast import viper.silver.ast.Exp +import java.nio.file.{Files, Path, Paths} import java.util.concurrent.atomic.AtomicInteger import scala.annotation.elidable import scala.annotation.elidable._ @@ -205,11 +205,6 @@ object SymbExLogger { def freshUid(): Int = uidCounter.getAndIncrement() - /** - * stores the last SMT solver statistics to calculate the diff - */ - private var prevSmtStatistics: Map[String, String] = new Map() - /** Add a new log for a method, function or predicate (member). * * @param member Either a MethodRecord, PredicateRecord or a FunctionRecord. @@ -298,47 +293,10 @@ object SymbExLogger { filePath = null logConfig = LogConfig.default() listenerProvider = new InMemorySymbLog(_) - prevSmtStatistics = new Map() } def resetMemberList(): Unit = { memberList.clear() - // or reset by calling it from Decider.reset - prevSmtStatistics = new Map() - } - - /** - * Calculates diff between `currentStatistics` and the statistics from a previous call. - * The difference is calculated if value can be converted to an int or double - * @param currentStatistics most recent statistics from the SMT solver - * @return map with differences (only containing values that could be converted) and keys with appended "-delta" - */ - def getDeltaSmtStatistics(currentStatistics: Map[String, String]) : Map[String, String] = { - val deltaStatistics = currentStatistics map getDelta filter { case (_, value) => value.nonEmpty } map { - case (key, Some(value)) => (key + "-delta", value) - case other => sys.error(s"Unexpected result pair $other") - } - // set prevStatistics (i.e. override values with same key or add): - prevSmtStatistics = prevSmtStatistics ++ currentStatistics - deltaStatistics - } - - private def getDelta(pair: (String, String)): (String, Option[String]) = { - val curValInt = pair._2.toIntOption - val prevValInt = prevSmtStatistics.get(pair._1) match { - case Some(value) => value.toIntOption - case _ => Some(0) // value not found - } - val curValDouble = pair._2.toDoubleOption - val prevValDouble = prevSmtStatistics.get(pair._1) match { - case Some(value) => value.toDoubleOption - case _ => Some(0.0) // value not found - } - (curValInt, prevValInt, curValDouble, prevValDouble) match { - case (Some(curInt), Some(prevInt), _, _) => (pair._1, Some((curInt - prevInt).toString)) - case (_, _, Some(curDouble), Some(prevDouble)) => (pair._1, Some((curDouble - prevDouble).toString)) - case _ => (pair._1, None) - } } } From 8fab02f6d9c952edf9934b55f7d44aa905ea717a Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 29 Jun 2022 12:48:34 +0200 Subject: [PATCH 03/31] move smt statistics calculations out of ProverStdIO --- src/main/scala/decider/Decider.scala | 2 +- src/main/scala/decider/ProverStdIO.scala | 42 +----------------------- src/main/scala/logger/SymbExLogger.scala | 38 +++++++++++++++++++++ 3 files changed, 40 insertions(+), 42 deletions(-) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 3084e16fb..3c587f380 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -263,7 +263,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => val result = prover.assert(t, timeout) if (SymbExLogger.enabled) { - assertRecord.statistics = Some(prover.deltaStatistics()) + assertRecord.statistics = Some(SymbExLogger.currentLog().deltaStatistics(prover.statistics())) } SymbExLogger.currentLog().closeScope(sepIdentifier) diff --git a/src/main/scala/decider/ProverStdIO.scala b/src/main/scala/decider/ProverStdIO.scala index 165fced30..4d010f678 100644 --- a/src/main/scala/decider/ProverStdIO.scala +++ b/src/main/scala/decider/ProverStdIO.scala @@ -40,7 +40,6 @@ abstract class ProverStdIO(uniqueId: String, var proverPath: Path = _ var lastModel : String = _ - var lastStatistics: Map[String, String] = Map.empty def name: String def minVersion: Version @@ -320,7 +319,7 @@ abstract class ProverStdIO(uniqueId: String, } } - private def queryStatistics(): Map[String, String] = { + def statistics(): Map[String, String] = { var repeat = true var line = "" var stats = scala.collection.immutable.SortedMap[String, String]() @@ -348,45 +347,6 @@ abstract class ProverStdIO(uniqueId: String, toMap(stats) } - def statistics(): Map[String, String] = { - lastStatistics = queryStatistics() - lastStatistics - } - - /** - * Queries the statistics, and calculates the diff between it and the last statistics query. - * The difference is calculated if value can be converted to an int or double - * @return map with the current statistics, and the differences (only containing values that could be converted) - * and keys with appended "-delta" - */ - def deltaStatistics(): Map[String, String] = { - val currentStatistics = queryStatistics() - val deltaStatistics = currentStatistics map getDelta filter { case (_, value) => value.nonEmpty } map { - case (key, Some(value)) => (key + "-delta", value) - case other => sys.error(s"Unexpected result pair $other") - } - lastStatistics = lastStatistics ++ currentStatistics - currentStatistics ++ deltaStatistics - } - - private def getDelta(pair: (String, String)): (String, Option[String]) = { - val curValInt = pair._2.toIntOption - val prevValInt = lastStatistics.get(pair._1) match { - case Some(value) => value.toIntOption - case _ => Some(0) // value not found - } - val curValDouble = pair._2.toDoubleOption - val prevValDouble = lastStatistics.get(pair._1) match { - case Some(value) => value.toDoubleOption - case _ => Some(0.0) // value not found - } - (curValInt, prevValInt, curValDouble, prevValDouble) match { - case (Some(curInt), Some(prevInt), _, _) => (pair._1, Some((curInt - prevInt).toString)) - case (_, _, Some(curDouble), Some(prevDouble)) => (pair._1, Some((curDouble - prevDouble).toString)) - case _ => (pair._1, None) - } - } - def comment(str: String): Unit = { val sanitisedStr = str.replaceAll("\r", "") diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index 57d96cb3a..d9b8ea44b 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -398,6 +398,11 @@ class SymbLog(val listener: SymbLogListener, val v: ast.Member, val s: State, va */ private var isClosed: Boolean = false + /** + * Most recent output of (get-info :all-statistics) from the underlying prover + */ + private var lastStatistics: Map[String, String] = Map.empty + // Maps macros to their body private var _macros = Map[App, Term]() @@ -532,6 +537,39 @@ class SymbLog(val listener: SymbLogListener, val v: ast.Member, val s: State, va } } + /** + * Calculates the diff between the current and last statistics query. + * The difference is calculated if value can be converted to an int or double + * @return map with the current statistics, and the differences (only containing values that could be converted) + * and keys with appended "-delta" + */ + def deltaStatistics(currentStatistics: Map[String, String]): Map[String, String] = { + val deltaStatistics = currentStatistics map getDelta filter { case (_, value) => value.nonEmpty } map { + case (key, Some(value)) => (key + "-delta", value) + case other => sys.error(s"Unexpected result pair $other") + } + lastStatistics = lastStatistics ++ currentStatistics + currentStatistics ++ deltaStatistics + } + + private def getDelta(pair: (String, String)): (String, Option[String]) = { + val curValInt = pair._2.toIntOption + val prevValInt = lastStatistics.get(pair._1) match { + case Some(value) => value.toIntOption + case _ => Some(0) // value not found + } + val curValDouble = pair._2.toDoubleOption + val prevValDouble = lastStatistics.get(pair._1) match { + case Some(value) => value.toDoubleOption + case _ => Some(0.0) // value not found + } + (curValInt, prevValInt, curValDouble, prevValDouble) match { + case (Some(curInt), Some(prevInt), _, _) => (pair._1, Some((curInt - prevInt).toString)) + case (_, _, Some(curDouble), Some(prevDouble)) => (pair._1, Some((curDouble - prevDouble).toString)) + case _ => (pair._1, None) + } + } + def macros(): Map[App, Term] = _macros @elidable(INFO) From 91372f4b8fea3054017f7b8f86c5ca7ab2e747c2 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Fri, 23 Sep 2022 16:32:33 +0200 Subject: [PATCH 04/31] Bump silver submodule to master branch version --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 30396357d..2d50707d8 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 30396357d472af235c42875ef6cde52589dc9dcc +Subproject commit 2d50707d8a7d5be039ffa933085f3883d3f15904 From 7876aea6ee447f2fe9ca37a7e5a10b8bd1f01a23 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Thu, 17 Nov 2022 11:14:01 +0100 Subject: [PATCH 05/31] move symbexlogger state into classes, shim the old usage --- src/main/scala/logger/SymbExLogger.scala | 392 ++++++++---------- .../logger/renderer/SimpleTreeRenderer.scala | 11 +- .../logger/writer/SymbExLogReportWriter.scala | 8 +- .../scala/verifier/DefaultMainVerifier.scala | 4 +- 4 files changed, 183 insertions(+), 232 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index d9b8ea44b..eaa2cbe73 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -6,8 +6,6 @@ package viper.silicon.logger -import com.typesafe.scalalogging.Logger -import org.slf4j.LoggerFactory import spray.json._ import viper.silicon.decider.PathConditionStack import viper.silicon.logger.LogConfigProtocol._ @@ -20,20 +18,15 @@ import viper.silicon.state._ import viper.silicon.state.terms._ import viper.silicon.{Config, Map} import viper.silver.ast -import viper.silver.ast.Exp +import viper.silver.ast.{Exp, Member} -import java.nio.file.{Files, Path, Paths} +import java.nio.file.{Files, Paths} import java.util.concurrent.atomic.AtomicInteger import scala.annotation.elidable import scala.annotation.elidable._ -import scala.collection.mutable.ArrayBuffer +import scala.collection.immutable import scala.util.{Failure, Success, Try} -/* TODO: InsertionOrderedSet is used by the logger, but the insertion order is - * probably irrelevant for logging. I.e. it might be ok if these sets were - * traversed in non-deterministic order. - */ - /** * ================================ * SymbExLogger Usage @@ -192,69 +185,19 @@ import scala.util.{Failure, Success, Try} * // SymbExLogger.currentLog().markReachable(uidBranchPoint) */ -object SymbExLogger { - /** Collection of logged Method/Predicates/Functions. **/ - val memberList: ArrayBuffer[SymbLog] = ArrayBuffer() - var _currentLog: ThreadLocal[Option[SymbLog]] = ThreadLocal.withInitial(() => None) - - private val uidCounter = new AtomicInteger(0) - - var enabled = false - var logConfig: LogConfig = LogConfig.default() - var listenerProvider: LogConfig => SymbLogListener = new InMemorySymbLog(_) - - def freshUid(): Int = uidCounter.getAndIncrement() - - /** Add a new log for a method, function or predicate (member). - * - * @param member Either a MethodRecord, PredicateRecord or a FunctionRecord. - * @param s Current state. Since the body of the method (predicate/function) is not yet - * executed/logged, this is usually the empty state (use Σ(Ø, Ø, Ø) for empty - * state). - * @param pcs Current path conditions. - */ - @elidable(INFO) - def openMemberScope(member: ast.Member, s: State, pcs: PathConditionStack): Unit = { - val log = new SymbLog(listenerProvider(logConfig), member, s, pcs) - memberList.synchronized { memberList += log } - _currentLog.set(Some(log)) - } - - /** Use this method to access the current log, e.g., to access the log of the method - * that gets currently symbolically executed. - * - * @return Returns the current method, predicate or function that is being logged. - */ - def currentLog(): SymbLog = { - if (enabled) - _currentLog.get.get - else NoopSymbLog - } - - @elidable(INFO) - def closeMemberScope(): Unit = { - if (enabled) { - currentLog().closeMemberScope() - _currentLog.set(None) - } - } - - /** - * Passes config from Silicon to SymbExLogger. - * - * @param c Config of Silicon. - */ - def setConfig(c: Config): Unit = { - setEnabled(c.ideModeAdvanced()) - logConfig = parseLogConfig(c) - } - - def setListenerProvider(listener: LogConfig => SymbLogListener): Unit = - listenerProvider = listener - - @elidable(INFO) - private def setEnabled(b: Boolean): Unit = { - enabled = b +case object SymbExLogger { + def currentLog(): MemberSymbExLog = ??? + def memberList: Seq[SymbExLog] = ??? + def logConfig: LogConfig = ??? + def openMemberScope(x: Any, y: Any, z: Any): Unit = ??? + def closeMemberScope(): Unit = ??? + def enabled: Boolean = ??? + + def ofConfig(c: Config): SymbExLogger[_] = { + if(c.ideModeAdvanced()) + SymbExLog(parseLogConfig(c)) + else + NoopSymbExLog } private def parseLogConfig(c: Config): LogConfig = { @@ -269,129 +212,75 @@ object SymbExLogger { case Failure(_) => LogConfig.default() } } - - /** - * Simple string representation of the logs. - */ - def toSimpleTreeString: String = { - if (enabled) { - val simpleTreeRenderer = new SimpleTreeRenderer() - simpleTreeRenderer.render(memberList.map(_.listener).collect { case l: InMemorySymbLog => l }) - } else "" - } - - /** Path to the file that is being executed. Is used for UnitTesting. **/ - var filePath: Path = _ - - /** - * Resets the SymbExLogger-object, to make it ready for a new file. - * Only needed when several files are verified together (e.g., sbt test). - */ - def reset(): Unit = { - memberList.clear() - uidCounter.set(0) - filePath = null - logConfig = LogConfig.default() - listenerProvider = new InMemorySymbLog(_) - } - - def resetMemberList(): Unit = { - memberList.clear() - } } -//========================= SymbLog ======================== +abstract class SymbExLogger[Log <: MemberSymbExLogger]() { + /** Collection of logged Method/Predicates/Functions. */ + protected var members: immutable.Map[ast.Member, Log] = Map.empty + protected val uidCounter: AtomicInteger = new AtomicInteger(0) -trait SymbLogListener { - def appendDataRecord(symbLog: SymbLog, r: DataRecord): Unit - def appendScopingRecord(symbLog: SymbLog, r: ScopingRecord, ignoreBranchingStack: Boolean = false): Unit - def appendBranchingRecord(symbLog: SymbLog, r: BranchingRecord): Unit + def newEntityLogger(member: ast.Member, s: State, pcs: PathConditionStack): Log + def config: LogConfig - def switchToNextBranch(symbLog: SymbLog, uidBranchPoint: Int): Unit - def markBranchReachable(symbLog: SymbLog, uidBranchPoint: Int): Unit - def endBranchPoint(symbLog: SymbLog, uidBranchPoint: Int): Unit -} - -class InMemorySymbLog(config: LogConfig) extends SymbLogListener { - /** top level log entries for this member; these log entries were recorded consecutively without branching; - * in case branching occured, one of these records is a BranchingRecord with all branches as field attached to it */ - var log: Vector[SymbolicRecord] = Vector[SymbolicRecord]() + def freshUid(): Int = uidCounter.getAndIncrement() - /** this stack keeps track of BranchingRecords while adding records to the log; as soon as all branches of a - * BranchingRecord are done, logging has to switch back to the previous BranchingRecord */ - var branchingStack: List[BranchingRecord] = List[BranchingRecord]() + def whenEnabled(f: => Unit): Unit = f - /** if a record was ignored due to the logConfig, its ID is tracked here and corresponding open and close scope - * records will be ignored too */ - var ignoredDataRecords: Set[Int] = Set() + def logs: Iterable[Log] = members.values - def appendRecord(r: SymbolicRecord, ignoreBranchingStack: Boolean = false): Unit = { - if (branchingStack.isEmpty || ignoreBranchingStack) { - log = log :+ r - } else { - branchingStack.head.appendLog(r) - } - } + /** Add a new log for a method, function or predicate (member). + * + * @param member Either a MethodRecord, PredicateRecord or a FunctionRecord. + * @param s Current state. Since the body of the method (predicate/function) is not yet + * executed/logged, this is usually the empty state (use Σ(Ø, Ø, Ø) for empty + * state). + * @param pcs Current path conditions. + */ + @elidable(INFO) + def openMemberScope(member: ast.Member, s: State, pcs: PathConditionStack): Log = { + val log = newEntityLogger(member, s, pcs) - override def appendDataRecord(symbLog: SymbLog, r: DataRecord): Unit = { - val shouldIgnore = config.getRecordConfig(r) match { - case Some(_) => config.isBlackList - case None => !config.isBlackList + members.synchronized { + members += member -> log } - if(shouldIgnore) { - ignoredDataRecords = ignoredDataRecords + r.id - } else { - appendRecord(r) - } + log } +} - override def appendScopingRecord(symbLog: SymbLog, r: ScopingRecord, ignoreBranchingStack: Boolean): Unit = { - if(!ignoredDataRecords.contains(r.refId)) { - if(ignoreBranchingStack) { - log = log :+ r - } else { - appendRecord(r) - } - } - } +case object NoopSymbExLog extends SymbExLogger[NoopMemberSymbExLog.type] { + override def newEntityLogger(member: Member, s: State, pcs: PathConditionStack): NoopMemberSymbExLog.type = + NoopMemberSymbExLog - override def appendBranchingRecord(symbLog: SymbLog, r: BranchingRecord): Unit = { - appendRecord(r) - branchingStack +:= r - } + override def config: LogConfig = null - override def switchToNextBranch(symbLog: SymbLog, uidBranchPoint: Int): Unit = { - assert(branchingStack.nonEmpty) - val branchingRecord = branchingStack.head - assert(branchingRecord.id == uidBranchPoint) - // no close scope is inserted because branches are not considered scopes - branchingRecord.switchToNextBranch() - } + override def whenEnabled(f: => Unit): Unit = {} +} - override def markBranchReachable(symbLog: SymbLog, uidBranchPoint: Int): Unit = { - assert(branchingStack.nonEmpty) - val branchingRecord = branchingStack.head - assert(branchingRecord.id == uidBranchPoint) - branchingRecord.markReachable() - } +case class SymbExLog(config: LogConfig) extends SymbExLogger[MemberSymbExLog]() { + override def newEntityLogger(member: ast.Member, s: State, pcs: PathConditionStack): MemberSymbExLog = + new MemberSymbExLog(this, member, s, pcs) - override def endBranchPoint(symbLog: SymbLog, uidBranchPoint: Int): Unit = { - assert(branchingStack.nonEmpty) - val branchingRecord = branchingStack.head - assert(branchingRecord.id == uidBranchPoint) - // no close scope is inserted because branches are not considered scopes - branchingStack = branchingStack.tail + /** + * Simple string representation of the logs. + */ + def toSimpleTreeString: String = { + val simpleTreeRenderer = new SimpleTreeRenderer() + simpleTreeRenderer.render(members.values) } } -/** - * Concept: One object of SymbLog per Method/Predicate/Function. SymbLog - * is used in the SymbExLogger-object. - */ -class SymbLog(val listener: SymbLogListener, val v: ast.Member, val s: State, val pcs: PathConditionStack) { - val logger: Logger = - Logger(LoggerFactory.getLogger(s"${this.getClass.getName}")) +abstract class MemberSymbExLogger(log: SymbExLogger[_], + val member: ast.Member, + val state: State, + val pcs: PathConditionStack) { + def appendDataRecord(r: DataRecord): Unit + def appendScopingRecord(r: ScopingRecord, ignoreBranchingStack: Boolean = false): Unit + def appendBranchingRecord(r: BranchingRecord): Unit + + def switchToNextBranch(uidBranchPoint: Int): Unit + def markBranchReachable(uidBranchPoint: Int): Unit + def endBranchPoint(uidBranchPoint: Int): Unit /** * indicates whether this member's close was already closed @@ -406,39 +295,41 @@ class SymbLog(val listener: SymbLogListener, val v: ast.Member, val s: State, va // Maps macros to their body private var _macros = Map[App, Term]() - val main: MemberRecord = v match { - case m: ast.Method => new MethodRecord(m, s, pcs) - case p: ast.Predicate => new PredicateRecord(p, s, pcs) - case f: ast.Function => new FunctionRecord(f, s, pcs) - case _ => null + val main: MemberRecord = member match { + case m: ast.Method => new MethodRecord(m, state, pcs) + case p: ast.Predicate => new PredicateRecord(p, state, pcs) + case f: ast.Function => new FunctionRecord(f, state, pcs) + case _ => ??? } openScope(main) /** * Inserts the record as well as a corresponding open scope record into the log + * * @param s non-null record * @return id with which closeScope should be called */ @elidable(INFO) def openScope(s: DataRecord): Int = { - s.id = SymbExLogger.freshUid() - listener.appendDataRecord(this, s) + s.id = log.freshUid() + appendDataRecord(s) insert(new OpenScopeRecord(s)) s.id } /** * Appends a scoping record to the log unless it's referenced data record is ignored - * @param s non-null scoping record + * + * @param s non-null scoping record * @param ignoreBranchingStack true if the record should always be inserted in the root level * @return id of the scoping record */ @elidable(INFO) private def insert(s: ScopingRecord, ignoreBranchingStack: Boolean = false): Int = { - s.id = SymbExLogger.freshUid() + s.id = log.freshUid() s.timeMs = System.currentTimeMillis() - listener.appendScopingRecord(this, s, ignoreBranchingStack) + appendScopingRecord(s, ignoreBranchingStack) s.id } @@ -446,38 +337,32 @@ class SymbLog(val listener: SymbLogListener, val v: ast.Member, val s: State, va * Creates and appends a branching record to the log. Branching records do not cause scopes. * Use `switchToNextBranch` to change from the current to the next branch and `endBranchPoint` to conclude the * branch point after all branches were visited. + * * @param possibleBranchesCount number of branches that this branch point has but are not necessarily all reachable - * @param condition branch condition + * @param condition branch condition * @return id of the branching record */ @elidable(INFO) def insertBranchPoint(possibleBranchesCount: Int, condition: Option[Term] = None, conditionExp: Option[Exp] = None): Int = { val branchingRecord = new BranchingRecord(possibleBranchesCount, condition, conditionExp) - branchingRecord.id = SymbExLogger.freshUid() - listener.appendBranchingRecord(this, branchingRecord) + branchingRecord.id = log.freshUid() + appendBranchingRecord(branchingRecord) branchingRecord.id } - /** - * Changes from the current to the next branch of a specific branch point - * @param uidBranchPoint id of the branching record - */ - @elidable(INFO) - def switchToNextBranch(uidBranchPoint: Int): Unit = { - listener.switchToNextBranch(this, uidBranchPoint) - } - /** * Marks the current branch of a specific branch point as being reachable + * * @param uidBranchPoint id of the branching record */ @elidable(INFO) def markReachable(uidBranchPoint: Int): Unit = { - listener.markBranchReachable(this, uidBranchPoint) + markBranchReachable(uidBranchPoint) } /** * Ends the scope of a specific data record by inserting a corresponding close scope record into the log + * * @param n id of the data record */ @elidable(INFO) @@ -486,15 +371,6 @@ class SymbLog(val listener: SymbLogListener, val v: ast.Member, val s: State, va insert(closeRecord) } - /** - * Concludes a specific branch point (which normaly happens after visiting all branches belonging to the branch point) - * @param uidBranchPoint id of the branch point - */ - @elidable(INFO) - def endBranchPoint(uidBranchPoint: Int): Unit = { - listener.endBranchPoint(this, uidBranchPoint) - } - /** * Ends the scope of the member (i.e. main) by inserting a corresponding close scope record into the log */ @@ -540,6 +416,7 @@ class SymbLog(val listener: SymbLogListener, val v: ast.Member, val s: State, va /** * Calculates the diff between the current and last statistics query. * The difference is calculated if value can be converted to an int or double + * * @return map with the current statistics, and the differences (only containing values that could be converted) * and keys with appended "-delta" */ @@ -576,19 +453,94 @@ class SymbLog(val listener: SymbLogListener, val v: ast.Member, val s: State, va def addMacro(m: App, body: Term): Unit = { _macros = _macros + (m -> body) } - - override def toString: String = listener match { - case log: InMemorySymbLog => new SimpleTreeRenderer().renderMember(log) - case _ => super.toString - } } -object NoopSymbLog extends SymbLog(null, null, null, null) { - override def openScope(s: DataRecord): Int = 0 - override def insertBranchPoint(possibleBranchesCount: Int, condition: Option[Term], conditionExp: Option[Exp]): Int = 0 +case object NoopMemberSymbExLog extends MemberSymbExLogger(null, null, null, null) { + override def appendDataRecord(r: DataRecord): Unit = {} + override def appendScopingRecord(r: ScopingRecord, ignoreBranchingStack: Boolean): Unit = {} + override def appendBranchingRecord(r: BranchingRecord): Unit = {} + override def markBranchReachable(uidBranchPoint: Int): Unit = {} override def switchToNextBranch(uidBranchPoint: Int): Unit = {} - override def markReachable(uidBranchPoint: Int): Unit = {} - override def closeScope(n: Int): Unit = {} override def endBranchPoint(uidBranchPoint: Int): Unit = {} - override def closeMemberScope(): Unit = {} } + +class MemberSymbExLog(rootLog: SymbExLogger[MemberSymbExLog], + member: ast.Member, + state: State, + pcs: PathConditionStack) extends MemberSymbExLogger(rootLog, member, state, pcs) { + def close(): Unit = ??? // clear from log, add close record? + + /** top level log entries for this member; these log entries were recorded consecutively without branching; + * in case branching occured, one of these records is a BranchingRecord with all branches as field attached to it */ + var log: Vector[SymbolicRecord] = Vector[SymbolicRecord]() + + /** this stack keeps track of BranchingRecords while adding records to the log; as soon as all branches of a + * BranchingRecord are done, logging has to switch back to the previous BranchingRecord */ + var branchingStack: List[BranchingRecord] = List[BranchingRecord]() + + /** if a record was ignored due to the logConfig, its ID is tracked here and corresponding open and close scope + * records will be ignored too */ + var ignoredDataRecords: Set[Int] = Set() + + override def toString: String = + new SimpleTreeRenderer().renderMember(this) + + def appendRecord(r: SymbolicRecord, ignoreBranchingStack: Boolean = false): Unit = { + if (branchingStack.isEmpty || ignoreBranchingStack) { + log = log :+ r + } else { + branchingStack.head.appendLog(r) + } + } + + override def appendDataRecord(r: DataRecord): Unit = { + val shouldIgnore = rootLog.config.getRecordConfig(r) match { + case Some(_) => rootLog.config.isBlackList + case None => !rootLog.config.isBlackList + } + + if (shouldIgnore) { + ignoredDataRecords = ignoredDataRecords + r.id + } else { + appendRecord(r) + } + } + + override def appendScopingRecord(r: ScopingRecord, ignoreBranchingStack: Boolean): Unit = { + if (!ignoredDataRecords.contains(r.refId)) { + if (ignoreBranchingStack) { + log = log :+ r + } else { + appendRecord(r) + } + } + } + + override def appendBranchingRecord(r: BranchingRecord): Unit = { + appendRecord(r) + branchingStack +:= r + } + + override def switchToNextBranch(uidBranchPoint: Int): Unit = { + assert(branchingStack.nonEmpty) + val branchingRecord = branchingStack.head + assert(branchingRecord.id == uidBranchPoint) + // no close scope is inserted because branches are not considered scopes + branchingRecord.switchToNextBranch() + } + + override def markBranchReachable(uidBranchPoint: Int): Unit = { + assert(branchingStack.nonEmpty) + val branchingRecord = branchingStack.head + assert(branchingRecord.id == uidBranchPoint) + branchingRecord.markReachable() + } + + override def endBranchPoint(uidBranchPoint: Int): Unit = { + assert(branchingStack.nonEmpty) + val branchingRecord = branchingStack.head + assert(branchingRecord.id == uidBranchPoint) + // no close scope is inserted because branches are not considered scopes + branchingStack = branchingStack.tail + } +} \ No newline at end of file diff --git a/src/main/scala/logger/renderer/SimpleTreeRenderer.scala b/src/main/scala/logger/renderer/SimpleTreeRenderer.scala index ffa96f802..e7b35a528 100644 --- a/src/main/scala/logger/renderer/SimpleTreeRenderer.scala +++ b/src/main/scala/logger/renderer/SimpleTreeRenderer.scala @@ -6,16 +6,17 @@ package viper.silicon.logger.renderer -import scala.annotation.unused -import viper.silicon.logger.InMemorySymbLog +import viper.silicon.logger.MemberSymbExLog import viper.silicon.logger.records.SymbolicRecord import viper.silicon.logger.records.data.DataRecord import viper.silicon.logger.records.scoping.{CloseScopeRecord, OpenScopeRecord} import viper.silicon.logger.records.structural.{BranchingRecord, JoiningRecord} import viper.silicon.state.terms.Not -class SimpleTreeRenderer extends Renderer[InMemorySymbLog, String] { - def render(memberList: Iterable[InMemorySymbLog]): String = { +import scala.annotation.unused + +class SimpleTreeRenderer extends Renderer[MemberSymbExLog, String] { + def render(memberList: Iterable[MemberSymbExLog]): String = { var res = "" for (m <- memberList) { res = res + renderMember(m) + "\n" @@ -23,7 +24,7 @@ class SimpleTreeRenderer extends Renderer[InMemorySymbLog, String] { res } - def renderMember(member: InMemorySymbLog): String = { + def renderMember(member: MemberSymbExLog): String = { // val filteredLog = filterEmptyScopes(member.log) toSimpleTree(member.log, 0, 0) } diff --git a/src/main/scala/logger/writer/SymbExLogReportWriter.scala b/src/main/scala/logger/writer/SymbExLogReportWriter.scala index 40ba9cefa..8f1af0749 100644 --- a/src/main/scala/logger/writer/SymbExLogReportWriter.scala +++ b/src/main/scala/logger/writer/SymbExLogReportWriter.scala @@ -10,7 +10,7 @@ import spray.json.{JsArray, JsBoolean, JsNull, JsNumber, JsObject, JsString, JsT import viper.silicon.Map import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.interfaces.state.Chunk -import viper.silicon.logger.InMemorySymbLog +import viper.silicon.logger.MemberSymbExLog import viper.silicon.logger.records.scoping.{CloseScopeRecord, OpenScopeRecord} import viper.silicon.logger.records.structural.{BranchInfo, BranchingRecord, JoiningRecord} import viper.silicon.logger.records.{RecordData, SymbolicRecord} @@ -107,9 +107,9 @@ object SymbExLogReportWriter { * @param members A symbolic log per member to translate. * @return array of all records. */ - def toJSON(members: Seq[InMemorySymbLog]): JsArray = { + def toJSON(members: Seq[MemberSymbExLog]): JsArray = { val records = members.foldLeft(Vector[JsValue]()) { - (prevVal: Vector[JsValue], member: InMemorySymbLog) => prevVal ++ toJSON(member) + (prevVal: Vector[JsValue], member: MemberSymbExLog) => prevVal ++ toJSON(member) } JsArray(records) } @@ -119,7 +119,7 @@ object SymbExLogReportWriter { * @param symbLog The symbolic log to translate. * @return array of all records. */ - def toJSON(symbLog: InMemorySymbLog): Vector[JsValue] = { + def toJSON(symbLog: MemberSymbExLog): Vector[JsValue] = { val allRecords = getAllRecords(symbLog.log) allRecords.map(toJSON).toVector } diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index d8a2feb4d..98da3b8fd 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -196,9 +196,7 @@ class DefaultMainVerifier(config: Config, override val reporter: Reporter) allProvers.saturate(config.proverSaturationTimeouts.afterPrelude) - - SymbExLogger.resetMemberList() - SymbExLogger.setConfig(config) + ??? // make loggers here /* TODO: A workaround for Silver issue #94. toList must be before flatMap. * Otherwise Set will be used internally and some error messages will be lost. From 0ea06e8e0da171781df76cd97748c7c18f31dc53 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Thu, 17 Nov 2022 11:39:47 +0100 Subject: [PATCH 06/31] make Verifier own a current MemberSymbExLogger --- src/main/scala/verifier/BaseVerifier.scala | 5 +++++ src/main/scala/verifier/DefaultMainVerifier.scala | 4 +++- src/main/scala/verifier/Verifier.scala | 6 +++++- 3 files changed, 13 insertions(+), 2 deletions(-) diff --git a/src/main/scala/verifier/BaseVerifier.scala b/src/main/scala/verifier/BaseVerifier.scala index fd867919f..ec02407f5 100644 --- a/src/main/scala/verifier/BaseVerifier.scala +++ b/src/main/scala/verifier/BaseVerifier.scala @@ -12,6 +12,7 @@ import viper.silicon.Config.StateConsolidationMode import viper.silver.components.StatefulComponent import viper.silicon.{utils, _} import viper.silicon.decider.{DefaultDeciderProvider, TermToSMTLib2Converter} +import viper.silicon.logger.MemberSymbExLogger import viper.silicon.state._ import viper.silicon.state.terms.{AxiomRewriter, TriggerGenerator} import viper.silicon.supporters._ @@ -35,6 +36,10 @@ abstract class BaseVerifier(val config: Config, val logger: Logger = Logger(LoggerFactory.getLogger(s"${this.getClass.getName}-$uniqueId")) + private var currentSymbExLog: Option[MemberSymbExLogger] = None + override def symbExLog: MemberSymbExLogger = currentSymbExLog.get + override def symbExLog_=(logger: MemberSymbExLogger): Unit = { currentSymbExLog = Some(logger) } + private val counters = mutable.Map[AnyRef, Counter]() def counter(id: AnyRef): Counter = { diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 98da3b8fd..46dda56f9 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -19,7 +19,7 @@ import viper.silicon.decider.SMTLib2PreambleReader import viper.silicon.extensions.ConditionalPermissionRewriter import viper.silicon.interfaces._ import viper.silicon.interfaces.decider.ProverLike -import viper.silicon.logger.SymbExLogger +import viper.silicon.logger.{MemberSymbExLogger, SymbExLogger} import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult} import viper.silicon.state._ import viper.silicon.state.terms.{Decl, Sort, Term, sorts} @@ -54,6 +54,8 @@ class DefaultMainVerifier(config: Config, override val reporter: Reporter) private val uniqueIdCounter = new Counter(1) def nextUniqueVerifierId(): String = f"${uniqueIdCounter.next()}%02d" + val rootSymbExLogger: SymbExLogger[_] = SymbExLogger.ofConfig(config) + protected val preambleReader = new SMTLib2PreambleReader protected val sequencesContributor = new DefaultSequencesContributor(domainTranslator, config) diff --git a/src/main/scala/verifier/Verifier.scala b/src/main/scala/verifier/Verifier.scala index e0298a9e1..d7a2eda10 100644 --- a/src/main/scala/verifier/Verifier.scala +++ b/src/main/scala/verifier/Verifier.scala @@ -14,14 +14,18 @@ import viper.silicon.rules.StateConsolidationRules import viper.silicon.state.{IdentifierFactory, SymbolConverter} import viper.silicon.supporters.{QuantifierSupporter, SnapshotSupporter} import viper.silicon.utils.Counter -import viper.silicon.{Config} +import viper.silicon.Config +import viper.silicon.logger.MemberSymbExLogger import viper.silver.ast import viper.silver.reporter.Reporter + import java.util.concurrent.atomic.AtomicInteger trait Verifier { def uniqueId: String + def symbExLog: MemberSymbExLogger + def symbExLog_=(logger: MemberSymbExLogger): Unit def logger: Logger def reporter: Reporter def counter(id: AnyRef): Counter From bd87c973ef8a404e3f4176e7d9d6277cb35f7e19 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Thu, 17 Nov 2022 13:13:13 +0100 Subject: [PATCH 07/31] Give Verifier the capability to open symbexlogs for members The root symbexlog comes from Silicon and is computed explicitly on configuration, so it can be overridden From there, the MainVerifier owns the root log, and WorkerVerifiers ask the MainVerifier for a member-scoped symbexlog --- src/main/scala/Silicon.scala | 10 +++++++--- src/main/scala/logger/SymbExLogger.scala | 2 +- src/main/scala/verifier/BaseVerifier.scala | 4 ++-- src/main/scala/verifier/DefaultMainVerifier.scala | 11 +++++++---- src/main/scala/verifier/Verifier.scala | 2 +- src/main/scala/verifier/WorkerVerifier.scala | 5 +++++ src/test/scala/SymbExLoggerTests.scala | 7 ++----- 7 files changed, 25 insertions(+), 16 deletions(-) diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala index eb04c91df..7c1c2a006 100644 --- a/src/main/scala/Silicon.scala +++ b/src/main/scala/Silicon.scala @@ -8,7 +8,6 @@ package viper.silicon import java.text.SimpleDateFormat import java.util.concurrent.{Callable, Executors, TimeUnit, TimeoutException} - import scala.collection.immutable.ArraySeq import scala.util.{Left, Right} import ch.qos.logback.classic.{Level, Logger} @@ -19,7 +18,7 @@ import viper.silver.frontend.{DefaultStates, SilFrontend} import viper.silver.reporter._ import viper.silver.verifier.{AbstractVerificationError => SilAbstractVerificationError, Failure => SilFailure, Success => SilSuccess, TimeoutOccurred => SilTimeoutOccurred, VerificationResult => SilVerificationResult, Verifier => SilVerifier} import viper.silicon.interfaces.Failure -import viper.silicon.logger.SymbExLogger +import viper.silicon.logger.{MemberSymbExLogger, SymbExLogger} import viper.silicon.reporting.{MultiRunRecorders, condenseToViperResult} import viper.silicon.verifier.DefaultMainVerifier import viper.silicon.decider.{Cvc5ProverStdIO, Z3ProverStdIO} @@ -93,6 +92,10 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)] private var _config: Config = _ final def config = _config + private var _symbExLog: SymbExLogger[_ <: MemberSymbExLogger] = _ + final def symbExLog = _symbExLog + final def symbExLog_=(log: SymbExLogger[_ <: MemberSymbExLogger]) = { _symbExLog = log } + private sealed trait LifetimeState private object LifetimeState { @@ -113,6 +116,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)] lifetimeState = LifetimeState.Configured _config = new Config(args) + _symbExLog = SymbExLogger.ofConfig(_config) } def debugInfo(debugInfo: Seq[(String, Any)]): Unit = { this.debugInfo = debugInfo } @@ -129,7 +133,7 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)] setLogLevelsFromConfig() - verifier = new DefaultMainVerifier(config, reporter) + verifier = new DefaultMainVerifier(config, reporter, symbExLog) verifier.start() } diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index eaa2cbe73..588583702 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -193,7 +193,7 @@ case object SymbExLogger { def closeMemberScope(): Unit = ??? def enabled: Boolean = ??? - def ofConfig(c: Config): SymbExLogger[_] = { + def ofConfig(c: Config): SymbExLogger[_ <: MemberSymbExLogger] = { if(c.ideModeAdvanced()) SymbExLog(parseLogConfig(c)) else diff --git a/src/main/scala/verifier/BaseVerifier.scala b/src/main/scala/verifier/BaseVerifier.scala index ec02407f5..2aa9efb81 100644 --- a/src/main/scala/verifier/BaseVerifier.scala +++ b/src/main/scala/verifier/BaseVerifier.scala @@ -36,9 +36,9 @@ abstract class BaseVerifier(val config: Config, val logger: Logger = Logger(LoggerFactory.getLogger(s"${this.getClass.getName}-$uniqueId")) - private var currentSymbExLog: Option[MemberSymbExLogger] = None + private var currentSymbExLog: Option[_ <: MemberSymbExLogger] = None override def symbExLog: MemberSymbExLogger = currentSymbExLog.get - override def symbExLog_=(logger: MemberSymbExLogger): Unit = { currentSymbExLog = Some(logger) } + protected def symbExLog_=(logger: MemberSymbExLogger): Unit = { currentSymbExLog = Some(logger) } private val counters = mutable.Map[AnyRef, Counter]() diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 46dda56f9..4a69ddcd6 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -41,9 +41,12 @@ import viper.silver.verifier.TypecheckerWarning trait MainVerifier extends Verifier { def nextUniqueVerifierId(): String def verificationPoolManager: VerificationPoolManager + def rootSymbExLogger: SymbExLogger[_ <: MemberSymbExLogger] } -class DefaultMainVerifier(config: Config, override val reporter: Reporter) +class DefaultMainVerifier(config: Config, + override val reporter: Reporter, + override val rootSymbExLogger: SymbExLogger[_ <: MemberSymbExLogger]) extends BaseVerifier(config, "00") with MainVerifier with DefaultFunctionVerificationUnitProvider @@ -54,7 +57,9 @@ class DefaultMainVerifier(config: Config, override val reporter: Reporter) private val uniqueIdCounter = new Counter(1) def nextUniqueVerifierId(): String = f"${uniqueIdCounter.next()}%02d" - val rootSymbExLogger: SymbExLogger[_] = SymbExLogger.ofConfig(config) + override def openSymbExLogger(member: Member): Unit = { + symbExLog = rootSymbExLogger.newEntityLogger(member, null, decider.pcs) + } protected val preambleReader = new SMTLib2PreambleReader @@ -198,8 +203,6 @@ class DefaultMainVerifier(config: Config, override val reporter: Reporter) allProvers.saturate(config.proverSaturationTimeouts.afterPrelude) - ??? // make loggers here - /* TODO: A workaround for Silver issue #94. toList must be before flatMap. * Otherwise Set will be used internally and some error messages will be lost. */ diff --git a/src/main/scala/verifier/Verifier.scala b/src/main/scala/verifier/Verifier.scala index d7a2eda10..3b1f08b5a 100644 --- a/src/main/scala/verifier/Verifier.scala +++ b/src/main/scala/verifier/Verifier.scala @@ -25,7 +25,7 @@ trait Verifier { def uniqueId: String def symbExLog: MemberSymbExLogger - def symbExLog_=(logger: MemberSymbExLogger): Unit + def openSymbExLogger(member: ast.Member): Unit def logger: Logger def reporter: Reporter def counter(id: AnyRef): Counter diff --git a/src/main/scala/verifier/WorkerVerifier.scala b/src/main/scala/verifier/WorkerVerifier.scala index a36b4a0af..265957317 100644 --- a/src/main/scala/verifier/WorkerVerifier.scala +++ b/src/main/scala/verifier/WorkerVerifier.scala @@ -7,6 +7,7 @@ package viper.silicon.verifier import viper.silicon.supporters._ +import viper.silver.ast.Member import viper.silver.components.StatefulComponent import viper.silver.reporter.Reporter @@ -24,6 +25,10 @@ class WorkerVerifier(mainVerifier: MainVerifier, def verificationPoolManager: VerificationPoolManager = mainVerifier.verificationPoolManager + override def openSymbExLogger(member: Member): Unit = { + symbExLog = mainVerifier.rootSymbExLogger.newEntityLogger(member, null, decider.pcs) + } + /* Lifetime */ override def start(): Unit = { diff --git a/src/test/scala/SymbExLoggerTests.scala b/src/test/scala/SymbExLoggerTests.scala index 6601faf21..670d1e035 100644 --- a/src/test/scala/SymbExLoggerTests.scala +++ b/src/test/scala/SymbExLoggerTests.scala @@ -8,8 +8,7 @@ package viper.silicon.tests import java.io.File import java.nio.file.{Files, Path, Paths} - -import viper.silicon.logger.SymbExLogger +import viper.silicon.logger.{SymbExLog, SymbExLogger} import viper.silver.testing.{LocatedAnnotation, MissingOutput, SilSuite, UnexpectedOutput} import viper.silver.verifier.{AbstractError, Verifier, Failure => SilFailure, Success => SilSuccess, VerificationResult => SilVerificationResult} import viper.silicon.{Silicon, SiliconFrontend} @@ -28,8 +27,6 @@ class SymbExLoggerTests extends SilSuite { // to be tested must be known, which is why it's passed here to the SymbExLogger-Object. // SymbExLogger.reset() cleans the logging object (only relevant for verifying multiple // tests at once, e.g. with the 'test'-sbt-command. - SymbExLogger.reset() - SymbExLogger.filePath = files.head val fe = new SiliconFrontendWithUnitTesting(files.head) fe.init(verifier) fe.reset(files.head) @@ -90,7 +87,7 @@ class SiliconFrontendWithUnitTesting(path: Path) extends SiliconFrontend(NoopRep if (testIsExecuted) { val pw = new java.io.PrintWriter(new File(actualPath)) - try pw.write(SymbExLogger.toSimpleTreeString) finally pw.close() + try pw.write(siliconInstance.symbExLog.asInstanceOf[SymbExLog].toSimpleTreeString) finally pw.close() val expectedSource = scala.io.Source.fromFile(expectedPath) val expected = expectedSource.getLines() From 35a2ff08800b2957720caac96e586cc562baf38f Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Thu, 17 Nov 2022 13:55:42 +0100 Subject: [PATCH 08/31] swap out shims --- src/main/scala/decider/Decider.scala | 28 +++++++++---------- src/main/scala/logger/SymbExLogger.scala | 10 +++---- .../scala/logger/records/SymbolicRecord.scala | 4 ++- .../logger/records/data/DataRecord.scala | 14 +++++----- .../logger/records/data/MemberRecord.scala | 5 ++-- .../records/data/ProverAssertRecord.scala | 5 ++-- .../records/scoping/ScopingRecord.scala | 5 ++-- .../logger/writer/SymbExLogReportWriter.scala | 14 +++++----- src/main/scala/rules/Brancher.scala | 10 +++---- src/main/scala/rules/Consumer.scala | 16 +++++------ src/main/scala/rules/Evaluator.scala | 20 ++++++------- .../scala/rules/ExecutionFlowController.scala | 4 +-- src/main/scala/rules/Executor.scala | 26 ++++++++--------- src/main/scala/rules/Joiner.scala | 4 +-- .../rules/MoreCompleteExhaleSupporter.scala | 2 +- src/main/scala/rules/Producer.scala | 16 +++++------ .../scala/rules/QuantifiedChunkSupport.scala | 6 ++-- src/main/scala/rules/StateConsolidator.scala | 16 +++++------ .../scala/supporters/MethodSupporter.scala | 8 +++--- .../PredicateVerificationUnit.scala | 4 +-- .../functions/FunctionVerificationUnit.scala | 4 +-- .../scala/verifier/DefaultMainVerifier.scala | 2 +- 22 files changed, 114 insertions(+), 109 deletions(-) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 3b48ab6b1..1dffc792a 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -178,18 +178,18 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => def pushScope(): Unit = { //val commentRecord = new CommentRecord("push", null, null) - //val sepIdentifier = SymbExLogger.currentLog().openScope(commentRecord) + //val sepIdentifier = symbExLog.openScope(commentRecord) pathConditions.pushScope() _prover.push(timeout = Verifier.config.pushTimeout.toOption) - //SymbExLogger.currentLog().closeScope(sepIdentifier) + //symbExLog.closeScope(sepIdentifier) } def popScope(): Unit = { //val commentRecord = new CommentRecord("pop", null, null) - //val sepIdentifier = SymbExLogger.currentLog().openScope(commentRecord) + //val sepIdentifier = symbExLog.openScope(commentRecord) _prover.pop() pathConditions.popScope() - //SymbExLogger.currentLog().closeScope(sepIdentifier) + //symbExLog.closeScope(sepIdentifier) } def setCurrentBranchCondition(t: Term, te: Option[ast.Exp] = None): Unit = { @@ -218,7 +218,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => private def assumeWithoutSmokeChecks(terms: InsertionOrderedSet[Term]) = { val assumeRecord = new DeciderAssumeRecord(terms) - val sepIdentifier = SymbExLogger.currentLog().openScope(assumeRecord) + val sepIdentifier = symbExLog.openScope(assumeRecord) /* Add terms to Silicon-managed path conditions */ terms foreach pathConditions.add @@ -226,7 +226,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => /* Add terms to the prover's assumptions */ terms foreach prover.assume - SymbExLogger.currentLog().closeScope(sepIdentifier) + symbExLog.closeScope(sepIdentifier) None } @@ -247,21 +247,21 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => // previously (it did not cause a verification failure) and ignore the // current one, because it cannot cause a verification error. if (success) - SymbExLogger.currentLog().discardSMTQuery() + symbExLog.discardSMTQuery() else - SymbExLogger.currentLog().setSMTQuery(t) + symbExLog.setSMTQuery(t) Q(success) } private def deciderAssert(t: Term, timeout: Option[Int]) = { val assertRecord = new DeciderAssertRecord(t, timeout) - val sepIdentifier = SymbExLogger.currentLog().openScope(assertRecord) + val sepIdentifier = symbExLog.openScope(assertRecord) val asserted = isKnownToBeTrue(t) val result = asserted || proverAssert(t, timeout) - SymbExLogger.currentLog().closeScope(sepIdentifier) + symbExLog.closeScope(sepIdentifier) result } @@ -275,15 +275,15 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => private def proverAssert(t: Term, timeout: Option[Int]) = { val assertRecord = new ProverAssertRecord(t, timeout) - val sepIdentifier = SymbExLogger.currentLog().openScope(assertRecord) + val sepIdentifier = symbExLog.openScope(assertRecord) val result = prover.assert(t, timeout) - if (SymbExLogger.enabled) { - assertRecord.statistics = Some(SymbExLogger.currentLog().deltaStatistics(prover.statistics())) + symbExLog.whenEnabled { + assertRecord.statistics = Some(symbExLog.deltaStatistics(prover.statistics())) } - SymbExLogger.currentLog().closeScope(sepIdentifier) + symbExLog.closeScope(sepIdentifier) result } diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index 588583702..c0926e7dd 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -188,10 +188,6 @@ import scala.util.{Failure, Success, Try} case object SymbExLogger { def currentLog(): MemberSymbExLog = ??? def memberList: Seq[SymbExLog] = ??? - def logConfig: LogConfig = ??? - def openMemberScope(x: Any, y: Any, z: Any): Unit = ??? - def closeMemberScope(): Unit = ??? - def enabled: Boolean = ??? def ofConfig(c: Config): SymbExLogger[_ <: MemberSymbExLogger] = { if(c.ideModeAdvanced()) @@ -253,8 +249,10 @@ case object NoopSymbExLog extends SymbExLogger[NoopMemberSymbExLog.type] { NoopMemberSymbExLog override def config: LogConfig = null - override def whenEnabled(f: => Unit): Unit = {} + + override def openMemberScope(member: Member, s: State, pcs: PathConditionStack): NoopMemberSymbExLog.type = + NoopMemberSymbExLog } case class SymbExLog(config: LogConfig) extends SymbExLogger[MemberSymbExLog]() { @@ -282,6 +280,8 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], def markBranchReachable(uidBranchPoint: Int): Unit def endBranchPoint(uidBranchPoint: Int): Unit + def whenEnabled(f: => Unit): Unit = log.whenEnabled(f) + /** * indicates whether this member's close was already closed */ diff --git a/src/main/scala/logger/records/SymbolicRecord.scala b/src/main/scala/logger/records/SymbolicRecord.scala index 38addaea6..e43432265 100644 --- a/src/main/scala/logger/records/SymbolicRecord.scala +++ b/src/main/scala/logger/records/SymbolicRecord.scala @@ -6,6 +6,8 @@ package viper.silicon.logger.records +import viper.silicon.logger.LogConfig + trait SymbolicRecord { var id: Int = -1 @@ -17,7 +19,7 @@ trait SymbolicRecord { def toSimpleString: String - def getData: RecordData = { + def getData(config: LogConfig): RecordData = { new RecordData() } } diff --git a/src/main/scala/logger/records/data/DataRecord.scala b/src/main/scala/logger/records/data/DataRecord.scala index f1f3eca5b..bfc2204c4 100644 --- a/src/main/scala/logger/records/data/DataRecord.scala +++ b/src/main/scala/logger/records/data/DataRecord.scala @@ -7,7 +7,7 @@ package viper.silicon.logger.records.data import viper.silicon.common.collections.immutable.InsertionOrderedSet -import viper.silicon.logger.SymbExLogger +import viper.silicon.logger.{LogConfig, SymbExLogger} import viper.silicon.logger.records.{RecordData, SymbolicRecord} import viper.silicon.state.State import viper.silicon.state.terms.Term @@ -35,24 +35,24 @@ trait DataRecord extends SymbolicRecord { else "null" } - override def getData: RecordData = { - val data = super.getData + override def getData(config: LogConfig): RecordData = { + val data = super.getData(config) value match { case posValue: ast.Node with Positioned => data.pos = Some(utils.ast.sourceLineColumn(posValue)) case _ => } if (state != null) { - if (SymbExLogger.logConfig.includeStore) { + if (config.includeStore) { data.store = Some(state.g) } - if (SymbExLogger.logConfig.includeHeap) { + if (config.includeHeap) { data.heap = Some(state.h) } - if (SymbExLogger.logConfig.includeOldHeap) { + if (config.includeOldHeap) { data.oldHeap = state.oldHeaps.get(Verifier.PRE_STATE_LABEL) } } - if (pcs != null && SymbExLogger.logConfig.includePcs) { + if (pcs != null && config.includePcs) { data.pcs = Some(pcs) } data diff --git a/src/main/scala/logger/records/data/MemberRecord.scala b/src/main/scala/logger/records/data/MemberRecord.scala index 2e7cd617e..55ee44184 100644 --- a/src/main/scala/logger/records/data/MemberRecord.scala +++ b/src/main/scala/logger/records/data/MemberRecord.scala @@ -6,14 +6,15 @@ package viper.silicon.logger.records.data +import viper.silicon.logger.LogConfig import viper.silicon.logger.records.RecordData import viper.silicon.state.terms.Term trait MemberRecord extends DataRecord { var lastFailedProverQuery: Option[Term] = None - override lazy val getData: RecordData = { - val data = super.getData + override def getData(config: LogConfig): RecordData = { + val data = super.getData(config) data.lastSMTQuery = lastFailedProverQuery data } diff --git a/src/main/scala/logger/records/data/ProverAssertRecord.scala b/src/main/scala/logger/records/data/ProverAssertRecord.scala index e1b5f3541..a0d88596a 100644 --- a/src/main/scala/logger/records/data/ProverAssertRecord.scala +++ b/src/main/scala/logger/records/data/ProverAssertRecord.scala @@ -9,6 +9,7 @@ package viper.silicon.logger.records.data import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.logger.records.RecordData import viper.silicon.Map +import viper.silicon.logger.LogConfig import viper.silicon.state.State import viper.silicon.state.terms.Term import viper.silver.ast @@ -26,8 +27,8 @@ class ProverAssertRecord(val term: Term, val timeout: Option[Int]) extends DataR else "null" } - override lazy val getData: RecordData = { - val data = super.getData + override def getData(config: LogConfig): RecordData = { + val data = super.getData(config) data.isSmtQuery = true data.smtStatistics = statistics data diff --git a/src/main/scala/logger/records/scoping/ScopingRecord.scala b/src/main/scala/logger/records/scoping/ScopingRecord.scala index 641a92da2..00264413a 100644 --- a/src/main/scala/logger/records/scoping/ScopingRecord.scala +++ b/src/main/scala/logger/records/scoping/ScopingRecord.scala @@ -6,14 +6,15 @@ package viper.silicon.logger.records.scoping +import viper.silicon.logger.LogConfig import viper.silicon.logger.records.{RecordData, SymbolicRecord} trait ScopingRecord extends SymbolicRecord { val refId: Int var timeMs: Long = 0 - override def getData: RecordData = { - val data = super.getData + override def getData(config: LogConfig): RecordData = { + val data = super.getData(config) data.refId = Some(refId) data.timeMs = Some(timeMs) data diff --git a/src/main/scala/logger/writer/SymbExLogReportWriter.scala b/src/main/scala/logger/writer/SymbExLogReportWriter.scala index 8f1af0749..096b62fad 100644 --- a/src/main/scala/logger/writer/SymbExLogReportWriter.scala +++ b/src/main/scala/logger/writer/SymbExLogReportWriter.scala @@ -10,7 +10,7 @@ import spray.json.{JsArray, JsBoolean, JsNull, JsNumber, JsObject, JsString, JsT import viper.silicon.Map import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.interfaces.state.Chunk -import viper.silicon.logger.MemberSymbExLog +import viper.silicon.logger.{LogConfig, MemberSymbExLog} import viper.silicon.logger.records.scoping.{CloseScopeRecord, OpenScopeRecord} import viper.silicon.logger.records.structural.{BranchInfo, BranchingRecord, JoiningRecord} import viper.silicon.logger.records.{RecordData, SymbolicRecord} @@ -107,9 +107,9 @@ object SymbExLogReportWriter { * @param members A symbolic log per member to translate. * @return array of all records. */ - def toJSON(members: Seq[MemberSymbExLog]): JsArray = { + def toJSON(members: Seq[MemberSymbExLog], config: LogConfig): JsArray = { val records = members.foldLeft(Vector[JsValue]()) { - (prevVal: Vector[JsValue], member: MemberSymbExLog) => prevVal ++ toJSON(member) + (prevVal: Vector[JsValue], member: MemberSymbExLog) => prevVal ++ toJSON(member, config) } JsArray(records) } @@ -119,9 +119,9 @@ object SymbExLogReportWriter { * @param symbLog The symbolic log to translate. * @return array of all records. */ - def toJSON(symbLog: MemberSymbExLog): Vector[JsValue] = { + def toJSON(symbLog: MemberSymbExLog, config: LogConfig): Vector[JsValue] = { val allRecords = getAllRecords(symbLog.log) - allRecords.map(toJSON).toVector + allRecords.map(toJSON(_, config)).toVector } def getAllRecords(logs: Seq[SymbolicRecord]): Seq[SymbolicRecord] = { @@ -143,13 +143,13 @@ object SymbExLogReportWriter { * @param record The symbolic to translate. * @return The record translated as a JsValue. */ - def toJSON(record: SymbolicRecord): JsValue = { + def toJSON(record: SymbolicRecord, config: LogConfig): JsValue = { var isJoinPoint: Boolean = false var isScopeOpen: Boolean = false var isScopeClose: Boolean = false val isSyntactic: Boolean = false var branches: Option[JsArray] = None - val data: Option[JsObject] = toJSON(record.getData) + val data: Option[JsObject] = toJSON(record.getData(config)) record match { case br: BranchingRecord => branches = Some(JsArray(br.getBranchInfos.map(toJSON))) case _: JoiningRecord => isJoinPoint = true diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index 812aaa0a0..67e8494c4 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -80,7 +80,7 @@ object brancher extends BranchingRules { v.decider.prover.comment(thenBranchComment) v.decider.prover.comment(elseBranchComment) - val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(2, Some(condition), conditionExp) + val uidBranchPoint = v.symbExLog.insertBranchPoint(2, Some(condition), conditionExp) var functionsOfCurrentDecider: immutable.InsertionOrderedSet[FunctionDecl] = null var macrosOfCurrentDecider: Vector[MacroDecl] = null var pcsOfCurrentDecider: PathConditionStack = null @@ -102,8 +102,8 @@ object brancher extends BranchingRules { } (v0: Verifier) => { - SymbExLogger.currentLog().switchToNextBranch(uidBranchPoint) - SymbExLogger.currentLog().markReachable(uidBranchPoint) + v.symbExLog.switchToNextBranch(uidBranchPoint) + v.symbExLog.markReachable(uidBranchPoint) if (v.uniqueId != v0.uniqueId){ /* [BRANCH-PARALLELISATION] */ // executing the else branch on a different verifier, need to adapt the state @@ -154,7 +154,7 @@ object brancher extends BranchingRules { } val res = (if (executeThenBranch) { - SymbExLogger.currentLog().markReachable(uidBranchPoint) + v.symbExLog.markReachable(uidBranchPoint) executionFlowController.locally(s, v)((s1, v1) => { v1.decider.prover.comment(s"[then-branch: $cnt | $condition]") v1.decider.setCurrentBranchCondition(condition, conditionExp) @@ -194,7 +194,7 @@ object brancher extends BranchingRules { rs.head }, alwaysWaitForOther = parallelizeElseBranch) - SymbExLogger.currentLog().endBranchPoint(uidBranchPoint) + v.symbExLog.endBranchPoint(uidBranchPoint) res } } diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index 8997c357c..d9a3e526c 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -158,10 +158,10 @@ object consumer extends ConsumptionRules { val h0 = s0.h /* h0 is h, but potentially consolidated */ val s1 = s0.copy(h = s.h) /* s1 is s, but the retrying flag might be set */ - val sepIdentifier = SymbExLogger.currentLog().openScope(new ConsumeRecord(a, s1, v.decider.pcs)) + val sepIdentifier = v.symbExLog.openScope(new ConsumeRecord(a, s1, v.decider.pcs)) consumeTlc(s1, h0, a, pve, v1)((s2, h2, snap2, v2) => { - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) QS(s2, h2, snap2, v2)}) })(Q) } @@ -186,31 +186,31 @@ object consumer extends ConsumptionRules { val consumed = a match { case imp @ ast.Implies(e0, a0) if !a.isPure => val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume") - val uidImplies = SymbExLogger.currentLog().openScope(impliesRecord) + val uidImplies = v.symbExLog.openScope(impliesRecord) evaluator.eval(s, e0, pve, v)((s1, t0, v1) => branch(s1, t0, Some(e0), v1)( (s2, v2) => consumeR(s2, h, a0, pve, v2)((s3, h1, t1, v3) => { - SymbExLogger.currentLog().closeScope(uidImplies) + v.symbExLog.closeScope(uidImplies) Q(s3, h1, t1, v3) }), (s2, v2) => { - SymbExLogger.currentLog().closeScope(uidImplies) + v.symbExLog.closeScope(uidImplies) Q(s2, h, Unit, v2) })) case ite @ ast.CondExp(e0, a1, a2) if !a.isPure => val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "consume") - val uidCondExp = SymbExLogger.currentLog().openScope(condExpRecord) + val uidCondExp = v.symbExLog.openScope(condExpRecord) eval(s, e0, pve, v)((s1, t0, v1) => branch(s1, t0, Some(e0), v1)( (s2, v2) => consumeR(s2, h, a1, pve, v2)((s3, h1, t1, v3) => { - SymbExLogger.currentLog().closeScope(uidCondExp) + v.symbExLog.closeScope(uidCondExp) Q(s3, h1, t1, v3) }), (s2, v2) => consumeR(s2, h, a2, pve, v2)((s3, h1, t1, v3) => { - SymbExLogger.currentLog().closeScope(uidCondExp) + v.symbExLog.closeScope(uidCondExp) Q(s3, h1, t1, v3) }))) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index d5e950b87..c95364a2f 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -86,9 +86,9 @@ object evaluator extends EvaluationRules { (Q: (State, Term, Verifier) => VerificationResult) : VerificationResult = { - val sepIdentifier = SymbExLogger.currentLog().openScope(new EvaluateRecord(e, s, v.decider.pcs)) + val sepIdentifier = v.symbExLog.openScope(new EvaluateRecord(e, s, v.decider.pcs)) eval3(s, e, pve, v)((s1, t, v1) => { - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) Q(s1, t, v1)}) } @@ -313,16 +313,16 @@ object evaluator extends EvaluationRules { case implies @ ast.Implies(e0, e1) => val impliesRecord = new ImpliesRecord(implies, s, v.decider.pcs, "Implies") - val uidImplies = SymbExLogger.currentLog().openScope(impliesRecord) + val uidImplies = v.symbExLog.openScope(impliesRecord) eval(s, e0, pve, v)((s1, t0, v1) => evalImplies(s1, t0, Some(e0), e1, implies.info == FromShortCircuitingAnd, pve, v1)((s2, t1, v2) => { - SymbExLogger.currentLog().closeScope(uidImplies) + v.symbExLog.closeScope(uidImplies) Q(s2, t1, v2) })) case condExp @ ast.CondExp(e0, e1, e2) => val condExpRecord = new CondExpRecord(condExp, s, v.decider.pcs, "CondExp") - val uidCondExp = SymbExLogger.currentLog().openScope(condExpRecord) + val uidCondExp = v.symbExLog.openScope(condExpRecord) eval(s, e0, pve, v)((s1, t0, v1) => joiner.join[Term, Term](s1, v1)((s2, v2, QB) => brancher.branch(s2, t0, Some(e0), v2)( @@ -340,7 +340,7 @@ object evaluator extends EvaluationRules { sys.error(s"Unexpected join data entries: $entries")} (s2, result) })((s4, t3, v3) => { - SymbExLogger.currentLog().closeScope(uidCondExp) + v.symbExLog.closeScope(uidCondExp) Q(s4, t3, v3) })) @@ -547,7 +547,7 @@ object evaluator extends EvaluationRules { // TODO LA: nonQuantArgs are not recorded yet val impliesRecord = new ImpliesRecord(null, s2, v.decider.pcs, "bindRcvrsAndEvalBody") - val uidImplies = SymbExLogger.currentLog().openScope(impliesRecord) + val uidImplies = v.symbExLog.openScope(impliesRecord) evals(s2, nonQuantArgs, _ => pve, v)((s3, tArgs, v1) => { val argsWithIndex = tArgs zip indices @@ -556,7 +556,7 @@ object evaluator extends EvaluationRules { evalImplies(s3, Ite(argsPairWiseEqual, And(addCons :+ IsPositive(ch.perm)), False()), None,body, false, pve, v1) ((s4, tImplies, v2) => bindRcvrsAndEvalBody(s4, chs.tail, args, tImplies +: ts, v2)((s5, ts1, v3) => { - SymbExLogger.currentLog().closeScope(uidImplies) + v.symbExLog.closeScope(uidImplies) Q(s5, ts1, v3) })) }) @@ -579,7 +579,7 @@ object evaluator extends EvaluationRules { // TODO LA: args are not recorded yet val impliesRecord = new ImpliesRecord(null, s1, v.decider.pcs, "bindQuantRcvrsAndEvalBody") - val uidImplies = SymbExLogger.currentLog().openScope(impliesRecord) + val uidImplies = v.symbExLog.openScope(impliesRecord) evals(s1, args, _ => pve, v)((s2, ts1, v1) => { val bc = IsPositive(ch.perm.replace(ch.quantifiedVars, ts1)) @@ -594,7 +594,7 @@ object evaluator extends EvaluationRules { evalImplies(s2, And(trig, bc), None, body, false, pve, v1)((s3, tImplies, v2) => { val tQuant = Quantification(Forall, tVars, tImplies, tTriggers) bindQuantRcvrsAndEvalBody(s3, chs.tail, args, tQuant +: ts, v2)((s4, ts2, v3) => { - SymbExLogger.currentLog().closeScope(uidImplies) + v.symbExLog.closeScope(uidImplies) Q(s4, ts2, v3) })}) }) diff --git a/src/main/scala/rules/ExecutionFlowController.scala b/src/main/scala/rules/ExecutionFlowController.scala index 9c0df9048..4b1192071 100644 --- a/src/main/scala/rules/ExecutionFlowController.scala +++ b/src/main/scala/rules/ExecutionFlowController.scala @@ -128,9 +128,9 @@ object executionFlowController extends ExecutionFlowRules { val s0 = v.stateConsolidator.consolidate(s, v) val comLog = new CommentRecord("Retry", s0, v.decider.pcs) - val sepIdentifier = SymbExLogger.currentLog().openScope(comLog) + val sepIdentifier = v.symbExLog.openScope(comLog) action(s0.copy(retrying = true, retryLevel = s.retryLevel), v, (s1, r, v1) => { - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) Q(s1.copy(retrying = false), r, v1) }) } diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index fd08cb20e..d422ec092 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -67,7 +67,7 @@ object executor extends ExecutionRules { edge match { case ce: cfg.ConditionalEdge[ast.Stmt, ast.Exp] => val condEdgeRecord = new ConditionalEdgeRecord(ce.condition, s, v.decider.pcs) - val sepIdentifier = SymbExLogger.currentLog().openScope(condEdgeRecord) + val sepIdentifier = v.symbExLog.openScope(condEdgeRecord) val s1 = handleOutEdge(s, edge, v) eval(s1, ce.condition, IfFailed(ce.condition), v)((s2, tCond, v1) => /* Using branch(...) here ensures that the edge condition is recorded @@ -76,11 +76,11 @@ object executor extends ExecutionRules { brancher.branch(s2, tCond, Some(ce.condition), v1)( (s3, v3) => exec(s3, ce.target, ce.kind, v3)((s4, v4) => { - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) Q(s4, v4) }), (_, _) => { - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) Success() })) @@ -106,32 +106,32 @@ object executor extends ExecutionRules { case Seq(thenEdge@ConditionalEdge(cond1, _, _, Kind.Normal), elseEdge@ConditionalEdge(cond2, _, _, Kind.Normal)) if Verifier.config.parallelizeBranches() && cond2 == ast.Not(cond1)() => val condEdgeRecord = new ConditionalEdgeRecord(thenEdge.condition, s, v.decider.pcs) - val sepIdentifier = SymbExLogger.currentLog().openScope(condEdgeRecord) + val sepIdentifier = v.symbExLog.openScope(condEdgeRecord) val res = eval(s, thenEdge.condition, IfFailed(thenEdge.condition), v)((s2, tCond, v1) => brancher.branch(s2, tCond, Some(thenEdge.condition), v1)( (s3, v3) => exec(s3, thenEdge.target, thenEdge.kind, v3)((s4, v4) => { - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) val branchRes = Q(s4, v4) branchRes }), (s3, v3) => exec(s3, elseEdge.target, elseEdge.kind, v3)((s4, v4) => { - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) Q(s4, v4) }))) res case _ => - val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(edges.length) + val uidBranchPoint = v.symbExLog.insertBranchPoint(edges.length) val res = edges.zipWithIndex.foldLeft(Success(): VerificationResult) { case (result: VerificationResult, (edge, edgeIndex)) => if (edgeIndex != 0) { - SymbExLogger.currentLog().switchToNextBranch(uidBranchPoint) + v.symbExLog.switchToNextBranch(uidBranchPoint) } - SymbExLogger.currentLog().markReachable(uidBranchPoint) + v.symbExLog.markReachable(uidBranchPoint) result combine follow(s, edge, v)(Q) } - SymbExLogger.currentLog().endBranchPoint(uidBranchPoint) + v.symbExLog.endBranchPoint(uidBranchPoint) res } } @@ -250,9 +250,9 @@ object executor extends ExecutionRules { def exec(s: State, stmt: ast.Stmt, v: Verifier) (Q: (State, Verifier) => VerificationResult) : VerificationResult = { - val sepIdentifier = SymbExLogger.currentLog().openScope(new ExecuteRecord(stmt, s, v.decider.pcs)) + val sepIdentifier = v.symbExLog.openScope(new ExecuteRecord(stmt, s, v.decider.pcs)) exec2(s, stmt, v)((s1, v1) => { - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) Q(s1, v1)}) } @@ -468,7 +468,7 @@ object executor extends ExecutionRules { val pveCall = CallFailed(call).withReasonNodeTransformed(reasonTransformer) val mcLog = new MethodCallRecord(call, s, v.decider.pcs) - val currentLog = SymbExLogger.currentLog() + val currentLog = v.symbExLog val sepIdentifier = currentLog.openScope(mcLog) val paramLog = new CommentRecord("Parameters", s, v.decider.pcs) val paramId = currentLog.openScope(paramLog) diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala index 4d0344448..f6fbba0e6 100644 --- a/src/main/scala/rules/Joiner.scala +++ b/src/main/scala/rules/Joiner.scala @@ -33,7 +33,7 @@ object joiner extends JoiningRules { var entries: Seq[JoinDataEntry[D]] = Vector.empty val joiningRecord = new JoiningRecord(s, v.decider.pcs) - val uidJoin = SymbExLogger.currentLog().openScope(joiningRecord) + val uidJoin = v.symbExLog.openScope(joiningRecord) executionFlowController.locally(s, v)((s1, v1) => { val preMark = v1.decider.setPathConditionMark() @@ -54,7 +54,7 @@ object joiner extends JoiningRules { Success() }) }) combine { - SymbExLogger.currentLog().closeScope(uidJoin) + v.symbExLog.closeScope(uidJoin) if (entries.isEmpty) { /* No block data was collected, which we interpret as all branches through * the block being infeasible. In turn, we assume that the overall verification path diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index 50a1c3f25..fc6f0aead 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -255,7 +255,7 @@ object moreCompleteExhaleSupporter extends SymbolicExecutionRules { val pTaken = App(pTakenMacro, pTakenArgs) currentFunctionRecorder = currentFunctionRecorder.recordFreshMacro(pTakenDecl) - SymbExLogger.currentLog().addMacro(pTaken, pTakenBody) + v.symbExLog.addMacro(pTaken, pTakenBody) val newChunk = ch.withPerm(PermMinus(ch.perm, pTaken)) pNeeded = PermMinus(pNeeded, pTaken) diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index 7872c3c4e..bb191f7c7 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -185,9 +185,9 @@ object producer extends ProductionRules { (Q: (State, Verifier) => VerificationResult) : VerificationResult = { - val sepIdentifier = SymbExLogger.currentLog().openScope(new ProduceRecord(a, s, v.decider.pcs)) + val sepIdentifier = v.symbExLog.openScope(new ProduceRecord(a, s, v.decider.pcs)) produceTlc(s, sf, a, pve, v)((s1, v1) => { - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) Q(s1, v1)}) } @@ -208,12 +208,12 @@ object producer extends ProductionRules { val produced = a match { case imp @ ast.Implies(e0, a0) if !a.isPure => val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "produce") - val uidImplies = SymbExLogger.currentLog().openScope(impliesRecord) + val uidImplies = v.symbExLog.openScope(impliesRecord) eval(s, e0, pve, v)((s1, t0, v1) => branch(s1, t0, Some(e0), v1)( (s2, v2) => produceR(s2, sf, a0, pve, v2)((s3, v3) => { - SymbExLogger.currentLog().closeScope(uidImplies) + v.symbExLog.closeScope(uidImplies) Q(s3, v3) }), (s2, v2) => { @@ -222,22 +222,22 @@ object producer extends ProductionRules { * otherwise. In order words, only make this assumption if `sf` has * already been used, e.g. in a snapshot equality such as `s0 == (s1, s2)`. */ - SymbExLogger.currentLog().closeScope(uidImplies) + v.symbExLog.closeScope(uidImplies) Q(s2, v2) })) case ite @ ast.CondExp(e0, a1, a2) if !a.isPure => val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "produce") - val uidCondExp = SymbExLogger.currentLog().openScope(condExpRecord) + val uidCondExp = v.symbExLog.openScope(condExpRecord) eval(s, e0, pve, v)((s1, t0, v1) => branch(s1, t0, Some(e0), v1)( (s2, v2) => produceR(s2, sf, a1, pve, v2)((s3, v3) => { - SymbExLogger.currentLog().closeScope(uidCondExp) + v.symbExLog.closeScope(uidCondExp) Q(s3, v3) }), (s2, v2) => produceR(s2, sf, a2, pve, v2)((s3, v3) => { - SymbExLogger.currentLog().closeScope(uidCondExp) + v.symbExLog.closeScope(uidCondExp) Q(s3, v3) }))) diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 415578e0a..28e575f42 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -1310,7 +1310,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { : (ConsumptionResult, State, Seq[QuantifiedBasicChunk]) = { val rmPermRecord = new CommentRecord("removePermissions", s, v.decider.pcs) - val sepIdentifier = SymbExLogger.currentLog().openScope(rmPermRecord) + val sepIdentifier = v.symbExLog.openScope(rmPermRecord) val requiredId = ChunkIdentifier(resource, s.program) assert( @@ -1341,7 +1341,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { val permsTaken = App(permsTakenMacro, permsTakenArgs) currentFunctionRecorder = currentFunctionRecorder.recordFreshMacro(permsTakenDecl) - SymbExLogger.currentLog().addMacro(permsTaken, permsTakenBody) + v.symbExLog.addMacro(permsTaken, permsTakenBody) permsNeeded = PermMinus(permsNeeded, permsTaken) @@ -1402,7 +1402,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport { success v.decider.prover.comment("Done removing quantified permissions") - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) (success, s.copy(functionRecorder = currentFunctionRecorder), remainingChunks) } diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index fdcb273f1..6412f0ff8 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -57,7 +57,7 @@ class MinimalStateConsolidator extends StateConsolidationRules { class DefaultStateConsolidator(protected val config: Config) extends StateConsolidationRules { def consolidate(s: State, v: Verifier): State = { val comLog = new CommentRecord("state consolidation", s, v.decider.pcs) - val sepIdentifier = SymbExLogger.currentLog().openScope(comLog) + val sepIdentifier = v.symbExLog.openScope(comLog) v.decider.prover.comment("[state consolidation]") v.decider.prover.saturate(config.proverSaturationTimeouts.beforeIteration) @@ -77,7 +77,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol var fixedPointRound: Int = 0 do { val roundLog = new CommentRecord("Round " + fixedPointRound, s, v.decider.pcs) - val roundSepIdentifier = SymbExLogger.currentLog().openScope(roundLog) + val roundSepIdentifier = v.symbExLog.openScope(roundLog) val (_functionRecorder, _mergedChunks, _, snapEqs) = singleMerge(functionRecorder, destChunks, newChunks, v) @@ -89,7 +89,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol newChunks = mergedChunks continue = snapEqs.nonEmpty - SymbExLogger.currentLog().closeScope(roundSepIdentifier) + v.symbExLog.closeScope(roundSepIdentifier) fixedPointRound = fixedPointRound + 1 } while (continue) @@ -105,7 +105,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol v.decider.assume(interpreter.buildPathConditionsForResource(id, desc.delayedProperties)) } - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) (functionRecorder, hs :+ Heap(allChunks)) } @@ -128,7 +128,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol def merge(fr1: FunctionRecorder, h: Heap, newH: Heap, v: Verifier): (FunctionRecorder, Heap) = { val mergeLog = new CommentRecord("Merge", null, v.decider.pcs) - val sepIdentifier = SymbExLogger.currentLog().openScope(mergeLog) + val sepIdentifier = v.symbExLog.openScope(mergeLog) val (nonQuantifiedChunks, otherChunks) = partition(h) val (newNonQuantifiedChunks, newOtherChunk) = partition(newH) val (fr2, mergedChunks, newlyAddedChunks, snapEqs) = singleMerge(fr1, nonQuantifiedChunks, newNonQuantifiedChunks, v) @@ -141,7 +141,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol v.decider.assume(interpreter.buildPathConditionsForChunk(ch, resource.instanceProperties)) } - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) (fr2, Heap(mergedChunks ++ otherChunks ++ newOtherChunk)) } @@ -155,7 +155,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol InsertionOrderedSet[Term]) = { val mergeLog = new SingleMergeRecord(destChunks, newChunks, v.decider.pcs) - val sepIdentifier = SymbExLogger.currentLog().openScope(mergeLog) + val sepIdentifier = v.symbExLog.openScope(mergeLog) // bookkeeper.heapMergeIterations += 1 val initial = (fr, destChunks, Seq[NonQuantifiedChunk](), InsertionOrderedSet[Term]()) @@ -180,7 +180,7 @@ class DefaultStateConsolidator(protected val config: Config) extends StateConsol (fr1, nextChunk +: accMergedChunks, nextChunk +: accNewChunks, accSnapEqs) } } - SymbExLogger.currentLog().closeScope(sepIdentifier) + v.symbExLog.closeScope(sepIdentifier) result } diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index 5a9149f07..d2feb4d06 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -45,7 +45,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif logger.debug("\n\n" + "-" * 10 + " METHOD " + method.name + "-" * 10 + "\n") decider.prover.comment("%s %s %s".format("-" * 10, method.name, "-" * 10)) - SymbExLogger.openMemberScope(method, null, v.decider.pcs) + openSymbExLogger(method) val pres = method.pres val posts = method.posts @@ -84,9 +84,9 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif ( executionFlowController.locally(s2a, v2)((s3, v3) => { val s4 = s3.copy(h = Heap()) val impLog = new WellformednessCheckRecord(posts, s, v.decider.pcs) - val sepIdentifier = SymbExLogger.currentLog().openScope(impLog) + val sepIdentifier = symbExLog.openScope(impLog) produces(s4, freshSnap, posts, ContractNotWellformed, v3)((_, _) => { - SymbExLogger.currentLog().closeScope(sepIdentifier) + symbExLog.closeScope(sepIdentifier) Success()})}) && { executionFlowController.locally(s2a, v2)((s3, v3) => { @@ -94,7 +94,7 @@ trait DefaultMethodVerificationUnitProvider extends VerifierComponent { v: Verif consumes(s4, posts, postViolated, v4)((_, _, _) => Success()))}) } )})}) - SymbExLogger.closeMemberScope() + symbExLog.closeMemberScope() Seq(result) } diff --git a/src/main/scala/supporters/PredicateVerificationUnit.scala b/src/main/scala/supporters/PredicateVerificationUnit.scala index 7db3a727f..a8714079b 100644 --- a/src/main/scala/supporters/PredicateVerificationUnit.scala +++ b/src/main/scala/supporters/PredicateVerificationUnit.scala @@ -85,7 +85,7 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve logger.debug("\n\n" + "-" * 10 + " PREDICATE " + predicate.name + "-" * 10 + "\n") decider.prover.comment("%s %s %s".format("-" * 10, predicate.name, "-" * 10)) - SymbExLogger.openMemberScope(predicate, null, v.decider.pcs) + openSymbExLogger(predicate) val ins = predicate.formalArgs.map(_.localVar) val s = sInit.copy(g = Store(ins.map(x => (x, decider.fresh(x)))), @@ -104,7 +104,7 @@ trait DefaultPredicateVerificationUnitProvider extends VerifierComponent { v: Ve Success())}) } - SymbExLogger.closeMemberScope() + symbExLog.closeMemberScope() Seq(result) } diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala index bc49b1c70..7056f6d27 100644 --- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala +++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala @@ -147,14 +147,14 @@ trait DefaultFunctionVerificationUnitProvider extends VerifierComponent { v: Ver logger.debug(s"\n\n$comment\n") decider.prover.comment(comment) - SymbExLogger.openMemberScope(function, null, v.decider.pcs) + openSymbExLogger(function) val data = functionData(function) data.formalArgs.values foreach (v => decider.prover.declare(ConstDecl(v))) decider.prover.declare(ConstDecl(data.formalResult)) val res = Seq(handleFunction(sInit, function)) - SymbExLogger.closeMemberScope() + symbExLog.closeMemberScope() res } diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 4a69ddcd6..1fdb0144d 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -272,7 +272,7 @@ class DefaultMainVerifier(config: Config, if (config.ideModeAdvanced()) { reporter report ExecutionTraceReport( - SymbExLogger.memberList.toIndexedSeq, + rootSymbExLogger.logs.toIndexedSeq, this.axiomsAfterAnalysis().toList, this.postConditionAxioms().toList) } From 4aadffec7a67e4e409337add1eb7966c3e1730ab Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Thu, 17 Nov 2022 17:17:38 +0100 Subject: [PATCH 09/31] some bugs: - do not use newEntityLogger directly, because it's not inserted in the members of the root log - synchronize on the log instead of the map, because I'm using a var instead of mutable.Map - delay opening the member scope to avoid using early initializers --- src/main/scala/logger/SymbExLogger.scala | 25 ++++++++++++------- .../scala/verifier/DefaultMainVerifier.scala | 2 +- src/main/scala/verifier/WorkerVerifier.scala | 2 +- 3 files changed, 18 insertions(+), 11 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index c0926e7dd..ef9b07326 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -215,7 +215,7 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { protected var members: immutable.Map[ast.Member, Log] = Map.empty protected val uidCounter: AtomicInteger = new AtomicInteger(0) - def newEntityLogger(member: ast.Member, s: State, pcs: PathConditionStack): Log + protected def newEntityLogger(member: ast.Member, s: State, pcs: PathConditionStack): Log def config: LogConfig def freshUid(): Int = uidCounter.getAndIncrement() @@ -234,13 +234,20 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { */ @elidable(INFO) def openMemberScope(member: ast.Member, s: State, pcs: PathConditionStack): Log = { - val log = newEntityLogger(member, s, pcs) + try { + val log = newEntityLogger(member, s, pcs) - members.synchronized { - members += member -> log - } + synchronized { + members += member -> log + } - log + log.openMemberScope() + log + } catch { + case anything: Throwable => + println(anything) + throw anything + } } } @@ -302,7 +309,9 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], case _ => ??? } - openScope(main) + def openMemberScope(): Unit = { + openScope(main) + } /** * Inserts the record as well as a corresponding open scope record into the log @@ -468,8 +477,6 @@ class MemberSymbExLog(rootLog: SymbExLogger[MemberSymbExLog], member: ast.Member, state: State, pcs: PathConditionStack) extends MemberSymbExLogger(rootLog, member, state, pcs) { - def close(): Unit = ??? // clear from log, add close record? - /** top level log entries for this member; these log entries were recorded consecutively without branching; * in case branching occured, one of these records is a BranchingRecord with all branches as field attached to it */ var log: Vector[SymbolicRecord] = Vector[SymbolicRecord]() diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 1fdb0144d..30b4fcf57 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -58,7 +58,7 @@ class DefaultMainVerifier(config: Config, def nextUniqueVerifierId(): String = f"${uniqueIdCounter.next()}%02d" override def openSymbExLogger(member: Member): Unit = { - symbExLog = rootSymbExLogger.newEntityLogger(member, null, decider.pcs) + symbExLog = rootSymbExLogger.openMemberScope(member, null, decider.pcs) } protected val preambleReader = new SMTLib2PreambleReader diff --git a/src/main/scala/verifier/WorkerVerifier.scala b/src/main/scala/verifier/WorkerVerifier.scala index 265957317..78c2ec68b 100644 --- a/src/main/scala/verifier/WorkerVerifier.scala +++ b/src/main/scala/verifier/WorkerVerifier.scala @@ -26,7 +26,7 @@ class WorkerVerifier(mainVerifier: MainVerifier, def verificationPoolManager: VerificationPoolManager = mainVerifier.verificationPoolManager override def openSymbExLogger(member: Member): Unit = { - symbExLog = mainVerifier.rootSymbExLogger.newEntityLogger(member, null, decider.pcs) + symbExLog = mainVerifier.rootSymbExLogger.openMemberScope(member, null, decider.pcs) } /* Lifetime */ From aa574464347a72eafdac6315e3ffc11e1bba7d2f Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Thu, 17 Nov 2022 17:25:30 +0100 Subject: [PATCH 10/31] address comment --- src/main/scala/logger/LogConfig.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/scala/logger/LogConfig.scala b/src/main/scala/logger/LogConfig.scala index dd7d635e6..46d55da51 100644 --- a/src/main/scala/logger/LogConfig.scala +++ b/src/main/scala/logger/LogConfig.scala @@ -17,7 +17,7 @@ case class LogConfig(isBlackList: Boolean, if (rc.kind.equals(d.toTypeString)) { rc.value match { case Some(value) => if (value.equals(d.toSimpleString)) return Some(rc) - case _ => return Some(rc) + case None => return Some(rc) } } } From 05caac577d65764cfb362179f977746061a8d93b Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Thu, 17 Nov 2022 17:59:33 +0100 Subject: [PATCH 11/31] make NoopLog do nothing --- src/main/scala/logger/SymbExLogger.scala | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index ef9b07326..1857a2e35 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -302,14 +302,16 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], // Maps macros to their body private var _macros = Map[App, Term]() - val main: MemberRecord = member match { - case m: ast.Method => new MethodRecord(m, state, pcs) - case p: ast.Predicate => new PredicateRecord(p, state, pcs) - case f: ast.Function => new FunctionRecord(f, state, pcs) - case _ => ??? - } + var main: MemberRecord = _ def openMemberScope(): Unit = { + main = member match { + case m: ast.Method => new MethodRecord(m, state, pcs) + case p: ast.Predicate => new PredicateRecord(p, state, pcs) + case f: ast.Function => new FunctionRecord(f, state, pcs) + case _ => ??? + } + openScope(main) } @@ -471,6 +473,15 @@ case object NoopMemberSymbExLog extends MemberSymbExLogger(null, null, null, nul override def markBranchReachable(uidBranchPoint: Int): Unit = {} override def switchToNextBranch(uidBranchPoint: Int): Unit = {} override def endBranchPoint(uidBranchPoint: Int): Unit = {} + + override def openMemberScope(): Unit = {} + override def openScope(s: DataRecord): Int = 0 + override def insertBranchPoint(possibleBranchesCount: Int, condition: Option[Term] = None, conditionExp: Option[Exp] = None): Int = 0 + override def markReachable(uidBranchPoint: Int): Unit = {} + override def closeScope(n: Int): Unit = {} + override def closeMemberScope(): Unit = {} + override def setSMTQuery(query: Term): Unit = {} + override def discardSMTQuery(): Unit = {} } class MemberSymbExLog(rootLog: SymbExLogger[MemberSymbExLog], From 19f9a371d9dc6f26f28c7953b87ca56cc73ccad2 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Thu, 17 Nov 2022 18:06:49 +0100 Subject: [PATCH 12/31] also do nothing on whenEnabled for NoopLog --- src/main/scala/logger/SymbExLogger.scala | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index 1857a2e35..f8bca20d3 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -474,6 +474,8 @@ case object NoopMemberSymbExLog extends MemberSymbExLogger(null, null, null, nul override def switchToNextBranch(uidBranchPoint: Int): Unit = {} override def endBranchPoint(uidBranchPoint: Int): Unit = {} + override def whenEnabled(f: => Unit): Unit = {} + override def openMemberScope(): Unit = {} override def openScope(s: DataRecord): Int = 0 override def insertBranchPoint(possibleBranchesCount: Int, condition: Option[Term] = None, conditionExp: Option[Exp] = None): Int = 0 From 11037a564f4e11fba108e8860d5cd120a6e27c63 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Fri, 18 Nov 2022 10:19:10 +0100 Subject: [PATCH 13/31] symbexlogs can be closed: they do not accept further records (now unrelated to closeMemberScope) --- src/main/scala/logger/SymbExLogger.scala | 69 ++++++++++++++++-------- src/test/scala/SymbExLoggerTests.scala | 11 ++-- 2 files changed, 53 insertions(+), 27 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index f8bca20d3..1e681de61 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -213,6 +213,8 @@ case object SymbExLogger { abstract class SymbExLogger[Log <: MemberSymbExLogger]() { /** Collection of logged Method/Predicates/Functions. */ protected var members: immutable.Map[ast.Member, Log] = Map.empty + protected var closed: Boolean = false + def isClosed: Boolean = closed protected val uidCounter: AtomicInteger = new AtomicInteger(0) protected def newEntityLogger(member: ast.Member, s: State, pcs: PathConditionStack): Log @@ -238,7 +240,13 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { val log = newEntityLogger(member, s, pcs) synchronized { - members += member -> log + if(closed) { + // If we time out and close the log, but somehow manage to race to move on to a new member in time, the log is + // closed so the records are not vacuously recorded, and the log is not added to the map of logs. + log.close() + } else { + members += member -> log + } } log.openMemberScope() @@ -279,20 +287,21 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], val member: ast.Member, val state: State, val pcs: PathConditionStack) { - def appendDataRecord(r: DataRecord): Unit - def appendScopingRecord(r: ScopingRecord, ignoreBranchingStack: Boolean = false): Unit - def appendBranchingRecord(r: BranchingRecord): Unit + protected def appendDataRecord(r: DataRecord): Unit + protected def appendScopingRecord(r: ScopingRecord, ignoreBranchingStack: Boolean = false): Unit + protected def appendBranchingRecord(r: BranchingRecord): Unit - def switchToNextBranch(uidBranchPoint: Int): Unit - def markBranchReachable(uidBranchPoint: Int): Unit - def endBranchPoint(uidBranchPoint: Int): Unit + protected def doSwitchToNextBranch(uidBranchPoint: Int): Unit + protected def markBranchReachable(uidBranchPoint: Int): Unit + protected def doEndBranchPoint(uidBranchPoint: Int): Unit def whenEnabled(f: => Unit): Unit = log.whenEnabled(f) /** * indicates whether this member's close was already closed */ - private var isClosed: Boolean = false + private var closed: Boolean = false + def isClosed: Boolean = closed /** * Most recent output of (get-info :all-statistics) from the underlying prover @@ -302,6 +311,16 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], // Maps macros to their body private var _macros = Map[App, Term]() + def close(): Unit = + synchronized { + closed = true + } + + def whenOpen(f: => Unit): Unit = + synchronized { + if(!isClosed) f else () + } + var main: MemberRecord = _ def openMemberScope(): Unit = { @@ -324,7 +343,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], @elidable(INFO) def openScope(s: DataRecord): Int = { s.id = log.freshUid() - appendDataRecord(s) + whenOpen { appendDataRecord(s) } insert(new OpenScopeRecord(s)) s.id } @@ -340,7 +359,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], private def insert(s: ScopingRecord, ignoreBranchingStack: Boolean = false): Int = { s.id = log.freshUid() s.timeMs = System.currentTimeMillis() - appendScopingRecord(s, ignoreBranchingStack) + whenOpen { appendScopingRecord(s, ignoreBranchingStack) } s.id } @@ -357,10 +376,15 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], def insertBranchPoint(possibleBranchesCount: Int, condition: Option[Term] = None, conditionExp: Option[Exp] = None): Int = { val branchingRecord = new BranchingRecord(possibleBranchesCount, condition, conditionExp) branchingRecord.id = log.freshUid() - appendBranchingRecord(branchingRecord) + whenOpen { appendBranchingRecord(branchingRecord) } branchingRecord.id } + @elidable(INFO) + def switchToNextBranch(uidBranchPoint: Int): Unit = { + whenEnabled { doSwitchToNextBranch(uidBranchPoint) } + } + /** * Marks the current branch of a specific branch point as being reachable * @@ -368,7 +392,12 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], */ @elidable(INFO) def markReachable(uidBranchPoint: Int): Unit = { - markBranchReachable(uidBranchPoint) + whenEnabled { markBranchReachable(uidBranchPoint) } + } + + @elidable(INFO) + def endBranchPoint(uidBranchPoint: Int): Unit = { + whenEnabled { doEndBranchPoint(uidBranchPoint) } } /** @@ -386,13 +415,9 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], * Ends the scope of the member (i.e. main) by inserting a corresponding close scope record into the log */ def closeMemberScope(): Unit = { - if (isClosed) { - return - } val closeRecord = new CloseScopeRecord(main.id) // always insert this close scope record on the root log instead of at the correct place depending on branching stack: insert(closeRecord, ignoreBranchingStack = true) - isClosed = true } /** Record the last prover query that failed. @@ -436,7 +461,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], case (key, Some(value)) => (key + "-delta", value) case other => sys.error(s"Unexpected result pair $other") } - lastStatistics = lastStatistics ++ currentStatistics + whenEnabled { lastStatistics = lastStatistics ++ currentStatistics } currentStatistics ++ deltaStatistics } @@ -461,7 +486,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], def macros(): Map[App, Term] = _macros @elidable(INFO) - def addMacro(m: App, body: Term): Unit = { + def addMacro(m: App, body: Term): Unit = whenEnabled { _macros = _macros + (m -> body) } } @@ -471,8 +496,8 @@ case object NoopMemberSymbExLog extends MemberSymbExLogger(null, null, null, nul override def appendScopingRecord(r: ScopingRecord, ignoreBranchingStack: Boolean): Unit = {} override def appendBranchingRecord(r: BranchingRecord): Unit = {} override def markBranchReachable(uidBranchPoint: Int): Unit = {} - override def switchToNextBranch(uidBranchPoint: Int): Unit = {} - override def endBranchPoint(uidBranchPoint: Int): Unit = {} + override def doSwitchToNextBranch(uidBranchPoint: Int): Unit = {} + override def doEndBranchPoint(uidBranchPoint: Int): Unit = {} override def whenEnabled(f: => Unit): Unit = {} @@ -541,7 +566,7 @@ class MemberSymbExLog(rootLog: SymbExLogger[MemberSymbExLog], branchingStack +:= r } - override def switchToNextBranch(uidBranchPoint: Int): Unit = { + override def doSwitchToNextBranch(uidBranchPoint: Int): Unit = { assert(branchingStack.nonEmpty) val branchingRecord = branchingStack.head assert(branchingRecord.id == uidBranchPoint) @@ -556,7 +581,7 @@ class MemberSymbExLog(rootLog: SymbExLogger[MemberSymbExLog], branchingRecord.markReachable() } - override def endBranchPoint(uidBranchPoint: Int): Unit = { + override def doEndBranchPoint(uidBranchPoint: Int): Unit = { assert(branchingStack.nonEmpty) val branchingRecord = branchingStack.head assert(branchingRecord.id == uidBranchPoint) diff --git a/src/test/scala/SymbExLoggerTests.scala b/src/test/scala/SymbExLoggerTests.scala index 670d1e035..55e7e100b 100644 --- a/src/test/scala/SymbExLoggerTests.scala +++ b/src/test/scala/SymbExLoggerTests.scala @@ -6,16 +6,17 @@ package viper.silicon.tests -import java.io.File -import java.nio.file.{Files, Path, Paths} -import viper.silicon.logger.{SymbExLog, SymbExLogger} -import viper.silver.testing.{LocatedAnnotation, MissingOutput, SilSuite, UnexpectedOutput} -import viper.silver.verifier.{AbstractError, Verifier, Failure => SilFailure, Success => SilSuccess, VerificationResult => SilVerificationResult} +import viper.silicon.logger.SymbExLog import viper.silicon.{Silicon, SiliconFrontend} import viper.silver.ast import viper.silver.ast.Position import viper.silver.frontend.{DefaultStates, Frontend} import viper.silver.reporter.NoopReporter +import viper.silver.testing.{LocatedAnnotation, MissingOutput, SilSuite, UnexpectedOutput} +import viper.silver.verifier.{AbstractError, Verifier, Failure => SilFailure, Success => SilSuccess, VerificationResult => SilVerificationResult} + +import java.io.File +import java.nio.file.{Files, Path, Paths} class SymbExLoggerTests extends SilSuite { val testDirectories = Seq("symbExLogTests") From e73b8ceedae04979d2398afc79cb528c7ca1dda6 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Fri, 18 Nov 2022 10:26:01 +0100 Subject: [PATCH 14/31] close log on timeout --- src/main/scala/Silicon.scala | 5 ++--- src/main/scala/logger/SymbExLogger.scala | 10 ++++++---- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/main/scala/Silicon.scala b/src/main/scala/Silicon.scala index 7c1c2a006..f62553cd7 100644 --- a/src/main/scala/Silicon.scala +++ b/src/main/scala/Silicon.scala @@ -206,10 +206,9 @@ class Silicon(val reporter: Reporter, private var debugInfo: Seq[(String, Any)] result = Some(condenseToViperResult(failures)) } catch { /* Catch exceptions thrown during verification (errors are not caught) */ case _: TimeoutException => - // verification was interrupted, therefore close the current member's scope: - SymbExLogger.currentLog().closeMemberScope() if (config.ideModeAdvanced()) { - reporter report ExecutionTraceReport(SymbExLogger.memberList.toIndexedSeq, List(), List()) + symbExLog.close() + reporter report ExecutionTraceReport(symbExLog.logs.toSeq, List(), List()) } result = Some(SilFailure(SilTimeoutOccurred(config.timeout(), "second(s)") :: Nil)) case exception: Exception if !config.disableCatchingExceptions() => diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index 1e681de61..d7ac64f43 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -186,9 +186,6 @@ import scala.util.{Failure, Success, Try} */ case object SymbExLogger { - def currentLog(): MemberSymbExLog = ??? - def memberList: Seq[SymbExLog] = ??? - def ofConfig(c: Config): SymbExLogger[_ <: MemberSymbExLogger] = { if(c.ideModeAdvanced()) SymbExLog(parseLogConfig(c)) @@ -240,7 +237,7 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { val log = newEntityLogger(member, s, pcs) synchronized { - if(closed) { + if(isClosed) { // If we time out and close the log, but somehow manage to race to move on to a new member in time, the log is // closed so the records are not vacuously recorded, and the log is not added to the map of logs. log.close() @@ -257,6 +254,11 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { throw anything } } + + def close(): Unit = + synchronized { + members.values.foreach(_.close()) + } } case object NoopSymbExLog extends SymbExLogger[NoopMemberSymbExLog.type] { From 285baec7791aeaf8a348a68e60d470760ae8220c Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Fri, 18 Nov 2022 10:52:31 +0100 Subject: [PATCH 15/31] SymbExLogger.ofConfig makes the silicon slightly less lazy, so invalid options are not silently ignored when doing nothing --- src/test/scala/ConcurrentInstantiationTests.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/test/scala/ConcurrentInstantiationTests.scala b/src/test/scala/ConcurrentInstantiationTests.scala index 90a39fd88..0fc81b812 100644 --- a/src/test/scala/ConcurrentInstantiationTests.scala +++ b/src/test/scala/ConcurrentInstantiationTests.scala @@ -24,7 +24,7 @@ class ConcurrentInstantiationTests extends AnyFunSuite { val tasks: Seq[Future[Unit]] = for (_ <- 1 to numTasks) yield Future { val verifier = new Silicon() - verifier.parseCommandLine(Seq("--logLevel ALL", "dummy-program.sil")) + verifier.parseCommandLine(Seq("--logLevel", "ALL", "dummy-program.sil")) } val aggregated: Future[Seq[Unit]] = Future.sequence(tasks) From d81637283c60119c36a8bbe2be5cf0d1c21cf622 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Fri, 18 Nov 2022 11:13:01 +0100 Subject: [PATCH 16/31] use NoopMemberSymbExLog if there is no log yet (a bug, but better than crashing) disallow use of ideModeAdvanced in the presence of parallelizeBranches --- src/main/scala/Config.scala | 9 +++++++++ src/main/scala/verifier/BaseVerifier.scala | 4 ++-- 2 files changed, 11 insertions(+), 2 deletions(-) diff --git a/src/main/scala/Config.scala b/src/main/scala/Config.scala index e034d9343..9b27bed03 100644 --- a/src/main/scala/Config.scala +++ b/src/main/scala/Config.scala @@ -754,6 +754,15 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") { case _ => Right(()) } + validateOpt(ideModeAdvanced, parallelizeBranches) { + case (Some(false), _) => Right(()) + case (_, Some(false)) => Right(()) + case (Some(true), Some(true)) => + Left(s"Option ${ideModeAdvanced.name} is not supported in combination with ${parallelizeBranches.name}") + case other => + sys.error(s"Unexpected combination: $other") + } + validateOpt(counterexample, enableMoreCompleteExhale) { case (Some(_), Some(false)) => Left( s"Option ${counterexample.name} requires setting " + s"flag ${enableMoreCompleteExhale.name}") diff --git a/src/main/scala/verifier/BaseVerifier.scala b/src/main/scala/verifier/BaseVerifier.scala index 2aa9efb81..a688f1f8c 100644 --- a/src/main/scala/verifier/BaseVerifier.scala +++ b/src/main/scala/verifier/BaseVerifier.scala @@ -12,7 +12,7 @@ import viper.silicon.Config.StateConsolidationMode import viper.silver.components.StatefulComponent import viper.silicon.{utils, _} import viper.silicon.decider.{DefaultDeciderProvider, TermToSMTLib2Converter} -import viper.silicon.logger.MemberSymbExLogger +import viper.silicon.logger.{MemberSymbExLogger, NoopMemberSymbExLog} import viper.silicon.state._ import viper.silicon.state.terms.{AxiomRewriter, TriggerGenerator} import viper.silicon.supporters._ @@ -37,7 +37,7 @@ abstract class BaseVerifier(val config: Config, Logger(LoggerFactory.getLogger(s"${this.getClass.getName}-$uniqueId")) private var currentSymbExLog: Option[_ <: MemberSymbExLogger] = None - override def symbExLog: MemberSymbExLogger = currentSymbExLog.get + override def symbExLog: MemberSymbExLogger = currentSymbExLog.getOrElse(NoopMemberSymbExLog) protected def symbExLog_=(logger: MemberSymbExLogger): Unit = { currentSymbExLog = Some(logger) } private val counters = mutable.Map[AnyRef, Counter]() From f17c120402e3ab5aaaf4e34de9d4f6e27fd9cc96 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Fri, 18 Nov 2022 12:00:40 +0100 Subject: [PATCH 17/31] move config to concrete logger; state is always null, so drop it. --- src/main/scala/logger/SymbExLogger.scala | 35 +++++++++---------- .../logger/records/data/DataRecord.scala | 12 ------- .../logger/records/data/FunctionRecord.scala | 3 +- .../logger/records/data/MethodRecord.scala | 3 +- .../logger/records/data/PredicateRecord.scala | 3 +- .../scala/verifier/DefaultMainVerifier.scala | 2 +- src/main/scala/verifier/WorkerVerifier.scala | 2 +- 7 files changed, 21 insertions(+), 39 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index d7ac64f43..5d4d463ca 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -214,8 +214,7 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { def isClosed: Boolean = closed protected val uidCounter: AtomicInteger = new AtomicInteger(0) - protected def newEntityLogger(member: ast.Member, s: State, pcs: PathConditionStack): Log - def config: LogConfig + protected def newEntityLogger(member: ast.Member, pcs: PathConditionStack): Log def freshUid(): Int = uidCounter.getAndIncrement() @@ -232,9 +231,9 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { * @param pcs Current path conditions. */ @elidable(INFO) - def openMemberScope(member: ast.Member, s: State, pcs: PathConditionStack): Log = { + def openMemberScope(member: ast.Member, pcs: PathConditionStack): Log = { try { - val log = newEntityLogger(member, s, pcs) + val log = newEntityLogger(member, pcs) synchronized { if(isClosed) { @@ -262,19 +261,18 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { } case object NoopSymbExLog extends SymbExLogger[NoopMemberSymbExLog.type] { - override def newEntityLogger(member: Member, s: State, pcs: PathConditionStack): NoopMemberSymbExLog.type = + override def newEntityLogger(member: Member, pcs: PathConditionStack): NoopMemberSymbExLog.type = NoopMemberSymbExLog - override def config: LogConfig = null override def whenEnabled(f: => Unit): Unit = {} - override def openMemberScope(member: Member, s: State, pcs: PathConditionStack): NoopMemberSymbExLog.type = + override def openMemberScope(member: Member, pcs: PathConditionStack): NoopMemberSymbExLog.type = NoopMemberSymbExLog } case class SymbExLog(config: LogConfig) extends SymbExLogger[MemberSymbExLog]() { - override def newEntityLogger(member: ast.Member, s: State, pcs: PathConditionStack): MemberSymbExLog = - new MemberSymbExLog(this, member, s, pcs) + override def newEntityLogger(member: ast.Member, pcs: PathConditionStack): MemberSymbExLog = + new MemberSymbExLog(this, config, member, pcs) /** * Simple string representation of the logs. @@ -287,7 +285,6 @@ case class SymbExLog(config: LogConfig) extends SymbExLogger[MemberSymbExLog]() abstract class MemberSymbExLogger(log: SymbExLogger[_], val member: ast.Member, - val state: State, val pcs: PathConditionStack) { protected def appendDataRecord(r: DataRecord): Unit protected def appendScopingRecord(r: ScopingRecord, ignoreBranchingStack: Boolean = false): Unit @@ -327,9 +324,9 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], def openMemberScope(): Unit = { main = member match { - case m: ast.Method => new MethodRecord(m, state, pcs) - case p: ast.Predicate => new PredicateRecord(p, state, pcs) - case f: ast.Function => new FunctionRecord(f, state, pcs) + case m: ast.Method => new MethodRecord(m, pcs) + case p: ast.Predicate => new PredicateRecord(p, pcs) + case f: ast.Function => new FunctionRecord(f, pcs) case _ => ??? } @@ -493,7 +490,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], } } -case object NoopMemberSymbExLog extends MemberSymbExLogger(null, null, null, null) { +case object NoopMemberSymbExLog extends MemberSymbExLogger(null, null, null) { override def appendDataRecord(r: DataRecord): Unit = {} override def appendScopingRecord(r: ScopingRecord, ignoreBranchingStack: Boolean): Unit = {} override def appendBranchingRecord(r: BranchingRecord): Unit = {} @@ -514,9 +511,9 @@ case object NoopMemberSymbExLog extends MemberSymbExLogger(null, null, null, nul } class MemberSymbExLog(rootLog: SymbExLogger[MemberSymbExLog], + config: LogConfig, member: ast.Member, - state: State, - pcs: PathConditionStack) extends MemberSymbExLogger(rootLog, member, state, pcs) { + pcs: PathConditionStack) extends MemberSymbExLogger(rootLog, member, pcs) { /** top level log entries for this member; these log entries were recorded consecutively without branching; * in case branching occured, one of these records is a BranchingRecord with all branches as field attached to it */ var log: Vector[SymbolicRecord] = Vector[SymbolicRecord]() @@ -541,9 +538,9 @@ class MemberSymbExLog(rootLog: SymbExLogger[MemberSymbExLog], } override def appendDataRecord(r: DataRecord): Unit = { - val shouldIgnore = rootLog.config.getRecordConfig(r) match { - case Some(_) => rootLog.config.isBlackList - case None => !rootLog.config.isBlackList + val shouldIgnore = config.getRecordConfig(r) match { + case Some(_) => config.isBlackList + case None => !config.isBlackList } if (shouldIgnore) { diff --git a/src/main/scala/logger/records/data/DataRecord.scala b/src/main/scala/logger/records/data/DataRecord.scala index bfc2204c4..70ef4dd13 100644 --- a/src/main/scala/logger/records/data/DataRecord.scala +++ b/src/main/scala/logger/records/data/DataRecord.scala @@ -18,7 +18,6 @@ import viper.silver.ast.Positioned trait DataRecord extends SymbolicRecord { val value: ast.Node - val state: State // TODO: It would be nicer to use the PathConditionStack instead of the // Decider's internal representation for the pcs. // However, the recording happens to early such that the wrong @@ -41,17 +40,6 @@ trait DataRecord extends SymbolicRecord { case posValue: ast.Node with Positioned => data.pos = Some(utils.ast.sourceLineColumn(posValue)) case _ => } - if (state != null) { - if (config.includeStore) { - data.store = Some(state.g) - } - if (config.includeHeap) { - data.heap = Some(state.h) - } - if (config.includeOldHeap) { - data.oldHeap = state.oldHeaps.get(Verifier.PRE_STATE_LABEL) - } - } if (pcs != null && config.includePcs) { data.pcs = Some(pcs) } diff --git a/src/main/scala/logger/records/data/FunctionRecord.scala b/src/main/scala/logger/records/data/FunctionRecord.scala index 8dcc8e5ca..a2b6f6066 100644 --- a/src/main/scala/logger/records/data/FunctionRecord.scala +++ b/src/main/scala/logger/records/data/FunctionRecord.scala @@ -12,9 +12,8 @@ import viper.silicon.state.State import viper.silicon.state.terms.Term import viper.silver.ast -class FunctionRecord(v: ast.Function, s: State, p: PathConditionStack) extends MemberRecord { +class FunctionRecord(v: ast.Function, p: PathConditionStack) extends MemberRecord { val value: ast.Function = v - val state: State = s val pcs: InsertionOrderedSet[Term] = if (p != null) p.assumptions else null override val toTypeString: String = "function" diff --git a/src/main/scala/logger/records/data/MethodRecord.scala b/src/main/scala/logger/records/data/MethodRecord.scala index 40169b556..d75c3a7ae 100644 --- a/src/main/scala/logger/records/data/MethodRecord.scala +++ b/src/main/scala/logger/records/data/MethodRecord.scala @@ -12,9 +12,8 @@ import viper.silicon.state._ import viper.silicon.state.terms.Term import viper.silver.ast -class MethodRecord(v: ast.Method, s: State, p: PathConditionStack) extends MemberRecord { +class MethodRecord(v: ast.Method, p: PathConditionStack) extends MemberRecord { val value: ast.Method = v - val state: State = s val pcs: InsertionOrderedSet[Term] = if (p != null) p.assumptions else null override val toTypeString: String = "method" diff --git a/src/main/scala/logger/records/data/PredicateRecord.scala b/src/main/scala/logger/records/data/PredicateRecord.scala index ee41c51b1..de6e016b3 100644 --- a/src/main/scala/logger/records/data/PredicateRecord.scala +++ b/src/main/scala/logger/records/data/PredicateRecord.scala @@ -12,9 +12,8 @@ import viper.silicon.state.State import viper.silicon.state.terms.Term import viper.silver.ast -class PredicateRecord(v: ast.Predicate, s: State, p: PathConditionStack) extends MemberRecord { +class PredicateRecord(v: ast.Predicate, p: PathConditionStack) extends MemberRecord { val value: ast.Predicate = v - val state: State = s val pcs: InsertionOrderedSet[Term] = if (p != null) p.assumptions else null override val toTypeString: String = "predicate" diff --git a/src/main/scala/verifier/DefaultMainVerifier.scala b/src/main/scala/verifier/DefaultMainVerifier.scala index 30b4fcf57..5c21a19dc 100644 --- a/src/main/scala/verifier/DefaultMainVerifier.scala +++ b/src/main/scala/verifier/DefaultMainVerifier.scala @@ -58,7 +58,7 @@ class DefaultMainVerifier(config: Config, def nextUniqueVerifierId(): String = f"${uniqueIdCounter.next()}%02d" override def openSymbExLogger(member: Member): Unit = { - symbExLog = rootSymbExLogger.openMemberScope(member, null, decider.pcs) + symbExLog = rootSymbExLogger.openMemberScope(member, decider.pcs) } protected val preambleReader = new SMTLib2PreambleReader diff --git a/src/main/scala/verifier/WorkerVerifier.scala b/src/main/scala/verifier/WorkerVerifier.scala index 78c2ec68b..cd561517d 100644 --- a/src/main/scala/verifier/WorkerVerifier.scala +++ b/src/main/scala/verifier/WorkerVerifier.scala @@ -26,7 +26,7 @@ class WorkerVerifier(mainVerifier: MainVerifier, def verificationPoolManager: VerificationPoolManager = mainVerifier.verificationPoolManager override def openSymbExLogger(member: Member): Unit = { - symbExLog = mainVerifier.rootSymbExLogger.openMemberScope(member, null, decider.pcs) + symbExLog = mainVerifier.rootSymbExLogger.openMemberScope(member, decider.pcs) } /* Lifetime */ From 4846a2cb7d92ac04b072baf3216dc94b64ba0f90 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Fri, 25 Nov 2022 13:33:12 +0100 Subject: [PATCH 18/31] update silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index 7b30d299f..d978f88eb 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 7b30d299f4a7bbde64696681f71b6a7432cbc9ca +Subproject commit d978f88eb363440390ca3baa62ce56ad3fadc42c From 505c61b1442fa78dcf8748bc1084bcfe0904df8f Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Tue, 29 Nov 2022 13:18:45 +0100 Subject: [PATCH 19/31] change by-name trickery to lambdas --- src/main/scala/decider/Decider.scala | 2 +- src/main/scala/logger/SymbExLogger.scala | 28 ++++++++++++------------ 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 42b458040..14870893d 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -284,7 +284,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => val result = prover.assert(t, timeout) - symbExLog.whenEnabled { + symbExLog.whenEnabled { () => assertRecord.statistics = Some(symbExLog.deltaStatistics(prover.statistics())) } diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index 5d4d463ca..044689757 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -218,7 +218,7 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { def freshUid(): Int = uidCounter.getAndIncrement() - def whenEnabled(f: => Unit): Unit = f + def whenEnabled(f: () => Unit): Unit = f() def logs: Iterable[Log] = members.values @@ -264,7 +264,7 @@ case object NoopSymbExLog extends SymbExLogger[NoopMemberSymbExLog.type] { override def newEntityLogger(member: Member, pcs: PathConditionStack): NoopMemberSymbExLog.type = NoopMemberSymbExLog - override def whenEnabled(f: => Unit): Unit = {} + override def whenEnabled(f: () => Unit): Unit = {} override def openMemberScope(member: Member, pcs: PathConditionStack): NoopMemberSymbExLog.type = NoopMemberSymbExLog @@ -294,7 +294,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], protected def markBranchReachable(uidBranchPoint: Int): Unit protected def doEndBranchPoint(uidBranchPoint: Int): Unit - def whenEnabled(f: => Unit): Unit = log.whenEnabled(f) + def whenEnabled(f: () => Unit): Unit = log.whenEnabled(f) /** * indicates whether this member's close was already closed @@ -315,9 +315,9 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], closed = true } - def whenOpen(f: => Unit): Unit = + def whenOpen(f: () => Unit): Unit = synchronized { - if(!isClosed) f else () + if(!isClosed) f() else () } var main: MemberRecord = _ @@ -342,7 +342,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], @elidable(INFO) def openScope(s: DataRecord): Int = { s.id = log.freshUid() - whenOpen { appendDataRecord(s) } + whenOpen { () => appendDataRecord(s) } insert(new OpenScopeRecord(s)) s.id } @@ -358,7 +358,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], private def insert(s: ScopingRecord, ignoreBranchingStack: Boolean = false): Int = { s.id = log.freshUid() s.timeMs = System.currentTimeMillis() - whenOpen { appendScopingRecord(s, ignoreBranchingStack) } + whenOpen { () => appendScopingRecord(s, ignoreBranchingStack) } s.id } @@ -375,13 +375,13 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], def insertBranchPoint(possibleBranchesCount: Int, condition: Option[Term] = None, conditionExp: Option[Exp] = None): Int = { val branchingRecord = new BranchingRecord(possibleBranchesCount, condition, conditionExp) branchingRecord.id = log.freshUid() - whenOpen { appendBranchingRecord(branchingRecord) } + whenOpen { () => appendBranchingRecord(branchingRecord) } branchingRecord.id } @elidable(INFO) def switchToNextBranch(uidBranchPoint: Int): Unit = { - whenEnabled { doSwitchToNextBranch(uidBranchPoint) } + whenEnabled { () => doSwitchToNextBranch(uidBranchPoint) } } /** @@ -391,12 +391,12 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], */ @elidable(INFO) def markReachable(uidBranchPoint: Int): Unit = { - whenEnabled { markBranchReachable(uidBranchPoint) } + whenEnabled { () => markBranchReachable(uidBranchPoint) } } @elidable(INFO) def endBranchPoint(uidBranchPoint: Int): Unit = { - whenEnabled { doEndBranchPoint(uidBranchPoint) } + whenEnabled { () => doEndBranchPoint(uidBranchPoint) } } /** @@ -460,7 +460,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], case (key, Some(value)) => (key + "-delta", value) case other => sys.error(s"Unexpected result pair $other") } - whenEnabled { lastStatistics = lastStatistics ++ currentStatistics } + whenEnabled { () => lastStatistics = lastStatistics ++ currentStatistics } currentStatistics ++ deltaStatistics } @@ -485,7 +485,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], def macros(): Map[App, Term] = _macros @elidable(INFO) - def addMacro(m: App, body: Term): Unit = whenEnabled { + def addMacro(m: App, body: Term): Unit = whenEnabled { () => _macros = _macros + (m -> body) } } @@ -498,7 +498,7 @@ case object NoopMemberSymbExLog extends MemberSymbExLogger(null, null, null) { override def doSwitchToNextBranch(uidBranchPoint: Int): Unit = {} override def doEndBranchPoint(uidBranchPoint: Int): Unit = {} - override def whenEnabled(f: => Unit): Unit = {} + override def whenEnabled(f: () => Unit): Unit = {} override def openMemberScope(): Unit = {} override def openScope(s: DataRecord): Int = 0 From a32cc49148b13df75d662b128e543958f3afddd3 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Tue, 29 Nov 2022 14:36:03 +0100 Subject: [PATCH 20/31] remove debug println --- src/main/scala/logger/SymbExLogger.scala | 30 ++++++++++-------------- 1 file changed, 12 insertions(+), 18 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index 044689757..d8ac89889 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -232,26 +232,20 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { */ @elidable(INFO) def openMemberScope(member: ast.Member, pcs: PathConditionStack): Log = { - try { - val log = newEntityLogger(member, pcs) - - synchronized { - if(isClosed) { - // If we time out and close the log, but somehow manage to race to move on to a new member in time, the log is - // closed so the records are not vacuously recorded, and the log is not added to the map of logs. - log.close() - } else { - members += member -> log - } - } + val log = newEntityLogger(member, pcs) - log.openMemberScope() - log - } catch { - case anything: Throwable => - println(anything) - throw anything + synchronized { + if(isClosed) { + // If we time out and close the log, but somehow manage to race to move on to a new member in time, the log is + // closed so the records are not vacuously recorded, and the log is not added to the map of logs. + log.close() + } else { + members += member -> log + } } + + log.openMemberScope() + log } def close(): Unit = From a2daeedcf3e9d782189ee294c72063b037987631 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Tue, 29 Nov 2022 14:53:52 +0100 Subject: [PATCH 21/31] namespace Member --- src/main/scala/verifier/WorkerVerifier.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main/scala/verifier/WorkerVerifier.scala b/src/main/scala/verifier/WorkerVerifier.scala index cd561517d..10140de24 100644 --- a/src/main/scala/verifier/WorkerVerifier.scala +++ b/src/main/scala/verifier/WorkerVerifier.scala @@ -7,7 +7,7 @@ package viper.silicon.verifier import viper.silicon.supporters._ -import viper.silver.ast.Member +import viper.silver.ast import viper.silver.components.StatefulComponent import viper.silver.reporter.Reporter @@ -25,7 +25,7 @@ class WorkerVerifier(mainVerifier: MainVerifier, def verificationPoolManager: VerificationPoolManager = mainVerifier.verificationPoolManager - override def openSymbExLogger(member: Member): Unit = { + override def openSymbExLogger(member: ast.Member): Unit = { symbExLog = mainVerifier.rootSymbExLogger.openMemberScope(member, decider.pcs) } From c060dc1a3f21c82e09c33bbf8879b54e3fb09606 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Tue, 29 Nov 2022 15:03:51 +0100 Subject: [PATCH 22/31] clarify val names for Config vs LogConfig --- src/main/scala/logger/SymbExLogger.scala | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index d8ac89889..6c3b28f71 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -186,15 +186,15 @@ import scala.util.{Failure, Success, Try} */ case object SymbExLogger { - def ofConfig(c: Config): SymbExLogger[_ <: MemberSymbExLogger] = { - if(c.ideModeAdvanced()) - SymbExLog(parseLogConfig(c)) + def ofConfig(config: Config): SymbExLogger[_ <: MemberSymbExLogger] = { + if(config.ideModeAdvanced()) + SymbExLog(parseLogConfig(config)) else NoopSymbExLog } - private def parseLogConfig(c: Config): LogConfig = { - var logConfigPath = Try(c.logConfig()) + private def parseLogConfig(config: Config): LogConfig = { + var logConfigPath = Try(config.logConfig()) logConfigPath = logConfigPath.filter(path => Files.exists(Paths.get(path))) val source = logConfigPath.map(path => scala.io.Source.fromFile(path)) val fileContent = source.map(s => s.getLines().mkString) @@ -264,9 +264,9 @@ case object NoopSymbExLog extends SymbExLogger[NoopMemberSymbExLog.type] { NoopMemberSymbExLog } -case class SymbExLog(config: LogConfig) extends SymbExLogger[MemberSymbExLog]() { +case class SymbExLog(logConfig: LogConfig) extends SymbExLogger[MemberSymbExLog]() { override def newEntityLogger(member: ast.Member, pcs: PathConditionStack): MemberSymbExLog = - new MemberSymbExLog(this, config, member, pcs) + new MemberSymbExLog(this, logConfig, member, pcs) /** * Simple string representation of the logs. @@ -505,7 +505,7 @@ case object NoopMemberSymbExLog extends MemberSymbExLogger(null, null, null) { } class MemberSymbExLog(rootLog: SymbExLogger[MemberSymbExLog], - config: LogConfig, + logConfig: LogConfig, member: ast.Member, pcs: PathConditionStack) extends MemberSymbExLogger(rootLog, member, pcs) { /** top level log entries for this member; these log entries were recorded consecutively without branching; @@ -532,9 +532,9 @@ class MemberSymbExLog(rootLog: SymbExLogger[MemberSymbExLog], } override def appendDataRecord(r: DataRecord): Unit = { - val shouldIgnore = config.getRecordConfig(r) match { - case Some(_) => config.isBlackList - case None => !config.isBlackList + val shouldIgnore = logConfig.getRecordConfig(r) match { + case Some(_) => logConfig.isBlackList + case None => !logConfig.isBlackList } if (shouldIgnore) { From 4b9728e4036a5090c1fd93803b95d736da4cdfa3 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Tue, 29 Nov 2022 15:45:31 +0100 Subject: [PATCH 23/31] Revert "change by-name trickery to lambdas" This reverts commit 505c61b1442fa78dcf8748bc1084bcfe0904df8f. --- src/main/scala/decider/Decider.scala | 2 +- src/main/scala/logger/SymbExLogger.scala | 28 ++++++++++++------------ 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 14870893d..42b458040 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -284,7 +284,7 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier => val result = prover.assert(t, timeout) - symbExLog.whenEnabled { () => + symbExLog.whenEnabled { assertRecord.statistics = Some(symbExLog.deltaStatistics(prover.statistics())) } diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index 6c3b28f71..88f16a0c2 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -218,7 +218,7 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { def freshUid(): Int = uidCounter.getAndIncrement() - def whenEnabled(f: () => Unit): Unit = f() + def whenEnabled(f: => Unit): Unit = f def logs: Iterable[Log] = members.values @@ -258,7 +258,7 @@ case object NoopSymbExLog extends SymbExLogger[NoopMemberSymbExLog.type] { override def newEntityLogger(member: Member, pcs: PathConditionStack): NoopMemberSymbExLog.type = NoopMemberSymbExLog - override def whenEnabled(f: () => Unit): Unit = {} + override def whenEnabled(f: => Unit): Unit = {} override def openMemberScope(member: Member, pcs: PathConditionStack): NoopMemberSymbExLog.type = NoopMemberSymbExLog @@ -288,7 +288,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], protected def markBranchReachable(uidBranchPoint: Int): Unit protected def doEndBranchPoint(uidBranchPoint: Int): Unit - def whenEnabled(f: () => Unit): Unit = log.whenEnabled(f) + def whenEnabled(f: => Unit): Unit = log.whenEnabled(f) /** * indicates whether this member's close was already closed @@ -309,9 +309,9 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], closed = true } - def whenOpen(f: () => Unit): Unit = + def whenOpen(f: => Unit): Unit = synchronized { - if(!isClosed) f() else () + if(!isClosed) f else () } var main: MemberRecord = _ @@ -336,7 +336,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], @elidable(INFO) def openScope(s: DataRecord): Int = { s.id = log.freshUid() - whenOpen { () => appendDataRecord(s) } + whenOpen { appendDataRecord(s) } insert(new OpenScopeRecord(s)) s.id } @@ -352,7 +352,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], private def insert(s: ScopingRecord, ignoreBranchingStack: Boolean = false): Int = { s.id = log.freshUid() s.timeMs = System.currentTimeMillis() - whenOpen { () => appendScopingRecord(s, ignoreBranchingStack) } + whenOpen { appendScopingRecord(s, ignoreBranchingStack) } s.id } @@ -369,13 +369,13 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], def insertBranchPoint(possibleBranchesCount: Int, condition: Option[Term] = None, conditionExp: Option[Exp] = None): Int = { val branchingRecord = new BranchingRecord(possibleBranchesCount, condition, conditionExp) branchingRecord.id = log.freshUid() - whenOpen { () => appendBranchingRecord(branchingRecord) } + whenOpen { appendBranchingRecord(branchingRecord) } branchingRecord.id } @elidable(INFO) def switchToNextBranch(uidBranchPoint: Int): Unit = { - whenEnabled { () => doSwitchToNextBranch(uidBranchPoint) } + whenEnabled { doSwitchToNextBranch(uidBranchPoint) } } /** @@ -385,12 +385,12 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], */ @elidable(INFO) def markReachable(uidBranchPoint: Int): Unit = { - whenEnabled { () => markBranchReachable(uidBranchPoint) } + whenEnabled { markBranchReachable(uidBranchPoint) } } @elidable(INFO) def endBranchPoint(uidBranchPoint: Int): Unit = { - whenEnabled { () => doEndBranchPoint(uidBranchPoint) } + whenEnabled { doEndBranchPoint(uidBranchPoint) } } /** @@ -454,7 +454,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], case (key, Some(value)) => (key + "-delta", value) case other => sys.error(s"Unexpected result pair $other") } - whenEnabled { () => lastStatistics = lastStatistics ++ currentStatistics } + whenEnabled { lastStatistics = lastStatistics ++ currentStatistics } currentStatistics ++ deltaStatistics } @@ -479,7 +479,7 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], def macros(): Map[App, Term] = _macros @elidable(INFO) - def addMacro(m: App, body: Term): Unit = whenEnabled { () => + def addMacro(m: App, body: Term): Unit = whenEnabled { _macros = _macros + (m -> body) } } @@ -492,7 +492,7 @@ case object NoopMemberSymbExLog extends MemberSymbExLogger(null, null, null) { override def doSwitchToNextBranch(uidBranchPoint: Int): Unit = {} override def doEndBranchPoint(uidBranchPoint: Int): Unit = {} - override def whenEnabled(f: () => Unit): Unit = {} + override def whenEnabled(f: => Unit): Unit = {} override def openMemberScope(): Unit = {} override def openScope(s: DataRecord): Int = 0 From 6951369940bcc4419c3f324a29438529ec34a69e Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 30 Nov 2022 11:05:20 +0100 Subject: [PATCH 24/31] validateFileOpt already checks whether the file exists --- src/main/scala/logger/SymbExLogger.scala | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index 88f16a0c2..66d8eb400 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -194,8 +194,7 @@ case object SymbExLogger { } private def parseLogConfig(config: Config): LogConfig = { - var logConfigPath = Try(config.logConfig()) - logConfigPath = logConfigPath.filter(path => Files.exists(Paths.get(path))) + val logConfigPath = Try(config.logConfig()) val source = logConfigPath.map(path => scala.io.Source.fromFile(path)) val fileContent = source.map(s => s.getLines().mkString) val jsonAst = fileContent.flatMap(content => Try(content.parseJson)) From 0939b02e809dd318652648f20a2a2b9a40c47260 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 30 Nov 2022 11:27:51 +0100 Subject: [PATCH 25/31] log a warning when the symbexlog config cannot be parsed --- src/main/scala/logger/SymbExLogger.scala | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index 66d8eb400..465ba8ae1 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -6,6 +6,7 @@ package viper.silicon.logger +import org.slf4j.LoggerFactory import spray.json._ import viper.silicon.decider.PathConditionStack import viper.silicon.logger.LogConfigProtocol._ @@ -193,15 +194,21 @@ case object SymbExLogger { NoopSymbExLog } + private lazy val textLogger = LoggerFactory.getLogger(classOf[SymbExLogger[_]]) + private def parseLogConfig(config: Config): LogConfig = { - val logConfigPath = Try(config.logConfig()) - val source = logConfigPath.map(path => scala.io.Source.fromFile(path)) + val logConfigPath = config.logConfig.getOrElse(return LogConfig.default()) + val source = Success(logConfigPath).map(path => scala.io.Source.fromFile(path)) val fileContent = source.map(s => s.getLines().mkString) val jsonAst = fileContent.flatMap(content => Try(content.parseJson)) val logConfig = jsonAst.flatMap(ast => Try(ast.convertTo[LogConfig])) logConfig match { case Success(convertedConfig) => convertedConfig - case Failure(_) => LogConfig.default() + case Failure(err) => + textLogger.warn( + s"Could not parse the configuration for the symbolic execution logger at $logConfigPath: " + + s"${err.getMessage} The default configuration will be used instead.") + LogConfig.default() } } } From 2edf5a8da75db33301ce0d410a553eefa9ff529e Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 30 Nov 2022 11:46:56 +0100 Subject: [PATCH 26/31] no delta for values not yet encountered --- src/main/scala/logger/SymbExLogger.scala | 20 +++++--------------- 1 file changed, 5 insertions(+), 15 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index 465ba8ae1..a3e3de5ed 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -465,21 +465,11 @@ abstract class MemberSymbExLogger(log: SymbExLogger[_], } private def getDelta(pair: (String, String)): (String, Option[String]) = { - val curValInt = pair._2.toIntOption - val prevValInt = lastStatistics.get(pair._1) match { - case Some(value) => value.toIntOption - case _ => Some(0) // value not found - } - val curValDouble = pair._2.toDoubleOption - val prevValDouble = lastStatistics.get(pair._1) match { - case Some(value) => value.toDoubleOption - case _ => Some(0.0) // value not found - } - (curValInt, prevValInt, curValDouble, prevValDouble) match { - case (Some(curInt), Some(prevInt), _, _) => (pair._1, Some((curInt - prevInt).toString)) - case (_, _, Some(curDouble), Some(prevDouble)) => (pair._1, Some((curDouble - prevDouble).toString)) - case _ => (pair._1, None) - } + val delta = + Try { (pair._2.toInt - lastStatistics(pair._1).toInt).toString } orElse + Try { (pair._2.toDouble - lastStatistics(pair._1).toDouble).toString } + + pair._1 -> delta.toOption } def macros(): Map[App, Term] = _macros From 85bd80df71cb19e9ada2cd3c22620652ac81e1c6 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 30 Nov 2022 12:19:51 +0100 Subject: [PATCH 27/31] use the symbExLog of the current verifier --- src/main/scala/rules/Brancher.scala | 4 +-- src/main/scala/rules/Consumer.scala | 12 ++++---- src/main/scala/rules/Evaluator.scala | 10 +++---- .../scala/rules/ExecutionFlowController.scala | 2 +- src/main/scala/rules/Executor.scala | 29 +++++++++---------- src/main/scala/rules/Producer.scala | 10 +++---- 6 files changed, 33 insertions(+), 34 deletions(-) diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index 9610a20c6..a2e509204 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -100,8 +100,8 @@ object brancher extends BranchingRules { } (v0: Verifier) => { - v.symbExLog.switchToNextBranch(uidBranchPoint) - v.symbExLog.markReachable(uidBranchPoint) + v0.symbExLog.switchToNextBranch(uidBranchPoint) + v0.symbExLog.markReachable(uidBranchPoint) if (v.uniqueId != v0.uniqueId){ /* [BRANCH-PARALLELISATION] */ // executing the else branch on a different verifier, need to adapt the state diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index d9a3e526c..b97b96216 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -158,10 +158,10 @@ object consumer extends ConsumptionRules { val h0 = s0.h /* h0 is h, but potentially consolidated */ val s1 = s0.copy(h = s.h) /* s1 is s, but the retrying flag might be set */ - val sepIdentifier = v.symbExLog.openScope(new ConsumeRecord(a, s1, v.decider.pcs)) + val sepIdentifier = v1.symbExLog.openScope(new ConsumeRecord(a, s1, v.decider.pcs)) consumeTlc(s1, h0, a, pve, v1)((s2, h2, snap2, v2) => { - v.symbExLog.closeScope(sepIdentifier) + v2.symbExLog.closeScope(sepIdentifier) QS(s2, h2, snap2, v2)}) })(Q) } @@ -191,11 +191,11 @@ object consumer extends ConsumptionRules { evaluator.eval(s, e0, pve, v)((s1, t0, v1) => branch(s1, t0, Some(e0), v1)( (s2, v2) => consumeR(s2, h, a0, pve, v2)((s3, h1, t1, v3) => { - v.symbExLog.closeScope(uidImplies) + v3.symbExLog.closeScope(uidImplies) Q(s3, h1, t1, v3) }), (s2, v2) => { - v.symbExLog.closeScope(uidImplies) + v2.symbExLog.closeScope(uidImplies) Q(s2, h, Unit, v2) })) @@ -206,11 +206,11 @@ object consumer extends ConsumptionRules { eval(s, e0, pve, v)((s1, t0, v1) => branch(s1, t0, Some(e0), v1)( (s2, v2) => consumeR(s2, h, a1, pve, v2)((s3, h1, t1, v3) => { - v.symbExLog.closeScope(uidCondExp) + v3.symbExLog.closeScope(uidCondExp) Q(s3, h1, t1, v3) }), (s2, v2) => consumeR(s2, h, a2, pve, v2)((s3, h1, t1, v3) => { - v.symbExLog.closeScope(uidCondExp) + v3.symbExLog.closeScope(uidCondExp) Q(s3, h1, t1, v3) }))) diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index c95364a2f..710674994 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -88,7 +88,7 @@ object evaluator extends EvaluationRules { val sepIdentifier = v.symbExLog.openScope(new EvaluateRecord(e, s, v.decider.pcs)) eval3(s, e, pve, v)((s1, t, v1) => { - v.symbExLog.closeScope(sepIdentifier) + v1.symbExLog.closeScope(sepIdentifier) Q(s1, t, v1)}) } @@ -316,7 +316,7 @@ object evaluator extends EvaluationRules { val uidImplies = v.symbExLog.openScope(impliesRecord) eval(s, e0, pve, v)((s1, t0, v1) => evalImplies(s1, t0, Some(e0), e1, implies.info == FromShortCircuitingAnd, pve, v1)((s2, t1, v2) => { - v.symbExLog.closeScope(uidImplies) + v2.symbExLog.closeScope(uidImplies) Q(s2, t1, v2) })) @@ -340,7 +340,7 @@ object evaluator extends EvaluationRules { sys.error(s"Unexpected join data entries: $entries")} (s2, result) })((s4, t3, v3) => { - v.symbExLog.closeScope(uidCondExp) + v3.symbExLog.closeScope(uidCondExp) Q(s4, t3, v3) })) @@ -556,7 +556,7 @@ object evaluator extends EvaluationRules { evalImplies(s3, Ite(argsPairWiseEqual, And(addCons :+ IsPositive(ch.perm)), False()), None,body, false, pve, v1) ((s4, tImplies, v2) => bindRcvrsAndEvalBody(s4, chs.tail, args, tImplies +: ts, v2)((s5, ts1, v3) => { - v.symbExLog.closeScope(uidImplies) + v3.symbExLog.closeScope(uidImplies) Q(s5, ts1, v3) })) }) @@ -594,7 +594,7 @@ object evaluator extends EvaluationRules { evalImplies(s2, And(trig, bc), None, body, false, pve, v1)((s3, tImplies, v2) => { val tQuant = Quantification(Forall, tVars, tImplies, tTriggers) bindQuantRcvrsAndEvalBody(s3, chs.tail, args, tQuant +: ts, v2)((s4, ts2, v3) => { - v.symbExLog.closeScope(uidImplies) + v3.symbExLog.closeScope(uidImplies) Q(s4, ts2, v3) })}) }) diff --git a/src/main/scala/rules/ExecutionFlowController.scala b/src/main/scala/rules/ExecutionFlowController.scala index 4b1192071..7d316964b 100644 --- a/src/main/scala/rules/ExecutionFlowController.scala +++ b/src/main/scala/rules/ExecutionFlowController.scala @@ -130,7 +130,7 @@ object executionFlowController extends ExecutionFlowRules { val comLog = new CommentRecord("Retry", s0, v.decider.pcs) val sepIdentifier = v.symbExLog.openScope(comLog) action(s0.copy(retrying = true, retryLevel = s.retryLevel), v, (s1, r, v1) => { - v.symbExLog.closeScope(sepIdentifier) + v1.symbExLog.closeScope(sepIdentifier) Q(s1.copy(retrying = false), r, v1) }) } diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index f9ab2816d..826314e18 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -63,11 +63,11 @@ object executor extends ExecutionRules { brancher.branch(s2, tCond, Some(ce.condition), v1)( (s3, v3) => exec(s3, ce.target, ce.kind, v3)((s4, v4) => { - v.symbExLog.closeScope(sepIdentifier) + v4.symbExLog.closeScope(sepIdentifier) Q(s4, v4) }), - (_, _) => { - v.symbExLog.closeScope(sepIdentifier) + (_, v3) => { + v3.symbExLog.closeScope(sepIdentifier) Success() })) @@ -112,7 +112,7 @@ object executor extends ExecutionRules { (s3, v3) => { val s3p = handleOutEdge(s3, thenEdge, v3) exec(s3p, thenEdge.target, thenEdge.kind, v3)((s4, v4) => { - v.symbExLog.closeScope(sepIdentifier) + v4.symbExLog.closeScope(sepIdentifier) val branchRes = Q(s4, v4) branchRes }) @@ -120,7 +120,7 @@ object executor extends ExecutionRules { (s3, v3) => { val s3p = handleOutEdge(s3, elseEdge, v3) exec(s3p, elseEdge.target, elseEdge.kind, v3)((s4, v4) => { - v.symbExLog.closeScope(sepIdentifier) + v4.symbExLog.closeScope(sepIdentifier) Q(s4, v4) }) })) @@ -256,7 +256,7 @@ object executor extends ExecutionRules { : VerificationResult = { val sepIdentifier = v.symbExLog.openScope(new ExecuteRecord(stmt, s, v.decider.pcs)) exec2(s, stmt, v)((s1, v1) => { - v.symbExLog.closeScope(sepIdentifier) + v1.symbExLog.closeScope(sepIdentifier) Q(s1, v1)}) } @@ -472,37 +472,36 @@ object executor extends ExecutionRules { val pveCall = CallFailed(call).withReasonNodeTransformed(reasonTransformer) val mcLog = new MethodCallRecord(call, s, v.decider.pcs) - val currentLog = v.symbExLog - val sepIdentifier = currentLog.openScope(mcLog) + val sepIdentifier = v.symbExLog.openScope(mcLog) val paramLog = new CommentRecord("Parameters", s, v.decider.pcs) - val paramId = currentLog.openScope(paramLog) + val paramId = v.symbExLog.openScope(paramLog) evals(s, eArgs, _ => pveCall, v)((s1, tArgs, v1) => { - currentLog.closeScope(paramId) + v1.symbExLog.closeScope(paramId) val exampleTrafo = CounterexampleTransformer({ case ce: SiliconCounterexample => ce.withStore(s1.g) case ce => ce }) val pvePre = ErrorWrapperWithExampleTransformer(PreconditionInCallFalse(call).withReasonNodeTransformed(reasonTransformer), exampleTrafo) val preCondLog = new CommentRecord("Precondition", s1, v1.decider.pcs) - val preCondId = currentLog.openScope(preCondLog) + val preCondId = v1.symbExLog.openScope(preCondLog) val s2 = s1.copy(g = Store(fargs.zip(tArgs)), recordVisited = true) consumes(s2, meth.pres, _ => pvePre, v1)((s3, _, v2) => { - currentLog.closeScope(preCondId) + v2.symbExLog.closeScope(preCondId) val postCondLog = new CommentRecord("Postcondition", s3, v2.decider.pcs) - val postCondId = currentLog.openScope(postCondLog) + val postCondId = v2.symbExLog.openScope(postCondLog) val outs = meth.formalReturns.map(_.localVar) val gOuts = Store(outs.map(x => (x, v2.decider.fresh(x))).toMap) val s4 = s3.copy(g = s3.g + gOuts, oldHeaps = s3.oldHeaps + (Verifier.PRE_STATE_LABEL -> s1.h)) produces(s4, freshSnap, meth.posts, _ => pveCall, v2)((s5, v3) => { - currentLog.closeScope(postCondId) + v3.symbExLog.closeScope(postCondId) v3.decider.prover.saturate(Verifier.config.proverSaturationTimeouts.afterContract) val gLhs = Store(lhs.zip(outs) .map(p => (p._1, s5.g(p._2))).toMap) val s6 = s5.copy(g = s1.g + gLhs, oldHeaps = s1.oldHeaps, recordVisited = s1.recordVisited) - currentLog.closeScope(sepIdentifier) + v3.symbExLog.closeScope(sepIdentifier) Q(s6, v3)})})}) case fold @ ast.Fold(ast.PredicateAccessPredicate(ast.PredicateAccess(eArgs, predicateName), ePerm)) => diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index bb191f7c7..d2347dadf 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -187,7 +187,7 @@ object producer extends ProductionRules { val sepIdentifier = v.symbExLog.openScope(new ProduceRecord(a, s, v.decider.pcs)) produceTlc(s, sf, a, pve, v)((s1, v1) => { - v.symbExLog.closeScope(sepIdentifier) + v1.symbExLog.closeScope(sepIdentifier) Q(s1, v1)}) } @@ -213,7 +213,7 @@ object producer extends ProductionRules { eval(s, e0, pve, v)((s1, t0, v1) => branch(s1, t0, Some(e0), v1)( (s2, v2) => produceR(s2, sf, a0, pve, v2)((s3, v3) => { - v.symbExLog.closeScope(uidImplies) + v3.symbExLog.closeScope(uidImplies) Q(s3, v3) }), (s2, v2) => { @@ -222,7 +222,7 @@ object producer extends ProductionRules { * otherwise. In order words, only make this assumption if `sf` has * already been used, e.g. in a snapshot equality such as `s0 == (s1, s2)`. */ - v.symbExLog.closeScope(uidImplies) + v2.symbExLog.closeScope(uidImplies) Q(s2, v2) })) @@ -233,11 +233,11 @@ object producer extends ProductionRules { eval(s, e0, pve, v)((s1, t0, v1) => branch(s1, t0, Some(e0), v1)( (s2, v2) => produceR(s2, sf, a1, pve, v2)((s3, v3) => { - v.symbExLog.closeScope(uidCondExp) + v3.symbExLog.closeScope(uidCondExp) Q(s3, v3) }), (s2, v2) => produceR(s2, sf, a2, pve, v2)((s3, v3) => { - v.symbExLog.closeScope(uidCondExp) + v3.symbExLog.closeScope(uidCondExp) Q(s3, v3) }))) From aab07e5d9fde1a4244fac10815cf7707de32d1f7 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 30 Nov 2022 12:26:20 +0100 Subject: [PATCH 28/31] resolve warnings: clean up imports; mark unused vals as @unused --- src/main/scala/decider/Decider.scala | 1 - src/main/scala/logger/SymbExLogger.scala | 2 -- src/main/scala/logger/records/SymbolicRecord.scala | 4 +++- src/main/scala/logger/records/data/DataRecord.scala | 4 +--- src/main/scala/logger/records/data/FunctionRecord.scala | 1 - src/main/scala/logger/records/data/MethodRecord.scala | 1 - src/main/scala/logger/records/data/PredicateRecord.scala | 1 - src/main/scala/rules/Brancher.scala | 1 - src/main/scala/rules/Consumer.scala | 1 - src/main/scala/rules/Evaluator.scala | 1 - src/main/scala/rules/ExecutionFlowController.scala | 1 - src/main/scala/rules/Executor.scala | 2 -- src/main/scala/rules/Joiner.scala | 1 - src/main/scala/rules/MoreCompleteExhaleSupporter.scala | 1 - src/main/scala/rules/Producer.scala | 1 - src/main/scala/rules/QuantifiedChunkSupport.scala | 1 - src/main/scala/rules/StateConsolidator.scala | 1 - src/main/scala/supporters/MethodSupporter.scala | 1 - src/main/scala/supporters/PredicateVerificationUnit.scala | 1 - .../scala/supporters/functions/FunctionVerificationUnit.scala | 1 - 20 files changed, 4 insertions(+), 24 deletions(-) diff --git a/src/main/scala/decider/Decider.scala b/src/main/scala/decider/Decider.scala index 42b458040..6b389d49b 100644 --- a/src/main/scala/decider/Decider.scala +++ b/src/main/scala/decider/Decider.scala @@ -15,7 +15,6 @@ import viper.silicon._ import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.interfaces._ import viper.silicon.interfaces.decider._ -import viper.silicon.logger.SymbExLogger import viper.silicon.logger.records.data.{DeciderAssertRecord, DeciderAssumeRecord, ProverAssertRecord} import viper.silicon.state._ import viper.silicon.state.terms._ diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index a3e3de5ed..3b6f38b68 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -15,13 +15,11 @@ import viper.silicon.logger.records.data._ import viper.silicon.logger.records.scoping.{CloseScopeRecord, OpenScopeRecord, ScopingRecord} import viper.silicon.logger.records.structural.BranchingRecord import viper.silicon.logger.renderer.SimpleTreeRenderer -import viper.silicon.state._ import viper.silicon.state.terms._ import viper.silicon.{Config, Map} import viper.silver.ast import viper.silver.ast.{Exp, Member} -import java.nio.file.{Files, Paths} import java.util.concurrent.atomic.AtomicInteger import scala.annotation.elidable import scala.annotation.elidable._ diff --git a/src/main/scala/logger/records/SymbolicRecord.scala b/src/main/scala/logger/records/SymbolicRecord.scala index e43432265..4d0c9c1d2 100644 --- a/src/main/scala/logger/records/SymbolicRecord.scala +++ b/src/main/scala/logger/records/SymbolicRecord.scala @@ -8,6 +8,8 @@ package viper.silicon.logger.records import viper.silicon.logger.LogConfig +import scala.annotation.unused + trait SymbolicRecord { var id: Int = -1 @@ -19,7 +21,7 @@ trait SymbolicRecord { def toSimpleString: String - def getData(config: LogConfig): RecordData = { + def getData(@unused config: LogConfig): RecordData = { new RecordData() } } diff --git a/src/main/scala/logger/records/data/DataRecord.scala b/src/main/scala/logger/records/data/DataRecord.scala index 70ef4dd13..7fc43f60a 100644 --- a/src/main/scala/logger/records/data/DataRecord.scala +++ b/src/main/scala/logger/records/data/DataRecord.scala @@ -7,12 +7,10 @@ package viper.silicon.logger.records.data import viper.silicon.common.collections.immutable.InsertionOrderedSet -import viper.silicon.logger.{LogConfig, SymbExLogger} +import viper.silicon.logger.LogConfig import viper.silicon.logger.records.{RecordData, SymbolicRecord} -import viper.silicon.state.State import viper.silicon.state.terms.Term import viper.silicon.utils -import viper.silicon.verifier.Verifier import viper.silver.ast import viper.silver.ast.Positioned diff --git a/src/main/scala/logger/records/data/FunctionRecord.scala b/src/main/scala/logger/records/data/FunctionRecord.scala index a2b6f6066..ac09be1a4 100644 --- a/src/main/scala/logger/records/data/FunctionRecord.scala +++ b/src/main/scala/logger/records/data/FunctionRecord.scala @@ -8,7 +8,6 @@ package viper.silicon.logger.records.data import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.PathConditionStack -import viper.silicon.state.State import viper.silicon.state.terms.Term import viper.silver.ast diff --git a/src/main/scala/logger/records/data/MethodRecord.scala b/src/main/scala/logger/records/data/MethodRecord.scala index d75c3a7ae..9a2d4b1b8 100644 --- a/src/main/scala/logger/records/data/MethodRecord.scala +++ b/src/main/scala/logger/records/data/MethodRecord.scala @@ -8,7 +8,6 @@ package viper.silicon.logger.records.data import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.PathConditionStack -import viper.silicon.state._ import viper.silicon.state.terms.Term import viper.silver.ast diff --git a/src/main/scala/logger/records/data/PredicateRecord.scala b/src/main/scala/logger/records/data/PredicateRecord.scala index de6e016b3..01b3a4d44 100644 --- a/src/main/scala/logger/records/data/PredicateRecord.scala +++ b/src/main/scala/logger/records/data/PredicateRecord.scala @@ -8,7 +8,6 @@ package viper.silicon.logger.records.data import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.PathConditionStack -import viper.silicon.state.State import viper.silicon.state.terms.Term import viper.silver.ast diff --git a/src/main/scala/rules/Brancher.scala b/src/main/scala/rules/Brancher.scala index a2e509204..e062ead3a 100644 --- a/src/main/scala/rules/Brancher.scala +++ b/src/main/scala/rules/Brancher.scala @@ -10,7 +10,6 @@ import java.util.concurrent._ import viper.silicon.common.concurrency._ import viper.silicon.decider.PathConditionStack import viper.silicon.interfaces.{Unreachable, VerificationResult} -import viper.silicon.logger.SymbExLogger import viper.silicon.state.State import viper.silicon.state.terms.{FunctionDecl, MacroDecl, Not, Term} import viper.silicon.verifier.Verifier diff --git a/src/main/scala/rules/Consumer.scala b/src/main/scala/rules/Consumer.scala index b97b96216..808227804 100644 --- a/src/main/scala/rules/Consumer.scala +++ b/src/main/scala/rules/Consumer.scala @@ -12,7 +12,6 @@ import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssert import viper.silver.verifier.PartialVerificationError import viper.silver.verifier.reasons._ import viper.silicon.interfaces.VerificationResult -import viper.silicon.logger.SymbExLogger import viper.silicon.logger.records.data.{CondExpRecord, ConsumeRecord, ImpliesRecord} import viper.silicon.state._ import viper.silicon.state.terms._ diff --git a/src/main/scala/rules/Evaluator.scala b/src/main/scala/rules/Evaluator.scala index 710674994..c5722d67f 100644 --- a/src/main/scala/rules/Evaluator.scala +++ b/src/main/scala/rules/Evaluator.scala @@ -22,7 +22,6 @@ import viper.silicon.utils.ast.flattenOperator import viper.silicon.verifier.Verifier import viper.silicon.{Map, TriggerSets} import viper.silicon.interfaces.state.{ChunkIdentifer, NonQuantifiedChunk} -import viper.silicon.logger.SymbExLogger import viper.silicon.logger.records.data.{CondExpRecord, EvaluateRecord, ImpliesRecord} /* TODO: With the current design w.r.t. parallelism, eval should never "move" an execution diff --git a/src/main/scala/rules/ExecutionFlowController.scala b/src/main/scala/rules/ExecutionFlowController.scala index 7d316964b..dee0d37f6 100644 --- a/src/main/scala/rules/ExecutionFlowController.scala +++ b/src/main/scala/rules/ExecutionFlowController.scala @@ -7,7 +7,6 @@ package viper.silicon.rules import viper.silicon.interfaces._ -import viper.silicon.logger.SymbExLogger import viper.silicon.logger.records.data.CommentRecord import viper.silicon.state.State import viper.silicon.verifier.Verifier diff --git a/src/main/scala/rules/Executor.scala b/src/main/scala/rules/Executor.scala index 826314e18..2d81b7f2f 100644 --- a/src/main/scala/rules/Executor.scala +++ b/src/main/scala/rules/Executor.scala @@ -13,10 +13,8 @@ import viper.silver.verifier.{CounterexampleTransformer, PartialVerificationErro import viper.silver.verifier.errors._ import viper.silver.verifier.reasons._ import viper.silver.{ast, cfg} -import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.RecordedPathConditions import viper.silicon.interfaces._ -import viper.silicon.logger.SymbExLogger import viper.silicon.logger.records.data.{CommentRecord, ConditionalEdgeRecord, ExecuteRecord, MethodCallRecord} import viper.silicon.resources.FieldID import viper.silicon.state._ diff --git a/src/main/scala/rules/Joiner.scala b/src/main/scala/rules/Joiner.scala index f6fbba0e6..5c46680f6 100644 --- a/src/main/scala/rules/Joiner.scala +++ b/src/main/scala/rules/Joiner.scala @@ -8,7 +8,6 @@ package viper.silicon.rules import viper.silicon.decider.RecordedPathConditions import viper.silicon.interfaces.{Success, VerificationResult} -import viper.silicon.logger.SymbExLogger import viper.silicon.logger.records.structural.JoiningRecord import viper.silicon.state.State import viper.silicon.verifier.Verifier diff --git a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala index fc6f0aead..248f0469a 100644 --- a/src/main/scala/rules/MoreCompleteExhaleSupporter.scala +++ b/src/main/scala/rules/MoreCompleteExhaleSupporter.scala @@ -10,7 +10,6 @@ import scala.collection.mutable.ListBuffer import viper.silicon.{MList, MMap} import viper.silicon.interfaces.state._ import viper.silicon.interfaces.{Success, VerificationResult} -import viper.silicon.logger.SymbExLogger import viper.silicon.resources.{FieldID, NonQuantifiedPropertyInterpreter, Resources} import viper.silicon.rules.chunkSupporter.findChunksWithID import viper.silicon.state._ diff --git a/src/main/scala/rules/Producer.scala b/src/main/scala/rules/Producer.scala index d2347dadf..1340dd67c 100644 --- a/src/main/scala/rules/Producer.scala +++ b/src/main/scala/rules/Producer.scala @@ -11,7 +11,6 @@ import viper.silver.ast import viper.silver.ast.utility.QuantifiedPermissions.QuantifiedPermissionAssertion import viper.silver.verifier.PartialVerificationError import viper.silicon.interfaces.VerificationResult -import viper.silicon.logger.SymbExLogger import viper.silicon.logger.records.data.{CondExpRecord, ImpliesRecord, ProduceRecord} import viper.silicon.resources.{FieldID, PredicateID} import viper.silicon.state.terms.predef.`?r` diff --git a/src/main/scala/rules/QuantifiedChunkSupport.scala b/src/main/scala/rules/QuantifiedChunkSupport.scala index 28e575f42..c832f7f61 100644 --- a/src/main/scala/rules/QuantifiedChunkSupport.scala +++ b/src/main/scala/rules/QuantifiedChunkSupport.scala @@ -14,7 +14,6 @@ import viper.silver.verifier.reasons.{InsufficientPermission, MagicWandChunkNotF import viper.silicon.Map import viper.silicon.interfaces.state._ import viper.silicon.interfaces.VerificationResult -import viper.silicon.logger.SymbExLogger import viper.silicon.logger.records.data.CommentRecord import viper.silicon.resources.{NonQuantifiedPropertyInterpreter, QuantifiedPropertyInterpreter, Resources} import viper.silicon.state._ diff --git a/src/main/scala/rules/StateConsolidator.scala b/src/main/scala/rules/StateConsolidator.scala index 6412f0ff8..373076b8a 100644 --- a/src/main/scala/rules/StateConsolidator.scala +++ b/src/main/scala/rules/StateConsolidator.scala @@ -10,7 +10,6 @@ import scala.annotation.unused import viper.silicon.Config import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.interfaces.state._ -import viper.silicon.logger.SymbExLogger import viper.silicon.logger.records.data.{CommentRecord, SingleMergeRecord} import viper.silicon.resources.{NonQuantifiedPropertyInterpreter, Resources} import viper.silicon.state._ diff --git a/src/main/scala/supporters/MethodSupporter.scala b/src/main/scala/supporters/MethodSupporter.scala index d2feb4d06..e78253f3f 100644 --- a/src/main/scala/supporters/MethodSupporter.scala +++ b/src/main/scala/supporters/MethodSupporter.scala @@ -12,7 +12,6 @@ import viper.silver.components.StatefulComponent import viper.silver.verifier.errors._ import viper.silicon.interfaces._ import viper.silicon.decider.Decider -import viper.silicon.logger.SymbExLogger import viper.silicon.logger.records.data.WellformednessCheckRecord import viper.silicon.rules.{consumer, executionFlowController, executor, producer} import viper.silicon.state.{Heap, State, Store} diff --git a/src/main/scala/supporters/PredicateVerificationUnit.scala b/src/main/scala/supporters/PredicateVerificationUnit.scala index a8714079b..388c54709 100644 --- a/src/main/scala/supporters/PredicateVerificationUnit.scala +++ b/src/main/scala/supporters/PredicateVerificationUnit.scala @@ -18,7 +18,6 @@ import viper.silicon.state._ import viper.silicon.state.State.OldHeaps import viper.silicon.state.terms._ import viper.silicon.interfaces._ -import viper.silicon.logger.SymbExLogger import viper.silicon.rules.executionFlowController import viper.silicon.verifier.{Verifier, VerifierComponent} import viper.silicon.utils.freshSnap diff --git a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala index 7056f6d27..4c0c7c5f7 100644 --- a/src/main/scala/supporters/functions/FunctionVerificationUnit.scala +++ b/src/main/scala/supporters/functions/FunctionVerificationUnit.scala @@ -20,7 +20,6 @@ import viper.silicon.state.terms._ import viper.silicon.state.terms.predef.`?s` import viper.silicon.common.collections.immutable.InsertionOrderedSet import viper.silicon.decider.Decider -import viper.silicon.logger.SymbExLogger import viper.silicon.rules.{consumer, evaluator, executionFlowController, producer} import viper.silicon.supporters.PredicateData import viper.silicon.verifier.{Verifier, VerifierComponent} From 59f43e1531161ac23f540a053c0da8233475ed6c Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 30 Nov 2022 12:35:35 +0100 Subject: [PATCH 29/31] missed merge conflict: just use ours --- src/main/scala/logger/SymbExLogger.scala | 62 ------------------------ 1 file changed, 62 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index bcd840d53..3b6f38b68 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -276,70 +276,8 @@ case class SymbExLog(logConfig: LogConfig) extends SymbExLogger[MemberSymbExLog] * Simple string representation of the logs. */ def toSimpleTreeString: String = { -<<<<<<< HEAD val simpleTreeRenderer = new SimpleTreeRenderer() simpleTreeRenderer.render(members.values) -======= - if (enabled) { - val simpleTreeRenderer = new SimpleTreeRenderer() - simpleTreeRenderer.render(memberList) - } else "" - } - - /** Path to the file that is being executed. Is used for UnitTesting. **/ - var filePath: Path = _ - - /** - * Resets the SymbExLogger-object, to make it ready for a new file. - * Only needed when several files are verified together (e.g., sbt test). - */ - def reset(): Unit = { - memberList = Seq[SymbLog]() - uidCounter = 0 - filePath = null - logConfig = LogConfig.default() - prevSmtStatistics = Map.empty - } - - def resetMemberList(): Unit = { - memberList = Seq[SymbLog]() - // or reset by calling it from Decider.reset - prevSmtStatistics = Map.empty - } - - /** - * Calculates diff between `currentStatistics` and the statistics from a previous call. - * The difference is calculated if value can be converted to an int or double - * @param currentStatistics most recent statistics from the SMT solver - * @return map with differences (only containing values that could be converted) and keys with appended "-delta" - */ - def getDeltaSmtStatistics(currentStatistics: Map[String, String]) : Map[String, String] = { - val deltaStatistics = currentStatistics map getDelta filter { case (_, value) => value.nonEmpty } map { - case (key, Some(value)) => (key + "-delta", value) - case other => sys.error(s"Unexpected result pair $other") - } - // set prevStatistics (i.e. override values with same key or add): - prevSmtStatistics = prevSmtStatistics ++ currentStatistics - deltaStatistics - } - - private def getDelta(pair: (String, String)): (String, Option[String]) = { - val curValInt = pair._2.toIntOption - val prevValInt = prevSmtStatistics.get(pair._1) match { - case Some(value) => value.toIntOption - case _ => Some(0) // value not found - } - val curValDouble = pair._2.toDoubleOption - val prevValDouble = prevSmtStatistics.get(pair._1) match { - case Some(value) => value.toDoubleOption - case _ => Some(0.0) // value not found - } - (curValInt, prevValInt, curValDouble, prevValDouble) match { - case (Some(curInt), Some(prevInt), _, _) => (pair._1, Some((curInt - prevInt).toString)) - case (_, _, Some(curDouble), Some(prevDouble)) => (pair._1, Some((curDouble - prevDouble).toString)) - case _ => (pair._1, None) - } ->>>>>>> upstream-master } } From b333909f54825ef30a23eeb50ff5118da93ef7a6 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 30 Nov 2022 13:10:35 +0100 Subject: [PATCH 30/31] adjust documentation --- src/main/scala/logger/SymbExLogger.scala | 42 ++++++++++--------- .../logger/writer/SymbExLogReportWriter.scala | 2 +- 2 files changed, 24 insertions(+), 20 deletions(-) diff --git a/src/main/scala/logger/SymbExLogger.scala b/src/main/scala/logger/SymbExLogger.scala index 3b6f38b68..b368c2c0a 100644 --- a/src/main/scala/logger/SymbExLogger.scala +++ b/src/main/scala/logger/SymbExLogger.scala @@ -68,23 +68,30 @@ import scala.util.{Failure, Success, Try} * well as any ExecuteRecord with statement "a := 1" (all other ExecuteRecords will be omitted) */ -/* +/** * ================================ * SymbExLogger Architecture * ================================ * Overall concept: - * 1) SymbExLogger Object: - * Is used as interface to access the logs. Code from this file that is used in Silicon - * should only be used via SymbExLogger. Contains a list of SymbLog, one SymbLog - * per method/function/predicate (member). The method 'currentLog()' gives access to the log - * of the currently executed member. - * 2) SymbLog: - * Contains the log for a member. Most important methods: openScope/closeScope/insertBranchPoint. To 'start' + * 1) [[SymbExLogger]]: + * SymbExLogger is the root log for a verification run. Implementers of SymbExLogger define how to make a + * [[MemberSymbExLogger]]: the log for a method/function/predicate (member). Contains a map of members logs. + * The default implementation is [[NoopSymbExLog]], which ignores all log records. When the symbolic execution logger + * is enabled, [[SymbExLog]] is used instead. It instantiates the member loggers as MemberSymbExLog, which records + * all log records in memory. + * [[viper.silicon.verifier.MainVerifier]] owns the root SymbExLogger, from which member logs can be created. + * 2) [[MemberSymbExLogger]]: + * Handles the log for a member. Most important methods: openScope/closeScope/insertBranchPoint. To 'start' * a record use openScope, to finish the recording use closeScope. For each execution path, there should be a * closeScope for each openScope. Due to branching this means that there might be multiple closeScopes for a * openScope, because the scope has to be closed on each branch. However to support verification failures, the log * does not have to be complete. In case of a missing close scope record, the scope will be closed immediately * before an outer close scope record. + * The default implementation is [[NoopMemberSymbExLog]], which ignores all log records. When the symbolic execution + * logger is enabled, [[MemberSymbExLog]] is used instead, which records all log records in memory. + * Each [[viper.silicon.verifier.Verifier]] owns a [[MemberSymbExLog]] for the member it is currently verifying. + * [[viper.silicon.verifier.DefaultMainVerifier]] also owns a [[MemberSymbExLog]], since it also verifies members + * itself. * 3) Records: * There are scoping records representing open and close scope in the log. These records will be automatically * inserted in the log by SymbExLogger depending on other records. @@ -145,8 +152,8 @@ import scala.util.{Failure, Success, Try} * * Use of CommentRecord (1): * At the point in the code where you want to add the comment, call - * //val id = SymbExLogger.currentLog().openScope(new CommentRecord(my_info, σ, c) - * //SymbExLogger.currentLog().closeScope(id) + * //val id = symbExLog.openScope(new CommentRecord(my_info, σ, c) + * //symbExLog.closeScope(id) * σ is the current state (AnyRef, but should be of type State[_,_,_] usually), my_info * is a string that contains the information you want to store, c is the current * context. If you want to store more information than just a string, consider (2). @@ -159,10 +166,10 @@ import scala.util.{Failure, Success, Try} * As an example, the joining (e.g. occurring in pure conditional expressions) is discussed next: * Silicon uses Joiner to join execution after an execution block. A JoiningRecord is created at the beginning of the * Joiner and added to the log by calling: - * // val uidJoin = SymbExLogger.currentLog().openScope(joiningRecord) + * // val uidJoin = symbExLog.openScope(joiningRecord) * After executing the block and joining the execution, the following call to the SymbExLogger is made to close the * join scope: - * // SymbExLogger.currentLog().closeScope(uidJoin) + * // symbExLog.closeScope(uidJoin) * Although JoiningRecord is a structural record and joining in symbolic execution has significant impact on the * execution structure, JoiningRecord behalves almost as a data record in SymbExLogger: * Due to the design that each data record (and joining record) causes a scope and the scope contains all @@ -173,15 +180,15 @@ import scala.util.{Failure, Success, Try} * logger has to be informed about it in order that records on the individual branches are correctly logged. * To do so, the following call creates a new branch point with a number of branches that result out of it (but aren't * necessarily all reachable): - * // val uidBranchPoint = SymbExLogger.currentLog().insertBranchPoint(2, Some(condition)) + * // val uidBranchPoint = symbExLog.insertBranchPoint(2, Some(condition)) * All records that will subsequently be inserted will be assigned to the first branch. * As soon as the execution of the first branch is complete, the logger needs to switch to the next branch: - * // SymbExLogger.currentLog().switchToNextBranch(uidBranchPoint) + * // symbExLog.switchToNextBranch(uidBranchPoint) * When the execution of all branches is done, the branch point is concluded: - * // SymbExLogger.currentLog().endBranchPoint(uidBranchPoint) + * // symbExLog.endBranchPoint(uidBranchPoint) * Because the existence as well as non-existence of records on a branch does not imply reachability, the logger * needs to be explicitly informed for each branch that is reachable: - * // SymbExLogger.currentLog().markReachable(uidBranchPoint) + * // symbExLog.markReachable(uidBranchPoint) */ case object SymbExLogger { @@ -229,9 +236,6 @@ abstract class SymbExLogger[Log <: MemberSymbExLogger]() { /** Add a new log for a method, function or predicate (member). * * @param member Either a MethodRecord, PredicateRecord or a FunctionRecord. - * @param s Current state. Since the body of the method (predicate/function) is not yet - * executed/logged, this is usually the empty state (use Σ(Ø, Ø, Ø) for empty - * state). * @param pcs Current path conditions. */ @elidable(INFO) diff --git a/src/main/scala/logger/writer/SymbExLogReportWriter.scala b/src/main/scala/logger/writer/SymbExLogReportWriter.scala index 4ad60d8a0..8b3d9928f 100644 --- a/src/main/scala/logger/writer/SymbExLogReportWriter.scala +++ b/src/main/scala/logger/writer/SymbExLogReportWriter.scala @@ -114,7 +114,7 @@ object SymbExLogReportWriter { JsArray(records) } - /** Translates a InMemorySymbLog to a vector of JsValues. + /** Translates a MemberSymbExLog to a vector of JsValues. * * @param symbLog The symbolic log to translate. * @return array of all records. From 6dff920667041c2dcb8b4dbed43a18fe317b9396 Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Wed, 30 Nov 2022 13:33:48 +0100 Subject: [PATCH 31/31] update silver --- silver | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/silver b/silver index d978f88eb..8b6c8e363 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit d978f88eb363440390ca3baa62ce56ad3fadc42c +Subproject commit 8b6c8e363e2f569a8fde394d6aa4ee7b2835c24c