Assignment cover analysis (#261)

* Cover checker

* Added CoverAnalysisPass

* Updated test syntax

* IntPrime check + error msg

tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverChecker.scala

@@ -0,0 +1,109 @@
+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 scala.collection.immutable.{Map, Set}
+
+/**
+  * Checks to see whether a specifications satisfies the covering property, i.e. whether
+  * there exists at least one assignment candidate for each variable in `variables`
+  * on each branch.
+  */
+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 {
+    /** 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) )
+
+      /** 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 ) =>
+      mkCoverInternal( initialLetInOperBodyMap )( subEx )
+
+    case OperEx( TlaControlOper.ifThenElse, star, thenExpr, elseExpr ) =>
+      /** Recurse on both branches */
+      val thenResults = mkCoverInternal( initialLetInOperBodyMap )(thenExpr)
+      val elseResults = mkCoverInternal( 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 -> mkCoverInternal( initialLetInOperBodyMap )( d.body )
+      }).toMap
+
+      /** Then, analyze the body, with the bodyResults map */
+      mkCoverInternal( 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 mkCover( ex: TlaEx) : CoverData = {
+    mkCoverInternal( Map.empty )(ex)
+  }
+
+  /** 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 }
+
+  }
+
+  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 )
+    }
+
+  }
+}

tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/CoverData.scala

@@ -0,0 +1,117 @@
+package at.forsyte.apalache.tla.assignments
+
+import at.forsyte.apalache.tla.lir.UID
+
+/**
+  * CoveringData is a tree structure, detailing branch points in a TLA+ specification.
+  * Each ITE or \/, not belonging to a star-expression, constitutes a branch-point, i.e.
+  * each of its child-expressions will belong to a different branch.
+  */
+class CoverData( uid: UID )
+sealed case class BranchPoint( uid: UID, branches: CoverData* ) extends CoverData(uid)
+sealed case class NonBranch( uid: UID, elements: CoverData* ) extends CoverData(uid)
+sealed case class Candidate( varName: String, uid: UID ) extends CoverData(uid)
+sealed case class NonCandidate( uid: UID ) extends CoverData(uid)
+
+object CoverData{
+
+  class CoverException( s : String ) extends Exception( s )
+
+  class IncompleteCover(seq: Seq[UID]) {
+    def get: Seq[UID] = seq
+    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 )
+
+  /**
+    * ProblemData represents potential witnesses to cover violations.
+    * The collection `problemUIDs` lists the largest subexpressions (by UID), which
+    * witness cover violation, relative to the expression from which ProblemData
+    * is computed. The map `blameMap` allows us to find more fine-grained violations;
+    * if a value k in `problemUIDs` is a key in `blameMap`, a value v, that k maps to, is
+    * the value of `problemUIDs`, taking the expression corresponding to k
+    * as the root of computation.
+    */
+  sealed case class ProblemData(
+                                 problemUIDs: IncompleteCover,
+                                 blameMap: Map[UID, IncompleteCover]
+                               ) {
+    /** Checks if any witnesses exist */
+    def noProblem: Boolean = problemUIDs.isEmpty && blameMap.isEmpty
+
+    /**
+      * If an expression e labeled with `uid` is a witness, we can attempt to
+      * find a subexpression of e, which is a "better" (smaller) witness,
+      * by tracing `blameMap`
+      */
+    def focusOn( uid: UID ): Option[ProblemData] =
+        blameMap.get( uid ) map { ic =>
+          ProblemData( ic, blameMap )
+        }
+
+    /**
+      * Enumerates all possible ways to refine witnesses.
+      */
+    def focusCandidates: Seq[ProblemData] = problemUIDs.get flatMap focusOn
+
+  }
+
+  def uncoveredBranchPoints( varName: String )( cd: CoverData ) : ProblemData = cd match {
+    case Candidate( v, loc ) =>
+      // Candidate(v, _) covers varName iff v == varName
+      val problem = if ( varName == v ) NoProblem() else AtLeastOne( Seq( loc ) )
+      ProblemData( problem, Map.empty )
+    case NonCandidate( loc ) =>
+      // NonCandidate never covers varname, but is also a leaf in blameMap
+      ProblemData( AtLeastOne( Seq( loc ) ), 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 ) ) {
+          case (pd,brCd) =>
+            val brPd = uncoveredBranchPoints( varName )( brCd )
+            ProblemData(
+              All( pd.problemUIDs.get ++ brPd.problemUIDs.get ),
+              pd.blameMap ++ brPd.blameMap
+            )
+        }
+
+      if (!branchIssues.problemUIDs.isEmpty){
+        // 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 ) ),
+          branchIssues.blameMap + ( loc -> branchIssues.problemUIDs )
+        )
+      } else {
+        branchIssues
+      }
+
+    case NonBranch( loc, elements@_* ) =>
+      // 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 ) ) {
+        // If a suitable cover is found, report NoProblem
+        ProblemData( NoProblem(), Map.empty )
+      } else {
+        // Otherwise, no sub-expression covers varName, so we aggregate all sub-locations
+        val problemAggregate = elemIssues.foldLeft( ProblemData( NoProblem(), Map.empty ) ) {
+          case (pd,brPd) =>
+            ProblemData(
+              AtLeastOne( pd.problemUIDs.get ++ brPd.problemUIDs.get),
+              pd.blameMap ++ brPd.blameMap
+            )
+        }
+        // Then, NonBranch sets itself as a problem location, as in the previous case
+        ProblemData(
+          AtLeastOne( Seq( loc ) ),
+          problemAggregate.blameMap + ( loc -> problemAggregate.problemUIDs )
+        )
+      }
+  }
+
+}

tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPass.scala

@@ -0,0 +1,9 @@
+package at.forsyte.apalache.tla.assignments.passes
+
+
+import at.forsyte.apalache.infra.passes.{Pass, TlaModuleMixin}
+
+/**
+  * CoverAnalysisPass reports, on a per-operator basis, which variables are covered within the body of the operator.
+  */
+trait CoverAnalysisPass extends Pass with TlaModuleMixin

tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/CoverAnalysisPassImpl.scala

@@ -0,0 +1,85 @@
+package at.forsyte.apalache.tla.assignments.passes
+
+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.imp.findBodyOf
+import at.forsyte.apalache.tla.lir.storage.BodyMapFactory
+import at.forsyte.apalache.tla.lir.TlaOperDecl
+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,
+                                      tracker: TransformationTracker,
+                                      @Named("AfterCoverAnalysis") nextPass: Pass with TlaModuleMixin )
+  extends CoverAnalysisPass with LazyLogging {
+
+  override def name: String = "CoverAnalysisPass"
+
+  override def execute(): Boolean = {
+    val inModule = tlaModule.get
+
+    val operDecls = inModule.operDeclarations
+    val varSet = inModule.varDeclarations.map(_.name).toSet
+
+    val bodyMap = BodyMapFactory.makeFromDecls(operDecls)
+
+    val initName = options.getOrElse("checker", "init", "Init")
+    val initPrimedName = initName + "Primed"
+    val nextName = options.getOrElse("checker", "next", "Next")
+
+    // We check for manual assignments in InitPrime and Next
+    val initBody= findBodyOf(initPrimedName, inModule.declarations: _*)
+    val nextBody = findBodyOf(nextName, inModule.declarations: _*)
+
+    val manualAssignments =
+      ManualAssignments.findAll( initBody ) ++ ManualAssignments.findAll( nextBody )
+    val coverChecker = new CoverChecker(varSet, manualAssignments)
+
+    logger.info(s"  > Computing assignment cover for $nextName")
+    val coverMap = 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
+    }
+
+    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 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
+  }
+
+  /**
+    * Get the next pass in the chain. What is the next pass is up
+    * to the module configuration and the pass outcome.
+    *
+    * @return the next pass, if exists, or None otherwise
+    */
+  override def next(): Option[Pass] = {
+    tlaModule map { m =>
+      nextPass.setModule(m)
+      nextPass
+    }
+  }
+
+
+}

tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/passes/TransitionPassImpl.scala

@@ -90,9 +90,11 @@ class TransitionPassImpl @Inject()(options: PassOptions,
     val primedName = findBodyOf(inOperName, module.declarations: _*)
     val vars = module.varDeclarations.map(_.name)
 
+    val sourceLoc = SourceLocator(sourceStore.makeSourceMap, changeListener)
+
     val transitionPairs = SymbolicTransitionExtractor(tracker)(vars, primedName)
     // sort the transitions by their occurrence in the source code
-    val sorter = new TransitionOrder(SourceLocator(sourceStore.makeSourceMap, changeListener))
+    val sorter = new TransitionOrder( sourceLoc )
     val sortedPairs = sorter.sortBySource(transitionPairs)
     if (sortedPairs.isEmpty) {
       throw new AssignmentException("Failed to find assignments and symbolic transitions in " + inOperName)