Skip to content

Ignore quantified fields/predicates in bodies of called methods #604

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
marcoeilers merged 3 commits into from
Aug 31, 2022
Merged

Ignore quantified fields/predicates in bodies of called methods #604

Changes from 1 commit
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b012f2c
Ignore quantified fields/predicates in bodies of called methods, only…
marcoeilers Aug 29, 2022
4a57829
Simplified after review
marcoeilers Aug 31, 2022
f389208
Merge branch 'master' into meilers_precise_quantified_fields
marcoeilers Aug 31, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
74 changes: 46 additions & 28 deletions src/main/scala/viper/silver/ast/utility/QuantifiedPermissions.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,39 +53,33 @@ 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
}

/* 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
}
Expand All @@ -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))
}
Comment thread
marcoeilers marked this conversation as resolved.
Outdated

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))
Comment thread
marcoeilers marked this conversation as resolved.
Outdated
}

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)
}
}
}
}

Expand Down
⚡