diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/JFrameRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/JFrameRefinements.java new file mode 100644 index 00000000..e5fb3730 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/JFrameRefinements.java @@ -0,0 +1,18 @@ +package testSuite.classes.inherited_external_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("javax.swing.JFrame") +public interface JFrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void JFrame(String title); + + @StateRefinement(to = "displayable(this)") + void pack(); + + @StateRefinement(from = "notDisplayable(this)") + void setUndecorated(boolean undecorated); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/UseFrame.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/UseFrame.java new file mode 100644 index 00000000..d6c6566b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_correct/UseFrame.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_external_correct; + +import javax.swing.JFrame; + +public class UseFrame { + static void configure() { + JFrame frame = new JFrame("example"); + frame.setUndecorated(true); + frame.pack(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/JFrameRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/JFrameRefinements.java new file mode 100644 index 00000000..1c08cfab --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/JFrameRefinements.java @@ -0,0 +1,18 @@ +package testSuite.classes.inherited_external_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"displayable", "notDisplayable"}) +@ExternalRefinementsFor("javax.swing.JFrame") +public interface JFrameRefinements { + @StateRefinement(to = "notDisplayable(this)") + void JFrame(String title); + + @StateRefinement(to = "displayable(this)") + void pack(); + + @StateRefinement(from = "notDisplayable(this)") + void setUndecorated(boolean undecorated); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/UseFrame.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/UseFrame.java new file mode 100644 index 00000000..22ee1218 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_error/UseFrame.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_external_error; + +import javax.swing.JFrame; + +public class UseFrame { + static void configure() { + JFrame frame = new JFrame("example"); + frame.pack(); + frame.setUndecorated(true); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Base.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Base.java new file mode 100644 index 00000000..9a6f94f3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Base.java @@ -0,0 +1,7 @@ +package testSuite.classes.inherited_external_visibility.parent; + +public class Base { + private void privateMethod() {} + void packageMethod() {} + protected void protectedMethod() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Child.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Child.java new file mode 100644 index 00000000..3ec4be44 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/Child.java @@ -0,0 +1,3 @@ +package testSuite.classes.inherited_external_visibility; + +public class Child extends testSuite.classes.inherited_external_visibility.parent.Base implements StaticParent {} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/ChildRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/ChildRefinements.java new file mode 100644 index 00000000..3ba6f4b3 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/ChildRefinements.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_external_visibility; + +import liquidjava.specification.ExternalRefinementsFor; + +@ExternalRefinementsFor("testSuite.classes.inherited_external_visibility.Child") +public interface ChildRefinements { + void privateMethod(); // Expect: Warning + void packageMethod(); // Expect: Warning + void interfaceStatic(); // Expect: Warning + void protectedMethod(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/DefaultChildRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/DefaultChildRefinements.java new file mode 100644 index 00000000..bae14779 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/DefaultChildRefinements.java @@ -0,0 +1,12 @@ +import liquidjava.specification.ExternalRefinementsFor; + +class DefaultParent { + void packageMethod() {} +} + +class DefaultChild extends DefaultParent {} + +@ExternalRefinementsFor("DefaultChild") +public interface DefaultChildRefinements { + void packageMethod(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/StaticParent.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/StaticParent.java new file mode 100644 index 00000000..f3582767 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_external_visibility/StaticParent.java @@ -0,0 +1,5 @@ +package testSuite.classes.inherited_external_visibility; + +public interface StaticParent { + static void interfaceStatic() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/StackRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/StackRefinements.java new file mode 100644 index 00000000..4179a0e5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/StackRefinements.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_overload_correct; + +import liquidjava.specification.*; + +@ExternalRefinementsFor("java.util.Stack") +@StateSet({"ready", "changed"}) +public interface StackRefinements { + @StateRefinement(to = "ready(this)") void Stack(); + @StateRefinement(to = "changed(this)") E remove(int index); + @StateRefinement(from = "ready(this)") E peek(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/UseStack.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/UseStack.java new file mode 100644 index 00000000..8ee4445e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_correct/UseStack.java @@ -0,0 +1,12 @@ +package testSuite.classes.inherited_overload_correct; + +import java.util.Stack; + +public class UseStack { + static void check() { + Stack stack = new Stack<>(); + stack.add("value"); + stack.remove("value"); + stack.peek(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/StackRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/StackRefinements.java new file mode 100644 index 00000000..d0158bbf --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/StackRefinements.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_overload_error; + +import liquidjava.specification.*; + +@ExternalRefinementsFor("java.util.Stack") +@StateSet({"ready", "changed"}) +public interface StackRefinements { + @StateRefinement(to = "ready(this)") void Stack(); + @StateRefinement(to = "changed(this)") E remove(int index); + @StateRefinement(from = "ready(this)") E peek(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/UseStack.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/UseStack.java new file mode 100644 index 00000000..08e6c026 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_overload_error/UseStack.java @@ -0,0 +1,12 @@ +package testSuite.classes.inherited_overload_error; + +import java.util.Stack; + +public class UseStack { + static void check() { + Stack stack = new Stack<>(); + stack.add("value"); + stack.remove(0); + stack.peek(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Base.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Base.java new file mode 100644 index 00000000..4e920a01 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Base.java @@ -0,0 +1,9 @@ +package testSuite.classes.inherited_source_correct; + +public class Base { + public void change(int value) {} + public void change(String value) {} + public void use() {} + public void inheritedPositive(@liquidjava.specification.Refinement("_ > 0") int value) {} + public void overridePositive(@liquidjava.specification.Refinement("_ > 0") int value) {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Child.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Child.java new file mode 100644 index 00000000..cc89e155 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/Child.java @@ -0,0 +1,6 @@ +package testSuite.classes.inherited_source_correct; + +public class Child extends Base { + @Override + public void overridePositive(@liquidjava.specification.Refinement("_ >= 0") int value) {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/ChildRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/ChildRefinements.java new file mode 100644 index 00000000..55edbf02 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/ChildRefinements.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_source_correct; + +import liquidjava.specification.*; + +@ExternalRefinementsFor("testSuite.classes.inherited_source_correct.Child") +@StateSet({"ready", "changed"}) +public interface ChildRefinements { + @StateRefinement(to = "ready(this)") void Child(); + @StateRefinement(to = "changed(this)") void change(int value); + @StateRefinement(from = "ready(this)") void use(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/UseChild.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/UseChild.java new file mode 100644 index 00000000..37098da4 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_correct/UseChild.java @@ -0,0 +1,17 @@ +package testSuite.classes.inherited_source_correct; + +public class UseChild { + static void check() { + Child child = new Child(); + child.change("unchanged"); + child.use(); + } + + static void superclassFallback() { + new Child().inheritedPositive(1); + } + + static void subclassOverride() { + new Child().overridePositive(0); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Base.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Base.java new file mode 100644 index 00000000..7f7ed5f5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Base.java @@ -0,0 +1,9 @@ +package testSuite.classes.inherited_source_error; + +public class Base { + public void change(int value) {} + public void change(String value) {} + public void use() {} + public void inheritedPositive(@liquidjava.specification.Refinement("_ > 0") int value) {} + public void overridePositive(@liquidjava.specification.Refinement("_ > 0") int value) {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Child.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Child.java new file mode 100644 index 00000000..7b22bbfb --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/Child.java @@ -0,0 +1,6 @@ +package testSuite.classes.inherited_source_error; + +public class Child extends Base { + @Override + public void overridePositive(@liquidjava.specification.Refinement("_ >= 0") int value) {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/ChildRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/ChildRefinements.java new file mode 100644 index 00000000..918418f5 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/ChildRefinements.java @@ -0,0 +1,11 @@ +package testSuite.classes.inherited_source_error; + +import liquidjava.specification.*; + +@ExternalRefinementsFor("testSuite.classes.inherited_source_error.Child") +@StateSet({"ready", "changed"}) +public interface ChildRefinements { + @StateRefinement(to = "ready(this)") void Child(); + @StateRefinement(to = "changed(this)") void change(int value); + @StateRefinement(from = "ready(this)") void use(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/UseChild.java b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/UseChild.java new file mode 100644 index 00000000..e65c4a57 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/inherited_source_error/UseChild.java @@ -0,0 +1,17 @@ +package testSuite.classes.inherited_source_error; + +public class UseChild { + static void check() { + Child child = new Child(); + child.change(1); + child.use(); // Expect: State Refinement Error + } + + static void superclassFallback() { + new Child().inheritedPositive(-1); // Expect: Refinement Error + } + + static void subclassOverride() { + new Child().overridePositive(0); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java index e8731991..0334d15c 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -344,12 +344,18 @@ public RefinedFunction getFunction(String name, String target, int size) { } public RefinedFunction getFunction(String name, String target, List> paramTypes) { + RefinedFunction exact = getFunctionExact(name, target, paramTypes); + return exact != null ? exact : getFunction(name, target, paramTypes.size()); + } + + /** Looks up a receiver-specific contract without selecting a different overload by arity. */ + public RefinedFunction getFunctionExact(String name, String target, List> paramTypes) { for (RefinedFunction fi : ctxFunctions) { if (fi.getTargetClass() != null && fi.getName().equals(name) && fi.getTargetClass().equals(target) && argumentTypesMatch(fi.getArguments(), paramTypes)) return fi; } - return getFunction(name, target, paramTypes.size()); + return null; } private boolean argumentTypesMatch(List args, List> paramTypes) { diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java index 1339355c..df5bb976 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/ExternalRefinementTypeChecker.java @@ -2,6 +2,7 @@ import java.util.List; import java.util.Optional; +import java.util.stream.Stream; import liquidjava.diagnostics.Diagnostics; import liquidjava.diagnostics.errors.LJError; @@ -140,11 +141,36 @@ private boolean classExists(String className) { private boolean methodExists(CtType targetType, CtMethod method) { // find method with matching signature - return targetType.getMethods().stream().filter(m -> m.getSimpleName().equals(method.getSimpleName())) + return inheritedMethods(targetType).filter(m -> m.getSimpleName().equals(method.getSimpleName())) .anyMatch(m -> parametersMatch(m.getParameters(), method.getParameters()) && typesMatch(m.getType(), method.getType())); } + /** Includes only methods that are declared on, or inherited by, the external target. */ + private Stream> inheritedMethods(CtType targetType) { + return targetType.getAllMethods().stream().filter(method -> { + CtType owner = method.getDeclaringType(); + if (owner == null) + return false; + if (owner.getQualifiedName().equals(targetType.getQualifiedName())) + return true; + if (method.isPrivate() || owner instanceof CtInterface && method.isStatic()) + return false; + if (method.isPublic() || method.isProtected()) + return true; + // A package-private method stops being inherited when a superclass crosses package boundaries. + CtType current = targetType; + while (current != null && !current.getQualifiedName().equals(owner.getQualifiedName())) { + if (current.getPackage() == null || owner.getPackage() == null + || !current.getPackage().getQualifiedName().equals(owner.getPackage().getQualifiedName())) + return false; + CtTypeReference parent = current.getSuperclass(); + current = parent == null ? null : parent.getTypeDeclaration(); + } + return current != null; + }); + } + private boolean constructorExists(CtType targetType, CtMethod method) { // find constructor with matching signature CtClass targetClass = (CtClass) targetType; @@ -188,7 +214,7 @@ private boolean parametersMatch(List targetParams, List refinementParams) } private String[] getOverloads(CtType targetType, CtMethod method) { - return targetType.getMethods().stream().filter(m -> m.getSimpleName().equals(method.getSimpleName())) + return inheritedMethods(targetType).filter(m -> m.getSimpleName().equals(method.getSimpleName())) .map(m -> String.format("%s %s", m.getType().getSimpleName(), m.getSignature())).toArray(String[]::new); } } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java index 88a37936..57c0b031 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/MethodsFunctionsChecker.java @@ -233,6 +233,8 @@ public void getReturnRefinements(CtReturn ret) throws LJError { // ################################ public void getInvocationRefinements(CtInvocation invocation) throws LJError { + if (tryReceiverRefinements(invocation)) + return; CtExecutable method = invocation.getExecutable().getDeclaration(); if (method == null) { @@ -252,6 +254,23 @@ public void getInvocationRefinements(CtInvocation invocation) throws LJEr } } + private boolean tryReceiverRefinements(CtInvocation invocation) throws LJError { + CtExpression receiver = invocation.getTarget(); + if (receiver == null || receiver.getType() == null) + return false; + String receiverType = receiver.getType().getQualifiedName(); + CtExecutableReference executable = invocation.getExecutable(); + for (String key : List.of(Utils.qualifyName(receiverType, executable.getSignature()), executable.getSignature(), + executable.getSimpleName(), Utils.qualifyName(receiverType, executable.getSimpleName()))) { + if (rtc.getContext().getFunctionExact(key, receiverType, executable.getParameters()) != null) { + checkInvocationRefinements(invocation, invocation.getArguments(), receiver, key, receiverType, + executable.getParameters()); + return true; + } + } + return false; + } + private void searchMethodInLibrary(CtExecutableReference ctr, CtInvocation invocation) throws LJError { CtTypeReference ctref = ctr.getDeclaringType(); if (ctref == null) {