Skip to content

Commit

Permalink
Merge
Browse files Browse the repository at this point in the history
  • Loading branch information
@marcoeilers
marcoeilers committed Sep 3, 2024
2 parents 73058c2 + e3a690b commit 23986cd
Show file tree
Hide file tree
Showing 5 changed files with 26 additions and 16 deletions.
20 changes: 16 additions & 4 deletions src/main/scala/debugger/SiliconDebugger.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,7 +69,7 @@ case class ProofObligation(s: State,
val shape = mwc.id.ghostFreeWand
val expBindings = mwc.bindings.map(b => b._1 -> b._2._2.get)
val instantiated = shape.replace(expBindings)
instantiated.toString
s"acc(${instantiated.toString}, ${Simplifier.simplify(mwc.permExp.get, true)})"
case qfc: QuantifiedFieldChunk =>
if (qfc.singletonRcvrExp.isDefined) {
val receiver = Simplifier.simplify(qfc.singletonRcvrExp.get, true)
Expand All @@ -78,7 +78,7 @@ case class ProofObligation(s: State,
} else {
val varsString = qfc.quantifiedVarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
val qvarsString = "forall " + qfc.invs.get.qvarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
val varsEqualString = qfc.invs.get.qvarExps.get.zip(qfc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${Simplifier.simplify(v._2, true)}").mkString(" && ")
val varsEqualString = qfc.quantifiedVarExps.get.zip(qfc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${Simplifier.simplify(v._2, true)}").mkString(" && ")
s"forall ${varsString} :: ${qvarsString} :: ${varsEqualString} ==> acc(${qfc.quantifiedVarExps.get.head.name}.${qfc.id}, ${Simplifier.simplify(qfc.permExp.get, true)})"
}
case qpc: QuantifiedPredicateChunk =>
Expand All @@ -87,11 +87,23 @@ case class ProofObligation(s: State,
} else {
val varsString = qpc.quantifiedVarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
val qvarsString = "forall " + qpc.invs.get.qvarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
val varsEqualString = qpc.invs.get.qvarExps.get.zip(qpc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${Simplifier.simplify(v._2, true)}").mkString(" && ")
val varsEqualString = qpc.quantifiedVarExps.get.zip(qpc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${Simplifier.simplify(v._2, true)}").mkString(" && ")
s"forall ${varsString} :: ${qvarsString} :: ${varsEqualString} ==> acc(${qpc.id}(${qpc.quantifiedVarExps.get.map(_.name).mkString(", ")}), ${Simplifier.simplify(qpc.permExp.get, true)})"
}
case qwc: QuantifiedMagicWandChunk =>
qwc.toString // TODO
val shape = qwc.id.ghostFreeWand
if (qwc.singletonArgExps.isDefined) {
val instantiated = shape.replace(shape.subexpressionsToEvaluate(s.program).zip(qwc.singletonArgExps.get).map(e => e._1 -> Simplifier.simplify(e._2, true)).toMap)
val permReplaced = Simplifier.simplify(qwc.permExp.get.replace(qwc.quantifiedVarExps.get.zip(qwc.singletonArgExps.get).map(e => e._1.localVar -> e._2).toMap), true)

s"acc(${instantiated.toString}, ${permReplaced})"
} else{
val varsString = qwc.quantifiedVarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
val qvarsString = "forall " + qwc.invs.get.qvarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
val varsEqualString = qwc.quantifiedVarExps.get.zip(qwc.invs.get.invertibleExps.get).map(v => s"${v._1.name} == ${Simplifier.simplify(v._2, true)}").mkString(" && ")
val instantiated = shape.replace(shape.subexpressionsToEvaluate(s.program).zip(qwc.invs.get.invertibleExps.get).map(e => e._1 -> Simplifier.simplify(e._2, true)).toMap)
s"forall ${varsString} :: ${qvarsString} :: ${varsEqualString} ==> acc(${instantiated}, ${Simplifier.simplify(qwc.permExp.get, true)})"
}
}
res
}
Expand Down
4 changes: 2 additions & 2 deletions src/main/scala/rules/Consumer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -468,7 +468,7 @@ object consumer extends ConsumptionRules {
case wand: ast.MagicWand if s.qpMagicWands.contains(MagicWandIdentifier(wand, s.program)) =>
val bodyVars = wand.subexpressionsToEvaluate(s.program)
val formalVars = bodyVars.indices.toList.map(i => Var(Identifier(s"x$i"), v.symbolConverter.toSort(bodyVars(i).typ), false))

val formalVarExps = Option.when(withExp)(bodyVars.indices.toList.map(i => ast.LocalVarDecl(s"x$i", bodyVars(i).typ)()))
evals(s, bodyVars, _ => pve, v)((s1, tArgs, bodyVarsNew, v1) => {
val s1p = if (s1.heapDependentTriggers.contains(MagicWandIdentifier(wand, s.program))){
val (relevantChunks, _) =
Expand All @@ -490,7 +490,7 @@ object consumer extends ConsumptionRules {
s1p,
h,
formalVars,
Option.when(withExp)(wand.formalArgs),
formalVarExps,
tArgs,
Option.when(withExp)(bodyVars),
wand,
Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/rules/HavocSupporter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -133,7 +133,7 @@ object havocSupporter extends SymbolicExecutionRules {
case false => createFailure(pve dueTo notInjectiveReason, v, s1, receiverInjectivityCheck, "QP receiver injective")
case true =>
// Generate the inverse axioms
val (inverseFunctions, imagesOfCodomain, _) = quantifiedChunkSupporter.getFreshInverseFunctions(
val (inverseFunctions, imagesOfCodomain) = quantifiedChunkSupporter.getFreshInverseFunctions(
qvars = tVars,
qvarExps = eVars,
condition = tCond,
Expand Down
2 changes: 1 addition & 1 deletion src/main/scala/rules/Producer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -383,7 +383,7 @@ object producer extends ProductionRules {
if (s1.recordPcs) (s1.conservedPcs.head :+ v1.decider.pcs.after(definitionalAxiomMark)) +: s1.conservedPcs.tail
else s1.conservedPcs
val ch =
quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, formalVarExps, wand, args, Option.when(withExp)(bodyVars),
quantifiedChunkSupporter.createSingletonQuantifiedChunk(formalVars, formalVarExps, wand, args, bodyVarsNew,
FullPerm, Option.when(withExp)(ast.FullPerm()(wand.pos, wand.info, wand.errT)), sm, s.program)
val h2 = s1.h + ch
val smCache1 = if (s1.heapDependentTriggers.contains(MagicWandIdentifier(wand, s1.program))){
Expand Down
14 changes: 6 additions & 8 deletions src/main/scala/rules/QuantifiedChunkSupport.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,7 +156,7 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
userProvidedTriggers: Option[Seq[Trigger]],
qidPrefix: String,
v: Verifier)
: (InverseFunctions, Seq[Term], Option[Seq[ast.Exp]])
: (InverseFunctions, Seq[Term])

def injectivityAxiom(qvars: Seq[Var],
condition: Term,
Expand Down Expand Up @@ -293,7 +293,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
program: ast.Program)
: (QuantifiedBasicChunk, InverseFunctions) = {

val (inverseFunctions, imagesOfCodomain, imagesOfCodomainExp) =
val (inverseFunctions, imagesOfCodomain) =
getFreshInverseFunctions(
qvars,
qvarExps,
Expand All @@ -318,7 +318,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {

val conditionalizedPermissionsExp =
Option.when(withExp)(ast.CondExp(
ast.And(BigAnd(imagesOfCodomainExp.get), conditionExp.get)(),
conditionExp.get,
permissionExps.get,
ast.NoPerm()())())

Expand Down Expand Up @@ -1138,7 +1138,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
(Q: (State, Heap, Term, Verifier) => VerificationResult)
: VerificationResult = {

val (inverseFunctions, imagesOfFormalQVars, imagesOfFormalQVarExps) =
val (inverseFunctions, imagesOfFormalQVars) =
quantifiedChunkSupporter.getFreshInverseFunctions(
qvars,
qvarExps,
Expand Down Expand Up @@ -1818,7 +1818,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
userProvidedTriggers: Option[Seq[Trigger]],
qidPrefix: String,
v: Verifier)
: (InverseFunctions, Seq[Term], Option[Seq[ast.Exp]]) = {
: (InverseFunctions, Seq[Term]) = {

assert(
invertibles.length == codomainQVars.length,
Expand All @@ -1837,7 +1837,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
val imageFunctions = Array.ofDim[Function](qvars.length) /* img_i */
val imagesOfFcts = Array.ofDim[Term](qvars.length) // /* img_i(f_1(xs), ..., f_m(xs)) */
val imagesOfCodomains = Array.ofDim[Term](qvars.length) /* img_i(rs) */
val imagesOfCodomainExps = Option.when(withExp)(Array.ofDim[ast.Exp](qvars.length))
val inversesOfFcts = Array.ofDim[Term](qvars.length) /* inv_i(f_1(xs), ..., f_m(xs)) */
val inversesOfCodomains = Array.ofDim[Term](qvars.length) /* inv_i(rs) */

Expand All @@ -1855,7 +1854,6 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
imageFunctions(idx) = imgFun
imagesOfFcts(idx) = img(invertibles)
imagesOfCodomains(idx) = img(codomainQVars)
if (withExp) imagesOfCodomainExps.get(idx) = ast.FuncApp(imgFun.id.name, additionalInvArgExps.get ++ codomainQVarExps.get.map(_.localVar))(ast.NoPosition, ast.NoInfo, ast.Bool, ast.NoTrafos)
}

/* f_1(inv_1(rs), ..., inv_n(rs)), ..., f_m(inv_1(rs), ..., inv_n(rs)) */
Expand Down Expand Up @@ -1934,7 +1932,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
qvars.zip(inverseFunctions).to(Map),
qvars.zip(imageFunctions).filter(_._2 != null).to(Map)
)
(res, imagesOfCodomains, imagesOfCodomainExps.map(_.toSeq))
(res, imagesOfCodomains)
}

def hintBasedChunkOrderHeuristic(hints: Seq[Term])
Expand Down

0 comments on commit 23986cd

Please sign in to comment.