From 8b707528d7a533864f48f758fd3ebaa2eab17877 Mon Sep 17 00:00:00 2001 From: Laurenz Stampfl Date: Fri, 6 Dec 2024 13:19:34 +0100 Subject: [PATCH 1/6] Add some debug stuff --- src/main/scala/viper/silver/ast/Ast.scala | 7 +++++++ src/main/scala/viper/silver/ast/Expression.scala | 2 ++ src/main/scala/viper/silver/ast/Program.scala | 2 ++ 3 files changed, 11 insertions(+) diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala index 304de1bcf..1b7246aef 100644 --- a/src/main/scala/viper/silver/ast/Ast.scala +++ b/src/main/scala/viper/silver/ast/Ast.scala @@ -111,6 +111,13 @@ trait Node extends Iterable[Node] with Rewritable { /** @see [[Visitor.hasSubnode()]] */ def hasSubnode(toFind: Node): Boolean = Visitor.hasSubnode(this, toFind, Nodes.subnodes) + def showSimple = s"${this.getClass.getSimpleName()}" + + def printAll(indent: Int = 0): String = { + val class_name = " ".repeat(indent) + "<" + showSimple + ">"; + this.subnodes.map(n => n.printAll(indent + 4)).foldLeft(class_name)((f, s) => f + "\n" + s) + } + override def toString() = FastPrettyPrinter.pretty(this) def toOneLinerStr() = s"<${getClass.getSimpleName()}> ``" + ( diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala index 1b64f482b..953e00aa8 100644 --- a/src/main/scala/viper/silver/ast/Expression.scala +++ b/src/main/scala/viper/silver/ast/Expression.scala @@ -447,6 +447,8 @@ case class FieldAccess(rcv: Exp, field: Field) def loc(p : Program) = field lazy val typ = field.typ + override def showSimple: String = super.showSimple + s" (${field.name})" + def getArgs: Seq[Exp] = Seq(rcv) def withArgs(args: Seq[Exp]): FieldAccess = copy(rcv = args.head, field)(pos, info, errT) // def asManifestation: Exp = this diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala index e9f2d6eee..e47b97613 100644 --- a/src/main/scala/viper/silver/ast/Program.scala +++ b/src/main/scala/viper/silver/ast/Program.scala @@ -528,6 +528,8 @@ case class LocalVarDecl(name: String, typ: Type)(val pos: Position = NoPosition, * Returns a local variable with equivalent information */ lazy val localVar = LocalVar(name, typ)(pos, info, errT) + + override def showSimple: String = super.showSimple + s" ($name: $typ)" } From b1e39407547c85caa1412e99b54bd05de7fd5e00 Mon Sep 17 00:00:00 2001 From: Laurenz Stampfl Date: Fri, 13 Dec 2024 13:00:50 +0100 Subject: [PATCH 2/6] Form the transitive closure when verifiying a specific method/function --- .../scala/viper/silver/utility/Caching.scala | 77 +++++++++++++------ 1 file changed, 52 insertions(+), 25 deletions(-) diff --git a/src/main/scala/viper/silver/utility/Caching.scala b/src/main/scala/viper/silver/utility/Caching.scala index e8b6eb504..7ad4b910a 100644 --- a/src/main/scala/viper/silver/utility/Caching.scala +++ b/src/main/scala/viper/silver/utility/Caching.scala @@ -19,6 +19,20 @@ trait DependencyAware { val dependencyHashMap: Map[Method, String] + private def handleFunction(p: Program, marker: mutable.Set[Hashable], func: Function): Seq[Hashable] = { + if (!marker.contains(func)) { + markSubAST(func, marker) + Seq(func) ++ getDependenciesRec(p, func.pres ++ func.posts ++ extractOptionalNode(func.body), marker) + } else Nil + } + + private def handlePredicate(p: Program, marker: mutable.Set[Hashable], pred: Predicate): Seq[Hashable] = { + if (!marker.contains(pred)) { + markSubAST(pred, marker) + Seq(pred) ++ getDependenciesRec(p, extractOptionalNode(pred.body), marker) + } else Nil + } + /** * Get the (irreflexive) transitive closure of dependencies of nodes from a list. * @@ -37,20 +51,35 @@ trait DependencyAware { n.deepCollect { case func_app: FuncApp => val func = p.findFunction(func_app.funcname) - if (!marker.contains(func)) { - markSubAST(func, marker) - Seq(func) ++ getDependenciesRec(p, func.pres ++ func.posts ++ extractOptionalNode(func.body), marker) - } else Nil + handleFunction(p, marker, func) case pred_access: PredicateAccess => val pred = p.findPredicate(pred_access.predicateName) - if (!marker.contains(pred)) { - markSubAST(pred, marker) - Seq(pred) ++ getDependenciesRec(p, extractOptionalNode(pred.body), marker) - } else Nil + handlePredicate(p, marker, pred) } flatten } toList } + private def getDependenciesInner(p: Program, m: Method, includeMethods: Boolean): List[Hashable] = { + val marker: mutable.Set[Hashable] = mutable.Set.empty + markSubAST(m, marker) + Seq(m) ++ p.domains ++ p.fields ++ + (m.pres ++ m.posts ++ m.body.toSeq).flatMap { + n => n.deepCollect { + case method_call: MethodCall => + val method = p.findMethod(method_call.methodName) + if (!marker.contains(method)) { + (if(includeMethods) {getDependenciesInner(p, method, includeMethods)} else {Seq()}) ++ method.formalArgs ++ method.formalReturns ++ + method.pres ++ method.posts ++ + getDependenciesRec(p, method.formalArgs ++ method.formalReturns ++ method.pres ++ method.posts, marker) + } else Nil + case func_app: FuncApp => + getDependenciesRec(p, Seq(func_app), marker) + case pred_access: PredicateAccess => + getDependenciesRec(p, Seq(pred_access), marker) + } flatten + } toList + } + /** * Find all (irreflexive) dependencies of the current method. * @@ -70,24 +99,22 @@ trait DependencyAware { * List of dependency [[Hashable]]s. */ def getDependencies(p: Program, m: Method): List[Hashable] = { + getDependenciesInner(p, m, false) + } + + /** + * Same as `getDependencies`, but instead also collects all methods that are used transitively. + * `getDependencies` is used for caching, which for some reason does not include transitively called + * methods (only their pres, posts, etc.). `getDependenciesWithMethods` is instead used for the functionality that allows to verify + * one specific methods, where we need to determine the + */ + def getMethodDependenciesWithMethods(p: Program, m: Method): List[Hashable] = { + getDependenciesInner(p, m, true) + } + + def getFunctionDependencies(p: Program, f: Function): List[Hashable] = { val marker: mutable.Set[Hashable] = mutable.Set.empty - markSubAST(m, marker) - Seq(m) ++ p.domains ++ p.fields ++ - (m.pres ++ m.posts ++ m.body.toSeq).flatMap { - n => n.deepCollect { - case method_call: MethodCall => - val method = p.findMethod(method_call.methodName) - if (!marker.contains(method)) { - method.formalArgs ++ method.formalReturns ++ - method.pres ++ method.posts ++ - getDependenciesRec(p, method.formalArgs ++ method.formalReturns ++ method.pres ++ method.posts, marker) - } else Nil - case func_app: FuncApp => - getDependenciesRec(p, Seq(func_app), marker) - case pred_access: PredicateAccess => - getDependenciesRec(p, Seq(pred_access), marker) - } flatten - } toList + handleFunction(p, marker, f) toList } private def markSubAST(node: Node, marker: mutable.Set[Hashable]): Unit = node.deepCollect { From 2ad251dbbbd72e80821cce17bdcef81337e689ff Mon Sep 17 00:00:00 2001 From: Laurenz Stampfl Date: Mon, 20 Jan 2025 20:23:58 +0100 Subject: [PATCH 3/6] Add verification of a specific target --- src/main/scala/viper/silver/ast/Position.scala | 6 ++++++ src/main/scala/viper/silver/parser/Translator.scala | 6 +++--- src/main/scala/viper/silver/reporter/Message.scala | 8 +++++++- src/main/scala/viper/silver/reporter/Reporter.scala | 6 ++++++ 4 files changed, 22 insertions(+), 4 deletions(-) diff --git a/src/main/scala/viper/silver/ast/Position.scala b/src/main/scala/viper/silver/ast/Position.scala index d353499ac..630ba3e81 100644 --- a/src/main/scala/viper/silver/ast/Position.scala +++ b/src/main/scala/viper/silver/ast/Position.scala @@ -34,6 +34,12 @@ trait HasLineColumn extends Position { else column <= other.column } + def >=(other: HasLineColumn): Boolean = { + if (line > other.line) true + else if (line < other.line) false + else column >= other.column + } + def deltaColumn(delta: Int): HasLineColumn override def toString = s"$line.$column" } diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala index 91653fb3d..14ee4dba8 100644 --- a/src/main/scala/viper/silver/parser/Translator.scala +++ b/src/main/scala/viper/silver/parser/Translator.scala @@ -78,13 +78,13 @@ case class Translator(program: PProgram) { private def translate(m: PMethod): Method = m match { case PMethod(_, _, idndef, _, _, pres, posts, body) => - val m = findMethod(idndef) + val me = findMethod(idndef) val newBody = body.map(actualBody => stmt(actualBody).asInstanceOf[Seqn]) - val finalMethod = m.copy(pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = newBody)(m.pos, m.info, m.errT) + val finalMethod = me.copy(pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = newBody)(me.pos, me.info, me.errT) - members(m.name) = finalMethod + members(me.name) = finalMethod finalMethod } diff --git a/src/main/scala/viper/silver/reporter/Message.scala b/src/main/scala/viper/silver/reporter/Message.scala index 441810eee..fb2333ba6 100644 --- a/src/main/scala/viper/silver/reporter/Message.scala +++ b/src/main/scala/viper/silver/reporter/Message.scala @@ -8,7 +8,7 @@ package viper.silver.reporter import viper.silver.reporter.BackendSubProcessStages.BackendSubProcessStage import viper.silver.verifier._ -import viper.silver.ast.{QuantifiedExp, Trigger} +import viper.silver.ast.{QuantifiedExp, SourcePosition, Trigger} import viper.silver.parser.PProgram /** @@ -180,6 +180,12 @@ case class StatisticsReport(nOfMethods: Int, nOfFunctions: Int, nOfPredicates: I override val name = "statistics" } +case class TargetSelectionReport(target: SourcePosition) extends Message { + + override lazy val toString: String = s"target_selection_report(target=${target})" + override val name: String = "target_selection" +} + case class ProgramOutlineReport(members: List[Entity]) extends Message { override lazy val toString: String = s"program_outline_report(members=${members.map(print)})" diff --git a/src/main/scala/viper/silver/reporter/Reporter.scala b/src/main/scala/viper/silver/reporter/Reporter.scala index 0c51bd50d..b6ae2a462 100644 --- a/src/main/scala/viper/silver/reporter/Reporter.scala +++ b/src/main/scala/viper/silver/reporter/Reporter.scala @@ -48,6 +48,9 @@ case class CSVReporter(name: String = "csv_reporter", path: String = "report.csv warnings.foreach(report => { csv_file.write(s"WarningsDuringParsing,${report}\n") }) + case TargetSelectionReport(ts) => { + csv_file.write(s"TargetSelection,${ts}\n") + } case WarningsDuringTypechecking(warnings) => warnings.foreach(report => { csv_file.write(s"WarningsDuringTypechecking,${report}\n") @@ -153,6 +156,9 @@ case class StdIOReporter(name: String = "stdout_reporter", timeInfo: Boolean = t case AnnotationWarning(text) => println(s"Annotation warning: ${text}") + case TargetSelectionReport(rep) => + println(s"Target selection: ${rep}") + case InvalidArgumentsReport(_, errors) => errors.foreach(e => println(s" ${e.readableMessage}")) println( s"Run with just --help for usage and options" ) From 4c3175e32aa3399c02a9dc00b07f900e8beda68c Mon Sep 17 00:00:00 2001 From: Laurenz Stampfl Date: Mon, 20 Jan 2025 20:40:36 +0100 Subject: [PATCH 4/6] Remove some unnecessary changes --- src/main/scala/viper/silver/ast/Ast.scala | 7 ------- src/main/scala/viper/silver/ast/Expression.scala | 2 -- src/main/scala/viper/silver/parser/Translator.scala | 6 +++--- src/main/scala/viper/silver/utility/Caching.scala | 9 ++++++--- 4 files changed, 9 insertions(+), 15 deletions(-) diff --git a/src/main/scala/viper/silver/ast/Ast.scala b/src/main/scala/viper/silver/ast/Ast.scala index 1b7246aef..304de1bcf 100644 --- a/src/main/scala/viper/silver/ast/Ast.scala +++ b/src/main/scala/viper/silver/ast/Ast.scala @@ -111,13 +111,6 @@ trait Node extends Iterable[Node] with Rewritable { /** @see [[Visitor.hasSubnode()]] */ def hasSubnode(toFind: Node): Boolean = Visitor.hasSubnode(this, toFind, Nodes.subnodes) - def showSimple = s"${this.getClass.getSimpleName()}" - - def printAll(indent: Int = 0): String = { - val class_name = " ".repeat(indent) + "<" + showSimple + ">"; - this.subnodes.map(n => n.printAll(indent + 4)).foldLeft(class_name)((f, s) => f + "\n" + s) - } - override def toString() = FastPrettyPrinter.pretty(this) def toOneLinerStr() = s"<${getClass.getSimpleName()}> ``" + ( diff --git a/src/main/scala/viper/silver/ast/Expression.scala b/src/main/scala/viper/silver/ast/Expression.scala index 953e00aa8..1b64f482b 100644 --- a/src/main/scala/viper/silver/ast/Expression.scala +++ b/src/main/scala/viper/silver/ast/Expression.scala @@ -447,8 +447,6 @@ case class FieldAccess(rcv: Exp, field: Field) def loc(p : Program) = field lazy val typ = field.typ - override def showSimple: String = super.showSimple + s" (${field.name})" - def getArgs: Seq[Exp] = Seq(rcv) def withArgs(args: Seq[Exp]): FieldAccess = copy(rcv = args.head, field)(pos, info, errT) // def asManifestation: Exp = this diff --git a/src/main/scala/viper/silver/parser/Translator.scala b/src/main/scala/viper/silver/parser/Translator.scala index 14ee4dba8..91653fb3d 100644 --- a/src/main/scala/viper/silver/parser/Translator.scala +++ b/src/main/scala/viper/silver/parser/Translator.scala @@ -78,13 +78,13 @@ case class Translator(program: PProgram) { private def translate(m: PMethod): Method = m match { case PMethod(_, _, idndef, _, _, pres, posts, body) => - val me = findMethod(idndef) + val m = findMethod(idndef) val newBody = body.map(actualBody => stmt(actualBody).asInstanceOf[Seqn]) - val finalMethod = me.copy(pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = newBody)(me.pos, me.info, me.errT) + val finalMethod = m.copy(pres = pres.toSeq map (p => exp(p.e)), posts = posts.toSeq map (p => exp(p.e)), body = newBody)(m.pos, m.info, m.errT) - members(me.name) = finalMethod + members(m.name) = finalMethod finalMethod } diff --git a/src/main/scala/viper/silver/utility/Caching.scala b/src/main/scala/viper/silver/utility/Caching.scala index 7ad4b910a..f2d478bd3 100644 --- a/src/main/scala/viper/silver/utility/Caching.scala +++ b/src/main/scala/viper/silver/utility/Caching.scala @@ -104,9 +104,12 @@ trait DependencyAware { /** * Same as `getDependencies`, but instead also collects all methods that are used transitively. - * `getDependencies` is used for caching, which for some reason does not include transitively called - * methods (only their pres, posts, etc.). `getDependenciesWithMethods` is instead used for the functionality that allows to verify - * one specific methods, where we need to determine the + * `getDependencies` is used for caching, which does not include transitively called + * methods (only their pres, posts, etc.). + * + * `getDependenciesWithMethods` is instead used for the IDE functionality that allows to verify + * a method or function at a specific source code location. In this case, we do want to also include + * methods, so that we can form the transitive closure. */ def getMethodDependenciesWithMethods(p: Program, m: Method): List[Hashable] = { getDependenciesInner(p, m, true) From 165b688d9a894caf36af27aed9fe2214989942b5 Mon Sep 17 00:00:00 2001 From: Laurenz Stampfl Date: Mon, 20 Jan 2025 20:41:22 +0100 Subject: [PATCH 5/6] Remove more --- src/main/scala/viper/silver/ast/Program.scala | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/main/scala/viper/silver/ast/Program.scala b/src/main/scala/viper/silver/ast/Program.scala index e47b97613..e9f2d6eee 100644 --- a/src/main/scala/viper/silver/ast/Program.scala +++ b/src/main/scala/viper/silver/ast/Program.scala @@ -528,8 +528,6 @@ case class LocalVarDecl(name: String, typ: Type)(val pos: Position = NoPosition, * Returns a local variable with equivalent information */ lazy val localVar = LocalVar(name, typ)(pos, info, errT) - - override def showSimple: String = super.showSimple + s" ($name: $typ)" } From 6074cfb2969480ef6480281c20465893d86e763e Mon Sep 17 00:00:00 2001 From: Laurenz Stampfl Date: Mon, 20 Jan 2025 21:09:01 +0100 Subject: [PATCH 6/6] Add test for method dependency analysis --- src/test/scala/MethodDependencyTests.scala | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/test/scala/MethodDependencyTests.scala b/src/test/scala/MethodDependencyTests.scala index 497c7fc66..1a66d40a1 100644 --- a/src/test/scala/MethodDependencyTests.scala +++ b/src/test/scala/MethodDependencyTests.scala @@ -135,6 +135,11 @@ class MethodDependencyTests extends AnyFunSuite with Matchers { val computed_deps: List[Hashable] = p.getDependencies(p, test) + // These are for testing the method that also fetches transitive method depdendencies. + val must_be_deps_with_methods: List[Hashable] = List(test) ++ global_deps ++ via_pre_deps ++ via_post_deps ++ via_body_deps ++ transitive_deps ++ List(m0) ++ List(m1) + val must_not_be_deps_with_methods: List[Hashable] = List(fun3, p3) + + val computed_deps_with_methods: List[Hashable] = p.getMethodDependenciesWithMethods(p, test) val test_prefix = s"Test Dependency Analysis" @@ -195,6 +200,14 @@ class MethodDependencyTests extends AnyFunSuite with Matchers { } } + test(s"$test_prefix: do we fetch method dependencies for `getMethodDependenciesWithMethods`?") { + computed_deps_with_methods.foreach { + n => + if ( !must_be_deps_with_methods.contains(n) || must_not_be_deps_with_methods.contains(n) ) + fail(s"AST node ```$n``` is not expected to be a dependency of ```$test```, but is present in the result of `getDependenciesWithMethods`.") + } + } + test(s"$test_prefix: are there duplicated dependencies?") { computed_deps.size should be (computed_deps.distinct.size) }