Make Boolean inst op more precise when writing within range

zafer-esen · Mar 13, 2024 · 917a13b · 917a13b
1 parent 4b40c9a
commit 917a13b
Show file tree

Hide file tree

Showing 3 changed files with 63 additions and 28 deletions.
diff --git a/...bs/horn/extendedquantifiers/instrumentationoperators/BooleanInstrumentationOperator.scala b/...bs/horn/extendedquantifiers/instrumentationoperators/BooleanInstrumentationOperator.scala
@@ -45,9 +45,25 @@ import lazabs.prover.PrincessWrapper.expr2Formula
 import scala.collection.mutable.ArrayBuffer
 
 /**
+ *
  * An instrumentation operator for forall and exists.
+ *@param exq                              The extended quantifier theory.
+ *@param doNotResetWithinBoundsCondition  If a store is made within the tracked
+ *                                        range, normally the range is reset
+ *                                        unless the extended quantifier is
+ *                                        cancellative. If the quantifier is
+ *                                        non-cancellative, then this parameter
+ *                                        can be passed to not reset the range
+ *                                        if the current value satisfies a
+ *                                        condition. Example: for forall, if the
+ *                                        aggregate value is true, we do not need
+ *                                        to reset on a write. Converse for exists.
+ *                                        I.e., for forall  expr2Formula(arg)
+ *                                          and for exists !expr2Formula(arg)
  */
