Merge pull request #823 from viperproject/meilers_flexible_more_joins

More flexible moreJoins

Author: marcoeilers

src/main/scala/Config.scala

@@ -668,9 +668,10 @@ class Config(args: Seq[String]) extends SilFrontendConfig(args, "Silicon") {
     noshort = true
   )
 
-  val moreJoins: ScallopOption[Boolean] = opt[Boolean]("moreJoins",
-    descr = "Enable more joins using a more complete implementation of state merging.",
-    default = Some(false),
+  val moreJoins: ScallopOption[Int] = opt[Int]("moreJoins",
+    descr = "Enable more joins using a more complete implementation of state merging. " +
+      "0 = off, 1 = don't branch on impure conditionals, 2 = join all branches when possible.",
+    default = Some(0),
     noshort = true
   )
 

src/main/scala/rules/Brancher.scala

@@ -244,7 +244,8 @@ object brancher extends BranchingRules {
       v.decider.prover.comment(s"Bulk-declaring functions")
       v.decider.declareAndRecordAsFreshFunctions(functionsOfElseBranchDecider, true)
       v.decider.prover.comment(s"Bulk-declaring macros")
-      v.decider.declareAndRecordAsFreshMacros(macrosOfElseBranchDecider, true)
+      // Declare macros without duplicates; we keep only the last occurrence of every declaration to avoid errors.
+      v.decider.declareAndRecordAsFreshMacros(macrosOfElseBranchDecider.reverse.distinct.reverse, true)
     }
     res
   }

src/main/scala/rules/Consumer.scala

@@ -183,7 +183,7 @@ object consumer extends ConsumptionRules {
       v.logger.debug("hR = " + s.reserveHeaps.map(v.stateFormatter.format).mkString("", ",\n     ", ""))
 
     val consumed = a match {
-      case imp @ ast.Implies(e0, a0) if !a.isPure && s.moreJoins =>
+      case imp @ ast.Implies(e0, a0) if !a.isPure && s.moreJoins > 0 =>
         val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "consume")
         val uidImplies = v.symbExLog.openScope(impliesRecord)
         consumeConditionalTlcMoreJoins(s, h, e0, a0, None, uidImplies, pve, v)(Q)
@@ -203,7 +203,7 @@ object consumer extends ConsumptionRules {
               Q(s2, h, Unit, v2)
             }))
 
-      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && s.moreJoins =>
+      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && s.moreJoins > 0 =>
         val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "consume")
         val uidCondExp = v.symbExLog.openScope(condExpRecord)
         consumeConditionalTlcMoreJoins(s, h, e0, a1, Some(a2), uidCondExp, pve, v)(Q)
@@ -507,7 +507,7 @@ object consumer extends ConsumptionRules {
               // Asume that entry1.pcs is inverse of entry2.pcs
               Ite(And(entry1.pathConditions.branchConditions), entry1.data._2, entry2.data._2)
             )
-            (entry1.pathConditionAwareMerge(entry2, v1), mergedData)
+            (entry1.pathConditionAwareMergeWithoutConsolidation(entry2, v1), mergedData)
           case _ =>
             sys.error(s"Unexpected join data entries: $entries")
         }

src/main/scala/rules/Evaluator.scala

@@ -785,7 +785,7 @@ object evaluator extends EvaluationRules {
                                  * incomplete).
                                  */
                              smDomainNeeded = true,
