diff --git a/liquidjava-example/src/main/java/testSuite/CorrectCallResultReceiver.java b/liquidjava-example/src/main/java/testSuite/CorrectCallResultReceiver.java new file mode 100644 index 00000000..b1320f09 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectCallResultReceiver.java @@ -0,0 +1,30 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +class CorrectCallResultDoor { + @StateRefinement(to = "open(this)") + public CorrectCallResultDoor() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} + + @StateRefinement(to = "closed(this)") + public void slam() {} +} + +class CorrectCallResultHolder { + private final CorrectCallResultDoor door = new CorrectCallResultDoor(); + + CorrectCallResultDoor get() { + return door; + } +} + +public class CorrectCallResultReceiver { + static void use(CorrectCallResultHolder holder) { + holder.get().slam(); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumWithMethod.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumWithMethod.java new file mode 100644 index 00000000..62147557 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectEnumWithMethod.java @@ -0,0 +1,19 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +enum CorrectEnumWithMethodAction { + UNDO, REDO; + + String getText() { + return name(); + } +} + +public class CorrectEnumWithMethod { + static String describe(CorrectEnumWithMethodAction action) { + @Refinement("_ > 0") + int width = 1; + return action.getText() + width; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java b/liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java new file mode 100644 index 00000000..cb67dd7e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectVarargsCall.java @@ -0,0 +1,15 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +class CorrectVarargsLogger { + void debug(@Refinement("_ >= 0") int level, String format, Object... args) {} +} + +public class CorrectVarargsCall { + static void log(CorrectVarargsLogger logger, Object a, Object b) { + logger.debug(1, "{} and {}", a, b); + logger.debug(2, "nothing"); + logger.debug(3, "{}", new Object[] {a}); + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorCallResultReceiver.java b/liquidjava-example/src/main/java/testSuite/ErrorCallResultReceiver.java new file mode 100644 index 00000000..b50f6d5b --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorCallResultReceiver.java @@ -0,0 +1,27 @@ +package testSuite; + +import liquidjava.specification.StateRefinement; +import liquidjava.specification.StateSet; + +@StateSet({"open", "closed"}) +class ErrorCallResultDoor { + @StateRefinement(to = "open(this)") + public ErrorCallResultDoor() {} + + @StateRefinement(from = "open(this)", to = "closed(this)") + public void close() {} +} + +class ErrorCallResultHolder { + private final ErrorCallResultDoor door = new ErrorCallResultDoor(); + + ErrorCallResultDoor get() { + return door; + } +} + +public class ErrorCallResultReceiver { + static void use(ErrorCallResultHolder holder) { + holder.get().close(); // Expect: State Refinement Error + } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorVarargsCall.java b/liquidjava-example/src/main/java/testSuite/ErrorVarargsCall.java new file mode 100644 index 00000000..e01cde34 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorVarargsCall.java @@ -0,0 +1,13 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +class ErrorVarargsLogger { + void debug(@Refinement("_ >= 0") int level, String format, Object... args) {} +} + +public class ErrorVarargsCall { + static void log(ErrorVarargsLogger logger, Object a, Object b) { + logger.debug(-1, "{} and {}", a, b); // Expect: Refinement Error + } +} 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 df5bb976..077c1a74 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 @@ -21,6 +21,7 @@ import spoon.reflect.declaration.CtRecord; import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtField; +import spoon.reflect.declaration.CtEnum; import spoon.reflect.declaration.CtInterface; import spoon.reflect.declaration.CtMethod; import spoon.reflect.declaration.CtParameter; @@ -46,6 +47,11 @@ public void visitCtRecord(CtRecord ctRecord) { // records are user code, like classes: external specs are only read from interfaces } + @Override + public > void visitCtEnum(CtEnum ctEnum) { + // enums are user code too; their methods have no external target + } + @Override public void visitCtInterface(CtInterface intrface) { Optional> externalRef = getExternalRefinement(intrface); 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 cd686f24..92f0b9d2 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 @@ -419,7 +419,7 @@ private void applyReturnRefinement(CtElement invocation, RefinedFunction f, Map< private Map mapInvocation(List> arguments, RefinedFunction f) { Map mapInvocation = new HashMap<>(); List functionParams = f.getArguments(); - for (int i = 0; i < arguments.size(); i++) { + for (int i = 0; i < matchedArguments(arguments, functionParams); i++) { Variable fArg = functionParams.get(i); CtExpression iArg = arguments.get(i); String invStr; @@ -437,6 +437,16 @@ private Map mapInvocation(List> arguments, Refin return mapInvocation; } + /** + * The number of arguments bound one to one to parameters. A varargs call can pass more (or fewer) arguments than + * there are parameters; the ones collected into the varargs array are left out. + */ + private static int matchedArguments(List> arguments, List params) { + if (arguments.size() == params.size()) + return arguments.size(); + return Math.min(arguments.size(), Math.max(params.size() - 1, 0)); + } + private String createVariableRepresentingArgument(CtExpression iArg, Variable fArg) { Predicate met = (Predicate) iArg.getMetadata(Keys.REFINEMENT); if (met == null) @@ -451,7 +461,7 @@ private String createVariableRepresentingArgument(CtExpression iArg, Variable private void checkParameters(CtElement invocation, List> arguments, RefinedFunction f, Map map) throws LJError { List functionParams = f.getArguments(); - for (int i = 0; i < arguments.size(); i++) { + for (int i = 0; i < matchedArguments(arguments, functionParams); i++) { Variable fArg = functionParams.get(i); Predicate c = fArg.getMainRefinement(); c = c.substituteVariable(fArg.getName(), map.get(fArg.getName())); 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 089ef693..bbaec9af 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 @@ -848,6 +848,21 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, newCall.putMetadata(Keys.RECEIVER, receiver); invocation.putMetadata(Keys.TARGET, receiver); return name; + } else if (target2 instanceof CtInvocation call + && call.getMetadata(Keys.RECEIVER)instanceof RefinedVariable receiver) { + invocation.putMetadata(Keys.TARGET, receiver); + return receiver.getName(); + } else if (target2 instanceof CtInvocation call && call.getMetadata(Keys.TARGET) != null + && !isReturnValue(call)) { + // `a.get().method()` where get() has no return refinement: the call's TARGET is its own receiver (a), not + // the value it returns, so the receiver is a fresh value of the call's type, in a state not known here + String name = String.format(Formats.FRESH, tc.getContext().getCounter()); + CtTypeReference type = call.getType(); + RefinedVariable receiver = tc.getContext().addInstanceToContext(name, type, new Predicate(), call); + receiver.addSuperTypes(type.getSuperclass(), type.getSuperInterfaces()); + call.putMetadata(Keys.RECEIVER, receiver); + invocation.putMetadata(Keys.TARGET, receiver); + return name; } else if (target2.getMetadata(Keys.TARGET) != null) { VariableInstance target2Vi = (VariableInstance) target2.getMetadata(Keys.TARGET); Optional v = target2Vi.getParent(); @@ -857,6 +872,12 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, return null; } + /** Whether a call's TARGET metadata is the value it returns (set when its return refinement is applied). */ + private static boolean isReturnValue(CtInvocation call) { + return call.getMetadata(Keys.TARGET)instanceof VariableInstance vi + && vi.getName().equals(call.getMetadata(Keys.RETURN_VAR_NAME)); + } + static VariableInstance getTarget(CtElement invocation) { if (invocation.getMetadata(Keys.TARGET) != null) { return (VariableInstance) invocation.getMetadata(Keys.TARGET);