From 36012471b7515a0102acac2028bff81a203dba9b Mon Sep 17 00:00:00 2001 From: Pieter Bos Date: Mon, 9 Oct 2023 12:37:43 +0200 Subject: [PATCH] fix #463: consider whether the context is static when resolving loose names, and derefences/invocations of class names --- src/col/vct/col/resolve/Resolve.scala | 8 ++- .../ctx/ReferenceResolutionContext.scala | 1 + src/col/vct/col/resolve/lang/Java.scala | 62 ++++++++++++++----- .../integration/features/ResolutionSpec.scala | 41 ++++++++++++ .../integration/meta/ExampleCoverage.scala | 4 +- 5 files changed, 96 insertions(+), 20 deletions(-) create mode 100644 test/main/vct/test/integration/features/ResolutionSpec.scala diff --git a/src/col/vct/col/resolve/Resolve.scala b/src/col/vct/col/resolve/Resolve.scala index bafced31c0..0dd8c0f33b 100644 --- a/src/col/vct/col/resolve/Resolve.scala +++ b/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 diff --git a/src/col/vct/col/resolve/ctx/ReferenceResolutionContext.scala b/src/col/vct/col/resolve/ctx/ReferenceResolutionContext.scala index f96b748160..e0ef142ed4 100644 --- a/src/col/vct/col/resolve/ctx/ReferenceResolutionContext.scala +++ b/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 diff --git a/src/col/vct/col/resolve/lang/Java.scala b/src/col/vct/col/resolve/lang/Java.scala index b60168d399..285db39e29 100644 --- a/src/col/vct/col/resolve/lang/Java.scala +++ b/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 diff --git a/test/main/vct/test/integration/features/ResolutionSpec.scala b/test/main/vct/test/integration/features/ResolutionSpec.scala new file mode 100644 index 0000000000..1ecc59ce99 --- /dev/null +++ b/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() {} + } + """ +} diff --git a/test/main/vct/test/integration/meta/ExampleCoverage.scala b/test/main/vct/test/integration/meta/ExampleCoverage.scala index 816df554d6..d4472e8120 100644 --- a/test/main/vct/test/integration/meta/ExampleCoverage.scala +++ b/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(),