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 000000000..82c1fa7ae --- /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 000000000..a41810cb5 --- /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-example/src/main/java/testSuite/CorrectOuterFieldAfterNestedClass.java b/liquidjava-example/src/main/java/testSuite/CorrectOuterFieldAfterNestedClass.java new file mode 100644 index 000000000..7c994eb20 --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/CorrectOuterFieldAfterNestedClass.java @@ -0,0 +1,12 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +class CorrectOuterFieldAfterNestedClass { + @Refinement("_ > 0") int x = 1; + + static class Inner { int y; } + + @Refinement("_ > 0") + public int get() { return x; } +} diff --git a/liquidjava-example/src/main/java/testSuite/ErrorNestedFieldLeak.java b/liquidjava-example/src/main/java/testSuite/ErrorNestedFieldLeak.java new file mode 100644 index 000000000..3ff32b16e --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/ErrorNestedFieldLeak.java @@ -0,0 +1,14 @@ +package testSuite; + +import liquidjava.specification.Refinement; + +class ErrorNestedFieldLeak { + int x = 1; + + static class Inner { + @Refinement("_ < 0") int x = -1; + } + + @Refinement("_ < 0") + public int get() { return x; } // Expect: Refinement Error +} diff --git a/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java b/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java new file mode 100644 index 000000000..4f7190cff --- /dev/null +++ b/liquidjava-example/src/main/java/testSuite/classes/forward_field_read_correct/ReadBefore.java @@ -0,0 +1,17 @@ +package testSuite.classes.forward_field_read_correct; + +import liquidjava.specification.Refinement; + +public class ReadBefore { + private final Job job = new Job(); + + @Refinement("_ >= 0") + public int get() { + return job.port; + } + + static class Job { + @Refinement("_ >= 0") + int port; + } +} 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 298179e60..b1d30f5fd 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/context/Context.java @@ -47,6 +47,27 @@ public void reinitializeContext() { clearInstanceVariables(); } + public ClassScope enterClassScope() { + ClassScope scope = new ClassScope(ctxVars, ctxInstanceVars); + reinitializeContext(); + return scope; + } + + public void exitClassScope(ClassScope scope) { + ctxVars = scope.variables; + ctxInstanceVars = scope.instances; + } + + public static class ClassScope { + private final Stack> variables; + private final List instances; + + private ClassScope(Stack> variables, List instances) { + this.variables = variables; + this.instances = instances; + } + } + public void clearInstanceVariables() { ctxInstanceVars = new ArrayList<>(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java index 3dda3881b..fcfdea182 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java @@ -32,41 +32,45 @@ public MethodsFirstChecker(Context context, Factory factory) { @Override public void visitCtClass(CtClass ctClass) { - context.reinitializeContext(); if (visitedClasses.contains(ctClass.getQualifiedName())) return; else visitedClasses.add(ctClass.getQualifiedName()); - // visitInterfaces - if (!ctClass.getSuperInterfaces().isEmpty()) - for (CtTypeReference t : ctClass.getSuperInterfaces()) { - if (t.isInterface()) { - CtType ct = t.getDeclaration(); - if (ct instanceof CtInterface) - visitCtInterface((CtInterface) ct); + Context.ClassScope scope = context.enterClassScope(); + try { + // visitInterfaces + if (!ctClass.getSuperInterfaces().isEmpty()) + for (CtTypeReference t : ctClass.getSuperInterfaces()) { + if (t.isInterface()) { + CtType ct = t.getDeclaration(); + if (ct instanceof CtInterface) + visitCtInterface((CtInterface) ct); + } } + // visitSubclasses + CtTypeReference sup = ctClass.getSuperclass(); + if (sup != null && sup.isClass()) { + CtType ct = sup.getDeclaration(); + if (ct instanceof CtClass) + visitCtClass((CtClass) ct); } - // visitSubclasses - CtTypeReference sup = ctClass.getSuperclass(); - if (sup != null && sup.isClass()) { - CtType ct = sup.getDeclaration(); - if (ct instanceof CtClass) - visitCtClass((CtClass) ct); - } - // first try-catch: process class-level annotations) - // errors here should not prevent visiting methods, constructors or fields of the class - try { - getRefinementFromAnnotation(ctClass); - handleStateSetsFromAnnotation(ctClass); - } catch (LJError e) { - diagnostics.add(e); - } - // second try-catch: visit class children (methods, constructors, fields) - // errors from one child should not prevent visiting sibling elements - try { - super.visitCtClass(ctClass); - } catch (LJError e) { - diagnostics.add(e); + // first try-catch: process class-level annotations) + // errors here should not prevent visiting methods, constructors or fields of the class + try { + getRefinementFromAnnotation(ctClass); + handleStateSetsFromAnnotation(ctClass); + } catch (LJError e) { + diagnostics.add(e); + } + // second try-catch: visit class children (methods, constructors, fields) + // errors from one child should not prevent visiting sibling elements + try { + super.visitCtClass(ctClass); + } catch (LJError e) { + diagnostics.add(e); + } + } finally { + context.exitClassScope(scope); } } 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 bf6dcc999..572349481 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; @@ -74,15 +75,14 @@ public RefinementTypeChecker(Context context, Factory factory) { @Override public void visitCtClass(CtClass ctClass) { - // System.out.println("CTCLASS:"+ctClass.getSimpleName()); - context.reinitializeContext(); - + Context.ClassScope scope = context.enterClassScope(); try { super.visitCtClass(ctClass); } catch (LJError e) { diagnostics.add(e); + } finally { + context.exitClassScope(scope); } - } @Override @@ -221,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 @@ -262,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); @@ -292,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))); @@ -308,6 +308,10 @@ public void visitCtFieldRead(CtFieldRead fieldRead) { Predicate.createEquals(Predicate.createVar(Keys.WILDCARD), Predicate.createVar(enumLiteral))); } else if (tryStaticFinalConstantRefinement(fieldRead)) { // refinement metadata set by helper + } else if (fieldRead.getVariable().getDeclaration() != null) { + Predicate declared = getRefinementFromAnnotation(fieldRead.getVariable().getDeclaration()) + .orElseGet(Predicate::new); + fieldRead.putMetadata(Keys.REFINEMENT, declared.substituteVariable(fieldName, Keys.WILDCARD)); } else { fieldRead.putMetadata(Keys.REFINEMENT, new Predicate()); // TODO DO WE WANT THIS OR TO SHOW ERROR MESSAGE? 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 550d67817..e547cdd05 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 4ed8fcae0..03d14b807 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 38f6b2efb..6c1e1d60b 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)