-                             moreJoins = false)
+                             moreJoins = 0)
             consumes(s3, pres, _ => pvePre, v2)((s4, snap, v3) => {
               val snap1 = snap.convert(sorts.Snap)
               val preFApp = App(functionSupporter.preconditionVersion(v3.symbolConverter.toFunction(func)), snap1 :: tArgs)

src/main/scala/rules/Executor.scala

@@ -111,7 +111,7 @@ object executor extends ExecutionRules {
       case (Seq(), _) => Q(s, v)
       case (Seq(edge), _) => follow(s, edge, v, joinPoint)(Q)
       case (Seq(edge1, edge2), Some(newJoinPoint)) if
-          s.moreJoins &&
+          s.moreJoins > 1 &&
           // Can't directly match type because of type erasure ...
           edge1.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&
           edge2.isInstanceOf[ConditionalEdge[ast.Stmt, ast.Exp]] &&

src/main/scala/rules/Joiner.scala

@@ -21,6 +21,10 @@ case class JoinDataEntry[D](s: State, data: D, pathConditions: RecordedPathCondi
     val res = State.merge(this.s, this.pathConditions, other.s, other.pathConditions)
     v.stateConsolidator.consolidate(res, v)
   }
+
+  def pathConditionAwareMergeWithoutConsolidation(other: JoinDataEntry[D], v: Verifier): State = {
+    State.merge(this.s, this.pathConditions, other.s, other.pathConditions)
+  }
 }
 
 trait JoiningRules extends SymbolicExecutionRules {

src/main/scala/rules/Producer.scala

@@ -214,7 +214,7 @@ object producer extends ProductionRules {
       continuation(if (state.exhaleExt) state.copy(reserveHeaps = state.h +: state.reserveHeaps.drop(1)) else state, verifier)
 
     val produced = a match {
-      case imp @ ast.Implies(e0, a0) if !a.isPure && s.moreJoins =>
+      case imp @ ast.Implies(e0, a0) if !a.isPure && s.moreJoins > 0 =>
         val impliesRecord = new ImpliesRecord(imp, s, v.decider.pcs, "produce")
         val uidImplies = v.symbExLog.openScope(impliesRecord)
 
@@ -240,7 +240,7 @@ object producer extends ProductionRules {
               case Seq(entry) => // One branch is dead
                 entry.s
               case Seq(entry1, entry2) => // Both branches are alive
-                entry1.pathConditionAwareMerge(entry2, v1)
+                entry1.pathConditionAwareMergeWithoutConsolidation(entry2, v1)
               case _ =>
                 sys.error(s"Unexpected join data entries: $entries")}
             (s2, null)
@@ -267,7 +267,7 @@ object producer extends ProductionRules {
                 Q(s2, v2)
             }))
 
-      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && s.moreJoins =>
+      case ite @ ast.CondExp(e0, a1, a2) if !a.isPure && s.moreJoins > 0=>
         val condExpRecord = new CondExpRecord(ite, s, v.decider.pcs, "produce")
         val uidCondExp = v.symbExLog.openScope(condExpRecord)
 

src/main/scala/state/State.scala

@@ -71,7 +71,7 @@ final case class State(g: Store = Store(),
                        /* ast.Field, ast.Predicate, or MagicWandIdentifier */
                        heapDependentTriggers: InsertionOrderedSet[Any] = InsertionOrderedSet.empty,
                        moreCompleteExhale: Boolean = false,
-                       moreJoins: Boolean = false)
+                       moreJoins: Int = 0)
     extends Mergeable[State] {
 
   val isMethodVerification: Boolean = {

src/main/scala/verifier/DefaultMainVerifier.scala

@@ -323,10 +323,28 @@ class DefaultMainVerifier(config: Config,
       case _ => Verifier.config.exhaleMode == ExhaleMode.MoreComplete
     }
     val moreJoinsAnnotated = member.info.getUniqueInfo[ast.AnnotationInfo] match {
-      case Some(ai) => ai.values.contains("moreJoins")
-      case _ => false
+      case Some(ai) if ai.values.contains("moreJoins") =>
+        ai.values("moreJoins") match {
+          case Seq() => Some(2)
+          case Seq(vl) =>
+            try {
+              Some(vl.toInt)
+            } catch {
+              case _: NumberFormatException =>
+                reporter report AnnotationWarning(s"Member ${member.name} has invalid moreJoins annotation value $vl. Annotation will be ignored.")
+                None
+            }
+          case v =>
+            reporter report AnnotationWarning(s"Member ${member.name} has invalid moreJoins annotation value $v. Annotation will be ignored.")
+            None
+        }
+      case _ => None
+    }
+    val moreJoins = if (member.isInstanceOf[ast.Method]) {
+      moreJoinsAnnotated.getOrElse(Verifier.config.moreJoins.getOrElse(0))
+    } else {
+      0
     }
-    val moreJoins = (Verifier.config.moreJoins() || moreJoinsAnnotated) && member.isInstanceOf[ast.Method]
 
     val methodPermCache = mutable.HashMap[String, InsertionOrderedSet[ast.Location]]()
     val permResources: InsertionOrderedSet[ast.Location] = if (Verifier.config.unsafeWildcardOptimization()) member match {

src/test/scala/SiliconTestsMoreJoins.scala

@@ -19,6 +19,6 @@ class SiliconTestsMoreJoins extends SiliconTests {
 
   override val commandLineArguments: Seq[String] = Seq(
     "--timeout", "300" /* seconds */,
-    "--moreJoins"
+    "--moreJoins=2"
   )
 }