Fix collisions between same-named fields

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;
+    }
+}

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;
+    }
+}

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; }
+}

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
+}

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;
+    }
+}

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<List<RefinedVariable>> variables;
+        private final List<RefinedVariable> instances;
+
+        private ClassScope(Stack<List<RefinedVariable>> variables, List<RefinedVariable> instances) {
+            this.variables = variables;
+            this.instances = instances;
+        }
+    }
+
     public void clearInstanceVariables() {
         ctxInstanceVars = new ArrayList<>();
     }

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/MethodsFirstChecker.java

@@ -32,41 +32,45 @@ public MethodsFirstChecker(Context context, Factory factory) {
 
     @Override
     public <T> void visitCtClass(CtClass<T> 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);
         }
     }
 

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 <T> void visitCtClass(CtClass<T> 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 <T, A extends T> void visitAssignment(CtAssignment<T, A> 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 <T> void visitCtLiteral(CtLiteral<T> lit) {
     public <T> void visitCtField(CtField<T> f) {
         super.visitCtField(f);
         Optional<Predicate> 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 <T> void visitCtFieldRead(CtFieldRead<T> 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 <T> void visitCtFieldRead(CtFieldRead<T> 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?

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java

@@ -10,13 +10,15 @@
 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;
 import liquidjava.utils.constants.Types;
 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 <T> void getUnaryOpRefinements(CtUnaryOperator<T> operator) throws LJError {
         CtExpression<T> ex = (CtExpression<T>) 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<T> 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());

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/object_checkers/AuxStateHandler.java

@@ -180,13 +180,13 @@ private static ObjectState getStates(CtAnnotation<? extends Annotation> 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<? extends Annotation> 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;
             }