Skip to content

Commit

Permalink
fix compilation
Browse files Browse the repository at this point in the history
  • Loading branch information
@Felalolf
Felalolf committed Sep 11, 2024
1 parent 112bcf4 commit 4f5bfac
Show file tree
Hide file tree
Showing 2 changed files with 46 additions and 10 deletions.
12 changes: 6 additions & 6 deletions src/main/scala/viper/gobra/translator/transformers/hyper/SIFError.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ import viper.silver.verifier._


case class SIFTerminationChannelCheckFailed(offendingNode: ErrorNode, reason: ErrorReason,
override val cached: Boolean = false) extends AbstractVerificationError {
override val cached: Boolean = false) extends ExtensionAbstractVerificationError {
val id: String = "termination_channel_check.failed"
val text: String = "Termination channel might exist."
override def withNode(offendingNode: ErrorNode = this.offendingNode): ErrorMessage =
Expand All @@ -21,31 +21,31 @@ case class SIFTerminationChannelCheckFailed(offendingNode: ErrorNode, reason: Er
override def withReason(r: ErrorReason): AbstractVerificationError = SIFTerminationChannelCheckFailed(offendingNode, r)
}

case class SIFFoldNotLow(offendingNode: Fold) extends AbstractErrorReason {
case class SIFFoldNotLow(offendingNode: Fold) extends ExtensionAbstractErrorReason {
val id: String = "sif.fold"
val readableMessage: String = s"The low parts of predicate ${offendingNode.acc.loc.predicateName} might not hold."

override def withNode(offendingNode: ErrorNode = this.offendingNode): ErrorMessage =
SIFFoldNotLow(offendingNode.asInstanceOf[Fold])
}

case class SIFUnfoldNotLow(offendingNode: Unfold) extends AbstractErrorReason {
case class SIFUnfoldNotLow(offendingNode: Unfold) extends ExtensionAbstractErrorReason {
val id: String = "sif.unfold"
val readableMessage: String = s"The low parts of predicate ${offendingNode.acc.loc.predicateName} might not hold."

override def withNode(offendingNode: ErrorNode = this.offendingNode): ErrorMessage =
SIFUnfoldNotLow(offendingNode.asInstanceOf[Unfold])
}

case class SIFTermCondNotLow(offendingNode: SIFTerminatesExp) extends AbstractErrorReason {
case class SIFTermCondNotLow(offendingNode: SIFTerminatesExp) extends ExtensionAbstractErrorReason {
val id: String = "sif_termination.condition_not_low"
val readableMessage: String = s"Termination condition ${offendingNode.cond} might not be low."

override def withNode(offendingNode: ErrorNode = this.offendingNode): ErrorMessage =
SIFTermCondNotLow(offendingNode.asInstanceOf[SIFTerminatesExp])
}

case class SIFTermCondLowEvent(offendingNode: SIFTerminatesExp) extends AbstractErrorReason {
case class SIFTermCondLowEvent(offendingNode: SIFTerminatesExp) extends ExtensionAbstractErrorReason {
val id: String = "sif_termination.not_lowevent"
val readableMessage: String =
s"Termination condition ${offendingNode.cond} evaluating to false might not imply both executions don't terminate."
Expand All @@ -54,7 +54,7 @@ case class SIFTermCondLowEvent(offendingNode: SIFTerminatesExp) extends Abstract
SIFTermCondLowEvent(offendingNode.asInstanceOf[SIFTerminatesExp])
}

case class SIFTermCondNotTight(offendingNode: SIFTerminatesExp) extends AbstractErrorReason {
case class SIFTermCondNotTight(offendingNode: SIFTerminatesExp) extends ExtensionAbstractErrorReason {
val id: String = "sif_termination.condition_not_tight"
val readableMessage: String = s"Termination condition ${offendingNode.cond} might not be tight."

Expand Down
44 changes: 40 additions & 4 deletions src/main/scala/viper/gobra/translator/transformers/hyper/SIFLowGuardTransformer.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -131,18 +131,40 @@ trait SIFLowGuardTransformer {
f.copy(name = ctx.rename(f.name))(f.pos, f.info, f.errT)
}

def domain(d: Domain, @unused ctx: Context): Vector[Member] = Vector(d)
def domain(d: Domain, ctx: Context): Vector[Member] = {
val relationalTriggers = d.functions.filter(f => isRelationalTrigger(f.name)).map { f =>
val formalArgs = f.formalArgs.zipWithIndex.map{
case (v: LocalVarDecl, _) => v
case (v: UnnamedLocalVarDecl, idx) => LocalVarDecl(s"""v$idx""", v.typ)(v.pos, v.info, v.errT)
}

val newFormalArgs = formalArgs.map(runLocalVarDecl(_, ctx.major)) ++ formalArgs.map(runLocalVarDecl(_, ctx.minor))
DomainFunc(ctx.predicateFunctionName(f.name), newFormalArgs, Bool)(f.pos,f.info,d.name,f.errT)
}

val relationalAxioms = d.axioms.filter(ax => isRelational(ax.exp, ctx)).map {
case ax: NamedDomainAxiom => ax.copy(exp = assertion(ax.exp, ctx))(ax.pos, ax.info, ax.domainName, ax.errT)
case ax: AnonymousDomainAxiom => ax.copy(exp = assertion(ax.exp, ctx))(ax.pos, ax.info, ax.domainName, ax.errT)
}

Vector(d.copy(
functions = d.functions ++ relationalTriggers,
axioms = d.axioms ++ relationalAxioms,
)(d.pos,d.info,d.errT))
}

def directlyRelational(e: Exp): Boolean = {
e.exists {
case _: SIFLowExp => true
case f: DomainFuncApp => isRelationalTrigger(f.funcname)
case _ => false
}
}

def isRelational(e: Exp, ctx: Context): Boolean = {
e.exists {
case _: SIFLowExp => true
case f: DomainFuncApp => isRelationalTrigger(f.funcname)
case p: PredicateAccess => ctx.isRelationalPredicate(p.predicateName)
case _ => false
}
Expand Down Expand Up @@ -184,6 +206,13 @@ trait SIFLowGuardTransformer {
case l: SIFLowExp => comparison(l, ctx)
case l: SIFLowEventExp => TrueLit()(l.pos, l.info, l.errT)

case a: DomainFuncApp =>
assert(isRelationalTrigger(a.funcname), s"Expected relational trigger, but got $a.")
a.copy(
funcname = ctx.predicateFunctionName(a.funcname),
args = a.args.map(runExp(_, ctx.major)) ++ a.args.map(runExp(_, ctx.minor)),
)(a.pos, a.info, a.typ, a.domainName, a.errT)

case p: PredicateAccess =>
assert(isPositive)
And(positiveUnary(p), predicateAccess(p.predicateName, p.args, ctx)(p.pos, p.info, p.errT))(p.pos, p.info, p.errT)
Expand All @@ -194,8 +223,7 @@ trait SIFLowGuardTransformer {
case f: Forall =>
Forall(
variables = f.variables.map(runLocalVarDecl(_, ctx.major)) ++ f.variables.map(runLocalVarDecl(_, ctx.minor)),
triggers = f.triggers.map(t => Trigger(t.exps.map(runExp(_, ctx.major)))(t.pos, t.info, t.errT)) ++
f.triggers.map(t => Trigger(t.exps.map(runExp(_, ctx.minor)))(t.pos, t.info, t.errT)),
triggers = f.triggers.flatMap(trigger(_, ctx)),
exp = go(f.exp, isPositive),
)(f.pos, f.info, f.errT).autoTrigger

Expand All @@ -217,7 +245,13 @@ trait SIFLowGuardTransformer {
Simplifier.simplify(go(e, isPositive = true))
}


def trigger(t: Trigger, ctx: Context): Vector[Trigger] = {
def triggerExp(e: Exp): Vector[Exp] = {
if (isRelational(e, ctx)) Vector(assertion(e, ctx))
else Vector(runExp(e, ctx.major), runExp(e, ctx.minor))
}
Vector(Trigger(t.exps.flatMap(triggerExp))(t.pos,t.info,t.errT))
}

def predicateAccess(p: String, args: Seq[Exp], ctx: Context)(pos: Position, info: Info, errT: ErrorTrafo): FuncApp = {
FuncApp(
Expand Down Expand Up @@ -450,6 +484,8 @@ trait SIFLowGuardTransformer {
case s: Seqn => s
case s => Seqn(Seq(s), Seq.empty)(s.pos, s.info, s.errT)
}

def isRelationalTrigger(s: String): Boolean = s.startsWith("rel_")
}

trait Context {
Expand Down

0 comments on commit 4f5bfac

Please sign in to comment.