From 2960e1a62643d3af0d3319e85e424cec3d6e0c7e Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 30 Dec 2024 17:36:00 +0100 Subject: [PATCH 1/2] Desugaring quasihavocall to an exhale-inhale --- silver | 2 +- .../scala/viper/carbon/CarbonVerifier.scala | 4 +- .../modules/impls/DefaultMainModule.scala | 52 +++++++++++++++++-- 3 files changed, 50 insertions(+), 8 deletions(-) diff --git a/silver b/silver index 65febaeb..ef4a285c 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit 65febaeb1be635c4f825d1789e5d0e1809f6ef18 +Subproject commit ef4a285c2d81e1c9e2276b50657f99f00c667193 diff --git a/src/main/scala/viper/carbon/CarbonVerifier.scala b/src/main/scala/viper/carbon/CarbonVerifier.scala index f6c55489..c2083e68 100644 --- a/src/main/scala/viper/carbon/CarbonVerifier.scala +++ b/src/main/scala/viper/carbon/CarbonVerifier.scala @@ -161,8 +161,8 @@ case class CarbonVerifier(override val reporter: Reporter, program.shallowCollect( n => n match { - case q: Quasihavocall => - ConsistencyError("Carbon does not support quasihavocall", q.pos) + case q@Quasihavocall(_, _, MagicWand(_, _)) => + ConsistencyError("Carbon does not support quasihavocall of magic wands", q.pos) case q@Quasihavoc(_, MagicWand(_, _)) => ConsistencyError("Carbon does not support quasihavoc of magic wands", q.pos) } diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala index 2a5cf608..f624213f 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala @@ -22,7 +22,9 @@ import viper.silver.verifier.{TypecheckerWarning, errors} import viper.carbon.verifier.Verifier import viper.silver.ast.Quasihavoc import viper.silver.ast.utility.rewriter.Traverse -import viper.silver.reporter.{Reporter, WarningsDuringTypechecking, QuantifierChosenTriggersMessage} +import viper.silver.reporter.{QuantifierChosenTriggersMessage, Reporter, WarningsDuringTypechecking} +import viper.silver.verifier.errors.{ExhaleFailed, HavocallFailed, InhaleFailed} +import viper.silver.verifier.reasons.{QPAssertionNotInjective, QuasihavocallNotInjective} import scala.collection.mutable @@ -72,7 +74,8 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles reporter report QuantifierChosenTriggersMessage(res, res.triggers, e.triggers) res } - case q: Quasihavoc => desugarQuasihavoc(q) + case q: sil.Quasihavoc => desugarQuasihavoc(q) + case q: sil.Quasihavocall => desugarQuasihavocall(q) }, Traverse.TopDown) ) @@ -273,7 +276,10 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles sil.FieldAccessPredicate(r, Some(curPermVar))() case r: sil.PredicateAccess => sil.PredicateAccessPredicate(r, Some(curPermVar))() - case _ => sys.error("Not supported resource in quasihavoc") + case _ => + // Currently no way to desugar magic wands in quasihavoc, since they do not allow exhaling/inhaling specific + // permission amounts, so we cannot exhale the correct amount in case a wand is held more than once. + sys.error("Not supported resource in quasihavoc") } val curPermInhExPermission = @@ -282,8 +288,7 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles Seq( sil.Exhale(resourceCurPerm)(), sil.Inhale(resourceCurPerm)() - ) - , + ), Seq(curPermVarDecl) )() @@ -297,4 +302,41 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles sil.Seqn(curPermInhExPermission, Seq())() } } + + /** * + * Desugar a quasihavocall into an exhale followed by an inhale statement + * + * @param q should be a field or pedicate quasihavocall + * @return + */ + private def desugarQuasihavocall(q: sil.Quasihavocall) = { + val labelName = "perm_temp_quasihavoc_" + val beforeHavocLabelDecl = sil.Label(labelName, Seq())() + val curPermExpr = sil.LabelledOld(sil.CurrentPerm(q.exp)(), labelName)() + val triggers = Seq(sil.Trigger(Seq(q.exp))()) + val resourceCurPerm = + q.exp match { + case r: sil.FieldAccess => + sil.Forall(q.vars, triggers, sil.Implies(q.lhs.getOrElse(sil.TrueLit()()), sil.FieldAccessPredicate(r, Some(curPermExpr))())())() + case r: sil.PredicateAccess => + sil.Forall(q.vars, triggers, sil.Implies(q.lhs.getOrElse(sil.TrueLit()()), sil.PredicateAccessPredicate(r, Some(curPermExpr))())())() + case _ => + // Currently no way to desugar magic wands in quasihavocall, since they do not allow exhaling/inhaling + // specific permission amounts, so we cannot exhale the correct amount in case a wand is held more than once. + sys.error("Not supported resource in quasihavocall") + } + + val errTrafo = sil.ErrTrafo({ + case ExhaleFailed(_, QPAssertionNotInjective(_), cached) => HavocallFailed(q, QuasihavocallNotInjective(q), cached) + case InhaleFailed(_, QPAssertionNotInjective(_), cached) => HavocallFailed(q, QuasihavocallNotInjective(q), cached) + }) + sil.Seqn( + beforeHavocLabelDecl +: + Seq( + sil.Exhale(resourceCurPerm)(errT=errTrafo), + sil.Inhale(resourceCurPerm)(errT=errTrafo) + ), + Seq(beforeHavocLabelDecl) + )() + } } From 18b43d43b963199d82d116861fb3d46e676dc0b6 Mon Sep 17 00:00:00 2001 From: marcoeilers Date: Mon, 30 Dec 2024 17:59:03 +0100 Subject: [PATCH 2/2] Make label and variable names unique --- silver | 2 +- .../modules/impls/DefaultMainModule.scala | 27 ++++++++++++++----- 2 files changed, 22 insertions(+), 7 deletions(-) diff --git a/silver b/silver index ef4a285c..53bd1f6c 160000 --- a/silver +++ b/silver @@ -1 +1 @@ -Subproject commit ef4a285c2d81e1c9e2276b50657f99f00c667193 +Subproject commit 53bd1f6c846ae3ae1bd9ced60e75a42dae41b79a diff --git a/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala b/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala index f624213f..3986d875 100644 --- a/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala +++ b/src/main/scala/viper/carbon/modules/impls/DefaultMainModule.scala @@ -55,6 +55,7 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles override def translate(p: sil.Program, reporter: Reporter): (Program, Map[String, Map[String, String]]) = { + val usedIdentifiers: mutable.HashSet[String] = mutable.HashSet.from(p.transitiveScopedDeclNames) verifier.replaceProgram( p.transform( { @@ -74,8 +75,8 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles reporter report QuantifierChosenTriggersMessage(res, res.triggers, e.triggers) res } - case q: sil.Quasihavoc => desugarQuasihavoc(q) - case q: sil.Quasihavocall => desugarQuasihavocall(q) + case q: sil.Quasihavoc => desugarQuasihavoc(q, usedIdentifiers) + case q: sil.Quasihavocall => desugarQuasihavocall(q, usedIdentifiers) }, Traverse.TopDown) ) @@ -262,13 +263,26 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles res } + private def uniqueName(name: String, usedNames: mutable.HashSet[String]): String = { + var i = 1 + var newName = name + while (usedNames.contains(newName)) { + newName = name + i + i += 1 + } + usedNames.add(newName) + newName + } + /*** * Desugar a quasihavoc into an exhale followed by an inhale statement * @param q should be a field or pedicate quasihavoc + * @param usedNames a set of all names used in the program * @return */ - private def desugarQuasihavoc(q: sil.Quasihavoc) = { - val curPermVarDecl = sil.LocalVarDecl("perm_temp_quasihavoc_", sil.Perm)() + private def desugarQuasihavoc(q: sil.Quasihavoc, usedNames: mutable.HashSet[String]) = { + val permVarName = uniqueName("perm_temp_quasihavoc_", usedNames) + val curPermVarDecl = sil.LocalVarDecl(permVarName, sil.Perm)() val curPermVar = curPermVarDecl.localVar val resourceCurPerm = q.exp match { @@ -307,10 +321,11 @@ class DefaultMainModule(val verifier: Verifier) extends MainModule with Stateles * Desugar a quasihavocall into an exhale followed by an inhale statement * * @param q should be a field or pedicate quasihavocall + * @param usedNames a set of all names used in the program * @return */ - private def desugarQuasihavocall(q: sil.Quasihavocall) = { - val labelName = "perm_temp_quasihavoc_" + private def desugarQuasihavocall(q: sil.Quasihavocall, usedNames: mutable.HashSet[String]) = { + val labelName = uniqueName("perm_temp_quasihavoc_", usedNames) val beforeHavocLabelDecl = sil.Label(labelName, Seq())() val curPermExpr = sil.LabelledOld(sil.CurrentPerm(q.exp)(), labelName)() val triggers = Seq(sil.Trigger(Seq(q.exp))())