Merge pull request #1067 from utwente-fmt/issue-463

fix #463: consider whether the context is static

src/col/vct/col/resolve/Resolve.scala

@@ -149,7 +149,7 @@ case object ResolveTypes {
       // PB: needs to be in ResolveTypes if we want to support method inheritance at some point.
       cls.supports.foreach(_.tryResolve(name => Spec.findClass(name, ctx).getOrElse(throw NoSuchNameError("class", name, cls))))
     case local: JavaLocal[G] =>
-      Java.findJavaName(local.name, ctx) match {
+      Java.findJavaName(local.name, fromStaticContext = false, ctx) match {
         case Some(
         _: RefVariable[G] | _: RefJavaField[G] | _: RefJavaLocalDeclaration[G] | // Regular names
         _ // Statically imported, or regular previously imported typename
@@ -280,9 +280,13 @@ case object ResolveReferences extends LazyLogging {
       .declare(cls.declarations)
     case method: JavaMethod[G] => ctx
       .copy(currentResult=Some(RefJavaMethod(method)))
+      .copy(inStaticJavaContext=method.modifiers.collectFirst { case _: JavaStatic[_] => () }.nonEmpty)
       .declare(method.declarations ++ method.body.map(scanLabels).getOrElse(Nil))
     case fields: JavaFields[G] => ctx
       .copy(currentInitializerType=Some(fields.t))
+      .copy(inStaticJavaContext=fields.modifiers.collectFirst { case _: JavaStatic[_] => () }.nonEmpty)
+    case init: JavaSharedInitialization[G] => ctx
+      .copy(inStaticJavaContext=init.isStatic)
     case locals: JavaLocalDeclaration[G] => ctx
       .copy(currentInitializerType=Some(locals.t))
     case decl: JavaVariableDeclaration[G] => ctx
@@ -361,7 +365,7 @@ case object ResolveReferences extends LazyLogging {
         Java.findJavaBipGuard(ctx, name).map(RefJavaBipGuard(_))
       } else { None }
       local.ref = Some(start.orElse(
-        Java.findJavaName(name, ctx.asTypeResolutionContext)
+        Java.findJavaName(name, fromStaticContext = ctx.inStaticJavaContext, ctx.asTypeResolutionContext)
           .orElse(Java.findJavaTypeName(Seq(name), ctx.asTypeResolutionContext) match {
             case Some(target: JavaNameTarget[G]) => Some(target)
             case Some(_) | None => None

src/col/vct/col/resolve/ctx/ReferenceResolutionContext.scala

@@ -22,6 +22,7 @@ case class ReferenceResolutionContext[G]
   currentThis: Option[ThisTarget[G]] = None,
   currentResult: Option[ResultTarget[G]] = None,
   currentInitializerType: Option[Type[G]] = None,
+  inStaticJavaContext: Boolean = false,
   javaBipStatePredicates: ListMap[Expr[G], JavaAnnotation[G]] = ListMap[Expr[G], JavaAnnotation[G]](),
   javaBipGuards: ListMap[Expr[G], JavaMethod[G]] = ListMap[Expr[G], JavaMethod[G]](),
   // When true and resolving a local, guard names should also be considered

src/col/vct/col/resolve/lang/Java.scala

@@ -5,7 +5,7 @@ import hre.io.RWFile
 import hre.util.FuncTools
 import vct.col.ast.lang.JavaAnnotationEx
 import vct.col.ast.`type`.TFloats
-import vct.col.ast.{ADTFunction, ApplicableContract, AxiomaticDataType, BipPortType, Block, CType, EmptyProcess, Expr, JavaAnnotation, JavaAnnotationInterface, JavaClass, JavaClassDeclaration, JavaClassOrInterface, JavaConstructor, JavaFields, JavaFinal, JavaImport, JavaInterface, JavaMethod, JavaName, JavaNamedType, JavaNamespace, JavaParam, JavaStatic, JavaTClass, JavaType, JavaVariableDeclaration, LiteralBag, LiteralMap, LiteralSeq, LiteralSet, Node, Null, OptNone, PVLType, TAny, TAnyClass, TArray, TAxiomatic, TBag, TBool, TBoundedInt, TChar, TClass, TEither, TEnum, TFloat, TFraction, TInt, TMap, TMatrix, TModel, TNotAValue, TNothing, TNull, TOption, TPointer, TProcess, TProverType, TRational, TRef, TResource, TSeq, TSet, TString, TTuple, TType, TUnion, TVar, TVoid, TZFraction, Type, UnitAccountedPredicate, Variable, Void}
+import vct.col.ast.{ADTFunction, ApplicableContract, AxiomaticDataType, BipPortType, Block, CType, EmptyProcess, Expr, JavaAnnotation, JavaAnnotationInterface, JavaClass, JavaClassDeclaration, JavaClassOrInterface, JavaConstructor, JavaFields, JavaFinal, JavaImport, JavaInterface, JavaMethod, JavaModifier, JavaName, JavaNamedType, JavaNamespace, JavaParam, JavaStatic, JavaTClass, JavaType, JavaVariableDeclaration, LiteralBag, LiteralMap, LiteralSeq, LiteralSet, Node, Null, OptNone, PVLType, TAny, TAnyClass, TArray, TAxiomatic, TBag, TBool, TBoundedInt, TChar, TClass, TEither, TEnum, TFloat, TFraction, TInt, TMap, TMatrix, TModel, TNotAValue, TNothing, TNull, TOption, TPointer, TProcess, TProverType, TRational, TRef, TResource, TSeq, TSet, TString, TTuple, TType, TUnion, TVar, TVoid, TZFraction, Type, UnitAccountedPredicate, Variable, Void}
 import vct.col.origin._
 import vct.col.ref.Ref
 import vct.col.resolve.ResolveTypes.JavaClassPathEntry
@@ -23,6 +23,7 @@ import java.lang.reflect.{Modifier, Parameter}
 import java.nio.file.Path
 import scala.annotation.tailrec
 import scala.collection.mutable
+import scala.reflect.ClassTag
 
 case object Java extends LazyLogging {
   case class UnexpectedJreDefinition(expectedKind: String, fullyQualifiedName: Seq[String]) extends UserError {
@@ -45,6 +46,13 @@ case object Java extends LazyLogging {
   def JAVA_LANG_STRING: Seq[String] = JAVA_LANG :+ "String"
   def JAVA_LANG: Seq[String] = Seq("java", "lang")
 
+  implicit class ModifiersHelpers[G](modifiers: Seq[JavaModifier[G]]) {
+    def all[T <: JavaModifier[G]](implicit tag: ClassTag[T]): Seq[T] = modifiers.collect { case t: T => t }
+    def first[T <: JavaModifier[G]](implicit tag: ClassTag[T]): Option[T] = modifiers.collectFirst { case t: T => t }
+    def is[T <: JavaModifier[G]](implicit tag: ClassTag[T]): Boolean = first[T].nonEmpty
+    def isNot[T <: JavaModifier[G]](implicit tag: ClassTag[T]): Boolean = first[T].isEmpty
+  }
+
   def findLoadedJavaTypeName[G](potentialFQName: Seq[String], ctx: TypeResolutionContext[G]): Option[JavaTypeNameTarget[G]] = {
     (ctx.stack.lastOption.getOrElse(Seq()) ++ ctx.externallyLoadedElements.flatMap(Referrable.from)).foreach {
       case RefJavaNamespace(ns: JavaNamespace[G]) =>
@@ -277,9 +285,26 @@ case object Java extends LazyLogging {
       }
   }
 
-  def findJavaName[G](name: String, ctx: TypeResolutionContext[G]): Option[JavaNameTarget[G]] = {
+  def allowedFromStaticContext[G](target: JavaNameTarget[G]): Boolean = target match {
+    case RefAxiomaticDataType(_) => true
+    case RefClass(_) => true // PB: except maybe in non-static inner classes?
+    case RefEnum(_) => true
+    case RefEnumConstant(_, _) => true
+    case RefJavaClass(decl) => true
+    case RefUnloadedJavaNamespace(names) => true
+
+    case RefJavaField(decls, _) => decls.modifiers.is[JavaStatic[G]]
+    case RefModelField(_) => false
+    case RefJavaBipGuard(_) => false
+
+    case RefVariable(_) => true
+    case RefJavaLocalDeclaration(_, _) => true
+    case RefJavaParam(_) => true
+  }
+
+  def findJavaName[G](name: String, fromStaticContext: Boolean, ctx: TypeResolutionContext[G]): Option[JavaNameTarget[G]] = {
     ctx.stack.flatten.collectFirst {
-      case target: JavaNameTarget[G] if target.name == name => target
+      case target: JavaNameTarget[G] if target.name == name && (!fromStaticContext || allowedFromStaticContext(target)) => target
     }.orElse(ctx.namespace.flatMap(ns => {
       // PB: I optionified this, but not entirely sure what the intention is here.
       def classOrEnum(target: JavaTypeNameTarget[G]): Option[JavaNameTarget[G]] = target match {
@@ -311,7 +336,7 @@ case object Java extends LazyLogging {
             .getOrElse(RefUnloadedJavaNamespace(pkg :+ name)))
         case RefJavaClass(decl) =>
           decl.decls.flatMap(Referrable.from).collectFirst {
-            case ref @ RefJavaField(decls, idx) if ref.name == name && ref.decls.modifiers.contains(JavaStatic[G]()) => ref
+            case ref @ RefJavaField(decls, idx) if ref.name == name && ref.decls.modifiers.is[JavaStatic[G]] => ref
           }
         case RefEnum(enum) =>
           enum.getConstant(name)
@@ -321,18 +346,18 @@ case object Java extends LazyLogging {
         case ref @ RefModelField(_) if ref.name == name => ref
       }
       case JavaTClass(Ref(cls), _) => cls.decls.flatMap(Referrable.from).collectFirst {
-        case ref @ RefJavaField(_, _) if ref.name == name && !ref.decls.modifiers.contains(JavaStatic[G]()) => ref
+        case ref @ RefJavaField(_, _) if ref.name == name && !ref.decls.modifiers.is[JavaStatic[G]] => ref
       }
       case _ => None
     }) : Option[JavaDerefTarget[G]]).orElse[JavaDerefTarget[G]](Spec.builtinField(obj, name, blame))
 
-  def findMethodInClass[G](cls: JavaClassOrInterface[G], method: String, args: Seq[Expr[G]]): Option[JavaInvocationTarget[G]] =
+  def findMethodInClass[G](cls: JavaClassOrInterface[G], fromStaticContext: Boolean, method: String, args: Seq[Expr[G]]): Option[JavaInvocationTarget[G]] =
     cls.decls.flatMap(Referrable.from).collectFirst {
-      case ref: RefJavaMethod[G] if ref.name == method && Util.compatJavaParams(args, ref.decl.parameters) => ref
-      case ref: RefJavaAnnotationMethod[G] if ref.name == method && args.length == 0 => ref
-      case ref: RefInstanceFunction[G] if ref.name == method && Util.compat(args, ref.decl.args) => ref
-      case ref: RefInstanceMethod[G] if ref.name == method && Util.compat(args, ref.decl.args) => ref
-      case ref: RefInstancePredicate[G] if ref.name == method && Util.compat(args, ref.decl.args) => ref
+      case ref: RefJavaMethod[G] if ref.name == method && Util.compatJavaParams(args, ref.decl.parameters) && (!fromStaticContext || ref.decl.modifiers.is[JavaStatic[G]]) => ref
+      case ref: RefJavaAnnotationMethod[G] if ref.name == method && args.isEmpty && !fromStaticContext => ref
+      case ref: RefInstanceFunction[G] if ref.name == method && Util.compat(args, ref.decl.args) && !fromStaticContext => ref
+      case ref: RefInstanceMethod[G] if ref.name == method && Util.compat(args, ref.decl.args) && !fromStaticContext => ref
+      case ref: RefInstancePredicate[G] if ref.name == method && Util.compat(args, ref.decl.args) && !fromStaticContext => ref
     }
 
   @tailrec
@@ -342,9 +367,9 @@ case object Java extends LazyLogging {
         case ref: RefModelAction[G] if ref.name == method => ref
         case ref: RefModelProcess[G] if ref.name == method => ref
       }
-      case JavaTClass(Ref(cls), Nil) => findMethodInClass(cls, method, args)
+      case JavaTClass(Ref(cls), Nil) => findMethodInClass(cls, fromStaticContext = false, method, args)
       case TUnion(ts) => findMethodOnType(ctx, Types.leastCommonSuperType(ts), method, args)
-      case TNotAValue(RefJavaClass(cls: JavaClassOrInterface[G @unchecked])) => findMethodInClass[G](cls, method, args)
+      case TNotAValue(RefJavaClass(cls: JavaClassOrInterface[G @unchecked])) => findMethodInClass[G](cls, fromStaticContext = true, method, args)
       case TNotAValue(RefAxiomaticDataType(adt: AxiomaticDataType[G @unchecked])) => adt.decls.flatMap(Referrable.from).collectFirst {
         case ref: RefADTFunction[G] if ref.name == method && Util.compat(args, ref.decl.args) => ref
       }
@@ -354,12 +379,15 @@ case object Java extends LazyLogging {
   def findMethod[G](ctx: ReferenceResolutionContext[G], obj: Expr[G], method: String, args: Seq[Expr[G]], blame: Blame[BuiltinError]): Option[JavaInvocationTarget[G]] =
     findMethodOnType(ctx, obj.t, method, args).orElse(Spec.builtinInstanceMethod(obj, method, blame))
 
+  def matchesStatic(ctx: ReferenceResolutionContext[_], modifiers: Seq[JavaModifier[_]]): Boolean =
+    !ctx.inStaticJavaContext || modifiers.collectFirst { case _: JavaStatic[_] => () }.nonEmpty
+
   def findMethod[G](ctx: ReferenceResolutionContext[G], method: String, args: Seq[Expr[G]]): Option[JavaInvocationTarget[G]] = {
     val selectMatchingSignature: PartialFunction[Referrable[G], JavaInvocationTarget[G]] = {
-      case ref: RefJavaMethod[G] if ref.name == method && Util.compatJavaParams(args, ref.decl.parameters) => ref
-      case ref: RefInstanceFunction[G] if ref.name == method && Util.compat(args, ref.decl.args) => ref
-      case ref: RefInstanceMethod[G] if ref.name == method && Util.compat(args, ref.decl.args) => ref
-      case ref: RefInstancePredicate[G] if ref.name == method && Util.compat(args, ref.decl.args) => ref
+      case ref: RefJavaMethod[G] if ref.name == method && Util.compatJavaParams(args, ref.decl.parameters) && matchesStatic(ctx, ref.decl.modifiers) => ref
+      case ref: RefInstanceFunction[G] if ref.name == method && Util.compat(args, ref.decl.args) && !ctx.inStaticJavaContext => ref
+      case ref: RefInstanceMethod[G] if ref.name == method && Util.compat(args, ref.decl.args) && !ctx.inStaticJavaContext => ref
+      case ref: RefInstancePredicate[G] if ref.name == method && Util.compat(args, ref.decl.args) && !ctx.inStaticJavaContext => ref
       case ref: RefFunction[G] if ref.name == method && Util.compat(args, ref.decl.args) => ref
       case ref: RefProcedure[G] if ref.name == method && Util.compat(args, ref.decl.args) => ref
       case ref: RefPredicate[G] if ref.name == method && Util.compat(args, ref.decl.args) => ref

test/main/vct/test/integration/features/ResolutionSpec.scala

@@ -0,0 +1,41 @@
+package vct.test.integration.features
+
+import vct.test.integration.helper.VercorsSpec
+
+class ResolutionSpec extends VercorsSpec {
+  vercors should error withCode "noSuchName" in "example with incorrect usage from static context: single name invocation" java """
+    class Test {
+      //@ resource x() = true;
+
+      //@ requires x();
+      static void bar() {}
+    }
+  """
+
+  vercors should error withCode "noSuchName" in "example with incorrect usage from static context: qualified invocation" java """
+    class Test {
+      //@ resource x() = true;
+
+      //@ requires Test.x();
+      static void bar() {}
+    }
+  """
+
+  vercors should error withCode "noSuchName" in "example with incorrect usage from static context: single name" java """
+    class Test {
+      int x;
+
+      //@ requires x == 5;
+      static void bar() {}
+    }
+  """
+
+  vercors should error withCode "noSuchName" in "example with incorrect usage from static context: qualified name" java """
+    class Test {
+      int x;
+
+      //@ requires Test.x == 5;
+      static void bar() {}
+    }
+  """
+}

test/main/vct/test/integration/meta/ExampleCoverage.scala

@@ -2,7 +2,8 @@ package vct.test.integration.meta
 
 import org.scalatest.flatspec.AnyFlatSpec
 import vct.test.integration.examples._
-import vct.test.integration.helper.{ExampleFiles, VercorsSpec}
+import vct.test.integration.features._
+import vct.test.integration.helper._
 
 class ExampleCoverage extends AnyFlatSpec {
   it should "cover all examples in the examples directory" in {
@@ -34,6 +35,7 @@ class ExampleCoverage extends AnyFlatSpec {
       new PredicatesSpec(),
       new PublicationsSpec(),
       new RefuteSpec(),
+      new ResolutionSpec(),
       new SequencesSpec(),
       new SetsSpec(),
       new SilverDomainSpec(),