Fix selective import

src/main/scala/viper/gobra/ast/frontend/Ast.scala

@@ -28,6 +28,13 @@ 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])
+    val childrenSubNodes = directSubNodes flatMap (_.subNodes())
+    this +: (directSubNodes ++ childrenSubNodes)
+  }
 
   override def toString: String = formatted
 }
@@ -36,6 +43,7 @@ object PNode {
   type PPkg = String
   val defaultPrettyPrinter = new DefaultPrettyPrinter
   val shortPrettyPrinter = new ShortPrettyPrinter
+  val shortSpecLessPrettyPrinter = new SpecLessShortPrettyPrinter
 }
 
 sealed trait PScope extends PNode

src/main/scala/viper/gobra/ast/frontend/PrettyPrinter.scala

@@ -663,4 +663,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)
+  }
 }

src/main/scala/viper/gobra/frontend/Config.scala

@@ -172,6 +172,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",
@@ -368,7 +375,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,

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)

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,54 @@ 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(_.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 = {
+      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 {

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 =

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

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
   }
 

src/test/resources/regressions/features/import/selective_import/pkg/test.gobra

@@ -0,0 +1,58 @@
+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)
+
+func usedInBody()
+
+func Test8() {
+    usedInBody()
+}

src/test/resources/regressions/features/import/selective_import/selective-import-simple1.gobra

@@ -0,0 +1,37 @@
+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)
+}
+
+func test6() {
+    pkg.Test8()
+}