Skip to content

Commit

Permalink
progress qp merging
Browse files Browse the repository at this point in the history
  • Loading branch information
@mlimbeck
mlimbeck committed Nov 26, 2024
1 parent 7c2463d commit cf7524c
Show file tree
Hide file tree
Showing 3 changed files with 113 additions and 136 deletions.
4 changes: 2 additions & 2 deletions src/main/scala/logger/writer/SymbExLogReportWriter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,8 +25,8 @@ object SymbExLogReportWriter {

private def inverseFunctionsToJSON(invs: InverseFunctions): JsValue = {
JsArray(
TermWriter.toJSON(invs.axiomInversesOfInvertibles),
TermWriter.toJSON(invs.axiomInvertiblesOfInverses)
(invs.axiomInversesOfInvertibles.map(a => TermWriter.toJSON(a)) ++
invs.axiomInvertiblesOfInverses.map(a => TermWriter.toJSON(a))).toVector
)
}

Expand Down
145 changes: 29 additions & 116 deletions src/main/scala/rules/QuantifiedChunkSupport.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ import viper.silicon.state.terms.predef.`?r`
import viper.silicon.state.terms.utils.consumeExactRead
import viper.silicon.supporters.functions.{FunctionRecorder, NoopFunctionRecorder}
import viper.silicon.utils.ast.{BigAnd, buildMinExp}
import viper.silicon.utils.freshSnap
import viper.silicon.utils.notNothing.NotNothing
import viper.silicon.verifier.Verifier
import viper.silver.ast
Expand All @@ -35,8 +36,8 @@ case class InverseFunctions(condition: Term,
invertibles: Seq[Term],
invertibleExps: Option[Seq[ast.Exp]],
additionalArguments: Vector[Var],
axiomInversesOfInvertibles: Quantification,
axiomInvertiblesOfInverses: Quantification,
axiomInversesOfInvertibles: Seq[Quantification],
axiomInvertiblesOfInverses: Seq[Quantification],
qvarExps: Option[Seq[ast.LocalVarDecl]],
qvarsToInverses: Map[Var, Seq[Function]],
qvarsToImages: Map[Var, Seq[Function]]) {
Expand All @@ -46,7 +47,7 @@ case class InverseFunctions(condition: Term,
val images: Iterable[Function] = qvarsToImages.values.flatten

val definitionalAxioms: Vector[Quantification] =
Vector(axiomInversesOfInvertibles, axiomInvertiblesOfInverses)
(axiomInversesOfInvertibles ++ axiomInvertiblesOfInverses).toVector

def inversesOf(argument: Term): Seq[App] =
inversesOf(Seq(argument))
Expand All @@ -66,15 +67,14 @@ case class InverseFunctions(condition: Term,
case (x, inv) => x -> inv.map(fn => App(fn, additionalArguments ++ arguments))
}.to(Map)


def mergeInvFunctions(invs: InverseFunctions): InverseFunctions = {
InverseFunctions(
condition = True,
invertibles = invertibles ++ invs.invertibles,
invertibleExps = Some(invertibleExps.getOrElse(Seq()) ++ invs.invertibleExps.getOrElse(Seq())),
additionalArguments = additionalArguments,
axiomInversesOfInvertibles = axiomInversesOfInvertibles,
axiomInvertiblesOfInverses = axiomInvertiblesOfInverses,
axiomInversesOfInvertibles = axiomInversesOfInvertibles ++ invs.axiomInversesOfInvertibles,
axiomInvertiblesOfInverses = axiomInvertiblesOfInverses ++ invs.axiomInvertiblesOfInverses,
qvarExps = qvarExps,
qvarsToInverses = qvarsToInverses ++ invs.qvarsToInverses,
qvarsToImages = qvarsToImages ++ invs.qvarsToImages,
Expand All @@ -89,9 +89,9 @@ case class InverseFunctions(condition: Term,
|$linePrefix invertibles: $invertibles
|$linePrefix additionalArguments: $additionalArguments
|$linePrefix axiomInversesOfInvertibles:
|$linePrefix ${axiomInversesOfInvertibles.stringRepresentationWithTriggers}
|$linePrefix ${axiomInversesOfInvertibles.map(a => a.stringRepresentationWithTriggers)}
|$linePrefix axiomInvertiblesOfInverses
|$linePrefix ${axiomInvertiblesOfInverses.stringRepresentationWithTriggers}
|$linePrefix ${axiomInvertiblesOfInverses.map(a => a.stringRepresentationWithTriggers)}
""".stripMargin
}

Expand Down Expand Up @@ -255,7 +255,8 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
* @param v The verifier to use.
* @return A tuple (fr, sm, def) of functionRecorder, a snapshot map sm and a term def constraining sm.
*/
def combineSnapshotMaps(fr: FunctionRecorder, valueFn: Term => Term, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term)
// def combineSnapshotMaps(fr: FunctionRecorder, valueFn: Term => Term, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term)

}

object quantifiedChunkSupporter extends QuantifiedChunkSupport {
Expand Down Expand Up @@ -476,7 +477,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
* The domain definition is `None` iff the provided `optSmDomainDefinitionCondition` is
* `None`.
*/
private def summarise(s: State,
def summarise(s: State,
relevantChunks: Seq[QuantifiedBasicChunk],
codomainQVars: Seq[Var], /* rs := r_1, ..., r_m. May be empty. */
resource: ast.Resource,
Expand Down Expand Up @@ -955,8 +956,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
* Note that the trigger generation code might have added quantified variables
* to that axiom.
*/
(inverseFunctions.axiomInversesOfInvertibles.triggers,
inverseFunctions.axiomInversesOfInvertibles.vars, qvarExps)
(inverseFunctions.axiomInversesOfInvertibles.flatMap(a => a.triggers),
inverseFunctions.axiomInversesOfInvertibles.flatMap(a => a.vars), qvarExps)
}

if (effectiveTriggers.isEmpty) {
Expand Down Expand Up @@ -1006,8 +1007,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
Option.when(withExp)(DebugExp.createInstance(comment, isInternal_ = true)))
v.decider.assert(receiverInjectivityCheck) {
case true =>
val ax = inverseFunctions.axiomInversesOfInvertibles
val inv = inverseFunctions.copy(axiomInversesOfInvertibles = Forall(ax.vars, ax.body, effectiveTriggers))
val ax = inverseFunctions.axiomInversesOfInvertibles.head
val inv = inverseFunctions.copy(axiomInversesOfInvertibles = Seq(Forall(ax.vars, ax.body, effectiveTriggers)))

val comment = "Definitional axioms for inverse functions"
v.decider.prover.comment(comment)
Expand Down Expand Up @@ -1192,8 +1193,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
* Note that the trigger generation code might have added quantified variables
* to that axiom.
*/
(inverseFunctions.axiomInversesOfInvertibles.triggers,
inverseFunctions.axiomInversesOfInvertibles.vars)
(inverseFunctions.axiomInversesOfInvertibles.flatMap(a => a.triggers),
inverseFunctions.axiomInversesOfInvertibles.flatMap(a => a.vars))
}

val comment = "Nested auxiliary terms: globals"
Expand Down Expand Up @@ -1346,9 +1347,9 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
s.program
)
val debugExp = Option.when(withExp)(DebugExp.createInstance("Inverse functions for quantified permission", true))
v.decider.assume(FunctionPreconditionTransformer.transform(inverseFunctions.axiomInvertiblesOfInverses, s3.program), debugExp)
v.decider.assume(inverseFunctions.axiomInvertiblesOfInverses, debugExp)
val substitutedAxiomInversesOfInvertibles = inverseFunctions.axiomInversesOfInvertibles.replace(formalQVars, tArgs)
v.decider.assume(FunctionPreconditionTransformer.transform(inverseFunctions.axiomInvertiblesOfInverses.head, s3.program), debugExp)
v.decider.assume(inverseFunctions.axiomInvertiblesOfInverses.head, debugExp)
val substitutedAxiomInversesOfInvertibles = inverseFunctions.axiomInversesOfInvertibles.head.replace(formalQVars, tArgs)
v.decider.assume(FunctionPreconditionTransformer.transform(substitutedAxiomInversesOfInvertibles, s3.program), debugExp)
v.decider.assume(substitutedAxiomInversesOfInvertibles, debugExp)
val h2 = Heap(remainingChunks ++ otherChunks)
Expand Down Expand Up @@ -1954,8 +1955,8 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
invertibles,
invertibleExps,
additionalInvArgs.toVector,
axInvsOfFct,
axFctsOfInvs,
Seq(axInvsOfFct),
Seq(axFctsOfInvs),
qvarExps,
qvars.zip(inverseFunctions).map{case (qvar, inv) => (qvar, Seq(inv))}.to(Map),
qvars.zip(imageFunctions).filter(_._2 != null).map{case (qvar, img) => (qvar, Seq(img))}.to(Map)
Expand All @@ -1972,84 +1973,12 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
matchingChunks ++ otherChunks
}

private def findChunk2(chunks: Iterable[Chunk], chunk: QuantifiedChunk, v: Verifier): Option[QuantifiedChunk] = {
val lr = chunk match {
case qfc: QuantifiedFieldChunk if qfc.invs.isDefined =>
Left(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.condition)
case qfc: QuantifiedFieldChunk if qfc.singletonArguments.isDefined =>
Right(qfc.singletonArguments.get)
case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined =>
Left(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.condition)
case qpc: QuantifiedPredicateChunk if qpc.singletonArguments.isDefined =>
Right(qpc.singletonArguments.get)
case _ => return None
}
val relevantChunks: Iterable[QuantifiedBasicChunk] = chunks.flatMap {
case ch: QuantifiedBasicChunk if ch.id == chunk.id => Some(ch)
case _ => None
}
return relevantChunks.headOption
val (receiverTerms, quantVars, cond) = lr match {
case Left(tuple) => tuple
case Right(singletonArguments) =>
return relevantChunks.find { ch =>
val chunkInfo = ch match {
case qfc: QuantifiedFieldChunk if qfc.singletonArguments.isDefined =>
Some(qfc.singletonArguments.get)
case qpc: QuantifiedPredicateChunk if qpc.singletonArguments.isDefined =>
Some(qpc.singletonArguments.get)
case _ => None
}
chunkInfo match {
case Some(cSingletonArguments) =>
val equalityTerm = And(singletonArguments.zip(cSingletonArguments).map { case (a, b) => a === b })
val result = v.decider.check(equalityTerm, Verifier.config.checkTimeout())
if (result) {
// Learn the equality
val debugExp = Option.when(withExp)(DebugExp.createInstance("Chunks alias", true))
v.decider.assume(equalityTerm, debugExp)
}
result
case _ => false
}
}
}
relevantChunks.find { ch =>
val chunkInfo = ch match {
case qfc: QuantifiedFieldChunk if qfc.invs.isDefined =>
Some(qfc.invs.get.invertibles, qfc.quantifiedVars, qfc.condition)
case qpc: QuantifiedPredicateChunk if qpc.invs.isDefined =>
Some(qpc.invs.get.invertibles, qpc.quantifiedVars, qpc.condition)
case _ => None
}
chunkInfo match {
case Some((cInvertibles, cQvars, cCond)) =>
receiverTerms.zip(cInvertibles).forall(p => {
if (cQvars.length == quantVars.length && cQvars.zip(quantVars).forall(vars => vars._1.sort == vars._2.sort)) {
val condReplaced = cCond.replace(cQvars, quantVars)
val secondReplaced = p._2.replace(cQvars, quantVars)
val equalityTerm = SimplifyingForall(quantVars, And(Seq(p._1 === secondReplaced, cond === condReplaced)), Seq())
val result = v.decider.check(equalityTerm, Verifier.config.checkTimeout())
if (result) {
// Learn the equality
val debugExp = Option.when(withExp)(DebugExp.createInstance("Chunks alias", true))
v.decider.assume(equalityTerm, debugExp)
}
result
} else {
false
}
})
case _ => false
}
}
}

override def findChunk(chunks: Iterable[Chunk], chunk: QuantifiedChunk, v: Verifier): Option[QuantifiedChunk] = {
val relevantChunks: Iterable[QuantifiedBasicChunk] = chunks.flatMap {
case ch: QuantifiedBasicChunk if ch.id == chunk.id => Some(ch)
case _ => None
}
return relevantChunks.headOption

relevantChunks foreach { ch =>
val codomainQVars = chunk.quantifiedVars
Expand All @@ -2067,29 +1996,13 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
None
}

// Based on StateConsolidator#combineSnapshots
override def combineSnapshotMaps(fr: FunctionRecorder, valueFn: Term => Term, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = {
val lookupT1 = valueFn(t1)
val lookupT2 = valueFn(t2)
val (fr2, sm, smDef, triggers) = (IsPositive(p1), IsPositive(p2)) match {
// If we statically know that both permission values are positive we can forego the quantifier
case (True, True) => return (fr, t1, t1 === t2)
case (True, b2) => (fr, t1, Implies(b2, lookupT1 === lookupT2), Seq(Trigger(lookupT1), Trigger(lookupT2)))
case (b1, True) => (fr, t2, Implies(b1, lookupT2 === lookupT1), Seq(Trigger(lookupT2), Trigger(lookupT1)))
case (b1, b2) =>
/*
* Since it is not definitely known whether p1 and p2 are positive,
* we have to introduce a fresh snapshot. Note that it is not sound
* to use t1 or t2 and constrain it.
*/
val t3 = v.decider.fresh(t1.sort, Option.when(withExp)(PUnknown()))
val lookupT3 = valueFn(t3)
(fr.recordConstrainedVar(t3, And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2))), t3,
And(Implies(b1, lookupT3 === lookupT1), Implies(b2, lookupT3 === lookupT2)), Seq(Trigger(lookupT1), Trigger(lookupT2), Trigger(lookupT3)))
}
// override def combineSnapshotMaps(fr: FunctionRecorder, s: stateresource, Resource, lookup: Term => Term, qVars: Seq[Var], t1: Term, t2: Term, p1: Term, p2: Term, v: Verifier): (FunctionRecorder, Term, Term) = {
// val snap = freshSnap(t1.sort, v)
// val smDef = Forall(qVars, And(Implies(IsPositive(p1), lookup(snap) === lookup(t1)), Implies(IsPositive(p2), lookup(snap) === lookup(t2))),
// Seq(Trigger(lookup(snap)), Trigger(lookup(t1)), Trigger(lookup(t2))))
// (fr.recordFreshSnapshot(snap).recordConstraint(smDef), snap, smDef)
// }

(fr2, sm, Forall(qVars, smDef, triggers))
}

def qpAppChunkOrderHeuristics(receiverTerms: Seq[Term], quantVars: Seq[Var], hints: Seq[Term], v: Verifier)
: Seq[QuantifiedBasicChunk] => Seq[QuantifiedBasicChunk] = {
Expand Down
Loading

0 comments on commit cf7524c

Please sign in to comment.