From 1da03220c9158dda512d5b6b5d98f0e6dd44ffe9 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Thu, 29 Oct 2020 14:12:02 +0100 Subject: [PATCH 1/5] Better cover info --- .../tla/assignments/CoverChecker.scala | 8 ++ .../apalache/tla/assignments/CoverData.scala | 38 +++--- .../passes/CoverAnalysisPassImpl.scala | 115 +++++++++++++++--- .../apalache/tla/lir/src/SourceLocation.scala | 11 +- 4 files changed, 141 insertions(+), 31 deletions(-) diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala index 1163547fed..a5467c4ba2 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala @@ -89,6 +89,14 @@ class CoverChecker( allVariables: Set[String], manuallyAssigned: Set[String] = S } + /** Computes a set of assignment candidates under `ex` */ + def assignmentLocaitons( ex: TlaEx ) : Set[Candidate] = { + val cd = mkCover( ex ) + allVariables flatMap { + v => CoverData.uncoveredBranchPoints( v )( cd ).problemUIDs.asgns + } + } + def findProblems( ex: TlaEx ): Option[Map[ String, ProblemData ]] = { val cd = mkCover(ex) diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverData.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverData.scala index d9bcac5166..a022038505 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverData.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverData.scala @@ -17,13 +17,14 @@ object CoverData{ class CoverException( s : String ) extends Exception( s ) - class IncompleteCover(seq: Seq[UID]) { + class IncompleteCover( seq: Seq[UID], assignments: Seq[Candidate]) { def get: Seq[UID] = seq + def asgns: Seq[Candidate] = assignments def isEmpty: Boolean = seq.isEmpty } - sealed case class AtLeastOne( seq: Seq[UID] ) extends IncompleteCover(seq) - sealed case class All( seq: Seq[UID] ) extends IncompleteCover(seq) - sealed case class NoProblem() extends IncompleteCover( Seq.empty ) + sealed case class AtLeastOne( seq: Seq[UID], assignments: Seq[Candidate] ) extends IncompleteCover(seq, assignments ) + sealed case class All( seq: Seq[UID], assignments: Seq[Candidate] ) extends IncompleteCover(seq, assignments) + sealed case class NoProblem( assignments: Seq[Candidate] ) extends IncompleteCover( Seq.empty, assignments) /** * ProblemData represents potential witnesses to cover violations. @@ -59,22 +60,25 @@ object CoverData{ } def uncoveredBranchPoints( varName: String )( cd: CoverData ) : ProblemData = cd match { - case Candidate( v, loc ) => + case c@Candidate( v, loc ) => // Candidate(v, _) covers varName iff v == varName - val problem = if ( varName == v ) NoProblem() else AtLeastOne( Seq( loc ) ) + val problem = if ( varName == v ) NoProblem( Seq( c ) ) else AtLeastOne( Seq( loc ), Seq.empty ) ProblemData( problem, Map.empty ) case NonCandidate( loc ) => // NonCandidate never covers varname, but is also a leaf in blameMap - ProblemData( AtLeastOne( Seq( loc ) ), Map.empty ) + ProblemData( AtLeastOne( Seq( loc ), Seq.empty ), Map.empty ) case BranchPoint( loc, branches@_* ) => // BranchPoint represents disjunction/ITE, so it covers varName iff // *all* disjuncts/ITE branches cover varName val branchIssues = - branches.foldLeft( ProblemData( NoProblem(), Map.empty ) ) { + branches.foldLeft( ProblemData( NoProblem( Seq.empty ), Map.empty ) ) { case (pd,brCd) => val brPd = uncoveredBranchPoints( varName )( brCd ) ProblemData( - All( pd.problemUIDs.get ++ brPd.problemUIDs.get ), + All( + pd.problemUIDs.get ++ brPd.problemUIDs.get, + pd.problemUIDs.asgns ++ brPd.problemUIDs.asgns + ), pd.blameMap ++ brPd.blameMap ) } @@ -83,7 +87,7 @@ object CoverData{ // If a subexpression contains a cover violation the BranchPoint sets itself // as a problem location and pushes the subexpression issues into blameMap ProblemData( - All( Seq( loc ) ), + All( Seq( loc ), branchIssues.problemUIDs.asgns ), branchIssues.blameMap + ( loc -> branchIssues.problemUIDs ) ) } else { @@ -94,21 +98,25 @@ object CoverData{ // NonBranch corresponds to conjunction, so it covers varName if any of its // subexpressions cover varName val elemIssues = elements map uncoveredBranchPoints( varName ) - if ( elemIssues.exists( _.problemUIDs.isEmpty ) ) { + val coverOpt = elemIssues.find( _.problemUIDs.isEmpty ) + if ( coverOpt.nonEmpty ) { // If a suitable cover is found, report NoProblem - ProblemData( NoProblem(), Map.empty ) + ProblemData( NoProblem( coverOpt.get.problemUIDs.asgns ), Map.empty ) } else { // Otherwise, no sub-expression covers varName, so we aggregate all sub-locations - val problemAggregate = elemIssues.foldLeft( ProblemData( NoProblem(), Map.empty ) ) { + val problemAggregate = elemIssues.foldLeft( ProblemData( NoProblem(Seq.empty), Map.empty ) ) { case (pd,brPd) => ProblemData( - AtLeastOne( pd.problemUIDs.get ++ brPd.problemUIDs.get), + AtLeastOne( + pd.problemUIDs.get ++ brPd.problemUIDs.get, + pd.problemUIDs.asgns ++ brPd.problemUIDs.asgns + ), pd.blameMap ++ brPd.blameMap ) } // Then, NonBranch sets itself as a problem location, as in the previous case ProblemData( - AtLeastOne( Seq( loc ) ), + AtLeastOne( Seq( loc ), problemAggregate.problemUIDs.asgns ), problemAggregate.blameMap + ( loc -> problemAggregate.problemUIDs ) ) } diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala index 2dfb7f4f64..b31e687c46 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala @@ -4,16 +4,20 @@ import java.io.{File, FileWriter, PrintWriter} import java.nio.file.Path import at.forsyte.apalache.infra.passes.{Pass, PassOptions, TlaModuleMixin} -import at.forsyte.apalache.tla.assignments.{CoverChecker, CoverData, ManualAssignments} +import at.forsyte.apalache.tla.assignments.{CoverChecker, ManualAssignments} import at.forsyte.apalache.tla.imp.findBodyOf -import at.forsyte.apalache.tla.lir.storage.BodyMapFactory +import at.forsyte.apalache.tla.imp.src.SourceStore +import at.forsyte.apalache.tla.lir.storage.{BodyMapFactory, ChangeListener, SourceLocator} import at.forsyte.apalache.tla.lir.TlaOperDecl +import at.forsyte.apalache.tla.lir.src.SourceLocation import at.forsyte.apalache.tla.lir.transformations.TransformationTracker import com.google.inject.Inject import com.google.inject.name.Named import com.typesafe.scalalogging.LazyLogging class CoverAnalysisPassImpl @Inject()(options: PassOptions, + sourceStore: SourceStore, + changeListener: ChangeListener, tracker: TransformationTracker, @Named("AfterCoverAnalysis") nextPass: Pass with TlaModuleMixin ) extends CoverAnalysisPass with LazyLogging { @@ -41,30 +45,113 @@ class CoverAnalysisPassImpl @Inject()(options: PassOptions, val coverChecker = new CoverChecker(varSet, manualAssignments) logger.info(s" > Computing assignment cover for $nextName") - val coverMap = bodyMap map { case (opName, TlaOperDecl( _, _, body )) => + val mustCoverMap = bodyMap map { case (opName, TlaOperDecl( _, _, body )) => // technically suboptimal, since the same CoverData is computed multiple times, // but no need to change it if it doesn't impact runtime - opName -> coverChecker.coveredVars( body ).toList.sorted + opName -> coverChecker.coveredVars( body ) } + // we compute assignment witnesses + val asgns = + coverChecker.assignmentLocaitons( nextBody ) ++ coverChecker.assignmentLocaitons( initBody ) val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] val outFile = new File(outdir.toFile, "out-cover.txt") - val outStr = coverMap.map { - case (opName, coverLst) => s"${opName} covers: ${coverLst.mkString(", ")}" } - .mkString("\n") + val sourceLoc = SourceLocator(sourceStore.makeSourceMap, changeListener) + + // we add source info + val locVarSet = asgns map { + cand => + ( cand.varName, sourceLoc.sourceOf( cand.uid ) ) + } // duplicates are removed + + // We remove all assignments for which source info isn't available + // and sort the rest by source + val sortedAsgns = + locVarSet.toList.withFilter { + _._2.nonEmpty + } map { case (x, yOpt) => + (x, yOpt.get) + } sortBy { + _._2 + } + + // For each operator, we compute the SourceLocation of its body + val opLocs = bodyMap map { + case (opName, opDecl) => opName -> sourceLoc.sourceOf( bodyMap(opName).body.ID ) + } + + // Given a SourceLocation, we can find the operator containing it, if it exists + def definingOper( loc: SourceLocation ) : Option[String] = + bodyMap.keySet.find { + opName => + opLocs(opName).exists { + bodyLoc : SourceLocation => + bodyLoc.region.contains( loc.region ) + } + } + + val defaultOpName = "" + + // We prepare the triplets that will be passed to the format strings + val outTriples = sortedAsgns map { case (varName, loc) => + ( loc.toString, definingOper( loc ).getOrElse(defaultOpName), varName ) + } + + // From them, we generate a may-cover map, by aggregating the variables for each operator + val mayCoverMap: Map[String, Set[String]] = + outTriples.foldLeft( Map.empty[String,Set[String]] ) { + case (m, (_, opName, varName)) => + m + ( opName -> ( m.getOrElse( opName, Set.empty ) + varName ) ) + } + + // For nicer formatting, we compute the max width for the source and name fields + val longestLoc = outTriples.map( _._1.length ).max + val longestOpName = outTriples.map( _._2.length ).max + + val formatStringMay = s"%-${longestLoc}s: %${longestOpName}s may update %s" + val formatStringMust = s"%-${longestLoc}s: %${longestOpName}s always updates: %s" + val formatStringWarning = s"%-${longestLoc}s: %${longestOpName}s sometimes does not update: %s \t [WARNING!] " + + // The first part of the output lists all assignment witnesses + val outStrMay = outTriples.map { case (loc, opName, varName) => + formatStringMay.format( loc, opName, varName ) + }.mkString("\n") ++ "\n\n" + + def sortedVarString( s: Set[String] ) = s.toList.sorted.mkString(", ") + + // The second part of the output lists, for each operator, all variables it must update (if any) + // and a warning for each variable that may be updated but is not guaranteed to be updated + val outStrMustWarning = mayCoverMap.keySet.toList.sortBy( k => opLocs(k).get) flatMap { opName: String => + val locOpt = opLocs(opName) + locOpt map { loc => + // for Init we know any updates appear only in InitPrime + val initPrimeNameCorrection = if (opName == initName) initPrimedName else opName + val mustVars = mustCoverMap.getOrElse( initPrimeNameCorrection, Set.empty ) + // if there are no guaranteed vars we don't want any output + val mustStrOpt = + if (mustVars.isEmpty) + None + else + Some( formatStringMust.format( loc.toString, opName, sortedVarString(mustVars) ) ) + val notGuaranteed = mayCoverMap(opName) -- mustVars + // Similarly, we only want to see a warning if `notGuaranteed` is nonempty + val warningOpt = + if (notGuaranteed.isEmpty) + None + else + Some( formatStringWarning.format( loc.toString, opName, sortedVarString( notGuaranteed) ) ) + + List( mustStrOpt, warningOpt ).flatten.mkString("\n") + } + } mkString "\n" + + val outStr = outStrMay + outStrMustWarning val pw = new PrintWriter(new FileWriter(outFile, false)) pw.write( outStr ) pw.close() - - val notCovered = (varSet -- coverMap(nextName).toSet).toList.sorted - if (notCovered.nonEmpty) - throw new CoverData.CoverException( - s"Operator $nextName does not cover: ${notCovered.mkString(", ")}. See ${outFile.getAbsolutePath}" - ) - true } diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/src/SourceLocation.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/src/SourceLocation.scala index 3593378af5..9afd97baf0 100644 --- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/src/SourceLocation.scala +++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/src/SourceLocation.scala @@ -7,7 +7,7 @@ package at.forsyte.apalache.tla.lir.src * * @author Igor Konnov */ -class SourceLocation(val filename: String, val region: SourceRegion) { +class SourceLocation(val filename: String, val region: SourceRegion) extends Ordered[SourceLocation]{ override def toString: String = filename + ".tla:" + region @@ -25,4 +25,11 @@ class SourceLocation(val filename: String, val region: SourceRegion) { val state = Seq(filename, region) state.map(_.hashCode()).foldLeft(0)((a, b) => 31 * a + b) } -} \ No newline at end of file + + // Defines an ordering on SourceLocation + override def compare( other : SourceLocation) : Int = + Ordering.Tuple3[String, Int, Int].compare( + (filename, region.start.offset, region.end.offset), + (other.filename, other.region.start.offset, other.region.end.offset) + ) +} From 1b222cba0d350b9516517ff45f067a0e3d300a5c Mon Sep 17 00:00:00 2001 From: Kukovec Date: Thu, 29 Oct 2020 15:36:45 +0100 Subject: [PATCH 2/5] Shifted cover analysis before inlining --- .../tla/assignments/CoverChecker.scala | 210 ++++++++++++------ .../passes/CoverAnalysisPassImpl.scala | 26 ++- .../apalache/tla/assignments/TestCover.scala | 4 +- .../tla/bmcmt/config/CheckerModule.scala | 30 +-- 4 files changed, 180 insertions(+), 90 deletions(-) diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala index a5467c4ba2..9c26b7ee77 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala @@ -1,8 +1,8 @@ package at.forsyte.apalache.tla.assignments -import at.forsyte.apalache.tla.assignments.CoverData.ProblemData import at.forsyte.apalache.tla.lir.oper._ import at.forsyte.apalache.tla.lir._ +import at.forsyte.apalache.tla.lir.storage.BodyMap import scala.collection.immutable.{Map, Set} @@ -13,105 +13,189 @@ import scala.collection.immutable.{Map, Set} */ class CoverChecker( allVariables: Set[String], manuallyAssigned: Set[String] = Set.empty ) { - type letInOperBodyMapType = Map[String, CoverData] - private def mkCoverInternal( initialLetInOperBodyMap : letInOperBodyMapType ) - ( ex: TlaEx ): CoverData = ex match { + type operCoverMapType = Map[String, CoverData] + + def mkCover( bodyMap: BodyMap ) : operCoverMapType = bodyMap.values.foldLeft( Map.empty[String,CoverData] ){ + case (partialMap, TlaOperDecl( opName, _, opBody)) => + val (opCover, sideComputedMap) = mkCoverInternal( bodyMap, partialMap, Map.empty )( opBody ) + sideComputedMap + ( opName -> opCover ) + } + + def mkCoverEx( bodyMap : BodyMap )( ex : TlaEx, initialCoverMap : operCoverMapType = Map.empty ) : CoverData = + mkCoverInternal( bodyMap, initialCoverMap, Map.empty )( ex )._1 + + private def mkCoverInternal( + bodyMap : BodyMap, + initialOperMap : operCoverMapType, + initialLetInOperBodyMap : operCoverMapType + ) + ( ex: TlaEx ): (CoverData,operCoverMapType) = ex match { /** Recursive case, connectives */ case OperEx( oper, args@_* ) if oper == TlaBoolOper.and || oper == TlaBoolOper.or => /** First, process children */ - val processedChildArgs : Seq[CoverData] = - args.map( mkCoverInternal(initialLetInOperBodyMap) ) + val processedChildArgs : Seq[(CoverData, operCoverMapType)] = + args.map( mkCoverInternal( bodyMap, initialOperMap, initialLetInOperBodyMap ) ) - /** Compute parent cover from children */ + val (childCover,newSideComputedMap) = processedChildArgs.foldLeft( Seq.empty[CoverData], initialOperMap ){ + case ((partialChildren, partialMap), (coverData, map) ) => + (partialChildren :+ coverData, partialMap ++ map) + } - if ( oper == TlaBoolOper.and ) - NonBranch( ex.ID, processedChildArgs:_* ) else - BranchPoint( ex.ID, processedChildArgs : _* ) + /** Compute parent cover from children */ + val parentCover = if ( oper == TlaBoolOper.and ) + NonBranch( ex.ID, childCover:_* ) else + BranchPoint( ex.ID, childCover : _* ) + (parentCover, newSideComputedMap) /** Base case, assignment candidates */ - case OperEx( TlaOper.eq, OperEx( TlaActionOper.prime, NameEx( name ) ), star ) => + case OperEx( TlaOper.eq, OperEx( TlaActionOper.prime, NameEx( name ) ), _ ) => /** it's a candidate for name iff name \notin manuallyAssigned */ - if ( !manuallyAssigned.contains( name ) ) Candidate( name, ex.ID ) else NonCandidate( ex.ID ) - case OperEx( BmcOper.assign, OperEx( TlaActionOper.prime, NameEx( name ) ), star ) => + val cover = if ( !manuallyAssigned.contains( name ) ) Candidate( name, ex.ID ) else NonCandidate( ex.ID ) + (cover, initialOperMap) + + case OperEx( BmcOper.assign, OperEx( TlaActionOper.prime, NameEx( name ) ), _ ) => /** it's a candidate for name iff name \in manuallyAssigned */ - if ( manuallyAssigned.contains( name ) ) Candidate( name, ex.ID ) else NonCandidate( ex.ID ) + val cover = if ( manuallyAssigned.contains( name ) ) Candidate( name, ex.ID ) else NonCandidate( ex.ID ) + (cover, initialOperMap) /** Recursive case, quantifier */ - case OperEx( TlaBoolOper.exists, NameEx( _ ), star, subEx ) => - mkCoverInternal( initialLetInOperBodyMap )( subEx ) + case OperEx( TlaBoolOper.exists, NameEx( _ ), _, subEx ) => + mkCoverInternal( bodyMap, initialOperMap, initialLetInOperBodyMap )( subEx ) - case OperEx( TlaControlOper.ifThenElse, star, thenExpr, elseExpr ) => + case OperEx( TlaControlOper.ifThenElse, _, thenExpr, elseExpr ) => /** Recurse on both branches */ - val thenResults = mkCoverInternal( initialLetInOperBodyMap )(thenExpr) - val elseResults = mkCoverInternal( initialLetInOperBodyMap )(elseExpr) + val (thenCover, thenMap) = mkCoverInternal( bodyMap, initialOperMap, initialLetInOperBodyMap )( thenExpr ) + val (elseCover, elseMap) = mkCoverInternal( bodyMap, initialOperMap, initialLetInOperBodyMap )( elseExpr ) /** Continue as with disjunction */ - BranchPoint( ex.ID, thenResults, elseResults ) + val cover = BranchPoint( ex.ID, thenCover, elseCover ) + (cover, thenMap ++ elseMap) /** Recursive case, nullary LetIn */ case LetInEx( body, defs@_* ) => // Sanity check, all operators must be nullary assert( defs.forall { _.formalParams.isEmpty } ) /** First, analyze the bodies, to reuse later */ - val bodyResults = (defs map { d => - d.name -> mkCoverInternal( initialLetInOperBodyMap )( d.body ) - }).toMap + val (newLetInMap, sideComputedMap) = defs.foldLeft( initialLetInOperBodyMap, initialOperMap ) { + case ((partialLetInMap, partialSideComputation), TlaOperDecl( letInDeclName, _, letInDeclbody )) => + val (cover, newSideComputedMap) = + mkCoverInternal( bodyMap, partialSideComputation, partialLetInMap )( letInDeclbody ) + (partialLetInMap + ( letInDeclName -> cover ), newSideComputedMap) + } /** Then, analyze the body, with the bodyResults map */ - mkCoverInternal( initialLetInOperBodyMap ++ bodyResults )( body ) + mkCoverInternal( bodyMap, sideComputedMap, newLetInMap )( body ) + + /** Application case, user-defined top-level operator */ + case OperEx( TlaOper.apply, NameEx(operName), _* ) if bodyMap.contains( operName ) => + // Assignments cannot appear in arguments to an operator, so we can ignore those + + // We can sometimes leverage memoization: + val preComputedOpt = initialOperMap.get( operName ) + if (preComputedOpt.nonEmpty) + (preComputedOpt.get, initialOperMap) + else { + // If not, we compute the cover and store it + val opBody = bodyMap( operName ).body + val (cover, sideComputedMap) = mkCoverInternal( bodyMap, initialOperMap, initialLetInOperBodyMap )( opBody ) + (cover, sideComputedMap + (operName -> cover)) + } - /** Nullary apply */ + + /** Other apply */ case OperEx( TlaOper.apply, NameEx(operName) ) => // Apply may appear in higher order operators, so it might not be possible to pre-analyze - initialLetInOperBodyMap.getOrElse( operName, NonCandidate( ex.ID ) ) + val cover = initialLetInOperBodyMap.getOrElse( operName, NonCandidate( ex.ID ) ) + (cover, initialOperMap) /** In the other cases, return the default args */ - case _ => NonCandidate( ex.ID ) - } - - def mkCover( ex: TlaEx) : CoverData = { - mkCoverInternal( Map.empty )(ex) + case _ => (NonCandidate( ex.ID ), initialOperMap) } - /** Computes the set of all variables, which are covered by `ex` */ - def coveredVars( ex: TlaEx ) : Set[String] = { - val cd = mkCover(ex) - val potentialProblemMap = (allVariables map { - v => v -> CoverData.uncoveredBranchPoints( v )( cd ) - }).toMap - - - potentialProblemMap.keySet.filter { k => potentialProblemMap(k).noProblem } - - } - - /** Computes a set of assignment candidates under `ex` */ - def assignmentLocaitons( ex: TlaEx ) : Set[Candidate] = { - val cd = mkCover( ex ) - allVariables flatMap { - v => CoverData.uncoveredBranchPoints( v )( cd ).problemUIDs.asgns +// private def mkCoverInternal2( initialLetInOperBodyMap : operCoverMapType ) +// ( ex: TlaEx ): CoverData = ex match { +// /** Recursive case, connectives */ +// case OperEx( oper, args@_* ) if oper == TlaBoolOper.and || oper == TlaBoolOper.or => +// +// /** First, process children */ +// val processedChildArgs : Seq[CoverData] = +// args.map( mkCoverInternal2(initialLetInOperBodyMap) ) +// +// /** Compute parent cover from children */ +// +// if ( oper == TlaBoolOper.and ) +// NonBranch( ex.ID, processedChildArgs:_* ) else +// BranchPoint( ex.ID, processedChildArgs : _* ) +// +// +// /** Base case, assignment candidates */ +// case OperEx( TlaOper.eq, OperEx( TlaActionOper.prime, NameEx( name ) ), star ) => +// /** it's a candidate for name iff name \notin manuallyAssigned */ +// if ( !manuallyAssigned.contains( name ) ) Candidate( name, ex.ID ) else NonCandidate( ex.ID ) +// case OperEx( BmcOper.assign, OperEx( TlaActionOper.prime, NameEx( name ) ), star ) => +// /** it's a candidate for name iff name \in manuallyAssigned */ +// if ( manuallyAssigned.contains( name ) ) Candidate( name, ex.ID ) else NonCandidate( ex.ID ) +// +// /** Recursive case, quantifier */ +// case OperEx( TlaBoolOper.exists, NameEx( _ ), star, subEx ) => +// mkCoverInternal2( initialLetInOperBodyMap )( subEx ) +// +// case OperEx( TlaControlOper.ifThenElse, star, thenExpr, elseExpr ) => +// /** Recurse on both branches */ +// val thenResults = mkCoverInternal2( initialLetInOperBodyMap )(thenExpr) +// val elseResults = mkCoverInternal2( initialLetInOperBodyMap )(elseExpr) +// +// /** Continue as with disjunction */ +// BranchPoint( ex.ID, thenResults, elseResults ) +// +// /** Recursive case, nullary LetIn */ +// case LetInEx( body, defs@_* ) => +// // Sanity check, all operators must be nullary +// assert( defs.forall { _.formalParams.isEmpty } ) +// /** First, analyze the bodies, to reuse later */ +// val bodyResults = (defs map { d => +// d.name -> mkCoverInternal2( initialLetInOperBodyMap )( d.body ) +// }).toMap +// +// /** Then, analyze the body, with the bodyResults map */ +// mkCoverInternal2( initialLetInOperBodyMap ++ bodyResults )( body ) +// +// /** Nullary apply */ +// case OperEx( TlaOper.apply, NameEx(operName) ) => +// // Apply may appear in higher order operators, so it might not be possible to pre-analyze +// initialLetInOperBodyMap.getOrElse( operName, NonCandidate( ex.ID ) ) +// +// /** In the other cases, return the default args */ +// case _ => NonCandidate( ex.ID ) +// } +// +// def mkCover2( ex: TlaEx) : CoverData = { +// mkCoverInternal2( Map.empty )(ex) +// } + + /** Computes the set of all variables, which are covered by each operator */ + def coveredVars( coverMap: operCoverMapType ) : Map[ String, Set[String]] = { + coverMap map { + case (opName, cover) => opName -> + allVariables.filter( + v => CoverData.uncoveredBranchPoints( v )( cover ).noProblem + ) } - } - def findProblems( ex: TlaEx ): Option[Map[ String, ProblemData ]] = { - val cd = mkCover(ex) - - val potentialProblemMap = (allVariables map { - v => v -> CoverData.uncoveredBranchPoints( v )( cd ) - }).toMap - - - val problemMap = potentialProblemMap.filter{ case (k,v) => !v.noProblem } + } - if (problemMap.isEmpty) { - None - } else { - Some( problemMap ) - } + /** Computes a set of assignment candidates under each operator */ + def assignmentLocaitons( coverMap: operCoverMapType ) : Map[String, Set[Candidate]] = + coverMap map { + case (opName, cover) => opName -> + allVariables.flatMap( + v => CoverData.uncoveredBranchPoints( v )( cover ).problemUIDs.asgns + ) } + } diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala index b31e687c46..2988644935 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala @@ -44,15 +44,14 @@ class CoverAnalysisPassImpl @Inject()(options: PassOptions, ManualAssignments.findAll( initBody ) ++ ManualAssignments.findAll( nextBody ) val coverChecker = new CoverChecker(varSet, manualAssignments) - logger.info(s" > Computing assignment cover for $nextName") - val mustCoverMap = bodyMap map { case (opName, TlaOperDecl( _, _, body )) => - // technically suboptimal, since the same CoverData is computed multiple times, - // but no need to change it if it doesn't impact runtime - opName -> coverChecker.coveredVars( body ) - } + logger.info(s" > Computing assignment cover") + val coverMap = coverChecker.mkCover( bodyMap ) + + val mustCoverMap = coverChecker.coveredVars( coverMap ) + // we compute assignment witnesses - val asgns = - coverChecker.assignmentLocaitons( nextBody ) ++ coverChecker.assignmentLocaitons( initBody ) + val asgnMap = coverChecker.assignmentLocaitons( coverMap ) + val asgns = asgnMap( nextName ) ++ asgnMap( initPrimedName ) val outdir = options.getOrError("io", "outdir").asInstanceOf[Path] val outFile = new File(outdir.toFile, "out-cover.txt") @@ -128,12 +127,19 @@ class CoverAnalysisPassImpl @Inject()(options: PassOptions, // for Init we know any updates appear only in InitPrime val initPrimeNameCorrection = if (opName == initName) initPrimedName else opName val mustVars = mustCoverMap.getOrElse( initPrimeNameCorrection, Set.empty ) + // Because of the order of terms, may-update witnesses sometimes do not include variables + // computed by must analysis. + // For example: A == x' = 1, B == x' = 2 /\ y' = 3, Next == A /\ B + // The may-analysis would only list that A may update x, but not B. Because A must update x + // we don't need to present the fact that B must also update x to the user, so we filter the must-variables + // by the may-variables for presentation purposes + val filtered = mustVars.intersect( mayCoverMap( opName ) ) // if there are no guaranteed vars we don't want any output val mustStrOpt = - if (mustVars.isEmpty) + if (filtered.isEmpty) None else - Some( formatStringMust.format( loc.toString, opName, sortedVarString(mustVars) ) ) + Some( formatStringMust.format( loc.toString, opName, sortedVarString(filtered) ) ) val notGuaranteed = mayCoverMap(opName) -- mustVars // Similarly, we only want to see a warning if `notGuaranteed` is nonempty val warningOpt = diff --git a/tla-assignments/src/test/scala/at/forsyte/apalache/tla/assignments/TestCover.scala b/tla-assignments/src/test/scala/at/forsyte/apalache/tla/assignments/TestCover.scala index 92fee617b1..4f087e5774 100644 --- a/tla-assignments/src/test/scala/at/forsyte/apalache/tla/assignments/TestCover.scala +++ b/tla-assignments/src/test/scala/at/forsyte/apalache/tla/assignments/TestCover.scala @@ -82,7 +82,7 @@ class TestCover extends FunSuite with TestingPredefs { ) val checker = new CoverChecker( Set( "x" ) ) - val cover = checker.mkCover( ex ) + val cover = checker.mkCoverEx( Map.empty )( ex ) assert( CoverData.uncoveredBranchPoints( "x" )( cover ).noProblem ) @@ -113,7 +113,7 @@ class TestCover extends FunSuite with TestingPredefs { val vars = Set( "x", "y" ) val checker = new CoverChecker( vars ) - val cover = checker.mkCover( ex ) + val cover = checker.mkCoverEx( Map.empty )( ex ) assert( CoverData.uncoveredBranchPoints( "y" )( cover ).noProblem ) diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerModule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerModule.scala index 53d3ee9c56..e9f4dafa2e 100644 --- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerModule.scala +++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerModule.scala @@ -64,23 +64,29 @@ class CheckerModule extends AbstractModule { bind(classOf[Pass]) .annotatedWith(Names.named("AfterConfiguration")) .to(classOf[UnrollPass]) - // the next pass is InlinePass - bind(classOf[InlinePass]) - .to(classOf[InlinePassImpl]) - bind(classOf[Pass]) - .annotatedWith(Names.named("AfterUnroll")) - .to(classOf[InlinePass]) // the next pass is PrimingPass bind(classOf[PrimingPass]) .to(classOf[PrimingPassImpl]) bind(classOf[Pass]) - .annotatedWith(Names.named("AfterInline")) + .annotatedWith(Names.named("AfterUnroll")) .to(classOf[PrimingPass]) + // the next pass is CoverAnalysisPass + bind(classOf[CoverAnalysisPass]) + .to(classOf[CoverAnalysisPassImpl]) + bind(classOf[Pass]) + .annotatedWith(Names.named("AfterPriming")) + .to(classOf[CoverAnalysisPass]) + // the next pass is InlinePass + bind(classOf[InlinePass]) + .to(classOf[InlinePassImpl]) + bind(classOf[Pass]) + .annotatedWith(Names.named("AfterCoverAnalysis")) + .to(classOf[InlinePass]) // the next pass is VCGenPass bind(classOf[VCGenPass]) .to(classOf[VCGenPassImpl]) bind(classOf[Pass]) - .annotatedWith(Names.named("AfterPriming")) + .annotatedWith(Names.named("AfterInline")) .to(classOf[VCGenPass]) // the next pass after SanyParserPass is PreproPass bind(classOf[PreproPass]) @@ -88,17 +94,11 @@ class CheckerModule extends AbstractModule { bind(classOf[Pass]) .annotatedWith(Names.named("AfterVCGen")) .to(classOf[PreproPass]) - // the next pass after PreproPass is CoverAnalysisPass - bind(classOf[CoverAnalysisPass]) - .to(classOf[CoverAnalysisPassImpl]) - bind(classOf[Pass]) - .annotatedWith(Names.named("AfterPrepro")) - .to(classOf[CoverAnalysisPass]) // the next pass after CoverAnalysisPass is AssignmentPass bind(classOf[TransitionPass]) .to(classOf[TransitionPassImpl]) bind(classOf[Pass]) - .annotatedWith(Names.named("AfterCoverAnalysis")) + .annotatedWith(Names.named("AfterPrepro")) .to(classOf[TransitionPass]) // the next pass after AssignmentPass is AnalysisPass bind(classOf[OptPass]) From 7bce81bbbe8a57b29c45dc68b00ef01208e31d3b Mon Sep 17 00:00:00 2001 From: Kukovec Date: Thu, 29 Oct 2020 15:54:10 +0100 Subject: [PATCH 3/5] Forgot to delete comments --- .../tla/assignments/CoverChecker.scala | 61 ------------------- .../passes/CoverAnalysisPassImpl.scala | 1 - 2 files changed, 62 deletions(-) diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala index 9c26b7ee77..43da15abe6 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala @@ -116,67 +116,6 @@ class CoverChecker( allVariables: Set[String], manuallyAssigned: Set[String] = S } -// private def mkCoverInternal2( initialLetInOperBodyMap : operCoverMapType ) -// ( ex: TlaEx ): CoverData = ex match { -// /** Recursive case, connectives */ -// case OperEx( oper, args@_* ) if oper == TlaBoolOper.and || oper == TlaBoolOper.or => -// -// /** First, process children */ -// val processedChildArgs : Seq[CoverData] = -// args.map( mkCoverInternal2(initialLetInOperBodyMap) ) -// -// /** Compute parent cover from children */ -// -// if ( oper == TlaBoolOper.and ) -// NonBranch( ex.ID, processedChildArgs:_* ) else -// BranchPoint( ex.ID, processedChildArgs : _* ) -// -// -// /** Base case, assignment candidates */ -// case OperEx( TlaOper.eq, OperEx( TlaActionOper.prime, NameEx( name ) ), star ) => -// /** it's a candidate for name iff name \notin manuallyAssigned */ -// if ( !manuallyAssigned.contains( name ) ) Candidate( name, ex.ID ) else NonCandidate( ex.ID ) -// case OperEx( BmcOper.assign, OperEx( TlaActionOper.prime, NameEx( name ) ), star ) => -// /** it's a candidate for name iff name \in manuallyAssigned */ -// if ( manuallyAssigned.contains( name ) ) Candidate( name, ex.ID ) else NonCandidate( ex.ID ) -// -// /** Recursive case, quantifier */ -// case OperEx( TlaBoolOper.exists, NameEx( _ ), star, subEx ) => -// mkCoverInternal2( initialLetInOperBodyMap )( subEx ) -// -// case OperEx( TlaControlOper.ifThenElse, star, thenExpr, elseExpr ) => -// /** Recurse on both branches */ -// val thenResults = mkCoverInternal2( initialLetInOperBodyMap )(thenExpr) -// val elseResults = mkCoverInternal2( initialLetInOperBodyMap )(elseExpr) -// -// /** Continue as with disjunction */ -// BranchPoint( ex.ID, thenResults, elseResults ) -// -// /** Recursive case, nullary LetIn */ -// case LetInEx( body, defs@_* ) => -// // Sanity check, all operators must be nullary -// assert( defs.forall { _.formalParams.isEmpty } ) -// /** First, analyze the bodies, to reuse later */ -// val bodyResults = (defs map { d => -// d.name -> mkCoverInternal2( initialLetInOperBodyMap )( d.body ) -// }).toMap -// -// /** Then, analyze the body, with the bodyResults map */ -// mkCoverInternal2( initialLetInOperBodyMap ++ bodyResults )( body ) -// -// /** Nullary apply */ -// case OperEx( TlaOper.apply, NameEx(operName) ) => -// // Apply may appear in higher order operators, so it might not be possible to pre-analyze -// initialLetInOperBodyMap.getOrElse( operName, NonCandidate( ex.ID ) ) -// -// /** In the other cases, return the default args */ -// case _ => NonCandidate( ex.ID ) -// } -// -// def mkCover2( ex: TlaEx) : CoverData = { -// mkCoverInternal2( Map.empty )(ex) -// } - /** Computes the set of all variables, which are covered by each operator */ def coveredVars( coverMap: operCoverMapType ) : Map[ String, Set[String]] = { coverMap map { diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala index 2988644935..12c40f7098 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala @@ -8,7 +8,6 @@ import at.forsyte.apalache.tla.assignments.{CoverChecker, ManualAssignments} import at.forsyte.apalache.tla.imp.findBodyOf import at.forsyte.apalache.tla.imp.src.SourceStore import at.forsyte.apalache.tla.lir.storage.{BodyMapFactory, ChangeListener, SourceLocator} -import at.forsyte.apalache.tla.lir.TlaOperDecl import at.forsyte.apalache.tla.lir.src.SourceLocation import at.forsyte.apalache.tla.lir.transformations.TransformationTracker import com.google.inject.Inject From 8938a825d5dfe740c71b176b6de51b14e2dc8a59 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Thu, 29 Oct 2020 16:06:31 +0100 Subject: [PATCH 4/5] Exception fixes --- .../apalache/tla/assignments/CoverChecker.scala | 2 -- .../tla/assignments/passes/CoverAnalysisPassImpl.scala | 10 +++++++--- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala index 43da15abe6..d0424e3b63 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala @@ -76,8 +76,6 @@ class CoverChecker( allVariables: Set[String], manuallyAssigned: Set[String] = S /** Recursive case, nullary LetIn */ case LetInEx( body, defs@_* ) => - // Sanity check, all operators must be nullary - assert( defs.forall { _.formalParams.isEmpty } ) /** First, analyze the bodies, to reuse later */ val (newLetInMap, sideComputedMap) = defs.foldLeft( initialLetInOperBodyMap, initialOperMap ) { case ((partialLetInMap, partialSideComputation), TlaOperDecl( letInDeclName, _, letInDeclbody )) => diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala index 12c40f7098..49a1b40f10 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala @@ -104,8 +104,8 @@ class CoverAnalysisPassImpl @Inject()(options: PassOptions, } // For nicer formatting, we compute the max width for the source and name fields - val longestLoc = outTriples.map( _._1.length ).max - val longestOpName = outTriples.map( _._2.length ).max + val longestLoc = if (outTriples.isEmpty) 0 else outTriples.map( _._1.length ).max + val longestOpName = if (outTriples.isEmpty) 0 else outTriples.map( _._2.length ).max val formatStringMay = s"%-${longestLoc}s: %${longestOpName}s may update %s" val formatStringMust = s"%-${longestLoc}s: %${longestOpName}s always updates: %s" @@ -120,7 +120,11 @@ class CoverAnalysisPassImpl @Inject()(options: PassOptions, // The second part of the output lists, for each operator, all variables it must update (if any) // and a warning for each variable that may be updated but is not guaranteed to be updated - val outStrMustWarning = mayCoverMap.keySet.toList.sortBy( k => opLocs(k).get) flatMap { opName: String => + + // TODO: All operators should have trackable locations, but some other bug is causing lookup errors here. + // For now, the code will filter out all operators for which source is unavailable. + val operatorsWithLocs = mayCoverMap.keySet.toList.filter( k => opLocs(k).nonEmpty ) + val outStrMustWarning = operatorsWithLocs.sortBy( k => opLocs(k).get) flatMap { opName: String => val locOpt = opLocs(opName) locOpt map { loc => // for Init we know any updates appear only in InitPrime From d24161758cc6749e2851daef1b839733b6bb9ce5 Mon Sep 17 00:00:00 2001 From: Kukovec Date: Thu, 29 Oct 2020 16:10:22 +0100 Subject: [PATCH 5/5] Bad constant choice --- .../tla/assignments/passes/CoverAnalysisPassImpl.scala | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala index 49a1b40f10..12f4326286 100644 --- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala +++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala @@ -104,8 +104,8 @@ class CoverAnalysisPassImpl @Inject()(options: PassOptions, } // For nicer formatting, we compute the max width for the source and name fields - val longestLoc = if (outTriples.isEmpty) 0 else outTriples.map( _._1.length ).max - val longestOpName = if (outTriples.isEmpty) 0 else outTriples.map( _._2.length ).max + val longestLoc = if (outTriples.isEmpty) 1 else outTriples.map( _._1.length ).max + val longestOpName = if (outTriples.isEmpty) 1 else outTriples.map( _._2.length ).max val formatStringMay = s"%-${longestLoc}s: %${longestOpName}s may update %s" val formatStringMust = s"%-${longestLoc}s: %${longestOpName}s always updates: %s"