From b012f2c541009685c2cf17a582559eccf5fd51ac Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Mon, 29 Aug 2022 15:03:13 +0200 Subject: [PATCH 1/2] Ignore quantified fields/predicates in bodies of called methods, only use their spec --- .../ast/utility/QuantifiedPermissions.scala | 74 ++++++++++++------- 1 file changed, 46 insertions(+), 28 deletions(-) diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala index 11324e86b..ebc6820f2 100644 --- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala +++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala @@ -53,19 +53,16 @@ object QuantifiedPermissions { * e.g. someMethod.quantifiedFields. */ - def quantifiedFields(root: Node, program: Program): collection.Set[Field] = { + def quantifiedFields(root: Member, program: Program): collection.Set[Field] = { val collected = mutable.LinkedHashSet[Field]() val visited = mutable.Set[Member]() val toVisit = mutable.Queue[Member]() - root match { - case m: Member => toVisit += m - case _ => - } + toVisit += root toVisit ++= Nodes.referencedMembers(root, program) - quantifiedFields(toVisit, collected, visited, program) + quantifiedFields(toVisit, root, collected, visited, program) collected } @@ -73,19 +70,16 @@ object QuantifiedPermissions { /* TODO: See comment above about caching * TODO: Unify with corresponding code for fields */ - def quantifiedPredicates(root: Node, program: Program): collection.Set[Predicate] = { + def quantifiedPredicates(root: Member, program: Program): collection.Set[Predicate] = { val collected = mutable.LinkedHashSet[Predicate]() val visited = mutable.Set[Member]() val toVisit = mutable.Queue[Member]() - root match { - case m: Member => toVisit += m - case _ => - } + toVisit += root toVisit ++= Nodes.referencedMembers(root, program) - quantifiedPredicates(toVisit, collected, visited, program) + quantifiedPredicates(toVisit, root, collected, visited, program) collected } @@ -98,44 +92,68 @@ object QuantifiedPermissions { } private def quantifiedFields(toVisit: mutable.Queue[Member], + root: Member, collected: mutable.LinkedHashSet[Field], visited: mutable.Set[Member], program: Program): Unit = { while (toVisit.nonEmpty) { - val root = toVisit.dequeue() + val currentRoot = toVisit.dequeue() - root visit { - case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) => - collected += acc.loc.field - case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field} + val relevantNodes: Map[Member, Seq[Node]] = currentRoot match { + case m@Method(_, _, _, pres, posts, _) if m != root => + // use only specification of called methods + Map(m -> (pres ++ posts)) + case _ => Map(currentRoot -> Seq(currentRoot)) } - visited += root + for ((member, ns) <- relevantNodes.toIndexedSeq) { + visited += member + + for (n <- ns){ + n visit { + case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) => + collected += acc.loc.field + case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field} + } + utility.Nodes.referencedMembers(n, program) foreach (m => + if (!visited.contains(m)) toVisit += m) - utility.Nodes.referencedMembers(root, program) foreach (m => - if (!visited.contains(m)) toVisit += m) + } + } } } private def quantifiedPredicates(toVisit: mutable.Queue[Member], + root: Member, collected: mutable.LinkedHashSet[Predicate], visited: mutable.Set[Member], program: Program): Unit = { while (toVisit.nonEmpty) { - val root = toVisit.dequeue() + val currentRoot = toVisit.dequeue() - root visit { - case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) => - collected += program.findPredicate(acc.loc.predicateName) - case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)} + val relevantNodes: Map[Member, Seq[Node]] = currentRoot match { + case m@Method(_, _, _, pres, posts, _) if m != root => + // use only specification of called methods + Map(m -> (pres ++ posts)) + case _ => Map(currentRoot -> Seq(currentRoot)) } - visited += root + for ((member, ns) <- relevantNodes.toIndexedSeq) { + visited += member + + for (n <- ns){ + n visit { + case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) => + collected += program.findPredicate(acc.loc.predicateName) + case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)} + } + utility.Nodes.referencedMembers(n, program) foreach (m => + if (!visited.contains(m)) toVisit += m) - utility.Nodes.referencedMembers(root, program) foreach (m => - if (!visited.contains(m)) toVisit += m) + } + } } } From 4a5782916dd80a21c2a5e4730b8595dc7ed529f4 Mon Sep 17 00:00:00 2001 From: Marco Eilers Date: Wed, 31 Aug 2022 11:51:22 +0200 Subject: [PATCH 2/2] Simplified after review --- .../ast/utility/QuantifiedPermissions.scala | 51 +++++++++---------- 1 file changed, 23 insertions(+), 28 deletions(-) diff --git a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala index ebc6820f2..76e589655 100644 --- a/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala +++ b/src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala @@ -100,26 +100,23 @@ object QuantifiedPermissions { while (toVisit.nonEmpty) { val currentRoot = toVisit.dequeue() - val relevantNodes: Map[Member, Seq[Node]] = currentRoot match { + val relevantNodes: Seq[Node] = currentRoot match { case m@Method(_, _, _, pres, posts, _) if m != root => // use only specification of called methods - Map(m -> (pres ++ posts)) - case _ => Map(currentRoot -> Seq(currentRoot)) + pres ++ posts + case _ => Seq(currentRoot) } - for ((member, ns) <- relevantNodes.toIndexedSeq) { - visited += member - - for (n <- ns){ - n visit { - case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) => - collected += acc.loc.field - case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field} - } - utility.Nodes.referencedMembers(n, program) foreach (m => - if (!visited.contains(m)) toVisit += m) + visited += currentRoot + for (n <- relevantNodes){ + n visit { + case QuantifiedPermissionAssertion(_, _, acc: FieldAccessPredicate) => + collected += acc.loc.field + case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case fa: FieldAccess => fa.field} } + utility.Nodes.referencedMembers(n, program) foreach (m => + if (!visited.contains(m)) toVisit += m) } } } @@ -133,26 +130,24 @@ object QuantifiedPermissions { while (toVisit.nonEmpty) { val currentRoot = toVisit.dequeue() - val relevantNodes: Map[Member, Seq[Node]] = currentRoot match { + val relevantNodes: Seq[Node] = currentRoot match { case m@Method(_, _, _, pres, posts, _) if m != root => // use only specification of called methods - Map(m -> (pres ++ posts)) - case _ => Map(currentRoot -> Seq(currentRoot)) + pres ++ posts + case _ => Seq(currentRoot) } - for ((member, ns) <- relevantNodes.toIndexedSeq) { - visited += member - - for (n <- ns){ - n visit { - case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) => - collected += program.findPredicate(acc.loc.predicateName) - case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)} - } - utility.Nodes.referencedMembers(n, program) foreach (m => - if (!visited.contains(m)) toVisit += m) + visited += currentRoot + for (n <- relevantNodes){ + n visit { + case QuantifiedPermissionAssertion(_, _, acc: PredicateAccessPredicate) => + collected += program.findPredicate(acc.loc.predicateName) + case Forall(_,triggers,_) => collected ++= triggers flatMap (_.exps) collect {case pa: PredicateAccess => pa.loc(program)} } + utility.Nodes.referencedMembers(n, program) foreach (m => + if (!visited.contains(m)) toVisit += m) + } } }