Skip to content

Commit

Permalink
Better displaying of QP chunks, ARP constraints, branch conditions
Browse files Browse the repository at this point in the history
  • Loading branch information
@marcoeilers
marcoeilers committed Sep 1, 2024
1 parent 032990f commit ec5c49d
Show file tree
Hide file tree
Showing 5 changed files with 44 additions and 18 deletions.
26 changes: 17 additions & 9 deletions src/main/scala/debugger/SiliconDebugger.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,16 +52,18 @@ case class ProofObligation(s: State,
}) +
s"\n\t\t${originalErrorReason.readableMessage}\n\n"

private lazy val stateString: String = s"Store:\n\t\t${s.g.values.map(v => s"${v._1} -> ${v._2._2.get}").mkString("\n\t\t")}\n\nHeap:\n\t\t${s.h.values.map(chunkString).mkString("\n\t\t")}\n\n"
private lazy val stateString: String =
s"Store:\n\t\t${s.g.values.map(v => s"${v._1} -> ${v._2._2.get}").mkString("\n\t\t")}\n\nHeap:\n\t\t${s.h.values.map(chunkString).mkString("\n\t\t")}\n\n"

private lazy val branchConditionString: String = s"Branch Conditions:\n\t\t${branchConditions.map(_._2).mkString("\n\t\t")}\n\n"
private lazy val branchConditionString: String =
s"Branch Conditions:\n\t\t${branchConditions.map(bc => Simplifier.simplify(bc._2, true)).filter(bc => bc != ast.TrueLit()()).mkString("\n\t\t")}\n\n"

