use ScopedStack + example

sakehl · May 21, 2024 · a35ebe0 · a35ebe0
1 parent 4c01568
commit a35ebe0
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 10 deletions.
diff --git a/src/rewrite/vct/rewrite/ExtractInlineQuantifierPatterns.scala b/src/rewrite/vct/rewrite/ExtractInlineQuantifierPatterns.scala
@@ -33,14 +33,14 @@ case class ExtractInlineQuantifierPatterns[Pre <: Generation]() extends Rewriter
 
   case class MakePattern(pattern: Pattern) extends Rewriter[Pre] {
     override val allScopes = outer.allScopes
-    var inScale: Boolean = false
+    val inScale: ScopedStack[Unit] = ScopedStack()
 
     override def dispatch(e: Expr[Pre]): Expr[Post] = e match {
       // PB: don't add nodes here just to be conservative: in general all terms are allowable in patterns, *except*
       // that z3 disallows all Bool-related operators, and Viper additionally disallows all arithmetic operators. Any
       // other operators is necessarily encoded as an smt function (allowed), or banned due to being a side effect
       // (later dealt with rigorously).
-      case e if inScale => e.rewriteDefault()
+      case e if inScale.nonEmpty => e.rewriteDefault()
 
       case And(_, _) | Or(_, _) | Implies(_, _) | Star(_, _) | Wand(_, _) | PolarityDependent(_, _) =>
         throw NotAllowedInTrigger(e)
@@ -59,9 +59,9 @@ case class ExtractInlineQuantifierPatterns[Pre <: Generation]() extends Rewriter
       case Local(Ref(v)) if pattern.letBindingsHere.contains(v) => dispatch(pattern.letBindingsHere(v))
 
       case p@PredicateApply(ref, args, perm) =>
-        inScale = true
-        val newPerm = dispatch(perm)
-        inScale = false
+        val newPerm = inScale.having(()){
+          dispatch(perm)
+        }
         PredicateApply(succ[Predicate[Post]](ref.decl), args.map(dispatch), newPerm)(e.o)
 
       case e => rewriteDefault(e)

diff --git a/src/viper/viper/api/transform/ColToSilver.scala b/src/viper/viper/api/transform/ColToSilver.scala
@@ -39,7 +39,7 @@ case class ColToSilver(program: col.Program[_]) {
   val currentMapGet: ScopedStack[col.MapGet[_]] = ScopedStack()
   val currentDividingExpr: ScopedStack[col.DividingExpr[_]] = ScopedStack()
 
-  var inTriggers = false
+  val inTriggers: ScopedStack[Unit] = ScopedStack()
 
   case class NotSupported(node: col.Node[_]) extends SystemError {
     override def text: String =
@@ -324,9 +324,9 @@ case class ColToSilver(program: col.Program[_]) {
       scoped {
         currentStarall.having(starall) {
           val newBindings = bindings.map(variable)
-          inTriggers = true
-          val newTriggers = triggers.map(trigger)
-          inTriggers = false
+          val newTriggers = inTriggers.having(()) {
+             triggers.map(trigger)
+          }
           val foralls: Seq[silver.Forall] = silver.utility.QuantifiedPermissions.desugarSourceQuantifiedPermissionSyntax(
             silver.Forall(newBindings, newTriggers, exp(body))(pos=pos(e), info=expInfo(e))
           )
@@ -356,7 +356,7 @@ case class ColToSilver(program: col.Program[_]) {
       permValue.info.asInstanceOf[NodeInfo[_]].permissionValuePermissionNode = Some(res)
       silver.FieldAccessPredicate(silver.FieldAccess(exp(obj), fields(field))(pos=pos(res), info=expInfo(res)), permValue)(pos=pos(res), info=expInfo(res))
     case res: col.PredicateApply[_] =>
-      if(inTriggers){
+      if(inTriggers.nonEmpty){
         return predInTrigger(res)
       }
       val silver = pred(res)

diff --git a/test/main/vct/test/integration/examples/PredicatesSpec.scala b/test/main/vct/test/integration/examples/PredicatesSpec.scala
@@ -10,4 +10,20 @@ class PredicatesSpec extends VercorsSpec {
    vercors should verify using silicon example "concepts/predicates/ScaleInlinePredicate.pvl"
   // https://github.com/utwente-fmt/vercors/discussions/842
   // vercors should verify using silicon example "concepts/predicates/TreeRecursive.java"
+
+  vercors should verify using anyBackend in "using predicate (with scale) in a trigger" pvl """
+resource x_perm(int x, int n, int[] data) =  (data != null && data.length == n && n>0 && x >= 0 && x < n) ** Perm(data[x], write);
+
+  context (\forall* int i=0..n; {:x_perm(i, n, xs):});
+  context (\forall* int i=0..n; {:[1\2]x_perm(i, n, ys):});
+void main(int[] xs, int[] ys, int n){
+  if(n>0){
+    unfold x_perm(0, n, xs);
+    unfold [1\2]x_perm(0, n, ys);
+    xs[0] = ys[0];
+    fold [1\2]x_perm(0, n, ys);
+    fold x_perm(0, n, xs);
+  }
 }
+  """
+}