diff --git a/liquidjava-example/src/main/java/testSuite/CorrectCombinedNestedFields.java b/liquidjava-example/src/main/java/testSuite/CorrectCombinedNestedFields.java new file mode 100644 index 00000000..82c1fa7a --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectCombinedNestedFields.java @@ -0,0 +1,33 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class CorrectCombinedNestedFields { + @Refinement("_ < 0") + int port = -1; + + private final Job job = new Job(); + + static class Marker { + int value; + } + + @Refinement("_ < 0") + public int getOuterPort() { + return port; + } + + @Refinement("_ >= 0") + public int getJobPort() { + return job.port; + } + + public void send() { + job.port = 5; + } + + static class Job { + @Refinement("_ >= 0") + int port; + } +} diff --git a/liquidjava-example/src/main/java/testSuite/CorrectDistinctClassFields.java b/liquidjava-example/src/main/java/testSuite/CorrectDistinctClassFields.java new file mode 100644 index 00000000..a41810cb --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectDistinctClassFields.java @@ -0,0 +1,16 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +public class CorrectDistinctClassFields { + @Refinement("_ < 0") int port = -1; + private final Job job = new Job(); + + public void send() { + job.port = 5; + } + + static class Job { + @Refinement("_ >= 0") int port; + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java index 4ec745b2..57234948 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/RefinementTypeChecker.java @@ -15,6 +15,7 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.Enum; import liquidjava.utils.StaticConstants; +import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Types; @@ -220,7 +221,7 @@ private void visitAssignment(CtAssignment assignment) thr } else if (ex instanceof CtFieldWrite fw) { CtFieldReference cr = fw.getVariable(); CtField f = fw.getVariable().getDeclaration(); - String updatedVarName = String.format(Formats.THIS, cr.getSimpleName()); + String updatedVarName = Utils.qualifyFieldName(cr); checkAssignment(updatedVarName, cr.getType(), ex, assignment.getAssignment(), assignment, f); // corresponding ghost function update @@ -261,7 +262,7 @@ public void visitCtLiteral(CtLiteral lit) { public void visitCtField(CtField f) { super.visitCtField(f); Optional c = getRefinementFromAnnotation(f); - String name = String.format(Formats.THIS, f.getSimpleName()); + String name = Utils.qualifyFieldName(f.getReference()); Predicate ret = new Predicate(); if (c.isPresent()) { ret = c.get().substituteVariable(Keys.WILDCARD, name).substituteVariable(f.getSimpleName(), name); @@ -291,8 +292,8 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(fieldName))); } - } else if (context.hasVariable(String.format(Formats.THIS, fieldName))) { - String thisName = String.format(Formats.THIS, fieldName); + } else if (context.hasVariable(Utils.qualifyFieldName(fieldRead.getVariable()))) { + String thisName = Utils.qualifyFieldName(fieldRead.getVariable()); fieldRead.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(thisName))); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 550d6781..e547cdd0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -10,6 +10,7 @@ import liquidjava.processor.context.Variable; import liquidjava.processor.context.VariableInstance; import liquidjava.processor.refinement_checker.TypeChecker; +import liquidjava.utils.Utils; import liquidjava.utils.constants.Formats; import liquidjava.utils.constants.Keys; import liquidjava.utils.constants.Ops; @@ -17,6 +18,7 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; +import liquidjava.rj_language.ast.UnaryExpression; import org.apache.commons.lang3.NotImplementedException; import spoon.reflect.code.BinaryOperatorKind; import spoon.reflect.code.CtAssignment; @@ -121,12 +123,19 @@ public Predicate getOperatorAssignmentRefinement(String assignedName, CtOperator @SuppressWarnings({ "unchecked" }) public void getUnaryOpRefinements(CtUnaryOperator operator) throws LJError { CtExpression ex = (CtExpression) operator.getOperand(); + if (operator.getKind() == UnaryOperatorKind.NEG && ex instanceof CtLiteral literal + && literal.getValue() instanceof Number) { + Predicate operand = Predicate.createLit(literal.getValue().toString(), ex.getType().getQualifiedName()); + Predicate value = new Predicate(new UnaryExpression("-", operand.getExpression())); + operator.putMetadata(Keys.REFINEMENT, Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), value)); + return; + } String name = Formats.FRESH; Predicate all; if (ex instanceof CtVariableWrite w) { name = w.getVariable().getSimpleName(); - if (w instanceof CtFieldWrite) - name = String.format(Formats.THIS, name); + if (w instanceof CtFieldWrite fieldWrite) + name = Utils.qualifyFieldName(fieldWrite.getVariable()); all = getRefinementUnaryVariableWrite(ex, operator, w, name); rtc.checkVariableRefinements(all, name, w.getType(), operator, w.getVariable().getDeclaration()); return; @@ -203,8 +212,8 @@ private Predicate getOperationRefinements(CtBinaryOperator operator, CtVariab if (element instanceof CtVariableRead elemVar) { String elemName = elemVar.getVariable().getSimpleName(); - if (elemVar instanceof CtFieldRead) - elemName = String.format(Formats.THIS, elemName); + if (elemVar instanceof CtFieldRead fieldRead) + elemName = Utils.qualifyFieldName(fieldRead.getVariable()); Predicate elemRef = rtc.getContext().getVariableRefinements(elemName); String returnName = elemName; @@ -336,8 +345,8 @@ private Predicate getCurrentVariableValue(String name) { private Predicate getOperatorAssignmentRefinement(CtExpression element) throws LJError { if (element instanceof CtVariableRead variableRead) { String name = variableRead.getVariable().getSimpleName(); - if (variableRead instanceof CtFieldRead) - name = String.format(Formats.THIS, name); + if (variableRead instanceof CtFieldRead fieldRead) + name = Utils.qualifyFieldName(fieldRead.getVariable()); return getCurrentVariableValue(name); } else if (element instanceof CtBinaryOperator binaryOperator) { Predicate left = getOperatorAssignmentRefinement(binaryOperator.getLeftHandOperand()); 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 4ed8fcae..03d14b80 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 @@ -180,13 +180,13 @@ private static ObjectState getStates(CtAnnotation ctAnnota // has from if (from != null) { - state.setFrom(createStatePredicate(from, f.getTargetClass(), tc, e, false, prefix)); + state.setFrom(createStatePredicate(new Predicate(from, e, prefix), from, f.getTargetClass(), tc, e, false)); state.setFromPosition(Utils.getLJAnnotationPosition(e, from)); } // has to if (to != null) { - state.setTo(createStatePredicate(to, f.getTargetClass(), tc, e, true, prefix)); + state.setTo(createStatePredicate(new Predicate(to, e, prefix), to, f.getTargetClass(), tc, e, true)); state.setToPosition(Utils.getLJAnnotationPosition(e, to)); } @@ -209,10 +209,9 @@ private static ObjectState getStates(CtAnnotation ctAnnota * * @return the created predicate */ - private static Predicate createStatePredicate(String value, String targetClass, TypeChecker tc, CtElement e, - boolean isTo, String prefix) throws LJError { + private static Predicate createStatePredicate(Predicate p, String value, String targetClass, TypeChecker tc, + CtElement e, boolean isTo) throws LJError { SourcePosition position = Utils.getLJAnnotationPosition(e, value); - Predicate p = new Predicate(value, e, prefix); if (!p.getExpression().isBooleanExpression()) { throw new InvalidRefinementError(position, "State refinement transition must be a boolean expression", value); @@ -392,7 +391,7 @@ public static void checkTargetChanges(TypeChecker tc, RefinedFunction f, CtExpre */ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws LJError { CtField field = fw.getVariable().getDeclaration(); - String updatedVarName = String.format(Formats.THIS, fw.getVariable().getSimpleName()); + String updatedVarName = Utils.qualifyFieldName(fw.getVariable()); String targetClass = field.getDeclaringType().getQualifiedName(); // state transition annotation construction @@ -421,8 +420,12 @@ public static void updateGhostField(CtFieldWrite fw, TypeChecker tc) throws L ObjectState stateChange = new ObjectState(); String prefix = field.getDeclaringType().getQualifiedName(); - Predicate fromPredicate = createStatePredicate(stateChangeRefinementFrom, targetClass, tc, fw, false, prefix); - Predicate toPredicate = createStatePredicate(stateChangeRefinementTo, targetClass, tc, fw, true, prefix); + Predicate fromPredicate = createStatePredicate(new Predicate(), stateChangeRefinementFrom, targetClass, tc, fw, + false); + Predicate toPredicate = Predicate.createEquals(Predicate + .createInvocation(Utils.qualifyName(prefix, field.getSimpleName()), Predicate.createVar(Keys.THIS)), + Predicate.createVar(updatedVarName)); + toPredicate = createStatePredicate(toPredicate, stateChangeRefinementTo, targetClass, tc, fw, true); stateChange.setFrom(fromPredicate); stateChange.setTo(toPredicate); @@ -604,7 +607,7 @@ public static String prepareInvocationTarget(TypeChecker tc, CtElement target2, // means invocation is in a form of `t.method(args)` String name = v.getVariable().getSimpleName(); if (target2 instanceof CtFieldRead fieldRead && fieldRead.getTarget() instanceof CtThisAccess) { - String fieldName = String.format(Formats.THIS, name); + String fieldName = Utils.qualifyFieldName(fieldRead.getVariable()); if (tc.getContext().hasVariable(fieldName)) name = fieldName; } diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java index 38f6b2ef..6c1e1d60 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java +++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java @@ -19,6 +19,7 @@ import spoon.reflect.declaration.CtElement; import spoon.reflect.declaration.CtMethod; import spoon.reflect.factory.Factory; +import spoon.reflect.reference.CtFieldReference; import spoon.reflect.reference.CtTypeReference; import spoon.support.reflect.cu.position.SourcePositionImpl; @@ -50,6 +51,10 @@ public static String qualifyName(String prefix, String name) { return String.format("%s.%s", prefix, name); } + public static String qualifyFieldName(CtFieldReference field) { + return "this#" + field.getDeclaringType().getQualifiedName() + "." + field.getSimpleName(); + } + public static String getFile(CtElement element) { SourcePosition pos = element.getPosition(); if (pos == null || pos.getFile() == null)