private def chunkString(c: Chunk): String = {
c match {
val res = c match {
case bc: BasicChunk =>
bc.resourceID match {
case FieldID => s"${bc.argsExp.head}.${bc.id} -> ${bc.snap} # ${Simplifier.simplify(bc.permExp.get, true)}"
case PredicateID => s"${bc.id}(${bc.argsExp.mkString(", ")}) -> ${bc.snap} # ${Simplifier.simplify(bc.permExp.get, true)}"
case FieldID => s"acc(${bc.argsExp.get.head}.${bc.id}, ${Simplifier.simplify(bc.permExp.get, true)})"
case PredicateID => s"acc(${bc.id}(${bc.argsExp.mkString(", ")}), ${Simplifier.simplify(bc.permExp.get, true)})"
}
case mwc: MagicWandChunk =>
val shape = mwc.id.ghostFreeWand
Expand All @@ -72,20 +74,26 @@ case class ProofObligation(s: State,
if (qfc.singletonRcvrExp.isDefined) {
val receiver = Simplifier.simplify(qfc.singletonRcvrExp.get, true)
val perm = Simplifier.simplify(qfc.permExp.get.replace(qfc.quantifiedVarExps.get.head.localVar, receiver), true)
s"${receiver}.${qfc.id} -> ${qfc.fvf} # ${perm}"
s"acc(${receiver}.${qfc.id}, ${perm})"
} else {
val varsString = qfc.quantifiedVarExps.get.map(v => s"${v.name}: ${v.typ}").mkString(", ")
qfc.toString // TODO
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(" && ")
s"forall ${varsString} :: ${qvarsString} :: ${varsEqualString} ==> acc(${qfc.quantifiedVarExps.get.head.name}.${qfc.id}, ${Simplifier.simplify(qfc.permExp.get, true)})"
}
case qpc: QuantifiedPredicateChunk =>
if (qpc.singletonArgExps.isDefined) {
s"${qpc.id}(${qpc.singletonArgExps.get.map(e => Simplifier.simplify(e, true)).mkString(", ")}) -> ${qpc.psf} # ${Simplifier.simplify(qpc.permExp.get, true)}"
s"acc(${qpc.id}(${qpc.singletonArgExps.get.map(e => Simplifier.simplify(e, true)).mkString(", ")}), ${Simplifier.simplify(qpc.permExp.get, true)})"
} else {
qpc.toString // TODO
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(" && ")
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
}
res
}

private def assumptionString: String = {
Expand Down
6 changes: 3 additions & 3 deletions src/main/scala/decider/Decider.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,7 +81,7 @@ trait Decider {

def fresh(sort: Sort, pType: Option[PType]): Var
def fresh(v: ast.AbstractLocalVar): (Var, Option[ast.LocalVarWithVersion])
def freshARP(id: String = "$k"): (Var, Term)
def freshARP(id: String = "$k"): (Var, Term, Option[ast.LocalVarWithVersion])
def appliedFresh(id: String, sort: Sort, appliedArgs: Seq[Term]): App

def generateModel(): Unit
Expand Down Expand Up @@ -452,11 +452,11 @@ trait DefaultDeciderProvider extends VerifierComponent { this: Verifier =>
(term, Option.when(withExp)(LocalVarWithVersion(simplifyVariableName(term.id.name), v.typ)(v.pos, v.info, v.errT)))
}

def freshARP(id: String = "$k"): (Var, Term) = {
def freshARP(id: String = "$k"): (Var, Term, Option[ast.LocalVarWithVersion]) = {
val permVar = prover_fresh[Var](id, Nil, sorts.Perm, true)
val permVarConstraints = IsReadPermVar(permVar)
if (debugMode) debugVariableTypes += (permVar.id.name -> PPrimitiv(PReserved(PKw.Perm)((NoPosition, NoPosition)))())
(permVar, permVarConstraints)
(permVar, permVarConstraints, Option.when(debugMode)(LocalVarWithVersion(simplifyVariableName(permVar.id.name), ast.Perm)()))
}

def freshMacro(id: String, formalArgs: Seq[Var], body: Term): MacroDecl = {
Expand Down
6 changes: 3 additions & 3 deletions src/main/scala/rules/Evaluator.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -182,8 +182,8 @@ object evaluator extends EvaluationRules {
=> Q(s2, t, e0New.map(ast.FractionalPerm(_, e1New.get)(e.pos, e.info, e.errT)), v2)))

case _: ast.WildcardPerm =>
val (tVar, tConstraints) = v.decider.freshARP()
val constraintExp = Option.when(withExp)(DebugExp.createInstance(s"wildcard == ${tVar.toString}", true))
val (tVar, tConstraints, eVar) = v.decider.freshARP()
val constraintExp = Option.when(withExp)(DebugExp.createInstance(s"${eVar.get.toString} > none", true))
v.decider.assumeDefinition(tConstraints, constraintExp)
/* TODO: Only record wildcards in State.constrainableARPs that are used in exhale
* position. Currently, wildcards used in inhale position (only) may not be removed
Expand All @@ -199,7 +199,7 @@ object evaluator extends EvaluationRules {
val s1 =
s.copy(functionRecorder = s.functionRecorder.recordConstrainedVar(tVar, tConstraints))
.setConstrainable(Seq(tVar), true)
Q(s1, tVar, eOpt, v)
Q(s1, tVar, eVar, v)

case fa: ast.FieldAccess if s.qpFields.contains(fa.field) =>
eval(s, fa.rcv, pve, v)((s1, tRcvr, eRcvr, v1) => {
Expand Down
4 changes: 3 additions & 1 deletion src/main/scala/rules/HavocSupporter.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ object havocSupporter extends SymbolicExecutionRules {
pve = pve,
v = v)
{
case (s1, tVars, _, Seq(tCond), _, Some((tArgs, _, Seq(), _, _)), v1) =>
case (s1, tVars, eVars, Seq(tCond), _, Some((tArgs, eArgs, Seq(), _, _)), v1) =>
// Seq() represents an empty list of Triggers
// TODO: unnamed arguments are (tAuxGlobal, tAux) and (auxGlobalsExp, auxNonGlobalsExp). How should these be handled?

Expand Down Expand Up @@ -135,8 +135,10 @@ object havocSupporter extends SymbolicExecutionRules {
// Generate the inverse axioms
val (inverseFunctions, imagesOfCodomain, _) = quantifiedChunkSupporter.getFreshInverseFunctions(
qvars = tVars,
qvarExps = eVars,
condition = tCond,
invertibles = tArgs,
invertibleExps = eArgs,
codomainQVars = codomainQVars,
codomainQVarExps = codomainQVarsExp,
additionalInvArgs = Seq(), // There are no additional quantified vars
Expand Down
20 changes: 18 additions & 2 deletions src/main/scala/rules/QuantifiedChunkSupport.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -33,9 +33,11 @@ import scala.reflect.ClassTag

case class InverseFunctions(condition: Term,
invertibles: Seq[Term],
invertibleExps: Option[Seq[ast.Exp]],
additionalArguments: Vector[Var],
axiomInversesOfInvertibles: Quantification,
axiomInvertiblesOfInverses: Quantification,
qvarExps: Option[Seq[ast.LocalVarDecl]],
qvarsToInverses: Map[Var, Function],
qvarsToImages: Map[Var, Function]) {

Expand Down Expand Up @@ -143,8 +145,10 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
* variables, and thus they only have meaning for the caller).
*/
def getFreshInverseFunctions(qvars: Seq[Var],
qvarExps: Option[Seq[ast.LocalVarDecl]],
condition: Term,
invertibles: Seq[Term],
invertibleExps: Option[Seq[ast.Exp]],
codomainQVars: Seq[Var],
codomainQVarExps: Option[Seq[ast.LocalVarDecl]],
additionalInvArgs: Seq[Var],
Expand Down Expand Up @@ -193,6 +197,7 @@ trait QuantifiedChunkSupport extends SymbolicExecutionRules {
* see [[getFreshInverseFunctions]].
*/
def createQuantifiedChunk(qvars: Seq[Var],
qvarExps: Option[Seq[ast.LocalVarDecl]],
condition: Term,
conditionExp: Option[ast.Exp],
resource: ast.Resource,
Expand Down Expand Up @@ -269,6 +274,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {

/** @inheritdoc [[QuantifiedChunkSupport.createQuantifiedChunk]] */
def createQuantifiedChunk(qvars: Seq[Var],
qvarExps: Option[Seq[ast.LocalVarDecl]],
condition: Term,
conditionExp: Option[ast.Exp],
resource: ast.Resource,
Expand All @@ -290,8 +296,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
val (inverseFunctions, imagesOfCodomain, imagesOfCodomainExp) =
getFreshInverseFunctions(
qvars,
qvarExps,
And(condition, IsPositive(permissions)),
arguments,
argumentExps,
codomainQVars,
codomainQVarExps,
additionalInvArgs,
Expand Down Expand Up @@ -871,6 +879,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
val (ch: QuantifiedBasicChunk, inverseFunctions) =
quantifiedChunkSupporter.createQuantifiedChunk(
qvars = qvars,
qvarExps = qvarExps,
condition = tCond,
conditionExp = eCond,
resource = resource,
Expand Down Expand Up @@ -1105,7 +1114,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
h: Heap,
resource: ast.Resource,
qvars: Seq[Var],
qVarExps: Option[Seq[ast.LocalVarDecl]],
qvarExps: Option[Seq[ast.LocalVarDecl]],
formalQVars: Seq[Var],
formalQVarsExp: Option[Seq[ast.LocalVarDecl]],
qid: String,
Expand All @@ -1132,8 +1141,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
val (inverseFunctions, imagesOfFormalQVars, imagesOfFormalQVarExps) =
quantifiedChunkSupporter.getFreshInverseFunctions(
qvars,
qvarExps,
And(tCond, IsPositive(tPerm)),
tArgs,
eArgs,
formalQVars,
formalQVarsExp,
s.relevantQuantifiedVariables(tArgs).map(_._1),
Expand Down Expand Up @@ -1177,7 +1188,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
val nonNegImplication = Implies(tCond, perms.IsNonNegative(tPerm))
val nonNegImplicationExp = ePerm.map(p => ast.Implies(eCond.get, ast.PermGeCmp(p, ast.NoPerm()())())(p.pos, p.info, p.errT))
val nonNegTerm = Forall(qvars, Implies(FunctionPreconditionTransformer.transform(nonNegImplication, s.program), nonNegImplication), Nil)
val nonNegExp = qVarExps.map(qv => ast.Forall(qv, Nil, nonNegImplicationExp.get)())
val nonNegExp = qvarExps.map(qv => ast.Forall(qv, Nil, nonNegImplicationExp.get)())
// TODO: Replace by QP-analogue of permissionSupporter.assertNotNegative
v.decider.assert(nonNegTerm) {
case true =>
Expand Down Expand Up @@ -1285,6 +1296,7 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
}
val (consumedChunk, inverseFunctions) = quantifiedChunkSupporter.createQuantifiedChunk(
qvars,
qvarExps,
condOfInvOfLoc,
eCond,
resource,
Expand Down Expand Up @@ -1795,8 +1807,10 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
// TODO: Update method's API documentation
/** @inheritdoc [[QuantifiedChunkSupport.getFreshInverseFunctions()]] */
def getFreshInverseFunctions(qvars: Seq[Var], /* xs := x_1, ..., x_n */
qvarExps: Option[Seq[ast.LocalVarDecl]],
condition: Term, /* c(xs) */
invertibles: Seq[Term], /* fs := f_1(xs), ..., f_m(xs) */
invertibleExps: Option[Seq[ast.Exp]],
codomainQVars: Seq[Var], /* rs := r_1, ..., r_m */
codomainQVarExps: Option[Seq[ast.LocalVarDecl]],
additionalInvArgs: Seq[Var],
Expand Down Expand Up @@ -1912,9 +1926,11 @@ object quantifiedChunkSupporter extends QuantifiedChunkSupport {
val res = InverseFunctions(
condition,
invertibles,
invertibleExps,
additionalInvArgs.toVector,
axInvsOfFct,
axFctsOfInvs,
qvarExps,
qvars.zip(inverseFunctions).to(Map),
qvars.zip(imageFunctions).filter(_._2 != null).to(Map)
)
Expand Down

0 comments on commit ec5c49d

Please sign in to comment.