Preserve enclosing class refinements across nested classes

Author: rcosta358

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

@@ -74,15 +74,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