-class BooleanInstrumentationOperator(exq : ExtendedQuantifierWithPredicate)
+class BooleanInstrumentationOperator(
+  exq                             : ExtendedQuantifierWithPredicate,
+  doNotResetWithinBoundsCondition : Option[ITerm => IFormula])
     extends InstrumentationOperator(exq) {
   // Extended quantifier ghost variables.
   case object GhLo     extends GhostVar(exq.arrayIndexSort, "gLo")
@@ -253,17 +269,25 @@ class BooleanInstrumentationOperator(exq : ExtendedQuantifierWithPredicate)
       val storeAbove =
         (newRes === exq.reduceOp(oldRes, pred(o, i, alienSubstMap))) &
           (newHi === i + 1 & newLo === oldLo)
-      val storeInside =
-        exq.invReduceOp match {
-          case Some(f) =>
-            newRes === exq.reduceOp(
-              f(oldRes, exq.arrayTheory.select(a1, i)),
-              pred(o, i, alienSubstMap)) &
-            newLo === oldLo & newHi === oldHi
-          case _ =>
-            storeEmptySeq
-        }
-        val storeOutside = storeEmptySeq
+      val storeInside = exq.invReduceOp match {
+        case Some(f) =>
+          newRes === exq.reduceOp(
+            f(oldRes, exq.arrayTheory.select(a1, i)),
+            pred(o, i, alienSubstMap)) &
+          newLo === oldLo & newHi === oldHi
+        case None =>
+          doNotResetWithinBoundsCondition match {
+            case Some(f) =>
+              ite(f(oldRes),
+                  newRes === exq.reduceOp(oldRes, pred(o, i, alienSubstMap)) &
+                    newLo === oldLo & newHi === oldHi,
+                  storeEmptySeq)
+
+            case None =>
+              storeEmptySeq
+          }
+      }
+      val storeOutside = storeEmptySeq
 
       val instrConstraint =
         (newArr === a2) &&& alienTermInitFormula &&&

diff --git a/src/main/scala/lazabs/horn/preprocessor/Slicer.scala b/src/main/scala/lazabs/horn/preprocessor/Slicer.scala
@@ -108,7 +108,8 @@ object Slicer extends HornPreprocessor {
               val bodyStates =
                 for (c <- children) yield newNext(c - 1)._1
               val simpleMapping =
-                computeHeapArgMapping(clause, oldClause, bodyStates, newHeadArgs)
+                computeHeapArgMapping(
+                  clause, oldClause, bodyStates, newHeadArgs, frozenPredicates)
 
               // check whether the values of all head arguments can
               // now be derived
@@ -199,10 +200,13 @@ object Slicer extends HornPreprocessor {
   private def computeHeapArgMapping(newClause : Clause,
                                     oldClause : Clause,
                                     oldBodyStates : Seq[IAtom],
-                                    newHeadArgs : Seq[ITerm])
+                                    newHeadArgs : Seq[ITerm],
+                                    frozenPredicates : Set[Predicate])
                                   : Map[ConstantTerm, ITerm] = {
     val Clause(newHead, newBody, newConstraint) = newClause
-    val Clause(oldHead, oldBody, oldConstraint) = oldClause
+    val Clause(oldHead, oldBodyWithFrozenPreds, oldConstraint) = oldClause
+    val oldBody = oldBodyWithFrozenPreds.filterNot(
+      b => frozenPredicates contains b.pred)
 
     assert(newHeadArgs.size == newHead.args.size)
     assert(oldBody.size == oldBodyStates.size)

diff --git a/src/main/scala/lazabs/horn/tests/ExtQuansWithSearchTest.scala b/src/main/scala/lazabs/horn/tests/ExtQuansWithSearchTest.scala
@@ -143,7 +143,8 @@ object ExtQuansForallTest extends App {
 
     val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
       Map(
-        extQuan -> new BooleanInstrumentationOperator(extQuan)
+        extQuan -> new BooleanInstrumentationOperator(
+          extQuan, Some((a: ITerm) => expr2Formula(a)))
       )
 
     val instrLoop = new InstrumentationLoop(
@@ -212,7 +213,8 @@ object ExtQuansExistsTestSafe extends App {
 
     val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
       Map(
-        extQuan -> new BooleanInstrumentationOperator(extQuan)
+        extQuan -> new BooleanInstrumentationOperator(
+          extQuan, Some((a: ITerm) => !expr2Formula(a)))
       )
 
     val instrLoop = new InstrumentationLoop(
@@ -281,7 +283,8 @@ object ExtQuansExistsTestUnsafe extends App {
 
     val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
       Map(
-        extQuan -> new BooleanInstrumentationOperator(extQuan)
+        extQuan -> new BooleanInstrumentationOperator(
+          extQuan, Some((a: ITerm) => !expr2Formula(a)))
       )
 
     val instrLoop = new InstrumentationLoop(
@@ -351,7 +354,7 @@ object ExtQuansNumofTestUnsafe extends App {
 
     val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
       Map(
-        extQuan -> new BooleanInstrumentationOperator(extQuan)
+        extQuan -> new BooleanInstrumentationOperator(extQuan, None)
       )
 
     val instrLoop = new InstrumentationLoop(
@@ -421,7 +424,7 @@ object ExtQuansNumofTestSafe extends App {
 
     val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
       Map(
-        extQuan -> new BooleanInstrumentationOperator(extQuan)
+        extQuan -> new BooleanInstrumentationOperator(extQuan, None)
       )
 
     val instrLoop = new InstrumentationLoop(
@@ -503,7 +506,8 @@ object ExtQuansForallAlienTermTestSafe extends App {
 
     val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
       Map(
-        extQuan -> new BooleanInstrumentationOperator(extQuan)
+        extQuan -> new BooleanInstrumentationOperator(
+          extQuan, Some((a: ITerm) => expr2Formula(a)))
       )
 
     val instrLoop = new InstrumentationLoop(
@@ -585,7 +589,8 @@ object ExtQuansForallAlienTermTestUnsafe extends App {
 
     val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
       Map(
-        extQuan -> new BooleanInstrumentationOperator(extQuan)
+        extQuan -> new BooleanInstrumentationOperator(
+          extQuan, Some((a: ITerm) => expr2Formula(a)))
       )
 
     val instrLoop = new InstrumentationLoop(
@@ -666,7 +671,8 @@ object ExtQuansForallTestTwoSelectsSafe extends App {
 
     val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
       Map(
-        extQuan -> new BooleanInstrumentationOperator(extQuan)
+        extQuan -> new BooleanInstrumentationOperator(
+          extQuan, Some((a: ITerm) => expr2Formula(a)))
         )
 
     val instrLoop = new InstrumentationLoop(
@@ -740,7 +746,8 @@ object ExtQuansForallTestTwoStoresSafe extends App {
 
     val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
       Map(
-        extQuan -> new BooleanInstrumentationOperator(extQuan)
+        extQuan -> new BooleanInstrumentationOperator(
+          extQuan, Some((a: ITerm) => expr2Formula(a)))
         )
 
     val instrLoop = new InstrumentationLoop(
@@ -773,12 +780,11 @@ object ExtQuansForallTestTwoStores2Safe extends App {
 
     val a1 = new SortedConstantTerm("a1", ar.sort)
     val a2 = new SortedConstantTerm("a2", ar.sort)
-    val a3 = new SortedConstantTerm("a3", ar.sort)
 
     val i = new ConstantTerm("i")
 
-    val p = for (i <- 0 until 5) yield (new MonoSortedPredicate("p" + i,
-                                                                Seq(ar.sort, Sort.Integer)))
+    val p = for (i <- 0 until 5) yield
+      new MonoSortedPredicate("p" + i, Seq(ar.sort, Sort.Integer))
 
     val arrAccess = ar.select(a1, i)
     val arrIndex = i
@@ -814,7 +820,8 @@ object ExtQuansForallTestTwoStores2Safe extends App {
 
     val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
       Map(
-        extQuan -> new BooleanInstrumentationOperator(extQuan)
+        extQuan -> new BooleanInstrumentationOperator(
+          extQuan, Some((a: ITerm) => expr2Formula(a)))
         )
 
     val instrLoop = new InstrumentationLoop(