From f3e488ba196b111d5a847423d040b60dc73aa0ca Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Fri, 30 Apr 2021 20:09:35 +0200 Subject: [PATCH 1/5] Fix selective import --- .../scala/viper/gobra/frontend/Desugar.scala | 2 +- .../info/implementation/TypeInfoImpl.scala | 45 +++++++++++++++- .../import/selective_import/Pkg/test.gobra | 52 +++++++++++++++++++ .../selective-import-simple1.gobra | 33 ++++++++++++ 4 files changed, 130 insertions(+), 2 deletions(-) create mode 100644 src/test/resources/regressions/features/import/selective_import/Pkg/test.gobra create mode 100644 src/test/resources/regressions/features/import/selective_import/selective-import-simple1.gobra diff --git a/src/main/scala/viper/gobra/frontend/Desugar.scala b/src/main/scala/viper/gobra/frontend/Desugar.scala index 55e92bd07..54d26750f 100644 --- a/src/main/scala/viper/gobra/frontend/Desugar.scala +++ b/src/main/scala/viper/gobra/frontend/Desugar.scala @@ -32,7 +32,7 @@ object Desugar { val typeInfo: TypeInfo = tI.getTypeInfo val importedPackage = typeInfo.tree.originalRoot val d = new Desugarer(importedPackage.positions, typeInfo)(config) - (d, d.packageD(importedPackage)) + (d, d.packageD(importedPackage, tI.isUsed)) }} // desugar the main package, i.e. the package on which verification is performed: val mainDesugarer = new Desugarer(pkg.positions, info)(config) diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala index 7a696a5bc..786446fd1 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala @@ -9,6 +9,7 @@ package viper.gobra.frontend.info.implementation import com.typesafe.scalalogging.StrictLogging import org.bitbucket.inkytonik.kiama.attribution.Attribution import viper.gobra.ast.frontend._ +import viper.gobra.ast.frontend.{AstPattern => ap} import viper.gobra.frontend.Config import viper.gobra.frontend.info.base.SymbolTable.{Regular, TypeMember, UnknownEntity, lookup} import viper.gobra.frontend.info.base.{SymbolTable, Type} @@ -87,10 +88,52 @@ class TypeInfoImpl(final val tree: Info.GoTree, final val context: Info.Context, private var externallyAccessedMembers: Vector[PNode] = Vector() private def registerExternallyAccessedEntity(r: SymbolTable.Regular): SymbolTable.Regular = { - if (!externallyAccessedMembers.contains(r.rep)) externallyAccessedMembers = externallyAccessedMembers :+ r.rep + if (!externallyAccessedMembers.contains(r.rep)) { + externallyAccessedMembers = externallyAccessedMembers :+ r.rep + addTransitiveDeps(r) + } r } + private def addTransitiveDeps(r: SymbolTable.Regular): Unit = { + def checkedNodesFromFuncSpec(spec: PFunctionSpec): Vector[PNode] = + spec.pres ++ spec.posts ++ (spec.pres ++ spec.posts) flatMap allChildren + + def handleNodes(checkedNodes: Vector[PNode]): Unit = { + checkedNodes.foreach { + case n: PExpressionOrType => resolve(n) match { + case Some(ap.PredicateCall(p: ap.Symbolic, _)) if !p.isInstanceOf[ap.BuiltInPredicateKind] => + registerExternallyAccessedEntity(p.symb) + case Some(pred: ap.PredicateKind with ap.Symbolic) if !pred.isInstanceOf[ap.BuiltInPredicateKind] => + registerExternallyAccessedEntity(pred.symb) + case Some(ap.FunctionCall(f: ap.Symbolic, _)) if !f.isInstanceOf[ap.BuiltInFunctionKind] => + registerExternallyAccessedEntity(f.symb) + case Some(func: ap.FunctionKind with ap.Symbolic) if !func.isInstanceOf[ap.BuiltInFunctionKind] => + registerExternallyAccessedEntity(func.symb) + case Some(const: ap.Constant) => + // assumes that all constants are global. True for now but may change in the future + registerExternallyAccessedEntity(const.symb) + case _ => + } + case _ => + } + } + + r match { + case SymbolTable.Function(decl, _, _) => + handleNodes(checkedNodesFromFuncSpec(decl.spec)) + case SymbolTable.MethodSpec(sig, _, _, _) => + handleNodes(checkedNodesFromFuncSpec(sig.spec)) + case SymbolTable.MethodImpl(decl, _, _) => + handleNodes(checkedNodesFromFuncSpec(decl.spec)) + case SymbolTable.FPredicate(decl, _) => + decl.body.foreach { body => handleNodes(body +: allChildren(body)) } + case SymbolTable.MPredicateImpl(decl, _) => + decl.body.foreach { body => handleNodes(body +: allChildren(body)) } + case _ => + } + } + override def externalRegular(n: PIdnNode): Option[SymbolTable.Regular] = { // TODO restrict lookup to members starting with a capital letter lookup(topLevelEnvironment, n.name, UnknownEntity()) match { diff --git a/src/test/resources/regressions/features/import/selective_import/Pkg/test.gobra b/src/test/resources/regressions/features/import/selective_import/Pkg/test.gobra new file mode 100644 index 000000000..603ec2873 --- /dev/null +++ b/src/test/resources/regressions/features/import/selective_import/Pkg/test.gobra @@ -0,0 +1,52 @@ +package pkg + +const CONST1 = 1 + +ensures res == CONST1 +func Test1() (res int) { + return CONST1 +} + +ensures res +pure func F(x int) (res bool) + +requires F(x) +func Test2(x int) + +type T struct { + field1 int + field2 string +} + +func Test3(x T) T + +pred P1(x int) + + +pred P2(x int) { + true +} + +pure func G(x int) bool + +pred P3(x int) { + G(x) +} + +requires P1(x) +func Test4(x int) + +requires P2(x) +func Test5(x int) + +requires P3(x) +func Test6(x int) + +pred P4(x int) { + P5(x) +} + +pred P5(x int) + +requires P4(x) +func Test7(x int) \ No newline at end of file diff --git a/src/test/resources/regressions/features/import/selective_import/selective-import-simple1.gobra b/src/test/resources/regressions/features/import/selective_import/selective-import-simple1.gobra new file mode 100644 index 000000000..bffcde4fd --- /dev/null +++ b/src/test/resources/regressions/features/import/selective_import/selective-import-simple1.gobra @@ -0,0 +1,33 @@ +package Test + +// ##(-I ./) +import "pkg" + +func test1(){ + pkg.Test1() + + pkg.Test2(1) + + var t pkg.T = pkg.T{1, "one"} + t := pkg.Test3(t) +} + +func test2() { + //:: ExpectedOutput(precondition_error) + pkg.Test4(1) +} + +func test3() { + //:: ExpectedOutput(precondition_error) + pkg.Test5(2) +} + +func test4() { + //:: ExpectedOutput(precondition_error) + pkg.Test6(2) +} + +func test5() { + //:: ExpectedOutput(precondition_error) + pkg.Test7(2) +} \ No newline at end of file From 1c6eef1833a1b854484a5a1f3c1a0f4f1638d6c0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sun, 2 May 2021 23:14:53 +0200 Subject: [PATCH 2/5] fix directory name --- .../features/import/selective_import/{Pkg => pkg}/test.gobra | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename src/test/resources/regressions/features/import/selective_import/{Pkg => pkg}/test.gobra (100%) diff --git a/src/test/resources/regressions/features/import/selective_import/Pkg/test.gobra b/src/test/resources/regressions/features/import/selective_import/pkg/test.gobra similarity index 100% rename from src/test/resources/regressions/features/import/selective_import/Pkg/test.gobra rename to src/test/resources/regressions/features/import/selective_import/pkg/test.gobra From fa01511193a9e704650398c6f48916674df87f5b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Mon, 3 May 2021 14:55:28 +0200 Subject: [PATCH 3/5] Test with subNodes method --- src/main/scala/viper/gobra/ast/frontend/Ast.scala | 6 ++++++ .../gobra/frontend/info/implementation/TypeInfoImpl.scala | 5 ++++- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index 8958f8293..eb526b8e0 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/src/main/scala/viper/gobra/ast/frontend/Ast.scala @@ -28,6 +28,12 @@ sealed trait PNode extends Product { lazy val formatted: String = pretty() lazy val formattedShort: String = pretty(PNode.shortPrettyPrinter) + def subNodes(): Vector[PNode] = { + val directSubNodes = this.productIterator.toVector.filter(_.isInstanceOf[PNode]).map(_.asInstanceOf[PNode]) + val childrenSubNodes = directSubNodes flatMap (_.subNodes()) + this +: (directSubNodes ++ childrenSubNodes) + } + override def toString: String = formatted } diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala index 786446fd1..30419c5ce 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala @@ -97,9 +97,12 @@ class TypeInfoImpl(final val tree: Info.GoTree, final val context: Info.Context, private def addTransitiveDeps(r: SymbolTable.Regular): Unit = { def checkedNodesFromFuncSpec(spec: PFunctionSpec): Vector[PNode] = - spec.pres ++ spec.posts ++ (spec.pres ++ spec.posts) flatMap allChildren + spec.pres ++ spec.posts ++ (spec.pres ++ spec.posts).flatMap(_.subNodes) + // TODO: check why this causes node not in tree exception + // (try { (spec.pres ++ spec.posts) flatMap allChildren } catch { case e => Seq.empty }) def handleNodes(checkedNodes: Vector[PNode]): Unit = { + println(s"Before Exploding: $checkedNodes") checkedNodes.foreach { case n: PExpressionOrType => resolve(n) match { case Some(ap.PredicateCall(p: ap.Symbolic, _)) if !p.isInstanceOf[ap.BuiltInPredicateKind] => From 6ed90355e0629908b7c67b25c026a1e96607ab6d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sat, 8 May 2021 17:00:37 +0200 Subject: [PATCH 4/5] Added support for profiling --- src/main/scala/viper/gobra/ast/frontend/Ast.scala | 2 ++ .../viper/gobra/ast/frontend/PrettyPrinter.scala | 14 ++++++++++++++ src/main/scala/viper/gobra/frontend/Config.scala | 10 +++++++++- .../info/implementation/TypeInfoImpl.scala | 1 - .../reporting/DefaultMessageBackTranslator.scala | 4 ++-- src/main/scala/viper/gobra/reporting/Message.scala | 10 ++++++---- .../scala/viper/gobra/reporting/Reporter.scala | 5 ++++- 7 files changed, 37 insertions(+), 9 deletions(-) diff --git a/src/main/scala/viper/gobra/ast/frontend/Ast.scala b/src/main/scala/viper/gobra/ast/frontend/Ast.scala index eb526b8e0..74a92743e 100644 --- a/src/main/scala/viper/gobra/ast/frontend/Ast.scala +++ b/src/main/scala/viper/gobra/ast/frontend/Ast.scala @@ -27,6 +27,7 @@ sealed trait PNode extends Product { lazy val formatted: String = pretty() lazy val formattedShort: String = pretty(PNode.shortPrettyPrinter) + lazy val formattedSpecLessShort: String = pretty(PNode.shortSpecLessPrettyPrinter) def subNodes(): Vector[PNode] = { val directSubNodes = this.productIterator.toVector.filter(_.isInstanceOf[PNode]).map(_.asInstanceOf[PNode]) @@ -41,6 +42,7 @@ object PNode { type PPkg = String val defaultPrettyPrinter = new DefaultPrettyPrinter val shortPrettyPrinter = new ShortPrettyPrinter + val shortSpecLessPrettyPrinter = new SpecLessShortPrettyPrinter } sealed trait PScope extends PNode diff --git a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala index b4a349d6e..a0f74183a 100644 --- a/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala +++ b/src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala @@ -638,4 +638,18 @@ class ShortPrettyPrinter extends DefaultPrettyPrinter { showType(ip.subT) <+> "implements" <+> showType(ip.superT) } } +} + +// TODO: Compress with previous one +class SpecLessShortPrettyPrinter extends ShortPrettyPrinter { + override val defaultIndent = 2 + override val defaultWidth = 80 + + override def showMember(mem: PMember): Doc = mem match { + case PFunctionDecl(id, args, res, _, _) => + "func" <+> showId(id) <> parens(showParameterList(args)) <> showResult(res) + case PMethodDecl(id, rec, args, res, _, _) => + "func" <+> showReceiver(rec) <+> showId(id) <> parens(showParameterList(args)) <> showResult(res) + case _ => super.showMember(mem) + } } \ No newline at end of file diff --git a/src/main/scala/viper/gobra/frontend/Config.scala b/src/main/scala/viper/gobra/frontend/Config.scala index 85c022f32..72635a32e 100644 --- a/src/main/scala/viper/gobra/frontend/Config.scala +++ b/src/main/scala/viper/gobra/frontend/Config.scala @@ -171,6 +171,13 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals noshort = true ) + val profiling: ScallopOption[Boolean] = toggle( + name = "profiling", + descrYes = "Print the time it takes to verify each function and method", + default = Some(debug()), + noshort = true + ) + val parseOnly: ScallopOption[Boolean] = toggle( name = "parseOnly", descrYes = "Perform only the parsing step", @@ -367,7 +374,8 @@ class ScallopGobraConfig(arguments: Seq[String], isInputOptional: Boolean = fals goify = goify(), debug = debug(), printInternal = printInternal(), - printVpr = printVpr()), + printVpr = printVpr(), + profiling = profiling()), backend = backend(), z3Exe = z3Exe.toOption, boogieExe = boogieExe.toOption, diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala index 30419c5ce..dd80bd16d 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/TypeInfoImpl.scala @@ -102,7 +102,6 @@ class TypeInfoImpl(final val tree: Info.GoTree, final val context: Info.Context, // (try { (spec.pres ++ spec.posts) flatMap allChildren } catch { case e => Seq.empty }) def handleNodes(checkedNodes: Vector[PNode]): Unit = { - println(s"Before Exploding: $checkedNodes") checkedNodes.foreach { case n: PExpressionOrType => resolve(n) match { case Some(ap.PredicateCall(p: ap.Symbolic, _)) if !p.isInstanceOf[ap.BuiltInPredicateKind] => diff --git a/src/main/scala/viper/gobra/reporting/DefaultMessageBackTranslator.scala b/src/main/scala/viper/gobra/reporting/DefaultMessageBackTranslator.scala index 2769c3c1b..3b928a75b 100644 --- a/src/main/scala/viper/gobra/reporting/DefaultMessageBackTranslator.scala +++ b/src/main/scala/viper/gobra/reporting/DefaultMessageBackTranslator.scala @@ -20,8 +20,8 @@ class DefaultMessageBackTranslator(backTrackInfo: BackTrackInfo, config: Config) private def defaultTranslate: PartialFunction[Message, GobraMessage] = { case m: OverallSuccessMessage => GobraOverallSuccessMessage(m.verifier) case m: OverallFailureMessage => GobraOverallFailureMessage(m.verifier, translate(m.result)) - case EntitySuccessMessage(verifier, Source(info), _, _) => GobraEntitySuccessMessage(verifier, info) - case EntityFailureMessage(verifier, Source(info), _, result, _) => GobraEntityFailureMessage(verifier, info, translate(result)) + case EntitySuccessMessage(verifier, Source(info), time, _) => GobraEntitySuccessMessage(verifier, time, info) + case EntityFailureMessage(verifier, Source(info), time, result, _) => GobraEntityFailureMessage(verifier, time, info, translate(result)) } private def translate(result: VerificationResult): VerifierResult = diff --git a/src/main/scala/viper/gobra/reporting/Message.scala b/src/main/scala/viper/gobra/reporting/Message.scala index 1f7c8e78a..5ae12f20e 100644 --- a/src/main/scala/viper/gobra/reporting/Message.scala +++ b/src/main/scala/viper/gobra/reporting/Message.scala @@ -14,7 +14,7 @@ import viper.gobra.ast.{internal => in} import viper.gobra.reporting.VerifierResult.Success import viper.silver import viper.silver.{ast => vpr} -import viper.silver.reporter.Message +import viper.silver.reporter.{Message, Time} /** * Messages reported by GobraReporter @@ -46,20 +46,22 @@ case class GobraOverallFailureMessage(verifier: String, result: VerifierResult) s"failure=${result.toString})" } -case class GobraEntitySuccessMessage(verifier: String, concerning: Source.Verifier.Info) extends GobraVerificationResultMessage { +case class GobraEntitySuccessMessage(verifier: String, time: Time, concerning: Source.Verifier.Info) extends GobraVerificationResultMessage { override val name: String = s"entity_success_message" val result: VerifierResult = Success override def toString: String = s"entity_success_message(" + s"verifier=${verifier}, " + - s"concerning=${concerning.toString})" + s"time=${time} ms, " + + s"concerning=${concerning.pnode.formattedSpecLessShort})" } -case class GobraEntityFailureMessage(verifier: String, concerning: Source.Verifier.Info, result: VerifierResult) extends GobraVerificationResultMessage { +case class GobraEntityFailureMessage(verifier: String, time: Time, concerning: Source.Verifier.Info, result: VerifierResult) extends GobraVerificationResultMessage { override val name: String = s"entity_failure_message" override def toString: String = s"entity_failure_message(" + s"verifier=${verifier}, " + + s"time=${time} ms, " + s"concerning=${concerning.toString}, " + s"failure=${result.toString})" } diff --git a/src/main/scala/viper/gobra/reporting/Reporter.scala b/src/main/scala/viper/gobra/reporting/Reporter.scala index ca2207479..ec6862cca 100644 --- a/src/main/scala/viper/gobra/reporting/Reporter.scala +++ b/src/main/scala/viper/gobra/reporting/Reporter.scala @@ -39,7 +39,8 @@ case class FileWriterReporter(name: String = "filewriter_reporter", goify: Boolean = false, debug: Boolean = false, printInternal: Boolean = false, - printVpr: Boolean = false) extends GobraReporter { + printVpr: Boolean = false, + profiling: Boolean = false) extends GobraReporter { override def report(msg: GobraMessage): Unit = msg match { case ParsedInputMessage(file, program) if unparse => write(file, "unparsed", program().formatted) case TypeCheckSuccessMessage(file, _, erasedGhostCode, goifiedGhostCode) => @@ -50,6 +51,8 @@ case class FileWriterReporter(name: String = "filewriter_reporter", case AppliedInternalTransformsMessage(file, internal) if printInternal => write(file, "internal", internal().formatted) case m@GeneratedViperMessage(file, _, _) if printVpr => write(file, "vpr", m.vprAstFormatted) case CopyrightReport(text) => println(text) + case msg: GobraEntitySuccessMessage if profiling => println(msg.toString) // TODO: write to file instead? + case msg: GobraEntityFailureMessage if profiling => println(msg.toString) case _ => // ignore } From 77d17ea007d36244094913bca95fbe809feaeb22 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= Date: Sat, 8 May 2021 21:25:25 +0200 Subject: [PATCH 5/5] Add more tests --- .../features/import/selective_import/pkg/test.gobra | 8 +++++++- .../selective_import/selective-import-simple1.gobra | 4 ++++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/test/resources/regressions/features/import/selective_import/pkg/test.gobra b/src/test/resources/regressions/features/import/selective_import/pkg/test.gobra index 603ec2873..345035eae 100644 --- a/src/test/resources/regressions/features/import/selective_import/pkg/test.gobra +++ b/src/test/resources/regressions/features/import/selective_import/pkg/test.gobra @@ -49,4 +49,10 @@ pred P4(x int) { pred P5(x int) requires P4(x) -func Test7(x int) \ No newline at end of file +func Test7(x int) + +func usedInBody() + +func Test8() { + usedInBody() +} \ No newline at end of file diff --git a/src/test/resources/regressions/features/import/selective_import/selective-import-simple1.gobra b/src/test/resources/regressions/features/import/selective_import/selective-import-simple1.gobra index bffcde4fd..4f7a5c6fb 100644 --- a/src/test/resources/regressions/features/import/selective_import/selective-import-simple1.gobra +++ b/src/test/resources/regressions/features/import/selective_import/selective-import-simple1.gobra @@ -30,4 +30,8 @@ func test4() { func test5() { //:: ExpectedOutput(precondition_error) pkg.Test7(2) +} + +func test6() { + pkg.Test8() } \ No newline at end of file