diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/HashMapRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/HashMapRefinements.java new file mode 100644 index 00000000..9f6a9239 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/HashMapRefinements.java @@ -0,0 +1,15 @@ +package testSuite.classes.delegated_argument_reassigned_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.HashMap") +@Ghost("int capacity") +public interface HashMapRefinements { + @StateRefinement(to = "capacity(this) == initialCapacity") + void HashMap(int initialCapacity); + + @StateRefinement(from = "capacity(this) == 5") + V get(Object key); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/Test.java new file mode 100644 index 00000000..b34ece26 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_argument_reassigned_error/Test.java @@ -0,0 +1,34 @@ +package testSuite.classes.delegated_argument_reassigned_error; + +import java.util.function.IntFunction; +import javax.print.attribute.standard.PrinterStateReasons; + +// PrinterStateReasons(int) runs HashMap(int): the capacity is the argument's value at the call, not a later one +public class Test { + static void assignedBefore(int n) { + n = 5; + PrinterStateReasons r = new PrinterStateReasons(n); + r.get("k"); + } + + static void assignedAfter(int n) { + PrinterStateReasons r = new PrinterStateReasons(n); + n = 5; + r.get("k"); // Expect: State Refinement Error + } + + static void assignedBeforeAndAfter(int n) { + n = 6; + PrinterStateReasons r = new PrinterStateReasons(n); + n = 5; + r.get("k"); // Expect: State Refinement Error + } + + static IntFunction lambdaParameter() { + return k -> { + PrinterStateReasons r = new PrinterStateReasons(k); + r.get("k"); // Expect: State Refinement Error + return r; + }; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/HashSetRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/HashSetRefinements.java new file mode 100644 index 00000000..4171829f --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/HashSetRefinements.java @@ -0,0 +1,20 @@ +package testSuite.classes.delegated_constant_arguments_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.util.HashSet") +@Ghost("int capacity") +@StateSet({ "plain", "linked" }) +public interface HashSetRefinements { + @StateRefinement(to = "capacity(this) == initialCapacity && (dummy --> linked(this)) && (!dummy --> plain(this))") + void HashSet(int initialCapacity, float loadFactor, boolean dummy); + + @StateRefinement(from = "capacity(this) == 16 && linked(this)") + boolean add(E e); + + @StateRefinement(from = "plain(this)") + void clear(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/Test.java new file mode 100644 index 00000000..b33a51f0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_constant_arguments_error/Test.java @@ -0,0 +1,22 @@ +package testSuite.classes.delegated_constant_arguments_error; + +import java.util.LinkedHashSet; + +// LinkedHashSet() runs HashSet(16, .75f, true) and LinkedHashSet(int n) runs HashSet(n, .75f, true): the constants +// passed reach the spec as literals +public class Test { + static void defaultCapacity() { + LinkedHashSet s = new LinkedHashSet<>(); + s.add("x"); + } + + static void linked() { + LinkedHashSet s = new LinkedHashSet<>(); + s.clear(); // Expect: State Refinement Error + } + + static void otherCapacity(int n) { + LinkedHashSet s = new LinkedHashSet<>(n); + s.add("x"); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/HashMapRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/HashMapRefinements.java new file mode 100644 index 00000000..b3e63107 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/HashMapRefinements.java @@ -0,0 +1,16 @@ +package testSuite.classes.delegated_spec_keeping_other_sets_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.util.HashMap") +@StateSet({ "a1", "a2" }) +@StateSet({ "b1", "b2" }) +public interface HashMapRefinements { + @StateRefinement(to = "a2(this)") + void HashMap(int initialCapacity); + + @StateRefinement(from = "b1(this)") + V get(Object key); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/Test.java new file mode 100644 index 00000000..7b26e257 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_spec_keeping_other_sets_correct/Test.java @@ -0,0 +1,12 @@ +package testSuite.classes.delegated_spec_keeping_other_sets_correct; + +import javax.print.attribute.standard.PrinterStateReasons; + +// HashMap(int)'s spec leaves the b set unchanged, which refers to the old object: a new object has none, so the +// delegated call gets the default state (b1) instead of that spec +public class Test { + static void get() { + PrinterStateReasons r = new PrinterStateReasons(5); + r.get("k"); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/StackRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/StackRefinements.java new file mode 100644 index 00000000..640fce87 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/StackRefinements.java @@ -0,0 +1,15 @@ +package testSuite.classes.delegated_subclass_sets_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.util.Stack") +@StateSet({ "empty", "nonEmpty" }) +public interface StackRefinements { + @StateRefinement(from = "empty(this)", to = "nonEmpty(this)") + E push(E item); + + @StateRefinement(from = "nonEmpty(this)") + E peek(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/Test.java new file mode 100644 index 00000000..a55c1b87 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/Test.java @@ -0,0 +1,17 @@ +package testSuite.classes.delegated_subclass_sets_error; + +import java.util.Stack; + +// Stack() runs Vector(), whose spec sets only Vector's ghost: Stack's own state set starts at its default (empty) +public class Test { + static void pushThenPeek() { + Stack s = new Stack<>(); + s.push("a"); + s.peek(); + } + + static void peekEmpty() { + Stack s = new Stack<>(); + s.peek(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/VectorRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/VectorRefinements.java new file mode 100644 index 00000000..9c029a16 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/delegated_subclass_sets_error/VectorRefinements.java @@ -0,0 +1,12 @@ +package testSuite.classes.delegated_subclass_sets_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.Ghost; +import liquidjava.specification.StateRefinement; + +@ExternalRefinementsFor("java.util.Vector") +@Ghost("int elements") +public interface VectorRefinements { + @StateRefinement(to = "elements(this) == 0") + void Vector(); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Base.java b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Base.java new file mode 100644 index 00000000..c1101d4b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Base.java @@ -0,0 +1,13 @@ +package testSuite.classes.super_swapped_arguments_correct; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +public class Base { + @StateRefinement(to = "(x && !y && open(this)) || (!(x && !y) && closed(this))") + public Base(boolean x, boolean y) {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Sub.java b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Sub.java new file mode 100644 index 00000000..b134e0ec --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_correct/Sub.java @@ -0,0 +1,14 @@ +package testSuite.classes.super_swapped_arguments_correct; + +// The parameters of Sub are named like those of Base, in the other order: each Base parameter is replaced by the Sub +// parameter passed for it, all at once, so a name is not replaced twice +public class Sub extends Base { + public Sub(boolean y, boolean x) { + super(y, x); + } + + static void test() { + Sub s = new Sub(true, false); // Base(true, false): open + s.close(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Base.java b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Base.java new file mode 100644 index 00000000..c054560c --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Base.java @@ -0,0 +1,13 @@ +package testSuite.classes.super_swapped_arguments_error; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +public class Base { + @StateRefinement(to = "(x && !y && open(this)) || (!(x && !y) && closed(this))") + public Base(boolean x, boolean y) {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Sub.java b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Sub.java new file mode 100644 index 00000000..9d654f14 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/super_swapped_arguments_error/Sub.java @@ -0,0 +1,14 @@ +package testSuite.classes.super_swapped_arguments_error; + +// The parameters of Sub are named like those of Base, in the other order: each Base parameter is replaced by the Sub +// parameter passed for it, all at once, so a name is not replaced twice +public class Sub extends Base { + public Sub(boolean y, boolean x) { + super(y, x); + } + + static void test() { + Sub s = new Sub(false, true); // Base(false, true): closed + s.close(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/MyException.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/MyException.java new file mode 100644 index 00000000..64a15673 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/MyException.java @@ -0,0 +1,10 @@ +package testSuite.classes.throwable_jdk_subclass_correct; + +import java.io.IOException; + +// super(message) runs IOException(String), Exception(String) and then Throwable(String): no cause. +public class MyException extends IOException { + public MyException(String message) { + super(message); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/Test.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/Test.java new file mode 100644 index 00000000..69727b29 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/Test.java @@ -0,0 +1,29 @@ +package testSuite.classes.throwable_jdk_subclass_correct; + +// JDK exceptions whose constructors only pass their arguments up to Throwable(String) or Throwable() are created +// without a cause, so one initCause is allowed. +public class Test { + static RuntimeException wrap(Throwable t) { + RuntimeException e = new RuntimeException("failed"); + e.initCause(t); + return e; + } + + static IllegalStateException illegalState(Throwable t) { + IllegalStateException e = new IllegalStateException("failed"); + e.initCause(t); + return e; + } + + static Exception noMessage(Throwable t) { + Exception e = new Exception(); + e.initCause(t); + return e; + } + + static MyException mine(Throwable t) { + MyException e = new MyException("failed"); + e.initCause(t); + return e; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/ThrowableRefinements.java new file mode 100644 index 00000000..abf87ffa --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_correct/ThrowableRefinements.java @@ -0,0 +1,24 @@ +package testSuite.classes.throwable_jdk_subclass_correct; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.lang.Throwable") +@StateSet({ "noThrowable", "withThrowable" }) +public interface ThrowableRefinements { + @StateRefinement(to = "noThrowable(this)") + public void Throwable(); + + @StateRefinement(to = "noThrowable(this)") + public void Throwable(String message); + + @StateRefinement(to = "withThrowable(this)") + public void Throwable(String message, Throwable cause); + + @StateRefinement(to = "withThrowable(this)") + public void Throwable(Throwable cause); + + @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)") + public Throwable initCause(Throwable cause); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/NotFound.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/NotFound.java new file mode 100644 index 00000000..5544ed35 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/NotFound.java @@ -0,0 +1,7 @@ +package testSuite.classes.throwable_jdk_subclass_error; + +public class NotFound extends ClassNotFoundException { + public NotFound(String message) { + super(message); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/Test.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/Test.java new file mode 100644 index 00000000..4fa6d6c0 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/Test.java @@ -0,0 +1,34 @@ +package testSuite.classes.throwable_jdk_subclass_error; + +import java.util.MissingResourceException; + +public class Test { + // ClassNotFoundException() runs Throwable(Throwable) with a null cause, so initCause throws + // IllegalStateException("Can't overwrite cause") (scijava-common CommandInfo, fixed in a6fd9cf) + static ClassNotFoundException notFound(Throwable exc) throws ClassNotFoundException { + final ClassNotFoundException cnfe = new ClassNotFoundException(); + cnfe.initCause(exc); // Expect: State Refinement Error + throw cnfe; + } + + static RuntimeException causeTwice(Throwable cause, Throwable other) { + RuntimeException e = new RuntimeException("failed", cause); + e.initCause(other); // Expect: State Refinement Error + return e; + } + + // super(message) runs ClassNotFoundException(String), which passes a null cause on to Throwable(String, Throwable) + static NotFound notFoundSubclass(Throwable exc) { + NotFound e = new NotFound("missing"); + e.initCause(exc); // Expect: State Refinement Error + return e; + } + + // MissingResourceException(String, String, String) also writes fields after super(message), so it is not known to + // delegate and gets the default state, in which initCause cannot be shown to be allowed (#367) + static MissingResourceException notDelegating(Throwable exc) { + MissingResourceException e = new MissingResourceException("missing", "Bundle", "key"); + e.initCause(exc); // Expect: State Refinement Error + return e; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/ThrowableRefinements.java new file mode 100644 index 00000000..46ed475d --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_jdk_subclass_error/ThrowableRefinements.java @@ -0,0 +1,24 @@ +package testSuite.classes.throwable_jdk_subclass_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.lang.Throwable") +@StateSet({ "noThrowable", "withThrowable" }) +public interface ThrowableRefinements { + @StateRefinement(to = "noThrowable(this)") + public void Throwable(); + + @StateRefinement(to = "noThrowable(this)") + public void Throwable(String message); + + @StateRefinement(to = "withThrowable(this)") + public void Throwable(String message, Throwable cause); + + @StateRefinement(to = "withThrowable(this)") + public void Throwable(Throwable cause); + + @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)") + public Throwable initCause(Throwable cause); +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterImplicitSuper.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterImplicitSuper.java new file mode 100644 index 00000000..95227b24 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterImplicitSuper.java @@ -0,0 +1,16 @@ +package testSuite.classes.throwable_subclass_more_than_super_error; + +import java.io.IOException; + +// the implicit super() leaves no cause, but the constructor then sets one +public class CauseAfterImplicitSuper extends IOException { + public CauseAfterImplicitSuper(Throwable cause) { + initCause(cause); + } + + static CauseAfterImplicitSuper wrap(Throwable cause, Throwable other) { + CauseAfterImplicitSuper e = new CauseAfterImplicitSuper(cause); + e.initCause(other); // Expect: State Refinement Error + return e; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterSuper.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterSuper.java new file mode 100644 index 00000000..41dbc89e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseAfterSuper.java @@ -0,0 +1,16 @@ +package testSuite.classes.throwable_subclass_more_than_super_error; + +// super(message) leaves no cause, but the constructor then sets one, so it gets the default state, not +// Throwable(String)'s, and a second initCause is reported +public class CauseAfterSuper extends RuntimeException { + public CauseAfterSuper(String message, Throwable cause) { + super(message); + initCause(cause); + } + + static CauseAfterSuper wrap(Throwable cause, Throwable other) { + CauseAfterSuper e = new CauseAfterSuper("failed", cause); + e.initCause(other); // Expect: State Refinement Error + return e; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseInInitializer.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseInInitializer.java new file mode 100644 index 00000000..6274034a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/CauseInInitializer.java @@ -0,0 +1,18 @@ +package testSuite.classes.throwable_subclass_more_than_super_error; + +// an instance initializer runs right after super(message) and sets the cause +public class CauseInInitializer extends RuntimeException { + { + initCause(null); + } + + public CauseInInitializer(String message) { + super(message); + } + + static CauseInInitializer wrap(Throwable other) { + CauseInInitializer e = new CauseInInitializer("failed"); + e.initCause(other); // Expect: State Refinement Error + return e; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/ThrowableRefinements.java b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/ThrowableRefinements.java new file mode 100644 index 00000000..a6f282c8 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/throwable_subclass_more_than_super_error/ThrowableRefinements.java @@ -0,0 +1,24 @@ +package testSuite.classes.throwable_subclass_more_than_super_error; + +import liquidjava.specification.ExternalRefinementsFor; +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@ExternalRefinementsFor("java.lang.Throwable") +@StateSet({ "noThrowable", "withThrowable" }) +public interface ThrowableRefinements { + @StateRefinement(to = "noThrowable(this)") + public void Throwable(); + + @StateRefinement(to = "noThrowable(this)") + public void Throwable(String message); + + @StateRefinement(to = "withThrowable(this)") + public void Throwable(String message, Throwable cause); + + @StateRefinement(to = "withThrowable(this)") + public void Throwable(Throwable cause); + + @StateRefinement(from = "noThrowable(this)", to = "withThrowable(this)") + public Throwable initCause(Throwable cause); +} diff --git a/liquidjava-verifier/pom.xml b/liquidjava-verifier/pom.xml index 84891bc2..4ffa83bc 100644 --- a/liquidjava-verifier/pom.xml +++ b/liquidjava-verifier/pom.xml @@ -368,6 +368,12 @@ picocli 4.7.7 + + + org.ow2.asm + asm + 9.11 + 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 92f0b9d2..272c1e83 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 @@ -78,10 +78,13 @@ public void getConstructorInvocationRefinements(CtConstructorCall ctConstruct f.getTargetClass(), paramTypes); AuxStateHandler.constructorStateMetadata(Keys.REFINEMENT, f, map, ctConstructorCall); } else { - // default constructor refinements + // the state of a specified ancestor constructor it delegates to, else the default CtTypeReference type = exe.getDeclaringType() != null ? exe.getDeclaringType() : ctConstructorCall.getType(); - if (type != null) + Optional delegated = AuxStateHandler.delegatedConstructorState(rtc, ctConstructorCall); + if (delegated.isPresent()) + ctConstructorCall.putMetadata(Keys.REFINEMENT, delegated.get()); + else if (type != null) ctConstructorCall.putMetadata(Keys.REFINEMENT, AuxStateHandler.getDefaultState(rtc, type.getQualifiedName(), Predicate.createVar(Keys.THIS))); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java index a03c2824..5b951912 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java @@ -62,7 +62,7 @@ public static void handleConstructorState(CtConstructor c, RefinedFunction f, } /** - * An unannotated constructor whose body starts with {@code super(...)} leaves the object in the state that the + * An unannotated constructor whose body is only a {@code super(...)} call leaves the object in the state that the * called superclass constructor's specification gives it (e.g. {@code MyException(String m, Throwable c) { super(m, * c); }} with the {@code Throwable(String, Throwable)} spec: {@code withThrowable(this)}). The super constructor's * parameters are renamed to the arguments passed, which must be parameters of this constructor or literals. @@ -70,66 +70,207 @@ public static void handleConstructorState(CtConstructor c, RefinedFunction f, * @return whether a state was inherited (otherwise the caller falls back to the default state) */ private static boolean inheritSuperConstructorState(CtConstructor c, RefinedFunction f, TypeChecker tc) { - CtStatement first = c.getBody() == null || c.getBody().getStatements().isEmpty() ? null - : c.getBody().getStatement(0); - if (!(first instanceof CtInvocation call) || !call.getExecutable().isConstructor() - || c.getDeclaringType() == null - || c.getDeclaringType().getReference().equals(call.getExecutable().getDeclaringType())) - return false; // not a super(...) call (this(...) delegates within the class) - RefinedFunction superF = specifiedConstructor(tc, call.getExecutable()); - List> args = call.getArguments(); - if (superF == null || superF.getToStates().isEmpty() || superF.getArguments().size() != args.size()) + Optional> call = onlySuperCall(c); + if (call.isEmpty()) return false; + List> values = call.get().getArguments().stream().map(AuxStateHandler::argumentValue) + .toList(); + Optional> states = specifiedStates(tc, call.get().getExecutable(), values, + c.getDeclaringType().getQualifiedName()); + states.ifPresent( + to -> f.setAllStates(to.stream().map(p -> new ObjectState(null, p)).collect(Collectors.toList()))); + return states.isPresent(); + } + + /** + * The {@code super(...)} call that is all {@code c} runs, if so. Anything after it, or an instance initializer or + * field initializer of the class (which run right after it), may change the state, as in {@code super(m); + * initCause(c);}. This is the source counterpart of what {@link ConstructorDelegation} accepts in bytecode. + */ + private static Optional> onlySuperCall(CtConstructor c) { + CtType owner = c.getDeclaringType(); + if (owner == null || c.getBody() == null || c.getBody().getStatements().size() != 1 + || !(c.getBody().getStatement(0)instanceof CtInvocation call) + || !call.getExecutable().isConstructor() + || owner.getReference().equals(call.getExecutable().getDeclaringType())) + return Optional.empty(); // not only a super(...) call (this(...) delegates within the class) + boolean initializers = owner instanceof CtClass klass + && klass.getAnonymousExecutables().stream().anyMatch(block -> !block.isStatic()); + boolean fieldInitializers = owner.getFields().stream() + .anyMatch(field -> !field.isStatic() && field.getDefaultExpression() != null); + return initializers || fieldInitializers ? Optional.empty() : Optional.of(call); + } - // rename each super parameter to the argument passed for it; a state may not mention an unnamed one - Map rename = new HashMap<>(); - Set unnamed = new HashSet<>(); - for (int i = 0; i < args.size(); i++) { - String param = superF.getArguments().get(i).getName(); - argumentName(args.get(i)).ifPresentOrElse(a -> rename.put(param, a), () -> unnamed.add(param)); + /** + * The state that {@code new C(...)} gives when {@code C}'s constructor has no specification of its own but is a + * binary constructor that delegates to a specified one of an ancestor (e.g. {@code new RuntimeException(m)} runs + * {@code Throwable(String)}), with the arguments renamed as in {@link #inheritSuperConstructorState}. + */ + public static Optional delegatedConstructorState(TypeChecker tc, CtConstructorCall call) { + if (call instanceof CtNewClass || call.getExecutable().getDeclaringType() == null) + return Optional.empty(); // an anonymous class body may change the state + List> values = call.getArguments().stream().map(a -> callArgumentValue(tc, a)).toList(); + return specifiedStates(tc, call.getExecutable(), values, + call.getExecutable().getDeclaringType().getQualifiedName()).filter(to -> !to.isEmpty()) + .map(to -> to.get(0)); + } + + /** + * The to-states of the specified constructor that {@code exe} ends up running, with each of its parameters replaced + * by the value passed for it, and the default value for each state set of {@code constructed} that they leave + * unconstrained. Empty if no specified constructor is known, or if a state mentions a parameter whose value cannot + * be written. + * + * @param argumentValues + * how a state can write each argument of the call to {@code exe} + */ + private static Optional> specifiedStates(TypeChecker tc, CtExecutableReference exe, + List> argumentValues, String constructed) { + if (exe.getDeclaringType() == null || argumentValues.size() != exe.getParameters().size()) + return Optional.empty(); // e.g. a varargs call + Optional spec = specifiedConstructor(tc, exe); + if (spec.isEmpty() || spec.get().function().getToStates().isEmpty()) + return Optional.empty(); + + // replace each spec parameter by the value passed for it; a state may not mention one without a value + Map values = new HashMap<>(); + Set unknown = new HashSet<>(); + List params = spec.get().function().getArguments(); + for (int i = 0; i < params.size(); i++) { + String param = params.get(i).getName(); + ConstructorDelegation.Argument passed = spec.get().arguments().get(i); + Optional value = passed instanceof ConstructorDelegation.Parameter p + ? argumentValues.get(p.index()) + : ((ConstructorDelegation.Constant) passed).value().flatMap(AuxStateHandler::literal); + value.ifPresentOrElse(v -> values.put(param, v), () -> unknown.add(param)); } - if (superF.getToStates().stream().anyMatch(to -> to.getVariableNames().stream().anyMatch(unnamed::contains))) - return false; - f.setAllStates(superF.getToStates().stream() - .map(to -> new ObjectState(null, rename.entrySet().stream().reduce(to, - (p, r) -> p.substituteVariable(r.getKey(), r.getValue()), (p, q) -> p))) - .collect(Collectors.toList())); - return true; + List states = spec.get().function().getToStates(); + if (states.stream().anyMatch(to -> to.getVariableNames().stream().anyMatch(unknown::contains))) + return Optional.empty(); + // a spec that leaves some state sets unchanged refers to old(this), which a new object does not have + if (states.stream().anyMatch(to -> to.invokes(Keys.OLD))) + return Optional.empty(); + return Optional.of(states.stream().map(to -> substituteAll(to, values)) + .map(to -> withDefaultsForOtherSets(tc, constructed, to)).toList()); + } + + /** + * Replaces each variable of {@code values} at once, so a value that is also a name in {@code values} is not + * replaced again (e.g. {@code Sub(boolean y, boolean x) { super(y, x); }} for {@code Base(boolean x, boolean y)}). + */ + private static Predicate substituteAll(Predicate p, Map values) { + Map placeholders = new HashMap<>(); + for (String name : values.keySet()) { + String placeholder = "#param_" + placeholders.size(); + placeholders.put(name, placeholder); + p = p.substituteVariable(name, placeholder); + } + for (Map.Entry e : placeholders.entrySet()) + p = p.substituteVariable(e.getValue(), values.get(e.getKey())); + return p; } - /** How a state can refer to {@code arg}: by the caller's parameter name or a non-string literal's value. */ - private static Optional argumentName(CtExpression arg) { + /** + * {@code to} and the default value of each state set of {@code klass} it does not mention: an ancestor's + * constructor spec says nothing about the sets a subclass adds (e.g. {@code Stack}'s, after {@code Vector()}). + */ + private static Predicate withDefaultsForOtherSets(TypeChecker tc, String klass, Predicate to) { + return Predicate.createConjunction(to, + defaultValues(unmentionedSets(tc, klass, to), Predicate.createVar(Keys.THIS))); + } + + /** How a state can write {@code arg}: by the caller's parameter name or a literal. */ + private static Optional argumentValue(CtExpression arg) { if (arg instanceof CtVariableRead vr && vr.getVariable() instanceof spoon.reflect.reference.CtParameterReference) - return Optional.of(vr.getVariable().getSimpleName()); - if (arg instanceof CtLiteral lit && lit.getValue() != null && !(lit.getValue() instanceof String)) - return Optional.of(lit.getValue().toString()); + return Optional.of(Predicate.createVar(vr.getVariable().getSimpleName())); + return literalValue(arg); + } + + /** + * How a state can write {@code arg} at a call: by the variable's current instance, which keeps the value it has now + * even if the variable is assigned later, or a literal. A variable without an instance (e.g. a parameter not + * assigned yet) has no known value here. + */ + private static Optional callArgumentValue(TypeChecker tc, CtExpression arg) { + if (arg instanceof CtVariableRead vr && !(arg instanceof CtFieldRead)) + return tc.getContext().getLastVariableInstance(vr.getVariable().getSimpleName()) + .map(vi -> Predicate.createVar(vi.getName())); + return literalValue(arg); + } + + /** {@code arg} as a literal of the refinement language, if it is a boolean or int literal. */ + private static Optional literalValue(CtExpression arg) { + return arg instanceof CtLiteral lit ? literal(lit.getValue()) : Optional.empty(); + } + + private static Optional literal(Object value) { + if (value instanceof Boolean) + return Optional.of(Predicate.createLit(value.toString(), Types.BOOLEAN)); + if (value instanceof Integer || value instanceof Short || value instanceof Byte) + return Optional.of(Predicate.createLit(value.toString(), Types.INT)); return Optional.empty(); } /** - * JDK classes whose constructors all pass their arguments unchanged to the superclass constructor with the same - * parameter types (documented in their Javadoc), so a spec on that superclass constructor describes them too. Only - * these are walked through: other binary classes may not (e.g. {@code ClassNotFoundException(String)} sets a null - * cause), and assuming they did would hide real errors. + * A constructor specification, and what a call passes for each of its parameters. + * + * @param arguments + * for each parameter of {@code function}: an index into the call's arguments, or a constant */ - private static final Set DELEGATING_JDK_CLASSES = Set.of("java.lang.Exception", - "java.lang.RuntimeException", "java.lang.Error"); - - /** The specified constructor that {@code exe} ends up running, if one is known. */ - private static RefinedFunction specifiedConstructor(TypeChecker tc, CtExecutableReference exe) { - for (CtTypeReference t = exe.getDeclaringType(); t != null;) { - RefinedFunction f = tc.getContext().getFunction(exe.getSimpleName(), t.getQualifiedName(), - exe.getParameters()); - if (f != null || !DELEGATING_JDK_CLASSES.contains(t.getQualifiedName())) - return f; - try { - t = t.getSuperclass(); - } catch (RuntimeException | LinkageError e) { - return null; - } + private record SpecifiedConstructor(RefinedFunction function, List arguments) { + } + + /** + * The specified constructor that {@code exe} ends up running, if one is known. A binary constructor without a + * specification is walked through only when its bytecode just passes values on to a superclass constructor (e.g. + * {@code RuntimeException(String)} to {@code Exception(String)} to {@code Throwable(String)}); assuming any other + * constructor did so would hide real errors (e.g. {@code ClassNotFoundException(String)} also sets a null cause). + */ + private static Optional specifiedConstructor(TypeChecker tc, CtExecutableReference exe) { + List arguments = new ArrayList<>(); + for (int i = 0; i < exe.getParameters().size(); i++) + arguments.add(new ConstructorDelegation.Parameter(i)); + String klass = exe.getDeclaringType().getQualifiedName(); + RefinedFunction f = tc.getContext().getFunction(exe.getSimpleName(), klass, exe.getParameters()); + Optional> types = erasedNames(exe.getParameters()); + while (f == null && types.isPresent()) { + Optional delegation = ConstructorDelegation.of(klass, types.get()); + if (delegation.isEmpty()) + return Optional.empty(); + arguments = passedOn(arguments, delegation.get().arguments()); + klass = delegation.get().superclass(); + types = Optional.of(delegation.get().superParameterTypes()); + // exact types: the arity fallback of getFunction could pick another overload's spec + f = tc.getContext().getFunctionExact(exe.getSimpleName(), klass, typeReferences(tc, types.get())); + } + return f == null ? Optional.empty() : Optional.of(new SpecifiedConstructor(f, arguments)); + } + + /** + * What reaches the superclass constructor, in terms of the original call: a parameter passed on refers back to the + * value the call gave for it. + */ + private static List passedOn(List callArguments, + List delegated) { + return delegated.stream() + .map(a -> a instanceof ConstructorDelegation.Parameter p ? callArguments.get(p.index()) : a).toList(); + } + + /** The erased qualified names of {@code types}, as in bytecode descriptors, if they can be resolved. */ + private static Optional> erasedNames(List> types) { + try { + return Optional.of(types.stream().map(t -> t.getTypeErasure().getQualifiedName()).toList()); + } catch (RuntimeException e) { + return Optional.empty(); } - return null; + } + + private static List> typeReferences(TypeChecker tc, List names) { + List> refs = new ArrayList<>(); + for (String name : names) + refs.add(tc.getFactory().Type().createReference(name)); + return refs; } /** @@ -180,8 +321,12 @@ public static void setDefaultState(RefinedFunction f, TypeChecker tc) { } public static Predicate getDefaultState(TypeChecker tc, String klass, Predicate target) { + return defaultValues(getDifferentSets(tc, klass), target); + } + + /** Each of {@code sets} at its default value on {@code target}. */ + private static Predicate defaultValues(List sets, Predicate target) { Predicate c = new Predicate(); - List sets = getDifferentSets(tc, klass); for (GhostFunction sg : sets) { String retType = sg.getReturnType().toString(); Predicate typePredicate = switch (retType) { @@ -343,6 +488,11 @@ private static Predicate createStatePredicate(Predicate p, String value, String * @return the updated predicate */ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) { + return addOldStates(p, Predicate.createVar(Keys.THIS), unmentionedSets(tc, t, p)); + } + + /** The ghost state sets of class {@code t} that {@code p} does not mention. */ + private static List unmentionedSets(TypeChecker tc, String t, Predicate p) { List gs = p.getStateInvocations(getGhostStatesFor(t, tc)); List sets = getDifferentSets(tc, t); for (GhostState g : gs) { @@ -352,7 +502,7 @@ private static Predicate getMissingStates(String t, TypeChecker tc, Predicate p) sets.remove(g.getParent()); } } - return addOldStates(p, Predicate.createVar(Keys.THIS), sets); + return sets; } /** diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegation.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegation.java new file mode 100644 index 00000000..1b46a1b4 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegation.java @@ -0,0 +1,281 @@ +package liquidjava.processor.refinement_checker.object_checkers; + +import java.io.IOException; +import java.io.InputStream; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.Map; +import java.util.Optional; +import java.util.concurrent.ConcurrentHashMap; +import java.util.function.Function; + +import org.objectweb.asm.ClassReader; +import org.objectweb.asm.ClassVisitor; +import org.objectweb.asm.Handle; +import org.objectweb.asm.Label; +import org.objectweb.asm.MethodVisitor; +import org.objectweb.asm.Opcodes; +import org.objectweb.asm.Type; + +/** + * A binary constructor whose whole body is a call to a superclass constructor, read from its bytecode: which superclass + * constructor it calls and what it passes for each parameter. Only that exact shape is recognized, so the object ends + * up in whatever state the superclass constructor leaves it in: + * + * 
+ * aload_0
+ * (a load of one of its parameters | a constant [checkcast])*
+ * invokespecial Superclass.<init>
+ * return
+ *
+ * + * Anything else (field writes, method calls, this(...), branches) is not a delegation. Classes are read from the JDK + * only: the verifier runs without the analyzed program's classpath, and the verifier's own libraries may differ from + * the versions the program uses. The result therefore depends on the JDK the verifier runs on, which may not be the one + * the program is compiled against. + * + * @param superclass + * qualified name of the superclass whose constructor is called + * @param superParameterTypes + * qualified names of that constructor's parameter types + * @param arguments + * what is passed for each of them + */ +public record ConstructorDelegation(String superclass, List superParameterTypes, List arguments) { + + /** A value passed to the superclass constructor. */ + public sealed interface Argument permits Parameter,Constant { + } + + /** The delegating constructor's parameter at {@code index}, unchanged. */ + public record Parameter(int index) implements Argument { + } + + /** + * A constant, with its value when a state can refer to it (an {@link Integer} or a {@link Boolean}, by the type of + * the parameter it is passed for); empty when it cannot (e.g. {@code null}, a string). + */ + public record Constant(Optional value) implements Argument { + } + + private record Key(String className, List parameterTypes) { + } + + private static final Map> CACHE = new ConcurrentHashMap<>(); + + /** + * How the constructor of {@code className} with these parameter types delegates to a superclass constructor, if its + * bytecode is available and has exactly that shape. + */ + public static Optional of(String className, List parameterTypes) { + return CACHE.computeIfAbsent(new Key(className, parameterTypes), k -> read(className, parameterTypes)); + } + + private static Optional read(String className, List parameterTypes) { + String resource = className.replace('.', '/') + ".class"; + try (InputStream in = ClassLoader.getPlatformClassLoader().getResourceAsStream(resource)) { + if (in == null) + return Optional.empty(); + ClassReader reader = new ClassReader(in); + if (reader.getSuperName() == null) + return Optional.empty(); // java.lang.Object + ConstructorFinder finder = new ConstructorFinder(reader.getSuperName(), parameterTypes); + reader.accept(finder, ClassReader.SKIP_DEBUG); + return finder.delegation(); + } catch (IOException | RuntimeException e) { + return Optional.empty(); // unreadable or unsupported class file: not known to delegate + } + } + + /** Hands the constructor with the wanted parameter types to a {@link DelegationMatcher}. */ + private static final class ConstructorFinder extends ClassVisitor { + private final String superclass; + private final List parameterTypes; + private DelegationMatcher matcher; + + ConstructorFinder(String superclass, List parameterTypes) { + super(Opcodes.ASM9); + this.superclass = superclass; + this.parameterTypes = parameterTypes; + } + + @Override + public MethodVisitor visitMethod(int access, String name, String descriptor, String signature, + String[] exceptions) { + Type[] params = Type.getArgumentTypes(descriptor); + if (!name.equals("") + || !Arrays.stream(params).map(Type::getClassName).toList().equals(parameterTypes)) + return null; + matcher = new DelegationMatcher(superclass, params); + return matcher; + } + + Optional delegation() { + return matcher == null ? Optional.empty() : matcher.delegation(); + } + } + + /** + * Follows a constructor's instructions through the delegating shape, failing on the first one that does not fit. + * Labels, line numbers, frames and local variable tables are not instructions and are ignored. + */ + private static final class DelegationMatcher extends MethodVisitor { + private enum Step { + RECEIVER, ARGUMENTS, RETURN, DONE, FAILED + } + + private final String superclass; + private final Type[] params; + /** What each pushed value is, given the type of the superclass parameter it ends up passed for. */ + private final List> pushed = new ArrayList<>(); + private boolean lastPushedNull; + private Step step = Step.RECEIVER; + private ConstructorDelegation delegation; + + DelegationMatcher(String superclass, Type[] params) { + super(Opcodes.ASM9); + this.superclass = superclass; + this.params = params; + } + + Optional delegation() { + return step == Step.DONE ? Optional.of(delegation) : Optional.empty(); + } + + @Override + public void visitVarInsn(int opcode, int slot) { + if (step == Step.RECEIVER && opcode == Opcodes.ALOAD && slot == 0) + step = Step.ARGUMENTS; + else if (step == Step.ARGUMENTS) + parameterAt(slot).filter(i -> opcode == params[i].getOpcode(Opcodes.ILOAD)) + .ifPresentOrElse(i -> push(t -> new Parameter(i)), this::fail); + else + fail(); + } + + /** The parameter stored in local variable {@code slot} (slot 0 is {@code this}; long and double take two). */ + private Optional parameterAt(int slot) { + int next = 1; + for (int i = 0; i < params.length; next += params[i].getSize(), i++) + if (next == slot) + return Optional.of(i); + return Optional.empty(); + } + + @Override + public void visitInsn(int opcode) { + if (step == Step.RETURN && opcode == Opcodes.RETURN) + step = Step.DONE; + else if (step == Step.ARGUMENTS && opcode == Opcodes.ACONST_NULL) { + push(t -> new Constant(Optional.empty())); + lastPushedNull = true; + } else if (step == Step.ARGUMENTS && opcode >= Opcodes.ICONST_M1 && opcode <= Opcodes.ICONST_5) + pushInt(opcode - Opcodes.ICONST_0); + else if (step == Step.ARGUMENTS && opcode >= Opcodes.LCONST_0 && opcode <= Opcodes.DCONST_1) + push(t -> new Constant(Optional.empty())); + else + fail(); + } + + @Override + public void visitIntInsn(int opcode, int operand) { + if (step == Step.ARGUMENTS && (opcode == Opcodes.BIPUSH || opcode == Opcodes.SIPUSH)) + pushInt(operand); + else + fail(); + } + + /** An int constant: a boolean, a number, or a char a state cannot write, depending on the parameter. */ + private void pushInt(int value) { + push(t -> new Constant(switch (t.getSort()) { + case Type.BOOLEAN -> Optional.of(value != 0); + case Type.INT, Type.SHORT, Type.BYTE -> Optional.of(value); + default -> Optional.empty(); + })); + } + + private void push(Function argument) { + pushed.add(argument); + lastPushedNull = false; + } + + @Override + public void visitLdcInsn(Object value) { + if (step == Step.ARGUMENTS && value instanceof Integer i) + pushInt(i); + else if (step == Step.ARGUMENTS) + push(t -> new Constant(Optional.empty())); // strings, classes, other constants + else + fail(); + } + + @Override + public void visitTypeInsn(int opcode, String type) { + // javac casts a null argument to pick an overload, e.g. super((Throwable) null) + if (step != Step.ARGUMENTS || opcode != Opcodes.CHECKCAST || !lastPushedNull) + fail(); + } + + @Override + public void visitMethodInsn(int opcode, String owner, String name, String descriptor, boolean isInterface) { + Type[] superParams = Type.getArgumentTypes(descriptor); + if (step != Step.ARGUMENTS || opcode != Opcodes.INVOKESPECIAL || !owner.equals(superclass) + || !name.equals("") || superParams.length != pushed.size()) { + fail(); + return; + } + List arguments = new ArrayList<>(); + for (int i = 0; i < superParams.length; i++) + arguments.add(pushed.get(i).apply(superParams[i])); + delegation = new ConstructorDelegation(Type.getObjectType(superclass).getClassName(), + Arrays.stream(superParams).map(Type::getClassName).toList(), arguments); + step = Step.RETURN; + } + + @Override + public void visitFieldInsn(int opcode, String owner, String name, String descriptor) { + fail(); + } + + @Override + public void visitInvokeDynamicInsn(String name, String descriptor, Handle bootstrap, + Object... bootstrapArguments) { + fail(); + } + + @Override + public void visitJumpInsn(int opcode, Label label) { + fail(); + } + + @Override + public void visitIincInsn(int slot, int increment) { + fail(); + } + + @Override + public void visitTableSwitchInsn(int min, int max, Label dflt, Label... labels) { + fail(); + } + + @Override + public void visitLookupSwitchInsn(Label dflt, int[] keys, Label[] labels) { + fail(); + } + + @Override + public void visitMultiANewArrayInsn(String descriptor, int dimensions) { + fail(); + } + + @Override + public void visitTryCatchBlock(Label start, Label end, Label handler, String type) { + fail(); + } + + private void fail() { + step = Step.FAILED; + } + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 1bac14c9..0dfc158f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -178,6 +178,18 @@ public Predicate substituteVariable(String from, String to) { return new Predicate(ec); } + /** Replaces the variable {@code from} with the expression {@code to} (e.g. a literal). */ + public Predicate substituteVariable(String from, Predicate to) { + return new Predicate(exp.clone().substitute(new Var(from), to.getExpression().clone())); + } + + /** Whether the function {@code name} is called anywhere in this predicate. */ + public boolean invokes(String name) { + List found = new ArrayList<>(); + exp.getStateInvocations(found, List.of(name)); + return !found.isEmpty(); + } + public List getVariableNames() { List l = new ArrayList<>(); exp.getVariableNames(l); diff --git a/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDelegatedConstructorStates.java b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDelegatedConstructorStates.java new file mode 100644 index 00000000..f05645d6 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/api/tests/TestDelegatedConstructorStates.java @@ -0,0 +1,38 @@ +package liquidjava.api.tests; + +import static org.junit.jupiter.api.Assertions.*; + +import java.util.List; +import java.util.Map; +import java.util.stream.Collectors; + +import org.junit.jupiter.api.Test; + +import liquidjava.api.CommandLineLauncher; +import liquidjava.diagnostics.Diagnostics; +import liquidjava.diagnostics.errors.StateRefinementError; + +/** + * The test suite only checks where errors are reported. These check the state found there: a JDK constructor that + * delegates to a specified one gets that spec's state, not an unknown one. + */ +class TestDelegatedConstructorStates { + + private static final String TEST_SUITE = "../liquidjava-example/src/main/java/testSuite/"; + private static final List> WITH_CAUSE = List.of(List.of("withThrowable")); + + @Test + void delegatingJdkConstructorsGiveTheSpecifiedState() { + Map>> found = foundStatesByLine("classes/throwable_jdk_subclass_error"); + assertEquals(WITH_CAUSE, found.get(10)); // new ClassNotFoundException() + assertEquals(WITH_CAUSE, found.get(16)); // new RuntimeException(message, cause) + assertEquals(WITH_CAUSE, found.get(23)); // subclass calling ClassNotFoundException(String) + assertNotEquals(WITH_CAUSE, found.get(31)); // MissingResourceException: not delegating, default state + } + + private static Map>> foundStatesByLine(String test) { + CommandLineLauncher.launch(TEST_SUITE + test); + return Diagnostics.getInstance().getErrors().stream().map(e -> assertInstanceOf(StateRefinementError.class, e)) + .collect(Collectors.toMap(e -> e.getPosition().getLine(), e -> e.getContext().possibleStates())); + } +} diff --git a/liquidjava-verifier/src/test/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegationTest.java b/liquidjava-verifier/src/test/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegationTest.java new file mode 100644 index 00000000..ed0ef409 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/processor/refinement_checker/object_checkers/ConstructorDelegationTest.java @@ -0,0 +1,76 @@ +package liquidjava.processor.refinement_checker.object_checkers; + +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertTrue; + +import java.util.List; +import java.util.Optional; + +import liquidjava.processor.refinement_checker.object_checkers.ConstructorDelegation.Constant; +import liquidjava.processor.refinement_checker.object_checkers.ConstructorDelegation.Parameter; +import org.junit.jupiter.api.Test; + +class ConstructorDelegationTest { + + private static final Constant UNNAMED = new Constant(Optional.empty()); + + @Test + void passesItsParametersOnUnchanged() { + assertEquals(Optional.of(new ConstructorDelegation("java.lang.Throwable", + List.of("java.lang.String", "java.lang.Throwable"), List.of(new Parameter(0), new Parameter(1)))), + ConstructorDelegation.of("java.lang.Exception", List.of("java.lang.String", "java.lang.Throwable"))); + } + + @Test + void passesNullCastToPickAnOverload() { + // aload_0; aconst_null; checkcast Throwable; invokespecial ReflectiveOperationException(Throwable) + assertEquals( + Optional.of(new ConstructorDelegation("java.lang.ReflectiveOperationException", + List.of("java.lang.Throwable"), List.of(UNNAMED))), + ConstructorDelegation.of("java.lang.ClassNotFoundException", List.of())); + } + + @Test + void passesAParameterAndAConstant() { + assertEquals( + Optional.of(new ConstructorDelegation("java.lang.ReflectiveOperationException", + List.of("java.lang.String", "java.lang.Throwable"), List.of(new Parameter(0), UNNAMED))), + ConstructorDelegation.of("java.lang.ClassNotFoundException", List.of("java.lang.String"))); + } + + @Test + void typesIntConstantsBySuperParameterType() { + // LinkedHashSet() { super(16, .75f, true); } + assertEquals( + Optional.of(new ConstructorDelegation("java.util.HashSet", List.of("int", "float", "boolean"), + List.of(new Constant(Optional.of(16)), UNNAMED, new Constant(Optional.of(true))))), + ConstructorDelegation.of("java.util.LinkedHashSet", List.of())); + } + + @Test + void passesAParameterAmongConstants() { + // LinkedHashSet(int initialCapacity) { super(initialCapacity, .75f, true); } + assertEquals(List.of(new Parameter(0), UNNAMED, new Constant(Optional.of(true))), + ConstructorDelegation.of("java.util.LinkedHashSet", List.of("int")).orElseThrow().arguments()); + } + + @Test + void rejectsAConstructorThatDoesMoreThanDelegate() { + // super(s); this.className = className; this.key = key; + assertEquals(Optional.empty(), ConstructorDelegation.of("java.util.MissingResourceException", + List.of("java.lang.String", "java.lang.String", "java.lang.String"))); + } + + @Test + void rejectsObjectAndUnknownConstructorsAndClasses() { + assertEquals(Optional.empty(), ConstructorDelegation.of("java.lang.Object", List.of())); + assertEquals(Optional.empty(), ConstructorDelegation.of("java.lang.Exception", List.of("int"))); + assertEquals(Optional.empty(), ConstructorDelegation.of("does.not.Exist", List.of())); + } + + @Test + void readsOnlyJdkClasses() { + // on the test classpath, but not part of the JDK + assertEquals(Optional.empty(), ConstructorDelegation.of(getClass().getName(), List.of())); + } +}