Skip to content

Commit

Permalink
Fix a bug in preprocessing, add test cases
Browse files Browse the repository at this point in the history
  • Loading branch information
@zafer-esen
zafer-esen committed Mar 13, 2024
1 parent c092198 commit 3b38e7c
Show file tree
Hide file tree
Showing 4 changed files with 210 additions and 21 deletions.
1 change: 1 addition & 0 deletions src/main/scala/lazabs/horn/extendedquantifiers/GhostVariableAdder.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -139,6 +139,7 @@ class GhostVariableAdder(
* The terms need to be in the same order as the indexes assigned
* earlier, so we convert ghostVarToTerm into a seq and sort it.
*/
assert(exqAppId < ghostVariableInds.size)
ghostVarToTerm.toSeq.sortBy(
p => ghostVariableInds(exqAppId)(p._1)).map{
case (ghostVar, ghostTerm) =>
Expand Down
59 changes: 39 additions & 20 deletions src/main/scala/lazabs/horn/extendedquantifiers/InstrumentationLoop.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,9 +40,9 @@ import lazabs.horn.abstractions.{AbstractionRecord, StaticAbstractionBuilder}
import lazabs.horn.abstractions.VerificationHints.VerifHintElement
import lazabs.horn.bottomup.HornClauses.Clause
import lazabs.horn.bottomup.{DagInterpolator, IncrementalHornPredAbs, PredicateStore, TemplateInterpolator}
import lazabs.horn.bottomup.Util.{Dag, DagEmpty, DagNode}
import lazabs.horn.bottomup.Util.{Dag, DagEmpty}
import lazabs.horn.extendedquantifiers.theories.AbstractExtendedQuantifier
import lazabs.horn.preprocessor.DefaultPreprocessor
import lazabs.horn.preprocessor.{PreStagePreprocessor, DefaultPreprocessor}
import lazabs.horn.preprocessor.HornPreprocessor.{BackTranslator, Clauses, ComposedBackTranslator, VerificationHints}

import scala.collection.mutable.{ArrayBuffer, Buffer => MBuffer, HashMap => MHashMap, HashSet => MHashSet}
Expand Down Expand Up @@ -80,13 +80,12 @@ class InstrumentationLoop (
private val prefixCompressionPeriod = 50
private var prefixCompressionCounter = 0

private val preprocessor = new DefaultPreprocessor
private var curHints : VerificationHints = hints
private val (simpClauses, newHints1, backTranslator1) =
Console.withErr(Console.out) {
val slicingPre = GlobalParameters.get.slicing
GlobalParameters.get.slicing = false
val res = preprocessor.process(clauses, curHints)
val res = (new PreStagePreprocessor).process(clauses, curHints)
GlobalParameters.get.slicing = slicingPre
res
}
Expand All @@ -108,6 +107,7 @@ class InstrumentationLoop (
private val searchStepsPerNumGhostRanges = new MHashMap[Int, Int]
private var lastSolver : IncrementalHornPredAbs[Clause] = _
private var lastInstrumenter : InstrumentationOperatorApplier = _
private var lastBackTranslator : BackTranslator = _

while (ghostVarRanges.nonEmpty && rawResult == Inconclusive) {
val numRanges = ghostVarRanges.head
Expand All @@ -118,7 +118,26 @@ class InstrumentationLoop (
simpClauses, curHints, Set.empty, extendedQuantifierToInstOp, numRanges)
lastInstrumenter = instrumenter

curHints = instrumenter.newHints
val outStream =
if (lazabs.GlobalParameters.get.logStat) Console.err
else lazabs.horn.bottomup.HornWrapper.NullStream

val (simpClauses2, hints, bTranslator) =
Console.withErr(lazabs.horn.bottomup.HornWrapper.NullStream){
(new DefaultPreprocessor).process(
instrumenter.instrumentedClauses,
instrumenter.newHints,
instrumenter.branchPredicates
)}
lastBackTranslator = bTranslator
curHints = hints
val branchPreds =
instrumenter.branchPredicates intersect
simpClauses2.flatMap(_.predicates).toSet

val filteredSearchSpace = (for (inst <- instrumenter.searchSpace) yield
inst.filter(branchPreds contains _._1).sortBy(_._1.name))
.filter(_.nonEmpty).distinct

// println("="*80)
// println("Clauses after instrumentation")
Expand All @@ -131,18 +150,14 @@ class InstrumentationLoop (
// println("="*80)
// println("Clauses after instrumentation (simplified)")

val outStream =
if (lazabs.GlobalParameters.get.logStat) Console.err
else lazabs.horn.bottomup.HornWrapper.NullStream

val interpolator =
if (templateBasedInterpolation)
Console.withErr(outStream) {
val builder =
new StaticAbstractionBuilder(
instrumenter.instrumentedClauses, //simpClauses2,
simpClauses2,
templateBasedInterpolationType,
instrumenter.branchPredicates) //remainingBranchPredicates)
branchPreds) //remainingBranchPredicates)
val autoAbstractionMap =
builder.abstractionRecords

Expand Down Expand Up @@ -194,16 +209,16 @@ class InstrumentationLoop (

val incSolver =
new IncrementalHornPredAbs(
instrumenter.instrumentedClauses,
simpClauses2,
curHints.toInitialPredicates,
instrumenter.branchPredicates,
branchPreds,
interpolator)

lastSolver = incSolver

Random.setSeed(42)
val searchSpace = new MHashSet[Map[Predicate, Conjunction]]
Random.shuffle(instrumenter.searchSpace).foreach { search =>
Random.shuffle(filteredSearchSpace).foreach { search =>
searchSpace += search.toMap
}

Expand Down Expand Up @@ -245,7 +260,7 @@ class InstrumentationLoop (
// ineligiblePrefixes.toSet)

println("\n(" + numSteps + ") Remaining search space size: " +
(instrumenter.searchSpace.size - totalExplored - postponedSearches.size))
(searchSpace.size))
println("Postponed instrumentations : " + postponedSearches.size)
println("Selected branches: " + instrumentation.map{instr =>
instr._1.name + "(" + (instr._2.arithConj.positiveEqs.head.constant.
Expand Down Expand Up @@ -278,9 +293,8 @@ class InstrumentationLoop (
noTimeoutCount += 1
consecutiveTimeoutCount = 0
println("\ninconclusive, iterating...")
val prefix : Set[IAtom] = cex.subdagIterator.toList.flatMap(_.d
._2.body.filter(
instrumenter.branchPredicates contains _.pred)).toSet
val prefix : Set[IAtom] = cex.subdagIterator.toList.flatMap(
_.d._2.body.filter(branchPreds contains _.pred)).toSet

prefixCompressionCounter += 1
ineligiblePrefixes += prefix
Expand All @@ -293,7 +307,7 @@ class InstrumentationLoop (
ineligiblePrefixes.filter(_.size < prefix.size).
exists(other => other subsetOf prefix))
yield prefix
val beforeSize = ineligiblePrefixes.size
val beforeSize = ineligiblePrefixes.size
redundantPrefixes.foreach(ineligiblePrefixes -=)
println("Compressed ineligible prefixes: " + beforeSize +
" to " + ineligiblePrefixes.size)
Expand Down Expand Up @@ -328,13 +342,18 @@ class InstrumentationLoop (
currentTimeout / 1e3)
}
}
if(postponedSearches.isEmpty && searchSpace.forall(
instrumentation => ineligiblePrefixes.exists(
prefix => prefix subsetOf computeAtoms(instrumentation)))) {
println("Search space exhausted - inconclusive")
}
searchSpace.clear()
}
}

private val backTranslator =
new ComposedBackTranslator(
Seq(lastInstrumenter.backTranslator) ++ backTranslators.reverse)
Seq(lastBackTranslator) ++ backTranslators.reverse)

/**
* The result of CEGAR: either a solution of the Horn clauses, or
Expand Down
16 changes: 15 additions & 1 deletion ...bs/horn/extendedquantifiers/instrumentationoperators/BooleanInstrumentationOperator.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -361,7 +361,21 @@ class BooleanInstrumentationOperator(exq : ExtendedQuantifierWithPredicate)
otherConstants : Set[IConstant],
constInfo : ConstInfo)
: Seq[RewriteRules.Result] = {
???
val ConstInfo(a, o, arrayTheory2) = constInfo

if (arrayTheory2 != exq.arrayTheory) return Seq()

val (oldLo, newLo) = (oldGhostTerms(GhLo), newGhostTerms(GhLo))
val (oldHi, newHi) = (oldGhostTerms(GhHi), newGhostTerms(GhHi))
val (oldRes, newRes) = (oldGhostTerms(GhRes), newGhostTerms(GhRes))
val (oldArr, newArr) = (oldGhostTerms(GhArr), newGhostTerms(GhArr))
val (oldArrInd, newArrInd) = (oldGhostTerms(GhArrInd), newGhostTerms
(GhArrInd))

val instrConstraint = newLo === 0 & newHi === 0 & newArr === a
Seq(RewriteRules.Result(newConjunct = instrConstraint,
rewriteFormulas = Map(),
assertions = Seq()))
}

override def rewriteAggregate(ghostTerms : Seq[Map[GhostVar, ITerm]],
Expand Down
155 changes: 155 additions & 0 deletions src/main/scala/lazabs/horn/tests/ExtQuansWithSearchTest.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -605,3 +605,158 @@ object ExtQuansForallAlienTermTestUnsafe extends App {
println(instrLoop.result)
}
}

object ExtQuansForallTestTwoSelectsSafe extends App {
ap.util.Debug enableAllAssertions true
lazabs.GlobalParameters.get.setLogLevel(1)
lazabs.GlobalParameters.get.assertions = true

{
val ar = ExtArray(Seq(Sort.Integer), Sort.Integer)
val reduceOp : (ITerm, ITerm) => ITerm =
(a : ITerm, b : ITerm) => expr2Term(expr2Formula(a) &&& expr2Formula(b))

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 arrAccess = ar.select(a1, i)
val arrIndex = i
val pred = arrAccess === i
val predicate : (ITerm, ITerm) => ITerm =
(access : ITerm, index : ITerm) => expr2Term(
ExpressionReplacingVisitor(
ExpressionReplacingVisitor(pred, arrAccess, access),
arrIndex, index))
val extQuan = new ExtendedQuantifierWithPredicate(
name = "\\forall",
arrayTheory = ar,
identity = expr2Term(IBoolLit(true)),
reduceOp = reduceOp,
invReduceOp = None,
predicate = predicate,
rangeFormulaLo = Some((ghostLo : ITerm, lo : ITerm, p : ITerm) =>
ite(expr2Formula(p), ghostLo <= lo, ghostLo >=
lo)),
rangeFormulaHi = Some((ghostHi : ITerm, hi : ITerm, p : ITerm) =>
ite(expr2Formula(p), ghostHi >= hi, ghostHi <= hi)))
TheoryRegistry register extQuan

import ar._

// val clauses = List(
// p(0)(a1, i) :- (i === 0),
// p(1)(a2, i+1) :- (p(0)(a1, i), a2 === store(a1, i, i), i < 3),
// p(0)(a2, i) :- (p(1)(a1, i), a2 === store(a1, i, i)),
// p(2)(a1, i) :- (p(0)(a1, i), i >= 3),
// false :- (p(2)(a1, i), expr2Formula(extQuan.morphism(a1, 0, 3)))
// )
val clauses = List(
p(0)(a1, i) :- (i === 0),
p(1)(a1, i + 1) :- (p(0)(a1, i), i === select(a1, i), i < 3),
p(0)(a1, i) :- (p(1)(a1, i), i === select(a1, i)),
p(2)(a1, i) :- (p(0)(a1, i), i >= 3),
false :- (p(2)(a1, i), expr2Formula(extQuan.morphism(a1, 0, 3)))
)

val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
Map(
extQuan -> new BooleanInstrumentationOperator(extQuan)
)

val instrLoop = new InstrumentationLoop(
clauses, EmptyVerificationHints, instOps)

instrLoop.result match {
case Left(sln) =>
println("SAFE")
for((p, f) <- sln) {
println(s"$p -> ${SimpleAPI.pp(f)}")
}
case Right(cex) =>
println("UNSAFE")
cex.prettyPrint
}

println(instrLoop.result)
}
}

object ExtQuansForallTestTwoStoresSafe extends App {
ap.util.Debug enableAllAssertions true
lazabs.GlobalParameters.get.setLogLevel(1)
lazabs.GlobalParameters.get.assertions = true

{
val ar = ExtArray(Seq(Sort.Integer), Sort.Integer)
val reduceOp : (ITerm, ITerm) => ITerm =
(a : ITerm, b : ITerm) => expr2Term(expr2Formula(a) &&& expr2Formula(b))

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 arrAccess = ar.select(a1, i)
val arrIndex = i
val pred = arrAccess === i
val predicate : (ITerm, ITerm) => ITerm =
(access : ITerm, index : ITerm) => expr2Term(
ExpressionReplacingVisitor(
ExpressionReplacingVisitor(pred, arrAccess, access),
arrIndex, index))
val extQuan = new ExtendedQuantifierWithPredicate(
name = "\\forall",
arrayTheory = ar,
identity = expr2Term(IBoolLit(true)),
reduceOp = reduceOp,
invReduceOp = None,
predicate = predicate,
rangeFormulaLo = Some((ghostLo : ITerm, lo : ITerm, p : ITerm) =>
ite(expr2Formula(p), ghostLo <= lo, ghostLo >=
lo)),
rangeFormulaHi = Some((ghostHi : ITerm, hi : ITerm, p : ITerm) =>
ite(expr2Formula(p), ghostHi >= hi, ghostHi <= hi)))
TheoryRegistry register extQuan

import ar._

val clauses = List(
p(0)(a1, i) :- (i === 0),
p(1)(a2, i+1) :- (p(0)(a1, i), a2 === store(a1, i, i), i < 3),
p(0)(a2, i) :- (p(1)(a1, i), a2 === store(a1, i, i)),
p(2)(a1, i) :- (p(0)(a1, i), i >= 3),
false :- (p(2)(a1, i), expr2Formula(extQuan.morphism(a1, 0, 3)))
)

val instOps : Map[AbstractExtendedQuantifier, InstrumentationOperator] =
Map(
extQuan -> new BooleanInstrumentationOperator(extQuan)
)

val instrLoop = new InstrumentationLoop(
clauses, EmptyVerificationHints, instOps)

instrLoop.result match {
case Left(sln) =>
println("SAFE")
for((p, f) <- sln) {
println(s"$p -> ${SimpleAPI.pp(f)}")
}
case Right(cex) =>
println("UNSAFE")
cex.prettyPrint
}

println(instrLoop.result)
}
}

0 comments on commit 3b38e7c

Please sign in to comment.